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

Adding structural guidance.

This commit is contained in:
Alan Mishchenko 2025-03-18 17:51:40 -07:00
parent 2078b3945b
commit e7dd9151b1
5 changed files with 103 additions and 22 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

53
src/aig/gia/giaSatLut.c
View File

@ -1683,12 +1683,54 @@ int Gia_KSatFindFan( int * pMap, int i, int f, Vec_Int_t * vRes )
return -1;
}
Vec_Str_t * Gia_ManKSatCnf( int * pMap, int nIns, int nNodes, int nBound, int fMultiLevel )
Vec_Int_t * Gia_ManKSatGenLevels( char * pGuide, int nIns, int nNodes )
{
Vec_Int_t * vRes;
int i, k, Count = 0;
for ( i = 0; pGuide[i]; i++ )
Count += pGuide[i] - '0';
if ( Count != nNodes ) {
printf( "Guidance %s has %d nodes while the problem has %d nodes.\n", pGuide, Count, nNodes );
return NULL;
}
int FirstPrev = 0;
int FirstThis = nIns;
int FirstNext = FirstThis;
vRes = Vec_IntStartFull( 2*nIns );
for ( i = 0; pGuide[i]; i++ ) {
FirstNext += pGuide[i] - '0';
for ( k = FirstThis; k < FirstNext; k++ )
Vec_IntPushTwo( vRes, FirstPrev, FirstThis );
FirstPrev = FirstThis;
FirstThis = FirstNext;
}
assert( Vec_IntSize(vRes) == 2*(nIns + nNodes) );
Count = 0;
//int Start, Stop;
//Vec_IntForEachEntryDouble(vRes, Start, Stop, i)
// printf( "%2d : Start %2d Stop %2d\n", Count++, Start, Stop );
return vRes;
}
Vec_Str_t * Gia_ManKSatCnf( int * pMap, int nIns, int nNodes, int nBound, int fMultiLevel, char * pGuide )
{
Vec_Str_t * vStr = Vec_StrAlloc( 10000 );
int i, j, m, n, f, c, a, nLits = 0, pLits[256] = {0};
Vec_Int_t * vRes = pGuide ? Gia_ManKSatGenLevels( pGuide, nIns, nNodes ) : NULL;
int i, j, m, n, f, c, a, Start, Stop, nLits = 0, pLits[256] = {0};
Gia_SatDumpLiteral( vStr, 1 );
Gia_SatDumpLiteral( vStr, 2 );
Gia_SatDumpLiteral( vStr, 2 );
if ( vRes ) {
n = nIns;
Vec_IntForEachEntryDoubleStart( vRes, Start, Stop, i, 2*nIns ) {
for ( j = 0; j < Start; j++ )
Gia_SatDumpLiteral( vStr, Abc_Var2Lit( Gia_KSatVarFan(pMap, n, 1, j), 1 ) );
for ( f = 0; f < 2; f++ )
for ( j = Stop; j < n; j++ )
Gia_SatDumpLiteral( vStr, Abc_Var2Lit( Gia_KSatVarFan(pMap, n, f, j), 1 ) );
n++;
}
assert( n == nIns + nNodes );
}
// fanins are connected once
for ( n = nIns; n < nIns+nNodes; n++ )
for ( f = 0; f < 2; f++ ) {
@ -1854,6 +1896,7 @@ Vec_Str_t * Gia_ManKSatCnf( int * pMap, int nIns, int nNodes, int nBound, int fM
Gia_SatDumpClause( vStr, pLits, nLits );
}
Vec_StrPush( vStr, '\0' );
Vec_IntFreeP( &vRes );
return vStr;
}
@ -2005,7 +2048,7 @@ word Gia_ManGetTruth( Gia_Man_t * p )
return Const[Gia_ObjFaninC0(pObj)] ^ pFuncs[Gia_ObjFaninId0p(p, pObj)];
}
Gia_Man_t * Gia_ManKSatMapping( word Truth, int nIns, int nNodes, int nBound, int Seed, int fMultiLevel, int nBTLimit, int nTimeout, int fVerbose, int fKeepFile, int argc, char ** argv )
Gia_Man_t * Gia_ManKSatMapping( word Truth, int nIns, int nNodes, int nBound, int Seed, int fMultiLevel, int nBTLimit, int nTimeout, int fVerbose, int fKeepFile, int argc, char ** argv, char * pGuide )
{
abctime clkStart = Abc_Clock();
Gia_Man_t * pNew = NULL;
@ -2014,7 +2057,7 @@ Gia_Man_t * Gia_ManKSatMapping( word Truth, int nIns, int nNodes, int nBound, in
char pFileNameI[32]; sprintf( pFileNameI, "_%06x_.cnf", Rand );
char pFileNameO[32]; sprintf( pFileNameO, "_%06x_.out", Rand );
int nVars = 0, * pMap = Gia_KSatMapInit( nIns, nNodes, Truth, &nVars );
Vec_Str_t * vStr = Gia_ManKSatCnf( pMap, nIns, nNodes, nBound/2, fMultiLevel );
Vec_Str_t * vStr = Gia_ManKSatCnf( pMap, nIns, nNodes, nBound/2, fMultiLevel, pGuide );
if ( !Gia_ManDumpCnf(pFileNameI, vStr, nVars) ) {
Vec_StrFree( vStr );
return NULL;

4
src/aig/gia/giaSimBase.c
View File

@ -3199,7 +3199,7 @@ Vec_Int_t * Gia_ManRelDeriveSimple( Gia_Man_t * p, Vec_Wrd_t * vSims, Vec_Int_t
void Gia_ManRelSolve( Gia_Man_t * p, Vec_Wrd_t * vSims, Vec_Int_t * vIns, Vec_Int_t * vOuts, Vec_Int_t * vRel, Vec_Int_t * vDivs )
{
extern Mini_Aig_t * Exa4_ManGenTest( Vec_Wrd_t * vSimsIn, Vec_Wrd_t * vSimsOut, int nIns, int nDivs, int nOuts, int nNodes, int TimeOut, int fOnlyAnd, int fFancy, int fOrderNodes, int fUniqFans, int fVerbose, int fCard );
extern Mini_Aig_t * Exa4_ManGenTest( Vec_Wrd_t * vSimsIn, Vec_Wrd_t * vSimsOut, int nIns, int nDivs, int nOuts, int nNodes, int TimeOut, int fOnlyAnd, int fFancy, int fOrderNodes, int fUniqFans, int fVerbose, int fCard, char * pGuide );
int i, m, iObj, Entry, iMint = 0, nMints = Vec_IntSize(vRel) - Vec_IntCountEntry(vRel, -1);
Vec_Wrd_t * vSimsIn = Vec_WrdStart( nMints );
@ -3232,7 +3232,7 @@ void Gia_ManRelSolve( Gia_Man_t * p, Vec_Wrd_t * vSims, Vec_Int_t * vIns, Vec_In
}
assert( iMint == nMints );
printf( "Created %d minterms.\n", iMint );
Exa4_ManGenTest( vSimsIn, vSimsOut, Vec_IntSize(vIns), Vec_IntSize(vDivs), Vec_IntSize(vOuts), 10, 0, 0, 0, 0, 0, 1, 0 );
Exa4_ManGenTest( vSimsIn, vSimsOut, Vec_IntSize(vIns), Vec_IntSize(vDivs), Vec_IntSize(vOuts), 10, 0, 0, 0, 0, 0, 1, 0, NULL );
Vec_WrdFree( vSimsIn );
Vec_WrdFree( vSimsOut );
}

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

@ -10061,7 +10061,7 @@ int Abc_CommandTwoExact( Abc_Frame_t * pAbc, int argc, char ** argv )
Bmc_EsPar_t Pars, * pPars = &Pars;
Bmc_EsParSetDefault( pPars );
Extra_UtilGetoptReset();
while ( ( c = Extra_UtilGetopt( argc, argv, "INTGabdconugklmvh" ) ) != EOF )
while ( ( c = Extra_UtilGetopt( argc, argv, "INTGSabdconugklmvh" ) ) != EOF )
{
switch ( c )
{
@ -10109,6 +10109,15 @@ int Abc_CommandTwoExact( Abc_Frame_t * pAbc, int argc, char ** argv )
if ( GateSize < 0 )
goto usage;
break;
case 'S':
if ( globalUtilOptind >= argc )
{
Abc_Print( -1, "Command line switch \"-S\" should be followed by a file name.\n" );
goto usage;
}
pPars->pGuide = argv[globalUtilOptind];
globalUtilOptind++;
break;
case 'a':
pPars->fOnlyAnd ^= 1;
break;
@ -10193,12 +10202,13 @@ int Abc_CommandTwoExact( Abc_Frame_t * pAbc, int argc, char ** argv )
return 0;
usage:
Abc_Print( -2, "usage: twoexact [-INTG <num>] [-abdconugklmvh] <hex>\n" );
Abc_Print( -2, "usage: twoexact [-INTG <num>] [-S str] [-abdconugklmvh] <hex>\n" );
Abc_Print( -2, "\t exact synthesis of multi-input function using two-input gates\n" );
Abc_Print( -2, "\t-I <num> : the number of input variables [default = %d]\n", pPars->nVars );
Abc_Print( -2, "\t-N <num> : the number of two-input nodes [default = %d]\n", pPars->nNodes );
Abc_Print( -2, "\t-T <num> : the runtime limit in seconds [default = %d]\n", pPars->RuntimeLim );
Abc_Print( -2, "\t-G <num> : the largest allowed gate size (NANDs only) [default = %d]\n", GateSize );
Abc_Print( -2, "\t-S <str> : structural guidance from the user [default = %s]\n", pPars->pGuide ? pPars->pGuide : "unknown" );
Abc_Print( -2, "\t-a : toggle using only AND-gates (without XOR-gates) [default = %s]\n", pPars->fOnlyAnd ? "yes" : "no" );
Abc_Print( -2, "\t-b : toggle using only NAND-gates [default = %s]\n", fUseNands ? "yes" : "no" );
Abc_Print( -2, "\t-d : toggle using dynamic constraint addition [default = %s]\n", pPars->fDynConstr ? "yes" : "no" );
@ -44559,11 +44569,11 @@ usage:
int Abc_CommandAbc9Exmap( Abc_Frame_t * pAbc, int argc, char ** argv )
{
extern void Mio_IntallSimpleLibrary2();
extern Gia_Man_t * Gia_ManKSatMapping( word Truth, int nIns, int nNodes, int nBound, int Seed, int fMultiLevel, int nBTLimit, int nTimeout, int fVerbose, int fKeepFile, int argc, char ** argv );
Gia_Man_t * pTemp = NULL; char * pTruth = NULL; word Truth = 0;
extern Gia_Man_t * Gia_ManKSatMapping( word Truth, int nIns, int nNodes, int nBound, int Seed, int fMultiLevel, int nBTLimit, int nTimeout, int fVerbose, int fKeepFile, int argc, char ** argv, char * pGuide );
Gia_Man_t * pTemp = NULL; char * pTruth = NULL, * pGuide = NULL; word Truth = 0;
int c, nVars = 0, nNodes = 0, nVars2, Seed = 0, nBTLimit = 0, nBound = 0, fMultiLevel = 0, nTimeout = 0, fKeepFile = 0, fVerbose = 0;
Extra_UtilGetoptReset();
while ( ( c = Extra_UtilGetopt( argc, argv, "NBRCTmfvh" ) ) != EOF )
while ( ( c = Extra_UtilGetopt( argc, argv, "NBRCTSmfvh" ) ) != EOF )
{
switch ( c )
{
@ -44627,6 +44637,15 @@ int Abc_CommandAbc9Exmap( Abc_Frame_t * pAbc, int argc, char ** argv )
nTimeout = atoi(argv[globalUtilOptind]);
globalUtilOptind++;
break;
case 'S':
if ( globalUtilOptind >= argc )
{
Abc_Print( -1, "Command line switch \"-S\" should be followed by a file name.\n" );
goto usage;
}
pGuide = argv[globalUtilOptind];
globalUtilOptind++;
break;
case 'm':
fMultiLevel ^= 1;
break;
@ -44665,7 +44684,7 @@ int Abc_CommandAbc9Exmap( Abc_Frame_t * pAbc, int argc, char ** argv )
}
nVars2 = Abc_TtReadHex( &Truth, pTruth );
assert( nVars2 == nVars );
pTemp = Gia_ManKSatMapping( Truth, nVars, nNodes, nBound, Seed, fMultiLevel, nBTLimit, nTimeout, fVerbose, fKeepFile, argc, argv );
pTemp = Gia_ManKSatMapping( Truth, nVars, nNodes, nBound, Seed, fMultiLevel, nBTLimit, nTimeout, fVerbose, fKeepFile, argc, argv, pGuide );
if ( pTemp ) {
//Mio_IntallSimpleLibrary2();
Abc_FrameUpdateGia( pAbc, pTemp );
@ -44673,13 +44692,14 @@ int Abc_CommandAbc9Exmap( Abc_Frame_t * pAbc, int argc, char ** argv )
return 0;
usage:
Abc_Print( -2, "usage: &exmap [-NBRCT num] [-mfvh] <truth>\n" );
Abc_Print( -2, "usage: &exmap [-NBRCT num] [-S str] [-mfvh] <truth>\n" );
Abc_Print( -2, "\t performs simple mapping of the truth table\n" );
Abc_Print( -2, "\t-N num : the number of nodes [default = %d]\n", nNodes );
Abc_Print( -2, "\t-B num : the bound on the solution size [default = %d]\n", nBound );
Abc_Print( -2, "\t-R num : random number generator seed [default = %d]\n", Seed );
Abc_Print( -2, "\t-C num : the conflict limit [default = %d]\n", nBTLimit );
Abc_Print( -2, "\t-T num : runtime limit in seconds [default = %d]\n", nTimeout );
Abc_Print( -2, "\t-S str : structural guidance from the user [default = %s]\n", pGuide ? pGuide : "unknown" );
Abc_Print( -2, "\t-m : toggles using multi-level primitives [default = %s]\n", fMultiLevel? "yes": "no" );
Abc_Print( -2, "\t-f : toggles keeping the intermediate CNF file [default = %s]\n", fKeepFile? "yes": "no" );
Abc_Print( -2, "\t-v : toggles verbose output [default = %s]\n", fVerbose? "yes": "no" );

1
src/sat/bmc/bmc.h
View File

@ -70,6 +70,7 @@ struct Bmc_EsPar_t_
int fVerbose;
char * pTtStr;
char * pSymStr;
char * pGuide;
};
static inline void Bmc_EsParSetDefault( Bmc_EsPar_t * pPars )

33
src/sat/bmc/bmcMaj.c
View File

@ -1941,9 +1941,25 @@ static inline int Exa4_ManAddClause4( Exa4_Man_t * p, int Lit0, int Lit1, int Li
int pLits[4] = { Lit0, Lit1, Lit2, Lit3 };
return Exa4_ManAddClause( p, pLits, 4 );
}
int Exa4_ManGenStart( Exa4_Man_t * p, int fOnlyAnd, int fFancy, int fOrderNodes, int fUniqFans, int fCard )
int Exa4_ManGenStart( Exa4_Man_t * p, int fOnlyAnd, int fFancy, int fOrderNodes, int fUniqFans, int fCard, char * pGuide )
{
int pLits[2*MAJ_NOBJS], i, j, k, n, m, nLits;
extern Vec_Int_t * Gia_ManKSatGenLevels( char * pGuide, int nIns, int nNodes );
Vec_Int_t * vRes = pGuide ? Gia_ManKSatGenLevels( pGuide, p->nDivs, p->nNodes ) : NULL;
int pLits[2*MAJ_NOBJS], i, j, k, n, m, nLits, Start, Stop;
if ( vRes ) {
n = p->nDivs;
Vec_IntForEachEntryDoubleStart( vRes, Start, Stop, i, 2*p->nDivs ) {
for ( j = 0; j < Start; j++ )
if ( p->VarMarks[n][0][j] )
Exa4_ManAddClause4( p, Abc_Var2Lit( p->VarMarks[n][0][j], 1 ), 0, 0, 0 );
for ( k = 0; k < 2; k++ )
for ( j = Stop; j < n; j++ )
if ( p->VarMarks[n][k][j] )
Exa4_ManAddClause4( p, Abc_Var2Lit( p->VarMarks[n][k][j], 1 ), 0, 0, 0 );
n++;
}
assert( n == p->nDivs + p->nNodes );
}
for ( i = p->nDivs; i < p->nDivs + p->nNodes; i++ )
{
int iVarStart = 1 + 5*(i - p->nDivs);//
@ -2023,6 +2039,7 @@ int Exa4_ManGenStart( Exa4_Man_t * p, int fOnlyAnd, int fFancy, int fOrderNodes,
for ( m = n+1; m < nLits; m++ )
Exa4_ManAddClause4( p, Abc_LitNot(pLits[n]), Abc_LitNot(pLits[m]), 0, 0 );
}
Vec_IntFreeP( &vRes );
return 1;
}
void Exa4_ManGenMint( Exa4_Man_t * p, int iMint, int fOnlyAnd, int fFancy )
@ -2104,13 +2121,13 @@ void Exa4_ManGenMint( Exa4_Man_t * p, int iMint, int fOnlyAnd, int fFancy )
Exa4_ManAddClause4( p, Abc_Var2Lit(p->VarMarks[i][0][j], 1), Abc_LitNotCond(VarVals[j], n), Abc_LitNotCond(VarVals[i], !n), 0);
}
}
void Exa4_ManGenCnf( Exa4_Man_t * p, char * pFileName, int fOnlyAnd, int fFancy, int fOrderNodes, int fUniqFans, int fCard )
void Exa4_ManGenCnf( Exa4_Man_t * p, char * pFileName, int fOnlyAnd, int fFancy, int fOrderNodes, int fUniqFans, int fCard, char * pGuide )
{
int m;
assert( p->pFile == NULL );
p->pFile = fopen( pFileName, "wb" );
fputs( "p cnf \n", p->pFile );
Exa4_ManGenStart( p, fOnlyAnd, fFancy, fOrderNodes, fUniqFans, fCard );
Exa4_ManGenStart( p, fOnlyAnd, fFancy, fOrderNodes, fUniqFans, fCard, pGuide );
for ( m = 1; m < Vec_WrdSize(p->vSimsIn); m++ )
Exa4_ManGenMint( p, m, fOnlyAnd, fFancy );
rewind( p->pFile );
@ -2278,7 +2295,7 @@ Mini_Aig_t * Exa4_ManMiniAig( Exa4_Man_t * p, Vec_Int_t * vValues, int fFancy )
SeeAlso []
***********************************************************************/
Mini_Aig_t * Exa4_ManGenTest( Vec_Wrd_t * vSimsIn, Vec_Wrd_t * vSimsOut, int nIns, int nDivs, int nOuts, int nNodes, int TimeOut, int fOnlyAnd, int fFancy, int fOrderNodes, int fUniqFans, int fVerbose, int fCard )
Mini_Aig_t * Exa4_ManGenTest( Vec_Wrd_t * vSimsIn, Vec_Wrd_t * vSimsOut, int nIns, int nDivs, int nOuts, int nNodes, int TimeOut, int fOnlyAnd, int fFancy, int fOrderNodes, int fUniqFans, int fVerbose, int fCard, char * pGuide )
{
extern Vec_Int_t * Gia_RunKadical( char * pFileNameIn, char * pFileNameOut, int Seed, int nBTLimit, int TimeOut, int fVerbose, int * pStatus );
Mini_Aig_t * pMini = NULL;
@ -2290,7 +2307,7 @@ Mini_Aig_t * Exa4_ManGenTest( Vec_Wrd_t * vSimsIn, Vec_Wrd_t * vSimsOut, int nIn
char pFileNameOut[32]; sprintf( pFileNameOut, "_%05x_.out", Rand );
Exa4_Man_t * p = Exa4_ManAlloc( vSimsIn, vSimsOut, nIns, nDivs, nOuts, nNodes, fVerbose );
Exa_ManIsNormalized( vSimsIn, vSimsOut );
Exa4_ManGenCnf( p, pFileNameIn, fOnlyAnd, fFancy, fOrderNodes, fUniqFans, fCard );
Exa4_ManGenCnf( p, pFileNameIn, fOnlyAnd, fFancy, fOrderNodes, fUniqFans, fCard, pGuide );
if ( fVerbose )
printf( "Timeout = %d. OnlyAnd = %d. Fancy = %d. OrderNodes = %d. UniqueFans = %d. Verbose = %d.\n", TimeOut, fOnlyAnd, fFancy, fOrderNodes, fUniqFans, fVerbose );
if ( fVerbose )
@ -2327,7 +2344,7 @@ void Exa_ManExactSynthesis4_( Bmc_EsPar_t * pPars )
if ( (m >> i) & 1 )
Abc_TtSetBit( Vec_WrdEntryP(vSimsIn, m), 1+i );
}
pMini = Exa4_ManGenTest( vSimsIn, vSimsOut, 3, 4, 2, pPars->nNodes, pPars->RuntimeLim, pPars->fOnlyAnd, pPars->fFewerVars, pPars->fOrderNodes, pPars->fUniqFans, pPars->fVerbose, 0 );
pMini = Exa4_ManGenTest( vSimsIn, vSimsOut, 3, 4, 2, pPars->nNodes, pPars->RuntimeLim, pPars->fOnlyAnd, pPars->fFewerVars, pPars->fOrderNodes, pPars->fUniqFans, pPars->fVerbose, 0, pPars->pGuide );
if ( pMini ) Mini_AigStop( pMini );
Vec_WrdFree( vSimsIn );
Vec_WrdFree( vSimsOut );
@ -2349,7 +2366,7 @@ void Exa_ManExactSynthesis4( Bmc_EsPar_t * pPars )
Abc_TtSetBit( Vec_WrdEntryP(vSimsIn, m), 1+i );
}
assert( Vec_WrdSize(vSimsIn) == (1 << pPars->nVars) );
pMini = Exa4_ManGenTest( vSimsIn, vSimsOut, pPars->nVars, 1+pPars->nVars, 1, pPars->nNodes, pPars->RuntimeLim, pPars->fOnlyAnd, pPars->fFewerVars, pPars->fOrderNodes, pPars->fUniqFans, pPars->fVerbose, pPars->fCard );
pMini = Exa4_ManGenTest( vSimsIn, vSimsOut, pPars->nVars, 1+pPars->nVars, 1, pPars->nNodes, pPars->RuntimeLim, pPars->fOnlyAnd, pPars->fFewerVars, pPars->fOrderNodes, pPars->fUniqFans, pPars->fVerbose, pPars->fCard, pPars->pGuide );
if ( pMini ) Mini_AigStop( pMini );
if ( fCompl ) printf( "The resulting circuit, if computed, will be complemented.\n" );
Vec_WrdFree( vSimsIn );