summaryrefslogtreecommitdiffstats
path: root/src/opt/res
diff options
context:
space:
mode:
Diffstat (limited to 'src/opt/res')
-rw-r--r--src/opt/res/res.h2
-rw-r--r--src/opt/res/resCore.c102
-rw-r--r--src/opt/res/resDivs.c10
-rw-r--r--src/opt/res/resFilter.c147
-rw-r--r--src/opt/res/resInt.h16
-rw-r--r--src/opt/res/resSat.c163
-rw-r--r--src/opt/res/resSim.c505
-rw-r--r--src/opt/res/resSim_old.c521
-rw-r--r--src/opt/res/resWin.c13
9 files changed, 1314 insertions, 165 deletions
diff --git a/src/opt/res/res.h b/src/opt/res/res.h
index fda35b89..3c963e99 100644
--- a/src/opt/res/res.h
+++ b/src/opt/res/res.h
@@ -44,6 +44,8 @@ struct Res_Par_t_
int nWindow; // window size
int nSimWords; // the number of simulation words
int nCands; // the number of candidates to try
+ int fArea; // performs optimization for area
+ int fDelay; // performs optimization for delay
int fVerbose; // enable basic stats
int fVeryVerbose; // enable detailed stats
};
diff --git a/src/opt/res/resCore.c b/src/opt/res/resCore.c
index 609addf9..95728e9a 100644
--- a/src/opt/res/resCore.c
+++ b/src/opt/res/resCore.c
@@ -48,17 +48,24 @@ struct Res_Man_t_
int nDivNodes; // the total number of divisors
int nWinsTriv; // the total number of trivial windows
int nWinsUsed; // the total number of useful windows (with at least one candidate)
+ int nConstsUsed; // the total number of constant nodes under ODC
int nCandSets; // the total number of candidates
int nProvedSets; // the total number of proved groups
int nSimEmpty; // the empty simulation info
int nTotalNets; // the total number of nets
+ int nTotalNodes; // the total number of nodess
+ int nTotalNets2; // the total number of nets
+ int nTotalNodes2; // the total number of nodess
// runtime
int timeWin; // windowing
int timeDiv; // divisors
int timeAig; // strashing
int timeSim; // simulation
int timeCand; // resubstitution candidates
- int timeSat; // SAT solving
+ int timeSatTotal; // SAT solving total
+ int timeSatSat; // SAT solving (sat calls)
+ int timeSatUnsat; // SAT solving (unsat calls)
+ int timeSatSim; // SAT solving (simulation)
int timeInt; // interpolation
int timeUpd; // updating
int timeTotal; // total runtime
@@ -120,19 +127,30 @@ void Res_ManFree( Res_Man_t * p )
printf( "\n" );
printf( "WinsTriv = %d. ", p->nWinsTriv );
printf( "SimsEmpt = %d. ", p->nSimEmpty );
+ printf( "Const = %d. ", p->nConstsUsed );
printf( "WindUsed = %d. ", p->nWinsUsed );
printf( "Cands = %d. ", p->nCandSets );
- printf( "Proved = %d. (%.2f %%)", p->nProvedSets, 100.0*p->nProvedSets/p->nTotalNets );
+ printf( "Proved = %d.", p->nProvedSets );
+ printf( "\n" );
+ printf( "Reduction in nodes = %d. (%.2f %%) ",
+ p->nTotalNodes-p->nTotalNodes2,
+ 100.0*(p->nTotalNodes-p->nTotalNodes2)/p->nTotalNodes );
+ printf( "Reduction in nets = %d. (%.2f %%) ",
+ p->nTotalNets-p->nTotalNets2,
+ 100.0*(p->nTotalNets-p->nTotalNets2)/p->nTotalNets );
printf( "\n" );
- PRT( "Windowing ", p->timeWin );
- PRT( "Divisors ", p->timeDiv );
- PRT( "Strashing ", p->timeAig );
- PRT( "Simulation ", p->timeSim );
- PRT( "Candidates ", p->timeCand );
- PRT( "SAT solver ", p->timeSat );
- PRT( "Interpol ", p->timeInt );
- PRT( "Undating ", p->timeUpd );
+ PRTP( "Windowing ", p->timeWin, p->timeTotal );
+ PRTP( "Divisors ", p->timeDiv, p->timeTotal );
+ PRTP( "Strashing ", p->timeAig, p->timeTotal );
+ PRTP( "Simulation ", p->timeSim, p->timeTotal );
+ PRTP( "Candidates ", p->timeCand, p->timeTotal );
+ PRTP( "SAT solver ", p->timeSatTotal, p->timeTotal );
+ PRTP( " sat ", p->timeSatSat, p->timeTotal );
+ PRTP( " unsat ", p->timeSatUnsat, p->timeTotal );
+ PRTP( " simul ", p->timeSatSim, p->timeTotal );
+ PRTP( "Interpol ", p->timeInt, p->timeTotal );
+ PRTP( "Undating ", p->timeUpd, p->timeTotal );
PRT( "TOTAL ", p->timeTotal );
}
Res_WinFree( p->pWin );
@@ -160,6 +178,7 @@ void Res_ManFree( Res_Man_t * p )
***********************************************************************/
int Abc_NtkResynthesize( Abc_Ntk_t * pNtk, Res_Par_t * pPars )
{
+ ProgressBar * pProgress;
Res_Man_t * p;
Abc_Obj_t * pObj;
Hop_Obj_t * pFunc;
@@ -168,18 +187,33 @@ int Abc_NtkResynthesize( Abc_Ntk_t * pNtk, Res_Par_t * pPars )
unsigned * puTruth;
int i, k, RetValue, nNodesOld, nFanins;
int clk, clkTotal = clock();
- assert( Abc_NtkHasAig(pNtk) );
// start the manager
p = Res_ManAlloc( pPars );
p->nTotalNets = Abc_NtkGetTotalFanins(pNtk);
+ p->nTotalNodes = Abc_NtkNodeNum(pNtk);
+
+ // perform the network sweep
+ Abc_NtkSweep( pNtk, 0 );
+
+ // convert into the AIG
+ if ( !Abc_NtkLogicToAig(pNtk) )
+ {
+ fprintf( stdout, "Converting to BDD has failed.\n" );
+ Res_ManFree( p );
+ return 0;
+ }
+ assert( Abc_NtkHasAig(pNtk) );
+
// set the number of levels
Abc_NtkLevel( pNtk );
// try resynthesizing nodes in the topological order
nNodesOld = Abc_NtkObjNumMax(pNtk);
+ pProgress = Extra_ProgressBarStart( stdout, nNodesOld );
Abc_NtkForEachObj( pNtk, pObj, i )
{
+ Extra_ProgressBarUpdate( pProgress, i, NULL );
if ( !Abc_ObjIsNode(pObj) )
continue;
if ( pObj->Id > nNodesOld )
@@ -205,7 +239,7 @@ p->timeWin += clock() - clk;
// collect the divisors
clk = clock();
- Res_WinDivisors( p->pWin, pObj->Level - 1 );
+ Res_WinDivisors( p->pWin, pObj->Level + 2 ); //- 1 );
p->timeDiv += clock() - clk;
p->nWins++;
@@ -232,7 +266,7 @@ p->timeAig += clock() - clk;
// prepare simulation info
clk = clock();
- RetValue = Res_SimPrepare( p->pSim, p->pAig );
+ RetValue = Res_SimPrepare( p->pSim, p->pAig, Vec_PtrSize(p->pWin->vLeaves), 0 ); //p->pPars->fVerbose );
p->timeSim += clock() - clk;
if ( !RetValue )
{
@@ -240,14 +274,33 @@ p->timeSim += clock() - clk;
continue;
}
+ // consider the case of constant node
+ if ( p->pSim->fConst0 || p->pSim->fConst1 )
+ {
+ p->nConstsUsed++;
+
+ pFunc = p->pSim->fConst1? Hop_ManConst1(pNtk->pManFunc) : Hop_ManConst0(pNtk->pManFunc);
+ vFanins = Vec_VecEntry( p->vResubsW, 0 );
+ Vec_PtrClear( vFanins );
+ Res_UpdateNetwork( pObj, vFanins, pFunc, p->vLevels );
+ continue;
+ }
+
+// printf( " " );
+
// find resub candidates for the node
clk = clock();
- RetValue = Res_FilterCandidates( p->pWin, p->pAig, p->pSim, p->vResubs, p->vResubsW );
+ if ( p->pPars->fArea )
+ RetValue = Res_FilterCandidatesArea( p->pWin, p->pAig, p->pSim, p->vResubs, p->vResubsW );
+ else
+ RetValue = Res_FilterCandidatesNets( p->pWin, p->pAig, p->pSim, p->vResubs, p->vResubsW );
p->timeCand += clock() - clk;
p->nCandSets += RetValue;
if ( RetValue == 0 )
continue;
+// printf( "%d(%d) ", Vec_PtrSize(p->pWin->vDivs), RetValue );
+
p->nWinsUsed++;
// iterate through candidate resubstitutions
@@ -260,15 +313,20 @@ p->timeCand += clock() - clk;
clk = clock();
if ( p->pCnf ) Sto_ManFree( p->pCnf );
p->pCnf = Res_SatProveUnsat( p->pAig, vFanins );
-p->timeSat += clock() - clk;
if ( p->pCnf == NULL )
{
+p->timeSatSat += clock() - clk;
// printf( " Sat\n" );
+// printf( "-" );
continue;
}
+p->timeSatUnsat += clock() - clk;
+// printf( "+" );
+
p->nProvedSets++;
// printf( " Unsat\n" );
// continue;
+// printf( "Proved %d.\n", k );
// write it into a file
// Sto_ManDumpClauses( p->pCnf, "trace.cnf" );
@@ -277,10 +335,11 @@ p->timeSat += clock() - clk;
clk = clock();
nFanins = Int_ManInterpolate( p->pMan, p->pCnf, 0, &puTruth );
p->timeInt += clock() - clk;
- assert( nFanins == Vec_PtrSize(vFanins) - 2 );
+ if ( nFanins != Vec_PtrSize(vFanins) - 2 )
+ continue;
assert( puTruth );
// Extra_PrintBinary( stdout, puTruth, 1 << nFanins ); printf( "\n" );
-
+
// transform interpolant into the AIG
pGraph = Kit_TruthToGraph( puTruth, nFanins, p->vMem );
@@ -294,8 +353,15 @@ clk = clock();
p->timeUpd += clock() - clk;
break;
}
-
+// printf( "\n" );
}
+ Extra_ProgressBarStop( pProgress );
+
+p->timeSatSim += p->pSim->timeSat;
+p->timeSatTotal = p->timeSatSat + p->timeSatUnsat + p->timeSatSim;
+
+ p->nTotalNets2 = Abc_NtkGetTotalFanins(pNtk);
+ p->nTotalNodes2 = Abc_NtkNodeNum(pNtk);
// quit resubstitution manager
p->timeTotal = clock() - clkTotal;
diff --git a/src/opt/res/resDivs.c b/src/opt/res/resDivs.c
index af30592c..38294428 100644
--- a/src/opt/res/resDivs.c
+++ b/src/opt/res/resDivs.c
@@ -26,7 +26,6 @@
////////////////////////////////////////////////////////////////////////
static void Res_WinMarkTfi( Res_Win_t * p );
-static int Res_WinVisitMffc( Res_Win_t * p );
////////////////////////////////////////////////////////////////////////
/// FUNCTION DEFINITIONS ///
@@ -61,7 +60,7 @@ void Res_WinDivisors( Res_Win_t * p, int nLevDivMax )
// (3) the node's fanins (these are treated as a special case)
Abc_NtkIncrementTravId( p->pNode->pNtk );
Res_WinSweepLeafTfo_rec( p->pNode, p->nLevDivMax );
- Res_WinVisitMffc( p );
+ Res_WinVisitMffc( p->pNode );
Abc_ObjForEachFanin( p->pNode, pObj, k )
Abc_NodeSetTravIdCurrent( pObj );
@@ -260,13 +259,14 @@ int Res_NodeRef_rec( Abc_Obj_t * pNode )
SeeAlso []
***********************************************************************/
-int Res_WinVisitMffc( Res_Win_t * p )
+int Res_WinVisitMffc( Abc_Obj_t * pNode )
{
int Count1, Count2;
+ assert( Abc_ObjIsNode(pNode) );
// dereference the node (mark with the current trav ID)
- Count1 = Res_NodeDeref_rec( p->pNode );
+ Count1 = Res_NodeDeref_rec( pNode );
// reference it back
- Count2 = Res_NodeRef_rec( p->pNode );
+ Count2 = Res_NodeRef_rec( pNode );
assert( Count1 == Count2 );
return Count1;
}
diff --git a/src/opt/res/resFilter.c b/src/opt/res/resFilter.c
index 38f64815..afbbbe42 100644
--- a/src/opt/res/resFilter.c
+++ b/src/opt/res/resFilter.c
@@ -26,6 +26,7 @@
////////////////////////////////////////////////////////////////////////
static unsigned * Res_FilterCollectFaninInfo( Res_Win_t * pWin, Res_Sim_t * pSim, unsigned uMask );
+static int Res_FilterCriticalFanin( Abc_Obj_t * pNode );
////////////////////////////////////////////////////////////////////////
/// FUNCTION DEFINITIONS ///
@@ -42,7 +43,7 @@ static unsigned * Res_FilterCollectFaninInfo( Res_Win_t * pWin, Res_Sim_t * pSim
SeeAlso []
***********************************************************************/
-int Res_FilterCandidates( Res_Win_t * pWin, Abc_Ntk_t * pAig, Res_Sim_t * pSim, Vec_Vec_t * vResubs, Vec_Vec_t * vResubsW )
+int Res_FilterCandidatesNets( Res_Win_t * pWin, Abc_Ntk_t * pAig, Res_Sim_t * pSim, Vec_Vec_t * vResubs, Vec_Vec_t * vResubsW )
{
Abc_Obj_t * pFanin, * pFanin2;
unsigned * pInfo;
@@ -52,13 +53,19 @@ int Res_FilterCandidates( Res_Win_t * pWin, Abc_Ntk_t * pAig, Res_Sim_t * pSim,
pInfo = Vec_PtrEntry( pSim->vOuts, 1 );
RetValue = Abc_InfoIsOne( pInfo, pSim->nWordsOut );
if ( RetValue == 0 )
- printf( "Failed 1!\n" );
+ {
+// printf( "Failed 1!\n" );
+ return 0;
+ }
// collect the fanin info
pInfo = Res_FilterCollectFaninInfo( pWin, pSim, ~0 );
RetValue = Abc_InfoIsOne( pInfo, pSim->nWordsOut );
if ( RetValue == 0 )
- printf( "Failed 2!\n" );
+ {
+// printf( "Failed 2!\n" );
+ return 0;
+ }
// try removing fanins
// printf( "Fanins: " );
@@ -71,7 +78,7 @@ int Res_FilterCandidates( Res_Win_t * pWin, Abc_Ntk_t * pAig, Res_Sim_t * pSim,
RetValue = Abc_InfoIsOne( pInfo, pSim->nWordsOut );
if ( RetValue )
{
-// printf( "Node %4d. Removing fanin %4d.\n", pWin->pNode->Id, Abc_ObjFaninId(pWin->pNode, i) );
+// printf( "Node %4d. Candidate fanin %4d.\n", pWin->pNode->Id, pFanin->Id );
// collect the nodes
Vec_VecPush( vResubs, Counter, Abc_NtkPo(pAig,0) );
@@ -94,6 +101,104 @@ int Res_FilterCandidates( Res_Win_t * pWin, Abc_Ntk_t * pAig, Res_Sim_t * pSim,
return Counter;
}
+
+/**Function*************************************************************
+
+ Synopsis [Finds sets of feasible candidates.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+int Res_FilterCandidatesArea( Res_Win_t * pWin, Abc_Ntk_t * pAig, Res_Sim_t * pSim, Vec_Vec_t * vResubs, Vec_Vec_t * vResubsW )
+{
+ Abc_Obj_t * pFanin;
+ unsigned * pInfo, * pInfo2;
+ int Counter, RetValue, i, k, iBest;
+
+ // check that the info the node is one
+ pInfo = Vec_PtrEntry( pSim->vOuts, 1 );
+ RetValue = Abc_InfoIsOne( pInfo, pSim->nWordsOut );
+ if ( RetValue == 0 )
+ {
+// printf( "Failed 1!\n" );
+ return 0;
+ }
+
+ // collect the fanin info
+ pInfo = Res_FilterCollectFaninInfo( pWin, pSim, ~0 );
+ RetValue = Abc_InfoIsOne( pInfo, pSim->nWordsOut );
+ if ( RetValue == 0 )
+ {
+// printf( "Failed 2!\n" );
+ return 0;
+ }
+
+ // try removing fanins
+// printf( "Fanins: " );
+ Counter = 0;
+ Vec_VecClear( vResubs );
+ Vec_VecClear( vResubsW );
+ // get the best fanins
+ iBest = Res_FilterCriticalFanin( pWin->pNode );
+ if ( iBest == -1 )
+ return 0;
+
+ // get the info without the critical fanin
+ pInfo = Res_FilterCollectFaninInfo( pWin, pSim, ~(1 << iBest) );
+ RetValue = Abc_InfoIsOne( pInfo, pSim->nWordsOut );
+ if ( RetValue )
+ {
+// printf( "Can be done without one!\n" );
+ // collect the nodes
+ Vec_VecPush( vResubs, Counter, Abc_NtkPo(pAig,0) );
+ Vec_VecPush( vResubs, Counter, Abc_NtkPo(pAig,1) );
+ Abc_ObjForEachFanin( pWin->pNode, pFanin, k )
+ {
+ if ( k != iBest )
+ {
+ Vec_VecPush( vResubs, Counter, Abc_NtkPo(pAig,2+k) );
+ Vec_VecPush( vResubsW, Counter, pFanin );
+ }
+ }
+ Counter++;
+// printf( "*" );
+ return Counter;
+ }
+
+ // go through the divisors
+ for ( i = Abc_ObjFaninNum(pWin->pNode) + 2; i < Abc_NtkPoNum(pAig); i++ )
+ {
+ pInfo2 = Vec_PtrEntry( pSim->vOuts, i );
+ if ( !Abc_InfoIsOrOne( pInfo, pInfo2, pSim->nWordsOut ) )
+ continue;
+ // collect the nodes
+ Vec_VecPush( vResubs, Counter, Abc_NtkPo(pAig,0) );
+ Vec_VecPush( vResubs, Counter, Abc_NtkPo(pAig,1) );
+ // collect the remaning fanins and the divisor
+ Abc_ObjForEachFanin( pWin->pNode, pFanin, k )
+ {
+ if ( k != iBest )
+ {
+ Vec_VecPush( vResubs, Counter, Abc_NtkPo(pAig,2+k) );
+ Vec_VecPush( vResubsW, Counter, pFanin );
+ }
+ }
+ // collect the divisor
+ Vec_VecPush( vResubs, Counter, Abc_NtkPo(pAig,i) );
+ Vec_VecPush( vResubsW, Counter, Vec_PtrEntry(pWin->vDivs, i-2-Abc_ObjFaninNum(pWin->pNode)) );
+ Counter++;
+
+ if ( Counter == Vec_VecSize(vResubs) )
+ break;
+ }
+ return Counter;
+}
+
+
/**Function*************************************************************
Synopsis [Finds sets of feasible candidates.]
@@ -121,6 +226,40 @@ unsigned * Res_FilterCollectFaninInfo( Res_Win_t * pWin, Res_Sim_t * pSim, unsig
}
+/**Function*************************************************************
+
+ Synopsis [Returns the index of the most critical fanin.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+int Res_FilterCriticalFanin( Abc_Obj_t * pNode )
+{
+ Abc_Obj_t * pFanin;
+ int i, iBest = -1, CostMax = 0, CostCur;
+ Abc_ObjForEachFanin( pNode, pFanin, i )
+ {
+ if ( !Abc_ObjIsNode(pFanin) )
+ continue;
+ if ( Abc_ObjFanoutNum(pFanin) > 1 )
+ continue;
+ CostCur = Res_WinVisitMffc( pFanin );
+ if ( CostMax < CostCur )
+ {
+ CostMax = CostCur;
+ iBest = i;
+ }
+ }
+// if ( CostMax > 0 )
+// printf( "<%d>", CostMax );
+ return iBest;
+}
+
+
////////////////////////////////////////////////////////////////////////
/// END OF FILE ///
////////////////////////////////////////////////////////////////////////
diff --git a/src/opt/res/resInt.h b/src/opt/res/resInt.h
index 9d17cb1c..10e312b3 100644
--- a/src/opt/res/resInt.h
+++ b/src/opt/res/resInt.h
@@ -68,9 +68,15 @@ typedef struct Res_Sim_t_ Res_Sim_t;
struct Res_Sim_t_
{
Abc_Ntk_t * pAig; // AIG for simulation
+ int nTruePis; // the number of true PIs of the window
+ int fConst0; // the node can be replaced by constant 0
+ int fConst1; // the node can be replaced by constant 0
// simulation parameters
int nWords; // the number of simulation words
int nPats; // the number of patterns
+ int nWordsIn; // the number of simulation words in the input patterns
+ int nPatsIn; // the number of patterns in the input patterns
+ int nBytesIn; // the number of bytes in the input patterns
int nWordsOut; // the number of simulation words in the output patterns
int nPatsOut; // the number of patterns in the output patterns
// simulation info
@@ -82,6 +88,8 @@ struct Res_Sim_t_
int nPats1; // the number of 1-patterns accumulated
// resub candidates
Vec_Vec_t * vCands; // resubstitution candidates
+ // statistics
+ int timeSat;
};
////////////////////////////////////////////////////////////////////////
@@ -95,15 +103,17 @@ struct Res_Sim_t_
/*=== resDivs.c ==========================================================*/
extern void Res_WinDivisors( Res_Win_t * p, int nLevDivMax );
extern void Res_WinSweepLeafTfo_rec( Abc_Obj_t * pObj, int nLevelLimit );
+extern int Res_WinVisitMffc( Abc_Obj_t * pNode );
/*=== resFilter.c ==========================================================*/
-extern int Res_FilterCandidates( Res_Win_t * pWin, Abc_Ntk_t * pAig, Res_Sim_t * pSim, Vec_Vec_t * vResubs, Vec_Vec_t * vResubsW );
+extern int Res_FilterCandidatesNets( Res_Win_t * pWin, Abc_Ntk_t * pAig, Res_Sim_t * pSim, Vec_Vec_t * vResubs, Vec_Vec_t * vResubsW );
+extern int Res_FilterCandidatesArea( Res_Win_t * pWin, Abc_Ntk_t * pAig, Res_Sim_t * pSim, Vec_Vec_t * vResubs, Vec_Vec_t * vResubsW );
/*=== resSat.c ==========================================================*/
extern void * Res_SatProveUnsat( Abc_Ntk_t * pAig, Vec_Ptr_t * vFanins );
-extern void * Res_SatSimulateConstr( Abc_Ntk_t * pAig, Vec_Ptr_t * vFanins );
+extern int Res_SatSimulate( Res_Sim_t * p, int nPats, int fOnSet );
/*=== resSim.c ==========================================================*/
extern Res_Sim_t * Res_SimAlloc( int nWords );
extern void Res_SimFree( Res_Sim_t * p );
-extern int Res_SimPrepare( Res_Sim_t * p, Abc_Ntk_t * pAig );
+extern int Res_SimPrepare( Res_Sim_t * p, Abc_Ntk_t * pAig, int nTruePis, int fVerbose );
/*=== resStrash.c ==========================================================*/
extern Abc_Ntk_t * Res_WndStrash( Res_Win_t * p );
/*=== resWnd.c ==========================================================*/
diff --git a/src/opt/res/resSat.c b/src/opt/res/resSat.c
index f9558c97..dd0e7a23 100644
--- a/src/opt/res/resSat.c
+++ b/src/opt/res/resSat.c
@@ -128,25 +128,27 @@ void * Res_SatProveUnsat( Abc_Ntk_t * pAig, Vec_Ptr_t * vFanins )
Synopsis [Loads AIG into the SAT solver for constrained simulation.]
- Description [The array of fanins contains exactly two entries: the
- care set and the functions.]
+ Description []
SideEffects []
SeeAlso []
***********************************************************************/
-void * Res_SatSimulateConstr( Abc_Ntk_t * pAig, Vec_Ptr_t * vFanins )
+void * Res_SatSimulateConstr( Abc_Ntk_t * pAig, int fOnSet )
{
sat_solver * pSat;
+ Vec_Ptr_t * vFanins;
Vec_Ptr_t * vNodes;
Abc_Obj_t * pObj;
int i, nNodes;
- // make sure fanins contain POs of the AIG
- pObj = Vec_PtrEntry( vFanins, 0 );
- assert( pObj->pNtk == pAig && Abc_ObjIsPo(pObj) );
- assert( Vec_PtrSize(vFanins) == 2 );
+ // start the array
+ vFanins = Vec_PtrAlloc( 2 );
+ pObj = Abc_NtkPo( pAig, 0 );
+ Vec_PtrPush( vFanins, pObj );
+ pObj = Abc_NtkPo( pAig, 1 );
+ Vec_PtrPush( vFanins, pObj );
// collect reachable nodes
vNodes = Abc_NtkDfsNodes( pAig, (Abc_Obj_t **)vFanins->pArray, vFanins->nSize );
@@ -171,21 +173,154 @@ void * Res_SatSimulateConstr( Abc_Ntk_t * pAig, Vec_Ptr_t * vFanins )
Res_SatAddAnd( pSat, (int)pObj->pCopy,
(int)Abc_ObjFanin0(pObj)->pCopy, (int)Abc_ObjFanin1(pObj)->pCopy, Abc_ObjFaninC0(pObj), Abc_ObjFaninC1(pObj) );
Vec_PtrFree( vNodes );
- // add clauses for POs
- Vec_PtrForEachEntry( vFanins, pObj, i )
- Res_SatAddEqual( pSat, (int)pObj->pCopy,
- (int)Abc_ObjFanin0(pObj)->pCopy, Abc_ObjFaninC0(pObj) );
+ // add clauses for the first PO
+ pObj = Abc_NtkPo( pAig, 0 );
+ Res_SatAddEqual( pSat, (int)pObj->pCopy,
+ (int)Abc_ObjFanin0(pObj)->pCopy, Abc_ObjFaninC0(pObj) );
+ // add clauses for the second PO
+ pObj = Abc_NtkPo( pAig, 1 );
+ Res_SatAddEqual( pSat, (int)pObj->pCopy,
+ (int)Abc_ObjFanin0(pObj)->pCopy, Abc_ObjFaninC0(pObj) );
// add trivial clauses
- pObj = Vec_PtrEntry(vFanins, 0);
+ pObj = Abc_NtkPo( pAig, 0 );
Res_SatAddConst1( pSat, (int)pObj->pCopy, 0 ); // care-set
- pObj = Vec_PtrEntry(vFanins, 1);
- Res_SatAddConst1( pSat, (int)pObj->pCopy, 0 ); // on-set
+
+ pObj = Abc_NtkPo( pAig, 1 );
+ Res_SatAddConst1( pSat, (int)pObj->pCopy, !fOnSet ); // on-set
+
+ Vec_PtrFree( vFanins );
return pSat;
}
/**Function*************************************************************
+ Synopsis [Loads AIG into the SAT solver for constrained simulation.]
+
+ Description [Returns 1 if the required number of patterns are found.
+ Returns 0 if the solver ran out of time or proved a constant.
+ In the latter, case one of the flags, fConst0 or fConst1, are set to 1.]
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+int Res_SatSimulate( Res_Sim_t * p, int nPatsLimit, int fOnSet )
+{
+ Vec_Int_t * vLits;
+ Vec_Ptr_t * vPats;
+ sat_solver * pSat;
+ int RetValue, i, k, value, status, Lit, Var, iPat;
+ int clk = clock();
+
+//printf( "Looking for %s: ", fOnSet? "onset " : "offset" );
+
+ // decide what problem should be solved
+ Lit = toLitCond( (int)Abc_NtkPo(p->pAig,1)->pCopy, !fOnSet );
+ if ( fOnSet )
+ {
+ iPat = p->nPats1;
+ vPats = p->vPats1;
+ }
+ else
+ {
+ iPat = p->nPats0;
+ vPats = p->vPats0;
+ }
+ assert( iPat < nPatsLimit );
+
+ // derive the SAT solver
+ pSat = Res_SatSimulateConstr( p->pAig, fOnSet );
+ pSat->fSkipSimplify = 1;
+ status = sat_solver_simplify( pSat );
+ if ( status == 0 )
+ {
+ if ( iPat == 0 )
+ {
+// if ( fOnSet )
+// p->fConst0 = 1;
+// else
+// p->fConst1 = 1;
+ RetValue = 0;
+ }
+ goto finish;
+ }
+
+ // enumerate through the SAT assignments
+ RetValue = 1;
+ vLits = Vec_IntAlloc( 32 );
+ for ( k = iPat; k < nPatsLimit; k++ )
+ {
+ // solve with the assumption
+// status = sat_solver_solve( pSat, &Lit, &Lit + 1, (sint64)10000, (sint64)0, (sint64)0, (sint64)0 );
+ status = sat_solver_solve( pSat, NULL, NULL, (sint64)10000, (sint64)0, (sint64)0, (sint64)0 );
+ if ( status == l_False )
+ {
+//printf( "Const %d\n", !fOnSet );
+ if ( k == 0 )
+ {
+ if ( fOnSet )
+ p->fConst0 = 1;
+ else
+ p->fConst1 = 1;
+ RetValue = 0;
+ }
+ break;
+ }
+ else if ( status == l_True )
+ {
+ // save the pattern
+ Vec_IntClear( vLits );
+ for ( i = 0; i < p->nTruePis; i++ )
+ {
+ Var = (int)Abc_NtkPi(p->pAig,i)->pCopy;
+ value = (int)(pSat->model.ptr[Var] == l_True);
+ if ( value )
+ Abc_InfoSetBit( Vec_PtrEntry(vPats, i), k );
+ Lit = toLitCond( Var, value );
+ Vec_IntPush( vLits, Lit );
+// printf( "%d", value );
+ }
+// printf( "\n" );
+
+ status = sat_solver_addclause( pSat, Vec_IntArray(vLits), Vec_IntArray(vLits) + Vec_IntSize(vLits) );
+ if ( status == 0 )
+ {
+ k++;
+ RetValue = 1;
+ break;
+ }
+ }
+ else
+ {
+//printf( "Undecided\n" );
+ if ( k == 0 )
+ RetValue = 0;
+ else
+ RetValue = 1;
+ break;
+ }
+ }
+ Vec_IntFree( vLits );
+//printf( "Found %d patterns\n", k - iPat );
+
+ // set the new number of patterns
+ if ( fOnSet )
+ p->nPats1 = k;
+ else
+ p->nPats0 = k;
+
+finish:
+
+ sat_solver_delete( pSat );
+p->timeSat += clock() - clk;
+ return RetValue;
+}
+
+
+/**Function*************************************************************
+
Synopsis [Asserts equality of the variable to a constant.]
Description []
diff --git a/src/opt/res/resSim.c b/src/opt/res/resSim.c
index cc896ec0..5c1dd2b6 100644
--- a/src/opt/res/resSim.c
+++ b/src/opt/res/resSim.c
@@ -47,14 +47,17 @@ Res_Sim_t * Res_SimAlloc( int nWords )
memset( p, 0, sizeof(Res_Sim_t) );
// simulation parameters
p->nWords = nWords;
- p->nPats = 8 * sizeof(unsigned) * p->nWords;
+ p->nPats = p->nWords * 8 * sizeof(unsigned);
+ p->nWordsIn = p->nPats;
+ p->nBytesIn = p->nPats * sizeof(unsigned);
+ p->nPatsIn = p->nPats * 8 * sizeof(unsigned);
p->nWordsOut = p->nPats * p->nWords;
p->nPatsOut = p->nPats * p->nPats;
// simulation info
- p->vPats = Vec_PtrAllocSimInfo( 1024, p->nWords );
- p->vPats0 = Vec_PtrAllocSimInfo( 128, p->nWords );
- p->vPats1 = Vec_PtrAllocSimInfo( 128, p->nWords );
- p->vOuts = Vec_PtrAllocSimInfo( 128, p->nWordsOut );
+ p->vPats = Vec_PtrAllocSimInfo( 1024, p->nWordsIn );
+ p->vPats0 = Vec_PtrAllocSimInfo( 128, p->nWords );
+ p->vPats1 = Vec_PtrAllocSimInfo( 128, p->nWords );
+ p->vOuts = Vec_PtrAllocSimInfo( 128, p->nWordsOut );
// resub candidates
p->vCands = Vec_VecStart( 16 );
return p;
@@ -71,26 +74,27 @@ Res_Sim_t * Res_SimAlloc( int nWords )
SeeAlso []
***********************************************************************/
-void Res_SimAdjust( Res_Sim_t * p, Abc_Ntk_t * pAig )
+void Res_SimAdjust( Res_Sim_t * p, Abc_Ntk_t * pAig, int nTruePis )
{
srand( 0xABC );
assert( Abc_NtkIsStrash(pAig) );
p->pAig = pAig;
+ p->nTruePis = nTruePis;
if ( Vec_PtrSize(p->vPats) < Abc_NtkObjNumMax(pAig)+1 )
{
Vec_PtrFree( p->vPats );
- p->vPats = Vec_PtrAllocSimInfo( Abc_NtkObjNumMax(pAig)+1, p->nWords );
+ p->vPats = Vec_PtrAllocSimInfo( Abc_NtkObjNumMax(pAig)+1, p->nWordsIn );
}
- if ( Vec_PtrSize(p->vPats0) < Abc_NtkPiNum(pAig) )
+ if ( Vec_PtrSize(p->vPats0) < nTruePis )
{
Vec_PtrFree( p->vPats0 );
- p->vPats0 = Vec_PtrAllocSimInfo( Abc_NtkPiNum(pAig), p->nWords );
+ p->vPats0 = Vec_PtrAllocSimInfo( nTruePis, p->nWords );
}
- if ( Vec_PtrSize(p->vPats1) < Abc_NtkPiNum(pAig) )
+ if ( Vec_PtrSize(p->vPats1) < nTruePis )
{
Vec_PtrFree( p->vPats1 );
- p->vPats1 = Vec_PtrAllocSimInfo( Abc_NtkPiNum(pAig), p->nWords );
+ p->vPats1 = Vec_PtrAllocSimInfo( nTruePis, p->nWords );
}
if ( Vec_PtrSize(p->vOuts) < Abc_NtkPoNum(pAig) )
{
@@ -98,10 +102,12 @@ void Res_SimAdjust( Res_Sim_t * p, Abc_Ntk_t * pAig )
p->vOuts = Vec_PtrAllocSimInfo( Abc_NtkPoNum(pAig), p->nWordsOut );
}
// clean storage info for patterns
- Abc_InfoClear( Vec_PtrEntry(p->vPats0,0), p->nWords * Abc_NtkPiNum(pAig) );
- Abc_InfoClear( Vec_PtrEntry(p->vPats1,0), p->nWords * Abc_NtkPiNum(pAig) );
+ Abc_InfoClear( Vec_PtrEntry(p->vPats0,0), p->nWords * nTruePis );
+ Abc_InfoClear( Vec_PtrEntry(p->vPats1,0), p->nWords * nTruePis );
p->nPats0 = 0;
p->nPats1 = 0;
+ p->fConst0 = 0;
+ p->fConst1 = 0;
}
/**Function*************************************************************
@@ -137,7 +143,32 @@ void Res_SimFree( Res_Sim_t * p )
SeeAlso []
***********************************************************************/
-void Res_SimSetRandom( Res_Sim_t * p )
+void Abc_InfoRandomBytes( unsigned * p, int nWords )
+{
+ int i, Num;
+ for ( i = nWords - 1; i >= 0; i-- )
+ {
+ Num = rand();
+ p[i] = (Num & 1)? 0xff : 0;
+ p[i] = (p[i] << 8) | ((Num & 2)? 0xff : 0);
+ p[i] = (p[i] << 8) | ((Num & 4)? 0xff : 0);
+ p[i] = (p[i] << 8) | ((Num & 8)? 0xff : 0);
+ }
+// Extra_PrintBinary( stdout, p, 32 ); printf( "\n" );
+}
+
+/**Function*************************************************************
+
+ Synopsis [Sets random PI simulation info.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+void Res_SimSetRandomBytes( Res_Sim_t * p )
{
Abc_Obj_t * pObj;
unsigned * pInfo;
@@ -145,8 +176,155 @@ void Res_SimSetRandom( Res_Sim_t * p )
Abc_NtkForEachPi( p->pAig, pObj, i )
{
pInfo = Vec_PtrEntry( p->vPats, pObj->Id );
- Abc_InfoRandom( pInfo, p->nWords );
+ if ( i < p->nTruePis )
+ Abc_InfoRandomBytes( pInfo, p->nWordsIn );
+ else
+ Abc_InfoRandom( pInfo, p->nWordsIn );
}
+/*
+ // double-check that all are byte-patterns
+ Abc_NtkForEachPi( p->pAig, pObj, i )
+ {
+ if ( i == p->nTruePis )
+ break;
+ pInfoC = (unsigned char *)Vec_PtrEntry( p->vPats, pObj->Id );
+ for ( k = 0; k < p->nBytesIn; k++ )
+ assert( pInfoC[k] == 0 || pInfoC[k] == 0xff );
+ }
+*/
+}
+
+/**Function*************************************************************
+
+ Synopsis [Sets random PI simulation info.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+void Res_SimSetDerivedBytes( Res_Sim_t * p, int fUseWalk )
+{
+ Vec_Ptr_t * vPatsSource[2];
+ int nPatsSource[2];
+ Abc_Obj_t * pObj;
+ unsigned char * pInfo;
+ int i, k, z, s, nPats;
+
+ // set several random patterns
+ assert( p->nBytesIn % 32 == 0 );
+ nPats = p->nBytesIn/8;
+ Abc_NtkForEachPi( p->pAig, pObj, i )
+ {
+ if ( i == p->nTruePis )
+ break;
+ Abc_InfoRandomBytes( Vec_PtrEntry(p->vPats, pObj->Id), nPats/4 );
+ }
+
+ // set special patterns
+ if ( fUseWalk )
+ {
+ for ( z = 0; z < 2; z++ )
+ {
+ // set the zero pattern
+ Abc_NtkForEachPi( p->pAig, pObj, i )
+ {
+ if ( i == p->nTruePis )
+ break;
+ pInfo = (unsigned char *)Vec_PtrEntry( p->vPats, pObj->Id );
+ pInfo[nPats] = z ? 0xff : 0;
+ }
+ if ( ++nPats == p->nBytesIn )
+ return;
+ // set the walking zero pattern
+ for ( k = 0; k < p->nTruePis; k++ )
+ {
+ Abc_NtkForEachPi( p->pAig, pObj, i )
+ {
+ if ( i == p->nTruePis )
+ break;
+ pInfo = (unsigned char *)Vec_PtrEntry( p->vPats, pObj->Id );
+ pInfo[nPats] = ((i == k) ^ z) ? 0xff : 0;
+ }
+ if ( ++nPats == p->nBytesIn )
+ return;
+ }
+ }
+ }
+
+ // decide what patterns to set first
+ if ( p->nPats0 < p->nPats1 )
+ {
+ nPatsSource[0] = p->nPats0;
+ vPatsSource[0] = p->vPats0;
+ nPatsSource[1] = p->nPats1;
+ vPatsSource[1] = p->vPats1;
+ }
+ else
+ {
+ nPatsSource[0] = p->nPats1;
+ vPatsSource[0] = p->vPats1;
+ nPatsSource[1] = p->nPats0;
+ vPatsSource[1] = p->vPats0;
+ }
+ for ( z = 0; z < 2; z++ )
+ {
+ for ( s = nPatsSource[z] - 1; s >= 0; s-- )
+ {
+// if ( s == 0 )
+// printf( "Patterns:\n" );
+ // set the given source pattern
+ for ( k = 0; k < p->nTruePis; k++ )
+ {
+ Abc_NtkForEachPi( p->pAig, pObj, i )
+ {
+ if ( i == p->nTruePis )
+ break;
+ pInfo = (unsigned char *)Vec_PtrEntry( p->vPats, pObj->Id );
+ if ( (i == k) ^ Abc_InfoHasBit( Vec_PtrEntry(vPatsSource[z], i), s ) )
+ {
+ pInfo[nPats] = 0xff;
+// if ( s == 0 )
+// printf( "1" );
+ }
+ else
+ {
+ pInfo[nPats] = 0;
+// if ( s == 0 )
+// printf( "0" );
+ }
+ }
+// if ( s == 0 )
+// printf( "\n" );
+ if ( ++nPats == p->nBytesIn )
+ return;
+ }
+ }
+ }
+ // clean the rest
+ for ( z = nPats; z < p->nBytesIn; z++ )
+ {
+ Abc_NtkForEachPi( p->pAig, pObj, i )
+ {
+ if ( i == p->nTruePis )
+ break;
+ pInfo = (unsigned char *)Vec_PtrEntry( p->vPats, pObj->Id );
+ memset( pInfo + nPats, 0, p->nBytesIn - nPats );
+ }
+ }
+/*
+ // double-check that all are byte-patterns
+ Abc_NtkForEachPi( p->pAig, pObj, i )
+ {
+ if ( i == p->nTruePis )
+ break;
+ pInfo = (unsigned char *)Vec_PtrEntry( p->vPats, pObj->Id );
+ for ( k = 0; k < p->nBytesIn; k++ )
+ assert( pInfo[k] == 0 || pInfo[k] == 0xff );
+ }
+*/
}
/**Function*************************************************************
@@ -167,6 +345,8 @@ void Res_SimSetGiven( Res_Sim_t * p, Vec_Ptr_t * vInfo )
int i, w;
Abc_NtkForEachPi( p->pAig, pObj, i )
{
+ if ( i == p->nTruePis )
+ break;
pInfo = Vec_PtrEntry( p->vPats, pObj->Id );
pInfo2 = Vec_PtrEntry( vInfo, i );
for ( w = 0; w < p->nWords; w++ )
@@ -249,64 +429,17 @@ void Res_SimTransferOne( Abc_Obj_t * pNode, Vec_Ptr_t * vSimInfo, int nSimWords
SeeAlso []
***********************************************************************/
-void Res_SimPerformRound( Res_Sim_t * p )
+void Res_SimPerformRound( Res_Sim_t * p, int nWords )
{
Abc_Obj_t * pObj;
int i;
- Abc_InfoFill( Vec_PtrEntry(p->vPats,0), p->nWords );
+ Abc_InfoFill( Vec_PtrEntry(p->vPats,0), nWords );
Abc_AigForEachAnd( p->pAig, pObj, i )
- Res_SimPerformOne( pObj, p->vPats, p->nWords );
+ Res_SimPerformOne( pObj, p->vPats, nWords );
Abc_NtkForEachPo( p->pAig, pObj, i )
- Res_SimTransferOne( pObj, p->vPats, p->nWords );
+ Res_SimTransferOne( pObj, p->vPats, nWords );
}
-/**Function*************************************************************
-
- Synopsis [Processes simulation patterns.]
-
- Description []
-
- SideEffects []
-
- SeeAlso []
-
-***********************************************************************/
-void Res_SimProcessPats( Res_Sim_t * p )
-{
- Abc_Obj_t * pObj;
- unsigned * pInfoCare, * pInfoNode;
- int i, j, nDcs = 0;
- pInfoCare = Vec_PtrEntry( p->vPats, Abc_NtkPo(p->pAig, 0)->Id );
- pInfoNode = Vec_PtrEntry( p->vPats, Abc_NtkPo(p->pAig, 1)->Id );
- for ( i = 0; i < p->nPats; i++ )
- {
- // skip don't-care patterns
- if ( !Abc_InfoHasBit(pInfoCare, i) )
- {
- nDcs++;
- continue;
- }
- // separate offset and onset patterns
- if ( !Abc_InfoHasBit(pInfoNode, i) )
- {
- if ( p->nPats0 >= p->nPats )
- continue;
- Abc_NtkForEachPi( p->pAig, pObj, j )
- if ( Abc_InfoHasBit( Vec_PtrEntry(p->vPats, pObj->Id), i ) )
- Abc_InfoSetBit( Vec_PtrEntry(p->vPats0, j), p->nPats0 );
- p->nPats0++;
- }
- else
- {
- if ( p->nPats1 >= p->nPats )
- continue;
- Abc_NtkForEachPi( p->pAig, pObj, j )
- if ( Abc_InfoHasBit( Vec_PtrEntry(p->vPats, pObj->Id), i ) )
- Abc_InfoSetBit( Vec_PtrEntry(p->vPats1, j), p->nPats1 );
- p->nPats1++;
- }
- }
-}
/**Function*************************************************************
@@ -396,7 +529,50 @@ void Res_SimDeriveInfoComplement( Res_Sim_t * p )
/**Function*************************************************************
- Synopsis [Free simulation engine.]
+ Synopsis [Prints output patterns.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+void Res_SimPrintOutPatterns( Res_Sim_t * p, Abc_Ntk_t * pAig )
+{
+ Abc_Obj_t * pObj;
+ unsigned * pInfo2;
+ int i;
+ Abc_NtkForEachPo( pAig, pObj, i )
+ {
+ pInfo2 = Vec_PtrEntry( p->vOuts, i );
+ Extra_PrintBinary( stdout, pInfo2, p->nPatsOut );
+ printf( "\n" );
+ }
+}
+
+/**Function*************************************************************
+
+ Synopsis [Prints output patterns.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+void Res_SimPrintNodePatterns( Res_Sim_t * p, Abc_Ntk_t * pAig )
+{
+ unsigned * pInfo;
+ pInfo = Vec_PtrEntry( p->vPats, Abc_NtkPo(p->pAig, 1)->Id );
+ Extra_PrintBinary( stdout, pInfo, p->nPats );
+ printf( "\n" );
+}
+
+/**Function*************************************************************
+
+ Synopsis [Counts the number of patters of different type.]
Description []
@@ -405,40 +581,102 @@ void Res_SimDeriveInfoComplement( Res_Sim_t * p )
SeeAlso []
***********************************************************************/
-void Res_SimReportOne( Res_Sim_t * p )
+void Res_SimCountResults( Res_Sim_t * p, int * pnDcs, int * pnOnes, int * pnZeros, int fVerbose )
{
- unsigned * pInfoCare, * pInfoNode;
- int i, nDcs, nOnes, nZeros;
- pInfoCare = Vec_PtrEntry( p->vPats, Abc_NtkPo(p->pAig, 0)->Id );
- pInfoNode = Vec_PtrEntry( p->vPats, Abc_NtkPo(p->pAig, 1)->Id );
- nDcs = nOnes = nZeros = 0;
- for ( i = 0; i < p->nPats; i++ )
+ unsigned char * pInfoCare, * pInfoNode;
+ int i, nTotal = 0;
+ pInfoCare = (unsigned char *)Vec_PtrEntry( p->vPats, Abc_NtkPo(p->pAig, 0)->Id );
+ pInfoNode = (unsigned char *)Vec_PtrEntry( p->vPats, Abc_NtkPo(p->pAig, 1)->Id );
+ for ( i = 0; i < p->nBytesIn; i++ )
+ {
+ if ( !pInfoCare[i] )
+ (*pnDcs)++;
+ else if ( !pInfoNode[i] )
+ (*pnZeros)++;
+ else
+ (*pnOnes)++;
+ }
+ nTotal += *pnDcs;
+ nTotal += *pnZeros;
+ nTotal += *pnOnes;
+ if ( fVerbose )
+ {
+ printf( "Dc = %7.2f %% ", 100.0*(*pnDcs) /nTotal );
+ printf( "On = %7.2f %% ", 100.0*(*pnOnes) /nTotal );
+ printf( "Off = %7.2f %% ", 100.0*(*pnZeros)/nTotal );
+ }
+}
+
+/**Function*************************************************************
+
+ Synopsis [Counts the number of patters of different type.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+void Res_SimCollectPatterns( Res_Sim_t * p, int fVerbose )
+{
+ Abc_Obj_t * pObj;
+ unsigned char * pInfoCare, * pInfoNode, * pInfo;
+ int i, j;
+ pInfoCare = (unsigned char *)Vec_PtrEntry( p->vPats, Abc_NtkPo(p->pAig, 0)->Id );
+ pInfoNode = (unsigned char *)Vec_PtrEntry( p->vPats, Abc_NtkPo(p->pAig, 1)->Id );
+ for ( i = 0; i < p->nBytesIn; i++ )
{
// skip don't-care patterns
- if ( !Abc_InfoHasBit(pInfoCare, i) )
- {
- nDcs++;
+ if ( !pInfoCare[i] )
continue;
- }
// separate offset and onset patterns
- if ( !Abc_InfoHasBit(pInfoNode, i) )
- nZeros++;
+ assert( pInfoNode[i] == 0 || pInfoNode[i] == 0xff );
+ if ( !pInfoNode[i] )
+ {
+ if ( p->nPats0 >= p->nPats )
+ continue;
+ Abc_NtkForEachPi( p->pAig, pObj, j )
+ {
+ if ( j == p->nTruePis )
+ break;
+ pInfo = (unsigned char *)Vec_PtrEntry( p->vPats, pObj->Id );
+ assert( pInfo[i] == 0 || pInfo[i] == 0xff );
+ if ( pInfo[i] )
+ Abc_InfoSetBit( Vec_PtrEntry(p->vPats0, j), p->nPats0 );
+ }
+ p->nPats0++;
+ }
else
- nOnes++;
+ {
+ if ( p->nPats1 >= p->nPats )
+ continue;
+ Abc_NtkForEachPi( p->pAig, pObj, j )
+ {
+ if ( j == p->nTruePis )
+ break;
+ pInfo = (unsigned char *)Vec_PtrEntry( p->vPats, pObj->Id );
+ assert( pInfo[i] == 0 || pInfo[i] == 0xff );
+ if ( pInfo[i] )
+ Abc_InfoSetBit( Vec_PtrEntry(p->vPats1, j), p->nPats1 );
+ }
+ p->nPats1++;
+ }
+ if ( p->nPats0 >= p->nPats && p->nPats1 >= p->nPats )
+ break;
+ }
+ if ( fVerbose )
+ {
+ printf( "| " );
+ printf( "On = %3d ", p->nPats1 );
+ printf( "Off = %3d ", p->nPats0 );
+ printf( "\n" );
}
- printf( "On = %3d (%7.2f %%) ", nOnes, 100.0*nOnes/p->nPats );
- printf( "Off = %3d (%7.2f %%) ", nZeros, 100.0*nZeros/p->nPats );
- printf( "Dc = %3d (%7.2f %%) ", nDcs, 100.0*nDcs/p->nPats );
- printf( "P0 = %3d ", p->nPats0 );
- printf( "P1 = %3d ", p->nPats1 );
- if ( p->nPats0 < 4 || p->nPats1 < 4 )
- printf( "*" );
- printf( "\n" );
}
/**Function*************************************************************
- Synopsis [Prints output patterns.]
+ Synopsis [Verifies the last pattern.]
Description []
@@ -447,17 +685,33 @@ void Res_SimReportOne( Res_Sim_t * p )
SeeAlso []
***********************************************************************/
-void Res_SimPrintOutPatterns( Res_Sim_t * p, Abc_Ntk_t * pAig )
+int Res_SimVerifyValue( Res_Sim_t * p, int fOnSet )
{
Abc_Obj_t * pObj;
- unsigned * pInfo2;
- int i;
- Abc_NtkForEachPo( pAig, pObj, i )
+ unsigned * pInfo, * pInfo2;
+ int i, value;
+ Abc_NtkForEachPi( p->pAig, pObj, i )
{
- pInfo2 = Vec_PtrEntry( p->vOuts, i );
- Extra_PrintBinary( stdout, pInfo2, p->nPatsOut );
- printf( "\n" );
+ if ( i == p->nTruePis )
+ break;
+ if ( fOnSet )
+ {
+ pInfo2 = Vec_PtrEntry( p->vPats1, i );
+ value = Abc_InfoHasBit( pInfo2, p->nPats1 - 1 );
+ }
+ else
+ {
+ pInfo2 = Vec_PtrEntry( p->vPats0, i );
+ value = Abc_InfoHasBit( pInfo2, p->nPats0 - 1 );
+ }
+ pInfo = Vec_PtrEntry( p->vPats, pObj->Id );
+ pInfo[0] = value ? ~0 : 0;
}
+ Res_SimPerformRound( p, 1 );
+ pObj = Abc_NtkPo( p->pAig, 1 );
+ pInfo = Vec_PtrEntry( p->vPats, pObj->Id );
+ assert( pInfo[0] == 0 || pInfo[0] == ~0 );
+ return pInfo[0] > 0;
}
/**Function*************************************************************
@@ -471,30 +725,43 @@ void Res_SimPrintOutPatterns( Res_Sim_t * p, Abc_Ntk_t * pAig )
SeeAlso []
***********************************************************************/
-int Res_SimPrepare( Res_Sim_t * p, Abc_Ntk_t * pAig )
+int Res_SimPrepare( Res_Sim_t * p, Abc_Ntk_t * pAig, int nTruePis, int fVerbose )
{
- int Limit;
+ int i, nOnes = 0, nZeros = 0, nDcs = 0;
+ if ( fVerbose )
+ printf( "\n" );
// prepare the manager
- Res_SimAdjust( p, pAig );
- // collect 0/1 simulation info
- for ( Limit = 0; Limit < 10; Limit++ )
+ Res_SimAdjust( p, pAig, nTruePis );
+ // estimate the number of patterns
+ Res_SimSetRandomBytes( p );
+ Res_SimPerformRound( p, p->nWordsIn );
+ Res_SimCountResults( p, &nDcs, &nOnes, &nZeros, fVerbose );
+ // collect the patterns
+ Res_SimCollectPatterns( p, fVerbose );
+ // add more patterns using constraint simulation
+ if ( p->nPats0 < 8 )
{
- Res_SimSetRandom( p );
- Res_SimPerformRound( p );
- Res_SimProcessPats( p );
- if ( !(p->nPats0 < p->nPats || p->nPats1 < p->nPats) )
- break;
+ if ( !Res_SatSimulate( p, 16, 0 ) )
+ return p->fConst0 || p->fConst1;
+// return 0;
+// printf( "Value0 = %d\n", Res_SimVerifyValue( p, 0 ) );
}
-// printf( "%d ", Limit );
- // report the last set of patterns
-// Res_SimReportOne( p );
-// printf( "\n" );
- // quit if there is not enough
-// if ( p->nPats0 < 4 || p->nPats1 < 4 )
- if ( p->nPats0 < 4 || p->nPats1 < 4 )
+ if ( p->nPats1 < 8 )
{
-// Res_SimReportOne( p );
- return 0;
+ if ( !Res_SatSimulate( p, 16, 1 ) )
+ return p->fConst0 || p->fConst1;
+// return 0;
+// printf( "Value1 = %d\n", Res_SimVerifyValue( p, 1 ) );
+ }
+ // generate additional patterns
+ for ( i = 0; i < 2; i++ )
+ {
+ if ( p->nPats0 > p->nPats*7/8 && p->nPats1 > p->nPats*7/8 )
+ break;
+ Res_SimSetDerivedBytes( p, i==0 );
+ Res_SimPerformRound( p, p->nWordsIn );
+ Res_SimCountResults( p, &nDcs, &nOnes, &nZeros, fVerbose );
+ Res_SimCollectPatterns( p, fVerbose );
}
// create bit-matrix info
if ( p->nPats0 < p->nPats )
@@ -503,11 +770,13 @@ int Res_SimPrepare( Res_Sim_t * p, Abc_Ntk_t * pAig )
Res_SimPadSimInfo( p->vPats1, p->nPats1, p->nWords );
// resimulate 0-patterns
Res_SimSetGiven( p, p->vPats0 );
- Res_SimPerformRound( p );
+ Res_SimPerformRound( p, p->nWords );
+//Res_SimPrintNodePatterns( p, pAig );
Res_SimDeriveInfoReplicate( p );
// resimulate 1-patterns
Res_SimSetGiven( p, p->vPats1 );
- Res_SimPerformRound( p );
+ Res_SimPerformRound( p, p->nWords );
+//Res_SimPrintNodePatterns( p, pAig );
Res_SimDeriveInfoComplement( p );
// print output patterns
// Res_SimPrintOutPatterns( p, pAig );
diff --git a/src/opt/res/resSim_old.c b/src/opt/res/resSim_old.c
new file mode 100644
index 00000000..23ce29e4
--- /dev/null
+++ b/src/opt/res/resSim_old.c
@@ -0,0 +1,521 @@
+/**CFile****************************************************************
+
+ FileName [resSim.c]
+
+ SystemName [ABC: Logic synthesis and verification system.]
+
+ PackageName [Resynthesis package.]
+
+ Synopsis [Simulation engine.]
+
+ Author [Alan Mishchenko]
+
+ Affiliation [UC Berkeley]
+
+ Date [Ver. 1.0. Started - January 15, 2007.]
+
+ Revision [$Id: resSim.c,v 1.00 2007/01/15 00:00:00 alanmi Exp $]
+
+***********************************************************************/
+
+#include "abc.h"
+#include "resInt.h"
+
+////////////////////////////////////////////////////////////////////////
+/// DECLARATIONS ///
+////////////////////////////////////////////////////////////////////////
+
+////////////////////////////////////////////////////////////////////////
+/// FUNCTION DEFINITIONS ///
+////////////////////////////////////////////////////////////////////////
+
+/**Function*************************************************************
+
+ Synopsis [Allocate simulation engine.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+Res_Sim_t * Res_SimAlloc( int nWords )
+{
+ Res_Sim_t * p;
+ p = ALLOC( Res_Sim_t, 1 );
+ memset( p, 0, sizeof(Res_Sim_t) );
+ // simulation parameters
+ p->nWords = nWords;
+ p->nPats = 8 * sizeof(unsigned) * p->nWords;
+ p->nWordsOut = p->nPats * p->nWords;
+ p->nPatsOut = p->nPats * p->nPats;
+ // simulation info
+ p->vPats = Vec_PtrAllocSimInfo( 1024, p->nWords );
+ p->vPats0 = Vec_PtrAllocSimInfo( 128, p->nWords );
+ p->vPats1 = Vec_PtrAllocSimInfo( 128, p->nWords );
+ p->vOuts = Vec_PtrAllocSimInfo( 128, p->nWordsOut );
+ // resub candidates
+ p->vCands = Vec_VecStart( 16 );
+ return p;
+}
+
+/**Function*************************************************************
+
+ Synopsis [Allocate simulation engine.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+void Res_SimAdjust( Res_Sim_t * p, Abc_Ntk_t * pAig )
+{
+ srand( 0xABC );
+
+ assert( Abc_NtkIsStrash(pAig) );
+ p->pAig = pAig;
+ if ( Vec_PtrSize(p->vPats) < Abc_NtkObjNumMax(pAig)+1 )
+ {
+ Vec_PtrFree( p->vPats );
+ p->vPats = Vec_PtrAllocSimInfo( Abc_NtkObjNumMax(pAig)+1, p->nWords );
+ }
+ if ( Vec_PtrSize(p->vPats0) < Abc_NtkPiNum(pAig) )
+ {
+ Vec_PtrFree( p->vPats0 );
+ p->vPats0 = Vec_PtrAllocSimInfo( Abc_NtkPiNum(pAig), p->nWords );
+ }
+ if ( Vec_PtrSize(p->vPats1) < Abc_NtkPiNum(pAig) )
+ {
+ Vec_PtrFree( p->vPats1 );
+ p->vPats1 = Vec_PtrAllocSimInfo( Abc_NtkPiNum(pAig), p->nWords );
+ }
+ if ( Vec_PtrSize(p->vOuts) < Abc_NtkPoNum(pAig) )
+ {
+ Vec_PtrFree( p->vOuts );
+ p->vOuts = Vec_PtrAllocSimInfo( Abc_NtkPoNum(pAig), p->nWordsOut );
+ }
+ // clean storage info for patterns
+ Abc_InfoClear( Vec_PtrEntry(p->vPats0,0), p->nWords * Abc_NtkPiNum(pAig) );
+ Abc_InfoClear( Vec_PtrEntry(p->vPats1,0), p->nWords * Abc_NtkPiNum(pAig) );
+ p->nPats0 = 0;
+ p->nPats1 = 0;
+}
+
+/**Function*************************************************************
+
+ Synopsis [Free simulation engine.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+void Res_SimFree( Res_Sim_t * p )
+{
+ Vec_PtrFree( p->vPats );
+ Vec_PtrFree( p->vPats0 );
+ Vec_PtrFree( p->vPats1 );
+ Vec_PtrFree( p->vOuts );
+ Vec_VecFree( p->vCands );
+ free( p );
+}
+
+
+/**Function*************************************************************
+
+ Synopsis [Sets random PI simulation info.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+void Res_SimSetRandom( Res_Sim_t * p )
+{
+ Abc_Obj_t * pObj;
+ unsigned * pInfo;
+ int i;
+ Abc_NtkForEachPi( p->pAig, pObj, i )
+ {
+ pInfo = Vec_PtrEntry( p->vPats, pObj->Id );
+ Abc_InfoRandom( pInfo, p->nWords );
+ }
+}
+
+/**Function*************************************************************
+
+ Synopsis [Sets given PI simulation info.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+void Res_SimSetGiven( Res_Sim_t * p, Vec_Ptr_t * vInfo )
+{
+ Abc_Obj_t * pObj;
+ unsigned * pInfo, * pInfo2;
+ int i, w;
+ Abc_NtkForEachPi( p->pAig, pObj, i )
+ {
+ pInfo = Vec_PtrEntry( p->vPats, pObj->Id );
+ pInfo2 = Vec_PtrEntry( vInfo, i );
+ for ( w = 0; w < p->nWords; w++ )
+ pInfo[w] = pInfo2[w];
+ }
+}
+
+/**Function*************************************************************
+
+ Synopsis [Simulates one node.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+void Res_SimPerformOne( Abc_Obj_t * pNode, Vec_Ptr_t * vSimInfo, int nSimWords )
+{
+ unsigned * pInfo, * pInfo1, * pInfo2;
+ int k, fComp1, fComp2;
+ // simulate the internal nodes
+ assert( Abc_ObjIsNode(pNode) );
+ pInfo = Vec_PtrEntry(vSimInfo, pNode->Id);
+ pInfo1 = Vec_PtrEntry(vSimInfo, Abc_ObjFaninId0(pNode));
+ pInfo2 = Vec_PtrEntry(vSimInfo, Abc_ObjFaninId1(pNode));
+ fComp1 = Abc_ObjFaninC0(pNode);
+ fComp2 = Abc_ObjFaninC1(pNode);
+ if ( fComp1 && fComp2 )
+ for ( k = 0; k < nSimWords; k++ )
+ pInfo[k] = ~pInfo1[k] & ~pInfo2[k];
+ else if ( fComp1 && !fComp2 )
+ for ( k = 0; k < nSimWords; k++ )
+ pInfo[k] = ~pInfo1[k] & pInfo2[k];
+ else if ( !fComp1 && fComp2 )
+ for ( k = 0; k < nSimWords; k++ )
+ pInfo[k] = pInfo1[k] & ~pInfo2[k];
+ else // if ( fComp1 && fComp2 )
+ for ( k = 0; k < nSimWords; k++ )
+ pInfo[k] = pInfo1[k] & pInfo2[k];
+}
+
+/**Function*************************************************************
+
+ Synopsis [Simulates one CO node.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+void Res_SimTransferOne( Abc_Obj_t * pNode, Vec_Ptr_t * vSimInfo, int nSimWords )
+{
+ unsigned * pInfo, * pInfo1;
+ int k, fComp1;
+ // simulate the internal nodes
+ assert( Abc_ObjIsCo(pNode) );
+ pInfo = Vec_PtrEntry(vSimInfo, pNode->Id);
+ pInfo1 = Vec_PtrEntry(vSimInfo, Abc_ObjFaninId0(pNode));
+ fComp1 = Abc_ObjFaninC0(pNode);
+ if ( fComp1 )
+ for ( k = 0; k < nSimWords; k++ )
+ pInfo[k] = ~pInfo1[k];
+ else
+ for ( k = 0; k < nSimWords; k++ )
+ pInfo[k] = pInfo1[k];
+}
+
+/**Function*************************************************************
+
+ Synopsis [Performs one round of simulation.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+void Res_SimPerformRound( Res_Sim_t * p )
+{
+ Abc_Obj_t * pObj;
+ int i;
+ Abc_InfoFill( Vec_PtrEntry(p->vPats,0), p->nWords );
+ Abc_AigForEachAnd( p->pAig, pObj, i )
+ Res_SimPerformOne( pObj, p->vPats, p->nWords );
+ Abc_NtkForEachPo( p->pAig, pObj, i )
+ Res_SimTransferOne( pObj, p->vPats, p->nWords );
+}
+
+/**Function*************************************************************
+
+ Synopsis [Processes simulation patterns.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+void Res_SimProcessPats( Res_Sim_t * p )
+{
+ Abc_Obj_t * pObj;
+ unsigned * pInfoCare, * pInfoNode;
+ int i, j, nDcs = 0;
+ pInfoCare = Vec_PtrEntry( p->vPats, Abc_NtkPo(p->pAig, 0)->Id );
+ pInfoNode = Vec_PtrEntry( p->vPats, Abc_NtkPo(p->pAig, 1)->Id );
+ for ( i = 0; i < p->nPats; i++ )
+ {
+ // skip don't-care patterns
+ if ( !Abc_InfoHasBit(pInfoCare, i) )
+ {
+ nDcs++;
+ continue;
+ }
+ // separate offset and onset patterns
+ if ( !Abc_InfoHasBit(pInfoNode, i) )
+ {
+ if ( p->nPats0 >= p->nPats )
+ continue;
+ Abc_NtkForEachPi( p->pAig, pObj, j )
+ if ( Abc_InfoHasBit( Vec_PtrEntry(p->vPats, pObj->Id), i ) )
+ Abc_InfoSetBit( Vec_PtrEntry(p->vPats0, j), p->nPats0 );
+ p->nPats0++;
+ }
+ else
+ {
+ if ( p->nPats1 >= p->nPats )
+ continue;
+ Abc_NtkForEachPi( p->pAig, pObj, j )
+ if ( Abc_InfoHasBit( Vec_PtrEntry(p->vPats, pObj->Id), i ) )
+ Abc_InfoSetBit( Vec_PtrEntry(p->vPats1, j), p->nPats1 );
+ p->nPats1++;
+ }
+ }
+}
+
+/**Function*************************************************************
+
+ Synopsis [Pads the extra space with duplicated simulation info.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+void Res_SimPadSimInfo( Vec_Ptr_t * vPats, int nPats, int nWords )
+{
+ unsigned * pInfo;
+ int i, w, iWords;
+ assert( nPats > 0 && nPats < nWords * 8 * (int) sizeof(unsigned) );
+ // pad the first word
+ if ( nPats < 8 * sizeof(unsigned) )
+ {
+ Vec_PtrForEachEntry( vPats, pInfo, i )
+ if ( pInfo[0] & 1 )
+ pInfo[0] |= ((~0) << nPats);
+ nPats = 8 * sizeof(unsigned);
+ }
+ // pad the empty words
+ iWords = nPats / (8 * sizeof(unsigned));
+ Vec_PtrForEachEntry( vPats, pInfo, i )
+ {
+ for ( w = iWords; w < nWords; w++ )
+ pInfo[w] = pInfo[0];
+ }
+}
+
+/**Function*************************************************************
+
+ Synopsis [Duplicates the simulation info to fill the space.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+void Res_SimDeriveInfoReplicate( Res_Sim_t * p )
+{
+ unsigned * pInfo, * pInfo2;
+ Abc_Obj_t * pObj;
+ int i, j, w;
+ Abc_NtkForEachPo( p->pAig, pObj, i )
+ {
+ pInfo = Vec_PtrEntry( p->vPats, pObj->Id );
+ pInfo2 = Vec_PtrEntry( p->vOuts, i );
+ for ( j = 0; j < p->nPats; j++ )
+ for ( w = 0; w < p->nWords; w++ )
+ *pInfo2++ = pInfo[w];
+ }
+}
+
+/**Function*************************************************************
+
+ Synopsis [Complement the simulation info if necessary.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+void Res_SimDeriveInfoComplement( Res_Sim_t * p )
+{
+ unsigned * pInfo, * pInfo2;
+ Abc_Obj_t * pObj;
+ int i, j, w;
+ Abc_NtkForEachPo( p->pAig, pObj, i )
+ {
+ pInfo = Vec_PtrEntry( p->vPats, pObj->Id );
+ pInfo2 = Vec_PtrEntry( p->vOuts, i );
+ for ( j = 0; j < p->nPats; j++, pInfo2 += p->nWords )
+ if ( Abc_InfoHasBit( pInfo, j ) )
+ for ( w = 0; w < p->nWords; w++ )
+ pInfo2[w] = ~pInfo2[w];
+ }
+}
+
+/**Function*************************************************************
+
+ Synopsis [Free simulation engine.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+void Res_SimReportOne( Res_Sim_t * p )
+{
+ unsigned * pInfoCare, * pInfoNode;
+ int i, nDcs, nOnes, nZeros;
+ pInfoCare = Vec_PtrEntry( p->vPats, Abc_NtkPo(p->pAig, 0)->Id );
+ pInfoNode = Vec_PtrEntry( p->vPats, Abc_NtkPo(p->pAig, 1)->Id );
+ nDcs = nOnes = nZeros = 0;
+ for ( i = 0; i < p->nPats; i++ )
+ {
+ // skip don't-care patterns
+ if ( !Abc_InfoHasBit(pInfoCare, i) )
+ {
+ nDcs++;
+ continue;
+ }
+ // separate offset and onset patterns
+ if ( !Abc_InfoHasBit(pInfoNode, i) )
+ nZeros++;
+ else
+ nOnes++;
+ }
+ printf( "On = %3d (%7.2f %%) ", nOnes, 100.0*nOnes/p->nPats );
+ printf( "Off = %3d (%7.2f %%) ", nZeros, 100.0*nZeros/p->nPats );
+ printf( "Dc = %3d (%7.2f %%) ", nDcs, 100.0*nDcs/p->nPats );
+ printf( "P0 = %3d ", p->nPats0 );
+ printf( "P1 = %3d ", p->nPats1 );
+ if ( p->nPats0 < 4 || p->nPats1 < 4 )
+ printf( "*" );
+ printf( "\n" );
+}
+
+/**Function*************************************************************
+
+ Synopsis [Prints output patterns.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+void Res_SimPrintOutPatterns( Res_Sim_t * p, Abc_Ntk_t * pAig )
+{
+ Abc_Obj_t * pObj;
+ unsigned * pInfo2;
+ int i;
+ Abc_NtkForEachPo( pAig, pObj, i )
+ {
+ pInfo2 = Vec_PtrEntry( p->vOuts, i );
+ Extra_PrintBinary( stdout, pInfo2, p->nPatsOut );
+ printf( "\n" );
+ }
+}
+
+/**Function*************************************************************
+
+ Synopsis [Prepares simulation info for candidate filtering.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+int Res_SimPrepare( Res_Sim_t * p, Abc_Ntk_t * pAig, int nTruePis, int fVerbose )
+{
+ int Limit;
+ // prepare the manager
+ Res_SimAdjust( p, pAig );
+ // collect 0/1 simulation info
+ for ( Limit = 0; Limit < 10; Limit++ )
+ {
+ Res_SimSetRandom( p );
+ Res_SimPerformRound( p );
+ Res_SimProcessPats( p );
+ if ( !(p->nPats0 < p->nPats || p->nPats1 < p->nPats) )
+ break;
+ }
+// printf( "%d ", Limit );
+ // report the last set of patterns
+// Res_SimReportOne( p );
+// printf( "\n" );
+ // quit if there is not enough
+// if ( p->nPats0 < 4 || p->nPats1 < 4 )
+ if ( p->nPats0 < 4 || p->nPats1 < 4 )
+ {
+// Res_SimReportOne( p );
+ return 0;
+ }
+ // create bit-matrix info
+ if ( p->nPats0 < p->nPats )
+ Res_SimPadSimInfo( p->vPats0, p->nPats0, p->nWords );
+ if ( p->nPats1 < p->nPats )
+ Res_SimPadSimInfo( p->vPats1, p->nPats1, p->nWords );
+ // resimulate 0-patterns
+ Res_SimSetGiven( p, p->vPats0 );
+ Res_SimPerformRound( p );
+ Res_SimDeriveInfoReplicate( p );
+ // resimulate 1-patterns
+ Res_SimSetGiven( p, p->vPats1 );
+ Res_SimPerformRound( p );
+ Res_SimDeriveInfoComplement( p );
+ // print output patterns
+// Res_SimPrintOutPatterns( p, pAig );
+ return 1;
+}
+
+////////////////////////////////////////////////////////////////////////
+/// END OF FILE ///
+////////////////////////////////////////////////////////////////////////
+
+
diff --git a/src/opt/res/resWin.c b/src/opt/res/resWin.c
index 80a65ea8..a3648925 100644
--- a/src/opt/res/resWin.c
+++ b/src/opt/res/resWin.c
@@ -94,7 +94,7 @@ void Res_WinFree( Res_Win_t * p )
SeeAlso []
***********************************************************************/
-void Res_WinCollectLeavesAndNodes( Res_Win_t * p )
+int Res_WinCollectLeavesAndNodes( Res_Win_t * p )
{
Vec_Ptr_t * vFront;
Abc_Obj_t * pObj, * pTemp;
@@ -127,7 +127,8 @@ void Res_WinCollectLeavesAndNodes( Res_Win_t * p )
}
}
}
- assert( Vec_PtrSize(p->vLeaves) > 0 );
+ if ( Vec_PtrSize(p->vLeaves) == 0 )
+ return 0;
// collect the nodes in the reverse order
Vec_PtrClear( p->vNodes );
@@ -146,6 +147,7 @@ void Res_WinCollectLeavesAndNodes( Res_Win_t * p )
// set minimum traversal level
p->nLevTravMin = ABC_MAX( ((int)p->pNode->Level) - p->nWinTfiMax - p->nLevTfiMinus, p->nLevLeafMin );
assert( p->nLevTravMin >= 0 );
+ return 1;
}
@@ -371,6 +373,7 @@ void Res_WinAddMissing_rec( Res_Win_t * p, Abc_Obj_t * pObj, int nLevTravMin )
// if this is not an internal node - make it a new branch
if ( !Abc_NodeIsTravIdPrevious(pObj) )
{
+ assert( Vec_PtrFind(p->vLeaves, pObj) == -1 );
Abc_NodeSetTravIdCurrent( pObj );
Vec_PtrPush( p->vBranches, pObj );
return;
@@ -452,11 +455,15 @@ int Res_WinCompute( Abc_Obj_t * pNode, int nWinTfiMax, int nWinTfoMax, Res_Win_t
p->pNode = pNode;
p->nWinTfiMax = nWinTfiMax;
p->nWinTfoMax = nWinTfoMax;
+
+ Vec_PtrClear( p->vBranches );
+ Vec_PtrClear( p->vDivs );
Vec_PtrClear( p->vRoots );
Vec_PtrPush( p->vRoots, pNode );
// compute the leaves
- Res_WinCollectLeavesAndNodes( p );
+ if ( !Res_WinCollectLeavesAndNodes( p ) )
+ return 0;
// compute the candidate roots
if ( p->nWinTfoMax > 0 && Res_WinComputeRoots(p) )
generated by cgit v1.2.3 (git 2.25.1) at 2024-12-26 17:07:49 +0000