Skip to content

A
abc
Commit 20c46b5a by Alan Mishchenko
Options

Experiments with precomputation and matching.

parent d25473b3
Showing with 623 additions and 79 deletions
src/base/abci/abc.c
......@@ -5160,7 +5160,7 @@ int Abc_CommandMfs3( Abc_Frame_t * pAbc, int argc, char ** argv )
// set defaults
Sfm_ParSetDefault3( pPars );
Extra_UtilGetoptReset();
while ( ( c = Extra_UtilGetopt( argc, argv, "OIFXMLCNdavwh" ) ) != EOF )
while ( ( c = Extra_UtilGetopt( argc, argv, "OIFXMLCNdaovwh" ) ) != EOF )
{
switch ( c )
{
......@@ -5258,6 +5258,9 @@ int Abc_CommandMfs3( Abc_Frame_t * pAbc, int argc, char ** argv )
case 'a':
pPars->fArea ^= 1;
break;
case 'o':
pPars->fRrOnly ^= 1;
break;
case 'v':
pPars->fVerbose ^= 1;
break;
......@@ -5285,7 +5288,7 @@ int Abc_CommandMfs3( Abc_Frame_t * pAbc, int argc, char ** argv )
return 0;
usage:
Abc_Print( -2, "usage: mfs3 [-OIFXMLCN <num>] [-avwh]\n" );
Abc_Print( -2, "usage: mfs3 [-OIFXMLCN <num>] [-aovwh]\n" );
Abc_Print( -2, "\t performs don't-care-based optimization of mapped networks\n" );
Abc_Print( -2, "\t-O <num> : the number of levels in the TFO cone (0 <= num) [default = %d]\n", pPars->nTfoLevMax );
Abc_Print( -2, "\t-I <num> : the number of levels in the TFI cone (1 <= num) [default = %d]\n", pPars->nTfiLevMax );
......@@ -5296,6 +5299,7 @@ usage:
Abc_Print( -2, "\t-C <num> : the max number of conflicts in one SAT run (0 = no limit) [default = %d]\n", pPars->nBTLimit );
Abc_Print( -2, "\t-N <num> : the max number of nodes to try (0 = all) [default = %d]\n", pPars->nNodesMax );
Abc_Print( -2, "\t-a : toggle minimizing area or area+edges [default = %s]\n", pPars->fArea? "area": "area+edges" );
Abc_Print( -2, "\t-o : toggle using old implementation for comparison [default = %s]\n", pPars->fRrOnly? "yes": "no" );
Abc_Print( -2, "\t-v : toggle printing optimization summary [default = %s]\n", pPars->fVerbose? "yes": "no" );
Abc_Print( -2, "\t-w : toggle printing detailed stats for each node [default = %s]\n", pPars->fVeryVerbose? "yes": "no" );
Abc_Print( -2, "\t-h : print the command usage\n");
src/map/mio/mio.c
......@@ -443,7 +443,7 @@ int Mio_CommandWriteGenlib( Abc_Frame_t * pAbc, int argc, char **argv )
printf( "Error! Cannot open file \"%s\" for writing the library.\n", pFileName );
return 1;
}
Mio_WriteLibrary( pFile, (Mio_Library_t *)Abc_FrameReadLibGen(), 0 );
Mio_WriteLibrary( pFile, (Mio_Library_t *)Abc_FrameReadLibGen(), 0, 0 );
fclose( pFile );
printf( "The current genlib library is written into file \"%s\".\n", pFileName );
return 0;
......@@ -472,7 +472,8 @@ int Mio_CommandPrintGenlib( Abc_Frame_t * pAbc, int argc, char **argv )
{
FILE * pOut, * pErr;
Abc_Ntk_t * pNet;
int fVerbose;
int fShort = 0;
int fVerbose = 0;
int c;
pNet = Abc_FrameReadNtk(pAbc);
......@@ -480,12 +481,14 @@ int Mio_CommandPrintGenlib( Abc_Frame_t * pAbc, int argc, char **argv )
pErr = Abc_FrameReadErr(pAbc);
// set the defaults
fVerbose = 1;
Extra_UtilGetoptReset();
while ( (c = Extra_UtilGetopt(argc, argv, "vh")) != EOF )
while ( (c = Extra_UtilGetopt(argc, argv, "svh")) != EOF )
{
switch (c)
{
case 's':
fShort ^= 1;
break;
case 'v':
fVerbose ^= 1;
break;
......@@ -501,12 +504,13 @@ int Mio_CommandPrintGenlib( Abc_Frame_t * pAbc, int argc, char **argv )
printf( "Library is not available.\n" );
return 1;
}
Mio_WriteLibrary( stdout, (Mio_Library_t *)Abc_FrameReadLibGen(), 0 );
Mio_WriteLibrary( stdout, (Mio_Library_t *)Abc_FrameReadLibGen(), 0, fShort );
return 0;
usage:
fprintf( pErr, "\nusage: print_genlib [-vh]\n");
fprintf( pErr, "\nusage: print_genlib [-svh]\n");
fprintf( pErr, "\t print the current genlib library\n" );
fprintf( pErr, "\t-s : toggles writing short form [default = %s]\n", fShort? "yes" : "no" );
fprintf( pErr, "\t-v : toggles enabling of verbose output [default = %s]\n", fVerbose? "yes" : "no" );
fprintf( pErr, "\t-h : print the command usage\n");
return 1;
......
src/map/mio/mio.h
......@@ -58,6 +58,7 @@ typedef struct Mio_Cell2_t_ Mio_Cell2_t;
struct Mio_Cell2_t_
{
char * pName; // name
Vec_Int_t * vExpr; // expression
unsigned Id : 28; // gate ID
unsigned nFanins : 4; // gate fanins
word Area; // area
......@@ -177,7 +178,7 @@ extern void Mio_LibraryDelete( Mio_Library_t * pLib );
extern void Mio_GateDelete( Mio_Gate_t * pGate );
extern void Mio_PinDelete( Mio_Pin_t * pPin );
extern Mio_Pin_t * Mio_PinDup( Mio_Pin_t * pPin );
extern void Mio_WriteLibrary( FILE * pFile, Mio_Library_t * pLib, int fPrintSops );
extern void Mio_WriteLibrary( FILE * pFile, Mio_Library_t * pLib, int fPrintSops, int fShort );
extern Mio_Gate_t ** Mio_CollectRoots( Mio_Library_t * pLib, int nInputs, float tDelay, int fSkipInv, int * pnGates, int fVerbose );
extern Mio_Cell_t * Mio_CollectRootsNew( Mio_Library_t * pLib, int nInputs, int * pnGates, int fVerbose );
extern Mio_Cell_t * Mio_CollectRootsNewDefault( int nInputs, int * pnGates, int fVerbose );
......
src/map/mio/mioRead.c
......@@ -329,6 +329,16 @@ int Mio_LibraryReadInternal( Mio_Library_t * pLib, char * pBuffer, int fExtended
SeeAlso []
***********************************************************************/
char * Mio_LibraryCleanStr( char * p )
{
int i, k;
char * pRes = Abc_UtilStrsav( p );
for ( i = k = 0; pRes[i]; i++ )
if ( pRes[i] != ' ' && pRes[i] != '\t' && pRes[i] != '\r' && pRes[i] != '\n' )
pRes[k++] = pRes[i];
pRes[k] = 0;
return pRes;
}
Mio_Gate_t * Mio_LibraryReadGate( char ** ppToken, int fExtendedFormat )
{
Mio_Gate_t * pGate;
......@@ -354,7 +364,7 @@ Mio_Gate_t * Mio_LibraryReadGate( char ** ppToken, int fExtendedFormat )
// then rest of the expression
pToken = strtok( NULL, ";" );
pGate->pForm = chomp( pToken );
pGate->pForm = Mio_LibraryCleanStr( pToken );
// read the pin info
// start the linked list of pins
......
src/map/mio/mioUtils.c
......@@ -200,10 +200,10 @@ void Mio_WritePin( FILE * pFile, Mio_Pin_t * pPin, int NameLen, int fAllPins )
fprintf( pFile, "%7s ", pPhaseNames[pPin->Phase] );
fprintf( pFile, "%3d ", (int)pPin->dLoadInput );
fprintf( pFile, "%3d ", (int)pPin->dLoadMax );
fprintf( pFile, "%6.2f ", pPin->dDelayBlockRise );
fprintf( pFile, "%6.2f ", pPin->dDelayFanoutRise );
fprintf( pFile, "%6.2f ", pPin->dDelayBlockFall );
fprintf( pFile, "%6.2f", pPin->dDelayFanoutFall );
fprintf( pFile, "%8.2f ", pPin->dDelayBlockRise );
fprintf( pFile, "%8.2f ", pPin->dDelayFanoutRise );
fprintf( pFile, "%8.2f ", pPin->dDelayBlockFall );
fprintf( pFile, "%8.2f", pPin->dDelayFanoutFall );
}
/**Function*************************************************************
......@@ -225,7 +225,7 @@ void Mio_WriteGate( FILE * pFile, Mio_Gate_t * pGate, int GateLen, int NameLen,
sprintf( Buffer, "%s=%s;", pGate->pOutName, pGate->pForm );
fprintf( pFile, "GATE %-*s ", GateLen, pGate->pName );
fprintf( pFile, "%8.2f ", pGate->dArea );
fprintf( pFile, "%-*s ", Abc_MinInt(NameLen+FormLen+2, 30), Buffer );
fprintf( pFile, "%-*s ", Abc_MinInt(NameLen+FormLen+2, 60), Buffer );
// print the pins
if ( fPrintSops )
fprintf( pFile, "%s", pGate->pSop? pGate->pSop : "unspecified\n" );
......@@ -248,12 +248,12 @@ void Mio_WriteGate( FILE * pFile, Mio_Gate_t * pGate, int GateLen, int NameLen,
SeeAlso []
***********************************************************************/
void Mio_WriteLibrary( FILE * pFile, Mio_Library_t * pLib, int fPrintSops )
void Mio_WriteLibrary( FILE * pFile, Mio_Library_t * pLib, int fPrintSops, int fShort )
{
Mio_Gate_t * pGate;
Mio_Pin_t * pPin;
int i, GateLen = 0, NameLen = 0, FormLen = 0;
int fAllPins = Mio_CheckGates( pLib );
int fAllPins = fShort || Mio_CheckGates( pLib );
Mio_LibraryForEachGate( pLib, pGate )
{
GateLen = Abc_MaxInt( GateLen, strlen(pGate->pName) );
......@@ -631,6 +631,7 @@ static inline void Mio_CollectCopy2( Mio_Cell2_t * pCell, Mio_Gate_t * pGate )
{
Mio_Pin_t * pPin; int k;
pCell->pName = pGate->pName;
pCell->vExpr = pGate->vExpr;
pCell->uTruth = pGate->uTruth;
pCell->Area = (word)(MIO_NUM * pGate->dArea);
pCell->nFanins = pGate->nInputs;
......
src/opt/sfm/sfmDec.c
......@@ -22,6 +22,8 @@
#include "misc/st/st.h"
#include "map/mio/mio.h"
#include "base/abc/abc.h"
#include "misc/util/utilTruth.h"
#include "opt/dau/dau.h"
ABC_NAMESPACE_IMPL_START
......@@ -30,13 +32,12 @@ ABC_NAMESPACE_IMPL_START
/// DECLARATIONS ///
////////////////////////////////////////////////////////////////////////
#define SFM_FAN_MAX 6
typedef struct Sfm_Dec_t_ Sfm_Dec_t;
struct Sfm_Dec_t_
{
// parameters
// external
Sfm_Par_t * pPars; // parameters
Sfm_Lib_t * pLib; // library
// library
Vec_Int_t vGateSizes; // fanin counts
Vec_Wrd_t vGateFuncs; // gate truth tables
......@@ -52,6 +53,7 @@ struct Sfm_Dec_t_
int nDivs; // the number of divisors
int nMffc; // the number of divisors
int iTarget; // target node
int fUseLast; // internal switch
Vec_Int_t vObjRoots; // roots of the window
Vec_Int_t vObjGates; // functionality
Vec_Wec_t vObjFanins; // fanin IDs
......@@ -61,10 +63,11 @@ struct Sfm_Dec_t_
sat_solver * pSat; // reusable solver
Vec_Wec_t vClauses; // CNF clauses for the node
Vec_Int_t vImpls[2]; // onset/offset implications
Vec_Int_t vCounts[2]; // onset/offset counters
Vec_Wrd_t vSets[2]; // onset/offset patterns
int nPats[2]; // CEX count
word uMask[2]; // mask count
word TtElems[SFM_SUPP_MAX][SFM_WORD_MAX];
word * pTtElems[SFM_SUPP_MAX];
// temporary
Vec_Int_t vTemp;
Vec_Int_t vTemp2;
......@@ -138,14 +141,21 @@ void Sfm_ParSetDefault3( Sfm_Par_t * pPars )
***********************************************************************/
Sfm_Dec_t * Sfm_DecStart( Sfm_Par_t * pPars )
{
Sfm_Dec_t * p = ABC_CALLOC( Sfm_Dec_t, 1 );
Sfm_Dec_t * p = ABC_CALLOC( Sfm_Dec_t, 1 ); int i;
p->pPars = pPars;
p->pSat = sat_solver_new();
p->timeStart = Abc_Clock();
for ( i = 0; i < SFM_SUPP_MAX; i++ )
p->pTtElems[i] = p->TtElems[i];
Abc_TtElemInit( p->pTtElems, SFM_SUPP_MAX );
p->pLib = Sfm_LibPrepare( pPars->nMffcMax + 1, 1, pPars->fVerbose );
if ( pPars->fVeryVerbose )
Sfm_LibPrint( p->pLib );
return p;
}
void Sfm_DecStop( Sfm_Dec_t * p )
{
Sfm_LibStop( p->pLib );
// library
Vec_IntErase( &p->vGateSizes );
Vec_WrdErase( &p->vGateFuncs );
......@@ -162,8 +172,6 @@ void Sfm_DecStop( Sfm_Dec_t * p )
Vec_WecErase( &p->vClauses );
Vec_IntErase( &p->vImpls[0] );
Vec_IntErase( &p->vImpls[1] );
Vec_IntErase( &p->vCounts[0] );
Vec_IntErase( &p->vCounts[1] );
Vec_WrdErase( &p->vSets[0] );
Vec_WrdErase( &p->vSets[1] );
// temporary
......@@ -270,25 +278,59 @@ int Sfm_DecPrepareSolver( Sfm_Dec_t * p )
SeeAlso []
***********************************************************************/
int Sfm_DecFindWeight( Sfm_Dec_t * p, int c, int iLit )
int Sfm_DecFindWeight( Sfm_Dec_t * p, int c, int iLit, word Mask )
{
int Value = Vec_IntEntry( &p->vCounts[!c], Abc_Lit2Var(iLit) );
return Abc_LitIsCompl(iLit) ? Value : p->nPats[!c] - Value;
int Value0 = Abc_TtCountOnes( Vec_WrdEntry(&p->vSets[!c], Abc_Lit2Var(iLit)) & Mask );
int Weight0 = Abc_LitIsCompl(iLit) ? Abc_TtCountOnes( p->uMask[!c] & Mask ) - Value0 : Value0;
return Weight0;
}
void Sfm_DecPrint( Sfm_Dec_t * p, word * Masks )
{
int c, i, k, Entry;
for ( c = 0; c < 2; c++ )
{
Vec_Int_t * vLevel = Vec_WecEntry( &p->vObjFanins, p->iTarget );
printf( "\n%s-SET of object %d (divs = %d) with gate \"%s\" and fanins: ",
c ? "OFF": "ON", p->iTarget, p->nDivs,
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_IntForEachEntry( &p->vImpls[c], Entry, i )
printf( "%s%d(%d) ", Abc_LitIsCompl(Entry)? "!":"", Abc_Lit2Var(Entry), Sfm_DecFindWeight(p, c, Entry, Masks ? Masks[!c] : ~(word)0) );
printf( "\n" );
printf( " " );
for ( i = 0; i <= p->iTarget; i++ )
printf( "%d", i / 10 );
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" );
}
printf( "\n" );
}
}
int Sfm_DecPeformDecOne( Sfm_Dec_t * p, int * pfConst )
{
int fVerbose = p->pPars->fVeryVerbose;
int nBTLimit = 0;
int i, k, c, Entry, status, Lits[3], RetValue;
int iLitBest = -1, iCBest = -1, WeightBest = -1, Weight;
int iLitBest = -1, iCBest = -1, WeightBest = ABC_INFINITY, Weight;
*pfConst = -1;
// check stuck-at-0/1 (on/off-set empty)
p->nPats[0] = p->nPats[1] = 0;
p->uMask[0] = p->uMask[1] = 0;
Vec_IntClear( &p->vImpls[0] );
Vec_IntClear( &p->vImpls[1] );
Vec_IntClear( &p->vCounts[0] );
Vec_IntClear( &p->vCounts[1] );
Vec_WrdClear( &p->vSets[0] );
Vec_WrdClear( &p->vSets[1] );
for ( c = 0; c < 2; c++ )
......@@ -309,11 +351,7 @@ int Sfm_DecPeformDecOne( Sfm_Dec_t * p, int * pfConst )
assert( status == l_True );
// record this status
for ( i = 0; i <= p->iTarget; i++ )
{
Entry = sat_solver_var_value(p->pSat, i);
Vec_IntPush( &p->vCounts[c], Entry );
Vec_WrdPush( &p->vSets[c], (word)Entry );
}
Vec_WrdPush( &p->vSets[c], (word)sat_solver_var_value(p->pSat, i) );
p->nPats[c]++;
p->uMask[c] = 1;
}
......@@ -342,10 +380,7 @@ int Sfm_DecPeformDecOne( Sfm_Dec_t * p, int * pfConst )
// record this status
for ( k = 0; k <= p->iTarget; k++ )
if ( sat_solver_var_value(p->pSat, k) )
{
Vec_IntAddToEntry( &p->vCounts[c], k, 1 );
*Vec_WrdEntryP(&p->vSets[c], k) |= ((word)1 << p->nPats[c]);
}
p->uMask[c] |= ((word)1 << p->nPats[c]++);
}
}
......@@ -354,8 +389,8 @@ int Sfm_DecPeformDecOne( Sfm_Dec_t * p, int * pfConst )
{
Vec_IntForEachEntry( &p->vImpls[c], Entry, i )
{
Weight = Sfm_DecFindWeight(p, c, Entry);
if ( WeightBest < Weight )
Weight = Sfm_DecFindWeight(p, c, Entry, (~(word)0));
if ( WeightBest > Weight )
{
WeightBest = Weight;
iLitBest = Entry;
......@@ -363,7 +398,7 @@ int Sfm_DecPeformDecOne( Sfm_Dec_t * p, int * pfConst )
}
}
}
if ( WeightBest == -1 )
if ( WeightBest == ABC_INFINITY )
{
p->nNoDecs++;
return -2;
......@@ -376,43 +411,11 @@ int Sfm_DecPeformDecOne( Sfm_Dec_t * p, int * pfConst )
if ( RetValue == 0 )
return -1;
// print the results
if ( !fVerbose )
return Abc_Var2Lit( iLitBest, iCBest );
printf( "\nBest literal (%d; %s%d) with weight %d.\n\n", iCBest, Abc_LitIsCompl(iLitBest)? "!":"", Abc_Lit2Var(iLitBest), WeightBest );
for ( c = 0; c < 2; c++ )
if ( fVerbose )
{
Vec_Int_t * vLevel = Vec_WecEntry( &p->vObjFanins, p->iTarget );
printf( "\n%s-SET of object %d (divs = %d) with gate \"%s\" and fanins: ",
c ? "OFF": "ON", p->iTarget, p->nDivs,
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_IntForEachEntry( &p->vImpls[c], Entry, i )
printf( "%s%d(%d) ", Abc_LitIsCompl(Entry)? "!":"", Abc_Lit2Var(Entry), Sfm_DecFindWeight(p, c, Entry) );
printf( "\n" );
printf( " " );
for ( i = 0; i <= p->iTarget; i++ )
printf( "%d", i / 10 );
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" );
}
printf( "\n" );
printf( "\nBest literal (%d; %s%d) with weight %d.\n\n", iCBest, Abc_LitIsCompl(iLitBest)? "!":"", Abc_Lit2Var(iLitBest), WeightBest );
Sfm_DecPrint( p, NULL );
}
return Abc_Var2Lit( iLitBest, iCBest );
}
......@@ -507,6 +510,216 @@ int Sfm_DecPeformDec( Sfm_Dec_t * p )
/**Function*************************************************************
Synopsis []
Description []
SideEffects []
SeeAlso []
***********************************************************************/
int Sfm_DecCombineDec( Sfm_Dec_t * p, word * pTruth0, word * pTruth1, int * pSupp0, int * pSupp1, int nSupp0, int nSupp1, word * pTruth, int * pSupp, int Var )
{
Vec_Int_t vVec0 = { 2*SFM_SUPP_MAX, nSupp0, pSupp0 };
Vec_Int_t vVec1 = { 2*SFM_SUPP_MAX, nSupp1, pSupp1 };
Vec_Int_t vVec = { 2*SFM_SUPP_MAX, 0, pSupp };
int nWords0 = Abc_TtWordNum(nSupp0);
int nWords1 = Abc_TtWordNum(nSupp1);
int nSupp, iSuppVar;
// check the case of equal cofactors
if ( nSupp0 == nSupp1 && !memcmp(pSupp0, pSupp1, sizeof(int)*nSupp0) && !memcmp(pTruth0, pTruth1, sizeof(word)*nWords0) )
{
memcpy( pSupp, pSupp0, sizeof(int)*nSupp0 );
memcpy( pTruth, pTruth0, sizeof(word)*nWords0 );
return nSupp0;
}
// merge support variables
Vec_IntTwoMerge2Int( &vVec0, &vVec1, &vVec );
Vec_IntPushOrder( &vVec, Var );
nSupp = Vec_IntSize( &vVec );
if ( nSupp > SFM_SUPP_MAX )
return -2;
// expand truth tables
Abc_TtStretch6( pTruth0, nSupp0, nSupp );
Abc_TtStretch6( pTruth1, nSupp1, nSupp );
Abc_TtExpand( pTruth0, nSupp, pSupp0, nSupp0, pSupp, nSupp );
Abc_TtExpand( pTruth1, nSupp, pSupp1, nSupp1, pSupp, nSupp );
// perform operation
iSuppVar = Vec_IntFind( &vVec, Var );
Abc_TtMux( pTruth, p->pTtElems[iSuppVar], pTruth1, pTruth0, Abc_TtWordNum(nSupp) );
return nSupp;
}
int Sfm_DecPeformDec_rec( Sfm_Dec_t * p, word * pTruth, int * pSupp, int * pAssump, int nAssump, word Masks[2], int fCofactor )
{
int nBTLimit = 0;
int fVerbose = p->pPars->fVeryVerbose;
int c, i, d, Var, WeightBest, status;
Vec_Int_t vAss = { SFM_SUPP_MAX, nAssump, pAssump };
// if ( nAssump > SFM_SUPP_MAX )
if ( nAssump > p->nMffc )
return -2;
// check constant
for ( c = 0; c < 2; c++ )
{
if ( p->uMask[c] & Masks[c] ) // there are some patterns
continue;
p->nSatCalls++;
pAssump[nAssump] = Abc_Var2Lit( p->iTarget, c );
status = sat_solver_solve( p->pSat, pAssump, pAssump + nAssump + 1, nBTLimit, 0, 0, 0 );
if ( status == l_Undef )
return -2;
if ( status == l_False )
{
pTruth[0] = c ? ~((word)0) : 0;
return 0;
}
assert( status == l_True );
if ( p->nPats[c] == 64 )
return -2;//continue;
for ( i = 0; i <= p->iTarget; i++ )
if ( sat_solver_var_value(p->pSat, i) )
*Vec_WrdEntryP(&p->vSets[c], i) |= ((word)1 << p->nPats[c]);
p->uMask[c] |= ((word)1 << p->nPats[c]++);
}
// check implications
Vec_IntClear( &p->vImpls[0] );
Vec_IntClear( &p->vImpls[1] );
for ( d = 0; d < p->nDivs; d++ )
{
int Impls[2] = {-1, -1};
for ( c = 0; c < 2; c++ )
{
word MaskAll = p->uMask[c] & Masks[c];
word MaskCur = Vec_WrdEntry(&p->vSets[c], d) & Masks[c];
assert( MaskAll );
if ( MaskCur != 0 && MaskCur != MaskAll ) // has both ones and zeros
continue;
pAssump[nAssump] = Abc_Var2Lit( p->iTarget, c );
pAssump[nAssump+1] = Abc_Var2Lit( d, MaskCur != 0 );
p->nSatCalls++;
status = sat_solver_solve( p->pSat, pAssump, pAssump + nAssump + 2, nBTLimit, 0, 0, 0 );
if ( status == l_Undef )
return -2;
if ( status == l_False )
{
Impls[c] = Abc_LitNot(pAssump[nAssump+1]);
Vec_IntPush( &p->vImpls[c], Abc_LitNot(pAssump[nAssump+1]) );
continue;
}
assert( status == l_True );
if ( p->nPats[c] == 64 )
return -2;//continue;
// record this status
for ( i = 0; i <= p->iTarget; i++ )
if ( sat_solver_var_value(p->pSat, i) )
*Vec_WrdEntryP(&p->vSets[c], i) |= ((word)1 << p->nPats[c]);
p->uMask[c] |= ((word)1 << p->nPats[c]++);
}
if ( Impls[0] == -1 || Impls[1] == -1 || Impls[0] == Impls[1] )
continue;
assert( Abc_Lit2Var(Impls[0]) == Abc_Lit2Var(Impls[1]) );
// found buffer/inverter
pTruth[0] = Abc_LitIsCompl(Impls[0]) ? ~p->pTtElems[0][0] : p->pTtElems[0][0];
pSupp[0] = Abc_Lit2Var(Impls[0]);
return 1;
}
// find the best cofactoring variable
Var = -1, WeightBest = ABC_INFINITY;
for ( c = 0; c < 2; c++ )
{
int iLit, Weight;
Vec_IntForEachEntry( &p->vImpls[c], iLit, i )
{
Weight = Sfm_DecFindWeight( p, c, iLit, Masks[!c] );
if ( WeightBest > Weight )
{
WeightBest = Weight;
Var = Abc_Lit2Var(iLit);
}
}
}
if ( Var == -1 && fCofactor )
{
if ( p->fUseLast )
Var = p->nDivs - 1;
else
Var = p->nDivs - 2;
fCofactor = 0;
}
// printf( "Assumptions: " );
// Vec_IntPrint( &vAss );
// Sfm_DecPrint( p, Masks );
//printf( "Best var %d with weight %d.\n", Var, WeightBest );
// cofactor the problem
if ( Var >= 0 )
{
word uTruth[2][SFM_WORD_MAX], MasksNext[2];
int Supp[2][2*SFM_SUPP_MAX], nSupp[2], nSuppAll;
//if ( Abc_TtCountOnes(
for ( i = 0; i < 2; i++ )
{
for ( c = 0; c < 2; c++ )
{
word MaskVar = Vec_WrdEntry(&p->vSets[c], Var);
MasksNext[c] = Masks[c] & (i ? MaskVar | ~p->uMask[c] : ~MaskVar);
}
pAssump[nAssump] = Abc_Var2Lit( Var, !i );
nSupp[i] = Sfm_DecPeformDec_rec( p, uTruth[i], Supp[i], pAssump, nAssump+1, MasksNext, fCofactor );
if ( nSupp[i] == -2 )
return -2;
}
// combine solutions
nSuppAll = Sfm_DecCombineDec( p, uTruth[0], uTruth[1], Supp[0], Supp[1], nSupp[0], nSupp[1], pTruth, pSupp, Var );
//if ( nSuppAll > p->nMffc )
// return -2;
return nSuppAll;
}
return -2;
}
int Sfm_DecPeformDec2Int( Sfm_Dec_t * p )
{
word uTruth[SFM_WORD_MAX];
word Masks[2] = { ~((word)0), ~((word)0) };
int pAssump[2*SFM_SUPP_MAX];
int pSupp[2*SFM_SUPP_MAX], nSupp;
p->nPats[0] = p->nPats[1] = 0;
p->uMask[0] = p->uMask[1] = 0;
Vec_WrdFill( &p->vSets[0], p->iTarget+1, 0 );
Vec_WrdFill( &p->vSets[1], p->iTarget+1, 0 );
nSupp = Sfm_DecPeformDec_rec( p, uTruth, pSupp, pAssump, 0, Masks, 1 );
//printf( "%d %d ", p->nPats[0], p->nPats[1] );
// printf( "Node %4d : ", p->iTarget );
// printf( "MFFC %2d ", p->nMffc );
if ( nSupp == -2 )
{
// printf( "NO DEC.\n" );
p->nNoDecs++;
return -2;
}
// transform truth table
Dau_DsdPrintFromTruth( uTruth, nSupp );
return -1;
}
int Sfm_DecPeformDec2( Sfm_Dec_t * p )
{
p->fUseLast = 1;
Sfm_DecPeformDec2Int( p );
// p->fUseLast = 0;
// Sfm_DecPeformDec2Int( p );
// printf( "\n" );
//Sfm_LibImplement( p->pLib, uTruth, pSupp, nSupp, &p->vObjGates, &p->vObjFanins );
return -1;
}
/**Function*************************************************************
Synopsis [Incremental level update.]
Description []
......@@ -790,8 +1003,8 @@ void Abc_NtkPerformMfs3( Abc_Ntk_t * pNtk, Sfm_Par_t * pPars )
Sfm_Dec_t * p = Sfm_DecStart( pPars );
Abc_Obj_t * pObj;
abctime clk;
int i, Limit, RetValue, Count = 0, nStop = Abc_NtkObjNumMax(pNtk);
//int iNode = 2341;//8;//70;
int i = 0, Limit, RetValue, Count = 0, nStop = Abc_NtkObjNumMax(pNtk);
int iNode = 70; //2341;//8;//70;
printf( "Running remapping with parameters: " );
printf( "TFO = %d. ", pPars->nTfoLevMax );
printf( "TFI = %d. ", pPars->nTfiLevMax );
......@@ -844,10 +1057,17 @@ p->timeCnf += Abc_Clock() - clk;
if ( !RetValue )
continue;
clk = Abc_Clock();
if ( pPars->fRrOnly )
RetValue = Sfm_DecPeformDec( p );
else
RetValue = Sfm_DecPeformDec2( p );
p->timeSat += Abc_Clock() - clk;
if ( RetValue == -1 )
//break;
if ( RetValue < 0 )
continue;
if ( pPars->fRrOnly )
Sfm_DecInsert( pNtk, pObj, Limit, &p->vObjGates, &p->vObjFanins, &p->vObjMap, &p->vGateHands );
if ( pPars->fVeryVerbose )
printf( "This was modification %d\n", Count );
......
src/opt/sfm/sfmInt.h
......@@ -45,10 +45,16 @@ ABC_NAMESPACE_HEADER_START
#define SFM_SAT_UNDEC 0x1234567812345678
#define SFM_SAT_SAT 0x8765432187654321
#define SFM_SUPP_MAX 6
#define SFM_WORD_MAX ((SFM_SUPP_MAX>6) ? (1<<(SFM_SUPP_MAX-6)) : 1)
////////////////////////////////////////////////////////////////////////
/// BASIC TYPES ///
////////////////////////////////////////////////////////////////////////
typedef struct Sfm_Fun_t_ Sfm_Fun_t;
typedef struct Sfm_Lib_t_ Sfm_Lib_t;
struct Sfm_Ntk_t_
{
// parameters
......@@ -182,6 +188,11 @@ extern int Sfm_TruthToCnf( word Truth, int nVars, Vec_Int_t * vCover, V
extern Vec_Wec_t * Sfm_CreateCnf( Sfm_Ntk_t * p );
extern void Sfm_TranslateCnf( Vec_Wec_t * vRes, Vec_Str_t * vCnf, Vec_Int_t * vFaninMap, int iPivotVar );
/*=== sfmCore.c ==========================================================*/
/*=== sfmLib.c ==========================================================*/
extern Sfm_Lib_t * Sfm_LibPrepare( int nVars, int fTwo, int fVerbose );
extern void Sfm_LibPrint( Sfm_Lib_t * p );
extern void Sfm_LibStop( Sfm_Lib_t * p );
extern int Sfm_LibImplement( Sfm_Lib_t * p, word uTruth, int * pFanins, int nFanins, Vec_Int_t * vGates, Vec_Wec_t * vFanins );
/*=== sfmNtk.c ==========================================================*/
extern Sfm_Ntk_t * Sfm_ConstructNetwork( Vec_Wec_t * vFanins, int nPis, int nPos );
extern void Sfm_NtkPrepare( Sfm_Ntk_t * p );
......
src/opt/sfm/sfmLib.c
......@@ -21,6 +21,11 @@
#include "sfmInt.h"
#include "misc/st/st.h"
#include "map/mio/mio.h"
#include "misc/vec/vecMem.h"
#include "misc/util/utilTruth.h"
#include "misc/extra/extra.h"
#include "map/mio/exp.h"
#include "opt/dau/dau.h"
ABC_NAMESPACE_IMPL_START
......@@ -29,6 +34,31 @@ ABC_NAMESPACE_IMPL_START
/// DECLARATIONS ///
////////////////////////////////////////////////////////////////////////
struct Sfm_Fun_t_
{
int Next; // next function in the list
int Area; // area of this function
char pFansT[8]; // top gate ID, followed by fanin perm
char pFansB[8]; // bottom gate ID, followed by fanin perm
};
struct Sfm_Lib_t_
{
Mio_Cell2_t * pCells; // library gates
int nCells; // library gate count
int nObjs; // object count
int nObjsAlloc; // object count
Sfm_Fun_t * pObjs; // objects
Vec_Mem_t * vTtMem; // truth tables
Vec_Int_t vLists; // lists of funcs for each truth table
Vec_Int_t vCounts; // counters of functions for each truth table
};
static inline Sfm_Fun_t * Sfm_LibFun( Sfm_Lib_t * p, int i ) { return i == -1 ? NULL : p->pObjs + i; }
#define Sfm_LibForEachSuper( p, pObj, Func ) \
for ( pObj = Sfm_LibFun(p, Vec_IntEntry(&p->vLists, Func)); pObj; pObj = Sfm_LibFun(p, pObj->Next) )
////////////////////////////////////////////////////////////////////////
/// FUNCTION DEFINITIONS ///
////////////////////////////////////////////////////////////////////////
......@@ -93,6 +123,269 @@ void Sfm_LibPreprocess( Mio_Library_t * pLib, Vec_Int_t * vGateSizes, Vec_Wrd_t
Sfm_DecCreateCnf( vGateSizes, vGateFuncs, vGateCnfs );
}
/**Function*************************************************************
Synopsis []
Description []
SideEffects []
SeeAlso []
***********************************************************************/
Sfm_Lib_t * Sfm_LibStart( int nVars )
{
Sfm_Lib_t * p = ABC_CALLOC( Sfm_Lib_t, 1 );
p->vTtMem = Vec_MemAllocForTT( nVars, 0 );
Vec_IntGrow( &p->vLists, (1 << 16) );
Vec_IntGrow( &p->vCounts, (1 << 16) );
Vec_IntFill( &p->vLists, 2, -1 );
Vec_IntFill( &p->vCounts, 2, -1 );
p->nObjsAlloc = (1 << 16);
p->pObjs = ABC_CALLOC( Sfm_Fun_t, p->nObjsAlloc );
return p;
}
void Sfm_LibStop( Sfm_Lib_t * p )
{
Vec_MemHashFree( p->vTtMem );
Vec_MemFree( p->vTtMem );
Vec_IntErase( &p->vLists );
Vec_IntErase( &p->vCounts );
ABC_FREE( p->pCells );
ABC_FREE( p->pObjs );
ABC_FREE( p );
}
/**Function*************************************************************
Synopsis []
Description []
SideEffects []
SeeAlso []
***********************************************************************/
word Sfm_LibTruthTwo( Mio_Cell2_t * pCellBot, Mio_Cell2_t * pCellTop, int InTop )
{
word uTruthBot = Exp_Truth6( pCellBot->nFanins, pCellBot->vExpr, NULL );
word uFanins[6]; int i, k;
assert( InTop >= 0 && InTop < (int)pCellTop->nFanins );
for ( i = 0, k = pCellBot->nFanins; i < (int)pCellTop->nFanins; i++ )
uFanins[i] = (i == InTop) ? uTruthBot : s_Truths6[k++];
assert( (int)pCellBot->nFanins + (int)pCellTop->nFanins == k + 1 );
uTruthBot = Exp_Truth6( pCellTop->nFanins, pCellTop->vExpr, uFanins );
return uTruthBot;
}
/**Function*************************************************************
Synopsis []
Description []
SideEffects []
SeeAlso []
***********************************************************************/
void Sfm_LibPrepareAdd( Sfm_Lib_t * p, word uTruth, int * Perm, int nFanins, Mio_Cell2_t * pCellBot, Mio_Cell2_t * pCellTop, int InTop )
{
Sfm_Fun_t * pObj;
int Area = (int)(pCellBot->Area / 1000) + (pCellTop ? (int)(pCellTop->Area / 1000) : 0);
int i, k, iFunc = Vec_MemHashInsert( p->vTtMem, &uTruth );
if ( iFunc == Vec_IntSize(&p->vLists) )
{
Vec_IntPush( &p->vLists, -1 );
Vec_IntPush( &p->vCounts, 0 );
}
assert( pCellBot != NULL );
// iterate through the supergates of this truth table
Sfm_LibForEachSuper( p, pObj, iFunc )
{
if ( Area >= pObj->Area )
return;
}
// create new object
if ( p->nObjs == p->nObjsAlloc )
{
int nObjsAlloc = 2 * p->nObjsAlloc;
p->pObjs = ABC_REALLOC( Sfm_Fun_t, p->pObjs, nObjsAlloc );
memset( p->pObjs + p->nObjsAlloc, 0, sizeof(Sfm_Fun_t) * p->nObjsAlloc );
p->nObjsAlloc = nObjsAlloc;
}
pObj = p->pObjs + p->nObjs;
pObj->Area = Area;
pObj->Next = Vec_IntEntry(&p->vLists, iFunc);
Vec_IntWriteEntry( &p->vLists, iFunc, p->nObjs++ );
Vec_IntAddToEntry( &p->vCounts, iFunc, 1 );
// create gate
assert( pCellBot->Id < 128 );
pObj->pFansB[0] = (char)pCellBot->Id;
for ( k = 0; k < (int)pCellBot->nFanins; k++ )
pObj->pFansB[k+1] = Perm[k];
if ( pCellTop == NULL )
return;
assert( pCellTop->Id < 128 );
pObj->pFansT[0] = (char)pCellTop->Id;
for ( i = 0; i < (int)pCellTop->nFanins; i++ )
pObj->pFansT[i+1] = (char)(i == InTop ? 16 : Perm[k++]);
assert( k == nFanins );
}
Sfm_Lib_t * Sfm_LibPrepare( int nVars, int fTwo, int fVerbose )
{
abctime clk = Abc_Clock();
Sfm_Lib_t * p = Sfm_LibStart( nVars );
Mio_Cell2_t * pCell1, * pCell2, * pLimit;
int * pPerm[7], * Perm1, * Perm2, Perm[6];
int nPerms[7], i, f, n;
Vec_Int_t * vUseful;
word tTemp1, tCur;
char pRes[1000];
assert( nVars <= 6 );
// precompute gates
p->pCells = Mio_CollectRootsNewDefault2( nVars, &p->nCells, 0 );
pLimit = p->pCells + p->nCells;
// find useful ones
vUseful = Vec_IntStart( p->nCells );
// vUseful = Vec_IntStartFull( p->nCells );
for ( pCell1 = p->pCells + 4; pCell1 < pLimit; pCell1++ )
{
word uTruth = pCell1->uTruth;
if ( Dau_DsdDecompose(&uTruth, pCell1->nFanins, 0, 0, pRes) <= 3 )
Vec_IntWriteEntry( vUseful, pCell1 - p->pCells, 1 );
else
printf( "Skipping gate \"%s\" with non-DSD function %s\n", pCell1->pName, pRes );
}
// generate permutations
for ( i = 2; i <= nVars; i++ )
pPerm[i] = Extra_PermSchedule( i );
for ( i = 2; i <= nVars; i++ )
nPerms[i] = Extra_Factorial( i );
// add single cells
for ( pCell1 = p->pCells + 4; pCell1 < pLimit; pCell1++ )
if ( Vec_IntEntry(vUseful, pCell1 - p->pCells) )
{
int nFanins = pCell1->nFanins;
assert( nFanins >= 2 && nFanins <= 6 );
for ( i = 0; i < nFanins; i++ )
Perm[i] = i;
// permute truth table
tCur = tTemp1 = pCell1->uTruth;
for ( n = 0; n < nPerms[nFanins]; n++ )
{
Sfm_LibPrepareAdd( p, tCur, Perm, nFanins, pCell1, NULL, -1 );
// update
tCur = Abc_Tt6SwapAdjacent( tCur, pPerm[nFanins][n] );
Perm1 = Perm + pPerm[nFanins][n];
Perm2 = Perm1 + 1;
ABC_SWAP( int, *Perm1, *Perm2 );
}
assert( tTemp1 == tCur );
}
// add double cells
if ( fTwo )
for ( pCell1 = p->pCells + 4; pCell1 < pLimit; pCell1++ )
if ( Vec_IntEntry(vUseful, pCell1 - p->pCells) )
for ( pCell2 = p->pCells + 4; pCell2 < pLimit; pCell2++ )
if ( Vec_IntEntry(vUseful, pCell2 - p->pCells) )
if ( (int)pCell1->nFanins + (int)pCell2->nFanins <= nVars + 1 )
for ( f = 0; f < (int)pCell2->nFanins; f++ )
{
int nFanins = pCell1->nFanins + pCell2->nFanins - 1;
assert( nFanins >= 2 && nFanins <= nVars );
for ( i = 0; i < nFanins; i++ )
Perm[i] = i;
// permute truth table
tCur = tTemp1 = Sfm_LibTruthTwo( pCell1, pCell2, f );
for ( n = 0; n < nPerms[nFanins]; n++ )
{
Sfm_LibPrepareAdd( p, tCur, Perm, nFanins, pCell1, pCell2, f );
// update
tCur = Abc_Tt6SwapAdjacent( tCur, pPerm[nFanins][n] );
Perm1 = Perm + pPerm[nFanins][n];
Perm2 = Perm1 + 1;
ABC_SWAP( int, *Perm1, *Perm2 );
}
assert( tTemp1 == tCur );
}
// cleanup
for ( i = 2; i <= nVars; i++ )
ABC_FREE( pPerm[i] );
Vec_IntFree( vUseful );
if ( fVerbose )
{
printf( "Library processing: Var = %d. Cells = %d. Func = %6d. Obj = %8d. Ave = %8.2f ", nVars, p->nCells, Vec_MemEntryNum(p->vTtMem), p->nObjs, 1.0*p->nObjs/Vec_MemEntryNum(p->vTtMem) );
Abc_PrintTime( 1, "Time", Abc_Clock() - clk );
}
return p;
}
void Sfm_LibPrintGate( Mio_Cell2_t * pCell, char * pFanins, Mio_Cell2_t * pCell2, char * pFanins2 )
{
int k;
printf( " %s(", pCell->pName );
for ( k = 0; k < (int)pCell->nFanins; k++ )
if ( pFanins[k] == (char)16 )
Sfm_LibPrintGate( pCell2, pFanins2, NULL, NULL );
else
printf( " %c", 'a' + pFanins[k] );
printf( " )" );
}
void Sfm_LibPrintObj( Sfm_Lib_t * p, Sfm_Fun_t * pObj )
{
Mio_Cell2_t * pCellB = p->pCells + (int)pObj->pFansB[0];
Mio_Cell2_t * pCellT = p->pCells + (int)pObj->pFansT[0];
int nFanins = pCellB->nFanins + (pCellT == p->pCells ? 0 : pCellT->nFanins);
printf( " Area = %6.2f Fanins = %d ", 0.001*pObj->Area, nFanins );
if ( pCellT == p->pCells )
Sfm_LibPrintGate( pCellB, pObj->pFansB + 1, NULL, NULL );
else
Sfm_LibPrintGate( pCellT, pObj->pFansT + 1, pCellB, pObj->pFansB + 1 );
printf( "\n" );
}
void Sfm_LibPrint( Sfm_Lib_t * p )
{
word * pTruth; Sfm_Fun_t * pObj; int iFunc;
Vec_MemForEachEntry( p->vTtMem, pTruth, iFunc )
{
if ( iFunc < 2 )
continue;
//if ( iFunc % 10000 )
// continue;
printf( "%d : Count = %d ", iFunc, Vec_IntEntry(&p->vCounts, iFunc) );
Dau_DsdPrintFromTruth( pTruth, Abc_TtSupportSize(pTruth, 6) );
Sfm_LibForEachSuper( p, pObj, iFunc )
Sfm_LibPrintObj( p, pObj );
}
}
void Sfm_LibTest( int nVars, int fTwo, int fVerbose )
{
Sfm_Lib_t * p = Sfm_LibPrepare( nVars, fTwo, 1 );
if ( fVerbose )
Sfm_LibPrint( p );
Sfm_LibStop( p );
}
/**Function*************************************************************
Synopsis []
Description []
SideEffects []
SeeAlso []
***********************************************************************/
int Sfm_LibImplement( Sfm_Lib_t * p, word uTruth, int * pFanins, int nFanins, Vec_Int_t * vGates, Vec_Wec_t * vFanins )
{
return 0;
}
////////////////////////////////////////////////////////////////////////
/// END OF FILE ///
////////////////////////////////////////////////////////////////////////
......
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment