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

Version abc80202

This commit is contained in:
Alan Mishchenko 2008-02-02 08:01:00 -08:00
parent 0c6505a26a
commit 3b790eb17e
38 changed files with 2305 additions and 178 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

2
Makefile
View File

@ -13,7 +13,7 @@ MODULES := src/base/abc src/base/abci src/base/cmd \
src/map/fpga src/map/mapper src/map/mio src/map/super src/map/if \
src/misc/extra src/misc/mvc src/misc/st src/misc/util \
src/misc/espresso src/misc/nm src/misc/vec src/misc/hash \
src/opt/cut src/opt/dec src/opt/fxu src/opt/rwr \
src/opt/cut src/opt/dec src/opt/fxu src/opt/rwr src/opt/mfs \
src/opt/sim src/opt/ret src/opt/res src/opt/lpk src/opt/fret \
src/sat/bsat src/sat/csat src/sat/msat src/sat/fraig \
src/aig/ivy src/aig/hop src/aig/rwt src/aig/deco \

44
abc.dsp
View File

@ -42,7 +42,7 @@ RSC=rc.exe
# PROP Ignore_Export_Lib 0
# PROP Target_Dir ""
# ADD BASE CPP /nologo /W3 /GX /O2 /D "WIN32" /D "NDEBUG" /D "_CONSOLE" /D "_MBCS" /YX /FD /c
# ADD CPP /nologo /W3 /GX /O2 /I "src/base/abc" /I "src/base/abci" /I "src/base/cmd" /I "src/base/io" /I "src/base/main" /I "src/base/ver" /I "src/bdd/cudd" /I "src/bdd/dsd" /I "src/bdd/epd" /I "src/bdd/mtr" /I "src/bdd/parse" /I "src/bdd/reo" /I "src/bdd/cas" /I "src/map/fpga" /I "src/map/mapper" /I "src/map/mio" /I "src/map/super" /I "src/map/if" /I "src/map/pcm" /I "src/map/ply" /I "src/misc/extra" /I "src/misc/mvc" /I "src/misc/st" /I "src/misc/util" /I "src/misc/espresso" /I "src/misc/nm" /I "src/misc/vec" /I "src/misc/hash" /I "src/opt/cut" /I "src/opt/dec" /I "src/opt/fxu" /I "src/opt/rwr" /I "src/opt/sim" /I "src/opt/ret" /I "src/opt/res" /I "src/opt/lpk" /I "src/sat/bsat" /I "src/sat/csat" /I "src/sat/msat" /I "src/sat/fraig" /I "src/aig/ivy" /I "src/aig/hop" /I "src/aig/rwt" /I "src/aig/deco" /I "src/aig/mem" /I "src/aig/dar" /I "src/aig/fra" /I "src/aig/cnf" /I "src/aig/csw" /I "src/aig/ioa" /I "src/aig/aig" /I "src/aig/kit" /I "src/aig/bdc" /I "src/aig/bar" /I "src/aig/ntl" /I "src/aig/tim" /D "WIN32" /D "NDEBUG" /D "_CONSOLE" /D "_MBCS" /D "__STDC__" /FR /YX /FD /c
# ADD CPP /nologo /W3 /GX /O2 /I "src/base/abc" /I "src/base/abci" /I "src/base/cmd" /I "src/base/io" /I "src/base/main" /I "src/base/ver" /I "src/bdd/cudd" /I "src/bdd/dsd" /I "src/bdd/epd" /I "src/bdd/mtr" /I "src/bdd/parse" /I "src/bdd/reo" /I "src/bdd/cas" /I "src/map/fpga" /I "src/map/mapper" /I "src/map/mio" /I "src/map/super" /I "src/map/if" /I "src/map/pcm" /I "src/map/ply" /I "src/misc/extra" /I "src/misc/mvc" /I "src/misc/st" /I "src/misc/util" /I "src/misc/espresso" /I "src/misc/nm" /I "src/misc/vec" /I "src/misc/hash" /I "src/opt/cut" /I "src/opt/dec" /I "src/opt/fxu" /I "src/opt/rwr" /I "src/opt/sim" /I "src/opt/ret" /I "src/opt/res" /I "src/opt/lpk" /I "src/sat/bsat" /I "src/sat/csat" /I "src/sat/msat" /I "src/sat/fraig" /I "src/aig/ivy" /I "src/aig/hop" /I "src/aig/rwt" /I "src/aig/deco" /I "src/aig/mem" /I "src/aig/dar" /I "src/aig/fra" /I "src/aig/cnf" /I "src/aig/csw" /I "src/aig/ioa" /I "src/aig/aig" /I "src/aig/kit" /I "src/aig/bdc" /I "src/aig/bar" /I "src/aig/ntl" /I "src/aig/tim" /I "src/opt/mfs" /D "WIN32" /D "NDEBUG" /D "_CONSOLE" /D "_MBCS" /D "__STDC__" /FR /YX /FD /c
# ADD BASE RSC /l 0x409 /d "NDEBUG"
# ADD RSC /l 0x409 /d "NDEBUG"
BSC32=bscmake.exe
@ -66,7 +66,7 @@ LINK32=link.exe
# PROP Ignore_Export_Lib 0
# PROP Target_Dir ""
# ADD BASE CPP /nologo /W3 /Gm /GX /ZI /Od /D "WIN32" /D "_DEBUG" /D "_CONSOLE" /D "_MBCS" /YX /FD /GZ /c
# ADD CPP /nologo /W3 /Gm /GX /ZI /Od /I "src/base/abc" /I "src/base/abci" /I "src/base/cmd" /I "src/base/io" /I "src/base/main" /I "src/base/ver" /I "src/bdd/cudd" /I "src/bdd/dsd" /I "src/bdd/epd" /I "src/bdd/mtr" /I "src/bdd/parse" /I "src/bdd/reo" /I "src/bdd/cas" /I "src/map/fpga" /I "src/map/mapper" /I "src/map/mio" /I "src/map/super" /I "src/map/if" /I "src/map/pcm" /I "src/map/ply" /I "src/misc/extra" /I "src/misc/mvc" /I "src/misc/st" /I "src/misc/util" /I "src/misc/espresso" /I "src/misc/nm" /I "src/misc/vec" /I "src/misc/hash" /I "src/opt/cut" /I "src/opt/dec" /I "src/opt/fxu" /I "src/opt/rwr" /I "src/opt/sim" /I "src/opt/ret" /I "src/opt/res" /I "src/opt/lpk" /I "src/sat/bsat" /I "src/sat/csat" /I "src/sat/msat" /I "src/sat/fraig" /I "src/aig/ivy" /I "src/aig/hop" /I "src/aig/rwt" /I "src/aig/deco" /I "src/aig/mem" /I "src/aig/dar" /I "src/aig/fra" /I "src/aig/cnf" /I "src/aig/csw" /I "src/aig/ioa" /I "src/aig/aig" /I "src/aig/kit" /I "src/aig/bdc" /I "src/aig/bar" /I "src/aig/ntl" /I "src/aig/tim" /D "WIN32" /D "_DEBUG" /D "_CONSOLE" /D "_MBCS" /D "__STDC__" /FR /YX /FD /GZ /c
# ADD CPP /nologo /W3 /Gm /GX /ZI /Od /I "src/base/abc" /I "src/base/abci" /I "src/base/cmd" /I "src/base/io" /I "src/base/main" /I "src/base/ver" /I "src/bdd/cudd" /I "src/bdd/dsd" /I "src/bdd/epd" /I "src/bdd/mtr" /I "src/bdd/parse" /I "src/bdd/reo" /I "src/bdd/cas" /I "src/map/fpga" /I "src/map/mapper" /I "src/map/mio" /I "src/map/super" /I "src/map/if" /I "src/map/pcm" /I "src/map/ply" /I "src/misc/extra" /I "src/misc/mvc" /I "src/misc/st" /I "src/misc/util" /I "src/misc/espresso" /I "src/misc/nm" /I "src/misc/vec" /I "src/misc/hash" /I "src/opt/cut" /I "src/opt/dec" /I "src/opt/fxu" /I "src/opt/rwr" /I "src/opt/sim" /I "src/opt/ret" /I "src/opt/res" /I "src/opt/lpk" /I "src/sat/bsat" /I "src/sat/csat" /I "src/sat/msat" /I "src/sat/fraig" /I "src/aig/ivy" /I "src/aig/hop" /I "src/aig/rwt" /I "src/aig/deco" /I "src/aig/mem" /I "src/aig/dar" /I "src/aig/fra" /I "src/aig/cnf" /I "src/aig/csw" /I "src/aig/ioa" /I "src/aig/aig" /I "src/aig/kit" /I "src/aig/bdc" /I "src/aig/bar" /I "src/aig/ntl" /I "src/aig/tim" /I "src/opt/mfs" /D "WIN32" /D "_DEBUG" /D "_CONSOLE" /D "_MBCS" /D "__STDC__" /FR /YX /FD /GZ /c
# SUBTRACT CPP /X
# ADD BASE RSC /l 0x409 /d "_DEBUG"
# ADD RSC /l 0x409 /d "_DEBUG"
@ -1613,6 +1613,38 @@ SOURCE=.\src\opt\fret\fretMain.c
SOURCE=.\src\opt\fret\fretTime.c
# End Source File
# End Group
# Begin Group "mfs"
# PROP Default_Filter ""
# Begin Source File
SOURCE=.\src\opt\mfs\mfs.h
# End Source File
# Begin Source File
SOURCE=.\src\opt\mfs\mfsCore.c
# End Source File
# Begin Source File
SOURCE=.\src\opt\mfs\mfsInt.h
# End Source File
# Begin Source File
SOURCE=.\src\opt\mfs\mfsMan.c
# End Source File
# Begin Source File
SOURCE=.\src\opt\mfs\mfsSat.c
# End Source File
# Begin Source File
SOURCE=.\src\opt\mfs\mfsStrash.c
# End Source File
# Begin Source File
SOURCE=.\src\opt\mfs\mfsWin.c
# End Source File
# End Group
# End Group
# Begin Group "map"
@ -2666,6 +2698,10 @@ SOURCE=.\src\aig\fra\fraCore.c
# End Source File
# Begin Source File
SOURCE=.\src\aig\fra\fraHot.c
# End Source File
# Begin Source File
SOURCE=.\src\aig\fra\fraImp.c
# End Source File
# Begin Source File
@ -2674,6 +2710,10 @@ SOURCE=.\src\aig\fra\fraInd.c
# End Source File
# Begin Source File
SOURCE=.\src\aig\fra\fraIndVer.c
# End Source File
# Begin Source File
SOURCE=.\src\aig\fra\fraLcr.c
# End Source File
# Begin Source File

1
abc.rc
View File

@ -36,6 +36,7 @@ alias pex print_exdc -d
alias pf print_factor
alias pfan print_fanio
alias pl print_level
alias plat print_latch
alias pio print_io
alias pk print_kmap
alias ps print_stats

3
src/aig/aig/aig.h
View File

