diff options
Diffstat (limited to 'src/aig/ntl')
| -rw-r--r-- | src/aig/ntl/ntl.h | 32 | ||||
| -rw-r--r-- | src/aig/ntl/ntlCheck.c | 77 | ||||
| -rw-r--r-- | src/aig/ntl/ntlExtract.c | 198 | ||||
| -rw-r--r-- | src/aig/ntl/ntlInsert.c | 52 | ||||
| -rw-r--r-- | src/aig/ntl/ntlMan.c | 101 | ||||
| -rw-r--r-- | src/aig/ntl/ntlMap.c | 2 | ||||
| -rw-r--r-- | src/aig/ntl/ntlObj.c | 27 | ||||
| -rw-r--r-- | src/aig/ntl/ntlReadBlif.c | 15 | ||||
| -rw-r--r-- | src/aig/ntl/ntlTable.c | 44 | ||||
| -rw-r--r-- | src/aig/ntl/ntlTime.c | 2 |
10 files changed, 431 insertions, 119 deletions
diff --git a/src/aig/ntl/ntl.h b/src/aig/ntl/ntl.h index 72a5674b..6d4f5c29 100644 --- a/src/aig/ntl/ntl.h +++ b/src/aig/ntl/ntl.h @@ -31,7 +31,7 @@ extern "C" { #include "aig.h" #include "tim.h" -#include "ntk.h" +#include "nwk.h" //////////////////////////////////////////////////////////////////////// /// PARAMETERS /// @@ -94,11 +94,14 @@ struct Ntl_Mod_t_ Vec_Int_t * vArrivals; Vec_Int_t * vRequireds; float * pDelayTable; + // other data members + void * pCopy; }; struct Ntl_Obj_t_ { Ntl_Mod_t * pModel; // the model + void * pCopy; // the copy of this object unsigned Type : 3; // object type unsigned Id : 27; // object ID unsigned MarkA : 1; // temporary mark @@ -115,9 +118,9 @@ struct Ntl_Obj_t_ struct Ntl_Net_t_ { - Ntl_Obj_t * pDriver; // driver of the net Ntl_Net_t * pNext; // next net in the hash table - Aig_Obj_t * pFunc; // the AIG representation + void * pCopy; // the copy of this object + Ntl_Obj_t * pDriver; // driver of the net char nVisits; // the number of times the net is visited char fMark; // temporary mark char pName[0]; // the name of this net @@ -140,6 +143,8 @@ struct Ntl_Lut_t_ /// INLINED FUNCTIONS /// //////////////////////////////////////////////////////////////////////// +static inline Ntl_Mod_t * Ntl_ManRootModel( Ntl_Man_t * p ) { return Vec_PtrEntry( p->vModels, 0 ); } + static inline int Ntl_ModelPiNum( Ntl_Mod_t * p ) { return p->nObjs[NTL_OBJ_PI]; } static inline int Ntl_ModelPoNum( Ntl_Mod_t * p ) { return p->nObjs[NTL_OBJ_PO]; } static inline int Ntl_ModelNodeNum( Ntl_Mod_t * p ) { return p->nObjs[NTL_OBJ_NODE]; } @@ -169,7 +174,7 @@ static inline Ntl_Net_t * Ntl_ObjFanin0( Ntl_Obj_t * p ) { return p->pF static inline Ntl_Net_t * Ntl_ObjFanout0( Ntl_Obj_t * p ) { return p->pFanio[p->nFanins]; } static inline Ntl_Net_t * Ntl_ObjFanin( Ntl_Obj_t * p, int i ) { return p->pFanio[i]; } -static inline Ntl_Net_t * Ntl_ObjFanout( Ntl_Obj_t * p, int i ) { return p->pFanio[p->nFanins+1]; } +static inline Ntl_Net_t * Ntl_ObjFanout( Ntl_Obj_t * p, int i ) { return p->pFanio[p->nFanins+i]; } static inline void Ntl_ObjSetFanin( Ntl_Obj_t * p, Ntl_Net_t * pNet, int i ) { p->pFanio[i] = pNet; } static inline void Ntl_ObjSetFanout( Ntl_Obj_t * p, Ntl_Net_t * pNet, int i ) { p->pFanio[p->nFanins+i] = pNet; pNet->pDriver = p; } @@ -186,10 +191,10 @@ static inline void Ntl_ObjSetFanout( Ntl_Obj_t * p, Ntl_Net_t * pNet, int Vec_PtrForEachEntry( p->vCos, pNtl, i ) #define Ntl_ManForEachNode( p, pObj, i ) \ for ( i = 0; (i < Vec_PtrSize(p->vNodes)) && (((pObj) = Vec_PtrEntry(p->vNodes, i)), 1); i++ ) \ - if ( !Ntl_ObjIsNode(pObj) ) {} else + if ( (pObj) == NULL || !Ntl_ObjIsNode(pObj) ) {} else #define Ntl_ManForEachBox( p, pObj, i ) \ for ( i = 0; (i < Vec_PtrSize(p->vNodes)) && (((pObj) = Vec_PtrEntry(p->vNodes, i)), 1); i++ ) \ - if ( !Ntl_ObjIsBox(pObj) ) {} else + if ( (pObj) == NULL || !Ntl_ObjIsBox(pObj) ) {} else #define Ntl_ModelForEachPi( pNtl, pObj, i ) \ Vec_PtrForEachEntry( pNtl->vPis, pObj, i ) @@ -200,13 +205,13 @@ static inline void Ntl_ObjSetFanout( Ntl_Obj_t * p, Ntl_Net_t * pNet, int if ( pObj == NULL ) {} else #define Ntl_ModelForEachLatch( pNtl, pObj, i ) \ for ( i = 0; (i < Vec_PtrSize(pNtl->vObjs)) && (((pObj) = Vec_PtrEntry(pNtl->vObjs, i)), 1); i++ ) \ - if ( !Ntl_ObjIsLatch(pObj) ) {} else + if ( (pObj) == NULL || !Ntl_ObjIsLatch(pObj) ) {} else #define Ntl_ModelForEachNode( pNtl, pObj, i ) \ for ( i = 0; (i < Vec_PtrSize(pNtl->vObjs)) && (((pObj) = Vec_PtrEntry(pNtl->vObjs, i)), 1); i++ ) \ - if ( !Ntl_ObjIsNode(pObj) ) {} else + if ( (pObj) == NULL || !Ntl_ObjIsNode(pObj) ) {} else #define Ntl_ModelForEachBox( pNtl, pObj, i ) \ for ( i = 0; (i < Vec_PtrSize(pNtl->vObjs)) && (((pObj) = Vec_PtrEntry(pNtl->vObjs, i)), 1); i++ ) \ - if ( !Ntl_ObjIsBox(pObj) ) {} else + if ( (pObj) == NULL || !Ntl_ObjIsBox(pObj) ) {} else #define Ntl_ModelForEachNet( pNtl, pNet, i ) \ for ( i = 0; i < pNtl->nTableSize; i++ ) \ for ( pNet = pNtl->pTable[i]; pNet; pNet = pNet->pNext ) @@ -225,21 +230,25 @@ extern int Ntl_ManInsertTest( Ntl_Man_t * p, Aig_Man_t * pAig ); extern int Ntl_ManInsertTestIf( Ntl_Man_t * p, Aig_Man_t * pAig ); /*=== ntlExtract.c ==========================================================*/ extern Aig_Man_t * Ntl_ManExtract( Ntl_Man_t * p ); +extern Aig_Man_t * Ntl_ManCollapse( Ntl_Man_t * p ); extern char * Ntl_SopFromTruth( Ntl_Man_t * p, unsigned * pTruth, int nVars, Vec_Int_t * vCover ); /*=== ntlInsert.c ==========================================================*/ extern int Ntl_ManInsert( Ntl_Man_t * p, Vec_Ptr_t * vMapping, Aig_Man_t * pAig ); -extern int Ntl_ManInsertNtk( Ntl_Man_t * p, Ntk_Man_t * pNtk ); +extern int Ntl_ManInsertNtk( Ntl_Man_t * p, Nwk_Man_t * pNtk ); /*=== ntlCheck.c ==========================================================*/ extern int Ntl_ManCheck( Ntl_Man_t * pMan ); extern int Ntl_ModelCheck( Ntl_Mod_t * pModel ); extern void Ntl_ModelFixNonDrivenNets( Ntl_Mod_t * pModel ); /*=== ntlMan.c ============================================================*/ extern Ntl_Man_t * Ntl_ManAlloc( char * pFileName ); +extern Ntl_Man_t * Ntl_ManStartFrom( Ntl_Man_t * p ); +extern Ntl_Man_t * Ntl_ManDup( Ntl_Man_t * p ); extern void Ntl_ManFree( Ntl_Man_t * p ); extern Ntl_Mod_t * Ntl_ManFindModel( Ntl_Man_t * p, char * pName ); extern void Ntl_ManPrintStats( Ntl_Man_t * p ); extern Tim_Man_t * Ntl_ManReadTimeMan( Ntl_Man_t * p ); extern Ntl_Mod_t * Ntl_ModelAlloc( Ntl_Man_t * pMan, char * pName ); +extern Ntl_Mod_t * Ntl_ModelDup( Ntl_Man_t * pManNew, Ntl_Mod_t * pModelOld ); extern void Ntl_ModelFree( Ntl_Mod_t * p ); /*=== ntlMap.c ============================================================*/ extern Vec_Ptr_t * Ntl_MappingAlloc( int nLuts, int nVars ); @@ -252,14 +261,15 @@ extern Ntl_Obj_t * Ntl_ModelCreatePo( Ntl_Mod_t * pModel, Ntl_Net_t * pNet ) extern Ntl_Obj_t * Ntl_ModelCreateLatch( Ntl_Mod_t * pModel ); extern Ntl_Obj_t * Ntl_ModelCreateNode( Ntl_Mod_t * pModel, int nFanins ); extern Ntl_Obj_t * Ntl_ModelCreateBox( Ntl_Mod_t * pModel, int nFanins, int nFanouts ); +extern Ntl_Obj_t * Ntl_ModelDupObj( Ntl_Mod_t * pModel, Ntl_Obj_t * pOld ); extern char * Ntl_ManStoreName( Ntl_Man_t * p, char * pName ); extern char * Ntl_ManStoreSop( Ntl_Man_t * p, char * pSop ); extern char * Ntl_ManStoreFileName( Ntl_Man_t * p, char * pFileName ); /*=== ntlTable.c ==========================================================*/ extern Ntl_Net_t * Ntl_ModelFindNet( Ntl_Mod_t * p, char * pName ); extern Ntl_Net_t * Ntl_ModelFindOrCreateNet( Ntl_Mod_t * p, char * pName ); -extern int Ntl_ModelSetNetDriver( Ntl_Obj_t * pObj, Ntl_Net_t * pNet ); extern int Ntl_ModelFindPioNumber( Ntl_Mod_t * p, char * pName, int * pNumber ); +extern int Ntl_ModelSetNetDriver( Ntl_Obj_t * pObj, Ntl_Net_t * pNet ); /*=== ntlTime.c ==========================================================*/ extern Tim_Man_t * Ntl_ManCreateTiming( Ntl_Man_t * p ); /*=== ntlReadBlif.c ==========================================================*/ diff --git a/src/aig/ntl/ntlCheck.c b/src/aig/ntl/ntlCheck.c index d01c7d5e..5973e967 100644 --- a/src/aig/ntl/ntlCheck.c +++ b/src/aig/ntl/ntlCheck.c @@ -40,11 +40,40 @@ SeeAlso [] ***********************************************************************/ -int Ntl_ManCheck( Ntl_Man_t * pMan ) +int Ntl_ModelCheck( Ntl_Mod_t * pModel ) { - // check that the models have unique names - // check that the models (except the first one) do not have boxes - return 1; + Ntl_Obj_t * pObj; + Ntl_Net_t * pNet; + int i, k, fStatus = 1; + Ntl_ModelForEachNet( pModel, pNet, i ) + { + if ( pNet->pName == NULL ) + { + printf( "Net %d does not have a name\n", i ); + fStatus = 0; + } + if ( pNet->pDriver == NULL ) + { + printf( "Net %d (%s) does not have a driver\n", i, pNet->pName ); + fStatus = 0; + } + } + Ntl_ModelForEachObj( pModel, pObj, i ) + { + Ntl_ObjForEachFanin( pObj, pNet, k ) + if ( pNet == NULL ) + { + printf( "Object %d does not have fanin net %d\n", i, k ); + fStatus = 0; + } + Ntl_ObjForEachFanout( pObj, pNet, k ) + if ( pNet == NULL ) + { + printf( "Object %d does not have fanout net %d\n", i, k ); + fStatus = 0; + } + } + return fStatus; } /**Function************************************************************* @@ -58,9 +87,45 @@ int Ntl_ManCheck( Ntl_Man_t * pMan ) SeeAlso [] ***********************************************************************/ -int Ntl_ModelCheck( Ntl_Mod_t * pModel ) +int Ntl_ManCheck( Ntl_Man_t * pMan ) { - return 1; + Ntl_Mod_t * pMod1, * pMod2; + int i, k, fStatus = 1; + // check that the models have unique names + Ntl_ManForEachModel( pMan, pMod1, i ) + { + if ( pMod1->pName == NULL ) + { + printf( "Model %d does not have a name\n", i ); + fStatus = 0; + } + Ntl_ManForEachModel( pMan, pMod2, k ) + { + if ( i >= k ) + continue; + if ( strcmp(pMod1->pName, pMod2->pName) == 0 ) + { + printf( "Models %d and %d have the same name (%s).\n", i, k, pMod1->pName ); + fStatus = 0; + } + } + } + // check that the models (except the first one) do not have boxes + Ntl_ManForEachModel( pMan, pMod1, i ) + { + if ( i == 0 ) + continue; + if ( Ntl_ModelBoxNum(pMod1) > 0 ) + { + printf( "Non-root model %d (%s) has %d boxes.\n", i, pMod1->pName, Ntl_ModelBoxNum(pMod1) ); + fStatus = 0; + } + } + // check models + Ntl_ManForEachModel( pMan, pMod1, i ) + if ( !Ntl_ModelCheck( pMod1 ) ) + fStatus = 0; + return fStatus; } diff --git a/src/aig/ntl/ntlExtract.c b/src/aig/ntl/ntlExtract.c index a54618e5..0654bb27 100644 --- a/src/aig/ntl/ntlExtract.c +++ b/src/aig/ntl/ntlExtract.c @@ -269,9 +269,9 @@ Aig_Obj_t * Ntl_ConvertSopToAigInternal( Aig_Man_t * pMan, Ntl_Obj_t * pNode, ch { pNet = Ntl_ObjFanin( pNode, i ); if ( Value == '1' ) - pAnd = Aig_And( pMan, pAnd, pNet->pFunc ); + pAnd = Aig_And( pMan, pAnd, pNet->pCopy ); else if ( Value == '0' ) - pAnd = Aig_And( pMan, pAnd, Aig_Not(pNet->pFunc) ); + pAnd = Aig_And( pMan, pAnd, Aig_Not(pNet->pCopy) ); } // add to the sum of cubes pSum = Aig_Or( pMan, pSum, pAnd ); @@ -326,7 +326,7 @@ Aig_Obj_t * Ntl_GraphToNetworkAig( Aig_Man_t * pMan, Dec_Graph_t * pGraph ) SeeAlso [] ***********************************************************************/ -Aig_Obj_t * Ntl_ManExtractAigNode( Ntl_Obj_t * pNode ) +Aig_Obj_t * Ntl_ManBuildNodeAig( Ntl_Obj_t * pNode ) { Aig_Man_t * pMan = pNode->pModel->pMan->pAig; int fUseFactor = 0; @@ -344,7 +344,7 @@ Aig_Obj_t * Ntl_ManExtractAigNode( Ntl_Obj_t * pNode ) pFForm = Dec_Factor( pNode->pSop ); // collect the fanins Dec_GraphForEachLeaf( pFForm, pFFNode, i ) - pFFNode->pFunc = Ntl_ObjFanin(pNode, i)->pFunc; + pFFNode->pFunc = Ntl_ObjFanin(pNode, i)->pCopy; // perform strashing pFunc = Ntl_GraphToNetworkAig( pMan, pFForm ); Dec_GraphFree( pFForm ); @@ -391,23 +391,23 @@ int Ntl_ManExtract_rec( Ntl_Man_t * p, Ntl_Net_t * pNet ) Vec_IntPush( p->vBox1Cos, Aig_ManPoNum(p->pAig) ); Ntl_ObjForEachFanin( pObj, pNetFanin, i ) { - LevelCur = Aig_ObjLevel( Aig_Regular(pNetFanin->pFunc) ); + LevelCur = Aig_ObjLevel( Aig_Regular(pNetFanin->pCopy) ); LevelMax = AIG_MAX( LevelMax, LevelCur ); Vec_PtrPush( p->vCos, pNetFanin ); - Aig_ObjCreatePo( p->pAig, pNetFanin->pFunc ); + Aig_ObjCreatePo( p->pAig, pNetFanin->pCopy ); } Ntl_ObjForEachFanout( pObj, pNetFanin, i ) { Vec_PtrPush( p->vCis, pNetFanin ); - pNetFanin->pFunc = Aig_ObjCreatePi( p->pAig ); - Aig_ObjSetLevel( pNetFanin->pFunc, LevelMax + 1 ); + pNetFanin->pCopy = Aig_ObjCreatePi( p->pAig ); + Aig_ObjSetLevel( pNetFanin->pCopy, LevelMax + 1 ); } //printf( "Creating fake PO with ID = %d.\n", Aig_ManPo(p->pAig, Vec_IntEntryLast(p->vBox1Cos))->Id ); } // store the node Vec_PtrPush( p->vNodes, pObj ); if ( Ntl_ObjIsNode(pObj) ) - pNet->pFunc = Ntl_ManExtractAigNode( pObj ); + pNet->pCopy = Ntl_ManBuildNodeAig( pObj ); pNet->nVisits = 2; return 1; } @@ -441,14 +441,17 @@ Aig_Man_t * Ntl_ManExtract( Ntl_Man_t * p ) p->pAig->pName = Aig_UtilStrsav( p->pName ); p->pAig->pSpec = Aig_UtilStrsav( p->pSpec ); // get the root model - pRoot = Vec_PtrEntry( p->vModels, 0 ); + pRoot = Ntl_ManRootModel( p ); + // clear net visited flags + Ntl_ModelForEachNet( pRoot, pNet, i ) + pNet->nVisits = 0; // collect primary inputs Ntl_ModelForEachPi( pRoot, pObj, i ) { assert( Ntl_ObjFanoutNum(pObj) == 1 ); pNet = Ntl_ObjFanout0(pObj); Vec_PtrPush( p->vCis, pNet ); - pNet->pFunc = Aig_ObjCreatePi( p->pAig ); + pNet->pCopy = Aig_ObjCreatePi( p->pAig ); if ( pNet->nVisits ) { printf( "Ntl_ManExtract(): Primary input appears twice in the list.\n" ); @@ -462,7 +465,7 @@ Aig_Man_t * Ntl_ManExtract( Ntl_Man_t * p ) assert( Ntl_ObjFanoutNum(pObj) == 1 ); pNet = Ntl_ObjFanout0(pObj); Vec_PtrPush( p->vCis, pNet ); - pNet->pFunc = Aig_ObjCreatePi( p->pAig ); + pNet->pCopy = Aig_ObjCreatePi( p->pAig ); if ( pNet->nVisits ) { printf( "Ntl_ManExtract(): Latch output is duplicated or defined as a primary input.\n" ); @@ -483,7 +486,7 @@ Aig_Man_t * Ntl_ManExtract( Ntl_Man_t * p ) return 0; } Vec_PtrPush( p->vCos, pNet ); - Aig_ObjCreatePo( p->pAig, pNet->pFunc ); + Aig_ObjCreatePo( p->pAig, pNet->pCopy ); } // visit the nodes starting from latch inputs outputs Ntl_ModelForEachLatch( pRoot, pObj, i ) @@ -498,7 +501,7 @@ Aig_Man_t * Ntl_ManExtract( Ntl_Man_t * p ) return 0; } Vec_PtrPush( p->vCos, pNet ); - Aig_ObjCreatePo( p->pAig, pNet->pFunc ); + Aig_ObjCreatePo( p->pAig, pNet->pCopy ); } // report the number of dangling objects nUselessObjects = Ntl_ModelNodeNum(pRoot) + Ntl_ModelBoxNum(pRoot) - Vec_PtrSize(p->vNodes); @@ -517,12 +520,54 @@ Aig_Man_t * Ntl_ManExtract( Ntl_Man_t * p ) +/**Function************************************************************* + + Synopsis [Collects the nodes in a topological order.] + + Description [] + + SideEffects [] + SeeAlso [] +***********************************************************************/ +int Ntl_ManBuildModelAig( Ntl_Man_t * p, Ntl_Obj_t * pBox ) +{ + extern int Ntl_ManCollapse_rec( Ntl_Man_t * p, Ntl_Net_t * pNet ); + Ntl_Mod_t * pModel = pBox->pImplem; + Ntl_Obj_t * pObj; + Ntl_Net_t * pNet, * pNetBox; + int i; + assert( Ntl_ObjFaninNum(pBox) == Ntl_ModelPiNum(pModel) ); + assert( Ntl_ObjFanoutNum(pBox) == Ntl_ModelPoNum(pModel) ); + // clear net visited flags + Ntl_ModelForEachNet( pModel, pNet, i ) + pNet->nVisits = 0; + // transfer from the box to the PIs of the model + Ntl_ModelForEachPi( pModel, pObj, i ) + { + pNet = Ntl_ObjFanout0(pObj); + pNetBox = Ntl_ObjFanin( pBox, i ); + pNet->pCopy = pNetBox->pCopy; + pNet->nVisits = 2; + } + // compute AIG for the internal nodes + Ntl_ModelForEachPo( pModel, pObj, i ) + if ( !Ntl_ManCollapse_rec( p, Ntl_ObjFanin0(pObj) ) ) + return 0; + // transfer from the POs of the model to the box + Ntl_ModelForEachPo( pModel, pObj, i ) + { + pNet = Ntl_ObjFanin0(pObj); + pNetBox = Ntl_ObjFanout( pBox, i ); + pNetBox->pCopy = pNet->pCopy; + } + return 1; +} /**Function************************************************************* - Synopsis [Extracts AIG from the netlist.] + Synopsis [Collects the nodes in a topological order.] Description [] @@ -531,32 +576,121 @@ Aig_Man_t * Ntl_ManExtract( Ntl_Man_t * p ) SeeAlso [] ***********************************************************************/ -/* -int Ntl_ManExtract_old( Ntl_Man_t * p ) +int Ntl_ManCollapse_rec( Ntl_Man_t * p, Ntl_Net_t * pNet ) +{ + Ntl_Obj_t * pObj; + Ntl_Net_t * pNetFanin; + int i; + // skip visited + if ( pNet->nVisits == 2 ) + return 1; + // if the node is on the path, this is a combinational loop + if ( pNet->nVisits == 1 ) + return 0; + // mark the node as the one on the path + pNet->nVisits = 1; + // derive the box + pObj = pNet->pDriver; + assert( Ntl_ObjIsNode(pObj) || Ntl_ObjIsBox(pObj) ); + // visit the input nets of the box + Ntl_ObjForEachFanin( pObj, pNetFanin, i ) + if ( !Ntl_ManCollapse_rec( p, pNetFanin ) ) + return 0; + // add box inputs/outputs to COs/CIs + if ( Ntl_ObjIsBox(pObj) ) + { + if ( !Ntl_ManBuildModelAig( p, pObj ) ) + return 0; + } + // store the node + if ( Ntl_ObjIsNode(pObj) ) + pNet->pCopy = Ntl_ManBuildNodeAig( pObj ); + pNet->nVisits = 2; + return 1; +} + +/**Function************************************************************* + + Synopsis [Performs DFS.] + + Description [Checks for combinational loops. Collects PI/PO nets. + Collects nodes in the topological order.] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Aig_Man_t * Ntl_ManCollapse( Ntl_Man_t * p ) { - Ntl_Obj_t * pNode; + Aig_Man_t * pAig; + Ntl_Mod_t * pRoot; + Ntl_Obj_t * pObj; Ntl_Net_t * pNet; int i; - // check the DFS traversal - if ( !Ntl_ManDfs( p ) ) - return 0; // start the AIG manager assert( p->pAig == NULL ); p->pAig = Aig_ManStart( 10000 ); - // create the primary inputs - Ntl_ManForEachCiNet( p, pNet, i ) - pNet->pFunc = Aig_ObjCreatePi( p->pAig ); - // convert internal nodes to AIGs - Ntl_ManForEachNode( p, pNode, i ) - Ntl_ObjFanout0(pNode)->pFunc = Ntl_ManExtractAigNode( pNode ); - // create the primary outputs - Ntl_ManForEachCoNet( p, pNet, i ) - Aig_ObjCreatePo( p->pAig, pNet->pFunc ); + p->pAig->pName = Aig_UtilStrsav( p->pName ); + p->pAig->pSpec = Aig_UtilStrsav( p->pSpec ); + // get the root model + pRoot = Ntl_ManRootModel( p ); + // clear net visited flags + Ntl_ModelForEachNet( pRoot, pNet, i ) + pNet->nVisits = 0; + // collect primary inputs + Ntl_ModelForEachPi( pRoot, pObj, i ) + { + assert( Ntl_ObjFanoutNum(pObj) == 1 ); + pNet = Ntl_ObjFanout0(pObj); + pNet->pCopy = Aig_ObjCreatePi( p->pAig ); + if ( pNet->nVisits ) + { + printf( "Ntl_ManCollapse(): Primary input appears twice in the list.\n" ); + return 0; + } + pNet->nVisits = 2; + } + // collect latch outputs + Ntl_ModelForEachLatch( pRoot, pObj, i ) + { + assert( Ntl_ObjFanoutNum(pObj) == 1 ); + pNet = Ntl_ObjFanout0(pObj); + pNet->pCopy = Aig_ObjCreatePi( p->pAig ); + if ( pNet->nVisits ) + { + printf( "Ntl_ManCollapse(): Latch output is duplicated or defined as a primary input.\n" ); + return 0; + } + pNet->nVisits = 2; + } + // visit the nodes starting from primary outputs + Ntl_ModelForEachPo( pRoot, pObj, i ) + { + pNet = Ntl_ObjFanin0(pObj); + if ( !Ntl_ManCollapse_rec( p, pNet ) ) + { + printf( "Ntl_ManCollapse(): Error: Combinational loop is detected.\n" ); + return 0; + } + Aig_ObjCreatePo( p->pAig, pNet->pCopy ); + } + // visit the nodes starting from latch inputs outputs + Ntl_ModelForEachLatch( pRoot, pObj, i ) + { + pNet = Ntl_ObjFanin0(pObj); + if ( !Ntl_ManCollapse_rec( p, pNet ) ) + { + printf( "Ntl_ManCollapse(): Error: Combinational loop is detected.\n" ); + return 0; + } + Aig_ObjCreatePo( p->pAig, pNet->pCopy ); + } // cleanup the AIG Aig_ManCleanup( p->pAig ); - return 1; + pAig = p->pAig; p->pAig = NULL; + return pAig; } -*/ //////////////////////////////////////////////////////////////////////// diff --git a/src/aig/ntl/ntlInsert.c b/src/aig/ntl/ntlInsert.c index 84a7af84..2eb48e84 100644 --- a/src/aig/ntl/ntlInsert.c +++ b/src/aig/ntl/ntlInsert.c @@ -52,17 +52,17 @@ int Ntl_ManInsert( Ntl_Man_t * p, Vec_Ptr_t * vMapping, Aig_Man_t * pAig ) int i, k, nDigits; // map the AIG back onto the design Ntl_ManForEachCiNet( p, pNet, i ) - pNet->pFunc = Aig_ManPi( pAig, i ); + pNet->pCopy = Aig_ManPi( pAig, i ); Ntl_ManForEachCoNet( p, pNet, i ) - pNet->pFunc = Aig_ObjChild0( Aig_ManPo( pAig, i ) ); + pNet->pCopy = Aig_ObjChild0( Aig_ManPo( pAig, i ) ); // remove old nodes - pRoot = Vec_PtrEntry( p->vModels, 0 ); + pRoot = Ntl_ManRootModel( p ); Ntl_ModelForEachNode( pRoot, pNode, i ) Vec_PtrWriteEntry( pRoot->vObjs, pNode->Id, NULL ); // start mapping of AIG nodes into their copies vCopies = Vec_PtrStart( Aig_ManObjNumMax(pAig) ); Ntl_ManForEachCiNet( p, pNet, i ) - Vec_PtrWriteEntry( vCopies, pNet->pFunc->Id, pNet ); + Vec_PtrWriteEntry( vCopies, ((Aig_Obj_t *)pNet->pCopy)->Id, pNet ); // create a new node for each LUT vCover = Vec_IntAlloc( 1 << 16 ); nDigits = Aig_Base10Log( Vec_PtrSize(vMapping) ); @@ -100,16 +100,16 @@ int Ntl_ManInsert( Ntl_Man_t * p, Vec_Ptr_t * vMapping, Aig_Man_t * pAig ) Vec_IntFree( vCover ); // mark CIs and outputs of the registers Ntl_ManForEachCiNet( p, pNetCo, i ) - pNetCo->nVisits = 101; + pNetCo->nVisits = 101; // using "101" is harmless because nVisits can only be 0, 1 or 2 // update the CO pointers Ntl_ManForEachCoNet( p, pNetCo, i ) { if ( pNetCo->nVisits == 101 ) continue; pNetCo->nVisits = 101; - pNet = Vec_PtrEntry( vCopies, Aig_Regular(pNetCo->pFunc)->Id ); + pNet = Vec_PtrEntry( vCopies, Aig_Regular(pNetCo->pCopy)->Id ); pNode = Ntl_ModelCreateNode( pRoot, 1 ); - pNode->pSop = Aig_IsComplement(pNetCo->pFunc)? Ntl_ManStoreSop( p, "0 1\n" ) : Ntl_ManStoreSop( p, "1 1\n" ); + pNode->pSop = Aig_IsComplement(pNetCo->pCopy)? Ntl_ManStoreSop( p, "0 1\n" ) : Ntl_ManStoreSop( p, "1 1\n" ); Ntl_ObjSetFanin( pNode, pNet, 0 ); // update the CO driver net pNetCo->pDriver = NULL; @@ -134,7 +134,7 @@ int Ntl_ManInsert( Ntl_Man_t * p, Vec_Ptr_t * vMapping, Aig_Man_t * pAig ) SeeAlso [] ***********************************************************************/ -int Ntl_ManInsertNtk( Ntl_Man_t * p, Ntk_Man_t * pNtk ) +int Ntl_ManInsertNtk( Ntl_Man_t * p, Nwk_Man_t * pNtk ) { char Buffer[100]; Vec_Int_t * vTruth; @@ -142,32 +142,34 @@ int Ntl_ManInsertNtk( Ntl_Man_t * p, Ntk_Man_t * pNtk ) Ntl_Mod_t * pRoot; Ntl_Obj_t * pNode; Ntl_Net_t * pNet, * pNetCo; - Ntk_Obj_t * pObj, * pFanin; + Nwk_Obj_t * pObj, * pFanin; int i, k, nDigits; unsigned * pTruth; - assert( Vec_PtrSize(p->vCis) == Ntk_ManCiNum(pNtk) ); - assert( Vec_PtrSize(p->vCos) == Ntk_ManCoNum(pNtk) ); + assert( Vec_PtrSize(p->vCis) == Nwk_ManCiNum(pNtk) ); + assert( Vec_PtrSize(p->vCos) == Nwk_ManCoNum(pNtk) ); // set the correspondence between the PI/PO nodes Ntl_ManForEachCiNet( p, pNet, i ) - Ntk_ManCi( pNtk, i )->pCopy = pNet; + Nwk_ManCi( pNtk, i )->pCopy = pNet; // Ntl_ManForEachCoNet( p, pNet, i ) -// Ntk_ManCo( pNtk, i )->pCopy = pNet; +// Nwk_ManCo( pNtk, i )->pCopy = pNet; // remove old nodes - pRoot = Vec_PtrEntry( p->vModels, 0 ); + pRoot = Ntl_ManRootModel( p ); Ntl_ModelForEachNode( pRoot, pNode, i ) Vec_PtrWriteEntry( pRoot->vObjs, pNode->Id, NULL ); // create a new node for each LUT vTruth = Vec_IntAlloc( 1 << 16 ); vCover = Vec_IntAlloc( 1 << 16 ); - nDigits = Aig_Base10Log( Ntk_ManNodeNum(pNtk) ); - Ntk_ManForEachNode( pNtk, pObj, i ) + nDigits = Aig_Base10Log( Nwk_ManNodeNum(pNtk) ); + Nwk_ManForEachNode( pNtk, pObj, i ) { - pNode = Ntl_ModelCreateNode( pRoot, Ntk_ObjFaninNum(pObj) ); - pTruth = Hop_ManConvertAigToTruth( pNtk->pManHop, pObj->pFunc, Ntk_ObjFaninNum(pObj), vTruth, 0 ); - pNode->pSop = Ntl_SopFromTruth( p, pTruth, Ntk_ObjFaninNum(pObj), vCover ); - if ( !Kit_TruthIsConst0(pTruth, Ntk_ObjFaninNum(pObj)) && !Kit_TruthIsConst1(pTruth, Ntk_ObjFaninNum(pObj)) ) + pNode = Ntl_ModelCreateNode( pRoot, Nwk_ObjFaninNum(pObj) ); + pTruth = Hop_ManConvertAigToTruth( pNtk->pManHop, Hop_Regular(pObj->pFunc), Nwk_ObjFaninNum(pObj), vTruth, 0 ); + if ( Hop_IsComplement(pObj->pFunc) ) + Kit_TruthNot( pTruth, pTruth, Nwk_ObjFaninNum(pObj) ); + pNode->pSop = Ntl_SopFromTruth( p, pTruth, Nwk_ObjFaninNum(pObj), vCover ); + if ( !Kit_TruthIsConst0(pTruth, Nwk_ObjFaninNum(pObj)) && !Kit_TruthIsConst1(pTruth, Nwk_ObjFaninNum(pObj)) ) { - Ntk_ObjForEachFanin( pObj, pFanin, k ) + Nwk_ObjForEachFanin( pObj, pFanin, k ) { pNet = pFanin->pCopy; if ( pNet == NULL ) @@ -204,12 +206,12 @@ int Ntl_ManInsertNtk( Ntl_Man_t * p, Ntk_Man_t * pNtk ) continue; pNetCo->nVisits = 101; // get the corresponding PO and its driver - pObj = Ntk_ManCo( pNtk, i ); - pFanin = Ntk_ObjFanin0( pObj ); + pObj = Nwk_ManCo( pNtk, i ); + pFanin = Nwk_ObjFanin0( pObj ); // get the net driving the driver - pNet = pFanin->pCopy; //Vec_PtrEntry( vCopies, Aig_Regular(pNetCo->pFunc)->Id ); + pNet = pFanin->pCopy; //Vec_PtrEntry( vCopies, Aig_Regular(pNetCo->pCopy)->Id ); pNode = Ntl_ModelCreateNode( pRoot, 1 ); - pNode->pSop = pObj->fCompl /*Aig_IsComplement(pNetCo->pFunc)*/? Ntl_ManStoreSop( p, "0 1\n" ) : Ntl_ManStoreSop( p, "1 1\n" ); + pNode->pSop = pObj->fCompl /*Aig_IsComplement(pNetCo->pCopy)*/? Ntl_ManStoreSop( p, "0 1\n" ) : Ntl_ManStoreSop( p, "1 1\n" ); Ntl_ObjSetFanin( pNode, pNet, 0 ); // update the CO driver net pNetCo->pDriver = NULL; diff --git a/src/aig/ntl/ntlMan.c b/src/aig/ntl/ntlMan.c index 9614a423..82660263 100644 --- a/src/aig/ntl/ntlMan.c +++ b/src/aig/ntl/ntlMan.c @@ -61,6 +61,57 @@ Ntl_Man_t * Ntl_ManAlloc( char * pFileName ) /**Function************************************************************* + Synopsis [Duplicates the interface of the top level model.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Ntl_Man_t * Ntl_ManStartFrom( Ntl_Man_t * pOld ) +{ + return NULL; +} + +/**Function************************************************************* + + Synopsis [Duplicates the interface of the top level model.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Ntl_Man_t * Ntl_ManDup( Ntl_Man_t * pOld ) +{ + Ntl_Man_t * pNew; + Ntl_Mod_t * pModel; + Ntl_Obj_t * pBox; + Ntl_Net_t * pNet; + int i, k; + pNew = Ntl_ManAlloc( pOld->pSpec ); + Vec_PtrForEachEntry( pOld->vModels, pModel, i ) + pModel->pCopy = Ntl_ModelDup( pNew, pModel ); + Vec_PtrForEachEntry( pOld->vModels, pModel, i ) + Ntl_ModelForEachBox( pModel, pBox, k ) + ((Ntl_Obj_t *)pBox->pCopy)->pImplem = pBox->pImplem->pCopy; + Ntl_ManForEachCiNet( pOld, pNet, i ) + Vec_PtrPush( pNew->vCis, pNet->pCopy ); + Ntl_ManForEachCoNet( pOld, pNet, i ) + Vec_PtrPush( pNew->vCos, pNet->pCopy ); + if ( pOld->pManTime ) + pNew->pManTime = Tim_ManDup( pOld->pManTime, 0 ); + if ( !Ntl_ManCheck( pNew ) ) + printf( "Ntl_ManDup: The check has failed for design %s.\n", pNew->pName ); + return pNew; +} + +/**Function************************************************************* + Synopsis [Deallocates the netlist manager.] Description [] @@ -126,15 +177,16 @@ Ntl_Mod_t * Ntl_ManFindModel( Ntl_Man_t * p, char * pName ) void Ntl_ManPrintStats( Ntl_Man_t * p ) { Ntl_Mod_t * pRoot; - pRoot = Vec_PtrEntry( p->vModels, 0 ); + pRoot = Ntl_ManRootModel( p ); printf( "%-15s : ", p->pName ); printf( "pi = %5d ", Ntl_ModelPiNum(pRoot) ); printf( "po = %5d ", Ntl_ModelPoNum(pRoot) ); - printf( "latch = %5d ", Ntl_ModelLatchNum(pRoot) ); + printf( "lat = %5d ", Ntl_ModelLatchNum(pRoot) ); printf( "node = %5d ", Ntl_ModelNodeNum(pRoot) ); printf( "box = %4d ", Ntl_ModelBoxNum(pRoot) ); - printf( "model = %3d", Vec_PtrSize(p->vModels) ); + printf( "mod = %3d", Vec_PtrSize(p->vModels) ); printf( "\n" ); + fflush( stdout ); } /**Function************************************************************* @@ -173,11 +225,11 @@ Ntl_Mod_t * Ntl_ModelAlloc( Ntl_Man_t * pMan, char * pName ) p->pMan = pMan; p->pName = Ntl_ManStoreName( p->pMan, pName ); Vec_PtrPush( pMan->vModels, p ); - p->vObjs = Vec_PtrAlloc( 10000 ); - p->vPis = Vec_PtrAlloc( 1000 ); - p->vPos = Vec_PtrAlloc( 1000 ); + p->vObjs = Vec_PtrAlloc( 1000 ); + p->vPis = Vec_PtrAlloc( 100 ); + p->vPos = Vec_PtrAlloc( 100 ); // start the table - p->nTableSize = Aig_PrimeCudd( 10000 ); + p->nTableSize = Aig_PrimeCudd( 1000 ); p->pTable = ALLOC( Ntl_Net_t *, p->nTableSize ); memset( p->pTable, 0, sizeof(Ntl_Net_t *) * p->nTableSize ); return p; @@ -185,6 +237,41 @@ Ntl_Mod_t * Ntl_ModelAlloc( Ntl_Man_t * pMan, char * pName ) /**Function************************************************************* + Synopsis [Duplicates the model.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Ntl_Mod_t * Ntl_ModelDup( Ntl_Man_t * pManNew, Ntl_Mod_t * pModelOld ) +{ + Ntl_Mod_t * pModelNew; + Ntl_Net_t * pNet; + Ntl_Obj_t * pObj; + int i, k; + pModelNew = Ntl_ModelAlloc( pManNew, pModelOld->pName ); + Ntl_ModelForEachNet( pModelOld, pNet, i ) + pNet->pCopy = Ntl_ModelFindOrCreateNet( pModelNew, pNet->pName ); + Ntl_ModelForEachObj( pModelOld, pObj, i ) + { + pObj->pCopy = Ntl_ModelDupObj( pModelNew, pObj ); + Ntl_ObjForEachFanin( pObj, pNet, k ) + Ntl_ObjSetFanin( pObj->pCopy, pNet->pCopy, k ); + Ntl_ObjForEachFanout( pObj, pNet, k ) + Ntl_ObjSetFanout( pObj->pCopy, pNet->pCopy, k ); + if ( Ntl_ObjIsLatch(pObj) ) + ((Ntl_Obj_t *)pObj->pCopy)->LatchId = pObj->LatchId; + if ( Ntl_ObjIsNode(pObj) ) + ((Ntl_Obj_t *)pObj->pCopy)->pSop = Ntl_ManStoreSop( pManNew, pObj->pSop ); + } + return pModelNew; +} + +/**Function************************************************************* + Synopsis [Deallocates the model.] Description [] diff --git a/src/aig/ntl/ntlMap.c b/src/aig/ntl/ntlMap.c index 20bc79cf..faae32d2 100644 --- a/src/aig/ntl/ntlMap.c +++ b/src/aig/ntl/ntlMap.c @@ -136,7 +136,7 @@ void Ntl_ManSetIfParsDefault( If_Par_t * pPars ) pPars->fExpRed = 0; pPars->fLatchPaths = 0; pPars->fEdge = 1; - pPars->fCutMin = 1; + pPars->fCutMin = 0; pPars->fSeqMap = 0; pPars->fVerbose = 1; // internal parameters diff --git a/src/aig/ntl/ntlObj.c b/src/aig/ntl/ntlObj.c index 2e39fbbf..ad43623a 100644 --- a/src/aig/ntl/ntlObj.c +++ b/src/aig/ntl/ntlObj.c @@ -163,6 +163,33 @@ Ntl_Obj_t * Ntl_ModelCreateBox( Ntl_Mod_t * pModel, int nFanins, int nFanouts ) /**Function************************************************************* + Synopsis [Create the latch.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Ntl_Obj_t * Ntl_ModelDupObj( Ntl_Mod_t * pModel, Ntl_Obj_t * pOld ) +{ + Ntl_Obj_t * pNew; + if ( Ntl_ObjIsPi( pOld ) ) + pNew = Ntl_ModelCreatePi( pModel ); + else if ( Ntl_ObjIsPo( pOld ) ) + pNew = Ntl_ModelCreatePo( pModel, NULL ); + else if ( Ntl_ObjIsLatch( pOld ) ) + pNew = Ntl_ModelCreateLatch( pModel ); + else if ( Ntl_ObjIsNode( pOld ) ) + pNew = Ntl_ModelCreateNode( pModel, Ntl_ObjFaninNum(pOld) ); + else if ( Ntl_ObjIsBox( pOld ) ) + pNew = Ntl_ModelCreateBox( pModel, Ntl_ObjFaninNum(pOld), Ntl_ObjFanoutNum(pOld) ); + return pNew; +} + +/**Function************************************************************* + Synopsis [Allocates memory and copies the name into it.] Description [] diff --git a/src/aig/ntl/ntlReadBlif.c b/src/aig/ntl/ntlReadBlif.c index d085b5e6..e5a94610 100644 --- a/src/aig/ntl/ntlReadBlif.c +++ b/src/aig/ntl/ntlReadBlif.c @@ -108,9 +108,7 @@ Ntl_Man_t * Ioa_ReadBlif( char * pFileName, int fCheck ) { FILE * pFile; Ioa_ReadMan_t * p; - Ntl_Mod_t * pNtk; Ntl_Man_t * pDesign; - int i; // check that the file is available pFile = fopen( pFileName, "rb" ); @@ -158,20 +156,9 @@ Ntl_Man_t * Ioa_ReadBlif( char * pFileName, int fCheck ) // make sure that everything is okay with the network structure if ( fCheck ) { - // check individual models - Vec_PtrForEachEntry( pDesign->vModels, pNtk, i ) - { - if ( !Ntl_ModelCheck( pNtk ) ) - { - printf( "Ioa_ReadBlif: The network check has failed for network %s.\n", pNtk->pName ); - Ntl_ManFree( pDesign ); - return NULL; - } - } - // check the hierarchy if ( !Ntl_ManCheck( pDesign ) ) { - printf( "Ioa_ReadBlif: The hierarchy check has failed for design %s.\n", pDesign->pName ); + printf( "Ioa_ReadBlif: The check has failed for design %s.\n", pDesign->pName ); Ntl_ManFree( pDesign ); return NULL; } diff --git a/src/aig/ntl/ntlTable.c b/src/aig/ntl/ntlTable.c index b84ac1a5..909a64fd 100644 --- a/src/aig/ntl/ntlTable.c +++ b/src/aig/ntl/ntlTable.c @@ -151,28 +151,6 @@ Ntl_Net_t * Ntl_ModelFindOrCreateNet( Ntl_Mod_t * p, char * pName ) /**Function************************************************************* - Synopsis [Finds or creates the net.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -int Ntl_ModelSetNetDriver( Ntl_Obj_t * pObj, Ntl_Net_t * pNet ) -{ - if ( pObj->pFanio[pObj->nFanins] != NULL ) - return 0; - if ( pNet->pDriver != NULL ) - return 0; - pObj->pFanio[pObj->nFanins] = pNet; - pNet->pDriver = pObj; - return 1; -} - -/**Function************************************************************* - Synopsis [Returns -1, 0, +1 (when it is PI, not found, or PO).] Description [] @@ -210,6 +188,28 @@ int Ntl_ModelFindPioNumber( Ntl_Mod_t * p, char * pName, int * pNumber ) return 0; } +/**Function************************************************************* + + Synopsis [Finds or creates the net.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Ntl_ModelSetNetDriver( Ntl_Obj_t * pObj, Ntl_Net_t * pNet ) +{ + if ( pObj->pFanio[pObj->nFanins] != NULL ) + return 0; + if ( pNet->pDriver != NULL ) + return 0; + pObj->pFanio[pObj->nFanins] = pNet; + pNet->pDriver = pObj; + return 1; +} + //////////////////////////////////////////////////////////////////////// /// END OF FILE /// //////////////////////////////////////////////////////////////////////// diff --git a/src/aig/ntl/ntlTime.c b/src/aig/ntl/ntlTime.c index 50f3d290..cf2ec0f1 100644 --- a/src/aig/ntl/ntlTime.c +++ b/src/aig/ntl/ntlTime.c @@ -84,7 +84,7 @@ Tim_Man_t * Ntl_ManCreateTiming( Ntl_Man_t * p ) Ntl_Obj_t * pObj; int i, curPi, iBox, Entry; assert( p->pAig != NULL ); - pRoot = Vec_PtrEntry( p->vModels, 0 ); + pRoot = Ntl_ManRootModel( p ); // start the timing manager pMan = Tim_ManStart( Aig_ManPiNum(p->pAig), Aig_ManPoNum(p->pAig) ); // unpack the data in the arrival times |