Skip to content

A
abc
Commit 80fdd58c by Mathias Soeken
Options

Several updates to exact synthesis.

parent 0f1624e5
Showing with 459 additions and 76 deletions
src/base/abc/abc.h
......@@ -643,7 +643,7 @@ 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 nMaxDepth, int fVerbose );
extern ABC_DLL Abc_Ntk_t * Abc_NtkFindExact( word * pTruth, int nVars, int nFunc, int nMaxDepth, int * pArrivalTimes, 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 );
......
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] <truth>\n" );
Abc_Print( -2, "\t finds optimum networks using SAT-based exact synthesis for hex truth table <truth>\n" );
Abc_Print( -2, "\t-D <num> : constrain maximum depth\n" );
Abc_Print( -2, "\t-v : toggle verbose printout [default = %s]\n", fVerbose ? "yes": "no" );
Abc_Print( -2, "usage: exact [-D <num>] [-atvh] <truth1> <truth2> ...\n" );
Abc_Print( -2, "\t finds optimum networks using SAT-based exact synthesis for hex truth tables <truth1> <truth2> ...\n" );
Abc_Print( -2, "\t-D <num> : 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" );
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 ///
......
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment