diff options
Diffstat (limited to 'src')
| -rw-r--r-- | src/base/abci/abc.c | 51 | ||||
| -rw-r--r-- | src/sat/bmc/bmcMaj3.c | 304 |
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..f4949af5 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 = (int)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", (int)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 /// //////////////////////////////////////////////////////////////////////// |