From 6130e39b18b5f53902e4eab14f6d5cdde5219563 Mon Sep 17 00:00:00 2001 From: Alan Mishchenko Date: Mon, 1 Nov 2010 01:35:04 -0700 Subject: initial commit of public abc --- src/aig/ssw/module.make | 2 + src/aig/ssw/ssw.h | 51 ++-- src/aig/ssw/sswAig.c | 22 +- src/aig/ssw/sswBmc.c | 9 +- src/aig/ssw/sswClass.c | 114 +++++++-- src/aig/ssw/sswCnf.c | 15 +- src/aig/ssw/sswConstr.c | 635 +++++++++++++++++++++++++++++++++++++++++++++++ src/aig/ssw/sswCore.c | 225 ++++++++++++++--- src/aig/ssw/sswDyn.c | 19 +- src/aig/ssw/sswFilter.c | 492 ++++++++++++++++++++++++++++++++++++ src/aig/ssw/sswInt.h | 38 ++- src/aig/ssw/sswIslands.c | 31 ++- src/aig/ssw/sswLcorr.c | 13 +- src/aig/ssw/sswMan.c | 29 ++- src/aig/ssw/sswPairs.c | 13 +- src/aig/ssw/sswPart.c | 22 +- src/aig/ssw/sswSat.c | 39 ++- src/aig/ssw/sswSemi.c | 11 +- src/aig/ssw/sswSim.c | 48 ++-- src/aig/ssw/sswSimSat.c | 37 +-- src/aig/ssw/sswSweep.c | 51 +--- src/aig/ssw/sswUnique.c | 11 +- 22 files changed, 1710 insertions(+), 217 deletions(-) create mode 100644 src/aig/ssw/sswConstr.c create mode 100644 src/aig/ssw/sswFilter.c (limited to 'src/aig/ssw') diff --git a/src/aig/ssw/module.make b/src/aig/ssw/module.make index 1e79c955..9d93fb93 100644 --- a/src/aig/ssw/module.make +++ b/src/aig/ssw/module.make @@ -2,8 +2,10 @@ SRC += src/aig/ssw/sswAig.c \ src/aig/ssw/sswBmc.c \ src/aig/ssw/sswClass.c \ src/aig/ssw/sswCnf.c \ + src/aig/ssw/sswConstr.c \ src/aig/ssw/sswCore.c \ src/aig/ssw/sswDyn.c \ + src/aig/ssw/sswFilter.c \ src/aig/ssw/sswIslands.c \ src/aig/ssw/sswLcorr.c \ src/aig/ssw/sswMan.c \ diff --git a/src/aig/ssw/ssw.h b/src/aig/ssw/ssw.h index c2a33ee4..207ebea9 100644 --- a/src/aig/ssw/ssw.h +++ b/src/aig/ssw/ssw.h @@ -21,6 +21,7 @@ #ifndef __SSW_H__ #define __SSW_H__ + //////////////////////////////////////////////////////////////////////// /// INCLUDES /// //////////////////////////////////////////////////////////////////////// @@ -29,9 +30,7 @@ /// PARAMETERS /// //////////////////////////////////////////////////////////////////////// -#ifdef __cplusplus -extern "C" { -#endif +ABC_NAMESPACE_HEADER_START //////////////////////////////////////////////////////////////////////// /// BASIC TYPES /// @@ -45,7 +44,8 @@ struct Ssw_Pars_t_ 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 fConstrs; // treat the last nConstrs POs as seq constraints + int fMergeFull; // enables full merge when constraints are used int nMaxLevs; // the max number of levels of nodes to consider int nBTLimit; // conflict limit at a node int nBTLimitGlobal;// conflict limit for multiple runs @@ -53,10 +53,13 @@ struct Ssw_Pars_t_ int nItersStop; // stop after the given number of iterations int fDumpSRInit; // dumps speculative reduction int nResimDelta; // the number of nodes to resimulate + int nStepsMax; // (scorr only) the max number of induction steps + int TimeLimit; // time out in seconds int fPolarFlip; // uses polarity adjustment int fLatchCorr; // perform register correspondence + int fOutputCorr; // perform 'PO correspondence' int fSemiFormal; // enable semiformal filtering - int fUniqueness; // enable uniqueness constraints +// int fUniqueness; // enable uniqueness constraints int fDynamic; // enable dynamic addition of constraints int fLocalSim; // enable local simulation simulation int fPartSigCorr; // uses partial signal correspondence @@ -75,18 +78,9 @@ struct Ssw_Pars_t_ // internal parameters int nIters; // the number of iterations performed int nConflicts; // the total number of conflicts 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) + // callback + void * pData; + void * pFunc; }; typedef struct Ssw_Sml_t_ Ssw_Sml_t; // sequential simulation manager @@ -101,6 +95,8 @@ typedef struct Ssw_Sml_t_ Ssw_Sml_t; // sequential simulation manager /*=== sswBmc.c ==========================================================*/ extern int Ssw_BmcDynamic( Aig_Man_t * pAig, int nFramesMax, int nConfLimit, int fVerbose, int * piFrame ); +/*=== sswConstr.c ==========================================================*/ +extern int Ssw_ManSetConstrPhases( Aig_Man_t * p, int nFrames, Vec_Int_t ** pvInits ); /*=== sswCore.c ==========================================================*/ extern void Ssw_ManSetDefaultParams( Ssw_Pars_t * p ); extern void Ssw_ManSetDefaultParamsLcorr( Ssw_Pars_t * p ); @@ -110,7 +106,6 @@ extern Aig_Man_t * Ssw_LatchCorrespondence( Aig_Man_t * pAig, Ssw_Pars_t * pPa extern int Ssw_SecWithSimilarityPairs( Aig_Man_t * p0, Aig_Man_t * p1, Vec_Int_t * vPairs, Ssw_Pars_t * pPars ); extern int Ssw_SecWithSimilarity( Aig_Man_t * p0, Aig_Man_t * p1, Ssw_Pars_t * pPars ); /*=== sswMiter.c ===================================================*/ -extern int Ssw_SecSpecialMiter( Aig_Man_t * p0, Aig_Man_t * p1, int nFrames, int fVerbose ); /*=== sswPart.c ==========================================================*/ extern Aig_Man_t * Ssw_SignalCorrespondencePart( Aig_Man_t * pAig, Ssw_Pars_t * pPars ); /*=== sswPairs.c ===================================================*/ @@ -127,15 +122,17 @@ extern int Ssw_SmlNumFrames( Ssw_Sml_t * p ); extern int Ssw_SmlNumWordsTotal( Ssw_Sml_t * p ); extern unsigned * Ssw_SmlSimInfo( Ssw_Sml_t * p, Aig_Obj_t * pObj ); extern int Ssw_SmlObjsAreEqualWord( Ssw_Sml_t * p, Aig_Obj_t * pObj0, Aig_Obj_t * pObj1 ); -extern Ssw_Cex_t * Ssw_SmlAllocCounterExample( int nRegs, int nRealPis, int nFrames ); -extern void Ssw_SmlFreeCounterExample( Ssw_Cex_t * pCex ); -extern int Ssw_SmlRunCounterExample( Aig_Man_t * pAig, Ssw_Cex_t * p ); -extern int Ssw_SmlFindOutputCounterExample( Aig_Man_t * pAig, Ssw_Cex_t * p ); -extern Ssw_Cex_t * Ssw_SmlDupCounterExample( Ssw_Cex_t * p, int nRegsNew ); - -#ifdef __cplusplus -} -#endif +extern Abc_Cex_t * Ssw_SmlAllocCounterExample( int nRegs, int nRealPis, int nFrames ); +extern void Ssw_SmlFreeCounterExample( Abc_Cex_t * pCex ); +extern int Ssw_SmlRunCounterExample( Aig_Man_t * pAig, Abc_Cex_t * p ); +extern int Ssw_SmlFindOutputCounterExample( Aig_Man_t * pAig, Abc_Cex_t * p ); +extern Abc_Cex_t * Ssw_SmlDupCounterExample( Abc_Cex_t * p, int nRegsNew ); + + + +ABC_NAMESPACE_HEADER_END + + #endif diff --git a/src/aig/ssw/sswAig.c b/src/aig/ssw/sswAig.c index 62e93d2d..f3174470 100644 --- a/src/aig/ssw/sswAig.c +++ b/src/aig/ssw/sswAig.c @@ -20,6 +20,9 @@ #include "sswInt.h" +ABC_NAMESPACE_IMPL_START + + //////////////////////////////////////////////////////////////////////// /// DECLARATIONS /// //////////////////////////////////////////////////////////////////////// @@ -142,7 +145,7 @@ Aig_Man_t * Ssw_FramesWithClasses( Ssw_Man_t * p ) { Aig_Man_t * pFrames; Aig_Obj_t * pObj, * pObjLi, * pObjLo, * pObjNew; - int i, f; + int i, f, iLits; assert( p->pFrames == NULL ); assert( Aig_ManRegNum(p->pAig) > 0 ); assert( Aig_ManRegNum(p->pAig) < Aig_ManPiNum(p->pAig) ); @@ -154,12 +157,17 @@ Aig_Man_t * Ssw_FramesWithClasses( Ssw_Man_t * p ) Saig_ManForEachLo( p->pAig, pObj, i ) Ssw_ObjSetFrame( p, pObj, 0, Aig_ObjCreatePi(pFrames) ); // add timeframes + iLits = 0; for ( f = 0; f < p->pPars->nFramesK; f++ ) { // map constants and PIs Ssw_ObjSetFrame( p, Aig_ManConst1(p->pAig), f, Aig_ManConst1(pFrames) ); Saig_ManForEachPi( p->pAig, pObj, i ) - Ssw_ObjSetFrame( p, pObj, f, Aig_ObjCreatePi(pFrames) ); + { + pObjNew = Aig_ObjCreatePi(pFrames); + pObjNew->fPhase = (p->vInits != NULL) && Vec_IntEntry(p->vInits, iLits++); + Ssw_ObjSetFrame( p, pObj, f, pObjNew ); + } // set the constraints on the latch outputs Saig_ManForEachLo( p->pAig, pObj, i ) Ssw_FramesConstrainNode( p, pFrames, p->pAig, pObj, f, 1 ); @@ -170,10 +178,14 @@ Aig_Man_t * Ssw_FramesWithClasses( Ssw_Man_t * p ) Ssw_ObjSetFrame( p, pObj, f, pObjNew ); Ssw_FramesConstrainNode( p, pFrames, p->pAig, pObj, f, 1 ); } + // transfer to the primary outputs + Aig_ManForEachPo( p->pAig, pObj, i ) + Ssw_ObjSetFrame( p, pObj, f, Ssw_ObjChild0Fra(p, pObj,f) ); // transfer latch input to the latch outputs Saig_ManForEachLiLo( p->pAig, pObjLi, pObjLo, i ) - Ssw_ObjSetFrame( p, pObjLo, f+1, Ssw_ObjChild0Fra(p, pObjLi,f) ); + Ssw_ObjSetFrame( p, pObjLo, f+1, Ssw_ObjFrame(p, pObjLi,f) ); } + assert( p->vInits == NULL || Vec_IntSize(p->vInits) == iLits + Saig_ManPiNum(p->pAig) ); // add the POs for the latch outputs of the last frame Saig_ManForEachLo( p->pAig, pObj, i ) Aig_ObjCreatePo( pFrames, Ssw_ObjFrame( p, pObj, p->pPars->nFramesK ) ); @@ -186,8 +198,6 @@ Aig_Man_t * Ssw_FramesWithClasses( Ssw_Man_t * p ) return pFrames; } - - /**Function************************************************************* Synopsis [Prepares the inductive case with speculative reduction.] @@ -245,3 +255,5 @@ Aig_Man_t * Ssw_SpeculativeReduction( Ssw_Man_t * p ) //////////////////////////////////////////////////////////////////////// +ABC_NAMESPACE_IMPL_END + diff --git a/src/aig/ssw/sswBmc.c b/src/aig/ssw/sswBmc.c index 86d04424..aba32304 100644 --- a/src/aig/ssw/sswBmc.c +++ b/src/aig/ssw/sswBmc.c @@ -20,6 +20,9 @@ #include "sswInt.h" +ABC_NAMESPACE_IMPL_START + + //////////////////////////////////////////////////////////////////////// /// DECLARATIONS /// //////////////////////////////////////////////////////////////////////// @@ -84,9 +87,9 @@ Aig_Obj_t * Ssw_BmcUnroll_rec( Ssw_Frm_t * pFrm, Aig_Obj_t * pObj, int f ) SeeAlso [] ***********************************************************************/ -Ssw_Cex_t * Ssw_BmcGetCounterExample( Ssw_Frm_t * pFrm, Ssw_Sat_t * pSat, int iPo, int iFrame ) +Abc_Cex_t * Ssw_BmcGetCounterExample( Ssw_Frm_t * pFrm, Ssw_Sat_t * pSat, int iPo, int iFrame ) { - Ssw_Cex_t * pCex; + Abc_Cex_t * pCex; Aig_Obj_t * pObj, * pObjFrames; int f, i, nShift; assert( Saig_ManRegNum(pFrm->pAig) > 0 ); @@ -217,3 +220,5 @@ int Ssw_BmcDynamic( Aig_Man_t * pAig, int nFramesMax, int nConfLimit, int fVerbo //////////////////////////////////////////////////////////////////////// +ABC_NAMESPACE_IMPL_END + diff --git a/src/aig/ssw/sswClass.c b/src/aig/ssw/sswClass.c index ce6ebf85..7fd2a21b 100644 --- a/src/aig/ssw/sswClass.c +++ b/src/aig/ssw/sswClass.c @@ -20,6 +20,9 @@ #include "sswInt.h" +ABC_NAMESPACE_IMPL_START + + /* The candidate equivalence classes are stored as a vector of pointers to the array of pointers to the nodes in each class. @@ -144,8 +147,8 @@ Ssw_Cla_t * Ssw_ClassesStart( Aig_Man_t * 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) ); + if ( pAig->pReprs == NULL ) + Aig_ManReprStart( pAig, Aig_ManObjNumMax(pAig) ); return p; } @@ -412,7 +415,7 @@ void Ssw_ClassesPrint( Ssw_Cla_t * p, int fVeryVerbose ) Aig_Obj_t ** ppClass; Aig_Obj_t * pObj; int i; - printf( "Equivalence classes: Const1 = %5d. Class = %5d. Lit = %5d.\n", + printf( "Equiv classes: Const1 = %5d. Class = %5d. Lit = %5d.\n", p->nCands1, p->nClasses, p->nCands1+p->nLits ); if ( !fVeryVerbose ) return; @@ -508,7 +511,7 @@ int Ssw_ClassesPrepareRehash( Ssw_Cla_t * p, Vec_Ptr_t * vCands ) // sort through the candidates nEntries = 0; p->nCands1 = 0; - Vec_PtrForEachEntry( vCands, pObj, i ) + Vec_PtrForEachEntry( Aig_Obj_t *, vCands, pObj, i ) { assert( p->pClassSizes[pObj->Id] == 0 ); Aig_ObjSetRepr( p->pAig, pObj, NULL ); @@ -547,7 +550,7 @@ int Ssw_ClassesPrepareRehash( Ssw_Cla_t * p, Vec_Ptr_t * vCands ) // copy the entries into storage in the topological order nEntries2 = 0; - Vec_PtrForEachEntry( vCands, pObj, i ) + Vec_PtrForEachEntry( Aig_Obj_t *, vCands, pObj, i ) { nNodes = p->pClassSizes[pObj->Id]; // skip the nodes that are not representatives of non-trivial classes @@ -587,7 +590,7 @@ int Ssw_ClassesPrepareRehash( Ssw_Cla_t * p, Vec_Ptr_t * vCands ) SeeAlso [] ***********************************************************************/ -Ssw_Cla_t * Ssw_ClassesPrepare( Aig_Man_t * pAig, int nFramesK, int fLatchCorr, int nMaxLevs, int fVerbose ) +Ssw_Cla_t * Ssw_ClassesPrepare( Aig_Man_t * pAig, int nFramesK, int fLatchCorr, int fOutputCorr, int nMaxLevs, int fVerbose ) { // int nFrames = 4; // int nWords = 1; @@ -622,7 +625,7 @@ if ( fVerbose ) // set comparison procedures clk = clock(); - Ssw_ClassesSetData( p, pSml, Ssw_SmlObjHashWord, Ssw_SmlObjIsConstWord, Ssw_SmlObjsAreEqualWord ); + Ssw_ClassesSetData( p, pSml, (unsigned(*)(void *,Aig_Obj_t *))Ssw_SmlObjHashWord, (int(*)(void *,Aig_Obj_t *))Ssw_SmlObjIsConstWord, (int(*)(void *,Aig_Obj_t *,Aig_Obj_t *))Ssw_SmlObjsAreEqualWord ); // collect nodes to be considered as candidates vCands = Vec_PtrAlloc( 1000 ); @@ -643,6 +646,22 @@ clk = clock(); } Vec_PtrPush( vCands, pObj ); } + + // this change will consider all PO drivers + if ( fOutputCorr ) + { + Vec_PtrClear( vCands ); + Aig_ManForEachObj( p->pAig, pObj, i ) + pObj->fMarkB = 0; + Saig_ManForEachPo( p->pAig, pObj, i ) + if ( Aig_ObjIsCand(Aig_ObjFanin0(pObj)) ) + Aig_ObjFanin0(pObj)->fMarkB = 1; + Aig_ManForEachObj( p->pAig, pObj, i ) + if ( pObj->fMarkB ) + Vec_PtrPush( vCands, pObj ); + Aig_ManForEachObj( p->pAig, pObj, i ) + pObj->fMarkB = 0; + } // allocate room for classes p->pMemClasses = ABC_ALLOC( Aig_Obj_t *, Vec_PtrSize(vCands) ); @@ -730,6 +749,69 @@ Ssw_Cla_t * Ssw_ClassesPrepareSimple( Aig_Man_t * pAig, int fLatchCorr, int nMax return p; } +/**Function************************************************************* + + Synopsis [Creates initial simulation classes.] + + Description [Assumes that simulation info is assigned.] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Ssw_Cla_t * Ssw_ClassesPrepareFromReprs( Aig_Man_t * pAig ) +{ + Ssw_Cla_t * p; + Aig_Obj_t * pObj, * pRepr; + int * pClassSizes, nEntries, i; + // start the classes + p = Ssw_ClassesStart( pAig ); + // allocate memory for classes + p->pMemClasses = ABC_CALLOC( Aig_Obj_t *, Aig_ManObjNumMax(pAig) ); + // count classes + p->nCands1 = 0; + Aig_ManForEachObj( pAig, pObj, i ) + { + if ( Ssw_ObjIsConst1Cand(pAig, pObj) ) + { + p->nCands1++; + continue; + } + if ( (pRepr = Aig_ObjRepr(pAig, pObj)) ) + { + if ( p->pClassSizes[pRepr->Id]++ == 0 ) + p->pClassSizes[pRepr->Id]++; + } + } + // add nodes + nEntries = 0; + p->nClasses = 0; + pClassSizes = ABC_CALLOC( int, Aig_ManObjNumMax(pAig) ); + Aig_ManForEachObj( pAig, pObj, i ) + { + if ( p->pClassSizes[i] ) + { + p->pId2Class[i] = p->pMemClasses + nEntries; + nEntries += p->pClassSizes[i]; + p->pId2Class[i][pClassSizes[i]++] = pObj; + p->nClasses++; + continue; + } + if ( Ssw_ObjIsConst1Cand(pAig, pObj) ) + continue; + if ( (pRepr = Aig_ObjRepr(pAig, pObj)) ) + p->pId2Class[pRepr->Id][pClassSizes[pRepr->Id]++] = pObj; + } + p->pMemClassesFree = p->pMemClasses + nEntries; + p->nLits = nEntries - p->nClasses; + assert( memcmp(pClassSizes, p->pClassSizes, sizeof(int)*Aig_ManObjNumMax(pAig)) == 0 ); + ABC_FREE( pClassSizes ); +// printf( "After converting:\n" ); +// Ssw_ClassesPrint( p, 0 ); + return p; +} + /**Function************************************************************* Synopsis [Creates initial simulation classes.] @@ -902,20 +984,20 @@ int Ssw_ClassesRefineOneClass( Ssw_Cla_t * p, Aig_Obj_t * pReprOld, int fRecursi // Vec_PtrPush( p->vRefined, pObj ); // get the new representative - pReprNew = Vec_PtrEntry( p->vClassNew, 0 ); + pReprNew = (Aig_Obj_t *)Vec_PtrEntry( p->vClassNew, 0 ); assert( Vec_PtrSize(p->vClassOld) > 0 ); assert( Vec_PtrSize(p->vClassNew) > 0 ); // create old class pClassOld = Ssw_ObjRemoveClass( p, pReprOld ); - Vec_PtrForEachEntry( p->vClassOld, pObj, i ) + Vec_PtrForEachEntry( Aig_Obj_t *, p->vClassOld, pObj, i ) { pClassOld[i] = pObj; Aig_ObjSetRepr( p->pAig, pObj, i? pReprOld : NULL ); } // create new class pClassNew = pClassOld + i; - Vec_PtrForEachEntry( p->vClassNew, pObj, i ) + Vec_PtrForEachEntry( Aig_Obj_t *, p->vClassNew, pObj, i ) { pClassNew[i] = pObj; Aig_ObjSetRepr( p->pAig, pObj, i? pReprNew : NULL ); @@ -972,21 +1054,21 @@ int Ssw_ClassesRefineConst1Group( Ssw_Cla_t * p, Vec_Ptr_t * vRoots, int fRecurs return 0; // collect the nodes to be refined Vec_PtrClear( p->vClassNew ); - Vec_PtrForEachEntry( vRoots, pObj, i ) + Vec_PtrForEachEntry( Aig_Obj_t *, vRoots, pObj, i ) if ( !p->pFuncNodeIsConst( p->pManData, pObj ) ) Vec_PtrPush( p->vClassNew, pObj ); // check if there is a new class if ( Vec_PtrSize(p->vClassNew) == 0 ) return 0; p->nCands1 -= Vec_PtrSize(p->vClassNew); - pReprNew = Vec_PtrEntry( p->vClassNew, 0 ); + pReprNew = (Aig_Obj_t *)Vec_PtrEntry( p->vClassNew, 0 ); Aig_ObjSetRepr( p->pAig, pReprNew, NULL ); if ( Vec_PtrSize(p->vClassNew) == 1 ) return 1; // create a new class composed of these nodes ppClassNew = p->pMemClassesFree; p->pMemClassesFree += Vec_PtrSize(p->vClassNew); - Vec_PtrForEachEntry( p->vClassNew, pObj, i ) + Vec_PtrForEachEntry( Aig_Obj_t *, p->vClassNew, pObj, i ) { ppClassNew[i] = pObj; Aig_ObjSetRepr( p->pAig, pObj, i? pReprNew : NULL ); @@ -1029,14 +1111,14 @@ int Ssw_ClassesRefineConst1( Ssw_Cla_t * p, int fRecursive ) if ( Vec_PtrSize(p->vClassNew) == 0 ) return 0; p->nCands1 -= Vec_PtrSize(p->vClassNew); - pReprNew = Vec_PtrEntry( p->vClassNew, 0 ); + pReprNew = (Aig_Obj_t *)Vec_PtrEntry( p->vClassNew, 0 ); Aig_ObjSetRepr( p->pAig, pReprNew, NULL ); if ( Vec_PtrSize(p->vClassNew) == 1 ) return 1; // create a new class composed of these nodes ppClassNew = p->pMemClassesFree; p->pMemClassesFree += Vec_PtrSize(p->vClassNew); - Vec_PtrForEachEntry( p->vClassNew, pObj, i ) + Vec_PtrForEachEntry( Aig_Obj_t *, p->vClassNew, pObj, i ) { ppClassNew[i] = pObj; Aig_ObjSetRepr( p->pAig, pObj, i? pReprNew : NULL ); @@ -1054,3 +1136,5 @@ int Ssw_ClassesRefineConst1( Ssw_Cla_t * p, int fRecursive ) //////////////////////////////////////////////////////////////////////// +ABC_NAMESPACE_IMPL_END + diff --git a/src/aig/ssw/sswCnf.c b/src/aig/ssw/sswCnf.c index 73fa0b02..1970c62f 100644 --- a/src/aig/ssw/sswCnf.c +++ b/src/aig/ssw/sswCnf.c @@ -20,6 +20,9 @@ #include "sswInt.h" +ABC_NAMESPACE_IMPL_START + + //////////////////////////////////////////////////////////////////////// /// DECLARATIONS /// //////////////////////////////////////////////////////////////////////// @@ -228,7 +231,7 @@ void Ssw_AddClausesSuper( Ssw_Sat_t * p, Aig_Obj_t * pNode, Vec_Ptr_t * vSuper ) pLits = ABC_ALLOC( int, nLits ); // suppose AND-gate is A & B = C // add !A => !C or A + !C - Vec_PtrForEachEntry( vSuper, pFanin, i ) + Vec_PtrForEachEntry( Aig_Obj_t *, vSuper, pFanin, i ) { pLits[0] = toLitCond(Ssw_ObjSatNum(p,Aig_Regular(pFanin)), Aig_IsComplement(pFanin)); pLits[1] = toLitCond(Ssw_ObjSatNum(p,pNode), 1); @@ -241,7 +244,7 @@ void Ssw_AddClausesSuper( Ssw_Sat_t * p, Aig_Obj_t * pNode, Vec_Ptr_t * vSuper ) assert( RetValue ); } // add A & B => C or !A + !B + C - Vec_PtrForEachEntry( vSuper, pFanin, i ) + Vec_PtrForEachEntry( Aig_Obj_t *, vSuper, pFanin, i ) { pLits[i] = toLitCond(Ssw_ObjSatNum(p,Aig_Regular(pFanin)), !Aig_IsComplement(pFanin)); if ( p->fPolarFlip ) @@ -357,7 +360,7 @@ void Ssw_CnfNodeAddToSolver( Ssw_Sat_t * p, Aig_Obj_t * pObj ) vFrontier = Vec_PtrAlloc( 100 ); Ssw_ObjAddToFrontier( p, pObj, vFrontier ); // explore nodes in the frontier - Vec_PtrForEachEntry( vFrontier, pNode, i ) + Vec_PtrForEachEntry( Aig_Obj_t *, vFrontier, pNode, i ) { // create the supergate assert( Ssw_ObjSatNum(p,pNode) ); @@ -368,14 +371,14 @@ void Ssw_CnfNodeAddToSolver( Ssw_Sat_t * p, Aig_Obj_t * pObj ) Vec_PtrPushUnique( p->vFanins, Aig_ObjFanin0( Aig_ObjFanin1(pNode) ) ); Vec_PtrPushUnique( p->vFanins, Aig_ObjFanin1( Aig_ObjFanin0(pNode) ) ); Vec_PtrPushUnique( p->vFanins, Aig_ObjFanin1( Aig_ObjFanin1(pNode) ) ); - Vec_PtrForEachEntry( p->vFanins, pFanin, k ) + Vec_PtrForEachEntry( Aig_Obj_t *, p->vFanins, pFanin, k ) Ssw_ObjAddToFrontier( p, Aig_Regular(pFanin), vFrontier ); Ssw_AddClausesMux( p, pNode ); } else { Ssw_CollectSuper( pNode, fUseMuxes, p->vFanins ); - Vec_PtrForEachEntry( p->vFanins, pFanin, k ) + Vec_PtrForEachEntry( Aig_Obj_t *, p->vFanins, pFanin, k ) Ssw_ObjAddToFrontier( p, Aig_Regular(pFanin), vFrontier ); Ssw_AddClausesSuper( p, pNode, p->vFanins ); } @@ -421,3 +424,5 @@ int Ssw_CnfGetNodeValue( Ssw_Sat_t * p, Aig_Obj_t * pObj ) //////////////////////////////////////////////////////////////////////// +ABC_NAMESPACE_IMPL_END + diff --git a/src/aig/ssw/sswConstr.c b/src/aig/ssw/sswConstr.c new file mode 100644 index 00000000..e233f133 --- /dev/null +++ b/src/aig/ssw/sswConstr.c @@ -0,0 +1,635 @@ +/**CFile**************************************************************** + + FileName [sswConstr.c] + + SystemName [ABC: Logic synthesis and verification system.] + + PackageName [Inductive prover with constraints.] + + Synopsis [One round of SAT sweeping.] + + Author [Alan Mishchenko] + + Affiliation [UC Berkeley] + + Date [Ver. 1.0. Started - September 1, 2008.] + + Revision [$Id: sswConstr.c,v 1.00 2008/09/01 00:00:00 alanmi Exp $] + +***********************************************************************/ + +#include "sswInt.h" +#include "cnf.h" +#include "bar.h" + +ABC_NAMESPACE_IMPL_START + + +//////////////////////////////////////////////////////////////////////// +/// DECLARATIONS /// +//////////////////////////////////////////////////////////////////////// + +//////////////////////////////////////////////////////////////////////// +/// FUNCTION DEFINITIONS /// +//////////////////////////////////////////////////////////////////////// + +/**Function************************************************************* + + Synopsis [Constructs initialized timeframes with constraints as POs.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Aig_Man_t * Ssw_FramesWithConstraints( Aig_Man_t * p, int nFrames ) +{ + Aig_Man_t * pFrames; + Aig_Obj_t * pObj, * pObjLi, * pObjLo; + int i, f; + assert( Saig_ManConstrNum(p) > 0 ); + assert( Aig_ManRegNum(p) > 0 ); + assert( Aig_ManRegNum(p) < Aig_ManPiNum(p) ); + // start the fraig package + pFrames = Aig_ManStart( Aig_ManObjNumMax(p) * nFrames ); + // create latches for the first frame + Saig_ManForEachLo( p, pObj, i ) + Aig_ObjSetCopy( pObj, Aig_ManConst0(pFrames) ); + // add timeframes + for ( f = 0; f < nFrames; f++ ) + { + // map constants and PIs + Aig_ObjSetCopy( Aig_ManConst1(p), Aig_ManConst1(pFrames) ); + Saig_ManForEachPi( p, pObj, i ) + Aig_ObjSetCopy( pObj, Aig_ObjCreatePi(pFrames) ); + // add internal nodes of this frame + Aig_ManForEachNode( p, pObj, i ) + Aig_ObjSetCopy( pObj, Aig_And( pFrames, Aig_ObjChild0Copy(pObj), Aig_ObjChild1Copy(pObj) ) ); + // transfer to the primary output + Aig_ManForEachPo( p, pObj, i ) + Aig_ObjSetCopy( pObj, Aig_ObjChild0Copy(pObj) ); + // create constraint outputs + Saig_ManForEachPo( p, pObj, i ) + { + if ( i < Saig_ManPoNum(p) - Saig_ManConstrNum(p) ) + continue; + Aig_ObjCreatePo( pFrames, Aig_Not( Aig_ObjCopy(pObj) ) ); + } + // transfer latch inputs to the latch outputs + Saig_ManForEachLiLo( p, pObjLi, pObjLo, i ) + Aig_ObjSetCopy( pObjLo, Aig_ObjCopy(pObjLi) ); + } + // remove dangling nodes + Aig_ManCleanup( pFrames ); + return pFrames; +} + +/**Function************************************************************* + + Synopsis [Finds one satisfiable assignment of the timeframes.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Ssw_ManSetConstrPhases( Aig_Man_t * p, int nFrames, Vec_Int_t ** pvInits ) +{ + Aig_Man_t * pFrames; + sat_solver * pSat; + Cnf_Dat_t * pCnf; + Aig_Obj_t * pObj; + int i, RetValue; + if ( pvInits ) + *pvInits = NULL; + assert( p->nConstrs > 0 ); + // derive the timeframes + pFrames = Ssw_FramesWithConstraints( p, nFrames ); + // create CNF + pCnf = Cnf_Derive( pFrames, 0 ); + // create SAT solver + pSat = (sat_solver *)Cnf_DataWriteIntoSolver( pCnf, 1, 0 ); + if ( pSat == NULL ) + { + Cnf_DataFree( pCnf ); + Aig_ManStop( pFrames ); + return 1; + } + // solve + RetValue = sat_solver_solve( pSat, NULL, NULL, + (ABC_INT64_T)1000000, (ABC_INT64_T)0, (ABC_INT64_T)0, (ABC_INT64_T)0 ); + if ( RetValue == l_True && pvInits ) + { + *pvInits = Vec_IntAlloc( 1000 ); + Aig_ManForEachPi( pFrames, pObj, i ) + Vec_IntPush( *pvInits, sat_solver_var_value(pSat, pCnf->pVarNums[Aig_ObjId(pObj)]) ); + +// Aig_ManForEachPi( pFrames, pObj, i ) +// printf( "%d", Vec_IntEntry(*pvInits, i) ); +// printf( "\n" ); + } + sat_solver_delete( pSat ); + Cnf_DataFree( pCnf ); + Aig_ManStop( pFrames ); + if ( RetValue == l_False ) + return 1; + if ( RetValue == l_True ) + return 0; + return -1; +} + +/**Function************************************************************* + + Synopsis [Performs fraiging for one node.] + + Description [Returns the fraiged node.] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Ssw_ManSetConstrPhases_( Aig_Man_t * p, int nFrames, Vec_Int_t ** pvInits ) +{ + Vec_Int_t * vLits; + sat_solver * pSat; + Cnf_Dat_t * pCnf; + Aig_Obj_t * pObj; + int i, f, iVar, RetValue, nRegs; + if ( pvInits ) + *pvInits = NULL; + assert( p->nConstrs > 0 ); + // create CNF + nRegs = p->nRegs; p->nRegs = 0; + pCnf = Cnf_Derive( p, Aig_ManPoNum(p) ); + p->nRegs = nRegs; + // create SAT solver + pSat = (sat_solver *)Cnf_DataWriteIntoSolver( pCnf, nFrames, 0 ); + assert( pSat->size == nFrames * pCnf->nVars ); + // collect constraint literals + vLits = Vec_IntAlloc( 100 ); + Saig_ManForEachLo( p, pObj, i ) + { + assert( pCnf->pVarNums[Aig_ObjId(pObj)] >= 0 ); + Vec_IntPush( vLits, toLitCond(pCnf->pVarNums[Aig_ObjId(pObj)], 1) ); + } + for ( f = 0; f < nFrames; f++ ) + { + Saig_ManForEachPo( p, pObj, i ) + { + if ( i < Saig_ManPoNum(p) - Saig_ManConstrNum(p) ) + continue; + assert( pCnf->pVarNums[Aig_ObjId(pObj)] >= 0 ); + iVar = pCnf->pVarNums[Aig_ObjId(pObj)] + pCnf->nVars*f; + Vec_IntPush( vLits, toLitCond(iVar, 1) ); + } + } + RetValue = sat_solver_solve( pSat, (int *)Vec_IntArray(vLits), + (int *)Vec_IntArray(vLits) + Vec_IntSize(vLits), + (ABC_INT64_T)1000000, (ABC_INT64_T)0, (ABC_INT64_T)0, (ABC_INT64_T)0 ); + if ( RetValue == l_True && pvInits ) + { + *pvInits = Vec_IntAlloc( 1000 ); + for ( f = 0; f < nFrames; f++ ) + { + Saig_ManForEachPi( p, pObj, i ) + { + iVar = pCnf->pVarNums[Aig_ObjId(pObj)] + pCnf->nVars*f; + Vec_IntPush( *pvInits, sat_solver_var_value(pSat, iVar) ); + } + } + } + sat_solver_delete( pSat ); + Vec_IntFree( vLits ); + Cnf_DataFree( pCnf ); + if ( RetValue == l_False ) + return 1; + if ( RetValue == l_True ) + return 0; + return -1; +} + +/**Function************************************************************* + + Synopsis [Performs fraiging for one node.] + + Description [Returns the fraiged node.] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Ssw_ManPrintPolarity( Aig_Man_t * p ) +{ + Aig_Obj_t * pObj; + int i; + Aig_ManForEachObj( p, pObj, i ) + printf( "%d", pObj->fPhase ); + printf( "\n" ); +} + +/**Function************************************************************* + + Synopsis [Performs fraiging for one node.] + + Description [Returns the fraiged node.] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Ssw_ManRefineByConstrSim( Ssw_Man_t * p ) +{ + Aig_Obj_t * pObj, * pObjLi; + int f, i, iLits, RetValue1, RetValue2; + int nFrames = Vec_IntSize(p->vInits) / Saig_ManPiNum(p->pAig); + assert( Vec_IntSize(p->vInits) % Saig_ManPiNum(p->pAig) == 0 ); + // assign register outputs + Saig_ManForEachLi( p->pAig, pObj, i ) + pObj->fMarkB = 0; + // simulate the timeframes + iLits = 0; + for ( f = 0; f < nFrames; f++ ) + { + // set the PI simulation information + Aig_ManConst1(p->pAig)->fMarkB = 1; + Saig_ManForEachPi( p->pAig, pObj, i ) + pObj->fMarkB = Vec_IntEntry( p->vInits, iLits++ ); + Saig_ManForEachLiLo( p->pAig, pObjLi, pObj, i ) + pObj->fMarkB = pObjLi->fMarkB; + // simulate internal nodes + Aig_ManForEachNode( p->pAig, pObj, i ) + pObj->fMarkB = ( Aig_ObjFanin0(pObj)->fMarkB ^ Aig_ObjFaninC0(pObj) ) + & ( Aig_ObjFanin1(pObj)->fMarkB ^ Aig_ObjFaninC1(pObj) ); + // assign the COs + Aig_ManForEachPo( p->pAig, pObj, i ) + pObj->fMarkB = ( Aig_ObjFanin0(pObj)->fMarkB ^ Aig_ObjFaninC0(pObj) ); + // check the outputs + Saig_ManForEachPo( p->pAig, pObj, i ) + { + if ( i < Saig_ManPoNum(p->pAig) - Saig_ManConstrNum(p->pAig) ) + { + if ( pObj->fMarkB ) + printf( "output %d failed in frame %d.\n", i, f ); + } + else + { + if ( pObj->fMarkB ) + printf( "constraint %d failed in frame %d.\n", i, f ); + } + } + // transfer + if ( f == 0 ) + { // copy markB into phase + Aig_ManForEachObj( p->pAig, pObj, i ) + pObj->fPhase = pObj->fMarkB; + } + else + { // refine classes + RetValue1 = Ssw_ClassesRefineConst1( p->ppClasses, 0 ); + RetValue2 = Ssw_ClassesRefine( p->ppClasses, 0 ); + } + } + assert( iLits == Vec_IntSize(p->vInits) ); +} + + +/**Function************************************************************* + + Synopsis [Performs fraiging for one node.] + + Description [Returns the fraiged node.] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Ssw_ManSweepNodeConstr( Ssw_Man_t * p, Aig_Obj_t * pObj, int f, int fBmc ) +{ + Aig_Obj_t * pObjRepr, * pObjFraig, * pObjFraig2, * pObjReprFraig; + int RetValue; + // get representative of this class + pObjRepr = Aig_ObjRepr( p->pAig, pObj ); + if ( pObjRepr == NULL ) + return 0; + // get the fraiged node + pObjFraig = Ssw_ObjFrame( p, pObj, f ); + // get the fraiged representative + pObjReprFraig = Ssw_ObjFrame( p, pObjRepr, f ); + // check if constant 0 pattern distinquishes these nodes + assert( pObjFraig != NULL && pObjReprFraig != NULL ); + assert( (pObj->fPhase == pObjRepr->fPhase) == (Aig_ObjPhaseReal(pObjFraig) == Aig_ObjPhaseReal(pObjReprFraig)) ); + // if the fraiged nodes are the same, return + if ( Aig_Regular(pObjFraig) == Aig_Regular(pObjReprFraig) ) + return 0; + // call equivalence checking + 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_ObjSetFrame( p, pObj, f, pObjFraig2 ); + return 0; + } + if ( RetValue == -1 ) // timed out + { + Ssw_ClassesRemoveNode( p->ppClasses, pObj ); + return 1; + } + // disproved equivalence + Ssw_SmlSavePatternAig( p, f ); + Ssw_ManResimulateBit( p, pObj, pObjRepr ); + assert( Aig_ObjRepr( p->pAig, pObj ) != pObjRepr ); + if ( Aig_ObjRepr( p->pAig, pObj ) == pObjRepr ) + { + printf( "Ssw_ManSweepNodeConstr(): Failed to refine representative.\n" ); + } + return 1; +} + +/**Function************************************************************* + + Synopsis [Performs fraiging for the internal nodes.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Aig_Obj_t * Ssw_ManSweepBmcConstr_rec( Ssw_Man_t * p, Aig_Obj_t * pObj, int f ) +{ + Aig_Obj_t * pObjNew, * pObjLi; + pObjNew = Ssw_ObjFrame( p, pObj, f ); + if ( pObjNew ) + return pObjNew; + assert( !Saig_ObjIsPi(p->pAig, pObj) ); + if ( Saig_ObjIsLo(p->pAig, pObj) ) + { + assert( f > 0 ); + pObjLi = Saig_ObjLoToLi( p->pAig, pObj ); + pObjNew = Ssw_ManSweepBmcConstr_rec( p, Aig_ObjFanin0(pObjLi), f-1 ); + pObjNew = Aig_NotCond( pObjNew, Aig_ObjFaninC0(pObjLi) ); + } + else + { + assert( Aig_ObjIsNode(pObj) ); + Ssw_ManSweepBmcConstr_rec( p, Aig_ObjFanin0(pObj), f ); + Ssw_ManSweepBmcConstr_rec( p, Aig_ObjFanin1(pObj), f ); + pObjNew = Aig_And( p->pFrames, Ssw_ObjChild0Fra(p, pObj, f), Ssw_ObjChild1Fra(p, pObj, f) ); + } + Ssw_ObjSetFrame( p, pObj, f, pObjNew ); + assert( pObjNew != NULL ); + return pObjNew; +} + +/**Function************************************************************* + + Synopsis [Performs fraiging for the internal nodes.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Ssw_ManSweepBmcConstr( Ssw_Man_t * p ) +{ + Bar_Progress_t * pProgress = NULL; + Aig_Obj_t * pObj, * pObjNew, * pObjLi, * pObjLo; + int i, f, iLits, clk; +clk = clock(); + + // start initialized timeframes + p->pFrames = Aig_ManStart( Aig_ManObjNumMax(p->pAig) * p->pPars->nFramesK ); + Saig_ManForEachLo( p->pAig, pObj, i ) + Ssw_ObjSetFrame( p, pObj, 0, Aig_ManConst0(p->pFrames) ); + + // build the constraint outputs + iLits = 0; + for ( f = 0; f < p->pPars->nFramesK; f++ ) + { + // map constants and PIs + Ssw_ObjSetFrame( p, Aig_ManConst1(p->pAig), f, Aig_ManConst1(p->pFrames) ); + Saig_ManForEachPi( p->pAig, pObj, i ) + { + pObjNew = Aig_ObjCreatePi(p->pFrames); + pObjNew->fPhase = Vec_IntEntry( p->vInits, iLits++ ); + Ssw_ObjSetFrame( p, pObj, f, pObjNew ); + } + // build the constraint cones + Saig_ManForEachPo( p->pAig, pObj, i ) + { + if ( i < Saig_ManPoNum(p->pAig) - Saig_ManConstrNum(p->pAig) ) + continue; + pObjNew = Ssw_ManSweepBmcConstr_rec( p, Aig_ObjFanin0(pObj), f ); + pObjNew = Aig_NotCond( pObjNew, Aig_ObjFaninC0(pObj) ); + if ( Aig_Regular(pObjNew) == Aig_ManConst1(p->pFrames) ) + { + assert( Aig_IsComplement(pObjNew) ); + continue; + } + Ssw_NodesAreConstrained( p, pObjNew, Aig_ManConst0(p->pFrames) ); + } + } + assert( Vec_IntSize(p->vInits) == iLits + Saig_ManPiNum(p->pAig) ); + + // sweep internal nodes + p->fRefined = 0; + if ( p->pPars->fVerbose ) + pProgress = Bar_ProgressStart( stdout, Aig_ManObjNumMax(p->pAig) * p->pPars->nFramesK ); + for ( f = 0; f < p->pPars->nFramesK; f++ ) + { + // sweep internal nodes + Aig_ManForEachNode( p->pAig, pObj, i ) + { + if ( p->pPars->fVerbose ) + 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_ObjSetFrame( p, pObj, f, pObjNew ); + p->fRefined |= Ssw_ManSweepNodeConstr( p, pObj, f, 1 ); + } + // quit if this is the last timeframe + if ( f == p->pPars->nFramesK - 1 ) + break; + // transfer latch input to the latch outputs + Aig_ManForEachPo( p->pAig, pObj, i ) + Ssw_ObjSetFrame( p, pObj, f, Ssw_ObjChild0Fra(p, pObj, f) ); + // build logic cones for register outputs + Saig_ManForEachLiLo( p->pAig, pObjLi, pObjLo, i ) + { + pObjNew = Ssw_ObjFrame( p, pObjLi, f ); + Ssw_ObjSetFrame( p, pObjLo, f+1, pObjNew ); + Ssw_CnfNodeAddToSolver( p->pMSat, Aig_Regular(pObjNew) );// + } + } + if ( p->pPars->fVerbose ) + Bar_ProgressStop( pProgress ); + + // cleanup +// Ssw_ClassesCheck( p->ppClasses ); +p->timeBmc += clock() - clk; + return p->fRefined; +} + + + + +/**Function************************************************************* + + Synopsis [Performs fraiging for the internal nodes.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Aig_Obj_t * Ssw_FramesWithClasses_rec( Ssw_Man_t * p, Aig_Obj_t * pObj, int f ) +{ + Aig_Obj_t * pObjNew, * pObjLi; + pObjNew = Ssw_ObjFrame( p, pObj, f ); + if ( pObjNew ) + return pObjNew; + assert( !Saig_ObjIsPi(p->pAig, pObj) ); + if ( Saig_ObjIsLo(p->pAig, pObj) ) + { + assert( f > 0 ); + pObjLi = Saig_ObjLoToLi( p->pAig, pObj ); + pObjNew = Ssw_FramesWithClasses_rec( p, Aig_ObjFanin0(pObjLi), f-1 ); + pObjNew = Aig_NotCond( pObjNew, Aig_ObjFaninC0(pObjLi) ); + } + else + { + assert( Aig_ObjIsNode(pObj) ); + Ssw_FramesWithClasses_rec( p, Aig_ObjFanin0(pObj), f ); + Ssw_FramesWithClasses_rec( p, Aig_ObjFanin1(pObj), f ); + pObjNew = Aig_And( p->pFrames, Ssw_ObjChild0Fra(p, pObj, f), Ssw_ObjChild1Fra(p, pObj, f) ); + } + Ssw_ObjSetFrame( p, pObj, f, pObjNew ); + assert( pObjNew != NULL ); + return pObjNew; +} + + +/**Function************************************************************* + + Synopsis [Performs fraiging for the internal nodes.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Ssw_ManSweepConstr( Ssw_Man_t * p ) +{ + Bar_Progress_t * pProgress = NULL; + Aig_Obj_t * pObj, * pObj2, * pObjNew; + int nConstrPairs, clk, i, f, iLits; +//Ssw_ManPrintPolarity( p->pAig ); + + // perform speculative reduction +clk = clock(); + // create timeframes + p->pFrames = Ssw_FramesWithClasses( p ); + // add constants + nConstrPairs = Aig_ManPoNum(p->pFrames)-Aig_ManRegNum(p->pAig); + assert( (nConstrPairs & 1) == 0 ); + for ( i = 0; i < nConstrPairs; i += 2 ) + { + pObj = Aig_ManPo( p->pFrames, i ); + pObj2 = Aig_ManPo( p->pFrames, i+1 ); + Ssw_NodesAreConstrained( p, Aig_ObjChild0(pObj), Aig_ObjChild0(pObj2) ); + } + // build logic cones for register inputs + for ( i = 0; i < Aig_ManRegNum(p->pAig); i++ ) + { + pObj = Aig_ManPo( p->pFrames, nConstrPairs + i ); + Ssw_CnfNodeAddToSolver( p->pMSat, Aig_ObjFanin0(pObj) );// + } + + // map constants and PIs of the last frame + f = p->pPars->nFramesK; +// iLits = 0; + iLits = f * Saig_ManPiNum(p->pAig); + Ssw_ObjSetFrame( p, Aig_ManConst1(p->pAig), f, Aig_ManConst1(p->pFrames) ); + Saig_ManForEachPi( p->pAig, pObj, i ) + { + pObjNew = Aig_ObjCreatePi(p->pFrames); + pObjNew->fPhase = (p->vInits != NULL) && Vec_IntEntry(p->vInits, iLits++); + Ssw_ObjSetFrame( p, pObj, f, pObjNew ); + } + assert( Vec_IntSize(p->vInits) == iLits ); +p->timeReduce += clock() - clk; + + // add constraints to all timeframes + for ( f = 0; f <= p->pPars->nFramesK; f++ ) + { + Saig_ManForEachPo( p->pAig, pObj, i ) + { + if ( i < Saig_ManPoNum(p->pAig) - Saig_ManConstrNum(p->pAig) ) + continue; + Ssw_FramesWithClasses_rec( p, Aig_ObjFanin0(pObj), f ); +// if ( Aig_Regular(Ssw_ObjChild0Fra(p,pObj,f)) == Aig_ManConst1(p->pFrames) ) + if ( Ssw_ObjChild0Fra(p,pObj,f) == Aig_ManConst0(p->pFrames) ) + continue; + assert( Ssw_ObjChild0Fra(p,pObj,f) != Aig_ManConst1(p->pFrames) ); + if ( Ssw_ObjChild0Fra(p,pObj,f) == Aig_ManConst1(p->pFrames) ) + { + printf( "Polarity violation.\n" ); + continue; + } + Ssw_NodesAreConstrained( p, Ssw_ObjChild0Fra(p,pObj,f), Aig_ManConst0(p->pFrames) ); + } + } + f = p->pPars->nFramesK; + // clean the solver + sat_solver_simplify( p->pMSat->pSat ); + + + // sweep internal nodes + p->fRefined = 0; + Ssw_ClassesClearRefined( p->ppClasses ); + if ( p->pPars->fVerbose ) + pProgress = Bar_ProgressStart( stdout, Aig_ManObjNumMax(p->pAig) ); + Aig_ManForEachObj( p->pAig, pObj, i ) + { + if ( p->pPars->fVerbose ) + Bar_ProgressUpdate( pProgress, i, NULL ); + if ( Saig_ObjIsLo(p->pAig, pObj) ) + p->fRefined |= Ssw_ManSweepNodeConstr( p, pObj, f, 0 ); + else if ( Aig_ObjIsNode(pObj) ) + { + pObjNew = Aig_And( p->pFrames, Ssw_ObjChild0Fra(p, pObj, f), Ssw_ObjChild1Fra(p, pObj, f) ); + Ssw_ObjSetFrame( p, pObj, f, pObjNew ); + p->fRefined |= Ssw_ManSweepNodeConstr( p, pObj, f, 0 ); + } + } + if ( p->pPars->fVerbose ) + Bar_ProgressStop( pProgress ); + // cleanup +// Ssw_ClassesCheck( p->ppClasses ); + return p->fRefined; +} + +//////////////////////////////////////////////////////////////////////// +/// END OF FILE /// +//////////////////////////////////////////////////////////////////////// + + +ABC_NAMESPACE_IMPL_END + diff --git a/src/aig/ssw/sswCore.c b/src/aig/ssw/sswCore.c index 6cb84800..c277d76e 100644 --- a/src/aig/ssw/sswCore.c +++ b/src/aig/ssw/sswCore.c @@ -20,6 +20,9 @@ #include "sswInt.h" +ABC_NAMESPACE_IMPL_START + + //////////////////////////////////////////////////////////////////////// /// DECLARATIONS /// //////////////////////////////////////////////////////////////////////// @@ -46,16 +49,18 @@ void Ssw_ManSetDefaultParams( Ssw_Pars_t * p ) 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->fConstrs = 0; // treat the last nConstrs POs as seq constraints + p->fMergeFull = 0; // enables full merge when constraints are used p->nBTLimit = 1000; // conflict limit at a node p->nBTLimitGlobal = 5000000; // conflict limit for all runs p->nMinDomSize = 100; // min clock domain considered for optimization p->nItersStop = -1; // stop after the given number of iterations p->nResimDelta = 1000; // the internal of nodes to resimulate + p->nStepsMax = -1; // (scorr only) the max number of induction steps p->fPolarFlip = 0; // uses polarity adjustment p->fLatchCorr = 0; // performs register correspondence + p->fOutputCorr = 0; // perform 'PO correspondence' p->fSemiFormal = 0; // enable semiformal filtering - p->fUniqueness = 0; // enable uniqueness constraints p->fDynamic = 0; // dynamic partitioning p->fLocalSim = 0; // local simulation p->fVerbose = 0; // verbose stats @@ -88,6 +93,130 @@ void Ssw_ManSetDefaultParamsLcorr( Ssw_Pars_t * p ) p->nBTLimit = 10000; } +/**Function************************************************************* + + Synopsis [Reports improvements for property cones.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Ssw_ReportConeReductions( Ssw_Man_t * p, Aig_Man_t * pAigInit, Aig_Man_t * pAigStop ) +{ + Aig_Man_t * pAig1, * pAig2, * pAux; + pAig1 = Aig_ManDupOneOutput( pAigInit, 0, 1 ); + pAig1 = Aig_ManScl( pAux = pAig1, 1, 1, 0 ); + Aig_ManStop( pAux ); + pAig2 = Aig_ManDupOneOutput( pAigStop, 0, 1 ); + pAig2 = Aig_ManScl( pAux = pAig2, 1, 1, 0 ); + Aig_ManStop( pAux ); + + p->nNodesBegC = Aig_ManNodeNum(pAig1); + p->nNodesEndC = Aig_ManNodeNum(pAig2); + p->nRegsBegC = Aig_ManRegNum(pAig1); + p->nRegsEndC = Aig_ManRegNum(pAig2); + + Aig_ManStop( pAig1 ); + Aig_ManStop( pAig2 ); +} + +/**Function************************************************************* + + Synopsis [Reports one node.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Ssw_ReportOneOutput( Aig_Man_t * p, Aig_Obj_t * pObj ) +{ + if ( pObj == Aig_ManConst1(p) ) + printf( "1" ); + else if ( pObj == Aig_ManConst0(p) ) + printf( "0" ); + else + printf( "X" ); +} + +/**Function************************************************************* + + Synopsis [Reports improvements for property cones.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Ssw_ReportOutputs( Aig_Man_t * pAig ) +{ + Aig_Obj_t * pObj; + int i; + Saig_ManForEachPo( pAig, pObj, i ) + { + if ( i < Saig_ManPoNum(pAig)-Saig_ManConstrNum(pAig) ) + printf( "o" ); + else + printf( "c" ); + Ssw_ReportOneOutput( pAig, Aig_ObjChild0(pObj) ); + } + printf( "\n" ); +} + +/**Function************************************************************* + + Synopsis [Remove from-equivs that are in the cone of constraints.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Ssw_ManUpdateEquivs( Ssw_Man_t * p, Aig_Man_t * pAig, int fVerbose ) +{ + Vec_Ptr_t * vCones; + Aig_Obj_t ** pArray; + Aig_Obj_t * pObj; + int i, nTotal = 0, nRemoved = 0; + // collect the nodes in the cone of constraints + pArray = (Aig_Obj_t **)Vec_PtrArray(pAig->vPos); + pArray += Saig_ManPoNum(pAig) - Saig_ManConstrNum(pAig); + vCones = Aig_ManDfsNodes( pAig, pArray, Saig_ManConstrNum(pAig) ); + // remove all the node that are equiv to something and are in the cones + Aig_ManForEachObj( pAig, pObj, i ) + { + if ( !Aig_ObjIsPi(pObj) && !Aig_ObjIsNode(pObj) ) + continue; + if ( pAig->pReprs[i] != NULL ) + nTotal++; + if ( !Aig_ObjIsTravIdCurrent(pAig, pObj) ) + continue; + if ( pAig->pReprs[i] ) + { + if ( p->pPars->fConstrs && !p->pPars->fMergeFull ) + { + pAig->pReprs[i] = NULL; + nRemoved++; + } + } + } + // collect statistics + p->nConesTotal = Aig_ManPiNum(pAig) + Aig_ManNodeNum(pAig); + p->nConesConstr = Vec_PtrSize(vCones); + p->nEquivsTotal = nTotal; + p->nEquivsConstr = nRemoved; + Vec_PtrFree( vCones ); +} + /**Function************************************************************* Synopsis [Performs computation of signal correspondence with constraints.] @@ -118,9 +247,10 @@ Aig_Man_t * Ssw_SignalCorrespondenceRefine( Ssw_Man_t * p ) if ( !p->pPars->fLatchCorr ) { p->pMSat = Ssw_SatStart( 0 ); - Ssw_ManSweepBmc( p ); - if ( p->pPars->nFramesK > 1 && p->pPars->fUniqueness ) - Ssw_UniqueRegisterPairInfo( p ); + if ( p->pPars->fConstrs ) + Ssw_ManSweepBmcConstr( p ); + else + Ssw_ManSweepBmc( p ); Ssw_SatStop( p->pMSat ); p->pMSat = NULL; Ssw_ManCleanup( p ); @@ -142,10 +272,25 @@ Aig_Man_t * Ssw_SignalCorrespondenceRefine( Ssw_Man_t * p ) Aig_ManStop( pSRed ); } */ + if ( p->pPars->pFunc ) + { + ((int (*)(void *))p->pPars->pFunc)( p->pPars->pData ); + ((int (*)(void *))p->pPars->pFunc)( p->pPars->pData ); + } + if ( p->pPars->nStepsMax == 0 ) + { + printf( "Stopped signal correspondence after BMC.\n" ); + goto finalize; + } // refine classes using induction nSatProof = nSatCallsSat = nRecycles = nSatFailsReal = nUniques = 0; for ( nIter = 0; ; nIter++ ) { + if ( p->pPars->nStepsMax == nIter ) + { + printf( "Stopped signal correspondence after %d refiment iterations.\n", nIter ); + goto finalize; + } if ( p->pPars->nItersStop >= 0 && p->pPars->nItersStop == nIter ) { Aig_Man_t * pSRed = Ssw_SpeculativeReduction( p ); @@ -174,19 +319,20 @@ clk = clock(); } else { - if ( p->pPars->fDynamic ) + if ( p->pPars->fConstrs ) + RetValue = Ssw_ManSweepConstr( p ); + else if ( p->pPars->fDynamic ) RetValue = Ssw_ManSweepDyn( p ); else RetValue = Ssw_ManSweep( p ); + p->pPars->nConflicts += p->pMSat->pSat->stats.conflicts; if ( p->pPars->fVerbose ) { printf( "%3d : C =%7d. Cl =%7d. LR =%6d. NR =%6d. ", nIter, Ssw_ClassesCand1Num(p->ppClasses), Ssw_ClassesClassNum(p->ppClasses), p->nConstrReduced, Aig_ManNodeNum(p->pFrames) ); - if ( p->pPars->fUniqueness ) - printf( "U =%4d. ", p->nUniques-nUniques ); - else if ( p->pPars->fDynamic ) + if ( p->pPars->fDynamic ) { printf( "Cex =%5d. ", p->nSatCallsSat-nSatCallsSat ); printf( "R =%4d. ", p->nRecycles-nRecycles ); @@ -211,9 +357,15 @@ clk = clock(); Ssw_ManCleanup( p ); if ( !RetValue ) break; + if ( p->pPars->pFunc ) + ((int (*)(void *))p->pPars->pFunc)( p->pPars->pData ); } + +finalize: p->pPars->nIters = nIter + 1; p->timeTotal = clock() - clkTotal; + + Ssw_ManUpdateEquivs( p, p->pAig, p->pPars->fVerbose ); pAigNew = Aig_ManDupRepr( p->pAig, 0 ); Aig_ManSeqCleanup( pAigNew ); //Ssw_ClassesPrint( p->ppClasses, 1 ); @@ -221,6 +373,9 @@ p->timeTotal = clock() - clkTotal; p->nLitsEnd = Ssw_ClassesLitNum( p->ppClasses ); p->nNodesEnd = Aig_ManNodeNum(pAigNew); p->nRegsEnd = Aig_ManRegNum(pAigNew); + // cleanup + Aig_ManSetPhase( p->pAig ); + Aig_ManCleanMarkB( p->pAig ); return pAigNew; } @@ -255,13 +410,6 @@ Aig_Man_t * Ssw_SignalCorrespondence( Aig_Man_t * pAig, Ssw_Pars_t * pPars ) return Aig_ManDupOrdered(pAig); } // check and update parameters - if ( pPars->fUniqueness ) - { - pPars->nFramesAddSim = 0; - if ( pPars->nFramesK != 2 ) - printf( "Setting K = 2 for uniqueness constraints to work.\n" ); - pPars->nFramesK = 2; - } if ( pPars->fLatchCorrOpt ) { pPars->fLatchCorr = 1; @@ -291,15 +439,31 @@ Aig_Man_t * Ssw_SignalCorrespondence( Aig_Man_t * pAig, Ssw_Pars_t * pPars ) return Cec_SignalCorrespondence( pAig, pPars->nBTLimit, pPars->fUseCSat ); } } - + // start the induction manager p = Ssw_ManCreate( pAig, pPars ); // compute candidate equivalence classes // p->pPars->nConstrs = 1; - if ( p->pPars->nConstrs == 0 ) + if ( p->pPars->fConstrs ) + { + // 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_SmlObjIsConstBit, Ssw_SmlObjsAreEqualBit ); + // derive phase bits to satisfy the constraints + if ( Ssw_ManSetConstrPhases( pAig, p->pPars->nFramesK + 1, &p->vInits ) != 0 ) + { + printf( "Ssw_SignalCorrespondence(): The init state does not satisfy the constraints!\n" ); + p->pPars->fVerbose = 0; + Ssw_ManStop( p ); + return NULL; + } + // perform simulation of the first timeframes + Ssw_ManRefineByConstrSim( p ); + } + else { // perform one round of seq simulation and generate candidate equivalence classes - p->ppClasses = Ssw_ClassesPrepare( pAig, pPars->nFramesK, pPars->fLatchCorr, pPars->nMaxLevs, pPars->fVerbose ); + p->ppClasses = Ssw_ClassesPrepare( pAig, pPars->nFramesK, pPars->fLatchCorr, pPars->fOutputCorr, pPars->nMaxLevs, pPars->fVerbose ); // p->ppClasses = Ssw_ClassesPrepareTargets( pAig ); if ( pPars->fLatchCorrOpt ) p->pSml = Ssw_SmlStart( pAig, 0, 2, 1 ); @@ -307,21 +471,16 @@ Aig_Man_t * Ssw_SignalCorrespondence( Aig_Man_t * pAig, Ssw_Pars_t * pPars ) p->pSml = Ssw_SmlStart( pAig, 0, p->nFrames + p->pPars->nFramesAddSim, 1 ); else p->pSml = Ssw_SmlStart( pAig, 0, 1 + p->pPars->nFramesAddSim, 1 ); - Ssw_ClassesSetData( p->ppClasses, p->pSml, Ssw_SmlObjHashWord, Ssw_SmlObjIsConstWord, Ssw_SmlObjsAreEqualWord ); - } - else - { - // 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_SmlObjIsConstBit, Ssw_SmlObjsAreEqualBit ); + Ssw_ClassesSetData( p->ppClasses, p->pSml, (unsigned(*)(void *,Aig_Obj_t *))Ssw_SmlObjHashWord, (int(*)(void *,Aig_Obj_t *))Ssw_SmlObjIsConstWord, (int(*)(void *,Aig_Obj_t *,Aig_Obj_t *))Ssw_SmlObjsAreEqualWord ); } + // allocate storage if ( p->pPars->fLocalSim ) p->pVisited = ABC_CALLOC( int, Ssw_SmlNumFrames( p->pSml ) * Aig_ManObjNumMax(p->pAig) ); // perform refinement of classes pAigNew = Ssw_SignalCorrespondenceRefine( p ); - if ( pPars->fUniqueness ) - printf( "Uniqueness constraints = %3d. Prevented counter-examples = %3d.\n", - p->nUniquesAdded, p->nUniquesUseful ); +// Ssw_ReportOutputs( pAigNew ); + if ( pPars->fConstrs && pPars->fVerbose ) + Ssw_ReportConeReductions( p, pAig, pAigNew ); // cleanup Ssw_ManStop( p ); return pAigNew; @@ -340,10 +499,14 @@ Aig_Man_t * Ssw_SignalCorrespondence( Aig_Man_t * pAig, Ssw_Pars_t * pPars ) ***********************************************************************/ Aig_Man_t * Ssw_LatchCorrespondence( Aig_Man_t * pAig, Ssw_Pars_t * pPars ) { + Aig_Man_t * pRes; Ssw_Pars_t Pars; if ( pPars == NULL ) Ssw_ManSetDefaultParamsLcorr( pPars = &Pars ); - return Ssw_SignalCorrespondence( pAig, pPars ); + pRes = Ssw_SignalCorrespondence( pAig, pPars ); +// if ( pPars->fConstrs && pPars->fVerbose ) +// Ssw_ReportConeReductions( pAig, pRes ); + return pRes; } @@ -352,3 +515,5 @@ Aig_Man_t * Ssw_LatchCorrespondence( Aig_Man_t * pAig, Ssw_Pars_t * pPars ) //////////////////////////////////////////////////////////////////////// +ABC_NAMESPACE_IMPL_END + diff --git a/src/aig/ssw/sswDyn.c b/src/aig/ssw/sswDyn.c index 04e66f09..7e8edc66 100644 --- a/src/aig/ssw/sswDyn.c +++ b/src/aig/ssw/sswDyn.c @@ -21,6 +21,9 @@ #include "sswInt.h" #include "bar.h" +ABC_NAMESPACE_IMPL_START + + //////////////////////////////////////////////////////////////////////// /// DECLARATIONS /// //////////////////////////////////////////////////////////////////////// @@ -153,7 +156,7 @@ void Ssw_ManLoadSolver( Ssw_Man_t * p, Aig_Obj_t * pRepr, Aig_Obj_t * pObj ) Ssw_ManCollectPis_rec( pRepr, p->vNewLos ); Ssw_ManCollectPis_rec( pObj, p->vNewLos ); // add logic cones for register outputs - Vec_PtrForEachEntry( p->vNewLos, pTemp, i ) + Vec_PtrForEachEntry( Aig_Obj_t *, p->vNewLos, pTemp, i ) { pObj0 = Aig_Regular( Ssw_ObjFrame( p, pTemp, p->pPars->nFramesK ) ); Ssw_CnfNodeAddToSolver( p->pMSat, pObj0 ); @@ -172,7 +175,7 @@ void Ssw_ManLoadSolver( Ssw_Man_t * p, Aig_Obj_t * pRepr, Aig_Obj_t * pObj ) // collect the related constraint POs Vec_IntClear( p->vNewPos ); - Vec_PtrForEachEntry( p->vNewLos, pTemp, i ) + Vec_PtrForEachEntry( Aig_Obj_t *, p->vNewLos, pTemp, i ) Ssw_ManCollectPos_rec( p, pTemp, p->vNewPos ); // check if the corresponding pairs are added Vec_IntForEachEntry( p->vNewPos, iConstr, i ) @@ -222,7 +225,7 @@ void Ssw_ManSweepTransferDyn( Ssw_Man_t * p ) } assert( !Aig_IsComplement(pObjFraig) ); assert( Aig_ObjIsPi(pObjFraig) ); - pInfo = Vec_PtrEntry( p->vSimInfo, Aig_ObjPioNum(pObjFraig) ); + pInfo = (unsigned *)Vec_PtrEntry( p->vSimInfo, Aig_ObjPioNum(pObjFraig) ); Ssw_SmlObjSetWord( p->pSml, pObj, pInfo[0], 0, 0 ); } // set random simulation info for the second frame @@ -233,7 +236,7 @@ void Ssw_ManSweepTransferDyn( Ssw_Man_t * p ) pObjFraig = Ssw_ObjFrame( p, pObj, f ); assert( !Aig_IsComplement(pObjFraig) ); assert( Aig_ObjIsPi(pObjFraig) ); - pInfo = Vec_PtrEntry( p->vSimInfo, Aig_ObjPioNum(pObjFraig) ); + pInfo = (unsigned *)Vec_PtrEntry( p->vSimInfo, Aig_ObjPioNum(pObjFraig) ); Ssw_SmlObjSetWord( p->pSml, pObj, pInfo[0], 0, f ); } } @@ -327,10 +330,10 @@ int Ssw_ManSweepResimulateDynLocal( Ssw_Man_t * p, int f ) // Aig_ManIncrementTravId( p->pAig ); // Aig_ObjIsTravIdCurrent( p->pAig, Aig_ManConst1(p->pAig) ); p->nVisCounter++; - Vec_PtrForEachEntry( p->vResimConsts, pObj, i ) + Vec_PtrForEachEntry( Aig_Obj_t *, p->vResimConsts, pObj, i ) Ssw_SmlSimulateOneDyn_rec( p->pSml, pObj, p->nFrames-1, p->pVisited, p->nVisCounter ); // resimulate the cone of influence of the cand classes - Vec_PtrForEachEntry( p->vResimClasses, pRepr, i ) + Vec_PtrForEachEntry( Aig_Obj_t *, p->vResimClasses, pRepr, i ) { ppClass = Ssw_ClassesReadClass( p->ppClasses, pRepr, &nSize ); for ( k = 0; k < nSize; k++ ) @@ -343,7 +346,7 @@ int Ssw_ManSweepResimulateDynLocal( Ssw_Man_t * p, int f ) // refine these nodes RetValue1 = Ssw_ClassesRefineConst1Group( p->ppClasses, p->vResimConsts, 1 ); RetValue2 = 0; - Vec_PtrForEachEntry( p->vResimClasses, pRepr, i ) + Vec_PtrForEachEntry( Aig_Obj_t *, p->vResimClasses, pRepr, i ) RetValue2 += Ssw_ClassesRefineOneClass( p->ppClasses, pRepr, 1 ); // prepare simulation info for the next round @@ -482,3 +485,5 @@ p->timeReduce += clock() - clk; //////////////////////////////////////////////////////////////////////// +ABC_NAMESPACE_IMPL_END + diff --git a/src/aig/ssw/sswFilter.c b/src/aig/ssw/sswFilter.c new file mode 100644 index 00000000..a0c0934a --- /dev/null +++ b/src/aig/ssw/sswFilter.c @@ -0,0 +1,492 @@ +/**CFile**************************************************************** + + FileName [sswConstr.c] + + SystemName [ABC: Logic synthesis and verification system.] + + PackageName [Inductive prover with constraints.] + + Synopsis [One round of SAT sweeping.] + + Author [Alan Mishchenko] + + Affiliation [UC Berkeley] + + Date [Ver. 1.0. Started - September 1, 2008.] + + Revision [$Id: sswConstr.c,v 1.00 2008/09/01 00:00:00 alanmi Exp $] + +***********************************************************************/ + +#include "sswInt.h" +#include "giaAig.h" + +ABC_NAMESPACE_IMPL_START + + +//////////////////////////////////////////////////////////////////////// +/// DECLARATIONS /// +//////////////////////////////////////////////////////////////////////// + +//////////////////////////////////////////////////////////////////////// +/// FUNCTION DEFINITIONS /// +//////////////////////////////////////////////////////////////////////// + +/**Function************************************************************* + + Synopsis [Performs fraiging for one node.] + + Description [Returns the fraiged node.] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Ssw_ManRefineByFilterSim( Ssw_Man_t * p, int nFrames ) +{ + Aig_Obj_t * pObj, * pObjLi; + int f, i, RetValue1, RetValue2; + assert( nFrames > 0 ); + // assign register outputs + Saig_ManForEachLi( p->pAig, pObj, i ) + pObj->fMarkB = Aig_InfoHasBit( p->pPatWords, Saig_ManPiNum(p->pAig) + i ); + // simulate the timeframes + for ( f = 0; f < nFrames; f++ ) + { + // set the PI simulation information + Aig_ManConst1(p->pAig)->fMarkB = 1; + Saig_ManForEachPi( p->pAig, pObj, i ) + pObj->fMarkB = 0; + Saig_ManForEachLiLo( p->pAig, pObjLi, pObj, i ) + pObj->fMarkB = pObjLi->fMarkB; + // simulate internal nodes + Aig_ManForEachNode( p->pAig, pObj, i ) + pObj->fMarkB = ( Aig_ObjFanin0(pObj)->fMarkB ^ Aig_ObjFaninC0(pObj) ) + & ( Aig_ObjFanin1(pObj)->fMarkB ^ Aig_ObjFaninC1(pObj) ); + // assign the COs + Aig_ManForEachPo( p->pAig, pObj, i ) + pObj->fMarkB = ( Aig_ObjFanin0(pObj)->fMarkB ^ Aig_ObjFaninC0(pObj) ); + // transfer + if ( f == 0 ) + { // copy markB into phase + Aig_ManForEachObj( p->pAig, pObj, i ) + pObj->fPhase = pObj->fMarkB; + } + else + { // refine classes + RetValue1 = Ssw_ClassesRefineConst1( p->ppClasses, 0 ); + RetValue2 = Ssw_ClassesRefine( p->ppClasses, 0 ); + } + } +} + + +/**Function************************************************************* + + Synopsis [Performs fraiging for one node.] + + Description [Returns the fraiged node.] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Ssw_ManRollForward( Ssw_Man_t * p, int nFrames ) +{ + Aig_Obj_t * pObj, * pObjLi; + int f, i; + assert( nFrames > 0 ); + // assign register outputs + Saig_ManForEachLi( p->pAig, pObj, i ) + pObj->fMarkB = Aig_InfoHasBit( p->pPatWords, Saig_ManPiNum(p->pAig) + i ); + // simulate the timeframes + for ( f = 0; f < nFrames; f++ ) + { + // set the PI simulation information + Aig_ManConst1(p->pAig)->fMarkB = 1; + Saig_ManForEachPi( p->pAig, pObj, i ) + pObj->fMarkB = Aig_ManRandom(0) & 1; + Saig_ManForEachLiLo( p->pAig, pObjLi, pObj, i ) + pObj->fMarkB = pObjLi->fMarkB; + // simulate internal nodes + Aig_ManForEachNode( p->pAig, pObj, i ) + pObj->fMarkB = ( Aig_ObjFanin0(pObj)->fMarkB ^ Aig_ObjFaninC0(pObj) ) + & ( Aig_ObjFanin1(pObj)->fMarkB ^ Aig_ObjFaninC1(pObj) ); + // assign the COs + Aig_ManForEachPo( p->pAig, pObj, i ) + pObj->fMarkB = ( Aig_ObjFanin0(pObj)->fMarkB ^ Aig_ObjFaninC0(pObj) ); + } + // record the new pattern + Saig_ManForEachLi( p->pAig, pObj, i ) + if ( pObj->fMarkB ^ Aig_InfoHasBit(p->pPatWords, Saig_ManPiNum(p->pAig) + i) ) + Aig_InfoXorBit( p->pPatWords, Saig_ManPiNum(p->pAig) + i ); +} + +/**Function************************************************************* + + Synopsis [Performs fraiging for one node.] + + Description [Returns the fraiged node.] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Ssw_ManFindStartingState( Ssw_Man_t * p, Abc_Cex_t * pCex ) +{ + Aig_Obj_t * pObj, * pObjLi; + int f, i, iBit; + // assign register outputs + Saig_ManForEachLi( p->pAig, pObj, i ) + pObj->fMarkB = 0; + // simulate the timeframes + iBit = pCex->nRegs; + for ( f = 0; f <= pCex->iFrame; f++ ) + { + // set the PI simulation information + Aig_ManConst1(p->pAig)->fMarkB = 1; + Saig_ManForEachPi( p->pAig, pObj, i ) + pObj->fMarkB = Aig_InfoHasBit( pCex->pData, iBit++ ); + Saig_ManForEachLiLo( p->pAig, pObjLi, pObj, i ) + pObj->fMarkB = pObjLi->fMarkB; + // simulate internal nodes + Aig_ManForEachNode( p->pAig, pObj, i ) + pObj->fMarkB = ( Aig_ObjFanin0(pObj)->fMarkB ^ Aig_ObjFaninC0(pObj) ) + & ( Aig_ObjFanin1(pObj)->fMarkB ^ Aig_ObjFaninC1(pObj) ); + // assign the COs + Aig_ManForEachPo( p->pAig, pObj, i ) + pObj->fMarkB = ( Aig_ObjFanin0(pObj)->fMarkB ^ Aig_ObjFaninC0(pObj) ); + } + assert( iBit == pCex->nBits ); + // check that the output failed as expected -- cannot check because it is not an SRM! +// pObj = Aig_ManPo( p->pAig, pCex->iPo ); +// if ( pObj->fMarkB != 1 ) +// printf( "The counter-example does not refine the output.\n" ); + // record the new pattern + Saig_ManForEachLo( p->pAig, pObj, i ) + if ( pObj->fMarkB ^ Aig_InfoHasBit(p->pPatWords, Saig_ManPiNum(p->pAig) + i) ) + Aig_InfoXorBit( p->pPatWords, Saig_ManPiNum(p->pAig) + i ); +} + +/**Function************************************************************* + + Synopsis [Performs fraiging for one node.] + + Description [Returns the fraiged node.] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Ssw_ManSweepNodeFilter( Ssw_Man_t * p, Aig_Obj_t * pObj, int f ) +{ + Aig_Obj_t * pObjRepr, * pObjFraig, * pObjFraig2, * pObjReprFraig; + int RetValue; + // get representative of this class + pObjRepr = Aig_ObjRepr( p->pAig, pObj ); + if ( pObjRepr == NULL ) + return 0; + // get the fraiged node + pObjFraig = Ssw_ObjFrame( p, pObj, f ); + // get the fraiged representative + pObjReprFraig = Ssw_ObjFrame( p, pObjRepr, f ); + // check if constant 0 pattern distinquishes these nodes + assert( pObjFraig != NULL && pObjReprFraig != NULL ); + assert( (pObj->fPhase == pObjRepr->fPhase) == (Aig_ObjPhaseReal(pObjFraig) == Aig_ObjPhaseReal(pObjReprFraig)) ); + // if the fraiged nodes are the same, return + if ( Aig_Regular(pObjFraig) == Aig_Regular(pObjReprFraig) ) + return 0; + // call equivalence checking + 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_ObjSetFrame( p, pObj, f, pObjFraig2 ); + return 0; + } + if ( RetValue == -1 ) // timed out + { +// Ssw_ClassesRemoveNode( p->ppClasses, pObj ); + return 1; + } + // disproved equivalence + Ssw_SmlSavePatternAig( p, f ); + Ssw_ManResimulateBit( p, pObj, pObjRepr ); + assert( Aig_ObjRepr( p->pAig, pObj ) != pObjRepr ); + if ( Aig_ObjRepr( p->pAig, pObj ) == pObjRepr ) + { + printf( "Ssw_ManSweepNodeFilter(): Failed to refine representative.\n" ); + } + return 0; +} + +/**Function************************************************************* + + Synopsis [Performs fraiging for the internal nodes.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Aig_Obj_t * Ssw_ManSweepBmcFilter_rec( Ssw_Man_t * p, Aig_Obj_t * pObj, int f ) +{ + Aig_Obj_t * pObjNew, * pObjLi; + pObjNew = Ssw_ObjFrame( p, pObj, f ); + if ( pObjNew ) + return pObjNew; + assert( !Saig_ObjIsPi(p->pAig, pObj) ); + if ( Saig_ObjIsLo(p->pAig, pObj) ) + { + assert( f > 0 ); + pObjLi = Saig_ObjLoToLi( p->pAig, pObj ); + pObjNew = Ssw_ManSweepBmcFilter_rec( p, Aig_ObjFanin0(pObjLi), f-1 ); + pObjNew = Aig_NotCond( pObjNew, Aig_ObjFaninC0(pObjLi) ); + } + else + { + assert( Aig_ObjIsNode(pObj) ); + Ssw_ManSweepBmcFilter_rec( p, Aig_ObjFanin0(pObj), f ); + Ssw_ManSweepBmcFilter_rec( p, Aig_ObjFanin1(pObj), f ); + pObjNew = Aig_And( p->pFrames, Ssw_ObjChild0Fra(p, pObj, f), Ssw_ObjChild1Fra(p, pObj, f) ); + } + Ssw_ObjSetFrame( p, pObj, f, pObjNew ); + assert( pObjNew != NULL ); + return pObjNew; +} + +/**Function************************************************************* + + Synopsis [Filter equivalence classes of nodes.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Ssw_ManSweepBmcFilter( Ssw_Man_t * p, int TimeLimit ) +{ + Aig_Obj_t * pObj, * pObjNew, * pObjLi, * pObjLo; + int f, f1, i, clkTotal = clock(); + // start initialized timeframes + p->pFrames = Aig_ManStart( Aig_ManObjNumMax(p->pAig) * p->pPars->nFramesK ); + Saig_ManForEachLo( p->pAig, pObj, i ) + { + if ( Aig_InfoHasBit( p->pPatWords, Saig_ManPiNum(p->pAig) + i ) ) + { + Ssw_ObjSetFrame( p, pObj, 0, Aig_ManConst1(p->pFrames) ); +//printf( "1" ); + } + else + { + Ssw_ObjSetFrame( p, pObj, 0, Aig_ManConst0(p->pFrames) ); +//printf( "0" ); + } + } +//printf( "\n" ); + + // sweep internal nodes + for ( f = 0; f < p->pPars->nFramesK; f++ ) + { + // realloc mapping of timeframes + if ( f == p->nFrames-1 ) + { + Aig_Obj_t ** pNodeToFrames; + pNodeToFrames = ABC_CALLOC( Aig_Obj_t *, Aig_ManObjNumMax(p->pAig) * 2 * p->nFrames ); + for ( f1 = 0; f1 < p->nFrames; f1++ ) + { + Aig_ManForEachObj( p->pAig, pObj, i ) + pNodeToFrames[2*p->nFrames*pObj->Id + f1] = Ssw_ObjFrame( p, pObj, f1 ); + } + ABC_FREE( p->pNodeToFrames ); + p->pNodeToFrames = pNodeToFrames; + p->nFrames *= 2; + } + // map constants and PIs + Ssw_ObjSetFrame( p, Aig_ManConst1(p->pAig), f, Aig_ManConst1(p->pFrames) ); + Saig_ManForEachPi( p->pAig, pObj, i ) + { + pObjNew = Aig_ObjCreatePi(p->pFrames); + Ssw_ObjSetFrame( p, pObj, f, pObjNew ); + } + // sweep internal nodes + Aig_ManForEachNode( p->pAig, pObj, i ) + { + pObjNew = Aig_And( p->pFrames, Ssw_ObjChild0Fra(p, pObj, f), Ssw_ObjChild1Fra(p, pObj, f) ); + Ssw_ObjSetFrame( p, pObj, f, pObjNew ); + if ( Ssw_ManSweepNodeFilter( p, pObj, f ) ) + break; + } + // printout + if ( p->pPars->fVerbose ) + { + printf( "Frame %4d : ", f ); + Ssw_ClassesPrint( p->ppClasses, 0 ); + } + if ( i < Vec_PtrSize(p->pAig->vObjs) ) + { + if ( p->pPars->fVerbose ) + printf( "Exceeded the resource limits (%d conflicts). Quitting...\n", p->pPars->nBTLimit ); + break; + } + // quit if this is the last timeframe + if ( f == p->pPars->nFramesK - 1 ) + { + if ( p->pPars->fVerbose ) + printf( "Exceeded the time frame limit (%d time frames). Quitting...\n", p->pPars->nFramesK ); + break; + } + // check timeout + if ( TimeLimit && ((float)TimeLimit <= (float)(clock()-clkTotal)/(float)(CLOCKS_PER_SEC)) ) + break; + // transfer latch input to the latch outputs + Aig_ManForEachPo( p->pAig, pObj, i ) + Ssw_ObjSetFrame( p, pObj, f, Ssw_ObjChild0Fra(p, pObj, f) ); + // build logic cones for register outputs + Saig_ManForEachLiLo( p->pAig, pObjLi, pObjLo, i ) + { + pObjNew = Ssw_ObjFrame( p, pObjLi, f ); + Ssw_ObjSetFrame( p, pObjLo, f+1, pObjNew ); + Ssw_CnfNodeAddToSolver( p->pMSat, Aig_Regular(pObjNew) );// + } + } + // verify +// Ssw_ClassesCheck( p->ppClasses ); + return 1; +} + +/**Function************************************************************* + + Synopsis [Filter equivalence classes of nodes.] + + Description [Unrolls at most nFramesMax frames. Works with nConfMax + conflicts until the first undefined SAT call. Verbose prints the message.] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Ssw_SignalFilter( Aig_Man_t * pAig, int nFramesMax, int nConfMax, int nRounds, int TimeLimit, int TimeLimit2, Abc_Cex_t * pCex, int fVerbose ) +{ + Ssw_Pars_t Pars, * pPars = &Pars; + Ssw_Man_t * p; + int r, TimeLimitPart, clkTotal = clock(); + assert( Aig_ManRegNum(pAig) > 0 ); + assert( Aig_ManConstrNum(pAig) == 0 ); + // consider the case of empty AIG + if ( Aig_ManNodeNum(pAig) == 0 ) + return; + // reset random numbers + Aig_ManRandom( 1 ); + // if parameters are not given, create them + Ssw_ManSetDefaultParams( pPars = &Pars ); + pPars->nFramesK = 3; //nFramesMax; + pPars->nBTLimit = nConfMax; + pPars->TimeLimit = TimeLimit; + pPars->fVerbose = fVerbose; + // start the induction manager + p = Ssw_ManCreate( pAig, pPars ); + pPars->nFramesK = nFramesMax; + // create trivial equivalence classes with all nodes being candidates for constant 1 + if ( pAig->pReprs == NULL ) + p->ppClasses = Ssw_ClassesPrepareSimple( pAig, 0, 0 ); + else + p->ppClasses = Ssw_ClassesPrepareFromReprs( pAig ); + Ssw_ClassesSetData( p->ppClasses, NULL, NULL, Ssw_SmlObjIsConstBit, Ssw_SmlObjsAreEqualBit ); + assert( p->vInits == NULL ); + // compute starting state if needed + if ( pCex ) + Ssw_ManFindStartingState( p, pCex ); + // refine classes using BMC + for ( r = 0; r < nRounds; r++ ) + { + if ( p->pPars->fVerbose ) + printf( "Round %3d:\n", r ); + // start filtering equivalence classes + Ssw_ManRefineByFilterSim( p, p->pPars->nFramesK ); + if ( Ssw_ClassesCand1Num(p->ppClasses) == 0 && Ssw_ClassesClassNum(p->ppClasses) == 0 ) + { + printf( "All equivalences are refined away.\n" ); + break; + } + // printout + if ( p->pPars->fVerbose ) + { + printf( "Initial : " ); + Ssw_ClassesPrint( p->ppClasses, 0 ); + } + p->pMSat = Ssw_SatStart( 0 ); + TimeLimitPart = TimeLimit ? TimeLimit - (int)((float)(clock()-clkTotal)/(float)(CLOCKS_PER_SEC)) : 0; + if ( TimeLimit2 ) + { + if ( TimeLimitPart ) + TimeLimitPart = ABC_MIN( TimeLimitPart, TimeLimit2 ); + else + TimeLimitPart = TimeLimit2; + } + Ssw_ManSweepBmcFilter( p, TimeLimitPart ); + Ssw_SatStop( p->pMSat ); + p->pMSat = NULL; + Ssw_ManCleanup( p ); + // simulate pattern forward + Ssw_ManRollForward( p, p->pPars->nFramesK ); + // check timeout + if ( TimeLimit && ((float)TimeLimit <= (float)(clock()-clkTotal)/(float)(CLOCKS_PER_SEC)) ) + { + printf( "Reached timeout (%d seconds).\n", TimeLimit ); + break; + } + } + // cleanup + Aig_ManSetPhase( p->pAig ); + Aig_ManCleanMarkB( p->pAig ); + // cleanup + pPars->fVerbose = 0; + Ssw_ManStop( p ); +} + +/**Function************************************************************* + + Synopsis [Filter equivalence classes of nodes.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Ssw_SignalFilterGia( Gia_Man_t * p, int nFramesMax, int nConfMax, int nRounds, int TimeLimit, int TimeLimit2, Abc_Cex_t * pCex, int fVerbose ) +{ + Aig_Man_t * pAig; + pAig = Gia_ManToAigSimple( p ); + if ( p->pReprs != NULL ) + { + Gia_ManReprToAigRepr2( pAig, p ); + ABC_FREE( p->pReprs ); + ABC_FREE( p->pNexts ); + } + Ssw_SignalFilter( pAig, nFramesMax, nConfMax, nRounds, TimeLimit, TimeLimit2, pCex, fVerbose ); + Gia_ManReprFromAigRepr( pAig, p ); + Aig_ManStop( pAig ); +} + +//////////////////////////////////////////////////////////////////////// +/// END OF FILE /// +//////////////////////////////////////////////////////////////////////// + + +ABC_NAMESPACE_IMPL_END + diff --git a/src/aig/ssw/sswInt.h b/src/aig/ssw/sswInt.h index 269bdad7..e3a9a341 100644 --- a/src/aig/ssw/sswInt.h +++ b/src/aig/ssw/sswInt.h @@ -21,6 +21,7 @@ #ifndef __SSW_INT_H__ #define __SSW_INT_H__ + //////////////////////////////////////////////////////////////////////// /// INCLUDES /// //////////////////////////////////////////////////////////////////////// @@ -33,9 +34,10 @@ /// PARAMETERS /// //////////////////////////////////////////////////////////////////////// -#ifdef __cplusplus -extern "C" { -#endif + + +ABC_NAMESPACE_HEADER_START + //////////////////////////////////////////////////////////////////////// /// BASIC TYPES /// @@ -93,6 +95,7 @@ struct Ssw_Man_t_ int iNodeLast; // the last node considered Vec_Ptr_t * vResimConsts; // resimulation constants Vec_Ptr_t * vResimClasses; // resimulation classes + Vec_Int_t * vInits; // the init values of primary inputs under constraints // counter example storage int nPatWords; // the number of words in the counter example unsigned * pPatWords; // the counter example @@ -113,6 +116,15 @@ struct Ssw_Man_t_ int nNodesEnd; int nRegsBeg; int nRegsEnd; + // equiv statistis + int nConesTotal; + int nConesConstr; + int nEquivsTotal; + int nEquivsConstr; + int nNodesBegC; + int nNodesEndC; + int nRegsBegC; + int nRegsEndC; // runtime stats int timeBmc; // bounded model checking int timeReduce; // speculative reduction @@ -172,7 +184,7 @@ static inline void Ssw_ObjSetFrame( Ssw_Man_t * p, Aig_Obj_t * pObj, int static inline Aig_Obj_t * Ssw_ObjChild0Fra( Ssw_Man_t * p, Aig_Obj_t * pObj, int i ) { assert( !Aig_IsComplement(pObj) ); return Aig_ObjFanin0(pObj)? Aig_NotCond(Ssw_ObjFrame(p, Aig_ObjFanin0(pObj), i), Aig_ObjFaninC0(pObj)) : NULL; } static inline Aig_Obj_t * Ssw_ObjChild1Fra( Ssw_Man_t * p, Aig_Obj_t * pObj, int i ) { assert( !Aig_IsComplement(pObj) ); return Aig_ObjFanin1(pObj)? Aig_NotCond(Ssw_ObjFrame(p, Aig_ObjFanin1(pObj), i), Aig_ObjFaninC1(pObj)) : NULL; } -static inline Aig_Obj_t * Ssw_ObjFrame_( Ssw_Frm_t * p, Aig_Obj_t * pObj, int i ) { return Vec_PtrGetEntry( p->vAig2Frm, p->nObjs*i+pObj->Id ); } +static inline Aig_Obj_t * Ssw_ObjFrame_( Ssw_Frm_t * p, Aig_Obj_t * pObj, int i ) { return (Aig_Obj_t *)Vec_PtrGetEntry( p->vAig2Frm, p->nObjs*i+pObj->Id ); } static inline void Ssw_ObjSetFrame_( Ssw_Frm_t * p, Aig_Obj_t * pObj, int i, Aig_Obj_t * pNode ) { Vec_PtrSetEntry( p->vAig2Frm, p->nObjs*i+pObj->Id, pNode ); } static inline Aig_Obj_t * Ssw_ObjChild0Fra_( Ssw_Frm_t * p, Aig_Obj_t * pObj, int i ) { assert( !Aig_IsComplement(pObj) ); return Aig_ObjFanin0(pObj)? Aig_NotCond(Ssw_ObjFrame_(p, Aig_ObjFanin0(pObj), i), Aig_ObjFaninC0(pObj)) : NULL; } @@ -206,8 +218,9 @@ extern void Ssw_ClassesCollectClass( Ssw_Cla_t * p, Aig_Obj_t * pRepr, 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 nFramesK, int fLatchCorr, int nMaxLevs, int fVerbose ); +extern Ssw_Cla_t * Ssw_ClassesPrepare( Aig_Man_t * pAig, int nFramesK, int fLatchCorr, int fOutputCorr, int nMaxLevs, int fVerbose ); extern Ssw_Cla_t * Ssw_ClassesPrepareSimple( Aig_Man_t * pAig, int fLatchCorr, int nMaxLevs ); +extern Ssw_Cla_t * Ssw_ClassesPrepareFromReprs( Aig_Man_t * pAig ); extern Ssw_Cla_t * Ssw_ClassesPrepareTargets( Aig_Man_t * pAig ); extern Ssw_Cla_t * Ssw_ClassesPreparePairs( Aig_Man_t * pAig, Vec_Int_t ** pvClasses ); extern Ssw_Cla_t * Ssw_ClassesPreparePairsSimple( Aig_Man_t * pMiter, Vec_Int_t * vPairs ); @@ -220,6 +233,10 @@ extern Ssw_Sat_t * Ssw_SatStart( int fPolarFlip ); extern void Ssw_SatStop( Ssw_Sat_t * p ); extern void Ssw_CnfNodeAddToSolver( Ssw_Sat_t * p, Aig_Obj_t * pObj ); extern int Ssw_CnfGetNodeValue( Ssw_Sat_t * p, Aig_Obj_t * pObjFraig ); +/*=== sswConstr.c ===================================================*/ +extern int Ssw_ManSweepBmcConstr( Ssw_Man_t * p ); +extern int Ssw_ManSweepConstr( Ssw_Man_t * p ); +extern void Ssw_ManRefineByConstrSim( Ssw_Man_t * p ); /*=== sswCore.c ===================================================*/ extern Aig_Man_t * Ssw_SignalCorrespondenceRefine( Ssw_Man_t * p ); /*=== sswDyn.c ===================================================*/ @@ -231,10 +248,10 @@ extern int Ssw_ManSweepLatch( Ssw_Man_t * p ); extern Ssw_Man_t * Ssw_ManCreate( Aig_Man_t * pAig, Ssw_Pars_t * pPars ); extern void Ssw_ManCleanup( Ssw_Man_t * p ); extern void Ssw_ManStop( Ssw_Man_t * p ); -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 ); +extern int Ssw_NodeIsConstrained( Ssw_Man_t * p, Aig_Obj_t * pPoObj ); /*=== sswSemi.c ===================================================*/ extern int Ssw_FilterUsingSemi( Ssw_Man_t * pMan, int fCheckTargets, int nConfMax, int fVerbose ); /*=== sswSim.c ===================================================*/ @@ -259,6 +276,7 @@ extern void Ssw_ManResimulateBit( Ssw_Man_t * p, Aig_Obj_t * pObj, Aig_ extern void Ssw_ManResimulateWord( Ssw_Man_t * p, Aig_Obj_t * pCand, Aig_Obj_t * pRepr, int f ); /*=== sswSweep.c ===================================================*/ extern int Ssw_ManGetSatVarValue( Ssw_Man_t * p, Aig_Obj_t * pObj, int f ); +extern void Ssw_SmlSavePatternAig( Ssw_Man_t * p, int f ); extern int Ssw_ManSweepNode( Ssw_Man_t * p, Aig_Obj_t * pObj, int f, int fBmc ); extern int Ssw_ManSweepBmc( Ssw_Man_t * p ); extern int Ssw_ManSweep( Ssw_Man_t * p ); @@ -267,9 +285,11 @@ extern void Ssw_UniqueRegisterPairInfo( Ssw_Man_t * p ); extern int Ssw_ManUniqueOne( Ssw_Man_t * p, Aig_Obj_t * pRepr, Aig_Obj_t * pObj, int fVerbose ); extern int Ssw_ManUniqueAddConstraint( Ssw_Man_t * p, Vec_Ptr_t * vCommon, int f1, int f2 ); -#ifdef __cplusplus -} -#endif + + +ABC_NAMESPACE_HEADER_END + + #endif diff --git a/src/aig/ssw/sswIslands.c b/src/aig/ssw/sswIslands.c index 8913116c..d1ebe4bc 100644 --- a/src/aig/ssw/sswIslands.c +++ b/src/aig/ssw/sswIslands.c @@ -20,6 +20,9 @@ #include "sswInt.h" +ABC_NAMESPACE_IMPL_START + + //////////////////////////////////////////////////////////////////////// /// DECLARATIONS /// //////////////////////////////////////////////////////////////////////// @@ -99,7 +102,7 @@ void Ssw_MatchingStart( Aig_Man_t * p0, Aig_Man_t * p1, Vec_Int_t * vPairs ) { if ( pObj0->pData == NULL ) continue; - pObj1 = pObj0->pData; + pObj1 = (Aig_Obj_t *)pObj0->pData; if ( !Saig_ObjIsLo(p1, pObj1) ) printf( "Mismatch between LO pairs.\n" ); } @@ -107,7 +110,7 @@ void Ssw_MatchingStart( Aig_Man_t * p0, Aig_Man_t * p1, Vec_Int_t * vPairs ) { if ( pObj1->pData == NULL ) continue; - pObj0 = pObj1->pData; + pObj0 = (Aig_Obj_t *)pObj1->pData; if ( !Saig_ObjIsLo(p0, pObj0) ) printf( "Mismatch between LO pairs.\n" ); } @@ -234,9 +237,9 @@ void Ssw_MatchingExtend( Aig_Man_t * p0, Aig_Man_t * p1, int nDist, int fVerbose { Ssw_MatchingExtendOne( p0, vNodes0 ); Ssw_MatchingExtendOne( p1, vNodes1 ); - Vec_PtrForEachEntry( vNodes0, pNext0, k ) + Vec_PtrForEachEntry( Aig_Obj_t *, vNodes0, pNext0, k ) { - pNext1 = pNext0->pData; + pNext1 = (Aig_Obj_t *)pNext0->pData; if ( pNext1 == NULL ) continue; assert( pNext1->pData == pNext0 ); @@ -245,9 +248,9 @@ void Ssw_MatchingExtend( Aig_Man_t * p0, Aig_Man_t * p1, int nDist, int fVerbose pNext0->pData = NULL; pNext1->pData = NULL; } - Vec_PtrForEachEntry( vNodes1, pNext0, k ) + Vec_PtrForEachEntry( Aig_Obj_t *, vNodes1, pNext0, k ) { - pNext1 = pNext0->pData; + pNext1 = (Aig_Obj_t *)pNext0->pData; if ( pNext1 == NULL ) continue; assert( pNext1->pData == pNext0 ); @@ -307,7 +310,7 @@ void Ssw_MatchingComplete( Aig_Man_t * p0, Aig_Man_t * p1 ) pObj1->pData = pObj0; } // create register outputs in p0 that are absent in p1 - Vec_PtrForEachEntry( vNewLis, pObj0Li, i ) + Vec_PtrForEachEntry( Aig_Obj_t *, vNewLis, pObj0Li, i ) Aig_ObjCreatePo( p1, Aig_ObjChild0Copy(pObj0Li) ); // increment the number of registers Aig_ManSetRegNum( p1, Aig_ManRegNum(p1) + Vec_PtrSize(vNewLis) ); @@ -342,7 +345,7 @@ Vec_Int_t * Ssw_MatchingPairs( Aig_Man_t * p0, Aig_Man_t * p1 ) { if ( Aig_ObjIsPo(pObj0) ) continue; - pObj1 = pObj0->pData; + pObj1 = (Aig_Obj_t *)pObj0->pData; Vec_IntPush( vPairsNew, pObj0->Id ); Vec_IntPush( vPairsNew, pObj1->Id ); } @@ -379,11 +382,11 @@ Vec_Int_t * Ssw_MatchingMiter( Aig_Man_t * pMiter, Aig_Man_t * p0, Aig_Man_t * p assert( pObj1->pData != NULL ); if ( pObj0->pData == pObj1->pData ) continue; - if ( Aig_ObjIsNone(pObj0->pData) || Aig_ObjIsNone(pObj1->pData) ) + if ( Aig_ObjIsNone((Aig_Obj_t *)pObj0->pData) || Aig_ObjIsNone((Aig_Obj_t *)pObj1->pData) ) continue; // get the miter nodes - pObj0 = pObj0->pData; - pObj1 = pObj1->pData; + pObj0 = (Aig_Obj_t *)pObj0->pData; + pObj1 = (Aig_Obj_t *)pObj1->pData; assert( !Aig_IsComplement(pObj0) ); assert( !Aig_IsComplement(pObj1) ); assert( Aig_ObjType(pObj0) == Aig_ObjType(pObj1) ); @@ -435,7 +438,7 @@ Aig_Man_t * Ssw_SecWithSimilaritySweep( Aig_Man_t * p0, Aig_Man_t * p1, Vec_Int_ if ( p->pPars->fPartSigCorr ) p->ppClasses = Ssw_ClassesPreparePairsSimple( pMiter, vPairsMiter ); else - p->ppClasses = Ssw_ClassesPrepare( pMiter, pPars->nFramesK, pPars->fLatchCorr, pPars->nMaxLevs, pPars->fVerbose ); + p->ppClasses = Ssw_ClassesPrepare( pMiter, pPars->nFramesK, pPars->fLatchCorr, pPars->fOutputCorr, pPars->nMaxLevs, pPars->fVerbose ); if ( p->pPars->fDumpSRInit ) { if ( p->pPars->fPartSigCorr ) @@ -449,7 +452,7 @@ Aig_Man_t * Ssw_SecWithSimilaritySweep( Aig_Man_t * p0, Aig_Man_t * p1, Vec_Int_ printf( "Dumping speculative miter is possible only for partial signal correspondence (switch \"-c\").\n" ); } p->pSml = Ssw_SmlStart( pMiter, 0, 1 + p->pPars->nFramesAddSim, 1 ); - Ssw_ClassesSetData( p->ppClasses, p->pSml, Ssw_SmlObjHashWord, Ssw_SmlObjIsConstWord, Ssw_SmlObjsAreEqualWord ); + Ssw_ClassesSetData( p->ppClasses, p->pSml, (unsigned(*)(void *,Aig_Obj_t *))Ssw_SmlObjHashWord, (int(*)(void *,Aig_Obj_t *))Ssw_SmlObjIsConstWord, (int(*)(void *,Aig_Obj_t *,Aig_Obj_t *))Ssw_SmlObjsAreEqualWord ); // perform refinement of classes pAigNew = Ssw_SignalCorrespondenceRefine( p ); // cleanup @@ -591,3 +594,5 @@ int Ssw_SecWithSimilarity( Aig_Man_t * p0, Aig_Man_t * p1, Ssw_Pars_t * pPars ) //////////////////////////////////////////////////////////////////////// +ABC_NAMESPACE_IMPL_END + diff --git a/src/aig/ssw/sswLcorr.c b/src/aig/ssw/sswLcorr.c index fb36c31d..7cd94727 100644 --- a/src/aig/ssw/sswLcorr.c +++ b/src/aig/ssw/sswLcorr.c @@ -21,6 +21,9 @@ #include "sswInt.h" //#include "bar.h" +ABC_NAMESPACE_IMPL_START + + //////////////////////////////////////////////////////////////////////// /// DECLARATIONS /// //////////////////////////////////////////////////////////////////////// @@ -56,7 +59,7 @@ void Ssw_ManSweepTransfer( Ssw_Man_t * p ) } assert( !Aig_IsComplement(pObjFraig) ); assert( Aig_ObjIsPi(pObjFraig) ); - pInfo = Vec_PtrEntry( p->vSimInfo, Aig_ObjPioNum(pObjFraig) ); + pInfo = (unsigned *)Vec_PtrEntry( p->vSimInfo, Aig_ObjPioNum(pObjFraig) ); Ssw_SmlObjSetWord( p->pSml, pObj, pInfo[0], 0, 0 ); } } @@ -106,14 +109,14 @@ void Ssw_SmlAddPattern( Ssw_Man_t * p, Aig_Obj_t * pRepr, Aig_Obj_t * pCand ) Aig_Obj_t * pObj; unsigned * pInfo; int i, nVarNum, Value; - Vec_PtrForEachEntry( p->pMSat->vUsedPis, pObj, i ) + Vec_PtrForEachEntry( Aig_Obj_t *, p->pMSat->vUsedPis, pObj, i ) { nVarNum = Ssw_ObjSatNum( p->pMSat, pObj ); assert( nVarNum > 0 ); Value = sat_solver_var_value( p->pMSat->pSat, nVarNum ); if ( Value == 0 ) continue; - pInfo = Vec_PtrEntry( p->vSimInfo, Aig_ObjPioNum(pObj) ); + pInfo = (unsigned *)Vec_PtrEntry( p->vSimInfo, Aig_ObjPioNum(pObj) ); Aig_InfoSetBit( pInfo, p->nPatterns ); } } @@ -284,7 +287,7 @@ int Ssw_ManSweepLatch( Ssw_Man_t * p ) if ( Vec_PtrSize(vClass) == 0 ) continue; // try to prove equivalences in this class - Vec_PtrForEachEntry( vClass, pTemp, k ) + Vec_PtrForEachEntry( Aig_Obj_t *, vClass, pTemp, k ) if ( Aig_ObjRepr(p->pAig, pTemp) == pObj ) { Ssw_ManSweepLatchOne( p, pObj, pTemp ); @@ -329,3 +332,5 @@ int Ssw_ManSweepLatch( Ssw_Man_t * p ) //////////////////////////////////////////////////////////////////////// +ABC_NAMESPACE_IMPL_END + diff --git a/src/aig/ssw/sswMan.c b/src/aig/ssw/sswMan.c index 90cc9028..0f1317e1 100644 --- a/src/aig/ssw/sswMan.c +++ b/src/aig/ssw/sswMan.c @@ -20,6 +20,9 @@ #include "sswInt.h" +ABC_NAMESPACE_IMPL_START + + //////////////////////////////////////////////////////////////////////// /// DECLARATIONS /// //////////////////////////////////////////////////////////////////////// @@ -57,13 +60,12 @@ Ssw_Man_t * Ssw_ManCreate( Aig_Man_t * pAig, Ssw_Pars_t * pPars ) p->iOutputLit = -1; // allocate storage for sim pattern p->nPatWords = Aig_BitWordNum( Saig_ManPiNum(pAig) * p->nFrames + Saig_ManRegNum(pAig) ); - p->pPatWords = ABC_ALLOC( unsigned, p->nPatWords ); + p->pPatWords = ABC_CALLOC( unsigned, p->nPatWords ); // other p->vNewLos = Vec_PtrAlloc( 100 ); p->vNewPos = Vec_IntAlloc( 100 ); p->vResimConsts = Vec_PtrAlloc( 100 ); p->vResimClasses = Vec_PtrAlloc( 100 ); - // p->pPars->fVerbose = 1; return p; } @@ -104,10 +106,10 @@ 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: F = %d. AddF = %d. C-lim = %d. Constr = %d. MaxLev = %d. Mem = %0.2f Mb.\n", - p->pPars->nFramesK, p->pPars->nFramesAddSim, p->pPars->nBTLimit, p->pPars->nConstrs, p->pPars->nMaxLevs, nMemory ); + p->pPars->nFramesK, p->pPars->nFramesAddSim, p->pPars->nBTLimit, Saig_ManConstrNum(p->pAig), 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), - 0/p->pPars->nIters ); + 0/(p->pPars->nIters+1) ); printf( "SAT calls : Proof = %d. Cex = %d. Fail = %d. Lits proved = %d.\n", p->nSatProof, p->nSatCallsSat, p->nSatFailsReal, Ssw_ManCountEquivs(p) ); printf( "SAT solver: Vars max = %d. Calls max = %d. Recycles = %d. Sim rounds = %d.\n", @@ -127,6 +129,19 @@ void Ssw_ManPrintStats( Ssw_Man_t * p ) ABC_PRTP( " undecided", p->timeSatUndec, p->timeTotal ); ABC_PRTP( "Other ", p->timeOther, p->timeTotal ); ABC_PRTP( "TOTAL ", p->timeTotal, p->timeTotal ); + + // report the reductions + if ( p->pAig->nConstrs ) + { + printf( "Statistics reflecting the use of constraints:\n" ); + printf( "Total cones = %6d. Constraint cones = %6d. (%6.2f %%)\n", + p->nConesTotal, p->nConesConstr, 100.0*p->nConesConstr/p->nConesTotal ); + printf( "Total equivs = %6d. Removed equivs = %6d. (%6.2f %%)\n", + p->nEquivsTotal, p->nEquivsConstr, 100.0*p->nEquivsConstr/p->nEquivsTotal ); + printf( "NBeg = %d. NEnd = %d. (Gain = %6.2f %%). RBeg = %d. REnd = %d. (Gain = %6.2f %%).\n", + p->nNodesBegC, p->nNodesEndC, 100.0*(p->nNodesBegC-p->nNodesEndC)/(p->nNodesBegC?p->nNodesBegC:1), + p->nRegsBegC, p->nRegsEndC, 100.0*(p->nRegsBegC-p->nRegsEndC)/(p->nRegsBegC?p->nRegsBegC:1) ); + } } /**Function************************************************************* @@ -174,7 +189,7 @@ void Ssw_ManCleanup( Ssw_Man_t * p ) void Ssw_ManStop( Ssw_Man_t * p ) { ABC_FREE( p->pVisited ); - if ( p->pPars->fVerbose ) + if ( p->pPars->fVerbose )//&& p->pPars->nStepsMax == -1 ) Ssw_ManPrintStats( p ); if ( p->ppClasses ) Ssw_ClassesStop( p->ppClasses ); @@ -182,6 +197,8 @@ void Ssw_ManStop( Ssw_Man_t * p ) Ssw_SmlStop( p->pSml ); if ( p->vDiffPairs ) Vec_IntFree( p->vDiffPairs ); + if ( p->vInits ) + Vec_IntFree( p->vInits ); Vec_PtrFree( p->vResimConsts ); Vec_PtrFree( p->vResimClasses ); Vec_PtrFree( p->vNewLos ); @@ -197,3 +214,5 @@ void Ssw_ManStop( Ssw_Man_t * p ) //////////////////////////////////////////////////////////////////////// +ABC_NAMESPACE_IMPL_END + diff --git a/src/aig/ssw/sswPairs.c b/src/aig/ssw/sswPairs.c index 3c079922..0aba942f 100644 --- a/src/aig/ssw/sswPairs.c +++ b/src/aig/ssw/sswPairs.c @@ -20,6 +20,9 @@ #include "sswInt.h" +ABC_NAMESPACE_IMPL_START + + //////////////////////////////////////////////////////////////////////// /// DECLARATIONS /// //////////////////////////////////////////////////////////////////////// @@ -113,8 +116,8 @@ Vec_Int_t * Ssw_TransferSignalPairs( Aig_Man_t * pMiter, Aig_Man_t * pAig1, Aig_ { pObj1 = Aig_ManObj( pAig1, Vec_IntEntry(vIds1, i) ); pObj2 = Aig_ManObj( pAig2, Vec_IntEntry(vIds2, i) ); - pObj1m = Aig_Regular(pObj1->pData); - pObj2m = Aig_Regular(pObj2->pData); + pObj1m = Aig_Regular((Aig_Obj_t *)pObj1->pData); + pObj2m = Aig_Regular((Aig_Obj_t *)pObj2->pData); assert( pObj1m && pObj2m ); if ( pObj1m == pObj2m ) continue; @@ -290,7 +293,7 @@ Aig_Man_t * Ssw_SignalCorrespondenceWithPairs( Aig_Man_t * pAig1, Aig_Man_t * pA // create equivalence classes using these IDs p->ppClasses = Ssw_ClassesPreparePairs( pMiter, pvClasses ); p->pSml = Ssw_SmlStart( pMiter, 0, p->nFrames + p->pPars->nFramesAddSim, 1 ); - Ssw_ClassesSetData( p->ppClasses, p->pSml, Ssw_SmlObjHashWord, Ssw_SmlObjIsConstWord, Ssw_SmlObjsAreEqualWord ); + Ssw_ClassesSetData( p->ppClasses, p->pSml, (unsigned(*)(void *,Aig_Obj_t *))Ssw_SmlObjHashWord, (int(*)(void *,Aig_Obj_t *))Ssw_SmlObjIsConstWord, (int(*)(void *,Aig_Obj_t *,Aig_Obj_t *))Ssw_SmlObjsAreEqualWord ); // perform refinement of classes pAigNew = Ssw_SignalCorrespondenceRefine( p ); // cleanup @@ -326,7 +329,7 @@ Aig_Man_t * Ssw_SignalCorrespondeceTestPairs( Aig_Man_t * pAig ) vIds2 = Vec_IntAlloc( Aig_ManObjNumMax(pAig) ); Aig_ManForEachObj( pAig, pObj, i ) { - pRepr = Aig_Regular(pObj->pData); + pRepr = Aig_Regular((Aig_Obj_t *)pObj->pData); if ( pRepr == NULL ) continue; if ( Aig_ManObj(pAigNew, pRepr->Id) == NULL ) @@ -470,3 +473,5 @@ int Ssw_SecGeneralMiter( Aig_Man_t * pMiter, Ssw_Pars_t * pPars ) //////////////////////////////////////////////////////////////////////// +ABC_NAMESPACE_IMPL_END + diff --git a/src/aig/ssw/sswPart.c b/src/aig/ssw/sswPart.c index f481b457..8a0e69da 100644 --- a/src/aig/ssw/sswPart.c +++ b/src/aig/ssw/sswPart.c @@ -19,6 +19,10 @@ ***********************************************************************/ #include "sswInt.h" +#include "ioa.h" + +ABC_NAMESPACE_IMPL_START + //////////////////////////////////////////////////////////////////////// /// DECLARATIONS /// @@ -50,16 +54,20 @@ Aig_Man_t * Ssw_SignalCorrespondencePart( Aig_Man_t * pAig, Ssw_Pars_t * pPars ) int i, nCountPis, nCountRegs; int nClasses, nPartSize, fVerbose; int clk = clock(); - + if ( pPars->fConstrs ) + { + printf( "Cannot use partitioned computation with constraints.\n" ); + return NULL; + } // save parameters nPartSize = pPars->nPartSize; pPars->nPartSize = 0; - fVerbose = pPars->fVerbose; pPars->fVerbose = 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 ) + Vec_PtrForEachEntry( Vec_Int_t *, (Vec_Ptr_t *)pAig->vClockDoms, vPart, i ) { if ( nPartSize && Vec_IntSize(vPart) > nPartSize ) Aig_ManPartDivide( vResult, vPart, nPartSize, pPars->nOverSize ); @@ -75,9 +83,9 @@ Aig_Man_t * Ssw_SignalCorrespondencePart( Aig_Man_t * pAig, Ssw_Pars_t * pPars ) { // print partitions printf( "Simple partitioning. %d partitions are saved:\n", Vec_PtrSize(vResult) ); - Vec_PtrForEachEntry( vResult, vPart, i ) + Vec_PtrForEachEntry( Vec_Int_t *, vResult, vPart, i ) { - extern void Ioa_WriteAiger( Aig_Man_t * pMan, char * pFileName, int fWriteSymbols, int fCompact ); +// 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 ); @@ -89,7 +97,7 @@ Aig_Man_t * Ssw_SignalCorrespondencePart( Aig_Man_t * pAig, Ssw_Pars_t * pPars ) // perform SSW with partitions Aig_ManReprStart( pAig, Aig_ManObjNumMax(pAig) ); - Vec_PtrForEachEntry( vResult, vPart, i ) + Vec_PtrForEachEntry( Vec_Int_t *, vResult, vPart, i ) { pTemp = Aig_ManRegCreatePart( pAig, vPart, &nCountPis, &nCountRegs, &pMapBack ); Aig_ManSetRegNum( pTemp, pTemp->nRegs ); @@ -129,3 +137,5 @@ Aig_Man_t * Ssw_SignalCorrespondencePart( Aig_Man_t * pAig, Ssw_Pars_t * pPars ) //////////////////////////////////////////////////////////////////////// +ABC_NAMESPACE_IMPL_END + diff --git a/src/aig/ssw/sswSat.c b/src/aig/ssw/sswSat.c index 21c5c1f1..7d371cac 100644 --- a/src/aig/ssw/sswSat.c +++ b/src/aig/ssw/sswSat.c @@ -20,6 +20,9 @@ #include "sswInt.h" +ABC_NAMESPACE_IMPL_START + + //////////////////////////////////////////////////////////////////////// /// DECLARATIONS /// //////////////////////////////////////////////////////////////////////// @@ -50,9 +53,6 @@ int Ssw_NodesAreEquiv( Ssw_Man_t * p, Aig_Obj_t * pOld, Aig_Obj_t * pNew ) assert( !Aig_IsComplement(pOld) ); assert( !Aig_IsComplement(pNew) ); assert( pOld != pNew ); - -// if ( p->pSat == NULL ) -// Ssw_ManStartSolver( p ); assert( p->pMSat != NULL ); // if the nodes do not have SAT variables, allocate them @@ -199,7 +199,7 @@ int Ssw_NodesAreConstrained( Ssw_Man_t * p, Aig_Obj_t * pOld, Aig_Obj_t * pNew ) // sanity checks assert( Aig_Regular(pOld) != Aig_Regular(pNew) ); - assert( Aig_ObjPhaseReal(pOld) == Aig_ObjPhaseReal(pNew) ); + assert( p->pPars->fConstrs || Aig_ObjPhaseReal(pOld) == Aig_ObjPhaseReal(pNew) ); // move constant to the old node if ( Aig_Regular(pNew) == Aig_ManConst1(p->pFrames) ) @@ -216,9 +216,6 @@ int Ssw_NodesAreConstrained( Ssw_Man_t * p, Aig_Obj_t * pOld, Aig_Obj_t * pNew ) pOld = Aig_Regular(pOld); pNew = Aig_Not(pNew); } - -// if ( p->pSat == NULL ) -// Ssw_ManStartSolver( p ); assert( p->pMSat != NULL ); // if the nodes do not have SAT variables, allocate them @@ -274,8 +271,36 @@ int Ssw_NodesAreConstrained( Ssw_Man_t * p, Aig_Obj_t * pOld, Aig_Obj_t * pNew ) return 1; } +/**Function************************************************************* + + Synopsis [Constrains one node in the SAT solver.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Ssw_NodeIsConstrained( Ssw_Man_t * p, Aig_Obj_t * pPoObj ) +{ + int RetValue, Lit; + Ssw_CnfNodeAddToSolver( p->pMSat, Aig_ObjFanin0(pPoObj) ); + // add constraint A = 1 ----> A + Lit = toLitCond( Ssw_ObjSatNum(p->pMSat,Aig_ObjFanin0(pPoObj)), !Aig_ObjFaninC0(pPoObj) ); + if ( p->pPars->fPolarFlip ) + { + if ( Aig_ObjFanin0(pPoObj)->fPhase ) Lit = lit_neg( Lit ); + } + RetValue = sat_solver_addclause( p->pMSat->pSat, &Lit, &Lit + 1 ); + assert( RetValue ); + return 1; +} + //////////////////////////////////////////////////////////////////////// /// END OF FILE /// //////////////////////////////////////////////////////////////////////// +ABC_NAMESPACE_IMPL_END + diff --git a/src/aig/ssw/sswSemi.c b/src/aig/ssw/sswSemi.c index 1d578291..dfb2fb0f 100644 --- a/src/aig/ssw/sswSemi.c +++ b/src/aig/ssw/sswSemi.c @@ -20,6 +20,9 @@ #include "sswInt.h" +ABC_NAMESPACE_IMPL_START + + //////////////////////////////////////////////////////////////////////// /// DECLARATIONS /// //////////////////////////////////////////////////////////////////////// @@ -127,7 +130,7 @@ int Ssw_SemCheckTargets( Ssw_Sem_t * p ) { Aig_Obj_t * pObj; int i; - Vec_PtrForEachEntry( p->vTargets, pObj, i ) + Vec_PtrForEachEntry( Aig_Obj_t *, p->vTargets, pObj, i ) if ( !Ssw_ObjIsConst1Cand(p->pMan->pAig, pObj) ) return 1; return 0; @@ -153,7 +156,7 @@ void Ssw_ManFilterBmcSavePattern( Ssw_Sem_t * p ) return; Saig_ManForEachLo( p->pMan->pAig, pObj, i ) { - pInfo = Vec_PtrEntry( p->vPatterns, i ); + pInfo = (unsigned *)Vec_PtrEntry( p->vPatterns, i ); if ( Aig_InfoHasBit( p->pMan->pPatWords, Saig_ManPiNum(p->pMan->pAig) + i ) ) Aig_InfoSetBit( pInfo, p->nPatterns ); } @@ -183,7 +186,7 @@ clk = clock(); p->pFrames = Aig_ManStart( Aig_ManObjNumMax(p->pAig) * 3 ); Saig_ManForEachLo( p->pAig, pObj, i ) { - pInfo = Vec_PtrEntry( pBmc->vPatterns, i ); + pInfo = (unsigned *)Vec_PtrEntry( pBmc->vPatterns, i ); pObjNew = Aig_NotCond( Aig_ManConst1(p->pFrames), !Aig_InfoHasBit(pInfo, iPat) ); Ssw_ObjSetFrame( p, pObj, 0, pObjNew ); } @@ -315,3 +318,5 @@ clk = clock(); //////////////////////////////////////////////////////////////////////// +ABC_NAMESPACE_IMPL_END + diff --git a/src/aig/ssw/sswSim.c b/src/aig/ssw/sswSim.c index cf5270dd..37bf5717 100644 --- a/src/aig/ssw/sswSim.c +++ b/src/aig/ssw/sswSim.c @@ -20,6 +20,9 @@ #include "sswInt.h" +ABC_NAMESPACE_IMPL_START + + //////////////////////////////////////////////////////////////////////// /// DECLARATIONS /// //////////////////////////////////////////////////////////////////////// @@ -349,7 +352,7 @@ int Ssw_SmlNodeCountOnesRealVec( Ssw_Sml_t * p, Vec_Ptr_t * vObjs ) for ( i = 0; i < p->nWordsTotal; i++ ) { uWord = 0; - Vec_PtrForEachEntry( vObjs, pObj, k ) + Vec_PtrForEachEntry( Aig_Obj_t *, vObjs, pObj, k ) { pSims = Ssw_ObjSim(p, Aig_Regular(pObj)->Id); if ( Aig_Regular(pObj)->fPhase ^ Aig_IsComplement(pObj) ) @@ -858,7 +861,7 @@ void Ssw_SmlInitialize( Ssw_Sml_t * p, int fInit ) if ( fInit ) { assert( Aig_ManRegNum(p->pAig) > 0 ); - assert( Aig_ManRegNum(p->pAig) < Aig_ManPiNum(p->pAig) ); + 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 ); @@ -1240,12 +1243,12 @@ unsigned * Ssw_SmlSimInfo( Ssw_Sml_t * p, Aig_Obj_t * pObj ) SeeAlso [] ***********************************************************************/ -Ssw_Cex_t * Ssw_SmlAllocCounterExample( int nRegs, int nRealPis, int nFrames ) +Abc_Cex_t * Ssw_SmlAllocCounterExample( int nRegs, int nRealPis, int nFrames ) { - Ssw_Cex_t * pCex; + Abc_Cex_t * pCex; int nWords = Aig_BitWordNum( nRegs + nRealPis * nFrames ); - pCex = (Ssw_Cex_t *)ABC_ALLOC( char, sizeof(Ssw_Cex_t) + sizeof(unsigned) * nWords ); - memset( pCex, 0, sizeof(Ssw_Cex_t) + sizeof(unsigned) * nWords ); + pCex = (Abc_Cex_t *)ABC_ALLOC( char, sizeof(Abc_Cex_t) + sizeof(unsigned) * nWords ); + memset( pCex, 0, sizeof(Abc_Cex_t) + sizeof(unsigned) * nWords ); pCex->nRegs = nRegs; pCex->nPis = nRealPis; pCex->nBits = nRegs + nRealPis * nFrames; @@ -1263,7 +1266,7 @@ Ssw_Cex_t * Ssw_SmlAllocCounterExample( int nRegs, int nRealPis, int nFrames ) SeeAlso [] ***********************************************************************/ -void Ssw_SmlFreeCounterExample( Ssw_Cex_t * pCex ) +void Ssw_SmlFreeCounterExample( Abc_Cex_t * pCex ) { ABC_FREE( pCex ); } @@ -1279,11 +1282,15 @@ void Ssw_SmlFreeCounterExample( Ssw_Cex_t * pCex ) SeeAlso [] ***********************************************************************/ -int Ssw_SmlRunCounterExample( Aig_Man_t * pAig, Ssw_Cex_t * p ) +int Ssw_SmlRunCounterExample( Aig_Man_t * pAig, Abc_Cex_t * p ) { Ssw_Sml_t * pSml; Aig_Obj_t * pObj; int RetValue, i, k, iBit; + if ( Saig_ManPiNum(pAig) != p->nPis ) + return 0; +// if ( Saig_ManRegNum(pAig) != p->nRegs ) +// return 0; // assert( Aig_ManRegNum(pAig) > 0 ); // assert( Aig_ManRegNum(pAig) < Aig_ManPiNum(pAig) ); // start a new sequential simulator @@ -1293,10 +1300,11 @@ int Ssw_SmlRunCounterExample( Aig_Man_t * pAig, Ssw_Cex_t * p ) Saig_ManForEachLo( pAig, pObj, i ) Ssw_SmlObjAssignConst( pSml, pObj, Aig_InfoHasBit(p->pData, iBit++), 0 ); // assign simulation info for the primary inputs + iBit = Saig_ManRegNum(pAig); for ( i = 0; i <= p->iFrame; i++ ) Saig_ManForEachPi( pAig, pObj, k ) Ssw_SmlObjAssignConst( pSml, pObj, Aig_InfoHasBit(p->pData, iBit++), i ); - assert( iBit == p->nBits ); +// assert( iBit == p->nBits ); // run random simulation Ssw_SmlSimulateOne( pSml ); // check if the given output has failed @@ -1316,7 +1324,7 @@ int Ssw_SmlRunCounterExample( Aig_Man_t * pAig, Ssw_Cex_t * p ) SeeAlso [] ***********************************************************************/ -int Ssw_SmlFindOutputCounterExample( Aig_Man_t * pAig, Ssw_Cex_t * p ) +int Ssw_SmlFindOutputCounterExample( Aig_Man_t * pAig, Abc_Cex_t * p ) { Ssw_Sml_t * pSml; Aig_Obj_t * pObj; @@ -1359,9 +1367,9 @@ int Ssw_SmlFindOutputCounterExample( Aig_Man_t * pAig, Ssw_Cex_t * p ) SeeAlso [] ***********************************************************************/ -Ssw_Cex_t * Ssw_SmlGetCounterExample( Ssw_Sml_t * p ) +Abc_Cex_t * Ssw_SmlGetCounterExample( Ssw_Sml_t * p ) { - Ssw_Cex_t * pCex; + Abc_Cex_t * pCex; Aig_Obj_t * pObj; unsigned * pSims; int iPo, iFrame, iBit, i, k; @@ -1433,9 +1441,9 @@ Ssw_Cex_t * Ssw_SmlGetCounterExample( Ssw_Sml_t * p ) SeeAlso [] ***********************************************************************/ -Ssw_Cex_t * Ssw_SmlCopyCounterExample( Aig_Man_t * pAig, Aig_Man_t * pFrames, int * pModel ) +Abc_Cex_t * Ssw_SmlCopyCounterExample( Aig_Man_t * pAig, Aig_Man_t * pFrames, int * pModel ) { - Ssw_Cex_t * pCex; + Abc_Cex_t * pCex; Aig_Obj_t * pObj; int i, nFrames, nTruePis, nTruePos, iPo, iFrame; // get the number of frames @@ -1493,9 +1501,9 @@ Ssw_Cex_t * Ssw_SmlCopyCounterExample( Aig_Man_t * pAig, Aig_Man_t * pFrames, in SeeAlso [] ***********************************************************************/ -Ssw_Cex_t * Ssw_SmlTrivCounterExample( Aig_Man_t * pAig, int iFrameOut ) +Abc_Cex_t * Ssw_SmlTrivCounterExample( Aig_Man_t * pAig, int iFrameOut ) { - Ssw_Cex_t * pCex; + Abc_Cex_t * pCex; int nTruePis, nTruePos, iPo, iFrame; assert( Aig_ManRegNum(pAig) > 0 ); nTruePis = Aig_ManPiNum(pAig)-Aig_ManRegNum(pAig); @@ -1520,9 +1528,9 @@ Ssw_Cex_t * Ssw_SmlTrivCounterExample( Aig_Man_t * pAig, int iFrameOut ) SeeAlso [] ***********************************************************************/ -Ssw_Cex_t * Ssw_SmlDupCounterExample( Ssw_Cex_t * p, int nRegsNew ) +Abc_Cex_t * Ssw_SmlDupCounterExample( Abc_Cex_t * p, int nRegsNew ) { - Ssw_Cex_t * pCex; + Abc_Cex_t * pCex; int i; pCex = Ssw_SmlAllocCounterExample( nRegsNew, p->nPis, p->iFrame+1 ); pCex->iPo = p->iPo; @@ -1544,7 +1552,7 @@ Ssw_Cex_t * Ssw_SmlDupCounterExample( Ssw_Cex_t * p, int nRegsNew ) SeeAlso [] ***********************************************************************/ -int Ssw_SmlWriteCounterExample( FILE * pFile, Aig_Man_t * pAig, Ssw_Cex_t * p ) +int Ssw_SmlWriteCounterExample( FILE * pFile, Aig_Man_t * pAig, Abc_Cex_t * p ) { Ssw_Sml_t * pSml; Aig_Obj_t * pObj; @@ -1614,3 +1622,5 @@ int Ssw_SmlWriteCounterExample( FILE * pFile, Aig_Man_t * pAig, Ssw_Cex_t * p ) //////////////////////////////////////////////////////////////////////// +ABC_NAMESPACE_IMPL_END + diff --git a/src/aig/ssw/sswSimSat.c b/src/aig/ssw/sswSimSat.c index c85b8bcf..6b18a3a6 100644 --- a/src/aig/ssw/sswSimSat.c +++ b/src/aig/ssw/sswSimSat.c @@ -20,6 +20,9 @@ #include "sswInt.h" +ABC_NAMESPACE_IMPL_START + + //////////////////////////////////////////////////////////////////////// /// DECLARATIONS /// //////////////////////////////////////////////////////////////////////// @@ -51,21 +54,25 @@ void Ssw_ManResimulateBit( Ssw_Man_t * p, Aig_Obj_t * pCand, Aig_Obj_t * pRepr ) Aig_ManForEachNode( p->pAig, pObj, i ) pObj->fMarkB = ( Aig_ObjFanin0(pObj)->fMarkB ^ Aig_ObjFaninC0(pObj) ) & ( Aig_ObjFanin1(pObj)->fMarkB ^ Aig_ObjFaninC1(pObj) ); - // check equivalence classes - RetValue1 = Ssw_ClassesRefineConst1( p->ppClasses, 0 ); - RetValue2 = Ssw_ClassesRefine( p->ppClasses, 0 ); - // make sure refinement happened - if ( Aig_ObjIsConst1(pRepr) ) - { - assert( RetValue1 ); - if ( RetValue1 == 0 ) - printf( "\nSsw_ManResimulateBit() Error: RetValue1 does not hold.\n" ); - } - else + // if repr is given, perform refinement + if ( pRepr ) { - assert( RetValue2 ); - if ( RetValue2 == 0 ) - printf( "\nSsw_ManResimulateBit() Error: RetValue2 does not hold.\n" ); + // check equivalence classes + RetValue1 = Ssw_ClassesRefineConst1( p->ppClasses, 0 ); + RetValue2 = Ssw_ClassesRefine( p->ppClasses, 0 ); + // make sure refinement happened + if ( Aig_ObjIsConst1(pRepr) ) + { + assert( RetValue1 ); + if ( RetValue1 == 0 ) + printf( "\nSsw_ManResimulateBit() Error: RetValue1 does not hold.\n" ); + } + else + { + assert( RetValue2 ); + if ( RetValue2 == 0 ) + printf( "\nSsw_ManResimulateBit() Error: RetValue2 does not hold.\n" ); + } } p->timeSimSat += clock() - clk; } @@ -112,3 +119,5 @@ p->timeSimSat += clock() - clk; //////////////////////////////////////////////////////////////////////// +ABC_NAMESPACE_IMPL_END + diff --git a/src/aig/ssw/sswSweep.c b/src/aig/ssw/sswSweep.c index a2f3c175..39fcd48e 100644 --- a/src/aig/ssw/sswSweep.c +++ b/src/aig/ssw/sswSweep.c @@ -21,6 +21,9 @@ #include "sswInt.h" #include "bar.h" +ABC_NAMESPACE_IMPL_START + + //////////////////////////////////////////////////////////////////////// /// DECLARATIONS /// //////////////////////////////////////////////////////////////////////// @@ -157,14 +160,14 @@ void Ssw_SmlAddPatternDyn( Ssw_Man_t * p ) unsigned * pInfo; int i, nVarNum; // iterate through the PIs of the frames - Vec_PtrForEachEntry( p->pMSat->vUsedPis, pObj, i ) + Vec_PtrForEachEntry( Aig_Obj_t *, p->pMSat->vUsedPis, pObj, i ) { assert( Aig_ObjIsPi(pObj) ); nVarNum = Ssw_ObjSatNum( p->pMSat, pObj ); assert( nVarNum > 0 ); if ( sat_solver_var_value( p->pMSat->pSat, nVarNum ) ) { - pInfo = Vec_PtrEntry( p->vSimInfo, Aig_ObjPioNum(pObj) ); + pInfo = (unsigned *)Vec_PtrEntry( p->vSimInfo, Aig_ObjPioNum(pObj) ); Aig_InfoSetBit( pInfo, p->nPatterns ); } } @@ -232,34 +235,7 @@ p->timeMarkCones += clock() - clk; } else Ssw_SmlSavePatternAig( p, f ); - // consider uniqueness - if ( !fBmc && !p->pPars->fDynamic && p->pPars->fUniqueness && p->pPars->nFramesK > 1 && - Ssw_ManUniqueOne( p, pObjRepr, pObj, p->pPars->fVerbose ) && p->iOutputLit == -1 ) - { - if ( Ssw_ManUniqueAddConstraint( p, p->vCommon, 0, 1 ) ) - { - int RetValue2 = Ssw_NodesAreEquiv( p, Aig_Regular(pObjReprFraig), Aig_Regular(pObjFraig) ); - p->iOutputLit = -1; - p->nUniques++; - p->nUniquesAdded++; - if ( RetValue2 == 0 ) - { - int x; -// printf( "Second time:\n" ); - x = Ssw_ManUniqueOne( p, pObjRepr, pObj, p->pPars->fVerbose ); - Ssw_SmlSavePatternAig( p, f ); - Ssw_ManResimulateWord( p, pObj, pObjRepr, f ); - if ( Aig_ObjRepr( p->pAig, pObj ) == pObjRepr ) - printf( "Ssw_ManSweepNode(): Refinement did not happen!!!.\n" ); - return 1; - } - else - p->nUniquesUseful++; -// printf( "Counter-example prevented!!!\n" ); - return 0; - } - } - if ( p->pPars->nConstrs == 0 ) + if ( !p->pPars->fConstrs ) Ssw_ManResimulateWord( p, pObj, pObjRepr, f ); else Ssw_ManResimulateBit( p, pObj, pObjRepr ); @@ -298,7 +274,6 @@ clk = clock(); p->fRefined = 0; if ( p->pPars->fVerbose ) pProgress = Bar_ProgressStart( stdout, Aig_ManObjNumMax(p->pAig) * p->pPars->nFramesK ); -// Ssw_ManStartSolver( p ); for ( f = 0; f < p->pPars->nFramesK; f++ ) { // map constants and PIs @@ -318,10 +293,12 @@ clk = clock(); if ( f == p->pPars->nFramesK - 1 ) break; // transfer latch input to the latch outputs + Aig_ManForEachPo( p->pAig, pObj, i ) + Ssw_ObjSetFrame( p, pObj, f, Ssw_ObjChild0Fra(p, pObj, f) ); // build logic cones for register outputs Saig_ManForEachLiLo( p->pAig, pObjLi, pObjLo, i ) { - pObjNew = Ssw_ObjChild0Fra(p, pObjLi,f); + pObjNew = Ssw_ObjFrame( p, pObjLi, f ); Ssw_ObjSetFrame( p, pObjLo, f+1, pObjNew ); Ssw_CnfNodeAddToSolver( p->pMSat, Aig_Regular(pObjNew) );// } @@ -350,7 +327,7 @@ int Ssw_ManSweep( Ssw_Man_t * p ) { Bar_Progress_t * pProgress = NULL; Aig_Obj_t * pObj, * pObj2, * pObjNew; - int nConstrPairs, clk, i, f, v; + int nConstrPairs, clk, i, f; // perform speculative reduction clk = clock(); @@ -380,12 +357,6 @@ clk = clock(); Ssw_ObjSetFrame( p, pObj, f, Aig_ObjCreatePi(p->pFrames) ); p->timeReduce += clock() - clk; - // bring up the previous frames - if ( p->pPars->fUniqueness ) - for ( v = 0; v < f; v++ ) - Saig_ManForEachLo( p->pAig, pObj, i ) - Ssw_CnfNodeAddToSolver( p->pMSat, Aig_Regular(Ssw_ObjFrame(p, pObj, v)) ); - // sweep internal nodes p->fRefined = 0; Ssw_ClassesClearRefined( p->ppClasses ); @@ -417,3 +388,5 @@ p->timeReduce += clock() - clk; //////////////////////////////////////////////////////////////////////// +ABC_NAMESPACE_IMPL_END + diff --git a/src/aig/ssw/sswUnique.c b/src/aig/ssw/sswUnique.c index d6590716..b5f6a853 100644 --- a/src/aig/ssw/sswUnique.c +++ b/src/aig/ssw/sswUnique.c @@ -20,6 +20,9 @@ #include "sswInt.h" +ABC_NAMESPACE_IMPL_START + + //////////////////////////////////////////////////////////////////////// /// DECLARATIONS /// //////////////////////////////////////////////////////////////////////// @@ -100,7 +103,7 @@ int Ssw_ManUniqueOne( Ssw_Man_t * p, Aig_Obj_t * pRepr, Aig_Obj_t * pObj, int fV RetValue = Vec_PtrSize( p->vCommon ); fFeasible = 0; k = 0; - Vec_PtrForEachEntry( p->vCommon, pTemp, i ) + Vec_PtrForEachEntry( Aig_Obj_t *, p->vCommon, pTemp, i ) { assert( Aig_ObjIsPi(pTemp) ); if ( !Saig_ObjIsLo(p->pAig, pTemp) ) @@ -119,7 +122,7 @@ int Ssw_ManUniqueOne( Ssw_Man_t * p, Aig_Obj_t * pRepr, Aig_Obj_t * pObj, int fV // check the current values RetValue = 1; - Vec_PtrForEachEntry( p->vCommon, pTemp, i ) + Vec_PtrForEachEntry( Aig_Obj_t *, p->vCommon, pTemp, i ) { Value0 = Ssw_ManGetSatVarValue( p, pTemp, 0 ); Value1 = Ssw_ManGetSatVarValue( p, pTemp, 1 ); @@ -153,7 +156,7 @@ int Ssw_ManUniqueAddConstraint( Ssw_Man_t * p, Vec_Ptr_t * vCommon, int f1, int assert( Vec_PtrSize(vCommon) > 0 ); // generate the constraint pTotal = Aig_ManConst0(p->pFrames); - Vec_PtrForEachEntry( vCommon, pObj, i ) + Vec_PtrForEachEntry( Aig_Obj_t *, vCommon, pObj, i ) { assert( Saig_ObjIsLo(p->pAig, pObj) ); pObj1New = Ssw_ObjFrame( p, pObj, f1 ); @@ -190,3 +193,5 @@ int Ssw_ManUniqueAddConstraint( Ssw_Man_t * p, Vec_Ptr_t * vCommon, int f1, int //////////////////////////////////////////////////////////////////////// +ABC_NAMESPACE_IMPL_END + -- cgit v1.2.3