summaryrefslogtreecommitdiffstats
path: root/src
diff options
context:
space:
mode:
Diffstat (limited to 'src')
-rw-r--r--src/aig/aig/aigRepr.c11
-rw-r--r--src/aig/dar/darScript.c80
-rw-r--r--src/aig/dch/dch.h18
-rw-r--r--src/aig/dch/dchChoice.c86
-rw-r--r--src/aig/dch/dchClass.c21
-rw-r--r--src/aig/dch/dchCnf.c52
-rw-r--r--src/aig/dch/dchCore.c16
-rw-r--r--src/aig/dch/dchInt.h19
-rw-r--r--src/aig/dch/dchMan.c41
-rw-r--r--src/aig/dch/dchSat.c15
-rw-r--r--src/aig/dch/dchSim.c39
-rw-r--r--src/aig/dch/dchSimSat.c243
-rw-r--r--src/aig/dch/dchSweep.c158
-rw-r--r--src/aig/dch/module.make1
-rw-r--r--src/aig/ntl/ntlCore.c20
-rw-r--r--src/base/abci/abc.c133
16 files changed, 694 insertions, 259 deletions
diff --git a/src/aig/aig/aigRepr.c b/src/aig/aig/aigRepr.c
index 9fb9b9e6..7a092c0f 100644
--- a/src/aig/aig/aigRepr.c
+++ b/src/aig/aig/aigRepr.c
@@ -473,17 +473,11 @@ void Aig_ManMarkValidChoices( Aig_Man_t * p )
{
Aig_Obj_t * pObj, * pRepr;
int i;
- int nReprs, nEquivs;
-
-extern int Dch_DeriveChoiceCountReprs( Aig_Man_t * pAig );
-extern int Dch_DeriveChoiceCountEquivs( Aig_Man_t * pAig );
-
assert( p->pReprs != NULL );
// create equivalent nodes in the manager
assert( p->pEquivs == NULL );
p->pEquivs = ALLOC( Aig_Obj_t *, Aig_ManObjNumMax(p) );
memset( p->pEquivs, 0, sizeof(Aig_Obj_t *) * Aig_ManObjNumMax(p) );
-
// make the choice nodes
Aig_ManForEachNode( p, pObj, i )
{
@@ -513,11 +507,6 @@ extern int Dch_DeriveChoiceCountEquivs( Aig_Man_t * pAig );
p->pEquivs[pObj->Id] = p->pEquivs[pRepr->Id];
p->pEquivs[pRepr->Id] = pObj;
}
-
- nReprs = Dch_DeriveChoiceCountReprs( p );
- nEquivs = Dch_DeriveChoiceCountEquivs( p );
- printf( "\nReprs = %d. Equivs = %d. Choices = %d.\n",
- nReprs, nEquivs, Aig_ManCountChoices(p) );
}
diff --git a/src/aig/dar/darScript.c b/src/aig/dar/darScript.c
index b27addd4..d82239f8 100644
--- a/src/aig/dar/darScript.c
+++ b/src/aig/dar/darScript.c
@@ -416,6 +416,86 @@ PRT( "Choicing time ", clock() - clk );
// return NULL;
}
+#include "dch.h"
+
+/**Function*************************************************************
+
+ Synopsis [Reproduces script "compress2".]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+Aig_Man_t * Dar_ManChoiceNew( Aig_Man_t * pAig, Dch_Pars_t * pPars )
+{
+ extern Aig_Man_t * Dch_ComputeChoices( Vec_Ptr_t * vAigs, Dch_Pars_t * pPars );
+
+ int fVerbose = pPars->fVerbose;
+ int fConstruct = 0;
+ Aig_Man_t * pMan, * pTemp;
+ Vec_Ptr_t * vAigs;
+ int i, clk;
+
+clk = clock();
+// vAigs = Dar_ManChoiceSynthesisExt();
+ vAigs = Dar_ManChoiceSynthesis( pAig, 1, 1, fVerbose );
+
+ // swap the first and last network
+ // this should lead to the primary choice being "better" because of synthesis
+ // (it is also important when constructing choices)
+ if ( !fConstruct )
+ {
+ pMan = Vec_PtrPop( vAigs );
+ Vec_PtrPush( vAigs, Vec_PtrEntry(vAigs,0) );
+ Vec_PtrWriteEntry( vAigs, 0, pMan );
+ }
+
+if ( fVerbose )
+{
+PRT( "Synthesis time", clock() - clk );
+}
+// pPars->timeSynth = clock() - clk;
+
+clk = clock();
+/*
+ if ( fConstruct )
+ pMan = Aig_ManChoiceConstructive( vAigs, fVerbose );
+ else
+ pMan = Aig_ManChoicePartitioned( vAigs, 300, nConfMax, nLevelMax, fVerbose );
+*/
+ pMan = Dch_ComputeChoices( vAigs, pPars );
+
+ // reconstruct the network
+ pMan = Aig_ManDupDfsGuided( pTemp = pMan, Vec_PtrEntry(vAigs,0) );
+ Aig_ManStop( pTemp );
+ // duplicate the timing manager
+ pTemp = Vec_PtrEntry( vAigs, 0 );
+ if ( pTemp->pManTime )
+ {
+ extern void * Tim_ManDup( void * p, int fDiscrete );
+ pMan->pManTime = Tim_ManDup( pTemp->pManTime, 0 );
+ }
+ // reset levels
+ Aig_ManChoiceLevel( pMan );
+ pMan->pName = Aig_UtilStrsav( pTemp->pName );
+ pMan->pSpec = Aig_UtilStrsav( pTemp->pSpec );
+
+ // cleanup
+ Vec_PtrForEachEntry( vAigs, pTemp, i )
+ Aig_ManStop( pTemp );
+ Vec_PtrFree( vAigs );
+
+if ( fVerbose )
+{
+//PRT( "Choicing time ", clock() - clk );
+}
+ return pMan;
+// return NULL;
+}
+
////////////////////////////////////////////////////////////////////////
/// END OF FILE ///
////////////////////////////////////////////////////////////////////////
diff --git a/src/aig/dch/dch.h b/src/aig/dch/dch.h
index 9f6cfdca..f1718a78 100644
--- a/src/aig/dch/dch.h
+++ b/src/aig/dch/dch.h
@@ -1,6 +1,6 @@
/**CFile****************************************************************
- FileName [dch.h]
+ FileName [dch.h]
SystemName [ABC: Logic synthesis and verification system.]
@@ -41,12 +41,16 @@ extern "C" {
typedef struct Dch_Pars_t_ Dch_Pars_t;
struct Dch_Pars_t_
{
- int nWords; // the number of simulation words
- int nBTLimit; // conflict limit at a node
- int nSatVarMax; // the max number of SAT variables
- int fSynthesis; // set to 1 to perform synthesis
- int fVerbose; // verbose stats
- int timeSynth; // synthesis runtime
+ int nWords; // the number of simulation words
+ int nBTLimit; // conflict limit at a node
+ int nSatVarMax; // the max number of SAT variables
+ int fSynthesis; // set to 1 to perform synthesis
+ int fPolarFlip; // uses polarity adjustment
+ int fSimulateTfo; // uses simulatin of TFO classes
+ int fVerbose; // verbose stats
+ int timeSynth; // synthesis runtime
+ int nNodesAhead; // the lookahead in terms of nodes
+ int nCallsRecycle; // calls to perform before recycling SAT solver
};
////////////////////////////////////////////////////////////////////////
diff --git a/src/aig/dch/dchChoice.c b/src/aig/dch/dchChoice.c
index fe069fef..09bbf2fb 100644
--- a/src/aig/dch/dchChoice.c
+++ b/src/aig/dch/dchChoice.c
@@ -67,18 +67,27 @@ int Dch_DeriveChoiceCountReprs( Aig_Man_t * pAig )
***********************************************************************/
int Dch_DeriveChoiceCountEquivs( Aig_Man_t * pAig )
{
- Aig_Obj_t * pObj, * pTemp;
- int i, nEquivs = 0;
+ Aig_Obj_t * pObj, * pTemp, * pPrev;
+ int i, nEquivs = 0, Counter = 0;
Aig_ManForEachObj( pAig, pObj, i )
{
if ( !Aig_ObjIsChoice(pAig, pObj) )
continue;
- for ( pTemp = Aig_ObjEquiv(pAig, pObj); pTemp; pTemp = Aig_ObjEquiv(pAig, pTemp) )
+ for ( pPrev = pObj, pTemp = Aig_ObjEquiv(pAig, pObj); pTemp;
+ pPrev = pTemp, pTemp = Aig_ObjEquiv(pAig, pTemp) )
{
- assert( pTemp->nRefs == 0 );
+ if ( pTemp->nRefs > 0 )
+ {
+ // remove referenced node from equivalence class
+ assert( pAig->pEquivs[pPrev->Id] == pTemp );
+ pAig->pEquivs[pPrev->Id] = pAig->pEquivs[pTemp->Id];
+ Counter++;
+ }
nEquivs++;
}
}
+// if ( Counter )
+// printf( "Removed %d equiv nodes because of non-zero ref counter.\n", Counter );
return nEquivs;
}
@@ -146,51 +155,6 @@ int Dch_ObjCheckTfi( Aig_Man_t * p, Aig_Obj_t * pObj, Aig_Obj_t * pRepr )
/**Function*************************************************************
- Synopsis [Derives the AIG with choices from representatives.]
-
- Description []
-
- SideEffects []
-
- SeeAlso []
-
-***********************************************************************/
-void Dch_DeriveChoiceAig_rec( Aig_Man_t * pAigNew, Aig_Man_t * pAigOld, Aig_Obj_t * pObj )
-{
- Aig_Obj_t * pRepr, * pObjNew, * pReprNew;
- if ( pObj->pData )
- return;
- // construct AIG for the representative
- if ( (pRepr = Aig_ObjRepr(pAigOld, pObj)) )
- Dch_DeriveChoiceAig_rec( pAigNew, pAigOld, pRepr );
- // construct AIG for the fanins
- Dch_DeriveChoiceAig_rec( pAigNew, pAigOld, Aig_ObjFanin0(pObj) );
- Dch_DeriveChoiceAig_rec( pAigNew, pAigOld, Aig_ObjFanin1(pObj) );
- pObj->pData = Aig_And( pAigNew, Aig_ObjChild0Copy(pObj), Aig_ObjChild1Copy(pObj) );
- if ( pRepr == NULL )
- return;
- // get the corresponding new nodes
- pObjNew = Aig_Regular(pObj->pData);
- pReprNew = Aig_Regular(pRepr->pData);
- if ( pObjNew == pReprNew )
- return;
- assert( pObjNew->nRefs == 0 );
- // update new nodes of the object
- pObj->pData = Aig_NotCond( pRepr->pData, pObj->fPhase ^ pRepr->fPhase );
- if ( !Aig_ObjIsNode(pRepr) )
- return;
- // skip choices with combinational loops
- if ( Dch_ObjCheckTfi( pAigNew, pObjNew, pReprNew ) )
-// if ( Aig_ObjCheckTfi( pAigNew, pObjNew, pReprNew ) )
- return;
- // add choice
- pAigNew->pEquivs[pObjNew->Id] = pAigNew->pEquivs[pReprNew->Id];
- pAigNew->pEquivs[pReprNew->Id] = pObjNew;
-}
-
-
-/**Function*************************************************************
-
Synopsis [Returns representatives of fanin in approapriate polarity.]
Description []
@@ -237,19 +201,24 @@ void Dch_DeriveChoiceAigNode( Aig_Man_t * pAigNew, Aig_Man_t * pAigOld, Aig_Obj_
pReprNew = Aig_Regular(pRepr->pData);
if ( pObjNew == pReprNew )
return;
-// assert( pObjNew->nRefs == 0 );
+ // skip the earlier nodes
+ if ( pReprNew->Id > pObjNew->Id )
+ return;
+ assert( pReprNew->Id < pObjNew->Id );
// set the representatives
Aig_ObjSetRepr( pAigNew, pObjNew, pReprNew );
+ // skip used nodes
+ if ( pObjNew->nRefs > 0 )
+ return;
+ assert( pObjNew->nRefs == 0 );
// update new nodes of the object
if ( !Aig_ObjIsNode(pRepr) )
return;
- if ( pObjNew->nRefs > 0 )
- return;
// skip choices with combinational loops
if ( Dch_ObjCheckTfi( pAigNew, pObjNew, pReprNew ) )
return;
// add choice
- pAigNew->pEquivs[pObjNew->Id] = pAigNew->pEquivs[pReprNew->Id];
+ pAigNew->pEquivs[pObjNew->Id] = pAigNew->pEquivs[pReprNew->Id];
pAigNew->pEquivs[pReprNew->Id] = pObjNew;
}
@@ -272,21 +241,14 @@ Aig_Man_t * Dch_DeriveChoiceAig( Aig_Man_t * pAig )
// start recording equivalences
pChoices = Aig_ManStart( Aig_ManObjNumMax(pAig) );
pChoices->pEquivs = CALLOC( Aig_Obj_t *, Aig_ManObjNumMax(pAig) );
- pChoices->pReprs = CALLOC( Aig_Obj_t *, Aig_ManObjNumMax(pAig) );
+ pChoices->pReprs = CALLOC( Aig_Obj_t *, Aig_ManObjNumMax(pAig) );
// map constants and PIs
Aig_ManCleanData( pAig );
Aig_ManConst1(pAig)->pData = Aig_ManConst1(pChoices);
Aig_ManForEachPi( pAig, pObj, i )
pObj->pData = Aig_ObjCreatePi( pChoices );
- // construct choice nodes from the POs
+ // construct choices for the internal nodes
assert( pAig->pReprs != NULL );
-/*
- Aig_ManForEachPo( pAig, pObj, i )
- {
- Dch_DeriveChoiceAig_rec( pChoices, pAig, Aig_ObjFanin0(pObj) );
- Aig_ObjCreatePo( pChoices, Aig_ObjChild0Copy(pObj) );
- }
-*/
Aig_ManForEachNode( pAig, pObj, i )
Dch_DeriveChoiceAigNode( pChoices, pAig, pObj );
Aig_ManForEachPo( pAig, pObj, i )
diff --git a/src/aig/dch/dchClass.c b/src/aig/dch/dchClass.c
index 5d192195..ab306ca9 100644
--- a/src/aig/dch/dchClass.c
+++ b/src/aig/dch/dchClass.c
@@ -26,7 +26,7 @@
The first node of the class is its representative node.
The representative has the smallest topological order among the class nodes.
The nodes inside each class are ordered according to their topological order.
- The classes are ordered according to the topological order of their representatives.
+ The classes are ordered according to the topo order of their representatives.
*/
// internal representation of candidate equivalence classes
@@ -207,6 +207,25 @@ int Dch_ClassesLitNum( Dch_Cla_t * p )
/**Function*************************************************************
+ Synopsis [Stop representation of equivalence classes.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+Aig_Obj_t ** Dch_ClassesReadClass( Dch_Cla_t * p, Aig_Obj_t * pRepr, int * pnSize )
+{
+ assert( p->pId2Class[pRepr->Id] != NULL );
+ assert( p->pClassSizes[pRepr->Id] > 1 );
+ *pnSize = p->pClassSizes[pRepr->Id];
+ return p->pId2Class[pRepr->Id];
+}
+
+/**Function*************************************************************
+
Synopsis [Checks candidate equivalence classes.]
Description []
diff --git a/src/aig/dch/dchCnf.c b/src/aig/dch/dchCnf.c
index 6533ca81..dc822d77 100644
--- a/src/aig/dch/dchCnf.c
+++ b/src/aig/dch/dchCnf.c
@@ -68,21 +68,45 @@ void Dch_AddClausesMux( Dch_Man_t * p, Aig_Obj_t * pNode )
pLits[0] = toLitCond(VarI, 1);
pLits[1] = toLitCond(VarT, 1^fCompT);
pLits[2] = toLitCond(VarF, 0);
+ if ( p->pPars->fPolarFlip )
+ {
+ if ( pNodeI->fPhase ) pLits[0] = lit_neg( pLits[0] );
+ if ( Aig_Regular(pNodeT)->fPhase ) pLits[1] = lit_neg( pLits[1] );
+ if ( pNode->fPhase ) pLits[2] = lit_neg( pLits[2] );
+ }
RetValue = sat_solver_addclause( p->pSat, pLits, pLits + 3 );
assert( RetValue );
pLits[0] = toLitCond(VarI, 1);
pLits[1] = toLitCond(VarT, 0^fCompT);
pLits[2] = toLitCond(VarF, 1);
+ if ( p->pPars->fPolarFlip )
+ {
+ if ( pNodeI->fPhase ) pLits[0] = lit_neg( pLits[0] );
+ if ( Aig_Regular(pNodeT)->fPhase ) pLits[1] = lit_neg( pLits[1] );
+ if ( pNode->fPhase ) pLits[2] = lit_neg( pLits[2] );
+ }
RetValue = sat_solver_addclause( p->pSat, pLits, pLits + 3 );
assert( RetValue );
pLits[0] = toLitCond(VarI, 0);
pLits[1] = toLitCond(VarE, 1^fCompE);
pLits[2] = toLitCond(VarF, 0);
+ if ( p->pPars->fPolarFlip )
+ {
+ if ( pNodeI->fPhase ) pLits[0] = lit_neg( pLits[0] );
+ if ( Aig_Regular(pNodeE)->fPhase ) pLits[1] = lit_neg( pLits[1] );
+ if ( pNode->fPhase ) pLits[2] = lit_neg( pLits[2] );
+ }
RetValue = sat_solver_addclause( p->pSat, pLits, pLits + 3 );
assert( RetValue );
pLits[0] = toLitCond(VarI, 0);
pLits[1] = toLitCond(VarE, 0^fCompE);
pLits[2] = toLitCond(VarF, 1);
+ if ( p->pPars->fPolarFlip )
+ {
+ if ( pNodeI->fPhase ) pLits[0] = lit_neg( pLits[0] );
+ if ( Aig_Regular(pNodeE)->fPhase ) pLits[1] = lit_neg( pLits[1] );
+ if ( pNode->fPhase ) pLits[2] = lit_neg( pLits[2] );
+ }
RetValue = sat_solver_addclause( p->pSat, pLits, pLits + 3 );
assert( RetValue );
@@ -102,11 +126,23 @@ void Dch_AddClausesMux( Dch_Man_t * p, Aig_Obj_t * pNode )
pLits[0] = toLitCond(VarT, 0^fCompT);
pLits[1] = toLitCond(VarE, 0^fCompE);
pLits[2] = toLitCond(VarF, 1);
+ if ( p->pPars->fPolarFlip )
+ {
+ if ( Aig_Regular(pNodeT)->fPhase ) pLits[0] = lit_neg( pLits[0] );
+ if ( Aig_Regular(pNodeE)->fPhase ) pLits[1] = lit_neg( pLits[1] );
+ if ( pNode->fPhase ) pLits[2] = lit_neg( pLits[2] );
+ }
RetValue = sat_solver_addclause( p->pSat, pLits, pLits + 3 );
assert( RetValue );
pLits[0] = toLitCond(VarT, 1^fCompT);
pLits[1] = toLitCond(VarE, 1^fCompE);
pLits[2] = toLitCond(VarF, 0);
+ if ( p->pPars->fPolarFlip )
+ {
+ if ( Aig_Regular(pNodeT)->fPhase ) pLits[0] = lit_neg( pLits[0] );
+ if ( Aig_Regular(pNodeE)->fPhase ) pLits[1] = lit_neg( pLits[1] );
+ if ( pNode->fPhase ) pLits[2] = lit_neg( pLits[2] );
+ }
RetValue = sat_solver_addclause( p->pSat, pLits, pLits + 3 );
assert( RetValue );
}
@@ -137,13 +173,28 @@ void Dch_AddClausesSuper( Dch_Man_t * p, Aig_Obj_t * pNode, Vec_Ptr_t * vSuper )
{
pLits[0] = toLitCond(Dch_ObjSatNum(p,Aig_Regular(pFanin)), Aig_IsComplement(pFanin));
pLits[1] = toLitCond(Dch_ObjSatNum(p,pNode), 1);
+ if ( p->pPars->fPolarFlip )
+ {
+ if ( Aig_Regular(pFanin)->fPhase ) pLits[0] = lit_neg( pLits[0] );
+ if ( pNode->fPhase ) pLits[1] = lit_neg( pLits[1] );
+ }
RetValue = sat_solver_addclause( p->pSat, pLits, pLits + 2 );
assert( RetValue );
}
// add A & B => C or !A + !B + C
Vec_PtrForEachEntry( vSuper, pFanin, i )
+ {
pLits[i] = toLitCond(Dch_ObjSatNum(p,Aig_Regular(pFanin)), !Aig_IsComplement(pFanin));
+ if ( p->pPars->fPolarFlip )
+ {
+ if ( Aig_Regular(pFanin)->fPhase ) pLits[i] = lit_neg( pLits[i] );
+ }
+ }
pLits[nLits-1] = toLitCond(Dch_ObjSatNum(p,pNode), 0);
+ if ( p->pPars->fPolarFlip )
+ {
+ if ( pNode->fPhase ) pLits[nLits-1] = lit_neg( pLits[nLits-1] );
+ }
RetValue = sat_solver_addclause( p->pSat, pLits, pLits + nLits );
assert( RetValue );
free( pLits );
@@ -213,6 +264,7 @@ void Dch_ObjAddToFrontier( Dch_Man_t * p, Aig_Obj_t * pObj, Vec_Ptr_t * vFrontie
assert( Dch_ObjSatNum(p,pObj) == 0 );
if ( Aig_ObjIsConst1(pObj) )
return;
+ Vec_PtrPush( p->vUsedNodes, pObj );
Dch_ObjSetSatNum( p, pObj, p->nSatVars++ );
if ( Aig_ObjIsNode(pObj) )
Vec_PtrPush( vFrontier, pObj );
diff --git a/src/aig/dch/dchCore.c b/src/aig/dch/dchCore.c
index b73fceb3..76813d1a 100644
--- a/src/aig/dch/dchCore.c
+++ b/src/aig/dch/dchCore.c
@@ -42,11 +42,15 @@
void Dch_ManSetDefaultParams( Dch_Pars_t * p )
{
memset( p, 0, sizeof(Dch_Pars_t) );
- p->nWords = 4; // the number of simulation words
- p->nBTLimit = 100; // conflict limit at a node
- p->nSatVarMax = 10000; // the max number of SAT variables
- p->fSynthesis = 1; // derives three snapshots
- p->fVerbose = 1; // verbose stats
+ p->nWords = 8; // the number of simulation words
+ p->nBTLimit = 1000; // conflict limit at a node
+ p->nSatVarMax = 5000; // the max number of SAT variables
+ p->fSynthesis = 1; // derives three snapshots
+ p->fPolarFlip = 1; // uses polarity adjustment
+ p->fSimulateTfo = 1; // simulate TFO
+ p->fVerbose = 0; // verbose stats
+ p->nNodesAhead = 1000; // the lookahead in terms of nodes
+ p->nCallsRecycle = 100; // calls to perform before recycling SAT solver
}
/**Function*************************************************************
@@ -66,6 +70,8 @@ Aig_Man_t * Dch_ComputeChoices( Vec_Ptr_t * vAigs, Dch_Pars_t * pPars )
Aig_Man_t * pResult;
int clk, clkTotal = clock();
assert( Vec_PtrSize(vAigs) > 0 );
+ // reset random numbers
+ Aig_ManRandom(1);
// start the choicing manager
p = Dch_ManCreate( vAigs, pPars );
// compute candidate equivalence classes
diff --git a/src/aig/dch/dchInt.h b/src/aig/dch/dchInt.h
index a71cba69..e9a6f2e4 100644
--- a/src/aig/dch/dchInt.h
+++ b/src/aig/dch/dchInt.h
@@ -63,8 +63,10 @@ struct Dch_Man_t_
int * pSatVars; // mapping of each node into its SAT var
Vec_Ptr_t * vUsedNodes; // nodes whose SAT vars are assigned
int nRecycles; // the number of times SAT solver was recycled
+ int nCallsSince; // the number of calls since the last recycle
Vec_Ptr_t * vFanins; // fanins of the CNF node
- Vec_Ptr_t * vRoots; // the roots of the current equiv class
+ Vec_Ptr_t * vSimRoots; // the roots of cand const 1 nodes to simulate
+ Vec_Ptr_t * vSimClasses; // the roots of cand equiv classes to simulate
// solver cone size
int nConeThis;
int nConeMax;
@@ -95,6 +97,12 @@ struct Dch_Man_t_
/// MACRO DEFINITIONS ///
////////////////////////////////////////////////////////////////////////
+static inline int Dch_ObjSatNum( Dch_Man_t * p, Aig_Obj_t * pObj ) { return p->pSatVars[pObj->Id]; }
+static inline void Dch_ObjSetSatNum( Dch_Man_t * p, Aig_Obj_t * pObj, int Num ) { p->pSatVars[pObj->Id] = Num; }
+
+static inline Aig_Obj_t * Dch_ObjFraig( Aig_Obj_t * pObj ) { return pObj->pData; }
+static inline void Dch_ObjSetFraig( Aig_Obj_t * pObj, Aig_Obj_t * pNode ) { pObj->pData = pNode; }
+
static inline int Dch_ObjIsConst1Cand( Aig_Man_t * pAig, Aig_Obj_t * pObj )
{
return Aig_ObjRepr(pAig, pObj) == Aig_ManConst1(pAig);
@@ -105,9 +113,6 @@ static inline void Dch_ObjSetConst1Cand( Aig_Man_t * pAig, Aig_Obj_t * pObj )
Aig_ObjSetRepr( pAig, pObj, Aig_ManConst1(pAig) );
}
-static inline int Dch_ObjSatNum( Dch_Man_t * p, Aig_Obj_t * pObj ) { return p->pSatVars[pObj->Id]; }
-static inline void Dch_ObjSetSatNum( Dch_Man_t * p, Aig_Obj_t * pObj, int Num ) { p->pSatVars[pObj->Id] = Num; }
-
////////////////////////////////////////////////////////////////////////
/// FUNCTION DECLARATIONS ///
////////////////////////////////////////////////////////////////////////
@@ -126,6 +131,7 @@ extern void Dch_ClassesSetData( Dch_Cla_t * p, void * pManData,
int (*pFuncNodesAreEqual)(void *,Aig_Obj_t *, Aig_Obj_t *) );
extern void Dch_ClassesStop( Dch_Cla_t * p );
extern int Dch_ClassesLitNum( Dch_Cla_t * p );
+extern Aig_Obj_t ** Dch_ClassesReadClass( Dch_Cla_t * p, Aig_Obj_t * pRepr, int * pnSize );
extern void Dch_ClassesPrint( Dch_Cla_t * p, int fVeryVerbose );
extern void Dch_ClassesPrepare( Dch_Cla_t * p, int fLatchCorr, int nMaxLevs );
extern int Dch_ClassesRefine( Dch_Cla_t * p );
@@ -143,7 +149,10 @@ extern void Dch_ManSatSolverRecycle( Dch_Man_t * p );
extern int Dch_NodesAreEquiv( Dch_Man_t * p, Aig_Obj_t * pObj1, Aig_Obj_t * pObj2 );
/*=== dchSim.c ===================================================*/
extern Dch_Cla_t * Dch_CreateCandEquivClasses( Aig_Man_t * pAig, int nWords, int fVerbose );
-/*=== dchSim.c ===================================================*/
+/*=== dchSimSat.c ===================================================*/
+extern void Dch_ManResimulateCex( Dch_Man_t * p, Aig_Obj_t * pObj, Aig_Obj_t * pRepr );
+extern void Dch_ManResimulateCex2( Dch_Man_t * p, Aig_Obj_t * pObj, Aig_Obj_t * pRepr );
+/*=== dchSweep.c ===================================================*/
extern void Dch_ManSweep( Dch_Man_t * p );
#ifdef __cplusplus
diff --git a/src/aig/dch/dchMan.c b/src/aig/dch/dchMan.c
index 6a0eecfe..02d91ca3 100644
--- a/src/aig/dch/dchMan.c
+++ b/src/aig/dch/dchMan.c
@@ -45,15 +45,17 @@ Dch_Man_t * Dch_ManCreate( Vec_Ptr_t * vAigs, Dch_Pars_t * pPars )
// create interpolation manager
p = ALLOC( Dch_Man_t, 1 );
memset( p, 0, sizeof(Dch_Man_t) );
- p->pPars = pPars;
- p->vAigs = vAigs;
- p->pAigTotal = Dch_DeriveTotalAig( vAigs );
+ p->pPars = pPars;
+ p->vAigs = vAigs;
+ p->pAigTotal = Dch_DeriveTotalAig( vAigs );
+ Aig_ManFanoutStart( p->pAigTotal );
// SAT solving
- p->nSatVars = 1;
- p->pSatVars = CALLOC( int, Aig_ManObjNumMax(p->pAigTotal) );
- p->vUsedNodes = Vec_PtrAlloc( 1000 );
- p->vFanins = Vec_PtrAlloc( 100 );
- p->vRoots = Vec_PtrAlloc( 1000 );
+ p->nSatVars = 1;
+ p->pSatVars = CALLOC( int, Aig_ManObjNumMax(p->pAigTotal) );
+ p->vUsedNodes = Vec_PtrAlloc( 1000 );
+ p->vFanins = Vec_PtrAlloc( 100 );
+ p->vSimRoots = Vec_PtrAlloc( 1000 );
+ p->vSimClasses = Vec_PtrAlloc( 1000 );
// equivalences proved
p->pReprsProved = CALLOC( Aig_Obj_t *, Aig_ManObjNumMax(p->pAigTotal) );
return p;
@@ -73,10 +75,7 @@ Dch_Man_t * Dch_ManCreate( Vec_Ptr_t * vAigs, Dch_Pars_t * pPars )
void Dch_ManPrintStats( Dch_Man_t * p )
{
// Aig_Man_t * pAig;
- int i;
- for ( i = 0; i < 85; i++ )
- printf( " " );
- printf( "\r" );
+// int i;
// printf( "Choicing will be performed with %d AIGs:\n", Vec_PtrSize(p->vAigs) );
// Vec_PtrForEachEntry( p->vAigs, pAig, i )
// Aig_ManPrintStats( pAig );
@@ -94,7 +93,7 @@ void Dch_ManPrintStats( Dch_Man_t * p )
p->nSatCallsSat, p->nSatFailsReal );
printf( "Choices : Lits = %6d. Reprs = %5d. Equivs = %5d. Choices = %5d.\n",
p->nLits, p->nReprs, p->nEquivs, p->nChoices );
- printf( "Runtime statistics:\n" );
+ printf( "Choicing runtime statistics:\n" );
p->timeOther = p->timeTotal-p->timeSimInit-p->timeSimSat-p->timeSat-p->timeChoice;
PRTP( "Sim init ", p->timeSimInit, p->timeTotal );
PRTP( "Sim SAT ", p->timeSimSat, p->timeTotal );
@@ -105,7 +104,10 @@ void Dch_ManPrintStats( Dch_Man_t * p )
PRTP( "Choice ", p->timeChoice, p->timeTotal );
PRTP( "Other ", p->timeOther, p->timeTotal );
PRTP( "TOTAL ", p->timeTotal, p->timeTotal );
+ if ( p->pPars->timeSynth )
+ {
PRT( "Synthesis ", p->pPars->timeSynth );
+ }
}
/**Function*************************************************************
@@ -133,7 +135,8 @@ void Dch_ManStop( Dch_Man_t * p )
sat_solver_delete( p->pSat );
Vec_PtrFree( p->vUsedNodes );
Vec_PtrFree( p->vFanins );
- Vec_PtrFree( p->vRoots );
+ Vec_PtrFree( p->vSimRoots );
+ Vec_PtrFree( p->vSimClasses );
FREE( p->pReprsProved );
FREE( p->pSatVars );
free( p );
@@ -155,16 +158,24 @@ void Dch_ManSatSolverRecycle( Dch_Man_t * p )
int Lit;
if ( p->pSat )
{
+ Aig_Obj_t * pObj;
+ int i;
+ Vec_PtrForEachEntry( p->vUsedNodes, pObj, i )
+ Dch_ObjSetSatNum( p, pObj, 0 );
+ Vec_PtrClear( p->vUsedNodes );
+// memset( p->pSatVars, 0, sizeof(int) * Aig_ManObjNumMax(p->pAigTotal) );
sat_solver_delete( p->pSat );
- memset( p->pSatVars, 0, sizeof(int) * Aig_ManObjNumMax(p->pAigTotal) );
}
p->pSat = sat_solver_new();
sat_solver_setnvars( p->pSat, 1000 );
// var 0 is reserved for const1 node - add the clause
Lit = toLit( 0 );
+ if ( p->pPars->fPolarFlip )
+ Lit = lit_neg( Lit );
sat_solver_addclause( p->pSat, &Lit, &Lit + 1 );
p->nSatVars = 1;
p->nRecycles++;
+ p->nCallsSince = 0;
}
diff --git a/src/aig/dch/dchSat.c b/src/aig/dch/dchSat.c
index 19aaffee..e0a446f8 100644
--- a/src/aig/dch/dchSat.c
+++ b/src/aig/dch/dchSat.c
@@ -51,7 +51,10 @@ int Dch_NodesAreEquiv( Dch_Man_t * p, Aig_Obj_t * pOld, Aig_Obj_t * pNew )
assert( pNew != pOld );
// check if SAT solver needs recycling
- if ( p->pSat == NULL || (p->pPars->nSatVarMax && p->nSatVars > p->pPars->nSatVarMax) )
+ if ( p->pSat == NULL ||
+ (p->pPars->nSatVarMax &&
+ p->nSatVars > p->pPars->nSatVarMax &&
+ ++p->nCallsSince > p->pPars->nCallsRecycle) )
Dch_ManSatSolverRecycle( p );
// if the nodes do not have SAT variables, allocate them
@@ -70,6 +73,11 @@ int Dch_NodesAreEquiv( Dch_Man_t * p, Aig_Obj_t * pOld, Aig_Obj_t * pNew )
// A = 1; B = 0 OR A = 1; B = 1
pLits[0] = toLitCond( Dch_ObjSatNum(p,pOld), 0 );
pLits[1] = toLitCond( Dch_ObjSatNum(p,pNew), pOld->fPhase == pNew->fPhase );
+ if ( p->pPars->fPolarFlip )
+ {
+ if ( pOld->fPhase ) pLits[0] = lit_neg( pLits[0] );
+ if ( pNew->fPhase ) pLits[1] = lit_neg( pLits[1] );
+ }
//Sat_SolverWriteDimacs( p->pSat, "temp.cnf", pLits, pLits + 2, 1 );
clk = clock();
RetValue1 = sat_solver_solve( p->pSat, pLits, pLits + 2,
@@ -108,6 +116,11 @@ p->timeSatUndec += clock() - clk;
// A = 0; B = 1 OR A = 0; B = 0
pLits[0] = toLitCond( Dch_ObjSatNum(p,pOld), 1 );
pLits[1] = toLitCond( Dch_ObjSatNum(p,pNew), pOld->fPhase ^ pNew->fPhase );
+ if ( p->pPars->fPolarFlip )
+ {
+ if ( pOld->fPhase ) pLits[0] = lit_neg( pLits[0] );
+ if ( pNew->fPhase ) pLits[1] = lit_neg( pLits[1] );
+ }
clk = clock();
RetValue1 = sat_solver_solve( p->pSat, pLits, pLits + 2,
(sint64)nBTLimit, (sint64)0, (sint64)0, (sint64)0 );
diff --git a/src/aig/dch/dchSim.c b/src/aig/dch/dchSim.c
index 9882dd05..49734b5a 100644
--- a/src/aig/dch/dchSim.c
+++ b/src/aig/dch/dchSim.c
@@ -6,7 +6,7 @@
PackageName [Computation of equivalence classes using simulation.]
- Synopsis [Calls to the SAT solver.]
+ Synopsis [Performs random simulation at the beginning.]
Author [Alan Mishchenko]
@@ -39,6 +39,38 @@ static inline unsigned Dch_ObjRandomSim()
/**Function*************************************************************
+ Synopsis [Returns 1 if the node appears to be constant 1 candidate.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+int Dch_NodeIsConstCex( void * p, Aig_Obj_t * pObj )
+{
+ return pObj->fPhase == pObj->fMarkB;
+}
+
+/**Function*************************************************************
+
+ Synopsis [Returns 1 if the nodes appear equal.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+int Dch_NodesAreEqualCex( void * p, Aig_Obj_t * pObj0, Aig_Obj_t * pObj1 )
+{
+ return (pObj0->fPhase == pObj1->fPhase) == (pObj0->fMarkB == pObj1->fMarkB);
+}
+
+/**Function*************************************************************
+
Synopsis [Computes hash value of the node using its simulation info.]
Description []
@@ -241,14 +273,15 @@ Dch_Cla_t * Dch_CreateCandEquivClasses( Aig_Man_t * pAig, int nWords, int fVerbo
// hash nodes by sim info
Dch_ClassesPrepare( pClasses, 0, 0 );
// iterate random simulation
- for ( i = 0; i < 3; i++ )
+ for ( i = 0; i < 7; i++ )
{
Dch_PerformRandomSimulation( pAig, vSims );
Dch_ClassesRefine( pClasses );
}
// clean up and return
- Dch_ClassesSetData( pClasses, NULL, NULL, NULL, NULL );
Vec_PtrFree( vSims );
+ // prepare class refinement procedures
+ Dch_ClassesSetData( pClasses, NULL, NULL, Dch_NodeIsConstCex, Dch_NodesAreEqualCex );
return pClasses;
}
diff --git a/src/aig/dch/dchSimSat.c b/src/aig/dch/dchSimSat.c
new file mode 100644
index 00000000..cdfb9271
--- /dev/null
+++ b/src/aig/dch/dchSimSat.c
@@ -0,0 +1,243 @@
+/**CFile****************************************************************
+
+ FileName [dchSimSat.c]
+
+ SystemName [ABC: Logic synthesis and verification system.]
+
+ PackageName [Choice computation for tech-mapping.]
+
+ Synopsis [Performs resimulation using counter-examples.]
+
+ Author [Alan Mishchenko]
+
+ Affiliation [UC Berkeley]
+
+ Date [Ver. 1.0. Started - June 29, 2008.]
+
+ Revision [$Id: dchSimSat.c,v 1.00 2008/07/29 00:00:00 alanmi Exp $]
+
+***********************************************************************/
+
+#include "dchInt.h"
+
+////////////////////////////////////////////////////////////////////////
+/// DECLARATIONS ///
+////////////////////////////////////////////////////////////////////////
+
+////////////////////////////////////////////////////////////////////////
+/// FUNCTION DEFINITIONS ///
+////////////////////////////////////////////////////////////////////////
+
+/**Function*************************************************************
+
+ Synopsis [Collects internal nodes in the reverse DFS order.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+void Dch_ManCollectTfoCands_rec( Dch_Man_t * p, Aig_Obj_t * pObj )
+{
+ Aig_Obj_t * pFanout, * pRepr;
+ int iFanout = -1, i;
+ assert( !Aig_IsComplement(pObj) );
+ if ( Aig_ObjIsTravIdCurrent(p->pAigTotal, pObj) )
+ return;
+ Aig_ObjSetTravIdCurrent(p->pAigTotal, pObj);
+ // traverse the fanouts
+ Aig_ObjForEachFanout( p->pAigTotal, pObj, pFanout, iFanout, i )
+ Dch_ManCollectTfoCands_rec( p, pFanout );
+ // check if the given node has a representative
+ pRepr = Aig_ObjRepr( p->pAigTotal, pObj );
+ if ( pRepr == NULL )
+ return;
+ // pRepr is the constant 1 node
+ if ( pRepr == Aig_ManConst1(p->pAigTotal) )
+ {
+ Vec_PtrPush( p->vSimRoots, pObj );
+ return;
+ }
+ // pRepr is the representative of the equivalence class
+ if ( Aig_ObjIsTravIdCurrent(p->pAigTotal, pRepr) )
+ return;
+ Aig_ObjSetTravIdCurrent(p->pAigTotal, pRepr);
+ Vec_PtrPush( p->vSimClasses, pRepr );
+}
+
+/**Function*************************************************************
+
+ Synopsis [Collect equivalence classes and const1 cands in the TFO.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+void Dch_ManCollectTfoCands( Dch_Man_t * p, Aig_Obj_t * pObj1, Aig_Obj_t * pObj2 )
+{
+ Vec_PtrClear( p->vSimRoots );
+ Vec_PtrClear( p->vSimClasses );
+ Aig_ManIncrementTravId( p->pAigTotal );
+ Aig_ObjSetTravIdCurrent( p->pAigTotal, Aig_ManConst1(p->pAigTotal) );
+ Dch_ManCollectTfoCands_rec( p, pObj1 );
+ Dch_ManCollectTfoCands_rec( p, pObj2 );
+}
+
+/**Function*************************************************************
+
+ Synopsis [Resimulates the cone of influence of the solved nodes.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+void Dch_ManResimulateSolved_rec( Dch_Man_t * p, Aig_Obj_t * pObj )
+{
+ if ( Aig_ObjIsTravIdCurrent(p->pAigTotal, pObj) )
+ return;
+ Aig_ObjSetTravIdCurrent(p->pAigTotal, pObj);
+ if ( Aig_ObjIsPi(pObj) )
+ {
+ Aig_Obj_t * pObjFraig = Dch_ObjFraig( pObj );
+ int nVarNum = Dch_ObjSatNum( p, pObjFraig );
+ // get the value from the SAT solver
+ // (account for the fact that some vars may be minimized away)
+ pObj->fMarkB = !nVarNum? 0 : sat_solver_var_value( p->pSat, nVarNum );
+ return;
+ }
+ Dch_ManResimulateSolved_rec( p, Aig_ObjFanin0(pObj) );
+ Dch_ManResimulateSolved_rec( p, Aig_ObjFanin1(pObj) );
+ pObj->fMarkB = ( Aig_ObjFanin0(pObj)->fMarkB ^ Aig_ObjFaninC0(pObj) )
+ & ( Aig_ObjFanin1(pObj)->fMarkB ^ Aig_ObjFaninC1(pObj) );
+ // count the cone size
+ if ( Dch_ObjSatNum( p, Aig_Regular(Dch_ObjFraig(pObj)) ) > 0 )
+ p->nConeThis++;
+}
+
+/**Function*************************************************************
+
+ Synopsis [Resimulates the cone of influence of the other nodes.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+void Dch_ManResimulateOther_rec( Dch_Man_t * p, Aig_Obj_t * pObj )
+{
+ if ( Aig_ObjIsTravIdCurrent(p->pAigTotal, pObj) )
+ return;
+ Aig_ObjSetTravIdCurrent(p->pAigTotal, pObj);
+ if ( Aig_ObjIsPi(pObj) )
+ {
+ // set random value
+ pObj->fMarkB = Aig_ManRandom(0) & 1;
+ return;
+ }
+ Dch_ManResimulateOther_rec( p, Aig_ObjFanin0(pObj) );
+ Dch_ManResimulateOther_rec( p, Aig_ObjFanin1(pObj) );
+ pObj->fMarkB = ( Aig_ObjFanin0(pObj)->fMarkB ^ Aig_ObjFaninC0(pObj) )
+ & ( Aig_ObjFanin1(pObj)->fMarkB ^ Aig_ObjFaninC1(pObj) );
+}
+
+/**Function*************************************************************
+
+ Synopsis [Handle the counter-example.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+void Dch_ManResimulateCex( Dch_Man_t * p, Aig_Obj_t * pObj, Aig_Obj_t * pRepr )
+{
+ Aig_Obj_t * pRoot, ** ppClass;
+ int i, k, nSize, RetValue1, RetValue2, clk = clock();
+ // get the equivalence classes
+ Dch_ManCollectTfoCands( p, pObj, pRepr );
+ // resimulate the cone of influence of the solved nodes
+ p->nConeThis = 0;
+ Aig_ManIncrementTravId( p->pAigTotal );
+ Aig_ObjSetTravIdCurrent( p->pAigTotal, Aig_ManConst1(p->pAigTotal) );
+ Dch_ManResimulateSolved_rec( p, pObj );
+ Dch_ManResimulateSolved_rec( p, pRepr );
+ p->nConeMax = AIG_MAX( p->nConeMax, p->nConeThis );
+ // resimulate the cone of influence of the other nodes
+ Vec_PtrForEachEntry( p->vSimRoots, pRoot, i )
+ Dch_ManResimulateOther_rec( p, pRoot );
+ // refine these nodes
+ RetValue1 = Dch_ClassesRefineConst1Group( p->ppClasses, p->vSimRoots, 0 );
+ // resimulate the cone of influence of the cand classes
+ RetValue2 = 0;
+ Vec_PtrForEachEntry( p->vSimClasses, pRoot, i )
+ {
+ ppClass = Dch_ClassesReadClass( p->ppClasses, pRoot, &nSize );
+ for ( k = 0; k < nSize; k++ )
+ Dch_ManResimulateOther_rec( p, ppClass[k] );
+ // refine this class
+ RetValue2 += Dch_ClassesRefineOneClass( p->ppClasses, pRoot, 0 );
+ }
+ // make sure refinement happened
+ if ( Aig_ObjIsConst1(pRepr) )
+ assert( RetValue1 );
+ else
+ assert( RetValue2 );
+p->timeSimSat += clock() - clk;
+}
+
+/**Function*************************************************************
+
+ Synopsis [Handle the counter-example.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+void Dch_ManResimulateCex2( Dch_Man_t * p, Aig_Obj_t * pObj, Aig_Obj_t * pRepr )
+{
+ Aig_Obj_t * pRoot;
+ int i, RetValue, clk = clock();
+ // get the equivalence class
+ if ( Dch_ObjIsConst1Cand(p->pAigTotal, pObj) )
+ Dch_ClassesCollectConst1Group( p->ppClasses, pObj, 500, p->vSimRoots );
+ else
+ Dch_ClassesCollectOneClass( p->ppClasses, pRepr, p->vSimRoots );
+ // resimulate the cone of influence of the solved nodes
+ p->nConeThis = 0;
+ Aig_ManIncrementTravId( p->pAigTotal );
+ Aig_ObjSetTravIdCurrent( p->pAigTotal, Aig_ManConst1(p->pAigTotal) );
+ Dch_ManResimulateSolved_rec( p, pObj );
+ Dch_ManResimulateSolved_rec( p, pRepr );
+ p->nConeMax = AIG_MAX( p->nConeMax, p->nConeThis );
+ // resimulate the cone of influence of the other nodes
+ Vec_PtrForEachEntry( p->vSimRoots, pRoot, i )
+ Dch_ManResimulateOther_rec( p, pRoot );
+ // refine this class
+ if ( Dch_ObjIsConst1Cand(p->pAigTotal, pObj) )
+ RetValue = Dch_ClassesRefineConst1Group( p->ppClasses, p->vSimRoots, 0 );
+ else
+ RetValue = Dch_ClassesRefineOneClass( p->ppClasses, pRepr, 0 );
+ assert( RetValue );
+p->timeSimSat += clock() - clk;
+}
+
+////////////////////////////////////////////////////////////////////////
+/// END OF FILE ///
+////////////////////////////////////////////////////////////////////////
+
+
diff --git a/src/aig/dch/dchSweep.c b/src/aig/dch/dchSweep.c
index 305e19ee..019f6707 100644
--- a/src/aig/dch/dchSweep.c
+++ b/src/aig/dch/dchSweep.c
@@ -1,12 +1,12 @@
/**CFile****************************************************************
- FileName [dchSat.c]
+ FileName [dchSweep.c]
SystemName [ABC: Logic synthesis and verification system.]
PackageName [Choice computation for tech-mapping.]
- Synopsis [Calls to the SAT solver.]
+ Synopsis [One round of SAT sweeping.]
Author [Alan Mishchenko]
@@ -14,7 +14,7 @@
Date [Ver. 1.0. Started - June 29, 2008.]
- Revision [$Id: dchSat.c,v 1.00 2008/07/29 00:00:00 alanmi Exp $]
+ Revision [$Id: dchSweep.c,v 1.00 2008/07/29 00:00:00 alanmi Exp $]
***********************************************************************/
@@ -25,9 +25,6 @@
/// DECLARATIONS ///
////////////////////////////////////////////////////////////////////////
-static inline Aig_Obj_t * Dch_ObjFraig( Aig_Obj_t * pObj ) { return pObj->pData; }
-static inline void Dch_ObjSetFraig( Aig_Obj_t * pObj, Aig_Obj_t * pNode ) { pObj->pData = pNode; }
-
static inline Aig_Obj_t * Dch_ObjChild0Fra( Aig_Obj_t * pObj ) { assert( !Aig_IsComplement(pObj) ); return Aig_ObjFanin0(pObj)? Aig_NotCond(Dch_ObjFraig(Aig_ObjFanin0(pObj)), Aig_ObjFaninC0(pObj)) : NULL; }
static inline Aig_Obj_t * Dch_ObjChild1Fra( Aig_Obj_t * pObj ) { assert( !Aig_IsComplement(pObj) ); return Aig_ObjFanin1(pObj)? Aig_NotCond(Dch_ObjFraig(Aig_ObjFanin1(pObj)), Aig_ObjFaninC1(pObj)) : NULL; }
@@ -37,137 +34,6 @@ static inline Aig_Obj_t * Dch_ObjChild1Fra( Aig_Obj_t * pObj ) { assert( !Aig_Is
/**Function*************************************************************
- Synopsis [Returns 1 if the node appears to be constant 1 candidate.]
-
- Description []
-
- SideEffects []
-
- SeeAlso []
-
-***********************************************************************/
-int Dch_NodeIsConstCex( void * p, Aig_Obj_t * pObj )
-{
- return pObj->fPhase == pObj->fMarkB;
-}
-
-/**Function*************************************************************
-
- Synopsis [Returns 1 if the nodes appear equal.]
-
- Description []
-
- SideEffects []
-
- SeeAlso []
-
-***********************************************************************/
-int Dch_NodesAreEqualCex( void * p, Aig_Obj_t * pObj0, Aig_Obj_t * pObj1 )
-{
- return (pObj0->fPhase == pObj1->fPhase) == (pObj0->fMarkB == pObj1->fMarkB);
-}
-
-/**Function*************************************************************
-
- Synopsis [Resimulates the cone of influence of the solved nodes.]
-
- Description []
-
- SideEffects []
-
- SeeAlso []
-
-***********************************************************************/
-void Dch_ManResimulateSolved_rec( Dch_Man_t * p, Aig_Obj_t * pObj )
-{
- if ( Aig_ObjIsTravIdCurrent(p->pAigTotal, pObj) )
- return;
- Aig_ObjSetTravIdCurrent(p->pAigTotal, pObj);
- if ( Aig_ObjIsPi(pObj) )
- {
- // get the value from the SAT solver
- assert( p->pSatVars[pObj->Id] > 0 );
- pObj->fMarkB = sat_solver_var_value( p->pSat, p->pSatVars[pObj->Id] );
- return;
- }
- Dch_ManResimulateSolved_rec( p, Aig_ObjFanin0(pObj) );
- Dch_ManResimulateSolved_rec( p, Aig_ObjFanin1(pObj) );
- pObj->fMarkB = ( Aig_ObjFanin0(pObj)->fMarkB ^ Aig_ObjFaninC0(pObj) )
- & ( Aig_ObjFanin1(pObj)->fMarkB ^ Aig_ObjFaninC1(pObj) );
- // count the cone size
- if ( Dch_ObjSatNum( p, Aig_Regular(Dch_ObjFraig(pObj)) ) > 0 )
- p->nConeThis++;
-}
-
-/**Function*************************************************************
-
- Synopsis [Resimulates the cone of influence of the other nodes.]
-
- Description []
-
- SideEffects []
-
- SeeAlso []
-
-***********************************************************************/
-void Dch_ManResimulateOther_rec( Dch_Man_t * p, Aig_Obj_t * pObj )
-{
- if ( Aig_ObjIsTravIdCurrent(p->pAigTotal, pObj) )
- return;
- Aig_ObjSetTravIdCurrent(p->pAigTotal, pObj);
- if ( Aig_ObjIsPi(pObj) )
- {
- // set random value
- pObj->fMarkB = Aig_ManRandom(0) & 1;
- return;
- }
- Dch_ManResimulateOther_rec( p, Aig_ObjFanin0(pObj) );
- Dch_ManResimulateOther_rec( p, Aig_ObjFanin1(pObj) );
- pObj->fMarkB = ( Aig_ObjFanin0(pObj)->fMarkB ^ Aig_ObjFaninC0(pObj) )
- & ( Aig_ObjFanin1(pObj)->fMarkB ^ Aig_ObjFaninC1(pObj) );
-}
-
-/**Function*************************************************************
-
- Synopsis [Handle the counter-example.]
-
- Description []
-
- SideEffects []
-
- SeeAlso []
-
-***********************************************************************/
-void Dch_ManSweepResimulate( Dch_Man_t * p, Aig_Obj_t * pObj, Aig_Obj_t * pRepr )
-{
- Aig_Obj_t * pRoot;
- int i, RetValue, clk = clock();
- // get the equivalence class
- if ( Dch_ObjIsConst1Cand(p->pAigTotal, pObj) )
- Dch_ClassesCollectConst1Group( p->ppClasses, pObj, 500, p->vRoots );
- else
- Dch_ClassesCollectOneClass( p->ppClasses, pRepr, p->vRoots );
- // resimulate the cone of influence of the solved nodes
- p->nConeThis = 0;
- Aig_ManIncrementTravId( p->pAigTotal );
- Aig_ObjSetTravIdCurrent( p->pAigTotal, Aig_ManConst1(p->pAigTotal) );
- Dch_ManResimulateSolved_rec( p, pObj );
- Dch_ManResimulateSolved_rec( p, pRepr );
- p->nConeMax = AIG_MAX( p->nConeMax, p->nConeThis );
- // resimulate the cone of influence of the other nodes
- Vec_PtrForEachEntry( p->vRoots, pRoot, i )
- Dch_ManResimulateOther_rec( p, pRoot );
- // refine this class
- if ( Dch_ObjIsConst1Cand(p->pAigTotal, pObj) )
- RetValue = Dch_ClassesRefineConst1Group( p->ppClasses, p->vRoots, 0 );
- else
- RetValue = Dch_ClassesRefineOneClass( p->ppClasses, pRepr, 0 );
- assert( RetValue );
-p->timeSimSat += clock() - clk;
-}
-
-/**Function*************************************************************
-
Synopsis [Performs fraiging for one node.]
Description [Returns the fraiged node.]
@@ -187,8 +53,12 @@ void Dch_ManSweepNode( Dch_Man_t * p, Aig_Obj_t * pObj )
return;
// get the fraiged node
pObjFraig = Dch_ObjFraig( pObj );
+ if ( pObjFraig == NULL )
+ return;
// get the fraiged representative
pObjReprFraig = Dch_ObjFraig( pObjRepr );
+ if ( pObjReprFraig == NULL )
+ return;
// if the fraiged nodes are the same, return
if ( Aig_Regular(pObjFraig) == Aig_Regular(pObjReprFraig) )
{
@@ -199,7 +69,10 @@ void Dch_ManSweepNode( Dch_Man_t * p, Aig_Obj_t * pObj )
assert( Aig_Regular(pObjFraig) != Aig_ManConst1(p->pAigFraig) );
RetValue = Dch_NodesAreEquiv( p, Aig_Regular(pObjReprFraig), Aig_Regular(pObjFraig) );
if ( RetValue == -1 ) // timed out
+ {
+ Dch_ObjSetFraig( pObj, NULL );
return;
+ }
if ( RetValue == 1 ) // proved equivalent
{
pObjFraig2 = Aig_NotCond( pObjReprFraig, pObj->fPhase ^ pObjRepr->fPhase );
@@ -209,7 +82,10 @@ void Dch_ManSweepNode( Dch_Man_t * p, Aig_Obj_t * pObj )
return;
}
// disproved the equivalence
- Dch_ManSweepResimulate( p, pObj, pObjRepr );
+ if ( p->pPars->fSimulateTfo )
+ Dch_ManResimulateCex( p, pObj, pObjRepr );
+ else
+ Dch_ManResimulateCex2( p, pObj, pObjRepr );
}
/**Function*************************************************************
@@ -234,19 +110,21 @@ void Dch_ManSweep( Dch_Man_t * p )
Aig_ManConst1(p->pAigTotal)->pData = Aig_ManConst1(p->pAigFraig);
Aig_ManForEachPi( p->pAigTotal, pObj, i )
pObj->pData = Aig_ObjCreatePi( p->pAigFraig );
- // prepare class refinement procedures
- Dch_ClassesSetData( p->ppClasses, NULL, NULL, Dch_NodeIsConstCex, Dch_NodesAreEqualCex );
// sweep internal nodes
pProgress = Bar_ProgressStart( stdout, Aig_ManObjNumMax(p->pAigTotal) );
Aig_ManForEachNode( p->pAigTotal, pObj, i )
{
Bar_ProgressUpdate( pProgress, i, NULL );
+ if ( Dch_ObjFraig(Aig_ObjFanin0(pObj)) == NULL ||
+ Dch_ObjFraig(Aig_ObjFanin1(pObj)) == NULL )
+ continue;
pObjNew = Aig_And( p->pAigFraig, Dch_ObjChild0Fra(pObj), Dch_ObjChild1Fra(pObj) );
if ( pObjNew == NULL )
continue;
Dch_ObjSetFraig( pObj, pObjNew );
Dch_ManSweepNode( p, pObj );
}
+ Bar_ProgressStop( pProgress );
// update the representatives of the nodes (makes classes invalid)
FREE( p->pAigTotal->pReprs );
p->pAigTotal->pReprs = p->pReprsProved;
diff --git a/src/aig/dch/module.make b/src/aig/dch/module.make
index 08d5a555..5709f87a 100644
--- a/src/aig/dch/module.make
+++ b/src/aig/dch/module.make
@@ -6,4 +6,5 @@ SRC += src/aig/dch/dchAig.c \
src/aig/dch/dchMan.c \
src/aig/dch/dchSat.c \
src/aig/dch/dchSim.c \
+ src/aig/dch/dchSimSat.c \
src/aig/dch/dchSweep.c
diff --git a/src/aig/ntl/ntlCore.c b/src/aig/ntl/ntlCore.c
index a5c40444..6bff57d9 100644
--- a/src/aig/ntl/ntlCore.c
+++ b/src/aig/ntl/ntlCore.c
@@ -19,6 +19,7 @@
***********************************************************************/
#include "ntl.h"
+#include "dch.h"
////////////////////////////////////////////////////////////////////////
/// DECLARATIONS ///
@@ -39,7 +40,7 @@
SeeAlso []
***********************************************************************/
-Aig_Man_t * Ntl_ManPerformSynthesis( Aig_Man_t * pAig, int fBalance, int fUpdateLevel, int fConstruct, int nConfMax, int nLevelMax, int fVerbose )
+Aig_Man_t * Ntl_ManPerformChoicing( Aig_Man_t * pAig, int fBalance, int fUpdateLevel, int fConstruct, int nConfMax, int nLevelMax, int fVerbose )
{
extern Aig_Man_t * Dar_ManBalance( Aig_Man_t * pAig, int fUpdateLevel );
extern Aig_Man_t * Dar_ManCompress( Aig_Man_t * pAig, int fBalance, int fUpdateLevel, int fVerbose );
@@ -58,6 +59,23 @@ Aig_Man_t * Ntl_ManPerformSynthesis( Aig_Man_t * pAig, int fBalance, int fUpdate
/**Function*************************************************************
+ Synopsis [Extracts AIG from the netlist.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+Aig_Man_t * Ntl_ManPerformChoicingNew( Aig_Man_t * pAig, Dch_Pars_t * pPars )
+{
+ extern Aig_Man_t * Dar_ManChoiceNew( Aig_Man_t * pAig, Dch_Pars_t * pPars );
+ return Dar_ManChoiceNew( pAig, pPars );
+}
+
+/**Function*************************************************************
+
Synopsis [Testing procedure for insertion of mapping into the netlist.]
Description []
diff --git a/src/base/abci/abc.c b/src/base/abci/abc.c
index 5e65d636..26f97b78 100644
--- a/src/base/abci/abc.c
+++ b/src/base/abci/abc.c
@@ -229,6 +229,7 @@ static int Abc_CommandAbc8Ps ( Abc_Frame_t * pAbc, int argc, char ** arg
static int Abc_CommandAbc8Pfan ( Abc_Frame_t * pAbc, int argc, char ** argv );
static int Abc_CommandAbc8If ( Abc_Frame_t * pAbc, int argc, char ** argv );
static int Abc_CommandAbc8DChoice ( Abc_Frame_t * pAbc, int argc, char ** argv );
+static int Abc_CommandAbc8Dch ( Abc_Frame_t * pAbc, int argc, char ** argv );
static int Abc_CommandAbc8DC2 ( Abc_Frame_t * pAbc, int argc, char ** argv );
static int Abc_CommandAbc8Bidec ( Abc_Frame_t * pAbc, int argc, char ** argv );
static int Abc_CommandAbc8Strash ( Abc_Frame_t * pAbc, int argc, char ** argv );
@@ -488,6 +489,7 @@ void Abc_Init( Abc_Frame_t * pAbc )
Cmd_CommandAdd( pAbc, "ABC8", "*pfan", Abc_CommandAbc8Pfan, 0 );
Cmd_CommandAdd( pAbc, "ABC8", "*if", Abc_CommandAbc8If, 0 );
Cmd_CommandAdd( pAbc, "ABC8", "*dchoice", Abc_CommandAbc8DChoice, 0 );
+ Cmd_CommandAdd( pAbc, "ABC8", "*dch", Abc_CommandAbc8Dch, 0 );
Cmd_CommandAdd( pAbc, "ABC8", "*dc2", Abc_CommandAbc8DC2, 0 );
Cmd_CommandAdd( pAbc, "ABC8", "*bidec", Abc_CommandAbc8Bidec, 0 );
Cmd_CommandAdd( pAbc, "ABC8", "*st", Abc_CommandAbc8Strash, 0 );
@@ -7703,7 +7705,7 @@ int Abc_CommandTest( Abc_Frame_t * pAbc, int argc, char ** argv )
// extern Abc_Ntk_t * Abc_NtkNtkTest( Abc_Ntk_t * pNtk, If_Lib_t * pLutLib );
extern Abc_Ntk_t * Abc_NtkDarRetimeStep( Abc_Ntk_t * pNtk, int fVerbose );
extern void Abc_NtkDarTest( Abc_Ntk_t * pNtk );
- extern void Aig_ProcedureTest();
+// extern void Aig_ProcedureTest();
pNtk = Abc_FrameReadNtk(pAbc);
@@ -7910,7 +7912,7 @@ int Abc_CommandTest( Abc_Frame_t * pAbc, int argc, char ** argv )
pFileName = argv[globalUtilOptind];
Nwk_ManLutMergeGraphTest( pFileName );
*/
- Aig_ProcedureTest();
+// Aig_ProcedureTest();
return 0;
usage:
@@ -8929,7 +8931,7 @@ int Abc_CommandDChoice( Abc_Frame_t * pAbc, int argc, char ** argv )
usage:
fprintf( pErr, "usage: dchoice [-C num] [-L num] [-blcvh]\n" );
- fprintf( pErr, "\t performs partitioned choicing using a new AIG package\n" );
+ fprintf( pErr, "\t performs partitioned choicing using new AIG package\n" );
fprintf( pErr, "\t-C num : the max number of conflicts at a node [default = %d]\n", nConfMax );
fprintf( pErr, "\t-L num : the max level of nodes to consider (0 = not used) [default = %d]\n", nLevelMax );
fprintf( pErr, "\t-b : toggle internal balancing [default = %s]\n", fBalance? "yes": "no" );
@@ -8967,7 +8969,7 @@ int Abc_CommandDch( Abc_Frame_t * pAbc, int argc, char ** argv )
// set defaults
Dch_ManSetDefaultParams( pPars );
Extra_UtilGetoptReset();
- while ( ( c = Extra_UtilGetopt( argc, argv, "WCSsvh" ) ) != EOF )
+ while ( ( c = Extra_UtilGetopt( argc, argv, "WCSsptvh" ) ) != EOF )
{
switch ( c )
{
@@ -9007,6 +9009,12 @@ int Abc_CommandDch( Abc_Frame_t * pAbc, int argc, char ** argv )
case 's':
pPars->fSynthesis ^= 1;
break;
+ case 'p':
+ pPars->fPolarFlip ^= 1;
+ break;
+ case 't':
+ pPars->fSimulateTfo ^= 1;
+ break;
case 'v':
pPars->fVerbose ^= 1;
break;
@@ -9037,12 +9045,14 @@ int Abc_CommandDch( Abc_Frame_t * pAbc, int argc, char ** argv )
return 0;
usage:
- fprintf( pErr, "usage: dch [-WCS num] [-svh]\n" );
- fprintf( pErr, "\t performs computation of structural choices\n" );
+ fprintf( pErr, "usage: dch [-WCS num] [-sptvh]\n" );
+ fprintf( pErr, "\t computes structural choices using a new approach\n" );
fprintf( pErr, "\t-W num : the max number of simulation words [default = %d]\n", pPars->nWords );
fprintf( pErr, "\t-C num : the max number of conflicts at a node [default = %d]\n", pPars->nBTLimit );
fprintf( pErr, "\t-S num : the max number of SAT variables [default = %d]\n", pPars->nSatVarMax );
fprintf( pErr, "\t-s : toggle synthesizing three snapshots [default = %s]\n", pPars->fSynthesis? "yes": "no" );
+ fprintf( pErr, "\t-p : toggle alighning polarity of SAT variables [default = %s]\n", pPars->fPolarFlip? "yes": "no" );
+ fprintf( pErr, "\t-t : toggle simulation of the TFO classes [default = %s]\n", pPars->fSimulateTfo? "yes": "no" );
fprintf( pErr, "\t-v : toggle verbose printout [default = %s]\n", pPars->fVerbose? "yes": "no" );
fprintf( pErr, "\t-h : print the command usage\n");
return 1;
@@ -17155,7 +17165,7 @@ int Abc_CommandAbc8DChoice( Abc_Frame_t * pAbc, int argc, char ** argv )
Aig_Man_t * pAigNew;
int fBalance, fVerbose, fUpdateLevel, fConstruct, c;
int nConfMax, nLevelMax;
- extern Aig_Man_t * Ntl_ManPerformSynthesis( Aig_Man_t * pAig, int fBalance, int fUpdateLevel, int fConstruct, int nConfMax, int nLevelMax, int fVerbose );
+ extern Aig_Man_t * Ntl_ManPerformChoicing( Aig_Man_t * pAig, int fBalance, int fUpdateLevel, int fConstruct, int nConfMax, int nLevelMax, int fVerbose );
// set defaults
fBalance = 1;
@@ -17216,7 +17226,7 @@ int Abc_CommandAbc8DChoice( Abc_Frame_t * pAbc, int argc, char ** argv )
}
// get the input file name
- pAigNew = Ntl_ManPerformSynthesis( pAbc->pAbc8Aig, fBalance, fUpdateLevel, fConstruct, nConfMax, nLevelMax, fVerbose );
+ pAigNew = Ntl_ManPerformChoicing( pAbc->pAbc8Aig, fBalance, fUpdateLevel, fConstruct, nConfMax, nLevelMax, fVerbose );
if ( pAigNew == NULL )
{
printf( "Abc_CommandAbc8DChoice(): Tranformation of the AIG has failed.\n" );
@@ -17250,6 +17260,113 @@ usage:
SeeAlso []
***********************************************************************/
+int Abc_CommandAbc8Dch( Abc_Frame_t * pAbc, int argc, char ** argv )
+{
+ Dch_Pars_t Pars, * pPars = &Pars;
+ Aig_Man_t * pAigNew;
+ int c;
+ extern Aig_Man_t * Ntl_ManPerformChoicingNew( Aig_Man_t * pAig, Dch_Pars_t * pPars );
+
+ // set defaults
+ Dch_ManSetDefaultParams( pPars );
+ Extra_UtilGetoptReset();
+ while ( ( c = Extra_UtilGetopt( argc, argv, "WCSsptvh" ) ) != EOF )
+ {
+ switch ( c )
+ {
+ case 'W':
+ if ( globalUtilOptind >= argc )
+ {
+ fprintf( stdout, "Command line switch \"-W\" should be followed by an integer.\n" );
+ goto usage;
+ }
+ pPars->nWords = atoi(argv[globalUtilOptind]);
+ globalUtilOptind++;
+ if ( pPars->nWords < 0 )
+ goto usage;
+ break;
+ case 'C':
+ if ( globalUtilOptind >= argc )
+ {
+ fprintf( stdout, "Command line switch \"-C\" should be followed by an integer.\n" );
+ goto usage;
+ }
+ pPars->nBTLimit = atoi(argv[globalUtilOptind]);
+ globalUtilOptind++;
+ if ( pPars->nBTLimit < 0 )
+ goto usage;
+ break;
+ case 'S':
+ if ( globalUtilOptind >= argc )
+ {
+ fprintf( stdout, "Command line switch \"-S\" should be followed by an integer.\n" );
+ goto usage;
+ }
+ pPars->nSatVarMax = atoi(argv[globalUtilOptind]);
+ globalUtilOptind++;
+ if ( pPars->nSatVarMax < 0 )
+ goto usage;
+ break;
+ case 's':
+ pPars->fSynthesis ^= 1;
+ break;
+ case 'p':
+ pPars->fPolarFlip ^= 1;
+ break;
+ case 't':
+ pPars->fSimulateTfo ^= 1;
+ break;
+ case 'v':
+ pPars->fVerbose ^= 1;
+ break;
+ case 'h':
+ goto usage;
+ default:
+ goto usage;
+ }
+ }
+ if ( pAbc->pAbc8Aig == NULL )
+ {
+ printf( "Abc_CommandAbc8Dch(): There is no AIG to synthesize.\n" );
+ return 1;
+ }
+
+ // get the input file name
+ pAigNew = Ntl_ManPerformChoicingNew( pAbc->pAbc8Aig, pPars );
+ if ( pAigNew == NULL )
+ {
+ printf( "Abc_CommandAbc8Dch(): Tranformation of the AIG has failed.\n" );
+ return 1;
+ }
+ Aig_ManStop( pAbc->pAbc8Aig );
+ pAbc->pAbc8Aig = pAigNew;
+ return 0;
+
+usage:
+ fprintf( stdout, "usage: *dch [-WCS num] [-sptvh]\n" );
+ fprintf( stdout, "\t computes structural choices using a new approach\n" );
+ fprintf( stdout, "\t-W num : the max number of simulation words [default = %d]\n", pPars->nWords );
+ fprintf( stdout, "\t-C num : the max number of conflicts at a node [default = %d]\n", pPars->nBTLimit );
+ fprintf( stdout, "\t-S num : the max number of SAT variables [default = %d]\n", pPars->nSatVarMax );
+ fprintf( stdout, "\t-s : toggle synthesizing three snapshots [default = %s]\n", pPars->fSynthesis? "yes": "no" );
+ fprintf( stdout, "\t-p : toggle alighning polarity of SAT variables [default = %s]\n", pPars->fPolarFlip? "yes": "no" );
+ fprintf( stdout, "\t-t : toggle simulation of the TFO classes [default = %s]\n", pPars->fSimulateTfo? "yes": "no" );
+ fprintf( stdout, "\t-v : toggle verbose printout [default = %s]\n", pPars->fVerbose? "yes": "no" );
+ fprintf( stdout, "\t-h : print the command usage\n");
+ return 1;
+}
+
+/**Function*************************************************************
+
+ Synopsis []
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
int Abc_CommandAbc8DC2( Abc_Frame_t * pAbc, int argc, char ** argv )
{
Aig_Man_t * pAigNew;
generated by cgit v1.2.3 (git 2.25.1) at 2025-10-31 06:49:51 +0000