diff options
| -rw-r--r-- | abclib.dsp | 4 | ||||
| -rw-r--r-- | src/opt/sfm/module.make | 1 | ||||
| -rw-r--r-- | src/opt/sfm/sfmDec.c | 549 |
3 files changed, 554 insertions, 0 deletions
@@ -2519,6 +2519,10 @@ SOURCE=.\src\opt\sfm\sfmCore.c # End Source File # Begin Source File +SOURCE=.\src\opt\sfm\sfmDec.c +# End Source File +# Begin Source File + SOURCE=.\src\opt\sfm\sfmInt.h # End Source File # Begin Source File diff --git a/src/opt/sfm/module.make b/src/opt/sfm/module.make index b78355e1..c2401559 100644 --- a/src/opt/sfm/module.make +++ b/src/opt/sfm/module.make @@ -1,5 +1,6 @@ SRC += src/opt/sfm/sfmCnf.c \ src/opt/sfm/sfmCore.c \ + src/opt/sfm/sfmDec.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 new file mode 100644 index 00000000..c93c2be5 --- /dev/null +++ b/src/opt/sfm/sfmDec.c @@ -0,0 +1,549 @@ +/**CFile**************************************************************** + + FileName [sfmDec.c] + + SystemName [ABC: Logic synthesis and verification system.] + + PackageName [SAT-based optimization using internal don't-cares.] + + Synopsis [SAT-based decomposition.] + + Author [Alan Mishchenko] + + Affiliation [UC Berkeley] + + Date [Ver. 1.0. Started - June 20, 2005.] + + Revision [$Id: sfmDec.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $] + +***********************************************************************/ + +#include "sfmInt.h" +#include "bool/kit/kit.h" +#include "base/abc/abc.h" + +ABC_NAMESPACE_IMPL_START + + +//////////////////////////////////////////////////////////////////////// +/// DECLARATIONS /// +//////////////////////////////////////////////////////////////////////// + +#define SFM_FAN_MAX 6 + +typedef struct Sfm_Dec_t_ Sfm_Dec_t; +struct Sfm_Dec_t_ +{ + // parameters + Sfm_Par_t * pPars; // parameters + // library + Vec_Int_t vGateSizes; // fanin counts + Vec_Wrd_t vGateFuncs; // gate truth tables + Vec_Wec_t vGateCnfs; // gate CNFs + // objects + int iTarget; // target node + Vec_Int_t vObjTypes; // PI (1), PO (2) + Vec_Int_t vObjGates; // functionality + Vec_Wec_t vObjFanins; // fanin IDs + // solver + 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 vImpls[2]; // onset/offset implications + Vec_Wrd_t vSets[2]; // onset/offset patterns + int nPats[3]; + // temporary + Vec_Int_t vTemp; + Vec_Int_t vTemp2; + // statistics + abctime timeWin; + abctime timeCnf; + abctime timeSat; +}; + +//////////////////////////////////////////////////////////////////////// +/// FUNCTION DEFINITIONS /// +//////////////////////////////////////////////////////////////////////// + +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Sfm_Dec_t * Sfm_DecStart() +{ + Sfm_Dec_t * p = ABC_CALLOC( Sfm_Dec_t, 1 ); + p->pSat = sat_solver_new(); + return p; +} +void Sfm_DecStop( Sfm_Dec_t * p ) +{ + // library + Vec_IntErase( &p->vGateSizes ); + Vec_WrdErase( &p->vGateFuncs ); + Vec_WecErase( &p->vGateCnfs ); + // objects + Vec_IntErase( &p->vObjTypes ); + Vec_IntErase( &p->vObjGates ); + Vec_WecErase( &p->vObjFanins ); + // solver + sat_solver_delete( p->pSat ); + Vec_WecErase( &p->vClauses ); + Vec_IntErase( &p->vPols[0] ); + Vec_IntErase( &p->vPols[1] ); + Vec_IntErase( &p->vImpls[0] ); + Vec_IntErase( &p->vImpls[1] ); + Vec_WrdErase( &p->vSets[0] ); + Vec_WrdErase( &p->vSets[1] ); + // temporary + Vec_IntErase( &p->vTemp ); + Vec_IntErase( &p->vTemp2 ); + ABC_FREE( p ); +} + +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + 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 * 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) ); + // collect variables of root nodes + Vec_IntClear( &p->vTemp ); + Vec_IntForEachEntryStart( &p->vObjTypes, Type, i, p->iTarget ) + if ( Type == 2 ) + Vec_IntPush( &p->vTemp, i ); + assert( Vec_IntSize(&p->vTemp) > 0 ); + // create SAT solver + sat_solver_restart( p->pSat ); + sat_solver_setnvars( p->pSat, nSatVars + Vec_IntSize(&p->vTemp) ); + // add CNF clauses for the TFI + Vec_IntForEachEntryStop( &p->vObjTypes, Type, i, p->iTarget + 1 ) + { + if ( Type == 1 ) + continue; + // generate CNF + Gate = Vec_IntEntry( &p->vObjGates, i ); + vLevel = Vec_WecEntry( &p->vObjFanins, i ); + Sfm_TranslateCnf( &p->vClauses, (Vec_Str_t *)Vec_WecEntry(&p->vGateCnfs, Gate), vLevel, -1 ); + // add clauses + Vec_WecForEachLevel( &p->vClauses, vClause, k ) + { + if ( Vec_IntSize(vClause) == 0 ) + break; + RetValue = sat_solver_addclause( p->pSat, Vec_IntArray(vClause), Vec_IntArray(vClause) + Vec_IntSize(vClause) ); + if ( RetValue == 0 ) + return 0; + } + } + // add CNF clauses for the TFO + Vec_IntForEachEntryStart( &p->vObjTypes, Type, i, p->iTarget + 1 ) + { + 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) ); + // add clauses + Vec_WecForEachLevel( &p->vClauses, vClause, k ) + { + if ( Vec_IntSize(vClause) == 0 ) + break; + RetValue = sat_solver_addclause( p->pSat, Vec_IntArray(vClause), Vec_IntArray(vClause) + Vec_IntSize(vClause) ); + if ( RetValue == 0 ) + return 0; + } + } + if ( p->iTarget + 1 < Vec_IntSize(&p->vObjTypes) ) + { + // create XOR clauses for the roots + Vec_IntForEachEntry( &p->vTemp, 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) ); + } + // make OR clause for the last nRoots variables + RetValue = sat_solver_addclause( p->pSat, Vec_IntArray(&p->vTemp), Vec_IntLimit(&p->vTemp) ); + if ( RetValue == 0 ) + return 0; + assert( nSatVars == sat_solver_nvars(p->pSat) ); + } + else assert( Vec_IntSize(&p->vTemp) == 1 ); + // finalize + RetValue = sat_solver_simplify( p->pSat ); + p->timeCnf += Abc_Clock() - clk; + return 1; +} + +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Sfm_DecPeformDec( Sfm_Dec_t * p ) +{ + int fVerbose = 1; + int nBTLimit = 0; + abctime clk = Abc_Clock(); + int i, k, c, status, Lits[2]; + // check stuck-at-0/1 (on/off-set empty) + p->nPats[0] = p->nPats[1] = 0; + for ( c = 0; c < 2; c++ ) + { + Lits[0] = Abc_Var2Lit( p->iTarget, c ); + status = sat_solver_solve( p->pSat, Lits, Lits + 1, nBTLimit, 0, 0, 0 ); + if ( status == l_Undef ) + return 0; + if ( status == l_False ) + { + Vec_IntPush( &p->vObjTypes, 0 ); + Vec_IntPush( &p->vObjGates, c ); + Vec_WecPushLevel( &p->vObjFanins ); + return 1; + } + assert( status == l_True ); + // record this status + 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]++; + } + // proceed checking divisors based on their values + for ( c = 0; c < 2; c++ ) + { + Lits[0] = Abc_Var2Lit( p->iTarget, c ); + for ( i = 0; i < p->iTarget; i++ ) + { + if ( Vec_WrdEntry(&p->vSets[c], i) ) // diff value is possible + continue; + Lits[1] = Abc_Var2Lit( i, Vec_IntEntry(&p->vPols[c], i) ); + 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 ); + continue; + } + assert( status == l_True ); + // 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]); + 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) ); + printf( "\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++ ) + printf( "%d", (int)((Vec_WrdEntry(&p->vSets[c], i) >> k) & 1) ); + printf( "\n" ); + } + } + p->timeSat += Abc_Clock() - clk; + return 1; +} + +/**Function************************************************************* + + Synopsis [Testbench for the new AIG minimization.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Abc_NtkDfsReverseOne_rec( Abc_Obj_t * pNode, Vec_Int_t * vNodes ) +{ + Abc_Obj_t * pFanout; int i; + if ( Abc_NodeIsTravIdCurrent( pNode ) ) + return; + Abc_NodeSetTravIdCurrent( pNode ); + if ( Abc_ObjIsCo(pNode) ) + { + Vec_IntPush( vNodes, Abc_ObjId(pNode) ); + return; + } + assert( Abc_ObjIsNode( pNode ) ); + Abc_ObjForEachFanout( pNode, pFanout, i ) + Abc_NtkDfsReverseOne_rec( pFanout, vNodes ); + Vec_IntPush( vNodes, Abc_ObjId(pNode) ); +} +void Abc_NtkDfsOne_rec( Abc_Obj_t * pNode, Vec_Int_t * vMap, Vec_Int_t * vTypes ) +{ + Abc_Obj_t * pFanin; int i; + if ( Abc_NodeIsTravIdCurrent( pNode ) ) + return; + Abc_NodeSetTravIdCurrent( pNode ); + if ( Abc_ObjIsCi(pNode) ) + { + pNode->iTemp = Vec_IntSize(vMap); + Vec_IntPush( vMap, 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) ); + 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 ) +{ + Abc_Obj_t * pNode = Abc_NtkObj( pNtk, iNode ); + Vec_Int_t * vLevel; + int i, iObj, iTarget; + assert( Abc_ObjIsNode(pNode) ); + // collect transitive fanout + Vec_IntClear( vTemp ); + Abc_NtkIncrementTravId( pNtk ); + Abc_NtkDfsReverseOne_rec( pNode, vTemp ); + // collect transitive fanin + Vec_IntClear( vMap ); + Vec_IntClear( vTypes ); + Abc_NtkDfsOne_rec( pNode, vMap, vTypes ); + Vec_IntPop( vMap ); + Vec_IntPop( vTypes ); + assert( Vec_IntSize(vMap) == Vec_IntSize(vTypes) ); + // remember target node + iTarget = Vec_IntSize( vMap ); + // add transitive fanout + Vec_IntForEachEntryReverse( vTemp, iObj, i ) + { + pNode = Abc_NtkObj( pNtk, iObj ); + if ( Abc_ObjIsCo(pNode) ) + { + assert( Vec_IntEntry(vTypes, Abc_ObjFanin0(pNode)->iTemp) == 0 ); + Vec_IntWriteEntry( vTypes, Abc_ObjFanin0(pNode)->iTemp, 2 ); + continue; + } + pNode->iTemp = Vec_IntSize(vMap); + Vec_IntPush( vMap, Abc_ObjId(pNode) ); + Vec_IntPush( vTypes, 0 ); + } + assert( Vec_IntSize(vMap) == Vec_IntSize(vTypes) ); + // create gates and fanins + Vec_IntClear( vGates ); + Vec_WecClear( vFanins ); + Vec_IntForEachEntry( vMap, iObj, i ) + { + vLevel = Vec_WecPushLevel( vFanins ); + pNode = Abc_NtkObj( pNtk, iObj ); + if ( Abc_ObjIsCi(pNode) ) + { + 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 ); + } + 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 ) +{ + Abc_Obj_t * pTarget = Abc_NtkObj( pNtk, iNode ); + Vec_Int_t * vLevel; + Abc_Obj_t * pObjNew = NULL; + int i, k, iObj, Gate; + assert( Limit < Vec_IntSize(vTypes) ); + 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 ); + } +} +void Sfm_DecTestBench( Abc_Ntk_t * pNtk ) +{ + Vec_Int_t * vMap, * vTemp; + Abc_Obj_t * pObj; int i, Limit; + 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 ) + { + p->iTarget = Sfm_DecExtract( pNtk, i, &p->vObjTypes, &p->vObjGates, &p->vObjFanins, vMap, 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 ); + } + Vec_IntFree( vMap ); + Vec_IntFree( vTemp ); + Sfm_DecStop( p ); +} + +//////////////////////////////////////////////////////////////////////// +/// END OF FILE /// +//////////////////////////////////////////////////////////////////////// + + +ABC_NAMESPACE_IMPL_END + |