mirror of https://github.com/YosysHQ/abc.git
New SAT-based optimization package.
This commit is contained in:
Alan Mishchenko
parent
254ac2df8f
commit
585f3a6407
2
Makefile
2
Makefile
|
|
@ -22,7 +22,7 @@ MODULES := \
|
|||
src/misc/mem src/misc/bar src/misc/bbl src/misc/parse \
|
||||
src/opt/cut src/opt/fxu src/opt/fxch src/opt/rwr src/opt/mfs src/opt/sim \
|
||||
src/opt/ret src/opt/fret src/opt/res src/opt/lpk src/opt/nwk src/opt/rwt \
|
||||
src/opt/cgt src/opt/csw src/opt/dar src/opt/dau src/opt/dsc src/opt/sfm \
|
||||
src/opt/cgt src/opt/csw src/opt/dar src/opt/dau src/opt/dsc src/opt/sfm src/opt/sbd \
|
||||
src/sat/bsat src/sat/csat src/sat/msat src/sat/psat src/sat/cnf src/sat/bmc \
|
||||
src/bool/bdc src/bool/deco src/bool/dec src/bool/kit src/bool/lucky \
|
||||
src/bool/rsb src/bool/rpo \
|
||||
|
|
|
|||
32
abclib.dsp
32
abclib.dsp
|
|
@ -2686,6 +2686,38 @@ SOURCE=.\src\opt\dsc\dsc.c
|
|||
SOURCE=.\src\opt\dsc\dsc.h
|
||||
# End Source File
|
||||
# End Group
|
||||
# Begin Group "sbd"
|
||||
|
||||
# PROP Default_Filter ""
|
||||
# Begin Source File
|
||||
|
||||
SOURCE=.\src\opt\sbd\sbd.c
|
||||
# End Source File
|
||||
# Begin Source File
|
||||
|
||||
SOURCE=.\src\opt\sbd\sbd.h
|
||||
# End Source File
|
||||
# Begin Source File
|
||||
|
||||
SOURCE=.\src\opt\sbd\sbdCnf.c
|
||||
# End Source File
|
||||
# Begin Source File
|
||||
|
||||
SOURCE=.\src\opt\sbd\sbdCore.c
|
||||
# End Source File
|
||||
# Begin Source File
|
||||
|
||||
SOURCE=.\src\opt\sbd\sbdInt.h
|
||||
# End Source File
|
||||
# Begin Source File
|
||||
|
||||
SOURCE=.\src\opt\sbd\sbdSat.c
|
||||
# End Source File
|
||||
# Begin Source File
|
||||
|
||||
SOURCE=.\src\opt\sbd\sbdWin.c
|
||||
# End Source File
|
||||
# End Group
|
||||
# End Group
|
||||
# Begin Group "map"
|
||||
|
||||
|
|
|
|||
|
|
@ -0,0 +1,5 @@
|
|||
SRC += src/opt/sbd/sbd.c \
|
||||
src/opt/sbd/sbdCnf.c \
|
||||
src/opt/sbd/sbdCore.c \
|
||||
src/opt/sbd/sbdSat.c \
|
||||
src/opt/sbd/sbdWin.c
|
||||
|
|
@ -0,0 +1,53 @@
|
|||
/**CFile****************************************************************
|
||||
|
||||
FileName [sbd.c]
|
||||
|
||||
SystemName [ABC: Logic synthesis and verification system.]
|
||||
|
||||
PackageName [SAT-based optimization using internal don't-cares.]
|
||||
|
||||
Synopsis []
|
||||
|
||||
Author [Alan Mishchenko]
|
||||
|
||||
Affiliation [UC Berkeley]
|
||||
|
||||
Date [Ver. 1.0. Started - June 20, 2005.]
|
||||
|
||||
Revision [$Id: sbd.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
|
||||
|
||||
***********************************************************************/
|
||||
|
||||
#include "sbdInt.h"
|
||||
|
||||
ABC_NAMESPACE_IMPL_START
|
||||
|
||||
|
||||
////////////////////////////////////////////////////////////////////////
|
||||
/// DECLARATIONS ///
|
||||
////////////////////////////////////////////////////////////////////////
|
||||
|
||||
////////////////////////////////////////////////////////////////////////
|
||||
/// FUNCTION DEFINITIONS ///
|
||||
////////////////////////////////////////////////////////////////////////
|
||||
|
||||
/**Function*************************************************************
|
||||
|
||||
Synopsis []
|
||||
|
||||
Description []
|
||||
|
||||
SideEffects []
|
||||
|
||||
SeeAlso []
|
||||
|
||||
***********************************************************************/
|
||||
|
||||
|
||||
////////////////////////////////////////////////////////////////////////
|
||||
/// END OF FILE ///
|
||||
////////////////////////////////////////////////////////////////////////
|
||||
|
||||
|
||||
ABC_NAMESPACE_IMPL_END
|
||||
|
||||
|
|
@ -0,0 +1,104 @@
|
|||
/**CFile****************************************************************
|
||||
|
||||
FileName [sbd.h]
|
||||
|
||||
SystemName [ABC: Logic synthesis and verification system.]
|
||||
|
||||
PackageName [SAT-based optimization using internal don't-cares.]
|
||||
|
||||
Synopsis [External declarations.]
|
||||
|
||||
Author [Alan Mishchenko]
|
||||
|
||||
Affiliation [UC Berkeley]
|
||||
|
||||
Date [Ver. 1.0. Started - June 20, 2005.]
|
||||
|
||||
Revision [$Id: sbd.h,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
|
||||
|
||||
***********************************************************************/
|
||||
|
||||
#ifndef ABC__opt_sbd__h
|
||||
#define ABC__opt_sbd__h
|
||||
|
||||
////////////////////////////////////////////////////////////////////////
|
||||
/// INCLUDES ///
|
||||
////////////////////////////////////////////////////////////////////////
|
||||
|
||||
////////////////////////////////////////////////////////////////////////
|
||||
/// PARAMETERS ///
|
||||
////////////////////////////////////////////////////////////////////////
|
||||
|
||||
ABC_NAMESPACE_HEADER_START
|
||||
|
||||
////////////////////////////////////////////////////////////////////////
|
||||
/// BASIC TYPES ///
|
||||
////////////////////////////////////////////////////////////////////////
|
||||
|
||||
typedef struct Sbd_Ntk_t_ Sbd_Ntk_t;
|
||||
typedef struct Sbd_Par_t_ Sbd_Par_t;
|
||||
struct Sbd_Par_t_
|
||||
{
|
||||
int nTfoLevMax; // the maximum fanout levels
|
||||
int nTfiLevMax; // the maximum fanin levels
|
||||
int nFanoutMax; // the maximum number of fanouts
|
||||
int nDepthMax; // the maximum depth to try
|
||||
int nVarMax; // the maximum variable count
|
||||
int nMffcMin; // the minimum MFFC size
|
||||
int nMffcMax; // the maximum MFFC size
|
||||
int nDecMax; // the maximum number of decompositions
|
||||
int nWinSizeMax; // the maximum window size
|
||||
int nGrowthLevel; // the maximum allowed growth in level
|
||||
int nBTLimit; // the maximum number of conflicts in one SAT run
|
||||
int nNodesMax; // the maximum number of nodes to try
|
||||
int iNodeOne; // one particular node to try
|
||||
int nFirstFixed; // the number of first nodes to be treated as fixed
|
||||
int nTimeWin; // the size of timing window in percents
|
||||
int DeltaCrit; // delay delta in picoseconds
|
||||
int DelAreaRatio; // delay/area tradeoff (how many ps we trade for a unit of area)
|
||||
int fRrOnly; // perform redundance removal
|
||||
int fArea; // performs optimization for area
|
||||
int fAreaRev; // performs optimization for area in reverse order
|
||||
int fMoreEffort; // performs high-affort minimization
|
||||
int fUseAndOr; // enable internal detection of AND/OR gates
|
||||
int fZeroCost; // enable zero-cost replacement
|
||||
int fUseSim; // enable simulation
|
||||
int fPrintDecs; // enable printing decompositions
|
||||
int fAllBoxes; // enable preserving all boxes
|
||||
int fLibVerbose; // enable library stats
|
||||
int fDelayVerbose; // enable delay stats
|
||||
int fVerbose; // enable basic stats
|
||||
int fVeryVerbose; // enable detailed stats
|
||||
};
|
||||
|
||||
////////////////////////////////////////////////////////////////////////
|
||||
/// MACRO DEFINITIONS ///
|
||||
////////////////////////////////////////////////////////////////////////
|
||||
|
||||
////////////////////////////////////////////////////////////////////////
|
||||
/// FUNCTION DECLARATIONS ///
|
||||
////////////////////////////////////////////////////////////////////////
|
||||
|
||||
/*=== sbdCnf.c ==========================================================*/
|
||||
/*=== sbdCore.c ==========================================================*/
|
||||
extern void Sbd_ParSetDefault( Sbd_Par_t * pPars );
|
||||
extern int Sbd_NtkPerform( Sbd_Ntk_t * p, Sbd_Par_t * pPars );
|
||||
/*=== sbdNtk.c ==========================================================*/
|
||||
extern Sbd_Ntk_t * Sbd_NtkConstruct( Vec_Wec_t * vFanins, int nPis, int nPos, Vec_Str_t * vFixed, Vec_Str_t * vEmpty, Vec_Wrd_t * vTruths );
|
||||
extern void Sbd_NtkFree( Sbd_Ntk_t * p );
|
||||
extern Vec_Int_t * Sbd_NodeReadFanins( Sbd_Ntk_t * p, int i );
|
||||
extern word * Sbd_NodeReadTruth( Sbd_Ntk_t * p, int i );
|
||||
extern int Sbd_NodeReadFixed( Sbd_Ntk_t * p, int i );
|
||||
extern int Sbd_NodeReadUsed( Sbd_Ntk_t * p, int i );
|
||||
/*=== sbdWin.c ==========================================================*/
|
||||
extern Vec_Int_t * Sbd_NtkDfs( Sbd_Ntk_t * p, Vec_Wec_t * vGroups, Vec_Int_t * vGroupMap, Vec_Int_t * vBoxesLeft, int fAllBoxes );
|
||||
|
||||
|
||||
ABC_NAMESPACE_HEADER_END
|
||||
|
||||
#endif
|
||||
|
||||
////////////////////////////////////////////////////////////////////////
|
||||
/// END OF FILE ///
|
||||
////////////////////////////////////////////////////////////////////////
|
||||
|
||||
|
|
@ -0,0 +1,147 @@
|
|||
/**CFile****************************************************************
|
||||
|
||||
FileName [sbdCnf.c]
|
||||
|
||||
SystemName [ABC: Logic synthesis and verification system.]
|
||||
|
||||
PackageName [SAT-based optimization using internal don't-cares.]
|
||||
|
||||
Synopsis [CNF computation.]
|
||||
|
||||
Author [Alan Mishchenko]
|
||||
|
||||
Affiliation [UC Berkeley]
|
||||
|
||||
Date [Ver. 1.0. Started - June 20, 2005.]
|
||||
|
||||
Revision [$Id: sbdCnf.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
|
||||
|
||||
***********************************************************************/
|
||||
|
||||
#include "sbdInt.h"
|
||||
|
||||
ABC_NAMESPACE_IMPL_START
|
||||
|
||||
|
||||
////////////////////////////////////////////////////////////////////////
|
||||
/// DECLARATIONS ///
|
||||
////////////////////////////////////////////////////////////////////////
|
||||
|
||||
////////////////////////////////////////////////////////////////////////
|
||||
/// FUNCTION DEFINITIONS ///
|
||||
////////////////////////////////////////////////////////////////////////
|
||||
|
||||
/**Function*************************************************************
|
||||
|
||||
Synopsis []
|
||||
|
||||
Description []
|
||||
|
||||
SideEffects []
|
||||
|
||||
SeeAlso []
|
||||
|
||||
***********************************************************************/
|
||||
void Sbd_PrintCnf( Vec_Str_t * vCnf )
|
||||
{
|
||||
char Entry;
|
||||
int i, Lit;
|
||||
Vec_StrForEachEntry( vCnf, Entry, i )
|
||||
{
|
||||
Lit = (int)Entry;
|
||||
if ( Lit == -1 )
|
||||
printf( "\n" );
|
||||
else
|
||||
printf( "%s%d ", Abc_LitIsCompl(Lit) ? "-":"", Abc_Lit2Var(Lit) );
|
||||
}
|
||||
}
|
||||
|
||||
/**Function*************************************************************
|
||||
|
||||
Synopsis []
|
||||
|
||||
Description []
|
||||
|
||||
SideEffects []
|
||||
|
||||
SeeAlso []
|
||||
|
||||
***********************************************************************/
|
||||
int Sbd_TruthToCnf( word Truth, int nVars, Vec_Int_t * vCover, Vec_Str_t * vCnf )
|
||||
{
|
||||
Vec_StrClear( vCnf );
|
||||
if ( Truth == 0 || ~Truth == 0 )
|
||||
{
|
||||
// assert( nVars == 0 );
|
||||
Vec_StrPush( vCnf, (char)(Truth == 0) );
|
||||
Vec_StrPush( vCnf, (char)-1 );
|
||||
return 1;
|
||||
}
|
||||
else
|
||||
{
|
||||
int i, k, c, RetValue, Literal, Cube, nCubes = 0;
|
||||
assert( nVars > 0 );
|
||||
for ( c = 0; c < 2; c ++ )
|
||||
{
|
||||
Truth = c ? ~Truth : Truth;
|
||||
RetValue = Kit_TruthIsop( (unsigned *)&Truth, nVars, vCover, 0 );
|
||||
assert( RetValue == 0 );
|
||||
nCubes += Vec_IntSize( vCover );
|
||||
Vec_IntForEachEntry( vCover, Cube, i )
|
||||
{
|
||||
for ( k = 0; k < nVars; k++ )
|
||||
{
|
||||
Literal = 3 & (Cube >> (k << 1));
|
||||
if ( Literal == 1 ) // '0' -> pos lit
|
||||
Vec_StrPush( vCnf, (char)Abc_Var2Lit(k, 0) );
|
||||
else if ( Literal == 2 ) // '1' -> neg lit
|
||||
Vec_StrPush( vCnf, (char)Abc_Var2Lit(k, 1) );
|
||||
else if ( Literal != 0 )
|
||||
assert( 0 );
|
||||
}
|
||||
Vec_StrPush( vCnf, (char)Abc_Var2Lit(nVars, c) );
|
||||
Vec_StrPush( vCnf, (char)-1 );
|
||||
}
|
||||
}
|
||||
return nCubes;
|
||||
}
|
||||
}
|
||||
|
||||
/**Function*************************************************************
|
||||
|
||||
Synopsis []
|
||||
|
||||
Description []
|
||||
|
||||
SideEffects []
|
||||
|
||||
SeeAlso []
|
||||
|
||||
***********************************************************************/
|
||||
void Sbd_TranslateCnf( Vec_Wec_t * vRes, Vec_Str_t * vCnf, Vec_Int_t * vFaninMap, int iPivotVar )
|
||||
{
|
||||
Vec_Int_t * vClause;
|
||||
char Entry;
|
||||
int i, Lit;
|
||||
Vec_WecClear( vRes );
|
||||
vClause = Vec_WecPushLevel( vRes );
|
||||
Vec_StrForEachEntry( vCnf, Entry, i )
|
||||
{
|
||||
if ( (int)Entry == -1 )
|
||||
{
|
||||
vClause = Vec_WecPushLevel( vRes );
|
||||
continue;
|
||||
}
|
||||
Lit = Abc_Lit2LitV( Vec_IntArray(vFaninMap), (int)Entry );
|
||||
Lit = Abc_LitNotCond( Lit, Abc_Lit2Var(Lit) == iPivotVar );
|
||||
Vec_IntPush( vClause, Lit );
|
||||
}
|
||||
}
|
||||
|
||||
////////////////////////////////////////////////////////////////////////
|
||||
/// END OF FILE ///
|
||||
////////////////////////////////////////////////////////////////////////
|
||||
|
||||
|
||||
ABC_NAMESPACE_IMPL_END
|
||||
|
||||
|
|
@ -0,0 +1,53 @@
|
|||
/**CFile****************************************************************
|
||||
|
||||
FileName [sbd.c]
|
||||
|
||||
SystemName [ABC: Logic synthesis and verification system.]
|
||||
|
||||
PackageName [SAT-based optimization using internal don't-cares.]
|
||||
|
||||
Synopsis []
|
||||
|
||||
Author [Alan Mishchenko]
|
||||
|
||||
Affiliation [UC Berkeley]
|
||||
|
||||
Date [Ver. 1.0. Started - June 20, 2005.]
|
||||
|
||||
Revision [$Id: sbd.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
|
||||
|
||||
***********************************************************************/
|
||||
|
||||
#include "sbdInt.h"
|
||||
|
||||
ABC_NAMESPACE_IMPL_START
|
||||
|
||||
|
||||
////////////////////////////////////////////////////////////////////////
|
||||
/// DECLARATIONS ///
|
||||
////////////////////////////////////////////////////////////////////////
|
||||
|
||||
////////////////////////////////////////////////////////////////////////
|
||||
/// FUNCTION DEFINITIONS ///
|
||||
////////////////////////////////////////////////////////////////////////
|
||||
|
||||
/**Function*************************************************************
|
||||
|
||||
Synopsis []
|
||||
|
||||
Description []
|
||||
|
||||
SideEffects []
|
||||
|
||||
SeeAlso []
|
||||
|
||||
***********************************************************************/
|
||||
|
||||
|
||||
////////////////////////////////////////////////////////////////////////
|
||||
/// END OF FILE ///
|
||||
////////////////////////////////////////////////////////////////////////
|
||||
|
||||
|
||||
ABC_NAMESPACE_IMPL_END
|
||||
|
||||
|
|
@ -0,0 +1,75 @@
|
|||
/**CFile****************************************************************
|
||||
|
||||
FileName [rsbInt.h]
|
||||
|
||||
SystemName [ABC: Logic synthesis and verification system.]
|
||||
|
||||
PackageName [SAT-based optimization using internal don't-cares.]
|
||||
|
||||
Synopsis [Internal declarations.]
|
||||
|
||||
Author [Alan Mishchenko]
|
||||
|
||||
Affiliation [UC Berkeley]
|
||||
|
||||
Date [Ver. 1.0. Started - June 20, 2005.]
|
||||
|
||||
Revision [$Id: rsbInt.h,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
|
||||
|
||||
***********************************************************************/
|
||||
|
||||
#ifndef ABC__opt_sbdInt__h
|
||||
#define ABC__opt_sbdInt__h
|
||||
|
||||
|
||||
////////////////////////////////////////////////////////////////////////
|
||||
/// INCLUDES ///
|
||||
////////////////////////////////////////////////////////////////////////
|
||||
|
||||
#include <stdio.h>
|
||||
#include <stdlib.h>
|
||||
#include <string.h>
|
||||
#include <assert.h>
|
||||
|
||||
#include "misc/vec/vec.h"
|
||||
#include "sat/bsat/satSolver.h"
|
||||
#include "misc/util/utilNam.h"
|
||||
#include "map/scl/sclLib.h"
|
||||
#include "map/scl/sclCon.h"
|
||||
#include "bool/kit/kit.h"
|
||||
#include "misc/st/st.h"
|
||||
#include "map/mio/mio.h"
|
||||
#include "base/abc/abc.h"
|
||||
#include "sbd.h"
|
||||
|
||||
////////////////////////////////////////////////////////////////////////
|
||||
/// PARAMETERS ///
|
||||
////////////////////////////////////////////////////////////////////////
|
||||
|
||||
ABC_NAMESPACE_HEADER_START
|
||||
|
||||
|
||||
////////////////////////////////////////////////////////////////////////
|
||||
/// BASIC TYPES ///
|
||||
////////////////////////////////////////////////////////////////////////
|
||||
|
||||
|
||||
////////////////////////////////////////////////////////////////////////
|
||||
/// MACRO DEFINITIONS ///
|
||||
////////////////////////////////////////////////////////////////////////
|
||||
|
||||
|
||||
////////////////////////////////////////////////////////////////////////
|
||||
/// FUNCTION DECLARATIONS ///
|
||||
////////////////////////////////////////////////////////////////////////
|
||||
|
||||
/*=== sbdCnf.c ==========================================================*/
|
||||
|
||||
ABC_NAMESPACE_HEADER_END
|
||||
|
||||
#endif
|
||||
|
||||
////////////////////////////////////////////////////////////////////////
|
||||
/// END OF FILE ///
|
||||
////////////////////////////////////////////////////////////////////////
|
||||
|
||||
|
|
@ -0,0 +1,161 @@
|
|||
/**CFile****************************************************************
|
||||
|
||||
FileName [sbd.c]
|
||||
|
||||
SystemName [ABC: Logic synthesis and verification system.]
|
||||
|
||||
PackageName [SAT-based optimization using internal don't-cares.]
|
||||
|
||||
Synopsis []
|
||||
|
||||
Author [Alan Mishchenko]
|
||||
|
||||
Affiliation [UC Berkeley]
|
||||
|
||||
Date [Ver. 1.0. Started - June 20, 2005.]
|
||||
|
||||
Revision [$Id: sbd.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
|
||||
|
||||
***********************************************************************/
|
||||
|
||||
#include "sbdInt.h"
|
||||
|
||||
ABC_NAMESPACE_IMPL_START
|
||||
|
||||
|
||||
////////////////////////////////////////////////////////////////////////
|
||||
/// DECLARATIONS ///
|
||||
////////////////////////////////////////////////////////////////////////
|
||||
|
||||
#define MAX_M 12 // max inputs
|
||||
#define MAX_N 20 // max nodes
|
||||
#define MAX_K 6 // max lutsize
|
||||
|
||||
////////////////////////////////////////////////////////////////////////
|
||||
/// FUNCTION DEFINITIONS ///
|
||||
////////////////////////////////////////////////////////////////////////
|
||||
|
||||
/**Function*************************************************************
|
||||
|
||||
Synopsis []
|
||||
|
||||
Description []
|
||||
|
||||
SideEffects []
|
||||
|
||||
SeeAlso []
|
||||
|
||||
***********************************************************************/
|
||||
sat_solver * Sbd_SolverTopo( int M, int N, int K, int pVars[MAX_N][MAX_M+MAX_N][MAX_K] ) // inputs, nodes, lutsize
|
||||
{
|
||||
sat_solver * pSat = NULL;
|
||||
Vec_Int_t * vTemp = Vec_IntAlloc(100);
|
||||
// assign vars
|
||||
int RetValue, n, i, k, nVars = 0;
|
||||
for ( n = 0; n < N; n++ )
|
||||
for ( i = 0; i < M+N; i++ )
|
||||
for ( k = 0; k < K; k++ )
|
||||
pVars[n][i][k] = nVars++;
|
||||
printf( "Number of vars = %d.\n", nVars );
|
||||
// add constraints
|
||||
pSat = sat_solver_new();
|
||||
sat_solver_setnvars( pSat, nVars );
|
||||
// each node is used
|
||||
for ( i = 0; i < M+N-1; i++ )
|
||||
{
|
||||
Vec_IntClear( vTemp );
|
||||
for ( n = 0; n < N; n++ )
|
||||
for ( k = 0; k < K; k++ )
|
||||
Vec_IntPush( vTemp, Abc_Var2Lit(pVars[n][i][k], 0) );
|
||||
RetValue = sat_solver_addclause( pSat, Vec_IntArray(vTemp), Vec_IntLimit(vTemp) );
|
||||
assert( RetValue );
|
||||
}
|
||||
// each fanin of each node is connected
|
||||
for ( n = 0; n < N; n++ )
|
||||
for ( k = 0; k < K; k++ )
|
||||
{
|
||||
Vec_IntClear( vTemp );
|
||||
for ( i = 0; i < M+n; i++ )
|
||||
Vec_IntPush( vTemp, Abc_Var2Lit(pVars[n][i][k], 0) );
|
||||
RetValue = sat_solver_addclause( pSat, Vec_IntArray(vTemp), Vec_IntLimit(vTemp) );
|
||||
assert( RetValue );
|
||||
}
|
||||
// each fanin is connected once; fanins are ordered; nodes are ordered
|
||||
for ( n = 0; n < N; n++ )
|
||||
for ( i = 0; i < M+N; i++ )
|
||||
for ( k = 0; k < K; k++ )
|
||||
{
|
||||
int n2, i2, k2;
|
||||
for ( n2 = 0; n2 <=n; n2++ )
|
||||
for ( i2 = i; i2 < M+N; i2++ )
|
||||
for ( k2 = k; k2 < K; k2++ )
|
||||
{
|
||||
if ( n2 == n && i2 == i && k2 == k )
|
||||
continue;
|
||||
Vec_IntPushTwo( vTemp, Abc_Var2Lit(pVars[n][i][k], 1), Abc_Var2Lit(pVars[n2][i2][k2], 1) );
|
||||
RetValue = sat_solver_addclause( pSat, Vec_IntArray(vTemp), Vec_IntLimit(vTemp) );
|
||||
assert( RetValue );
|
||||
}
|
||||
}
|
||||
Vec_IntFree( vTemp );
|
||||
return pSat;
|
||||
}
|
||||
void Sbd_SolverTopoPrint( sat_solver * pSat, int M, int N, int K, int pVars[MAX_N][MAX_M+MAX_N][MAX_K] )
|
||||
{
|
||||
int n, i, k;
|
||||
printf( "Solution:\n" );
|
||||
for ( i = M+N-1; i >= 0; i-- )
|
||||
{
|
||||
printf( "%2d %c : ", i, i < M ? 'i' : 'n' );
|
||||
for ( n = 0; n < N; n++ )
|
||||
{
|
||||
for ( k = 0; k < K; k++ )
|
||||
printf( "%c", sat_solver_var_value(pSat, pVars[n][i][k]) ? '*' : '.' );
|
||||
printf( " " );
|
||||
}
|
||||
printf( "\n" );
|
||||
}
|
||||
}
|
||||
void Sbd_SolverTopoTest()
|
||||
{
|
||||
int M = 4; // inputs
|
||||
int N = 3; // nodes
|
||||
int K = 2; // lutsize
|
||||
int status, nCalls, v, nVars;
|
||||
int pVars[MAX_N][MAX_M+MAX_N][MAX_K]; // 20 x 32 x 6 = 3840
|
||||
Vec_Int_t * vLits = Vec_IntAlloc(100);
|
||||
sat_solver * pSat = Sbd_SolverTopo( M, N, K, pVars );
|
||||
nVars = sat_solver_nvars( pSat );
|
||||
for ( nCalls = 0; nCalls < 1000000; nCalls++ )
|
||||
{
|
||||
// find onset minterm
|
||||
status = sat_solver_solve( pSat, NULL, NULL, 0, 0, 0, 0 );
|
||||
if ( status == l_Undef )
|
||||
break;
|
||||
if ( status == l_False )
|
||||
break;
|
||||
assert( status == l_True );
|
||||
// print solution
|
||||
Sbd_SolverTopoPrint( pSat, M, N, K, pVars );
|
||||
// remember variable values
|
||||
Vec_IntClear( vLits );
|
||||
for ( v = 0; v < nVars; v++ )
|
||||
if ( sat_solver_var_value(pSat, v) )
|
||||
Vec_IntPush( vLits, Abc_Var2Lit(v, 1) );
|
||||
// add breaking clause
|
||||
status = sat_solver_addclause( pSat, Vec_IntArray(vLits), Vec_IntLimit(vLits) );
|
||||
assert( status );
|
||||
}
|
||||
printf( "Found %d solutions.\n", nCalls );
|
||||
sat_solver_delete( pSat );
|
||||
Vec_IntFree( vLits );
|
||||
}
|
||||
|
||||
|
||||
////////////////////////////////////////////////////////////////////////
|
||||
/// END OF FILE ///
|
||||
////////////////////////////////////////////////////////////////////////
|
||||
|
||||
|
||||
ABC_NAMESPACE_IMPL_END
|
||||
|
||||
|
|
@ -0,0 +1,52 @@
|
|||
/**CFile****************************************************************
|
||||
|
||||
FileName [sbd.c]
|
||||
|
||||
SystemName [ABC: Logic synthesis and verification system.]
|
||||
|
||||
PackageName [SAT-based optimization using internal don't-cares.]
|
||||
|
||||
Synopsis []
|
||||
|
||||
Author [Alan Mishchenko]
|
||||
|
||||
Affiliation [UC Berkeley]
|
||||
|
||||
Date [Ver. 1.0. Started - June 20, 2005.]
|
||||
|
||||
Revision [$Id: sbd.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
|
||||
|
||||
***********************************************************************/
|
||||
|
||||
#include "sbdInt.h"
|
||||
|
||||
ABC_NAMESPACE_IMPL_START
|
||||
|
||||
|
||||
////////////////////////////////////////////////////////////////////////
|
||||
/// DECLARATIONS ///
|
||||
////////////////////////////////////////////////////////////////////////
|
||||
|
||||
////////////////////////////////////////////////////////////////////////
|
||||
/// FUNCTION DEFINITIONS ///
|
||||
////////////////////////////////////////////////////////////////////////
|
||||
|
||||
/**Function*************************************************************
|
||||
|
||||
Synopsis []
|
||||
|
||||
Description []
|
||||
|
||||
SideEffects []
|
||||
|
||||
SeeAlso []
|
||||
|
||||
***********************************************************************/
|
||||
|
||||
////////////////////////////////////////////////////////////////////////
|
||||
/// END OF FILE ///
|
||||
////////////////////////////////////////////////////////////////////////
|
||||
|
||||
|
||||
ABC_NAMESPACE_IMPL_END
|
||||
|
||||
Loading…
Reference in New Issue