diff options
author | Alan Mishchenko <alanmi@berkeley.edu> | 2016-07-16 07:51:58 -0700 |
---|---|---|
committer | Alan Mishchenko <alanmi@berkeley.edu> | 2016-07-16 07:51:58 -0700 |
commit | 32d1516c64eca2805f951b1dc6f3d6ce93c29f4e (patch) | |
tree | 6c3aa971d91a091cce0f6ca02075b3c9e6931576 | |
parent | abdf39711f8c175840da90fd8531183c61691f68 (diff) | |
download | abc-32d1516c64eca2805f951b1dc6f3d6ce93c29f4e.tar.gz abc-32d1516c64eca2805f951b1dc6f3d6ce93c29f4e.tar.bz2 abc-32d1516c64eca2805f951b1dc6f3d6ce93c29f4e.zip |
Adding command 'exact' developed by Mathias Soeken to implement Knuth's exact synthesis algorithm.
-rw-r--r-- | src/base/abc/abc.h | 2 | ||||
-rw-r--r-- | src/base/abci/abc.c | 57 | ||||
-rw-r--r-- | src/base/abci/abcExact.c | 589 | ||||
-rw-r--r-- | src/base/abci/module.make | 1 |
4 files changed, 649 insertions, 0 deletions
diff --git a/src/base/abc/abc.h b/src/base/abc/abc.h index 78afb412..2d63af2d 100644 --- a/src/base/abc/abc.h +++ b/src/base/abc/abc.h @@ -642,6 +642,8 @@ extern ABC_DLL int Abc_NtkLevelReverse( Abc_Ntk_t * pNtk ); extern ABC_DLL int Abc_NtkIsAcyclic( Abc_Ntk_t * pNtk ); extern ABC_DLL int Abc_NtkIsAcyclicWithBoxes( Abc_Ntk_t * pNtk ); extern ABC_DLL Vec_Ptr_t * Abc_AigGetLevelizedOrder( Abc_Ntk_t * pNtk, int fCollectCis ); +/*=== abcExact.c ==========================================================*/ +extern ABC_DLL Abc_Ntk_t * Abc_NtkFindExact( word * pTruth, int nVars, int nFunc, int fVerbose ); /*=== abcFanio.c ==========================================================*/ extern ABC_DLL void Abc_ObjAddFanin( Abc_Obj_t * pObj, Abc_Obj_t * pFanin ); extern ABC_DLL void Abc_ObjDeleteFanin( Abc_Obj_t * pObj, Abc_Obj_t * pFanin ); diff --git a/src/base/abci/abc.c b/src/base/abci/abc.c index e883c8fc..bc411998 100644 --- a/src/base/abci/abc.c +++ b/src/base/abci/abc.c @@ -135,6 +135,7 @@ static int Abc_CommandCascade ( Abc_Frame_t * pAbc, int argc, cha static int Abc_CommandExtract ( Abc_Frame_t * pAbc, int argc, char ** argv ); static int Abc_CommandVarMin ( Abc_Frame_t * pAbc, int argc, char ** argv ); static int Abc_CommandDetect ( Abc_Frame_t * pAbc, int argc, char ** argv ); +static int Abc_CommandExact ( 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 ); @@ -773,6 +774,7 @@ void Abc_Init( Abc_Frame_t * pAbc ) Cmd_CommandAdd( pAbc, "Synthesis", "extract", Abc_CommandExtract, 1 ); Cmd_CommandAdd( pAbc, "Synthesis", "varmin", Abc_CommandVarMin, 0 ); Cmd_CommandAdd( pAbc, "Synthesis", "detect", Abc_CommandDetect, 0 ); + Cmd_CommandAdd( pAbc, "Synthesis", "exact", Abc_CommandExact, 1 ); Cmd_CommandAdd( pAbc, "Various", "logic", Abc_CommandLogic, 1 ); Cmd_CommandAdd( pAbc, "Various", "comb", Abc_CommandComb, 1 ); @@ -7274,6 +7276,61 @@ usage: SeeAlso [] ***********************************************************************/ +int Abc_CommandExact( Abc_Frame_t * pAbc, int argc, char ** argv ) +{ + int c, fVerbose = 0, nVars; + word pTruth[1]; + Abc_Ntk_t * pNtkRes; + + 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 ) + { + goto usage; + } + + nVars = Abc_TtReadHex( pTruth, argv[globalUtilOptind] ); + pNtkRes = Abc_NtkFindExact( pTruth, nVars, 1, fVerbose ); + assert( pNtkRes != NULL ); + Abc_FrameReplaceCurrentNetwork( pAbc, pNtkRes ); + Abc_FrameClearVerifStatus( pAbc ); + return 0; + +usage: + Abc_Print( -2, "usage: exact [-vh] <truth>\n" ); + Abc_Print( -2, "\t finds optimum networks using SAT-based exact synthesis\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" ); + Abc_Print( -2, "\t The author can be contacted as mathias.soeken at epfl.ch\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/base/abci/abcExact.c b/src/base/abci/abcExact.c new file mode 100644 index 00000000..68d9ebab --- /dev/null +++ b/src/base/abci/abcExact.c @@ -0,0 +1,589 @@ +/**CFile**************************************************************** + + FileName [abcExact.c] + + SystemName [ABC: Logic synthesis and verification system.] + + PackageName [Network and node package.] + + Synopsis [Find minimum size networks with a SAT solver.] + + Author [Mathias Soeken] + + Affiliation [EPFL] + + Date [Ver. 1.0. Started - July 15, 2016.] + + Revision [$Id: abcFanio.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $] + +***********************************************************************/ + +/* This implementation is based on Exercises 477 and 478 in + * Donald E. Knuth TAOCP Fascicle 6 (Satisfiability) Section 7.2.2.2 + */ + +#include "base/abc/abc.h" + +#include "misc/util/utilTruth.h" +#include "misc/vec/vecInt.h" +#include "misc/vec/vecPtr.h" +#include "sat/bsat/satSolver.h" + +ABC_NAMESPACE_IMPL_START + + +//////////////////////////////////////////////////////////////////////// +/// DECLARATIONS /// +//////////////////////////////////////////////////////////////////////// + +typedef struct Ses_Man_t_ Ses_Man_t; +struct Ses_Man_t_ +{ + sat_solver * pSat; /* SAT solver */ + + word * pSpec; /* specification */ + int bSpecInv; /* remembers whether spec was inverted for normalization */ + int nSpecVars; /* number of variables in specification */ + int nSpecFunc; /* number of functions to synthesize */ + int nRows; /* number of rows in the specification (without 0) */ + int fVerbose; /* be verbose */ + int fVeryVerbose; /* be very verbose */ + + int nGates; /* number of gates */ + + int nSimVars; /* number of simulation vars x(i, t) */ + int nOutputVars; /* number of output variables g(h, i) */ + int nGateVars; /* number of gate variables f(i, p, q) */ + int nSelectVars; /* number of select variables s(i, j, k ) */ + + int nOutputOffset; /* offset where output variables start */ + int nGateOffset; /* offset where gate variables start */ + int nSelectOffset; /* offset where select variables start */ + + abctime timeSat; /* SAT runtime */ + abctime timeSatSat; /* SAT runtime (sat instance) */ + abctime timeSatUnsat; /* SAT runtime (unsat instance) */ + abctime timeTotal; /* all runtime */ +}; + +//////////////////////////////////////////////////////////////////////// +/// FUNCTION DEFINITIONS /// +//////////////////////////////////////////////////////////////////////// + +static inline Ses_Man_t * Ses_ManAlloc( word * pTruth, int nVars, int nFunc, int fVerbose ) +{ + int h; + + 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 ) + { + pTruth[h] = ~pTruth[h]; + p->bSpecInv |= ( 1 << h ); + } + p->pSpec = pTruth; + p->nSpecVars = nVars; + p->nSpecFunc = nFunc; + p->nRows = ( 1 << nVars ) - 1; + p->fVerbose = fVerbose; + p->fVeryVerbose = 0; + + return p; +} + +static inline void Ses_ManClean( Ses_Man_t * pSes ) +{ + int h; + for ( h = 0; h < pSes->nSpecFunc; ++h ) + if ( ( pSes->bSpecInv >> h ) & 1 ) + pSes->pSpec[h] = ~( pSes->pSpec[h] ); + + if ( pSes->pSat ) + sat_solver_delete( pSes->pSat ); + + ABC_FREE( pSes ); +} + +/**Function************************************************************* + + Synopsis [Access variables based on indexes.] + +***********************************************************************/ +static inline int Ses_ManSimVar( Ses_Man_t * pSes, int i, int t ) +{ + assert( i < pSes->nGates ); + assert( t < pSes->nRows ); + + return pSes->nRows * i + t; +} + +static inline int Ses_ManOutputVar( Ses_Man_t * pSes, int h, int i ) +{ + assert( h < pSes->nSpecFunc ); + assert( i < pSes->nGates ); + + return pSes->nOutputOffset + pSes->nGates * h + i; +} + +static inline int Ses_ManGateVar( Ses_Man_t * pSes, int i, int p, int q ) +{ + assert( i < pSes->nGates ); + assert( p < 2 ); + assert( q < 2 ); + assert( p > 0 || q > 0 ); + + return pSes->nGateOffset + i * 3 + ( p << 1 ) + q - 1; +} + +static inline int Ses_ManSelectVar( Ses_Man_t * pSes, int i, int j, int k ) +{ + int a; + int offset; + + assert( i < pSes->nGates ); + assert( k < pSes->nSpecVars + i ); + assert( j < k ); + + offset = pSes->nSelectOffset; + for ( a = pSes->nSpecVars; a < pSes->nSpecVars + i; ++a ) + offset += a * ( a - 1 ) / 2; + + return offset + ( -j * ( 1 + j - 2 * ( pSes->nSpecVars + i ) ) ) / 2 + ( k - j - 1 ); +} + +/**Function************************************************************* + + Synopsis [Setup variables to find network with nGates gates.] + +***********************************************************************/ +static void Ses_ManCreateVars( Ses_Man_t * pSes, int nGates ) +{ + int i; + + if ( pSes->fVerbose ) + { + printf( "create variables for network with %d functions over %d variables and %d gates\n", pSes->nSpecFunc, pSes->nSpecVars, nGates ); + } + + pSes->nGates = nGates; + pSes->nSimVars = nGates * pSes->nRows; + pSes->nOutputVars = pSes->nSpecFunc * nGates; + pSes->nGateVars = nGates * 3; + pSes->nSelectVars = 0; + for ( i = pSes->nSpecVars; i < pSes->nSpecVars + nGates; ++i ) + pSes->nSelectVars += ( i * ( i - 1 ) ) / 2; + + pSes->nOutputOffset = pSes->nSimVars; + pSes->nGateOffset = pSes->nSimVars + pSes->nOutputVars; + pSes->nSelectOffset = pSes->nSimVars + pSes->nOutputVars + pSes->nGateVars; + + if ( pSes->pSat ) + sat_solver_delete( pSes->pSat ); + pSes->pSat = sat_solver_new(); + sat_solver_setnvars( pSes->pSat, pSes->nSimVars + pSes->nOutputVars + pSes->nGateVars + pSes->nSelectVars ); +} + +/**Function************************************************************* + + Synopsis [Create clauses.] + +***********************************************************************/ +static inline void Ses_ManCreateMainClause( Ses_Man_t * pSes, int t, int i, int j, int k, int a, int b, int c ) +{ + int pLits[5], ctr = 0, value; + + pLits[ctr++] = Abc_Var2Lit( Ses_ManSelectVar( pSes, i, j, k ), 1 ); + pLits[ctr++] = Abc_Var2Lit( Ses_ManSimVar( pSes, i, t ), a ); + + if ( j < pSes->nSpecVars ) + { + if ( ( ( s_Truths6[j] >> ( t + 1 ) ) & 1 ) != b ) /* 1 in clause, we can omit the clause */ + return; + } + else + pLits[ctr++] = Abc_Var2Lit( Ses_ManSimVar( pSes, j - pSes->nSpecVars, t ), b ); + + if ( k < pSes->nSpecVars ) + { + if ( ( ( s_Truths6[k] >> ( t + 1 ) ) & 1 ) != c ) /* 1 in clause, we can omit the clause */ + return; + } + else + pLits[ctr++] = Abc_Var2Lit( Ses_ManSimVar( pSes, k - pSes->nSpecVars, t ), c ); + + if ( b > 0 || c > 0 ) + pLits[ctr++] = Abc_Var2Lit( Ses_ManGateVar( pSes, i, b, c ), 1 - a ); + + value = sat_solver_addclause( pSes->pSat, pLits, pLits + ctr ); + assert( value ); +} + +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 pLits[2]; + Vec_Int_t * vLits; + + for ( t = 0; t < pSes->nRows; ++t ) + for ( i = 0; i < pSes->nGates; ++i ) + { + /* main clauses */ + for ( j = 0; j < pSes->nSpecVars + i; ++j ) + for ( k = j + 1; k < pSes->nSpecVars + i; ++k ) + { + Ses_ManCreateMainClause( pSes, t, i, j, k, 0, 0, 1 ); + Ses_ManCreateMainClause( pSes, t, i, j, k, 0, 1, 0 ); + Ses_ManCreateMainClause( pSes, t, i, j, k, 0, 1, 1 ); + Ses_ManCreateMainClause( pSes, t, i, j, k, 1, 0, 0 ); + Ses_ManCreateMainClause( pSes, t, i, j, k, 1, 0, 1 ); + Ses_ManCreateMainClause( pSes, t, i, j, k, 1, 1, 0 ); + Ses_ManCreateMainClause( pSes, t, i, j, k, 1, 1, 1 ); + } + + /* output clauses */ + 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 ) ); + assert( sat_solver_addclause( pSes->pSat, pLits, pLits + 2 ) ); + } + } + + /* some output is selected */ + for ( h = 0; h < pSes->nSpecFunc; ++h ) + { + vLits = Vec_IntAlloc( pSes->nGates ); + for ( i = 0; i < pSes->nGates; ++i ) + Vec_IntPush( vLits, Abc_Var2Lit( Ses_ManOutputVar( pSes, h, i ), 0 ) ); + assert( sat_solver_addclause( pSes->pSat, Vec_IntArray( vLits ), Vec_IntLimit( vLits ) ) ); + Vec_IntFree( vLits ); + } + + /* each gate has two operands */ + for ( i = 0; i < pSes->nGates; ++i ) + { + vLits = Vec_IntAlloc( ( ( pSes->nSpecVars + i ) * ( pSes->nSpecVars + i - 1 ) ) / 2 ); + for ( j = 0; j < pSes->nSpecVars + i; ++j ) + for ( k = j + 1; k < pSes->nSpecVars + i; ++k ) + Vec_IntPush( vLits, Abc_Var2Lit( Ses_ManSelectVar( pSes, i, j, k ), 0 ) ); + assert( sat_solver_addclause( pSes->pSat, Vec_IntArray( vLits ), Vec_IntLimit( vLits ) ) ); + Vec_IntFree( vLits ); + } + + /* EXTRA clauses: use gate i at least once */ + for ( i = 0; i < pSes->nGates; ++i ) + { + vLits = Vec_IntAlloc( 0 ); + for ( h = 0; h < pSes->nSpecFunc; ++h ) + Vec_IntPush( vLits, Abc_Var2Lit( Ses_ManOutputVar( pSes, h, i ), 0 ) ); + for ( ii = i + 1; ii < pSes->nGates; ++ii ) + { + for ( j = 0; j < pSes->nSpecVars + i; ++j ) + Vec_IntPush( vLits, Abc_Var2Lit( Ses_ManSelectVar( pSes, ii, j, pSes->nSpecVars + i ), 0 ) ); + for ( j = pSes->nSpecVars + i + 1; j < pSes->nSpecVars + ii; ++j ) + Vec_IntPush( vLits, Abc_Var2Lit( Ses_ManSelectVar( pSes, ii, pSes->nSpecVars + i, j ), 0 ) ); + } + assert( sat_solver_addclause( pSes->pSat, Vec_IntArray( vLits ), Vec_IntLimit( vLits ) ) ); + Vec_IntFree( vLits ); + } + + /* EXTRA clauses: co-lexicographic order */ + for ( i = 0; i < pSes->nGates - 1; ++i ) + { + for ( k = 2; k < pSes->nSpecVars + i; ++k ) + { + for ( j = 1; j < k; ++j ) + for ( jj = 0; jj < j; ++jj ) + { + pLits[0] = Abc_Var2Lit( Ses_ManSelectVar( pSes, i, j, k ), 1 ); + pLits[1] = Abc_Var2Lit( Ses_ManSelectVar( pSes, i + 1, jj, k ), 1 ); + } + + for ( j = 0; j < k; ++j ) + for ( kk = 1; kk < k; ++kk ) + for ( jj = 0; jj < kk; ++jj ) + { + pLits[0] = Abc_Var2Lit( Ses_ManSelectVar( pSes, i, j, k ), 1 ); + pLits[1] = Abc_Var2Lit( Ses_ManSelectVar( pSes, i + 1, jj, kk ), 1 ); + } + } + } + + /* EXTRA clauses: symmetric variables */ + 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 ( pSes->fVeryVerbose ) + printf( "variables %d and %d are symmetric\n", p, q ); + for ( i = 0; i < pSes->nGates; ++i ) + for ( j = 0; j < q; ++j ) + { + if ( j == p ) continue; + + vLits = Vec_IntAlloc( 0 ); + Vec_IntPush( vLits, Abc_Var2Lit( Ses_ManSelectVar( pSes, i, j, q ), 1 ) ); + for ( ii = 0; ii < i; ++ii ) + for ( kk = 1; kk < pSes->nSpecVars + ii; ++kk ) + for ( jj = 0; jj < kk; ++jj ) + if ( jj == p || kk == p ) + Vec_IntPush( vLits, Abc_Var2Lit( Ses_ManSelectVar( pSes, ii, jj, kk ), 0 ) ); + assert( sat_solver_addclause( pSes->pSat, Vec_IntArray( vLits ), Vec_IntLimit( vLits ) ) ); + Vec_IntFree( vLits ); + } + } +} + +/**Function************************************************************* + + Synopsis [Solve.] + +***********************************************************************/ +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 ) ); + // } + + timeStart = Abc_Clock(); + status = sat_solver_solve( pSes->pSat, NULL, NULL, 0, 0, 0, 0 ); + timeDelta = Abc_Clock() - timeStart; + + pSes->timeSat += timeDelta; + + if ( status == l_True ) + { + pSes->timeSatSat += timeDelta; + return 1; + } + else if ( status == l_False ) + { + pSes->timeSatUnsat += timeDelta; + return 0; + } + else + { + if ( pSes->fVerbose ) + { + printf( "undefined\n" ); + } + return 0; + } +} + +/**Function************************************************************* + + Synopsis [Extract solution.] + +***********************************************************************/ +static Abc_Ntk_t * Ses_ManExtractSolution( Ses_Man_t * pSes ) +{ + int h, i, j, k; + Abc_Ntk_t * pNtk; + Abc_Obj_t * pObj; + Vec_Ptr_t * pGates, * vNames; + char pGateTruth[5]; + char * pSopCover; + + pNtk = Abc_NtkAlloc( ABC_NTK_LOGIC, ABC_FUNC_SOP, 1 ); + pNtk->pName = Extra_UtilStrsav( "exact" ); + pGates = Vec_PtrAlloc( pSes->nSpecVars + pSes->nGates ); + pGateTruth[3] = '0'; + pGateTruth[4] = '\0'; + vNames = Abc_NodeGetFakeNames( pSes->nSpecVars + pSes->nSpecFunc ); + + /* primary inputs */ + Vec_PtrPush( pNtk->vObjs, NULL ); + for ( i = 0; i < pSes->nSpecVars; ++i ) + { + pObj = Abc_NtkCreatePi( pNtk ); + Abc_ObjAssignName( pObj, (char*)Vec_PtrEntry( vNames, i ), NULL ); + Vec_PtrPush( pGates, pObj ); + } + + /* gates */ + for ( i = 0; i < pSes->nGates; ++i ) + { + pGateTruth[2] = '0' + sat_solver_var_value( pSes->pSat, Ses_ManGateVar( pSes, i, 0, 1 ) ); + pGateTruth[1] = '0' + sat_solver_var_value( pSes->pSat, Ses_ManGateVar( pSes, i, 1, 0 ) ); + pGateTruth[0] = '0' + sat_solver_var_value( pSes->pSat, Ses_ManGateVar( pSes, i, 1, 1 ) ); + + if ( pSes->fVeryVerbose ) + { + printf( "gate %d has truth table %s", pSes->nSpecVars + i, pGateTruth ); + } + + pSopCover = Abc_SopFromTruthBin( pGateTruth ); + pObj = Abc_NtkCreateNode( pNtk ); + pObj->pData = Abc_SopRegister( (Mem_Flex_t*)pNtk->pManFunc, pSopCover ); + Vec_PtrPush( pGates, pObj ); + ABC_FREE( pSopCover ); + + 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 ) ) ) + { + if ( pSes->fVeryVerbose ) + printf( " with children %d and %d\n", j, k ); + Abc_ObjAddFanin( pObj, (Abc_Obj_t *)Vec_PtrEntry( pGates, j ) ); + Abc_ObjAddFanin( pObj, (Abc_Obj_t *)Vec_PtrEntry( pGates, k ) ); + break; + } + } + + /* outputs */ + for ( h = 0; h < pSes->nSpecFunc; ++h ) + { + pObj = Abc_NtkCreatePo( pNtk ); + Abc_ObjAssignName( pObj, (char*)Vec_PtrEntry( vNames, pSes->nSpecVars + h ), NULL ); + for ( i = 0; i < pSes->nGates; ++i ) + { + if ( sat_solver_var_value( pSes->pSat, Ses_ManOutputVar( pSes, h, i ) ) ) + { + /* if output has been inverted, we need to add an inverter */ + if ( ( pSes->bSpecInv >> h ) & 1 ) + Abc_ObjAddFanin( pObj, Abc_NtkCreateNodeInv( pNtk, (Abc_Obj_t *)Vec_PtrEntry( pGates, pSes->nSpecVars + i ) ) ); + else + Abc_ObjAddFanin( pObj, (Abc_Obj_t *)Vec_PtrEntry( pGates, pSes->nSpecVars + i ) ); + } + } + } + Abc_NodeFreeNames( vNames ); + + Vec_PtrFree( pGates ); + + if ( !Abc_NtkCheck( pNtk ) ) + printf( "Ses_ManExtractSolution(): Network check has failed.\n" ); + + + return pNtk; +} + +/**Function************************************************************* + + Synopsis [Synthesis algorithm.] + +***********************************************************************/ +static Abc_Ntk_t * Ses_ManFindMinimumSize( Ses_Man_t * pSes ) +{ + int nGates = 0; + abctime timeStart; + Abc_Ntk_t * pNtk; + + timeStart = Abc_Clock(); + + while ( true ) + { + ++nGates; + Ses_ManCreateVars( pSes, nGates ); + Ses_ManCreateClauses( pSes ); + if ( Ses_ManSolve( pSes ) ) + { + pNtk = Ses_ManExtractSolution( pSes ); + pSes->timeTotal = Abc_Clock() - timeStart; + return pNtk; + } + } +} + +/**Function************************************************************* + + Synopsis [Debug.] + +***********************************************************************/ +static void Ses_ManPrintRuntime( Ses_Man_t * pSes ) +{ + printf( "Runtime breakdown:\n" ); + ABC_PRTP( "Sat ", pSes->timeSat, pSes->timeTotal ); + ABC_PRTP( " Sat ", pSes->timeSatSat, pSes->timeTotal ); + ABC_PRTP( " Unsat", pSes->timeSatUnsat, pSes->timeTotal ); + ABC_PRTP( "ALL ", pSes->timeTotal, pSes->timeTotal ); +} + +static inline void Ses_ManPrintVars( Ses_Man_t * pSes ) +{ + int h, i, j, k, p, q, t; + + for ( i = 0; i < pSes->nGates; ++i ) + for ( t = 0; t < pSes->nRows; ++t ) + printf( "x(%d, %d) : %d\n", i, t, Ses_ManSimVar( pSes, i, t ) ); + + for ( h = 0; h < pSes->nSpecFunc; ++h ) + for ( i = 0; i < pSes->nGates; ++i ) + printf( "h(%d, %d) : %d\n", h, i, Ses_ManOutputVar( pSes, h, i ) ); + + for ( i = 0; i < pSes->nGates; ++i ) + for ( p = 0; p <= 1; ++p ) + for ( q = 0; q <= 1; ++ q) + { + if ( p == 0 && q == 0 ) { continue; } + printf( "f(%d, %d, %d) : %d\n", i, p, q, Ses_ManGateVar( pSes, i, p, q ) ); + } + + for ( i = 0; i < pSes->nGates; ++i ) + for ( j = 0; j < pSes->nSpecVars + i; ++j ) + for ( k = j + 1; k < pSes->nSpecVars + i; ++k ) + printf( "s(%d, %d, %d) : %d\n", i, j, k, Ses_ManSelectVar( pSes, i, j, k ) ); + +} + +/**Function************************************************************* + + Synopsis [Find minimum size networks with a SAT solver.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Abc_Ntk_t * Abc_NtkFindExact( word * pTruth, int nVars, int nFunc, int fVerbose ) +{ + int i, j; + Ses_Man_t * pSes; + Abc_Ntk_t * pNtk; + + /* some checks */ + assert( nVars >= 2 && nVars <= 6 ); + + 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" ); + } + } + + pSes = Ses_ManAlloc( pTruth, nVars, nFunc, fVerbose ); + pNtk = Ses_ManFindMinimumSize( pSes ); + + if ( fVerbose ) + Ses_ManPrintRuntime( pSes ); + + /* cleanup */ + Ses_ManClean( pSes ); + + return pNtk; +} + + +//////////////////////////////////////////////////////////////////////// +/// END OF FILE /// +//////////////////////////////////////////////////////////////////////// + + +ABC_NAMESPACE_IMPL_END diff --git a/src/base/abci/module.make b/src/base/abci/module.make index a3c343ee..492fc62a 100644 --- a/src/base/abci/module.make +++ b/src/base/abci/module.make @@ -16,6 +16,7 @@ SRC += src/base/abci/abc.c \ src/base/abci/abcDress.c \ src/base/abci/abcDress2.c \ src/base/abci/abcDsd.c \ + src/base/abci/abcExact.c \ src/base/abci/abcExtract.c \ src/base/abci/abcFraig.c \ src/base/abci/abcFx.c \ |