summaryrefslogtreecommitdiffstats
diff options
context:
space:
mode:
Diffstat
-rw-r--r--abc.dsp16
-rw-r--r--abc.rc4
-rw-r--r--src/aig/aig/aig.h14
-rw-r--r--src/aig/aig/aigFrames.c133
-rw-r--r--src/aig/aig/aigHaig.c270
-rw-r--r--src/aig/aig/aigMan.c53
-rw-r--r--src/aig/aig/aigObj.c17
-rw-r--r--src/aig/aig/aigOper.c9
-rw-r--r--src/aig/aig/aigRetF.c219
-rw-r--r--src/aig/aig/aigScl.c6
-rw-r--r--src/aig/aig/aigTable.c21
-rw-r--r--src/aig/aig/aigUtil.c8
-rw-r--r--src/aig/fra/fraClau.c737
-rw-r--r--src/aig/fra/fraCore.c2
-rw-r--r--src/aig/fra/fraInd.c9
-rw-r--r--src/aig/fra/fraSec.c5
-rw-r--r--src/base/abc/abcCheck.c8
-rw-r--r--src/base/abci/abc.c118
-rw-r--r--src/base/abci/abcDar.c107
-rw-r--r--src/base/io/io.c2
-rw-r--r--src/base/ver/verCore.c109
-rw-r--r--src/map/fpga/fpgaLib.c3
-rw-r--r--src/misc/extra/extraUtilUtil.c28
-rw-r--r--src/sat/bsat/satSolver.h18
24 files changed, 1885 insertions, 31 deletions
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" );
@@ -10818,6 +10826,106 @@ usage:
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 []
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
int Abc_CommandSeqFpga( Abc_Frame_t * pAbc, int argc, char ** argv )
{
FILE * pOut, * pErr;
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 );
@@ -1284,6 +1293,65 @@ Abc_Ntk_t * Abc_NtkDarRetime( Abc_Ntk_t * pNtk, int nStepsMax, int fVerbose )
/**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.]
Description []
@@ -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" ) )
@@ -1366,6 +1370,105 @@ int Ver_ParseGateStandard( Ver_Man_t * pMan, Abc_Ntk_t * pNtk, Ver_GateType_t Ga
/**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.]
Description []
@@ -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
generated by cgit v1.2.3 (git 2.25.1) at 2024-07-01 01:31:50 +0000