@ -142,6 +142,7 @@ struct Aig_Man_t_
Vec_Int_t * vFlopNums;
void * pSeqModel;
Aig_Man_t * pManHaig;
Aig_Man_t * pManExdc;
// timing statistics
int time1;
int time2;
@ -210,6 +211,7 @@ static inline Aig_Cut_t * Aig_CutNext( Aig_Cut_t * pCut ) { return
#define PRT(a,t) printf("%s = ", (a)); printf("%6.2f sec\n", (float)(t)/(float)(CLOCKS_PER_SEC))
#endif
static inline int Aig_IntAbs( int n ) { return (n < 0)? -n : n; }
static inline int Aig_Float2Int( float Val ) { return *((int *)&Val); }
static inline float Aig_Int2Float( int Num ) { return *((float *)&Num); }
static inline int Aig_Base2Log( unsigned n ) { int r; assert( n >= 0 ); if ( n < 2 ) return n; for ( r = 0, n--; n; n >>= 1, r++ ); return r; }
@ -536,6 +538,7 @@ extern Aig_Man_t * Aig_ManRemap( Aig_Man_t * p, Vec_Ptr_t * vMap );
extern int Aig_ManSeqCleanup( Aig_Man_t * p );
extern int Aig_ManCountMergeRegs( Aig_Man_t * p );
extern Aig_Man_t * Aig_ManReduceLaches( Aig_Man_t * p, int fVerbose );
extern void Aig_ManComputeSccs( Aig_Man_t * p );
/*=== aigSeq.c ========================================================*/
extern int Aig_ManSeqStrash( Aig_Man_t * p, int nLatches, int * pInits );
/*=== aigShow.c ========================================================*/

1
src/aig/aig/aigMan.c
View File

@ -294,6 +294,7 @@ void Aig_ManStop( Aig_Man_t * p )
if ( p->vLevelR ) Vec_IntFree( p->vLevelR );
if ( p->vLevels ) Vec_VecFree( p->vLevels );
if ( p->vFlopNums) Vec_IntFree( p->vFlopNums );
if ( p->pManExdc ) Aig_ManStop( p->pManExdc );
FREE( p->pSeqModel );
FREE( p->pName );
FREE( p->pObjCopies );

5
src/aig/aig/aigPart.c
View File

@ -257,9 +257,10 @@ Vec_Int_t * Part_ManTransferEntry( Part_One_t * p )
Synopsis [Computes supports of the POs in the multi-output AIG.]
Description []
Description [Returns the array of integer arrays containing indices
of the primary inputs.]
SideEffects []
SideEffects [Adds the integer PO number at end of each array.]
SeeAlso []

109
src/aig/aig/aigScl.c
View File

@ -391,6 +391,115 @@ Aig_Man_t * Aig_ManReduceLaches( Aig_Man_t * p, int fVerbose )
return p;
}
/**Function*************************************************************
Synopsis [Computes strongly connected components of registers.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
void Aig_ManComputeSccs( Aig_Man_t * p )
{
Vec_Ptr_t * vSupports, * vMatrix, * vMatrix2;
Vec_Int_t * vSupp, * vSupp2, * vComp;
char * pVarsTot;
int i, k, m, iOut, iIn, nComps;
if ( Aig_ManRegNum(p) == 0 )
{
printf( "The network is combinational.\n" );
return;
}
// get structural supports for each output
vSupports = Aig_ManSupports( p );
// transforms the supports into the latch dependency matrix
vMatrix = Vec_PtrStart( Aig_ManRegNum(p) );
Vec_PtrForEachEntry( vSupports, vSupp, i )
{
// skip true POs
iOut = Vec_IntPop( vSupp );
iOut -= Aig_ManPoNum(p) - Aig_ManRegNum(p);
if ( iOut < 0 )
continue;
// remove PIs
m = 0;
Vec_IntForEachEntry( vSupp, iIn, k )
{
iIn -= Aig_ManPiNum(p) - Aig_ManRegNum(p);
if ( iIn < 0 )
continue;
assert( iIn < Aig_ManRegNum(p) );
Vec_IntWriteEntry( vSupp, m++, iIn );
}
Vec_IntShrink( vSupp, m );
// store support in the matrix
assert( iOut < Aig_ManRegNum(p) );
Vec_PtrWriteEntry( vMatrix, iOut, vSupp );
}
// create the reverse matrix
vMatrix2 = Vec_PtrAlloc( Aig_ManRegNum(p) );
for ( i = 0; i < Aig_ManRegNum(p); i++ )
Vec_PtrPush( vMatrix2, Vec_IntAlloc(8) );
Vec_PtrForEachEntry( vMatrix, vSupp, i )
{
Vec_IntForEachEntry( vSupp, iIn, k )
{
vSupp2 = Vec_PtrEntry( vMatrix2, iIn );
Vec_IntPush( vSupp2, i );
}
}
// detect strongly connected components
vComp = Vec_IntAlloc( Aig_ManRegNum(p) );
pVarsTot = ALLOC( char, Aig_ManRegNum(p) );
memset( pVarsTot, 0, Aig_ManRegNum(p) * sizeof(char) );
for ( nComps = 0; ; nComps++ )
{
Vec_IntClear( vComp );
// get the first support
for ( iOut = 0; iOut < Aig_ManRegNum(p); iOut++ )
if ( pVarsTot[iOut] == 0 )
break;
if ( iOut == Aig_ManRegNum(p) )
break;
pVarsTot[iOut] = 1;
Vec_IntPush( vComp, iOut );
Vec_IntForEachEntry( vComp, iOut, i )
{
vSupp = Vec_PtrEntry( vMatrix, iOut );
Vec_IntForEachEntry( vSupp, iIn, k )
{
if ( pVarsTot[iIn] )
continue;
pVarsTot[iIn] = 1;
Vec_IntPush( vComp, iIn );
}
vSupp2 = Vec_PtrEntry( vMatrix2, iOut );
Vec_IntForEachEntry( vSupp2, iIn, k )
{
if ( pVarsTot[iIn] )
continue;
pVarsTot[iIn] = 1;
Vec_IntPush( vComp, iIn );
}
}
if ( Vec_IntSize(vComp) == Aig_ManRegNum(p) )
{
printf( "There is only one SCC of registers in this network.\n" );
break;
}
printf( "SCC #%d contains %5d registers.\n", nComps+1, Vec_IntSize(vComp) );
}
free( pVarsTot );
Vec_IntFree( vComp );
Vec_PtrFree( vMatrix );
Vec_VecFree( (Vec_Vec_t *)vMatrix2 );
Vec_VecFree( (Vec_Vec_t *)vSupports );
}
////////////////////////////////////////////////////////////////////////
/// END OF FILE ///

2
src/aig/cnf/cnf.h
View File

@ -132,6 +132,8 @@ extern void Cnf_ReadMsops( char ** ppSopSizes, char *** ppSops );
extern Cnf_Man_t * Cnf_ManStart();
extern void Cnf_ManStop( Cnf_Man_t * p );
extern Vec_Int_t * Cnf_DataCollectPiSatNums( Cnf_Dat_t * pCnf, Aig_Man_t * p );
extern Cnf_Dat_t * Cnf_DataAlloc( Aig_Man_t * pAig, int nVars, int nClauses, int nLiterals );
extern Cnf_Dat_t * Cnf_DataDup( Cnf_Dat_t * p );
extern void Cnf_DataFree( Cnf_Dat_t * p );
extern void Cnf_DataLift( Cnf_Dat_t * p, int nVarsPlus );
extern void Cnf_DataWriteIntoFile( Cnf_Dat_t * p, char * pFileName, int fReadable );

51
src/aig/cnf/cnfMan.c
View File

@ -107,6 +107,57 @@ Vec_Int_t * Cnf_DataCollectPiSatNums( Cnf_Dat_t * pCnf, Aig_Man_t * p )
return vCiIds;
}
/**Function*************************************************************
Synopsis [Allocates the new CNF.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
Cnf_Dat_t * Cnf_DataAlloc( Aig_Man_t * pAig, int nVars, int nClauses, int nLiterals )
{
Cnf_Dat_t * pCnf;
pCnf = ALLOC( Cnf_Dat_t, 1 );
memset( pCnf, 0, sizeof(Cnf_Dat_t) );
pCnf->pMan = pAig;
pCnf->nVars = nVars;
pCnf->nClauses = nClauses;
pCnf->nLiterals = nLiterals;
pCnf->pClauses = ALLOC( int *, nClauses + 1 );
pCnf->pClauses[0] = ALLOC( int, nLiterals );
pCnf->pClauses[nClauses] = pCnf->pClauses[0] + nLiterals;
pCnf->pVarNums = ALLOC( int, Aig_ManObjNumMax(pAig) );
memset( pCnf->pVarNums, 0xff, sizeof(int) * Aig_ManObjNumMax(pAig) );
return pCnf;
}
/**Function*************************************************************
Synopsis [Allocates the new CNF.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
Cnf_Dat_t * Cnf_DataDup( Cnf_Dat_t * p )
{
Cnf_Dat_t * pCnf;
int i;
pCnf = Cnf_DataAlloc( p->pMan, p->nVars, p->nClauses, p->nLiterals );
memcpy( pCnf->pClauses[0], p->pClauses[0], sizeof(int) * p->nLiterals );
memcpy( pCnf->pVarNums, p->pVarNums, sizeof(int) * Aig_ManObjNumMax(p->pMan) );
for ( i = 1; i < p->nClauses; i++ )
pCnf->pClauses[i] = pCnf->pClauses[0] + (p->pClauses[i] - p->pClauses[0]);
return pCnf;
}
/**Function*************************************************************
Synopsis []

16
src/aig/fra/fra.h
View File

@ -80,6 +80,7 @@ struct Fra_Par_t_
int fRewrite; // use rewriting for constraint reduction
int fLatchCorr; // computes latch correspondence only
int fUseImps; // use implications
int fUse1Hot; // use one-hotness conditions
int fWriteImps; // record implications
int fDontShowBar; // does not show progressbar during fraiging
};
@ -153,6 +154,8 @@ struct Fra_Man_t_
int nPatWords; // the number of words in the counter example
unsigned * pPatWords; // the counter example
Vec_Int_t * vCex;
// one-hotness conditions
Vec_Int_t * vOneHots;
// satisfiability solving
sat_solver * pSat; // SAT solver
int nSatVars; // the number of variables currently used
@ -265,6 +268,14 @@ extern int Fra_FraigMiterAssertedOutput( Aig_Man_t * p );
extern Aig_Man_t * Fra_FraigPerform( Aig_Man_t * pManAig, Fra_Par_t * pPars );
extern Aig_Man_t * Fra_FraigChoice( Aig_Man_t * pManAig, int nConfMax );
extern Aig_Man_t * Fra_FraigEquivence( Aig_Man_t * pManAig, int nConfMax, int fProve );
/*=== fraHot.c ========================================================*/
extern Vec_Int_t * Fra_OneHotCompute( Fra_Man_t * p, Fra_Sml_t * pSim );
extern void Fra_OneHotAssume( Fra_Man_t * p, Vec_Int_t * vOneHots );
extern void Fra_OneHotCheck( Fra_Man_t * p, Vec_Int_t * vOneHots );
extern int Fra_OneHotRefineUsingCex( Fra_Man_t * p, Vec_Int_t * vOneHots );
extern int Fra_OneHotCount( Fra_Man_t * p, Vec_Int_t * vOneHots );
extern void Fra_OneHotEstimateCoverage( Fra_Man_t * p, Vec_Int_t * vOneHots );
extern Aig_Man_t * Fra_OneHotCreateExdc( Fra_Man_t * p, Vec_Int_t * vOneHots );
/*=== fraImp.c ========================================================*/
extern Vec_Int_t * Fra_ImpDerive( Fra_Man_t * p, int nImpMaxLimit, int nImpUseLimit, int fLatchCorr );
extern void Fra_ImpAddToSolver( Fra_Man_t * p, Vec_Int_t * vImps, int * pSatVarNums );
@ -275,7 +286,9 @@ extern double Fra_ImpComputeStateSpaceRatio( Fra_Man_t * p );
extern int Fra_ImpVerifyUsingSimulation( Fra_Man_t * p );
extern void Fra_ImpRecordInManager( Fra_Man_t * p, Aig_Man_t * pNew );
/*=== fraInd.c ========================================================*/
extern Aig_Man_t * Fra_FraigInduction( Aig_Man_t * p, int nFramesP, int nFramesK, int nMaxImps, int nMaxLevs, int fRewrite, int fUseImps, int fLatchCorr, int fWriteImps, int fVerbose, int * pnIter );
extern Aig_Man_t * Fra_FraigInduction( Aig_Man_t * p, int nFramesP, int nFramesK, int nMaxImps, int nMaxLevs, int fRewrite, int fUseImps, int fLatchCorr, int fWriteImps, int fUse1Hot, int fVerbose, int * pnIter );
/*=== fraIndVer.c =====================================================*/
extern int Fra_InvariantVerify( Aig_Man_t * p, int nFrames, Vec_Int_t * vClauses, Vec_Int_t * vLits );
/*=== fraLcr.c ========================================================*/
extern Aig_Man_t * Fra_FraigLatchCorrespondence( Aig_Man_t * pAig, int nFramesP, int nConfMax, int fProve, int fVerbose, int * pnIter );
/*=== fraMan.c ========================================================*/
@ -290,6 +303,7 @@ extern void Fra_ManPrint( Fra_Man_t * p );
/*=== fraSat.c ========================================================*/
extern int Fra_NodesAreEquiv( Fra_Man_t * p, Aig_Obj_t * pOld, Aig_Obj_t * pNew );
extern int Fra_NodesAreImp( Fra_Man_t * p, Aig_Obj_t * pOld, Aig_Obj_t * pNew, int fComplL, int fComplR );
extern int Fra_NodesAreClause( Fra_Man_t * p, Aig_Obj_t * pOld, Aig_Obj_t * pNew, int fComplL, int fComplR );
extern int Fra_NodeIsConst( Fra_Man_t * p, Aig_Obj_t * pNew );
/*=== fraSec.c ========================================================*/
extern int Fra_FraigSec( Aig_Man_t * p, int nFrames, int fRetimeFirst, int fVerbose, int fVeryVerbose );

37
src/aig/fra/fraClaus.c
View File

