summaryrefslogtreecommitdiffstats
diff options
context:
space:
mode:
authorAlan Mishchenko <alanmi@berkeley.edu>2007-08-28 08:01:00 -0700
committerAlan Mishchenko <alanmi@berkeley.edu>2007-08-28 08:01:00 -0700
commitddc6d1c1682a18e293399b7d6c9f4a9018c30c70 (patch)
tree165c2a7ebb0561d9272673ce8caaa012f82d4717
parent28467823812f63a40f9a322b1fefc7decce4b766 (diff)
downloadabc-ddc6d1c1682a18e293399b7d6c9f4a9018c30c70.tar.gz
abc-ddc6d1c1682a18e293399b7d6c9f4a9018c30c70.tar.bz2
abc-ddc6d1c1682a18e293399b7d6c9f4a9018c30c70.zip
Version abc70828
-rw-r--r--abc.dsp8
-rw-r--r--src/aig/aig/aig.h15
-rw-r--r--src/aig/aig/aigMan.c331
-rw-r--r--src/aig/aig/aigPart.c2
-rw-r--r--src/aig/aig/aigRepr.c2
-rw-r--r--src/aig/aig/aigScl.c370
-rw-r--r--src/aig/aig/aigTsim.c4
-rw-r--r--src/aig/aig/aigUtil.c14
-rw-r--r--src/aig/aig/module.make2
-rw-r--r--src/aig/fra/fra.h22
-rw-r--r--src/aig/fra/fraBmc.c128
-rw-r--r--src/aig/fra/fraClass.c9
-rw-r--r--src/aig/fra/fraCore.c33
-rw-r--r--src/aig/fra/fraImp.c202
-rw-r--r--src/aig/fra/fraInd.c131
-rw-r--r--src/aig/fra/fraLcr.c644
-rw-r--r--src/aig/fra/fraMan.c8
-rw-r--r--src/aig/fra/fraSec.c136
-rw-r--r--src/aig/fra/fraSim.c12
-rw-r--r--src/aig/fra/module.make1
-rw-r--r--src/base/abc/abc.h1
-rw-r--r--src/base/abc/abcUtil.c27
-rw-r--r--src/base/abci/abc.c335
-rw-r--r--src/base/abci/abcDar.c128
-rw-r--r--src/base/abci/abcPrint.c3
-rw-r--r--src/base/abci/abcStrash.c3
-rw-r--r--src/base/abci/abcXsim.c26
-rw-r--r--src/opt/fxu/fxu.c14
-rw-r--r--src/opt/fxu/fxu.h3
-rw-r--r--src/opt/fxu/fxuCreate.c21
-rw-r--r--src/opt/fxu/fxuInt.h4
-rw-r--r--src/opt/fxu/fxuSingle.c138
-rw-r--r--src/opt/fxu/fxuUpdate.c3
33 files changed, 2220 insertions, 560 deletions
diff --git a/abc.dsp b/abc.dsp
index 17c2006a..c4f6e05f 100644
--- a/abc.dsp
+++ b/abc.dsp
@@ -2586,6 +2586,10 @@ SOURCE=.\src\aig\fra\fraInd.c
# End Source File
# Begin Source File
+SOURCE=.\src\aig\fra\fraLcr.c
+# End Source File
+# Begin Source File
+
SOURCE=.\src\aig\fra\fraMan.c
# End Source File
# Begin Source File
@@ -2794,6 +2798,10 @@ SOURCE=.\src\aig\aig\aigRet.c
# End Source File
# Begin Source File
+SOURCE=.\src\aig\aig\aigScl.c
+# End Source File
+# Begin Source File
+
SOURCE=.\src\aig\aig\aigSeq.c
# End Source File
# Begin Source File
diff --git a/src/aig/aig/aig.h b/src/aig/aig/aig.h
index 1ee62ad6..a6428e65 100644
--- a/src/aig/aig/aig.h
+++ b/src/aig/aig/aig.h
@@ -128,6 +128,8 @@ struct Aig_Man_t_
int fCatchExor; // enables EXOR nodes
int fAddStrash; // performs additional strashing
Aig_Obj_t ** pObjCopies; // mapping of AIG nodes into FRAIG nodes
+ void (*pImpFunc) (void*, void*); // implication checking precedure
+ void * pImpData; // implication checking data
// timing statistics
int time1;
int time2;
@@ -298,6 +300,9 @@ static inline void Aig_ManRecycleMemory( Aig_Man_t * p, Aig_Obj_t * pEntry )
// iterator over the primary outputs
#define Aig_ManForEachPo( p, pObj, i ) \
Vec_PtrForEachEntry( p->vPos, pObj, i )
+// iterator over the assertions
+#define Aig_ManForEachAssert( p, pObj, i ) \
+ Vec_PtrForEachEntryStart( p->vPos, pObj, i, Aig_ManPoNum(p)-p->nAsserts )
// iterator over all objects, including those currently not used
#define Aig_ManForEachObj( p, pObj, i ) \
Vec_PtrForEachEntry( p->vObjs, pObj, i ) if ( (pObj) == NULL ) {} else
@@ -373,15 +378,12 @@ extern void Aig_ManFanoutStop( Aig_Man_t * p );
/*=== aigMan.c ==========================================================*/
extern Aig_Man_t * Aig_ManStart( int nNodesMax );
extern Aig_Man_t * Aig_ManStartFrom( Aig_Man_t * p );
+extern Aig_Obj_t * Aig_ManDup_rec( Aig_Man_t * pNew, Aig_Man_t * p, Aig_Obj_t * pObj );
extern Aig_Man_t * Aig_ManDup( Aig_Man_t * p, int fOrdered );
-extern Aig_Man_t * Aig_ManRemap( Aig_Man_t * p, Vec_Ptr_t * vMap );
extern Aig_Man_t * Aig_ManExtractMiter( Aig_Man_t * p, Aig_Obj_t * pNode1, Aig_Obj_t * pNode2 );
extern void Aig_ManStop( Aig_Man_t * p );
extern int Aig_ManCleanup( Aig_Man_t * p );
-extern int Aig_ManCountMergeRegs( Aig_Man_t * p );
-extern int Aig_ManSeqCleanup( Aig_Man_t * p );
extern void Aig_ManPrintStats( Aig_Man_t * p );
-extern Aig_Man_t * Aig_ManReduceLaches( Aig_Man_t * p, int fVerbose );
/*=== aigMem.c ==========================================================*/
extern void Aig_ManStartMemory( Aig_Man_t * p );
extern void Aig_ManStopMemory( Aig_Man_t * p );
@@ -436,6 +438,11 @@ extern Aig_Man_t * Aig_ManRehash( Aig_Man_t * p );
extern void Aig_ManCreateChoices( Aig_Man_t * p );
/*=== aigRet.c ========================================================*/
extern Aig_Man_t * Rtm_ManRetime( Aig_Man_t * p, int fForward, int nStepsMax, int fVerbose );
+/*=== aigScl.c ==========================================================*/
+extern Aig_Man_t * Aig_ManRemap( Aig_Man_t * p, Vec_Ptr_t * vMap );
+extern int Aig_ManSeqCleanup( Aig_Man_t * p );
+extern int Aig_ManCountMergeRegs( Aig_Man_t * p );
+extern Aig_Man_t * Aig_ManReduceLaches( Aig_Man_t * p, int fVerbose );
/*=== aigSeq.c ========================================================*/
extern int Aig_ManSeqStrash( Aig_Man_t * p, int nLatches, int * pInits );
/*=== aigShow.c ========================================================*/
diff --git a/src/aig/aig/aigMan.c b/src/aig/aig/aigMan.c
index 122daaa4..076cc420 100644
--- a/src/aig/aig/aigMan.c
+++ b/src/aig/aig/aigMan.c
@@ -172,54 +172,6 @@ Aig_Man_t * Aig_ManDup( Aig_Man_t * p, int fOrdered )
/**Function*************************************************************
- Synopsis [Remaps the manager.]
-
- Description [Map in the array specifies for each CI nodes the node that
- should be used after remapping.]
-
- SideEffects []
-
- SeeAlso []
-
-***********************************************************************/
-Aig_Man_t * Aig_ManRemap( Aig_Man_t * p, Vec_Ptr_t * vMap )
-{
- Aig_Man_t * pNew;
- Aig_Obj_t * pObj, * pObjMapped;
- int i;
- // create the new manager
- pNew = Aig_ManStart( Aig_ManObjIdMax(p) + 1 );
- pNew->nRegs = p->nRegs;
- pNew->nAsserts = p->nAsserts;
- // create the PIs
- Aig_ManCleanData( p );
- Aig_ManConst1(p)->pData = Aig_ManConst1(pNew);
- Aig_ManForEachPi( p, pObj, i )
- pObj->pData = Aig_ObjCreatePi(pNew);
- // implement the mapping
- Aig_ManForEachPi( p, pObj, i )
- {
- pObjMapped = Vec_PtrEntry( vMap, i );
- pObj->pData = Aig_NotCond( Aig_Regular(pObjMapped)->pData, Aig_IsComplement(pObjMapped) );
- }
- // duplicate internal nodes
- Aig_ManForEachObj( p, pObj, i )
- if ( Aig_ObjIsBuf(pObj) )
- pObj->pData = Aig_ObjChild0Copy(pObj);
- else if ( Aig_ObjIsNode(pObj) )
- pObj->pData = Aig_And( pNew, Aig_ObjChild0Copy(pObj), Aig_ObjChild1Copy(pObj) );
- // add the POs
- Aig_ManForEachPo( p, pObj, i )
- Aig_ObjCreatePo( pNew, Aig_ObjChild0Copy(pObj) );
- assert( Aig_ManNodeNum(p) >= Aig_ManNodeNum(pNew) );
- // check the resulting network
- if ( !Aig_ManCheck(pNew) )
- printf( "Aig_ManDup(): The check has failed.\n" );
- return pNew;
-}
-
-/**Function*************************************************************
-
Synopsis [Extracts the miter composed of XOR of the two nodes.]
Description []
@@ -306,110 +258,6 @@ void Aig_ManStop( Aig_Man_t * p )
SeeAlso []
***********************************************************************/
-void Aig_ManSeqCleanup_rec( Aig_Man_t * p, Aig_Obj_t * pObj, Vec_Ptr_t * vNodes )
-{
- if ( Aig_ObjIsTravIdCurrent(p, pObj) )
- return;
- Aig_ObjSetTravIdCurrent(p, pObj);
- // collect latch input corresponding to unmarked PI (latch output)
- if ( Aig_ObjIsPi(pObj) )
- {
- Vec_PtrPush( vNodes, pObj->pNext );
- return;
- }
- if ( Aig_ObjIsPo(pObj) )
- {
- Aig_ManSeqCleanup_rec( p, Aig_ObjFanin0(pObj), vNodes );
- return;
- }
- assert( Aig_ObjIsNode(pObj) );
- Aig_ManSeqCleanup_rec( p, Aig_ObjFanin0(pObj), vNodes );
- Aig_ManSeqCleanup_rec( p, Aig_ObjFanin1(pObj), vNodes );
-}
-
-/**Function*************************************************************
-
- Synopsis [Returns the number of dangling nodes removed.]
-
- Description []
-
- SideEffects []
-
- SeeAlso []
-
-***********************************************************************/
-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 );
-
- // mark the PIs
- Aig_ManIncrementTravId( p );
- Aig_ObjSetTravIdCurrent( p, Aig_ManConst1(p) );
- Aig_ManForEachPiSeq( p, pObj, i )
- Aig_ObjSetTravIdCurrent( p, pObj );
-
- // prepare to collect nodes reachable from POs
- vNodes = Vec_PtrAlloc( 100 );
- Aig_ManForEachPoSeq( p, pObj, i )
- Vec_PtrPush( vNodes, pObj );
-
- // remember latch inputs in latch outputs
- Aig_ManForEachLiLoSeq( p, pObjLi, pObjLo, i )
- pObjLo->pNext = pObjLi;
- // mark the nodes reachable from these nodes
- Vec_PtrForEachEntry( vNodes, pObj, i )
- Aig_ManSeqCleanup_rec( p, pObj, vNodes );
- assert( Vec_PtrSize(vNodes) <= Aig_ManPoNum(p) );
- // clean latch output pointers
- Aig_ManForEachLiLoSeq( p, pObjLi, pObjLo, i )
- pObjLo->pNext = NULL;
-
- // if some latches are removed, update PIs/POs
- if ( Vec_PtrSize(vNodes) < Aig_ManPoNum(p) )
- {
- // collect new CIs/COs
- vCis = Vec_PtrAlloc( Aig_ManPiNum(p) );
- Aig_ManForEachPi( p, pObj, i )
- if ( Aig_ObjIsTravIdCurrent(p, pObj) )
- Vec_PtrPush( vCis, pObj );
- vCos = Vec_PtrAlloc( Aig_ManPoNum(p) );
- Aig_ManForEachPo( p, pObj, i )
- if ( Aig_ObjIsTravIdCurrent(p, pObj) )
- Vec_PtrPush( vCos, pObj );
- else
- Aig_ObjDisconnect( p, pObj );
- // remember the number of true PIs/POs
- nTruePis = Aig_ManPiNum(p) - Aig_ManRegNum(p);
- nTruePos = Aig_ManPoNum(p) - Aig_ManRegNum(p);
- // set the new number of registers
- p->nRegs -= Aig_ManPoNum(p) - Vec_PtrSize(vNodes);
- // create new PIs/POs
- assert( Vec_PtrSize(vCis) == nTruePis + p->nRegs );
- assert( Vec_PtrSize(vCos) == nTruePos + p->nRegs );
- Vec_PtrFree( p->vPis ); p->vPis = vCis;
- Vec_PtrFree( p->vPos ); p->vPos = vCos;
- p->nObjs[AIG_OBJ_PI] = Vec_PtrSize( p->vPis );
- p->nObjs[AIG_OBJ_PO] = Vec_PtrSize( p->vPos );
- }
- Vec_PtrFree( vNodes );
- // remove dangling nodes
- return Aig_ManCleanup( p );
-}
-
-/**Function*************************************************************
-
- Synopsis [Returns the number of dangling nodes removed.]
-
- Description []
-
- SideEffects []
-
- SeeAlso []
-
-***********************************************************************/
int Aig_ManCleanup( Aig_Man_t * p )
{
Vec_Ptr_t * vObjs;
@@ -430,42 +278,6 @@ int Aig_ManCleanup( Aig_Man_t * p )
/**Function*************************************************************
- Synopsis [Returns the number of dangling nodes removed.]
-
- Description []
-
- SideEffects []
-
- SeeAlso []
-
-***********************************************************************/
-int Aig_ManCountMergeRegs( Aig_Man_t * p )
-{
- Aig_Obj_t * pObj, * pFanin;
- int i, Counter = 0, Const0 = 0, Const1 = 0;
- Aig_ManIncrementTravId( p );
- Aig_ManForEachLiSeq( p, pObj, i )
- {
- pFanin = Aig_ObjFanin0(pObj);
- if ( Aig_ObjIsConst1(pFanin) )
- {
- if ( Aig_ObjFaninC0(pObj) )
- Const0++;
- else
- Const1++;
- }
- if ( Aig_ObjIsTravIdCurrent(p, pFanin) )
- continue;
- Aig_ObjSetTravIdCurrent(p, pFanin);
- Counter++;
- }
- printf( "Regs = %d. Fanins = %d. Const0 = %d. Const1 = %d.\n",
- Aig_ManRegNum(p), Counter, Const0, Const1 );
- return 0;
-}
-
-/**Function*************************************************************
-
Synopsis [Stops the AIG manager.]
Description []
@@ -491,149 +303,6 @@ void Aig_ManPrintStats( Aig_Man_t * p )
printf( "\n" );
}
-/**Function*************************************************************
-
- Synopsis [Checks how many latches can be reduced.]
-
- Description []
-
- SideEffects []
-
- SeeAlso []
-
-***********************************************************************/
-int Aig_ManReduceLachesCount( Aig_Man_t * p )
-{
- Aig_Obj_t * pObj, * pFanin;
- int i, Counter = 0;
- assert( Aig_ManRegNum(p) > 0 );
- Aig_ManForEachObj( p, pObj, i )
- assert( !pObj->fMarkA && !pObj->fMarkB );
- Aig_ManForEachLiSeq( p, pObj, i )
- {
- pFanin = Aig_ObjFanin0(pObj);
- if ( Aig_ObjFaninC0(pObj) )
- {
- if ( pFanin->fMarkB )
- Counter++;
- else
- pFanin->fMarkB = 1;
- }
- else
- {
- if ( pFanin->fMarkA )
- Counter++;
- else
- pFanin->fMarkA = 1;
- }
- }
- Aig_ManForEachLiSeq( p, pObj, i )
- {
- pFanin = Aig_ObjFanin0(pObj);
- pFanin->fMarkA = pFanin->fMarkB = 0;
- }
- return Counter;
-}
-
-/**Function*************************************************************
-
- Synopsis [Reduces the latches.]
-
- Description []
-
- SideEffects []
-
- SeeAlso []
-
-***********************************************************************/
-Vec_Ptr_t * Aig_ManReduceLachesOnce( Aig_Man_t * p )
-{
- Vec_Ptr_t * vMap;
- Aig_Obj_t * pObj, * pObjLi, * pObjLo, * pFanin;
- int * pMapping, i;
- // start mapping by adding the true PIs
- vMap = Vec_PtrAlloc( Aig_ManPiNum(p) );
- Aig_ManForEachPiSeq( p, pObj, i )
- Vec_PtrPush( vMap, pObj );
- // create mapping of fanin nodes into the corresponding latch outputs
- pMapping = ALLOC( int, 2 * (Aig_ManObjIdMax(p) + 1) );
- Aig_ManForEachLiLoSeq( p, pObjLi, pObjLo, i )
- {
- pFanin = Aig_ObjFanin0(pObjLi);
- if ( Aig_ObjFaninC0(pObjLi) )
- {
- if ( pFanin->fMarkB )
- {
- Vec_PtrPush( vMap, Aig_ManLo(p, pMapping[2*pFanin->Id + 1]) );
- }
- else
- {
- pFanin->fMarkB = 1;
- pMapping[2*pFanin->Id + 1] = i;
- Vec_PtrPush( vMap, pObjLo );
- }
- }
- else
- {
- if ( pFanin->fMarkA )
- {
- Vec_PtrPush( vMap, Aig_ManLo(p, pMapping[2*pFanin->Id]) );
- }
- else
- {
- pFanin->fMarkA = 1;
- pMapping[2*pFanin->Id] = i;
- Vec_PtrPush( vMap, pObjLo );
- }
- }
- }
- free( pMapping );
- Aig_ManForEachLiSeq( p, pObj, i )
- {
- pFanin = Aig_ObjFanin0(pObj);
- pFanin->fMarkA = pFanin->fMarkB = 0;
- }
- return vMap;
-}
-
-/**Function*************************************************************
-
- Synopsis [Reduces the latches.]
-
- Description []
-
- SideEffects []
-
- SeeAlso []
-
-***********************************************************************/
-Aig_Man_t * Aig_ManReduceLaches( Aig_Man_t * p, int fVerbose )
-{
- Aig_Man_t * pTemp;
- Vec_Ptr_t * vMap;
- int nSaved, nCur;
- for ( nSaved = 0; nCur = Aig_ManReduceLachesCount(p); nSaved += nCur )
- {
- if ( fVerbose )
- {
- printf( "Saved = %5d. ", nCur );
- printf( "RBeg = %5d. NBeg = %6d. ", Aig_ManRegNum(p), Aig_ManNodeNum(p) );
- }
- vMap = Aig_ManReduceLachesOnce( p );
- p = Aig_ManRemap( pTemp = p, vMap );
- Aig_ManStop( pTemp );
- Vec_PtrFree( vMap );
- Aig_ManSeqCleanup( p );
- if ( fVerbose )
- {
- printf( "REnd = %5d. NEnd = %6d. ", Aig_ManRegNum(p), Aig_ManNodeNum(p) );
- printf( "\n" );
- }
- }
- return p;
-}
-
-
////////////////////////////////////////////////////////////////////////
/// END OF FILE ///
////////////////////////////////////////////////////////////////////////
diff --git a/src/aig/aig/aigPart.c b/src/aig/aig/aigPart.c
index f616bc25..d230f0d9 100644
--- a/src/aig/aig/aigPart.c
+++ b/src/aig/aig/aigPart.c
@@ -321,7 +321,7 @@ Vec_Vec_t * Aig_ManSupports( Aig_Man_t * pMan )
}
assert( 0 );
}
-printf( "Memory usage = %d Mb.\n", Vec_PtrSize(p->vMemory) * p->nChunkSize / (1<<20) );
+//printf( "Memory usage = %d Mb.\n", Vec_PtrSize(p->vMemory) * p->nChunkSize / (1<<20) );
Part_ManStop( p );
// sort supports by size
Vec_VecSort( vSupps, 1 );
diff --git a/src/aig/aig/aigRepr.c b/src/aig/aig/aigRepr.c
index 3e588979..cea3c438 100644
--- a/src/aig/aig/aigRepr.c
+++ b/src/aig/aig/aigRepr.c
@@ -253,7 +253,7 @@ Aig_Obj_t * Aig_ManDupRepr_rec( Aig_Man_t * pNew, Aig_Man_t * p, Aig_Obj_t * pOb
***********************************************************************/
Aig_Man_t * Aig_ManDupRepr( Aig_Man_t * p )
{
- int fOrdered = 1;
+ int fOrdered = 0;
Aig_Man_t * pNew;
Aig_Obj_t * pObj;
int i;
diff --git a/src/aig/aig/aigScl.c b/src/aig/aig/aigScl.c
new file mode 100644
index 00000000..f8989446
--- /dev/null
+++ b/src/aig/aig/aigScl.c
@@ -0,0 +1,370 @@
+/**CFile****************************************************************
+
+ FileName [aigScl.c]
+
+ SystemName [ABC: Logic synthesis and verification system.]
+
+ PackageName [AIG package.]
+
+ Synopsis [Sequential cleanup.]
+
+ Author [Alan Mishchenko]
+
+ Affiliation [UC Berkeley]
+
+ Date [Ver. 1.0. Started - April 28, 2007.]
+
+ Revision [$Id: aigScl.c,v 1.00 2007/04/28 00:00:00 alanmi Exp $]
+
+***********************************************************************/
+
+#include "aig.h"
+
+////////////////////////////////////////////////////////////////////////
+/// DECLARATIONS ///
+////////////////////////////////////////////////////////////////////////
+
+////////////////////////////////////////////////////////////////////////
+/// FUNCTION DEFINITIONS ///
+////////////////////////////////////////////////////////////////////////
+
+/**Function*************************************************************
+
+ Synopsis [Remaps the manager.]
+
+ Description [Map in the array specifies for each CI nodes the node that
+ should be used after remapping.]
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+Aig_Man_t * Aig_ManRemap( Aig_Man_t * p, Vec_Ptr_t * vMap )
+{
+ Aig_Man_t * pNew;
+ Aig_Obj_t * pObj, * pObjMapped;
+ int i;
+ // create the new manager
+ pNew = Aig_ManStart( Aig_ManObjIdMax(p) + 1 );
+ pNew->nRegs = p->nRegs;
+ pNew->nAsserts = p->nAsserts;
+ // create the PIs
+ Aig_ManCleanData( p );
+ Aig_ManConst1(p)->pData = Aig_ManConst1(pNew);
+ Aig_ManForEachPi( p, pObj, i )
+ pObj->pData = Aig_ObjCreatePi(pNew);
+ // implement the mapping
+ Aig_ManForEachPi( p, pObj, i )
+ {
+ pObjMapped = Vec_PtrEntry( vMap, i );
+ pObj->pData = Aig_NotCond( Aig_Regular(pObjMapped)->pData, Aig_IsComplement(pObjMapped) );
+ }
+ // duplicate internal nodes
+ Aig_ManForEachObj( p, pObj, i )
+ if ( Aig_ObjIsBuf(pObj) )
+ pObj->pData = Aig_ObjChild0Copy(pObj);
+ else if ( Aig_ObjIsNode(pObj) )
+ pObj->pData = Aig_And( pNew, Aig_ObjChild0Copy(pObj), Aig_ObjChild1Copy(pObj) );
+ // add the POs
+ Aig_ManForEachPo( p, pObj, i )
+ Aig_ObjCreatePo( pNew, Aig_ObjChild0Copy(pObj) );
+ assert( Aig_ManNodeNum(p) >= Aig_ManNodeNum(pNew) );
+ // check the resulting network
+ if ( !Aig_ManCheck(pNew) )
+ printf( "Aig_ManDup(): The check has failed.\n" );
+ return pNew;
+}
+
+/**Function*************************************************************
+
+ Synopsis [Returns the number of dangling nodes removed.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+void Aig_ManSeqCleanup_rec( Aig_Man_t * p, Aig_Obj_t * pObj, Vec_Ptr_t * vNodes )
+{
+ if ( Aig_ObjIsTravIdCurrent(p, pObj) )
+ return;
+ Aig_ObjSetTravIdCurrent(p, pObj);
+ // collect latch input corresponding to unmarked PI (latch output)
+ if ( Aig_ObjIsPi(pObj) )
+ {
+ Vec_PtrPush( vNodes, pObj->pNext );
+ return;
+ }
+ if ( Aig_ObjIsPo(pObj) )
+ {
+ Aig_ManSeqCleanup_rec( p, Aig_ObjFanin0(pObj), vNodes );
+ return;
+ }
+ assert( Aig_ObjIsNode(pObj) );
+ Aig_ManSeqCleanup_rec( p, Aig_ObjFanin0(pObj), vNodes );
+ Aig_ManSeqCleanup_rec( p, Aig_ObjFanin1(pObj), vNodes );
+}
+
+/**Function*************************************************************
+
+ Synopsis [Returns the number of dangling nodes removed.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+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 );
+
+ // mark the PIs
+ Aig_ManIncrementTravId( p );
+ Aig_ObjSetTravIdCurrent( p, Aig_ManConst1(p) );
+ Aig_ManForEachPiSeq( p, pObj, i )
+ Aig_ObjSetTravIdCurrent( p, pObj );
+
+ // prepare to collect nodes reachable from POs
+ vNodes = Vec_PtrAlloc( 100 );
+ Aig_ManForEachPoSeq( p, pObj, i )
+ Vec_PtrPush( vNodes, pObj );
+
+ // remember latch inputs in latch outputs
+ Aig_ManForEachLiLoSeq( p, pObjLi, pObjLo, i )
+ pObjLo->pNext = pObjLi;
+ // mark the nodes reachable from these nodes
+ Vec_PtrForEachEntry( vNodes, pObj, i )
+ Aig_ManSeqCleanup_rec( p, pObj, vNodes );
+ assert( Vec_PtrSize(vNodes) <= Aig_ManPoNum(p) );
+ // clean latch output pointers
+ Aig_ManForEachLiLoSeq( p, pObjLi, pObjLo, i )
+ pObjLo->pNext = NULL;
+
+ // if some latches are removed, update PIs/POs
+ if ( Vec_PtrSize(vNodes) < Aig_ManPoNum(p) )
+ {
+ // collect new CIs/COs
+ vCis = Vec_PtrAlloc( Aig_ManPiNum(p) );
+ Aig_ManForEachPi( p, pObj, i )
+ if ( Aig_ObjIsTravIdCurrent(p, pObj) )
+ Vec_PtrPush( vCis, pObj );
+ vCos = Vec_PtrAlloc( Aig_ManPoNum(p) );
+ Aig_ManForEachPo( p, pObj, i )
+ if ( Aig_ObjIsTravIdCurrent(p, pObj) )
+ Vec_PtrPush( vCos, pObj );
+ else
+ Aig_ObjDisconnect( p, pObj );
+ // remember the number of true PIs/POs
+ nTruePis = Aig_ManPiNum(p) - Aig_ManRegNum(p);
+ nTruePos = Aig_ManPoNum(p) - Aig_ManRegNum(p);
+ // set the new number of registers
+ p->nRegs -= Aig_ManPoNum(p) - Vec_PtrSize(vNodes);
+ // create new PIs/POs
+ assert( Vec_PtrSize(vCis) == nTruePis + p->nRegs );
+ assert( Vec_PtrSize(vCos) == nTruePos + p->nRegs );
+ Vec_PtrFree( p->vPis ); p->vPis = vCis;
+ Vec_PtrFree( p->vPos ); p->vPos = vCos;
+ p->nObjs[AIG_OBJ_PI] = Vec_PtrSize( p->vPis );
+ p->nObjs[AIG_OBJ_PO] = Vec_PtrSize( p->vPos );
+ }
+ Vec_PtrFree( vNodes );
+ // remove dangling nodes
+ return Aig_ManCleanup( p );
+}
+
+/**Function*************************************************************
+
+ Synopsis [Returns the number of dangling nodes removed.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+int Aig_ManCountMergeRegs( Aig_Man_t * p )
+{
+ Aig_Obj_t * pObj, * pFanin;
+ int i, Counter = 0, Const0 = 0, Const1 = 0;
+ Aig_ManIncrementTravId( p );
+ Aig_ManForEachLiSeq( p, pObj, i )
+ {
+ pFanin = Aig_ObjFanin0(pObj);
+ if ( Aig_ObjIsConst1(pFanin) )
+ {
+ if ( Aig_ObjFaninC0(pObj) )
+ Const0++;
+ else
+ Const1++;
+ }
+ if ( Aig_ObjIsTravIdCurrent(p, pFanin) )
+ continue;
+ Aig_ObjSetTravIdCurrent(p, pFanin);
+ Counter++;
+ }
+ printf( "Regs = %d. Fanins = %d. Const0 = %d. Const1 = %d.\n",
+ Aig_ManRegNum(p), Counter, Const0, Const1 );
+ return 0;
+}
+
+
+/**Function*************************************************************
+
+ Synopsis [Checks how many latches can be reduced.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+int Aig_ManReduceLachesCount( Aig_Man_t * p )
+{
+ Aig_Obj_t * pObj, * pFanin;
+ int i, Counter = 0, Diffs = 0;
+ assert( Aig_ManRegNum(p) > 0 );
+ Aig_ManForEachObj( p, pObj, i )
+ assert( !pObj->fMarkA && !pObj->fMarkB );
+ Aig_ManForEachLiSeq( p, pObj, i )
+ {
+ pFanin = Aig_ObjFanin0(pObj);
+ if ( Aig_ObjFaninC0(pObj) )
+ {
+ if ( pFanin->fMarkB )
+ Counter++;
+ else
+ pFanin->fMarkB = 1;
+ }
+ else
+ {
+ if ( pFanin->fMarkA )
+ Counter++;
+ else
+ pFanin->fMarkA = 1;
+ }
+ }
+ // count fanins that have both attributes
+ Aig_ManForEachLiSeq( p, pObj, i )
+ {
+ pFanin = Aig_ObjFanin0(pObj);
+ Diffs += pFanin->fMarkA && pFanin->fMarkB;
+ pFanin->fMarkA = pFanin->fMarkB = 0;
+ }
+// printf( "Diffs = %d.\n", Diffs );
+ return Counter;
+}
+
+/**Function*************************************************************
+
+ Synopsis [Reduces the latches.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+Vec_Ptr_t * Aig_ManReduceLachesOnce( Aig_Man_t * p )
+{
+ Vec_Ptr_t * vMap;
+ Aig_Obj_t * pObj, * pObjLi, * pObjLo, * pFanin;
+ int * pMapping, i;
+ // start mapping by adding the true PIs
+ vMap = Vec_PtrAlloc( Aig_ManPiNum(p) );
+ Aig_ManForEachPiSeq( p, pObj, i )
+ Vec_PtrPush( vMap, pObj );
+ // create mapping of fanin nodes into the corresponding latch outputs
+ pMapping = ALLOC( int, 2 * (Aig_ManObjIdMax(p) + 1) );
+ Aig_ManForEachLiLoSeq( p, pObjLi, pObjLo, i )
+ {
+ pFanin = Aig_ObjFanin0(pObjLi);
+ if ( Aig_ObjFaninC0(pObjLi) )
+ {
+ if ( pFanin->fMarkB )
+ {
+ Vec_PtrPush( vMap, Aig_ManLo(p, pMapping[2*pFanin->Id + 1]) );
+ }
+ else
+ {
+ pFanin->fMarkB = 1;
+ pMapping[2*pFanin->Id + 1] = i;
+ Vec_PtrPush( vMap, pObjLo );
+ }
+ }
+ else
+ {
+ if ( pFanin->fMarkA )
+ {
+ Vec_PtrPush( vMap, Aig_ManLo(p, pMapping[2*pFanin->Id]) );
+ }
+ else
+ {
+ pFanin->fMarkA = 1;
+ pMapping[2*pFanin->Id] = i;
+ Vec_PtrPush( vMap, pObjLo );
+ }
+ }
+ }
+ free( pMapping );
+ Aig_ManForEachLiSeq( p, pObj, i )
+ {
+ pFanin = Aig_ObjFanin0(pObj);
+ pFanin->fMarkA = pFanin->fMarkB = 0;
+ }
+ return vMap;
+}
+
+/**Function*************************************************************
+
+ Synopsis [Reduces the latches.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+Aig_Man_t * Aig_ManReduceLaches( Aig_Man_t * p, int fVerbose )
+{
+ Aig_Man_t * pTemp;
+ Vec_Ptr_t * vMap;
+ int nSaved, nCur;
+ for ( nSaved = 0; nCur = Aig_ManReduceLachesCount(p); nSaved += nCur )
+ {
+ if ( fVerbose )
+ {
+ printf( "Saved = %5d. ", nCur );
+ printf( "RBeg = %5d. NBeg = %6d. ", Aig_ManRegNum(p), Aig_ManNodeNum(p) );
+ }
+ vMap = Aig_ManReduceLachesOnce( p );
+ p = Aig_ManRemap( pTemp = p, vMap );
+ Aig_ManStop( pTemp );
+ Vec_PtrFree( vMap );
+ Aig_ManSeqCleanup( p );
+ if ( fVerbose )
+ {
+ printf( "REnd = %5d. NEnd = %6d. ", Aig_ManRegNum(p), Aig_ManNodeNum(p) );
+ printf( "\n" );
+ }
+ }
+ return p;
+}
+
+
+////////////////////////////////////////////////////////////////////////
+/// END OF FILE ///
+////////////////////////////////////////////////////////////////////////
+
+
diff --git a/src/aig/aig/aigTsim.c b/src/aig/aig/aigTsim.c
index b8296cb2..e5b96879 100644
--- a/src/aig/aig/aigTsim.c
+++ b/src/aig/aig/aigTsim.c
@@ -24,7 +24,7 @@
/// DECLARATIONS ///
////////////////////////////////////////////////////////////////////////
-#define TSI_MAX_ROUNDS 10000
+#define TSI_MAX_ROUNDS 1000
#define AIG_XVS0 1
#define AIG_XVS1 2
@@ -340,7 +340,7 @@ Vec_Ptr_t * Aig_ManTernarySimulate( Aig_Man_t * p, int fVerbose )
}
if ( f == TSI_MAX_ROUNDS )
{
- printf( "Aig_ManTernarySimulate(): Did not reach a fixed point after %d iterations.\n", TSI_MAX_ROUNDS );
+ printf( "Aig_ManTernarySimulate(): Did not reach a fixed point after %d iterations (not a bug).\n", TSI_MAX_ROUNDS );
Aig_TsiStop( pTsi );
return NULL;
}
diff --git a/src/aig/aig/aigUtil.c b/src/aig/aig/aigUtil.c
index cdf1fdf7..4d99e254 100644
--- a/src/aig/aig/aigUtil.c
+++ b/src/aig/aig/aigUtil.c
@@ -662,7 +662,7 @@ void Aig_ManDumpBlif( Aig_Man_t * p, char * pFileName )
{
FILE * pFile;
Vec_Ptr_t * vNodes;
- Aig_Obj_t * pObj, * pConst1 = NULL;
+ Aig_Obj_t * pObj, * pObjLi, * pObjLo, * pConst1 = NULL;
int i, nDigits, Counter = 0;
if ( Aig_ManPoNum(p) == 0 )
{
@@ -687,14 +687,22 @@ void Aig_ManDumpBlif( Aig_Man_t * p, char * pFileName )
fprintf( pFile, ".model test\n" );
// write PIs
fprintf( pFile, ".inputs" );
- Aig_ManForEachPi( p, pObj, i )
+ Aig_ManForEachPiSeq( p, pObj, i )
fprintf( pFile, " n%0*d", nDigits, (int)pObj->pData );
fprintf( pFile, "\n" );
// write POs
fprintf( pFile, ".outputs" );
- Aig_ManForEachPo( p, pObj, i )
+ Aig_ManForEachPoSeq( p, pObj, i )
fprintf( pFile, " n%0*d", nDigits, (int)pObj->pData );
fprintf( pFile, "\n" );
+ // write latches
+ if ( Aig_ManRegNum(p) )
+ {
+ fprintf( pFile, "\n" );
+ Aig_ManForEachLiLoSeq( p, pObjLi, pObjLo, i )
+ fprintf( pFile, ".latch n%0*d n%0*d 0\n", nDigits, (int)pObjLi->pData, nDigits, (int)pObjLo->pData );
+ fprintf( pFile, "\n" );
+ }
// write nodes
Vec_PtrForEachEntry( vNodes, pObj, i )
{
diff --git a/src/aig/aig/module.make b/src/aig/aig/module.make
index 45ed62ee..d1b1cd3b 100644
--- a/src/aig/aig/module.make
+++ b/src/aig/aig/module.make
@@ -9,6 +9,8 @@ SRC += src/aig/aig/aigCheck.c \
src/aig/aig/aigOrder.c \
src/aig/aig/aigPart.c \
src/aig/aig/aigRepr.c \
+ src/aig/aig/aigRet.c \
+ src/aig/aig/aigScl.c \
src/aig/aig/aigSeq.c \
src/aig/aig/aigTable.c \
src/aig/aig/aigTiming.c \
diff --git a/src/aig/fra/fra.h b/src/aig/fra/fra.h
index 217d1fba..931e0930 100644
--- a/src/aig/fra/fra.h
+++ b/src/aig/fra/fra.h
@@ -77,6 +77,7 @@ struct Fra_Par_t_
int fRewrite; // use rewriting for constraint reduction
int fLatchCorr; // computes latch correspondence only
int fUseImps; // use implications
+ int fWriteImps; // record implications
};
// FRAIG equivalence classes
@@ -148,7 +149,6 @@ struct Fra_Man_t_
// statistics
int nSimRounds;
int nNodesMiter;
- int nLitsZero;
int nLitsBeg;
int nLitsEnd;
int nNodesBeg;
@@ -202,6 +202,10 @@ static inline void Fra_ClassObjSetRepr( Aig_Obj_t * pObj, Aig_Obj_t * pN
static inline Aig_Obj_t * Fra_ObjChild0Fra( Aig_Obj_t * pObj, int i ) { assert( !Aig_IsComplement(pObj) ); return Aig_ObjFanin0(pObj)? Aig_NotCond(Fra_ObjFraig(Aig_ObjFanin0(pObj),i), Aig_ObjFaninC0(pObj)) : NULL; }
static inline Aig_Obj_t * Fra_ObjChild1Fra( Aig_Obj_t * pObj, int i ) { assert( !Aig_IsComplement(pObj) ); return Aig_ObjFanin1(pObj)? Aig_NotCond(Fra_ObjFraig(Aig_ObjFanin1(pObj),i), Aig_ObjFaninC1(pObj)) : NULL; }
+static inline int Fra_ImpLeft( int Imp ) { return Imp & 0xFFFF; }
+static inline int Fra_ImpRight( int Imp ) { return Imp >> 16; }
+static inline int Fra_ImpCreate( int Left, int Right ) { return (Right << 16) | Left; }
+
////////////////////////////////////////////////////////////////////////
/// ITERATORS ///
////////////////////////////////////////////////////////////////////////
@@ -222,7 +226,7 @@ extern void Fra_ClassesCopyReprs( Fra_Cla_t * p, Vec_Ptr_t * vFai
extern void Fra_ClassesPrint( Fra_Cla_t * p, int fVeryVerbose );
extern void Fra_ClassesPrepare( Fra_Cla_t * p, int fLatchCorr );
extern int Fra_ClassesRefine( Fra_Cla_t * p );
-extern int Fra_ClassesRefine1( Fra_Cla_t * p );
+extern int Fra_ClassesRefine1( Fra_Cla_t * p, int fRefineNewClass, int * pSkipped );
extern int Fra_ClassesCountLits( Fra_Cla_t * p );
extern int Fra_ClassesCountPairs( Fra_Cla_t * p );
extern void Fra_ClassesTest( Fra_Cla_t * p, int Id1, int Id2 );
@@ -233,18 +237,24 @@ extern Aig_Man_t * Fra_ClassesDeriveAig( Fra_Cla_t * p, int nFramesK );
/*=== fraCnf.c ========================================================*/
extern void Fra_CnfNodeAddToSolver( Fra_Man_t * p, Aig_Obj_t * pOld, Aig_Obj_t * pNew );
/*=== fraCore.c ========================================================*/
-extern Aig_Man_t * Fra_FraigPerform( Aig_Man_t * pManAig, Fra_Par_t * pPars );
-extern Aig_Man_t * Fra_FraigChoice( Aig_Man_t * pManAig );
extern void Fra_FraigSweep( Fra_Man_t * pManAig );
extern int Fra_FraigMiterStatus( Aig_Man_t * p );
+extern Aig_Man_t * Fra_FraigPerform( Aig_Man_t * pManAig, Fra_Par_t * pPars );
+extern Aig_Man_t * Fra_FraigChoice( Aig_Man_t * pManAig );
+extern Aig_Man_t * Fra_FraigEquivence( Aig_Man_t * pManAig, int nConfMax );
/*=== fraImp.c ========================================================*/
extern Vec_Int_t * Fra_ImpDerive( Fra_Man_t * p, int nImpMaxLimit, int nImpUseLimit, int fLatchCorr );
extern void Fra_ImpAddToSolver( Fra_Man_t * p, Vec_Int_t * vImps, int * pSatVarNums );
extern int Fra_ImpCheckForNode( Fra_Man_t * p, Vec_Int_t * vImps, Aig_Obj_t * pNode, int Pos );
extern int Fra_ImpRefineUsingCex( Fra_Man_t * p, Vec_Int_t * vImps );
extern void Fra_ImpCompactArray( Vec_Int_t * vImps );
+extern double Fra_ImpComputeStateSpaceRatio( Fra_Man_t * p );
+extern int Fra_ImpVerifyUsingSimulation( Fra_Man_t * p );
+extern void Fra_ImpRecordInManager( Fra_Man_t * p, Aig_Man_t * pNew );
/*=== fraInd.c ========================================================*/
-extern Aig_Man_t * Fra_FraigInduction( Aig_Man_t * p, int nFramesP, int nFramesK, int nMaxImps, int fRewrite, int fUseImps, int fLatchCorr, int fVerbose, int * pnIter );
+extern Aig_Man_t * Fra_FraigInduction( Aig_Man_t * p, int nFramesP, int nFramesK, int nMaxImps, int fRewrite, int fUseImps, int fLatchCorr, int fWriteImps, int fVerbose, int * pnIter );
+/*=== fraLcr.c ========================================================*/
+extern Aig_Man_t * Fra_FraigLatchCorrespondence( Aig_Man_t * pAig, int nFramesP, int nConfMax, int fVerbose, int * pnIter );
/*=== fraMan.c ========================================================*/
extern void Fra_ParamsDefault( Fra_Par_t * pParams );
extern void Fra_ParamsDefaultSeq( Fra_Par_t * pParams );
@@ -259,7 +269,7 @@ extern int Fra_NodesAreEquiv( Fra_Man_t * p, Aig_Obj_t * pOld, A
extern int Fra_NodesAreImp( Fra_Man_t * p, Aig_Obj_t * pOld, Aig_Obj_t * pNew, int fComplL, int fComplR );
extern int Fra_NodeIsConst( Fra_Man_t * p, Aig_Obj_t * pNew );
/*=== fraSec.c ========================================================*/
-extern int Fra_FraigSec( Aig_Man_t * p, int nFrames, int fVerbose, int fVeryVerbose );
+extern int Fra_FraigSec( Aig_Man_t * p, int nFrames, int fRetimeFirst, int fVerbose, int fVeryVerbose );
/*=== fraSim.c ========================================================*/
extern int Fra_SmlNodeHash( Aig_Obj_t * pObj, int nTableSize );
extern int Fra_SmlNodeIsConst( Aig_Obj_t * pObj );
diff --git a/src/aig/fra/fraBmc.c b/src/aig/fra/fraBmc.c
index 45c162af..648d08c4 100644
--- a/src/aig/fra/fraBmc.c
+++ b/src/aig/fra/fraBmc.c
@@ -31,6 +31,8 @@ struct Fra_Bmc_t_
int nPref; // the size of the prefix
int nDepth; // the depth of the frames
int nFramesAll; // the total number of timeframes
+ // implications to be filtered
+ Vec_Int_t * vImps;
// AIG managers
Aig_Man_t * pAig; // the original AIG manager
Aig_Man_t * pAigFrames; // initialized timeframes
@@ -67,7 +69,6 @@ static inline Aig_Obj_t * Bmc_ObjChild1Frames( Aig_Obj_t * pObj, int i ) { asse
int Fra_BmcNodesAreEqual( Aig_Obj_t * pObj0, Aig_Obj_t * pObj1 )
{
Fra_Man_t * p = pObj0->pData;
-// Aig_Obj_t ** ppNodes = p->pBmc->pObjToFraig;
Aig_Obj_t * pObjFrames0, * pObjFrames1;
Aig_Obj_t * pObjFraig0, * pObjFraig1;
int i;
@@ -102,6 +103,69 @@ int Fra_BmcNodeIsConst( Aig_Obj_t * pObj )
return Fra_BmcNodesAreEqual( pObj, Aig_ManConst1(p->pManAig) );
}
+/**Function*************************************************************
+
+ Synopsis [Refines implications using BMC.]
+
+ Description [The input is the combinational FRAIG manager,
+ which is used to FRAIG the timeframes. ]
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+void Fra_BmcFilterImplications( Fra_Man_t * p, Fra_Bmc_t * pBmc )
+{
+ Aig_Obj_t * pLeft, * pRight;
+ Aig_Obj_t * pLeftT, * pRightT;
+ Aig_Obj_t * pLeftF, * pRightF;
+ int i, f, Imp, Left, Right;
+ int fComplL, fComplR;
+ assert( p->nFramesAll == 1 );
+ assert( p->pManAig == pBmc->pAigFrames );
+ Vec_IntForEachEntry( pBmc->vImps, Imp, i )
+ {
+ if ( Imp == 0 )
+ continue;
+ Left = Fra_ImpLeft(Imp);
+ Right = Fra_ImpRight(Imp);
+ // get the corresponding nodes
+ pLeft = Aig_ManObj( pBmc->pAig, Left );
+ pRight = Aig_ManObj( pBmc->pAig, Right );
+ // iterate through the timeframes
+ for ( f = pBmc->nPref; f < pBmc->nFramesAll; f++ )
+ {
+ // get timeframes nodes
+ pLeftT = Bmc_ObjFrames( pLeft, f );
+ pRightT = Bmc_ObjFrames( pRight, f );
+ // get the corresponding FRAIG nodes
+ pLeftF = Fra_ObjFraig( Aig_Regular(pLeftT), 0 );
+ pRightF = Fra_ObjFraig( Aig_Regular(pRightT), 0 );
+ // get the complemented attributes
+ fComplL = pLeft->fPhase ^ Aig_IsComplement(pLeftF) ^ Aig_IsComplement(pLeftT);
+ fComplR = pRight->fPhase ^ Aig_IsComplement(pRightF) ^ Aig_IsComplement(pRightT);
+ // check equality
+ if ( Aig_Regular(pLeftF) == Aig_Regular(pRightF) )
+ {
+ if ( fComplL != fComplR )
+ Vec_IntWriteEntry( pBmc->vImps, i, 0 );
+ break;
+ }
+ // check the implication
+ // - if true, a clause is added
+ // - if false, a cex is simulated
+ // make sure the implication is refined
+ if ( Fra_NodesAreImp( p, Aig_Regular(pLeftF), Aig_Regular(pRightF), fComplL, fComplR ) != 1 )
+ {
+ Vec_IntWriteEntry( pBmc->vImps, i, 0 );
+ break;
+ }
+ }
+ }
+ Fra_ImpCompactArray( pBmc->vImps );
+}
+
/**Function*************************************************************
@@ -125,8 +189,6 @@ Fra_Bmc_t * Fra_BmcStart( Aig_Man_t * pAig, int nPref, int nDepth )
p->nFramesAll = nPref + nDepth;
p->pObjToFrames = ALLOC( Aig_Obj_t *, p->nFramesAll * (Aig_ManObjIdMax(pAig) + 1) );
memset( p->pObjToFrames, 0, sizeof(Aig_Obj_t *) * p->nFramesAll * (Aig_ManObjIdMax(pAig) + 1) );
-// p->pObjToFraig = ALLOC( Aig_Obj_t *, p->nFramesAll * (Aig_ManObjIdMax(pAig) + 1) );
-// memset( p->pObjToFraig, 0, sizeof(Aig_Obj_t *) * p->nFramesAll * (Aig_ManObjIdMax(pAig) + 1) );
return p;
}
@@ -215,34 +277,6 @@ Aig_Man_t * Fra_BmcFrames( Fra_Bmc_t * p )
/**Function*************************************************************
- Synopsis [Constructs FRAIG manager for the initialized timeframes.]
-
- Description []
-
- SideEffects []
-
- SeeAlso []
-
-***********************************************************************/
-Aig_Man_t * Fra_BmcFraig( Fra_Bmc_t * p )
-{
- Aig_Man_t * pFraig;
- Fra_Par_t Pars, * pPars = &Pars;
- Fra_ParamsDefault( pPars );
- pPars->nBTLimitNode = 100000;
- pPars->fVerbose = 0;
- pPars->fProve = 0;
- pPars->fDoSparse = 1;
- pPars->fSpeculate = 0;
- pPars->fChoicing = 0;
- pFraig = Fra_FraigPerform( p->pAigFrames, pPars );
- p->pObjToFraig = p->pAigFrames->pObjCopies;
- p->pAigFrames->pObjCopies = NULL;
- return pFraig;
-}
-
-/**Function*************************************************************
-
Synopsis [Performs BMC for the given AIG.]
Description []
@@ -255,12 +289,22 @@ Aig_Man_t * Fra_BmcFraig( Fra_Bmc_t * p )
void Fra_BmcPerform( Fra_Man_t * p, int nPref, int nDepth )
{
Aig_Obj_t * pObj;
- int i, clk = clock();
+ int i, nImpsOld, clk = clock();
assert( p->pBmc == NULL );
// derive and fraig the frames
p->pBmc = Fra_BmcStart( p->pManAig, nPref, nDepth );
p->pBmc->pAigFrames = Fra_BmcFrames( p->pBmc );
- p->pBmc->pAigFraig = Fra_BmcFraig( p->pBmc );
+ // if implications are present, configure the AIG manager to check them
+ if ( p->pCla->vImps )
+ {
+ p->pBmc->pAigFrames->pImpFunc = Fra_BmcFilterImplications;
+ p->pBmc->pAigFrames->pImpData = p->pBmc;
+ p->pBmc->vImps = p->pCla->vImps;
+ nImpsOld = Vec_IntSize(p->pCla->vImps);
+ }
+ p->pBmc->pAigFraig = Fra_FraigEquivence( p->pBmc->pAigFrames, 1000000 );
+ p->pBmc->pObjToFraig = p->pBmc->pAigFrames->pObjCopies;
+ p->pBmc->pAigFrames->pObjCopies = NULL;
// annotate frames nodes with pointers to the manager
Aig_ManForEachObj( p->pBmc->pAigFrames, pObj, i )
pObj->pData = p;
@@ -271,19 +315,31 @@ void Fra_BmcPerform( Fra_Man_t * p, int nPref, int nDepth )
Aig_ManNodeNum(p->pBmc->pAig), p->pBmc->nFramesAll,
Aig_ManNodeNum(p->pBmc->pAigFrames), Aig_ManNodeNum(p->pBmc->pAigFraig) );
PRT( "Time", clock() - clk );
- printf( "Before BMC: " ); Fra_ClassesPrint( p->pCla, 0 );
+ printf( "Before BMC: " );
+// Fra_ClassesPrint( p->pCla, 0 );
+ printf( "Const = %5d. Class = %5d. Lit = %5d. ",
+ Vec_PtrSize(p->pCla->vClasses1), Vec_PtrSize(p->pCla->vClasses), Fra_ClassesCountLits(p->pCla) );
+ if ( p->pCla->vImps && Vec_IntSize(p->pCla->vImps) > 0 )
+ printf( "Imp = %5d. ", nImpsOld );
+ printf( "\n" );
}
// refine the classes
p->pCla->pFuncNodeIsConst = Fra_BmcNodeIsConst;
p->pCla->pFuncNodesAreEqual = Fra_BmcNodesAreEqual;
Fra_ClassesRefine( p->pCla );
- Fra_ClassesRefine1( p->pCla );
+ Fra_ClassesRefine1( p->pCla, 1, NULL );
p->pCla->pFuncNodeIsConst = Fra_SmlNodeIsConst;
p->pCla->pFuncNodesAreEqual = Fra_SmlNodesAreEqual;
// report the results
if ( p->pPars->fVerbose )
{
- printf( "After BMC: " ); Fra_ClassesPrint( p->pCla, 0 );
+ printf( "After BMC: " );
+// Fra_ClassesPrint( p->pCla, 0 );
+ printf( "Const = %5d. Class = %5d. Lit = %5d. ",
+ Vec_PtrSize(p->pCla->vClasses1), Vec_PtrSize(p->pCla->vClasses), Fra_ClassesCountLits(p->pCla) );
+ if ( p->pCla->vImps && Vec_IntSize(p->pCla->vImps) > 0 )
+ printf( "Imp = %5d. ", Vec_IntSize(p->pCla->vImps) );
+ printf( "\n" );
}
// free the BMC manager
Fra_BmcStop( p->pBmc );
diff --git a/src/aig/fra/fraClass.c b/src/aig/fra/fraClass.c
index d6db125b..3e3392c7 100644
--- a/src/aig/fra/fraClass.c
+++ b/src/aig/fra/fraClass.c
@@ -520,10 +520,10 @@ int Fra_ClassesRefine( Fra_Cla_t * p )
SeeAlso []
***********************************************************************/
-int Fra_ClassesRefine1( Fra_Cla_t * p )
+int Fra_ClassesRefine1( Fra_Cla_t * p, int fRefineNewClass, int * pSkipped )
{
Aig_Obj_t * pObj, ** ppClass;
- int i, k, nRefis;
+ int i, k, nRefis = 1;
// check if there is anything to refine
if ( Vec_PtrSize(p->vClasses1) == 0 )
return 0;
@@ -565,7 +565,10 @@ int Fra_ClassesRefine1( Fra_Cla_t * p )
assert( ppClass[0] != NULL );
Vec_PtrPush( p->vClasses, ppClass );
// iteratively refine this class
- nRefis = 1 + Fra_RefineClassLastIter( p, p->vClasses );
+ if ( fRefineNewClass )
+ nRefis += Fra_RefineClassLastIter( p, p->vClasses );
+ else if ( pSkipped )
+ (*pSkipped)++;
return nRefis;
}
diff --git a/src/aig/fra/fraCore.c b/src/aig/fra/fraCore.c
index 9adbb7a9..94beb61a 100644
--- a/src/aig/fra/fraCore.c
+++ b/src/aig/fra/fraCore.c
@@ -246,7 +246,7 @@ static inline void Fra_FraigNode( Fra_Man_t * p, Aig_Obj_t * pObj )
Vec_PtrPush( p->vTimeouts, pObj );
// verify that the counter-example satisfies all the constraints
// if ( p->vCex )
-// Fra_FraigVerifyCounterEx( p, p->vCex );
+// Fra_FraigVerifyCounterEx( p, p->vCex );
// simulate the counter-example and return the Fraig node
Fra_SmlResimulate( p );
if ( !p->pPars->nFramesK && Fra_ClassObjRepr(pObj) == pObjRepr )
@@ -334,12 +334,15 @@ clk = clock();
if ( p->pPars->fChoicing )
Aig_ManReprStart( p->pManFraig, Aig_ManObjIdMax(p->pManAig)+1 );
// collect initial states
- p->nLitsZero = Vec_PtrSize( p->pCla->vClasses1 );
p->nLitsBeg = Fra_ClassesCountLits( p->pCla );
p->nNodesBeg = Aig_ManNodeNum(pManAig);
p->nRegsBeg = Aig_ManRegNum(pManAig);
// perform fraig sweep
Fra_FraigSweep( p );
+ // call back the procedure to check implications
+ if ( pManAig->pImpFunc )
+ pManAig->pImpFunc( p, pManAig->pImpData );
+ // finalize the fraiged manager
Fra_ManFinalizeComb( p );
if ( p->pPars->fChoicing )
{
@@ -397,6 +400,32 @@ Aig_Man_t * Fra_FraigChoice( Aig_Man_t * pManAig )
pPars->fChoicing = 1;
return Fra_FraigPerform( pManAig, pPars );
}
+
+/**Function*************************************************************
+
+ Synopsis []
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+Aig_Man_t * Fra_FraigEquivence( Aig_Man_t * pManAig, int nConfMax )
+{
+ Aig_Man_t * pFraig;
+ Fra_Par_t Pars, * pPars = &Pars;
+ Fra_ParamsDefault( pPars );
+ pPars->nBTLimitNode = nConfMax;
+ pPars->fVerbose = 0;
+ pPars->fProve = 0;
+ pPars->fDoSparse = 1;
+ pPars->fSpeculate = 0;
+ pPars->fChoicing = 0;
+ pFraig = Fra_FraigPerform( pManAig, pPars );
+ return pFraig;
+}
////////////////////////////////////////////////////////////////////////
/// END OF FILE ///
diff --git a/src/aig/fra/fraImp.c b/src/aig/fra/fraImp.c
index 8af11b78..5e4b8c28 100644
--- a/src/aig/fra/fraImp.c
+++ b/src/aig/fra/fraImp.c
@@ -24,10 +24,6 @@
/// DECLARATIONS ///
////////////////////////////////////////////////////////////////////////
-static inline int Sml_ImpLeft( int Imp ) { return Imp & 0xFFFF; }
-static inline int Sml_ImpRight( int Imp ) { return Imp >> 16; }
-static inline int Sml_ImpCreate( int Left, int Right ) { return (Right << 16) | Left; }
-
////////////////////////////////////////////////////////////////////////
/// FUNCTION DEFINITIONS ///
////////////////////////////////////////////////////////////////////////
@@ -43,19 +39,35 @@ static inline int Sml_ImpCreate( int Left, int Right ) { return (Right << 16)
SeeAlso []
***********************************************************************/
+static inline int Fra_SmlCountOnesOne( Fra_Sml_t * p, int Node )
+{
+ unsigned * pSim;
+ int k, Counter = 0;
+ pSim = Fra_ObjSim( p, Node );
+ for ( k = p->nWordsPref; k < p->nWordsTotal; k++ )
+ Counter += Aig_WordCountOnes( pSim[k] );
+ return Counter;
+}
+
+/**Function*************************************************************
+
+ Synopsis [Counts the number of 1s in each siminfo of each node.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
static inline int * Fra_SmlCountOnes( Fra_Sml_t * p )
{
Aig_Obj_t * pObj;
- unsigned * pSim;
- int i, k, * pnBits;
+ int i, * pnBits;
pnBits = ALLOC( int, Aig_ManObjIdMax(p->pAig) + 1 );
memset( pnBits, 0, sizeof(int) * (Aig_ManObjIdMax(p->pAig) + 1) );
Aig_ManForEachObj( p->pAig, pObj, i )
- {
- pSim = Fra_ObjSim( p, i );
- for ( k = p->nWordsPref; k < p->nWordsTotal; k++ )
- pnBits[i] += Aig_WordCountOnes( pSim[k] );
- }
+ pnBits[i] = Fra_SmlCountOnesOne( p, i );
return pnBits;
}
@@ -106,6 +118,27 @@ static inline int Sml_NodeNotImpWeight( Fra_Sml_t * p, int Left, int Right )
/**Function*************************************************************
+ Synopsis [Counts the number of 1s in the reverse implication.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+static inline void Sml_NodeSaveNotImpPatterns( Fra_Sml_t * p, int Left, int Right, unsigned * pResult )
+{
+ unsigned * pSimL, * pSimR;
+ int k;
+ pSimL = Fra_ObjSim( p, Left );
+ pSimR = Fra_ObjSim( p, Right );
+ for ( k = p->nWordsPref; k < p->nWordsTotal; k++ )
+ pResult[k] |= pSimL[k] & ~pSimR[k];
+}
+
+/**Function*************************************************************
+
Synopsis [Returns the array of nodes sorted by the number of 1s.]
Description []
@@ -284,7 +317,6 @@ int Sml_CompareMaxId( unsigned short * pImp1, unsigned short * pImp2 )
***********************************************************************/
Vec_Int_t * Fra_ImpDerive( Fra_Man_t * p, int nImpMaxLimit, int nImpUseLimit, int fLatchCorr )
{
-// Aig_Obj_t * pObj;
int nSimWords = 64;
Fra_Sml_t * pSeq, * pComb;
Vec_Int_t * vImps, * vTemp;
@@ -293,21 +325,13 @@ Vec_Int_t * Fra_ImpDerive( Fra_Man_t * p, int nImpMaxLimit, int nImpUseLimit, in
int nImpsTotal = 0, nImpsTried = 0, nImpsNonSeq = 0, nImpsComb = 0, nImpsCollected = 0;
int CostMin = AIG_INFINITY, CostMax = 0;
int i, k, Imp, CostRange, clk = clock();
+ assert( Aig_ManObjIdMax(p->pManAig) + 1 < (1 << 15) );
assert( nImpMaxLimit > 0 && nImpUseLimit > 0 && nImpUseLimit <= nImpMaxLimit );
// normalize both managers
pComb = Fra_SmlSimulateComb( p->pManAig, nSimWords );
pSeq = Fra_SmlSimulateSeq( p->pManAig, p->pPars->nFramesP, nSimWords, 1 );
// get the nodes sorted by the number of 1s
vNodes = Fra_SmlSortUsingOnes( pSeq, fLatchCorr );
-/*
-Aig_ManForEachObj( p->pManAig, pObj, i )
-{
- printf( "%6s", Aig_ObjIsPi(pObj)? "pi" : (Aig_ObjIsNode(pObj)? "node" : "other" ) );
- printf( "%d (%d) :\n", i, pObj->fPhase );
- Extra_PrintBinary( stdout, Fra_ObjSim( pComb, i ), 64 ); printf( "\n" );
- Extra_PrintBinary( stdout, Fra_ObjSim( pSeq, i ), 64 ); printf( "\n" );
-}
-*/
// count the total number of implications
for ( k = nSimWords * 32; k > 0; k-- )
for ( i = k - 1; i > 0; i-- )
@@ -335,10 +359,8 @@ Aig_ManForEachObj( p->pManAig, pObj, i )
nImpsComb++;
continue;
}
-// printf( "d=%d c=%d ", k-i, Sml_NodeNotImpWeight(pComb, *pNodesI, *pNodesK) );
-
nImpsCollected++;
- Imp = Sml_ImpCreate( *pNodesI, *pNodesK );
+ Imp = Fra_ImpCreate( *pNodesI, *pNodesK );
pImpCosts[ Vec_IntSize(vImps) ] = Sml_NodeNotImpWeight(pComb, *pNodesI, *pNodesK);
CostMin = AIG_MIN( CostMin, pImpCosts[ Vec_IntSize(vImps) ] );
CostMax = AIG_MAX( CostMax, pImpCosts[ Vec_IntSize(vImps) ] );
@@ -368,13 +390,16 @@ finish:
(int (*)(const void *, const void *)) Sml_CompareMaxId );
if ( p->pPars->fVerbose )
{
-printf( "Tot = %d. Try = %d. NonS = %d. C = %d. Found = %d. Cost = [%d < %d < %d] ",
- nImpsTotal, nImpsTried, nImpsNonSeq, nImpsComb, nImpsCollected, CostMin, CostRange, CostMax );
+printf( "Implications: All = %d. Try = %d. NonSeq = %d. Comb = %d. Res = %d.\n",
+ nImpsTotal, nImpsTried, nImpsNonSeq, nImpsComb, nImpsCollected );
+printf( "Implication weight: Min = %d. Pivot = %d. Max = %d. ",
+ CostMin, CostRange, CostMax );
PRT( "Time", clock() - clk );
}
return vImps;
}
+
// the following three procedures are called to
// - add implications to the SAT solver
// - check implications using the SAT solver
@@ -401,8 +426,8 @@ void Fra_ImpAddToSolver( Fra_Man_t * p, Vec_Int_t * vImps, int * pSatVarNums )
Vec_IntForEachEntry( vImps, Imp, i )
{
// get the corresponding nodes
- pLeft = Aig_ManObj( p->pManAig, Sml_ImpLeft(Imp) );
- pRight = Aig_ManObj( p->pManAig, Sml_ImpRight(Imp) );
+ pLeft = Aig_ManObj( p->pManAig, Fra_ImpLeft(Imp) );
+ pRight = Aig_ManObj( p->pManAig, Fra_ImpRight(Imp) );
// check if all the nodes are present
for ( f = 0; f < p->pPars->nFramesK; f++ )
{
@@ -431,7 +456,7 @@ void Fra_ImpAddToSolver( Fra_Man_t * p, Vec_Int_t * vImps, int * pSatVarNums )
// get the complemented attributes
fComplL = pLeft->fPhase ^ Aig_IsComplement(pLeftF);
fComplR = pRight->fPhase ^ Aig_IsComplement(pRightF);
- // get the constaint
+ // get the constraint
// L => R L' v R (complement = L & R')
pLits[0] = 2 * Left + !fComplL;
pLits[1] = 2 * Right + fComplR;
@@ -476,8 +501,8 @@ int Fra_ImpCheckForNode( Fra_Man_t * p, Vec_Int_t * vImps, Aig_Obj_t * pNode, in
{
if ( Imp == 0 )
continue;
- Left = Sml_ImpLeft(Imp);
- Right = Sml_ImpRight(Imp);
+ Left = Fra_ImpLeft(Imp);
+ Right = Fra_ImpRight(Imp);
Max = AIG_MAX( Left, Right );
assert( Max >= pNode->Id );
if ( Max > pNode->Id )
@@ -494,9 +519,6 @@ int Fra_ImpCheckForNode( Fra_Man_t * p, Vec_Int_t * vImps, Aig_Obj_t * pNode, in
// check equality
if ( Aig_Regular(pLeftF) == Aig_Regular(pRightF) )
{
-// assert( fComplL == fComplR );
-// if ( fComplL != fComplR )
-// printf( "Fra_ImpCheckForNode(): Unexpected situation!\n" );
if ( fComplL != fComplR )
Vec_IntWriteEntry( vImps, i, 0 );
continue;
@@ -507,6 +529,7 @@ int Fra_ImpCheckForNode( Fra_Man_t * p, Vec_Int_t * vImps, Aig_Obj_t * pNode, in
// make sure the implication is refined
if ( Fra_NodesAreImp( p, Aig_Regular(pLeftF), Aig_Regular(pRightF), fComplL, fComplR ) == 0 )
{
+ p->pCla->fRefinement = 1;
Fra_SmlResimulate( p );
if ( Vec_IntEntry(vImps, i) != 0 )
printf( "Fra_ImpCheckForNode(): Implication is not refined!\n" );
@@ -536,8 +559,8 @@ int Fra_ImpRefineUsingCex( Fra_Man_t * p, Vec_Int_t * vImps )
if ( Imp == 0 )
continue;
// get the corresponding nodes
- pLeft = Aig_ManObj( p->pManAig, Sml_ImpLeft(Imp) );
- pRight = Aig_ManObj( p->pManAig, Sml_ImpRight(Imp) );
+ pLeft = Aig_ManObj( p->pManAig, Fra_ImpLeft(Imp) );
+ pRight = Aig_ManObj( p->pManAig, Fra_ImpRight(Imp) );
// check if implication holds using this simulation info
if ( !Sml_NodeCheckImp(p->pSml, pLeft->Id, pRight->Id) )
{
@@ -569,6 +592,113 @@ void Fra_ImpCompactArray( Vec_Int_t * vImps )
Vec_IntShrink( vImps, k );
}
+/**Function*************************************************************
+
+ Synopsis [Determines the ratio of the state space by computed implications.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+double Fra_ImpComputeStateSpaceRatio( Fra_Man_t * p )
+{
+ int nSimWords = 64;
+ Fra_Sml_t * pComb;
+ unsigned * pResult;
+ double Ratio = 0.0;
+ int Left, Right, Imp, i;
+ if ( p->pCla->vImps == NULL || Vec_IntSize(p->pCla->vImps) == 0 )
+ return Ratio;
+ // simulate the AIG manager with combinational patterns
+ pComb = Fra_SmlSimulateComb( p->pManAig, nSimWords );
+ // go through the implications and collect where they do not hold
+ pResult = Fra_ObjSim( pComb, 0 );
+ assert( pResult[0] == 0 );
+ Vec_IntForEachEntry( p->pCla->vImps, Imp, i )
+ {
+ Left = Fra_ImpLeft(Imp);
+ Right = Fra_ImpRight(Imp);
+ Sml_NodeSaveNotImpPatterns( pComb, Left, Right, pResult );
+ }
+ // count the number of ones in this area
+ Ratio = 100.0 * Fra_SmlCountOnesOne( pComb, 0 ) / (32*(pComb->nWordsTotal-pComb->nWordsPref));
+ Fra_SmlStop( pComb );
+ return Ratio;
+}
+
+/**Function*************************************************************
+
+ Synopsis [Returns the number of failed implications.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+int Fra_ImpVerifyUsingSimulation( Fra_Man_t * p )
+{
+ int nSimWords = 2000;
+ Fra_Sml_t * pSeq;
+ char * pfFails;
+ int Left, Right, Imp, i, Counter;
+ if ( p->pCla->vImps == NULL || Vec_IntSize(p->pCla->vImps) == 0 )
+ return 0;
+ // simulate the AIG manager with combinational patterns
+ pSeq = Fra_SmlSimulateSeq( p->pManAig, p->pPars->nFramesP, nSimWords, 4 );
+ // go through the implications and check how many of them do not hold
+ pfFails = ALLOC( char, Vec_IntSize(p->pCla->vImps) );
+ memset( pfFails, 0, sizeof(char) * Vec_IntSize(p->pCla->vImps) );
+ Vec_IntForEachEntry( p->pCla->vImps, Imp, i )
+ {
+ Left = Fra_ImpLeft(Imp);
+ Right = Fra_ImpRight(Imp);
+ pfFails[i] = !Sml_NodeCheckImp( pSeq, Left, Right );
+ }
+ // count how many has failed
+ Counter = 0;
+ for ( i = 0; i < Vec_IntSize(p->pCla->vImps); i++ )
+ Counter += pfFails[i];
+ free( pfFails );
+ return Counter;
+}
+
+/**Function*************************************************************
+
+ Synopsis [Record proven implications in the AIG manager.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+void Fra_ImpRecordInManager( Fra_Man_t * p, Aig_Man_t * pNew )
+{
+ Aig_Obj_t * pLeft, * pRight, * pMiter;
+ int nPosOld, Imp, i;
+ if ( p->pCla->vImps == NULL || Vec_IntSize(p->pCla->vImps) == 0 )
+ return;
+ // go through the implication
+ nPosOld = Aig_ManPoNum(pNew);
+ Vec_IntForEachEntry( p->pCla->vImps, Imp, i )
+ {
+ pLeft = Aig_ManObj( p->pManAig, Fra_ImpLeft(Imp) );
+ pRight = Aig_ManObj( p->pManAig, Fra_ImpRight(Imp) );
+ // record the implication: L' + R
+ pMiter = Aig_Or( pNew,
+ Aig_NotCond(pLeft->pData, !pLeft->fPhase),
+ Aig_NotCond(pRight->pData, pRight->fPhase) );
+ Aig_ObjCreatePo( pNew, pMiter );
+ }
+ pNew->nAsserts = Aig_ManPoNum(pNew) - nPosOld;
+}
+
////////////////////////////////////////////////////////////////////////
/// END OF FILE ///
////////////////////////////////////////////////////////////////////////
diff --git a/src/aig/fra/fraInd.c b/src/aig/fra/fraInd.c
index 6d8305c0..53dbdbb6 100644
--- a/src/aig/fra/fraInd.c
+++ b/src/aig/fra/fraInd.c
@@ -177,6 +177,61 @@ Aig_Man_t * Fra_FramesWithClasses( Fra_Man_t * p )
/**Function*************************************************************
+ Synopsis [Prepares the inductive case with speculative reduction.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+void Fra_FramesAddMore( Aig_Man_t * p, int nFrames )
+{
+ Aig_Obj_t * pObj, ** pLatches;
+ int i, k, f, nNodesOld;
+ // set copy pointer of each object to point to itself
+ Aig_ManForEachObj( p, pObj, i )
+ pObj->pData = pObj;
+ // iterate and add objects
+ nNodesOld = Aig_ManObjIdMax(p);
+ pLatches = ALLOC( Aig_Obj_t *, Aig_ManRegNum(p) );
+ for ( f = 0; f < nFrames; f++ )
+ {
+ // clean latch inputs and outputs
+ Aig_ManForEachLiSeq( p, pObj, i )
+ pObj->pData = NULL;
+ Aig_ManForEachLoSeq( p, pObj, i )
+ pObj->pData = NULL;
+ // save the latch input values
+ k = 0;
+ Aig_ManForEachLiSeq( p, pObj, i )
+ {
+ if ( Aig_ObjFanin0(pObj)->pData )
+ pLatches[k++] = Aig_ObjChild0Copy(pObj);
+ else
+ pLatches[k++] = NULL;
+ }
+ // insert them as the latch output values
+ k = 0;
+ Aig_ManForEachLoSeq( p, pObj, i )
+ pObj->pData = pLatches[k++];
+ // create the next time frame of nodes
+ Aig_ManForEachNode( p, pObj, i )
+ {
+ if ( i > nNodesOld )
+ break;
+ if ( Aig_ObjFanin0(pObj)->pData && Aig_ObjFanin1(pObj)->pData )
+ pObj->pData = Aig_And( p, Aig_ObjChild0Copy(pObj), Aig_ObjChild1Copy(pObj) );
+ else
+ pObj->pData = NULL;
+ }
+ }
+ free( pLatches );
+}
+
+/**Function*************************************************************
+
Synopsis [Performs choicing of the AIG.]
Description []
@@ -186,7 +241,7 @@ Aig_Man_t * Fra_FramesWithClasses( Fra_Man_t * p )
SeeAlso []
***********************************************************************/
-Aig_Man_t * Fra_FraigInduction( Aig_Man_t * pManAig, int nFramesP, int nFramesK, int nMaxImps, int fRewrite, int fUseImps, int fLatchCorr, int fVerbose, int * pnIter )
+Aig_Man_t * Fra_FraigInduction( Aig_Man_t * pManAig, int nFramesP, int nFramesK, int nMaxImps, int fRewrite, int fUseImps, int fLatchCorr, int fWriteImps, int fVerbose, int * pnIter )
{
int fUseSimpleCnf = 0;
int fUseOldSimulation = 0;
@@ -201,8 +256,9 @@ Aig_Man_t * Fra_FraigInduction( Aig_Man_t * pManAig, int nFramesP, int nFramesK,
Aig_Obj_t * pObj;
Cnf_Dat_t * pCnf;
Aig_Man_t * pManAigNew;
-// Vec_Int_t * vImps;
+ int nNodesBeg, nRegsBeg, Temp;
int nIter, i, clk = clock(), clk2;
+
if ( Aig_ManNodeNum(pManAig) == 0 )
{
if ( pnIter ) *pnIter = 0;
@@ -212,6 +268,12 @@ Aig_Man_t * Fra_FraigInduction( Aig_Man_t * pManAig, int nFramesP, int nFramesK,
assert( Aig_ManRegNum(pManAig) > 0 );
assert( nFramesK > 0 );
//Aig_ManShow( pManAig, 0, NULL );
+
+ nNodesBeg = Aig_ManNodeNum(pManAig);
+ nRegsBeg = Aig_ManRegNum(pManAig);
+
+ // enhance the AIG by adding timeframes
+// Fra_FramesAddMore( pManAig, 3 );
// get parameters
Fra_ParamsDefaultSeq( pPars );
@@ -222,6 +284,7 @@ Aig_Man_t * Fra_FraigInduction( Aig_Man_t * pManAig, int nFramesP, int nFramesK,
pPars->fRewrite = fRewrite;
pPars->fLatchCorr = fLatchCorr;
pPars->fUseImps = fUseImps;
+ pPars->fWriteImps = fWriteImps;
// start the fraig manager for this run
p = Fra_ManStart( pManAig, pPars );
@@ -255,19 +318,19 @@ PRT( "Time", clock() - clk );
p->pSml = Fra_SmlStart( pManAig, 0, pPars->nFramesK + 1, pPars->nSimWords );
}
- // perform BMC (for the min number of frames)
- Fra_BmcPerform( p, pPars->nFramesP, pPars->nFramesK );
-//Fra_ClassesPrint( p->pCla, 1 );
-// p->vCex = Vec_IntAlloc( 1000 );
-
// select the most expressive implications
if ( pPars->fUseImps )
p->pCla->vImps = Fra_ImpDerive( p, 5000000, pPars->nMaxImps, pPars->fLatchCorr );
-
- p->nLitsZero = Vec_PtrSize( p->pCla->vClasses1 );
+
+ // perform BMC (for the min number of frames)
+ Fra_BmcPerform( p, pPars->nFramesP, pPars->nFramesK+1 ); // +1 is needed to prevent non-refinement
+//Fra_ClassesPrint( p->pCla, 1 );
+// if ( p->vCex == NULL )
+// p->vCex = Vec_IntAlloc( 1000 );
+
p->nLitsBeg = Fra_ClassesCountLits( p->pCla );
- p->nNodesBeg = Aig_ManNodeNum(pManAig);
- p->nRegsBeg = Aig_ManRegNum(pManAig);
+ p->nNodesBeg = nNodesBeg; // Aig_ManNodeNum(pManAig);
+ p->nRegsBeg = nRegsBeg; // Aig_ManRegNum(pManAig);
// dump AIG of the timeframes
// pManAigNew = Fra_ClassesDeriveAig( p->pCla, pPars->nFramesK );
@@ -279,6 +342,8 @@ PRT( "Time", clock() - clk );
p->pCla->fRefinement = 1;
for ( nIter = 0; p->pCla->fRefinement; nIter++ )
{
+ int nLitsOld = Fra_ClassesCountLits(p->pCla);
+ int nImpsOld = p->pCla->vImps? Vec_IntSize(p->pCla->vImps) : 0;
// mark the classes as non-refined
p->pCla->fRefinement = 0;
// derive non-init K-timeframes while implementing e-classes
@@ -325,13 +390,13 @@ PRT( "Time", clock() - clk );
// report the intermediate results
if ( fVerbose )
{
- printf( "%3d : Const = %6d. Class = %6d. L = %6d. LR = %6d. %s = %6d. NR = %6d.\n",
+ printf( "%3d : Const = %6d. Class = %6d. L = %6d. LR = %6d. ",
nIter, Vec_PtrSize(p->pCla->vClasses1), Vec_PtrSize(p->pCla->vClasses),
- Fra_ClassesCountLits(p->pCla), p->pManFraig->nAsserts,
- p->pCla->vImps? "I" : "N",
- p->pCla->vImps? Vec_IntSize(p->pCla->vImps) : Aig_ManNodeNum(p->pManAig),
- Aig_ManNodeNum(p->pManFraig) );
- }
+ 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) );
+ }
// perform sweeping
p->nSatCallsRecent = 0;
@@ -341,18 +406,40 @@ PRT( "Time", clock() - clk );
assert( p->vTimeouts == NULL );
if ( p->vTimeouts )
printf( "Fra_FraigInduction(): SAT solver timed out!\n" );
-
// cleanup
Fra_ManClean( p );
-// if ( nIter == 3 )
-// break;
+ // check if refinement has happened
+// p->pCla->fRefinement = (int)(nLitsOld != Fra_ClassesCountLits(p->pCla));
+ if ( p->pCla->fRefinement &&
+ nLitsOld == Fra_ClassesCountLits(p->pCla) &&
+ nImpsOld == (p->pCla->vImps? Vec_IntSize(p->pCla->vImps) : 0) )
+ {
+ printf( "Fra_FraigInduction(): Internal error. The result may not verify.\n" );
+ break;
+ }
}
-// Fra_ClassesPrint( p->pCla, 1 );
-// Fra_ClassesSelectRepr( p->pCla );
+ // check implications using simulation
+ if ( p->pCla->vImps && Vec_IntSize(p->pCla->vImps) )
+ {
+ int clk = clock();
+ if ( Temp = Fra_ImpVerifyUsingSimulation( p ) )
+ printf( "Implications failing the simulation test = %d (out of %d). ", Temp, Vec_IntSize(p->pCla->vImps) );
+ else
+ printf( "All %d implications have passed the simulation test. ", Vec_IntSize(p->pCla->vImps) );
+ PRT( "Time", clock() - clk );
+ }
+
+
// move the classes into representatives and reduce AIG
clk2 = clock();
+// Fra_ClassesPrint( p->pCla, 1 );
+ Fra_ClassesSelectRepr( p->pCla );
Fra_ClassesCopyReprs( p->pCla, p->vTimeouts );
pManAigNew = Aig_ManDupRepr( pManAig );
+ // add implications to the manager
+ if ( fWriteImps && p->pCla->vImps && Vec_IntSize(p->pCla->vImps) )
+ Fra_ImpRecordInManager( p, pManAigNew );
+ // cleanup the new manager
Aig_ManSeqCleanup( pManAigNew );
// Aig_ManCountMergeRegs( pManAigNew );
p->timeTrav += clock() - clk2;
diff --git a/src/aig/fra/fraLcr.c b/src/aig/fra/fraLcr.c
new file mode 100644
index 00000000..c3b5504e
--- /dev/null
+++ b/src/aig/fra/fraLcr.c
@@ -0,0 +1,644 @@
+/**CFile****************************************************************
+
+ FileName [fraLcorr.c]
+
+ SystemName [ABC: Logic synthesis and verification system.]
+
+ PackageName [New FRAIG package.]
+
+ Synopsis [Latch correspondence computation.]
+
+ Author [Alan Mishchenko]
+
+ Affiliation [UC Berkeley]
+
+ Date [Ver. 1.0. Started - June 30, 2007.]
+
+ Revision [$Id: fraLcorr.c,v 1.00 2007/06/30 00:00:00 alanmi Exp $]
+
+***********************************************************************/
+
+#include "fra.h"
+
+////////////////////////////////////////////////////////////////////////
+/// DECLARATIONS ///
+////////////////////////////////////////////////////////////////////////
+
+typedef struct Fra_Lcr_t_ Fra_Lcr_t;
+struct Fra_Lcr_t_
+{
+ // original AIG
+ Aig_Man_t * pAig;
+ // equivalence class representation
+ Fra_Cla_t * pCla;
+ // partitioning information
+ Vec_Ptr_t * vParts; // output partitions
+ int * pInToOutPart; // mapping of PI num into PO partition num
+ int * pInToOutNum; // mapping of PI num into the num of this PO in the partition
+ // AIGs for the partitions
+ Vec_Ptr_t * vFraigs;
+ // other variables
+ int fRefining;
+ // parameters
+ int nFramesP;
+ int fVerbose;
+ // statistics
+ int nIters;
+ int nLitsBeg;
+ int nLitsEnd;
+ int nNodesBeg;
+ int nNodesEnd;
+ int nRegsBeg;
+ int nRegsEnd;
+ // runtime
+ int timeSim;
+ int timePart;
+ int timeTrav;
+ int timeFraig;
+ int timeUpdate;
+ int timeTotal;
+};
+
+////////////////////////////////////////////////////////////////////////
+/// FUNCTION DEFINITIONS ///
+////////////////////////////////////////////////////////////////////////
+
+/**Function*************************************************************
+
+ Synopsis [Allocates the retiming manager.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+Fra_Lcr_t * Lcr_ManAlloc( Aig_Man_t * pAig )
+{
+ Fra_Lcr_t * p;
+ p = ALLOC( Fra_Lcr_t, 1 );
+ memset( p, 0, sizeof(Fra_Lcr_t) );
+ p->pAig = pAig;
+ p->pInToOutPart = ALLOC( int, Aig_ManPiNum(pAig) );
+ memset( p->pInToOutPart, 0, sizeof(int) * Aig_ManPiNum(pAig) );
+ p->pInToOutNum = ALLOC( int, Aig_ManPiNum(pAig) );
+ memset( p->pInToOutNum, 0, sizeof(int) * Aig_ManPiNum(pAig) );
+ p->vFraigs = Vec_PtrAlloc( 1000 );
+ return p;
+}
+
+/**Function*************************************************************
+
+ Synopsis [Prints stats for the fraiging manager.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+void Lcr_ManPrint( Fra_Lcr_t * p )
+{
+ printf( "Iterations = %d. LitBeg = %d. LitEnd = %d. (%6.2f %%).\n",
+ p->nIters, p->nLitsBeg, p->nLitsEnd, 100.0*p->nLitsEnd/p->nLitsBeg );
+ printf( "NBeg = %d. NEnd = %d. (Gain = %6.2f %%). RBeg = %d. REnd = %d. (Gain = %6.2f %%).\n",
+ p->nNodesBeg, p->nNodesEnd, 100.0*(p->nNodesBeg-p->nNodesEnd)/p->nNodesBeg,
+ p->nRegsBeg, p->nRegsEnd, 100.0*(p->nRegsBeg-p->nRegsEnd)/p->nRegsBeg );
+ PRT( "AIG simulation ", p->timeSim );
+ PRT( "AIG partitioning", p->timePart );
+ PRT( "AIG rebuiding ", p->timeTrav );
+ PRT( "FRAIGing ", p->timeFraig );
+ PRT( "AIG updating ", p->timeUpdate );
+ PRT( "TOTAL RUNTIME ", p->timeTotal );
+}
+
+/**Function*************************************************************
+
+ Synopsis [Deallocates the retiming manager.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+void Lcr_ManFree( Fra_Lcr_t * p )
+{
+ Aig_Obj_t * pObj;
+ int i;
+ if ( p->fVerbose )
+ Lcr_ManPrint( p );
+ Aig_ManForEachPi( p->pAig, pObj, i )
+ pObj->pNext = NULL;
+ Vec_PtrFree( p->vFraigs );
+ if ( p->pCla ) Fra_ClassesStop( p->pCla );
+ if ( p->vParts ) Vec_VecFree( (Vec_Vec_t *)p->vParts );
+ free( p->pInToOutPart );
+ free( p->pInToOutNum );
+ free( p );
+}
+
+/**Function*************************************************************
+
+ Synopsis [Prepare the AIG for class computation.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+Fra_Man_t * Fra_LcrAigPrepare( Aig_Man_t * pAig )
+{
+ Fra_Man_t * p;
+ Aig_Obj_t * pObj;
+ int i;
+ p = ALLOC( Fra_Man_t, 1 );
+ memset( p, 0, sizeof(Fra_Man_t) );
+ Aig_ManForEachPi( pAig, pObj, i )
+ pObj->pData = p;
+ return p;
+}
+
+/**Function*************************************************************
+
+ Synopsis [Prepare the AIG for class computation.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+void Fra_LcrAigPrepareTwo( Aig_Man_t * pAig, Fra_Man_t * p )
+{
+ Aig_Obj_t * pObj;
+ int i;
+ Aig_ManForEachPi( pAig, pObj, i )
+ pObj->pData = p;
+}
+
+/**Function*************************************************************
+
+ Synopsis [Compares two nodes for equivalence after partitioned fraiging.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+int Fra_LcrNodesAreEqual( Aig_Obj_t * pObj0, Aig_Obj_t * pObj1 )
+{
+ Fra_Man_t * pTemp = pObj0->pData;
+ Fra_Lcr_t * pLcr = (Fra_Lcr_t *)pTemp->pBmc;
+ Aig_Man_t * pFraig;
+ Aig_Obj_t * pOut0, * pOut1;
+ int nPart0, nPart1;
+ assert( Aig_ObjIsPi(pObj0) );
+ assert( Aig_ObjIsPi(pObj1) );
+ // find the partition to which these nodes belong
+ nPart0 = pLcr->pInToOutPart[(int)pObj0->pNext];
+ nPart1 = pLcr->pInToOutPart[(int)pObj1->pNext];
+ // if this is the result of refinement of the class created const-1 nodes
+ // the nodes may end up in different partions - we assume them equivalent
+ if ( nPart0 != nPart1 )
+ {
+ assert( 0 );
+ return 1;
+ }
+ assert( nPart0 == nPart1 );
+ pFraig = Vec_PtrEntry( pLcr->vFraigs, nPart0 );
+ // get the fraig outputs
+ pOut0 = Aig_ManPo( pFraig, pLcr->pInToOutNum[(int)pObj0->pNext] );
+ pOut1 = Aig_ManPo( pFraig, pLcr->pInToOutNum[(int)pObj1->pNext] );
+ return Aig_ObjFanin0(pOut0) == Aig_ObjFanin0(pOut1);
+}
+
+/**Function*************************************************************
+
+ Synopsis [Compares the node with a constant after partioned fraiging.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+int Fra_LcrNodeIsConst( Aig_Obj_t * pObj )
+{
+ Fra_Man_t * pTemp = pObj->pData;
+ Fra_Lcr_t * pLcr = (Fra_Lcr_t *)pTemp->pBmc;
+ Aig_Man_t * pFraig;
+ Aig_Obj_t * pOut;
+ int nPart;
+ assert( Aig_ObjIsPi(pObj) );
+ // find the partition to which these nodes belong
+ nPart = pLcr->pInToOutPart[(int)pObj->pNext];
+ pFraig = Vec_PtrEntry( pLcr->vFraigs, nPart );
+ // get the fraig outputs
+ pOut = Aig_ManPo( pFraig, pLcr->pInToOutNum[(int)pObj->pNext] );
+ return Aig_ObjFanin0(pOut) == Aig_ManConst1(pFraig);
+}
+
+/**Function*************************************************************
+
+ Synopsis [Give the AIG and classes, reduces AIG for partitioning.]
+
+ Description [Ignores registers that are not in the classes.
+ Places candidate equivalent classes of registers into single outputs
+ (for ease of partitioning). The resulting combinational AIG contains
+ outputs in the same order as equivalence classes of registers,
+ followed by constant-1 registers. Preserves the set of all inputs.
+ Complemented attributes of the outputs do not matter because we need
+ then only for collecting the structural info.]
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+Aig_Man_t * Fra_LcrDeriveAigForPartitioning( Fra_Lcr_t * pLcr )
+{
+ Aig_Man_t * pNew;
+ Aig_Obj_t * pObj, * pObjPo, * pObjNew, ** ppClass, * pMiter;
+ int i, c, Offset;
+ // remember the numbers of the inputs of the original AIG
+ Aig_ManForEachPi( pLcr->pAig, pObj, i )
+ {
+ pObj->pData = pLcr;
+ pObj->pNext = (Aig_Obj_t *)i;
+ }
+ // compute the LO/LI offset
+ Offset = Aig_ManPoNum(pLcr->pAig) - Aig_ManPiNum(pLcr->pAig);
+ // create the PIs
+ Aig_ManCleanData( pLcr->pAig );
+ pNew = Aig_ManStartFrom( pLcr->pAig );
+ // go over the equivalence classes
+ Vec_PtrForEachEntry( pLcr->pCla->vClasses, ppClass, i )
+ {
+ pMiter = Aig_ManConst0(pNew);
+ for ( c = 0; ppClass[c]; c++ )
+ {
+ assert( Aig_ObjIsPi(ppClass[c]) );
+ pObjPo = Aig_ManPo( pLcr->pAig, Offset+(int)ppClass[c]->pNext );
+ pObjNew = Aig_ManDup_rec( pNew, pLcr->pAig, Aig_ObjFanin0(pObjPo) );
+ pMiter = Aig_Exor( pNew, pMiter, pObjNew );
+ }
+ Aig_ObjCreatePo( pNew, pMiter );
+ }
+ // go over the constant candidates
+ Vec_PtrForEachEntry( pLcr->pCla->vClasses1, pObj, i )
+ {
+ assert( Aig_ObjIsPi(pObj) );
+ pObjPo = Aig_ManPo( pLcr->pAig, Offset+(int)pObj->pNext );
+ pMiter = Aig_ManDup_rec( pNew, pLcr->pAig, Aig_ObjFanin0(pObjPo) );
+ Aig_ObjCreatePo( pNew, pMiter );
+ }
+ return pNew;
+}
+
+/**Function*************************************************************
+
+ Synopsis [Remaps partitions into the inputs of original AIG.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+void Fra_LcrRemapPartitions( Vec_Ptr_t * vParts, Fra_Cla_t * pCla, int * pInToOutPart, int * pInToOutNum )
+{
+ Vec_Int_t * vOne, * vOneNew;
+ Aig_Obj_t ** ppClass, * pObjPi;
+ int Out, Offset, i, k, c;
+ // compute the LO/LI offset
+ Offset = Aig_ManPoNum(pCla->pAig) - Aig_ManPiNum(pCla->pAig);
+ Vec_PtrForEachEntry( vParts, vOne, i )
+ {
+ vOneNew = Vec_IntAlloc( Vec_IntSize(vOne) );
+ Vec_IntForEachEntry( vOne, Out, k )
+ {
+ if ( Out < Vec_PtrSize(pCla->vClasses) )
+ {
+ ppClass = Vec_PtrEntry( pCla->vClasses, Out );
+ for ( c = 0; ppClass[c]; c++ )
+ {
+ pInToOutPart[(int)ppClass[c]->pNext] = i;
+ pInToOutNum[(int)ppClass[c]->pNext] = Vec_IntSize(vOneNew);
+ Vec_IntPush( vOneNew, Offset+(int)ppClass[c]->pNext );
+ }
+ }
+ else
+ {
+ pObjPi = Vec_PtrEntry( pCla->vClasses1, Out - Vec_PtrSize(pCla->vClasses) );
+ pInToOutPart[(int)pObjPi->pNext] = i;
+ pInToOutNum[(int)pObjPi->pNext] = Vec_IntSize(vOneNew);
+ Vec_IntPush( vOneNew, Offset+(int)pObjPi->pNext );
+ }
+ }
+ // replace the class
+ Vec_PtrWriteEntry( vParts, i, vOneNew );
+ Vec_IntFree( vOne );
+ }
+}
+
+/**Function*************************************************************
+
+ Synopsis [Creates AIG of one partition with speculative reduction.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+Aig_Obj_t * Fra_LcrCreatePart_rec( Fra_Cla_t * pCla, Aig_Man_t * pNew, Aig_Man_t * p, Aig_Obj_t * pObj )
+{
+ assert( !Aig_IsComplement(pObj) );
+ if ( Aig_ObjIsTravIdCurrent(p, pObj) )
+ return pObj->pData;
+ Aig_ObjSetTravIdCurrent(p, pObj);
+ if ( Aig_ObjIsPi(pObj) )
+ {
+// Aig_Obj_t * pRepr = Fra_ClassObjRepr(pObj);
+ Aig_Obj_t * pRepr = pCla->pMemRepr[pObj->Id];
+ if ( pRepr == NULL )
+ pObj->pData = Aig_ObjCreatePi( pNew );
+ else
+ {
+ pObj->pData = Fra_LcrCreatePart_rec( pCla, pNew, p, pRepr );
+ pObj->pData = Aig_NotCond( pObj->pData, pRepr->fPhase ^ pObj->fPhase );
+ }
+ return pObj->pData;
+ }
+ Fra_LcrCreatePart_rec( pCla, pNew, p, Aig_ObjFanin0(pObj) );
+ Fra_LcrCreatePart_rec( pCla, pNew, p, Aig_ObjFanin1(pObj) );
+ return pObj->pData = Aig_And( pNew, Aig_ObjChild0Copy(pObj), Aig_ObjChild1Copy(pObj) );
+}
+
+/**Function*************************************************************
+
+ Synopsis [Creates AIG of one partition with speculative reduction.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+Aig_Man_t * Fra_LcrCreatePart( Fra_Lcr_t * p, Vec_Int_t * vPart )
+{
+ Aig_Man_t * pNew;
+ Aig_Obj_t * pObj, * pObjNew;
+ int Out, i;
+ // create new AIG for this partition
+ pNew = Aig_ManStartFrom( p->pAig );
+ Aig_ManIncrementTravId( p->pAig );
+ Aig_ObjSetTravIdCurrent( p->pAig, Aig_ManConst1(p->pAig) );
+ Aig_ManConst1(p->pAig)->pData = Aig_ManConst1(pNew);
+ Vec_IntForEachEntry( vPart, Out, i )
+ {
+ pObj = Aig_ManPo( p->pAig, Out );
+ if ( pObj->fMarkA )
+ {
+ pObjNew = Fra_LcrCreatePart_rec( p->pCla, pNew, p->pAig, Aig_ObjFanin0(pObj) );
+ pObjNew = Aig_NotCond( pObjNew, Aig_ObjFaninC0(pObj) );
+ }
+ else
+ pObjNew = Aig_ManConst1( pNew );
+ Aig_ObjCreatePo( pNew, pObjNew );
+ }
+ return pNew;
+}
+
+/**Function*************************************************************
+
+ Synopsis [Marks the nodes belonging to the equivalence classes.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+void Fra_ClassNodesMark( Fra_Lcr_t * p )
+{
+ Aig_Obj_t * pObj, ** ppClass;
+ int i, c, Offset;
+ // compute the LO/LI offset
+ Offset = Aig_ManPoNum(p->pCla->pAig) - Aig_ManPiNum(p->pCla->pAig);
+ // mark the nodes remaining in the classes
+ Vec_PtrForEachEntry( p->pCla->vClasses1, pObj, i )
+ {
+ pObj = Aig_ManPo( p->pCla->pAig, Offset+(int)pObj->pNext );
+ pObj->fMarkA = 1;
+ }
+ Vec_PtrForEachEntry( p->pCla->vClasses, ppClass, i )
+ {
+ for ( c = 0; ppClass[c]; c++ )
+ {
+ pObj = Aig_ManPo( p->pCla->pAig, Offset+(int)ppClass[c]->pNext );
+ pObj->fMarkA = 1;
+ }
+ }
+}
+
+/**Function*************************************************************
+
+ Synopsis [Unmarks the nodes belonging to the equivalence classes.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+void Fra_ClassNodesUnmark( Fra_Lcr_t * p )
+{
+ Aig_Obj_t * pObj, ** ppClass;
+ int i, c, Offset;
+ // compute the LO/LI offset
+ Offset = Aig_ManPoNum(p->pCla->pAig) - Aig_ManPiNum(p->pCla->pAig);
+ // mark the nodes remaining in the classes
+ Vec_PtrForEachEntry( p->pCla->vClasses1, pObj, i )
+ {
+ pObj = Aig_ManPo( p->pCla->pAig, Offset+(int)pObj->pNext );
+ pObj->fMarkA = 0;
+ }
+ Vec_PtrForEachEntry( p->pCla->vClasses, ppClass, i )
+ {
+ for ( c = 0; ppClass[c]; c++ )
+ {
+ pObj = Aig_ManPo( p->pCla->pAig, Offset+(int)ppClass[c]->pNext );
+ pObj->fMarkA = 0;
+ }
+ }
+}
+
+/**Function*************************************************************
+
+ Synopsis [Performs choicing of the AIG.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+Aig_Man_t * Fra_FraigLatchCorrespondence( Aig_Man_t * pAig, int nFramesP, int nConfMax, int fVerbose, int * pnIter )
+{
+ int nPartSize = 200;
+ int fReprSelect = 0;
+
+ Fra_Lcr_t * p;
+ Fra_Man_t * pTemp;
+ Aig_Man_t * pAigPart, * pAigNew = NULL;
+ Vec_Int_t * vPart;
+ Aig_Obj_t * pObj = Aig_ManObj(pAig, 2078);
+ int i, nIter, clk = clock(), clk2, clk3;
+ if ( Aig_ManNodeNum(pAig) == 0 )
+ {
+ if ( pnIter ) *pnIter = 0;
+ return Aig_ManDup(pAig, 1);
+ }
+ assert( Aig_ManLatchNum(pAig) == 0 );
+ assert( Aig_ManRegNum(pAig) > 0 );
+
+ // start the manager
+ p = Lcr_ManAlloc( pAig );
+ p->nFramesP = nFramesP;
+ p->fVerbose = fVerbose;
+
+ // simulate the AIG
+clk2 = clock();
+if ( fVerbose )
+printf( "Simulating AIG with %d nodes for %d cycles ... ", Aig_ManNodeNum(pAig), nFramesP + 32 );
+ pTemp = Fra_LcrAigPrepare( p->pAig );
+ pTemp->pBmc = (Fra_Bmc_t *)p;
+ pTemp->pSml = Fra_SmlSimulateSeq( p->pAig, p->nFramesP, 32, 1 );
+if ( fVerbose )
+{
+PRT( "Time", clock() - clk2 );
+p->timeSim += clock() - clk2;
+}
+ // get preliminary info about equivalence classes
+ pTemp->pCla = p->pCla = Fra_ClassesStart( p->pAig );
+ Fra_ClassesPrepare( p->pCla, 1 );
+ p->pCla->pFuncNodeIsConst = Fra_LcrNodeIsConst;
+ p->pCla->pFuncNodesAreEqual = Fra_LcrNodesAreEqual;
+ Fra_SmlStop( pTemp->pSml );
+
+ // partition the AIG for latch correspondence computation
+clk2 = clock();
+if ( fVerbose )
+printf( "Partitioning AIG ... " );
+ pAigPart = Fra_LcrDeriveAigForPartitioning( p );
+ p->vParts = (Vec_Ptr_t *)Aig_ManPartitionSmart( pAigPart, nPartSize, 0, NULL );
+ Fra_LcrRemapPartitions( p->vParts, p->pCla, p->pInToOutPart, p->pInToOutNum );
+ Aig_ManStop( pAigPart );
+if ( fVerbose )
+{
+PRT( "Time", clock() - clk2 );
+p->timePart += clock() - clk2;
+}
+
+ // get the initial stats
+ p->nLitsBeg = Fra_ClassesCountLits( p->pCla );
+ p->nNodesBeg = Aig_ManNodeNum(p->pAig);
+ p->nRegsBeg = Aig_ManRegNum(p->pAig);
+
+ // perforn interative reduction of the partitions
+ p->fRefining = 1;
+ for ( nIter = 0; p->fRefining; nIter++ )
+ {
+ p->fRefining = 0;
+ clk3 = clock();
+ // derive AIGs for each partition
+ Fra_ClassNodesMark( p );
+ Vec_PtrClear( p->vFraigs );
+ Vec_PtrForEachEntry( p->vParts, vPart, i )
+ {
+clk2 = clock();
+ pAigPart = Fra_LcrCreatePart( p, vPart );
+p->timeTrav += clock() - clk2;
+clk2 = clock();
+ pAigNew = Fra_FraigEquivence( pAigPart, nConfMax );
+p->timeFraig += clock() - clk2;
+ Vec_PtrPush( p->vFraigs, pAigNew );
+ Aig_ManStop( pAigPart );
+ }
+ Fra_ClassNodesUnmark( p );
+ // report the intermediate results
+ if ( fVerbose )
+ {
+ printf( "%3d : Const = %6d. Class = %6d. L = %6d. Part = %3d. ",
+ nIter, Vec_PtrSize(p->pCla->vClasses1), Vec_PtrSize(p->pCla->vClasses),
+ Fra_ClassesCountLits(p->pCla), Vec_PtrSize(p->vParts) );
+ PRT( "T", clock() - clk3 );
+ }
+ // refine the classes
+ Fra_LcrAigPrepareTwo( p->pAig, pTemp );
+ if ( Fra_ClassesRefine( p->pCla ) )
+ p->fRefining = 1;
+ if ( Fra_ClassesRefine1( p->pCla, 0, NULL ) )
+ p->fRefining = 1;
+ // clean the fraigs
+ Vec_PtrForEachEntry( p->vFraigs, pAigPart, i )
+ Aig_ManStop( pAigPart );
+
+ // repartition if needed
+ if ( 1 )
+ {
+clk2 = clock();
+ Vec_VecFree( (Vec_Vec_t *)p->vParts );
+ pAigPart = Fra_LcrDeriveAigForPartitioning( p );
+ p->vParts = (Vec_Ptr_t *)Aig_ManPartitionSmart( pAigPart, nPartSize, 0, NULL );
+ Fra_LcrRemapPartitions( p->vParts, p->pCla, p->pInToOutPart, p->pInToOutNum );
+ Aig_ManStop( pAigPart );
+p->timePart += clock() - clk2;
+ }
+ }
+ free( pTemp );
+ p->nIters = nIter;
+
+ // move the classes into representatives and reduce AIG
+clk2 = clock();
+// Fra_ClassesPrint( p->pCla, 1 );
+ if ( fReprSelect )
+ Fra_ClassesSelectRepr( p->pCla );
+ Fra_ClassesCopyReprs( p->pCla, NULL );
+ pAigNew = Aig_ManDupRepr( p->pAig );
+ Aig_ManSeqCleanup( pAigNew );
+// Aig_ManCountMergeRegs( pAigNew );
+p->timeUpdate += clock() - clk2;
+p->timeTotal = clock() - clk;
+ // get the final stats
+ p->nLitsEnd = Fra_ClassesCountLits( p->pCla );
+ p->nNodesEnd = Aig_ManNodeNum(pAigNew);
+ p->nRegsEnd = Aig_ManRegNum(pAigNew);
+ Lcr_ManFree( p );
+ if ( pnIter ) *pnIter = nIter;
+ return pAigNew;
+}
+
+
+////////////////////////////////////////////////////////////////////////
+/// END OF FILE ///
+////////////////////////////////////////////////////////////////////////
+
+
diff --git a/src/aig/fra/fraMan.c b/src/aig/fra/fraMan.c
index 0116bbc4..97282e98 100644
--- a/src/aig/fra/fraMan.c
+++ b/src/aig/fra/fraMan.c
@@ -181,6 +181,8 @@ Aig_Man_t * Fra_ManPrepareComb( Fra_Man_t * p )
assert( p->pManFraig == NULL );
// start the fraig package
pManFraig = Aig_ManStart( Aig_ManObjIdMax(p->pManAig) + 1 );
+ pManFraig->nRegs = p->pManAig->nRegs;
+ pManFraig->nAsserts = p->pManAig->nAsserts;
// set the pointers to the available fraig nodes
Fra_ObjSetFraig( Aig_ManConst1(p->pManAig), 0, Aig_ManConst1(pManFraig) );
Aig_ManForEachPi( p->pManAig, pObj, i )
@@ -271,9 +273,9 @@ void Fra_ManPrint( Fra_Man_t * p )
{
double nMemory = 1.0*Aig_ManObjIdMax(p->pManAig)*(p->pSml->nWordsTotal*sizeof(unsigned)+6*sizeof(void*))/(1<<20);
printf( "SimWord = %d. Round = %d. Mem = %0.2f Mb. LitBeg = %d. LitEnd = %d. (%6.2f %%).\n",
- p->pPars->nSimWords, p->pSml->nSimRounds, nMemory, p->nLitsBeg, p->nLitsEnd, 100.0*p->nLitsEnd/p->nLitsBeg );
- printf( "Proof = %d. Cex = %d. Fail = %d. FailReal = %d. Zero = %d. C-lim = %d. Vars = %d.\n",
- p->nSatProof, p->nSatCallsSat, p->nSatFails, p->nSatFailsReal, p->nLitsZero, p->pPars->nBTLimitNode, p->nSatVars );
+ p->pPars->nSimWords, p->pSml->nSimRounds, nMemory, p->nLitsBeg, p->nLitsEnd, 100.0*p->nLitsEnd/(p->nLitsBeg?p->nLitsBeg:1) );
+ printf( "Proof = %d. Cex = %d. Fail = %d. FailReal = %d. C-lim = %d. ImpRatio = %6.2f %%\n",
+ p->nSatProof, p->nSatCallsSat, p->nSatFails, p->nSatFailsReal, p->pPars->nBTLimitNode, Fra_ImpComputeStateSpaceRatio(p) );
printf( "NBeg = %d. NEnd = %d. (Gain = %6.2f %%). RBeg = %d. REnd = %d. (Gain = %6.2f %%).\n",
p->nNodesBeg, p->nNodesEnd, 100.0*(p->nNodesBeg-p->nNodesEnd)/p->nNodesBeg,
p->nRegsBeg, p->nRegsEnd, 100.0*(p->nRegsBeg-p->nRegsEnd)/p->nRegsBeg );
diff --git a/src/aig/fra/fraSec.c b/src/aig/fra/fraSec.c
index 8b9258cb..88c552dc 100644
--- a/src/aig/fra/fraSec.c
+++ b/src/aig/fra/fraSec.c
@@ -39,7 +39,7 @@
SeeAlso []
***********************************************************************/
-int Fra_FraigSec( Aig_Man_t * p, int nFramesFix, int fVerbose, int fVeryVerbose )
+int Fra_FraigSec2( Aig_Man_t * p, int nFramesFix, int fVerbose, int fVeryVerbose )
{
Aig_Man_t * pNew;
int nFrames, RetValue, nIter, clk, clkTotal = clock();
@@ -48,7 +48,7 @@ int Fra_FraigSec( Aig_Man_t * p, int nFramesFix, int fVerbose, int fVeryVerbose
{
nFrames = nFramesFix;
// perform seq sweeping for one frame number
- pNew = Fra_FraigInduction( p, 0, nFrames, 0, 0, 0, fLatchCorr, fVeryVerbose, &nIter );
+ pNew = Fra_FraigInduction( p, 0, nFrames, 0, 0, 0, fLatchCorr, 0, fVeryVerbose, &nIter );
}
else
{
@@ -56,7 +56,7 @@ int Fra_FraigSec( Aig_Man_t * p, int nFramesFix, int fVerbose, int fVeryVerbose
for ( nFrames = 1; ; nFrames++ )
{
clk = clock();
- pNew = Fra_FraigInduction( p, 0, nFrames, 0, 0, 0, fLatchCorr, fVeryVerbose, &nIter );
+ pNew = Fra_FraigInduction( p, 0, nFrames, 0, 0, 0, fLatchCorr, 0, fVeryVerbose, &nIter );
RetValue = Fra_FraigMiterStatus( pNew );
if ( fVerbose )
{
@@ -89,6 +89,136 @@ PRT( "Time", clock() - clkTotal );
}
+/**Function*************************************************************
+
+ Synopsis []
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+int Fra_FraigSec( Aig_Man_t * p, int nFramesFix, int fRetimeFirst, int fVerbose, int fVeryVerbose )
+{
+ Aig_Man_t * pNew, * pTemp;
+ int nFrames, RetValue, nIter, clk, clkTotal = clock();
+ int fLatchCorr = 0;
+
+ pNew = Aig_ManDup( p, 1 );
+ if ( fVerbose )
+ {
+ printf( "Original miter: Latches = %5d. Nodes = %6d.\n",
+ Aig_ManRegNum(pNew), Aig_ManNodeNum(pNew) );
+ }
+//Aig_ManDumpBlif( pNew, "after.blif" );
+
+ // perform sequential cleanup
+clk = clock();
+ pNew = Aig_ManReduceLaches( pNew, 0 );
+ pNew = Aig_ManConstReduce( pNew, 0 );
+ if ( fVerbose )
+ {
+ printf( "Sequential cleanup: Latches = %5d. Nodes = %6d. ",
+ Aig_ManRegNum(pNew), Aig_ManNodeNum(pNew) );
+PRT( "Time", clock() - clk );
+ }
+
+ // perform forward retiming
+ if ( fRetimeFirst )
+ {
+clk = clock();
+ pNew = Rtm_ManRetime( pTemp = pNew, 1, 1000, 0 );
+ Aig_ManStop( pTemp );
+ if ( fVerbose )
+ {
+ printf( "Forward retiming: Latches = %5d. Nodes = %6d. ",
+ Aig_ManRegNum(pNew), Aig_ManNodeNum(pNew) );
+PRT( "Time", clock() - clk );
+ }
+ }
+
+ // run latch correspondence
+clk = clock();
+ pNew = Aig_ManDup( pTemp = pNew, 1 );
+ Aig_ManStop( pTemp );
+ pNew = Fra_FraigLatchCorrespondence( pTemp = pNew, 0, 100000, fVeryVerbose, &nIter );
+ Aig_ManStop( pTemp );
+ if ( fVerbose )
+ {
+ printf( "Latch-corr (I=%3d): Latches = %5d. Nodes = %6d. ",
+ nIter, Aig_ManRegNum(pNew), Aig_ManNodeNum(pNew) );
+PRT( "Time", clock() - clk );
+ }
+
+ // perform fraiging
+clk = clock();
+ pNew = Fra_FraigEquivence( pTemp = pNew, 1000 );
+ Aig_ManStop( pTemp );
+ if ( fVerbose )
+ {
+ printf( "Fraiging: Latches = %5d. Nodes = %6d. ",
+ Aig_ManRegNum(pNew), Aig_ManNodeNum(pNew) );
+PRT( "Time", clock() - clk );
+ }
+
+ // perform seq sweeping while increasing the number of frames
+ RetValue = Fra_FraigMiterStatus( pNew );
+ if ( RetValue == -1 )
+ for ( nFrames = 1; ; nFrames *= 2 )
+ {
+clk = clock();
+ pNew = Fra_FraigInduction( pTemp = pNew, 0, nFrames, 0, 0, 0, fLatchCorr, 0, fVeryVerbose, &nIter );
+ Aig_ManStop( pTemp );
+ RetValue = Fra_FraigMiterStatus( pNew );
+ if ( fVerbose )
+ {
+ printf( "K-step (K=%2d,I=%3d): Latches = %5d. Nodes = %6d. ",
+ nFrames, nIter, Aig_ManRegNum(pNew), Aig_ManNodeNum(pNew) );
+PRT( "Time", clock() - clk );
+ }
+ if ( RetValue != -1 )
+ break;
+ // perform rewriting
+clk = clock();
+ pNew = Aig_ManDup( pTemp = pNew, 1 );
+ Aig_ManStop( pTemp );
+ pNew = Dar_ManRewriteDefault( pTemp = pNew );
+ if ( fVerbose )
+ {
+ printf( "Rewriting: Latches = %5d. Nodes = %6d. ",
+ Aig_ManRegNum(pNew), Aig_ManNodeNum(pNew) );
+PRT( "Time", clock() - clk );
+ }
+ // perform retiming
+clk = clock();
+ pNew = Rtm_ManRetime( pTemp = pNew, 1, 1000, 0 );
+ Aig_ManStop( pTemp );
+ pNew = Aig_ManDup( pTemp = pNew, 1 );
+ Aig_ManStop( pTemp );
+ if ( fVerbose )
+ {
+ printf( "Forward retiming: Latches = %5d. Nodes = %6d. ",
+ Aig_ManRegNum(pNew), Aig_ManNodeNum(pNew) );
+PRT( "Time", clock() - clk );
+ }
+ }
+ // get the miter status
+ RetValue = Fra_FraigMiterStatus( pNew );
+ Aig_ManStop( pNew );
+
+ // report the miter
+ if ( RetValue == 1 )
+ printf( "Networks are equivalent. " );
+ else if ( RetValue == 0 )
+ printf( "Networks are NOT EQUIVALENT. " );
+ else
+ printf( "Networks are UNDECIDED. " );
+PRT( "Time", clock() - clkTotal );
+ return RetValue;
+}
+
////////////////////////////////////////////////////////////////////////
/// END OF FILE ///
////////////////////////////////////////////////////////////////////////
diff --git a/src/aig/fra/fraSim.c b/src/aig/fra/fraSim.c
index 3463ee0d..0b93fb73 100644
--- a/src/aig/fra/fraSim.c
+++ b/src/aig/fra/fraSim.c
@@ -199,7 +199,7 @@ void Fra_SmlSavePattern( Fra_Man_t * p )
Aig_ManForEachPi( p->pManFraig, pObj, i )
if ( p->pSat->model.ptr[Fra_ObjSatNum(pObj)] == l_True )
Aig_InfoSetBit( p->pPatWords, i );
-/*
+
if ( p->vCex )
{
Vec_IntClear( p->vCex );
@@ -208,7 +208,6 @@ void Fra_SmlSavePattern( Fra_Man_t * p )
for ( i = Aig_ManPiNum(p->pManFraig) - Aig_ManRegNum(p->pManFraig); i < Aig_ManPiNum(p->pManFraig); i++ )
Vec_IntPush( p->vCex, Aig_InfoHasBit( p->pPatWords, i ) );
}
-*/
/*
printf( "Pattern: " );
@@ -608,7 +607,7 @@ void Fra_SmlResimulate( Fra_Man_t * p )
return;
clk = clock();
nChanges = Fra_ClassesRefine( p->pCla );
- nChanges += Fra_ClassesRefine1( p->pCla );
+ nChanges += Fra_ClassesRefine1( p->pCla, 1, NULL );
if ( p->pCla->vImps )
nChanges += Fra_ImpRefineUsingCex( p, p->pCla->vImps );
p->timeRef += clock() - clk;
@@ -652,7 +651,7 @@ printf( "Starting classes = %5d. Lits = %6d.\n", Vec_PtrSize(p->pCla->vClasses
return;
clk = clock();
nChanges = Fra_ClassesRefine( p->pCla );
- nChanges += Fra_ClassesRefine1( p->pCla );
+ nChanges += Fra_ClassesRefine1( p->pCla, 1, NULL );
p->timeRef += clock() - clk;
if ( fVerbose )
printf( "Refined classes = %5d. Changes = %4d. Lits = %6d.\n", Vec_PtrSize(p->pCla->vClasses), nChanges, Fra_ClassesCountLits(p->pCla) );
@@ -663,7 +662,7 @@ printf( "Refined classes = %5d. Changes = %4d. Lits = %6d.\n", Vec_PtrSize(
return;
clk = clock();
nChanges = Fra_ClassesRefine( p->pCla );
- nChanges += Fra_ClassesRefine1( p->pCla );
+ nChanges += Fra_ClassesRefine1( p->pCla, 1, NULL );
p->timeRef += clock() - clk;
if ( fVerbose )
@@ -677,7 +676,7 @@ printf( "Refined classes = %5d. Changes = %4d. Lits = %6d.\n", Vec_PtrSize(
return;
clk = clock();
nChanges = Fra_ClassesRefine( p->pCla );
- nChanges += Fra_ClassesRefine1( p->pCla );
+ nChanges += Fra_ClassesRefine1( p->pCla, 1, NULL );
p->timeRef += clock() - clk;
if ( fVerbose )
printf( "Refined classes = %5d. Changes = %4d. Lits = %6d.\n", Vec_PtrSize(p->pCla->vClasses), nChanges, Fra_ClassesCountLits(p->pCla) );
@@ -704,7 +703,6 @@ printf( "Refined classes = %5d. Changes = %4d. Lits = %6d.\n", Vec_PtrSize(
Fra_Sml_t * Fra_SmlStart( Aig_Man_t * pAig, int nPref, int nFrames, int nWordsFrame )
{
Fra_Sml_t * p;
- assert( Aig_ManObjIdMax(pAig) + 1 < (1 << 16) );
p = (Fra_Sml_t *)malloc( sizeof(Fra_Sml_t) + sizeof(unsigned) * (Aig_ManObjIdMax(pAig) + 1) * (nPref + nFrames) * nWordsFrame );
memset( p, 0, sizeof(Fra_Sml_t) + sizeof(unsigned) * (nPref + nFrames) * nWordsFrame );
p->pAig = pAig;
diff --git a/src/aig/fra/module.make b/src/aig/fra/module.make
index bd8a20be..e7264fdc 100644
--- a/src/aig/fra/module.make
+++ b/src/aig/fra/module.make
@@ -5,6 +5,7 @@ SRC += src/aig/fra/fraBmc.c \
src/aig/fra/fraCore.c \
src/aig/fra/fraImp.c \
src/aig/fra/fraInd.c \
+ src/aig/fra/fraLcr.c \
src/aig/fra/fraMan.c \
src/aig/fra/fraSat.c \
src/aig/fra/fraSec.c \
diff --git a/src/base/abc/abc.h b/src/base/abc/abc.h
index bda8781c..42820550 100644
--- a/src/base/abc/abc.h
+++ b/src/base/abc/abc.h
@@ -869,6 +869,7 @@ extern void * Abc_NtkAttrFree( Abc_Ntk_t * pNtk, int Attr, int fFree
extern void Abc_NtkIncrementTravId( Abc_Ntk_t * pNtk );
extern void Abc_NtkOrderCisCos( Abc_Ntk_t * pNtk );
extern int Abc_NtkGetCubeNum( Abc_Ntk_t * pNtk );
+extern int Abc_NtkGetCubePairNum( Abc_Ntk_t * pNtk );
extern int Abc_NtkGetLitNum( Abc_Ntk_t * pNtk );
extern int Abc_NtkGetLitFactNum( Abc_Ntk_t * pNtk );
extern int Abc_NtkGetBddNodeNum( Abc_Ntk_t * pNtk );
diff --git a/src/base/abc/abcUtil.c b/src/base/abc/abcUtil.c
index bb1ae2ed..b4a97223 100644
--- a/src/base/abc/abcUtil.c
+++ b/src/base/abc/abcUtil.c
@@ -148,6 +148,33 @@ int Abc_NtkGetCubeNum( Abc_Ntk_t * pNtk )
/**Function*************************************************************
+ Synopsis [Reads the number of cubes of the node.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+int Abc_NtkGetCubePairNum( Abc_Ntk_t * pNtk )
+{
+ Abc_Obj_t * pNode;
+ int i, nCubes, nCubePairs = 0;
+ assert( Abc_NtkHasSop(pNtk) );
+ Abc_NtkForEachNode( pNtk, pNode, i )
+ {
+ if ( Abc_NodeIsConst(pNode) )
+ continue;
+ assert( pNode->pData );
+ nCubes = Abc_SopGetCubeNum( pNode->pData );
+ nCubePairs += nCubes * (nCubes - 1) / 2;
+ }
+ return nCubePairs;
+}
+
+/**Function*************************************************************
+
Synopsis [Reads the number of literals in the SOPs of the nodes.]
Description []
diff --git a/src/base/abci/abc.c b/src/base/abci/abc.c
index 78519d40..3902830d 100644
--- a/src/base/abci/abc.c
+++ b/src/base/abci/abc.c
@@ -123,6 +123,7 @@ static int Abc_CommandIFraig ( Abc_Frame_t * pAbc, int argc, char ** arg
static int Abc_CommandDFraig ( Abc_Frame_t * pAbc, int argc, char ** argv );
static int Abc_CommandCSweep ( Abc_Frame_t * pAbc, int argc, char ** argv );
static int Abc_CommandIProve ( Abc_Frame_t * pAbc, int argc, char ** argv );
+static int Abc_CommandDProve ( Abc_Frame_t * pAbc, int argc, char ** argv );
static int Abc_CommandHaig ( Abc_Frame_t * pAbc, int argc, char ** argv );
static int Abc_CommandMini ( Abc_Frame_t * pAbc, int argc, char ** argv );
static int Abc_CommandBmc ( Abc_Frame_t * pAbc, int argc, char ** argv );
@@ -166,6 +167,7 @@ static int Abc_CommandRetime ( Abc_Frame_t * pAbc, int argc, char ** arg
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 );
+static int Abc_CommandLcorr ( Abc_Frame_t * pAbc, int argc, char ** argv );
static int Abc_CommandSeqCleanup ( Abc_Frame_t * pAbc, int argc, char ** argv );
static int Abc_CommandCycle ( Abc_Frame_t * pAbc, int argc, char ** argv );
static int Abc_CommandXsim ( Abc_Frame_t * pAbc, int argc, char ** argv );
@@ -326,12 +328,11 @@ void Abc_Init( Abc_Frame_t * pAbc )
Cmd_CommandAdd( pAbc, "Sequential", "init", Abc_CommandInit, 1 );
Cmd_CommandAdd( pAbc, "Sequential", "zero", Abc_CommandZero, 1 );
// Cmd_CommandAdd( pAbc, "Sequential", "pipe", Abc_CommandPipe, 1 );
-// Cmd_CommandAdd( pAbc, "Sequential", "seq", Abc_CommandSeq, 1 );
-// Cmd_CommandAdd( pAbc, "Sequential", "unseq", Abc_CommandUnseq, 1 );
Cmd_CommandAdd( pAbc, "Sequential", "retime", Abc_CommandRetime, 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 );
+ Cmd_CommandAdd( pAbc, "Sequential", "lcorr", Abc_CommandLcorr, 1 );
Cmd_CommandAdd( pAbc, "Sequential", "scleanup", Abc_CommandSeqCleanup, 1 );
Cmd_CommandAdd( pAbc, "Sequential", "cycle", Abc_CommandCycle, 1 );
Cmd_CommandAdd( pAbc, "Sequential", "xsim", Abc_CommandXsim, 0 );
@@ -339,6 +340,7 @@ void Abc_Init( Abc_Frame_t * pAbc )
Cmd_CommandAdd( pAbc, "Verification", "cec", Abc_CommandCec, 0 );
Cmd_CommandAdd( pAbc, "Verification", "sec", Abc_CommandSec, 0 );
Cmd_CommandAdd( pAbc, "Verification", "dsec", Abc_CommandDSec, 0 );
+ Cmd_CommandAdd( pAbc, "Verification", "dprove", Abc_CommandDProve, 0 );
Cmd_CommandAdd( pAbc, "Verification", "sat", Abc_CommandSat, 0 );
Cmd_CommandAdd( pAbc, "Verification", "dsat", Abc_CommandDSat, 0 );
Cmd_CommandAdd( pAbc, "Verification", "prove", Abc_CommandProve, 1 );
@@ -2588,22 +2590,34 @@ int Abc_CommandFastExtract( Abc_Frame_t * pAbc, int argc, char ** argv )
p = ALLOC( Fxu_Data_t, 1 );
memset( p, 0, sizeof(Fxu_Data_t) );
// set the defaults
- p->nPairsMax = 30000;
- p->nNodesExt = 10000;
- p->fOnlyS = 0;
- p->fOnlyD = 0;
- p->fUse0 = 0;
- p->fUseCompl = 1;
- p->fVerbose = 0;
+ p->nSingleMax = 20000;
+ p->nPairsMax = 30000;
+ p->nNodesExt = 10000;
+ p->fOnlyS = 0;
+ p->fOnlyD = 0;
+ p->fUse0 = 0;
+ p->fUseCompl = 1;
+ p->fVerbose = 0;
Extra_UtilGetoptReset();
- while ( (c = Extra_UtilGetopt(argc, argv, "LNsdzcvh")) != EOF )
+ while ( (c = Extra_UtilGetopt(argc, argv, "SDNsdzcvh")) != EOF )
{
switch (c)
{
- case 'L':
+ case 'S':
if ( globalUtilOptind >= argc )
{
- fprintf( pErr, "Command line switch \"-L\" should be followed by an integer.\n" );
+ fprintf( pErr, "Command line switch \"-S\" should be followed by an integer.\n" );
+ goto usage;
+ }
+ p->nSingleMax = atoi(argv[globalUtilOptind]);
+ globalUtilOptind++;
+ if ( p->nSingleMax < 0 )
+ goto usage;
+ break;
+ case 'D':
+ if ( globalUtilOptind >= argc )
+ {
+ fprintf( pErr, "Command line switch \"-D\" should be followed by an integer.\n" );
goto usage;
}
p->nPairsMax = atoi(argv[globalUtilOptind]);
@@ -2643,7 +2657,7 @@ int Abc_CommandFastExtract( Abc_Frame_t * pAbc, int argc, char ** argv )
default:
goto usage;
}
- }
+ }
if ( pNtk == NULL )
{
@@ -2673,10 +2687,11 @@ int Abc_CommandFastExtract( Abc_Frame_t * pAbc, int argc, char ** argv )
return 0;
usage:
- fprintf( pErr, "usage: fx [-N num] [-L num] [-sdzcvh]\n");
+ fprintf( pErr, "usage: fx [-S num] [-D num] [-N num] [-sdzcvh]\n");
fprintf( pErr, "\t performs unate fast extract on the current network\n");
+ fprintf( pErr, "\t-S num : max number of single-cube divisors to consider [default = %d]\n", p->nSingleMax );
+ fprintf( pErr, "\t-D num : max number of double-cube divisors to consider [default = %d]\n", p->nPairsMax );
fprintf( pErr, "\t-N num : the maximum number of divisors to extract [default = %d]\n", p->nNodesExt );
- fprintf( pErr, "\t-L num : the maximum number of cube pairs to consider [default = %d]\n", p->nPairsMax );
fprintf( pErr, "\t-s : use only single-cube divisors [default = %s]\n", p->fOnlyS? "yes": "no" );
fprintf( pErr, "\t-d : use only double-cube divisors [default = %s]\n", p->fOnlyD? "yes": "no" );
fprintf( pErr, "\t-z : use zero-weight divisors [default = %s]\n", p->fUse0? "yes": "no" );
@@ -6175,7 +6190,7 @@ int Abc_CommandTest( Abc_Frame_t * pAbc, int argc, char ** argv )
pErr = Abc_FrameReadErr(pAbc);
// set defaults
- nLevels = 128;
+ nLevels = 1000;
Extra_UtilGetoptReset();
while ( ( c = Extra_UtilGetopt( argc, argv, "Nh" ) ) != EOF )
{
@@ -6293,7 +6308,7 @@ int Abc_CommandTest( Abc_Frame_t * pAbc, int argc, char ** argv )
}
// pNtkRes = Abc_NtkDar( pNtk );
- pNtkRes = Abc_NtkDarRetime( pNtk, 1000, 1 );
+ pNtkRes = Abc_NtkDarRetime( pNtk, nLevels, 1 );
if ( pNtkRes == NULL )
{
fprintf( pErr, "Command has failed.\n" );
@@ -8674,7 +8689,7 @@ int Abc_CommandFraigDress( Abc_Frame_t * pAbc, int argc, char ** argv )
pErr = Abc_FrameReadErr(pAbc);
// set defaults
- fVerbose = 1;
+ fVerbose = 0;
Extra_UtilGetoptReset();
while ( ( c = Extra_UtilGetopt( argc, argv, "vh" ) ) != EOF )
{
@@ -10975,12 +10990,12 @@ int Abc_CommandSeqSweep( Abc_Frame_t * pAbc, int argc, char ** argv )
int nFramesP;
int nFramesK;
int nMaxImps;
- int fExdc;
int fUseImps;
int fRewrite;
int fLatchCorr;
+ int fWriteImps;
int fVerbose;
- extern Abc_Ntk_t * Abc_NtkDarSeqSweep( Abc_Ntk_t * pNtk, int nFramesP, int nFrames, int nMaxImps, int fRewrite, int fUseImps, int fLatchCorr, int fVerbose );
+ extern Abc_Ntk_t * Abc_NtkDarSeqSweep( Abc_Ntk_t * pNtk, int nFramesP, int nFrames, int nMaxImps, int fRewrite, int fUseImps, int fLatchCorr, int fWriteImps, int fVerbose );
pNtk = Abc_FrameReadNtk(pAbc);
pOut = Abc_FrameReadOut(pAbc);
@@ -10990,13 +11005,13 @@ int Abc_CommandSeqSweep( Abc_Frame_t * pAbc, int argc, char ** argv )
nFramesP = 0;
nFramesK = 1;
nMaxImps = 5000;
- fExdc = 1;
fUseImps = 0;
fRewrite = 0;
fLatchCorr = 0;
+ fWriteImps = 0;
fVerbose = 0;
Extra_UtilGetoptReset();
- while ( ( c = Extra_UtilGetopt( argc, argv, "PFIeirlvh" ) ) != EOF )
+ while ( ( c = Extra_UtilGetopt( argc, argv, "PFIirlevh" ) ) != EOF )
{
switch ( c )
{
@@ -11033,9 +11048,6 @@ int Abc_CommandSeqSweep( Abc_Frame_t * pAbc, int argc, char ** argv )
if ( nMaxImps <= 0 )
goto usage;
break;
- case 'e':
- fExdc ^= 1;
- break;
case 'i':
fUseImps ^= 1;
break;
@@ -11045,6 +11057,9 @@ int Abc_CommandSeqSweep( Abc_Frame_t * pAbc, int argc, char ** argv )
case 'l':
fLatchCorr ^= 1;
break;
+ case 'e':
+ fWriteImps ^= 1;
+ break;
case 'v':
fVerbose ^= 1;
break;
@@ -11069,12 +11084,12 @@ int Abc_CommandSeqSweep( Abc_Frame_t * pAbc, int argc, char ** argv )
if ( !Abc_NtkIsStrash(pNtk) )
{
- fprintf( pErr, "Sequential sweep works only for structurally hashed networks (run \"strash\").\n" );
- return 1;
+ printf( "This command works only for structrally hashed networks. Run \"st\".\n" );
+ return 0;
}
// get the new network
- pNtkRes = Abc_NtkDarSeqSweep( pNtk, nFramesP, nFramesK, nMaxImps, fRewrite, fUseImps, fLatchCorr, fVerbose );
+ pNtkRes = Abc_NtkDarSeqSweep( pNtk, nFramesP, nFramesK, nMaxImps, fRewrite, fUseImps, fLatchCorr, fWriteImps, fVerbose );
if ( pNtkRes == NULL )
{
fprintf( pErr, "Sequential sweeping has failed.\n" );
@@ -11085,15 +11100,120 @@ int Abc_CommandSeqSweep( Abc_Frame_t * pAbc, int argc, char ** argv )
return 0;
usage:
- fprintf( pErr, "usage: ssweep [-P num] [-F num] [-I num] [-ilrvh]\n" );
+ fprintf( pErr, "usage: ssweep [-P num] [-F num] [-I num] [-ilrevh]\n" );
fprintf( pErr, "\t performs sequential sweep using K-step induction\n" );
fprintf( pErr, "\t-P num : number of time frames to use as the prefix [default = %d]\n", nFramesP );
fprintf( pErr, "\t-F num : number of time frames for induction (1=simple) [default = %d]\n", nFramesK );
fprintf( pErr, "\t-I num : max number of implications to consider [default = %d]\n", nMaxImps );
-// fprintf( pErr, "\t-e : toggle writing EXDC network [default = %s]\n", fExdc? "yes": "no" );
fprintf( pErr, "\t-i : toggle using implications [default = %s]\n", fUseImps? "yes": "no" );
fprintf( pErr, "\t-l : toggle latch correspondence only [default = %s]\n", fLatchCorr? "yes": "no" );
fprintf( pErr, "\t-r : toggle AIG rewriting [default = %s]\n", fRewrite? "yes": "no" );
+ fprintf( pErr, "\t-e : toggle writing implications as assertions [default = %s]\n", fWriteImps? "yes": "no" );
+ fprintf( pErr, "\t-v : toggle 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_CommandLcorr( Abc_Frame_t * pAbc, int argc, char ** argv )
+{
+ FILE * pOut, * pErr;
+ Abc_Ntk_t * pNtk, * pNtkRes;
+ int c;
+ int nFramesP;
+ int nConfMax;
+ int fVerbose;
+ extern Abc_Ntk_t * Abc_NtkDarLcorr( Abc_Ntk_t * pNtk, int nFramesP, int nConfMax, int fVerbose );
+
+ pNtk = Abc_FrameReadNtk(pAbc);
+ pOut = Abc_FrameReadOut(pAbc);
+ pErr = Abc_FrameReadErr(pAbc);
+
+ // set defaults
+ nFramesP = 0;
+ nConfMax = 10000;
+ fVerbose = 0;
+ Extra_UtilGetoptReset();
+ while ( ( c = Extra_UtilGetopt( argc, argv, "PCvh" ) ) != EOF )
+ {
+ switch ( c )
+ {
+ case 'P':
+ if ( globalUtilOptind >= argc )
+ {
+ fprintf( pErr, "Command line switch \"-P\" should be followed by an integer.\n" );
+ goto usage;
+ }
+ nFramesP = atoi(argv[globalUtilOptind]);
+ globalUtilOptind++;
+ if ( nFramesP < 0 )
+ goto usage;
+ break;
+ case 'C':
+ if ( globalUtilOptind >= argc )
+ {
+ fprintf( pErr, "Command line switch \"-C\" should be followed by an integer.\n" );
+ goto usage;
+ }
+ nConfMax = atoi(argv[globalUtilOptind]);
+ globalUtilOptind++;
+ if ( nConfMax < 0 )
+ goto usage;
+ 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_NtkIsComb(pNtk) )
+ {
+ fprintf( pErr, "The network is combinational (run \"fraig\" or \"fraig_sweep\").\n" );
+ return 1;
+ }
+
+ if ( !Abc_NtkIsStrash(pNtk) )
+ {
+ printf( "This command works only for structrally hashed networks. Run \"st\".\n" );
+ return 0;
+ }
+
+ // get the new network
+ pNtkRes = Abc_NtkDarLcorr( pNtk, nFramesP, nConfMax, fVerbose );
+ if ( pNtkRes == NULL )
+ {
+ fprintf( pErr, "Sequential sweeping has failed.\n" );
+ return 1;
+ }
+ // replace the current network
+ Abc_FrameReplaceCurrentNetwork( pAbc, pNtkRes );
+ return 0;
+
+usage:
+ fprintf( pErr, "usage: lcorr [-P num] [-C num] [-vh]\n" );
+ fprintf( pErr, "\t computes latch correspondence using 1-step induction\n" );
+ fprintf( pErr, "\t-P num : number of time frames to use as the prefix [default = %d]\n", nFramesP );
+ fprintf( pErr, "\t-C num : max conflict number when proving latch equivalence [default = %d]\n", nConfMax );
fprintf( pErr, "\t-v : toggle verbose output [default = %s]\n", fVerbose? "yes": "no" );
fprintf( pErr, "\t-h : print the command usage\n");
return 1;
@@ -11113,12 +11233,12 @@ usage:
int Abc_CommandSeqCleanup( Abc_Frame_t * pAbc, int argc, char ** argv )
{
FILE * pOut, * pErr;
- Abc_Ntk_t * pNtk, * pNtkRes, * pTemp;
+ Abc_Ntk_t * pNtk, * pNtkRes;
int c;
int fLatchSweep;
int fAutoSweep;
int fVerbose;
- extern Abc_Ntk_t * Abc_NtkDarLatchSweep( Abc_Ntk_t * pNtk, int fVerbose );
+ extern Abc_Ntk_t * Abc_NtkDarLatchSweep( Abc_Ntk_t * pNtk, int fLatchSweep, int fVerbose );
pNtk = Abc_FrameReadNtk(pAbc);
pOut = Abc_FrameReadOut(pAbc);
@@ -11153,23 +11273,13 @@ int Abc_CommandSeqCleanup( Abc_Frame_t * pAbc, int argc, char ** argv )
fprintf( pErr, "Empty network.\n" );
return 1;
}
- if ( !Abc_NtkIsLogic(pNtk) )
+ if ( !Abc_NtkIsStrash(pNtk) )
{
- fprintf( pErr, "Only works for logic networks.\n" );
+ fprintf( pErr, "Only works for structrally hashed networks.\n" );
return 1;
}
// modify the current network
-
- // get the new network
- pNtkRes = Abc_NtkDup( pNtk );
- Abc_NtkCleanupSeq( pNtkRes, 0, fAutoSweep, fVerbose );
- if ( fLatchSweep )
- {
- pNtkRes = Abc_NtkStrash( pTemp = pNtkRes, 0, 0, 0 );
- Abc_NtkDelete( pTemp );
- pNtkRes = Abc_NtkDarLatchSweep( pTemp = pNtkRes, fVerbose );
- Abc_NtkDelete( pTemp );
- }
+ pNtkRes = Abc_NtkDarLatchSweep( pNtk, fLatchSweep, fVerbose );
if ( pNtkRes == NULL )
{
fprintf( pErr, "Sequential cleanup has failed.\n" );
@@ -11180,14 +11290,14 @@ int Abc_CommandSeqCleanup( Abc_Frame_t * pAbc, int argc, char ** argv )
return 0;
usage:
- fprintf( pErr, "usage: scleanup [-lavh]\n" );
+ fprintf( pErr, "usage: scleanup [-lvh]\n" );
fprintf( pErr, "\t performs sequential cleanup\n" );
fprintf( pErr, "\t - removes nodes/latches that do not feed into POs\n" );
fprintf( pErr, "\t - removes stuck-at and identical latches (latch sweep)\n" );
- fprintf( pErr, "\t - replaces autonomous logic by free PI variables\n" );
+// fprintf( pErr, "\t - replaces autonomous logic by free PI variables\n" );
fprintf( pErr, "\t (the latter may change sequential behaviour)\n" );
fprintf( pErr, "\t-l : toggle sweeping latches [default = %s]\n", fLatchSweep? "yes": "no" );
- fprintf( pErr, "\t-a : toggle removing autonomous logic [default = %s]\n", fAutoSweep? "yes": "no" );
+// fprintf( pErr, "\t-a : toggle removing autonomous logic [default = %s]\n", fAutoSweep? "yes": "no" );
fprintf( pErr, "\t-v : toggle verbose output [default = %s]\n", fVerbose? "yes": "no" );
fprintf( pErr, "\t-h : print the command usage\n");
return 1;
@@ -11291,9 +11401,10 @@ int Abc_CommandXsim( Abc_Frame_t * pAbc, int argc, char ** argv )
Abc_Ntk_t * pNtk;
int c;
int nFrames;
- int fInputs;
+ int fXInputs;
+ int fXState;
int fVerbose;
- extern void Abc_NtkXValueSimulate( Abc_Ntk_t * pNtk, int nFrames, int fInputs, int fVerbose );
+ extern void Abc_NtkXValueSimulate( Abc_Ntk_t * pNtk, int nFrames, int fXInputs, int fXState, int fVerbose );
pNtk = Abc_FrameReadNtk(pAbc);
pOut = Abc_FrameReadOut(pAbc);
@@ -11301,10 +11412,11 @@ int Abc_CommandXsim( Abc_Frame_t * pAbc, int argc, char ** argv )
// set defaults
nFrames = 10;
- fInputs = 0;
+ fXInputs = 0;
+ fXState = 0;
fVerbose = 0;
Extra_UtilGetoptReset();
- while ( ( c = Extra_UtilGetopt( argc, argv, "Fivh" ) ) != EOF )
+ while ( ( c = Extra_UtilGetopt( argc, argv, "Fisvh" ) ) != EOF )
{
switch ( c )
{
@@ -11320,7 +11432,10 @@ int Abc_CommandXsim( Abc_Frame_t * pAbc, int argc, char ** argv )
goto usage;
break;
case 'i':
- fInputs ^= 1;
+ fXInputs ^= 1;
+ break;
+ case 's':
+ fXState ^= 1;
break;
case 'v':
fVerbose ^= 1;
@@ -11343,14 +11458,15 @@ int Abc_CommandXsim( Abc_Frame_t * pAbc, int argc, char ** argv )
return 1;
}
- Abc_NtkXValueSimulate( pNtk, nFrames, fInputs, fVerbose );
+ Abc_NtkXValueSimulate( pNtk, nFrames, fXInputs, fXState, fVerbose );
return 0;
usage:
- fprintf( pErr, "usage: xsim [-F num] [-ivh]\n" );
+ fprintf( pErr, "usage: xsim [-F num] [-isvh]\n" );
fprintf( pErr, "\t performs X-valued simulation of the AIG\n" );
fprintf( pErr, "\t-F num : the number of frames to simulate [default = %d]\n", nFrames );
- fprintf( pErr, "\t-i : toggle X-valued state or X-valued inputs [default = %s]\n", fInputs? "inputs": "state" );
+ fprintf( pErr, "\t-i : toggle X-valued representation of inputs [default = %s]\n", fXInputs? "yes": "no" );
+ fprintf( pErr, "\t-s : toggle X-valued representation of state [default = %s]\n", fXState? "yes": "no" );
fprintf( pErr, "\t-v : toggle printing verbose information [default = %s]\n", fVerbose? "yes": "no" );
fprintf( pErr, "\t-h : print the command usage\n");
return 1;
@@ -11674,11 +11790,12 @@ int Abc_CommandDSec( Abc_Frame_t * pAbc, int argc, char ** argv )
char ** pArgvNew;
int nArgcNew;
int c;
+ int fRetimeFirst;
int fVerbose;
int fVeryVerbose;
int nFrames;
- extern int Abc_NtkDarSec( Abc_Ntk_t * pNtk1, Abc_Ntk_t * pNtk2, int nFrames, int fVerbose, int fVeryVerbose );
+ extern int Abc_NtkDarSec( Abc_Ntk_t * pNtk1, Abc_Ntk_t * pNtk2, int nFrames, int fRetimeFirst, int fVerbose, int fVeryVerbose );
pNtk = Abc_FrameReadNtk(pAbc);
pOut = Abc_FrameReadOut(pAbc);
@@ -11686,10 +11803,11 @@ int Abc_CommandDSec( Abc_Frame_t * pAbc, int argc, char ** argv )
// set defaults
nFrames = 0; // if 0, iterates through frames
- fVerbose = 1;
+ fRetimeFirst = 1;
+ fVerbose = 0;
fVeryVerbose = 0;
Extra_UtilGetoptReset();
- while ( ( c = Extra_UtilGetopt( argc, argv, "Fwvh" ) ) != EOF )
+ while ( ( c = Extra_UtilGetopt( argc, argv, "Frwvh" ) ) != EOF )
{
switch ( c )
{
@@ -11704,6 +11822,9 @@ int Abc_CommandDSec( Abc_Frame_t * pAbc, int argc, char ** argv )
if ( nFrames <= 0 )
goto usage;
break;
+ case 'r':
+ fRetimeFirst ^= 1;
+ break;
case 'w':
fVeryVerbose ^= 1;
break;
@@ -11727,18 +11848,19 @@ int Abc_CommandDSec( Abc_Frame_t * pAbc, int argc, char ** argv )
}
// perform verification
- Abc_NtkDarSec( pNtk1, pNtk2, nFrames, fVerbose, fVeryVerbose );
+ Abc_NtkDarSec( pNtk1, pNtk2, nFrames, fRetimeFirst, fVerbose, fVeryVerbose );
if ( fDelete1 ) Abc_NtkDelete( pNtk1 );
if ( fDelete2 ) Abc_NtkDelete( pNtk2 );
return 0;
usage:
- fprintf( pErr, "usage: dsec [-F num] [-wvh] <file1> <file2>\n" );
+ fprintf( pErr, "usage: dsec [-F num] [-rwvh] <file1> <file2>\n" );
fprintf( pErr, "\t performs inductive sequential equivalence checking\n" );
fprintf( pErr, "\t-F num : the number of time frames to use [default = %d]\n", nFrames );
- fprintf( pErr, "\t-w : toggles additional verbose output [default = %s]\n", fVeryVerbose? "yes": "no" );
+ fprintf( pErr, "\t-r : toggles forward retiming at the beginning [default = %s]\n", fRetimeFirst? "yes": "no" );
fprintf( pErr, "\t-v : toggles verbose output [default = %s]\n", fVerbose? "yes": "no" );
+ fprintf( pErr, "\t-w : toggles additional verbose output [default = %s]\n", fVeryVerbose? "yes": "no" );
fprintf( pErr, "\t-h : print the command usage\n");
fprintf( pErr, "\tfile1 : (optional) the file with the first network\n");
fprintf( pErr, "\tfile2 : (optional) the file with the second network\n");
@@ -11746,6 +11868,95 @@ usage:
fprintf( pErr, "\t if one file is given, uses the current network and the file\n");
return 1;
}
+
+/**Function*************************************************************
+
+ Synopsis []
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+int Abc_CommandDProve( Abc_Frame_t * pAbc, int argc, char ** argv )
+{
+ FILE * pOut, * pErr;
+ Abc_Ntk_t * pNtk;
+ int c;
+ int fRetimeFirst;
+ int fVerbose;
+ int fVeryVerbose;
+ int nFrames;
+
+ extern int Abc_NtkDarProve( Abc_Ntk_t * pNtk, int nFrames, int fRetimeFirst, int fVerbose, int fVeryVerbose );
+
+ pNtk = Abc_FrameReadNtk(pAbc);
+ pOut = Abc_FrameReadOut(pAbc);
+ pErr = Abc_FrameReadErr(pAbc);
+
+ // set defaults
+ nFrames = 0; // if 0, iterates through frames
+ fRetimeFirst = 1;
+ fVerbose = 0;
+ fVeryVerbose = 0;
+ Extra_UtilGetoptReset();
+ while ( ( c = Extra_UtilGetopt( argc, argv, "Frwvh" ) ) != EOF )
+ {
+ switch ( c )
+ {
+ case 'F':
+ if ( globalUtilOptind >= argc )
+ {
+ fprintf( pErr, "Command line switch \"-F\" should be followed by an integer.\n" );
+ goto usage;
+ }
+ nFrames = atoi(argv[globalUtilOptind]);
+ globalUtilOptind++;
+ if ( nFrames <= 0 )
+ goto usage;
+ break;
+ case 'r':
+ fRetimeFirst ^= 1;
+ break;
+ case 'w':
+ fVeryVerbose ^= 1;
+ break;
+ case 'v':
+ fVerbose ^= 1;
+ break;
+ default:
+ goto usage;
+ }
+ }
+
+ if ( Abc_NtkLatchNum(pNtk) == 0 )
+ {
+ printf( "The network has no latches. Used combinational command \"iprove\".\n" );
+ return 0;
+ }
+ if ( !Abc_NtkIsStrash(pNtk) )
+ {
+ printf( "This command works only for structrally hashed networks. Run \"st\".\n" );
+ return 0;
+ }
+
+ // perform verification
+ Abc_NtkDarProve( pNtk, nFrames, fRetimeFirst, fVerbose, fVeryVerbose );
+ return 0;
+
+usage:
+ fprintf( pErr, "usage: dprove [-F num] [-rwvh]\n" );
+ fprintf( pErr, "\t performs SEC on the sequential miter\n" );
+ fprintf( pErr, "\t-F num : the number of time frames to use [default = %d]\n", nFrames );
+ fprintf( pErr, "\t-r : toggles forward retiming at the beginning [default = %s]\n", fRetimeFirst? "yes": "no" );
+ fprintf( pErr, "\t-v : toggles verbose output [default = %s]\n", fVerbose? "yes": "no" );
+ fprintf( pErr, "\t-w : toggles additional verbose output [default = %s]\n", fVeryVerbose? "yes": "no" );
+ fprintf( pErr, "\t-h : print the command usage\n");
+ return 1;
+}
+
/**Function*************************************************************
Synopsis []
diff --git a/src/base/abci/abcDar.c b/src/base/abci/abcDar.c
index ce783c95..40a52ce8 100644
--- a/src/base/abci/abcDar.c
+++ b/src/base/abci/abcDar.c
@@ -122,6 +122,7 @@ Abc_Ntk_t * Abc_NtkFromDar( Abc_Ntk_t * pNtkOld, Aig_Man_t * pMan )
{
Vec_Ptr_t * vNodes;
Abc_Ntk_t * pNtkNew;
+ Abc_Obj_t * pObjNew;
Aig_Obj_t * pObj;
int i;
assert( Aig_ManRegNum(pMan) == Abc_NtkLatchNum(pNtkOld) );
@@ -141,7 +142,19 @@ Abc_Ntk_t * Abc_NtkFromDar( Abc_Ntk_t * pNtkOld, Aig_Man_t * pMan )
Vec_PtrFree( vNodes );
// connect the PO nodes
Aig_ManForEachPo( pMan, pObj, i )
+ {
+ if ( pMan->nAsserts && i == Aig_ManPoNum(pMan) - pMan->nAsserts )
+ break;
Abc_ObjAddFanin( Abc_NtkCo(pNtkNew, i), (Abc_Obj_t *)Aig_ObjChild0Copy(pObj) );
+ }
+ // if there are assertions, add them
+ if ( pMan->nAsserts > 0 )
+ Aig_ManForEachAssert( pMan, pObj, i )
+ {
+ pObjNew = Abc_NtkCreateAssert(pNtkNew);
+ Abc_ObjAssignName( pObjNew, "assert_", Abc_ObjName(pObjNew) );
+ Abc_ObjAddFanin( pObjNew, (Abc_Obj_t *)Aig_ObjChild0Copy(pObj) );
+ }
if ( !Abc_NtkCheck( pNtkNew ) )
fprintf( stdout, "Abc_NtkFromDar(): Network check has failed.\n" );
return pNtkNew;
@@ -194,7 +207,19 @@ Abc_Ntk_t * Abc_NtkFromDarSeqSweep( Abc_Ntk_t * pNtkOld, Aig_Man_t * pMan )
Vec_PtrFree( vNodes );
// connect the PO nodes
Aig_ManForEachPo( pMan, pObj, i )
+ {
+ if ( pMan->nAsserts && i == Aig_ManPoNum(pMan) - pMan->nAsserts )
+ break;
Abc_ObjAddFanin( Abc_NtkCo(pNtkNew, i), (Abc_Obj_t *)Aig_ObjChild0Copy(pObj) );
+ }
+ // if there are assertions, add them
+ if ( pMan->nAsserts > 0 )
+ Aig_ManForEachAssert( pMan, pObj, i )
+ {
+ pObjNew = Abc_NtkCreateAssert(pNtkNew);
+ Abc_ObjAssignName( pObjNew, "assert_", Abc_ObjName(pObjNew) );
+ Abc_ObjAddFanin( pObjNew, (Abc_Obj_t *)Aig_ObjChild0Copy(pObj) );
+ }
if ( !Abc_NtkCheck( pNtkNew ) )
fprintf( stdout, "Abc_NtkFromDar(): Network check has failed.\n" );
return pNtkNew;
@@ -892,7 +917,7 @@ int Abc_NtkDSat( Abc_Ntk_t * pNtk, sint64 nConfLimit, sint64 nInsLimit, int fVer
SeeAlso []
***********************************************************************/
-Abc_Ntk_t * Abc_NtkDarSeqSweep( Abc_Ntk_t * pNtk, int nFramesP, int nFramesK, int nMaxImps, int fRewrite, int fUseImps, int fLatchCorr, int fVerbose )
+Abc_Ntk_t * Abc_NtkDarSeqSweep( Abc_Ntk_t * pNtk, int nFramesP, int nFramesK, int nMaxImps, int fRewrite, int fUseImps, int fLatchCorr, int fWriteImps, int fVerbose )
{
Fraig_Params_t Params;
Abc_Ntk_t * pNtkAig, * pNtkFraig;
@@ -916,7 +941,7 @@ PRT( "Initial fraiging time", clock() - clk );
if ( pMan == NULL )
return NULL;
- pMan = Fra_FraigInduction( pTemp = pMan, nFramesP, nFramesK, nMaxImps, fRewrite, fUseImps, fLatchCorr, fVerbose, NULL );
+ pMan = Fra_FraigInduction( pTemp = pMan, nFramesP, nFramesK, nMaxImps, fRewrite, fUseImps, fLatchCorr, fWriteImps, fVerbose, NULL );
Aig_ManStop( pTemp );
if ( Aig_ManRegNum(pMan) < Abc_NtkLatchNum(pNtk) )
@@ -929,6 +954,34 @@ PRT( "Initial fraiging time", clock() - clk );
/**Function*************************************************************
+ Synopsis [Computes latch correspondence.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+Abc_Ntk_t * Abc_NtkDarLcorr( Abc_Ntk_t * pNtk, int nFramesP, int nConfMax, int fVerbose )
+{
+ Aig_Man_t * pMan, * pTemp;
+ Abc_Ntk_t * pNtkAig;
+ pMan = Abc_NtkToDar( pNtk, 1 );
+ if ( pMan == NULL )
+ return NULL;
+ pMan = Fra_FraigLatchCorrespondence( pTemp = pMan, nFramesP, nConfMax, fVerbose, NULL );
+ Aig_ManStop( pTemp );
+ if ( Aig_ManRegNum(pMan) < Abc_NtkLatchNum(pNtk) )
+ pNtkAig = Abc_NtkFromDarSeqSweep( pNtk, pMan );
+ else
+ pNtkAig = Abc_NtkFromDar( pNtk, pMan );
+ Aig_ManStop( pMan );
+ return pNtkAig;
+}
+
+/**Function*************************************************************
+
Synopsis [Gives the current ABC network to AIG manager for processing.]
Description []
@@ -938,11 +991,40 @@ PRT( "Initial fraiging time", clock() - clk );
SeeAlso []
***********************************************************************/
-int Abc_NtkDarSec( Abc_Ntk_t * pNtk1, Abc_Ntk_t * pNtk2, int nFrames, int fVerbose, int fVeryVerbose )
+int Abc_NtkDarProve( Abc_Ntk_t * pNtk, int nFrames, int fRetimeFirst, int fVerbose, int fVeryVerbose )
{
- Fraig_Params_t Params;
Aig_Man_t * pMan;
- Abc_Ntk_t * pMiter, * pTemp;
+ int RetValue;
+ // derive the AIG manager
+ pMan = Abc_NtkToDar( pNtk, 1 );
+ if ( pMan == NULL )
+ {
+ printf( "Converting miter into AIG has failed.\n" );
+ return -1;
+ }
+ assert( pMan->nRegs > 0 );
+ // perform verification
+ RetValue = Fra_FraigSec( pMan, nFrames, fRetimeFirst, fVerbose, fVeryVerbose );
+ Aig_ManStop( pMan );
+ return RetValue;
+}
+
+/**Function*************************************************************
+
+ Synopsis [Gives the current ABC network to AIG manager for processing.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+int Abc_NtkDarSec( Abc_Ntk_t * pNtk1, Abc_Ntk_t * pNtk2, int nFrames, int fRetimeFirst, int fVerbose, int fVeryVerbose )
+{
+// Fraig_Params_t Params;
+ Aig_Man_t * pMan;
+ Abc_Ntk_t * pMiter;//, * pTemp;
int RetValue;
// get the miter of the two networks
@@ -971,6 +1053,8 @@ int Abc_NtkDarSec( Abc_Ntk_t * pNtk1, Abc_Ntk_t * pNtk2, int nFrames, int fVerbo
return 1;
}
+ // commented out because something became non-inductive
+/*
// preprocess the miter by fraiging it
// (note that for each functional class, fraiging leaves one representative;
// so fraiging does not reduce the number of functions represented by nodes
@@ -978,7 +1062,25 @@ int Abc_NtkDarSec( Abc_Ntk_t * pNtk1, Abc_Ntk_t * pNtk2, int nFrames, int fVerbo
Params.nBTLimit = 100000;
pMiter = Abc_NtkFraig( pTemp = pMiter, &Params, 0, 0 );
Abc_NtkDelete( pTemp );
-
+ RetValue = Abc_NtkMiterIsConstant( pMiter );
+ if ( RetValue == 0 )
+ {
+ extern void Abc_NtkVerifyReportErrorSeq( Abc_Ntk_t * pNtk1, Abc_Ntk_t * pNtk2, int * pModel, int nFrames );
+ printf( "Networks are NOT EQUIVALENT after structural hashing.\n" );
+ // report the error
+ pMiter->pModel = Abc_NtkVerifyGetCleanModel( pMiter, nFrames );
+ Abc_NtkVerifyReportErrorSeq( pNtk1, pNtk2, pMiter->pModel, nFrames );
+ FREE( pMiter->pModel );
+ Abc_NtkDelete( pMiter );
+ return 0;
+ }
+ if ( RetValue == 1 )
+ {
+ Abc_NtkDelete( pMiter );
+ printf( "Networks are equivalent after structural hashing.\n" );
+ return 1;
+ }
+*/
// derive the AIG manager
pMan = Abc_NtkToDar( pMiter, 1 );
Abc_NtkDelete( pMiter );
@@ -990,7 +1092,7 @@ int Abc_NtkDarSec( Abc_Ntk_t * pNtk1, Abc_Ntk_t * pNtk2, int nFrames, int fVerbo
assert( pMan->nRegs > 0 );
// perform verification
- RetValue = Fra_FraigSec( pMan, nFrames, fVerbose, fVeryVerbose );
+ RetValue = Fra_FraigSec( pMan, nFrames, fRetimeFirst, fVerbose, fVeryVerbose );
Aig_ManStop( pMan );
return RetValue;
}
@@ -1006,15 +1108,19 @@ int Abc_NtkDarSec( Abc_Ntk_t * pNtk1, Abc_Ntk_t * pNtk2, int nFrames, int fVerbo
SeeAlso []
***********************************************************************/
-Abc_Ntk_t * Abc_NtkDarLatchSweep( Abc_Ntk_t * pNtk, int fVerbose )
+Abc_Ntk_t * Abc_NtkDarLatchSweep( Abc_Ntk_t * pNtk, int fLatchSweep, int fVerbose )
{
Abc_Ntk_t * pNtkAig;
Aig_Man_t * pMan;
pMan = Abc_NtkToDar( pNtk, 1 );
if ( pMan == NULL )
return NULL;
- pMan = Aig_ManReduceLaches( pMan, fVerbose );
- pMan = Aig_ManConstReduce( pMan, fVerbose );
+ Aig_ManSeqCleanup( pMan );
+ if ( fLatchSweep )
+ {
+ pMan = Aig_ManReduceLaches( pMan, fVerbose );
+ pMan = Aig_ManConstReduce( pMan, fVerbose );
+ }
pNtkAig = Abc_NtkFromDarSeqSweep( pNtk, pMan );
Aig_ManStop( pMan );
return pNtkAig;
@@ -1038,6 +1144,8 @@ Abc_Ntk_t * Abc_NtkDarRetime( Abc_Ntk_t * pNtk, int nStepsMax, int fVerbose )
pMan = Abc_NtkToDar( pNtk, 1 );
if ( pMan == NULL )
return NULL;
+// Aig_ManReduceLachesCount( pMan );
+
pMan = Rtm_ManRetime( pTemp = pMan, 1, nStepsMax, 0 );
Aig_ManStop( pTemp );
diff --git a/src/base/abci/abcPrint.c b/src/base/abci/abcPrint.c
index 004d1f39..f9b053ba 100644
--- a/src/base/abci/abcPrint.c
+++ b/src/base/abci/abcPrint.c
@@ -213,6 +213,9 @@ void Abc_NtkPrintStats( FILE * pFile, Abc_Ntk_t * pNtk, int fFactored )
printf( "Total nodes = %6d %6.2f Mb Changes = %6d.\n",
s_TotalNodes, s_TotalNodes * 20.0 / (1<<20), s_TotalChanges );
*/
+
+// if ( Abc_NtkHasSop(pNtk) )
+// printf( "The total number of cube pairs = %d.\n", Abc_NtkGetCubePairNum(pNtk) );
}
/**Function*************************************************************
diff --git a/src/base/abci/abcStrash.c b/src/base/abci/abcStrash.c
index 4fdb7cbc..69373597 100644
--- a/src/base/abci/abcStrash.c
+++ b/src/base/abci/abcStrash.c
@@ -233,7 +233,8 @@ int Abc_NtkAppend( Abc_Ntk_t * pNtk1, Abc_Ntk_t * pNtk2, int fAddPos )
// perform strashing
nNewCis = 0;
Abc_NtkCleanCopy( pNtk2 );
- Abc_AigConst1(pNtk2)->pCopy = Abc_AigConst1(pNtk1);
+ if ( Abc_NtkIsStrash(pNtk2) )
+ Abc_AigConst1(pNtk2)->pCopy = Abc_AigConst1(pNtk1);
Abc_NtkForEachCi( pNtk2, pObj, i )
{
pName = Abc_ObjName(pObj);
diff --git a/src/base/abci/abcXsim.c b/src/base/abci/abcXsim.c
index c05823da..5d9e4634 100644
--- a/src/base/abci/abcXsim.c
+++ b/src/base/abci/abcXsim.c
@@ -103,7 +103,7 @@ static inline void Abc_XsimPrint( FILE * pFile, int Value )
SeeAlso []
***********************************************************************/
-void Abc_NtkXValueSimulate( Abc_Ntk_t * pNtk, int nFrames, int fInputs, int fVerbose )
+void Abc_NtkXValueSimulate( Abc_Ntk_t * pNtk, int nFrames, int fXInputs, int fXState, int fVerbose )
{
Abc_Obj_t * pObj;
int i, f;
@@ -111,20 +111,26 @@ void Abc_NtkXValueSimulate( Abc_Ntk_t * pNtk, int nFrames, int fInputs, int fVer
srand( 0x12341234 );
// start simulation
Abc_ObjSetXsim( Abc_AigConst1(pNtk), XVS1 );
- if ( fInputs )
+ if ( fXInputs )
{
Abc_NtkForEachPi( pNtk, pObj, i )
Abc_ObjSetXsim( pObj, XVSX );
- Abc_NtkForEachLatch( pNtk, pObj, i )
- Abc_ObjSetXsim( Abc_ObjFanout0(pObj), Abc_LatchInit(pObj) );
}
else
{
Abc_NtkForEachPi( pNtk, pObj, i )
Abc_ObjSetXsim( pObj, Abc_XsimRand2() );
+ }
+ if ( fXState )
+ {
Abc_NtkForEachLatch( pNtk, pObj, i )
Abc_ObjSetXsim( Abc_ObjFanout0(pObj), XVSX );
}
+ else
+ {
+ Abc_NtkForEachLatch( pNtk, pObj, i )
+ Abc_ObjSetXsim( Abc_ObjFanout0(pObj), Abc_LatchInit(pObj) );
+ }
// simulate and print the result
fprintf( stdout, "Frame : Inputs : Latches : Outputs\n" );
for ( f = 0; f < nFrames; f++ )
@@ -147,14 +153,24 @@ void Abc_NtkXValueSimulate( Abc_Ntk_t * pNtk, int nFrames, int fInputs, int fVer
fprintf( stdout, " : " );
Abc_NtkForEachPo( pNtk, pObj, i )
Abc_XsimPrint( stdout, Abc_ObjGetXsim(pObj) );
+ if ( Abc_NtkAssertNum(pNtk) )
+ {
+ fprintf( stdout, " : " );
+ Abc_NtkForEachAssert( pNtk, pObj, i )
+ Abc_XsimPrint( stdout, Abc_ObjGetXsim(pObj) );
+ }
fprintf( stdout, "\n" );
// assign input values
- if ( fInputs )
+ if ( fXInputs )
+ {
Abc_NtkForEachPi( pNtk, pObj, i )
Abc_ObjSetXsim( pObj, XVSX );
+ }
else
+ {
Abc_NtkForEachPi( pNtk, pObj, i )
Abc_ObjSetXsim( pObj, Abc_XsimRand2() );
+ }
// transfer the latch values
Abc_NtkForEachLatch( pNtk, pObj, i )
Abc_ObjSetXsim( Abc_ObjFanout0(pObj), Abc_ObjGetXsim(Abc_ObjFanin0(pObj)) );
diff --git a/src/opt/fxu/fxu.c b/src/opt/fxu/fxu.c
index a92ef934..d11fd793 100644
--- a/src/opt/fxu/fxu.c
+++ b/src/opt/fxu/fxu.c
@@ -58,6 +58,7 @@ int Fxu_FastExtract( Fxu_Data_t * pData )
Fxu_Single * pSingle;
Fxu_Double * pDouble;
int Weight1, Weight2, Weight3;
+ int Counter = 0;
s_MemoryTotal = 0;
s_MemoryPeak = 0;
@@ -77,7 +78,7 @@ int Fxu_FastExtract( Fxu_Data_t * pData )
{
Weight1 = Fxu_HeapSingleReadMaxWeight( p->pHeapSingle );
if ( pData->fVerbose )
- printf( "Best single = %3d.\n", Weight1 );
+ printf( "Div %5d : Best single = %5d.\r", Counter++, Weight1 );
if ( Weight1 > 0 || Weight1 == 0 && pData->fUse0 )
Fxu_UpdateSingle( p );
else
@@ -92,7 +93,7 @@ int Fxu_FastExtract( Fxu_Data_t * pData )
{
Weight2 = Fxu_HeapDoubleReadMaxWeight( p->pHeapDouble );
if ( pData->fVerbose )
- printf( "Best double = %3d.\n", Weight2 );
+ printf( "Div %5d : Best double = %5d.\r", Counter++, Weight2 );
if ( Weight2 > 0 || Weight2 == 0 && pData->fUse0 )
Fxu_UpdateDouble( p );
else
@@ -109,7 +110,7 @@ int Fxu_FastExtract( Fxu_Data_t * pData )
Weight2 = Fxu_HeapDoubleReadMaxWeight( p->pHeapDouble );
if ( pData->fVerbose )
- printf( "Best double = %3d. Best single = %3d.\n", Weight2, Weight1 );
+ printf( "Div %5d : Best double = %5d. Best single = %5d.\r", Counter++, Weight2, Weight1 );
//Fxu_Select( p, &pSingle, &pDouble );
if ( Weight1 >= Weight2 )
@@ -140,8 +141,8 @@ int Fxu_FastExtract( Fxu_Data_t * pData )
// select the best single and double
Weight3 = Fxu_Select( p, &pSingle, &pDouble );
if ( pData->fVerbose )
- printf( "Best double = %3d. Best single = %3d. Best complement = %3d.\n",
- Weight2, Weight1, Weight3 );
+ printf( "Div %5d : Best double = %5d. Best single = %5d. Best complement = %5d.\r",
+ Counter++, Weight2, Weight1, Weight3 );
if ( Weight3 > 0 || Weight3 == 0 && pData->fUse0 )
Fxu_Update( p, pSingle, pDouble );
@@ -152,7 +153,8 @@ int Fxu_FastExtract( Fxu_Data_t * pData )
}
if ( pData->fVerbose )
- printf( "Total single = %3d. Total double = %3d. Total compl = %3d.\n", p->nDivs1, p->nDivs2, p->nDivs3 );
+ printf( "Total single = %3d. Total double = %3d. Total compl = %3d. \n",
+ p->nDivs1, p->nDivs2, p->nDivs3 );
// create the new covers
if ( pData->nNodesNew )
diff --git a/src/opt/fxu/fxu.h b/src/opt/fxu/fxu.h
index 7025d019..e6d0b69e 100644
--- a/src/opt/fxu/fxu.h
+++ b/src/opt/fxu/fxu.h
@@ -55,7 +55,8 @@ struct FxuDataStruct
bool fUseCompl; // set to 1 to have complement taken into account
bool fVerbose; // set to 1 to have verbose output
int nNodesExt; // the number of divisors to extract
- int nPairsMax; // the maximum number of cube pairs to consider
+ int nSingleMax; // the max number of single-cube divisors to consider
+ int nPairsMax; // the max number of double-cube divisors to consider
// the input information
Vec_Ptr_t * vSops; // the SOPs for each node in the network
Vec_Ptr_t * vFanins; // the fanins of each node in the network
diff --git a/src/opt/fxu/fxuCreate.c b/src/opt/fxu/fxuCreate.c
index 99942a88..e3300df9 100644
--- a/src/opt/fxu/fxuCreate.c
+++ b/src/opt/fxu/fxuCreate.c
@@ -178,12 +178,26 @@ Fxu_Matrix * Fxu_CreateMatrix( Fxu_Data_t * pData )
// consider the case when cube pairs should be preprocessed
// before adding them to the set of divisors
+// if ( pData->fVerbose )
+// printf( "The total number of cube pairs is %d.\n", nPairsTotal );
+ if ( nPairsTotal > 10000000 )
+ {
+ printf( "The total number of cube pairs of the network is more than 10,000,000.\n" );
+ printf( "Command \"fx\" takes a long time to run in such cases. It is suggested\n" );
+ printf( "that the user changes the network by reducing the size of logic node and\n" );
+ printf( "consequently the number of cube pairs to be processed by this command.\n" );
+ printf( "One way to achieve this is to run the commands \"st; multi -m -F <num>\"\n" );
+ printf( "as a proprocessing step, while selecting <num> as approapriate.\n" );
+ return NULL;
+ }
if ( nPairsTotal > pData->nPairsMax )
if ( !Fxu_PreprocessCubePairs( p, pData->vSops, nPairsTotal, pData->nPairsMax ) )
return NULL;
+// if ( pData->fVerbose )
+// printf( "Only %d best cube pairs will be used by the fast extract command.\n", pData->nPairsMax );
// add the var pairs to the heap
- Fxu_MatrixComputeSingles( p );
+ Fxu_MatrixComputeSingles( p, pData->fUse0, pData->nSingleMax );
// print stats
if ( pData->fVerbose )
@@ -194,9 +208,8 @@ Fxu_Matrix * Fxu_CreateMatrix( Fxu_Data_t * pData )
p->lVars.nItems, p->lCubes.nItems );
fprintf( stdout, "Lits = %d Density = %.5f%%\n",
p->nEntries, Density );
- fprintf( stdout, "1-cube divisors = %6d. ", p->lSingles.nItems );
- fprintf( stdout, "2-cube divisors = %6d. ", p->nDivsTotal );
- fprintf( stdout, "Cube pairs = %6d.", nPairsTotal );
+ fprintf( stdout, "1-cube divs = %6d. (Total = %6d) ", p->lSingles.nItems, p->nSingleTotal );
+ fprintf( stdout, "2-cube divs = %6d. (Total = %6d)", p->nDivsTotal, nPairsTotal );
fprintf( stdout, "\n" );
}
// Fxu_MatrixPrint( stdout, p );
diff --git a/src/opt/fxu/fxuInt.h b/src/opt/fxu/fxuInt.h
index 0ae1d79e..ea85cb79 100644
--- a/src/opt/fxu/fxuInt.h
+++ b/src/opt/fxu/fxuInt.h
@@ -172,6 +172,8 @@ struct FxuMatrix // ~ 30 words
// the single cube divisors
Fxu_ListSingle lSingles; // the linked list of single cube divisors
Fxu_HeapSingle * pHeapSingle; // the heap of variables by the number of literals in the matrix
+ int nWeightLimit;// the limit on weight of single cube divisors collected
+ int nSingleTotal;// the total number of single cube divisors
// storage for cube pairs
Fxu_Pair *** pppPairs;
Fxu_Pair ** ppPairs;
@@ -459,7 +461,7 @@ extern void Fxu_PairClearStorage( Fxu_Cube * pCube );
extern Fxu_Pair * Fxu_PairAlloc( Fxu_Matrix * p, Fxu_Cube * pCube1, Fxu_Cube * pCube2 );
extern void Fxu_PairAdd( Fxu_Pair * pPair );
/*===== fxuSingle.c ====================================================*/
-extern void Fxu_MatrixComputeSingles( Fxu_Matrix * p );
+extern void Fxu_MatrixComputeSingles( Fxu_Matrix * p, int fUse0, int nSingleMax );
extern void Fxu_MatrixComputeSinglesOne( Fxu_Matrix * p, Fxu_Var * pVar );
extern int Fxu_SingleCountCoincidence( Fxu_Matrix * p, Fxu_Var * pVar1, Fxu_Var * pVar2 );
/*===== fxuMatrix.c ====================================================*/
diff --git a/src/opt/fxu/fxuSingle.c b/src/opt/fxu/fxuSingle.c
index be90e159..73d9a76c 100644
--- a/src/opt/fxu/fxuSingle.c
+++ b/src/opt/fxu/fxuSingle.c
@@ -17,11 +17,14 @@
***********************************************************************/
#include "fxuInt.h"
+#include "vec.h"
////////////////////////////////////////////////////////////////////////
/// DECLARATIONS ///
////////////////////////////////////////////////////////////////////////
+static void Fxu_MatrixComputeSinglesOneCollect( Fxu_Matrix * p, Fxu_Var * pVar, Vec_Ptr_t * vSingles );
+
////////////////////////////////////////////////////////////////////////
/// FUNCTION DEFINITIONS ///
////////////////////////////////////////////////////////////////////////
@@ -38,12 +41,130 @@
SeeAlso []
***********************************************************************/
-void Fxu_MatrixComputeSingles( Fxu_Matrix * p )
+void Fxu_MatrixComputeSingles( Fxu_Matrix * p, int fUse0, int nSingleMax )
{
Fxu_Var * pVar;
- // iterate through the columns in the matrix
+ Vec_Ptr_t * vSingles;
+ int i, k;
+ // set the weight limit
+ p->nWeightLimit = 1 - fUse0;
+ // iterate through columns in the matrix and collect single-cube divisors
+ vSingles = Vec_PtrAlloc( 10000 );
Fxu_MatrixForEachVariable( p, pVar )
- Fxu_MatrixComputeSinglesOne( p, pVar );
+ Fxu_MatrixComputeSinglesOneCollect( p, pVar, vSingles );
+ p->nSingleTotal = Vec_PtrSize(vSingles) / 3;
+ // check if divisors should be filtered
+ if ( Vec_PtrSize(vSingles) > nSingleMax )
+ {
+ int * pWeigtCounts, nDivCount, Weight, i, c;;
+ assert( Vec_PtrSize(vSingles) % 3 == 0 );
+ // count how many divisors have the given weight
+ pWeigtCounts = ALLOC( int, 1000 );
+ memset( pWeigtCounts, 0, sizeof(int) * 1000 );
+ for ( i = 2; i < Vec_PtrSize(vSingles); i += 3 )
+ {
+ Weight = (int)Vec_PtrEntry(vSingles, i);
+ if ( Weight >= 999 )
+ pWeigtCounts[999]++;
+ else
+ pWeigtCounts[Weight]++;
+ }
+ // select the bound on the weight (above this bound, singles will be included)
+ nDivCount = 0;
+ for ( c = 999; c >= 0; c-- )
+ {
+ nDivCount += pWeigtCounts[c];
+ if ( nDivCount >= nSingleMax )
+ break;
+ }
+ free( pWeigtCounts );
+ // collect singles with the given costs
+ k = 0;
+ for ( i = 2; i < Vec_PtrSize(vSingles); i += 3 )
+ {
+ Weight = (int)Vec_PtrEntry(vSingles, i);
+ if ( Weight < c )
+ continue;
+ Vec_PtrWriteEntry( vSingles, k++, Vec_PtrEntry(vSingles, i-2) );
+ Vec_PtrWriteEntry( vSingles, k++, Vec_PtrEntry(vSingles, i-1) );
+ Vec_PtrWriteEntry( vSingles, k++, Vec_PtrEntry(vSingles, i) );
+ if ( k/3 == nSingleMax )
+ break;
+ }
+ Vec_PtrShrink( vSingles, k );
+ // adjust the weight limit
+ p->nWeightLimit = c;
+ }
+ // collect the selected divisors
+ assert( Vec_PtrSize(vSingles) % 3 == 0 );
+ for ( i = 0; i < Vec_PtrSize(vSingles); i += 3 )
+ {
+ Fxu_MatrixAddSingle( p,
+ Vec_PtrEntry(vSingles,i),
+ Vec_PtrEntry(vSingles,i+1),
+ (int)Vec_PtrEntry(vSingles,i+2) );
+ }
+ Vec_PtrFree( vSingles );
+}
+
+/**Function*************************************************************
+
+ Synopsis [Adds the single-cube divisors associated with a new column.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+void Fxu_MatrixComputeSinglesOneCollect( Fxu_Matrix * p, Fxu_Var * pVar, Vec_Ptr_t * vSingles )
+{
+ Fxu_Lit * pLitV, * pLitH;
+ Fxu_Var * pVar2;
+ int Coin;
+ int WeightCur;
+
+ // start collecting the affected vars
+ Fxu_MatrixRingVarsStart( p );
+ // go through all the literals of this variable
+ for ( pLitV = pVar->lLits.pHead; pLitV; pLitV = pLitV->pVNext )
+ // for this literal, go through all the horizontal literals
+ for ( pLitH = pLitV->pHPrev; pLitH; pLitH = pLitH->pHPrev )
+ {
+ // get another variable
+ pVar2 = pLitH->pVar;
+ // skip the var if it is already used
+ if ( pVar2->pOrder )
+ continue;
+ // skip the var if it belongs to the same node
+// if ( pValue2Node[pVar->iVar] == pValue2Node[pVar2->iVar] )
+// continue;
+ // collect the var
+ Fxu_MatrixRingVarsAdd( p, pVar2 );
+ }
+ // stop collecting the selected vars
+ Fxu_MatrixRingVarsStop( p );
+
+ // iterate through the selected vars
+ Fxu_MatrixForEachVarInRing( p, pVar2 )
+ {
+ // count the coincidence
+ Coin = Fxu_SingleCountCoincidence( p, pVar2, pVar );
+ assert( Coin > 0 );
+ // get the new weight
+ WeightCur = Coin - 2;
+ // peformance fix (August 24, 2007)
+ if ( WeightCur >= p->nWeightLimit )
+ {
+ Vec_PtrPush( vSingles, pVar2 );
+ Vec_PtrPush( vSingles, pVar );
+ Vec_PtrPush( vSingles, (void *)WeightCur );
+ }
+ }
+
+ // unmark the vars
+ Fxu_MatrixRingVarsUnmark( p );
}
/**Function*************************************************************
@@ -59,12 +180,9 @@ void Fxu_MatrixComputeSingles( Fxu_Matrix * p )
***********************************************************************/
void Fxu_MatrixComputeSinglesOne( Fxu_Matrix * p, Fxu_Var * pVar )
{
-// int * pValue2Node = p->pValue2Node;
Fxu_Lit * pLitV, * pLitH;
Fxu_Var * pVar2;
int Coin;
-// int CounterAll;
-// int CounterTest;
int WeightCur;
// start collecting the affected vars
@@ -76,7 +194,6 @@ void Fxu_MatrixComputeSinglesOne( Fxu_Matrix * p, Fxu_Var * pVar )
{
// get another variable
pVar2 = pLitH->pVar;
-// CounterAll++;
// skip the var if it is already used
if ( pVar2->pOrder )
continue;
@@ -92,16 +209,17 @@ void Fxu_MatrixComputeSinglesOne( Fxu_Matrix * p, Fxu_Var * pVar )
// iterate through the selected vars
Fxu_MatrixForEachVarInRing( p, pVar2 )
{
-// CounterTest++;
// count the coincidence
Coin = Fxu_SingleCountCoincidence( p, pVar2, pVar );
assert( Coin > 0 );
// get the new weight
WeightCur = Coin - 2;
- if ( WeightCur >= 0 )
+ // peformance fix (August 24, 2007)
+// if ( WeightCur >= 0 )
+// Fxu_MatrixAddSingle( p, pVar2, pVar, WeightCur );
+ if ( WeightCur >= p->nWeightLimit )
Fxu_MatrixAddSingle( p, pVar2, pVar, WeightCur );
}
-
// unmark the vars
Fxu_MatrixRingVarsUnmark( p );
}
diff --git a/src/opt/fxu/fxuUpdate.c b/src/opt/fxu/fxuUpdate.c
index a430b9c1..274f79f6 100644
--- a/src/opt/fxu/fxuUpdate.c
+++ b/src/opt/fxu/fxuUpdate.c
@@ -757,12 +757,14 @@ void Fxu_UpdateCleanOldSingles( Fxu_Matrix * p )
{
Fxu_Single * pSingle, * pSingle2;
int WeightNew;
+ int Counter = 0;
Fxu_MatrixForEachSingleSafe( p, pSingle, pSingle2 )
{
// if at least one of the variables is marked, recalculate
if ( pSingle->pVar1->pOrder || pSingle->pVar2->pOrder )
{
+ Counter++;
// get the new weight
WeightNew = -2 + Fxu_SingleCountCoincidence( p, pSingle->pVar1, pSingle->pVar2 );
if ( WeightNew >= 0 )
@@ -778,6 +780,7 @@ void Fxu_UpdateCleanOldSingles( Fxu_Matrix * p )
}
}
}
+// printf( "Called procedure %d times.\n", Counter );
}
/**Function*************************************************************