From 369f008e69a4f201cbc7c890a08221086bee4698 Mon Sep 17 00:00:00 2001 From: Alan Mishchenko Date: Fri, 30 Nov 2007 08:01:00 -0800 Subject: Version abc71130 --- abc.dsp | 16 + abc.rc | 4 + src/aig/aig/aig.h | 14 +- src/aig/aig/aigFrames.c | 133 ++++++++ src/aig/aig/aigHaig.c | 270 +++++++++++++++ src/aig/aig/aigMan.c | 53 ++- src/aig/aig/aigObj.c | 17 +- src/aig/aig/aigOper.c | 9 + src/aig/aig/aigRetF.c | 219 ++++++++++++ src/aig/aig/aigScl.c | 6 +- src/aig/aig/aigTable.c | 21 ++ src/aig/aig/aigUtil.c | 8 +- src/aig/fra/fraClau.c | 737 +++++++++++++++++++++++++++++++++++++++++ src/aig/fra/fraCore.c | 2 + src/aig/fra/fraInd.c | 9 +- src/aig/fra/fraSec.c | 5 +- src/base/abc/abcCheck.c | 8 +- src/base/abci/abc.c | 118 ++++++- src/base/abci/abcDar.c | 107 +++++- src/base/io/io.c | 2 + src/base/ver/verCore.c | 109 ++++++ src/map/fpga/fpgaLib.c | 3 +- src/misc/extra/extraUtilUtil.c | 28 +- src/sat/bsat/satSolver.h | 18 + 24 files changed, 1885 insertions(+), 31 deletions(-) create mode 100644 src/aig/aig/aigFrames.c create mode 100644 src/aig/aig/aigHaig.c create mode 100644 src/aig/aig/aigRetF.c create mode 100644 src/aig/fra/fraClau.c diff --git a/abc.dsp b/abc.dsp index 4a26368b..78e7f3bb 100644 --- a/abc.dsp +++ b/abc.dsp @@ -2622,6 +2622,10 @@ SOURCE=.\src\aig\fra\fraClass.c # End Source File # Begin Source File +SOURCE=.\src\aig\fra\fraClau.c +# End Source File +# Begin Source File + SOURCE=.\src\aig\fra\fraCnf.c # End Source File # Begin Source File @@ -2830,6 +2834,14 @@ SOURCE=.\src\aig\aig\aigFanout.c # End Source File # Begin Source File +SOURCE=.\src\aig\aig\aigFrames.c +# End Source File +# Begin Source File + +SOURCE=.\src\aig\aig\aigHaig.c +# End Source File +# Begin Source File + SOURCE=.\src\aig\aig\aigMan.c # End Source File # Begin Source File @@ -2866,6 +2878,10 @@ SOURCE=.\src\aig\aig\aigRet.c # End Source File # Begin Source File +SOURCE=.\src\aig\aig\aigRetF.c +# End Source File +# Begin Source File + SOURCE=.\src\aig\aig\aigScl.c # End Source File # Begin Source File diff --git a/abc.rc b/abc.rc index 5de41064..c4d3d375 100644 --- a/abc.rc +++ b/abc.rc @@ -52,6 +52,7 @@ alias rh read_hie alias rl read_blif alias rb read_bench alias ret retime +alias dret dretime alias rp read_pla alias rt read_truth alias rv read_verilog @@ -121,4 +122,7 @@ alias trec "rec_start; r c.blif; st; rec_add; rec_use" alias trec4 "rec_start -K 4; r i10.blif; st; rec_add; rec_use" alias bmc2 "frames -i -F 10; orpos; iprove" +alias t0 "r test/mc1.blif; st; test" +alias t1 "r s27mc2.blif; st; test" +alias t2 "r i/intel_001.aig; ps; test" 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 diff --git a/src/base/abc/abcCheck.c b/src/base/abc/abcCheck.c index 3072e40f..79b76348 100644 --- a/src/base/abc/abcCheck.c +++ b/src/base/abc/abcCheck.c @@ -913,7 +913,7 @@ int Abc_NtkCheckUniqueCoNames( Abc_Ntk_t * pNtk ) ***********************************************************************/ int Abc_NtkCheckUniqueCioNames( Abc_Ntk_t * pNtk ) { - Abc_Obj_t * pObj, * pObjCi; + Abc_Obj_t * pObj, * pObjCi, * pFanin; int i, nCiId, fRetValue = 1; assert( !Abc_NtkIsNetlist(pNtk) ); Abc_NtkForEachCo( pNtk, pObj, i ) @@ -923,9 +923,11 @@ int Abc_NtkCheckUniqueCioNames( Abc_Ntk_t * pNtk ) continue; pObjCi = Abc_NtkObj( pNtk, nCiId ); assert( !strcmp( Abc_ObjName(pObj), Abc_ObjName(pObjCi) ) ); - if ( Abc_ObjFanin0(pObj) != pObjCi ) + pFanin = Abc_ObjFanin0(pObj); + if ( pFanin != pObjCi ) { - printf( "Abc_NtkCheck: A CI/CO pair share the name (%s) but do not link directly.\n", Abc_ObjName(pObj) ); + printf( "Abc_NtkCheck: A CI/CO pair share the name (%s) but do not link directly. The name of the CO fanin is %s.\n", + Abc_ObjName(pObj), Abc_ObjName(Abc_ObjFanin0(pObj)) ); fRetValue = 0; } } diff --git a/src/base/abci/abc.c b/src/base/abci/abc.c index 3f9ffb40..20aa7247 100644 --- a/src/base/abci/abc.c +++ b/src/base/abci/abc.c @@ -164,6 +164,7 @@ static int Abc_CommandPipe ( Abc_Frame_t * pAbc, int argc, char ** arg static int Abc_CommandSeq ( Abc_Frame_t * pAbc, int argc, char ** argv ); static int Abc_CommandUnseq ( Abc_Frame_t * pAbc, int argc, char ** argv ); static int Abc_CommandRetime ( Abc_Frame_t * pAbc, int argc, char ** argv ); +static int Abc_CommandDRetime ( Abc_Frame_t * pAbc, int argc, char ** argv ); static int Abc_CommandSeqFpga ( Abc_Frame_t * pAbc, int argc, char ** argv ); static int Abc_CommandSeqMap ( Abc_Frame_t * pAbc, int argc, char ** argv ); static int Abc_CommandSeqSweep ( Abc_Frame_t * pAbc, int argc, char ** argv ); @@ -333,6 +334,7 @@ void Abc_Init( Abc_Frame_t * pAbc ) Cmd_CommandAdd( pAbc, "Sequential", "undc", Abc_CommandUndc, 1 ); // Cmd_CommandAdd( pAbc, "Sequential", "pipe", Abc_CommandPipe, 1 ); Cmd_CommandAdd( pAbc, "Sequential", "retime", Abc_CommandRetime, 1 ); + Cmd_CommandAdd( pAbc, "Sequential", "dretime", Abc_CommandDRetime, 1 ); // Cmd_CommandAdd( pAbc, "Sequential", "sfpga", Abc_CommandSeqFpga, 1 ); // Cmd_CommandAdd( pAbc, "Sequential", "smap", Abc_CommandSeqMap, 1 ); Cmd_CommandAdd( pAbc, "Sequential", "ssweep", Abc_CommandSeqSweep, 1 ); @@ -6189,7 +6191,7 @@ usage: int Abc_CommandTest( Abc_Frame_t * pAbc, int argc, char ** argv ) { FILE * pOut, * pErr; - Abc_Ntk_t * pNtk, * pNtkRes; + Abc_Ntk_t * pNtk;//, * pNtkRes; int c; int nLevels; int fVerbose; @@ -6204,14 +6206,16 @@ int Abc_CommandTest( Abc_Frame_t * pAbc, int argc, char ** argv ) extern Abc_Ntk_t * Abc_NtkFilter( Abc_Ntk_t * pNtk ); extern Abc_Ntk_t * Abc_NtkDarRetime( Abc_Ntk_t * pNtk, int nStepsMax, int fVerbose ); extern Abc_Ntk_t * Abc_NtkPcmTest( Abc_Ntk_t * pNtk, int fVerbose ); + extern Abc_NtkDarHaigRecord( Abc_Ntk_t * pNtk ); + extern int Abc_NtkDarClau( Abc_Ntk_t * pNtk, int nStepsMax, int fVerbose ); pNtk = Abc_FrameReadNtk(pAbc); pOut = Abc_FrameReadOut(pAbc); pErr = Abc_FrameReadErr(pAbc); // set defaults - fVerbose = 0; - nLevels = 1000; + fVerbose = 1; + nLevels = 1000; Extra_UtilGetoptReset(); while ( ( c = Extra_UtilGetopt( argc, argv, "Nvh" ) ) != EOF ) { @@ -6324,13 +6328,14 @@ int Abc_CommandTest( Abc_Frame_t * pAbc, int argc, char ** argv ) return 1; } */ -/* + if ( !Abc_NtkIsStrash(pNtk) ) { fprintf( stdout, "Currently only works for structurally hashed circuits.\n" ); return 0; } -*/ + +/* if ( Abc_NtkIsStrash(pNtk) ) { fprintf( stdout, "Currently only works for logic circuits.\n" ); @@ -6348,6 +6353,9 @@ int Abc_CommandTest( Abc_Frame_t * pAbc, int argc, char ** argv ) } // replace the current network Abc_FrameReplaceCurrentNetwork( pAbc, pNtkRes ); +*/ +// Abc_NtkDarHaigRecord( pNtk ); + Abc_NtkDarClau( pNtk, 1000, fVerbose ); return 0; usage: fprintf( pErr, "usage: test [-h]\n" ); @@ -10807,6 +10815,106 @@ usage: // fprintf( pErr, "\t-i : toggle computation of initial state [default = %s]\n", fInitial? "yes": "no" ); } +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Abc_CommandDRetime( Abc_Frame_t * pAbc, int argc, char ** argv ) +{ + FILE * pOut, * pErr; + Abc_Ntk_t * pNtk, * pNtkRes; + int nStepsMax; + int fFastAlgo; + int fVerbose; + int c; + extern Abc_Ntk_t * Abc_NtkDarRetimeF( Abc_Ntk_t * pNtk, int nStepsMax, int fVerbose ); + + pNtk = Abc_FrameReadNtk(pAbc); + pOut = Abc_FrameReadOut(pAbc); + pErr = Abc_FrameReadErr(pAbc); + + // set defaults + nStepsMax = 100000; + fFastAlgo = 0; + fVerbose = 0; + Extra_UtilGetoptReset(); + while ( ( c = Extra_UtilGetopt( argc, argv, "Savh" ) ) != EOF ) + { + switch ( c ) + { + case 'S': + if ( globalUtilOptind >= argc ) + { + fprintf( pErr, "Command line switch \"-S\" should be followed by a positive integer.\n" ); + goto usage; + } + nStepsMax = atoi(argv[globalUtilOptind]); + globalUtilOptind++; + if ( nStepsMax < 0 ) + goto usage; + break; + case 'a': + fFastAlgo ^= 1; + break; + case 'v': + fVerbose ^= 1; + break; + case 'h': + goto usage; + default: + goto usage; + } + } + + if ( pNtk == NULL ) + { + fprintf( pErr, "Empty network.\n" ); + return 1; + } + + if ( !Abc_NtkLatchNum(pNtk) ) + { + fprintf( pErr, "The network has no latches. Retiming is not performed.\n" ); + return 0; + } + + if ( !Abc_NtkIsStrash(pNtk) ) + { + printf( "This command works only for structrally hashed networks. Run \"st\".\n" ); + return 0; + } + + // perform the retiming + if ( fFastAlgo ) + pNtkRes = Abc_NtkDarRetime( pNtk, nStepsMax, fVerbose ); + else + pNtkRes = Abc_NtkDarRetimeF( pNtk, nStepsMax, fVerbose ); + if ( pNtkRes == NULL ) + { + fprintf( pErr, "Retiming has failed.\n" ); + return 1; + } + // replace the current network + Abc_FrameReplaceCurrentNetwork( pAbc, pNtkRes ); + return 0; + +usage: + fprintf( pErr, "usage: dretime [-S num] [-avh]\n" ); + fprintf( pErr, "\t retimes the current network forward\n" ); + fprintf( pErr, "\t-S num : the max number of retiming steps to perform [default = %d]\n", nStepsMax ); + fprintf( pErr, "\t-a : enables a fast algorithm [default = %s]\n", fFastAlgo? "yes": "no" ); + fprintf( pErr, "\t-v : enables verbose output [default = %s]\n", fVerbose? "yes": "no" ); + fprintf( pErr, "\t-h : print the command usage\n"); + return 1; +} + /**Function************************************************************* Synopsis [] diff --git a/src/base/abci/abcDar.c b/src/base/abci/abcDar.c index ab8614fb..67f22eb7 100644 --- a/src/base/abci/abcDar.c +++ b/src/base/abci/abcDar.c @@ -87,7 +87,8 @@ Aig_Man_t * Abc_NtkToDar( Abc_Ntk_t * pNtk, int fRegisters ) if ( fRegisters ) { pMan->nRegs = Abc_NtkLatchNum(pNtk); - pMan->vFlopNums = Vec_IntStartNatural( pMan->nRegs ); +// pMan->vFlopNums = Vec_IntStartNatural( pMan->nRegs ); + pMan->vFlopNums = NULL; } // transfer the pointers to the basic nodes Abc_AigConst1(pNtk)->pCopy = (Abc_Obj_t *)Aig_ManConst1(pMan); @@ -198,7 +199,7 @@ Abc_Ntk_t * Abc_NtkFromDarSeqSweep( Abc_Ntk_t * pNtkOld, Aig_Man_t * pMan ) Abc_Ntk_t * pNtkNew; Abc_Obj_t * pObjNew, * pLatch; Aig_Obj_t * pObj, * pObjLo, * pObjLi; - int i; + int i, iNodeId; // assert( Aig_ManRegNum(pMan) != Abc_NtkLatchNum(pNtkOld) ); // perform strashing pNtkNew = Abc_NtkStartFromNoLatches( pNtkOld, ABC_NTK_STRASH, ABC_FUNC_AIG ); @@ -242,7 +243,12 @@ Abc_Ntk_t * Abc_NtkFromDarSeqSweep( Abc_Ntk_t * pNtkOld, Aig_Man_t * pMan ) { if ( pMan->nAsserts && i == Aig_ManPoNum(pMan) - pMan->nAsserts ) break; - Abc_ObjAddFanin( Abc_NtkCo(pNtkNew, i), (Abc_Obj_t *)Aig_ObjChild0Copy(pObj) ); + iNodeId = Nm_ManFindIdByNameTwoTypes( pNtkNew->pManName, Abc_ObjName(Abc_NtkCo(pNtkNew, i)), ABC_OBJ_PI, ABC_OBJ_BO ); + if ( iNodeId >= 0 ) + pObjNew = Abc_NtkObj( pNtkNew, iNodeId ); + else + pObjNew = (Abc_Obj_t *)Aig_ObjChild0Copy(pObj); + Abc_ObjAddFanin( Abc_NtkCo(pNtkNew, i), pObjNew ); } // if there are assertions, add them if ( pMan->nAsserts > 0 ) @@ -1270,6 +1276,9 @@ Abc_Ntk_t * Abc_NtkDarRetime( Abc_Ntk_t * pNtk, int nStepsMax, int fVerbose ) if ( pMan == NULL ) return NULL; // Aig_ManReduceLachesCount( pMan ); + if ( pMan->vFlopNums ) + Vec_IntFree( pMan->vFlopNums ); + pMan->vFlopNums = NULL; pMan = Rtm_ManRetime( pTemp = pMan, 1, nStepsMax, 0 ); Aig_ManStop( pTemp ); @@ -1282,6 +1291,65 @@ Abc_Ntk_t * Abc_NtkDarRetime( Abc_Ntk_t * pNtk, int nStepsMax, int fVerbose ) return pNtkAig; } +/**Function************************************************************* + + Synopsis [Gives the current ABC network to AIG manager for processing.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Abc_Ntk_t * Abc_NtkDarRetimeF( Abc_Ntk_t * pNtk, int nStepsMax, int fVerbose ) +{ + Abc_Ntk_t * pNtkAig; + Aig_Man_t * pMan, * pTemp; + pMan = Abc_NtkToDar( pNtk, 1 ); + if ( pMan == NULL ) + return NULL; +// Aig_ManReduceLachesCount( pMan ); + if ( pMan->vFlopNums ) + Vec_IntFree( pMan->vFlopNums ); + pMan->vFlopNums = NULL; + + pMan = Aig_ManRetimeFrontier( pTemp = pMan, nStepsMax ); + Aig_ManStop( pTemp ); + +// pMan = Aig_ManReduceLaches( pMan, 1 ); +// pMan = Aig_ManConstReduce( pMan, 1 ); + + pNtkAig = Abc_NtkFromDarSeqSweep( pNtk, pMan ); + Aig_ManStop( pMan ); + return pNtkAig; +} + +/**Function************************************************************* + + Synopsis [Gives the current ABC network to AIG manager for processing.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Abc_NtkDarHaigRecord( Abc_Ntk_t * pNtk ) +{ + Aig_Man_t * pMan; + pMan = Abc_NtkToDar( pNtk, 1 ); + if ( pMan == NULL ) + return; +// Aig_ManReduceLachesCount( pMan ); + if ( pMan->vFlopNums ) + Vec_IntFree( pMan->vFlopNums ); + pMan->vFlopNums = NULL; + Aig_ManHaigRecord( pMan ); + Aig_ManStop( pMan ); +} + /**Function************************************************************* Synopsis [Performs random simulation.] @@ -1322,6 +1390,39 @@ int Abc_NtkDarSeqSim( Abc_Ntk_t * pNtk, int nFrames, int nWords, int fVerbose ) return RetValue; } +/**Function************************************************************* + + Synopsis [Gives the current ABC network to AIG manager for processing.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Abc_NtkDarClau( Abc_Ntk_t * pNtk, int nStepsMax, int fVerbose ) +{ + extern int Fra_Clau( Aig_Man_t * pMan, int nIters, int fVerbose ); + Aig_Man_t * pMan; + if ( Abc_NtkPoNum(pNtk) != 1 ) + { + printf( "The number of outputs should be 1.\n" ); + return 1; + } + pMan = Abc_NtkToDar( pNtk, 1 ); + if ( pMan == NULL ) + return 1; +// Aig_ManReduceLachesCount( pMan ); + if ( pMan->vFlopNums ) + Vec_IntFree( pMan->vFlopNums ); + pMan->vFlopNums = NULL; + + Fra_Clau( pMan, nStepsMax, fVerbose ); + Aig_ManStop( pMan ); + return 1; +} + //////////////////////////////////////////////////////////////////////// /// END OF FILE /// //////////////////////////////////////////////////////////////////////// diff --git a/src/base/io/io.c b/src/base/io/io.c index 941ef7a7..ed314fcd 100644 --- a/src/base/io/io.c +++ b/src/base/io/io.c @@ -348,6 +348,8 @@ int IoCommandReadBlif( Abc_Frame_t * pAbc, int argc, char ** argv ) { Abc_Ntk_t * pTemp; pNtk = Io_ReadBlif( pFileName, fCheck ); + if ( pNtk == NULL ) + return 1; pNtk = Abc_NtkToLogic( pTemp = pNtk ); Abc_NtkDelete( pTemp ); } diff --git a/src/base/ver/verCore.c b/src/base/ver/verCore.c index 7a217fd7..322ce720 100644 --- a/src/base/ver/verCore.c +++ b/src/base/ver/verCore.c @@ -58,6 +58,7 @@ static int Ver_ParseAlways( Ver_Man_t * p, Abc_Ntk_t * pNtk ); static int Ver_ParseInitial( Ver_Man_t * p, Abc_Ntk_t * pNtk ); static int Ver_ParseAssign( Ver_Man_t * p, Abc_Ntk_t * pNtk ); static int Ver_ParseGateStandard( Ver_Man_t * pMan, Abc_Ntk_t * pNtk, Ver_GateType_t GateType ); +static int Ver_ParseFlopStandard( Ver_Man_t * pMan, Abc_Ntk_t * pNtk ); static int Ver_ParseGate( Ver_Man_t * p, Abc_Ntk_t * pNtk, Mio_Gate_t * pGate ); static int Ver_ParseBox( Ver_Man_t * pMan, Abc_Ntk_t * pNtk, Abc_Ntk_t * pNtkBox ); static int Ver_ParseConnectBox( Ver_Man_t * pMan, Abc_Obj_t * pBox ); @@ -472,6 +473,9 @@ int Ver_ParseModule( Ver_Man_t * pMan ) else if ( !strcmp( pWord, "not" ) ) RetValue = Ver_ParseGateStandard( pMan, pNtk, VER_GATE_NOT ); + else if ( !strcmp( pWord, "dff" ) ) + RetValue = Ver_ParseFlopStandard( pMan, pNtk ); + else if ( !strcmp( pWord, "assign" ) ) RetValue = Ver_ParseAssign( pMan, pNtk ); else if ( !strcmp( pWord, "always" ) ) @@ -1364,6 +1368,105 @@ int Ver_ParseGateStandard( Ver_Man_t * pMan, Abc_Ntk_t * pNtk, Ver_GateType_t Ga return 1; } +/**Function************************************************************* + + Synopsis [Parses one directive.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Ver_ParseFlopStandard( Ver_Man_t * pMan, Abc_Ntk_t * pNtk ) +{ + Ver_Stream_t * p = pMan->pReader; + Abc_Obj_t * pNetLi, * pNetLo, * pLatch; + char * pWord, Symbol; + + // convert from the blackbox into the network with local functions representated by AIGs + if ( !Ver_ParseConvertNetwork( pMan, pNtk, pMan->fMapped ) ) + return 0; + + // this is gate name - throw it away + if ( Ver_StreamPopChar(p) != '(' ) + { + sprintf( pMan->sError, "Cannot parse a standard gate (expected opening paranthesis)." ); + Ver_ParsePrintErrorMessage( pMan ); + return 0; + } + Ver_ParseSkipComments( pMan ); + + // parse the output name + pWord = Ver_ParseGetName( pMan ); + if ( pWord == NULL ) + return 0; + // get the net corresponding to this output + pNetLo = Ver_ParseFindNet( pNtk, pWord ); + if ( pNetLo == NULL ) + { + sprintf( pMan->sError, "Net is missing in gate %s.", pWord ); + Ver_ParsePrintErrorMessage( pMan ); + return 0; + } + + // check if it is the end of gate + Ver_ParseSkipComments( pMan ); + Symbol = Ver_StreamPopChar(p); + if ( Symbol == ')' ) + { + sprintf( pMan->sError, "Cannot parse the flop." ); + Ver_ParsePrintErrorMessage( pMan ); + return 0; + } + // skip comma + if ( Symbol != ',' ) + { + sprintf( pMan->sError, "Cannot parse the flop." ); + Ver_ParsePrintErrorMessage( pMan ); + return 0; + } + Ver_ParseSkipComments( pMan ); + + // parse the output name + pWord = Ver_ParseGetName( pMan ); + if ( pWord == NULL ) + return 0; + // get the net corresponding to this output + pNetLi = Ver_ParseFindNet( pNtk, pWord ); + if ( pNetLi == NULL ) + { + sprintf( pMan->sError, "Net is missing in gate %s.", pWord ); + Ver_ParsePrintErrorMessage( pMan ); + return 0; + } + + // check if it is the end of gate + Ver_ParseSkipComments( pMan ); + Symbol = Ver_StreamPopChar(p); + if ( Symbol != ')' ) + { + sprintf( pMan->sError, "Cannot parse the flop." ); + Ver_ParsePrintErrorMessage( pMan ); + return 0; + } + + // check if it is the end of gate + Ver_ParseSkipComments( pMan ); + if ( Ver_StreamPopChar(p) != ';' ) + { + sprintf( pMan->sError, "Cannot parse the flop." ); + Ver_ParsePrintErrorMessage( pMan ); + return 0; + } + + // create the latch + pLatch = Ver_ParseCreateLatch( pNtk, pNetLi, pNetLo ); + Abc_LatchSetInit0( pLatch ); + return 1; +} + /**Function************************************************************* Synopsis [Returns the index of the given pin the gate.] @@ -1606,6 +1709,12 @@ int Ver_ParseBox( Ver_Man_t * pMan, Abc_Ntk_t * pNtk, Abc_Ntk_t * pNtkBox ) pNode->pCopy = (Abc_Obj_t *)vBundles; while ( 1 ) { +/* + if ( Ver_StreamGetLineNumber(pMan->pReader) == 5967 ) + { + int x = 0; + } +*/ // allocate the bundle (formal name + array of actual nets) pBundle = ALLOC( Ver_Bundle_t, 1 ); pBundle->pNameFormal = NULL; diff --git a/src/map/fpga/fpgaLib.c b/src/map/fpga/fpgaLib.c index e74def32..b1bb4cdc 100644 --- a/src/map/fpga/fpgaLib.c +++ b/src/map/fpga/fpgaLib.c @@ -113,10 +113,11 @@ Fpga_LutLib_t * Fpga_LutLibCreate( char * FileName, int fVerbose ) i++; } p->LutMax = i-1; + if ( p->LutMax > FPGA_MAX_LEAVES ) { p->LutMax = FPGA_MAX_LEAVES; - printf( "Warning: LUTs with more than %d input will not be used.\n", FPGA_MAX_LEAVES ); + printf( "Warning: LUTs with more than %d inputs will not be used.\n", FPGA_MAX_LEAVES ); } // check the library diff --git a/src/misc/extra/extraUtilUtil.c b/src/misc/extra/extraUtilUtil.c index ee0c400a..c685f7bc 100644 --- a/src/misc/extra/extraUtilUtil.c +++ b/src/misc/extra/extraUtilUtil.c @@ -193,7 +193,7 @@ char * Extra_UtilStrsav( char *s ) Synopsis [util_tilde_expand()] - Description [] + Description [The code contributed by Niklas Sorensson.] SideEffects [] @@ -203,6 +203,32 @@ char * Extra_UtilStrsav( char *s ) char * Extra_UtilTildeExpand( char *fname ) { return Extra_UtilStrsav( fname ); +/* + int n_tildes = 0; + const char* home; + char* expanded; + int length; + int i, j, k; + + for (i = 0; i < (int)strlen(fname); i++) + if (fname[i] == '~') n_tildes++; + + home = getenv("HOME"); + length = n_tildes * strlen(home) + strlen(fname); + expanded = ALLOC(char, length + 1); + + j = 0; + for (i = 0; i < (int)strlen(fname); i++){ + if (fname[i] == '~'){ + for (k = 0; k < (int)strlen(home); k++) + expanded[j++] = home[k]; + }else + expanded[j++] = fname[i]; + } + + expanded[j] = '\0'; + return expanded; +*/ } /**Function************************************************************* diff --git a/src/sat/bsat/satSolver.h b/src/sat/bsat/satSolver.h index 542b9895..ca2954d2 100644 --- a/src/sat/bsat/satSolver.h +++ b/src/sat/bsat/satSolver.h @@ -188,4 +188,22 @@ struct sat_solver_t int nRoots; }; +static int sat_solver_var_value( sat_solver* s, int v ) +{ + assert( s->model.ptr != NULL && v < s->size ); + return (int)(s->model.ptr[v] == l_True); +} +static int sat_solver_var_literal( sat_solver* s, int v ) +{ + assert( s->model.ptr != NULL && v < s->size ); + return toLitCond( v, s->model.ptr[v] != l_True ); +} +static void sat_solver_act_var_clear(sat_solver* s) +{ + int i; + for (i = 0; i < s->size; i++) + s->activity[i] = 0.0; + s->var_inc = 1.0; +} + #endif -- cgit v1.2.3