mirror of https://github.com/YosysHQ/abc.git
Version abc80725
This commit is contained in:
Alan Mishchenko
parent
2c96c8af36
commit
1afa8a2f38
3
Makefile
3
Makefile
|
|
@ -24,7 +24,8 @@ MODULES := \
|
||||||
src/aig/mem src/aig/dar src/aig/fra src/aig/cnf \
|
src/aig/mem src/aig/dar src/aig/fra src/aig/cnf \
|
||||||
src/aig/csw src/aig/ioa src/aig/aig src/aig/kit \
|
src/aig/csw src/aig/ioa src/aig/aig src/aig/kit \
|
||||||
src/aig/bdc src/aig/bar src/aig/ntl src/aig/nwk \
|
src/aig/bdc src/aig/bar src/aig/ntl src/aig/nwk \
|
||||||
src/aig/mfx src/aig/tim src/aig/saig src/aig/bbr
|
src/aig/mfx src/aig/tim src/aig/saig src/aig/bbr \
|
||||||
|
src/aig/int
|
||||||
|
|
||||||
default: $(PROG)
|
default: $(PROG)
|
||||||
|
|
||||||
|
|
|
||||||
54
abc.dsp
54
abc.dsp
|
|
@ -42,7 +42,7 @@ RSC=rc.exe
|
||||||
# PROP Ignore_Export_Lib 0
|
# PROP Ignore_Export_Lib 0
|
||||||
# PROP Target_Dir ""
|
# PROP Target_Dir ""
|
||||||
# ADD BASE CPP /nologo /W3 /GX /O2 /D "WIN32" /D "NDEBUG" /D "_CONSOLE" /D "_MBCS" /YX /FD /c
|
# 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/misc/bzlib" /I "src/misc/zlib" /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/sat/nsat" /I "src/sat/psat" /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/nwk" /I "src/aig/tim" /I "src/opt/mfs" /I "src/aig/mfx" /I "src/aig/saig" /I "src/aig/bbr" /D "WIN32" /D "NDEBUG" /D "_CONSOLE" /D "_MBCS" /D "__STDC__" /D ABC_DLL=DLLEXPORT /D "_CRT_SECURE_NO_DEPRECATE" /D "ABC_USE_LIBRARIES" /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/misc/bzlib" /I "src/misc/zlib" /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/sat/nsat" /I "src/sat/psat" /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/nwk" /I "src/aig/tim" /I "src/opt/mfs" /I "src/aig/mfx" /I "src/aig/saig" /I "src/aig/bbr" /I "src/aig/int" /D "WIN32" /D "NDEBUG" /D "_CONSOLE" /D "_MBCS" /D "__STDC__" /D ABC_DLL=DLLEXPORT /D "_CRT_SECURE_NO_DEPRECATE" /D "ABC_USE_LIBRARIES" /FR /YX /FD /c
|
||||||
# ADD BASE RSC /l 0x409 /d "NDEBUG"
|
# ADD BASE RSC /l 0x409 /d "NDEBUG"
|
||||||
# ADD RSC /l 0x409 /d "NDEBUG"
|
# ADD RSC /l 0x409 /d "NDEBUG"
|
||||||
BSC32=bscmake.exe
|
BSC32=bscmake.exe
|
||||||
|
|
@ -66,7 +66,7 @@ LINK32=link.exe
|
||||||
# PROP Ignore_Export_Lib 0
|
# PROP Ignore_Export_Lib 0
|
||||||
# PROP Target_Dir ""
|
# 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 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/misc/bzlib" /I "src/misc/zlib" /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/sat/nsat" /I "src/sat/psat" /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/nwk" /I "src/aig/tim" /I "src/opt/mfs" /I "src/aig/mfx" /I "src/aig/saig" /I "src/aig/bbr" /D "WIN32" /D "_DEBUG" /D "_CONSOLE" /D "_MBCS" /D "__STDC__" /D ABC_DLL=DLLEXPORT /D "_CRT_SECURE_NO_DEPRECATE" /D "ABC_USE_LIBRARIES" /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/misc/bzlib" /I "src/misc/zlib" /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/sat/nsat" /I "src/sat/psat" /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/nwk" /I "src/aig/tim" /I "src/opt/mfs" /I "src/aig/mfx" /I "src/aig/saig" /I "src/aig/bbr" /I "src/aig/int" /D "WIN32" /D "_DEBUG" /D "_CONSOLE" /D "_MBCS" /D "__STDC__" /D ABC_DLL=DLLEXPORT /D "_CRT_SECURE_NO_DEPRECATE" /D "ABC_USE_LIBRARIES" /FR /YX /FD /GZ /c
|
||||||
# SUBTRACT CPP /X
|
# SUBTRACT CPP /X
|
||||||
# ADD BASE RSC /l 0x409 /d "_DEBUG"
|
# ADD BASE RSC /l 0x409 /d "_DEBUG"
|
||||||
# ADD RSC /l 0x409 /d "_DEBUG"
|
# ADD RSC /l 0x409 /d "_DEBUG"
|
||||||
|
|
@ -3194,10 +3194,6 @@ SOURCE=.\src\aig\saig\saigHaig.c
|
||||||
# End Source File
|
# End Source File
|
||||||
# Begin Source File
|
# Begin Source File
|
||||||
|
|
||||||
SOURCE=.\src\aig\saig\saigInter.c
|
|
||||||
# End Source File
|
|
||||||
# Begin Source File
|
|
||||||
|
|
||||||
SOURCE=.\src\aig\saig\saigIoa.c
|
SOURCE=.\src\aig\saig\saigIoa.c
|
||||||
# End Source File
|
# End Source File
|
||||||
# Begin Source File
|
# Begin Source File
|
||||||
|
|
@ -3228,9 +3224,53 @@ SOURCE=.\src\aig\saig\saigScl.c
|
||||||
|
|
||||||
SOURCE=.\src\aig\saig\saigTrans.c
|
SOURCE=.\src\aig\saig\saigTrans.c
|
||||||
# End Source File
|
# End Source File
|
||||||
|
# End Group
|
||||||
|
# Begin Group "int"
|
||||||
|
|
||||||
|
# PROP Default_Filter ""
|
||||||
# Begin Source File
|
# Begin Source File
|
||||||
|
|
||||||
SOURCE=.\src\aig\saig\saigUnique.c
|
SOURCE=.\src\aig\int\int.h
|
||||||
|
# End Source File
|
||||||
|
# Begin Source File
|
||||||
|
|
||||||
|
SOURCE=.\src\aig\int\intContain.c
|
||||||
|
# End Source File
|
||||||
|
# Begin Source File
|
||||||
|
|
||||||
|
SOURCE=.\src\aig\int\intCore.c
|
||||||
|
# End Source File
|
||||||
|
# Begin Source File
|
||||||
|
|
||||||
|
SOURCE=.\src\aig\int\intDup.c
|
||||||
|
# End Source File
|
||||||
|
# Begin Source File
|
||||||
|
|
||||||
|
SOURCE=.\src\aig\int\intFrames.c
|
||||||
|
# End Source File
|
||||||
|
# Begin Source File
|
||||||
|
|
||||||
|
SOURCE=.\src\aig\int\intInt.h
|
||||||
|
# End Source File
|
||||||
|
# Begin Source File
|
||||||
|
|
||||||
|
SOURCE=.\src\aig\int\intInter.c
|
||||||
|
# End Source File
|
||||||
|
# Begin Source File
|
||||||
|
|
||||||
|
SOURCE=.\src\aig\int\intM114.c
|
||||||
|
# End Source File
|
||||||
|
# Begin Source File
|
||||||
|
|
||||||
|
SOURCE=.\src\aig\int\intM114p.c
|
||||||
|
# End Source File
|
||||||
|
# Begin Source File
|
||||||
|
|
||||||
|
SOURCE=.\src\aig\int\intMan.c
|
||||||
|
# End Source File
|
||||||
|
# Begin Source File
|
||||||
|
|
||||||
|
SOURCE=.\src\aig\int\intUtil.c
|
||||||
# End Source File
|
# End Source File
|
||||||
# End Group
|
# End Group
|
||||||
# End Group
|
# End Group
|
||||||
|
|
|
||||||
|
|
@ -486,7 +486,7 @@ extern Aig_Man_t * Aig_ManDupWithoutPos( Aig_Man_t * p );
|
||||||
extern Aig_Man_t * Aig_ManDupRepres( Aig_Man_t * p );
|
extern Aig_Man_t * Aig_ManDupRepres( Aig_Man_t * p );
|
||||||
extern Aig_Man_t * Aig_ManDupRepresDfs( Aig_Man_t * p );
|
extern Aig_Man_t * Aig_ManDupRepresDfs( Aig_Man_t * p );
|
||||||
extern Aig_Man_t * Aig_ManCreateMiter( Aig_Man_t * p1, Aig_Man_t * p2, int fImpl );
|
extern Aig_Man_t * Aig_ManCreateMiter( Aig_Man_t * p1, Aig_Man_t * p2, int fImpl );
|
||||||
extern Aig_Man_t * Aig_ManDupOneOutput( Aig_Man_t * p, int iPoNum );
|
extern Aig_Man_t * Aig_ManDupOneOutput( Aig_Man_t * p, int iPoNum, int fAddRegs );
|
||||||
/*=== aigFanout.c ==========================================================*/
|
/*=== aigFanout.c ==========================================================*/
|
||||||
extern void Aig_ObjAddFanout( Aig_Man_t * p, Aig_Obj_t * pObj, Aig_Obj_t * pFanout );
|
extern void Aig_ObjAddFanout( Aig_Man_t * p, Aig_Obj_t * pObj, Aig_Obj_t * pFanout );
|
||||||
extern void Aig_ObjRemoveFanout( Aig_Man_t * p, Aig_Obj_t * pObj, Aig_Obj_t * pFanout );
|
extern void Aig_ObjRemoveFanout( Aig_Man_t * p, Aig_Obj_t * pObj, Aig_Obj_t * pFanout );
|
||||||
|
|
|
||||||
|
|
@ -17,7 +17,7 @@
|
||||||
Revision [$Id: aigCheck.c,v 1.00 2007/04/28 00:00:00 alanmi Exp $]
|
Revision [$Id: aigCheck.c,v 1.00 2007/04/28 00:00:00 alanmi Exp $]
|
||||||
|
|
||||||
***********************************************************************/
|
***********************************************************************/
|
||||||
|
|
||||||
#include "aig.h"
|
#include "aig.h"
|
||||||
|
|
||||||
////////////////////////////////////////////////////////////////////////
|
////////////////////////////////////////////////////////////////////////
|
||||||
|
|
|
||||||
|
|
@ -905,7 +905,7 @@ Aig_Man_t * Aig_ManCreateMiter( Aig_Man_t * p1, Aig_Man_t * p2, int Oper )
|
||||||
SeeAlso []
|
SeeAlso []
|
||||||
|
|
||||||
***********************************************************************/
|
***********************************************************************/
|
||||||
Aig_Man_t * Aig_ManDupOneOutput( Aig_Man_t * p, int iPoNum )
|
Aig_Man_t * Aig_ManDupOneOutput( Aig_Man_t * p, int iPoNum, int fAddRegs )
|
||||||
{
|
{
|
||||||
Aig_Man_t * pNew;
|
Aig_Man_t * pNew;
|
||||||
Aig_Obj_t * pObj;
|
Aig_Obj_t * pObj;
|
||||||
|
|
@ -922,8 +922,8 @@ Aig_Man_t * Aig_ManDupOneOutput( Aig_Man_t * p, int iPoNum )
|
||||||
Aig_ManForEachPi( p, pObj, i )
|
Aig_ManForEachPi( p, pObj, i )
|
||||||
pObj->pData = Aig_ObjCreatePi( pNew );
|
pObj->pData = Aig_ObjCreatePi( pNew );
|
||||||
// set registers
|
// set registers
|
||||||
pNew->nRegs = p->nRegs;
|
pNew->nRegs = fAddRegs? p->nRegs : 0;
|
||||||
pNew->nTruePis = p->nTruePis;
|
pNew->nTruePis = fAddRegs? p->nTruePis : p->nTruePis + p->nRegs;
|
||||||
pNew->nTruePos = 1;
|
pNew->nTruePos = 1;
|
||||||
// duplicate internal nodes
|
// duplicate internal nodes
|
||||||
Aig_ManForEachNode( p, pObj, i )
|
Aig_ManForEachNode( p, pObj, i )
|
||||||
|
|
@ -932,8 +932,11 @@ Aig_Man_t * Aig_ManDupOneOutput( Aig_Man_t * p, int iPoNum )
|
||||||
pObj = Aig_ManPo( p, iPoNum );
|
pObj = Aig_ManPo( p, iPoNum );
|
||||||
Aig_ObjCreatePo( pNew, Aig_ObjChild0Copy(pObj) );
|
Aig_ObjCreatePo( pNew, Aig_ObjChild0Copy(pObj) );
|
||||||
// create register inputs with MUXes
|
// create register inputs with MUXes
|
||||||
Aig_ManForEachLiSeq( p, pObj, i )
|
if ( fAddRegs )
|
||||||
Aig_ObjCreatePo( pNew, Aig_ObjChild0Copy(pObj) );
|
{
|
||||||
|
Aig_ManForEachLiSeq( p, pObj, i )
|
||||||
|
Aig_ObjCreatePo( pNew, Aig_ObjChild0Copy(pObj) );
|
||||||
|
}
|
||||||
Aig_ManCleanup( pNew );
|
Aig_ManCleanup( pNew );
|
||||||
return pNew;
|
return pNew;
|
||||||
}
|
}
|
||||||
|
|
|
||||||
|
|
@ -60,9 +60,9 @@ static void Bar_ProgressClean( Bar_Progress_t * p );
|
||||||
Bar_Progress_t * Bar_ProgressStart( FILE * pFile, int nItemsTotal )
|
Bar_Progress_t * Bar_ProgressStart( FILE * pFile, int nItemsTotal )
|
||||||
{
|
{
|
||||||
Bar_Progress_t * p;
|
Bar_Progress_t * p;
|
||||||
// extern int Abc_FrameShowProgress( void * p );
|
extern int Abc_FrameShowProgress( void * p );
|
||||||
// extern void * Abc_FrameGetGlobalFrame();
|
extern void * Abc_FrameGetGlobalFrame();
|
||||||
// if ( !Abc_FrameShowProgress(Abc_FrameGetGlobalFrame()) ) return NULL;
|
if ( !Abc_FrameShowProgress(Abc_FrameGetGlobalFrame()) ) return NULL;
|
||||||
p = (Bar_Progress_t *) malloc(sizeof(Bar_Progress_t));
|
p = (Bar_Progress_t *) malloc(sizeof(Bar_Progress_t));
|
||||||
memset( p, 0, sizeof(Bar_Progress_t) );
|
memset( p, 0, sizeof(Bar_Progress_t) );
|
||||||
p->pFile = pFile;
|
p->pFile = pFile;
|
||||||
|
|
|
||||||
|
|
@ -20,6 +20,7 @@
|
||||||
|
|
||||||
#include "fra.h"
|
#include "fra.h"
|
||||||
#include "ioa.h"
|
#include "ioa.h"
|
||||||
|
#include "int.h"
|
||||||
|
|
||||||
////////////////////////////////////////////////////////////////////////
|
////////////////////////////////////////////////////////////////////////
|
||||||
/// DECLARATIONS ///
|
/// DECLARATIONS ///
|
||||||
|
|
@ -389,11 +390,15 @@ PRT( "Time", clock() - clkTotal );
|
||||||
clk = clock();
|
clk = clock();
|
||||||
if ( pParSec->fInterpolation && RetValue == -1 && Aig_ManRegNum(pNew) > 0 && Aig_ManPoNum(pNew)-Aig_ManRegNum(pNew) == 1 )
|
if ( pParSec->fInterpolation && RetValue == -1 && Aig_ManRegNum(pNew) > 0 && Aig_ManPoNum(pNew)-Aig_ManRegNum(pNew) == 1 )
|
||||||
{
|
{
|
||||||
extern int Saig_Interpolate( Aig_Man_t * pAig, int nConfLimit, int nFramesMax, int fRewrite, int fTransLoop, int fUsePudlak, int fUseOther, int fUseMiniSat, int fCheckInd, int fCheckKstep, int fVerbose, int * pDepth );
|
Inter_ManParams_t Pars, * pPars = &Pars;
|
||||||
int Depth;
|
int Depth;
|
||||||
pNew->nTruePis = Aig_ManPiNum(pNew) - Aig_ManRegNum(pNew);
|
pNew->nTruePis = Aig_ManPiNum(pNew) - Aig_ManRegNum(pNew);
|
||||||
pNew->nTruePos = Aig_ManPoNum(pNew) - Aig_ManRegNum(pNew);
|
pNew->nTruePos = Aig_ManPoNum(pNew) - Aig_ManRegNum(pNew);
|
||||||
RetValue = Saig_Interpolate( pNew, 5000, 40, 0, 1, 0, 0, 0, 1, 1, pParSec->fVeryVerbose, &Depth );
|
|
||||||
|
Inter_ManSetDefaultParams( pPars );
|
||||||
|
pPars->fVerbose = pParSec->fVeryVerbose;
|
||||||
|
RetValue = Inter_ManPerformInterpolation( pNew, pPars, &Depth );
|
||||||
|
|
||||||
if ( pParSec->fVerbose )
|
if ( pParSec->fVerbose )
|
||||||
{
|
{
|
||||||
if ( RetValue == 1 )
|
if ( RetValue == 1 )
|
||||||
|
|
@ -454,7 +459,7 @@ PRT( "Time", clock() - clk );
|
||||||
iCount++;
|
iCount++;
|
||||||
if ( !pParSec->fSilent )
|
if ( !pParSec->fSilent )
|
||||||
printf( "*** Running output %d of the miter (number %d out of %d unsolved).\n", i, iCount, Counter );
|
printf( "*** Running output %d of the miter (number %d out of %d unsolved).\n", i, iCount, Counter );
|
||||||
pNew2 = Aig_ManDupOneOutput( pNew, i );
|
pNew2 = Aig_ManDupOneOutput( pNew, i, 1 );
|
||||||
|
|
||||||
TimeLimitCopy = pParSec->TimeLimit;
|
TimeLimitCopy = pParSec->TimeLimit;
|
||||||
pParSec->TimeLimit = TimeLimit2;
|
pParSec->TimeLimit = TimeLimit2;
|
||||||
|
|
|
||||||
|
|
@ -531,6 +531,35 @@ void Fra_SmlNodeSimulate( Fra_Sml_t * p, Aig_Obj_t * pObj, int iFrame )
|
||||||
}
|
}
|
||||||
}
|
}
|
||||||
|
|
||||||
|
/**Function*************************************************************
|
||||||
|
|
||||||
|
Synopsis [Simulates one node.]
|
||||||
|
|
||||||
|
Description []
|
||||||
|
|
||||||
|
SideEffects []
|
||||||
|
|
||||||
|
SeeAlso []
|
||||||
|
|
||||||
|
***********************************************************************/
|
||||||
|
int Fra_SmlNodesCompareInFrame( Fra_Sml_t * p, Aig_Obj_t * pObj0, Aig_Obj_t * pObj1, int iFrame0, int iFrame1 )
|
||||||
|
{
|
||||||
|
unsigned * pSims0, * pSims1;
|
||||||
|
int i;
|
||||||
|
assert( !Aig_IsComplement(pObj0) );
|
||||||
|
assert( !Aig_IsComplement(pObj1) );
|
||||||
|
assert( iFrame0 == 0 || p->nWordsFrame < p->nWordsTotal );
|
||||||
|
assert( iFrame1 == 0 || p->nWordsFrame < p->nWordsTotal );
|
||||||
|
// get hold of the simulation information
|
||||||
|
pSims0 = Fra_ObjSim(p, pObj0->Id) + p->nWordsFrame * iFrame0;
|
||||||
|
pSims1 = Fra_ObjSim(p, pObj1->Id) + p->nWordsFrame * iFrame1;
|
||||||
|
// compare
|
||||||
|
for ( i = 0; i < p->nWordsFrame; i++ )
|
||||||
|
if ( pSims0[i] != pSims1[i] )
|
||||||
|
return 0;
|
||||||
|
return 1;
|
||||||
|
}
|
||||||
|
|
||||||
/**Function*************************************************************
|
/**Function*************************************************************
|
||||||
|
|
||||||
Synopsis [Simulates one node.]
|
Synopsis [Simulates one node.]
|
||||||
|
|
|
||||||
|
|
@ -0,0 +1,85 @@
|
||||||
|
/**CFile****************************************************************
|
||||||
|
|
||||||
|
FileName [int.h]
|
||||||
|
|
||||||
|
SystemName [ABC: Logic synthesis and verification system.]
|
||||||
|
|
||||||
|
PackageName [Interpolation engine.]
|
||||||
|
|
||||||
|
Synopsis [External declarations.]
|
||||||
|
|
||||||
|
Author [Alan Mishchenko]
|
||||||
|
|
||||||
|
Affiliation [UC Berkeley]
|
||||||
|
|
||||||
|
Date [Ver. 1.0. Started - June 24, 2008.]
|
||||||
|
|
||||||
|
Revision [$Id: int.h,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
|
||||||
|
|
||||||
|
***********************************************************************/
|
||||||
|
|
||||||
|
#ifndef __INT_H__
|
||||||
|
#define __INT_H__
|
||||||
|
|
||||||
|
#ifdef __cplusplus
|
||||||
|
extern "C" {
|
||||||
|
#endif
|
||||||
|
|
||||||
|
/*
|
||||||
|
The interpolation algorithm implemented here was introduced in the paper:
|
||||||
|
K. L. McMillan. Interpolation and SAT-based model checking. CAV’03, pp. 1-13.
|
||||||
|
*/
|
||||||
|
|
||||||
|
////////////////////////////////////////////////////////////////////////
|
||||||
|
/// INCLUDES ///
|
||||||
|
////////////////////////////////////////////////////////////////////////
|
||||||
|
|
||||||
|
////////////////////////////////////////////////////////////////////////
|
||||||
|
/// PARAMETERS ///
|
||||||
|
////////////////////////////////////////////////////////////////////////
|
||||||
|
|
||||||
|
////////////////////////////////////////////////////////////////////////
|
||||||
|
/// BASIC TYPES ///
|
||||||
|
////////////////////////////////////////////////////////////////////////
|
||||||
|
|
||||||
|
// simulation manager
|
||||||
|
typedef struct Inter_ManParams_t_ Inter_ManParams_t;
|
||||||
|
struct Inter_ManParams_t_
|
||||||
|
{
|
||||||
|
int nBTLimit; // limit on the number of conflicts
|
||||||
|
int nFramesMax; // the max number timeframes to unroll
|
||||||
|
int nFramesK; // the number of timeframes to use in induction
|
||||||
|
int fRewrite; // use additional rewriting to simplify timeframes
|
||||||
|
int fTransLoop; // add transition into the init state under new PI var
|
||||||
|
int fUsePudlak; // use Pudluk interpolation procedure
|
||||||
|
int fUseOther; // use other undisclosed option
|
||||||
|
int fUseMiniSat; // use MiniSat-1.14p instead of internal proof engine
|
||||||
|
int fCheckKstep; // check using K-step induction
|
||||||
|
int fUseBias; // bias decisions to global variables
|
||||||
|
int fUseBackward; // perform backward interpolation
|
||||||
|
int fVerbose; // print verbose statistics
|
||||||
|
};
|
||||||
|
|
||||||
|
////////////////////////////////////////////////////////////////////////
|
||||||
|
/// MACRO DEFINITIONS ///
|
||||||
|
////////////////////////////////////////////////////////////////////////
|
||||||
|
|
||||||
|
////////////////////////////////////////////////////////////////////////
|
||||||
|
/// FUNCTION DECLARATIONS ///
|
||||||
|
////////////////////////////////////////////////////////////////////////
|
||||||
|
|
||||||
|
/*=== intCore.c ==========================================================*/
|
||||||
|
extern void Inter_ManSetDefaultParams( Inter_ManParams_t * p );
|
||||||
|
extern int Inter_ManPerformInterpolation( Aig_Man_t * pAig, Inter_ManParams_t * pPars, int * pDepth );
|
||||||
|
|
||||||
|
|
||||||
|
#ifdef __cplusplus
|
||||||
|
}
|
||||||
|
#endif
|
||||||
|
|
||||||
|
#endif
|
||||||
|
|
||||||
|
////////////////////////////////////////////////////////////////////////
|
||||||
|
/// END OF FILE ///
|
||||||
|
////////////////////////////////////////////////////////////////////////
|
||||||
|
|
||||||
|
|
@ -0,0 +1,328 @@
|
||||||
|
/**CFile****************************************************************
|
||||||
|
|
||||||
|
FileName [intContain.c]
|
||||||
|
|
||||||
|
SystemName [ABC: Logic synthesis and verification system.]
|
||||||
|
|
||||||
|
PackageName [Interpolation engine.]
|
||||||
|
|
||||||
|
Synopsis [Interpolant containment checking.]
|
||||||
|
|
||||||
|
Author [Alan Mishchenko]
|
||||||
|
|
||||||
|
Affiliation [UC Berkeley]
|
||||||
|
|
||||||
|
Date [Ver. 1.0. Started - June 24, 2008.]
|
||||||
|
|
||||||
|
Revision [$Id: intContain.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
|
||||||
|
|
||||||
|
***********************************************************************/
|
||||||
|
|
||||||
|
#include "intInt.h"
|
||||||
|
#include "fra.h"
|
||||||
|
|
||||||
|
////////////////////////////////////////////////////////////////////////
|
||||||
|
/// DECLARATIONS ///
|
||||||
|
////////////////////////////////////////////////////////////////////////
|
||||||
|
|
||||||
|
extern int Inter_ManCheckUniqueness( Aig_Man_t * p, sat_solver * pSat, Cnf_Dat_t * pCnf, int nFrames );
|
||||||
|
|
||||||
|
////////////////////////////////////////////////////////////////////////
|
||||||
|
/// FUNCTION DEFINITIONS ///
|
||||||
|
////////////////////////////////////////////////////////////////////////
|
||||||
|
|
||||||
|
/**Function*************************************************************
|
||||||
|
|
||||||
|
Synopsis [Checks constainment of two interpolants.]
|
||||||
|
|
||||||
|
Description []
|
||||||
|
|
||||||
|
SideEffects []
|
||||||
|
|
||||||
|
SeeAlso []
|
||||||
|
|
||||||
|
***********************************************************************/
|
||||||
|
int Inter_ManCheckContainment( Aig_Man_t * pNew, Aig_Man_t * pOld )
|
||||||
|
{
|
||||||
|
Aig_Man_t * pMiter, * pAigTemp;
|
||||||
|
int RetValue;
|
||||||
|
pMiter = Aig_ManCreateMiter( pNew, pOld, 1 );
|
||||||
|
// pMiter = Dar_ManRwsat( pAigTemp = pMiter, 1, 0 );
|
||||||
|
// Aig_ManStop( pAigTemp );
|
||||||
|
RetValue = Fra_FraigMiterStatus( pMiter );
|
||||||
|
if ( RetValue == -1 )
|
||||||
|
{
|
||||||
|
pAigTemp = Fra_FraigEquivence( pMiter, 1000000, 1 );
|
||||||
|
RetValue = Fra_FraigMiterStatus( pAigTemp );
|
||||||
|
Aig_ManStop( pAigTemp );
|
||||||
|
// RetValue = Fra_FraigSat( pMiter, 1000000, 0, 0, 0 );
|
||||||
|
}
|
||||||
|
assert( RetValue != -1 );
|
||||||
|
Aig_ManStop( pMiter );
|
||||||
|
return RetValue;
|
||||||
|
}
|
||||||
|
|
||||||
|
/**Function*************************************************************
|
||||||
|
|
||||||
|
Synopsis [Checks constainment of two interpolants.]
|
||||||
|
|
||||||
|
Description []
|
||||||
|
|
||||||
|
SideEffects []
|
||||||
|
|
||||||
|
SeeAlso []
|
||||||
|
|
||||||
|
***********************************************************************/
|
||||||
|
int Inter_ManCheckEquivalence( Aig_Man_t * pNew, Aig_Man_t * pOld )
|
||||||
|
{
|
||||||
|
Aig_Man_t * pMiter, * pAigTemp;
|
||||||
|
int RetValue;
|
||||||
|
pMiter = Aig_ManCreateMiter( pNew, pOld, 0 );
|
||||||
|
// pMiter = Dar_ManRwsat( pAigTemp = pMiter, 1, 0 );
|
||||||
|
// Aig_ManStop( pAigTemp );
|
||||||
|
RetValue = Fra_FraigMiterStatus( pMiter );
|
||||||
|
if ( RetValue == -1 )
|
||||||
|
{
|
||||||
|
pAigTemp = Fra_FraigEquivence( pMiter, 1000000, 1 );
|
||||||
|
RetValue = Fra_FraigMiterStatus( pAigTemp );
|
||||||
|
Aig_ManStop( pAigTemp );
|
||||||
|
// RetValue = Fra_FraigSat( pMiter, 1000000, 0, 0, 0 );
|
||||||
|
}
|
||||||
|
assert( RetValue != -1 );
|
||||||
|
Aig_ManStop( pMiter );
|
||||||
|
return RetValue;
|
||||||
|
}
|
||||||
|
|
||||||
|
|
||||||
|
/**Function*************************************************************
|
||||||
|
|
||||||
|
Synopsis [Create timeframes of the manager for interpolation.]
|
||||||
|
|
||||||
|
Description [The resulting manager is combinational. The primary inputs
|
||||||
|
corresponding to register outputs are ordered first.]
|
||||||
|
|
||||||
|
SideEffects []
|
||||||
|
|
||||||
|
SeeAlso []
|
||||||
|
|
||||||
|
***********************************************************************/
|
||||||
|
Aig_Man_t * Inter_ManFramesLatches( Aig_Man_t * pAig, int nFrames, Vec_Ptr_t ** pvMapReg )
|
||||||
|
{
|
||||||
|
Aig_Man_t * pFrames;
|
||||||
|
Aig_Obj_t * pObj, * pObjLi, * pObjLo;
|
||||||
|
int i, f;
|
||||||
|
assert( Saig_ManRegNum(pAig) > 0 );
|
||||||
|
pFrames = Aig_ManStart( Aig_ManNodeNum(pAig) * nFrames );
|
||||||
|
// map the constant node
|
||||||
|
Aig_ManConst1(pAig)->pData = Aig_ManConst1( pFrames );
|
||||||
|
// create variables for register outputs
|
||||||
|
*pvMapReg = Vec_PtrAlloc( (nFrames+1) * Saig_ManRegNum(pAig) );
|
||||||
|
Saig_ManForEachLo( pAig, pObj, i )
|
||||||
|
{
|
||||||
|
pObj->pData = Aig_ObjCreatePi( pFrames );
|
||||||
|
Vec_PtrPush( *pvMapReg, pObj->pData );
|
||||||
|
}
|
||||||
|
// add timeframes
|
||||||
|
for ( f = 0; f < nFrames; f++ )
|
||||||
|
{
|
||||||
|
// create PI nodes for this frame
|
||||||
|
Saig_ManForEachPi( pAig, pObj, i )
|
||||||
|
pObj->pData = Aig_ObjCreatePi( pFrames );
|
||||||
|
// add internal nodes of this frame
|
||||||
|
Aig_ManForEachNode( pAig, pObj, i )
|
||||||
|
pObj->pData = Aig_And( pFrames, Aig_ObjChild0Copy(pObj), Aig_ObjChild1Copy(pObj) );
|
||||||
|
// save register inputs
|
||||||
|
Saig_ManForEachLi( pAig, pObj, i )
|
||||||
|
pObj->pData = Aig_ObjChild0Copy(pObj);
|
||||||
|
// transfer to register outputs
|
||||||
|
Saig_ManForEachLiLo( pAig, pObjLi, pObjLo, i )
|
||||||
|
{
|
||||||
|
pObjLo->pData = pObjLi->pData;
|
||||||
|
Vec_PtrPush( *pvMapReg, pObjLo->pData );
|
||||||
|
}
|
||||||
|
}
|
||||||
|
return pFrames;
|
||||||
|
}
|
||||||
|
|
||||||
|
/**Function*************************************************************
|
||||||
|
|
||||||
|
Synopsis [Duplicates AIG while mapping PIs into the given array.]
|
||||||
|
|
||||||
|
Description []
|
||||||
|
|
||||||
|
SideEffects []
|
||||||
|
|
||||||
|
SeeAlso []
|
||||||
|
|
||||||
|
***********************************************************************/
|
||||||
|
void Inter_ManAppendCone( Aig_Man_t * pOld, Aig_Man_t * pNew, Aig_Obj_t ** ppNewPis, int fCompl )
|
||||||
|
{
|
||||||
|
Aig_Obj_t * pObj;
|
||||||
|
int i;
|
||||||
|
assert( Aig_ManPoNum(pOld) == 1 );
|
||||||
|
// create the PIs
|
||||||
|
Aig_ManCleanData( pOld );
|
||||||
|
Aig_ManConst1(pOld)->pData = Aig_ManConst1(pNew);
|
||||||
|
Aig_ManForEachPi( pOld, pObj, i )
|
||||||
|
pObj->pData = ppNewPis[i];
|
||||||
|
// duplicate internal nodes
|
||||||
|
Aig_ManForEachNode( pOld, pObj, i )
|
||||||
|
pObj->pData = Aig_And( pNew, Aig_ObjChild0Copy(pObj), Aig_ObjChild1Copy(pObj) );
|
||||||
|
// add one PO to new
|
||||||
|
pObj = Aig_ManPo( pOld, 0 );
|
||||||
|
Aig_ObjCreatePo( pNew, Aig_NotCond( Aig_ObjChild0Copy(pObj), fCompl ) );
|
||||||
|
}
|
||||||
|
|
||||||
|
|
||||||
|
/**Function*************************************************************
|
||||||
|
|
||||||
|
Synopsis [Checks constainment of two interpolants inductively.]
|
||||||
|
|
||||||
|
Description []
|
||||||
|
|
||||||
|
SideEffects []
|
||||||
|
|
||||||
|
SeeAlso []
|
||||||
|
|
||||||
|
***********************************************************************/
|
||||||
|
int Inter_ManCheckInductiveContainment( Aig_Man_t * pTrans, Aig_Man_t * pInter, int nSteps, int fBackward )
|
||||||
|
{
|
||||||
|
Aig_Man_t * pFrames;
|
||||||
|
Aig_Obj_t ** ppNodes;
|
||||||
|
Vec_Ptr_t * vMapRegs;
|
||||||
|
Cnf_Dat_t * pCnf;
|
||||||
|
sat_solver * pSat;
|
||||||
|
int f, nRegs, status;
|
||||||
|
nRegs = Saig_ManRegNum(pTrans);
|
||||||
|
assert( nRegs > 0 );
|
||||||
|
// generate the timeframes
|
||||||
|
pFrames = Inter_ManFramesLatches( pTrans, nSteps, &vMapRegs );
|
||||||
|
assert( Vec_PtrSize(vMapRegs) == (nSteps + 1) * nRegs );
|
||||||
|
// add main constraints to the timeframes
|
||||||
|
ppNodes = (Aig_Obj_t **)Vec_PtrArray(vMapRegs);
|
||||||
|
if ( fBackward )
|
||||||
|
{
|
||||||
|
// p -> !p -> ... -> !p
|
||||||
|
Inter_ManAppendCone( pInter, pFrames, ppNodes + 0 * nRegs, 1 );
|
||||||
|
for ( f = 1; f <= nSteps; f++ )
|
||||||
|
Inter_ManAppendCone( pInter, pFrames, ppNodes + f * nRegs, 0 );
|
||||||
|
}
|
||||||
|
else
|
||||||
|
{
|
||||||
|
// !p -> p -> ... -> p
|
||||||
|
for ( f = 0; f < nSteps; f++ )
|
||||||
|
Inter_ManAppendCone( pInter, pFrames, ppNodes + f * nRegs, 0 );
|
||||||
|
Inter_ManAppendCone( pInter, pFrames, ppNodes + f * nRegs, 1 );
|
||||||
|
}
|
||||||
|
Vec_PtrFree( vMapRegs );
|
||||||
|
Aig_ManCleanup( pFrames );
|
||||||
|
|
||||||
|
// convert to CNF
|
||||||
|
pCnf = Cnf_Derive( pFrames, 0 );
|
||||||
|
pSat = Cnf_DataWriteIntoSolver( pCnf, 1, 0 );
|
||||||
|
// Cnf_DataFree( pCnf );
|
||||||
|
// Aig_ManStop( pFrames );
|
||||||
|
|
||||||
|
if ( pSat == NULL )
|
||||||
|
{
|
||||||
|
Cnf_DataFree( pCnf );
|
||||||
|
Aig_ManStop( pFrames );
|
||||||
|
return 1;
|
||||||
|
}
|
||||||
|
|
||||||
|
// solve the problem
|
||||||
|
status = sat_solver_solve( pSat, NULL, NULL, (sint64)0, (sint64)0, (sint64)0, (sint64)0 );
|
||||||
|
|
||||||
|
// Inter_ManCheckUniqueness( pTrans, pSat, pCnf, nSteps );
|
||||||
|
|
||||||
|
Cnf_DataFree( pCnf );
|
||||||
|
Aig_ManStop( pFrames );
|
||||||
|
|
||||||
|
sat_solver_delete( pSat );
|
||||||
|
return status == l_False;
|
||||||
|
}
|
||||||
|
|
||||||
|
#include "fra.h"
|
||||||
|
|
||||||
|
/**Function*************************************************************
|
||||||
|
|
||||||
|
Synopsis [Check if cex satisfies uniqueness constraints.]
|
||||||
|
|
||||||
|
Description []
|
||||||
|
|
||||||
|
SideEffects []
|
||||||
|
|
||||||
|
SeeAlso []
|
||||||
|
|
||||||
|
***********************************************************************/
|
||||||
|
int Inter_ManCheckUniqueness( Aig_Man_t * p, sat_solver * pSat, Cnf_Dat_t * pCnf, int nFrames )
|
||||||
|
{
|
||||||
|
extern int Fra_SmlNodesCompareInFrame( Fra_Sml_t * p, Aig_Obj_t * pObj0, Aig_Obj_t * pObj1, int iFrame0, int iFrame1 );
|
||||||
|
extern void Fra_SmlAssignConst( Fra_Sml_t * p, Aig_Obj_t * pObj, int fConst1, int iFrame );
|
||||||
|
extern void Fra_SmlSimulateOne( Fra_Sml_t * p );
|
||||||
|
|
||||||
|
Fra_Sml_t * pSml;
|
||||||
|
Vec_Int_t * vPis;
|
||||||
|
Aig_Obj_t * pObj, * pObj0;
|
||||||
|
int i, k, v, iBit, * pCounterEx;
|
||||||
|
int Counter;
|
||||||
|
if ( nFrames == 1 )
|
||||||
|
return 1;
|
||||||
|
if ( pSat->model.size == 0 )
|
||||||
|
return 1;
|
||||||
|
// assert( Saig_ManPoNum(p) == 1 );
|
||||||
|
assert( Aig_ManRegNum(p) > 0 );
|
||||||
|
assert( Aig_ManRegNum(p) < Aig_ManPiNum(p) );
|
||||||
|
|
||||||
|
// get the counter-example
|
||||||
|
vPis = Vec_IntAlloc( 100 );
|
||||||
|
Aig_ManForEachPi( pCnf->pMan, pObj, k )
|
||||||
|
Vec_IntPush( vPis, pCnf->pVarNums[Aig_ObjId(pObj)] );
|
||||||
|
assert( Vec_IntSize(vPis) == Aig_ManRegNum(p) + nFrames * Saig_ManPiNum(p) );
|
||||||
|
pCounterEx = Sat_SolverGetModel( pSat, vPis->pArray, vPis->nSize );
|
||||||
|
Vec_IntFree( vPis );
|
||||||
|
|
||||||
|
// start a new sequential simulator
|
||||||
|
pSml = Fra_SmlStart( p, 0, nFrames, 1 );
|
||||||
|
// assign simulation info for the registers
|
||||||
|
iBit = 0;
|
||||||
|
Aig_ManForEachLoSeq( p, pObj, i )
|
||||||
|
Fra_SmlAssignConst( pSml, pObj, pCounterEx[iBit++], 0 );
|
||||||
|
// assign simulation info for the primary inputs
|
||||||
|
for ( i = 0; i < nFrames; i++ )
|
||||||
|
Aig_ManForEachPiSeq( p, pObj, k )
|
||||||
|
Fra_SmlAssignConst( pSml, pObj, pCounterEx[iBit++], i );
|
||||||
|
assert( iBit == Aig_ManPiNum(pCnf->pMan) );
|
||||||
|
// run simulation
|
||||||
|
Fra_SmlSimulateOne( pSml );
|
||||||
|
|
||||||
|
// check if the given output has failed
|
||||||
|
// RetValue = !Fra_SmlNodeIsZero( pSml, Aig_ManPo(pAig, 0) );
|
||||||
|
// assert( RetValue );
|
||||||
|
|
||||||
|
// check values at the internal nodes
|
||||||
|
Counter = 0;
|
||||||
|
for ( i = 0; i < nFrames; i++ )
|
||||||
|
for ( k = i+1; k < nFrames; k++ )
|
||||||
|
{
|
||||||
|
for ( v = 0; v < Aig_ManRegNum(p); v++ )
|
||||||
|
{
|
||||||
|
pObj0 = Aig_ManLo(p, v);
|
||||||
|
if ( !Fra_SmlNodesCompareInFrame( pSml, pObj0, pObj0, i, k ) )
|
||||||
|
break;
|
||||||
|
}
|
||||||
|
if ( v == Aig_ManRegNum(p) )
|
||||||
|
Counter++;
|
||||||
|
}
|
||||||
|
printf( "Uniquness does not hold in %d frames.\n", Counter );
|
||||||
|
|
||||||
|
Fra_SmlStop( pSml );
|
||||||
|
free( pCounterEx );
|
||||||
|
return 1;
|
||||||
|
}
|
||||||
|
|
||||||
|
////////////////////////////////////////////////////////////////////////
|
||||||
|
/// END OF FILE ///
|
||||||
|
////////////////////////////////////////////////////////////////////////
|
||||||
|
|
||||||
|
|
||||||
|
|
@ -0,0 +1,286 @@
|
||||||
|
/**CFile****************************************************************
|
||||||
|
|
||||||
|
FileName [intCore.c]
|
||||||
|
|
||||||
|
SystemName [ABC: Logic synthesis and verification system.]
|
||||||
|
|
||||||
|
PackageName [Interpolation engine.]
|
||||||
|
|
||||||
|
Synopsis [Core procedures.]
|
||||||
|
|
||||||
|
Author [Alan Mishchenko]
|
||||||
|
|
||||||
|
Affiliation [UC Berkeley]
|
||||||
|
|
||||||
|
Date [Ver. 1.0. Started - June 24, 2008.]
|
||||||
|
|
||||||
|
Revision [$Id: intCore.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
|
||||||
|
|
||||||
|
***********************************************************************/
|
||||||
|
|
||||||
|
#include "intInt.h"
|
||||||
|
|
||||||
|
////////////////////////////////////////////////////////////////////////
|
||||||
|
/// DECLARATIONS ///
|
||||||
|
////////////////////////////////////////////////////////////////////////
|
||||||
|
|
||||||
|
////////////////////////////////////////////////////////////////////////
|
||||||
|
/// FUNCTION DEFINITIONS ///
|
||||||
|
////////////////////////////////////////////////////////////////////////
|
||||||
|
|
||||||
|
/**Function*************************************************************
|
||||||
|
|
||||||
|
Synopsis [This procedure sets default values of interpolation parameters.]
|
||||||
|
|
||||||
|
Description []
|
||||||
|
|
||||||
|
SideEffects []
|
||||||
|
|
||||||
|
SeeAlso []
|
||||||
|
|
||||||
|
***********************************************************************/
|
||||||
|
void Inter_ManSetDefaultParams( Inter_ManParams_t * p )
|
||||||
|
{
|
||||||
|
memset( p, 0, sizeof(Inter_ManParams_t) );
|
||||||
|
p->nBTLimit = 10000; // limit on the number of conflicts
|
||||||
|
p->nFramesMax = 40; // the max number timeframes to unroll
|
||||||
|
p->nFramesK = 1; // the number of timeframes to use in induction
|
||||||
|
p->fRewrite = 0; // use additional rewriting to simplify timeframes
|
||||||
|
p->fTransLoop = 1; // add transition into the init state under new PI var
|
||||||
|
p->fUsePudlak = 0; // use Pudluk interpolation procedure
|
||||||
|
p->fUseOther = 0; // use other undisclosed option
|
||||||
|
p->fUseMiniSat = 0; // use MiniSat-1.14p instead of internal proof engine
|
||||||
|
p->fCheckKstep = 1; // check using K-step induction
|
||||||
|
p->fUseBias = 0; // bias decisions to global variables
|
||||||
|
p->fUseBackward = 0; // perform backward interpolation
|
||||||
|
p->fVerbose = 0; // print verbose statistics
|
||||||
|
}
|
||||||
|
|
||||||
|
/**Function*************************************************************
|
||||||
|
|
||||||
|
Synopsis [Interplates while the number of conflicts is not exceeded.]
|
||||||
|
|
||||||
|
Description [Returns 1 if proven. 0 if failed. -1 if undecided.]
|
||||||
|
|
||||||
|
SideEffects [Does not check the property in 0-th frame.]
|
||||||
|
|
||||||
|
SeeAlso []
|
||||||
|
|
||||||
|
***********************************************************************/
|
||||||
|
int Inter_ManPerformInterpolation( Aig_Man_t * pAig, Inter_ManParams_t * pPars, int * pDepth )
|
||||||
|
{
|
||||||
|
extern int Inter_ManCheckInductiveContainment( Aig_Man_t * pTrans, Aig_Man_t * pInter, int nSteps, int fBackward );
|
||||||
|
Inter_Man_t * p;
|
||||||
|
Aig_Man_t * pAigTemp;
|
||||||
|
int s, i, RetValue, Status, clk, clk2, clkTotal = clock();
|
||||||
|
// sanity checks
|
||||||
|
assert( Saig_ManRegNum(pAig) > 0 );
|
||||||
|
assert( Saig_ManPiNum(pAig) > 0 );
|
||||||
|
assert( Saig_ManPoNum(pAig) == 1 );
|
||||||
|
/*
|
||||||
|
if ( Inter_ManCheckInitialState(pAig) )
|
||||||
|
{
|
||||||
|
printf( "Property trivially fails in the initial state.\n" );
|
||||||
|
return 0;
|
||||||
|
}
|
||||||
|
if ( Inter_ManCheckAllStates(pAig) )
|
||||||
|
{
|
||||||
|
printf( "Property trivially holds in all states.\n" );
|
||||||
|
return 1;
|
||||||
|
}
|
||||||
|
*/
|
||||||
|
// create interpolation manager
|
||||||
|
// can perform SAT sweeping and/or rewriting of this AIG...
|
||||||
|
p = Inter_ManCreate( pAig, pPars );
|
||||||
|
if ( pPars->fTransLoop )
|
||||||
|
p->pAigTrans = Inter_ManStartOneOutput( pAig, 0 );
|
||||||
|
else
|
||||||
|
p->pAigTrans = Inter_ManStartDuplicated( pAig );
|
||||||
|
// derive CNF for the transformed AIG
|
||||||
|
clk = clock();
|
||||||
|
p->pCnfAig = Cnf_Derive( p->pAigTrans, Aig_ManRegNum(p->pAigTrans) );
|
||||||
|
p->timeCnf += clock() - clk;
|
||||||
|
if ( pPars->fVerbose )
|
||||||
|
{
|
||||||
|
printf( "AIG: PI/PO/Reg = %d/%d/%d. And = %d. Lev = %d. CNF: Var/Cla = %d/%d.\n",
|
||||||
|
Saig_ManPiNum(pAig), Saig_ManPoNum(pAig), Saig_ManRegNum(pAig),
|
||||||
|
Aig_ManAndNum(pAig), Aig_ManLevelNum(pAig),
|
||||||
|
p->pCnfAig->nVars, p->pCnfAig->nClauses );
|
||||||
|
}
|
||||||
|
|
||||||
|
// derive interpolant
|
||||||
|
*pDepth = -1;
|
||||||
|
p->nFrames = 1;
|
||||||
|
for ( s = 0; ; s++ )
|
||||||
|
{
|
||||||
|
clk2 = clock();
|
||||||
|
// initial state
|
||||||
|
if ( pPars->fUseBackward )
|
||||||
|
p->pInter = Inter_ManStartOneOutput( pAig, 1 );
|
||||||
|
else
|
||||||
|
p->pInter = Inter_ManStartInitState( Aig_ManRegNum(pAig) );
|
||||||
|
assert( Aig_ManPoNum(p->pInter) == 1 );
|
||||||
|
clk = clock();
|
||||||
|
p->pCnfInter = Cnf_Derive( p->pInter, 0 );
|
||||||
|
p->timeCnf += clock() - clk;
|
||||||
|
// timeframes
|
||||||
|
p->pFrames = Inter_ManFramesInter( pAig, p->nFrames, pPars->fUseBackward );
|
||||||
|
clk = clock();
|
||||||
|
if ( pPars->fRewrite )
|
||||||
|
{
|
||||||
|
p->pFrames = Dar_ManRwsat( pAigTemp = p->pFrames, 1, 0 );
|
||||||
|
Aig_ManStop( pAigTemp );
|
||||||
|
// p->pFrames = Fra_FraigEquivence( pAigTemp = p->pFrames, 100, 0 );
|
||||||
|
// Aig_ManStop( pAigTemp );
|
||||||
|
}
|
||||||
|
p->timeRwr += clock() - clk;
|
||||||
|
// can also do SAT sweeping on the timeframes...
|
||||||
|
clk = clock();
|
||||||
|
if ( pPars->fUseBackward )
|
||||||
|
p->pCnfFrames = Cnf_Derive( p->pFrames, Aig_ManPoNum(p->pFrames) );
|
||||||
|
else
|
||||||
|
p->pCnfFrames = Cnf_Derive( p->pFrames, 0 );
|
||||||
|
p->timeCnf += clock() - clk;
|
||||||
|
// report statistics
|
||||||
|
if ( pPars->fVerbose )
|
||||||
|
{
|
||||||
|
printf( "Step = %2d. Frames = 1 + %d. And = %5d. Lev = %5d. ",
|
||||||
|
s+1, p->nFrames, Aig_ManNodeNum(p->pFrames), Aig_ManLevelNum(p->pFrames) );
|
||||||
|
PRT( "Time", clock() - clk2 );
|
||||||
|
}
|
||||||
|
// iterate the interpolation procedure
|
||||||
|
for ( i = 0; ; i++ )
|
||||||
|
{
|
||||||
|
if ( p->nFrames + i >= pPars->nFramesMax )
|
||||||
|
{
|
||||||
|
if ( pPars->fVerbose )
|
||||||
|
printf( "Reached limit (%d) on the number of timeframes.\n", pPars->nFramesMax );
|
||||||
|
p->timeTotal = clock() - clkTotal;
|
||||||
|
Inter_ManStop( p );
|
||||||
|
return -1;
|
||||||
|
}
|
||||||
|
|
||||||
|
// perform interpolation
|
||||||
|
clk = clock();
|
||||||
|
#ifdef ABC_USE_LIBRARIES
|
||||||
|
if ( pPars->fUseMiniSat )
|
||||||
|
{
|
||||||
|
assert( !pPars->fUseBackward );
|
||||||
|
RetValue = Inter_ManPerformOneStepM114p( p, pPars->fUsePudlak, pPars->fUseOther );
|
||||||
|
}
|
||||||
|
else
|
||||||
|
#endif
|
||||||
|
RetValue = Inter_ManPerformOneStep( p, pPars->fUseBias, pPars->fUseBackward );
|
||||||
|
|
||||||
|
if ( pPars->fVerbose )
|
||||||
|
{
|
||||||
|
printf( " I = %2d. Bmc =%3d. IntAnd =%6d. IntLev =%5d. Conf =%6d. ",
|
||||||
|
i+1, i + 1 + p->nFrames, Aig_ManNodeNum(p->pInter), Aig_ManLevelNum(p->pInter), p->nConfCur );
|
||||||
|
PRT( "Time", clock() - clk );
|
||||||
|
}
|
||||||
|
if ( RetValue == 0 ) // found a (spurious?) counter-example
|
||||||
|
{
|
||||||
|
if ( i == 0 ) // real counterexample
|
||||||
|
{
|
||||||
|
if ( pPars->fVerbose )
|
||||||
|
printf( "Found a real counterexample in the first frame.\n" );
|
||||||
|
p->timeTotal = clock() - clkTotal;
|
||||||
|
*pDepth = p->nFrames + 1;
|
||||||
|
Inter_ManStop( p );
|
||||||
|
return 0;
|
||||||
|
}
|
||||||
|
// likely spurious counter-example
|
||||||
|
p->nFrames += i;
|
||||||
|
Inter_ManClean( p );
|
||||||
|
break;
|
||||||
|
}
|
||||||
|
else if ( RetValue == -1 ) // timed out
|
||||||
|
{
|
||||||
|
if ( pPars->fVerbose )
|
||||||
|
printf( "Reached limit (%d) on the number of conflicts.\n", p->nConfLimit );
|
||||||
|
assert( p->nConfCur >= p->nConfLimit );
|
||||||
|
p->timeTotal = clock() - clkTotal;
|
||||||
|
Inter_ManStop( p );
|
||||||
|
return -1;
|
||||||
|
}
|
||||||
|
assert( RetValue == 1 ); // found new interpolant
|
||||||
|
// compress the interpolant
|
||||||
|
clk = clock();
|
||||||
|
if ( p->pInterNew )
|
||||||
|
{
|
||||||
|
p->pInterNew = Dar_ManRwsat( pAigTemp = p->pInterNew, 1, 0 );
|
||||||
|
Aig_ManStop( pAigTemp );
|
||||||
|
}
|
||||||
|
p->timeRwr += clock() - clk;
|
||||||
|
|
||||||
|
// check if interpolant is trivial
|
||||||
|
if ( p->pInterNew == NULL || Aig_ObjChild0(Aig_ManPo(p->pInterNew,0)) == Aig_ManConst0(p->pInterNew) )
|
||||||
|
{
|
||||||
|
// printf( "interpolant is constant 0\n" );
|
||||||
|
if ( pPars->fVerbose )
|
||||||
|
printf( "The problem is trivially true for all states.\n" );
|
||||||
|
p->timeTotal = clock() - clkTotal;
|
||||||
|
Inter_ManStop( p );
|
||||||
|
return 1;
|
||||||
|
}
|
||||||
|
|
||||||
|
// check containment of interpolants
|
||||||
|
clk = clock();
|
||||||
|
if ( pPars->fCheckKstep ) // k-step unique-state induction
|
||||||
|
{
|
||||||
|
if ( Aig_ManPiNum(p->pInterNew) == Aig_ManPiNum(p->pInter) )
|
||||||
|
Status = Inter_ManCheckInductiveContainment( p->pAigTrans, p->pInterNew, pPars->nFramesK, pPars->fUseBackward );
|
||||||
|
else
|
||||||
|
Status = 0;
|
||||||
|
}
|
||||||
|
else // combinational containment
|
||||||
|
{
|
||||||
|
if ( Aig_ManPiNum(p->pInterNew) == Aig_ManPiNum(p->pInter) )
|
||||||
|
Status = Inter_ManCheckContainment( p->pInterNew, p->pInter );
|
||||||
|
else
|
||||||
|
Status = 0;
|
||||||
|
}
|
||||||
|
p->timeEqu += clock() - clk;
|
||||||
|
if ( Status ) // contained
|
||||||
|
{
|
||||||
|
if ( pPars->fVerbose )
|
||||||
|
printf( "Proved containment of interpolants.\n" );
|
||||||
|
p->timeTotal = clock() - clkTotal;
|
||||||
|
Inter_ManStop( p );
|
||||||
|
return 1;
|
||||||
|
}
|
||||||
|
// save interpolant and convert it into CNF
|
||||||
|
if ( pPars->fTransLoop )
|
||||||
|
{
|
||||||
|
Aig_ManStop( p->pInter );
|
||||||
|
p->pInter = p->pInterNew;
|
||||||
|
}
|
||||||
|
else
|
||||||
|
{
|
||||||
|
p->pInter = Aig_ManCreateMiter( pAigTemp = p->pInter, p->pInterNew, 2 );
|
||||||
|
Aig_ManStop( pAigTemp );
|
||||||
|
Aig_ManStop( p->pInterNew );
|
||||||
|
// compress the interpolant
|
||||||
|
clk = clock();
|
||||||
|
p->pInter = Dar_ManRwsat( pAigTemp = p->pInter, 1, 0 );
|
||||||
|
Aig_ManStop( pAigTemp );
|
||||||
|
p->timeRwr += clock() - clk;
|
||||||
|
}
|
||||||
|
p->pInterNew = NULL;
|
||||||
|
Cnf_DataFree( p->pCnfInter );
|
||||||
|
clk = clock();
|
||||||
|
p->pCnfInter = Cnf_Derive( p->pInter, 0 );
|
||||||
|
p->timeCnf += clock() - clk;
|
||||||
|
}
|
||||||
|
}
|
||||||
|
assert( 0 );
|
||||||
|
return RetValue;
|
||||||
|
}
|
||||||
|
|
||||||
|
|
||||||
|
|
||||||
|
////////////////////////////////////////////////////////////////////////
|
||||||
|
/// END OF FILE ///
|
||||||
|
////////////////////////////////////////////////////////////////////////
|
||||||
|
|
||||||
|
|
||||||
|
|
@ -0,0 +1,161 @@
|
||||||
|
/**CFile****************************************************************
|
||||||
|
|
||||||
|
FileName [intDup.c]
|
||||||
|
|
||||||
|
SystemName [ABC: Logic synthesis and verification system.]
|
||||||
|
|
||||||
|
PackageName [Interpolation engine.]
|
||||||
|
|
||||||
|
Synopsis [Specialized AIG duplication procedures.]
|
||||||
|
|
||||||
|
Author [Alan Mishchenko]
|
||||||
|
|
||||||
|
Affiliation [UC Berkeley]
|
||||||
|
|
||||||
|
Date [Ver. 1.0. Started - June 24, 2008.]
|
||||||
|
|
||||||
|
Revision [$Id: intDup.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
|
||||||
|
|
||||||
|
***********************************************************************/
|
||||||
|
|
||||||
|
#include "intInt.h"
|
||||||
|
|
||||||
|
////////////////////////////////////////////////////////////////////////
|
||||||
|
/// DECLARATIONS ///
|
||||||
|
////////////////////////////////////////////////////////////////////////
|
||||||
|
|
||||||
|
////////////////////////////////////////////////////////////////////////
|
||||||
|
/// FUNCTION DEFINITIONS ///
|
||||||
|
////////////////////////////////////////////////////////////////////////
|
||||||
|
|
||||||
|
/**Function*************************************************************
|
||||||
|
|
||||||
|
Synopsis [Create trivial AIG manager for the init state.]
|
||||||
|
|
||||||
|
Description []
|
||||||
|
|
||||||
|
SideEffects []
|
||||||
|
|
||||||
|
SeeAlso []
|
||||||
|
|
||||||
|
***********************************************************************/
|
||||||
|
Aig_Man_t * Inter_ManStartInitState( int nRegs )
|
||||||
|
{
|
||||||
|
Aig_Man_t * p;
|
||||||
|
Aig_Obj_t * pRes;
|
||||||
|
Aig_Obj_t ** ppInputs;
|
||||||
|
int i;
|
||||||
|
assert( nRegs > 0 );
|
||||||
|
ppInputs = ALLOC( Aig_Obj_t *, nRegs );
|
||||||
|
p = Aig_ManStart( nRegs );
|
||||||
|
for ( i = 0; i < nRegs; i++ )
|
||||||
|
ppInputs[i] = Aig_Not( Aig_ObjCreatePi(p) );
|
||||||
|
pRes = Aig_Multi( p, ppInputs, nRegs, AIG_OBJ_AND );
|
||||||
|
Aig_ObjCreatePo( p, pRes );
|
||||||
|
free( ppInputs );
|
||||||
|
return p;
|
||||||
|
}
|
||||||
|
|
||||||
|
/**Function*************************************************************
|
||||||
|
|
||||||
|
Synopsis [Duplicate the AIG w/o POs.]
|
||||||
|
|
||||||
|
Description []
|
||||||
|
|
||||||
|
SideEffects []
|
||||||
|
|
||||||
|
SeeAlso []
|
||||||
|
|
||||||
|
***********************************************************************/
|
||||||
|
Aig_Man_t * Inter_ManStartDuplicated( Aig_Man_t * p )
|
||||||
|
{
|
||||||
|
Aig_Man_t * pNew;
|
||||||
|
Aig_Obj_t * pObj;
|
||||||
|
int i;
|
||||||
|
assert( Aig_ManRegNum(p) > 0 );
|
||||||
|
// create the new manager
|
||||||
|
pNew = Aig_ManStart( Aig_ManObjNumMax(p) );
|
||||||
|
pNew->pName = Aig_UtilStrsav( p->pName );
|
||||||
|
pNew->pSpec = Aig_UtilStrsav( p->pSpec );
|
||||||
|
// create the PIs
|
||||||
|
Aig_ManCleanData( p );
|
||||||
|
Aig_ManConst1(p)->pData = Aig_ManConst1(pNew);
|
||||||
|
Aig_ManForEachPi( p, pObj, i )
|
||||||
|
pObj->pData = Aig_ObjCreatePi( pNew );
|
||||||
|
// set registers
|
||||||
|
pNew->nRegs = p->nRegs;
|
||||||
|
pNew->nTruePis = p->nTruePis;
|
||||||
|
pNew->nTruePos = 0;
|
||||||
|
// duplicate internal nodes
|
||||||
|
Aig_ManForEachNode( p, pObj, i )
|
||||||
|
pObj->pData = Aig_And( pNew, Aig_ObjChild0Copy(pObj), Aig_ObjChild1Copy(pObj) );
|
||||||
|
// create register inputs with MUXes
|
||||||
|
Saig_ManForEachLi( p, pObj, i )
|
||||||
|
Aig_ObjCreatePo( pNew, Aig_ObjChild0Copy(pObj) );
|
||||||
|
Aig_ManCleanup( pNew );
|
||||||
|
return pNew;
|
||||||
|
}
|
||||||
|
|
||||||
|
/**Function*************************************************************
|
||||||
|
|
||||||
|
Synopsis [Duplicate the AIG w/o POs and transforms to transit into init state.]
|
||||||
|
|
||||||
|
Description []
|
||||||
|
|
||||||
|
SideEffects []
|
||||||
|
|
||||||
|
SeeAlso []
|
||||||
|
|
||||||
|
***********************************************************************/
|
||||||
|
Aig_Man_t * Inter_ManStartOneOutput( Aig_Man_t * p, int fAddFirstPo )
|
||||||
|
{
|
||||||
|
Aig_Man_t * pNew;
|
||||||
|
Aig_Obj_t * pObj, * pObjLi, * pObjLo;
|
||||||
|
Aig_Obj_t * pCtrl = NULL; // Suppress "might be used uninitialized"
|
||||||
|
int i;
|
||||||
|
assert( Aig_ManRegNum(p) > 0 );
|
||||||
|
// create the new manager
|
||||||
|
pNew = Aig_ManStart( Aig_ManObjNumMax(p) );
|
||||||
|
pNew->pName = Aig_UtilStrsav( p->pName );
|
||||||
|
pNew->pSpec = Aig_UtilStrsav( p->pSpec );
|
||||||
|
// create the PIs
|
||||||
|
Aig_ManCleanData( p );
|
||||||
|
Aig_ManConst1(p)->pData = Aig_ManConst1(pNew);
|
||||||
|
Aig_ManForEachPi( p, pObj, i )
|
||||||
|
{
|
||||||
|
if ( i == Saig_ManPiNum(p) )
|
||||||
|
pCtrl = Aig_ObjCreatePi( pNew );
|
||||||
|
pObj->pData = Aig_ObjCreatePi( pNew );
|
||||||
|
}
|
||||||
|
// set registers
|
||||||
|
pNew->nRegs = fAddFirstPo? 0 : p->nRegs;
|
||||||
|
pNew->nTruePis = fAddFirstPo? Aig_ManPiNum(p) + 1 : p->nTruePis + 1;
|
||||||
|
pNew->nTruePos = fAddFirstPo;
|
||||||
|
// duplicate internal nodes
|
||||||
|
Aig_ManForEachNode( p, pObj, i )
|
||||||
|
pObj->pData = Aig_And( pNew, Aig_ObjChild0Copy(pObj), Aig_ObjChild1Copy(pObj) );
|
||||||
|
// add the PO
|
||||||
|
if ( fAddFirstPo )
|
||||||
|
{
|
||||||
|
pObj = Aig_ManPo( p, 0 );
|
||||||
|
Aig_ObjCreatePo( pNew, Aig_ObjChild0Copy(pObj) );
|
||||||
|
}
|
||||||
|
else
|
||||||
|
{
|
||||||
|
// create register inputs with MUXes
|
||||||
|
Saig_ManForEachLiLo( p, pObjLi, pObjLo, i )
|
||||||
|
{
|
||||||
|
pObj = Aig_Mux( pNew, pCtrl, pObjLo->pData, Aig_ObjChild0Copy(pObjLi) );
|
||||||
|
// pObj = Aig_Mux( pNew, pCtrl, Aig_ManConst0(pNew), Aig_ObjChild0Copy(pObjLi) );
|
||||||
|
Aig_ObjCreatePo( pNew, pObj );
|
||||||
|
}
|
||||||
|
}
|
||||||
|
Aig_ManCleanup( pNew );
|
||||||
|
return pNew;
|
||||||
|
}
|
||||||
|
|
||||||
|
////////////////////////////////////////////////////////////////////////
|
||||||
|
/// END OF FILE ///
|
||||||
|
////////////////////////////////////////////////////////////////////////
|
||||||
|
|
||||||
|
|
||||||
|
|
@ -0,0 +1,103 @@
|
||||||
|
/**CFile****************************************************************
|
||||||
|
|
||||||
|
FileName [intFrames.c]
|
||||||
|
|
||||||
|
SystemName [ABC: Logic synthesis and verification system.]
|
||||||
|
|
||||||
|
PackageName [Interpolation engine.]
|
||||||
|
|
||||||
|
Synopsis [Sequential AIG unrolling for interpolation.]
|
||||||
|
|
||||||
|
Author [Alan Mishchenko]
|
||||||
|
|
||||||
|
Affiliation [UC Berkeley]
|
||||||
|
|
||||||
|
Date [Ver. 1.0. Started - June 24, 2008.]
|
||||||
|
|
||||||
|
Revision [$Id: intFrames.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
|
||||||
|
|
||||||
|
***********************************************************************/
|
||||||
|
|
||||||
|
#include "intInt.h"
|
||||||
|
|
||||||
|
////////////////////////////////////////////////////////////////////////
|
||||||
|
/// DECLARATIONS ///
|
||||||
|
////////////////////////////////////////////////////////////////////////
|
||||||
|
|
||||||
|
////////////////////////////////////////////////////////////////////////
|
||||||
|
/// FUNCTION DEFINITIONS ///
|
||||||
|
////////////////////////////////////////////////////////////////////////
|
||||||
|
|
||||||
|
/**Function*************************************************************
|
||||||
|
|
||||||
|
Synopsis [Create timeframes of the manager for interpolation.]
|
||||||
|
|
||||||
|
Description [The resulting manager is combinational. The primary inputs
|
||||||
|
corresponding to register outputs are ordered first. The only POs of the
|
||||||
|
manager is the property output of the last timeframe.]
|
||||||
|
|
||||||
|
SideEffects []
|
||||||
|
|
||||||
|
SeeAlso []
|
||||||
|
|
||||||
|
***********************************************************************/
|
||||||
|
Aig_Man_t * Inter_ManFramesInter( Aig_Man_t * pAig, int nFrames, int fAddRegOuts )
|
||||||
|
{
|
||||||
|
Aig_Man_t * pFrames;
|
||||||
|
Aig_Obj_t * pObj, * pObjLi, * pObjLo;
|
||||||
|
int i, f;
|
||||||
|
assert( Saig_ManRegNum(pAig) > 0 );
|
||||||
|
assert( Saig_ManPoNum(pAig) == 1 );
|
||||||
|
pFrames = Aig_ManStart( Aig_ManNodeNum(pAig) * nFrames );
|
||||||
|
// map the constant node
|
||||||
|
Aig_ManConst1(pAig)->pData = Aig_ManConst1( pFrames );
|
||||||
|
// create variables for register outputs
|
||||||
|
if ( fAddRegOuts )
|
||||||
|
{
|
||||||
|
Saig_ManForEachLo( pAig, pObj, i )
|
||||||
|
pObj->pData = Aig_ManConst0( pFrames );
|
||||||
|
}
|
||||||
|
else
|
||||||
|
{
|
||||||
|
Saig_ManForEachLo( pAig, pObj, i )
|
||||||
|
pObj->pData = Aig_ObjCreatePi( pFrames );
|
||||||
|
}
|
||||||
|
// add timeframes
|
||||||
|
for ( f = 0; f < nFrames; f++ )
|
||||||
|
{
|
||||||
|
// create PI nodes for this frame
|
||||||
|
Saig_ManForEachPi( pAig, pObj, i )
|
||||||
|
pObj->pData = Aig_ObjCreatePi( pFrames );
|
||||||
|
// add internal nodes of this frame
|
||||||
|
Aig_ManForEachNode( pAig, pObj, i )
|
||||||
|
pObj->pData = Aig_And( pFrames, Aig_ObjChild0Copy(pObj), Aig_ObjChild1Copy(pObj) );
|
||||||
|
if ( f == nFrames - 1 )
|
||||||
|
break;
|
||||||
|
// save register inputs
|
||||||
|
Saig_ManForEachLi( pAig, pObj, i )
|
||||||
|
pObj->pData = Aig_ObjChild0Copy(pObj);
|
||||||
|
// transfer to register outputs
|
||||||
|
Saig_ManForEachLiLo( pAig, pObjLi, pObjLo, i )
|
||||||
|
pObjLo->pData = pObjLi->pData;
|
||||||
|
}
|
||||||
|
// create POs for each register output
|
||||||
|
if ( fAddRegOuts )
|
||||||
|
{
|
||||||
|
Saig_ManForEachLi( pAig, pObj, i )
|
||||||
|
Aig_ObjCreatePo( pFrames, Aig_ObjChild0Copy(pObj) );
|
||||||
|
}
|
||||||
|
// create the only PO of the manager
|
||||||
|
else
|
||||||
|
{
|
||||||
|
pObj = Aig_ManPo( pAig, 0 );
|
||||||
|
Aig_ObjCreatePo( pFrames, Aig_ObjChild0Copy(pObj) );
|
||||||
|
}
|
||||||
|
Aig_ManCleanup( pFrames );
|
||||||
|
return pFrames;
|
||||||
|
}
|
||||||
|
|
||||||
|
////////////////////////////////////////////////////////////////////////
|
||||||
|
/// END OF FILE ///
|
||||||
|
////////////////////////////////////////////////////////////////////////
|
||||||
|
|
||||||
|
|
||||||
|
|
@ -0,0 +1,127 @@
|
||||||
|
/**CFile****************************************************************
|
||||||
|
|
||||||
|
FileName [intInt.h]
|
||||||
|
|
||||||
|
SystemName [ABC: Logic synthesis and verification system.]
|
||||||
|
|
||||||
|
PackageName [Interpolation engine.]
|
||||||
|
|
||||||
|
Synopsis [Internal declarations.]
|
||||||
|
|
||||||
|
Author [Alan Mishchenko]
|
||||||
|
|
||||||
|
Affiliation [UC Berkeley]
|
||||||
|
|
||||||
|
Date [Ver. 1.0. Started - June 24, 2008.]
|
||||||
|
|
||||||
|
Revision [$Id: intInt.h,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
|
||||||
|
|
||||||
|
***********************************************************************/
|
||||||
|
|
||||||
|
#ifndef __INT_INT_H__
|
||||||
|
#define __INT_INT_H__
|
||||||
|
|
||||||
|
#ifdef __cplusplus
|
||||||
|
extern "C" {
|
||||||
|
#endif
|
||||||
|
|
||||||
|
////////////////////////////////////////////////////////////////////////
|
||||||
|
/// INCLUDES ///
|
||||||
|
////////////////////////////////////////////////////////////////////////
|
||||||
|
|
||||||
|
#include "saig.h"
|
||||||
|
#include "cnf.h"
|
||||||
|
#include "satSolver.h"
|
||||||
|
#include "satStore.h"
|
||||||
|
#include "int.h"
|
||||||
|
|
||||||
|
////////////////////////////////////////////////////////////////////////
|
||||||
|
/// PARAMETERS ///
|
||||||
|
////////////////////////////////////////////////////////////////////////
|
||||||
|
|
||||||
|
////////////////////////////////////////////////////////////////////////
|
||||||
|
/// BASIC TYPES ///
|
||||||
|
////////////////////////////////////////////////////////////////////////
|
||||||
|
|
||||||
|
// simulation manager
|
||||||
|
typedef struct Inter_Man_t_ Inter_Man_t;
|
||||||
|
struct Inter_Man_t_
|
||||||
|
{
|
||||||
|
// AIG manager
|
||||||
|
Aig_Man_t * pAig; // the original AIG manager
|
||||||
|
Aig_Man_t * pAigTrans; // the transformed original AIG manager
|
||||||
|
Cnf_Dat_t * pCnfAig; // CNF for the original manager
|
||||||
|
// interpolant
|
||||||
|
Aig_Man_t * pInter; // the current interpolant
|
||||||
|
Cnf_Dat_t * pCnfInter; // CNF for the current interplant
|
||||||
|
// timeframes
|
||||||
|
Aig_Man_t * pFrames; // the timeframes
|
||||||
|
Cnf_Dat_t * pCnfFrames; // CNF for the timeframes
|
||||||
|
// other data
|
||||||
|
Vec_Int_t * vVarsAB; // the variables participating in
|
||||||
|
// temporary place for the new interpolant
|
||||||
|
Aig_Man_t * pInterNew;
|
||||||
|
Vec_Ptr_t * vInters;
|
||||||
|
// parameters
|
||||||
|
int nFrames; // the number of timeframes
|
||||||
|
int nConfCur; // the current number of conflicts
|
||||||
|
int nConfLimit; // the limit on the number of conflicts
|
||||||
|
int fVerbose; // the verbosiness flag
|
||||||
|
// runtime
|
||||||
|
int timeRwr;
|
||||||
|
int timeCnf;
|
||||||
|
int timeSat;
|
||||||
|
int timeInt;
|
||||||
|
int timeEqu;
|
||||||
|
int timeOther;
|
||||||
|
int timeTotal;
|
||||||
|
};
|
||||||
|
|
||||||
|
////////////////////////////////////////////////////////////////////////
|
||||||
|
/// MACRO DEFINITIONS ///
|
||||||
|
////////////////////////////////////////////////////////////////////////
|
||||||
|
|
||||||
|
////////////////////////////////////////////////////////////////////////
|
||||||
|
/// FUNCTION DECLARATIONS ///
|
||||||
|
////////////////////////////////////////////////////////////////////////
|
||||||
|
|
||||||
|
/*=== intContain.c ==========================================================*/
|
||||||
|
extern int Inter_ManCheckContainment( Aig_Man_t * pNew, Aig_Man_t * pOld );
|
||||||
|
extern int Inter_ManCheckEquivalence( Aig_Man_t * pNew, Aig_Man_t * pOld );
|
||||||
|
extern int Inter_ManCheckInductiveContainment( Aig_Man_t * pTrans, Aig_Man_t * pInter, int nSteps, int fBackward );
|
||||||
|
|
||||||
|
/*=== intDup.c ==========================================================*/
|
||||||
|
extern Aig_Man_t * Inter_ManStartInitState( int nRegs );
|
||||||
|
extern Aig_Man_t * Inter_ManStartDuplicated( Aig_Man_t * p );
|
||||||
|
extern Aig_Man_t * Inter_ManStartOneOutput( Aig_Man_t * p, int fAddFirstPo );
|
||||||
|
|
||||||
|
/*=== intFrames.c ==========================================================*/
|
||||||
|
extern Aig_Man_t * Inter_ManFramesInter( Aig_Man_t * pAig, int nFrames, int fAddRegOuts );
|
||||||
|
|
||||||
|
/*=== intMan.c ==========================================================*/
|
||||||
|
extern Inter_Man_t * Inter_ManCreate( Aig_Man_t * pAig, Inter_ManParams_t * pPars );
|
||||||
|
extern void Inter_ManClean( Inter_Man_t * p );
|
||||||
|
extern void Inter_ManStop( Inter_Man_t * p );
|
||||||
|
|
||||||
|
/*=== intM114.c ==========================================================*/
|
||||||
|
extern int Inter_ManPerformOneStep( Inter_Man_t * p, int fUseBias, int fUseBackward );
|
||||||
|
|
||||||
|
/*=== intM114p.c ==========================================================*/
|
||||||
|
#ifdef ABC_USE_LIBRARIES
|
||||||
|
extern int Inter_ManPerformOneStepM114p( Inter_Man_t * p, int fUsePudlak, int fUseOther );
|
||||||
|
#endif
|
||||||
|
|
||||||
|
/*=== intUtil.c ==========================================================*/
|
||||||
|
extern int Inter_ManCheckInitialState( Aig_Man_t * p );
|
||||||
|
extern int Inter_ManCheckAllStates( Aig_Man_t * p );
|
||||||
|
|
||||||
|
#ifdef __cplusplus
|
||||||
|
}
|
||||||
|
#endif
|
||||||
|
|
||||||
|
#endif
|
||||||
|
|
||||||
|
////////////////////////////////////////////////////////////////////////
|
||||||
|
/// END OF FILE ///
|
||||||
|
////////////////////////////////////////////////////////////////////////
|
||||||
|
|
||||||
|
|
@ -0,0 +1,140 @@
|
||||||
|
/**CFile****************************************************************
|
||||||
|
|
||||||
|
FileName [intInter.c]
|
||||||
|
|
||||||
|
SystemName [ABC: Logic synthesis and verification system.]
|
||||||
|
|
||||||
|
PackageName [Interpolation engine.]
|
||||||
|
|
||||||
|
Synopsis [Experimental procedures to derive and compare interpolants.]
|
||||||
|
|
||||||
|
Author [Alan Mishchenko]
|
||||||
|
|
||||||
|
Affiliation [UC Berkeley]
|
||||||
|
|
||||||
|
Date [Ver. 1.0. Started - June 24, 2008.]
|
||||||
|
|
||||||
|
Revision [$Id: intInter.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
|
||||||
|
|
||||||
|
***********************************************************************/
|
||||||
|
|
||||||
|
#include "intInt.h"
|
||||||
|
|
||||||
|
////////////////////////////////////////////////////////////////////////
|
||||||
|
/// DECLARATIONS ///
|
||||||
|
////////////////////////////////////////////////////////////////////////
|
||||||
|
|
||||||
|
////////////////////////////////////////////////////////////////////////
|
||||||
|
/// FUNCTION DEFINITIONS ///
|
||||||
|
////////////////////////////////////////////////////////////////////////
|
||||||
|
|
||||||
|
/**Function*************************************************************
|
||||||
|
|
||||||
|
Synopsis []
|
||||||
|
|
||||||
|
Description []
|
||||||
|
|
||||||
|
SideEffects []
|
||||||
|
|
||||||
|
SeeAlso []
|
||||||
|
|
||||||
|
***********************************************************************/
|
||||||
|
Aig_Man_t * Inter_ManDupExpand( Aig_Man_t * pInter, Aig_Man_t * pOther )
|
||||||
|
{
|
||||||
|
Aig_Man_t * pInterC;
|
||||||
|
assert( Aig_ManPiNum(pInter) <= Aig_ManPiNum(pOther) );
|
||||||
|
pInterC = Aig_ManDupSimple( pInter );
|
||||||
|
Aig_IthVar( pInterC, Aig_ManPiNum(pOther)-1 );
|
||||||
|
assert( Aig_ManPiNum(pInterC) == Aig_ManPiNum(pOther) );
|
||||||
|
return pInterC;
|
||||||
|
}
|
||||||
|
|
||||||
|
/**Function*************************************************************
|
||||||
|
|
||||||
|
Synopsis []
|
||||||
|
|
||||||
|
Description []
|
||||||
|
|
||||||
|
SideEffects []
|
||||||
|
|
||||||
|
SeeAlso []
|
||||||
|
|
||||||
|
***********************************************************************/
|
||||||
|
void Inter_ManVerifyInterpolant1( Inta_Man_t * pMan, Sto_Man_t * pCnf, Aig_Man_t * pInter )
|
||||||
|
{
|
||||||
|
extern Aig_Man_t * Inta_ManDeriveClauses( Inta_Man_t * pMan, Sto_Man_t * pCnf, int fClausesA );
|
||||||
|
Aig_Man_t * pLower, * pUpper, * pInterC;
|
||||||
|
int RetValue1, RetValue2;
|
||||||
|
|
||||||
|
pLower = Inta_ManDeriveClauses( pMan, pCnf, 1 );
|
||||||
|
pUpper = Inta_ManDeriveClauses( pMan, pCnf, 0 );
|
||||||
|
Aig_ManFlipFirstPo( pUpper );
|
||||||
|
|
||||||
|
pInterC = Inter_ManDupExpand( pInter, pLower );
|
||||||
|
RetValue1 = Inter_ManCheckContainment( pLower, pInterC );
|
||||||
|
Aig_ManStop( pInterC );
|
||||||
|
|
||||||
|
pInterC = Inter_ManDupExpand( pInter, pUpper );
|
||||||
|
RetValue2 = Inter_ManCheckContainment( pInterC, pUpper );
|
||||||
|
Aig_ManStop( pInterC );
|
||||||
|
|
||||||
|
if ( RetValue1 && RetValue2 )
|
||||||
|
printf( "Im is correct.\n" );
|
||||||
|
if ( !RetValue1 )
|
||||||
|
printf( "Property A => Im fails.\n" );
|
||||||
|
if ( !RetValue2 )
|
||||||
|
printf( "Property Im => !B fails.\n" );
|
||||||
|
|
||||||
|
Aig_ManStop( pLower );
|
||||||
|
Aig_ManStop( pUpper );
|
||||||
|
}
|
||||||
|
|
||||||
|
/**Function*************************************************************
|
||||||
|
|
||||||
|
Synopsis []
|
||||||
|
|
||||||
|
Description []
|
||||||
|
|
||||||
|
SideEffects []
|
||||||
|
|
||||||
|
SeeAlso []
|
||||||
|
|
||||||
|
***********************************************************************/
|
||||||
|
void Inter_ManVerifyInterpolant2( Intb_Man_t * pMan, Sto_Man_t * pCnf, Aig_Man_t * pInter )
|
||||||
|
{
|
||||||
|
extern Aig_Man_t * Intb_ManDeriveClauses( Intb_Man_t * pMan, Sto_Man_t * pCnf, int fClausesA );
|
||||||
|
Aig_Man_t * pLower, * pUpper, * pInterC;
|
||||||
|
int RetValue1, RetValue2;
|
||||||
|
|
||||||
|
pLower = Intb_ManDeriveClauses( pMan, pCnf, 1 );
|
||||||
|
pUpper = Intb_ManDeriveClauses( pMan, pCnf, 0 );
|
||||||
|
Aig_ManFlipFirstPo( pUpper );
|
||||||
|
|
||||||
|
pInterC = Inter_ManDupExpand( pInter, pLower );
|
||||||
|
//Aig_ManPrintStats( pLower );
|
||||||
|
//Aig_ManPrintStats( pUpper );
|
||||||
|
//Aig_ManPrintStats( pInterC );
|
||||||
|
//Aig_ManDumpBlif( pInterC, "inter_c.blif", NULL, NULL );
|
||||||
|
RetValue1 = Inter_ManCheckContainment( pLower, pInterC );
|
||||||
|
Aig_ManStop( pInterC );
|
||||||
|
|
||||||
|
pInterC = Inter_ManDupExpand( pInter, pUpper );
|
||||||
|
RetValue2 = Inter_ManCheckContainment( pInterC, pUpper );
|
||||||
|
Aig_ManStop( pInterC );
|
||||||
|
|
||||||
|
if ( RetValue1 && RetValue2 )
|
||||||
|
printf( "Ip is correct.\n" );
|
||||||
|
if ( !RetValue1 )
|
||||||
|
printf( "Property A => Ip fails.\n" );
|
||||||
|
if ( !RetValue2 )
|
||||||
|
printf( "Property Ip => !B fails.\n" );
|
||||||
|
|
||||||
|
Aig_ManStop( pLower );
|
||||||
|
Aig_ManStop( pUpper );
|
||||||
|
}
|
||||||
|
|
||||||
|
////////////////////////////////////////////////////////////////////////
|
||||||
|
/// END OF FILE ///
|
||||||
|
////////////////////////////////////////////////////////////////////////
|
||||||
|
|
||||||
|
|
||||||
|
|
@ -0,0 +1,311 @@
|
||||||
|
/**CFile****************************************************************
|
||||||
|
|
||||||
|
FileName [intM114.c]
|
||||||
|
|
||||||
|
SystemName [ABC: Logic synthesis and verification system.]
|
||||||
|
|
||||||
|
PackageName [Interpolation engine.]
|
||||||
|
|
||||||
|
Synopsis [Intepolation using ABC's proof generator added to MiniSat-1.14c.]
|
||||||
|
|
||||||
|
Author [Alan Mishchenko]
|
||||||
|
|
||||||
|
Affiliation [UC Berkeley]
|
||||||
|
|
||||||
|
Date [Ver. 1.0. Started - June 24, 2008.]
|
||||||
|
|
||||||
|
Revision [$Id: intM114.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
|
||||||
|
|
||||||
|
***********************************************************************/
|
||||||
|
|
||||||
|
#include "intInt.h"
|
||||||
|
|
||||||
|
////////////////////////////////////////////////////////////////////////
|
||||||
|
/// DECLARATIONS ///
|
||||||
|
////////////////////////////////////////////////////////////////////////
|
||||||
|
|
||||||
|
////////////////////////////////////////////////////////////////////////
|
||||||
|
/// FUNCTION DEFINITIONS ///
|
||||||
|
////////////////////////////////////////////////////////////////////////
|
||||||
|
|
||||||
|
/**Function*************************************************************
|
||||||
|
|
||||||
|
Synopsis [Returns the SAT solver for one interpolation run.]
|
||||||
|
|
||||||
|
Description [pInter is the previous interpolant. pAig is one time frame.
|
||||||
|
pFrames is the unrolled time frames.]
|
||||||
|
|
||||||
|
SideEffects []
|
||||||
|
|
||||||
|
SeeAlso []
|
||||||
|
|
||||||
|
***********************************************************************/
|
||||||
|
sat_solver * Inter_ManDeriveSatSolver(
|
||||||
|
Aig_Man_t * pInter, Cnf_Dat_t * pCnfInter,
|
||||||
|
Aig_Man_t * pAig, Cnf_Dat_t * pCnfAig,
|
||||||
|
Aig_Man_t * pFrames, Cnf_Dat_t * pCnfFrames,
|
||||||
|
Vec_Int_t * vVarsAB, int fUseBackward )
|
||||||
|
{
|
||||||
|
sat_solver * pSat;
|
||||||
|
Aig_Obj_t * pObj, * pObj2;
|
||||||
|
int i, Lits[2];
|
||||||
|
|
||||||
|
//Aig_ManDumpBlif( pInter, "out_inter.blif", NULL, NULL );
|
||||||
|
//Aig_ManDumpBlif( pAig, "out_aig.blif", NULL, NULL );
|
||||||
|
//Aig_ManDumpBlif( pFrames, "out_frames.blif", NULL, NULL );
|
||||||
|
|
||||||
|
// sanity checks
|
||||||
|
assert( Aig_ManRegNum(pInter) == 0 );
|
||||||
|
assert( Aig_ManRegNum(pAig) > 0 );
|
||||||
|
assert( Aig_ManRegNum(pFrames) == 0 );
|
||||||
|
assert( Aig_ManPoNum(pInter) == 1 );
|
||||||
|
assert( Aig_ManPoNum(pFrames) == fUseBackward? Saig_ManRegNum(pAig) : 1 );
|
||||||
|
assert( fUseBackward || Aig_ManPiNum(pInter) == Aig_ManRegNum(pAig) );
|
||||||
|
// assert( (Aig_ManPiNum(pFrames) - Aig_ManRegNum(pAig)) % Saig_ManPiNum(pAig) == 0 );
|
||||||
|
|
||||||
|
// prepare CNFs
|
||||||
|
Cnf_DataLift( pCnfAig, pCnfFrames->nVars );
|
||||||
|
Cnf_DataLift( pCnfInter, pCnfFrames->nVars + pCnfAig->nVars );
|
||||||
|
|
||||||
|
// start the solver
|
||||||
|
pSat = sat_solver_new();
|
||||||
|
sat_solver_store_alloc( pSat );
|
||||||
|
sat_solver_setnvars( pSat, pCnfInter->nVars + pCnfAig->nVars + pCnfFrames->nVars );
|
||||||
|
|
||||||
|
// add clauses of A
|
||||||
|
// interpolant
|
||||||
|
for ( i = 0; i < pCnfInter->nClauses; i++ )
|
||||||
|
{
|
||||||
|
if ( !sat_solver_addclause( pSat, pCnfInter->pClauses[i], pCnfInter->pClauses[i+1] ) )
|
||||||
|
{
|
||||||
|
sat_solver_delete( pSat );
|
||||||
|
// return clauses to the original state
|
||||||
|
Cnf_DataLift( pCnfAig, -pCnfFrames->nVars );
|
||||||
|
Cnf_DataLift( pCnfInter, -pCnfFrames->nVars -pCnfAig->nVars );
|
||||||
|
return NULL;
|
||||||
|
}
|
||||||
|
}
|
||||||
|
// connector clauses
|
||||||
|
if ( fUseBackward )
|
||||||
|
{
|
||||||
|
Saig_ManForEachLi( pAig, pObj2, i )
|
||||||
|
{
|
||||||
|
if ( Saig_ManRegNum(pAig) == Aig_ManPiNum(pInter) )
|
||||||
|
pObj = Aig_ManPi( pInter, i );
|
||||||
|
else
|
||||||
|
{
|
||||||
|
assert( Aig_ManPiNum(pAig) == Aig_ManPiNum(pInter) );
|
||||||
|
pObj = Aig_ManPi( pInter, Aig_ManPiNum(pAig)-Saig_ManRegNum(pAig) + i );
|
||||||
|
}
|
||||||
|
|
||||||
|
Lits[0] = toLitCond( pCnfInter->pVarNums[pObj->Id], 0 );
|
||||||
|
Lits[1] = toLitCond( pCnfAig->pVarNums[pObj2->Id], 1 );
|
||||||
|
if ( !sat_solver_addclause( pSat, Lits, Lits+2 ) )
|
||||||
|
assert( 0 );
|
||||||
|
Lits[0] = toLitCond( pCnfInter->pVarNums[pObj->Id], 1 );
|
||||||
|
Lits[1] = toLitCond( pCnfAig->pVarNums[pObj2->Id], 0 );
|
||||||
|
if ( !sat_solver_addclause( pSat, Lits, Lits+2 ) )
|
||||||
|
assert( 0 );
|
||||||
|
}
|
||||||
|
}
|
||||||
|
else
|
||||||
|
{
|
||||||
|
Aig_ManForEachPi( pInter, pObj, i )
|
||||||
|
{
|
||||||
|
pObj2 = Saig_ManLo( pAig, i );
|
||||||
|
|
||||||
|
Lits[0] = toLitCond( pCnfInter->pVarNums[pObj->Id], 0 );
|
||||||
|
Lits[1] = toLitCond( pCnfAig->pVarNums[pObj2->Id], 1 );
|
||||||
|
if ( !sat_solver_addclause( pSat, Lits, Lits+2 ) )
|
||||||
|
assert( 0 );
|
||||||
|
Lits[0] = toLitCond( pCnfInter->pVarNums[pObj->Id], 1 );
|
||||||
|
Lits[1] = toLitCond( pCnfAig->pVarNums[pObj2->Id], 0 );
|
||||||
|
if ( !sat_solver_addclause( pSat, Lits, Lits+2 ) )
|
||||||
|
assert( 0 );
|
||||||
|
}
|
||||||
|
}
|
||||||
|
// one timeframe
|
||||||
|
for ( i = 0; i < pCnfAig->nClauses; i++ )
|
||||||
|
{
|
||||||
|
if ( !sat_solver_addclause( pSat, pCnfAig->pClauses[i], pCnfAig->pClauses[i+1] ) )
|
||||||
|
assert( 0 );
|
||||||
|
}
|
||||||
|
// connector clauses
|
||||||
|
Vec_IntClear( vVarsAB );
|
||||||
|
if ( fUseBackward )
|
||||||
|
{
|
||||||
|
Aig_ManForEachPo( pFrames, pObj, i )
|
||||||
|
{
|
||||||
|
assert( pCnfFrames->pVarNums[pObj->Id] >= 0 );
|
||||||
|
Vec_IntPush( vVarsAB, pCnfFrames->pVarNums[pObj->Id] );
|
||||||
|
|
||||||
|
pObj2 = Saig_ManLo( pAig, i );
|
||||||
|
Lits[0] = toLitCond( pCnfFrames->pVarNums[pObj->Id], 0 );
|
||||||
|
Lits[1] = toLitCond( pCnfAig->pVarNums[pObj2->Id], 1 );
|
||||||
|
if ( !sat_solver_addclause( pSat, Lits, Lits+2 ) )
|
||||||
|
assert( 0 );
|
||||||
|
Lits[0] = toLitCond( pCnfFrames->pVarNums[pObj->Id], 1 );
|
||||||
|
Lits[1] = toLitCond( pCnfAig->pVarNums[pObj2->Id], 0 );
|
||||||
|
if ( !sat_solver_addclause( pSat, Lits, Lits+2 ) )
|
||||||
|
assert( 0 );
|
||||||
|
}
|
||||||
|
}
|
||||||
|
else
|
||||||
|
{
|
||||||
|
Aig_ManForEachPi( pFrames, pObj, i )
|
||||||
|
{
|
||||||
|
if ( i == Aig_ManRegNum(pAig) )
|
||||||
|
break;
|
||||||
|
Vec_IntPush( vVarsAB, pCnfFrames->pVarNums[pObj->Id] );
|
||||||
|
|
||||||
|
pObj2 = Saig_ManLi( pAig, i );
|
||||||
|
Lits[0] = toLitCond( pCnfFrames->pVarNums[pObj->Id], 0 );
|
||||||
|
Lits[1] = toLitCond( pCnfAig->pVarNums[pObj2->Id], 1 );
|
||||||
|
if ( !sat_solver_addclause( pSat, Lits, Lits+2 ) )
|
||||||
|
assert( 0 );
|
||||||
|
Lits[0] = toLitCond( pCnfFrames->pVarNums[pObj->Id], 1 );
|
||||||
|
Lits[1] = toLitCond( pCnfAig->pVarNums[pObj2->Id], 0 );
|
||||||
|
if ( !sat_solver_addclause( pSat, Lits, Lits+2 ) )
|
||||||
|
assert( 0 );
|
||||||
|
}
|
||||||
|
}
|
||||||
|
// add clauses of B
|
||||||
|
sat_solver_store_mark_clauses_a( pSat );
|
||||||
|
for ( i = 0; i < pCnfFrames->nClauses; i++ )
|
||||||
|
{
|
||||||
|
if ( !sat_solver_addclause( pSat, pCnfFrames->pClauses[i], pCnfFrames->pClauses[i+1] ) )
|
||||||
|
{
|
||||||
|
pSat->fSolved = 1;
|
||||||
|
break;
|
||||||
|
}
|
||||||
|
}
|
||||||
|
sat_solver_store_mark_roots( pSat );
|
||||||
|
// return clauses to the original state
|
||||||
|
Cnf_DataLift( pCnfAig, -pCnfFrames->nVars );
|
||||||
|
Cnf_DataLift( pCnfInter, -pCnfFrames->nVars -pCnfAig->nVars );
|
||||||
|
return pSat;
|
||||||
|
}
|
||||||
|
|
||||||
|
/**Function*************************************************************
|
||||||
|
|
||||||
|
Synopsis [Performs one SAT run with interpolation.]
|
||||||
|
|
||||||
|
Description [Returns 1 if proven. 0 if failed. -1 if undecided.]
|
||||||
|
|
||||||
|
SideEffects []
|
||||||
|
|
||||||
|
SeeAlso []
|
||||||
|
|
||||||
|
***********************************************************************/
|
||||||
|
int Inter_ManPerformOneStep( Inter_Man_t * p, int fUseBias, int fUseBackward )
|
||||||
|
{
|
||||||
|
sat_solver * pSat;
|
||||||
|
void * pSatCnf = NULL;
|
||||||
|
Inta_Man_t * pManInterA;
|
||||||
|
// Intb_Man_t * pManInterB;
|
||||||
|
int * pGlobalVars;
|
||||||
|
int clk, status, RetValue;
|
||||||
|
int i, Var;
|
||||||
|
assert( p->pInterNew == NULL );
|
||||||
|
|
||||||
|
// derive the SAT solver
|
||||||
|
pSat = Inter_ManDeriveSatSolver( p->pInter, p->pCnfInter, p->pAigTrans, p->pCnfAig, p->pFrames, p->pCnfFrames, p->vVarsAB, fUseBackward );
|
||||||
|
if ( pSat == NULL )
|
||||||
|
{
|
||||||
|
p->pInterNew = NULL;
|
||||||
|
return 1;
|
||||||
|
}
|
||||||
|
|
||||||
|
// collect global variables
|
||||||
|
pGlobalVars = CALLOC( int, sat_solver_nvars(pSat) );
|
||||||
|
Vec_IntForEachEntry( p->vVarsAB, Var, i )
|
||||||
|
pGlobalVars[Var] = 1;
|
||||||
|
pSat->pGlobalVars = fUseBias? pGlobalVars : NULL;
|
||||||
|
|
||||||
|
// solve the problem
|
||||||
|
clk = clock();
|
||||||
|
status = sat_solver_solve( pSat, NULL, NULL, (sint64)p->nConfLimit, (sint64)0, (sint64)0, (sint64)0 );
|
||||||
|
p->nConfCur = pSat->stats.conflicts;
|
||||||
|
p->timeSat += clock() - clk;
|
||||||
|
|
||||||
|
pSat->pGlobalVars = NULL;
|
||||||
|
FREE( pGlobalVars );
|
||||||
|
if ( status == l_False )
|
||||||
|
{
|
||||||
|
pSatCnf = sat_solver_store_release( pSat );
|
||||||
|
RetValue = 1;
|
||||||
|
}
|
||||||
|
else if ( status == l_True )
|
||||||
|
{
|
||||||
|
RetValue = 0;
|
||||||
|
}
|
||||||
|
else
|
||||||
|
{
|
||||||
|
RetValue = -1;
|
||||||
|
}
|
||||||
|
sat_solver_delete( pSat );
|
||||||
|
if ( pSatCnf == NULL )
|
||||||
|
return RetValue;
|
||||||
|
|
||||||
|
// create the resulting manager
|
||||||
|
clk = clock();
|
||||||
|
/*
|
||||||
|
if ( !fUseIp )
|
||||||
|
{
|
||||||
|
pManInterA = Inta_ManAlloc();
|
||||||
|
p->pInterNew = Inta_ManInterpolate( pManInterA, pSatCnf, p->vVarsAB, 0 );
|
||||||
|
Inta_ManFree( pManInterA );
|
||||||
|
}
|
||||||
|
else
|
||||||
|
{
|
||||||
|
Aig_Man_t * pInterNew2;
|
||||||
|
int RetValue;
|
||||||
|
|
||||||
|
pManInterA = Inta_ManAlloc();
|
||||||
|
p->pInterNew = Inta_ManInterpolate( pManInterA, pSatCnf, p->vVarsAB, 0 );
|
||||||
|
// Inter_ManVerifyInterpolant1( pManInterA, pSatCnf, p->pInterNew );
|
||||||
|
Inta_ManFree( pManInterA );
|
||||||
|
|
||||||
|
pManInterB = Intb_ManAlloc();
|
||||||
|
pInterNew2 = Intb_ManInterpolate( pManInterB, pSatCnf, p->vVarsAB, 0 );
|
||||||
|
Inter_ManVerifyInterpolant2( pManInterB, pSatCnf, pInterNew2 );
|
||||||
|
Intb_ManFree( pManInterB );
|
||||||
|
|
||||||
|
// check relationship
|
||||||
|
RetValue = Inter_ManCheckEquivalence( pInterNew2, p->pInterNew );
|
||||||
|
if ( RetValue )
|
||||||
|
printf( "Equivalence \"Ip == Im\" holds\n" );
|
||||||
|
else
|
||||||
|
{
|
||||||
|
// printf( "Equivalence \"Ip == Im\" does not hold\n" );
|
||||||
|
RetValue = Inter_ManCheckContainment( pInterNew2, p->pInterNew );
|
||||||
|
if ( RetValue )
|
||||||
|
printf( "Containment \"Ip -> Im\" holds\n" );
|
||||||
|
else
|
||||||
|
printf( "Containment \"Ip -> Im\" does not hold\n" );
|
||||||
|
|
||||||
|
RetValue = Inter_ManCheckContainment( p->pInterNew, pInterNew2 );
|
||||||
|
if ( RetValue )
|
||||||
|
printf( "Containment \"Im -> Ip\" holds\n" );
|
||||||
|
else
|
||||||
|
printf( "Containment \"Im -> Ip\" does not hold\n" );
|
||||||
|
}
|
||||||
|
|
||||||
|
Aig_ManStop( pInterNew2 );
|
||||||
|
}
|
||||||
|
*/
|
||||||
|
|
||||||
|
pManInterA = Inta_ManAlloc();
|
||||||
|
p->pInterNew = Inta_ManInterpolate( pManInterA, pSatCnf, p->vVarsAB, 0 );
|
||||||
|
Inta_ManFree( pManInterA );
|
||||||
|
|
||||||
|
p->timeInt += clock() - clk;
|
||||||
|
Sto_ManFree( pSatCnf );
|
||||||
|
return RetValue;
|
||||||
|
}
|
||||||
|
|
||||||
|
////////////////////////////////////////////////////////////////////////
|
||||||
|
/// END OF FILE ///
|
||||||
|
////////////////////////////////////////////////////////////////////////
|
||||||
|
|
||||||
|
|
||||||
|
|
@ -0,0 +1,435 @@
|
||||||
|
/**CFile****************************************************************
|
||||||
|
|
||||||
|
FileName [intM114p.c]
|
||||||
|
|
||||||
|
SystemName [ABC: Logic synthesis and verification system.]
|
||||||
|
|
||||||
|
PackageName [Interpolation engine.]
|
||||||
|
|
||||||
|
Synopsis [Intepolation using interfaced to MiniSat-1.14p.]
|
||||||
|
|
||||||
|
Author [Alan Mishchenko]
|
||||||
|
|
||||||
|
Affiliation [UC Berkeley]
|
||||||
|
|
||||||
|
Date [Ver. 1.0. Started - June 24, 2008.]
|
||||||
|
|
||||||
|
Revision [$Id: intM114p.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
|
||||||
|
|
||||||
|
***********************************************************************/
|
||||||
|
|
||||||
|
#ifdef ABC_USE_LIBRARIES
|
||||||
|
|
||||||
|
#include "intInt.h"
|
||||||
|
#include "m114p.h"
|
||||||
|
|
||||||
|
////////////////////////////////////////////////////////////////////////
|
||||||
|
/// DECLARATIONS ///
|
||||||
|
////////////////////////////////////////////////////////////////////////
|
||||||
|
|
||||||
|
////////////////////////////////////////////////////////////////////////
|
||||||
|
/// FUNCTION DEFINITIONS ///
|
||||||
|
////////////////////////////////////////////////////////////////////////
|
||||||
|
|
||||||
|
/**Function*************************************************************
|
||||||
|
|
||||||
|
Synopsis [Returns the SAT solver for one interpolation run.]
|
||||||
|
|
||||||
|
Description [pInter is the previous interpolant. pAig is one time frame.
|
||||||
|
pFrames is the unrolled time frames.]
|
||||||
|
|
||||||
|
SideEffects []
|
||||||
|
|
||||||
|
SeeAlso []
|
||||||
|
|
||||||
|
***********************************************************************/
|
||||||
|
M114p_Solver_t Inter_ManDeriveSatSolverM114p(
|
||||||
|
Aig_Man_t * pInter, Cnf_Dat_t * pCnfInter,
|
||||||
|
Aig_Man_t * pAig, Cnf_Dat_t * pCnfAig,
|
||||||
|
Aig_Man_t * pFrames, Cnf_Dat_t * pCnfFrames,
|
||||||
|
Vec_Int_t ** pvMapRoots, Vec_Int_t ** pvMapVars )
|
||||||
|
{
|
||||||
|
M114p_Solver_t pSat;
|
||||||
|
Aig_Obj_t * pObj, * pObj2;
|
||||||
|
int i, Lits[2];
|
||||||
|
|
||||||
|
// sanity checks
|
||||||
|
assert( Aig_ManRegNum(pInter) == 0 );
|
||||||
|
assert( Aig_ManRegNum(pAig) > 0 );
|
||||||
|
assert( Aig_ManRegNum(pFrames) == 0 );
|
||||||
|
assert( Aig_ManPoNum(pInter) == 1 );
|
||||||
|
assert( Aig_ManPoNum(pFrames) == 1 );
|
||||||
|
assert( Aig_ManPiNum(pInter) == Aig_ManRegNum(pAig) );
|
||||||
|
// assert( (Aig_ManPiNum(pFrames) - Aig_ManRegNum(pAig)) % Saig_ManPiNum(pAig) == 0 );
|
||||||
|
|
||||||
|
// prepare CNFs
|
||||||
|
Cnf_DataLift( pCnfAig, pCnfFrames->nVars );
|
||||||
|
Cnf_DataLift( pCnfInter, pCnfFrames->nVars + pCnfAig->nVars );
|
||||||
|
|
||||||
|
*pvMapRoots = Vec_IntAlloc( 10000 );
|
||||||
|
*pvMapVars = Vec_IntAlloc( 0 );
|
||||||
|
Vec_IntFill( *pvMapVars, pCnfInter->nVars + pCnfAig->nVars + pCnfFrames->nVars, -1 );
|
||||||
|
for ( i = 0; i < pCnfFrames->nVars; i++ )
|
||||||
|
Vec_IntWriteEntry( *pvMapVars, i, -2 );
|
||||||
|
|
||||||
|
// start the solver
|
||||||
|
pSat = M114p_SolverNew( 1 );
|
||||||
|
M114p_SolverSetVarNum( pSat, pCnfInter->nVars + pCnfAig->nVars + pCnfFrames->nVars );
|
||||||
|
|
||||||
|
// add clauses of A
|
||||||
|
// interpolant
|
||||||
|
for ( i = 0; i < pCnfInter->nClauses; i++ )
|
||||||
|
{
|
||||||
|
Vec_IntPush( *pvMapRoots, 0 );
|
||||||
|
if ( !M114p_SolverAddClause( pSat, pCnfInter->pClauses[i], pCnfInter->pClauses[i+1] ) )
|
||||||
|
assert( 0 );
|
||||||
|
}
|
||||||
|
// connector clauses
|
||||||
|
Aig_ManForEachPi( pInter, pObj, i )
|
||||||
|
{
|
||||||
|
pObj2 = Saig_ManLo( pAig, i );
|
||||||
|
Lits[0] = toLitCond( pCnfInter->pVarNums[pObj->Id], 0 );
|
||||||
|
Lits[1] = toLitCond( pCnfAig->pVarNums[pObj2->Id], 1 );
|
||||||
|
Vec_IntPush( *pvMapRoots, 0 );
|
||||||
|
if ( !M114p_SolverAddClause( pSat, Lits, Lits+2 ) )
|
||||||
|
assert( 0 );
|
||||||
|
Lits[0] = toLitCond( pCnfInter->pVarNums[pObj->Id], 1 );
|
||||||
|
Lits[1] = toLitCond( pCnfAig->pVarNums[pObj2->Id], 0 );
|
||||||
|
Vec_IntPush( *pvMapRoots, 0 );
|
||||||
|
if ( !M114p_SolverAddClause( pSat, Lits, Lits+2 ) )
|
||||||
|
assert( 0 );
|
||||||
|
}
|
||||||
|
// one timeframe
|
||||||
|
for ( i = 0; i < pCnfAig->nClauses; i++ )
|
||||||
|
{
|
||||||
|
Vec_IntPush( *pvMapRoots, 0 );
|
||||||
|
if ( !M114p_SolverAddClause( pSat, pCnfAig->pClauses[i], pCnfAig->pClauses[i+1] ) )
|
||||||
|
assert( 0 );
|
||||||
|
}
|
||||||
|
// connector clauses
|
||||||
|
Aig_ManForEachPi( pFrames, pObj, i )
|
||||||
|
{
|
||||||
|
if ( i == Aig_ManRegNum(pAig) )
|
||||||
|
break;
|
||||||
|
// Vec_IntPush( vVarsAB, pCnfFrames->pVarNums[pObj->Id] );
|
||||||
|
Vec_IntWriteEntry( *pvMapVars, pCnfFrames->pVarNums[pObj->Id], i );
|
||||||
|
|
||||||
|
pObj2 = Saig_ManLi( pAig, i );
|
||||||
|
Lits[0] = toLitCond( pCnfFrames->pVarNums[pObj->Id], 0 );
|
||||||
|
Lits[1] = toLitCond( pCnfAig->pVarNums[pObj2->Id], 1 );
|
||||||
|
Vec_IntPush( *pvMapRoots, 0 );
|
||||||
|
if ( !M114p_SolverAddClause( pSat, Lits, Lits+2 ) )
|
||||||
|
assert( 0 );
|
||||||
|
Lits[0] = toLitCond( pCnfFrames->pVarNums[pObj->Id], 1 );
|
||||||
|
Lits[1] = toLitCond( pCnfAig->pVarNums[pObj2->Id], 0 );
|
||||||
|
Vec_IntPush( *pvMapRoots, 0 );
|
||||||
|
if ( !M114p_SolverAddClause( pSat, Lits, Lits+2 ) )
|
||||||
|
assert( 0 );
|
||||||
|
}
|
||||||
|
// add clauses of B
|
||||||
|
for ( i = 0; i < pCnfFrames->nClauses; i++ )
|
||||||
|
{
|
||||||
|
Vec_IntPush( *pvMapRoots, 1 );
|
||||||
|
if ( !M114p_SolverAddClause( pSat, pCnfFrames->pClauses[i], pCnfFrames->pClauses[i+1] ) )
|
||||||
|
{
|
||||||
|
// assert( 0 );
|
||||||
|
break;
|
||||||
|
}
|
||||||
|
}
|
||||||
|
// return clauses to the original state
|
||||||
|
Cnf_DataLift( pCnfAig, -pCnfFrames->nVars );
|
||||||
|
Cnf_DataLift( pCnfInter, -pCnfFrames->nVars -pCnfAig->nVars );
|
||||||
|
return pSat;
|
||||||
|
}
|
||||||
|
|
||||||
|
|
||||||
|
/**Function*************************************************************
|
||||||
|
|
||||||
|
Synopsis [Performs one resolution step.]
|
||||||
|
|
||||||
|
Description []
|
||||||
|
|
||||||
|
SideEffects []
|
||||||
|
|
||||||
|
SeeAlso []
|
||||||
|
|
||||||
|
***********************************************************************/
|
||||||
|
int Inter_ManResolveM114p( Vec_Int_t * vResolvent, int * pLits, int nLits, int iVar )
|
||||||
|
{
|
||||||
|
int i, k, iLit = -1, fFound = 0;
|
||||||
|
// find the variable in the clause
|
||||||
|
for ( i = 0; i < vResolvent->nSize; i++ )
|
||||||
|
if ( lit_var(vResolvent->pArray[i]) == iVar )
|
||||||
|
{
|
||||||
|
iLit = vResolvent->pArray[i];
|
||||||
|
vResolvent->pArray[i] = vResolvent->pArray[--vResolvent->nSize];
|
||||||
|
break;
|
||||||
|
}
|
||||||
|
assert( iLit != -1 );
|
||||||
|
// add other variables
|
||||||
|
for ( i = 0; i < nLits; i++ )
|
||||||
|
{
|
||||||
|
if ( lit_var(pLits[i]) == iVar )
|
||||||
|
{
|
||||||
|
assert( iLit == lit_neg(pLits[i]) );
|
||||||
|
fFound = 1;
|
||||||
|
continue;
|
||||||
|
}
|
||||||
|
// check if this literal appears
|
||||||
|
for ( k = 0; k < vResolvent->nSize; k++ )
|
||||||
|
if ( vResolvent->pArray[k] == pLits[i] )
|
||||||
|
break;
|
||||||
|
if ( k < vResolvent->nSize )
|
||||||
|
continue;
|
||||||
|
// add this literal
|
||||||
|
Vec_IntPush( vResolvent, pLits[i] );
|
||||||
|
}
|
||||||
|
assert( fFound );
|
||||||
|
return 1;
|
||||||
|
}
|
||||||
|
|
||||||
|
/**Function*************************************************************
|
||||||
|
|
||||||
|
Synopsis [Computes interpolant using MiniSat-1.14p.]
|
||||||
|
|
||||||
|
Description [Assumes that the solver returned UNSAT and proof
|
||||||
|
logging was enabled. Array vMapRoots maps number of each root clause
|
||||||
|
into 0 (clause of A) or 1 (clause of B). Array vMapVars maps each SAT
|
||||||
|
solver variable into -1 (var of A), -2 (var of B), and <num> (var of C),
|
||||||
|
where <num> is the var's 0-based number in the ordering of C variables.]
|
||||||
|
|
||||||
|
SideEffects []
|
||||||
|
|
||||||
|
SeeAlso []
|
||||||
|
|
||||||
|
***********************************************************************/
|
||||||
|
Aig_Man_t * Inter_ManInterpolateM114pPudlak( M114p_Solver_t s, Vec_Int_t * vMapRoots, Vec_Int_t * vMapVars )
|
||||||
|
{
|
||||||
|
Aig_Man_t * p;
|
||||||
|
Aig_Obj_t * pInter, * pInter2, * pVar;
|
||||||
|
Vec_Ptr_t * vInters;
|
||||||
|
Vec_Int_t * vLiterals, * vClauses, * vResolvent;
|
||||||
|
int * pLitsNext, nLitsNext, nOffset, iLit;
|
||||||
|
int * pLits, * pClauses, * pVars;
|
||||||
|
int nLits, nVars, i, k, v, iVar;
|
||||||
|
assert( M114p_SolverProofIsReady(s) );
|
||||||
|
vInters = Vec_PtrAlloc( 1000 );
|
||||||
|
|
||||||
|
vLiterals = Vec_IntAlloc( 10000 );
|
||||||
|
vClauses = Vec_IntAlloc( 1000 );
|
||||||
|
vResolvent = Vec_IntAlloc( 100 );
|
||||||
|
|
||||||
|
// create elementary variables
|
||||||
|
p = Aig_ManStart( 10000 );
|
||||||
|
Vec_IntForEachEntry( vMapVars, iVar, i )
|
||||||
|
if ( iVar >= 0 )
|
||||||
|
Aig_IthVar(p, iVar);
|
||||||
|
// process root clauses
|
||||||
|
M114p_SolverForEachRoot( s, &pLits, nLits, i )
|
||||||
|
{
|
||||||
|
if ( Vec_IntEntry(vMapRoots, i) == 1 ) // clause of B
|
||||||
|
pInter = Aig_ManConst1(p);
|
||||||
|
else // clause of A
|
||||||
|
pInter = Aig_ManConst0(p);
|
||||||
|
Vec_PtrPush( vInters, pInter );
|
||||||
|
|
||||||
|
// save the root clause
|
||||||
|
Vec_IntPush( vClauses, Vec_IntSize(vLiterals) );
|
||||||
|
Vec_IntPush( vLiterals, nLits );
|
||||||
|
for ( v = 0; v < nLits; v++ )
|
||||||
|
Vec_IntPush( vLiterals, pLits[v] );
|
||||||
|
}
|
||||||
|
assert( Vec_PtrSize(vInters) == Vec_IntSize(vMapRoots) );
|
||||||
|
|
||||||
|
// process learned clauses
|
||||||
|
M114p_SolverForEachChain( s, &pClauses, &pVars, nVars, i )
|
||||||
|
{
|
||||||
|
pInter = Vec_PtrEntry( vInters, pClauses[0] );
|
||||||
|
|
||||||
|
// initialize the resolvent
|
||||||
|
nOffset = Vec_IntEntry( vClauses, pClauses[0] );
|
||||||
|
nLitsNext = Vec_IntEntry( vLiterals, nOffset );
|
||||||
|
pLitsNext = Vec_IntArray(vLiterals) + nOffset + 1;
|
||||||
|
Vec_IntClear( vResolvent );
|
||||||
|
for ( v = 0; v < nLitsNext; v++ )
|
||||||
|
Vec_IntPush( vResolvent, pLitsNext[v] );
|
||||||
|
|
||||||
|
for ( k = 0; k < nVars; k++ )
|
||||||
|
{
|
||||||
|
iVar = Vec_IntEntry( vMapVars, pVars[k] );
|
||||||
|
pInter2 = Vec_PtrEntry( vInters, pClauses[k+1] );
|
||||||
|
|
||||||
|
// resolve it with the next clause
|
||||||
|
nOffset = Vec_IntEntry( vClauses, pClauses[k+1] );
|
||||||
|
nLitsNext = Vec_IntEntry( vLiterals, nOffset );
|
||||||
|
pLitsNext = Vec_IntArray(vLiterals) + nOffset + 1;
|
||||||
|
Inter_ManResolveM114p( vResolvent, pLitsNext, nLitsNext, pVars[k] );
|
||||||
|
|
||||||
|
if ( iVar == -1 ) // var of A
|
||||||
|
pInter = Aig_Or( p, pInter, pInter2 );
|
||||||
|
else if ( iVar == -2 ) // var of B
|
||||||
|
pInter = Aig_And( p, pInter, pInter2 );
|
||||||
|
else // var of C
|
||||||
|
{
|
||||||
|
// check polarity of the pivot variable in the clause
|
||||||
|
for ( v = 0; v < nLitsNext; v++ )
|
||||||
|
if ( lit_var(pLitsNext[v]) == pVars[k] )
|
||||||
|
break;
|
||||||
|
assert( v < nLitsNext );
|
||||||
|
pVar = Aig_NotCond( Aig_IthVar(p, iVar), lit_sign(pLitsNext[v]) );
|
||||||
|
pInter = Aig_Mux( p, pVar, pInter, pInter2 );
|
||||||
|
}
|
||||||
|
}
|
||||||
|
Vec_PtrPush( vInters, pInter );
|
||||||
|
|
||||||
|
// store the resulting clause
|
||||||
|
Vec_IntPush( vClauses, Vec_IntSize(vLiterals) );
|
||||||
|
Vec_IntPush( vLiterals, Vec_IntSize(vResolvent) );
|
||||||
|
Vec_IntForEachEntry( vResolvent, iLit, v )
|
||||||
|
Vec_IntPush( vLiterals, iLit );
|
||||||
|
}
|
||||||
|
assert( Vec_PtrSize(vInters) == M114p_SolverProofClauseNum(s) );
|
||||||
|
assert( Vec_IntSize(vResolvent) == 0 ); // the empty clause
|
||||||
|
Vec_PtrFree( vInters );
|
||||||
|
Vec_IntFree( vLiterals );
|
||||||
|
Vec_IntFree( vClauses );
|
||||||
|
Vec_IntFree( vResolvent );
|
||||||
|
Aig_ObjCreatePo( p, pInter );
|
||||||
|
Aig_ManCleanup( p );
|
||||||
|
return p;
|
||||||
|
}
|
||||||
|
|
||||||
|
|
||||||
|
/**Function*************************************************************
|
||||||
|
|
||||||
|
Synopsis [Computes interpolant using MiniSat-1.14p.]
|
||||||
|
|
||||||
|
Description [Assumes that the solver returned UNSAT and proof
|
||||||
|
logging was enabled. Array vMapRoots maps number of each root clause
|
||||||
|
into 0 (clause of A) or 1 (clause of B). Array vMapVars maps each SAT
|
||||||
|
solver variable into -1 (var of A), -2 (var of B), and <num> (var of C),
|
||||||
|
where <num> is the var's 0-based number in the ordering of C variables.]
|
||||||
|
|
||||||
|
SideEffects []
|
||||||
|
|
||||||
|
SeeAlso []
|
||||||
|
|
||||||
|
***********************************************************************/
|
||||||
|
Aig_Man_t * Inter_ManpInterpolateM114( M114p_Solver_t s, Vec_Int_t * vMapRoots, Vec_Int_t * vMapVars )
|
||||||
|
{
|
||||||
|
Aig_Man_t * p;
|
||||||
|
Aig_Obj_t * pInter, * pInter2, * pVar;
|
||||||
|
Vec_Ptr_t * vInters;
|
||||||
|
int * pLits, * pClauses, * pVars;
|
||||||
|
int nLits, nVars, i, k, iVar;
|
||||||
|
|
||||||
|
assert( M114p_SolverProofIsReady(s) );
|
||||||
|
|
||||||
|
vInters = Vec_PtrAlloc( 1000 );
|
||||||
|
// process root clauses
|
||||||
|
p = Aig_ManStart( 10000 );
|
||||||
|
M114p_SolverForEachRoot( s, &pLits, nLits, i )
|
||||||
|
{
|
||||||
|
if ( Vec_IntEntry(vMapRoots, i) == 1 ) // clause of B
|
||||||
|
pInter = Aig_ManConst1(p);
|
||||||
|
else // clause of A
|
||||||
|
{
|
||||||
|
pInter = Aig_ManConst0(p);
|
||||||
|
for ( k = 0; k < nLits; k++ )
|
||||||
|
{
|
||||||
|
iVar = Vec_IntEntry( vMapVars, lit_var(pLits[k]) );
|
||||||
|
if ( iVar < 0 ) // var of A or B
|
||||||
|
continue;
|
||||||
|
// this is a variable of C
|
||||||
|
pVar = Aig_NotCond( Aig_IthVar(p, iVar), lit_sign(pLits[k]) );
|
||||||
|
pInter = Aig_Or( p, pInter, pVar );
|
||||||
|
}
|
||||||
|
}
|
||||||
|
Vec_PtrPush( vInters, pInter );
|
||||||
|
}
|
||||||
|
// assert( Vec_PtrSize(vInters) == Vec_IntSize(vMapRoots) );
|
||||||
|
|
||||||
|
// process learned clauses
|
||||||
|
M114p_SolverForEachChain( s, &pClauses, &pVars, nVars, i )
|
||||||
|
{
|
||||||
|
pInter = Vec_PtrEntry( vInters, pClauses[0] );
|
||||||
|
for ( k = 0; k < nVars; k++ )
|
||||||
|
{
|
||||||
|
iVar = Vec_IntEntry( vMapVars, pVars[k] );
|
||||||
|
pInter2 = Vec_PtrEntry( vInters, pClauses[k+1] );
|
||||||
|
if ( iVar == -1 ) // var of A
|
||||||
|
pInter = Aig_Or( p, pInter, pInter2 );
|
||||||
|
else // var of B or C
|
||||||
|
pInter = Aig_And( p, pInter, pInter2 );
|
||||||
|
}
|
||||||
|
Vec_PtrPush( vInters, pInter );
|
||||||
|
}
|
||||||
|
|
||||||
|
assert( Vec_PtrSize(vInters) == M114p_SolverProofClauseNum(s) );
|
||||||
|
Vec_PtrFree( vInters );
|
||||||
|
Aig_ObjCreatePo( p, pInter );
|
||||||
|
Aig_ManCleanup( p );
|
||||||
|
assert( Aig_ManCheck(p) );
|
||||||
|
return p;
|
||||||
|
}
|
||||||
|
|
||||||
|
|
||||||
|
/**Function*************************************************************
|
||||||
|
|
||||||
|
Synopsis [Performs one SAT run with interpolation.]
|
||||||
|
|
||||||
|
Description [Returns 1 if proven. 0 if failed. -1 if undecided.]
|
||||||
|
|
||||||
|
SideEffects []
|
||||||
|
|
||||||
|
SeeAlso []
|
||||||
|
|
||||||
|
***********************************************************************/
|
||||||
|
int Inter_ManPerformOneStepM114p( Inter_Man_t * p, int fUsePudlak, int fUseOther )
|
||||||
|
{
|
||||||
|
M114p_Solver_t pSat;
|
||||||
|
Vec_Int_t * vMapRoots, * vMapVars;
|
||||||
|
int clk, status, RetValue;
|
||||||
|
assert( p->pInterNew == NULL );
|
||||||
|
// derive the SAT solver
|
||||||
|
pSat = Inter_ManDeriveSatSolverM114p( p->pInter, p->pCnfInter,
|
||||||
|
p->pAigTrans, p->pCnfAig, p->pFrames, p->pCnfFrames,
|
||||||
|
&vMapRoots, &vMapVars );
|
||||||
|
// solve the problem
|
||||||
|
clk = clock();
|
||||||
|
status = M114p_SolverSolve( pSat, NULL, NULL, 0 );
|
||||||
|
p->nConfCur = M114p_SolverGetConflictNum( pSat );
|
||||||
|
p->timeSat += clock() - clk;
|
||||||
|
if ( status == 0 )
|
||||||
|
{
|
||||||
|
RetValue = 1;
|
||||||
|
// Inter_ManpInterpolateM114Report( pSat, vMapRoots, vMapVars );
|
||||||
|
|
||||||
|
clk = clock();
|
||||||
|
if ( fUsePudlak )
|
||||||
|
p->pInterNew = Inter_ManInterpolateM114pPudlak( pSat, vMapRoots, vMapVars );
|
||||||
|
else
|
||||||
|
p->pInterNew = Inter_ManpInterpolateM114( pSat, vMapRoots, vMapVars );
|
||||||
|
p->timeInt += clock() - clk;
|
||||||
|
}
|
||||||
|
else if ( status == 1 )
|
||||||
|
{
|
||||||
|
RetValue = 0;
|
||||||
|
}
|
||||||
|
else
|
||||||
|
{
|
||||||
|
RetValue = -1;
|
||||||
|
}
|
||||||
|
M114p_SolverDelete( pSat );
|
||||||
|
Vec_IntFree( vMapRoots );
|
||||||
|
Vec_IntFree( vMapVars );
|
||||||
|
return RetValue;
|
||||||
|
}
|
||||||
|
|
||||||
|
////////////////////////////////////////////////////////////////////////
|
||||||
|
/// END OF FILE ///
|
||||||
|
////////////////////////////////////////////////////////////////////////
|
||||||
|
|
||||||
|
#endif
|
||||||
|
|
||||||
|
|
||||||
|
|
@ -0,0 +1,128 @@
|
||||||
|
/**CFile****************************************************************
|
||||||
|
|
||||||
|
FileName [intMan.c]
|
||||||
|
|
||||||
|
SystemName [ABC: Logic synthesis and verification system.]
|
||||||
|
|
||||||
|
PackageName [Interpolation engine.]
|
||||||
|
|
||||||
|
Synopsis [Interpolation manager procedures.]
|
||||||
|
|
||||||
|
Author [Alan Mishchenko]
|
||||||
|
|
||||||
|
Affiliation [UC Berkeley]
|
||||||
|
|
||||||
|
Date [Ver. 1.0. Started - June 24, 2008.]
|
||||||
|
|
||||||
|
Revision [$Id: intMan.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
|
||||||
|
|
||||||
|
***********************************************************************/
|
||||||
|
|
||||||
|
#include "intInt.h"
|
||||||
|
|
||||||
|
////////////////////////////////////////////////////////////////////////
|
||||||
|
/// DECLARATIONS ///
|
||||||
|
////////////////////////////////////////////////////////////////////////
|
||||||
|
|
||||||
|
////////////////////////////////////////////////////////////////////////
|
||||||
|
/// FUNCTION DEFINITIONS ///
|
||||||
|
////////////////////////////////////////////////////////////////////////
|
||||||
|
|
||||||
|
/**Function*************************************************************
|
||||||
|
|
||||||
|
Synopsis [Frees the interpolation manager.]
|
||||||
|
|
||||||
|
Description []
|
||||||
|
|
||||||
|
SideEffects []
|
||||||
|
|
||||||
|
SeeAlso []
|
||||||
|
|
||||||
|
***********************************************************************/
|
||||||
|
Inter_Man_t * Inter_ManCreate( Aig_Man_t * pAig, Inter_ManParams_t * pPars )
|
||||||
|
{
|
||||||
|
Inter_Man_t * p;
|
||||||
|
// create interpolation manager
|
||||||
|
p = ALLOC( Inter_Man_t, 1 );
|
||||||
|
memset( p, 0, sizeof(Inter_Man_t) );
|
||||||
|
p->vVarsAB = Vec_IntAlloc( Aig_ManRegNum(pAig) );
|
||||||
|
p->nConfLimit = pPars->nBTLimit;
|
||||||
|
p->fVerbose = pPars->fVerbose;
|
||||||
|
p->pAig = pAig;
|
||||||
|
return p;
|
||||||
|
}
|
||||||
|
|
||||||
|
/**Function*************************************************************
|
||||||
|
|
||||||
|
Synopsis [Frees the interpolation manager.]
|
||||||
|
|
||||||
|
Description []
|
||||||
|
|
||||||
|
SideEffects []
|
||||||
|
|
||||||
|
SeeAlso []
|
||||||
|
|
||||||
|
***********************************************************************/
|
||||||
|
void Inter_ManClean( Inter_Man_t * p )
|
||||||
|
{
|
||||||
|
if ( p->pCnfInter )
|
||||||
|
Cnf_DataFree( p->pCnfInter );
|
||||||
|
if ( p->pCnfFrames )
|
||||||
|
Cnf_DataFree( p->pCnfFrames );
|
||||||
|
if ( p->pInter )
|
||||||
|
Aig_ManStop( p->pInter );
|
||||||
|
if ( p->pFrames )
|
||||||
|
Aig_ManStop( p->pFrames );
|
||||||
|
}
|
||||||
|
|
||||||
|
/**Function*************************************************************
|
||||||
|
|
||||||
|
Synopsis [Frees the interpolation manager.]
|
||||||
|
|
||||||
|
Description []
|
||||||
|
|
||||||
|
SideEffects []
|
||||||
|
|
||||||
|
SeeAlso []
|
||||||
|
|
||||||
|
***********************************************************************/
|
||||||
|
void Inter_ManStop( Inter_Man_t * p )
|
||||||
|
{
|
||||||
|
if ( p->fVerbose )
|
||||||
|
{
|
||||||
|
p->timeOther = p->timeTotal-p->timeRwr-p->timeCnf-p->timeSat-p->timeInt-p->timeEqu;
|
||||||
|
printf( "Runtime statistics:\n" );
|
||||||
|
PRTP( "Rewriting ", p->timeRwr, p->timeTotal );
|
||||||
|
PRTP( "CNF mapping", p->timeCnf, p->timeTotal );
|
||||||
|
PRTP( "SAT solving", p->timeSat, p->timeTotal );
|
||||||
|
PRTP( "Interpol ", p->timeInt, p->timeTotal );
|
||||||
|
PRTP( "Containment", p->timeEqu, p->timeTotal );
|
||||||
|
PRTP( "Other ", p->timeOther, p->timeTotal );
|
||||||
|
PRTP( "TOTAL ", p->timeTotal, p->timeTotal );
|
||||||
|
}
|
||||||
|
|
||||||
|
if ( p->pCnfAig )
|
||||||
|
Cnf_DataFree( p->pCnfAig );
|
||||||
|
if ( p->pCnfFrames )
|
||||||
|
Cnf_DataFree( p->pCnfFrames );
|
||||||
|
if ( p->pCnfInter )
|
||||||
|
Cnf_DataFree( p->pCnfInter );
|
||||||
|
Vec_IntFree( p->vVarsAB );
|
||||||
|
if ( p->pAigTrans )
|
||||||
|
Aig_ManStop( p->pAigTrans );
|
||||||
|
if ( p->pFrames )
|
||||||
|
Aig_ManStop( p->pFrames );
|
||||||
|
if ( p->pInter )
|
||||||
|
Aig_ManStop( p->pInter );
|
||||||
|
if ( p->pInterNew )
|
||||||
|
Aig_ManStop( p->pInterNew );
|
||||||
|
free( p );
|
||||||
|
}
|
||||||
|
|
||||||
|
|
||||||
|
|
||||||
|
////////////////////////////////////////////////////////////////////////
|
||||||
|
/// END OF FILE ///
|
||||||
|
////////////////////////////////////////////////////////////////////////
|
||||||
|
|
||||||
|
|
||||||
|
|
@ -0,0 +1,92 @@
|
||||||
|
/**CFile****************************************************************
|
||||||
|
|
||||||
|
FileName [intUtil.c]
|
||||||
|
|
||||||
|
SystemName [ABC: Logic synthesis and verification system.]
|
||||||
|
|
||||||
|
PackageName [Interpolation engine.]
|
||||||
|
|
||||||
|
Synopsis [Various interpolation utilities.]
|
||||||
|
|
||||||
|
Author [Alan Mishchenko]
|
||||||
|
|
||||||
|
Affiliation [UC Berkeley]
|
||||||
|
|
||||||
|
Date [Ver. 1.0. Started - June 24, 2008.]
|
||||||
|
|
||||||
|
Revision [$Id: intUtil.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
|
||||||
|
|
||||||
|
***********************************************************************/
|
||||||
|
|
||||||
|
#include "intInt.h"
|
||||||
|
|
||||||
|
////////////////////////////////////////////////////////////////////////
|
||||||
|
/// DECLARATIONS ///
|
||||||
|
////////////////////////////////////////////////////////////////////////
|
||||||
|
|
||||||
|
////////////////////////////////////////////////////////////////////////
|
||||||
|
/// FUNCTION DEFINITIONS ///
|
||||||
|
////////////////////////////////////////////////////////////////////////
|
||||||
|
|
||||||
|
|
||||||
|
/**Function*************************************************************
|
||||||
|
|
||||||
|
Synopsis [Returns 1 if the property fails in the initial state.]
|
||||||
|
|
||||||
|
Description []
|
||||||
|
|
||||||
|
SideEffects []
|
||||||
|
|
||||||
|
SeeAlso []
|
||||||
|
|
||||||
|
***********************************************************************/
|
||||||
|
int Inter_ManCheckInitialState( Aig_Man_t * p )
|
||||||
|
{
|
||||||
|
Cnf_Dat_t * pCnf;
|
||||||
|
sat_solver * pSat;
|
||||||
|
int status;
|
||||||
|
int clk = clock();
|
||||||
|
pCnf = Cnf_Derive( p, Saig_ManRegNum(p) );
|
||||||
|
pSat = Cnf_DataWriteIntoSolver( pCnf, 1, 1 );
|
||||||
|
Cnf_DataFree( pCnf );
|
||||||
|
if ( pSat == NULL )
|
||||||
|
return 0;
|
||||||
|
status = sat_solver_solve( pSat, NULL, NULL, (sint64)0, (sint64)0, (sint64)0, (sint64)0 );
|
||||||
|
sat_solver_delete( pSat );
|
||||||
|
PRT( "Time", clock() - clk );
|
||||||
|
return status == l_True;
|
||||||
|
}
|
||||||
|
|
||||||
|
/**Function*************************************************************
|
||||||
|
|
||||||
|
Synopsis [Returns 1 if the property holds in all states.]
|
||||||
|
|
||||||
|
Description []
|
||||||
|
|
||||||
|
SideEffects []
|
||||||
|
|
||||||
|
SeeAlso []
|
||||||
|
|
||||||
|
***********************************************************************/
|
||||||
|
int Inter_ManCheckAllStates( Aig_Man_t * p )
|
||||||
|
{
|
||||||
|
Cnf_Dat_t * pCnf;
|
||||||
|
sat_solver * pSat;
|
||||||
|
int status;
|
||||||
|
int clk = clock();
|
||||||
|
pCnf = Cnf_Derive( p, Saig_ManRegNum(p) );
|
||||||
|
pSat = Cnf_DataWriteIntoSolver( pCnf, 1, 0 );
|
||||||
|
Cnf_DataFree( pCnf );
|
||||||
|
if ( pSat == NULL )
|
||||||
|
return 1;
|
||||||
|
status = sat_solver_solve( pSat, NULL, NULL, (sint64)0, (sint64)0, (sint64)0, (sint64)0 );
|
||||||
|
sat_solver_delete( pSat );
|
||||||
|
PRT( "Time", clock() - clk );
|
||||||
|
return status == l_False;
|
||||||
|
}
|
||||||
|
|
||||||
|
////////////////////////////////////////////////////////////////////////
|
||||||
|
/// END OF FILE ///
|
||||||
|
////////////////////////////////////////////////////////////////////////
|
||||||
|
|
||||||
|
|
||||||
|
|
@ -0,0 +1,9 @@
|
||||||
|
SRC += src/aig/int/intContain.c \
|
||||||
|
src/aig/int/intCore.c \
|
||||||
|
src/aig/int/intDup.c \
|
||||||
|
src/aig/int/intFrames.c \
|
||||||
|
src/aig/int/intInter.c \
|
||||||
|
src/aig/int/intM114.c \
|
||||||
|
src/aig/int/intM114p.c \
|
||||||
|
src/aig/int/intMan.c \
|
||||||
|
src/aig/int/intUtil.c
|
||||||
|
|
@ -803,8 +803,8 @@ Nwk_Man_t * Ntl_ManExtractNwk( Ntl_Man_t * p, Aig_Man_t * pAig, Tim_Man_t * pMan
|
||||||
pNtk->pManTime = Tim_ManDup( pManTime, 0 );
|
pNtk->pManTime = Tim_ManDup( pManTime, 0 );
|
||||||
else
|
else
|
||||||
pNtk->pManTime = Tim_ManDup( p->pManTime, 0 );
|
pNtk->pManTime = Tim_ManDup( p->pManTime, 0 );
|
||||||
// Nwk_ManRemoveDupFanins( pNtk, 0 );
|
Nwk_ManRemoveDupFanins( pNtk, 0 );
|
||||||
// assert( Nwk_ManCheck( pNtk ) );
|
assert( Nwk_ManCheck( pNtk ) );
|
||||||
return pNtk;
|
return pNtk;
|
||||||
}
|
}
|
||||||
|
|
||||||
|
|
|
||||||
|
|
@ -145,13 +145,20 @@ void Ntl_ManReduce( Ntl_Man_t * p, Aig_Man_t * pAig )
|
||||||
continue;
|
continue;
|
||||||
assert( pObj != pObjRepr );
|
assert( pObj != pObjRepr );
|
||||||
pNet = pObj->pData;
|
pNet = pObj->pData;
|
||||||
// do not reduce the net if it is driven by a multi-output box
|
|
||||||
if ( Ntl_ObjIsBox(pNet->pDriver) && Ntl_ObjFanoutNum(pNet->pDriver) > 1 )
|
|
||||||
continue;
|
|
||||||
// do not reduce the net if it has no-merge attribute
|
|
||||||
if ( Ntl_ObjIsBox(pNet->pDriver) && pNet->pDriver->pImplem->attrNoMerge )
|
|
||||||
continue;
|
|
||||||
pNetRepr = pObjRepr->pData;
|
pNetRepr = pObjRepr->pData;
|
||||||
|
// consider special cases, when the net should not be reduced
|
||||||
|
if ( Ntl_ObjIsBox(pNet->pDriver) )
|
||||||
|
{
|
||||||
|
// do not reduce the net if it is driven by a multi-output box
|
||||||
|
if ( Ntl_ObjFanoutNum(pNet->pDriver) > 1 )
|
||||||
|
continue;
|
||||||
|
// do not reduce the net if it has no-merge attribute
|
||||||
|
if ( pNet->pDriver->pImplem->attrNoMerge )
|
||||||
|
continue;
|
||||||
|
// do not reduce the net if the replacement net has no-merge attribute
|
||||||
|
if ( pNetRepr != NULL && pNetRepr->pDriver->pImplem->attrNoMerge )
|
||||||
|
continue;
|
||||||
|
}
|
||||||
if ( pNetRepr == NULL )
|
if ( pNetRepr == NULL )
|
||||||
{
|
{
|
||||||
// this is the constant node
|
// this is the constant node
|
||||||
|
|
|
||||||
|
|
@ -1,7 +1,6 @@
|
||||||
SRC += src/aig/saig/saigBmc.c \
|
SRC += src/aig/saig/saigBmc.c \
|
||||||
src/aig/saig/saigCone.c \
|
src/aig/saig/saigCone.c \
|
||||||
src/aig/saig/saigHaig.c \
|
src/aig/saig/saigHaig.c \
|
||||||
src/aig/saig/saigInter.c \
|
|
||||||
src/aig/saig/saigIoa.c \
|
src/aig/saig/saigIoa.c \
|
||||||
src/aig/saig/saigMiter.c \
|
src/aig/saig/saigMiter.c \
|
||||||
src/aig/saig/saigPhase.c \
|
src/aig/saig/saigPhase.c \
|
||||||
|
|
@ -9,5 +8,4 @@ SRC += src/aig/saig/saigBmc.c \
|
||||||
src/aig/saig/saigRetMin.c \
|
src/aig/saig/saigRetMin.c \
|
||||||
src/aig/saig/saigRetStep.c \
|
src/aig/saig/saigRetStep.c \
|
||||||
src/aig/saig/saigScl.c \
|
src/aig/saig/saigScl.c \
|
||||||
src/aig/saig/saigTrans.c \
|
src/aig/saig/saigTrans.c
|
||||||
src/aig/saig/saigUnique.c
|
|
||||||
|
|
|
||||||
|
|
@ -30,6 +30,7 @@ extern "C" {
|
||||||
////////////////////////////////////////////////////////////////////////
|
////////////////////////////////////////////////////////////////////////
|
||||||
|
|
||||||
#include "aig.h"
|
#include "aig.h"
|
||||||
|
#include "int.h"
|
||||||
|
|
||||||
////////////////////////////////////////////////////////////////////////
|
////////////////////////////////////////////////////////////////////////
|
||||||
/// PARAMETERS ///
|
/// PARAMETERS ///
|
||||||
|
|
@ -85,7 +86,7 @@ extern Aig_Man_t * Saig_ManHaigRecord( Aig_Man_t * p, int nIters, int nSte
|
||||||
extern void Saig_ManDumpBlif( Aig_Man_t * p, char * pFileName );
|
extern void Saig_ManDumpBlif( Aig_Man_t * p, char * pFileName );
|
||||||
extern Aig_Man_t * Saig_ManReadBlif( char * pFileName );
|
extern Aig_Man_t * Saig_ManReadBlif( char * pFileName );
|
||||||
/*=== saigInter.c ==========================================================*/
|
/*=== saigInter.c ==========================================================*/
|
||||||
extern int Saig_Interpolate( Aig_Man_t * pAig, int nConfLimit, int nFramesMax, int fRewrite, int fTransLoop, int fUsePudlak, int fUseOther, int fUseMiniSat, int fCheckInd, int fCheckKstep, int fVerbose, int * pDepth );
|
extern int Saig_Interpolate( Aig_Man_t * pAig, Inter_ManParams_t * pPars, int * pDepth );
|
||||||
/*=== saigMiter.c ==========================================================*/
|
/*=== saigMiter.c ==========================================================*/
|
||||||
extern Aig_Man_t * Saig_ManCreateMiter( Aig_Man_t * p1, Aig_Man_t * p2, int Oper );
|
extern Aig_Man_t * Saig_ManCreateMiter( Aig_Man_t * p1, Aig_Man_t * p2, int Oper );
|
||||||
/*=== saigPhase.c ==========================================================*/
|
/*=== saigPhase.c ==========================================================*/
|
||||||
|
|
|
||||||
File diff suppressed because it is too large
Load Diff
|
|
@ -1,170 +0,0 @@
|
||||||
/**CFile****************************************************************
|
|
||||||
|
|
||||||
FileName [saigUnique.c]
|
|
||||||
|
|
||||||
SystemName [ABC: Logic synthesis and verification system.]
|
|
||||||
|
|
||||||
PackageName [Sequential AIG package.]
|
|
||||||
|
|
||||||
Synopsis [Containment checking with unique state constraints.]
|
|
||||||
|
|
||||||
Author [Alan Mishchenko]
|
|
||||||
|
|
||||||
Affiliation [UC Berkeley]
|
|
||||||
|
|
||||||
Date [Ver. 1.0. Started - June 20, 2005.]
|
|
||||||
|
|
||||||
Revision [$Id: saigUnique.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
|
|
||||||
|
|
||||||
***********************************************************************/
|
|
||||||
|
|
||||||
#include "saig.h"
|
|
||||||
#include "cnf.h"
|
|
||||||
#include "satSolver.h"
|
|
||||||
|
|
||||||
////////////////////////////////////////////////////////////////////////
|
|
||||||
/// DECLARATIONS ///
|
|
||||||
////////////////////////////////////////////////////////////////////////
|
|
||||||
|
|
||||||
////////////////////////////////////////////////////////////////////////
|
|
||||||
/// FUNCTION DEFINITIONS ///
|
|
||||||
////////////////////////////////////////////////////////////////////////
|
|
||||||
|
|
||||||
/**Function*************************************************************
|
|
||||||
|
|
||||||
Synopsis [Create timeframes of the manager for interpolation.]
|
|
||||||
|
|
||||||
Description [The resulting manager is combinational. The primary inputs
|
|
||||||
corresponding to register outputs are ordered first.]
|
|
||||||
|
|
||||||
SideEffects []
|
|
||||||
|
|
||||||
SeeAlso []
|
|
||||||
|
|
||||||
***********************************************************************/
|
|
||||||
Aig_Man_t * Saig_ManFramesLatches( Aig_Man_t * pAig, int nFrames, Vec_Ptr_t ** pvMapReg )
|
|
||||||
{
|
|
||||||
Aig_Man_t * pFrames;
|
|
||||||
Aig_Obj_t * pObj, * pObjLi, * pObjLo;
|
|
||||||
int i, f;
|
|
||||||
assert( Saig_ManRegNum(pAig) > 0 );
|
|
||||||
pFrames = Aig_ManStart( Aig_ManNodeNum(pAig) * nFrames );
|
|
||||||
// map the constant node
|
|
||||||
Aig_ManConst1(pAig)->pData = Aig_ManConst1( pFrames );
|
|
||||||
// create variables for register outputs
|
|
||||||
*pvMapReg = Vec_PtrAlloc( (nFrames+1) * Saig_ManRegNum(pAig) );
|
|
||||||
Saig_ManForEachLo( pAig, pObj, i )
|
|
||||||
{
|
|
||||||
pObj->pData = Aig_ObjCreatePi( pFrames );
|
|
||||||
Vec_PtrPush( *pvMapReg, pObj->pData );
|
|
||||||
}
|
|
||||||
// add timeframes
|
|
||||||
for ( f = 0; f < nFrames; f++ )
|
|
||||||
{
|
|
||||||
// create PI nodes for this frame
|
|
||||||
Saig_ManForEachPi( pAig, pObj, i )
|
|
||||||
pObj->pData = Aig_ObjCreatePi( pFrames );
|
|
||||||
// add internal nodes of this frame
|
|
||||||
Aig_ManForEachNode( pAig, pObj, i )
|
|
||||||
pObj->pData = Aig_And( pFrames, Aig_ObjChild0Copy(pObj), Aig_ObjChild1Copy(pObj) );
|
|
||||||
// save register inputs
|
|
||||||
Saig_ManForEachLi( pAig, pObj, i )
|
|
||||||
pObj->pData = Aig_ObjChild0Copy(pObj);
|
|
||||||
// transfer to register outputs
|
|
||||||
Saig_ManForEachLiLo( pAig, pObjLi, pObjLo, i )
|
|
||||||
{
|
|
||||||
pObjLo->pData = pObjLi->pData;
|
|
||||||
Vec_PtrPush( *pvMapReg, pObjLo->pData );
|
|
||||||
}
|
|
||||||
}
|
|
||||||
return pFrames;
|
|
||||||
}
|
|
||||||
|
|
||||||
/**Function*************************************************************
|
|
||||||
|
|
||||||
Synopsis [Duplicates AIG while mapping PIs into the given array.]
|
|
||||||
|
|
||||||
Description []
|
|
||||||
|
|
||||||
SideEffects []
|
|
||||||
|
|
||||||
SeeAlso []
|
|
||||||
|
|
||||||
***********************************************************************/
|
|
||||||
void Saig_ManAppendCone( Aig_Man_t * pOld, Aig_Man_t * pNew, Aig_Obj_t ** ppNewPis, int fCompl )
|
|
||||||
{
|
|
||||||
Aig_Obj_t * pObj;
|
|
||||||
int i;
|
|
||||||
assert( Aig_ManPoNum(pOld) == 1 );
|
|
||||||
// create the PIs
|
|
||||||
Aig_ManCleanData( pOld );
|
|
||||||
Aig_ManConst1(pOld)->pData = Aig_ManConst1(pNew);
|
|
||||||
Aig_ManForEachPi( pOld, pObj, i )
|
|
||||||
pObj->pData = ppNewPis[i];
|
|
||||||
// duplicate internal nodes
|
|
||||||
Aig_ManForEachNode( pOld, pObj, i )
|
|
||||||
pObj->pData = Aig_And( pNew, Aig_ObjChild0Copy(pObj), Aig_ObjChild1Copy(pObj) );
|
|
||||||
// add one PO to new
|
|
||||||
pObj = Aig_ManPo( pOld, 0 );
|
|
||||||
Aig_ObjCreatePo( pNew, Aig_NotCond( Aig_ObjChild0Copy(pObj), fCompl ) );
|
|
||||||
}
|
|
||||||
|
|
||||||
/**Function*************************************************************
|
|
||||||
|
|
||||||
Synopsis []
|
|
||||||
|
|
||||||
Description []
|
|
||||||
|
|
||||||
SideEffects []
|
|
||||||
|
|
||||||
SeeAlso []
|
|
||||||
|
|
||||||
***********************************************************************/
|
|
||||||
int Saig_ManUniqueState( Aig_Man_t * pTrans, Vec_Ptr_t * vInters )
|
|
||||||
{
|
|
||||||
Aig_Man_t * pFrames, * pInterNext, * pInterThis;
|
|
||||||
Aig_Obj_t ** ppNodes;
|
|
||||||
Vec_Ptr_t * vMapRegs;
|
|
||||||
Cnf_Dat_t * pCnf;
|
|
||||||
sat_solver * pSat;
|
|
||||||
int f, nRegs, status;
|
|
||||||
nRegs = Saig_ManRegNum(pTrans);
|
|
||||||
assert( nRegs > 0 );
|
|
||||||
assert( Vec_PtrSize(vInters) > 1 );
|
|
||||||
// generate the timeframes
|
|
||||||
pFrames = Saig_ManFramesLatches( pTrans, Vec_PtrSize(vInters)-1, &vMapRegs );
|
|
||||||
assert( Vec_PtrSize(vMapRegs) == Vec_PtrSize(vInters) * nRegs );
|
|
||||||
// add main constraints to the timeframes
|
|
||||||
ppNodes = (Aig_Obj_t **)Vec_PtrArray(vMapRegs);
|
|
||||||
Vec_PtrForEachEntryStop( vInters, pInterThis, f, Vec_PtrSize(vInters)-1 )
|
|
||||||
{
|
|
||||||
assert( nRegs == Aig_ManPiNum(pInterThis) );
|
|
||||||
pInterNext = Vec_PtrEntry( vInters, f+1 );
|
|
||||||
Saig_ManAppendCone( pInterNext, pFrames, ppNodes + f * nRegs, 0 );
|
|
||||||
Saig_ManAppendCone( pInterThis, pFrames, ppNodes + f * nRegs, 1 );
|
|
||||||
}
|
|
||||||
Saig_ManAppendCone( Vec_PtrEntryLast(vInters), pFrames, ppNodes + f * nRegs, 1 );
|
|
||||||
Aig_ManCleanup( pFrames );
|
|
||||||
Vec_PtrFree( vMapRegs );
|
|
||||||
|
|
||||||
// convert to CNF
|
|
||||||
pCnf = Cnf_Derive( pFrames, 0 );
|
|
||||||
pSat = Cnf_DataWriteIntoSolver( pCnf, 1, 0 );
|
|
||||||
Cnf_DataFree( pCnf );
|
|
||||||
Aig_ManStop( pFrames );
|
|
||||||
|
|
||||||
if ( pSat == NULL )
|
|
||||||
return 1;
|
|
||||||
|
|
||||||
// solve the problem
|
|
||||||
status = sat_solver_solve( pSat, NULL, NULL, (sint64)0, (sint64)0, (sint64)0, (sint64)0 );
|
|
||||||
sat_solver_delete( pSat );
|
|
||||||
return status == l_False;
|
|
||||||
}
|
|
||||||
|
|
||||||
|
|
||||||
////////////////////////////////////////////////////////////////////////
|
|
||||||
/// END OF FILE ///
|
|
||||||
////////////////////////////////////////////////////////////////////////
|
|
||||||
|
|
||||||
|
|
||||||
|
|
@ -748,7 +748,7 @@ extern ABC_DLL bool Abc_NodeIsBuf( Abc_Obj_t * pNode );
|
||||||
extern ABC_DLL bool Abc_NodeIsInv( Abc_Obj_t * pNode );
|
extern ABC_DLL bool Abc_NodeIsInv( Abc_Obj_t * pNode );
|
||||||
extern ABC_DLL void Abc_NodeComplement( Abc_Obj_t * pNode );
|
extern ABC_DLL void Abc_NodeComplement( Abc_Obj_t * pNode );
|
||||||
/*=== abcPrint.c ==========================================================*/
|
/*=== abcPrint.c ==========================================================*/
|
||||||
extern ABC_DLL void Abc_NtkPrintStats( FILE * pFile, Abc_Ntk_t * pNtk, int fFactored, int fSaveBest, int fDumpResult, int fUseLutLib );
|
extern ABC_DLL void Abc_NtkPrintStats( FILE * pFile, Abc_Ntk_t * pNtk, int fFactored, int fSaveBest, int fDumpResult, int fUseLutLib, int fPrintMuxes );
|
||||||
extern ABC_DLL void Abc_NtkPrintIo( FILE * pFile, Abc_Ntk_t * pNtk );
|
extern ABC_DLL void Abc_NtkPrintIo( FILE * pFile, Abc_Ntk_t * pNtk );
|
||||||
extern ABC_DLL void Abc_NtkPrintLatch( FILE * pFile, Abc_Ntk_t * pNtk );
|
extern ABC_DLL void Abc_NtkPrintLatch( FILE * pFile, Abc_Ntk_t * pNtk );
|
||||||
extern ABC_DLL void Abc_NtkPrintFanio( FILE * pFile, Abc_Ntk_t * pNtk );
|
extern ABC_DLL void Abc_NtkPrintFanio( FILE * pFile, Abc_Ntk_t * pNtk );
|
||||||
|
|
|
||||||
|
|
@ -933,15 +933,36 @@ bool Abc_NodeIsMuxType( Abc_Obj_t * pNode )
|
||||||
pNode0 = Abc_ObjFanin0(pNode);
|
pNode0 = Abc_ObjFanin0(pNode);
|
||||||
pNode1 = Abc_ObjFanin1(pNode);
|
pNode1 = Abc_ObjFanin1(pNode);
|
||||||
// if the children are not ANDs, this is not MUX
|
// if the children are not ANDs, this is not MUX
|
||||||
if ( Abc_ObjFaninNum(pNode0) != 2 || Abc_ObjFaninNum(pNode1) != 2 )
|
if ( !Abc_AigNodeIsAnd(pNode0) || !Abc_AigNodeIsAnd(pNode1) )
|
||||||
return 0;
|
return 0;
|
||||||
// otherwise the node is MUX iff it has a pair of equal grandchildren
|
// otherwise the node is MUX iff it has a pair of equal grandchildren with opposite polarity
|
||||||
return (Abc_ObjFaninId0(pNode0) == Abc_ObjFaninId0(pNode1) && (Abc_ObjFaninC0(pNode0) ^ Abc_ObjFaninC0(pNode1))) ||
|
return (Abc_ObjFaninId0(pNode0) == Abc_ObjFaninId0(pNode1) && (Abc_ObjFaninC0(pNode0) ^ Abc_ObjFaninC0(pNode1))) ||
|
||||||
(Abc_ObjFaninId0(pNode0) == Abc_ObjFaninId1(pNode1) && (Abc_ObjFaninC0(pNode0) ^ Abc_ObjFaninC1(pNode1))) ||
|
(Abc_ObjFaninId0(pNode0) == Abc_ObjFaninId1(pNode1) && (Abc_ObjFaninC0(pNode0) ^ Abc_ObjFaninC1(pNode1))) ||
|
||||||
(Abc_ObjFaninId1(pNode0) == Abc_ObjFaninId0(pNode1) && (Abc_ObjFaninC1(pNode0) ^ Abc_ObjFaninC0(pNode1))) ||
|
(Abc_ObjFaninId1(pNode0) == Abc_ObjFaninId0(pNode1) && (Abc_ObjFaninC1(pNode0) ^ Abc_ObjFaninC0(pNode1))) ||
|
||||||
(Abc_ObjFaninId1(pNode0) == Abc_ObjFaninId1(pNode1) && (Abc_ObjFaninC1(pNode0) ^ Abc_ObjFaninC1(pNode1)));
|
(Abc_ObjFaninId1(pNode0) == Abc_ObjFaninId1(pNode1) && (Abc_ObjFaninC1(pNode0) ^ Abc_ObjFaninC1(pNode1)));
|
||||||
}
|
}
|
||||||
|
|
||||||
|
/**Function*************************************************************
|
||||||
|
|
||||||
|
Synopsis [Returns 1 if the node is the root of MUX or EXOR/NEXOR.]
|
||||||
|
|
||||||
|
Description []
|
||||||
|
|
||||||
|
SideEffects []
|
||||||
|
|
||||||
|
SeeAlso []
|
||||||
|
|
||||||
|
***********************************************************************/
|
||||||
|
int Abc_NtkCountMuxes( Abc_Ntk_t * pNtk )
|
||||||
|
{
|
||||||
|
Abc_Obj_t * pNode;
|
||||||
|
int i;
|
||||||
|
int Counter = 0;
|
||||||
|
Abc_NtkForEachNode( pNtk, pNode, i )
|
||||||
|
Counter += Abc_NodeIsMuxType( pNode );
|
||||||
|
return Counter;
|
||||||
|
}
|
||||||
|
|
||||||
/**Function*************************************************************
|
/**Function*************************************************************
|
||||||
|
|
||||||
Synopsis [Returns 1 if the node is the control type of the MUX.]
|
Synopsis [Returns 1 if the node is the control type of the MUX.]
|
||||||
|
|
|
||||||
|
|
@ -34,6 +34,7 @@
|
||||||
#include "fra.h"
|
#include "fra.h"
|
||||||
#include "saig.h"
|
#include "saig.h"
|
||||||
#include "nwkMerge.h"
|
#include "nwkMerge.h"
|
||||||
|
#include "int.h"
|
||||||
|
|
||||||
////////////////////////////////////////////////////////////////////////
|
////////////////////////////////////////////////////////////////////////
|
||||||
/// DECLARATIONS ///
|
/// DECLARATIONS ///
|
||||||
|
|
@ -65,6 +66,7 @@ static int Abc_CommandShowCut ( Abc_Frame_t * pAbc, int argc, char ** arg
|
||||||
static int Abc_CommandCollapse ( Abc_Frame_t * pAbc, int argc, char ** argv );
|
static int Abc_CommandCollapse ( Abc_Frame_t * pAbc, int argc, char ** argv );
|
||||||
static int Abc_CommandStrash ( Abc_Frame_t * pAbc, int argc, char ** argv );
|
static int Abc_CommandStrash ( Abc_Frame_t * pAbc, int argc, char ** argv );
|
||||||
static int Abc_CommandBalance ( Abc_Frame_t * pAbc, int argc, char ** argv );
|
static int Abc_CommandBalance ( Abc_Frame_t * pAbc, int argc, char ** argv );
|
||||||
|
static int Abc_CommandMuxStruct ( Abc_Frame_t * pAbc, int argc, char ** argv );
|
||||||
static int Abc_CommandMulti ( Abc_Frame_t * pAbc, int argc, char ** argv );
|
static int Abc_CommandMulti ( Abc_Frame_t * pAbc, int argc, char ** argv );
|
||||||
static int Abc_CommandRenode ( Abc_Frame_t * pAbc, int argc, char ** argv );
|
static int Abc_CommandRenode ( Abc_Frame_t * pAbc, int argc, char ** argv );
|
||||||
static int Abc_CommandCleanup ( Abc_Frame_t * pAbc, int argc, char ** argv );
|
static int Abc_CommandCleanup ( Abc_Frame_t * pAbc, int argc, char ** argv );
|
||||||
|
|
@ -327,6 +329,7 @@ void Abc_Init( Abc_Frame_t * pAbc )
|
||||||
Cmd_CommandAdd( pAbc, "Synthesis", "collapse", Abc_CommandCollapse, 1 );
|
Cmd_CommandAdd( pAbc, "Synthesis", "collapse", Abc_CommandCollapse, 1 );
|
||||||
Cmd_CommandAdd( pAbc, "Synthesis", "strash", Abc_CommandStrash, 1 );
|
Cmd_CommandAdd( pAbc, "Synthesis", "strash", Abc_CommandStrash, 1 );
|
||||||
Cmd_CommandAdd( pAbc, "Synthesis", "balance", Abc_CommandBalance, 1 );
|
Cmd_CommandAdd( pAbc, "Synthesis", "balance", Abc_CommandBalance, 1 );
|
||||||
|
Cmd_CommandAdd( pAbc, "Synthesis", "mux_struct", Abc_CommandMuxStruct, 1 );
|
||||||
Cmd_CommandAdd( pAbc, "Synthesis", "multi", Abc_CommandMulti, 1 );
|
Cmd_CommandAdd( pAbc, "Synthesis", "multi", Abc_CommandMulti, 1 );
|
||||||
Cmd_CommandAdd( pAbc, "Synthesis", "renode", Abc_CommandRenode, 1 );
|
Cmd_CommandAdd( pAbc, "Synthesis", "renode", Abc_CommandRenode, 1 );
|
||||||
Cmd_CommandAdd( pAbc, "Synthesis", "cleanup", Abc_CommandCleanup, 1 );
|
Cmd_CommandAdd( pAbc, "Synthesis", "cleanup", Abc_CommandCleanup, 1 );
|
||||||
|
|
@ -588,6 +591,7 @@ int Abc_CommandPrintStats( Abc_Frame_t * pAbc, int argc, char ** argv )
|
||||||
int fDumpResult;
|
int fDumpResult;
|
||||||
int fUseLutLib;
|
int fUseLutLib;
|
||||||
int fPrintTime;
|
int fPrintTime;
|
||||||
|
int fPrintMuxes;
|
||||||
int c;
|
int c;
|
||||||
|
|
||||||
pNtk = Abc_FrameReadNtk(pAbc);
|
pNtk = Abc_FrameReadNtk(pAbc);
|
||||||
|
|
@ -600,8 +604,9 @@ int Abc_CommandPrintStats( Abc_Frame_t * pAbc, int argc, char ** argv )
|
||||||
fDumpResult = 0;
|
fDumpResult = 0;
|
||||||
fUseLutLib = 0;
|
fUseLutLib = 0;
|
||||||
fPrintTime = 0;
|
fPrintTime = 0;
|
||||||
|
fPrintMuxes = 1;
|
||||||
Extra_UtilGetoptReset();
|
Extra_UtilGetoptReset();
|
||||||
while ( ( c = Extra_UtilGetopt( argc, argv, "fbdlth" ) ) != EOF )
|
while ( ( c = Extra_UtilGetopt( argc, argv, "fbdltmh" ) ) != EOF )
|
||||||
{
|
{
|
||||||
switch ( c )
|
switch ( c )
|
||||||
{
|
{
|
||||||
|
|
@ -620,6 +625,9 @@ int Abc_CommandPrintStats( Abc_Frame_t * pAbc, int argc, char ** argv )
|
||||||
case 't':
|
case 't':
|
||||||
fPrintTime ^= 1;
|
fPrintTime ^= 1;
|
||||||
break;
|
break;
|
||||||
|
case 'm':
|
||||||
|
fPrintMuxes ^= 1;
|
||||||
|
break;
|
||||||
case 'h':
|
case 'h':
|
||||||
goto usage;
|
goto usage;
|
||||||
default:
|
default:
|
||||||
|
|
@ -632,7 +640,12 @@ int Abc_CommandPrintStats( Abc_Frame_t * pAbc, int argc, char ** argv )
|
||||||
fprintf( Abc_FrameReadErr(pAbc), "Empty network.\n" );
|
fprintf( Abc_FrameReadErr(pAbc), "Empty network.\n" );
|
||||||
return 1;
|
return 1;
|
||||||
}
|
}
|
||||||
Abc_NtkPrintStats( pOut, pNtk, fFactor, fSaveBest, fDumpResult, fUseLutLib );
|
if ( !Abc_NtkIsLogic(pNtk) && fUseLutLib )
|
||||||
|
{
|
||||||
|
fprintf( Abc_FrameReadErr(pAbc), "Cannot print LUT delay for a non-logic network.\n" );
|
||||||
|
return 1;
|
||||||
|
}
|
||||||
|
Abc_NtkPrintStats( pOut, pNtk, fFactor, fSaveBest, fDumpResult, fUseLutLib, fPrintMuxes );
|
||||||
if ( fPrintTime )
|
if ( fPrintTime )
|
||||||
{
|
{
|
||||||
pAbc->TimeTotal += pAbc->TimeCommand;
|
pAbc->TimeTotal += pAbc->TimeCommand;
|
||||||
|
|
@ -643,13 +656,14 @@ int Abc_CommandPrintStats( Abc_Frame_t * pAbc, int argc, char ** argv )
|
||||||
return 0;
|
return 0;
|
||||||
|
|
||||||
usage:
|
usage:
|
||||||
fprintf( pErr, "usage: print_stats [-fbdlth]\n" );
|
fprintf( pErr, "usage: print_stats [-fbdltmh]\n" );
|
||||||
fprintf( pErr, "\t prints the network statistics\n" );
|
fprintf( pErr, "\t prints the network statistics\n" );
|
||||||
fprintf( pErr, "\t-f : toggles printing the literal count in the factored forms [default = %s]\n", fFactor? "yes": "no" );
|
fprintf( pErr, "\t-f : toggles printing the literal count in the factored forms [default = %s]\n", fFactor? "yes": "no" );
|
||||||
fprintf( pErr, "\t-b : toggles saving the best logic network in \"best.blif\" [default = %s]\n", fSaveBest? "yes": "no" );
|
fprintf( pErr, "\t-b : toggles saving the best logic network in \"best.blif\" [default = %s]\n", fSaveBest? "yes": "no" );
|
||||||
fprintf( pErr, "\t-d : toggles dumping network into file \"<input_file_name>_dump.blif\" [default = %s]\n", fDumpResult? "yes": "no" );
|
fprintf( pErr, "\t-d : toggles dumping network into file \"<input_file_name>_dump.blif\" [default = %s]\n", fDumpResult? "yes": "no" );
|
||||||
fprintf( pErr, "\t-l : toggles printing delay of LUT mapping using LUT library [default = %s]\n", fSaveBest? "yes": "no" );
|
fprintf( pErr, "\t-l : toggles printing delay of LUT mapping using LUT library [default = %s]\n", fSaveBest? "yes": "no" );
|
||||||
fprintf( pErr, "\t-t : toggles printing runtime statistics [default = %s]\n", fPrintTime? "yes": "no" );
|
fprintf( pErr, "\t-t : toggles printing runtime statistics [default = %s]\n", fPrintTime? "yes": "no" );
|
||||||
|
fprintf( pErr, "\t-m : toggles printing MUX statistics [default = %s]\n", fPrintMuxes? "yes": "no" );
|
||||||
fprintf( pErr, "\t-h : print the command usage\n");
|
fprintf( pErr, "\t-h : print the command usage\n");
|
||||||
return 1;
|
return 1;
|
||||||
}
|
}
|
||||||
|
|
@ -735,7 +749,7 @@ int Abc_CommandPrintExdc( Abc_Frame_t * pAbc, int argc, char ** argv )
|
||||||
}
|
}
|
||||||
else
|
else
|
||||||
printf( "EXDC network statistics: \n" );
|
printf( "EXDC network statistics: \n" );
|
||||||
Abc_NtkPrintStats( pOut, pNtk->pExdc, 0, 0, 0, 0 );
|
Abc_NtkPrintStats( pOut, pNtk->pExdc, 0, 0, 0, 0, 0 );
|
||||||
return 0;
|
return 0;
|
||||||
|
|
||||||
usage:
|
usage:
|
||||||
|
|
@ -2472,6 +2486,78 @@ usage:
|
||||||
return 1;
|
return 1;
|
||||||
}
|
}
|
||||||
|
|
||||||
|
/**Function*************************************************************
|
||||||
|
|
||||||
|
Synopsis []
|
||||||
|
|
||||||
|
Description []
|
||||||
|
|
||||||
|
SideEffects []
|
||||||
|
|
||||||
|
SeeAlso []
|
||||||
|
|
||||||
|
***********************************************************************/
|
||||||
|
int Abc_CommandMuxStruct( Abc_Frame_t * pAbc, int argc, char ** argv )
|
||||||
|
{
|
||||||
|
FILE * pOut, * pErr;
|
||||||
|
Abc_Ntk_t * pNtk, * pNtkRes;
|
||||||
|
int c;
|
||||||
|
int fVerbose;
|
||||||
|
|
||||||
|
extern Abc_Ntk_t * Abc_NtkMuxRestructure( Abc_Ntk_t * pNtk, int fVerbose );
|
||||||
|
|
||||||
|
pNtk = Abc_FrameReadNtk(pAbc);
|
||||||
|
pOut = Abc_FrameReadOut(pAbc);
|
||||||
|
pErr = Abc_FrameReadErr(pAbc);
|
||||||
|
|
||||||
|
// set defaults
|
||||||
|
fVerbose = 0;
|
||||||
|
Extra_UtilGetoptReset();
|
||||||
|
while ( ( c = Extra_UtilGetopt( argc, argv, "vh" ) ) != EOF )
|
||||||
|
{
|
||||||
|
switch ( c )
|
||||||
|
{
|
||||||
|
case 'v':
|
||||||
|
fVerbose ^= 1;
|
||||||
|
break;
|
||||||
|
case 'h':
|
||||||
|
goto usage;
|
||||||
|
default:
|
||||||
|
goto usage;
|
||||||
|
}
|
||||||
|
}
|
||||||
|
|
||||||
|
if ( pNtk == NULL )
|
||||||
|
{
|
||||||
|
fprintf( pErr, "Empty network.\n" );
|
||||||
|
return 1;
|
||||||
|
}
|
||||||
|
// get the new network
|
||||||
|
if ( !Abc_NtkIsStrash(pNtk) )
|
||||||
|
{
|
||||||
|
fprintf( pErr, "Does not work for a logic network.\n" );
|
||||||
|
return 1;
|
||||||
|
}
|
||||||
|
// check if balancing worked
|
||||||
|
// pNtkRes = Abc_NtkMuxRestructure( pNtk, fVerbose );
|
||||||
|
pNtkRes = NULL;
|
||||||
|
if ( pNtkRes == NULL )
|
||||||
|
{
|
||||||
|
fprintf( pErr, "MUX restructuring has failed.\n" );
|
||||||
|
return 1;
|
||||||
|
}
|
||||||
|
// replace the current network
|
||||||
|
Abc_FrameReplaceCurrentNetwork( pAbc, pNtkRes );
|
||||||
|
return 0;
|
||||||
|
|
||||||
|
usage:
|
||||||
|
fprintf( pErr, "usage: mux_struct [-vh]\n" );
|
||||||
|
fprintf( pErr, "\t performs MUX restructuring of the current network\n" );
|
||||||
|
fprintf( pErr, "\t-v : print verbose information [default = %s]\n", fVerbose? "yes": "no" );
|
||||||
|
fprintf( pErr, "\t-h : print the command usage\n");
|
||||||
|
return 1;
|
||||||
|
}
|
||||||
|
|
||||||
/**Function*************************************************************
|
/**Function*************************************************************
|
||||||
|
|
||||||
Synopsis []
|
Synopsis []
|
||||||
|
|
@ -15494,6 +15580,7 @@ usage:
|
||||||
return 1;
|
return 1;
|
||||||
}
|
}
|
||||||
|
|
||||||
|
|
||||||
/**Function*************************************************************
|
/**Function*************************************************************
|
||||||
|
|
||||||
Synopsis []
|
Synopsis []
|
||||||
|
|
@ -15507,39 +15594,21 @@ usage:
|
||||||
***********************************************************************/
|
***********************************************************************/
|
||||||
int Abc_CommandBmcInter( Abc_Frame_t * pAbc, int argc, char ** argv )
|
int Abc_CommandBmcInter( Abc_Frame_t * pAbc, int argc, char ** argv )
|
||||||
{
|
{
|
||||||
|
Inter_ManParams_t Pars, * pPars = &Pars;
|
||||||
FILE * pOut, * pErr;
|
FILE * pOut, * pErr;
|
||||||
Abc_Ntk_t * pNtk;
|
Abc_Ntk_t * pNtk;
|
||||||
int c;
|
int c;
|
||||||
int nBTLimit;
|
|
||||||
int nFramesMax;
|
|
||||||
int fRewrite;
|
|
||||||
int fTransLoop;
|
|
||||||
int fUsePudlak;
|
|
||||||
int fUseOther;
|
|
||||||
int fUseMiniSat;
|
|
||||||
int fCheckInd;
|
|
||||||
int fCheckKstep;
|
|
||||||
int fVerbose;
|
|
||||||
|
|
||||||
extern int Abc_NtkDarBmcInter( Abc_Ntk_t * pNtk, int nConfLimit, int nFramesMax, int fRewrite, int fTransLoop, int fUsePudlak, int fUseOther, int fUseMiniSat, int fCheckInd, int fCheckKstep, int fVerbose );
|
extern int Abc_NtkDarBmcInter( Abc_Ntk_t * pNtk, Inter_ManParams_t * pPars );
|
||||||
|
|
||||||
pNtk = Abc_FrameReadNtk(pAbc);
|
pNtk = Abc_FrameReadNtk(pAbc);
|
||||||
pOut = Abc_FrameReadOut(pAbc);
|
pOut = Abc_FrameReadOut(pAbc);
|
||||||
pErr = Abc_FrameReadErr(pAbc);
|
pErr = Abc_FrameReadErr(pAbc);
|
||||||
|
|
||||||
// set defaults
|
// set defaults
|
||||||
nBTLimit = 20000;
|
Inter_ManSetDefaultParams( pPars );
|
||||||
nFramesMax = 40;
|
|
||||||
fRewrite = 0;
|
|
||||||
fTransLoop = 1;
|
|
||||||
fUsePudlak = 0;
|
|
||||||
fUseOther = 0;
|
|
||||||
fUseMiniSat= 0;
|
|
||||||
fCheckInd = 0;
|
|
||||||
fCheckKstep= 0;
|
|
||||||
fVerbose = 0;
|
|
||||||
Extra_UtilGetoptReset();
|
Extra_UtilGetoptReset();
|
||||||
while ( ( c = Extra_UtilGetopt( argc, argv, "CFrtpomikvh" ) ) != EOF )
|
while ( ( c = Extra_UtilGetopt( argc, argv, "CNFrtpomcgbvh" ) ) != EOF )
|
||||||
{
|
{
|
||||||
switch ( c )
|
switch ( c )
|
||||||
{
|
{
|
||||||
|
|
@ -15549,9 +15618,20 @@ int Abc_CommandBmcInter( Abc_Frame_t * pAbc, int argc, char ** argv )
|
||||||
fprintf( pErr, "Command line switch \"-C\" should be followed by an integer.\n" );
|
fprintf( pErr, "Command line switch \"-C\" should be followed by an integer.\n" );
|
||||||
goto usage;
|
goto usage;
|
||||||
}
|
}
|
||||||
nBTLimit = atoi(argv[globalUtilOptind]);
|
pPars->nBTLimit = atoi(argv[globalUtilOptind]);
|
||||||
globalUtilOptind++;
|
globalUtilOptind++;
|
||||||
if ( nBTLimit < 0 )
|
if ( pPars->nBTLimit < 0 )
|
||||||
|
goto usage;
|
||||||
|
break;
|
||||||
|
case 'N':
|
||||||
|
if ( globalUtilOptind >= argc )
|
||||||
|
{
|
||||||
|
fprintf( pErr, "Command line switch \"-N\" should be followed by an integer.\n" );
|
||||||
|
goto usage;
|
||||||
|
}
|
||||||
|
pPars->nFramesMax = atoi(argv[globalUtilOptind]);
|
||||||
|
globalUtilOptind++;
|
||||||
|
if ( pPars->nFramesMax < 0 )
|
||||||
goto usage;
|
goto usage;
|
||||||
break;
|
break;
|
||||||
case 'F':
|
case 'F':
|
||||||
|
|
@ -15560,34 +15640,37 @@ int Abc_CommandBmcInter( Abc_Frame_t * pAbc, int argc, char ** argv )
|
||||||
fprintf( pErr, "Command line switch \"-F\" should be followed by an integer.\n" );
|
fprintf( pErr, "Command line switch \"-F\" should be followed by an integer.\n" );
|
||||||
goto usage;
|
goto usage;
|
||||||
}
|
}
|
||||||
nFramesMax = atoi(argv[globalUtilOptind]);
|
pPars->nFramesK = atoi(argv[globalUtilOptind]);
|
||||||
globalUtilOptind++;
|
globalUtilOptind++;
|
||||||
if ( nFramesMax < 0 )
|
if ( pPars->nFramesK < 0 )
|
||||||
goto usage;
|
goto usage;
|
||||||
break;
|
break;
|
||||||
case 'r':
|
case 'r':
|
||||||
fRewrite ^= 1;
|
pPars->fRewrite ^= 1;
|
||||||
break;
|
break;
|
||||||
case 't':
|
case 't':
|
||||||
fTransLoop ^= 1;
|
pPars->fTransLoop ^= 1;
|
||||||
break;
|
break;
|
||||||
case 'p':
|
case 'p':
|
||||||
fUsePudlak ^= 1;
|
pPars->fUsePudlak ^= 1;
|
||||||
break;
|
break;
|
||||||
case 'o':
|
case 'o':
|
||||||
fUseOther ^= 1;
|
pPars->fUseOther ^= 1;
|
||||||
break;
|
break;
|
||||||
case 'm':
|
case 'm':
|
||||||
fUseMiniSat ^= 1;
|
pPars->fUseMiniSat ^= 1;
|
||||||
break;
|
break;
|
||||||
case 'i':
|
case 'c':
|
||||||
fCheckInd ^= 1;
|
pPars->fCheckKstep ^= 1;
|
||||||
break;
|
break;
|
||||||
case 'k':
|
case 'g':
|
||||||
fCheckKstep ^= 1;
|
pPars->fUseBias ^= 1;
|
||||||
|
break;
|
||||||
|
case 'b':
|
||||||
|
pPars->fUseBackward ^= 1;
|
||||||
break;
|
break;
|
||||||
case 'v':
|
case 'v':
|
||||||
fVerbose ^= 1;
|
pPars->fVerbose ^= 1;
|
||||||
break;
|
break;
|
||||||
case 'h':
|
case 'h':
|
||||||
goto usage;
|
goto usage;
|
||||||
|
|
@ -15615,22 +15698,24 @@ int Abc_CommandBmcInter( Abc_Frame_t * pAbc, int argc, char ** argv )
|
||||||
fprintf( stdout, "Currently only works for single-output miters (run \"orpos\").\n" );
|
fprintf( stdout, "Currently only works for single-output miters (run \"orpos\").\n" );
|
||||||
return 0;
|
return 0;
|
||||||
}
|
}
|
||||||
Abc_NtkDarBmcInter( pNtk, nBTLimit, nFramesMax, fRewrite, fTransLoop, fUsePudlak, fUseOther, fUseMiniSat, fCheckInd, fCheckKstep, fVerbose );
|
Abc_NtkDarBmcInter( pNtk, pPars );
|
||||||
return 0;
|
return 0;
|
||||||
|
|
||||||
usage:
|
usage:
|
||||||
fprintf( pErr, "usage: int [-CF num] [-rtpomikvh]\n" );
|
fprintf( pErr, "usage: int [-CNF num] [-rtpomcgbvh]\n" );
|
||||||
fprintf( pErr, "\t uses interpolation to prove the property\n" );
|
fprintf( pErr, "\t uses interpolation to prove the property\n" );
|
||||||
fprintf( pErr, "\t-C num : the limit on conflicts for one SAT run [default = %d]\n", nBTLimit );
|
fprintf( pErr, "\t-C num : the limit on conflicts for one SAT run [default = %d]\n", pPars->nBTLimit );
|
||||||
fprintf( pErr, "\t-F num : the limit on number of frames to unroll [default = %d]\n", nFramesMax );
|
fprintf( pErr, "\t-N num : the limit on number of frames to unroll [default = %d]\n", pPars->nFramesMax );
|
||||||
fprintf( pErr, "\t-r : toggle the use of rewriting [default = %s]\n", fRewrite? "yes": "no" );
|
fprintf( pErr, "\t-F num : the number of steps in inductive checking [default = %d]\n", pPars->nFramesK );
|
||||||
fprintf( pErr, "\t-t : toggle adding transition into the init state [default = %s]\n", fTransLoop? "yes": "no" );
|
fprintf( pErr, "\t-r : toggle the use of rewriting unrolled timeframes [default = %s]\n", pPars->fRewrite? "yes": "no" );
|
||||||
fprintf( pErr, "\t-p : toggle using original Pudlak's interpolation procedure [default = %s]\n", fUsePudlak? "yes": "no" );
|
fprintf( pErr, "\t-t : toggle adding transition into the init state [default = %s]\n", pPars->fTransLoop? "yes": "no" );
|
||||||
fprintf( pErr, "\t-o : toggle using optimized Pudlak's interpolation procedure [default = %s]\n", fUseOther? "yes": "no" );
|
fprintf( pErr, "\t-p : toggle using original Pudlak's interpolation procedure [default = %s]\n", pPars->fUsePudlak? "yes": "no" );
|
||||||
fprintf( pErr, "\t-m : toggle using MiniSat-1.14p (now, Windows-only) [default = %s]\n", fUseMiniSat? "yes": "no" );
|
fprintf( pErr, "\t-o : toggle using optimized Pudlak's interpolation procedure [default = %s]\n", pPars->fUseOther? "yes": "no" );
|
||||||
fprintf( pErr, "\t-i : toggle inductive containment checking [default = %s]\n", fCheckInd? "yes": "no" );
|
fprintf( pErr, "\t-m : toggle using MiniSat-1.14p (now, Windows-only) [default = %s]\n", pPars->fUseMiniSat? "yes": "no" );
|
||||||
fprintf( pErr, "\t-k : toggle simple and k-step induction [default = %s]\n", fCheckKstep? "k-step": "simple" );
|
fprintf( pErr, "\t-c : toggle using inductive containment check [default = %s]\n", pPars->fCheckKstep? "yes": "no" );
|
||||||
fprintf( pErr, "\t-v : toggle verbose output [default = %s]\n", fVerbose? "yes": "no" );
|
fprintf( pErr, "\t-g : toggle using bias for global variables using SAT [default = %s]\n", pPars->fUseBias? "yes": "no" );
|
||||||
|
fprintf( pErr, "\t-b : toggle using backward interpolation [default = %s]\n", pPars->fUseBackward? "yes": "no" );
|
||||||
|
fprintf( pErr, "\t-v : toggle verbose output [default = %s]\n", pPars->fVerbose? "yes": "no" );
|
||||||
fprintf( pErr, "\t-h : print the command usage\n");
|
fprintf( pErr, "\t-h : print the command usage\n");
|
||||||
return 1;
|
return 1;
|
||||||
}
|
}
|
||||||
|
|
|
||||||
|
|
@ -25,6 +25,7 @@
|
||||||
#include "cnf.h"
|
#include "cnf.h"
|
||||||
#include "fra.h"
|
#include "fra.h"
|
||||||
#include "fraig.h"
|
#include "fraig.h"
|
||||||
|
#include "int.h"
|
||||||
|
|
||||||
////////////////////////////////////////////////////////////////////////
|
////////////////////////////////////////////////////////////////////////
|
||||||
/// DECLARATIONS ///
|
/// DECLARATIONS ///
|
||||||
|
|
@ -1295,7 +1296,7 @@ PRT( "Time", clock() - clk );
|
||||||
SeeAlso []
|
SeeAlso []
|
||||||
|
|
||||||
***********************************************************************/
|
***********************************************************************/
|
||||||
int Abc_NtkDarBmcInter( Abc_Ntk_t * pNtk, int nConfLimit, int nFramesMax, int fRewrite, int fTransLoop, int fUsePudlak, int fUseOther, int fUseMiniSat, int fCheckInd, int fCheckKstep, int fVerbose )
|
int Abc_NtkDarBmcInter( Abc_Ntk_t * pNtk, Inter_ManParams_t * pPars )
|
||||||
{
|
{
|
||||||
Aig_Man_t * pMan;
|
Aig_Man_t * pMan;
|
||||||
int RetValue, Depth, clk = clock();
|
int RetValue, Depth, clk = clock();
|
||||||
|
|
@ -1307,7 +1308,7 @@ int Abc_NtkDarBmcInter( Abc_Ntk_t * pNtk, int nConfLimit, int nFramesMax, int fR
|
||||||
return -1;
|
return -1;
|
||||||
}
|
}
|
||||||
assert( pMan->nRegs > 0 );
|
assert( pMan->nRegs > 0 );
|
||||||
RetValue = Saig_Interpolate( pMan, nConfLimit, nFramesMax, fRewrite, fTransLoop, fUsePudlak, fUseOther, fUseMiniSat, fCheckInd, fCheckKstep, fVerbose, &Depth );
|
RetValue = Inter_ManPerformInterpolation( pMan, pPars, &Depth );
|
||||||
if ( RetValue == 1 )
|
if ( RetValue == 1 )
|
||||||
printf( "Property proved. " );
|
printf( "Property proved. " );
|
||||||
else if ( RetValue == 0 )
|
else if ( RetValue == 0 )
|
||||||
|
|
|
||||||
|
|
@ -111,7 +111,7 @@ int Abc_NtkCompareAndSaveBest( Abc_Ntk_t * pNtk )
|
||||||
SeeAlso []
|
SeeAlso []
|
||||||
|
|
||||||
***********************************************************************/
|
***********************************************************************/
|
||||||
void Abc_NtkPrintStats( FILE * pFile, Abc_Ntk_t * pNtk, int fFactored, int fSaveBest, int fDumpResult, int fUseLutLib )
|
void Abc_NtkPrintStats( FILE * pFile, Abc_Ntk_t * pNtk, int fFactored, int fSaveBest, int fDumpResult, int fUseLutLib, int fPrintMuxes )
|
||||||
{
|
{
|
||||||
int Num;
|
int Num;
|
||||||
|
|
||||||
|
|
@ -153,6 +153,12 @@ void Abc_NtkPrintStats( FILE * pFile, Abc_Ntk_t * pNtk, int fFactored, int fSave
|
||||||
// fprintf( pFile, " (mux = %d)", Num2-Num );
|
// fprintf( pFile, " (mux = %d)", Num2-Num );
|
||||||
// if ( Num2 )
|
// if ( Num2 )
|
||||||
// fprintf( pFile, " (other = %d)", Abc_NtkNodeNum(pNtk)-3*Num2 );
|
// fprintf( pFile, " (other = %d)", Abc_NtkNodeNum(pNtk)-3*Num2 );
|
||||||
|
if ( fPrintMuxes )
|
||||||
|
{
|
||||||
|
extern int Abc_NtkCountMuxes( Abc_Ntk_t * pNtk );
|
||||||
|
fprintf( pFile, " (mux = %d)", Abc_NtkCountMuxes(pNtk)-Num );
|
||||||
|
fprintf( pFile, " (pure and = %d)", Abc_NtkNodeNum(pNtk) - (Abc_NtkCountMuxes(pNtk) * 3) );
|
||||||
|
}
|
||||||
}
|
}
|
||||||
else
|
else
|
||||||
{
|
{
|
||||||
|
|
|
||||||
|
|
@ -275,6 +275,12 @@ void Io_WriteDotNtk( Abc_Ntk_t * pNtk, Vec_Ptr_t * vNodes, Vec_Ptr_t * vNodesSho
|
||||||
fprintf( pFile, " Level%d;\n", Level );
|
fprintf( pFile, " Level%d;\n", Level );
|
||||||
Vec_PtrForEachEntry( vNodes, pNode, i )
|
Vec_PtrForEachEntry( vNodes, pNode, i )
|
||||||
{
|
{
|
||||||
|
if ( (int)pNode->Level != Level )
|
||||||
|
continue;
|
||||||
|
if ( Abc_ObjFaninNum(pNode) == 0 )
|
||||||
|
continue;
|
||||||
|
|
||||||
|
/*
|
||||||
int SuppSize;
|
int SuppSize;
|
||||||
Vec_Ptr_t * vSupp;
|
Vec_Ptr_t * vSupp;
|
||||||
if ( (int)pNode->Level != Level )
|
if ( (int)pNode->Level != Level )
|
||||||
|
|
@ -284,6 +290,7 @@ void Io_WriteDotNtk( Abc_Ntk_t * pNtk, Vec_Ptr_t * vNodes, Vec_Ptr_t * vNodesSho
|
||||||
vSupp = Abc_NtkNodeSupport( pNtk, &pNode, 1 );
|
vSupp = Abc_NtkNodeSupport( pNtk, &pNode, 1 );
|
||||||
SuppSize = Vec_PtrSize( vSupp );
|
SuppSize = Vec_PtrSize( vSupp );
|
||||||
Vec_PtrFree( vSupp );
|
Vec_PtrFree( vSupp );
|
||||||
|
*/
|
||||||
|
|
||||||
// fprintf( pFile, " Node%d [label = \"%d\"", pNode->Id, pNode->Id );
|
// fprintf( pFile, " Node%d [label = \"%d\"", pNode->Id, pNode->Id );
|
||||||
if ( Abc_NtkIsStrash(pNtk) )
|
if ( Abc_NtkIsStrash(pNtk) )
|
||||||
|
|
@ -294,10 +301,10 @@ void Io_WriteDotNtk( Abc_Ntk_t * pNtk, Vec_Ptr_t * vNodes, Vec_Ptr_t * vNodesSho
|
||||||
pSopString = Abc_NtkPrintSop(Mio_GateReadSop(pNode->pData));
|
pSopString = Abc_NtkPrintSop(Mio_GateReadSop(pNode->pData));
|
||||||
else
|
else
|
||||||
pSopString = Abc_NtkPrintSop(pNode->pData);
|
pSopString = Abc_NtkPrintSop(pNode->pData);
|
||||||
// fprintf( pFile, " Node%d [label = \"%d\\n%s\"", pNode->Id, pNode->Id, pSopString );
|
fprintf( pFile, " Node%d [label = \"%d\\n%s\"", pNode->Id, pNode->Id, pSopString );
|
||||||
fprintf( pFile, " Node%d [label = \"%d\\n%s\"", pNode->Id,
|
// fprintf( pFile, " Node%d [label = \"%d\\n%s\"", pNode->Id,
|
||||||
SuppSize,
|
// SuppSize,
|
||||||
pSopString );
|
// pSopString );
|
||||||
|
|
||||||
fprintf( pFile, ", shape = ellipse" );
|
fprintf( pFile, ", shape = ellipse" );
|
||||||
if ( pNode->fMarkB )
|
if ( pNode->fMarkB )
|
||||||
|
|
|
||||||
|
|
@ -34,7 +34,7 @@ static int Map_LibraryGetMaxSuperPi_rec( Map_Super_t * pGate );
|
||||||
static unsigned Map_LibraryGetGateSupp_rec( Map_Super_t * pGate );
|
static unsigned Map_LibraryGetGateSupp_rec( Map_Super_t * pGate );
|
||||||
|
|
||||||
// fanout limits
|
// fanout limits
|
||||||
static const int s_MapFanoutLimits[10] = { 1/*0*/, 10/*1*/, 5/*2*/, 2/*3*/, 1/*4*/, 1/*5*/, 1/*6*/ };
|
extern const int s_MapFanoutLimits[10] = { 1/*0*/, 10/*1*/, 5/*2*/, 2/*3*/, 1/*4*/, 1/*5*/, 1/*6*/ };
|
||||||
|
|
||||||
////////////////////////////////////////////////////////////////////////
|
////////////////////////////////////////////////////////////////////////
|
||||||
/// FUNCTION DEFINITIONS ///
|
/// FUNCTION DEFINITIONS ///
|
||||||
|
|
@ -124,7 +124,14 @@ int Map_LibraryReadFileTree( Map_SuperLib_t * pLib, FILE * pFile, char *pFileNam
|
||||||
|
|
||||||
// get the genlib file name (base)
|
// get the genlib file name (base)
|
||||||
pLibName = strtok( pTemp, " \t\r\n" );
|
pLibName = strtok( pTemp, " \t\r\n" );
|
||||||
|
#ifdef __linux__
|
||||||
|
if( strchr( pLibName, '/' ) != NULL )
|
||||||
|
pLibName = strrchr( pLibName, '/' ) + 1;
|
||||||
|
#else
|
||||||
|
if( strchr( pLibName, '\\' ) != NULL )
|
||||||
|
pLibName = strrchr( pLibName, '\\' ) + 1;
|
||||||
|
#endif
|
||||||
|
|
||||||
if ( strcmp( pLibName, "GATE" ) == 0 )
|
if ( strcmp( pLibName, "GATE" ) == 0 )
|
||||||
{
|
{
|
||||||
printf( "The input file \"%s\" looks like a GENLIB file and not a supergate library file.\n", pLib->pName );
|
printf( "The input file \"%s\" looks like a GENLIB file and not a supergate library file.\n", pLib->pName );
|
||||||
|
|
@ -145,7 +152,7 @@ int Map_LibraryReadFileTree( Map_SuperLib_t * pLib, FILE * pFile, char *pFileNam
|
||||||
if ( pStr == pLibFile )
|
if ( pStr == pLibFile )
|
||||||
strcpy( pLibFile, pLibName );
|
strcpy( pLibFile, pLibName );
|
||||||
else
|
else
|
||||||
sprintf( pStr, "/%s", pLibName );
|
sprintf( pStr, "\\%s", pLibName );
|
||||||
}
|
}
|
||||||
#endif
|
#endif
|
||||||
|
|
||||||
|
|
|
||||||
|
|
@ -0,0 +1,823 @@
|
||||||
|
/**CFile****************************************************************
|
||||||
|
|
||||||
|
FileName [mapperTree.c]
|
||||||
|
|
||||||
|
PackageName [MVSIS 1.3: Multi-valued logic synthesis system.]
|
||||||
|
|
||||||
|
Synopsis [Generic technology mapping engine.]
|
||||||
|
|
||||||
|
Author [MVSIS Group]
|
||||||
|
|
||||||
|
Affiliation [UC Berkeley]
|
||||||
|
|
||||||
|
Date [Ver. 2.0. Started - June 1, 2004.]
|
||||||
|
|
||||||
|
Revision [$Id: mapperTree.c,v 1.9 2005/01/23 06:59:45 alanmi Exp $]
|
||||||
|
|
||||||
|
***********************************************************************/
|
||||||
|
|
||||||
|
#ifdef __linux__
|
||||||
|
#include <libgen.h>
|
||||||
|
#endif
|
||||||
|
|
||||||
|
#include "mapperInt.h"
|
||||||
|
|
||||||
|
////////////////////////////////////////////////////////////////////////
|
||||||
|
/// DECLARATIONS ///
|
||||||
|
////////////////////////////////////////////////////////////////////////
|
||||||
|
|
||||||
|
static int Map_LibraryReadFileTree( Map_SuperLib_t * pLib, FILE * pFile, char *pFileName );
|
||||||
|
static Map_Super_t * Map_LibraryReadGateTree( Map_SuperLib_t * pLib, char * pBuffer, int Number, int nVars );
|
||||||
|
static int Map_LibraryDeriveGateInfo( Map_SuperLib_t * pLib, st_table * tExcludeGate );
|
||||||
|
static void Map_LibraryAddFaninDelays( Map_SuperLib_t * pLib, Map_Super_t * pGate, Map_Super_t * pFanin, Mio_Pin_t * pPin );
|
||||||
|
static int Map_LibraryGetMaxSuperPi_rec( Map_Super_t * pGate );
|
||||||
|
static unsigned Map_LibraryGetGateSupp_rec( Map_Super_t * pGate );
|
||||||
|
|
||||||
|
// fanout limits
|
||||||
|
extern const int s_MapFanoutLimits[10] = { 1/*0*/, 10/*1*/, 5/*2*/, 2/*3*/, 1/*4*/, 1/*5*/, 1/*6*/ };
|
||||||
|
|
||||||
|
////////////////////////////////////////////////////////////////////////
|
||||||
|
/// FUNCTION DEFINITIONS ///
|
||||||
|
////////////////////////////////////////////////////////////////////////
|
||||||
|
|
||||||
|
/**Function*************************************************************
|
||||||
|
|
||||||
|
Synopsis [Reads the supergate library from file.]
|
||||||
|
|
||||||
|
Description []
|
||||||
|
|
||||||
|
SideEffects []
|
||||||
|
|
||||||
|
SeeAlso []
|
||||||
|
|
||||||
|
***********************************************************************/
|
||||||
|
int Map_LibraryReadTree( Map_SuperLib_t * pLib, char * pFileName, char * pExcludeFile )
|
||||||
|
{
|
||||||
|
FILE * pFile;
|
||||||
|
int Status, num;
|
||||||
|
Abc_Frame_t * pAbc;
|
||||||
|
st_table * tExcludeGate = 0;
|
||||||
|
|
||||||
|
// read the beginning of the file
|
||||||
|
assert( pLib->pGenlib == NULL );
|
||||||
|
pFile = Io_FileOpen( pFileName, "open_path", "r", 1 );
|
||||||
|
// pFile = fopen( pFileName, "r" );
|
||||||
|
if ( pFile == NULL )
|
||||||
|
{
|
||||||
|
printf( "Cannot open input file \"%s\".\n", pFileName );
|
||||||
|
return 0;
|
||||||
|
}
|
||||||
|
|
||||||
|
if ( pExcludeFile )
|
||||||
|
{
|
||||||
|
pAbc = Abc_FrameGetGlobalFrame();
|
||||||
|
|
||||||
|
tExcludeGate = st_init_table(strcmp, st_strhash);
|
||||||
|
if ( (num = Mio_LibraryReadExclude( pAbc, pExcludeFile, tExcludeGate )) == -1 )
|
||||||
|
{
|
||||||
|
st_free_table( tExcludeGate );
|
||||||
|
tExcludeGate = 0;
|
||||||
|
return 0;
|
||||||
|
}
|
||||||
|
|
||||||
|
fprintf ( Abc_FrameReadOut( pAbc ), "Read %d gates from exclude file\n", num );
|
||||||
|
}
|
||||||
|
|
||||||
|
Status = Map_LibraryReadFileTree( pLib, pFile, pFileName );
|
||||||
|
fclose( pFile );
|
||||||
|
if ( Status == 0 )
|
||||||
|
return 0;
|
||||||
|
// prepare the info about the library
|
||||||
|
return Map_LibraryDeriveGateInfo( pLib, tExcludeGate );
|
||||||
|
}
|
||||||
|
|
||||||
|
|
||||||
|
/**Function*************************************************************
|
||||||
|
|
||||||
|
Synopsis [Reads the library file.]
|
||||||
|
|
||||||
|
Description []
|
||||||
|
|
||||||
|
SideEffects []
|
||||||
|
|
||||||
|
SeeAlso []
|
||||||
|
|
||||||
|
***********************************************************************/
|
||||||
|
int Map_LibraryReadFileTree( Map_SuperLib_t * pLib, FILE * pFile, char *pFileName )
|
||||||
|
{
|
||||||
|
ProgressBar * pProgress;
|
||||||
|
char pBuffer[5000], pLibFile[5000];
|
||||||
|
FILE * pFileGen;
|
||||||
|
Map_Super_t * pGate;
|
||||||
|
char * pTemp = 0, * pLibName;
|
||||||
|
int nCounter, k, i;
|
||||||
|
|
||||||
|
// skip empty and comment lines
|
||||||
|
while ( fgets( pBuffer, 5000, pFile ) != NULL )
|
||||||
|
{
|
||||||
|
// skip leading spaces
|
||||||
|
for ( pTemp = pBuffer; *pTemp == ' ' || *pTemp == '\r' || *pTemp == '\n'; pTemp++ );
|
||||||
|
// skip comment lines and empty lines
|
||||||
|
if ( *pTemp != 0 && *pTemp != '#' )
|
||||||
|
break;
|
||||||
|
}
|
||||||
|
|
||||||
|
// get the genlib file name (base)
|
||||||
|
pLibName = strtok( pTemp, " \t\r\n" );
|
||||||
|
#ifdef __linux__
|
||||||
|
pLibName = strrchr( pLibName, '/' )+1;
|
||||||
|
#else
|
||||||
|
pLibName = strrchr( pLibName, '\\' )+1;
|
||||||
|
#endif
|
||||||
|
|
||||||
|
if ( strcmp( pLibName, "GATE" ) == 0 )
|
||||||
|
{
|
||||||
|
printf( "The input file \"%s\" looks like a GENLIB file and not a supergate library file.\n", pLib->pName );
|
||||||
|
return 0;
|
||||||
|
}
|
||||||
|
|
||||||
|
|
||||||
|
// now figure out the directory if any in the pFileName
|
||||||
|
#ifdef __linux__
|
||||||
|
snprintf( pLibFile, 5000, "%s/%s", dirname(strdup(pFileName)), pLibName );
|
||||||
|
#else
|
||||||
|
{
|
||||||
|
char * pStr;
|
||||||
|
strcpy( pLibFile, pFileName );
|
||||||
|
pStr = pLibFile + strlen(pBuffer) - 1;
|
||||||
|
while ( pStr > pLibFile && *pStr != '\\' && *pStr != '/' )
|
||||||
|
pStr--;
|
||||||
|
if ( pStr == pLibFile )
|
||||||
|
strcpy( pLibFile, pLibName );
|
||||||
|
else
|
||||||
|
sprintf( pStr, "\\%s", pLibName );
|
||||||
|
}
|
||||||
|
#endif
|
||||||
|
|
||||||
|
pFileGen = Io_FileOpen( pLibFile, "open_path", "r", 1 );
|
||||||
|
// pFileGen = fopen( pLibFile, "r" );
|
||||||
|
if ( pFileGen == NULL )
|
||||||
|
{
|
||||||
|
printf( "Cannot open the GENLIB file \"%s\".\n", pLibFile );
|
||||||
|
return 0;
|
||||||
|
}
|
||||||
|
fclose( pFileGen );
|
||||||
|
|
||||||
|
// read the genlib library
|
||||||
|
pLib->pGenlib = Mio_LibraryRead( Abc_FrameGetGlobalFrame(), pLibFile, 0, 0 );
|
||||||
|
if ( pLib->pGenlib == NULL )
|
||||||
|
{
|
||||||
|
printf( "Cannot read GENLIB file \"%s\".\n", pLibFile );
|
||||||
|
return 0;
|
||||||
|
}
|
||||||
|
|
||||||
|
// read the number of variables
|
||||||
|
fscanf( pFile, "%d\n", &pLib->nVarsMax );
|
||||||
|
if ( pLib->nVarsMax < 2 || pLib->nVarsMax > 10 )
|
||||||
|
{
|
||||||
|
printf( "Suspicious number of variables (%d).\n", pLib->nVarsMax );
|
||||||
|
return 0;
|
||||||
|
}
|
||||||
|
|
||||||
|
// read the number of gates
|
||||||
|
fscanf( pFile, "%d\n", &pLib->nSupersReal );
|
||||||
|
if ( pLib->nSupersReal < 1 || pLib->nSupersReal > 10000000 )
|
||||||
|
{
|
||||||
|
printf( "Suspicious number of gates (%d).\n", pLib->nSupersReal );
|
||||||
|
return 0;
|
||||||
|
}
|
||||||
|
|
||||||
|
// read the number of lines
|
||||||
|
fscanf( pFile, "%d\n", &pLib->nLines );
|
||||||
|
if ( pLib->nLines < 1 || pLib->nLines > 10000000 )
|
||||||
|
{
|
||||||
|
printf( "Suspicious number of lines (%d).\n", pLib->nLines );
|
||||||
|
return 0;
|
||||||
|
}
|
||||||
|
|
||||||
|
// allocate room for supergate pointers
|
||||||
|
pLib->ppSupers = ALLOC( Map_Super_t *, pLib->nLines + 10000 );
|
||||||
|
|
||||||
|
// create the elementary supergates
|
||||||
|
for ( i = 0; i < pLib->nVarsMax; i++ )
|
||||||
|
{
|
||||||
|
// get a new gate
|
||||||
|
pGate = (Map_Super_t *)Extra_MmFixedEntryFetch( pLib->mmSupers );
|
||||||
|
memset( pGate, 0, sizeof(Map_Super_t) );
|
||||||
|
// assign the elementary variable, the truth table, and the delays
|
||||||
|
pGate->Num = i;
|
||||||
|
// set the truth table
|
||||||
|
pGate->uTruth[0] = pLib->uTruths[i][0];
|
||||||
|
pGate->uTruth[1] = pLib->uTruths[i][1];
|
||||||
|
// set the arrival times of all input to non-existent delay
|
||||||
|
for ( k = 0; k < pLib->nVarsMax; k++ )
|
||||||
|
{
|
||||||
|
pGate->tDelaysR[k].Rise = pGate->tDelaysR[k].Fall = MAP_NO_VAR;
|
||||||
|
pGate->tDelaysF[k].Rise = pGate->tDelaysF[k].Fall = MAP_NO_VAR;
|
||||||
|
}
|
||||||
|
// set an existent arrival time for rise and fall
|
||||||
|
pGate->tDelaysR[i].Rise = 0.0;
|
||||||
|
pGate->tDelaysF[i].Fall = 0.0;
|
||||||
|
// set the gate
|
||||||
|
pLib->ppSupers[i] = pGate;
|
||||||
|
}
|
||||||
|
|
||||||
|
// read the lines
|
||||||
|
nCounter = pLib->nVarsMax;
|
||||||
|
pProgress = Extra_ProgressBarStart( stdout, pLib->nLines );
|
||||||
|
while ( fgets( pBuffer, 5000, pFile ) != NULL )
|
||||||
|
{
|
||||||
|
for ( pTemp = pBuffer; *pTemp == ' ' || *pTemp == '\r' || *pTemp == '\n'; pTemp++ );
|
||||||
|
if ( pTemp[0] == '\0' )
|
||||||
|
continue;
|
||||||
|
// if ( pTemp[0] == 'a' || pTemp[2] == 'a' )
|
||||||
|
// {
|
||||||
|
// pLib->nLines--;
|
||||||
|
// continue;
|
||||||
|
// }
|
||||||
|
|
||||||
|
// get the gate
|
||||||
|
pGate = Map_LibraryReadGateTree( pLib, pTemp, nCounter, pLib->nVarsMax );
|
||||||
|
if ( pGate == NULL )
|
||||||
|
{
|
||||||
|
Extra_ProgressBarStop( pProgress );
|
||||||
|
return 0;
|
||||||
|
}
|
||||||
|
pLib->ppSupers[nCounter++] = pGate;
|
||||||
|
// later we will derive: truth table, delays, area, number of component gates, etc
|
||||||
|
|
||||||
|
// update the progress bar
|
||||||
|
Extra_ProgressBarUpdate( pProgress, nCounter, NULL );
|
||||||
|
}
|
||||||
|
Extra_ProgressBarStop( pProgress );
|
||||||
|
if ( nCounter != pLib->nLines )
|
||||||
|
printf( "The number of lines read (%d) is different what the file says (%d).\n", nCounter, pLib->nLines );
|
||||||
|
pLib->nSupersAll = nCounter;
|
||||||
|
// count the number of real supergates
|
||||||
|
nCounter = 0;
|
||||||
|
for ( k = 0; k < pLib->nLines; k++ )
|
||||||
|
nCounter += pLib->ppSupers[k]->fSuper;
|
||||||
|
if ( nCounter != pLib->nSupersReal )
|
||||||
|
printf( "The number of gates read (%d) is different what the file says (%d).\n", nCounter, pLib->nSupersReal );
|
||||||
|
pLib->nSupersReal = nCounter;
|
||||||
|
return 1;
|
||||||
|
}
|
||||||
|
|
||||||
|
/**Function*************************************************************
|
||||||
|
|
||||||
|
Synopsis [Reads one gate.]
|
||||||
|
|
||||||
|
Description []
|
||||||
|
|
||||||
|
SideEffects []
|
||||||
|
|
||||||
|
SeeAlso []
|
||||||
|
|
||||||
|
***********************************************************************/
|
||||||
|
Map_Super_t * Map_LibraryReadGateTree( Map_SuperLib_t * pLib, char * pBuffer, int Number, int nVarsMax )
|
||||||
|
{
|
||||||
|
Map_Super_t * pGate;
|
||||||
|
char * pTemp;
|
||||||
|
int i, Num;
|
||||||
|
|
||||||
|
// start and clean the gate
|
||||||
|
pGate = (Map_Super_t *)Extra_MmFixedEntryFetch( pLib->mmSupers );
|
||||||
|
memset( pGate, 0, sizeof(Map_Super_t) );
|
||||||
|
|
||||||
|
// set the gate number
|
||||||
|
pGate->Num = Number;
|
||||||
|
|
||||||
|
// read the mark
|
||||||
|
pTemp = strtok( pBuffer, " " );
|
||||||
|
if ( pTemp[0] == '*' )
|
||||||
|
{
|
||||||
|
pGate->fSuper = 1;
|
||||||
|
pTemp = strtok( NULL, " " );
|
||||||
|
}
|
||||||
|
|
||||||
|
// read the root gate
|
||||||
|
pGate->pRoot = Mio_LibraryReadGateByName( pLib->pGenlib, pTemp );
|
||||||
|
if ( pGate->pRoot == NULL )
|
||||||
|
{
|
||||||
|
printf( "Cannot read the root gate names %s.\n", pTemp );
|
||||||
|
return NULL;
|
||||||
|
}
|
||||||
|
// set the max number of fanouts
|
||||||
|
pGate->nFanLimit = s_MapFanoutLimits[ Mio_GateReadInputs(pGate->pRoot) ];
|
||||||
|
|
||||||
|
// read the pin-to-pin delay
|
||||||
|
for ( i = 0; ( pTemp = strtok( NULL, " \n\0" ) ); i++ )
|
||||||
|
{
|
||||||
|
if ( pTemp[0] == '#' )
|
||||||
|
break;
|
||||||
|
if ( i == nVarsMax )
|
||||||
|
{
|
||||||
|
printf( "There are too many entries on the line.\n" );
|
||||||
|
return NULL;
|
||||||
|
}
|
||||||
|
Num = atoi(pTemp);
|
||||||
|
if ( Num < 0 )
|
||||||
|
{
|
||||||
|
printf( "The number of a child supergate is negative.\n" );
|
||||||
|
return NULL;
|
||||||
|
}
|
||||||
|
if ( Num > pLib->nLines )
|
||||||
|
{
|
||||||
|
printf( "The number of a child supergate (%d) exceeded the number of lines (%d).\n",
|
||||||
|
Num, pLib->nLines );
|
||||||
|
return NULL;
|
||||||
|
}
|
||||||
|
pGate->pFanins[i] = pLib->ppSupers[Num];
|
||||||
|
}
|
||||||
|
pGate->nFanins = i;
|
||||||
|
if ( pGate->nFanins != (unsigned)Mio_GateReadInputs(pGate->pRoot) )
|
||||||
|
{
|
||||||
|
printf( "The number of fanins of a root gate is wrong.\n" );
|
||||||
|
return NULL;
|
||||||
|
}
|
||||||
|
|
||||||
|
// save the gate name, just in case
|
||||||
|
if ( pTemp && pTemp[0] == '#' )
|
||||||
|
{
|
||||||
|
if ( pTemp[1] == 0 )
|
||||||
|
pTemp = strtok( NULL, " \n\0" );
|
||||||
|
else // skip spaces
|
||||||
|
for ( pTemp++; *pTemp == ' '; pTemp++ );
|
||||||
|
// save the formula
|
||||||
|
pGate->pFormula = Extra_MmFlexEntryFetch( pLib->mmForms, strlen(pTemp)+1 );
|
||||||
|
strcpy( pGate->pFormula, pTemp );
|
||||||
|
}
|
||||||
|
// check the rest of the string
|
||||||
|
pTemp = strtok( NULL, " \n\0" );
|
||||||
|
if ( pTemp != NULL )
|
||||||
|
printf( "The following trailing symbols found \"%s\".\n", pTemp );
|
||||||
|
return pGate;
|
||||||
|
}
|
||||||
|
|
||||||
|
|
||||||
|
/**Function*************************************************************
|
||||||
|
|
||||||
|
Synopsis [Derives information about the library.]
|
||||||
|
|
||||||
|
Description []
|
||||||
|
|
||||||
|
SideEffects []
|
||||||
|
|
||||||
|
SeeAlso []
|
||||||
|
|
||||||
|
***********************************************************************/
|
||||||
|
int Map_LibraryDeriveGateInfo( Map_SuperLib_t * pLib, st_table * tExcludeGate )
|
||||||
|
{
|
||||||
|
Map_Super_t * pGate, * pFanin;
|
||||||
|
Mio_Pin_t * pPin;
|
||||||
|
unsigned uCanon[2];
|
||||||
|
unsigned uTruths[6][2];
|
||||||
|
int i, k, nRealVars;
|
||||||
|
|
||||||
|
// set all the derivable info related to the supergates
|
||||||
|
for ( i = pLib->nVarsMax; i < (int)pLib->nLines; i++ )
|
||||||
|
{
|
||||||
|
pGate = pLib->ppSupers[i];
|
||||||
|
|
||||||
|
if ( tExcludeGate )
|
||||||
|
{
|
||||||
|
if ( st_is_member( tExcludeGate, Mio_GateReadName( pGate->pRoot ) ) )
|
||||||
|
pGate->fExclude = 1;
|
||||||
|
for ( k = 0; k < (int)pGate->nFanins; k++ )
|
||||||
|
{
|
||||||
|
pFanin = pGate->pFanins[k];
|
||||||
|
if ( pFanin->fExclude )
|
||||||
|
{
|
||||||
|
pGate->fExclude = 1;
|
||||||
|
continue;
|
||||||
|
}
|
||||||
|
}
|
||||||
|
}
|
||||||
|
|
||||||
|
// collect the truth tables of the fanins
|
||||||
|
for ( k = 0; k < (int)pGate->nFanins; k++ )
|
||||||
|
{
|
||||||
|
pFanin = pGate->pFanins[k];
|
||||||
|
uTruths[k][0] = pFanin->uTruth[0];
|
||||||
|
uTruths[k][1] = pFanin->uTruth[1];
|
||||||
|
}
|
||||||
|
// derive the new truth table
|
||||||
|
Mio_DeriveTruthTable( pGate->pRoot, uTruths, pGate->nFanins, 6, pGate->uTruth );
|
||||||
|
|
||||||
|
// set the initial delays of the supergate
|
||||||
|
for ( k = 0; k < pLib->nVarsMax; k++ )
|
||||||
|
{
|
||||||
|
pGate->tDelaysR[k].Rise = pGate->tDelaysR[k].Fall = MAP_NO_VAR;
|
||||||
|
pGate->tDelaysF[k].Rise = pGate->tDelaysF[k].Fall = MAP_NO_VAR;
|
||||||
|
}
|
||||||
|
// get the linked list of pins for the given root gate
|
||||||
|
pPin = Mio_GateReadPins( pGate->pRoot );
|
||||||
|
// update the initial delay of the supergate using info from the corresponding pin
|
||||||
|
for ( k = 0; k < (int)pGate->nFanins; k++, pPin = Mio_PinReadNext(pPin) )
|
||||||
|
{
|
||||||
|
// if there is no corresponding pin, this is a bug, return fail
|
||||||
|
if ( pPin == NULL )
|
||||||
|
{
|
||||||
|
printf( "There are less pins than gate inputs.\n" );
|
||||||
|
return 0;
|
||||||
|
}
|
||||||
|
// update the delay information of k-th fanins info from the corresponding pin
|
||||||
|
Map_LibraryAddFaninDelays( pLib, pGate, pGate->pFanins[k], pPin );
|
||||||
|
}
|
||||||
|
// if there are some pins left, this is a bug, return fail
|
||||||
|
if ( pPin != NULL )
|
||||||
|
{
|
||||||
|
printf( "There are more pins than gate inputs.\n" );
|
||||||
|
return 0;
|
||||||
|
}
|
||||||
|
// find the max delay
|
||||||
|
pGate->tDelayMax.Rise = pGate->tDelayMax.Fall = MAP_NO_VAR;
|
||||||
|
for ( k = 0; k < pLib->nVarsMax; k++ )
|
||||||
|
{
|
||||||
|
// the rise of the output depends on the rise and fall of the output
|
||||||
|
if ( pGate->tDelayMax.Rise < pGate->tDelaysR[k].Rise )
|
||||||
|
pGate->tDelayMax.Rise = pGate->tDelaysR[k].Rise;
|
||||||
|
if ( pGate->tDelayMax.Rise < pGate->tDelaysR[k].Fall )
|
||||||
|
pGate->tDelayMax.Rise = pGate->tDelaysR[k].Fall;
|
||||||
|
// the fall of the output depends on the rise and fall of the output
|
||||||
|
if ( pGate->tDelayMax.Fall < pGate->tDelaysF[k].Rise )
|
||||||
|
pGate->tDelayMax.Fall = pGate->tDelaysF[k].Rise;
|
||||||
|
if ( pGate->tDelayMax.Fall < pGate->tDelaysF[k].Fall )
|
||||||
|
pGate->tDelayMax.Fall = pGate->tDelaysF[k].Fall;
|
||||||
|
|
||||||
|
pGate->tDelaysF[k].Worst = MAP_MAX( pGate->tDelaysF[k].Fall, pGate->tDelaysF[k].Rise );
|
||||||
|
pGate->tDelaysR[k].Worst = MAP_MAX( pGate->tDelaysR[k].Fall, pGate->tDelaysR[k].Rise );
|
||||||
|
}
|
||||||
|
|
||||||
|
// count gates and area of the supergate
|
||||||
|
pGate->nGates = 1;
|
||||||
|
pGate->Area = (float)Mio_GateReadArea(pGate->pRoot);
|
||||||
|
for ( k = 0; k < (int)pGate->nFanins; k++ )
|
||||||
|
{
|
||||||
|
pGate->nGates += pGate->pFanins[k]->nGates;
|
||||||
|
pGate->Area += pGate->pFanins[k]->Area;
|
||||||
|
}
|
||||||
|
// do not add the gate to the table, if this gate is an internal gate
|
||||||
|
// of some supegate and does not correspond to a supergate output
|
||||||
|
if ( ( !pGate->fSuper ) || pGate->fExclude )
|
||||||
|
continue;
|
||||||
|
|
||||||
|
// find the maximum index of a variable in the support of the supergates
|
||||||
|
// this is important for two reasons:
|
||||||
|
// (1) to limit the number of permutations considered for canonicization
|
||||||
|
// (2) to get rid of equivalence phases to speed-up matching
|
||||||
|
nRealVars = Map_LibraryGetMaxSuperPi_rec( pGate ) + 1;
|
||||||
|
assert( nRealVars > 0 && nRealVars <= pLib->nVarsMax );
|
||||||
|
// if there are some problems with this code, try this instead
|
||||||
|
// nRealVars = pLib->nVarsMax;
|
||||||
|
|
||||||
|
// find the N-canonical form of this supergate
|
||||||
|
pGate->nPhases = Map_CanonComputeSlow( pLib->uTruths, pLib->nVarsMax, nRealVars, pGate->uTruth, pGate->uPhases, uCanon );
|
||||||
|
// add the supergate into the table by its N-canonical table
|
||||||
|
Map_SuperTableInsertC( pLib->tTableC, uCanon, pGate );
|
||||||
|
/*
|
||||||
|
{
|
||||||
|
int uCanon1, uCanon2;
|
||||||
|
uCanon1 = uCanon[0];
|
||||||
|
pGate->uTruth[0] = ~pGate->uTruth[0];
|
||||||
|
pGate->uTruth[1] = ~pGate->uTruth[1];
|
||||||
|
Map_CanonComputeSlow( pLib->uTruths, pLib->nVarsMax, nRealVars, pGate->uTruth, pGate->uPhases, uCanon );
|
||||||
|
uCanon2 = uCanon[0];
|
||||||
|
Rwt_Man5ExploreCount( uCanon1 < uCanon2 ? uCanon1 : uCanon2 );
|
||||||
|
}
|
||||||
|
*/
|
||||||
|
}
|
||||||
|
// sort the gates in each line
|
||||||
|
Map_SuperTableSortSupergatesByDelay( pLib->tTableC, pLib->nSupersAll );
|
||||||
|
|
||||||
|
// let the glory be manifest
|
||||||
|
// Map_LibraryPrintTree( pLib );
|
||||||
|
return 1;
|
||||||
|
}
|
||||||
|
|
||||||
|
/**Function*************************************************************
|
||||||
|
|
||||||
|
Synopsis [Finds the largest PI number in the support of the supergate.]
|
||||||
|
|
||||||
|
Description []
|
||||||
|
|
||||||
|
SideEffects []
|
||||||
|
|
||||||
|
SeeAlso []
|
||||||
|
|
||||||
|
***********************************************************************/
|
||||||
|
int Map_LibraryGetMaxSuperPi_rec( Map_Super_t * pGate )
|
||||||
|
{
|
||||||
|
int i, VarCur, VarMax = 0;
|
||||||
|
if ( pGate->pRoot == NULL )
|
||||||
|
return pGate->Num;
|
||||||
|
for ( i = 0; i < (int)pGate->nFanins; i++ )
|
||||||
|
{
|
||||||
|
VarCur = Map_LibraryGetMaxSuperPi_rec( pGate->pFanins[i] );
|
||||||
|
if ( VarMax < VarCur )
|
||||||
|
VarMax = VarCur;
|
||||||
|
}
|
||||||
|
return VarMax;
|
||||||
|
}
|
||||||
|
|
||||||
|
/**Function*************************************************************
|
||||||
|
|
||||||
|
Synopsis [Finds the largest PI number in the support of the supergate.]
|
||||||
|
|
||||||
|
Description []
|
||||||
|
|
||||||
|
SideEffects []
|
||||||
|
|
||||||
|
SeeAlso []
|
||||||
|
|
||||||
|
***********************************************************************/
|
||||||
|
unsigned Map_LibraryGetGateSupp_rec( Map_Super_t * pGate )
|
||||||
|
{
|
||||||
|
unsigned uSupport;
|
||||||
|
int i;
|
||||||
|
if ( pGate->pRoot == NULL )
|
||||||
|
return (unsigned)(1 << (pGate->Num));
|
||||||
|
uSupport = 0;
|
||||||
|
for ( i = 0; i < (int)pGate->nFanins; i++ )
|
||||||
|
uSupport |= Map_LibraryGetGateSupp_rec( pGate->pFanins[i] );
|
||||||
|
return uSupport;
|
||||||
|
}
|
||||||
|
|
||||||
|
/**Function*************************************************************
|
||||||
|
|
||||||
|
Synopsis [Derives the pin-to-pin delay constraints for the supergate.]
|
||||||
|
|
||||||
|
Description []
|
||||||
|
|
||||||
|
SideEffects []
|
||||||
|
|
||||||
|
SeeAlso []
|
||||||
|
|
||||||
|
***********************************************************************/
|
||||||
|
void Map_LibraryAddFaninDelays( Map_SuperLib_t * pLib, Map_Super_t * pGate, Map_Super_t * pFanin, Mio_Pin_t * pPin )
|
||||||
|
{
|
||||||
|
Mio_PinPhase_t PinPhase;
|
||||||
|
float tDelayBlockRise, tDelayBlockFall, tDelayPin;
|
||||||
|
bool fMaxDelay = 0;
|
||||||
|
int i;
|
||||||
|
|
||||||
|
// use this node to enable max-delay model
|
||||||
|
if ( fMaxDelay )
|
||||||
|
{
|
||||||
|
float tDelayBlockMax;
|
||||||
|
// get the maximum delay
|
||||||
|
tDelayBlockMax = (float)Mio_PinReadDelayBlockMax(pPin);
|
||||||
|
// go through the supergate inputs
|
||||||
|
for ( i = 0; i < pLib->nVarsMax; i++ )
|
||||||
|
{
|
||||||
|
if ( pFanin->tDelaysR[i].Rise < 0 )
|
||||||
|
continue;
|
||||||
|
tDelayPin = pFanin->tDelaysR[i].Rise + tDelayBlockMax;
|
||||||
|
if ( pGate->tDelaysR[i].Rise < tDelayPin )
|
||||||
|
pGate->tDelaysR[i].Rise = tDelayPin;
|
||||||
|
}
|
||||||
|
// go through the supergate inputs
|
||||||
|
for ( i = 0; i < pLib->nVarsMax; i++ )
|
||||||
|
{
|
||||||
|
if ( pFanin->tDelaysF[i].Fall < 0 )
|
||||||
|
continue;
|
||||||
|
tDelayPin = pFanin->tDelaysF[i].Fall + tDelayBlockMax;
|
||||||
|
if ( pGate->tDelaysF[i].Fall < tDelayPin )
|
||||||
|
pGate->tDelaysF[i].Fall = tDelayPin;
|
||||||
|
}
|
||||||
|
return;
|
||||||
|
}
|
||||||
|
|
||||||
|
// get the interesting parameters of this pin
|
||||||
|
PinPhase = Mio_PinReadPhase(pPin);
|
||||||
|
tDelayBlockRise = (float)Mio_PinReadDelayBlockRise( pPin );
|
||||||
|
tDelayBlockFall = (float)Mio_PinReadDelayBlockFall( pPin );
|
||||||
|
|
||||||
|
// update the rise and fall of the output depending on the phase of the pin
|
||||||
|
if ( PinPhase != MIO_PHASE_INV ) // NONINV phase is present
|
||||||
|
{
|
||||||
|
// the rise of the gate is determined by the rise of the fanin
|
||||||
|
// the fall of the gate is determined by the fall of the fanin
|
||||||
|
for ( i = 0; i < pLib->nVarsMax; i++ )
|
||||||
|
{
|
||||||
|
////////////////////////////////////////////////////////
|
||||||
|
// consider the rise of the gate
|
||||||
|
////////////////////////////////////////////////////////
|
||||||
|
// check two types of constraints on the rise of the fanin:
|
||||||
|
// (1) the constraints related to the rise of the PIs
|
||||||
|
// (2) the constraints related to the fall of the PIs
|
||||||
|
if ( pFanin->tDelaysR[i].Rise >= 0 ) // case (1)
|
||||||
|
{ // fanin's rise depends on the rise of i-th PI
|
||||||
|
// update the rise of the gate's output
|
||||||
|
if ( pGate->tDelaysR[i].Rise < pFanin->tDelaysR[i].Rise + tDelayBlockRise )
|
||||||
|
pGate->tDelaysR[i].Rise = pFanin->tDelaysR[i].Rise + tDelayBlockRise;
|
||||||
|
}
|
||||||
|
if ( pFanin->tDelaysR[i].Fall >= 0 ) // case (2)
|
||||||
|
{ // fanin's rise depends on the fall of i-th PI
|
||||||
|
// update the rise of the gate's output
|
||||||
|
if ( pGate->tDelaysR[i].Fall < pFanin->tDelaysR[i].Fall + tDelayBlockRise )
|
||||||
|
pGate->tDelaysR[i].Fall = pFanin->tDelaysR[i].Fall + tDelayBlockRise;
|
||||||
|
}
|
||||||
|
////////////////////////////////////////////////////////
|
||||||
|
|
||||||
|
////////////////////////////////////////////////////////
|
||||||
|
// consider the fall of the gate (similar)
|
||||||
|
////////////////////////////////////////////////////////
|
||||||
|
// check two types of constraints on the fall of the fanin:
|
||||||
|
// (1) the constraints related to the rise of the PIs
|
||||||
|
// (2) the constraints related to the fall of the PIs
|
||||||
|
if ( pFanin->tDelaysF[i].Rise >= 0 ) // case (1)
|
||||||
|
{
|
||||||
|
if ( pGate->tDelaysF[i].Rise < pFanin->tDelaysF[i].Rise + tDelayBlockFall )
|
||||||
|
pGate->tDelaysF[i].Rise = pFanin->tDelaysF[i].Rise + tDelayBlockFall;
|
||||||
|
}
|
||||||
|
if ( pFanin->tDelaysF[i].Fall >= 0 ) // case (2)
|
||||||
|
{
|
||||||
|
if ( pGate->tDelaysF[i].Fall < pFanin->tDelaysF[i].Fall + tDelayBlockFall )
|
||||||
|
pGate->tDelaysF[i].Fall = pFanin->tDelaysF[i].Fall + tDelayBlockFall;
|
||||||
|
}
|
||||||
|
////////////////////////////////////////////////////////
|
||||||
|
}
|
||||||
|
}
|
||||||
|
if ( PinPhase != MIO_PHASE_NONINV ) // INV phase is present
|
||||||
|
{
|
||||||
|
// the rise of the gate is determined by the fall of the fanin
|
||||||
|
// the fall of the gate is determined by the rise of the fanin
|
||||||
|
for ( i = 0; i < pLib->nVarsMax; i++ )
|
||||||
|
{
|
||||||
|
////////////////////////////////////////////////////////
|
||||||
|
// consider the rise of the gate's output
|
||||||
|
////////////////////////////////////////////////////////
|
||||||
|
// check two types of constraints on the fall of the fanin:
|
||||||
|
// (1) the constraints related to the rise of the PIs
|
||||||
|
// (2) the constraints related to the fall of the PIs
|
||||||
|
if ( pFanin->tDelaysF[i].Rise >= 0 ) // case (1)
|
||||||
|
{ // fanin's rise depends on the rise of i-th PI
|
||||||
|
// update the rise of the gate
|
||||||
|
if ( pGate->tDelaysR[i].Rise < pFanin->tDelaysF[i].Rise + tDelayBlockRise )
|
||||||
|
pGate->tDelaysR[i].Rise = pFanin->tDelaysF[i].Rise + tDelayBlockRise;
|
||||||
|
}
|
||||||
|
if ( pFanin->tDelaysF[i].Fall >= 0 ) // case (2)
|
||||||
|
{ // fanin's rise depends on the fall of i-th PI
|
||||||
|
// update the rise of the gate
|
||||||
|
if ( pGate->tDelaysR[i].Fall < pFanin->tDelaysF[i].Fall + tDelayBlockRise )
|
||||||
|
pGate->tDelaysR[i].Fall = pFanin->tDelaysF[i].Fall + tDelayBlockRise;
|
||||||
|
}
|
||||||
|
////////////////////////////////////////////////////////
|
||||||
|
|
||||||
|
////////////////////////////////////////////////////////
|
||||||
|
// consider the fall of the gate (similar)
|
||||||
|
////////////////////////////////////////////////////////
|
||||||
|
// check two types of constraints on the rise of the fanin:
|
||||||
|
// (1) the constraints related to the rise of the PIs
|
||||||
|
// (2) the constraints related to the fall of the PIs
|
||||||
|
if ( pFanin->tDelaysR[i].Rise >= 0 ) // case (1)
|
||||||
|
{
|
||||||
|
if ( pGate->tDelaysF[i].Rise < pFanin->tDelaysR[i].Rise + tDelayBlockFall )
|
||||||
|
pGate->tDelaysF[i].Rise = pFanin->tDelaysR[i].Rise + tDelayBlockFall;
|
||||||
|
}
|
||||||
|
if ( pFanin->tDelaysR[i].Fall >= 0 ) // case (2)
|
||||||
|
{
|
||||||
|
if ( pGate->tDelaysF[i].Fall < pFanin->tDelaysR[i].Fall + tDelayBlockFall )
|
||||||
|
pGate->tDelaysF[i].Fall = pFanin->tDelaysR[i].Fall + tDelayBlockFall;
|
||||||
|
}
|
||||||
|
////////////////////////////////////////////////////////
|
||||||
|
}
|
||||||
|
}
|
||||||
|
}
|
||||||
|
|
||||||
|
|
||||||
|
/**Function*************************************************************
|
||||||
|
|
||||||
|
Synopsis [Performs phase transformation for one function.]
|
||||||
|
|
||||||
|
Description []
|
||||||
|
|
||||||
|
SideEffects []
|
||||||
|
|
||||||
|
SeeAlso []
|
||||||
|
|
||||||
|
***********************************************************************/
|
||||||
|
unsigned Map_CalculatePhase( unsigned uTruths[][2], int nVars, unsigned uTruth, unsigned uPhase )
|
||||||
|
{
|
||||||
|
int v, Shift;
|
||||||
|
for ( v = 0, Shift = 1; v < nVars; v++, Shift <<= 1 )
|
||||||
|
if ( uPhase & Shift )
|
||||||
|
uTruth = (((uTruth & ~uTruths[v][0]) << Shift) | ((uTruth & uTruths[v][0]) >> Shift));
|
||||||
|
return uTruth;
|
||||||
|
}
|
||||||
|
|
||||||
|
/**Function*************************************************************
|
||||||
|
|
||||||
|
Synopsis [Performs phase transformation for one function.]
|
||||||
|
|
||||||
|
Description []
|
||||||
|
|
||||||
|
SideEffects []
|
||||||
|
|
||||||
|
SeeAlso []
|
||||||
|
|
||||||
|
***********************************************************************/
|
||||||
|
void Map_CalculatePhase6( unsigned uTruths[][2], int nVars, unsigned uTruth[], unsigned uPhase, unsigned uTruthRes[] )
|
||||||
|
{
|
||||||
|
unsigned uTemp;
|
||||||
|
int v, Shift;
|
||||||
|
|
||||||
|
// initialize the result
|
||||||
|
uTruthRes[0] = uTruth[0];
|
||||||
|
uTruthRes[1] = uTruth[1];
|
||||||
|
if ( uPhase == 0 )
|
||||||
|
return;
|
||||||
|
// compute the phase
|
||||||
|
for ( v = 0, Shift = 1; v < nVars; v++, Shift <<= 1 )
|
||||||
|
if ( uPhase & Shift )
|
||||||
|
{
|
||||||
|
if ( Shift < 32 )
|
||||||
|
{
|
||||||
|
uTruthRes[0] = (((uTruthRes[0] & ~uTruths[v][0]) << Shift) | ((uTruthRes[0] & uTruths[v][0]) >> Shift));
|
||||||
|
uTruthRes[1] = (((uTruthRes[1] & ~uTruths[v][1]) << Shift) | ((uTruthRes[1] & uTruths[v][1]) >> Shift));
|
||||||
|
}
|
||||||
|
else
|
||||||
|
{
|
||||||
|
uTemp = uTruthRes[0];
|
||||||
|
uTruthRes[0] = uTruthRes[1];
|
||||||
|
uTruthRes[1] = uTemp;
|
||||||
|
}
|
||||||
|
}
|
||||||
|
}
|
||||||
|
|
||||||
|
/**Function*************************************************************
|
||||||
|
|
||||||
|
Synopsis [Prints the supergate library after deriving parameters.]
|
||||||
|
|
||||||
|
Description [This procedure is very useful to see the library after
|
||||||
|
it has been read into the mapper by "read_super" and all the information
|
||||||
|
about the supergates derived.]
|
||||||
|
|
||||||
|
SideEffects []
|
||||||
|
|
||||||
|
SeeAlso []
|
||||||
|
|
||||||
|
***********************************************************************/
|
||||||
|
void Map_LibraryPrintTree( Map_SuperLib_t * pLib )
|
||||||
|
{
|
||||||
|
Map_Super_t * pGate;
|
||||||
|
int i, k;
|
||||||
|
|
||||||
|
// print all the info related to the supergates
|
||||||
|
// for ( i = pLib->nVarsMax; i < (int)pLib->nLines; i++ )
|
||||||
|
for ( i = pLib->nVarsMax; i < 20; i++ )
|
||||||
|
{
|
||||||
|
pGate = pLib->ppSupers[i];
|
||||||
|
|
||||||
|
// write the gate's fanin info and formula
|
||||||
|
printf( "%6d ", pGate->Num );
|
||||||
|
printf( "%c ", pGate->fSuper? '*' : ' ' );
|
||||||
|
printf( "%6s", Mio_GateReadName(pGate->pRoot) );
|
||||||
|
for ( k = 0; k < (int)pGate->nFanins; k++ )
|
||||||
|
printf( " %6d", pGate->pFanins[k]->Num );
|
||||||
|
printf( " %s", pGate->pFormula );
|
||||||
|
printf( "\n" );
|
||||||
|
|
||||||
|
// write the gate's derived info
|
||||||
|
Extra_PrintBinary( stdout, pGate->uTruth, 64 );
|
||||||
|
printf( " %3d", pGate->nGates );
|
||||||
|
printf( " %6.2f", pGate->Area );
|
||||||
|
printf( " (%4.2f, %4.2f)", pGate->tDelayMax.Rise, pGate->tDelayMax.Fall );
|
||||||
|
printf( "\n" );
|
||||||
|
for ( k = 0; k < pLib->nVarsMax; k++ )
|
||||||
|
{
|
||||||
|
// print the constraint on the rise of the gate in the form (D1, D2),
|
||||||
|
// where D1 is the constraint related to the rise of the k-th PI
|
||||||
|
// where D2 is the constraint related to the fall of the k-th PI
|
||||||
|
if ( pGate->tDelaysR[k].Rise < 0 && pGate->tDelaysR[k].Fall < 0 )
|
||||||
|
printf( " (----, ----)" );
|
||||||
|
else if ( pGate->tDelaysR[k].Fall < 0 )
|
||||||
|
printf( " (%4.2f, ----)", pGate->tDelaysR[k].Rise );
|
||||||
|
else if ( pGate->tDelaysR[k].Rise < 0 )
|
||||||
|
printf( " (----, %4.2f)", pGate->tDelaysR[k].Fall );
|
||||||
|
else
|
||||||
|
printf( " (%4.2f, %4.2f)", pGate->tDelaysR[k].Rise, pGate->tDelaysR[k].Fall );
|
||||||
|
|
||||||
|
// print the constraint on the fall of the gate in the form (D1, D2),
|
||||||
|
// where D1 is the constraint related to the rise of the k-th PI
|
||||||
|
// where D2 is the constraint related to the fall of the k-th PI
|
||||||
|
if ( pGate->tDelaysF[k].Rise < 0 && pGate->tDelaysF[k].Fall < 0 )
|
||||||
|
printf( " (----, ----)" );
|
||||||
|
else if ( pGate->tDelaysF[k].Fall < 0 )
|
||||||
|
printf( " (%4.2f, ----)", pGate->tDelaysF[k].Rise );
|
||||||
|
else if ( pGate->tDelaysF[k].Rise < 0 )
|
||||||
|
printf( " (----, %4.2f)", pGate->tDelaysF[k].Fall );
|
||||||
|
else
|
||||||
|
printf( " (%4.2f, %4.2f)", pGate->tDelaysF[k].Rise, pGate->tDelaysF[k].Fall );
|
||||||
|
printf( "\n" );
|
||||||
|
}
|
||||||
|
printf( "\n" );
|
||||||
|
}
|
||||||
|
}
|
||||||
|
|
||||||
|
////////////////////////////////////////////////////////////////////////
|
||||||
|
/// END OF FILE ///
|
||||||
|
////////////////////////////////////////////////////////////////////////
|
||||||
|
|
||||||
|
|
||||||
|
|
@ -226,7 +226,8 @@ static inline void act_var_rescale(sat_solver* s) {
|
||||||
}
|
}
|
||||||
|
|
||||||
static inline void act_var_bump(sat_solver* s, int v) {
|
static inline void act_var_bump(sat_solver* s, int v) {
|
||||||
s->activity[v] += s->var_inc;
|
// s->activity[v] += s->var_inc;
|
||||||
|
s->activity[v] += (s->pGlobalVars? 3.0 : 1.0) * s->var_inc;
|
||||||
if (s->activity[v] > 1e100)
|
if (s->activity[v] > 1e100)
|
||||||
act_var_rescale(s);
|
act_var_rescale(s);
|
||||||
//printf("bump %d %f\n", v-1, activity[v]);
|
//printf("bump %d %f\n", v-1, activity[v]);
|
||||||
|
|
@ -243,6 +244,15 @@ static inline void act_var_bump_factor(sat_solver* s, int v) {
|
||||||
order_update(s,v);
|
order_update(s,v);
|
||||||
}
|
}
|
||||||
|
|
||||||
|
static inline void act_var_bump_global(sat_solver* s, int v) {
|
||||||
|
s->activity[v] += (s->var_inc * 3.0 * s->pGlobalVars[v]);
|
||||||
|
if (s->activity[v] > 1e100)
|
||||||
|
act_var_rescale(s);
|
||||||
|
//printf("bump %d %f\n", v-1, activity[v]);
|
||||||
|
if (s->orderpos[v] != -1)
|
||||||
|
order_update(s,v);
|
||||||
|
}
|
||||||
|
|
||||||
static inline void act_var_decay(sat_solver* s) { s->var_inc *= s->var_decay; }
|
static inline void act_var_decay(sat_solver* s) { s->var_inc *= s->var_decay; }
|
||||||
|
|
||||||
static inline void act_clause_rescale(sat_solver* s) {
|
static inline void act_clause_rescale(sat_solver* s) {
|
||||||
|
|
@ -845,6 +855,11 @@ static lbool sat_solver_search(sat_solver* s, sint64 nof_conflicts, sint64 nof_l
|
||||||
for ( i = 0; i < s->act_vars.size; i++ )
|
for ( i = 0; i < s->act_vars.size; i++ )
|
||||||
act_var_bump_factor(s, s->act_vars.ptr[i]);
|
act_var_bump_factor(s, s->act_vars.ptr[i]);
|
||||||
|
|
||||||
|
// use activity factors in every restart
|
||||||
|
if ( s->pGlobalVars && veci_size(&s->act_vars) > 0 )
|
||||||
|
for ( i = 0; i < s->act_vars.size; i++ )
|
||||||
|
act_var_bump_global(s, s->act_vars.ptr[i]);
|
||||||
|
|
||||||
for (;;){
|
for (;;){
|
||||||
clause* confl = sat_solver_propagate(s);
|
clause* confl = sat_solver_propagate(s);
|
||||||
if (confl != 0){
|
if (confl != 0){
|
||||||
|
|
|
||||||
|
|
@ -180,6 +180,7 @@ struct sat_solver_t
|
||||||
|
|
||||||
int fSkipSimplify; // set to one to skip simplification of the clause database
|
int fSkipSimplify; // set to one to skip simplification of the clause database
|
||||||
|
|
||||||
|
int * pGlobalVars; // for experiments with global vars during interpolation
|
||||||
// clause store
|
// clause store
|
||||||
void * pStore;
|
void * pStore;
|
||||||
int fSolved;
|
int fSolved;
|
||||||
|
|
|
||||||
Loading…
Reference in New Issue