From 80fdd58c28d69beda41e504b6a9676d63248a866 Mon Sep 17 00:00:00 2001 From: Mathias Soeken Date: Thu, 28 Jul 2016 20:37:09 +0200 Subject: Several updates to exact synthesis. --- src/base/abci/abc.c | 76 ++++++-- src/base/abci/abcExact.c | 457 ++++++++++++++++++++++++++++++++++++++++------- 2 files changed, 458 insertions(+), 75 deletions(-) (limited to 'src/base/abci') diff --git a/src/base/abci/abc.c b/src/base/abci/abc.c index 74598b4b..244255da 100644 --- a/src/base/abci/abc.c +++ b/src/base/abci/abc.c @@ -7284,12 +7284,15 @@ usage: ***********************************************************************/ int Abc_CommandExact( Abc_Frame_t * pAbc, int argc, char ** argv ) { - int c, nMaxDepth = -1, fVerbose = 0, nVars; - word pTruth[1]; + extern Gia_Man_t * Gia_ManFindExact( word * pTruth, int nVars, int nFunc, int nMaxDepth, int * pArrivalTimes, int fVerbose ); + + int c, nMaxDepth = -1, fMakeAIG = 0, fTest = 0, fVerbose = 0, nVars = 0, nVarsTmp, nFunc = 0; + word pTruth[64]; Abc_Ntk_t * pNtkRes; + Gia_Man_t * pGiaRes; Extra_UtilGetoptReset(); - while ( ( c = Extra_UtilGetopt( argc, argv, "Dvh" ) ) != EOF ) + while ( ( c = Extra_UtilGetopt( argc, argv, "Datvh" ) ) != EOF ) { switch ( c ) { @@ -7304,6 +7307,12 @@ int Abc_CommandExact( Abc_Frame_t * pAbc, int argc, char ** argv ) if ( nMaxDepth < 0 ) goto usage; break; + case 'a': + fMakeAIG ^= 1; + break; + case 't': + fTest ^= 1; + break; case 'v': fVerbose ^= 1; break; @@ -7314,23 +7323,64 @@ int Abc_CommandExact( Abc_Frame_t * pAbc, int argc, char ** argv ) } } - if ( argc != globalUtilOptind + 1 ) + if ( fTest ) { + extern void Abc_ExactTest(); + + printf( "run test suite, ignore all other settings\n" ); + Abc_ExactTest( fVerbose ); + return 0; + } + + if ( argc == globalUtilOptind ) goto usage; + + memset( pTruth, 0, 64 ); + while ( globalUtilOptind < argc ) + { + if ( nFunc == 16 ) + { + Abc_Print( -1, "Too many functions (at most 16 supported).\n" ); + goto usage; + } + nVarsTmp = Abc_TtReadHex( &pTruth[nFunc << 2], argv[globalUtilOptind++] ); + nFunc++; + if ( nVars == 0 ) + nVars = nVarsTmp; + else if ( nVars > 8 ) + { + Abc_Print( -1, "Only 8-variable functions are supported.\n" ); + goto usage; + } + else if ( nVars != nVarsTmp ) + { + Abc_Print( -1, "All functions need to have the same size.\n" ); + goto usage; + } } - nVars = Abc_TtReadHex( pTruth, argv[globalUtilOptind] ); - pNtkRes = Abc_NtkFindExact( pTruth, nVars, 1, nMaxDepth, fVerbose ); - assert( pNtkRes != NULL ); - Abc_FrameReplaceCurrentNetwork( pAbc, pNtkRes ); - Abc_FrameClearVerifStatus( pAbc ); + if ( fMakeAIG ) + { + pGiaRes = Gia_ManFindExact( pTruth, nVars, nFunc, nMaxDepth, NULL, fVerbose ); + assert( pGiaRes != NULL ); + Abc_FrameUpdateGia( pAbc, pGiaRes ); + } + else + { + pNtkRes = Abc_NtkFindExact( pTruth, nVars, nFunc, nMaxDepth, NULL, fVerbose ); + assert( pNtkRes != NULL ); + Abc_FrameReplaceCurrentNetwork( pAbc, pNtkRes ); + Abc_FrameClearVerifStatus( pAbc ); + } return 0; usage: - Abc_Print( -2, "usage: exact [-vh] \n" ); - Abc_Print( -2, "\t finds optimum networks using SAT-based exact synthesis for hex truth table \n" ); - Abc_Print( -2, "\t-D : constrain maximum depth\n" ); - Abc_Print( -2, "\t-v : toggle verbose printout [default = %s]\n", fVerbose ? "yes": "no" ); + Abc_Print( -2, "usage: exact [-D ] [-atvh] ...\n" ); + Abc_Print( -2, "\t finds optimum networks using SAT-based exact synthesis for hex truth tables ...\n" ); + Abc_Print( -2, "\t-D : constrain maximum depth (if too low, algorithm may not terminate)\n" ); + Abc_Print( -2, "\t-a : create AIG [default = %s]\n", fMakeAIG ? "yes" : "no" ); + Abc_Print( -2, "\t-t : run test suite\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\n" ); Abc_Print( -2, "\t This command was contributed by Mathias Soeken from EPFL in July 2016.\n" ); diff --git a/src/base/abci/abcExact.c b/src/base/abci/abcExact.c index c721992b..1bb7973a 100644 --- a/src/base/abci/abcExact.c +++ b/src/base/abci/abcExact.c @@ -24,9 +24,11 @@ #include "base/abc/abc.h" +#include "aig/gia/gia.h" #include "misc/util/utilTruth.h" #include "misc/vec/vecInt.h" #include "misc/vec/vecPtr.h" +#include "proof/cec/cec.h" #include "sat/bsat/satSolver.h" ABC_NAMESPACE_IMPL_START @@ -36,6 +38,17 @@ ABC_NAMESPACE_IMPL_START /// DECLARATIONS /// //////////////////////////////////////////////////////////////////////// +static word s_Truths8[32] = { + ABC_CONST(0xAAAAAAAAAAAAAAAA), ABC_CONST(0xAAAAAAAAAAAAAAAA), ABC_CONST(0xAAAAAAAAAAAAAAAA), ABC_CONST(0xAAAAAAAAAAAAAAAA), + ABC_CONST(0xCCCCCCCCCCCCCCCC), ABC_CONST(0xCCCCCCCCCCCCCCCC), ABC_CONST(0xCCCCCCCCCCCCCCCC), ABC_CONST(0xCCCCCCCCCCCCCCCC), + ABC_CONST(0xF0F0F0F0F0F0F0F0), ABC_CONST(0xF0F0F0F0F0F0F0F0), ABC_CONST(0xF0F0F0F0F0F0F0F0), ABC_CONST(0xF0F0F0F0F0F0F0F0), + ABC_CONST(0xFF00FF00FF00FF00), ABC_CONST(0xFF00FF00FF00FF00), ABC_CONST(0xFF00FF00FF00FF00), ABC_CONST(0xFF00FF00FF00FF00), + ABC_CONST(0xFFFF0000FFFF0000), ABC_CONST(0xFFFF0000FFFF0000), ABC_CONST(0xFFFF0000FFFF0000), ABC_CONST(0xFFFF0000FFFF0000), + ABC_CONST(0xFFFFFFFF00000000), ABC_CONST(0xFFFFFFFF00000000), ABC_CONST(0xFFFFFFFF00000000), ABC_CONST(0xFFFFFFFF00000000), + ABC_CONST(0x0000000000000000), ABC_CONST(0xFFFFFFFFFFFFFFFF), ABC_CONST(0x0000000000000000), ABC_CONST(0xFFFFFFFFFFFFFFFF), + ABC_CONST(0x0000000000000000), ABC_CONST(0x0000000000000000), ABC_CONST(0xFFFFFFFFFFFFFFFF), ABC_CONST(0xFFFFFFFFFFFFFFFF) +}; + typedef struct Ses_Man_t_ Ses_Man_t; struct Ses_Man_t_ { @@ -47,6 +60,11 @@ struct Ses_Man_t_ int nSpecFunc; /* number of functions to synthesize */ int nRows; /* number of rows in the specification (without 0) */ int nMaxDepth; /* maximum depth (-1 if depth is not constrained) */ + int * pArrivalTimes; /* arrival times of inputs (NULL if arrival times are ignored) */ + int nArrivalDelta; /* delta to the original arrival times (arrival times are normalized to have 0 as minimum element) */ + int nArrivalMax; /* maximum normalized arrival time */ + int nBTLimit; /* conflict limit */ + int fMakeAIG; /* create AIG instead of general network */ int fVerbose; /* be verbose */ int fVeryVerbose; /* be very verbose */ @@ -73,36 +91,73 @@ struct Ses_Man_t_ /// FUNCTION DEFINITIONS /// //////////////////////////////////////////////////////////////////////// -static inline Ses_Man_t * Ses_ManAlloc( word * pTruth, int nVars, int nFunc, int nMaxDepth, int fVerbose ) +int NormalizeArrivalTimes( int * pArrivalTimes, int nVars, int * maxNormalized ) { - int h; + int * p = pArrivalTimes, * pEnd = pArrivalTimes + nVars; + int delta = *p; + + while ( ++p < pEnd ) + if ( *p < delta ) + delta = *p; + + *maxNormalized = 0; + p = pArrivalTimes; + while ( p < pEnd ) + { + *p -= delta; + if ( *p > *maxNormalized ) + *maxNormalized = *p; + ++p; + } + + *maxNormalized += 1; + + return delta; +} + +static inline Ses_Man_t * Ses_ManAlloc( word * pTruth, int nVars, int nFunc, int nMaxDepth, int * pArrivalTimes, int fMakeAIG, int fVerbose ) +{ + int h, i; Ses_Man_t * p = ABC_CALLOC( Ses_Man_t, 1 ); p->pSat = NULL; p->bSpecInv = 0; for ( h = 0; h < nFunc; ++h ) - if ( pTruth[h] & 1 ) + if ( pTruth[h << 2] & 1 ) { - pTruth[h] = ~pTruth[h]; + for ( i = 0; i < 4; ++i ) + pTruth[(h << 2) + i] = ~pTruth[(h << 2) + i]; p->bSpecInv |= ( 1 << h ); } - p->pSpec = pTruth; - p->nSpecVars = nVars; - p->nSpecFunc = nFunc; - p->nRows = ( 1 << nVars ) - 1; - p->nMaxDepth = nMaxDepth; - p->fVerbose = fVerbose; - p->fVeryVerbose = 0; + p->pSpec = pTruth; + p->nSpecVars = nVars; + p->nSpecFunc = nFunc; + p->nRows = ( 1 << nVars ) - 1; + p->nMaxDepth = nMaxDepth; + p->pArrivalTimes = nMaxDepth >= 0 ? pArrivalTimes : NULL; + if ( p->pArrivalTimes ) + p->nArrivalDelta = NormalizeArrivalTimes( p->pArrivalTimes, nVars, &p->nArrivalMax ); + else + p->nArrivalDelta = p->nArrivalMax = 0; + p->fMakeAIG = fMakeAIG; + p->nBTLimit = nMaxDepth >= 0 ? 50000 : 0; + p->fVerbose = fVerbose; + p->fVeryVerbose = 0; return p; } static inline void Ses_ManClean( Ses_Man_t * pSes ) { - int h; + int h, i; for ( h = 0; h < pSes->nSpecFunc; ++h ) if ( ( pSes->bSpecInv >> h ) & 1 ) - pSes->pSpec[h] = ~( pSes->pSpec[h] ); + for ( i = 0; i < 4; ++i ) + pSes->pSpec[(h << 2) + i] = ~( pSes->pSpec[(h << 2) + i] ); + + if ( pSes->pArrivalTimes ) + for ( i = 0; i < pSes->nSpecVars; ++i ) + pSes->pArrivalTimes[i] += pSes->nArrivalDelta; if ( pSes->pSat ) sat_solver_delete( pSes->pSat ); @@ -160,9 +215,9 @@ static inline int Ses_ManSelectVar( Ses_Man_t * pSes, int i, int j, int k ) static inline int Ses_ManDepthVar( Ses_Man_t * pSes, int i, int j ) { assert( i < pSes->nGates ); - assert( j <= i ); + assert( j <= pSes->nArrivalMax + i ); - return pSes->nDepthOffset + ( ( i * ( i + 1 ) ) / 2 ) + j; + return pSes->nDepthOffset + i * pSes->nArrivalMax + ( ( i * ( i + 1 ) ) / 2 ) + j; } /**Function************************************************************* @@ -186,7 +241,7 @@ static void Ses_ManCreateVars( Ses_Man_t * pSes, int nGates ) pSes->nSelectVars = 0; for ( i = pSes->nSpecVars; i < pSes->nSpecVars + nGates; ++i ) pSes->nSelectVars += ( i * ( i - 1 ) ) / 2; - pSes->nDepthVars = pSes->nMaxDepth > 0 ? ( nGates * ( nGates + 1 ) ) / 2 : 0; + pSes->nDepthVars = pSes->nMaxDepth > 0 ? nGates * pSes->nArrivalMax + ( nGates * ( nGates + 1 ) ) / 2 : 0; pSes->nOutputOffset = pSes->nSimVars; pSes->nGateOffset = pSes->nSimVars + pSes->nOutputVars; @@ -213,7 +268,7 @@ static inline void Ses_ManCreateMainClause( Ses_Man_t * pSes, int t, int i, int if ( j < pSes->nSpecVars ) { - if ( ( ( s_Truths6[j] >> ( t + 1 ) ) & 1 ) != b ) /* 1 in clause, we can omit the clause */ + if ( Abc_TtGetBit( s_Truths8 + ( j << 2 ), t + 1 ) != b ) /* 1 in clause, we can omit the clause */ return; } else @@ -221,7 +276,7 @@ static inline void Ses_ManCreateMainClause( Ses_Man_t * pSes, int t, int i, int if ( k < pSes->nSpecVars ) { - if ( ( ( s_Truths6[k] >> ( t + 1 ) ) & 1 ) != c ) /* 1 in clause, we can omit the clause */ + if ( Abc_TtGetBit( s_Truths8 + ( k << 2 ), t + 1 ) != c ) /* 1 in clause, we can omit the clause */ return; } else @@ -238,7 +293,7 @@ static void Ses_ManCreateClauses( Ses_Man_t * pSes ) { extern int Extra_TruthVarsSymm( unsigned * pTruth, int nVars, int iVar0, int iVar1 ); - int h, i, j, k, t, ii, jj, kk, p, q; + int h, i, j, k, t, ii, jj, kk, p, q, d; int pLits[3]; Vec_Int_t * vLits; @@ -262,7 +317,7 @@ static void Ses_ManCreateClauses( Ses_Man_t * pSes ) for ( h = 0; h < pSes->nSpecFunc; ++h ) { pLits[0] = Abc_Var2Lit( Ses_ManOutputVar( pSes, h, i ), 1 ); - pLits[1] = Abc_Var2Lit( Ses_ManSimVar( pSes, i, t ), 1 - (int)( ( pSes->pSpec[h] >> ( t + 1 ) ) & 1 ) ); + pLits[1] = Abc_Var2Lit( Ses_ManSimVar( pSes, i, t ), 1 - Abc_TtGetBit( &pSes->pSpec[h << 2], t + 1 ) ); assert( sat_solver_addclause( pSes->pSat, pLits, pLits + 2 ) ); } } @@ -288,6 +343,29 @@ static void Ses_ManCreateClauses( Ses_Man_t * pSes ) Vec_IntFree( vLits ); } + /* only AIG */ + if ( pSes->fMakeAIG ) + { + for ( i = 0; i < pSes->nGates; ++i ) + { + /* not 2 ones */ + pLits[0] = Abc_Var2Lit( Ses_ManGateVar( pSes, i, 0, 1 ), 1 ); + pLits[1] = Abc_Var2Lit( Ses_ManGateVar( pSes, i, 1, 0 ), 1 ); + pLits[2] = Abc_Var2Lit( Ses_ManGateVar( pSes, i, 1, 1 ), 0 ); + assert( sat_solver_addclause( pSes->pSat, pLits, pLits + 3 ) ); + + pLits[0] = Abc_Var2Lit( Ses_ManGateVar( pSes, i, 0, 1 ), 1 ); + pLits[1] = Abc_Var2Lit( Ses_ManGateVar( pSes, i, 1, 0 ), 0 ); + pLits[2] = Abc_Var2Lit( Ses_ManGateVar( pSes, i, 1, 1 ), 1 ); + assert( sat_solver_addclause( pSes->pSat, pLits, pLits + 3 ) ); + + pLits[0] = Abc_Var2Lit( Ses_ManGateVar( pSes, i, 0, 1 ), 0 ); + pLits[1] = Abc_Var2Lit( Ses_ManGateVar( pSes, i, 1, 0 ), 1 ); + pLits[2] = Abc_Var2Lit( Ses_ManGateVar( pSes, i, 1, 1 ), 1 ); + assert( sat_solver_addclause( pSes->pSat, pLits, pLits + 3 ) ); + } + } + /* EXTRA clauses: use gate i at least once */ for ( i = 0; i < pSes->nGates; ++i ) { @@ -331,7 +409,7 @@ static void Ses_ManCreateClauses( Ses_Man_t * pSes ) if ( pSes->nSpecFunc == 1 ) /* only check if there is one output function */ for ( q = 1; q < pSes->nSpecVars; ++q ) for ( p = 0; p < q; ++p ) - if ( Extra_TruthVarsSymm( (unsigned*)pSes->pSpec, pSes->nSpecVars, p, q ) ) + if ( Extra_TruthVarsSymm( (unsigned*)( &pSes->pSpec[h << 2] ), pSes->nSpecVars, p, q ) ) { if ( pSes->fVeryVerbose ) printf( "variables %d and %d are symmetric\n", p, q ); @@ -357,11 +435,12 @@ static void Ses_ManCreateClauses( Ses_Man_t * pSes ) { for ( i = 0; i < pSes->nGates; ++i ) { + /* propagate depths from children */ for ( k = 1; k < i; ++k ) for ( j = 0; j < k; ++j ) { pLits[0] = Abc_Var2Lit( Ses_ManSelectVar( pSes, i, pSes->nSpecVars + j, pSes->nSpecVars + k ), 1 ); - for ( jj = 0; jj <= j; ++jj ) + for ( jj = 0; jj <= pSes->nArrivalMax + j; ++jj ) { pLits[1] = Abc_Var2Lit( Ses_ManDepthVar( pSes, j, jj ), 1 ); pLits[2] = Abc_Var2Lit( Ses_ManDepthVar( pSes, i, jj + 1 ), 0 ); @@ -373,7 +452,7 @@ static void Ses_ManCreateClauses( Ses_Man_t * pSes ) for ( j = 0; j < pSes->nSpecVars + k; ++j ) { pLits[0] = Abc_Var2Lit( Ses_ManSelectVar( pSes, i, j, pSes->nSpecVars + k ), 1 ); - for ( kk = 0; kk <= k; ++kk ) + for ( kk = 0; kk <= pSes->nArrivalMax + k; ++kk ) { pLits[1] = Abc_Var2Lit( Ses_ManDepthVar( pSes, k, kk ), 1 ); pLits[2] = Abc_Var2Lit( Ses_ManDepthVar( pSes, i, kk + 1 ), 0 ); @@ -381,17 +460,38 @@ static void Ses_ManCreateClauses( Ses_Man_t * pSes ) } } - pLits[0] = Abc_Var2Lit( Ses_ManDepthVar( pSes, i, 0 ), 0 ); - assert( sat_solver_addclause( pSes->pSat, pLits, pLits + 1 ) ); + /* propagate depths from arrival times at PIs */ + if ( pSes->pArrivalTimes ) + { + for ( k = 1; k < pSes->nSpecVars + i; ++k ) + for ( j = 0; j < ( ( k < pSes->nSpecVars ) ? k : pSes->nSpecVars ); ++j ) + { + d = pSes->pArrivalTimes[j]; + if ( k < pSes->nSpecVars && pSes->pArrivalTimes[k] > d ) + d = pSes->pArrivalTimes[k]; + + pLits[0] = Abc_Var2Lit( Ses_ManSelectVar( pSes, i, j, k ), 1 ); + pLits[1] = Abc_Var2Lit( Ses_ManDepthVar( pSes, i, d + 1 ), 0 ); + assert( sat_solver_addclause( pSes->pSat, pLits, pLits + 2 ) ); + } + } + else + { + /* arrival times are 0 */ + pLits[0] = Abc_Var2Lit( Ses_ManDepthVar( pSes, i, 0 ), 0 ); + assert( sat_solver_addclause( pSes->pSat, pLits, pLits + 1 ) ); + } - for ( j = 1; j <= i; ++j ) + /* reverse order encoding of depth variables */ + for ( j = 1; j <= pSes->nArrivalMax + i; ++j ) { pLits[0] = Abc_Var2Lit( Ses_ManDepthVar( pSes, i, j ), 1 ); pLits[1] = Abc_Var2Lit( Ses_ManDepthVar( pSes, i, j - 1 ), 0 ); assert( sat_solver_addclause( pSes->pSat, pLits, pLits + 2 ) ); } - if ( pSes->nMaxDepth < i ) + /* constrain maximum depth */ + if ( pSes->nMaxDepth < pSes->nArrivalMax + i ) for ( h = 0; h < pSes->nSpecFunc; ++h ) { pLits[0] = Abc_Var2Lit( Ses_ManOutputVar( pSes, h, i ), 1 ); @@ -412,13 +512,13 @@ static inline int Ses_ManSolve( Ses_Man_t * pSes ) int status; abctime timeStart, timeDelta; - // if ( pSes->fVerbose ) - // { - // printf( "solve SAT instance with %d clauses and %d variables\n", sat_solver_nclauses( pSes->pSat ), sat_solver_nvars( pSes->pSat ) ); - // } + if ( pSes->fVeryVerbose ) + { + printf( "solve SAT instance with %d clauses and %d variables\n", sat_solver_nclauses( pSes->pSat ), sat_solver_nvars( pSes->pSat ) ); + } timeStart = Abc_Clock(); - status = sat_solver_solve( pSes->pSat, NULL, NULL, 0, 0, 0, 0 ); + status = sat_solver_solve( pSes->pSat, NULL, NULL, pSes->nBTLimit, 0, 0, 0 ); timeDelta = Abc_Clock() - timeStart; pSes->timeSat += timeDelta; @@ -437,9 +537,9 @@ static inline int Ses_ManSolve( Ses_Man_t * pSes ) { if ( pSes->fVerbose ) { - printf( "undefined\n" ); + printf( "resource limit reached\n" ); } - return 0; + return 2; } } @@ -448,7 +548,7 @@ static inline int Ses_ManSolve( Ses_Man_t * pSes ) Synopsis [Extract solution.] ***********************************************************************/ -static Abc_Ntk_t * Ses_ManExtractSolution( Ses_Man_t * pSes ) +static Abc_Ntk_t * Ses_ManExtractNtk( Ses_Man_t * pSes ) { int h, i, j, k; Abc_Ntk_t * pNtk; @@ -507,7 +607,7 @@ static Abc_Ntk_t * Ses_ManExtractSolution( Ses_Man_t * pSes ) if ( pSes->nMaxDepth > 0 ) { printf( " and depth vector " ); - for ( j = 0; j <= i; ++j ) + for ( j = 0; j <= pSes->nArrivalMax + i; ++j ) printf( "%d", sat_solver_var_value( pSes->pSat, Ses_ManDepthVar( pSes, i, j ) ) ); } printf( "\n" ); @@ -551,6 +651,88 @@ static Abc_Ntk_t * Ses_ManExtractSolution( Ses_Man_t * pSes ) return pNtk; } +static Gia_Man_t * Ses_ManExtractGia( Ses_Man_t * pSes ) +{ + int h, i, j, k; + Gia_Man_t * pGia; + Vec_Int_t * pGates; + Vec_Ptr_t * vNames; + int nObj, nChild1, nChild2, fChild1Comp, fChild2Comp; + + pGia = Gia_ManStart( pSes->nSpecVars + pSes->nGates + pSes->nSpecFunc + 1 ); + pGia->nConstrs = 0; + pGia->pName = Extra_UtilStrsav( "exact" ); + + pGates = Vec_IntAlloc( pSes->nSpecVars + pSes->nGates ); + vNames = Abc_NodeGetFakeNames( pSes->nSpecVars + pSes->nSpecFunc ); + + /* primary inputs */ + pGia->vNamesIn = Vec_PtrStart( pSes->nSpecVars ); + for ( i = 0; i < pSes->nSpecVars; ++i ) + { + nObj = Gia_ManAppendCi( pGia ); + Vec_IntPush( pGates, nObj ); + Vec_PtrSetEntry( pGia->vNamesIn, i, Extra_UtilStrsav( Vec_PtrEntry( vNames, i ) ) ); + } + + /* gates */ + for ( i = 0; i < pSes->nGates; ++i ) + { + for ( k = 0; k < pSes->nSpecVars + i; ++k ) + for ( j = 0; j < k; ++j ) + if ( sat_solver_var_value( pSes->pSat, Ses_ManSelectVar( pSes, i, j, k ) ) ) + { + nChild1 = Vec_IntEntry( pGates, j ); + nChild2 = Vec_IntEntry( pGates, k ); + fChild1Comp = fChild2Comp = 0; + + if ( sat_solver_var_value( pSes->pSat, Ses_ManGateVar( pSes, i, 0, 1 ) ) ) + { + nChild1 = Abc_LitNot( nChild1 ); + fChild1Comp = 1; + } + if ( sat_solver_var_value( pSes->pSat, Ses_ManGateVar( pSes, i, 1, 0 ) ) ) + { + nChild2 = Abc_LitNot( nChild2 ); + fChild2Comp = 1; + } + nObj = Gia_ManAppendAnd( pGia, nChild1, nChild2 ); + if ( fChild1Comp && fChild2Comp ) + { + assert( sat_solver_var_value( pSes->pSat, Ses_ManGateVar( pSes, i, 1, 1 ) ) ); + nObj = Abc_LitNot( nObj ); + } + + Vec_IntPush( pGates, nObj ); + + break; + } + } + + /* outputs */ + pGia->vNamesOut = Vec_PtrStart( pSes->nSpecFunc ); + for ( h = 0; h < pSes->nSpecFunc; ++h ) + { + for ( i = 0; i < pSes->nGates; ++i ) + { + if ( sat_solver_var_value( pSes->pSat, Ses_ManOutputVar( pSes, h, i ) ) ) + { + nObj = Vec_IntEntry( pGates, pSes->nSpecVars + i ); + /* if output has been inverted, we need to add an inverter */ + if ( ( pSes->bSpecInv >> h ) & 1 ) + nObj = Abc_LitNot( nObj ); + Gia_ManAppendCo( pGia, nObj ); + Vec_PtrSetEntry( pGia->vNamesOut, h, Extra_UtilStrsav( Vec_PtrEntry( vNames, pSes->nSpecVars + h ) ) ); + } + } + } + Abc_NodeFreeNames( vNames ); + + Vec_IntFree( pGates ); + + return pGia; +} + /**Function************************************************************* Synopsis [Debug.] @@ -565,6 +747,19 @@ static void Ses_ManPrintRuntime( Ses_Man_t * pSes ) ABC_PRTP( "ALL ", pSes->timeTotal, pSes->timeTotal ); } +static inline void Ses_ManPrintFuncs( Ses_Man_t * pSes ) +{ + int h; + + printf( "find optimum circuit for %d %d-variable functions:\n", pSes->nSpecFunc, pSes->nSpecVars ); + for ( h = 0; h < pSes->nSpecFunc; ++h ) + { + printf( " func %d: ", h + 1 ); + Abc_TtPrintHexRev( stdout, &pSes->pSpec[h >> 2], pSes->nSpecVars ); + printf( "\n" ); + } +} + static inline void Ses_ManPrintVars( Ses_Man_t * pSes ) { int h, i, j, k, p, q, t; @@ -602,63 +797,92 @@ static inline void Ses_ManPrintVars( Ses_Man_t * pSes ) Synopsis [Synthesis algorithm.] ***********************************************************************/ -static Abc_Ntk_t * Ses_ManFindMinimumSize( Ses_Man_t * pSes ) +static int Ses_ManFindMinimumSize( Ses_Man_t * pSes ) { int nGates = 0; - abctime timeStart; - Abc_Ntk_t * pNtk; - - timeStart = Abc_Clock(); while ( true ) { ++nGates; + + /* give up if number of gates is impossible for given depth */ + if ( pSes->nMaxDepth != -1 && nGates >= ( 1 << pSes->nMaxDepth ) ) + return 0; + Ses_ManCreateVars( pSes, nGates ); Ses_ManCreateClauses( pSes ); - if ( Ses_ManSolve( pSes ) ) + switch ( Ses_ManSolve( pSes ) ) { - pNtk = Ses_ManExtractSolution( pSes ); - pSes->timeTotal = Abc_Clock() - timeStart; - return pNtk; + case 1: return 1; /* SAT */ + case 2: return 0; /* resource limit */ } } + + return 0; } /**Function************************************************************* Synopsis [Find minimum size networks with a SAT solver.] - Description [] + Description [If nMaxDepth is -1, then depth constraints are ignored. + If nMaxDepth is not -1, one can set pArrivalTimes which should have the length of nVars. + One can ignore pArrivalTimes by setting it to NULL.] SideEffects [] SeeAlso [] ***********************************************************************/ -Abc_Ntk_t * Abc_NtkFindExact( word * pTruth, int nVars, int nFunc, int nMaxDepth, int fVerbose ) +Abc_Ntk_t * Abc_NtkFindExact( word * pTruth, int nVars, int nFunc, int nMaxDepth, int * pArrivalTimes, int fVerbose ) { - int i, j; Ses_Man_t * pSes; - Abc_Ntk_t * pNtk; + Abc_Ntk_t * pNtk = NULL; + abctime timeStart; /* some checks */ - assert( nVars >= 2 && nVars <= 6 ); + assert( nVars >= 2 && nVars <= 8 ); + + timeStart = Abc_Clock(); + pSes = Ses_ManAlloc( pTruth, nVars, nFunc, nMaxDepth, pArrivalTimes, 0, fVerbose ); if ( fVerbose ) - { - printf( "find optimum circuit for %d %d-variable functions:\n", nFunc, nVars ); - for ( i = 0; i < nFunc; ++i ) - { - printf( " func %d: ", i + 1 ); - for ( j = 0; j < ( 1 << nVars ); ++j ) - printf( "%lu", ( pTruth[i] >> j ) & 1 ); - printf( "\n" ); - } - } + Ses_ManPrintFuncs( pSes ); + + if ( Ses_ManFindMinimumSize( pSes ) ) + pNtk = Ses_ManExtractNtk( pSes ); + + pSes->timeTotal = Abc_Clock() - timeStart; + + if ( fVerbose ) + Ses_ManPrintRuntime( pSes ); + + /* cleanup */ + Ses_ManClean( pSes ); + + return pNtk; +} + +Gia_Man_t * Gia_ManFindExact( word * pTruth, int nVars, int nFunc, int nMaxDepth, int * pArrivalTimes, int fVerbose ) +{ + Ses_Man_t * pSes; + Gia_Man_t * pGia = NULL; + abctime timeStart; + + /* some checks */ + assert( nVars >= 2 && nVars <= 8 ); + + timeStart = Abc_Clock(); - pSes = Ses_ManAlloc( pTruth, nVars, nFunc, nMaxDepth, fVerbose ); - pNtk = Ses_ManFindMinimumSize( pSes ); + pSes = Ses_ManAlloc( pTruth, nVars, nFunc, nMaxDepth, pArrivalTimes, 1, fVerbose ); + if ( fVerbose ) + Ses_ManPrintFuncs( pSes ); + + if ( Ses_ManFindMinimumSize( pSes ) ) + pGia = Ses_ManExtractGia( pSes ); + + pSes->timeTotal = Abc_Clock() - timeStart; if ( fVerbose ) Ses_ManPrintRuntime( pSes ); @@ -666,9 +890,118 @@ Abc_Ntk_t * Abc_NtkFindExact( word * pTruth, int nVars, int nFunc, int nMaxDepth /* cleanup */ Ses_ManClean( pSes ); + return pGia; +} + +/**Function************************************************************* + + Synopsis [Some test cases.] + +***********************************************************************/ + +Abc_Ntk_t * Abc_NtkFromTruthTable( word * pTruth, int nVars ) +{ + Abc_Ntk_t * pNtk; + Mem_Flex_t * pMan; + char * pSopCover; + + pMan = Mem_FlexStart(); + pSopCover = Abc_SopCreateFromTruth( pMan, nVars, (unsigned*)pTruth ); + pNtk = Abc_NtkCreateWithNode( pSopCover ); + Abc_NtkShortNames( pNtk ); + Mem_FlexStop( pMan, 0 ); + return pNtk; } +void Abc_ExactTestSingleOutput( int fVerbose ) +{ + extern void Abc_NtkCecSat( Abc_Ntk_t * pNtk1, Abc_Ntk_t * pNtk2, int nConfLimit, int nInsLimit ); + + word pTruth[4] = {0xcafe, 0, 0, 0}; + Abc_Ntk_t * pNtk, * pNtk2, * pNtk3, * pNtk4; + int pArrivalTimes[4] = {6, 2, 8, 5}; + + pNtk = Abc_NtkFromTruthTable( pTruth, 4 ); + + pNtk2 = Abc_NtkFindExact( pTruth, 4, 1, -1, NULL, fVerbose ); + Abc_NtkShortNames( pNtk2 ); + Abc_NtkCecSat( pNtk, pNtk2, 10000, 0 ); + assert( pNtk2 ); + assert( Abc_NtkNodeNum( pNtk2 ) == 6 ); + Abc_NtkDelete( pNtk2 ); + + pNtk3 = Abc_NtkFindExact( pTruth, 4, 1, 3, NULL, fVerbose ); + Abc_NtkShortNames( pNtk3 ); + Abc_NtkCecSat( pNtk, pNtk3, 10000, 0 ); + assert( pNtk3 ); + assert( Abc_NtkLevel( pNtk3 ) <= 3 ); + Abc_NtkDelete( pNtk3 ); + + pNtk4 = Abc_NtkFindExact( pTruth, 4, 1, 9, pArrivalTimes, fVerbose ); + Abc_NtkShortNames( pNtk4 ); + Abc_NtkCecSat( pNtk, pNtk4, 10000, 0 ); + assert( pNtk4 ); + assert( Abc_NtkLevel( pNtk4 ) <= 9 ); + Abc_NtkDelete( pNtk4 ); + + assert( !Abc_NtkFindExact( pTruth, 4, 1, 2, NULL, fVerbose ) ); + + assert( !Abc_NtkFindExact( pTruth, 4, 1, 8, pArrivalTimes, fVerbose ) ); + + Abc_NtkDelete( pNtk ); +} + +void Abc_ExactTestSingleOutputAIG( int fVerbose ) +{ + word pTruth[4] = {0xcafe, 0, 0, 0}; + Abc_Ntk_t * pNtk; + Gia_Man_t * pGia, * pGia2, * pGia3, * pGia4, * pMiter; + Cec_ParCec_t ParsCec, * pPars = &ParsCec; + int pArrivalTimes[4] = {6, 2, 8, 5}; + + Cec_ManCecSetDefaultParams( pPars ); + + pNtk = Abc_NtkFromTruthTable( pTruth, 4 ); + Abc_NtkToAig( pNtk ); + pGia = Abc_NtkAigToGia( pNtk, 1 ); + + pGia2 = Gia_ManFindExact( pTruth, 4, 1, -1, NULL, fVerbose ); + pMiter = Gia_ManMiter( pGia, pGia2, 0, 1, 0, 0, 1 ); + assert( pMiter ); + Cec_ManVerify( pMiter, pPars ); + Gia_ManStop( pMiter ); + + pGia3 = Gia_ManFindExact( pTruth, 4, 1, 3, NULL, fVerbose ); + pMiter = Gia_ManMiter( pGia, pGia3, 0, 1, 0, 0, 1 ); + assert( pMiter ); + Cec_ManVerify( pMiter, pPars ); + Gia_ManStop( pMiter ); + + pGia4 = Gia_ManFindExact( pTruth, 4, 1, 9, pArrivalTimes, fVerbose ); + pMiter = Gia_ManMiter( pGia, pGia4, 0, 1, 0, 0, 1 ); + assert( pMiter ); + Cec_ManVerify( pMiter, pPars ); + Gia_ManStop( pMiter ); + + assert( !Gia_ManFindExact( pTruth, 4, 1, 2, NULL, fVerbose ) ); + + assert( !Gia_ManFindExact( pTruth, 4, 1, 8, pArrivalTimes, fVerbose ) ); + + Gia_ManStop( pGia ); + Gia_ManStop( pGia2 ); + Gia_ManStop( pGia3 ); + Gia_ManStop( pGia4 ); +} + +void Abc_ExactTest( int fVerbose ) +{ + Abc_ExactTestSingleOutput( fVerbose ); + Abc_ExactTestSingleOutputAIG( fVerbose ); + + printf( "\n" ); +} + //////////////////////////////////////////////////////////////////////// /// END OF FILE /// -- cgit v1.2.3