diff options
Diffstat (limited to 'src/aig')
-rw-r--r-- | src/aig/aig/aigDfs.c | 7 | ||||
-rw-r--r-- | src/aig/ntl/ntl.h | 5 | ||||
-rw-r--r-- | src/aig/ntl/ntlEc.c | 7 | ||||
-rw-r--r-- | src/aig/ntl/ntlExtract.c | 10 | ||||
-rw-r--r-- | src/aig/ntl/ntlReadBlif.c | 42 | ||||
-rw-r--r-- | src/aig/ntl/ntlSweep.c | 6 | ||||
-rw-r--r-- | src/aig/ntl/ntlWriteBlif.c | 2 | ||||
-rw-r--r-- | src/aig/nwk/nwkDfs.c | 12 |
8 files changed, 86 insertions, 5 deletions
diff --git a/src/aig/aig/aigDfs.c b/src/aig/aig/aigDfs.c index 9f7d286d..47597f93 100644 --- a/src/aig/aig/aigDfs.c +++ b/src/aig/aig/aigDfs.c @@ -448,6 +448,13 @@ int Aig_ManChoiceLevel( Aig_Man_t * p ) if ( LevelMax < Aig_ObjLevel(pObj) ) LevelMax = Aig_ObjLevel(pObj); } + // account for dangling boxes + Aig_ManForEachPi( p, pObj, i ) + { + Aig_ManChoiceLevel_rec( p, pObj ); + if ( LevelMax < Aig_ObjLevel(pObj) ) + LevelMax = Aig_ObjLevel(pObj); + } Aig_ManCleanPioNumbers( p ); // Aig_ManForEachNode( p, pObj, i ) // assert( Aig_ObjLevel(pObj) > 0 ); diff --git a/src/aig/ntl/ntl.h b/src/aig/ntl/ntl.h index 1028bd97..659f6c60 100644 --- a/src/aig/ntl/ntl.h +++ b/src/aig/ntl/ntl.h @@ -86,6 +86,7 @@ struct Ntl_Mod_t_ Vec_Ptr_t * vPis; // the array of PI objects Vec_Ptr_t * vPos; // the array of PO objects int nObjs[NTL_OBJ_VOID]; // counter of objects of each type + int fKeep; // indicates persistant model // hashing names into nets Ntl_Net_t ** pTable; // the hash table of names into nets int nTableSize; // the allocated table size @@ -219,9 +220,9 @@ static inline void Ntl_ObjSetFanout( Ntl_Obj_t * p, Ntl_Net_t * pNet, int for ( pNet = pNwk->pTable[i]; pNet; pNet = pNet->pNext ) #define Ntl_ObjForEachFanin( pObj, pFanin, i ) \ - for ( i = 0; (i < (pObj)->nFanins) && ((pFanin) = (pObj)->pFanio[i]); i++ ) + for ( i = 0; (i < (pObj)->nFanins) && (((pFanin) = (pObj)->pFanio[i]), 1); i++ ) #define Ntl_ObjForEachFanout( pObj, pFanout, i ) \ - for ( i = 0; (i < (pObj)->nFanouts) && ((pFanout) = (pObj)->pFanio[(pObj)->nFanins+i]); i++ ) + for ( i = 0; (i < (pObj)->nFanouts) && (((pFanout) = (pObj)->pFanio[(pObj)->nFanins+i]), 1); i++ ) //////////////////////////////////////////////////////////////////////// /// FUNCTION DECLARATIONS /// diff --git a/src/aig/ntl/ntlEc.c b/src/aig/ntl/ntlEc.c index 0cd75cbc..8c7f7156 100644 --- a/src/aig/ntl/ntlEc.c +++ b/src/aig/ntl/ntlEc.c @@ -226,6 +226,13 @@ void Ntl_ManPrepareCec( char * pFileName1, char * pFileName2, Aig_Man_t ** ppMan } // normalize inputs/outputs Ntl_ManCreateMissingInputs( pModel1, pModel2, 0 ); + if ( Ntl_ModelCiNum(pModel1) != Ntl_ModelCiNum(pModel2) ) + { + if ( pMan1 ) Ntl_ManFree( pMan1 ); + if ( pMan2 ) Ntl_ManFree( pMan2 ); + printf( "Ntl_ManPrepareCec(): Cannot verify designs with too many different CIs.\n" ); + return; + } Ntl_ManDeriveCommonCis( pMan1, pMan2, 0 ); Ntl_ManDeriveCommonCos( pMan1, pMan2, 0 ); if ( Vec_PtrSize(pMan1->vCos) == 0 ) diff --git a/src/aig/ntl/ntlExtract.c b/src/aig/ntl/ntlExtract.c index 69219282..a6fb58ae 100644 --- a/src/aig/ntl/ntlExtract.c +++ b/src/aig/ntl/ntlExtract.c @@ -289,6 +289,16 @@ Aig_Man_t * Ntl_ManExtract( Ntl_Man_t * p ) Vec_PtrPush( p->vCos, pNet ); Aig_ObjCreatePo( p->pAig, pNet->pCopy ); } + // visit dangling boxes + Ntl_ModelForEachBox( pRoot, pObj, i ) + { + pNet = Ntl_ObjFanout0(pObj); + if ( !Ntl_ManExtract_rec( p, pNet ) ) + { + printf( "Ntl_ManExtract(): Error: Combinational loop is detected.\n" ); + return 0; + } + } // report the number of dangling objects nUselessObjects = Ntl_ModelNodeNum(pRoot) + Ntl_ModelLut1Num(pRoot) + Ntl_ModelBoxNum(pRoot) - Vec_PtrSize(p->vNodes); // if ( nUselessObjects ) diff --git a/src/aig/ntl/ntlReadBlif.c b/src/aig/ntl/ntlReadBlif.c index 13050047..cac53058 100644 --- a/src/aig/ntl/ntlReadBlif.c +++ b/src/aig/ntl/ntlReadBlif.c @@ -31,6 +31,7 @@ struct Ioa_ReadMod_t_ { // file lines char * pFirst; // .model line + char * pAttrib; // .attrib line Vec_Ptr_t * vInputs; // .inputs lines Vec_Ptr_t * vOutputs; // .outputs lines Vec_Ptr_t * vLatches; // .latch lines @@ -78,6 +79,7 @@ static void Ioa_ReadReadPreparse( Ioa_ReadMan_t * p ); static int Ioa_ReadReadInterfaces( Ioa_ReadMan_t * p ); static Ntl_Man_t * Ioa_ReadParse( Ioa_ReadMan_t * p ); static int Ioa_ReadParseLineModel( Ioa_ReadMod_t * p, char * pLine ); +static int Ioa_ReadParseLineAttrib( Ioa_ReadMod_t * p, char * pLine ); static int Ioa_ReadParseLineInputs( Ioa_ReadMod_t * p, char * pLine ); static int Ioa_ReadParseLineOutputs( Ioa_ReadMod_t * p, char * pLine ); static int Ioa_ReadParseLineLatch( Ioa_ReadMod_t * p, char * pLine ); @@ -519,6 +521,8 @@ static void Ioa_ReadReadPreparse( Ioa_ReadMan_t * p ) p->pLatest->pFirst = pCur; p->pLatest->pMan = p; } + else if ( !strncmp(pCur, "attrib", 6) ) + p->pLatest->pAttrib = pCur; else if ( !strncmp(pCur, "end", 3) ) { if ( p->pLatest ) @@ -562,6 +566,9 @@ static int Ioa_ReadReadInterfaces( Ioa_ReadMan_t * p ) // parse the model if ( !Ioa_ReadParseLineModel( pMod, pMod->pFirst ) ) return 0; + // parse the model attributes + if ( pMod->pAttrib && !Ioa_ReadParseLineAttrib( pMod, pMod->pAttrib ) ) + return 0; // parse the inputs Vec_PtrForEachEntry( pMod->vInputs, pLine, k ) if ( !Ioa_ReadParseLineInputs( pMod, pLine ) ) @@ -651,7 +658,7 @@ static int Ioa_ReadParseLineModel( Ioa_ReadMod_t * p, char * pLine ) assert( !strcmp(pToken, "model") ); if ( Vec_PtrSize(vTokens) != 2 ) { - sprintf( p->pMan->sError, "Line %d: The number of entries in .model line (%d) is different from two.", Ioa_ReadGetLine(p->pMan, pToken), Vec_PtrSize(vTokens) ); + sprintf( p->pMan->sError, "Line %d: The number of entries (%d) in .model line is different from two.", Ioa_ReadGetLine(p->pMan, pToken), Vec_PtrSize(vTokens) ); return 0; } p->pNtk = Ntl_ModelAlloc( p->pMan->pDesign, Vec_PtrEntry(vTokens, 1) ); @@ -660,6 +667,39 @@ static int Ioa_ReadParseLineModel( Ioa_ReadMod_t * p, char * pLine ) /**Function************************************************************* + Synopsis [Parses the model line.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +static int Ioa_ReadParseLineAttrib( Ioa_ReadMod_t * p, char * pLine ) +{ + Vec_Ptr_t * vTokens = p->pMan->vTokens; + char * pToken; + Ioa_ReadSplitIntoTokens( vTokens, pLine, '\0' ); + pToken = Vec_PtrEntry( vTokens, 0 ); + assert( !strcmp(pToken, "attrib") ); + if ( Vec_PtrSize(vTokens) != 2 ) + { + sprintf( p->pMan->sError, "Line %d: The number of entries (%d) in .attrib line is different from two.", Ioa_ReadGetLine(p->pMan, pToken), Vec_PtrSize(vTokens) ); + return 0; + } + if ( strcmp( Vec_PtrEntry(vTokens, 1), "keep" ) == 0 ) + p->pNtk->fKeep = 1; + else + { + sprintf( p->pMan->sError, "Line %d: Unknown attribute (%s) in the .attrib line of model %s.", Ioa_ReadGetLine(p->pMan, pToken), Vec_PtrEntry(vTokens, 1), p->pNtk->pName ); + return 0; + } + return 1; +} + +/**Function************************************************************* + Synopsis [Parses the inputs line.] Description [] diff --git a/src/aig/ntl/ntlSweep.c b/src/aig/ntl/ntlSweep.c index 000b8f0a..ed602297 100644 --- a/src/aig/ntl/ntlSweep.c +++ b/src/aig/ntl/ntlSweep.c @@ -77,11 +77,15 @@ void Ntl_ManSweepMark( Ntl_Man_t * p ) // start from the primary outputs Ntl_ModelForEachPo( pRoot, pObj, i ) Ntl_ManSweepMark_rec( p, pObj ); + // start from the persistant boxes + Ntl_ModelForEachBox( pRoot, pObj, i ) + if ( pObj->pImplem->fKeep ) + Ntl_ManSweepMark_rec( p, pObj ); } /**Function************************************************************* - Synopsis [Derives new netlist by sweeping current netlist with the current AIG.] + Synopsis [Removes logic that does not fanout into POs.] Description [] diff --git a/src/aig/ntl/ntlWriteBlif.c b/src/aig/ntl/ntlWriteBlif.c index ed45fcaf..9814ed5d 100644 --- a/src/aig/ntl/ntlWriteBlif.c +++ b/src/aig/ntl/ntlWriteBlif.c @@ -47,6 +47,8 @@ void Ioa_WriteBlifModel( FILE * pFile, Ntl_Mod_t * pModel ) float Delay; int i, k, fClockAdded = 0; fprintf( pFile, ".model %s\n", pModel->pName ); + if ( pModel->fKeep ) + fprintf( pFile, ".attrib keep\n" ); fprintf( pFile, ".inputs" ); Ntl_ModelForEachPi( pModel, pObj, i ) fprintf( pFile, " %s", Ntl_ObjFanout0(pObj)->pName ); diff --git a/src/aig/nwk/nwkDfs.c b/src/aig/nwk/nwkDfs.c index 90bab0dc..ec4ad440 100644 --- a/src/aig/nwk/nwkDfs.c +++ b/src/aig/nwk/nwkDfs.c @@ -222,6 +222,12 @@ int Nwk_ManLevel( Nwk_Man_t * pNtk ) if ( LevelMax < Nwk_ObjLevel(pObj) ) LevelMax = Nwk_ObjLevel(pObj); } + Nwk_ManForEachCi( pNtk, pObj, i ) + { + Nwk_ManLevel_rec( pObj ); + if ( LevelMax < Nwk_ObjLevel(pObj) ) + LevelMax = Nwk_ObjLevel(pObj); + } return LevelMax; } @@ -297,7 +303,7 @@ void Nwk_ManDfs_rec( Nwk_Obj_t * pObj, Vec_Ptr_t * vNodes ) Nwk_ManDfs_rec( pNext, vNodes ); Vec_PtrPush( vNodes, pObj ); } - + /**Function************************************************************* Synopsis [Returns the DFS ordered array of all objects except latches.] @@ -448,6 +454,10 @@ Vec_Ptr_t * Nwk_ManDfsReverse( Nwk_Man_t * pNtk ) vNodes = Vec_PtrAlloc( 100 ); Nwk_ManForEachPi( pNtk, pObj, i ) Nwk_ManDfsReverse_rec( pObj, vNodes ); + // add nodes without fanins + Nwk_ManForEachNode( pNtk, pObj, i ) + if ( Nwk_ObjFaninNum(pObj) == 0 && !Nwk_ObjIsTravIdCurrent(pObj) ) + Vec_PtrPush( vNodes, pObj ); return vNodes; } |