From 4db86550728b9c5ffeed4a158faf19afd6518b42 Mon Sep 17 00:00:00 2001 From: Alan Mishchenko Date: Wed, 10 Sep 2008 08:01:00 -0700 Subject: Version abc80910 --- src/aig/ssw/module.make | 1 + src/aig/ssw/ssw.h | 5 ++ src/aig/ssw/sswClass.c | 55 +++++++++++++- src/aig/ssw/sswCore.c | 41 +++++++++-- src/aig/ssw/sswInt.h | 10 ++- src/aig/ssw/sswMan.c | 30 ++++---- src/aig/ssw/sswPart.c | 129 ++++++++++++++++++++++++++++++++ src/aig/ssw/sswSimSat.c | 26 +------ src/aig/ssw/sswSweep.c | 191 ++++++++++++++++++++++++++++++++++++------------ 9 files changed, 393 insertions(+), 95 deletions(-) create mode 100644 src/aig/ssw/sswPart.c (limited to 'src/aig/ssw') diff --git a/src/aig/ssw/module.make b/src/aig/ssw/module.make index 2619751e..b176d4db 100644 --- a/src/aig/ssw/module.make +++ b/src/aig/ssw/module.make @@ -3,6 +3,7 @@ SRC += src/aig/ssw/sswAig.c \ src/aig/ssw/sswCnf.c \ src/aig/ssw/sswCore.c \ src/aig/ssw/sswMan.c \ + src/aig/ssw/sswPart.c \ src/aig/ssw/sswSat.c \ src/aig/ssw/sswSim.c \ src/aig/ssw/sswSimSat.c \ diff --git a/src/aig/ssw/ssw.h b/src/aig/ssw/ssw.h index aaaa6407..f76664ec 100644 --- a/src/aig/ssw/ssw.h +++ b/src/aig/ssw/ssw.h @@ -44,11 +44,14 @@ struct Ssw_Pars_t_ int nPartSize; // size of the partition int nOverSize; // size of the overlap between partitions int nFramesK; // the induction depth + int nFramesAddSim; // the number of additional frames to simulate int nConstrs; // treat the last nConstrs POs as seq constraints int nMaxLevs; // the max number of levels of nodes to consider int nBTLimit; // conflict limit at a node + int nMinDomSize; // min clock domain considered for optimization int fPolarFlip; // uses polarity adjustment int fLatchCorr; // perform register correspondence + int fSkipCheck; // does not run equivalence check for unaffected cones int fVerbose; // verbose stats // internal parameters int nIters; // the number of iterations performed @@ -77,6 +80,8 @@ struct Ssw_Cex_t_ /*=== sswCore.c ==========================================================*/ extern void Ssw_ManSetDefaultParams( Ssw_Pars_t * p ); extern Aig_Man_t * Ssw_SignalCorrespondence( Aig_Man_t * p, Ssw_Pars_t * pPars ); +/*=== sswPart.c ==========================================================*/ +extern Aig_Man_t * Ssw_SignalCorrespondencePart( Aig_Man_t * pAig, Ssw_Pars_t * pPars ); #ifdef __cplusplus diff --git a/src/aig/ssw/sswClass.c b/src/aig/ssw/sswClass.c index 66b86009..d06cce49 100644 --- a/src/aig/ssw/sswClass.c +++ b/src/aig/ssw/sswClass.c @@ -46,6 +46,7 @@ struct Ssw_Cla_t_ // temporary data Vec_Ptr_t * vClassOld; // old equivalence class after splitting Vec_Ptr_t * vClassNew; // new equivalence class(es) after splitting + Vec_Ptr_t * vRefined; // the nodes refined since the last iteration // procedures used for class refinement void * pManData; unsigned (*pFuncNodeHash) (void *,Aig_Obj_t *); // returns hash key of the node @@ -141,6 +142,7 @@ Ssw_Cla_t * Ssw_ClassesStart( Aig_Man_t * pAig ) p->pClassSizes = CALLOC( int, Aig_ManObjNumMax(pAig) ); p->vClassOld = Vec_PtrAlloc( 100 ); p->vClassNew = Vec_PtrAlloc( 100 ); + p->vRefined = Vec_PtrAlloc( 1000 ); assert( pAig->pReprs == NULL ); Aig_ManReprStart( pAig, Aig_ManObjNumMax(pAig) ); return p; @@ -183,12 +185,45 @@ void Ssw_ClassesStop( Ssw_Cla_t * p ) { if ( p->vClassNew ) Vec_PtrFree( p->vClassNew ); if ( p->vClassOld ) Vec_PtrFree( p->vClassOld ); + Vec_PtrFree( p->vRefined ); FREE( p->pId2Class ); FREE( p->pClassSizes ); FREE( p->pMemClasses ); free( p ); } +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Vec_Ptr_t * Ssw_ClassesGetRefined( Ssw_Cla_t * p ) +{ + return p->vRefined; +} + +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Ssw_ClassesClearRefined( Ssw_Cla_t * p ) +{ + Vec_PtrClear( p->vRefined ); +} + /**Function************************************************************* Synopsis [Stop representation of equivalence classes.] @@ -368,12 +403,14 @@ 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 ); + Vec_PtrPush( p->vRefined, pObj ); if ( Ssw_ObjIsConst1Cand( p->pAig, pObj ) ) { Aig_ObjSetRepr( p->pAig, pObj, NULL ); p->nCands1--; return; } + Vec_PtrPush( p->vRefined, pRepr ); Aig_ObjSetRepr( p->pAig, pObj, NULL ); assert( p->pId2Class[pRepr->Id][0] == pRepr ); assert( p->pClassSizes[pRepr->Id] >= 2 ); @@ -409,7 +446,7 @@ void Ssw_ClassesRemoveNode( Ssw_Cla_t * p, Aig_Obj_t * pObj ) SeeAlso [] ***********************************************************************/ -Ssw_Cla_t * Ssw_ClassesPrepare( Aig_Man_t * pAig, int fLatchCorr, int nMaxLevs ) +Ssw_Cla_t * Ssw_ClassesPrepare( Aig_Man_t * pAig, int fLatchCorr, int nMaxLevs, int fVerbose ) { Ssw_Cla_t * p; Ssw_Sml_t * pSml; @@ -424,7 +461,10 @@ Ssw_Cla_t * Ssw_ClassesPrepare( Aig_Man_t * pAig, int fLatchCorr, int nMaxLevs ) // perform sequential simulation clk = clock(); pSml = Ssw_SmlSimulateSeq( pAig, 0, 32, 4 ); +if ( fVerbose ) +{ PRT( "Simulation of 32 frames with 4 words", clock() - clk ); +} // set comparison procedures clk = clock(); @@ -441,7 +481,7 @@ clk = clock(); { if ( fLatchCorr ) { - if ( !Saig_ObjIsPi(p->pAig, pObj) ) + if ( !Saig_ObjIsLo(p->pAig, pObj) ) continue; } else @@ -521,7 +561,10 @@ clk = clock(); Ssw_ClassesCheck( p ); Ssw_SmlStop( pSml ); // Ssw_ClassesPrint( p, 0 ); +if ( fVerbose ) +{ PRT( "Collecting candidate equival classes", clock() - clk ); +} return p; } @@ -597,8 +640,6 @@ Ssw_Cla_t * Ssw_ClassesPrepareSimple( Aig_Man_t * pAig, int fLatchCorr, int nMax } // allocate room for classes p->pMemClassesFree = p->pMemClasses = ALLOC( Aig_Obj_t *, p->nCands1 ); - // set comparison procedures - Ssw_ClassesSetData( p, NULL, NULL, Ssw_NodeIsConstCex, Ssw_NodesAreEqualCex ); // Ssw_ClassesPrint( p, 0 ); return p; } @@ -631,6 +672,9 @@ int Ssw_ClassesRefineOneClass( Ssw_Cla_t * p, Aig_Obj_t * pReprOld, int fRecursi // check if splitting happened if ( Vec_PtrSize(p->vClassNew) == 0 ) return 0; + // remember that this class is refined + Ssw_ClassForEachNode( p, pReprOld, pObj, i ) + Vec_PtrPush( p->vRefined, pObj ); // get the new representative pReprNew = Vec_PtrEntry( p->vClassNew, 0 ); @@ -751,7 +795,10 @@ int Ssw_ClassesRefineConst1( Ssw_Cla_t * p, int fRecursive ) { pObj = Aig_ManObj( p->pAig, i ); if ( !p->pFuncNodeIsConst( p->pManData, pObj ) ) + { Vec_PtrPush( p->vClassNew, pObj ); + Vec_PtrPush( p->vRefined, pObj ); + } } // check if there is a new class if ( Vec_PtrSize(p->vClassNew) == 0 ) diff --git a/src/aig/ssw/sswCore.c b/src/aig/ssw/sswCore.c index 409a1ebe..e6096c54 100644 --- a/src/aig/ssw/sswCore.c +++ b/src/aig/ssw/sswCore.c @@ -45,8 +45,10 @@ void Ssw_ManSetDefaultParams( Ssw_Pars_t * p ) p->nPartSize = 0; // size of the partition p->nOverSize = 0; // size of the overlap between partitions p->nFramesK = 1; // the induction depth + p->nFramesAddSim = 2; // additional frames to simulate p->nConstrs = 0; // treat the last nConstrs POs as seq constraints p->nBTLimit = 1000; // conflict limit at a node + p->nMinDomSize = 100; // min clock domain considered for optimization p->fPolarFlip = 0; // uses polarity adjustment p->fLatchCorr = 0; // performs register correspondence p->fVerbose = 0; // verbose stats @@ -71,21 +73,44 @@ Aig_Man_t * Ssw_SignalCorrespondence( Aig_Man_t * pAig, Ssw_Pars_t * pPars ) int RetValue, nIter, clk, clkTotal = clock(); // reset random numbers Aig_ManRandom( 1 ); + + // consider the case of empty AIG + if ( Aig_ManNodeNum(pAig) == 0 ) + { + pPars->nIters = 0; + // Ntl_ManFinalize() needs the following to satisfy an assertion + Aig_ManReprStart( pAig,Aig_ManObjNumMax(pAig) ); + return Aig_ManDupOrdered(pAig); + } + + // check and update parameters + assert( Aig_ManRegNum(pAig) > 0 ); + assert( pPars->nFramesK > 0 ); + if ( pPars->nFramesK > 1 ) + pPars->fSkipCheck = 0; + + // perform partitioning + if ( (pPars->nPartSize > 0 && pPars->nPartSize < Aig_ManRegNum(pAig)) + || (pAig->vClockDoms && Vec_VecSize(pAig->vClockDoms) > 0) ) + return Ssw_SignalCorrespondencePart( pAig, pPars ); + // start the choicing manager p = Ssw_ManCreate( pAig, pPars ); // compute candidate equivalence classes +// p->pPars->nConstrs = 1; if ( p->pPars->nConstrs == 0 ) { - p->ppClasses = Ssw_ClassesPrepare( pAig, pPars->fLatchCorr, pPars->nMaxLevs ); - p->pSml = Ssw_SmlStart( pAig, 0, p->nFrames + 2, 2 ); + // perform one round of seq simulation and generate candidate equivalence classes + p->ppClasses = Ssw_ClassesPrepare( pAig, pPars->fLatchCorr, pPars->nMaxLevs, pPars->fVerbose ); + p->pSml = Ssw_SmlStart( pAig, 0, p->nFrames + p->pPars->nFramesAddSim, 1 ); Ssw_ClassesSetData( p->ppClasses, p->pSml, Ssw_SmlNodeHash, Ssw_SmlNodeIsConst, Ssw_SmlNodesAreEqual ); } else { - assert( 0 ); + // create trivial equivalence classes with all nodes being candidates for constant 1 p->ppClasses = Ssw_ClassesPrepareSimple( pAig, pPars->fLatchCorr, pPars->nMaxLevs ); + Ssw_ClassesSetData( p->ppClasses, NULL, NULL, Ssw_NodeIsConstCex, Ssw_NodesAreEqualCex ); } -// Ssw_ClassesSetData( p->ppClasses, NULL, NULL, Ssw_NodeIsConstCex, Ssw_NodesAreEqualCex ); // get the starting stats p->nLitsBeg = Ssw_ClassesLitNum( p->ppClasses ); @@ -111,9 +136,11 @@ clk = clock(); RetValue = Ssw_ManSweep( p ); if ( pPars->fVerbose ) { - printf( "%3d : Const = %6d. Cl = %6d. L = %6d. LR = %6d. NR = %6d. ", + printf( "%3d : Const = %6d. Cl = %6d. LR = %6d. NR = %6d. F = %5d. ", nIter, Ssw_ClassesCand1Num(p->ppClasses), Ssw_ClassesClassNum(p->ppClasses), - p->nConstrTotal, p->nConstrReduced, Aig_ManNodeNum(p->pFrames) ); + p->nConstrReduced, Aig_ManNodeNum(p->pFrames), p->nSatFailsReal ); + printf( "Use = %5d. Skip = %5d. ", + p->nRefUse, p->nRefSkip ); PRT( "T", clock() - clk ); } Ssw_ManCleanup( p ); @@ -133,6 +160,8 @@ p->timeTotal = clock() - clkTotal; return pAigNew; } + + //////////////////////////////////////////////////////////////////////// /// END OF FILE /// //////////////////////////////////////////////////////////////////////// diff --git a/src/aig/ssw/sswInt.h b/src/aig/ssw/sswInt.h index 009c09c4..c9dd1958 100644 --- a/src/aig/ssw/sswInt.h +++ b/src/aig/ssw/sswInt.h @@ -57,6 +57,8 @@ struct Ssw_Man_t_ // equivalence classes Ssw_Cla_t * ppClasses; // equivalence classes of nodes int fRefined; // is set to 1 when refinement happens + int nRefUse; + int nRefSkip; // SAT solving sat_solver * pSat; // recyclable SAT solver int nSatVars; // the counter of SAT variables @@ -77,8 +79,8 @@ struct Ssw_Man_t_ // 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 nSatFailsTotal; // the number of timeouts int nSatCallsUnsat; // the number of unsat SAT calls int nSatCallsSat; // the number of sat SAT calls // node/register/lit statistics @@ -91,6 +93,7 @@ struct Ssw_Man_t_ // runtime stats int timeBmc; // bounded model checking int timeReduce; // speculative reduction + int timeMarkCones; // marking the cones not to be refined int timeSimSat; // simulation of the counter-examples int timeSat; // solving SAT int timeSatSat; // sat @@ -136,6 +139,8 @@ extern void Ssw_ClassesSetData( Ssw_Cla_t * p, void * pManData, int (*pFuncNodeIsConst)(void *,Aig_Obj_t *), int (*pFuncNodesAreEqual)(void *,Aig_Obj_t *, Aig_Obj_t *) ); extern void Ssw_ClassesStop( Ssw_Cla_t * p ); +extern Vec_Ptr_t * Ssw_ClassesGetRefined( Ssw_Cla_t * p ); +extern void Ssw_ClassesClearRefined( Ssw_Cla_t * p ); extern int Ssw_ClassesCand1Num( Ssw_Cla_t * p ); extern int Ssw_ClassesClassNum( Ssw_Cla_t * p ); extern int Ssw_ClassesLitNum( Ssw_Cla_t * p ); @@ -143,7 +148,7 @@ 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 Ssw_Cla_t * Ssw_ClassesPrepare( Aig_Man_t * pAig, int fLatchCorr, int nMaxLevs ); +extern Ssw_Cla_t * Ssw_ClassesPrepare( Aig_Man_t * pAig, int fLatchCorr, int nMaxLevs, int fVerbose ); extern Ssw_Cla_t * Ssw_ClassesPrepareSimple( Aig_Man_t * pAig, int fLatchCorr, int nMaxLevs ); extern int Ssw_ClassesRefine( Ssw_Cla_t * p, int fRecursive ); extern int Ssw_ClassesRefineOneClass( Ssw_Cla_t * p, Aig_Obj_t * pRepr, int fRecursive ); @@ -171,6 +176,7 @@ extern int Ssw_SmlNodesAreEqual( Ssw_Sml_t * p, Aig_Obj_t * pObj0, Aig extern void Ssw_SmlAssignDist1Plus( Ssw_Sml_t * p, unsigned * pPat ); extern void Ssw_SmlSimulateOne( Ssw_Sml_t * p ); /*=== sswSimSat.c ===================================================*/ +extern int Ssw_ManOriginalPiValue( Ssw_Man_t * p, Aig_Obj_t * pObj, int f ); 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 ); diff --git a/src/aig/ssw/sswMan.c b/src/aig/ssw/sswMan.c index a6e02125..f25cee45 100644 --- a/src/aig/ssw/sswMan.c +++ b/src/aig/ssw/sswMan.c @@ -99,27 +99,28 @@ void Ssw_ManPrintStats( Ssw_Man_t * p ) { 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( "Parameters: Fr = %d. C-limit = %d. Constr = %d. SkipCheck = %d. MaxLev = %d. Mem = %0.2f Mb.\n", + p->pPars->nFramesK, p->pPars->nBTLimit, p->pPars->nConstrs, p->pPars->fSkipCheck, 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( "SAT calls : Proof = %d. Cex = %d. Fail = %d. Equivs = %d. Str = %d.\n", + p->nSatProof, p->nSatCallsSat, p->nSatFailsTotal, 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 ); - PRTP( "Sim SAT ", p->timeSimSat, p->timeTotal ); - PRTP( "SAT solving", p->timeSat, p->timeTotal ); - PRTP( " unsat ", p->timeSatUnsat, p->timeTotal ); - PRTP( " sat ", p->timeSatSat, p->timeTotal ); - PRTP( " undecided", p->timeSatUndec, p->timeTotal ); - PRTP( "Other ", p->timeOther, p->timeTotal ); - PRTP( "TOTAL ", p->timeTotal, p->timeTotal ); + p->timeOther = p->timeTotal-p->timeBmc-p->timeReduce-p->timeMarkCones-p->timeSimSat-p->timeSat; + PRTP( "BMC ", p->timeBmc, p->timeTotal ); + PRTP( "Spec reduce", p->timeReduce, p->timeTotal ); + PRTP( "Mark cones ", p->timeMarkCones, p->timeTotal ); + PRTP( "Sim SAT ", p->timeSimSat, p->timeTotal ); + PRTP( "SAT solving", p->timeSat, p->timeTotal ); + PRTP( " unsat ", p->timeSatUnsat, p->timeTotal ); + PRTP( " sat ", p->timeSatSat, p->timeTotal ); + PRTP( " undecided", p->timeSatUndec, p->timeTotal ); + PRTP( "Other ", p->timeOther, p->timeTotal ); + PRTP( "TOTAL ", p->timeTotal, p->timeTotal ); } /**Function************************************************************* @@ -167,6 +168,7 @@ void Ssw_ManCleanup( Ssw_Man_t * p ) ***********************************************************************/ void Ssw_ManStop( Ssw_Man_t * p ) { + Aig_ManCleanMarkA( p->pAig ); if ( p->pPars->fVerbose ) Ssw_ManPrintStats( p ); if ( p->ppClasses ) diff --git a/src/aig/ssw/sswPart.c b/src/aig/ssw/sswPart.c new file mode 100644 index 00000000..7eb6b8fe --- /dev/null +++ b/src/aig/ssw/sswPart.c @@ -0,0 +1,129 @@ +/**CFile**************************************************************** + + FileName [sswPart.c] + + SystemName [ABC: Logic synthesis and verification system.] + + PackageName [Inductive prover with constraints.] + + Synopsis [Partitioned signal correspondence.] + + Author [Alan Mishchenko] + + Affiliation [UC Berkeley] + + Date [Ver. 1.0. Started - September 1, 2008.] + + Revision [$Id: sswPart.c,v 1.00 2008/09/01 00:00:00 alanmi Exp $] + +***********************************************************************/ + +#include "sswInt.h" + +//////////////////////////////////////////////////////////////////////// +/// DECLARATIONS /// +//////////////////////////////////////////////////////////////////////// + +//////////////////////////////////////////////////////////////////////// +/// FUNCTION DEFINITIONS /// +//////////////////////////////////////////////////////////////////////// + +/**Function************************************************************* + + Synopsis [Performs partitioned sequential SAT sweepingG.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Aig_Man_t * Ssw_SignalCorrespondencePart( Aig_Man_t * pAig, Ssw_Pars_t * pPars ) +{ + int fPrintParts = 0; + char Buffer[100]; + Aig_Man_t * pTemp, * pNew; + Vec_Ptr_t * vResult; + Vec_Int_t * vPart; + int * pMapBack; + int i, nCountPis, nCountRegs; + int nClasses, nPartSize, fVerbose; + int clk = clock(); + + // save parameters + nPartSize = pPars->nPartSize; pPars->nPartSize = 0; + fVerbose = pPars->fVerbose; pPars->fVerbose = 0; + // generate partitions + if ( pAig->vClockDoms ) + { + // divide large clock domains into separate partitions + vResult = Vec_PtrAlloc( 100 ); + Vec_PtrForEachEntry( (Vec_Ptr_t *)pAig->vClockDoms, vPart, i ) + { + if ( nPartSize && Vec_IntSize(vPart) > nPartSize ) + Aig_ManPartDivide( vResult, vPart, nPartSize, pPars->nOverSize ); + else + Vec_PtrPush( vResult, Vec_IntDup(vPart) ); + } + } + else + vResult = Aig_ManRegPartitionSimple( pAig, nPartSize, pPars->nOverSize ); +// vResult = Aig_ManPartitionSmartRegisters( pAig, nPartSize, 0 ); +// vResult = Aig_ManRegPartitionSmart( pAig, nPartSize ); + if ( fPrintParts ) + { + // print partitions + printf( "Simple partitioning. %d partitions are saved:\n", Vec_PtrSize(vResult) ); + Vec_PtrForEachEntry( vResult, vPart, i ) + { + extern void Ioa_WriteAiger( Aig_Man_t * pMan, char * pFileName, int fWriteSymbols, int fCompact ); + sprintf( Buffer, "part%03d.aig", i ); + pTemp = Aig_ManRegCreatePart( pAig, vPart, &nCountPis, &nCountRegs, NULL ); + Ioa_WriteAiger( pTemp, Buffer, 0, 0 ); + printf( "part%03d.aig : Reg = %4d. PI = %4d. (True = %4d. Regs = %4d.) And = %5d.\n", + i, Vec_IntSize(vPart), Aig_ManPiNum(pTemp)-Vec_IntSize(vPart), nCountPis, nCountRegs, Aig_ManNodeNum(pTemp) ); + Aig_ManStop( pTemp ); + } + } + + // perform SSW with partitions + Aig_ManReprStart( pAig, Aig_ManObjNumMax(pAig) ); + Vec_PtrForEachEntry( vResult, vPart, i ) + { + pTemp = Aig_ManRegCreatePart( pAig, vPart, &nCountPis, &nCountRegs, &pMapBack ); + Aig_ManSetRegNum( pTemp, pTemp->nRegs ); + // create the projection of 1-hot registers + if ( pAig->vOnehots ) + pTemp->vOnehots = Aig_ManRegProjectOnehots( pAig, pTemp, pAig->vOnehots, fVerbose ); + // run SSW + pNew = Ssw_SignalCorrespondence( pTemp, pPars ); + nClasses = Aig_TransferMappedClasses( pAig, pTemp, pMapBack ); + if ( fVerbose ) + printf( "%3d : Reg = %4d. PI = %4d. (True = %4d. Regs = %4d.) And = %5d. It = %3d. Cl = %5d.\n", + i, Vec_IntSize(vPart), Aig_ManPiNum(pTemp)-Vec_IntSize(vPart), nCountPis, nCountRegs, Aig_ManNodeNum(pTemp), pPars->nIters, nClasses ); + Aig_ManStop( pNew ); + Aig_ManStop( pTemp ); + free( pMapBack ); + } + // remap the AIG + pNew = Aig_ManDupRepr( pAig, 0 ); + Aig_ManSeqCleanup( pNew ); +// Aig_ManPrintStats( pAig ); +// Aig_ManPrintStats( pNew ); + Vec_VecFree( (Vec_Vec_t *)vResult ); + pPars->nPartSize = nPartSize; + pPars->fVerbose = fVerbose; + if ( fVerbose ) + { + PRT( "Total time", clock() - clk ); + } + return pNew; +} + + +//////////////////////////////////////////////////////////////////////// +/// END OF FILE /// +//////////////////////////////////////////////////////////////////////// + + diff --git a/src/aig/ssw/sswSimSat.c b/src/aig/ssw/sswSimSat.c index 547755f0..6ef5ec20 100644 --- a/src/aig/ssw/sswSimSat.c +++ b/src/aig/ssw/sswSimSat.c @@ -234,7 +234,8 @@ void Ssw_ManResimulateCexTotal( Ssw_Man_t * p, Aig_Obj_t * pCand, Aig_Obj_t * pR // set the PI simulation information Aig_ManConst1(p->pAig)->fMarkB = 1; Aig_ManForEachPi( p->pAig, pObj, i ) - pObj->fMarkB = Ssw_ManOriginalPiValue( p, pObj, f ); +// pObj->fMarkB = Ssw_ManOriginalPiValue( p, pObj, f ); + pObj->fMarkB = Aig_InfoHasBit( p->pPatWords, i ); // simulate internal nodes Aig_ManForEachNode( p->pAig, pObj, i ) pObj->fMarkB = ( Aig_ObjFanin0(pObj)->fMarkB ^ Aig_ObjFaninC0(pObj) ) @@ -251,27 +252,6 @@ 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.] @@ -287,7 +267,7 @@ void Ssw_ManResimulateCexTotalSim( Ssw_Man_t * p, Aig_Obj_t * pCand, Aig_Obj_t * { int RetValue1, RetValue2, clk = clock(); // save the counter-example - Ssw_SmlSavePatternAig( p, f ); +// Ssw_SmlSavePatternAig( p, f ); // set the PI simulation information Ssw_SmlAssignDist1Plus( p->pSml, p->pPatWords ); // simulate internal nodes diff --git a/src/aig/ssw/sswSweep.c b/src/aig/ssw/sswSweep.c index 7c99fad2..5ad6d78e 100644 --- a/src/aig/ssw/sswSweep.c +++ b/src/aig/ssw/sswSweep.c @@ -29,6 +29,95 @@ /// FUNCTION DEFINITIONS /// //////////////////////////////////////////////////////////////////////// +/**Function************************************************************* + + Synopsis [Mark nodes affected by sweep in the previous iteration.] + + Description [Assumes that affected nodes are in p->ppClasses->vRefined.] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Ssw_ManSweepMarkRefinement( Ssw_Man_t * p ) +{ + Vec_Ptr_t * vRefined, * vSupp; + Aig_Obj_t * pObj, * pObjLo, * pObjLi; + int i, k; + vRefined = Ssw_ClassesGetRefined( p->ppClasses ); + if ( Vec_PtrSize(vRefined) == 0 ) + { + Aig_ManForEachObj( p->pAig, pObj, i ) + pObj->fMarkA = 1; + return; + } + // mark the nodes to be refined + Aig_ManCleanMarkA( p->pAig ); + Vec_PtrForEachEntry( vRefined, pObj, i ) + { + if ( Aig_ObjIsPi(pObj) ) + { + pObj->fMarkA = 1; + continue; + } + assert( Aig_ObjIsNode(pObj) ); + vSupp = Aig_Support( p->pAig, pObj ); + Vec_PtrForEachEntry( vSupp, pObjLo, k ) + pObjLo->fMarkA = 1; + Vec_PtrFree( vSupp ); + } + // mark refinement + Aig_ManForEachNode( p->pAig, pObj, i ) + pObj->fMarkA = Aig_ObjFanin0(pObj)->fMarkA | Aig_ObjFanin1(pObj)->fMarkA; + Saig_ManForEachLi( p->pAig, pObj, i ) + pObj->fMarkA |= Aig_ObjFanin0(pObj)->fMarkA; + Saig_ManForEachLiLo( p->pAig, pObjLi, pObjLo, i ) + pObjLo->fMarkA |= pObjLi->fMarkA; +} + +/**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 [Copy pattern from the solver into the internal storage.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Ssw_SmlSavePatternAigPhase( 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 ( Aig_ObjPhaseReal( Ssw_ObjFraig(p, pObj, f) ) ) + Aig_InfoSetBit( p->pPatWords, i ); +} + /**Function************************************************************* Synopsis [Performs fraiging for one node.] @@ -40,7 +129,7 @@ SeeAlso [] ***********************************************************************/ -void Ssw_ManSweepNode( Ssw_Man_t * p, Aig_Obj_t * pObj, int f ) +void Ssw_ManSweepNode( Ssw_Man_t * p, Aig_Obj_t * pObj, int f, int fBmc ) { Aig_Obj_t * pObjRepr, * pObjFraig, * pObjFraig2, * pObjReprFraig; int RetValue; @@ -50,59 +139,58 @@ void Ssw_ManSweepNode( Ssw_Man_t * p, Aig_Obj_t * pObj, int f ) return; // get the fraiged node pObjFraig = Ssw_ObjFraig( p, pObj, f ); - assert( pObjFraig != NULL ); // get the fraiged representative pObjReprFraig = Ssw_ObjFraig( p, pObjRepr, f ); - assert( pObjReprFraig != NULL ); // check if constant 0 pattern distinquishes these nodes + assert( pObjFraig != NULL && pObjReprFraig != NULL ); if ( (pObj->fPhase == pObjRepr->fPhase) != (Aig_ObjPhaseReal(pObjFraig) == Aig_ObjPhaseReal(pObjReprFraig)) ) { - Aig_Obj_t * pObj; - int i; - if ( p->pSat->model.cap < p->pSat->size ) - { - veci_resize(&p->pSat->model, 0); - for ( i = 0; i < p->pSat->size; i++ ) - veci_push( &p->pSat->model, (int)l_False ); - } - // set the values of SAT vars to be equal to the phase of the nodes - Aig_ManForEachObj( p->pFrames, pObj, i ) - if ( Ssw_ObjSatNum( p, pObj ) ) - { - int iVar = Ssw_ObjSatNum( p, pObj ); - assert( iVar < p->pSat->size ); - p->pSat->model.ptr[iVar] = (int)(p->pPars->fPolarFlip? 0 : (pObj->fPhase? l_True : l_False)); - p->pSat->model.size = p->pSat->size; - } p->nStrangers++; - return; + Ssw_SmlSavePatternAigPhase( p, f ); } - // if the fraiged nodes are the same, return - if ( Aig_Regular(pObjFraig) == Aig_Regular(pObjReprFraig) ) - 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) ); else - RetValue = Ssw_NodesAreEquiv( p, Aig_Regular(pObjFraig), Aig_Regular(pObjReprFraig) ); - - if ( RetValue == -1 ) // timed out - { -// assert( 0 ); - Ssw_ClassesRemoveNode( p->ppClasses, pObj ); - p->fRefined = 1; - return; - } - if ( RetValue == 1 ) // proved equivalent { - pObjFraig2 = Aig_NotCond( pObjReprFraig, pObj->fPhase ^ pObjRepr->fPhase ); - Ssw_ObjSetFraig( p, pObj, f, pObjFraig2 ); - return; + // if the fraiged nodes are the same, return + if ( Aig_Regular(pObjFraig) == Aig_Regular(pObjReprFraig) ) + return; + // count the number of skipped calls + if ( !pObj->fMarkA && !pObjRepr->fMarkA ) + p->nRefSkip++; + else + p->nRefUse++; + // call equivalence checking + if ( p->pPars->fSkipCheck && !fBmc && !pObj->fMarkA && !pObjRepr->fMarkA ) + RetValue = 1; + else if ( Aig_Regular(pObjFraig) != Aig_ManConst1(p->pFrames) ) + RetValue = Ssw_NodesAreEquiv( p, Aig_Regular(pObjReprFraig), Aig_Regular(pObjFraig) ); + else + RetValue = Ssw_NodesAreEquiv( p, Aig_Regular(pObjFraig), Aig_Regular(pObjReprFraig) ); + if ( RetValue == 1 ) // proved equivalent + { + pObjFraig2 = Aig_NotCond( pObjReprFraig, pObj->fPhase ^ pObjRepr->fPhase ); + Ssw_ObjSetFraig( p, pObj, f, pObjFraig2 ); + return; + } + if ( RetValue == -1 ) // timed out + { + Ssw_ClassesRemoveNode( p->ppClasses, pObj ); + p->fRefined = 1; + return; + } + // check if skipping calls works correctly + if ( p->pPars->fSkipCheck && !fBmc && !pObj->fMarkA && !pObjRepr->fMarkA ) + { + assert( 0 ); + printf( "\nMistake!!!\n" ); + } + // disproved the equivalence + Ssw_SmlSavePatternAig( p, f ); } - // disproved the equivalence // Ssw_ManResimulateCex( p, pObj, pObjRepr, f ); -// Ssw_ManResimulateCexTotal( p, pObj, pObjRepr, f ); - Ssw_ManResimulateCexTotalSim( p, pObj, pObjRepr, f ); + if ( p->pPars->nConstrs == 0 ) + Ssw_ManResimulateCexTotalSim( p, pObj, pObjRepr, f ); + else + Ssw_ManResimulateCexTotal( p, pObj, pObjRepr, f ); assert( Aig_ObjRepr( p->pAig, pObj ) != pObjRepr ); p->fRefined = 1; } @@ -147,7 +235,7 @@ clk = clock(); Bar_ProgressUpdate( pProgress, Aig_ManObjNumMax(p->pAig) * f + i, NULL ); 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 ); + Ssw_ManSweepNode( p, pObj, f, 1 ); } // quit if this is the last timeframe if ( f == p->pPars->nFramesK - 1 ) @@ -205,6 +293,12 @@ clk = clock(); sat_solver_simplify( p->pSat ); p->timeReduce += clock() - clk; + // mark nodes that do not have to be refined +clk = clock(); + if ( p->pPars->fSkipCheck ) + Ssw_ManSweepMarkRefinement( p ); +p->timeMarkCones += clock() - clk; + // map constants and PIs of the last frame f = p->pPars->nFramesK; Ssw_ObjSetFraig( p, Aig_ManConst1(p->pAig), f, Aig_ManConst1(p->pFrames) ); @@ -215,6 +309,9 @@ p->timeReduce += clock() - clk; assert( Ssw_ObjFraig( p, pObj, f ) != NULL ); // sweep internal nodes p->fRefined = 0; + p->nSatFailsReal = 0; + p->nRefUse = p->nRefSkip = 0; + Ssw_ClassesClearRefined( p->ppClasses ); if ( p->pPars->fVerbose ) pProgress = Bar_ProgressStart( stdout, Aig_ManObjNumMax(p->pAig) ); Aig_ManForEachObj( p->pAig, pObj, i ) @@ -222,14 +319,16 @@ p->timeReduce += clock() - clk; if ( p->pPars->fVerbose ) Bar_ProgressUpdate( pProgress, i, NULL ); if ( Saig_ObjIsLo(p->pAig, pObj) ) - Ssw_ManSweepNode( p, pObj, f ); + Ssw_ManSweepNode( p, pObj, f, 0 ); else if ( Aig_ObjIsNode(pObj) ) { + pObj->fMarkA = Aig_ObjFanin0(pObj)->fMarkA | Aig_ObjFanin1(pObj)->fMarkA; 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 ); + Ssw_ManSweepNode( p, pObj, f, 0 ); } } + p->nSatFailsTotal += p->nSatFailsReal; if ( p->pPars->fVerbose ) Bar_ProgressStop( pProgress ); -- cgit v1.2.3