summaryrefslogtreecommitdiffstats
diff options
context:
space:
mode:
Diffstat
-rw-r--r--src/aig/gia/giaMuxes.c2
-rw-r--r--src/base/abci/abc.c11
-rw-r--r--src/opt/dau/dauGia.c8
-rw-r--r--src/opt/sbd/sbd.h1
-rw-r--r--src/opt/sbd/sbdCore.c180
-rw-r--r--src/opt/sbd/sbdWin.c5
6 files changed, 168 insertions, 39 deletions
diff --git a/src/aig/gia/giaMuxes.c b/src/aig/gia/giaMuxes.c
index c38cbf43..4ce109f6 100644
--- a/src/aig/gia/giaMuxes.c
+++ b/src/aig/gia/giaMuxes.c
@@ -100,7 +100,7 @@ Gia_Man_t * Gia_ManDupMuxes( Gia_Man_t * p, int Limit )
Gia_Obj_t * pObj, * pFan0, * pFan1, * pFanC, * pSiblNew, * pObjNew;
int i;
assert( p->pMuxes == NULL );
- assert( Limit >= 1 ); // allows to create AIG with XORs without MUXes
+ assert( Limit >= 0 ); // allows to create AIG with XORs without MUXes
ABC_FREE( p->pRefs );
Gia_ManCreateRefs( p );
// start the new manager
diff --git a/src/base/abci/abc.c b/src/base/abci/abc.c
index ba4d37b3..1fdffd77 100644
--- a/src/base/abci/abc.c
+++ b/src/base/abci/abc.c
@@ -27643,6 +27643,7 @@ static inline int Gia_ManCompareWithBest( Gia_Man_t * pBest, Gia_Man_t * p, int
*pnBestLuts = nCurLuts;
*pnBestEdges = nCurEdges;
*pnBestLevels = nCurLevels;
+ //printf( "\nUpdating best (%d %d %d).\n\n", nCurLuts, nCurEdges, nCurLevels );
return 1;
}
return 0;
@@ -31023,7 +31024,7 @@ usage:
Abc_Print( -2, "\t-C num : the max number of conflicts at a node [default = %d]\n", pPars->nBTLimit );
Abc_Print( -2, "\t-S num : the max number of SAT variables [default = %d]\n", pPars->nSatVarMax );
Abc_Print( -2, "\t-K num : the target LUT size for downstream mapping [default = %d]\n", nLutSize );
- Abc_Print( -2, "\t-R num : the delay relaxation ratio (num >= 0) [default = %d]\n", nRelaxRatio );
+ Abc_Print( -2, "\t-R num : the delay relaxation ratio (num >= 0) [default = %d]\n", nRelaxRatio );
Abc_Print( -2, "\t-f : toggle using lighter logic synthesis [default = %s]\n", pPars->fLightSynth? "yes": "no" );
Abc_Print( -2, "\t-v : toggle verbose printout [default = %s]\n", pPars->fVerbose? "yes": "no" );
Abc_Print( -2, "\t-h : print the command usage\n");
@@ -40852,7 +40853,7 @@ int Abc_CommandAbc9Mfsd( Abc_Frame_t * pAbc, int argc, char ** argv )
Sbd_Par_t Pars, * pPars = &Pars;
Sbd_ParSetDefault( pPars );
Extra_UtilGetoptReset();
- while ( ( c = Extra_UtilGetopt( argc, argv, "KWFMCavwh" ) ) != EOF )
+ while ( ( c = Extra_UtilGetopt( argc, argv, "KWFMCacvwh" ) ) != EOF )
{
switch ( c )
{
@@ -40914,6 +40915,9 @@ int Abc_CommandAbc9Mfsd( Abc_Frame_t * pAbc, int argc, char ** argv )
case 'a':
pPars->fArea ^= 1;
break;
+ case 'c':
+ pPars->fCover ^= 1;
+ break;
case 'v':
pPars->fVerbose ^= 1;
break;
@@ -40946,7 +40950,7 @@ int Abc_CommandAbc9Mfsd( Abc_Frame_t * pAbc, int argc, char ** argv )
return 0;
usage:
- Abc_Print( -2, "usage: &mfsd [-KWFMC <num>] [-avwh]\n" );
+ Abc_Print( -2, "usage: &mfsd [-KWFMC <num>] [-acvwh]\n" );
Abc_Print( -2, "\t performs SAT-based delay-oriented AIG optimization\n" );
Abc_Print( -2, "\t-K <num> : the LUT size for delay minimization (2 <= num <= 6) [default = %d]\n", pPars->nLutSize );
Abc_Print( -2, "\t-W <num> : the number of levels in the TFO cone (0 <= num) [default = %d]\n", pPars->nTfoLevels );
@@ -40954,6 +40958,7 @@ usage:
Abc_Print( -2, "\t-M <num> : the max node count of windows to consider (0 = no limit) [default = %d]\n", pPars->nWinSizeMax );
Abc_Print( -2, "\t-C <num> : the max number of conflicts in one SAT run (0 = no limit) [default = %d]\n", pPars->nBTLimit );
Abc_Print( -2, "\t-a : toggle minimizing area or area+edges [default = %s]\n", pPars->fArea? "area": "area+edges" );
+ Abc_Print( -2, "\t-c : toggle using complete slow covering procedure [default = %s]\n", pPars->fCover? "yes": "no" );
Abc_Print( -2, "\t-v : toggle printing optimization summary [default = %s]\n", pPars->fVerbose? "yes": "no" );
Abc_Print( -2, "\t-w : toggle printing detailed stats for each node [default = %s]\n", pPars->fVeryVerbose? "yes": "no" );
Abc_Print( -2, "\t-h : print the command usage\n");
diff --git a/src/opt/dau/dauGia.c b/src/opt/dau/dauGia.c
index c7f5c11f..6489cd86 100644
--- a/src/opt/dau/dauGia.c
+++ b/src/opt/dau/dauGia.c
@@ -243,7 +243,11 @@ int Dau_DsdBalance( Gia_Man_t * pGia, int * pFans, int nFans, int fAnd )
if ( fAnd )
iFan = Gia_ManAppendAnd( pGia, iFan0, iFan1 );
else if ( pGia->pMuxes )
- iFan = Gia_ManAppendXorReal( pGia, iFan0, iFan1 );
+ {
+ int fCompl = Abc_LitIsCompl(iFan0) ^ Abc_LitIsCompl(iFan1);
+ iFan = Gia_ManAppendXorReal( pGia, Abc_LitRegular(iFan0), Abc_LitRegular(iFan1) );
+ iFan = Abc_LitNotCond( iFan, fCompl );
+ }
else
iFan = Gia_ManAppendXor( pGia, iFan0, iFan1 );
}
@@ -369,7 +373,7 @@ int Dau_DsdToGia_rec( Gia_Man_t * pGia, char * pStr, char ** p, int * pMatches,
pObj = Gia_ManObj(pGia, Abc_Lit2Var(Res));
if ( Gia_ObjIsAnd(pObj) )
{
- if ( pGia->pMuxes )
+ if ( pGia->pMuxes && pGia->pHTable != NULL )
Gia_ObjSetMuxLevel( pGia, pObj );
else
{
diff --git a/src/opt/sbd/sbd.h b/src/opt/sbd/sbd.h
index e1e39a3b..89d29958 100644
--- a/src/opt/sbd/sbd.h
+++ b/src/opt/sbd/sbd.h
@@ -45,6 +45,7 @@ struct Sbd_Par_t_
int nBTLimit; // maximum number of SAT conflicts
int nWords; // simulation word count
int fArea; // area-oriented optimization
+ int fCover; // use complete cover procedure
int fVerbose; // verbose flag
int fVeryVerbose; // verbose flag
};
diff --git a/src/opt/sbd/sbdCore.c b/src/opt/sbd/sbdCore.c
index f5c944c9..b6ec70f9 100644
--- a/src/opt/sbd/sbdCore.c
+++ b/src/opt/sbd/sbdCore.c
@@ -20,6 +20,7 @@
#include "sbdInt.h"
#include "opt/dau/dau.h"
+#include "misc/tim/tim.h"
ABC_NAMESPACE_IMPL_START
@@ -97,6 +98,7 @@ void Sbd_ParSetDefault( Sbd_Par_t * pPars )
pPars->nBTLimit = 0; // maximum number of SAT conflicts
pPars->nWords = 1; // simulation word count
pPars->fArea = 0; // area-oriented optimization
+ pPars->fCover = 0; // use complete cover procedure
pPars->fVerbose = 0; // verbose flag
pPars->fVeryVerbose = 0; // verbose flag
}
@@ -467,6 +469,14 @@ int Sbd_ManCheckConst( Sbd_Man_t * p, int Pivot )
extern sat_solver * Sbd_ManSatSolver( sat_solver * pSat, Gia_Man_t * p, Vec_Int_t * vMirrors, int Pivot, Vec_Int_t * vWinObjs, Vec_Int_t * vObj2Var, Vec_Int_t * vTfo, Vec_Int_t * vRoots );
p->pSat = Sbd_ManSatSolver( p->pSat, p->pGia, p->vMirrors, Pivot, p->vWinObjs, p->vObj2Var, p->vTfo, p->vRoots );
p->timeCnf += Abc_Clock() - clk;
+ if ( p->pSat == NULL )
+ {
+ if ( p->pPars->fVerbose )
+ printf( "Found stuck-at-%d node %d.\n", 0, Pivot );
+ Vec_IntWriteEntry( p->vLutLevs, Pivot, 0 );
+ p->nConsts++;
+ return 0;
+ }
//return -1;
//Sbd_ManPrintObj( p, Pivot );
@@ -822,7 +832,7 @@ static inline int Sbd_ManAddCube2( word Cover[2][64], int nRows, word Cube[2] )
return nRows;
}
-static inline int Sbd_ManFindCands( Sbd_Man_t * p, word Cover[64], int nDivs )
+static inline int Sbd_ManFindCandsSimple( Sbd_Man_t * p, word Cover[64], int nDivs )
{
int c0, c1, c2, c3;
word Target = Cover[nDivs];
@@ -871,6 +881,72 @@ static inline int Sbd_ManFindCands( Sbd_Man_t * p, word Cover[64], int nDivs )
return 0;
}
+static inline int Sbd_ManFindCands( Sbd_Man_t * p, word Cover[64], int nDivs )
+{
+ int Ones[64], Order[64];
+ int Limits[4] = { nDivs/4+1, nDivs/3+2, nDivs/2+3, nDivs };
+ int c0, c1, c2, c3;
+ word Target = Cover[nDivs];
+
+ if ( nDivs < 8 || p->pPars->fCover )
+ return Sbd_ManFindCandsSimple( p, Cover, nDivs );
+
+ Vec_IntClear( p->vDivVars );
+ for ( c0 = 0; c0 < nDivs; c0++ )
+ if ( Cover[c0] == Target )
+ {
+ Vec_IntPush( p->vDivVars, c0 );
+ return 1;
+ }
+
+ for ( c0 = 0; c0 < nDivs; c0++ )
+ for ( c1 = c0+1; c1 < nDivs; c1++ )
+ if ( (Cover[c0] | Cover[c1]) == Target )
+ {
+ Vec_IntPush( p->vDivVars, c0 );
+ Vec_IntPush( p->vDivVars, c1 );
+ return 1;
+ }
+
+ // count ones
+ for ( c0 = 0; c0 < nDivs; c0++ )
+ Ones[c0] = Abc_TtCountOnes( Cover[c0] );
+
+ // sort by the number of ones
+ for ( c0 = 0; c0 < nDivs; c0++ )
+ Order[c0] = c0;
+ Vec_IntSelectSortCost2Reverse( Order, nDivs, Ones );
+
+ // sort with limits
+ for ( c0 = 0; c0 < Limits[0]; c0++ )
+ for ( c1 = c0+1; c1 < Limits[1]; c1++ )
+ for ( c2 = c1+1; c2 < Limits[2]; c2++ )
+ if ( (Cover[Order[c0]] | Cover[Order[c1]] | Cover[Order[c2]]) == Target )
+ {
+ Vec_IntPush( p->vDivVars, Order[c0] );
+ Vec_IntPush( p->vDivVars, Order[c1] );
+ Vec_IntPush( p->vDivVars, Order[c2] );
+ return 1;
+ }
+
+ for ( c0 = 0; c0 < Limits[0]; c0++ )
+ for ( c1 = c0+1; c1 < Limits[1]; c1++ )
+ for ( c2 = c1+1; c2 < Limits[2]; c2++ )
+ for ( c3 = c2+1; c3 < Limits[3]; c3++ )
+ {
+ if ( (Cover[Order[c0]] | Cover[Order[c1]] | Cover[Order[c2]] | Cover[Order[c3]]) == Target )
+ {
+ Vec_IntPush( p->vDivVars, Order[c0] );
+ Vec_IntPush( p->vDivVars, Order[c1] );
+ Vec_IntPush( p->vDivVars, Order[c2] );
+ Vec_IntPush( p->vDivVars, Order[c3] );
+ return 1;
+ }
+ }
+ return 0;
+}
+
+
int Sbd_ManExplore( Sbd_Man_t * p, int Pivot, word * pTruth )
{
int fVerbose = 0;
@@ -1158,7 +1234,7 @@ int Sbd_ManMergeCuts( Sbd_Man_t * p, int Node )
assert( pCutRes[0] <= p->pPars->nLutSize );
memcpy( Sbd_ObjCut(p, Node), pCutRes, sizeof(int) * (pCutRes[0] + 1) );
//printf( "Setting node %d with delay %d.\n", Node, LevCur );
- return LevCur == Abc_MaxInt(Level0, Level1);
+ return LevCur == 1; // LevCur == Abc_MaxInt(Level0, Level1);
}
int Sbd_ManDelay( Sbd_Man_t * p )
{
@@ -1223,11 +1299,11 @@ void Sbd_ManFindCut( Sbd_Man_t * p, int Node, Vec_Int_t * vCutLits )
int Sbd_ManImplement( Sbd_Man_t * p, int Pivot, word Truth )
{
+ Gia_Obj_t * pObj;
int i, k, w, iLit, Entry, Node;
int iObjLast = Gia_ManObjNum(p->pGia);
int iCurLev = Vec_IntEntry(p->vLutLevs, Pivot);
int iNewLev;
- Gia_Obj_t * pObj;
// collect leaf literals
Vec_IntClear( p->vLits );
Vec_IntForEachEntry( p->vDivVars, Node, i )
@@ -1239,12 +1315,13 @@ int Sbd_ManImplement( Sbd_Man_t * p, int Pivot, word Truth )
Vec_IntPush( p->vLits, Abc_Var2Lit(Node, 0) );
}
// pretend to have MUXes
- assert( p->pGia->pMuxes == NULL );
- if ( p->pGia->nXors )
+// assert( p->pGia->pMuxes == NULL );
+ if ( p->pGia->nXors && p->pGia->pMuxes == NULL )
p->pGia->pMuxes = (unsigned *)p;
// derive new function of the node
iLit = Dsm_ManTruthToGia( p->pGia, &Truth, p->vLits, p->vCover );
- p->pGia->pMuxes = NULL;
+ if ( p->pGia->pMuxes == (unsigned *)p )
+ p->pGia->pMuxes = NULL;
// remember this function
assert( Vec_IntEntry(p->vMirrors, Pivot) == -1 );
Vec_IntWriteEntry( p->vMirrors, Pivot, iLit );
@@ -1323,6 +1400,8 @@ Gia_Man_t * Sbd_ManDerive( Gia_Man_t * p, Vec_Int_t * vMirrors )
pNew = Gia_ManStart( Gia_ManObjNum(p) );
pNew->pName = Abc_UtilStrsav( p->pName );
pNew->pSpec = Abc_UtilStrsav( p->pSpec );
+ if ( p->pMuxes )
+ pNew->pMuxes = ABC_CALLOC( unsigned, Gia_ManObjNum(p) );
Gia_ManConst0(p)->Value = 0;
Gia_ManHashAlloc( pNew );
Gia_ManForEachCi( p, pObj, i )
@@ -1333,6 +1412,7 @@ Gia_Man_t * Sbd_ManDerive( Gia_Man_t * p, Vec_Int_t * vMirrors )
pObj->Value = Gia_ManAppendCo( pNew, Gia_ObjFanin0Copy(pObj) );
Gia_ManHashStop( pNew );
Gia_ManSetRegNum( pNew, Gia_ManRegNum(p) );
+ Gia_ManTransferTiming( pNew, p );
return pNew;
}
@@ -1347,36 +1427,69 @@ Gia_Man_t * Sbd_ManDerive( Gia_Man_t * p, Vec_Int_t * vMirrors )
SeeAlso []
***********************************************************************/
+void Sbd_NtkPerformOne( Sbd_Man_t * p, int Pivot )
+{
+ int RetValue; word Truth = 0;
+ if ( Sbd_ManMergeCuts( p, Pivot ) )
+ return;
+ //if ( Pivot != 344 )
+ // continue;
+ if ( p->pPars->fVerbose )
+ printf( "\nLooking at node %d\n", Pivot );
+ if ( Sbd_ManWindow( p, Pivot ) )
+ return;
+ RetValue = Sbd_ManCheckConst( p, Pivot );
+ if ( RetValue >= 0 )
+ Vec_IntWriteEntry( p->vMirrors, Pivot, RetValue );
+ else if ( Sbd_ManExplore( p, Pivot, &Truth ) )
+ Sbd_ManImplement( p, Pivot, Truth );
+}
Gia_Man_t * Sbd_NtkPerform( Gia_Man_t * pGia, Sbd_Par_t * pPars )
{
Gia_Man_t * pNew;
+ Gia_Obj_t * pObj;
Sbd_Man_t * p = Sbd_ManStart( pGia, pPars );
int nNodesOld = Gia_ManObjNum(pGia);//, Count = 0;
- int RetValue, Pivot; word Truth = 0;
+ int k, Pivot;
assert( pPars->nLutSize <= 6 );
//Sbd_ManMergeTest( p );
//return NULL;
- Gia_ManForEachAndId( pGia, Pivot )
+ if ( pGia->pManTime != NULL && Tim_ManBoxNum((Tim_Man_t*)pGia->pManTime) )
{
- if ( Pivot >= nNodesOld )
- break;
- if ( Sbd_ManMergeCuts( p, Pivot ) )
- continue;
- //if ( Pivot != 344 )
- // continue;
- if ( p->pPars->fVerbose )
- printf( "\nLooking at node %d\n", Pivot );
- if ( Sbd_ManWindow( p, Pivot ) )
- continue;
- RetValue = Sbd_ManCheckConst( p, Pivot );
- if ( RetValue >= 0 )
- Vec_IntWriteEntry( p->vMirrors, Pivot, RetValue );
- else if ( Sbd_ManExplore( p, Pivot, &Truth ) )
+ Vec_Int_t * vNodes = Gia_ManOrderWithBoxes( pGia );
+ Tim_Man_t * pTimOld = (Tim_Man_t *)pGia->pManTime;
+ pGia->pManTime = Tim_ManDup( pTimOld, 1 );
+ Tim_ManIncrementTravId( (Tim_Man_t *)pGia->pManTime );
+ Gia_ManForEachObjVec( vNodes, pGia, pObj, k )
{
- Sbd_ManImplement( p, Pivot, Truth );
- //if ( Count++ == 1 )
- // break;
+ Pivot = Gia_ObjId( pGia, pObj );
+ if ( Pivot >= nNodesOld )
+ continue;
+ if ( Gia_ObjIsAnd(pObj) )
+ Sbd_NtkPerformOne( p, Pivot );
+ else if ( Gia_ObjIsCi(pObj) )
+ {
+ int arrTime = Tim_ManGetCiArrival( (Tim_Man_t*)pGia->pManTime, Gia_ObjCioId(pObj) );
+ Vec_IntWriteEntry( p->vLutLevs, Pivot, arrTime );
+ }
+ else if ( Gia_ObjIsCo(pObj) )
+ {
+ int arrTime = Vec_IntEntry( p->vLutLevs, Gia_ObjFaninId0(pObj, Pivot) );
+ Tim_ManSetCoArrival( (Tim_Man_t*)pGia->pManTime, Gia_ObjCioId(pObj), arrTime );
+ }
+ else if ( !Gia_ObjIsConst0(pObj) )
+ assert( 0 );
}
+ //Tim_ManPrint( pGia->pManTime );
+ Tim_ManStop( (Tim_Man_t *)pGia->pManTime );
+ pGia->pManTime = pTimOld;
+ Vec_IntFree( vNodes );
+ }
+ else
+ {
+ Gia_ManForEachAndId( pGia, Pivot )
+ if ( Pivot < nNodesOld )
+ Sbd_NtkPerformOne( p, Pivot );
}
printf( "Found %d constants and %d replacements with delay %d. ", p->nConsts, p->nChanges, Sbd_ManDelay(p) );
p->timeTotal = Abc_Clock() - p->timeTotal;
@@ -1384,13 +1497,16 @@ Gia_Man_t * Sbd_NtkPerform( Gia_Man_t * pGia, Sbd_Par_t * pPars )
pNew = Sbd_ManDerive( pGia, p->vMirrors );
// print runtime statistics
p->timeOther = p->timeTotal - p->timeWin - p->timeCnf - p->timeSat - p->timeCov - p->timeEnu;
- ABC_PRTP( "Win", p->timeWin , p->timeTotal );
- ABC_PRTP( "Cnf", p->timeCnf , p->timeTotal );
- ABC_PRTP( "Sat", p->timeSat , p->timeTotal );
- ABC_PRTP( "Cov", p->timeCov , p->timeTotal );
- ABC_PRTP( "Enu", p->timeEnu , p->timeTotal );
- ABC_PRTP( "Oth", p->timeOther, p->timeTotal );
- ABC_PRTP( "ALL", p->timeTotal, p->timeTotal );
+ if ( 0 )
+ {
+ ABC_PRTP( "Win", p->timeWin , p->timeTotal );
+ ABC_PRTP( "Cnf", p->timeCnf , p->timeTotal );
+ ABC_PRTP( "Sat", p->timeSat , p->timeTotal );
+ ABC_PRTP( "Cov", p->timeCov , p->timeTotal );
+ ABC_PRTP( "Enu", p->timeEnu , p->timeTotal );
+ ABC_PRTP( "Oth", p->timeOther, p->timeTotal );
+ ABC_PRTP( "ALL", p->timeTotal, p->timeTotal );
+ }
Sbd_ManStop( p );
return pNew;
}
diff --git a/src/opt/sbd/sbdWin.c b/src/opt/sbd/sbdWin.c
index 7100462b..d722f456 100644
--- a/src/opt/sbd/sbdWin.c
+++ b/src/opt/sbd/sbdWin.c
@@ -123,7 +123,10 @@ sat_solver * Sbd_ManSatSolver( sat_solver * pSat, Gia_Man_t * p, Vec_Int_t * vMi
RetValue = sat_solver_addclause( pSat, Vec_IntArray(vFaninVars), Vec_IntLimit(vFaninVars) );
Vec_IntFree( vFaninVars );
if ( RetValue == 0 )
- return 0;
+ {
+ sat_solver_delete( pSat );
+ return NULL;
+ }
assert( sat_solver_nvars(pSat) == nVars + 32 );
}
// finalize
generated by cgit v1.2.3 (git 2.25.1) at 2024-11-05 02:09:43 +0000