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

Merge remote-tracking branch 'upstream/master' into yosys-experimental

This commit is contained in:
Miodrag Milanovic 2026-06-08 12:54:10 +02:00
parent 5d51a5e420 59896d6ec8
commit 3df13d9aad
20 changed files with 1479 additions and 170 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

103
src/aig/gia/giaGen.c
View File

@ -1446,23 +1446,76 @@ void Gia_ManGenPrefix( Gia_Man_t * pNew, int * p, int * g, int p2, int g2 )
*g = Gia_ManHashOr(pNew, *g, Gia_ManHashAnd(pNew, *p, g2));
*p = Gia_ManHashAnd(pNew, *p, p2);
}
Gia_Man_t * Gia_ManGenAdder( int nVars, int fSK, int fBK, int fHC, int fCarries, int fVerbose )
static int Gia_ManGenAdderMaj( Gia_Man_t * p, int a, int b, int c )
{
int ab = Gia_ManHashAnd( p, a, b );
int ac = Gia_ManHashAnd( p, a, c );
int bc = Gia_ManHashAnd( p, b, c );
return Gia_ManHashOr( p, ab, Gia_ManHashOr( p, ac, bc ) );
}
static int Gia_ManGenAdderFloorPow2( int n )
{
int r = 1;
assert( n > 0 );
while ( r <= n / 2 )
r *= 2;
return r;
}
static void Gia_ManGenAdderMMRange( Gia_Man_t * p, int nVars, int * pLitsI, int * pM0, int * pM1, int i, int k )
{
int Index = i * nVars + k;
int nRange, nLeft, j;
assert( 0 <= i && i <= k && k < nVars );
if ( pM0[Index] >= 0 )
return;
if ( i == k )
{
pM0[Index] = pLitsI[2*i];
pM1[Index] = pLitsI[2*i+1];
return;
}
nRange = k - i + 1;
nLeft = Gia_ManGenAdderFloorPow2( nRange - 1 );
j = i + nLeft - 1;
Gia_ManGenAdderMMRange( p, nVars, pLitsI, pM0, pM1, i, j );
Gia_ManGenAdderMMRange( p, nVars, pLitsI, pM0, pM1, j+1, k );
pM0[Index] = Gia_ManGenAdderMaj( p, pM0[(j+1)*nVars+k], pM1[(j+1)*nVars+k], pM0[i*nVars+j] );
pM1[Index] = Gia_ManGenAdderMaj( p, pM0[(j+1)*nVars+k], pM1[(j+1)*nVars+k], pM1[i*nVars+j] );
}
static int Gia_ManGenAdderMMCarry( Gia_Man_t * p, int nVars, int * pLitsI, int * pM0, int * pM1, int * pCarries, int iCarry )
{
int nBase, iBeg;
assert( 0 <= iCarry && iCarry <= nVars );
if ( pCarries[iCarry] >= 0 )
return pCarries[iCarry];
nBase = Gia_ManGenAdderFloorPow2( iCarry );
iBeg = nBase - 1;
Gia_ManGenAdderMMRange( p, nVars, pLitsI, pM0, pM1, iBeg, iCarry-1 );
pCarries[iCarry] = Gia_ManGenAdderMaj( p, pM0[iBeg*nVars+iCarry-1], pM1[iBeg*nVars+iCarry-1], Gia_ManGenAdderMMCarry( p, nVars, pLitsI, pM0, pM1, pCarries, iBeg ) );
return pCarries[iCarry];
}
Gia_Man_t * Gia_ManGenAdder( int nVars, int fSK, int fBK, int fHC, int fMM, int fCarries, int fVerbose )
{
extern void Wlc_BlastFullAdder( Gia_Man_t * pNew, int a, int b, int c, int * pc, int * ps );
int i, k, nBits = Abc_Base2Log(nVars), nVarsAlloc = (1 << nBits) + 2;
int ** pStore = (int **)Extra_ArrayAlloc( nVarsAlloc, nVarsAlloc, 4 );
int ** pStore = fMM ? NULL : (int **)Extra_ArrayAlloc( nVarsAlloc, nVarsAlloc, 4 );
printf( "Generating %d-bit ", nVars );
Gia_ManGenPrep( nVars+2, pStore );
if ( fSK )
Gia_ManGenSK( nVars, pStore ), printf("Sklansky ");
else if ( fBK )
Gia_ManGenBK( nVars, pStore ), printf("Brent-Kung ");
else if ( fHC )
Gia_ManGenHC( nVars, pStore ), printf("Huan-Carlsson ");
if ( fMM )
printf("M/M ");
else
Gia_ManGenRca( nVars, pStore ), printf("ripple-carry ");
{
Gia_ManGenPrep( nVars+2, pStore );
if ( fSK )
Gia_ManGenSK( nVars, pStore ), printf("Sklansky ");
else if ( fBK )
Gia_ManGenBK( nVars, pStore ), printf("Brent-Kung ");
else if ( fHC )
Gia_ManGenHC( nVars, pStore ), printf("Huan-Carlsson ");
else
Gia_ManGenRca( nVars, pStore ), printf("ripple-carry ");
}
printf( "adder with%s carry-in and carry-out\n", fCarries ? "":"out" );
if ( fVerbose ) Gia_ManGenPrint( nVars, pStore );
if ( fVerbose && !fMM ) Gia_ManGenPrint( nVars, pStore );
Gia_Man_t * p = Gia_ManStart( 1000 ), * pTemp;
p->pName = Abc_UtilStrsav( "adder" );
int * pLitsI = ABC_CALLOC( int, 2*nVars+10 );
@ -1472,6 +1525,33 @@ Gia_Man_t * Gia_ManGenAdder( int nVars, int fSK, int fBK, int fHC, int fCarries,
pLitsI[2*k+1] = Gia_ManAppendCi(p);
int Carry = fCarries ? Gia_ManAppendCi(p) : 0;
Gia_ManHashStart( p );
if ( fMM )
{
int nPairs = nVars * nVars;
int * pM0 = ABC_ALLOC( int, nPairs );
int * pM1 = ABC_ALLOC( int, nPairs );
int * pCarries = ABC_ALLOC( int, nVars + 1 );
int * pProps = ABC_ALLOC( int, nVars );
for ( k = 0; k < nPairs; k++ )
pM0[k] = pM1[k] = -1;
for ( k = 0; k <= nVars; k++ )
pCarries[k] = -1;
pCarries[0] = Carry;
for ( k = 0; k < nVars; k++ )
pProps[k] = Gia_ManHashXor( p, pLitsI[2*k], pLitsI[2*k+1] );
if ( fCarries )
Gia_ManAppendCo( p, Gia_ManGenAdderMMCarry( p, nVars, pLitsI, pM0, pM1, pCarries, nVars ) );
for ( k = 0; k < nVars; k++ )
Gia_ManAppendCo( p, Gia_ManHashXor( p, pProps[k], Gia_ManGenAdderMMCarry( p, nVars, pLitsI, pM0, pM1, pCarries, k ) ) );
ABC_FREE( pM0 );
ABC_FREE( pM1 );
ABC_FREE( pCarries );
ABC_FREE( pProps );
ABC_FREE( pLitsI );
p = Gia_ManCleanup( pTemp = p );
Gia_ManStop( pTemp );
return p;
}
for ( k = 0; k < nVars; k++ )
Wlc_BlastFullAdder( p, pLitsI[2*k], pLitsI[2*k+1], k ? 0 : Carry, &pLitsI[2*k+1], &pLitsI[2*k] );
int * pLits = ABC_CALLOC( int, 2*nVars+10 );
@ -1498,4 +1578,3 @@ Gia_Man_t * Gia_ManGenAdder( int nVars, int fSK, int fBK, int fHC, int fCarries,
ABC_NAMESPACE_IMPL_END

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

@ -10603,19 +10603,391 @@ usage:
SeeAlso []
***********************************************************************/
static int Abc_TwoExactPermAddFanin( int * pFans, int iNode, int iFanin )
{
int * pNode = pFans + 2 * iNode;
if ( pNode[0] == iFanin || pNode[1] == iFanin )
return 0;
if ( pNode[0] == -1 && pNode[1] == -1 )
pNode[Abc_Random(0) & 1] = iFanin;
else if ( pNode[0] == -1 )
pNode[0] = iFanin;
else if ( pNode[1] == -1 )
pNode[1] = iFanin;
else
return 0;
return 1;
}
static int Abc_TwoExactPermAddRequired( int * pFans, int nVars, int nNodes, int iFanin )
{
int iNodeStart = (iFanin + 1 > nVars) ? iFanin + 1 - nVars : 0;
int i, nChoices = 0, iChoice = -1;
for ( i = iNodeStart; i < nNodes; i++ )
{
int * pNode = pFans + 2 * i;
if ( pNode[0] == iFanin || pNode[1] == iFanin )
continue;
if ( pNode[0] != -1 && pNode[1] != -1 )
continue;
if ( Abc_Random(0) % ++nChoices == 0 )
iChoice = i;
}
return iChoice >= 0 && Abc_TwoExactPermAddFanin( pFans, iChoice, iFanin );
}
static int Abc_TwoExactPermCountDistinct( int * pFans, int nVars, int iNode )
{
int iPrevObj = nVars + iNode - 1;
int pVals[4], nVals = 0, i, k;
assert( iNode > 0 );
for ( i = iNode - 1; i <= iNode; i++ )
for ( k = 0; k < 2; k++ )
{
int v = pFans[2 * i + k];
int j, fSeen = 0;
if ( v == iPrevObj )
continue;
for ( j = 0; j < nVals; j++ )
fSeen |= pVals[j] == v;
if ( !fSeen )
pVals[nVals++] = v;
}
return nVals;
}
static int Abc_TwoExactPermCheck( int * pFans, int nVars, int nNodes, int fStrict )
{
int nObjs = nVars + nNodes;
int * pUsed = ABC_CALLOC( int, nObjs );
int i, RetValue = 1;
for ( i = 0; i < nNodes; i++ )
{
if ( pFans[2*i] < 0 || pFans[2*i+1] < 0 || pFans[2*i] >= nVars + i || pFans[2*i+1] >= nVars + i || pFans[2*i] == pFans[2*i+1] )
RetValue = 0;
if ( fStrict && i > 0 && Abc_TwoExactPermCountDistinct(pFans, nVars, i) < 3 )
RetValue = 0;
if ( !RetValue )
break;
pUsed[pFans[2*i]]++;
pUsed[pFans[2*i+1]]++;
}
if ( RetValue )
for ( i = 0; i < nObjs - 1; i++ )
if ( pUsed[i] == 0 )
{
RetValue = 0;
break;
}
ABC_FREE( pUsed );
return RetValue;
}
static char * Abc_TwoExactPermEncode( int * pFans, int nVars, int nNodes )
{
char * pPerm = ABC_ALLOC( char, 3 * nNodes );
int i, k, Pos = 0;
for ( i = 0; i < nNodes; i++ )
{
if ( i )
pPerm[Pos++] = '_';
for ( k = 0; k < 2; k++ )
pPerm[Pos++] = pFans[2*i+k] >= 0 && pFans[2*i+k] < nVars ? 'a' + pFans[2*i+k] : '*';
}
pPerm[Pos] = 0;
return pPerm;
}
static char * Abc_TwoExactObjName( int iObj, int nVars, char * pBuffer )
{
if ( iObj < 0 )
sprintf( pBuffer, "*" );
else if ( iObj < nVars )
sprintf( pBuffer, "%c", 'a' + iObj );
else if ( iObj - nVars < 26 )
sprintf( pBuffer, "%c", 'A' + iObj - nVars );
else
sprintf( pBuffer, "N%d", iObj - nVars );
return pBuffer;
}
static char * Abc_TwoExactPermEncodeFull( int * pFans, int nVars, int nNodes )
{
int nSize = 8 * (nNodes + 1);
char * pPerm = ABC_ALLOC( char, nSize );
int i, k, Pos = 0;
char Name[16];
for ( i = 0; i < nNodes; i++ )
{
if ( i )
pPerm[Pos++] = '_';
for ( k = 0; k < 2; k++ )
Pos += sprintf( pPerm + Pos, "%s", Abc_TwoExactObjName(pFans[2*i+k], nVars, Name) );
}
pPerm[Pos] = 0;
return pPerm;
}
static int Abc_TwoExactPermParseObj( char ** ppToken, int nVars, int nNodes, int * pObj )
{
char * pToken = *ppToken;
if ( *pToken == '*' )
{
*pObj = -1;
*ppToken = pToken + 1;
return 1;
}
if ( *pToken >= 'a' && *pToken < 'a' + nVars )
{
*pObj = *pToken - 'a';
*ppToken = pToken + 1;
return 1;
}
if ( *pToken >= 'A' && *pToken <= 'Z' )
{
*pObj = nVars + *pToken - 'A';
*ppToken = pToken + 1;
return *pObj < nVars + nNodes;
}
if ( *pToken == 'N' )
{
char * pNext = pToken + 1;
int Num = 0;
if ( *pNext < '0' || *pNext > '9' )
return 0;
while ( *pNext >= '0' && *pNext <= '9' )
Num = 10 * Num + *pNext++ - '0';
*pObj = nVars + Num;
*ppToken = pNext;
return *pObj < nVars + nNodes;
}
return 0;
}
static int Abc_TwoExactPermAddDcs( int * pFans, int nVars, int nNodes, int nDcs, int nSkip, int fAll )
{
int i, k, nLetters = 0;
if ( nDcs == 0 )
return 1;
for ( i = nSkip; i < 2 * nNodes; i++ )
nLetters += pFans[i] >= 0 && (fAll || pFans[i] < nVars);
if ( nDcs > nLetters )
return 0;
for ( k = 0; k < nDcs; k++ )
{
int iChoice = -1, nChoices = 0;
for ( i = nSkip; i < 2 * nNodes; i++ )
if ( pFans[i] >= 0 && (fAll || pFans[i] < nVars) && Abc_Random(0) % ++nChoices == 0 )
iChoice = i;
assert( iChoice >= 0 );
pFans[iChoice] = -1;
}
return 1;
}
static int * Abc_TwoExactPermRandom( int nVars, int nNodes, int nDcs )
{
int nObjs = nVars + nNodes;
int Attempt, i, k;
for ( Attempt = 0; Attempt < 200; Attempt++ )
{
int * pFans = ABC_ALLOC( int, 2 * nNodes );
int fOk = 1;
for ( i = 0; i < 2 * nNodes; i++ )
pFans[i] = -1;
for ( i = nObjs - 2; i >= nVars && fOk; i-- )
fOk = Abc_TwoExactPermAddRequired( pFans, nVars, nNodes, i );
for ( i = 0; i < nVars && fOk; i++ )
fOk = Abc_TwoExactPermAddRequired( pFans, nVars, nNodes, i );
for ( i = 0; i < nNodes && fOk; i++ )
{
int Limit = nVars + i;
for ( k = 0; k < 2; k++ )
{
int Try;
if ( pFans[2*i+k] != -1 )
continue;
for ( Try = 0; Try < 100; Try++ )
if ( Abc_TwoExactPermAddFanin( pFans, i, Abc_Random(0) % Limit ) )
break;
if ( Try == 100 )
fOk = 0;
}
if ( pFans[2*i] > pFans[2*i+1] )
ABC_SWAP( int, pFans[2*i], pFans[2*i+1] );
}
if ( fOk && Abc_TwoExactPermCheck(pFans, nVars, nNodes, 1) && Abc_TwoExactPermAddDcs(pFans, nVars, nNodes, nDcs, 0, 0) )
return pFans;
ABC_FREE( pFans );
}
return NULL;
}
static int * Abc_TwoExactPermRandomSeeded( int nVars, int nNodes, int nDcs, Vec_Int_t * vSeedPairs, int nSeeds )
{
int nObjs = nVars + nNodes;
int Attempt, i, k;
nSeeds = Abc_MinInt( nSeeds, Vec_IntSize(vSeedPairs) );
for ( Attempt = 0; Attempt < 200; Attempt++ )
{
int * pFans = ABC_ALLOC( int, 2 * nNodes );
int * pUsed = ABC_CALLOC( int, Vec_IntSize(vSeedPairs) );
int fOk = 1;
for ( i = 0; i < 2 * nNodes; i++ )
pFans[i] = -1;
for ( i = 0; i < nSeeds; i++ )
{
int s, iSeed = -1, nChoices = 0;
for ( s = 0; s < Vec_IntSize(vSeedPairs); s++ )
if ( !pUsed[s] && Abc_Random(0) % ++nChoices == 0 )
iSeed = s;
assert( iSeed >= 0 );
pUsed[iSeed] = 1;
int Pair = Vec_IntEntry( vSeedPairs, iSeed );
pFans[2*i] = Pair / nVars;
pFans[2*i+1] = Pair % nVars;
}
for ( i = nObjs - 2; i >= nVars && fOk; i-- )
fOk = Abc_TwoExactPermAddRequired( pFans, nVars, nNodes, i );
for ( i = 0; i < nVars && fOk; i++ )
fOk = Abc_TwoExactPermAddRequired( pFans, nVars, nNodes, i );
for ( i = 0; i < nNodes && fOk; i++ )
{
int Limit = nVars + i;
for ( k = 0; k < 2; k++ )
{
int Try;
if ( pFans[2*i+k] != -1 )
continue;
for ( Try = 0; Try < 100; Try++ )
if ( Abc_TwoExactPermAddFanin( pFans, i, Abc_Random(0) % Limit ) )
break;
if ( Try == 100 )
fOk = 0;
}
if ( pFans[2*i] > pFans[2*i+1] )
ABC_SWAP( int, pFans[2*i], pFans[2*i+1] );
}
if ( fOk && Abc_TwoExactPermCheck(pFans, nVars, nNodes, 0) && Abc_TwoExactPermAddDcs(pFans, nVars, nNodes, nDcs, 2*nSeeds, 1) )
{
ABC_FREE( pUsed );
return pFans;
}
ABC_FREE( pUsed );
ABC_FREE( pFans );
}
return NULL;
}
static char * Abc_TwoExactCofactorHex( char * pHex, int nVars, int iVar, int Value )
{
word pTruth[64], pCof[64];
int nCofVars = nVars - 1;
int nMints = 1 << nCofVars;
char * pRes = ABC_ALLOC( char, (nCofVars >= 2 ? (1 << (nCofVars-2)) : 1) + 10 );
int m;
memset( pTruth, 0, sizeof(word) * 64 );
memset( pCof, 0, sizeof(word) * 64 );
Abc_TtReadHex( pTruth, pHex );
for ( m = 0; m < nMints; m++ )
{
int Low = m & ((1 << iVar) - 1);
int High = m >> iVar;
int Mint = Low | (Value << iVar) | (High << (iVar + 1));
if ( Abc_TtGetBit(pTruth, Mint) )
Abc_TtSetBit( pCof, m );
}
Extra_PrintHexadecimalString( pRes, (unsigned *)pCof, nCofVars );
return pRes;
}
static int Abc_TwoExactRun( Bmc_EsPar_t * pPars )
{
extern int Exa_ManExactSynthesis( Bmc_EsPar_t * pPars );
extern int Exa_ManExactSynthesis2( Bmc_EsPar_t * pPars );
return pPars->fGlucose ? Exa_ManExactSynthesis( pPars ) : Exa_ManExactSynthesis2( pPars );
}
static int Abc_TwoExactRunMin( Bmc_EsPar_t * pPars, int nNodeMax )
{
int n, nNodeBeg = pPars->nVars + 1;
int fFound = 0;
for ( n = nNodeBeg; n <= nNodeMax; n++ )
{
if ( !pPars->fSilent )
printf( "\nTrying N = %d:\n", n );
pPars->nNodes = n;
ABC_FREE( pPars->pSolFans );
fFound = Abc_TwoExactRun( pPars );
if ( fFound )
return n;
}
return 0;
}
static Vec_Int_t * Abc_TwoExactCofactorSeeds( Bmc_EsPar_t * pPars, int nNodeMax )
{
int Counts[16][16];
int v, c, i, k, nPairs = 0;
Vec_Int_t * vPairs = Vec_IntAlloc( 16 );
memset( Counts, 0, sizeof(Counts) );
if ( pPars->nVars > 16 )
return vPairs;
for ( v = 0; v < pPars->nVars; v++ )
for ( c = 0; c < 2; c++ )
{
Bmc_EsPar_t CofPars, * pCof = &CofPars;
char * pCofHex = Abc_TwoExactCofactorHex( pPars->pTtStr, pPars->nVars, v, c );
int nFound;
Bmc_EsParSetDefault( pCof );
pCof->nVars = pPars->nVars - 1;
pCof->nNodes = nNodeMax;
pCof->pTtStr = pCofHex;
pCof->fOnlyAnd = pPars->fOnlyAnd;
pCof->fGlucose = pPars->fGlucose;
pCof->RuntimeLim = pPars->RuntimeLim ? pPars->RuntimeLim : 1;
pCof->fSilent = 1;
nFound = Abc_TwoExactRunMin( pCof, nNodeMax );
if ( nFound )
{
printf( "Cofactor %c=%d: minimum N = %d, truth = %s\n", 'a' + v, c, nFound, pCofHex );
for ( i = 0; i < nFound; i++ )
{
int Fan0 = pCof->pSolFans[2*i];
int Fan1 = pCof->pSolFans[2*i+1];
if ( Fan0 >= pCof->nVars || Fan1 >= pCof->nVars )
continue;
Fan0 += Fan0 >= v;
Fan1 += Fan1 >= v;
if ( Fan0 > Fan1 )
ABC_SWAP( int, Fan0, Fan1 );
Counts[Fan0][Fan1]++;
}
}
else
printf( "Cofactor %c=%d: no solution up to N = %d, truth = %s\n", 'a' + v, c, nNodeMax, pCofHex );
ABC_FREE( pCof->pSolFans );
ABC_FREE( pCofHex );
}
for ( k = pPars->nVars * pPars->nVars; k > 0; k-- )
{
int BestI = -1, BestJ = -1, Best = 0;
for ( i = 0; i < pPars->nVars; i++ )
for ( v = i + 1; v < pPars->nVars; v++ )
if ( Counts[i][v] > Best )
{
Best = Counts[i][v];
BestI = i;
BestJ = v;
}
if ( Best == 0 )
break;
printf( "Frequent seed %d: %c%c appears %d time%s.\n", ++nPairs, 'a' + BestI, 'a' + BestJ, Best, Best == 1 ? "" : "s" );
for ( v = 0; v < Best; v++ )
Vec_IntPush( vPairs, BestI * pPars->nVars + BestJ );
Counts[BestI][BestJ] = 0;
}
return vPairs;
}
int Abc_CommandTwoExact( Abc_Frame_t * pAbc, int argc, char ** argv )
{
extern void Exa_ManExactSynthesis( Bmc_EsPar_t * pPars );
extern void Exa_ManExactSynthesis2( Bmc_EsPar_t * pPars );
extern int Exa_ManExactSynthesis( Bmc_EsPar_t * pPars );
extern int Exa_ManExactSynthesis2( Bmc_EsPar_t * pPars );
extern void Exa_ManExactSynthesis4( Bmc_EsPar_t * pPars );
extern void Exa_ManExactSynthesis5( Bmc_EsPar_t * pPars );
extern void Exa_ManExactSynthesis6( Bmc_EsPar_t * pPars, char * pFileName );
extern void Exa_ManExactSynthesis7( Bmc_EsPar_t * pPars, int GateSize );
int c, fKissat = 0, fKissat2 = 0, fUseNands = 0, GateSize = 0;
int c, fKissat = 0, fKissat2 = 0, fUseNands = 0, GateSize = 0, nCandPerms = 0, nPermDcs = 0, fTryMin = 0, fSmartGen = 0, nSeedNodes = 0;
Bmc_EsPar_t Pars, * pPars = &Pars;
Bmc_EsParSetDefault( pPars );
Extra_UtilGetoptReset();
while ( ( c = Extra_UtilGetopt( argc, argv, "INTGSabdconugklmvh" ) ) != EOF )
while ( ( c = Extra_UtilGetopt( argc, argv, "INTGSPCDEabdconugklmtxvh" ) ) != EOF )
{
switch ( c )
{
@ -10672,6 +11044,48 @@ int Abc_CommandTwoExact( Abc_Frame_t * pAbc, int argc, char ** argv )
pPars->pGuide = argv[globalUtilOptind];
globalUtilOptind++;
break;
case 'P':
if ( globalUtilOptind >= argc )
{
Abc_Print( -1, "Command line switch \"-P\" should be followed by a variable permutation.\n" );
goto usage;
}
pPars->pPermStr = argv[globalUtilOptind];
globalUtilOptind++;
break;
case 'C':
if ( globalUtilOptind >= argc )
{
Abc_Print( -1, "Command line switch \"-C\" should be followed by an integer.\n" );
goto usage;
}
nCandPerms = atoi(argv[globalUtilOptind]);
globalUtilOptind++;
if ( nCandPerms < 0 )
goto usage;
break;
case 'D':
if ( globalUtilOptind >= argc )
{
Abc_Print( -1, "Command line switch \"-D\" should be followed by an integer.\n" );
goto usage;
}
nPermDcs = atoi(argv[globalUtilOptind]);
globalUtilOptind++;
if ( nPermDcs < 0 )
goto usage;
break;
case 'E':
if ( globalUtilOptind >= argc )
{
Abc_Print( -1, "Command line switch \"-E\" should be followed by an integer.\n" );
goto usage;
}
nSeedNodes = atoi(argv[globalUtilOptind]);
globalUtilOptind++;
if ( nSeedNodes < 0 )
goto usage;
break;
case 'a':
pPars->fOnlyAnd ^= 1;
break;
@ -10705,6 +11119,12 @@ int Abc_CommandTwoExact( Abc_Frame_t * pAbc, int argc, char ** argv )
case 'm':
pPars->fCard ^= 1;
break;
case 't':
fTryMin ^= 1;
break;
case 'x':
fSmartGen ^= 1;
break;
case 'v':
pPars->fVerbose ^= 1;
break;
@ -10718,6 +11138,11 @@ int Abc_CommandTwoExact( Abc_Frame_t * pAbc, int argc, char ** argv )
{
if ( strstr(argv[globalUtilOptind], ".") )
{
if ( pPars->pPermStr || nCandPerms )
{
Abc_Print( -1, "Permutation options -P and -C are not supported when reading the function from a file.\n" );
return 1;
}
Exa_ManExactSynthesis6( pPars, argv[globalUtilOptind] );
return 0;
}
@ -10743,6 +11168,147 @@ int Abc_CommandTwoExact( Abc_Frame_t * pAbc, int argc, char ** argv )
Abc_Print( -1, "Function should not have more than 10 inputs.\n" );
return 1;
}
if ( nPermDcs && nCandPerms == 0 )
{
Abc_Print( -1, "Command line switch \"-D\" can only be used together with \"-C\".\n" );
return 1;
}
if ( fSmartGen && nCandPerms == 0 )
{
Abc_Print( -1, "Command line switch \"-x\" can only be used together with \"-C\".\n" );
return 1;
}
if ( nSeedNodes && !fSmartGen )
{
Abc_Print( -1, "Command line switch \"-E\" can only be used together with \"-x\".\n" );
return 1;
}
if ( nCandPerms && pPars->pPermStr )
{
Abc_Print( -1, "Command line switch \"-C\" cannot be used together with \"-P\".\n" );
return 1;
}
if ( fTryMin && nCandPerms )
{
Abc_Print( -1, "Command line switch \"-t\" cannot be used together with \"-C\".\n" );
return 1;
}
if ( nPermDcs > 2 * pPars->nNodes )
{
Abc_Print( -1, "The number of don't-care positions should not exceed %d.\n", 2 * pPars->nNodes );
return 1;
}
if ( pPars->pPermStr )
{
char * pToken = pPars->pPermStr;
int nEntries = 0;
while ( *pToken )
{
int iObj = -1;
if ( *pToken == '_' )
{
pToken++;
continue;
}
if ( !Abc_TwoExactPermParseObj(&pToken, pPars->nVars, pPars->nNodes, &iObj) )
{
Abc_Print( -1, "Permutation should use '*', '_', input variables 'a' through '%c', or internal nodes 'A' through '%c'.\n", 'a' + pPars->nVars - 1, 'A' + Abc_MinInt(pPars->nNodes, 26) - 1 );
return 1;
}
nEntries++;
}
if ( nEntries != 2 * pPars->nNodes )
{
Abc_Print( -1, "Permutation should contain %d non-separator symbols (instead of %d).\n", 2 * pPars->nNodes, nEntries );
return 1;
}
if ( fUseNands || fKissat || fKissat2 || pPars->fCard )
{
Abc_Print( -1, "Permutation option -P is currently supported by the default and Glucose (-g) twoexact engines.\n" );
return 1;
}
}
if ( nCandPerms )
{
int i, fFound = 0, nGenerated = 0, nFailed = 0, fSilentSave = pPars->fSilent;
Vec_Int_t * vSeedPairs = NULL;
abctime clk = Abc_Clock();
if ( fUseNands || fKissat || fKissat2 || pPars->fCard )
{
Abc_Print( -1, "Candidate generation with -C is currently supported by the default and Glucose (-g) twoexact engines.\n" );
return 1;
}
Abc_Random( 1 );
if ( fSmartGen )
{
printf( "Deriving frequent seed nodes from cofactors.\n" );
vSeedPairs = Abc_TwoExactCofactorSeeds( pPars, pPars->nNodes );
nSeedNodes = Abc_MinInt( nSeedNodes, Vec_IntSize(vSeedPairs) );
printf( "Trying %d smart candidate input assignments with %d frozen seed node%s and %d randomized don't-care position%s.\n", nCandPerms, nSeedNodes, nSeedNodes == 1 ? "" : "s", nPermDcs, nPermDcs == 1 ? "" : "s" );
}
else
printf( "Trying %d random candidate input assignments with %d randomized don't-care position%s.\n", nCandPerms, nPermDcs, nPermDcs == 1 ? "" : "s" );
pPars->fSilent = 1;
for ( i = 0; i < nCandPerms; i++ )
{
int * pFans = fSmartGen ? Abc_TwoExactPermRandomSeeded( pPars->nVars, pPars->nNodes, nPermDcs, vSeedPairs, nSeedNodes ) : Abc_TwoExactPermRandom( pPars->nVars, pPars->nNodes, nPermDcs );
char * pPerm, * pStruct;
if ( pFans == NULL )
{
nFailed++;
continue;
}
pPerm = Abc_TwoExactPermEncode( pFans, pPars->nVars, pPars->nNodes );
pStruct = Abc_TwoExactPermEncodeFull( pFans, pPars->nVars, pPars->nNodes );
nGenerated++;
pPars->pPermFans = pFans;
pPars->pPermStr = pPerm;
if ( nGenerated == 1 || nGenerated % 10000 == 0 )
printf( "Trying candidate %d/%d: %s\n", nGenerated, nCandPerms, pStruct );
fFound = pPars->fGlucose ? Exa_ManExactSynthesis( pPars ) : Exa_ManExactSynthesis2( pPars );
if ( fFound )
{
pPars->fSilent = fSilentSave;
Abc_TwoExactRun( pPars );
printf( "Found solution using candidate %d: %s\n", nGenerated, pStruct );
ABC_FREE( pStruct );
ABC_FREE( pPerm );
ABC_FREE( pFans );
break;
}
ABC_FREE( pStruct );
ABC_FREE( pPerm );
ABC_FREE( pFans );
pPars->pPermStr = NULL;
pPars->pPermFans = NULL;
}
pPars->pPermStr = NULL;
pPars->pPermFans = NULL;
pPars->fSilent = fSilentSave;
Vec_IntFreeP( &vSeedPairs );
ABC_FREE( pPars->pSolFans );
if ( !fFound )
printf( "No solution found after trying %d generated candidate%s (%d generation failure%s).\n", nGenerated, nGenerated == 1 ? "" : "s", nFailed, nFailed == 1 ? "" : "s" );
Abc_PrintTime( 1, "Total candidate-search runtime", Abc_Clock() - clk );
return 0;
}
if ( fTryMin )
{
if ( fUseNands || fKissat || fKissat2 || pPars->fCard )
{
Abc_Print( -1, "Minimum-node enumeration with -t is currently supported by the default and Glucose (-g) twoexact engines.\n" );
return 1;
}
if ( pPars->nNodes < pPars->nVars + 1 )
{
Abc_Print( -1, "Command line switch \"-t\" expects \"-N <num>\" to be at least %d.\n", pPars->nVars + 1 );
return 1;
}
if ( !Abc_TwoExactRunMin(pPars, pPars->nNodes) )
printf( "No solution found from N = %d through N = %d.\n", pPars->nVars + 1, pPars->nNodes );
ABC_FREE( pPars->pSolFans );
return 0;
}
if ( fUseNands )
Exa_ManExactSynthesis7( pPars, GateSize );
else if ( fKissat || pPars->fCard )
@ -10753,16 +11319,21 @@ int Abc_CommandTwoExact( Abc_Frame_t * pAbc, int argc, char ** argv )
Exa_ManExactSynthesis( pPars );
else
Exa_ManExactSynthesis2( pPars );
ABC_FREE( pPars->pSolFans );
return 0;
usage:
Abc_Print( -2, "usage: twoexact [-INTG <num>] [-S str] [-abdconugklmvh] <hex>\n" );
Abc_Print( -2, "usage: twoexact [-INTGCDE <num>] [-S str] [-P str] [-abdconugklmtxvh] <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-P <str> : fixed input permutation; '_' separates gates, '*' leaves fanin free [default = %s]\n", pPars->pPermStr ? pPars->pPermStr : "none" );
Abc_Print( -2, "\t-C <num> : number of random candidate permutations to try [default = %d]\n", nCandPerms );
Abc_Print( -2, "\t-D <num> : number of fixed variable positions randomized to '*' in each candidate [default = %d]\n", nPermDcs );
Abc_Print( -2, "\t-E <num> : number of frequent cofactor seed nodes used with -x [default = %d]\n", nSeedNodes );
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" );
@ -10774,6 +11345,8 @@ usage:
Abc_Print( -2, "\t-k : toggle using Kissat by Armin Biere [default = %s]\n", fKissat ? "yes" : "no" );
Abc_Print( -2, "\t-l : toggle using Kissat by Armin Biere [default = %s]\n", fKissat2 ? "yes" : "no" );
Abc_Print( -2, "\t-m : toggle using CaDiCaL by Armin Biere [default = %s]\n", pPars->fCard ? "yes" : "no" );
Abc_Print( -2, "\t-t : toggle trying increasing node counts up to \"-N <num>\" [default = %s]\n", fTryMin ? "yes" : "no" );
Abc_Print( -2, "\t-x : toggle smart candidate generation using cofactor seed nodes [default = %s]\n", fSmartGen ? "yes" : "no" );
Abc_Print( -2, "\t-v : toggle verbose printout [default = %s]\n", pPars->fVerbose ? "yes" : "no" );
Abc_Print( -2, "\t-h : print the command usage\n" );
Abc_Print( -2, "\t<hex> : truth table in hex notation\n" );
@ -30698,7 +31271,7 @@ int Abc_CommandBmc3( Abc_Frame_t * pAbc, int argc, char ** argv )
int c;
Saig_ParBmcSetDefaultParams( pPars );
Extra_UtilGetoptReset();
while ( ( c = Extra_UtilGetopt( argc, argv, "SFTHGCDJIPQRLWaxdursgvzh" ) ) != EOF )
while ( ( c = Extra_UtilGetopt( argc, argv, "SFTHGCDJIPQRLWaxdursgvzhc" ) ) != EOF )
{
switch ( c )
{
@ -30873,6 +31446,9 @@ int Abc_CommandBmc3( Abc_Frame_t * pAbc, int argc, char ** argv )
case 'g':
pPars->fUseGlucose ^= 1;
break;
case 'c':
pPars->fUseCadical ^= 1;
break;
case 'v':
pPars->fVerbose ^= 1;
break;
@ -30967,6 +31543,7 @@ usage:
Abc_Print( -2, "\t-r : toggle disabling periodic restarts [default = %s]\n", pPars->fNoRestarts? "yes": "no" );
Abc_Print( -2, "\t-s : toggle using Satoko by Bruno Schmitt [default = %s]\n", pPars->fUseSatoko? "yes": "no" );
Abc_Print( -2, "\t-g : toggle using Glucose 3.0 by Gilles Audemard and Laurent Simon [default = %s]\n",pPars->fUseGlucose? "yes": "no" );
Abc_Print( -2, "\t-c : toggle using CaDiCaL by Armin Biere, University of Freiburg [default = %s]\n",pPars->fUseCadical? "yes": "no" );
Abc_Print( -2, "\t-v : toggle verbose output [default = %s]\n", pPars->fVerbose? "yes": "no" );
Abc_Print( -2, "\t-z : toggle suppressing report about solved outputs [default = %s]\n", pPars->fNotVerbose? "yes": "no" );
Abc_Print( -2, "\t-h : print the command usage\n");
@ -42705,6 +43282,105 @@ static Gia_Man_t * Abc_GiaReorderInputsByName( Gia_Man_t * pFirst, Gia_Man_t * p
return pNew;
}
static Gia_Man_t * Abc_GiaDupPermOutputs( Gia_Man_t * p, Vec_Int_t * vPoPerm )
{
Gia_Man_t * pNew;
Gia_Obj_t * pObj;
int i;
assert( Vec_IntSize(vPoPerm) == Gia_ManPoNum(p) );
pNew = Gia_ManStart( Gia_ManObjNum(p) );
pNew->pName = Abc_UtilStrsav( p->pName );
pNew->pSpec = Abc_UtilStrsav( p->pSpec );
Gia_ManConst0(p)->Value = 0;
Gia_ManForEachCi( p, pObj, i )
pObj->Value = Gia_ManAppendCi( pNew );
Gia_ManForEachAnd( p, pObj, i )
{
if ( Gia_ObjIsBuf(pObj) )
pObj->Value = Gia_ManAppendBuf( pNew, Gia_ObjFanin0Copy(pObj) );
else
pObj->Value = Gia_ManAppendAnd( pNew, Gia_ObjFanin0Copy(pObj), Gia_ObjFanin1Copy(pObj) );
}
Gia_ManForEachPo( p, pObj, i )
Gia_ManAppendCo( pNew, Gia_ObjFanin0Copy(Gia_ManPo(p, Vec_IntEntry(vPoPerm, i))) );
Gia_ManForEachRi( p, pObj, i )
Gia_ManAppendCo( pNew, Gia_ObjFanin0Copy(pObj) );
Gia_ManSetRegNum( pNew, Gia_ManRegNum(p) );
return pNew;
}
static Gia_Man_t * Abc_GiaReorderOutputsByName( Gia_Man_t * pFirst, Gia_Man_t * pSecond )
{
Vec_Int_t * vPoPerm;
Gia_Man_t * pNew;
char * pName1, * pName2;
int * pUsed;
int i, k, nPos, fDiff = 0;
if ( pFirst == NULL || pSecond == NULL || pFirst->vNamesOut == NULL || pSecond->vNamesOut == NULL )
return NULL;
nPos = Gia_ManPoNum( pFirst );
if ( nPos != Gia_ManPoNum(pSecond) )
return NULL;
if ( Vec_PtrSize(pFirst->vNamesOut) < nPos || Vec_PtrSize(pSecond->vNamesOut) < nPos )
return NULL;
vPoPerm = Vec_IntAlloc( nPos );
pUsed = ABC_CALLOC( int, nPos );
for ( i = 0; i < nPos; i++ )
{
pName1 = (char *)Vec_PtrEntry( pFirst->vNamesOut, i );
if ( pName1 == NULL )
break;
for ( k = 0; k < nPos; k++ )
{
pName2 = (char *)Vec_PtrEntry( pSecond->vNamesOut, k );
if ( pName2 && !pUsed[k] && !strcmp(pName1, pName2) )
break;
}
if ( k == nPos )
break;
pUsed[k] = 1;
Vec_IntPush( vPoPerm, k );
fDiff |= (k != i);
}
ABC_FREE( pUsed );
if ( i < nPos || !fDiff )
{
Vec_IntFree( vPoPerm );
return NULL;
}
pNew = Abc_GiaDupPermOutputs( pSecond, vPoPerm );
Vec_IntFree( vPoPerm );
pNew->vNamesIn = Abc_GiaDupNameVec( pSecond->vNamesIn );
pNew->vNamesOut = Vec_PtrAlloc( Vec_PtrSize(pSecond->vNamesOut) );
for ( i = 0; i < nPos; i++ )
{
pName1 = (char *)Vec_PtrEntry( pFirst->vNamesOut, i );
Vec_PtrPush( pNew->vNamesOut, pName1 ? Abc_UtilStrsav(pName1) : NULL );
}
for ( i = nPos; i < Vec_PtrSize(pSecond->vNamesOut); i++ )
{
pName2 = (char *)Vec_PtrEntry( pSecond->vNamesOut, i );
Vec_PtrPush( pNew->vNamesOut, pName2 ? Abc_UtilStrsav(pName2) : NULL );
}
return pNew;
}
static void Abc_GiaTransferNamesIfMatch( Gia_Man_t * pGia, Gia_Man_t * pGiaNames )
{
if ( pGia == NULL || pGiaNames == NULL )
return;
if ( pGia->vNamesIn == NULL && pGiaNames->vNamesIn != NULL && Gia_ManCiNum(pGia) == Vec_PtrSize(pGiaNames->vNamesIn) )
{
pGia->vNamesIn = pGiaNames->vNamesIn;
pGiaNames->vNamesIn = NULL;
}
if ( pGia->vNamesOut == NULL && pGiaNames->vNamesOut != NULL && Gia_ManCoNum(pGia) == Vec_PtrSize(pGiaNames->vNamesOut) )
{
pGia->vNamesOut = pGiaNames->vNamesOut;
pGiaNames->vNamesOut = NULL;
}
}
/**Function*************************************************************
Synopsis []
@ -42722,6 +43398,7 @@ static Gia_Man_t * Abc_ReadAigerOrVerilogFile( char * pFileName, char * pFileNam
Gia_Man_t * pGia;
char * pTemp;
char * pOrigFileName = NULL;
char * pFileTemp = NULL;
int fVerilog, fSystemVerilog;
*pAbc_ReadAigerOrVerilogFileStatus = 0;
@ -42750,17 +43427,24 @@ static Gia_Man_t * Abc_ReadAigerOrVerilogFile( char * pFileName, char * pFileNam
extern Aig_Man_t * Abc_NtkToDar( Abc_Ntk_t * pNtk, int fExors, int fRegisters );
Aig_Man_t * pAig = NULL;
char pCommand[2000];
char * pFileBase;
int RetValue;
int fSystemVerilog2 = pFileName2 && Extra_FileIsType( pFileName2, ".sv", NULL, NULL );
// Save the original filename before changing it
pOrigFileName = pFileName;
pFileBase = pTopModule ? Abc_UtilStrsav(pTopModule) :
Extra_FileNameGeneric( Extra_FileNameWithoutPath(pFileName) );
pFileTemp = ABC_ALLOC( char, strlen(pFileBase) + 5 );
sprintf( pFileTemp, "%s.aig", pFileBase );
ABC_FREE( pFileBase );
snprintf( pCommand, sizeof(pCommand),
"yosys -qp \"read_verilog %s%s %s%s%s%s; hierarchy %s%s; flatten; proc; opt; async2sync; opt; setundef -undriven -zero; techmap; memory -nomap; memory_map; dffunmap; opt_clean; opt_expr; %saigmap; write_aiger -symbols _temp_.aig\"",
"yosys -qp \"read_verilog %s%s %s%s%s%s; hierarchy %s%s; flatten; proc; opt; async2sync; opt; setundef -undriven -zero; techmap; memory -nomap; memory_map; dffunmap; opt_clean; opt_expr; %saigmap; write_aiger -symbols %s\"",
pDefines ? "-D" : "", pDefines ? pDefines : "",
(fSystemVerilog || fSystemVerilog2) ? "-sv " : "", pFileName,
pFileName2 ? " " : "", pFileName2 ? pFileName2 : "",
pTopModule ? "-top " : "-auto-top", pTopModule ? pTopModule : "",
pFileName2 ? "delete t:\\$scopeinfo; " : "" );
pFileName2 ? "delete t:\\$scopeinfo; " : "",
pFileTemp );
#if defined(__wasm)
RetValue = 1;
#else
@ -42769,14 +43453,17 @@ static Gia_Man_t * Abc_ReadAigerOrVerilogFile( char * pFileName, char * pFileNam
if ( RetValue != 0 )
{
Abc_Print( -1, "Yosys command failed: \"%s\".\n", pCommand );
ABC_FREE( pFileTemp );
return NULL;
}
if ( pFileName2 )
{
Abc_Ntk_t * pNtk = Io_Read( "_temp_.aig", IO_FILE_AIGER, 1, 0 );
Gia_Man_t * pGiaNames = NULL;
Abc_Ntk_t * pNtk = Io_Read( pFileTemp, IO_FILE_AIGER, 1, 0 );
if ( pNtk == NULL )
{
Abc_Print( -1, "Reading AIGER from file \"%s\" has failed.\n", "_temp_.aig" );
Abc_Print( -1, "Reading AIGER from file \"%s\" has failed.\n", pFileTemp );
ABC_FREE( pFileTemp );
return NULL;
}
pAig = Abc_NtkToDar( pNtk, 0, 1 );
@ -42784,14 +43471,19 @@ static Gia_Man_t * Abc_ReadAigerOrVerilogFile( char * pFileName, char * pFileNam
if ( pAig == NULL )
{
Abc_Print( -1, "Converting the AIGER network into an internal AIG has failed.\n" );
ABC_FREE( pFileTemp );
return NULL;
}
pGia = Gia_ManFromAig( pAig );
Aig_ManStop( pAig );
pGiaNames = Gia_AigerRead( pFileTemp, 0, 1, 0 );
Abc_GiaTransferNamesIfMatch( pGia, pGiaNames );
if ( pGiaNames )
Gia_ManStop( pGiaNames );
}
else
{
pFileName = "_temp_.aig";
pFileName = pFileTemp;
pGia = Gia_AigerRead( pFileName, 0, 0, 0 );
}
}
@ -42800,6 +43492,7 @@ static Gia_Man_t * Abc_ReadAigerOrVerilogFile( char * pFileName, char * pFileNam
if ( pGia == NULL )
{
Abc_Print( -1, "Reading AIGER from file \"%s\" has failed.\n", pFileName );
ABC_FREE( pFileTemp );
return NULL;
}
@ -42810,6 +43503,7 @@ static Gia_Man_t * Abc_ReadAigerOrVerilogFile( char * pFileName, char * pFileNam
pGia->pSpec = Abc_UtilStrsav( pOrigFileName );
}
ABC_FREE( pFileTemp );
return pGia;
}
@ -43069,6 +43763,15 @@ int Abc_CommandAbc9Cec( Abc_Frame_t * pAbc, int argc, char ** argv )
Gia_ManStop( pGias[1] );
pGias[1] = pTemp;
}
pTemp = Abc_GiaReorderOutputsByName( pGias[0], pGias[1] );
if ( pTemp )
{
if ( pPars->fVerbose )
Abc_Print( 1, "Reordered primary outputs of the second network using output names.\n" );
if ( pGias[1] != pAbc->pGia && pGias[1] != pAbc->pGiaSaved )
Gia_ManStop( pGias[1] );
pGias[1] = pTemp;
}
}
pPars->pNameSpec = pGias[0] ? (pGias[0]->pSpec ? pGias[0]->pSpec : pGias[0]->pName) : NULL;
pPars->pNameImpl = pGias[1] ? (pGias[1]->pSpec ? pGias[1]->pSpec : pGias[1]->pName) : NULL;
@ -51747,12 +52450,12 @@ int Abc_CommandAbc9SProve( Abc_Frame_t * pAbc, int argc, char ** argv )
usage:
Abc_Print( -2, "usage: &sprove [-PTUW num] [-C str] [-R file] [-usvwh]\n" );
Abc_Print( -2, "\t proves CEC problem by case-splitting\n" );
Abc_Print( -2, "\t concurrent sequential model checker\n" );
Abc_Print( -2, "\t-P num : the number of concurrent processes (1 <= num <= 6) [default = %d]\n", nProcs );
Abc_Print( -2, "\t-T num : runtime limit in seconds per subproblem [default = %d]\n", nTimeOut );
Abc_Print( -2, "\t-U num : second-stage timeout in seconds [default = %d]\n", nTimeOut2 );
Abc_Print( -2, "\t-T num : first-stage timeout for proving original and scnew reduction [default = %d]\n", nTimeOut );
Abc_Print( -2, "\t-U num : second-stage proving timeout on optimized miter [default = %d]\n", nTimeOut2 );
Abc_Print( -2, "\t-W num : late-stage timeout for optimization and final proving [default = %d]\n", nTimeOut3 );
Abc_Print( -2, "\t-C str : with -u, pass this option string to internal %%ufar\n" );
Abc_Print( -2, "\t-W num : runtime limit in seconds per subproblem [default = %d]\n", nTimeOut3 );
Abc_Print( -2, "\t-R str : dump replay/trace file for later execution by &sprove2\n" );
Abc_Print( -2, "\t-u : enable concurrent UFAR on word-level design (uses internal %%blast + &miter -x)\n" );
Abc_Print( -2, "\t-s : enable silent computation (no reporting) [default = %s]\n", fSilent? "yes": "no" );
@ -58745,11 +59448,11 @@ usage:
***********************************************************************/
int Abc_CommandAbc9GenAdder( Abc_Frame_t * pAbc, int argc, char ** argv )
{
extern Gia_Man_t * Gia_ManGenAdder( int nVars, int fSK, int fBK, int fHC, int fCarries, int fVerbose );
extern Gia_Man_t * Gia_ManGenAdder( int nVars, int fSK, int fBK, int fHC, int fMM, int fCarries, int fVerbose );
Gia_Man_t * pTemp = NULL;
int c, nBits = 0, fSK = 0, fBK = 0, fHC = 0, fCarries = 0, fVerbose = 0;
int c, nBits = 0, fSK = 0, fBK = 0, fHC = 0, fMM = 0, fCarries = 0, fVerbose = 0;
Extra_UtilGetoptReset();
while ( ( c = Extra_UtilGetopt( argc, argv, "Nsbhcv" ) ) != EOF )
while ( ( c = Extra_UtilGetopt( argc, argv, "Nsbhmcv" ) ) != EOF )
{
switch ( c )
{
@ -58773,6 +59476,9 @@ int Abc_CommandAbc9GenAdder( Abc_Frame_t * pAbc, int argc, char ** argv )
case 'h':
fHC ^= 1;
break;
case 'm':
fMM ^= 1;
break;
case 'c':
fCarries ^= 1;
break;
@ -58788,17 +59494,18 @@ int Abc_CommandAbc9GenAdder( Abc_Frame_t * pAbc, int argc, char ** argv )
Abc_Print( -1, "Abc_CommandAbc9GenAdder(): The number of inputs should be defined on the command line \"-N num\".\n" );
return 0;
}
pTemp = Gia_ManGenAdder( nBits, fSK, fBK, fHC, fCarries, fVerbose );
pTemp = Gia_ManGenAdder( nBits, fSK, fBK, fHC, fMM, fCarries, fVerbose );
Abc_FrameUpdateGia( pAbc, pTemp );
return 0;
usage:
Abc_Print( -2, "usage: &genadder [-N <num>] [-sbhcv]\n" );
Abc_Print( -2, "usage: &genadder [-N <num>] [-sbhmcv]\n" );
Abc_Print( -2, "\t generates a prefix adder (by default, the ripple carry adder)\n" );
Abc_Print( -2, "\t-N num : the bit-width of the adder [default = undefined]\n" );
Abc_Print( -2, "\t-s : toggles using Sklansky adder [default = %s]\n", fSK ? "yes": "no" );
Abc_Print( -2, "\t-b : toggles using Brent-Kung adder [default = %s]\n", fBK ? "yes": "no" );
Abc_Print( -2, "\t-h : toggles using Huan-Carlsson adder [default = %s]\n", fHC ? "yes": "no" );
Abc_Print( -2, "\t-m : toggles using majority-based M/M adder [default = %s]\n", fMM ? "yes": "no" );
Abc_Print( -2, "\t-c : toggles using carry-in and carry-out [default = %s]\n", fCarries ? "yes": "no" );
Abc_Print( -2, "\t-v : toggles printing verbose information [default = %s]\n", fVerbose ? "yes": "no" );
return 1;
@ -60470,7 +61177,7 @@ int Abc_CommandAbc9elSLIM( Abc_Frame_t * pAbc, int argc, char ** argv ) {
seteSLIMParams(&params);
Extra_UtilGetoptReset();
params.subcircuit_max_size = 4;
while ( ( c = Extra_UtilGetopt( argc, argv, "CDGIPRSTVWXZfhist" ) ) != EOF ) {
while ( ( c = Extra_UtilGetopt( argc, argv, "CDGIPRSTVWXZcfhist" ) ) != EOF ) {
switch ( c ) {
case 'C':
if ( globalUtilOptind >= argc )

12
src/base/main/mainUtils.c
View File

@ -18,6 +18,12 @@
***********************************************************************/
#ifdef WIN32
#include <process.h>
#else
#include <unistd.h>
#endif
#include "base/abc/abc.h"
#include "mainInt.h"
@ -91,7 +97,13 @@ char * Abc_UtilsGetUsersInput( Abc_Frame_t * pAbc )
{
char * pRetValue;
fprintf( pAbc->Out, "%s", Prompt );
fflush( pAbc->Out );
pRetValue = fgets( Prompt, 5000, stdin );
if ( pRetValue == NULL ) { exit(0); }
if ( !isatty( fileno(stdin) ) ) {
fputs( Prompt, pAbc->Out );
fflush( pAbc->Out );
}
return Prompt;
}
#endif

111
src/base/wln/wlnCom.c
View File

@ -92,13 +92,16 @@ void Wln_End( Abc_Frame_t * pAbc )
******************************************************************************/
int Abc_CommandYosys( Abc_Frame_t * pAbc, int argc, char ** argv )
{
extern Abc_Ntk_t * Wln_ReadMappedSystemVerilog( char * pFileName, char * pTopModule, char * pDefines, char * pLibrary, int fVerbose );
extern Gia_Man_t * Wln_BlastSystemVerilog( char * pFileName, char * pFileName2, char * pTopModule, char * pDefines, int fSkipStrash, int fInvert, int fTechMap, int fLibInDir, int fSetUndef, int fVerbose );
extern Rtl_Lib_t * Wln_ReadSystemVerilog( char * pFileName, char * pTopModule, char * pDefines, int fCollapse, int fVerbose );
extern Abc_Ntk_t * Wln_ReadMappedSystemVerilog( char ** ppFileNames, int nFileNames, char * pTopModule, char * pDefines, char * pLibrary, int fVerbose );
extern Gia_Man_t * Wln_BlastSystemVerilog( char ** ppFileNames, int nFileNames, char * pTopModule, char * pDefines, int fSkipStrash, int fInvert, int fTechMap, int fLibInDir, int fSetUndef, int fVerbose );
extern Rtl_Lib_t * Wln_ReadSystemVerilog( char ** ppFileNames, int nFileNames, char * pTopModule, char * pDefines, int fCollapse, int fVerbose );
FILE * pFile;
char * pFileName = NULL;
char * pFileName2= NULL;
char ** ppFileNames = NULL;
int nFileNames = 0;
int fFileNamesAlloc = 0;
char * pTopModule= NULL;
char * pDefines = NULL;
char * pLibrary = NULL;
@ -194,48 +197,64 @@ int Abc_CommandYosys( Abc_Frame_t * pAbc, int argc, char ** argv )
goto usage;
}
}
if ( argc != globalUtilOptind + 1 )
nFileNames = argc - globalUtilOptind;
if ( nFileNames < 1 )
{
printf( "Abc_CommandReadWlc(): Input file name should be given on the command line.\n" );
printf( "Abc_CommandReadWlc(): Input file name(s) should be given on the command line.\n" );
return 0;
}
// get the file name
pFileName = argv[globalUtilOptind];
if ( (pFile = fopen( pFileName, "r" )) == NULL )
{
Abc_Print( 1, "Cannot open input file \"%s\". ", pFileName );
if ( (pFileName = Extra_FileGetSimilarName( pFileName, ".v", ".sv", NULL, NULL, NULL )) )
Abc_Print( 1, "Did you mean \"%s\"?", pFileName );
Abc_Print( 1, "\n" );
return 0;
}
fclose( pFile );
ppFileNames = pFileName2 ? ABC_ALLOC( char *, nFileNames + 1 ) : argv + globalUtilOptind;
fFileNamesAlloc = pFileName2 != NULL;
if ( pFileName2 )
{
if ( (pFile = fopen( pFileName2, "r" )) == NULL )
int i;
for ( i = 0; i < nFileNames; i++ )
ppFileNames[i] = argv[globalUtilOptind + i];
ppFileNames[nFileNames++] = pFileName2;
}
pFileName = ppFileNames[0];
for ( c = 0; c < nFileNames; c++ )
{
if ( (pFile = fopen( ppFileNames[c], "r" )) == NULL )
{
Abc_Print( 1, "Cannot open input file \"%s\".\n", pFileName2 );
Abc_Print( 1, "Cannot open input file \"%s\". ", ppFileNames[c] );
if ( (pFileName = Extra_FileGetSimilarName( ppFileNames[c], ".v", ".sv", NULL, NULL, NULL )) )
Abc_Print( 1, "Did you mean \"%s\"?", pFileName );
Abc_Print( 1, "\n" );
if ( fFileNamesAlloc )
ABC_FREE( ppFileNames );
return 0;
}
fclose( pFile );
}
// perform reading
if ( pLibrary )
pFileName = ppFileNames[0];
if ( nFileNames > 1 )
{
if ( pFileName2 )
int i, fAllVerilog = 1;
for ( i = 0; i < nFileNames; i++ )
fAllVerilog &= Extra_FileIsType( ppFileNames[i], ".v", ".sv", NULL );
if ( !fAllVerilog )
{
Abc_Print( 1, "Command line switch \"-F\" only applies in the default bit-blasting path.\n" );
Abc_Print( 1, "Multiple input files are supported only for Verilog/SystemVerilog files.\n" );
if ( fFileNamesAlloc )
ABC_FREE( ppFileNames );
return 0;
}
}
// perform reading
if ( pLibrary )
{
Abc_Ntk_t * pNtk = NULL;
if ( !strcmp( Extra_FileNameExtension(pFileName), "v" ) )
pNtk = Wln_ReadMappedSystemVerilog( pFileName, pTopModule, pDefines, pLibrary, fVerbose );
pNtk = Wln_ReadMappedSystemVerilog( ppFileNames, nFileNames, pTopModule, pDefines, pLibrary, fVerbose );
else if ( !strcmp( Extra_FileNameExtension(pFileName), "sv" ) )
pNtk = Wln_ReadMappedSystemVerilog( pFileName, pTopModule, pDefines, pLibrary, fVerbose );
pNtk = Wln_ReadMappedSystemVerilog( ppFileNames, nFileNames, pTopModule, pDefines, pLibrary, fVerbose );
else
{
printf( "Abc_CommandYosys(): Unknown file extension.\n" );
if ( fFileNamesAlloc )
ABC_FREE( ppFileNames );
return 0;
}
Abc_FrameReplaceCurrentNetwork( pAbc, pNtk );
@ -244,55 +263,67 @@ int Abc_CommandYosys( Abc_Frame_t * pAbc, int argc, char ** argv )
{
Gia_Man_t * pNew = NULL;
if ( !strcmp( Extra_FileNameExtension(pFileName), "v" ) )
pNew = Wln_BlastSystemVerilog( pFileName, pFileName2, pTopModule, pDefines, fSkipStrash, fInvert, fTechMap, fLibInDir, fSetUndef, fVerbose );
pNew = Wln_BlastSystemVerilog( ppFileNames, nFileNames, pTopModule, pDefines, fSkipStrash, fInvert, fTechMap, fLibInDir, fSetUndef, fVerbose );
else if ( !strcmp( Extra_FileNameExtension(pFileName), "sv" ) )
pNew = Wln_BlastSystemVerilog( pFileName, pFileName2, pTopModule, pDefines, fSkipStrash, fInvert, fTechMap, fLibInDir, fSetUndef, fVerbose );
pNew = Wln_BlastSystemVerilog( ppFileNames, nFileNames, pTopModule, pDefines, fSkipStrash, fInvert, fTechMap, fLibInDir, fSetUndef, fVerbose );
else if ( !strcmp( Extra_FileNameExtension(pFileName), "rtlil" ) )
{
if ( pFileName2 )
if ( nFileNames > 1 )
{
Abc_Print( 1, "Command line switch \"-F\" is only supported when the main input is Verilog/SystemVerilog.\n" );
Abc_Print( 1, "Multiple input files are supported only for Verilog/SystemVerilog files.\n" );
if ( fFileNamesAlloc )
ABC_FREE( ppFileNames );
return 0;
}
pNew = Wln_BlastSystemVerilog( pFileName, NULL, pTopModule, pDefines, fSkipStrash, fInvert, fTechMap, fLibInDir, fSetUndef, fVerbose );
pNew = Wln_BlastSystemVerilog( ppFileNames, nFileNames, pTopModule, pDefines, fSkipStrash, fInvert, fTechMap, fLibInDir, fSetUndef, fVerbose );
}
else
{
printf( "Abc_CommandYosys(): Unknown file extension.\n" );
if ( fFileNamesAlloc )
ABC_FREE( ppFileNames );
return 0;
}
Abc_FrameUpdateGia( pAbc, pNew );
}
else
{
if ( pFileName2 )
{
Abc_Print( 1, "Command line switch \"-F\" only applies in the default bit-blasting path.\n" );
return 0;
}
Rtl_Lib_t * pLib = NULL;
if ( !strcmp( Extra_FileNameExtension(pFileName), "v" ) )
pLib = Wln_ReadSystemVerilog( pFileName, pTopModule, pDefines, fCollapse, fVerbose );
pLib = Wln_ReadSystemVerilog( ppFileNames, nFileNames, pTopModule, pDefines, fCollapse, fVerbose );
else if ( !strcmp( Extra_FileNameExtension(pFileName), "sv" ) )
pLib = Wln_ReadSystemVerilog( pFileName, pTopModule, pDefines, fCollapse, fVerbose );
pLib = Wln_ReadSystemVerilog( ppFileNames, nFileNames, pTopModule, pDefines, fCollapse, fVerbose );
else if ( !strcmp( Extra_FileNameExtension(pFileName), "rtlil" ) )
pLib = Wln_ReadSystemVerilog( pFileName, pTopModule, pDefines, fCollapse, fVerbose );
{
if ( nFileNames > 1 )
{
Abc_Print( 1, "Multiple input files are supported only for Verilog/SystemVerilog files.\n" );
if ( fFileNamesAlloc )
ABC_FREE( ppFileNames );
return 0;
}
pLib = Wln_ReadSystemVerilog( ppFileNames, nFileNames, pTopModule, pDefines, fCollapse, fVerbose );
}
else
{
printf( "Abc_CommandYosys(): Unknown file extension.\n" );
if ( fFileNamesAlloc )
ABC_FREE( ppFileNames );
return 0;
}
Wln_AbcUpdateRtl( pAbc, pLib );
}
if ( fFileNamesAlloc )
ABC_FREE( ppFileNames );
return 0;
usage:
Abc_Print( -2, "usage: %%yosys [-TM <module>] [-D <defines>] [-L <liberty_file>] [-F <file>] [-bdisumlcvh] <file_name>\n" );
Abc_Print( -2, "usage: %%yosys [-TM <module>] [-D <defines>] [-L <liberty_file>] [-F <file>] [-bdisumlcvh] <file_name> [file_name...]\n" );
Abc_Print( -2, "\t reads Verilog or SystemVerilog using Yosys\n" );
Abc_Print( -2, "\t-T : specify the top module name (default uses \"-auto-top\")\n" );
Abc_Print( -2, "\t-M : specify the top module name (default uses \"-auto-top\") (equivalent to \"-T\")\n" );
Abc_Print( -2, "\t-D : specify defines to be used by Yosys (default \"not used\")\n" );
Abc_Print( -2, "\t-L : specify the Liberty library to read a mapped design (default \"not used\")\n" );
Abc_Print( -2, "\t-F : specify a second Verilog/SystemVerilog file for the default bit-blasting flow (default \"not used\")\n" );
Abc_Print( -2, "\t-F : specify an additional Verilog/SystemVerilog file (default \"not used\")\n" );
Abc_Print( -2, "\t-b : toggle bit-blasting the design into an AIG using Yosys (this switch has no effect)\n" );
Abc_Print( -2, "\t-d : toggle bit-blasting the design into an AIG using Yosys [default = %s]\n", !fDontBlast? "yes": "no" );
Abc_Print( -2, "\t-i : toggle inverting the outputs (useful for miters) [default = %s]\n", fInvert? "yes": "no" );

155
src/base/wln/wlnRtl.c
View File

@ -122,6 +122,45 @@ char * Wln_GetYosysName()
#endif
return pYosysName;
}
static char * Wln_FileNamesJoin( char ** ppFileNames, int nFileNames )
{
char * pFileNames;
int i, nChars = 1;
for ( i = 0; i < nFileNames; i++ )
nChars += strlen( ppFileNames[i] ) + 1;
pFileNames = ABC_ALLOC( char, nChars );
pFileNames[0] = 0;
for ( i = 0; i < nFileNames; i++ )
{
if ( i )
strcat( pFileNames, " " );
strcat( pFileNames, ppFileNames[i] );
}
return pFileNames;
}
static int Wln_FileNamesHasSv( char ** ppFileNames, int nFileNames )
{
int i;
for ( i = 0; i < nFileNames; i++ )
if ( strstr( ppFileNames[i], ".sv" ) != NULL )
return 1;
return 0;
}
static void Wln_GiaTransferNamesIfMatch( Gia_Man_t * pGia, Gia_Man_t * pGiaNames )
{
if ( pGia == NULL || pGiaNames == NULL )
return;
if ( pGia->vNamesIn == NULL && pGiaNames->vNamesIn != NULL && Gia_ManCiNum(pGia) == Vec_PtrSize(pGiaNames->vNamesIn) )
{
pGia->vNamesIn = pGiaNames->vNamesIn;
pGiaNames->vNamesIn = NULL;
}
if ( pGia->vNamesOut == NULL && pGiaNames->vNamesOut != NULL && Gia_ManCoNum(pGia) == Vec_PtrSize(pGiaNames->vNamesOut) )
{
pGia->vNamesOut = pGiaNames->vNamesOut;
pGiaNames->vNamesOut = NULL;
}
}
int Wln_ConvertToRtl( char * pCommand, char * pFileTemp )
{
#if defined(__wasm)
@ -142,29 +181,39 @@ int Wln_ConvertToRtl( char * pCommand, char * pFileTemp )
return 1;
#endif
}
Rtl_Lib_t * Wln_ReadSystemVerilog( char * pFileName, char * pTopModule, char * pDefines, int fCollapse, int fVerbose )
Rtl_Lib_t * Wln_ReadSystemVerilog( char ** ppFileNames, int nFileNames, char * pTopModule, char * pDefines, int fCollapse, int fVerbose )
{
Rtl_Lib_t * pNtk = NULL;
char Command[1000];
char * pFileNames, * pCommand;
char * pFileTemp = "_temp_.rtlil";
int fSVlog = strstr(pFileName, ".sv") != NULL;
if ( strstr(pFileName, ".rtl") )
return Rtl_LibReadFile( pFileName, pFileName );
sprintf( Command, "%s -qp \"read_verilog %s%s %s%s; hierarchy %s%s; %sproc; memory -nomap; memory_map; write_rtlil %s\"",
int fSVlog = Wln_FileNamesHasSv(ppFileNames, nFileNames);
int nCommand;
if ( nFileNames == 1 && strstr(ppFileNames[0], ".rtl") )
return Rtl_LibReadFile( ppFileNames[0], ppFileNames[0] );
pFileNames = Wln_FileNamesJoin( ppFileNames, nFileNames );
nCommand = strlen(Wln_GetYosysName()) + strlen(pFileNames) + (pDefines ? strlen(pDefines) : 0) + (pTopModule ? strlen(pTopModule) : 0) + strlen(pFileTemp) + 200;
pCommand = ABC_ALLOC( char, nCommand );
sprintf( pCommand, "%s -qp \"read_verilog %s%s %s%s; hierarchy %s%s; %sproc; memory -nomap; memory_map; write_rtlil %s\"",
Wln_GetYosysName(),
pDefines ? "-D" : "",
pDefines ? pDefines : "",
fSVlog ? "-sv " : "",
pFileName,
pFileNames,
pTopModule ? "-top " : "",
pTopModule ? pTopModule : "",
fCollapse ? "flatten; ": "",
pFileTemp );
if ( fVerbose )
printf( "%s\n", Command );
if ( !Wln_ConvertToRtl(Command, pFileTemp) )
printf( "%s\n", pCommand );
if ( !Wln_ConvertToRtl(pCommand, pFileTemp) )
{
ABC_FREE( pCommand );
ABC_FREE( pFileNames );
return NULL;
pNtk = Rtl_LibReadFile( pFileTemp, pFileName );
}
ABC_FREE( pCommand );
ABC_FREE( pFileNames );
pNtk = Rtl_LibReadFile( pFileTemp, ppFileNames[0] );
if ( pNtk == NULL )
{
printf( "Dumped the design into file \"%s\".\n", pFileTemp );
@ -174,40 +223,56 @@ Rtl_Lib_t * Wln_ReadSystemVerilog( char * pFileName, char * pTopModule, char * p
unlink( pFileTemp );
return pNtk;
}
Gia_Man_t * Wln_BlastSystemVerilog( char * pFileName, char * pFileName2, char * pTopModule, char * pDefines, int fSkipStrash, int fInvert, int fTechMap, int fLibInDir, int fSetUndef, int fVerbose )
Gia_Man_t * Wln_BlastSystemVerilog( char ** ppFileNames, int nFileNames, char * pTopModule, char * pDefines, int fSkipStrash, int fInvert, int fTechMap, int fLibInDir, int fSetUndef, int fVerbose )
{
Gia_Man_t * pGia = NULL;
char Command[1000];
char * pFileTemp = "_temp_.aig";
int fRtlil = strstr(pFileName, ".rtl") != NULL;
int fSVlog = strstr(pFileName, ".sv") != NULL || (pFileName2 && strstr(pFileName2, ".sv") != NULL);
sprintf( Command, "%s -qp \"%s %s%s %s%s%s%s; hierarchy %s%s; flatten; proc; opt; async2sync; opt; setundef -undriven -zero; %s%smemory -nomap; memory_map; dffunmap; opt_clean; opt_expr; %saigmap; write_aiger -symbols %s\"",
char * pFileNames, * pCommand;
char * pFileTemp, * pFileBase;
int fRtlil = nFileNames == 1 && strstr(ppFileNames[0], ".rtl") != NULL;
int fSVlog = Wln_FileNamesHasSv(ppFileNames, nFileNames);
int nCommand;
pFileBase = pTopModule ? Abc_UtilStrsav(pTopModule) :
Extra_FileNameGeneric( Extra_FileNameWithoutPath(ppFileNames[0]) );
pFileTemp = ABC_ALLOC( char, strlen(pFileBase) + 5 );
sprintf( pFileTemp, "%s.aig", pFileBase );
ABC_FREE( pFileBase );
pFileNames = Wln_FileNamesJoin( ppFileNames, nFileNames );
nCommand = strlen(Wln_GetYosysName()) + strlen(pFileNames) + (pDefines ? strlen(pDefines) : 0) + (pTopModule ? strlen(pTopModule) : 0) + strlen(pFileTemp) + 500;
pCommand = ABC_ALLOC( char, nCommand );
sprintf( pCommand, "%s -qp \"%s %s%s %s%s; hierarchy %s%s; flatten; proc; opt; async2sync; opt; setundef -undriven -zero; %s%smemory -nomap; memory_map; dffunmap; opt_clean; opt_expr; %saigmap; write_aiger -symbols %s\"",
Wln_GetYosysName(),
fRtlil ? "read_rtlil" : "read_verilog",
pDefines ? "-D" : "",
pDefines ? pDefines : "",
fSVlog ? "-sv " : "",
pFileName,
pFileName2 ? " " : "",
pFileName2 ? pFileName2 : "",
pFileNames,
pTopModule ? "-top " : "-auto-top",
pTopModule ? pTopModule : "",
fTechMap ? (fLibInDir ? "techmap -map techmap.v; " : "techmap; ") : "",
fSetUndef ? "setundef -init -zero; " : "",
pFileName2 ? "delete t:\\$scopeinfo; " : "",
nFileNames > 1 ? "delete t:\\$scopeinfo; " : "",
pFileTemp );
if ( fVerbose )
printf( "%s\n", Command );
if ( !Wln_ConvertToRtl(Command, pFileTemp) )
printf( "%s\n", pCommand );
if ( !Wln_ConvertToRtl(pCommand, pFileTemp) )
{
ABC_FREE( pCommand );
ABC_FREE( pFileNames );
ABC_FREE( pFileTemp );
return NULL;
if ( pFileName2 )
}
ABC_FREE( pCommand );
ABC_FREE( pFileNames );
if ( nFileNames > 1 )
{
extern Aig_Man_t * Abc_NtkToDar( Abc_Ntk_t * pNtk, int fExors, int fRegisters );
Aig_Man_t * pAig = NULL;
Gia_Man_t * pGiaNames = NULL;
Abc_Ntk_t * pNtk = Io_Read( pFileTemp, IO_FILE_AIGER, 1, 0 );
if ( pNtk == NULL )
{
printf( "Reading AIGER from file \"%s\" has failed.\n", pFileTemp );
ABC_FREE( pFileTemp );
return NULL;
}
pAig = Abc_NtkToDar( pNtk, 0, 1 );
@ -215,22 +280,29 @@ Gia_Man_t * Wln_BlastSystemVerilog( char * pFileName, char * pFileName2, char *
if ( pAig == NULL )
{
printf( "Converting the AIGER network into an internal AIG has failed.\n" );
ABC_FREE( pFileTemp );
return NULL;
}
pGia = fSkipStrash ? Gia_ManFromAigSimple(pAig) : Gia_ManFromAig(pAig);
Aig_ManStop( pAig );
pGiaNames = Gia_AigerRead( pFileTemp, 0, 1, 0 );
Wln_GiaTransferNamesIfMatch( pGia, pGiaNames );
if ( pGiaNames )
Gia_ManStop( pGiaNames );
}
else
pGia = Gia_AigerRead( pFileTemp, 0, fSkipStrash, 0 );
if ( pGia == NULL )
{
printf( "Converting to AIG has failed.\n" );
ABC_FREE( pFileTemp );
return NULL;
}
ABC_FREE( pGia->pName );
pGia->pName = pTopModule ? Abc_UtilStrsav(pTopModule) :
Extra_FileNameGeneric( Extra_FileNameWithoutPath(pFileName) );
Extra_FileNameGeneric( Extra_FileNameWithoutPath(ppFileNames[0]) );
unlink( pFileTemp );
ABC_FREE( pFileTemp );
// complement the outputs
if ( fInvert )
{
@ -240,35 +312,48 @@ Gia_Man_t * Wln_BlastSystemVerilog( char * pFileName, char * pFileName2, char *
}
return pGia;
}
Abc_Ntk_t * Wln_ReadMappedSystemVerilog( char * pFileName, char * pTopModule, char * pDefines, char * pLibrary, int fVerbose )
Abc_Ntk_t * Wln_ReadMappedSystemVerilog( char ** ppFileNames, int nFileNames, char * pTopModule, char * pDefines, char * pLibrary, int fVerbose )
{
Abc_Ntk_t * pNtk = NULL;
char Command[1000];
char * pFileNames, * pCommand;
char * pFileTemp = "_temp_.blif";
int fSVlog = strstr(pFileName, ".sv") != NULL;
sprintf( Command, "%s -qp \"read_liberty -lib %s; read %s %s%s %s; hierarchy %s%s; flatten; proc; memory -nomap; memory_map; write_blif %s%s -impltf -gates %s\"",
int fSVlog = Wln_FileNamesHasSv(ppFileNames, nFileNames);
int nCommand;
pFileNames = Wln_FileNamesJoin( ppFileNames, nFileNames );
nCommand = strlen(Wln_GetYosysName()) + strlen(pLibrary) + strlen(pFileNames) + (pDefines ? strlen(pDefines) : 0) + 2 * (pTopModule ? strlen(pTopModule) : 0) + strlen(pFileTemp) + 300;
pCommand = ABC_ALLOC( char, nCommand );
sprintf( pCommand, "%s -qp \"read_liberty -lib %s; read %s %s%s %s; hierarchy %s%s; flatten; proc; memory -nomap; memory_map; write_blif %s%s -impltf -gates %s\"",
Wln_GetYosysName(),
pLibrary,
fSVlog ? "-sv " : "-vlog95",
pDefines ? "-D" : "",
pDefines ? pDefines : "",
pFileName,
pFileNames,
pTopModule ? "-top " : "-auto-top",
pTopModule ? pTopModule : "",
pTopModule ? "-top " : "",
pTopModule ? pTopModule : "",
pFileTemp );
if ( fVerbose )
printf( "%s\n", Command );
if ( !Wln_ConvertToRtl(Command, pFileTemp) )
return NULL;
sprintf( Command, "read_lib %s", pLibrary );
if ( Cmd_CommandExecute( Abc_FrameReadGlobalFrame(), Command ) )
printf( "%s\n", pCommand );
if ( !Wln_ConvertToRtl(pCommand, pFileTemp) )
{
fprintf( stdout, "Cannot execute ABC command \"%s\".\n", Command );
ABC_FREE( pCommand );
ABC_FREE( pFileNames );
return NULL;
}
ABC_FREE( pCommand );
ABC_FREE( pFileNames );
pCommand = ABC_ALLOC( char, strlen(pLibrary) + 20 );
sprintf( pCommand, "read_lib %s", pLibrary );
if ( Cmd_CommandExecute( Abc_FrameReadGlobalFrame(), pCommand ) )
{
fprintf( stdout, "Cannot execute ABC command \"%s\".\n", pCommand );
ABC_FREE( pCommand );
unlink( pFileTemp );
return NULL;
}
ABC_FREE( pCommand );
pNtk = Io_Read( pFileTemp, IO_FILE_BLIF, 1, 0 );
if ( pNtk == NULL )
{

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

@ -194,7 +194,7 @@ void If_ObjPerformMappingAnd( If_Man_t * p, If_Obj_t * pObj, int Mode, int fPrep
pCut->Delay = If_CutSopBalanceEval( p, pCut, NULL );
else if ( p->pPars->fDsdBalance )
pCut->Delay = If_CutDsdBalanceEval( p, pCut, NULL );
else if ( p->pPars->fEnableCheck07 && p->pPars->fDelayOptCell )
else if ( p->pPars->fEnableCheck07 && p->pPars->pCellLib )
{
int iLeaf, Intrinsic[IF_MAX_LUTSIZE];
float Delay = -IF_FLOAT_LARGE;
@ -364,7 +364,7 @@ IfMapBestCutDone:
for ( iLeaf = 0; iLeaf < p->nCutLeavesCur; iLeaf++ )
{
If_Obj_t * pLeaf = If_CutLeaf( p, pCut, iLeaf );
if ( p->pPars->fEnableCheck07 && p->pPars->fDelayOptCell && pCut->nLeaves > 1 )
if ( p->pPars->fEnableCheck07 && p->pPars->pCellLib && pCut->nLeaves > 1 )
{
If_Cut_t * pBestCut = If_ObjCutBest( pLeaf );
assert( pBestCut != NULL );
@ -472,8 +472,10 @@ IfMapBestCutDone:
pCut->Delay = If_CutSopBalanceEval( p, pCut, NULL );
else if ( p->pPars->fDsdBalance )
pCut->Delay = If_CutDsdBalanceEval( p, pCut, NULL );
else if ( p->pPars->fEnableCheck07 && p->pPars->fDelayOptCell )
else if ( p->pPars->fEnableCheck07 && p->pPars->pCellLib )
{
int iLeaf, Intrinsic[IF_MAX_LUTSIZE];
float Delay = -IF_FLOAT_LARGE;
if ( pCut->nLeaves == 0 )
{
pCut->Delay = 0.0;
@ -487,9 +489,16 @@ IfMapBestCutDone:
pCut->fUseless = 0;
goto IfMapCutEvalDone;
}
assert( pCut->fUseless || p->fCutDelayCurValid );
assert( pCut->fUseless || pCut->Config != 0 );
pCut->Delay = pCut->fUseless ? IF_FLOAT_LARGE : p->CutDelayCur;
if ( pCut->fUseless )
pCut->Delay = IF_FLOAT_LARGE;
else
{
If_CutComputeIntrinsicJ( p, pCut->Config, pCut->nLeaves, Intrinsic );
If_CutForEachLeaf( p, pCut, pLeaf, iLeaf )
Delay = IF_MAX( Delay, If_ObjArrTime(pLeaf) + (float)Intrinsic[iLeaf] );
pCut->Delay = Delay;
}
IfMapCutEvalDone:
;
}

11
src/map/if/ifTime.c
View File

@ -131,7 +131,7 @@ float If_CutDelay( If_Man_t * p, If_Obj_t * pObj, If_Cut_t * pCut )
}
else
{
if ( p->pPars->fEnableCheck07 && p->pPars->fDelayOptCell && p->pPars->pCellLib )
if ( p->pPars->fEnableCheck07 && p->pPars->pCellLib )
{
int Intrinsic[IF_MAX_LUTSIZE];
if ( pCut->nLeaves == 0 )
@ -233,7 +233,7 @@ void If_CutPropagateRequired( If_Man_t * p, If_Obj_t * pObj, If_Cut_t * pCut, fl
}
else
{
if ( p->pPars->fEnableCheck07 && p->pPars->fDelayOptCell && p->pPars->pCellLib )
if ( p->pPars->fEnableCheck07 && p->pPars->pCellLib )
{
int Intrinsic[IF_MAX_LUTSIZE];
if ( pCut->nLeaves == 0 )
@ -338,7 +338,7 @@ float If_ManDelayMax( If_Man_t * p, int fSeq )
void If_ManComputeRequired( If_Man_t * p )
{
If_Obj_t * pObj;
int i, Counter;
int i, iBox, Counter;
float reqTime;
// compute area, clean required times, collect nodes used in the mapping
@ -480,7 +480,7 @@ void If_ManComputeRequired( If_Man_t * p )
if ( p->pPars->pTimesReq )
{
Counter = 0;
If_ManForEachCo( p, pObj, i )
If_ManForEachPo( p, pObj, i )
{
reqTime = p->pPars->pTimesReq[i];
if ( If_ObjArrTime(If_ObjFanin0(pObj)) > reqTime + p->fEpsilon )
@ -551,6 +551,9 @@ void If_ManComputeRequired( If_Man_t * p )
{
reqTime = pObj->Required;
Tim_ManSetCiRequired( p->pManTim, pObj->IdPio, reqTime );
iBox = Tim_ManBoxForCi( p->pManTim, pObj->IdPio );
if ( iBox >= 0 )
Tim_ManSetPreviousTravIdBoxInputs( p->pManTim, iBox );
}
else if ( If_ObjIsCo(pObj) )
{

10
src/opt/eslim/eSLIM.cpp
View File

@ -603,6 +603,10 @@ Circuitrepresentation* runeSLIM(Circuitrepresentation * cir, const eSLIM_ParamSt
Gia_Man_t* applyeSLIM(Gia_Man_t * pGia, const eSLIM_ParamStruct* params) {
if (Gia_ManHasDangling(pGia)) {
std::cout << "Warning: Circuit must not contain dangling nodes.\n";
return pGia;
}
return runeSLIM(pGia, params);
}
@ -610,12 +614,6 @@ Abc_Ntk_t* applyelSLIM(Abc_Ntk_t * ntk, const eSLIM_ParamStruct* params) {
return runeSLIM(ntk, params);
}
Abc_Ntk_t* applyetSLIM(Abc_Ntk_t * ntk, const eSLIM_ParamStruct* params) {
return runeSLIM(ntk, params);
}

1
src/opt/eslim/eslimCirMan.cpp
View File

@ -79,6 +79,7 @@ namespace eSLIM {
}
eSLIMCirMan::eSLIMCirMan(Gia_Man_t * pGia) : eSLIMCirMan(Gia_ManObjNum(pGia)) {
assert (!Gia_ManHasDangling(pGia));
Gia_ManConst0(pGia)->Value = 0;
Gia_Obj_t * pObj;
int i;

6
src/opt/eslim/relationSynthesiser.cpp
View File

@ -27,8 +27,8 @@ ABC_NAMESPACE_IMPL_START
namespace eSLIM {
RelationSynthesiser::RelationSynthesiser(const Relation& relation, const Subcircuit& subcir, unsigned int max_size, const eSLIMConfig& cfg, eSLIMLog& log)
: relation(relation), subcir(subcir),
max_size(max_size), config(cfg), log(log) {
: subcir(subcir), max_size(max_size),
relation(relation), config(cfg), log(log) {
setupEncoding();
}
@ -609,4 +609,4 @@ namespace eSLIM {
}
ABC_NAMESPACE_IMPL_END
ABC_NAMESPACE_IMPL_END

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

@ -82,6 +82,8 @@ struct Bmc_EsPar_t_
char * pSymStr;
char * pPermStr;
char * pGuide;
int * pPermFans;
int * pSolFans;
Vec_Wrd_t* vTruths;
};
@ -134,6 +136,7 @@ struct Saig_ParBmc_t_
int fNoRestarts; // disables periodic restarts
int fUseSatoko; // enables using Satoko
int fUseGlucose; // enables using Glucose 3.0
int fUseCadical; // enables using CaDiCaL
int nLearnedStart; // starting learned clause limit
int nLearnedDelta; // delta of learned clause limit
int nLearnedPerce; // ratio of learned clause limit

74
src/sat/bmc/bmcBmc3.c
View File

@ -23,12 +23,21 @@
#include "sat/bsat/satStore.h"
#include "sat/satoko/satoko.h"
#include "sat/glucose/AbcGlucose.h"
#include "sat/cadical/cadicalSolver.h"
#include "sat/cadical/ccadical.h"
#include "misc/vec/vecHsh.h"
#include "misc/vec/vecWec.h"
#include "bmc.h"
ABC_NAMESPACE_IMPL_START
static inline void Bmc3_CadicalSetRuntimeLimit( cadical_solver * pSat4, abctime nSeconds )
{
if ( pSat4 == NULL || nSeconds <= 0 )
return;
ccadical_limit( (CCaDiCaL *)pSat4->p, "seconds", nSeconds );
}
////////////////////////////////////////////////////////////////////////
/// DECLARATIONS ///
////////////////////////////////////////////////////////////////////////
@ -64,6 +73,7 @@ struct Gia_ManBmc_t_
sat_solver * pSat; // SAT solver
satoko_t * pSat2; // SAT solver
bmcg_sat_solver * pSat3; // SAT solver
cadical_solver * pSat4; // SAT solver
int nSatVars; // SAT variables
int nObjNums; // SAT objects
int nWordNum; // unsigned words for ternary simulation
@ -718,7 +728,7 @@ Vec_Int_t * Saig_ManBmcComputeMappingRefs( Aig_Man_t * p, Vec_Int_t * vMap )
SeeAlso []
***********************************************************************/
Gia_ManBmc_t * Saig_Bmc3ManStart( Aig_Man_t * pAig, int nTimeOutOne, int nConfLimit, int fUseSatoko, int fUseGlucose )
Gia_ManBmc_t * Saig_Bmc3ManStart( Aig_Man_t * pAig, int nTimeOutOne, int nConfLimit, int fUseSatoko, int fUseGlucose, int fUseCadical )
{
Gia_ManBmc_t * p;
Aig_Obj_t * pObj;
@ -763,6 +773,11 @@ Gia_ManBmc_t * Saig_Bmc3ManStart( Aig_Man_t * pAig, int nTimeOutOne, int nConfLi
for ( i = 0; i < 1000; i++ )
bmcg_sat_solver_addvar( p->pSat3 );
}
else if ( fUseCadical )
{
p->pSat4 = cadical_solver_new();
cadical_solver_setnvars(p->pSat4, 1000);
}
else
{
p->pSat = sat_solver_new();
@ -806,9 +821,9 @@ void Saig_Bmc3ManStop( Gia_ManBmc_t * p )
p->pSat ? p->pSat->nLearntDelta : 0,
p->pSat ? p->pSat->nLearntRatio : 0,
p->pSat ? p->pSat->nDBreduces : 0,
p->pSat ? sat_solver_nvars(p->pSat) : p->pSat3 ? bmcg_sat_solver_varnum(p->pSat3) : satoko_varnum(p->pSat2),
p->pSat ? sat_solver_nvars(p->pSat) : p->pSat4 ? cadical_solver_nvars(p->pSat4) : p->pSat3 ? bmcg_sat_solver_varnum(p->pSat3) : satoko_varnum(p->pSat2),
nUsedVars,
100.0*nUsedVars/(p->pSat ? sat_solver_nvars(p->pSat) : p->pSat3 ? bmcg_sat_solver_varnum(p->pSat3) : satoko_varnum(p->pSat2)) );
100.0*nUsedVars/(p->pSat ? sat_solver_nvars(p->pSat) : p->pSat4 ? cadical_solver_nvars(p->pSat4) : p->pSat3 ? bmcg_sat_solver_varnum(p->pSat3) : satoko_varnum(p->pSat2)) );
Abc_Print( 1, "Buffs = %d. Dups = %d. Hash hits = %d. Hash misses = %d. UniProps = %d.\n",
p->nBufNum, p->nDupNum, p->nHashHit, p->nHashMiss, p->nUniProps );
}
@ -830,6 +845,7 @@ void Saig_Bmc3ManStop( Gia_ManBmc_t * p )
if ( p->pSat ) sat_solver_delete( p->pSat );
if ( p->pSat2 ) satoko_destroy( p->pSat2 );
if ( p->pSat3 ) bmcg_sat_solver_stop( p->pSat3 );
if ( p->pSat4 ) cadical_solver_delete( p->pSat4 );
ABC_FREE( p->pTime4Outs );
Vec_IntFree( p->vData );
Hsh_IntManStop( p->vHash );
@ -1029,6 +1045,11 @@ static inline void Saig_ManBmcAddClauses( Gia_ManBmc_t * p, int uTruth, int Lits
if ( !bmcg_sat_solver_addclause( p->pSat3, ClaLits, nClaLits ) )
assert( 0 );
}
else if ( p->pSat4 )
{
if ( !cadical_solver_addclause( p->pSat4, ClaLits, ClaLits+nClaLits ) )
assert( 0 );
}
else
{
if ( !sat_solver_addclause( p->pSat, ClaLits, ClaLits+nClaLits ) )
@ -1287,6 +1308,11 @@ int Saig_ManBmcCreateCnf( Gia_ManBmc_t * p, Aig_Obj_t * pObj, int iFrame )
for ( i = bmcg_sat_solver_varnum(p->pSat3); i < p->nSatVars; i++ )
bmcg_sat_solver_addvar( p->pSat3 );
}
else if ( p->pSat4 )
{
for ( i = cadical_solver_nvars(p->pSat4); i < p->nSatVars; i++ )
cadical_solver_addvar( p->pSat4 );
}
else
sat_solver_setnvars( p->pSat, p->nSatVars );
return Lit;
@ -1411,6 +1437,11 @@ Abc_Cex_t * Saig_ManGenerateCex( Gia_ManBmc_t * p, int f, int i )
if ( iLit != ~0 && bmcg_sat_solver_read_cex_varvalue(p->pSat3, lit_var(iLit)) )
Abc_InfoSetBit( pCex->pData, iBit + k );
}
else if ( p->pSat4)
{
if ( iLit != ~0 && cadical_solver_get_var_value(p->pSat4, lit_var(iLit)) )
Abc_InfoSetBit( pCex->pData, iBit + k );
}
else
{
if ( iLit != ~0 && sat_solver_var_value(p->pSat, lit_var(iLit)) )
@ -1445,6 +1476,10 @@ int Saig_ManCallSolver( Gia_ManBmc_t * p, int Lit )
bmcg_sat_solver_set_conflict_budget( p->pSat3, p->pPars->nConfLimit );
return bmcg_sat_solver_solve( p->pSat3, &Lit, 1 );
}
else if ( p->pSat4 )
{
return cadical_solver_solve( p->pSat4, &Lit, &Lit + 1, (ABC_INT64_T)p->pPars->nConfLimit, (ABC_INT64_T)0, (ABC_INT64_T)0, (ABC_INT64_T)0 );
}
else
return sat_solver_solve( p->pSat, &Lit, &Lit + 1, (ABC_INT64_T)p->pPars->nConfLimit, (ABC_INT64_T)0, (ABC_INT64_T)0, (ABC_INT64_T)0 );
}
@ -1482,7 +1517,7 @@ int Saig_ManBmcScalable( Aig_Man_t * pAig, Saig_ParBmc_t * pPars )
nTimeToStopNG = pPars->nTimeOut ? pPars->nTimeOut * CLOCKS_PER_SEC + Abc_Clock(): 0;
nTimeToStop = Saig_ManBmcTimeToStop( pPars, nTimeToStopNG );
// create BMC manager
p = Saig_Bmc3ManStart( pAig, pPars->nTimeOutOne, pPars->nConfLimit, pPars->fUseSatoko, pPars->fUseGlucose );
p = Saig_Bmc3ManStart( pAig, pPars->nTimeOutOne, pPars->nConfLimit, pPars->fUseSatoko, pPars->fUseGlucose, pPars->fUseCadical );
p->pPars = pPars;
if ( p->pSat )
{
@ -1498,6 +1533,10 @@ int Saig_ManBmcScalable( Aig_Man_t * pAig, Saig_ParBmc_t * pPars )
{
// satoko_set_runid(p->pSat3, p->pPars->RunId);
// satoko_set_stop_func(p->pSat3, p->pPars->pFuncStop);
}
else if ( p->pSat4 )
{
}
else
{
@ -1522,6 +1561,8 @@ int Saig_ManBmcScalable( Aig_Man_t * pAig, Saig_ParBmc_t * pPars )
satoko_set_runtime_limit( p->pSat2, nTimeToStop );
else if ( p->pSat3 )
bmcg_sat_solver_set_runtime_limit( p->pSat3, nTimeToStop );
else if ( p-> pSat4 )
Bmc3_CadicalSetRuntimeLimit( p->pSat4, nTimeToStop );
else
sat_solver_set_runtime_limit( p->pSat, nTimeToStop );
}
@ -1659,6 +1700,8 @@ clkOther += Abc_Clock() - clk2;
satoko_set_runtime_limit( p->pSat2, p->pTime4Outs[i] + Abc_Clock() );
else if ( p->pSat3 )
bmcg_sat_solver_set_runtime_limit( p->pSat3, p->pTime4Outs[i] + Abc_Clock() );
else if ( p-> pSat4 )
Bmc3_CadicalSetRuntimeLimit( p->pSat4, p->pTime4Outs[i] + Abc_Clock() );
else
sat_solver_set_runtime_limit( p->pSat, p->pTime4Outs[i] + Abc_Clock() );
}
@ -1690,6 +1733,8 @@ nTimeUnsat += clkSatRun;
status = satoko_add_clause( p->pSat2, &Lit, 1 );
else if ( p->pSat3 )
status = bmcg_sat_solver_addclause( p->pSat3, &Lit, 1 );
else if ( p->pSat4 )
status = cadical_solver_addclause( p->pSat4, &Lit, &Lit + 1 );
else
status = sat_solver_addclause( p->pSat, &Lit, &Lit + 1 );
assert( status );
@ -1721,12 +1766,12 @@ nTimeSat += clkSatRun;
{
Abc_Print( 1, "%4d %s : ", f, fUnfinished ? "-" : "+" );
Abc_Print( 1, "Var =%8.0f. ", (double)p->nSatVars );
Abc_Print( 1, "Cla =%9.0f. ", (double)(p->pSat ? p->pSat->stats.clauses : p->pSat3 ? bmcg_sat_solver_clausenum(p->pSat3) : satoko_clausenum(p->pSat2)) );
Abc_Print( 1, "Conf =%7.0f. ", (double)(p->pSat ? p->pSat->stats.conflicts : p->pSat3 ? bmcg_sat_solver_conflictnum(p->pSat3) : satoko_conflictnum(p->pSat2)) );
Abc_Print( 1, "Cla =%9.0f. ", (double)(p->pSat ? p->pSat->stats.clauses : p->pSat4 ? cadical_solver_nclauses(p->pSat4) : p->pSat3 ? bmcg_sat_solver_clausenum(p->pSat3) : satoko_clausenum(p->pSat2)) );
Abc_Print( 1, "Conf =%7.0f. ", (double)(p->pSat ? p->pSat->stats.conflicts : p->pSat4 ? cadical_solver_nconflicts(p->pSat4) : p->pSat3 ? bmcg_sat_solver_conflictnum(p->pSat3) : satoko_conflictnum(p->pSat2)) );
// Abc_Print( 1, "Imp =%10.0f. ", (double)p->pSat->stats.propagations );
// Abc_Print( 1, "Uni =%7.0f. ",(double)(p->pSat ? sat_solver_count_assigned(p->pSat) : 0) );
// ABC_PRT( "Time", Abc_Clock() - clk );
Abc_Print( 1, "Learn =%7.0f. ", (double)(p->pSat ? p->pSat->stats.learnts : p->pSat3 ? bmcg_sat_solver_learntnum(p->pSat3) : satoko_learntnum(p->pSat2)) );
Abc_Print( 1, "Learn =%7.0f. ", (double)(p->pSat ? p->pSat->stats.learnts : p->pSat4 ? cadical_solver_nlearned(p->pSat4) : p->pSat3 ? bmcg_sat_solver_learntnum(p->pSat3) : satoko_learntnum(p->pSat2)) );
Abc_Print( 1, "%4.0f MB", 4.25*(f+1)*p->nObjNums /(1<<20) );
Abc_Print( 1, "%4.0f MB", 1.0*(p->pSat ? sat_solver_memory(p->pSat) : 0)/(1<<20) );
Abc_Print( 1, "%9.2f sec ", (float)(Abc_Clock() - clkTotal)/(float)(CLOCKS_PER_SEC) );
@ -1773,6 +1818,8 @@ nTimeSat += clkSatRun;
satoko_set_runtime_limit( p->pSat2, nTimeToStop );
else if ( p->pSat3 )
bmcg_sat_solver_set_runtime_limit( p->pSat3, nTimeToStop );
else if ( p->pSat4 )
Bmc3_CadicalSetRuntimeLimit ( p->pSat4, nTimeToStop );
else
sat_solver_set_runtime_limit( p->pSat, nTimeToStop );
}
@ -1798,6 +1845,11 @@ nTimeSat += clkSatRun;
if ( bmcg_sat_solver_read_cex_varvalue(p->pSat3, lit_var(Lit)) == Abc_LitIsCompl(Lit) )
continue;
}
else if (p->pSat4)
{
if ( cadical_solver_get_var_value(p->pSat4, lit_var(Lit)) == Abc_LitIsCompl(Lit) )
continue;
}
else
{
if ( sat_solver_var_value(p->pSat, lit_var(Lit)) == Abc_LitIsCompl(Lit) )
@ -1841,7 +1893,7 @@ nTimeUndec += clkSatRun;
}
if ( pPars->fVerbose )
{
if ( fFirst == 1 && f > 0 && (p->pSat ? p->pSat->stats.conflicts : p->pSat3 ? bmcg_sat_solver_conflictnum(p->pSat3) : satoko_conflictnum(p->pSat2)) > 1 )
if ( fFirst == 1 && f > 0 && (p->pSat ? p->pSat->stats.conflicts : p->pSat4 ? cadical_solver_nconflicts(p->pSat4) : p->pSat3 ? bmcg_sat_solver_conflictnum(p->pSat3) : satoko_conflictnum(p->pSat2)) > 1 )
{
fFirst = 0;
// Abc_Print( 1, "Outputs of frames up to %d are trivially UNSAT.\n", f );
@ -1849,11 +1901,11 @@ nTimeUndec += clkSatRun;
Abc_Print( 1, "%4d %s : ", f, fUnfinished ? "-" : "+" );
Abc_Print( 1, "Var =%8.0f. ", (double)p->nSatVars );
// Abc_Print( 1, "Used =%8.0f. ", (double)sat_solver_count_usedvars(p->pSat) );
Abc_Print( 1, "Cla =%9.0f. ", (double)(p->pSat ? p->pSat->stats.clauses : p->pSat3 ? bmcg_sat_solver_clausenum(p->pSat3) : satoko_clausenum(p->pSat2)) );
Abc_Print( 1, "Conf =%7.0f. ",(double)(p->pSat ? p->pSat->stats.conflicts : p->pSat3 ? bmcg_sat_solver_conflictnum(p->pSat3) : satoko_conflictnum(p->pSat2)) );
Abc_Print( 1, "Cla =%9.0f. ", (double)(p->pSat ? p->pSat->stats.clauses : p->pSat4 ? cadical_solver_nclauses(p->pSat4) : p->pSat3 ? bmcg_sat_solver_clausenum(p->pSat3) : satoko_clausenum(p->pSat2)) );
Abc_Print( 1, "Conf =%7.0f. ",(double)(p->pSat ? p->pSat->stats.conflicts : p->pSat4 ? cadical_solver_nconflicts(p->pSat4) : p->pSat3 ? bmcg_sat_solver_conflictnum(p->pSat3) : satoko_conflictnum(p->pSat2)) );
// Abc_Print( 1, "Imp =%10.0f. ", (double)p->pSat->stats.propagations );
// Abc_Print( 1, "Uni =%7.0f. ", (double)(p->pSat ? sat_solver_count_assigned(p->pSat) : 0) );
Abc_Print( 1, "Learn =%7.0f. ", (double)(p->pSat ? p->pSat->stats.learnts : p->pSat3 ? bmcg_sat_solver_learntnum(p->pSat3) : satoko_learntnum(p->pSat2)) );
Abc_Print( 1, "Learn =%7.0f. ", (double)(p->pSat ? p->pSat->stats.learnts : p->pSat4 ? cadical_solver_nlearned(p->pSat4) : p->pSat3 ? bmcg_sat_solver_learntnum(p->pSat3) : satoko_learntnum(p->pSat2)) );
if ( pPars->fSolveAll )
Abc_Print( 1, "CEX =%5d. ", pPars->nFailOuts );
if ( pPars->nTimeOutOne )

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

@ -488,7 +488,8 @@ int Exa_ManMarkup( Exa_Man_t * p )
}
}
}
printf( "The number of parameter variables = %d.\n", p->iVar );
if ( !p->pPars->fSilent )
printf( "The number of parameter variables = %d.\n", p->iVar );
return p->iVar;
// printout
for ( i = p->nVars; i < p->nObjs; i++ )
@ -569,6 +570,18 @@ static inline int Exa_ManFindFanin( Exa_Man_t * p, int i, int k )
assert( Count == 1 );
return iVar;
}
static inline char * Exa_ManObjName( Exa_Man_t * p, int iObj, char * pBuffer )
{
if ( iObj < 0 )
sprintf( pBuffer, "*" );
else if ( iObj < p->nVars )
sprintf( pBuffer, "%c", 'a' + iObj );
else if ( iObj - p->nVars < 26 )
sprintf( pBuffer, "%c", 'A' + iObj - p->nVars );
else
sprintf( pBuffer, "N%d", iObj - p->nVars );
return pBuffer;
}
static inline int Exa_ManEval( Exa_Man_t * p )
{
static int Flag = 0;
@ -637,20 +650,18 @@ void Exa_ManDumpBlif( Exa_Man_t * p, int fCompl )
int Val1 = bmcg_sat_solver_read_cex_varvalue(p->pSat, iVarStart);
int Val2 = bmcg_sat_solver_read_cex_varvalue(p->pSat, iVarStart+1);
int Val3 = bmcg_sat_solver_read_cex_varvalue(p->pSat, iVarStart+2);
char Name[16];
fprintf( pFile, ".names" );
for ( k = 1; k >= 0; k-- )
{
iVar = Exa_ManFindFanin( p, i, k );
if ( iVar >= 0 && iVar < p->nVars )
fprintf( pFile, " %c", 'a'+iVar );
else
fprintf( pFile, " %02d", iVar );
fprintf( pFile, " %s", Exa_ManObjName(p, iVar, Name) );
}
if ( i == p->nObjs - 1 )
fprintf( pFile, " F\n" );
else
fprintf( pFile, " %02d\n", i );
fprintf( pFile, " %s\n", Exa_ManObjName(p, i, Name) );
if ( i == p->nObjs - 1 && fCompl )
fprintf( pFile, "00 1\n" );
if ( (i == p->nObjs - 1 && fCompl) ^ Val1 )
@ -668,6 +679,7 @@ void Exa_ManDumpBlif( Exa_Man_t * p, int fCompl )
void Exa_ManPrintSolution( Exa_Man_t * p, int fCompl )
{
int i, k, iVar;
char Name[16];
printf( "Realization of given %d-input function using %d two-input gates:\n", p->nVars, p->nNodes );
// for ( i = p->nVars + 2; i < p->nObjs; i++ )
for ( i = p->nObjs - 1; i >= p->nVars; i-- )
@ -677,20 +689,107 @@ void Exa_ManPrintSolution( Exa_Man_t * p, int fCompl )
int Val2 = bmcg_sat_solver_read_cex_varvalue(p->pSat, iVarStart+1);
int Val3 = bmcg_sat_solver_read_cex_varvalue(p->pSat, iVarStart+2);
if ( i == p->nObjs - 1 && fCompl )
printf( "%02d = 4\'b%d%d%d1(", i, !Val3, !Val2, !Val1 );
printf( "%s = 4\'b%d%d%d1(", Exa_ManObjName(p, i, Name), !Val3, !Val2, !Val1 );
else
printf( "%02d = 4\'b%d%d%d0(", i, Val3, Val2, Val1 );
printf( "%s = 4\'b%d%d%d0(", Exa_ManObjName(p, i, Name), Val3, Val2, Val1 );
for ( k = 1; k >= 0; k-- )
{
iVar = Exa_ManFindFanin( p, i, k );
if ( iVar >= 0 && iVar < p->nVars )
printf( " %c", 'a'+iVar );
else
printf( " %02d", iVar );
printf( " %s", Exa_ManObjName(p, iVar, Name) );
}
printf( " )\n" );
}
}
static inline int Exa_ManPermFanin( Exa_Man_t * p, int i, int k )
{
char * pPermStr = p->pPars->pPermStr;
int iTarget = 2 * (i - p->nVars) + (k ? 0 : 1);
int nSeen = 0;
char * pToken;
if ( p->pPars->pPermFans )
return p->pPars->pPermFans[iTarget];
assert( pPermStr != NULL );
for ( pToken = pPermStr; *pToken; )
{
int iObj = -2;
if ( *pToken == '_' )
{
pToken++;
continue;
}
if ( *pToken == '*' )
{
iObj = -1;
pToken++;
}
else if ( *pToken >= 'a' && *pToken < 'a' + p->nVars )
iObj = *pToken++ - 'a';
else if ( *pToken >= 'A' && *pToken <= 'Z' )
iObj = p->nVars + (*pToken++ - 'A');
else if ( *pToken == 'N' )
{
char * pNext = pToken + 1;
int Num = 0;
assert( *pNext >= '0' && *pNext <= '9' );
while ( *pNext >= '0' && *pNext <= '9' )
Num = 10 * Num + *pNext++ - '0';
iObj = p->nVars + Num;
pToken = pNext;
}
else
assert( 0 );
if ( nSeen++ == iTarget )
return iObj;
}
assert( 0 );
return -1;
}
static void Exa_ManPrintPermFanin( Exa_Man_t * p, int iFanin )
{
char Name[16];
printf( "%s ", Exa_ManObjName(p, iFanin, Name) );
}
static void Exa_ManPrintFixedPerm( Exa_Man_t * p )
{
int i, k;
char Name[16];
if ( (p->pPars->pPermStr == NULL && p->pPars->pPermFans == NULL) || p->pPars->fSilent )
return;
printf( "Using fixed input assignment provided by the user %s:\n", p->pPars->pPermStr ? p->pPars->pPermStr : "" );
for ( i = p->nObjs - 1; i >= p->nVars; i-- )
{
printf( "%s : ", Exa_ManObjName(p, i, Name) );
for ( k = 1; k >= 0; k-- )
Exa_ManPrintPermFanin( p, Exa_ManPermFanin(p, i, k) );
printf( "\n" );
}
}
static void Exa_ManPrintPerm( Exa_Man_t * p )
{
int i, k, iVar;
char Name[16];
printf( "The variable permutation is \"" );
for ( i = p->nVars; i < p->nObjs; i++ )
{
if ( i > p->nVars )
printf( "_" );
for ( k = 1; k >= 0; k-- )
{
iVar = Exa_ManFindFanin( p, i, k );
printf( "%s", Exa_ManObjName(p, iVar, Name) );
}
}
printf( "\".\n" );
}
static void Exa_ManSaveSolution( Exa_Man_t * p )
{
int i, k, Pos = 0;
ABC_FREE( p->pPars->pSolFans );
p->pPars->pSolFans = ABC_ALLOC( int, 2 * p->nNodes );
for ( i = p->nVars; i < p->nObjs; i++ )
for ( k = 1; k >= 0; k-- )
p->pPars->pSolFans[Pos++] = Exa_ManFindFanin( p, i, k );
}
/**Function*************************************************************
@ -716,6 +815,39 @@ static inline int Exa_ManAddClause( Exa_Man_t * p, int * pLits, int nLits )
}
return bmcg_sat_solver_addclause( p->pSat, pLits, nLits );
}
static int Exa_ManAddPermConstr( Exa_Man_t * p )
{
int i, k, iVar, Lit;
char Name0[16], Name1[16];
if ( p->pPars->pPermStr == NULL && p->pPars->pPermFans == NULL )
return 1;
Exa_ManPrintFixedPerm( p );
for ( i = p->nVars; i < p->nObjs; i++ )
{
for ( k = 0; k < 2; k++ )
{
iVar = Exa_ManPermFanin( p, i, k );
if ( iVar == -1 )
continue;
if ( iVar < 0 || iVar >= p->nVars || p->VarMarks[i][k][iVar] == 0 )
{
if ( iVar >= p->nVars && iVar < i && p->VarMarks[i][k][iVar] )
{
Lit = Abc_Var2Lit( p->VarMarks[i][k][iVar], 0 );
if ( !Exa_ManAddClause( p, &Lit, 1 ) )
return 0;
continue;
}
printf( "Cannot force node %s fanin %d to object %s because this connection is not available.\n", Exa_ManObjName(p, i, Name0), k, Exa_ManObjName(p, iVar, Name1) );
return 0;
}
Lit = Abc_Var2Lit( p->VarMarks[i][k][iVar], 0 );
if ( !Exa_ManAddClause( p, &Lit, 1 ) )
return 0;
}
}
return 1;
}
int Exa_ManAddCnfAdd( Exa_Man_t * p, int * pnAdded )
{
int pLits[MAJ_NOBJS], pLits2[2], i, j, k, n, m;
@ -794,6 +926,8 @@ int Exa_ManAddCnfStart( Exa_Man_t * p, int fOnlyAnd )
assert( n == p->nVars + p->nNodes );
Vec_IntFreeP( &vRes );
}
if ( !Exa_ManAddPermConstr(p) )
return 0;
// input constraints
for ( i = p->nVars; i < p->nObjs; i++ )
{
@ -946,9 +1080,10 @@ int Exa_ManAddCnf( Exa_Man_t * p, int iMint )
p->iVar += 3*p->nNodes;
return 1;
}
void Exa_ManExactSynthesis( Bmc_EsPar_t * pPars )
int Exa_ManExactSynthesis( Bmc_EsPar_t * pPars )
{
int i, status, iMint = 1;
int fFound = 0;
abctime clkTotal = Abc_Clock();
Exa_Man_t * p; int fCompl = 0;
word pTruth[64]; Abc_TtReadHex( pTruth, pPars->pTtStr );
@ -956,8 +1091,13 @@ void Exa_ManExactSynthesis( Bmc_EsPar_t * pPars )
p = Exa_ManAlloc( pPars, pTruth );
if ( pTruth[0] & 1 ) { fCompl = 1; Abc_TtNot( pTruth, p->nWords ); }
status = Exa_ManAddCnfStart( p, pPars->fOnlyAnd );
assert( status );
printf( "Running exact synthesis for %d-input function with %d two-input gates...\n", p->nVars, p->nNodes );
if ( !status )
{
Exa_ManFree( p );
return 0;
}
if ( !pPars->fSilent )
printf( "Running exact synthesis for %d-input function with %d two-input gates...\n", p->nVars, p->nNodes );
for ( i = 0; iMint != -1; i++ )
{
abctime clk = Abc_Clock();
@ -978,23 +1118,33 @@ void Exa_ManExactSynthesis( Bmc_EsPar_t * pPars )
}
if ( status == GLUCOSE_UNSAT )
{
printf( "The problem has no solution.\n" );
if ( !pPars->fSilent )
printf( "The problem has no solution.\n" );
break;
}
if ( status == GLUCOSE_UNDEC )
{
printf( "The solver timed out after %d sec.\n", pPars->RuntimeLim );
if ( !pPars->fSilent )
printf( "The solver timed out after %d sec.\n", pPars->RuntimeLim );
break;
}
iMint = Exa_ManEval( p );
}
if ( iMint == -1 )
{
Exa_ManPrintSolution( p, fCompl );
Exa_ManDumpBlif( p, fCompl );
Exa_ManSaveSolution( p );
if ( !pPars->fSilent )
{
Exa_ManPrintSolution( p, fCompl );
Exa_ManPrintPerm( p );
Exa_ManDumpBlif( p, fCompl );
}
fFound = 1;
}
Exa_ManFree( p );
Abc_PrintTime( 1, "Total runtime", Abc_Clock() - clkTotal );
if ( !pPars->fSilent )
Abc_PrintTime( 1, "Total runtime", Abc_Clock() - clkTotal );
return fFound;
}

179
src/sat/bmc/bmcMaj2.c
View File

@ -577,7 +577,8 @@ static int Exa_ManMarkup( Exa_Man_t * p )
}
}
}
printf( "The number of parameter variables = %d.\n", p->iVar );
if ( !p->pPars->fSilent )
printf( "The number of parameter variables = %d.\n", p->iVar );
return p->iVar;
// printout
for ( i = p->nVars; i < p->nObjs; i++ )
@ -640,6 +641,18 @@ static inline int Exa_ManFindFanin( Exa_Man_t * p, int i, int k )
assert( Count == 1 );
return iVar;
}
static inline char * Exa_ManObjName( Exa_Man_t * p, int iObj, char * pBuffer )
{
if ( iObj < 0 )
sprintf( pBuffer, "*" );
else if ( iObj < p->nVars )
sprintf( pBuffer, "%c", 'a' + iObj );
else if ( iObj - p->nVars < 26 )
sprintf( pBuffer, "%c", 'A' + iObj - p->nVars );
else
sprintf( pBuffer, "N%d", iObj - p->nVars );
return pBuffer;
}
static inline int Exa_ManEval( Exa_Man_t * p )
{
static int Flag = 0;
@ -681,6 +694,7 @@ static inline int Exa_ManEval( Exa_Man_t * p )
static void Exa_ManPrintSolution( Exa_Man_t * p, int fCompl )
{
int i, k, iVar;
char Name[16];
printf( "Realization of given %d-input function using %d two-input gates:\n", p->nVars, p->nNodes );
// for ( i = p->nVars + 2; i < p->nObjs; i++ )
for ( i = p->nObjs - 1; i >= p->nVars; i-- )
@ -690,20 +704,140 @@ static void Exa_ManPrintSolution( Exa_Man_t * p, int fCompl )
int Val2 = sat_solver_var_value(p->pSat, iVarStart+1);
int Val3 = sat_solver_var_value(p->pSat, iVarStart+2);
if ( i == p->nObjs - 1 && fCompl )
printf( "%02d = 4\'b%d%d%d1(", i, !Val3, !Val2, !Val1 );
printf( "%s = 4\'b%d%d%d1(", Exa_ManObjName(p, i, Name), !Val3, !Val2, !Val1 );
else
printf( "%02d = 4\'b%d%d%d0(", i, Val3, Val2, Val1 );
printf( "%s = 4\'b%d%d%d0(", Exa_ManObjName(p, i, Name), Val3, Val2, Val1 );
for ( k = 1; k >= 0; k-- )
{
iVar = Exa_ManFindFanin( p, i, k );
if ( iVar >= 0 && iVar < p->nVars )
printf( " %c", 'a'+iVar );
else
printf( " %02d", iVar );
printf( " %s", Exa_ManObjName(p, iVar, Name) );
}
printf( " )\n" );
}
}
static inline int Exa_ManPermFanin( Exa_Man_t * p, int i, int k )
{
char * pPermStr = p->pPars->pPermStr;
int iTarget = 2 * (i - p->nVars) + (k ? 0 : 1);
int nSeen = 0;
char * pToken;
if ( p->pPars->pPermFans )
return p->pPars->pPermFans[iTarget];
assert( pPermStr != NULL );
for ( pToken = pPermStr; *pToken; )
{
int iObj = -2;
if ( *pToken == '_' )
{
pToken++;
continue;
}
if ( *pToken == '*' )
{
iObj = -1;
pToken++;
}
else if ( *pToken >= 'a' && *pToken < 'a' + p->nVars )
iObj = *pToken++ - 'a';
else if ( *pToken >= 'A' && *pToken <= 'Z' )
iObj = p->nVars + (*pToken++ - 'A');
else if ( *pToken == 'N' )
{
char * pNext = pToken + 1;
int Num = 0;
assert( *pNext >= '0' && *pNext <= '9' );
while ( *pNext >= '0' && *pNext <= '9' )
Num = 10 * Num + *pNext++ - '0';
iObj = p->nVars + Num;
pToken = pNext;
}
else
assert( 0 );
if ( nSeen++ == iTarget )
return iObj;
}
assert( 0 );
return -1;
}
static void Exa_ManPrintPermFanin( Exa_Man_t * p, int iFanin )
{
char Name[16];
printf( "%s ", Exa_ManObjName(p, iFanin, Name) );
}
static void Exa_ManPrintFixedPerm( Exa_Man_t * p )
{
int i, k;
char Name[16];
if ( (p->pPars->pPermStr == NULL && p->pPars->pPermFans == NULL) || p->pPars->fSilent )
return;
printf( "Using fixed input assignment provided by the user %s:\n", p->pPars->pPermStr ? p->pPars->pPermStr : "" );
for ( i = p->nObjs - 1; i >= p->nVars; i-- )
{
printf( "%s : ", Exa_ManObjName(p, i, Name) );
for ( k = 1; k >= 0; k-- )
Exa_ManPrintPermFanin( p, Exa_ManPermFanin(p, i, k) );
printf( "\n" );
}
}
static void Exa_ManPrintPerm( Exa_Man_t * p )
{
int i, k, iVar;
char Name[16];
printf( "The variable permutation is \"" );
for ( i = p->nVars; i < p->nObjs; i++ )
{
if ( i > p->nVars )
printf( "_" );
for ( k = 1; k >= 0; k-- )
{
iVar = Exa_ManFindFanin( p, i, k );
printf( "%s", Exa_ManObjName(p, iVar, Name) );
}
}
printf( "\".\n" );
}
static void Exa_ManSaveSolution( Exa_Man_t * p )
{
int i, k, Pos = 0;
ABC_FREE( p->pPars->pSolFans );
p->pPars->pSolFans = ABC_ALLOC( int, 2 * p->nNodes );
for ( i = p->nVars; i < p->nObjs; i++ )
for ( k = 1; k >= 0; k-- )
p->pPars->pSolFans[Pos++] = Exa_ManFindFanin( p, i, k );
}
static int Exa_ManAddPermConstr( Exa_Man_t * p )
{
int i, k, iVar, Lit;
char Name0[16], Name1[16];
if ( p->pPars->pPermStr == NULL && p->pPars->pPermFans == NULL )
return 1;
Exa_ManPrintFixedPerm( p );
for ( i = p->nVars; i < p->nObjs; i++ )
{
for ( k = 0; k < 2; k++ )
{
iVar = Exa_ManPermFanin( p, i, k );
if ( iVar == -1 )
continue;
if ( iVar < 0 || iVar >= p->nVars || p->VarMarks[i][k][iVar] == 0 )
{
if ( iVar >= p->nVars && iVar < i && p->VarMarks[i][k][iVar] )
{
Lit = Abc_Var2Lit( p->VarMarks[i][k][iVar], 0 );
if ( !sat_solver_addclause( p->pSat, &Lit, &Lit + 1 ) )
return 0;
continue;
}
printf( "Cannot force node %s fanin %d to object %s because this connection is not available.\n", Exa_ManObjName(p, i, Name0), k, Exa_ManObjName(p, iVar, Name1) );
return 0;
}
Lit = Abc_Var2Lit( p->VarMarks[i][k][iVar], 0 );
if ( !sat_solver_addclause( p->pSat, &Lit, &Lit + 1 ) )
return 0;
}
}
return 1;
}
/**Function*************************************************************
@ -720,6 +854,8 @@ static void Exa_ManPrintSolution( Exa_Man_t * p, int fCompl )
static int Exa_ManAddCnfStart( Exa_Man_t * p, int fOnlyAnd )
{
int pLits[MAJ_NOBJS], pLits2[2], i, j, k, n, m;
if ( !Exa_ManAddPermConstr(p) )
return 0;
// input constraints
for ( i = p->nVars; i < p->nObjs; i++ )
{
@ -849,9 +985,10 @@ static int Exa_ManAddCnf( Exa_Man_t * p, int iMint )
p->iVar += 3*p->nNodes;
return 1;
}
void Exa_ManExactSynthesis2( Bmc_EsPar_t * pPars )
int Exa_ManExactSynthesis2( Bmc_EsPar_t * pPars )
{
int i, status, iMint = 1;
int fFound = 0;
abctime clkTotal = Abc_Clock();
Exa_Man_t * p; int fCompl = 0;
word pTruth[64]; Abc_TtReadHex( pTruth, pPars->pTtStr );
@ -859,8 +996,13 @@ void Exa_ManExactSynthesis2( Bmc_EsPar_t * pPars )
p = Exa_ManAlloc( pPars, pTruth );
if ( pTruth[0] & 1 ) { fCompl = 1; Abc_TtNot( pTruth, p->nWords ); }
status = Exa_ManAddCnfStart( p, pPars->fOnlyAnd );
assert( status );
printf( "Running exact synthesis for %d-input function with %d two-input gates...\n", p->nVars, p->nNodes );
if ( !status )
{
Exa_ManFree( p );
return 0;
}
if ( !pPars->fSilent )
printf( "Running exact synthesis for %d-input function with %d two-input gates...\n", p->nVars, p->nNodes );
for ( i = 0; iMint != -1; i++ )
{
abctime clk = Abc_Clock();
@ -878,15 +1020,26 @@ void Exa_ManExactSynthesis2( Bmc_EsPar_t * pPars )
}
if ( status == l_False )
{
printf( "The problem has no solution.\n" );
if ( !pPars->fSilent )
printf( "The problem has no solution.\n" );
break;
}
iMint = Exa_ManEval( p );
}
if ( iMint == -1 )
Exa_ManPrintSolution( p, fCompl );
{
Exa_ManSaveSolution( p );
if ( !pPars->fSilent )
{
Exa_ManPrintSolution( p, fCompl );
Exa_ManPrintPerm( p );
}
fFound = 1;
}
Exa_ManFree( p );
Abc_PrintTime( 1, "Total runtime", Abc_Clock() - clkTotal );
if ( !pPars->fSilent )
Abc_PrintTime( 1, "Total runtime", Abc_Clock() - clkTotal );
return fFound;
}

1
src/sat/cadical/cadical.hpp
View File

@ -1058,6 +1058,7 @@ public:
// Extra APIs
int clauses ();
int conflicts ();
int learned ();
private:
//==== start of state ====================================================

15
src/sat/cadical/cadicalSolver.c
View File

@ -297,6 +297,21 @@ int cadical_solver_nconflicts(cadical_solver* s) {
return ccadical_conflicts((CCaDiCaL*)s->p);
}
/**Function*************************************************************
Synopsis [get number of learned clauses]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
int cadical_solver_nlearned(cadical_solver* s) {
return ccadical_learned((CCaDiCaL*)s->p);
}
/**Function*************************************************************

1
src/sat/cadical/cadicalSolver.h
View File

@ -67,6 +67,7 @@ extern void cadical_solver_setnvars(cadical_solver* s,int n);
extern int cadical_solver_get_var_value(cadical_solver* s, int v);
extern int cadical_solver_nclauses(cadical_solver* s);
extern int cadical_solver_nconflicts(cadical_solver* s);
extern int cadical_solver_nlearned(cadical_solver* s);
extern Vec_Int_t * cadical_solve_cnf( Cnf_Dat_t * pCnf, char * pArgs, int nConfs, int nTimeLimit, int fSat, int fUnsat, int fPrintCex, int fVerbose );
ABC_NAMESPACE_HEADER_END

4
src/sat/cadical/cadical_ccadical.cpp
View File

@ -228,4 +228,8 @@ int ccadical_conflicts(CCaDiCaL *ptr) {
return ((Wrapper *) ptr)->solver->conflicts ();
}
int ccadical_learned(CCaDiCaL *ptr) {
return ((Wrapper *) ptr)->solver->learned ();
}
ABC_NAMESPACE_IMPL_END

4
src/sat/cadical/cadical_solver.cpp
View File

@ -1853,6 +1853,10 @@ int Solver::conflicts () {
return internal->stats.conflicts;
}
int Solver::learned () {
return internal->stats.learned.clauses;
}
} // namespace CaDiCaL
ABC_NAMESPACE_IMPL_END

1
src/sat/cadical/ccadical.h
View File

@ -63,6 +63,7 @@ void ccadical_resize(CCaDiCaL *, int min_max_var);
int ccadical_is_inconsistent(CCaDiCaL *);
int ccadical_clauses(CCaDiCaL *);
int ccadical_conflicts(CCaDiCaL *);
int ccadical_learned(CCaDiCaL *);
/*------------------------------------------------------------------------*/