summaryrefslogtreecommitdiffstats
path: root/src/aig/ntl/ntlCheck.c
diff options
context:
space:
mode:
authorAlan Mishchenko <alanmi@berkeley.edu>2008-06-11 08:01:00 -0700
committerAlan Mishchenko <alanmi@berkeley.edu>2008-06-11 08:01:00 -0700
commitd0341836ddb38ccc087bdac3df4e8b2ff7fe7a8f (patch)
treee77965a44562efdb045b5a9c5d565986b4f65623 /src/aig/ntl/ntlCheck.c
parent9d09f583b6ea1181ebd5af1654acd3432c427445 (diff)
downloadabc-d0341836ddb38ccc087bdac3df4e8b2ff7fe7a8f.tar.gz
abc-d0341836ddb38ccc087bdac3df4e8b2ff7fe7a8f.tar.bz2
abc-d0341836ddb38ccc087bdac3df4e8b2ff7fe7a8f.zip
Version abc80611
Diffstat (limited to 'src/aig/ntl/ntlCheck.c')
-rw-r--r--src/aig/ntl/ntlCheck.c77
1 files changed, 71 insertions, 6 deletions
diff --git a/src/aig/ntl/ntlCheck.c b/src/aig/ntl/ntlCheck.c
index d3aecc8d..b4125804 100644
--- a/src/aig/ntl/ntlCheck.c
+++ b/src/aig/ntl/ntlCheck.c
@@ -31,6 +31,61 @@
/**Function*************************************************************
+ Synopsis []
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+int Ntl_ModelCheckCombPoPaths_rec( Ntl_Mod_t * pModel, Ntl_Net_t * pNet )
+{
+ Ntl_Net_t * pFanin;
+ int i;
+ // skip visited nets
+ if ( pNet->nVisits == 2 )
+ return 1;
+ pNet->nVisits = 2;
+ // process PIs
+ if ( Ntl_ObjIsPi(pNet->pDriver) )
+ return 0;
+ // process registers
+ if ( Ntl_ObjIsLatch(pNet->pDriver) )
+ return 1;
+ assert( Ntl_ObjIsNode(pNet->pDriver) );
+ // call recursively
+ Ntl_ObjForEachFanin( pNet->pDriver, pFanin, i )
+ if ( !Ntl_ModelCheckCombPoPaths_rec( pModel, pFanin ) )
+ return 0;
+ return 1;
+}
+
+/**Function*************************************************************
+
+ Synopsis [Checks the existence of combinational paths from POs to PIs.]
+
+ Description [Returns 0 if the path is found.]
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+int Ntl_ModelCheckCombPoPaths( Ntl_Mod_t * pModel )
+{
+ Ntl_Obj_t * pObj;
+ int i;
+ Ntl_ModelClearNets( pModel );
+ Ntl_ModelForEachPo( pModel, pObj, i )
+ if ( !Ntl_ModelCheckCombPoPaths_rec( pModel, Ntl_ObjFanin0(pObj) ) )
+ return 0;
+ return 1;
+}
+
+/**Function*************************************************************
+
Synopsis [Checks one model.]
Description []
@@ -91,14 +146,14 @@ int Ntl_ModelCheck( Ntl_Mod_t * pModel, int fMain )
printf( "Warning: Seq model %s does not have input arrival/required time info. Default 0.0 is assumed.\n", pModel->pName );
pModel->vTimeInputs = Vec_IntAlloc( 2 );
Vec_IntPush( pModel->vTimeInputs, -1 );
- Vec_IntPush( pModel->vTimeInputs, Aig_Float2Int(1.0) );
+ Vec_IntPush( pModel->vTimeInputs, Aig_Float2Int(0.0) );
}
if ( pModel->vTimeOutputs == NULL )
{
- printf( "Warning: Seq model %s does not have output arrival/required time info. Default 0.0 is assumed.\n", pModel->pName );
+// printf( "Warning: Seq model %s does not have output arrival/required time info. Default 0.0 is assumed.\n", pModel->pName );
pModel->vTimeOutputs = Vec_IntAlloc( 2 );
Vec_IntPush( pModel->vTimeOutputs, -1 );
- Vec_IntPush( pModel->vTimeOutputs, Aig_Float2Int(1.0) );
+ Vec_IntPush( pModel->vTimeOutputs, Aig_Float2Int(0.0) );
}
}
@@ -122,12 +177,22 @@ int Ntl_ModelCheck( Ntl_Mod_t * pModel, int fMain )
// this is a white box
if ( pModel->attrComb && Ntl_ModelNodeNum(pModel) + Ntl_ModelLut1Num(pModel) == 0 )
{
- printf( "Model %s is a comb blackbox, yet it has no nodes.\n", pModel->pName );
+ printf( "Model %s is a comb white box, yet it has no nodes.\n", pModel->pName );
+ fStatus = 0;
+ }
+ if ( pModel->attrComb && Ntl_ModelLatchNum(pModel) > 0 )
+ {
+ printf( "Model %s is a comb white box, yet it has registers.\n", pModel->pName );
fStatus = 0;
}
if ( !pModel->attrComb && Ntl_ModelLatchNum(pModel) == 0 )
{
- printf( "Model %s is a seq blackbox, yet it has no registers.\n", pModel->pName );
+ printf( "Model %s is a seq white box, yet it has no registers.\n", pModel->pName );
+ fStatus = 0;
+ }
+ if ( !pModel->attrComb && !Ntl_ModelCheckCombPoPaths(pModel) )
+ {
+ printf( "Model %s is a seq white box with comb paths from PIs to POs.\n", pModel->pName );
fStatus = 0;
}
}
@@ -292,7 +357,7 @@ void Ntl_ModelTransformLatches( Ntl_Mod_t * pModel )
pLatch->pImplem = pMod[Init];
pLatch->Type = NTL_OBJ_BOX;
}
- printf( "Root level model %s: %d registers turned into white seq boxes.\n", pModel->pName, Ntl_ModelLatchNum(pModel) );
+ printf( "In the main model \"%s\", %d latches are transformed into white seq boxes.\n", pModel->pName, Ntl_ModelLatchNum(pModel) );
pModel->nObjs[NTL_OBJ_BOX] += Ntl_ModelLatchNum(pModel);
pModel->nObjs[NTL_OBJ_LATCH] = 0;
}