@ -67,7 +67,6 @@ struct Clu_Man_t_
// clauses proven
Vec_Int_t * vLitsProven;
Vec_Int_t * vClausesProven;
int nClausesProven;
// counter-examples
Vec_Ptr_t * vCexes;
int nCexes;
@ -516,6 +515,21 @@ int Fra_ClausCollectLatchClauses( Clu_Man_t * p, Fra_Sml_t * pSeq )
nCountConst = nCountImps = 0;
CostMax = p->nSimWords * 32;
// add the property
{
Aig_Obj_t * pObj;
int Lits[1];
pObj = Aig_ManPo( p->pAig, 0 );
Lits[0] = toLitCond( p->pCnf->pVarNums[pObj->Id], 1 );
Vec_IntPush( p->vLits, Lits[0] );
Vec_IntPush( p->vClauses, Vec_IntSize(p->vLits) );
Vec_IntPush( p->vCosts, CostMax );
nCountConst++;
// printf( "Added the target property to the set of clauses to be inductively checked.\n" );
}
pSeq->nWordsPref = p->nSimWordsPref;
Aig_ManForEachLoSeq( p->pAig, pObj1, i )
{
@ -1600,11 +1614,11 @@ if ( p->fVerbose )
clk = clock();
// derive CNF
if ( p->fTarget )
p->pAig->nRegs++;
// if ( p->fTarget )
// p->pAig->nRegs++;
p->pCnf = Cnf_DeriveSimple( p->pAig, Aig_ManPoNum(p->pAig) );
if ( p->fTarget )
p->pAig->nRegs--;
// if ( p->fTarget )
// p->pAig->nRegs--;
if ( fVerbose )
{
//PRT( "CNF ", clock() - clk );
@ -1705,6 +1719,9 @@ clk = clock();
}
clk = clock();
}
// add proved clauses to storage
Fra_ClausAddToStorage( p );
// report the results
if ( p->fTarget )
{
if ( Counter == -1 )
@ -1722,12 +1739,14 @@ clk = clock();
printf( "Finished proving inductive clauses. " );
PRT( "Time ", clock() - clkTotal );
}
// add proved clauses to storage
Fra_ClausAddToStorage( p );
}
if ( !p->fTarget && p->fVerbose )
// verify the computed interpolant
Fra_InvariantVerify( pAig, nFrames, p->vClausesProven, p->vLitsProven );
// printf( "THIS COMMAND IS KNOWN TO HAVE A BUG!\n" );
// if ( !p->fTarget && p->fVerbose )
if ( p->fVerbose )
{
Fra_ClausPrintIndClauses( p );
Fra_ClausEstimateCoverage( p );

1
src/aig/fra/fraCore.c
View File

@ -378,6 +378,7 @@ clk = clock();
// call back the procedure to check implications
if ( pManAig->pImpFunc )
pManAig->pImpFunc( p, pManAig->pImpData );
// no need to filter one-hot clauses because they satisfy base case by construction
// finalize the fraiged manager
Fra_ManFinalizeComb( p );
if ( p->pPars->fChoicing )

424
src/aig/fra/fraHot.c Normal file
View File

@ -0,0 +1,424 @@
/**CFile****************************************************************
FileName [fraHot.c]
SystemName [ABC: Logic synthesis and verification system.]
PackageName [New FRAIG package.]
Synopsis [Computing and using one-hotness conditions.]
Author [Alan Mishchenko]
Affiliation [UC Berkeley]
Date [Ver. 1.0. Started - June 30, 2007.]
Revision [$Id: fraHot.c,v 1.00 2007/06/30 00:00:00 alanmi Exp $]
***********************************************************************/
#include "fra.h"
////////////////////////////////////////////////////////////////////////
/// DECLARATIONS ///
////////////////////////////////////////////////////////////////////////
static inline int Fra_RegToLit( int n, int c ) { return c? -n-1 : n+1; }
static inline int Fra_LitReg( int n ) { return (n>0)? n-1 : -n-1; }
static inline int Fra_LitSign( int n ) { return (n<0); }
////////////////////////////////////////////////////////////////////////
/// FUNCTION DEFINITIONS ///
////////////////////////////////////////////////////////////////////////
/**Function*************************************************************
Synopsis [Returns 1 if simulation info is composed of all zeros.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
int Fra_OneHotNodeIsConst( Fra_Sml_t * pSeq, Aig_Obj_t * pObj )
{
unsigned * pSims;
int i;
pSims = Fra_ObjSim(pSeq, pObj->Id);
for ( i = pSeq->nWordsPref; i < pSeq->nWordsTotal; i++ )
if ( pSims[i] )
return 0;
return 1;
}
/**Function*************************************************************
Synopsis [Returns 1 if simulation infos are equal.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
int Fra_OneHotNodesAreEqual( Fra_Sml_t * pSeq, Aig_Obj_t * pObj0, Aig_Obj_t * pObj1 )
{
unsigned * pSims0, * pSims1;
int i;
pSims0 = Fra_ObjSim(pSeq, pObj0->Id);
pSims1 = Fra_ObjSim(pSeq, pObj1->Id);
for ( i = pSeq->nWordsPref; i < pSeq->nWordsTotal; i++ )
if ( pSims0[i] != pSims1[i] )
return 0;
return 1;
}
/**Function*************************************************************
Synopsis [Returns 1 if implications holds.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
int Fra_OneHotNodesAreClause( Fra_Sml_t * pSeq, Aig_Obj_t * pObj1, Aig_Obj_t * pObj2, int fCompl1, int fCompl2 )
{
unsigned * pSim1, * pSim2;
int k;
pSim1 = Fra_ObjSim(pSeq, pObj1->Id);
pSim2 = Fra_ObjSim(pSeq, pObj2->Id);
if ( fCompl1 && fCompl2 )
{
for ( k = pSeq->nWordsPref; k < pSeq->nWordsTotal; k++ )
if ( pSim1[k] & pSim2[k] )
return 0;
}
else if ( fCompl1 )
{
for ( k = pSeq->nWordsPref; k < pSeq->nWordsTotal; k++ )
if ( pSim1[k] & ~pSim2[k] )
return 0;
}
else if ( fCompl2 )
{
for ( k = pSeq->nWordsPref; k < pSeq->nWordsTotal; k++ )
if ( ~pSim1[k] & pSim2[k] )
return 0;
}
else
assert( 0 );
return 1;
}
/**Function*************************************************************
Synopsis [Computes one-hot implications.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
Vec_Int_t * Fra_OneHotCompute( Fra_Man_t * p, Fra_Sml_t * pSim )
{
int fSkipConstEqu = 1;
Vec_Int_t * vOneHots;
Aig_Obj_t * pObj1, * pObj2;
int i, k;
int nTruePis = Aig_ManPiNum(pSim->pAig) - Aig_ManRegNum(pSim->pAig);
assert( pSim->pAig == p->pManAig );
vOneHots = Vec_IntAlloc( 100 );
Aig_ManForEachLoSeq( pSim->pAig, pObj1, i )
{
if ( fSkipConstEqu && Fra_OneHotNodeIsConst(pSim, pObj1) )
continue;
assert( i-nTruePis >= 0 );
// Aig_ManForEachLoSeq( pSim->pAig, pObj2, k )
// Vec_PtrForEachEntryStart( pSim->pAig->vPis, pObj2, k, Aig_ManPiNum(p)-Aig_ManRegNum(p) )
Vec_PtrForEachEntryStart( pSim->pAig->vPis, pObj2, k, i+1 )
{
if ( fSkipConstEqu && Fra_OneHotNodeIsConst(pSim, pObj2) )
continue;
if ( fSkipConstEqu && Fra_OneHotNodesAreEqual( pSim, pObj1, pObj2 ) )
continue;
assert( k-nTruePis >= 0 );
if ( Fra_OneHotNodesAreClause( pSim, pObj1, pObj2, 1, 1 ) )
{
Vec_IntPush( vOneHots, Fra_RegToLit(i-nTruePis, 1) );
Vec_IntPush( vOneHots, Fra_RegToLit(k-nTruePis, 1) );
continue;
}
if ( Fra_OneHotNodesAreClause( pSim, pObj1, pObj2, 0, 1 ) )
{
Vec_IntPush( vOneHots, Fra_RegToLit(i-nTruePis, 0) );
Vec_IntPush( vOneHots, Fra_RegToLit(k-nTruePis, 1) );
continue;
}
if ( Fra_OneHotNodesAreClause( pSim, pObj1, pObj2, 1, 0 ) )
{
Vec_IntPush( vOneHots, Fra_RegToLit(i-nTruePis, 1) );
Vec_IntPush( vOneHots, Fra_RegToLit(k-nTruePis, 0) );
continue;
}
}
}
return vOneHots;
}
/**Function*************************************************************
Synopsis [Assumes one-hot implications in the SAT solver.]
Description []
SideEffects []
SeeAlso []
**********************************************************************/
void Fra_OneHotAssume( Fra_Man_t * p, Vec_Int_t * vOneHots )
{
Aig_Obj_t * pObj1, * pObj2;
int i, Out1, Out2, pLits[2];
int nPiNum = Aig_ManPiNum(p->pManFraig) - Aig_ManRegNum(p->pManFraig);
assert( p->pPars->nFramesK == 1 ); // add to only one frame
for ( i = 0; i < Vec_IntSize(vOneHots); i += 2 )
{
Out1 = Vec_IntEntry( vOneHots, i );
Out2 = Vec_IntEntry( vOneHots, i+1 );
if ( Out1 == 0 && Out2 == 0 )
continue;
pObj1 = Aig_ManPi( p->pManFraig, nPiNum + Fra_LitReg(Out1) );
pObj2 = Aig_ManPi( p->pManFraig, nPiNum + Fra_LitReg(Out2) );
pLits[0] = toLitCond( Fra_ObjSatNum(pObj1), Fra_LitSign(Out1) );
pLits[1] = toLitCond( Fra_ObjSatNum(pObj2), Fra_LitSign(Out2) );
// add contraint to solver
if ( !sat_solver_addclause( p->pSat, pLits, pLits + 2 ) )
{
printf( "Fra_OneHotAssume(): Adding clause makes SAT solver unsat.\n" );
sat_solver_delete( p->pSat );
p->pSat = NULL;
return;
}
}
}
/**Function*************************************************************
Synopsis [Checks one-hot implications.]
Description []
SideEffects []
SeeAlso []
**********************************************************************/
void Fra_OneHotCheck( Fra_Man_t * p, Vec_Int_t * vOneHots )
{
Aig_Obj_t * pObj1, * pObj2;
int RetValue, i, Out1, Out2;
int nTruePos = Aig_ManPoNum(p->pManFraig) - Aig_ManRegNum(p->pManFraig);
for ( i = 0; i < Vec_IntSize(vOneHots); i += 2 )
{
Out1 = Vec_IntEntry( vOneHots, i );
Out2 = Vec_IntEntry( vOneHots, i+1 );
if ( Out1 == 0 && Out2 == 0 )
continue;
pObj1 = Aig_ManPo( p->pManFraig, nTruePos + Fra_LitReg(Out1) );
pObj2 = Aig_ManPo( p->pManFraig, nTruePos + Fra_LitReg(Out2) );
RetValue = Fra_NodesAreClause( p, pObj1, pObj2, Fra_LitSign(Out1), Fra_LitSign(Out2) );
if ( RetValue != 1 )
{
p->pCla->fRefinement = 1;
if ( RetValue == 0 )
Fra_SmlResimulate( p );
if ( Vec_IntEntry(vOneHots, i) != 0 )
printf( "Fra_OneHotCheck(): Clause is not refined!\n" );
assert( Vec_IntEntry(vOneHots, i) == 0 );
}
}
}
/**Function*************************************************************
Synopsis [Removes those implications that no longer hold.]
Description [Returns 1 if refinement has happened.]
SideEffects []
SeeAlso []
***********************************************************************/
int Fra_OneHotRefineUsingCex( Fra_Man_t * p, Vec_Int_t * vOneHots )
{
Aig_Obj_t * pObj1, * pObj2;
int i, Out1, Out2, RetValue = 0;
int nPiNum = Aig_ManPiNum(p->pManAig) - Aig_ManRegNum(p->pManAig);
assert( p->pSml->pAig == p->pManAig );
for ( i = 0; i < Vec_IntSize(vOneHots); i += 2 )
{
Out1 = Vec_IntEntry( vOneHots, i );
Out2 = Vec_IntEntry( vOneHots, i+1 );
if ( Out1 == 0 && Out2 == 0 )
continue;
// get the corresponding nodes
pObj1 = Aig_ManPi( p->pManAig, nPiNum + Fra_LitReg(Out1) );
pObj2 = Aig_ManPi( p->pManAig, nPiNum + Fra_LitReg(Out2) );
// check if implication holds using this simulation info
if ( !Fra_OneHotNodesAreClause( p->pSml, pObj1, pObj2, Fra_LitSign(Out1), Fra_LitSign(Out2) ) )
{
Vec_IntWriteEntry( vOneHots, i, 0 );
Vec_IntWriteEntry( vOneHots, i+1, 0 );
RetValue = 1;
}
}
return RetValue;
}
/**Function*************************************************************
Synopsis [Removes those implications that no longer hold.]
Description [Returns 1 if refinement has happened.]
SideEffects []
SeeAlso []
***********************************************************************/
int Fra_OneHotCount( Fra_Man_t * p, Vec_Int_t * vOneHots )
{
int i, Out1, Out2, Counter = 0;
for ( i = 0; i < Vec_IntSize(vOneHots); i += 2 )
{
Out1 = Vec_IntEntry( vOneHots, i );
Out2 = Vec_IntEntry( vOneHots, i+1 );
if ( Out1 == 0 && Out2 == 0 )
continue;
Counter++;
}
return Counter;
}
/**Function*************************************************************
Synopsis [Estimates the coverage of state space by clauses.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
void Fra_OneHotEstimateCoverage( Fra_Man_t * p, Vec_Int_t * vOneHots )
{
int nSimWords = (1<<14);
int nRegs = Aig_ManRegNum(p->pManAig);
Vec_Ptr_t * vSimInfo;
unsigned * pSim1, * pSim2, * pSimTot;
int i, w, Out1, Out2, nCovered, Counter = 0;
int clk = clock();
// generate random sim-info at register outputs
vSimInfo = Vec_PtrAllocSimInfo( nRegs + 1, nSimWords );
srand( 0xAABBAABB );
for ( i = 0; i < nRegs; i++ )
{
pSim1 = Vec_PtrEntry( vSimInfo, i );
for ( w = 0; w < nSimWords; w++ )
pSim1[w] = Fra_ObjRandomSim();
}
pSimTot = Vec_PtrEntry( vSimInfo, nRegs );
// collect simulation info
memset( pSimTot, 0, sizeof(unsigned) * nSimWords );
for ( i = 0; i < Vec_IntSize(vOneHots); i += 2 )
{
Out1 = Vec_IntEntry( vOneHots, i );
Out2 = Vec_IntEntry( vOneHots, i+1 );
if ( Out1 == 0 && Out2 == 0 )
continue;
//printf( "(%c%d,%c%d) ",
//Fra_LitSign(Out1)? '-': '+', Fra_LitReg(Out1),
//Fra_LitSign(Out2)? '-': '+', Fra_LitReg(Out2) );
Counter++;
pSim1 = Vec_PtrEntry( vSimInfo, Fra_LitReg(Out1) );
pSim2 = Vec_PtrEntry( vSimInfo, Fra_LitReg(Out2) );
if ( Fra_LitSign(Out1) && Fra_LitSign(Out2) )
for ( w = 0; w < nSimWords; w++ )
pSimTot[w] |= pSim1[w] & pSim2[w];
else if ( Fra_LitSign(Out1) )
for ( w = 0; w < nSimWords; w++ )
pSimTot[w] |= pSim1[w] & ~pSim2[w];
else if ( Fra_LitSign(Out2) )
for ( w = 0; w < nSimWords; w++ )
pSimTot[w] |= ~pSim1[w] & pSim2[w];
else
assert( 0 );
}
//printf( "\n" );
// count the total number of patterns contained in the don't-care
nCovered = 0;
for ( w = 0; w < nSimWords; w++ )
nCovered += Aig_WordCountOnes( pSimTot[w] );
Vec_PtrFree( vSimInfo );
// print the result
printf( "Care states ratio = %f. ", 1.0 * (nSimWords * 32 - nCovered) / (nSimWords * 32) );
printf( "(%d out of %d patterns) ", nSimWords * 32 - nCovered, nSimWords * 32 );
PRT( "Time", clock() - clk );
}
/**Function*************************************************************
Synopsis [Creates one-hotness EXDC.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
Aig_Man_t * Fra_OneHotCreateExdc( Fra_Man_t * p, Vec_Int_t * vOneHots )
{
Aig_Man_t * pNew;
Aig_Obj_t * pObj1, * pObj2, * pObj;
int i, Out1, Out2;
pNew = Aig_ManStart( Vec_IntSize(vOneHots)/2 );
for ( i = 0; i < Aig_ManRegNum(p->pManAig); i++ )
Aig_ObjCreatePi(pNew);
for ( i = 0; i < Vec_IntSize(vOneHots); i += 2 )
{
Out1 = Vec_IntEntry( vOneHots, i );
Out2 = Vec_IntEntry( vOneHots, i+1 );
if ( Out1 == 0 && Out2 == 0 )
continue;
pObj1 = Aig_ManPi( pNew, Fra_LitReg(Out1) );
pObj2 = Aig_ManPi( pNew, Fra_LitReg(Out2) );
pObj1 = Aig_NotCond( pObj1, Fra_LitSign(Out1) );
pObj2 = Aig_NotCond( pObj2, Fra_LitSign(Out2) );
pObj = Aig_Or( pNew, pObj1, pObj2 );
Aig_ObjCreatePo( pNew, pObj );
}
Aig_ManCleanup(pNew);
printf( "Created AIG with %d nodes and %d outputs.\n", Aig_ManNodeNum(pNew), Aig_ManPoNum(pNew) );
return pNew;
}
////////////////////////////////////////////////////////////////////////
/// END OF FILE ///
////////////////////////////////////////////////////////////////////////

43
src/aig/fra/fraInd.c
View File

@ -243,7 +243,7 @@ void Fra_FramesAddMore( Aig_Man_t * p, int nFrames )
SeeAlso []
***********************************************************************/
Aig_Man_t * Fra_FraigInduction( Aig_Man_t * pManAig, int nFramesP, int nFramesK, int nMaxImps, int nMaxLevs, int fRewrite, int fUseImps, int fLatchCorr, int fWriteImps, int fVerbose, int * pnIter )
Aig_Man_t * Fra_FraigInduction( Aig_Man_t * pManAig, int nFramesP, int nFramesK, int nMaxImps, int nMaxLevs, int fRewrite, int fUseImps, int fLatchCorr, int fWriteImps, int fUse1Hot, int fVerbose, int * pnIter )
{
int fUseSimpleCnf = 0;
int fUseOldSimulation = 0;
@ -288,6 +288,10 @@ Aig_Man_t * Fra_FraigInduction( Aig_Man_t * pManAig, int nFramesP, int nFramesK,
pPars->fLatchCorr = fLatchCorr;
pPars->fUseImps = fUseImps;
pPars->fWriteImps = fWriteImps;
pPars->fUse1Hot = fUse1Hot;
assert( !(pPars->nFramesP > 0 && pPars->fUse1Hot) );
assert( !(pPars->nFramesK > 1 && pPars->fUse1Hot) );
// start the fraig manager for this run
p = Fra_ManStart( pManAig, pPars );
@ -316,6 +320,9 @@ PRT( "Time", clock() - clk );
}
Fra_ClassesPrepare( p->pCla, p->pPars->fLatchCorr, p->pPars->nMaxLevs );
// Fra_ClassesPostprocess( p->pCla );
// compute one-hotness conditions
if ( p->pPars->fUse1Hot )
p->vOneHots = Fra_OneHotCompute( p, p->pSml );
// allocate new simulation manager for simulating counter-examples
Fra_SmlStop( p->pSml );
p->pSml = Fra_SmlStart( pManAig, 0, pPars->nFramesK + 1, pPars->nSimWords );
@ -347,6 +354,7 @@ PRT( "Time", clock() - clk );
{
int nLitsOld = Fra_ClassesCountLits(p->pCla);
int nImpsOld = p->pCla->vImps? Vec_IntSize(p->pCla->vImps) : 0;
int nHotsOld = p->vOneHots? Fra_OneHotCount(p, p->vOneHots) : 0;
// mark the classes as non-refined
p->pCla->fRefinement = 0;
// derive non-init K-timeframes while implementing e-classes
@ -377,7 +385,7 @@ p->timeTrav += clock() - clk2;
if ( p->pSat == NULL )
printf( "Fra_FraigInduction(): Adding implicationsn to CNF led to a conflict.\n" );
}
// set the pointers to the manager
Aig_ManForEachObj( p->pManFraig, pObj, i )
pObj->pData = p;
@ -395,6 +403,10 @@ p->timeTrav += clock() - clk2;
}
Cnf_DataFree( pCnf );
// add one-hotness clauses
if ( p->pPars->fUse1Hot )
Fra_OneHotAssume( p, p->vOneHots );
// report the intermediate results
if ( fVerbose )
{
@ -403,6 +415,8 @@ p->timeTrav += clock() - clk2;
Fra_ClassesCountLits(p->pCla), p->pManFraig->nAsserts );
if ( p->pCla->vImps )
printf( "I = %6d. ", Vec_IntSize(p->pCla->vImps) );
if ( p->pPars->fUse1Hot )
printf( "1h = %6d. ", Fra_OneHotCount(p, p->vOneHots) );
printf( "NR = %6d. ", Aig_ManNodeNum(p->pManFraig) );
printf( "\n" );
}
@ -411,6 +425,8 @@ p->timeTrav += clock() - clk2;
p->nSatCallsRecent = 0;
p->nSatCallsSkipped = 0;
clk2 = clock();
if ( p->pPars->fUse1Hot )
Fra_OneHotCheck( p, p->vOneHots );
Fra_FraigSweep( p );
if ( fVerbose )
{
@ -430,7 +446,8 @@ clk2 = clock();
// p->pCla->fRefinement = (int)(nLitsOld != Fra_ClassesCountLits(p->pCla));
if ( p->pCla->fRefinement &&
nLitsOld == Fra_ClassesCountLits(p->pCla) &&
nImpsOld == (p->pCla->vImps? Vec_IntSize(p->pCla->vImps) : 0) )
nImpsOld == (p->pCla->vImps? Vec_IntSize(p->pCla->vImps) : 0) &&
nHotsOld == (p->vOneHots? Fra_OneHotCount(p, p->vOneHots) : 0) )
{
printf( "Fra_FraigInduction(): Internal error. The result may not verify.\n" );
break;
@ -451,13 +468,21 @@ clk2 = clock();
// move the classes into representatives and reduce AIG
clk2 = clock();
// Fra_ClassesPrint( p->pCla, 1 );
Fra_ClassesSelectRepr( p->pCla );
Fra_ClassesCopyReprs( p->pCla, p->vTimeouts );
pManAigNew = Aig_ManDupRepr( pManAig, 0 );
if ( p->pPars->fWriteImps && p->vOneHots && Fra_OneHotCount(p, p->vOneHots) )
{
pManAigNew = Aig_ManDup( pManAig, 1 );
pManAigNew->pManExdc = Fra_OneHotCreateExdc( p, p->vOneHots );
}
else
{
// Fra_ClassesPrint( p->pCla, 1 );
Fra_ClassesSelectRepr( p->pCla );
Fra_ClassesCopyReprs( p->pCla, p->vTimeouts );
pManAigNew = Aig_ManDupRepr( pManAig, 0 );
}
// add implications to the manager
if ( fWriteImps && p->pCla->vImps && Vec_IntSize(p->pCla->vImps) )
Fra_ImpRecordInManager( p, pManAigNew );
// if ( fWriteImps && p->pCla->vImps && Vec_IntSize(p->pCla->vImps) )
// Fra_ImpRecordInManager( p, pManAigNew );
// cleanup the new manager
Aig_ManSeqCleanup( pManAigNew );
// Aig_ManCountMergeRegs( pManAigNew );

161
src/aig/fra/fraIndVer.c Normal file
View File

@ -0,0 +1,161 @@
/**CFile****************************************************************
FileName [fraIndVer.c]
SystemName [ABC: Logic synthesis and verification system.]
PackageName [New FRAIG package.]
Synopsis [Verification of the inductive invariant.]
Author [Alan Mishchenko]
Affiliation [UC Berkeley]
Date [Ver. 1.0. Started - June 30, 2007.]
Revision [$Id: fraIndVer.c,v 1.00 2007/06/30 00:00:00 alanmi Exp $]
***********************************************************************/
#include "fra.h"
#include "cnf.h"
////////////////////////////////////////////////////////////////////////
/// DECLARATIONS ///
////////////////////////////////////////////////////////////////////////
////////////////////////////////////////////////////////////////////////
/// FUNCTION DEFINITIONS ///
////////////////////////////////////////////////////////////////////////
/**Function*************************************************************
Synopsis [Verifies the inductive invariant.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
int Fra_InvariantVerify( Aig_Man_t * pAig, int nFrames, Vec_Int_t * vClauses, Vec_Int_t * vLits )
{
Cnf_Dat_t * pCnf;
sat_solver * pSat;
int * pStart;
int RetValue, Beg, End, i, k;
int CounterBase = 0, CounterInd = 0;
int clk = clock();
if ( nFrames != 1 )
{
printf( "Invariant verification: Can only verify for K = 1\n" );
return 1;
}
// derive CNF
pCnf = Cnf_DeriveSimple( pAig, Aig_ManPoNum(pAig) );
/*
// add the property
{
Aig_Obj_t * pObj;
int Lits[1];
pObj = Aig_ManPo( pAig, 0 );
Lits[0] = toLitCond( pCnf->pVarNums[pObj->Id], 1 );
Vec_IntPush( vLits, Lits[0] );
Vec_IntPush( vClauses, Vec_IntSize(vLits) );
printf( "Added the target property to the set of clauses to be inductively checked.\n" );
}
*/
// derive initialized frames for the base case
pSat = Cnf_DataWriteIntoSolver( pCnf, nFrames, 1 );
// check clauses in the base case
Beg = 0;
pStart = Vec_IntArray( vLits );
Vec_IntForEachEntry( vClauses, End, i )
{
// complement the literals
for ( k = Beg; k < End; k++ )
pStart[k] = lit_neg(pStart[k]);
RetValue = sat_solver_solve( pSat, pStart + Beg, pStart + End, 0, 0, 0, 0 );
for ( k = Beg; k < End; k++ )
pStart[k] = lit_neg(pStart[k]);
Beg = End;
if ( RetValue == l_False )
continue;
// printf( "Clause %d failed the base case.\n", i );
CounterBase++;
}
sat_solver_delete( pSat );
// derive initialized frames for the base case
pSat = Cnf_DataWriteIntoSolver( pCnf, nFrames + 1, 0 );
assert( pSat->size == 2 * pCnf->nVars );
// add clauses to the first frame
Beg = 0;
pStart = Vec_IntArray( vLits );
Vec_IntForEachEntry( vClauses, End, i )
{
RetValue = sat_solver_addclause( pSat, pStart + Beg, pStart + End );
Beg = End;
if ( RetValue == 0 )
{
Cnf_DataFree( pCnf );
sat_solver_delete( pSat );
printf( "Invariant verification: SAT solver is unsat after adding a clause.\n" );
return 0;
}
}
// simplify the solver
if ( pSat->qtail != pSat->qhead )
{
RetValue = sat_solver_simplify(pSat);
assert( RetValue != 0 );
assert( pSat->qtail == pSat->qhead );
}
// check clauses in the base case
Beg = 0;
pStart = Vec_IntArray( vLits );
Vec_IntForEachEntry( vClauses, End, i )
{
// complement the literals
for ( k = Beg; k < End; k++ )
{
pStart[k] += 2 * pCnf->nVars;
pStart[k] = lit_neg(pStart[k]);
}
RetValue = sat_solver_solve( pSat, pStart + Beg, pStart + End, 0, 0, 0, 0 );
for ( k = Beg; k < End; k++ )
{
pStart[k] = lit_neg(pStart[k]);
pStart[k] -= 2 * pCnf->nVars;
}
Beg = End;
if ( RetValue == l_False )
continue;
// printf( "Clause %d failed the inductive case.\n", i );
CounterInd++;
}
sat_solver_delete( pSat );
Cnf_DataFree( pCnf );
if ( CounterBase )
printf( "Invariant verification: %d clauses (out of %d) FAILED the base case.\n", CounterBase, Vec_IntSize(vClauses) );
if ( CounterInd )
printf( "Invariant verification: %d clauses (out of %d) FAILED the inductive case.\n", CounterInd, Vec_IntSize(vClauses) );
if ( CounterBase || CounterInd )
return 0;
printf( "Invariant verification: %d clauses verified correctly. ", Vec_IntSize(vClauses) );
PRT( "Time", clock() - clk );
return 1;
}
////////////////////////////////////////////////////////////////////////
/// END OF FILE ///
////////////////////////////////////////////////////////////////////////

