summaryrefslogtreecommitdiffstats
diff options
context:
space:
mode:
Diffstat
-rw-r--r--abc.dsp16
-rw-r--r--abc.rc22
-rw-r--r--src/aig/aig/aigMan.c4
-rw-r--r--src/aig/aig/aigScl.c22
-rw-r--r--src/aig/aig/aigTsim.c6
-rw-r--r--src/aig/mfx/mfxCore.c2
-rw-r--r--src/aig/saig/module.make4
-rw-r--r--src/aig/saig/saig.h15
-rw-r--r--src/aig/saig/saigRetFwd.c242
-rw-r--r--src/aig/saig/saigRetMin.c10
-rw-r--r--src/aig/saig/saigScl.c74
-rw-r--r--src/base/abci/abc.c145
-rw-r--r--src/base/abci/abcDar.c57
-rw-r--r--src/base/abci/abcFpga.c8
-rw-r--r--src/base/abci/abcIf.c8
-rw-r--r--src/base/abci/abcReach.c313
-rw-r--r--src/base/abci/module.make1
-rw-r--r--src/bdd/cas/casCore.c2
-rw-r--r--src/bdd/cas/casDec.c2
-rw-r--r--src/map/pcm/module.make0
-rw-r--r--src/map/ply/module.make0
-rw-r--r--src/misc/extra/extra.h25
-rw-r--r--src/misc/extra/extraBddImage.c1157
-rw-r--r--src/misc/extra/extraBddMisc.c28
-rw-r--r--src/misc/extra/module.make1
-rw-r--r--src/opt/mfs/mfsCore.c26
26 files changed, 2111 insertions, 79 deletions
diff --git a/abc.dsp b/abc.dsp
index f6685065..60fe207b 100644
--- a/abc.dsp
+++ b/abc.dsp
@@ -342,6 +342,10 @@ SOURCE=.\src\base\abci\abcQuant.c
# End Source File
# Begin Source File
+SOURCE=.\src\base\abci\abcReach.c
+# End Source File
+# Begin Source File
+
SOURCE=.\src\base\abci\abcRec.c
# End Source File
# Begin Source File
@@ -2034,6 +2038,10 @@ SOURCE=.\src\misc\extra\extraBddCas.c
# End Source File
# Begin Source File
+SOURCE=.\src\misc\extra\extraBddImage.c
+# End Source File
+# Begin Source File
+
SOURCE=.\src\misc\extra\extraBddKmap.c
# End Source File
# Begin Source File
@@ -3250,8 +3258,16 @@ SOURCE=.\src\aig\saig\saigPhase.c
# End Source File
# Begin Source File
+SOURCE=.\src\aig\saig\saigRetFwd.c
+# End Source File
+# Begin Source File
+
SOURCE=.\src\aig\saig\saigRetMin.c
# End Source File
+# Begin Source File
+
+SOURCE=.\src\aig\saig\saigScl.c
+# End Source File
# End Group
# End Group
# End Group
diff --git a/abc.rc b/abc.rc
index 5f7d5904..aff51d6d 100644
--- a/abc.rc
+++ b/abc.rc
@@ -120,17 +120,17 @@ alias resyn2rsdc "b; rs -K 6 -F 2; rw; rs -K 6 -N 2 -F 2; rf; rs -K 8 -F 2; b
alias compress2rsdc "b -l; rs -K 6 -F 2 -l; rw -l; rs -K 6 -N 2 -F 2 -l; rf -l; rs -K 8 -F 2 -l; b -l; rs -K 8 -N 2 -F 2 -l; rw -l; rs -K 10 -F 2 -l; rwz -l; rs -K 10 -N 2 -F 2 -l; b -l; rs -K 12 -F 2 -l; rfz -l; rs -K 12 -N 2 -F 2 -l; rwz -l; b -l"
# temporaries
-alias reach "st; ps; compress2; ps; qrel; ps; compress2; ps; qreach -v; ps"
-alias chnew "st; haig_start; resyn2; haig_use"
-alias chnewrs "st; haig_start; resyn2rs; haig_use"
-alias stdsd "r test/6in.blif; st; ps; u; bdd; dsd -g; st; ps"
-alias trec "rec_start; r c.blif; st; rec_add; rec_use"
-alias trec4 "rec_start -K 4; r i10.blif; st; rec_add; rec_use"
-alias bmc2 "frames -i -F 10; orpos; iprove"
+alias reachable "st; ps; compress2; ps; qrel; ps; compress2; ps; qreach -v; ps"
+alias chnew "st; haig_start; resyn2; haig_use"
+alias chnewrs "st; haig_start; resyn2rs; haig_use"
+alias stdsd "r test/6in.blif; st; ps; u; bdd; dsd -g; st; ps"
+alias trec "rec_start; r c.blif; st; rec_add; rec_use"
+alias trec4 "rec_start -K 4; r i10.blif; st; rec_add; rec_use"
+alias bmc2 "frames -i -F 10; orpos; iprove"
-alias pjsolve "scl; dc2; fr; dc2; ic; ic -t; if -a; cs tacas/005_care.aig; mfs; lp; st; ic"
+alias pjsolve "scl; dc2; fr; dc2; ic; ic -t; if -a; cs tacas/005_care.aig; mfs; lp; st; ic"
-alias t0 "r test/mc1.blif; st; test"
-alias t1 "r s27mc2.blif; st; test"
-alias t2 "r i/intel_001.aig; ps; indcut -v"
+alias t0 "r test/mc1.blif; st; test"
+alias t1 "r s27mc2.blif; st; test"
+alias t2 "r i/intel_001.aig; ps; indcut -v"
diff --git a/src/aig/aig/aigMan.c b/src/aig/aig/aigMan.c
index 41a62484..47ee8d4d 100644
--- a/src/aig/aig/aigMan.c
+++ b/src/aig/aig/aigMan.c
@@ -350,10 +350,10 @@ void Aig_ManPrintStats( Aig_Man_t * p )
***********************************************************************/
void Aig_ManReportImprovement( Aig_Man_t * p, Aig_Man_t * pNew )
{
- printf( "REGs: Beg = %d. End = %d. (R = %6.2f %%). ",
+ printf( "REG: Beg = %5d. End = %5d. (R =%5.1f %%) ",
Aig_ManRegNum(p), Aig_ManRegNum(pNew),
Aig_ManRegNum(p)? 100.0*(Aig_ManRegNum(p)-Aig_ManRegNum(pNew))/Aig_ManRegNum(p) : 0.0 );
- printf( "ANDs: Beg = %d. End = %d. (R = %6.2f %%).",
+ printf( "AND: Beg = %6d. End = %6d. (R =%5.1f %%)",
Aig_ManNodeNum(p), Aig_ManNodeNum(pNew),
Aig_ManNodeNum(p)? 100.0*(Aig_ManNodeNum(p)-Aig_ManNodeNum(pNew))/Aig_ManNodeNum(p) : 0.0 );
printf( "\n" );
diff --git a/src/aig/aig/aigScl.c b/src/aig/aig/aigScl.c
index 00a8159e..c2d08350 100644
--- a/src/aig/aig/aigScl.c
+++ b/src/aig/aig/aigScl.c
@@ -451,27 +451,17 @@ Aig_Man_t * Aig_ManReduceLaches( Aig_Man_t * p, int fVerbose )
Aig_Man_t * pTemp;
Vec_Ptr_t * vMap;
int nSaved, nCur;
+ if ( fVerbose )
+ printf( "Performing combinational register sweep:\n" );
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 );
-//Aig_ManPrintStats( p );
p = Aig_ManRemap( pTemp = p, vMap );
-//Aig_ManPrintStats( p );
- Aig_ManStop( pTemp );
Vec_PtrFree( vMap );
Aig_ManSeqCleanup( p );
-//Aig_ManPrintStats( p );
-//printf( "\n" );
if ( fVerbose )
- {
- printf( "REnd = %5d. NEnd = %6d. ", Aig_ManRegNum(p), Aig_ManNodeNum(p) );
- printf( "\n" );
- }
+ Aig_ManReportImprovement( pTemp, p );
+ Aig_ManStop( pTemp );
if ( p->nRegs == 0 )
break;
}
@@ -600,6 +590,8 @@ void Aig_ManComputeSccs( Aig_Man_t * p )
***********************************************************************/
Aig_Man_t * Aig_ManScl( Aig_Man_t * pAig, int fLatchConst, int fLatchEqual, int fVerbose )
{
+ extern void Saig_ManReportUselessRegisters( Aig_Man_t * pAig );
+
Aig_Man_t * pAigInit, * pAigNew;
Aig_Obj_t * pFlop1, * pFlop2;
int i, Entry1, Entry2, nTruePis;
@@ -633,6 +625,8 @@ Aig_Man_t * Aig_ManScl( Aig_Man_t * pAig, int fLatchConst, int fLatchEqual, int
// Aig_ManSeqCleanup( pAigInit );
pAigNew = Aig_ManDupRepr( pAigInit, 0 );
Aig_ManSeqCleanup( pAigNew );
+
+ Saig_ManReportUselessRegisters( pAigNew );
return pAigNew;
}
diff --git a/src/aig/aig/aigTsim.c b/src/aig/aig/aigTsim.c
index 1d974778..d3f78902 100644
--- a/src/aig/aig/aigTsim.c
+++ b/src/aig/aig/aigTsim.c
@@ -479,14 +479,12 @@ Aig_Man_t * Aig_ManConstReduce( Aig_Man_t * p, int fVerbose )
Vec_Ptr_t * vMap;
while ( (vMap = Aig_ManTernarySimulate( p, fVerbose )) )
{
- if ( fVerbose )
- printf( "RBeg = %5d. NBeg = %6d. ", Aig_ManRegNum(p), Aig_ManNodeNum(p) );
p = Aig_ManRemap( pTemp = p, vMap );
- Aig_ManStop( pTemp );
Vec_PtrFree( vMap );
Aig_ManSeqCleanup( p );
if ( fVerbose )
- printf( "REnd = %5d. NEnd = %6d. \n", Aig_ManRegNum(p), Aig_ManNodeNum(p) );
+ Aig_ManReportImprovement( pTemp, p );
+ Aig_ManStop( pTemp );
}
return p;
}
diff --git a/src/aig/mfx/mfxCore.c b/src/aig/mfx/mfxCore.c
index 8867f7c1..48107e7e 100644
--- a/src/aig/mfx/mfxCore.c
+++ b/src/aig/mfx/mfxCore.c
@@ -245,7 +245,7 @@ int Mfx_Perform( Nwk_Man_t * pNtk, Mfx_Par_t * pPars, If_Lib_t * pLutLib )
p->nFaninMax = nFaninMax;
if ( !pPars->fResub )
{
- pDecPars->nVarsMax = nFaninMax;
+ pDecPars->nVarsMax = (nFaninMax < 3) ? 3 : nFaninMax;
pDecPars->fVerbose = pPars->fVerbose;
p->vTruth = Vec_IntAlloc( 0 );
p->pManDec = Bdc_ManAlloc( pDecPars );
diff --git a/src/aig/saig/module.make b/src/aig/saig/module.make
index 3902ce70..7de3ccdc 100644
--- a/src/aig/saig/module.make
+++ b/src/aig/saig/module.make
@@ -1,3 +1,5 @@
SRC += src/aig/saig/saig_.c \
src/aig/saig/saigPhase.c \
- src/aig/saig/saigRetMin.c
+ src/aig/saig/saigRetFwd.c \
+ src/aig/saig/saigRetMin.c \
+ src/aig/saig/saigScl.c
diff --git a/src/aig/saig/saig.h b/src/aig/saig/saig.h
index ce09fd32..e399b8bb 100644
--- a/src/aig/saig/saig.h
+++ b/src/aig/saig/saig.h
@@ -49,6 +49,11 @@ static inline int Saig_ManRegNum( Aig_Man_t * p ) { return p->n
static inline Aig_Obj_t * Saig_ManLo( Aig_Man_t * p, int i ) { return (Aig_Obj_t *)Vec_PtrEntry(p->vPis, Saig_ManPiNum(p)+i); }
static inline Aig_Obj_t * Saig_ManLi( Aig_Man_t * p, int i ) { return (Aig_Obj_t *)Vec_PtrEntry(p->vPos, Saig_ManPoNum(p)+i); }
+static inline int Saig_ObjIsPi( Aig_Man_t * p, Aig_Obj_t * pObj ) { return Aig_ObjIsPi(pObj) && Aig_ObjPioNum(pObj) < Saig_ManPiNum(p); }
+static inline int Saig_ObjIsPo( Aig_Man_t * p, Aig_Obj_t * pObj ) { return Aig_ObjIsPo(pObj) && Aig_ObjPioNum(pObj) < Saig_ManPoNum(p); }
+static inline int Saig_ObjIsLo( Aig_Man_t * p, Aig_Obj_t * pObj ) { return Aig_ObjIsPi(pObj) && Aig_ObjPioNum(pObj) >= Saig_ManPiNum(p); }
+static inline int Saig_ObjIsLi( Aig_Man_t * p, Aig_Obj_t * pObj ) { return Aig_ObjIsPo(pObj) && Aig_ObjPioNum(pObj) >= Saig_ManPoNum(p); }
+
// iterator over the primary inputs/outputs
#define Saig_ManForEachPi( p, pObj, i ) \
Vec_PtrForEachEntryStop( p->vPis, pObj, i, Saig_ManPiNum(p) )
@@ -69,7 +74,15 @@ static inline Aig_Obj_t * Saig_ManLi( Aig_Man_t * p, int i ) { return (Aig
////////////////////////////////////////////////////////////////////////
/*=== saigPhase.c ==========================================================*/
-
+extern Aig_Man_t * Saig_ManPhaseAbstract( Aig_Man_t * p, Vec_Int_t * vInits, int nFrames, int fIgnore, int fPrint, int fVerbose );
+/*=== saigRetFwd.c ==========================================================*/
+extern Aig_Man_t * Saig_ManRetimeForward( Aig_Man_t * p, int nMaxIters, int fVerbose );
+/*=== saigRetMin.c ==========================================================*/
+extern Aig_Man_t * Saig_ManRetimeDupForward( Aig_Man_t * p, Vec_Ptr_t * vCut );
+extern Aig_Man_t * Saig_ManRetimeMinArea( Aig_Man_t * p, int nMaxIters, int fForwardOnly, int fBackwardOnly, int fInitial, int fVerbose );
+/*=== saigScl.c ==========================================================*/
+extern void Saig_ManReportUselessRegisters( Aig_Man_t * pAig );
+
#ifdef __cplusplus
}
#endif
diff --git a/src/aig/saig/saigRetFwd.c b/src/aig/saig/saigRetFwd.c
new file mode 100644
index 00000000..b6321da6
--- /dev/null
+++ b/src/aig/saig/saigRetFwd.c
@@ -0,0 +1,242 @@
+/**CFile****************************************************************
+
+ FileName [saigRetFwd.c]
+
+ SystemName [ABC: Logic synthesis and verification system.]
+
+ PackageName [Sequential AIG package.]
+
+ Synopsis [Most-forward retiming.]
+
+ Author [Alan Mishchenko]
+
+ Affiliation [UC Berkeley]
+
+ Date [Ver. 1.0. Started - June 20, 2005.]
+
+ Revision [$Id: saigRetFwd.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
+
+***********************************************************************/
+
+#include "saig.h"
+
+////////////////////////////////////////////////////////////////////////
+/// DECLARATIONS ///
+////////////////////////////////////////////////////////////////////////
+
+static inline Aig_Obj_t * Aig_ObjFanoutStatic( Aig_Obj_t * pObj, int i ) { return ((Aig_Obj_t **)pObj->pData)[i]; }
+static inline void Aig_ObjSetFanoutStatic( Aig_Obj_t * pObj, Aig_Obj_t * pFan ) { ((Aig_Obj_t **)pObj->pData)[pObj->nRefs++] = pFan; }
+
+#define Aig_ObjForEachFanoutStatic( pObj, pFan, i ) \
+ for ( i = 0; (i < (int)(pObj)->nRefs) && ((pFan) = Aig_ObjFanoutStatic(pObj, i)); i++ )
+
+////////////////////////////////////////////////////////////////////////
+/// FUNCTION DEFINITIONS ///
+////////////////////////////////////////////////////////////////////////
+
+/**Function*************************************************************
+
+ Synopsis [Allocate static fanout for all nodes in the AIG manager.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+Aig_Obj_t ** Aig_ManStaticFanoutStart( Aig_Man_t * p )
+{
+ Aig_Obj_t ** ppFanouts, * pObj;
+ int i, nFanouts, nFanoutsAlloc;
+ // allocate fanouts
+ nFanoutsAlloc = 2 * Aig_ManObjNumMax(p) - Aig_ManPiNum(p) - Aig_ManPoNum(p);
+ ppFanouts = ALLOC( Aig_Obj_t *, nFanoutsAlloc );
+ // mark up storage
+ nFanouts = 0;
+ Aig_ManForEachObj( p, pObj, i )
+ {
+ pObj->pData = ppFanouts + nFanouts;
+ nFanouts += pObj->nRefs;
+ pObj->nRefs = 0;
+ }
+ assert( nFanouts < nFanoutsAlloc );
+ // add fanouts
+ Aig_ManForEachObj( p, pObj, i )
+ {
+ if ( Aig_ObjChild0(pObj) )
+ Aig_ObjSetFanoutStatic( Aig_ObjFanin0(pObj), pObj );
+ if ( Aig_ObjChild1(pObj) )
+ Aig_ObjSetFanoutStatic( Aig_ObjFanin1(pObj), pObj );
+ }
+ return ppFanouts;
+}
+
+/**Function*************************************************************
+
+ Synopsis [Marks the objects reachable from the given object.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+void Aig_ManMarkAutonomous_rec( Aig_Man_t * p, Aig_Obj_t * pObj )
+{
+ Aig_Obj_t * pFanout;
+ int i;
+ if ( Aig_ObjIsTravIdCurrent(p, pObj) )
+ return;
+ Aig_ObjSetTravIdCurrent(p, pObj);
+ Aig_ObjForEachFanoutStatic( pObj, pFanout, i )
+ Aig_ManMarkAutonomous_rec( p, pFanout );
+}
+
+/**Function*************************************************************
+
+ Synopsis [Marks with current trav ID nodes reachable from Const1 and PIs.]
+
+ Description [Returns the number of unreachable registers.]
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+void Saig_ManMarkAutonomous( Aig_Man_t * p )
+{
+ Aig_Obj_t ** ppFanouts;
+ Aig_Obj_t * pObj, * pObjLi, * pObjLo;
+ int i;
+ // temporarily connect register outputs to register inputs
+ Saig_ManForEachLiLo( p, pObjLi, pObjLo, i )
+ {
+ pObjLo->pFanin0 = pObjLi;
+ pObjLi->nRefs = 1;
+ }
+ // mark nodes reachable from Const1 and PIs
+ Aig_ManIncrementTravId( p );
+ ppFanouts = Aig_ManStaticFanoutStart( p );
+ Aig_ManMarkAutonomous_rec( p, Aig_ManConst1(p) );
+ Saig_ManForEachPi( p, pObj, i )
+ Aig_ManMarkAutonomous_rec( p, pObj );
+ free( ppFanouts );
+ // disconnect LIs/LOs and label unreachable registers
+ Saig_ManForEachLiLo( p, pObjLi, pObjLo, i )
+ {
+ assert( pObjLo->pFanin0 && pObjLi->nRefs == 1 );
+ pObjLo->pFanin0 = NULL;
+ pObjLi->nRefs = 0;
+ }
+}
+
+/**Function*************************************************************
+
+ Synopsis [Derives the cut for forward retiming.]
+
+ Description [Assumes topological ordering of the nodes.]
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+Aig_Man_t * Saig_ManRetimeForwardOne( Aig_Man_t * p, int * pnRegFixed, int * pnRegMoves )
+{
+ Aig_Man_t * pNew;
+ Vec_Ptr_t * vCut;
+ Aig_Obj_t * pObj, * pFanin;
+ int i;
+ // mark the retimable nodes
+ Saig_ManMarkAutonomous( p );
+ // mark the retimable registers with the fresh trav ID
+ Aig_ManIncrementTravId( p );
+ *pnRegFixed = 0;
+ Saig_ManForEachLo( p, pObj, i )
+ if ( Aig_ObjIsTravIdPrevious(p, pObj) )
+ Aig_ObjSetTravIdCurrent(p, pObj);
+ else
+ (*pnRegFixed)++;
+ // mark all the nodes that can be retimed forward
+ *pnRegMoves = 0;
+ Aig_ManForEachNode( p, pObj, i )
+ if ( Aig_ObjIsTravIdCurrent(p, Aig_ObjFanin0(pObj)) && Aig_ObjIsTravIdCurrent(p, Aig_ObjFanin1(pObj)) )
+ {
+ Aig_ObjSetTravIdCurrent(p, pObj);
+ (*pnRegMoves)++;
+ }
+ // mark the remaining registers
+ Saig_ManForEachLo( p, pObj, i )
+ Aig_ObjSetTravIdCurrent(p, pObj);
+ // find the cut (all such marked objects that fanout into unmarked nodes)
+ vCut = Vec_PtrAlloc( 1000 );
+ Aig_ManIncrementTravId( p );
+ Aig_ManForEachObj( p, pObj, i )
+ {
+ if ( Aig_ObjIsTravIdPrevious(p, pObj) )
+ continue;
+ pFanin = Aig_ObjFanin0(pObj);
+ if ( pFanin && Aig_ObjIsTravIdPrevious(p, pFanin) )
+ {
+ Vec_PtrPush( vCut, pFanin );
+ Aig_ObjSetTravIdCurrent( p, pFanin );
+ }
+ pFanin = Aig_ObjFanin1(pObj);
+ if ( pFanin && Aig_ObjIsTravIdPrevious(p, pFanin) )
+ {
+ Vec_PtrPush( vCut, pFanin );
+ Aig_ObjSetTravIdCurrent( p, pFanin );
+ }
+ }
+ // finally derive the new manager
+ pNew = Saig_ManRetimeDupForward( p, vCut );
+ Vec_PtrFree( vCut );
+ return pNew;
+}
+
+/**Function*************************************************************
+
+ Synopsis [Derives the cut for forward retiming.]
+
+ Description [Assumes topological ordering of the nodes.]
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+Aig_Man_t * Saig_ManRetimeForward( Aig_Man_t * p, int nMaxIters, int fVerbose )
+{
+ Aig_Man_t * pNew, * pTemp;
+ int i, clk, nRegFixed, nRegMoves = 1;
+ pNew = p;
+ for ( i = 0; i < nMaxIters && nRegMoves > 0; i++ )
+ {
+ clk = clock();
+ pNew = Saig_ManRetimeForwardOne( pTemp = pNew, &nRegFixed, &nRegMoves );
+ if ( fVerbose )
+ {
+ printf( "%2d : And = %6d. Reg = %5d. Unret = %5d. Move = %6d. ",
+ i + 1, Aig_ManNodeNum(pTemp), Aig_ManRegNum(pTemp), nRegFixed, nRegMoves );
+ PRT( "Time", clock() - clk );
+ }
+ if ( pTemp != p )
+ Aig_ManStop( pTemp );
+ }
+ clk = clock();
+ pNew = Aig_ManReduceLaches( pNew, fVerbose );
+ if ( fVerbose )
+ {
+ PRT( "Register sharing time", clock() - clk );
+ }
+ return pNew;
+}
+
+
+////////////////////////////////////////////////////////////////////////
+/// END OF FILE ///
+////////////////////////////////////////////////////////////////////////
+
+
diff --git a/src/aig/saig/saigRetMin.c b/src/aig/saig/saigRetMin.c
index c53d6d6b..324d8867 100644
--- a/src/aig/saig/saigRetMin.c
+++ b/src/aig/saig/saigRetMin.c
@@ -617,16 +617,16 @@ Aig_Man_t * Saig_ManRetimeMinAreaBackward( Aig_Man_t * pNew, int fVerbose )
SeeAlso []
***********************************************************************/
-Aig_Man_t * Saig_ManRetimeMinArea( Aig_Man_t * p, int fForwardOnly, int fBackwardOnly, int fInitial, int fVerbose )
+Aig_Man_t * Saig_ManRetimeMinArea( Aig_Man_t * p, int nMaxIters, int fForwardOnly, int fBackwardOnly, int fInitial, int fVerbose )
{
Vec_Ptr_t * vCut;
Aig_Man_t * pNew, * pTemp, * pCopy;
- int fChanges;
+ int i, fChanges;
pNew = Aig_ManDup( p );
// perform several iterations of forward retiming
fChanges = 0;
if ( !fBackwardOnly )
- while ( 1 )
+ for ( i = 0; i < nMaxIters; i++ )
{
vCut = Nwk_ManDeriveRetimingCut( pNew, 1, fVerbose );
if ( Vec_PtrSize(vCut) >= Aig_ManRegNum(pNew) )
@@ -646,7 +646,7 @@ Aig_Man_t * Saig_ManRetimeMinArea( Aig_Man_t * p, int fForwardOnly, int fBackwar
// perform several iterations of backward retiming
fChanges = 0;
if ( !fForwardOnly && !fInitial )
- while ( 1 )
+ for ( i = 0; i < nMaxIters; i++ )
{
vCut = Nwk_ManDeriveRetimingCut( pNew, 0, fVerbose );
if ( Vec_PtrSize(vCut) >= Aig_ManRegNum(pNew) )
@@ -664,7 +664,7 @@ Aig_Man_t * Saig_ManRetimeMinArea( Aig_Man_t * p, int fForwardOnly, int fBackwar
fChanges = 1;
}
else if ( !fForwardOnly && fInitial )
- while ( 1 )
+ for ( i = 0; i < nMaxIters; i++ )
{
pCopy = Aig_ManDup( pNew );
pTemp = Saig_ManRetimeMinAreaBackward( pCopy, fVerbose );
diff --git a/src/aig/saig/saigScl.c b/src/aig/saig/saigScl.c
new file mode 100644
index 00000000..b747eff9
--- /dev/null
+++ b/src/aig/saig/saigScl.c
@@ -0,0 +1,74 @@
+/**CFile****************************************************************
+
+ FileName [saigScl.c]
+
+ SystemName [ABC: Logic synthesis and verification system.]
+
+ PackageName [Sequential AIG package.]
+
+ Synopsis [Sequential cleanup.]
+
+ Author [Alan Mishchenko]
+
+ Affiliation [UC Berkeley]
+
+ Date [Ver. 1.0. Started - June 20, 2005.]
+
+ Revision [$Id: saigScl.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
+
+***********************************************************************/
+
+#include "saig.h"
+
+////////////////////////////////////////////////////////////////////////
+/// DECLARATIONS ///
+////////////////////////////////////////////////////////////////////////
+
+////////////////////////////////////////////////////////////////////////
+/// FUNCTION DEFINITIONS ///
+////////////////////////////////////////////////////////////////////////
+
+/**Function*************************************************************
+
+ Synopsis [Report registers useless for SEC.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+void Saig_ManReportUselessRegisters( Aig_Man_t * pAig )
+{
+ Aig_Obj_t * pObj, * pDriver;
+ int i, Counter1, Counter2;
+ // set PIO numbers
+ Aig_ManSetPioNumbers( pAig );
+ // check how many POs are driven by a register whose ref count is 1
+ Counter1 = 0;
+ Saig_ManForEachPo( pAig, pObj, i )
+ {
+ pDriver = Aig_ObjFanin0(pObj);
+ if ( Saig_ObjIsLo(pAig, pDriver) && Aig_ObjRefs(pDriver) == 1 )
+ Counter1++;
+ }
+ // check how many PIs have ref count 1 and drive a register
+ Counter2 = 0;
+ Saig_ManForEachLi( pAig, pObj, i )
+ {
+ pDriver = Aig_ObjFanin0(pObj);
+ if ( Saig_ObjIsPi(pAig, pDriver) && Aig_ObjRefs(pDriver) == 1 )
+ Counter2++;
+ }
+ if ( Counter1 )
+ printf( "Network has %d (out of %d) registers driving POs.\n", Counter1, Saig_ManRegNum(pAig) );
+ if ( Counter2 )
+ printf( "Network has %d (out of %d) registers driven by PIs.\n", Counter2, Saig_ManRegNum(pAig) );
+}
+
+////////////////////////////////////////////////////////////////////////
+/// END OF FILE ///
+////////////////////////////////////////////////////////////////////////
+
+
diff --git a/src/base/abci/abc.c b/src/base/abci/abc.c
index 492fefae..e7896cb1 100644
--- a/src/base/abci/abc.c
+++ b/src/base/abci/abc.c
@@ -98,6 +98,7 @@ static int Abc_CommandBidec ( Abc_Frame_t * pAbc, int argc, char ** arg
static int Abc_CommandOrder ( Abc_Frame_t * pAbc, int argc, char ** argv );
static int Abc_CommandMuxes ( Abc_Frame_t * pAbc, int argc, char ** argv );
static int Abc_CommandExtSeqDcs ( Abc_Frame_t * pAbc, int argc, char ** argv );
+static int Abc_CommandReach ( Abc_Frame_t * pAbc, int argc, char ** argv );
static int Abc_CommandCone ( Abc_Frame_t * pAbc, int argc, char ** argv );
static int Abc_CommandNode ( Abc_Frame_t * pAbc, int argc, char ** argv );
static int Abc_CommandTopmost ( Abc_Frame_t * pAbc, int argc, char ** argv );
@@ -349,6 +350,7 @@ void Abc_Init( Abc_Frame_t * pAbc )
Cmd_CommandAdd( pAbc, "Various", "order", Abc_CommandOrder, 0 );
Cmd_CommandAdd( pAbc, "Various", "muxes", Abc_CommandMuxes, 1 );
Cmd_CommandAdd( pAbc, "Various", "ext_seq_dcs", Abc_CommandExtSeqDcs, 0 );
+ Cmd_CommandAdd( pAbc, "Various", "reach", Abc_CommandReach, 0 );
Cmd_CommandAdd( pAbc, "Various", "cone", Abc_CommandCone, 1 );
Cmd_CommandAdd( pAbc, "Various", "node", Abc_CommandNode, 1 );
Cmd_CommandAdd( pAbc, "Various", "topmost", Abc_CommandTopmost, 1 );
@@ -5605,6 +5607,116 @@ usage:
SeeAlso []
***********************************************************************/
+int Abc_CommandReach( Abc_Frame_t * pAbc, int argc, char ** argv )
+{
+ FILE * pOut, * pErr;
+ Abc_Ntk_t * pNtk;
+ int nBddMax;
+ int nIterMax;
+ int fPartition;
+ int fReorder;
+ int fVerbose;
+ int c;
+ extern void Abc_NtkVerifyUsingBdds( Abc_Ntk_t * pNtk, int nBddMax, int nIterMax, int fPartition, int fReorder, int fVerbose );
+
+ pNtk = Abc_FrameReadNtk(pAbc);
+ pOut = Abc_FrameReadOut(pAbc);
+ pErr = Abc_FrameReadErr(pAbc);
+
+ // set defaults
+ nBddMax = 50000;
+ nIterMax = 1000;
+ fPartition = 1;
+ fReorder = 1;
+ fVerbose = 0;
+ Extra_UtilGetoptReset();
+ while ( ( c = Extra_UtilGetopt( argc, argv, "BFprvh" ) ) != EOF )
+ {
+ switch ( c )
+ {
+ case 'B':
+ if ( globalUtilOptind >= argc )
+ {
+ fprintf( pErr, "Command line switch \"-B\" should be followed by an integer.\n" );
+ goto usage;
+ }
+ nBddMax = atoi(argv[globalUtilOptind]);
+ globalUtilOptind++;
+ if ( nBddMax < 0 )
+ goto usage;
+ break;
+ case 'F':
+ if ( globalUtilOptind >= argc )
+ {
+ fprintf( pErr, "Command line switch \"-F\" should be followed by an integer.\n" );
+ goto usage;
+ }
+ nIterMax = atoi(argv[globalUtilOptind]);
+ globalUtilOptind++;
+ if ( nIterMax < 0 )
+ goto usage;
+ break;
+ case 'p':
+ fPartition ^= 1;
+ break;
+ case 'r':
+ fReorder ^= 1;
+ break;
+ case 'v':
+ fVerbose ^= 1;
+ break;
+ case 'h':
+ goto usage;
+ default:
+ goto usage;
+ }
+ }
+ if ( pNtk == NULL )
+ {
+ fprintf( pErr, "Empty network.\n" );
+ return 1;
+ }
+ if ( Abc_NtkLatchNum(pNtk) == 0 )
+ {
+ fprintf( stdout, "The current network has no latches.\n" );
+ return 0;
+ }
+ if ( !Abc_NtkIsStrash(pNtk) )
+ {
+ fprintf( stdout, "Reachability analysis works only for AIGs (run \"strash\").\n" );
+ return 1;
+ }
+ if ( Abc_NtkPoNum(pNtk) != 1 )
+ {
+ fprintf( stdout, "The sequential miter has more than one output (run \"orpos\").\n" );
+ return 1;
+ }
+ Abc_NtkVerifyUsingBdds( pNtk, nBddMax, nIterMax, fPartition, fReorder, fVerbose );
+ return 0;
+
+usage:
+ fprintf( pErr, "usage: reach [-BF num] [-prvh]\n" );
+ fprintf( pErr, "\t verifies sequential miter using BDD-based reachability\n" );
+ fprintf( pErr, "\t-B num : max number of nodes in the intermediate BDDs [default = %d]\n", nBddMax );
+ fprintf( pErr, "\t-F num : max number of reachability iterations [default = %d]\n", nIterMax );
+ fprintf( pErr, "\t-p : enable partitioned image computation [default = %s]\n", fPartition? "yes": "no" );
+ fprintf( pErr, "\t-r : enable dynamic BDD variable reordering [default = %s]\n", fReorder? "yes": "no" );
+ fprintf( pErr, "\t-v : prints verbose information [default = %s]\n", fVerbose? "yes": "no" );
+ fprintf( pErr, "\t-h : print the command usage\n");
+ return 1;
+}
+
+/**Function*************************************************************
+
+ Synopsis []
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
int Abc_CommandCone( Abc_Frame_t * pAbc, int argc, char ** argv )
{
FILE * pOut, * pErr;
@@ -11925,10 +12037,11 @@ int Abc_CommandDRetime( Abc_Frame_t * pAbc, int argc, char ** argv )
int nStepsMax;
int fFastAlgo;
int fVerbose;
- int c;
+ int c, nMaxIters;
extern Abc_Ntk_t * Abc_NtkDarRetime( Abc_Ntk_t * pNtk, int nStepsMax, int fVerbose );
extern Abc_Ntk_t * Abc_NtkDarRetimeF( Abc_Ntk_t * pNtk, int nStepsMax, int fVerbose );
- extern Abc_Ntk_t * Abc_NtkDarRetimeMinArea( Abc_Ntk_t * pNtk, int fForwardOnly, int fBackwardOnly, int fInitial, int fVerbose );
+ extern Abc_Ntk_t * Abc_NtkDarRetimeMinArea( Abc_Ntk_t * pNtk, int nMaxIters, int fForwardOnly, int fBackwardOnly, int fInitial, int fVerbose );
+ extern Abc_Ntk_t * Abc_NtkDarRetimeMostFwd( Abc_Ntk_t * pNtk, int nMaxIters, int fVerbose );
pNtk = Abc_FrameReadNtk(pAbc);
pOut = Abc_FrameReadOut(pAbc);
@@ -11940,13 +12053,25 @@ int Abc_CommandDRetime( Abc_Frame_t * pAbc, int argc, char ** argv )
fBackwardOnly = 0;
fInitial = 1;
nStepsMax = 100000;
- fFastAlgo = 1;
+ fFastAlgo = 0;
+ nMaxIters = 20;
fVerbose = 0;
Extra_UtilGetoptReset();
- while ( ( c = Extra_UtilGetopt( argc, argv, "Smfbiavh" ) ) != EOF )
+ while ( ( c = Extra_UtilGetopt( argc, argv, "NSmfbiavh" ) ) != EOF )
{
switch ( c )
{
+ case 'N':
+ if ( globalUtilOptind >= argc )
+ {
+ fprintf( pErr, "Command line switch \"-N\" should be followed by a positive integer.\n" );
+ goto usage;
+ }
+ nMaxIters = atoi(argv[globalUtilOptind]);
+ globalUtilOptind++;
+ if ( nMaxIters < 0 )
+ goto usage;
+ break;
case 'S':
if ( globalUtilOptind >= argc )
{
@@ -12003,11 +12128,12 @@ int Abc_CommandDRetime( Abc_Frame_t * pAbc, int argc, char ** argv )
// perform the retiming
if ( fMinArea )
- pNtkRes = Abc_NtkDarRetimeMinArea( pNtk, fForwardOnly, fBackwardOnly, fInitial, fVerbose );
+ pNtkRes = Abc_NtkDarRetimeMinArea( pNtk, nMaxIters, fForwardOnly, fBackwardOnly, fInitial, fVerbose );
else if ( fFastAlgo )
pNtkRes = Abc_NtkDarRetime( pNtk, nStepsMax, fVerbose );
else
- pNtkRes = Abc_NtkDarRetimeF( pNtk, nStepsMax, fVerbose );
+// pNtkRes = Abc_NtkDarRetimeF( pNtk, nStepsMax, fVerbose );
+ pNtkRes = Abc_NtkDarRetimeMostFwd( pNtk, nMaxIters, fVerbose );
if ( pNtkRes == NULL )
{
fprintf( pErr, "Retiming has failed.\n" );
@@ -12018,12 +12144,13 @@ int Abc_CommandDRetime( Abc_Frame_t * pAbc, int argc, char ** argv )
return 0;
usage:
- fprintf( pErr, "usage: dretime [-S num] [-mfbiavh]\n" );
- fprintf( pErr, "\t new implementation of min-area retiming\n" );
- fprintf( pErr, "\t-m : toggle min-area and most-forward retiming [default = %s]\n", fMinArea? "min-area": "most-fwd" );
+ fprintf( pErr, "usage: dretime [-NS num] [-mfbiavh]\n" );
+ fprintf( pErr, "\t new implementation of min-area (or most-forward) retiming\n" );
+ fprintf( pErr, "\t-m : toggle min-area retiming and most-forward retiming [default = %s]\n", fMinArea? "min-area": "most-fwd" );
fprintf( pErr, "\t-f : enables forward-only retiming [default = %s]\n", fForwardOnly? "yes": "no" );
fprintf( pErr, "\t-b : enables backward-only retiming [default = %s]\n", fBackwardOnly? "yes": "no" );
fprintf( pErr, "\t-i : enables init state computation [default = %s]\n", fInitial? "yes": "no" );
+ fprintf( pErr, "\t-N num : the max number of one-frame iterations to perform [default = %d]\n", nMaxIters );
fprintf( pErr, "\t-S num : the max number of forward retiming steps to perform [default = %d]\n", nStepsMax );
fprintf( pErr, "\t-a : enables a fast most-forward algorithm [default = %s]\n", fFastAlgo? "yes": "no" );
fprintf( pErr, "\t-v : enables verbose output [default = %s]\n", fVerbose? "yes": "no" );
diff --git a/src/base/abci/abcDar.c b/src/base/abci/abcDar.c
index 20557fb3..4b1a37c2 100644
--- a/src/base/abci/abcDar.c
+++ b/src/base/abci/abcDar.c
@@ -1409,7 +1409,7 @@ Abc_Ntk_t * Abc_NtkDarRetime( Abc_Ntk_t * pNtk, int nStepsMax, int fVerbose )
Vec_IntFree( pMan->vFlopNums );
pMan->vFlopNums = NULL;
- pMan = Rtm_ManRetime( pTemp = pMan, 1, nStepsMax, 0 );
+ pMan = Rtm_ManRetime( pTemp = pMan, 1, nStepsMax, fVerbose );
Aig_ManStop( pTemp );
// pMan = Aig_ManReduceLaches( pMan, 1 );
@@ -1431,24 +1431,24 @@ Abc_Ntk_t * Abc_NtkDarRetime( Abc_Ntk_t * pNtk, int nStepsMax, int fVerbose )
SeeAlso []
***********************************************************************/
-Abc_Ntk_t * Abc_NtkDarRetimeMinArea( Abc_Ntk_t * pNtk, int fForwardOnly, int fBackwardOnly, int fInitial, int fVerbose )
+Abc_Ntk_t * Abc_NtkDarRetimeF( Abc_Ntk_t * pNtk, int nStepsMax, int fVerbose )
{
- extern Aig_Man_t * Saig_ManRetimeMinArea( Aig_Man_t * p, int fForwardOnly, int fBackwardOnly, int fInitial, int fVerbose );
Abc_Ntk_t * pNtkAig;
Aig_Man_t * pMan, * pTemp;
pMan = Abc_NtkToDar( pNtk, 0, 1 );
if ( pMan == NULL )
return NULL;
+// Aig_ManReduceLachesCount( pMan );
if ( pMan->vFlopNums )
Vec_IntFree( pMan->vFlopNums );
pMan->vFlopNums = NULL;
- pMan->nTruePis = Aig_ManPiNum(pMan) - Aig_ManRegNum(pMan);
- pMan->nTruePos = Aig_ManPoNum(pMan) - Aig_ManRegNum(pMan);
-
- pMan = Saig_ManRetimeMinArea( pTemp = pMan, fForwardOnly, fBackwardOnly, fInitial, fVerbose );
+ pMan = Aig_ManRetimeFrontier( pTemp = pMan, nStepsMax );
Aig_ManStop( pTemp );
+// pMan = Aig_ManReduceLaches( pMan, 1 );
+// pMan = Aig_ManConstReduce( pMan, 1 );
+
pNtkAig = Abc_NtkFromDarSeqSweep( pNtk, pMan );
Aig_ManStop( pMan );
return pNtkAig;
@@ -1465,8 +1465,10 @@ Abc_Ntk_t * Abc_NtkDarRetimeMinArea( Abc_Ntk_t * pNtk, int fForwardOnly, int fBa
SeeAlso []
***********************************************************************/
-Abc_Ntk_t * Abc_NtkDarRetimeF( Abc_Ntk_t * pNtk, int nStepsMax, int fVerbose )
+Abc_Ntk_t * Abc_NtkDarRetimeMostFwd( Abc_Ntk_t * pNtk, int nMaxIters, int fVerbose )
{
+ extern Aig_Man_t * Saig_ManRetimeForward( Aig_Man_t * p, int nIters, int fVerbose );
+
Abc_Ntk_t * pNtkAig;
Aig_Man_t * pMan, * pTemp;
pMan = Abc_NtkToDar( pNtk, 0, 1 );
@@ -1477,7 +1479,10 @@ Abc_Ntk_t * Abc_NtkDarRetimeF( Abc_Ntk_t * pNtk, int nStepsMax, int fVerbose )
Vec_IntFree( pMan->vFlopNums );
pMan->vFlopNums = NULL;
- pMan = Aig_ManRetimeFrontier( pTemp = pMan, nStepsMax );
+ pMan->nTruePis = Aig_ManPiNum(pMan) - Aig_ManRegNum(pMan);
+ pMan->nTruePos = Aig_ManPoNum(pMan) - Aig_ManRegNum(pMan);
+
+ pMan = Saig_ManRetimeForward( pTemp = pMan, nMaxIters, fVerbose );
Aig_ManStop( pTemp );
// pMan = Aig_ManReduceLaches( pMan, 1 );
@@ -1499,6 +1504,40 @@ Abc_Ntk_t * Abc_NtkDarRetimeF( Abc_Ntk_t * pNtk, int nStepsMax, int fVerbose )
SeeAlso []
***********************************************************************/
+Abc_Ntk_t * Abc_NtkDarRetimeMinArea( Abc_Ntk_t * pNtk, int nMaxIters, int fForwardOnly, int fBackwardOnly, int fInitial, int fVerbose )
+{
+ extern Aig_Man_t * Saig_ManRetimeMinArea( Aig_Man_t * p, int nMaxIters, int fForwardOnly, int fBackwardOnly, int fInitial, int fVerbose );
+ Abc_Ntk_t * pNtkAig;
+ Aig_Man_t * pMan, * pTemp;
+ pMan = Abc_NtkToDar( pNtk, 0, 1 );
+ if ( pMan == NULL )
+ return NULL;
+ if ( pMan->vFlopNums )
+ Vec_IntFree( pMan->vFlopNums );
+ pMan->vFlopNums = NULL;
+
+ pMan->nTruePis = Aig_ManPiNum(pMan) - Aig_ManRegNum(pMan);
+ pMan->nTruePos = Aig_ManPoNum(pMan) - Aig_ManRegNum(pMan);
+
+ pMan = Saig_ManRetimeMinArea( pTemp = pMan, nMaxIters, fForwardOnly, fBackwardOnly, fInitial, fVerbose );
+ Aig_ManStop( pTemp );
+
+ pNtkAig = Abc_NtkFromDarSeqSweep( pNtk, pMan );
+ Aig_ManStop( pMan );
+ return pNtkAig;
+}
+
+/**Function*************************************************************
+
+ Synopsis [Gives the current ABC network to AIG manager for processing.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
void Abc_NtkDarHaigRecord( Abc_Ntk_t * pNtk )
{
/*
diff --git a/src/base/abci/abcFpga.c b/src/base/abci/abcFpga.c
index 171cbf0a..78e7cf6b 100644
--- a/src/base/abci/abcFpga.c
+++ b/src/base/abci/abcFpga.c
@@ -201,7 +201,7 @@ Abc_Ntk_t * Abc_NtkFromFpga( Fpga_Man_t * pMan, Abc_Ntk_t * pNtk )
ProgressBar * pProgress;
Abc_Ntk_t * pNtkNew;
Abc_Obj_t * pNode, * pNodeNew;
- int i;//, nDupGates;
+ int i, nDupGates;
// create the new network
pNtkNew = Abc_NtkStartFrom( pNtk, ABC_NTK_LOGIC, ABC_FUNC_BDD );
// make the mapper point to the new network
@@ -229,9 +229,9 @@ Abc_Ntk_t * Abc_NtkFromFpga( Fpga_Man_t * pMan, Abc_Ntk_t * pNtk )
if ( Abc_ObjFanoutNum(pNodeNew) == 0 )
Abc_NtkDeleteObj( pNodeNew );
// decouple the PO driver nodes to reduce the number of levels
-// nDupGates = Abc_NtkLogicMakeSimpleCos( pNtkNew, 1 );
-// if ( nDupGates && Fpga_ManReadVerbose(pMan) )
-// printf( "Duplicated %d gates to decouple the CO drivers.\n", nDupGates );
+ nDupGates = Abc_NtkLogicMakeSimpleCos( pNtkNew, 1 );
+ if ( nDupGates && Fpga_ManReadVerbose(pMan) )
+ printf( "Duplicated %d gates to decouple the CO drivers.\n", nDupGates );
return pNtkNew;
}
diff --git a/src/base/abci/abcIf.c b/src/base/abci/abcIf.c
index cf6f88ae..94c7dda8 100644
--- a/src/base/abci/abcIf.c
+++ b/src/base/abci/abcIf.c
@@ -186,7 +186,7 @@ Abc_Ntk_t * Abc_NtkFromIf( If_Man_t * pIfMan, Abc_Ntk_t * pNtk )
Abc_Ntk_t * pNtkNew;
Abc_Obj_t * pNode, * pNodeNew;
Vec_Int_t * vCover;
- int i;//, nDupGates;
+ int i, nDupGates;
// create the new network
if ( pIfMan->pPars->fUseBdds || pIfMan->pPars->fUseCnfs || pIfMan->pPars->fUseMv )
pNtkNew = Abc_NtkStartFrom( pNtk, ABC_NTK_LOGIC, ABC_FUNC_BDD );
@@ -223,9 +223,9 @@ Abc_Ntk_t * Abc_NtkFromIf( If_Man_t * pIfMan, Abc_Ntk_t * pNtk )
if ( pIfMan->pPars->fUseBdds )
Abc_NtkBddReorder( pNtkNew, 0 );
// decouple the PO driver nodes to reduce the number of levels
-// nDupGates = Abc_NtkLogicMakeSimpleCos( pNtkNew, 1 );
-// if ( nDupGates && If_ManReadVerbose(pIfMan) )
-// printf( "Duplicated %d gates to decouple the CO drivers.\n", nDupGates );
+ nDupGates = Abc_NtkLogicMakeSimpleCos( pNtkNew, 1 );
+ if ( nDupGates && pIfMan->pPars->fVerbose )
+ printf( "Duplicated %d gates to decouple the CO drivers.\n", nDupGates );
return pNtkNew;
}
diff --git a/src/base/abci/abcReach.c b/src/base/abci/abcReach.c
new file mode 100644
index 00000000..42494b5c
--- /dev/null
+++ b/src/base/abci/abcReach.c
@@ -0,0 +1,313 @@
+/**CFile****************************************************************
+
+ FileName [abcReach.c]
+
+ SystemName [ABC: Logic synthesis and verification system.]
+
+ PackageName [Network and node package.]
+
+ Synopsis [Performs reachability analysis.]
+
+ Author [Alan Mishchenko]
+
+ Affiliation [UC Berkeley]
+
+ Date [Ver. 1.0. Started - June 20, 2005.]
+
+ Revision [$Id: abcReach.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
+
+***********************************************************************/
+
+#include "abc.h"
+
+////////////////////////////////////////////////////////////////////////
+/// DECLARATIONS ///
+////////////////////////////////////////////////////////////////////////
+
+////////////////////////////////////////////////////////////////////////
+/// FUNCTION DEFINITIONS ///
+////////////////////////////////////////////////////////////////////////
+
+/**Function*************************************************************
+
+ Synopsis [Computes the initial state and sets up the variable map.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+DdNode * Abc_NtkInitStateVarMap( DdManager * dd, Abc_Ntk_t * pNtk, int fVerbose )
+{
+ DdNode ** pbVarsX, ** pbVarsY;
+ DdNode * bTemp, * bProd, * bVar;
+ Abc_Obj_t * pLatch;
+ int i;
+
+ // set the variable mapping for Cudd_bddVarMap()
+ pbVarsX = ALLOC( DdNode *, dd->size );
+ pbVarsY = ALLOC( DdNode *, dd->size );
+ bProd = b1; Cudd_Ref( bProd );
+ Abc_NtkForEachLatch( pNtk, pLatch, i )
+ {
+ pbVarsX[i] = dd->vars[ Abc_NtkPiNum(pNtk) + i ];
+ pbVarsY[i] = dd->vars[ Abc_NtkCiNum(pNtk) + i ];
+ // get the initial value of the latch
+ bVar = Cudd_NotCond( pbVarsX[i], !Abc_LatchIsInit1(pLatch) );
+ bProd = Cudd_bddAnd( dd, bTemp = bProd, bVar ); Cudd_Ref( bProd );
+ Cudd_RecursiveDeref( dd, bTemp );
+ }
+ Cudd_SetVarMap( dd, pbVarsX, pbVarsY, Abc_NtkLatchNum(pNtk) );
+ FREE( pbVarsX );
+ FREE( pbVarsY );
+
+ Cudd_Deref( bProd );
+ return bProd;
+}
+
+/**Function*************************************************************
+
+ Synopsis []
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+DdNode ** Abc_NtkCreatePartitions( DdManager * dd, Abc_Ntk_t * pNtk, int fReorder, int fVerbose )
+{
+ DdNode ** pbParts;
+ DdNode * bVar;
+ Abc_Obj_t * pNode;
+ int i;
+
+ // extand the BDD manager to represent NS variables
+ assert( dd->size == Abc_NtkCiNum(pNtk) );
+ Cudd_bddIthVar( dd, Abc_NtkCiNum(pNtk) + Abc_NtkLatchNum(pNtk) - 1 );
+
+ // enable reordering
+ if ( fReorder )
+ Cudd_AutodynEnable( dd, CUDD_REORDER_SYMM_SIFT );
+ else
+ Cudd_AutodynDisable( dd );
+
+ // compute the transition relation
+ pbParts = ALLOC( DdNode *, Abc_NtkLatchNum(pNtk) );
+ Abc_NtkForEachLatch( pNtk, pNode, i )
+ {
+ bVar = Cudd_bddIthVar( dd, Abc_NtkCiNum(pNtk) + i );
+ pbParts[i] = Cudd_bddXnor( dd, bVar, Abc_ObjGlobalBdd(Abc_ObjFanin0(pNode)) ); Cudd_Ref( pbParts[i] );
+ }
+ // free the global BDDs
+ Abc_NtkFreeGlobalBdds( pNtk, 0 );
+
+ // reorder and disable reordering
+ if ( fReorder )
+ {
+ if ( fVerbose )
+ fprintf( stdout, "BDD nodes in the partitions before reordering %d.\n", Cudd_SharingSize(pbParts,Abc_NtkLatchNum(pNtk)) );
+ Cudd_ReduceHeap( dd, CUDD_REORDER_SYMM_SIFT, 100 );
+ Cudd_AutodynDisable( dd );
+ if ( fVerbose )
+ fprintf( stdout, "BDD nodes in the partitions after reordering %d.\n", Cudd_SharingSize(pbParts,Abc_NtkLatchNum(pNtk)) );
+ }
+ return pbParts;
+}
+
+/**Function*************************************************************
+
+ Synopsis [Computes the set of unreachable states.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+DdNode * Abc_NtkComputeReachable( DdManager * dd, Abc_Ntk_t * pNtk, DdNode ** pbParts, DdNode * bInitial, DdNode * bOutput, int nBddMax, int nIterMax, int fPartition, int fReorder, int fVerbose )
+{
+ int fInternalReorder = 0;
+ Extra_ImageTree_t * pTree;
+ Extra_ImageTree2_t * pTree2;
+ DdNode * bReached, * bCubeCs;
+ DdNode * bCurrent, * bNext, * bTemp;
+ DdNode ** pbVarsY;
+ Abc_Obj_t * pLatch;
+ int i, nIters, nBddSize;
+ int nThreshold = 10000;
+
+ // collect the NS variables
+ // set the variable mapping for Cudd_bddVarMap()
+ pbVarsY = ALLOC( DdNode *, dd->size );
+ Abc_NtkForEachLatch( pNtk, pLatch, i )
+ pbVarsY[i] = dd->vars[ Abc_NtkCiNum(pNtk) + i ];
+
+ // start the image computation
+ bCubeCs = Extra_bddComputeRangeCube( dd, Abc_NtkPiNum(pNtk), Abc_NtkCiNum(pNtk) ); Cudd_Ref( bCubeCs );
+ if ( fPartition )
+ pTree = Extra_bddImageStart( dd, bCubeCs, Abc_NtkLatchNum(pNtk), pbParts, Abc_NtkLatchNum(pNtk), pbVarsY, fVerbose );
+ else
+ pTree2 = Extra_bddImageStart2( dd, bCubeCs, Abc_NtkLatchNum(pNtk), pbParts, Abc_NtkLatchNum(pNtk), pbVarsY, fVerbose );
+ free( pbVarsY );
+ Cudd_RecursiveDeref( dd, bCubeCs );
+
+ // perform reachability analisys
+ bCurrent = bInitial; Cudd_Ref( bCurrent );
+ bReached = bInitial; Cudd_Ref( bReached );
+ for ( nIters = 1; nIters <= nIterMax; nIters++ )
+ {
+ // compute the next states
+ if ( fPartition )
+ bNext = Extra_bddImageCompute( pTree, bCurrent );
+ else
+ bNext = Extra_bddImageCompute2( pTree2, bCurrent );
+ Cudd_Ref( bNext );
+ Cudd_RecursiveDeref( dd, bCurrent );
+ // remap these states into the current state vars
+ bNext = Cudd_bddVarMap( dd, bTemp = bNext ); Cudd_Ref( bNext );
+ Cudd_RecursiveDeref( dd, bTemp );
+ // check if there are any new states
+ if ( Cudd_bddLeq( dd, bNext, bReached ) )
+ break;
+ // check the BDD size
+ nBddSize = Cudd_DagSize(bNext);
+ if ( nBddSize > nBddMax )
+ break;
+ // check the result
+ if ( !Cudd_bddLeq( dd, bNext, Cudd_Not(bOutput) ) )
+ {
+ printf( "The miter is proved REACHABLE in %d iterations. ", nIters );
+ Cudd_RecursiveDeref( dd, bReached );
+ bReached = NULL;
+ break;
+ }
+ // get the new states
+ bCurrent = Cudd_bddAnd( dd, bNext, Cudd_Not(bReached) ); Cudd_Ref( bCurrent );
+ // minimize the new states with the reached states
+// bCurrent = Cudd_bddConstrain( dd, bTemp = bCurrent, Cudd_Not(bReached) ); Cudd_Ref( bCurrent );
+// Cudd_RecursiveDeref( dd, bTemp );
+ // add to the reached states
+ bReached = Cudd_bddOr( dd, bTemp = bReached, bNext ); Cudd_Ref( bReached );
+ Cudd_RecursiveDeref( dd, bTemp );
+ Cudd_RecursiveDeref( dd, bNext );
+ if ( fVerbose )
+ fprintf( stdout, "Iteration = %3d. BDD = %5d. ", nIters, nBddSize );
+ if ( fInternalReorder && fReorder && nBddSize > nThreshold )
+ {
+ if ( fVerbose )
+ fprintf( stdout, "Reordering... Before = %5d. ", Cudd_DagSize(bReached) );
+ Cudd_ReduceHeap( dd, CUDD_REORDER_SYMM_SIFT, 100 );
+ Cudd_AutodynDisable( dd );
+ if ( fVerbose )
+ fprintf( stdout, "After = %5d.\r", Cudd_DagSize(bReached) );
+ nThreshold *= 2;
+ }
+ if ( fVerbose )
+ fprintf( stdout, "\r" );
+ }
+ Cudd_RecursiveDeref( dd, bNext );
+ // undo the image tree
+ if ( fPartition )
+ Extra_bddImageTreeDelete( pTree );
+ else
+ Extra_bddImageTreeDelete2( pTree2 );
+ if ( bReached == NULL )
+ return NULL;
+ // report the stats
+ if ( fVerbose )
+ {
+ double nMints = Cudd_CountMinterm(dd, bReached, Abc_NtkLatchNum(pNtk) );
+ if ( nIters > nIterMax || Cudd_DagSize(bReached) > nBddMax )
+ fprintf( stdout, "Reachability analysis is stopped after %d iterations.\n", nIters );
+ else
+ fprintf( stdout, "Reachability analysis completed in %d iterations.\n", nIters );
+ fprintf( stdout, "Reachable states = %.0f. (Ratio = %.4f %%)\n", nMints, 100.0*nMints/pow(2.0, Abc_NtkLatchNum(pNtk)) );
+ fflush( stdout );
+ }
+//PRB( dd, bReached );
+ Cudd_Deref( bReached );
+ if ( nIters > nIterMax || Cudd_DagSize(bReached) > nBddMax )
+ printf( "Verified ONLY FOR STATES REACHED in %d iterations. \n", nIters );
+ printf( "The miter is proved unreachable in %d iteration. ", nIters );
+ return bReached;
+}
+
+/**Function*************************************************************
+
+ Synopsis [Performs reachability to see if any .]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+void Abc_NtkVerifyUsingBdds( Abc_Ntk_t * pNtk, int nBddMax, int nIterMax, int fPartition, int fReorder, int fVerbose )
+{
+ DdManager * dd;
+ DdNode ** pbParts;
+ DdNode * bOutput, * bReached, * bInitial;
+ int i, clk = clock();
+
+ assert( Abc_NtkIsStrash(pNtk) );
+ assert( Abc_NtkPoNum(pNtk) == 1 );
+ assert( Abc_ObjFanoutNum(Abc_NtkPo(pNtk,0)) == 0 ); // PO should go first
+
+ // compute the global BDDs of the latches
+ dd = Abc_NtkBuildGlobalBdds( pNtk, nBddMax, 1, fReorder, fVerbose );
+ if ( dd == NULL )
+ {
+ printf( "The number of intermediate BDD nodes exceeded the limit (%d).\n", nBddMax );
+ return;
+ }
+ if ( fVerbose )
+ printf( "Shared BDD size is %6d nodes.\n", Cudd_ReadKeys(dd) - Cudd_ReadDead(dd) );
+
+ // save the output BDD
+ bOutput = Abc_ObjGlobalBdd(Abc_NtkPo(pNtk,0)); Cudd_Ref( bOutput );
+
+ // create partitions
+ pbParts = Abc_NtkCreatePartitions( dd, pNtk, fReorder, fVerbose );
+
+ // create the initial state and the variable map
+ bInitial = Abc_NtkInitStateVarMap( dd, pNtk, fVerbose ); Cudd_Ref( bInitial );
+
+ // check the result
+ if ( !Cudd_bddLeq( dd, bInitial, Cudd_Not(bOutput) ) )
+ printf( "The miter is proved REACHABLE in the initial state. " );
+ else
+ {
+ // compute the reachable states
+ bReached = Abc_NtkComputeReachable( dd, pNtk, pbParts, bInitial, bOutput, nBddMax, nIterMax, fPartition, fReorder, fVerbose );
+ if ( bReached != NULL )
+ {
+ Cudd_Ref( bReached );
+ Cudd_RecursiveDeref( dd, bReached );
+ }
+ }
+
+ // cleanup
+ Cudd_RecursiveDeref( dd, bOutput );
+ Cudd_RecursiveDeref( dd, bInitial );
+ for ( i = 0; i < Abc_NtkLatchNum(pNtk); i++ )
+ Cudd_RecursiveDeref( dd, pbParts[i] );
+ free( pbParts );
+ Extra_StopManager( dd );
+
+ // report the runtime
+ PRT( "Time", clock() - clk );
+ fflush( stdout );
+}
+
+
+////////////////////////////////////////////////////////////////////////
+/// END OF FILE ///
+////////////////////////////////////////////////////////////////////////
+
+
diff --git a/src/base/abci/module.make b/src/base/abci/module.make
index 716f1618..ca2f2501 100644
--- a/src/base/abci/module.make
+++ b/src/base/abci/module.make
@@ -39,6 +39,7 @@ SRC += src/base/abci/abc.c \
src/base/abci/abcQuant.c \
src/base/abci/abcRec.c \
src/base/abci/abcReconv.c \
+ src/base/abci/abcReach.c \
src/base/abci/abcRefactor.c \
src/base/abci/abcRenode.c \
src/base/abci/abcReorder.c \
diff --git a/src/bdd/cas/casCore.c b/src/bdd/cas/casCore.c
index 579235b1..84d1e97b 100644
--- a/src/bdd/cas/casCore.c
+++ b/src/bdd/cas/casCore.c
@@ -52,7 +52,7 @@ DdNode * Cudd_bddTransferPermute( DdManager * ddSource, DdManager * ddDestinatio
////////////////////////////////////////////////////////////////////////
#define PRD(p) printf( "\nDECOMPOSITION TREE:\n\n" ); PrintDecEntry( (p), 0 )
-#define PRB(f) printf( #f " = " ); Cudd_bddPrint(dd,f); printf( "\n" )
+#define PRB_(f) printf( #f " = " ); Cudd_bddPrint(dd,f); printf( "\n" )
#define PRK(f,n) Cudd_PrintKMap(stdout,dd,(f),Cudd_Not(f),(n),NULL,0); printf( "K-map for function" #f "\n\n" )
#define PRK2(f,g,n) Cudd_PrintKMap(stdout,dd,(f),(g),(n),NULL,0); printf( "K-map for function <" #f ", " #g ">\n\n" )
diff --git a/src/bdd/cas/casDec.c b/src/bdd/cas/casDec.c
index a1eb5f36..3435f30d 100644
--- a/src/bdd/cas/casDec.c
+++ b/src/bdd/cas/casDec.c
@@ -94,7 +94,7 @@ long s_EncComputeTime;
/// debugging macros ///
////////////////////////////////////////////////////////////////////////
-#define PRB(f) printf( #f " = " ); Cudd_bddPrint(dd,f); printf( "\n" )
+#define PRB_(f) printf( #f " = " ); Cudd_bddPrint(dd,f); printf( "\n" )
#define PRK(f,n) Cudd_PrintKMap(stdout,dd,(f),Cudd_Not(f),(n),NULL,0); printf( "K-map for function" #f "\n\n" )
#define PRK2(f,g,n) Cudd_PrintKMap(stdout,dd,(f),(g),(n),NULL,0); printf( "K-map for function <" #f ", " #g ">\n\n" )
diff --git a/src/map/pcm/module.make b/src/map/pcm/module.make
new file mode 100644
index 00000000..e69de29b
--- /dev/null
+++ b/src/map/pcm/module.make
diff --git a/src/map/ply/module.make b/src/map/ply/module.make
new file mode 100644
index 00000000..e69de29b
--- /dev/null
+++ b/src/map/ply/module.make
diff --git a/src/misc/extra/extra.h b/src/misc/extra/extra.h
index 8f86fc32..9870c3d0 100644
--- a/src/misc/extra/extra.h
+++ b/src/misc/extra/extra.h
@@ -118,6 +118,10 @@ typedef unsigned long long uint64;
#define PRTP(a,t,T) printf("%s = ", (a)); printf("%6.2f sec (%6.2f %%)\n", (float)(t)/(float)(CLOCKS_PER_SEC), (T)? 100.0*(t)/(T) : 0.0)
#endif
+#ifndef PRB
+#define PRB(dd,f) printf("%s = ", #f); Extra_bddPrint(dd,f); printf("\n")
+#endif
+
/*===========================================================================*/
/* Various Utilities */
/*===========================================================================*/
@@ -162,6 +166,26 @@ extern int Extra_bddNodePathsUnderCutArray( DdManager * dd, DdNode ** p
/* find the profile of a DD (the number of edges crossing each level) */
extern int Extra_ProfileWidth( DdManager * dd, DdNode * F, int * Profile, int CutLevel );
+/*=== extraBddImage.c ================================================================*/
+
+typedef struct Extra_ImageTree_t_ Extra_ImageTree_t;
+extern Extra_ImageTree_t * Extra_bddImageStart(
+ DdManager * dd, DdNode * bCare,
+ int nParts, DdNode ** pbParts,
+ int nVars, DdNode ** pbVars, int fVerbose );
+extern DdNode * Extra_bddImageCompute( Extra_ImageTree_t * pTree, DdNode * bCare );
+extern void Extra_bddImageTreeDelete( Extra_ImageTree_t * pTree );
+extern DdNode * Extra_bddImageRead( Extra_ImageTree_t * pTree );
+
+typedef struct Extra_ImageTree2_t_ Extra_ImageTree2_t;
+extern Extra_ImageTree2_t * Extra_bddImageStart2(
+ DdManager * dd, DdNode * bCare,
+ int nParts, DdNode ** pbParts,
+ int nVars, DdNode ** pbVars, int fVerbose );
+extern DdNode * Extra_bddImageCompute2( Extra_ImageTree2_t * pTree, DdNode * bCare );
+extern void Extra_bddImageTreeDelete2( Extra_ImageTree2_t * pTree );
+extern DdNode * Extra_bddImageRead2( Extra_ImageTree2_t * pTree );
+
/*=== extraBddMisc.c ========================================================*/
extern DdNode * Extra_TransferPermute( DdManager * ddSource, DdManager * ddDestination, DdNode * f, int * Permute );
@@ -190,6 +214,7 @@ extern DdNode * Extra_bddCreateOr( DdManager * dd, int nVars );
extern DdNode * Extra_bddCreateExor( DdManager * dd, int nVars );
extern DdNode * Extra_zddPrimes( DdManager * dd, DdNode * F );
extern void Extra_bddPermuteArray( DdManager * dd, DdNode ** bNodesIn, DdNode ** bNodesOut, int nNodes, int *permut );
+extern DdNode * Extra_bddComputeCube( DdManager * dd, DdNode ** bXVars, int nVars );
/*=== extraBddKmap.c ================================================================*/
diff --git a/src/misc/extra/extraBddImage.c b/src/misc/extra/extraBddImage.c
new file mode 100644
index 00000000..d21cfe23
--- /dev/null
+++ b/src/misc/extra/extraBddImage.c
@@ -0,0 +1,1157 @@
+/**CFile****************************************************************
+
+ FileName [extraBddImage.c]
+
+ PackageName [extra]
+
+ Synopsis [Various reusable software utilities.]
+
+ Author [Alan Mishchenko]
+
+ Affiliation [UC Berkeley]
+
+ Date [Ver. 1.0. Started - September 1, 2003.]
+
+ Revision [$Id: extraBddImage.c,v 1.0 2003/09/01 00:00:00 alanmi Exp $]
+
+***********************************************************************/
+
+#include "extra.h"
+
+/*
+ The ideas implemented in this file are inspired by the paper:
+ Pankaj Chauhan, Edmund Clarke, Somesh Jha, Jim Kukula, Tom Shiple,
+ Helmut Veith, Dong Wang. Non-linear Quantification Scheduling in
+ Image Computation. ICCAD, 2001.
+*/
+
+/*---------------------------------------------------------------------------*/
+/* Constant declarations */
+/*---------------------------------------------------------------------------*/
+
+/*---------------------------------------------------------------------------*/
+/* Stucture declarations */
+/*---------------------------------------------------------------------------*/
+
+typedef struct Extra_ImageNode_t_ Extra_ImageNode_t;
+typedef struct Extra_ImagePart_t_ Extra_ImagePart_t;
+typedef struct Extra_ImageVar_t_ Extra_ImageVar_t;
+
+struct Extra_ImageTree_t_
+{
+ Extra_ImageNode_t * pRoot; // the root of quantification tree
+ Extra_ImageNode_t * pCare; // the leaf node with the care set
+ DdNode * bCareSupp; // the cube to quantify from the care
+ int fVerbose; // the verbosity flag
+ int nNodesMax; // the max number of nodes in one iter
+ int nNodesMaxT; // the overall max number of nodes
+ int nIter; // the number of iterations with this tree
+};
+
+struct Extra_ImageNode_t_
+{
+ DdManager * dd; // the manager
+ DdNode * bCube; // the cube to quantify
+ DdNode * bImage; // the partial image
+ Extra_ImageNode_t * pNode1; // the first branch
+ Extra_ImageNode_t * pNode2; // the second branch
+ Extra_ImagePart_t * pPart; // the partition (temporary)
+};
+
+struct Extra_ImagePart_t_
+{
+ DdNode * bFunc; // the partition
+ DdNode * bSupp; // the support of this partition
+ int nNodes; // the number of BDD nodes
+ short nSupp; // the number of support variables
+ short iPart; // the number of this partition
+};
+
+struct Extra_ImageVar_t_
+{
+ int iNum; // the BDD index of this variable
+ DdNode * bParts; // the partition numbers
+ int nParts; // the number of partitions
+};
+
+/*---------------------------------------------------------------------------*/
+/* Type declarations */
+/*---------------------------------------------------------------------------*/
+
+/*---------------------------------------------------------------------------*/
+/* Variable declarations */
+/*---------------------------------------------------------------------------*/
+
+/*---------------------------------------------------------------------------*/
+/* Macro declarations */
+/*---------------------------------------------------------------------------*/
+
+/**AutomaticStart*************************************************************/
+
+
+/*---------------------------------------------------------------------------*/
+/* Static function prototypes */
+/*---------------------------------------------------------------------------*/
+
+static Extra_ImagePart_t ** Extra_CreateParts( DdManager * dd,
+ int nParts, DdNode ** pbParts, DdNode * bCare );
+static Extra_ImageVar_t ** Extra_CreateVars( DdManager * dd,
+ int nParts, Extra_ImagePart_t ** pParts,
+ int nVars, DdNode ** pbVarsNs );
+static Extra_ImageNode_t ** Extra_CreateNodes( DdManager * dd,
+ int nParts, Extra_ImagePart_t ** pParts,
+ int nVars, Extra_ImageVar_t ** pVars );
+static void Extra_DeleteParts_rec( Extra_ImageNode_t * pNode );
+static int Extra_BuildTreeNode( DdManager * dd,
+ int nNodes, Extra_ImageNode_t ** pNodes,
+ int nVars, Extra_ImageVar_t ** pVars );
+static Extra_ImageNode_t * Extra_MergeTopNodes( DdManager * dd,
+ int nNodes, Extra_ImageNode_t ** pNodes );
+static void Extra_bddImageTreeDelete_rec( Extra_ImageNode_t * pNode );
+static void Extra_bddImageCompute_rec( Extra_ImageTree_t * pTree, Extra_ImageNode_t * pNode );
+static int Extra_FindBestVariable( DdManager * dd,
+ int nNodes, Extra_ImageNode_t ** pNodes,
+ int nVars, Extra_ImageVar_t ** pVars );
+static void Extra_FindBestPartitions( DdManager * dd, DdNode * bParts,
+ int nNodes, Extra_ImageNode_t ** pNodes,
+ int * piNode1, int * piNode2 );
+static Extra_ImageNode_t * Extra_CombineTwoNodes( DdManager * dd, DdNode * bCube,
+ Extra_ImageNode_t * pNode1, Extra_ImageNode_t * pNode2 );
+
+static void Extra_bddImagePrintLatchDependency( DdManager * dd, DdNode * bCare,
+ int nParts, DdNode ** pbParts,
+ int nVars, DdNode ** pbVars );
+static void Extra_bddImagePrintLatchDependencyOne( DdManager * dd, DdNode * bFunc,
+ DdNode * bVarsCs, DdNode * bVarsNs, int iPart );
+
+static void Extra_bddImagePrintTree( Extra_ImageTree_t * pTree );
+static void Extra_bddImagePrintTree_rec( Extra_ImageNode_t * pNode, int nOffset );
+
+
+/**AutomaticEnd***************************************************************/
+
+
+/*---------------------------------------------------------------------------*/
+/* Definition of exported functions */
+/*---------------------------------------------------------------------------*/
+
+/**Function*************************************************************
+
+ Synopsis [Starts the image computation using tree-based scheduling.]
+
+ Description [This procedure starts the image computation. It uses
+ the given care set to test-run the image computation and creates the
+ quantification tree by scheduling variable quantifications. The tree can
+ be used to compute images for other care sets without rescheduling.
+ In this case, Extra_bddImageCompute() should be called.]
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+Extra_ImageTree_t * Extra_bddImageStart(
+ DdManager * dd, DdNode * bCare, // the care set
+ int nParts, DdNode ** pbParts, // the partitions for image computation
+ int nVars, DdNode ** pbVars, int fVerbose ) // the NS and parameter variables (not quantified!)
+{
+ Extra_ImageTree_t * pTree;
+ Extra_ImagePart_t ** pParts;
+ Extra_ImageVar_t ** pVars;
+ Extra_ImageNode_t ** pNodes;
+ int v;
+
+ if ( fVerbose && dd->size <= 80 )
+ Extra_bddImagePrintLatchDependency( dd, bCare, nParts, pbParts, nVars, pbVars );
+
+ // create variables, partitions and leaf nodes
+ pParts = Extra_CreateParts( dd, nParts, pbParts, bCare );
+ pVars = Extra_CreateVars( dd, nParts + 1, pParts, nVars, pbVars );
+ pNodes = Extra_CreateNodes( dd, nParts + 1, pParts, dd->size, pVars );
+
+ // create the tree
+ pTree = ALLOC( Extra_ImageTree_t, 1 );
+ memset( pTree, 0, sizeof(Extra_ImageTree_t) );
+ pTree->pCare = pNodes[nParts];
+ pTree->fVerbose = fVerbose;
+
+ // process the nodes
+ while ( Extra_BuildTreeNode( dd, nParts + 1, pNodes, dd->size, pVars ) );
+
+ // make sure the variables are gone
+ for ( v = 0; v < dd->size; v++ )
+ assert( pVars[v] == NULL );
+ FREE( pVars );
+
+ // merge the topmost nodes
+ while ( (pTree->pRoot = Extra_MergeTopNodes( dd, nParts + 1, pNodes )) == NULL );
+
+ // make sure the nodes are gone
+ for ( v = 0; v < nParts + 1; v++ )
+ assert( pNodes[v] == NULL );
+ FREE( pNodes );
+
+// if ( fVerbose )
+// Extra_bddImagePrintTree( pTree );
+
+ // set the support of the care set
+ pTree->bCareSupp = Cudd_Support( dd, bCare ); Cudd_Ref( pTree->bCareSupp );
+
+ // clean the partitions
+ Extra_DeleteParts_rec( pTree->pRoot );
+ FREE( pParts );
+ return pTree;
+}
+
+/**Function*************************************************************
+
+ Synopsis [Compute the image.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+DdNode * Extra_bddImageCompute( Extra_ImageTree_t * pTree, DdNode * bCare )
+{
+ DdManager * dd = pTree->pCare->dd;
+ DdNode * bSupp, * bRem;
+
+ pTree->nIter++;
+
+ // make sure the supports are okay
+ bSupp = Cudd_Support( dd, bCare ); Cudd_Ref( bSupp );
+ if ( bSupp != pTree->bCareSupp )
+ {
+ bRem = Cudd_bddExistAbstract( dd, bSupp, pTree->bCareSupp ); Cudd_Ref( bRem );
+ if ( bRem != b1 )
+ {
+printf( "Original care set support: " );
+PRB( dd, pTree->bCareSupp );
+printf( "Current care set support: " );
+PRB( dd, bSupp );
+ Cudd_RecursiveDeref( dd, bSupp );
+ Cudd_RecursiveDeref( dd, bRem );
+ printf( "The care set depends on some vars that were not in the care set during scheduling.\n" );
+ return NULL;
+ }
+ Cudd_RecursiveDeref( dd, bRem );
+ }
+ Cudd_RecursiveDeref( dd, bSupp );
+
+ // remove the previous image
+ Cudd_RecursiveDeref( dd, pTree->pCare->bImage );
+ pTree->pCare->bImage = bCare; Cudd_Ref( bCare );
+
+ // compute the image
+ pTree->nNodesMax = 0;
+ Extra_bddImageCompute_rec( pTree, pTree->pRoot );
+ if ( pTree->nNodesMaxT < pTree->nNodesMax )
+ pTree->nNodesMaxT = pTree->nNodesMax;
+
+// if ( pTree->fVerbose )
+// printf( "Iter %2d : Max nodes = %5d.\n", pTree->nIter, pTree->nNodesMax );
+ return pTree->pRoot->bImage;
+}
+
+/**Function*************************************************************
+
+ Synopsis [Delete the tree.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+void Extra_bddImageTreeDelete( Extra_ImageTree_t * pTree )
+{
+ if ( pTree->bCareSupp )
+ Cudd_RecursiveDeref( pTree->pRoot->dd, pTree->bCareSupp );
+ Extra_bddImageTreeDelete_rec( pTree->pRoot );
+ FREE( pTree );
+}
+
+/**Function*************************************************************
+
+ Synopsis [Reads the image from the tree.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+DdNode * Extra_bddImageRead( Extra_ImageTree_t * pTree )
+{
+ return pTree->pRoot->bImage;
+}
+
+/*---------------------------------------------------------------------------*/
+/* Definition of internal functions */
+/*---------------------------------------------------------------------------*/
+
+/*---------------------------------------------------------------------------*/
+/* Definition of static Functions */
+/*---------------------------------------------------------------------------*/
+
+/**Function*************************************************************
+
+ Synopsis [Creates partitions.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+Extra_ImagePart_t ** Extra_CreateParts( DdManager * dd,
+ int nParts, DdNode ** pbParts, DdNode * bCare )
+{
+ Extra_ImagePart_t ** pParts;
+ int i;
+
+ // start the partitions
+ pParts = ALLOC( Extra_ImagePart_t *, nParts + 1 );
+ // create structures for each variable
+ for ( i = 0; i < nParts; i++ )
+ {
+ pParts[i] = ALLOC( Extra_ImagePart_t, 1 );
+ pParts[i]->bFunc = pbParts[i]; Cudd_Ref( pParts[i]->bFunc );
+ pParts[i]->bSupp = Cudd_Support( dd, pParts[i]->bFunc ); Cudd_Ref( pParts[i]->bSupp );
+ pParts[i]->nSupp = Extra_bddSuppSize( dd, pParts[i]->bSupp );
+ pParts[i]->nNodes = Cudd_DagSize( pParts[i]->bFunc );
+ pParts[i]->iPart = i;
+ }
+ // add the care set as the last partition
+ pParts[nParts] = ALLOC( Extra_ImagePart_t, 1 );
+ pParts[nParts]->bFunc = bCare; Cudd_Ref( pParts[nParts]->bFunc );
+ pParts[nParts]->bSupp = Cudd_Support( dd, pParts[nParts]->bFunc ); Cudd_Ref( pParts[nParts]->bSupp );
+ pParts[nParts]->nSupp = Extra_bddSuppSize( dd, pParts[nParts]->bSupp );
+ pParts[nParts]->nNodes = Cudd_DagSize( pParts[nParts]->bFunc );
+ pParts[nParts]->iPart = nParts;
+ return pParts;
+}
+
+/**Function*************************************************************
+
+ Synopsis [Creates variables.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+Extra_ImageVar_t ** Extra_CreateVars( DdManager * dd,
+ int nParts, Extra_ImagePart_t ** pParts,
+ int nVars, DdNode ** pbVars )
+{
+ Extra_ImageVar_t ** pVars;
+ DdNode ** pbFuncs;
+ DdNode * bCubeNs, * bSupp, * bParts, * bTemp, * bSuppTemp;
+ int nVarsTotal, iVar, p, Counter;
+
+ // put all the functions into one array
+ pbFuncs = ALLOC( DdNode *, nParts );
+ for ( p = 0; p < nParts; p++ )
+ pbFuncs[p] = pParts[p]->bSupp;
+ bSupp = Cudd_VectorSupport( dd, pbFuncs, nParts ); Cudd_Ref( bSupp );
+ FREE( pbFuncs );
+
+ // remove the NS vars
+ bCubeNs = Cudd_bddComputeCube( dd, pbVars, NULL, nVars ); Cudd_Ref( bCubeNs );
+ bSupp = Cudd_bddExistAbstract( dd, bTemp = bSupp, bCubeNs ); Cudd_Ref( bSupp );
+ Cudd_RecursiveDeref( dd, bTemp );
+ Cudd_RecursiveDeref( dd, bCubeNs );
+
+ // get the number of I and CS variables to be quantified
+ nVarsTotal = Extra_bddSuppSize( dd, bSupp );
+
+ // start the variables
+ pVars = ALLOC( Extra_ImageVar_t *, dd->size );
+ memset( pVars, 0, sizeof(Extra_ImageVar_t *) * dd->size );
+ // create structures for each variable
+ for ( bSuppTemp = bSupp; bSuppTemp != b1; bSuppTemp = cuddT(bSuppTemp) )
+ {
+ iVar = bSuppTemp->index;
+ pVars[iVar] = ALLOC( Extra_ImageVar_t, 1 );
+ pVars[iVar]->iNum = iVar;
+ // collect all the parts this var belongs to
+ Counter = 0;
+ bParts = b1; Cudd_Ref( bParts );
+ for ( p = 0; p < nParts; p++ )
+ if ( Cudd_bddLeq( dd, pParts[p]->bSupp, dd->vars[bSuppTemp->index] ) )
+ {
+ bParts = Cudd_bddAnd( dd, bTemp = bParts, dd->vars[p] ); Cudd_Ref( bParts );
+ Cudd_RecursiveDeref( dd, bTemp );
+ Counter++;
+ }
+ pVars[iVar]->bParts = bParts; // takes ref
+ pVars[iVar]->nParts = Counter;
+ }
+ Cudd_RecursiveDeref( dd, bSupp );
+ return pVars;
+}
+
+/**Function*************************************************************
+
+ Synopsis [Creates variables.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+Extra_ImageNode_t ** Extra_CreateNodes( DdManager * dd,
+ int nParts, Extra_ImagePart_t ** pParts,
+ int nVars, Extra_ImageVar_t ** pVars )
+{
+ Extra_ImageNode_t ** pNodes;
+ Extra_ImageNode_t * pNode;
+ DdNode * bTemp;
+ int i, v, iPart;
+/*
+ DdManager * dd; // the manager
+ DdNode * bCube; // the cube to quantify
+ DdNode * bImage; // the partial image
+ Extra_ImageNode_t * pNode1; // the first branch
+ Extra_ImageNode_t * pNode2; // the second branch
+ Extra_ImagePart_t * pPart; // the partition (temporary)
+*/
+ // start the partitions
+ pNodes = ALLOC( Extra_ImageNode_t *, nParts );
+ // create structures for each leaf nodes
+ for ( i = 0; i < nParts; i++ )
+ {
+ pNodes[i] = ALLOC( Extra_ImageNode_t, 1 );
+ memset( pNodes[i], 0, sizeof(Extra_ImageNode_t) );
+ pNodes[i]->dd = dd;
+ pNodes[i]->pPart = pParts[i];
+ }
+ // find the quantification cubes for each leaf node
+ for ( v = 0; v < nVars; v++ )
+ {
+ if ( pVars[v] == NULL )
+ continue;
+ assert( pVars[v]->nParts > 0 );
+ if ( pVars[v]->nParts > 1 )
+ continue;
+ iPart = pVars[v]->bParts->index;
+ if ( pNodes[iPart]->bCube == NULL )
+ {
+ pNodes[iPart]->bCube = dd->vars[v];
+ Cudd_Ref( dd->vars[v] );
+ }
+ else
+ {
+ pNodes[iPart]->bCube = Cudd_bddAnd( dd, bTemp = pNodes[iPart]->bCube, dd->vars[v] );
+ Cudd_Ref( pNodes[iPart]->bCube );
+ Cudd_RecursiveDeref( dd, bTemp );
+ }
+ // remove these variables
+ Cudd_RecursiveDeref( dd, pVars[v]->bParts );
+ FREE( pVars[v] );
+ }
+
+ // assign the leaf node images
+ for ( i = 0; i < nParts; i++ )
+ {
+ pNode = pNodes[i];
+ if ( pNode->bCube )
+ {
+ // update the partition
+ pParts[i]->bFunc = Cudd_bddExistAbstract( dd, bTemp = pParts[i]->bFunc, pNode->bCube );
+ Cudd_Ref( pParts[i]->bFunc );
+ Cudd_RecursiveDeref( dd, bTemp );
+ // update the support the partition
+ pParts[i]->bSupp = Cudd_bddExistAbstract( dd, bTemp = pParts[i]->bSupp, pNode->bCube );
+ Cudd_Ref( pParts[i]->bSupp );
+ Cudd_RecursiveDeref( dd, bTemp );
+ // update the numbers
+ pParts[i]->nSupp = Extra_bddSuppSize( dd, pParts[i]->bSupp );
+ pParts[i]->nNodes = Cudd_DagSize( pParts[i]->bFunc );
+ // get rid of the cube
+ // save the last (care set) quantification cube
+ if ( i < nParts - 1 )
+ {
+ Cudd_RecursiveDeref( dd, pNode->bCube );
+ pNode->bCube = NULL;
+ }
+ }
+ // copy the function
+ pNode->bImage = pParts[i]->bFunc; Cudd_Ref( pNode->bImage );
+ }
+/*
+ for ( i = 0; i < nParts; i++ )
+ {
+ pNode = pNodes[i];
+PRB( dd, pNode->bCube );
+PRB( dd, pNode->pPart->bFunc );
+PRB( dd, pNode->pPart->bSupp );
+printf( "\n" );
+ }
+*/
+ return pNodes;
+}
+
+
+/**Function*************************************************************
+
+ Synopsis [Delete the partitions from the nodes.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+void Extra_DeleteParts_rec( Extra_ImageNode_t * pNode )
+{
+ Extra_ImagePart_t * pPart;
+ if ( pNode->pNode1 )
+ Extra_DeleteParts_rec( pNode->pNode1 );
+ if ( pNode->pNode2 )
+ Extra_DeleteParts_rec( pNode->pNode2 );
+ pPart = pNode->pPart;
+ Cudd_RecursiveDeref( pNode->dd, pPart->bFunc );
+ Cudd_RecursiveDeref( pNode->dd, pPart->bSupp );
+ FREE( pNode->pPart );
+}
+
+/**Function*************************************************************
+
+ Synopsis [Delete the partitions from the nodes.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+void Extra_bddImageTreeDelete_rec( Extra_ImageNode_t * pNode )
+{
+ if ( pNode->pNode1 )
+ Extra_bddImageTreeDelete_rec( pNode->pNode1 );
+ if ( pNode->pNode2 )
+ Extra_bddImageTreeDelete_rec( pNode->pNode2 );
+ if ( pNode->bCube )
+ Cudd_RecursiveDeref( pNode->dd, pNode->bCube );
+ if ( pNode->bImage )
+ Cudd_RecursiveDeref( pNode->dd, pNode->bImage );
+ assert( pNode->pPart == NULL );
+ FREE( pNode );
+}
+
+/**Function*************************************************************
+
+ Synopsis [Recompute the image.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+void Extra_bddImageCompute_rec( Extra_ImageTree_t * pTree, Extra_ImageNode_t * pNode )
+{
+ DdManager * dd = pNode->dd;
+ DdNode * bTemp;
+ int nNodes;
+
+ // trivial case
+ if ( pNode->pNode1 == NULL )
+ {
+ if ( pNode->bCube )
+ {
+ pNode->bImage = Cudd_bddExistAbstract( dd, bTemp = pNode->bImage, pNode->bCube );
+ Cudd_Ref( pNode->bImage );
+ Cudd_RecursiveDeref( dd, bTemp );
+ }
+ return;
+ }
+
+ // compute the children
+ if ( pNode->pNode1 )
+ Extra_bddImageCompute_rec( pTree, pNode->pNode1 );
+ if ( pNode->pNode2 )
+ Extra_bddImageCompute_rec( pTree, pNode->pNode2 );
+
+ // clean the old image
+ if ( pNode->bImage )
+ Cudd_RecursiveDeref( dd, pNode->bImage );
+ pNode->bImage = NULL;
+
+ // compute the new image
+ if ( pNode->bCube )
+ pNode->bImage = Cudd_bddAndAbstract( dd,
+ pNode->pNode1->bImage, pNode->pNode2->bImage, pNode->bCube );
+ else
+ pNode->bImage = Cudd_bddAnd( dd, pNode->pNode1->bImage, pNode->pNode2->bImage );
+ Cudd_Ref( pNode->bImage );
+
+ if ( pTree->fVerbose )
+ {
+ nNodes = Cudd_DagSize( pNode->bImage );
+ if ( pTree->nNodesMax < nNodes )
+ pTree->nNodesMax = nNodes;
+ }
+}
+
+/**Function*************************************************************
+
+ Synopsis [Builds the tree.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+int Extra_BuildTreeNode( DdManager * dd,
+ int nNodes, Extra_ImageNode_t ** pNodes,
+ int nVars, Extra_ImageVar_t ** pVars )
+{
+ Extra_ImageNode_t * pNode1, * pNode2;
+ Extra_ImageVar_t * pVar;
+ Extra_ImageNode_t * pNode;
+ DdNode * bCube, * bTemp, * bSuppTemp, * bParts;
+ int iNode1, iNode2;
+ int iVarBest, nSupp, v;
+
+ // find the best variable
+ iVarBest = Extra_FindBestVariable( dd, nNodes, pNodes, nVars, pVars );
+ if ( iVarBest == -1 )
+ return 0;
+
+ pVar = pVars[iVarBest];
+
+ // this var cannot appear in one partition only
+ nSupp = Extra_bddSuppSize( dd, pVar->bParts );
+ assert( nSupp == pVar->nParts );
+ assert( nSupp != 1 );
+
+ // if it appears in only two partitions, quantify it
+ if ( pVar->nParts == 2 )
+ {
+ // get the nodes
+ iNode1 = pVar->bParts->index;
+ iNode2 = cuddT(pVar->bParts)->index;
+ pNode1 = pNodes[iNode1];
+ pNode2 = pNodes[iNode2];
+
+ // get the quantification cube
+ bCube = dd->vars[pVar->iNum]; Cudd_Ref( bCube );
+ // add the variables that appear only in these partitions
+ for ( v = 0; v < nVars; v++ )
+ if ( pVars[v] && v != iVarBest && pVars[v]->bParts == pVars[iVarBest]->bParts )
+ {
+ // add this var
+ bCube = Cudd_bddAnd( dd, bTemp = bCube, dd->vars[pVars[v]->iNum] ); Cudd_Ref( bCube );
+ Cudd_RecursiveDeref( dd, bTemp );
+ // clean this var
+ Cudd_RecursiveDeref( dd, pVars[v]->bParts );
+ FREE( pVars[v] );
+ }
+ // clean the best var
+ Cudd_RecursiveDeref( dd, pVars[iVarBest]->bParts );
+ FREE( pVars[iVarBest] );
+
+ // combines two nodes
+ pNode = Extra_CombineTwoNodes( dd, bCube, pNode1, pNode2 );
+ Cudd_RecursiveDeref( dd, bCube );
+ }
+ else // if ( pVar->nParts > 2 )
+ {
+ // find two smallest BDDs that have this var
+ Extra_FindBestPartitions( dd, pVar->bParts, nNodes, pNodes, &iNode1, &iNode2 );
+ pNode1 = pNodes[iNode1];
+ pNode2 = pNodes[iNode2];
+
+ // it is not possible that a var appears only in these two
+ // otherwise, it would have a different cost
+ bParts = Cudd_bddAnd( dd, dd->vars[iNode1], dd->vars[iNode2] ); Cudd_Ref( bParts );
+ for ( v = 0; v < nVars; v++ )
+ if ( pVars[v] && pVars[v]->bParts == bParts )
+ assert( 0 );
+ Cudd_RecursiveDeref( dd, bParts );
+
+ // combines two nodes
+ pNode = Extra_CombineTwoNodes( dd, b1, pNode1, pNode2 );
+ }
+
+ // clean the old nodes
+ pNodes[iNode1] = pNode;
+ pNodes[iNode2] = NULL;
+
+ // update the variables that appear in pNode[iNode2]
+ for ( bSuppTemp = pNode2->pPart->bSupp; bSuppTemp != b1; bSuppTemp = cuddT(bSuppTemp) )
+ {
+ pVar = pVars[bSuppTemp->index];
+ if ( pVar == NULL ) // this variable is not be quantified
+ continue;
+ // quantify this var
+ assert( Cudd_bddLeq( dd, pVar->bParts, dd->vars[iNode2] ) );
+ pVar->bParts = Cudd_bddExistAbstract( dd, bTemp = pVar->bParts, dd->vars[iNode2] ); Cudd_Ref( pVar->bParts );
+ Cudd_RecursiveDeref( dd, bTemp );
+ // add the new var
+ pVar->bParts = Cudd_bddAnd( dd, bTemp = pVar->bParts, dd->vars[iNode1] ); Cudd_Ref( pVar->bParts );
+ Cudd_RecursiveDeref( dd, bTemp );
+ // update the score
+ pVar->nParts = Extra_bddSuppSize( dd, pVar->bParts );
+ }
+ return 1;
+}
+
+
+/**Function*************************************************************
+
+ Synopsis [Merges the nodes.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+Extra_ImageNode_t * Extra_MergeTopNodes(
+ DdManager * dd, int nNodes, Extra_ImageNode_t ** pNodes )
+{
+ Extra_ImageNode_t * pNode;
+ int n1 = -1, n2 = -1, n;
+
+ // find the first and the second non-empty spots
+ for ( n = 0; n < nNodes; n++ )
+ if ( pNodes[n] )
+ {
+ if ( n1 == -1 )
+ n1 = n;
+ else if ( n2 == -1 )
+ {
+ n2 = n;
+ break;
+ }
+ }
+ assert( n1 != -1 );
+ // check the situation when only one such node is detected
+ if ( n2 == -1 )
+ {
+ // save the node
+ pNode = pNodes[n1];
+ // clean the node
+ pNodes[n1] = NULL;
+ return pNode;
+ }
+
+ // combines two nodes
+ pNode = Extra_CombineTwoNodes( dd, b1, pNodes[n1], pNodes[n2] );
+
+ // clean the old nodes
+ pNodes[n1] = pNode;
+ pNodes[n2] = NULL;
+ return NULL;
+}
+
+/**Function*************************************************************
+
+ Synopsis [Merges two nodes.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+Extra_ImageNode_t * Extra_CombineTwoNodes( DdManager * dd, DdNode * bCube,
+ Extra_ImageNode_t * pNode1, Extra_ImageNode_t * pNode2 )
+{
+ Extra_ImageNode_t * pNode;
+ Extra_ImagePart_t * pPart;
+
+ // create a new partition
+ pPart = ALLOC( Extra_ImagePart_t, 1 );
+ memset( pPart, 0, sizeof(Extra_ImagePart_t) );
+ // create the function
+ pPart->bFunc = Cudd_bddAndAbstract( dd, pNode1->pPart->bFunc, pNode2->pPart->bFunc, bCube );
+ Cudd_Ref( pPart->bFunc );
+ // update the support the partition
+ pPart->bSupp = Cudd_bddAndAbstract( dd, pNode1->pPart->bSupp, pNode2->pPart->bSupp, bCube );
+ Cudd_Ref( pPart->bSupp );
+ // update the numbers
+ pPart->nSupp = Extra_bddSuppSize( dd, pPart->bSupp );
+ pPart->nNodes = Cudd_DagSize( pPart->bFunc );
+ pPart->iPart = -1;
+/*
+PRB( dd, pNode1->pPart->bSupp );
+PRB( dd, pNode2->pPart->bSupp );
+PRB( dd, pPart->bSupp );
+*/
+ // create a new node
+ pNode = ALLOC( Extra_ImageNode_t, 1 );
+ memset( pNode, 0, sizeof(Extra_ImageNode_t) );
+ pNode->dd = dd;
+ pNode->pPart = pPart;
+ pNode->pNode1 = pNode1;
+ pNode->pNode2 = pNode2;
+ // compute the image
+ pNode->bImage = Cudd_bddAndAbstract( dd, pNode1->bImage, pNode2->bImage, bCube );
+ Cudd_Ref( pNode->bImage );
+ // save the cube
+ if ( bCube != b1 )
+ {
+ pNode->bCube = bCube; Cudd_Ref( bCube );
+ }
+ return pNode;
+}
+
+/**Function*************************************************************
+
+ Synopsis [Computes the best variable.]
+
+ Description [The variables is the best if the sum of squares of the
+ BDD sizes of the partitions, in which it participates, is the minimum.]
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+int Extra_FindBestVariable( DdManager * dd,
+ int nNodes, Extra_ImageNode_t ** pNodes,
+ int nVars, Extra_ImageVar_t ** pVars )
+{
+ DdNode * bTemp;
+ int iVarBest, v;
+ double CostBest, CostCur;
+
+ CostBest = 100000000000000;
+ iVarBest = -1;
+ for ( v = 0; v < nVars; v++ )
+ if ( pVars[v] )
+ {
+ CostCur = 0;
+ for ( bTemp = pVars[v]->bParts; bTemp != b1; bTemp = cuddT(bTemp) )
+ CostCur += pNodes[bTemp->index]->pPart->nNodes *
+ pNodes[bTemp->index]->pPart->nNodes;
+ if ( CostBest > CostCur )
+ {
+ CostBest = CostCur;
+ iVarBest = v;
+ }
+ }
+ return iVarBest;
+}
+
+/**Function*************************************************************
+
+ Synopsis [Computes two smallest partions that have this var.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+void Extra_FindBestPartitions( DdManager * dd, DdNode * bParts,
+ int nNodes, Extra_ImageNode_t ** pNodes,
+ int * piNode1, int * piNode2 )
+{
+ DdNode * bTemp;
+ int iPart1, iPart2;
+ int CostMin1, CostMin2, Cost;
+
+ // go through the partitions
+ iPart1 = iPart2 = -1;
+ CostMin1 = CostMin2 = 1000000;
+ for ( bTemp = bParts; bTemp != b1; bTemp = cuddT(bTemp) )
+ {
+ Cost = pNodes[bTemp->index]->pPart->nNodes;
+ if ( CostMin1 > Cost )
+ {
+ CostMin2 = CostMin1; iPart2 = iPart1;
+ CostMin1 = Cost; iPart1 = bTemp->index;
+ }
+ else if ( CostMin2 > Cost )
+ {
+ CostMin2 = Cost; iPart2 = bTemp->index;
+ }
+ }
+
+ *piNode1 = iPart1;
+ *piNode2 = iPart2;
+}
+
+/**Function*************************************************************
+
+ Synopsis [Prints the latch dependency matrix.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+void Extra_bddImagePrintLatchDependency(
+ DdManager * dd, DdNode * bCare, // the care set
+ int nParts, DdNode ** pbParts, // the partitions for image computation
+ int nVars, DdNode ** pbVars ) // the NS and parameter variables (not quantified!)
+{
+ int i;
+ DdNode * bVarsCs, * bVarsNs;
+
+ bVarsCs = Cudd_Support( dd, bCare ); Cudd_Ref( bVarsCs );
+ bVarsNs = Cudd_bddComputeCube( dd, pbVars, NULL, nVars ); Cudd_Ref( bVarsNs );
+
+ printf( "The latch dependency matrix:\n" );
+ printf( "Partitions = %d Variables: total = %d non-quantifiable = %d\n",
+ nParts, dd->size, nVars );
+ printf( " : " );
+ for ( i = 0; i < dd->size; i++ )
+ printf( "%d", i % 10 );
+ printf( "\n" );
+
+ for ( i = 0; i < nParts; i++ )
+ Extra_bddImagePrintLatchDependencyOne( dd, pbParts[i], bVarsCs, bVarsNs, i );
+ Extra_bddImagePrintLatchDependencyOne( dd, bCare, bVarsCs, bVarsNs, nParts );
+
+ Cudd_RecursiveDeref( dd, bVarsCs );
+ Cudd_RecursiveDeref( dd, bVarsNs );
+}
+
+/**Function*************************************************************
+
+ Synopsis [Prints one row of the latch dependency matrix.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+void Extra_bddImagePrintLatchDependencyOne(
+ DdManager * dd, DdNode * bFunc, // the function
+ DdNode * bVarsCs, DdNode * bVarsNs, // the current/next state vars
+ int iPart )
+{
+ DdNode * bSupport;
+ int v;
+ bSupport = Cudd_Support( dd, bFunc ); Cudd_Ref( bSupport );
+ printf( " %3d : ", iPart );
+ for ( v = 0; v < dd->size; v++ )
+ {
+ if ( Cudd_bddLeq( dd, bSupport, dd->vars[v] ) )
+ {
+ if ( Cudd_bddLeq( dd, bVarsCs, dd->vars[v] ) )
+ printf( "c" );
+ else if ( Cudd_bddLeq( dd, bVarsNs, dd->vars[v] ) )
+ printf( "n" );
+ else
+ printf( "i" );
+ }
+ else
+ printf( "." );
+ }
+ printf( "\n" );
+ Cudd_RecursiveDeref( dd, bSupport );
+}
+
+
+/**Function*************************************************************
+
+ Synopsis [Prints the tree for quenstification scheduling.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+void Extra_bddImagePrintTree( Extra_ImageTree_t * pTree )
+{
+ printf( "The quantification scheduling tree:\n" );
+ Extra_bddImagePrintTree_rec( pTree->pRoot, 1 );
+}
+
+/**Function*************************************************************
+
+ Synopsis [Prints the tree for quenstification scheduling.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+void Extra_bddImagePrintTree_rec( Extra_ImageNode_t * pNode, int Offset )
+{
+ DdNode * Cube;
+ int i;
+
+ Cube = pNode->bCube;
+
+ if ( pNode->pNode1 == NULL )
+ {
+ printf( "<%d> ", pNode->pPart->iPart );
+ if ( Cube != NULL )
+ {
+ PRB( pNode->dd, Cube );
+ }
+ else
+ printf( "\n" );
+ return;
+ }
+
+ printf( "<*> " );
+ if ( Cube != NULL )
+ {
+ PRB( pNode->dd, Cube );
+ }
+ else
+ printf( "\n" );
+
+ for ( i = 0; i < Offset; i++ )
+ printf( " " );
+ Extra_bddImagePrintTree_rec( pNode->pNode1, Offset + 1 );
+
+ for ( i = 0; i < Offset; i++ )
+ printf( " " );
+ Extra_bddImagePrintTree_rec( pNode->pNode2, Offset + 1 );
+}
+
+
+
+
+
+struct Extra_ImageTree2_t_
+{
+ DdManager * dd;
+ DdNode * bRel;
+ DdNode * bCube;
+ DdNode * bImage;
+};
+
+/**Function*************************************************************
+
+ Synopsis [Starts the monolithic image computation.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+Extra_ImageTree2_t * Extra_bddImageStart2(
+ DdManager * dd, DdNode * bCare,
+ int nParts, DdNode ** pbParts,
+ int nVars, DdNode ** pbVars, int fVerbose )
+{
+ Extra_ImageTree2_t * pTree;
+ DdNode * bCubeAll, * bCubeNot, * bTemp;
+ int i;
+
+ pTree = ALLOC( Extra_ImageTree2_t, 1 );
+ pTree->dd = dd;
+ pTree->bImage = NULL;
+
+ bCubeAll = Extra_bddComputeCube( dd, dd->vars, dd->size ); Cudd_Ref( bCubeAll );
+ bCubeNot = Extra_bddComputeCube( dd, pbVars, nVars ); Cudd_Ref( bCubeNot );
+ pTree->bCube = Cudd_bddExistAbstract( dd, bCubeAll, bCubeNot ); Cudd_Ref( pTree->bCube );
+ Cudd_RecursiveDeref( dd, bCubeAll );
+ Cudd_RecursiveDeref( dd, bCubeNot );
+
+ // derive the monolithic relation
+ pTree->bRel = b1; Cudd_Ref( pTree->bRel );
+ for ( i = 0; i < nParts; i++ )
+ {
+ pTree->bRel = Cudd_bddAnd( dd, bTemp = pTree->bRel, pbParts[i] ); Cudd_Ref( pTree->bRel );
+ Cudd_RecursiveDeref( dd, bTemp );
+ }
+ Extra_bddImageCompute2( pTree, bCare );
+ return pTree;
+}
+
+
+/**Function*************************************************************
+
+ Synopsis []
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+DdNode * Extra_bddImageCompute2( Extra_ImageTree2_t * pTree, DdNode * bCare )
+{
+ if ( pTree->bImage )
+ Cudd_RecursiveDeref( pTree->dd, pTree->bImage );
+ pTree->bImage = Cudd_bddAndAbstract( pTree->dd, pTree->bRel, bCare, pTree->bCube );
+ Cudd_Ref( pTree->bImage );
+ return pTree->bImage;
+}
+
+/**Function*************************************************************
+
+ Synopsis []
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+void Extra_bddImageTreeDelete2( Extra_ImageTree2_t * pTree )
+{
+ if ( pTree->bRel )
+ Cudd_RecursiveDeref( pTree->dd, pTree->bRel );
+ if ( pTree->bCube )
+ Cudd_RecursiveDeref( pTree->dd, pTree->bCube );
+ if ( pTree->bImage )
+ Cudd_RecursiveDeref( pTree->dd, pTree->bImage );
+ FREE( pTree );
+}
+
+/**Function*************************************************************
+
+ Synopsis [Returns the previously computed image.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+DdNode * Extra_bddImageRead2( Extra_ImageTree2_t * pTree )
+{
+ return pTree->bImage;
+}
+
+
+////////////////////////////////////////////////////////////////////////
+/// END OF FILE ///
+////////////////////////////////////////////////////////////////////////
+
+
diff --git a/src/misc/extra/extraBddMisc.c b/src/misc/extra/extraBddMisc.c
index e4790325..023a9841 100644
--- a/src/misc/extra/extraBddMisc.c
+++ b/src/misc/extra/extraBddMisc.c
@@ -961,6 +961,34 @@ void Extra_bddPermuteArray( DdManager * manager, DdNode ** bNodesIn, DdNode ** b
} /* end of Extra_bddPermuteArray */
+/**Function********************************************************************
+
+ Synopsis [Computes the positive polarty cube composed of the first vars in the array.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+******************************************************************************/
+DdNode * Extra_bddComputeCube( DdManager * dd, DdNode ** bXVars, int nVars )
+{
+ DdNode * bRes;
+ DdNode * bTemp;
+ int i;
+
+ bRes = b1; Cudd_Ref( bRes );
+ for ( i = 0; i < nVars; i++ )
+ {
+ bRes = Cudd_bddAnd( dd, bTemp = bRes, bXVars[i] ); Cudd_Ref( bRes );
+ Cudd_RecursiveDeref( dd, bTemp );
+ }
+
+ Cudd_Deref( bRes );
+ return bRes;
+}
+
/*---------------------------------------------------------------------------*/
/* Definition of internal functions */
/*---------------------------------------------------------------------------*/
diff --git a/src/misc/extra/module.make b/src/misc/extra/module.make
index ec8bca4d..c7c9be4e 100644
--- a/src/misc/extra/module.make
+++ b/src/misc/extra/module.make
@@ -1,5 +1,6 @@
SRC += src/misc/extra/extraBddAuto.c \
src/misc/extra/extraBddCas.c \
+ src/misc/extra/extraBddImage.c \
src/misc/extra/extraBddKmap.c \
src/misc/extra/extraBddMisc.c \
src/misc/extra/extraBddSymm.c \
diff --git a/src/opt/mfs/mfsCore.c b/src/opt/mfs/mfsCore.c
index 7104d3b3..a941f153 100644
--- a/src/opt/mfs/mfsCore.c
+++ b/src/opt/mfs/mfsCore.c
@@ -241,21 +241,23 @@ int Abc_NtkMfs( Abc_Ntk_t * pNtk, Mfs_Par_t * pPars )
if ( pNtk->pExcare )
{
Abc_Ntk_t * pTemp;
- pTemp = Abc_NtkStrash( pNtk->pExcare, 0, 0, 0 );
- p->pCare = Abc_NtkToDar( pTemp, 0 );
- Abc_NtkDelete( pTemp );
- p->vSuppsInv = Aig_ManSupportsInverse( p->pCare );
- }
-// if ( pPars->fVerbose )
- {
- if ( p->pCare != NULL )
- printf( "Performing optimization with %d external care clauses.\n", Aig_ManPoNum(p->pCare) );
-// else
-// printf( "Performing optimization without constraints.\n" );
+ if ( Abc_NtkPiNum(pNtk->pExcare) != Abc_NtkCiNum(pNtk) )
+ printf( "The PI count of careset (%d) and logic network (%d) differ. Careset is not used.\n",
+ Abc_NtkPiNum(pNtk->pExcare), Abc_NtkCiNum(pNtk) );
+ else
+ {
+ pTemp = Abc_NtkStrash( pNtk->pExcare, 0, 0, 0 );
+ p->pCare = Abc_NtkToDar( pTemp, 0 );
+ Abc_NtkDelete( pTemp );
+ p->vSuppsInv = Aig_ManSupportsInverse( p->pCare );
+ }
}
+ if ( p->pCare != NULL )
+ printf( "Performing optimization with %d external care clauses.\n", Aig_ManPoNum(p->pCare) );
+ // prepare the BDC manager
if ( !pPars->fResub )
{
- pDecPars->nVarsMax = nFaninMax;
+ pDecPars->nVarsMax = (nFaninMax < 3) ? 3 : nFaninMax;
pDecPars->fVerbose = pPars->fVerbose;
p->vTruth = Vec_IntAlloc( 0 );
p->pManDec = Bdc_ManAlloc( pDecPars );
generated by cgit v1.2.3 (git 2.25.1) at 2024-07-01 01:51:38 +0000