diff options
author | Alan Mishchenko <alanmi@berkeley.edu> | 2007-07-31 08:01:00 -0700 |
---|---|---|
committer | Alan Mishchenko <alanmi@berkeley.edu> | 2007-07-31 08:01:00 -0700 |
commit | 29c9b0c0c4c66cb09b7c00c5c7290141be2af6a0 (patch) | |
tree | cd06159f7ddf9e75fc8dff354a7ef5c593b56856 /src/aig/fra | |
parent | fefd8b901d89ad0d977db8896c12123cc747e3d7 (diff) | |
download | abc-29c9b0c0c4c66cb09b7c00c5c7290141be2af6a0.tar.gz abc-29c9b0c0c4c66cb09b7c00c5c7290141be2af6a0.tar.bz2 abc-29c9b0c0c4c66cb09b7c00c5c7290141be2af6a0.zip |
Version abc70731
Diffstat (limited to 'src/aig/fra')
-rw-r--r-- | src/aig/fra/fra.h | 18 | ||||
-rw-r--r-- | src/aig/fra/fraClass.c | 25 | ||||
-rw-r--r-- | src/aig/fra/fraCore.c | 24 | ||||
-rw-r--r-- | src/aig/fra/fraInd.c | 108 | ||||
-rw-r--r-- | src/aig/fra/fraMan.c | 30 | ||||
-rw-r--r-- | src/aig/fra/fraSim.c | 24 |
6 files changed, 169 insertions, 60 deletions
diff --git a/src/aig/fra/fra.h b/src/aig/fra/fra.h index 91a1f8b1..5d357290 100644 --- a/src/aig/fra/fra.h +++ b/src/aig/fra/fra.h @@ -70,6 +70,7 @@ struct Fra_Par_t_ int nBTLimitNode; // conflict limit at a node int nBTLimitMiter; // conflict limit at an output int nFramesK; // the number of timeframes to unroll + int fRewrite; // use rewriting for constraint reduction }; // FRAIG equivalence classes @@ -121,11 +122,13 @@ struct Fra_Man_t_ // statistics int nSimRounds; int nNodesMiter; - int nClassesZero; - int nClassesBeg; - int nClassesEnd; - int nPairsBeg; - int nPairsEnd; + int nLitsZero; + int nLitsBeg; + int nLitsEnd; + int nNodesBeg; + int nNodesEnd; + int nRegsBeg; + int nRegsEnd; int nSatCalls; int nSatCallsSat; int nSatCallsUnsat; @@ -138,6 +141,7 @@ struct Fra_Man_t_ // runtime int timeSim; int timeTrav; + int timeRwr; int timeSat; int timeSatUnsat; int timeSatSat; @@ -182,7 +186,7 @@ static inline Aig_Obj_t * Fra_ObjChild1Fra( Aig_Obj_t * pObj, int i ) { assert( 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 ); -extern void Fra_ClassesPrint( Fra_Cla_t * p ); +extern void Fra_ClassesPrint( Fra_Cla_t * p, int fVeryVerbose ); extern void Fra_ClassesPrepare( Fra_Cla_t * p ); extern int Fra_ClassesRefine( Fra_Cla_t * p ); extern int Fra_ClassesRefine1( Fra_Cla_t * p ); @@ -197,7 +201,7 @@ extern Aig_Man_t * Fra_FraigChoice( Aig_Man_t * pManAig ); extern void Fra_FraigSweep( Fra_Man_t * pManAig ); /*=== fraDfs.c ========================================================*/ /*=== fraInd.c ========================================================*/ -extern Aig_Man_t * Fra_FraigInduction( Aig_Man_t * p, int nFramesK, int fVerbose ); +extern Aig_Man_t * Fra_FraigInduction( Aig_Man_t * p, int nFramesK, int fRewrite, int fVerbose ); /*=== fraMan.c ========================================================*/ extern void Fra_ParamsDefault( Fra_Par_t * pParams ); extern void Fra_ParamsDefaultSeq( Fra_Par_t * pParams ); diff --git a/src/aig/fra/fraClass.c b/src/aig/fra/fraClass.c index 05c07889..31d6270a 100644 --- a/src/aig/fra/fraClass.c +++ b/src/aig/fra/fraClass.c @@ -215,25 +215,28 @@ int Fra_ClassesCountPairs( Fra_Cla_t * p ) SeeAlso [] ***********************************************************************/ -void Fra_ClassesPrint( Fra_Cla_t * p ) +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", Vec_PtrSize(p->vClasses1), Vec_PtrSize(p->vClasses), Fra_ClassesCountLits(p) ); -/* - printf( "Constants { " ); - Vec_PtrForEachEntry( p->vClasses1, pObj, i ) - printf( "%d ", pObj->Id ); - printf( "}\n" ); - Vec_PtrForEachEntry( p->vClasses, pClass, i ) + + if ( fVeryVerbose ) { - printf( "%3d (%3d) : ", i, Fra_ClassCount(pClass) ); - Fra_PrintClass( pClass ); + printf( "Constants { " ); + Vec_PtrForEachEntry( p->vClasses1, pObj, i ) + printf( "%d ", pObj->Id ); + printf( "}\n" ); + Vec_PtrForEachEntry( p->vClasses, pClass, i ) + { + printf( "%3d (%3d) : ", i, Fra_ClassCount(pClass) ); + Fra_PrintClass( pClass ); + } + printf( "\n" ); } - printf( "\n" ); -*/ } /**Function************************************************************* diff --git a/src/aig/fra/fraCore.c b/src/aig/fra/fraCore.c index 9f2b8ca7..71e12a75 100644 --- a/src/aig/fra/fraCore.c +++ b/src/aig/fra/fraCore.c @@ -39,7 +39,7 @@ SeeAlso [] ***********************************************************************/ -void Fra_FraigNodeSpeculate( Fra_Man_t * p, Aig_Obj_t * pObj, Aig_Obj_t * pObjFraig, Aig_Obj_t * pObjReprFraig ) +static inline void Fra_FraigNodeSpeculate( Fra_Man_t * p, Aig_Obj_t * pObj, Aig_Obj_t * pObjFraig, Aig_Obj_t * pObjReprFraig ) { static int Counter = 0; char FileName[20]; @@ -47,8 +47,7 @@ void Fra_FraigNodeSpeculate( Fra_Man_t * p, Aig_Obj_t * pObj, Aig_Obj_t * pObjFr Aig_Obj_t * pNode; int i; // create manager with the logic for these two nodes - Aig_Obj_t * ppNodes[2] = { pObjFraig, pObjReprFraig }; - pTemp = Aig_ManExtractMiter( p->pManFraig, ppNodes, 2 ); + pTemp = Aig_ManExtractMiter( p->pManFraig, pObjFraig, pObjReprFraig ); // dump the logic into a file sprintf( FileName, "aig\\%03d.blif", ++Counter ); Aig_ManDumpBlif( pTemp, FileName ); @@ -70,7 +69,7 @@ void Fra_FraigNodeSpeculate( Fra_Man_t * p, Aig_Obj_t * pObj, Aig_Obj_t * pObjFr SeeAlso [] ***********************************************************************/ -void Fra_FraigNode( Fra_Man_t * p, Aig_Obj_t * pObj ) +static inline void Fra_FraigNode( Fra_Man_t * p, Aig_Obj_t * pObj ) { Aig_Obj_t * pObjRepr, * pObjFraig, * pObjFraig2, * pObjReprFraig; int RetValue; @@ -123,6 +122,8 @@ void Fra_FraigNode( Fra_Man_t * p, Aig_Obj_t * pObj ) // simulate the counter-example and return the Fraig node Fra_Resimulate( p ); assert( Fra_ClassObjRepr(pObj) != pObjRepr ); + if ( Fra_ClassObjRepr(pObj) == pObjRepr ) + printf( "Fra_FraigNode(): Error in class refinement!\n" ); } /**Function************************************************************* @@ -141,8 +142,6 @@ void Fra_FraigSweep( Fra_Man_t * p ) ProgressBar * pProgress; Aig_Obj_t * pObj, * pObjNew; int i, k = 0; -p->nClassesZero = Vec_PtrSize(p->pCla->vClasses1); -p->nClassesBeg = Vec_PtrSize(p->pCla->vClasses) + (int)(Vec_PtrSize(p->pCla->vClasses1) > 0); // duplicate internal nodes pProgress = Extra_ProgressBarStart( stdout, Aig_ManObjIdMax(p->pManAig) ); // fraig latch outputs @@ -163,7 +162,6 @@ p->nClassesBeg = Vec_PtrSize(p->pCla->vClasses) + (int)(Vec_PtrSize(p->pCla->vC Fra_FraigNode( p, pObj ); } Extra_ProgressBarStop( pProgress ); -p->nClassesEnd = Vec_PtrSize(p->pCla->vClasses) + (int)(Vec_PtrSize(p->pCla->vClasses1) > 0); // try to prove the outputs of the miter p->nNodesMiter = Aig_ManNodeNum(p->pManFraig); // Fra_MiterStatus( p->pManFraig ); @@ -196,15 +194,23 @@ clk = clock(); Fra_Simulate( p, 0 ); if ( p->pPars->fChoicing ) Aig_ManReprStart( p->pManFraig, Aig_ManObjIdMax(p->pManAig)+1 ); + // collect initial states + p->nLitsZero = Vec_PtrSize( p->pCla->vClasses1 ); + p->nLitsBeg = Fra_ClassesCountLits( p->pCla ); + p->nNodesBeg = Aig_ManNodeNum(pManAig); + p->nRegsBeg = Aig_ManRegNum(pManAig); + // perform fraig sweep Fra_FraigSweep( p ); Fra_ManFinalizeComb( p ); if ( p->pPars->fChoicing ) { + int clk2 = clock(); Fra_ClassesCopyReprs( p->pCla, p->vTimeouts ); pManAigNew = Aig_ManDupRepr( p->pManAig ); Aig_ManCreateChoices( pManAigNew ); Aig_ManStop( p->pManFraig ); p->pManFraig = NULL; +p->timeTrav += clock() - clk2; } else { @@ -221,6 +227,10 @@ clk = clock(); */ } p->timeTotal = clock() - clk; + // collect final stats + p->nLitsEnd = Fra_ClassesCountLits( p->pCla ); + p->nNodesEnd = Aig_ManNodeNum(pManAigNew); + p->nRegsEnd = Aig_ManRegNum(pManAigNew); Fra_ManStop( p ); return pManAigNew; } diff --git a/src/aig/fra/fraInd.c b/src/aig/fra/fraInd.c index 71e535f7..bb4c4287 100644 --- a/src/aig/fra/fraInd.c +++ b/src/aig/fra/fraInd.c @@ -20,6 +20,7 @@ #include "fra.h" #include "cnf.h" +#include "dar.h" //////////////////////////////////////////////////////////////////////// /// DECLARATIONS /// @@ -31,6 +32,54 @@ /**Function************************************************************* + Synopsis [Performs AIG rewriting on the constaint manager.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Fra_FraigInductionRewrite( Fra_Man_t * p ) +{ + Aig_Man_t * pTemp; + Aig_Obj_t * pObj, * pObjPo; + int nTruePis, k, i, clk = clock(); + // perform AIG rewriting on the speculated frames + pTemp = Aig_ManDup( p->pManFraig, 0 ); +// pTemp = Dar_ManRwsat( pTemp, 1, 0 ); + pTemp = Dar_ManRewriteDefault( pTemp ); + +// printf( "Before = %6d. After = %6d.\n", Aig_ManNodeNum(p->pManFraig), Aig_ManNodeNum(pTemp) ); +//Aig_ManDumpBlif( p->pManFraig, "1.blif" ); +//Aig_ManDumpBlif( pTemp, "2.blif" ); + +// Fra_FramesWriteCone( pTemp ); +// Aig_ManStop( pTemp ); + // transfer PI/register pointers + assert( p->pManFraig->nRegs == pTemp->nRegs ); + assert( p->pManFraig->nAsserts == pTemp->nAsserts ); + nTruePis = Aig_ManPiNum(p->pManAig) - Aig_ManRegNum(p->pManAig); + memset( p->pMemFraig, 0, sizeof(Aig_Obj_t *) * p->nSizeAlloc * p->nFramesAll ); + Fra_ObjSetFraig( Aig_ManConst1(p->pManAig), p->pPars->nFramesK, Aig_ManConst1(pTemp) ); + Aig_ManForEachPiSeq( p->pManAig, pObj, i ) + Fra_ObjSetFraig( pObj, p->pPars->nFramesK, Aig_ManPi(pTemp,nTruePis*p->pPars->nFramesK+i) ); + k = 0; + assert( Aig_ManRegNum(p->pManAig) == Aig_ManPoNum(pTemp) - pTemp->nAsserts ); + Aig_ManForEachLoSeq( p->pManAig, pObj, i ) + { + pObjPo = Aig_ManPo(pTemp, pTemp->nAsserts + k++); + Fra_ObjSetFraig( pObj, p->pPars->nFramesK, Aig_ObjChild0(pObjPo) ); + } + // exchange + Aig_ManStop( p->pManFraig ); + p->pManFraig = pTemp; +p->timeRwr += clock() - clk; +} + +/**Function************************************************************* + Synopsis [Performs speculative reduction for one node.] Description [] @@ -131,6 +180,8 @@ Aig_Man_t * Fra_FramesWithClasses( Fra_Man_t * p ) Aig_ManForEachLiSeq( p->pManAig, pObj, i ) Aig_ObjCreatePo( pManFraig, Fra_ObjChild0Fra(pObj,f-1) ); + // remove dangling nodes + Aig_ManCleanup( pManFraig ); // make sure the satisfying assignment is node assigned assert( pManFraig->pData == NULL ); return pManFraig; @@ -147,35 +198,39 @@ Aig_Man_t * Fra_FramesWithClasses( Fra_Man_t * p ) SeeAlso [] ***********************************************************************/ -Aig_Man_t * Fra_FraigInduction( Aig_Man_t * pManAig, int nFramesK, int fVerbose ) +Aig_Man_t * Fra_FraigInduction( Aig_Man_t * pManAig, int nFramesK, int fRewrite, int fVerbose ) { Fra_Man_t * p; Fra_Par_t Pars, * pPars = &Pars; Aig_Obj_t * pObj; Cnf_Dat_t * pCnf; Aig_Man_t * pManAigNew; - int nIter, i; + int nIter, i, clk = clock(), clk2; if ( Aig_ManNodeNum(pManAig) == 0 ) return Aig_ManDup(pManAig, 1); assert( Aig_ManLatchNum(pManAig) == 0 ); assert( Aig_ManRegNum(pManAig) > 0 ); assert( nFramesK > 0 ); +//Aig_ManShow( pManAig, 0, NULL ); // get parameters Fra_ParamsDefaultSeq( pPars ); pPars->nFramesK = nFramesK; pPars->fVerbose = fVerbose; + pPars->fRewrite = fRewrite; // start the fraig manager for this run p = Fra_ManStart( pManAig, pPars ); - // derive and refine e-classes using the 1st init frame + // derive and refine e-classes using K initialized frames Fra_Simulate( p, 1 ); -// Fra_ClassesTest( p->pCla, 2, 3 ); -//Aig_ManShow( pManAig, 0, NULL ); - - // refine e-classes using sequential simulation + // refine e-classes using sequential simulation? + p->nLitsZero = Vec_PtrSize( p->pCla->vClasses1 ); + p->nLitsBeg = Fra_ClassesCountLits( p->pCla ); + p->nNodesBeg = Aig_ManNodeNum(pManAig); + p->nRegsBeg = Aig_ManRegNum(pManAig); + // iterate the inductive case p->pCla->fRefinement = 1; for ( nIter = 0; p->pCla->fRefinement; nIter++ ) @@ -184,6 +239,10 @@ Aig_Man_t * Fra_FraigInduction( Aig_Man_t * pManAig, int nFramesK, int fVerbose p->pCla->fRefinement = 0; // derive non-init K-timeframes while implementing e-classes p->pManFraig = Fra_FramesWithClasses( p ); + // perform AIG rewriting + if ( p->pPars->fRewrite ) + Fra_FraigInductionRewrite( p ); + // report the intermediate results if ( fVerbose ) { printf( "%3d : Const = %6d. Class = %6d. L = %6d. LR = %6d. N = %6d. NR = %6d.\n", @@ -191,19 +250,22 @@ Aig_Man_t * Fra_FraigInduction( Aig_Man_t * pManAig, int nFramesK, int fVerbose Fra_ClassesCountLits(p->pCla), p->pManFraig->nAsserts, Aig_ManNodeNum(p->pManAig), Aig_ManNodeNum(p->pManFraig) ); } - // perform AIG rewriting on the speculated frames // convert the manager to SAT solver (the last nLatches outputs are inputs) -// pCnf = Cnf_Derive( p->pManFraig, Aig_ManRegNum(p->pManFraig) ); - pCnf = Cnf_DeriveSimple( p->pManFraig, Aig_ManRegNum(p->pManFraig) ); + pCnf = Cnf_Derive( p->pManFraig, Aig_ManRegNum(p->pManFraig) ); +// pCnf = Cnf_DeriveSimple( p->pManFraig, Aig_ManRegNum(p->pManFraig) ); //Cnf_DataWriteIntoFile( pCnf, "temp.cnf", 1 ); p->pSat = Cnf_DataWriteIntoSolver( pCnf ); p->nSatVars = pCnf->nVars; + assert( p->pSat != NULL ); + if ( p->pSat == NULL ) + printf( "Fra_FraigInduction(): Computed CNF is not valid.\n" ); // set the pointers to the manager Aig_ManForEachObj( p->pManFraig, pObj, i ) pObj->pData = p; + // transfer PI/LO variable numbers pObj = Aig_ManConst1( p->pManFraig ); Fra_ObjSetSatNum( pObj, pCnf->pVarNums[pObj->Id] ); @@ -216,20 +278,40 @@ Aig_Man_t * Fra_FraigInduction( Aig_Man_t * pManAig, int nFramesK, int fVerbose Fra_ObjSetFaninVec( pObj, (void *)1 ); } Cnf_DataFree( pCnf ); +/* + Aig_ManForEachObj( p->pManFraig, pObj, i ) + { + Fra_ObjSetSatNum( pObj, pCnf->pVarNums[pObj->Id] ); + Fra_ObjSetFaninVec( pObj, (void *)1 ); + } + Cnf_DataFree( pCnf ); +*/ // perform sweeping Fra_FraigSweep( p ); assert( p->vTimeouts == NULL ); + if ( p->vTimeouts ) + printf( "Fra_FraigInduction(): SAT solver timed out!\n" ); // cleanup Fra_ManClean( p ); } - - // move the classes into representatives + // move the classes into representatives and reduce AIG +clk2 = clock(); Fra_ClassesCopyReprs( p->pCla, p->vTimeouts ); - // implement the classes pManAigNew = Aig_ManDupRepr( pManAig ); +p->timeTrav += clock() - clk2; +p->timeTotal = clock() - clk; + // get the final stats + p->nLitsEnd = Fra_ClassesCountLits( p->pCla ); + p->nNodesEnd = Aig_ManNodeNum(pManAigNew); + p->nRegsEnd = Aig_ManRegNum(pManAigNew); + // free the manager Fra_ManStop( p ); + // check the output + if ( Aig_ManPoNum(pManAigNew) - Aig_ManRegNum(pManAigNew) == 1 ) + if ( Aig_ObjChild0( Aig_ManPo(pManAigNew,0) ) == Aig_ManConst0(pManAigNew) ) + printf( "Proved output constant 0.\n" ); return pManAigNew; } diff --git a/src/aig/fra/fraMan.c b/src/aig/fra/fraMan.c index fdd1ccc5..95cf28d8 100644 --- a/src/aig/fra/fraMan.c +++ b/src/aig/fra/fraMan.c @@ -55,6 +55,7 @@ void Fra_ParamsDefault( Fra_Par_t * pPars ) pPars->nBTLimitMiter = 500000; // conflict limit at an output pPars->nFramesK = 0; // the number of timeframes to unroll pPars->fConeBias = 1; + pPars->fRewrite = 0; } /**Function************************************************************* @@ -71,7 +72,7 @@ void Fra_ParamsDefault( Fra_Par_t * pPars ) void Fra_ParamsDefaultSeq( Fra_Par_t * pPars ) { memset( pPars, 0, sizeof(Fra_Par_t) ); - pPars->nSimWords = 4; // the number of words in the simulation info + pPars->nSimWords = 1; // the number of words in the simulation info pPars->dSimSatur = 0.005; // the ratio of refined classes when saturation is reached pPars->fPatScores = 0; // enables simulation pattern scoring pPars->MaxScore = 25; // max score after which resimulation is used @@ -80,10 +81,11 @@ void Fra_ParamsDefaultSeq( Fra_Par_t * pPars ) // pPars->dActConeBumpMax = 5.0; // the largest bump of activity pPars->dActConeRatio = 0.3; // the ratio of cone to be bumped pPars->dActConeBumpMax = 10.0; // the largest bump of activity - pPars->nBTLimitNode = 1000000; // conflict limit at a node + pPars->nBTLimitNode =10000000; // conflict limit at a node pPars->nBTLimitMiter = 500000; // conflict limit at an output pPars->nFramesK = 1; // the number of timeframes to unroll pPars->fConeBias = 0; + pPars->fRewrite = 0; } /**Function************************************************************* @@ -165,7 +167,6 @@ void Fra_ManClean( Fra_Man_t * p ) sat_solver_delete( p->pSat ); p->pSat = NULL; - p->nSatVars = 0; } /**Function************************************************************* @@ -268,23 +269,28 @@ void Fra_ManStop( Fra_Man_t * p ) void Fra_ManPrint( Fra_Man_t * p ) { double nMemory = 1.0*Aig_ManObjIdMax(p->pManAig)*((p->nSimWords+2)*sizeof(unsigned)+6*sizeof(void*))/(1<<20); - printf( "SimWords = %d. Rounds = %d. Mem = %0.2f Mb. ", p->nSimWords, p->nSimRounds, nMemory ); - printf( "Classes: Beg = %d. End = %d.\n", p->nClassesBeg, p->nClassesEnd ); - printf( "Limits: BTNode = %d. BTMiter = %d.\n", p->pPars->nBTLimitNode, p->pPars->nBTLimitMiter ); - printf( "Proof = %d. Counter-example = %d. Fail = %d. FailReal = %d. Zero = %d.\n", - p->nSatProof, p->nSatCallsSat, p->nSatFails, p->nSatFailsReal, p->nClassesZero ); - printf( "Final = %d. Miter = %d. Total = %d. Mux = %d. (Exor = %d.) SatVars = %d.\n", - p->pManFraig? Aig_ManNodeNum(p->pManFraig) : -1, p->nNodesMiter, Aig_ManNodeNum(p->pManAig), 0, 0, p->nSatVars ); + printf( "SimWord = %d. Round = %d. Mem = %0.2f Mb. LitBeg = %d. LitEnd = %d. (%6.2f %%).\n", + p->nSimWords, p->nSimRounds, nMemory, p->nLitsBeg, p->nLitsEnd, 100.0*p->nLitsEnd/p->nLitsBeg ); + printf( "Proof = %d. Cex = %d. Fail = %d. FailReal = %d. Zero = %d. C-lim = %d. Vars = %d.\n", + p->nSatProof, p->nSatCallsSat, p->nSatFails, p->nSatFailsReal, p->nLitsZero, p->pPars->nBTLimitNode, p->nSatVars ); + printf( "NBeg = %d. NEnd = %d. (Gain = %6.2f %%). RBeg = %d. REnd = %d. (Gain = %6.2f %%).\n", + p->nNodesBeg, p->nNodesEnd, 100.0*(p->nNodesBeg-p->nNodesEnd)/p->nNodesBeg, + p->nRegsBeg, p->nRegsEnd, 100.0*(p->nRegsBeg-p->nRegsEnd)/p->nRegsBeg ); if ( p->pSat ) Sat_SolverPrintStats( stdout, p->pSat ); PRT( "AIG simulation ", p->timeSim ); - PRT( "AIG traversal ", p->timeTrav ); - PRT( "SAT solving ", p->timeSat ); + PRT( "AIG traversal ", p->timeTrav ); + if ( p->timeRwr ) + { + PRT( "AIG rewriting ", p->timeRwr ); + } + PRT( "SAT solving ", p->timeSat ); PRT( " Unsat ", p->timeSatUnsat ); PRT( " Sat ", p->timeSatSat ); PRT( " Fail ", p->timeSatFail ); PRT( "Class refining ", p->timeRef ); PRT( "TOTAL RUNTIME ", p->timeTotal ); if ( p->time1 ) { PRT( "time1 ", p->time1 ); } + if ( p->nSpeculs ) printf( "Speculations = %d.\n", p->nSpeculs ); } diff --git a/src/aig/fra/fraSim.c b/src/aig/fra/fraSim.c index 4ae8a686..4a6e0251 100644 --- a/src/aig/fra/fraSim.c +++ b/src/aig/fra/fraSim.c @@ -142,10 +142,14 @@ void Fra_AssignDist1( Fra_Man_t * p, unsigned * pPat ) Fra_NodeAssignConst( p, pObj, Aig_InfoHasBit(pPat, nTruePis * p->nFramesAll + k++), 0 ); assert( p->pManFraig == NULL || nTruePis * p->nFramesAll + k == Aig_ManPiNum(p->pManFraig) ); - // flip one bit of the first frame - Limit = AIG_MIN( nTruePis, p->pPars->nSimWords * 32 - 1 ); - for ( i = 0; i < Limit; i++ ) - Aig_InfoXorBit( Fra_ObjSim( Aig_ManPi(p->pManAig,i) ), i+1 ); + // flip one bit of the last frame + if ( p->nFramesAll == 2 ) + { + Limit = AIG_MIN( nTruePis, p->pPars->nSimWords * 32 - 1 ); + for ( i = 0; i < Limit; i++ ) + Aig_InfoXorBit( Fra_ObjSim( Aig_ManPi(p->pManAig, i) ), i+1 ); +// Aig_InfoXorBit( Fra_ObjSim( Aig_ManPi(p->pManAig, nTruePis*(p->nFramesAll-2) + i) ), i+1 ); + } } } @@ -261,8 +265,8 @@ void Fra_NodeSimulate( Fra_Man_t * p, Aig_Obj_t * pObj, int iFrame ) pSims1 = Fra_ObjSim(Aig_ObjFanin1(pObj)) + nSimWords * iFrame; // get complemented attributes of the children using their random info fCompl = pObj->fPhase; - fCompl0 = Aig_ObjFaninPhase(Aig_ObjChild0(pObj)); - fCompl1 = Aig_ObjFaninPhase(Aig_ObjChild1(pObj)); + fCompl0 = Aig_ObjPhaseReal(Aig_ObjChild0(pObj)); + fCompl1 = Aig_ObjPhaseReal(Aig_ObjChild1(pObj)); // simulate if ( fCompl0 && fCompl1 ) { @@ -326,7 +330,7 @@ void Fra_NodeCopyFanin( Fra_Man_t * p, Aig_Obj_t * pObj, int iFrame ) pSims0 = Fra_ObjSim(Aig_ObjFanin0(pObj)) + nSimWords * iFrame; // get complemented attributes of the children using their random info fCompl = pObj->fPhase; - fCompl0 = Aig_ObjFaninPhase(Aig_ObjChild0(pObj)); + fCompl0 = Aig_ObjPhaseReal(Aig_ObjChild0(pObj)); // copy information as it is if ( fCompl0 ) for ( i = 0; i < nSimWords; i++ ) @@ -624,7 +628,7 @@ void Fra_Simulate( Fra_Man_t * p, int fInit ) Fra_AssignRandom( p, fInit ); Fra_SimulateOne( p ); Fra_ClassesPrepare( p->pCla ); -// Fra_ClassesPrint( p->pCla ); +// Fra_ClassesPrint( p->pCla, 0 ); //printf( "Starting classes = %5d. Pairs = %6d.\n", p->lClasses.nItems, Fra_CountPairsClasses(p) ); // refine classes by walking 0/1 patterns @@ -667,7 +671,7 @@ p->timeRef += clock() - clk; // printf( "Consts = %6d. Classes = %6d. Literals = %6d.\n", // Vec_PtrSize(p->pCla->vClasses1), Vec_PtrSize(p->pCla->vClasses), Fra_ClassesCountLits(p->pCla) ); -// Fra_ClassesPrint( p->pCla ); +// Fra_ClassesPrint( p->pCla, 0 ); } /**Function************************************************************* @@ -729,7 +733,7 @@ int Fra_CheckOutputSims( Fra_Man_t * p ) int i; // make sure the reference simulation pattern does not detect the bug pObj = Aig_ManPo( p->pManAig, 0 ); - assert( Aig_ObjFanin0(pObj)->fPhase == (unsigned)Aig_ObjFaninC0(pObj) ); // Aig_ObjFaninPhase(Aig_ObjChild0(pObj)) == 0 + assert( Aig_ObjFanin0(pObj)->fPhase == (unsigned)Aig_ObjFaninC0(pObj) ); Aig_ManForEachPo( p->pManAig, pObj, i ) { if ( !Fra_NodeHasZeroSim( Aig_ObjFanin0(pObj) ) ) |