From ae4b51351c93983a1285ce1028e3bbd90a6d5721 Mon Sep 17 00:00:00 2001 From: Alan Mishchenko Date: Thu, 13 Jan 2011 12:38:59 -0800 Subject: Cumulative changes in the last few weeks. --- Makefile | 2 +- abcexe.dsp | 4 +- abclib.dsp | 102 ++++---- src/aig/cnf/cnf.h | 4 + src/aig/cnf/cnfCore.c | 53 ++++ src/aig/cnf/cnfMan.c | 2 + src/aig/cnf/cnfWrite.c | 171 +++++++++++- src/aig/fra/fra.h | 2 + src/aig/fra/fraSec.c | 23 +- src/aig/gia/gia.h | 1 + src/aig/gia/giaEquiv.c | 5 + src/aig/gia/giaSim.c | 29 ++- src/aig/gia/giaUtil.c | 4 + src/aig/gia/module.make | 1 + src/aig/live/liveness.c | 2 +- src/aig/live/ltl_parser.c | 1 + src/aig/llb/llbCore.c | 2 +- src/aig/llb/llbReach.c | 2 +- src/aig/mfx/mfxInt.h | 3 +- src/aig/mfx/mfxInter.c | 18 +- src/aig/mfx/mfxMan.c | 6 +- src/aig/mfx/mfxResub.c | 12 +- src/aig/mfx/mfxSat.c | 10 +- src/aig/saig/module.make | 1 + src/aig/saig/saig.h | 3 +- src/aig/saig/saigBmc2.c | 9 +- src/aig/saig/saigDup.c | 52 +++- src/aig/saig/saigPhase.c | 68 ++++- src/aig/ssw/ssw.h | 1 + src/aig/ssw/sswConstr.c | 4 +- src/aig/ssw/sswCore.c | 2 + src/aig/ssw/sswDyn.c | 4 +- src/aig/ssw/sswInt.h | 2 +- src/aig/ssw/sswSemi.c | 2 +- src/aig/ssw/sswSim.c | 96 ++----- src/aig/ssw/sswSweep.c | 52 +++- src/base/abci/abc.c | 637 ++++++++++++++++++++++++++++++++++----------- src/base/abci/abcBalance.c | 2 +- src/base/abci/abcCut.c | 2 +- src/base/abci/abcDar.c | 56 +++- src/base/abci/abcIvy.c | 2 +- src/base/cmd/cmdPlugin.c | 2 +- src/base/io/ioReadBlifMv.c | 1 + src/base/io/ioReadPla.c | 13 +- src/misc/util/utilFile.c | 6 + src/opt/mfs/mfsCore.c | 12 +- src/opt/mfs/mfsGia.c | 2 +- src/opt/mfs/mfsInt.h | 7 +- src/opt/mfs/mfsInter.c | 18 +- src/opt/mfs/mfsMan.c | 10 +- src/opt/mfs/mfsResub.c | 44 ++-- src/opt/mfs/mfsSat.c | 10 +- src/opt/mfs/module.make | 1 - src/sat/bsat/satSolver.c | 189 +++++++++++--- src/sat/bsat/satSolver.h | 2 - 55 files changed, 1326 insertions(+), 445 deletions(-) diff --git a/Makefile b/Makefile index 52b24c90..ee52118e 100644 --- a/Makefile +++ b/Makefile @@ -20,7 +20,7 @@ MODULES := \ src/opt/cut src/opt/dec src/opt/fxu src/opt/rwr src/opt/mfs \ src/opt/sim src/opt/ret src/opt/res src/opt/lpk \ src/sat/bsat src/sat/csat src/sat/msat src/sat/fraig \ - src/sat/psat \ + src/sat/psat src/sat/pdr \ src/aig/ivy src/aig/hop src/aig/rwt src/aig/deco \ src/aig/mem src/aig/dar src/aig/fra src/aig/cnf \ src/aig/csw src/aig/ioa src/aig/aig src/aig/kit \ diff --git a/abcexe.dsp b/abcexe.dsp index eab61b0c..58aa7c14 100644 --- a/abcexe.dsp +++ b/abcexe.dsp @@ -50,7 +50,7 @@ BSC32=bscmake.exe # ADD BSC32 /nologo LINK32=link.exe # ADD BASE LINK32 kernel32.lib user32.lib gdi32.lib winspool.lib comdlg32.lib advapi32.lib shell32.lib ole32.lib oleaut32.lib uuid.lib odbc32.lib odbccp32.lib kernel32.lib user32.lib gdi32.lib winspool.lib comdlg32.lib advapi32.lib shell32.lib ole32.lib oleaut32.lib uuid.lib odbc32.lib odbccp32.lib /nologo /subsystem:console /machine:I386 -# ADD LINK32 kernel32.lib user32.lib gdi32.lib winspool.lib comdlg32.lib advapi32.lib shell32.lib ole32.lib oleaut32.lib uuid.lib odbc32.lib odbccp32.lib kernel32.lib user32.lib gdi32.lib winspool.lib comdlg32.lib advapi32.lib shell32.lib ole32.lib oleaut32.lib uuid.lib odbc32.lib odbccp32.lib lib\abcr.lib lib\abcextr.lib /nologo /subsystem:console /incremental:yes /debug /machine:I386 /out:"_TEST/abc.exe" +# ADD LINK32 kernel32.lib user32.lib gdi32.lib winspool.lib comdlg32.lib advapi32.lib shell32.lib ole32.lib oleaut32.lib uuid.lib odbc32.lib odbccp32.lib kernel32.lib user32.lib gdi32.lib winspool.lib comdlg32.lib advapi32.lib shell32.lib ole32.lib oleaut32.lib uuid.lib odbc32.lib odbccp32.lib lib\abcr.lib /nologo /subsystem:console /incremental:yes /debug /machine:I386 /out:"_TEST/abc.exe" !ELSEIF "$(CFG)" == "abcexe - Win32 Debug" @@ -74,7 +74,7 @@ BSC32=bscmake.exe # ADD BSC32 /nologo LINK32=link.exe # ADD BASE LINK32 kernel32.lib user32.lib gdi32.lib winspool.lib comdlg32.lib advapi32.lib shell32.lib ole32.lib oleaut32.lib uuid.lib odbc32.lib odbccp32.lib kernel32.lib user32.lib gdi32.lib winspool.lib comdlg32.lib advapi32.lib shell32.lib ole32.lib oleaut32.lib uuid.lib odbc32.lib odbccp32.lib /nologo /subsystem:console /debug /machine:I386 /pdbtype:sept -# ADD LINK32 kernel32.lib user32.lib gdi32.lib winspool.lib comdlg32.lib advapi32.lib shell32.lib ole32.lib oleaut32.lib uuid.lib odbc32.lib odbccp32.lib kernel32.lib user32.lib gdi32.lib winspool.lib comdlg32.lib advapi32.lib shell32.lib ole32.lib oleaut32.lib uuid.lib odbc32.lib odbccp32.lib lib\abcd.lib lib\abcextd.lib /nologo /subsystem:console /debug /machine:I386 /out:"_TEST/abc.exe" +# ADD LINK32 kernel32.lib user32.lib gdi32.lib winspool.lib comdlg32.lib advapi32.lib shell32.lib ole32.lib oleaut32.lib uuid.lib odbc32.lib odbccp32.lib kernel32.lib user32.lib gdi32.lib winspool.lib comdlg32.lib advapi32.lib shell32.lib ole32.lib oleaut32.lib uuid.lib odbc32.lib odbccp32.lib lib\abcd.lib /nologo /subsystem:console /debug /machine:I386 /out:"_TEST/abc.exe" !ENDIF diff --git a/abclib.dsp b/abclib.dsp index d85b17ae..725b3a53 100644 --- a/abclib.dsp +++ b/abclib.dsp @@ -41,7 +41,7 @@ RSC=rc.exe # PROP Intermediate_Dir "ReleaseLib" # PROP Target_Dir "" # ADD BASE CPP /nologo /W3 /GX /O2 /D "WIN32" /D "NDEBUG" /D "_MBCS" /D "_LIB" /YX /FD /c -# ADD CPP /nologo /MD /W3 /GX /O2 /I "src/ext/ext" /I "src/misc/ext" /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/cov" /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" /I "src/aig/dch" /I "src/aig/ssw" /I "src/sat/lsat" /I "src/aig/cec" /I "src/aig/cgt" /I "src/aig/sec" /I "src/map/amap" /I "src/aig/fsim" /I "src/aig/gia" /I "src/aig/bbl" /I "src/aig/llb" /D "WIN32" /D "NDEBUG" /D "_CONSOLE" /D "_MBCS" /D ABC_DLL=ABC_DLLEXPORT /D "_CRT_SECURE_NO_DEPRECATE" /FR /YX /FD /c +# ADD CPP /nologo /MD /W3 /GX /O2 /I "src/sat/pdr" /I "src/ext/ext" /I "src/misc/ext" /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/cov" /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" /I "src/aig/dch" /I "src/aig/ssw" /I "src/sat/lsat" /I "src/aig/cec" /I "src/aig/cgt" /I "src/aig/sec" /I "src/map/amap" /I "src/aig/fsim" /I "src/aig/gia" /I "src/aig/bbl" /I "src/aig/llb" /D "WIN32" /D "NDEBUG" /D "_CONSOLE" /D "_MBCS" /D ABC_DLL=ABC_DLLEXPORT /D "_CRT_SECURE_NO_DEPRECATE" /FR /YX /FD /c # ADD BASE RSC /l 0x409 /d "NDEBUG" # ADD RSC /l 0x409 /d "NDEBUG" BSC32=bscmake.exe @@ -64,7 +64,7 @@ LIB32=link.exe -lib # PROP Intermediate_Dir "DebugLib" # PROP Target_Dir "" # ADD BASE CPP /nologo /W3 /Gm /GX /ZI /Od /D "WIN32" /D "_DEBUG" /D "_MBCS" /D "_LIB" /YX /FD /GZ /c -# ADD CPP /nologo /MDd /W3 /Gm /GX /ZI /Od /I "src/ext/ext" /I "src/misc/ext" /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/cov" /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" /I "src/aig/dch" /I "src/aig/ssw" /I "src/sat/lsat" /I "src/aig/cec" /I "src/aig/cgt" /I "src/aig/sec" /I "src/map/amap" /I "src/aig/fsim" /I "src/aig/gia" /I "src/aig/bbl" /I "src/aig/llb" /D "WIN32" /D "_DEBUG" /D "_CONSOLE" /D "_MBCS" /D ABC_DLL=ABC_DLLEXPORT /D "_CRT_SECURE_NO_DEPRECATE" /FR /YX /FD /GZ /c +# ADD CPP /nologo /MDd /W3 /Gm /GX /ZI /Od /I "src/sat/pdr" /I "src/ext/ext" /I "src/misc/ext" /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/cov" /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" /I "src/aig/dch" /I "src/aig/ssw" /I "src/sat/lsat" /I "src/aig/cec" /I "src/aig/cgt" /I "src/aig/sec" /I "src/map/amap" /I "src/aig/fsim" /I "src/aig/gia" /I "src/aig/bbl" /I "src/aig/llb" /D "WIN32" /D "_DEBUG" /D "_CONSOLE" /D "_MBCS" /D ABC_DLL=ABC_DLLEXPORT /D "_CRT_SECURE_NO_DEPRECATE" /FR /YX /FD /GZ /c # ADD BASE RSC /l 0x409 /d "_DEBUG" # ADD RSC /l 0x409 /d "_DEBUG" BSC32=bscmake.exe @@ -1306,16 +1306,56 @@ SOURCE=.\src\sat\psat\m114p.h SOURCE=.\src\sat\psat\m114p_types.h # End Source File # End Group -# Begin Group "nsat" +# Begin Group "lsat" # PROP Default_Filter "" +# Begin Source File + +SOURCE=.\src\sat\lsat\solver.h +# End Source File # End Group -# Begin Group "lsat" +# Begin Group "pdr" # PROP Default_Filter "" # Begin Source File -SOURCE=.\src\sat\lsat\solver.h +SOURCE=.\src\sat\pdr\pdr.h +# End Source File +# Begin Source File + +SOURCE=.\src\sat\pdr\pdrClass.c +# End Source File +# Begin Source File + +SOURCE=.\src\sat\pdr\pdrCnf.c +# End Source File +# Begin Source File + +SOURCE=.\src\sat\pdr\pdrCore.c +# End Source File +# Begin Source File + +SOURCE=.\src\sat\pdr\pdrInt.h +# End Source File +# Begin Source File + +SOURCE=.\src\sat\pdr\pdrInv.c +# End Source File +# Begin Source File + +SOURCE=.\src\sat\pdr\pdrMan.c +# End Source File +# Begin Source File + +SOURCE=.\src\sat\pdr\pdrSat.c +# End Source File +# Begin Source File + +SOURCE=.\src\sat\pdr\pdrTsim.c +# End Source File +# Begin Source File + +SOURCE=.\src\sat\pdr\pdrUtil.c # End Source File # End Group # End Group @@ -3483,6 +3523,10 @@ SOURCE=.\src\aig\saig\saigSynch.c # End Source File # Begin Source File +SOURCE=.\src\aig\saig\saigTempor.c +# End Source File +# Begin Source File + SOURCE=.\src\aig\saig\saigTrans.c # End Source File # Begin Source File @@ -3927,6 +3971,10 @@ SOURCE=.\src\aig\gia\giaSim.c # End Source File # Begin Source File +SOURCE=.\src\aig\gia\giaSim2.c +# End Source File +# Begin Source File + SOURCE=.\src\aig\gia\giaSort.c # End Source File # Begin Source File @@ -4038,50 +4086,6 @@ SOURCE=.\src\aig\llb\llbReach.c SOURCE=.\src\aig\llb\llbSched.c # End Source File # End Group -# Begin Group "sky" - -# PROP Default_Filter "" -# End Group -# Begin Group "pdr" - -# PROP Default_Filter "" -# Begin Source File - -SOURCE=.\src\xxx\pdr\pdr.c -# End Source File -# Begin Source File - -SOURCE=.\src\xxx\pdr\pdr.h -# End Source File -# Begin Source File - -SOURCE=.\src\xxx\pdr\pdrClass.c -# End Source File -# Begin Source File - -SOURCE=.\src\xxx\pdr\pdrCore.c -# End Source File -# Begin Source File - -SOURCE=.\src\xxx\pdr\pdrInt.h -# End Source File -# Begin Source File - -SOURCE=.\src\xxx\pdr\pdrMan.c -# End Source File -# Begin Source File - -SOURCE=.\src\xxx\pdr\pdrSat.c -# End Source File -# Begin Source File - -SOURCE=.\src\xxx\pdr\pdrTsim.c -# End Source File -# Begin Source File - -SOURCE=.\src\xxx\pdr\pdrUtil.c -# End Source File -# End Group # End Group # End Group # Begin Group "Header Files" diff --git a/src/aig/cnf/cnf.h b/src/aig/cnf/cnf.h index 7c3bf06b..42dcd9a9 100644 --- a/src/aig/cnf/cnf.h +++ b/src/aig/cnf/cnf.h @@ -62,6 +62,8 @@ struct Cnf_Dat_t_ int nClauses; // the number of CNF clauses int ** pClauses; // the CNF clauses int * pVarNums; // the number of CNF variable for each node ID (-1 if unused) + int * pObj2Clause; // the mapping of objects into clauses + int * pObj2Count; // the mapping of objects into clause number }; // the cut used to represent node in the AIG @@ -125,6 +127,7 @@ static inline void Cnf_ObjSetBestCut( Aig_Obj_t * pObj, Cnf_Cut_t * pCut /*=== cnfCore.c ========================================================*/ extern Vec_Int_t * Cnf_DeriveMappingArray( Aig_Man_t * pAig ); extern Cnf_Dat_t * Cnf_Derive( Aig_Man_t * pAig, int nOutputs ); +extern Cnf_Dat_t * Cnf_DeriveOther( Aig_Man_t * pAig ); extern Cnf_Man_t * Cnf_ManRead(); extern void Cnf_ClearMemory(); /*=== cnfCut.c ========================================================*/ @@ -167,6 +170,7 @@ extern Vec_Int_t * Cnf_DataCollectCoSatNums( Cnf_Dat_t * pCnf, Aig_Man_t * p extern Vec_Int_t * Cnf_ManWriteCnfMapping( Cnf_Man_t * p, Vec_Ptr_t * vMapped ); extern void Cnf_SopConvertToVector( char * pSop, int nCubes, Vec_Int_t * vCover ); extern Cnf_Dat_t * Cnf_ManWriteCnf( Cnf_Man_t * p, Vec_Ptr_t * vMapped, int nOutputs ); +extern Cnf_Dat_t * Cnf_ManWriteCnfOther( Cnf_Man_t * p, Vec_Ptr_t * vMapped ); extern Cnf_Dat_t * Cnf_DeriveSimple( Aig_Man_t * p, int nOutputs ); extern Cnf_Dat_t * Cnf_DeriveSimpleForRetiming( Aig_Man_t * p ); diff --git a/src/aig/cnf/cnfCore.c b/src/aig/cnf/cnfCore.c index 85c971c2..eb46e704 100644 --- a/src/aig/cnf/cnfCore.c +++ b/src/aig/cnf/cnfCore.c @@ -138,6 +138,59 @@ p->timeSave = clock() - clk; //ABC_PRT( "Saving ", p->timeSave ); return pCnf; } + +/**Function************************************************************* + + Synopsis [Converts AIG into the SAT solver.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Cnf_Dat_t * Cnf_DeriveOther( Aig_Man_t * pAig ) +{ + Cnf_Man_t * p; + Cnf_Dat_t * pCnf; + Vec_Ptr_t * vMapped; + Aig_MmFixed_t * pMemCuts; + int clk; + // allocate the CNF manager + if ( s_pManCnf == NULL ) + s_pManCnf = Cnf_ManStart(); + // connect the managers + p = s_pManCnf; + p->pManAig = pAig; + + // generate cuts for all nodes, assign cost, and find best cuts +clk = clock(); + pMemCuts = Dar_ManComputeCuts( pAig, 10, 0 ); +p->timeCuts = clock() - clk; + + // find the mapping +clk = clock(); + Cnf_DeriveMapping( p ); +p->timeMap = clock() - clk; +// Aig_ManScanMapping( p, 1 ); + + // convert it into CNF +clk = clock(); + Cnf_ManTransferCuts( p ); + vMapped = Cnf_ManScanMapping( p, 1, 1 ); + pCnf = Cnf_ManWriteCnfOther( p, vMapped ); + Vec_PtrFree( vMapped ); + Aig_MmFixedStop( pMemCuts, 0 ); +p->timeSave = clock() - clk; + + // reset reference counters + Aig_ManResetRefs( pAig ); +//ABC_PRT( "Cuts ", p->timeCuts ); +//ABC_PRT( "Map ", p->timeMap ); +//ABC_PRT( "Saving ", p->timeSave ); + return pCnf; +} /**Function************************************************************* diff --git a/src/aig/cnf/cnfMan.c b/src/aig/cnf/cnfMan.c index 762673ad..837ca2c2 100644 --- a/src/aig/cnf/cnfMan.c +++ b/src/aig/cnf/cnfMan.c @@ -180,6 +180,8 @@ void Cnf_DataFree( Cnf_Dat_t * p ) { if ( p == NULL ) return; + ABC_FREE( p->pObj2Clause ); + ABC_FREE( p->pObj2Count ); ABC_FREE( p->pClauses[0] ); ABC_FREE( p->pClauses ); ABC_FREE( p->pVarNums ); diff --git a/src/aig/cnf/cnfWrite.c b/src/aig/cnf/cnfWrite.c index 4f737305..7a9443f2 100644 --- a/src/aig/cnf/cnfWrite.c +++ b/src/aig/cnf/cnfWrite.c @@ -245,8 +245,7 @@ Cnf_Dat_t * Cnf_ManWriteCnf( Cnf_Man_t * p, Vec_Ptr_t * vMapped, int nOutputs ) //printf( "\n" ); // allocate CNF - pCnf = ABC_ALLOC( Cnf_Dat_t, 1 ); - memset( pCnf, 0, sizeof(Cnf_Dat_t) ); + pCnf = ABC_CALLOC( Cnf_Dat_t, 1 ); pCnf->pMan = p->pManAig; pCnf->nLiterals = nLiterals; pCnf->nClauses = nClauses; @@ -367,6 +366,174 @@ Cnf_Dat_t * Cnf_ManWriteCnf( Cnf_Man_t * p, Vec_Ptr_t * vMapped, int nOutputs ) // verify that the correct number of literals and clauses was written assert( pLits - pCnf->pClauses[0] == nLiterals ); assert( pClas - pCnf->pClauses == nClauses ); +//Cnf_DataPrint( pCnf, 1 ); + return pCnf; +} + + +/**Function************************************************************* + + Synopsis [Derives CNF for the mapping.] + + Description [Derives CNF with obj IDs as SAT vars and mapping of + objects into clauses (pObj2Clause and pObj2Count).] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Cnf_Dat_t * Cnf_ManWriteCnfOther( Cnf_Man_t * p, Vec_Ptr_t * vMapped ) +{ + Aig_Obj_t * pObj; + Cnf_Dat_t * pCnf; + Cnf_Cut_t * pCut; + Vec_Int_t * vCover, * vSopTemp; + int OutVar, PoVar, pVars[32], * pLits, ** pClas; + unsigned uTruth; + int i, k, nLiterals, nClauses, Cube; + + // count the number of literals and clauses + nLiterals = 1 + 4 * Aig_ManPoNum( p->pManAig ); + nClauses = 1 + 2 * Aig_ManPoNum( p->pManAig ); + Vec_PtrForEachEntry( Aig_Obj_t *, vMapped, pObj, i ) + { + assert( Aig_ObjIsNode(pObj) ); + pCut = Cnf_ObjBestCut( pObj ); + // positive polarity of the cut + if ( pCut->nFanins < 5 ) + { + uTruth = 0xFFFF & *Cnf_CutTruth(pCut); + nLiterals += Cnf_SopCountLiterals( p->pSops[uTruth], p->pSopSizes[uTruth] ) + p->pSopSizes[uTruth]; + assert( p->pSopSizes[uTruth] >= 0 ); + nClauses += p->pSopSizes[uTruth]; + } + else + { + nLiterals += Cnf_IsopCountLiterals( pCut->vIsop[1], pCut->nFanins ) + Vec_IntSize(pCut->vIsop[1]); + nClauses += Vec_IntSize(pCut->vIsop[1]); + } + // negative polarity of the cut + if ( pCut->nFanins < 5 ) + { + uTruth = 0xFFFF & ~*Cnf_CutTruth(pCut); + nLiterals += Cnf_SopCountLiterals( p->pSops[uTruth], p->pSopSizes[uTruth] ) + p->pSopSizes[uTruth]; + assert( p->pSopSizes[uTruth] >= 0 ); + nClauses += p->pSopSizes[uTruth]; + } + else + { + nLiterals += Cnf_IsopCountLiterals( pCut->vIsop[0], pCut->nFanins ) + Vec_IntSize(pCut->vIsop[0]); + nClauses += Vec_IntSize(pCut->vIsop[0]); + } + } + + // allocate CNF + pCnf = ABC_CALLOC( Cnf_Dat_t, 1 ); + pCnf->pMan = p->pManAig; + pCnf->nLiterals = nLiterals; + pCnf->nClauses = nClauses; + pCnf->pClauses = ABC_ALLOC( int *, nClauses + 1 ); + pCnf->pClauses[0] = ABC_ALLOC( int, nLiterals ); + pCnf->pClauses[nClauses] = pCnf->pClauses[0] + nLiterals; + // create room for variable numbers + pCnf->pObj2Clause = ABC_ALLOC( int, Aig_ManObjNumMax(p->pManAig) ); + pCnf->pObj2Count = ABC_ALLOC( int, Aig_ManObjNumMax(p->pManAig) ); + for ( i = 0; i < Aig_ManObjNumMax(p->pManAig); i++ ) + pCnf->pObj2Clause[i] = pCnf->pObj2Count[i] = -1; + pCnf->nVars = Aig_ManObjNumMax(p->pManAig); + + // clear the PI counters + Aig_ManForEachPi( p->pManAig, pObj, i ) + pCnf->pObj2Count[pObj->Id] = 0; + + // assign the clauses + vSopTemp = Vec_IntAlloc( 1 << 16 ); + pLits = pCnf->pClauses[0]; + pClas = pCnf->pClauses; + Vec_PtrForEachEntry( Aig_Obj_t *, vMapped, pObj, i ) + { + // remember the starting clause + pCnf->pObj2Clause[pObj->Id] = pClas - pCnf->pClauses; + pCnf->pObj2Count[pObj->Id] = 0; + + // get the best cut + pCut = Cnf_ObjBestCut( pObj ); + // save variables of this cut + OutVar = pObj->Id; + for ( k = 0; k < (int)pCut->nFanins; k++ ) + { + pVars[k] = pCut->pFanins[k]; + assert( pVars[k] <= Aig_ManObjNumMax(p->pManAig) ); + } + + // positive polarity of the cut + if ( pCut->nFanins < 5 ) + { + uTruth = 0xFFFF & *Cnf_CutTruth(pCut); + Cnf_SopConvertToVector( p->pSops[uTruth], p->pSopSizes[uTruth], vSopTemp ); + vCover = vSopTemp; + } + else + vCover = pCut->vIsop[1]; + Vec_IntForEachEntry( vCover, Cube, k ) + { + *pClas++ = pLits; + *pLits++ = 2 * OutVar; + pLits += Cnf_IsopWriteCube( Cube, pCut->nFanins, pVars, pLits ); + } + pCnf->pObj2Count[pObj->Id] += Vec_IntSize(vCover); + + // negative polarity of the cut + if ( pCut->nFanins < 5 ) + { + uTruth = 0xFFFF & ~*Cnf_CutTruth(pCut); + Cnf_SopConvertToVector( p->pSops[uTruth], p->pSopSizes[uTruth], vSopTemp ); + vCover = vSopTemp; + } + else + vCover = pCut->vIsop[0]; + Vec_IntForEachEntry( vCover, Cube, k ) + { + *pClas++ = pLits; + *pLits++ = 2 * OutVar + 1; + pLits += Cnf_IsopWriteCube( Cube, pCut->nFanins, pVars, pLits ); + } + pCnf->pObj2Count[pObj->Id] += Vec_IntSize(vCover); + } + Vec_IntFree( vSopTemp ); + + // write the output literals + Aig_ManForEachPo( p->pManAig, pObj, i ) + { + // remember the starting clause + pCnf->pObj2Clause[pObj->Id] = pClas - pCnf->pClauses; + pCnf->pObj2Count[pObj->Id] = 2; + // get variables + OutVar = Aig_ObjFanin0(pObj)->Id; + PoVar = pObj->Id; + // first clause + *pClas++ = pLits; + *pLits++ = 2 * PoVar; + *pLits++ = 2 * OutVar + !Aig_ObjFaninC0(pObj); + // second clause + *pClas++ = pLits; + *pLits++ = 2 * PoVar + 1; + *pLits++ = 2 * OutVar + Aig_ObjFaninC0(pObj); + } + + // remember the starting clause + pCnf->pObj2Clause[Aig_ManConst1(p->pManAig)->Id] = pClas - pCnf->pClauses; + pCnf->pObj2Count[Aig_ManConst1(p->pManAig)->Id] = 1; + // write the constant literal + OutVar = Aig_ManConst1(p->pManAig)->Id; + *pClas++ = pLits; + *pLits++ = 2 * OutVar; + + // verify that the correct number of literals and clauses was written + assert( pLits - pCnf->pClauses[0] == nLiterals ); + assert( pClas - pCnf->pClauses == nClauses ); +//Cnf_DataPrint( pCnf, 1 ); return pCnf; } diff --git a/src/aig/fra/fra.h b/src/aig/fra/fra.h index b046cc47..aee38d08 100644 --- a/src/aig/fra/fra.h +++ b/src/aig/fra/fra.h @@ -123,6 +123,7 @@ struct Fra_Sec_t_ int nBddVarsMax; // the state space limit for BDD reachability int nBddMax; // the max number of BDD nodes int nBddIterMax; // the limit on the number of BDD iterations + int nPdrTimeout; // the timeout for PDR in the end int fPhaseAbstract; // enables phase abstraction int fRetimeFirst; // enables most-forward retiming at the beginning int fRetimeRegs; // enables min-register retiming at the beginning @@ -134,6 +135,7 @@ struct Fra_Sec_t_ int fReorderImage; // enables BDD reordering during image computation int fStopOnFirstFail; // enables stopping after first output of a miter has failed to prove int fUseNewProver; // the new prover + int fUsePdr; // the PDR int fSilent; // disables all output int fVerbose; // enables verbose reporting of statistics int fVeryVerbose; // enables very verbose reporting diff --git a/src/aig/fra/fraSec.c b/src/aig/fra/fraSec.c index 1576a70a..7608791f 100644 --- a/src/aig/fra/fraSec.c +++ b/src/aig/fra/fraSec.c @@ -24,6 +24,7 @@ #include "ssw.h" #include "saig.h" #include "bbr.h" +#include "pdr.h" ABC_NAMESPACE_IMPL_START @@ -70,6 +71,8 @@ void Fra_SecSetDefaultParams( Fra_Sec_t * p ) p->fReorderImage = 1; // enables variable reordering during image computation p->fStopOnFirstFail = 1; // enables stopping after first output of a miter has failed to prove p->fUseNewProver = 0; // enables new prover + p->fUsePdr = 1; // enables PDR + p->nPdrTimeout = 60; // enabled PDR timeout p->fSilent = 0; // disables all output p->fVerbose = 0; // enables verbose reporting of statistics p->fVeryVerbose = 0; // enables very verbose reporting @@ -539,7 +542,7 @@ clk = clock(); } else { - Aig_Man_t * pNewOrpos = Said_ManDupOrpos( pNew ); + Aig_Man_t * pNewOrpos = Saig_ManDupOrpos( pNew ); RetValue = Inter_ManPerformInterpolation( pNewOrpos, pPars, &Depth ); if ( pNewOrpos->pSeqModel ) { @@ -582,6 +585,24 @@ ABC_PRT( "Time", clock() - clk ); RetValue = Aig_ManVerifyUsingBdds( pNew, pPars ); } + // try PDR + if ( pParSec->fUsePdr && RetValue == -1 && Aig_ManRegNum(pNew) > 0 ) + { + Abc_Cex_t * pCex = NULL; + Aig_Man_t * pNewOrpos = Saig_ManDupOrpos( pNew ); + Pdr_Par_t Pars, * pPars = &Pars; + Pdr_ManSetDefaultParams( pPars ); + pPars->nTimeOut = pParSec->nPdrTimeout; + pPars->fVerbose = pParSec->fVerbose; + if ( pParSec->fVerbose ) + printf( "Running property directed reachability...\n" ); + RetValue = Pdr_ManSolve( pNewOrpos, pPars, &pCex ); + if ( pCex ) + pCex->iPo = Ssw_SmlFindOutputCounterExample( pNew, pCex ); + Aig_ManStop( pNewOrpos ); + pNew->pSeqModel = pCex; + } + finish: // report the miter if ( RetValue == 1 ) diff --git a/src/aig/gia/gia.h b/src/aig/gia/gia.h index 3358ca76..e3546686 100644 --- a/src/aig/gia/gia.h +++ b/src/aig/gia/gia.h @@ -179,6 +179,7 @@ struct Gia_ParSim_t_ // user-controlled parameters int nWords; // the number of machine words int nIters; // the number of timeframes + int RandSeed; // seed to generate random numbers int TimeLimit; // time limit in seconds int fCheckMiter; // check if miter outputs are non-zero int fVerbose; // enables verbose output diff --git a/src/aig/gia/giaEquiv.c b/src/aig/gia/giaEquiv.c index 4c19b4f5..581383ea 100644 --- a/src/aig/gia/giaEquiv.c +++ b/src/aig/gia/giaEquiv.c @@ -1049,6 +1049,11 @@ Gia_Man_t * Gia_ManSpecReduceInitFrames( Gia_Man_t * p, Abc_Cex_t * pInit, int n break; if ( f == nFramesMax ) break; + if ( Gia_ManAndNum(pFrames) > 500000 ) + { + Gia_ManStop( pFrames ); + return NULL; + } Gia_ManStop( pFrames ); pFrames = NULL; } diff --git a/src/aig/gia/giaSim.c b/src/aig/gia/giaSim.c index 68b50fb6..1de1a2d4 100644 --- a/src/aig/gia/giaSim.c +++ b/src/aig/gia/giaSim.c @@ -65,6 +65,7 @@ void Gia_ManSimSetDefaultParams( Gia_ParSim_t * p ) // user-controlled parameters p->nWords = 8; // the number of machine words p->nIters = 32; // the number of timeframes + p->RandSeed = 0; // the seed to generate random numbers p->TimeLimit = 60; // time limit in seconds p->fCheckMiter = 0; // check if miter outputs are non-zero p->fVerbose = 0; // enables verbose output @@ -437,9 +438,8 @@ Abc_Cex_t * Gia_ManGenerateCounter( Gia_Man_t * pAig, int iFrame, int iOut, int int f, i, w, iPioId, Counter; p = Gia_ManAllocCounterExample( Gia_ManRegNum(pAig), Gia_ManPiNum(pAig), iFrame+1 ); p->iFrame = iFrame; - p->iPo = iOut; + p->iPo = iOut; // fill in the binary data - Gia_ManRandom( 1 ); Counter = p->nRegs; pData = ABC_ALLOC( unsigned, nWords ); for ( f = 0; f <= iFrame; f++, Counter += p->nPis ) @@ -457,6 +457,25 @@ Abc_Cex_t * Gia_ManGenerateCounter( Gia_Man_t * pAig, int iFrame, int iOut, int return p; } +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Gia_ManResetRandom( Gia_ParSim_t * pPars ) +{ + int i; + Gia_ManRandom( 1 ); + for ( i = 0; i < pPars->RandSeed; i++ ) + Gia_ManRandom( 0 ); +} + /**Function************************************************************* Synopsis [] @@ -470,12 +489,15 @@ Abc_Cex_t * Gia_ManGenerateCounter( Gia_Man_t * pAig, int iFrame, int iOut, int ***********************************************************************/ int Gia_ManSimSimulate( Gia_Man_t * pAig, Gia_ParSim_t * pPars ) { + extern int Gia_ManSimSimulateEquiv( Gia_Man_t * pAig, Gia_ParSim_t * pPars ); Gia_ManSim_t * p; int i, clkTotal = clock(); int iOut, iPat, RetValue = 0; + if ( pAig->pReprs && pAig->pNexts ) + return Gia_ManSimSimulateEquiv( pAig, pPars ); ABC_FREE( pAig->pCexSeq ); p = Gia_ManSimCreate( pAig, pPars ); - Gia_ManRandom( 1 ); + Gia_ManResetRandom( pPars ); Gia_ManSimInfoInit( p ); for ( i = 0; i < pPars->nIters; i++ ) { @@ -487,6 +509,7 @@ int Gia_ManSimSimulate( Gia_Man_t * pAig, Gia_ParSim_t * pPars ) } if ( pPars->fCheckMiter && Gia_ManCheckPos( p, &iOut, &iPat ) ) { + Gia_ManResetRandom( pPars ); pPars->iOutFail = iOut; pAig->pCexSeq = Gia_ManGenerateCounter( pAig, i, iOut, p->nWords, iPat, p->vCis2Ids ); Abc_Print( 1, "Networks are NOT EQUIVALENT. Output %d was asserted in frame %d. ", iOut, i ); diff --git a/src/aig/gia/giaUtil.c b/src/aig/gia/giaUtil.c index 002e766d..82bdb367 100644 --- a/src/aig/gia/giaUtil.c +++ b/src/aig/gia/giaUtil.c @@ -952,8 +952,12 @@ int Gia_ManVerifyCounterExample( Gia_Man_t * pAig, Abc_Cex_t * p, int fDualOut ) (Gia_ObjFanin1(pObj)->fMark0 ^ Gia_ObjFaninC1(pObj)); Gia_ManForEachCo( pAig, pObj, k ) pObj->fMark0 = Gia_ObjFanin0(pObj)->fMark0 ^ Gia_ObjFaninC0(pObj); + if ( i == p->iFrame ) + break; Gia_ManForEachRiRo( pAig, pObjRi, pObjRo, k ) + { pObjRo->fMark0 = pObjRi->fMark0; + } } assert( iBit == p->nBits ); if ( fDualOut ) diff --git a/src/aig/gia/module.make b/src/aig/gia/module.make index fc1c5c73..fd0e0a5e 100644 --- a/src/aig/gia/module.make +++ b/src/aig/gia/module.make @@ -29,6 +29,7 @@ SRC += src/aig/gia/gia.c \ src/aig/gia/giaScl.c \ src/aig/gia/giaShrink.c \ src/aig/gia/giaSim.c \ + src/aig/gia/giaSim2.c \ src/aig/gia/giaSort.c \ src/aig/gia/giaSpeedup.c \ src/aig/gia/giaSupMin.c \ diff --git a/src/aig/live/liveness.c b/src/aig/live/liveness.c index e0511556..324865a9 100644 --- a/src/aig/live/liveness.c +++ b/src/aig/live/liveness.c @@ -2230,7 +2230,7 @@ Aig_Man_t * LivenessToSafetyTransformationWithLTL( int mode, Abc_Ntk_t * pNtk, A #ifdef ALLOW_SAFETY_PROPERTIES printf("liveness output is conjoined with safety assertions\n"); pObjSafetyAndLiveToSafety = Aig_Or( pNew, pObjSafetyGate, pNegatedSafetyConjunction ); - pObjSafetyPropertyOutput = Vec_PtrEntry( vPoForLtlProps, iii ); + pObjSafetyPropertyOutput = (Aig_Obj_t *)Vec_PtrEntry( vPoForLtlProps, iii ); Aig_ObjPatchFanin0( pNew, pObjSafetyPropertyOutput, pObjSafetyAndLiveToSafety ); #else pObjSafetyPropertyOutput = Vec_PtrEntry( vPoForLtlProps, iii ); diff --git a/src/aig/live/ltl_parser.c b/src/aig/live/ltl_parser.c index 66d7f72d..58125818 100644 --- a/src/aig/live/ltl_parser.c +++ b/src/aig/live/ltl_parser.c @@ -78,6 +78,7 @@ void Abc_FrameCopyLTLDataBase( Abc_Frame_t *pAbc, Abc_Ntk_t * pNtk ) if( pAbc->vLTLProperties_global != NULL ) { // printf("Deleting exisitng LTL database from the frame\n"); + Vec_PtrFree( pAbc->vLTLProperties_global ); pAbc->vLTLProperties_global = NULL; } pAbc->vLTLProperties_global = Vec_PtrAlloc(Vec_PtrSize(pNtk->vLtlProperties)); diff --git a/src/aig/llb/llbCore.c b/src/aig/llb/llbCore.c index 562a9800..cbd527e2 100644 --- a/src/aig/llb/llbCore.c +++ b/src/aig/llb/llbCore.c @@ -48,7 +48,7 @@ void Llb_ManSetDefaultParams( Gia_ParLlb_t * p ) { memset( p, 0, sizeof(Gia_ParLlb_t) ); p->nBddMax = 1000000; - p->nIterMax = 1000; + p->nIterMax = 10000000; p->nClusterMax = 20; p->nHintDepth = 0; p->HintFirst = 0; diff --git a/src/aig/llb/llbReach.c b/src/aig/llb/llbReach.c index 7c12a88c..76ee7147 100644 --- a/src/aig/llb/llbReach.c +++ b/src/aig/llb/llbReach.c @@ -575,7 +575,7 @@ int Llb_ManReachability( Llb_Man_t * p, Vec_Int_t * vHints, DdManager ** pddGlo Cudd_RecursiveDeref( p->dd, bConstrNs ); bConstrNs = NULL; if ( bReached == NULL ) return 0; // reachable - assert( bCurrent == NULL ); +// assert( bCurrent == NULL ); if ( bCurrent ) Cudd_RecursiveDeref( p->dd, bCurrent ); // report the stats diff --git a/src/aig/mfx/mfxInt.h b/src/aig/mfx/mfxInt.h index 1fcf4e91..320e7a8e 100644 --- a/src/aig/mfx/mfxInt.h +++ b/src/aig/mfx/mfxInt.h @@ -60,7 +60,8 @@ struct Mfx_Man_t_ Vec_Ptr_t * vNodes; // the internal nodes of the window Vec_Ptr_t * vDivs; // the divisors of the node Vec_Int_t * vDivLits; // the SAT literals of divisor nodes - Vec_Int_t * vProjVars; // the projection variables + Vec_Int_t * vProjVarsCnf; // the projection variables + Vec_Int_t * vProjVarsSat; // the projection variables // intermediate simulation data Vec_Ptr_t * vDivCexes; // the counter-example for dividors int nDivWords; // the number of words diff --git a/src/aig/mfx/mfxInter.c b/src/aig/mfx/mfxInter.c index 2263398d..db2e5e7e 100644 --- a/src/aig/mfx/mfxInter.c +++ b/src/aig/mfx/mfxInter.c @@ -96,13 +96,13 @@ sat_solver * Mfx_CreateSolverResub( Mfx_Man_t * p, int * pCands, int nCands, int Lits[0] = toLitCond( p->pCnf->pVarNums[pObjPo->Id], fInvert ); // collect the outputs of the divisors - Vec_IntClear( p->vProjVars ); + Vec_IntClear( p->vProjVarsCnf ); Vec_PtrForEachEntryStart( Aig_Obj_t *, p->pAigWin->vPos, pObjPo, i, Aig_ManPoNum(p->pAigWin) - Vec_PtrSize(p->vDivs) ) { assert( p->pCnf->pVarNums[pObjPo->Id] >= 0 ); - Vec_IntPush( p->vProjVars, p->pCnf->pVarNums[pObjPo->Id] ); + Vec_IntPush( p->vProjVarsCnf, p->pCnf->pVarNums[pObjPo->Id] ); } - assert( Vec_IntSize(p->vProjVars) == Vec_PtrSize(p->vDivs) ); + assert( Vec_IntSize(p->vProjVarsCnf) == Vec_PtrSize(p->vDivs) ); // start the solver pSat = sat_solver_new(); @@ -161,7 +161,7 @@ sat_solver * Mfx_CreateSolverResub( Mfx_Man_t * p, int * pCands, int nCands, int // get the variable number of this divisor i = lit_var( pCands[c] ) - 2 * p->pCnf->nVars; // get the corresponding SAT variable - iVar = Vec_IntEntry( p->vProjVars, i ); + iVar = Vec_IntEntry( p->vProjVarsCnf, i ); // add the corresponding EXOR gate if ( !Mfx_SatAddXor( pSat, iVar, iVar + p->pCnf->nVars, 2 * p->pCnf->nVars + i ) ) { @@ -181,15 +181,17 @@ sat_solver * Mfx_CreateSolverResub( Mfx_Man_t * p, int * pCands, int nCands, int else { // add the clauses for the EXOR gates - and remember their outputs - Vec_IntForEachEntry( p->vProjVars, iVar, i ) + Vec_IntClear( p->vProjVarsSat ); + Vec_IntForEachEntry( p->vProjVarsCnf, iVar, i ) { if ( !Mfx_SatAddXor( pSat, iVar, iVar + p->pCnf->nVars, 2 * p->pCnf->nVars + i ) ) { sat_solver_delete( pSat ); return NULL; } - Vec_IntWriteEntry( p->vProjVars, i, 2 * p->pCnf->nVars + i ); + Vec_IntPush( p->vProjVarsSat, 2 * p->pCnf->nVars + i ); } + assert( Vec_IntSize(p->vProjVarsCnf) == Vec_IntSize(p->vProjVarsSat) ); // simplify the solver status = sat_solver_simplify(pSat); if ( status == 0 ) @@ -242,7 +244,7 @@ unsigned * Mfx_InterplateTruth( Mfx_Man_t * p, int * pCands, int nCands, int fIn // get the variable number of this divisor i = lit_var( pCands[c] ) - 2 * p->pCnf->nVars; // get the corresponding SAT variable - pGloVars[c] = Vec_IntEntry( p->vProjVars, i ); + pGloVars[c] = Vec_IntEntry( p->vProjVarsCnf, i ); } // derive the interpolant @@ -342,7 +344,7 @@ Hop_Obj_t * Mfx_Interplate( Mfx_Man_t * p, int * pCands, int nCands ) // get the variable number of this divisor i = lit_var( pCands[c] ) - 2 * p->pCnf->nVars; // get the corresponding SAT variable - pGloVars[c] = Vec_IntEntry( p->vProjVars, i ); + pGloVars[c] = Vec_IntEntry( p->vProjVarsCnf, i ); } // derive the interpolant diff --git a/src/aig/mfx/mfxMan.c b/src/aig/mfx/mfxMan.c index 9d9994bf..ff8b02fd 100644 --- a/src/aig/mfx/mfxMan.c +++ b/src/aig/mfx/mfxMan.c @@ -49,7 +49,8 @@ Mfx_Man_t * Mfx_ManAlloc( Mfx_Par_t * pPars ) p = ABC_ALLOC( Mfx_Man_t, 1 ); memset( p, 0, sizeof(Mfx_Man_t) ); p->pPars = pPars; - p->vProjVars = Vec_IntAlloc( 100 ); + p->vProjVarsCnf = Vec_IntAlloc( 100 ); + p->vProjVarsSat = Vec_IntAlloc( 100 ); p->vDivLits = Vec_IntAlloc( 100 ); p->nDivWords = Aig_BitWordNum(p->pPars->nDivMax + MFX_FANIN_MAX); p->vDivCexes = Vec_PtrAllocSimInfo( p->pPars->nDivMax+MFX_FANIN_MAX+1, p->nDivWords ); @@ -178,7 +179,8 @@ void Mfx_ManStop( Mfx_Man_t * p ) Vec_IntFree( p->vMem ); Vec_VecFree( p->vLevels ); Vec_PtrFree( p->vFanins ); - Vec_IntFree( p->vProjVars ); + Vec_IntFree( p->vProjVarsCnf ); + Vec_IntFree( p->vProjVarsSat ); Vec_IntFree( p->vDivLits ); Vec_PtrFree( p->vDivCexes ); ABC_FREE( p ); diff --git a/src/aig/mfx/mfxResub.c b/src/aig/mfx/mfxResub.c index 83673661..5a4786d6 100644 --- a/src/aig/mfx/mfxResub.c +++ b/src/aig/mfx/mfxResub.c @@ -111,7 +111,7 @@ int Mfx_TryResubOnce( Mfx_Man_t * p, int * pCands, int nCands ) } p->nSatCexes++; // store the counter-example - Vec_IntForEachEntry( p->vProjVars, iVar, i ) + Vec_IntForEachEntry( p->vProjVarsSat, iVar, i ) { pData = (unsigned *)Vec_PtrEntry( p->vDivCexes, i ); if ( !sat_solver_var_value( p->pSat, iVar ) ) // remove 0s!!! @@ -166,7 +166,7 @@ int Mfx_SolveSatResub( Mfx_Man_t * p, Nwk_Obj_t * pNode, int iFanin, int fOnlyRe continue; Vec_PtrPush( p->vFanins, pFanin ); iVar = Vec_PtrSize(p->vDivs) - Nwk_ObjFaninNum(pNode) + i; - pCands[nCands++] = toLitCond( Vec_IntEntry( p->vProjVars, iVar ), 1 ); + pCands[nCands++] = toLitCond( Vec_IntEntry( p->vProjVarsSat, iVar ), 1 ); } RetValue = Mfx_TryResubOnce( p, pCands, nCands ); if ( RetValue == -1 ) @@ -244,7 +244,7 @@ p->timeInt += clock() - clk; if ( iVar == Vec_PtrSize(p->vDivs)-Nwk_ObjFaninNum(pNode) ) return 0; - pCands[nCands] = toLitCond( Vec_IntEntry(p->vProjVars, iVar), 1 ); + pCands[nCands] = toLitCond( Vec_IntEntry(p->vProjVarsSat, iVar), 1 ); RetValue = Mfx_TryResubOnce( p, pCands, nCands+1 ); if ( RetValue == -1 ) return 0; @@ -316,7 +316,7 @@ int Mfx_SolveSatResub2( Mfx_Man_t * p, Nwk_Obj_t * pNode, int iFanin, int iFanin continue; Vec_PtrPush( p->vFanins, pFanin ); iVar = Vec_PtrSize(p->vDivs) - Nwk_ObjFaninNum(pNode) + i; - pCands[nCands++] = toLitCond( Vec_IntEntry( p->vProjVars, iVar ), 1 ); + pCands[nCands++] = toLitCond( Vec_IntEntry( p->vProjVarsSat, iVar ), 1 ); } RetValue = Mfx_TryResubOnce( p, pCands, nCands ); if ( RetValue == -1 ) @@ -390,8 +390,8 @@ p->timeInt += clock() - clk; if ( iVar == Vec_PtrSize(p->vDivs)-Nwk_ObjFaninNum(pNode) ) return 0; - pCands[nCands] = toLitCond( Vec_IntEntry(p->vProjVars, iVar2), 1 ); - pCands[nCands+1] = toLitCond( Vec_IntEntry(p->vProjVars, iVar), 1 ); + pCands[nCands] = toLitCond( Vec_IntEntry(p->vProjVarsSat, iVar2), 1 ); + pCands[nCands+1] = toLitCond( Vec_IntEntry(p->vProjVarsSat, iVar), 1 ); RetValue = Mfx_TryResubOnce( p, pCands, nCands+2 ); if ( RetValue == -1 ) return 0; diff --git a/src/aig/mfx/mfxSat.c b/src/aig/mfx/mfxSat.c index dc4cd862..974563ab 100644 --- a/src/aig/mfx/mfxSat.c +++ b/src/aig/mfx/mfxSat.c @@ -58,7 +58,7 @@ int Mfx_SolveSat_iter( Mfx_Man_t * p ) p->nCares++; // add SAT assignment to the solver Mint = 0; - Vec_IntForEachEntry( p->vProjVars, iVar, b ) + Vec_IntForEachEntry( p->vProjVarsSat, iVar, b ) { Lits[b] = toLit( iVar ); if ( sat_solver_var_value( p->pSat, iVar ) ) @@ -70,7 +70,7 @@ int Mfx_SolveSat_iter( Mfx_Man_t * p ) assert( !Aig_InfoHasBit(p->uCare, Mint) ); Aig_InfoSetBit( p->uCare, Mint ); // add the blocking clause - RetValue = sat_solver_addclause( p->pSat, Lits, Lits + Vec_IntSize(p->vProjVars) ); + RetValue = sat_solver_addclause( p->pSat, Lits, Lits + Vec_IntSize(p->vProjVarsSat) ); if ( RetValue == 0 ) return 0; return 1; @@ -92,15 +92,15 @@ int Mfx_SolveSat( Mfx_Man_t * p, Nwk_Obj_t * pNode ) Aig_Obj_t * pObjPo; int RetValue, i; // collect projection variables - Vec_IntClear( p->vProjVars ); + Vec_IntClear( p->vProjVarsSat ); Vec_PtrForEachEntryStart( Aig_Obj_t *, p->pAigWin->vPos, pObjPo, i, Aig_ManPoNum(p->pAigWin) - Nwk_ObjFaninNum(pNode) ) { assert( p->pCnf->pVarNums[pObjPo->Id] >= 0 ); - Vec_IntPush( p->vProjVars, p->pCnf->pVarNums[pObjPo->Id] ); + Vec_IntPush( p->vProjVarsSat, p->pCnf->pVarNums[pObjPo->Id] ); } // prepare the truth table of care set - p->nFanins = Vec_IntSize( p->vProjVars ); + p->nFanins = Vec_IntSize( p->vProjVarsSat ); p->nWords = Aig_TruthWordNum( p->nFanins ); memset( p->uCare, 0, sizeof(unsigned) * p->nWords ); diff --git a/src/aig/saig/module.make b/src/aig/saig/module.make index 88935121..a1f0e976 100644 --- a/src/aig/saig/module.make +++ b/src/aig/saig/module.make @@ -24,5 +24,6 @@ SRC += src/aig/saig/saigAbs.c \ src/aig/saig/saigStrSim.c \ src/aig/saig/saigSwitch.c \ src/aig/saig/saigSynch.c \ + src/aig/saig/saigTempor.c \ src/aig/saig/saigTrans.c \ src/aig/saig/saigWnd.c diff --git a/src/aig/saig/saig.h b/src/aig/saig/saig.h index fc85d52a..b1017bdb 100644 --- a/src/aig/saig/saig.h +++ b/src/aig/saig/saig.h @@ -146,7 +146,8 @@ extern void Saig_ManDetectConstrFuncTest( Aig_Man_t * p, int nFrame extern Aig_Man_t * Saig_ManDupFoldConstrsFunc( Aig_Man_t * pAig, int fCompl, int fVerbose ); extern Aig_Man_t * Saig_ManDupUnfoldConstrsFunc( Aig_Man_t * pAig, int nFrames, int nConfs, int nProps, int fOldAlgo, int fVerbose ); /*=== saigDup.c ==========================================================*/ -extern Aig_Man_t * Said_ManDupOrpos( Aig_Man_t * p ); +extern Aig_Man_t * Saig_ManDupOrpos( Aig_Man_t * p ); +extern Aig_Man_t * Saig_ManCreateEquivMiter( Aig_Man_t * pAig, Vec_Int_t * vPairs ); extern Aig_Man_t * Saig_ManDeriveAbstraction( Aig_Man_t * pAig, Vec_Int_t * vFlops ); /*=== saigHaig.c ==========================================================*/ extern Aig_Man_t * Saig_ManHaigRecord( Aig_Man_t * p, int nIters, int nSteps, int fRetimingOnly, int fAddBugs, int fUseCnf, int fVerbose ); diff --git a/src/aig/saig/saigBmc2.c b/src/aig/saig/saigBmc2.c index c7129c67..3d57ae6e 100644 --- a/src/aig/saig/saigBmc2.c +++ b/src/aig/saig/saigBmc2.c @@ -820,7 +820,12 @@ int Saig_BmcPerform( Aig_Man_t * pAig, int nStart, int nFramesMax, int nNodesMax { printf( "No output was asserted in %d frames. ", p->iFramePrev-1 ); if ( piFrames ) - *piFrames = p->iFramePrev-1; + { + if ( p->iOutputLast > 0 ) + *piFrames = p->iFramePrev - 1; + else + *piFrames = p->iFramePrev; + } } if ( fVerbOverwrite ) { @@ -834,7 +839,7 @@ int Saig_BmcPerform( Aig_Man_t * pAig, int nStart, int nFramesMax, int nNodesMax { if ( p->iFrameLast >= p->nFramesMax ) printf( "Reached limit on the number of timeframes (%d).\n", p->nFramesMax ); - else if ( p->pSat->stats.conflicts > p->nConfMaxAll ) + else if ( p->nConfMaxAll && p->pSat->stats.conflicts > p->nConfMaxAll ) printf( "Reached global conflict limit (%d).\n", p->nConfMaxAll ); else printf( "Reached local conflict limit (%d).\n", p->nConfMaxOne ); diff --git a/src/aig/saig/saigDup.c b/src/aig/saig/saigDup.c index 268540da..4d34224e 100644 --- a/src/aig/saig/saigDup.c +++ b/src/aig/saig/saigDup.c @@ -42,7 +42,7 @@ ABC_NAMESPACE_IMPL_START SeeAlso [] ***********************************************************************/ -Aig_Man_t * Said_ManDupOrpos( Aig_Man_t * pAig ) +Aig_Man_t * Saig_ManDupOrpos( Aig_Man_t * pAig ) { Aig_Man_t * pAigNew; Aig_Obj_t * pObj, * pMiter; @@ -77,6 +77,56 @@ Aig_Man_t * Said_ManDupOrpos( Aig_Man_t * pAig ) return pAigNew; } +/**Function************************************************************* + + Synopsis [Duplicates while ORing the POs of sequential circuit.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Aig_Man_t * Saig_ManCreateEquivMiter( Aig_Man_t * pAig, Vec_Int_t * vPairs ) +{ + Aig_Man_t * pAigNew; + Aig_Obj_t * pObj, * pObj2, * pMiter; + int i; + if ( pAig->nConstrs > 0 ) + { + printf( "The AIG manager should have no constraints.\n" ); + return NULL; + } + // start the new manager + pAigNew = Aig_ManStart( Aig_ManNodeNum(pAig) ); + pAigNew->pName = Aig_UtilStrsav( pAig->pName ); + pAigNew->nConstrs = pAig->nConstrs; + // map the constant node + Aig_ManConst1(pAig)->pData = Aig_ManConst1( pAigNew ); + // create variables for PIs + Aig_ManForEachPi( pAig, pObj, i ) + pObj->pData = Aig_ObjCreatePi( pAigNew ); + // add internal nodes of this frame + Aig_ManForEachNode( pAig, pObj, i ) + pObj->pData = Aig_And( pAigNew, Aig_ObjChild0Copy(pObj), Aig_ObjChild1Copy(pObj) ); + // create POs + assert( Vec_IntSize(vPairs) % 2 == 0 ); + Aig_ManForEachNodeVec( pAig, vPairs, pObj, i ) + { + pObj2 = Aig_ManObj( pAig, Vec_IntEntry(vPairs, ++i) ); + pMiter = Aig_Exor( pAigNew, pObj->pData, pObj2->pData ); + pMiter = Aig_NotCond( pMiter, pObj->fPhase ^ pObj2->fPhase ); + Aig_ObjCreatePo( pAigNew, pMiter ); + } + // transfer to register outputs + Saig_ManForEachLi( pAig, pObj, i ) + Aig_ObjCreatePo( pAigNew, Aig_ObjChild0Copy(pObj) ); + Aig_ManCleanup( pAigNew ); + Aig_ManSetRegNum( pAigNew, Aig_ManRegNum(pAig) ); + return pAigNew; +} + /**Function************************************************************* Synopsis [Duplicates the AIG manager recursively.] diff --git a/src/aig/saig/saigPhase.c b/src/aig/saig/saigPhase.c index 340910d0..4a23ecf3 100644 --- a/src/aig/saig/saigPhase.c +++ b/src/aig/saig/saigPhase.c @@ -255,15 +255,22 @@ int Saig_TsiCountNonXValuedRegisters( Saig_Tsim_t * p, int nWords, int nPref ) SeeAlso [] ***********************************************************************/ -void Saig_TsiPrintTraces( Saig_Tsim_t * p, int nWords, int nPrefix ) +void Saig_TsiPrintTraces( Saig_Tsim_t * p, int nWords, int nPrefix, int nLoop ) { unsigned * pState; int nRegs = p->pAig->nRegs; int Value, i, k, Counter = 0; - if ( Vec_PtrSize(p->vStates) > 80 ) - return; + printf( "Ternary traces for each flop:\n" ); + printf( " : " ); + for ( i = 0; i < Vec_PtrSize(p->vStates) - nLoop - 1; i++ ) + printf( "%d", i%10 ); + printf( " " ); + for ( i = 0; i < nLoop; i++ ) + printf( "%d", i%10 ); + printf( "\n" ); for ( i = 0; i < nRegs; i++ ) { +/* Vec_PtrForEachEntry( unsigned *, p->vStates, pState, k ) { Value = (Aig_InfoHasBit( pState, 2 * i + 1 ) << 1) | Aig_InfoHasBit( pState, 2 * i ); @@ -274,8 +281,11 @@ void Saig_TsiPrintTraces( Saig_Tsim_t * p, int nWords, int nPrefix ) Counter++; else continue; +*/ + // print trace - printf( "%5d : %5d %5d ", Counter, i, Saig_ManLo(p->pAig, i)->Id ); +// printf( "%5d : %5d %5d ", Counter, i, Saig_ManLo(p->pAig, i)->Id ); + printf( "%5d : ", Counter++ ); Vec_PtrForEachEntryStop( unsigned *, p->vStates, pState, k, Vec_PtrSize(p->vStates)-1 ) { Value = (Aig_InfoHasBit( pState, 2 * i + 1 ) << 1) | Aig_InfoHasBit( pState, 2 * i ); @@ -488,7 +498,7 @@ Saig_Tsim_t * Saig_ManReachableTernary( Aig_Man_t * p, Vec_Int_t * vInits, int f Saig_ManForEachLo( p, pObj, i ) Saig_ObjSetXsim( pObj, Saig_XsimConvertValue(Vec_IntEntry(vInits, i)) ); } - else + else { Saig_ManForEachLo( p, pObj, i ) Saig_ObjSetXsim( pObj, SAIG_XVS0 ); @@ -800,6 +810,42 @@ int Saig_ManPhaseFrameNum( Aig_Man_t * p, Vec_Int_t * vInits ) return nFrames; } +/**Function************************************************************* + + Synopsis [Performs automated phase abstraction.] + + Description [Takes the AIG manager and the array of initial states.] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Saig_ManPhasePrefixLength( Aig_Man_t * p, int fVerbose, int fVeryVerbose ) +{ + Saig_Tsim_t * pTsi; + int nFrames, nPrefix, nNonXRegs; + assert( Saig_ManRegNum(p) ); + assert( Saig_ManPiNum(p) ); + assert( Saig_ManPoNum(p) ); + // perform terminary simulation + pTsi = Saig_ManReachableTernary( p, NULL, 0 ); + if ( pTsi == NULL ) + return 0; + // derive information + nPrefix = Saig_TsiComputePrefix( pTsi, (unsigned *)Vec_PtrEntryLast(pTsi->vStates), pTsi->nWords ); + nFrames = Vec_PtrSize(pTsi->vStates) - 1 - nPrefix; + nNonXRegs = Saig_TsiCountNonXValuedRegisters( pTsi, pTsi->nWords, nPrefix ); + // print statistics + if ( fVerbose ) + printf( "Lead = %5d. Loop = %5d. Total flops = %5d. Binary flops = %5d.\n", nPrefix, nFrames, p->nRegs, nNonXRegs ); + if ( fVeryVerbose ) + Saig_TsiPrintTraces( pTsi, pTsi->nWords, nPrefix, nFrames ); + Saig_TsiStop( pTsi ); + // potentially, may need to reduce nFrames if nPrefix is less than nFrames + return nPrefix; +} + /**Function************************************************************* Synopsis [Performs automated phase abstraction.] @@ -829,10 +875,10 @@ Aig_Man_t * Saig_ManPhaseAbstract( Aig_Man_t * p, Vec_Int_t * vInits, int nFrame // print statistics if ( fVerbose ) { - printf( "Prefix = %5d. Cycle = %5d. Total = %5d. Non-ternary = %5d.\n", + printf( "Lead = %5d. Loop = %5d. Total flops = %5d. Binary flops = %5d.\n", pTsi->nPrefix, pTsi->nCycle, p->nRegs, pTsi->nNonXRegs ); - if ( pTsi->nNonXRegs < 100 ) - Saig_TsiPrintTraces( pTsi, pTsi->nWords, pTsi->nPrefix ); + if ( pTsi->nNonXRegs < 100 && Vec_PtrSize(pTsi->vStates) < 80 ) + Saig_TsiPrintTraces( pTsi, pTsi->nWords, pTsi->nPrefix, pTsi->nCycle ); } if ( fPrint ) printf( "Print-out finished. Phase assignment is not performed.\n" ); @@ -885,10 +931,10 @@ Aig_Man_t * Saig_ManPhaseAbstractAuto( Aig_Man_t * p, int fVerbose ) // print statistics if ( fVerbose ) { - printf( "Prefix = %5d. Cycle = %5d. Total = %5d. Non-ternary = %5d.\n", + printf( "Lead = %5d. Loop = %5d. Total flops = %5d. Binary flops = %5d.\n", pTsi->nPrefix, pTsi->nCycle, p->nRegs, pTsi->nNonXRegs ); - if ( pTsi->nNonXRegs < 100 ) - Saig_TsiPrintTraces( pTsi, pTsi->nWords, pTsi->nPrefix ); + if ( pTsi->nNonXRegs < 100 && Vec_PtrSize(pTsi->vStates) < 80 ) + Saig_TsiPrintTraces( pTsi, pTsi->nWords, pTsi->nPrefix, pTsi->nCycle ); } nFrames = pTsi->nCycle; if ( fPrint ) diff --git a/src/aig/ssw/ssw.h b/src/aig/ssw/ssw.h index 207ebea9..bf8c918e 100644 --- a/src/aig/ssw/ssw.h +++ b/src/aig/ssw/ssw.h @@ -68,6 +68,7 @@ struct Ssw_Pars_t_ int fUseCSat; // new SAT solver using when fScorrGia is selected int fVerbose; // verbose stats int fFlopVerbose; // verbose printout of redundant flops + int fEquivDump; // enables dumping equivalences // optimized latch correspondence int fLatchCorrOpt; // perform register correspondence (optimized) int nSatVarMax; // max number of SAT vars before recycling SAT solver (optimized latch corr only) diff --git a/src/aig/ssw/sswConstr.c b/src/aig/ssw/sswConstr.c index e233f133..6afdd270 100644 --- a/src/aig/ssw/sswConstr.c +++ b/src/aig/ssw/sswConstr.c @@ -83,8 +83,8 @@ Aig_Man_t * Ssw_FramesWithConstraints( Aig_Man_t * p, int nFrames ) } // remove dangling nodes Aig_ManCleanup( pFrames ); - return pFrames; -} + return pFrames; +} /**Function************************************************************* diff --git a/src/aig/ssw/sswCore.c b/src/aig/ssw/sswCore.c index c277d76e..1419b889 100644 --- a/src/aig/ssw/sswCore.c +++ b/src/aig/ssw/sswCore.c @@ -64,6 +64,8 @@ void Ssw_ManSetDefaultParams( Ssw_Pars_t * p ) p->fDynamic = 0; // dynamic partitioning p->fLocalSim = 0; // local simulation p->fVerbose = 0; // verbose stats + p->fEquivDump = 0; // enables dumping equivalences + // latch correspondence p->fLatchCorrOpt = 0; // performs optimized register correspondence p->nSatVarMax = 1000; // the max number of SAT variables diff --git a/src/aig/ssw/sswDyn.c b/src/aig/ssw/sswDyn.c index 7e8edc66..7bdb2652 100644 --- a/src/aig/ssw/sswDyn.c +++ b/src/aig/ssw/sswDyn.c @@ -409,12 +409,12 @@ p->timeReduce += clock() - clk; if ( p->pPars->fVerbose ) Bar_ProgressUpdate( pProgress, i, NULL ); if ( Saig_ObjIsLo(p->pAig, pObj) ) - p->fRefined |= Ssw_ManSweepNode( p, pObj, f, 0 ); + p->fRefined |= Ssw_ManSweepNode( p, pObj, f, 0, NULL ); else if ( Aig_ObjIsNode(pObj) ) { pObjNew = Aig_And( p->pFrames, Ssw_ObjChild0Fra(p, pObj, f), Ssw_ObjChild1Fra(p, pObj, f) ); Ssw_ObjSetFrame( p, pObj, f, pObjNew ); - p->fRefined |= Ssw_ManSweepNode( p, pObj, f, 0 ); + p->fRefined |= Ssw_ManSweepNode( p, pObj, f, 0, NULL ); } // check if it is time to recycle the solver if ( p->pMSat->pSat == NULL || diff --git a/src/aig/ssw/sswInt.h b/src/aig/ssw/sswInt.h index e3a9a341..ad868c6e 100644 --- a/src/aig/ssw/sswInt.h +++ b/src/aig/ssw/sswInt.h @@ -277,7 +277,7 @@ extern void Ssw_ManResimulateWord( Ssw_Man_t * p, Aig_Obj_t * pCand, Ai /*=== sswSweep.c ===================================================*/ extern int Ssw_ManGetSatVarValue( Ssw_Man_t * p, Aig_Obj_t * pObj, int f ); extern void Ssw_SmlSavePatternAig( Ssw_Man_t * p, int f ); -extern int Ssw_ManSweepNode( Ssw_Man_t * p, Aig_Obj_t * pObj, int f, int fBmc ); +extern int Ssw_ManSweepNode( Ssw_Man_t * p, Aig_Obj_t * pObj, int f, int fBmc, Vec_Int_t * vPairs ); extern int Ssw_ManSweepBmc( Ssw_Man_t * p ); extern int Ssw_ManSweep( Ssw_Man_t * p ); /*=== sswUnique.c ===================================================*/ diff --git a/src/aig/ssw/sswSemi.c b/src/aig/ssw/sswSemi.c index dfb2fb0f..2a28a29b 100644 --- a/src/aig/ssw/sswSemi.c +++ b/src/aig/ssw/sswSemi.c @@ -204,7 +204,7 @@ clk = clock(); { pObjNew = Aig_And( p->pFrames, Ssw_ObjChild0Fra(p, pObj, f), Ssw_ObjChild1Fra(p, pObj, f) ); Ssw_ObjSetFrame( p, pObj, f, pObjNew ); - if ( Ssw_ManSweepNode( p, pObj, f, 1 ) ) + if ( Ssw_ManSweepNode( p, pObj, f, 1, NULL ) ) { Ssw_ManFilterBmcSavePattern( pBmc ); if ( fFirst == 0 ) diff --git a/src/aig/ssw/sswSim.c b/src/aig/ssw/sswSim.c index 37bf5717..404302f2 100644 --- a/src/aig/ssw/sswSim.c +++ b/src/aig/ssw/sswSim.c @@ -302,6 +302,23 @@ int Ssw_SmlNodeIsZero( Ssw_Sml_t * p, Aig_Obj_t * pObj ) return 1; } +/**Function************************************************************* + + Synopsis [Returns 1 if simulation info is composed of all zeros.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Ssw_SmlNodeIsZeroFrame( Ssw_Sml_t * p, Aig_Obj_t * pObj, int f ) +{ + unsigned * pSims = Ssw_ObjSim(p, pObj->Id); + return pSims[f] == 0; +} + /**Function************************************************************* Synopsis [Counts the number of one's in the patten the object.] @@ -1308,7 +1325,7 @@ int Ssw_SmlRunCounterExample( Aig_Man_t * pAig, Abc_Cex_t * p ) // run random simulation Ssw_SmlSimulateOne( pSml ); // check if the given output has failed - RetValue = !Ssw_SmlNodeIsZero( pSml, Aig_ManPo(pAig, p->iPo) ); + RetValue = !Ssw_SmlNodeIsZeroFrame( pSml, Aig_ManPo(pAig, p->iPo), p->iFrame ); Ssw_SmlStop( pSml ); return RetValue; } @@ -1347,7 +1364,7 @@ int Ssw_SmlFindOutputCounterExample( Aig_Man_t * pAig, Abc_Cex_t * p ) // check if the given output has failed iOut = -1; Saig_ManForEachPo( pAig, pObj, k ) - if ( !Ssw_SmlNodeIsZero( pSml, Aig_ManPo(pAig, k) ) ) + if ( !Ssw_SmlNodeIsZeroFrame( pSml, Aig_ManPo(pAig, k), p->iFrame ) ) { iOut = k; break; @@ -1541,81 +1558,6 @@ Abc_Cex_t * Ssw_SmlDupCounterExample( Abc_Cex_t * p, int nRegsNew ) return pCex; } -/**Function************************************************************* - - Synopsis [Resimulates the counter-example.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -int Ssw_SmlWriteCounterExample( FILE * pFile, Aig_Man_t * pAig, Abc_Cex_t * p ) -{ - Ssw_Sml_t * pSml; - Aig_Obj_t * pObj; - int RetValue, i, k, iBit; - unsigned * pSims; - assert( Aig_ManRegNum(pAig) > 0 ); - assert( Aig_ManRegNum(pAig) < Aig_ManPiNum(pAig) ); - // start a new sequential simulator - pSml = Ssw_SmlStart( pAig, 0, p->iFrame+1, 1 ); - // assign simulation info for the registers - iBit = 0; - Saig_ManForEachLo( pAig, pObj, i ) -// Ssw_SmlObjAssignConst( pSml, pObj, Aig_InfoHasBit(p->pData, iBit++), 0 ); - Ssw_SmlObjAssignConst( pSml, pObj, 0, 0 ); - // assign simulation info for the primary inputs - iBit = p->nRegs; - for ( i = 0; i <= p->iFrame; i++ ) - Saig_ManForEachPi( pAig, pObj, k ) - Ssw_SmlObjAssignConst( pSml, pObj, Aig_InfoHasBit(p->pData, iBit++), i ); - assert( iBit == p->nBits ); - // run random simulation - Ssw_SmlSimulateOne( pSml ); - // check if the given output has failed - RetValue = !Ssw_SmlNodeIsZero( pSml, Aig_ManPo(pAig, p->iPo) ); - - // write the output file - for ( i = 0; i <= p->iFrame; i++ ) - { -/* - Saig_ManForEachLo( pAig, pObj, k ) - { - pSims = Ssw_ObjSim(pSml, pObj->Id); - fprintf( pFile, "%d", (int)(pSims[i] != 0) ); - } - fprintf( pFile, " " ); -*/ - Saig_ManForEachPi( pAig, pObj, k ) - { - pSims = Ssw_ObjSim(pSml, pObj->Id); - fprintf( pFile, "%d", (int)(pSims[i] != 0) ); - } -/* - fprintf( pFile, " " ); - Saig_ManForEachPo( pAig, pObj, k ) - { - pSims = Ssw_ObjSim(pSml, pObj->Id); - fprintf( pFile, "%d", (int)(pSims[i] != 0) ); - } - fprintf( pFile, " " ); - Saig_ManForEachLi( pAig, pObj, k ) - { - pSims = Ssw_ObjSim(pSml, pObj->Id); - fprintf( pFile, "%d", (int)(pSims[i] != 0) ); - } -*/ - fprintf( pFile, "\n" ); - } - - Ssw_SmlStop( pSml ); - return RetValue; -} - - //////////////////////////////////////////////////////////////////////// /// END OF FILE /// diff --git a/src/aig/ssw/sswSweep.c b/src/aig/ssw/sswSweep.c index 39fcd48e..40121e42 100644 --- a/src/aig/ssw/sswSweep.c +++ b/src/aig/ssw/sswSweep.c @@ -184,7 +184,7 @@ void Ssw_SmlAddPatternDyn( Ssw_Man_t * p ) SeeAlso [] ***********************************************************************/ -int Ssw_ManSweepNode( Ssw_Man_t * p, Aig_Obj_t * pObj, int f, int fBmc ) +int Ssw_ManSweepNode( Ssw_Man_t * p, Aig_Obj_t * pObj, int f, int fBmc, Vec_Int_t * vPairs ) { Aig_Obj_t * pObjRepr, * pObjFraig, * pObjFraig2, * pObjReprFraig; int RetValue, clk; @@ -221,6 +221,11 @@ p->timeMarkCones += clock() - clk; Ssw_ObjSetFrame( p, pObj, f, pObjFraig2 ); return 0; } + if ( vPairs ) + { + Vec_IntPush( vPairs, pObjRepr->Id ); + Vec_IntPush( vPairs, pObj->Id ); + } if ( RetValue == -1 ) // timed out { Ssw_ClassesRemoveNode( p->ppClasses, pObj ); @@ -287,7 +292,7 @@ clk = clock(); Bar_ProgressUpdate( pProgress, Aig_ManObjNumMax(p->pAig) * f + i, NULL ); pObjNew = Aig_And( p->pFrames, Ssw_ObjChild0Fra(p, pObj, f), Ssw_ObjChild1Fra(p, pObj, f) ); Ssw_ObjSetFrame( p, pObj, f, pObjNew ); - p->fRefined |= Ssw_ManSweepNode( p, pObj, f, 1 ); + p->fRefined |= Ssw_ManSweepNode( p, pObj, f, 1, NULL ); } // quit if this is the last timeframe if ( f == p->pPars->nFramesK - 1 ) @@ -312,6 +317,39 @@ p->timeBmc += clock() - clk; return p->fRefined; } + +/**Function************************************************************* + + Synopsis [Generates AIG with the following nodes put into seq miters.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Ssw_ManDumpEquivMiter( Aig_Man_t * p, Vec_Int_t * vPairs, int Num ) +{ + extern void Ioa_WriteAiger( Aig_Man_t * pMan, char * pFileName, int fWriteSymbols, int fCompact ); + FILE * pFile; + char pBuffer[16]; + Aig_Man_t * pNew; + sprintf( pBuffer, "equiv%03d.aig", Num ); + pFile = fopen( pBuffer, "w" ); + if ( pFile == NULL ) + { + printf( "Cannot open file %s for writing.\n", pBuffer ); + return; + } + fclose( pFile ); + pNew = Saig_ManCreateEquivMiter( p, vPairs ); + Ioa_WriteAiger( pNew, pBuffer, 0, 0 ); + Aig_ManStop( pNew ); + printf( "AIG with %4d disproved equivs is dumped into file \"%s\".\n", Vec_IntSize(vPairs)/2, pBuffer ); +} + + /**Function************************************************************* Synopsis [Performs fraiging for the internal nodes.] @@ -325,9 +363,11 @@ p->timeBmc += clock() - clk; ***********************************************************************/ int Ssw_ManSweep( Ssw_Man_t * p ) { + static int Counter; Bar_Progress_t * pProgress = NULL; Aig_Obj_t * pObj, * pObj2, * pObjNew; int nConstrPairs, clk, i, f; + Vec_Int_t * vDisproved; // perform speculative reduction clk = clock(); @@ -362,17 +402,18 @@ p->timeReduce += clock() - clk; Ssw_ClassesClearRefined( p->ppClasses ); if ( p->pPars->fVerbose ) pProgress = Bar_ProgressStart( stdout, Aig_ManObjNumMax(p->pAig) ); + vDisproved = p->pPars->fEquivDump? Vec_IntAlloc(1000) : NULL; Aig_ManForEachObj( p->pAig, pObj, i ) { if ( p->pPars->fVerbose ) Bar_ProgressUpdate( pProgress, i, NULL ); if ( Saig_ObjIsLo(p->pAig, pObj) ) - p->fRefined |= Ssw_ManSweepNode( p, pObj, f, 0 ); + p->fRefined |= Ssw_ManSweepNode( p, pObj, f, 0, vDisproved ); else if ( Aig_ObjIsNode(pObj) ) { pObjNew = Aig_And( p->pFrames, Ssw_ObjChild0Fra(p, pObj, f), Ssw_ObjChild1Fra(p, pObj, f) ); Ssw_ObjSetFrame( p, pObj, f, pObjNew ); - p->fRefined |= Ssw_ManSweepNode( p, pObj, f, 0 ); + p->fRefined |= Ssw_ManSweepNode( p, pObj, f, 0, vDisproved ); } } if ( p->pPars->fVerbose ) @@ -380,6 +421,9 @@ p->timeReduce += clock() - clk; // cleanup // Ssw_ClassesCheck( p->ppClasses ); + if ( p->pPars->fEquivDump ) + Ssw_ManDumpEquivMiter( p->pAig, vDisproved, Counter++ ); + Vec_IntFreeP( &vDisproved ); return p->fRefined; } diff --git a/src/base/abci/abc.c b/src/base/abci/abc.c index fca9f68c..2973eb6e 100644 --- a/src/base/abci/abc.c +++ b/src/base/abci/abc.c @@ -5,7 +5,7 @@ SystemName [ABC: Logic synthesis and verification system.] PackageName [Network and node package.] - + Synopsis [Command file.] Author [Alan Mishchenko] @@ -46,6 +46,7 @@ #include "cnf.h" #include "cec.h" #include "giaAbs.h" +#include "pdr.h" #include "tim.h" #include "llb.h" @@ -56,7 +57,6 @@ #include "cmd.h" #include "extra.h" -//#include "magic.h" #ifdef _WIN32 //#include @@ -130,6 +130,7 @@ static int Abc_CommandOrPos ( Abc_Frame_t * pAbc, int argc, cha static int Abc_CommandAndPos ( Abc_Frame_t * pAbc, int argc, char ** argv ); static int Abc_CommandZeroPo ( Abc_Frame_t * pAbc, int argc, char ** argv ); static int Abc_CommandSwapPos ( Abc_Frame_t * pAbc, int argc, char ** argv ); +static int Abc_CommandAddPi ( Abc_Frame_t * pAbc, int argc, char ** argv ); static int Abc_CommandAppend ( Abc_Frame_t * pAbc, int argc, char ** argv ); static int Abc_CommandFrames ( Abc_Frame_t * pAbc, int argc, char ** argv ); static int Abc_CommandDFrames ( Abc_Frame_t * pAbc, int argc, char ** argv ); @@ -266,6 +267,7 @@ static int Abc_CommandBmc3 ( Abc_Frame_t * pAbc, int argc, cha static int Abc_CommandBmcInter ( Abc_Frame_t * pAbc, int argc, char ** argv ); static int Abc_CommandIndcut ( Abc_Frame_t * pAbc, int argc, char ** argv ); static int Abc_CommandEnlarge ( Abc_Frame_t * pAbc, int argc, char ** argv ); +static int Abc_CommandTempor ( Abc_Frame_t * pAbc, int argc, char ** argv ); static int Abc_CommandInduction ( Abc_Frame_t * pAbc, int argc, char ** argv ); static int Abc_CommandCegar ( Abc_Frame_t * pAbc, int argc, char ** argv ); static int Abc_CommandConstr ( Abc_Frame_t * pAbc, int argc, char ** argv ); @@ -530,6 +532,7 @@ void Abc_Init( Abc_Frame_t * pAbc ) Cmd_CommandAdd( pAbc, "Various", "andpos", Abc_CommandAndPos, 1 ); Cmd_CommandAdd( pAbc, "Various", "zeropo", Abc_CommandZeroPo, 1 ); Cmd_CommandAdd( pAbc, "Various", "swappos", Abc_CommandSwapPos, 1 ); + Cmd_CommandAdd( pAbc, "Various", "addpi", Abc_CommandAddPi, 1 ); Cmd_CommandAdd( pAbc, "Various", "append", Abc_CommandAppend, 1 ); Cmd_CommandAdd( pAbc, "Various", "frames", Abc_CommandFrames, 1 ); Cmd_CommandAdd( pAbc, "Various", "dframes", Abc_CommandDFrames, 1 ); @@ -665,6 +668,7 @@ void Abc_Init( Abc_Frame_t * pAbc ) Cmd_CommandAdd( pAbc, "Verification", "int", Abc_CommandBmcInter, 1 ); Cmd_CommandAdd( pAbc, "Verification", "indcut", Abc_CommandIndcut, 0 ); Cmd_CommandAdd( pAbc, "Verification", "enlarge", Abc_CommandEnlarge, 1 ); + Cmd_CommandAdd( pAbc, "Verification", "tempor", Abc_CommandTempor, 1 ); Cmd_CommandAdd( pAbc, "Verification", "ind", Abc_CommandInduction, 0 ); Cmd_CommandAdd( pAbc, "Verification", "abs", Abc_CommandCegar, 1 ); Cmd_CommandAdd( pAbc, "Verification", "constr", Abc_CommandConstr, 0 ); @@ -1746,12 +1750,12 @@ int Abc_CommandPrintAuto( Abc_Frame_t * pAbc, int argc, char ** argv ) return 0; usage: - Abc_Print( -2, "usage: print_auto [-O num] [-nvh]\n" ); - Abc_Print( -2, "\t computes autosymmetries of the PO functions\n" ); - Abc_Print( -2, "\t-O num : (optional) the 0-based number of the output [default = all]\n"); - Abc_Print( -2, "\t-n : enable naive BDD-based computation [default = %s].\n", fNaive? "yes": "no" ); - Abc_Print( -2, "\t-v : enable verbose output [default = %s].\n", fVerbose? "yes": "no" ); - Abc_Print( -2, "\t-h : print the command usage\n"); + Abc_Print( -2, "usage: print_auto [-O ] [-nvh]\n" ); + Abc_Print( -2, "\t computes autosymmetries of the PO functions\n" ); + Abc_Print( -2, "\t-O : (optional) the 0-based number of the output [default = all]\n"); + Abc_Print( -2, "\t-n : enable naive BDD-based computation [default = %s].\n", fNaive? "yes": "no" ); + Abc_Print( -2, "\t-v : enable verbose output [default = %s].\n", fVerbose? "yes": "no" ); + Abc_Print( -2, "\t-h : print the command usage\n"); return 1; } @@ -1835,7 +1839,7 @@ usage: Abc_Print( -2, "\t shows the truth table of the node\n" ); Abc_Print( -2, "\t-n : toggles real/dummy fanin names [default = %s]\n", fUseRealNames? "real": "dummy" ); Abc_Print( -2, "\t-h : print the command usage\n"); - Abc_Print( -2, "\tnode : the node to consider (default = the driver of the first PO)\n"); + Abc_Print( -2, "\t: the node to consider (default = the driver of the first PO)\n"); return 1; } @@ -2099,12 +2103,12 @@ int Abc_CommandPrintDsd( Abc_Frame_t * pAbc, int argc, char ** argv ) return 0; usage: - Abc_Print( -2, "usage: print_dsd [-pch] [-N num]\n" ); - Abc_Print( -2, "\t print DSD formula for a single-output function with less than 16 variables\n" ); - Abc_Print( -2, "\t-p : toggle printing profile [default = %s]\n", fProfile? "yes": "no" ); - Abc_Print( -2, "\t-c : toggle recursive cofactoring [default = %s]\n", fCofactor? "yes": "no" ); - Abc_Print( -2, "\t-N num : the number of levels to cofactor [default = %d]\n", nCofLevel ); - Abc_Print( -2, "\t-h : print the command usage\n"); + Abc_Print( -2, "usage: print_dsd [-pch] [-N ]\n" ); + Abc_Print( -2, "\t print DSD formula for a single-output function with less than 16 variables\n" ); + Abc_Print( -2, "\t-p : toggle printing profile [default = %s]\n", fProfile? "yes": "no" ); + Abc_Print( -2, "\t-c : toggle recursive cofactoring [default = %s]\n", fCofactor? "yes": "no" ); + Abc_Print( -2, "\t-N : the number of levels to cofactor [default = %d]\n", nCofLevel ); + Abc_Print( -2, "\t-h : print the command usage\n"); return 1; } @@ -2414,7 +2418,7 @@ usage: Abc_Print( -2, " \"dot.exe\" and \"gsview32.exe\" should be set in the paths\n" ); Abc_Print( -2, " (\"gsview32.exe\" may be in \"C:\\Program Files\\Ghostgum\\gsview\\\")\n" ); #endif - Abc_Print( -2, "\tnode : the node to consider [default = the driver of the first PO]\n"); + Abc_Print( -2, "\t: the node to consider [default = the driver of the first PO]\n"); Abc_Print( -2, "\t-h : print the command usage\n"); return 1; } @@ -2503,16 +2507,16 @@ int Abc_CommandShowCut( Abc_Frame_t * pAbc, int argc, char ** argv ) return 0; usage: - Abc_Print( -2, "usage: show_cut [-N num] [-C num] [-h] \n" ); - Abc_Print( -2, " visualizes the cut of a node using DOT and GSVIEW\n" ); + Abc_Print( -2, "usage: show_cut [-N ] [-C ] [-h] \n" ); + Abc_Print( -2, " visualizes the cut of a node using DOT and GSVIEW\n" ); #ifdef WIN32 - Abc_Print( -2, " \"dot.exe\" and \"gsview32.exe\" should be set in the paths\n" ); - Abc_Print( -2, " (\"gsview32.exe\" may be in \"C:\\Program Files\\Ghostgum\\gsview\\\")\n" ); + Abc_Print( -2, " \"dot.exe\" and \"gsview32.exe\" should be set in the paths\n" ); + Abc_Print( -2, " (\"gsview32.exe\" may be in \"C:\\Program Files\\Ghostgum\\gsview\\\")\n" ); #endif - Abc_Print( -2, "\t-N num : the max size of the cut to be computed [default = %d]\n", nNodeSizeMax ); - Abc_Print( -2, "\t-C num : the max support of the containing cone [default = %d]\n", nConeSizeMax ); - Abc_Print( -2, "\tnode : the node to consider\n"); - Abc_Print( -2, "\t-h : print the command usage\n"); + Abc_Print( -2, "\t-N : the max size of the cut to be computed [default = %d]\n", nNodeSizeMax ); + Abc_Print( -2, "\t-C : the max support of the containing cone [default = %d]\n", nConeSizeMax ); + Abc_Print( -2, "\t : the node to consider\n"); + Abc_Print( -2, "\t-h : print the command usage\n"); return 1; } @@ -2606,9 +2610,9 @@ int Abc_CommandCollapse( Abc_Frame_t * pAbc, int argc, char ** argv ) return 0; usage: - Abc_Print( -2, "usage: collapse [-B num] [-rdvh]\n" ); + Abc_Print( -2, "usage: collapse [-B ] [-rdvh]\n" ); Abc_Print( -2, "\t collapses the network by constructing global BDDs\n" ); - Abc_Print( -2, "\t-B num : limit on live BDD nodes during collapsing [default = %d]\n", fBddSizeMax ); + Abc_Print( -2, "\t-B : limit on live BDD nodes during collapsing [default = %d]\n", fBddSizeMax ); Abc_Print( -2, "\t-r : toggles dynamic variable reordering [default = %s]\n", fReorder? "yes": "no" ); Abc_Print( -2, "\t-d : toggles dual-rail collapsing mode [default = %s]\n", fDualRail? "yes": "no" ); Abc_Print( -2, "\t-v : print verbose information [default = %s]\n", fVerbose? "yes": "no" ); @@ -2971,10 +2975,10 @@ int Abc_CommandMulti( Abc_Frame_t * pAbc, int argc, char ** argv ) return 0; usage: - Abc_Print( -2, "usage: multi [-T num] [-F num] [-msfch]\n" ); + Abc_Print( -2, "usage: multi [-TF ] [-msfch]\n" ); Abc_Print( -2, "\t transforms an AIG into a logic network by creating larger nodes\n" ); - Abc_Print( -2, "\t-F num : the maximum fanin size after renoding [default = %d]\n", nFaninMax ); - Abc_Print( -2, "\t-T num : the threshold for AIG node duplication [default = %d]\n", nThresh ); + Abc_Print( -2, "\t-F : the maximum fanin size after renoding [default = %d]\n", nFaninMax ); + Abc_Print( -2, "\t-T : the threshold for AIG node duplication [default = %d]\n", nThresh ); Abc_Print( -2, "\t (an AIG node is the root of a new node after renoding\n" ); Abc_Print( -2, "\t if this leads to duplication of no more than %d AIG nodes,\n", nThresh ); Abc_Print( -2, "\t that is, if [(numFanouts(Node)-1) * size(MFFC(Node))] <= %d)\n", nThresh ); @@ -3138,13 +3142,13 @@ int Abc_CommandRenode( Abc_Frame_t * pAbc, int argc, char ** argv ) return 0; usage: - Abc_Print( -2, "usage: renode [-K num] [-C num] [-F num] [-A num] [-sbciav]\n" ); + Abc_Print( -2, "usage: renode [-KCFA ] [-sbciav]\n" ); Abc_Print( -2, "\t transforms the AIG into a logic network with larger nodes\n" ); Abc_Print( -2, "\t while minimizing the number of FF literals of the node SOPs\n" ); - Abc_Print( -2, "\t-K num : the max cut size for renoding (2 < num < %d) [default = %d]\n", IF_MAX_FUNC_LUTSIZE+1, nLutSize ); - Abc_Print( -2, "\t-C num : the max number of cuts used at a node (0 < num < 2^12) [default = %d]\n", nCutsMax ); - Abc_Print( -2, "\t-F num : the number of area flow recovery iterations (num >= 0) [default = %d]\n", nFlowIters ); - Abc_Print( -2, "\t-A num : the number of exact area recovery iterations (num >= 0) [default = %d]\n", nAreaIters ); + Abc_Print( -2, "\t-K : the max cut size for renoding (2 < num < %d) [default = %d]\n", IF_MAX_FUNC_LUTSIZE+1, nLutSize ); + Abc_Print( -2, "\t-C : the max number of cuts used at a node (0 < num < 2^12) [default = %d]\n", nCutsMax ); + Abc_Print( -2, "\t-F : the number of area flow recovery iterations (num >= 0) [default = %d]\n", nFlowIters ); + Abc_Print( -2, "\t-A : the number of exact area recovery iterations (num >= 0) [default = %d]\n", nAreaIters ); Abc_Print( -2, "\t-s : toggles minimizing SOP cubes instead of FF lits [default = %s]\n", fUseSops? "yes": "no" ); Abc_Print( -2, "\t-b : toggles minimizing BDD nodes instead of FF lits [default = %s]\n", fUseBdds? "yes": "no" ); Abc_Print( -2, "\t-c : toggles minimizing CNF clauses instead of FF lits [default = %s]\n", fUseCnfs? "yes": "no" ); @@ -3414,17 +3418,17 @@ int Abc_CommandFastExtract( Abc_Frame_t * pAbc, int argc, char ** argv ) return 0; usage: - Abc_Print( -2, "usage: fx [-SDN num] [-sdzcvh]\n"); - Abc_Print( -2, "\t performs unate fast extract on the current network\n"); - Abc_Print( -2, "\t-S num : max number of single-cube divisors to consider [default = %d]\n", p->nSingleMax ); - Abc_Print( -2, "\t-D num : max number of double-cube divisors to consider [default = %d]\n", p->nPairsMax ); - Abc_Print( -2, "\t-N num : the maximum number of divisors to extract [default = %d]\n", p->nNodesExt ); - Abc_Print( -2, "\t-s : use only single-cube divisors [default = %s]\n", p->fOnlyS? "yes": "no" ); - Abc_Print( -2, "\t-d : use only double-cube divisors [default = %s]\n", p->fOnlyD? "yes": "no" ); - Abc_Print( -2, "\t-z : use zero-weight divisors [default = %s]\n", p->fUse0? "yes": "no" ); - Abc_Print( -2, "\t-c : use complement in the binary case [default = %s]\n", p->fUseCompl? "yes": "no" ); - Abc_Print( -2, "\t-v : print verbose information [default = %s]\n", p->fVerbose? "yes": "no" ); - Abc_Print( -2, "\t-h : print the command usage\n"); + Abc_Print( -2, "usage: fx [-SDN ] [-sdzcvh]\n"); + Abc_Print( -2, "\t performs unate fast extract on the current network\n"); + Abc_Print( -2, "\t-S : max number of single-cube divisors to consider [default = %d]\n", p->nSingleMax ); + Abc_Print( -2, "\t-D : max number of double-cube divisors to consider [default = %d]\n", p->nPairsMax ); + Abc_Print( -2, "\t-N : the maximum number of divisors to extract [default = %d]\n", p->nNodesExt ); + Abc_Print( -2, "\t-s : use only single-cube divisors [default = %s]\n", p->fOnlyS? "yes": "no" ); + Abc_Print( -2, "\t-d : use only double-cube divisors [default = %s]\n", p->fOnlyD? "yes": "no" ); + Abc_Print( -2, "\t-z : use zero-weight divisors [default = %s]\n", p->fUse0? "yes": "no" ); + Abc_Print( -2, "\t-c : use complement in the binary case [default = %s]\n", p->fUseCompl? "yes": "no" ); + Abc_Print( -2, "\t-v : print verbose information [default = %s]\n", p->fVerbose? "yes": "no" ); + Abc_Print( -2, "\t-h : print the command usage\n"); Abc_NtkFxuFreeInfo( p ); return 1; } @@ -3506,12 +3510,12 @@ int Abc_CommandEliminate( Abc_Frame_t * pAbc, int argc, char ** argv ) return 0; usage: - Abc_Print( -2, "usage: eliminate [-N num] [-rvh]\n"); - Abc_Print( -2, "\t greedily eliminates nodes by collapsing them into fanouts\n"); - Abc_Print( -2, "\t-N num : the maximum support size after collapsing [default = %d]\n", nMaxSize ); - Abc_Print( -2, "\t-r : use the reverse topological order [default = %s]\n", fReverse? "yes": "no" ); - Abc_Print( -2, "\t-v : print verbose information [default = %s]\n", fVerbose? "yes": "no" ); - Abc_Print( -2, "\t-h : print the command usage\n"); + Abc_Print( -2, "usage: eliminate [-N ] [-rvh]\n"); + Abc_Print( -2, "\t greedily eliminates nodes by collapsing them into fanouts\n"); + Abc_Print( -2, "\t-N : the maximum support size after collapsing [default = %d]\n", nMaxSize ); + Abc_Print( -2, "\t-r : use the reverse topological order [default = %s]\n", fReverse? "yes": "no" ); + Abc_Print( -2, "\t-v : print verbose information [default = %s]\n", fVerbose? "yes": "no" ); + Abc_Print( -2, "\t-h : print the command usage\n"); return 1; } @@ -3762,7 +3766,7 @@ int Abc_CommandLutpack( Abc_Frame_t * pAbc, int argc, char ** argv ) return 0; usage: - Abc_Print( -2, "usage: lutpack [-N ] [-Q ] [-S ] [-L ] [-szfovwh]\n" ); + Abc_Print( -2, "usage: lutpack [-NQSL ] [-szfovwh]\n" ); Abc_Print( -2, "\t performs \"rewriting\" for LUT network;\n" ); Abc_Print( -2, "\t determines LUT size as the max fanin count of a node;\n" ); Abc_Print( -2, "\t if the network is not LUT-mapped, packs it into 6-LUTs\n" ); @@ -3964,7 +3968,7 @@ int Abc_CommandImfs( Abc_Frame_t * pAbc, int argc, char ** argv ) return 0; usage: - Abc_Print( -2, "usage: imfs [-W ] [-L ] [-C ] [-S ] [-avwh]\n" ); + Abc_Print( -2, "usage: imfs [-W ] [-LCS ] [-avwh]\n" ); Abc_Print( -2, "\t performs resubstitution-based resynthesis with interpolation\n" ); Abc_Print( -2, "\t (there is another command for resynthesis after LUT mapping, \"lutpack\")\n" ); Abc_Print( -2, "\t-W : fanin/fanout levels (NxM) of the window (00 <= NM <= 99) [default = %d%d]\n", pPars->nWindow/10, pPars->nWindow%10 ); @@ -4302,7 +4306,7 @@ int Abc_CommandSpeedup( Abc_Frame_t * pAbc, int argc, char ** argv ) return 0; usage: - Abc_Print( -2, "usage: speedup [-P num] [-N num] [-lvwh]\n" ); + Abc_Print( -2, "usage: speedup [-PN ] [-lvwh]\n" ); Abc_Print( -2, "\t transforms LUT-mapped network into an AIG with choices;\n" ); Abc_Print( -2, "\t the choices are added to speedup the next round of mapping\n" ); Abc_Print( -2, "\t-P : delay delta defining critical path for library model [default = %d%%]\n", Percentage ); @@ -4409,7 +4413,7 @@ int Abc_CommandPowerdown( Abc_Frame_t * pAbc, int argc, char ** argv ) return 0; usage: - Abc_Print( -2, "usage: powerdown [-P num] [-N num] [-vwh]\n" ); + Abc_Print( -2, "usage: powerdown [-PN ] [-vwh]\n" ); Abc_Print( -2, "\t transforms LUT-mapped network into an AIG with choices;\n" ); Abc_Print( -2, "\t the choices are added to power down the next round of mapping\n" ); Abc_Print( -2, "\t-P : switching propability delta defining power critical edges [default = %d%%]\n", Percentage ); @@ -4540,7 +4544,7 @@ int Abc_CommandMerge( Abc_Frame_t * pAbc, int argc, char ** argv ) return 0; usage: - Abc_Print( -2, "usage: merge [-NSDLF num] [-scwvh]\n" ); + Abc_Print( -2, "usage: merge [-NSDLF ] [-scwvh]\n" ); Abc_Print( -2, "\t creates pairs of topologically-related LUTs\n" ); Abc_Print( -2, "\t-N : the max LUT size for merging (1 < num) [default = %d]\n", pPars->nMaxLutSize ); Abc_Print( -2, "\t-S : the max total support size after merging (1 < num) [default = %d]\n", pPars->nMaxSuppSize ); @@ -4765,15 +4769,15 @@ int Abc_CommandRefactor( Abc_Frame_t * pAbc, int argc, char ** argv ) return 0; usage: - Abc_Print( -2, "usage: refactor [-N num] [-C num] [-lzdvh]\n" ); - Abc_Print( -2, "\t performs technology-independent refactoring of the AIG\n" ); - Abc_Print( -2, "\t-N num : the max support of the collapsed node [default = %d]\n", nNodeSizeMax ); - Abc_Print( -2, "\t-C num : the max support of the containing cone [default = %d]\n", nConeSizeMax ); - Abc_Print( -2, "\t-l : toggle preserving the number of levels [default = %s]\n", fUpdateLevel? "yes": "no" ); - Abc_Print( -2, "\t-z : toggle using zero-cost replacements [default = %s]\n", fUseZeros? "yes": "no" ); - Abc_Print( -2, "\t-d : toggle using don't-cares [default = %s]\n", fUseDcs? "yes": "no" ); - Abc_Print( -2, "\t-v : toggle verbose printout [default = %s]\n", fVerbose? "yes": "no" ); - Abc_Print( -2, "\t-h : print the command usage\n"); + Abc_Print( -2, "usage: refactor [-NC ] [-lzdvh]\n" ); + Abc_Print( -2, "\t performs technology-independent refactoring of the AIG\n" ); + Abc_Print( -2, "\t-N : the max support of the collapsed node [default = %d]\n", nNodeSizeMax ); + Abc_Print( -2, "\t-C : the max support of the containing cone [default = %d]\n", nConeSizeMax ); + Abc_Print( -2, "\t-l : toggle preserving the number of levels [default = %s]\n", fUpdateLevel? "yes": "no" ); + Abc_Print( -2, "\t-z : toggle using zero-cost replacements [default = %s]\n", fUseZeros? "yes": "no" ); + Abc_Print( -2, "\t-d : toggle using don't-cares [default = %s]\n", fUseDcs? "yes": "no" ); + Abc_Print( -2, "\t-v : toggle verbose printout [default = %s]\n", fVerbose? "yes": "no" ); + Abc_Print( -2, "\t-h : print the command usage\n"); return 1; } @@ -4865,13 +4869,13 @@ int Abc_CommandRestructure( Abc_Frame_t * pAbc, int argc, char ** argv ) return 0; usage: - Abc_Print( -2, "usage: restructure [-K num] [-lzvh]\n" ); - Abc_Print( -2, "\t performs technology-independent restructuring of the AIG\n" ); - Abc_Print( -2, "\t-K num : the max cut size (%d <= num <= %d) [default = %d]\n", CUT_SIZE_MIN, CUT_SIZE_MAX, nCutsMax ); - Abc_Print( -2, "\t-l : toggle preserving the number of levels [default = %s]\n", fUpdateLevel? "yes": "no" ); - Abc_Print( -2, "\t-z : toggle using zero-cost replacements [default = %s]\n", fUseZeros? "yes": "no" ); - Abc_Print( -2, "\t-v : toggle verbose printout [default = %s]\n", fVerbose? "yes": "no" ); - Abc_Print( -2, "\t-h : print the command usage\n"); + Abc_Print( -2, "usage: restructure [-K ] [-lzvh]\n" ); + Abc_Print( -2, "\t performs technology-independent restructuring of the AIG\n" ); + Abc_Print( -2, "\t-K : the max cut size (%d <= num <= %d) [default = %d]\n", CUT_SIZE_MIN, CUT_SIZE_MAX, nCutsMax ); + Abc_Print( -2, "\t-l : toggle preserving the number of levels [default = %s]\n", fUpdateLevel? "yes": "no" ); + Abc_Print( -2, "\t-z : toggle using zero-cost replacements [default = %s]\n", fUseZeros? "yes": "no" ); + Abc_Print( -2, "\t-v : toggle verbose printout [default = %s]\n", fVerbose? "yes": "no" ); + Abc_Print( -2, "\t-h : print the command usage\n"); return 1; } @@ -5001,16 +5005,16 @@ int Abc_CommandResubstitute( Abc_Frame_t * pAbc, int argc, char ** argv ) return 0; usage: - Abc_Print( -2, "usage: resub [-K num] [-N num] [-F num] [-lzvwh]\n" ); - Abc_Print( -2, "\t performs technology-independent restructuring of the AIG\n" ); - Abc_Print( -2, "\t-K num : the max cut size (%d <= num <= %d) [default = %d]\n", RS_CUT_MIN, RS_CUT_MAX, nCutsMax ); - Abc_Print( -2, "\t-N num : the max number of nodes to add (0 <= num <= 3) [default = %d]\n", nNodesMax ); - Abc_Print( -2, "\t-F num : the number of fanout levels for ODC computation [default = %d]\n", nLevelsOdc ); - Abc_Print( -2, "\t-l : toggle preserving the number of levels [default = %s]\n", fUpdateLevel? "yes": "no" ); - Abc_Print( -2, "\t-z : toggle using zero-cost replacements [default = %s]\n", fUseZeros? "yes": "no" ); - Abc_Print( -2, "\t-v : toggle verbose printout [default = %s]\n", fVerbose? "yes": "no" ); - Abc_Print( -2, "\t-w : toggle verbose printout of ODC computation [default = %s]\n", fVeryVerbose? "yes": "no" ); - Abc_Print( -2, "\t-h : print the command usage\n"); + Abc_Print( -2, "usage: resub [-KN ] [-lzvwh]\n" ); + Abc_Print( -2, "\t performs technology-independent restructuring of the AIG\n" ); + Abc_Print( -2, "\t-K : the max cut size (%d <= num <= %d) [default = %d]\n", RS_CUT_MIN, RS_CUT_MAX, nCutsMax ); + Abc_Print( -2, "\t-N : the max number of nodes to add (0 <= num <= 3) [default = %d]\n", nNodesMax ); + Abc_Print( -2, "\t-F : the number of fanout levels for ODC computation [default = %d]\n", nLevelsOdc ); + Abc_Print( -2, "\t-l : toggle preserving the number of levels [default = %s]\n", fUpdateLevel? "yes": "no" ); + Abc_Print( -2, "\t-z : toggle using zero-cost replacements [default = %s]\n", fUseZeros? "yes": "no" ); + Abc_Print( -2, "\t-v : toggle verbose printout [default = %s]\n", fVerbose? "yes": "no" ); + Abc_Print( -2, "\t-w : toggle verbose printout of ODC computation [default = %s]\n", fVeryVerbose? "yes": "no" ); + Abc_Print( -2, "\t-h : print the command usage\n"); return 1; } @@ -5190,12 +5194,12 @@ int Abc_CommandCascade( Abc_Frame_t * pAbc, int argc, char ** argv ) usage: Abc_Print( -2, "usage: cascade [-K ] [-cvh]\n" ); - Abc_Print( -2, "\t performs LUT cascade synthesis for the current network\n" ); - Abc_Print( -2, "\t-K num : the number of LUT inputs [default = %d]\n", nLutSize ); - Abc_Print( -2, "\t-c : check equivalence after synthesis [default = %s]\n", fCheck? "yes": "no" ); - Abc_Print( -2, "\t-v : toggle verbose printout [default = %s]\n", fVerbose? "yes": "no" ); - Abc_Print( -2, "\t-h : print the command usage\n"); - Abc_Print( -2, "\t \n"); + Abc_Print( -2, "\t performs LUT cascade synthesis for the current network\n" ); + Abc_Print( -2, "\t-K : the number of LUT inputs [default = %d]\n", nLutSize ); + Abc_Print( -2, "\t-c : check equivalence after synthesis [default = %s]\n", fCheck? "yes": "no" ); + Abc_Print( -2, "\t-v : toggle verbose printout [default = %s]\n", fVerbose? "yes": "no" ); + Abc_Print( -2, "\t-h : print the command usage\n"); + Abc_Print( -2, "\t \n"); Abc_Print( -2, " A lookup-table cascade is a programmable architecture developed by\n"); Abc_Print( -2, " Professor Tsutomu Sasao (sasao@cse.kyutech.ac.jp) at Kyushu Institute\n"); Abc_Print( -2, " of Technology. This work received Takeda Techno-Entrepreneurship Award:\n"); @@ -5341,11 +5345,11 @@ int Abc_CommandComb( Abc_Frame_t * pAbc, int argc, char ** argv ) return 0; usage: - Abc_Print( -2, "usage: comb [-L num] [-lh]\n" ); - Abc_Print( -2, "\t converts comb network into seq, and vice versa\n" ); - Abc_Print( -2, "\t-L : number of latches to add to comb network (0 = do not add) [default = %d]\n", nLatchesToAdd ); - Abc_Print( -2, "\t-l : toggle converting latches to PIs/POs or removing them [default = %s]\n", fRemoveLatches? "remove": "convert" ); - Abc_Print( -2, "\t-h : print the command usage\n"); + Abc_Print( -2, "usage: comb [-L ] [-lh]\n" ); + Abc_Print( -2, "\t converts comb network into seq, and vice versa\n" ); + Abc_Print( -2, "\t-L : number of latches to add to comb network (0 = do not add) [default = %d]\n", nLatchesToAdd ); + Abc_Print( -2, "\t-l : toggle converting latches to PIs/POs or removing them [default = %s]\n", fRemoveLatches? "remove": "convert" ); + Abc_Print( -2, "\t-h : print the command usage\n"); return 1; } @@ -5436,17 +5440,17 @@ usage: strcpy( Buffer, "unused" ); else sprintf( Buffer, "%d", nPartSize ); - Abc_Print( -2, "usage: miter [-P num] [-cimh] \n" ); - Abc_Print( -2, "\t computes the miter of the two circuits\n" ); - Abc_Print( -2, "\t-P num : output partition size [default = %s]\n", Buffer ); - Abc_Print( -2, "\t-c : toggles deriving combinational miter (latches as POs) [default = %s]\n", fComb? "yes": "no" ); - Abc_Print( -2, "\t-i : toggles deriving implication miter (file1 => file2) [default = %s]\n", fImplic? "yes": "no" ); - Abc_Print( -2, "\t-m : toggles creating multi-output miter [default = %s]\n", fMulti? "yes": "no" ); - Abc_Print( -2, "\t-h : print the command usage\n"); - Abc_Print( -2, "\tfile1 : (optional) the file with the first network\n"); - Abc_Print( -2, "\tfile2 : (optional) the file with the second network\n"); - Abc_Print( -2, "\t if no files are given, uses the current network and its spec\n"); - Abc_Print( -2, "\t if one file is given, uses the current network and the file\n"); + Abc_Print( -2, "usage: miter [-P ] [-cimh] \n" ); + Abc_Print( -2, "\t computes the miter of the two circuits\n" ); + Abc_Print( -2, "\t-P : output partition size [default = %s]\n", Buffer ); + Abc_Print( -2, "\t-c : toggles deriving combinational miter (latches as POs) [default = %s]\n", fComb? "yes": "no" ); + Abc_Print( -2, "\t-i : toggles deriving implication miter (file1 => file2) [default = %s]\n", fImplic? "yes": "no" ); + Abc_Print( -2, "\t-m : toggles creating multi-output miter [default = %s]\n", fMulti? "yes": "no" ); + Abc_Print( -2, "\t-h : print the command usage\n"); + Abc_Print( -2, "\tfile1 : (optional) the file with the first network\n"); + Abc_Print( -2, "\tfile2 : (optional) the file with the second network\n"); + Abc_Print( -2, "\t if no files are given, uses the current network and its spec\n"); + Abc_Print( -2, "\t if one file is given, uses the current network and the file\n"); return 1; } @@ -5484,6 +5488,12 @@ int Abc_CommandDemiter( Abc_Frame_t * pAbc, int argc, char ** argv ) } } + if ( pNtk == NULL ) + { + Abc_Print( -1, "Empty network.\n" ); + return 1; + } + if ( !Abc_NtkIsStrash(pNtk) ) { Abc_Print( -1, "The network is not strashed.\n" ); @@ -5561,6 +5571,12 @@ int Abc_CommandOrPos( Abc_Frame_t * pAbc, int argc, char ** argv ) } } + if ( pNtk == NULL ) + { + Abc_Print( -1, "Empty network.\n" ); + return 1; + } + if ( !Abc_NtkIsStrash(pNtk) ) { Abc_Print( -1, "The network is not strashed.\n" ); @@ -5629,6 +5645,12 @@ int Abc_CommandAndPos( Abc_Frame_t * pAbc, int argc, char ** argv ) } } + if ( pNtk == NULL ) + { + Abc_Print( -1, "Empty network.\n" ); + return 1; + } + if ( !Abc_NtkIsStrash(pNtk) ) { Abc_Print( -1, "The network is not strashed.\n" ); @@ -5704,6 +5726,12 @@ int Abc_CommandZeroPo( Abc_Frame_t * pAbc, int argc, char ** argv ) } } + if ( pNtk == NULL ) + { + Abc_Print( -1, "Empty network.\n" ); + return 1; + } + if ( !Abc_NtkIsStrash(pNtk) ) { Abc_Print( -1, "The network is not strashed.\n" ); @@ -5727,10 +5755,10 @@ int Abc_CommandZeroPo( Abc_Frame_t * pAbc, int argc, char ** argv ) return 0; usage: - Abc_Print( -2, "usage: zeropo [-N num] [-h]\n" ); - Abc_Print( -2, "\t replaces the PO driver by constant 0\n" ); - Abc_Print( -2, "\t-N num : the zero-based index of the PO to replace [default = %d]\n", iOutput ); - Abc_Print( -2, "\t-h : print the command usage\n"); + Abc_Print( -2, "usage: zeropo [-N ] [-h]\n" ); + Abc_Print( -2, "\t replaces the PO driver by constant 0\n" ); + Abc_Print( -2, "\t-N : the zero-based index of the PO to replace [default = %d]\n", iOutput ); + Abc_Print( -2, "\t-h : print the command usage\n"); return 1; } @@ -5773,6 +5801,12 @@ int Abc_CommandSwapPos( Abc_Frame_t * pAbc, int argc, char ** argv ) } } + if ( pNtk == NULL ) + { + Abc_Print( -1, "Empty network.\n" ); + return 1; + } + if ( !Abc_NtkIsStrash(pNtk) ) { Abc_Print( -1, "The network is not strashed.\n" ); @@ -5796,9 +5830,61 @@ int Abc_CommandSwapPos( Abc_Frame_t * pAbc, int argc, char ** argv ) return 0; usage: - Abc_Print( -2, "usage: swappos [-N num] [-h]\n" ); - Abc_Print( -2, "\t swap the 0-th PO with the -th PO\n" ); - Abc_Print( -2, "\t-N num : the zero-based index of the PO to swap [default = %d]\n", iOutput ); + Abc_Print( -2, "usage: swappos [-N ] [-h]\n" ); + Abc_Print( -2, "\t swap the 0-th PO with the -th PO\n" ); + Abc_Print( -2, "\t-N : the zero-based index of the PO to swap [default = %d]\n", iOutput ); + Abc_Print( -2, "\t-h : print the command usage\n"); + return 1; +} + +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Abc_CommandAddPi( Abc_Frame_t * pAbc, int argc, char ** argv ) +{ + Abc_Ntk_t * pNtk = Abc_FrameReadNtk(pAbc), * pNtkRes; + int c; + + // set defaults + Extra_UtilGetoptReset(); + while ( ( c = Extra_UtilGetopt( argc, argv, "h" ) ) != EOF ) + { + switch ( c ) + { + case 'h': + default: + goto usage; + } + } + + if ( pNtk == NULL ) + { + Abc_Print( -1, "Empty network.\n" ); + return 1; + } + + // get the new network + pNtkRes = Abc_NtkDup( pNtk ); + if ( Abc_NtkPiNum(pNtkRes) == 0 ) + { + Abc_Obj_t * pObj = Abc_NtkCreatePi( pNtkRes ); + Abc_ObjAssignName( pObj, "dummy_pi", NULL ); + Abc_NtkOrderCisCos( pNtkRes ); + } + Abc_FrameReplaceCurrentNetwork( pAbc, pNtkRes ); + return 0; + +usage: + Abc_Print( -2, "usage: addpi [-h]\n" ); + Abc_Print( -2, "\t if the network has no PIs, add one dummy PI\n" ); Abc_Print( -2, "\t-h : print the command usage\n"); return 1; } @@ -5963,12 +6049,12 @@ int Abc_CommandFrames( Abc_Frame_t * pAbc, int argc, char ** argv ) return 0; usage: - Abc_Print( -2, "usage: frames [-F num] [-ivh]\n" ); - Abc_Print( -2, "\t unrolls the network for a number of time frames\n" ); - Abc_Print( -2, "\t-F num : the number of frames to unroll [default = %d]\n", nFrames ); - Abc_Print( -2, "\t-i : toggles initializing the first frame [default = %s]\n", fInitial? "yes": "no" ); - Abc_Print( -2, "\t-v : toggles outputting verbose information [default = %s]\n", fVerbose? "yes": "no" ); - Abc_Print( -2, "\t-h : print the command usage\n"); + Abc_Print( -2, "usage: frames [-F ] [-ivh]\n" ); + Abc_Print( -2, "\t unrolls the network for a number of time frames\n" ); + Abc_Print( -2, "\t-F : the number of frames to unroll [default = %d]\n", nFrames ); + Abc_Print( -2, "\t-i : toggles initializing the first frame [default = %s]\n", fInitial? "yes": "no" ); + Abc_Print( -2, "\t-v : toggles outputting verbose information [default = %s]\n", fVerbose? "yes": "no" ); + Abc_Print( -2, "\t-h : print the command usage\n"); return 1; } @@ -6070,7 +6156,7 @@ int Abc_CommandDFrames( Abc_Frame_t * pAbc, int argc, char ** argv ) return 0; usage: - Abc_Print( -2, "usage: dframes [-NF num] [-ivh]\n" ); + Abc_Print( -2, "usage: dframes [-NF ] [-ivh]\n" ); Abc_Print( -2, "\t unrolls the network with simplification\n" ); Abc_Print( -2, "\t-N num : the number of frames to use as prefix [default = %d]\n", nPrefix ); Abc_Print( -2, "\t-F num : the number of frames to unroll [default = %d]\n", nFrames ); @@ -14403,7 +14489,7 @@ int Abc_CommandSeqSweep2( Abc_Frame_t * pAbc, int argc, char ** argv ) // set defaults Ssw_ManSetDefaultParams( pPars ); Extra_UtilGetoptReset(); - while ( ( c = Extra_UtilGetopt( argc, argv, "PQFCLSIVMNcmplofdsvwh" ) ) != EOF ) + while ( ( c = Extra_UtilGetopt( argc, argv, "PQFCLSIVMNcmplofdsevwh" ) ) != EOF ) { switch ( c ) { @@ -14541,6 +14627,9 @@ int Abc_CommandSeqSweep2( Abc_Frame_t * pAbc, int argc, char ** argv ) case 's': pPars->fLocalSim ^= 1; break; + case 'e': + pPars->fEquivDump ^= 1; + break; case 'v': pPars->fVerbose ^= 1; break; @@ -14607,7 +14696,7 @@ int Abc_CommandSeqSweep2( Abc_Frame_t * pAbc, int argc, char ** argv ) return 0; usage: - Abc_Print( -2, "usage: scorr [-PQFCLSIVMN ] [-cmplodsvwh]\n" ); + Abc_Print( -2, "usage: scorr [-PQFCLSIVMN ] [-cmplodsevwh]\n" ); Abc_Print( -2, "\t performs sequential sweep using K-step induction\n" ); Abc_Print( -2, "\t-P num : max partition size (0 = no partitioning) [default = %d]\n", pPars->nPartSize ); Abc_Print( -2, "\t-Q num : partition overlap (0 = no overlap) [default = %d]\n", pPars->nOverSize ); @@ -14628,6 +14717,7 @@ usage: // Abc_Print( -2, "\t-f : toggle filtering using iterative BMC [default = %s]\n", pPars->fSemiFormal? "yes": "no" ); Abc_Print( -2, "\t-d : toggle dynamic addition of constraints [default = %s]\n", pPars->fDynamic? "yes": "no" ); Abc_Print( -2, "\t-s : toggle local simulation in the cone of influence [default = %s]\n", pPars->fLocalSim? "yes": "no" ); + Abc_Print( -2, "\t-e : toggle dumping disproved internal equivalences [default = %s]\n", pPars->fEquivDump? "yes": "no" ); Abc_Print( -2, "\t-w : toggle printout of flop equivalences [default = %s]\n", pPars->fFlopVerbose? "yes": "no" ); Abc_Print( -2, "\t-v : toggle verbose output [default = %s]\n", pPars->fVerbose? "yes": "no" ); Abc_Print( -2, "\t-h : print the command usage\n"); @@ -16631,7 +16721,7 @@ int Abc_CommandDProve( Abc_Frame_t * pAbc, int argc, char ** argv ) Fra_SecSetDefaultParams( pSecPar ); // pSecPar->TimeLimit = 300; Extra_UtilGetoptReset(); - while ( ( c = Extra_UtilGetopt( argc, argv, "cbFCGDVBRLarmfijkouwvh" ) ) != EOF ) + while ( ( c = Extra_UtilGetopt( argc, argv, "cbFCGDVBRTLarmfijkouwvh" ) ) != EOF ) { switch ( c ) { @@ -16718,6 +16808,17 @@ int Abc_CommandDProve( Abc_Frame_t * pAbc, int argc, char ** argv ) if ( pSecPar->nBddIterMax < 0 ) goto usage; break; + case 'T': + if ( globalUtilOptind >= argc ) + { + Abc_Print( -1, "Command line switch \"-T\" should be followed by an integer.\n" ); + goto usage; + } + pSecPar->nPdrTimeout = atoi(argv[globalUtilOptind]); + globalUtilOptind++; + if ( pSecPar->nPdrTimeout < 0 ) + goto usage; + break; case 'L': if ( globalUtilOptind >= argc ) { @@ -16754,6 +16855,9 @@ int Abc_CommandDProve( Abc_Frame_t * pAbc, int argc, char ** argv ) case 'u': pSecPar->fReadUnsolved ^= 1; break; + case 'p': + pSecPar->fUsePdr ^= 1; + break; case 'w': pSecPar->fVeryVerbose ^= 1; break; @@ -16796,7 +16900,7 @@ int Abc_CommandDProve( Abc_Frame_t * pAbc, int argc, char ** argv ) return 0; usage: - Abc_Print( -2, "usage: dprove [-FCGDVBR num] [-L file] [-cbarmfijouwvh]\n" ); + Abc_Print( -2, "usage: dprove [-FCGDVBRT num] [-L file] [-cbarmfijoupvwh]\n" ); Abc_Print( -2, "\t performs SEC on the sequential miter\n" ); Abc_Print( -2, "\t-F num : the limit on the depth of induction [default = %d]\n", pSecPar->nFramesMax ); Abc_Print( -2, "\t-C num : the conflict limit at a node during induction [default = %d]\n", pSecPar->nBTLimit ); @@ -16805,6 +16909,7 @@ usage: Abc_Print( -2, "\t-V num : the flop count limit for BDD-based reachablity [default = %d]\n", pSecPar->nBddVarsMax ); Abc_Print( -2, "\t-B num : the BDD size limit in BDD-based reachablity [default = %d]\n", pSecPar->nBddMax ); Abc_Print( -2, "\t-R num : the max number of reachability iterations [default = %d]\n", pSecPar->nBddIterMax ); + Abc_Print( -2, "\t-T num : the timeout for property directed reachability [default = %d]\n", pSecPar->nPdrTimeout ); Abc_Print( -2, "\t-L file: the log file name [default = %s]\n", pLogFileName ? pLogFileName : "no logging" ); Abc_Print( -2, "\t-c : toggles using CEC before attempting SEC [default = %s]\n", pSecPar->fTryComb? "yes": "no" ); Abc_Print( -2, "\t-b : toggles using BMC before attempting SEC [default = %s]\n", pSecPar->fTryBmc? "yes": "no" ); @@ -16817,6 +16922,7 @@ usage: Abc_Print( -2, "\t-k : toggles applying interpolation to each output [default = %s]\n", pSecPar->fInterSeparate? "yes": "no" ); Abc_Print( -2, "\t-o : toggles using BDD variable reordering during image computation [default = %s]\n", pSecPar->fReorderImage? "yes": "no" ); Abc_Print( -2, "\t-u : toggles reading back unsolved reduced sequential miter [default = %s]\n", pSecPar->fReadUnsolved? "yes": "no" ); + Abc_Print( -2, "\t-p : toggles trying property directed reachability in the end [default = %s]\n", pSecPar->fUsePdr? "yes": "no" ); Abc_Print( -2, "\t-v : toggles verbose output [default = %s]\n", pSecPar->fVerbose? "yes": "no" ); Abc_Print( -2, "\t-w : toggles additional verbose output [default = %s]\n", pSecPar->fVeryVerbose? "yes": "no" ); Abc_Print( -2, "\t-h : print the command usage\n"); @@ -18855,7 +18961,120 @@ usage: Abc_Print( -2, "\t-h : print the command usage\n"); return 1; } - + +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Abc_CommandTempor( Abc_Frame_t * pAbc, int argc, char ** argv ) +{ + extern Abc_Ntk_t * Abc_NtkDarTempor( Abc_Ntk_t * pNtk, int nFrames, int TimeOut, int nConfLimit, int fUseBmc, int fVerbose, int fVeryVerbose ); + Abc_Ntk_t * pNtkRes, * pNtk = Abc_FrameReadNtk(pAbc); + int nFrames = 0; + int TimeOut = 300; + int nConfMax = 100000; + int fUseBmc = 1; + int fVerbose = 0; + int fVeryVerbose = 0; + int c; + Extra_UtilGetoptReset(); + while ( ( c = Extra_UtilGetopt( argc, argv, "FTCbvwh" ) ) != EOF ) + { + switch ( c ) + { + case 'F': + if ( globalUtilOptind >= argc ) + { + Abc_Print( -1, "Command line switch \"-F\" should be followed by an integer.\n" ); + goto usage; + } + nFrames = atoi(argv[globalUtilOptind]); + globalUtilOptind++; + if ( nFrames < 0 ) + goto usage; + break; + case 'T': + if ( globalUtilOptind >= argc ) + { + Abc_Print( -1, "Command line switch \"-T\" should be followed by an integer.\n" ); + goto usage; + } + TimeOut = atoi(argv[globalUtilOptind]); + globalUtilOptind++; + if ( TimeOut < 0 ) + goto usage; + break; + case 'C': + if ( globalUtilOptind >= argc ) + { + Abc_Print( -1, "Command line switch \"-C\" should be followed by an integer.\n" ); + goto usage; + } + nConfMax = atoi(argv[globalUtilOptind]); + globalUtilOptind++; + if ( nConfMax < 0 ) + goto usage; + break; + case 'b': + fUseBmc ^= 1; + break; + case 'v': + fVerbose ^= 1; + break; + case 'w': + fVeryVerbose ^= 1; + break; + case 'h': + default: + goto usage; + } + } + if ( pNtk == NULL ) + { + Abc_Print( -2, "There is no current network.\n"); + return 0; + } + if ( Abc_NtkLatchNum(pNtk) == 0 ) + { + Abc_Print( -2, "The current network is combinational.\n"); + return 0; + } + if ( !Abc_NtkIsStrash(pNtk) ) + { + Abc_Print( -2, "The current network is not an AIG (run \"strash\").\n"); + return 0; + } + // modify the current network + pNtkRes = Abc_NtkDarTempor( pNtk, nFrames, TimeOut, nConfMax, fUseBmc, fVerbose, fVeryVerbose ); + if ( pNtkRes == NULL ) + { + Abc_Print( -1, "Temporal decomposition has failed.\n" ); + return 1; + } + // replace the current network + Abc_FrameReplaceCurrentNetwork( pAbc, pNtkRes ); + return 0; + +usage: + Abc_Print( -2, "usage: tempor [-FTC ] [-bvwh]\n" ); + Abc_Print( -2, "\t performs temporal decomposition\n" ); + Abc_Print( -2, "\t-F : init logic timeframe count (0 = use leading length) [default = %d]\n", nFrames ); + Abc_Print( -2, "\t-T : runtime limit in seconds for BMC (0=unused) [default = %d]\n", TimeOut ); + Abc_Print( -2, "\t-C : max number of SAT conflicts in BMC (0=unused) [default = %d]\n", nConfMax ); + Abc_Print( -2, "\t-b : toggle running BMC2 on the init frames [default = %s]\n", fUseBmc? "yes": "no" ); + Abc_Print( -2, "\t-v : toggle printing verbose output [default = %s]\n", fVerbose? "yes": "no" ); + Abc_Print( -2, "\t-w : toggle printing ternary state space [default = %s]\n", fVeryVerbose? "yes": "no" ); + Abc_Print( -2, "\t-h : print the command usage\n"); + return 1; +} + /**Function************************************************************* Synopsis [] @@ -19615,12 +19834,13 @@ int Abc_CommandTestCex( Abc_Frame_t * pAbc, int argc, char ** argv ) extern Aig_Man_t * Abc_NtkToDar( Abc_Ntk_t * pNtk, int fExors, int fRegisters ); Aig_Man_t * pAig = Abc_NtkToDar( pNtk, 0, 1 ); Gia_Man_t * pGia = Gia_ManFromAigSimple( pAig ); - Aig_ManStop( pAig ); if ( !Gia_ManVerifyCounterExample( pGia, pAbc->pCex, 0 ) ) +// if ( !Ssw_SmlRunCounterExample( pAig, pAbc->pCex ) ) Abc_Print( 1, "Main AIG: The cex does not fail any outputs.\n" ); else Abc_Print( 1, "Main AIG: The cex is correct.\n" ); Gia_ManStop( pGia ); + Aig_ManStop( pAig ); } // check the AND AIG @@ -19661,19 +19881,92 @@ usage: ***********************************************************************/ int Abc_CommandPdr( Abc_Frame_t * pAbc, int argc, char ** argv ) { - extern int Abc_NtkDarPdr( Abc_Ntk_t * pNtk, Abc_Cex_t ** ppCex ); - Abc_Ntk_t * pNtk = Abc_FrameReadNtk(pAbc); - Abc_Cex_t * pCex; + extern int Abc_NtkDarPdr( Abc_Ntk_t * pNtk, Pdr_Par_t * pPars, Abc_Cex_t ** ppCex ); + Pdr_Par_t Pars, * pPars = &Pars; + Abc_Ntk_t * pNtk = Abc_FrameReadNtk(pAbc); + Abc_Cex_t * pCex = NULL; int c; + Pdr_ManSetDefaultParams( pPars ); Extra_UtilGetoptReset(); - while ( ( c = Extra_UtilGetopt( argc, argv, "h" ) ) != EOF ) + while ( ( c = Extra_UtilGetopt( argc, argv, "OMFCTrmsdvwh" ) ) != EOF ) { switch ( c ) { + case 'O': + if ( globalUtilOptind >= argc ) + { + Abc_Print( -1, "Command line switch \"-O\" should be followed by an integer.\n" ); + goto usage; + } + pPars->iOutput = atoi(argv[globalUtilOptind]); + globalUtilOptind++; + if ( pPars->iOutput < 0 ) + goto usage; + break; + case 'M': + if ( globalUtilOptind >= argc ) + { + Abc_Print( -1, "Command line switch \"-M\" should be followed by an integer.\n" ); + goto usage; + } + pPars->nRecycle = atoi(argv[globalUtilOptind]); + globalUtilOptind++; + if ( pPars->nRecycle < 0 ) + goto usage; + break; + case 'F': + if ( globalUtilOptind >= argc ) + { + Abc_Print( -1, "Command line switch \"-F\" should be followed by an integer.\n" ); + goto usage; + } + pPars->nFrameMax = atoi(argv[globalUtilOptind]); + globalUtilOptind++; + if ( pPars->nFrameMax < 0 ) + goto usage; + break; + case 'C': + if ( globalUtilOptind >= argc ) + { + Abc_Print( -1, "Command line switch \"-C\" should be followed by an integer.\n" ); + goto usage; + } + pPars->nConfLimit = atoi(argv[globalUtilOptind]); + globalUtilOptind++; + if ( pPars->nConfLimit < 0 ) + goto usage; + break; + case 'T': + if ( globalUtilOptind >= argc ) + { + Abc_Print( -1, "Command line switch \"-T\" should be followed by an integer.\n" ); + goto usage; + } + pPars->nTimeOut = atoi(argv[globalUtilOptind]); + globalUtilOptind++; + if ( pPars->nTimeOut < 0 ) + goto usage; + break; + case 'r': + pPars->fTwoRounds ^= 1; + break; + case 'm': + pPars->fMonoCnf ^= 1; + break; + case 's': + pPars->fShortest ^= 1; + break; + case 'd': + pPars->fDumpInv ^= 1; + break; + case 'v': + pPars->fVerbose ^= 1; + break; + case 'w': + pPars->fVeryVerbose ^= 1; + break; case 'h': - goto usage; default: - Abc_Print( -2, "Unknown switch.\n"); goto usage; } } @@ -19687,29 +19980,49 @@ int Abc_CommandPdr( Abc_Frame_t * pAbc, int argc, char ** argv ) Abc_Print( -2, "The current network is combinational.\n"); return 0; } - if ( Abc_NtkPoNum(pNtk) != 1 ) + if ( !Abc_NtkIsStrash(pNtk) ) { - Abc_Print( -2, "The number of POs is different from 1.\n"); + Abc_Print( -2, "The current network is not an AIG (run \"strash\").\n"); return 0; } - if ( !Abc_NtkIsStrash(pNtk) ) + if ( pPars->iOutput != -1 && (pPars->iOutput < 0 || pPars->iOutput >= Abc_NtkPoNum(pNtk)) ) { - Abc_Print( -2, "The current network is not an AIG (run \"strash\").\n"); + Abc_Print( -2, "Output index (%d) is incorrect (can be 0 through %d).\n", + pPars->iOutput, Abc_NtkPoNum(pNtk)-1 ); return 0; } + if ( Abc_NtkPoNum(pNtk) != 1 && pPars->fVerbose ) + { + if ( pPars->iOutput == -1 ) + Abc_Print( -2, "The %d property outputs are ORed together.\n", Abc_NtkPoNum(pNtk) ); + else + Abc_Print( -2, "Working on the primary output with zero-based number %d (out of %d).\n", + pPars->iOutput, Abc_NtkPoNum(pNtk) ); + } // run the procedure - pAbc->Status = Abc_NtkDarPdr( pNtk, &pCex ); + pAbc->Status = Abc_NtkDarPdr( pNtk, pPars, &pCex ); pAbc->nFrames = pCex ? pCex->iFrame : -1; Abc_FrameReplaceCex( pAbc, &pCex ); return 0; usage: - Abc_Print( -2, "usage: pdr -h\n" ); - Abc_Print( -2, "\t model checking using property driven reachability (aka ic3)\n" ); - Abc_Print( -2, "\t pioneered by Aaron Bradley (http://ecee.colorado.edu/~bradleya/ic3/)\n" ); - Abc_Print( -2, "\t with improvements by Niklas Een (http://een.se/niklas/)\n" ); - Abc_Print( -2, "\t-h : print the command usage\n"); - return 1; + Abc_Print( -2, "usage: pdr [-OMFCTnRecycle ); + Abc_Print( -2, "\t-F num : number of timeframes explored to stop computation [default = %d]\n", pPars->nFrameMax ); + Abc_Print( -2, "\t-C num : number of conflicts in a SAT call (0 = no limit) [default = %d]\n", pPars->nConfLimit ); + Abc_Print( -2, "\t-T num : approximate timeout in seconds (0 = no limit) [default = %d]\n", pPars->nTimeOut ); + Abc_Print( -2, "\t-r : toggle using more effort in generalization [default = %s]\n", pPars->fTwoRounds? "yes": "no" ); + Abc_Print( -2, "\t-m : toggle using monolythic CNF computation [default = %s]\n", pPars->fMonoCnf? "yes": "no" ); + Abc_Print( -2, "\t-s : toggle creating only shortest counter-examples [default = %s]\n", pPars->fShortest? "yes": "no" ); + Abc_Print( -2, "\t-d : toggle dumping inductive invariant [default = %s]\n", pPars->fDumpInv? "yes": "no" ); + Abc_Print( -2, "\t-v : toggle printing optimization summary [default = %s]\n", pPars->fVerbose? "yes": "no" ); + Abc_Print( -2, "\t-w : toggle printing detailed stats default = %s]\n", pPars->fVeryVerbose? "yes": "no" ); + Abc_Print( -2, "\t-h : print the command usage\n"); + return 1; } /**Function************************************************************* @@ -21267,7 +21580,7 @@ int Abc_CommandAbc8Mfs( Abc_Frame_t * pAbc, int argc, char ** argv ) return 0; usage: - Abc_Print( -2, "usage: *mfs [-WFDMLC ] [-raespvh]\n" ); + Abc_Print( -2, "usage: *mfs [-WFDMLC num] [-raespvh]\n" ); Abc_Print( -2, "\t performs don't-care-based optimization of logic networks\n" ); Abc_Print( -2, "\t-W : the number of levels in the TFO cone (0 <= num) [default = %d]\n", pPars->nWinTfoLevs ); Abc_Print( -2, "\t-F : the max number of fanouts to skip (1 <= num) [default = %d]\n", pPars->nFanoutsMax ); @@ -22475,7 +22788,7 @@ int Abc_CommandAbc8Scorr( Abc_Frame_t * pAbc, int argc, char ** argv ) return 0; usage: - Abc_Print( -2, "usage: *scorr [-PQFCLSDVM ] [-pldsncvh]\n" ); + Abc_Print( -2, "usage: *scorr [-PQFCLSDVM num] [-pldsncvh]\n" ); Abc_Print( -2, "\t performs sequential sweep using K-step induction\n" ); Abc_Print( -2, "\t-P num : max partition size (0 = no partitioning) [default = %d]\n", pPars->nPartSize ); Abc_Print( -2, "\t-Q num : partition overlap (0 = no overlap) [default = %d]\n", pPars->nOverSize ); @@ -23786,7 +24099,7 @@ int Abc_CommandAbc9Sim( Abc_Frame_t * pAbc, int argc, char ** argv ) int c; Gia_ManSimSetDefaultParams( pPars ); Extra_UtilGetoptReset(); - while ( ( c = Extra_UtilGetopt( argc, argv, "WFTmvh" ) ) != EOF ) + while ( ( c = Extra_UtilGetopt( argc, argv, "WFRTmvh" ) ) != EOF ) { switch ( c ) { @@ -23812,6 +24125,17 @@ int Abc_CommandAbc9Sim( Abc_Frame_t * pAbc, int argc, char ** argv ) if ( pPars->nIters < 0 ) goto usage; break; + case 'R': + if ( globalUtilOptind >= argc ) + { + Abc_Print( -1, "Command line switch \"-R\" should be followed by an integer.\n" ); + goto usage; + } + pPars->RandSeed = atoi(argv[globalUtilOptind]); + globalUtilOptind++; + if ( pPars->RandSeed < 0 ) + goto usage; + break; case 'T': if ( globalUtilOptind >= argc ) { @@ -23845,14 +24169,23 @@ int Abc_CommandAbc9Sim( Abc_Frame_t * pAbc, int argc, char ** argv ) Abc_Print( -1, "The network is combinational.\n" ); return 0; } - Gia_ManSimSimulate( pAbc->pGia, pPars ); + pAbc->nFrames = -1; + if ( Gia_ManSimSimulate( pAbc->pGia, pPars ) ) + pAbc->Status = 0; + else + pAbc->Status = -1; + Abc_FrameReplaceCex( pAbc, &pAbc->pGia->pCexSeq ); +// if ( pLogFileName ) +// Abc_NtkWriteLogFile( pLogFileName, pAbc->pCex, pAbc->Status, "&sim" ); return 0; usage: - Abc_Print( -2, "usage: &sim [-WFT ] [-mvh]\n" ); + Abc_Print( -2, "usage: &sim [-WFRT num] [-mvh]\n" ); Abc_Print( -2, "\t performs random simulation of the sequential miter\n" ); + Abc_Print( -2, "\t (if candidate equivalences are defined, performs refinement)\n" ); Abc_Print( -2, "\t-W num : the number of words to simulate [default = %d]\n", pPars->nWords ); Abc_Print( -2, "\t-F num : the number of frames to simulate [default = %d]\n", pPars->nIters ); + Abc_Print( -2, "\t-R num : random number seed (1 <= num <= 10000) [default = %d]\n", pPars->RandSeed ); Abc_Print( -2, "\t-T num : approximate runtime limit in seconds [default = %d]\n", pPars->TimeLimit ); Abc_Print( -2, "\t-m : toggle miter vs. any circuit [default = %s]\n", pPars->fCheckMiter? "miter": "circuit" ); Abc_Print( -2, "\t-v : toggle printing verbose information [default = %s]\n", pPars->fVerbose? "yes": "no" ); @@ -23916,7 +24249,7 @@ int Abc_CommandAbc9Resim( Abc_Frame_t * pAbc, int argc, char ** argv ) return 0; usage: - Abc_Print( -2, "usage: &resim [-F ] [-mvh]\n" ); + Abc_Print( -2, "usage: &resim [-F num] [-mvh]\n" ); Abc_Print( -2, "\t resimulates equivalence classes using counter-example\n" ); Abc_Print( -2, "\t-F num : the number of additinal frames to simulate [default = %d]\n", pPars->nFrames ); Abc_Print( -2, "\t-m : toggle miter vs. any circuit [default = %s]\n", pPars->fCheckMiter? "miter": "circuit" ); @@ -23996,7 +24329,7 @@ int Abc_CommandAbc9SpecI( Abc_Frame_t * pAbc, int argc, char ** argv ) return 0; usage: - Abc_Print( -2, "usage: &speci [-FC ] [-fmvh]\n" ); + Abc_Print( -2, "usage: &speci [-FC num] [-fmvh]\n" ); Abc_Print( -2, "\t refines equivalence classes using speculative reduction\n" ); Abc_Print( -2, "\t-F num : the max number of time frames [default = %d]\n", nFrames ); Abc_Print( -2, "\t-C num : the max number of conflicts at a node [default = %d]\n", nBTLimit ); @@ -24112,7 +24445,7 @@ int Abc_CommandAbc9Equiv( Abc_Frame_t * pAbc, int argc, char ** argv ) return 0; usage: - Abc_Print( -2, "usage: &equiv [-WFRST ] [-smdvh]\n" ); + Abc_Print( -2, "usage: &equiv [-WFRST num] [-smdvh]\n" ); Abc_Print( -2, "\t computes candidate equivalence classes\n" ); Abc_Print( -2, "\t-W num : the number of words to simulate [default = %d]\n", pPars->nWords ); Abc_Print( -2, "\t-F num : the number of frames to simulate [default = %d]\n", pPars->nFrames ); @@ -24242,7 +24575,7 @@ int Abc_CommandAbc9Equiv2( Abc_Frame_t * pAbc, int argc, char ** argv ) return 0; usage: - Abc_Print( -2, "usage: &equiv2 [-FCRTS ] [-xvh]\n" ); + Abc_Print( -2, "usage: &equiv2 [-FCRTS num] [-xvh]\n" ); Abc_Print( -2, "\t computes candidate equivalence classes\n" ); Abc_Print( -2, "\t-F num : the max number of frames for BMC [default = %d]\n", nFramesMax ); Abc_Print( -2, "\t-C num : the max number of conflicts at a node [default = %d]\n", nConfMax ); @@ -24377,7 +24710,7 @@ int Abc_CommandAbc9Semi( Abc_Frame_t * pAbc, int argc, char ** argv ) return 0; usage: - Abc_Print( -2, "usage: &semi [-WRFSMCT ] [-mdvh]\n" ); + Abc_Print( -2, "usage: &semi [-WRFSMCT num] [-mdvh]\n" ); Abc_Print( -2, "\t performs semiformal refinement of equivalence classes\n" ); Abc_Print( -2, "\t-W num : the number of words to simulate [default = %d]\n", pPars->nWords ); Abc_Print( -2, "\t-R num : the max number of rounds to simulate [default = %d]\n", pPars->nRounds ); @@ -27249,7 +27582,7 @@ int Abc_CommandAbc9Reach( Abc_Frame_t * pAbc, int argc, char ** argv ) { Abc_Print( -1, "Abc_CommandAbc9Reach(): The current AIG has no latches.\n" ); return 0; - } + } pAbc->Status = Llb_ManModelCheckGia( pAbc->pGia, pPars ); pAbc->nFrames = pPars->iFrame; Abc_FrameReplaceCex( pAbc, &pAbc->pGia->pCexSeq ); diff --git a/src/base/abci/abcBalance.c b/src/base/abci/abcBalance.c index 9c16bd2c..840fd6f5 100644 --- a/src/base/abci/abcBalance.c +++ b/src/base/abci/abcBalance.c @@ -68,7 +68,7 @@ Abc_Ntk_t * Abc_NtkBalance( Abc_Ntk_t * pNtk, int fDuplicate, int fSelective, in // perform balancing Abc_NtkBalancePerform( pNtk, pNtkAig, fDuplicate, fSelective, fUpdateLevel ); Abc_NtkFinalize( pNtk, pNtkAig ); - Abc_AigCleanup( pNtkAig->pManFunc ); + Abc_AigCleanup( (Abc_Aig_t *)pNtkAig->pManFunc ); // undo the required times if ( fSelective ) { diff --git a/src/base/abci/abcCut.c b/src/base/abci/abcCut.c index f8b27c32..10cacff1 100644 --- a/src/base/abci/abcCut.c +++ b/src/base/abci/abcCut.c @@ -173,7 +173,7 @@ Cut_Man_t * Abc_NtkCuts( Abc_Ntk_t * pNtk, Cut_Params_t * pParams ) // continue; Extra_ProgressBarUpdate( pProgress, i, NULL ); // compute the cuts to the internal node - pList = Abc_NodeGetCuts( p, pObj, pParams->fDag, pParams->fTree ); + pList = (Cut_Cut_t *)Abc_NodeGetCuts( p, pObj, pParams->fDag, pParams->fTree ); if ( pParams->fNpnSave && pList ) { extern void Npn_ManSaveOne( unsigned * puTruth, int nVars ); diff --git a/src/base/abci/abcDar.c b/src/base/abci/abcDar.c index 13205183..85880882 100644 --- a/src/base/abci/abcDar.c +++ b/src/base/abci/abcDar.c @@ -35,6 +35,7 @@ #include "cec.h" #include "csw.h" #include "giaAbs.h" +#include "pdr.h" ABC_NAMESPACE_IMPL_START @@ -2245,14 +2246,6 @@ int Abc_NtkDarSec( Abc_Ntk_t * pNtk1, Abc_Ntk_t * pNtk2, Fra_Sec_t * pSecPar ) return RetValue; } -typedef struct Pdr_Par_t_ Pdr_Par_t; -struct Pdr_Par_t_ -{ - int fAbstract; // perform abstraction - int fVerbose; // enable verbose output - int fVeryVerbose; // enable verbose output -}; - /**Function************************************************************* Synopsis [Gives the current ABC network to AIG manager for processing.] @@ -2264,14 +2257,10 @@ struct Pdr_Par_t_ SeeAlso [] ***********************************************************************/ -int Abc_NtkDarPdr( Abc_Ntk_t * pNtk, Abc_Cex_t ** ppCex ) +int Abc_NtkDarPdr( Abc_Ntk_t * pNtk, Pdr_Par_t * pPars, Abc_Cex_t ** ppCex ) { -// extern void Pdr_ManSetDefaultParams( Pdr_Par_t * pPars ); -// extern int Pdr_ManSolve( Aig_Man_t * pAig, Abc_Cex_t ** ppCex, Pdr_Par_t * pPars ); int RetValue = -1, clk = clock(); - Pdr_Par_t Pars, * pPars = &Pars; Aig_Man_t * pMan; -// Pdr_ManSetDefaultParams( pPars ); *ppCex = NULL; pMan = Abc_NtkToDar( pNtk, 0, 1 ); if ( pMan == NULL ) @@ -2279,7 +2268,18 @@ int Abc_NtkDarPdr( Abc_Ntk_t * pNtk, Abc_Cex_t ** ppCex ) printf( "Converting network into AIG has failed.\n" ); return -1; } -// RetValue = Pdr_ManSolve( pMan, ppCex, pPars ); + // perform ORing the primary outputs + if ( pPars->iOutput == -1 ) + { + Aig_Man_t * pTemp = Saig_ManDupOrpos( pMan ); + RetValue = Pdr_ManSolve( pTemp, pPars, ppCex ); + if ( RetValue == 0 ) + (*ppCex)->iPo = Ssw_SmlFindOutputCounterExample( pMan, *ppCex ); + Aig_ManStop( pTemp ); + } + else + RetValue = Pdr_ManSolve( pMan, pPars, ppCex ); + // output the result if ( RetValue == 1 ) printf( "Property proved. " ); else if ( RetValue == 0 ) @@ -2929,6 +2929,34 @@ Abc_Ntk_t * Abc_NtkDarEnlarge( Abc_Ntk_t * pNtk, int nFrames, int fVerbose ) return pNtkAig; } +/**Function************************************************************* + + Synopsis [Performs targe enlargement.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Abc_Ntk_t * Abc_NtkDarTempor( Abc_Ntk_t * pNtk, int nFrames, int TimeOut, int nConfLimit, int fUseBmc, int fVerbose, int fVeryVerbose ) +{ + extern Aig_Man_t * Saig_ManTempor( Aig_Man_t * pAig, int nFrames, int TimeOut, int nConfLimit, int fUseBmc, int fVerbose, int fVeryVerbose ); + Abc_Ntk_t * pNtkAig; + Aig_Man_t * pMan, * pTemp; + pMan = Abc_NtkToDar( pNtk, 0, 1 ); + if ( pMan == NULL ) + return NULL; + pTemp = Saig_ManTempor( pMan, nFrames, TimeOut, nConfLimit, fUseBmc, fVerbose, fVeryVerbose ); + Aig_ManStop( pMan ); + if ( pTemp == NULL ) + return Abc_NtkDup( pNtk ); + pNtkAig = Abc_NtkFromDarSeqSweep( pNtk, pTemp ); + Aig_ManStop( pTemp ); + return pNtkAig; +} + /**Function************************************************************* Synopsis [Performs induction for property only.] diff --git a/src/base/abci/abcIvy.c b/src/base/abci/abcIvy.c index 759c96a7..979b2a4a 100644 --- a/src/base/abci/abcIvy.c +++ b/src/base/abci/abcIvy.c @@ -508,7 +508,7 @@ int Abc_NtkIvyProve( Abc_Ntk_t ** ppNtk, void * pPars ) // pParams->fUseBdds = 1; // pParams->fBddReorder = 1; // pParams->nTotalBacktrackLimit = 10000; - + // strash the network if it is not strashed already if ( !Abc_NtkIsStrash(pNtk) ) { diff --git a/src/base/cmd/cmdPlugin.c b/src/base/cmd/cmdPlugin.c index be7a9245..7375eb42 100644 --- a/src/base/cmd/cmdPlugin.c +++ b/src/base/cmd/cmdPlugin.c @@ -136,7 +136,7 @@ char * Abc_GetBinaryName( Abc_Frame_t * pAbc, int argc, char ** argv ) { i++; if ( strcmp( pTemp, argv[0] ) == 0 ) - return Vec_PtrEntry( pAbc->vPlugInComBinPairs, i ); + return (char *)Vec_PtrEntry( pAbc->vPlugInComBinPairs, i ); } assert( 0 ); return NULL; diff --git a/src/base/io/ioReadBlifMv.c b/src/base/io/ioReadBlifMv.c index 00b2a5e6..cc8bff17 100644 --- a/src/base/io/ioReadBlifMv.c +++ b/src/base/io/ioReadBlifMv.c @@ -232,6 +232,7 @@ Abc_Ntk_t * Io_ReadBlifMv( char * pFileName, int fBlifMv, int fCheck ) Vec_PtrForEachEntry( char *, vGlobalLtlArray, pLtlProp, i ) Vec_PtrPush( pNtk->vLtlProperties, pLtlProp ); + Vec_PtrFreeP( &vGlobalLtlArray ); return pNtk; } diff --git a/src/base/io/ioReadPla.c b/src/base/io/ioReadPla.c index 85029ce8..63ffa296 100644 --- a/src/base/io/ioReadPla.c +++ b/src/base/io/ioReadPla.c @@ -51,6 +51,7 @@ Abc_Ntk_t * Io_ReadPla( char * pFileName, int fZeros, int fCheck ) // start the file p = Extra_FileReaderAlloc( pFileName, "#", "\n\r", " \t|" ); +// p = Extra_FileReaderAlloc( pFileName, "", "\n\r", " \t|" ); if ( p == NULL ) return NULL; @@ -91,7 +92,7 @@ Abc_Ntk_t * Io_ReadPlaNetwork( Extra_FileReader_t * p, int fZeros ) int nInputs = -1, nOutputs = -1, nProducts = -1; char * pCubeIn, * pCubeOut; int i, k, iLine, nDigits, nCubes; - + // allocate the empty network pNtk = Abc_NtkStartRead( Extra_FileReaderGetFileName(p) ); @@ -103,9 +104,17 @@ Abc_Ntk_t * Io_ReadPlaNetwork( Extra_FileReader_t * p, int fZeros ) Extra_ProgressBarUpdate( pProgress, Extra_FileReaderGetCurPosition(p), NULL ); // if it is the end of file, quit the loop - if ( strcmp( (char *)vTokens->pArray[0], ".e" ) == 0 ) + if ( strncmp( (char *)vTokens->pArray[0], ".e", 2 ) == 0 ) break; + // if it is the model name, get the name + if ( strcmp( (char *)vTokens->pArray[0], ".model" ) == 0 ) + { + ABC_FREE( pNtk->pName ); + pNtk->pName = Extra_UtilStrsav( (char *)vTokens->pArray[1] ); + continue; + } + if ( vTokens->nSize == 1 ) { printf( "%s (line %d): Wrong number of token.\n", diff --git a/src/misc/util/utilFile.c b/src/misc/util/utilFile.c index 09af7b0a..2c40c32c 100644 --- a/src/misc/util/utilFile.c +++ b/src/misc/util/utilFile.c @@ -98,6 +98,7 @@ int tmpFile(const char* prefix, const char* suffix, char** out_name) free(*out_name); *out_name = NULL; }else{ + // Kludge: close(fd); unlink(*out_name); @@ -107,6 +108,11 @@ int tmpFile(const char* prefix, const char* suffix, char** out_name) free(*out_name); *out_name = NULL; } + +// assert( 0 ); + // commented out because had problem with g++ saying that + // close() and unlink() are not defined in the namespace + } return fd; diff --git a/src/opt/mfs/mfsCore.c b/src/opt/mfs/mfsCore.c index bda95d55..72774730 100644 --- a/src/opt/mfs/mfsCore.c +++ b/src/opt/mfs/mfsCore.c @@ -268,10 +268,10 @@ clk = clock(); p->nNodesBad++; return 1; } -clk = clock(); - if ( p->pPars->fGiaSat ) - Abc_NtkMfsConstructGia( p ); -p->timeGia += clock() - clk; +//clk = clock(); +// if ( p->pPars->fGiaSat ) +// Abc_NtkMfsConstructGia( p ); +//p->timeGia += clock() - clk; // solve the SAT problem if ( p->pPars->fPower ) Abc_NtkMfsEdgePower( p, pNode ); @@ -284,8 +284,8 @@ p->timeGia += clock() - clk; Abc_NtkMfsResubNode2( p, pNode ); } p->timeSat += clock() - clk; - if ( p->pPars->fGiaSat ) - Abc_NtkMfsDeconstructGia( p ); +// if ( p->pPars->fGiaSat ) +// Abc_NtkMfsDeconstructGia( p ); return 1; } diff --git a/src/opt/mfs/mfsGia.c b/src/opt/mfs/mfsGia.c index 016b4ae2..af6cc159 100644 --- a/src/opt/mfs/mfsGia.c +++ b/src/opt/mfs/mfsGia.c @@ -271,7 +271,7 @@ int Abc_NtkMfsTryResubOnceGia( Mfs_Man_t * p, int * pCands, int nCands ) assert( Val3 == 1 ); */ // store the counter-example - Vec_IntForEachEntry( p->vProjVars, iVar, i ) + Vec_IntForEachEntry( p->vProjVarsSat, iVar, i ) { pData = (unsigned *)Vec_PtrEntry( p->vDivCexes, i ); iOut = iVar - 2 * p->pCnf->nVars; diff --git a/src/opt/mfs/mfsInt.h b/src/opt/mfs/mfsInt.h index 5611afa0..28a68bd8 100644 --- a/src/opt/mfs/mfsInt.h +++ b/src/opt/mfs/mfsInt.h @@ -61,19 +61,22 @@ struct Mfs_Man_t_ Vec_Ptr_t * vNodes; // the internal nodes of the window Vec_Ptr_t * vDivs; // the divisors of the node Vec_Int_t * vDivLits; // the SAT literals of divisor nodes - Vec_Int_t * vProjVars; // the projection variables + Vec_Int_t * vProjVarsCnf; // the projection variables + Vec_Int_t * vProjVarsSat; // the projection variables // intermediate simulation data Vec_Ptr_t * vDivCexes; // the counter-example for dividors int nDivWords; // the number of words int nCexes; // the numbe rof current counter-examples int nSatCalls; int nSatCexes; +/* // intermediate AIG data Gia_Man_t * pGia; // replica of the AIG in the new package // Gia_Obj_t ** pSat2Gia; // mapping of PO SAT var into internal GIA nodes Tas_Man_t * pTas; // the SAT solver Vec_Int_t * vCex; // the counter-example Vec_Ptr_t * vGiaLits; // literals given as assumptions +*/ // used for bidecomposition Vec_Int_t * vTruth; Bdc_Man_t * pManDec; @@ -87,7 +90,7 @@ struct Mfs_Man_t_ Int_Man_t * pMan; // interpolation manager; Vec_Int_t * vMem; // memory for intermediate SOPs Vec_Vec_t * vLevels; // levelized structure for updating - Vec_Ptr_t * vFanins; // the new set of fanins + Vec_Ptr_t * vMfsFanins; // the new set of fanins int nTotConfLim; // total conflict limit int nTotConfLevel; // total conflicts on this level // switching activity diff --git a/src/opt/mfs/mfsInter.c b/src/opt/mfs/mfsInter.c index 1b3f2415..0934513b 100644 --- a/src/opt/mfs/mfsInter.c +++ b/src/opt/mfs/mfsInter.c @@ -96,13 +96,13 @@ sat_solver * Abc_MfsCreateSolverResub( Mfs_Man_t * p, int * pCands, int nCands, Lits[0] = toLitCond( p->pCnf->pVarNums[pObjPo->Id], fInvert ); // collect the outputs of the divisors - Vec_IntClear( p->vProjVars ); + Vec_IntClear( p->vProjVarsCnf ); Vec_PtrForEachEntryStart( Aig_Obj_t *, p->pAigWin->vPos, pObjPo, i, Aig_ManPoNum(p->pAigWin) - Vec_PtrSize(p->vDivs) ) { assert( p->pCnf->pVarNums[pObjPo->Id] >= 0 ); - Vec_IntPush( p->vProjVars, p->pCnf->pVarNums[pObjPo->Id] ); + Vec_IntPush( p->vProjVarsCnf, p->pCnf->pVarNums[pObjPo->Id] ); } - assert( Vec_IntSize(p->vProjVars) == Vec_PtrSize(p->vDivs) ); + assert( Vec_IntSize(p->vProjVarsCnf) == Vec_PtrSize(p->vDivs) ); // start the solver pSat = sat_solver_new(); @@ -178,7 +178,7 @@ sat_solver * Abc_MfsCreateSolverResub( Mfs_Man_t * p, int * pCands, int nCands, // get the variable number of this divisor i = lit_var( pCands[c] ) - 2 * p->pCnf->nVars; // get the corresponding SAT variable - iVar = Vec_IntEntry( p->vProjVars, i ); + iVar = Vec_IntEntry( p->vProjVarsCnf, i ); // add the corresponding EXOR gate if ( !Abc_MfsSatAddXor( pSat, iVar, iVar + p->pCnf->nVars, 2 * p->pCnf->nVars + i ) ) { @@ -198,15 +198,17 @@ sat_solver * Abc_MfsCreateSolverResub( Mfs_Man_t * p, int * pCands, int nCands, else { // add the clauses for the EXOR gates - and remember their outputs - Vec_IntForEachEntry( p->vProjVars, iVar, i ) + Vec_IntClear( p->vProjVarsSat ); + Vec_IntForEachEntry( p->vProjVarsCnf, iVar, i ) { if ( !Abc_MfsSatAddXor( pSat, iVar, iVar + p->pCnf->nVars, 2 * p->pCnf->nVars + i ) ) { sat_solver_delete( pSat ); return NULL; } - Vec_IntWriteEntry( p->vProjVars, i, 2 * p->pCnf->nVars + i ); + Vec_IntPush( p->vProjVarsSat, 2 * p->pCnf->nVars + i ); } + assert( Vec_IntSize(p->vProjVarsCnf) == Vec_IntSize(p->vProjVarsSat) ); // simplify the solver status = sat_solver_simplify(pSat); if ( status == 0 ) @@ -259,7 +261,7 @@ unsigned * Abc_NtkMfsInterplateTruth( Mfs_Man_t * p, int * pCands, int nCands, i // get the variable number of this divisor i = lit_var( pCands[c] ) - 2 * p->pCnf->nVars; // get the corresponding SAT variable - pGloVars[c] = Vec_IntEntry( p->vProjVars, i ); + pGloVars[c] = Vec_IntEntry( p->vProjVarsCnf, i ); } // derive the interpolant @@ -362,7 +364,7 @@ Hop_Obj_t * Abc_NtkMfsInterplate( Mfs_Man_t * p, int * pCands, int nCands ) // get the variable number of this divisor i = lit_var( pCands[c] ) - 2 * p->pCnf->nVars; // get the corresponding SAT variable - pGloVars[c] = Vec_IntEntry( p->vProjVars, i ); + pGloVars[c] = Vec_IntEntry( p->vProjVarsCnf, i ); } // derive the interpolant diff --git a/src/opt/mfs/mfsMan.c b/src/opt/mfs/mfsMan.c index 74889c45..df331b43 100644 --- a/src/opt/mfs/mfsMan.c +++ b/src/opt/mfs/mfsMan.c @@ -49,14 +49,15 @@ Mfs_Man_t * Mfs_ManAlloc( Mfs_Par_t * pPars ) p = ABC_ALLOC( Mfs_Man_t, 1 ); memset( p, 0, sizeof(Mfs_Man_t) ); p->pPars = pPars; - p->vProjVars = Vec_IntAlloc( 100 ); + p->vProjVarsCnf = Vec_IntAlloc( 100 ); + p->vProjVarsSat = Vec_IntAlloc( 100 ); p->vDivLits = Vec_IntAlloc( 100 ); p->nDivWords = Aig_BitWordNum(p->pPars->nDivMax + MFS_FANIN_MAX); p->vDivCexes = Vec_PtrAllocSimInfo( p->pPars->nDivMax+MFS_FANIN_MAX+1, p->nDivWords ); p->pMan = Int_ManAlloc(); p->vMem = Vec_IntAlloc( 0 ); p->vLevels = Vec_VecStart( 32 ); - p->vFanins = Vec_PtrAlloc( 32 ); + p->vMfsFanins= Vec_PtrAlloc( 32 ); return p; } @@ -201,8 +202,9 @@ void Mfs_ManStop( Mfs_Man_t * p ) Int_ManFree( p->pMan ); Vec_IntFree( p->vMem ); Vec_VecFree( p->vLevels ); - Vec_PtrFree( p->vFanins ); - Vec_IntFree( p->vProjVars ); + Vec_PtrFree( p->vMfsFanins ); + Vec_IntFree( p->vProjVarsCnf ); + Vec_IntFree( p->vProjVarsSat ); Vec_IntFree( p->vDivLits ); Vec_PtrFree( p->vDivCexes ); ABC_FREE( p ); diff --git a/src/opt/mfs/mfsResub.c b/src/opt/mfs/mfsResub.c index 38004089..40cb6198 100644 --- a/src/opt/mfs/mfsResub.c +++ b/src/opt/mfs/mfsResub.c @@ -42,14 +42,14 @@ ABC_NAMESPACE_IMPL_START SeeAlso [] ***********************************************************************/ -void Abc_NtkMfsUpdateNetwork( Mfs_Man_t * p, Abc_Obj_t * pObj, Vec_Ptr_t * vFanins, Hop_Obj_t * pFunc ) +void Abc_NtkMfsUpdateNetwork( Mfs_Man_t * p, Abc_Obj_t * pObj, Vec_Ptr_t * vMfsFanins, Hop_Obj_t * pFunc ) { Abc_Obj_t * pObjNew, * pFanin; int k; // create the new node pObjNew = Abc_NtkCreateNode( pObj->pNtk ); pObjNew->pData = pFunc; - Vec_PtrForEachEntry( Abc_Obj_t *, vFanins, pFanin, k ) + Vec_PtrForEachEntry( Abc_Obj_t *, vMfsFanins, pFanin, k ) Abc_ObjAddFanin( pObjNew, pFanin ); // replace the old node by the new node //printf( "Replacing node " ); Abc_ObjPrint( stdout, pObj ); @@ -103,14 +103,14 @@ int Abc_NtkMfsTryResubOnce( Mfs_Man_t * p, int * pCands, int nCands ) int fVeryVerbose = 0; unsigned * pData; int RetValue, RetValue2 = -1, iVar, i, clk = clock(); - +/* if ( p->pPars->fGiaSat ) { RetValue2 = Abc_NtkMfsTryResubOnceGia( p, pCands, nCands ); p->timeGia += clock() - clk; return RetValue2; } - +*/ p->nSatCalls++; RetValue = sat_solver_solve( p->pSat, pCands, pCands + nCands, (ABC_INT64_T)p->pPars->nBTLimit, (ABC_INT64_T)0, (ABC_INT64_T)0, (ABC_INT64_T)0 ); // assert( RetValue == l_False || RetValue == l_True ); @@ -137,7 +137,7 @@ p->timeGia += clock() - clk; printf( "S " ); p->nSatCexes++; // store the counter-example - Vec_IntForEachEntry( p->vProjVars, iVar, i ) + Vec_IntForEachEntry( p->vProjVarsSat, iVar, i ) { pData = (unsigned *)Vec_PtrEntry( p->vDivCexes, i ); if ( !sat_solver_var_value( p->pSat, iVar ) ) // remove 0s!!! @@ -186,14 +186,14 @@ int Abc_NtkMfsSolveSatResub( Mfs_Man_t * p, Abc_Obj_t * pNode, int iFanin, int f // try fanins without the critical fanin nCands = 0; - Vec_PtrClear( p->vFanins ); + Vec_PtrClear( p->vMfsFanins ); Abc_ObjForEachFanin( pNode, pFanin, i ) { if ( i == iFanin ) continue; - Vec_PtrPush( p->vFanins, pFanin ); + Vec_PtrPush( p->vMfsFanins, pFanin ); iVar = Vec_PtrSize(p->vDivs) - Abc_ObjFaninNum(pNode) + i; - pCands[nCands++] = toLitCond( Vec_IntEntry( p->vProjVars, iVar ), 1 ); + pCands[nCands++] = toLitCond( Vec_IntEntry( p->vProjVarsSat, iVar ), 1 ); } RetValue = Abc_NtkMfsTryResubOnce( p, pCands, nCands ); if ( RetValue == -1 ) @@ -212,7 +212,7 @@ clk = clock(); if ( pFunc == NULL ) return 0; // update the network - Abc_NtkMfsUpdateNetwork( p, pNode, p->vFanins, pFunc ); + Abc_NtkMfsUpdateNetwork( p, pNode, p->vMfsFanins, pFunc ); p->timeInt += clock() - clk; return 1; } @@ -269,7 +269,7 @@ p->timeInt += clock() - clk; if ( iVar == Vec_PtrSize(p->vDivs)-Abc_ObjFaninNum(pNode) ) return 0; - pCands[nCands] = toLitCond( Vec_IntEntry(p->vProjVars, iVar), 1 ); + pCands[nCands] = toLitCond( Vec_IntEntry(p->vProjVarsSat, iVar), 1 ); RetValue = Abc_NtkMfsTryResubOnce( p, pCands, nCands+1 ); if ( RetValue == -1 ) return 0; @@ -287,8 +287,8 @@ clk = clock(); if ( pFunc == NULL ) return 0; // update the network - Vec_PtrPush( p->vFanins, Vec_PtrEntry(p->vDivs, iVar) ); - Abc_NtkMfsUpdateNetwork( p, pNode, p->vFanins, pFunc ); + Vec_PtrPush( p->vMfsFanins, Vec_PtrEntry(p->vDivs, iVar) ); + Abc_NtkMfsUpdateNetwork( p, pNode, p->vMfsFanins, pFunc ); p->timeInt += clock() - clk; return 1; } @@ -334,14 +334,14 @@ int Abc_NtkMfsSolveSatResub2( Mfs_Man_t * p, Abc_Obj_t * pNode, int iFanin, int // try fanins without the critical fanin nCands = 0; - Vec_PtrClear( p->vFanins ); + Vec_PtrClear( p->vMfsFanins ); Abc_ObjForEachFanin( pNode, pFanin, i ) { if ( i == iFanin || i == iFanin2 ) continue; - Vec_PtrPush( p->vFanins, pFanin ); + Vec_PtrPush( p->vMfsFanins, pFanin ); iVar = Vec_PtrSize(p->vDivs) - Abc_ObjFaninNum(pNode) + i; - pCands[nCands++] = toLitCond( Vec_IntEntry( p->vProjVars, iVar ), 1 ); + pCands[nCands++] = toLitCond( Vec_IntEntry( p->vProjVarsSat, iVar ), 1 ); } RetValue = Abc_NtkMfsTryResubOnce( p, pCands, nCands ); if ( RetValue == -1 ) @@ -358,7 +358,7 @@ clk = clock(); if ( pFunc == NULL ) return 0; // update the network - Abc_NtkMfsUpdateNetwork( p, pNode, p->vFanins, pFunc ); + Abc_NtkMfsUpdateNetwork( p, pNode, p->vMfsFanins, pFunc ); p->timeInt += clock() - clk; return 1; } @@ -435,8 +435,8 @@ p->timeInt += clock() - clk; if ( iVar == Vec_PtrSize(p->vDivs)-Abc_ObjFaninNum(pNode) ) return 0; - pCands[nCands] = toLitCond( Vec_IntEntry(p->vProjVars, iVar2), 1 ); - pCands[nCands+1] = toLitCond( Vec_IntEntry(p->vProjVars, iVar), 1 ); + pCands[nCands] = toLitCond( Vec_IntEntry(p->vProjVarsSat, iVar2), 1 ); + pCands[nCands+1] = toLitCond( Vec_IntEntry(p->vProjVarsSat, iVar), 1 ); RetValue = Abc_NtkMfsTryResubOnce( p, pCands, nCands+2 ); if ( RetValue == -1 ) return 0; @@ -452,10 +452,10 @@ clk = clock(); if ( pFunc == NULL ) return 0; // update the network - Vec_PtrPush( p->vFanins, Vec_PtrEntry(p->vDivs, iVar2) ); - Vec_PtrPush( p->vFanins, Vec_PtrEntry(p->vDivs, iVar) ); - assert( Vec_PtrSize(p->vFanins) == nCands + 2 ); - Abc_NtkMfsUpdateNetwork( p, pNode, p->vFanins, pFunc ); + Vec_PtrPush( p->vMfsFanins, Vec_PtrEntry(p->vDivs, iVar2) ); + Vec_PtrPush( p->vMfsFanins, Vec_PtrEntry(p->vDivs, iVar) ); + assert( Vec_PtrSize(p->vMfsFanins) == nCands + 2 ); + Abc_NtkMfsUpdateNetwork( p, pNode, p->vMfsFanins, pFunc ); p->timeInt += clock() - clk; return 1; } diff --git a/src/opt/mfs/mfsSat.c b/src/opt/mfs/mfsSat.c index c5806f2a..37ee2b39 100644 --- a/src/opt/mfs/mfsSat.c +++ b/src/opt/mfs/mfsSat.c @@ -63,7 +63,7 @@ int Abc_NtkMfsSolveSat_iter( Mfs_Man_t * p ) p->nCares++; // add SAT assignment to the solver Mint = 0; - Vec_IntForEachEntry( p->vProjVars, iVar, b ) + Vec_IntForEachEntry( p->vProjVarsSat, iVar, b ) { Lits[b] = toLit( iVar ); if ( sat_solver_var_value( p->pSat, iVar ) ) @@ -75,7 +75,7 @@ int Abc_NtkMfsSolveSat_iter( Mfs_Man_t * p ) assert( !Aig_InfoHasBit(p->uCare, Mint) ); Aig_InfoSetBit( p->uCare, Mint ); // add the blocking clause - RetValue = sat_solver_addclause( p->pSat, Lits, Lits + Vec_IntSize(p->vProjVars) ); + RetValue = sat_solver_addclause( p->pSat, Lits, Lits + Vec_IntSize(p->vProjVarsSat) ); if ( RetValue == 0 ) return 0; return 1; @@ -97,15 +97,15 @@ int Abc_NtkMfsSolveSat( Mfs_Man_t * p, Abc_Obj_t * pNode ) Aig_Obj_t * pObjPo; int RetValue, i; // collect projection variables - Vec_IntClear( p->vProjVars ); + Vec_IntClear( p->vProjVarsSat ); Vec_PtrForEachEntryStart( Aig_Obj_t *, p->pAigWin->vPos, pObjPo, i, Aig_ManPoNum(p->pAigWin) - Abc_ObjFaninNum(pNode) ) { assert( p->pCnf->pVarNums[pObjPo->Id] >= 0 ); - Vec_IntPush( p->vProjVars, p->pCnf->pVarNums[pObjPo->Id] ); + Vec_IntPush( p->vProjVarsSat, p->pCnf->pVarNums[pObjPo->Id] ); } // prepare the truth table of care set - p->nFanins = Vec_IntSize( p->vProjVars ); + p->nFanins = Vec_IntSize( p->vProjVarsSat ); p->nWords = Aig_TruthWordNum( p->nFanins ); memset( p->uCare, 0, sizeof(unsigned) * p->nWords ); diff --git a/src/opt/mfs/module.make b/src/opt/mfs/module.make index bafc1ce5..544accec 100644 --- a/src/opt/mfs/module.make +++ b/src/opt/mfs/module.make @@ -1,6 +1,5 @@ SRC += src/opt/mfs/mfsCore.c \ src/opt/mfs/mfsDiv.c \ - src/opt/mfs/mfsGia.c \ src/opt/mfs/mfsInter.c \ src/opt/mfs/mfsMan.c \ src/opt/mfs/mfsResub.c \ diff --git a/src/sat/bsat/satSolver.c b/src/sat/bsat/satSolver.c index 1f02adec..1ad903c1 100644 --- a/src/sat/bsat/satSolver.c +++ b/src/sat/bsat/satSolver.c @@ -28,6 +28,9 @@ OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWA #include "satStore.h" ABC_NAMESPACE_IMPL_START + +#define SAT_USE_ANALYZE_FINAL + /* extern int Sto_ManAddClause( void * p, lit * pBeg, lit * pEnd ); extern int Sto_ManAddClause( void * p, lit * pBeg, lit * pEnd ); @@ -40,8 +43,10 @@ extern int Sto_ManChangeLastClause( void * p ); extern void Sto_ManMarkRoots( void * p ); extern void Sto_ManMarkClausesA( void * p ); */ + //#define SAT_USE_SYSTEM_MEMORY_MANAGEMENT + //================================================================================================= // Debug: @@ -457,14 +462,14 @@ static inline int enqueue(sat_solver* s, lit l, clause* from) } -static inline void assume(sat_solver* s, lit l){ +static inline int assume(sat_solver* s, lit l){ assert(s->qtail == s->qhead); assert(s->assigns[lit_var(l)] == l_Undef); #ifdef VERBOSEDEBUG printf(L_IND"assume("L_LIT")\n", L_ind, L_lit(l)); #endif veci_push(&s->trail_lim,s->qtail); - enqueue(s,l,(clause*)0); + return enqueue(s,l,(clause*)0); } @@ -624,52 +629,73 @@ static int sat_solver_lit_removable(sat_solver* s, lit l, int minl) | stores the result in 'out_conflict'. |________________________________________________________________________________________________@*/ /* -void Solver::analyzeFinal(Lit p, vec& out_conflict) +void Solver::analyzeFinal(Clause* confl, bool skip_first) { - out_conflict.clear(); - out_conflict.push(p); - - if (decisionLevel() == 0) - return; - - seen[var(p)] = 1; + // -- NOTE! This code is relatively untested. Please report bugs! + conflict.clear(); + if (root_level == 0) return; + + vec& seen = analyze_seen; + for (int i = skip_first ? 1 : 0; i < confl->size(); i++){ + Var x = var((*confl)[i]); + if (level[x] > 0) + seen[x] = 1; + } - for (int i = trail.size()-1; i >= trail_lim[0]; i--){ - Var x = var(trail[i]); + int start = (root_level >= trail_lim.size()) ? trail.size()-1 : trail_lim[root_level]; + for (int i = start; i >= trail_lim[0]; i--){ + Var x = var(trail[i]); if (seen[x]){ - if (reason(x) == GClause_NULL){ - assert(level(x) > 0); - out_conflict.push(~trail[i]); + GClause r = reason[x]; + if (r == GClause_NULL){ + assert(level[x] > 0); + conflict.push(~trail[i]); }else{ - Clause& c = ca.deref(smartReason(x)); - for (int j = 1; j < c.size(); j++) - if (level(var(c[j])) > 0) - seen[var(c[j])] = 1; + if (r.isLit()){ + Lit p = r.lit(); + if (level[var(p)] > 0) + seen[var(p)] = 1; + }else{ + Clause& c = *r.clause(); + for (int j = 1; j < c.size(); j++) + if (level[var(c[j])] > 0) + seen[var(c[j])] = 1; + } } seen[x] = 0; } } - - seen[var(p)] = 0; } */ -static void sat_solver_analyze_final(sat_solver* s, lit p, veci* out_conflict) +#ifdef SAT_USE_ANALYZE_FINAL + +static void sat_solver_analyze_final(sat_solver* s, clause* conf, int skip_first) { - int i, j; - veci_resize(out_conflict,0); -// veci_push(out_conflict,p); // do not write conflict literal - if ( sat_solver_dlevel(s) == 0 ) + int i, j, start; + veci_resize(&s->conf_final,0); + if ( s->root_level == 0 ) return; assert( veci_size(&s->tagged) == 0 ); - assert( s->tags[lit_var(p)] == l_Undef ); - s->tags[lit_var(p)] = l_True; - for (i = s->qtail-1; i >= (veci_begin(&s->trail_lim))[0]; i--){ +// assert( s->tags[lit_var(p)] == l_Undef ); +// s->tags[lit_var(p)] = l_True; + for (i = skip_first ? 1 : 0; i < clause_size(conf); i++) + { + int x = lit_var(clause_begin(conf)[i]); + if (s->levels[x] > 0) + { + s->tags[x] = l_True; + veci_push(&s->tagged,x); + } + } + + start = (s->root_level >= veci_size(&s->trail_lim))? s->qtail-1 : (veci_begin(&s->trail_lim))[s->root_level]; + for (i = start; i >= (veci_begin(&s->trail_lim))[0]; i--){ int x = lit_var(s->trail[i]); if (s->tags[x] == l_True){ if (s->reasons[x] == NULL){ assert(s->levels[x] > 0); - veci_push(out_conflict,lit_neg(s->trail[i])); + veci_push(&s->conf_final,lit_neg(s->trail[i])); }else{ clause* c = s->reasons[x]; if (clause_is_lit(c)){ @@ -698,6 +724,8 @@ static void sat_solver_analyze_final(sat_solver* s, lit p, veci* out_conflict) veci_resize(&s->tagged,0); } +#endif + static void sat_solver_analyze(sat_solver* s, clause* c, veci* learnt) { @@ -976,8 +1004,9 @@ static lbool sat_solver_search(sat_solver* s, ABC_INT64_T nof_conflicts, ABC_INT #endif s->stats.conflicts++; conflictC++; if (sat_solver_dlevel(s) == s->root_level){ - lit p = clause_is_lit(confl)? clause_read_lit(confl) : clause_begin(confl)[0]; -// sat_solver_analyze_final(s, lit_neg(p), &s->conf_final); +#ifdef SAT_USE_ANALYZE_FINAL + sat_solver_analyze_final(s, confl, 0); +#endif veci_delete(&learnt_clause); return l_False; } @@ -988,6 +1017,10 @@ static lbool sat_solver_search(sat_solver* s, ABC_INT64_T nof_conflicts, ABC_INT blevel = s->root_level > blevel ? s->root_level : blevel; sat_solver_canceluntil(s,blevel); sat_solver_record(s,&learnt_clause); +#ifdef SAT_USE_ANALYZE_FINAL +// if (learnt_clause.size() == 1) level[var(learnt_clause[0])] = 0; // (this is ugly (but needed for 'analyzeFinal()') -- in future versions, we will backtrack past the 'root_level' and redo the assumptions) + if ( learnt_clause.size == 1 ) s->levels[lit_var(learnt_clause.ptr[0])] = 0; +#endif act_var_decay(s); act_clause_decay(s); @@ -1340,25 +1373,107 @@ int sat_solver_solve(sat_solver* s, lit* begin, lit* end, ABC_INT64_T nConfLimit if ( nInsLimitGlobal && (s->nInsLimit == 0 || s->nInsLimit > nInsLimitGlobal) ) s->nInsLimit = nInsLimitGlobal; +#ifndef SAT_USE_ANALYZE_FINAL + //printf("solve: "); printlits(begin, end); printf("\n"); for (i = begin; i < end; i++){ switch (lit_sign(*i) ? -values[lit_var(*i)] : values[lit_var(*i)]){ - case 1: /* l_True: */ + case 1: // l_True: break; - case 0: /* l_Undef */ + case 0: // l_Undef assume(s, *i); if (sat_solver_propagate(s) == NULL) break; // fallthrough - case -1: /* l_False */ + case -1: // l_False sat_solver_canceluntil(s, 0); return l_False; } } - s->nCalls2++; - s->root_level = sat_solver_dlevel(s); +#endif + +/* + // Perform assumptions: + root_level = assumps.size(); + for (int i = 0; i < assumps.size(); i++){ + Lit p = assumps[i]; + assert(var(p) < nVars()); + if (!assume(p)){ + GClause r = reason[var(p)]; + if (r != GClause_NULL){ + Clause* confl; + if (r.isLit()){ + confl = propagate_tmpbin; + (*confl)[1] = ~p; + (*confl)[0] = r.lit(); + }else + confl = r.clause(); + analyzeFinal(confl, true); + conflict.push(~p); + }else + conflict.clear(), + conflict.push(~p); + cancelUntil(0); + return false; } + Clause* confl = propagate(); + if (confl != NULL){ + analyzeFinal(confl), assert(conflict.size() > 0); + cancelUntil(0); + return false; } + } + assert(root_level == decisionLevel()); +*/ + +#ifdef SAT_USE_ANALYZE_FINAL + // Perform assumptions: + s->root_level = end - begin; + for ( i = begin; i < end; i++ ) + { + lit p = *i; + assert(lit_var(p) < s->size); + veci_push(&s->trail_lim,s->qtail); + if (!enqueue(s,p,(clause*)0)) + { + clause * r = s->reasons[lit_var(p)]; + if (r != NULL) + { + clause* confl; + if (clause_is_lit(r)) + { + confl = s->binary; + (clause_begin(confl))[1] = lit_neg(p); + (clause_begin(confl))[0] = clause_read_lit(r); + } + else + confl = r; + sat_solver_analyze_final(s, confl, 1); + veci_push(&s->conf_final, lit_neg(p)); + } + else + { + veci_resize(&s->conf_final,0); + veci_push(&s->conf_final, lit_neg(p)); + } + sat_solver_canceluntil(s, 0); + return l_False; + } + else + { + clause* confl = sat_solver_propagate(s); + if (confl != NULL){ + sat_solver_analyze_final(s, confl, 0); + assert(s->conf_final.size > 0); + sat_solver_canceluntil(s, 0); + return l_False; } + } + } + assert(s->root_level == sat_solver_dlevel(s)); +#endif + + s->nCalls2++; + if (s->verbosity >= 1){ printf("==================================[MINISAT]===================================\n"); printf("| Conflicts | ORIGINAL | LEARNT | Progress |\n"); diff --git a/src/sat/bsat/satSolver.h b/src/sat/bsat/satSolver.h index f474fc1d..2b148328 100644 --- a/src/sat/bsat/satSolver.h +++ b/src/sat/bsat/satSolver.h @@ -85,8 +85,6 @@ extern int sat_solver_nconflicts(sat_solver* s); extern void sat_solver_setnvars(sat_solver* s,int n); -extern int sat_solver_final(sat_solver* s, int ** ppArray); - struct stats_t { ABC_INT64_T starts, decisions, propagations, inspects, conflicts; -- cgit v1.2.3