From 0e57e953062cd2d97573d8428f6f77853ba8535e Mon Sep 17 00:00:00 2001 From: Alan Mishchenko Date: Fri, 3 Mar 2006 08:01:00 -0800 Subject: Version abc60303 --- src/base/abc/abc.h | 29 +- src/base/abc/abcAig.c | 2 + src/base/abc/abcFunc.c | 13 +- src/base/abc/abcInt.h | 4 +- src/base/abc/abcNames.c | 33 ++ src/base/abc/abcNetlist.c | 8 +- src/base/abc/abcNtk.c | 58 +++ src/base/abc/abcObj.c | 13 +- src/base/abci/abc.c | 328 +++++++++------- src/base/abci/abcAuto.c | 2 +- src/base/abci/abcClpBdd.c | 46 ++- src/base/abci/abcCut.c | 42 --- src/base/abci/abcDsd.c | 2 +- src/base/abci/abcEspresso.c | 2 +- src/base/abci/abcFxu.c | 2 +- src/base/abci/abcMap.c | 4 +- src/base/abci/abcMiter.c | 4 +- src/base/abci/abcNewAig.c | 2 +- src/base/abci/abcNtbdd.c | 26 +- src/base/abci/abcPrint.c | 2 +- src/base/abci/abcProve.c | 53 ++- src/base/abci/abcReconv.c | 6 +- src/base/abci/abcRenode.c | 31 +- src/base/abci/abcRestruct.c | 8 +- src/base/abci/abcResub.c | 801 ++++++++++++++++++++++++++++++++++++++++ src/base/abci/abcSat.c | 4 + src/base/abci/abcStrash.c | 4 +- src/base/abci/abcSweep.c | 2 +- src/base/abci/abcSymm.c | 2 +- src/base/abci/abcUnate.c | 2 +- src/base/abci/abcUnreach.c | 4 +- src/base/abci/abcVanEijk.c | 26 +- src/base/abci/abcVanImp.c | 25 +- src/base/abci/abcVerify.c | 6 +- src/base/abci/module.make | 2 + src/base/cmd/cmd.c | 4 +- src/base/cmd/cmd.h | 12 +- src/base/io/io.c | 105 +++++- src/base/io/io.h | 12 +- src/base/io/ioInt.h | 4 +- src/base/io/ioWriteBlif.c | 2 +- src/base/io/ioWriteDot.c | 2 +- src/base/io/ioWritePla.c | 19 +- src/base/main/main.h | 12 +- src/base/main/mainInt.h | 4 +- src/base/seq/seq.h | 12 +- src/base/seq/seqInt.h | 12 +- src/base/seq/seqRetCore.c | 2 +- src/bdd/dsd/dsd.h | 12 +- src/bdd/dsd/dsdInt.h | 4 +- src/bdd/parse/parse.h | 3 +- src/bdd/parse/parseInt.h | 3 +- src/bdd/reo/reo.h | 12 +- src/generic.h | 12 +- src/map/fpga/fpga.h | 10 +- src/map/fpga/fpgaInt.h | 4 +- src/map/fpga/fpgaTruth.c | 3 +- src/map/mapper/mapper.h | 11 +- src/map/mapper/mapperInt.h | 4 +- src/map/mio/mio.h | 12 +- src/map/mio/mioInt.h | 4 +- src/map/pga/pga.h | 12 +- src/map/pga/pgaInt.h | 4 +- src/map/super/super.h | 11 +- src/map/super/superInt.h | 4 +- src/misc/extra/extra.h | 8 + src/misc/mvc/mvc.h | 4 +- src/misc/st/st.h | 8 + src/misc/st/stmm.h | 8 + src/misc/util/util_hack.h | 8 + src/misc/vec/vec.h | 12 +- src/misc/vec/vecInt.h | 4 +- src/misc/vec/vecPtr.h | 4 +- src/misc/vec/vecStr.h | 4 +- src/misc/vec/vecVec.h | 4 +- src/opt/cut/cut.h | 12 +- src/opt/cut/cutInt.h | 4 +- src/opt/cut/cutList.h | 4 +- src/opt/dec/dec.h | 12 +- src/opt/dec/decAbc.c | 5 +- src/opt/fxu/fxu.h | 12 +- src/opt/fxu/fxuInt.h | 3 +- src/opt/rwr/rwr.h | 12 +- src/opt/sim/sim.h | 12 +- src/opt/xyz/xyz.h | 14 + src/sat/aig/aig.h | 12 +- src/sat/asat/asatmem.h | 4 +- src/sat/asat/solver.h | 8 + src/sat/csat/csat_apis.h | 8 +- src/sat/fraig/fraig.h | 12 +- src/sat/fraig/fraigApi.c | 2 + src/sat/fraig/fraigInt.h | 4 +- src/sat/msat/msat.h | 11 +- src/sat/msat/msatSolverCore.c | 2 +- src/sat/msat/msatSolverSearch.c | 2 +- 95 files changed, 1789 insertions(+), 355 deletions(-) create mode 100644 src/base/abci/abcResub.c (limited to 'src') diff --git a/src/base/abc/abc.h b/src/base/abc/abc.h index e36f133e..c68c74e2 100644 --- a/src/base/abc/abc.h +++ b/src/base/abc/abc.h @@ -21,6 +21,10 @@ #ifndef __ABC_H__ #define __ABC_H__ +#ifdef __cplusplus +extern "C" { +#endif + //////////////////////////////////////////////////////////////////////// /// INCLUDES /// //////////////////////////////////////////////////////////////////////// @@ -435,7 +439,7 @@ extern bool Abc_NtkDoCheck( Abc_Ntk_t * pNtk ); extern bool Abc_NtkCheckObj( Abc_Ntk_t * pNtk, Abc_Obj_t * pObj ); extern bool Abc_NtkCompareSignals( Abc_Ntk_t * pNtk1, Abc_Ntk_t * pNtk2, int fComb ); /*=== abcCollapse.c ==========================================================*/ -extern Abc_Ntk_t * Abc_NtkCollapse( Abc_Ntk_t * pNtk, int fVerbose ); +extern Abc_Ntk_t * Abc_NtkCollapse( Abc_Ntk_t * pNtk, int fBddSizeMax, int fDualRail, int fVerbose ); /*=== abcCut.c ==========================================================*/ extern void * Abc_NodeGetCutsRecursive( void * p, Abc_Obj_t * pObj, int fMulti ); extern void * Abc_NodeGetCuts( void * p, Abc_Obj_t * pObj, int fMulti ); @@ -471,7 +475,7 @@ extern void Abc_NtkFraigStoreClean(); extern int Abc_NtkSopToBdd( Abc_Ntk_t * pNtk ); extern DdNode * Abc_ConvertSopToBdd( DdManager * dd, char * pSop ); extern char * Abc_ConvertBddToSop( Extra_MmFlex_t * pMan, DdManager * dd, DdNode * bFuncOn, DdNode * bFuncOnDc, int nFanins, Vec_Str_t * vCube, int fMode ); -extern int Abc_NtkBddToSop( Abc_Ntk_t * pNtk ); +extern int Abc_NtkBddToSop( Abc_Ntk_t * pNtk, int fDirect ); extern void Abc_NodeBddToCnf( Abc_Obj_t * pNode, Extra_MmFlex_t * pMmMan, Vec_Str_t * vCube, char ** ppSop0, char ** ppSop1 ); extern int Abc_CountZddCubes( DdManager * dd, DdNode * zCover ); extern void Abc_NtkLogicMakeDirectSops( Abc_Ntk_t * pNtk ); @@ -528,6 +532,7 @@ extern char * Abc_NtkLogicStoreName( Abc_Obj_t * pNodeNew, char * pN extern char * Abc_NtkLogicStoreNamePlus( Abc_Obj_t * pNodeNew, char * pNameOld, char * pSuffix ); extern void Abc_NtkCreateCioNamesTable( Abc_Ntk_t * pNtk ); extern void Abc_NtkDupCioNamesTable( Abc_Ntk_t * pNtk, Abc_Ntk_t * pNtkNew ); +extern void Abc_NtkDupCioNamesTableDual( Abc_Ntk_t * pNtk, Abc_Ntk_t * pNtkNew ); extern Vec_Ptr_t * Abc_NodeGetFaninNames( Abc_Obj_t * pNode ); extern Vec_Ptr_t * Abc_NodeGetFakeNames( int nNames ); extern void Abc_NodeFreeNames( Vec_Ptr_t * vNames ); @@ -541,7 +546,7 @@ extern void Abc_NtkShortNames( Abc_Ntk_t * pNtk ); extern stmm_table * Abc_NtkNamesToTable( Vec_Ptr_t * vNodes ); /*=== abcNetlist.c ==========================================================*/ extern Abc_Ntk_t * Abc_NtkNetlistToLogic( Abc_Ntk_t * pNtk ); -extern Abc_Ntk_t * Abc_NtkLogicToNetlist( 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 ); @@ -549,12 +554,12 @@ extern Abc_Ntk_t * Abc_NtkAigToLogicSopBench( 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 ); -extern DdManager * Abc_NtkGlobalBdds( Abc_Ntk_t * pNtk, int fLatchOnly ); +extern DdManager * Abc_NtkGlobalBdds( Abc_Ntk_t * pNtk, int fBddSizeMax, int fLatchOnly ); extern void Abc_NtkFreeGlobalBdds( Abc_Ntk_t * pNtk ); /*=== abcNtk.c ==========================================================*/ extern Abc_Ntk_t * Abc_NtkAlloc( Abc_NtkType_t Type, Abc_NtkFunc_t Func ); extern Abc_Ntk_t * Abc_NtkStartFrom( Abc_Ntk_t * pNtk, Abc_NtkType_t Type, Abc_NtkFunc_t Func ); -extern Abc_Ntk_t * Abc_NtkStartFromSeq( Abc_Ntk_t * pNtk, Abc_NtkType_t Type, Abc_NtkFunc_t Func ); +extern Abc_Ntk_t * Abc_NtkStartFromDual( Abc_Ntk_t * pNtk, Abc_NtkType_t Type, Abc_NtkFunc_t Func ); extern void Abc_NtkFinalize( Abc_Ntk_t * pNtk, Abc_Ntk_t * pNtkNew ); extern void Abc_NtkFinalizeRegular( Abc_Ntk_t * pNtk, Abc_Ntk_t * pNtkNew ); extern void Abc_NtkFinalizeLatches( Abc_Ntk_t * pNtk ); @@ -599,7 +604,7 @@ extern void Abc_NodeMffsConeSupp( Abc_Obj_t * pNode, Vec_Ptr_t * v extern int Abc_NodeDeref_rec( Abc_Obj_t * pNode ); extern int Abc_NodeRef_rec( Abc_Obj_t * pNode ); /*=== abcRenode.c ==========================================================*/ -extern Abc_Ntk_t * Abc_NtkRenode( Abc_Ntk_t * pNtk, int nThresh, int nFaninMax, int fCnf, int fMulti, int fSimple ); +extern Abc_Ntk_t * Abc_NtkRenode( Abc_Ntk_t * pNtk, int nThresh, int nFaninMax, int fCnf, int fMulti, int fSimple, int fFactor ); extern DdNode * Abc_NtkRenodeDeriveBdd( DdManager * dd, Abc_Obj_t * pNodeOld, Vec_Ptr_t * vFaninsOld ); /*=== abcSat.c ==========================================================*/ extern int Abc_NtkMiterSat( Abc_Ntk_t * pNtk, int nConfLimit, int nImpLimit, int fVerbose ); @@ -698,10 +703,16 @@ extern Vec_Int_t * Abc_NtkFanoutCounts( Abc_Ntk_t * pNtk ); extern Vec_Ptr_t * Abc_NtkCollectObjects( Abc_Ntk_t * pNtk ); extern Vec_Int_t * Abc_NtkGetCiIds( Abc_Ntk_t * pNtk ); extern void Abc_NtkReassignIds( Abc_Ntk_t * pNtk ); +/*=== abcVerify.c ==========================================================*/ +extern int * Abc_NtkVerifyGetCleanModel( Abc_Ntk_t * pNtk, int nFrames ); +extern int * Abc_NtkVerifySimulatePattern( Abc_Ntk_t * pNtk, int * pModel ); -//////////////////////////////////////////////////////////////////////// -/// END OF FILE /// -//////////////////////////////////////////////////////////////////////// +#ifdef __cplusplus +} +#endif #endif +//////////////////////////////////////////////////////////////////////// +/// END OF FILE /// +//////////////////////////////////////////////////////////////////////// diff --git a/src/base/abc/abcAig.c b/src/base/abc/abcAig.c index e5f39127..f2f50f77 100644 --- a/src/base/abc/abcAig.c +++ b/src/base/abc/abcAig.c @@ -295,6 +295,7 @@ Abc_Obj_t * Abc_AigAndCreate( Abc_Aig_t * pMan, Abc_Obj_t * p0, Abc_Obj_t * p1 ) // create the cuts if defined // if ( pAnd->pNtk->pManCut ) // Abc_NodeGetCuts( pAnd->pNtk->pManCut, pAnd ); + pAnd->pCopy = NULL; return pAnd; } @@ -331,6 +332,7 @@ Abc_Obj_t * Abc_AigAndCreateFrom( Abc_Aig_t * pMan, Abc_Obj_t * p0, Abc_Obj_t * // create the cuts if defined // if ( pAnd->pNtk->pManCut ) // Abc_NodeGetCuts( pAnd->pNtk->pManCut, pAnd ); + pAnd->pCopy = NULL; return pAnd; } diff --git a/src/base/abc/abcFunc.c b/src/base/abc/abcFunc.c index 2ab3842f..cb20cec3 100644 --- a/src/base/abc/abcFunc.c +++ b/src/base/abc/abcFunc.c @@ -195,20 +195,25 @@ void Abc_NtkLogicMakeDirectSops( Abc_Ntk_t * pNtk ) Synopsis [Converts the network from BDD to SOP representation.] - Description [] + Description [If the flag is set to 1, forces the direct phase of all covers.] SideEffects [] SeeAlso [] ***********************************************************************/ -int Abc_NtkBddToSop( Abc_Ntk_t * pNtk ) +int Abc_NtkBddToSop( Abc_Ntk_t * pNtk, int fDirect ) { Abc_Obj_t * pNode; DdManager * dd = pNtk->pManFunc; DdNode * bFunc; Vec_Str_t * vCube; - int i; + int i, fMode; + + if ( fDirect ) + fMode = 1; + else + fMode = -1; assert( Abc_NtkIsBddLogic(pNtk) ); Cudd_zddVarsFromBddVars( dd, 2 ); @@ -223,7 +228,7 @@ int Abc_NtkBddToSop( Abc_Ntk_t * pNtk ) { assert( pNode->pData ); bFunc = pNode->pData; - pNode->pData = Abc_ConvertBddToSop( pNtk->pManFunc, dd, bFunc, bFunc, Abc_ObjFaninNum(pNode), vCube, -1 ); + pNode->pData = Abc_ConvertBddToSop( pNtk->pManFunc, dd, bFunc, bFunc, Abc_ObjFaninNum(pNode), vCube, fMode ); if ( pNode->pData == NULL ) { Vec_StrFree( vCube ); diff --git a/src/base/abc/abcInt.h b/src/base/abc/abcInt.h index 967f5695..0e35e774 100644 --- a/src/base/abc/abcInt.h +++ b/src/base/abc/abcInt.h @@ -43,10 +43,10 @@ /// FUNCTION DECLARATIONS /// //////////////////////////////////////////////////////////////////////// +#endif + //////////////////////////////////////////////////////////////////////// /// END OF FILE /// //////////////////////////////////////////////////////////////////////// -#endif - diff --git a/src/base/abc/abcNames.c b/src/base/abc/abcNames.c index ccbd2c85..14f0b505 100644 --- a/src/base/abc/abcNames.c +++ b/src/base/abc/abcNames.c @@ -288,6 +288,39 @@ void Abc_NtkDupCioNamesTable( Abc_Ntk_t * pNtk, Abc_Ntk_t * pNtkNew ) Abc_NtkLogicStoreName( Abc_NtkLatch(pNtkNew,i), Abc_ObjName(pObj) ); } +/**Function************************************************************* + + Synopsis [Duplicates the name arrays.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Abc_NtkDupCioNamesTableDual( Abc_Ntk_t * pNtk, Abc_Ntk_t * pNtkNew ) +{ + Abc_Obj_t * pObj; + int i; + assert( Abc_NtkPiNum(pNtk) == Abc_NtkPiNum(pNtkNew) ); + assert( Abc_NtkPoNum(pNtk) * 2 == Abc_NtkPoNum(pNtkNew) ); + assert( Abc_NtkLatchNum(pNtk) == Abc_NtkLatchNum(pNtkNew) ); + assert( st_count(pNtk->tObj2Name) > 0 ); + assert( st_count(pNtkNew->tObj2Name) == 0 ); + // copy the CI/CO names if given + Abc_NtkForEachPi( pNtk, pObj, i ) + Abc_NtkLogicStoreName( Abc_NtkPi(pNtkNew,i), Abc_ObjName(pObj) ); + Abc_NtkForEachPo( pNtk, pObj, i ) + { + Abc_NtkLogicStoreNamePlus( Abc_NtkPo(pNtkNew,2*i+0), Abc_ObjName(pObj), "_pos" ); + Abc_NtkLogicStoreNamePlus( Abc_NtkPo(pNtkNew,2*i+1), Abc_ObjName(pObj), "_neg" ); + } + if ( !Abc_NtkIsSeq(pNtk) ) + Abc_NtkForEachLatch( pNtk, pObj, i ) + Abc_NtkLogicStoreName( Abc_NtkLatch(pNtkNew,i), Abc_ObjName(pObj) ); +} + /**Function************************************************************* Synopsis [Gets fanin node names.] diff --git a/src/base/abc/abcNetlist.c b/src/base/abc/abcNetlist.c index 65cc6e2e..d289cd35 100644 --- a/src/base/abc/abcNetlist.c +++ b/src/base/abc/abcNetlist.c @@ -83,7 +83,7 @@ Abc_Ntk_t * Abc_NtkNetlistToLogic( Abc_Ntk_t * pNtk ) SeeAlso [] ***********************************************************************/ -Abc_Ntk_t * Abc_NtkLogicToNetlist( Abc_Ntk_t * pNtk ) +Abc_Ntk_t * Abc_NtkLogicToNetlist( Abc_Ntk_t * pNtk, int fDirect ) { Abc_Ntk_t * pNtkNew, * pNtkTemp; assert( Abc_NtkIsLogic(pNtk) || Abc_NtkIsStrash(pNtk) || Abc_NtkIsSeq(pNtk) ); @@ -101,7 +101,7 @@ Abc_Ntk_t * Abc_NtkLogicToNetlist( Abc_Ntk_t * pNtk ) } else if ( Abc_NtkIsBddLogic(pNtk) ) { - Abc_NtkBddToSop(pNtk); + Abc_NtkBddToSop(pNtk, fDirect); pNtkNew = Abc_NtkLogicSopToNetlist( pNtk ); Abc_NtkSopToBdd(pNtk); } @@ -157,7 +157,7 @@ Abc_Ntk_t * Abc_NtkLogicSopToNetlist( Abc_Ntk_t * pNtk ) assert( Abc_NtkLogicHasSimpleCos(pNtk) ); if ( Abc_NtkIsBddLogic(pNtk) ) - Abc_NtkBddToSop(pNtk); + Abc_NtkBddToSop(pNtk,0); // start the netlist by creating PI/PO/Latch objects pNtkNew = Abc_NtkStartFrom( pNtk, ABC_NTK_NETLIST, pNtk->ntkFunc ); @@ -220,7 +220,7 @@ 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 ); + pNtkNew->pExdc = Abc_NtkLogicToNetlist( pNtk->pExdc, 0 ); if ( !Abc_NtkCheck( pNtkNew ) ) fprintf( stdout, "Abc_NtkLogicSopToNetlist(): Network check has failed.\n" ); return pNtkNew; diff --git a/src/base/abc/abcNtk.c b/src/base/abc/abcNtk.c index 31b4c5f4..0692819b 100644 --- a/src/base/abc/abcNtk.c +++ b/src/base/abc/abcNtk.c @@ -146,6 +146,64 @@ Abc_Ntk_t * Abc_NtkStartFrom( Abc_Ntk_t * pNtk, Abc_NtkType_t Type, Abc_NtkFunc_ return pNtkNew; } +/**Function************************************************************* + + Synopsis [Starts a new network using existing network as a model.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Abc_Ntk_t * Abc_NtkStartFromDual( Abc_Ntk_t * pNtk, Abc_NtkType_t Type, Abc_NtkFunc_t Func ) +{ + Abc_Ntk_t * pNtkNew; + Abc_Obj_t * pObj, * pObjNew; + int i; + if ( pNtk == NULL ) + return NULL; + // start the network + pNtkNew = Abc_NtkAlloc( Type, Func ); + // duplicate the name and the spec + pNtkNew->pName = Extra_UtilStrsav(pNtk->pName); + pNtkNew->pSpec = NULL; + // clean the node copy fields + Abc_NtkForEachNode( pNtk, pObj, i ) + pObj->pCopy = NULL; + // map the constant nodes + if ( Abc_NtkConst1(pNtk) ) + Abc_NtkConst1(pNtk)->pCopy = Abc_NtkConst1(pNtkNew); + // clone the PIs/POs/latches + Abc_NtkForEachPi( pNtk, pObj, i ) + Abc_NtkDupObj(pNtkNew, pObj); + Abc_NtkForEachPo( pNtk, pObj, i ) + { + Abc_NtkDupObj(pNtkNew, pObj); + pObjNew = pObj->pCopy; + Abc_NtkDupObj(pNtkNew, pObj); + // connect second to the first + pObjNew->pCopy = pObj->pCopy; + // collect first to old + pObj->pCopy = pObjNew; + } + Abc_NtkForEachLatch( pNtk, pObj, i ) + { + pObjNew = Abc_NtkDupObj(pNtkNew, pObj); + Vec_PtrPush( pNtkNew->vCis, pObjNew ); + Vec_PtrPush( pNtkNew->vCos, pObjNew ); + } + // transfer the names + Abc_NtkDupCioNamesTableDual( pNtk, pNtkNew ); +// Abc_ManTimeDup( pNtk, pNtkNew ); + // check that the CI/CO/latches are copied correctly + assert( Abc_NtkCiNum(pNtk) == Abc_NtkCiNum(pNtkNew) ); + assert( Abc_NtkCoNum(pNtk)* 2 == Abc_NtkCoNum(pNtkNew) ); + assert( Abc_NtkLatchNum(pNtk) == Abc_NtkLatchNum(pNtkNew) ); + return pNtkNew; +} + /**Function************************************************************* Synopsis [Finalizes the network using the existing network as a model.] diff --git a/src/base/abc/abcObj.c b/src/base/abc/abcObj.c index 481b069f..d6adfeb2 100644 --- a/src/base/abc/abcObj.c +++ b/src/base/abc/abcObj.c @@ -227,7 +227,18 @@ void Abc_NtkDeleteObj( Abc_Obj_t * pObj ) { pNtk->nLatches--; } - else + else if ( Abc_ObjIsPo(pObj) ) + { + assert( Abc_NtkPoNum(pObj->pNtk) == 1 ); + Vec_PtrRemove( pObj->pNtk->vCos, pObj ); + pObj->pNtk->nPos--; + // add the name to the table + if ( !stmm_delete( pObj->pNtk->tObj2Name, (char **)&pObj, NULL ) ) + { + assert( 0 ); // the PO is not in the table + } + } + else assert( 0 ); // recycle the net itself Abc_ObjRecycle( pObj ); diff --git a/src/base/abci/abc.c b/src/base/abci/abc.c index d2422b64..8927279f 100644 --- a/src/base/abci/abc.c +++ b/src/base/abci/abc.c @@ -71,7 +71,6 @@ static int Abc_CommandSop ( Abc_Frame_t * pAbc, int argc, char ** argv static int Abc_CommandBdd ( Abc_Frame_t * pAbc, int argc, char ** argv ); static int Abc_CommandReorder ( Abc_Frame_t * pAbc, int argc, char ** argv ); static int Abc_CommandMuxes ( Abc_Frame_t * pAbc, int argc, char ** argv ); -static int Abc_CommandSat ( Abc_Frame_t * pAbc, int argc, char ** argv ); static int Abc_CommandExtSeqDcs ( Abc_Frame_t * pAbc, int argc, char ** argv ); static int Abc_CommandOneOutput ( Abc_Frame_t * pAbc, int argc, char ** argv ); static int Abc_CommandOneNode ( Abc_Frame_t * pAbc, int argc, char ** argv ); @@ -112,6 +111,7 @@ static int Abc_CommandSeqCleanup ( Abc_Frame_t * pAbc, int argc, char ** argv static int Abc_CommandCec ( Abc_Frame_t * pAbc, int argc, char ** argv ); static int Abc_CommandSec ( Abc_Frame_t * pAbc, int argc, char ** argv ); +static int Abc_CommandSat ( Abc_Frame_t * pAbc, int argc, char ** argv ); static int Abc_CommandProve ( Abc_Frame_t * pAbc, int argc, char ** argv ); //////////////////////////////////////////////////////////////////////// @@ -173,7 +173,6 @@ void Abc_Init( Abc_Frame_t * pAbc ) Cmd_CommandAdd( pAbc, "Various", "bdd", Abc_CommandBdd, 0 ); Cmd_CommandAdd( pAbc, "Various", "reorder", Abc_CommandReorder, 0 ); Cmd_CommandAdd( pAbc, "Various", "muxes", Abc_CommandMuxes, 1 ); - Cmd_CommandAdd( pAbc, "Various", "sat", Abc_CommandSat, 0 ); Cmd_CommandAdd( pAbc, "Various", "ext_seq_dcs", Abc_CommandExtSeqDcs, 0 ); Cmd_CommandAdd( pAbc, "Various", "cone", Abc_CommandOneOutput, 1 ); Cmd_CommandAdd( pAbc, "Various", "node", Abc_CommandOneNode, 1 ); @@ -214,6 +213,7 @@ void Abc_Init( Abc_Frame_t * pAbc ) Cmd_CommandAdd( pAbc, "Verification", "cec", Abc_CommandCec, 0 ); Cmd_CommandAdd( pAbc, "Verification", "sec", Abc_CommandSec, 0 ); + Cmd_CommandAdd( pAbc, "Verification", "sat", Abc_CommandSat, 0 ); Cmd_CommandAdd( pAbc, "Verification", "prove", Abc_CommandProve, 1 ); // Rwt_Man4ExploreStart(); @@ -1594,6 +1594,8 @@ int Abc_CommandCollapse( Abc_Frame_t * pAbc, int argc, char ** argv ) { FILE * pOut, * pErr; Abc_Ntk_t * pNtk, * pNtkRes; + int fBddSizeMax; + int fDualRail; int c; pNtk = Abc_FrameReadNtk(pAbc); @@ -1601,11 +1603,27 @@ int Abc_CommandCollapse( Abc_Frame_t * pAbc, int argc, char ** argv ) pErr = Abc_FrameReadErr(pAbc); // set defaults + fDualRail = 0; + fBddSizeMax = 1000000; Extra_UtilGetoptReset(); - while ( ( c = Extra_UtilGetopt( argc, argv, "h" ) ) != EOF ) + while ( ( c = Extra_UtilGetopt( argc, argv, "Bdh" ) ) != EOF ) { switch ( c ) { + case 'B': + if ( globalUtilOptind >= argc ) + { + fprintf( pErr, "Command line switch \"-B\" should be followed by an integer.\n" ); + goto usage; + } + fBddSizeMax = atoi(argv[globalUtilOptind]); + globalUtilOptind++; + if ( fBddSizeMax < 0 ) + goto usage; + break; + case 'd': + fDualRail ^= 1; + break; case 'h': goto usage; default: @@ -1627,11 +1645,11 @@ int Abc_CommandCollapse( Abc_Frame_t * pAbc, int argc, char ** argv ) // get the new network if ( Abc_NtkIsStrash(pNtk) ) - pNtkRes = Abc_NtkCollapse( pNtk, 1 ); + pNtkRes = Abc_NtkCollapse( pNtk, fBddSizeMax, fDualRail, 1 ); else { pNtk = Abc_NtkStrash( pNtk, 0, 0 ); - pNtkRes = Abc_NtkCollapse( pNtk, 1 ); + pNtkRes = Abc_NtkCollapse( pNtk, fBddSizeMax, fDualRail, 1 ); Abc_NtkDelete( pNtk ); } if ( pNtkRes == NULL ) @@ -1644,9 +1662,11 @@ int Abc_CommandCollapse( Abc_Frame_t * pAbc, int argc, char ** argv ) return 0; usage: - fprintf( pErr, "usage: collapse [-h]\n" ); - fprintf( pErr, "\t collapses the network by constructing global BDDs\n" ); - fprintf( pErr, "\t-h : print the command usage\n"); + fprintf( pErr, "usage: collapse [-B num] [-dh]\n" ); + fprintf( pErr, "\t collapses the network by constructing global BDDs\n" ); + fprintf( pErr, "\t-B num : limit on live BDD nodes during collapsing [default = %d]\n", fBddSizeMax ); + fprintf( pErr, "\t-d : toggles dual-rail collapsing mode [default = %s]\n", fDualRail? "yes": "no" ); + fprintf( pErr, "\t-h : print the command usage\n"); return 1; } @@ -1837,6 +1857,7 @@ int Abc_CommandRenode( Abc_Frame_t * pAbc, int argc, char ** argv ) int fCnf; int fMulti; int fSimple; + int fFactor; pNtk = Abc_FrameReadNtk(pAbc); pOut = Abc_FrameReadOut(pAbc); @@ -1848,8 +1869,9 @@ int Abc_CommandRenode( Abc_Frame_t * pAbc, int argc, char ** argv ) fCnf = 0; fMulti = 0; fSimple = 0; + fFactor = 0; Extra_UtilGetoptReset(); - while ( ( c = Extra_UtilGetopt( argc, argv, "TFmcsh" ) ) != EOF ) + while ( ( c = Extra_UtilGetopt( argc, argv, "TFmcsfh" ) ) != EOF ) { switch ( c ) { @@ -1884,6 +1906,9 @@ int Abc_CommandRenode( Abc_Frame_t * pAbc, int argc, char ** argv ) case 's': fSimple ^= 1; break; + case 'f': + fFactor ^= 1; + break; case 'h': goto usage; default: @@ -1903,7 +1928,7 @@ int Abc_CommandRenode( Abc_Frame_t * pAbc, int argc, char ** argv ) } // get the new network - pNtkRes = Abc_NtkRenode( pNtk, nThresh, nFaninMax, fCnf, fMulti, fSimple ); + pNtkRes = Abc_NtkRenode( pNtk, nThresh, nFaninMax, fCnf, fMulti, fSimple, fFactor ); if ( pNtkRes == NULL ) { fprintf( pErr, "Renoding has failed.\n" ); @@ -1914,7 +1939,7 @@ int Abc_CommandRenode( Abc_Frame_t * pAbc, int argc, char ** argv ) return 0; usage: - fprintf( pErr, "usage: renode [-T num] [-F num] [-cmsh]\n" ); + fprintf( pErr, "usage: renode [-T num] [-F num] [-msfch]\n" ); fprintf( pErr, "\t transforms an AIG into a logic network by creating larger nodes\n" ); fprintf( pErr, "\t-F num : the maximum fanin size after renoding [default = %d]\n", nFaninMax ); fprintf( pErr, "\t-T num : the threshold for AIG node duplication [default = %d]\n", nThresh ); @@ -1923,6 +1948,7 @@ usage: fprintf( pErr, "\t that is, if [(numFanouts(Node)-1) * size(MFFC(Node))] <= %d)\n", nThresh ); fprintf( pErr, "\t-m : creates multi-input AND graph [default = %s]\n", fMulti? "yes": "no" ); fprintf( pErr, "\t-s : creates a simple AIG (no renoding) [default = %s]\n", fSimple? "yes": "no" ); + fprintf( pErr, "\t-f : creates a factor-cut network [default = %s]\n", fFactor? "yes": "no" ); fprintf( pErr, "\t-c : performs renoding to derive the CNF [default = %s]\n", fCnf? "yes": "no" ); fprintf( pErr, "\t-h : print the command usage\n"); return 1; @@ -2852,6 +2878,7 @@ int Abc_CommandSop( Abc_Frame_t * pAbc, int argc, char ** argv ) { FILE * pOut, * pErr; Abc_Ntk_t * pNtk; + int fDirect; int c; pNtk = Abc_FrameReadNtk(pAbc); @@ -2859,11 +2886,15 @@ int Abc_CommandSop( Abc_Frame_t * pAbc, int argc, char ** argv ) pErr = Abc_FrameReadErr(pAbc); // set defaults + fDirect = 0; Extra_UtilGetoptReset(); - while ( ( c = Extra_UtilGetopt( argc, argv, "h" ) ) != EOF ) + while ( ( c = Extra_UtilGetopt( argc, argv, "dh" ) ) != EOF ) { switch ( c ) { + case 'd': + fDirect ^= 1; + break; case 'h': goto usage; default: @@ -2883,7 +2914,7 @@ int Abc_CommandSop( Abc_Frame_t * pAbc, int argc, char ** argv ) fprintf( pErr, "Converting to SOP is possible when node functions are BDDs.\n" ); return 1; } - if ( !Abc_NtkBddToSop( pNtk ) ) + if ( !Abc_NtkBddToSop( pNtk, fDirect ) ) { fprintf( pErr, "Converting to SOP has failed.\n" ); return 1; @@ -2891,8 +2922,9 @@ int Abc_CommandSop( Abc_Frame_t * pAbc, int argc, char ** argv ) return 0; usage: - fprintf( pErr, "usage: sop [-h]\n" ); + fprintf( pErr, "usage: sop [-dh]\n" ); fprintf( pErr, "\t converts node functions from BDD to SOP\n" ); + fprintf( pErr, "\t-d : toggles using both phases or only positive [default = %s]\n", fDirect? "direct": "both" ); fprintf( pErr, "\t-h : print the command usage\n"); return 1; } @@ -3084,130 +3116,6 @@ usage: return 1; } -/**Function************************************************************* - - Synopsis [] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -int Abc_CommandSat( Abc_Frame_t * pAbc, int argc, char ** argv ) -{ - FILE * pOut, * pErr; - Abc_Ntk_t * pNtk; - int c; - int RetValue; - int fVerbose; - int nConfLimit; - int nImpLimit; - int clk; - - pNtk = Abc_FrameReadNtk(pAbc); - pOut = Abc_FrameReadOut(pAbc); - pErr = Abc_FrameReadErr(pAbc); - - // set defaults - fVerbose = 0; - nConfLimit = 100000; - nImpLimit = 0; - Extra_UtilGetoptReset(); - while ( ( c = Extra_UtilGetopt( argc, argv, "CIvh" ) ) != EOF ) - { - switch ( c ) - { - case 'C': - if ( globalUtilOptind >= argc ) - { - fprintf( pErr, "Command line switch \"-C\" should be followed by an integer.\n" ); - goto usage; - } - nConfLimit = atoi(argv[globalUtilOptind]); - globalUtilOptind++; - if ( nConfLimit < 0 ) - goto usage; - break; - case 'I': - if ( globalUtilOptind >= argc ) - { - fprintf( pErr, "Command line switch \"-I\" should be followed by an integer.\n" ); - goto usage; - } - nImpLimit = atoi(argv[globalUtilOptind]); - globalUtilOptind++; - if ( nImpLimit < 0 ) - goto usage; - break; - case 'v': - fVerbose ^= 1; - break; - case 'h': - goto usage; - default: - goto usage; - } - } - - if ( pNtk == NULL ) - { - fprintf( pErr, "Empty network.\n" ); - return 1; - } - if ( Abc_NtkLatchNum(pNtk) > 0 ) - { - fprintf( stdout, "Currently can only solve the miter for combinational circuits.\n" ); - return 0; - } - if ( Abc_NtkIsSeq(pNtk) ) - { - fprintf( stdout, "This command cannot be applied to the sequential AIG.\n" ); - return 0; - } - - if ( Abc_NtkIsStrash(pNtk) ) - { - clk = clock(); - RetValue = Abc_NtkMiterSat( pNtk, nConfLimit, nImpLimit, fVerbose ); - if ( RetValue == -1 ) - printf( "UNDECIDED " ); - else if ( RetValue == 0 ) - printf( "SATISFIABLE " ); - else - printf( "UNSATISFIABLE " ); - //printf( "\n" ); - PRT( "Time", clock() - clk ); - } - else - { - Abc_Ntk_t * pTemp; - pTemp = Abc_NtkStrash( pNtk, 0, 0 ); - clk = clock(); - RetValue = Abc_NtkMiterSat( pTemp, nConfLimit, nImpLimit, fVerbose ); - if ( RetValue == -1 ) - printf( "UNDECIDED " ); - else if ( RetValue == 0 ) - printf( "SATISFIABLE " ); - else - printf( "UNSATISFIABLE " ); - //printf( "\n" ); - PRT( "Time", clock() - clk ); - Abc_NtkDelete( pTemp ); - } - return 0; - -usage: - fprintf( pErr, "usage: sat [-C num] [-I num] [-vh]\n" ); - fprintf( pErr, "\t solves the combinational miter\n" ); - fprintf( pErr, "\t-C num : limit on the number of conflicts [default = %d]\n", nConfLimit ); - fprintf( pErr, "\t-I num : limit on the number of implications [default = %d]\n", nImpLimit ); - fprintf( pErr, "\t-v : prints verbose information [default = %s]\n", fVerbose? "yes": "no" ); - fprintf( pErr, "\t-h : print the command usage\n"); - return 1; -} - /**Function************************************************************* @@ -4148,7 +4056,7 @@ int Abc_CommandTest( Abc_Frame_t * pAbc, int argc, char ** argv ) FILE * pOut, * pErr; Abc_Ntk_t * pNtk, * pNtkRes; int c; - extern Abc_Ntk_t * Abc_NtkNewAig( Abc_Ntk_t * pNtk ); +// extern Abc_Ntk_t * Abc_NtkNewAig( Abc_Ntk_t * pNtk ); pNtk = Abc_FrameReadNtk(pAbc); pOut = Abc_FrameReadOut(pAbc); @@ -4184,8 +4092,8 @@ int Abc_CommandTest( Abc_Frame_t * pAbc, int argc, char ** argv ) // run the command // pNtkRes = Abc_NtkMiterForCofactors( pNtk, 0, 0, -1 ); - pNtkRes = Abc_NtkNewAig( pNtk ); -// pNtkRes = NULL; +// pNtkRes = Abc_NtkNewAig( pNtk ); + pNtkRes = NULL; if ( pNtkRes == NULL ) { fprintf( pErr, "Command has failed.\n" ); @@ -6413,6 +6321,133 @@ usage: return 1; } +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Abc_CommandSat( Abc_Frame_t * pAbc, int argc, char ** argv ) +{ + FILE * pOut, * pErr; + Abc_Ntk_t * pNtk; + int c; + int RetValue; + int fVerbose; + int nConfLimit; + int nImpLimit; + int clk; + + pNtk = Abc_FrameReadNtk(pAbc); + pOut = Abc_FrameReadOut(pAbc); + pErr = Abc_FrameReadErr(pAbc); + + // set defaults + fVerbose = 0; + nConfLimit = 100000; + nImpLimit = 0; + Extra_UtilGetoptReset(); + while ( ( c = Extra_UtilGetopt( argc, argv, "CIvh" ) ) != EOF ) + { + switch ( c ) + { + case 'C': + if ( globalUtilOptind >= argc ) + { + fprintf( pErr, "Command line switch \"-C\" should be followed by an integer.\n" ); + goto usage; + } + nConfLimit = atoi(argv[globalUtilOptind]); + globalUtilOptind++; + if ( nConfLimit < 0 ) + goto usage; + break; + case 'I': + if ( globalUtilOptind >= argc ) + { + fprintf( pErr, "Command line switch \"-I\" should be followed by an integer.\n" ); + goto usage; + } + nImpLimit = atoi(argv[globalUtilOptind]); + globalUtilOptind++; + if ( nImpLimit < 0 ) + goto usage; + break; + case 'v': + fVerbose ^= 1; + break; + case 'h': + goto usage; + default: + goto usage; + } + } + + if ( pNtk == NULL ) + { + fprintf( pErr, "Empty network.\n" ); + return 1; + } + if ( Abc_NtkLatchNum(pNtk) > 0 ) + { + fprintf( stdout, "Currently can only solve the miter for combinational circuits.\n" ); + return 0; + } + if ( Abc_NtkIsSeq(pNtk) ) + { + fprintf( stdout, "This command cannot be applied to the sequential AIG.\n" ); + return 0; + } + + clk = clock(); + if ( Abc_NtkIsStrash(pNtk) ) + { + RetValue = Abc_NtkMiterSat( pNtk, nConfLimit, nImpLimit, fVerbose ); + } + else + { + Abc_Ntk_t * pTemp; + pTemp = Abc_NtkStrash( pNtk, 0, 0 ); + RetValue = Abc_NtkMiterSat( pTemp, nConfLimit, nImpLimit, fVerbose ); + pNtk->pModel = pTemp->pModel; pTemp->pModel = NULL; + Abc_NtkDelete( pTemp ); + } + + // verify that the pattern is correct + if ( RetValue == 0 && Abc_NtkPoNum(pNtk) == 1 ) + { + int * pSimInfo = Abc_NtkVerifySimulatePattern( pNtk, pNtk->pModel ); + if ( pSimInfo[0] != 1 ) + printf( "ERROR in Abc_NtkMiterProve(): Generated counter example is invalid.\n" ); + free( pSimInfo ); + } + + if ( RetValue == -1 ) + printf( "UNDECIDED " ); + else if ( RetValue == 0 ) + printf( "SATISFIABLE " ); + else + printf( "UNSATISFIABLE " ); + //printf( "\n" ); + PRT( "Time", clock() - clk ); + return 0; + +usage: + fprintf( pErr, "usage: sat [-C num] [-I num] [-vh]\n" ); + fprintf( pErr, "\t solves the combinational miter using SAT solver MiniSat-1.14\n" ); + fprintf( pErr, "\t derives CNF from the current network and leave it unchanged\n" ); + fprintf( pErr, "\t-C num : limit on the number of conflicts [default = %d]\n", nConfLimit ); + fprintf( pErr, "\t-I num : limit on the number of implications [default = %d]\n", nImpLimit ); + fprintf( pErr, "\t-v : prints verbose information [default = %s]\n", fVerbose? "yes": "no" ); + fprintf( pErr, "\t-h : print the command usage\n"); + return 1; +} + /**Function************************************************************* Synopsis [] @@ -6519,6 +6554,16 @@ int Abc_CommandProve( Abc_Frame_t * pAbc, int argc, char ** argv ) pNtkTemp = Abc_NtkStrash( pNtk, 0, 0 ); RetValue = Abc_NtkMiterProve( &pNtkTemp, nConfLimit, nImpLimit, fRewrite, fFraig, fVerbose ); + + // verify that the pattern is correct + if ( RetValue == 0 ) + { + int * pSimInfo = Abc_NtkVerifySimulatePattern( pNtk, pNtkTemp->pModel ); + if ( pSimInfo[0] != 1 ) + printf( "ERROR in Abc_NtkMiterProve(): Generated counter-example is invalid.\n" ); + free( pSimInfo ); + } + if ( RetValue == -1 ) printf( "UNDECIDED " ); else if ( RetValue == 0 ) @@ -6535,6 +6580,7 @@ int Abc_CommandProve( Abc_Frame_t * pAbc, int argc, char ** argv ) usage: fprintf( pErr, "usage: prove [-C num] [-I num] [-rfvh]\n" ); fprintf( pErr, "\t solves combinational miter by rewriting, FRAIGing, and SAT\n" ); + fprintf( pErr, "\t replaces the current network by the cone modified by rewriting\n" ); fprintf( pErr, "\t-C num : limit on the number of conflicts [default = %d]\n", nConfLimit ); fprintf( pErr, "\t-I num : limit on the number of implications [default = %d]\n", nImpLimit ); fprintf( pErr, "\t-r : toggle the use of rewriting [default = %s]\n", fRewrite? "yes": "no" ); diff --git a/src/base/abci/abcAuto.c b/src/base/abci/abcAuto.c index f1e1ef75..fb818ff3 100644 --- a/src/base/abci/abcAuto.c +++ b/src/base/abci/abcAuto.c @@ -51,7 +51,7 @@ void Abc_NtkAutoPrint( Abc_Ntk_t * pNtk, int Output, int fNaive, int fVerbose ) int nOutputs, nInputs, i; // compute the global BDDs - if ( Abc_NtkGlobalBdds(pNtk, 0) == NULL ) + if ( Abc_NtkGlobalBdds(pNtk, 10000000, 0) == NULL ) return; // get information about the network diff --git a/src/base/abci/abcClpBdd.c b/src/base/abci/abcClpBdd.c index 59c76e09..84016436 100644 --- a/src/base/abci/abcClpBdd.c +++ b/src/base/abci/abcClpBdd.c @@ -25,6 +25,7 @@ //////////////////////////////////////////////////////////////////////// static Abc_Ntk_t * Abc_NtkFromGlobalBdds( Abc_Ntk_t * pNtk ); +static Abc_Ntk_t * Abc_NtkFromGlobalBddsDual( Abc_Ntk_t * pNtk ); static Abc_Obj_t * Abc_NodeFromGlobalBdds( Abc_Ntk_t * pNtkNew, DdManager * dd, DdNode * bFunc ); //////////////////////////////////////////////////////////////////////// @@ -42,20 +43,23 @@ static Abc_Obj_t * Abc_NodeFromGlobalBdds( Abc_Ntk_t * pNtkNew, DdManager * dd, SeeAlso [] ***********************************************************************/ -Abc_Ntk_t * Abc_NtkCollapse( Abc_Ntk_t * pNtk, int fVerbose ) +Abc_Ntk_t * Abc_NtkCollapse( Abc_Ntk_t * pNtk, int fBddSizeMax, int fDualRail, int fVerbose ) { Abc_Ntk_t * pNtkNew; assert( Abc_NtkIsStrash(pNtk) ); // compute the global BDDs - if ( Abc_NtkGlobalBdds(pNtk, 0) == NULL ) + if ( Abc_NtkGlobalBdds(pNtk, fBddSizeMax, 0) == NULL ) return NULL; if ( fVerbose ) printf( "The shared BDD size is %d nodes.\n", Cudd_ReadKeys(pNtk->pManGlob) - Cudd_ReadDead(pNtk->pManGlob) ); // create the new network - pNtkNew = Abc_NtkFromGlobalBdds( pNtk ); + if ( fDualRail ) + pNtkNew = Abc_NtkFromGlobalBddsDual( pNtk ); + else + pNtkNew = Abc_NtkFromGlobalBdds( pNtk ); Abc_NtkFreeGlobalBdds( pNtk ); if ( pNtkNew == NULL ) { @@ -116,6 +120,42 @@ Abc_Ntk_t * Abc_NtkFromGlobalBdds( Abc_Ntk_t * pNtk ) return pNtkNew; } +/**Function************************************************************* + + Synopsis [Derives the network with the given global BDD.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Abc_Ntk_t * Abc_NtkFromGlobalBddsDual( Abc_Ntk_t * pNtk ) +{ + ProgressBar * pProgress; + Abc_Ntk_t * pNtkNew; + Abc_Obj_t * pNode, * pNodeNew; + DdManager * dd = pNtk->pManGlob; + int i; + // start the new network + pNtkNew = Abc_NtkStartFromDual( pNtk, ABC_NTK_LOGIC, ABC_FUNC_BDD ); + // make sure the new manager has the same number of inputs + Cudd_bddIthVar( pNtkNew->pManFunc, dd->size-1 ); + // process the POs + pProgress = Extra_ProgressBarStart( stdout, Abc_NtkCoNum(pNtk) ); + Abc_NtkForEachCo( pNtk, pNode, i ) + { + Extra_ProgressBarUpdate( pProgress, i, NULL ); + pNodeNew = Abc_NodeFromGlobalBdds( pNtkNew, dd, Cudd_Not( Vec_PtrEntry(pNtk->vFuncsGlob, i) ) ); + Abc_ObjAddFanin( pNode->pCopy->pCopy, pNodeNew ); + pNodeNew = Abc_NodeFromGlobalBdds( pNtkNew, dd, Vec_PtrEntry(pNtk->vFuncsGlob, i) ); + Abc_ObjAddFanin( pNode->pCopy, pNodeNew ); + } + Extra_ProgressBarStop( pProgress ); + return pNtkNew; +} + /**Function************************************************************* Synopsis [Derives the network with the given global BDD.] diff --git a/src/base/abci/abcCut.c b/src/base/abci/abcCut.c index 1ee9a712..2b1816c4 100644 --- a/src/base/abci/abcCut.c +++ b/src/base/abci/abcCut.c @@ -57,41 +57,6 @@ Cut_Man_t * Abc_NtkCuts( Abc_Ntk_t * pNtk, Cut_Params_t * pParams ) extern void Abc_NtkBalanceDetach( Abc_Ntk_t * pNtk ); assert( Abc_NtkIsStrash(pNtk) ); -/* - if ( pParams->fMulti ) - { - Abc_Obj_t * pNode, * pNodeA, * pNodeB, * pNodeC; - int nFactors; - // lebel the nodes, which will be the roots of factor-cuts - // mark the multiple-fanout nodes - Abc_AigForEachAnd( pNtk, pNode, i ) - if ( pNode->vFanouts.nSize > 1 ) - pNode->fMarkB = 1; - // unmark the control inputs of MUXes and inputs of EXOR gates - Abc_AigForEachAnd( pNtk, pNode, i ) - { - if ( !Abc_NodeIsMuxType(pNode) ) - continue; - - pNodeC = Abc_NodeRecognizeMux( pNode, &pNodeA, &pNodeB ); - // if real children are used, skip - if ( Abc_ObjFanin0(pNode)->vFanouts.nSize > 1 || Abc_ObjFanin1(pNode)->vFanouts.nSize > 1 ) - continue; - - if ( pNodeC->vFanouts.nSize == 2 ) - pNodeC->fMarkB = 0; - if ( Abc_ObjRegular(pNodeA) == Abc_ObjRegular(pNodeB) && Abc_ObjRegular(pNodeA)->vFanouts.nSize == 2 ) - Abc_ObjRegular(pNodeA)->fMarkB = 0; - } - // mark the PO drivers -// Abc_NtkForEachCo( pNtk, pNode, i ) -// Abc_ObjFanin0(pNode)->fMarkB = 1; - nFactors = 0; - Abc_AigForEachAnd( pNtk, pNode, i ) - nFactors += pNode->fMarkB; - printf( "Total nodes = %6d. Total factors = %6d.\n", Abc_NtkNodeNum(pNtk), nFactors ); - } -*/ // start the manager pParams->nIdsMax = Abc_NtkObjNumMax( pNtk ); p = Cut_ManStart( pParams ); @@ -135,13 +100,6 @@ Cut_Man_t * Abc_NtkCuts( Abc_Ntk_t * pNtk, Cut_Params_t * pParams ) } Vec_PtrFree( vNodes ); Vec_IntFree( vChoices ); -/* - if ( pParams->fMulti ) - { - Abc_NtkForEachObj( pNtk, pNode, i ) - pNode->fMarkB = 0; - } -*/ PRT( "Total", clock() - clk ); //Abc_NtkPrintCuts_( p, pNtk, 0 ); // Cut_ManPrintStatsToFile( p, pNtk->pSpec, clock() - clk ); diff --git a/src/base/abci/abcDsd.c b/src/base/abci/abcDsd.c index 9dd5ea3a..18a85a04 100644 --- a/src/base/abci/abcDsd.c +++ b/src/base/abci/abcDsd.c @@ -60,7 +60,7 @@ Abc_Ntk_t * Abc_NtkDsdGlobal( Abc_Ntk_t * pNtk, bool fVerbose, bool fPrint, bool assert( Abc_NtkIsStrash(pNtk) ); // perform FPGA mapping - if ( Abc_NtkGlobalBdds(pNtk, 0) == NULL ) + if ( Abc_NtkGlobalBdds(pNtk, 10000000, 0) == NULL ) return NULL; if ( fVerbose ) printf( "The shared BDD size is %d nodes.\n", Cudd_ReadKeys(pNtk->pManGlob) - Cudd_ReadDead(pNtk->pManGlob) ); diff --git a/src/base/abci/abcEspresso.c b/src/base/abci/abcEspresso.c index ee6598c9..744169b5 100644 --- a/src/base/abci/abcEspresso.c +++ b/src/base/abci/abcEspresso.c @@ -54,7 +54,7 @@ void Abc_NtkEspresso( Abc_Ntk_t * pNtk, int fVerbose ) if ( Abc_NtkHasMapping(pNtk) ) Abc_NtkUnmap(pNtk); else if ( Abc_NtkHasBdd(pNtk) ) - Abc_NtkBddToSop(pNtk); + Abc_NtkBddToSop(pNtk, 0); // minimize SOPs of all nodes Abc_NtkForEachNode( pNtk, pNode, i ) if ( i ) Abc_NodeEspresso( pNode ); diff --git a/src/base/abci/abcFxu.c b/src/base/abci/abcFxu.c index 5c629b30..b377da1d 100644 --- a/src/base/abci/abcFxu.c +++ b/src/base/abci/abcFxu.c @@ -57,7 +57,7 @@ bool Abc_NtkFastExtract( Abc_Ntk_t * pNtk, Fxu_Data_t * p ) if ( Abc_NtkIsMappedLogic(pNtk) ) Abc_NtkUnmap(pNtk); else if ( Abc_NtkIsBddLogic(pNtk) ) - Abc_NtkBddToSop(pNtk); + Abc_NtkBddToSop(pNtk, 0); else { // to make sure the SOPs are SCC-free // Abc_NtkSopToBdd(pNtk); diff --git a/src/base/abci/abcMap.c b/src/base/abci/abcMap.c index 39bf15aa..25d9e30f 100644 --- a/src/base/abci/abcMap.c +++ b/src/base/abci/abcMap.c @@ -521,8 +521,8 @@ Abc_Ntk_t * Abc_NtkFromMapSuperChoice( Map_Man_t * pMan, Abc_Ntk_t * pNtk ) // duplicate the network pNtkNew2 = Abc_NtkDup( pNtk ); - pNtkNew = Abc_NtkRenode( pNtkNew2, 0, 20, 0, 0, 1 ); - Abc_NtkBddToSop( pNtkNew ); + pNtkNew = Abc_NtkRenode( pNtkNew2, 0, 20, 0, 0, 1, 0 ); + Abc_NtkBddToSop( pNtkNew, 0 ); // set the old network to point to the new network Abc_NtkForEachCi( pNtk, pNode, i ) diff --git a/src/base/abci/abcMiter.c b/src/base/abci/abcMiter.c index 30fc3a79..c0658d5e 100644 --- a/src/base/abci/abcMiter.c +++ b/src/base/abci/abcMiter.c @@ -414,7 +414,7 @@ Abc_Ntk_t * Abc_NtkMiterQuantify( Abc_Ntk_t * pNtk, int In, int fExist ) /**Function************************************************************* - Synopsis [Derives the miter of two cofactors of one output.] + Synopsis [Quantifies all the PIs existentially from the only PO of the network.] Description [] @@ -470,7 +470,7 @@ int Abc_NtkMiterIsConstant( Abc_Ntk_t * pMiter ) if ( !Abc_ObjIsComplement(pChild) ) { // if the miter is constant 1, return immediately - printf( "MITER IS CONSTANT 1!\n" ); +// printf( "MITER IS CONSTANT 1!\n" ); return 0; } } diff --git a/src/base/abci/abcNewAig.c b/src/base/abci/abcNewAig.c index ce76195a..209fc991 100644 --- a/src/base/abci/abcNewAig.c +++ b/src/base/abci/abcNewAig.c @@ -65,7 +65,7 @@ Abc_Ntk_t * Abc_NtkNewAig( Abc_Ntk_t * pNtk ) assert( !Abc_NtkIsNetlist(pNtk) ); assert( !Abc_NtkIsSeq(pNtk) ); if ( Abc_NtkIsBddLogic(pNtk) ) - Abc_NtkBddToSop(pNtk); + Abc_NtkBddToSop(pNtk, 0); // print warning about choice nodes if ( Abc_NtkGetChoiceNum( pNtk ) ) printf( "Warning: The choice nodes in the initial AIG are removed by strashing.\n" ); diff --git a/src/base/abci/abcNtbdd.c b/src/base/abci/abcNtbdd.c index b961ec15..d92da31b 100644 --- a/src/base/abci/abcNtbdd.c +++ b/src/base/abci/abcNtbdd.c @@ -27,7 +27,7 @@ static void Abc_NtkBddToMuxesPerform( Abc_Ntk_t * pNtk, Abc_Ntk_t * pNtkNew ); static Abc_Obj_t * Abc_NodeBddToMuxes( Abc_Obj_t * pNodeOld, Abc_Ntk_t * pNtkNew ); static Abc_Obj_t * Abc_NodeBddToMuxes_rec( DdManager * dd, DdNode * bFunc, Abc_Ntk_t * pNtkNew, st_table * tBdd2Node ); -static DdNode * Abc_NodeGlobalBdds_rec( DdManager * dd, Abc_Obj_t * pNode ); +static DdNode * Abc_NodeGlobalBdds_rec( DdManager * dd, Abc_Obj_t * pNode, int nBddSizeMax ); //////////////////////////////////////////////////////////////////////// /// FUNCTION DEFINITIONS /// @@ -243,7 +243,7 @@ Abc_Obj_t * Abc_NodeBddToMuxes_rec( DdManager * dd, DdNode * bFunc, Abc_Ntk_t * SeeAlso [] ***********************************************************************/ -DdManager * Abc_NtkGlobalBdds( Abc_Ntk_t * pNtk, int fLatchOnly ) +DdManager * Abc_NtkGlobalBdds( Abc_Ntk_t * pNtk, int nBddSizeMax, int fLatchOnly ) { int fReorder = 1; ProgressBar * pProgress; @@ -276,10 +276,10 @@ DdManager * Abc_NtkGlobalBdds( Abc_Ntk_t * pNtk, int fLatchOnly ) Abc_NtkForEachLatch( pNtk, pNode, i ) { Extra_ProgressBarUpdate( pProgress, i, NULL ); - bFunc = Abc_NodeGlobalBdds_rec( dd, Abc_ObjFanin0(pNode) ); + bFunc = Abc_NodeGlobalBdds_rec( dd, Abc_ObjFanin0(pNode), nBddSizeMax ); if ( bFunc == NULL ) { - printf( "Constructing global BDDs timed out.\n" ); + printf( "Constructing global BDDs is aborted.\n" ); Extra_ProgressBarStop( pProgress ); Cudd_Quit( dd ); return NULL; @@ -296,10 +296,10 @@ DdManager * Abc_NtkGlobalBdds( Abc_Ntk_t * pNtk, int fLatchOnly ) Abc_NtkForEachCo( pNtk, pNode, i ) { Extra_ProgressBarUpdate( pProgress, i, NULL ); - bFunc = Abc_NodeGlobalBdds_rec( dd, Abc_ObjFanin0(pNode) ); + bFunc = Abc_NodeGlobalBdds_rec( dd, Abc_ObjFanin0(pNode), nBddSizeMax ); if ( bFunc == NULL ) { - printf( "Constructing global BDDs timed out.\n" ); + printf( "Constructing global BDDs is aborted.\n" ); Extra_ProgressBarStop( pProgress ); Cudd_Quit( dd ); return NULL; @@ -339,21 +339,25 @@ DdManager * Abc_NtkGlobalBdds( Abc_Ntk_t * pNtk, int fLatchOnly ) SeeAlso [] ***********************************************************************/ -DdNode * Abc_NodeGlobalBdds_rec( DdManager * dd, Abc_Obj_t * pNode ) +DdNode * Abc_NodeGlobalBdds_rec( DdManager * dd, Abc_Obj_t * pNode, int nBddSizeMax ) { DdNode * bFunc, * bFunc0, * bFunc1; assert( !Abc_ObjIsComplement(pNode) ); - if ( Cudd_ReadKeys(dd) > 5000000 ) + if ( Cudd_ReadKeys(dd)-Cudd_ReadDead(dd) > (unsigned)nBddSizeMax ) + { + printf( "The number of live nodes reached %d.\n", nBddSizeMax ); + fflush( stdout ); return NULL; + } // if the result is available return if ( pNode->pCopy ) return (DdNode *)pNode->pCopy; // compute the result for both branches - bFunc0 = Abc_NodeGlobalBdds_rec( dd, Abc_ObjFanin(pNode,0) ); + bFunc0 = Abc_NodeGlobalBdds_rec( dd, Abc_ObjFanin(pNode,0), nBddSizeMax ); if ( bFunc0 == NULL ) return NULL; Cudd_Ref( bFunc0 ); - bFunc1 = Abc_NodeGlobalBdds_rec( dd, Abc_ObjFanin(pNode,1) ); + bFunc1 = Abc_NodeGlobalBdds_rec( dd, Abc_ObjFanin(pNode,1), nBddSizeMax ); if ( bFunc1 == NULL ) return NULL; Cudd_Ref( bFunc1 ); @@ -423,7 +427,7 @@ double Abc_NtkSpacePercentage( Abc_Obj_t * pNode ) Vec_PtrForEachEntry( vNodes, pObj, i ) pObj->pCopy = (Abc_Obj_t *)dd->vars[i]; // build the BDD of the cone - bFunc = Abc_NodeGlobalBdds_rec( dd, pNodeR ); Cudd_Ref( bFunc ); + bFunc = Abc_NodeGlobalBdds_rec( dd, pNodeR, 10000000 ); Cudd_Ref( bFunc ); bFunc = Cudd_NotCond( bFunc, pNode != pNodeR ); // count minterms Result = Cudd_CountMinterm( dd, bFunc, dd->size ); diff --git a/src/base/abci/abcPrint.c b/src/base/abci/abcPrint.c index 6791f08c..d299a29d 100644 --- a/src/base/abci/abcPrint.c +++ b/src/base/abci/abcPrint.c @@ -644,7 +644,7 @@ void Abc_NtkPrintGates( Abc_Ntk_t * pNtk, int fUseLibrary ) // transform logic functions from BDD to SOP if ( fHasBdds = Abc_NtkIsBddLogic(pNtk) ) - Abc_NtkBddToSop(pNtk); + Abc_NtkBddToSop(pNtk, 0); // get hold of the SOP of the node CountConst = CountBuf = CountInv = CountAnd = CountOr = CountOther = CounterTotal = 0; diff --git a/src/base/abci/abcProve.c b/src/base/abci/abcProve.c index 18ee9a3f..ae4bb250 100644 --- a/src/base/abci/abcProve.c +++ b/src/base/abci/abcProve.c @@ -29,7 +29,7 @@ extern int Abc_NtkRewrite( Abc_Ntk_t * pNtk, int fUpdateLevel, int fUseZeros, i extern int Abc_NtkRefactor( Abc_Ntk_t * pNtk, int nNodeSizeMax, int nConeSizeMax, bool fUpdateLevel, bool fUseZeros, bool fUseDcs, bool fVerbose ); extern Abc_Ntk_t * Abc_NtkFromFraig( Fraig_Man_t * pMan, Abc_Ntk_t * pNtk ); -static Abc_Ntk_t * Abc_NtkMiterFraig( Abc_Ntk_t * pNtk, int nBTLimit, int * pRetValue ); +static Abc_Ntk_t * Abc_NtkMiterFraig( Abc_Ntk_t * pNtk, int nBTLimit, int * pRetValue, int * pNumFails ); static void Abc_NtkMiterPrint( Abc_Ntk_t * pNtk, char * pString, int clk, int fVerbose ); //////////////////////////////////////////////////////////////////////// @@ -53,8 +53,8 @@ static void Abc_NtkMiterPrint( Abc_Ntk_t * pNtk, char * pString, int clk, int fV int Abc_NtkMiterProve( Abc_Ntk_t ** ppNtk, int nConfLimit, int nImpLimit, int fUseRewrite, int fUseFraig, int fVerbose ) { Abc_Ntk_t * pNtk, * pNtkTemp; - int nConfsStart = 1000, nImpsStart = 0, nBTLimitStart = 2; - int nConfs, nImps, nBTLimit, RetValue; + int nConfsStart = 1000, nImpsStart = 0, nBTLimitStart = 2; // was 5000 + int nConfs, nImps, nBTLimit, RetValue, nSatFails; int nIter = 0, clk, timeStart = clock(); // get the starting network @@ -85,7 +85,10 @@ int Abc_NtkMiterProve( Abc_Ntk_t ** ppNtk, int nConfLimit, int nImpLimit, int fU nIter++; if ( fVerbose ) + { printf( "ITERATION %2d : Confs = %6d. FraigBTL = %3d. \n", nIter, nConfs, nBTLimit ); + fflush( stdout ); + } // try brute-force SAT clk = clock(); @@ -116,25 +119,30 @@ int Abc_NtkMiterProve( Abc_Ntk_t ** ppNtk, int nConfLimit, int nImpLimit, int fU { // try FRAIGing clk = clock(); - pNtk = Abc_NtkMiterFraig( pNtkTemp = pNtk, nBTLimit, &RetValue ); Abc_NtkDelete( pNtkTemp ); + pNtk = Abc_NtkMiterFraig( pNtkTemp = pNtk, nBTLimit, &RetValue, &nSatFails ); Abc_NtkDelete( pNtkTemp ); Abc_NtkMiterPrint( pNtk, "FRAIGing ", clk, fVerbose ); +// printf( "NumFails = %d\n", nSatFails ); if ( RetValue >= 0 ) break; } + else + nSatFails = 1000; // increase resource limits - nConfs = ABC_MIN( nConfs * 3 / 2, 1000000000 ); +// nConfs = ABC_MIN( nConfs * 3 / 2, 1000000000 ); // was 4/2 + nConfs = nSatFails * nBTLimit / 2; nImps = ABC_MIN( nImps * 3 / 2, 1000000000 ); nBTLimit = ABC_MIN( nBTLimit * 8, 1000000000 ); // timeout at 5 minutes - if ( clock() - timeStart >= 300 * CLOCKS_PER_SEC ) - break; - if ( nIter == 4 ) +// if ( clock() - timeStart >= 1200 * CLOCKS_PER_SEC ) +// break; + if ( nIter == 7 ) break; } - while ( (nConfLimit == 0 || nConfs <= nConfLimit) && - (nImpLimit == 0 || nImps <= nImpLimit ) ); +// while ( (nConfLimit == 0 || nConfs <= nConfLimit) && +// (nImpLimit == 0 || nImps <= nImpLimit ) ); + while ( 1 ); // try to prove it using brute force SAT if ( RetValue < 0 ) @@ -144,6 +152,12 @@ int Abc_NtkMiterProve( Abc_Ntk_t ** ppNtk, int nConfLimit, int nImpLimit, int fU Abc_NtkMiterPrint( pNtk, "SAT solving", clk, fVerbose ); } + // assign the model if it was proved by rewriting (const 1 miter) + if ( RetValue == 0 && pNtk->pModel == NULL ) + { + pNtk->pModel = ALLOC( int, Abc_NtkCiNum(pNtk) ); + memset( pNtk->pModel, 0, sizeof(int) * Abc_NtkCiNum(pNtk) ); + } *ppNtk = pNtk; return RetValue; } @@ -159,7 +173,7 @@ int Abc_NtkMiterProve( Abc_Ntk_t ** ppNtk, int nConfLimit, int nImpLimit, int fU SeeAlso [] ***********************************************************************/ -Abc_Ntk_t * Abc_NtkMiterFraig( Abc_Ntk_t * pNtk, int nBTLimit, int * pRetValue ) +Abc_Ntk_t * Abc_NtkMiterFraig( Abc_Ntk_t * pNtk, int nBTLimit, int * pRetValue, int * pNumFails ) { Abc_Ntk_t * pNtkNew; Fraig_Params_t Params, * pParams = &Params; @@ -190,19 +204,24 @@ Abc_Ntk_t * Abc_NtkMiterFraig( Abc_Ntk_t * pNtk, int nBTLimit, int * pRetValue ) Fraig_ManProveMiter( pMan ); RetValue = Fraig_ManCheckMiter( pMan ); + // create the network + pNtkNew = Abc_NtkFromFraig( pMan, pNtk ); + // save model if ( RetValue == 0 ) { pModel = Fraig_ManReadModel( pMan ); - FREE( pNtk->pModel ); - pNtk->pModel = ALLOC( int, Abc_NtkCiNum(pNtk) ); - memcpy( pNtk->pModel, pModel, sizeof(int) * Abc_NtkCiNum(pNtk) ); + FREE( pNtkNew->pModel ); + pNtkNew->pModel = ALLOC( int, Abc_NtkCiNum(pNtkNew) ); + memcpy( pNtkNew->pModel, pModel, sizeof(int) * Abc_NtkCiNum(pNtkNew) ); } - // create the network - pNtkNew = Abc_NtkFromFraig( pMan, pNtk ); + + // save the return values + *pRetValue = RetValue; + *pNumFails = Fraig_ManReadSatFails( pMan ); + // delete the fraig manager Fraig_ManFree( pMan ); - *pRetValue = RetValue; return pNtkNew; } diff --git a/src/base/abci/abcReconv.c b/src/base/abci/abcReconv.c index 2a7188f0..100551c7 100644 --- a/src/base/abci/abcReconv.c +++ b/src/base/abci/abcReconv.c @@ -489,18 +489,20 @@ void Abc_NodeConeMarkCollect_rec( Abc_Obj_t * pNode, Vec_Ptr_t * vVisited ) SeeAlso [] ***********************************************************************/ -DdNode * Abc_NodeConeBdd( DdManager * dd, DdNode ** pbVars, Abc_Obj_t * pNode, Vec_Ptr_t * vLeaves, Vec_Ptr_t * vVisited ) +DdNode * Abc_NodeConeBdd( DdManager * dd, DdNode ** pbVars, Abc_Obj_t * pRoot, Vec_Ptr_t * vLeaves, Vec_Ptr_t * vVisited ) { + Abc_Obj_t * pNode; DdNode * bFunc0, * bFunc1, * bFunc; int i; // get the nodes in the cut without fanins in the DFS order - Abc_NodeConeCollect( &pNode, 1, vLeaves, vVisited, 0 ); + Abc_NodeConeCollect( &pRoot, 1, vLeaves, vVisited, 0 ); // set the elementary BDDs Vec_PtrForEachEntry( vLeaves, pNode, i ) pNode->pCopy = (Abc_Obj_t *)pbVars[i]; // compute the BDDs for the collected nodes Vec_PtrForEachEntry( vVisited, pNode, i ) { + assert( !Abc_ObjIsPi(pNode) ); bFunc0 = Cudd_NotCond( Abc_ObjFanin0(pNode)->pCopy, Abc_ObjFaninC0(pNode) ); bFunc1 = Cudd_NotCond( Abc_ObjFanin1(pNode)->pCopy, Abc_ObjFaninC1(pNode) ); bFunc = Cudd_bddAnd( dd, bFunc0, bFunc1 ); Cudd_Ref( bFunc ); diff --git a/src/base/abci/abcRenode.c b/src/base/abci/abcRenode.c index cfb05aee..ea728858 100644 --- a/src/base/abci/abcRenode.c +++ b/src/base/abci/abcRenode.c @@ -33,6 +33,7 @@ static void Abc_NtkRenodeSetBounds( Abc_Ntk_t * pNtk, int nThresh, int nF static void Abc_NtkRenodeSetBoundsCnf( Abc_Ntk_t * pNtk ); static void Abc_NtkRenodeSetBoundsMulti( Abc_Ntk_t * pNtk, int nThresh ); static void Abc_NtkRenodeSetBoundsSimple( Abc_Ntk_t * pNtk ); +static void Abc_NtkRenodeSetBoundsFactor( Abc_Ntk_t * pNtk ); static void Abc_NtkRenodeCone( Abc_Obj_t * pNode, Vec_Ptr_t * vCone ); //////////////////////////////////////////////////////////////////////// @@ -50,7 +51,7 @@ static void Abc_NtkRenodeCone( Abc_Obj_t * pNode, Vec_Ptr_t * vCone ); SeeAlso [] ***********************************************************************/ -Abc_Ntk_t * Abc_NtkRenode( Abc_Ntk_t * pNtk, int nThresh, int nFaninMax, int fCnf, int fMulti, int fSimple ) +Abc_Ntk_t * Abc_NtkRenode( Abc_Ntk_t * pNtk, int nThresh, int nFaninMax, int fCnf, int fMulti, int fSimple, int fFactor ) { Abc_Ntk_t * pNtkNew; @@ -69,6 +70,8 @@ Abc_Ntk_t * Abc_NtkRenode( Abc_Ntk_t * pNtk, int nThresh, int nFaninMax, int fCn Abc_NtkRenodeSetBoundsMulti( pNtk, nThresh ); else if ( fSimple ) Abc_NtkRenodeSetBoundsSimple( pNtk ); + else if ( fFactor ) + Abc_NtkRenodeSetBoundsFactor( pNtk ); else Abc_NtkRenodeSetBounds( pNtk, nThresh, nFaninMax ); @@ -562,6 +565,32 @@ void Abc_NtkRenodeSetBoundsSimple( Abc_Ntk_t * pNtk ) pNode->fMarkA = 1; } +/**Function************************************************************* + + Synopsis [Sets a factor-cut boundary.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Abc_NtkRenodeSetBoundsFactor( Abc_Ntk_t * pNtk ) +{ + Abc_Obj_t * pNode; + int i; + // make sure the mark is not set + Abc_NtkForEachObj( pNtk, pNode, i ) + assert( pNode->fMarkA == 0 ); + // mark the nodes where expansion stops using pNode->fMarkA + Abc_NtkForEachNode( pNtk, pNode, i ) + pNode->fMarkA = (pNode->vFanouts.nSize > 1 && !Abc_NodeIsMuxControlType(pNode)); + // mark the PO drivers + Abc_NtkForEachCo( pNtk, pNode, i ) + Abc_ObjFanin0(pNode)->fMarkA = 1; +} + /**Function************************************************************* Synopsis [Collects the fanins of a large node.] diff --git a/src/base/abci/abcRestruct.c b/src/base/abci/abcRestruct.c index 137573a5..32e878b8 100644 --- a/src/base/abci/abcRestruct.c +++ b/src/base/abci/abcRestruct.c @@ -332,9 +332,15 @@ Dec_Graph_t * Abc_NodeRestructureCut( Abc_ManRst_t * p, Abc_Obj_t * pRoot, Cut_C return NULL; Vec_PtrPush( p->vLeaves, pLeaf ); } + + if ( pRoot->Id == 29 ) + { + int x = 0; + } + clk = clock(); // collect the internal nodes of the cut - Abc_NodeConeCollect( &pRoot, 1, p->vLeaves, p->vVisited, 0 ); +// Abc_NodeConeCollect( &pRoot, 1, p->vLeaves, p->vVisited, 0 ); // derive the BDD of the cut bFunc = Abc_NodeConeBdd( p->dd, p->dd->vars, pRoot, p->vLeaves, p->vVisited ); Cudd_Ref( bFunc ); p->timeBdd += clock() - clk; diff --git a/src/base/abci/abcResub.c b/src/base/abci/abcResub.c new file mode 100644 index 00000000..30e2eca2 --- /dev/null +++ b/src/base/abci/abcResub.c @@ -0,0 +1,801 @@ +/**CFile**************************************************************** + + FileName [abcResub.c] + + SystemName [ABC: Logic synthesis and verification system.] + + PackageName [Network and node package.] + + Synopsis [Resubstitution manager.] + + Author [Alan Mishchenko] + + Affiliation [UC Berkeley] + + Date [Ver. 1.0. Started - June 20, 2005.] + + Revision [$Id: abcResub.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $] + +***********************************************************************/ + +#include "abc.h" +#include "dec.h" + +//////////////////////////////////////////////////////////////////////// +/// DECLARATIONS /// +//////////////////////////////////////////////////////////////////////// + +typedef struct Abc_ResubMan_t_ Abc_ResubMan_t; +struct Abc_ResubMan_t_ +{ + // paramers + int nLeavesMax; // the max number of leaves in the cone + int nDivsMax; // the max number of divisors in the cone + // representation of the cone + Abc_Obj_t * pRoot; // the root of the cone + int nLeaves; // the number of leaves + int nDivs; // the number of all divisor (including leaves) + int nMffc; // the size of MFFC + Vec_Ptr_t * vDivs; // the divisors + // representation of the simulation info + int nBits; // the number of simulation bits + int nWords; // the number of unsigneds for siminfo + Vec_Ptr_t * vSims; // simulation info + unsigned * pInfo; // pointer to simulation info + // internal divisor storage + Vec_Ptr_t * vDivs1U; // the single-node unate divisors + Vec_Ptr_t * vDivs1B; // the single-node binate divisors + Vec_Ptr_t * vDivs2U0; // the double-node unate divisors + Vec_Ptr_t * vDivs2U1; // the double-node unate divisors + // other data + Vec_Ptr_t * vTemp; // temporary array of nodes +}; + + +// external procedures +extern Abc_ResubMan_t * Abc_ResubManStart( int nLeavesMax, int nDivsMax ); +extern void Abc_ResubManStop( Abc_ResubMan_t * p ); +extern Dec_Graph_t * Abc_ResubManEval( Abc_ResubMan_t * p, Abc_Obj_t * pRoot, Vec_Ptr_t * vLeaves, int nSteps ); + + +static int Abc_ResubManCollectDivs( Abc_ResubMan_t * p, Abc_Obj_t * pRoot, Vec_Ptr_t * vLeaves ); +static int Abc_ResubManMffc( Abc_ResubMan_t * p, Vec_Ptr_t * vDivs, Abc_Obj_t * pRoot, int nLeaves ); +static void Abc_ResubManSimulate( Vec_Ptr_t * vDivs, int nLeaves, Vec_Ptr_t * vSims, int nLeavesMax, int nWords ); + +static Dec_Graph_t * Abc_ResubManQuit( Abc_ResubMan_t * p ); +static Dec_Graph_t * Abc_ResubManDivs0( Abc_ResubMan_t * p ); +static Dec_Graph_t * Abc_ResubManDivs1( Abc_ResubMan_t * p ); +static Dec_Graph_t * Abc_ResubManDivsD( Abc_ResubMan_t * p ); +static Dec_Graph_t * Abc_ResubManDivs2( Abc_ResubMan_t * p ); +static Dec_Graph_t * Abc_ResubManDivs3( Abc_ResubMan_t * p ); + +//////////////////////////////////////////////////////////////////////// +/// FUNCTION DEFINITIONS /// +//////////////////////////////////////////////////////////////////////// + +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Abc_ResubMan_t * Abc_ResubManStart( int nLeavesMax, int nDivsMax ) +{ + Abc_ResubMan_t * p; + unsigned * pData; + int i, k; + p = ALLOC( Abc_ResubMan_t, 1 ); + memset( p, 0, sizeof(Abc_ResubMan_t) ); + p->nLeavesMax = nLeavesMax; + p->nDivsMax = nDivsMax; + p->vDivs = Vec_PtrAlloc( p->nDivsMax ); + // allocate simulation info + p->nBits = (1 << p->nLeavesMax); + p->nWords = (p->nBits <= 32)? 1 : p->nBits / sizeof(unsigned) / 8; + p->pInfo = ALLOC( unsigned, p->nWords * p->nDivsMax ); + memset( p->pInfo, 0, sizeof(unsigned) * p->nWords * p->nLeavesMax ); + p->vSims = Vec_PtrAlloc( p->nDivsMax ); + for ( i = 0; i < p->nDivsMax; i++ ) + Vec_PtrPush( p->vSims, p->pInfo + i * p->nWords ); + // set elementary truth tables + for ( k = 0; k < p->nLeavesMax; k++ ) + { + pData = p->vSims->pArray[k]; + for ( i = 0; i < p->nBits; i++ ) + if ( i & (1 << k) ) + pData[i/32] |= (1 << (i%32)); + } + // create the remaining divisors + p->vDivs1U = Vec_PtrAlloc( p->nDivsMax ); + p->vDivs1B = Vec_PtrAlloc( p->nDivsMax ); + p->vDivs2U0 = Vec_PtrAlloc( p->nDivsMax ); + p->vDivs2U1 = Vec_PtrAlloc( p->nDivsMax ); + p->vTemp = Vec_PtrAlloc( p->nDivsMax ); + return p; +} + +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Abc_ResubManStop( Abc_ResubMan_t * p ) +{ + Vec_PtrFree( p->vDivs ); + Vec_PtrFree( p->vSims ); + Vec_PtrFree( p->vDivs1U ); + Vec_PtrFree( p->vDivs1B ); + Vec_PtrFree( p->vDivs2U0 ); + Vec_PtrFree( p->vDivs2U1 ); + Vec_PtrFree( p->vTemp ); + free( p->pInfo ); + free( p ); +} + + +/**Function************************************************************* + + Synopsis [Evaluates resubstution of one cut.] + + Description [Returns the graph to add if any.] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Dec_Graph_t * Abc_ResubManEval( Abc_ResubMan_t * p, Abc_Obj_t * pRoot, Vec_Ptr_t * vLeaves, int nSteps ) +{ + Dec_Graph_t * pGraph; + assert( nSteps >= 0 ); + assert( nSteps <= 3 ); + // get the number of leaves + p->pRoot = pRoot; + p->nLeaves = Vec_PtrSize(vLeaves); + // collect the divisor nodes + Abc_ResubManCollectDivs( p, pRoot, vLeaves ); + // quit if the number of divisors collected is too large + if ( Vec_PtrSize(p->vDivs) - p->nLeaves > p->nDivsMax - p->nLeavesMax ) + return NULL; + // get the number nodes in its MFFC (and reorder the nodes) + p->nMffc = Abc_ResubManMffc( p, p->vDivs, pRoot, p->nLeaves ); + assert( p->nMffc > 0 ); + // get the number of divisors + p->nDivs = Vec_PtrSize(p->vDivs) - p->nMffc; + // simulate the nodes + Abc_ResubManSimulate( p->vDivs, p->nLeaves, p->vSims, p->nLeavesMax, p->nWords ); + + // consider constants + if ( pGraph = Abc_ResubManQuit( p ) ) + return pGraph; + + // consider equal nodes + if ( pGraph = Abc_ResubManDivs0( p ) ) + return pGraph; + if ( nSteps == 0 || p->nLeavesMax == 1 ) + return NULL; + + // consider one node + if ( pGraph = Abc_ResubManDivs1( p ) ) + return pGraph; + if ( nSteps == 1 || p->nLeavesMax == 2 ) + return NULL; + + // get the two level divisors + Abc_ResubManDivsD( p ); + + // consider two nodes + if ( pGraph = Abc_ResubManDivs2( p ) ) + return pGraph; + if ( nSteps == 2 || p->nLeavesMax == 3 ) + return NULL; + + // consider two nodes + if ( pGraph = Abc_ResubManDivs3( p ) ) + return pGraph; + if ( nSteps == 3 || p->nLeavesMax == 4 ) + return NULL; + return NULL; +} + + + +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Abc_ResubManCollectDivs( Abc_ResubMan_t * p, Abc_Obj_t * pRoot, Vec_Ptr_t * vLeaves ) +{ + Abc_Obj_t * pNode, * pFanout; + int i, k; + // collect the leaves of the cut + Vec_PtrClear( p->vDivs ); + Abc_NtkIncrementTravId( pRoot->pNtk ); + Vec_PtrForEachEntry( vLeaves, pNode, i ) + { + Vec_PtrPush( p->vDivs, pNode ); + Abc_NodeSetTravIdCurrent( pNode ); + } + // explore the fanouts + Vec_PtrForEachEntry( p->vDivs, pNode, i ) + { + // if the fanout has both fanins in the set, add it + Abc_ObjForEachFanout( pNode, pFanout, k ) + { + if ( Abc_NodeIsTravIdCurrent(pFanout) || Abc_ObjIsPo(pFanout) ) + continue; + if ( Abc_NodeIsTravIdCurrent(Abc_ObjFanin0(pFanout)) && Abc_NodeIsTravIdCurrent(Abc_ObjFanin1(pFanout)) ) + { + Vec_PtrPush( p->vDivs, pFanout ); + Abc_NodeSetTravIdCurrent( pFanout ); + } + } + } + return 1; +} + +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Abc_ResubManMffc_rec( Abc_Obj_t * pNode ) +{ + if ( Abc_NodeIsTravIdCurrent(pNode) ) + return 0; + Abc_NodeSetTravIdCurrent( pNode ); + return 1 + Abc_ResubManMffc_rec( Abc_ObjFanin0(pNode) ) + + Abc_ResubManMffc_rec( Abc_ObjFanin1(pNode) ); +} + +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Abc_ResubManMffc( Abc_ResubMan_t * p, Vec_Ptr_t * vDivs, Abc_Obj_t * pRoot, int nLeaves ) +{ + Abc_Obj_t * pObj; + int Counter, i, k; + // increment the traversal ID for the leaves + Abc_NtkIncrementTravId( pRoot->pNtk ); + // label the leaves + Vec_PtrForEachEntryStop( vDivs, pObj, i, nLeaves ) + Abc_NodeSetTravIdCurrent( pObj ); + // make sure the node is in the cone and is no one of the leaves + assert( Abc_NodeIsTravIdPrevious(pRoot) ); + Counter = Abc_ResubManMffc_rec( pRoot ); + // move the labeled nodes to the end + Vec_PtrClear( p->vTemp ); + k = 0; + Vec_PtrForEachEntryStart( vDivs, pObj, i, nLeaves ) + if ( Abc_NodeIsTravIdCurrent(pObj) ) + Vec_PtrPush( p->vTemp, pObj ); + else + Vec_PtrWriteEntry( vDivs, k++, pObj ); + // add the labeled nodes + Vec_PtrForEachEntry( p->vTemp, pObj, i ) + Vec_PtrWriteEntry( vDivs, k++, pObj ); + assert( k == Vec_PtrSize(p->vDivs) ); + assert( pRoot == Vec_PtrEntryLast(p->vDivs) ); + return Counter; +} + +/**Function************************************************************* + + Synopsis [Performs simulation.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Abc_ResubManSimulate( Vec_Ptr_t * vDivs, int nLeaves, Vec_Ptr_t * vSims, int nLeavesMax, int nWords ) +{ + Abc_Obj_t * pObj; + unsigned * puData0, * puData1, * puData; + int i, k; + // initialize random simulation data + Vec_PtrForEachEntryStop( vDivs, pObj, i, nLeaves ) + pObj->pData = Vec_PtrEntry( vSims, i ); + // simulate + Vec_PtrForEachEntryStart( vDivs, pObj, i, nLeaves ) + { + pObj->pData = Vec_PtrEntry( vSims, i + nLeavesMax ); + puData0 = Abc_ObjFanin0(pObj)->pData; + puData1 = Abc_ObjFanin1(pObj)->pData; + puData = pObj->pData; + // simulate + if ( Abc_ObjFaninC0(pObj) && Abc_ObjFaninC1(pObj) ) + for ( k = 0; k < nWords; k++ ) + puData[k] = ~puData0[k] & ~puData1[k]; + else if ( Abc_ObjFaninC0(pObj) ) + for ( k = 0; k < nWords; k++ ) + puData[k] = ~puData0[k] & puData1[k]; + else if ( Abc_ObjFaninC1(pObj) ) + for ( k = 0; k < nWords; k++ ) + puData[k] = puData0[k] & ~puData1[k]; + else + for ( k = 0; k < nWords; k++ ) + puData[k] = puData0[k] & puData1[k]; + } + // complement if needed + Vec_PtrForEachEntry( vDivs, pObj, i ) + { + puData = pObj->pData; + pObj->fPhase = (puData[0] & 1); + if ( pObj->fPhase ) + for ( k = 0; k < nWords; k++ ) + puData[k] = ~puData[k]; + } +} + + +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Dec_Graph_t * Abc_ResubManQuit( Abc_ResubMan_t * p ) +{ + Dec_Graph_t * pGraph; + unsigned * upData; + int w; + upData = p->pRoot->pData; + for ( w = 0; w < p->nWords; w++ ) + if ( upData[0] == 0 ) + break; + if ( w != p->nWords ) + return NULL; + // get the graph if the node looks constant + if ( p->pRoot->fPhase ) + pGraph = Dec_GraphCreateConst1(); + else + pGraph = Dec_GraphCreateConst0(); + return pGraph; +} + +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Dec_Graph_t * Abc_ResubManQuit0( Abc_Obj_t * pRoot, Abc_Obj_t * pObj ) +{ + Dec_Graph_t * pGraph; + Dec_Edge_t eRoot; + pGraph = Dec_GraphCreate( 1 ); + Dec_GraphNode( pGraph, 0 )->pFunc = pObj; + eRoot = Dec_EdgeCreate( 0, pObj->fPhase ); + Dec_GraphSetRoot( pGraph, eRoot ); + if ( pRoot->fPhase ) + Dec_GraphComplement( pGraph ); + return pGraph; +} + +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Dec_Graph_t * Abc_ResubManQuit1( Abc_Obj_t * pRoot, Abc_Obj_t * pObj0, Abc_Obj_t * pObj1 ) +{ + Dec_Graph_t * pGraph; + Dec_Edge_t eRoot, eNode0, eNode1; + assert( !Abc_ObjIsComplement(pObj0) ); + assert( !Abc_ObjIsComplement(pObj1) ); + pGraph = Dec_GraphCreate( 2 ); + Dec_GraphNode( pGraph, 0 )->pFunc = pObj0; + Dec_GraphNode( pGraph, 1 )->pFunc = pObj1; + eNode0 = Dec_EdgeCreate( 0, pObj0->fPhase ); + eNode1 = Dec_EdgeCreate( 1, pObj1->fPhase ); + eRoot = Dec_GraphAddNodeOr( pGraph, eNode0, eNode1 ); + Dec_GraphSetRoot( pGraph, eRoot ); + if ( pRoot->fPhase ) + Dec_GraphComplement( pGraph ); + return pGraph; +} + +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Dec_Graph_t * Abc_ResubManQuit2( Abc_Obj_t * pRoot, Abc_Obj_t * pObj0, Abc_Obj_t * pObj1, Abc_Obj_t * pObj2 ) +{ + Dec_Graph_t * pGraph; + Dec_Edge_t eRoot, eAnd, eNode0, eNode1, eNode2; + assert( !Abc_ObjIsComplement(pObj0) ); + pGraph = Dec_GraphCreate( 3 ); + Dec_GraphNode( pGraph, 0 )->pFunc = Abc_ObjRegular(pObj0); + Dec_GraphNode( pGraph, 1 )->pFunc = Abc_ObjRegular(pObj1); + Dec_GraphNode( pGraph, 2 )->pFunc = Abc_ObjRegular(pObj2); + eNode0 = Dec_EdgeCreate( 0, Abc_ObjIsComplement(pObj0) ^ pObj0->fPhase ); + eNode1 = Dec_EdgeCreate( 1, Abc_ObjIsComplement(pObj1) ^ pObj1->fPhase ); + eNode2 = Dec_EdgeCreate( 2, Abc_ObjIsComplement(pObj2) ^ pObj2->fPhase ); + eAnd = Dec_GraphAddNodeAnd( pGraph, eNode1, eNode2 ); + eRoot = Dec_GraphAddNodeOr( pGraph, eNode0, eAnd ); + Dec_GraphSetRoot( pGraph, eRoot ); + if ( pRoot->fPhase ) + Dec_GraphComplement( pGraph ); + return pGraph; +} + +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Dec_Graph_t * Abc_ResubManQuit3( Abc_Obj_t * pRoot, Abc_Obj_t * pObj0, Abc_Obj_t * pObj1, Abc_Obj_t * pObj2, Abc_Obj_t * pObj3 ) +{ + Dec_Graph_t * pGraph; + Dec_Edge_t eRoot, eAnd0, eAnd1, eNode0, eNode1, eNode2, eNode3; + pGraph = Dec_GraphCreate( 4 ); + Dec_GraphNode( pGraph, 0 )->pFunc = Abc_ObjRegular(pObj0); + Dec_GraphNode( pGraph, 1 )->pFunc = Abc_ObjRegular(pObj1); + Dec_GraphNode( pGraph, 2 )->pFunc = Abc_ObjRegular(pObj2); + Dec_GraphNode( pGraph, 3 )->pFunc = Abc_ObjRegular(pObj3); + eNode0 = Dec_EdgeCreate( 0, Abc_ObjIsComplement(pObj0) ^ pObj0->fPhase ); + eNode1 = Dec_EdgeCreate( 1, Abc_ObjIsComplement(pObj1) ^ pObj1->fPhase ); + eNode2 = Dec_EdgeCreate( 2, Abc_ObjIsComplement(pObj2) ^ pObj2->fPhase ); + eNode3 = Dec_EdgeCreate( 3, Abc_ObjIsComplement(pObj3) ^ pObj3->fPhase ); + eAnd0 = Dec_GraphAddNodeAnd( pGraph, eNode0, eNode1 ); + eAnd1 = Dec_GraphAddNodeAnd( pGraph, eNode2, eNode3 ); + eRoot = Dec_GraphAddNodeOr( pGraph, eAnd0, eAnd1 ); + Dec_GraphSetRoot( pGraph, eRoot ); + if ( pRoot->fPhase ) + Dec_GraphComplement( pGraph ); + return pGraph; +} + + +/**Function************************************************************* + + Synopsis [Derives unate/binate divisors.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Dec_Graph_t * Abc_ResubManDivs0( Abc_ResubMan_t * p ) +{ + Abc_Obj_t * pObj; + unsigned * puData, * puDataR; + int i, w; + Vec_PtrClear( p->vDivs1U ); + Vec_PtrClear( p->vDivs1B ); + puDataR = p->pRoot->pData; + Vec_PtrForEachEntryStop( p->vDivs, pObj, i, p->nDivs ) + { + puData = pObj->pData; + for ( w = 0; w < p->nWords; w++ ) + if ( puData[w] != puDataR[w] ) + break; + if ( w == p->nWords ) + return Abc_ResubManQuit0( p->pRoot, pObj ); + for ( w = 0; w < p->nWords; w++ ) + if ( puData[w] & ~puDataR[w] ) + break; + if ( w == p->nWords ) + Vec_PtrPush( p->vDivs1U, pObj ); + else + Vec_PtrPush( p->vDivs1B, pObj ); + } + return NULL; +} + +/**Function************************************************************* + + Synopsis [Derives unate/binate divisors.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Dec_Graph_t * Abc_ResubManDivs1( Abc_ResubMan_t * p ) +{ + Abc_Obj_t * pObj0, * pObj1; + unsigned * puData0, * puData1, * puDataR; + int i, k, w; + puDataR = p->pRoot->pData; + Vec_PtrForEachEntry( p->vDivs1U, pObj0, i ) + { + puData0 = pObj0->pData; + Vec_PtrForEachEntryStart( p->vDivs1U, pObj1, k, i + 1 ) + { + puData1 = pObj1->pData; + for ( w = 0; w < p->nWords; w++ ) + if ( (puData0[w] | puData1[w]) != puDataR[w] ) + break; + if ( w == p->nWords ) + return Abc_ResubManQuit1( p->pRoot, pObj0, pObj1 ); + } + } + return NULL; +} + +/**Function************************************************************* + + Synopsis [Derives unate/binate divisors.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Dec_Graph_t * Abc_ResubManDivsD( Abc_ResubMan_t * p ) +{ + Abc_Obj_t * pObj0, * pObj1; + unsigned * puData0, * puData1, * puDataR; + int i, k, w; + Vec_PtrClear( p->vDivs2U0 ); + Vec_PtrClear( p->vDivs2U1 ); + puDataR = p->pRoot->pData; + Vec_PtrForEachEntry( p->vDivs1U, pObj0, i ) + { + puData0 = pObj0->pData; + Vec_PtrForEachEntryStart( p->vDivs1U, pObj1, k, i + 1 ) + { + puData1 = pObj1->pData; + + for ( w = 0; w < p->nWords; w++ ) + if ( (puData0[w] & puData1[w]) & ~puDataR[w] ) + break; + if ( w == p->nWords ) + { + Vec_PtrPush( p->vDivs2U0, pObj0 ); + Vec_PtrPush( p->vDivs2U1, pObj1 ); + } + + for ( w = 0; w < p->nWords; w++ ) + if ( (~puData0[w] & puData1[w]) & ~puDataR[w] ) + break; + if ( w == p->nWords ) + { + Vec_PtrPush( p->vDivs2U0, Abc_ObjNot(pObj0) ); + Vec_PtrPush( p->vDivs2U1, pObj1 ); + } + + for ( w = 0; w < p->nWords; w++ ) + if ( (puData0[w] & ~puData1[w]) & ~puDataR[w] ) + break; + if ( w == p->nWords ) + { + Vec_PtrPush( p->vDivs2U0, pObj0 ); + Vec_PtrPush( p->vDivs2U1, Abc_ObjNot(pObj1) ); + } + } + } + return NULL; +} + +/**Function************************************************************* + + Synopsis [Derives unate/binate divisors.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Dec_Graph_t * Abc_ResubManDivs2( Abc_ResubMan_t * p ) +{ + Abc_Obj_t * pObj0, * pObj1, * pObj2; + unsigned * puData0, * puData1, * puData2, * puDataR; + int i, k, w; + puDataR = p->pRoot->pData; + Vec_PtrForEachEntry( p->vDivs1U, pObj0, i ) + { + puData0 = pObj0->pData; + Vec_PtrForEachEntryStart( p->vDivs2U0, pObj1, k, i + 1 ) + { + pObj2 = Vec_PtrEntry( p->vDivs2U1, k ); + puData1 = Abc_ObjRegular(pObj1)->pData; + puData2 = Abc_ObjRegular(pObj2)->pData; + + if ( !Abc_ObjFaninC0(pObj1) && !Abc_ObjFaninC1(pObj2) ) + { + for ( w = 0; w < p->nWords; w++ ) + if ( (puData0[w] | (puData1[w] & puData2[w])) != puDataR[w] ) + break; + } + else if ( Abc_ObjFaninC0(pObj1) ) + { + for ( w = 0; w < p->nWords; w++ ) + if ( (puData0[w] | (~puData1[w] & puData2[w])) != puDataR[w] ) + break; + } + else if ( Abc_ObjFaninC1(pObj2) ) + { + for ( w = 0; w < p->nWords; w++ ) + if ( (puData0[w] | (puData1[w] & ~puData2[w])) != puDataR[w] ) + break; + } + else assert( 0 ); + if ( w == p->nWords ) + return Abc_ResubManQuit2( p->pRoot, pObj0, pObj1, pObj2 ); + } + } + return NULL; +} + +/**Function************************************************************* + + Synopsis [Derives unate/binate divisors.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Dec_Graph_t * Abc_ResubManDivs3( Abc_ResubMan_t * p ) +{ + Abc_Obj_t * pObj0, * pObj1, * pObj2, * pObj3; + unsigned * puData0, * puData1, * puData2, * puData3, * puDataR; + int i, k, w; + puDataR = p->pRoot->pData; + Vec_PtrForEachEntry( p->vDivs2U0, pObj0, i ) + { + pObj1 = Vec_PtrEntry( p->vDivs2U1, i ); + puData0 = Abc_ObjRegular(pObj0)->pData; + puData1 = Abc_ObjRegular(pObj1)->pData; + + Vec_PtrForEachEntryStart( p->vDivs2U0, pObj2, k, i + 1 ) + { + pObj3 = Vec_PtrEntry( p->vDivs2U1, k ); + puData2 = Abc_ObjRegular(pObj2)->pData; + puData3 = Abc_ObjRegular(pObj3)->pData; + + if ( !Abc_ObjFaninC0(pObj0) && !Abc_ObjFaninC1(pObj1) ) + { + if ( !Abc_ObjFaninC0(pObj2) && !Abc_ObjFaninC1(pObj3) ) + { + for ( w = 0; w < p->nWords; w++ ) + if ( ((puData0[w] & puData1[w]) | (puData2[w] & puData3[w])) != puDataR[w] ) + break; + } + else if ( Abc_ObjFaninC0(pObj2) ) + { + for ( w = 0; w < p->nWords; w++ ) + if ( ((puData0[w] & puData1[w]) | (~puData2[w] & puData3[w])) != puDataR[w] ) + break; + } + else if ( Abc_ObjFaninC0(pObj3) ) + { + for ( w = 0; w < p->nWords; w++ ) + if ( ((puData0[w] & puData1[w]) | (puData2[w] & ~puData3[w])) != puDataR[w] ) + break; + } + else assert( 0 ); + } + else if ( Abc_ObjFaninC0(pObj0) ) + { + if ( !Abc_ObjFaninC0(pObj2) && !Abc_ObjFaninC1(pObj3) ) + { + for ( w = 0; w < p->nWords; w++ ) + if ( ((~puData0[w] & puData1[w]) | (puData2[w] & puData3[w])) != puDataR[w] ) + break; + } + else if ( Abc_ObjFaninC0(pObj2) ) + { + for ( w = 0; w < p->nWords; w++ ) + if ( ((~puData0[w] & puData1[w]) | (~puData2[w] & puData3[w])) != puDataR[w] ) + break; + } + else if ( Abc_ObjFaninC0(pObj3) ) + { + for ( w = 0; w < p->nWords; w++ ) + if ( ((~puData0[w] & puData1[w]) | (puData2[w] & ~puData3[w])) != puDataR[w] ) + break; + } + else assert( 0 ); + } + else if ( Abc_ObjFaninC1(pObj1) ) + { + if ( !Abc_ObjFaninC0(pObj2) && !Abc_ObjFaninC1(pObj3) ) + { + for ( w = 0; w < p->nWords; w++ ) + if ( ((puData0[w] & ~puData1[w]) | (puData2[w] & puData3[w])) != puDataR[w] ) + break; + } + else if ( Abc_ObjFaninC0(pObj2) ) + { + for ( w = 0; w < p->nWords; w++ ) + if ( ((puData0[w] & ~puData1[w]) | (~puData2[w] & puData3[w])) != puDataR[w] ) + break; + } + else if ( Abc_ObjFaninC0(pObj3) ) + { + for ( w = 0; w < p->nWords; w++ ) + if ( ((puData0[w] & ~puData1[w]) | (puData2[w] & ~puData3[w])) != puDataR[w] ) + break; + } + else assert( 0 ); + } + else assert( 0 ); + if ( w == p->nWords ) + return Abc_ResubManQuit3( p->pRoot, pObj0, pObj1, pObj2, pObj3 ); + } + } + return NULL; +} + +//////////////////////////////////////////////////////////////////////// +/// END OF FILE /// +//////////////////////////////////////////////////////////////////////// + + diff --git a/src/base/abci/abcSat.c b/src/base/abci/abcSat.c index 5376444b..f7400313 100644 --- a/src/base/abci/abcSat.c +++ b/src/base/abci/abcSat.c @@ -400,6 +400,10 @@ int Abc_NtkMiterSatCreateInt( solver * pSat, Abc_Ntk_t * pNtk ) assert( Abc_NtkIsStrash(pNtk) ); + // clean the CI node pointers + Abc_NtkForEachCi( pNtk, pNode, i ) + pNode->pCopy = NULL; + // start the data structures vNodes = Vec_PtrAlloc( 1000 ); // the nodes corresponding to vars in the solver vSuper = Vec_PtrAlloc( 100 ); // the nodes belonging to the given implication supergate diff --git a/src/base/abci/abcStrash.c b/src/base/abci/abcStrash.c index 72f4215b..fbaca324 100644 --- a/src/base/abci/abcStrash.c +++ b/src/base/abci/abcStrash.c @@ -58,7 +58,7 @@ Abc_Ntk_t * Abc_NtkStrash( Abc_Ntk_t * pNtk, bool fAllNodes, bool fCleanup ) assert( !Abc_NtkIsNetlist(pNtk) ); assert( !Abc_NtkIsSeq(pNtk) ); if ( Abc_NtkIsBddLogic(pNtk) ) - Abc_NtkBddToSop(pNtk); + Abc_NtkBddToSop(pNtk, 0); // print warning about choice nodes if ( Abc_NtkGetChoiceNum( pNtk ) ) printf( "Warning: The choice nodes in the initial AIG are removed by strashing.\n" ); @@ -108,7 +108,7 @@ int Abc_NtkAppend( Abc_Ntk_t * pNtk1, Abc_Ntk_t * pNtk2 ) assert( Abc_NtkIsStrash(pNtk1) ); assert( Abc_NtkIsLogic(pNtk2) || Abc_NtkIsStrash(pNtk2) ); if ( Abc_NtkIsBddLogic(pNtk2) ) - Abc_NtkBddToSop(pNtk2); + Abc_NtkBddToSop(pNtk2, 0); // check that the networks have the same PIs // reorder PIs of pNtk2 according to pNtk1 if ( !Abc_NtkCompareSignals( pNtk1, pNtk2, 1 ) ) diff --git a/src/base/abci/abcSweep.c b/src/base/abci/abcSweep.c index 228e27eb..08236edc 100644 --- a/src/base/abci/abcSweep.c +++ b/src/base/abci/abcSweep.c @@ -545,7 +545,7 @@ int Abc_NtkSweep( Abc_Ntk_t * pNtk, int fVerbose ) while ( nSweptNew ); // conver back to BDD if ( fConvert ) - Abc_NtkBddToSop(pNtk); + Abc_NtkBddToSop(pNtk, 0); // report if ( fVerbose ) printf( "Sweep removed %d nodes.\n", nSwept ); diff --git a/src/base/abci/abcSymm.c b/src/base/abci/abcSymm.c index 12cdab85..35cf896f 100644 --- a/src/base/abci/abcSymm.c +++ b/src/base/abci/abcSymm.c @@ -88,7 +88,7 @@ void Abc_NtkSymmetriesUsingBdds( Abc_Ntk_t * pNtk, int fNaive, int fVerbose ) // compute the global functions clk = clock(); - dd = Abc_NtkGlobalBdds( pNtk, 0 ); + dd = Abc_NtkGlobalBdds( pNtk, 10000000, 0 ); Cudd_AutodynDisable( dd ); Cudd_zddVarsFromBddVars( dd, 2 ); clkBdd = clock() - clk; diff --git a/src/base/abci/abcUnate.c b/src/base/abci/abcUnate.c index 08a42623..88188655 100644 --- a/src/base/abci/abcUnate.c +++ b/src/base/abci/abcUnate.c @@ -73,7 +73,7 @@ void Abc_NtkPrintUnateBdd( Abc_Ntk_t * pNtk, int fUseNaive, int fVerbose ) int clkBdd, clkUnate; // compute the global BDDs - if ( Abc_NtkGlobalBdds(pNtk, 0) == NULL ) + if ( Abc_NtkGlobalBdds(pNtk, 10000000, 0) == NULL ) return; clkBdd = clock() - clk; diff --git a/src/base/abci/abcUnreach.c b/src/base/abci/abcUnreach.c index 34757145..5690013b 100644 --- a/src/base/abci/abcUnreach.c +++ b/src/base/abci/abcUnreach.c @@ -58,7 +58,7 @@ int Abc_NtkExtractSequentialDcs( Abc_Ntk_t * pNtk, bool fVerbose ) } // compute the global BDDs of the latches - dd = Abc_NtkGlobalBdds( pNtk, 1 ); + dd = Abc_NtkGlobalBdds( pNtk, 10000000, 1 ); if ( dd == NULL ) return 0; if ( fVerbose ) @@ -331,7 +331,7 @@ Abc_Ntk_t * Abc_NtkConstructExdc( DdManager * dd, Abc_Ntk_t * pNtk, DdNode * bUn Abc_NtkLogicMakeSimpleCos( pNtkNew, 0 ); // transform the network to the SOP representation - Abc_NtkBddToSop( pNtkNew ); + Abc_NtkBddToSop( pNtkNew, 0 ); return pNtkNew; } diff --git a/src/base/abci/abcVanEijk.c b/src/base/abci/abcVanEijk.c index d719df4f..c178c013 100644 --- a/src/base/abci/abcVanEijk.c +++ b/src/base/abci/abcVanEijk.c @@ -713,7 +713,7 @@ Fraig_Man_t * Abc_NtkVanEijkFraig( Abc_Ntk_t * pMulti, int fInit ) Abc_Ntk_t * Abc_NtkVanEijkDeriveExdc( Abc_Ntk_t * pNtk, Vec_Ptr_t * vClasses ) { Abc_Ntk_t * pNtkNew; - Abc_Obj_t * pClass, * pNode, * pRepr, * pObj; + Abc_Obj_t * pClass, * pNode, * pRepr, * pObj, *pObjNew; Abc_Obj_t * pMiter, * pTotal; Vec_Ptr_t * vCone; int i, k; @@ -766,6 +766,30 @@ Abc_Ntk_t * Abc_NtkVanEijkDeriveExdc( Abc_Ntk_t * pNtk, Vec_Ptr_t * vClasses ) pTotal = Abc_AigOr( pNtkNew->pManFunc, pTotal, pMiter ); } +/* + // create the only PO + pObjNew = Abc_NtkCreatePo( pNtkNew ); + // add the PO name + Abc_NtkLogicStoreName( pObjNew, "DC" ); + // add the PO + Abc_ObjAddFanin( pObjNew, pTotal ); + + // quontify the PIs existentially + pNtkNew = Abc_NtkMiterQuantifyPis( pNtkNew ); + + // get the new PO + pObjNew = Abc_NtkPo( pNtkNew, 0 ); + // remember the miter output + pTotal = Abc_ObjChild0( pObjNew ); + // remove the PO + Abc_NtkDeleteObj( pObjNew ); + + // make the old network point to the new things + Abc_NtkConst1(pNtk)->pCopy = Abc_NtkConst1(pNtkNew); + Abc_NtkForEachCi( pNtk, pObj, i ) + pObj->pCopy = Abc_NtkPi( pNtkNew, i ); +*/ + // for each CO, create PO (skip POs equal to CIs because of name conflict) Abc_NtkForEachPo( pNtk, pObj, i ) if ( !Abc_ObjIsCi(Abc_ObjFanin0(pObj)) ) diff --git a/src/base/abci/abcVanImp.c b/src/base/abci/abcVanImp.c index 1805378c..c92667a3 100644 --- a/src/base/abci/abcVanImp.c +++ b/src/base/abci/abcVanImp.c @@ -870,7 +870,7 @@ Abc_Ntk_t * Abc_NtkVanImpDeriveExdc( Abc_Ntk_t * pNtk, Vec_Ptr_t * vZeros, Vec_I { Abc_Ntk_t * pNtkNew; Vec_Ptr_t * vCone; - Abc_Obj_t * pObj, * pMiter, * pTotal, * pNode, * pNode1, * pNode2; + Abc_Obj_t * pObj, * pMiter, * pTotal, * pNode, * pNode1, * pNode2, * pObjNew; unsigned Imp; int i, k; @@ -942,6 +942,29 @@ Abc_Ntk_t * Abc_NtkVanImpDeriveExdc( Abc_Ntk_t * pNtk, Vec_Ptr_t * vZeros, Vec_I pMiter = Abc_AigAnd( pNtkNew->pManFunc, pNode1->pCopy, Abc_ObjNot(pNode2->pCopy) ); pTotal = Abc_AigOr( pNtkNew->pManFunc, pTotal, pMiter ); } +/* + // create the only PO + pObjNew = Abc_NtkCreatePo( pNtkNew ); + // add the PO name + Abc_NtkLogicStoreName( pObjNew, "DC" ); + // add the PO + Abc_ObjAddFanin( pObjNew, pTotal ); + + // quontify the PIs existentially + pNtkNew = Abc_NtkMiterQuantifyPis( pNtkNew ); + + // get the new PO + pObjNew = Abc_NtkPo( pNtkNew, 0 ); + // remember the miter output + pTotal = Abc_ObjChild0( pObjNew ); + // remove the PO + Abc_NtkDeleteObj( pObjNew ); + + // make the old network point to the new things + Abc_NtkConst1(pNtk)->pCopy = Abc_NtkConst1(pNtkNew); + Abc_NtkForEachCi( pNtk, pObj, i ) + pObj->pCopy = Abc_NtkPi( pNtkNew, i ); +*/ // for each CO, create PO (skip POs equal to CIs because of name conflict) Abc_NtkForEachPo( pNtk, pObj, i ) diff --git a/src/base/abci/abcVerify.c b/src/base/abci/abcVerify.c index 5c7b525e..718ad657 100644 --- a/src/base/abci/abcVerify.c +++ b/src/base/abci/abcVerify.c @@ -26,8 +26,6 @@ /// DECLARATIONS /// //////////////////////////////////////////////////////////////////////// -static int * Abc_NtkVerifyGetCleanModel( Abc_Ntk_t * pNtk, int nFrames ); -static int * Abc_NtkVerifySimulatePattern( Abc_Ntk_t * pNtk, int * pModel ); static void Abc_NtkVerifyReportError( Abc_Ntk_t * pNtk1, Abc_Ntk_t * pNtk2, int * pModel ); static void Abc_NtkVerifyReportErrorSeq( Abc_Ntk_t * pNtk1, Abc_Ntk_t * pNtk2, int * pModel, int nFrames ); @@ -78,7 +76,7 @@ void Abc_NtkCecSat( Abc_Ntk_t * pNtk1, Abc_Ntk_t * pNtk2, int nConfLimit, int nI } // convert the miter into a CNF - pCnf = Abc_NtkRenode( pMiter, 0, 100, 1, 0, 0 ); + pCnf = Abc_NtkRenode( pMiter, 0, 100, 1, 0, 0, 0 ); Abc_NtkDelete( pMiter ); if ( pCnf == NULL ) { @@ -235,7 +233,7 @@ void Abc_NtkSecSat( Abc_Ntk_t * pNtk1, Abc_Ntk_t * pNtk2, int nConfLimit, int nI } // convert the miter into a CNF - pCnf = Abc_NtkRenode( pFrames, 0, 100, 1, 0, 0 ); + pCnf = Abc_NtkRenode( pFrames, 0, 100, 1, 0, 0, 0 ); Abc_NtkDelete( pFrames ); if ( pCnf == NULL ) { diff --git a/src/base/abci/module.make b/src/base/abci/module.make index 3ca188b7..4339b520 100644 --- a/src/base/abci/module.make +++ b/src/base/abci/module.make @@ -19,6 +19,8 @@ SRC += src/base/abci/abc.c \ src/base/abci/abcReconv.c \ src/base/abci/abcRefactor.c \ src/base/abci/abcRenode.c \ + src/base/abci/abcRestruct.c \ + src/base/abci/abcResub.c \ src/base/abci/abcRewrite.c \ src/base/abci/abcSat.c \ src/base/abci/abcStrash.c \ diff --git a/src/base/cmd/cmd.c b/src/base/cmd/cmd.c index 21dba247..c2c09697 100644 --- a/src/base/cmd/cmd.c +++ b/src/base/cmd/cmd.c @@ -1252,7 +1252,7 @@ int CmdCommandSis( Abc_Frame_t * pAbc, int argc, char **argv ) } // write out the current network - pNetlist = Abc_NtkLogicToNetlist(pNtk); + pNetlist = Abc_NtkLogicToNetlist(pNtk,0); Io_WriteBlif( pNetlist, "_sis_in.blif", 1 ); Abc_NtkDelete( pNetlist ); @@ -1388,7 +1388,7 @@ int CmdCommandMvsis( Abc_Frame_t * pAbc, int argc, char **argv ) } // write out the current network - pNetlist = Abc_NtkLogicToNetlist(pNtk); + pNetlist = Abc_NtkLogicToNetlist(pNtk,0); Io_WriteBlif( pNetlist, "_mvsis_in.blif", 1 ); Abc_NtkDelete( pNetlist ); diff --git a/src/base/cmd/cmd.h b/src/base/cmd/cmd.h index 4e54df21..030b77e8 100644 --- a/src/base/cmd/cmd.h +++ b/src/base/cmd/cmd.h @@ -21,6 +21,10 @@ #ifndef __CMD_H__ #define __CMD_H__ +#ifdef __cplusplus +extern "C" { +#endif + //////////////////////////////////////////////////////////////////////// /// INCLUDES /// //////////////////////////////////////////////////////////////////////// @@ -57,9 +61,13 @@ extern void Cmd_FlagUpdateValue( Abc_Frame_t * pAbc, char * key, char * v /*=== cmdHist.c ========================================================*/ extern void Cmd_HistoryAddCommand( Abc_Frame_t * pAbc, char * command ); +#ifdef __cplusplus +} +#endif + +#endif + //////////////////////////////////////////////////////////////////////// /// END OF FILE /// //////////////////////////////////////////////////////////////////////// -#endif - diff --git a/src/base/io/io.c b/src/base/io/io.c index 2725eb8a..0aa5e415 100644 --- a/src/base/io/io.c +++ b/src/base/io/io.c @@ -45,6 +45,7 @@ static int IoCommandWriteGml ( Abc_Frame_t * pAbc, int argc, char **argv ); static int IoCommandWriteList ( Abc_Frame_t * pAbc, int argc, char **argv ); static int IoCommandWritePla ( Abc_Frame_t * pAbc, int argc, char **argv ); static int IoCommandWriteVerilog( Abc_Frame_t * pAbc, int argc, char **argv ); +static int IoCommandWriteCounter( Abc_Frame_t * pAbc, int argc, char **argv ); //////////////////////////////////////////////////////////////////////// /// FUNCTION DEFINITIONS /// @@ -83,6 +84,7 @@ void Io_Init( Abc_Frame_t * pAbc ) Cmd_CommandAdd( pAbc, "I/O", "write_list", IoCommandWriteList, 0 ); Cmd_CommandAdd( pAbc, "I/O", "write_pla", IoCommandWritePla, 0 ); Cmd_CommandAdd( pAbc, "I/O", "write_verilog", IoCommandWriteVerilog, 0 ); + Cmd_CommandAdd( pAbc, "I/O", "write_counter", IoCommandWriteCounter, 0 ); } /**Function************************************************************* @@ -1174,7 +1176,7 @@ int IoCommandWriteEqn( Abc_Frame_t * pAbc, int argc, char **argv ) if ( Abc_NtkIsSopLogic(pNtk) ) Abc_NtkLogicMakeDirectSops(pNtk); // derive the netlist - pNtkTemp = Abc_NtkLogicToNetlist(pNtk); + pNtkTemp = Abc_NtkLogicToNetlist(pNtk,1); if ( pNtkTemp == NULL ) { fprintf( pAbc->Out, "Writing BENCH has failed.\n" ); @@ -1358,6 +1360,12 @@ int IoCommandWritePla( Abc_Frame_t * pAbc, int argc, char **argv ) return 0; } + if ( Abc_NtkGetLevelNum(pNtk) > 1 ) + { + fprintf( pAbc->Out, "PLA writing is available for collapsed networks.\n" ); + return 0; + } + if ( Abc_NtkLatchNum(pNtk) > 0 ) { fprintf( pAbc->Out, "Latches are writed at PI/PO pairs in the PLA file.\n" ); @@ -1368,11 +1376,12 @@ int IoCommandWritePla( Abc_Frame_t * pAbc, int argc, char **argv ) { goto usage; } + // get the input file name FileName = argv[globalUtilOptind]; // derive the netlist - pNtkTemp = Abc_NtkLogicToNetlist(pNtk); + pNtkTemp = Abc_NtkLogicToNetlist(pNtk,1); if ( pNtkTemp == NULL ) { fprintf( pAbc->Out, "Writing PLA has failed.\n" ); @@ -1434,7 +1443,7 @@ int IoCommandWriteVerilog( Abc_Frame_t * pAbc, int argc, char **argv ) FileName = argv[globalUtilOptind]; // derive the netlist - pNtkTemp = Abc_NtkLogicToNetlist(pNtk); + pNtkTemp = Abc_NtkLogicToNetlist(pNtk,0); if ( pNtkTemp == NULL ) { fprintf( pAbc->Out, "Writing PLA has failed.\n" ); @@ -1452,6 +1461,96 @@ usage: return 1; } +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int IoCommandWriteCounter( Abc_Frame_t * pAbc, int argc, char **argv ) +{ + Abc_Ntk_t * pNtk; + char * FileName; + int c; + int fNames; + + fNames = 0; + Extra_UtilGetoptReset(); + while ( ( c = Extra_UtilGetopt( argc, argv, "nh" ) ) != EOF ) + { + switch ( c ) + { + case 'n': + fNames ^= 1; + break; + case 'h': + goto usage; + default: + goto usage; + } + } + + pNtk = pAbc->pNtkCur; + if ( pNtk == NULL ) + { + fprintf( pAbc->Out, "Empty network.\n" ); + return 0; + } + + if ( argc != globalUtilOptind + 1 ) + { + goto usage; + } + // get the input file name + FileName = argv[globalUtilOptind]; + + if ( pNtk->pModel == NULL ) + { + fprintf( pAbc->Out, "Counter-example is not available.\n" ); + return 0; + } + + // write the counter-example into the file + { + Abc_Obj_t * pObj; + FILE * pFile = fopen( FileName, "w" ); + int i; + if ( pFile == NULL ) + { + fprintf( stdout, "Io_WriteVerilog(): Cannot open the output file \"%s\".\n", FileName ); + return 1; + } + if ( fNames ) + { + Abc_NtkForEachPi( pNtk, pObj, i ) + fprintf( pFile, "%s=%c ", Abc_ObjName(pObj), '0'+(pNtk->pModel[i]==1) ); + } + else + { + Abc_NtkForEachPi( pNtk, pObj, i ) + fprintf( pFile, "%c", '0'+(pNtk->pModel[i]==1) ); + } + fprintf( pFile, "\n" ); + fclose( pFile ); + } + + return 0; + +usage: + fprintf( pAbc->Err, "usage: write_counter [-nh] \n" ); + fprintf( pAbc->Err, "\t writes the counter-example derived by \"prove\" or \"sat\"\n" ); + fprintf( pAbc->Err, "\t the file contains values for each PI in the natural order\n" ); + fprintf( pAbc->Err, "\t-n : write input names into the file [default = %s]\n", fNames? "yes": "no" ); + fprintf( pAbc->Err, "\t-h : print the help massage\n" ); + fprintf( pAbc->Err, "\tfile : the name of the file to write\n" ); + return 1; +} + //////////////////////////////////////////////////////////////////////// /// END OF FILE /// diff --git a/src/base/io/io.h b/src/base/io/io.h index fe5c237f..a9a61040 100644 --- a/src/base/io/io.h +++ b/src/base/io/io.h @@ -21,6 +21,10 @@ #ifndef __IO_H__ #define __IO_H__ +#ifdef __cplusplus +extern "C" { +#endif + //////////////////////////////////////////////////////////////////////// /// INCLUDES /// //////////////////////////////////////////////////////////////////////// @@ -94,9 +98,13 @@ extern int Io_WritePla( Abc_Ntk_t * pNtk, char * FileName ); /*=== abcWriteVerilog.c ==========================================================*/ extern void Io_WriteVerilog( Abc_Ntk_t * pNtk, char * FileName ); +#ifdef __cplusplus +} +#endif + +#endif + //////////////////////////////////////////////////////////////////////// /// END OF FILE /// //////////////////////////////////////////////////////////////////////// -#endif - diff --git a/src/base/io/ioInt.h b/src/base/io/ioInt.h index 7f4e200e..3daf3c75 100644 --- a/src/base/io/ioInt.h +++ b/src/base/io/ioInt.h @@ -41,9 +41,9 @@ /// FUNCTION DECLARATIONS /// //////////////////////////////////////////////////////////////////////// +#endif + //////////////////////////////////////////////////////////////////////// /// END OF FILE /// //////////////////////////////////////////////////////////////////////// -#endif - diff --git a/src/base/io/ioWriteBlif.c b/src/base/io/ioWriteBlif.c index 6b6c4a92..1b515a1e 100644 --- a/src/base/io/ioWriteBlif.c +++ b/src/base/io/ioWriteBlif.c @@ -53,7 +53,7 @@ void Io_WriteBlifLogic( Abc_Ntk_t * pNtk, char * FileName, int fWriteLatches ) { Abc_Ntk_t * pNtkTemp; // derive the netlist - pNtkTemp = Abc_NtkLogicToNetlist(pNtk); + pNtkTemp = Abc_NtkLogicToNetlist(pNtk,0); if ( pNtkTemp == NULL ) { fprintf( stdout, "Writing BLIF has failed.\n" ); diff --git a/src/base/io/ioWriteDot.c b/src/base/io/ioWriteDot.c index 373c4636..dbf157bf 100644 --- a/src/base/io/ioWriteDot.c +++ b/src/base/io/ioWriteDot.c @@ -412,7 +412,7 @@ void Io_WriteDotNtk( Abc_Ntk_t * pNtk, Vec_Ptr_t * vNodes, Vec_Ptr_t * vNodesSho // transform logic functions from BDD to SOP if ( fHasBdds = Abc_NtkIsBddLogic(pNtk) ) - Abc_NtkBddToSop(pNtk); + Abc_NtkBddToSop(pNtk, 0); // mark the nodes from the set Vec_PtrForEachEntry( vNodes, pNode, i ) diff --git a/src/base/io/ioWritePla.c b/src/base/io/ioWritePla.c index 12ac9ef7..4da8aca8 100644 --- a/src/base/io/ioWritePla.c +++ b/src/base/io/ioWritePla.c @@ -88,7 +88,7 @@ int Io_WritePlaOne( FILE * pFile, Abc_Ntk_t * pNtk ) nProducts = 0; Abc_NtkForEachCo( pNtk, pNode, i ) { - pDriver = Abc_ObjFanin0Ntk(pNode); + pDriver = Abc_ObjFanin0Ntk( Abc_ObjFanin0(pNode) ); if ( !Abc_ObjIsNode(pDriver) ) { nProducts++; @@ -138,9 +138,10 @@ int Io_WritePlaOne( FILE * pFile, Abc_Ntk_t * pNtk ) pCubeOut[i] = '1'; // consider special cases of nodes - pDriver = Abc_ObjFanin0Ntk(pNode); + pDriver = Abc_ObjFanin0Ntk( Abc_ObjFanin0(pNode) ); if ( !Abc_ObjIsNode(pDriver) ) { + assert( Abc_ObjIsCi(pDriver) ); pCubeIn[(int)pDriver->pCopy] = '1' - Abc_ObjFaninC0(pNode); fprintf( pFile, "%s %s\n", pCubeIn, pCubeOut ); pCubeIn[(int)pDriver->pCopy] = '-'; @@ -152,17 +153,29 @@ int Io_WritePlaOne( FILE * pFile, Abc_Ntk_t * pNtk ) fprintf( pFile, "%s %s\n", pCubeIn, pCubeOut ); continue; } + + // make sure the cover is not complemented + assert( !Abc_SopIsComplement( pDriver->pData ) ); + // write the cubes nFanins = Abc_ObjFaninNum(pDriver); Abc_SopForEachCube( pDriver->pData, nFanins, pCube ) { Abc_ObjForEachFanin( pDriver, pFanin, k ) + { + pFanin = Abc_ObjFanin0Ntk(pFanin); + assert( (int)pFanin->pCopy < nInputs ); pCubeIn[(int)pFanin->pCopy] = pCube[k]; + } fprintf( pFile, "%s %s\n", pCubeIn, pCubeOut ); } // clean the cube for future writing Abc_ObjForEachFanin( pDriver, pFanin, k ) + { + pFanin = Abc_ObjFanin0Ntk(pFanin); + assert( Abc_ObjIsCi(pFanin) ); pCubeIn[(int)pFanin->pCopy] = '-'; + } Extra_ProgressBarUpdate( pProgress, i, NULL ); } Extra_ProgressBarStop( pProgress ); @@ -171,6 +184,8 @@ int Io_WritePlaOne( FILE * pFile, Abc_Ntk_t * pNtk ) // clean the CI nodes Abc_NtkForEachCi( pNtk, pNode, i ) pNode->pCopy = NULL; + free( pCubeIn ); + free( pCubeOut ); return 1; } diff --git a/src/base/main/main.h b/src/base/main/main.h index d5a463f5..9b483904 100644 --- a/src/base/main/main.h +++ b/src/base/main/main.h @@ -21,6 +21,10 @@ #ifndef __MAIN_H__ #define __MAIN_H__ +#ifdef __cplusplus +extern "C" { +#endif + //////////////////////////////////////////////////////////////////////// /// TYPEDEFS /// //////////////////////////////////////////////////////////////////////// @@ -104,8 +108,12 @@ extern void Abc_FrameSetLibGen( void * pLib ); extern void Abc_FrameSetLibSuper( void * pLib ); extern void Abc_FrameSetFlag( char * pFlag, char * pValue ); +#ifdef __cplusplus +} +#endif + +#endif + //////////////////////////////////////////////////////////////////////// /// END OF FILE /// //////////////////////////////////////////////////////////////////////// - -#endif diff --git a/src/base/main/mainInt.h b/src/base/main/mainInt.h index ec932838..d2bca1ab 100644 --- a/src/base/main/mainInt.h +++ b/src/base/main/mainInt.h @@ -102,8 +102,8 @@ extern void Abc_UtilsPrintHello( Abc_Frame_t * pAbc ); extern void Abc_UtilsPrintUsage( Abc_Frame_t * pAbc, char * ProgName ); extern void Abc_UtilsSource( Abc_Frame_t * pAbc ); +#endif + //////////////////////////////////////////////////////////////////////// /// END OF FILE /// //////////////////////////////////////////////////////////////////////// - -#endif diff --git a/src/base/seq/seq.h b/src/base/seq/seq.h index cba15e47..b66799b5 100644 --- a/src/base/seq/seq.h +++ b/src/base/seq/seq.h @@ -21,6 +21,10 @@ #ifndef __SEQ_H__ #define __SEQ_H__ +#ifdef __cplusplus +extern "C" { +#endif + //////////////////////////////////////////////////////////////////////// /// INCLUDES /// //////////////////////////////////////////////////////////////////////// @@ -82,9 +86,13 @@ extern int Seq_MapComputeAreaFlows( Abc_Ntk_t * pNtk, int fVerbose ) extern Vec_Ptr_t * Seq_NtkReachNodes( Abc_Ntk_t * pNtk, int fFromPos ); extern int Seq_NtkCleanup( Abc_Ntk_t * pNtk, int fVerbose ); +#ifdef __cplusplus +} +#endif + +#endif + //////////////////////////////////////////////////////////////////////// /// END OF FILE /// //////////////////////////////////////////////////////////////////////// -#endif - diff --git a/src/base/seq/seqInt.h b/src/base/seq/seqInt.h index 3d3d0804..221efc91 100644 --- a/src/base/seq/seqInt.h +++ b/src/base/seq/seqInt.h @@ -21,6 +21,10 @@ #ifndef __SEQ_INT_H__ #define __SEQ_INT_H__ +#ifdef __cplusplus +extern "C" { +#endif + //////////////////////////////////////////////////////////////////////// /// INCLUDES /// //////////////////////////////////////////////////////////////////////// @@ -240,9 +244,13 @@ extern int Seq_ObjFanoutLMin( Abc_Obj_t * pObj ); extern int Seq_ObjFanoutLSum( Abc_Obj_t * pObj ); extern int Seq_ObjFaninLSum( Abc_Obj_t * pObj ); +#ifdef __cplusplus +} +#endif + +#endif + //////////////////////////////////////////////////////////////////////// /// END OF FILE /// //////////////////////////////////////////////////////////////////////// -#endif - diff --git a/src/base/seq/seqRetCore.c b/src/base/seq/seqRetCore.c index 4aba069d..0805a838 100644 --- a/src/base/seq/seqRetCore.c +++ b/src/base/seq/seqRetCore.c @@ -107,7 +107,7 @@ Abc_Ntk_t * Seq_NtkRetimeDerive( Abc_Ntk_t * pNtk, int fVerbose ) // transform logic functions from BDD to SOP if ( fHasBdds = Abc_NtkIsBddLogic(pNtk) ) - Abc_NtkBddToSop(pNtk); + Abc_NtkBddToSop(pNtk, 0); // start the network pNtkNew = Abc_NtkAlloc( ABC_NTK_SEQ, ABC_FUNC_AIG ); diff --git a/src/bdd/dsd/dsd.h b/src/bdd/dsd/dsd.h index 04385933..a3fc4948 100644 --- a/src/bdd/dsd/dsd.h +++ b/src/bdd/dsd/dsd.h @@ -28,6 +28,10 @@ #ifndef __DSD_H__ #define __DSD_H__ +#ifdef __cplusplus +extern "C" { +#endif + //////////////////////////////////////////////////////////////////////// /// TYPEDEF DEFINITIONS /// //////////////////////////////////////////////////////////////////////// @@ -114,8 +118,12 @@ extern void Dsd_NodePrint( FILE * pFile, Dsd_Node_t * pNode ); /*=== dsdLocal.c =======================================================*/ extern DdNode * Dsd_TreeGetPrimeFunction( DdManager * dd, Dsd_Node_t * pNode ); +#ifdef __cplusplus +} +#endif + +#endif + //////////////////////////////////////////////////////////////////////// /// END OF FILE /// //////////////////////////////////////////////////////////////////////// - -#endif \ No newline at end of file diff --git a/src/bdd/dsd/dsdInt.h b/src/bdd/dsd/dsdInt.h index 5569c443..62ce7e99 100644 --- a/src/bdd/dsd/dsdInt.h +++ b/src/bdd/dsd/dsdInt.h @@ -83,9 +83,9 @@ extern void Dsd_TreeNodeDelete( DdManager * dd, Dsd_Node_t * pNode ); extern void Dsd_TreeUnmark( Dsd_Manager_t * dMan ); extern DdNode * Dsd_TreeGetPrimeFunctionOld( DdManager * dd, Dsd_Node_t * pNode, int fRemap ); +#endif + //////////////////////////////////////////////////////////////////////// /// END OF FILE /// //////////////////////////////////////////////////////////////////////// - -#endif \ No newline at end of file diff --git a/src/bdd/parse/parse.h b/src/bdd/parse/parse.h index c16c8991..4923fbdd 100644 --- a/src/bdd/parse/parse.h +++ b/src/bdd/parse/parse.h @@ -47,7 +47,8 @@ extern DdNode * Parse_FormulaParser( FILE * pOutput, char * pFormula, int nVars, int nRanks, char * ppVarNames[], DdManager * dd, DdNode * pbVars[] ); +#endif + //////////////////////////////////////////////////////////////////////// /// END OF FILE /// //////////////////////////////////////////////////////////////////////// -#endif diff --git a/src/bdd/parse/parseInt.h b/src/bdd/parse/parseInt.h index 14623681..a1730f2c 100644 --- a/src/bdd/parse/parseInt.h +++ b/src/bdd/parse/parseInt.h @@ -67,7 +67,8 @@ extern void Parse_StackOpPush ( Parse_StackOp_t * p, int Oper ); extern int Parse_StackOpPop ( Parse_StackOp_t * p ); extern void Parse_StackOpFree ( Parse_StackOp_t * p ); +#endif + //////////////////////////////////////////////////////////////////////// /// END OF FILE /// //////////////////////////////////////////////////////////////////////// -#endif diff --git a/src/bdd/reo/reo.h b/src/bdd/reo/reo.h index 7e4be855..45667768 100644 --- a/src/bdd/reo/reo.h +++ b/src/bdd/reo/reo.h @@ -19,6 +19,10 @@ #ifndef __REO_H__ #define __REO_H__ +#ifdef __cplusplus +extern "C" { +#endif + #include #include #include "extra.h" @@ -215,8 +219,12 @@ extern DdNode * Extra_ReorderCudd( DdManager * dd, DdNode * aFunc, int pPermut extern int Extra_bddReorderTest( DdManager * dd, DdNode * bF ); extern int Extra_addReorderTest( DdManager * dd, DdNode * aF ); +#ifdef __cplusplus +} +#endif + +#endif + //////////////////////////////////////////////////////////////////////// /// END OF FILE /// //////////////////////////////////////////////////////////////////////// - -#endif diff --git a/src/generic.h b/src/generic.h index f634ea1c..e17d2edf 100644 --- a/src/generic.h +++ b/src/generic.h @@ -21,6 +21,10 @@ #ifndef __zzz_H__ #define __zzz_H__ +#ifdef __cplusplus +extern "C" { +#endif + //////////////////////////////////////////////////////////////////////// /// INCLUDES /// //////////////////////////////////////////////////////////////////////// @@ -42,10 +46,14 @@ //////////////////////////////////////////////////////////////////////// /*=== zzz.c ==========================================================*/ + +#ifdef __cplusplus +} +#endif + +#endif //////////////////////////////////////////////////////////////////////// /// END OF FILE /// //////////////////////////////////////////////////////////////////////// -#endif - diff --git a/src/map/fpga/fpga.h b/src/map/fpga/fpga.h index 51868188..bbb95984 100644 --- a/src/map/fpga/fpga.h +++ b/src/map/fpga/fpga.h @@ -19,6 +19,10 @@ #ifndef __FPGA_H__ #define __FPGA_H__ +#ifdef __cplusplus +extern "C" { +#endif + //////////////////////////////////////////////////////////////////////// /// INCLUDES /// //////////////////////////////////////////////////////////////////////// @@ -153,8 +157,12 @@ extern int Fpga_ManCheckConsistency( Fpga_Man_t * p ); extern void Fpga_ManCleanData0( Fpga_Man_t * pMan ); extern Fpga_NodeVec_t * Fpga_CollectNodeTfo( Fpga_Man_t * pMan, Fpga_Node_t * pNode ); +#ifdef __cplusplus +} +#endif + +#endif //////////////////////////////////////////////////////////////////////// /// END OF FILE /// //////////////////////////////////////////////////////////////////////// -#endif diff --git a/src/map/fpga/fpgaInt.h b/src/map/fpga/fpgaInt.h index b6ac71d4..3a35d6dc 100644 --- a/src/map/fpga/fpgaInt.h +++ b/src/map/fpga/fpgaInt.h @@ -376,8 +376,8 @@ extern void Fpga_MappingSetChoiceLevels( Fpga_Man_t * pMan ); /*=== CUDD package.c ===============================================================*/ extern unsigned int Cudd_Prime( unsigned int p ); +#endif + //////////////////////////////////////////////////////////////////////// /// END OF FILE /// //////////////////////////////////////////////////////////////////////// - -#endif diff --git a/src/map/fpga/fpgaTruth.c b/src/map/fpga/fpgaTruth.c index 11660731..e3eb487f 100644 --- a/src/map/fpga/fpgaTruth.c +++ b/src/map/fpga/fpgaTruth.c @@ -94,8 +94,7 @@ void * Fpga_TruthsCutBdd( void * dd, Fpga_Cut_t * pCut ) Cudd_RecursiveDeref( dd, (DdNode*)pCut->uSign ); pCut->uSign = 0; } - printf( "%d ", vVisited->nSize ); - +// printf( "%d ", vVisited->nSize ); Fpga_NodeVecFree( vVisited ); Cudd_Deref( bFunc ); return bFunc; diff --git a/src/map/mapper/mapper.h b/src/map/mapper/mapper.h index 9b059fd0..10839382 100644 --- a/src/map/mapper/mapper.h +++ b/src/map/mapper/mapper.h @@ -19,6 +19,10 @@ #ifndef __MAPPER_H__ #define __MAPPER_H__ +#ifdef __cplusplus +extern "C" { +#endif + //////////////////////////////////////////////////////////////////////// /// INCLUDES /// //////////////////////////////////////////////////////////////////////// @@ -180,7 +184,12 @@ extern void Map_ManCleanData( Map_Man_t * p ); extern void Map_MappingSetupTruthTables( unsigned uTruths[][2] ); extern void Map_MappingSetupTruthTablesLarge( unsigned uTruths[][32] ); +#ifdef __cplusplus +} +#endif + +#endif + //////////////////////////////////////////////////////////////////////// /// END OF FILE /// //////////////////////////////////////////////////////////////////////// -#endif diff --git a/src/map/mapper/mapperInt.h b/src/map/mapper/mapperInt.h index fd7ac946..a3a2cf40 100644 --- a/src/map/mapper/mapperInt.h +++ b/src/map/mapper/mapperInt.h @@ -470,8 +470,8 @@ extern void Map_NodeVecWriteEntry( Map_NodeVec_t * p, int i, Map_No extern Map_Node_t * Map_NodeVecReadEntry( Map_NodeVec_t * p, int i ); extern void Map_NodeVecSortByLevel( Map_NodeVec_t * p ); +#endif + //////////////////////////////////////////////////////////////////////// /// END OF FILE /// //////////////////////////////////////////////////////////////////////// - -#endif diff --git a/src/map/mio/mio.h b/src/map/mio/mio.h index 0e2c085d..dabc05dd 100644 --- a/src/map/mio/mio.h +++ b/src/map/mio/mio.h @@ -19,6 +19,10 @@ #ifndef __MIO_H__ #define __MIO_H__ +#ifdef __cplusplus +extern "C" { +#endif + //////////////////////////////////////////////////////////////////////// /// INCLUDES /// //////////////////////////////////////////////////////////////////////// @@ -133,7 +137,13 @@ extern void Mio_DeriveGateDelays( Mio_Gate_t * pGate, float * ptDelaysRes, float * ptPinDelayMax ); extern Mio_Gate_t * Mio_GateCreatePseudo( int nInputs ); +#ifdef __cplusplus +} +#endif + +#endif + //////////////////////////////////////////////////////////////////////// /// END OF FILE /// //////////////////////////////////////////////////////////////////////// -#endif + diff --git a/src/map/mio/mioInt.h b/src/map/mio/mioInt.h index a25ca026..3f90b625 100644 --- a/src/map/mio/mioInt.h +++ b/src/map/mio/mioInt.h @@ -118,8 +118,8 @@ struct Mio_PinStruct_t_ /*=== mioRead.c =============================================================*/ /*=== mioUtils.c =============================================================*/ +#endif + //////////////////////////////////////////////////////////////////////// /// END OF FILE /// //////////////////////////////////////////////////////////////////////// - -#endif diff --git a/src/map/pga/pga.h b/src/map/pga/pga.h index ac129c7f..4b2a9df4 100644 --- a/src/map/pga/pga.h +++ b/src/map/pga/pga.h @@ -21,6 +21,10 @@ #ifndef __PGA_H__ #define __PGA_H__ +#ifdef __cplusplus +extern "C" { +#endif + //////////////////////////////////////////////////////////////////////// /// INCLUDES /// //////////////////////////////////////////////////////////////////////// @@ -64,9 +68,13 @@ extern Vec_Ptr_t * Pga_DoMapping( Pga_Man_t * p ); extern Pga_Man_t * Pga_ManStart( Pga_Params_t * pParams ); extern void Pga_ManStop( Pga_Man_t * p ); +#ifdef __cplusplus +} +#endif + +#endif + //////////////////////////////////////////////////////////////////////// /// END OF FILE /// //////////////////////////////////////////////////////////////////////// -#endif - diff --git a/src/map/pga/pgaInt.h b/src/map/pga/pgaInt.h index 65832c8d..da9aa9a9 100644 --- a/src/map/pga/pgaInt.h +++ b/src/map/pga/pgaInt.h @@ -124,9 +124,9 @@ extern float Pga_MappingSetRefsAndArea( Pga_Man_t * p ); extern float Pga_MappingGetSwitching( Pga_Man_t * p ); extern void Pga_MappingPrintOutputArrivals( Pga_Man_t * p ); +#endif + //////////////////////////////////////////////////////////////////////// /// END OF FILE /// //////////////////////////////////////////////////////////////////////// -#endif - diff --git a/src/map/super/super.h b/src/map/super/super.h index 9d475116..a7169924 100644 --- a/src/map/super/super.h +++ b/src/map/super/super.h @@ -19,6 +19,10 @@ #ifndef __SUPER_H__ #define __SUPER_H__ +#ifdef __cplusplus +extern "C" { +#endif + //////////////////////////////////////////////////////////////////////// /// INCLUDES /// //////////////////////////////////////////////////////////////////////// @@ -44,8 +48,13 @@ //////////////////////////////////////////////////////////////////////// /*=== superCore.c =============================================================*/ + +#ifdef __cplusplus +} +#endif + +#endif //////////////////////////////////////////////////////////////////////// /// END OF FILE /// //////////////////////////////////////////////////////////////////////// -#endif diff --git a/src/map/super/superInt.h b/src/map/super/superInt.h index 97ed4c5a..ec6d0a38 100644 --- a/src/map/super/superInt.h +++ b/src/map/super/superInt.h @@ -55,8 +55,8 @@ extern void Super2_Precompute( int nInputs, int nLevels, int fVerbose ); /*=== superGate.c =============================================================*/ extern void Super_Precompute( Mio_Library_t * pLibGen, int nInputs, int nLevels, float tDelayMax, float tAreaMax, int TimeLimit, bool fSkipInv, bool fWriteOldFormat, int fVerbose ); +#endif + //////////////////////////////////////////////////////////////////////// /// END OF FILE /// //////////////////////////////////////////////////////////////////////// - -#endif diff --git a/src/misc/extra/extra.h b/src/misc/extra/extra.h index 666d7388..1b6abaa6 100644 --- a/src/misc/extra/extra.h +++ b/src/misc/extra/extra.h @@ -29,6 +29,10 @@ #ifndef __EXTRA_H__ #define __EXTRA_H__ +#ifdef __cplusplus +extern "C" { +#endif + #ifdef _WIN32 #define inline __inline // compatible with MS VS 6.0 #endif @@ -434,4 +438,8 @@ extern int globalUtilOptind; /**AutomaticEnd***************************************************************/ +#ifdef __cplusplus +} +#endif + #endif /* __EXTRA_H__ */ diff --git a/src/misc/mvc/mvc.h b/src/misc/mvc/mvc.h index 363b1e57..650f698d 100644 --- a/src/misc/mvc/mvc.h +++ b/src/misc/mvc/mvc.h @@ -724,9 +724,9 @@ extern Mvc_Manager_t * Mvc_ManagerAllocCube( int nWords ); extern Mvc_Manager_t * Mvc_ManagerFreeCover( Mvc_Cover_t * pCover ); extern Mvc_Manager_t * Mvc_ManagerFreeCube( Mvc_Cover_t * pCube, int nWords ); +#endif + //////////////////////////////////////////////////////////////////////// /// END OF FILE /// //////////////////////////////////////////////////////////////////////// -#endif - diff --git a/src/misc/st/st.h b/src/misc/st/st.h index 1802cf9b..b15f3c83 100644 --- a/src/misc/st/st.h +++ b/src/misc/st/st.h @@ -14,6 +14,10 @@ #ifndef ST_INCLUDED #define ST_INCLUDED +#ifdef __cplusplus +extern "C" { +#endif + typedef struct st_table_entry st_table_entry; struct st_table_entry { char *key; @@ -85,4 +89,8 @@ extern void st_free_gen (st_generator *); #define ST_OUT_OF_MEM -10000 +#ifdef __cplusplus +} +#endif + #endif /* ST_INCLUDED */ diff --git a/src/misc/st/stmm.h b/src/misc/st/stmm.h index d7b8a3f3..4330416e 100644 --- a/src/misc/st/stmm.h +++ b/src/misc/st/stmm.h @@ -14,6 +14,10 @@ #ifndef STMM_INCLUDED #define STMM_INCLUDED +#ifdef __cplusplus +extern "C" { +#endif + #include "extra.h" typedef struct stmm_table_entry stmm_table_entry; @@ -116,4 +120,8 @@ EXTERN void stmm_clean ARGS ((stmm_table *)); */ +#ifdef __cplusplus +} +#endif + #endif /* STMM_INCLUDED */ diff --git a/src/misc/util/util_hack.h b/src/misc/util/util_hack.h index 57914c47..a9b90e61 100644 --- a/src/misc/util/util_hack.h +++ b/src/misc/util/util_hack.h @@ -21,6 +21,10 @@ #ifndef __UTIL_HACK_H__ #define __UTIL_HACK_H__ +#ifdef __cplusplus +extern "C" { +#endif + #include #include #include @@ -84,4 +88,8 @@ extern char * Extra_UtilFileSearch( char *file, char *path, char *mode ); extern char * globalUtilOptarg; extern int globalUtilOptind; +#ifdef __cplusplus +} +#endif + #endif diff --git a/src/misc/vec/vec.h b/src/misc/vec/vec.h index f5ecf9bd..6ab23298 100644 --- a/src/misc/vec/vec.h +++ b/src/misc/vec/vec.h @@ -21,6 +21,10 @@ #ifndef __VEC_H__ #define __VEC_H__ +#ifdef __cplusplus +extern "C" { +#endif + //////////////////////////////////////////////////////////////////////// /// INCLUDES /// //////////////////////////////////////////////////////////////////////// @@ -50,9 +54,13 @@ /// FUNCTION DECLARATIONS /// //////////////////////////////////////////////////////////////////////// +#ifdef __cplusplus +} +#endif + +#endif + //////////////////////////////////////////////////////////////////////// /// END OF FILE /// //////////////////////////////////////////////////////////////////////// -#endif - diff --git a/src/misc/vec/vecInt.h b/src/misc/vec/vecInt.h index 06526332..ee848df7 100644 --- a/src/misc/vec/vecInt.h +++ b/src/misc/vec/vecInt.h @@ -696,9 +696,9 @@ static inline void Vec_IntSortUnsigned( Vec_Int_t * p ) (int (*)(const void *, const void *)) Vec_IntSortCompareUnsigned ); } +#endif + //////////////////////////////////////////////////////////////////////// /// END OF FILE /// //////////////////////////////////////////////////////////////////////// -#endif - diff --git a/src/misc/vec/vecPtr.h b/src/misc/vec/vecPtr.h index 66198eb0..65314af6 100644 --- a/src/misc/vec/vecPtr.h +++ b/src/misc/vec/vecPtr.h @@ -529,10 +529,10 @@ static inline void Vec_PtrSort( Vec_Ptr_t * p, int (*Vec_PtrSortCompare)() ) (int (*)(const void *, const void *)) Vec_PtrSortCompare ); } +#endif + //////////////////////////////////////////////////////////////////////// /// END OF FILE /// //////////////////////////////////////////////////////////////////////// -#endif - diff --git a/src/misc/vec/vecStr.h b/src/misc/vec/vecStr.h index 86a5046a..5549d374 100644 --- a/src/misc/vec/vecStr.h +++ b/src/misc/vec/vecStr.h @@ -501,9 +501,9 @@ static inline void Vec_StrSort( Vec_Str_t * p, int fReverse ) (int (*)(const void *, const void *)) Vec_StrSortCompare1 ); } +#endif + //////////////////////////////////////////////////////////////////////// /// END OF FILE /// //////////////////////////////////////////////////////////////////////// -#endif - diff --git a/src/misc/vec/vecVec.h b/src/misc/vec/vecVec.h index f95b334c..8518184a 100644 --- a/src/misc/vec/vecVec.h +++ b/src/misc/vec/vecVec.h @@ -256,9 +256,9 @@ static inline void Vec_VecPushUnique( Vec_Vec_t * p, int Level, void * Entry ) Vec_PtrPushUnique( (Vec_Ptr_t*)p->pArray[Level], Entry ); } +#endif + //////////////////////////////////////////////////////////////////////// /// END OF FILE /// //////////////////////////////////////////////////////////////////////// -#endif - diff --git a/src/opt/cut/cut.h b/src/opt/cut/cut.h index b724c976..0a1cd41a 100644 --- a/src/opt/cut/cut.h +++ b/src/opt/cut/cut.h @@ -21,6 +21,10 @@ #ifndef __CUT_H__ #define __CUT_H__ +#ifdef __cplusplus +extern "C" { +#endif + //////////////////////////////////////////////////////////////////////// /// INCLUDES /// //////////////////////////////////////////////////////////////////////// @@ -133,9 +137,13 @@ extern void Cut_OracleTryDroppingCuts( Cut_Oracle_t * p, int Node ); /*=== cutTruth.c ==========================================================*/ extern void Cut_TruthCanonicize( Cut_Cut_t * pCut ); +#ifdef __cplusplus +} +#endif + +#endif + //////////////////////////////////////////////////////////////////////// /// END OF FILE /// //////////////////////////////////////////////////////////////////////// -#endif - diff --git a/src/opt/cut/cutInt.h b/src/opt/cut/cutInt.h index eca2fcd5..375d2213 100644 --- a/src/opt/cut/cutInt.h +++ b/src/opt/cut/cutInt.h @@ -141,9 +141,9 @@ extern int Cut_TableReadTime( Cut_HashTable_t * pTable ); /*=== cutTruth.c ==========================================================*/ extern void Cut_TruthCompute( Cut_Cut_t * pCut, Cut_Cut_t * pCut0, Cut_Cut_t * pCut1, int fCompl0, int fCompl1 ); +#endif + //////////////////////////////////////////////////////////////////////// /// END OF FILE /// //////////////////////////////////////////////////////////////////////// -#endif - diff --git a/src/opt/cut/cutList.h b/src/opt/cut/cutList.h index 12db2207..a03ec9d5 100644 --- a/src/opt/cut/cutList.h +++ b/src/opt/cut/cutList.h @@ -199,9 +199,9 @@ static inline Cut_Cut_t * Cut_ListFinish( Cut_List_t * p ) return pHead; } +#endif + //////////////////////////////////////////////////////////////////////// /// END OF FILE /// //////////////////////////////////////////////////////////////////////// -#endif - diff --git a/src/opt/dec/dec.h b/src/opt/dec/dec.h index 7b8b2e94..2987723f 100644 --- a/src/opt/dec/dec.h +++ b/src/opt/dec/dec.h @@ -21,6 +21,10 @@ #ifndef __DEC_H__ #define __DEC_H__ +#ifdef __cplusplus +extern "C" { +#endif + //////////////////////////////////////////////////////////////////////// /// INCLUDES /// //////////////////////////////////////////////////////////////////////// @@ -699,9 +703,13 @@ static inline Dec_Edge_t Dec_GraphAddNodeMux( Dec_Graph_t * pGraph, Dec_Edge_t e return eNode; } +#ifdef __cplusplus +} +#endif + +#endif + //////////////////////////////////////////////////////////////////////// /// END OF FILE /// //////////////////////////////////////////////////////////////////////// -#endif - diff --git a/src/opt/dec/decAbc.c b/src/opt/dec/decAbc.c index 066b3bb2..af76cd84 100644 --- a/src/opt/dec/decAbc.c +++ b/src/opt/dec/decAbc.c @@ -18,7 +18,7 @@ #include "abc.h" #include "dec.h" -#include "aig.h" +//#include "aig.h" //////////////////////////////////////////////////////////////////////// /// DECLARATIONS /// @@ -214,6 +214,7 @@ void Dec_GraphUpdateNetwork( Abc_Obj_t * pRoot, Dec_Graph_t * pGraph, bool fUpda SeeAlso [] ***********************************************************************/ +/* Aig_Node_t * Dec_GraphToNetworkAig( Aig_Man_t * pMan, Dec_Graph_t * pGraph ) { Dec_Node_t * pNode; @@ -235,7 +236,7 @@ Aig_Node_t * Dec_GraphToNetworkAig( Aig_Man_t * pMan, Dec_Graph_t * pGraph ) // complement the result if necessary return Aig_NotCond( pNode->pFunc, Dec_GraphIsComplement(pGraph) ); } - +*/ //////////////////////////////////////////////////////////////////////// /// END OF FILE /// diff --git a/src/opt/fxu/fxu.h b/src/opt/fxu/fxu.h index df43b6b3..6a1bb5e3 100644 --- a/src/opt/fxu/fxu.h +++ b/src/opt/fxu/fxu.h @@ -19,6 +19,10 @@ #ifndef __FXU_H__ #define __FXU_H__ +#ifdef __cplusplus +extern "C" { +#endif + //////////////////////////////////////////////////////////////////////// /// INCLUDES /// //////////////////////////////////////////////////////////////////////// @@ -74,9 +78,13 @@ struct FxuDataStruct /*===== fxu.c ==========================================================*/ extern int Fxu_FastExtract( Fxu_Data_t * pData ); +#ifdef __cplusplus +} +#endif + +#endif + //////////////////////////////////////////////////////////////////////// /// END OF FILE /// //////////////////////////////////////////////////////////////////////// -#endif - diff --git a/src/opt/fxu/fxuInt.h b/src/opt/fxu/fxuInt.h index d82a68db..0ae1d79e 100644 --- a/src/opt/fxu/fxuInt.h +++ b/src/opt/fxu/fxuInt.h @@ -529,8 +529,9 @@ extern int Fxu_HeapSingleReadMaxWeight( Fxu_HeapSingle * p ); extern Fxu_Single * Fxu_HeapSingleReadMax( Fxu_HeapSingle * p ); extern Fxu_Single * Fxu_HeapSingleGetMax( Fxu_HeapSingle * p ); +#endif + //////////////////////////////////////////////////////////////////////// /// END OF FILE /// //////////////////////////////////////////////////////////////////////// -#endif diff --git a/src/opt/rwr/rwr.h b/src/opt/rwr/rwr.h index 70e1070b..8de225e8 100644 --- a/src/opt/rwr/rwr.h +++ b/src/opt/rwr/rwr.h @@ -21,6 +21,10 @@ #ifndef __RWR_H__ #define __RWR_H__ +#ifdef __cplusplus +extern "C" { +#endif + //////////////////////////////////////////////////////////////////////// /// INCLUDES /// //////////////////////////////////////////////////////////////////////// @@ -145,9 +149,13 @@ extern void Rwr_ManLoadFromFile( Rwr_Man_t * p, char * pFileName ); extern void Rwr_ListAddToTail( Rwr_Node_t ** ppList, Rwr_Node_t * pNode ); extern char * Rwr_ManGetPractical( Rwr_Man_t * p ); +#ifdef __cplusplus +} +#endif + +#endif + //////////////////////////////////////////////////////////////////////// /// END OF FILE /// //////////////////////////////////////////////////////////////////////// -#endif - diff --git a/src/opt/sim/sim.h b/src/opt/sim/sim.h index 963f0ad6..7f32fc34 100644 --- a/src/opt/sim/sim.h +++ b/src/opt/sim/sim.h @@ -21,6 +21,10 @@ #ifndef __SIM_H__ #define __SIM_H__ +#ifdef __cplusplus +extern "C" { +#endif + /* The ideas realized in this package are described in the paper: "Detecting Symmetries in Boolean Functions using Circuit Representation, @@ -217,9 +221,13 @@ extern int Sim_UtilCountAllPairs( Vec_Ptr_t * vSuppFun, int nSimWord extern void Sim_UtilCountPairsAll( Sym_Man_t * p ); extern int Sim_UtilMatrsAreDisjoint( Sym_Man_t * p ); +#ifdef __cplusplus +} +#endif + +#endif + //////////////////////////////////////////////////////////////////////// /// END OF FILE /// //////////////////////////////////////////////////////////////////////// -#endif - diff --git a/src/opt/xyz/xyz.h b/src/opt/xyz/xyz.h index ea488068..4fec2150 100644 --- a/src/opt/xyz/xyz.h +++ b/src/opt/xyz/xyz.h @@ -18,6 +18,13 @@ ***********************************************************************/ +#ifndef __XYZ_H__ +#define __XYZ_H__ + +#ifdef __cplusplus +extern "C" { +#endif + #include "abc.h" #include "xyzInt.h" @@ -89,8 +96,15 @@ extern void Abc_NodeXyzDropData( Xyz_Man_t * p, Abc_Obj_t * pObj ); /*=== xyzTest.c ===========================================================*/ extern Abc_Ntk_t * Abc_NtkXyzTestSop( Abc_Ntk_t * pNtk ); +#ifdef __cplusplus +} +#endif + +#endif + //////////////////////////////////////////////////////////////////////// /// END OF FILE /// //////////////////////////////////////////////////////////////////////// + diff --git a/src/sat/aig/aig.h b/src/sat/aig/aig.h index c83af527..5d2547ea 100644 --- a/src/sat/aig/aig.h +++ b/src/sat/aig/aig.h @@ -21,6 +21,10 @@ #ifndef __AIG_H__ #define __AIG_H__ +#ifdef __cplusplus +extern "C" { +#endif + /* AIG is an And-Inv Graph with structural hashing. It is always structurally hashed. It means that at any time: @@ -358,10 +362,14 @@ extern void Aig_PatternFill( Aig_Pattern_t * pPat ); extern int Aig_PatternCount( Aig_Pattern_t * pPat ); extern void Aig_PatternRandom( Aig_Pattern_t * pPat ); extern void Aig_PatternFree( Aig_Pattern_t * pPat ); + +#ifdef __cplusplus +} +#endif + +#endif //////////////////////////////////////////////////////////////////////// /// END OF FILE /// //////////////////////////////////////////////////////////////////////// -#endif - diff --git a/src/sat/asat/asatmem.h b/src/sat/asat/asatmem.h index 56115e7d..7351d77b 100644 --- a/src/sat/asat/asatmem.h +++ b/src/sat/asat/asatmem.h @@ -70,7 +70,9 @@ extern char * Asat_MmStepEntryFetch( Asat_MmStep_t * p, int nBytes extern void Asat_MmStepEntryRecycle( Asat_MmStep_t * p, char * pEntry, int nBytes ); extern int Asat_MmStepReadMemUsage( Asat_MmStep_t * p ); +#endif + //////////////////////////////////////////////////////////////////////// /// END OF FILE /// //////////////////////////////////////////////////////////////////////// -#endif + diff --git a/src/sat/asat/solver.h b/src/sat/asat/solver.h index d798a7a9..62815656 100644 --- a/src/sat/asat/solver.h +++ b/src/sat/asat/solver.h @@ -22,6 +22,10 @@ OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWA #ifndef solver_h #define solver_h +#ifdef __cplusplus +extern "C" { +#endif + #ifdef _WIN32 #define inline __inline // compatible with MS VS 6.0 #endif @@ -141,5 +145,9 @@ struct solver_t stats solver_stats; }; + +#ifdef __cplusplus +} +#endif #endif diff --git a/src/sat/csat/csat_apis.h b/src/sat/csat/csat_apis.h index e187845c..d2fa770e 100644 --- a/src/sat/csat/csat_apis.h +++ b/src/sat/csat/csat_apis.h @@ -206,12 +206,12 @@ extern void ABC_TargetResFree( CSAT_Target_ResultT * p ); extern void CSAT_SetCaller(ABC_Manager mng, enum CSAT_CallerT caller); -//////////////////////////////////////////////////////////////////////// -/// END OF FILE /// -//////////////////////////////////////////////////////////////////////// - #ifdef __cplusplus } #endif #endif + +//////////////////////////////////////////////////////////////////////// +/// END OF FILE /// +//////////////////////////////////////////////////////////////////////// diff --git a/src/sat/fraig/fraig.h b/src/sat/fraig/fraig.h index 4637c030..4e2a295e 100644 --- a/src/sat/fraig/fraig.h +++ b/src/sat/fraig/fraig.h @@ -18,7 +18,11 @@ #ifndef __FRAIG_H__ #define __FRAIG_H__ - + +#ifdef __cplusplus +extern "C" { +#endif + //////////////////////////////////////////////////////////////////////// /// INCLUDES /// //////////////////////////////////////////////////////////////////////// @@ -106,6 +110,7 @@ extern int * Fraig_ManReadModel( Fraig_Man_t * p ); extern int Fraig_ManReadPatternNumRandom( Fraig_Man_t * p ); extern int Fraig_ManReadPatternNumDynamic( Fraig_Man_t * p ); extern int Fraig_ManReadPatternNumDynamicFiltered( Fraig_Man_t * p ); +extern int Fraig_ManReadSatFails( Fraig_Man_t * p ); extern void Fraig_ManSetFuncRed( Fraig_Man_t * p, int fFuncRed ); extern void Fraig_ManSetFeedBack( Fraig_Man_t * p, int fFeedBack ); @@ -208,4 +213,9 @@ extern Fraig_NodeVec_t * Fraig_CollectSupergate( Fraig_Node_t * pNode, int fSt //////////////////////////////////////////////////////////////////////// /// END OF FILE /// //////////////////////////////////////////////////////////////////////// + +#ifdef __cplusplus +} +#endif + #endif diff --git a/src/sat/fraig/fraigApi.c b/src/sat/fraig/fraigApi.c index aeea01f1..3b8da17f 100644 --- a/src/sat/fraig/fraigApi.c +++ b/src/sat/fraig/fraigApi.c @@ -64,6 +64,8 @@ int Fraig_ManReadPatternNumRandom( Fraig_Man_t * p ) { int Fraig_ManReadPatternNumDynamic( Fraig_Man_t * p ) { return p->iWordStart * 32; } // returns the number of dynamic patterns proved useful to distinquish some FRAIG nodes (this number is more than 0 after the first garbage collection of patterns) int Fraig_ManReadPatternNumDynamicFiltered( Fraig_Man_t * p ) { return p->iPatsPerm; } +// returns the number of times FRAIG package timed out +int Fraig_ManReadSatFails( Fraig_Man_t * p ) { return p->nSatFails; } /**Function************************************************************* diff --git a/src/sat/fraig/fraigInt.h b/src/sat/fraig/fraigInt.h index f5e792eb..890af13c 100644 --- a/src/sat/fraig/fraigInt.h +++ b/src/sat/fraig/fraigInt.h @@ -441,8 +441,8 @@ extern int Fraig_NodeIsTravIdPrevious( Fraig_Man_t * pMan, Fraig /*=== fraigVec.c ===============================================================*/ extern void Fraig_NodeVecSortByRefCount( Fraig_NodeVec_t * p ); +#endif + //////////////////////////////////////////////////////////////////////// /// END OF FILE /// //////////////////////////////////////////////////////////////////////// - -#endif diff --git a/src/sat/msat/msat.h b/src/sat/msat/msat.h index 40028784..94416a5d 100644 --- a/src/sat/msat/msat.h +++ b/src/sat/msat/msat.h @@ -21,6 +21,10 @@ #ifndef __MSAT_H__ #define __MSAT_H__ +#ifdef __cplusplus +extern "C" { +#endif + //////////////////////////////////////////////////////////////////////// /// INCLUDES /// //////////////////////////////////////////////////////////////////////// @@ -154,8 +158,13 @@ extern double Msat_VarHeapReadMaxWeight( Msat_VarHeap_t * p ); extern int Msat_VarHeapCountNodes( Msat_VarHeap_t * p, double WeightLimit ); extern int Msat_VarHeapReadMax( Msat_VarHeap_t * p ); extern int Msat_VarHeapGetMax( Msat_VarHeap_t * p ); + +#ifdef __cplusplus +} +#endif + +#endif //////////////////////////////////////////////////////////////////////// /// END OF FILE /// //////////////////////////////////////////////////////////////////////// -#endif diff --git a/src/sat/msat/msatSolverCore.c b/src/sat/msat/msatSolverCore.c index 091a0c55..397dbcdc 100644 --- a/src/sat/msat/msatSolverCore.c +++ b/src/sat/msat/msatSolverCore.c @@ -176,7 +176,7 @@ bool Msat_SolverSolve( Msat_Solver_t * p, Msat_IntVec_t * vAssumps, int nBackTra nConflictsLimit *= 1.5; nLearnedLimit *= 1.1; // if the limit on the number of backtracks is given, quit the restart loop - if ( nBackTrackLimit > 0 ) + if ( nBackTrackLimit > 0 && (int)p->Stats.nConflicts - p->nBackTracks > nBackTrackLimit ) break; // if the runtime limit is exceeded, quit the restart loop if ( nTimeLimit > 0 && clock() - timeStart >= nTimeLimit * CLOCKS_PER_SEC ) diff --git a/src/sat/msat/msatSolverSearch.c b/src/sat/msat/msatSolverSearch.c index e594d9c3..4b73d6b3 100644 --- a/src/sat/msat/msatSolverSearch.c +++ b/src/sat/msat/msatSolverSearch.c @@ -599,7 +599,7 @@ Msat_Type_t Msat_SolverSearch( Msat_Solver_t * p, int nConfLimit, int nLearnedLi Msat_SolverCancelUntil( p, p->nLevelRoot ); return MSAT_UNKNOWN; } - else if ( nBackTrackLimit > 0 && nConfs > nBackTrackLimit ) { + else if ( nBackTrackLimit > 0 && (int)p->Stats.nConflicts - p->nBackTracks > nBackTrackLimit ) { // Reached bound on number of conflicts: Msat_QueueClear( p->pQueue ); Msat_SolverCancelUntil( p, p->nLevelRoot ); -- cgit v1.2.3