luke
/
abc
mirror of https://github.com/YosysHQ/abc.git
1
0
Fork 0
Code Issues Packages Projects Releases Wiki Activity

Experiments with functional matching.

This commit is contained in:
Alan Mishchenko 2015-10-05 16:10:57 -07:00
parent a1e9f668a8
commit 72f4dfff1b
5 changed files with 282 additions and 195 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

4
abclib.dsp
View File

@ -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

12
src/base/abci/abc.c
View File

@ -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:

1
src/opt/sfm/module.make
View File

@ -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

358
src/opt/sfm/sfmDec.c
View File

@ -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] );
@ -107,97 +117,6 @@ void Sfm_DecStop( Sfm_Dec_t * p )
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 []
@ -212,29 +131,35 @@ void Vec_IntLift( Vec_Int_t * p, int Amount )
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 );
}

102
src/opt/sfm/sfmLib.c Normal file
View File

@ -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