diff options
| -rw-r--r-- | abclib.dsp | 4 | ||||
| -rw-r--r-- | src/base/abci/abc.c | 12 | ||||
| -rw-r--r-- | src/opt/sfm/module.make | 1 | ||||
| -rw-r--r-- | src/opt/sfm/sfmDec.c | 358 | ||||
| -rw-r--r-- | src/opt/sfm/sfmLib.c | 102 |
5 files changed, 282 insertions, 195 deletions
@@ -2527,6 +2527,10 @@ SOURCE=.\src\opt\sfm\sfmInt.h # End Source File # Begin Source File +SOURCE=.\src\opt\sfm\sfmLib.c +# End Source File +# Begin Source File + SOURCE=.\src\opt\sfm\sfmNtk.c # End Source File # Begin Source File diff --git a/src/base/abci/abc.c b/src/base/abci/abc.c index d1c86e62..f2b436f8 100644 --- a/src/base/abci/abc.c +++ b/src/base/abci/abc.c @@ -10820,11 +10820,11 @@ int Abc_CommandTestColor( Abc_Frame_t * pAbc, int argc, char ** argv ) ***********************************************************************/ int Abc_CommandTest( Abc_Frame_t * pAbc, int argc, char ** argv ) { -// Abc_Ntk_t * pNtk = Abc_FrameReadNtk(pAbc); + Abc_Ntk_t * pNtk = Abc_FrameReadNtk(pAbc); int nCutMax = 1; int nLeafMax = 4; int nDivMax = 2; - int nDecMax = 20; + int nDecMax = 70; int nNumOnes = 4; int fNewAlgo = 0; int fNewOrder = 0; @@ -10909,13 +10909,13 @@ int Abc_CommandTest( Abc_Frame_t * pAbc, int argc, char ** argv ) goto usage; } } -/* + if ( pNtk == NULL ) { Abc_Print( -1, "Empty network.\n" ); return 1; } - +/* if ( Abc_NtkIsStrash(pNtk) ) { Abc_Print( -1, "This command works only for logic networks.\n" ); @@ -11029,9 +11029,11 @@ int Abc_CommandTest( Abc_Frame_t * pAbc, int argc, char ** argv ) } { extern void Tab_DecomposeTest(); + extern void Sfm_DecTestBench( Abc_Ntk_t * pNtk, int iNode ); //Tab_DecomposeTest(); extern void Cnf_AddCardinConstrTest(); - Cnf_AddCardinConstrTest(); + //Cnf_AddCardinConstrTest(); + Sfm_DecTestBench( pNtk, nDecMax ); } return 0; usage: diff --git a/src/opt/sfm/module.make b/src/opt/sfm/module.make index c2401559..d9306418 100644 --- a/src/opt/sfm/module.make +++ b/src/opt/sfm/module.make @@ -1,6 +1,7 @@ SRC += src/opt/sfm/sfmCnf.c \ src/opt/sfm/sfmCore.c \ src/opt/sfm/sfmDec.c \ + src/opt/sfm/sfmLib.c \ src/opt/sfm/sfmNtk.c \ src/opt/sfm/sfmSat.c \ src/opt/sfm/sfmWin.c diff --git a/src/opt/sfm/sfmDec.c b/src/opt/sfm/sfmDec.c index c93c2be5..b4376718 100644 --- a/src/opt/sfm/sfmDec.c +++ b/src/opt/sfm/sfmDec.c @@ -19,7 +19,8 @@ ***********************************************************************/ #include "sfmInt.h" -#include "bool/kit/kit.h" +#include "misc/st/st.h" +#include "map/mio/mio.h" #include "base/abc/abc.h" ABC_NAMESPACE_IMPL_START @@ -40,6 +41,11 @@ struct Sfm_Dec_t_ Vec_Int_t vGateSizes; // fanin counts Vec_Wrd_t vGateFuncs; // gate truth tables Vec_Wec_t vGateCnfs; // gate CNFs + Vec_Ptr_t vGateHands; // gate handles + int GateConst0; // special gates + int GateConst1; // special gates + int GateBuffer; // special gates + int GateInvert; // special gates // objects int iTarget; // target node Vec_Int_t vObjTypes; // PI (1), PO (2) @@ -49,6 +55,7 @@ struct Sfm_Dec_t_ sat_solver * pSat; // reusable solver Vec_Wec_t vClauses; // CNF clauses for the node Vec_Int_t vPols[2]; // onset/offset polarity + Vec_Int_t vTaken[2]; // onset/offset implied nodes Vec_Int_t vImpls[2]; // onset/offset implications Vec_Wrd_t vSets[2]; // onset/offset patterns int nPats[3]; @@ -88,6 +95,7 @@ void Sfm_DecStop( Sfm_Dec_t * p ) Vec_IntErase( &p->vGateSizes ); Vec_WrdErase( &p->vGateFuncs ); Vec_WecErase( &p->vGateCnfs ); + Vec_PtrErase( &p->vGateHands ); // objects Vec_IntErase( &p->vObjTypes ); Vec_IntErase( &p->vObjGates ); @@ -97,6 +105,8 @@ void Sfm_DecStop( Sfm_Dec_t * p ) Vec_WecErase( &p->vClauses ); Vec_IntErase( &p->vPols[0] ); Vec_IntErase( &p->vPols[1] ); + Vec_IntErase( &p->vTaken[0] ); + Vec_IntErase( &p->vTaken[1] ); Vec_IntErase( &p->vImpls[0] ); Vec_IntErase( &p->vImpls[1] ); Vec_WrdErase( &p->vSets[0] ); @@ -118,123 +128,38 @@ void Sfm_DecStop( Sfm_Dec_t * p ) SeeAlso [] ***********************************************************************/ -void Sfm_DecCreateCnf( Sfm_Dec_t * p ) -{ - Vec_Str_t * vCnf, * vCnfBase; - Vec_Int_t * vCover; - word uTruth; - int i, nCubes; - vCnf = Vec_StrAlloc( 100 ); - vCover = Vec_IntAlloc( 100 ); - Vec_WecInit( &p->vGateCnfs, Vec_IntSize(&p->vGateSizes) ); - Vec_WrdForEachEntry( &p->vGateFuncs, uTruth, i ) - { - nCubes = Sfm_TruthToCnf( uTruth, Vec_IntEntry(&p->vGateSizes, i), vCover, vCnf ); - vCnfBase = (Vec_Str_t *)Vec_WecEntry( &p->vGateCnfs, i ); - Vec_StrGrow( vCnfBase, Vec_StrSize(vCnf) ); - memcpy( Vec_StrArray(vCnfBase), Vec_StrArray(vCnf), Vec_StrSize(vCnf) ); - vCnfBase->nSize = Vec_StrSize(vCnf); - } - Vec_IntFree( vCover ); - Vec_StrFree( vCnf ); -} - -/**Function************************************************************* - - Synopsis [] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -void Sfm_DecCreateAigLibrary( Sfm_Dec_t * p ) -{ - // const0 - Vec_IntPush( &p->vGateSizes, 0 ); - Vec_WrdPush( &p->vGateFuncs, 0 ); - // const1 - Vec_IntPush( &p->vGateSizes, 0 ); - Vec_WrdPush( &p->vGateFuncs, ~(word)0 ); - // buffer - Vec_IntPush( &p->vGateSizes, 1 ); - Vec_WrdPush( &p->vGateFuncs, ABC_CONST(0xAAAAAAAAAAAAAAAA) ); - // inverter - Vec_IntPush( &p->vGateSizes, 1 ); - Vec_WrdPush( &p->vGateFuncs, ABC_CONST(0x5555555555555555) ); - // and00 - Vec_IntPush( &p->vGateSizes, 2 ); - Vec_WrdPush( &p->vGateFuncs, ABC_CONST(0xCCCCCCCCCCCCCCCC) & ABC_CONST(0xAAAAAAAAAAAAAAAA) ); - // and01 - Vec_IntPush( &p->vGateSizes, 2 ); - Vec_WrdPush( &p->vGateFuncs, ABC_CONST(0xCCCCCCCCCCCCCCCC) &~ABC_CONST(0xAAAAAAAAAAAAAAAA) ); - // and10 - Vec_IntPush( &p->vGateSizes, 2 ); - Vec_WrdPush( &p->vGateFuncs,~ABC_CONST(0xCCCCCCCCCCCCCCCC) & ABC_CONST(0xAAAAAAAAAAAAAAAA) ); - // and11 - Vec_IntPush( &p->vGateSizes, 2 ); - Vec_WrdPush( &p->vGateFuncs,~ABC_CONST(0xCCCCCCCCCCCCCCCC) &~ABC_CONST(0xAAAAAAAAAAAAAAAA) ); -/* - // xor - Vec_IntPush( &p->vGateSizes, 2 ); - Vec_WrdPush( &p->vGateFuncs, ABC_CONST(0xCCCCCCCCCCCCCCCC) ^ ABC_CONST(0xAAAAAAAAAAAAAAAA) ); - // xnor - Vec_IntPush( &p->vGateSizes, 2 ); - Vec_WrdPush( &p->vGateFuncs, ABC_CONST(0xCCCCCCCCCCCCCCCC) ^~ABC_CONST(0xAAAAAAAAAAAAAAAA) ); - // mux - Vec_IntPush( &p->vGateSizes, 3 ); - Vec_WrdPush( &p->vGateFuncs, (ABC_CONST(0xF0F0F0F0F0F0F0F0) & ABC_CONST(0xCCCCCCCCCCCCCCCC)) | (ABC_CONST(0x0F0F0F0F0F0F0F0F) & ABC_CONST(0xAAAAAAAAAAAAAAAA)) ); -*/ - // derive CNF for these functions - Sfm_DecCreateCnf( p ); -} - -void Vec_IntLift( Vec_Int_t * p, int Amount ) -{ - int i; - for ( i = 0; i < p->nSize; i++ ) - p->pArray[i] += Amount; -} - -/**Function************************************************************* - - Synopsis [] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ int Sfm_DecPrepareSolver( Sfm_Dec_t * p ) { abctime clk = Abc_Clock(); + Vec_Int_t * vRoots = &p->vTemp; + Vec_Int_t * vFaninVars = &p->vTemp2; Vec_Int_t * vLevel, * vClause; int i, k, Type, Gate, iObj, RetValue; - int nSatVars = 2 * Vec_IntSize(&p->vObjTypes) - p->iTarget - 1; - assert( Vec_IntSize(&p->vObjTypes) == Vec_IntSize(&p->vObjGates) ); - assert( p->iTarget < Vec_IntSize(&p->vObjTypes) ); + int nTfiSize = p->iTarget + 1; // including node + int nWinSize = Vec_IntSize(&p->vObjTypes); + int nSatVars = 2 * nWinSize - nTfiSize; + assert( nWinSize == Vec_IntSize(&p->vObjGates) ); + assert( p->iTarget < nWinSize ); // collect variables of root nodes - Vec_IntClear( &p->vTemp ); + Vec_IntClear( vRoots ); Vec_IntForEachEntryStart( &p->vObjTypes, Type, i, p->iTarget ) if ( Type == 2 ) - Vec_IntPush( &p->vTemp, i ); - assert( Vec_IntSize(&p->vTemp) > 0 ); + Vec_IntPush( vRoots, i ); + assert( Vec_IntSize(vRoots) > 0 ); // create SAT solver sat_solver_restart( p->pSat ); - sat_solver_setnvars( p->pSat, nSatVars + Vec_IntSize(&p->vTemp) ); + sat_solver_setnvars( p->pSat, nSatVars + Vec_IntSize(vRoots) ); // add CNF clauses for the TFI - Vec_IntForEachEntryStop( &p->vObjTypes, Type, i, p->iTarget + 1 ) + Vec_IntForEachEntryStop( &p->vObjTypes, Type, i, nTfiSize ) { if ( Type == 1 ) continue; + vLevel = Vec_WecEntry( &p->vObjFanins, i ); // generate CNF Gate = Vec_IntEntry( &p->vObjGates, i ); - vLevel = Vec_WecEntry( &p->vObjFanins, i ); + Vec_IntPush( vLevel, i ); Sfm_TranslateCnf( &p->vClauses, (Vec_Str_t *)Vec_WecEntry(&p->vGateCnfs, Gate), vLevel, -1 ); + Vec_IntPop( vLevel ); // add clauses Vec_WecForEachLevel( &p->vClauses, vClause, k ) { @@ -246,15 +171,17 @@ int Sfm_DecPrepareSolver( Sfm_Dec_t * p ) } } // add CNF clauses for the TFO - Vec_IntForEachEntryStart( &p->vObjTypes, Type, i, p->iTarget + 1 ) + Vec_IntForEachEntryStart( &p->vObjTypes, Type, i, nTfiSize ) { assert( Type != 1 ); - // generate CNF - Gate = Vec_IntEntry( &p->vObjGates, i ); vLevel = Vec_WecEntry( &p->vObjFanins, i ); - Vec_IntLift( vLevel, Vec_IntSize(&p->vObjTypes) ); - Sfm_TranslateCnf( &p->vClauses, (Vec_Str_t *)Vec_WecEntry(&p->vGateCnfs, Gate), vLevel, p->iTarget ); - Vec_IntLift( vLevel, Vec_IntSize(&p->vObjTypes) ); + Vec_IntClear( vFaninVars ); + Vec_IntForEachEntry( vLevel, iObj, k ) + Vec_IntPush( vFaninVars, iObj <= p->iTarget ? iObj : iObj + nWinSize - nTfiSize ); + Vec_IntPush( vFaninVars, i + nWinSize - nTfiSize ); + // generate CNF + Gate = Vec_IntEntry( &p->vObjGates, i ); + Sfm_TranslateCnf( &p->vClauses, (Vec_Str_t *)Vec_WecEntry(&p->vGateCnfs, Gate), vFaninVars, p->iTarget ); // add clauses Vec_WecForEachLevel( &p->vClauses, vClause, k ) { @@ -265,21 +192,21 @@ int Sfm_DecPrepareSolver( Sfm_Dec_t * p ) return 0; } } - if ( p->iTarget + 1 < Vec_IntSize(&p->vObjTypes) ) + if ( p->iTarget + 1 < nWinSize ) { // create XOR clauses for the roots - Vec_IntForEachEntry( &p->vTemp, iObj, i ) + Vec_IntForEachEntry( vRoots, iObj, i ) { - sat_solver_add_xor( p->pSat, iObj, 2*iObj + Vec_IntSize(&p->vObjTypes) - p->iTarget - 1, nSatVars++, 0 ); - Vec_IntWriteEntry( &p->vTemp, i, Abc_Var2Lit(nSatVars-1, 0) ); + sat_solver_add_xor( p->pSat, iObj, iObj + nWinSize - nTfiSize, nSatVars++, 0 ); + Vec_IntWriteEntry( vRoots, i, Abc_Var2Lit(nSatVars-1, 0) ); } // make OR clause for the last nRoots variables - RetValue = sat_solver_addclause( p->pSat, Vec_IntArray(&p->vTemp), Vec_IntLimit(&p->vTemp) ); + RetValue = sat_solver_addclause( p->pSat, Vec_IntArray(vRoots), Vec_IntLimit(vRoots) ); if ( RetValue == 0 ) return 0; assert( nSatVars == sat_solver_nvars(p->pSat) ); } - else assert( Vec_IntSize(&p->vTemp) == 1 ); + else assert( Vec_IntSize(vRoots) == 1 ); // finalize RetValue = sat_solver_simplify( p->pSat ); p->timeCnf += Abc_Clock() - clk; @@ -302,7 +229,7 @@ int Sfm_DecPeformDec( Sfm_Dec_t * p ) int fVerbose = 1; int nBTLimit = 0; abctime clk = Abc_Clock(); - int i, k, c, status, Lits[2]; + int i, j, k, c, n, Pol, Pol2, Entry, Entry2, status, Lits[3]; // check stuck-at-0/1 (on/off-set empty) p->nPats[0] = p->nPats[1] = 0; for ( c = 0; c < 2; c++ ) @@ -314,18 +241,20 @@ int Sfm_DecPeformDec( Sfm_Dec_t * p ) if ( status == l_False ) { Vec_IntPush( &p->vObjTypes, 0 ); - Vec_IntPush( &p->vObjGates, c ); + Vec_IntPush( &p->vObjGates, c ? p->GateConst1 : p->GateConst0 ); Vec_WecPushLevel( &p->vObjFanins ); return 1; } assert( status == l_True ); // record this status - for ( i = 0; i < p->iTarget; i++ ) + for ( i = 0; i <= p->iTarget; i++ ) { Vec_IntPush( &p->vPols[c], sat_solver_var_value(p->pSat, i) ); Vec_WrdPush( &p->vSets[c], 0 ); } p->nPats[c]++; + Vec_IntClear( &p->vImpls[c] ); + Vec_IntFill( &p->vTaken[c], p->iTarget, 0 ); } // proceed checking divisors based on their values for ( c = 0; c < 2; c++ ) @@ -335,42 +264,101 @@ int Sfm_DecPeformDec( Sfm_Dec_t * p ) { if ( Vec_WrdEntry(&p->vSets[c], i) ) // diff value is possible continue; - Lits[1] = Abc_Var2Lit( i, Vec_IntEntry(&p->vPols[c], i) ); + Pol = Vec_IntEntry(&p->vPols[c], i); + Lits[1] = Abc_Var2Lit( i, Pol ); status = sat_solver_solve( p->pSat, Lits, Lits + 2, nBTLimit, 0, 0, 0 ); if ( status == l_Undef ) return 0; if ( status == l_False ) { - Vec_IntPush( &p->vImpls[c], i ); + Vec_IntWriteEntry( &p->vTaken[c], i, 1 ); + Vec_IntPushTwo( &p->vImpls[c], Abc_Var2Lit(i, Pol), -1 ); continue; } assert( status == l_True ); + if ( p->nPats[c] == 64 ) + continue; // record this status - for ( i = 0; i < p->iTarget; i++ ) - if ( sat_solver_var_value(p->pSat, i) ^ Vec_IntEntry(&p->vPols[c], i) ) - *Vec_WrdEntryP(&p->vSets[c], i) |= ((word)1 << p->nPats[c]); + for ( k = 0; k <= p->iTarget; k++ ) + if ( sat_solver_var_value(p->pSat, k) ^ Vec_IntEntry(&p->vPols[c], k) ) + *Vec_WrdEntryP(&p->vSets[c], k) |= ((word)1 << p->nPats[c]); p->nPats[c]++; } } + // proceed checking divisor pairs + for ( c = 0; c < 2; c++ ) + { + Lits[0] = Abc_Var2Lit( p->iTarget, c ); + for ( i = 0; i < p->iTarget; i++ ) + if ( !Vec_IntEntry(&p->vTaken[c], i) ) + for ( j = 0; j < i; j++ ) + if ( !Vec_IntEntry(&p->vTaken[c], j) ) + { + word SignI = Vec_WrdEntry(&p->vSets[c], i); + word SignJ = Vec_WrdEntry(&p->vSets[c], j); + for ( n = 0; n < 3; n++ ) + { + if ( ((n&1) ? ~SignI : SignI) & ((n>>1) ? ~SignJ : SignJ) ) // diff value is possible + continue; + Pol = Vec_IntEntry(&p->vPols[c], i) ^ (n&1); + Pol2 = Vec_IntEntry(&p->vPols[c], j) ^ (n>>1); + Lits[1] = Abc_Var2Lit( i, Pol ); + Lits[2] = Abc_Var2Lit( j, Pol2 ); + status = sat_solver_solve( p->pSat, Lits, Lits + 3, nBTLimit, 0, 0, 0 ); + if ( status == l_Undef ) + return 0; + if ( status == l_False ) + { + Vec_IntPushTwo( &p->vImpls[c], Abc_Var2Lit(i, Pol), Abc_Var2Lit(j, Pol2) ); + continue; + } + assert( status == l_True ); + if ( p->nPats[c] == 64 ) + continue; + // record this status + for ( k = 0; k <= p->iTarget; k++ ) + if ( sat_solver_var_value(p->pSat, k) ^ Vec_IntEntry(&p->vPols[c], k) ) + *Vec_WrdEntryP(&p->vSets[c], k) |= ((word)1 << p->nPats[c]); + p->nPats[c]++; + } + } + } + // print the results if ( fVerbose ) for ( c = 0; c < 2; c++ ) { - printf( "\nON-SET reference vertex:\n" ); - for ( i = 0; i < p->iTarget; i++ ) - printf( "%d", Vec_IntEntry(&p->vPols[c], i) ); + Vec_Int_t * vLevel = Vec_WecEntry( &p->vObjFanins, p->iTarget ); + printf( "\n%s-SET of object %d with gate \"%s\" and fanins: ", c ? "OFF": "ON", p->iTarget, Mio_GateReadName((Mio_Gate_t *)Vec_PtrEntry(&p->vGateHands, Vec_IntEntry(&p->vObjGates,p->iTarget))) ); + Vec_IntForEachEntry( vLevel, Entry, i ) + printf( "%d ", Entry ); + printf( "\n" ); + + printf( "Implications: " ); + Vec_IntForEachEntryDouble( &p->vImpls[c], Entry, Entry2, i ) + { + if ( Entry2 == -1 ) + printf( "%s%d ", Abc_LitIsCompl(Entry)? "!":"", Abc_Lit2Var(Entry) ); + else + printf( "%s%d:%s%d ", Abc_LitIsCompl(Entry)? "!":"", Abc_Lit2Var(Entry), Abc_LitIsCompl(Entry2)? "!":"", Abc_Lit2Var(Entry2) ); + } printf( "\n" ); printf( " " ); - for ( i = 0; i < p->iTarget; i++ ) + for ( i = 0; i <= p->iTarget; i++ ) + printf( "%d", Vec_IntEntry(&p->vPols[c], i) ); + printf( "\n\n" ); + printf( " " ); + for ( i = 0; i <= p->iTarget; i++ ) printf( "%d", i % 10 ); printf( "\n" ); for ( k = 0; k < p->nPats[c]; k++ ) { printf( "%2d : ", k ); - for ( i = 0; i < p->iTarget; i++ ) + for ( i = 0; i <= p->iTarget; i++ ) printf( "%d", (int)((Vec_WrdEntry(&p->vSets[c], i) >> k) & 1) ); printf( "\n" ); } + printf( "\n" ); } p->timeSat += Abc_Clock() - clk; return 1; @@ -387,7 +375,7 @@ int Sfm_DecPeformDec( Sfm_Dec_t * p ) SeeAlso [] ***********************************************************************/ -void Abc_NtkDfsReverseOne_rec( Abc_Obj_t * pNode, Vec_Int_t * vNodes ) +void Abc_NtkDfsReverseOne_rec( Abc_Obj_t * pNode, Vec_Int_t * vTfo ) { Abc_Obj_t * pFanout; int i; if ( Abc_NodeIsTravIdCurrent( pNode ) ) @@ -395,15 +383,15 @@ void Abc_NtkDfsReverseOne_rec( Abc_Obj_t * pNode, Vec_Int_t * vNodes ) Abc_NodeSetTravIdCurrent( pNode ); if ( Abc_ObjIsCo(pNode) ) { - Vec_IntPush( vNodes, Abc_ObjId(pNode) ); + Vec_IntPush( vTfo, Abc_ObjId(pNode) ); return; } assert( Abc_ObjIsNode( pNode ) ); Abc_ObjForEachFanout( pNode, pFanout, i ) - Abc_NtkDfsReverseOne_rec( pFanout, vNodes ); - Vec_IntPush( vNodes, Abc_ObjId(pNode) ); + Abc_NtkDfsReverseOne_rec( pFanout, vTfo ); + Vec_IntPush( vTfo, Abc_ObjId(pNode) ); } -void Abc_NtkDfsOne_rec( Abc_Obj_t * pNode, Vec_Int_t * vMap, Vec_Int_t * vTypes ) +void Abc_NtkDfsOne_rec( Abc_Obj_t * pNode, Vec_Int_t * vTfi, Vec_Int_t * vTypes ) { Abc_Obj_t * pFanin; int i; if ( Abc_NodeIsTravIdCurrent( pNode ) ) @@ -411,31 +399,32 @@ void Abc_NtkDfsOne_rec( Abc_Obj_t * pNode, Vec_Int_t * vMap, Vec_Int_t * vTypes Abc_NodeSetTravIdCurrent( pNode ); if ( Abc_ObjIsCi(pNode) ) { - pNode->iTemp = Vec_IntSize(vMap); - Vec_IntPush( vMap, Abc_ObjId(pNode) ); + pNode->iTemp = Vec_IntSize(vTfi); + Vec_IntPush( vTfi, Abc_ObjId(pNode) ); Vec_IntPush( vTypes, 1 ); return; } assert( Abc_ObjIsNode(pNode) ); Abc_ObjForEachFanin( pNode, pFanin, i ) - Abc_NtkDfsOne_rec( pFanin, vMap, vTypes ); - pNode->iTemp = Vec_IntSize(vMap); - Vec_IntPush( vMap, Abc_ObjId(pNode) ); + Abc_NtkDfsOne_rec( pFanin, vTfi, vTypes ); + pNode->iTemp = Vec_IntSize(vTfi); + Vec_IntPush( vTfi, Abc_ObjId(pNode) ); Vec_IntPush( vTypes, 0 ); } -int Sfm_DecExtract( Abc_Ntk_t * pNtk, int iNode, Vec_Int_t * vTypes, Vec_Int_t * vGates, Vec_Wec_t * vFanins, Vec_Int_t * vMap, Vec_Int_t * vTemp ) +int Sfm_DecExtract( Abc_Ntk_t * pNtk, Abc_Obj_t * pNode, Vec_Int_t * vTypes, Vec_Int_t * vGates, Vec_Wec_t * vFanins, Vec_Int_t * vMap, Vec_Int_t * vTfo ) { - Abc_Obj_t * pNode = Abc_NtkObj( pNtk, iNode ); Vec_Int_t * vLevel; - int i, iObj, iTarget; + Abc_Obj_t * pFanin; + int i, k, iObj, iTarget; assert( Abc_ObjIsNode(pNode) ); - // collect transitive fanout - Vec_IntClear( vTemp ); + // collect transitive fanout including COs + Vec_IntClear( vTfo ); Abc_NtkIncrementTravId( pNtk ); - Abc_NtkDfsReverseOne_rec( pNode, vTemp ); + Abc_NtkDfsReverseOne_rec( pNode, vTfo ); // collect transitive fanin Vec_IntClear( vMap ); Vec_IntClear( vTypes ); + Abc_NtkIncrementTravId( pNtk ); Abc_NtkDfsOne_rec( pNode, vMap, vTypes ); Vec_IntPop( vMap ); Vec_IntPop( vTypes ); @@ -443,12 +432,12 @@ int Sfm_DecExtract( Abc_Ntk_t * pNtk, int iNode, Vec_Int_t * vTypes, Vec_Int_t * // remember target node iTarget = Vec_IntSize( vMap ); // add transitive fanout - Vec_IntForEachEntryReverse( vTemp, iObj, i ) + Vec_IntForEachEntryReverse( vTfo, iObj, i ) { pNode = Abc_NtkObj( pNtk, iObj ); if ( Abc_ObjIsCo(pNode) ) { - assert( Vec_IntEntry(vTypes, Abc_ObjFanin0(pNode)->iTemp) == 0 ); + assert( Vec_IntEntry(vTypes, Abc_ObjFanin0(pNode)->iTemp) == 0 ); // CO points to a unique node Vec_IntWriteEntry( vTypes, Abc_ObjFanin0(pNode)->iTemp, 2 ); continue; } @@ -469,74 +458,63 @@ int Sfm_DecExtract( Abc_Ntk_t * pNtk, int iNode, Vec_Int_t * vTypes, Vec_Int_t * Vec_IntPush( vGates, -1 ); continue; } - assert( Abc_ObjFaninNum(pNode) == 2 ); - if ( !Abc_ObjFaninC0(pNode) && !Abc_ObjFaninC1(pNode) ) - Vec_IntPush( vGates, 4 ); - else if ( !Abc_ObjFaninC0(pNode) && Abc_ObjFaninC1(pNode) ) - Vec_IntPush( vGates, 5 ); - else if ( Abc_ObjFaninC0(pNode) && !Abc_ObjFaninC1(pNode) ) - Vec_IntPush( vGates, 6 ); - else //if ( Abc_ObjFaninC0(pNode) && Abc_ObjFaninC1(pNode) ) - Vec_IntPush( vGates, 7 ); - Vec_IntPush( vLevel, Abc_ObjFanin0(pNode)->iTemp ); - Vec_IntPush( vLevel, Abc_ObjFanin1(pNode)->iTemp ); + Abc_ObjForEachFanin( pNode, pFanin, k ) + Vec_IntPush( vLevel, pFanin->iTemp ); + Vec_IntPush( vGates, Mio_GateReadValue((Mio_Gate_t *)pNode->pData) ); } return iTarget; } -void Sfm_DecInsert( Abc_Ntk_t * pNtk, int iNode, int Limit, Vec_Int_t * vTypes, Vec_Int_t * vGates, Vec_Wec_t * vFanins, Vec_Int_t * vMap ) +void Sfm_DecInsert( Abc_Ntk_t * pNtk, int iNode, int Limit, Vec_Int_t * vTypes, Vec_Int_t * vGates, Vec_Wec_t * vFanins, Vec_Int_t * vMap, Vec_Ptr_t * vGateHandles ) { Abc_Obj_t * pTarget = Abc_NtkObj( pNtk, iNode ); - Vec_Int_t * vLevel; Abc_Obj_t * pObjNew = NULL; int i, k, iObj, Gate; + // assuming that new gates are appended at the end assert( Limit < Vec_IntSize(vTypes) ); + // introduce new gates Vec_IntForEachEntryStart( vGates, Gate, i, Limit ) { - assert( Gate >= 0 && Gate <= 7 ); - vLevel = Vec_WecEntry( vFanins, i ); - if ( Gate == 0 ) - pObjNew = Abc_NtkCreateNodeConst0( pNtk ); - else if ( Gate == 1 ) - pObjNew = Abc_NtkCreateNodeConst1( pNtk ); - else if ( Gate == 2 ) - pObjNew = Abc_NtkCreateNodeBuf( pNtk, Abc_NtkObj(pNtk, Vec_IntEntry(vMap, Vec_IntEntry(vLevel,0))) ); - else if ( Gate == 3 ) - pObjNew = Abc_NtkCreateNodeInv( pNtk, Abc_NtkObj(pNtk, Vec_IntEntry(vMap, Vec_IntEntry(vLevel,0))) ); - else // if ( Gate >= 4 ) - { - pObjNew = Abc_NtkCreateNode( pNtk ); - Vec_IntForEachEntry( vLevel, iObj, k ) - Abc_ObjAddFanin( pObjNew, Abc_NtkObj(pNtk, Vec_IntEntry(vMap, iObj)) ); - pObjNew->pData = NULL; // SELECTION FUNCTION - } - // transfer the fanout - Abc_ObjTransferFanout( pTarget, pObjNew ); - assert( Abc_ObjFanoutNum(pTarget) == 0 ); - Abc_NtkDeleteObj_rec( pTarget, 1 ); + Vec_Int_t * vLevel = Vec_WecEntry( vFanins, i ); + pObjNew = Abc_NtkCreateNode( pNtk ); + Vec_IntForEachEntry( vLevel, iObj, k ) + Abc_ObjAddFanin( pObjNew, Abc_NtkObj(pNtk, Vec_IntEntry(vMap, iObj)) ); + pObjNew->pData = Vec_PtrEntry( vGateHandles, Gate ); } + // transfer the fanout + Abc_ObjTransferFanout( pTarget, pObjNew ); + assert( Abc_ObjFanoutNum(pTarget) == 0 ); + Abc_NtkDeleteObj_rec( pTarget, 1 ); } -void Sfm_DecTestBench( Abc_Ntk_t * pNtk ) +void Sfm_DecTestBench( Abc_Ntk_t * pNtk, int iNode ) { - Vec_Int_t * vMap, * vTemp; - Abc_Obj_t * pObj; int i, Limit; + extern void Sfm_LibPreprocess( Mio_Library_t * pLib, Vec_Int_t * vGateSizes, Vec_Wrd_t * vGateFuncs, Vec_Wec_t * vGateCnfs, Vec_Ptr_t * vGateHands ); + Mio_Library_t * pLib = (Mio_Library_t *)pNtk->pManFunc; Sfm_Dec_t * p = Sfm_DecStart(); - Sfm_DecCreateAigLibrary( p ); - assert( Abc_NtkIsSopLogic(pNtk) ); - assert( Abc_NtkGetFaninMax(pNtk) <= 2 ); - vMap = Vec_IntAlloc( Abc_NtkObjNumMax(pNtk) ); // Sfm->Ntk - vTemp = Vec_IntAlloc( Abc_NtkObjNumMax(pNtk) ); - Abc_NtkForEachNode( pNtk, pObj, i ) + Vec_Int_t * vMap = Vec_IntAlloc( Abc_NtkObjNumMax(pNtk) ); // Sfm->Ntk + Abc_Obj_t * pObj; + int i, Limit; + // enter library + assert( Abc_NtkIsMappedLogic(pNtk) ); + Sfm_LibPreprocess( pLib, &p->vGateSizes, &p->vGateFuncs, &p->vGateCnfs, &p->vGateHands ); + p->GateConst0 = Mio_GateReadValue( Mio_LibraryReadConst0(pLib) ); + p->GateConst1 = Mio_GateReadValue( Mio_LibraryReadConst1(pLib) ); + p->GateBuffer = Mio_GateReadValue( Mio_LibraryReadBuf(pLib) ); + p->GateInvert = Mio_GateReadValue( Mio_LibraryReadInv(pLib) ); + // iterate over nodes +// Abc_NtkForEachNode( pNtk, pObj, i ) + for ( ; pObj = Abc_NtkObj(pNtk, iNode); ) { - p->iTarget = Sfm_DecExtract( pNtk, i, &p->vObjTypes, &p->vObjGates, &p->vObjFanins, vMap, vTemp ); + p->iTarget = Sfm_DecExtract( pNtk, pObj, &p->vObjTypes, &p->vObjGates, &p->vObjFanins, vMap, &p->vTemp ); Limit = Vec_IntSize( &p->vObjTypes ); if ( !Sfm_DecPrepareSolver( p ) ) continue; if ( !Sfm_DecPeformDec( p ) ) continue; - Sfm_DecInsert( pNtk, p->iTarget, Limit, &p->vObjTypes, &p->vObjGates, &p->vObjFanins, vMap ); +// Sfm_DecInsert( pNtk, p->iTarget, Limit, &p->vObjTypes, &p->vObjGates, &p->vObjFanins, vMap, vGateHandles ); + + break; } Vec_IntFree( vMap ); - Vec_IntFree( vTemp ); Sfm_DecStop( p ); } diff --git a/src/opt/sfm/sfmLib.c b/src/opt/sfm/sfmLib.c new file mode 100644 index 00000000..fefa21bb --- /dev/null +++ b/src/opt/sfm/sfmLib.c @@ -0,0 +1,102 @@ +/**CFile**************************************************************** + + FileName [sfmLib.c] + + SystemName [ABC: Logic synthesis and verification system.] + + PackageName [SAT-based optimization using internal don't-cares.] + + Synopsis [Preprocessing genlib library.] + + Author [Alan Mishchenko] + + Affiliation [UC Berkeley] + + Date [Ver. 1.0. Started - June 20, 2005.] + + Revision [$Id: sfmLib.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $] + +***********************************************************************/ + +#include "sfmInt.h" +#include "misc/st/st.h" +#include "map/mio/mio.h" + +ABC_NAMESPACE_IMPL_START + + +//////////////////////////////////////////////////////////////////////// +/// DECLARATIONS /// +//////////////////////////////////////////////////////////////////////// + +//////////////////////////////////////////////////////////////////////// +/// FUNCTION DEFINITIONS /// +//////////////////////////////////////////////////////////////////////// + +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Sfm_DecCreateCnf( Vec_Int_t * vGateSizes, Vec_Wrd_t * vGateFuncs, Vec_Wec_t * vGateCnfs ) +{ + Vec_Str_t * vCnf, * vCnfBase; + Vec_Int_t * vCover; + word uTruth; + int i, nCubes; + vCnf = Vec_StrAlloc( 100 ); + vCover = Vec_IntAlloc( 100 ); + Vec_WrdForEachEntry( vGateFuncs, uTruth, i ) + { + nCubes = Sfm_TruthToCnf( uTruth, Vec_IntEntry(vGateSizes, i), vCover, vCnf ); + vCnfBase = (Vec_Str_t *)Vec_WecEntry( vGateCnfs, i ); + Vec_StrGrow( vCnfBase, Vec_StrSize(vCnf) ); + memcpy( Vec_StrArray(vCnfBase), Vec_StrArray(vCnf), Vec_StrSize(vCnf) ); + vCnfBase->nSize = Vec_StrSize(vCnf); + } + Vec_IntFree( vCover ); + Vec_StrFree( vCnf ); +} + +/**Function************************************************************* + + Synopsis [Preprocess the library.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Sfm_LibPreprocess( Mio_Library_t * pLib, Vec_Int_t * vGateSizes, Vec_Wrd_t * vGateFuncs, Vec_Wec_t * vGateCnfs, Vec_Ptr_t * vGateHands ) +{ + Mio_Gate_t * pGate; + int nGates = Mio_LibraryReadGateNum(pLib); + Vec_IntGrow( vGateSizes, nGates ); + Vec_WrdGrow( vGateFuncs, nGates ); + Vec_WecInit( vGateCnfs, nGates ); + Vec_PtrGrow( vGateHands, nGates ); + Mio_LibraryForEachGate( pLib, pGate ) + { + Vec_IntPush( vGateSizes, Mio_GateReadPinNum(pGate) ); + Vec_WrdPush( vGateFuncs, Mio_GateReadTruth(pGate) ); + Mio_GateSetValue( pGate, Vec_PtrSize(vGateHands) ); + Vec_PtrPush( vGateHands, pGate ); + } + Sfm_DecCreateCnf( vGateSizes, vGateFuncs, vGateCnfs ); +} + +//////////////////////////////////////////////////////////////////////// +/// END OF FILE /// +//////////////////////////////////////////////////////////////////////// + + +ABC_NAMESPACE_IMPL_END + |