diff options
-rw-r--r-- | abc.dsp | 4 | ||||
-rw-r--r-- | abc.rc | 5 | ||||
-rw-r--r-- | src/aig/aig/aig.h | 1 | ||||
-rw-r--r-- | src/aig/aig/aigMan.c | 1 | ||||
-rw-r--r-- | src/aig/fra/fra.h | 36 | ||||
-rw-r--r-- | src/aig/fra/fraBmc.c | 298 | ||||
-rw-r--r-- | src/aig/fra/fraClass.c | 106 | ||||
-rw-r--r-- | src/aig/fra/fraCnf.c | 2 | ||||
-rw-r--r-- | src/aig/fra/fraCore.c | 32 | ||||
-rw-r--r-- | src/aig/fra/fraImp.c | 32 | ||||
-rw-r--r-- | src/aig/fra/fraInd.c | 73 | ||||
-rw-r--r-- | src/aig/fra/fraMan.c | 10 | ||||
-rw-r--r-- | src/aig/fra/fraSat.c | 14 | ||||
-rw-r--r-- | src/aig/fra/fraSec.c | 4 | ||||
-rw-r--r-- | src/aig/fra/fraSim.c | 142 | ||||
-rw-r--r-- | src/aig/fra/module.make | 3 | ||||
-rw-r--r-- | src/base/abc/abcAig.c | 8 | ||||
-rw-r--r-- | src/base/abci/abc.c | 26 | ||||
-rw-r--r-- | src/base/abci/abcDar.c | 4 | ||||
-rw-r--r-- | src/base/abci/abcSweep.c | 8 | ||||
-rw-r--r-- | todo.txt | 3 |
21 files changed, 614 insertions, 198 deletions
@@ -2558,6 +2558,10 @@ SOURCE=.\src\aig\fra\fra.h # End Source File # Begin Source File +SOURCE=.\src\aig\fra\fraBmc.c +# End Source File +# Begin Source File + SOURCE=.\src\aig\fra\fraCec.c # End Source File # Begin Source File @@ -88,8 +88,7 @@ alias wp write_pla alias wv write_verilog # standard scripts -alias share "b; ren -s; fx; b" -alias sharedsd "b; ren -b; dsd -g; sw; fx; b" +alias share "b; multi; fx; b" alias resyn "b; rw; rwz; b; rwz; b" alias resyn2 "b; rw; rf; b; rw; rwz; b; rfz; rwz; b" alias resyn2a "b; rw; b; rw; rwz; b; rwz; b" @@ -171,4 +170,6 @@ alias tst6 "r i10_if6.blif; st; ps; r x/rec6_16_.blif; st; rec_start; r i10_ #alias t "r i10.blif; st; drw -v" alias t "r c.blif; st; drf" +alias bmc "frames -i -F 10; orpos; iprove" + diff --git a/src/aig/aig/aig.h b/src/aig/aig/aig.h index a1abd2b7..953d98ac 100644 --- a/src/aig/aig/aig.h +++ b/src/aig/aig/aig.h @@ -127,6 +127,7 @@ struct Aig_Man_t_ int nTravIds; // the current traversal ID int fCatchExor; // enables EXOR nodes int fAddStrash; // performs additional strashing + Aig_Obj_t ** pObjCopies; // mapping of AIG nodes into FRAIG nodes // timing statistics int time1; int time2; diff --git a/src/aig/aig/aigMan.c b/src/aig/aig/aigMan.c index d09bf41b..122daaa4 100644 --- a/src/aig/aig/aigMan.c +++ b/src/aig/aig/aigMan.c @@ -288,6 +288,7 @@ void Aig_ManStop( Aig_Man_t * p ) if ( p->vBufs ) Vec_PtrFree( p->vBufs ); if ( p->vLevelR ) Vec_IntFree( p->vLevelR ); if ( p->vLevels ) Vec_VecFree( p->vLevels ); + FREE( p->pObjCopies ); FREE( p->pReprs ); FREE( p->pEquivs ); free( p->pTable ); diff --git a/src/aig/fra/fra.h b/src/aig/fra/fra.h index 2bb19a34..c8617d84 100644 --- a/src/aig/fra/fra.h +++ b/src/aig/fra/fra.h @@ -52,6 +52,7 @@ typedef struct Fra_Par_t_ Fra_Par_t; typedef struct Fra_Man_t_ Fra_Man_t; typedef struct Fra_Cla_t_ Fra_Cla_t; typedef struct Fra_Sml_t_ Fra_Sml_t; +typedef struct Fra_Bmc_t_ Fra_Bmc_t; // FRAIG parameters struct Fra_Par_t_ @@ -70,6 +71,7 @@ struct Fra_Par_t_ int fConeBias; // bias variables in the cone (good for unsat runs) int nBTLimitNode; // conflict limit at a node int nBTLimitMiter; // conflict limit at an output + int nFramesP; // the number of timeframes to in the prefix int nFramesK; // the number of timeframes to unroll int fRewrite; // use rewriting for constraint reduction int fLatchCorr; // computes latch correspondence only @@ -91,15 +93,21 @@ struct Fra_Cla_t_ int nPairs; // the number of pairs of nodes int fRefinement; // set to 1 when refinement has happened Vec_Int_t * vImps; // implications + // procedures used for class refinement + int (*pFuncNodeHash) (Aig_Obj_t *, int); // returns has key of the node + int (*pFuncNodeIsConst) (Aig_Obj_t *); // returns 1 if the node is a constant + int (*pFuncNodesAreEqual)(Aig_Obj_t *, Aig_Obj_t *); // returns 1 if nodes are equal up to a complement }; // simulation manager struct Fra_Sml_t_ { Aig_Man_t * pAig; // the original AIG manager - int nFrames; // the number of times frames + int nPref; // the number of times frames in the prefix + int nFrames; // the number of times frames int nWordsFrame; // the number of words in each time frame int nWordsTotal; // the total number of words at a node + int nWordsPref; // the number of word in the prefix int nSimRounds; // statistics int timeSim; // statistics unsigned pData[0]; // simulation data for the nodes @@ -120,6 +128,8 @@ struct Fra_Man_t_ Fra_Cla_t * pCla; // representation of (candidate) equivalent nodes // simulation info Fra_Sml_t * pSml; // simulation manager + // bounded model checking manager + Fra_Bmc_t * pBmc; // counter example storage int nPatWords; // the number of words in the counter example unsigned * pPatWords; // the counter example @@ -199,6 +209,11 @@ static inline Aig_Obj_t * Fra_ObjChild1Fra( Aig_Obj_t * pObj, int i ) { assert( //////////////////////////////////////////////////////////////////////// /*=== fraClass.c ========================================================*/ +extern int Fra_BmcNodeIsConst( Aig_Obj_t * pObj ); +extern int Fra_BmcNodesAreEqual( Aig_Obj_t * pObj0, Aig_Obj_t * pObj1 ); +extern void Fra_BmcStop( Fra_Bmc_t * p ); +extern void Fra_BmcPerform( Fra_Man_t * p, int nPref, int nDepth ); +/*=== fraClass.c ========================================================*/ extern Fra_Cla_t * Fra_ClassesStart( Aig_Man_t * pAig ); extern void Fra_ClassesStop( Fra_Cla_t * p ); extern void Fra_ClassesCopyReprs( Fra_Cla_t * p, Vec_Ptr_t * vFailed ); @@ -212,7 +227,7 @@ extern void Fra_ClassesTest( Fra_Cla_t * p, int Id1, int Id2 ); extern void Fra_ClassesLatchCorr( Fra_Man_t * p ); extern void Fra_ClassesPostprocess( Fra_Cla_t * p ); /*=== fraCnf.c ========================================================*/ -extern void Fra_NodeAddToSolver( Fra_Man_t * p, Aig_Obj_t * pOld, Aig_Obj_t * pNew ); +extern void Fra_CnfNodeAddToSolver( Fra_Man_t * p, Aig_Obj_t * pOld, Aig_Obj_t * pNew ); /*=== fraCore.c ========================================================*/ extern Aig_Man_t * Fra_FraigPerform( Aig_Man_t * pManAig, Fra_Par_t * pPars ); extern Aig_Man_t * Fra_FraigChoice( Aig_Man_t * pManAig ); @@ -225,7 +240,7 @@ extern int Fra_ImpCheckForNode( Fra_Man_t * p, Vec_Int_t * vImps extern int Fra_ImpRefineUsingCex( Fra_Man_t * p, Vec_Int_t * vImps ); extern void Fra_ImpCompactArray( Vec_Int_t * vImps ); /*=== fraInd.c ========================================================*/ -extern Aig_Man_t * Fra_FraigInduction( Aig_Man_t * p, int nFramesK, int fRewrite, int fUseImps, int fLatchCorr, int fVerbose, int * pnIter ); +extern Aig_Man_t * Fra_FraigInduction( Aig_Man_t * p, int nFramesP, int nFramesK, int fRewrite, int fUseImps, int fLatchCorr, int fVerbose, int * pnIter ); /*=== fraMan.c ========================================================*/ extern void Fra_ParamsDefault( Fra_Par_t * pParams ); extern void Fra_ParamsDefaultSeq( Fra_Par_t * pParams ); @@ -242,16 +257,17 @@ extern int Fra_NodeIsConst( Fra_Man_t * p, Aig_Obj_t * pNew ); /*=== fraSec.c ========================================================*/ extern int Fra_FraigSec( Aig_Man_t * p, int nFrames, int fVerbose, int fVeryVerbose ); /*=== fraSim.c ========================================================*/ -extern int Fra_NodeHasZeroSim( Aig_Obj_t * pObj ); -extern int Fra_NodeCompareSims( Aig_Obj_t * pObj0, Aig_Obj_t * pObj1 ); -extern unsigned Fra_NodeHashSims( Aig_Obj_t * pObj ); -extern int Fra_CheckOutputSims( Fra_Man_t * p ); -extern void Fra_SavePattern( Fra_Man_t * p ); +extern int Fra_SmlNodeHash( Aig_Obj_t * pObj, int nTableSize ); +extern int Fra_SmlNodeIsConst( Aig_Obj_t * pObj ); +extern int Fra_SmlNodesAreEqual( Aig_Obj_t * pObj0, Aig_Obj_t * pObj1 ); +extern int Fra_SmlNodeNotEquWeight( Fra_Sml_t * p, int Left, int Right ); +extern int Fra_SmlCheckOutput( Fra_Man_t * p ); +extern void Fra_SmlSavePattern( Fra_Man_t * p ); extern void Fra_SmlSimulate( Fra_Man_t * p, int fInit ); extern void Fra_SmlResimulate( Fra_Man_t * p ); -extern Fra_Sml_t * Fra_SmlStart( Aig_Man_t * pAig, int nFrames, int nWordsFrame ); +extern Fra_Sml_t * Fra_SmlStart( Aig_Man_t * pAig, int nPref, int nFrames, int nWordsFrame ); extern void Fra_SmlStop( Fra_Sml_t * p ); -extern Fra_Sml_t * Fra_SmlSimulateSeq( Aig_Man_t * pAig, int nFrames, int nWords ); +extern Fra_Sml_t * Fra_SmlSimulateSeq( Aig_Man_t * pAig, int nPref, int nFrames, int nWords ); extern Fra_Sml_t * Fra_SmlSimulateComb( Aig_Man_t * pAig, int nWords ); diff --git a/src/aig/fra/fraBmc.c b/src/aig/fra/fraBmc.c new file mode 100644 index 00000000..45c162af --- /dev/null +++ b/src/aig/fra/fraBmc.c @@ -0,0 +1,298 @@ +/**CFile**************************************************************** + + FileName [fraBmc.c] + + SystemName [ABC: Logic synthesis and verification system.] + + PackageName [New FRAIG package.] + + Synopsis [Bounded model checking.] + + Author [Alan Mishchenko] + + Affiliation [UC Berkeley] + + Date [Ver. 1.0. Started - June 30, 2007.] + + Revision [$Id: fraBmc.c,v 1.00 2007/06/30 00:00:00 alanmi Exp $] + +***********************************************************************/ + +#include "fra.h" + +//////////////////////////////////////////////////////////////////////// +/// DECLARATIONS /// +//////////////////////////////////////////////////////////////////////// + +// simulation manager +struct Fra_Bmc_t_ +{ + // parameters + int nPref; // the size of the prefix + int nDepth; // the depth of the frames + int nFramesAll; // the total number of timeframes + // AIG managers + Aig_Man_t * pAig; // the original AIG manager + Aig_Man_t * pAigFrames; // initialized timeframes + Aig_Man_t * pAigFraig; // the fraiged initialized timeframes + // mapping of nodes + Aig_Obj_t ** pObjToFrames; // mapping of the original node into frames + Aig_Obj_t ** pObjToFraig; // mapping of the frames node into fraig +}; + +static inline Aig_Obj_t * Bmc_ObjFrames( Aig_Obj_t * pObj, int i ) { return ((Fra_Man_t *)pObj->pData)->pBmc->pObjToFrames[((Fra_Man_t *)pObj->pData)->pBmc->nFramesAll*pObj->Id + i]; } +static inline void Bmc_ObjSetFrames( Aig_Obj_t * pObj, int i, Aig_Obj_t * pNode ) { ((Fra_Man_t *)pObj->pData)->pBmc->pObjToFrames[((Fra_Man_t *)pObj->pData)->pBmc->nFramesAll*pObj->Id + i] = pNode; } + +static inline Aig_Obj_t * Bmc_ObjFraig( Aig_Obj_t * pObj ) { return ((Fra_Man_t *)pObj->pData)->pBmc->pObjToFraig[pObj->Id]; } +static inline void Bmc_ObjSetFraig( Aig_Obj_t * pObj, Aig_Obj_t * pNode ) { ((Fra_Man_t *)pObj->pData)->pBmc->pObjToFraig[pObj->Id] = pNode; } + +static inline Aig_Obj_t * Bmc_ObjChild0Frames( Aig_Obj_t * pObj, int i ) { assert( !Aig_IsComplement(pObj) ); return Aig_ObjFanin0(pObj)? Aig_NotCond(Bmc_ObjFrames(Aig_ObjFanin0(pObj),i), Aig_ObjFaninC0(pObj)) : NULL; } +static inline Aig_Obj_t * Bmc_ObjChild1Frames( Aig_Obj_t * pObj, int i ) { assert( !Aig_IsComplement(pObj) ); return Aig_ObjFanin1(pObj)? Aig_NotCond(Bmc_ObjFrames(Aig_ObjFanin1(pObj),i), Aig_ObjFaninC1(pObj)) : NULL; } + +//////////////////////////////////////////////////////////////////////// +/// FUNCTION DEFINITIONS /// +//////////////////////////////////////////////////////////////////////// + +/**Function************************************************************* + + Synopsis [Returns 1 if the nodes are equivalent.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Fra_BmcNodesAreEqual( Aig_Obj_t * pObj0, Aig_Obj_t * pObj1 ) +{ + Fra_Man_t * p = pObj0->pData; +// Aig_Obj_t ** ppNodes = p->pBmc->pObjToFraig; + Aig_Obj_t * pObjFrames0, * pObjFrames1; + Aig_Obj_t * pObjFraig0, * pObjFraig1; + int i; + for ( i = p->pBmc->nPref; i < p->pBmc->nFramesAll; i++ ) + { + pObjFrames0 = Aig_Regular( Bmc_ObjFrames(pObj0, i) ); + pObjFrames1 = Aig_Regular( Bmc_ObjFrames(pObj1, i) ); + if ( pObjFrames0 == pObjFrames1 ) + continue; + pObjFraig0 = Aig_Regular( Bmc_ObjFraig(pObjFrames0) ); + pObjFraig1 = Aig_Regular( Bmc_ObjFraig(pObjFrames1) ); + if ( pObjFraig0 != pObjFraig1 ) + return 0; + } + return 1; +} + +/**Function************************************************************* + + Synopsis [Returns 1 if the node is costant.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Fra_BmcNodeIsConst( Aig_Obj_t * pObj ) +{ + Fra_Man_t * p = pObj->pData; + return Fra_BmcNodesAreEqual( pObj, Aig_ManConst1(p->pManAig) ); +} + + +/**Function************************************************************* + + Synopsis [Starts the BMC manager.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Fra_Bmc_t * Fra_BmcStart( Aig_Man_t * pAig, int nPref, int nDepth ) +{ + Fra_Bmc_t * p; + p = ALLOC( Fra_Bmc_t, 1 ); + memset( p, 0, sizeof(Fra_Bmc_t) ); + p->pAig = pAig; + p->nPref = nPref; + p->nDepth = nDepth; + p->nFramesAll = nPref + nDepth; + p->pObjToFrames = ALLOC( Aig_Obj_t *, p->nFramesAll * (Aig_ManObjIdMax(pAig) + 1) ); + memset( p->pObjToFrames, 0, sizeof(Aig_Obj_t *) * p->nFramesAll * (Aig_ManObjIdMax(pAig) + 1) ); +// p->pObjToFraig = ALLOC( Aig_Obj_t *, p->nFramesAll * (Aig_ManObjIdMax(pAig) + 1) ); +// memset( p->pObjToFraig, 0, sizeof(Aig_Obj_t *) * p->nFramesAll * (Aig_ManObjIdMax(pAig) + 1) ); + return p; +} + +/**Function************************************************************* + + Synopsis [Stops the BMC manager.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Fra_BmcStop( Fra_Bmc_t * p ) +{ + Aig_ManStop( p->pAigFrames ); + Aig_ManStop( p->pAigFraig ); + free( p->pObjToFrames ); + free( p->pObjToFraig ); + free( p ); +} + +/**Function************************************************************* + + Synopsis [Constructs initialized timeframes of the AIG.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Aig_Man_t * Fra_BmcFrames( Fra_Bmc_t * p ) +{ + Aig_Man_t * pAigFrames; + Aig_Obj_t * pObj, * pObjNew; + Aig_Obj_t ** pLatches; + int i, k, f; + + // start the fraig package + pAigFrames = Aig_ManStart( (Aig_ManObjIdMax(p->pAig) + 1) * p->nFramesAll ); + // create PI nodes for the frames + for ( f = 0; f < p->nFramesAll; f++ ) + Bmc_ObjSetFrames( Aig_ManConst1(p->pAig), f, Aig_ManConst1(pAigFrames) ); + for ( f = 0; f < p->nFramesAll; f++ ) + Aig_ManForEachPiSeq( p->pAig, pObj, i ) + Bmc_ObjSetFrames( pObj, f, Aig_ObjCreatePi(pAigFrames) ); + // set initial state for the latches + Aig_ManForEachLoSeq( p->pAig, pObj, i ) + Bmc_ObjSetFrames( pObj, 0, Aig_ManConst0(pAigFrames) ); + + // add timeframes + pLatches = ALLOC( Aig_Obj_t *, Aig_ManRegNum(p->pAig) ); + for ( f = 0; f < p->nFramesAll; f++ ) + { + // add internal nodes of this frame + Aig_ManForEachNode( p->pAig, pObj, i ) + { + pObjNew = Aig_And( pAigFrames, Bmc_ObjChild0Frames(pObj,f), Bmc_ObjChild1Frames(pObj,f) ); + Bmc_ObjSetFrames( pObj, f, pObjNew ); + } + if ( f == p->nFramesAll - 1 ) + break; + // save the latch input values + k = 0; + Aig_ManForEachLiSeq( p->pAig, pObj, i ) + pLatches[k++] = Bmc_ObjChild0Frames(pObj,f); + assert( k == Aig_ManRegNum(p->pAig) ); + // insert them to the latch output values + k = 0; + Aig_ManForEachLoSeq( p->pAig, pObj, i ) + Bmc_ObjSetFrames( pObj, f+1, pLatches[k++] ); + assert( k == Aig_ManRegNum(p->pAig) ); + } + free( pLatches ); + // add POs to all the dangling nodes + Aig_ManForEachObj( pAigFrames, pObjNew, i ) + if ( Aig_ObjIsNode(pObjNew) && pObjNew->nRefs == 0 ) + Aig_ObjCreatePo( pAigFrames, pObjNew ); + + // return the new manager + return pAigFrames; +} + +/**Function************************************************************* + + Synopsis [Constructs FRAIG manager for the initialized timeframes.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Aig_Man_t * Fra_BmcFraig( Fra_Bmc_t * p ) +{ + Aig_Man_t * pFraig; + Fra_Par_t Pars, * pPars = &Pars; + Fra_ParamsDefault( pPars ); + pPars->nBTLimitNode = 100000; + pPars->fVerbose = 0; + pPars->fProve = 0; + pPars->fDoSparse = 1; + pPars->fSpeculate = 0; + pPars->fChoicing = 0; + pFraig = Fra_FraigPerform( p->pAigFrames, pPars ); + p->pObjToFraig = p->pAigFrames->pObjCopies; + p->pAigFrames->pObjCopies = NULL; + return pFraig; +} + +/**Function************************************************************* + + Synopsis [Performs BMC for the given AIG.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Fra_BmcPerform( Fra_Man_t * p, int nPref, int nDepth ) +{ + Aig_Obj_t * pObj; + int i, clk = clock(); + assert( p->pBmc == NULL ); + // derive and fraig the frames + p->pBmc = Fra_BmcStart( p->pManAig, nPref, nDepth ); + p->pBmc->pAigFrames = Fra_BmcFrames( p->pBmc ); + p->pBmc->pAigFraig = Fra_BmcFraig( p->pBmc ); + // annotate frames nodes with pointers to the manager + Aig_ManForEachObj( p->pBmc->pAigFrames, pObj, i ) + pObj->pData = p; + // report the results + if ( p->pPars->fVerbose ) + { + printf( "Original AIG = %d. Init %d frames = %d. Fraig = %d. ", + Aig_ManNodeNum(p->pBmc->pAig), p->pBmc->nFramesAll, + Aig_ManNodeNum(p->pBmc->pAigFrames), Aig_ManNodeNum(p->pBmc->pAigFraig) ); + PRT( "Time", clock() - clk ); + printf( "Before BMC: " ); Fra_ClassesPrint( p->pCla, 0 ); + } + // refine the classes + p->pCla->pFuncNodeIsConst = Fra_BmcNodeIsConst; + p->pCla->pFuncNodesAreEqual = Fra_BmcNodesAreEqual; + Fra_ClassesRefine( p->pCla ); + Fra_ClassesRefine1( p->pCla ); + p->pCla->pFuncNodeIsConst = Fra_SmlNodeIsConst; + p->pCla->pFuncNodesAreEqual = Fra_SmlNodesAreEqual; + // report the results + if ( p->pPars->fVerbose ) + { + printf( "After BMC: " ); Fra_ClassesPrint( p->pCla, 0 ); + } + // free the BMC manager + Fra_BmcStop( p->pBmc ); + p->pBmc = NULL; +} + + +//////////////////////////////////////////////////////////////////////// +/// END OF FILE /// +//////////////////////////////////////////////////////////////////////// + + diff --git a/src/aig/fra/fraClass.c b/src/aig/fra/fraClass.c index 9c10ae3b..a9d727da 100644 --- a/src/aig/fra/fraClass.c +++ b/src/aig/fra/fraClass.c @@ -67,6 +67,9 @@ Fra_Cla_t * Fra_ClassesStart( Aig_Man_t * pAig ) p->vClassesTemp = Vec_PtrAlloc( 100 ); p->vClassOld = Vec_PtrAlloc( 100 ); p->vClassNew = Vec_PtrAlloc( 100 ); + p->pFuncNodeHash = Fra_SmlNodeHash; + p->pFuncNodeIsConst = Fra_SmlNodeIsConst; + p->pFuncNodesAreEqual = Fra_SmlNodesAreEqual; return p; } @@ -127,27 +130,6 @@ void Fra_ClassesCopyReprs( Fra_Cla_t * p, Vec_Ptr_t * vFailed ) SeeAlso [] ***********************************************************************/ -void Fra_PrintClass( Aig_Obj_t ** pClass ) -{ - Aig_Obj_t * pTemp; - int i; - printf( "{ " ); - for ( i = 0; pTemp = pClass[i]; i++ ) - printf( "%d ", pTemp->Id ); - printf( "}\n" ); -} - -/**Function************************************************************* - - Synopsis [Prints simulation classes.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ int Fra_ClassCount( Aig_Obj_t ** pClass ) { Aig_Obj_t * pTemp; @@ -216,17 +198,42 @@ int Fra_ClassesCountPairs( Fra_Cla_t * p ) SeeAlso [] ***********************************************************************/ +void Fra_PrintClass( Aig_Obj_t ** pClass ) +{ + Aig_Obj_t * pTemp; + int i; + for ( i = 1; pTemp = pClass[i]; i++ ) + assert( Fra_ClassObjRepr(pTemp) == pClass[0] ); + printf( "{ " ); + for ( i = 0; pTemp = pClass[i]; i++ ) + printf( "%d ", pTemp->Id, Fra_ClassObjRepr(pTemp)? Fra_ClassObjRepr(pTemp)->Id : -1 ); + printf( "}\n" ); +} + +/**Function************************************************************* + + Synopsis [Prints simulation classes.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ void Fra_ClassesPrint( Fra_Cla_t * p, int fVeryVerbose ) { Aig_Obj_t ** pClass; Aig_Obj_t * pObj; int i; - printf( "Consts = %6d. Classes = %6d. Literals = %6d.\n", + printf( "Const = %5d. Class = %5d. Lit = %5d.\n", Vec_PtrSize(p->vClasses1), Vec_PtrSize(p->vClasses), Fra_ClassesCountLits(p) ); if ( fVeryVerbose ) { + Vec_PtrForEachEntry( p->vClasses1, pObj, i ) + assert( Fra_ClassObjRepr(pObj) == Aig_ManConst1(p->pAig) ); printf( "Constants { " ); Vec_PtrForEachEntry( p->vClasses1, pObj, i ) printf( "%d ", pObj->Id ); @@ -281,9 +288,9 @@ void Fra_ClassesPrepare( Fra_Cla_t * p, int fLatchCorr ) //Extra_PrintBinary( stdout, Fra_ObjSim(pObj), 32 ); //printf( "\n" ); // hash the node by its simulation info - iEntry = Fra_NodeHashSims( pObj ) % nTableSize; + iEntry = p->pFuncNodeHash( pObj, nTableSize ); // check if the node belongs to the class of constant 1 - if ( iEntry == 0 && Fra_NodeHasZeroSim( pObj ) ) + if ( p->pFuncNodeIsConst( pObj ) ) { Vec_PtrPush( p->vClasses1, pObj ); Fra_ClassObjSetRepr( pObj, Aig_ManConst1(p->pAig) ); @@ -351,7 +358,6 @@ void Fra_ClassesPrepare( Fra_Cla_t * p, int fLatchCorr ) Fra_ClassObjSetRepr( pTemp, pObj ); } // add as many empty entries -// memset( p->pMemClasses + 2*nEntries + nNodes, 0, sizeof(Aig_Obj_t *) * nNodes ); p->pMemClasses[2*nEntries + nNodes] = NULL; // increment the number of entries nEntries += k; @@ -381,7 +387,7 @@ Aig_Obj_t ** Fra_RefineClassOne( Fra_Cla_t * p, Aig_Obj_t ** ppClass ) // check if the class is going to be refined for ( ppThis = ppClass + 1; pObj = *ppThis; ppThis++ ) - if ( !Fra_NodeCompareSims(ppClass[0], pObj) ) + if ( !p->pFuncNodesAreEqual(ppClass[0], pObj) ) break; if ( pObj == NULL ) return NULL; @@ -390,7 +396,7 @@ Aig_Obj_t ** Fra_RefineClassOne( Fra_Cla_t * p, Aig_Obj_t ** ppClass ) Vec_PtrClear( p->vClassNew ); Vec_PtrPush( p->vClassOld, ppClass[0] ); for ( ppThis = ppClass + 1; pObj = *ppThis; ppThis++ ) - if ( Fra_NodeCompareSims(ppClass[0], pObj) ) + if ( p->pFuncNodesAreEqual(ppClass[0], pObj) ) Vec_PtrPush( p->vClassOld, pObj ); else Vec_PtrPush( p->vClassNew, pObj ); @@ -517,7 +523,7 @@ int Fra_ClassesRefine1( Fra_Cla_t * p ) Vec_PtrClear( p->vClassNew ); Vec_PtrForEachEntry( p->vClasses1, pObj, i ) { - if ( Fra_NodeHasZeroSim( pObj ) ) + if ( p->pFuncNodeIsConst( pObj ) ) Vec_PtrWriteEntry( p->vClasses1, k++, pObj ); else Vec_PtrPush( p->vClassNew, pObj ); @@ -526,6 +532,12 @@ int Fra_ClassesRefine1( Fra_Cla_t * p ) if ( Vec_PtrSize(p->vClassNew) == 0 ) return 0; p->fRefinement = 1; +/* + printf( "Refined const-1 class: {" ); + Vec_PtrForEachEntry( p->vClassNew, pObj, i ) + printf( " %d", pObj->Id ); + printf( " }\n" ); +*/ if ( Vec_PtrSize(p->vClassNew) == 1 ) { Fra_ClassObjSetRepr( Vec_PtrEntry(p->vClassNew,0), NULL ); @@ -600,28 +612,6 @@ void Fra_ClassesLatchCorr( Fra_Man_t * p ) /**Function************************************************************* - Synopsis [Counts the number of 1s in the XOR of simulation data.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -static inline int Fra_SmlNodeNotEquWeight( Fra_Sml_t * p, int Left, int Right ) -{ - unsigned * pSimL, * pSimR; - int k, Counter = 0; - pSimL = Fra_ObjSim( p, Left ); - pSimR = Fra_ObjSim( p, Right ); - for ( k = 0; k < p->nWordsTotal; k++ ) - Counter += Aig_WordCountOnes( pSimL[k] ^ pSimR[k] ); - return Counter; -} - -/**Function************************************************************* - Synopsis [Postprocesses the classes by removing half of the less useful.] Description [] @@ -685,6 +675,22 @@ void Fra_ClassesPostprocess( Fra_Cla_t * p ) free( pWeights ); } +/**Function************************************************************* + + Synopsis [Derives AIG for the partitioned problem.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Aig_Man_t * Fra_ClassesDeriveAig( Fra_Cla_t * p, int nFramesK ) +{ + +} + //////////////////////////////////////////////////////////////////////// /// END OF FILE /// //////////////////////////////////////////////////////////////////////// diff --git a/src/aig/fra/fraCnf.c b/src/aig/fra/fraCnf.c index 7df55d93..d56c0254 100644 --- a/src/aig/fra/fraCnf.c +++ b/src/aig/fra/fraCnf.c @@ -234,7 +234,7 @@ void Fra_ObjAddToFrontier( Fra_Man_t * p, Aig_Obj_t * pObj, Vec_Ptr_t * vFrontie SeeAlso [] ***********************************************************************/ -void Fra_NodeAddToSolver( Fra_Man_t * p, Aig_Obj_t * pOld, Aig_Obj_t * pNew ) +void Fra_CnfNodeAddToSolver( Fra_Man_t * p, Aig_Obj_t * pOld, Aig_Obj_t * pNew ) { Vec_Ptr_t * vFrontier, * vFanins; Aig_Obj_t * pNode, * pFanin; diff --git a/src/aig/fra/fraCore.c b/src/aig/fra/fraCore.c index f28793aa..3c76af03 100644 --- a/src/aig/fra/fraCore.c +++ b/src/aig/fra/fraCore.c @@ -181,8 +181,38 @@ static inline void Fra_FraigNode( Fra_Man_t * p, Aig_Obj_t * pObj ) Vec_PtrPush( p->vTimeouts, pObj ); // simulate the counter-example and return the Fraig node Fra_SmlResimulate( p ); +/* +printf( "%d -> %d.\n", pObj->Id, pObjRepr->Id ); +Fra_ClassesPrint( p->pCla, 1 ); +printf( "%3d : ", 19 ); +Extra_PrintBinary( stdout, Fra_ObjSim(p->pSml, 19), 32 * p->pSml->nWordsTotal ); +printf( "\n" ); +printf( "%3d : ", 27 ); +Extra_PrintBinary( stdout, Fra_ObjSim(p->pSml, 27), 32 * p->pSml->nWordsTotal ); +printf( "\n" ); +printf( "%3d : ", 30 ); +Extra_PrintBinary( stdout, Fra_ObjSim(p->pSml, 30), 32 * p->pSml->nWordsTotal ); +printf( "\n" ); +printf( "\n\n" ); +*/ if ( Fra_ClassObjRepr(pObj) == pObjRepr ) + { +/* +//Fra_ClassesPrint( p->pCla, 1 ); +//printf( "\n\n" ); +printf( "%3d : ", pObj->Id ); +Extra_PrintBinary( stdout, Fra_ObjSim(p->pSml, pObj->Id), 32 * p->pSml->nWordsTotal ); +printf( "\n" ); +printf( "%3d : ", pObjRepr->Id ); +Extra_PrintBinary( stdout, Fra_ObjSim(p->pSml, pObjRepr->Id), 32 * p->pSml->nWordsTotal ); +printf( "\n" ); +*/ + if ( Aig_ObjIsPi(pObj) ) + printf( "primary input\n" ); + else + printf( "NOT primary input\n" ); printf( "Fra_FraigNode(): Error in class refinement!\n" ); + } assert( Fra_ClassObjRepr(pObj) != pObjRepr ); } @@ -261,7 +291,7 @@ clk = clock(); assert( Aig_ManLatchNum(pManAig) == 0 ); p = Fra_ManStart( pManAig, pPars ); p->pManFraig = Fra_ManPrepareComb( p ); - p->pSml = Fra_SmlStart( pManAig, 1, pPars->nSimWords ); + p->pSml = Fra_SmlStart( pManAig, 0, 1, pPars->nSimWords ); Fra_SmlSimulate( p, 0 ); if ( p->pPars->fChoicing ) Aig_ManReprStart( p->pManFraig, Aig_ManObjIdMax(p->pManAig)+1 ); diff --git a/src/aig/fra/fraImp.c b/src/aig/fra/fraImp.c index d5761fbe..25b34e03 100644 --- a/src/aig/fra/fraImp.c +++ b/src/aig/fra/fraImp.c @@ -53,7 +53,7 @@ static inline int * Fra_SmlCountOnes( Fra_Sml_t * p ) Aig_ManForEachObj( p->pAig, pObj, i ) { pSim = Fra_ObjSim( p, i ); - for ( k = 0; k < p->nWordsTotal; k++ ) + for ( k = p->nWordsPref; k < p->nWordsTotal; k++ ) pnBits[i] += Aig_WordCountOnes( pSim[k] ); } return pnBits; @@ -61,7 +61,7 @@ static inline int * Fra_SmlCountOnes( Fra_Sml_t * p ) /**Function************************************************************* - Synopsis [Counts the number of 1s in the reverse implication.] + Synopsis [Returns 1 if implications holds.] Description [] @@ -70,20 +70,21 @@ static inline int * Fra_SmlCountOnes( Fra_Sml_t * p ) SeeAlso [] ***********************************************************************/ -static inline int Sml_NodeNotImpWeight( Fra_Sml_t * p, int Left, int Right ) +static inline int Sml_NodeCheckImp( Fra_Sml_t * p, int Left, int Right ) { unsigned * pSimL, * pSimR; - int k, Counter = 0; + int k; pSimL = Fra_ObjSim( p, Left ); pSimR = Fra_ObjSim( p, Right ); - for ( k = 0; k < p->nWordsTotal; k++ ) - Counter += Aig_WordCountOnes( pSimL[k] & ~pSimR[k] ); - return Counter; + for ( k = p->nWordsPref; k < p->nWordsTotal; k++ ) + if ( pSimL[k] & ~pSimR[k] ) + return 0; + return 1; } /**Function************************************************************* - Synopsis [Returns 1 if implications holds.] + Synopsis [Counts the number of 1s in the reverse implication.] Description [] @@ -92,16 +93,15 @@ static inline int Sml_NodeNotImpWeight( Fra_Sml_t * p, int Left, int Right ) SeeAlso [] ***********************************************************************/ -static inline int Sml_NodeCheckImp( Fra_Sml_t * p, int Left, int Right ) +static inline int Sml_NodeNotImpWeight( Fra_Sml_t * p, int Left, int Right ) { unsigned * pSimL, * pSimR; - int k; + int k, Counter = 0; pSimL = Fra_ObjSim( p, Left ); pSimR = Fra_ObjSim( p, Right ); - for ( k = 0; k < p->nWordsTotal; k++ ) - if ( pSimL[k] & ~pSimR[k] ) - return 0; - return 1; + for ( k = p->nWordsPref; k < p->nWordsTotal; k++ ) + Counter += Aig_WordCountOnes( pSimL[k] & ~pSimR[k] ); + return Counter; } /**Function************************************************************* @@ -294,7 +294,7 @@ Vec_Int_t * Fra_ImpDerive( Fra_Man_t * p, int nImpMaxLimit, int nImpUseLimit, in assert( nImpMaxLimit > 0 && nImpUseLimit > 0 && nImpUseLimit <= nImpMaxLimit ); // normalize both managers pComb = Fra_SmlSimulateComb( p->pManAig, nSimWords ); - pSeq = Fra_SmlSimulateSeq( p->pManAig, nSimWords, 1 ); + pSeq = Fra_SmlSimulateSeq( p->pManAig, p->pPars->nFramesP, nSimWords, 1 ); // get the nodes sorted by the number of 1s vNodes = Fra_SmlSortUsingOnes( pSeq, fLatchCorr ); /* @@ -334,7 +334,7 @@ Aig_ManForEachObj( p->pManAig, pObj, i ) continue; } // printf( "d=%d c=%d ", k-i, Sml_NodeNotImpWeight(pComb, *pNodesI, *pNodesK) ); - + nImpsCollected++; Imp = Sml_ImpCreate( *pNodesI, *pNodesK ); pImpCosts[ Vec_IntSize(vImps) ] = Sml_NodeNotImpWeight(pComb, *pNodesI, *pNodesK); diff --git a/src/aig/fra/fraInd.c b/src/aig/fra/fraInd.c index 76cadd0f..d754f3ae 100644 --- a/src/aig/fra/fraInd.c +++ b/src/aig/fra/fraInd.c @@ -198,8 +198,16 @@ Aig_Man_t * Fra_FramesWithClasses( Fra_Man_t * p ) SeeAlso [] ***********************************************************************/ -Aig_Man_t * Fra_FraigInduction( Aig_Man_t * pManAig, int nFramesK, int fRewrite, int fUseImps, int fLatchCorr, int fVerbose, int * pnIter ) +Aig_Man_t * Fra_FraigInduction( Aig_Man_t * pManAig, int nFramesP, int nFramesK, int fRewrite, int fUseImps, int fLatchCorr, int fVerbose, int * pnIter ) { + int fUseSimpleCnf = 0; + int fUseOldSimulation = 0; + // other paramaters affecting performance + // - presence of FRAIGing in Abc_NtkDarSeqSweep() + // - using distance-1 patterns in Fra_SmlAssignDist1() + // - the number of simulation patterns + // - the number of BMC frames + Fra_Man_t * p; Fra_Par_t Pars, * pPars = &Pars; Aig_Obj_t * pObj; @@ -207,7 +215,6 @@ Aig_Man_t * Fra_FraigInduction( Aig_Man_t * pManAig, int nFramesK, int fRewrite, Aig_Man_t * pManAigNew; // Vec_Int_t * vImps; int nIter, i, clk = clock(), clk2; - if ( Aig_ManNodeNum(pManAig) == 0 ) { if ( pnIter ) *pnIter = 0; @@ -220,6 +227,7 @@ Aig_Man_t * Fra_FraigInduction( Aig_Man_t * pManAig, int nFramesK, int fRewrite, // get parameters Fra_ParamsDefaultSeq( pPars ); + pPars->nFramesP = nFramesP; pPars->nFramesK = nFramesK; pPars->fVerbose = fVerbose; pPars->fRewrite = fRewrite; @@ -229,17 +237,31 @@ Aig_Man_t * Fra_FraigInduction( Aig_Man_t * pManAig, int nFramesK, int fRewrite, // start the fraig manager for this run p = Fra_ManStart( pManAig, pPars ); // derive and refine e-classes using K initialized frames -// p->pSml = Fra_SmlStart( pManAig, pPars->nFramesK + 1, pPars->nSimWords ); -// Fra_SmlSimulate( p, 1 ); - - // remember that strange bug: r iscas/blif/s5378.blif ; st; ssw -F 4; sec -F 10 - // refine the classes with more simulation rounds - p->pSml = Fra_SmlSimulateSeq( pManAig, 32, 2 ); - Fra_ClassesPrepare( p->pCla, p->pPars->fLatchCorr ); -// Fra_ClassesPostprocess( p->pCla ); - // allocate new simulation manager for simulating counter-examples - Fra_SmlStop( p->pSml ); - p->pSml = Fra_SmlStart( pManAig, pPars->nFramesK + 1, pPars->nSimWords ); + if ( fUseOldSimulation ) + { + if ( pPars->nFramesP > 0 ) + { + pPars->nFramesP = 0; + printf( "Fra_FraigInduction(): Prefix cannot be used.\n" ); + } + p->pSml = Fra_SmlStart( pManAig, 0, pPars->nFramesK + 1, pPars->nSimWords ); + Fra_SmlSimulate( p, 1 ); + } + else + { + // bug: r iscas/blif/s1238.blif ; st; ssw -v + // refine the classes with more simulation rounds + p->pSml = Fra_SmlSimulateSeq( pManAig, pPars->nFramesP, 32, 2 ); //pPars->nFramesK + 1, 6 ); // 32, 2 ); + Fra_ClassesPrepare( p->pCla, p->pPars->fLatchCorr ); +// Fra_ClassesPostprocess( p->pCla ); + // allocate new simulation manager for simulating counter-examples + Fra_SmlStop( p->pSml ); + p->pSml = Fra_SmlStart( pManAig, 0, pPars->nFramesK + 1, pPars->nSimWords ); + } + + // perform BMC + Fra_BmcPerform( p, pPars->nFramesP, pPars->nFramesK + 1 ); +//Fra_ClassesPrint( p->pCla, 1 ); // select the most expressive implications if ( pPars->fUseImps ) @@ -264,9 +286,8 @@ Aig_Man_t * Fra_FraigInduction( Aig_Man_t * pManAig, int nFramesK, int fRewrite, if ( p->pPars->fRewrite ) Fra_FraigInductionRewrite( p ); - // bug: r iscas/blif/s1238.blif ; st; ssw -v // convert the manager to SAT solver (the last nLatches outputs are inputs) - if ( pPars->fUseImps ) + if ( fUseSimpleCnf || pPars->fUseImps ) pCnf = Cnf_DeriveSimple( p->pManFraig, Aig_ManRegNum(p->pManFraig) ); else pCnf = Cnf_Derive( p->pManFraig, Aig_ManRegNum(p->pManFraig) ); @@ -289,32 +310,24 @@ Aig_Man_t * Fra_FraigInduction( Aig_Man_t * pManAig, int nFramesK, int fRewrite, pObj->pData = p; // transfer PI/LO variable numbers - pObj = Aig_ManConst1( p->pManFraig ); - Fra_ObjSetSatNum( pObj, pCnf->pVarNums[pObj->Id] ); - Aig_ManForEachPi( p->pManFraig, pObj, i ) - Fra_ObjSetSatNum( pObj, pCnf->pVarNums[pObj->Id] ); - // transfer LI variable numbers - Aig_ManForEachLiSeq( p->pManFraig, pObj, i ) - { - Fra_ObjSetSatNum( pObj, pCnf->pVarNums[pObj->Id] ); - Fra_ObjSetFaninVec( pObj, (void *)1 ); - } - Cnf_DataFree( pCnf ); -/* Aig_ManForEachObj( p->pManFraig, pObj, i ) { + if ( pCnf->pVarNums[pObj->Id] == -1 ) + continue; Fra_ObjSetSatNum( pObj, pCnf->pVarNums[pObj->Id] ); Fra_ObjSetFaninVec( pObj, (void *)1 ); } Cnf_DataFree( pCnf ); -*/ + // report the intermediate results if ( fVerbose ) { - printf( "%3d : Const = %6d. Class = %6d. L = %6d. LR = %6d. I = %6d. NR = %6d.\n", + printf( "%3d : Const = %6d. Class = %6d. L = %6d. LR = %6d. %s = %6d. NR = %6d.\n", nIter, Vec_PtrSize(p->pCla->vClasses1), Vec_PtrSize(p->pCla->vClasses), Fra_ClassesCountLits(p->pCla), p->pManFraig->nAsserts, - p->pCla->vImps? Vec_IntSize(p->pCla->vImps) : 0, Aig_ManNodeNum(p->pManFraig) ); + p->pCla->vImps? "I" : "N", + p->pCla->vImps? Vec_IntSize(p->pCla->vImps) : Aig_ManNodeNum(p->pManAig), + Aig_ManNodeNum(p->pManFraig) ); } // perform sweeping diff --git a/src/aig/fra/fraMan.c b/src/aig/fra/fraMan.c index 84621d60..2b8e0a68 100644 --- a/src/aig/fra/fraMan.c +++ b/src/aig/fra/fraMan.c @@ -111,7 +111,7 @@ Fra_Man_t * Fra_ManStart( Aig_Man_t * pManAig, Fra_Par_t * pPars ) p->nSizeAlloc = Aig_ManObjIdMax( pManAig ) + 1; p->nFramesAll = pPars->nFramesK + 1; // allocate storage for sim pattern - p->nPatWords = Aig_BitWordNum( Aig_ManPiNum(pManAig) * p->nFramesAll ); + p->nPatWords = Aig_BitWordNum( (Aig_ManPiNum(pManAig) - Aig_ManRegNum(pManAig)) * p->nFramesAll + Aig_ManRegNum(pManAig) ); p->pPatWords = ALLOC( unsigned, p->nPatWords ); p->vPiVars = Vec_PtrAlloc( 100 ); // equivalence classes @@ -232,6 +232,14 @@ void Fra_ManStop( Fra_Man_t * p ) int i; if ( p->pPars->fVerbose ) Fra_ManPrint( p ); + // save mapping from original nodes into FRAIG nodes + if ( p->pManAig ) + { + if ( p->pManAig->pObjCopies ) + free( p->pManAig->pObjCopies ); + p->pManAig->pObjCopies = p->pMemFraig; + p->pMemFraig = NULL; + } for ( i = 0; i < p->nSizeAlloc; i++ ) if ( p->pMemFanins[i] && p->pMemFanins[i] != (void *)1 ) Vec_PtrFree( p->pMemFanins[i] ); diff --git a/src/aig/fra/fraSat.c b/src/aig/fra/fraSat.c index 417163d5..bc8ef08a 100644 --- a/src/aig/fra/fraSat.c +++ b/src/aig/fra/fraSat.c @@ -77,7 +77,7 @@ int Fra_NodesAreEquiv( Fra_Man_t * p, Aig_Obj_t * pOld, Aig_Obj_t * pNew ) } // if the nodes do not have SAT variables, allocate them - Fra_NodeAddToSolver( p, pOld, pNew ); + Fra_CnfNodeAddToSolver( p, pOld, pNew ); if ( p->pSat->qtail != p->pSat->qhead ) { @@ -113,7 +113,7 @@ p->timeSatUnsat += clock() - clk; else if ( RetValue1 == l_True ) { p->timeSatSat += clock() - clk; - Fra_SavePattern( p ); + Fra_SmlSavePattern( p ); p->nSatCallsSat++; return 0; } @@ -156,7 +156,7 @@ p->timeSatUnsat += clock() - clk; else if ( RetValue1 == l_True ) { p->timeSatSat += clock() - clk; - Fra_SavePattern( p ); + Fra_SmlSavePattern( p ); p->nSatCallsSat++; return 0; } @@ -234,7 +234,7 @@ int Fra_NodesAreImp( Fra_Man_t * p, Aig_Obj_t * pOld, Aig_Obj_t * pNew, int fCom } // if the nodes do not have SAT variables, allocate them - Fra_NodeAddToSolver( p, pOld, pNew ); + Fra_CnfNodeAddToSolver( p, pOld, pNew ); if ( p->pSat->qtail != p->pSat->qhead ) { @@ -272,7 +272,7 @@ p->timeSatUnsat += clock() - clk; else if ( RetValue1 == l_True ) { p->timeSatSat += clock() - clk; - Fra_SavePattern( p ); + Fra_SmlSavePattern( p ); p->nSatCallsSat++; return 0; } @@ -320,7 +320,7 @@ int Fra_NodeIsConst( Fra_Man_t * p, Aig_Obj_t * pNew ) } // if the nodes do not have SAT variables, allocate them - Fra_NodeAddToSolver( p, NULL, pNew ); + Fra_CnfNodeAddToSolver( p, NULL, pNew ); // prepare variable activity if ( p->pPars->fConeBias ) @@ -346,7 +346,7 @@ p->timeSatUnsat += clock() - clk; { p->timeSatSat += clock() - clk; if ( p->pPatWords ) - Fra_SavePattern( p ); + Fra_SmlSavePattern( p ); p->nSatCallsSat++; return 0; } diff --git a/src/aig/fra/fraSec.c b/src/aig/fra/fraSec.c index 814fe59e..2a0d06b5 100644 --- a/src/aig/fra/fraSec.c +++ b/src/aig/fra/fraSec.c @@ -47,7 +47,7 @@ int Fra_FraigSec( Aig_Man_t * p, int nFramesFix, int fVerbose, int fVeryVerbose { nFrames = nFramesFix; // perform seq sweeping for one frame number - pNew = Fra_FraigInduction( p, nFrames, 0, 0, 0, fVeryVerbose, &nIter ); + pNew = Fra_FraigInduction( p, 0, nFrames, 0, 0, 0, fVeryVerbose, &nIter ); } else { @@ -55,7 +55,7 @@ int Fra_FraigSec( Aig_Man_t * p, int nFramesFix, int fVerbose, int fVeryVerbose for ( nFrames = 1; ; nFrames++ ) { clk = clock(); - pNew = Fra_FraigInduction( p, nFrames, 0, 0, 0, fVeryVerbose, &nIter ); + pNew = Fra_FraigInduction( p, 0, nFrames, 0, 0, 0, fVeryVerbose, &nIter ); RetValue = Fra_FraigMiterStatus( pNew ); if ( fVerbose ) { diff --git a/src/aig/fra/fraSim.c b/src/aig/fra/fraSim.c index a0929f99..b31fcb7f 100644 --- a/src/aig/fra/fraSim.c +++ b/src/aig/fra/fraSim.c @@ -30,6 +30,46 @@ /**Function************************************************************* + Synopsis [Computes hash value of the node using its simulation info.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Fra_SmlNodeHash( Aig_Obj_t * pObj, int nTableSize ) +{ + Fra_Man_t * p = pObj->pData; + static int s_FPrimes[128] = { + 1009, 1049, 1093, 1151, 1201, 1249, 1297, 1361, 1427, 1459, + 1499, 1559, 1607, 1657, 1709, 1759, 1823, 1877, 1933, 1997, + 2039, 2089, 2141, 2213, 2269, 2311, 2371, 2411, 2467, 2543, + 2609, 2663, 2699, 2741, 2797, 2851, 2909, 2969, 3037, 3089, + 3169, 3221, 3299, 3331, 3389, 3461, 3517, 3557, 3613, 3671, + 3719, 3779, 3847, 3907, 3943, 4013, 4073, 4129, 4201, 4243, + 4289, 4363, 4441, 4493, 4549, 4621, 4663, 4729, 4793, 4871, + 4933, 4973, 5021, 5087, 5153, 5227, 5281, 5351, 5417, 5471, + 5519, 5573, 5651, 5693, 5749, 5821, 5861, 5923, 6011, 6073, + 6131, 6199, 6257, 6301, 6353, 6397, 6481, 6563, 6619, 6689, + 6737, 6803, 6863, 6917, 6977, 7027, 7109, 7187, 7237, 7309, + 7393, 7477, 7523, 7561, 7607, 7681, 7727, 7817, 7877, 7933, + 8011, 8039, 8059, 8081, 8093, 8111, 8123, 8147 + }; + unsigned * pSims; + unsigned uHash; + int i; +// assert( p->pSml->nWordsTotal <= 128 ); + uHash = 0; + pSims = Fra_ObjSim(p->pSml, pObj->Id); + for ( i = p->pSml->nWordsPref; i < p->pSml->nWordsTotal; i++ ) + uHash ^= pSims[i] * s_FPrimes[i & 0x7F]; + return uHash % nTableSize; +} + +/**Function************************************************************* + Synopsis [Returns 1 if simulation info is composed of all zeros.] Description [] @@ -39,13 +79,13 @@ SeeAlso [] ***********************************************************************/ -int Fra_NodeHasZeroSim( Aig_Obj_t * pObj ) +int Fra_SmlNodeIsConst( Aig_Obj_t * pObj ) { Fra_Man_t * p = pObj->pData; unsigned * pSims; int i; pSims = Fra_ObjSim(p->pSml, pObj->Id); - for ( i = 0; i < p->pSml->nWordsTotal; i++ ) + for ( i = p->pSml->nWordsPref; i < p->pSml->nWordsTotal; i++ ) if ( pSims[i] ) return 0; return 1; @@ -62,14 +102,14 @@ int Fra_NodeHasZeroSim( Aig_Obj_t * pObj ) SeeAlso [] ***********************************************************************/ -int Fra_NodeCompareSims( Aig_Obj_t * pObj0, Aig_Obj_t * pObj1 ) +int Fra_SmlNodesAreEqual( Aig_Obj_t * pObj0, Aig_Obj_t * pObj1 ) { Fra_Man_t * p = pObj0->pData; unsigned * pSims0, * pSims1; int i; pSims0 = Fra_ObjSim(p->pSml, pObj0->Id); pSims1 = Fra_ObjSim(p->pSml, pObj1->Id); - for ( i = 0; i < p->pSml->nWordsTotal; i++ ) + for ( i = p->pSml->nWordsPref; i < p->pSml->nWordsTotal; i++ ) if ( pSims0[i] != pSims1[i] ) return 0; return 1; @@ -77,7 +117,7 @@ int Fra_NodeCompareSims( Aig_Obj_t * pObj0, Aig_Obj_t * pObj1 ) /**Function************************************************************* - Synopsis [Computes hash value of the node using its simulation info.] + Synopsis [Counts the number of 1s in the XOR of simulation data.] Description [] @@ -86,39 +126,19 @@ int Fra_NodeCompareSims( Aig_Obj_t * pObj0, Aig_Obj_t * pObj1 ) SeeAlso [] ***********************************************************************/ -unsigned Fra_NodeHashSims( Aig_Obj_t * pObj ) +int Fra_SmlNodeNotEquWeight( Fra_Sml_t * p, int Left, int Right ) { - Fra_Man_t * p = pObj->pData; - static int s_FPrimes[128] = { - 1009, 1049, 1093, 1151, 1201, 1249, 1297, 1361, 1427, 1459, - 1499, 1559, 1607, 1657, 1709, 1759, 1823, 1877, 1933, 1997, - 2039, 2089, 2141, 2213, 2269, 2311, 2371, 2411, 2467, 2543, - 2609, 2663, 2699, 2741, 2797, 2851, 2909, 2969, 3037, 3089, - 3169, 3221, 3299, 3331, 3389, 3461, 3517, 3557, 3613, 3671, - 3719, 3779, 3847, 3907, 3943, 4013, 4073, 4129, 4201, 4243, - 4289, 4363, 4441, 4493, 4549, 4621, 4663, 4729, 4793, 4871, - 4933, 4973, 5021, 5087, 5153, 5227, 5281, 5351, 5417, 5471, - 5519, 5573, 5651, 5693, 5749, 5821, 5861, 5923, 6011, 6073, - 6131, 6199, 6257, 6301, 6353, 6397, 6481, 6563, 6619, 6689, - 6737, 6803, 6863, 6917, 6977, 7027, 7109, 7187, 7237, 7309, - 7393, 7477, 7523, 7561, 7607, 7681, 7727, 7817, 7877, 7933, - 8011, 8039, 8059, 8081, 8093, 8111, 8123, 8147 - }; - unsigned * pSims; - unsigned uHash; - int i; - assert( p->pSml->nWordsTotal <= 128 ); - uHash = 0; - pSims = Fra_ObjSim(p->pSml, pObj->Id); - for ( i = 0; i < p->pSml->nWordsTotal; i++ ) - uHash ^= pSims[i] * s_FPrimes[i]; - return uHash; + unsigned * pSimL, * pSimR; + int k, Counter = 0; + pSimL = Fra_ObjSim( p, Left ); + pSimR = Fra_ObjSim( p, Right ); + for ( k = p->nWordsPref; k < p->nWordsTotal; k++ ) + Counter += Aig_WordCountOnes( pSimL[k] ^ pSimR[k] ); + return Counter; } - - /**Function************************************************************* Synopsis [Generated const 0 pattern.] @@ -130,7 +150,7 @@ unsigned Fra_NodeHashSims( Aig_Obj_t * pObj ) SeeAlso [] ***********************************************************************/ -void Fra_SavePattern0( Fra_Man_t * p, int fInit ) +void Fra_SmlSavePattern0( Fra_Man_t * p, int fInit ) { memset( p->pPatWords, 0, sizeof(unsigned) * p->nPatWords ); } @@ -146,13 +166,14 @@ void Fra_SavePattern0( Fra_Man_t * p, int fInit ) SeeAlso [] ***********************************************************************/ -void Fra_SavePattern1( Fra_Man_t * p, int fInit ) +void Fra_SmlSavePattern1( Fra_Man_t * p, int fInit ) { Aig_Obj_t * pObj; int i, k, nTruePis; memset( p->pPatWords, 0xff, sizeof(unsigned) * p->nPatWords ); if ( !fInit ) return; + // clear the state bits to correspond to all-0 initial state nTruePis = Aig_ManPiNum(p->pManAig) - Aig_ManRegNum(p->pManAig); k = 0; Aig_ManForEachLoSeq( p->pManAig, pObj, i ) @@ -170,7 +191,7 @@ void Fra_SavePattern1( Fra_Man_t * p, int fInit ) SeeAlso [] ***********************************************************************/ -void Fra_SavePattern( Fra_Man_t * p ) +void Fra_SmlSavePattern( Fra_Man_t * p ) { Aig_Obj_t * pObj; int i; @@ -199,7 +220,7 @@ void Fra_SavePattern( Fra_Man_t * p ) SeeAlso [] ***********************************************************************/ -void Fra_CheckOutputSimsSavePattern( Fra_Man_t * p, Aig_Obj_t * pObj ) +void Fra_SmlCheckOutputSavePattern( Fra_Man_t * p, Aig_Obj_t * pObj ) { unsigned * pSims; int i, k, BestPat, * pModel; @@ -241,7 +262,7 @@ void Fra_CheckOutputSimsSavePattern( Fra_Man_t * p, Aig_Obj_t * pObj ) SeeAlso [] ***********************************************************************/ -int Fra_CheckOutputSims( Fra_Man_t * p ) +int Fra_SmlCheckOutput( Fra_Man_t * p ) { Aig_Obj_t * pObj; int i; @@ -250,10 +271,10 @@ int Fra_CheckOutputSims( Fra_Man_t * p ) assert( Aig_ObjFanin0(pObj)->fPhase == (unsigned)Aig_ObjFaninC0(pObj) ); Aig_ManForEachPo( p->pManAig, pObj, i ) { - if ( !Fra_NodeHasZeroSim( Aig_ObjFanin0(pObj) ) ) + if ( !Fra_SmlNodeIsConst( Aig_ObjFanin0(pObj) ) ) { // create the counter-example from this pattern - Fra_CheckOutputSimsSavePattern( p, Aig_ObjFanin0(pObj) ); + Fra_SmlCheckOutputSavePattern( p, Aig_ObjFanin0(pObj) ); return 1; } } @@ -365,6 +386,8 @@ void Fra_SmlAssignDist1( Fra_Sml_t * p, unsigned * pPat ) } else { + int fUseDist1 = 0; + // copy the PI info for each frame nTruePis = Aig_ManPiNum(p->pAig) - Aig_ManRegNum(p->pAig); for ( f = 0; f < p->nFrames; f++ ) @@ -375,16 +398,15 @@ void Fra_SmlAssignDist1( Fra_Sml_t * p, unsigned * pPat ) Aig_ManForEachLoSeq( p->pAig, pObj, i ) Fra_SmlAssignConst( p, pObj, Aig_InfoHasBit(pPat, nTruePis * p->nFrames + k++), 0 ); // assert( p->pManFraig == NULL || nTruePis * p->nFrames + k == Aig_ManPiNum(p->pManFraig) ); -/* + // flip one bit of the last frame - if ( p->nFrames == 2 ) + if ( fUseDist1 && p->nFrames == 2 ) { Limit = AIG_MIN( nTruePis, p->nWordsFrame * 32 - 1 ); for ( i = 0; i < Limit; i++ ) Aig_InfoXorBit( Fra_ObjSim( p, Aig_ManPi(p->pAig, i)->Id ), i+1 ); // Aig_InfoXorBit( Fra_ObjSim( p, Aig_ManPi(p->pAig, nTruePis*(p->nFrames-2) + i)->Id ), i+1 ); } -*/ } } @@ -571,7 +593,7 @@ void Fra_SmlResimulate( Fra_Man_t * p ) Fra_SmlSimulateOne( p->pSml ); // if ( p->pPars->fPatScores ) // Fra_CleanPatScores( p ); - if ( p->pPars->fProve && Fra_CheckOutputSims(p) ) + if ( p->pPars->fProve && Fra_SmlCheckOutput(p) ) return; clk = clock(); nChanges = Fra_ClassesRefine( p->pCla ); @@ -581,7 +603,7 @@ clk = clock(); p->timeRef += clock() - clk; if ( nChanges < 1 ) printf( "Error: A counter-example did not refine classes!\n" ); - assert( nChanges >= 1 ); +// assert( nChanges >= 1 ); //printf( "Refined classes = %5d. Changes = %4d.\n", Vec_PtrSize(p->vClasses), nChanges ); } @@ -609,11 +631,13 @@ void Fra_SmlSimulate( Fra_Man_t * p, int fInit ) if ( fVerbose ) printf( "Starting classes = %5d. Lits = %6d.\n", Vec_PtrSize(p->pCla->vClasses), Fra_ClassesCountLits(p->pCla) ); +//return; + // refine classes by walking 0/1 patterns - Fra_SavePattern0( p, fInit ); + Fra_SmlSavePattern0( p, fInit ); Fra_SmlAssignDist1( p->pSml, p->pPatWords ); Fra_SmlSimulateOne( p->pSml ); - if ( p->pPars->fProve && Fra_CheckOutputSims(p) ) + if ( p->pPars->fProve && Fra_SmlCheckOutput(p) ) return; clk = clock(); nChanges = Fra_ClassesRefine( p->pCla ); @@ -621,10 +645,10 @@ clk = clock(); p->timeRef += clock() - clk; if ( fVerbose ) printf( "Refined classes = %5d. Changes = %4d. Lits = %6d.\n", Vec_PtrSize(p->pCla->vClasses), nChanges, Fra_ClassesCountLits(p->pCla) ); - Fra_SavePattern1( p, fInit ); + Fra_SmlSavePattern1( p, fInit ); Fra_SmlAssignDist1( p->pSml, p->pPatWords ); Fra_SmlSimulateOne( p->pSml ); - if ( p->pPars->fProve && Fra_CheckOutputSims(p) ) + if ( p->pPars->fProve && Fra_SmlCheckOutput(p) ) return; clk = clock(); nChanges = Fra_ClassesRefine( p->pCla ); @@ -638,7 +662,7 @@ printf( "Refined classes = %5d. Changes = %4d. Lits = %6d.\n", Vec_PtrSize( Fra_SmlInitialize( p->pSml, fInit ); Fra_SmlSimulateOne( p->pSml ); nClasses = Vec_PtrSize(p->pCla->vClasses); - if ( p->pPars->fProve && Fra_CheckOutputSims(p) ) + if ( p->pPars->fProve && Fra_SmlCheckOutput(p) ) return; clk = clock(); nChanges = Fra_ClassesRefine( p->pCla ); @@ -666,16 +690,18 @@ printf( "Refined classes = %5d. Changes = %4d. Lits = %6d.\n", Vec_PtrSize( SeeAlso [] ***********************************************************************/ -Fra_Sml_t * Fra_SmlStart( Aig_Man_t * pAig, int nFrames, int nWordsFrame ) +Fra_Sml_t * Fra_SmlStart( Aig_Man_t * pAig, int nPref, int nFrames, int nWordsFrame ) { Fra_Sml_t * p; assert( Aig_ManObjIdMax(pAig) + 1 < (1 << 16) ); - p = (Fra_Sml_t *)malloc( sizeof(Fra_Sml_t) + sizeof(unsigned) * (Aig_ManObjIdMax(pAig) + 1) * nFrames * nWordsFrame ); - memset( p, 0, sizeof(Fra_Sml_t) + sizeof(unsigned) * nFrames * nWordsFrame ); + p = (Fra_Sml_t *)malloc( sizeof(Fra_Sml_t) + sizeof(unsigned) * (Aig_ManObjIdMax(pAig) + 1) * (nPref + nFrames) * nWordsFrame ); + memset( p, 0, sizeof(Fra_Sml_t) + sizeof(unsigned) * (nPref + nFrames) * nWordsFrame ); p->pAig = pAig; - p->nFrames = nFrames; + p->nPref = nPref; + p->nFrames = nPref + nFrames; p->nWordsFrame = nWordsFrame; - p->nWordsTotal = nFrames * nWordsFrame; + p->nWordsTotal = (nPref + nFrames) * nWordsFrame; + p->nWordsPref = nPref * nWordsFrame; return p; } @@ -710,7 +736,7 @@ void Fra_SmlStop( Fra_Sml_t * p ) Fra_Sml_t * Fra_SmlSimulateComb( Aig_Man_t * pAig, int nWords ) { Fra_Sml_t * p; - p = Fra_SmlStart( pAig, 1, nWords ); + p = Fra_SmlStart( pAig, 0, 1, nWords ); Fra_SmlInitialize( p, 0 ); Fra_SmlSimulateOne( p ); return p; @@ -727,10 +753,10 @@ Fra_Sml_t * Fra_SmlSimulateComb( Aig_Man_t * pAig, int nWords ) SeeAlso [] ***********************************************************************/ -Fra_Sml_t * Fra_SmlSimulateSeq( Aig_Man_t * pAig, int nFrames, int nWords ) +Fra_Sml_t * Fra_SmlSimulateSeq( Aig_Man_t * pAig, int nPref, int nFrames, int nWords ) { Fra_Sml_t * p; - p = Fra_SmlStart( pAig, nFrames, nWords ); + p = Fra_SmlStart( pAig, nPref, nFrames, nWords ); Fra_SmlInitialize( p, 1 ); Fra_SmlSimulateOne( p ); return p; diff --git a/src/aig/fra/module.make b/src/aig/fra/module.make index f2a8b230..bd8a20be 100644 --- a/src/aig/fra/module.make +++ b/src/aig/fra/module.make @@ -1,4 +1,5 @@ -SRC += src/aig/fra/fraCec.c \ +SRC += src/aig/fra/fraBmc.c \ + src/aig/fra/fraCec.c \ src/aig/fra/fraClass.c \ src/aig/fra/fraCnf.c \ src/aig/fra/fraCore.c \ diff --git a/src/base/abc/abcAig.c b/src/base/abc/abcAig.c index f2017549..16f66dc6 100644 --- a/src/base/abc/abcAig.c +++ b/src/base/abc/abcAig.c @@ -700,7 +700,7 @@ Abc_Obj_t * Abc_AigConst1( Abc_Ntk_t * pNtk ) Abc_Obj_t * Abc_AigAnd( Abc_Aig_t * pMan, Abc_Obj_t * p0, Abc_Obj_t * p1 ) { Abc_Obj_t * pAnd; - if ( pAnd = Abc_AigAndLookup( pMan, p0, p1 ) ) + if ( (pAnd = Abc_AigAndLookup( pMan, p0, p1 )) ) return pAnd; return Abc_AigAndCreate( pMan, p0, p1 ); } @@ -886,7 +886,7 @@ void Abc_AigReplace_int( Abc_Aig_t * pMan, Abc_Obj_t * pOld, Abc_Obj_t * pNew, i pFanin2 = Abc_ObjChild( pFanout, iFanin ^ 1 ); assert( Abc_ObjRegular(pFanin2) != pFanout ); // check if the node with these fanins exists - if ( pFanoutNew = Abc_AigAndLookup( pMan, pFanin1, pFanin2 ) ) + if ( (pFanoutNew = Abc_AigAndLookup( pMan, pFanin1, pFanin2 )) ) { // such node exists (it may be a constant) // schedule replacement of the old fanout by the new fanout Vec_PtrPush( pMan->vStackReplaceOld, pFanout ); @@ -1347,8 +1347,8 @@ void Abc_AigCheckFaninOrder( Abc_Aig_t * pMan ) { if ( Abc_ObjRegular(Abc_ObjChild0(pEnt))->Id > Abc_ObjRegular(Abc_ObjChild1(pEnt))->Id ) { - int i0 = Abc_ObjRegular(Abc_ObjChild0(pEnt))->Id; - int i1 = Abc_ObjRegular(Abc_ObjChild1(pEnt))->Id; +// int i0 = Abc_ObjRegular(Abc_ObjChild0(pEnt))->Id; +// int i1 = Abc_ObjRegular(Abc_ObjChild1(pEnt))->Id; printf( "Node %d has incorrect ordering of fanins.\n", pEnt->Id ); } } diff --git a/src/base/abci/abc.c b/src/base/abci/abc.c index cd78f218..c2eead14 100644 --- a/src/base/abci/abc.c +++ b/src/base/abci/abc.c @@ -291,7 +291,7 @@ void Abc_Init( Abc_Frame_t * pAbc ) Cmd_CommandAdd( pAbc, "New AIG", "iprove", Abc_CommandIProve, 1 ); Cmd_CommandAdd( pAbc, "New AIG", "haig", Abc_CommandHaig, 1 ); Cmd_CommandAdd( pAbc, "New AIG", "mini", Abc_CommandMini, 1 ); - Cmd_CommandAdd( pAbc, "New AIG", "bmc", Abc_CommandBmc, 0 ); + Cmd_CommandAdd( pAbc, "New AIG", "_bmc", Abc_CommandBmc, 0 ); Cmd_CommandAdd( pAbc, "New AIG", "qbf", Abc_CommandQbf, 0 ); Cmd_CommandAdd( pAbc, "Fraiging", "fraig", Abc_CommandFraig, 1 ); @@ -8039,7 +8039,7 @@ int Abc_CommandBmc( Abc_Frame_t * pAbc, int argc, char ** argv ) return 0; usage: - fprintf( pErr, "usage: bmc [-K num] [-ivh]\n" ); + fprintf( pErr, "usage: _bmc [-K num] [-ivh]\n" ); fprintf( pErr, "\t perform bounded model checking\n" ); fprintf( pErr, "\t-K num : number of time frames [default = %d]\n", nFrames ); fprintf( pErr, "\t-i : toggle initialization of the first frame [default = %s]\n", fInit? "yes": "no" ); @@ -10972,19 +10972,21 @@ int Abc_CommandSeqSweep( Abc_Frame_t * pAbc, int argc, char ** argv ) FILE * pOut, * pErr; Abc_Ntk_t * pNtk, * pNtkRes; int c; + int nFramesP; int nFramesK; int fExdc; int fUseImps; int fRewrite; int fLatchCorr; int fVerbose; - extern Abc_Ntk_t * Abc_NtkSeqSweep( Abc_Ntk_t * pNtk, int nFrames, int fRewrite, int fUseImps, int fLatchCorr, int fVerbose ); + extern Abc_Ntk_t * Abc_NtkDarSeqSweep( Abc_Ntk_t * pNtk, int nFramesP, int nFrames, int fRewrite, int fUseImps, int fLatchCorr, int fVerbose ); pNtk = Abc_FrameReadNtk(pAbc); pOut = Abc_FrameReadOut(pAbc); pErr = Abc_FrameReadErr(pAbc); // set defaults + nFramesP = 0; nFramesK = 1; fExdc = 1; fUseImps = 0; @@ -10992,10 +10994,21 @@ int Abc_CommandSeqSweep( Abc_Frame_t * pAbc, int argc, char ** argv ) fLatchCorr = 0; fVerbose = 0; Extra_UtilGetoptReset(); - while ( ( c = Extra_UtilGetopt( argc, argv, "Feirlvh" ) ) != EOF ) + while ( ( c = Extra_UtilGetopt( argc, argv, "PFeirlvh" ) ) != EOF ) { switch ( c ) { + case 'P': + if ( globalUtilOptind >= argc ) + { + fprintf( pErr, "Command line switch \"-P\" should be followed by an integer.\n" ); + goto usage; + } + nFramesP = atoi(argv[globalUtilOptind]); + globalUtilOptind++; + if ( nFramesP < 0 ) + goto usage; + break; case 'F': if ( globalUtilOptind >= argc ) { @@ -11048,7 +11061,7 @@ int Abc_CommandSeqSweep( Abc_Frame_t * pAbc, int argc, char ** argv ) } // get the new network - pNtkRes = Abc_NtkSeqSweep( pNtk, nFramesK, fRewrite, fUseImps, fLatchCorr, fVerbose ); + pNtkRes = Abc_NtkDarSeqSweep( pNtk, nFramesP, nFramesK, fRewrite, fUseImps, fLatchCorr, fVerbose ); if ( pNtkRes == NULL ) { fprintf( pErr, "Sequential sweeping has failed.\n" ); @@ -11059,8 +11072,9 @@ int Abc_CommandSeqSweep( Abc_Frame_t * pAbc, int argc, char ** argv ) return 0; usage: - fprintf( pErr, "usage: ssweep [-F num] [-ilrvh]\n" ); + fprintf( pErr, "usage: ssweep [-P num] [-F num] [-ilrvh]\n" ); fprintf( pErr, "\t performs sequential sweep using K-step induction\n" ); + fprintf( pErr, "\t-P num : number of time frames to use as the prefix [default = %d]\n", nFramesP ); fprintf( pErr, "\t-F num : number of time frames for induction (1=simple) [default = %d]\n", nFramesK ); // fprintf( pErr, "\t-e : toggle writing EXDC network [default = %s]\n", fExdc? "yes": "no" ); fprintf( pErr, "\t-i : toggle using implications [default = %s]\n", fUseImps? "yes": "no" ); diff --git a/src/base/abci/abcDar.c b/src/base/abci/abcDar.c index de527306..99217030 100644 --- a/src/base/abci/abcDar.c +++ b/src/base/abci/abcDar.c @@ -892,7 +892,7 @@ int Abc_NtkDSat( Abc_Ntk_t * pNtk, sint64 nConfLimit, sint64 nInsLimit, int fVer SeeAlso [] ***********************************************************************/ -Abc_Ntk_t * Abc_NtkSeqSweep( Abc_Ntk_t * pNtk, int nFramesK, int fRewrite, int fUseImps, int fLatchCorr, int fVerbose ) +Abc_Ntk_t * Abc_NtkDarSeqSweep( Abc_Ntk_t * pNtk, int nFramesP, int nFramesK, int fRewrite, int fUseImps, int fLatchCorr, int fVerbose ) { Fraig_Params_t Params; Abc_Ntk_t * pNtkAig, * pNtkFraig; @@ -911,7 +911,7 @@ Abc_Ntk_t * Abc_NtkSeqSweep( Abc_Ntk_t * pNtk, int nFramesK, int fRewrite, int f if ( pMan == NULL ) return NULL; - pMan = Fra_FraigInduction( pTemp = pMan, nFramesK, fRewrite, fUseImps, fLatchCorr, fVerbose, NULL ); + pMan = Fra_FraigInduction( pTemp = pMan, nFramesP, nFramesK, fRewrite, fUseImps, fLatchCorr, fVerbose, NULL ); Aig_ManStop( pTemp ); if ( Aig_ManRegNum(pMan) < Abc_NtkLatchNum(pNtk) ) diff --git a/src/base/abci/abcSweep.c b/src/base/abci/abcSweep.c index c4ec68f3..1ae8745b 100644 --- a/src/base/abci/abcSweep.c +++ b/src/base/abci/abcSweep.c @@ -335,8 +335,8 @@ void Abc_NtkFraigMergeClassMapped( Abc_Ntk_t * pNtk, Abc_Obj_t * pChain, int fUs { Arrival1 = Abc_NodeReadArrival(pNodeMin)->Worst; Arrival2 = Abc_NodeReadArrival(pNode )->Worst; - assert( Abc_ObjIsCi(pNodeMin) || Arrival1 > 0 ); - assert( Abc_ObjIsCi(pNode) || Arrival2 > 0 ); +// assert( Abc_ObjIsCi(pNodeMin) || Arrival1 > 0 ); +// assert( Abc_ObjIsCi(pNode) || Arrival2 > 0 ); if ( Arrival1 > Arrival2 || Arrival1 == Arrival2 && pNodeMin->Level > pNode->Level || Arrival1 == Arrival2 && pNodeMin->Level == pNode->Level && @@ -355,8 +355,8 @@ void Abc_NtkFraigMergeClassMapped( Abc_Ntk_t * pNtk, Abc_Obj_t * pChain, int fUs { Arrival1 = Abc_NodeReadArrival(pNodeMin)->Worst; Arrival2 = Abc_NodeReadArrival(pNode )->Worst; - assert( Abc_ObjIsCi(pNodeMin) || Arrival1 > 0 ); - assert( Abc_ObjIsCi(pNode) || Arrival2 > 0 ); +// assert( Abc_ObjIsCi(pNodeMin) || Arrival1 > 0 ); +// assert( Abc_ObjIsCi(pNode) || Arrival2 > 0 ); if ( Arrival1 > Arrival2 || Arrival1 == Arrival2 && pNodeMin->Level > pNode->Level || Arrival1 == Arrival2 && pNodeMin->Level == pNode->Level && @@ -21,6 +21,3 @@ - comparing tts of differently derived the same cut - area flow based AIG rewriting - cut frontier adjustment - - - |