From a30c08bbe55d624ec3269577bf16f2f09215be12 Mon Sep 17 00:00:00 2001 From: Alan Mishchenko Date: Tue, 9 Sep 2008 08:01:00 -0700 Subject: Version abc80909 --- src/aig/aig/aigPartReg.c | 2 +- src/aig/aig/aigPartSat.c | 2 +- src/aig/dar/darCore.c | 2 +- src/aig/fra/fraClass.c | 1 + src/aig/fra/fraInd.c | 6 +- src/aig/fra/fraLcr.c | 3 + src/aig/saig/saigPhase.c | 5 + src/aig/ssw/module.make | 1 + src/aig/ssw/ssw.h | 12 + src/aig/ssw/sswAig.c | 1 - src/aig/ssw/sswClass.c | 35 +- src/aig/ssw/sswCnf.c | 2 +- src/aig/ssw/sswCore.c | 38 +- src/aig/ssw/sswInt.h | 40 +- src/aig/ssw/sswMan.c | 53 +- src/aig/ssw/sswSat.c | 14 +- src/aig/ssw/sswSim.c | 1263 ++++++++++++++++++++++++++++++++++++++++++++++ src/aig/ssw/sswSimSat.c | 55 +- src/aig/ssw/sswSweep.c | 23 +- src/base/abci/abc.c | 11 +- src/base/abci/abcDar.c | 1 + src/map/mio/mio.c | 3 + 22 files changed, 1501 insertions(+), 72 deletions(-) create mode 100644 src/aig/ssw/sswSim.c (limited to 'src') diff --git a/src/aig/aig/aigPartReg.c b/src/aig/aig/aigPartReg.c index 79761a41..6baeae31 100644 --- a/src/aig/aig/aigPartReg.c +++ b/src/aig/aig/aigPartReg.c @@ -19,7 +19,7 @@ ***********************************************************************/ #include "aig.h" -#include "fra.h" +//#include "fra.h" //////////////////////////////////////////////////////////////////////// /// DECLARATIONS /// diff --git a/src/aig/aig/aigPartSat.c b/src/aig/aig/aigPartSat.c index 2a3e975c..15aa1a05 100644 --- a/src/aig/aig/aigPartSat.c +++ b/src/aig/aig/aigPartSat.c @@ -494,7 +494,7 @@ int Aig_ManPartitionedSat( Aig_Man_t * p, int nAlgo, int nPartSize, Aig_Man_t * pAig, * pTemp; Vec_Int_t * vNode2Part, * vNode2Var; int nConfRemaining = nConfTotal, nNodes = 0; - int i, clk, status, RetValue; + int i, clk, status, RetValue = -1; // perform partitioning according to the selected algorithm clk = clock(); diff --git a/src/aig/dar/darCore.c b/src/aig/dar/darCore.c index ed461de5..3916a0b0 100644 --- a/src/aig/dar/darCore.c +++ b/src/aig/dar/darCore.c @@ -264,7 +264,7 @@ Aig_MmFixed_t * Dar_ManComputeCuts( Aig_Man_t * pAig, int nCutsMax, int fVerbose printf( "Nodes = %6d. Total cuts = %6d. 4-input cuts = %6d.\n", Aig_ManObjNum(pAig), nCuts, nCutsK ); printf( "Cut size = %2d. Truth size = %2d. Total mem = %5.2f Mb ", - sizeof(Dar_Cut_t), (int)4, 1.0*Aig_MmFixedReadMemUsage(p->pMemCuts)/(1<<20) ); + (int)sizeof(Dar_Cut_t), (int)4, 1.0*Aig_MmFixedReadMemUsage(p->pMemCuts)/(1<<20) ); PRT( "Runtime", clock() - clk ); /* Aig_ManForEachNode( pAig, pObj, i ) diff --git a/src/aig/fra/fraClass.c b/src/aig/fra/fraClass.c index 442cf80e..064d2b9c 100644 --- a/src/aig/fra/fraClass.c +++ b/src/aig/fra/fraClass.c @@ -378,6 +378,7 @@ void Fra_ClassesPrepare( Fra_Cla_t * p, int fLatchCorr, int nMaxLevs ) free( ppNexts ); // now it is time to refine the classes Fra_ClassesRefine( p ); +// Fra_ClassesPrint( p, 0 ); } /**Function************************************************************* diff --git a/src/aig/fra/fraInd.c b/src/aig/fra/fraInd.c index 76c7abad..ce9ec69b 100644 --- a/src/aig/fra/fraInd.c +++ b/src/aig/fra/fraInd.c @@ -568,7 +568,7 @@ p->timeTrav += clock() - clk2; Fra_OneHotAssume( p, p->vOneHots ); // if ( p->pManAig->vOnehots ) // Fra_OneHotAddKnownConstraint( p, p->pManAig->vOnehots ); - + // report the intermediate results if ( pPars->fVerbose ) { @@ -580,7 +580,6 @@ p->timeTrav += clock() - clk2; if ( p->pPars->fUse1Hot ) printf( "1h = %6d. ", Fra_OneHotCount(p, p->vOneHots) ); printf( "NR = %6d. ", Aig_ManNodeNum(p->pManFraig) ); - PRT( "T", clock() - clk3 ); // printf( "\n" ); } @@ -593,12 +592,13 @@ clk2 = clock(); Fra_FraigSweep( p ); if ( pPars->fVerbose ) { -// PRT( "t", clock() - clk2 ); + PRT( "T", clock() - clk3 ); } // Sat_SolverPrintStats( stdout, p->pSat ); // remove FRAIG and SAT solver Aig_ManStop( p->pManFraig ); p->pManFraig = NULL; +// printf( "Vars = %d. Clauses = %d. Learnts = %d.\n", p->pSat->size, p->pSat->clauses.size, p->pSat->learnts.size ); sat_solver_delete( p->pSat ); p->pSat = NULL; memset( p->pMemFraig, 0, sizeof(Aig_Obj_t *) * p->nSizeAlloc * p->nFramesAll ); // printf( "Recent SAT called = %d. Skipped = %d.\n", p->nSatCallsRecent, p->nSatCallsSkipped ); diff --git a/src/aig/fra/fraLcr.c b/src/aig/fra/fraLcr.c index 92e0d94b..4b2383aa 100644 --- a/src/aig/fra/fraLcr.c +++ b/src/aig/fra/fraLcr.c @@ -629,6 +629,9 @@ clk2 = clock(); p->timeFraig += clock() - clk2; Vec_PtrPush( p->vFraigs, pAigTemp ); Aig_ManStop( pAigPart ); + +//intf( "finished part %d (out of %d)\n", i, Vec_PtrSize(p->vParts) ); + } Fra_ClassNodesUnmark( p ); // report the intermediate results diff --git a/src/aig/saig/saigPhase.c b/src/aig/saig/saigPhase.c index 323a230f..12d323e2 100644 --- a/src/aig/saig/saigPhase.c +++ b/src/aig/saig/saigPhase.c @@ -886,6 +886,11 @@ Aig_Man_t * Saig_ManPhaseAbstractAuto( Aig_Man_t * p, int fVerbose ) Saig_TsiStop( pTsi ); if ( pNew == NULL ) pNew = Aig_ManDupSimple( p ); + if ( Aig_ManPiNum(pNew) == Aig_ManRegNum(pNew) ) + { + Aig_ManStop( pNew); + pNew = Aig_ManDupSimple( p ); + } return pNew; } diff --git a/src/aig/ssw/module.make b/src/aig/ssw/module.make index dcbe0081..2619751e 100644 --- a/src/aig/ssw/module.make +++ b/src/aig/ssw/module.make @@ -4,5 +4,6 @@ SRC += src/aig/ssw/sswAig.c \ src/aig/ssw/sswCore.c \ src/aig/ssw/sswMan.c \ src/aig/ssw/sswSat.c \ + src/aig/ssw/sswSim.c \ src/aig/ssw/sswSimSat.c \ src/aig/ssw/sswSweep.c diff --git a/src/aig/ssw/ssw.h b/src/aig/ssw/ssw.h index 3bdc63f6..aaaa6407 100644 --- a/src/aig/ssw/ssw.h +++ b/src/aig/ssw/ssw.h @@ -54,6 +54,18 @@ struct Ssw_Pars_t_ int nIters; // the number of iterations performed }; +// sequential counter-example +typedef struct Ssw_Cex_t_ Ssw_Cex_t; +struct Ssw_Cex_t_ +{ + int iPo; // the zero-based number of PO, for which verification failed + int iFrame; // the zero-based number of the time-frame, for which verificaiton failed + int nRegs; // the number of registers in the miter + int nPis; // the number of primary inputs in the miter + int nBits; // the number of words of bit data used + unsigned pData[0]; // the cex bit data (the number of bits: nRegs + (iFrame+1) * nPis) +}; + //////////////////////////////////////////////////////////////////////// /// MACRO DEFINITIONS /// //////////////////////////////////////////////////////////////////////// diff --git a/src/aig/ssw/sswAig.c b/src/aig/ssw/sswAig.c index 9304edc7..854a0e12 100644 --- a/src/aig/ssw/sswAig.c +++ b/src/aig/ssw/sswAig.c @@ -28,7 +28,6 @@ /// FUNCTION DEFINITIONS /// //////////////////////////////////////////////////////////////////////// - /**Function************************************************************* Synopsis [Performs speculative reduction for one node.] diff --git a/src/aig/ssw/sswClass.c b/src/aig/ssw/sswClass.c index c84a5d3d..66b86009 100644 --- a/src/aig/ssw/sswClass.c +++ b/src/aig/ssw/sswClass.c @@ -335,7 +335,7 @@ void Ssw_ClassesPrint( Ssw_Cla_t * p, int fVeryVerbose ) Aig_Obj_t * pObj; int i; printf( "Equivalence classes: Const1 = %5d. Class = %5d. Lit = %5d.\n", - p->nCands1, p->nClasses, p->nLits ); + p->nCands1, p->nClasses, p->nCands1+p->nLits ); if ( !fVeryVerbose ) return; printf( "Constants { " ); @@ -368,12 +368,13 @@ void Ssw_ClassesRemoveNode( Ssw_Cla_t * p, Aig_Obj_t * pObj ) assert( p->pId2Class[pObj->Id] == NULL ); pRepr = Aig_ObjRepr( p->pAig, pObj ); assert( pRepr != NULL ); - Aig_ObjSetRepr( p->pAig, pObj, NULL ); if ( Ssw_ObjIsConst1Cand( p->pAig, pObj ) ) { + Aig_ObjSetRepr( p->pAig, pObj, NULL ); p->nCands1--; return; } + Aig_ObjSetRepr( p->pAig, pObj, NULL ); assert( p->pId2Class[pRepr->Id][0] == pRepr ); assert( p->pClassSizes[pRepr->Id] >= 2 ); if ( p->pClassSizes[pRepr->Id] == 2 ) @@ -408,11 +409,26 @@ void Ssw_ClassesRemoveNode( Ssw_Cla_t * p, Aig_Obj_t * pObj ) SeeAlso [] ***********************************************************************/ -void Ssw_ClassesPrepare( Ssw_Cla_t * p, int fLatchCorr, int nMaxLevs ) +Ssw_Cla_t * Ssw_ClassesPrepare( Aig_Man_t * pAig, int fLatchCorr, int nMaxLevs ) { + Ssw_Cla_t * p; + Ssw_Sml_t * pSml; Aig_Obj_t ** ppTable, ** ppNexts, ** ppClassNew; Aig_Obj_t * pObj, * pTemp, * pRepr; int i, k, nTableSize, nNodes, iEntry, nEntries, nEntries2; + int clk; + + // start the classes + p = Ssw_ClassesStart( pAig ); + + // perform sequential simulation +clk = clock(); + pSml = Ssw_SmlSimulateSeq( pAig, 0, 32, 4 ); +PRT( "Simulation of 32 frames with 4 words", clock() - clk ); + + // set comparison procedures +clk = clock(); + Ssw_ClassesSetData( p, pSml, Ssw_SmlNodeHash, Ssw_SmlNodeIsConst, Ssw_SmlNodesAreEqual ); // allocate the hash table hashing simulation info into nodes nTableSize = Aig_PrimeCudd( Aig_ManObjNumMax(p->pAig)/4 ); @@ -430,7 +446,7 @@ void Ssw_ClassesPrepare( Ssw_Cla_t * p, int fLatchCorr, int nMaxLevs ) } else { - if ( !Aig_ObjIsNode(pObj) && !Saig_ObjIsPi(p->pAig, pObj) ) + if ( !Aig_ObjIsNode(pObj) && !Aig_ObjIsPi(pObj) ) continue; // skip the node with more that the given number of levels if ( nMaxLevs && (int)pObj->Level > nMaxLevs ) @@ -499,9 +515,14 @@ void Ssw_ClassesPrepare( Ssw_Cla_t * p, int fLatchCorr, int nMaxLevs ) assert( nEntries == nEntries2 ); free( ppTable ); free( ppNexts ); + // now it is time to refine the classes - Ssw_ClassesRefine( p ); + Ssw_ClassesRefine( p, 1 ); Ssw_ClassesCheck( p ); + Ssw_SmlStop( pSml ); +// Ssw_ClassesPrint( p, 0 ); +PRT( "Collecting candidate equival classes", clock() - clk ); + return p; } /**Function************************************************************* @@ -654,12 +675,12 @@ int Ssw_ClassesRefineOneClass( Ssw_Cla_t * p, Aig_Obj_t * pReprOld, int fRecursi SeeAlso [] ***********************************************************************/ -int Ssw_ClassesRefine( Ssw_Cla_t * p ) +int Ssw_ClassesRefine( Ssw_Cla_t * p, int fRecursive ) { Aig_Obj_t ** ppClass; int i, nRefis = 0; Ssw_ManForEachClass( p, ppClass, i ) - nRefis += Ssw_ClassesRefineOneClass( p, ppClass[0], 0 ); + nRefis += Ssw_ClassesRefineOneClass( p, ppClass[0], fRecursive ); return nRefis; } diff --git a/src/aig/ssw/sswCnf.c b/src/aig/ssw/sswCnf.c index f5047400..b047a312 100644 --- a/src/aig/ssw/sswCnf.c +++ b/src/aig/ssw/sswCnf.c @@ -264,8 +264,8 @@ void Ssw_ObjAddToFrontier( Ssw_Man_t * p, Aig_Obj_t * pObj, Vec_Ptr_t * vFrontie assert( Ssw_ObjSatNum(p,pObj) == 0 ); if ( Aig_ObjIsConst1(pObj) ) return; -// Vec_PtrPush( p->vUsedNodes, pObj ); Ssw_ObjSetSatNum( p, pObj, p->nSatVars++ ); + sat_solver_setnvars( p->pSat, 100 * (1 + p->nSatVars / 100) ); if ( Aig_ObjIsNode(pObj) ) Vec_PtrPush( vFrontier, pObj ); } diff --git a/src/aig/ssw/sswCore.c b/src/aig/ssw/sswCore.c index 6c19ab70..409a1ebe 100644 --- a/src/aig/ssw/sswCore.c +++ b/src/aig/ssw/sswCore.c @@ -48,8 +48,8 @@ void Ssw_ManSetDefaultParams( Ssw_Pars_t * p ) p->nConstrs = 0; // treat the last nConstrs POs as seq constraints p->nBTLimit = 1000; // conflict limit at a node p->fPolarFlip = 0; // uses polarity adjustment - p->fLatchCorr = 1; // performs register correspondence - p->fVerbose = 1; // verbose stats + p->fLatchCorr = 0; // performs register correspondence + p->fVerbose = 0; // verbose stats p->nIters = 0; // the number of iterations performed } @@ -70,18 +70,40 @@ Aig_Man_t * Ssw_SignalCorrespondence( Aig_Man_t * pAig, Ssw_Pars_t * pPars ) Ssw_Man_t * p; int RetValue, nIter, clk, clkTotal = clock(); // reset random numbers - Aig_ManRandom(1); + Aig_ManRandom( 1 ); // start the choicing manager p = Ssw_ManCreate( pAig, pPars ); // compute candidate equivalence classes - p->ppClasses = Ssw_ClassesPrepareSimple( pAig, pPars->fLatchCorr, pPars->nMaxLevs ); + if ( p->pPars->nConstrs == 0 ) + { + p->ppClasses = Ssw_ClassesPrepare( pAig, pPars->fLatchCorr, pPars->nMaxLevs ); + p->pSml = Ssw_SmlStart( pAig, 0, p->nFrames + 2, 2 ); + Ssw_ClassesSetData( p->ppClasses, p->pSml, Ssw_SmlNodeHash, Ssw_SmlNodeIsConst, Ssw_SmlNodesAreEqual ); + } + else + { + assert( 0 ); + p->ppClasses = Ssw_ClassesPrepareSimple( pAig, pPars->fLatchCorr, pPars->nMaxLevs ); + } +// Ssw_ClassesSetData( p->ppClasses, NULL, NULL, Ssw_NodeIsConstCex, Ssw_NodesAreEqualCex ); + + // get the starting stats + p->nLitsBeg = Ssw_ClassesLitNum( p->ppClasses ); + p->nNodesBeg = Aig_ManNodeNum(pAig); + p->nRegsBeg = Aig_ManRegNum(pAig); // refine classes using BMC if ( pPars->fVerbose ) + { + printf( "Before BMC: " ); Ssw_ClassesPrint( p->ppClasses, 0 ); + } Ssw_ManSweepBmc( p ); Ssw_ManCleanup( p ); if ( pPars->fVerbose ) + { + printf( "After BMC: " ); Ssw_ClassesPrint( p->ppClasses, 0 ); + } // refine classes using induction for ( nIter = 0; ; nIter++ ) { @@ -98,10 +120,16 @@ clk = clock(); if ( !RetValue ) break; } + p->pPars->nIters = nIter + 1; p->timeTotal = clock() - clkTotal; - Ssw_ManStop( p ); pAigNew = Aig_ManDupRepr( pAig, 0 ); Aig_ManSeqCleanup( pAigNew ); + // get the final stats + p->nLitsEnd = Ssw_ClassesLitNum( p->ppClasses ); + p->nNodesEnd = Aig_ManNodeNum(pAigNew); + p->nRegsEnd = Aig_ManRegNum(pAigNew); + // cleanup + Ssw_ManStop( p ); return pAigNew; } diff --git a/src/aig/ssw/sswInt.h b/src/aig/ssw/sswInt.h index 21621c0d..009c09c4 100644 --- a/src/aig/ssw/sswInt.h +++ b/src/aig/ssw/sswInt.h @@ -41,11 +41,10 @@ extern "C" { /// BASIC TYPES /// //////////////////////////////////////////////////////////////////////// -// equivalence classes -typedef struct Ssw_Cla_t_ Ssw_Cla_t; +typedef struct Ssw_Man_t_ Ssw_Man_t; // signal correspondence manager +typedef struct Ssw_Cla_t_ Ssw_Cla_t; // equivalence classe manager +typedef struct Ssw_Sml_t_ Ssw_Sml_t; // sequential simulation manager -// manager -typedef struct Ssw_Man_t_ Ssw_Man_t; struct Ssw_Man_t_ { // parameters @@ -57,25 +56,38 @@ struct Ssw_Man_t_ Aig_Obj_t ** pNodeToFraig; // mapping of AIG nodes into FRAIG nodes // equivalence classes Ssw_Cla_t * ppClasses; // equivalence classes of nodes -// Aig_Obj_t ** pReprsProved; // equivalences proved int fRefined; // is set to 1 when refinement happens // SAT solving sat_solver * pSat; // recyclable SAT solver int nSatVars; // the counter of SAT variables int * pSatVars; // mapping of each node into its SAT var + int nSatVarsTotal; // the total number of SAT vars created Vec_Ptr_t * vFanins; // fanins of the CNF node Vec_Ptr_t * vSimRoots; // the roots of cand const 1 nodes to simulate Vec_Ptr_t * vSimClasses; // the roots of cand equiv classes to simulate + // sequential simulator + Ssw_Sml_t * pSml; + // counter example storage + int nPatWords; // the number of words in the counter example + unsigned * pPatWords; // the counter example // constraints int nConstrTotal; // the number of total constraints int nConstrReduced; // the number of reduced constraints - int nStragers; + int nStrangers; // the number of strange situations // SAT calls statistics int nSatCalls; // the number of SAT calls int nSatProof; // the number of proofs + int nSatFails; // the number of timeouts int nSatFailsReal; // the number of timeouts int nSatCallsUnsat; // the number of unsat SAT calls int nSatCallsSat; // the number of sat SAT calls + // node/register/lit statistics + int nLitsBeg; + int nLitsEnd; + int nNodesBeg; + int nNodesEnd; + int nRegsBeg; + int nRegsEnd; // runtime stats int timeBmc; // bounded model checking int timeReduce; // speculative reduction @@ -131,12 +143,14 @@ extern Aig_Obj_t ** Ssw_ClassesReadClass( Ssw_Cla_t * p, Aig_Obj_t * pRepr, int extern void Ssw_ClassesCheck( Ssw_Cla_t * p ); extern void Ssw_ClassesPrint( Ssw_Cla_t * p, int fVeryVerbose ); extern void Ssw_ClassesRemoveNode( Ssw_Cla_t * p, Aig_Obj_t * pObj ); -extern void Ssw_ClassesPrepare( Ssw_Cla_t * p, int fLatchCorr, int nMaxLevs ); +extern Ssw_Cla_t * Ssw_ClassesPrepare( Aig_Man_t * pAig, int fLatchCorr, int nMaxLevs ); extern Ssw_Cla_t * Ssw_ClassesPrepareSimple( Aig_Man_t * pAig, int fLatchCorr, int nMaxLevs ); -extern int Ssw_ClassesRefine( Ssw_Cla_t * p ); +extern int Ssw_ClassesRefine( Ssw_Cla_t * p, int fRecursive ); extern int Ssw_ClassesRefineOneClass( Ssw_Cla_t * p, Aig_Obj_t * pRepr, int fRecursive ); extern int Ssw_ClassesRefineConst1Group( Ssw_Cla_t * p, Vec_Ptr_t * vRoots, int fRecursive ); extern int Ssw_ClassesRefineConst1( Ssw_Cla_t * p, int fRecursive ); +extern int Ssw_NodeIsConstCex( void * p, Aig_Obj_t * pObj ); +extern int Ssw_NodesAreEqualCex( void * p, Aig_Obj_t * pObj0, Aig_Obj_t * pObj1 ); /*=== sswCnf.c ===================================================*/ extern void Ssw_CnfNodeAddToSolver( Ssw_Man_t * p, Aig_Obj_t * pObj ); /*=== sswMan.c ===================================================*/ @@ -147,9 +161,19 @@ extern void Ssw_ManStartSolver( Ssw_Man_t * p ); /*=== sswSat.c ===================================================*/ extern int Ssw_NodesAreEquiv( Ssw_Man_t * p, Aig_Obj_t * pOld, Aig_Obj_t * pNew ); extern int Ssw_NodesAreConstrained( Ssw_Man_t * p, Aig_Obj_t * pOld, Aig_Obj_t * pNew ); +/*=== sswSim.c ===================================================*/ +extern Ssw_Sml_t * Ssw_SmlStart( Aig_Man_t * pAig, int nPref, int nFrames, int nWordsFrame ); +extern void Ssw_SmlStop( Ssw_Sml_t * p ); +extern Ssw_Sml_t * Ssw_SmlSimulateSeq( Aig_Man_t * pAig, int nPref, int nFrames, int nWords ); +extern unsigned Ssw_SmlNodeHash( Ssw_Sml_t * p, Aig_Obj_t * pObj ); +extern int Ssw_SmlNodeIsConst( Ssw_Sml_t * p, Aig_Obj_t * pObj ); +extern int Ssw_SmlNodesAreEqual( Ssw_Sml_t * p, Aig_Obj_t * pObj0, Aig_Obj_t * pObj1 ); +extern void Ssw_SmlAssignDist1Plus( Ssw_Sml_t * p, unsigned * pPat ); +extern void Ssw_SmlSimulateOne( Ssw_Sml_t * p ); /*=== sswSimSat.c ===================================================*/ extern void Ssw_ManResimulateCex( Ssw_Man_t * p, Aig_Obj_t * pObj, Aig_Obj_t * pRepr, int f ); extern void Ssw_ManResimulateCexTotal( Ssw_Man_t * p, Aig_Obj_t * pObj, Aig_Obj_t * pRepr, int f ); +extern void Ssw_ManResimulateCexTotalSim( Ssw_Man_t * p, Aig_Obj_t * pCand, Aig_Obj_t * pRepr, int f ); /*=== sswSweep.c ===================================================*/ extern int Ssw_ManSweepBmc( Ssw_Man_t * p ); extern int Ssw_ManSweep( Ssw_Man_t * p ); diff --git a/src/aig/ssw/sswMan.c b/src/aig/ssw/sswMan.c index 0b935daa..a6e02125 100644 --- a/src/aig/ssw/sswMan.c +++ b/src/aig/ssw/sswMan.c @@ -49,18 +49,18 @@ Ssw_Man_t * Ssw_ManCreate( Aig_Man_t * pAig, Ssw_Pars_t * pPars ) // create interpolation manager p = ALLOC( Ssw_Man_t, 1 ); memset( p, 0, sizeof(Ssw_Man_t) ); - p->pPars = pPars; - p->pAig = pAig; - p->nFrames = pPars->nFramesK + 1; - p->pNodeToFraig = CALLOC( Aig_Obj_t *, Aig_ManObjNumMax(p->pAig) * p->nFrames ); + p->pPars = pPars; + p->pAig = pAig; + p->nFrames = pPars->nFramesK + 1; + p->pNodeToFraig = CALLOC( Aig_Obj_t *, Aig_ManObjNumMax(p->pAig) * p->nFrames ); // SAT solving - p->nSatVars = 1; - p->pSatVars = CALLOC( int, Aig_ManObjNumMax(p->pAig) * p->nFrames ); - p->vFanins = Vec_PtrAlloc( 100 ); - p->vSimRoots = Vec_PtrAlloc( 1000 ); - p->vSimClasses = Vec_PtrAlloc( 1000 ); - // equivalences proved -// p->pReprsProved = CALLOC( Aig_Obj_t *, Aig_ManObjNumMax(p->pAig) ); + p->pSatVars = CALLOC( int, Aig_ManObjNumMax(p->pAig) * p->nFrames ); + p->vFanins = Vec_PtrAlloc( 100 ); + p->vSimRoots = Vec_PtrAlloc( 1000 ); + p->vSimClasses = Vec_PtrAlloc( 1000 ); + // allocate storage for sim pattern + p->nPatWords = Aig_BitWordNum( Saig_ManPiNum(pAig) * p->nFrames + Saig_ManRegNum(pAig) ); + p->pPatWords = ALLOC( unsigned, p->nPatWords ); return p; } @@ -80,7 +80,6 @@ int Ssw_ManCountEquivs( Ssw_Man_t * p ) Aig_Obj_t * pObj; int i, nEquivs = 0; Aig_ManForEachObj( p->pAig, pObj, i ) -// nEquivs += ( p->pReprsProved[i] != NULL ); nEquivs += ( Aig_ObjRepr(p->pAig, pObj) != NULL ); return nEquivs; } @@ -98,14 +97,19 @@ int Ssw_ManCountEquivs( Ssw_Man_t * p ) ***********************************************************************/ void Ssw_ManPrintStats( Ssw_Man_t * p ) { - printf( "Parameters: Frames = %d. Conf limit = %d. Constrs = %d.\n", - p->pPars->nFramesK, p->pPars->nBTLimit, p->pPars->nConstrs ); - printf( "AIG : PI = %d. PO = %d. Latch = %d. Node = %d. SAT vars = %d.\n", - Saig_ManPiNum(p->pAig), Saig_ManPoNum(p->pAig), Saig_ManRegNum(p->pAig), Aig_ManNodeNum(p->pAig), p->nSatVars ); - printf( "SAT calls : All = %6d. Unsat = %6d. Sat = %6d. Fail = %6d. Equivs = %d. Str = %d.\n", - p->nSatCalls, p->nSatCalls-p->nSatCallsSat-p->nSatFailsReal, - p->nSatCallsSat, p->nSatFailsReal, Ssw_ManCountEquivs(p), p->nStragers ); - printf( "Runtime statistics:\n" ); + double nMemory = 1.0*Aig_ManObjNumMax(p->pAig)*p->nFrames*(2*sizeof(int)+2*sizeof(void*))/(1<<20); + + printf( "Parameters: Frames = %d. Conf limit = %d. Constrs = %d. Max lev = %d. Mem = %0.2f Mb.\n", + p->pPars->nFramesK, p->pPars->nBTLimit, p->pPars->nConstrs, p->pPars->nMaxLevs, nMemory ); + printf( "AIG : PI = %d. PO = %d. Latch = %d. Node = %d. Ave SAT vars = %d.\n", + Saig_ManPiNum(p->pAig), Saig_ManPoNum(p->pAig), Saig_ManRegNum(p->pAig), Aig_ManNodeNum(p->pAig), + p->nSatVarsTotal/p->pPars->nIters ); + printf( "SAT calls : Proof = %d. Cex = %d. Fail = %d. FailReal = %d. Equivs = %d. Str = %d.\n", + p->nSatProof, p->nSatCallsSat, p->nSatFails, p->nSatFailsReal, Ssw_ManCountEquivs(p), p->nStrangers ); + 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->nNodesBeg:1), + p->nRegsBeg, p->nRegsEnd, 100.0*(p->nRegsBeg-p->nRegsEnd)/(p->nRegsBeg?p->nRegsBeg:1) ); + p->timeOther = p->timeTotal-p->timeBmc-p->timeReduce-p->timeSimSat-p->timeSat; PRTP( "BMC ", p->timeBmc, p->timeTotal ); PRTP( "Spec reduce", p->timeReduce, p->timeTotal ); @@ -140,9 +144,10 @@ void Ssw_ManCleanup( Ssw_Man_t * p ) } if ( p->pSat ) { +// printf( "Vars = %d. Clauses = %d. Learnts = %d.\n", p->pSat->size, p->pSat->clauses.size, p->pSat->learnts.size ); + p->nSatVarsTotal += p->pSat->size; sat_solver_delete( p->pSat ); p->pSat = NULL; -// p->nSatVars = 0; memset( p->pSatVars, 0, sizeof(int) * Aig_ManObjNumMax(p->pAig) * p->nFrames ); } p->nConstrTotal = 0; @@ -166,12 +171,14 @@ void Ssw_ManStop( Ssw_Man_t * p ) Ssw_ManPrintStats( p ); if ( p->ppClasses ) Ssw_ClassesStop( p->ppClasses ); + if ( p->pSml ) + Ssw_SmlStop( p->pSml ); Vec_PtrFree( p->vFanins ); Vec_PtrFree( p->vSimRoots ); Vec_PtrFree( p->vSimClasses ); FREE( p->pNodeToFraig ); -// FREE( p->pReprsProved ); FREE( p->pSatVars ); + FREE( p->pPatWords ); free( p ); } @@ -191,7 +198,7 @@ void Ssw_ManStartSolver( Ssw_Man_t * p ) int Lit; assert( p->pSat == NULL ); p->pSat = sat_solver_new(); - sat_solver_setnvars( p->pSat, 10000 ); + sat_solver_setnvars( p->pSat, 1000 ); // var 0 is not used // var 1 is reserved for const1 node - add the clause p->nSatVars = 1; diff --git a/src/aig/ssw/sswSat.c b/src/aig/ssw/sswSat.c index 90752baa..264b39d1 100644 --- a/src/aig/ssw/sswSat.c +++ b/src/aig/ssw/sswSat.c @@ -68,8 +68,11 @@ int Ssw_NodesAreEquiv( Ssw_Man_t * p, Aig_Obj_t * pOld, Aig_Obj_t * pNew ) } //Sat_SolverWriteDimacs( p->pSat, "temp.cnf", pLits, pLits + 2, 1 ); - RetValue = sat_solver_simplify(p->pSat); - assert( RetValue != 0 ); + if ( p->pSat->qtail != p->pSat->qhead ) + { + RetValue = sat_solver_simplify(p->pSat); + assert( RetValue != 0 ); + } clk = clock(); RetValue1 = sat_solver_solve( p->pSat, pLits, pLits + 2, @@ -114,8 +117,11 @@ p->timeSatUndec += clock() - clk; if ( pNew->fPhase ) pLits[1] = lit_neg( pLits[1] ); } - RetValue = sat_solver_simplify(p->pSat); - assert( RetValue != 0 ); + if ( p->pSat->qtail != p->pSat->qhead ) + { + RetValue = sat_solver_simplify(p->pSat); + assert( RetValue != 0 ); + } clk = clock(); RetValue1 = sat_solver_solve( p->pSat, pLits, pLits + 2, diff --git a/src/aig/ssw/sswSim.c b/src/aig/ssw/sswSim.c new file mode 100644 index 00000000..64175b40 --- /dev/null +++ b/src/aig/ssw/sswSim.c @@ -0,0 +1,1263 @@ +/**CFile**************************************************************** + + FileName [sswSim.c] + + SystemName [ABC: Logic synthesis and verification system.] + + PackageName [Inductive prover with constraints.] + + Synopsis [Sequential simulator used by the inductive prover.] + + Author [Alan Mishchenko] + + Affiliation [UC Berkeley] + + Date [Ver. 1.0. Started - September 1, 2008.] + + Revision [$Id: sswSim.c,v 1.00 2008/09/01 00:00:00 alanmi Exp $] + +***********************************************************************/ + +#include "sswInt.h" + +//////////////////////////////////////////////////////////////////////// +/// DECLARATIONS /// +//////////////////////////////////////////////////////////////////////// + +// simulation manager +struct Ssw_Sml_t_ +{ + Aig_Man_t * pAig; // the original AIG manager + int nPref; // the number of timeframes in the prefix + int nFrames; // the number of timeframes + int nWordsFrame; // the number of words in each timeframe + int nWordsTotal; // the total number of words at a node + int nWordsPref; // the number of word in the prefix + int fNonConstOut; // have seen a non-const-0 output during simulation + int nSimRounds; // statistics + int timeSim; // statistics + unsigned pData[0]; // simulation data for the nodes +}; + +static inline unsigned * Ssw_ObjSim( Ssw_Sml_t * p, int Id ) { return p->pData + p->nWordsTotal * Id; } +static inline unsigned Ssw_ObjRandomSim() { return Aig_ManRandom(0); } + +//////////////////////////////////////////////////////////////////////// +/// FUNCTION DEFINITIONS /// +//////////////////////////////////////////////////////////////////////// + +/**Function************************************************************* + + Synopsis [Computes hash value of the node using its simulation info.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +unsigned Ssw_SmlNodeHash( Ssw_Sml_t * p, Aig_Obj_t * pObj ) +{ + static int s_SPrimes[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->nWordsTotal <= 128 ); + uHash = 0; + pSims = Ssw_ObjSim(p, pObj->Id); + for ( i = p->nWordsPref; i < p->nWordsTotal; i++ ) + uHash ^= pSims[i] * s_SPrimes[i & 0x7F]; + return uHash; +} + +/**Function************************************************************* + + Synopsis [Returns 1 if simulation info is composed of all zeros.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Ssw_SmlNodeIsConst( Ssw_Sml_t * p, Aig_Obj_t * pObj ) +{ + unsigned * pSims; + int i; + pSims = Ssw_ObjSim(p, pObj->Id); + for ( i = p->nWordsPref; i < p->nWordsTotal; i++ ) + if ( pSims[i] ) + return 0; + return 1; +} + +/**Function************************************************************* + + Synopsis [Returns 1 if simulation infos are equal.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Ssw_SmlNodesAreEqual( Ssw_Sml_t * p, Aig_Obj_t * pObj0, Aig_Obj_t * pObj1 ) +{ + unsigned * pSims0, * pSims1; + int i; + pSims0 = Ssw_ObjSim(p, pObj0->Id); + pSims1 = Ssw_ObjSim(p, pObj1->Id); + for ( i = p->nWordsPref; i < p->nWordsTotal; i++ ) + if ( pSims0[i] != pSims1[i] ) + return 0; + return 1; +} + +/**Function************************************************************* + + Synopsis [Counts the number of 1s in the XOR of simulation data.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Ssw_SmlNodeNotEquWeight( Ssw_Sml_t * p, int Left, int Right ) +{ + unsigned * pSimL, * pSimR; + int k, Counter = 0; + pSimL = Ssw_ObjSim( p, Left ); + pSimR = Ssw_ObjSim( p, Right ); + for ( k = p->nWordsPref; k < p->nWordsTotal; k++ ) + Counter += Aig_WordCountOnes( pSimL[k] ^ pSimR[k] ); + return Counter; +} + +/**Function************************************************************* + + Synopsis [Returns 1 if simulation info is composed of all zeros.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Ssw_SmlNodeIsZero( Ssw_Sml_t * p, Aig_Obj_t * pObj ) +{ + unsigned * pSims; + int i; + pSims = Ssw_ObjSim(p, pObj->Id); + for ( i = p->nWordsPref; i < p->nWordsTotal; i++ ) + if ( pSims[i] ) + return 0; + return 1; +} + +/**Function************************************************************* + + Synopsis [Counts the number of one's in the patten of the output.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Ssw_SmlNodeCountOnes( Ssw_Sml_t * p, Aig_Obj_t * pObj ) +{ + unsigned * pSims; + int i, Counter = 0; + pSims = Ssw_ObjSim(p, pObj->Id); + for ( i = 0; i < p->nWordsTotal; i++ ) + Counter += Aig_WordCountOnes( pSims[i] ); + return Counter; +} + + + +/**Function************************************************************* + + Synopsis [Generated const 0 pattern.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Ssw_SmlSavePattern0( Ssw_Man_t * p, int fInit ) +{ + memset( p->pPatWords, 0, sizeof(unsigned) * p->nPatWords ); +} + +/**Function************************************************************* + + Synopsis [[Generated const 1 pattern.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Ssw_SmlSavePattern1( Ssw_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 = Saig_ManPiNum(p->pAig); + k = 0; + Saig_ManForEachLo( p->pAig, pObj, i ) + Aig_InfoXorBit( p->pPatWords, nTruePis * p->nFrames + k++ ); +} + +/**Function************************************************************* + + Synopsis [Copy pattern from the solver into the internal storage.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Ssw_SmlSavePattern( Ssw_Man_t * p ) +{ + Aig_Obj_t * pObj; + int i; + memset( p->pPatWords, 0, sizeof(unsigned) * p->nPatWords ); + Aig_ManForEachPi( p->pFrames, pObj, i ) + if ( p->pSat->model.ptr[Ssw_ObjSatNum(p, pObj)] == l_True ) + Aig_InfoSetBit( p->pPatWords, i ); +/* + if ( p->vCex ) + { + Vec_IntClear( p->vCex ); + for ( i = 0; i < Saig_ManPiNum(p->pAig); i++ ) + Vec_IntPush( p->vCex, Aig_InfoHasBit( p->pPatWords, i ) ); + for ( i = Saig_ManPiNum(p->pFrames); i < Aig_ManPiNum(p->pFrames); i++ ) + Vec_IntPush( p->vCex, Aig_InfoHasBit( p->pPatWords, i ) ); + } +*/ + +/* + printf( "Pattern: " ); + Aig_ManForEachPi( p->pFrames, pObj, i ) + printf( "%d", Aig_InfoHasBit( p->pPatWords, i ) ); + printf( "\n" ); +*/ +} + + + +/**Function************************************************************* + + Synopsis [Creates the counter-example from the successful pattern.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int * Ssw_SmlCheckOutputSavePattern( Ssw_Sml_t * p, Aig_Obj_t * pObjPo ) +{ + Aig_Obj_t * pFanin, * pObjPi; + unsigned * pSims; + int i, k, BestPat, * pModel; + // find the word of the pattern + pFanin = Aig_ObjFanin0(pObjPo); + pSims = Ssw_ObjSim(p, pFanin->Id); + for ( i = 0; i < p->nWordsTotal; i++ ) + if ( pSims[i] ) + break; + assert( i < p->nWordsTotal ); + // find the bit of the pattern + for ( k = 0; k < 32; k++ ) + if ( pSims[i] & (1 << k) ) + break; + assert( k < 32 ); + // determine the best pattern + BestPat = i * 32 + k; + // fill in the counter-example data + pModel = ALLOC( int, Aig_ManPiNum(p->pAig)+1 ); + Aig_ManForEachPi( p->pAig, pObjPi, i ) + { + pModel[i] = Aig_InfoHasBit(Ssw_ObjSim(p, pObjPi->Id), BestPat); +// printf( "%d", pModel[i] ); + } + pModel[Aig_ManPiNum(p->pAig)] = pObjPo->Id; +// printf( "\n" ); + return pModel; +} + +/**Function************************************************************* + + Synopsis [Returns 1 if the one of the output is already non-constant 0.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int * Ssw_SmlCheckOutput( Ssw_Sml_t * p ) +{ + Aig_Obj_t * pObj; + int i; + // make sure the reference simulation pattern does not detect the bug + pObj = Aig_ManPo( p->pAig, 0 ); + assert( Aig_ObjFanin0(pObj)->fPhase == (unsigned)Aig_ObjFaninC0(pObj) ); + Aig_ManForEachPo( p->pAig, pObj, i ) + { + if ( !Ssw_SmlNodeIsConst( p, Aig_ObjFanin0(pObj) ) ) + { + // create the counter-example from this pattern + return Ssw_SmlCheckOutputSavePattern( p, pObj ); + } + } + return NULL; +} + + + +/**Function************************************************************* + + Synopsis [Assigns random patterns to the PI node.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Ssw_SmlAssignRandom( Ssw_Sml_t * p, Aig_Obj_t * pObj ) +{ + unsigned * pSims; + int i; + assert( Aig_ObjIsPi(pObj) ); + pSims = Ssw_ObjSim( p, pObj->Id ); + for ( i = 0; i < p->nWordsTotal; i++ ) + pSims[i] = Ssw_ObjRandomSim(); +} + +/**Function************************************************************* + + Synopsis [Assigns random patterns to the PI node.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Ssw_SmlAssignRandomFrame( Ssw_Sml_t * p, Aig_Obj_t * pObj, int iFrame ) +{ + unsigned * pSims; + int i; + assert( Aig_ObjIsPi(pObj) ); + pSims = Ssw_ObjSim( p, pObj->Id ) + p->nWordsFrame * iFrame; + for ( i = 0; i < p->nWordsFrame; i++ ) + pSims[i] = Ssw_ObjRandomSim(); +} + +/**Function************************************************************* + + Synopsis [Assigns constant patterns to the PI node.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Ssw_SmlAssignConst( Ssw_Sml_t * p, Aig_Obj_t * pObj, int fConst1, int iFrame ) +{ + unsigned * pSims; + int i; + assert( Aig_ObjIsPi(pObj) ); + pSims = Ssw_ObjSim( p, pObj->Id ) + p->nWordsFrame * iFrame; + for ( i = 0; i < p->nWordsFrame; i++ ) + pSims[i] = fConst1? ~(unsigned)0 : 0; +} + +/**Function************************************************************* + + Synopsis [Assings random simulation info for the PIs.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Ssw_SmlInitialize( Ssw_Sml_t * p, int fInit ) +{ + Aig_Obj_t * pObj; + int i; + if ( fInit ) + { + assert( Aig_ManRegNum(p->pAig) > 0 ); + assert( Aig_ManRegNum(p->pAig) < Aig_ManPiNum(p->pAig) ); + // assign random info for primary inputs + Saig_ManForEachPi( p->pAig, pObj, i ) + Ssw_SmlAssignRandom( p, pObj ); + // assign the initial state for the latches + Saig_ManForEachLo( p->pAig, pObj, i ) + Ssw_SmlAssignConst( p, pObj, 0, 0 ); + } + else + { + Aig_ManForEachPi( p->pAig, pObj, i ) + Ssw_SmlAssignRandom( p, pObj ); + } +} + +/**Function************************************************************* + + Synopsis [Assings distance-1 simulation info for the PIs.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Ssw_SmlAssignDist1( Ssw_Sml_t * p, unsigned * pPat ) +{ + Aig_Obj_t * pObj; + int f, i, k, Limit, nTruePis; + assert( p->nFrames > 0 ); + if ( p->nFrames == 1 ) + { + // copy the PI info + Aig_ManForEachPi( p->pAig, pObj, i ) + Ssw_SmlAssignConst( p, pObj, Aig_InfoHasBit(pPat, i), 0 ); + // flip one bit + Limit = AIG_MIN( Aig_ManPiNum(p->pAig), p->nWordsTotal * 32 - 1 ); + for ( i = 0; i < Limit; i++ ) + Aig_InfoXorBit( Ssw_ObjSim( p, Aig_ManPi(p->pAig,i)->Id ), i+1 ); + } + 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++ ) + Saig_ManForEachPi( p->pAig, pObj, i ) + Ssw_SmlAssignConst( p, pObj, Aig_InfoHasBit(pPat, nTruePis * f + i), f ); + // copy the latch info + k = 0; + Saig_ManForEachLo( p->pAig, pObj, i ) + Ssw_SmlAssignConst( p, pObj, Aig_InfoHasBit(pPat, nTruePis * p->nFrames + k++), 0 ); +// assert( p->pFrames == NULL || nTruePis * p->nFrames + k == Aig_ManPiNum(p->pFrames) ); + + // flip one bit of the last frame + if ( fUseDist1 ) //&& p->nFrames == 2 ) + { + Limit = AIG_MIN( nTruePis, p->nWordsFrame * 32 - 1 ); + for ( i = 0; i < Limit; i++ ) + Aig_InfoXorBit( Ssw_ObjSim( p, Aig_ManPi(p->pAig, i)->Id ) + p->nWordsFrame*(p->nFrames-1), i+1 ); + } + } +} + +/**Function************************************************************* + + Synopsis [Assings distance-1 simulation info for the PIs.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Ssw_SmlAssignDist1Plus( Ssw_Sml_t * p, unsigned * pPat ) +{ + Aig_Obj_t * pObj; + int f, i, Limit; + assert( p->nFrames > 0 ); + + // copy the pattern into the primary inputs + Aig_ManForEachPi( p->pAig, pObj, i ) + Ssw_SmlAssignConst( p, pObj, Aig_InfoHasBit(pPat, i), 0 ); + + // set distance one PIs for the first frame + Limit = AIG_MIN( Saig_ManPiNum(p->pAig), p->nWordsFrame * 32 - 1 ); + for ( i = 0; i < Limit; i++ ) + Aig_InfoXorBit( Ssw_ObjSim( p, Aig_ManPi(p->pAig, i)->Id ), i+1 ); + + // create random info for the remaining timeframes + for ( f = 1; f < p->nFrames; f++ ) + Saig_ManForEachPi( p->pAig, pObj, i ) + Ssw_SmlAssignRandomFrame( p, pObj, f ); +} + + +/**Function************************************************************* + + Synopsis [Simulates one node.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Ssw_SmlNodeSimulate( Ssw_Sml_t * p, Aig_Obj_t * pObj, int iFrame ) +{ + unsigned * pSims, * pSims0, * pSims1; + int fCompl, fCompl0, fCompl1, i; + assert( !Aig_IsComplement(pObj) ); + assert( Aig_ObjIsNode(pObj) ); + assert( iFrame == 0 || p->nWordsFrame < p->nWordsTotal ); + // get hold of the simulation information + pSims = Ssw_ObjSim(p, pObj->Id) + p->nWordsFrame * iFrame; + pSims0 = Ssw_ObjSim(p, Aig_ObjFanin0(pObj)->Id) + p->nWordsFrame * iFrame; + pSims1 = Ssw_ObjSim(p, Aig_ObjFanin1(pObj)->Id) + p->nWordsFrame * iFrame; + // get complemented attributes of the children using their random info + fCompl = pObj->fPhase; + fCompl0 = Aig_ObjPhaseReal(Aig_ObjChild0(pObj)); + fCompl1 = Aig_ObjPhaseReal(Aig_ObjChild1(pObj)); + // simulate + if ( fCompl0 && fCompl1 ) + { + if ( fCompl ) + for ( i = 0; i < p->nWordsFrame; i++ ) + pSims[i] = (pSims0[i] | pSims1[i]); + else + for ( i = 0; i < p->nWordsFrame; i++ ) + pSims[i] = ~(pSims0[i] | pSims1[i]); + } + else if ( fCompl0 && !fCompl1 ) + { + if ( fCompl ) + for ( i = 0; i < p->nWordsFrame; i++ ) + pSims[i] = (pSims0[i] | ~pSims1[i]); + else + for ( i = 0; i < p->nWordsFrame; i++ ) + pSims[i] = (~pSims0[i] & pSims1[i]); + } + else if ( !fCompl0 && fCompl1 ) + { + if ( fCompl ) + for ( i = 0; i < p->nWordsFrame; i++ ) + pSims[i] = (~pSims0[i] | pSims1[i]); + else + for ( i = 0; i < p->nWordsFrame; i++ ) + pSims[i] = (pSims0[i] & ~pSims1[i]); + } + else // if ( !fCompl0 && !fCompl1 ) + { + if ( fCompl ) + for ( i = 0; i < p->nWordsFrame; i++ ) + pSims[i] = ~(pSims0[i] & pSims1[i]); + else + for ( i = 0; i < p->nWordsFrame; i++ ) + pSims[i] = (pSims0[i] & pSims1[i]); + } +} + +/**Function************************************************************* + + Synopsis [Simulates one node.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Ssw_SmlNodesCompareInFrame( Ssw_Sml_t * p, Aig_Obj_t * pObj0, Aig_Obj_t * pObj1, int iFrame0, int iFrame1 ) +{ + unsigned * pSims0, * pSims1; + int i; + assert( !Aig_IsComplement(pObj0) ); + assert( !Aig_IsComplement(pObj1) ); + assert( iFrame0 == 0 || p->nWordsFrame < p->nWordsTotal ); + assert( iFrame1 == 0 || p->nWordsFrame < p->nWordsTotal ); + // get hold of the simulation information + pSims0 = Ssw_ObjSim(p, pObj0->Id) + p->nWordsFrame * iFrame0; + pSims1 = Ssw_ObjSim(p, pObj1->Id) + p->nWordsFrame * iFrame1; + // compare + for ( i = 0; i < p->nWordsFrame; i++ ) + if ( pSims0[i] != pSims1[i] ) + return 0; + return 1; +} + +/**Function************************************************************* + + Synopsis [Simulates one node.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Ssw_SmlNodeCopyFanin( Ssw_Sml_t * p, Aig_Obj_t * pObj, int iFrame ) +{ + unsigned * pSims, * pSims0; + int fCompl, fCompl0, i; + assert( !Aig_IsComplement(pObj) ); + assert( Aig_ObjIsPo(pObj) ); + assert( iFrame == 0 || p->nWordsFrame < p->nWordsTotal ); + // get hold of the simulation information + pSims = Ssw_ObjSim(p, pObj->Id) + p->nWordsFrame * iFrame; + pSims0 = Ssw_ObjSim(p, Aig_ObjFanin0(pObj)->Id) + p->nWordsFrame * iFrame; + // get complemented attributes of the children using their random info + fCompl = pObj->fPhase; + fCompl0 = Aig_ObjPhaseReal(Aig_ObjChild0(pObj)); + // copy information as it is + if ( fCompl0 ) + for ( i = 0; i < p->nWordsFrame; i++ ) + pSims[i] = ~pSims0[i]; + else + for ( i = 0; i < p->nWordsFrame; i++ ) + pSims[i] = pSims0[i]; +} + +/**Function************************************************************* + + Synopsis [Simulates one node.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Ssw_SmlNodeTransferNext( Ssw_Sml_t * p, Aig_Obj_t * pOut, Aig_Obj_t * pIn, int iFrame ) +{ + unsigned * pSims0, * pSims1; + int i; + assert( !Aig_IsComplement(pOut) ); + assert( !Aig_IsComplement(pIn) ); + assert( Aig_ObjIsPo(pOut) ); + assert( Aig_ObjIsPi(pIn) ); + assert( iFrame == 0 || p->nWordsFrame < p->nWordsTotal ); + // get hold of the simulation information + pSims0 = Ssw_ObjSim(p, pOut->Id) + p->nWordsFrame * iFrame; + pSims1 = Ssw_ObjSim(p, pIn->Id) + p->nWordsFrame * (iFrame+1); + // copy information as it is + for ( i = 0; i < p->nWordsFrame; i++ ) + pSims1[i] = pSims0[i]; +} + + +/**Function************************************************************* + + Synopsis [Check if any of the POs becomes non-constant.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Ssw_SmlCheckNonConstOutputs( Ssw_Sml_t * p ) +{ + Aig_Obj_t * pObj; + int i; + Saig_ManForEachPo( p->pAig, pObj, i ) + if ( !Ssw_SmlNodeIsZero(p, pObj) ) + return 1; + return 0; +} + +/**Function************************************************************* + + Synopsis [Simulates AIG manager.] + + Description [Assumes that the PI simulation info is attached.] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Ssw_SmlSimulateOne( Ssw_Sml_t * p ) +{ + Aig_Obj_t * pObj, * pObjLi, * pObjLo; + int f, i, clk; +clk = clock(); + for ( f = 0; f < p->nFrames; f++ ) + { + // simulate the nodes + Aig_ManForEachNode( p->pAig, pObj, i ) + Ssw_SmlNodeSimulate( p, pObj, f ); + // copy simulation info into outputs + Saig_ManForEachPo( p->pAig, pObj, i ) + Ssw_SmlNodeCopyFanin( p, pObj, f ); + // quit if this is the last timeframe + if ( f == p->nFrames - 1 ) + break; + // copy simulation info into outputs + Saig_ManForEachLi( p->pAig, pObj, i ) + Ssw_SmlNodeCopyFanin( p, pObj, f ); + // copy simulation info into the inputs + Saig_ManForEachLiLo( p->pAig, pObjLi, pObjLo, i ) + Ssw_SmlNodeTransferNext( p, pObjLi, pObjLo, f ); + } +p->timeSim += clock() - clk; +p->nSimRounds++; +} + + +#if 0 + +/**Function************************************************************* + + Synopsis [Resimulates fraiging manager after finding a counter-example.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Ssw_SmlResimulate( Ssw_Man_t * p ) +{ + int nChanges, clk; + Ssw_SmlAssignDist1( p, p->pPatWords ); + Ssw_SmlSimulateOne( p ); +// if ( p->pPars->fPatScores ) +// Ssw_CleanPatScores( p ); + if ( p->pPars->fProve && Ssw_SmlCheckOutput(p) ) + return; +clk = clock(); + nChanges = Ssw_ClassesRefine( p->pCla, 1 ); + nChanges += Ssw_ClassesRefine1( p->pCla, 1, NULL ); + if ( p->pCla->vImps ) + nChanges += Ssw_ImpRefineUsingCex( p, p->pCla->vImps ); + if ( p->vOneHots ) + nChanges += Ssw_OneHotRefineUsingCex( p, p->vOneHots ); +p->timeRef += clock() - clk; + if ( !p->pPars->nFramesK && nChanges < 1 ) + printf( "Error: A counter-example did not refine classes!\n" ); +// assert( nChanges >= 1 ); +//printf( "Refined classes = %5d. Changes = %4d.\n", Vec_PtrSize(p->vClasses), nChanges ); +} + +/**Function************************************************************* + + Synopsis [Performs simulation of the manager.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Ssw_SmlSimulate( Ssw_Man_t * p, int fInit ) +{ + int fVerbose = 0; + int nChanges, nClasses, clk; + assert( !fInit || Aig_ManRegNum(p->pAig) ); + // start the classes + Ssw_SmlInitialize( p, fInit ); + Ssw_SmlSimulateOne( p ); + if ( p->pPars->fProve && Ssw_SmlCheckOutput(p) ) + return; + Ssw_ClassesPrepare( p->pCla, p->pPars->fLatchCorr, 0 ); +// Ssw_ClassesPrint( p->pCla, 0 ); +if ( fVerbose ) +printf( "Starting classes = %5d. Lits = %6d.\n", Vec_PtrSize(p->pCla->vClasses), Ssw_ClassesCountLits(p->pCla) ); + +//return; + + // refine classes by walking 0/1 patterns + Ssw_SmlSavePattern0( p, fInit ); + Ssw_SmlAssignDist1( p, p->pPatWords ); + Ssw_SmlSimulateOne( p ); + if ( p->pPars->fProve && Ssw_SmlCheckOutput(p) ) + return; +clk = clock(); + nChanges = Ssw_ClassesRefine( p->pCla, 1 ); + nChanges += Ssw_ClassesRefine1( p->pCla, 1, NULL ); +p->timeRef += clock() - clk; +if ( fVerbose ) +printf( "Refined classes = %5d. Changes = %4d. Lits = %6d.\n", Vec_PtrSize(p->pCla->vClasses), nChanges, Ssw_ClassesCountLits(p->pCla) ); + Ssw_SmlSavePattern1( p, fInit ); + Ssw_SmlAssignDist1( p, p->pPatWords ); + Ssw_SmlSimulateOne( p ); + if ( p->pPars->fProve && Ssw_SmlCheckOutput(p) ) + return; +clk = clock(); + nChanges = Ssw_ClassesRefine( p->pCla, 1 ); + nChanges += Ssw_ClassesRefine1( p->pCla, 1, NULL ); +p->timeRef += clock() - clk; + +if ( fVerbose ) +printf( "Refined classes = %5d. Changes = %4d. Lits = %6d.\n", Vec_PtrSize(p->pCla->vClasses), nChanges, Ssw_ClassesCountLits(p->pCla) ); + // refine classes by random simulation + do { + Ssw_SmlInitialize( p, fInit ); + Ssw_SmlSimulateOne( p ); + nClasses = Vec_PtrSize(p->pCla->vClasses); + if ( p->pPars->fProve && Ssw_SmlCheckOutput(p) ) + return; +clk = clock(); + nChanges = Ssw_ClassesRefine( p->pCla, 1 ); + nChanges += Ssw_ClassesRefine1( p->pCla, 1, NULL ); +p->timeRef += clock() - clk; +if ( fVerbose ) +printf( "Refined classes = %5d. Changes = %4d. Lits = %6d.\n", Vec_PtrSize(p->pCla->vClasses), nChanges, Ssw_ClassesCountLits(p->pCla) ); + } while ( (double)nChanges / nClasses > p->pPars->dSimSatur ); + +// if ( p->pPars->fVerbose ) +// printf( "Consts = %6d. Classes = %6d. Literals = %6d.\n", +// Vec_PtrSize(p->pCla->vClasses1), Vec_PtrSize(p->pCla->vClasses), Ssw_ClassesCountLits(p->pCla) ); +// Ssw_ClassesPrint( p->pCla, 0 ); +} + +#endif + +/**Function************************************************************* + + Synopsis [Allocates simulation manager.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Ssw_Sml_t * Ssw_SmlStart( Aig_Man_t * pAig, int nPref, int nFrames, int nWordsFrame ) +{ + Ssw_Sml_t * p; + p = (Ssw_Sml_t *)malloc( sizeof(Ssw_Sml_t) + sizeof(unsigned) * Aig_ManObjNumMax(pAig) * (nPref + nFrames) * nWordsFrame ); + memset( p, 0, sizeof(Ssw_Sml_t) + sizeof(unsigned) * (nPref + nFrames) * nWordsFrame ); + p->pAig = pAig; + p->nPref = nPref; + p->nFrames = nPref + nFrames; + p->nWordsFrame = nWordsFrame; + p->nWordsTotal = (nPref + nFrames) * nWordsFrame; + p->nWordsPref = nPref * nWordsFrame; + return p; +} + +/**Function************************************************************* + + Synopsis [Deallocates simulation manager.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Ssw_SmlStop( Ssw_Sml_t * p ) +{ + free( p ); +} + + +/**Function************************************************************* + + Synopsis [Performs simulation of the uninitialized circuit.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Ssw_Sml_t * Ssw_SmlSimulateComb( Aig_Man_t * pAig, int nWords ) +{ + Ssw_Sml_t * p; + p = Ssw_SmlStart( pAig, 0, 1, nWords ); + Ssw_SmlInitialize( p, 0 ); + Ssw_SmlSimulateOne( p ); + return p; +} + +/**Function************************************************************* + + Synopsis [Performs simulation of the initialized circuit.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Ssw_Sml_t * Ssw_SmlSimulateSeq( Aig_Man_t * pAig, int nPref, int nFrames, int nWords ) +{ + Ssw_Sml_t * p; + p = Ssw_SmlStart( pAig, nPref, nFrames, nWords ); + Ssw_SmlInitialize( p, 1 ); + Ssw_SmlSimulateOne( p ); + p->fNonConstOut = Ssw_SmlCheckNonConstOutputs( p ); + return p; +} + + + +/**Function************************************************************* + + Synopsis [Allocates a counter-example.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Ssw_Cex_t * Ssw_SmlAllocCounterExample( int nRegs, int nRealPis, int nFrames ) +{ + Ssw_Cex_t * pCex; + int nWords = Aig_BitWordNum( nRegs + nRealPis * nFrames ); + pCex = (Ssw_Cex_t *)malloc( sizeof(Ssw_Cex_t) + sizeof(unsigned) * nWords ); + memset( pCex, 0, sizeof(Ssw_Cex_t) + sizeof(unsigned) * nWords ); + pCex->nRegs = nRegs; + pCex->nPis = nRealPis; + pCex->nBits = nRegs + nRealPis * nFrames; + return pCex; +} + +/**Function************************************************************* + + Synopsis [Frees the counter-example.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Ssw_SmlFreeCounterExample( Ssw_Cex_t * pCex ) +{ + free( pCex ); +} + +/**Function************************************************************* + + Synopsis [Resimulates the counter-example.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Ssw_SmlRunCounterExample( Aig_Man_t * pAig, Ssw_Cex_t * p ) +{ + Ssw_Sml_t * pSml; + Aig_Obj_t * pObj; + int RetValue, i, k, iBit; + assert( Aig_ManRegNum(pAig) > 0 ); + assert( Aig_ManRegNum(pAig) < Aig_ManPiNum(pAig) ); + // start a new sequential simulator + pSml = Ssw_SmlStart( pAig, 0, p->iFrame+1, 1 ); + // assign simulation info for the registers + iBit = 0; + Saig_ManForEachLo( pAig, pObj, i ) + Ssw_SmlAssignConst( pSml, pObj, Aig_InfoHasBit(p->pData, iBit++), 0 ); + // assign simulation info for the primary inputs + for ( i = 0; i <= p->iFrame; i++ ) + Saig_ManForEachPi( pAig, pObj, k ) + Ssw_SmlAssignConst( pSml, pObj, Aig_InfoHasBit(p->pData, iBit++), i ); + assert( iBit == p->nBits ); + // run random simulation + Ssw_SmlSimulateOne( pSml ); + // check if the given output has failed + RetValue = !Ssw_SmlNodeIsZero( pSml, Aig_ManPo(pAig, p->iPo) ); + Ssw_SmlStop( pSml ); + return RetValue; +} + +/**Function************************************************************* + + Synopsis [Creates sequential counter-example from the simulation info.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Ssw_Cex_t * Ssw_SmlGetCounterExample( Ssw_Sml_t * p ) +{ + Ssw_Cex_t * pCex; + Aig_Obj_t * pObj; + unsigned * pSims; + int iPo, iFrame, iBit, i, k; + + // make sure the simulation manager has it + assert( p->fNonConstOut ); + + // find the first output that failed + iPo = -1; + iBit = -1; + iFrame = -1; + Saig_ManForEachPo( p->pAig, pObj, iPo ) + { + if ( Ssw_SmlNodeIsZero(p, pObj) ) + continue; + pSims = Ssw_ObjSim( p, pObj->Id ); + for ( i = p->nWordsPref; i < p->nWordsTotal; i++ ) + if ( pSims[i] ) + { + iFrame = i / p->nWordsFrame; + iBit = 32 * (i % p->nWordsFrame) + Aig_WordFindFirstBit( pSims[i] ); + break; + } + break; + } + assert( iPo < Aig_ManPoNum(p->pAig)-Aig_ManRegNum(p->pAig) ); + assert( iFrame < p->nFrames ); + assert( iBit < 32 * p->nWordsFrame ); + + // allocate the counter example + pCex = Ssw_SmlAllocCounterExample( Aig_ManRegNum(p->pAig), Aig_ManPiNum(p->pAig) - Aig_ManRegNum(p->pAig), iFrame + 1 ); + pCex->iPo = iPo; + pCex->iFrame = iFrame; + + // copy the bit data + Saig_ManForEachLo( p->pAig, pObj, k ) + { + pSims = Ssw_ObjSim( p, pObj->Id ); + if ( Aig_InfoHasBit( pSims, iBit ) ) + Aig_InfoSetBit( pCex->pData, k ); + } + for ( i = 0; i <= iFrame; i++ ) + { + Saig_ManForEachPi( p->pAig, pObj, k ) + { + pSims = Ssw_ObjSim( p, pObj->Id ); + if ( Aig_InfoHasBit( pSims, 32 * p->nWordsFrame * i + iBit ) ) + Aig_InfoSetBit( pCex->pData, pCex->nRegs + pCex->nPis * i + k ); + } + } + // verify the counter example + if ( !Ssw_SmlRunCounterExample( p->pAig, pCex ) ) + { + printf( "Ssw_SmlGetCounterExample(): Counter-example is invalid.\n" ); + Ssw_SmlFreeCounterExample( pCex ); + pCex = NULL; + } + return pCex; +} + +/**Function************************************************************* + + Synopsis [Generates seq counter-example from the combinational one.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Ssw_Cex_t * Ssw_SmlCopyCounterExample( Aig_Man_t * pAig, Aig_Man_t * pFrames, int * pModel ) +{ + Ssw_Cex_t * pCex; + Aig_Obj_t * pObj; + int i, nFrames, nTruePis, nTruePos, iPo, iFrame; + // get the number of frames + assert( Aig_ManRegNum(pAig) > 0 ); + assert( Aig_ManRegNum(pFrames) == 0 ); + nTruePis = Aig_ManPiNum(pAig)-Aig_ManRegNum(pAig); + nTruePos = Aig_ManPoNum(pAig)-Aig_ManRegNum(pAig); + nFrames = Aig_ManPiNum(pFrames) / nTruePis; + assert( nTruePis * nFrames == Aig_ManPiNum(pFrames) ); + assert( nTruePos * nFrames == Aig_ManPoNum(pFrames) ); + // find the PO that failed + iPo = -1; + iFrame = -1; + Aig_ManForEachPo( pFrames, pObj, i ) + if ( pObj->Id == pModel[Aig_ManPiNum(pFrames)] ) + { + iPo = i % nTruePos; + iFrame = i / nTruePos; + break; + } + assert( iPo >= 0 ); + // allocate the counter example + pCex = Ssw_SmlAllocCounterExample( Aig_ManRegNum(pAig), nTruePis, iFrame + 1 ); + pCex->iPo = iPo; + pCex->iFrame = iFrame; + + // copy the bit data + for ( i = 0; i < Aig_ManPiNum(pFrames); i++ ) + { + if ( pModel[i] ) + Aig_InfoSetBit( pCex->pData, pCex->nRegs + i ); + if ( pCex->nRegs + i == pCex->nBits - 1 ) + break; + } + + // verify the counter example + if ( !Ssw_SmlRunCounterExample( pAig, pCex ) ) + { + printf( "Ssw_SmlGetCounterExample(): Counter-example is invalid.\n" ); + Ssw_SmlFreeCounterExample( pCex ); + pCex = NULL; + } + return pCex; + +} + +/**Function************************************************************* + + Synopsis [Make the trivial counter-example for the trivially asserted output.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Ssw_Cex_t * Ssw_SmlTrivCounterExample( Aig_Man_t * pAig, int iFrameOut ) +{ + Ssw_Cex_t * pCex; + int nTruePis, nTruePos, iPo, iFrame; + assert( Aig_ManRegNum(pAig) > 0 ); + nTruePis = Aig_ManPiNum(pAig)-Aig_ManRegNum(pAig); + nTruePos = Aig_ManPoNum(pAig)-Aig_ManRegNum(pAig); + iPo = iFrameOut % nTruePos; + iFrame = iFrameOut / nTruePos; + // allocate the counter example + pCex = Ssw_SmlAllocCounterExample( Aig_ManRegNum(pAig), nTruePis, iFrame + 1 ); + pCex->iPo = iPo; + pCex->iFrame = iFrame; + return pCex; +} + +/**Function************************************************************* + + Synopsis [Resimulates the counter-example.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Ssw_SmlWriteCounterExample( FILE * pFile, Aig_Man_t * pAig, Ssw_Cex_t * p ) +{ + Ssw_Sml_t * pSml; + Aig_Obj_t * pObj; + int RetValue, i, k, iBit; + unsigned * pSims; + assert( Aig_ManRegNum(pAig) > 0 ); + assert( Aig_ManRegNum(pAig) < Aig_ManPiNum(pAig) ); + // start a new sequential simulator + pSml = Ssw_SmlStart( pAig, 0, p->iFrame+1, 1 ); + // assign simulation info for the registers + iBit = 0; + Saig_ManForEachLo( pAig, pObj, i ) +// Ssw_SmlAssignConst( pSml, pObj, Aig_InfoHasBit(p->pData, iBit++), 0 ); + Ssw_SmlAssignConst( pSml, pObj, 0, 0 ); + // assign simulation info for the primary inputs + iBit = p->nRegs; + for ( i = 0; i <= p->iFrame; i++ ) + Saig_ManForEachPi( pAig, pObj, k ) + Ssw_SmlAssignConst( pSml, pObj, Aig_InfoHasBit(p->pData, iBit++), i ); + assert( iBit == p->nBits ); + // run random simulation + Ssw_SmlSimulateOne( pSml ); + // check if the given output has failed + RetValue = !Ssw_SmlNodeIsZero( pSml, Aig_ManPo(pAig, p->iPo) ); + + // write the output file + for ( i = 0; i <= p->iFrame; i++ ) + { +/* + Saig_ManForEachLo( pAig, pObj, k ) + { + pSims = Ssw_ObjSim(pSml, pObj->Id); + fprintf( pFile, "%d", (int)(pSims[i] != 0) ); + } + fprintf( pFile, " " ); +*/ + Saig_ManForEachPi( pAig, pObj, k ) + { + pSims = Ssw_ObjSim(pSml, pObj->Id); + fprintf( pFile, "%d", (int)(pSims[i] != 0) ); + } +/* + fprintf( pFile, " " ); + Saig_ManForEachPo( pAig, pObj, k ) + { + pSims = Ssw_ObjSim(pSml, pObj->Id); + fprintf( pFile, "%d", (int)(pSims[i] != 0) ); + } + fprintf( pFile, " " ); + Saig_ManForEachLi( pAig, pObj, k ) + { + pSims = Ssw_ObjSim(pSml, pObj->Id); + fprintf( pFile, "%d", (int)(pSims[i] != 0) ); + } +*/ + fprintf( pFile, "\n" ); + } + + Ssw_SmlStop( pSml ); + return RetValue; +} + + + +//////////////////////////////////////////////////////////////////////// +/// END OF FILE /// +//////////////////////////////////////////////////////////////////////// + + diff --git a/src/aig/ssw/sswSimSat.c b/src/aig/ssw/sswSimSat.c index 868a016b..547755f0 100644 --- a/src/aig/ssw/sswSimSat.c +++ b/src/aig/ssw/sswSimSat.c @@ -241,7 +241,60 @@ void Ssw_ManResimulateCexTotal( Ssw_Man_t * p, Aig_Obj_t * pCand, Aig_Obj_t * pR & ( Aig_ObjFanin1(pObj)->fMarkB ^ Aig_ObjFaninC1(pObj) ); // check equivalence classes RetValue1 = Ssw_ClassesRefineConst1( p->ppClasses, 0 ); - RetValue2 = Ssw_ClassesRefine( p->ppClasses ); + RetValue2 = Ssw_ClassesRefine( p->ppClasses, 0 ); + // make sure refinement happened + if ( Aig_ObjIsConst1(pRepr) ) + assert( RetValue1 ); + else + assert( RetValue2 ); +p->timeSimSat += clock() - clk; +} + + +/**Function************************************************************* + + Synopsis [Copy pattern from the solver into the internal storage.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Ssw_SmlSavePatternAig( Ssw_Man_t * p, int f ) +{ + Aig_Obj_t * pObj; + int i; + memset( p->pPatWords, 0, sizeof(unsigned) * p->nPatWords ); + Aig_ManForEachPi( p->pAig, pObj, i ) + if ( Ssw_ManOriginalPiValue( p, pObj, f ) ) + Aig_InfoSetBit( p->pPatWords, i ); +} + +/**Function************************************************************* + + Synopsis [Handle the counter-example.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Ssw_ManResimulateCexTotalSim( Ssw_Man_t * p, Aig_Obj_t * pCand, Aig_Obj_t * pRepr, int f ) +{ + int RetValue1, RetValue2, clk = clock(); + // save the counter-example + Ssw_SmlSavePatternAig( p, f ); + // set the PI simulation information + Ssw_SmlAssignDist1Plus( p->pSml, p->pPatWords ); + // simulate internal nodes + Ssw_SmlSimulateOne( p->pSml ); + // check equivalence classes + RetValue1 = Ssw_ClassesRefineConst1( p->ppClasses, 1 ); + RetValue2 = Ssw_ClassesRefine( p->ppClasses, 1 ); // make sure refinement happened if ( Aig_ObjIsConst1(pRepr) ) assert( RetValue1 ); diff --git a/src/aig/ssw/sswSweep.c b/src/aig/ssw/sswSweep.c index 0630de56..7c99fad2 100644 --- a/src/aig/ssw/sswSweep.c +++ b/src/aig/ssw/sswSweep.c @@ -74,16 +74,12 @@ void Ssw_ManSweepNode( Ssw_Man_t * p, Aig_Obj_t * pObj, int f ) p->pSat->model.ptr[iVar] = (int)(p->pPars->fPolarFlip? 0 : (pObj->fPhase? l_True : l_False)); p->pSat->model.size = p->pSat->size; } - p->nStragers++; + p->nStrangers++; return; } // if the fraiged nodes are the same, return if ( Aig_Regular(pObjFraig) == Aig_Regular(pObjReprFraig) ) - { - // remember the proved equivalence -// p->pReprsProved[ pObj->Id ] = pObjRepr; return; - } // assert( Aig_Regular(pObjFraig) != Aig_ManConst1(p->pFrames) ); if ( Aig_Regular(pObjFraig) != Aig_ManConst1(p->pFrames) ) RetValue = Ssw_NodesAreEquiv( p, Aig_Regular(pObjReprFraig), Aig_Regular(pObjFraig) ); @@ -92,7 +88,7 @@ void Ssw_ManSweepNode( Ssw_Man_t * p, Aig_Obj_t * pObj, int f ) if ( RetValue == -1 ) // timed out { - assert( 0 ); +// assert( 0 ); Ssw_ClassesRemoveNode( p->ppClasses, pObj ); p->fRefined = 1; return; @@ -101,13 +97,12 @@ void Ssw_ManSweepNode( Ssw_Man_t * p, Aig_Obj_t * pObj, int f ) { pObjFraig2 = Aig_NotCond( pObjReprFraig, pObj->fPhase ^ pObjRepr->fPhase ); Ssw_ObjSetFraig( p, pObj, f, pObjFraig2 ); - // remember the proved equivalence -// p->pReprsProved[ pObj->Id ] = pObjRepr; return; } // disproved the equivalence // Ssw_ManResimulateCex( p, pObj, pObjRepr, f ); - Ssw_ManResimulateCexTotal( p, pObj, pObjRepr, f ); +// Ssw_ManResimulateCexTotal( p, pObj, pObjRepr, f ); + Ssw_ManResimulateCexTotalSim( p, pObj, pObjRepr, f ); assert( Aig_ObjRepr( p->pAig, pObj ) != pObjRepr ); p->fRefined = 1; } @@ -126,7 +121,7 @@ void Ssw_ManSweepNode( Ssw_Man_t * p, Aig_Obj_t * pObj, int f ) int Ssw_ManSweepBmc( Ssw_Man_t * p ) { Bar_Progress_t * pProgress = NULL; - Aig_Obj_t * pObj, * pObjNew; + Aig_Obj_t * pObj, * pObjNew, * pObjLi, * pObjLo; int i, f, clk; clk = clock(); @@ -154,6 +149,12 @@ clk = clock(); Ssw_ObjSetFraig( p, pObj, f, pObjNew ); Ssw_ManSweepNode( p, pObj, f ); } + // quit if this is the last timeframe + if ( f == p->pPars->nFramesK - 1 ) + break; + // transfer latch input to the latch outputs + Saig_ManForEachLiLo( p->pAig, pObjLi, pObjLo, i ) + Ssw_ObjSetFraig( p, pObjLo, f+1, Ssw_ObjChild0Fra(p, pObjLi,f) ); } if ( p->pPars->fVerbose ) Bar_ProgressStop( pProgress ); @@ -223,7 +224,7 @@ p->timeReduce += clock() - clk; if ( Saig_ObjIsLo(p->pAig, pObj) ) Ssw_ManSweepNode( p, pObj, f ); else if ( Aig_ObjIsNode(pObj) ) - { + { pObjNew = Aig_And( p->pFrames, Ssw_ObjChild0Fra(p, pObj, f), Ssw_ObjChild1Fra(p, pObj, f) ); Ssw_ObjSetFraig( p, pObj, f, pObjNew ); Ssw_ManSweepNode( p, pObj, f ); diff --git a/src/base/abci/abc.c b/src/base/abci/abc.c index 8df6f066..0125ae9e 100644 --- a/src/base/abci/abc.c +++ b/src/base/abci/abc.c @@ -7681,7 +7681,7 @@ int Abc_CommandTest( Abc_Frame_t * pAbc, int argc, char ** argv ) { FILE * pOut, * pErr; Abc_Ntk_t * pNtk; -// Abc_Ntk_t * pNtkRes; + Abc_Ntk_t * pNtkRes; int c; int fBmc; int nFrames; @@ -7700,7 +7700,7 @@ int Abc_CommandTest( Abc_Frame_t * pAbc, int argc, char ** argv ) extern Abc_Ntk_t * Abc_NtkDarToCnf( Abc_Ntk_t * pNtk, char * pFileName ); extern Abc_Ntk_t * Abc_NtkFilter( Abc_Ntk_t * pNtk ); // extern Abc_Ntk_t * Abc_NtkDarRetime( Abc_Ntk_t * pNtk, int nStepsMax, int fVerbose ); -// extern Abc_Ntk_t * Abc_NtkPcmTest( Abc_Ntk_t * pNtk, int fVerbose ); + extern Abc_Ntk_t * Abc_NtkPcmTest( Abc_Ntk_t * pNtk, int fVerbose ); extern Abc_Ntk_t * Abc_NtkDarHaigRecord( Abc_Ntk_t * pNtk, int nIters, int nSteps, int fRetimingOnly, int fAddBugs, int fUseCnf, int fVerbose ); // extern void Abc_NtkDarTestBlif( char * pFileName ); // extern Abc_Ntk_t * Abc_NtkDarPartition( Abc_Ntk_t * pNtk ); @@ -7869,9 +7869,10 @@ int Abc_CommandTest( Abc_Frame_t * pAbc, int argc, char ** argv ) */ -/* + // pNtkRes = Abc_NtkDar( pNtk ); -// pNtkRes = Abc_NtkDarRetime( pNtk, nLevels, 1 ); +// pNtkRes = Abc_NtkDarRetime( pNtk, nLevels, 1 ); +// pNtkRes = Abc_NtkPcmTestAig( pNtk, fVerbose ); pNtkRes = Abc_NtkPcmTest( pNtk, fVerbose ); // pNtkRes = NULL; if ( pNtkRes == NULL ) @@ -7882,7 +7883,7 @@ int Abc_CommandTest( Abc_Frame_t * pAbc, int argc, char ** argv ) // replace the current network Abc_FrameReplaceCurrentNetwork( pAbc, pNtkRes ); return 0; -*/ + // Abc_NtkDarClau( pNtk, nFrames, nLevels, fBmc, fVerbose, fVeryVerbose ); diff --git a/src/base/abci/abcDar.c b/src/base/abci/abcDar.c index a0284a17..c430137c 100644 --- a/src/base/abci/abcDar.c +++ b/src/base/abci/abcDar.c @@ -119,6 +119,7 @@ Aig_Man_t * Abc_NtkToDar( Abc_Ntk_t * pNtk, int fExors, int fRegisters ) Abc_NtkForEachCo( pNtk, pObj, i ) Aig_ObjCreatePo( pMan, (Aig_Obj_t *)Abc_ObjChild0Copy(pObj) ); // complement the 1-valued registers + Aig_ManSetRegNum( pMan, Abc_NtkLatchNum(pNtk) ); if ( fRegisters ) Aig_ManForEachLiSeq( pMan, pObjNew, i ) if ( Abc_LatchIsInit1(Abc_ObjFanout0(Abc_NtkCo(pNtk,i))) ) diff --git a/src/map/mio/mio.c b/src/map/mio/mio.c index e0000c38..37ba82c2 100644 --- a/src/map/mio/mio.c +++ b/src/map/mio/mio.c @@ -206,6 +206,9 @@ int Mio_CommandReadLibrary( Abc_Frame_t * pAbc, int argc, char **argv ) usage: fprintf( pErr, "usage: read_library [-vh]\n"); fprintf( pErr, "\t read the library from a genlib file\n" ); + fprintf( pErr, "\t (if the library contains more than one gate\n" ); + fprintf( pErr, "\t with the same Boolean function, only the first gate\n" ); + fprintf( pErr, "\t in the order of their appearance in the file is used)\n" ); fprintf( pErr, "\t-h : enable verbose output\n"); return 1; /* error exit */ } -- cgit v1.2.3