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

Improvements to Boolean matching.

This commit is contained in:
Alan Mishchenko 2014-09-19 14:06:51 -07:00
parent ee72791293
commit b05ee94311
8 changed files with 563 additions and 88 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

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

@ -15309,7 +15309,7 @@ int Abc_CommandIf( Abc_Frame_t * pAbc, int argc, char ** argv )
pPars->fEnableCheck07 ^= 1;
break;
case 'i':
pPars->fEnableCheck08 ^= 1;
pPars->fUseCofVars ^= 1;
break;
case 'k':
pPars->fUseDsdTune ^= 1;
@ -15376,7 +15376,7 @@ int Abc_CommandIf( Abc_Frame_t * pAbc, int argc, char ** argv )
pPars->fCutMin = 1;
}
if ( pPars->fEnableCheck07 + pPars->fEnableCheck08 + pPars->fUseDsdTune + (pPars->pLutStruct != NULL) > 1 )
if ( pPars->fEnableCheck07 + pPars->fUseCofVars + pPars->fUseDsdTune + (pPars->pLutStruct != NULL) > 1 )
{
Abc_Print( -1, "Only one additional check can be performed at the same time.\n" );
return 1;
@ -15391,14 +15391,13 @@ int Abc_CommandIf( Abc_Frame_t * pAbc, int argc, char ** argv )
pPars->pFuncCell = If_CutPerformCheck07;
pPars->fCutMin = 1;
}
if ( pPars->fEnableCheck08 )
if ( pPars->fUseCofVars )
{
if ( pPars->nLutSize < 6 || pPars->nLutSize > 8 )
if ( !(pPars->nLutSize & 1) )
{
Abc_Print( -1, "This feature only works for {6,7,8}-LUTs.\n" );
Abc_Print( -1, "This feature only works for odd-sized LUTs.\n" );
return 1;
}
pPars->pFuncCell = If_CutPerformCheck08;
pPars->fCutMin = 1;
}
if ( pPars->fUseDsdTune )
@ -15610,7 +15609,7 @@ usage:
Abc_Print( -2, "\t-y : toggles delay optimization with recorded library [default = %s]\n", pPars->fUserRecLib? "yes": "no" );
Abc_Print( -2, "\t-o : toggles using buffers to decouple combinational outputs [default = %s]\n", pPars->fUseBuffs? "yes": "no" );
Abc_Print( -2, "\t-j : toggles enabling additional check [default = %s]\n", pPars->fEnableCheck07? "yes": "no" );
Abc_Print( -2, "\t-i : toggles enabling additional check [default = %s]\n", pPars->fEnableCheck08? "yes": "no" );
Abc_Print( -2, "\t-i : toggles using cofactoring variables [default = %s]\n", pPars->fUseCofVars? "yes": "no" );
Abc_Print( -2, "\t-k : toggles matching based on precomputed DSD manager [default = %s]\n", pPars->fUseDsdTune? "yes": "no" );
Abc_Print( -2, "\t-t : toggles optimizing average rather than maximum level [default = %s]\n", pPars->fDoAverage? "yes": "no" );
Abc_Print( -2, "\t-n : toggles computing DSDs of the cut functions [default = %s]\n", pPars->fUseDsd? "yes": "no" );
@ -30984,7 +30983,7 @@ int Abc_CommandAbc9If( Abc_Frame_t * pAbc, int argc, char ** argv )
}
pPars->pLutLib = (If_LibLut_t *)pAbc->pLibLut;
Extra_UtilGetoptReset();
while ( ( c = Extra_UtilGetopt( argc, argv, "KCFAGRDEWSTqalepmrsdbgxyojikfuztncvh" ) ) != EOF )
while ( ( c = Extra_UtilGetopt( argc, argv, "KCFAGRDEWSTqalepmrsdbgxyojfuikztncvh" ) ) != EOF )
{
switch ( c )
{
@ -31159,18 +31158,18 @@ int Abc_CommandAbc9If( Abc_Frame_t * pAbc, int argc, char ** argv )
case 'j':
pPars->fEnableCheck07 ^= 1;
break;
case 'i':
pPars->fEnableCheck08 ^= 1;
break;
case 'k':
pPars->fUseDsdTune ^= 1;
break;
case 'f':
pPars->fEnableCheck75 ^= 1;
break;
case 'u':
pPars->fEnableCheck75u ^= 1;
break;
case 'i':
pPars->fUseCofVars ^= 1;
break;
case 'k':
pPars->fUseDsdTune ^= 1;
break;
case 'z':
pPars->fDeriveLuts ^= 1;
break;
@ -31247,7 +31246,7 @@ int Abc_CommandAbc9If( Abc_Frame_t * pAbc, int argc, char ** argv )
pPars->fCutMin = 1;
}
if ( pPars->fEnableCheck07 + pPars->fEnableCheck08 + pPars->fUseDsdTune + pPars->fEnableCheck75 + pPars->fEnableCheck75u + (pPars->pLutStruct != NULL) > 1 )
if ( pPars->fEnableCheck07 + pPars->fUseCofVars + pPars->fUseDsdTune + pPars->fEnableCheck75 + pPars->fEnableCheck75u + (pPars->pLutStruct != NULL) > 1 )
{
Abc_Print( -1, "Only one additional check can be performed at the same time.\n" );
return 1;
@ -31262,14 +31261,13 @@ int Abc_CommandAbc9If( Abc_Frame_t * pAbc, int argc, char ** argv )
pPars->pFuncCell = If_CutPerformCheck07;
pPars->fCutMin = 1;
}
if ( pPars->fEnableCheck08 )
if ( pPars->fUseCofVars )
{
if ( pPars->nLutSize < 6 || pPars->nLutSize > 8 )
if ( !(pPars->nLutSize & 1) )
{
Abc_Print( -1, "This feature only works for {6,7,8}-LUTs.\n" );
Abc_Print( -1, "This feature only works for odd-sized LUTs.\n" );
return 1;
}
pPars->pFuncCell = If_CutPerformCheck08;
pPars->fCutMin = 1;
}
if ( pPars->fUseDsdTune )
@ -31439,7 +31437,7 @@ usage:
sprintf(LutSize, "library" );
else
sprintf(LutSize, "%d", pPars->nLutSize );
Abc_Print( -2, "usage: &if [-KCFAGRT num] [-DEW float] [-S str] [-qarlepmsdbgxyojikfuztncvh]\n" );
Abc_Print( -2, "usage: &if [-KCFAGRT num] [-DEW float] [-S str] [-qarlepmsdbgxyojfuikztncvh]\n" );
Abc_Print( -2, "\t performs FPGA technology mapping of the network\n" );
Abc_Print( -2, "\t-K num : the number of LUT inputs (2 < num < %d) [default = %s]\n", IF_MAX_LUTSIZE+1, LutSize );
Abc_Print( -2, "\t-C num : the max number of priority cuts (0 < num < 2^12) [default = %d]\n", pPars->nCutsMax );
@ -31467,9 +31465,9 @@ usage:
Abc_Print( -2, "\t-y : toggles delay optimization with recorded library [default = %s]\n", pPars->fUserRecLib? "yes": "no" );
Abc_Print( -2, "\t-o : toggles using buffers to decouple combinational outputs [default = %s]\n", pPars->fUseBuffs? "yes": "no" );
Abc_Print( -2, "\t-j : toggles enabling additional check [default = %s]\n", pPars->fEnableCheck07? "yes": "no" );
Abc_Print( -2, "\t-i : toggles enabling additional check [default = %s]\n", pPars->fEnableCheck08? "yes": "no" );
Abc_Print( -2, "\t-f : toggles enabling additional check [default = %s]\n", pPars->fEnableCheck75? "yes": "no" );
Abc_Print( -2, "\t-u : toggles enabling additional check [default = %s]\n", pPars->fEnableCheck75u? "yes": "no" );
Abc_Print( -2, "\t-i : toggles using cofactoring variables [default = %s]\n", pPars->fUseCofVars? "yes": "no" );
Abc_Print( -2, "\t-k : toggles matching based on precomputed DSD manager [default = %s]\n", pPars->fUseDsdTune? "yes": "no" );
Abc_Print( -2, "\t-z : toggles deriving LUTs when mapping into LUT structures [default = %s]\n", pPars->fDeriveLuts? "yes": "no" );
Abc_Print( -2, "\t-t : toggles optimizing average rather than maximum level [default = %s]\n", pPars->fDoAverage? "yes": "no" );
@ -32255,7 +32253,7 @@ usage:
Abc_Print( -2, "\t-L num : the fanout limit for coarsening XOR/MUX (num >= 2) [default = %d]\n", pPars->nCoarseLimit );
Abc_Print( -2, "\t-E num : the area/edge tradeoff parameter (0 <= num <= 100) [default = %d]\n", pPars->nAreaTuner );
Abc_Print( -2, "\t-D num : sets the delay constraint for the mapping [default = %s]\n", Buffer );
Abc_Print( -2, "\t-M num : LUT size for the cofactoring (0 <= num <= 100) [default = %d]\n", pPars->nLutSizeMux );
Abc_Print( -2, "\t-M num : LUT size when cofactoring is performed (0 <= num <= 100) [default = %d]\n", pPars->nLutSizeMux );
// Abc_Print( -2, "\t-a : toggles area-oriented mapping [default = %s]\n", pPars->fAreaOnly? "yes": "no" );
Abc_Print( -2, "\t-e : toggles edge vs node minimization [default = %s]\n", pPars->fOptEdge? "yes": "no" );
Abc_Print( -2, "\t-k : toggles coarsening the subject graph [default = %s]\n", pPars->fCoarsen? "yes": "no" );

2
src/map/if/if.h
View File

@ -131,6 +131,7 @@ struct If_Par_t_
int fEnableCheck75u;// enable additional checking
int fUseDsd; // compute DSD of the cut functions
int fUseDsdTune; // use matching based on precomputed manager
int fUseCofVars; // use cofactoring variables
int fUseTtPerm; // compute truth tables of the cut functions
int fDeriveLuts; // enables deriving LUT structures
int fDoAverage; // optimize average rather than maximum level
@ -242,6 +243,7 @@ struct If_Man_t_
Vec_Wec_t * vTtIsops[IF_MAX_FUNC_LUTSIZE+1]; // mapping of truth table into DSD
Vec_Int_t * vTtDsds[IF_MAX_FUNC_LUTSIZE+1]; // mapping of truth table into DSD
Vec_Str_t * vTtPerms[IF_MAX_FUNC_LUTSIZE+1]; // mapping of truth table into permutations
Vec_Str_t * vTtVars[IF_MAX_FUNC_LUTSIZE+1]; // mapping of truth table into selected vars
Hash_IntMan_t * vPairHash; // hashing pairs of truth tables
Vec_Int_t * vPairRes; // resulting truth table
Vec_Str_t * vPairPerms; // resulting permutation

2
src/map/if/ifCut.c
View File

@ -754,7 +754,7 @@ void If_CutSort( If_Man_t * p, If_Set_t * pCutSet, If_Cut_t * pCut )
if ( !pCut->fUseless &&
(p->pPars->fUseDsd || p->pPars->fUseBat ||
p->pPars->pLutStruct || p->pPars->fUserRecLib ||
p->pPars->fEnableCheck07 || p->pPars->fEnableCheck08 ||
p->pPars->fEnableCheck07 || p->pPars->fUseCofVars ||
p->pPars->fUseDsdTune || p->pPars->fEnableCheck75 ||
p->pPars->fEnableCheck75u) )
{

5
src/map/if/ifDsd.c
View File

@ -2410,7 +2410,8 @@ void Id_DsdManTuneStr1( If_DsdMan_t * p, char * pStruct, int nConfls, int fVerbo
pProgress = Extra_ProgressBarStart( stdout, Vec_PtrSize(&p->vObjs) );
If_DsdVecForEachObjStart( &p->vObjs, pObj, i, p->nObjsPrev )
{
Extra_ProgressBarUpdate( pProgress, i, NULL );
if ( (i & 0xFF) == 0 )
Extra_ProgressBarUpdate( pProgress, i, NULL );
nVars = If_DsdObjSuppSize(pObj);
if ( nVars <= LutSize )
continue;
@ -2574,7 +2575,7 @@ void Id_DsdManTuneStr( If_DsdMan_t * p, char * pStruct, int nConfls, int nProcs,
}
for ( k = iCurrentObj; k < Vec_PtrSize(&p->vObjs); k++ )
{
if ( (k & 0x3FF) == 0 )
if ( (k & 0xFF) == 0 )
Extra_ProgressBarUpdate( pProgress, k, NULL );
pObj = If_DsdVecObj( &p->vObjs, k );
nVars = If_DsdObjSuppSize(pObj);

17
src/map/if/ifMan.c
View File

@ -125,6 +125,17 @@ If_Man_t * If_ManStart( If_Par_t * pPars )
p->vPairRes = Vec_IntAlloc( 1000 );
Vec_IntPush( p->vPairRes, -1 );
}
if ( pPars->fUseCofVars )
{
for ( v = 6; v <= Abc_MaxInt(6,p->pPars->nLutSize); v++ )
{
p->vTtVars[v] = Vec_StrAlloc( 1000 );
Vec_StrPush( p->vTtVars[v], 0 );
Vec_StrPush( p->vTtVars[v], 0 );
}
for ( v = 0; v < 6; v++ )
p->vTtVars[v] = p->vTtVars[6];
}
if ( pPars->fUseBat )
{
// abctime clk = Abc_Clock();
@ -209,8 +220,8 @@ void If_ManStop( If_Man_t * p )
{
for ( i = 0; i <= 16; i++ )
if ( p->nCutsUseless[i] )
Abc_Print( 1, "Useless cuts %2d = %9d (out of %9d) (%6.2f %%)\n", i, p->nCutsUseless[i], p->nCutsCount[i], 100.0*p->nCutsUseless[i]/(p->nCutsCount[i]+1) );
Abc_Print( 1, "Useless cuts all = %9d (out of %9d) (%6.2f %%)\n", p->nCutsUselessAll, p->nCutsCountAll, 100.0*p->nCutsUselessAll/(p->nCutsCountAll+1) );
Abc_Print( 1, "Useless cuts %2d = %9d (out of %9d) (%6.2f %%)\n", i, p->nCutsUseless[i], p->nCutsCount[i], 100.0*p->nCutsUseless[i]/Abc_MaxInt(p->nCutsCount[i],1) );
Abc_Print( 1, "Useless cuts all = %9d (out of %9d) (%6.2f %%)\n", p->nCutsUselessAll, p->nCutsCountAll, 100.0*p->nCutsUselessAll/Abc_MaxInt(p->nCutsCountAll,1) );
}
// if ( p->pPars->fVerbose && p->nCuts5 )
// Abc_Print( 1, "Statistics about 5-cuts: Total = %d Non-decomposable = %d (%.2f %%)\n", p->nCuts5, p->nCuts5-p->nCuts5a, 100.0*(p->nCuts5-p->nCuts5a)/p->nCuts5 );
@ -235,6 +246,8 @@ void If_ManStop( If_Man_t * p )
Vec_IntFreeP( &p->vTtDsds[i] );
for ( i = 6; i <= Abc_MaxInt(6,p->pPars->nLutSize); i++ )
Vec_StrFreeP( &p->vTtPerms[i] );
for ( i = 6; i <= Abc_MaxInt(6,p->pPars->nLutSize); i++ )
Vec_StrFreeP( &p->vTtVars[i] );
Vec_IntFreeP( &p->vCutData );
Vec_IntFreeP( &p->vPairRes );
Vec_StrFreeP( &p->vPairPerms );

19
src/map/if/ifMap.c
View File

@ -270,6 +270,25 @@ void If_ObjPerformMappingAnd( If_Man_t * p, If_Obj_t * pObj, int Mode, int fPrep
p->nCutsCountAll++;
p->nCutsCount[pCut->nLeaves]++;
}
else if ( p->pPars->fUseCofVars )
{
extern int Abc_TtCheckCondDepTest( word * pTruth, int nVars, int nSuppLim );
int iCofVar = -1, truthId = Abc_Lit2Var(pCut->iCutFunc);
if ( truthId >= Vec_StrSize(p->vTtVars[pCut->nLeaves]) || Vec_StrEntry(p->vTtVars[pCut->nLeaves], truthId) == (char)-1 )
{
while ( truthId >= Vec_StrSize(p->vTtVars[pCut->nLeaves]) )
Vec_StrPush( p->vTtVars[pCut->nLeaves], (char)-1 );
iCofVar = Abc_TtCheckCondDep( If_CutTruthWR(p, pCut), pCut->nLeaves, p->pPars->nLutSize / 2 );
Vec_StrWriteEntry( p->vTtVars[pCut->nLeaves], truthId, (char)iCofVar );
}
iCofVar = Vec_StrEntry(p->vTtVars[pCut->nLeaves], truthId);
assert( iCofVar >= 0 && iCofVar <= (int)pCut->nLeaves );
pCut->fUseless = (int)(iCofVar == (int)pCut->nLeaves && pCut->nLeaves > 0);
p->nCutsUselessAll += pCut->fUseless;
p->nCutsUseless[pCut->nLeaves] += pCut->fUseless;
p->nCutsCountAll++;
p->nCutsCount[pCut->nLeaves]++;
}
}
// compute the application-specific cost and depth

495
src/map/if/ifTune.c
View File

@ -37,14 +37,14 @@ ABC_NAMESPACE_IMPL_START
// network types
typedef enum {
IF_DSD_NONE = 0, // 0: unknown
IF_DSD_CONST0, // 1: constant
IF_DSD_VAR, // 2: variable
IF_DSD_AND, // 3: AND
IF_DSD_XOR, // 4: XOR
IF_DSD_MUX, // 5: MUX
IF_DSD_PRIME // 6: PRIME
} If_DsdType_t;
IFN_DSD_NONE = 0, // 0: unknown
IFN_DSD_CONST0, // 1: constant
IFN_DSD_VAR, // 2: variable
IFN_DSD_AND, // 3: AND
IFN_DSD_XOR, // 4: XOR
IFN_DSD_MUX, // 5: MUX
IFN_DSD_PRIME // 6: PRIME
} Ifn_DsdType_t;
// object types
static char * Ifn_Symbs[16] = {
@ -124,7 +124,7 @@ int Ifn_Prepare( Ifn_Ntk_t * p, word * pTruth, int nVars )
p->nPars = p->nObjs;
for ( i = p->nInps; i < p->nObjs; i++ )
{
if ( p->Nodes[i].Type != IF_DSD_PRIME )
if ( p->Nodes[i].Type != IFN_DSD_PRIME )
continue;
p->Nodes[i].iFirst = p->nPars;
p->nPars += (1 << p->Nodes[i].nFanins);
@ -162,7 +162,7 @@ int Ifn_NtkLutSizeMax( Ifn_Ntk_t * p )
{
int i, LutSize = 0;
for ( i = p->nInps; i < p->nObjs; i++ )
if ( p->Nodes[i].Type == IF_DSD_PRIME )
if ( p->Nodes[i].Type == IFN_DSD_PRIME )
LutSize = Abc_MaxInt( LutSize, (int)p->Nodes[i].nFanins );
return LutSize;
}
@ -182,9 +182,150 @@ int Ifn_NtkInputNum( Ifn_Ntk_t * p )
SeeAlso []
***********************************************************************/
int Ifn_ErrorMessage( const char * format, ... )
{
char * pMessage;
va_list args;
va_start( args, format );
pMessage = vnsprintf( format, args );
va_end( args );
printf( "%s", pMessage );
ABC_FREE( pMessage );
return 0;
}
int Inf_ManOpenSymb( char * pStr )
{
if ( pStr[0] == '(' )
return 3;
if ( pStr[0] == '[' )
return 4;
if ( pStr[0] == '<' )
return 5;
if ( pStr[0] == '{' )
return 6;
return 0;
}
int Ifn_ManStrCheck( char * pStr, int * pnInps, int * pnObjs )
{
int i, Marks[32] = {0}, MaxVar = 0, MaxDef = 0, RetValue = 1;
int i, nNodes = 0, Marks[32] = {0}, MaxVar = -1, RetValue = 1;
for ( i = 0; pStr[i]; i++ )
{
if ( Inf_ManOpenSymb(pStr+i) )
nNodes++;
if ( pStr[i] == ';' ||
pStr[i] == '(' || pStr[i] == ')' ||
pStr[i] == '[' || pStr[i] == ']' ||
pStr[i] == '<' || pStr[i] == '>' ||
pStr[i] == '{' || pStr[i] == '}' )
continue;
if ( pStr[i] >= 'A' && pStr[i] <= 'Z' )
continue;
if ( pStr[i] >= 'a' && pStr[i] <= 'z' )
{
MaxVar = Abc_MaxInt( MaxVar, (int)(pStr[i] - 'a') );
Marks[pStr[i] - 'a'] = 1;
continue;
}
return Ifn_ErrorMessage( "String \"%s\" contains unrecognized symbol \'%c\'.\n", pStr, pStr[i] );
}
for ( i = 0; i <= MaxVar; i++ )
if ( Marks[i] == 0 )
return Ifn_ErrorMessage( "String \"%s\" has no symbol \'%c\'.\n", pStr, 'a' + i );
*pnInps = MaxVar + 1;
*pnObjs = MaxVar + 1 + nNodes;
return 1;
}
static inline char * Ifn_NtkParseFindClosingParanthesis( char * pStr, char Open, char Close )
{
int Counter = 0;
assert( *pStr == Open );
for ( ; *pStr; pStr++ )
{
if ( *pStr == Open )
Counter++;
if ( *pStr == Close )
Counter--;
if ( Counter == 0 )
return pStr;
}
return NULL;
}
int Ifn_NtkParseInt_rec( char * pStr, Ifn_Ntk_t * p, char ** ppFinal, int * piNode )
{
Ifn_Obj_t * pObj;
int nFanins = 0, pFanins[IFN_INS];
int Type = Inf_ManOpenSymb( pStr );
char * pLim = Ifn_NtkParseFindClosingParanthesis( pStr++, Ifn_Symbs[Type][0], Ifn_Symbs[Type][1] );
*ppFinal = NULL;
if ( pLim == NULL )
return Ifn_ErrorMessage( "For symbol \'%c\' cannot find matching symbol \'%c\'.\n", Ifn_Symbs[Type][0], Ifn_Symbs[Type][1] );
while ( pStr < pLim )
{
assert( nFanins < IFN_INS );
if ( pStr[0] >= 'a' && pStr[0] <= 'z' )
pFanins[nFanins++] = pStr[0] - 'a', pStr++;
else if ( Inf_ManOpenSymb(pStr) )
{
if ( !Ifn_NtkParseInt_rec( pStr, p, &pStr, piNode ) )
return 0;
pFanins[nFanins++] = *piNode - 1;
}
else
return Ifn_ErrorMessage( "Substring \"%s\" contans unrecognized symbol \'%c\'.\n", pStr, pStr[0] );
}
assert( pStr == pLim );
pObj = p->Nodes + (*piNode)++;
pObj->Type = Type;
assert( pObj->nFanins == 0 );
pObj->nFanins = nFanins;
memcpy( pObj->Fanins, pFanins, sizeof(int) * nFanins );
*ppFinal = pLim + 1;
if ( Type == IFN_DSD_MUX && nFanins != 3 )
return Ifn_ErrorMessage( "MUX should have exactly three fanins.\n" );
return 1;
}
int Ifn_NtkParseInt( char * pStr, Ifn_Ntk_t * p )
{
char * pFinal; int iNode;
if ( !Ifn_ManStrCheck(pStr, &p->nInps, &p->nObjs) )
return 0;
if ( p->nInps > IFN_INS )
return Ifn_ErrorMessage( "The number of variables (%d) exceeds predefined limit (%d). Recompile with different value of IFN_INS.\n", p->nInps, IFN_INS );
assert( p->nInps > 1 && p->nInps < p->nObjs && p->nInps <= IFN_INS && p->nObjs < 2*IFN_INS );
if ( !Inf_ManOpenSymb(pStr) )
return Ifn_ErrorMessage( "The first symbol should be one of the symbols: (, [, <, {.\n" );
iNode = p->nInps;
if ( !Ifn_NtkParseInt_rec( pStr, p, &pFinal, &iNode ) )
return 0;
if ( pFinal[0] && pFinal[0] != ';' )
return Ifn_ErrorMessage( "The last symbol should be \';\'.\n" );
if ( iNode != p->nObjs )
return Ifn_ErrorMessage( "Mismatch in the number of nodes.\n" );
return 1;
}
/**Function*************************************************************
Synopsis []
Description []
SideEffects []
SeeAlso []
***********************************************************************/
int Ifn_ManStrType2( char * pStr )
{
int i;
for ( i = 0; pStr[i]; i++ )
if ( pStr[i] == '=' )
return 1;
return 0;
}
int Ifn_ManStrCheck2( char * pStr, int * pnInps, int * pnObjs )
{
int i, Marks[32] = {0}, MaxVar = 0, MaxDef = 0;
for ( i = 0; pStr[i]; i++ )
{
if ( pStr[i] == '=' || pStr[i] == ';' ||
@ -201,11 +342,8 @@ int Ifn_ManStrCheck( char * pStr, int * pnInps, int * pnObjs )
Marks[pStr[i] - 'a'] = 2, MaxDef = Abc_MaxInt(MaxDef, pStr[i] - 'a');
continue;
}
printf( "String \"%s\" contains unrecognized symbol (%c).\n", pStr, pStr[i] );
RetValue = 0;
return Ifn_ErrorMessage( "String \"%s\" contains unrecognized symbol \'%c\'.\n", pStr, pStr[i] );
}
if ( !RetValue )
return 0;
for ( i = 0; pStr[i]; i++ )
{
if ( pStr[i] == '=' || pStr[i] == ';' ||
@ -222,43 +360,27 @@ int Ifn_ManStrCheck( char * pStr, int * pnInps, int * pnObjs )
Marks[pStr[i] - 'a'] = 1, MaxVar = Abc_MaxInt(MaxVar, pStr[i] - 'a');
continue;
}
printf( "String \"%s\" contains unrecognized symbol (%c).\n", pStr, pStr[i] );
RetValue = 0;
return Ifn_ErrorMessage( "String \"%s\" contains unrecognized symbol \'%c\'.\n", pStr, pStr[i] );
}
if ( !RetValue )
return 0;
MaxVar++;
MaxDef++;
for ( i = 0; i < MaxDef; i++ )
if ( Marks[i] == 0 )
printf( "String \"%s\" has no symbol (%c).\n", pStr, 'a' + i ), RetValue = 0;
return Ifn_ErrorMessage( "String \"%s\" has no symbol \'%c\'.\n", pStr, 'a' + i );
for ( i = 0; i < MaxVar; i++ )
if ( Marks[i] == 2 )
printf( "String \"%s\" has definition of input variable (%c).\n", pStr, 'a' + i ), RetValue = 0;
return Ifn_ErrorMessage( "String \"%s\" has definition of input variable \'%c\'.\n", pStr, 'a' + i );
for ( i = MaxVar; i < MaxDef; i++ )
if ( Marks[i] == 1 )
printf( "String \"%s\" has no definition for internal variable (%c).\n", pStr, 'a' + i ), RetValue = 0;
if ( !RetValue )
return 0;
return Ifn_ErrorMessage( "String \"%s\" has no definition for internal variable \'%c\'.\n", pStr, 'a' + i );
*pnInps = MaxVar;
*pnObjs = MaxDef;
return 1;
}
int Ifn_ErrorMessage( const char * format, ... )
{
char * pMessage;
va_list args;
va_start( args, format );
pMessage = vnsprintf( format, args );
va_end( args );
printf( "%s", pMessage );
ABC_FREE( pMessage );
return 0;
}
int Ifn_NtkParseInt( char * pStr, Ifn_Ntk_t * p )
int Ifn_NtkParseInt2( char * pStr, Ifn_Ntk_t * p )
{
int i, k, n, f, nFans, iFan;
if ( !Ifn_ManStrCheck(pStr, &p->nInps, &p->nObjs) )
if ( !Ifn_ManStrCheck2(pStr, &p->nInps, &p->nObjs) )
return 0;
if ( p->nInps > IFN_INS )
return Ifn_ErrorMessage( "The number of variables (%d) exceeds predefined limit (%d). Recompile with different value of IFN_INS.\n", p->nInps, IFN_INS );
@ -270,25 +392,25 @@ int Ifn_NtkParseInt( char * pStr, Ifn_Ntk_t * p )
if ( pStr[k] == 'a' + i && pStr[k+1] == '=' )
break;
if ( pStr[k] == 0 )
return Ifn_ErrorMessage( "Cannot find definition of signal %c.\n", 'a' + i );
return Ifn_ErrorMessage( "Cannot find definition of signal \'%c\'.\n", 'a' + i );
if ( pStr[k+2] == '(' )
p->Nodes[i].Type = IF_DSD_AND, Next = ')';
p->Nodes[i].Type = IFN_DSD_AND, Next = ')';
else if ( pStr[k+2] == '[' )
p->Nodes[i].Type = IF_DSD_XOR, Next = ']';
p->Nodes[i].Type = IFN_DSD_XOR, Next = ']';
else if ( pStr[k+2] == '<' )
p->Nodes[i].Type = IF_DSD_MUX, Next = '>';
p->Nodes[i].Type = IFN_DSD_MUX, Next = '>';
else if ( pStr[k+2] == '{' )
p->Nodes[i].Type = IF_DSD_PRIME, Next = '}';
p->Nodes[i].Type = IFN_DSD_PRIME, Next = '}';
else
return Ifn_ErrorMessage( "Cannot find openning operation symbol in the defition of of signal %c.\n", 'a' + i );
return Ifn_ErrorMessage( "Cannot find openning operation symbol in the defition of of signal \'%c\'.\n", 'a' + i );
for ( n = k + 3; pStr[n]; n++ )
if ( pStr[n] == Next )
break;
if ( pStr[n] == 0 )
return Ifn_ErrorMessage( "Cannot find closing operation symbol in the defition of of signal %c.\n", 'a' + i );
return Ifn_ErrorMessage( "Cannot find closing operation symbol in the defition of of signal \'%c\'.\n", 'a' + i );
nFans = n - k - 3;
if ( nFans < 1 || nFans > 8 )
return Ifn_ErrorMessage( "Cannot find matching operation symbol in the defition of of signal %c.\n", 'a' + i );
return Ifn_ErrorMessage( "Cannot find matching operation symbol in the defition of of signal \'%c\'.\n", 'a' + i );
for ( f = 0; f < nFans; f++ )
{
iFan = pStr[k + 3 + f] - 'a';
@ -298,8 +420,11 @@ int Ifn_NtkParseInt( char * pStr, Ifn_Ntk_t * p )
}
p->Nodes[i].nFanins = nFans;
}
// truth tables
Abc_TtElemInit2( p->pTtElems, p->nInps );
return 1;
}
void Ifn_NtkParseConstraints( char * pStr, Ifn_Ntk_t * p )
{
int i, k;
// parse constraints
p->nConstr = 0;
for ( i = 0; i < p->nInps; i++ )
@ -311,17 +436,265 @@ int Ifn_NtkParseInt( char * pStr, Ifn_Ntk_t * p )
}
// if ( p->nConstr )
// printf( "Total constraints = %d\n", p->nConstr );
return 1;
}
Ifn_Ntk_t * Ifn_NtkParse( char * pStr )
{
Ifn_Ntk_t * p = ABC_CALLOC( Ifn_Ntk_t, 1 );
if ( Ifn_NtkParseInt( pStr, p ) )
return p;
ABC_FREE( p );
return NULL;
if ( Ifn_ManStrType2(pStr) )
{
if ( !Ifn_NtkParseInt2( pStr, p ) )
{
ABC_FREE( p );
return NULL;
}
}
else
{
if ( !Ifn_NtkParseInt( pStr, p ) )
{
ABC_FREE( p );
return NULL;
}
}
Ifn_NtkParseConstraints( pStr, p );
Abc_TtElemInit2( p->pTtElems, p->nInps );
printf( "Finished parsing: " ); Ifn_NtkPrint(p);
return p;
}
/**Function*************************************************************
Synopsis [Derive AIG.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
Gia_Man_t * Ifn_ManStrFindModel( Ifn_Ntk_t * p )
{
Gia_Man_t * pNew, * pTemp;
int i, k, iLit, * pVarMap = ABC_FALLOC( int, p->nParsVIni );
pNew = Gia_ManStart( 1000 );
pNew->pName = Abc_UtilStrsav( "model" );
Gia_ManHashStart( pNew );
for ( i = 0; i < p->nInps; i++ )
pVarMap[i] = Gia_ManAppendCi(pNew);
for ( i = p->nObjs; i < p->nParsVIni; i++ )
pVarMap[i] = Gia_ManAppendCi(pNew);
for ( i = p->nInps; i < p->nObjs; i++ )
{
int Type = p->Nodes[i].Type;
int nFans = p->Nodes[i].nFanins;
int * pFans = p->Nodes[i].Fanins;
int iFanin = p->Nodes[i].iFirst;
if ( Type == IFN_DSD_AND )
{
iLit = 1;
for ( k = 0; k < nFans; k++ )
iLit = Gia_ManHashAnd( pNew, iLit, pVarMap[pFans[k]] );
pVarMap[i] = iLit;
}
else if ( Type == IFN_DSD_XOR )
{
iLit = 0;
for ( k = 0; k < nFans; k++ )
iLit = Gia_ManHashXor( pNew, iLit, pVarMap[pFans[k]] );
pVarMap[i] = iLit;
}
else if ( Type == IFN_DSD_MUX )
{
assert( nFans == 3 );
pVarMap[i] = Gia_ManHashMux( pNew, pVarMap[pFans[0]], pVarMap[pFans[1]], pVarMap[pFans[2]] );
}
else if ( Type == IFN_DSD_PRIME )
{
int n, Step, pVarsData[256];
int nMints = (1 << nFans);
assert( nFans >= 1 && nFans <= 8 );
for ( k = 0; k < nMints; k++ )
pVarsData[k] = pVarMap[iFanin + k];
for ( Step = 1, k = 0; k < nFans; k++, Step <<= 1 )
for ( n = 0; n < nMints; n += Step << 1 )
pVarsData[n] = Gia_ManHashMux( pNew, pVarMap[pFans[k]], pVarsData[n+Step], pVarsData[n] );
assert( Step == nMints );
pVarMap[i] = pVarsData[0];
}
else assert( 0 );
}
Gia_ManAppendCo( pNew, pVarMap[p->nObjs-1] );
ABC_FREE( pVarMap );
pNew = Gia_ManCleanup( pTemp = pNew );
Gia_ManStop( pTemp );
assert( Gia_ManPiNum(pNew) == p->nParsVIni - (p->nObjs - p->nInps) );
assert( Gia_ManPoNum(pNew) == 1 );
return pNew;
}
// compute cofactors w.r.t. the first nIns variables
Gia_Man_t * Ifn_ManStrFindCofactors( int nIns, Gia_Man_t * p )
{
Gia_Man_t * pNew, * pTemp;
Gia_Obj_t * pObj;
int i, m, nMints = nIns;
pNew = Gia_ManStart( Gia_ManObjNum(p) );
pNew->pName = Abc_UtilStrsav( p->pName );
Gia_ManHashAlloc( pNew );
Gia_ManConst0(p)->Value = 0;
Gia_ManForEachCi( p, pObj, i )
if ( i >= nIns )
pObj->Value = Gia_ManAppendCi( pNew );
for ( m = 0; m < nMints; m++ )
{
Gia_ManForEachCi( p, pObj, i )
if ( i < nIns )
pObj->Value = ((m >> i) & 1);
Gia_ManForEachAnd( p, pObj, i )
pObj->Value = Gia_ManHashAnd( pNew, Gia_ObjFanin0Copy(pObj), Gia_ObjFanin1Copy(pObj) );
Gia_ManForEachPo( p, pObj, i )
pObj->Value = Gia_ManAppendCo( pNew, Gia_ObjFanin0Copy(pObj) );
}
pNew = Gia_ManCleanup( pTemp = pNew );
Gia_ManStop( pTemp );
return pNew;
}
/**Function*************************************************************
Synopsis [Derive SAT solver.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
static inline Cnf_Dat_t * Cnf_DeriveGiaRemapped( Gia_Man_t * p )
{
Cnf_Dat_t * pCnf;
Aig_Man_t * pAig = Gia_ManToAigSimple( p );
pAig->nRegs = 0;
pCnf = Cnf_Derive( pAig, Aig_ManCoNum(pAig) );
Aig_ManStop( pAig );
return pCnf;
}
sat_solver * Ifn_ManStrFindSolver( Gia_Man_t * p, Vec_Int_t ** pvPiVars, Vec_Int_t ** pvPoVars )
{
sat_solver * pSat;
Gia_Obj_t * pObj;
Cnf_Dat_t * pCnf;
int i;
pCnf = Cnf_DeriveGiaRemapped( p );
// start the SAT solver
pSat = sat_solver_new();
sat_solver_setnvars( pSat, pCnf->nVars );
// add timeframe clauses
for ( i = 0; i < pCnf->nClauses; i++ )
if ( !sat_solver_addclause( pSat, pCnf->pClauses[i], pCnf->pClauses[i+1] ) )
assert( 0 );
// inputs/outputs
*pvPiVars = Vec_IntAlloc( Gia_ManPiNum(p) );
Gia_ManForEachCi( p, pObj, i )
Vec_IntPush( *pvPiVars, pCnf->pVarNums[Gia_ObjId(p, pObj)] );
*pvPoVars = Vec_IntAlloc( Gia_ManPoNum(p) );
Gia_ManForEachCo( p, pObj, i )
Vec_IntPush( *pvPoVars, pCnf->pVarNums[Gia_ObjId(p, pObj)] );
Cnf_DataFree( pCnf );
return pSat;
}
sat_solver * Ifn_ManSatBuild( Ifn_Ntk_t * p, Vec_Int_t ** pvPiVars, Vec_Int_t ** pvPoVars )
{
Gia_Man_t * p1, * p2;
sat_solver * pSat = NULL;
*pvPiVars = *pvPoVars = NULL;
p1 = Ifn_ManStrFindModel( p );
// Gia_AigerWrite( p1, "satbuild.aig", 0, 0 );
p2 = Ifn_ManStrFindCofactors( p->nInps, p1 );
Gia_ManStop( p1 );
// Gia_AigerWrite( p2, "satbuild2.aig", 0, 0 );
pSat = Ifn_ManStrFindSolver( p2, pvPiVars, pvPoVars );
Gia_ManStop( p2 );
return pSat;
}
/**Function*************************************************************
Synopsis []
Description []
SideEffects []
SeeAlso []
***********************************************************************/
void Ifn_ManSatPrintPerm( char * pPerms, int nVars )
{
int i;
for ( i = 0; i < nVars; i++ )
printf( "%c", 'a' + pPerms[i] );
printf( "\n" );
}
int Ifn_ManSatCheckOne( sat_solver * pSat, Vec_Int_t * vPoVars, word * pTruth, int nVars, int * pPerm, int nVarsAll, Vec_Int_t * vLits )
{
int v, Value, m, mNew, nMints = (1 << nVars);
assert( (1 << nVarsAll) == Vec_IntSize(vPoVars) );
assert( nVars <= nVarsAll );
// remap minterms
Vec_IntFill( vLits, Vec_IntSize(vPoVars), -1 );
for ( m = 0; m < nMints; m++ )
{
mNew = 0;
for ( v = 0; v < nVarsAll; v++ )
{
assert( pPerm[v] < nVars );
if ( ((m >> pPerm[v]) & 1) )
mNew |= (1 << v);
}
assert( Vec_IntEntry(vLits, mNew) == -1 );
Vec_IntWriteEntry( vLits, mNew, Abc_TtGetBit(pTruth, m) );
}
// find assumptions
v = 0;
Vec_IntForEachEntry( vLits, Value, m )
if ( Value >= 0 )
Vec_IntWriteEntry( vLits, v++, Abc_Var2Lit(Vec_IntEntry(vPoVars, m), !Value) );
Vec_IntShrink( vLits, v );
// run SAT solver
Value = sat_solver_solve( pSat, Vec_IntArray(vLits), Vec_IntArray(vLits) + Vec_IntSize(vLits), 0, 0, 0, 0 );
return (int)(Value == l_True);
}
void Ifn_ManSatDeriveOne( sat_solver * pSat, Vec_Int_t * vPiVars, Vec_Int_t * vValues )
{
int i, iVar;
Vec_IntClear( vValues );
Vec_IntForEachEntry( vPiVars, iVar, i )
Vec_IntPush( vValues, sat_solver_var_value(pSat, iVar) );
}
int Ifn_ManSatFindCofigBits( sat_solver * pSat, Vec_Int_t * vPiVars, Vec_Int_t * vPoVars, word * pTruth, int nVars, word Perm, Vec_Int_t * vValues )
{
// extract permutation
int RetValue, i, pPerm[IF_MAX_FUNC_LUTSIZE];
for ( i = 0; i < Vec_IntSize(vPiVars); i++ )
{
pPerm[i] = Abc_TtGetHex( &Perm, i );
assert( pPerm[i] < nVars );
}
// perform SAT check
RetValue = Ifn_ManSatCheckOne( pSat, vPoVars, pTruth, nVars, pPerm, Vec_IntSize(vPiVars), vValues );
Vec_IntClear( vValues );
if ( RetValue == 0 )
return 0;
Ifn_ManSatDeriveOne( pSat, vPiVars, vValues );
return 1;
}
/**Function*************************************************************
Synopsis [Derive truth table given the configulation values.]
@ -353,24 +726,24 @@ word * Ifn_NtkDeriveTruth( Ifn_Ntk_t * p, int * pValues )
int nFans = p->Nodes[i].nFanins;
int * pFans = p->Nodes[i].Fanins;
word * pTruth = Ifn_ObjTruth( p, i );
if ( p->Nodes[i].Type == IF_DSD_AND )
if ( p->Nodes[i].Type == IFN_DSD_AND )
{
Abc_TtFill( pTruth, p->nWords );
for ( f = 0; f < nFans; f++ )
Abc_TtAnd( pTruth, pTruth, Ifn_ObjTruth(p, pFans[f]), p->nWords, 0 );
}
else if ( p->Nodes[i].Type == IF_DSD_XOR )
else if ( p->Nodes[i].Type == IFN_DSD_XOR )
{
Abc_TtClear( pTruth, p->nWords );
for ( f = 0; f < nFans; f++ )
Abc_TtXor( pTruth, pTruth, Ifn_ObjTruth(p, pFans[f]), p->nWords, 0 );
}
else if ( p->Nodes[i].Type == IF_DSD_MUX )
else if ( p->Nodes[i].Type == IFN_DSD_MUX )
{
assert( nFans == 3 );
Abc_TtMux( pTruth, Ifn_ObjTruth(p, pFans[0]), Ifn_ObjTruth(p, pFans[1]), Ifn_ObjTruth(p, pFans[2]), p->nWords );
}
else if ( p->Nodes[i].Type == IF_DSD_PRIME )
else if ( p->Nodes[i].Type == IFN_DSD_PRIME )
{
int nValues = (1 << nFans);
word * pTemp = Ifn_ObjTruth(p, p->nObjs);
@ -573,7 +946,7 @@ int Ifn_NtkAddClauses( Ifn_Ntk_t * p, int * pValues, sat_solver * pSat )
{
int nFans = p->Nodes[i].nFanins;
int * pFans = p->Nodes[i].Fanins;
if ( p->Nodes[i].Type == IF_DSD_AND )
if ( p->Nodes[i].Type == IFN_DSD_AND )
{
nLits = 0;
pLits[nLits++] = Abc_Var2Lit( p->Nodes[i].Var, 0 );
@ -590,7 +963,7 @@ int Ifn_NtkAddClauses( Ifn_Ntk_t * p, int * pValues, sat_solver * pSat )
if ( !Ifn_AddClause( pSat, pLits, pLits + nLits ) )
return 0;
}
else if ( p->Nodes[i].Type == IF_DSD_XOR )
else if ( p->Nodes[i].Type == IFN_DSD_XOR )
{
int m, nMints = (1 << (nFans+1));
for ( m = 0; m < nMints; m++ )
@ -609,7 +982,7 @@ int Ifn_NtkAddClauses( Ifn_Ntk_t * p, int * pValues, sat_solver * pSat )
return 0;
}
}
else if ( p->Nodes[i].Type == IF_DSD_MUX )
else if ( p->Nodes[i].Type == IFN_DSD_MUX )
{
pLits[0] = Abc_Var2Lit( p->Nodes[i].Var, 0 );
pLits[1] = Abc_Var2Lit( p->Nodes[pFans[0]].Var, 1 ); // ctrl
@ -635,7 +1008,7 @@ int Ifn_NtkAddClauses( Ifn_Ntk_t * p, int * pValues, sat_solver * pSat )
if ( !Ifn_AddClause( pSat, pLits, pLits + 3 ) )
return 0;
}
else if ( p->Nodes[i].Type == IF_DSD_PRIME )
else if ( p->Nodes[i].Type == IFN_DSD_PRIME )
{
int nValues = (1 << nFans);
int iParStart = p->Nodes[i].iFirst;
@ -704,7 +1077,7 @@ void Ifn_SatPrintConfig( Ifn_Ntk_t * p, sat_solver * pSat )
for ( v = p->nObjs; v < p->nPars; v++ )
{
for ( i = p->nInps; i < p->nObjs; i++ )
if ( p->Nodes[i].Type == IF_DSD_PRIME && (int)p->Nodes[i].iFirst == v )
if ( p->Nodes[i].Type == IFN_DSD_PRIME && (int)p->Nodes[i].iFirst == v )
break;
if ( i < p->nObjs )
printf( " " );

69
src/misc/util/utilTruth.h
View File

@ -1011,6 +1011,75 @@ static inline int Abc_Tt6SupportAndSize( word t, int nVars, int * pSuppSize )
return Supp;
}
/**Function*************************************************************
Synopsis [Checks if there is a var whose both cofs have supp <= nSuppLim.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
static inline int Abc_TtCheckCondDep2( word * pTruth, int nVars, int nSuppLim )
{
int v, d, nWords = Abc_TtWordNum(nVars);
if ( nVars <= nSuppLim + 1 )
return 0;
for ( v = 0; v < nVars; v++ )
{
int nDep0 = 0, nDep1 = 0;
for ( d = 0; d < nVars; d++ )
{
if ( v == d )
continue;
if ( v < d )
{
nDep0 += !Abc_TtCheckEqualCofs( pTruth, nWords, v, d, 0, 2 );
nDep1 += !Abc_TtCheckEqualCofs( pTruth, nWords, v, d, 1, 3 );
}
else // if ( v > d )
{
nDep0 += !Abc_TtCheckEqualCofs( pTruth, nWords, d, v, 0, 1 );
nDep1 += !Abc_TtCheckEqualCofs( pTruth, nWords, d, v, 2, 3 );
}
if ( nDep0 > nSuppLim || nDep1 > nSuppLim )
break;
}
if ( d == nVars )
return v;
}
return nVars;
}
static inline int Abc_TtCheckCondDep( word * pTruth, int nVars, int nSuppLim )
{
int nVarsMax = 12;
word Cof0[64], Cof1[64]; // pow( 2, nVarsMax-6 )
int v, d, nWords = Abc_TtWordNum(nVars);
assert( nVars <= nVarsMax );
if ( nVars <= nSuppLim + 1 )
return 0;
for ( v = 0; v < nVars; v++ )
{
int nDep0 = 0, nDep1 = 0;
Abc_TtCofactor0p( Cof0, pTruth, nWords, v );
Abc_TtCofactor1p( Cof1, pTruth, nWords, v );
for ( d = 0; d < nVars; d++ )
{
if ( v == d )
continue;
nDep0 += Abc_TtHasVar( Cof0, nVars, d );
nDep1 += Abc_TtHasVar( Cof1, nVars, d );
if ( nDep0 > nSuppLim || nDep1 > nSuppLim )
break;
}
if ( d == nVars )
return v;
}
return nVars;
}
/**Function*************************************************************