luke
/
abc
mirror of https://github.com/YosysHQ/abc.git
1
0
Fork 0
Code Issues Packages Projects Releases Wiki Activity

Updates to delay optimization project.

This commit is contained in:
Alan Mishchenko 2016-12-25 15:58:54 +07:00
parent b9dfb992c7
commit ac3216cf23
7 changed files with 555 additions and 63 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

4
abclib.dsp
View File

@ -2763,6 +2763,10 @@ SOURCE=.\src\opt\sbd\sbdInt.h
# End Source File
# Begin Source File
SOURCE=.\src\opt\sbd\sbdLut.c
# End Source File
# Begin Source File
SOURCE=.\src\opt\sbd\sbdSat.c
# End Source File
# Begin Source File

1
src/opt/sbd/module.make
View File

@ -1,5 +1,6 @@
SRC += src/opt/sbd/sbd.c \
src/opt/sbd/sbdCnf.c \
src/opt/sbd/sbdCore.c \
src/opt/sbd/sbdLut.c \
src/opt/sbd/sbdSat.c \
src/opt/sbd/sbdWin.c

166
src/opt/sbd/sbdCore.c
View File

@ -54,10 +54,12 @@ struct Sbd_Man_t_
abctime timeTotal;
// target node
int Pivot; // target node
int DivCutoff; // the place where D-2 divisors begin
Vec_Int_t * vTfo; // TFO (excludes node, includes roots) - precomputed
Vec_Int_t * vRoots; // TFO root nodes
Vec_Int_t * vWinObjs; // TFI + Pivot + sideTFI + TFO (including roots)
Vec_Int_t * vObj2Var; // SAT variables for the window (indexes of objects in vWinObjs)
Vec_Int_t * vDivSet; // divisor variables
Vec_Int_t * vDivVars; // divisor variables
Vec_Int_t * vDivValues; // SAT variables values for the divisor variables
Vec_Wec_t * vDivLevels; // divisors collected by levels
@ -200,6 +202,7 @@ Sbd_Man_t * Sbd_ManStart( Gia_Man_t * pGia, Sbd_Par_t * pPars )
p->vRoots = Vec_IntAlloc( 100 );
p->vWinObjs = Vec_IntAlloc( Gia_ManObjNum(pGia) );
p->vObj2Var = Vec_IntStart( Gia_ManObjNum(pGia) );
p->vDivSet = Vec_IntAlloc( 100 );
p->vDivVars = Vec_IntAlloc( 100 );
p->vDivValues = Vec_IntAlloc( 100 );
p->vDivLevels = Vec_WecAlloc( 100 );
@ -234,6 +237,7 @@ void Sbd_ManStop( Sbd_Man_t * p )
Vec_IntFree( p->vRoots );
Vec_IntFree( p->vWinObjs );
Vec_IntFree( p->vObj2Var );
Vec_IntFree( p->vDivSet );
Vec_IntFree( p->vDivVars );
Vec_IntFree( p->vDivValues );
Vec_WecFree( p->vDivLevels );
@ -318,12 +322,11 @@ void Sbd_ManUpdateOrder( Sbd_Man_t * p, int Pivot )
Vec_WecInit( p->vDivLevels, LevelMax + 1 );
Vec_IntForEachEntry( p->vWinObjs, Node, i )
Vec_WecPush( p->vDivLevels, Vec_IntEntry(p->vLutLevs, Node), Node );
// sort primary inputs
Vec_IntSort( Vec_WecEntry(p->vDivLevels, 0), 0 );
// reload divisors
Vec_IntClear( p->vWinObjs );
Vec_WecForEachLevel( p->vDivLevels, vLevel, i )
{
Vec_IntSort( vLevel, 0 );
Vec_IntForEachEntry( vLevel, Node, k )
{
Vec_IntWriteEntry( p->vObj2Var, Node, Vec_IntSize(p->vWinObjs) );
@ -334,8 +337,26 @@ void Sbd_ManUpdateOrder( Sbd_Man_t * p, int Pivot )
nTimeValidDivs = Vec_IntSize(p->vWinObjs);
}
assert( nTimeValidDivs > 0 );
Vec_IntFill( p->vDivValues, Abc_MinInt(63, nTimeValidDivs), 0 );
//printf( "%d ", Abc_MinInt(63, nTimeValidDivs) );
Vec_IntClear( p->vDivVars );
p->DivCutoff = -1;
Vec_IntForEachEntryStartStop( p->vWinObjs, Node, i, Abc_MaxInt(0, nTimeValidDivs-63), nTimeValidDivs )
{
if ( p->DivCutoff == -1 && Vec_IntEntry(p->vLutLevs, Node) == LevelMax - 2 )
p->DivCutoff = Vec_IntSize(p->vDivVars);
Vec_IntPush( p->vDivVars, i );
}
if ( p->DivCutoff == -1 )
p->DivCutoff = 0;
// verify
assert( Vec_IntSize(p->vDivVars) < 64 );
Vec_IntForEachEntryStart( p->vDivVars, Node, i, p->DivCutoff )
assert( Vec_IntEntry(p->vLutLevs, Vec_IntEntry(p->vWinObjs, Node)) == LevelMax - 2 );
Vec_IntForEachEntryStop( p->vDivVars, Node, i, p->DivCutoff )
assert( Vec_IntEntry(p->vLutLevs, Vec_IntEntry(p->vWinObjs, Node)) < LevelMax - 2 );
Vec_IntFill( p->vDivValues, Vec_IntSize(p->vDivVars), 0 );
//printf( "%d ", Vec_IntSize(p->vDivVars) );
// printf( "Node %4d : Win = %5d. Divs = %5d. D1 = %5d. D2 = %5d.\n",
// Pivot, Vec_IntSize(p->vWinObjs), Vec_IntSize(p->vDivVars), Vec_IntSize(p->vDivVars)-p->DivCutoff, p->DivCutoff );
}
void Sbd_ManWindowSim_rec( Sbd_Man_t * p, int NodeInit )
{
@ -408,6 +429,8 @@ int Sbd_ManWindow( Sbd_Man_t * p, int Pivot )
Gia_ObjSetTravIdCurrentId(p->pGia, 0);
Sbd_ManWindowSim_rec( p, Pivot );
Sbd_ManUpdateOrder( p, Pivot );
assert( Vec_IntSize(p->vDivVars) == Vec_IntSize(p->vDivValues) );
assert( Vec_IntSize(p->vDivVars) < Vec_IntSize(p->vWinObjs) );
// simulate node
Gia_ManObj(p->pGia, Pivot)->fMark0 = 1;
Abc_TtCopy( Sbd_ObjSim1(p, Pivot), Sbd_ObjSim0(p, Pivot), p->pPars->nWords, 1 );
@ -440,8 +463,8 @@ int Sbd_ManWindow( Sbd_Man_t * p, int Pivot )
p->timeWin += Abc_Clock() - clk;
// propagate controlability to fanins for the TFI nodes starting from the pivot
Sbd_ManPropagateControl( p, Pivot );
assert( Vec_IntSize(p->vDivValues) < 64 );
return (int)(Vec_IntSize(p->vDivValues) >= 64);
assert( Vec_IntSize(p->vDivValues) <= 64 );
return (int)(Vec_IntSize(p->vDivValues) > 64);
}
/**Function*************************************************************
@ -466,8 +489,8 @@ int Sbd_ManCheckConst( Sbd_Man_t * p, int Pivot )
int RetValue, i, iObj, Ind, fFindOnset, nCares[2] = {0};
abctime clk = Abc_Clock();
extern int Sbd_ManCollectConstants( sat_solver * pSat, int nCareMints[2], int PivotVar, word * pVarSims[], Vec_Int_t * vInds );
extern sat_solver * Sbd_ManSatSolver( sat_solver * pSat, Gia_Man_t * p, Vec_Int_t * vMirrors, int Pivot, Vec_Int_t * vWinObjs, Vec_Int_t * vObj2Var, Vec_Int_t * vTfo, Vec_Int_t * vRoots );
p->pSat = Sbd_ManSatSolver( p->pSat, p->pGia, p->vMirrors, Pivot, p->vWinObjs, p->vObj2Var, p->vTfo, p->vRoots );
extern sat_solver * Sbd_ManSatSolver( sat_solver * pSat, Gia_Man_t * p, Vec_Int_t * vMirrors, int Pivot, Vec_Int_t * vWinObjs, Vec_Int_t * vObj2Var, Vec_Int_t * vTfo, Vec_Int_t * vRoots, int fQbf );
p->pSat = Sbd_ManSatSolver( p->pSat, p->pGia, p->vMirrors, Pivot, p->vWinObjs, p->vObj2Var, p->vTfo, p->vRoots, 0 );
p->timeCnf += Abc_Clock() - clk;
if ( p->pSat == NULL )
{
@ -836,11 +859,11 @@ static inline int Sbd_ManFindCandsSimple( Sbd_Man_t * p, word Cover[64], int nDi
{
int c0, c1, c2, c3;
word Target = Cover[nDivs];
Vec_IntClear( p->vDivVars );
Vec_IntClear( p->vDivSet );
for ( c0 = 0; c0 < nDivs; c0++ )
if ( Cover[c0] == Target )
{
Vec_IntPush( p->vDivVars, c0 );
Vec_IntPush( p->vDivSet, c0 );
return 1;
}
@ -848,8 +871,8 @@ static inline int Sbd_ManFindCandsSimple( Sbd_Man_t * p, word Cover[64], int nDi
for ( c1 = c0+1; c1 < nDivs; c1++ )
if ( (Cover[c0] | Cover[c1]) == Target )
{
Vec_IntPush( p->vDivVars, c0 );
Vec_IntPush( p->vDivVars, c1 );
Vec_IntPush( p->vDivSet, c0 );
Vec_IntPush( p->vDivSet, c1 );
return 1;
}
@ -858,9 +881,9 @@ static inline int Sbd_ManFindCandsSimple( Sbd_Man_t * p, word Cover[64], int nDi
for ( c2 = c1+1; c2 < nDivs; c2++ )
if ( (Cover[c0] | Cover[c1] | Cover[c2]) == Target )
{
Vec_IntPush( p->vDivVars, c0 );
Vec_IntPush( p->vDivVars, c1 );
Vec_IntPush( p->vDivVars, c2 );
Vec_IntPush( p->vDivSet, c0 );
Vec_IntPush( p->vDivSet, c1 );
Vec_IntPush( p->vDivSet, c2 );
return 1;
}
@ -871,10 +894,10 @@ static inline int Sbd_ManFindCandsSimple( Sbd_Man_t * p, word Cover[64], int nDi
{
if ( (Cover[c0] | Cover[c1] | Cover[c2] | Cover[c3]) == Target )
{
Vec_IntPush( p->vDivVars, c0 );
Vec_IntPush( p->vDivVars, c1 );
Vec_IntPush( p->vDivVars, c2 );
Vec_IntPush( p->vDivVars, c3 );
Vec_IntPush( p->vDivSet, c0 );
Vec_IntPush( p->vDivSet, c1 );
Vec_IntPush( p->vDivSet, c2 );
Vec_IntPush( p->vDivSet, c3 );
return 1;
}
}
@ -891,11 +914,11 @@ static inline int Sbd_ManFindCands( Sbd_Man_t * p, word Cover[64], int nDivs )
if ( nDivs < 8 || p->pPars->fCover )
return Sbd_ManFindCandsSimple( p, Cover, nDivs );
Vec_IntClear( p->vDivVars );
Vec_IntClear( p->vDivSet );
for ( c0 = 0; c0 < nDivs; c0++ )
if ( Cover[c0] == Target )
{
Vec_IntPush( p->vDivVars, c0 );
Vec_IntPush( p->vDivSet, c0 );
return 1;
}
@ -903,8 +926,8 @@ static inline int Sbd_ManFindCands( Sbd_Man_t * p, word Cover[64], int nDivs )
for ( c1 = c0+1; c1 < nDivs; c1++ )
if ( (Cover[c0] | Cover[c1]) == Target )
{
Vec_IntPush( p->vDivVars, c0 );
Vec_IntPush( p->vDivVars, c1 );
Vec_IntPush( p->vDivSet, c0 );
Vec_IntPush( p->vDivSet, c1 );
return 1;
}
@ -923,9 +946,9 @@ static inline int Sbd_ManFindCands( Sbd_Man_t * p, word Cover[64], int nDivs )
for ( c2 = c1+1; c2 < Limits[2]; c2++ )
if ( (Cover[Order[c0]] | Cover[Order[c1]] | Cover[Order[c2]]) == Target )
{
Vec_IntPush( p->vDivVars, Order[c0] );
Vec_IntPush( p->vDivVars, Order[c1] );
Vec_IntPush( p->vDivVars, Order[c2] );
Vec_IntPush( p->vDivSet, Order[c0] );
Vec_IntPush( p->vDivSet, Order[c1] );
Vec_IntPush( p->vDivSet, Order[c2] );
return 1;
}
@ -936,10 +959,10 @@ static inline int Sbd_ManFindCands( Sbd_Man_t * p, word Cover[64], int nDivs )
{
if ( (Cover[Order[c0]] | Cover[Order[c1]] | Cover[Order[c2]] | Cover[Order[c3]]) == Target )
{
Vec_IntPush( p->vDivVars, Order[c0] );
Vec_IntPush( p->vDivVars, Order[c1] );
Vec_IntPush( p->vDivVars, Order[c2] );
Vec_IntPush( p->vDivVars, Order[c3] );
Vec_IntPush( p->vDivSet, Order[c0] );
Vec_IntPush( p->vDivSet, Order[c1] );
Vec_IntPush( p->vDivSet, Order[c2] );
Vec_IntPush( p->vDivSet, Order[c3] );
return 1;
}
}
@ -952,10 +975,10 @@ int Sbd_ManExplore( Sbd_Man_t * p, int Pivot, word * pTruth )
int fVerbose = 0;
abctime clk, clkSat = 0, clkEnu = 0, clkAll = Abc_Clock();
int nIters, nItersMax = 32;
extern word Sbd_ManSolve( sat_solver * pSat, int PivotVar, int FreeVar, Vec_Int_t * vDivVars, Vec_Int_t * vValues, Vec_Int_t * vTemp );
extern word Sbd_ManSolve( sat_solver * pSat, int PivotVar, int FreeVar, Vec_Int_t * vDivSet, Vec_Int_t * vDivVars, Vec_Int_t * vDivValues, Vec_Int_t * vTemp );
word MatrS[64] = {0}, MatrC[2][64] = {{0}}, Cubes[2][2][64] = {{{0}}}, Cover[64] = {0}, Cube, CubeNew[2];
int i, k, n, Index, nCubes[2] = {0}, nRows = 0, nRowsOld;
int i, k, n, Node, Index, nCubes[2] = {0}, nRows = 0, nRowsOld;
int nDivs = Vec_IntSize(p->vDivValues);
int PivotVar = Vec_IntEntry(p->vObj2Var, Pivot);
@ -969,11 +992,11 @@ int Sbd_ManExplore( Sbd_Man_t * p, int Pivot, word * pTruth )
Sbd_ManPrintObj( p, Pivot );
// collect bit-matrices
for ( i = 0; i < nDivs; i++ )
Vec_IntForEachEntry( p->vDivVars, Node, i )
{
MatrS[63-i] = *Sbd_ObjSim0( p, Vec_IntEntry(p->vWinObjs, i) );
MatrC[0][63-i] = *Sbd_ObjSim2( p, Vec_IntEntry(p->vWinObjs, i) );
MatrC[1][63-i] = *Sbd_ObjSim3( p, Vec_IntEntry(p->vWinObjs, i) );
MatrS[63-i] = *Sbd_ObjSim0( p, Vec_IntEntry(p->vWinObjs, Node) );
MatrC[0][63-i] = *Sbd_ObjSim2( p, Vec_IntEntry(p->vWinObjs, Node) );
MatrC[1][63-i] = *Sbd_ObjSim3( p, Vec_IntEntry(p->vWinObjs, Node) );
}
MatrS[63-i] = *Sbd_ObjSim0( p, Pivot );
MatrC[0][63-i] = *Sbd_ObjSim2( p, Pivot );
@ -1067,10 +1090,10 @@ int Sbd_ManExplore( Sbd_Man_t * p, int Pivot, word * pTruth )
if ( p->pPars->fVerbose )
printf( "Candidate support: " ),
Vec_IntPrint( p->vDivVars );
Vec_IntPrint( p->vDivSet );
clk = Abc_Clock();
*pTruth = Sbd_ManSolve( p->pSat, PivotVar, FreeVar+nIters, p->vDivVars, p->vDivValues, p->vLits );
*pTruth = Sbd_ManSolve( p->pSat, PivotVar, FreeVar+nIters, p->vDivSet, p->vDivVars, p->vDivValues, p->vLits );
clkSat += Abc_Clock() - clk;
if ( *pTruth == SBD_SAT_UNDEC )
@ -1103,7 +1126,7 @@ int Sbd_ManExplore( Sbd_Man_t * p, int Pivot, word * pTruth )
if ( p->pPars->fVerbose )
{
printf( "Node %d: UNSAT.\n", Pivot );
Extra_PrintBinary( stdout, (unsigned *)pTruth, 1 << Vec_IntSize(p->vDivVars) ), printf( "\n" );
Extra_PrintBinary( stdout, (unsigned *)pTruth, 1 << Vec_IntSize(p->vDivSet) ), printf( "\n" );
}
RetValue = 1;
break;
@ -1118,6 +1141,13 @@ int Sbd_ManExplore( Sbd_Man_t * p, int Pivot, word * pTruth )
return RetValue;
}
int Sbd_ManExplore2( Sbd_Man_t * p, int Pivot,
int nLuts, int nSels, int nVarsDivs[SBD_LUTS_MAX],
int pVarsDivs[SBD_LUTS_MAX][SBD_SIZE_MAX], word Truths[SBD_LUTS_MAX] )
{
return 0;
}
/**Function*************************************************************
Synopsis [Computes delay-oriented k-feasible cut at the node.]
@ -1233,7 +1263,7 @@ int Sbd_ManMergeCuts( Sbd_Man_t * p, int Node )
Vec_IntWriteEntry( p->vLutLevs, Node, LevCur );
assert( pCutRes[0] <= p->pPars->nLutSize );
memcpy( Sbd_ObjCut(p, Node), pCutRes, sizeof(int) * (pCutRes[0] + 1) );
//printf( "Setting node %d with delay %d.\n", Node, LevCur );
//printf( "Setting node %d with delay %d.\n", Node, LevCur );
return LevCur == 1; // LevCur == Abc_MaxInt(Level0, Level1);
}
int Sbd_ManDelay( Sbd_Man_t * p )
@ -1306,7 +1336,7 @@ int Sbd_ManImplement( Sbd_Man_t * p, int Pivot, word Truth )
int iNewLev;
// collect leaf literals
Vec_IntClear( p->vLits );
Vec_IntForEachEntry( p->vDivVars, Node, i )
Vec_IntForEachEntry( p->vDivSet, Node, i )
{
Node = Vec_IntEntry( p->vWinObjs, Node );
if ( Vec_IntEntry(p->vMirrors, Node) >= 0 )
@ -1429,20 +1459,68 @@ Gia_Man_t * Sbd_ManDerive( Gia_Man_t * p, Vec_Int_t * vMirrors )
***********************************************************************/
void Sbd_NtkPerformOne( Sbd_Man_t * p, int Pivot )
{
// extern void Sbd_ManSolveSelect( Gia_Man_t * p, Vec_Int_t * vMirrors, int Pivot, Vec_Int_t * vDivVars, Vec_Int_t * vDivValues, Vec_Int_t * vWinObjs, Vec_Int_t * vObj2Var, Vec_Int_t * vTfo, Vec_Int_t * vRoots );
int RetValue; word Truth = 0;
if ( Sbd_ManMergeCuts( p, Pivot ) )
return;
//if ( Pivot != 344 )
// continue;
// if ( Pivot != 13 )
// return;
if ( p->pPars->fVerbose )
printf( "\nLooking at node %d\n", Pivot );
if ( Sbd_ManWindow( p, Pivot ) )
return;
// Sbd_ManSolveSelect( p->pGia, p->vMirrors, Pivot, p->vDivVars, p->vDivValues, p->vWinObjs, p->vObj2Var, p->vTfo, p->vRoots );
RetValue = Sbd_ManCheckConst( p, Pivot );
if ( RetValue >= 0 )
{
Vec_IntWriteEntry( p->vMirrors, Pivot, RetValue );
//printf( " --> Pivot %4d. Constant %d.\n", Pivot, RetValue );
}
else if ( Sbd_ManExplore( p, Pivot, &Truth ) )
{
Sbd_ManImplement( p, Pivot, Truth );
//printf( " --> Pivot %4d. Supp %d.\n", Pivot, Vec_IntSize(p->vDivSet) );
}
/*
else
{
extern int Sbd_ProblemSolve(
Gia_Man_t * p, Vec_Int_t * vMirrors,
int Pivot, Vec_Int_t * vWinObjs, Vec_Int_t * vObj2Var,
Vec_Int_t * vTfo, Vec_Int_t * vRoots,
Vec_Int_t * vDivSet, int nStrs, Sbd_Str_t * pStr0, word Truths[SBD_LUTS_MAX]
);
Sbd_Str_t Strs[2] = {
{1, 4, {0, 1, 2, 7}},
{1, 4, {3, 4, 5, 6}}
};
word Truths[SBD_LUTS_MAX];
Vec_Int_t * vDivSet = Vec_IntAlloc( 8 );
int i, RetValue;
for ( i = 0; i < 7; i++ )
Vec_IntPush( vDivSet, i+1 );
RetValue = Sbd_ProblemSolve( p->pGia, p->vMirrors,
Pivot, p->vWinObjs, p->vObj2Var, p->vTfo, p->vRoots,
vDivSet, 2, Strs, Truths );
if ( RetValue )
{
printf( "Solving succeded.\n" );
//Sbd_ManImplement2( p, Pivot, Truth, nLuts, nSels, nVarsDivs, pVarsDivs, Truths );
}
Vec_IntFree( vDivSet );
}
*/
}
Gia_Man_t * Sbd_NtkPerform( Gia_Man_t * pGia, Sbd_Par_t * pPars )
{
@ -1488,8 +1566,10 @@ Gia_Man_t * Sbd_NtkPerform( Gia_Man_t * pGia, Sbd_Par_t * pPars )
else
{
Gia_ManForEachAndId( pGia, Pivot )
{
if ( Pivot < nNodesOld )
Sbd_NtkPerformOne( p, Pivot );
}
}
printf( "Found %d constants and %d replacements with delay %d. ", p->nConsts, p->nChanges, Sbd_ManDelay(p) );
p->timeTotal = Abc_Clock() - p->timeTotal;

11
src/opt/sbd/sbdInt.h
View File

@ -52,10 +52,21 @@ ABC_NAMESPACE_HEADER_START
#define SBD_SAT_UNDEC 0x1234567812345678
#define SBD_SAT_SAT 0x8765432187654321
#define SBD_LUTS_MAX 2
#define SBD_SIZE_MAX 4
#define SBD_DIV_MAX 7
////////////////////////////////////////////////////////////////////////
/// BASIC TYPES ///
////////////////////////////////////////////////////////////////////////
typedef struct Sbd_Str_t_ Sbd_Str_t;
struct Sbd_Str_t_
{
int fLut; // LUT or SEL
int nVarIns; // input count
int VarIns[SBD_DIV_MAX]; // input vars
};
////////////////////////////////////////////////////////////////////////
/// MACRO DEFINITIONS ///

255
src/opt/sbd/sbdLut.c Normal file
View File

@ -0,0 +1,255 @@
/**CFile****************************************************************
FileName [sbdLut.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: sbdLut.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 []
***********************************************************************/
// count the number of parameter variables in the structure
int Sbd_ProblemCountParams( int nStrs, Sbd_Str_t * pStr0 )
{
Sbd_Str_t * pStr; int nPars = 0;
for ( pStr = pStr0; pStr < pStr0 + nStrs; pStr++ )
nPars += (pStr->fLut ? 1 << pStr->nVarIns : pStr->nVarIns);
return nPars;
}
// add clauses for the structure
void Sbd_ProblemAddClauses( sat_solver * pSat, int nVars, int nStrs, int * pVars, Sbd_Str_t * pStr0 )
{
// variable order: inputs, structure outputs, parameters
Sbd_Str_t * pStr;
int VarOut = nVars;
int VarPar = nVars + nStrs;
int m, k, n, status, pLits[SBD_SIZE_MAX+2];
for ( pStr = pStr0; pStr < pStr0 + nStrs; pStr++, VarOut++ )
{
if ( pStr->fLut )
{
int nMints = 1 << pStr->nVarIns;
assert( pStr->nVarIns <= 6 );
for ( m = 0; m < nMints; m++, VarPar++ )
{
for ( k = 0; k < pStr->nVarIns; k++ )
pLits[k] = Abc_Var2Lit( pVars[pStr->VarIns[k]], (m >> k) & 1 );
for ( n = 0; n < 2; n++ )
{
pLits[pStr->nVarIns] = Abc_Var2Lit( pVars[VarPar], n );
pLits[pStr->nVarIns+1] = Abc_Var2Lit( pVars[VarOut], !n );
status = sat_solver_addclause( pSat, pLits, pLits + pStr->nVarIns + 2 );
assert( status );
}
}
}
else
{
for ( k = 0; k < pStr->nVarIns; k++, VarPar++ )
{
for ( n = 0; n < 2; n++ )
{
pLits[0] = Abc_Var2Lit( pVars[VarPar], 1 );
pLits[1] = Abc_Var2Lit( pVars[VarOut], n );
pLits[2] = Abc_Var2Lit( pVars[pStr->VarIns[k]], !n );
status = sat_solver_addclause( pSat, pLits, pLits + 3 );
assert( status );
}
}
}
}
}
void Sbd_ProblemAddClausesInit( sat_solver * pSat, int nVars, int nStrs, int * pVars, Sbd_Str_t * pStr0 )
{
Sbd_Str_t * pStr;
int VarPar = nVars + nStrs;
int m, m2, pLits[2], status;
// make sure selector parameters are mutually exclusive
for ( pStr = pStr0; pStr < pStr0 + nStrs; pStr++, VarPar = pStr->fLut ? 1 << pStr->nVarIns : pStr->nVarIns )
{
if ( pStr->fLut )
continue;
for ( m = 0; m < pStr->nVarIns; m++ )
for ( m2 = m+1; m2 < pStr->nVarIns; m2++ )
{
pLits[0] = Abc_Var2Lit( pVars[VarPar + m], 1 );
pLits[1] = Abc_Var2Lit( pVars[VarPar + m2], 1 );
status = sat_solver_addclause( pSat, pLits, pLits + 2 );
assert( status );
}
}
}
void Sbd_ProblemPrintSolution( int nStrs, Sbd_Str_t * pStr0, Vec_Int_t * vLits )
{
Sbd_Str_t * pStr;
int m, nIters, iLit = 0;
printf( "Solution found:\n" );
for ( pStr = pStr0; pStr < pStr0 + nStrs; pStr++ )
{
nIters = pStr->fLut ? 1 << pStr->nVarIns : pStr->nVarIns;
printf( "%s%d : ", pStr->fLut ? "LUT":"SEL", pStr-pStr0 );
for ( m = 0; m < nIters; m++ )
printf( "%d", Abc_LitIsCompl(Vec_IntEntry(vLits, iLit++)) );
printf( "\n" );
}
assert( iLit == Vec_IntSize(vLits) );
}
void Sbd_ProblemCollectSolution( int nStrs, Sbd_Str_t * pStr0, Vec_Int_t * vLits, word Truths[SBD_LUTS_MAX] )
{
}
/**Function*************************************************************
Synopsis [Solves QBF problem for the given window.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
int Sbd_ProblemSolve( Gia_Man_t * p, Vec_Int_t * vMirrors,
int Pivot, Vec_Int_t * vWinObjs, Vec_Int_t * vObj2Var,
Vec_Int_t * vTfo, Vec_Int_t * vRoots,
Vec_Int_t * vDivSet, int nStrs, Sbd_Str_t * pStr0, word Truths[SBD_LUTS_MAX] ) // divisors, structures
{
extern sat_solver * Sbd_ManSatSolver( sat_solver * pSat, Gia_Man_t * p, Vec_Int_t * vMirrors, int Pivot, Vec_Int_t * vWinObjs, Vec_Int_t * vObj2Var, Vec_Int_t * vTfo, Vec_Int_t * vRoots, int fQbf );
Vec_Int_t * vLits = Vec_IntAlloc( 100 );
sat_solver * pSatCec = Sbd_ManSatSolver( NULL, p, vMirrors, Pivot, vWinObjs, vObj2Var, vTfo, vRoots, 1 );
sat_solver * pSatQbf = sat_solver_new();
int nVars = Vec_IntSize( vDivSet );
int nPars = Sbd_ProblemCountParams( nStrs, pStr0 );
int VarCecOut = Vec_IntSize(vWinObjs) + Vec_IntSize(vTfo) + Vec_IntSize(vRoots);
int VarCecPar = VarCecOut + 1;
int VarCecFree = VarCecPar + nPars;
int VarQbfPar = 0;
int VarQbfFree = nPars;
int pVarsCec[256];
int pVarsQbf[256];
int i, iVar, iLit;
int RetValue = 0;
assert( Vec_IntSize(vDivSet) <= SBD_SIZE_MAX );
assert( nVars + nStrs + nPars <= 256 );
// collect CEC variables
Vec_IntForEachEntry( vDivSet, iVar, i )
pVarsCec[i] = iVar;
pVarsCec[nVars] = VarCecOut;
for ( i = 1; i < nStrs; i++ )
pVarsCec[nVars + i] = VarCecFree++;
for ( i = 0; i < nPars; i++ )
pVarsCec[nVars + nStrs + i] = VarCecPar + i;
// collect QBF variables
for ( i = 0; i < nVars + nStrs; i++ )
pVarsQbf[i] = -1;
for ( i = 0; i < nPars; i++ )
pVarsQbf[nVars + nStrs + i] = VarQbfPar + i;
// add clauses to the CEC problem
Sbd_ProblemAddClauses( pSatCec, nVars, nStrs, pVarsCec, pStr0 );
// create QBF solver
sat_solver_setnvars( pSatQbf, 1000 );
Sbd_ProblemAddClausesInit( pSatQbf, nVars, nStrs, pVarsQbf, pStr0 );
// assume all parameter variables are 0
Vec_IntClear( vLits );
for ( i = 0; i < nPars; i++ )
Vec_IntPush( vLits, Abc_Var2Lit(VarCecPar + i, 1) );
while ( 1 )
{
// check if these parameters solve the problem
int status = sat_solver_solve( pSatCec, Vec_IntArray(vLits), Vec_IntLimit(vLits), 0, 0, 0, 0 );
if ( status == l_False ) // solution found
break;
assert( status == l_True );
Vec_IntClear( vLits );
// create new QBF variables
for ( i = 0; i < nVars + nStrs; i++ )
pVarsQbf[i] = VarQbfFree++;
// set their values
Vec_IntForEachEntry( vDivSet, iVar, i )
{
iLit = Abc_Var2Lit( pVarsQbf[i], sat_solver_var_value(pSatCec, iVar) );
status = sat_solver_addclause( pSatQbf, &iLit, &iLit + 1 );
assert( status );
}
iLit = Abc_Var2Lit( pVarsQbf[nVars], sat_solver_var_value(pSatCec, VarCecOut) );
status = sat_solver_addclause( pSatQbf, &iLit, &iLit + 1 );
assert( status );
// add clauses to the QBF problem
Sbd_ProblemAddClauses( pSatQbf, nVars, nStrs, pVarsQbf, pStr0 );
// check if solution still exists
status = sat_solver_solve( pSatQbf, NULL, NULL, 0, 0, 0, 0 );
if ( status == l_False ) // solution does not exist
break;
assert( status == l_True );
// find the new values of parameters
assert( Vec_IntSize(vLits) == 0 );
for ( i = 0; i < nPars; i++ )
Vec_IntPush( vLits, Abc_Var2Lit(VarCecPar + i, sat_solver_var_value(pSatQbf, VarQbfPar + i)) );
}
if ( Vec_IntSize(vLits) > 0 )
{
Sbd_ProblemPrintSolution( nStrs, pStr0, vLits );
Sbd_ProblemCollectSolution( nStrs, pStr0, vLits, Truths );
RetValue = 1;
}
else
printf( "Solution does not exist.\n" );
sat_solver_delete( pSatCec );
sat_solver_delete( pSatQbf );
Vec_IntFree( vLits );
return RetValue;
}
////////////////////////////////////////////////////////////////////////
/// END OF FILE ///
////////////////////////////////////////////////////////////////////////
ABC_NAMESPACE_IMPL_END

4
src/opt/sbd/sbdSat.c
View File

@ -37,10 +37,6 @@ ABC_NAMESPACE_IMPL_START
/// FUNCTION DEFINITIONS ///
////////////////////////////////////////////////////////////////////////
#define SBD_LUTS_MAX 2
#define SBD_SIZE_MAX 4
#define SBD_DIV_MAX 16
// new AIG manager
typedef struct Sbd_Pro_t_ Sbd_Pro_t;
struct Sbd_Pro_t_

177
src/opt/sbd/sbdWin.c
View File

@ -39,19 +39,26 @@ ABC_NAMESPACE_IMPL_START
a DFS ordered array of objects (vWinObjs) whose indexed in the array
(which will be used as SAT variables) are given in array vObj2Var.
The TFO nodes are listed as the last ones in vWinObjs. The root nodes
are labeled with Abc_LitIsCompl() in vTfo and also given in vRoots.]
are labeled with Abc_LitIsCompl() in vTfo and also given in vRoots.
If fQbf is 1, returns the instance meant for QBF solving. It is using
the last variable (LastVar) as the placeholder for the second copy
of the pivot node.]
SideEffects []
SeeAlso []
***********************************************************************/
sat_solver * Sbd_ManSatSolver( sat_solver * pSat, Gia_Man_t * p, Vec_Int_t * vMirrors, int Pivot, Vec_Int_t * vWinObjs, Vec_Int_t * vObj2Var, Vec_Int_t * vTfo, Vec_Int_t * vRoots )
sat_solver * Sbd_ManSatSolver( sat_solver * pSat, Gia_Man_t * p, Vec_Int_t * vMirrors,
int Pivot, Vec_Int_t * vWinObjs, Vec_Int_t * vObj2Var,
Vec_Int_t * vTfo, Vec_Int_t * vRoots, int fQbf )
{
Gia_Obj_t * pObj;
int nAddVars = 64;
int i, iLit = 1, iObj, Fan0, Fan1, Lit0m, Lit1m, Node, fCompl0, fCompl1, RetValue;
int TfoStart = Vec_IntSize(vWinObjs) - Vec_IntSize(vTfo);
int PivotVar = Vec_IntEntry(vObj2Var, Pivot);
int LastVar = Vec_IntSize(vWinObjs) + Vec_IntSize(vTfo) + Vec_IntSize(vRoots);
//Vec_IntPrint( vWinObjs );
//Vec_IntPrint( vTfo );
//Vec_IntPrint( vRoots );
@ -60,7 +67,7 @@ sat_solver * Sbd_ManSatSolver( sat_solver * pSat, Gia_Man_t * p, Vec_Int_t * vMi
pSat = sat_solver_new();
else
sat_solver_restart( pSat );
sat_solver_setnvars( pSat, Vec_IntSize(vWinObjs) + Vec_IntSize(vTfo) + Vec_IntSize(vRoots) + 32 );
sat_solver_setnvars( pSat, Vec_IntSize(vWinObjs) + Vec_IntSize(vTfo) + Vec_IntSize(vRoots) + nAddVars );
// create constant 0 clause
sat_solver_addclause( pSat, &iLit, &iLit + 1 );
// add clauses for all nodes
@ -100,8 +107,13 @@ sat_solver * Sbd_ManSatSolver( sat_solver * pSat, Gia_Man_t * p, Vec_Int_t * vMi
Fan1 = Vec_IntEntry( vObj2Var, Fan1 );
Fan0 = Fan0 < TfoStart ? Fan0 : Fan0 + Vec_IntSize(vTfo);
Fan1 = Fan1 < TfoStart ? Fan1 : Fan1 + Vec_IntSize(vTfo);
fCompl0 = Gia_ObjFaninC0(pObj) ^ (Fan0 == PivotVar) ^ (Lit0m >= 0 && Abc_LitIsCompl(Lit0m));
fCompl1 = Gia_ObjFaninC1(pObj) ^ (Fan1 == PivotVar) ^ (Lit1m >= 0 && Abc_LitIsCompl(Lit1m));
if ( fQbf )
{
Fan0 = Fan0 == PivotVar ? LastVar : Fan0;
Fan1 = Fan1 == PivotVar ? LastVar : Fan1;
}
fCompl0 = Gia_ObjFaninC0(pObj) ^ (!fQbf && Fan0 == PivotVar) ^ (Lit0m >= 0 && Abc_LitIsCompl(Lit0m));
fCompl1 = Gia_ObjFaninC1(pObj) ^ (!fQbf && Fan1 == PivotVar) ^ (Lit1m >= 0 && Abc_LitIsCompl(Lit1m));
if ( Gia_ObjIsXor(pObj) )
sat_solver_add_xor( pSat, Node, Fan0, Fan1, fCompl0 ^ fCompl1 );
else
@ -127,7 +139,7 @@ sat_solver * Sbd_ManSatSolver( sat_solver * pSat, Gia_Man_t * p, Vec_Int_t * vMi
sat_solver_delete( pSat );
return NULL;
}
assert( sat_solver_nvars(pSat) == nVars + 32 );
assert( sat_solver_nvars(pSat) == nVars + nAddVars );
}
// finalize
RetValue = sat_solver_simplify( pSat );
@ -143,7 +155,7 @@ sat_solver * Sbd_ManSatSolver( sat_solver * pSat, Gia_Man_t * p, Vec_Int_t * vMi
Synopsis [Solves one SAT problem.]
Description [Computes node function for PivotVar with fanins in vDivVars
Description [Computes node function for PivotVar with fanins in vDivSet
using don't-care represented in the SAT solver. Uses array vValues to
return the values of the first Vec_IntSize(vValues) SAT variables in case
the implementation of the node with the given fanins does not exist.]
@ -153,12 +165,13 @@ sat_solver * Sbd_ManSatSolver( sat_solver * pSat, Gia_Man_t * p, Vec_Int_t * vMi
SeeAlso []
***********************************************************************/
word Sbd_ManSolve( sat_solver * pSat, int PivotVar, int FreeVar, Vec_Int_t * vDivVars, Vec_Int_t * vValues, Vec_Int_t * vTemp )
word Sbd_ManSolve( sat_solver * pSat, int PivotVar, int FreeVar, Vec_Int_t * vDivSet, Vec_Int_t * vDivVars, Vec_Int_t * vDivValues, Vec_Int_t * vTemp )
{
int nBTLimit = 0;
word uCube, uTruth = 0;
int status, i, iVar, nFinal, * pFinal, pLits[2], nIter = 0;
assert( FreeVar < sat_solver_nvars(pSat) );
assert( Vec_IntSize(vDivVars) == Vec_IntSize(vDivValues) );
pLits[0] = Abc_Var2Lit( PivotVar, 0 ); // F = 1
pLits[1] = Abc_Var2Lit( FreeVar, 0 ); // iNewLit
while ( 1 )
@ -171,12 +184,12 @@ word Sbd_ManSolve( sat_solver * pSat, int PivotVar, int FreeVar, Vec_Int_t * vDi
return uTruth;
assert( status == l_True );
// remember variable values
for ( i = 0; i < Vec_IntSize(vValues); i++ )
Vec_IntWriteEntry( vValues, i, 2*sat_solver_var_value(pSat, i) );
Vec_IntForEachEntry( vDivVars, iVar, i )
Vec_IntWriteEntry( vDivValues, i, 2*sat_solver_var_value(pSat, iVar) );
// collect divisor literals
Vec_IntClear( vTemp );
Vec_IntPush( vTemp, Abc_LitNot(pLits[0]) ); // F = 0
Vec_IntForEachEntry( vDivVars, iVar, i )
Vec_IntForEachEntry( vDivSet, iVar, i )
Vec_IntPush( vTemp, sat_solver_var_literal(pSat, iVar) );
// check against offset
status = sat_solver_solve( pSat, Vec_IntArray(vTemp), Vec_IntArray(vTemp) + Vec_IntSize(vTemp), nBTLimit, 0, 0, 0 );
@ -195,7 +208,7 @@ word Sbd_ManSolve( sat_solver * pSat, int PivotVar, int FreeVar, Vec_Int_t * vDi
if ( pFinal[i] == pLits[0] )
continue;
Vec_IntPush( vTemp, pFinal[i] );
iVar = Vec_IntFind( vDivVars, Abc_Lit2Var(pFinal[i]) ); assert( iVar >= 0 );
iVar = Vec_IntFind( vDivSet, Abc_Lit2Var(pFinal[i]) ); assert( iVar >= 0 );
uCube &= Abc_LitIsCompl(pFinal[i]) ? s_Truths6[iVar] : ~s_Truths6[iVar];
}
uTruth |= uCube;
@ -205,11 +218,11 @@ word Sbd_ManSolve( sat_solver * pSat, int PivotVar, int FreeVar, Vec_Int_t * vDi
}
assert( status == l_True );
// store the counter-example
for ( i = 0; i < Vec_IntSize(vValues); i++ )
Vec_IntAddToEntry( vValues, i, sat_solver_var_value(pSat, i) );
Vec_IntForEachEntry( vDivVars, iVar, i )
Vec_IntAddToEntry( vDivValues, i, sat_solver_var_value(pSat, iVar) );
for ( i = 0; i < Vec_IntSize(vValues); i++ )
Vec_IntAddToEntry( vValues, i, 0xC );
for ( i = 0; i < Vec_IntSize(vDivValues); i++ )
Vec_IntAddToEntry( vDivValues, i, 0xC );
/*
// reduce the counter example
for ( n = 0; n < 2; n++ )
@ -230,6 +243,138 @@ word Sbd_ManSolve( sat_solver * pSat, int PivotVar, int FreeVar, Vec_Int_t * vDi
return SBD_SAT_SAT;
}
/**Function*************************************************************
Synopsis []
Description []
SideEffects []
SeeAlso []
***********************************************************************/
int Sbd_ManSolve2( sat_solver * pSat, int PivotVar, int FreeVar, Vec_Int_t * vDivVars, Vec_Int_t * vDivValues, Vec_Int_t * vTemp, Vec_Int_t * vSop )
{
int nBTLimit = 0;
int status, i, iVar, nFinal, * pFinal, pLits[2], nIter = 0;
assert( FreeVar < sat_solver_nvars(pSat) );
assert( Vec_IntSize(vDivVars) == Vec_IntSize(vDivValues) );
pLits[0] = Abc_Var2Lit( PivotVar, 0 ); // F = 1
pLits[1] = Abc_Var2Lit( FreeVar, 0 ); // iNewLit
Vec_IntClear( vSop );
while ( 1 )
{
// find onset minterm
status = sat_solver_solve( pSat, pLits, pLits + 2, nBTLimit, 0, 0, 0 );
if ( status == l_Undef )
return 0;
if ( status == l_False )
return 1;
assert( status == l_True );
// remember variable values
//for ( i = 0; i < Vec_IntSize(vValues); i++ )
// Vec_IntWriteEntry( vValues, i, 2*sat_solver_var_value(pSat, i) );
// collect divisor literals
Vec_IntClear( vTemp );
Vec_IntPush( vTemp, Abc_LitNot(pLits[0]) ); // F = 0
//Vec_IntForEachEntry( vDivSet, iVar, i )
Vec_IntForEachEntry( vDivVars, iVar, i )
Vec_IntPush( vTemp, sat_solver_var_literal(pSat, iVar) );
// check against offset
status = sat_solver_solve( pSat, Vec_IntArray(vTemp), Vec_IntArray(vTemp) + Vec_IntSize(vTemp), nBTLimit, 0, 0, 0 );
if ( status == l_Undef )
return 0;
if ( status == l_True )
break;
assert( status == l_False );
// compute cube and add clause
nFinal = sat_solver_final( pSat, &pFinal );
Vec_IntClear( vTemp );
Vec_IntPush( vTemp, Abc_LitNot(pLits[1]) ); // NOT(iNewLit)
for ( i = 0; i < nFinal; i++ )
{
if ( pFinal[i] == pLits[0] )
continue;
Vec_IntPush( vTemp, pFinal[i] );
iVar = Vec_IntFind( vDivVars, Abc_Lit2Var(pFinal[i]) ); assert( iVar >= 0 );
//uCube &= Abc_LitIsCompl(pFinal[i]) ? s_Truths6[iVar] : ~s_Truths6[iVar];
Vec_IntPush( vSop, Abc_Var2Lit( iVar, !Abc_LitIsCompl(pFinal[i]) ) );
}
//uTruth |= uCube;
Vec_IntPush( vSop, -1 );
status = sat_solver_addclause( pSat, Vec_IntArray(vTemp), Vec_IntArray(vTemp) + Vec_IntSize(vTemp) );
assert( status );
nIter++;
}
assert( status == l_True );
// store the counter-example
//for ( i = 0; i < Vec_IntSize(vValues); i++ )
// Vec_IntAddToEntry( vValues, i, sat_solver_var_value(pSat, i) );
return 0;
}
word Sbd_ManSolverSupp( Vec_Int_t * vSop, int * pInds, int * pnVars )
{
word Supp = 0;
int i, Entry, nVars = 0;
Vec_IntForEachEntry( vSop, Entry, i )
{
if ( Entry == -1 )
continue;
assert( Abc_Lit2Var(Entry) < 64 );
if ( (Supp >> Abc_Lit2Var(Entry)) & 1 )
continue;
pInds[Abc_Lit2Var(Entry)] = nVars++;
Supp |= (word)1 << Abc_Lit2Var(Entry);
}
*pnVars = nVars;
return Supp;
}
void Sbd_ManSolverPrint( Vec_Int_t * vSop )
{
int v, i, Entry, nVars, pInds[64];
word Supp = Sbd_ManSolverSupp( vSop, pInds, &nVars );
char Cube[65] = {'\0'};
assert( Cube[nVars] == '\0' );
for ( v = 0; v < nVars; v++ )
Cube[v] = '-';
Vec_IntForEachEntry( vSop, Entry, i )
{
if ( Entry == -1 )
{
printf( "%s\n", Cube );
for ( v = 0; v < nVars; v++ )
Cube[v] = '-';
continue;
}
Cube[pInds[Abc_Lit2Var(Entry)]] = '1' - (char)Abc_LitIsCompl(Entry);
}
}
void Sbd_ManSolveSelect( Gia_Man_t * p, Vec_Int_t * vMirrors, int Pivot, Vec_Int_t * vDivVars, Vec_Int_t * vDivValues, Vec_Int_t * vWinObjs, Vec_Int_t * vObj2Var, Vec_Int_t * vTfo, Vec_Int_t * vRoots )
{
Vec_Int_t * vSop = Vec_IntAlloc( 100 );
Vec_Int_t * vTemp = Vec_IntAlloc( 100 );
sat_solver * pSat = Sbd_ManSatSolver( NULL, p, vMirrors, Pivot, vWinObjs, vObj2Var, vTfo, vRoots, 0 );
int PivotVar = Vec_IntEntry(vObj2Var, Pivot);
int FreeVar = Vec_IntSize(vWinObjs) + Vec_IntSize(vTfo) + Vec_IntSize(vRoots);
int Status = Sbd_ManSolve2( pSat, PivotVar, FreeVar, vDivVars, vDivValues, vTemp, vSop );
printf( "Pivot = %4d. Divs = %4d. ", Pivot, Vec_IntSize(vDivVars) );
if ( Status == 0 )
printf( "UNSAT.\n" );
else
{
int nVars, pInds[64];
word Supp = Sbd_ManSolverSupp( vSop, pInds, &nVars );
//Sbd_ManSolverPrint( vSop );
printf( "SAT with %d vars and %d cubes.\n", nVars, Vec_IntCountEntry(vSop, -1) );
}
Vec_IntFree( vTemp );
Vec_IntFree( vSop );
sat_solver_delete( pSat );
}
/**Function*************************************************************
Synopsis [Returns a bunch of positive/negative random care minterms.]