4
src/aig/fra/fraMan.c
View File

@ -251,6 +251,7 @@ void Fra_ManStop( Fra_Man_t * p )
if ( p->pCla ) Fra_ClassesStop( p->pCla );
if ( p->pSml ) Fra_SmlStop( p->pSml );
if ( p->vCex ) Vec_IntFree( p->vCex );
if ( p->vOneHots ) Vec_IntFree( p->vOneHots );
FREE( p->pMemFraig );
FREE( p->pMemFanins );
FREE( p->pMemSatNums );
@ -279,7 +280,8 @@ void Fra_ManPrint( Fra_Man_t * p )
printf( "NBeg = %d. NEnd = %d. (Gain = %6.2f %%). RBeg = %d. REnd = %d. (Gain = %6.2f %%).\n",
p->nNodesBeg, p->nNodesEnd, 100.0*(p->nNodesBeg-p->nNodesEnd)/(p->nNodesBeg?p->nNodesBeg:1),
p->nRegsBeg, p->nRegsEnd, 100.0*(p->nRegsBeg-p->nRegsEnd)/(p->nRegsBeg?p->nRegsBeg:1) );
if ( p->pSat ) Sat_SolverPrintStats( stdout, p->pSat );
if ( p->pSat ) Sat_SolverPrintStats( stdout, p->pSat );
if ( p->pPars->fUse1Hot ) Fra_OneHotEstimateCoverage( p, p->vOneHots );
PRT( "AIG simulation ", p->pSml->timeSim );
PRT( "AIG traversal ", p->timeTrav );
if ( p->timeRwr )

107
src/aig/fra/fraSat.c
View File

