diff options
-rw-r--r-- | abclib.dsp | 8 | ||||
-rw-r--r-- | src/aig/gia/giaDup.c | 25 | ||||
-rw-r--r-- | src/aig/gia/giaNf.c | 59 | ||||
-rw-r--r-- | src/base/abci/abc.c | 1 | ||||
-rw-r--r-- | src/base/wlc/wlc.c | 138 | ||||
-rw-r--r-- | src/map/mio/mio.c | 22 | ||||
-rw-r--r-- | src/map/mio/mio.h | 5 | ||||
-rw-r--r-- | src/map/mio/mioInt.h | 8 | ||||
-rw-r--r-- | src/map/mio/mioUtils.c | 177 | ||||
-rw-r--r-- | src/misc/vec/vec.h | 2 | ||||
-rw-r--r-- | src/opt/fxch/module.make | 2 | ||||
-rw-r--r-- | src/opt/sfm/module.make | 3 | ||||
-rw-r--r-- | src/opt/sfm/sfmArea.c | 380 | ||||
-rw-r--r-- | src/opt/sfm/sfmDec.c | 5 | ||||
-rw-r--r-- | src/sat/bmc/bmcGen.c | 195 | ||||
-rw-r--r-- | src/sat/bmc/module.make | 1 |
16 files changed, 970 insertions, 61 deletions
@@ -1875,6 +1875,10 @@ SOURCE=.\src\sat\bmc\bmcFx.c # End Source File # Begin Source File +SOURCE=.\src\sat\bmc\bmcGen.c +# End Source File +# Begin Source File + SOURCE=.\src\sat\bmc\bmcICheck.c # End Source File # Begin Source File @@ -2551,6 +2555,10 @@ SOURCE=.\src\opt\sfm\sfm.h # End Source File # Begin Source File +SOURCE=.\src\opt\sfm\sfmArea.c +# End Source File +# Begin Source File + SOURCE=.\src\opt\sfm\sfmCnf.c # End Source File # Begin Source File 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 \ |