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