diff options
author | Alan Mishchenko <alanmi@berkeley.edu> | 2008-06-11 08:01:00 -0700 |
---|---|---|
committer | Alan Mishchenko <alanmi@berkeley.edu> | 2008-06-11 08:01:00 -0700 |
commit | d0341836ddb38ccc087bdac3df4e8b2ff7fe7a8f (patch) | |
tree | e77965a44562efdb045b5a9c5d565986b4f65623 /src/aig/ntl/ntlCheck.c | |
parent | 9d09f583b6ea1181ebd5af1654acd3432c427445 (diff) | |
download | abc-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.c | 77 |
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; } |