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 15:08:46 -07:00
parent b05ee94311
commit f989aea224
2 changed files with 98 additions and 33 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

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

@ -86,6 +86,7 @@ struct If_DsdMan_t_
Vec_Ptr_t * vTtDecs[IF_MAX_FUNC_LUTSIZE+1]; // truth table decompositions Vec_Ptr_t * vTtDecs[IF_MAX_FUNC_LUTSIZE+1]; // truth table decompositions
Vec_Wec_t * vIsops[IF_MAX_FUNC_LUTSIZE+1]; // ISOP for each function Vec_Wec_t * vIsops[IF_MAX_FUNC_LUTSIZE+1]; // ISOP for each function
int * pSched[IF_MAX_FUNC_LUTSIZE]; // grey code schedules int * pSched[IF_MAX_FUNC_LUTSIZE]; // grey code schedules
Vec_Wrd_t * vPerms; // permutations
Gia_Man_t * pTtGia; // GIA to represent truth tables Gia_Man_t * pTtGia; // GIA to represent truth tables
Vec_Int_t * vCover; // temporary memory Vec_Int_t * vCover; // temporary memory
void * pSat; // SAT solver void * pSat; // SAT solver
@ -186,6 +187,7 @@ int If_DsdManReadMark( If_DsdMan_t * p, int iDsd )
} }
void If_DsdManSetNewAsUseless( If_DsdMan_t * p ) void If_DsdManSetNewAsUseless( If_DsdMan_t * p )
{ {
if ( p->nObjsPrev == 0 )
p->nObjsPrev = If_DsdManObjNum(p); p->nObjsPrev = If_DsdManObjNum(p);
p->fNewAsUseless = 1; p->fNewAsUseless = 1;
} }
@ -323,6 +325,7 @@ void If_DsdManFree( If_DsdMan_t * p, int fVerbose )
if ( p->vIsops[v] ) if ( p->vIsops[v] )
Vec_WecFree( p->vIsops[v] ); Vec_WecFree( p->vIsops[v] );
} }
Vec_WrdFreeP( &p->vPerms );
Vec_IntFreeP( &p->vTemp1 ); Vec_IntFreeP( &p->vTemp1 );
Vec_IntFreeP( &p->vTemp2 ); Vec_IntFreeP( &p->vTemp2 );
ABC_FREE( p->vObjs.pArray ); ABC_FREE( p->vObjs.pArray );
@ -2357,7 +2360,7 @@ void If_DsdManTune( If_DsdMan_t * p, int LutSize, int fFast, int fAdd, int fSpec
typedef struct Ifn_Ntk_t_ Ifn_Ntk_t; typedef struct Ifn_Ntk_t_ Ifn_Ntk_t;
extern Ifn_Ntk_t * Ifn_NtkParse( char * pStr ); extern Ifn_Ntk_t * Ifn_NtkParse( char * pStr );
extern int Ifn_NtkMatch( Ifn_Ntk_t * p, word * pTruth, int nVars, int nConfls, int fVerbose, int fVeryVerbose ); extern int Ifn_NtkMatch( Ifn_Ntk_t * p, word * pTruth, int nVars, int nConfls, int fVerbose, int fVeryVerbose, word * pPerm );
extern void Ifn_NtkPrint( Ifn_Ntk_t * p ); extern void Ifn_NtkPrint( Ifn_Ntk_t * p );
extern int Ifn_NtkLutSizeMax( Ifn_Ntk_t * p ); extern int Ifn_NtkLutSizeMax( Ifn_Ntk_t * p );
extern int Ifn_NtkInputNum( Ifn_Ntk_t * p ); extern int Ifn_NtkInputNum( Ifn_Ntk_t * p );
@ -2378,7 +2381,7 @@ void Id_DsdManTuneStr1( If_DsdMan_t * p, char * pStruct, int nConfls, int fVerbo
int fVeryVerbose = 0; int fVeryVerbose = 0;
ProgressBar * pProgress = NULL; ProgressBar * pProgress = NULL;
If_DsdObj_t * pObj; If_DsdObj_t * pObj;
word * pTruth; word * pTruth, Perm;
int i, nVars, Value, LutSize; int i, nVars, Value, LutSize;
abctime clk = Abc_Clock(); abctime clk = Abc_Clock();
// parse the structure // parse the structure
@ -2407,6 +2410,10 @@ void Id_DsdManTuneStr1( If_DsdMan_t * p, char * pStruct, int nConfls, int fVerbo
If_DsdVecForEachObj( &p->vObjs, pObj, i ) If_DsdVecForEachObj( &p->vObjs, pObj, i )
if ( i >= p->nObjsPrev ) if ( i >= p->nObjsPrev )
pObj->fMark = 0; pObj->fMark = 0;
if ( p->vPerms == NULL )
p->vPerms = Vec_WrdStart( Vec_PtrSize(&p->vObjs) );
else
Vec_WrdFillExtra( p->vPerms, Vec_PtrSize(&p->vObjs), 0 );
pProgress = Extra_ProgressBarStart( stdout, Vec_PtrSize(&p->vObjs) ); pProgress = Extra_ProgressBarStart( stdout, Vec_PtrSize(&p->vObjs) );
If_DsdVecForEachObjStart( &p->vObjs, pObj, i, p->nObjsPrev ) If_DsdVecForEachObjStart( &p->vObjs, pObj, i, p->nObjsPrev )
{ {
@ -2420,11 +2427,13 @@ void Id_DsdManTuneStr1( If_DsdMan_t * p, char * pStruct, int nConfls, int fVerbo
Dau_DsdPrintFromTruth( pTruth, nVars ); Dau_DsdPrintFromTruth( pTruth, nVars );
if ( fVerbose ) if ( fVerbose )
printf( "%6d : %2d ", i, nVars ); printf( "%6d : %2d ", i, nVars );
Value = Ifn_NtkMatch( pNtk, pTruth, nVars, nConfls, fVerbose, fVeryVerbose ); Value = Ifn_NtkMatch( pNtk, pTruth, nVars, nConfls, fVerbose, fVeryVerbose, &Perm );
if ( fVeryVerbose ) if ( fVeryVerbose )
printf( "\n" ); printf( "\n" );
if ( Value == 0 ) if ( Value == 0 )
If_DsdVecObjSetMark( &p->vObjs, i ); If_DsdVecObjSetMark( &p->vObjs, i );
else
Vec_WrdWriteEntry( p->vPerms, i, Perm );
} }
p->nObjsPrev = 0; p->nObjsPrev = 0;
Extra_ProgressBarStop( pProgress ); Extra_ProgressBarStop( pProgress );
@ -2465,6 +2474,7 @@ typedef struct Ifn_ThData_t_
int nConfls; // conflicts int nConfls; // conflicts
int Result; // result int Result; // result
int Status; // state int Status; // state
word Perm; // permutation
abctime clkUsed; // total runtime abctime clkUsed; // total runtime
} Ifn_ThData_t; } Ifn_ThData_t;
void * Ifn_WorkerThread( void * pArg ) void * Ifn_WorkerThread( void * pArg )
@ -2483,7 +2493,7 @@ void * Ifn_WorkerThread( void * pArg )
return NULL; return NULL;
} }
clk = Abc_Clock(); clk = Abc_Clock();
pThData->Result = Ifn_NtkMatch( pThData->pNtk, pThData->pTruth, pThData->nVars, pThData->nConfls, 0, 0 ); pThData->Result = Ifn_NtkMatch( pThData->pNtk, pThData->pTruth, pThData->nVars, pThData->nConfls, 0, 0, &pThData->Perm );
pThData->clkUsed += Abc_Clock() - clk; pThData->clkUsed += Abc_Clock() - clk;
pThData->Status = 0; pThData->Status = 0;
// printf( "Finished object %d\n", pThData->Id ); // printf( "Finished object %d\n", pThData->Id );
@ -2536,6 +2546,10 @@ void Id_DsdManTuneStr( If_DsdMan_t * p, char * pStruct, int nConfls, int nProcs,
If_DsdVecForEachObj( &p->vObjs, pObj, i ) If_DsdVecForEachObj( &p->vObjs, pObj, i )
if ( i >= p->nObjsPrev ) if ( i >= p->nObjsPrev )
pObj->fMark = 0; pObj->fMark = 0;
if ( p->vPerms == NULL )
p->vPerms = Vec_WrdStart( Vec_PtrSize(&p->vObjs) );
else
Vec_WrdFillExtra( p->vPerms, Vec_PtrSize(&p->vObjs), 0 );
pProgress = Extra_ProgressBarStart( stdout, Vec_PtrSize(&p->vObjs) ); pProgress = Extra_ProgressBarStart( stdout, Vec_PtrSize(&p->vObjs) );
// perform concurrent solving // perform concurrent solving
@ -2570,6 +2584,8 @@ void Id_DsdManTuneStr( If_DsdMan_t * p, char * pStruct, int nConfls, int nProcs,
assert( ThData[i].Result == 0 || ThData[i].Result == 1 ); assert( ThData[i].Result == 0 || ThData[i].Result == 1 );
if ( ThData[i].Result == 0 ) if ( ThData[i].Result == 0 )
If_DsdVecObjSetMark( &p->vObjs, ThData[i].Id ); If_DsdVecObjSetMark( &p->vObjs, ThData[i].Id );
else
Vec_WrdWriteEntry( p->vPerms, ThData[i].Id, ThData[i].Perm );
ThData[i].Id = -1; ThData[i].Id = -1;
ThData[i].Result = -1; ThData[i].Result = -1;
} }

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

