summaryrefslogtreecommitdiffstats
diff options
context:
space:
mode:
authorAlan Mishchenko <alanmi@berkeley.edu>2018-01-04 22:33:29 -0800
committerAlan Mishchenko <alanmi@berkeley.edu>2018-01-04 22:33:29 -0800
commit834e24801982138ad0d466f47bc873aebe7030c5 (patch)
treee4a1ddce05695aec0a59b557db5d778052eb5446
parentf3dcf87cea40e92eb34a107719bce0f1b609351f (diff)
downloadabc-834e24801982138ad0d466f47bc873aebe7030c5.tar.gz
abc-834e24801982138ad0d466f47bc873aebe7030c5.tar.bz2
abc-834e24801982138ad0d466f47bc873aebe7030c5.zip
New command 'testexact'.
-rw-r--r--src/base/abci/abc.c51
-rw-r--r--src/sat/bmc/bmcMaj3.c304
2 files changed, 348 insertions, 7 deletions
diff --git a/src/base/abci/abc.c b/src/base/abci/abc.c
index a9988497..3467008a 100644
--- a/src/base/abci/abc.c
+++ b/src/base/abci/abc.c
@@ -153,6 +153,7 @@ static int Abc_CommandMajExact ( Abc_Frame_t * pAbc, int argc, cha
static int Abc_CommandTwoExact ( Abc_Frame_t * pAbc, int argc, char ** argv );
static int Abc_CommandLutExact ( Abc_Frame_t * pAbc, int argc, char ** argv );
static int Abc_CommandAllExact ( Abc_Frame_t * pAbc, int argc, char ** argv );
+static int Abc_CommandTestExact ( Abc_Frame_t * pAbc, int argc, char ** argv );
static int Abc_CommandLogic ( Abc_Frame_t * pAbc, int argc, char ** argv );
static int Abc_CommandComb ( Abc_Frame_t * pAbc, int argc, char ** argv );
@@ -823,6 +824,7 @@ void Abc_Init( Abc_Frame_t * pAbc )
Cmd_CommandAdd( pAbc, "Exact synthesis", "twoexact", Abc_CommandTwoExact, 0 );
Cmd_CommandAdd( pAbc, "Exact synthesis", "lutexact", Abc_CommandLutExact, 0 );
Cmd_CommandAdd( pAbc, "Exact synthesis", "allexact", Abc_CommandAllExact, 0 );
+ Cmd_CommandAdd( pAbc, "Exact synthesis", "testexact", Abc_CommandTestExact, 0 );
Cmd_CommandAdd( pAbc, "Various", "logic", Abc_CommandLogic, 1 );
Cmd_CommandAdd( pAbc, "Various", "comb", Abc_CommandComb, 1 );
@@ -8578,6 +8580,55 @@ usage:
SeeAlso []
***********************************************************************/
+int Abc_CommandTestExact( Abc_Frame_t * pAbc, int argc, char ** argv )
+{
+ extern void Zyx_TestExact( char * pFileName );
+ char * pFileName = NULL;
+ int c, fVerbose = 0;
+ Extra_UtilGetoptReset();
+ while ( ( c = Extra_UtilGetopt( argc, argv, "vh" ) ) != EOF )
+ {
+ switch ( c )
+ {
+ case 'v':
+ fVerbose ^= 1;
+ break;
+ case 'h':
+ goto usage;
+ default:
+ goto usage;
+ }
+ }
+ if ( argc == globalUtilOptind + 1 )
+ pFileName = argv[globalUtilOptind];
+ if ( pFileName == NULL )
+ {
+ Abc_Print( -1, "File name is not given on the command line.\n" );
+ return 1;
+ }
+ Zyx_TestExact( pFileName );
+ return 0;
+
+usage:
+ Abc_Print( -2, "usage: testexact <file>\n" );
+ Abc_Print( -2, "\t tests solution of the exact synthesis problem\n" );
+ Abc_Print( -2, "\t-v : toggle verbose printout [default = %s]\n", fVerbose ? "yes" : "no" );
+ Abc_Print( -2, "\t-h : print the command usage\n" );
+ Abc_Print( -2, "\t<file> : file name in the specified format\n" );
+ return 1;
+}
+
+/**Function*************************************************************
+
+ Synopsis []
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
int Abc_CommandLogic( Abc_Frame_t * pAbc, int argc, char ** argv )
{
Abc_Ntk_t * pNtk, * pNtkRes;
diff --git a/src/sat/bmc/bmcMaj3.c b/src/sat/bmc/bmcMaj3.c
index bc77791d..0732da2a 100644
--- a/src/sat/bmc/bmcMaj3.c
+++ b/src/sat/bmc/bmcMaj3.c
@@ -22,6 +22,7 @@
#include "misc/extra/extra.h"
#include "misc/util/utilTruth.h"
#include "sat/glucose/AbcGlucose.h"
+#include "opt/dau/dau.h"
ABC_NAMESPACE_IMPL_START
@@ -562,6 +563,7 @@ struct Zyx_Man_t_
Vec_Int_t * vMidMints; // middle minterms
Vec_Bit_t * vUsed2; // bit masks
Vec_Bit_t * vUsed3; // bit masks
+ Vec_Int_t * vPairs; // sym var pairs
int nUsed[2];
int pFanins[MAJ3_OBJS][MAJ3_OBJS]; // fanins
int pLits[2][2*MAJ3_OBJS]; // neg/pos literals
@@ -765,6 +767,27 @@ Vec_Wrd_t * Zyx_ManTruthTables( Zyx_Man_t * p, word * pTruth )
//Dau_DsdPrintFromTruth( Zyx_ManTruth(p, p->nObjs), p->pPars->nVars );
return vInfo;
}
+Vec_Int_t * Zyx_ManCreateSymVarPairs( word * pTruth, int nVars )
+{
+ Vec_Int_t * vPairs = Vec_IntAlloc( 100 );
+ int i, k, nWords = Abc_TtWordNum(nVars);
+ word Cof0[64], Cof1[64];
+ word Cof01[64], Cof10[64];
+ assert( nVars <= 12 );
+ for ( i = 0; i < nVars; i++ )
+ {
+ Abc_TtCofactor0p( Cof0, pTruth, nWords, i );
+ Abc_TtCofactor1p( Cof1, pTruth, nWords, i );
+ for ( k = i+1; k < nVars; k++ )
+ {
+ Abc_TtCofactor1p( Cof01, Cof0, nWords, k );
+ Abc_TtCofactor0p( Cof10, Cof1, nWords, k );
+ if ( Abc_TtEqual( Cof01, Cof10, nWords ) )
+ Vec_IntPushTwo( vPairs, i, k );
+ }
+ }
+ return vPairs;
+}
Zyx_Man_t * Zyx_ManAlloc( Bmc_EsPar_t * pPars, word * pTruth )
{
Zyx_Man_t * p = ABC_CALLOC( Zyx_Man_t, 1 );
@@ -782,6 +805,7 @@ Zyx_Man_t * Zyx_ManAlloc( Bmc_EsPar_t * pPars, word * pTruth )
p->vUsed2 = Vec_BitStart( (1 << p->pPars->nVars) * p->pPars->nNodes * p->nObjs * p->nObjs );
else if ( p->pPars->nLutSize == 3 )
p->vUsed3 = Vec_BitStart( (1 << p->pPars->nVars) * p->pPars->nNodes * p->nObjs * p->nObjs * p->nObjs );
+ p->vPairs = Zyx_ManCreateSymVarPairs( p->pPars->fMajority ? Zyx_ManTruth(p, p->nObjs) : pTruth, p->pPars->nVars );
p->pSat = bmcg_sat_solver_start();
bmcg_sat_solver_set_nvars( p->pSat, p->MintBase + (1 << p->pPars->nVars) * p->nObjs );
Zyx_ManSetupVars( p );
@@ -795,6 +819,7 @@ void Zyx_ManFree( Zyx_Man_t * p )
Vec_WrdFree( p->vInfo );
Vec_BitFreeP( &p->vUsed2 );
Vec_BitFreeP( &p->vUsed3 );
+ Vec_IntFree( p->vPairs );
Vec_IntFree( p->vMidMints );
Vec_IntFree( p->vVarValues );
ABC_FREE( p );
@@ -826,7 +851,7 @@ int Zyx_ManCollectFanins( Zyx_Man_t * p, int i )
}
int Zyx_ManAddCnfLazyTopo( Zyx_Man_t * p )
{
- int i, k, j, nLazy = 0;
+ int i, k, j, Entry[2], Node[2], nLazy = 0;
// fanin count
//printf( "Adding topology clauses.\n" );
for ( i = p->pPars->nVars; i < p->nObjs; i++ )
@@ -858,12 +883,37 @@ int Zyx_ManAddCnfLazyTopo( Zyx_Man_t * p )
for ( k = p->pPars->nLutSize - 1; k >= 0; k-- )
if ( p->pFanins[i-1][k] != p->pFanins[i][k] )
break;
- if ( k == -1 )
+ if ( k == -1 ) // fanins are equal
{
- if ( !p->pPars->fMajority )
+ if ( p->pPars->fMajority )
+ continue;
+ // compare by LUT functions
+ for ( k = p->LutMask; k >= 0; k-- )
+ if ( bmcg_sat_solver_read_cex_varvalue(p->pSat, Zyx_FuncVar(p, i-1, k)) !=
+ bmcg_sat_solver_read_cex_varvalue(p->pSat, Zyx_FuncVar(p, i , k)) )
+ break;
+ if ( k == -1 ) // truth tables cannot be equal
+ continue;
+ // rule out these truth tables
+ if ( bmcg_sat_solver_read_cex_varvalue(p->pSat, Zyx_FuncVar(p, i-1, k)) == 0 &&
+ bmcg_sat_solver_read_cex_varvalue(p->pSat, Zyx_FuncVar(p, i , k)) == 1 )
{
- // compare by LUT functions
+ continue;
}
+ nLazy++;
+ assert( bmcg_sat_solver_read_cex_varvalue(p->pSat, Zyx_FuncVar(p, i-1, k)) == 1 );
+ assert( bmcg_sat_solver_read_cex_varvalue(p->pSat, Zyx_FuncVar(p, i , k)) == 0 );
+ // rule out this order
+ p->nLits[0] = 0;
+ for ( j = p->LutMask; j >= k; j-- )
+ {
+ int ValA = bmcg_sat_solver_read_cex_varvalue(p->pSat, Zyx_FuncVar(p, i-1, j));
+ int ValB = bmcg_sat_solver_read_cex_varvalue(p->pSat, Zyx_FuncVar(p, i, j));
+ p->pLits[0][p->nLits[0]++] = Abc_Var2Lit(Zyx_FuncVar(p, i-1, j), ValA );
+ p->pLits[0][p->nLits[0]++] = Abc_Var2Lit(Zyx_FuncVar(p, i, j), ValB );
+ }
+ if ( !bmcg_sat_solver_addclause( p->pSat, p->pLits[0], p->nLits[0] ) )
+ return -1;
continue;
}
if ( p->pFanins[i-1][k] < p->pFanins[i][k] )
@@ -891,6 +941,41 @@ int Zyx_ManAddCnfLazyTopo( Zyx_Man_t * p )
return -1;
//break;
}
+ // check symmetric variables
+ Vec_IntForEachEntryDouble( p->vPairs, Entry[0], Entry[1], k )
+ {
+ assert( Entry[0] < Entry[1] );
+ for ( j = 0; j < 2; j++ )
+ {
+ Node[j] = -1;
+ for ( i = p->pPars->nVars; i < p->nObjs; i++ )
+ if ( bmcg_sat_solver_read_cex_varvalue(p->pSat, Zyx_TopoVar(p, i, Entry[j])) )
+ {
+ Node[j] = i;
+ break;
+ }
+ assert( Node[j] >= p->pPars->nVars );
+ }
+ // compare the nodes
+ if ( Node[0] <= Node[1] )
+ continue;
+ assert( Node[0] > Node[1] );
+ // create blocking clause
+ nLazy++;
+ assert( bmcg_sat_solver_read_cex_varvalue(p->pSat, Zyx_TopoVar(p, Node[1], Entry[0])) == 0 );
+ assert( bmcg_sat_solver_read_cex_varvalue(p->pSat, Zyx_TopoVar(p, Node[1], Entry[1])) == 1 );
+ // rule out this order
+ p->nLits[0] = 0;
+ for ( j = p->pPars->nVars; j <= Node[1]; j++ )
+ {
+ int ValA = bmcg_sat_solver_read_cex_varvalue(p->pSat, Zyx_TopoVar(p, j, Entry[0]));
+ int ValB = bmcg_sat_solver_read_cex_varvalue(p->pSat, Zyx_TopoVar(p, j, Entry[1]));
+ p->pLits[0][p->nLits[0]++] = Abc_Var2Lit(Zyx_TopoVar(p, j, Entry[0]), ValA );
+ p->pLits[0][p->nLits[0]++] = Abc_Var2Lit(Zyx_TopoVar(p, j, Entry[1]), ValB );
+ }
+ if ( !bmcg_sat_solver_addclause( p->pSat, p->pLits[0], p->nLits[0] ) )
+ return -1;
+ }
return nLazy;
}
int Zyx_ManAddCnfBlockSolution( Zyx_Man_t * p )
@@ -977,7 +1062,45 @@ int Zyx_ManAddCnfLazyFunc( Zyx_Man_t * p, int iMint )
SeeAlso []
***********************************************************************/
-static void Zyx_ManPrintSolution( Zyx_Man_t * p, int fCompl )
+static void Zyx_ManPrintSolutionFile( Zyx_Man_t * p, int fCompl, int fFirst )
+{
+ FILE * pFile;
+ char FileName[1000]; int i, k;
+ if ( fCompl ) Abc_TtNot( p->pTruth, Abc_TtWordNum(p->pPars->nVars) );
+ Abc_TtWriteHexRev( FileName, p->pTruth, p->pPars->nVars );
+ if ( fCompl ) Abc_TtNot( p->pTruth, Abc_TtWordNum(p->pPars->nVars) );
+ sprintf( FileName + (1 << (p->pPars->nVars-2)), "-%d-%d.bool", p->pPars->nLutSize, p->pPars->nNodes );
+ pFile = fopen( FileName, fFirst ? "wb" : "ab" );
+ if ( pFile == NULL )
+ {
+ printf( "Cannot open input file \"%s\".\n", FileName );
+ return;
+ }
+ for ( i = p->pPars->nVars; i < p->nObjs; i++ )
+ {
+ fprintf( pFile, "%c", 'A' + i );
+ if ( p->pPars->fMajority )
+ fprintf( pFile, "maj3" );
+ else
+ {
+ for ( k = p->LutMask; k >= 0; k-- )
+ fprintf( pFile, "%d", bmcg_sat_solver_read_cex_varvalue(p->pSat, Zyx_FuncVar(p, i, k)) ^ (i == p->nObjs - 1 && fCompl) );
+ for ( k = 0; k < i; k++ )
+ if ( bmcg_sat_solver_read_cex_varvalue(p->pSat, Zyx_TopoVar(p, i, k)) )
+ {
+ if ( k >= 0 && k < p->pPars->nVars )
+ fprintf( pFile, "%c", 'a' + k );
+ else
+ fprintf( pFile, "%c", 'A' + k );
+ }
+ }
+ fprintf( pFile, "\n" );
+ }
+ fprintf( pFile, "\n" );
+ fclose( pFile );
+ printf( "Dumped solution into file \"%s\".\n", FileName );
+}
+static void Zyx_ManPrintSolution( Zyx_Man_t * p, int fCompl, int fFirst )
{
int i, k;
printf( "Realization of given %d-input function using %d %d-input %s:\n",
@@ -1004,6 +1127,8 @@ static void Zyx_ManPrintSolution( Zyx_Man_t * p, int fCompl )
}
printf( " )\n" );
}
+ if ( !p->pPars->fMajority )
+ Zyx_ManPrintSolutionFile( p, fCompl, fFirst );
}
static inline int Zyx_ManEval( Zyx_Man_t * p )
{
@@ -1115,7 +1240,7 @@ void Zyx_ManExactSynthesis( Bmc_EsPar_t * pPars )
Zyx_ManPrint( p, Iter, iMint, nLazyAll, Abc_Clock() - clkTotal );
clk = Abc_Clock();
}
- Zyx_ManPrintSolution( p, fCompl );
+ Zyx_ManPrintSolution( p, fCompl, nSols==1 );
if ( !Zyx_ManAddCnfBlockSolution( p ) )
{
status = GLUCOSE_UNSAT;
@@ -1146,7 +1271,7 @@ void Zyx_ManExactSynthesis( Bmc_EsPar_t * pPars )
if ( pPars->fEnumSols )
printf( "Finished enumerating %d solutions.\n", nSols );
else if ( iMint == -1 )
- Zyx_ManPrintSolution( p, fCompl );
+ Zyx_ManPrintSolution( p, fCompl, 1 );
else
printf( "The problem has no solution.\n" );
//Zyx_ManEvalStats( p );
@@ -1157,6 +1282,171 @@ void Zyx_ManExactSynthesis( Bmc_EsPar_t * pPars )
+/**Function*************************************************************
+
+ Synopsis [Tests solution to the exact synthesis problem.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+int Zyx_TestGetTruthTablePars( char * pFileName, word * pTruth, int * nVars, int * nLutSize, int * nNodes )
+{
+ char Symb, * pCur, * pBuffer = Abc_UtilStrsav( pFileName );
+ int nLength;
+ for ( pCur = pBuffer; *pCur; pCur++ )
+ if ( !Abc_TtIsHexDigit(*pCur) )
+ break;
+ Symb = *pCur; *pCur = 0;
+ nLength = strlen(pBuffer);
+ if ( nLength == 1 )
+ *nVars = 2;
+ else if ( nLength == 2 )
+ *nVars = 3;
+ else if ( nLength == 4 )
+ *nVars = 4;
+ else if ( nLength == 8 )
+ *nVars = 5;
+ else if ( nLength == 16 )
+ *nVars = 6;
+ else if ( nLength == 32 )
+ *nVars = 7;
+ else if ( nLength == 64 )
+ *nVars = 8;
+ else
+ {
+ ABC_FREE( pBuffer );
+ printf( "Invalid truth table size.\n" );
+ return 0;
+ }
+ Abc_TtReadHex( pTruth, pBuffer );
+ *pCur = Symb;
+ // read LUT size
+ while ( *pCur && *pCur++ != '-' );
+ if ( *pCur == 0 )
+ {
+ ABC_FREE( pBuffer );
+ printf( "Expecting \'-\' after truth table before LUT size.\n" );
+ return 0;
+ }
+ // read node count
+ *nLutSize = atoi(pCur);
+ while ( *pCur && *pCur++ != '-' );
+ if ( *pCur == 0 )
+ {
+ ABC_FREE( pBuffer );
+ printf( "Expecting \'-\' after LUT size before node count.\n" );
+ return 0;
+ }
+ *nNodes = atoi(pCur);
+ ABC_FREE( pBuffer );
+ return 1;
+}
+
+static inline word * Zyx_TestTruth( Vec_Wrd_t * vInfo, int i, int nWords ) { return Vec_WrdEntryP(vInfo, nWords * i); }
+
+Vec_Wrd_t * Zyx_TestCreateTruthTables( int nVars, int nNodes )
+{
+ int i, nWords = Abc_TtWordNum(nVars);
+ Vec_Wrd_t * vInfo = Vec_WrdStart( nWords * (nVars + nNodes + 1) );
+ for ( i = 0; i < nVars; i++ )
+ Abc_TtIthVar( Zyx_TestTruth(vInfo, i, nWords), i, nVars );
+ //Dau_DsdPrintFromTruth( Maj3_ManTruth(p, p->nObjs), p->nVars );
+ return vInfo;
+}
+int Zyx_TestReadNode( char * pLine, Vec_Wrd_t * vTruths, int nVars, int nLutSize, int iObj )
+{
+ int k, j, nWords = Abc_TtWordNum(nVars);
+ word * pFaninsW[6]; char * pTruth, * pFanins;
+ word * pThis, * pLast = Zyx_TestTruth( vTruths, Vec_WrdSize(vTruths)/nWords - 1, nWords );
+ if ( pLine[strlen(pLine)-1] == '\n' ) pLine[strlen(pLine)-1] = 0;
+ if ( pLine[strlen(pLine)-1] == '\r' ) pLine[strlen(pLine)-1] = 0;
+ if ( pLine[0] == 0 )
+ return 0;
+ if ( (int)strlen(pLine) != 1 + nLutSize + (1 << nLutSize) )
+ {
+ printf( "Node representation has %d chars (expecting %d chars).\n", strlen(pLine), 1 + nLutSize + (1 << nLutSize) );
+ return 0;
+ }
+ if ( pLine[0] != 'A' + iObj )
+ {
+ printf( "The output node in line %s is not correct.\n", pLine );
+ return 0;
+ }
+ pTruth = pLine + 1;
+ pFanins = pTruth + (1 << nLutSize);
+ for ( k = nLutSize - 1; k >= 0; k-- )
+ pFaninsW[k] = Zyx_TestTruth( vTruths, pFanins[k] >= 'a' ? pFanins[k] - 'a' : pFanins[k] - 'A', nWords );
+ pThis = Zyx_TestTruth(vTruths, iObj, nWords);
+ Abc_TtConst0( pThis, nWords );
+ for ( k = 0; k < (1 << nLutSize); k++ )
+ {
+ if ( pTruth[(1 << nLutSize) - 1 - k] == '0' )
+ continue;
+ Abc_TtConst1( pLast, nWords );
+ for ( j = 0; j < nLutSize; j++ )
+ Abc_TtAndCompl( pLast, pLast, 0, pFaninsW[j], !((k >> j) & 1), nWords );
+ Abc_TtOr( pThis, pThis, pLast, nWords );
+ }
+ //Dau_DsdPrintFromTruth( pThis, nVars );
+ return 1;
+}
+void Zyx_TestExact( char * pFileName )
+{
+ int iObj, nStrs = 0, nVars = -1, nLutSize = -1, nNodes = -1;
+ word * pImpl, pSpec[4]; Vec_Wrd_t * vInfo; char Line[1000];
+ FILE * pFile = fopen( pFileName, "rb" );
+ if ( pFile == NULL )
+ {
+ printf( "Cannot open input file \"%s\".\n", pFileName );
+ return;
+ }
+ if ( !Zyx_TestGetTruthTablePars( pFileName, pSpec, &nVars, &nLutSize, &nNodes ) )
+ return;
+ if ( nVars > 8 )
+ {
+ printf( "This tester does not support functions with more than 8 inputs.\n" );
+ return;
+ }
+ if ( nLutSize > 6 )
+ {
+ printf( "This tester does not support nodes with more than 6 inputs.\n" );
+ return;
+ }
+ if ( nNodes > 16 )
+ {
+ printf( "This tester does not support structures with more than 16 inputs.\n" );
+ return;
+ }
+ vInfo = Zyx_TestCreateTruthTables( nVars, nNodes );
+ for ( iObj = nVars; fgets(Line, 1000, pFile) != NULL; iObj++ )
+ {
+ if ( Zyx_TestReadNode( Line, vInfo, nVars, nLutSize, iObj ) )
+ continue;
+ if ( iObj != nVars + nNodes )
+ {
+ printf( "The number of nodes in the structure is not correct.\n" );
+ break;
+ }
+ nStrs++;
+ pImpl = Zyx_TestTruth( vInfo, iObj-1, Abc_TtWordNum(nVars) );
+ if ( Abc_TtEqual( pImpl, pSpec, Abc_TtWordNum(nVars) ) )
+ printf( "Structure %3d : Verification successful.\n", nStrs );
+ else
+ {
+ printf( "Structure %3d : Verification FAILED.\n", nStrs );
+ printf( "Implementation: " ); Dau_DsdPrintFromTruth( pImpl, nVars );
+ printf( "Specification: " ); Dau_DsdPrintFromTruth( pSpec, nVars );
+ }
+ iObj = nVars - 1;
+ }
+ Vec_WrdFree( vInfo );
+ fclose( pFile );
+}
+
////////////////////////////////////////////////////////////////////////
/// END OF FILE ///
////////////////////////////////////////////////////////////////////////