@ -298,6 +298,113 @@ p->timeSatFail += clock() - clk;
return 1;
}
/**Function*************************************************************
Synopsis [Runs the result of test for pObj => pNew.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
int Fra_NodesAreClause( Fra_Man_t * p, Aig_Obj_t * pOld, Aig_Obj_t * pNew, int fComplL, int fComplR )
{
int pLits[4], RetValue, RetValue1, nBTLimit, clk;//, clk2 = clock();
int status;
// make sure the nodes are not complemented
assert( !Aig_IsComplement(pNew) );
assert( !Aig_IsComplement(pOld) );
assert( pNew != pOld );
// if at least one of the nodes is a failed node, perform adjustments:
// if the backtrack limit is small, simply skip this node
// if the backtrack limit is > 10, take the quare root of the limit
nBTLimit = p->pPars->nBTLimitNode;
/*
if ( !p->pPars->fSpeculate && p->pPars->nFramesK == 0 && (nBTLimit > 0 && (pOld->fMarkB || pNew->fMarkB)) )
{
p->nSatFails++;
// fail immediately
// return -1;
if ( nBTLimit <= 10 )
return -1;
nBTLimit = (int)pow(nBTLimit, 0.7);
}
*/
p->nSatCalls++;
// make sure the solver is allocated and has enough variables
if ( p->pSat == NULL )
{
p->pSat = sat_solver_new();
p->nSatVars = 1;
sat_solver_setnvars( p->pSat, 1000 );
// var 0 is reserved for const1 node - add the clause
pLits[0] = toLit( 0 );
sat_solver_addclause( p->pSat, pLits, pLits + 1 );
}
// if the nodes do not have SAT variables, allocate them
Fra_CnfNodeAddToSolver( p, pOld, pNew );
if ( p->pSat->qtail != p->pSat->qhead )
{
status = sat_solver_simplify(p->pSat);
assert( status != 0 );
assert( p->pSat->qtail == p->pSat->qhead );
}
// prepare variable activity
if ( p->pPars->fConeBias )
Fra_SetActivityFactors( p, pOld, pNew );
// solve under assumptions
// A = 1; B = 0 OR A = 1; B = 1
clk = clock();
// pLits[0] = toLitCond( Fra_ObjSatNum(pOld), 0 );
// pLits[1] = toLitCond( Fra_ObjSatNum(pNew), pOld->fPhase == pNew->fPhase );
pLits[0] = toLitCond( Fra_ObjSatNum(pOld), !fComplL );
pLits[1] = toLitCond( Fra_ObjSatNum(pNew), !fComplR );
//Sat_SolverWriteDimacs( p->pSat, "temp.cnf", pLits, pLits + 2, 1 );
RetValue1 = sat_solver_solve( p->pSat, pLits, pLits + 2,
(sint64)nBTLimit, (sint64)0,
p->nBTLimitGlobal, p->nInsLimitGlobal );
p->timeSat += clock() - clk;
if ( RetValue1 == l_False )
{
p->timeSatUnsat += clock() - clk;
pLits[0] = lit_neg( pLits[0] );
pLits[1] = lit_neg( pLits[1] );
RetValue = sat_solver_addclause( p->pSat, pLits, pLits + 2 );
assert( RetValue );
// continue solving the other implication
p->nSatCallsUnsat++;
}
else if ( RetValue1 == l_True )
{
p->timeSatSat += clock() - clk;
Fra_SmlSavePattern( p );
p->nSatCallsSat++;
return 0;
}
else // if ( RetValue1 == l_Undef )
{
p->timeSatFail += clock() - clk;
// mark the node as the failed node
if ( pOld != p->pManFraig->pConst1 )
pOld->fMarkB = 1;
pNew->fMarkB = 1;
p->nSatFailsReal++;
return -1;
}
// return SAT proof
p->nSatProof++;
return 1;
}
/**Function*************************************************************
Synopsis [Runs equivalence test for one node.]

6
src/aig/fra/fraSec.c
View File

@ -49,7 +49,7 @@ int Fra_FraigSec2( Aig_Man_t * p, int nFramesFix, int fVerbose, int fVeryVerbose
{
nFrames = nFramesFix;
// perform seq sweeping for one frame number
pNew = Fra_FraigInduction( p, 0, nFrames, 0, 0, 0, 0, fLatchCorr, 0, fVeryVerbose, &nIter );
pNew = Fra_FraigInduction( p, 0, nFrames, 0, 0, 0, 0, fLatchCorr, 0, 0, fVeryVerbose, &nIter );
}
else
{
@ -57,7 +57,7 @@ int Fra_FraigSec2( Aig_Man_t * p, int nFramesFix, int fVerbose, int fVeryVerbose
for ( nFrames = 1; ; nFrames++ )
{
clk = clock();
pNew = Fra_FraigInduction( p, 0, nFrames, 0, 0, 0, 0, fLatchCorr, 0, fVeryVerbose, &nIter );
pNew = Fra_FraigInduction( p, 0, nFrames, 0, 0, 0, 0, fLatchCorr, 0, 0, fVeryVerbose, &nIter );
RetValue = Fra_FraigMiterStatus( pNew );
if ( fVerbose )
{
@ -185,7 +185,7 @@ PRT( "Time", clock() - clk );
for ( nFrames = 1; nFrames <= nFramesMax; nFrames *= 2 )
{
clk = clock();
pNew = Fra_FraigInduction( pTemp = pNew, 0, nFrames, 0, 0, 0, 0, fLatchCorr, 0, fVeryVerbose, &nIter );
pNew = Fra_FraigInduction( pTemp = pNew, 0, nFrames, 0, 0, 0, 0, fLatchCorr, 0, 0, fVeryVerbose, &nIter );
Aig_ManStop( pTemp );
RetValue = Fra_FraigMiterStatus( pNew );
if ( fVerbose )

2
src/aig/fra/fraSim.c
View File

@ -657,6 +657,8 @@ clk = clock();
nChanges += Fra_ClassesRefine1( p->pCla, 1, NULL );
if ( p->pCla->vImps )
nChanges += Fra_ImpRefineUsingCex( p, p->pCla->vImps );
if ( p->vOneHots )
nChanges += Fra_OneHotRefineUsingCex( p, p->vOneHots );
p->timeRef += clock() - clk;
if ( !p->pPars->nFramesK && nChanges < 1 )
printf( "Error: A counter-example did not refine classes!\n" );

2
src/aig/fra/module.make
View File

@ -5,8 +5,10 @@ SRC += src/aig/fra/fraBmc.c \
src/aig/fra/fraClaus.c \
src/aig/fra/fraCnf.c \
src/aig/fra/fraCore.c \
src/aig/fra/fraHot.c \
src/aig/fra/fraImp.c \
src/aig/fra/fraInd.c \
src/aig/fra/fraIndVer.c \
src/aig/fra/fraLcr.c \
src/aig/fra/fraMan.c \
src/aig/fra/fraPart.c \

1
src/base/abc/abc.h
View File

@ -199,6 +199,7 @@ struct Abc_Ntk_t_
int * pModel; // counter-example (for miters)
void * pSeqModel; // counter-example (for sequential miters)
Abc_Ntk_t * pExdc; // the EXDC network (if given)
void * pManExdc; // the EXDC network (if given)
void * pData; // misc
Abc_Ntk_t * pCopy;
Hop_Man_t * pHaig; // history AIG

10
src/base/abc/abcNtk.c
View File

@ -23,6 +23,8 @@
#include "main.h"
#include "mio.h"
#include "aig.h"
////////////////////////////////////////////////////////////////////////
/// DECLARATIONS ///
////////////////////////////////////////////////////////////////////////
@ -346,6 +348,8 @@ Abc_Ntk_t * Abc_NtkDup( Abc_Ntk_t * pNtk )
// duplicate the EXDC Ntk
if ( pNtk->pExdc )
pNtkNew->pExdc = Abc_NtkDup( pNtk->pExdc );
if ( pNtk->pManExdc )
pNtkNew->pManExdc = Aig_ManDup( pNtk->pManExdc, 0 );
if ( !Abc_NtkCheck( pNtkNew ) )
fprintf( stdout, "Abc_NtkDup(): Network check has failed.\n" );
pNtk->pCopy = pNtkNew;
@ -431,6 +435,7 @@ Abc_Ntk_t * Abc_NtkDouble( Abc_Ntk_t * pNtk )
Abc_ObjAssignName( Abc_NtkCo(pNtkNew, i), "1_", Abc_ObjName(pObj) );
Abc_ObjAssignName( Abc_NtkCo(pNtkNew, Abc_NtkCoNum(pNtk) + i), "2_", Abc_ObjName(pObj) );
}
Abc_NtkOrderCisCos( pNtkNew );
// perform the final check
if ( !Abc_NtkCheck( pNtkNew ) )
@ -936,6 +941,11 @@ void Abc_NtkDelete( Abc_Ntk_t * pNtk )
// free EXDC Ntk
if ( pNtk->pExdc )
Abc_NtkDelete( pNtk->pExdc );
if ( pNtk->pManExdc )
{
Aig_ManStop( pNtk->pManExdc );
pNtk->pManExdc = NULL;
}
// dereference the BDDs
if ( Abc_NtkHasBdd(pNtk) )
{

435
src/base/abci/abc.c
View File

@ -29,6 +29,7 @@
#include "lpk.h"
#include "aig.h"
#include "dar.h"
#include "mfs.h"
////////////////////////////////////////////////////////////////////////
/// DECLARATIONS ///
@ -66,8 +67,9 @@ static int Abc_CommandSweep ( Abc_Frame_t * pAbc, int argc, char ** arg
static int Abc_CommandFastExtract ( Abc_Frame_t * pAbc, int argc, char ** argv );
static int Abc_CommandEliminate ( Abc_Frame_t * pAbc, int argc, char ** argv );
static int Abc_CommandDisjoint ( Abc_Frame_t * pAbc, int argc, char ** argv );
static int Abc_CommandImfs ( Abc_Frame_t * pAbc, int argc, char ** argv );
static int Abc_CommandLutpack ( Abc_Frame_t * pAbc, int argc, char ** argv );
static int Abc_CommandImfs ( Abc_Frame_t * pAbc, int argc, char ** argv );
static int Abc_CommandMfs ( Abc_Frame_t * pAbc, int argc, char ** argv );
static int Abc_CommandRewrite ( Abc_Frame_t * pAbc, int argc, char ** argv );
static int Abc_CommandRefactor ( Abc_Frame_t * pAbc, int argc, char ** argv );
@ -244,8 +246,9 @@ void Abc_Init( Abc_Frame_t * pAbc )
Cmd_CommandAdd( pAbc, "Synthesis", "fx", Abc_CommandFastExtract, 1 );
Cmd_CommandAdd( pAbc, "Synthesis", "eliminate", Abc_CommandEliminate, 1 );
Cmd_CommandAdd( pAbc, "Synthesis", "dsd", Abc_CommandDisjoint, 1 );
Cmd_CommandAdd( pAbc, "Synthesis", "imfs", Abc_CommandImfs, 1 );
Cmd_CommandAdd( pAbc, "Synthesis", "lutpack", Abc_CommandLutpack, 1 );
Cmd_CommandAdd( pAbc, "Synthesis", "imfs", Abc_CommandImfs, 1 );
Cmd_CommandAdd( pAbc, "Synthesis", "mfs", Abc_CommandMfs, 1 );
Cmd_CommandAdd( pAbc, "Synthesis", "rewrite", Abc_CommandRewrite, 1 );
Cmd_CommandAdd( pAbc, "Synthesis", "refactor", Abc_CommandRefactor, 1 );
@ -650,17 +653,23 @@ int Abc_CommandPrintLatch( Abc_Frame_t * pAbc, int argc, char ** argv )
FILE * pOut, * pErr;
Abc_Ntk_t * pNtk;
int c;
int fPrintSccs;
extern void Abc_NtkPrintSccs( Abc_Ntk_t * pNtk, int fVerbose );
pNtk = Abc_FrameReadNtk(pAbc);
pOut = Abc_FrameReadOut(pAbc);
pErr = Abc_FrameReadErr(pAbc);
// set defaults
fPrintSccs = 0;
Extra_UtilGetoptReset();
while ( ( c = Extra_UtilGetopt( argc, argv, "h" ) ) != EOF )
while ( ( c = Extra_UtilGetopt( argc, argv, "sh" ) ) != EOF )
{
switch ( c )
{
case 's':
fPrintSccs ^= 1;
break;
case 'h':
goto usage;
default:
@ -675,11 +684,14 @@ int Abc_CommandPrintLatch( Abc_Frame_t * pAbc, int argc, char ** argv )
}
// print the nodes
Abc_NtkPrintLatch( pOut, pNtk );
if ( fPrintSccs )
Abc_NtkPrintSccs( pNtk, 0 );
return 0;
usage:
fprintf( pErr, "usage: print_latch [-h]\n" );
fprintf( pErr, "usage: print_latch [-sh]\n" );
fprintf( pErr, "\t prints information about latches\n" );
fprintf( pErr, "\t-s : toggles printing SCCs of registers [default = %s]\n", fPrintSccs? "yes": "no" );
fprintf( pErr, "\t-h : print the command usage\n");
return 1;
}
@ -2935,138 +2947,6 @@ usage:
return 1;
}
/**Function*************************************************************
Synopsis []
Description []
SideEffects []
SeeAlso []
***********************************************************************/
int Abc_CommandImfs( Abc_Frame_t * pAbc, int argc, char ** argv )
{
FILE * pOut, * pErr;
Abc_Ntk_t * pNtk;
Res_Par_t Pars, * pPars = &Pars;
int c;
// printf( "Implementation of this command is not finished.\n" );
// return 1;
pNtk = Abc_FrameReadNtk(pAbc);
pOut = Abc_FrameReadOut(pAbc);
pErr = Abc_FrameReadErr(pAbc);
// set defaults
pPars->nWindow = 62;
pPars->nCands = 5;
pPars->nSimWords = 4;
pPars->nGrowthLevel = 0;
pPars->fArea = 0;
pPars->fVerbose = 0;
pPars->fVeryVerbose = 0;
Extra_UtilGetoptReset();
while ( ( c = Extra_UtilGetopt( argc, argv, "WSCLavwh" ) ) != EOF )
{
switch ( c )
{
case 'W':
if ( globalUtilOptind >= argc )
{
fprintf( pErr, "Command line switch \"-W\" should be followed by an integer.\n" );
goto usage;
}
pPars->nWindow = atoi(argv[globalUtilOptind]);
globalUtilOptind++;
if ( pPars->nWindow < 1 || pPars->nWindow > 99 )
goto usage;
break;
case 'S':
if ( globalUtilOptind >= argc )
{
fprintf( pErr, "Command line switch \"-S\" should be followed by an integer.\n" );
goto usage;
}
pPars->nSimWords = atoi(argv[globalUtilOptind]);
globalUtilOptind++;
if ( pPars->nSimWords < 1 || pPars->nSimWords > 256 )
goto usage;
break;
case 'C':
if ( globalUtilOptind >= argc )
{
fprintf( pErr, "Command line switch \"-C\" should be followed by an integer.\n" );
goto usage;
}
pPars->nCands = atoi(argv[globalUtilOptind]);
globalUtilOptind++;
if ( pPars->nCands < 0 || pPars->nCands > ABC_INFINITY )
goto usage;
break;
case 'L':
if ( globalUtilOptind >= argc )
{
fprintf( pErr, "Command line switch \"-L\" should be followed by an integer.\n" );
goto usage;
}
pPars->nGrowthLevel = atoi(argv[globalUtilOptind]);
globalUtilOptind++;
if ( pPars->nGrowthLevel < 0 || pPars->nGrowthLevel > ABC_INFINITY )
goto usage;
break;
case 'a':
pPars->fArea ^= 1;
break;
case 'v':
pPars->fVerbose ^= 1;
break;
case 'w':
pPars->fVeryVerbose ^= 1;
break;
case 'h':
goto usage;
default:
goto usage;
}
}
if ( pNtk == NULL )
{
fprintf( pErr, "Empty network.\n" );
return 1;
}
if ( !Abc_NtkIsLogic(pNtk) )
{
fprintf( pErr, "This command can only be applied to a logic network.\n" );
return 1;
}
// modify the current network
if ( !Abc_NtkResynthesize( pNtk, pPars ) )
{
fprintf( pErr, "Resynthesis has failed.\n" );
return 1;
}
return 0;
usage:
fprintf( pErr, "usage: imfs [-W <NM>] [-L <num>] [-C <num>] [-S <num>] [-avwh]\n" );
fprintf( pErr, "\t performs resubstitution-based resynthesis with interpolation\n" );
fprintf( pErr, "\t (there is another command for resynthesis after LUT mapping, \"lutpack\")\n" );
fprintf( pErr, "\t-W <NM> : fanin/fanout levels (NxM) of the window (00 <= NM <= 99) [default = %d%d]\n", pPars->nWindow/10, pPars->nWindow%10 );
fprintf( pErr, "\t-C <num> : the max number of resub candidates (1 <= n) [default = %d]\n", pPars->nCands );
fprintf( pErr, "\t-S <num> : the number of simulation words (1 <= n <= 256) [default = %d]\n", pPars->nSimWords );
fprintf( pErr, "\t-L <num> : the largest increase in node level after resynthesis (0 <= num) [default = %d]\n", pPars->nGrowthLevel );
fprintf( pErr, "\t-a : toggle optimization for area only [default = %s]\n", pPars->fArea? "yes": "no" );
fprintf( pErr, "\t-v : toggle verbose printout [default = %s]\n", pPars->fVerbose? "yes": "no" );
fprintf( pErr, "\t-w : toggle printout subgraph statistics [default = %s]\n", pPars->fVeryVerbose? "yes": "no" );
fprintf( pErr, "\t-h : print the command usage\n");
return 1;
}
/**Function*************************************************************
Synopsis []
@ -3219,6 +3099,255 @@ usage:
return 1;
}
/**Function*************************************************************
Synopsis []
Description []
SideEffects []
SeeAlso []
***********************************************************************/
int Abc_CommandImfs( Abc_Frame_t * pAbc, int argc, char ** argv )
{
FILE * pOut, * pErr;
Abc_Ntk_t * pNtk;
Res_Par_t Pars, * pPars = &Pars;
int c;
// printf( "Implementation of this command is not finished.\n" );
// return 1;
pNtk = Abc_FrameReadNtk(pAbc);
pOut = Abc_FrameReadOut(pAbc);
pErr = Abc_FrameReadErr(pAbc);
// set defaults
pPars->nWindow = 62;
pPars->nCands = 5;
pPars->nSimWords = 4;
pPars->nGrowthLevel = 0;
pPars->fArea = 0;
pPars->fVerbose = 0;
pPars->fVeryVerbose = 0;
Extra_UtilGetoptReset();
while ( ( c = Extra_UtilGetopt( argc, argv, "WSCLavwh" ) ) != EOF )
{
switch ( c )
{
case 'W':
if ( globalUtilOptind >= argc )
{
fprintf( pErr, "Command line switch \"-W\" should be followed by an integer.\n" );
goto usage;
}
pPars->nWindow = atoi(argv[globalUtilOptind]);
globalUtilOptind++;
if ( pPars->nWindow < 1 || pPars->nWindow > 99 )
goto usage;
break;
case 'S':
if ( globalUtilOptind >= argc )
{
fprintf( pErr, "Command line switch \"-S\" should be followed by an integer.\n" );
goto usage;
}
pPars->nSimWords = atoi(argv[globalUtilOptind]);
globalUtilOptind++;
if ( pPars->nSimWords < 1 || pPars->nSimWords > 256 )
goto usage;
break;
case 'C':
if ( globalUtilOptind >= argc )
{
fprintf( pErr, "Command line switch \"-C\" should be followed by an integer.\n" );
goto usage;
}
pPars->nCands = atoi(argv[globalUtilOptind]);
globalUtilOptind++;
if ( pPars->nCands < 0 || pPars->nCands > ABC_INFINITY )
goto usage;
break;
case 'L':
if ( globalUtilOptind >= argc )
{
fprintf( pErr, "Command line switch \"-L\" should be followed by an integer.\n" );
goto usage;
}
pPars->nGrowthLevel = atoi(argv[globalUtilOptind]);
globalUtilOptind++;
if ( pPars->nGrowthLevel < 0 || pPars->nGrowthLevel > ABC_INFINITY )
goto usage;
break;
case 'a':
pPars->fArea ^= 1;
break;
case 'v':
pPars->fVerbose ^= 1;
break;
case 'w':
pPars->fVeryVerbose ^= 1;
break;
case 'h':
goto usage;
default:
goto usage;
}
}
if ( pNtk == NULL )
{
fprintf( pErr, "Empty network.\n" );
return 1;
}
if ( !Abc_NtkIsLogic(pNtk) )
{
fprintf( pErr, "This command can only be applied to a logic network.\n" );
return 1;
}
// modify the current network
if ( !Abc_NtkResynthesize( pNtk, pPars ) )
{
fprintf( pErr, "Resynthesis has failed.\n" );
return 1;
}
return 0;
usage:
fprintf( pErr, "usage: imfs [-W <NM>] [-L <num>] [-C <num>] [-S <num>] [-avwh]\n" );
fprintf( pErr, "\t performs resubstitution-based resynthesis with interpolation\n" );
fprintf( pErr, "\t (there is another command for resynthesis after LUT mapping, \"lutpack\")\n" );
fprintf( pErr, "\t-W <NM> : fanin/fanout levels (NxM) of the window (00 <= NM <= 99) [default = %d%d]\n", pPars->nWindow/10, pPars->nWindow%10 );
fprintf( pErr, "\t-C <num> : the max number of resub candidates (1 <= n) [default = %d]\n", pPars->nCands );
fprintf( pErr, "\t-S <num> : the number of simulation words (1 <= n <= 256) [default = %d]\n", pPars->nSimWords );
fprintf( pErr, "\t-L <num> : the largest increase in node level after resynthesis (0 <= num) [default = %d]\n", pPars->nGrowthLevel );
fprintf( pErr, "\t-a : toggle optimization for area only [default = %s]\n", pPars->fArea? "yes": "no" );
fprintf( pErr, "\t-v : toggle verbose printout [default = %s]\n", pPars->fVerbose? "yes": "no" );
fprintf( pErr, "\t-w : toggle printout subgraph statistics [default = %s]\n", pPars->fVeryVerbose? "yes": "no" );
fprintf( pErr, "\t-h : print the command usage\n");
return 1;
}
/**Function*************************************************************
Synopsis []
Description []
SideEffects []
SeeAlso []
***********************************************************************/
int Abc_CommandMfs( Abc_Frame_t * pAbc, int argc, char ** argv )
{
FILE * pOut, * pErr;
Abc_Ntk_t * pNtk;
Mfs_Par_t Pars, * pPars = &Pars;
int c;
// printf( "Implementation of this command is not finished.\n" );
// return 1;
pNtk = Abc_FrameReadNtk(pAbc);
pOut = Abc_FrameReadOut(pAbc);
pErr = Abc_FrameReadErr(pAbc);
// set defaults
pPars->nWinTfoLevs = 2;
pPars->nFanoutsMax = 10;
pPars->nGrowthLevel = 0;
pPars->fArea = 0;
pPars->fVerbose = 0;
pPars->fVeryVerbose = 0;
Extra_UtilGetoptReset();
while ( ( c = Extra_UtilGetopt( argc, argv, "WFLavwh" ) ) != EOF )
{
switch ( c )
{
case 'W':
if ( globalUtilOptind >= argc )
{
fprintf( pErr, "Command line switch \"-W\" should be followed by an integer.\n" );
goto usage;
}
pPars->nWinTfoLevs = atoi(argv[globalUtilOptind]);
globalUtilOptind++;
if ( pPars->nWinTfoLevs < 1 || pPars->nWinTfoLevs > 99 )
goto usage;
break;
case 'F':
if ( globalUtilOptind >= argc )
{
fprintf( pErr, "Command line switch \"-F\" should be followed by an integer.\n" );
goto usage;
}
pPars->nFanoutsMax = atoi(argv[globalUtilOptind]);
globalUtilOptind++;
if ( pPars->nFanoutsMax < 1 )
goto usage;
break;
case 'L':
if ( globalUtilOptind >= argc )
{
fprintf( pErr, "Command line switch \"-L\" should be followed by an integer.\n" );
goto usage;
}
pPars->nGrowthLevel = atoi(argv[globalUtilOptind]);
globalUtilOptind++;
if ( pPars->nGrowthLevel < 0 || pPars->nGrowthLevel > ABC_INFINITY )
goto usage;
break;
case 'a':
pPars->fArea ^= 1;
break;
case 'v':
pPars->fVerbose ^= 1;
break;
case 'w':
pPars->fVeryVerbose ^= 1;
break;
case 'h':
goto usage;
default:
goto usage;
}
}
if ( pNtk == NULL )
{
fprintf( pErr, "Empty network.\n" );
return 1;
}
if ( !Abc_NtkIsLogic(pNtk) )
{
fprintf( pErr, "This command can only be applied to a logic network.\n" );
return 1;
}
// modify the current network
if ( !Abc_NtkMfs( pNtk, pPars ) )
{
fprintf( pErr, "Resynthesis has failed.\n" );
return 1;
}
return 0;
usage:
fprintf( pErr, "usage: mfs [-W <num>] [-F <num>] [-L <num>] [-vh]\n" );
fprintf( pErr, "\t performs don't-care-based optimization of logic networks\n" );
fprintf( pErr, "\t-W <num> : the number of levels in the TFO cone (0 <= NM <= 100) [default = %d]\n", pPars->nWinTfoLevs );
fprintf( pErr, "\t-F <num> : the max number of fanouts to skip (1 <= n) [default = %d]\n", pPars->nFanoutsMax );
fprintf( pErr, "\t-L <num> : the largest increase in node level after resynthesis (0 <= num) [default = %d]\n", pPars->nGrowthLevel );
// fprintf( pErr, "\t-a : toggle optimization for area only [default = %s]\n", pPars->fArea? "yes": "no" );
fprintf( pErr, "\t-v : toggle verbose printout [default = %s]\n", pPars->fVerbose? "yes": "no" );
// fprintf( pErr, "\t-w : toggle printout subgraph statistics [default = %s]\n", pPars->fVeryVerbose? "yes": "no" );
fprintf( pErr, "\t-h : print the command usage\n");
return 1;
}
/**Function*************************************************************
@ -11552,10 +11681,12 @@ int Abc_CommandSeqSweep( Abc_Frame_t * pAbc, int argc, char ** argv )
int nMaxLevs;
int fUseImps;
int fRewrite;
int fFraiging;
int fLatchCorr;
int fWriteImps;
int fUse1Hot;
int fVerbose;
extern Abc_Ntk_t * Abc_NtkDarSeqSweep( Abc_Ntk_t * pNtk, int nFramesP, int nFrames, int nMaxImps, int nMaxLevs, int fRewrite, int fUseImps, int fLatchCorr, int fWriteImps, int fVerbose );
extern Abc_Ntk_t * Abc_NtkDarSeqSweep( Abc_Ntk_t * pNtk, int nFramesP, int nFrames, int nMaxImps, int nMaxLevs, int fRewrite, int fFraiging, int fUseImps, int fLatchCorr, int fWriteImps, int fUse1Hot, int fVerbose );
pNtk = Abc_FrameReadNtk(pAbc);
pOut = Abc_FrameReadOut(pAbc);
@ -11568,11 +11699,13 @@ int Abc_CommandSeqSweep( Abc_Frame_t * pAbc, int argc, char ** argv )
nMaxLevs = 0;
fUseImps = 0;
fRewrite = 0;
fFraiging = 0;
fLatchCorr = 0;
fWriteImps = 0;
fUse1Hot = 0;
fVerbose = 0;
Extra_UtilGetoptReset();
while ( ( c = Extra_UtilGetopt( argc, argv, "PFILirlevh" ) ) != EOF )
while ( ( c = Extra_UtilGetopt( argc, argv, "PFILirfletvh" ) ) != EOF )
{
switch ( c )
{
@ -11626,12 +11759,18 @@ int Abc_CommandSeqSweep( Abc_Frame_t * pAbc, int argc, char ** argv )
case 'r':
fRewrite ^= 1;
break;
case 'f':
fFraiging ^= 1;
break;
case 'l':
fLatchCorr ^= 1;
break;
case 'e':
fWriteImps ^= 1;
break;
case 't':
fUse1Hot ^= 1;
break;
case 'v':
fVerbose ^= 1;
break;
@ -11660,8 +11799,20 @@ int Abc_CommandSeqSweep( Abc_Frame_t * pAbc, int argc, char ** argv )
return 0;
}
if ( nFramesK > 1 && fUse1Hot )
{
printf( "Currrently can only use one-hotness for simple induction (K=1).\n" );
return 0;
}
if ( nFramesP && fUse1Hot )
{
printf( "Currrently can only use one-hotness without prefix.\n" );
return 0;
}
// get the new network
pNtkRes = Abc_NtkDarSeqSweep( pNtk, nFramesP, nFramesK, nMaxImps, nMaxLevs, fRewrite, fUseImps, fLatchCorr, fWriteImps, fVerbose );
pNtkRes = Abc_NtkDarSeqSweep( pNtk, nFramesP, nFramesK, nMaxImps, nMaxLevs, fRewrite, fFraiging, fUseImps, fLatchCorr, fWriteImps, fUse1Hot, fVerbose );
if ( pNtkRes == NULL )
{
fprintf( pErr, "Sequential sweeping has failed.\n" );
@ -11672,7 +11823,7 @@ int Abc_CommandSeqSweep( Abc_Frame_t * pAbc, int argc, char ** argv )
return 0;
usage:
fprintf( pErr, "usage: ssweep [-P num] [-F num] [-I num] [-ilrevh]\n" );
fprintf( pErr, "usage: ssweep [-P num] [-F num] [-I num] [-ilrfetvh]\n" );
fprintf( pErr, "\t performs sequential sweep using K-step induction\n" );
fprintf( pErr, "\t-P num : number of time frames to use as the prefix [default = %d]\n", nFramesP );
fprintf( pErr, "\t-F num : number of time frames for induction (1=simple) [default = %d]\n", nFramesK );
@ -11681,7 +11832,9 @@ usage:
fprintf( pErr, "\t-i : toggle using implications [default = %s]\n", fUseImps? "yes": "no" );
fprintf( pErr, "\t-l : toggle latch correspondence only [default = %s]\n", fLatchCorr? "yes": "no" );
fprintf( pErr, "\t-r : toggle AIG rewriting [default = %s]\n", fRewrite? "yes": "no" );
fprintf( pErr, "\t-f : toggle fraiging (combinational SAT sweeping) [default = %s]\n", fFraiging? "yes": "no" );
fprintf( pErr, "\t-e : toggle writing implications as assertions [default = %s]\n", fWriteImps? "yes": "no" );
fprintf( pErr, "\t-t : toggle using one-hotness conditions [default = %s]\n", fUse1Hot? "yes": "no" );
fprintf( pErr, "\t-v : toggle verbose output [default = %s]\n", fVerbose? "yes": "no" );
fprintf( pErr, "\t-h : print the command usage\n");
return 1;
@ -13376,7 +13529,7 @@ int Abc_CommandBmc( Abc_Frame_t * pAbc, int argc, char ** argv )
usage:
fprintf( pErr, "usage: bmc [-F num] [-C num] [-rvh]\n" );
fprintf( pErr, "\t perform bounded model checking\n" );
fprintf( pErr, "\t-F num : number of time frames [default = %d]\n", nFrames );
fprintf( pErr, "\t-F num : the number of time frames [default = %d]\n", nFrames );
fprintf( pErr, "\t-C num : the max number of conflicts at a node [default = %d]\n", nBTLimit );
fprintf( pErr, "\t-r : toggle initialization of the first frame [default = %s]\n", fRewrite? "yes": "no" );
fprintf( pErr, "\t-v : toggle verbose output [default = %s]\n", fVerbose? "yes": "no" );

37
src/base/abci/abcDar.c
View File

@ -184,6 +184,11 @@ Abc_Ntk_t * Abc_NtkFromDar( Abc_Ntk_t * pNtkOld, Aig_Man_t * pMan )
Abc_ObjAssignName( pObjNew, "assert_", Abc_ObjName(pObjNew) );
Abc_ObjAddFanin( pObjNew, (Abc_Obj_t *)Aig_ObjChild0Copy(pObj) );
}
if ( pMan->pManExdc )
{
pNtkNew->pManExdc = pMan->pManExdc;
pMan->pManExdc = NULL;
}
if ( !Abc_NtkCheck( pNtkNew ) )
fprintf( stdout, "Abc_NtkFromDar(): Network check has failed.\n" );
return pNtkNew;
@ -1022,7 +1027,7 @@ PRT( "Time", clock() - clkTotal );
SeeAlso []
***********************************************************************/
Abc_Ntk_t * Abc_NtkDarSeqSweep( Abc_Ntk_t * pNtk, int nFramesP, int nFramesK, int nMaxImps, int nMaxLevs, int fRewrite, int fUseImps, int fLatchCorr, int fWriteImps, int fVerbose )
Abc_Ntk_t * Abc_NtkDarSeqSweep( Abc_Ntk_t * pNtk, int nFramesP, int nFramesK, int nMaxImps, int nMaxLevs, int fRewrite, int fFraiging, int fUseImps, int fLatchCorr, int fWriteImps, int fUse1Hot, int fVerbose )
{
Fraig_Params_t Params;
Abc_Ntk_t * pNtkAig, * pNtkFraig;
@ -1034,8 +1039,10 @@ Abc_Ntk_t * Abc_NtkDarSeqSweep( Abc_Ntk_t * pNtk, int nFramesP, int nFramesK, in
// so fraiging does not reduce the number of functions represented by nodes
Fraig_ParamsSetDefault( &Params );
Params.nBTLimit = 100000;
// pNtkFraig = Abc_NtkFraig( pNtk, &Params, 0, 0 );
pNtkFraig = Abc_NtkDup( pNtk );
if ( fFraiging )
pNtkFraig = Abc_NtkFraig( pNtk, &Params, 0, 0 );
else
pNtkFraig = Abc_NtkDup( pNtk );
if ( fVerbose )
{
PRT( "Initial fraiging time", clock() - clk );
@ -1046,7 +1053,7 @@ PRT( "Initial fraiging time", clock() - clk );
if ( pMan == NULL )
return NULL;
pMan = Fra_FraigInduction( pTemp = pMan, nFramesP, nFramesK, nMaxImps, nMaxLevs, fRewrite, fUseImps, fLatchCorr, fWriteImps, fVerbose, NULL );
pMan = Fra_FraigInduction( pTemp = pMan, nFramesP, nFramesK, nMaxImps, nMaxLevs, fRewrite, fUseImps, fLatchCorr, fWriteImps, fUse1Hot, fVerbose, NULL );
Aig_ManStop( pTemp );
if ( Aig_ManRegNum(pMan) < Abc_NtkLatchNum(pNtk) )
@ -1530,6 +1537,28 @@ Abc_Ntk_t * Abc_NtkInter( Abc_Ntk_t * pNtkOn, Abc_Ntk_t * pNtkOff, int fVerbose
return pNtkAig;
}
/**Function*************************************************************
Synopsis [Interplates two networks.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
void Abc_NtkPrintSccs( Abc_Ntk_t * pNtk, int fVerbose )
{
Aig_Man_t * pMan;
pMan = Abc_NtkToDar( pNtk, 1 );
if ( pMan == NULL )
return;
Aig_ManComputeSccs( pMan );
Aig_ManStop( pMan );
}
#include "ntl.h"

10
src/base/abci/abcPrint.c
View File

@ -322,11 +322,11 @@ void Abc_NtkPrintLatch( FILE * pFile, Abc_Ntk_t * pNtk )
Counter2++;
}
}
fprintf( pFile, "%-15s: ", pNtk->pName );
fprintf( pFile, "Latch = %6d. No = %4d. Zero = %4d. One = %4d. DC = %4d.\n",
Abc_NtkLatchNum(pNtk), InitNums[0], InitNums[1], InitNums[2], InitNums[3] );
fprintf( pFile, "Const fanin = %3d. DC init = %3d. Matching init = %3d. ", Counter0, Counter1, Counter2 );
fprintf( pFile, "Self-feed latches = %2d.\n", -1 ); //Abc_NtkCountSelfFeedLatches(pNtk) );
// fprintf( pFile, "%-15s: ", pNtk->pName );
fprintf( pFile, "Total latches = %5d. Init0 = %d. Init1 = %d. InitDC = %d. Const data = %d.\n",
Abc_NtkLatchNum(pNtk), InitNums[1], InitNums[2], InitNums[3], Counter0 );
// fprintf( pFile, "Const fanin = %3d. DC init = %3d. Matching init = %3d. ", Counter0, Counter1, Counter2 );
// fprintf( pFile, "Self-feed latches = %2d.\n", -1 ); //Abc_NtkCountSelfFeedLatches(pNtk) );
}
/**Function*************************************************************

0
src/map/pcm/module.make Normal file
View File

0
src/map/ply/module.make Normal file
View File

73
src/opt/mfs/mfs.h Normal file
View File

@ -0,0 +1,73 @@
/**CFile****************************************************************
FileName [mfs.h]
SystemName [ABC: Logic synthesis and verification system.]
PackageName [The good old minimization with complete don't-cares.]
Synopsis [External declarations.]
Author [Alan Mishchenko]
Affiliation [UC Berkeley]
Date [Ver. 1.0. Started - June 20, 2005.]
Revision [$Id: mfs.h,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
***********************************************************************/
#ifndef __MFS_H__
#define __MFS_H__
#ifdef __cplusplus
extern "C" {
#endif
////////////////////////////////////////////////////////////////////////
/// INCLUDES ///
////////////////////////////////////////////////////////////////////////
////////////////////////////////////////////////////////////////////////
/// PARAMETERS ///
////////////////////////////////////////////////////////////////////////
////////////////////////////////////////////////////////////////////////
/// BASIC TYPES ///
////////////////////////////////////////////////////////////////////////
typedef struct Mfs_Par_t_ Mfs_Par_t;
struct Mfs_Par_t_
{
// general parameters
int nWinTfoLevs; // the maximum fanout levels
int nFanoutsMax; // the maximum number of fanouts
int nGrowthLevel; // the maximum allowed growth in level after one iteration of resynthesis
int fArea; // performs optimization for area
int fDelay; // performs optimization for delay
int fVerbose; // enable basic stats
int fVeryVerbose; // enable detailed stats
};
////////////////////////////////////////////////////////////////////////
/// MACRO DEFINITIONS ///
////////////////////////////////////////////////////////////////////////
////////////////////////////////////////////////////////////////////////
/// FUNCTION DECLARATIONS ///
////////////////////////////////////////////////////////////////////////
/*=== mfsCore.c ==========================================================*/
extern int Abc_NtkMfs( Abc_Ntk_t * pNtk, Mfs_Par_t * pPars );
#ifdef __cplusplus
}
#endif
#endif
////////////////////////////////////////////////////////////////////////
/// END OF FILE ///
////////////////////////////////////////////////////////////////////////

143
src/opt/mfs/mfsCore.c Normal file
View File

@ -0,0 +1,143 @@
/**CFile****************************************************************
FileName [mfsCore.c]
SystemName [ABC: Logic synthesis and verification system.]
PackageName [The good old minimization with complete don't-cares.]
Synopsis []
Author [Alan Mishchenko]
Affiliation [UC Berkeley]
Date [Ver. 1.0. Started - June 20, 2005.]
Revision [$Id: mfsCore.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
***********************************************************************/
#include "mfsInt.h"
////////////////////////////////////////////////////////////////////////
/// DECLARATIONS ///
////////////////////////////////////////////////////////////////////////
////////////////////////////////////////////////////////////////////////
/// FUNCTION DEFINITIONS ///
////////////////////////////////////////////////////////////////////////
/**Function*************************************************************
Synopsis []
Description []
SideEffects []
SeeAlso []
***********************************************************************/
int Abc_NtkMfsNode( Mfs_Man_t * p, Abc_Obj_t * pNode )
{
int clk;
// prepare data structure for this node
Mfs_ManClean( p );
// compute window roots, window support, and window nodes
clk = clock();
p->vRoots = Abc_MfsComputeRoots( pNode, p->pPars->nWinTfoLevs, p->pPars->nFanoutsMax );
p->vSupp = Abc_NtkNodeSupport( p->pNtk, (Abc_Obj_t **)Vec_PtrArray(p->vRoots), Vec_PtrSize(p->vRoots) );
p->vNodes = Abc_NtkDfsNodes( p->pNtk, (Abc_Obj_t **)Vec_PtrArray(p->vRoots), Vec_PtrSize(p->vRoots) );
p->timeWin += clock() - clk;
// construct AIG for the window
clk = clock();
p->pAigWin = Abc_NtkConstructAig( p, pNode );
p->timeAig += clock() - clk;
// translate it into CNF
clk = clock();
p->pCnf = Cnf_DeriveSimple( p->pAigWin, Abc_ObjFaninNum(pNode) );
p->timeCnf += clock() - clk;
// create the SAT problem
clk = clock();
p->pSat = Cnf_DataWriteIntoSolver( p->pCnf, 1, 0 );
// solve the SAT problem
Abc_NtkMfsSolveSat( p, pNode );
p->timeSat += clock() - clk;
return 1;
}
/**Function*************************************************************
Synopsis []
Description []
SideEffects []
SeeAlso []
***********************************************************************/
int Abc_NtkMfs( Abc_Ntk_t * pNtk, Mfs_Par_t * pPars )
{
Mfs_Man_t * p;
Abc_Obj_t * pObj;
int i, Counter;
assert( Abc_NtkIsLogic(pNtk) );
if ( Abc_NtkGetFaninMax(pNtk) > MFS_FANIN_MAX )
{
printf( "Some nodes have more than %d fanins. Quitting.\n", MFS_FANIN_MAX );
return 1;
}
// perform the network sweep
Abc_NtkSweep( pNtk, 0 );
// convert into the AIG
if ( !Abc_NtkToAig(pNtk) )
{
fprintf( stdout, "Converting to BDD has failed.\n" );
return 0;
}
assert( Abc_NtkHasAig(pNtk) );
if ( pNtk->pManExdc != NULL )
printf( "Performing don't-care computation with don't-cares.\n" );
// start the manager
p = Mfs_ManAlloc();
p->pPars = pPars;
p->pNtk = pNtk;
p->pCare = pNtk->pManExdc;
// label the register outputs
if ( p->pCare )
{
Counter = 1;
Abc_NtkForEachCi( pNtk, pObj, i )
if ( Abc_ObjFaninNum(pObj) == 0 )
pObj->pData = NULL;
else
pObj->pData = (void *)Counter++;
assert( Counter == Abc_NtkLatchNum(pNtk) + 1 );
}
// compute don't-cares for each node
Abc_NtkForEachNode( pNtk, pObj, i )
Abc_NtkMfsNode( p, pObj );
// undo labesl
if ( p->pCare )
{
Abc_NtkForEachCi( pNtk, pObj, i )
pObj->pData = NULL;
}
// free the manager
Mfs_ManStop( p );
return 1;
}
////////////////////////////////////////////////////////////////////////
/// END OF FILE ///
////////////////////////////////////////////////////////////////////////

110
src/opt/mfs/mfsInt.h Normal file
View File

@ -0,0 +1,110 @@
/**CFile****************************************************************
FileName [mfsInt.h]
SystemName [ABC: Logic synthesis and verification system.]
PackageName [The good old minimization with complete don't-cares.]
Synopsis [Internal declarations.]
Author [Alan Mishchenko]
Affiliation [UC Berkeley]
Date [Ver. 1.0. Started - June 20, 2005.]
Revision [$Id: mfsInt.h,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
***********************************************************************/
#ifndef __MFS_INT_H__
#define __MFS_INT_H__
#ifdef __cplusplus
extern "C" {
#endif
////////////////////////////////////////////////////////////////////////
/// INCLUDES ///
////////////////////////////////////////////////////////////////////////
#include "abc.h"
#include "mfs.h"
#include "aig.h"
#include "cnf.h"
#include "satSolver.h"
////////////////////////////////////////////////////////////////////////
/// PARAMETERS ///
////////////////////////////////////////////////////////////////////////
#define MFS_FANIN_MAX 10
typedef struct Mfs_Man_t_ Mfs_Man_t;
struct Mfs_Man_t_
{
// input data
Mfs_Par_t * pPars;
Abc_Ntk_t * pNtk;
Aig_Man_t * pCare;
// intermeditate data for the node
Vec_Ptr_t * vRoots; // the roots of the window
Vec_Ptr_t * vSupp; // the support of the window
Vec_Ptr_t * vNodes; // the internal nodes of the window
Vec_Int_t * vProjVars; // the projection variables
// solving data
Aig_Man_t * pAigWin; // window AIG with constraints
Cnf_Dat_t * pCnf; // the CNF for the window
sat_solver * pSat; // the SAT solver used
// the result of solving
int nFanins; // the number of fanins
int nWords; // the number of words
int nCares; // the number of care minterms
unsigned uCare[(MFS_FANIN_MAX<=5)?1:1<<(MFS_FANIN_MAX-5)]; // the computed care-set
// performance statistics
int nNodesTried;
int nNodesBad;
int nMintsCare;
int nMintsTotal;
// statistics
int timeWin;
int timeAig;
int timeCnf;
int timeSat;
};
////////////////////////////////////////////////////////////////////////
/// BASIC TYPES ///
////////////////////////////////////////////////////////////////////////
////////////////////////////////////////////////////////////////////////
/// MACRO DEFINITIONS ///
////////////////////////////////////////////////////////////////////////
////////////////////////////////////////////////////////////////////////
/// FUNCTION DECLARATIONS ///
////////////////////////////////////////////////////////////////////////
/*=== mfsMan.c ==========================================================*/
extern Mfs_Man_t * Mfs_ManAlloc();
extern void Mfs_ManStop( Mfs_Man_t * p );
extern void Mfs_ManClean( Mfs_Man_t * p );
/*=== mfsSat.c ==========================================================*/
extern void Abc_NtkMfsSolveSat( Mfs_Man_t * p, Abc_Obj_t * pNode );
/*=== mfsStrash.c ==========================================================*/
extern Aig_Man_t * Abc_NtkConstructAig( Mfs_Man_t * p, Abc_Obj_t * pNode );
/*=== mfsWin.c ==========================================================*/
extern Vec_Ptr_t * Abc_MfsComputeRoots( Abc_Obj_t * pNode, int nWinTfoMax, int nFanoutLimit );
#ifdef __cplusplus
}
#endif
#endif
////////////////////////////////////////////////////////////////////////
/// END OF FILE ///
////////////////////////////////////////////////////////////////////////

132
src/opt/mfs/mfsMan.c Normal file
View File

@ -0,0 +1,132 @@
/**CFile****************************************************************
FileName [mfsMan.c]
SystemName [ABC: Logic synthesis and verification system.]
PackageName [The good old minimization with complete don't-cares.]
Synopsis [Procedure to manipulation the manager.]
Author [Alan Mishchenko]
Affiliation [UC Berkeley]
Date [Ver. 1.0. Started - June 20, 2005.]
Revision [$Id: mfsMan.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
***********************************************************************/
#include "mfsInt.h"
////////////////////////////////////////////////////////////////////////
/// DECLARATIONS ///
////////////////////////////////////////////////////////////////////////
////////////////////////////////////////////////////////////////////////
/// FUNCTION DEFINITIONS ///
////////////////////////////////////////////////////////////////////////
/**Function*************************************************************
Synopsis []
Description []
SideEffects []
SeeAlso []
***********************************************************************/
Mfs_Man_t * Mfs_ManAlloc()
{
Mfs_Man_t * p;
// start the manager
p = ALLOC( Mfs_Man_t, 1 );
memset( p, 0, sizeof(Mfs_Man_t) );
p->vProjVars = Vec_IntAlloc( 100 );
return p;
}
/**Function*************************************************************
Synopsis []
Description []
SideEffects []
SeeAlso []
***********************************************************************/
void Mfs_ManClean( Mfs_Man_t * p )
{
if ( p->pAigWin )
Aig_ManStop( p->pAigWin );
if ( p->pCnf )
Cnf_DataFree( p->pCnf );
if ( p->pSat )
sat_solver_delete( p->pSat );
if ( p->vRoots )
Vec_PtrFree( p->vRoots );
if ( p->vSupp )
Vec_PtrFree( p->vSupp );
if ( p->vNodes )
Vec_PtrFree( p->vNodes );
p->pAigWin = NULL;
p->pCnf = NULL;
p->pSat = NULL;
p->vRoots = NULL;
p->vSupp = NULL;
p->vNodes = NULL;
}
/**Function*************************************************************
Synopsis []
Description []
SideEffects []
SeeAlso []
***********************************************************************/
void Mfs_ManPrint( Mfs_Man_t * p )
{
printf( "Nodes tried = %d. Bad nodes = %d.\n",
p->nNodesTried, p->nNodesBad );
printf( "Total mints = %d. Care mints = %d. Ratio = %5.2f.\n",
p->nMintsTotal, p->nMintsCare, 1.0 * p->nMintsCare / p->nMintsTotal );
PRT( "Win", p->timeWin );
PRT( "Aig", p->timeAig );
PRT( "Cnf", p->timeCnf );
PRT( "Sat", p->timeSat );
}
/**Function*************************************************************
Synopsis []
Description []
SideEffects []
SeeAlso []
***********************************************************************/
void Mfs_ManStop( Mfs_Man_t * p )
{
Mfs_ManPrint( p );
Mfs_ManClean( p );
Vec_IntFree( p->vProjVars );
free( p );
}
////////////////////////////////////////////////////////////////////////
/// END OF FILE ///
////////////////////////////////////////////////////////////////////////

113
src/opt/mfs/mfsSat.c Normal file
View File

@ -0,0 +1,113 @@
/**CFile****************************************************************
FileName [mfsSat.c]
SystemName [ABC: Logic synthesis and verification system.]
PackageName [The good old minimization with complete don't-cares.]
Synopsis []
Author [Alan Mishchenko]
Affiliation [UC Berkeley]
Date [Ver. 1.0. Started - June 20, 2005.]
Revision [$Id: mfsSat.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
***********************************************************************/
#include "mfsInt.h"
////////////////////////////////////////////////////////////////////////
/// DECLARATIONS ///
////////////////////////////////////////////////////////////////////////
////////////////////////////////////////////////////////////////////////
/// FUNCTION DEFINITIONS ///
////////////////////////////////////////////////////////////////////////
/**Function*************************************************************
Synopsis [Enumerates through the SAT assignments.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
int Abc_NtkMfsSolveSat_iter( Mfs_Man_t * p )
{
int Lits[MFS_FANIN_MAX];
int RetValue, iVar, b, Mint;
RetValue = sat_solver_solve( p->pSat, NULL, NULL, (sint64)10000, (sint64)0, (sint64)0, (sint64)0 );
if ( RetValue != l_True )
return 0;
// add SAT assignment to the solver
Mint = 0;
Vec_IntForEachEntry( p->vProjVars, iVar, b )
{
Lits[b] = toLit( iVar );
if ( sat_solver_var_value( p->pSat, iVar ) )
{
Mint |= (1 << b);
Lits[b] = lit_neg( Lits[b] );
}
}
assert( !Aig_InfoHasBit(p->uCare, Mint) );
Aig_InfoSetBit( p->uCare, Mint );
// add the blocking clause
RetValue = sat_solver_addclause( p->pSat, Lits, Lits + Vec_IntSize(p->vProjVars) );
if ( RetValue == 0 )
return 0;
return 1;
}
/**Function*************************************************************
Synopsis [Enumerates through the SAT assignments.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
void Abc_NtkMfsSolveSat( Mfs_Man_t * p, Abc_Obj_t * pNode )
{
Aig_Obj_t * pObjPo;
int i;
// collect projection variables
Vec_IntClear( p->vProjVars );
Vec_PtrForEachEntryStart( p->pAigWin->vPos, pObjPo, i, Aig_ManPoNum(p->pAigWin) - Abc_ObjFaninNum(pNode) )
{
assert( p->pCnf->pVarNums[pObjPo->Id] >= 0 );
Vec_IntPush( p->vProjVars, p->pCnf->pVarNums[pObjPo->Id] );
}
// prepare the truth table of care set
p->nFanins = Vec_IntSize( p->vProjVars );
p->nWords = Aig_TruthWordNum( p->nFanins );
memset( p->uCare, 0, sizeof(unsigned) * p->nWords );
// iterate through the SAT assignments
while ( Abc_NtkMfsSolveSat_iter( p ) );
// write statistics
p->nCares = 0;
for ( i = 0; i < p->nWords; i++ )
p->nCares += Aig_WordCountOnes( p->uCare[i] );
p->nMintsCare += p->nCares;
p->nMintsTotal += 32 * p->nWords;
}
////////////////////////////////////////////////////////////////////////
/// END OF FILE ///
////////////////////////////////////////////////////////////////////////

224
src/opt/mfs/mfsStrash.c Normal file
View File

@ -0,0 +1,224 @@
/**CFile****************************************************************
FileName [mfsStrash.c]
SystemName [ABC: Logic synthesis and verification system.]
PackageName [The good old minimization with complete don't-cares.]
Synopsis [Structural hashing of the window with ODCs.]
Author [Alan Mishchenko]
Affiliation [UC Berkeley]
Date [Ver. 1.0. Started - June 20, 2005.]
Revision [$Id: mfsStrash.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
***********************************************************************/
#include "mfsInt.h"
////////////////////////////////////////////////////////////////////////
/// DECLARATIONS ///
////////////////////////////////////////////////////////////////////////
////////////////////////////////////////////////////////////////////////
/// FUNCTION DEFINITIONS ///
////////////////////////////////////////////////////////////////////////
/**Function*************************************************************
Synopsis [Construct BDDs and mark AIG nodes.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
void Abc_MfsConvertHopToAig_rec( Hop_Obj_t * pObj, Aig_Man_t * pMan )
{
assert( !Hop_IsComplement(pObj) );
if ( !Hop_ObjIsNode(pObj) || Hop_ObjIsMarkA(pObj) )
return;
Abc_MfsConvertHopToAig_rec( Hop_ObjFanin0(pObj), pMan );
Abc_MfsConvertHopToAig_rec( Hop_ObjFanin1(pObj), pMan );
pObj->pData = Aig_And( pMan, (Aig_Obj_t *)Hop_ObjChild0Copy(pObj), (Aig_Obj_t *)Hop_ObjChild1Copy(pObj) );
assert( !Hop_ObjIsMarkA(pObj) ); // loop detection
Hop_ObjSetMarkA( pObj );
}
/**Function*************************************************************
Synopsis [Converts the network from AIG to BDD representation.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
void Abc_MfsConvertHopToAig( Abc_Obj_t * pObjOld, Aig_Man_t * pMan )
{
Hop_Man_t * pHopMan;
Hop_Obj_t * pRoot;
Abc_Obj_t * pFanin;
int i;
// get the local AIG
pHopMan = pObjOld->pNtk->pManFunc;
pRoot = pObjOld->pData;
// check the case of a constant
if ( Hop_ObjIsConst1( Hop_Regular(pRoot) ) )
{
pObjOld->pCopy = (Abc_Obj_t *)Aig_NotCond( Aig_ManConst1(pMan), Hop_IsComplement(pRoot) );
pObjOld->pNext = pObjOld->pCopy;
return;
}
// assign the fanin nodes
Abc_ObjForEachFanin( pObjOld, pFanin, i )
Hop_ManPi(pHopMan, i)->pData = pFanin->pCopy;
// construct the AIG
Abc_MfsConvertHopToAig_rec( Hop_Regular(pRoot), pMan );
pObjOld->pCopy = (Abc_Obj_t *)Aig_NotCond( Hop_Regular(pRoot)->pData, Hop_IsComplement(pRoot) );
Hop_ConeUnmark_rec( Hop_Regular(pRoot) );
// assign the fanin nodes
Abc_ObjForEachFanin( pObjOld, pFanin, i )
Hop_ManPi(pHopMan, i)->pData = pFanin->pNext;
// construct the AIG
Abc_MfsConvertHopToAig_rec( Hop_Regular(pRoot), pMan );
pObjOld->pNext = (Abc_Obj_t *)Aig_NotCond( Hop_Regular(pRoot)->pData, Hop_IsComplement(pRoot) );
Hop_ConeUnmark_rec( Hop_Regular(pRoot) );
}
/**Function*************************************************************
Synopsis [Computes the care set of the node under ODCs.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
Aig_Obj_t * Abc_NtkConstructAig_rec( Mfs_Man_t * p, Abc_Obj_t * pNode, Aig_Man_t * pMan )
{
Aig_Obj_t * pRoot, * pExor;
Abc_Obj_t * pObj;
int i;
// assign AIG nodes to the leaves
Vec_PtrForEachEntry( p->vSupp, pObj, i )
pObj->pCopy = pObj->pNext = (Abc_Obj_t *)Aig_ObjCreatePi( pMan );
// strash intermediate nodes
Abc_NtkIncrementTravId( pNode->pNtk );
Vec_PtrForEachEntry( p->vNodes, pObj, i )
{
Abc_MfsConvertHopToAig( pObj, pMan );
if ( pObj == pNode )
pObj->pNext = Abc_ObjNot(pObj->pNext);
}
// create the observability condition
pRoot = Aig_ManConst0(pMan);
Vec_PtrForEachEntry( p->vRoots, pObj, i )
{
pExor = Aig_Exor( pMan, (Aig_Obj_t *)pObj->pCopy, (Aig_Obj_t *)pObj->pNext );
pRoot = Aig_Or( pMan, pRoot, pExor );
}
return pRoot;
}
/**Function*************************************************************
Synopsis [Adds relevant constraints.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
Aig_Obj_t * Abc_NtkConstructCare_rec( Mfs_Man_t * p, Aig_Obj_t * pObj, Aig_Man_t * pMan )
{
Aig_Obj_t * pObj0, * pObj1;
if ( Aig_ObjIsTravIdCurrent( pMan, pObj ) )
return pObj->pData;
Aig_ObjSetTravIdCurrent( pMan, pObj );
if ( Aig_ObjIsPi(pObj) )
return pObj->pData = NULL;
pObj0 = Abc_NtkConstructCare_rec( p, Aig_ObjFanin0(pObj), pMan );
if ( pObj0 == NULL )
return pObj->pData = NULL;
pObj1 = Abc_NtkConstructCare_rec( p, Aig_ObjFanin1(pObj), pMan );
if ( pObj1 == NULL )
return pObj->pData = NULL;
pObj0 = Aig_NotCond( pObj0, Aig_ObjFaninC0(pObj) );
pObj1 = Aig_NotCond( pObj1, Aig_ObjFaninC1(pObj) );
return pObj->pData = Aig_And( pMan, pObj0, pObj1 );
}
/**Function*************************************************************
Synopsis [Creates AIG for the window with constraints.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
Aig_Man_t * Abc_NtkConstructAig( Mfs_Man_t * p, Abc_Obj_t * pNode )
{
Aig_Man_t * pMan;
Abc_Obj_t * pFanin;
Aig_Obj_t * pObjAig, * pPi, * pPo;
int i;
// start the new manager
pMan = Aig_ManStart( 1000 );
// construct the root node's AIG cone
pObjAig = Abc_NtkConstructAig_rec( p, pNode, pMan );
Aig_ObjCreatePo( pMan, pObjAig );
if ( p->pCare )
{
// mark the care set
Aig_ManIncrementTravId( p->pCare );
Vec_PtrForEachEntry( p->vSupp, pFanin, i )
{
if ( pFanin->pData == NULL )
continue;
pPi = Aig_ManPi( p->pCare, ((int)pFanin->pData) - 1 );
Aig_ObjSetTravIdCurrent( p->pCare, pPi );
pPi->pData = pFanin->pCopy;
}
// construct the constraints
Aig_ManForEachPo( p->pCare, pPo, i )
{
pObjAig = Abc_NtkConstructCare_rec( p, Aig_ObjFanin0(pPo), pMan );
if ( pObjAig == NULL )
continue;
pObjAig = Aig_NotCond( pObjAig, Aig_ObjFaninC0(pPo) );
Aig_ObjCreatePo( pMan, pObjAig );
}
}
// construct the fanins
Abc_ObjForEachFanin( pNode, pFanin, i )
{
pObjAig = (Aig_Obj_t *)pFanin->pCopy;
Aig_ObjCreatePo( pMan, pObjAig );
}
Aig_ManCleanup( pMan );
return pMan;
}
////////////////////////////////////////////////////////////////////////
/// END OF FILE ///
////////////////////////////////////////////////////////////////////////

112
src/opt/mfs/mfsWin.c Normal file
View File

@ -0,0 +1,112 @@
/**CFile****************************************************************
FileName [mfsWin.c]
SystemName [ABC: Logic synthesis and verification system.]
PackageName [The good old minimization with complete don't-cares.]
Synopsis []
Author [Alan Mishchenko]
Affiliation [UC Berkeley]
Date [Ver. 1.0. Started - June 20, 2005.]
Revision [$Id: mfsWin.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
***********************************************************************/
#include "mfsInt.h"
////////////////////////////////////////////////////////////////////////
/// DECLARATIONS ///
////////////////////////////////////////////////////////////////////////
////////////////////////////////////////////////////////////////////////
/// FUNCTION DEFINITIONS ///
////////////////////////////////////////////////////////////////////////
/**Function*************************************************************
Synopsis [Returns 1 if the node should be a root.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
static inline int Abc_MfsComputeRootsCheck( Abc_Obj_t * pNode, int nLevelMax, int nFanoutLimit )
{
Abc_Obj_t * pFanout;
int i;
// the node is the root if one of the following is true:
// (1) the node has more than fanouts than the limit
if ( Abc_ObjFanoutNum(pNode) > nFanoutLimit )
return 1;
// (2) the node has CO fanouts
// (3) the node has fanouts above the cutoff level
Abc_ObjForEachFanout( pNode, pFanout, i )
if ( Abc_ObjIsCo(pFanout) || (int)pFanout->Level > nLevelMax )
return 1;
return 0;
}
/**Function*************************************************************
Synopsis [Recursively collects the root candidates.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
void Abc_MfsComputeRoots_rec( Abc_Obj_t * pNode, int nLevelMax, int nFanoutLimit, Vec_Ptr_t * vRoots )
{
Abc_Obj_t * pFanout;
int i;
assert( Abc_ObjIsNode(pNode) );
if ( Abc_NodeIsTravIdCurrent(pNode) )
return;
Abc_NodeSetTravIdCurrent( pNode );
// check if the node should be the root
if ( Abc_MfsComputeRootsCheck( pNode, nLevelMax, nFanoutLimit ) )
Vec_PtrPush( vRoots, pNode );
else // if not, explore its fanouts
Abc_ObjForEachFanout( pNode, pFanout, i )
Abc_MfsComputeRoots_rec( pFanout, nLevelMax, nFanoutLimit, vRoots );
}
/**Function*************************************************************
Synopsis [Recursively collects the root candidates.]
Description [Returns 1 if the only root is this node.]
SideEffects []
SeeAlso []
***********************************************************************/
Vec_Ptr_t * Abc_MfsComputeRoots( Abc_Obj_t * pNode, int nWinTfoMax, int nFanoutLimit )
{
Vec_Ptr_t * vRoots;
vRoots = Vec_PtrAlloc( 10 );
Abc_NtkIncrementTravId( pNode->pNtk );
Abc_MfsComputeRoots_rec( pNode, pNode->Level + nWinTfoMax, nFanoutLimit, vRoots );
assert( Vec_PtrSize(vRoots) > 0 );
// if ( Vec_PtrSize(vRoots) == 1 && Vec_PtrEntry(vRoots, 0) == pNode )
// return 0;
return vRoots;
}
////////////////////////////////////////////////////////////////////////
/// END OF FILE ///
////////////////////////////////////////////////////////////////////////

47
src/opt/mfs/mfs_.c Normal file
View File

@ -0,0 +1,47 @@
/**CFile****************************************************************
FileName [mfs_.c]
SystemName [ABC: Logic synthesis and verification system.]
PackageName [The good old minimization with complete don't-cares.]
Synopsis []
Author [Alan Mishchenko]
Affiliation [UC Berkeley]
Date [Ver. 1.0. Started - June 20, 2005.]
Revision [$Id: mfs_.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
***********************************************************************/
#include "mfsInt.h"
////////////////////////////////////////////////////////////////////////
/// DECLARATIONS ///
////////////////////////////////////////////////////////////////////////
////////////////////////////////////////////////////////////////////////
/// FUNCTION DEFINITIONS ///
////////////////////////////////////////////////////////////////////////
/**Function*************************************************************
Synopsis []
Description []
SideEffects []
SeeAlso []
***********************************************************************/
////////////////////////////////////////////////////////////////////////
/// END OF FILE ///
////////////////////////////////////////////////////////////////////////

5
src/opt/mfs/module.make Normal file
View File

@ -0,0 +1,5 @@
SRC += src/opt/mfs/mfsCore.c \
src/opt/mfs/mfsMan.c \
src/opt/mfs/mfsSat.c \
src/opt/mfs/mfsStrash.c \
src/opt/mfs/mfsWin.c

8
src/sat/bsat/satSolver.c
View File

@ -946,6 +946,7 @@ sat_solver* sat_solver_new(void)
veci_new(&s->stack);
veci_new(&s->model);
veci_new(&s->act_vars);
veci_new(&s->temp_clause);
// initialize arrays
s->wlists = 0;
@ -1020,6 +1021,7 @@ void sat_solver_delete(sat_solver* s)
veci_delete(&s->stack);
veci_delete(&s->model);
veci_delete(&s->act_vars);
veci_delete(&s->temp_clause);
free(s->binary);
// delete arrays
@ -1052,6 +1054,12 @@ bool sat_solver_addclause(sat_solver* s, lit* begin, lit* end)
lbool* values;
lit last;
veci_resize( &s->temp_clause, 0 );
for ( i = begin; i < end; i++ )
veci_push( &s->temp_clause, *i );
begin = veci_begin( &s->temp_clause );
end = begin + veci_size( &s->temp_clause );
if (begin == end) return false;
//printlits(begin,end); printf("\n");

2
src/sat/bsat/satSolver.h
View File

@ -187,6 +187,8 @@ struct sat_solver_t
FILE * pFile;
int nClauses;
int nRoots;
veci temp_clause; // temporary storage for a CNF clause
};
static int sat_solver_var_value( sat_solver* s, int v )