@ -540,7 +540,7 @@ Gia_Man_t * Ifn_ManStrFindCofactors( int nIns, Gia_Man_t * p )
{ {
Gia_Man_t * pNew, * pTemp; Gia_Man_t * pNew, * pTemp;
Gia_Obj_t * pObj; Gia_Obj_t * pObj;
int i, m, nMints = nIns; int i, m, nMints = 1 << nIns;
pNew = Gia_ManStart( Gia_ManObjNum(p) ); pNew = Gia_ManStart( Gia_ManObjNum(p) );
pNew->pName = Abc_UtilStrsav( p->pName ); pNew->pName = Abc_UtilStrsav( p->pName );
Gia_ManHashAlloc( pNew ); Gia_ManHashAlloc( pNew );
@ -640,17 +640,17 @@ void Ifn_ManSatPrintPerm( char * pPerms, int nVars )
printf( "%c", 'a' + pPerms[i] ); printf( "%c", 'a' + pPerms[i] );
printf( "\n" ); 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 Ifn_ManSatCheckOne( sat_solver * pSat, Vec_Int_t * vPoVars, word * pTruth, int nVars, int * pPerm, int nInps, Vec_Int_t * vLits )
{ {
int v, Value, m, mNew, nMints = (1 << nVars); int v, Value, m, mNew, nMints = (1 << nVars);
assert( (1 << nVarsAll) == Vec_IntSize(vPoVars) ); assert( (1 << nInps) == Vec_IntSize(vPoVars) );
assert( nVars <= nVarsAll ); assert( nVars <= nInps );
// remap minterms // remap minterms
Vec_IntFill( vLits, Vec_IntSize(vPoVars), -1 ); Vec_IntFill( vLits, Vec_IntSize(vPoVars), -1 );
for ( m = 0; m < nMints; m++ ) for ( m = 0; m < nMints; m++ )
{ {
mNew = 0; mNew = 0;
for ( v = 0; v < nVarsAll; v++ ) for ( v = 0; v < nInps; v++ )
{ {
assert( pPerm[v] < nVars ); assert( pPerm[v] < nVars );
if ( ((m >> pPerm[v]) & 1) ) if ( ((m >> pPerm[v]) & 1) )
@ -676,23 +676,38 @@ void Ifn_ManSatDeriveOne( sat_solver * pSat, Vec_Int_t * vPiVars, Vec_Int_t * vV
Vec_IntForEachEntry( vPiVars, iVar, i ) Vec_IntForEachEntry( vPiVars, iVar, i )
Vec_IntPush( vValues, sat_solver_var_value(pSat, iVar) ); 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 ) int Ifn_ManSatFindCofigBits( sat_solver * pSat, Vec_Int_t * vPiVars, Vec_Int_t * vPoVars, word * pTruth, int nVars, word Perm, int nInps, Vec_Int_t * vValues )
{ {
// extract permutation // extract permutation
int RetValue, i, pPerm[IF_MAX_FUNC_LUTSIZE]; int RetValue, i, pPerm[IF_MAX_FUNC_LUTSIZE];
for ( i = 0; i < Vec_IntSize(vPiVars); i++ ) assert( nInps <= IF_MAX_FUNC_LUTSIZE );
for ( i = 0; i < nInps; i++ )
{ {
pPerm[i] = Abc_TtGetHex( &Perm, i ); pPerm[i] = Abc_TtGetHex( &Perm, i );
assert( pPerm[i] < nVars ); assert( pPerm[i] < nVars );
} }
// perform SAT check // perform SAT check
RetValue = Ifn_ManSatCheckOne( pSat, vPoVars, pTruth, nVars, pPerm, Vec_IntSize(vPiVars), vValues ); RetValue = Ifn_ManSatCheckOne( pSat, vPoVars, pTruth, nVars, pPerm, nInps, vValues );
Vec_IntClear( vValues ); Vec_IntClear( vValues );
if ( RetValue == 0 ) if ( RetValue == 0 )
return 0; return 0;
Ifn_ManSatDeriveOne( pSat, vPiVars, vValues ); Ifn_ManSatDeriveOne( pSat, vPiVars, vValues );
return 1; return 1;
} }
int Ifn_ManSatFindCofigBitsTest( Ifn_Ntk_t * p, word * pTruth, int nVars, word Perm )
{
Vec_Int_t * vValues = Vec_IntAlloc( 100 );
Vec_Int_t * vPiVars, * vPoVars;
sat_solver * pSat = Ifn_ManSatBuild( p, &vPiVars, &vPoVars );
int RetValue = Ifn_ManSatFindCofigBits( pSat, vPiVars, vPoVars, pTruth, nVars, Perm, p->nInps, vValues );
Vec_IntPrint( vValues );
// cleanup
sat_solver_delete( pSat );
Vec_IntFreeP( &vPiVars );
Vec_IntFreeP( &vPoVars );
Vec_IntFreeP( &vValues );
return RetValue;
}
/**Function************************************************************* /**Function*************************************************************
@ -1055,7 +1070,7 @@ int Ifn_NtkAddClauses( Ifn_Ntk_t * p, int * pValues, sat_solver * pSat )
SeeAlso [] SeeAlso []
***********************************************************************/ ***********************************************************************/
void Ifn_SatPrintStatus( sat_solver * p, int Iter, int status, int iMint, int Value, abctime clk ) void Ifn_NtkMatchPrintStatus( sat_solver * p, int Iter, int status, int iMint, int Value, abctime clk )
{ {
printf( "Iter = %5d ", Iter ); printf( "Iter = %5d ", Iter );
printf( "Mint = %5d ", iMint ); printf( "Mint = %5d ", iMint );
@ -1069,9 +1084,9 @@ void Ifn_SatPrintStatus( sat_solver * p, int Iter, int status, int iMint, int Va
printf( "status = sat " ); printf( "status = sat " );
else else
printf( "status = undec" ); printf( "status = undec" );
Abc_PrintTime( 1, "", clk ); Abc_PrintTime( 1, "Time", clk );
} }
void Ifn_SatPrintConfig( Ifn_Ntk_t * p, sat_solver * pSat ) void Ifn_NtkMatchPrintConfig( Ifn_Ntk_t * p, sat_solver * pSat )
{ {
int v, i; int v, i;
for ( v = p->nObjs; v < p->nPars; v++ ) for ( v = p->nObjs; v < p->nPars; v++ )
@ -1086,8 +1101,29 @@ void Ifn_SatPrintConfig( Ifn_Ntk_t * p, sat_solver * pSat )
printf( "%d", sat_solver_var_value(pSat, v) ); printf( "%d", sat_solver_var_value(pSat, v) );
} }
} }
word Ifn_NtkMatchCollectPerm( Ifn_Ntk_t * p, sat_solver * pSat )
int Ifn_NtkMatch( Ifn_Ntk_t * p, word * pTruth, int nVars, int nConfls, int fVerbose, int fVeryVerbose ) {
word Perm = 0;
int i, v, Mint;
assert( p->nParsVNum <= 4 );
for ( i = 0; i < p->nInps; i++ )
{
for ( Mint = v = 0; v < p->nParsVNum; v++ )
if ( sat_solver_var_value(pSat, p->nParsVIni + i * p->nParsVNum + v) )
Mint |= (1 << v);
Abc_TtSetHex( &Perm, i, Mint );
}
return Perm;
}
void Ifn_NtkMatchPrintPerm( word Perm, int nInps )
{
int i;
assert( nInps <= 16 );
for ( i = 0; i < nInps; i++ )
printf( "%c", 'a' + Abc_TtGetHex(&Perm, i) );
printf( "\n" );
}
int Ifn_NtkMatch( Ifn_Ntk_t * p, word * pTruth, int nVars, int nConfls, int fVerbose, int fVeryVerbose, word * pPerm )
{ {
word * pTruth1; word * pTruth1;
int RetValue = 0; int RetValue = 0;
@ -1100,7 +1136,8 @@ int Ifn_NtkMatch( Ifn_Ntk_t * p, word * pTruth, int nVars, int nConfls, int fVer
sat_solver_setnvars( pSat, p->nPars ); sat_solver_setnvars( pSat, p->nPars );
Ifn_NtkAddConstraints( p, pSat ); Ifn_NtkAddConstraints( p, pSat );
if ( fVeryVerbose ) if ( fVeryVerbose )
Ifn_SatPrintStatus( pSat, 0, l_True, -1, -1, Abc_Clock() - clk ); Ifn_NtkMatchPrintStatus( pSat, 0, l_True, -1, -1, Abc_Clock() - clk );
if ( pPerm ) *pPerm = 0;
for ( i = 0; i < nIterMax; i++ ) for ( i = 0; i < nIterMax; i++ )
{ {
// get variable assignment // get variable assignment
@ -1115,7 +1152,7 @@ int Ifn_NtkMatch( Ifn_Ntk_t * p, word * pTruth, int nVars, int nConfls, int fVer
status = sat_solver_solve( pSat, NULL, NULL, nConfls, 0, 0, 0 ); status = sat_solver_solve( pSat, NULL, NULL, nConfls, 0, 0, 0 );
// clkSat += Abc_Clock() - clk2; // clkSat += Abc_Clock() - clk2;
if ( fVeryVerbose ) if ( fVeryVerbose )
Ifn_SatPrintStatus( pSat, i+1, status, iMint, p->Values[p->nObjs-1], Abc_Clock() - clk ); Ifn_NtkMatchPrintStatus( pSat, i+1, status, iMint, p->Values[p->nObjs-1], Abc_Clock() - clk );
if ( status != l_True ) if ( status != l_True )
break; break;
// collect assignment // collect assignment
@ -1130,6 +1167,17 @@ int Ifn_NtkMatch( Ifn_Ntk_t * p, word * pTruth, int nVars, int nConfls, int fVer
iMint = Abc_TtFindFirstBit( pTruth1, p->nVars ); iMint = Abc_TtFindFirstBit( pTruth1, p->nVars );
if ( iMint == -1 ) if ( iMint == -1 )
{ {
if ( pPerm )
*pPerm = Ifn_NtkMatchCollectPerm( p, pSat );
/*
if ( pPerm )
{
int RetValue = Ifn_ManSatFindCofigBitsTest( p, pTruth, nVars, *pPerm );
Ifn_NtkMatchPrintPerm( *pPerm, p->nInps );
if ( RetValue == 0 )
printf( "Verification failed.\n" );
}
*/
RetValue = 1; RetValue = 1;
break; break;
} }
@ -1139,7 +1187,7 @@ int Ifn_NtkMatch( Ifn_Ntk_t * p, word * pTruth, int nVars, int nConfls, int fVer
{ {
printf( "%s Iter =%4d. Confl = %6d. ", RetValue ? "yes":"no ", i, sat_solver_nconflicts(pSat) ); printf( "%s Iter =%4d. Confl = %6d. ", RetValue ? "yes":"no ", i, sat_solver_nconflicts(pSat) );
if ( RetValue ) if ( RetValue )
Ifn_SatPrintConfig( p, pSat ); Ifn_NtkMatchPrintConfig( p, pSat );
printf( "\n" ); printf( "\n" );
} }
sat_solver_delete( pSat ); sat_solver_delete( pSat );
@ -1163,29 +1211,30 @@ int Ifn_NtkMatch( Ifn_Ntk_t * p, word * pTruth, int nVars, int nConfls, int fVer
void Ifn_NtkRead() void Ifn_NtkRead()
{ {
int RetValue; int RetValue;
int nVars = 9; int nVars = 8;
// int nVars = 8;
// int nVars = 3;
// word * pTruth = Dau_DsdToTruth( "(abcdefghi)", nVars ); // word * pTruth = Dau_DsdToTruth( "(abcdefghi)", nVars );
word * pTruth = Dau_DsdToTruth( "1008{(1008{(ab)cde}f)ghi}", nVars ); word * pTruth = Dau_DsdToTruth( "1008{(1008{(ab)cde}f)ghi}", nVars );
// word * pTruth = Dau_DsdToTruth( "18{(1008{(ab)cde}f)gh}", nVars ); // word * pTruth = Dau_DsdToTruth( "18{(1008{(ab)cde}f)gh}", nVars );
// word * pTruth = Dau_DsdToTruth( "1008{(1008{[ab]cde}f)ghi}", nVars ); // word * pTruth = Dau_DsdToTruth( "1008{(1008{[ab]cde}f)ghi}", nVars );
// word * pTruth = Dau_DsdToTruth( "(abcd)", nVars ); // word * pTruth = Dau_DsdToTruth( "(abcd)", nVars );
// word * pTruth = Dau_DsdToTruth( "(abc)", nVars ); // word * pTruth = Dau_DsdToTruth( "(abc)", nVars );
// word * pTruth = Dau_DsdToTruth( "18{(1008{(ab)cde}f)gh}", nVars );
// char * pStr = "e={abc};f={ed};"; // char * pStr = "e={abc};f={ed};";
// char * pStr = "d={ab};e={cd};"; // char * pStr = "d={ab};e={cd};";
// char * pStr = "j=(ab);k={jcde};l=(kf);m={lghi};"; // char * pStr = "j=(ab);k={jcde};l=(kf);m={lghi};";
// char * pStr = "i={abc};j={ide};k={ifg};l={jkh};"; // char * pStr = "i={abc};j={ide};k={ifg};l={jkh};";
// char * pStr = "h={abcde};i={abcdf};j=<ghi>;"; // char * pStr = "h={abcde};i={abcdf};j=<ghi>;";
// char * pStr = "g=<abc>;h=<ade>;i={fgh};"; // char * pStr = "g=<abc>;h=<ade>;i={fgh};";
char * pStr = "i=<abc>;j=(def);k=[gh];l={ijk};"; // char * pStr = "i=<abc>;j=(def);k=[gh];l={ijk};";
char * pStr = "{({(ab)cde}f)ghi};AB;CD;DE;GH;HI";
Ifn_Ntk_t * p = Ifn_NtkParse( pStr ); Ifn_Ntk_t * p = Ifn_NtkParse( pStr );
word Perm = 0;
if ( p == NULL ) if ( p == NULL )
return; return;
Ifn_NtkPrint( p ); Ifn_NtkPrint( p );
Dau_DsdPrintFromTruth( pTruth, nVars ); Dau_DsdPrintFromTruth( pTruth, nVars );
// get the given function // get the given function
RetValue = Ifn_NtkMatch( p, pTruth, nVars, 0, 1, 1 ); RetValue = Ifn_NtkMatch( p, pTruth, nVars, 0, 1, 1, &Perm );
ABC_FREE( p ); ABC_FREE( p );
} }