summaryrefslogtreecommitdiffstats
path: root/src
diff options
context:
space:
mode:
Diffstat (limited to 'src')
-rw-r--r--src/aig/gia/giaDup.c25
-rw-r--r--src/aig/gia/giaNf.c59
-rw-r--r--src/base/abci/abc.c1
-rw-r--r--src/base/wlc/wlc.c138
-rw-r--r--src/map/mio/mio.c22
-rw-r--r--src/map/mio/mio.h5
-rw-r--r--src/map/mio/mioInt.h8
-rw-r--r--src/map/mio/mioUtils.c177
-rw-r--r--src/misc/vec/vec.h2
-rw-r--r--src/opt/fxch/module.make2
-rw-r--r--src/opt/sfm/module.make3
-rw-r--r--src/opt/sfm/sfmArea.c380
-rw-r--r--src/opt/sfm/sfmDec.c5
-rw-r--r--src/sat/bmc/bmcGen.c195
-rw-r--r--src/sat/bmc/module.make1
15 files changed, 962 insertions, 61 deletions
diff --git a/src/aig/gia/giaDup.c b/src/aig/gia/giaDup.c
index dbfe38f3..946f6d4d 100644
--- a/src/aig/gia/giaDup.c
+++ b/src/aig/gia/giaDup.c
@@ -3747,21 +3747,17 @@ void Gia_ManCollectTopXors_rec( Gia_Man_t * p, Gia_Obj_t * pObj, Vec_Int_t * vXo
else
Gia_ManCollectTopXors_rec( p, Gia_ObjFanin1(pObj), vXors );
}
-Vec_Int_t * Gia_ManCollectTopXors( Gia_Man_t * p, Vec_Int_t * vPolar )
+Vec_Int_t * Gia_ManCollectTopXors( Gia_Man_t * p )
{
int i, iObj, iObj2, fFlip, * pPerm, Count1 = 0;
Vec_Int_t * vXors, * vSizes, * vPart[2], * vOrder;
Gia_Obj_t * pFan[2], * pObj = Gia_ManCo(p, 0);
assert( Gia_ManCoNum(p) == 1 );
- Vec_IntClear( vPolar );
- if ( !Gia_ObjFaninC0(pObj) )
- return NULL;
vXors = Vec_IntAlloc( 100 );
- pObj = Gia_ObjFanin0(pObj);
- if ( Gia_ObjIsAnd(pObj) )
- Gia_ManCollectTopXors_rec( p, pObj, vXors );
+ if ( Gia_ObjFaninC0(pObj) )
+ Gia_ManCollectTopXors_rec( p, Gia_ObjFanin0(pObj), vXors );
else
- Vec_IntPush( vXors, Gia_ObjId(p, pObj) );
+ Vec_IntPush( vXors, Gia_ObjId(p, Gia_ObjFanin0(pObj)) );
// order by support size
vSizes = Vec_IntAlloc( 100 );
Vec_IntForEachEntry( vXors, iObj, i )
@@ -3791,7 +3787,6 @@ Vec_Int_t * Gia_ManCollectTopXors( Gia_Man_t * p, Vec_Int_t * vPolar )
pFan[0] = Gia_Regular(pFan[0]);
pFan[1] = Gia_Regular(pFan[1]);
}
- Vec_IntPushTwo( vPolar, 0, fCompl );
fFlip = Gia_ManDecideWhereToAdd( p, vPart, pFan );
Vec_IntPush( vPart[0], Gia_ObjId(p, pFan[fFlip]) );
Vec_IntPush( vPart[1], Gia_ObjId(p, pFan[!fFlip]) );
@@ -3808,22 +3803,20 @@ Vec_Int_t * Gia_ManCollectTopXors( Gia_Man_t * p, Vec_Int_t * vPolar )
Vec_IntFree( vPart[0] );
Vec_IntFree( vPart[1] );
Vec_IntReverseOrder( vOrder ); // from LSB to MSB
- Vec_IntReverseOrder( vPolar );
//Vec_IntPrint( vOrder );
return vOrder;
}
Gia_Man_t * Gia_ManDemiterToDual( Gia_Man_t * p )
{
Gia_Man_t * pNew; Gia_Obj_t * pObj; int i;
- Vec_Int_t * vNodes, * vPolar = Vec_IntAlloc( 100 );
- Vec_Int_t * vOrder = Gia_ManCollectTopXors( p, vPolar );
+ Vec_Int_t * vNodes;
+ Vec_Int_t * vOrder = Gia_ManCollectTopXors( p );
if ( vOrder == NULL )
{
- Vec_IntFree( vPolar );
printf( "Cannot demiter because the top-most gate is an AND-gate.\n" );
return NULL;
}
- assert( Vec_IntSize(vOrder) == Vec_IntSize(vPolar) );
+ assert( Vec_IntSize(vOrder) % 2 == 0 );
vNodes = Vec_IntAlloc( Gia_ManObjNum(p) );
Gia_ManIncrementTravId( p );
Gia_ManCollectAnds( p, Vec_IntArray(vOrder), Vec_IntSize(vOrder), vNodes, NULL );
@@ -3835,9 +3828,9 @@ Gia_Man_t * Gia_ManDemiterToDual( Gia_Man_t * p )
pObj->Value = Gia_ManAppendCi( pNew );
Gia_ManForEachObjVec( vNodes, p, pObj, i )
pObj->Value = Gia_ManAppendAnd( pNew, Gia_ObjFanin0Copy(pObj), Gia_ObjFanin1Copy(pObj) );
+ Gia_ManSetPhase( p );
Gia_ManForEachObjVec( vOrder, p, pObj, i )
- Gia_ManAppendCo( pNew, Abc_LitNotCond(pObj->Value, Vec_IntEntry(vPolar, i)) );
- Vec_IntFree( vPolar );
+ Gia_ManAppendCo( pNew, Abc_LitNotCond(pObj->Value, pObj->fPhase) );
Vec_IntFree( vNodes );
Vec_IntFree( vOrder );
return pNew;
diff --git a/src/aig/gia/giaNf.c b/src/aig/gia/giaNf.c
index 510e7ddb..6761b617 100644
--- a/src/aig/gia/giaNf.c
+++ b/src/aig/gia/giaNf.c
@@ -178,18 +178,17 @@ int Nf_StoCellIsDominated( Mio_Cell2_t * pCell, int * pFans, int * pProf )
return 0;
return 1; // pCell is dominated
}
-void Nf_StoCreateGateAdd( Nf_Man_t * pMan, word uTruth, int * pFans, int nFans, int CellId, Vec_Wec_t * vProfs, Vec_Int_t * vStore )
+void Nf_StoCreateGateAdd( Vec_Mem_t * vTtMem, Vec_Wec_t * vTt2Match, Mio_Cell2_t * pCell, word uTruth, int * pFans, int nFans, Vec_Wec_t * vProfs, Vec_Int_t * vStore, int fPinFilter, int fPinPerm, int fPinQuick )
{
Vec_Int_t * vArray, * vArrayProfs = NULL;
- Mio_Cell2_t * pCell = Nf_ManCell( pMan, CellId );
int i, k, GateId, Entry, fCompl = (int)(uTruth & 1);
word uFunc = fCompl ? ~uTruth : uTruth;
- int iFunc = Vec_MemHashInsert( pMan->vTtMem, &uFunc );
+ int iFunc = Vec_MemHashInsert( vTtMem, &uFunc );
Nf_Cfg_t Mat = Nf_Int2Cfg(0);
// get match array
- if ( iFunc == Vec_WecSize(pMan->vTt2Match) )
- Vec_WecPushLevel( pMan->vTt2Match );
- vArray = Vec_WecEntry( pMan->vTt2Match, iFunc );
+ if ( iFunc == Vec_WecSize(vTt2Match) )
+ Vec_WecPushLevel( vTt2Match );
+ vArray = Vec_WecEntry( vTt2Match, iFunc );
// create match
Mat.fCompl = fCompl;
assert( nFans == (int)pCell->nFanins );
@@ -199,10 +198,10 @@ void Nf_StoCreateGateAdd( Nf_Man_t * pMan, word uTruth, int * pFans, int nFans,
Mat.Phase |= (unsigned)(Abc_LitIsCompl(pFans[i]) << Abc_Lit2Var(pFans[i]));
}
// check other profiles
- if ( pMan->pPars->fPinFilter )
+ if ( fPinFilter )
{
// get profile array
- assert( Vec_WecSize(pMan->vTt2Match) == Vec_WecSize(vProfs) );
+ assert( Vec_WecSize(vTt2Match) == Vec_WecSize(vProfs) );
if ( iFunc == Vec_WecSize(vProfs) )
Vec_WecPushLevel( vProfs );
vArrayProfs = Vec_WecEntry( vProfs, iFunc );
@@ -218,26 +217,26 @@ void Nf_StoCreateGateAdd( Nf_Man_t * pMan, word uTruth, int * pFans, int nFans,
}
}
// check pin permutation
- if ( !pMan->pPars->fPinPerm ) // do not use pin-permutation (improves delay when pin-delays differ)
+ if ( !fPinPerm ) // do not use pin-permutation (improves delay when pin-delays differ)
{
- if ( pMan->pPars->fPinQuick ) // reduce the number of matches agressively
+ if ( fPinQuick ) // reduce the number of matches agressively
{
Vec_IntForEachEntryDouble( vArray, GateId, Entry, i )
- if ( GateId == CellId && Abc_TtBitCount8[Nf_Int2Cfg(Entry).Phase] == Abc_TtBitCount8[Mat.Phase] )
+ if ( GateId == (int)pCell->Id && Abc_TtBitCount8[Nf_Int2Cfg(Entry).Phase] == Abc_TtBitCount8[Mat.Phase] )
return;
}
else // reduce the number of matches less agressively
{
Vec_IntForEachEntryDouble( vArray, GateId, Entry, i )
- if ( GateId == CellId && Nf_Int2Cfg(Entry).Phase == Mat.Phase )
+ if ( GateId == (int)pCell->Id && Nf_Int2Cfg(Entry).Phase == Mat.Phase )
return;
}
}
// save data and profile
- Vec_IntPush( vArray, CellId );
+ Vec_IntPush( vArray, pCell->Id );
Vec_IntPush( vArray, Nf_Cfg2Int(Mat) );
// add delay profile
- if ( pMan->pPars->fPinFilter )
+ if ( fPinFilter )
{
Vec_IntPush( vArrayProfs, Vec_IntSize(vStore) );
Vec_IntPush( vStore, Abc_Float2Int(pCell->AreaF) );
@@ -245,7 +244,7 @@ void Nf_StoCreateGateAdd( Nf_Man_t * pMan, word uTruth, int * pFans, int nFans,
Vec_IntPush( vStore, pCell->iDelays[Abc_Lit2Var(pFans[k])] );
}
}
-void Nf_StoCreateGateMaches( Nf_Man_t * pMan, Mio_Cell2_t * pCell, int ** pComp, int ** pPerm, int * pnPerms, Vec_Wec_t * vProfs, Vec_Int_t * vStore )
+void Nf_StoCreateGateMaches( Vec_Mem_t * vTtMem, Vec_Wec_t * vTt2Match, Mio_Cell2_t * pCell, int ** pComp, int ** pPerm, int * pnPerms, Vec_Wec_t * vProfs, Vec_Int_t * vStore, int fPinFilter, int fPinPerm, int fPinQuick )
{
int Perm[NF_LEAF_MAX], * Perm1, * Perm2;
int nPerms = pnPerms[pCell->nFanins];
@@ -261,7 +260,7 @@ void Nf_StoCreateGateMaches( Nf_Man_t * pMan, Mio_Cell2_t * pCell, int ** pComp,
tTemp2 = tCur;
for ( c = 0; c < nMints; c++ )
{
- Nf_StoCreateGateAdd( pMan, tCur, Perm, pCell->nFanins, pCell->Id, vProfs, vStore );
+ Nf_StoCreateGateAdd( vTtMem, vTt2Match, pCell, tCur, Perm, pCell->nFanins, vProfs, vStore, fPinFilter, fPinPerm, fPinQuick );
// update
tCur = Abc_Tt6Flip( tCur, pComp[pCell->nFanins][c] );
Perm1 = Perm + pComp[pCell->nFanins][c];
@@ -278,12 +277,14 @@ void Nf_StoCreateGateMaches( Nf_Man_t * pMan, Mio_Cell2_t * pCell, int ** pComp,
}
assert( tTemp1 == tCur );
}
-void Nf_StoDeriveMatches( Nf_Man_t * p, int fVerbose )
+Mio_Cell2_t * Nf_StoDeriveMatches( Vec_Mem_t * vTtMem, Vec_Wec_t * vTt2Match, int * pnCells, int fPinFilter, int fPinPerm, int fPinQuick )
{
-// abctime clk = Abc_Clock();
+ int fVerbose = 0;
+ //abctime clk = Abc_Clock();
Vec_Wec_t * vProfs = Vec_WecAlloc( 1000 );
Vec_Int_t * vStore = Vec_IntAlloc( 10000 );
int * pComp[7], * pPerm[7], nPerms[7], i;
+ Mio_Cell2_t * pCells;
Vec_WecPushLevel( vProfs );
Vec_WecPushLevel( vProfs );
for ( i = 1; i <= 6; i++ )
@@ -292,18 +293,18 @@ void Nf_StoDeriveMatches( Nf_Man_t * p, int fVerbose )
pPerm[i] = Extra_PermSchedule( i );
for ( i = 1; i <= 6; i++ )
nPerms[i] = Extra_Factorial( i );
- p->pCells = Mio_CollectRootsNewDefault2( 6, &p->nCells, fVerbose );
- for ( i = 2; i < p->nCells; i++ )
- Nf_StoCreateGateMaches( p, p->pCells + i, pComp, pPerm, nPerms, vProfs, vStore );
+ pCells = Mio_CollectRootsNewDefault2( 6, pnCells, fVerbose );
+ for ( i = 2; i < *pnCells; i++ )
+ Nf_StoCreateGateMaches( vTtMem, vTt2Match, pCells+i, pComp, pPerm, nPerms, vProfs, vStore, fPinFilter, fPinPerm, fPinQuick );
for ( i = 1; i <= 6; i++ )
ABC_FREE( pComp[i] );
for ( i = 1; i <= 6; i++ )
ABC_FREE( pPerm[i] );
Vec_WecFree( vProfs );
Vec_IntFree( vStore );
-// Abc_PrintTime( 1, "Time", Abc_Clock() - clk );
+ //Abc_PrintTime( 1, "Time", Abc_Clock() - clk );
+ return pCells;
}
-//void Nf_StoPrintOne( Nf_Man_t * p, int Count, int t, int i, int GateId, Pf_Mat_t Mat )
void Nf_StoPrintOne( Nf_Man_t * p, int Count, int t, int i, int GateId, Nf_Cfg_t Mat )
{
Mio_Cell2_t * pC = p->pCells + GateId;
@@ -398,12 +399,7 @@ Nf_Man_t * Nf_StoCreate( Gia_Man_t * pGia, Jf_Par_t * pPars )
}
Vec_IntFree(vFlowRefs);
// matching
- p->vTtMem = Vec_MemAllocForTT( 6, 0 );
- p->vTt2Match = Vec_WecAlloc( 1000 );
- Vec_WecPushLevel( p->vTt2Match );
- Vec_WecPushLevel( p->vTt2Match );
- assert( Vec_WecSize(p->vTt2Match) == Vec_MemEntryNum(p->vTtMem) );
- Nf_StoDeriveMatches( p, 0 );//pPars->fVerbose );
+ Mio_LibraryMatchesFetch( (Mio_Library_t *)Abc_FrameReadLibGen(), &p->vTtMem, &p->vTt2Match, &p->pCells, &p->nCells, p->pPars->fPinFilter, p->pPars->fPinPerm, p->pPars->fPinQuick );
p->InvDelayI = p->pCells[3].iDelays[0];
p->InvAreaW = p->pCells[3].AreaW;
p->InvAreaF = p->pCells[3].AreaF;
@@ -424,11 +420,6 @@ void Nf_StoDelete( Nf_Man_t * p )
ABC_FREE( p->vCutDelays.pArray );
ABC_FREE( p->vBackup.pArray );
ABC_FREE( p->pNfObjs );
- // matching
- Vec_WecFree( p->vTt2Match );
- Vec_MemHashFree( p->vTtMem );
- Vec_MemFree( p->vTtMem );
- ABC_FREE( p->pCells );
ABC_FREE( p );
}
diff --git a/src/base/abci/abc.c b/src/base/abci/abc.c
index f67bbb09..da3a2d96 100644
--- a/src/base/abci/abc.c
+++ b/src/base/abci/abc.c
@@ -41422,6 +41422,7 @@ int Abc_CommandAbc9Test( Abc_Frame_t * pAbc, int argc, char ** argv )
// Gia_ManCheckFalseTest( pAbc->pGia, nFrames );
// Gia_ParTest( pAbc->pGia, nWords, nProcs );
// Gia_PolynExplore( pAbc->pGia );
+// Gia_ManTestSatEnum( pAbc->pGia );
// printf( "\nThis command is currently disabled.\n\n" );
return 0;
diff --git a/src/base/wlc/wlc.c b/src/base/wlc/wlc.c
index 8e853181..6f0890e2 100644
--- a/src/base/wlc/wlc.c
+++ b/src/base/wlc/wlc.c
@@ -19,6 +19,7 @@
***********************************************************************/
#include "wlc.h"
+#include "sat/bsat/satStore.h"
ABC_NAMESPACE_IMPL_START
@@ -127,6 +128,143 @@ void Wlc_GenerateCodeMax4( int nBits )
}
+/**Function*************************************************************
+
+ Synopsis []
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+void Wlc_BlastFullAdderCtrlCnf( sat_solver * pSat, int a, int ac, int b, int c, int * pc, int * ps, int * piVars )
+{
+ int Cnf[12][6] = { // xabc cs // abc cs
+
+ { -1, 0, 0, 0, 0, 0 }, // -000 00 // 000 00
+ { -1, 0, 0, 1, 0, 1 }, // -001 01 // 001 01
+ { -1, 0, 1, 0, 0, 1 }, // -010 01 // 010 01
+ { -1, 0, 1, 1, 1, 0 }, // -011 10 // 011 10
+
+ { 0,-1, 0, 0, 0, 0 }, // 0-00 00
+ { 0,-1, 0, 1, 0, 1 }, // 0-01 01
+ { 0,-1, 1, 0, 0, 1 }, // 0-10 01
+ { 0,-1, 1, 1, 1, 0 }, // 0-11 10
+
+ { 1, 1, 0, 0, 0, 1 }, // 1100 01 // 100 01
+ { 1, 1, 0, 1, 1, 0 }, // 1101 10 // 101 10
+ { 1, 1, 1, 0, 1, 0 }, // 1110 10 // 110 10
+ { 1, 1, 1, 1, 1, 1 } // 1111 11 // 111 11
+ };
+
+ int pVars[6] = {a, ac, b, c, *piVars, *piVars+1};
+ int i, v, nLits, pLits[6];
+ for ( i = 0; i < 12; i++ )
+ {
+ nLits = 0;
+ for ( v = 0; v < 6; v++ )
+ {
+ if ( Cnf[i][v] == -1 )
+ continue;
+ if ( pVars[v] == 0 ) // const 0
+ {
+ if ( Cnf[i][v] == 0 )
+ continue;
+ if ( Cnf[i][v] == 1 )
+ break;
+ }
+ if ( pVars[v] == -1 ) // const -1
+ {
+ if ( Cnf[i][v] == 0 )
+ break;
+ if ( Cnf[i][v] == 1 )
+ continue;
+ }
+ pLits[nLits++] = Abc_Var2Lit( pVars[v], Cnf[i][v] );
+ }
+ if ( v < 6 )
+ continue;
+ assert( nLits > 2 );
+ sat_solver_addclause( pSat, pLits, pLits + nLits );
+ }
+ *pc = (*piVars)++;
+ *ps = (*piVars)++;
+}
+void Wlc_BlastMultiplierCnf( sat_solver * pSat, int * pArgA, int * pArgB, int nArgA, int nArgB, Vec_Int_t * vTemp, Vec_Int_t * vRes, int * piVars )
+{
+ int * pRes, * pArgC, * pArgS, a, b, Carry = 0;
+ assert( nArgA > 0 && nArgB > 0 );
+ // prepare result
+ Vec_IntFill( vRes, nArgA + nArgB, 0 );
+ pRes = Vec_IntArray( vRes );
+ // prepare intermediate storage
+ Vec_IntFill( vTemp, 2 * nArgA, 0 );
+ pArgC = Vec_IntArray( vTemp );
+ pArgS = pArgC + nArgA;
+ // create matrix
+ for ( b = 0; b < nArgB; b++ )
+ for ( a = 0; a < nArgA; a++ )
+ Wlc_BlastFullAdderCtrlCnf( pSat, pArgA[a], pArgB[b], pArgS[a], pArgC[a], &pArgC[a], a ? &pArgS[a-1] : &pRes[b], piVars );
+ // final addition
+ pArgS[nArgA-1] = 0;
+ for ( a = 0; a < nArgA; a++ )
+ Wlc_BlastFullAdderCtrlCnf( pSat, -1, pArgC[a], pArgS[a], Carry, &Carry, &pRes[nArgB+a], piVars );
+}
+sat_solver * Wlc_BlastMultiplierCnfMain( int nBits )
+{
+ Vec_Int_t * vRes1 = Vec_IntAlloc( 2*nBits );
+ Vec_Int_t * vRes2 = Vec_IntAlloc( 2*nBits );
+ Vec_Int_t * vTemp = Vec_IntAlloc( 2*nBits );
+
+ int * pArgA = ABC_ALLOC( int, nBits );
+ int * pArgB = ABC_ALLOC( int, nBits );
+ int i, Ent1, Ent2, nVars = 1 + 2*nBits;
+ int nVarsAll = 1 + 4*nBits + 4*nBits*(nBits + 1);
+
+ sat_solver * pSat = sat_solver_new();
+ sat_solver_setnvars( pSat, nVarsAll );
+
+ for ( i = 0; i < nBits; i++ )
+ pArgA[i] = 1 + i, pArgB[i] = 1 + nBits + i;
+ Wlc_BlastMultiplierCnf( pSat, pArgA, pArgB, nBits, nBits, vTemp, vRes1, &nVars );
+
+ for ( i = 0; i < nBits; i++ )
+ pArgA[i] = 1 + nBits + i, pArgB[i] = 1 + i;
+ Wlc_BlastMultiplierCnf( pSat, pArgA, pArgB, nBits, nBits, vTemp, vRes2, &nVars );
+
+ Vec_IntClear( vTemp );
+ Vec_IntForEachEntryTwo( vRes1, vRes2, Ent1, Ent2, i )
+ {
+ Vec_IntPush( vTemp, Abc_Var2Lit(nVars, 0) );
+ sat_solver_add_xor( pSat, Ent1, Ent2, nVars++, 0 );
+ }
+ assert( nVars == nVarsAll );
+ sat_solver_addclause( pSat, Vec_IntArray(vTemp), Vec_IntLimit(vTemp) );
+
+ ABC_FREE( pArgA );
+ ABC_FREE( pArgB );
+ Vec_IntFree( vRes1 );
+ Vec_IntFree( vRes2 );
+ Vec_IntFree( vTemp );
+ return pSat;
+}
+void Wlc_BlastMultiplierCnfTest( int nBits )
+{
+ abctime clk = Abc_Clock();
+ sat_solver * pSat = Wlc_BlastMultiplierCnfMain( nBits );
+ int i, status = sat_solver_solve( pSat, NULL, NULL, 0, 0, 0, 0 );
+ Sat_SolverWriteDimacs( pSat, "test_mult.cnf", NULL, NULL, 0 );
+ for ( i = 0; i < sat_solver_nvars(pSat); i++ )
+ printf( "%d=%d ", i, sat_solver_var_value(pSat, i) );
+ printf( "\n" );
+
+ printf( "Verifying for %d bits: %s ", nBits, status == l_True ? "SAT" : "UNSAT" );
+ Abc_PrintTime( 1, "Time", Abc_Clock() - clk );
+ sat_solver_delete( pSat );
+}
+
////////////////////////////////////////////////////////////////////////
/// END OF FILE ///
////////////////////////////////////////////////////////////////////////
diff --git a/src/map/mio/mio.c b/src/map/mio/mio.c
index 1f7ff612..8648a604 100644
--- a/src/map/mio/mio.c
+++ b/src/map/mio/mio.c
@@ -286,18 +286,14 @@ int Mio_CommandReadGenlib( Abc_Frame_t * pAbc, int argc, char **argv )
Amap_Lib_t * pLib2;
char * pFileName;
char * pExcludeFile = NULL;
- int fVerbose;
- double WireDelay;
- int c;
+ double WireDelay = 0.0;
+ int fShortNames = 0;
+ int c, fVerbose = 1;
pOut = Abc_FrameReadOut(pAbc);
pErr = Abc_FrameReadErr(pAbc);
-
- // set the defaults
- WireDelay = 0.0;
- fVerbose = 1;
Extra_UtilGetoptReset();
- while ( (c = Extra_UtilGetopt(argc, argv, "WEvh")) != EOF )
+ while ( (c = Extra_UtilGetopt(argc, argv, "WEnvh")) != EOF )
{
switch (c)
{
@@ -321,6 +317,9 @@ int Mio_CommandReadGenlib( Abc_Frame_t * pAbc, int argc, char **argv )
pExcludeFile = argv[globalUtilOptind];
globalUtilOptind++;
break;
+ case 'n':
+ fShortNames ^= 1;
+ break;
case 'v':
fVerbose ^= 1;
break;
@@ -358,6 +357,10 @@ int Mio_CommandReadGenlib( Abc_Frame_t * pAbc, int argc, char **argv )
if ( fVerbose )
printf( "Entered genlib library with %d gates from file \"%s\".\n", Mio_LibraryReadGateNum(pLib), pFileName );
+ // convert the library if needed
+ if ( fShortNames )
+ Mio_LibraryShortNames( pLib );
+
// add the fixed number (wire delay) to all delays in the library
if ( WireDelay != 0.0 )
Mio_LibraryShiftDelay( pLib, WireDelay );
@@ -376,13 +379,14 @@ int Mio_CommandReadGenlib( Abc_Frame_t * pAbc, int argc, char **argv )
return 0;
usage:
- fprintf( pErr, "usage: read_genlib [-W float] [-E filename] [-vh]\n");
+ fprintf( pErr, "usage: read_genlib [-W float] [-E filename] [-nvh]\n");
fprintf( pErr, "\t read the library from a genlib file\n" );
fprintf( pErr, "\t (if the library contains more than one gate\n" );
fprintf( pErr, "\t with the same Boolean function, only the gate\n" );
fprintf( pErr, "\t with the smallest area will be used)\n" );
fprintf( pErr, "\t-W float : wire delay (added to pin-to-pin gate delays) [default = %g]\n", WireDelay );
fprintf( pErr, "\t-E file : the file name with gates to be excluded [default = none]\n" );
+ fprintf( pErr, "\t-n : toggle replacing gate/pin names by short strings [default = %s]\n", fShortNames? "yes": "no" );
fprintf( pErr, "\t-v : toggle verbose printout [default = %s]\n", fVerbose? "yes": "no" );
fprintf( pErr, "\t-h : enable verbose output\n");
return 1;
diff --git a/src/map/mio/mio.h b/src/map/mio/mio.h
index 3f5df736..f45cce89 100644
--- a/src/map/mio/mio.h
+++ b/src/map/mio/mio.h
@@ -213,6 +213,11 @@ extern void Mio_LibraryTransferProfile( Mio_Library_t * pLibDst, Mi
extern void Mio_LibraryTransferProfile2( Mio_Library_t * pLibDst, Mio_Library_t * pLibSrc );
extern int Mio_LibraryHasProfile( Mio_Library_t * pLib );
extern void Mio_LibraryCleanProfile2( Mio_Library_t * pLib );
+extern void Mio_LibraryShortNames( Mio_Library_t * pLib );
+
+extern void Mio_LibraryMatchesStop( Mio_Library_t * pLib );
+extern void Mio_LibraryMatchesStart( Mio_Library_t * pLib, int fPinFilter, int fPinPerm, int fPinQuick );
+extern void Mio_LibraryMatchesFetch( Mio_Library_t * pLib, Vec_Mem_t ** pvTtMem, Vec_Wec_t ** pvTt2Match, Mio_Cell2_t ** ppCells, int * pnCells, int fPinFilter, int fPinPerm, int fPinQuick );
/*=== sclUtil.c =========================================================*/
extern Mio_Library_t * Abc_SclDeriveGenlibSimple( void * pScl );
diff --git a/src/map/mio/mioInt.h b/src/map/mio/mioInt.h
index 541a7a7f..23f48b2f 100644
--- a/src/map/mio/mioInt.h
+++ b/src/map/mio/mioInt.h
@@ -76,6 +76,14 @@ struct Mio_LibraryStruct_t_
st__table * tName2Gate; // the mapping of gate names into their pointer
Mem_Flex_t * pMmFlex; // the memory manaqer for SOPs
Vec_Str_t * vCube; // temporary cube
+ // matching
+ int fPinFilter; // pin filtering
+ int fPinPerm; // pin permutation
+ int fPinQuick; // pin permutation
+ Vec_Mem_t * vTtMem; // truth tables
+ Vec_Wec_t * vTt2Match; // matches for truth tables
+ Mio_Cell2_t * pCells; // library gates
+ int nCells; // library gate count
};
struct Mio_GateStruct_t_
diff --git a/src/map/mio/mioUtils.c b/src/map/mio/mioUtils.c
index 101d5d0f..7572b27c 100644
--- a/src/map/mio/mioUtils.c
+++ b/src/map/mio/mioUtils.c
@@ -53,6 +53,7 @@ void Mio_LibraryDelete( Mio_Library_t * pLib )
Mio_Gate_t * pGate, * pGate2;
if ( pLib == NULL )
return;
+ Mio_LibraryMatchesStop( pLib );
// free the bindings of nodes to gates from this library for all networks
Abc_FrameUnmapAllNetworks( Abc_FrameGetGlobalFrame() );
// free the library
@@ -732,8 +733,13 @@ Mio_Cell2_t * Mio_CollectRootsNew2( Mio_Library_t * pLib, int nInputs, int * pnG
assert( Mio_AreaCompare2( ppCells + 4, ppCells + iCell - 1 ) <= 0 );
}
// assign IDs
+ Mio_LibraryForEachGate( pLib, pGate0 )
+ Mio_GateSetCell( pGate0, -1 );
for ( i = 0; i < iCell; i++ )
+ {
ppCells[i].Id = ppCells[i].pName ? i : -1;
+ Mio_GateSetCell( (Mio_Gate_t *)ppCells[i].pMioGate, i );
+ }
// report
if ( fVerbose )
@@ -1465,6 +1471,177 @@ void Mio_LibraryCleanProfile2( Mio_Library_t * pLib )
Mio_GateSetProfile2( pGate, 0 );
}
+/**Function*************************************************************
+
+ Synopsis []
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+void Mio_LibraryHashGates( Mio_Library_t * pLib )
+{
+ Mio_Gate_t * pGate;
+ Mio_LibraryForEachGate( pLib, pGate )
+ if ( pGate->pTwin )
+ {
+ printf( "Gates with multiple outputs are not supported.\n" );
+ return;
+ }
+ if ( pLib->tName2Gate )
+ st__free_table( pLib->tName2Gate );
+ pLib->tName2Gate = st__init_table(strcmp, st__strhash);
+ Mio_LibraryForEachGate( pLib, pGate )
+ st__insert( pLib->tName2Gate, pGate->pName, (char *)pGate );
+}
+
+/**Function*************************************************************
+
+ Synopsis []
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+static inline int Abc_SclIsChar( char c )
+{
+ return (c >= 'a' && c <= 'z') || (c >= 'A' && c <= 'Z') || c == '_';
+}
+static inline int Abc_SclIsName( char c )
+{
+ return Abc_SclIsChar(c) || (c >= '0' && c <= '9');
+}
+static inline char * Abc_SclFindLimit( char * pName )
+{
+ assert( Abc_SclIsChar(*pName) );
+ while ( Abc_SclIsName(*pName) )
+ pName++;
+ return pName;
+}
+static inline int Abc_SclAreEqual( char * pBase, char * pName, char * pLimit )
+{
+ return !strncmp( pBase, pName, pLimit - pName );
+}
+void Mio_LibraryShortFormula( Mio_Gate_t * pCell, char * pForm, char * pBuffer )
+{
+ Mio_Pin_t * pPin;
+ char * pTemp, * pLimit; int i;
+ if ( !strncmp(pForm, "CONST", 5) )
+ {
+ sprintf( pBuffer, "%s", pForm );
+ return;
+ }
+ for ( pTemp = pForm; *pTemp; )
+ {
+ if ( !Abc_SclIsChar(*pTemp) )
+ {
+ *pBuffer++ = *pTemp++;
+ continue;
+ }
+ pLimit = Abc_SclFindLimit( pTemp );
+ i = 0;
+ Mio_GateForEachPin( pCell, pPin )
+ {
+ if ( Abc_SclAreEqual( pPin->pName, pTemp, pLimit ) )
+ {
+ *pBuffer++ = 'a' + i;
+ break;
+ }
+ i++;
+ }
+ pTemp = pLimit;
+ }
+ *pBuffer++ = 0;
+}
+void Mio_LibraryShortNames( Mio_Library_t * pLib )
+{
+ char Buffer[10000];
+ Mio_Gate_t * pGate; Mio_Pin_t * pPin;
+ int c = 0, i, nDigits = Abc_Base10Log( Mio_LibraryReadGateNum(pLib) );
+ // itereate through classes
+ Mio_LibraryForEachGate( pLib, pGate )
+ {
+ ABC_FREE( pGate->pName );
+ sprintf( Buffer, "g%0*d", nDigits, ++c );
+ pGate->pName = Abc_UtilStrsav( Buffer );
+ // update formula
+ Mio_LibraryShortFormula( pGate, pGate->pForm, Buffer );
+ ABC_FREE( pGate->pForm );
+ pGate->pForm = Abc_UtilStrsav( Buffer );
+ // pin names
+ i = 0;
+ Mio_GateForEachPin( pGate, pPin )
+ {
+ ABC_FREE( pPin->pName );
+ sprintf( Buffer, "%c", 'a'+i );
+ pPin->pName = Abc_UtilStrsav( Buffer );
+ i++;
+ }
+ // output pin
+ ABC_FREE( pGate->pOutName );
+ sprintf( Buffer, "z" );
+ pGate->pOutName = Abc_UtilStrsav( Buffer );
+ }
+ Mio_LibraryHashGates( pLib );
+ // update library name
+ printf( "Renaming library \"%s\" into \"%s%d\".\n", pLib->pName, "lib", Mio_LibraryReadGateNum(pLib) );
+ ABC_FREE( pLib->pName );
+ sprintf( Buffer, "lib%d", Mio_LibraryReadGateNum(pLib) );
+ pLib->pName = Abc_UtilStrsav( Buffer );
+}
+
+/**Function*************************************************************
+
+ Synopsis []
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+void Mio_LibraryMatchesStop( Mio_Library_t * pLib )
+{
+ if ( !pLib->vTtMem )
+ return;
+ Vec_WecFree( pLib->vTt2Match );
+ Vec_MemHashFree( pLib->vTtMem );
+ Vec_MemFree( pLib->vTtMem );
+ ABC_FREE( pLib->pCells );
+}
+void Mio_LibraryMatchesStart( Mio_Library_t * pLib, int fPinFilter, int fPinPerm, int fPinQuick )
+{
+ extern Mio_Cell2_t * Nf_StoDeriveMatches( Vec_Mem_t * vTtMem, Vec_Wec_t * vTt2Match, int * pnCells, int fPinFilter, int fPinPerm, int fPinQuick );
+ if ( pLib->vTtMem && pLib->fPinFilter == fPinFilter && pLib->fPinPerm == fPinPerm && pLib->fPinQuick == fPinQuick )
+ return;
+ if ( pLib->vTtMem )
+ Mio_LibraryMatchesStop( pLib );
+ pLib->fPinFilter = fPinFilter; // pin filtering
+ pLib->fPinPerm = fPinPerm; // pin permutation
+ pLib->fPinQuick = fPinQuick; // pin permutation
+ pLib->vTtMem = Vec_MemAllocForTT( 6, 0 );
+ pLib->vTt2Match = Vec_WecAlloc( 1000 );
+ Vec_WecPushLevel( pLib->vTt2Match );
+ Vec_WecPushLevel( pLib->vTt2Match );
+ assert( Vec_WecSize(pLib->vTt2Match) == Vec_MemEntryNum(pLib->vTtMem) );
+ pLib->pCells = Nf_StoDeriveMatches( pLib->vTtMem, pLib->vTt2Match, &pLib->nCells, fPinFilter, fPinPerm, fPinQuick );
+}
+void Mio_LibraryMatchesFetch( Mio_Library_t * pLib, Vec_Mem_t ** pvTtMem, Vec_Wec_t ** pvTt2Match, Mio_Cell2_t ** ppCells, int * pnCells, int fPinFilter, int fPinPerm, int fPinQuick )
+{
+ Mio_LibraryMatchesStart( pLib, fPinFilter, fPinPerm, fPinQuick );
+ *pvTtMem = pLib->vTtMem; // truth tables
+ *pvTt2Match = pLib->vTt2Match; // matches for truth tables
+ *ppCells = pLib->pCells; // library gates
+ *pnCells = pLib->nCells; // library gate count
+}
+
////////////////////////////////////////////////////////////////////////
/// END OF FILE ///
////////////////////////////////////////////////////////////////////////
diff --git a/src/misc/vec/vec.h b/src/misc/vec/vec.h
index ec3a70b8..839acdc3 100644
--- a/src/misc/vec/vec.h
+++ b/src/misc/vec/vec.h
@@ -36,6 +36,8 @@
#include "vecAtt.h"
#include "vecWrd.h"
#include "vecBit.h"
+#include "vecMem.h"
+#include "vecWec.h"
////////////////////////////////////////////////////////////////////////
/// MACRO DEFINITIONS ///
diff --git a/src/opt/fxch/module.make b/src/opt/fxch/module.make
index 48f36b13..630acb90 100644
--- a/src/opt/fxch/module.make
+++ b/src/opt/fxch/module.make
@@ -1,4 +1,4 @@
SRC += src/opt/fxch/Fxch.c \
src/opt/fxch/FxchDiv.c \
src/opt/fxch/FxchMan.c \
- src/opt/fxch/FxchSCHashTable.c \
+ src/opt/fxch/FxchSCHashTable.c
diff --git a/src/opt/sfm/module.make b/src/opt/sfm/module.make
index fbdaa2ec..66518e4e 100644
--- a/src/opt/sfm/module.make
+++ b/src/opt/sfm/module.make
@@ -1,4 +1,5 @@
-SRC += src/opt/sfm/sfmCnf.c \
+SRC += src/opt/sfm/sfmArea.c \
+ src/opt/sfm/sfmCnf.c \
src/opt/sfm/sfmCore.c \
src/opt/sfm/sfmDec.c \
src/opt/sfm/sfmLib.c \
diff --git a/src/opt/sfm/sfmArea.c b/src/opt/sfm/sfmArea.c
new file mode 100644
index 00000000..87f3b511
--- /dev/null
+++ b/src/opt/sfm/sfmArea.c
@@ -0,0 +1,380 @@
+/**CFile****************************************************************
+
+ FileName [sfmArea.c]
+
+ SystemName [ABC: Logic synthesis and verification system.]
+
+ PackageName [SAT-based optimization using internal don't-cares.]
+
+ Synopsis [Area optimization.]
+
+ Author [Alan Mishchenko]
+
+ Affiliation [UC Berkeley]
+
+ Date [Ver. 1.0. Started - June 20, 2005.]
+
+ Revision [$Id: sfmArea.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
+
+***********************************************************************/
+
+#include "sfmInt.h"
+#include "map/mio/mio.h"
+#include "misc/util/utilTruth.h"
+#include "misc/util/utilNam.h"
+#include "map/scl/sclLib.h"
+#include "map/scl/sclCon.h"
+#include "opt/dau/dau.h"
+
+ABC_NAMESPACE_IMPL_START
+
+
+////////////////////////////////////////////////////////////////////////
+/// DECLARATIONS ///
+////////////////////////////////////////////////////////////////////////
+
+////////////////////////////////////////////////////////////////////////
+/// FUNCTION DEFINITIONS ///
+////////////////////////////////////////////////////////////////////////
+
+/**Function*************************************************************
+
+ Synopsis [Precompute cell parameters.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+Vec_Int_t * Abc_NtkPrecomputeCellPairs( Mio_Cell2_t * pCells, int nCells )
+{
+ Vec_Int_t * vInfo = Vec_IntAlloc( 1000 );
+ word iBestArea, tCur, iThis;
+ int * pPerm[7], nPerms[7], Perm[7], * Perm1, * Perm2;
+ int iBestCell, iBestPerm, iBestDiff;
+ int i, k, n, v, p, Count = 0;
+ int iGate1 = -1, iGate2 = -1;
+
+ for ( i = 1; i <= 6; i++ )
+ pPerm[i] = Extra_PermSchedule( i );
+ for ( i = 1; i <= 6; i++ )
+ nPerms[i] = Extra_Factorial( i );
+
+ for ( i = 2; i < nCells; i++ )
+ {
+ int nFanins = pCells[i].nFanins;
+ for ( n = 0; n <= nFanins; n++ )
+ {
+ // get the truth table
+ iThis = (n == nFanins) ? ~pCells[i].uTruth : Abc_Tt6Flip(pCells[i].uTruth, n);
+ // init the comparison
+ iBestArea = ~((word)0);
+ iBestCell = iBestPerm = iBestDiff = -1;
+ // iterate through cells
+ for ( k = 2; k < nCells; k++ )
+ {
+ if ( nFanins != (int)pCells[k].nFanins )
+ continue;
+ if ( i != k && pCells[i].uTruth == pCells[k].uTruth )
+ {
+ iGate1 = i;
+ iGate2 = k;
+ Count++;
+ continue;
+ }
+ // set unit permutation
+ for ( v = 0; v < nFanins; v++ )
+ Perm[v] = v;
+ // go through all permutation of Cell[k]
+ tCur = pCells[k].uTruth;
+ for ( p = 0; p < nPerms[nFanins]; p++ )
+ {
+ if ( iThis == tCur && iBestArea > pCells[k].AreaW )
+ {
+ iBestArea = pCells[k].AreaW;
+ iBestCell = k;
+ iBestPerm = 0;
+ for ( v = 0; v < nFanins; v++ )
+ iBestPerm |= (v << (Perm[v] << 2));
+ iBestDiff = (pCells[i].AreaW >= pCells[k].AreaW) ? (int)(pCells[i].AreaW - pCells[k].AreaW) : -(int)(pCells[k].AreaW - pCells[i].AreaW);
+ }
+ if ( nPerms[nFanins] == 1 )
+ continue;
+ // update
+ tCur = Abc_Tt6SwapAdjacent( tCur, pPerm[nFanins][p] );
+ Perm1 = Perm + pPerm[nFanins][p];
+ Perm2 = Perm1 + 1;
+ ABC_SWAP( int, *Perm1, *Perm2 );
+ }
+ assert( tCur == pCells[k].uTruth );
+ }
+ Vec_IntPushThree( vInfo, iBestCell, iBestPerm, iBestDiff );
+ }
+ }
+
+ for ( i = 1; i <= 6; i++ )
+ ABC_FREE( pPerm[i] );
+ if ( Count )
+ printf( "In this library, %d cell pairs have equal functions (for example, %s and %s).\n", Count/2, pCells[iGate1].pName, pCells[iGate2].pName );
+ return vInfo;
+}
+Vec_Int_t * Abc_NtkPrecomputeFirsts( Mio_Cell2_t * pCells, int nCells )
+{
+ int i, Index = 0;
+ Vec_Int_t * vFirst = Vec_IntStartFull( 2 );
+ for ( i = 2; i < nCells; i++ )
+ {
+ Vec_IntPush( vFirst, Index );
+ Index += 3 * (pCells[i].nFanins + 1);
+ }
+ assert( nCells == Vec_IntSize(vFirst) );
+ return vFirst;
+}
+int Abc_NtkPrecomputePrint( Mio_Cell2_t * pCells, int nCells, Vec_Int_t * vInfo )
+{
+ int i, n, v, Index = 0, nRecUsed = 0;
+ for ( i = 2; i < nCells; i++ )
+ {
+ int nFanins = pCells[i].nFanins;
+ printf( "%3d : %8s Fanins = %d ", i, pCells[i].pName, nFanins );
+ Dau_DsdPrintFromTruth( &pCells[i].uTruth, nFanins );
+ for ( n = 0; n <= nFanins; n++, Index += 3 )
+ {
+ int iCellA = Vec_IntEntry( vInfo, Index+0 );
+ int iPerm = Vec_IntEntry( vInfo, Index+1 );
+ int Diff = Vec_IntEntry( vInfo, Index+2 );
+ if ( iCellA == -1 )
+ continue;
+ printf( "%d : {", n );
+ for ( v = 0; v < nFanins; v++ )
+ printf( " %d ", (iPerm >> (v << 2)) & 15 );
+ printf( "} Index = %d ", Index );
+
+ printf( "Gain = %6.2f ", Scl_Int2Flt(Diff) );
+ Dau_DsdPrintFromTruth( &pCells[iCellA].uTruth, pCells[iCellA].nFanins );
+ nRecUsed++;
+ }
+ }
+ return nRecUsed;
+}
+
+void Abc_NtkPrecomputeCellPairsTest()
+{
+ int nCells;
+ Mio_Cell2_t * pCells = Mio_CollectRootsNewDefault2( 6, &nCells, 0 );
+ Vec_Int_t * vInfo = Abc_NtkPrecomputeCellPairs( pCells, nCells );
+ int nRecUsed = Abc_NtkPrecomputePrint( pCells, nCells, vInfo );
+ // iterate through the cells
+ Vec_Int_t * vFirst = Abc_NtkPrecomputeFirsts( pCells, nCells );
+ printf( "Used records = %d. All records = %d.\n", nRecUsed, Vec_IntSize(vInfo)/3 - nRecUsed );
+ assert( nCells == Vec_IntSize(vFirst) );
+ Vec_IntFree( vFirst );
+ Vec_IntFree( vInfo );
+ ABC_FREE( pCells );
+}
+
+int Abc_NodeCheckFanoutHasFanin( Abc_Obj_t * pNode, Abc_Obj_t * pFanin )
+{
+ Abc_Obj_t * pThis;
+ int i;
+ Abc_ObjForEachFanout( pNode, pThis, i )
+ if ( Abc_NodeFindFanin(pThis, pFanin) >= 0 )
+ return i;
+ return -1;
+}
+
+/**Function*************************************************************
+
+ Synopsis [Evaluate changes.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+int Abc_ObjHasDupFanins( Abc_Obj_t * pObj )
+{
+ int * pArray = pObj->vFanins.pArray;
+ int i, k, Limit = Abc_ObjFaninNum(pObj);
+ for ( i = 0; i < Limit; i++ )
+ for ( k = i+1; k < Limit; k++ )
+ if ( pArray[i] == pArray[k] )
+ return 1;
+ return 0;
+}
+int Abc_ObjHasDupFanouts( Abc_Obj_t * pObj )
+{
+ int * pArray = pObj->vFanouts.pArray;
+ int i, k, Limit = Abc_ObjFanoutNum(pObj);
+ for ( i = 0; i < Limit; i++ )
+ for ( k = i+1; k < Limit; k++ )
+ if ( pArray[i] == pArray[k] )
+ return 1;
+ return 0;
+}
+int Abc_ObjChangeEval( Abc_Obj_t * pObj, Vec_Int_t * vInfo, Vec_Int_t * vFirst, int InvArea, int * pfUseInv )
+{
+ Abc_Obj_t * pNext;
+ Mio_Gate_t * pGate = (Mio_Gate_t *)pObj->pData;
+ int iFanCell, iNodeCell = Mio_GateReadCell( (Mio_Gate_t *)pObj->pData );
+ int * pFanInfo, * pNodeInfo = Vec_IntEntryP( vInfo, Vec_IntEntry(vFirst, iNodeCell) );
+ int i, fNeedInv = 0, Gain = 0, iFanin = Abc_ObjFaninNum(pObj), fUseInv = Abc_NodeIsInv(pObj);
+ assert( iFanin > 0 );
+ *pfUseInv = 0;
+ if ( pNodeInfo[3*iFanin] == -1 )
+ return 0;
+ if ( fUseInv )
+ Gain = InvArea;
+ else
+ Gain = pNodeInfo[3*iFanin+2];
+ Abc_ObjForEachFanout( pObj, pNext, i )
+ {
+ if ( fUseInv && Abc_NodeFindFanin(pNext, Abc_ObjFanin0(pObj)) >= 0 )
+ return 0;
+ if ( Abc_ObjHasDupFanins(pNext) )
+ return 0;
+ if ( !Abc_ObjIsNode(pNext) || Abc_NodeIsBuf(pNext) )
+ {
+ fNeedInv = 1;
+ continue;
+ }
+ if ( Abc_NodeIsInv(pNext) )
+ {
+ if ( Abc_NodeCheckFanoutHasFanin(pNext, pObj) >= 0 )
+ return 0;
+ Gain += InvArea;
+ continue;
+ }
+ iFanCell = Mio_GateReadCell( (Mio_Gate_t *)pNext->pData );
+ pFanInfo = Vec_IntEntryP( vInfo, Vec_IntEntry(vFirst, iFanCell) );
+ iFanin = Abc_NodeFindFanin( pNext, pObj );
+ if ( pFanInfo[3*iFanin] == -1 )
+ {
+ fNeedInv = 1;
+ continue;
+ }
+ Gain += pFanInfo[3*iFanin+2];
+ }
+ if ( fNeedInv )
+ Gain -= InvArea;
+ *pfUseInv = fNeedInv;
+ return Gain;
+}
+void Abc_ObjChangeUpdate( Abc_Obj_t * pObj, int iFanin, Mio_Cell2_t * pCells, int * pNodeInfo, Vec_Int_t * vTemp )
+{
+ int v, Perm, iNodeCell = pNodeInfo[3*iFanin];
+ Mio_Gate_t * pGate = (Mio_Gate_t *)pObj->pData;
+ //Abc_ObjPrint( stdout, pObj );
+ //printf( "Replacing fanout %d with %s by %s with fanin %d.\n", Abc_ObjId(pObj), Mio_GateReadName(pGate), Mio_GateReadName((Mio_Gate_t *)pCells[iNodeCell].pMioGate), iFanin );
+ pObj->pData = (Mio_Gate_t *)pCells[iNodeCell].pMioGate;
+ Perm = pNodeInfo[3*iFanin+1];
+ Vec_IntClear( vTemp );
+ for ( v = 0; v < Abc_ObjFaninNum(pObj); v++ )
+ Vec_IntPush( vTemp, Abc_ObjFaninId(pObj, (Perm >> (v << 2)) & 15) );
+ Vec_IntClear( &pObj->vFanins );
+ Vec_IntAppend( &pObj->vFanins, vTemp );
+}
+void Abc_ObjChangePerform( Abc_Obj_t * pObj, Vec_Int_t * vInfo, Vec_Int_t * vFirst, int fUseInv, Vec_Int_t * vTemp, Vec_Ptr_t * vFanout, Vec_Ptr_t * vFanout2, Mio_Cell2_t * pCells )
+{
+ Abc_Obj_t * pNext, * pNext2, * pNodeInv = NULL;
+ int iFanCell, iNodeCell = Mio_GateReadCell( (Mio_Gate_t *)pObj->pData );
+ int * pFanInfo, * pNodeInfo = Vec_IntEntryP( vInfo, Vec_IntEntry(vFirst, iNodeCell) );
+ int i, k, iFanin = Abc_ObjFaninNum(pObj);
+ assert( iFanin > 0 && pNodeInfo[3*iFanin] != -1 );
+ // update the node
+ Abc_NodeCollectFanouts( pObj, vFanout );
+ if ( Abc_NodeIsInv(pObj) )
+ {
+ Abc_Obj_t * pFanin = Abc_ObjFanin0(pObj);
+ Vec_PtrForEachEntry( Abc_Obj_t *, vFanout, pNext, k )
+ Abc_ObjPatchFanin( pNext, pObj, pFanin );
+ assert( Abc_ObjFanoutNum(pObj) == 0 );
+ Abc_NtkDeleteObj(pObj);
+ pObj = pFanin;
+ assert( fUseInv == 0 );
+ }
+ else
+ Abc_ObjChangeUpdate( pObj, iFanin, pCells, pNodeInfo, vTemp );
+ // add inverter if needed
+ if ( fUseInv )
+ pNodeInv = Abc_NtkCreateNodeInv(pObj->pNtk, pObj);
+ // update the fanouts
+ Vec_PtrForEachEntry( Abc_Obj_t *, vFanout, pNext, i )
+ {
+ if ( !Abc_ObjIsNode(pNext) || Abc_NodeIsBuf(pNext) )
+ {
+ Abc_ObjPatchFanin( pNext, pObj, pNodeInv );
+ continue;
+ }
+ if ( Abc_NodeIsInv(pNext) )
+ {
+ Abc_NodeCollectFanouts( pNext, vFanout2 );
+ Vec_PtrForEachEntry( Abc_Obj_t *, vFanout2, pNext2, k )
+ Abc_ObjPatchFanin( pNext2, pNext, pObj );
+ assert( Abc_ObjFanoutNum(pNext) == 0 );
+ Abc_NtkDeleteObj(pNext);
+ continue;
+ }
+ iFanin = Abc_NodeFindFanin( pNext, pObj );
+ iFanCell = Mio_GateReadCell( (Mio_Gate_t *)pNext->pData );
+ pFanInfo = Vec_IntEntryP( vInfo, Vec_IntEntry(vFirst, iFanCell) );
+ if ( pFanInfo[3*iFanin] == -1 )
+ {
+ Abc_ObjPatchFanin( pNext, pObj, pNodeInv );
+ continue;
+ }
+ Abc_ObjChangeUpdate( pNext, iFanin, pCells, pFanInfo, vTemp );
+ }
+}
+void Abc_NtkChangePerform( Abc_Ntk_t * pNtk, int fVerbose )
+{
+ abctime clk = Abc_Clock();
+ int i, fNeedInv, nCells, Gain, GainAll = 0, Count = 0, CountInv = 0;
+ Mio_Cell2_t * pCells = Mio_CollectRootsNewDefault2( 6, &nCells, 0 );
+ Vec_Int_t * vInfo = Abc_NtkPrecomputeCellPairs( pCells, nCells );
+ Vec_Int_t * vFirst = Abc_NtkPrecomputeFirsts( pCells, nCells );
+
+ Vec_Ptr_t * vFanout = Vec_PtrAlloc( 100 );
+ Vec_Ptr_t * vFanout2 = Vec_PtrAlloc( 100 );
+ Vec_Int_t * vTemp = Vec_IntAlloc( 100 );
+ Abc_Obj_t * pObj;
+ Abc_NtkForEachNode( pNtk, pObj, i )
+ {
+ if ( Abc_ObjFaninNum(pObj) < 2 && !Abc_NodeIsInv(pObj) )
+ continue;
+ if ( Abc_ObjHasDupFanouts(pObj) )
+ continue;
+ Gain = Abc_ObjChangeEval( pObj, vInfo, vFirst, (int)pCells[3].AreaW, &fNeedInv );
+ if ( Gain <= 0 )
+ continue;
+ //printf( "Obj %d\n", Abc_ObjId(pObj) );
+ Count++;
+ CountInv += Abc_NodeIsInv(pObj);
+ GainAll += Gain;
+ Abc_ObjChangePerform( pObj, vInfo, vFirst, fNeedInv, vTemp, vFanout, vFanout2, pCells );
+ }
+ Vec_PtrFree( vFanout2 );
+ Vec_PtrFree( vFanout );
+ Vec_IntFree( vTemp );
+
+ Vec_IntFree( vFirst );
+ Vec_IntFree( vInfo );
+ ABC_FREE( pCells );
+
+ if ( fVerbose )
+ printf( "Total gain in area = %6.2f after %d changes (including %d inverters). ", Scl_Int2Flt(GainAll), Count, CountInv );
+ if ( fVerbose )
+ Abc_PrintTime( 1, "Time", Abc_Clock() - clk );
+}
+
+////////////////////////////////////////////////////////////////////////
+/// END OF FILE ///
+////////////////////////////////////////////////////////////////////////
+
+
+ABC_NAMESPACE_IMPL_END
+
diff --git a/src/opt/sfm/sfmDec.c b/src/opt/sfm/sfmDec.c
index bce20624..c5af0ac0 100644
--- a/src/opt/sfm/sfmDec.c
+++ b/src/opt/sfm/sfmDec.c
@@ -2152,6 +2152,11 @@ void Abc_NtkPerformMfs3( Abc_Ntk_t * pNtk, Sfm_Par_t * pPars )
if ( pPars->fLibVerbose )
Sfm_LibPrint( p->pLib );
Sfm_DecStop( p );
+ if ( pPars->fArea )
+ {
+ extern void Abc_NtkChangePerform( Abc_Ntk_t * pNtk, int fVerbose );
+ Abc_NtkChangePerform( pNtk, pPars->fVerbose );
+ }
}
////////////////////////////////////////////////////////////////////////
diff --git a/src/sat/bmc/bmcGen.c b/src/sat/bmc/bmcGen.c
new file mode 100644
index 00000000..74af1b78
--- /dev/null
+++ b/src/sat/bmc/bmcGen.c
@@ -0,0 +1,195 @@
+/**CFile****************************************************************
+
+ FileName [bmcGen.c]
+
+ SystemName [ABC: Logic synthesis and verification system.]
+
+ PackageName [SAT-based bounded model checking.]
+
+ Synopsis [Generating satisfying assignments.]
+
+ Author [Alan Mishchenko]
+
+ Affiliation [UC Berkeley]
+
+ Date [Ver. 1.0. Started - June 20, 2005.]
+
+ Revision [$Id: bmcGen.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
+
+***********************************************************************/
+
+#include "bmc.h"
+#include "sat/cnf/cnf.h"
+#include "sat/bsat/satStore.h"
+
+ABC_NAMESPACE_IMPL_START
+
+
+////////////////////////////////////////////////////////////////////////
+/// DECLARATIONS ///
+////////////////////////////////////////////////////////////////////////
+
+extern Cnf_Dat_t * Mf_ManGenerateCnf( Gia_Man_t * pGia, int nLutSize, int fCnfObjIds, int fAddOrCla, int fVerbose );
+
+////////////////////////////////////////////////////////////////////////
+/// FUNCTION DEFINITIONS ///
+////////////////////////////////////////////////////////////////////////
+
+/**Function*************************************************************
+
+ Synopsis []
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+static inline word * Gia_ManMoObj( Gia_Man_t * p, int iObj )
+{
+ return Vec_WrdEntryP( p->vSims, iObj * p->iPatsPi );
+}
+static inline void Gia_ManMoSetCi( Gia_Man_t * p, int iObj )
+{
+ int w;
+ word * pSims = Gia_ManMoObj( p, iObj );
+ for ( w = 0; w < p->iPatsPi; w++ )
+ pSims[w] = Gia_ManRandomW( 0 );
+}
+static inline void Gia_ManMoSimAnd( Gia_Man_t * p, int iObj )
+{
+ int w;
+ Gia_Obj_t * pObj = Gia_ManObj( p, iObj );
+ word * pSims = Gia_ManMoObj( p, iObj );
+ word * pSims0 = Gia_ManMoObj( p, Gia_ObjFaninId0(pObj, iObj) );
+ word * pSims1 = Gia_ManMoObj( p, Gia_ObjFaninId1(pObj, iObj) );
+ if ( Gia_ObjFaninC0(pObj) )
+ {
+ if ( Gia_ObjFaninC1(pObj) )
+ for ( w = 0; w < p->iPatsPi; w++ )
+ pSims[w] = ~(pSims0[w] | pSims1[w]);
+ else
+ for ( w = 0; w < p->iPatsPi; w++ )
+ pSims[w] = ~pSims0[w] & pSims1[w];
+ }
+ else
+ {
+ if ( Gia_ObjFaninC1(pObj) )
+ for ( w = 0; w < p->iPatsPi; w++ )
+ pSims[w] = pSims0[w] & ~pSims1[w];
+ else
+ for ( w = 0; w < p->iPatsPi; w++ )
+ pSims[w] = pSims0[w] & pSims1[w];
+ }
+}
+static inline void Gia_ManMoSetCo( Gia_Man_t * p, int iObj )
+{
+ int w;
+ Gia_Obj_t * pObj = Gia_ManObj( p, iObj );
+ word * pSims = Gia_ManMoObj( p, iObj );
+ word * pSims0 = Gia_ManMoObj( p, Gia_ObjFaninId0(pObj, iObj) );
+ if ( Gia_ObjFaninC0(pObj) )
+ {
+ for ( w = 0; w < p->iPatsPi; w++ )
+ pSims[w] = ~pSims0[w];
+ }
+ else
+ {
+ for ( w = 0; w < p->iPatsPi; w++ )
+ pSims[w] = pSims0[w];
+ }
+}
+void Gia_ManMoFindSimulate( Gia_Man_t * p, int nWords )
+{
+ int i, iObj;
+ Gia_ManRandomW( 1 );
+ p->iPatsPi = nWords;
+ if ( p->vSims )
+ Vec_WrdFill( p->vSims, nWords * Gia_ManObjNum(p), 0 );
+ else
+ p->vSims = Vec_WrdStart( nWords * Gia_ManObjNum(p) );
+ Gia_ManForEachCiId( p, iObj, i )
+ Gia_ManMoSetCi( p, iObj );
+ Gia_ManForEachAndId( p, iObj )
+ Gia_ManMoSimAnd( p, iObj );
+ Gia_ManForEachCoId( p, iObj, i )
+ Gia_ManMoSetCo( p, iObj );
+}
+
+/**Function*************************************************************
+
+ Synopsis []
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+int Gia_ManTestSatEnum( Gia_Man_t * p )
+{
+ abctime clk = Abc_Clock(), clk2, clkTotal = 0;
+ Cnf_Dat_t * pCnf = Mf_ManGenerateCnf( p, 8, 0, 0, 0 );
+ sat_solver * pSat = (sat_solver *)Cnf_DataWriteIntoSolver(pCnf, 1, 0);
+ int i, v, status, iLit, nWords = 1, iOutVar = 1, Count = 0;
+ Vec_Int_t * vVars = Vec_IntAlloc( 1000 );
+ word * pSimInfo;
+
+ // add literals to the solver
+ iLit = Abc_Var2Lit( iOutVar, 0 );
+ status = sat_solver_addclause( pSat, &iLit, &iLit + 1 );
+ assert( status );
+
+ // simulate the AIG
+ Gia_ManMoFindSimulate( p, nWords );
+
+ // print outputs
+ pSimInfo = Gia_ManMoObj( p, Gia_ObjId(p, Gia_ManCo(p, 0)) );
+ for ( i = 0; i < 64*nWords; i++ )
+ printf( "%d", Abc_InfoHasBit( (unsigned *)pSimInfo, i ) );
+ printf( "\n" );
+
+ // iterate through the assignments
+ for ( i = 0; i < 64*nWords; i++ )
+ {
+ Vec_IntClear( vVars );
+ for ( v = 0; v < Gia_ManObjNum(p); v++ )
+ {
+ if ( pCnf->pVarNums[v] == -1 )
+ continue;
+ pSimInfo = Gia_ManMoObj( p, v );
+ if ( !Abc_InfoHasBit( (unsigned *)pSimInfo, i ) )
+ continue;
+ Vec_IntPush( vVars, pCnf->pVarNums[v] );
+ }
+ //sat_solver_act_var_clear( pSat );
+ //sat_solver_set_polarity( pSat, Vec_IntArray(vVars), Vec_IntSize(vVars) );
+
+ clk2 = Abc_Clock();
+ status = sat_solver_solve( pSat, NULL, NULL, 0, 0, 0, 0 );
+ clkTotal += Abc_Clock() - clk2;
+ printf( "%c", status == l_True ? '+' : '-' );
+ if ( status == l_True )
+ Count++;
+ }
+ printf( "\n" );
+ printf( "Finished generating %d assignments. ", Count );
+ Abc_PrintTime( 1, "Time", Abc_Clock() - clk );
+ Abc_PrintTime( 1, "SAT solver time", clkTotal );
+
+ Vec_WrdFreeP( &p->vSims );
+ Vec_IntFree( vVars );
+ sat_solver_delete( pSat );
+ Cnf_DataFree( pCnf );
+ return 1;
+}
+
+////////////////////////////////////////////////////////////////////////
+/// END OF FILE ///
+////////////////////////////////////////////////////////////////////////
+
+
+ABC_NAMESPACE_IMPL_END
+
diff --git a/src/sat/bmc/module.make b/src/sat/bmc/module.make
index e1777df8..40402bf3 100644
--- a/src/sat/bmc/module.make
+++ b/src/sat/bmc/module.make
@@ -16,6 +16,7 @@ SRC += src/sat/bmc/bmcBCore.c \
src/sat/bmc/bmcExpand.c \
src/sat/bmc/bmcFault.c \
src/sat/bmc/bmcFx.c \
+ src/sat/bmc/bmcGen.c \
src/sat/bmc/bmcICheck.c \
src/sat/bmc/bmcInse.c \
src/sat/bmc/bmcLoad.c \
generated by cgit v1.2.3 (git 2.25.1) at 2025-02-09 01:59:28 +0000