diff options
author | Alan Mishchenko <alanmi@berkeley.edu> | 2007-11-30 08:01:00 -0800 |
---|---|---|
committer | Alan Mishchenko <alanmi@berkeley.edu> | 2007-11-30 08:01:00 -0800 |
commit | 369f008e69a4f201cbc7c890a08221086bee4698 (patch) | |
tree | 6dbc56239d2c6cf916c660327525b19773a9907c /src/aig | |
parent | 765a21240891735a844dd64d1d73789ae6e55bc6 (diff) | |
download | abc-369f008e69a4f201cbc7c890a08221086bee4698.tar.gz abc-369f008e69a4f201cbc7c890a08221086bee4698.tar.bz2 abc-369f008e69a4f201cbc7c890a08221086bee4698.zip |
Version abc71130
Diffstat (limited to 'src/aig')
-rw-r--r-- | src/aig/aig/aig.h | 14 | ||||
-rw-r--r-- | src/aig/aig/aigFrames.c | 133 | ||||
-rw-r--r-- | src/aig/aig/aigHaig.c | 270 | ||||
-rw-r--r-- | src/aig/aig/aigMan.c | 53 | ||||
-rw-r--r-- | src/aig/aig/aigObj.c | 17 | ||||
-rw-r--r-- | src/aig/aig/aigOper.c | 9 | ||||
-rw-r--r-- | src/aig/aig/aigRetF.c | 219 | ||||
-rw-r--r-- | src/aig/aig/aigScl.c | 6 | ||||
-rw-r--r-- | src/aig/aig/aigTable.c | 21 | ||||
-rw-r--r-- | src/aig/aig/aigUtil.c | 8 | ||||
-rw-r--r-- | src/aig/fra/fraClau.c | 737 | ||||
-rw-r--r-- | src/aig/fra/fraCore.c | 2 | ||||
-rw-r--r-- | src/aig/fra/fraInd.c | 9 | ||||
-rw-r--r-- | src/aig/fra/fraSec.c | 5 |
14 files changed, 1485 insertions, 18 deletions
diff --git a/src/aig/aig/aig.h b/src/aig/aig/aig.h index 313406c7..b2e0293c 100644 --- a/src/aig/aig/aig.h +++ b/src/aig/aig/aig.h @@ -71,6 +71,7 @@ struct Aig_Obj_t_ // 8 words Aig_Obj_t * pNext; // strashing table Aig_Obj_t * pFanin0; // fanin Aig_Obj_t * pFanin1; // fanin + Aig_Obj_t * pHaig; // pointer to the HAIG node unsigned int Type : 3; // object type unsigned int fPhase : 1; // value under 000...0 pattern unsigned int fMarkA : 1; // multipurpose mask @@ -140,6 +141,7 @@ struct Aig_Man_t_ Vec_Ptr_t * vMapped; Vec_Int_t * vFlopNums; void * pSeqModel; + Aig_Man_t * pManHaig; // timing statistics int time1; int time2; @@ -251,11 +253,14 @@ static inline Aig_Obj_t * Aig_ObjChild0( Aig_Obj_t * pObj ) { return pObj- static inline Aig_Obj_t * Aig_ObjChild1( Aig_Obj_t * pObj ) { return pObj->pFanin1; } static inline Aig_Obj_t * Aig_ObjChild0Copy( Aig_Obj_t * pObj ) { assert( !Aig_IsComplement(pObj) ); return Aig_ObjFanin0(pObj)? Aig_NotCond((Aig_Obj_t *)Aig_ObjFanin0(pObj)->pData, Aig_ObjFaninC0(pObj)) : NULL; } static inline Aig_Obj_t * Aig_ObjChild1Copy( Aig_Obj_t * pObj ) { assert( !Aig_IsComplement(pObj) ); return Aig_ObjFanin1(pObj)? Aig_NotCond((Aig_Obj_t *)Aig_ObjFanin1(pObj)->pData, Aig_ObjFaninC1(pObj)) : NULL; } +static inline void Aig_ObjChild0Flip( Aig_Obj_t * pObj ) { pObj->pFanin0 = Aig_Not(pObj->pFanin0); } +static inline void Aig_ObjChild1Flip( Aig_Obj_t * pObj ) { pObj->pFanin1 = Aig_Not(pObj->pFanin1); } static inline int Aig_ObjLevel( Aig_Obj_t * pObj ) { return pObj->Level; } static inline int Aig_ObjLevelNew( Aig_Obj_t * pObj ) { return Aig_ObjFanin1(pObj)? 1 + Aig_ObjIsExor(pObj) + AIG_MAX(Aig_ObjFanin0(pObj)->Level, Aig_ObjFanin1(pObj)->Level) : Aig_ObjFanin0(pObj)->Level; } static inline void Aig_ObjClean( Aig_Obj_t * pObj ) { memset( pObj, 0, sizeof(Aig_Obj_t) ); } static inline Aig_Obj_t * Aig_ObjFanout0( Aig_Man_t * p, Aig_Obj_t * pObj ) { assert(p->pFanData && pObj->Id < p->nFansAlloc); return Aig_ManObj(p, p->pFanData[5*pObj->Id] >> 1); } -static inline Aig_Obj_t * Aig_ObjEquiv( Aig_Man_t * p, Aig_Obj_t * pObj ) { return p->pEquivs? p->pEquivs[pObj->Id] : NULL; } +static inline Aig_Obj_t * Aig_ObjEquiv( Aig_Man_t * p, Aig_Obj_t * pObj ) { return p->pEquivs? p->pEquivs[pObj->Id] : NULL; } +static inline Aig_Obj_t * Aig_ObjHaig( Aig_Obj_t * pObj ) { assert( Aig_Regular(pObj)->pHaig ); return Aig_NotCond( Aig_Regular(pObj)->pHaig, Aig_IsComplement(pObj) ); } static inline int Aig_ObjWhatFanin( Aig_Obj_t * pObj, Aig_Obj_t * pFanin ) { if ( Aig_ObjFanin0(pObj) == pFanin ) return 0; @@ -398,6 +403,10 @@ extern void Aig_ObjAddFanout( Aig_Man_t * p, Aig_Obj_t * pObj, Aig_Ob extern void Aig_ObjRemoveFanout( Aig_Man_t * p, Aig_Obj_t * pObj, Aig_Obj_t * pFanout ); extern void Aig_ManFanoutStart( Aig_Man_t * p ); extern void Aig_ManFanoutStop( Aig_Man_t * p ); +/*=== aigFrames.c ==========================================================*/ +extern Aig_Man_t * Aig_ManFrames( Aig_Man_t * pAig, int nFs, int fInit, int fOuts, int fRegs, Aig_Obj_t *** ppObjMap ); +/*=== aigHaig.c ==========================================================*/ +extern void Aig_ManHaigRecord( Aig_Man_t * p ); /*=== aigMan.c ==========================================================*/ extern Aig_Man_t * Aig_ManStart( int nNodesMax ); extern Aig_Man_t * Aig_ManStartFrom( Aig_Man_t * p ); @@ -463,6 +472,8 @@ extern Aig_Man_t * Aig_ManRehash( Aig_Man_t * p ); extern void Aig_ManMarkValidChoices( Aig_Man_t * p ); /*=== aigRet.c ========================================================*/ extern Aig_Man_t * Rtm_ManRetime( Aig_Man_t * p, int fForward, int nStepsMax, int fVerbose ); +/*=== aigRetF.c ========================================================*/ +extern Aig_Man_t * Aig_ManRetimeFrontier( Aig_Man_t * p, int nStepsMax ); /*=== aigScl.c ==========================================================*/ extern Aig_Man_t * Aig_ManRemap( Aig_Man_t * p, Vec_Ptr_t * vMap ); extern int Aig_ManSeqCleanup( Aig_Man_t * p ); @@ -479,6 +490,7 @@ extern void Aig_TableInsert( Aig_Man_t * p, Aig_Obj_t * pObj ); extern void Aig_TableDelete( Aig_Man_t * p, Aig_Obj_t * pObj ); extern int Aig_TableCountEntries( Aig_Man_t * p ); extern void Aig_TableProfile( Aig_Man_t * p ); +extern void Aig_TableClear( Aig_Man_t * p ); /*=== aigTiming.c ========================================================*/ extern void Aig_ObjClearReverseLevel( Aig_Man_t * p, Aig_Obj_t * pObj ); extern int Aig_ObjRequiredLevel( Aig_Man_t * p, Aig_Obj_t * pObj ); diff --git a/src/aig/aig/aigFrames.c b/src/aig/aig/aigFrames.c new file mode 100644 index 00000000..dc3efe28 --- /dev/null +++ b/src/aig/aig/aigFrames.c @@ -0,0 +1,133 @@ +/**CFile**************************************************************** + + FileName [aigFrames.c] + + SystemName [ABC: Logic synthesis and verification system.] + + PackageName [AIG package.] + + Synopsis [Performs timeframe expansion of the AIG.] + + Author [Alan Mishchenko] + + Affiliation [UC Berkeley] + + Date [Ver. 1.0. Started - April 28, 2007.] + + Revision [$Id: aigFrames.c,v 1.00 2007/04/28 00:00:00 alanmi Exp $] + +***********************************************************************/ + +#include "aig.h" + +//////////////////////////////////////////////////////////////////////// +/// DECLARATIONS /// +//////////////////////////////////////////////////////////////////////// + +static inline Aig_Obj_t * Aig_ObjFrames( Aig_Obj_t ** pObjMap, int nFs, Aig_Obj_t * pObj, int i ) { return pObjMap[nFs*pObj->Id + i]; } +static inline void Aig_ObjSetFrames( Aig_Obj_t ** pObjMap, int nFs, Aig_Obj_t * pObj, int i, Aig_Obj_t * pNode ) { pObjMap[nFs*pObj->Id + i] = pNode; } + +static inline Aig_Obj_t * Aig_ObjChild0Frames( Aig_Obj_t ** pObjMap, int nFs, Aig_Obj_t * pObj, int i ) { return Aig_ObjFanin0(pObj)? Aig_NotCond(Aig_ObjFrames(pObjMap,nFs,Aig_ObjFanin0(pObj),i), Aig_ObjFaninC0(pObj)) : NULL; } +static inline Aig_Obj_t * Aig_ObjChild1Frames( Aig_Obj_t ** pObjMap, int nFs, Aig_Obj_t * pObj, int i ) { return Aig_ObjFanin1(pObj)? Aig_NotCond(Aig_ObjFrames(pObjMap,nFs,Aig_ObjFanin1(pObj),i), Aig_ObjFaninC1(pObj)) : NULL; } + +//////////////////////////////////////////////////////////////////////// +/// FUNCTION DEFINITIONS /// +//////////////////////////////////////////////////////////////////////// + +/**Function************************************************************* + + Synopsis [Performs timeframe expansion of the AIG.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Aig_Man_t * Aig_ManFrames( Aig_Man_t * pAig, int nFs, int fInit, int fOuts, int fRegs, Aig_Obj_t *** ppObjMap ) +{ + Aig_Man_t * pFrames; + Aig_Obj_t * pObj, * pObjLi, * pObjLo, * pObjNew; + Aig_Obj_t ** pObjMap; + int i, f; + + // create mapping for the frames nodes + pObjMap = ALLOC( Aig_Obj_t *, nFs * Aig_ManObjNumMax(pAig) ); + memset( pObjMap, 0, sizeof(Aig_Obj_t *) * nFs * Aig_ManObjNumMax(pAig) ); + + // start the fraig package + pFrames = Aig_ManStart( Aig_ManObjNumMax(pAig) * nFs ); + pFrames->pName = Aig_UtilStrsav( pAig->pName ); + // map constant nodes + for ( f = 0; f < nFs; f++ ) + Aig_ObjSetFrames( pObjMap, nFs, Aig_ManConst1(pAig), f, Aig_ManConst1(pFrames) ); + // create PI nodes for the frames + for ( f = 0; f < nFs; f++ ) + Aig_ManForEachPiSeq( pAig, pObj, i ) + Aig_ObjSetFrames( pObjMap, nFs, pObj, f, Aig_ObjCreatePi(pFrames) ); + // set initial state for the latches + if ( fInit ) + { + Aig_ManForEachLoSeq( pAig, pObj, i ) + Aig_ObjSetFrames( pObjMap, nFs, pObj, 0, Aig_ManConst0(pFrames) ); + } + else + { + Aig_ManForEachLoSeq( pAig, pObj, i ) + Aig_ObjSetFrames( pObjMap, nFs, pObj, 0, Aig_ObjCreatePi(pFrames) ); + } + + // add timeframes + for ( f = 0; f < nFs; f++ ) + { +// printf( "Frame = %d.\n", f ); + // add internal nodes of this frame + Aig_ManForEachNode( pAig, pObj, i ) + { +// Aig_Obj_t * pFanin0 = Aig_ObjChild0Frames(pObjMap,nFs,pObj,f); +// Aig_Obj_t * pFanin1 = Aig_ObjChild1Frames(pObjMap,nFs,pObj,f); +// printf( "Node = %3d. Fanin0 = %3d. Fanin1 = %3d.\n", pObj->Id, Aig_Regular(pFanin0)->Id, Aig_Regular(pFanin1)->Id ); + pObjNew = Aig_And( pFrames, Aig_ObjChild0Frames(pObjMap,nFs,pObj,f), Aig_ObjChild1Frames(pObjMap,nFs,pObj,f) ); + Aig_ObjSetFrames( pObjMap, nFs, pObj, f, pObjNew ); + } + // set the latch inputs and copy them into the latch outputs of the next frame + Aig_ManForEachLiLoSeq( pAig, pObjLi, pObjLo, i ) + { + pObjNew = Aig_ObjChild0Frames(pObjMap,nFs,pObjLi,f); + if ( f < nFs - 1 ) + Aig_ObjSetFrames( pObjMap, nFs, pObjLo, f+1, pObjNew ); + } + } + if ( fOuts ) + { + for ( f = 0; f < nFs; f++ ) + Aig_ManForEachPoSeq( pAig, pObj, i ) + { + pObjNew = Aig_ObjCreatePo( pFrames, Aig_ObjChild0Frames(pObjMap,nFs,pObj,f) ); + Aig_ObjSetFrames( pObjMap, nFs, pObj, f, pObjNew ); + } + } + if ( fRegs ) + { + pFrames->nRegs = pAig->nRegs; + Aig_ManForEachLiSeq( pAig, pObj, i ) + { + pObjNew = Aig_ObjCreatePo( pFrames, Aig_ObjChild0Frames(pObjMap,nFs,pObj,nFs-1) ); + Aig_ObjSetFrames( pObjMap, nFs, pObj, nFs-1, pObjNew ); + } + } + Aig_ManCleanup( pFrames ); + // return the new manager + if ( ppObjMap ) + *ppObjMap = pObjMap; + else + free( pObjMap ); + return pFrames; +} + +//////////////////////////////////////////////////////////////////////// +/// END OF FILE /// +//////////////////////////////////////////////////////////////////////// + + diff --git a/src/aig/aig/aigHaig.c b/src/aig/aig/aigHaig.c new file mode 100644 index 00000000..273dc723 --- /dev/null +++ b/src/aig/aig/aigHaig.c @@ -0,0 +1,270 @@ +/**CFile**************************************************************** + + FileName [aigHaig.c] + + SystemName [ABC: Logic synthesis and verification system.] + + PackageName [AIG package.] + + Synopsis [] + + Author [Alan Mishchenko] + + Affiliation [UC Berkeley] + + Date [Ver. 1.0. Started - April 28, 2007.] + + Revision [$Id: aigHaig.c,v 1.00 2007/04/28 00:00:00 alanmi Exp $] + +***********************************************************************/ + +#include "aig.h" +#include "satSolver.h" +#include "cnf.h" + +//////////////////////////////////////////////////////////////////////// +/// DECLARATIONS /// +//////////////////////////////////////////////////////////////////////// + +static inline Aig_Obj_t * Aig_HaigObjFrames( Aig_Obj_t ** ppMap, int nFrames, Aig_Obj_t * pObj, int f ) { return ppMap[nFrames*pObj->Id + f]; } +static inline void Aig_HaigObjSetFrames( Aig_Obj_t ** ppMap, int nFrames, Aig_Obj_t * pObj, int f, Aig_Obj_t * pNode ) { ppMap[nFrames*pObj->Id + f] = pNode; } +static inline Aig_Obj_t * Aig_HaigObjChild0Frames( Aig_Obj_t ** ppMap, int nFrames, Aig_Obj_t * pObj, int i ) { assert( !Aig_IsComplement(pObj) ); return Aig_ObjFanin0(pObj)? Aig_NotCond(Aig_HaigObjFrames(ppMap,nFrames,Aig_ObjFanin0(pObj),i), Aig_ObjFaninC0(pObj)) : NULL; } +static inline Aig_Obj_t * Aig_HaigObjChild1Frames( Aig_Obj_t ** ppMap, int nFrames, Aig_Obj_t * pObj, int i ) { assert( !Aig_IsComplement(pObj) ); return Aig_ObjFanin1(pObj)? Aig_NotCond(Aig_HaigObjFrames(ppMap,nFrames,Aig_ObjFanin1(pObj),i), Aig_ObjFaninC1(pObj)) : NULL; } + +//////////////////////////////////////////////////////////////////////// +/// FUNCTION DEFINITIONS /// +//////////////////////////////////////////////////////////////////////// + +/**Function************************************************************* + + Synopsis [Performs speculative reduction for one node.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +static inline void Aig_ManHaigFramesNode( Aig_Obj_t ** ppMap, int nFrames, Aig_Man_t * pFrames, Aig_Obj_t * pObj, int iFrame ) +{ + Aig_Obj_t * pObjNew, * pObjNew2, * pObjRepr, * pObjReprNew, * pMiter; + // skip nodes without representative + pObjRepr = pObj->pHaig; + if ( pObjRepr == NULL ) + return; + assert( !Aig_IsComplement(pObjRepr) ); + assert( pObjRepr->Id < pObj->Id ); + // get the new node + pObjNew = Aig_HaigObjFrames( ppMap, nFrames, pObj, iFrame ); + // get the new node of the representative + pObjReprNew = Aig_HaigObjFrames( ppMap, nFrames, pObjRepr, iFrame ); + // if this is the same node, no need to add constraints + if ( Aig_Regular(pObjNew) == Aig_Regular(pObjReprNew) ) + return; + // these are different nodes - perform speculative reduction + pObjNew2 = Aig_NotCond( pObjReprNew, pObj->fPhase ^ pObjRepr->fPhase ); + // set the new node + Aig_HaigObjSetFrames( ppMap, nFrames, pObj, iFrame, pObjNew2 ); + // add the constraint + pMiter = Aig_Exor( pFrames, Aig_Regular(pObjNew), Aig_Regular(pObjReprNew) ); + pMiter = Aig_NotCond( pMiter, Aig_Regular(pMiter)->fPhase ^ Aig_IsComplement(pMiter) ); + pMiter = Aig_Not( pMiter ); + Aig_ObjCreatePo( pFrames, pMiter ); +} + +/**Function************************************************************* + + Synopsis [Prepares the inductive case with speculative reduction.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Aig_Man_t * Aig_ManHaigFrames( Aig_Man_t * pHaig, int nFrames ) +{ + Aig_Man_t * pFrames; + Aig_Obj_t * pObj, * pObjLi, * pObjLo, * pObjNew; + Aig_Obj_t ** ppMap; + int i, k, f; + assert( nFrames >= 2 ); + assert( Aig_ManRegNum(pHaig) > 0 ); + assert( Aig_ManRegNum(pHaig) < Aig_ManPiNum(pHaig) ); + + // create node mapping + ppMap = ALLOC( Aig_Obj_t *, Aig_ManObjNumMax(pHaig) * nFrames ); + memset( ppMap, 0, sizeof(Aig_Obj_t *) * Aig_ManObjNumMax(pHaig) * nFrames ); + + // start the frames + pFrames = Aig_ManStart( Aig_ManObjNumMax(pHaig) * nFrames ); + pFrames->pName = Aig_UtilStrsav( pHaig->pName ); + pFrames->nRegs = pHaig->nRegs; + + // create PI nodes for the frames + for ( f = 0; f < nFrames; f++ ) + Aig_HaigObjSetFrames( ppMap, nFrames, Aig_ManConst1(pHaig), f, Aig_ManConst1(pFrames) ); + for ( f = 0; f < nFrames; f++ ) + Aig_ManForEachPiSeq( pHaig, pObj, i ) + Aig_HaigObjSetFrames( ppMap, nFrames, pObj, f, Aig_ObjCreatePi(pFrames) ); + // create latches for the first frame + Aig_ManForEachLoSeq( pHaig, pObj, i ) + Aig_HaigObjSetFrames( ppMap, nFrames, pObj, 0, Aig_ObjCreatePi(pFrames) ); + + // add timeframes + for ( f = 0; f < nFrames; f++ ) + { + // mark the asserts + if ( f == nFrames - 1 ) + pFrames->nAsserts = Aig_ManPoNum(pFrames); + // constrain latch outputs and internal nodes + Aig_ManForEachObj( pHaig, pObj, i ) + { + if ( Aig_ObjIsPi(pObj) && Aig_HaigObjFrames(ppMap, nFrames, pObj, f) == NULL ) + { + Aig_ManHaigFramesNode( ppMap, nFrames, pFrames, pObj, f ); + } + else if ( Aig_ObjIsNode(pObj) ) + { + pObjNew = Aig_And( pFrames, + Aig_HaigObjChild0Frames(ppMap,nFrames,pObj,f), + Aig_HaigObjChild1Frames(ppMap,nFrames,pObj,f) ); + Aig_HaigObjSetFrames( ppMap, nFrames, pObj, f, pObjNew ); + Aig_ManHaigFramesNode( ppMap, nFrames, pFrames, pObj, f ); + } + } + +/* + // set the constraints on the latch outputs + Aig_ManForEachLoSeq( pHaig, pObj, i ) + Aig_ManHaigFramesNode( ppMap, nFrames, pFrames, pObj, f ); + // add internal nodes of this frame + Aig_ManForEachNode( pHaig, pObj, i ) + { + pObjNew = Aig_And( pFrames, + Aig_HaigObjChild0Frames(ppMap,nFrames,pObj,f), + Aig_HaigObjChild1Frames(ppMap,nFrames,pObj,f) ); + Aig_HaigObjSetFrames( ppMap, nFrames, pObj, f, pObjNew ); + Aig_ManHaigFramesNode( ppMap, nFrames, pFrames, pObj, f ); + } +*/ + // transfer latch inputs to the latch outputs + Aig_ManForEachLiLoSeq( pHaig, pObjLi, pObjLo, k ) + { + pObjNew = Aig_HaigObjChild0Frames(ppMap,nFrames,pObjLi,f); + Aig_HaigObjSetFrames( ppMap, nFrames, pObjLo, f+1, pObjNew ); + } + } + + // remove dangling nodes + Aig_ManCleanup( pFrames ); + free( ppMap ); + return pFrames; +} + +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Aig_ManHaigVerify( Aig_Man_t * pHaig ) +{ + int nBTLimit = 0; + Aig_Man_t * pFrames; + Cnf_Dat_t * pCnf; + sat_solver * pSat; + Aig_Obj_t * pObj; + int i, Lit, RetValue, Counter; + int clk = clock(); + + // create time frames with speculative reduction and convert them into CNF +clk = clock(); + pFrames = Aig_ManHaigFrames( pHaig, 2 ); + pCnf = Cnf_DeriveSimple( pFrames, Aig_ManPoNum(pFrames) - pFrames->nAsserts ); +// pCnf = Cnf_Derive( pFrames, Aig_ManPoNum(pFrames) - pFrames->nAsserts ); +//Cnf_DataWriteIntoFile( pCnf, "temp.cnf", 1 ); + // create the SAT solver to be used for this problem + pSat = Cnf_DataWriteIntoSolver( pCnf ); + + printf( "HAIG regs = %d. HAIG nodes = %d. Outputs = %d.\n", + Aig_ManRegNum(pHaig), Aig_ManNodeNum(pHaig), Aig_ManPoNum(pHaig) ); + printf( "Frames regs = %d. Frames nodes = %d. Outputs = %d. Assumptions = %d. Asserts = %d.\n", + Aig_ManRegNum(pFrames), Aig_ManNodeNum(pFrames), Aig_ManPoNum(pFrames), + pFrames->nAsserts, Aig_ManPoNum(pFrames) - pFrames->nAsserts ); + +PRT( "Preparation", clock() - clk ); + if ( pSat == NULL ) + { + printf( "Aig_ManHaigVerify(): Computed CNF is not valid.\n" ); + return -1; + } + + // solve each output +clk = clock(); + Counter = 0; + Aig_ManForEachPo( pFrames, pObj, i ) + { + if ( i < pFrames->nAsserts ) + continue; + Lit = toLitCond( pCnf->pVarNums[pObj->Id], pObj->fPhase ); + RetValue = sat_solver_solve( pSat, &Lit, &Lit + 1, (sint64)nBTLimit, (sint64)0, (sint64)0, (sint64)0 ); + if ( RetValue != l_False ) + Counter++; + } +PRT( "Solving ", clock() - clk ); + if ( Counter ) + printf( "Verification failed for %d classes.\n", Counter ); + else + printf( "Verification is successful.\n" ); + + // clean up + Aig_ManStop( pFrames ); + Cnf_DataFree( pCnf ); + sat_solver_delete( pSat ); + return Counter; +} + +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Aig_ManHaigRecord( Aig_Man_t * p ) +{ + Aig_Man_t * pNew; + Aig_Obj_t * pObj; + int i; + // start the HAIG + p->pManHaig = Aig_ManDup( p, 1 ); + // set the pointers to the HAIG nodes + Aig_ManForEachObj( p, pObj, i ) + pObj->pHaig = pObj->pData; + // remove structural hashing table + Aig_TableClear( p->pManHaig ); + // perform a sequence of synthesis steps + pNew = Aig_ManRetimeFrontier( p, 10000 ); + // use the haig for verification + Aig_ManDumpBlif( pNew->pManHaig, "haig_temp.blif" ); + Aig_ManHaigVerify( pNew->pManHaig ); + Aig_ManStop( pNew ); +} + +//////////////////////////////////////////////////////////////////////// +/// END OF FILE /// +//////////////////////////////////////////////////////////////////////// + + diff --git a/src/aig/aig/aigMan.c b/src/aig/aig/aigMan.c index 71ec389e..b915df99 100644 --- a/src/aig/aig/aigMan.c +++ b/src/aig/aig/aigMan.c @@ -115,7 +115,14 @@ Aig_Obj_t * Aig_ManDup_rec( Aig_Man_t * pNew, Aig_Man_t * p, Aig_Obj_t * pObj ) if ( Aig_ObjIsBuf(pObj) ) return pObj->pData = Aig_ObjChild0Copy(pObj); Aig_ManDup_rec( pNew, p, Aig_ObjFanin1(pObj) ); - return pObj->pData = Aig_And( pNew, Aig_ObjChild0Copy(pObj), Aig_ObjChild1Copy(pObj) ); + if ( pNew->pManHaig == NULL ) + return pObj->pData = Aig_And( pNew, Aig_ObjChild0Copy(pObj), Aig_ObjChild1Copy(pObj) ); + else + { + Aig_Obj_t * pObjNew = Aig_And( pNew, Aig_ObjChild0Copy(pObj), Aig_ObjChild1Copy(pObj) ); + Aig_Regular(pObjNew->pHaig)->pHaig = Aig_Regular(pObj->pHaig); + return pObj->pData = pObjNew; + } } /**Function************************************************************* @@ -132,28 +139,52 @@ Aig_Obj_t * Aig_ManDup_rec( Aig_Man_t * pNew, Aig_Man_t * p, Aig_Obj_t * pObj ) Aig_Man_t * Aig_ManDup( Aig_Man_t * p, int fOrdered ) { Aig_Man_t * pNew; - Aig_Obj_t * pObj; + Aig_Obj_t * pObj, * pObjNew; int i; // create the new manager pNew = Aig_ManStart( Aig_ManObjNumMax(p) ); pNew->pName = Aig_UtilStrsav( p->pName ); pNew->nRegs = p->nRegs; pNew->nAsserts = p->nAsserts; + pNew->pManHaig = p->pManHaig; if ( p->vFlopNums ) pNew->vFlopNums = Vec_IntDup( p->vFlopNums ); // create the PIs Aig_ManCleanData( p ); Aig_ManConst1(p)->pData = Aig_ManConst1(pNew); + Aig_ManConst1(pNew)->pHaig = Aig_ManConst1(p)->pHaig; Aig_ManForEachPi( p, pObj, i ) - pObj->pData = Aig_ObjCreatePi(pNew); + { + pObjNew = Aig_ObjCreatePi( pNew ); + pObjNew->pHaig = pObj->pHaig; + pObj->pData = pObjNew; + } // duplicate internal nodes if ( fOrdered ) { Aig_ManForEachObj( p, pObj, i ) if ( Aig_ObjIsBuf(pObj) ) - pObj->pData = Aig_ObjChild0Copy(pObj); + { + if ( pNew->pManHaig == NULL ) + pObj->pData = Aig_ObjChild0Copy(pObj); + else + { + Aig_Obj_t * pObjNew = Aig_ObjChild0Copy(pObj); + Aig_Regular(pObjNew->pHaig)->pHaig = Aig_Regular(pObj->pHaig); + pObj->pData = pObjNew; + } + } else if ( Aig_ObjIsNode(pObj) ) - pObj->pData = Aig_And( pNew, Aig_ObjChild0Copy(pObj), Aig_ObjChild1Copy(pObj) ); + { + if ( pNew->pManHaig == NULL ) + pObj->pData = Aig_And( pNew, Aig_ObjChild0Copy(pObj), Aig_ObjChild1Copy(pObj) ); + else + { + Aig_Obj_t * pObjNew = Aig_And( pNew, Aig_ObjChild0Copy(pObj), Aig_ObjChild1Copy(pObj) ); + Aig_Regular(pObjNew->pHaig)->pHaig = Aig_Regular(pObj->pHaig); + pObj->pData = pObjNew; + } + } } else { @@ -166,8 +197,16 @@ Aig_Man_t * Aig_ManDup( Aig_Man_t * p, int fOrdered ) } // add the POs Aig_ManForEachPo( p, pObj, i ) - Aig_ObjCreatePo( pNew, Aig_ObjChild0Copy(pObj) ); + { + pObjNew = Aig_ObjCreatePo( pNew, Aig_ObjChild0Copy(pObj) ); + pObjNew->pHaig = pObj->pHaig; + pObj->pData = pObjNew; + } assert( Aig_ManBufNum(p) != 0 || Aig_ManNodeNum(p) == Aig_ManNodeNum(pNew) ); + // pass the HAIG to the new AIG + p->pManHaig = NULL; + Aig_ManForEachObj( p, pObj, i ) + pObj->pHaig = NULL; // check the resulting network if ( !Aig_ManCheck(pNew) ) printf( "Aig_ManDup(): The check has failed.\n" ); @@ -228,6 +267,8 @@ void Aig_ManStop( Aig_Man_t * p ) { Aig_Obj_t * pObj; int i; + if ( p->pManHaig ) + Aig_ManStop( p->pManHaig ); if ( p->vMapped ) Vec_PtrFree( p->vMapped ); // print time diff --git a/src/aig/aig/aigObj.c b/src/aig/aig/aigObj.c index 8323249e..80838e19 100644 --- a/src/aig/aig/aigObj.c +++ b/src/aig/aig/aigObj.c @@ -88,7 +88,7 @@ Aig_Obj_t * Aig_ObjCreate( Aig_Man_t * p, Aig_Obj_t * pGhost ) Aig_Obj_t * pObj; assert( !Aig_IsComplement(pGhost) ); assert( Aig_ObjIsHash(pGhost) ); - assert( pGhost == &p->Ghost ); +// assert( pGhost == &p->Ghost ); // get memory for the new object pObj = Aig_ManFetchMemory( p ); pObj->Type = pGhost->Type; @@ -97,6 +97,12 @@ Aig_Obj_t * Aig_ObjCreate( Aig_Man_t * p, Aig_Obj_t * pGhost ) // update node counters of the manager p->nObjs[Aig_ObjType(pObj)]++; assert( pObj->pData == NULL ); + if ( p->pManHaig ) + { + pGhost->pFanin0 = Aig_ObjHaig( pGhost->pFanin0 ); + pGhost->pFanin1 = Aig_ObjHaig( pGhost->pFanin1 ); + pObj->pHaig = Aig_ObjCreate( p->pManHaig, pGhost ); + } return pObj; } @@ -365,6 +371,13 @@ void Aig_ObjReplace( Aig_Man_t * p, Aig_Obj_t * pObjOld, Aig_Obj_t * pObjNew, in // make sure object is not pointing to itself assert( pObjOld != Aig_ObjFanin0(pObjNewR) ); assert( pObjOld != Aig_ObjFanin1(pObjNewR) ); + // map the HAIG nodes + if ( p->pManHaig != NULL ) + { + assert( pObjNewR->pHaig != NULL ); + assert( pObjNewR->pHaig->pHaig == NULL ); + pObjNewR->pHaig->pHaig = pObjOld->pHaig; + } // recursively delete the old node - but leave the object there pObjNewR->nRefs++; Aig_ObjDelete_rec( p, pObjOld, 0 ); @@ -385,6 +398,8 @@ void Aig_ObjReplace( Aig_Man_t * p, Aig_Obj_t * pObjOld, Aig_Obj_t * pObjNew, in pObjOld->Type = pObjNew->Type; Aig_ObjDisconnect( p, pObjNew ); Aig_ObjConnect( p, pObjOld, pFanin0, pFanin1 ); + // update the haig node + pObjOld->pHaig = pObjNew->pHaig; // delete the new object Aig_ObjDelete( p, pObjNew ); // update levels diff --git a/src/aig/aig/aigOper.c b/src/aig/aig/aigOper.c index 66a6dce1..c19f551e 100644 --- a/src/aig/aig/aigOper.c +++ b/src/aig/aig/aigOper.c @@ -139,6 +139,15 @@ Aig_Obj_t * Aig_And( Aig_Man_t * p, Aig_Obj_t * p0, Aig_Obj_t * p1 ) { Aig_Obj_t * pGhost, * pResult; // Aig_Obj_t * pFan0, * pFan1; + if ( p->pTable == NULL ) + { +// pGhost = Aig_ObjCreateGhost( p, p0, p1, AIG_OBJ_AND ); + pGhost = Aig_ManGhost(p); + pGhost->Type = AIG_OBJ_AND; + pGhost->pFanin0 = p0; + pGhost->pFanin1 = p1; + return Aig_ObjCreate( p, pGhost ); + } // check trivial cases if ( p0 == p1 ) return p0; diff --git a/src/aig/aig/aigRetF.c b/src/aig/aig/aigRetF.c new file mode 100644 index 00000000..8ca4fba1 --- /dev/null +++ b/src/aig/aig/aigRetF.c @@ -0,0 +1,219 @@ +/**CFile**************************************************************** + + FileName [aigRetF.c] + + SystemName [ABC: Logic synthesis and verification system.] + + PackageName [AIG package.] + + Synopsis [Retiming frontier.] + + Author [Alan Mishchenko] + + Affiliation [UC Berkeley] + + Date [Ver. 1.0. Started - April 28, 2007.] + + Revision [$Id: aigRetF.c,v 1.00 2007/04/28 00:00:00 alanmi Exp $] + +***********************************************************************/ + +#include "aig.h" + +//////////////////////////////////////////////////////////////////////// +/// DECLARATIONS /// +//////////////////////////////////////////////////////////////////////// + +//////////////////////////////////////////////////////////////////////// +/// FUNCTION DEFINITIONS /// +//////////////////////////////////////////////////////////////////////// + +/**Function************************************************************* + + Synopsis [Mark the nodes reachable from the PIs in the reverse order.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Aig_ManRetimeMark_rec( Aig_Man_t * p, Aig_Obj_t * pObj ) +{ + if ( pObj->fMarkB ) + return 1; + if ( Aig_ObjIsPi(pObj) || Aig_ObjIsConst1(pObj) ) + return 0; + if ( Aig_ObjIsTravIdCurrent(p, pObj) ) + return pObj->fMarkB; + Aig_ObjSetTravIdCurrent(p, pObj); + if ( Aig_ManRetimeMark_rec( p, Aig_ObjFanin0(pObj) ) ) + return pObj->fMarkB = 1; + if ( Aig_ObjIsNode(pObj) && Aig_ManRetimeMark_rec( p, Aig_ObjFanin1(pObj) ) ) + return pObj->fMarkB = 1; + assert( pObj->fMarkB == 0 ); + return 0; +} + +/**Function************************************************************* + + Synopsis [Mark the nodes reachable from the true PIs.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Aig_ManRetimeMark( Aig_Man_t * p ) +{ + Aig_Obj_t * pObj, * pObjLi, * pObjLo; + int fChange, i; + // mark the PIs + Aig_ManForEachObj( p, pObj, i ) + assert( pObj->fMarkB == 0 ); + Aig_ManForEachPiSeq( p, pObj, i ) + pObj->fMarkB = 1; + // map registers into each other + Aig_ManForEachLiLoSeq( p, pObjLi, pObjLo, i ) + { + assert( pObjLo->pNext == NULL ); + assert( pObjLi->pNext == NULL ); + pObjLo->pNext = pObjLi; + pObjLi->pNext = pObjLo; + } + // iterativively mark the logic reachable from PIs + fChange = 1; + while ( fChange ) + { + fChange = 0; + Aig_ManIncrementTravId( p ); + Aig_ManForEachPo( p, pObj, i ) + { + if ( pObj->fMarkB ) + continue; + if ( Aig_ManRetimeMark_rec( p, pObj ) ) + { + if ( pObj->pNext ) + pObj->pNext->fMarkB = 1; + fChange = 1; + } + } + } + // clean register mapping + Aig_ManForEachLiLoSeq( p, pObjLi, pObjLo, i ) + pObjLo->pNext = pObjLi->pNext = NULL; +} + + +/**Function************************************************************* + + Synopsis [Performs forward retiming.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Aig_Man_t * Aig_ManRetimeFrontier( Aig_Man_t * p, int nStepsMax ) +{ + Aig_Obj_t * pObj, * pObjNew, * pObjLo, * pObjLo0, * pObjLo1, * pObjLi, * pObjLi0, * pObjLi1;//, * pObjLi0_, * pObjLi1_, * pObjLi0__, * pObjLi1__; + int i, Counter, fCompl, fChange; + assert( Aig_ManRegNum(p) > 0 ); + // remove structural hashing table + Aig_TableClear( p ); + // mark the retimable nodes + Aig_ManRetimeMark( p ); + // mark the register outputs + Aig_ManForEachLiLoSeq( p, pObjLi, pObjLo, i ) + { + pObjLo->fMarkA = 1; + pObjLo->pNext = pObjLi; + pObjLi->pNext = pObjLo; + } + // go through the nodes and find retimable ones + Counter = 0; + fChange = 1; + while ( fChange ) + { + fChange = 0; + Aig_ManForEachNode( p, pObj, i ) + { + if ( !pObj->fMarkB ) + continue; + if ( Aig_ObjIsBuf(pObj) ) + continue; + // get the real inputs of the node (skipping the buffers) + pObjLo0 = Aig_ObjReal_rec( Aig_ObjChild0(pObj) ); + pObjLo1 = Aig_ObjReal_rec( Aig_ObjChild1(pObj) ); + if ( !Aig_Regular(pObjLo0)->fMarkA || !Aig_Regular(pObjLo1)->fMarkA ) + continue; + // remember complemented attribute + fCompl = Aig_IsComplement(pObjLo0) & Aig_IsComplement(pObjLo1); + // get the register inputs +// pObjLi0_ = Aig_Regular(pObjLo0)->pNext; +// pObjLi1_ = Aig_Regular(pObjLo1)->pNext; +// pObjLi0__ = Aig_ObjChild0(Aig_Regular(pObjLo0)->pNext); +// pObjLi1__ = Aig_ObjChild0(Aig_Regular(pObjLo1)->pNext); + pObjLi0 = Aig_NotCond( Aig_ObjChild0(Aig_Regular(pObjLo0)->pNext), Aig_IsComplement(pObjLo0) ); + pObjLi1 = Aig_NotCond( Aig_ObjChild0(Aig_Regular(pObjLo1)->pNext), Aig_IsComplement(pObjLo1) ); + // create new node + pObjNew = Aig_And( p, pObjLi0, pObjLi1 ); + pObjNew->fMarkB = 1; + // create new register + pObjLo = Aig_ObjCreatePi(p); + pObjLo->fMarkA = 1; + pObjLi = Aig_ObjCreatePo( p, Aig_NotCond(pObjNew, fCompl) ); + p->nRegs++; + pObjLo->pNext = pObjLi; + pObjLi->pNext = pObjLo; + // add the buffer + Aig_ObjDisconnect( p, pObj ); + pObj->Type = AIG_OBJ_BUF; + p->nObjs[AIG_OBJ_AND]--; + p->nObjs[AIG_OBJ_BUF]++; + Aig_ObjConnect( p, pObj, Aig_NotCond(pObjLo, fCompl), NULL ); + // create HAIG if defined + if ( p->pManHaig ) + { + // create HAIG latch + pObjLo->pHaig = Aig_ObjCreatePi( p->pManHaig ); + pObjLi->pHaig = Aig_ObjCreatePo( p->pManHaig, Aig_ObjHaig( Aig_ObjChild0(pObjLi) ) ); + // create equivalence class + assert( pObjLo->pHaig != NULL ); + assert( pObjLo->pHaig->pHaig == NULL ); + pObjLo->pHaig->pHaig = Aig_Regular(pObj->pHaig); + } + // mark the change + fChange = 1; + // check the limit + if ( ++Counter >= nStepsMax ) + { + fChange = 0; + break; + } + } + } + // clean the markings + Aig_ManForEachLiLoSeq( p, pObjLi, pObjLo, i ) + { + pObjLo->fMarkA = 0; + pObjLo->pNext = pObjLi->pNext = NULL; + } + Aig_ManForEachObj( p, pObj, i ) + pObj->fMarkB = 0; + // remove useless registers + Aig_ManSeqCleanup( p ); + // rehash the nodes + return Aig_ManDup( p, 1 ); +} + +//////////////////////////////////////////////////////////////////////// +/// END OF FILE /// +//////////////////////////////////////////////////////////////////////// + + diff --git a/src/aig/aig/aigScl.c b/src/aig/aig/aigScl.c index aae088a3..9721dd17 100644 --- a/src/aig/aig/aigScl.c +++ b/src/aig/aig/aigScl.c @@ -32,7 +32,7 @@ Synopsis [Remaps the manager.] - Description [Map in the array specifies for each CI nodes the node that + Description [Map in the array specifies for each CI node the node that should be used after remapping.] SideEffects [] @@ -101,7 +101,7 @@ void Aig_ManSeqCleanup_rec( Aig_Man_t * p, Aig_Obj_t * pObj, Vec_Ptr_t * vNodes Vec_PtrPush( vNodes, pObj->pNext ); return; } - if ( Aig_ObjIsPo(pObj) ) + if ( Aig_ObjIsPo(pObj) || Aig_ObjIsBuf(pObj) ) { Aig_ManSeqCleanup_rec( p, Aig_ObjFanin0(pObj), vNodes ); return; @@ -127,7 +127,7 @@ int Aig_ManSeqCleanup( Aig_Man_t * p ) Vec_Ptr_t * vNodes, * vCis, * vCos; Aig_Obj_t * pObj, * pObjLi, * pObjLo; int i, nTruePis, nTruePos; - assert( Aig_ManBufNum(p) == 0 ); +// assert( Aig_ManBufNum(p) == 0 ); // mark the PIs Aig_ManIncrementTravId( p ); diff --git a/src/aig/aig/aigTable.c b/src/aig/aig/aigTable.c index 94593d70..357b63c3 100644 --- a/src/aig/aig/aigTable.c +++ b/src/aig/aig/aigTable.c @@ -184,6 +184,8 @@ Aig_Obj_t * Aig_TableLookupTwo( Aig_Man_t * p, Aig_Obj_t * pFanin0, Aig_Obj_t * void Aig_TableInsert( Aig_Man_t * p, Aig_Obj_t * pObj ) { Aig_Obj_t ** ppPlace; + if ( p->pTable == NULL ) + return; assert( !Aig_IsComplement(pObj) ); assert( Aig_TableLookup(p, pObj) == NULL ); if ( (pObj->Id & 0xFF) == 0 && 2 * p->nTableSize < Aig_ManNodeNum(p) ) @@ -207,6 +209,8 @@ void Aig_TableInsert( Aig_Man_t * p, Aig_Obj_t * pObj ) void Aig_TableDelete( Aig_Man_t * p, Aig_Obj_t * pObj ) { Aig_Obj_t ** ppPlace; + if ( p->pTable == NULL ) + return; assert( !Aig_IsComplement(pObj) ); ppPlace = Aig_TableFind( p, pObj ); assert( *ppPlace == pObj ); // node should be in the table @@ -261,6 +265,23 @@ void Aig_TableProfile( Aig_Man_t * p ) } } +/**Function******************************************************************** + + Synopsis [Profiles the hash table.] + + Description [] + + SideEffects [] + + SeeAlso [] + +******************************************************************************/ +void Aig_TableClear( Aig_Man_t * p ) +{ + FREE( p->pTable ); + p->nTableSize = 0; +} + //////////////////////////////////////////////////////////////////////// /// END OF FILE /// //////////////////////////////////////////////////////////////////////// diff --git a/src/aig/aig/aigUtil.c b/src/aig/aig/aigUtil.c index b70d11c7..354d94db 100644 --- a/src/aig/aig/aigUtil.c +++ b/src/aig/aig/aigUtil.c @@ -649,7 +649,7 @@ void Aig_ManDump( Aig_Man_t * p ) /**Function************************************************************* - Synopsis [Writes the AIG into the BLIF file.] + Synopsis [Writes the AIG into a BLIF file.] Description [] @@ -680,7 +680,7 @@ void Aig_ManDumpBlif( Aig_Man_t * p, char * pFileName ) Vec_PtrForEachEntry( vNodes, pObj, i ) pObj->iData = Counter++; nDigits = Aig_Base10Log( Counter ); - // write the file + // write the file pFile = fopen( pFileName, "w" ); fprintf( pFile, "# BLIF file written by procedure Aig_ManDumpBlif()\n" ); // fprintf( pFile, "# http://www.eecs.berkeley.edu/~alanmi/abc/\n" ); @@ -702,7 +702,7 @@ void Aig_ManDumpBlif( Aig_Man_t * p, char * pFileName ) Aig_ManForEachLiLoSeq( p, pObjLi, pObjLo, i ) fprintf( pFile, ".latch n%0*d n%0*d 0\n", nDigits, pObjLi->iData, nDigits, pObjLo->iData ); fprintf( pFile, "\n" ); - } + } // write nodes Vec_PtrForEachEntry( vNodes, pObj, i ) { @@ -731,7 +731,7 @@ void Aig_ManDumpBlif( Aig_Man_t * p, char * pFileName ) /**Function************************************************************* - Synopsis [Writes the AIG into the BLIF file.] + Synopsis [Writes the AIG into a Verilog file.] Description [] diff --git a/src/aig/fra/fraClau.c b/src/aig/fra/fraClau.c new file mode 100644 index 00000000..ea71c83b --- /dev/null +++ b/src/aig/fra/fraClau.c @@ -0,0 +1,737 @@ +/**CFile**************************************************************** + + FileName [fraClau.c] + + SystemName [ABC: Logic synthesis and verification system.] + + PackageName [New FRAIG package.] + + Synopsis [Induction with clause strengthening.] + + Author [Alan Mishchenko] + + Affiliation [UC Berkeley] + + Date [Ver. 1.0. Started - June 30, 2007.] + + Revision [$Id: fraClau.c,v 1.00 2007/06/30 00:00:00 alanmi Exp $] + +***********************************************************************/ + +#include "fra.h" +#include "cnf.h" +#include "satSolver.h" + +/* + This code is inspired by the paper: Aaron Bradley and Zohar Manna, + "Checking safety by inductive generalization of counterexamples to + induction", FMCAD '07. +*/ + +//////////////////////////////////////////////////////////////////////// +/// DECLARATIONS /// +//////////////////////////////////////////////////////////////////////// + +typedef struct Cla_Man_t_ Cla_Man_t; +struct Cla_Man_t_ +{ + // SAT solvers + sat_solver * pSatMain; + sat_solver * pSatTest; + sat_solver * pSatBmc; + // CNF for the test solver +// Cnf_Dat_t * pCnfTest; + // SAT variables + Vec_Int_t * vSatVarsMainCs; + Vec_Int_t * vSatVarsTestCs; + Vec_Int_t * vSatVarsTestNs; + Vec_Int_t * vSatVarsBmcNs; + // helper variables + int nSatVarsTestBeg; + int nSatVarsTestCur; + // counter-examples + Vec_Int_t * vCexMain0; + Vec_Int_t * vCexMain; + Vec_Int_t * vCexTest; + Vec_Int_t * vCexBase; + Vec_Int_t * vCexAssm; + Vec_Int_t * vCexBmc; + // mapping of CS into NS var numbers + int * pMapCsMainToCsTest; + int * pMapCsTestToCsMain; + int * pMapCsTestToNsTest; + int * pMapCsTestToNsBmc; +}; + +//////////////////////////////////////////////////////////////////////// +/// FUNCTION DEFINITIONS /// +//////////////////////////////////////////////////////////////////////// + +/**Function************************************************************* + + Synopsis [Saves variables corresponding to latch outputs.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Vec_Int_t * Fra_ClauSaveLatchVars( Aig_Man_t * pMan, Cnf_Dat_t * pCnf, int fCsVars ) +{ + Vec_Int_t * vVars; + Aig_Obj_t * pObjLo, * pObjLi; + int i; + vVars = Vec_IntAlloc( Aig_ManRegNum(pMan) ); + Aig_ManForEachLiLoSeq( pMan, pObjLi, pObjLo, i ) + Vec_IntPush( vVars, pCnf->pVarNums[fCsVars? pObjLo->Id : pObjLi->Id] ); + return vVars; +} + +/**Function************************************************************* + + Synopsis [Saves variables corresponding to latch outputs.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Vec_Int_t * Fra_ClauSaveOutputVars( Aig_Man_t * pMan, Cnf_Dat_t * pCnf ) +{ + Vec_Int_t * vVars; + Aig_Obj_t * pObj; + int i; + vVars = Vec_IntAlloc( Aig_ManPoNum(pMan) ); + Aig_ManForEachPo( pMan, pObj, i ) + Vec_IntPush( vVars, pCnf->pVarNums[pObj->Id] ); + return vVars; +} + +/**Function************************************************************* + + Synopsis [Saves variables corresponding to latch outputs.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Vec_Int_t * Fra_ClauSaveInputVars( Aig_Man_t * pMan, Cnf_Dat_t * pCnf, int nStarting ) +{ + Vec_Int_t * vVars; + Aig_Obj_t * pObj; + int i; + vVars = Vec_IntAlloc( Aig_ManPiNum(pMan) - nStarting ); + Aig_ManForEachPi( pMan, pObj, i ) + { + if ( i < nStarting ) + continue; + Vec_IntPush( vVars, pCnf->pVarNums[pObj->Id] ); + } + return vVars; +} + +/**Function************************************************************* + + Synopsis [Saves variables corresponding to latch outputs.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int * Fra_ClauCreateMapping( Vec_Int_t * vSatVarsFrom, Vec_Int_t * vSatVarsTo, int nVarsMax ) +{ + int * pMapping, Var, i; + assert( Vec_IntSize(vSatVarsFrom) == Vec_IntSize(vSatVarsTo) ); + pMapping = ALLOC( int, nVarsMax ); + for ( i = 0; i < nVarsMax; i++ ) + pMapping[i] = -1; + Vec_IntForEachEntry( vSatVarsFrom, Var, i ) + pMapping[Var] = Vec_IntEntry(vSatVarsTo,i); + return pMapping; +} + + +/**Function************************************************************* + + Synopsis [Deletes the manager.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Fra_ClauStop( Cla_Man_t * p ) +{ + free( p->pMapCsMainToCsTest ); + free( p->pMapCsTestToCsMain ); + free( p->pMapCsTestToNsTest ); + free( p->pMapCsTestToNsBmc ); + Vec_IntFree( p->vSatVarsMainCs ); + Vec_IntFree( p->vSatVarsTestCs ); + Vec_IntFree( p->vSatVarsTestNs ); + Vec_IntFree( p->vSatVarsBmcNs ); + Vec_IntFree( p->vCexMain0 ); + Vec_IntFree( p->vCexMain ); + Vec_IntFree( p->vCexTest ); + Vec_IntFree( p->vCexBase ); + Vec_IntFree( p->vCexAssm ); + Vec_IntFree( p->vCexBmc ); + if ( p->pSatMain ) sat_solver_delete( p->pSatMain ); + if ( p->pSatTest ) sat_solver_delete( p->pSatTest ); + if ( p->pSatBmc ) sat_solver_delete( p->pSatBmc ); + free( p ); +} + +/**Function************************************************************* + + Synopsis [Takes the AIG with the single output to be checked.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Cla_Man_t * Fra_ClauStart( Aig_Man_t * pMan ) +{ + Cla_Man_t * p; + Cnf_Dat_t * pCnfMain; + Cnf_Dat_t * pCnfTest; + Cnf_Dat_t * pCnfBmc; + Aig_Man_t * pFramesMain; + Aig_Man_t * pFramesTest; + Aig_Man_t * pFramesBmc; + assert( Aig_ManPoNum(pMan) - Aig_ManRegNum(pMan) == 1 ); + + // start the manager + p = ALLOC( Cla_Man_t, 1 ); + memset( p, 0, sizeof(Cla_Man_t) ); + p->vCexMain0 = Vec_IntAlloc( Aig_ManRegNum(pMan) ); + p->vCexMain = Vec_IntAlloc( Aig_ManRegNum(pMan) ); + p->vCexTest = Vec_IntAlloc( Aig_ManRegNum(pMan) ); + p->vCexBase = Vec_IntAlloc( Aig_ManRegNum(pMan) ); + p->vCexAssm = Vec_IntAlloc( Aig_ManRegNum(pMan) ); + p->vCexBmc = Vec_IntAlloc( Aig_ManRegNum(pMan) ); + + // derive two timeframes to be checked + pFramesMain = Aig_ManFrames( pMan, 2, 0, 1, 0, NULL ); // nFrames, fInit, fOuts, fRegs +//Aig_ManShow( pFramesMain, 0, NULL ); + assert( Aig_ManPoNum(pFramesMain) == 2 ); + Aig_ObjChild0Flip( Aig_ManPo(pFramesMain, 0) ); // complement the first output + pCnfMain = Cnf_DeriveSimple( pFramesMain, 0 ); +//Cnf_DataWriteIntoFile( pCnfMain, "temp.cnf", 1 ); + p->pSatMain = Cnf_DataWriteIntoSolver( pCnfMain ); +/* + { + int i; + Aig_Obj_t * pObj; + Aig_ManForEachObj( pFramesMain, pObj, i ) + printf( "%d -> %d \n", pObj->Id, pCnfMain->pVarNums[pObj->Id] ); + printf( "\n" ); + } +*/ + + // derive one timeframe to be checked + pFramesTest = Aig_ManFrames( pMan, 1, 0, 0, 1, NULL ); + assert( Aig_ManPoNum(pFramesTest) == Aig_ManRegNum(pMan) ); + pCnfTest = Cnf_DeriveSimple( pFramesTest, Aig_ManRegNum(pMan) ); + p->pSatTest = Cnf_DataWriteIntoSolver( pCnfTest ); + p->nSatVarsTestBeg = p->nSatVarsTestCur = sat_solver_nvars( p->pSatTest ); + + // derive one timeframe to be checked for BMC + pFramesBmc = Aig_ManFrames( pMan, 1, 1, 0, 1, NULL ); +//Aig_ManShow( pFramesBmc, 0, NULL ); + assert( Aig_ManPoNum(pFramesBmc) == Aig_ManRegNum(pMan) ); + pCnfBmc = Cnf_DeriveSimple( pFramesBmc, Aig_ManRegNum(pMan) ); + p->pSatBmc = Cnf_DataWriteIntoSolver( pCnfBmc ); + + // create variable sets + p->vSatVarsMainCs = Fra_ClauSaveInputVars( pFramesMain, pCnfMain, 2 * (Aig_ManPiNum(pMan)-Aig_ManRegNum(pMan)) ); + p->vSatVarsTestCs = Fra_ClauSaveLatchVars( pFramesTest, pCnfTest, 1 ); + p->vSatVarsTestNs = Fra_ClauSaveLatchVars( pFramesTest, pCnfTest, 0 ); + p->vSatVarsBmcNs = Fra_ClauSaveOutputVars( pFramesBmc, pCnfBmc ); + assert( Vec_IntSize(p->vSatVarsTestCs) == Vec_IntSize(p->vSatVarsMainCs) ); + assert( Vec_IntSize(p->vSatVarsTestCs) == Vec_IntSize(p->vSatVarsBmcNs) ); + + // create mapping of CS into NS vars + p->pMapCsMainToCsTest = Fra_ClauCreateMapping( p->vSatVarsMainCs, p->vSatVarsTestCs, Aig_ManObjNumMax(pFramesMain) ); + p->pMapCsTestToCsMain = Fra_ClauCreateMapping( p->vSatVarsTestCs, p->vSatVarsMainCs, Aig_ManObjNumMax(pFramesTest) ); + p->pMapCsTestToNsTest = Fra_ClauCreateMapping( p->vSatVarsTestCs, p->vSatVarsTestNs, Aig_ManObjNumMax(pFramesTest) ); + p->pMapCsTestToNsBmc = Fra_ClauCreateMapping( p->vSatVarsTestCs, p->vSatVarsBmcNs, Aig_ManObjNumMax(pFramesTest) ); + + // cleanup + Cnf_DataFree( pCnfMain ); + Cnf_DataFree( pCnfTest ); + Cnf_DataFree( pCnfBmc ); + Aig_ManStop( pFramesMain ); + Aig_ManStop( pFramesTest ); + Aig_ManStop( pFramesBmc ); + if ( p->pSatMain == NULL || p->pSatTest == NULL || p->pSatBmc == NULL ) + { + Fra_ClauStop( p ); + return NULL; + } + return p; +} + +/**Function************************************************************* + + Synopsis [Splits off second half and returns it as a new vector.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +static Vec_Int_t * Vec_IntSplitHalf( Vec_Int_t * vVec ) +{ + Vec_Int_t * vPart; + int Entry, i; + assert( Vec_IntSize(vVec) > 1 ); + vPart = Vec_IntAlloc( Vec_IntSize(vVec) / 2 + 1 ); + Vec_IntForEachEntryStart( vVec, Entry, i, Vec_IntSize(vVec) / 2 ) + Vec_IntPush( vPart, Entry ); + Vec_IntShrink( vVec, Vec_IntSize(vVec) / 2 ); + return vPart; +} + +/**Function************************************************************* + + Synopsis [Appends the contents of the second vector.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +static void Vec_IntAppend( Vec_Int_t * vVec1, Vec_Int_t * vVec2 ) +{ + int Entry, i; + Vec_IntForEachEntry( vVec2, Entry, i ) + Vec_IntPush( vVec1, Entry ); +} + +/**Function************************************************************* + + Synopsis [Complements all literals in the clause.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +static void Vec_IntComplement( Vec_Int_t * vVec ) +{ + int i; + for ( i = 0; i < Vec_IntSize(vVec); i++ ) + vVec->pArray[i] = lit_neg( vVec->pArray[i] ); +} + +/**Function************************************************************* + + Synopsis [Checks if the property holds. Returns counter-example if not.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Fra_ClauCheckProperty( Cla_Man_t * p, Vec_Int_t * vCex ) +{ + int nBTLimit = 0; + int RetValue, iVar, i; + sat_solver_act_var_clear( p->pSatMain ); + RetValue = sat_solver_solve( p->pSatMain, NULL, NULL, (sint64)nBTLimit, (sint64)0, (sint64)0, (sint64)0 ); + Vec_IntClear( vCex ); + if ( RetValue == l_False ) + return 1; + assert( RetValue == l_True ); + Vec_IntForEachEntry( p->vSatVarsMainCs, iVar, i ) + Vec_IntPush( vCex, sat_solver_var_literal(p->pSatMain, iVar) ); +/* + { + int i; + for (i = 0; i < p->pSatMain->size; i++) + printf( "%d=%d ", i, p->pSatMain->model.ptr[i] == l_True ); + printf( "\n" ); + } +*/ + return 0; +} + +/**Function************************************************************* + + Synopsis [Checks if the clause holds using BMC.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Fra_ClauCheckBmc( Cla_Man_t * p, Vec_Int_t * vClause ) +{ + int nBTLimit = 0; + int RetValue; + RetValue = sat_solver_solve( p->pSatBmc, Vec_IntArray(vClause), Vec_IntArray(vClause) + Vec_IntSize(vClause), + (sint64)nBTLimit, (sint64)0, (sint64)0, (sint64)0 ); + if ( RetValue == l_False ) + return 1; + assert( RetValue == l_True ); + return 0; +} + +/**Function************************************************************* + + Synopsis [Lifts the clause to depend on NS variables.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Fra_ClauRemapClause( int * pMap, Vec_Int_t * vClause, Vec_Int_t * vRemapped, int fInv ) +{ + int iLit, i; + Vec_IntClear( vRemapped ); + Vec_IntForEachEntry( vClause, iLit, i ) + { + assert( pMap[lit_var(iLit)] >= 0 ); + iLit = toLitCond( pMap[lit_var(iLit)], lit_sign(iLit) ^ fInv ); + Vec_IntPush( vRemapped, iLit ); + } +} + +/**Function************************************************************* + + Synopsis [Checks if the clause holds. Returns counter example if not.] + + Description [Uses test SAT solver.] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Fra_ClauCheckClause( Cla_Man_t * p, Vec_Int_t * vClause, Vec_Int_t * vCex ) +{ + int nBTLimit = 0; + int RetValue, iVar, i; + int nClauseSize = Vec_IntSize( vClause ); + // complement literals + Vec_IntPush( vClause, toLit( p->nSatVarsTestCur++ ) ); // helper positive + Vec_IntComplement( vClause ); // helper negative (the clause is C v h') + // add the clause + RetValue = sat_solver_addclause( p->pSatTest, Vec_IntArray(vClause), Vec_IntArray(vClause) + Vec_IntSize(vClause) ); + assert( RetValue == 1 ); + // complement all literals + Vec_IntPop( vClause ); // helper removed + Vec_IntComplement( vClause ); + // create the assumption in terms of NS variables + Fra_ClauRemapClause( p->pMapCsTestToNsTest, vClause, p->vCexAssm, 0 ); + // add helper literals + for ( i = p->nSatVarsTestBeg; i < p->nSatVarsTestCur - 1; i++ ) + Vec_IntPush( p->vCexAssm, toLitCond(i,1) ); // other helpers negative + Vec_IntPush( p->vCexAssm, toLitCond(i,0) ); // positive helper + // try to solve + RetValue = sat_solver_solve( p->pSatTest, Vec_IntArray(p->vCexAssm), Vec_IntArray(p->vCexAssm) + Vec_IntSize(p->vCexAssm), + (sint64)nBTLimit, (sint64)0, (sint64)0, (sint64)0 ); + if ( vCex ) + Vec_IntClear( vCex ); + if ( RetValue == l_False ) + return 1; + assert( RetValue == l_True ); + if ( vCex ) + { + Vec_IntForEachEntry( p->vSatVarsTestCs, iVar, i ) + Vec_IntPush( vCex, sat_solver_var_literal(p->pSatTest, iVar) ); + } + return 0; +} + +/**Function************************************************************* + + Synopsis [Reduces the counter-example by removing complemented literals.] + + Description [Removes literals from vMain that differ from those in the + counter-example (vNew). Relies on the fact that the PI variables are + assigned in the increasing order.] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Fra_ClauReduceClause( Vec_Int_t * vMain, Vec_Int_t * vNew ) +{ + int LitM, LitN, VarM, VarN, i, j, k; + assert( Vec_IntSize(vMain) <= Vec_IntSize(vNew) ); + for ( i = j = k = 0; i < Vec_IntSize(vMain) && j < Vec_IntSize(vNew); ) + { + LitM = Vec_IntEntry( vMain, i ); + LitN = Vec_IntEntry( vNew, j ); + VarM = lit_var( LitM ); + VarN = lit_var( LitN ); + if ( VarM > VarN ) + { + assert( 0 ); + } + else if ( VarM < VarN ) + { + j++; + } + else // if ( VarM == VarN ) + { + i++; + j++; + if ( LitM == LitN ) + Vec_IntWriteEntry( vMain, k++, LitM ); + } + } + assert( i == Vec_IntSize(vMain) ); + Vec_IntShrink( vMain, k ); +} + +/**Function************************************************************* + + Synopsis [Computes the minimal invariant that holds.] + + Description [On entrace, vBasis does not hold, vBasis+vExtra holds but + is not minimal. On exit, vBasis is unchanged, vBasis+vExtra is minimal.] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Fra_ClauMinimizeClause_rec( Cla_Man_t * p, Vec_Int_t * vBasis, Vec_Int_t * vExtra ) +{ + Vec_Int_t * vExtra2; + int nSizeOld; + if ( Vec_IntSize(vExtra) == 1 ) + return; + nSizeOld = Vec_IntSize( vBasis ); + vExtra2 = Vec_IntSplitHalf( vExtra ); + + // try the first half + Vec_IntAppend( vBasis, vExtra ); + if ( Fra_ClauCheckClause( p, vBasis, NULL ) ) + { + Vec_IntShrink( vBasis, nSizeOld ); + Fra_ClauMinimizeClause_rec( p, vBasis, vExtra ); + return; + } + Vec_IntShrink( vBasis, nSizeOld ); + + // try the second half + Vec_IntAppend( vBasis, vExtra2 ); + if ( Fra_ClauCheckClause( p, vBasis, NULL ) ) + { + Vec_IntShrink( vBasis, nSizeOld ); + Fra_ClauMinimizeClause_rec( p, vBasis, vExtra2 ); + return; + } +// Vec_IntShrink( vBasis, nSizeOld ); + + // find the smallest with the second half added + Fra_ClauMinimizeClause_rec( p, vBasis, vExtra ); + Vec_IntShrink( vBasis, nSizeOld ); + Vec_IntAppend( vBasis, vExtra ); + // find the smallest with the second half added + Fra_ClauMinimizeClause_rec( p, vBasis, vExtra2 ); + Vec_IntShrink( vBasis, nSizeOld ); + Vec_IntAppend( vExtra, vExtra2 ); + Vec_IntFree( vExtra2 ); +} + +/**Function************************************************************* + + Synopsis [Minimizes the clauses using a simple method.] + + Description [The input and output clause are in vExtra.] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Fra_ClauMinimizeClause( Cla_Man_t * p, Vec_Int_t * vBasis, Vec_Int_t * vExtra ) +{ + int iLit, iLit2, i, k; + Vec_IntForEachEntryReverse( vExtra, iLit, i ) + { + // copy literals without the given one + Vec_IntClear( vBasis ); + Vec_IntForEachEntry( vExtra, iLit2, k ) + if ( iLit2 != iLit ) + Vec_IntPush( vBasis, iLit2 ); + // try whether it is inductive + if ( !Fra_ClauCheckClause( p, vBasis, NULL ) ) + continue; + // the clause is inductive + // remove the literal + for ( k = iLit; k < Vec_IntSize(vExtra)-1; k++ ) + Vec_IntWriteEntry( vExtra, k, Vec_IntEntry(vExtra,k+1) ); + Vec_IntShrink( vExtra, Vec_IntSize(vExtra)-1 ); + } +} + +/**Function************************************************************* + + Synopsis [Prints the clause.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Fra_ClauPrintClause( Vec_Int_t * vSatCsVars, Vec_Int_t * vCex ) +{ + int LitM, VarM, VarN, i, j, k; + assert( Vec_IntSize(vCex) <= Vec_IntSize(vSatCsVars) ); + for ( i = j = k = 0; i < Vec_IntSize(vCex) && j < Vec_IntSize(vSatCsVars); ) + { + LitM = Vec_IntEntry( vCex, i ); + VarM = lit_var( LitM ); + VarN = Vec_IntEntry( vSatCsVars, j ); + if ( VarM > VarN ) + { + assert( 0 ); + } + else if ( VarM < VarN ) + { + j++; + printf( "-" ); + } + else // if ( VarM == VarN ) + { + i++; + j++; + printf( "%d", !lit_sign(LitM) ); + } + } + assert( i == Vec_IntSize(vCex) ); +} + +/**Function************************************************************* + + Synopsis [Takes the AIG with the single output to be checked.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Fra_Clau( Aig_Man_t * pMan, int nIters, int fVerbose ) +{ + Cla_Man_t * p; + int Iter, RetValue, fFailed, i; + assert( Aig_ManPoNum(pMan) - Aig_ManRegNum(pMan) == 1 ); + // create the manager + p = Fra_ClauStart( pMan ); + if ( p == NULL ) + { + printf( "The property is trivially inductive.\n" ); + return 1; + } + // generate counter-examples and expand them + for ( Iter = 0; !Fra_ClauCheckProperty( p, p->vCexMain0 ) && Iter < nIters; Iter++ ) + { + if ( fVerbose ) + printf( "%4d : ", Iter ); + // remap clause into the test manager + Fra_ClauRemapClause( p->pMapCsMainToCsTest, p->vCexMain0, p->vCexMain, 0 ); + if ( fVerbose ) + Fra_ClauPrintClause( p->vSatVarsTestCs, p->vCexMain ); + // the main counter-example is in p->vCexMain + // intermediate counter-examples are in p->vCexTest + // generate the reduced counter-example to the inductive property + fFailed = 0; + for ( i = 0; !Fra_ClauCheckClause( p, p->vCexMain, p->vCexTest ); i++ ) + { + Fra_ClauReduceClause( p->vCexMain, p->vCexTest ); + Fra_ClauRemapClause( p->pMapCsTestToNsBmc, p->vCexMain, p->vCexBmc, 0 ); + if ( !Fra_ClauCheckBmc(p, p->vCexBmc) ) + { + fFailed = 1; + break; + } + } + if ( fFailed ) + { + if ( fVerbose ) + printf( " Reducing failed after %d iterations (BMC failed).\n", i ); + continue; + } + if ( Vec_IntSize(p->vCexMain) == 0 ) + { + if ( fVerbose ) + printf( " Reducing failed after %d iterations (nothing left).\n", i ); + continue; + } + if ( fVerbose ) + printf( " LitsAfterRed = %3d. ", Vec_IntSize(p->vCexMain) ); + // minimize the inductive property + Vec_IntClear( p->vCexBase ); +// Fra_ClauMinimizeClause_rec( p, p->vCexBase, p->vCexMain ); +// Fra_ClauMinimizeClause( p, p->vCexBase, p->vCexMain ); + assert( Vec_IntSize(p->vCexMain) > 0 ); + if ( fVerbose ) + printf( " LitsAfterMin = %3d. ", Vec_IntSize(p->vCexMain) ); + if ( fVerbose ) + printf( "\n" ); + // add the clause to the solver + Fra_ClauRemapClause( p->pMapCsTestToCsMain, p->vCexMain, p->vCexAssm, 1 ); + RetValue = sat_solver_addclause( p->pSatMain, Vec_IntArray(p->vCexAssm), Vec_IntArray(p->vCexAssm) + Vec_IntSize(p->vCexAssm) ); + if ( RetValue == 0 ) + { + Iter++; + break; + } + } + + // report the results + if ( Iter == nIters ) + { + printf( "Property is not proved after %d iterations.\n", nIters ); + return 0; + } + printf( "Property is proved after %d iterations.\n", Iter ); + Fra_ClauStop( p ); + return 1; +} + + +//////////////////////////////////////////////////////////////////////// +/// END OF FILE /// +//////////////////////////////////////////////////////////////////////// + + diff --git a/src/aig/fra/fraCore.c b/src/aig/fra/fraCore.c index 7400b3f9..95d65e25 100644 --- a/src/aig/fra/fraCore.c +++ b/src/aig/fra/fraCore.c @@ -280,6 +280,8 @@ static inline void Fra_FraigNode( Fra_Man_t * p, Aig_Obj_t * pObj ) // Fra_FraigVerifyCounterEx( p, p->vCex ); // simulate the counter-example and return the Fraig node Fra_SmlResimulate( p ); + if ( p->pManFraig->pData ) + return; if ( !p->pPars->nFramesK && Fra_ClassObjRepr(pObj) == pObjRepr ) printf( "Fra_FraigNode(): Error in class refinement!\n" ); assert( p->pPars->nFramesK || Fra_ClassObjRepr(pObj) != pObjRepr ); diff --git a/src/aig/fra/fraInd.c b/src/aig/fra/fraInd.c index b41b7a29..6cfdc3ff 100644 --- a/src/aig/fra/fraInd.c +++ b/src/aig/fra/fraInd.c @@ -402,16 +402,21 @@ p->timeTrav += clock() - clk2; Fra_ClassesCountLits(p->pCla), p->pManFraig->nAsserts ); if ( p->pCla->vImps ) printf( "I = %6d. ", Vec_IntSize(p->pCla->vImps) ); - printf( "NR = %6d.\n", Aig_ManNodeNum(p->pManFraig) ); + printf( "NR = %6d. ", Aig_ManNodeNum(p->pManFraig) ); + printf( "\n" ); } // perform sweeping p->nSatCallsRecent = 0; p->nSatCallsSkipped = 0; +clk2 = clock(); Fra_FraigSweep( p ); + if ( fVerbose ) + { +// PRT( "t", clock() - clk2 ); + } // Sat_SolverPrintStats( stdout, p->pSat ); - // remove FRAIG and SAT solver Aig_ManStop( p->pManFraig ); p->pManFraig = NULL; sat_solver_delete( p->pSat ); p->pSat = NULL; diff --git a/src/aig/fra/fraSec.c b/src/aig/fra/fraSec.c index 573d3570..17a7335c 100644 --- a/src/aig/fra/fraSec.c +++ b/src/aig/fra/fraSec.c @@ -228,9 +228,11 @@ PRT( "Time", clock() - clk ); } if ( pNew->nRegs ) - pNew = Aig_ManConstReduce( pNew, 0 ); + pNew = Aig_ManConstReduce( pNew, 0 ); // perform sequential simulation + if ( pNew->nRegs ) + { clk = clock(); pSml = Fra_SmlSimulateSeq( pNew, 0, 128 * nFrames, 1 + 16/(1+Aig_ManNodeNum(pNew)/1000) ); if ( fVerbose ) @@ -250,6 +252,7 @@ PRT( "Time", clock() - clkTotal ); return RetValue; } Fra_SmlStop( pSml ); + } } // get the miter status |