From fb51057e4a36d2e5737bba8739b88140b55db7c7 Mon Sep 17 00:00:00 2001 From: Alan Mishchenko Date: Mon, 19 Feb 2007 08:01:00 -0800 Subject: Version abc70219 --- src/base/abc/abc.h | 26 +- src/base/abc/abcFunc.c | 50 +- src/base/abc/abcHie.c | 71 +- src/base/abc/abcLib.c | 2 + src/base/abc/abcNetlist.c | 74 +-- src/base/abc/abcNtk.c | 19 +- src/base/abc/abcShow.c | 2 +- src/base/abc/abcUtil.c | 2 + src/base/abci/abc.c | 16 +- src/base/abci/abcDebug.c | 2 +- src/base/abci/abcDress.c | 2 +- src/base/abci/abcFxu.c | 2 +- src/base/abci/abcIvy.c | 28 +- src/base/abci/abcMini.c | 14 +- src/base/abci/abcQuant.c | 97 ++- src/base/abci/abcStrash.c | 4 +- src/base/abci/abcSweep.c | 2 +- src/base/cmd/cmd.c | 6 +- src/base/io/io.c | 36 +- src/base/io/ioReadBench.c | 2 +- src/base/io/ioReadBlifMv.c | 105 ++- src/base/io/ioReadVerilog.c | 27 +- src/base/io/ioUtil.c | 54 +- src/base/io/ioWriteBlif.c | 34 +- src/base/io/ioWriteCnf.c | 2 +- src/base/io/ioWriteVerilog.c | 155 +++-- src/base/ver/ver.h | 14 +- src/base/ver/verCore.c | 1461 +++++++++++++++++++++++++++++------------- src/base/ver/verFormula.c | 2 +- src/base/ver/verParse.c | 2 +- 30 files changed, 1511 insertions(+), 802 deletions(-) (limited to 'src/base') 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 @@ -28,6 +28,39 @@ /// FUNCTION DEFINITIONS /// //////////////////////////////////////////////////////////////////////// +/**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.] @@ -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<Err, "usage: read [-ch] \n" ); + fprintf( pAbc->Err, "usage: read [-mch] \n" ); fprintf( pAbc->Err, "\t replaces the current network by the network read from \n" ); fprintf( pAbc->Err, "\t by calling the parser that matches the extension of \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] \n" ); - fprintf( pAbc->Err, "\t read the network in Verilog (IWLS 2005 subset)\n" ); + fprintf( pAbc->Err, "usage: read_verilog [-mch] \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] \n" ); fprintf( pAbc->Err, "\t writes the current network into by calling\n" ); fprintf( pAbc->Err, "\t the hierarchical writer that matches the extension of \n" ); + fprintf( pAbc->Err, "\t-m : toggle reading mapped Verilog for [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,41 +386,12 @@ 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++; } } -/**Function************************************************************* - - Synopsis [Writes the latches.] - - Description [] - - SideEffects [] - - 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.] @@ -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,118 +626,90 @@ int Ver_ParseSignal( Ver_Man_t * pMan, Ver_SignalType_t SigType ) SeeAlso [] ***********************************************************************/ -int Ver_ParseAssign( 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 * pNode, * pNet; - char * pWord, * pName, * pEquation; - Hop_Obj_t * pFunc; + Abc_Obj_t * pNet, * pNet2; + int fStopAfterOne; + char * pWord, * pWord2; 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 ); + // parse the directive + pWord = Ver_ParseGetName( pMan ); + if ( pWord == NULL ) return 0; - } - - while ( 1 ) + if ( pWord[0] == '@' ) { - // get the name of the output signal + Ver_StreamSkipToChars( p, ")" ); + Ver_StreamPopChar(p); + // parse the directive 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 ) + } + // decide how many statements to parse + fStopAfterOne = 0; + if ( strcmp( pWord, "begin" ) ) + fStopAfterOne = 1; + // iterate over the initial states + while ( 1 ) + { + if ( !fStopAfterOne ) { - pWord++; - pWord[strlen(pWord)-1] = 0; - assert( pWord[0] != '\\' ); + // get the name of the output signal + pWord = Ver_ParseGetName( pMan ); + if ( pWord == NULL ) + return 0; + // look for the end of directive + if ( !strcmp( pWord, "end" ) ) + break; } // get the fanout net - pNet = Abc_NtkFindNet( pNtk, pWord ); + pNet = Ver_ParseFindNet( pNtk, pWord ); if ( pNet == NULL ) { - sprintf( pMan->sError, "Cannot read the assign statement for %s (output wire is not defined).", pWord ); + sprintf( pMan->sError, "Cannot read the always statement for %s (output wire is not defined).", pWord ); Ver_ParsePrintErrorMessage( pMan ); return 0; } // get the equality sign - if ( Ver_StreamPopChar(p) != '=' ) + Symbol = Ver_StreamPopChar(p); + if ( Symbol != '<' && Symbol != '=' ) { - sprintf( pMan->sError, "Cannot read the assign statement for %s (expected equality sign).", pWord ); + sprintf( pMan->sError, "Cannot read the assign statement for %s (expected <= or =).", pWord ); Ver_ParsePrintErrorMessage( pMan ); return 0; } + if ( Symbol == '<' ) + Ver_StreamPopChar(p); // 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 ); + pWord2 = Ver_ParseGetName( pMan ); + if ( pWord2 == NULL ) return 0; + // check if the name is complemented + if ( pWord2[0] == '~' ) + { + pNet2 = Ver_ParseFindNet( pNtk, pWord2+1 ); + pNet2 = Ver_ParseCreateInv( pNtk, pNet2 ); } - - // 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 ) + pNet2 = Ver_ParseFindNet( pNtk, pWord2 ); + if ( pNet2 == NULL ) { + sprintf( pMan->sError, "Cannot read the always statement for %s (input wire is not defined).", pWord2 ); 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 ); - } + // create the latch + Ver_ParseCreateLatch( pNtk, pNet2, pNet ); + // remove the last symbol Symbol = Ver_StreamPopChar(p); - if ( Symbol == ',' ) - continue; - if ( Symbol == ';' ) - return 1; + assert( Symbol == ';' ); + // quit if only one directive + if ( fStopAfterOne ) + break; } return 1; } @@ -642,27 +725,17 @@ int Ver_ParseAssign( Ver_Man_t * pMan ) SeeAlso [] ***********************************************************************/ -int Ver_ParseAlways( 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 * pNet, * pNet2; + Abc_Obj_t * pNode, * pNet; int fStopAfterOne; - char * pWord, * pWord2; + char * pWord, * pEquation; char Symbol; // parse the directive pWord = Ver_ParseGetName( pMan ); if ( pWord == NULL ) return 0; - if ( pWord[0] == '@' ) - { - Ver_StreamSkipToChars( p, ")" ); - Ver_StreamPopChar(p); - // parse the directive - pWord = Ver_ParseGetName( pMan ); - if ( pWord == NULL ) - return 0; - } // decide how many statements to parse fStopAfterOne = 0; if ( strcmp( pWord, "begin" ) ) @@ -681,10 +754,10 @@ 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 ); + sprintf( pMan->sError, "Cannot read the initial statement for %s (output wire is not defined).", pWord ); Ver_ParsePrintErrorMessage( pMan ); return 0; } @@ -702,25 +775,31 @@ int Ver_ParseAlways( Ver_Man_t * pMan ) if ( !Ver_ParseSkipComments( pMan ) ) return 0; // get the second name - pWord2 = Ver_ParseGetName( pMan ); - if ( pWord2 == NULL ) + pEquation = Ver_StreamGetWord( p, ";" ); + if ( pEquation == NULL ) return 0; - // check if the name is complemented - if ( pWord2[0] == '~' ) + // find the corresponding latch + if ( Abc_ObjFaninNum(pNet) == 0 ) { - pNet2 = Abc_NtkFindNet( pNtk, pWord2+1 ); - pNet2 = Ver_ParseCreateInv( pNtk, pNet2 ); + sprintf( pMan->sError, "Cannot find the latch to assign the initial value." ); + Ver_ParsePrintErrorMessage( pMan ); + return 0; } - else - pNet2 = Abc_NtkFindNet( pNtk, pWord2 ); - if ( pNet2 == NULL ) + pNode = Abc_ObjFanin0(Abc_ObjFanin0(pNet)); + assert( Abc_ObjIsLatch(pNode) ); + // set the initial state + if ( !strcmp(pEquation, "0") || !strcmp(pEquation, "1\'b0") ) + Abc_LatchSetInit0( pNode ); + else if ( !strcmp(pEquation, "1") || !strcmp(pEquation, "1\'b1") ) + Abc_LatchSetInit1( pNode ); +// else if ( !strcmp(pEquation, "2") ) +// Abc_LatchSetInitDc( pNode ); + else { - sprintf( pMan->sError, "Cannot read the always statement for %s (input wire is not defined).", pWord2 ); + sprintf( pMan->sError, "Incorrect initial value of the latch %s.", Abc_ObjName(pNet) ); Ver_ParsePrintErrorMessage( pMan ); return 0; } - // create the latch - Ver_ParseCreateLatch( pNtk, pNet2, pNet ); // remove the last symbol Symbol = Ver_StreamPopChar(p); assert( Symbol == ';' ); @@ -742,88 +821,397 @@ int Ver_ParseAlways( Ver_Man_t * pMan ) SeeAlso [] ***********************************************************************/ -int Ver_ParseInitial( Ver_Man_t * pMan ) +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 * pNode, * pNet; - int fStopAfterOne; - char * pWord, * pEquation; + char * pWord, * pName, * pEquation; + Hop_Obj_t * pFunc; char Symbol; - // parse the directive - pWord = Ver_ParseGetName( pMan ); - if ( pWord == NULL ) + 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; - // decide how many statements to parse - fStopAfterOne = 0; - if ( strcmp( pWord, "begin" ) ) - fStopAfterOne = 1; - // iterate over the initial states + while ( 1 ) { - if ( !fStopAfterOne ) + // 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 ) { - // get the name of the output signal - pWord = Ver_ParseGetName( pMan ); - if ( pWord == NULL ) - return 0; - // look for the end of directive - if ( !strcmp( pWord, "end" ) ) - break; + pWord++; + pWord[strlen(pWord)-1] = 0; + assert( pWord[0] != '\\' ); } // 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 ); + 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 - Symbol = Ver_StreamPopChar(p); - if ( Symbol != '<' && Symbol != '=' ) + if ( Ver_StreamPopChar(p) != '=' ) { - sprintf( pMan->sError, "Cannot read the assign statement for %s (expected <= or =).", pWord ); + sprintf( pMan->sError, "Cannot read the assign statement for %s (expected equality sign).", pWord ); Ver_ParsePrintErrorMessage( pMan ); return 0; } - if ( Symbol == '<' ) - Ver_StreamPopChar(p); // skip the comments if ( !Ver_ParseSkipComments( pMan ) ) return 0; // get the second name - pEquation = Ver_StreamGetWord( p, ";" ); + 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; - // find the corresponding latch - if ( Abc_ObjFaninNum(pNet) == 0 ) + } + + // consider the case of mapped network + if ( pMan->fMapped ) { - sprintf( pMan->sError, "Cannot find the latch to assign the initial value." ); + 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; } - pNode = Abc_ObjFanin0(Abc_ObjFanin0(pNet)); - assert( Abc_ObjIsLatch(pNode) ); - // set the initial state - if ( !strcmp(pEquation, "0") || !strcmp(pEquation, "1\'b0") ) - Abc_LatchSetInit0( pNode ); - else if ( !strcmp(pEquation, "1") || !strcmp(pEquation, "1\'b1") ) - Abc_LatchSetInit1( pNode ); -// else if ( !strcmp(pEquation, "2") ) -// Abc_LatchSetInitDc( pNode ); - else + // 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 + if ( Ver_StreamPopChar(p) != '(' ) + { + 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 .).", Mio_GateReadName(pGate) ); + Ver_ParsePrintErrorMessage( pMan ); + return 0; + } + + // parse the formal name + pWord = Ver_ParseGetName( pMan ); + if ( pWord == NULL ) + return 0; + + // make sure that the formal name is the same as the gate's + if ( Mio_GateReadInputs(pGate) == Abc_ObjFaninNum(pNode) ) + { + 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, Mio_GateReadName(pGate) ); + Ver_ParsePrintErrorMessage( pMan ); + return 0; + } + + // parse the actual name + pWord = Ver_ParseGetName( pMan ); + if ( pWord == NULL ) + return 0; + // check if the name is complemented + assert( pWord[0] != '~' ); +/* + fCompl = (pWord[0] == '~'); + if ( fCompl ) + { + fComplUsed = 1; + 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 %s is missing.", pWord ); + Ver_ParsePrintErrorMessage( pMan ); + return 0; + } + + // close the paranthesis + if ( Ver_StreamPopChar(p) != ')' ) + { + sprintf( pMan->sError, "Cannot formal parameter %s of gate %s (expected closing paranthesis).", pWord, Mio_GateReadName(pGate) ); + Ver_ParsePrintErrorMessage( pMan ); + return 0; + } + + // add the fanin + if ( Mio_GateReadInputs(pGate) == Abc_ObjFaninNum(pNode) ) + Abc_ObjAddFanin( pNetActual, pNode ); // fanout + else + 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, "Incorrect initial value of the latch %s.", Abc_ObjName(pNet) ); + sprintf( pMan->sError, "Cannot formal parameter %s of gate %s (expected closing paranthesis).", pWord, Mio_GateReadName(pGate) ); Ver_ParsePrintErrorMessage( pMan ); return 0; } - // remove the last symbol - Symbol = Ver_StreamPopChar(p); - assert( Symbol == ';' ); - // quit if only one directive - if ( fStopAfterOne ) - break; + Ver_ParseSkipComments( pMan ); + + // get the next pin + pGatePin = Mio_PinReadNext(pGatePin); + } + + // check that the gate as the same number of input + if ( !(Abc_ObjFaninNum(pNode) == Mio_GateReadInputs(pGate) && Abc_ObjFanoutNum(pNode) == 1) ) + { + sprintf( pMan->sError, "Parsing of gate %s has failed.", Mio_GateReadName(pGate) ); + 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 gate %s (expected closing semicolumn).", Mio_GateReadName(pGate) ); + Ver_ParsePrintErrorMessage( pMan ); + return 0; } return 1; } @@ -839,40 +1227,42 @@ int Ver_ParseInitial( Ver_Man_t * pMan ) SeeAlso [] ***********************************************************************/ -int Ver_ParseGate( Ver_Man_t * pMan, Abc_Ntk_t * pNtkGate ) +int Ver_ParseBox( Ver_Man_t * pMan, Abc_Ntk_t * pNtk, Abc_Ntk_t * pNtkBox ) { Ver_Stream_t * p = pMan->pReader; - Abc_Ntk_t * pNtk = pMan->pNtkCur; + Vec_Ptr_t * vNetPairs; 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; + char * pWord, Symbol; + 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; - // this is gate name - throw it away - pGateName = pWord; + + // 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 gate %s (expected opening paranthesis).", pNtkGate->pName ); + sprintf( pMan->sError, "Cannot parse gate %s (expected opening paranthesis).", Abc_ObjName(pNode) ); Ver_ParsePrintErrorMessage( pMan ); return 0; } + // parse pairs of formal/actural inputs + vNetPairs = Vec_PtrAlloc( 16 ); + pNode->pCopy = (Abc_Obj_t *)vNetPairs; 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 .).", Abc_ObjName(pNode) ); Ver_ParsePrintErrorMessage( pMan ); return 0; } @@ -882,21 +1272,13 @@ int Ver_ParseGate( Ver_Man_t * pMan, Abc_Ntk_t * pNtkGate ) 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 ) - { - sprintf( pMan->sError, "Formal net is missing in gate %s.", pWord ); - Ver_ParsePrintErrorMessage( pMan ); - return 0; - } + pNetFormal = Abc_NtkFindOrCreateNet( pNtkBox, pWord ); + Vec_PtrPush( vNetPairs, pNetFormal ); // 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, Abc_ObjName(pNode)); Ver_ParsePrintErrorMessage( pMan ); return 0; } @@ -905,43 +1287,41 @@ int Ver_ParseGate( Ver_Man_t * pMan, Abc_Ntk_t * pNtkGate ) pWord = Ver_ParseGetName( pMan ); if ( pWord == NULL ) return 0; - // check if the name is complemented - fCompl = (pWord[0] == '~'); - if ( fCompl ) + // consider the case of empty name + fCompl = 0; + if ( pWord[0] == 0 ) { - fComplUsed = 1; - pWord++; - if ( pMan->pNtkCur->pData == NULL ) - pMan->pNtkCur->pData = Extra_MmFlexStart(); + // remove the formal net +// Vec_PtrPop( vNetPairs ); + pNetActual = Abc_NtkCreateObj( pNtk, ABC_OBJ_NET ); } - // get the actual net - pNetActual = Abc_NtkFindNet( pMan->pNtkCur, pWord ); - if ( pNetActual == NULL ) + else { - sprintf( pMan->sError, "Actual net is missing in gate %s.", pWord ); - Ver_ParsePrintErrorMessage( pMan ); - return 0; +/* + // 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, pNtkGate->pName ); - 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 ); - } - else - { - sprintf( pMan->sError, "Cannot match formal net %s with PI or PO of the gate %s.", pWord, pNtkGate->pName ); + sprintf( pMan->sError, "Cannot formal parameter %s of gate %s (expected closing paranthesis).", pWord, Abc_ObjName(pNode) ); Ver_ParsePrintErrorMessage( pMan ); return 0; } @@ -954,7 +1334,7 @@ int Ver_ParseGate( Ver_Man_t * pMan, Abc_Ntk_t * pNtkGate ) // 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, Abc_ObjName(pNode) ); Ver_ParsePrintErrorMessage( pMan ); return 0; } @@ -965,160 +1345,277 @@ int Ver_ParseGate( Ver_Man_t * pMan, Abc_Ntk_t * pNtkGate ) Ver_ParseSkipComments( pMan ); if ( Ver_StreamPopChar(p) != ';' ) { - sprintf( pMan->sError, "Cannot read gate %s (expected closing semicolumn).", pNtkGate->pName ); + sprintf( pMan->sError, "Cannot read gate %s (expected closing semicolumn).", Abc_ObjName(pNode) ); 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; - } -*/ + return 1; +} - // allocate memory to remember the phase - pPolarity = NULL; - if ( fComplUsed ) +/**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 ) { - int nBytes = 4 * Abc_BitWordNum( Abc_NtkPiNum(pNtkGate) ); - pPolarity = (unsigned *)Extra_MmFlexEntryFetch( pMan->pNtkCur->pData, nBytes ); - memset( pPolarity, 0, nBytes ); + // 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) ); } - // 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 ) + + // make sure all PI nets are assigned + Abc_NtkForEachPi( pNtkBox, pTerm, i ) { - if ( pPolarity && Abc_ObjIsComplement(pObj->pCopy) ) + if ( Abc_ObjFanout0(pTerm)->pCopy == NULL ) { - Abc_InfoSetBit( pPolarity, i ); - pObj->pCopy = Abc_ObjRegular( pObj->pCopy ); + 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; } - assert( !Abc_ObjIsComplement(pObj->pCopy) ); -// Abc_ObjAddFanin( pNode, pObj->pCopy ); - pTerm = Abc_NtkCreateBi( pNtk ); - Abc_ObjAddFanin( pTerm, pObj->pCopy ); - Abc_ObjAddFanin( pNode, pTerm ); + pTermNew = Abc_NtkCreateBi( pNtk ); + Abc_ObjAddFanin( pBox, pTermNew ); + Abc_ObjAddFanin( pTermNew, Abc_ObjFanout0(pTerm)->pCopy ); } - // connect to fanout nets - Abc_NtkForEachPo( pNtkGate, pObj, i ) + + // create fanins of the box + Abc_NtkForEachPo( pNtkBox, pTerm, 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 ); + 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 [Parses one directive.] + Synopsis [Attaches the boxes to the network.] - Description [] + Description [Makes sure that the undefined boxes are connected correctly.] SideEffects [] SeeAlso [] ***********************************************************************/ -int Ver_ParseGateStandard( Ver_Man_t * pMan, Ver_GateType_t GateType ) +int Vec_ParseAttachBoxes( Ver_Man_t * pMan ) { - Ver_Stream_t * p = pMan->pReader; - Hop_Man_t * pAig = pMan->pNtkCur->pManFunc; - Abc_Obj_t * pNet, * pNode; - char * pWord, Symbol; - // this is gate name - throw it away - if ( Ver_StreamPopChar(p) != '(' ) + 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 ) { - sprintf( pMan->sError, "Cannot parse a standard gate (expected opening paranthesis)." ); - Ver_ParsePrintErrorMessage( pMan ); - return 0; + Abc_NtkForEachBlackbox( pNtk, pBox, k ) + { + if ( pBox->pData && Ver_NtkIsDefined(pBox->pData) ) + if ( !Ver_ParseConnectBox( pMan, pBox ) ) + return 0; + } } - Ver_ParseSkipComments( pMan ); - // create the node - pNode = Abc_NtkCreateNode( pMan->pNtkCur ); - // parse pairs of formal/actural inputs - while ( 1 ) + + // 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 ) { - // parse the output 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 ) + assert( pNtk->pData == NULL ); + pNtk->pData = NULL; + } + Vec_PtrForEachEntry( pMan->pDesign->vModules, pNtk, i ) + Abc_NtkForEachBlackbox( pNtk, pBox, k ) { - sprintf( pMan->sError, "Net is missing in gate %s.", pWord ); - Ver_ParsePrintErrorMessage( pMan ); - return 0; + if ( pBox->pData == NULL ) + continue; + pNtkBox = pBox->pData; + pNtkBox->pData = (void *)((int)pNtkBox->pData + 1); } - // 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 != ',' ) + + // 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 ) { - sprintf( pMan->sError, "Cannot parse a standard gate %s (expected closing paranthesis).", Abc_ObjName(Abc_ObjFanout0(pNode)) ); - Ver_ParsePrintErrorMessage( pMan ); - return 0; + 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 ); + } } - Ver_ParseSkipComments( pMan ); } - if ( (GateType == VER_GATE_BUF || GateType == VER_GATE_NOT) && Abc_ObjFaninNum(pNode) != 1 ) + + // for each pivot net, find the driver + Vec_PtrForEachEntry( vPivots, pNetAct, i ) { - sprintf( pMan->sError, "Buffer or interver with multiple fanouts %s (currently not supported).", Abc_ObjName(Abc_ObjFanout0(pNode)) ); - Ver_ParsePrintErrorMessage( pMan ); - return 0; + 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 ); } - // check if it is the end of gate - Ver_ParseSkipComments( pMan ); - if ( Ver_StreamPopChar(p) != ';' ) + // for each pivot net, create driver + Vec_PtrForEachEntry( vPivots, pNetDr, i ) { - sprintf( pMan->sError, "Cannot read standard gate %s (expected closing semicolumn).", Abc_ObjName(Abc_ObjFanout0(pNode)) ); - Ver_ParsePrintErrorMessage( pMan ); - return 0; + 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; + } } - // 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; } @@ -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(),;" ); -- cgit v1.2.3