diff options
38 files changed, 1525 insertions, 761 deletions
@@ -57,6 +57,7 @@ alias rv read_verilog alias rvl read_verlib alias rsup read_super mcnc5_old.super alias rlib read_library +alias rlibc read_library cadence.genlib alias rw rewrite alias rwz rewrite -z alias rf refactor @@ -118,10 +119,10 @@ alias fflitmin "compress2rs; ren; sop; ps -f" alias t0 "r res.blif; aig; mfs" alias t "r res2.blif; aig; mfs" -alias tt "rh a/quip_opt/nut_001_opt.blif" +alias tt "r a/quip_opt/nut_001_opt.blif" alias ttb "wh a/quip_opt/nut_001_opt.blif 1.blif" alias ttv "wh a/quip_opt/nut_001_opt.blif 1.v" -alias reach "st; ps; compress2; ps; qrel; ps; qreach -v; ps" +alias reach "st; ps; compress2; ps; qrel; ps; compress2; ps; qreach -v; ps" diff --git a/abctestlib.dsw b/abctestlib.dsw new file mode 100644 index 00000000..7ae6cac9 --- /dev/null +++ b/abctestlib.dsw @@ -0,0 +1,29 @@ +Microsoft Developer Studio Workspace File, Format Version 6.00 +# WARNING: DO NOT EDIT OR DELETE THIS WORKSPACE FILE! + +############################################################################### + +Project: "abctestlib"=.\abctestlib.dsp - Package Owner=<4> + +Package=<5> +{{{ +}}} + +Package=<4> +{{{ +}}} + +############################################################################### + +Global: + +Package=<5> +{{{ +}}} + +Package=<3> +{{{ +}}} + +############################################################################### + diff --git a/src/base/abc/abc.h b/src/base/abc/abc.h index bbe6b078..f638097f 100644 --- a/src/base/abc/abc.h +++ b/src/base/abc/abc.h @@ -222,6 +222,7 @@ struct Abc_Lib_t_ Vec_Ptr_t * vModules; // the array of modules st_table * tModules; // the table hashing module names into their networks Abc_Lib_t * pLibrary; // the library used to map this design + void * pGenlib; // the genlib library used to map this design }; //////////////////////////////////////////////////////////////////////// @@ -468,11 +469,11 @@ static inline void Abc_ObjSetMvVar( Abc_Obj_t * pObj, void * pV) { Vec_At for ( i = 0; (i < Vec_PtrSize((pNtk)->vBoxes)) && (((pObj) = Abc_NtkBox(pNtk, i)), 1); i++ ) \ if ( !Abc_ObjIsLatch(pObj) ) {} else #define Abc_NtkForEachLatchInput( pNtk, pObj, i ) \ - for ( i = 0; (i < Vec_PtrSize((pNtk)->vBoxes)) && (((pObj) = Abc_ObjFanin0(Abc_NtkBox(pNtk, i))), 1); i++ ) \ - if ( !Abc_ObjIsLatch(Abc_NtkBox(pNtk, i)) ) {} else -#define Abc_NtkForEachLatchOutput( pNtk, pObj, i ) \ - for ( i = 0; (i < Vec_PtrSize((pNtk)->vBoxes)) && (((pObj) = Abc_ObjFanout0(Abc_NtkBox(pNtk, i))), 1); i++ ) \ - if ( !Abc_ObjIsLatch(Abc_NtkBox(pNtk, i)) ) {} else + for ( i = 0; (i < Vec_PtrSize((pNtk)->vBoxes)); i++ ) \ + if ( !(Abc_ObjIsLatch(Abc_NtkBox(pNtk, i)) && (((pObj) = Abc_ObjFanin0(Abc_NtkBox(pNtk, i))), 1)) ) {} else +#define Abc_NtkForEachLatchOutput( pNtk, pObj, i ) \ + for ( i = 0; (i < Vec_PtrSize((pNtk)->vBoxes)); i++ ) \ + if ( !(Abc_ObjIsLatch(Abc_NtkBox(pNtk, i)) && (((pObj) = Abc_ObjFanout0(Abc_NtkBox(pNtk, i))), 1)) ) {} else #define Abc_NtkForEachWhitebox( pNtk, pObj, i ) \ for ( i = 0; (i < Vec_PtrSize((pNtk)->vBoxes)) && (((pObj) = Abc_NtkBox(pNtk, i)), 1); i++ ) \ if ( !Abc_ObjIsWhitebox(pObj) ) {} else @@ -596,9 +597,9 @@ extern void Abc_NtkLogicMakeDirectSops( Abc_Ntk_t * pNtk ); extern int Abc_NtkSopToAig( Abc_Ntk_t * pNtk ); extern int Abc_NtkAigToBdd( Abc_Ntk_t * pNtk ); extern int Abc_NtkMapToSop( Abc_Ntk_t * pNtk ); -extern int Abc_NtkLogicToSop( Abc_Ntk_t * pNtk, int fDirect ); -extern int Abc_NtkLogicToBdd( Abc_Ntk_t * pNtk ); -extern int Abc_NtkLogicToAig( Abc_Ntk_t * pNtk ); +extern int Abc_NtkToSop( Abc_Ntk_t * pNtk, int fDirect ); +extern int Abc_NtkToBdd( Abc_Ntk_t * pNtk ); +extern int Abc_NtkToAig( Abc_Ntk_t * pNtk ); /*=== abcHie.c ==========================================================*/ extern Abc_Ntk_t * Abc_NtkFlattenLogicHierarchy( Abc_Ntk_t * pNtk ); extern Abc_Ntk_t * Abc_NtkConvertBlackboxes( Abc_Ntk_t * pNtk ); @@ -680,12 +681,9 @@ extern void Abc_NtkAddDummyAssertNames( Abc_Ntk_t * pNtk ); extern void Abc_NtkAddDummyBoxNames( Abc_Ntk_t * pNtk ); extern void Abc_NtkShortNames( Abc_Ntk_t * pNtk ); /*=== abcNetlist.c ==========================================================*/ -extern Abc_Ntk_t * Abc_NtkNetlistToLogic( Abc_Ntk_t * pNtk ); -extern Abc_Ntk_t * Abc_NtkLogicToNetlist( Abc_Ntk_t * pNtk, int fDirect ); -extern Abc_Ntk_t * Abc_NtkLogicToNetlistBench( Abc_Ntk_t * pNtk ); -extern Abc_Ntk_t * Abc_NtkLogicSopToNetlist( Abc_Ntk_t * pNtk ); -extern Abc_Ntk_t * Abc_NtkAigToLogicSop( Abc_Ntk_t * pNtk ); -extern Abc_Ntk_t * Abc_NtkAigToLogicSopBench( Abc_Ntk_t * pNtk ); +extern Abc_Ntk_t * Abc_NtkToLogic( Abc_Ntk_t * pNtk ); +extern Abc_Ntk_t * Abc_NtkToNetlist( Abc_Ntk_t * pNtk, int fDirect ); +extern Abc_Ntk_t * Abc_NtkToNetlistBench( Abc_Ntk_t * pNtk ); /*=== abcNtbdd.c ==========================================================*/ extern Abc_Ntk_t * Abc_NtkDeriveFromBdd( DdManager * dd, DdNode * bFunc, char * pNamePo, Vec_Ptr_t * vNamesPi ); extern Abc_Ntk_t * Abc_NtkBddToMuxes( Abc_Ntk_t * pNtk ); diff --git a/src/base/abc/abcFunc.c b/src/base/abc/abcFunc.c index 5e13807a..0947b58a 100644 --- a/src/base/abc/abcFunc.c +++ b/src/base/abc/abcFunc.c @@ -53,7 +53,7 @@ int Abc_NtkSopToBdd( Abc_Ntk_t * pNtk ) DdManager * dd; int nFaninsMax, i; - assert( Abc_NtkIsSopLogic(pNtk) ); + assert( Abc_NtkHasSop(pNtk) ); // start the functionality manager nFaninsMax = Abc_NtkGetFaninMax( pNtk ); @@ -159,7 +159,7 @@ void Abc_NtkLogicMakeDirectSops( Abc_Ntk_t * pNtk ) Abc_Obj_t * pNode; int nFaninsMax, fFound, i; - assert( Abc_NtkIsSopLogic(pNtk) ); + assert( Abc_NtkHasSop(pNtk) ); // check if there are nodes with complemented SOPs fFound = 0; @@ -221,7 +221,7 @@ int Abc_NtkBddToSop( Abc_Ntk_t * pNtk, int fDirect ) else fMode = -1; - assert( Abc_NtkIsBddLogic(pNtk) ); + assert( Abc_NtkHasBdd(pNtk) ); if ( dd->size > 0 ) Cudd_zddVarsFromBddVars( dd, 2 ); // create the new manager @@ -481,7 +481,7 @@ int Abc_ConvertZddToSop( DdManager * dd, DdNode * zCover, char * pSop, int nFani ***********************************************************************/ void Abc_NodeBddToCnf( Abc_Obj_t * pNode, Extra_MmFlex_t * pMmMan, Vec_Str_t * vCube, int fAllPrimes, char ** ppSop0, char ** ppSop1 ) { - assert( Abc_NtkIsBddLogic(pNode->pNtk) ); + assert( Abc_NtkHasBdd(pNode->pNtk) ); *ppSop0 = Abc_ConvertBddToSop( pMmMan, pNode->pNtk->pManFunc, pNode->pData, pNode->pData, Abc_ObjFaninNum(pNode), fAllPrimes, vCube, 0 ); *ppSop1 = Abc_ConvertBddToSop( pMmMan, pNode->pNtk->pManFunc, pNode->pData, pNode->pData, Abc_ObjFaninNum(pNode), fAllPrimes, vCube, 1 ); } @@ -554,7 +554,7 @@ int Abc_NtkSopToAig( Abc_Ntk_t * pNtk ) Hop_Man_t * pMan; int i; - assert( Abc_NtkIsSopLogic(pNtk) || Abc_NtkIsSopNetlist(pNtk) ); + assert( Abc_NtkHasSop(pNtk) ); // start the functionality manager pMan = Hop_ManStart(); @@ -664,7 +664,7 @@ int Abc_NtkAigToBdd( Abc_Ntk_t * pNtk ) DdManager * dd; int nFaninsMax, i; - assert( Abc_NtkIsAigLogic(pNtk) ); + assert( Abc_NtkHasAig(pNtk) ); // start the functionality manager nFaninsMax = Abc_NtkGetFaninMax( pNtk ); @@ -863,7 +863,7 @@ int Abc_NtkMapToSop( Abc_Ntk_t * pNtk ) char * pSop; int i; - assert( Abc_NtkIsMappedLogic(pNtk) ); + assert( Abc_NtkHasMapping(pNtk) ); // update the functionality manager assert( pNtk->pManFunc == Abc_FrameReadLibGen() ); pNtk->pManFunc = Extra_MmFlexStart(); @@ -889,10 +889,10 @@ int Abc_NtkMapToSop( Abc_Ntk_t * pNtk ) SeeAlso [] ***********************************************************************/ -int Abc_NtkLogicToSop( Abc_Ntk_t * pNtk, int fDirect ) +int Abc_NtkToSop( Abc_Ntk_t * pNtk, int fDirect ) { - assert( Abc_NtkIsLogic(pNtk) ); - if ( Abc_NtkIsSopLogic(pNtk) ) + assert( !Abc_NtkIsStrash(pNtk) ); + if ( Abc_NtkHasSop(pNtk) ) { if ( !fDirect ) return 1; @@ -900,11 +900,11 @@ int Abc_NtkLogicToSop( Abc_Ntk_t * pNtk, int fDirect ) return 0; return Abc_NtkBddToSop(pNtk, fDirect); } - if ( Abc_NtkIsMappedLogic(pNtk) ) + if ( Abc_NtkHasMapping(pNtk) ) return Abc_NtkMapToSop(pNtk); - if ( Abc_NtkIsBddLogic(pNtk) ) + if ( Abc_NtkHasBdd(pNtk) ) return Abc_NtkBddToSop(pNtk, fDirect); - if ( Abc_NtkIsAigLogic(pNtk) ) + if ( Abc_NtkHasAig(pNtk) ) { if ( !Abc_NtkAigToBdd(pNtk) ) return 0; @@ -925,19 +925,19 @@ int Abc_NtkLogicToSop( Abc_Ntk_t * pNtk, int fDirect ) SeeAlso [] ***********************************************************************/ -int Abc_NtkLogicToBdd( Abc_Ntk_t * pNtk ) +int Abc_NtkToBdd( Abc_Ntk_t * pNtk ) { - assert( Abc_NtkIsLogic(pNtk) ); - if ( Abc_NtkIsBddLogic(pNtk) ) + assert( !Abc_NtkIsStrash(pNtk) ); + if ( Abc_NtkHasBdd(pNtk) ) return 1; - if ( Abc_NtkIsMappedLogic(pNtk) ) + if ( Abc_NtkHasMapping(pNtk) ) { Abc_NtkMapToSop(pNtk); return Abc_NtkSopToBdd(pNtk); } - if ( Abc_NtkIsSopLogic(pNtk) ) + if ( Abc_NtkHasSop(pNtk) ) return Abc_NtkSopToBdd(pNtk); - if ( Abc_NtkIsAigLogic(pNtk) ) + if ( Abc_NtkHasAig(pNtk) ) return Abc_NtkAigToBdd(pNtk); assert( 0 ); return 0; @@ -954,23 +954,23 @@ int Abc_NtkLogicToBdd( Abc_Ntk_t * pNtk ) SeeAlso [] ***********************************************************************/ -int Abc_NtkLogicToAig( Abc_Ntk_t * pNtk ) +int Abc_NtkToAig( Abc_Ntk_t * pNtk ) { - assert( Abc_NtkIsLogic(pNtk) ); - if ( Abc_NtkIsAigLogic(pNtk) ) + assert( !Abc_NtkIsStrash(pNtk) ); + if ( Abc_NtkHasAig(pNtk) ) return 1; - if ( Abc_NtkIsMappedLogic(pNtk) ) + if ( Abc_NtkHasMapping(pNtk) ) { Abc_NtkMapToSop(pNtk); return Abc_NtkSopToAig(pNtk); } - if ( Abc_NtkIsBddLogic(pNtk) ) + if ( Abc_NtkHasBdd(pNtk) ) { if ( !Abc_NtkBddToSop(pNtk,0) ) return 0; return Abc_NtkSopToAig(pNtk); } - if ( Abc_NtkIsSopLogic(pNtk) ) + if ( Abc_NtkHasSop(pNtk) ) return Abc_NtkSopToAig(pNtk); assert( 0 ); return 0; diff --git a/src/base/abc/abcHie.c b/src/base/abc/abcHie.c index 342d6c83..b38afb59 100644 --- a/src/base/abc/abcHie.c +++ b/src/base/abc/abcHie.c @@ -195,7 +195,7 @@ Abc_Ntk_t * Abc_NtkFlattenLogicHierarchy( Abc_Ntk_t * pNtk ) // recursively flatten hierarchy, create internal logic, add new PI/PO names if there are black boxes Counter = -1; Abc_NtkFlattenLogicHierarchy_rec( pNtkNew, pNtk, &Counter ); - printf( "Hierarchy reader flattened %d logic instances. Preserved %d black boxes.\n", + printf( "Hierarchy reader flattened %d instances of logic boxes and left %d black boxes.\n", Counter, Abc_NtkBlackboxNum(pNtkNew) ); // pass the design @@ -249,44 +249,29 @@ Abc_Ntk_t * Abc_NtkConvertBlackboxes( Abc_Ntk_t * pNtk ) // clean the node copy fields Abc_NtkCleanCopy( pNtk ); - // create PIs/POs for the box inputs/outputs // mark the nodes that should not be connected Abc_NtkIncrementTravId( pNtk ); Abc_NtkForEachBlackbox( pNtk, pObj, i ) - { Abc_NodeSetTravIdCurrent( pObj ); + Abc_NtkForEachCi( pNtk, pTerm, i ) + Abc_NodeSetTravIdCurrent( pTerm ); + Abc_NtkForEachCo( pNtk, pTerm, i ) + Abc_NodeSetTravIdCurrent( pTerm ); + // unmark PIs and LIs/LOs + Abc_NtkForEachPi( pNtk, pTerm, i ) + Abc_NodeSetTravIdPrevious( pTerm ); + Abc_NtkForEachLatchInput( pNtk, pTerm, i ) + Abc_NodeSetTravIdPrevious( pTerm ); + Abc_NtkForEachLatchOutput( pNtk, pTerm, i ) + Abc_NodeSetTravIdPrevious( pTerm ); + // copy the box outputs + Abc_NtkForEachBlackbox( pNtk, pObj, i ) Abc_ObjForEachFanout( pObj, pTerm, k ) - { - pNet = Abc_ObjFanout0(pTerm); - if ( pNet->pCopy ) - { - printf( "Error in Abc_NtkConvertBlackboxes(): Output %s of a black box has a non-unique name.\n", Abc_ObjName(pNet->pCopy) ); - Abc_NtkDelete( pNtkNew ); - return NULL; - } - pNet->pCopy = Abc_NtkFindOrCreateNet( pNtkNew, Abc_ObjName(pNet) ); pTerm->pCopy = Abc_NtkCreatePi( pNtkNew ); - Abc_NodeSetTravIdCurrent( pTerm ); - } - } - Abc_NtkForEachBlackbox( pNtk, pObj, i ) - { - Abc_ObjForEachFanin( pObj, pTerm, k ) - { - pNet = Abc_ObjFanin0(pTerm); - if ( pNet->pCopy && !Abc_ObjIsCi(Abc_ObjFanin0(pNet)) ) - { - Abc_NodeSetTravIdCurrent( pTerm ); - continue; - } - pNet->pCopy = Abc_NtkFindOrCreateNet( pNtkNew, Abc_ObjName(pNet) ); - pTerm->pCopy = Abc_NtkCreatePo( pNtkNew ); - } - } // duplicate other objects Abc_NtkForEachObj( pNtk, pObj, i ) - if ( !Abc_NodeIsTravIdCurrent(pObj) && pObj->pCopy == NULL ) + if ( !Abc_NodeIsTravIdCurrent(pObj) ) Abc_NtkDupObj( pNtkNew, pObj, Abc_ObjIsNet(pObj) ); // connect all objects @@ -295,6 +280,23 @@ Abc_Ntk_t * Abc_NtkConvertBlackboxes( Abc_Ntk_t * pNtk ) Abc_ObjForEachFanin( pObj, pFanin, k ) Abc_ObjAddFanin( pObj->pCopy, pFanin->pCopy ); + // create unique PO for each net feeding into blackboxes or POs + Abc_NtkIncrementTravId( pNtk ); + Abc_NtkForEachCo( pNtk, pTerm, i ) + { + // skip latch inputs + assert( Abc_ObjFanoutNum(pTerm) <= 1 ); + if ( Abc_ObjFanoutNum(pTerm) > 0 && Abc_ObjIsLatch(Abc_ObjFanout0(pTerm)) ) + continue; + // check if the net is visited + pNet = Abc_ObjFanin0(pTerm); + if ( Abc_NodeIsTravIdCurrent(pNet) ) + continue; + // create PO + Abc_NodeSetTravIdCurrent( pNet ); + Abc_ObjAddFanin( Abc_NtkCreatePo(pNtkNew), pNet->pCopy ); + } + // check integrity if ( !Abc_NtkCheck( pNtkNew ) ) { @@ -337,18 +339,11 @@ Abc_Ntk_t * Abc_NtkInsertNewLogic( Abc_Ntk_t * pNtkH, Abc_Ntk_t * pNtkL ) assert( Abc_NtkWhiteboxNum(pNtkL) == 0 ); assert( Abc_NtkBlackboxNum(pNtkL) == 0 ); - if ( Abc_NtkIsSopNetlist(pNtkH) && Abc_NtkIsAigNetlist(pNtkL) ) - Abc_NtkSopToAig( pNtkH ); - if ( Abc_NtkIsAigNetlist(pNtkH) && Abc_NtkIsSopNetlist(pNtkL) ) - Abc_NtkSopToAig( pNtkL ); - - assert( pNtkH->ntkFunc == pNtkL->ntkFunc ); - // prepare the logic network for copying Abc_NtkCleanCopy( pNtkL ); // start the network - pNtkNew = Abc_NtkAlloc( pNtkH->ntkType, pNtkH->ntkFunc, 1 ); + pNtkNew = Abc_NtkAlloc( pNtkL->ntkType, pNtkL->ntkFunc, 1 ); // duplicate the name and the spec pNtkNew->pName = Extra_UtilStrsav( pNtkH->pName ); pNtkNew->pSpec = Extra_UtilStrsav( pNtkH->pSpec ); diff --git a/src/base/abc/abcLib.c b/src/base/abc/abcLib.c index 247f3915..1f741ca8 100644 --- a/src/base/abc/abcLib.c +++ b/src/base/abc/abcLib.c @@ -82,6 +82,7 @@ void Abc_LibFree( Abc_Lib_t * pLib, Abc_Ntk_t * pNtkSave ) if ( pNtk == pNtkSave ) continue; pNtk->pManFunc = NULL; + pNtk->pDesign = NULL; Abc_NtkDelete( pNtk ); } Vec_PtrFree( pLib->vModules ); @@ -166,6 +167,7 @@ int Abc_LibAddModel( Abc_Lib_t * pLib, Abc_Ntk_t * pNtk ) return 0; st_insert( pLib->tModules, (char *)pNtk->pName, (char *)pNtk ); Vec_PtrPush( pLib->vModules, pNtk ); + pNtk->pDesign = pLib; return 1; } diff --git a/src/base/abc/abcNetlist.c b/src/base/abc/abcNetlist.c index 30c7d621..f57bcc21 100644 --- a/src/base/abc/abcNetlist.c +++ b/src/base/abc/abcNetlist.c @@ -26,6 +26,9 @@ //////////////////////////////////////////////////////////////////////// static void Abc_NtkAddPoBuffers( Abc_Ntk_t * pNtk ); +static Abc_Ntk_t * Abc_NtkLogicToNetlist( Abc_Ntk_t * pNtk ); +static Abc_Ntk_t * Abc_NtkAigToLogicSop( Abc_Ntk_t * pNtk ); +static Abc_Ntk_t * Abc_NtkAigToLogicSopBench( Abc_Ntk_t * pNtk ); //////////////////////////////////////////////////////////////////////// /// FUNCTION DEFINITIONS /// @@ -42,22 +45,21 @@ static void Abc_NtkAddPoBuffers( Abc_Ntk_t * pNtk ); SeeAlso [] ***********************************************************************/ -Abc_Ntk_t * Abc_NtkNetlistToLogic( Abc_Ntk_t * pNtk ) +Abc_Ntk_t * Abc_NtkToLogic( Abc_Ntk_t * pNtk ) { Abc_Ntk_t * pNtkNew; Abc_Obj_t * pObj, * pFanin; int i, k; + // consider the case of the AIG + if ( Abc_NtkIsStrash(pNtk) ) + return Abc_NtkAigToLogicSop( pNtk ); assert( Abc_NtkIsNetlist(pNtk) ); // consider simple case when there is hierarchy assert( pNtk->pDesign == NULL ); -// assert( pNtk->tName2Model == NULL ); -// if ( pNtk->tName2Model ) -// return Abc_NtkNetlistToLogicHie( pNtk ); + assert( Abc_NtkWhiteboxNum(pNtk) == 0 ); + assert( Abc_NtkBlackboxNum(pNtk) == 0 ); // start the network - if ( Abc_NtkHasMapping(pNtk) ) - pNtkNew = Abc_NtkStartFrom( pNtk, ABC_NTK_LOGIC, ABC_FUNC_MAP ); - else - pNtkNew = Abc_NtkStartFrom( pNtk, ABC_NTK_LOGIC, pNtk->ntkFunc ); + pNtkNew = Abc_NtkStartFrom( pNtk, ABC_NTK_LOGIC, pNtk->ntkFunc ); // duplicate the nodes Abc_NtkForEachNode( pNtk, pObj, i ) Abc_NtkDupObj(pNtkNew, pObj, 0); @@ -71,9 +73,9 @@ Abc_Ntk_t * Abc_NtkNetlistToLogic( Abc_Ntk_t * pNtk ) Abc_NtkLogicMakeSimpleCos( pNtkNew, 0 ); // duplicate EXDC if ( pNtk->pExdc ) - pNtkNew->pExdc = Abc_NtkNetlistToLogic( pNtk->pExdc ); + pNtkNew->pExdc = Abc_NtkToLogic( pNtk->pExdc ); if ( !Abc_NtkCheck( pNtkNew ) ) - fprintf( stdout, "Abc_NtkNetlistToLogic(): Network check has failed.\n" ); + fprintf( stdout, "Abc_NtkToLogic(): Network check has failed.\n" ); return pNtkNew; } @@ -88,36 +90,18 @@ Abc_Ntk_t * Abc_NtkNetlistToLogic( Abc_Ntk_t * pNtk ) SeeAlso [] ***********************************************************************/ -Abc_Ntk_t * Abc_NtkLogicToNetlist( Abc_Ntk_t * pNtk, int fDirect ) +Abc_Ntk_t * Abc_NtkToNetlist( Abc_Ntk_t * pNtk, int fDirect ) { Abc_Ntk_t * pNtkNew, * pNtkTemp; assert( Abc_NtkIsLogic(pNtk) || Abc_NtkIsStrash(pNtk) ); if ( Abc_NtkIsStrash(pNtk) ) { pNtkTemp = Abc_NtkAigToLogicSop(pNtk); - pNtkNew = Abc_NtkLogicSopToNetlist( pNtkTemp ); + pNtkNew = Abc_NtkLogicToNetlist( pNtkTemp ); Abc_NtkDelete( pNtkTemp ); + return pNtkNew; } - else if ( Abc_NtkIsBddLogic(pNtk) ) - { - if ( !Abc_NtkBddToSop(pNtk, fDirect) ) - return NULL; - pNtkNew = Abc_NtkLogicSopToNetlist( pNtk ); - Abc_NtkSopToBdd(pNtk); - } - else if ( Abc_NtkIsAigLogic(pNtk) ) - { - if ( !Abc_NtkAigToBdd(pNtk) ) - return NULL; - if ( !Abc_NtkBddToSop(pNtk, fDirect) ) - return NULL; - pNtkNew = Abc_NtkLogicSopToNetlist( pNtk ); - Abc_NtkSopToAig(pNtk); - } - else if ( Abc_NtkIsSopLogic(pNtk) || Abc_NtkIsMappedLogic(pNtk) ) - pNtkNew = Abc_NtkLogicSopToNetlist( pNtk ); - else assert( 0 ); - return pNtkNew; + return Abc_NtkLogicToNetlist( pNtk ); } /**Function************************************************************* @@ -131,12 +115,12 @@ Abc_Ntk_t * Abc_NtkLogicToNetlist( Abc_Ntk_t * pNtk, int fDirect ) SeeAlso [] ***********************************************************************/ -Abc_Ntk_t * Abc_NtkLogicToNetlistBench( Abc_Ntk_t * pNtk ) +Abc_Ntk_t * Abc_NtkToNetlistBench( Abc_Ntk_t * pNtk ) { Abc_Ntk_t * pNtkNew, * pNtkTemp; assert( Abc_NtkIsStrash(pNtk) ); pNtkTemp = Abc_NtkAigToLogicSopBench( pNtk ); - pNtkNew = Abc_NtkLogicSopToNetlist( pNtkTemp ); + pNtkNew = Abc_NtkLogicToNetlist( pNtkTemp ); Abc_NtkDelete( pNtkTemp ); return pNtkNew; } @@ -156,32 +140,24 @@ Abc_Ntk_t * Abc_NtkLogicToNetlistBench( Abc_Ntk_t * pNtk ) SeeAlso [] ***********************************************************************/ -Abc_Ntk_t * Abc_NtkLogicSopToNetlist( Abc_Ntk_t * pNtk ) +Abc_Ntk_t * Abc_NtkLogicToNetlist( Abc_Ntk_t * pNtk ) { Abc_Ntk_t * pNtkNew; Abc_Obj_t * pObj, * pNet, * pDriver, * pFanin; int i, k; + assert( Abc_NtkIsLogic(pNtk) ); + // remove dangling nodes Abc_NtkCleanup( pNtk, 0 ); - assert( Abc_NtkIsLogic(pNtk) ); // assert( Abc_NtkLogicHasSimpleCos(pNtk) ); if ( !Abc_NtkLogicHasSimpleCos(pNtk) ) { - printf( "Abc_NtkLogicSopToNetlist() warning: The network is converted to have simple COs.\n" ); + printf( "Abc_NtkLogicToNetlist() warning: The network is converted to have simple COs.\n" ); Abc_NtkLogicMakeSimpleCos( pNtk, 0 ); } - if ( Abc_NtkIsBddLogic(pNtk) ) - { - if ( !Abc_NtkBddToSop(pNtk,0) ) - return NULL; - } - -// Abc_NtkForEachCo(pNtk, pObj, i) -// Abc_ObjPrint( stdout, Abc_ObjFanin0(pObj) ); - // start the netlist by creating PI/PO/Latch objects pNtkNew = Abc_NtkStartFrom( pNtk, ABC_NTK_NETLIST, pNtk->ntkFunc ); // create the CI nets and remember them in the new CI nodes @@ -227,7 +203,7 @@ Abc_Ntk_t * Abc_NtkLogicSopToNetlist( Abc_Ntk_t * pNtk ) if ( pObj->pCopy->pCopy ) // the net of the new object is already created continue; // create the new net - pNet = Abc_NtkFindOrCreateNet( pNtkNew, Abc_ObjName(pObj) ); + pNet = Abc_NtkFindOrCreateNet( pNtkNew, Abc_ObjName(pObj) ); // here we create ridiculous names net line "n48", where 48 is the ID of the node Abc_ObjAddFanin( pNet, pObj->pCopy ); pObj->pCopy->pCopy = pNet; } @@ -237,9 +213,9 @@ Abc_Ntk_t * Abc_NtkLogicSopToNetlist( Abc_Ntk_t * pNtk ) Abc_ObjAddFanin( pObj->pCopy, pFanin->pCopy->pCopy ); // duplicate EXDC if ( pNtk->pExdc ) - pNtkNew->pExdc = Abc_NtkLogicToNetlist( pNtk->pExdc, 0 ); + pNtkNew->pExdc = Abc_NtkToNetlist( pNtk->pExdc, 0 ); if ( !Abc_NtkCheck( pNtkNew ) ) - fprintf( stdout, "Abc_NtkLogicSopToNetlist(): Network check has failed.\n" ); + fprintf( stdout, "Abc_NtkLogicToNetlist(): Network check has failed.\n" ); return pNtkNew; } diff --git a/src/base/abc/abcNtk.c b/src/base/abc/abcNtk.c index 18b4a7c4..deddb712 100644 --- a/src/base/abc/abcNtk.c +++ b/src/base/abc/abcNtk.c @@ -242,9 +242,9 @@ Abc_Ntk_t * Abc_NtkStartRead( char * pName ) ***********************************************************************/ void Abc_NtkFinalizeRead( Abc_Ntk_t * pNtk ) { - Abc_Obj_t * pBox, * pObj, * pTerm; + Abc_Obj_t * pBox, * pObj, * pTerm, * pNet; int i; - if ( Abc_NtkHasBlackbox(pNtk) ) + if ( Abc_NtkHasBlackbox(pNtk) && Abc_NtkBoxNum(pNtk) == 0 ) { pBox = Abc_NtkCreateBlackbox(pNtk); Abc_NtkForEachPi( pNtk, pObj, i ) @@ -262,8 +262,23 @@ void Abc_NtkFinalizeRead( Abc_Ntk_t * pNtk ) return; } assert( Abc_NtkIsNetlist(pNtk) ); + + // check if constant 0 net is used + pNet = Abc_NtkFindOrCreateNet( pNtk, "1\'b0" ); + if ( Abc_ObjFanoutNum(pNet) == 0 ) + Abc_NtkDeleteObj(pNet); + else if ( Abc_ObjFaninNum(pNet) == 0 ) + Abc_ObjAddFanin( pNet, Abc_NtkCreateNodeConst0(pNtk) ); + // check if constant 1 net is used + pNet = Abc_NtkFindOrCreateNet( pNtk, "1\'b1" ); + if ( Abc_ObjFanoutNum(pNet) == 0 ) + Abc_NtkDeleteObj(pNet); + else if ( Abc_ObjFaninNum(pNet) == 0 ) + Abc_ObjAddFanin( pNet, Abc_NtkCreateNodeConst1(pNtk) ); + // fix the net drivers Abc_NtkFixNonDrivenNets( pNtk ); + // reorder the CI/COs to PI/POs first Abc_NtkOrderCisCos( pNtk ); } diff --git a/src/base/abc/abcShow.c b/src/base/abc/abcShow.c index ee86e8aa..40d1dcad 100644 --- a/src/base/abc/abcShow.c +++ b/src/base/abc/abcShow.c @@ -164,7 +164,7 @@ void Abc_NtkShow( Abc_Ntk_t * pNtk, int fGateNames, int fSeq, int fUseReverse ) } // convert to logic SOP if ( Abc_NtkIsLogic(pNtk) ) - Abc_NtkLogicToSop( pNtk, 0 ); + Abc_NtkToSop( pNtk, 0 ); // create the file name Abc_ShowGetFileName( pNtk->pName, FileNameDot ); // check that the file can be opened diff --git a/src/base/abc/abcUtil.c b/src/base/abc/abcUtil.c index 9a40fce9..353bf046 100644 --- a/src/base/abc/abcUtil.c +++ b/src/base/abc/abcUtil.c @@ -1404,6 +1404,8 @@ void Abc_NtkReassignIds( Abc_Ntk_t * pNtk ) // rehash the AIG Abc_AigRehash( pNtk->pManFunc ); + + // update the name manager!!! } /**Function************************************************************* diff --git a/src/base/abci/abc.c b/src/base/abci/abc.c index ae00ce5c..cf7cc0e9 100644 --- a/src/base/abci/abc.c +++ b/src/base/abci/abc.c @@ -3395,7 +3395,7 @@ int Abc_CommandLogic( Abc_Frame_t * pAbc, int argc, char ** argv ) } // get the new network - pNtkRes = Abc_NtkAigToLogicSop( pNtk ); + pNtkRes = Abc_NtkToLogic( pNtk ); if ( pNtkRes == NULL ) { fprintf( pErr, "Converting to a logic network has failed.\n" ); @@ -3984,7 +3984,7 @@ int Abc_CommandSop( Abc_Frame_t * pAbc, int argc, char ** argv ) fprintf( pErr, "Converting to SOP is possible only for logic networks.\n" ); return 1; } - if ( !Abc_NtkLogicToSop(pNtk, fDirect) ) + if ( !Abc_NtkToSop(pNtk, fDirect) ) { fprintf( pErr, "Converting to SOP has failed.\n" ); return 1; @@ -4047,7 +4047,7 @@ int Abc_CommandBdd( Abc_Frame_t * pAbc, int argc, char ** argv ) fprintf( pOut, "The logic network is already in the BDD form.\n" ); return 0; } - if ( !Abc_NtkLogicToBdd(pNtk) ) + if ( !Abc_NtkToBdd(pNtk) ) { fprintf( pErr, "Converting to BDD has failed.\n" ); return 1; @@ -4109,7 +4109,7 @@ int Abc_CommandAig( Abc_Frame_t * pAbc, int argc, char ** argv ) fprintf( pOut, "The logic network is already in the AIG form.\n" ); return 0; } - if ( !Abc_NtkLogicToAig(pNtk) ) + if ( !Abc_NtkToAig(pNtk) ) { fprintf( pErr, "Converting to AIG has failed.\n" ); return 1; @@ -7719,7 +7719,7 @@ int Abc_CommandSuperChoiceLut( Abc_Frame_t * pAbc, int argc, char ** argv ) } // convert the network into the SOP network - pNtkRes = Abc_NtkAigToLogicSop( pNtk ); + pNtkRes = Abc_NtkToLogic( pNtk ); // get the new network if ( !Abc_NtkSuperChoiceLut( pNtkRes, nLutSize, nCutSizeMax, fVerbose ) ) @@ -8716,7 +8716,7 @@ int Abc_CommandRetime( Abc_Frame_t * pAbc, int argc, char ** argv ) return 0; } // convert the network into an SOP network - pNtkRes = Abc_NtkAigToLogicSop( pNtk ); + pNtkRes = Abc_NtkToLogic( pNtk ); // perform the retiming Abc_NtkRetime( pNtkRes, Mode, fForward, fBackward, fVerbose ); // replace the current network @@ -8725,7 +8725,7 @@ int Abc_CommandRetime( Abc_Frame_t * pAbc, int argc, char ** argv ) } // get the network in the SOP form - if ( !Abc_NtkLogicToSop(pNtk, 0) ) + if ( !Abc_NtkToSop(pNtk, 0) ) { printf( "Converting to SOPs has failed.\n" ); return 0; @@ -9712,7 +9712,7 @@ int Abc_CommandSat( Abc_Frame_t * pAbc, int argc, char ** argv ) else { assert( Abc_NtkIsLogic(pNtk) ); - Abc_NtkLogicToBdd( pNtk ); + Abc_NtkToBdd( pNtk ); RetValue = Abc_NtkMiterSat( pNtk, (sint64)nConfLimit, (sint64)nInsLimit, fVerbose, NULL, NULL ); } diff --git a/src/base/abci/abcDebug.c b/src/base/abci/abcDebug.c index 7771148e..95b95d89 100644 --- a/src/base/abci/abcDebug.c +++ b/src/base/abci/abcDebug.c @@ -196,7 +196,7 @@ Abc_Ntk_t * Abc_NtkAutoDebugModify( Abc_Ntk_t * pNtkInit, int Step, int fConst1 Abc_NtkSweep( pNtk, 0 ); Abc_NtkCleanupSeq( pNtk, 0, 0, 0 ); - Abc_NtkLogicToSop( pNtk, 0 ); + Abc_NtkToSop( pNtk, 0 ); Abc_NtkCycleInitStateSop( pNtk, 50, 0 ); return pNtk; } diff --git a/src/base/abci/abcDress.c b/src/base/abci/abcDress.c index d7bb70fe..cc9ce0b9 100644 --- a/src/base/abci/abcDress.c +++ b/src/base/abci/abcDress.c @@ -63,7 +63,7 @@ void Abc_NtkDress( Abc_Ntk_t * pNtkLogic, char * pFileName, int fVerbose ) Abc_NtkCleanCopy(pNtkOrig); // convert it into the logic network - pNtkLogicOrig = Abc_NtkNetlistToLogic( pNtkOrig ); + pNtkLogicOrig = Abc_NtkToLogic( pNtkOrig ); // check that the networks have the same PIs/POs/latches if ( !Abc_NtkCompareSignals( pNtkLogic, pNtkLogicOrig, 1, 1 ) ) { diff --git a/src/base/abci/abcFxu.c b/src/base/abci/abcFxu.c index b6d57a5c..45515dd1 100644 --- a/src/base/abci/abcFxu.c +++ b/src/base/abci/abcFxu.c @@ -61,7 +61,7 @@ bool Abc_NtkFastExtract( Abc_Ntk_t * pNtk, Fxu_Data_t * p ) // Abc_NtkBddToSop(pNtk); } // get the network in the SOP form - if ( !Abc_NtkLogicToSop(pNtk, 0) ) + if ( !Abc_NtkToSop(pNtk, 0) ) { printf( "Abc_NtkFastExtract(): Converting to SOPs has failed.\n" ); return 0; diff --git a/src/base/abci/abcIvy.c b/src/base/abci/abcIvy.c index 0f0d9c8b..abcde7ce 100644 --- a/src/base/abci/abcIvy.c +++ b/src/base/abci/abcIvy.c @@ -27,9 +27,9 @@ /// DECLARATIONS /// //////////////////////////////////////////////////////////////////////// -static Abc_Ntk_t * Abc_NtkFromAig( Abc_Ntk_t * pNtkOld, Ivy_Man_t * pMan ); -static Abc_Ntk_t * Abc_NtkFromAigSeq( Abc_Ntk_t * pNtkOld, Ivy_Man_t * pMan, int fHaig ); -static Ivy_Man_t * Abc_NtkToAig( Abc_Ntk_t * pNtkOld ); +static Abc_Ntk_t * Abc_NtkFromIvy( Abc_Ntk_t * pNtkOld, Ivy_Man_t * pMan ); +static Abc_Ntk_t * Abc_NtkFromIvySeq( Abc_Ntk_t * pNtkOld, Ivy_Man_t * pMan, int fHaig ); +static Ivy_Man_t * Abc_NtkToIvy( Abc_Ntk_t * pNtkOld ); static void Abc_NtkStrashPerformAig( Abc_Ntk_t * pNtk, Ivy_Man_t * pMan ); static Ivy_Obj_t * Abc_NodeStrashAig( Ivy_Man_t * pMan, Abc_Obj_t * pNode ); @@ -93,7 +93,7 @@ Ivy_Man_t * Abc_NtkIvyBefore( Abc_Ntk_t * pNtk, int fSeq, int fUseDc ) if ( Abc_NtkGetChoiceNum( pNtk ) ) printf( "Warning: The choice nodes in the initial AIG are removed by strashing.\n" ); // convert to the AIG manager - pMan = Abc_NtkToAig( pNtk ); + pMan = Abc_NtkToIvy( pNtk ); if ( !Ivy_ManCheck( pMan ) ) { printf( "AIG check has failed.\n" ); @@ -130,9 +130,9 @@ Abc_Ntk_t * Abc_NtkIvyAfter( Abc_Ntk_t * pNtk, Ivy_Man_t * pMan, int fSeq, int f int nNodes, fCleanup = 1; // convert from the AIG manager if ( fSeq ) - pNtkAig = Abc_NtkFromAigSeq( pNtk, pMan, fHaig ); + pNtkAig = Abc_NtkFromIvySeq( pNtk, pMan, fHaig ); else - pNtkAig = Abc_NtkFromAig( pNtk, pMan ); + pNtkAig = Abc_NtkFromIvy( pNtk, pMan ); // report the cleanup results if ( !fHaig && fCleanup && (nNodes = Abc_AigCleanup(pNtkAig->pManFunc)) ) printf( "Warning: AIG cleanup removed %d nodes (this is not a bug).\n", nNodes ); @@ -608,7 +608,7 @@ Abc_Ntk_t * Abc_NtkIvy( Abc_Ntk_t * pNtk ) printf( "Warning: The choice nodes in the initial AIG are removed by strashing.\n" ); // convert to the AIG manager - pMan = Abc_NtkToAig( pNtk ); + pMan = Abc_NtkToIvy( pNtk ); if ( !Ivy_ManCheck( pMan ) ) { Vec_IntFree( vInit ); @@ -654,8 +654,8 @@ Abc_Ntk_t * Abc_NtkIvy( Abc_Ntk_t * pNtk ) /* // convert from the AIG manager - pNtkAig = Abc_NtkFromAig( pNtk, pMan ); -// pNtkAig = Abc_NtkFromAigSeq( pNtk, pMan ); + pNtkAig = Abc_NtkFromIvy( pNtk, pMan ); +// pNtkAig = Abc_NtkFromIvySeq( pNtk, pMan ); Ivy_ManStop( pMan ); // report the cleanup results @@ -691,7 +691,7 @@ Abc_Ntk_t * Abc_NtkIvy( Abc_Ntk_t * pNtk ) SeeAlso [] ***********************************************************************/ -Abc_Ntk_t * Abc_NtkFromAig( Abc_Ntk_t * pNtkOld, Ivy_Man_t * pMan ) +Abc_Ntk_t * Abc_NtkFromIvy( Abc_Ntk_t * pNtkOld, Ivy_Man_t * pMan ) { Vec_Int_t * vNodes; Abc_Ntk_t * pNtk; @@ -732,7 +732,7 @@ Abc_Ntk_t * Abc_NtkFromAig( Abc_Ntk_t * pNtkOld, Ivy_Man_t * pMan ) } Vec_IntFree( vNodes ); if ( !Abc_NtkCheck( pNtk ) ) - fprintf( stdout, "Abc_NtkFromAig(): Network check has failed.\n" ); + fprintf( stdout, "Abc_NtkFromIvy(): Network check has failed.\n" ); return pNtk; } @@ -747,7 +747,7 @@ Abc_Ntk_t * Abc_NtkFromAig( Abc_Ntk_t * pNtkOld, Ivy_Man_t * pMan ) SeeAlso [] ***********************************************************************/ -Abc_Ntk_t * Abc_NtkFromAigSeq( Abc_Ntk_t * pNtkOld, Ivy_Man_t * pMan, int fHaig ) +Abc_Ntk_t * Abc_NtkFromIvySeq( Abc_Ntk_t * pNtkOld, Ivy_Man_t * pMan, int fHaig ) { Vec_Int_t * vNodes, * vLatches; Abc_Ntk_t * pNtk; @@ -830,7 +830,7 @@ Abc_Ntk_t * Abc_NtkFromAigSeq( Abc_Ntk_t * pNtkOld, Ivy_Man_t * pMan, int fHaig Vec_IntFree( vLatches ); Vec_IntFree( vNodes ); if ( !Abc_NtkCheck( pNtk ) ) - fprintf( stdout, "Abc_NtkFromAigSeq(): Network check has failed.\n" ); + fprintf( stdout, "Abc_NtkFromIvySeq(): Network check has failed.\n" ); return pNtk; } @@ -845,7 +845,7 @@ Abc_Ntk_t * Abc_NtkFromAigSeq( Abc_Ntk_t * pNtkOld, Ivy_Man_t * pMan, int fHaig SeeAlso [] ***********************************************************************/ -Ivy_Man_t * Abc_NtkToAig( Abc_Ntk_t * pNtkOld ) +Ivy_Man_t * Abc_NtkToIvy( Abc_Ntk_t * pNtkOld ) { Ivy_Man_t * pMan; Abc_Obj_t * pObj; diff --git a/src/base/abci/abcMini.c b/src/base/abci/abcMini.c index dc90bee0..92985423 100644 --- a/src/base/abci/abcMini.c +++ b/src/base/abci/abcMini.c @@ -24,8 +24,8 @@ /// DECLARATIONS /// //////////////////////////////////////////////////////////////////////// -static Hop_Man_t * Abc_NtkToAig( Abc_Ntk_t * pNtk ); -static Abc_Ntk_t * Abc_NtkFromAig( Abc_Ntk_t * pNtkOld, Hop_Man_t * pMan ); +static Hop_Man_t * Abc_NtkToMini( Abc_Ntk_t * pNtk ); +static Abc_Ntk_t * Abc_NtkFromMini( Abc_Ntk_t * pNtkOld, Hop_Man_t * pMan ); //////////////////////////////////////////////////////////////////////// /// FUNCTION DEFINITIONS /// @@ -48,7 +48,7 @@ Abc_Ntk_t * Abc_NtkMiniBalance( Abc_Ntk_t * pNtk ) Hop_Man_t * pMan, * pTemp; assert( Abc_NtkIsStrash(pNtk) ); // convert to the AIG manager - pMan = Abc_NtkToAig( pNtk ); + pMan = Abc_NtkToMini( pNtk ); if ( pMan == NULL ) return NULL; if ( !Hop_ManCheck( pMan ) ) @@ -64,7 +64,7 @@ Abc_Ntk_t * Abc_NtkMiniBalance( Abc_Ntk_t * pNtk ) Hop_ManStop( pTemp ); Hop_ManPrintStats( pMan ); // convert from the AIG manager - pNtkAig = Abc_NtkFromAig( pNtk, pMan ); + pNtkAig = Abc_NtkFromMini( pNtk, pMan ); if ( pNtkAig == NULL ) return NULL; Hop_ManStop( pMan ); @@ -89,7 +89,7 @@ Abc_Ntk_t * Abc_NtkMiniBalance( Abc_Ntk_t * pNtk ) SeeAlso [] ***********************************************************************/ -Hop_Man_t * Abc_NtkToAig( Abc_Ntk_t * pNtk ) +Hop_Man_t * Abc_NtkToMini( Abc_Ntk_t * pNtk ) { Hop_Man_t * pMan; Abc_Obj_t * pObj; @@ -121,7 +121,7 @@ Hop_Man_t * Abc_NtkToAig( Abc_Ntk_t * pNtk ) SeeAlso [] ***********************************************************************/ -Abc_Ntk_t * Abc_NtkFromAig( Abc_Ntk_t * pNtk, Hop_Man_t * pMan ) +Abc_Ntk_t * Abc_NtkFromMini( Abc_Ntk_t * pNtk, Hop_Man_t * pMan ) { Vec_Ptr_t * vNodes; Abc_Ntk_t * pNtkNew; @@ -142,7 +142,7 @@ Abc_Ntk_t * Abc_NtkFromAig( Abc_Ntk_t * pNtk, Hop_Man_t * pMan ) Hop_ManForEachPo( pMan, pObj, i ) Abc_ObjAddFanin( Abc_NtkCo(pNtkNew, i), (Abc_Obj_t *)Hop_ObjChild0Copy(pObj) ); if ( !Abc_NtkCheck( pNtkNew ) ) - fprintf( stdout, "Abc_NtkFromAig(): Network check has failed.\n" ); + fprintf( stdout, "Abc_NtkFromMini(): Network check has failed.\n" ); return pNtkNew; } diff --git a/src/base/abci/abcQuant.c b/src/base/abci/abcQuant.c index 77d640c2..8591663e 100644 --- a/src/base/abci/abcQuant.c +++ b/src/base/abci/abcQuant.c @@ -30,6 +30,39 @@ /**Function************************************************************* + Synopsis [Performs fast synthesis.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Abc_NtkSynthesize( Abc_Ntk_t ** ppNtk, int fMoreEffort ) +{ + Abc_Ntk_t * pNtk, * pNtkTemp; + + pNtk = *ppNtk; + + Abc_NtkRewrite( pNtk, 0, 0, 0, 0, 0 ); + Abc_NtkRefactor( pNtk, 10, 16, 0, 0, 0, 0 ); + pNtk = Abc_NtkBalance( pNtkTemp = pNtk, 0, 0, 0 ); + Abc_NtkDelete( pNtkTemp ); + + if ( fMoreEffort ) + { + Abc_NtkRewrite( pNtk, 0, 0, 0, 0, 0 ); + Abc_NtkRefactor( pNtk, 10, 16, 0, 0, 0, 0 ); + pNtk = Abc_NtkBalance( pNtkTemp = pNtk, 0, 0, 0 ); + Abc_NtkDelete( pNtkTemp ); + } + + *ppNtk = pNtk; +} + +/**Function************************************************************* + Synopsis [Existentially quantifies one variable.] Description [] @@ -113,6 +146,7 @@ Abc_Ntk_t * Abc_NtkTransRel( Abc_Ntk_t * pNtk, int fInputs, int fVerbose ) Abc_Ntk_t * pNtkNew; Abc_Obj_t * pObj, * pMiter; int i, nLatches; + int fSynthesis = 1; assert( Abc_NtkIsStrash(pNtk) ); assert( Abc_NtkLatchNum(pNtk) ); @@ -136,7 +170,10 @@ Abc_Ntk_t * Abc_NtkTransRel( Abc_Ntk_t * pNtk, int fInputs, int fVerbose ) // create PI variables Abc_NtkForEachPi( pNtk, pObj, i ) Abc_NtkDupObj( pNtkNew, pObj, 1 ); + // create the PO + Abc_NtkCreatePo( pNtkNew ); // restrash the nodes (assuming a topological order of the old network) + Abc_AigConst1(pNtk)->pCopy = Abc_AigConst1(pNtkNew); Abc_NtkForEachNode( pNtk, pObj, i ) pObj->pCopy = Abc_AigAnd( pNtkNew->pManFunc, Abc_ObjChild0Copy(pObj), Abc_ObjChild1Copy(pObj) ); // create the function of the primary output @@ -150,7 +187,7 @@ Abc_Ntk_t * Abc_NtkTransRel( Abc_Ntk_t * pNtk, int fInputs, int fVerbose ) pMiter = Abc_AigMiter( pNtkNew->pManFunc, vPairs ); Vec_PtrFree( vPairs ); // add the primary output - Abc_ObjAddFanin( Abc_NtkCreatePo(pNtkNew), Abc_ObjNot(pMiter) ); + Abc_ObjAddFanin( Abc_NtkPo(pNtkNew,0), Abc_ObjNot(pMiter) ); Abc_ObjAssignName( Abc_NtkPo(pNtkNew,0), "rel", NULL ); // quantify inputs @@ -158,7 +195,20 @@ Abc_Ntk_t * Abc_NtkTransRel( Abc_Ntk_t * pNtk, int fInputs, int fVerbose ) { assert( Abc_NtkPiNum(pNtkNew) == Abc_NtkPiNum(pNtk) + 2*nLatches ); for ( i = Abc_NtkPiNum(pNtkNew) - 1; i >= 2*nLatches; i-- ) +// for ( i = 2*nLatches; i < Abc_NtkPiNum(pNtkNew); i++ ) + { Abc_NtkQuantify( pNtkNew, i, fVerbose ); +// if ( fSynthesis && (i % 3 == 2) ) + if ( fSynthesis ) + { + Abc_NtkCleanData( pNtkNew ); + Abc_AigCleanup( pNtkNew->pManFunc ); + Abc_NtkSynthesize( &pNtkNew, 1 ); + } +// printf( "Var = %3d. Nodes = %6d. ", Abc_NtkPiNum(pNtkNew) - 1 - i, Abc_NtkNodeNum(pNtkNew) ); +// printf( "Var = %3d. Nodes = %6d. ", i - 2*nLatches, Abc_NtkNodeNum(pNtkNew) ); + } +// printf( "\n" ); Abc_NtkCleanData( pNtkNew ); Abc_AigCleanup( pNtkNew->pManFunc ); for ( i = Abc_NtkPiNum(pNtkNew) - 1; i >= 2*nLatches; i-- ) @@ -169,7 +219,7 @@ Abc_Ntk_t * Abc_NtkTransRel( Abc_Ntk_t * pNtk, int fInputs, int fVerbose ) } } - // make sure that everything is okay + // check consistency of the network if ( !Abc_NtkCheck( pNtkNew ) ) { printf( "Abc_NtkTransRel: The network check has failed.\n" ); @@ -263,6 +313,7 @@ Abc_Ntk_t * Abc_NtkReachability( Abc_Ntk_t * pNtkRel, int nIters, int fVerbose ) int clk, i, v, nVars, nNodesOld, nNodesNew, nNodesPrev; int fFixedPoint = 0; int fSynthesis = 1; + int fMoreEffort = 1; assert( Abc_NtkIsStrash(pNtkRel) ); assert( Abc_NtkLatchNum(pNtkRel) == 0 ); @@ -273,8 +324,8 @@ Abc_Ntk_t * Abc_NtkReachability( Abc_Ntk_t * pNtkRel, int nIters, int fVerbose ) pNtkReached = Abc_NtkDup( pNtkFront ); //Abc_NtkShow( pNtkReached, 0, 0, 0 ); - if ( fVerbose ) - printf( "Transition relation = %6d.\n", Abc_NtkNodeNum(pNtkRel) ); +// if ( fVerbose ) +// printf( "Transition relation = %6d.\n", Abc_NtkNodeNum(pNtkRel) ); // perform iterations of reachability analysis nNodesPrev = Abc_NtkNodeNum(pNtkFront); @@ -293,25 +344,13 @@ Abc_Ntk_t * Abc_NtkReachability( Abc_Ntk_t * pNtkRel, int nIters, int fVerbose ) { Abc_NtkCleanData( pNtkNext ); Abc_AigCleanup( pNtkNext->pManFunc ); - - Abc_NtkRewrite( pNtkNext, 0, 0, 0, 0, 0 ); - pNtkNext = Abc_NtkBalance( pNtkTemp = pNtkNext, 0, 0, 0 ); - Abc_NtkDelete( pNtkTemp ); + Abc_NtkSynthesize( &pNtkNext, fMoreEffort ); } } Abc_NtkCleanData( pNtkNext ); Abc_AigCleanup( pNtkNext->pManFunc ); if ( fSynthesis ) - { - Abc_NtkRewrite( pNtkNext, 0, 0, 0, 0, 0 ); - pNtkNext = Abc_NtkBalance( pNtkTemp = pNtkNext, 0, 0, 0 ); - Abc_NtkDelete( pNtkTemp ); - - Abc_NtkRewrite( pNtkNext, 0, 0, 0, 0, 0 ); - Abc_NtkRefactor( pNtkReached, 10, 16, 0, 0, 0, 0 ); - pNtkNext = Abc_NtkBalance( pNtkTemp = pNtkNext, 0, 0, 0 ); - Abc_NtkDelete( pNtkTemp ); - } + Abc_NtkSynthesize( &pNtkNext, 1 ); // map the next states into the current states pNtkNext = Abc_NtkSwapVariables( pNtkTemp = pNtkNext ); Abc_NtkDelete( pNtkTemp ); @@ -333,20 +372,15 @@ Abc_Ntk_t * Abc_NtkReachability( Abc_Ntk_t * pNtkRel, int nIters, int fVerbose ) nNodesOld = Abc_NtkNodeNum(pNtkFront); if ( fSynthesis ) { - Abc_NtkRewrite( pNtkFront, 0, 0, 0, 0, 0 ); - pNtkFront = Abc_NtkBalance( pNtkTemp = pNtkFront, 0, 0, 0 ); - Abc_NtkDelete( pNtkTemp ); - - Abc_NtkRewrite( pNtkReached, 0, 0, 0, 0, 0 ); - pNtkReached = Abc_NtkBalance( pNtkTemp = pNtkReached, 0, 0, 0 ); - Abc_NtkDelete( pNtkTemp ); + Abc_NtkSynthesize( &pNtkFront, fMoreEffort ); + Abc_NtkSynthesize( &pNtkReached, fMoreEffort ); } nNodesNew = Abc_NtkNodeNum(pNtkFront); // print statistics if ( fVerbose ) { - printf( "I = %3d : Reached = %6d Front = %6d FrontM = %6d %6.2f %% ", - i + 1, Abc_NtkNodeNum(pNtkReached), nNodesOld, nNodesNew, 100.0*(nNodesNew-nNodesPrev)/nNodesNew ); + printf( "I = %3d : Reach = %6d Fr = %6d FrM = %6d %7.2f %% ", + i + 1, Abc_NtkNodeNum(pNtkReached), nNodesOld, nNodesNew, 100.0*(nNodesNew-nNodesPrev)/nNodesPrev ); PRT( "T", clock() - clk ); } nNodesPrev = Abc_NtkNodeNum(pNtkFront); @@ -354,13 +388,6 @@ Abc_Ntk_t * Abc_NtkReachability( Abc_Ntk_t * pNtkRel, int nIters, int fVerbose ) if ( !fFixedPoint ) fprintf( stdout, "Reachability analysis stopped after %d iterations.\n", nIters ); - // report the stats - if ( fVerbose ) - { -// nMints = 1; -// fprintf( stdout, "The estimated number of minterms in the reachable state set = %d. (%6.2f %%)\n", nMints, 100.0*nMints/(1<<Abc_NtkLatchNum(pNtk)) ); - } - // complement the output to represent the set of unreachable states Abc_ObjXorFaninC( Abc_NtkPo(pNtkReached,0), 0 ); @@ -372,7 +399,7 @@ Abc_Ntk_t * Abc_NtkReachability( Abc_Ntk_t * pNtkRel, int nIters, int fVerbose ) Abc_NtkDeleteObj( pObj ); } - // make sure that everything is okay + // check consistency of the network if ( !Abc_NtkCheck( pNtkReached ) ) { printf( "Abc_NtkReachability: The network check has failed.\n" ); diff --git a/src/base/abci/abcStrash.c b/src/base/abci/abcStrash.c index 88ef009b..45fc9089 100644 --- a/src/base/abci/abcStrash.c +++ b/src/base/abci/abcStrash.c @@ -105,7 +105,7 @@ Abc_Ntk_t * Abc_NtkStrash( Abc_Ntk_t * pNtk, bool fAllNodes, bool fCleanup ) if ( Abc_NtkIsStrash(pNtk) ) return Abc_NtkRestrash( pNtk, fCleanup ); // convert the node representation in the logic network to the AIG form - if ( !Abc_NtkLogicToAig(pNtk) ) + if ( !Abc_NtkToAig(pNtk) ) { printf( "Converting to AIGs has failed.\n" ); return NULL; @@ -156,7 +156,7 @@ int Abc_NtkAppend( Abc_Ntk_t * pNtk1, Abc_Ntk_t * pNtk2, int fAddPos ) // the first network should be an AIG assert( Abc_NtkIsStrash(pNtk1) ); assert( Abc_NtkIsLogic(pNtk2) || Abc_NtkIsStrash(pNtk2) ); - if ( Abc_NtkIsLogic(pNtk2) && !Abc_NtkLogicToAig(pNtk2) ) + if ( Abc_NtkIsLogic(pNtk2) && !Abc_NtkToAig(pNtk2) ) { printf( "Converting to AIGs has failed.\n" ); return 0; diff --git a/src/base/abci/abcSweep.c b/src/base/abci/abcSweep.c index 1b63b23c..4791c859 100644 --- a/src/base/abci/abcSweep.c +++ b/src/base/abci/abcSweep.c @@ -536,7 +536,7 @@ int Abc_NtkSweep( Abc_Ntk_t * pNtk, int fVerbose ) int i, nNodesOld; assert( Abc_NtkIsLogic(pNtk) ); // convert network to BDD representation - if ( !Abc_NtkLogicToBdd(pNtk) ) + if ( !Abc_NtkToBdd(pNtk) ) { fprintf( stdout, "Converting to BDD has failed.\n" ); return 1; diff --git a/src/base/cmd/cmd.c b/src/base/cmd/cmd.c index 08584290..92691d6c 100644 --- a/src/base/cmd/cmd.c +++ b/src/base/cmd/cmd.c @@ -1265,7 +1265,7 @@ int CmdCommandSis( Abc_Frame_t * pAbc, int argc, char **argv ) } // write out the current network - pNetlist = Abc_NtkLogicToNetlist(pNtk,0); + pNetlist = Abc_NtkToNetlist(pNtk,0); if ( pNetlist == NULL ) { fprintf( pErr, "Cannot produce the intermediate network.\n" ); @@ -1406,7 +1406,7 @@ int CmdCommandMvsis( Abc_Frame_t * pAbc, int argc, char **argv ) } // write out the current network - pNetlist = Abc_NtkLogicToNetlist(pNtk,0); + pNetlist = Abc_NtkToNetlist(pNtk,0); if ( pNetlist == NULL ) { fprintf( pErr, "Cannot produce the intermediate network.\n" ); @@ -1552,7 +1552,7 @@ int CmdCommandCapo( Abc_Frame_t * pAbc, int argc, char **argv ) } // write out the current network - pNetlist = Abc_NtkLogicToNetlist(pNtk,0); + pNetlist = Abc_NtkToNetlist(pNtk,0); if ( pNetlist == NULL ) { fprintf( pErr, "Cannot produce the intermediate network.\n" ); diff --git a/src/base/io/io.c b/src/base/io/io.c index 2267d4e7..3603519f 100644 --- a/src/base/io/io.c +++ b/src/base/io/io.c @@ -55,7 +55,7 @@ static int IoCommandWritePla ( Abc_Frame_t * pAbc, int argc, char **argv ); static int IoCommandWriteVerilog( Abc_Frame_t * pAbc, int argc, char **argv ); static int IoCommandWriteVerLib ( Abc_Frame_t * pAbc, int argc, char **argv ); -extern Abc_Lib_t * Ver_ParseFile( char * pFileName, Abc_Lib_t * pGateLib, int fCheck, int fUseMemMan ); +extern int glo_fMapped; //////////////////////////////////////////////////////////////////////// /// FUNCTION DEFINITIONS /// @@ -139,11 +139,15 @@ int IoCommandRead( Abc_Frame_t * pAbc, int argc, char ** argv ) int c; fCheck = 1; + glo_fMapped = 0; Extra_UtilGetoptReset(); - while ( ( c = Extra_UtilGetopt( argc, argv, "ch" ) ) != EOF ) + while ( ( c = Extra_UtilGetopt( argc, argv, "mch" ) ) != EOF ) { switch ( c ) { + case 'm': + glo_fMapped ^= 1; + break; case 'c': fCheck ^= 1; break; @@ -166,10 +170,11 @@ int IoCommandRead( Abc_Frame_t * pAbc, int argc, char ** argv ) return 0; usage: - fprintf( pAbc->Err, "usage: read [-ch] <file>\n" ); + fprintf( pAbc->Err, "usage: read [-mch] <file>\n" ); fprintf( pAbc->Err, "\t replaces the current network by the network read from <file>\n" ); fprintf( pAbc->Err, "\t by calling the parser that matches the extension of <file>\n" ); fprintf( pAbc->Err, "\t (to read a hierarchical design, use \"read_hie\")\n" ); + fprintf( pAbc->Err, "\t-m : toggle reading mapped Verilog [default = %s]\n", glo_fMapped? "yes":"no" ); fprintf( pAbc->Err, "\t-c : toggle network check after reading [default = %s]\n", fCheck? "yes":"no" ); fprintf( pAbc->Err, "\t-h : prints the command summary\n" ); fprintf( pAbc->Err, "\tfile : the name of a file to read\n" ); @@ -332,7 +337,13 @@ int IoCommandReadBlif( Abc_Frame_t * pAbc, int argc, char ** argv ) pNtk = Io_ReadBlifAsAig( pFileName, fCheck ); else // pNtk = Io_Read( pFileName, IO_FILE_BLIF, fCheck ); + { + Abc_Ntk_t * pTemp; pNtk = Io_ReadBlif( pFileName, fCheck ); + pNtk = Abc_NtkToLogic( pTemp = pNtk ); + Abc_NtkDelete( pTemp ); + } + if ( pNtk == NULL ) return 1; // replace the current network @@ -657,11 +668,15 @@ int IoCommandReadVerilog( Abc_Frame_t * pAbc, int argc, char ** argv ) return 0; fCheck = 1; + glo_fMapped = 0; Extra_UtilGetoptReset(); - while ( ( c = Extra_UtilGetopt( argc, argv, "ch" ) ) != EOF ) + while ( ( c = Extra_UtilGetopt( argc, argv, "mch" ) ) != EOF ) { switch ( c ) { + case 'm': + glo_fMapped ^= 1; + break; case 'c': fCheck ^= 1; break; @@ -684,8 +699,9 @@ int IoCommandReadVerilog( Abc_Frame_t * pAbc, int argc, char ** argv ) return 0; usage: - fprintf( pAbc->Err, "usage: read_verilog [-ch] <file>\n" ); - fprintf( pAbc->Err, "\t read the network in Verilog (IWLS 2005 subset)\n" ); + fprintf( pAbc->Err, "usage: read_verilog [-mch] <file>\n" ); + fprintf( pAbc->Err, "\t read the network in Verilog (IWLS 2002/2005 subset)\n" ); + fprintf( pAbc->Err, "\t-m : toggle reading mapped Verilog [default = %s]\n", glo_fMapped? "yes":"no" ); fprintf( pAbc->Err, "\t-c : toggle network check after reading [default = %s]\n", fCheck? "yes":"no" ); fprintf( pAbc->Err, "\t-h : prints the command summary\n" ); fprintf( pAbc->Err, "\tfile : the name of a file to read\n" ); @@ -712,6 +728,7 @@ int IoCommandReadVer( Abc_Frame_t * pAbc, int argc, char ** argv ) int fCheck; int c; extern Abc_Ntk_t * Abc_LibDeriveAig( Abc_Ntk_t * pNtk, Abc_Lib_t * pLib ); + extern Abc_Lib_t * Ver_ParseFile( char * pFileName, Abc_Lib_t * pGateLib, int fCheck, int fUseMemMan ); fCheck = 1; Extra_UtilGetoptReset(); @@ -921,11 +938,15 @@ int IoCommandWriteHie( Abc_Frame_t * pAbc, int argc, char **argv ) char * pBaseName, * pFileName; int c; + glo_fMapped = 0; Extra_UtilGetoptReset(); - while ( ( c = Extra_UtilGetopt( argc, argv, "h" ) ) != EOF ) + while ( ( c = Extra_UtilGetopt( argc, argv, "mh" ) ) != EOF ) { switch ( c ) { + case 'm': + glo_fMapped ^= 1; + break; case 'h': goto usage; default: @@ -946,6 +967,7 @@ usage: fprintf( pAbc->Err, "usage: write_hie [-h] <orig> <file>\n" ); fprintf( pAbc->Err, "\t writes the current network into <file> by calling\n" ); fprintf( pAbc->Err, "\t the hierarchical writer that matches the extension of <file>\n" ); + fprintf( pAbc->Err, "\t-m : toggle reading mapped Verilog for <orig> [default = %s]\n", glo_fMapped? "yes":"no" ); fprintf( pAbc->Err, "\t-h : print the help massage\n" ); fprintf( pAbc->Err, "\torig : the name of the original file with the hierarchical design\n" ); fprintf( pAbc->Err, "\tfile : the name of the file to write\n" ); diff --git a/src/base/io/ioReadBench.c b/src/base/io/ioReadBench.c index d8213994..7e54e5e3 100644 --- a/src/base/io/ioReadBench.c +++ b/src/base/io/ioReadBench.c @@ -150,7 +150,7 @@ Abc_Ntk_t * Io_ReadBenchNetwork( Extra_FileReader_t * p ) Abc_ObjSetData( pNode, Abc_SopRegister( pNtk->pManFunc, " 0\n" ) ); else { - printf( "Cannot determine gate type \"%s\" in line %d.\n", pType, Extra_FileReaderGetLineNumber(p, 0) ); + printf( "Io_ReadBenchNetwork(): Cannot determine gate type \"%s\" in line %d.\n", pType, Extra_FileReaderGetLineNumber(p, 0) ); Vec_StrFree( vString ); Abc_NtkDelete( pNtk ); return NULL; diff --git a/src/base/io/ioReadBlifMv.c b/src/base/io/ioReadBlifMv.c index 46a202e1..3e09caf0 100644 --- a/src/base/io/ioReadBlifMv.c +++ b/src/base/io/ioReadBlifMv.c @@ -98,6 +98,7 @@ static int Io_MvParseLineSubckt( Io_MvMod_t * p, char * pLine ); static int Io_MvParseLineMv( Io_MvMod_t * p, char * pLine ); static int Io_MvParseLineNamesMv( Io_MvMod_t * p, char * pLine, int fReset ); static int Io_MvParseLineNamesBlif( Io_MvMod_t * p, char * pLine ); +static int Io_MvParseLineGateBlif( Io_MvMod_t * p, Vec_Ptr_t * vTokens ); static int Io_MvCharIsSpace( char s ) { return s == ' ' || s == '\t' || s == '\r' || s == '\n'; } static int Io_MvCharIsMvSymb( char s ) { return s == '(' || s == ')' || s == '{' || s == '}' || s == '-' || s == ',' || s == '!'; } @@ -568,7 +569,7 @@ static void Io_MvReadPreparse( Io_MvMan_t * p ) // parse directives if ( *(pCur-1) != '.' ) continue; - if ( !strncmp(pCur, "names", 5) || !strncmp(pCur, "table", 5) ) + if ( !strncmp(pCur, "names", 5) || !strncmp(pCur, "table", 5) || !strncmp(pCur, "gate", 4) ) Vec_PtrPush( p->pLatest->vNames, pCur ); else if ( p->fBlifMv && (!strncmp(pCur, "def ", 4) || !strncmp(pCur, "default ", 8)) ) continue; @@ -1464,6 +1465,10 @@ static int Io_MvParseLineNamesBlif( Io_MvMod_t * p, char * pLine ) char * pName; assert( !p->pMan->fBlifMv ); Io_MvSplitIntoTokens( vTokens, pLine, '\0' ); + // parse the mapped node + if ( !strcmp(Vec_PtrEntry(vTokens,0), "gate") ) + return Io_MvParseLineGateBlif( p, vTokens ); + // parse the regular name line assert( !strcmp(Vec_PtrEntry(vTokens,0), "names") ); pName = Vec_PtrEntryLast( vTokens ); pNet = Abc_NtkFindOrCreateNet( p->pNtk, pName ); @@ -1483,6 +1488,104 @@ static int Io_MvParseLineNamesBlif( Io_MvMod_t * p, char * pLine ) } +#include "mio.h" +#include "main.h" + +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +static char * Io_ReadBlifCleanName( char * pName ) +{ + int i, Length; + Length = strlen(pName); + for ( i = 0; i < Length; i++ ) + if ( pName[i] == '=' ) + return pName + i + 1; + return NULL; +} + +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +static int Io_MvParseLineGateBlif( Io_MvMod_t * p, Vec_Ptr_t * vTokens ) +{ + Mio_Library_t * pGenlib; + Mio_Gate_t * pGate; + Abc_Obj_t * pNode; + char ** ppNames, * pName; + int i, nNames; + + pName = vTokens->pArray[0]; + + // check that the library is available + pGenlib = Abc_FrameReadLibGen(); + if ( pGenlib == NULL ) + { + sprintf( p->pMan->sError, "Line %d: The current library is not available.", Io_MvGetLine(p->pMan, pName) ); + return 0; + } + + // create a new node and add it to the network + if ( vTokens->nSize < 2 ) + { + sprintf( p->pMan->sError, "Line %d: The .gate line has less than two tokens.", Io_MvGetLine(p->pMan, pName) ); + return 0; + } + + // get the gate + pGate = Mio_LibraryReadGateByName( pGenlib, vTokens->pArray[1] ); + if ( pGate == NULL ) + { + sprintf( p->pMan->sError, "Line %d: Cannot find gate \"%s\" in the library.", Io_MvGetLine(p->pMan, pName), vTokens->pArray[1] ); + return 0; + } + + // if this is the first line with gate, update the network type + if ( Abc_NtkNodeNum(p->pNtk) == 0 ) + { + assert( p->pNtk->ntkFunc == ABC_FUNC_SOP ); + p->pNtk->ntkFunc = ABC_FUNC_MAP; + Extra_MmFlexStop( p->pNtk->pManFunc ); + p->pNtk->pManFunc = pGenlib; + } + + // remove the formal parameter names + for ( i = 2; i < vTokens->nSize; i++ ) + { + vTokens->pArray[i] = Io_ReadBlifCleanName( vTokens->pArray[i] ); + if ( vTokens->pArray[i] == NULL ) + { + sprintf( p->pMan->sError, "Line %d: Invalid gate input assignment.", Io_MvGetLine(p->pMan, pName) ); + return 0; + } + } + + // create the node + ppNames = (char **)vTokens->pArray + 2; + nNames = vTokens->nSize - 3; + pNode = Io_ReadCreateNode( p->pNtk, ppNames[nNames], ppNames, nNames ); + + // set the pointer to the functionality of the node + Abc_ObjSetData( pNode, pGate ); + return 1; +} + //////////////////////////////////////////////////////////////////////// /// END OF FILE /// //////////////////////////////////////////////////////////////////////// diff --git a/src/base/io/ioReadVerilog.c b/src/base/io/ioReadVerilog.c index 5956a9bc..090cf254 100644 --- a/src/base/io/ioReadVerilog.c +++ b/src/base/io/ioReadVerilog.c @@ -45,13 +45,12 @@ Abc_Ntk_t * Io_ReadVerilog( char * pFileName, int fCheck ) { Abc_Ntk_t * pNtk; Abc_Lib_t * pDesign; - int i; // parse the verilog file - pDesign = Ver_ParseFile( pFileName, NULL, 1, fCheck ); + pDesign = Ver_ParseFile( pFileName, NULL, fCheck, 1 ); if ( pDesign == NULL ) return NULL; - +/* // extract the master network pNtk = Vec_PtrEntryLast( pDesign->vModules ); pNtk->pDesign = pDesign; @@ -75,6 +74,28 @@ Abc_Ntk_t * Io_ReadVerilog( char * pFileName, int fCheck ) // check that there is no cyclic dependency Abc_NtkIsAcyclicHierarchy( pNtk ); } +*/ + // extract the master network + pNtk = Vec_PtrEntry( pDesign->vModules, 0 ); + pNtk->pDesign = pDesign; + pDesign->pManFunc = NULL; + +//Io_WriteVerilog( pNtk, "_temp.v" ); + + // verify the design for cyclic dependence + assert( Vec_PtrSize(pDesign->vModules) > 0 ); + if ( Vec_PtrSize(pDesign->vModules) == 1 ) + { +// printf( "Warning: The design is not hierarchical.\n" ); + Abc_LibFree( pDesign, pNtk ); + pNtk->pDesign = NULL; + pNtk->pSpec = Extra_UtilStrsav( pFileName ); + } + else + { + // check that there is no cyclic dependency + Abc_NtkIsAcyclicHierarchy( pNtk ); + } return pNtk; } diff --git a/src/base/io/ioUtil.c b/src/base/io/ioUtil.c index 2de93ddf..0ac3181a 100644 --- a/src/base/io/ioUtil.c +++ b/src/base/io/ioUtil.c @@ -209,7 +209,7 @@ Abc_NtkPrintStats( stdout, pNtk, 0 ); // convert blackboxes if ( Abc_NtkBlackboxNum(pNtk) > 0 ) { - printf( "Hierarchy reader converted %d blackboxes.\n", Abc_NtkBlackboxNum(pNtk) ); + printf( "Hierarchy reader converted %d instances of blackboxes.\n", Abc_NtkBlackboxNum(pNtk) ); pNtk = Abc_NtkConvertBlackboxes( pTemp = pNtk ); Abc_NtkDelete( pTemp ); if ( pNtk == NULL ) @@ -219,7 +219,7 @@ Abc_NtkPrintStats( stdout, pNtk, 0 ); } } // convert the netlist into the logic network - pNtk = Abc_NtkNetlistToLogic( pTemp = pNtk ); + pNtk = Abc_NtkToLogic( pTemp = pNtk ); Abc_NtkDelete( pTemp ); if ( pNtk == NULL ) { @@ -244,7 +244,6 @@ Abc_Ntk_t * Io_ReadHie( char * pFileName, Io_FileType_t FileType, int fCheck ) { Abc_Ntk_t * pNtk, * pTemp; // detect the file type - if ( Io_ReadFileType(pFileName) == IO_FILE_BLIF ) pNtk = Io_ReadBlifMv( pFileName, 0, fCheck ); // else if ( Io_ReadFileType(pFileName) == IO_FILE_BLIFMV ) @@ -274,7 +273,7 @@ Abc_Ntk_t * Io_ReadHie( char * pFileName, Io_FileType_t FileType, int fCheck ) // convert blackboxes if ( Abc_NtkBlackboxNum(pNtk) > 0 ) { - printf( "Hierarchy reader converted %d blackboxes.\n", Abc_NtkBlackboxNum(pNtk) ); + printf( "Hierarchy reader converted %d instances of blackboxes.\n", Abc_NtkBlackboxNum(pNtk) ); pNtk = Abc_NtkConvertBlackboxes( pTemp = pNtk ); Abc_NtkDelete( pTemp ); if ( pNtk == NULL ) @@ -284,7 +283,7 @@ Abc_Ntk_t * Io_ReadHie( char * pFileName, Io_FileType_t FileType, int fCheck ) } } // convert the netlist into the logic network - pNtk = Abc_NtkNetlistToLogic( pTemp = pNtk ); + pNtk = Abc_NtkToLogic( pTemp = pNtk ); Abc_NtkDelete( pTemp ); if ( pNtk == NULL ) { @@ -350,6 +349,7 @@ void Io_Write( Abc_Ntk_t * pNtk, char * pFileName, Io_FileType_t FileType ) Io_WriteGml( pNtk, pFileName ); return; } + // convert logic network into netlist if ( FileType == IO_FILE_PLA ) { @@ -359,13 +359,13 @@ void Io_Write( Abc_Ntk_t * pNtk, char * pFileName, Io_FileType_t FileType ) return; } if ( Abc_NtkIsComb(pNtk) ) - pNtkTemp = Abc_NtkLogicToNetlist( pNtk, 1 ); + pNtkTemp = Abc_NtkToNetlist( pNtk, 1 ); else { fprintf( stdout, "Latches are writen into the PLA file at PI/PO pairs.\n" ); pNtkCopy = Abc_NtkDup( pNtk ); Abc_NtkMakeComb( pNtkCopy ); - pNtkTemp = Abc_NtkLogicToNetlist( pNtk, 1 ); + pNtkTemp = Abc_NtkToNetlist( pNtk, 1 ); Abc_NtkDelete( pNtkCopy ); } } @@ -376,31 +376,37 @@ void Io_Write( Abc_Ntk_t * pNtk, char * pFileName, Io_FileType_t FileType ) fprintf( stdout, "Writing BENCH is available for AIGs.\n" ); return; } - pNtkTemp = Abc_NtkLogicToNetlistBench( pNtk ); + pNtkTemp = Abc_NtkToNetlistBench( pNtk ); } else - pNtkTemp = Abc_NtkLogicToNetlist( pNtk, 0 ); + pNtkTemp = Abc_NtkToNetlist( pNtk, 0 ); + if ( pNtkTemp == NULL ) { fprintf( stdout, "Converting to netlist has failed.\n" ); return; } + if ( FileType == IO_FILE_BLIF ) + { + if ( !Abc_NtkHasSop(pNtkTemp) && !Abc_NtkHasMapping(pNtkTemp) ) + Abc_NtkToSop( pNtkTemp, 0 ); Io_WriteBlif( pNtkTemp, pFileName, 1 ); + } else if ( FileType == IO_FILE_BENCH ) Io_WriteBench( pNtkTemp, pFileName ); else if ( FileType == IO_FILE_PLA ) Io_WritePla( pNtkTemp, pFileName ); else if ( FileType == IO_FILE_EQN ) { - if ( Abc_NtkIsSopNetlist(pNtkTemp) ) - Abc_NtkSopToAig( pNtkTemp ); + if ( !Abc_NtkHasAig(pNtkTemp) ) + Abc_NtkToAig( pNtkTemp ); Io_WriteEqn( pNtkTemp, pFileName ); } else if ( FileType == IO_FILE_VERILOG ) { - if ( Abc_NtkIsSopNetlist(pNtkTemp) ) - Abc_NtkSopToAig( pNtkTemp ); + if ( !Abc_NtkHasAig(pNtkTemp) && !Abc_NtkHasMapping(pNtkTemp) ) + Abc_NtkToAig( pNtkTemp ); Io_WriteVerilog( pNtkTemp, pFileName ); } else @@ -451,25 +457,17 @@ void Io_WriteHie( Abc_Ntk_t * pNtk, char * pBaseName, char * pFileName ) // reintroduce the boxes into the netlist if ( Abc_NtkBlackboxNum(pNtkBase) > 0 ) { - // bring the current network to the same representation - if ( Abc_NtkIsLogic(pNtk) ) - { - if ( Abc_NtkIsSopNetlist(pNtkBase) ) - Abc_NtkLogicToSop( pNtk, 0 ); - else if ( Abc_NtkIsAigNetlist(pNtkBase) ) - Abc_NtkLogicToAig( pNtk ); - } // derive the netlist - pNtkResult = Abc_NtkLogicToNetlist( pNtk, 0 ); + pNtkResult = Abc_NtkToNetlist( pNtk, 0 ); pNtkResult = Abc_NtkInsertNewLogic( pNtkBase, pNtkTemp = pNtkResult ); Abc_NtkDelete( pNtkTemp ); if ( pNtkResult ) - printf( "Hierarchy writer reintroduced %d blackboxes.\n", Abc_NtkBlackboxNum(pNtkBase) ); + printf( "Hierarchy writer reintroduced %d instances of blackboxes.\n", Abc_NtkBlackboxNum(pNtkBase) ); } else { printf( "Warning: The output network does not contain blackboxes.\n" ); - pNtkResult = Abc_NtkLogicToNetlist( pNtk, 0 ); + pNtkResult = Abc_NtkToNetlist( pNtk, 0 ); } Abc_NtkDelete( pNtkBase ); if ( pNtkResult == NULL ) @@ -477,11 +475,15 @@ void Io_WriteHie( Abc_Ntk_t * pNtk, char * pBaseName, char * pFileName ) // write the resulting network if ( Io_ReadFileType(pFileName) == IO_FILE_BLIF ) + { + if ( !Abc_NtkHasSop(pNtkResult) && !Abc_NtkHasMapping(pNtkResult) ) + Abc_NtkToSop( pNtkResult, 0 ); Io_WriteBlif( pNtkResult, pFileName, 1 ); + } else if ( Io_ReadFileType(pFileName) == IO_FILE_VERILOG ) { - if ( Abc_NtkIsSopNetlist(pNtkResult) ) - Abc_NtkSopToAig( pNtkResult ); + if ( !Abc_NtkHasAig(pNtkResult) && !Abc_NtkHasMapping(pNtkResult) ) + Abc_NtkToAig( pNtkResult ); Io_WriteVerilog( pNtkResult, pFileName ); } else diff --git a/src/base/io/ioWriteBlif.c b/src/base/io/ioWriteBlif.c index e48d0be8..417fe2a3 100644 --- a/src/base/io/ioWriteBlif.c +++ b/src/base/io/ioWriteBlif.c @@ -32,9 +32,9 @@ static void Io_NtkWritePis( FILE * pFile, Abc_Ntk_t * pNtk, int fWriteLatches ); static void Io_NtkWritePos( FILE * pFile, Abc_Ntk_t * pNtk, int fWriteLatches ); static void Io_NtkWriteSubckt( FILE * pFile, Abc_Obj_t * pNode ); static void Io_NtkWriteAsserts( FILE * pFile, Abc_Ntk_t * pNtk ); -static void Io_NtkWriteNodeGate( FILE * pFile, Abc_Obj_t * pNode ); +static void Io_NtkWriteNodeGate( FILE * pFile, Abc_Obj_t * pNode, int Length ); static void Io_NtkWriteNodeFanins( FILE * pFile, Abc_Obj_t * pNode ); -static void Io_NtkWriteNode( FILE * pFile, Abc_Obj_t * pNode ); +static void Io_NtkWriteNode( FILE * pFile, Abc_Obj_t * pNode, int Length ); static void Io_NtkWriteLatch( FILE * pFile, Abc_Obj_t * pLatch ); //////////////////////////////////////////////////////////////////////// @@ -56,7 +56,7 @@ void Io_WriteBlifLogic( Abc_Ntk_t * pNtk, char * FileName, int fWriteLatches ) { Abc_Ntk_t * pNtkTemp; // derive the netlist - pNtkTemp = Abc_NtkLogicToNetlist(pNtk,0); + pNtkTemp = Abc_NtkToNetlist(pNtk,0); if ( pNtkTemp == NULL ) { fprintf( stdout, "Writing BLIF has failed.\n" ); @@ -97,13 +97,22 @@ void Io_WriteBlif( Abc_Ntk_t * pNtk, char * FileName, int fWriteLatches ) if ( Abc_NtkBlackboxNum(pNtk) > 0 ) { Abc_Ntk_t * pNtkTemp; - Abc_Obj_t * pObj; int i; +/* + Abc_Obj_t * pObj; Abc_NtkForEachBlackbox( pNtk, pObj, i ) { pNtkTemp = pObj->pData; assert( pNtkTemp != NULL && Abc_NtkHasBlackbox(pNtkTemp) ); - fprintf( pFile, "\n\n", Abc_NtkName(pNtk) ); + fprintf( pFile, "\n\n" ); + Io_NtkWrite( pFile, pNtkTemp, fWriteLatches ); + } +*/ + Vec_PtrForEachEntry( pNtk->pDesign->vModules, pNtkTemp, i ) + { + if ( pNtkTemp == pNtk ) + continue; + fprintf( pFile, "\n\n" ); Io_NtkWrite( pFile, pNtkTemp, fWriteLatches ); } } @@ -156,7 +165,7 @@ void Io_NtkWriteOne( FILE * pFile, Abc_Ntk_t * pNtk, int fWriteLatches ) { ProgressBar * pProgress; Abc_Obj_t * pNode, * pLatch; - int i; + int i, Length; // write the PIs fprintf( pFile, ".inputs" ); @@ -206,11 +215,12 @@ void Io_NtkWriteOne( FILE * pFile, Abc_Ntk_t * pNtk, int fWriteLatches ) } // write each internal node + Length = Abc_NtkHasMapping(pNtk)? Mio_LibraryReadGateNameMax(pNtk->pManFunc) : 0; pProgress = Extra_ProgressBarStart( stdout, Abc_NtkObjNumMax(pNtk) ); Abc_NtkForEachNode( pNtk, pNode, i ) { Extra_ProgressBarUpdate( pProgress, i, NULL ); - Io_NtkWriteNode( pFile, pNode ); + Io_NtkWriteNode( pFile, pNode, Length ); } Extra_ProgressBarStop( pProgress ); } @@ -454,13 +464,13 @@ void Io_NtkWriteLatch( FILE * pFile, Abc_Obj_t * pLatch ) SeeAlso [] ***********************************************************************/ -void Io_NtkWriteNode( FILE * pFile, Abc_Obj_t * pNode ) +void Io_NtkWriteNode( FILE * pFile, Abc_Obj_t * pNode, int Length ) { if ( Abc_NtkHasMapping(pNode->pNtk) ) { // write the .gate line fprintf( pFile, ".gate" ); - Io_NtkWriteNodeGate( pFile, pNode ); + Io_NtkWriteNodeGate( pFile, pNode, Length ); fprintf( pFile, "\n" ); } else @@ -485,17 +495,17 @@ void Io_NtkWriteNode( FILE * pFile, Abc_Obj_t * pNode ) SeeAlso [] ***********************************************************************/ -void Io_NtkWriteNodeGate( FILE * pFile, Abc_Obj_t * pNode ) +void Io_NtkWriteNodeGate( FILE * pFile, Abc_Obj_t * pNode, int Length ) { Mio_Gate_t * pGate = pNode->pData; Mio_Pin_t * pGatePin; int i; // write the node - fprintf( pFile, " %s ", Mio_GateReadName(pGate) ); + fprintf( pFile, " %-*s ", Length, Mio_GateReadName(pGate) ); for ( pGatePin = Mio_GateReadPins(pGate), i = 0; pGatePin; pGatePin = Mio_PinReadNext(pGatePin), i++ ) fprintf( pFile, "%s=%s ", Mio_PinReadName(pGatePin), Abc_ObjName( Abc_ObjFanin(pNode,i) ) ); assert ( i == Abc_ObjFaninNum(pNode) ); - fprintf( pFile, "%s=%s", Mio_GateReadOutName(pGate), Abc_ObjName(pNode) ); + fprintf( pFile, "%s=%s", Mio_GateReadOutName(pGate), Abc_ObjName( Abc_ObjFanout0(pNode) ) ); } /**Function************************************************************* diff --git a/src/base/io/ioWriteCnf.c b/src/base/io/ioWriteCnf.c index 88695668..e1b2d956 100644 --- a/src/base/io/ioWriteCnf.c +++ b/src/base/io/ioWriteCnf.c @@ -66,7 +66,7 @@ int Io_WriteCnf( Abc_Ntk_t * pNtk, char * pFileName, int fAllPrimes ) } // convert to logic BDD network if ( Abc_NtkIsLogic(pNtk) ) - Abc_NtkLogicToBdd( pNtk ); + Abc_NtkToBdd( pNtk ); // create solver with clauses pSat = Abc_NtkMiterSatCreate( pNtk, fAllPrimes ); if ( pSat == NULL ) diff --git a/src/base/io/ioWriteVerilog.c b/src/base/io/ioWriteVerilog.c index 9524bdef..bf5182fb 100644 --- a/src/base/io/ioWriteVerilog.c +++ b/src/base/io/ioWriteVerilog.c @@ -34,7 +34,7 @@ static void Io_WriteVerilogRegs( FILE * pFile, Abc_Ntk_t * pNtk, int Start ); static void Io_WriteVerilogLatches( FILE * pFile, Abc_Ntk_t * pNtk ); static void Io_WriteVerilogObjects( FILE * pFile, Abc_Ntk_t * pNtk ); static int Io_WriteVerilogWiresCount( Abc_Ntk_t * pNtk ); -static char * Io_WriteVerilogGetName( Abc_Obj_t * pObj ); +static char * Io_WriteVerilogGetName( char * pName ); //////////////////////////////////////////////////////////////////////// /// FUNCTION DEFINITIONS /// @@ -57,9 +57,9 @@ void Io_WriteVerilog( Abc_Ntk_t * pNtk, char * pFileName ) FILE * pFile; int i; // can only write nodes represented using local AIGs - if ( !Abc_NtkIsAigNetlist(pNtk) ) + if ( !Abc_NtkIsAigNetlist(pNtk) && !Abc_NtkIsMappedNetlist(pNtk) ) { - printf( "Io_WriteVerilog(): Can produce Verilog for AIG netlists only.\n" ); + printf( "Io_WriteVerilog(): Can produce Verilog for mapped or AIG netlists only.\n" ); return; } // start the output stream @@ -77,16 +77,17 @@ void Io_WriteVerilog( Abc_Ntk_t * pNtk, char * pFileName ) // write modules if ( pNtk->pDesign ) { + // write the network first + Io_WriteVerilogInt( pFile, pNtk ); + // write other things Vec_PtrForEachEntry( pNtk->pDesign->vModules, pNetlist, i ) { assert( Abc_NtkIsNetlist(pNetlist) ); if ( pNetlist == pNtk ) continue; - Io_WriteVerilogInt( pFile, pNetlist ); fprintf( pFile, "\n" ); + Io_WriteVerilogInt( pFile, pNetlist ); } - // write the network last - Io_WriteVerilogInt( pFile, pNtk ); } else { @@ -185,7 +186,7 @@ void Io_WriteVerilogPis( FILE * pFile, Abc_Ntk_t * pNtk, int Start ) { pNet = Abc_ObjFanout0(pTerm); // get the line length after this name is written - AddedLength = strlen(Io_WriteVerilogGetName(pNet)) + 2; + AddedLength = strlen(Io_WriteVerilogGetName(Abc_ObjName(pNet))) + 2; if ( NameCounter && LineLength + AddedLength + 3 > IO_WRITE_LINE_LENGTH ) { // write the line extender fprintf( pFile, "\n " ); @@ -193,7 +194,7 @@ void Io_WriteVerilogPis( FILE * pFile, Abc_Ntk_t * pNtk, int Start ) LineLength = 3; NameCounter = 0; } - fprintf( pFile, " %s%s", Io_WriteVerilogGetName(pNet), (i==Abc_NtkPiNum(pNtk)-1)? "" : "," ); + fprintf( pFile, " %s%s", Io_WriteVerilogGetName(Abc_ObjName(pNet)), (i==Abc_NtkPiNum(pNtk)-1)? "" : "," ); LineLength += AddedLength; NameCounter++; } @@ -224,7 +225,7 @@ void Io_WriteVerilogPos( FILE * pFile, Abc_Ntk_t * pNtk, int Start ) { pNet = Abc_ObjFanin0(pTerm); // get the line length after this name is written - AddedLength = strlen(Io_WriteVerilogGetName(pNet)) + 2; + AddedLength = strlen(Io_WriteVerilogGetName(Abc_ObjName(pNet))) + 2; if ( NameCounter && LineLength + AddedLength + 3 > IO_WRITE_LINE_LENGTH ) { // write the line extender fprintf( pFile, "\n " ); @@ -232,7 +233,7 @@ void Io_WriteVerilogPos( FILE * pFile, Abc_Ntk_t * pNtk, int Start ) LineLength = 3; NameCounter = 0; } - fprintf( pFile, " %s%s", Io_WriteVerilogGetName(pNet), (i==Abc_NtkPoNum(pNtk)-1)? "" : "," ); + fprintf( pFile, " %s%s", Io_WriteVerilogGetName(Abc_ObjName(pNet)), (i==Abc_NtkPoNum(pNtk)-1)? "" : "," ); LineLength += AddedLength; NameCounter++; } @@ -273,7 +274,7 @@ void Io_WriteVerilogWires( FILE * pFile, Abc_Ntk_t * pNtk, int Start ) continue; Counter++; // get the line length after this name is written - AddedLength = strlen(Io_WriteVerilogGetName(pNet)) + 2; + AddedLength = strlen(Io_WriteVerilogGetName(Abc_ObjName(pNet))) + 2; if ( NameCounter && LineLength + AddedLength + 3 > IO_WRITE_LINE_LENGTH ) { // write the line extender fprintf( pFile, "\n " ); @@ -281,7 +282,7 @@ void Io_WriteVerilogWires( FILE * pFile, Abc_Ntk_t * pNtk, int Start ) LineLength = 3; NameCounter = 0; } - fprintf( pFile, " %s%s", Io_WriteVerilogGetName(pNet), (Counter==nNodes)? "" : "," ); + fprintf( pFile, " %s%s", Io_WriteVerilogGetName(Abc_ObjName(pNet)), (Counter==nNodes)? "" : "," ); LineLength += AddedLength; NameCounter++; } @@ -290,7 +291,7 @@ void Io_WriteVerilogWires( FILE * pFile, Abc_Ntk_t * pNtk, int Start ) pNet = Abc_ObjFanin0(Abc_ObjFanin0(pObj)); Counter++; // get the line length after this name is written - AddedLength = strlen(Io_WriteVerilogGetName(pNet)) + 2; + AddedLength = strlen(Io_WriteVerilogGetName(Abc_ObjName(pNet))) + 2; if ( NameCounter && LineLength + AddedLength + 3 > IO_WRITE_LINE_LENGTH ) { // write the line extender fprintf( pFile, "\n " ); @@ -298,7 +299,7 @@ void Io_WriteVerilogWires( FILE * pFile, Abc_Ntk_t * pNtk, int Start ) LineLength = 3; NameCounter = 0; } - fprintf( pFile, " %s%s", Io_WriteVerilogGetName(pNet), (Counter==nNodes)? "" : "," ); + fprintf( pFile, " %s%s", Io_WriteVerilogGetName(Abc_ObjName(pNet)), (Counter==nNodes)? "" : "," ); LineLength += AddedLength; NameCounter++; } @@ -311,7 +312,7 @@ void Io_WriteVerilogWires( FILE * pFile, Abc_Ntk_t * pNtk, int Start ) pNet = Abc_ObjFanin0(pTerm); Counter++; // get the line length after this name is written - AddedLength = strlen(Io_WriteVerilogGetName(pNet)) + 2; + AddedLength = strlen(Io_WriteVerilogGetName(Abc_ObjName(pNet))) + 2; if ( NameCounter && LineLength + AddedLength + 3 > IO_WRITE_LINE_LENGTH ) { // write the line extender fprintf( pFile, "\n " ); @@ -319,7 +320,7 @@ void Io_WriteVerilogWires( FILE * pFile, Abc_Ntk_t * pNtk, int Start ) LineLength = 3; NameCounter = 0; } - fprintf( pFile, " %s%s", Io_WriteVerilogGetName(pNet), (Counter==nNodes)? "" : "," ); + fprintf( pFile, " %s%s", Io_WriteVerilogGetName(Abc_ObjName(pNet)), (Counter==nNodes)? "" : "," ); LineLength += AddedLength; NameCounter++; } @@ -330,7 +331,7 @@ void Io_WriteVerilogWires( FILE * pFile, Abc_Ntk_t * pNtk, int Start ) continue; Counter++; // get the line length after this name is written - AddedLength = strlen(Io_WriteVerilogGetName(pNet)) + 2; + AddedLength = strlen(Io_WriteVerilogGetName(Abc_ObjName(pNet))) + 2; if ( NameCounter && LineLength + AddedLength + 3 > IO_WRITE_LINE_LENGTH ) { // write the line extender fprintf( pFile, "\n " ); @@ -338,7 +339,7 @@ void Io_WriteVerilogWires( FILE * pFile, Abc_Ntk_t * pNtk, int Start ) LineLength = 3; NameCounter = 0; } - fprintf( pFile, " %s%s", Io_WriteVerilogGetName(pNet), (Counter==nNodes)? "" : "," ); + fprintf( pFile, " %s%s", Io_WriteVerilogGetName(Abc_ObjName(pNet)), (Counter==nNodes)? "" : "," ); LineLength += AddedLength; NameCounter++; } @@ -377,7 +378,7 @@ void Io_WriteVerilogRegs( FILE * pFile, Abc_Ntk_t * pNtk, int Start ) pNet = Abc_ObjFanout0(Abc_ObjFanout0(pLatch)); Counter++; // get the line length after this name is written - AddedLength = strlen(Io_WriteVerilogGetName(pNet)) + 2; + AddedLength = strlen(Io_WriteVerilogGetName(Abc_ObjName(pNet))) + 2; if ( NameCounter && LineLength + AddedLength + 3 > IO_WRITE_LINE_LENGTH ) { // write the line extender fprintf( pFile, "\n " ); @@ -385,7 +386,7 @@ void Io_WriteVerilogRegs( FILE * pFile, Abc_Ntk_t * pNtk, int Start ) LineLength = 3; NameCounter = 0; } - fprintf( pFile, " %s%s", Io_WriteVerilogGetName(pNet), (Counter==nNodes)? "" : "," ); + fprintf( pFile, " %s%s", Io_WriteVerilogGetName(Abc_ObjName(pNet)), (Counter==nNodes)? "" : "," ); LineLength += AddedLength; NameCounter++; } @@ -402,35 +403,6 @@ void Io_WriteVerilogRegs( FILE * pFile, Abc_Ntk_t * pNtk, int Start ) SeeAlso [] ***********************************************************************/ -void Io_WriteVerilogLatches2( FILE * pFile, Abc_Ntk_t * pNtk ) -{ - Abc_Obj_t * pLatch; - int i; - Abc_NtkForEachLatch( pNtk, pLatch, i ) - { -// fprintf( pFile, " always @(posedge gclk) begin %s", Abc_ObjName(Abc_ObjFanout0(pLatch)) ); - fprintf( pFile, " always begin %s", Io_WriteVerilogGetName(Abc_ObjFanout0(Abc_ObjFanout0(pLatch))) ); - fprintf( pFile, " = %s; end\n", Io_WriteVerilogGetName(Abc_ObjFanin0(Abc_ObjFanin0(pLatch))) ); - if ( Abc_LatchInit(pLatch) == ABC_INIT_ZERO ) -// fprintf( pFile, " initial begin %s = 1\'b0; end\n", Io_WriteVerilogGetName(Abc_ObjFanout0(pLatch)) ); - fprintf( pFile, " initial begin %s = 0; end\n", Io_WriteVerilogGetName(Abc_ObjFanout0(Abc_ObjFanout0(pLatch))) ); - else if ( Abc_LatchInit(pLatch) == ABC_INIT_ONE ) -// fprintf( pFile, " initial begin %s = 1\'b1; end\n", Io_WriteVerilogGetName(Abc_ObjFanout0(pLatch)) ); - fprintf( pFile, " initial begin %s = 1; end\n", Io_WriteVerilogGetName(Abc_ObjFanout0(Abc_ObjFanout0(pLatch))) ); - } -} - -/**Function************************************************************* - - Synopsis [Writes the latches.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ void Io_WriteVerilogLatches( FILE * pFile, Abc_Ntk_t * pNtk ) { Abc_Obj_t * pLatch; @@ -442,8 +414,8 @@ void Io_WriteVerilogLatches( FILE * pFile, Abc_Ntk_t * pNtk ) fprintf( pFile, " always begin\n" ); Abc_NtkForEachLatch( pNtk, pLatch, i ) { - fprintf( pFile, " %s", Io_WriteVerilogGetName(Abc_ObjFanout0(Abc_ObjFanout0(pLatch))) ); - fprintf( pFile, " <= %s;\n", Io_WriteVerilogGetName(Abc_ObjFanin0(Abc_ObjFanin0(pLatch))) ); + fprintf( pFile, " %s", Io_WriteVerilogGetName(Abc_ObjName(Abc_ObjFanout0(Abc_ObjFanout0(pLatch)))) ); + fprintf( pFile, " <= %s;\n", Io_WriteVerilogGetName(Abc_ObjName(Abc_ObjFanin0(Abc_ObjFanin0(pLatch)))) ); } fprintf( pFile, " end\n" ); // check if there are initial values @@ -453,13 +425,13 @@ void Io_WriteVerilogLatches( FILE * pFile, Abc_Ntk_t * pNtk ) if ( i == Abc_NtkLatchNum(pNtk) ) return; // write the initial values - fprintf( pFile, " initial begin\n", Io_WriteVerilogGetName(Abc_ObjFanout0(Abc_NtkPi(pNtk,0))) ); + fprintf( pFile, " initial begin\n", Io_WriteVerilogGetName(Abc_ObjName(Abc_ObjFanout0(Abc_NtkPi(pNtk,0)))) ); Abc_NtkForEachLatch( pNtk, pLatch, i ) { if ( Abc_LatchInit(pLatch) == ABC_INIT_ZERO ) - fprintf( pFile, " %s <= 1\'b0;\n", Io_WriteVerilogGetName(Abc_ObjFanout0(Abc_ObjFanout0(pLatch))) ); + fprintf( pFile, " %s <= 1\'b0;\n", Io_WriteVerilogGetName(Abc_ObjName(Abc_ObjFanout0(Abc_ObjFanout0(pLatch)))) ); else if ( Abc_LatchInit(pLatch) == ABC_INIT_ONE ) - fprintf( pFile, " %s <= 1\'b1;\n", Io_WriteVerilogGetName(Abc_ObjFanout0(Abc_ObjFanout0(pLatch))) ); + fprintf( pFile, " %s <= 1\'b1;\n", Io_WriteVerilogGetName(Abc_ObjName(Abc_ObjFanout0(Abc_ObjFanout0(pLatch)))) ); } fprintf( pFile, " end\n" ); } @@ -481,48 +453,73 @@ void Io_WriteVerilogObjects( FILE * pFile, Abc_Ntk_t * pNtk ) Abc_Ntk_t * pNtkBox; Abc_Obj_t * pObj, * pTerm, * pFanin; Hop_Obj_t * pFunc; - int i, k, Counter, nDigits; - - Counter = 1; - nDigits = Extra_Base10Log( Abc_NtkNodeNum(pNtk) ); + int i, k, Counter, nDigits, Length; // write boxes + nDigits = Extra_Base10Log( Abc_NtkBoxNum(pNtk)-Abc_NtkLatchNum(pNtk) ); + Counter = 0; Abc_NtkForEachBox( pNtk, pObj, i ) { if ( Abc_ObjIsLatch(pObj) ) continue; pNtkBox = pObj->pData; - fprintf( pFile, " %s g%0*d", pNtkBox->pName, nDigits, Counter++ ); + fprintf( pFile, " %s box%0*d", pNtkBox->pName, nDigits, Counter++ ); fprintf( pFile, "(" ); Abc_NtkForEachPi( pNtkBox, pTerm, k ) { - fprintf( pFile, ".%s ", Io_WriteVerilogGetName(Abc_ObjFanout0(pTerm)) ); - fprintf( pFile, "(%s), ", Io_WriteVerilogGetName(Abc_ObjFanin0(Abc_ObjFanin(pObj,k))) ); + fprintf( pFile, ".%s", Io_WriteVerilogGetName(Abc_ObjName(Abc_ObjFanout0(pTerm))) ); + fprintf( pFile, "(%s), ", Io_WriteVerilogGetName(Abc_ObjName(Abc_ObjFanin0(Abc_ObjFanin(pObj,k)))) ); } Abc_NtkForEachPo( pNtkBox, pTerm, k ) { - fprintf( pFile, ".%s ", Io_WriteVerilogGetName(Abc_ObjFanin0(pTerm)) ); - fprintf( pFile, "(%s)%s", Io_WriteVerilogGetName(Abc_ObjFanout0(Abc_ObjFanout(pObj,k))), k==Abc_NtkPoNum(pNtkBox)-1? "":", " ); + fprintf( pFile, ".%s", Io_WriteVerilogGetName(Abc_ObjName(Abc_ObjFanin0(pTerm))) ); + fprintf( pFile, "(%s)%s", Io_WriteVerilogGetName(Abc_ObjName(Abc_ObjFanout0(Abc_ObjFanout(pObj,k)))), k==Abc_NtkPoNum(pNtkBox)-1? "":", " ); } fprintf( pFile, ");\n" ); } // write nodes - vLevels = Vec_VecAlloc( 10 ); - Abc_NtkForEachNode( pNtk, pObj, i ) + if ( Abc_NtkHasMapping(pNtk) ) { - pFunc = pObj->pData; - fprintf( pFile, " assign %s = ", Io_WriteVerilogGetName(Abc_ObjFanout0(pObj)) ); - // set the input names - Abc_ObjForEachFanin( pObj, pFanin, k ) - Hop_IthVar(pNtk->pManFunc, k)->pData = Extra_UtilStrsav(Io_WriteVerilogGetName(pFanin)); - // write the formula - Hop_ObjPrintVerilog( pFile, pFunc, vLevels, 0 ); - fprintf( pFile, ";\n" ); - // clear the input names - Abc_ObjForEachFanin( pObj, pFanin, k ) - free( Hop_IthVar(pNtk->pManFunc, k)->pData ); + Length = Mio_LibraryReadGateNameMax(pNtk->pManFunc); + nDigits = Extra_Base10Log( Abc_NtkNodeNum(pNtk) ); + Counter = 0; + Abc_NtkForEachNode( pNtk, pObj, k ) + { + Mio_Gate_t * pGate = pObj->pData; + Mio_Pin_t * pGatePin; + // write the node + fprintf( pFile, " %-*s g%0*d", Length, Mio_GateReadName(pGate), nDigits, Counter++ ); + fprintf( pFile, "(" ); + for ( pGatePin = Mio_GateReadPins(pGate), i = 0; pGatePin; pGatePin = Mio_PinReadNext(pGatePin), i++ ) + { + fprintf( pFile, ".%s", Io_WriteVerilogGetName(Mio_PinReadName(pGatePin)) ); + fprintf( pFile, "(%s), ", Io_WriteVerilogGetName(Abc_ObjName( Abc_ObjFanin(pObj,i) )) ); + } + assert ( i == Abc_ObjFaninNum(pObj) ); + fprintf( pFile, ".%s", Io_WriteVerilogGetName(Mio_GateReadOutName(pGate)) ); + fprintf( pFile, "(%s)", Io_WriteVerilogGetName(Abc_ObjName( Abc_ObjFanout0(pObj) )) ); + fprintf( pFile, ");\n" ); + } + } + else + { + vLevels = Vec_VecAlloc( 10 ); + Abc_NtkForEachNode( pNtk, pObj, i ) + { + pFunc = pObj->pData; + fprintf( pFile, " assign %s = ", Io_WriteVerilogGetName(Abc_ObjName(Abc_ObjFanout0(pObj))) ); + // set the input names + Abc_ObjForEachFanin( pObj, pFanin, k ) + Hop_IthVar(pNtk->pManFunc, k)->pData = Extra_UtilStrsav(Io_WriteVerilogGetName(Abc_ObjName(pFanin))); + // write the formula + Hop_ObjPrintVerilog( pFile, pFunc, vLevels, 0 ); + fprintf( pFile, ";\n" ); + // clear the input names + Abc_ObjForEachFanin( pObj, pFanin, k ) + free( Hop_IthVar(pNtk->pManFunc, k)->pData ); + } + Vec_VecFree( vLevels ); } - Vec_VecFree( vLevels ); } /**Function************************************************************* @@ -577,12 +574,10 @@ int Io_WriteVerilogWiresCount( Abc_Ntk_t * pNtk ) SeeAlso [] ***********************************************************************/ -char * Io_WriteVerilogGetName( Abc_Obj_t * pObj ) +char * Io_WriteVerilogGetName( char * pName ) { static char Buffer[500]; - char * pName; int Length, i; - pName = Abc_ObjName(pObj); Length = strlen(pName); // consider the case of a signal having name "0" or "1" if ( !(Length == 1 && (pName[0] == '0' || pName[0] == '1')) ) diff --git a/src/base/ver/ver.h b/src/base/ver/ver.h index 575ae7bb..0ba081db 100644 --- a/src/base/ver/ver.h +++ b/src/base/ver/ver.h @@ -45,18 +45,18 @@ typedef struct Ver_Stream_t_ Ver_Stream_t; struct Ver_Man_t_ { + // internal parameters + int fMapped; // mapped verilog + int fUseMemMan; // allocate memory manager in the networks + int fCheck; // checks network for currectness // input file stream char * pFileName; Ver_Stream_t * pReader; int fNameLast; ProgressBar * pProgress; - // current network and library - Abc_Ntk_t * pNtkCur; // the network under construction - Abc_Lib_t * pDesign; // the current design - // parameters - int fUseMemMan; // allocate memory manager in the networks - int fCheck; // checks network for currectness - // error recovery + // current design + Abc_Lib_t * pDesign; + // error handling FILE * Output; int fTopLevel; int fError; diff --git a/src/base/ver/verCore.c b/src/base/ver/verCore.c index a8ac99e5..6c036288 100644 --- a/src/base/ver/verCore.c +++ b/src/base/ver/verCore.c @@ -19,6 +19,8 @@ ***********************************************************************/ #include "ver.h" +#include "mio.h" +#include "main.h" //////////////////////////////////////////////////////////////////////// /// DECLARATIONS /// @@ -51,50 +53,29 @@ static void Ver_ParseStop( Ver_Man_t * p ); static void Ver_ParseFreeData( Ver_Man_t * p ); static void Ver_ParseInternal( Ver_Man_t * p ); static int Ver_ParseModule( Ver_Man_t * p ); -static int Ver_ParseSignal( Ver_Man_t * p, Ver_SignalType_t SigType ); -static int Ver_ParseAssign( Ver_Man_t * p ); -static int Ver_ParseAlways( Ver_Man_t * p ); -static int Ver_ParseInitial( Ver_Man_t * p ); -static int Ver_ParseGate( Ver_Man_t * p, Abc_Ntk_t * pNtkGate ); -static int Ver_ParseGateStandard( Ver_Man_t * pMan, Ver_GateType_t GateType ); +static int Ver_ParseSignal( Ver_Man_t * p, Abc_Ntk_t * pNtk, Ver_SignalType_t SigType ); +static int Ver_ParseAlways( Ver_Man_t * p, Abc_Ntk_t * pNtk ); +static int Ver_ParseInitial( Ver_Man_t * p, Abc_Ntk_t * pNtk ); +static int Ver_ParseAssign( Ver_Man_t * p, Abc_Ntk_t * pNtk ); +static int Ver_ParseGateStandard( Ver_Man_t * pMan, Abc_Ntk_t * pNtk, Ver_GateType_t GateType ); +static int Ver_ParseGate( Ver_Man_t * p, Abc_Ntk_t * pNtk, Mio_Gate_t * pGate ); +static int Ver_ParseBox( Ver_Man_t * pMan, Abc_Ntk_t * pNtk, Abc_Ntk_t * pNtkBox ); +static int Ver_ParseConnectBox( Ver_Man_t * pMan, Abc_Obj_t * pBox ); +static int Vec_ParseAttachBoxes( Ver_Man_t * pMan ); static Abc_Obj_t * Ver_ParseCreatePi( Abc_Ntk_t * pNtk, char * pName ); static Abc_Obj_t * Ver_ParseCreatePo( Abc_Ntk_t * pNtk, char * pName ); static Abc_Obj_t * Ver_ParseCreateLatch( Abc_Ntk_t * pNtk, Abc_Obj_t * pNetLI, Abc_Obj_t * pNetLO ); static Abc_Obj_t * Ver_ParseCreateInv( Abc_Ntk_t * pNtk, Abc_Obj_t * pNet ); +static inline int Ver_NtkIsDefined( Abc_Ntk_t * pNtkBox ) { assert( pNtkBox->pName ); return Abc_NtkPiNum(pNtkBox) || Abc_NtkPoNum(pNtkBox); } +static inline int Ver_ObjIsConnected( Abc_Obj_t * pObj ) { assert( Abc_ObjIsBox(pObj) ); return Abc_ObjFaninNum(pObj) || Abc_ObjFanoutNum(pObj); } + +int glo_fMapped = 0; // this is bad! + //////////////////////////////////////////////////////////////////////// /// FUNCTION DEFINITIONS /// //////////////////////////////////////////////////////////////////////// - -/**Function************************************************************* - - Synopsis [File parser.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -Abc_Lib_t * Ver_ParseFile( char * pFileName, Abc_Lib_t * pGateLib, int fCheck, int fUseMemMan ) -{ - Ver_Man_t * p; - Abc_Lib_t * pDesign; - // start the parser - p = Ver_ParseStart( pFileName, pGateLib ); - p->fCheck = fCheck; - p->fUseMemMan = fUseMemMan; - // parse the file - Ver_ParseInternal( p ); - // save the result - pDesign = p->pDesign; - p->pDesign = NULL; - // stop the parser - Ver_ParseStop( p ); - return pDesign; -} /**Function************************************************************* @@ -114,6 +95,8 @@ Ver_Man_t * Ver_ParseStart( char * pFileName, Abc_Lib_t * pGateLib ) memset( p, 0, sizeof(Ver_Man_t) ); p->pFileName = pFileName; p->pReader = Ver_StreamAlloc( pFileName ); + if ( p->pReader == NULL ) + return NULL; p->Output = stdout; p->pProgress = Extra_ProgressBarStart( stdout, Ver_StreamGetFileSize(p->pReader) ); p->vNames = Vec_PtrAlloc( 100 ); @@ -122,6 +105,7 @@ Ver_Man_t * Ver_ParseStart( char * pFileName, Abc_Lib_t * pGateLib ) // create the design library and assign the technology library p->pDesign = Abc_LibCreate( pFileName ); p->pDesign->pLibrary = pGateLib; + p->pDesign->pGenlib = Abc_FrameReadLibGen(); return p; } @@ -138,7 +122,6 @@ Ver_Man_t * Ver_ParseStart( char * pFileName, Abc_Lib_t * pGateLib ) ***********************************************************************/ void Ver_ParseStop( Ver_Man_t * p ) { - assert( p->pNtkCur == NULL ); Ver_StreamFree( p->pReader ); Extra_ProgressBarStop( p->pProgress ); Vec_PtrFree( p->vNames ); @@ -146,6 +129,41 @@ void Ver_ParseStop( Ver_Man_t * p ) Vec_IntFree( p->vStackOp ); free( p ); } + +/**Function************************************************************* + + Synopsis [File parser.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Abc_Lib_t * Ver_ParseFile( char * pFileName, Abc_Lib_t * pGateLib, int fCheck, int fUseMemMan ) +{ + Ver_Man_t * p; + Abc_Lib_t * pDesign; + // start the parser + p = Ver_ParseStart( pFileName, pGateLib ); + p->fMapped = glo_fMapped; + p->fCheck = fCheck; + p->fUseMemMan = fUseMemMan; + if ( glo_fMapped ) + { + Hop_ManStop(p->pDesign->pManFunc); + p->pDesign->pManFunc = NULL; + } + // parse the file + Ver_ParseInternal( p ); + // save the result + pDesign = p->pDesign; + p->pDesign = NULL; + // stop the parser + Ver_ParseStop( p ); + return pDesign; +} /**Function************************************************************* @@ -160,7 +178,11 @@ void Ver_ParseStop( Ver_Man_t * p ) ***********************************************************************/ void Ver_ParseInternal( Ver_Man_t * pMan ) { + Abc_Ntk_t * pNtk; char * pToken; + int i; + + // preparse the modeles while ( 1 ) { // get the next token @@ -173,30 +195,28 @@ void Ver_ParseInternal( Ver_Man_t * pMan ) Ver_ParsePrintErrorMessage( pMan ); return; } - // parse the module - if ( !Ver_ParseModule( pMan ) ) + if ( !Ver_ParseModule(pMan) ) return; + } + + // process defined and undefined boxes + if ( !Vec_ParseAttachBoxes( pMan ) ) + return; + // connect the boxes and check + Vec_PtrForEachEntry( pMan->pDesign->vModules, pNtk, i ) + { + // fix the dangling nets + Abc_NtkFinalizeRead( pNtk ); // check the network for correctness - if ( pMan->fCheck && !Abc_NtkCheckRead( pMan->pNtkCur ) ) - { - pMan->fTopLevel = 1; - sprintf( pMan->sError, "The network check has failed.", pMan->pNtkCur->pName ); - Ver_ParsePrintErrorMessage( pMan ); - return; - } - // add the module to the hash table - if ( st_is_member( pMan->pDesign->tModules, pMan->pNtkCur->pName ) ) + if ( pMan->fCheck && !Abc_NtkCheckRead( pNtk ) ) { pMan->fTopLevel = 1; - sprintf( pMan->sError, "Module \"%s\" is defined more than once.", pMan->pNtkCur->pName ); + sprintf( pMan->sError, "The network check has failed.", pNtk->pName ); Ver_ParsePrintErrorMessage( pMan ); return; } - Vec_PtrPush( pMan->pDesign->vModules, pMan->pNtkCur ); - st_insert( pMan->pDesign->tModules, pMan->pNtkCur->pName, (char *)pMan->pNtkCur ); - pMan->pNtkCur = NULL; } } @@ -213,12 +233,6 @@ void Ver_ParseInternal( Ver_Man_t * pMan ) ***********************************************************************/ void Ver_ParseFreeData( Ver_Man_t * p ) { - if ( p->pNtkCur ) - { - p->pNtkCur->pManFunc = NULL; - Abc_NtkDelete( p->pNtkCur ); - p->pNtkCur = NULL; - } if ( p->pDesign ) { Abc_LibFree( p->pDesign, NULL ); @@ -249,7 +263,105 @@ void Ver_ParsePrintErrorMessage( Ver_Man_t * p ) Ver_ParseFreeData( p ); } +/**Function************************************************************* + + Synopsis [Finds the network by name or create a new blackbox network.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Abc_Ntk_t * Ver_ParseFindOrCreateNetwork( Ver_Man_t * pMan, char * pName ) +{ + Abc_Ntk_t * pNtkNew; + // check if the network exists + if ( pNtkNew = Abc_LibFindModelByName( pMan->pDesign, pName ) ) + return pNtkNew; +//printf( "Creating network %s.\n", pName ); + // create new network + pNtkNew = Abc_NtkAlloc( ABC_NTK_NETLIST, ABC_FUNC_BLACKBOX, pMan->fUseMemMan ); + pNtkNew->pName = Extra_UtilStrsav( pName ); + pNtkNew->pSpec = NULL; + // add module to the design + Abc_LibAddModel( pMan->pDesign, pNtkNew ); + return pNtkNew; +} + +/**Function************************************************************* + + Synopsis [Finds the network by name or create a new blackbox network.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Abc_Obj_t * Ver_ParseFindNet( Abc_Ntk_t * pNtk, char * pName ) +{ + Abc_Obj_t * pObj; + if ( pObj = Abc_NtkFindNet(pNtk, pName) ) + return pObj; + if ( !strcmp( pName, "1\'b0" ) ) + return Abc_NtkFindOrCreateNet( pNtk, "1\'b0" ); + if ( !strcmp( pName, "1\'b1" ) ) + return Abc_NtkFindOrCreateNet( pNtk, "1\'b1" ); + return NULL; +} + +/**Function************************************************************* + + Synopsis [Converts the network from the blackbox type into a different one.] + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Ver_ParseConvertNetwork( Ver_Man_t * pMan, Abc_Ntk_t * pNtk, int fMapped ) +{ + if ( fMapped ) + { + // convert from the blackbox into the network with local functions representated by AIGs + if ( pNtk->ntkFunc == ABC_FUNC_BLACKBOX ) + { + // change network type + assert( pNtk->pManFunc == NULL ); + pNtk->ntkFunc = ABC_FUNC_MAP; + pNtk->pManFunc = pMan->pDesign->pGenlib; + } + else if ( pNtk->ntkFunc != ABC_FUNC_MAP ) + { + sprintf( pMan->sError, "The network %s appears to have both gates and assign statements. Currently such network are not allowed. One way to fix this problem might be to replace assigns by buffers from the library.", pNtk->pName ); + Ver_ParsePrintErrorMessage( pMan ); + return 0; + } + } + else + { + // convert from the blackbox into the network with local functions representated by AIGs + if ( pNtk->ntkFunc == ABC_FUNC_BLACKBOX ) + { + // change network type + assert( pNtk->pManFunc == NULL ); + pNtk->ntkFunc = ABC_FUNC_AIG; + pNtk->pManFunc = pMan->pDesign->pManFunc; + } + else if ( pNtk->ntkFunc != ABC_FUNC_AIG ) + { + sprintf( pMan->sError, "The network %s appears to have both gates and assign statements. Currently such network are not allowed. One way to fix this problem might be to replace assigns by buffers from the library.", pNtk->pName ); + Ver_ParsePrintErrorMessage( pMan ); + return 0; + } + } + return 1; +} /**Function************************************************************* @@ -264,26 +376,17 @@ void Ver_ParsePrintErrorMessage( Ver_Man_t * p ) ***********************************************************************/ int Ver_ParseModule( Ver_Man_t * pMan ) { + Mio_Gate_t * pGate; Ver_Stream_t * p = pMan->pReader; Abc_Ntk_t * pNtk, * pNtkTemp; - Abc_Obj_t * pNet; char * pWord, Symbol; int RetValue; - // start the current network - assert( pMan->pNtkCur == NULL ); - pNtk = pMan->pNtkCur = Abc_NtkAlloc( ABC_NTK_NETLIST, ABC_FUNC_BLACKBOX, pMan->fUseMemMan ); - pNtk->ntkFunc = ABC_FUNC_AIG; - pNtk->pManFunc = pMan->pDesign->pManFunc; - // get the network name pWord = Ver_ParseGetName( pMan ); - pNtk->pName = Extra_UtilStrsav( pWord ); - pNtk->pSpec = NULL; - // create constant nets - Abc_NtkFindOrCreateNet( pNtk, "1\'b0" ); - Abc_NtkFindOrCreateNet( pNtk, "1\'b1" ); + // get the network with this name + pNtk = Ver_ParseFindOrCreateNetwork( pMan, pWord ); // make sure we stopped at the opening paranthesis if ( Ver_StreamPopChar(p) != '(' ) @@ -313,15 +416,15 @@ int Ver_ParseModule( Ver_Man_t * pMan ) if ( pWord == NULL ) return 0; if ( !strcmp( pWord, "input" ) ) - RetValue = Ver_ParseSignal( pMan, VER_SIG_INPUT ); + RetValue = Ver_ParseSignal( pMan, pNtk, VER_SIG_INPUT ); else if ( !strcmp( pWord, "output" ) ) - RetValue = Ver_ParseSignal( pMan, VER_SIG_OUTPUT ); + RetValue = Ver_ParseSignal( pMan, pNtk, VER_SIG_OUTPUT ); else if ( !strcmp( pWord, "reg" ) ) - RetValue = Ver_ParseSignal( pMan, VER_SIG_REG ); + RetValue = Ver_ParseSignal( pMan, pNtk, VER_SIG_REG ); else if ( !strcmp( pWord, "wire" ) ) - RetValue = Ver_ParseSignal( pMan, VER_SIG_WIRE ); + RetValue = Ver_ParseSignal( pMan, pNtk, VER_SIG_WIRE ); else if ( !strcmp( pWord, "inout" ) ) - RetValue = Ver_ParseSignal( pMan, VER_SIG_INOUT ); + RetValue = Ver_ParseSignal( pMan, pNtk, VER_SIG_INOUT ); else break; if ( RetValue == 0 ) @@ -334,43 +437,38 @@ int Ver_ParseModule( Ver_Man_t * pMan ) Extra_ProgressBarUpdate( pMan->pProgress, Ver_StreamGetCurPosition(p), NULL ); if ( !strcmp( pWord, "and" ) ) - RetValue = Ver_ParseGateStandard( pMan, VER_GATE_AND ); + RetValue = Ver_ParseGateStandard( pMan, pNtk, VER_GATE_AND ); else if ( !strcmp( pWord, "or" ) ) - RetValue = Ver_ParseGateStandard( pMan, VER_GATE_OR ); + RetValue = Ver_ParseGateStandard( pMan, pNtk, VER_GATE_OR ); else if ( !strcmp( pWord, "xor" ) ) - RetValue = Ver_ParseGateStandard( pMan, VER_GATE_XOR ); + RetValue = Ver_ParseGateStandard( pMan, pNtk, VER_GATE_XOR ); else if ( !strcmp( pWord, "buf" ) ) - RetValue = Ver_ParseGateStandard( pMan, VER_GATE_BUF ); + RetValue = Ver_ParseGateStandard( pMan, pNtk, VER_GATE_BUF ); else if ( !strcmp( pWord, "nand" ) ) - RetValue = Ver_ParseGateStandard( pMan, VER_GATE_NAND ); + RetValue = Ver_ParseGateStandard( pMan, pNtk, VER_GATE_NAND ); else if ( !strcmp( pWord, "nor" ) ) - RetValue = Ver_ParseGateStandard( pMan, VER_GATE_NOR ); + RetValue = Ver_ParseGateStandard( pMan, pNtk, VER_GATE_NOR ); else if ( !strcmp( pWord, "xnor" ) ) - RetValue = Ver_ParseGateStandard( pMan, VER_GATE_XNOR ); + RetValue = Ver_ParseGateStandard( pMan, pNtk, VER_GATE_XNOR ); else if ( !strcmp( pWord, "not" ) ) - RetValue = Ver_ParseGateStandard( pMan, VER_GATE_NOT ); + RetValue = Ver_ParseGateStandard( pMan, pNtk, VER_GATE_NOT ); else if ( !strcmp( pWord, "assign" ) ) - RetValue = Ver_ParseAssign( pMan ); + RetValue = Ver_ParseAssign( pMan, pNtk ); else if ( !strcmp( pWord, "always" ) ) - RetValue = Ver_ParseAlways( pMan ); + RetValue = Ver_ParseAlways( pMan, pNtk ); else if ( !strcmp( pWord, "initial" ) ) - RetValue = Ver_ParseInitial( pMan ); + RetValue = Ver_ParseInitial( pMan, pNtk ); else if ( !strcmp( pWord, "endmodule" ) ) break; - else if ( pMan->pDesign->pLibrary && st_lookup(pMan->pDesign->pLibrary->tModules, pWord, (char**)&pNtkTemp) ) // gate library - RetValue = Ver_ParseGate( pMan, pNtkTemp ); - else if ( pMan->pDesign && st_lookup(pMan->pDesign->tModules, pWord, (char**)&pNtkTemp) ) // current design - RetValue = Ver_ParseGate( pMan, pNtkTemp ); - else + else if ( pMan->pDesign->pGenlib && (pGate = Mio_LibraryReadGateByName(pMan->pDesign->pGenlib, pWord)) ) // current design + RetValue = Ver_ParseGate( pMan, pNtk, pGate ); +// else if ( pMan->pDesign->pLibrary && st_lookup(pMan->pDesign->pLibrary->tModules, pWord, (char**)&pNtkTemp) ) // gate library +// RetValue = Ver_ParseGate( pMan, pNtkTemp ); + else // assume this is the box used in the current design { - printf( "Cannot find \"%s\".\n", pWord ); - Ver_StreamSkipToChars( p, ";" ); - Ver_StreamPopChar(p); - -// sprintf( pMan->sError, "Cannot find \"%s\" in the library.", pWord ); -// Ver_ParsePrintErrorMessage( pMan ); -// return 0; + pNtkTemp = Ver_ParseFindOrCreateNetwork( pMan, pWord ); + RetValue = Ver_ParseBox( pMan, pNtk, pNtkTemp ); } if ( RetValue == 0 ) return 0; @@ -383,28 +481,33 @@ int Ver_ParseModule( Ver_Man_t * pMan ) return 0; } - // check if constant 0 net is used - pNet = Abc_NtkFindOrCreateNet( pNtk, "1\'b0" ); - if ( Abc_ObjFanoutNum(pNet) == 0 ) - Abc_NtkDeleteObj(pNet); - else - Abc_ObjAddFanin( pNet, Abc_NtkCreateNodeConst0(pNtk) ); - // check if constant 1 net is used - pNet = Abc_NtkFindOrCreateNet( pNtk, "1\'b1" ); - if ( Abc_ObjFanoutNum(pNet) == 0 ) - Abc_NtkDeleteObj(pNet); - else - Abc_ObjAddFanin( pNet, Abc_NtkCreateNodeConst1(pNtk) ); - - // check the functionality to blackbox if insides are not defined - if ( Abc_NtkNodeNum(pNtk) == 0 && Abc_NtkBoxNum(pNtk) == 0 ) + // convert from the blackbox into the network with local functions representated by AIGs + if ( pNtk->ntkFunc == ABC_FUNC_BLACKBOX ) { - pNtk->ntkFunc = ABC_FUNC_BLACKBOX; - pNtk->pManFunc = NULL; + if ( Abc_NtkNodeNum(pNtk) > 0 || Abc_NtkBoxNum(pNtk) > 0 ) + { + if ( !Ver_ParseConvertNetwork( pMan, pNtk, pMan->fMapped ) ) + return 0; + } + else + { + Abc_Obj_t * pObj, * pBox, * pTerm; + int i; + pBox = Abc_NtkCreateBlackbox(pNtk); + Abc_NtkForEachPi( pNtk, pObj, i ) + { + pTerm = Abc_NtkCreateBi(pNtk); + Abc_ObjAddFanin( pTerm, Abc_ObjFanout0(pObj) ); + Abc_ObjAddFanin( pBox, pTerm ); + } + Abc_NtkForEachPo( pNtk, pObj, i ) + { + pTerm = Abc_NtkCreateBo(pNtk); + Abc_ObjAddFanin( pTerm, pBox ); + Abc_ObjAddFanin( Abc_ObjFanin0(pObj), pTerm ); + } + } } - - // fix the dangling nets - Abc_NtkFinalizeRead( pNtk ); return 1; } @@ -419,19 +522,21 @@ int Ver_ParseModule( Ver_Man_t * pMan ) SeeAlso [] ***********************************************************************/ -int Ver_ParseSignal( Ver_Man_t * pMan, Ver_SignalType_t SigType ) +int Ver_ParseSignal( Ver_Man_t * pMan, Abc_Ntk_t * pNtk, Ver_SignalType_t SigType ) { Ver_Stream_t * p = pMan->pReader; - Abc_Ntk_t * pNtk = pMan->pNtkCur; char Buffer[1000]; int Lower, Upper, i; char * pWord; char Symbol; + Lower = Upper = 0; while ( 1 ) { pWord = Ver_ParseGetName( pMan ); if ( pWord == NULL ) return 0; + + // check if the range is specified if ( pWord[0] == '[' && !pMan->fNameLast ) { Lower = atoi( pWord + 1 ); @@ -472,6 +577,20 @@ int Ver_ParseSignal( Ver_Man_t * pMan, Ver_SignalType_t SigType ) if ( pWord == NULL ) return 0; } + } + + // create signals + if ( Lower == 0 && Upper == 0 ) + { + if ( SigType == VER_SIG_INPUT || SigType == VER_SIG_INOUT ) + Ver_ParseCreatePi( pNtk, pWord ); + if ( SigType == VER_SIG_OUTPUT || SigType == VER_SIG_INOUT ) + Ver_ParseCreatePo( pNtk, pWord ); + if ( SigType == VER_SIG_WIRE || SigType == VER_SIG_REG ) + Abc_NtkFindOrCreateNet( pNtk, pWord ); + } + else + { for ( i = Lower; i <= Upper; i++ ) { sprintf( Buffer, "%s[%d]", pWord, i ); @@ -483,15 +602,7 @@ int Ver_ParseSignal( Ver_Man_t * pMan, Ver_SignalType_t SigType ) Abc_NtkFindOrCreateNet( pNtk, Buffer ); } } - else - { - if ( SigType == VER_SIG_INPUT || SigType == VER_SIG_INOUT ) - Ver_ParseCreatePi( pNtk, pWord ); - if ( SigType == VER_SIG_OUTPUT || SigType == VER_SIG_INOUT ) - Ver_ParseCreatePo( pNtk, pWord ); - if ( SigType == VER_SIG_WIRE || SigType == VER_SIG_REG ) - Abc_NtkFindOrCreateNet( pNtk, pWord ); - } + Symbol = Ver_StreamPopChar(p); if ( Symbol == ',' ) continue; @@ -515,137 +626,9 @@ int Ver_ParseSignal( Ver_Man_t * pMan, Ver_SignalType_t SigType ) SeeAlso [] ***********************************************************************/ -int Ver_ParseAssign( Ver_Man_t * pMan ) -{ - Ver_Stream_t * p = pMan->pReader; - Abc_Ntk_t * pNtk = pMan->pNtkCur; - Abc_Obj_t * pNode, * pNet; - char * pWord, * pName, * pEquation; - Hop_Obj_t * pFunc; - char Symbol; - int i, Length, fReduction; - -// if ( Ver_StreamGetLineNumber(p) == 2756 ) -// { -// int x = 0; -// } - - // convert from the mapped netlist into the BDD netlist - if ( pNtk->ntkFunc == ABC_FUNC_BLACKBOX ) - { - pNtk->ntkFunc = ABC_FUNC_AIG; - assert( pNtk->pManFunc == NULL ); - pNtk->pManFunc = pMan->pDesign->pManFunc; - } - else if ( pNtk->ntkFunc != ABC_FUNC_AIG ) - { - sprintf( pMan->sError, "The network %s appears to mapped gates and assign statements. Currently such network are not allowed. One way to fix this problem is to replace assigns by buffers from the library.", pMan->pNtkCur ); - Ver_ParsePrintErrorMessage( pMan ); - return 0; - } - - while ( 1 ) - { - // get the name of the output signal - pWord = Ver_ParseGetName( pMan ); - if ( pWord == NULL ) - return 0; - // consider the case of reduction operations - fReduction = 0; - if ( pWord[0] == '{' && !pMan->fNameLast ) - fReduction = 1; - if ( fReduction ) - { - pWord++; - pWord[strlen(pWord)-1] = 0; - assert( pWord[0] != '\\' ); - } - // get the fanout net - pNet = Abc_NtkFindNet( pNtk, pWord ); - if ( pNet == NULL ) - { - sprintf( pMan->sError, "Cannot read the assign statement for %s (output wire is not defined).", pWord ); - Ver_ParsePrintErrorMessage( pMan ); - return 0; - } - // get the equality sign - if ( Ver_StreamPopChar(p) != '=' ) - { - sprintf( pMan->sError, "Cannot read the assign statement for %s (expected equality sign).", pWord ); - Ver_ParsePrintErrorMessage( pMan ); - return 0; - } - // skip the comments - if ( !Ver_ParseSkipComments( pMan ) ) - return 0; - // get the second name - if ( fReduction ) - pEquation = Ver_StreamGetWord( p, ";" ); - else - pEquation = Ver_StreamGetWord( p, ",;" ); - if ( pEquation == NULL ) - { - sprintf( pMan->sError, "Cannot read the equation for %s.", Abc_ObjName(pNet) ); - Ver_ParsePrintErrorMessage( pMan ); - return 0; - } - - // parse the formula - if ( fReduction ) - pFunc = Ver_FormulaReduction( pEquation, pNtk->pManFunc, pMan->vNames, pMan->sError ); - else - pFunc = Ver_FormulaParser( pEquation, pNtk->pManFunc, pMan->vNames, pMan->vStackFn, pMan->vStackOp, pMan->sError ); - if ( pFunc == NULL ) - { - Ver_ParsePrintErrorMessage( pMan ); - return 0; - } - - // create the node with the given inputs - pNode = Abc_NtkCreateNode( pMan->pNtkCur ); - pNode->pData = pFunc; - Abc_ObjAddFanin( pNet, pNode ); - // connect to fanin nets - for ( i = 0; i < Vec_PtrSize(pMan->vNames)/2; i++ ) - { - // get the name of this signal - Length = (int)Vec_PtrEntry( pMan->vNames, 2*i ); - pName = Vec_PtrEntry( pMan->vNames, 2*i + 1 ); - pName[Length] = 0; - // find the corresponding net - pNet = Abc_NtkFindNet( pNtk, pName ); - if ( pNet == NULL ) - { - sprintf( pMan->sError, "Cannot read the assign statement for %s (input wire %d is not defined).", pWord, pName ); - Ver_ParsePrintErrorMessage( pMan ); - return 0; - } - Abc_ObjAddFanin( pNode, pNet ); - } - Symbol = Ver_StreamPopChar(p); - if ( Symbol == ',' ) - continue; - if ( Symbol == ';' ) - return 1; - } - return 1; -} - -/**Function************************************************************* - - Synopsis [Parses one directive.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -int Ver_ParseAlways( Ver_Man_t * pMan ) +int Ver_ParseAlways( Ver_Man_t * pMan, Abc_Ntk_t * pNtk ) { Ver_Stream_t * p = pMan->pReader; - Abc_Ntk_t * pNtk = pMan->pNtkCur; Abc_Obj_t * pNet, * pNet2; int fStopAfterOne; char * pWord, * pWord2; @@ -681,7 +664,7 @@ int Ver_ParseAlways( Ver_Man_t * pMan ) break; } // get the fanout net - pNet = Abc_NtkFindNet( pNtk, pWord ); + pNet = Ver_ParseFindNet( pNtk, pWord ); if ( pNet == NULL ) { sprintf( pMan->sError, "Cannot read the always statement for %s (output wire is not defined).", pWord ); @@ -708,11 +691,11 @@ int Ver_ParseAlways( Ver_Man_t * pMan ) // check if the name is complemented if ( pWord2[0] == '~' ) { - pNet2 = Abc_NtkFindNet( pNtk, pWord2+1 ); + pNet2 = Ver_ParseFindNet( pNtk, pWord2+1 ); pNet2 = Ver_ParseCreateInv( pNtk, pNet2 ); } else - pNet2 = Abc_NtkFindNet( pNtk, pWord2 ); + pNet2 = Ver_ParseFindNet( pNtk, pWord2 ); if ( pNet2 == NULL ) { sprintf( pMan->sError, "Cannot read the always statement for %s (input wire is not defined).", pWord2 ); @@ -742,10 +725,9 @@ int Ver_ParseAlways( Ver_Man_t * pMan ) SeeAlso [] ***********************************************************************/ -int Ver_ParseInitial( Ver_Man_t * pMan ) +int Ver_ParseInitial( Ver_Man_t * pMan, Abc_Ntk_t * pNtk ) { Ver_Stream_t * p = pMan->pReader; - Abc_Ntk_t * pNtk = pMan->pNtkCur; Abc_Obj_t * pNode, * pNet; int fStopAfterOne; char * pWord, * pEquation; @@ -772,7 +754,7 @@ int Ver_ParseInitial( Ver_Man_t * pMan ) break; } // get the fanout net - pNet = Abc_NtkFindNet( pNtk, pWord ); + pNet = Ver_ParseFindNet( pNtk, pWord ); if ( pNet == NULL ) { sprintf( pMan->sError, "Cannot read the initial statement for %s (output wire is not defined).", pWord ); @@ -839,40 +821,287 @@ int Ver_ParseInitial( Ver_Man_t * pMan ) SeeAlso [] ***********************************************************************/ -int Ver_ParseGate( Ver_Man_t * pMan, Abc_Ntk_t * pNtkGate ) +int Ver_ParseAssign( Ver_Man_t * pMan, Abc_Ntk_t * pNtk ) { Ver_Stream_t * p = pMan->pReader; - Abc_Ntk_t * pNtk = pMan->pNtkCur; - Abc_Obj_t * pNetFormal, * pNetActual; - Abc_Obj_t * pObj, * pNode, * pTerm; - char * pWord, Symbol, * pGateName; - int i, fCompl, fComplUsed = 0; - unsigned * pPolarity; - - // clean the PI/PO pointers - Abc_NtkForEachPi( pNtkGate, pObj, i ) - pObj->pCopy = NULL; - Abc_NtkForEachPo( pNtkGate, pObj, i ) - pObj->pCopy = NULL; + Abc_Obj_t * pNode, * pNet; + char * pWord, * pName, * pEquation; + Hop_Obj_t * pFunc; + char Symbol; + int i, Length, fReduction; + +// if ( Ver_StreamGetLineNumber(p) == 2756 ) +// { +// int x = 0; +// } + + // convert from the blackbox into the network with local functions representated by AIGs + if ( !Ver_ParseConvertNetwork( pMan, pNtk, pMan->fMapped ) ) + return 0; + + while ( 1 ) + { + // get the name of the output signal + pWord = Ver_ParseGetName( pMan ); + if ( pWord == NULL ) + return 0; + // consider the case of reduction operations + fReduction = 0; + if ( pWord[0] == '{' && !pMan->fNameLast ) + fReduction = 1; + if ( fReduction ) + { + pWord++; + pWord[strlen(pWord)-1] = 0; + assert( pWord[0] != '\\' ); + } + // get the fanout net + pNet = Ver_ParseFindNet( pNtk, pWord ); + if ( pNet == NULL ) + { + sprintf( pMan->sError, "Cannot read the assign statement for %s (output wire is not defined).", pWord ); + Ver_ParsePrintErrorMessage( pMan ); + return 0; + } + // get the equality sign + if ( Ver_StreamPopChar(p) != '=' ) + { + sprintf( pMan->sError, "Cannot read the assign statement for %s (expected equality sign).", pWord ); + Ver_ParsePrintErrorMessage( pMan ); + return 0; + } + // skip the comments + if ( !Ver_ParseSkipComments( pMan ) ) + return 0; + // get the second name + if ( fReduction ) + pEquation = Ver_StreamGetWord( p, ";" ); + else + pEquation = Ver_StreamGetWord( p, ",;" ); + if ( pEquation == NULL ) + { + sprintf( pMan->sError, "Cannot read the equation for %s.", Abc_ObjName(pNet) ); + Ver_ParsePrintErrorMessage( pMan ); + return 0; + } + + // consider the case of mapped network + if ( pMan->fMapped ) + { + Vec_PtrClear( pMan->vNames ); + if ( !strcmp( pEquation, "1\'b0" ) ) + pFunc = (Hop_Obj_t *)Mio_LibraryReadConst0(Abc_FrameReadLibGen()); + else if ( !strcmp( pEquation, "1\'b1" ) ) + pFunc = (Hop_Obj_t *)Mio_LibraryReadConst1(Abc_FrameReadLibGen()); + else + { + if ( Ver_ParseFindNet(pNtk, pEquation) == NULL ) + { + sprintf( pMan->sError, "Cannot read Verilog with non-trivail assignments in the mapped netlist.", pEquation ); + Ver_ParsePrintErrorMessage( pMan ); + return 0; + } + Vec_PtrPush( pMan->vNames, (void *)strlen(pEquation) ); + Vec_PtrPush( pMan->vNames, pEquation ); + // get the buffer + pFunc = (Hop_Obj_t *)Mio_LibraryReadBuf(Abc_FrameReadLibGen()); + } + } + else + { + // parse the formula + if ( fReduction ) + pFunc = Ver_FormulaReduction( pEquation, pNtk->pManFunc, pMan->vNames, pMan->sError ); + else + pFunc = Ver_FormulaParser( pEquation, pNtk->pManFunc, pMan->vNames, pMan->vStackFn, pMan->vStackOp, pMan->sError ); + if ( pFunc == NULL ) + { + Ver_ParsePrintErrorMessage( pMan ); + return 0; + } + } + + // create the node with the given inputs + pNode = Abc_NtkCreateNode( pNtk ); + pNode->pData = pFunc; + Abc_ObjAddFanin( pNet, pNode ); + // connect to fanin nets + for ( i = 0; i < Vec_PtrSize(pMan->vNames)/2; i++ ) + { + // get the name of this signal + Length = (int)Vec_PtrEntry( pMan->vNames, 2*i ); + pName = Vec_PtrEntry( pMan->vNames, 2*i + 1 ); + pName[Length] = 0; + // find the corresponding net + pNet = Ver_ParseFindNet( pNtk, pName ); + if ( pNet == NULL ) + { + sprintf( pMan->sError, "Cannot read the assign statement for %s (input wire %d is not defined).", pWord, pName ); + Ver_ParsePrintErrorMessage( pMan ); + return 0; + } + Abc_ObjAddFanin( pNode, pNet ); + } + + Symbol = Ver_StreamPopChar(p); + if ( Symbol == ',' ) + continue; + if ( Symbol == ';' ) + return 1; + } + return 1; +} + +/**Function************************************************************* + + Synopsis [Parses one directive.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Ver_ParseGateStandard( Ver_Man_t * pMan, Abc_Ntk_t * pNtk, Ver_GateType_t GateType ) +{ + Ver_Stream_t * p = pMan->pReader; + Abc_Obj_t * pNet, * pNode; + char * pWord, Symbol; + + // convert from the blackbox into the network with local functions representated by AIGs + if ( !Ver_ParseConvertNetwork( pMan, pNtk, pMan->fMapped ) ) + return 0; + + // this is gate name - throw it away + if ( Ver_StreamPopChar(p) != '(' ) + { + sprintf( pMan->sError, "Cannot parse a standard gate (expected opening paranthesis)." ); + Ver_ParsePrintErrorMessage( pMan ); + return 0; + } + Ver_ParseSkipComments( pMan ); + + // create the node + pNode = Abc_NtkCreateNode( pNtk ); + + // parse pairs of formal/actural inputs + while ( 1 ) + { + // parse the output name + pWord = Ver_ParseGetName( pMan ); + if ( pWord == NULL ) + return 0; + // get the net corresponding to this output + pNet = Ver_ParseFindNet( pNtk, pWord ); + if ( pNet == NULL ) + { + sprintf( pMan->sError, "Net is missing in gate %s.", pWord ); + Ver_ParsePrintErrorMessage( pMan ); + return 0; + } + // if this is the first net, add it as an output + if ( Abc_ObjFanoutNum(pNode) == 0 ) + Abc_ObjAddFanin( pNet, pNode ); + else + Abc_ObjAddFanin( pNode, pNet ); + // check if it is the end of gate + Ver_ParseSkipComments( pMan ); + Symbol = Ver_StreamPopChar(p); + if ( Symbol == ')' ) + break; + // skip comma + if ( Symbol != ',' ) + { + sprintf( pMan->sError, "Cannot parse a standard gate %s (expected closing paranthesis).", Abc_ObjName(Abc_ObjFanout0(pNode)) ); + Ver_ParsePrintErrorMessage( pMan ); + return 0; + } + Ver_ParseSkipComments( pMan ); + } + if ( (GateType == VER_GATE_BUF || GateType == VER_GATE_NOT) && Abc_ObjFaninNum(pNode) != 1 ) + { + sprintf( pMan->sError, "Buffer or interver with multiple fanouts %s (currently not supported).", Abc_ObjName(Abc_ObjFanout0(pNode)) ); + Ver_ParsePrintErrorMessage( pMan ); + return 0; + } + + // check if it is the end of gate + Ver_ParseSkipComments( pMan ); + if ( Ver_StreamPopChar(p) != ';' ) + { + sprintf( pMan->sError, "Cannot read standard gate %s (expected closing semicolumn).", Abc_ObjName(Abc_ObjFanout0(pNode)) ); + Ver_ParsePrintErrorMessage( pMan ); + return 0; + } + // add logic function + if ( GateType == VER_GATE_AND || GateType == VER_GATE_NAND ) + pNode->pData = Hop_CreateAnd( pNtk->pManFunc, Abc_ObjFaninNum(pNode) ); + else if ( GateType == VER_GATE_OR || GateType == VER_GATE_NOR ) + pNode->pData = Hop_CreateOr( pNtk->pManFunc, Abc_ObjFaninNum(pNode) ); + else if ( GateType == VER_GATE_XOR || GateType == VER_GATE_XNOR ) + pNode->pData = Hop_CreateExor( pNtk->pManFunc, Abc_ObjFaninNum(pNode) ); + else if ( GateType == VER_GATE_BUF || GateType == VER_GATE_NOT ) + pNode->pData = Hop_CreateAnd( pNtk->pManFunc, Abc_ObjFaninNum(pNode) ); + if ( GateType == VER_GATE_NAND || GateType == VER_GATE_NOR || GateType == VER_GATE_XNOR || GateType == VER_GATE_NOT ) + pNode->pData = Hop_Not( pNode->pData ); + return 1; +} + +/**Function************************************************************* + + Synopsis [Parses one directive.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Ver_ParseGate( Ver_Man_t * pMan, Abc_Ntk_t * pNtk, Mio_Gate_t * pGate ) +{ + Mio_Pin_t * pGatePin; + Ver_Stream_t * p = pMan->pReader; + Abc_Obj_t * pNetActual, * pNode; + char * pWord, Symbol; + + // convert from the blackbox into the network with local functions representated by gates + if ( 1 != pMan->fMapped ) + { + sprintf( pMan->sError, "The network appears to be mapped. Use \"r -m\" to read mapped Verilog." ); + Ver_ParsePrintErrorMessage( pMan ); + return 0; + } + + // update the network type if needed + if ( !Ver_ParseConvertNetwork( pMan, pNtk, 1 ) ) + return 0; + // parse the directive and set the pointers to the PIs/POs of the gate pWord = Ver_ParseGetName( pMan ); if ( pWord == NULL ) return 0; // this is gate name - throw it away - pGateName = pWord; if ( Ver_StreamPopChar(p) != '(' ) { - sprintf( pMan->sError, "Cannot parse gate %s (expected opening paranthesis).", pNtkGate->pName ); + sprintf( pMan->sError, "Cannot parse gate %s (expected opening paranthesis).", Mio_GateReadName(pGate) ); Ver_ParsePrintErrorMessage( pMan ); return 0; } + + // start the node + pNode = Abc_NtkCreateNode( pNtk ); + pNode->pData = pGate; + // parse pairs of formal/actural inputs + pGatePin = Mio_GateReadPins(pGate); while ( 1 ) { // process one pair of formal/actual parameters if ( Ver_StreamPopChar(p) != '.' ) { - sprintf( pMan->sError, "Cannot parse gate %s (expected .).", pNtkGate->pName ); + sprintf( pMan->sError, "Cannot parse gate %s (expected .).", Mio_GateReadName(pGate) ); Ver_ParsePrintErrorMessage( pMan ); return 0; } @@ -881,22 +1110,31 @@ int Ver_ParseGate( Ver_Man_t * pMan, Abc_Ntk_t * pNtkGate ) pWord = Ver_ParseGetName( pMan ); if ( pWord == NULL ) return 0; - // get the formal net - if ( Abc_NtkIsNetlist(pNtkGate) ) - pNetFormal = Abc_NtkFindNet( pNtkGate, pWord ); - else // if ( Abc_NtkIsStrash(pNtkGate) ) - assert( 0 ); - if ( pNetFormal == NULL ) + + // make sure that the formal name is the same as the gate's + if ( Mio_GateReadInputs(pGate) == Abc_ObjFaninNum(pNode) ) { - sprintf( pMan->sError, "Formal net is missing in gate %s.", pWord ); - Ver_ParsePrintErrorMessage( pMan ); - return 0; + if ( strcmp(pWord, Mio_GateReadOutName(pGate)) ) + { + sprintf( pMan->sError, "Formal output name listed %s is different from the name of the gate output %s.", pWord, Mio_GateReadOutName(pGate) ); + Ver_ParsePrintErrorMessage( pMan ); + return 0; + } + } + else + { + if ( strcmp(pWord, Mio_PinReadName(pGatePin)) ) + { + sprintf( pMan->sError, "Formal input name listed %s is different from the name of the corresponding pin %s.", pWord, Mio_PinReadName(pGatePin) ); + Ver_ParsePrintErrorMessage( pMan ); + return 0; + } } // open the paranthesis if ( Ver_StreamPopChar(p) != '(' ) { - sprintf( pMan->sError, "Cannot formal parameter %s of gate %s (expected opening paranthesis).", pWord, pNtkGate->pName ); + sprintf( pMan->sError, "Cannot formal parameter %s of gate %s (expected opening paranthesis).", pWord, Mio_GateReadName(pGate) ); Ver_ParsePrintErrorMessage( pMan ); return 0; } @@ -906,19 +1144,22 @@ int Ver_ParseGate( Ver_Man_t * pMan, Abc_Ntk_t * pNtkGate ) if ( pWord == NULL ) return 0; // check if the name is complemented + assert( pWord[0] != '~' ); +/* fCompl = (pWord[0] == '~'); if ( fCompl ) { fComplUsed = 1; pWord++; - if ( pMan->pNtkCur->pData == NULL ) - pMan->pNtkCur->pData = Extra_MmFlexStart(); + if ( pNtk->pData == NULL ) + pNtk->pData = Extra_MmFlexStart(); } +*/ // get the actual net - pNetActual = Abc_NtkFindNet( pMan->pNtkCur, pWord ); + pNetActual = Ver_ParseFindNet( pNtk, pWord ); if ( pNetActual == NULL ) { - sprintf( pMan->sError, "Actual net is missing in gate %s.", pWord ); + sprintf( pMan->sError, "Actual net %s is missing.", pWord ); Ver_ParsePrintErrorMessage( pMan ); return 0; } @@ -926,112 +1167,55 @@ int Ver_ParseGate( Ver_Man_t * pMan, Abc_Ntk_t * pNtkGate ) // close the paranthesis if ( Ver_StreamPopChar(p) != ')' ) { - sprintf( pMan->sError, "Cannot formal parameter %s of gate %s (expected closing paranthesis).", pWord, pNtkGate->pName ); + sprintf( pMan->sError, "Cannot formal parameter %s of gate %s (expected closing paranthesis).", pWord, Mio_GateReadName(pGate) ); Ver_ParsePrintErrorMessage( pMan ); return 0; } - // process the pair - if ( Abc_ObjFaninNum(pNetFormal) > 0 && Abc_ObjIsPi(Abc_ObjFanin0Ntk(pNetFormal)) ) // PI net (with polarity!) - Abc_ObjFanin0Ntk(pNetFormal)->pCopy = Abc_ObjNotCond( pNetActual, fCompl ); - else if ( Abc_ObjFanoutNum(pNetFormal) > 0 && Abc_ObjIsPo(Abc_ObjFanout0Ntk(pNetFormal)) ) // P0 net - { - assert( fCompl == 0 ); - Abc_ObjFanout0Ntk(pNetFormal)->pCopy = pNetActual; // Abc_ObjNotCond( pNetActual, fCompl ); - } + // add the fanin + if ( Mio_GateReadInputs(pGate) == Abc_ObjFaninNum(pNode) ) + Abc_ObjAddFanin( pNetActual, pNode ); // fanout else - { - sprintf( pMan->sError, "Cannot match formal net %s with PI or PO of the gate %s.", pWord, pNtkGate->pName ); - Ver_ParsePrintErrorMessage( pMan ); - return 0; - } + Abc_ObjAddFanin( pNode, pNetActual ); // fanin // check if it is the end of gate Ver_ParseSkipComments( pMan ); Symbol = Ver_StreamPopChar(p); if ( Symbol == ')' ) break; + // skip comma if ( Symbol != ',' ) { - sprintf( pMan->sError, "Cannot formal parameter %s of gate %s (expected closing paranthesis).", pWord, pNtkGate->pName ); + sprintf( pMan->sError, "Cannot formal parameter %s of gate %s (expected closing paranthesis).", pWord, Mio_GateReadName(pGate) ); Ver_ParsePrintErrorMessage( pMan ); return 0; } Ver_ParseSkipComments( pMan ); + + // get the next pin + pGatePin = Mio_PinReadNext(pGatePin); } - // check if it is the end of gate - Ver_ParseSkipComments( pMan ); - if ( Ver_StreamPopChar(p) != ';' ) + // check that the gate as the same number of input + if ( !(Abc_ObjFaninNum(pNode) == Mio_GateReadInputs(pGate) && Abc_ObjFanoutNum(pNode) == 1) ) { - sprintf( pMan->sError, "Cannot read gate %s (expected closing semicolumn).", pNtkGate->pName ); + sprintf( pMan->sError, "Parsing of gate %s has failed.", Mio_GateReadName(pGate) ); Ver_ParsePrintErrorMessage( pMan ); return 0; } - // make sure each input net is driven - Abc_NtkForEachPi( pNtkGate, pObj, i ) - if ( pObj->pCopy == NULL ) - { - sprintf( pMan->sError, "Formal input %s of gate %s has no actual input.", Abc_ObjName(Abc_ObjFanout0(pObj)), pNtkGate->pName ); - Ver_ParsePrintErrorMessage( pMan ); - return 0; - } -/* - // make sure each output net is driving something - Abc_NtkForEachPo( pNtkGate, pObj, i ) - if ( pObj->pCopy == NULL ) - { - sprintf( pMan->sError, "Formal output %s of gate %s has no actual output.", Abc_ObjName(Abc_ObjFanin0(pObj)), pNtkGate->pName ); - Ver_ParsePrintErrorMessage( pMan ); - return 0; - } -*/ - - // allocate memory to remember the phase - pPolarity = NULL; - if ( fComplUsed ) - { - int nBytes = 4 * Abc_BitWordNum( Abc_NtkPiNum(pNtkGate) ); - pPolarity = (unsigned *)Extra_MmFlexEntryFetch( pMan->pNtkCur->pData, nBytes ); - memset( pPolarity, 0, nBytes ); - } - // create box to represent this gate - if ( Abc_NtkHasBlackbox(pNtkGate) ) - pNode = Abc_NtkCreateBlackbox( pMan->pNtkCur ); - else - pNode = Abc_NtkCreateWhitebox( pMan->pNtkCur ); - pNode->pNext = (Abc_Obj_t *)pPolarity; - pNode->pData = pNtkGate; - // connect to fanin nets - Abc_NtkForEachPi( pNtkGate, pObj, i ) - { - if ( pPolarity && Abc_ObjIsComplement(pObj->pCopy) ) - { - Abc_InfoSetBit( pPolarity, i ); - pObj->pCopy = Abc_ObjRegular( pObj->pCopy ); - } - assert( !Abc_ObjIsComplement(pObj->pCopy) ); -// Abc_ObjAddFanin( pNode, pObj->pCopy ); - pTerm = Abc_NtkCreateBi( pNtk ); - Abc_ObjAddFanin( pTerm, pObj->pCopy ); - Abc_ObjAddFanin( pNode, pTerm ); - } - // connect to fanout nets - Abc_NtkForEachPo( pNtkGate, pObj, i ) + // check if it is the end of gate + Ver_ParseSkipComments( pMan ); + if ( Ver_StreamPopChar(p) != ';' ) { - if ( pObj->pCopy == NULL ) - pObj->pCopy = Abc_NtkFindOrCreateNet(pNtk, NULL); -// Abc_ObjAddFanin( pObj->pCopy, pNode ); - pTerm = Abc_NtkCreateBo( pNtk ); - Abc_ObjAddFanin( pTerm, pNode ); - Abc_ObjAddFanin( pObj->pCopy, pTerm ); + sprintf( pMan->sError, "Cannot read gate %s (expected closing semicolumn).", Mio_GateReadName(pGate) ); + Ver_ParsePrintErrorMessage( pMan ); + return 0; } return 1; } - /**Function************************************************************* Synopsis [Parses one directive.] @@ -1043,42 +1227,105 @@ int Ver_ParseGate( Ver_Man_t * pMan, Abc_Ntk_t * pNtkGate ) SeeAlso [] ***********************************************************************/ -int Ver_ParseGateStandard( Ver_Man_t * pMan, Ver_GateType_t GateType ) +int Ver_ParseBox( Ver_Man_t * pMan, Abc_Ntk_t * pNtk, Abc_Ntk_t * pNtkBox ) { Ver_Stream_t * p = pMan->pReader; - Hop_Man_t * pAig = pMan->pNtkCur->pManFunc; - Abc_Obj_t * pNet, * pNode; + Vec_Ptr_t * vNetPairs; + Abc_Obj_t * pNetFormal, * pNetActual; + Abc_Obj_t * pNode; char * pWord, Symbol; - // this is gate name - throw it away + int fCompl; + + // parse the directive and set the pointers to the PIs/POs of the gate + pWord = Ver_ParseGetName( pMan ); + if ( pWord == NULL ) + return 0; + + // create box to represent this gate + pNode = Abc_NtkCreateBlackbox( pNtk ); + pNode->pData = pNtkBox; + Abc_ObjAssignName( pNode, pWord, NULL ); + + // continue parsing the box if ( Ver_StreamPopChar(p) != '(' ) { - sprintf( pMan->sError, "Cannot parse a standard gate (expected opening paranthesis)." ); + sprintf( pMan->sError, "Cannot parse gate %s (expected opening paranthesis).", Abc_ObjName(pNode) ); Ver_ParsePrintErrorMessage( pMan ); return 0; } - Ver_ParseSkipComments( pMan ); - // create the node - pNode = Abc_NtkCreateNode( pMan->pNtkCur ); + // parse pairs of formal/actural inputs + vNetPairs = Vec_PtrAlloc( 16 ); + pNode->pCopy = (Abc_Obj_t *)vNetPairs; while ( 1 ) { - // parse the output name + // process one pair of formal/actual parameters + if ( Ver_StreamPopChar(p) != '.' ) + { + sprintf( pMan->sError, "Cannot parse gate %s (expected .).", Abc_ObjName(pNode) ); + Ver_ParsePrintErrorMessage( pMan ); + return 0; + } + + // parse the formal name pWord = Ver_ParseGetName( pMan ); if ( pWord == NULL ) return 0; - // get the net corresponding to this output - pNet = Abc_NtkFindNet( pMan->pNtkCur, pWord ); - if ( pNet == NULL ) + // get the formal net + pNetFormal = Abc_NtkFindOrCreateNet( pNtkBox, pWord ); + Vec_PtrPush( vNetPairs, pNetFormal ); + + // open the paranthesis + if ( Ver_StreamPopChar(p) != '(' ) { - sprintf( pMan->sError, "Net is missing in gate %s.", pWord ); + sprintf( pMan->sError, "Cannot formal parameter %s of gate %s (expected opening paranthesis).", pWord, Abc_ObjName(pNode)); Ver_ParsePrintErrorMessage( pMan ); return 0; } - // if this is the first net, add it as an output - if ( Abc_ObjFanoutNum(pNode) == 0 ) - Abc_ObjAddFanin( pNet, pNode ); + + // parse the actual name + pWord = Ver_ParseGetName( pMan ); + if ( pWord == NULL ) + return 0; + // consider the case of empty name + fCompl = 0; + if ( pWord[0] == 0 ) + { + // remove the formal net +// Vec_PtrPop( vNetPairs ); + pNetActual = Abc_NtkCreateObj( pNtk, ABC_OBJ_NET ); + } else - Abc_ObjAddFanin( pNode, pNet ); + { +/* + // check if the name is complemented + fCompl = (pWord[0] == '~'); + if ( fCompl ) + { + pWord++; + if ( pNtk->pData == NULL ) + pNtk->pData = Extra_MmFlexStart(); + } +*/ + // get the actual net + pNetActual = Ver_ParseFindNet( pNtk, pWord ); + if ( pNetActual == NULL ) + { + sprintf( pMan->sError, "Actual net is missing in gate %s.", Abc_ObjName(pNode) ); + Ver_ParsePrintErrorMessage( pMan ); + return 0; + } + } + Vec_PtrPush( vNetPairs, Abc_ObjNotCond( pNetActual, fCompl ) ); + + // close the paranthesis + if ( Ver_StreamPopChar(p) != ')' ) + { + sprintf( pMan->sError, "Cannot formal parameter %s of gate %s (expected closing paranthesis).", pWord, Abc_ObjName(pNode) ); + Ver_ParsePrintErrorMessage( pMan ); + return 0; + } + // check if it is the end of gate Ver_ParseSkipComments( pMan ); Symbol = Ver_StreamPopChar(p); @@ -1087,38 +1334,288 @@ int Ver_ParseGateStandard( Ver_Man_t * pMan, Ver_GateType_t GateType ) // skip comma if ( Symbol != ',' ) { - sprintf( pMan->sError, "Cannot parse a standard gate %s (expected closing paranthesis).", Abc_ObjName(Abc_ObjFanout0(pNode)) ); + sprintf( pMan->sError, "Cannot formal parameter %s of gate %s (expected closing paranthesis).", pWord, Abc_ObjName(pNode) ); Ver_ParsePrintErrorMessage( pMan ); return 0; } Ver_ParseSkipComments( pMan ); } - if ( (GateType == VER_GATE_BUF || GateType == VER_GATE_NOT) && Abc_ObjFaninNum(pNode) != 1 ) - { - sprintf( pMan->sError, "Buffer or interver with multiple fanouts %s (currently not supported).", Abc_ObjName(Abc_ObjFanout0(pNode)) ); - Ver_ParsePrintErrorMessage( pMan ); - return 0; - } // check if it is the end of gate Ver_ParseSkipComments( pMan ); if ( Ver_StreamPopChar(p) != ';' ) { - sprintf( pMan->sError, "Cannot read standard gate %s (expected closing semicolumn).", Abc_ObjName(Abc_ObjFanout0(pNode)) ); + sprintf( pMan->sError, "Cannot read gate %s (expected closing semicolumn).", Abc_ObjName(pNode) ); Ver_ParsePrintErrorMessage( pMan ); return 0; } - // add logic function - if ( GateType == VER_GATE_AND || GateType == VER_GATE_NAND ) - pNode->pData = Hop_CreateAnd( pAig, Abc_ObjFaninNum(pNode) ); - else if ( GateType == VER_GATE_OR || GateType == VER_GATE_NOR ) - pNode->pData = Hop_CreateOr( pAig, Abc_ObjFaninNum(pNode) ); - else if ( GateType == VER_GATE_XOR || GateType == VER_GATE_XNOR ) - pNode->pData = Hop_CreateExor( pAig, Abc_ObjFaninNum(pNode) ); - else if ( GateType == VER_GATE_BUF || GateType == VER_GATE_NOT ) - pNode->pData = Hop_CreateAnd( pAig, Abc_ObjFaninNum(pNode) ); - if ( GateType == VER_GATE_NAND || GateType == VER_GATE_NOR || GateType == VER_GATE_XNOR || GateType == VER_GATE_NOT ) - pNode->pData = Hop_Not( pNode->pData ); + + return 1; +} + +/**Function************************************************************* + + Synopsis [Connects one box to the network] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Ver_ParseConnectBox( Ver_Man_t * pMan, Abc_Obj_t * pBox ) +{ + Vec_Ptr_t * vNetPairs = (Vec_Ptr_t *)pBox->pCopy; + Abc_Ntk_t * pNtk = pBox->pNtk; + Abc_Ntk_t * pNtkBox = pBox->pData; + Abc_Obj_t * pNet, * pTerm, * pTermNew; + int i; + + assert( !Ver_ObjIsConnected(pBox) ); + assert( Ver_NtkIsDefined(pNtkBox) ); + assert( !Abc_NtkHasBlackbox(pNtkBox) || Abc_NtkBoxNum(pNtkBox) == 1 ); + + // clean the PI/PO nets + Abc_NtkForEachPi( pNtkBox, pTerm, i ) + Abc_ObjFanout0(pTerm)->pCopy = NULL; + Abc_NtkForEachPo( pNtkBox, pTerm, i ) + Abc_ObjFanin0(pTerm)->pCopy = NULL; + + // map formal nets into actual nets + Vec_PtrForEachEntry( vNetPairs, pNet, i ) + { + // get the actual net corresponding to this formal net (pNet) + pNet->pCopy = Vec_PtrEntry( vNetPairs, ++i ); + // make sure the actual net is not complemented (otherwise need to use polarity) + assert( !Abc_ObjIsComplement(pNet->pCopy) ); + } + + // make sure all PI nets are assigned + Abc_NtkForEachPi( pNtkBox, pTerm, i ) + { + if ( Abc_ObjFanout0(pTerm)->pCopy == NULL ) + { + sprintf( pMan->sError, "Input formal net %s of network %s is not driven in box %s.", + Abc_ObjName(Abc_ObjFanout0(pTerm)), pNtkBox->pName, Abc_ObjName(pBox) ); + Ver_ParsePrintErrorMessage( pMan ); + return 0; + } + pTermNew = Abc_NtkCreateBi( pNtk ); + Abc_ObjAddFanin( pBox, pTermNew ); + Abc_ObjAddFanin( pTermNew, Abc_ObjFanout0(pTerm)->pCopy ); + } + + // create fanins of the box + Abc_NtkForEachPo( pNtkBox, pTerm, i ) + { + if ( Abc_ObjFanin0(pTerm)->pCopy == NULL ) + Abc_ObjFanin0(pTerm)->pCopy = Abc_NtkCreateObj( pNtk, ABC_OBJ_NET ); + pTermNew = Abc_NtkCreateBo( pNtk ); + Abc_ObjAddFanin( Abc_ObjFanin0(pTerm)->pCopy, pTermNew ); + Abc_ObjAddFanin( pTermNew, pBox ); + } + + // free the mapping + Vec_PtrFree( vNetPairs ); + pBox->pCopy = NULL; + return 1; +} + +/**Function************************************************************* + + Synopsis [Attaches the boxes to the network.] + + Description [Makes sure that the undefined boxes are connected correctly.] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Vec_ParseAttachBoxes( Ver_Man_t * pMan ) +{ + Abc_Ntk_t * pNtk, * pNtkBox; + Vec_Ptr_t * vEnvoys, * vNetPairs, * vPivots; + Abc_Obj_t * pBox, * pTerm, * pNet, * pNetDr, * pNetAct; + int i, k, m, nBoxes; + + // connect defined boxes + Vec_PtrForEachEntry( pMan->pDesign->vModules, pNtk, i ) + { + Abc_NtkForEachBlackbox( pNtk, pBox, k ) + { + if ( pBox->pData && Ver_NtkIsDefined(pBox->pData) ) + if ( !Ver_ParseConnectBox( pMan, pBox ) ) + return 0; + } + } + + // convert blackboxes to whiteboxes + Vec_PtrForEachEntry( pMan->pDesign->vModules, pNtk, i ) + Abc_NtkForEachBlackbox( pNtk, pBox, k ) + { + pNtkBox = pBox->pData; + if ( pNtkBox == NULL ) + continue; + + if ( !strcmp( pNtkBox->pName, "ADDHX1" ) ) + { + int x = 0; + } + + if ( pBox->pData && !Abc_NtkHasBlackbox(pBox->pData) ) + Abc_ObjBlackboxToWhitebox( pBox ); + } + + + // search for undefined boxes + nBoxes = 0; + Vec_PtrForEachEntry( pMan->pDesign->vModules, pNtk, i ) + nBoxes += !Ver_NtkIsDefined(pNtk); + // quit if no undefined boxes are found + if ( nBoxes == 0 ) + return 1; + + // count how many times each box occurs + Vec_PtrForEachEntry( pMan->pDesign->vModules, pNtk, i ) + { + assert( pNtk->pData == NULL ); + pNtk->pData = NULL; + } + Vec_PtrForEachEntry( pMan->pDesign->vModules, pNtk, i ) + Abc_NtkForEachBlackbox( pNtk, pBox, k ) + { + if ( pBox->pData == NULL ) + continue; + pNtkBox = pBox->pData; + pNtkBox->pData = (void *)((int)pNtkBox->pData + 1); + } + + // print the boxes + printf( "Warning: The design contains %d undefined objects interpreted as blackboxes:\n", nBoxes ); + Vec_PtrForEachEntry( pMan->pDesign->vModules, pNtk, i ) + if ( !Ver_NtkIsDefined(pNtk) ) + printf( "%s (%d) ", Abc_NtkName(pNtk), (int)pNtk->pData ); + printf( "\n" ); + + // clean the boxes + Vec_PtrForEachEntry( pMan->pDesign->vModules, pNtk, i ) + pNtk->pData = NULL; + + + // map actual nets into formal nets belonging to the undef boxes + vPivots = Vec_PtrAlloc( 100 ); + Vec_PtrForEachEntry( pMan->pDesign->vModules, pNtk, i ) + { + Abc_NtkForEachBlackbox( pNtk, pBox, k ) + { + if ( pBox->pData == NULL || Ver_NtkIsDefined(pBox->pData) ) + continue; + vNetPairs = (Vec_Ptr_t *)pBox->pCopy; + Vec_PtrForEachEntry( vNetPairs, pNet, m ) + { + pNetAct = Vec_PtrEntry( vNetPairs, ++m ); + // skip already driven nets and constants + if ( Abc_ObjFaninNum(pNetAct) == 1 ) + continue; + if ( !(strcmp(Abc_ObjName(pNetAct), "1\'b0") && strcmp(Abc_ObjName(pNetAct), "1\'b1")) ) // constant + continue; + // add this net + if ( pNetAct->pData == NULL ) + { + pNetAct->pData = Vec_PtrAlloc( 16 ); + Vec_PtrPush( vPivots, pNetAct ); + } + vEnvoys = pNetAct->pData; + Vec_PtrPush( vEnvoys, pNet ); + } + } + } + + // for each pivot net, find the driver + Vec_PtrForEachEntry( vPivots, pNetAct, i ) + { + char * pName = Abc_ObjName(pNetAct); +/* + if ( !strcmp( Abc_ObjName(pNetAct), "dma_fifo_ff_cnt[2]" ) ) + { + int x = 0; + } +*/ + assert( Abc_ObjFaninNum(pNetAct) == 0 ); + assert( strcmp(Abc_ObjName(pNetAct), "1\'b0") && strcmp(Abc_ObjName(pNetAct), "1\'b1") ); + vEnvoys = pNetAct->pData; pNetAct->pData = NULL; + // find the driver starting from the last nets + pNetDr = NULL; + for ( m = 0; m < 64; m++ ) + { + Vec_PtrForEachEntry( vEnvoys, pNet, k ) + { + if ( Abc_ObjId(pNet) == 0 ) + continue; + if ( (int)Abc_ObjId(pNet) == Abc_NtkObjNumMax(pNet->pNtk) - 1 - m ) + { + pNetDr = pNet; + break; + } + } + if ( pNetDr ) + break; + } + assert( pNetDr != NULL ); + Vec_PtrWriteEntry( vPivots, i, pNetDr ); + Vec_PtrFree( vEnvoys ); + } + + // for each pivot net, create driver + Vec_PtrForEachEntry( vPivots, pNetDr, i ) + { + if ( pNetDr == NULL ) + continue; + assert( Abc_ObjFaninNum(pNetDr) <= 1 ); + if ( Abc_ObjFaninNum(pNetDr) == 1 ) + continue; + // drive this net with the box + pTerm = Abc_NtkCreateBo( pNetDr->pNtk ); + assert( Abc_NtkBoxNum(pNetDr->pNtk) <= 1 ); + pBox = Abc_NtkBoxNum(pNetDr->pNtk)? Abc_NtkBox(pNetDr->pNtk,0) : Abc_NtkCreateBlackbox(pNetDr->pNtk); + Abc_ObjAddFanin( Abc_NtkCreatePo(pNetDr->pNtk), pNetDr ); + Abc_ObjAddFanin( pNetDr, pTerm ); + Abc_ObjAddFanin( pTerm, pBox ); + } + Vec_PtrFree( vPivots ); + + // connect the remaining boxes + Vec_PtrForEachEntry( pMan->pDesign->vModules, pNtk, i ) + { + if ( Abc_NtkPiNum(pNtk) ) + continue; + Abc_NtkForEachNet( pNtk, pNet, k ) + { + if ( Abc_ObjFaninNum(pNet) ) + continue; + // drive this net + pTerm = Abc_NtkCreateBi( pNet->pNtk ); + assert( Abc_NtkBoxNum(pNet->pNtk) <= 1 ); + pBox = Abc_NtkBoxNum(pNet->pNtk)? Abc_NtkBox(pNet->pNtk,0) : Abc_NtkCreateBlackbox(pNet->pNtk); + Abc_ObjAddFanin( pBox, pTerm ); + Abc_ObjAddFanin( pTerm, pNet ); + Abc_ObjAddFanin( pNet, Abc_NtkCreatePi(pNet->pNtk) ); + } + } + + // connect the remaining boxes + Vec_PtrForEachEntry( pMan->pDesign->vModules, pNtk, i ) + { + Abc_NtkForEachBlackbox( pNtk, pBox, k ) + { + char * pName = Abc_ObjName(pBox); + if ( !Ver_ObjIsConnected(pBox) ) + if ( !Ver_ParseConnectBox( pMan, pBox ) ) + return 0; + } + } return 1; } @@ -1138,9 +1635,9 @@ Abc_Obj_t * Ver_ParseCreatePi( Abc_Ntk_t * pNtk, char * pName ) { Abc_Obj_t * pNet, * pTerm; // get the PI net - pNet = Abc_NtkFindNet( pNtk, pName ); - if ( pNet ) - printf( "Warning: PI \"%s\" appears twice in the list.\n", pName ); +// pNet = Ver_ParseFindNet( pNtk, pName ); +// if ( pNet ) +// printf( "Warning: PI \"%s\" appears twice in the list.\n", pName ); pNet = Abc_NtkFindOrCreateNet( pNtk, pName ); // add the PI node pTerm = Abc_NtkCreatePi( pNtk ); @@ -1163,9 +1660,9 @@ Abc_Obj_t * Ver_ParseCreatePo( Abc_Ntk_t * pNtk, char * pName ) { Abc_Obj_t * pNet, * pTerm; // get the PO net - pNet = Abc_NtkFindNet( pNtk, pName ); - if ( pNet && Abc_ObjFaninNum(pNet) == 0 ) - printf( "Warning: PO \"%s\" appears twice in the list.\n", pName ); +// pNet = Ver_ParseFindNet( pNtk, pName ); +// if ( pNet && Abc_ObjFaninNum(pNet) == 0 ) +// printf( "Warning: PO \"%s\" appears twice in the list.\n", pName ); pNet = Abc_NtkFindOrCreateNet( pNtk, pName ); // add the PO node pTerm = Abc_NtkCreatePo( pNtk ); @@ -1224,6 +1721,50 @@ Abc_Obj_t * Ver_ParseCreateInv( Abc_Ntk_t * pNtk, Abc_Obj_t * pNet ) return pNet; } + + +/* + // allocate memory to remember the phase + pPolarity = NULL; + if ( fComplUsed ) + { + int nBytes = 4 * Abc_BitWordNum( Abc_NtkPiNum(pNtkBox) ); + pPolarity = (unsigned *)Extra_MmFlexEntryFetch( pNtk->pData, nBytes ); + memset( pPolarity, 0, nBytes ); + } + // create box to represent this gate + if ( Abc_NtkHasBlackbox(pNtkBox) ) + pNode = Abc_NtkCreateBlackbox( pNtk ); + else + pNode = Abc_NtkCreateWhitebox( pNtk ); + pNode->pNext = (Abc_Obj_t *)pPolarity; + pNode->pData = pNtkBox; + // connect to fanin nets + Abc_NtkForEachPi( pNtkBox, pObj, i ) + { + if ( pPolarity && Abc_ObjIsComplement(pObj->pCopy) ) + { + Abc_InfoSetBit( pPolarity, i ); + pObj->pCopy = Abc_ObjRegular( pObj->pCopy ); + } + assert( !Abc_ObjIsComplement(pObj->pCopy) ); +// Abc_ObjAddFanin( pNode, pObj->pCopy ); + pTerm = Abc_NtkCreateBi( pNtk ); + Abc_ObjAddFanin( pTerm, pObj->pCopy ); + Abc_ObjAddFanin( pNode, pTerm ); + } + // connect to fanout nets + Abc_NtkForEachPo( pNtkBox, pObj, i ) + { + if ( pObj->pCopy == NULL ) + pObj->pCopy = Abc_NtkFindOrCreateNet(pNtk, NULL); +// Abc_ObjAddFanin( pObj->pCopy, pNode ); + pTerm = Abc_NtkCreateBo( pNtk ); + Abc_ObjAddFanin( pTerm, pNode ); + Abc_ObjAddFanin( pObj->pCopy, pTerm ); + } +*/ + //////////////////////////////////////////////////////////////////////// /// END OF FILE /// //////////////////////////////////////////////////////////////////////// diff --git a/src/base/ver/verFormula.c b/src/base/ver/verFormula.c index 16192f6a..253754ae 100644 --- a/src/base/ver/verFormula.c +++ b/src/base/ver/verFormula.c @@ -72,8 +72,8 @@ static int Ver_FormulaParserFindVar( char * pString, Vec_Ptr_t * vNames ***********************************************************************/ void * Ver_FormulaParser( char * pFormula, void * pMan, Vec_Ptr_t * vNames, Vec_Ptr_t * vStackFn, Vec_Int_t * vStackOp, char * pErrorMessage ) { - Hop_Obj_t * bFunc, * bTemp; char * pTemp; + Hop_Obj_t * bFunc, * bTemp; int nParans, Flag; int Oper, Oper1, Oper2; int v; diff --git a/src/base/ver/verParse.c b/src/base/ver/verParse.c index f3afaca0..9462fc8b 100644 --- a/src/base/ver/verParse.c +++ b/src/base/ver/verParse.c @@ -100,7 +100,7 @@ char * Ver_ParseGetName( Ver_Man_t * pMan ) { pMan->fNameLast = 1; Ver_StreamPopChar( p ); - pWord = Ver_StreamGetWord( p, " " ); + pWord = Ver_StreamGetWord( p, " \r\n" ); } else pWord = Ver_StreamGetWord( p, " \t\n\r(),;" ); diff --git a/src/map/mio/mio.h b/src/map/mio/mio.h index dabc05dd..dbe2420b 100644 --- a/src/map/mio/mio.h +++ b/src/map/mio/mio.h @@ -98,6 +98,7 @@ extern float Mio_LibraryReadDelayAnd2Max( Mio_Library_t * pLib ); extern float Mio_LibraryReadAreaInv ( Mio_Library_t * pLib ); extern float Mio_LibraryReadAreaBuf ( Mio_Library_t * pLib ); extern float Mio_LibraryReadAreaNand2 ( Mio_Library_t * pLib ); +extern int Mio_LibraryReadGateNameMax( Mio_Library_t * pLib ); extern char * Mio_GateReadName ( Mio_Gate_t * pGate ); extern char * Mio_GateReadOutName ( Mio_Gate_t * pGate ); extern double Mio_GateReadArea ( Mio_Gate_t * pGate ); @@ -120,8 +121,8 @@ extern double Mio_PinReadDelayFanoutFall( Mio_Pin_t * pPin ); extern double Mio_PinReadDelayBlockMax ( Mio_Pin_t * pPin ); extern Mio_Pin_t * Mio_PinReadNext ( Mio_Pin_t * pPin ); /*=== mioRead.c =============================================================*/ -extern Mio_Library_t * Mio_LibraryRead( Abc_Frame_t * pAbc, char * FileName, char * ExcludeFile, int fVerbose ); -extern int Mio_LibraryReadExclude( Abc_Frame_t * pAbc, char * ExcludeFile, st_table * tExcludeGate ); +extern Mio_Library_t * Mio_LibraryRead( void * pAbc, char * FileName, char * ExcludeFile, int fVerbose ); +extern int Mio_LibraryReadExclude( void * pAbc, char * ExcludeFile, st_table * tExcludeGate ); /*=== mioFunc.c =============================================================*/ extern int Mio_LibraryParseFormulas( Mio_Library_t * pLib ); /*=== mioUtils.c =============================================================*/ diff --git a/src/map/mio/mioApi.c b/src/map/mio/mioApi.c index a9aaac19..73473f8b 100644 --- a/src/map/mio/mioApi.c +++ b/src/map/mio/mioApi.c @@ -60,6 +60,30 @@ float Mio_LibraryReadAreaNand2 ( Mio_Library_t * pLib ) { retur /**Function************************************************************* + Synopsis [Returns the longest gate name.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Mio_LibraryReadGateNameMax( Mio_Library_t * pLib ) +{ + Mio_Gate_t * pGate; + int LenMax = 0, LenCur; + Mio_LibraryForEachGate( pLib, pGate ) + { + LenCur = strlen( Mio_GateReadName(pGate) ); + if ( LenMax < LenCur ) + LenMax = LenCur; + } + return LenMax; +} + +/**Function************************************************************* + Synopsis [Read Mvc of the gate by name.] Description [] diff --git a/src/opt/res/resCore.c b/src/opt/res/resCore.c index 95728e9a..4cc5e56b 100644 --- a/src/opt/res/resCore.c +++ b/src/opt/res/resCore.c @@ -197,7 +197,7 @@ int Abc_NtkResynthesize( Abc_Ntk_t * pNtk, Res_Par_t * pPars ) Abc_NtkSweep( pNtk, 0 ); // convert into the AIG - if ( !Abc_NtkLogicToAig(pNtk) ) + if ( !Abc_NtkToAig(pNtk) ) { fprintf( stdout, "Converting to BDD has failed.\n" ); Res_ManFree( p ); diff --git a/src/opt/ret/retCore.c b/src/opt/ret/retCore.c index 93181898..551ec594 100644 --- a/src/opt/ret/retCore.c +++ b/src/opt/ret/retCore.c @@ -116,7 +116,7 @@ int Abc_NtkRetimeDebug( Abc_Ntk_t * pNtk ) extern int Abc_NtkSecFraig( Abc_Ntk_t * pNtk1, Abc_Ntk_t * pNtk2, int nSeconds, int nFrames, int fVerbose ); Abc_Ntk_t * pNtkRet; assert( Abc_NtkIsLogic(pNtk) ); - Abc_NtkLogicToSop( pNtk, 0 ); + Abc_NtkToSop( pNtk, 0 ); // if ( !Abc_NtkCheck( pNtk ) ) // fprintf( stdout, "Abc_NtkRetimeDebug(): Network check has failed.\n" ); // Io_WriteBlifLogic( pNtk, "debug_temp.blif", 1 ); diff --git a/src/opt/ret/retInit.c b/src/opt/ret/retInit.c index 156df0dc..dcb71c60 100644 --- a/src/opt/ret/retInit.c +++ b/src/opt/ret/retInit.c @@ -50,7 +50,7 @@ Vec_Int_t * Abc_NtkRetimeInitialValues( Abc_Ntk_t * pNtkCone, Vec_Int_t * vValue return Vec_IntDup( vValues ); // convert the target network to AIG pNtkLogic = Abc_NtkDup( pNtkCone ); - Abc_NtkLogicToAig( pNtkLogic ); + Abc_NtkToAig( pNtkLogic ); // get the miter pNtkMiter = Abc_NtkCreateTarget( pNtkLogic, pNtkLogic->vCos, vValues ); if ( fVerbose ) diff --git a/src/sat/csat/csat_apis.c b/src/sat/csat/csat_apis.c index c7340824..9d27e892 100644 --- a/src/sat/csat/csat_apis.c +++ b/src/sat/csat/csat_apis.c @@ -677,7 +677,7 @@ void ABC_Dump_Bench_File( ABC_Manager mng ) // derive the netlist pNtkAig = Abc_NtkStrash( mng->pNtk, 0, 0 ); - pNtkTemp = Abc_NtkLogicToNetlistBench( pNtkAig ); + pNtkTemp = Abc_NtkToNetlistBench( pNtkAig ); Abc_NtkDelete( pNtkAig ); if ( pNtkTemp == NULL ) { printf( "ABC_Dump_Bench_File: Dumping BENCH has failed.\n" ); return; } |