diff options
| author | Alan Mishchenko <alanmi@berkeley.edu> | 2005-08-07 08:01:00 -0700 |
|---|---|---|
| committer | Alan Mishchenko <alanmi@berkeley.edu> | 2005-08-07 08:01:00 -0700 |
| commit | bd640142e0fe2260e3d28e187f21a36d3cc8e08f (patch) | |
| tree | 1d834271b729e18017519631edc73335b6d32553 | |
| parent | d0e834d1a615f8e0e9d04c2ac97811f63562bd0b (diff) | |
| download | abc-bd640142e0fe2260e3d28e187f21a36d3cc8e08f.tar.gz abc-bd640142e0fe2260e3d28e187f21a36d3cc8e08f.tar.bz2 abc-bd640142e0fe2260e3d28e187f21a36d3cc8e08f.zip | |
Version abc50807
51 files changed, 2618 insertions, 454 deletions
@@ -7,9 +7,10 @@ CP := cp PROG := abc MODULES := src/base/abc src/base/cmd src/base/io src/base/main \ - src/bdd/cudd src/bdd/epd src/bdd/mtr src/bdd/parse \ + src/bdd/cudd src/bdd/dsd src/bdd/epd src/bdd/mtr src/bdd/parse src/bdd/reo \ src/map/fpga src/map/mapper src/map/mio src/map/super \ src/misc/extra src/misc/st src/misc/util src/misc/vec \ + src/opt/fxu \ src/sat/asat src/sat/fraig src/sat/msat \ src/seq \ src/sop/ft src/sop/mvc @@ -189,10 +189,18 @@ SOURCE=.\src\base\abc\abcRenode.c # End Source File # Begin Source File +SOURCE=.\src\base\abc\abcRes.c +# End Source File +# Begin Source File + SOURCE=.\src\base\abc\abcSat.c # End Source File # Begin Source File +SOURCE=.\src\base\abc\abcShow.c +# End Source File +# Begin Source File + SOURCE=.\src\base\abc\abcSop.c # End Source File # Begin Source File @@ -209,6 +217,10 @@ SOURCE=.\src\base\abc\abcTiming.c # End Source File # Begin Source File +SOURCE=.\src\base\abc\abcUnreach.c +# End Source File +# Begin Source File + SOURCE=.\src\base\abc\abcUtil.c # End Source File # Begin Source File Binary files differ@@ -6,13 +6,13 @@ --------------------Configuration: abc - Win32 Debug-------------------- </h3> <h3>Command Lines</h3> -Creating temporary file "C:\DOCUME~1\alanmi\LOCALS~1\Temp\RSP448.tmp" with contents +Creating temporary file "C:\DOCUME~1\alanmi\LOCALS~1\Temp\RSP84B.tmp" with contents [ /nologo /MLd /W3 /Gm /GX /ZI /Od /I "src\base\abc" /I "src\base\cmd" /I "src\base\io" /I "src\base\main" /I "src\bdd\cudd" /I "src\bdd\epd" /I "src\bdd\mtr" /I "src\bdd\parse" /I "src\bdd\dsd" /I "src\bdd\reo" /I "src\sop\mvc" /I "src\sop\ft" /I "src\sat\asat" /I "src\sat\msat" /I "src\sat\fraig" /I "src\opt\fxa" /I "src\opt\fxu" /I "src\map\fpga" /I "src\map\mapper" /I "src\map\mio" /I "src\map\super" /I "src\misc\extra" /I "src\misc\st" /I "src\misc\util" /I "src\misc\vec" /D "WIN32" /D "_DEBUG" /D "_CONSOLE" /D "_MBCS" /D "__STDC__" /D "HAVE_ASSERT_H" /FR"Debug/" /Fp"Debug/abc.pch" /YX /Fo"Debug/" /Fd"Debug/" /FD /GZ /c -"C:\_projects\abc\src\opt\fxu\fxu.c" +"C:\_projects\abc\src\base\abc\abcRes.c" ] -Creating command line "cl.exe @C:\DOCUME~1\alanmi\LOCALS~1\Temp\RSP448.tmp" -Creating temporary file "C:\DOCUME~1\alanmi\LOCALS~1\Temp\RSP449.tmp" with contents +Creating command line "cl.exe @C:\DOCUME~1\alanmi\LOCALS~1\Temp\RSP84B.tmp" +Creating temporary file "C:\DOCUME~1\alanmi\LOCALS~1\Temp\RSP84C.tmp" with contents [ 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 /incremental:yes /pdb:"Debug/abc.pdb" /debug /machine:I386 /out:"_TEST/abc.exe" /pdbtype:sept .\Debug\abc.obj @@ -27,6 +27,7 @@ kernel32.lib user32.lib gdi32.lib winspool.lib comdlg32.lib advapi32.lib shell32 .\Debug\abcFpga.obj .\Debug\abcFraig.obj .\Debug\abcFunc.obj +.\Debug\abcFxu.obj .\Debug\abcLatch.obj .\Debug\abcMap.obj .\Debug\abcMinBase.obj @@ -36,11 +37,14 @@ kernel32.lib user32.lib gdi32.lib winspool.lib comdlg32.lib advapi32.lib shell32 .\Debug\abcPrint.obj .\Debug\abcRefs.obj .\Debug\abcRenode.obj +.\Debug\abcRes.obj .\Debug\abcSat.obj +.\Debug\abcShow.obj .\Debug\abcSop.obj .\Debug\abcStrash.obj .\Debug\abcSweep.obj .\Debug\abcTiming.obj +.\Debug\abcUnreach.obj .\Debug\abcUtil.obj .\Debug\abcVerify.obj .\Debug\cmd.obj @@ -188,6 +192,18 @@ kernel32.lib user32.lib gdi32.lib winspool.lib comdlg32.lib advapi32.lib shell32 .\Debug\fraigTable.obj .\Debug\fraigUtil.obj .\Debug\fraigVec.obj +.\Debug\fxu.obj +.\Debug\fxuCreate.obj +.\Debug\fxuHeapD.obj +.\Debug\fxuHeapS.obj +.\Debug\fxuList.obj +.\Debug\fxuMatrix.obj +.\Debug\fxuPair.obj +.\Debug\fxuPrint.obj +.\Debug\fxuReduce.obj +.\Debug\fxuSelect.obj +.\Debug\fxuSingle.obj +.\Debug\fxuUpdate.obj .\Debug\fpga.obj .\Debug\fpgaCore.obj .\Debug\fpgaCreate.obj @@ -242,26 +258,13 @@ kernel32.lib user32.lib gdi32.lib winspool.lib comdlg32.lib advapi32.lib shell32 .\Debug\safe_mem.obj .\Debug\strsav.obj .\Debug\texpand.obj -.\Debug\fxuUpdate.obj -.\Debug\fxu.obj -.\Debug\fxuCreate.obj -.\Debug\fxuHeapD.obj -.\Debug\fxuHeapS.obj -.\Debug\fxuList.obj -.\Debug\fxuMatrix.obj -.\Debug\fxuPair.obj -.\Debug\fxuPrint.obj -.\Debug\fxuReduce.obj -.\Debug\fxuSelect.obj -.\Debug\fxuSingle.obj -.\Debug\abcFxu.obj ] -Creating command line "link.exe @C:\DOCUME~1\alanmi\LOCALS~1\Temp\RSP449.tmp" +Creating command line "link.exe @C:\DOCUME~1\alanmi\LOCALS~1\Temp\RSP84C.tmp" <h3>Output Window</h3> Compiling... -fxu.c +abcRes.c Linking... -Creating temporary file "C:\DOCUME~1\alanmi\LOCALS~1\Temp\RSP44A.tmp" with contents +Creating temporary file "C:\DOCUME~1\alanmi\LOCALS~1\Temp\RSP84D.tmp" with contents [ /nologo /o"Debug/abc.bsc" .\Debug\abc.sbr @@ -276,6 +279,7 @@ Creating temporary file "C:\DOCUME~1\alanmi\LOCALS~1\Temp\RSP44A.tmp" with conte .\Debug\abcFpga.sbr .\Debug\abcFraig.sbr .\Debug\abcFunc.sbr +.\Debug\abcFxu.sbr .\Debug\abcLatch.sbr .\Debug\abcMap.sbr .\Debug\abcMinBase.sbr @@ -285,11 +289,14 @@ Creating temporary file "C:\DOCUME~1\alanmi\LOCALS~1\Temp\RSP44A.tmp" with conte .\Debug\abcPrint.sbr .\Debug\abcRefs.sbr .\Debug\abcRenode.sbr +.\Debug\abcRes.sbr .\Debug\abcSat.sbr +.\Debug\abcShow.sbr .\Debug\abcSop.sbr .\Debug\abcStrash.sbr .\Debug\abcSweep.sbr .\Debug\abcTiming.sbr +.\Debug\abcUnreach.sbr .\Debug\abcUtil.sbr .\Debug\abcVerify.sbr .\Debug\cmd.sbr @@ -437,6 +444,18 @@ Creating temporary file "C:\DOCUME~1\alanmi\LOCALS~1\Temp\RSP44A.tmp" with conte .\Debug\fraigTable.sbr .\Debug\fraigUtil.sbr .\Debug\fraigVec.sbr +.\Debug\fxu.sbr +.\Debug\fxuCreate.sbr +.\Debug\fxuHeapD.sbr +.\Debug\fxuHeapS.sbr +.\Debug\fxuList.sbr +.\Debug\fxuMatrix.sbr +.\Debug\fxuPair.sbr +.\Debug\fxuPrint.sbr +.\Debug\fxuReduce.sbr +.\Debug\fxuSelect.sbr +.\Debug\fxuSingle.sbr +.\Debug\fxuUpdate.sbr .\Debug\fpga.sbr .\Debug\fpgaCore.sbr .\Debug\fpgaCreate.sbr @@ -490,21 +509,8 @@ Creating temporary file "C:\DOCUME~1\alanmi\LOCALS~1\Temp\RSP44A.tmp" with conte .\Debug\pathsearch.sbr .\Debug\safe_mem.sbr .\Debug\strsav.sbr -.\Debug\texpand.sbr -.\Debug\fxuUpdate.sbr -.\Debug\fxu.sbr -.\Debug\fxuCreate.sbr -.\Debug\fxuHeapD.sbr -.\Debug\fxuHeapS.sbr -.\Debug\fxuList.sbr -.\Debug\fxuMatrix.sbr -.\Debug\fxuPair.sbr -.\Debug\fxuPrint.sbr -.\Debug\fxuReduce.sbr -.\Debug\fxuSelect.sbr -.\Debug\fxuSingle.sbr -.\Debug\abcFxu.sbr] -Creating command line "bscmake.exe @C:\DOCUME~1\alanmi\LOCALS~1\Temp\RSP44A.tmp" +.\Debug\texpand.sbr] +Creating command line "bscmake.exe @C:\DOCUME~1\alanmi\LOCALS~1\Temp\RSP84D.tmp" Creating browse info file... <h3>Output Window</h3> @@ -1,5 +1,6 @@ alias b balance alias clp collapse +alias esd ext_seq_dcs alias f fraig alias fs fraig_sweep alias pf print_factor diff --git a/src/base/abc/abc.c b/src/base/abc/abc.c index 1179e400..b8c9a3ef 100644 --- a/src/base/abc/abc.c +++ b/src/base/abc/abc.c @@ -28,41 +28,45 @@ /// DECLARATIONS /// //////////////////////////////////////////////////////////////////////// -static int Ntk_CommandPrintStats ( Abc_Frame_t * pAbc, int argc, char ** argv ); -static int Ntk_CommandPrintIo ( Abc_Frame_t * pAbc, int argc, char ** argv ); -static int Ntk_CommandPrintFanio ( Abc_Frame_t * pAbc, int argc, char ** argv ); -static int Ntk_CommandPrintFactor ( Abc_Frame_t * pAbc, int argc, char ** argv ); - -static int Ntk_CommandCollapse ( Abc_Frame_t * pAbc, int argc, char ** argv ); -static int Ntk_CommandStrash ( Abc_Frame_t * pAbc, int argc, char ** argv ); -static int Ntk_CommandBalance ( Abc_Frame_t * pAbc, int argc, char ** argv ); -static int Ntk_CommandRenode ( Abc_Frame_t * pAbc, int argc, char ** argv ); -static int Ntk_CommandCleanup ( Abc_Frame_t * pAbc, int argc, char ** argv ); -static int Ntk_CommandFx ( Abc_Frame_t * pAbc, int argc, char ** argv ); - -static int Ntk_CommandLogic ( Abc_Frame_t * pAbc, int argc, char ** argv ); -static int Ntk_CommandMiter ( Abc_Frame_t * pAbc, int argc, char ** argv ); -static int Ntk_CommandFrames ( Abc_Frame_t * pAbc, int argc, char ** argv ); -static int Ntk_CommandSop ( Abc_Frame_t * pAbc, int argc, char ** argv ); -static int Ntk_CommandBdd ( Abc_Frame_t * pAbc, int argc, char ** argv ); -static int Ntk_CommandSat ( Abc_Frame_t * pAbc, int argc, char ** argv ); - -static int Ntk_CommandFraig ( Abc_Frame_t * pAbc, int argc, char ** argv ); -static int Ntk_CommandFraigTrust ( Abc_Frame_t * pAbc, int argc, char ** argv ); -static int Ntk_CommandFraigStore ( Abc_Frame_t * pAbc, int argc, char ** argv ); -static int Ntk_CommandFraigRestore ( Abc_Frame_t * pAbc, int argc, char ** argv ); -static int Ntk_CommandFraigClean ( Abc_Frame_t * pAbc, int argc, char ** argv ); -static int Ntk_CommandFraigSweep ( Abc_Frame_t * pAbc, int argc, char ** argv ); - -static int Ntk_CommandMap ( Abc_Frame_t * pAbc, int argc, char ** argv ); -static int Ntk_CommandUnmap ( Abc_Frame_t * pAbc, int argc, char ** argv ); -static int Ntk_CommandAttach ( Abc_Frame_t * pAbc, int argc, char ** argv ); -static int Ntk_CommandSuperChoice ( Abc_Frame_t * pAbc, int argc, char ** argv ); - -static int Ntk_CommandFpga ( Abc_Frame_t * pAbc, int argc, char ** argv ); - -static int Ntk_CommandCec ( Abc_Frame_t * pAbc, int argc, char ** argv ); -static int Ntk_CommandSec ( Abc_Frame_t * pAbc, int argc, char ** argv ); +static int Abc_CommandPrintStats ( Abc_Frame_t * pAbc, int argc, char ** argv ); +static int Abc_CommandPrintIo ( Abc_Frame_t * pAbc, int argc, char ** argv ); +static int Abc_CommandPrintFanio ( Abc_Frame_t * pAbc, int argc, char ** argv ); +static int Abc_CommandPrintFactor ( Abc_Frame_t * pAbc, int argc, char ** argv ); +static int Abc_CommandShowBdd ( Abc_Frame_t * pAbc, int argc, char ** argv ); + +static int Abc_CommandCollapse ( Abc_Frame_t * pAbc, int argc, char ** argv ); +static int Abc_CommandStrash ( Abc_Frame_t * pAbc, int argc, char ** argv ); +static int Abc_CommandBalance ( Abc_Frame_t * pAbc, int argc, char ** argv ); +static int Abc_CommandRenode ( Abc_Frame_t * pAbc, int argc, char ** argv ); +static int Abc_CommandCleanup ( Abc_Frame_t * pAbc, int argc, char ** argv ); +static int Abc_CommandFastExtract ( Abc_Frame_t * pAbc, int argc, char ** argv ); +static int Abc_CommandDisjoint ( Abc_Frame_t * pAbc, int argc, char ** argv ); +static int Abc_CommandRes ( Abc_Frame_t * pAbc, int argc, char ** argv ); + +static int Abc_CommandLogic ( Abc_Frame_t * pAbc, int argc, char ** argv ); +static int Abc_CommandMiter ( Abc_Frame_t * pAbc, int argc, char ** argv ); +static int Abc_CommandFrames ( Abc_Frame_t * pAbc, int argc, char ** argv ); +static int Abc_CommandSop ( Abc_Frame_t * pAbc, int argc, char ** argv ); +static int Abc_CommandBdd ( Abc_Frame_t * pAbc, int argc, char ** argv ); +static int Abc_CommandSat ( Abc_Frame_t * pAbc, int argc, char ** argv ); +static int Abc_CommandExtSeqDcs ( Abc_Frame_t * pAbc, int argc, char ** argv ); + +static int Abc_CommandFraig ( Abc_Frame_t * pAbc, int argc, char ** argv ); +static int Abc_CommandFraigTrust ( Abc_Frame_t * pAbc, int argc, char ** argv ); +static int Abc_CommandFraigStore ( Abc_Frame_t * pAbc, int argc, char ** argv ); +static int Abc_CommandFraigRestore ( Abc_Frame_t * pAbc, int argc, char ** argv ); +static int Abc_CommandFraigClean ( Abc_Frame_t * pAbc, int argc, char ** argv ); +static int Abc_CommandFraigSweep ( Abc_Frame_t * pAbc, int argc, char ** argv ); + +static int Abc_CommandMap ( Abc_Frame_t * pAbc, int argc, char ** argv ); +static int Abc_CommandUnmap ( Abc_Frame_t * pAbc, int argc, char ** argv ); +static int Abc_CommandAttach ( Abc_Frame_t * pAbc, int argc, char ** argv ); +static int Abc_CommandSuperChoice ( Abc_Frame_t * pAbc, int argc, char ** argv ); + +static int Abc_CommandFpga ( Abc_Frame_t * pAbc, int argc, char ** argv ); + +static int Abc_CommandCec ( Abc_Frame_t * pAbc, int argc, char ** argv ); +static int Abc_CommandSec ( Abc_Frame_t * pAbc, int argc, char ** argv ); //////////////////////////////////////////////////////////////////////// /// FUNCTION DEFITIONS /// @@ -81,41 +85,46 @@ static int Ntk_CommandSec ( Abc_Frame_t * pAbc, int argc, char ** argv ***********************************************************************/ void Abc_Init( Abc_Frame_t * pAbc ) { - Cmd_CommandAdd( pAbc, "Printing", "print_stats", Ntk_CommandPrintStats, 0 ); - Cmd_CommandAdd( pAbc, "Printing", "print_io", Ntk_CommandPrintIo, 0 ); - Cmd_CommandAdd( pAbc, "Printing", "print_fanio", Ntk_CommandPrintFanio, 0 ); - Cmd_CommandAdd( pAbc, "Printing", "print_factor", Ntk_CommandPrintFactor, 0 ); - - Cmd_CommandAdd( pAbc, "Synthesis", "collapse", Ntk_CommandCollapse, 1 ); - Cmd_CommandAdd( pAbc, "Synthesis", "strash", Ntk_CommandStrash, 1 ); - Cmd_CommandAdd( pAbc, "Synthesis", "balance", Ntk_CommandBalance, 1 ); - Cmd_CommandAdd( pAbc, "Synthesis", "renode", Ntk_CommandRenode, 1 ); - Cmd_CommandAdd( pAbc, "Synthesis", "cleanup", Ntk_CommandCleanup, 1 ); - Cmd_CommandAdd( pAbc, "Synthesis", "fx", Ntk_CommandFx, 1 ); - - Cmd_CommandAdd( pAbc, "Various", "logic", Ntk_CommandLogic, 1 ); - Cmd_CommandAdd( pAbc, "Various", "miter", Ntk_CommandMiter, 1 ); - Cmd_CommandAdd( pAbc, "Various", "frames", Ntk_CommandFrames, 1 ); - Cmd_CommandAdd( pAbc, "Various", "sop", Ntk_CommandSop, 0 ); - Cmd_CommandAdd( pAbc, "Various", "bdd", Ntk_CommandBdd, 0 ); - Cmd_CommandAdd( pAbc, "Various", "sat", Ntk_CommandSat, 0 ); - - Cmd_CommandAdd( pAbc, "Fraiging", "fraig", Ntk_CommandFraig, 1 ); - Cmd_CommandAdd( pAbc, "Fraiging", "fraig_trust", Ntk_CommandFraigTrust, 1 ); - Cmd_CommandAdd( pAbc, "Fraiging", "fraig_store", Ntk_CommandFraigStore, 0 ); - Cmd_CommandAdd( pAbc, "Fraiging", "fraig_restore", Ntk_CommandFraigRestore, 1 ); - Cmd_CommandAdd( pAbc, "Fraiging", "fraig_clean", Ntk_CommandFraigClean, 0 ); - Cmd_CommandAdd( pAbc, "Fraiging", "fraig_sweep", Ntk_CommandFraigSweep, 1 ); - - Cmd_CommandAdd( pAbc, "SC mapping", "map", Ntk_CommandMap, 1 ); - Cmd_CommandAdd( pAbc, "SC mapping", "unmap", Ntk_CommandUnmap, 1 ); - Cmd_CommandAdd( pAbc, "SC mapping", "attach", Ntk_CommandAttach, 1 ); - Cmd_CommandAdd( pAbc, "SC mapping", "sc", Ntk_CommandSuperChoice, 1 ); - - Cmd_CommandAdd( pAbc, "FPGA mapping", "fpga", Ntk_CommandFpga, 1 ); - - Cmd_CommandAdd( pAbc, "Verification", "cec", Ntk_CommandCec, 0 ); - Cmd_CommandAdd( pAbc, "Verification", "sec", Ntk_CommandSec, 0 ); + Cmd_CommandAdd( pAbc, "Printing", "print_stats", Abc_CommandPrintStats, 0 ); + Cmd_CommandAdd( pAbc, "Printing", "print_io", Abc_CommandPrintIo, 0 ); + Cmd_CommandAdd( pAbc, "Printing", "print_fanio", Abc_CommandPrintFanio, 0 ); + Cmd_CommandAdd( pAbc, "Printing", "print_factor", Abc_CommandPrintFactor, 0 ); + + Cmd_CommandAdd( pAbc, "Printing", "show_bdd", Abc_CommandShowBdd, 0 ); + + Cmd_CommandAdd( pAbc, "Synthesis", "collapse", Abc_CommandCollapse, 1 ); + Cmd_CommandAdd( pAbc, "Synthesis", "strash", Abc_CommandStrash, 1 ); + Cmd_CommandAdd( pAbc, "Synthesis", "balance", Abc_CommandBalance, 1 ); + Cmd_CommandAdd( pAbc, "Synthesis", "renode", Abc_CommandRenode, 1 ); + Cmd_CommandAdd( pAbc, "Synthesis", "cleanup", Abc_CommandCleanup, 1 ); + Cmd_CommandAdd( pAbc, "Synthesis", "fx", Abc_CommandFastExtract, 1 ); + Cmd_CommandAdd( pAbc, "Synthesis", "dsd", Abc_CommandDisjoint, 1 ); + Cmd_CommandAdd( pAbc, "Synthesis", "res", Abc_CommandRes, 1 ); + + Cmd_CommandAdd( pAbc, "Various", "logic", Abc_CommandLogic, 1 ); + Cmd_CommandAdd( pAbc, "Various", "miter", Abc_CommandMiter, 1 ); + Cmd_CommandAdd( pAbc, "Various", "frames", Abc_CommandFrames, 1 ); + Cmd_CommandAdd( pAbc, "Various", "sop", Abc_CommandSop, 0 ); + Cmd_CommandAdd( pAbc, "Various", "bdd", Abc_CommandBdd, 0 ); + Cmd_CommandAdd( pAbc, "Various", "sat", Abc_CommandSat, 0 ); + Cmd_CommandAdd( pAbc, "Various", "ext_seq_dcs", Abc_CommandExtSeqDcs, 0 ); + + Cmd_CommandAdd( pAbc, "Fraiging", "fraig", Abc_CommandFraig, 1 ); + Cmd_CommandAdd( pAbc, "Fraiging", "fraig_trust", Abc_CommandFraigTrust, 1 ); + Cmd_CommandAdd( pAbc, "Fraiging", "fraig_store", Abc_CommandFraigStore, 0 ); + Cmd_CommandAdd( pAbc, "Fraiging", "fraig_restore", Abc_CommandFraigRestore, 1 ); + Cmd_CommandAdd( pAbc, "Fraiging", "fraig_clean", Abc_CommandFraigClean, 0 ); + Cmd_CommandAdd( pAbc, "Fraiging", "fraig_sweep", Abc_CommandFraigSweep, 1 ); + + Cmd_CommandAdd( pAbc, "SC mapping", "map", Abc_CommandMap, 1 ); + Cmd_CommandAdd( pAbc, "SC mapping", "unmap", Abc_CommandUnmap, 1 ); + Cmd_CommandAdd( pAbc, "SC mapping", "attach", Abc_CommandAttach, 1 ); + Cmd_CommandAdd( pAbc, "SC mapping", "sc", Abc_CommandSuperChoice, 1 ); + + Cmd_CommandAdd( pAbc, "FPGA mapping", "fpga", Abc_CommandFpga, 1 ); + + Cmd_CommandAdd( pAbc, "Verification", "cec", Abc_CommandCec, 0 ); + Cmd_CommandAdd( pAbc, "Verification", "sec", Abc_CommandSec, 0 ); Ft_FactorStartMan(); } @@ -148,7 +157,7 @@ void Abc_End() SeeAlso [] ***********************************************************************/ -int Ntk_CommandPrintStats( Abc_Frame_t * pAbc, int argc, char ** argv ) +int Abc_CommandPrintStats( Abc_Frame_t * pAbc, int argc, char ** argv ) { FILE * pOut, * pErr; Abc_Ntk_t * pNtk; @@ -202,7 +211,7 @@ usage: SeeAlso [] ***********************************************************************/ -int Ntk_CommandPrintIo( Abc_Frame_t * pAbc, int argc, char ** argv ) +int Abc_CommandPrintIo( Abc_Frame_t * pAbc, int argc, char ** argv ) { FILE * pOut, * pErr; Abc_Ntk_t * pNtk; @@ -271,7 +280,7 @@ usage: SeeAlso [] ***********************************************************************/ -int Ntk_CommandPrintFanio( Abc_Frame_t * pAbc, int argc, char ** argv ) +int Abc_CommandPrintFanio( Abc_Frame_t * pAbc, int argc, char ** argv ) { FILE * pOut, * pErr; Abc_Ntk_t * pNtk; @@ -322,7 +331,7 @@ usage: SeeAlso [] ***********************************************************************/ -int Ntk_CommandPrintFactor( Abc_Frame_t * pAbc, int argc, char ** argv ) +int Abc_CommandPrintFactor( Abc_Frame_t * pAbc, int argc, char ** argv ) { FILE * pOut, * pErr; Abc_Ntk_t * pNtk; @@ -391,6 +400,81 @@ usage: return 1; } +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Abc_CommandShowBdd( Abc_Frame_t * pAbc, int argc, char ** argv ) +{ + FILE * pOut, * pErr; + Abc_Ntk_t * pNtk; + Abc_Obj_t * pNode; + int c; + extern void Abc_NodePrintBdd( Abc_Obj_t * pNode ); + + pNtk = Abc_FrameReadNet(pAbc); + pOut = Abc_FrameReadOut(pAbc); + pErr = Abc_FrameReadErr(pAbc); + + // set defaults + util_getopt_reset(); + while ( ( c = util_getopt( argc, argv, "h" ) ) != EOF ) + { + switch ( c ) + { + case 'h': + goto usage; + default: + goto usage; + } + } + + if ( pNtk == NULL ) + { + fprintf( pErr, "Empty network.\n" ); + return 1; + } + + if ( !Abc_NtkIsLogicBdd(pNtk) ) + { + fprintf( pErr, "Printing BDDs can only be done for logic BDD networks.\n" ); + return 1; + } + + if ( argc != util_optind + 1 ) + { + fprintf( pErr, "Wrong number of auguments.\n" ); + goto usage; + } + + pNode = Abc_NtkFindNode( pNtk, argv[util_optind] ); + if ( pNode == NULL ) + { + fprintf( pErr, "Cannot find node \"%s\".\n", argv[util_optind] ); + return 1; + } + Abc_NodePrintBdd( pNode ); + return 0; + +usage: + fprintf( pErr, "usage: show_bdd [-h] <node>\n" ); + fprintf( pErr, " visualizes the BDD of a node using DOT and GSVIEW\n" ); +#ifdef WIN32 + fprintf( pErr, " \"dot.exe\" and \"gsview32.exe\" should be set in the paths\n" ); + fprintf( pErr, " (\"gsview32.exe\" may be in \"C:\\Program Files\\Ghostgum\\gsview\\\")\n" ); +#endif + fprintf( pErr, "\tnode : the node to consider\n"); + fprintf( pErr, "\t-h : print the command usage\n"); + return 1; +} + /**Function************************************************************* @@ -403,7 +487,7 @@ usage: SeeAlso [] ***********************************************************************/ -int Ntk_CommandCollapse( Abc_Frame_t * pAbc, int argc, char ** argv ) +int Abc_CommandCollapse( Abc_Frame_t * pAbc, int argc, char ** argv ) { FILE * pOut, * pErr; Abc_Ntk_t * pNtk, * pNtkRes; @@ -443,7 +527,7 @@ int Ntk_CommandCollapse( Abc_Frame_t * pAbc, int argc, char ** argv ) pNtkRes = Abc_NtkCollapse( pNtk, 1 ); else { - pNtk = Abc_NtkStrash( pNtk ); + pNtk = Abc_NtkStrash( pNtk, 0 ); pNtkRes = Abc_NtkCollapse( pNtk, 1 ); Abc_NtkDelete( pNtk ); } @@ -475,22 +559,27 @@ usage: SeeAlso [] ***********************************************************************/ -int Ntk_CommandStrash( Abc_Frame_t * pAbc, int argc, char ** argv ) +int Abc_CommandStrash( Abc_Frame_t * pAbc, int argc, char ** argv ) { FILE * pOut, * pErr; Abc_Ntk_t * pNtk, * pNtkRes; int c; + int fAllNodes; pNtk = Abc_FrameReadNet(pAbc); pOut = Abc_FrameReadOut(pAbc); pErr = Abc_FrameReadErr(pAbc); // set defaults + fAllNodes = 0; util_getopt_reset(); - while ( ( c = util_getopt( argc, argv, "h" ) ) != EOF ) + while ( ( c = util_getopt( argc, argv, "ah" ) ) != EOF ) { switch ( c ) { + case 'a': + fAllNodes ^= 1; + break; case 'h': goto usage; default: @@ -505,7 +594,7 @@ int Ntk_CommandStrash( Abc_Frame_t * pAbc, int argc, char ** argv ) } // get the new network - pNtkRes = Abc_NtkStrash( pNtk ); + pNtkRes = Abc_NtkStrash( pNtk, fAllNodes ); if ( pNtkRes == NULL ) { fprintf( pErr, "Strashing has failed.\n" ); @@ -516,8 +605,9 @@ int Ntk_CommandStrash( Abc_Frame_t * pAbc, int argc, char ** argv ) return 0; usage: - fprintf( pErr, "usage: strash [-h]\n" ); + fprintf( pErr, "usage: strash [-ah]\n" ); fprintf( pErr, "\t transforms combinational logic into an AIG\n" ); + fprintf( pErr, "\t-a : toggles between using all nodes and DFS nodes [default = %s]\n", fAllNodes? "all": "DFS" ); fprintf( pErr, "\t-h : print the command usage\n"); return 1; } @@ -533,7 +623,7 @@ usage: SeeAlso [] ***********************************************************************/ -int Ntk_CommandBalance( Abc_Frame_t * pAbc, int argc, char ** argv ) +int Abc_CommandBalance( Abc_Frame_t * pAbc, int argc, char ** argv ) { FILE * pOut, * pErr; Abc_Ntk_t * pNtk, * pNtkRes; @@ -602,7 +692,7 @@ usage: SeeAlso [] ***********************************************************************/ -int Ntk_CommandRenode( Abc_Frame_t * pAbc, int argc, char ** argv ) +int Abc_CommandRenode( Abc_Frame_t * pAbc, int argc, char ** argv ) { FILE * pOut, * pErr; Abc_Ntk_t * pNtk, * pNtkRes; @@ -709,7 +799,7 @@ usage: SeeAlso [] ***********************************************************************/ -int Ntk_CommandCleanup( Abc_Frame_t * pAbc, int argc, char ** argv ) +int Abc_CommandCleanup( Abc_Frame_t * pAbc, int argc, char ** argv ) { FILE * pOut, * pErr; Abc_Ntk_t * pNtk; @@ -767,7 +857,7 @@ usage: SeeAlso [] ***********************************************************************/ -int Ntk_CommandFx( Abc_Frame_t * pAbc, int argc, char ** argv ) +int Abc_CommandFastExtract( Abc_Frame_t * pAbc, int argc, char ** argv ) { Abc_Ntk_t * pNtk; FILE * pOut, * pErr; @@ -875,6 +965,129 @@ usage: return 1; } +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Abc_CommandDisjoint( Abc_Frame_t * pAbc, int argc, char ** argv ) +{ + FILE * pOut, * pErr; + Abc_Ntk_t * pNtk, * pNtkRes, * pNtkNew; + int fGlobal, fRecursive, fVerbose, fPrint, fShort, c; + + extern Abc_Ntk_t * Abc_NtkDsdGlobal( Abc_Ntk_t * pNtk, bool fVerbose, bool fPrint, bool fShort ); + extern int Abc_NtkDsdRecursive( Abc_Ntk_t * pNtk, bool fVerbose ); + + pNtk = Abc_FrameReadNet(pAbc); + pOut = Abc_FrameReadOut(pAbc); + pErr = Abc_FrameReadErr(pAbc); + + // set defaults + fGlobal = 1; + fRecursive = 0; + fVerbose = 0; + fPrint = 0; + fShort = 0; + util_getopt_reset(); + while ( ( c = util_getopt( argc, argv, "grvpsh" ) ) != EOF ) + { + switch ( c ) + { + case 'g': + fGlobal ^= 1; + break; + case 'r': + fRecursive ^= 1; + break; + case 'v': + fVerbose ^= 1; + break; + case 'p': + fPrint ^= 1; + break; + case 's': + fShort ^= 1; + break; + case 'h': + goto usage; + break; + default: + goto usage; + } + } + + if ( pNtk == NULL ) + { + fprintf( pErr, "Empty network.\n" ); + return 1; + } + + if ( !fGlobal && !fRecursive ) + { + fprintf( pErr, "Decomposition should be either global or recursive.\n" ); + return 1; + } + + if ( fGlobal ) + { + // get the new network + if ( !Abc_NtkIsAig(pNtk) ) + { + pNtkNew = Abc_NtkStrash( pNtk, 0 ); + pNtkRes = Abc_NtkDsdGlobal( pNtkNew, fVerbose, fPrint, fShort ); + Abc_NtkDelete( pNtkNew ); + } + else + { + pNtkRes = Abc_NtkDsdGlobal( pNtk, fVerbose, fPrint, fShort ); + } + if ( pNtkRes == NULL ) + { + fprintf( pErr, "Global disjoint support decomposition has failed.\n" ); + return 1; + } + if ( fRecursive ) + { + if ( !Abc_NtkDsdRecursive( pNtkRes, fVerbose ) ) + { + fprintf( pErr, "Recursive decomposition has failed.\n" ); + Abc_NtkDelete( pNtkRes ); + return 1; + } + } + // replace the current network + Abc_FrameReplaceCurrentNetwork( pAbc, pNtkRes ); + } + else if ( fRecursive ) + { + if ( !Abc_NtkIsLogicBdd( pNtk ) ) + { + fprintf( pErr, "This command is only applicable to logic BDD networks.\n" ); + return 1; + } + if ( !Abc_NtkDsdRecursive( pNtk, fVerbose ) ) + fprintf( pErr, "Recursive decomposition has failed.\n" ); + } + return 0; + +usage: + fprintf( pErr, "usage: dsd [-grvpsh]\n" ); + fprintf( pErr, "\t decomposes the network using disjoint-support decomposition\n" ); + fprintf( pErr, "\t-g : collapses the network and decomposes shared BDDs [default = %s]\n", fGlobal? "yes": "no" ); + fprintf( pErr, "\t-r : applied DSD and MUX-decomposition recursively [default = %s]\n", fRecursive? "yes": "no" ); + fprintf( pErr, "\t-v : prints DSD statistics and runtime [default = %s]\n", fVerbose? "yes": "no" ); + fprintf( pErr, "\t-p : prints DSD structure to the standard output [default = %s]\n", fPrint? "yes": "no" ); + fprintf( pErr, "\t-s : use short PI names when printing DSD structure [default = %s]\n", fShort? "yes": "no" ); + fprintf( pErr, "\t-h : print the command usage\n"); + return 1; +} /**Function************************************************************* @@ -887,7 +1100,106 @@ usage: SeeAlso [] ***********************************************************************/ -int Ntk_CommandLogic( Abc_Frame_t * pAbc, int argc, char ** argv ) +int Abc_CommandRes( Abc_Frame_t * pAbc, int argc, char ** argv ) +{ + FILE * pOut, * pErr; + Abc_Ntk_t * pNtk; + int c; + Abc_ManRes_t * p; + extern int Abc_NtkAigResynthesize( Abc_Ntk_t * pNtk, Abc_ManRes_t * p ); + + pNtk = Abc_FrameReadNet(pAbc); + pOut = Abc_FrameReadOut(pAbc); + pErr = Abc_FrameReadErr(pAbc); + + // set defaults + p = Abc_NtkManResStart(); + p->fVerbose = 0; + p->nNodeSizeMax = 10; + p->nConeSizeMax = 10; + util_getopt_reset(); + while ( ( c = util_getopt( argc, argv, "ncvh" ) ) != EOF ) + { + switch ( c ) + { + case 'n': + if ( util_optind >= argc ) + { + fprintf( pErr, "Command line switch \"-n\" should be followed by an integer.\n" ); + goto usage; + } + p->nNodeSizeMax = atoi(argv[util_optind]); + util_optind++; + if ( p->nNodeSizeMax < 0 ) + goto usage; + break; + case 'c': + if ( util_optind >= argc ) + { + fprintf( pErr, "Command line switch \"-c\" should be followed by an integer.\n" ); + goto usage; + } + p->nConeSizeMax = atoi(argv[util_optind]); + util_optind++; + if ( p->nConeSizeMax < 0 ) + goto usage; + break; + case 'v': + p->fVerbose ^= 1; + break; + case 'h': + goto usage; + default: + goto usage; + } + } + + if ( pNtk == NULL ) + { + fprintf( pErr, "Empty network.\n" ); + Abc_NtkManResStop( p ); + return 1; + } + if ( !Abc_NtkIsAig(pNtk) ) + { + fprintf( pErr, "This command can only be applied to an AIG.\n" ); + Abc_NtkManResStop( p ); + return 1; + } + if ( Abc_NtkCountChoiceNodes(pNtk) ) + { + fprintf( pErr, "AIG resynthesis cannot be applied to AIGs with choice nodes.\n" ); + Abc_NtkManResStop( p ); + return 1; + } + + // modify the current network + Abc_NtkAigResynthesize( pNtk, p ); + return 0; + +usage: + fprintf( pErr, "usage: res [-n num] [-c num] [-vh]\n" ); + fprintf( pErr, "\t performs technology-independent resynthesis of the AIG\n" ); + fprintf( pErr, "\t-n num : the max support of the collapsed node [default = %d]\n", p->nNodeSizeMax ); + fprintf( pErr, "\t-c num : the max support of the containing cone [default = %d]\n", p->nConeSizeMax ); + fprintf( pErr, "\t-v : toggle verbose printout [default = %s]\n", p->fVerbose? "yes": "no" ); + fprintf( pErr, "\t-h : print the command usage\n"); + return 1; +} + + +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Abc_CommandLogic( Abc_Frame_t * pAbc, int argc, char ** argv ) { FILE * pOut, * pErr; Abc_Ntk_t * pNtk, * pNtkRes; @@ -951,7 +1263,7 @@ usage: SeeAlso [] ***********************************************************************/ -int Ntk_CommandMiter( Abc_Frame_t * pAbc, int argc, char ** argv ) +int Abc_CommandMiter( Abc_Frame_t * pAbc, int argc, char ** argv ) { FILE * pOut, * pErr; Abc_Ntk_t * pNtk, * pNtk1, * pNtk2, * pNtkRes; @@ -1025,7 +1337,7 @@ usage: SeeAlso [] ***********************************************************************/ -int Ntk_CommandFrames( Abc_Frame_t * pAbc, int argc, char ** argv ) +int Abc_CommandFrames( Abc_Frame_t * pAbc, int argc, char ** argv ) { FILE * pOut, * pErr; Abc_Ntk_t * pNtk, * pNtkTemp, * pNtkRes; @@ -1075,7 +1387,7 @@ int Ntk_CommandFrames( Abc_Frame_t * pAbc, int argc, char ** argv ) // get the new network if ( !Abc_NtkIsAig(pNtk) ) { - pNtkTemp = Abc_NtkStrash( pNtk ); + pNtkTemp = Abc_NtkStrash( pNtk, 0 ); pNtkRes = Abc_NtkFrames( pNtkTemp, nFrames, fInitial ); Abc_NtkDelete( pNtkTemp ); } @@ -1111,7 +1423,7 @@ usage: SeeAlso [] ***********************************************************************/ -int Ntk_CommandSop( Abc_Frame_t * pAbc, int argc, char ** argv ) +int Abc_CommandSop( Abc_Frame_t * pAbc, int argc, char ** argv ) { FILE * pOut, * pErr; Abc_Ntk_t * pNtk; @@ -1171,7 +1483,7 @@ usage: SeeAlso [] ***********************************************************************/ -int Ntk_CommandBdd( Abc_Frame_t * pAbc, int argc, char ** argv ) +int Abc_CommandBdd( Abc_Frame_t * pAbc, int argc, char ** argv ) { FILE * pOut, * pErr; Abc_Ntk_t * pNtk; @@ -1231,7 +1543,7 @@ usage: SeeAlso [] ***********************************************************************/ -int Ntk_CommandSat( Abc_Frame_t * pAbc, int argc, char ** argv ) +int Abc_CommandSat( Abc_Frame_t * pAbc, int argc, char ** argv ) { FILE * pOut, * pErr; Abc_Ntk_t * pNtk; @@ -1295,6 +1607,76 @@ usage: } +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Abc_CommandExtSeqDcs( Abc_Frame_t * pAbc, int argc, char ** argv ) +{ + FILE * pOut, * pErr; + Abc_Ntk_t * pNtk; + int c; + int fVerbose; + extern int Abc_NtkExtractSequentialDcs( Abc_Ntk_t * pNet, bool fVerbose ); + + pNtk = Abc_FrameReadNet(pAbc); + pOut = Abc_FrameReadOut(pAbc); + pErr = Abc_FrameReadErr(pAbc); + + // set defaults + fVerbose = 0; + util_getopt_reset(); + while ( ( c = util_getopt( argc, argv, "vh" ) ) != EOF ) + { + switch ( c ) + { + case 'v': + fVerbose ^= 1; + break; + case 'h': + goto usage; + default: + goto usage; + } + } + + if ( pNtk == NULL ) + { + fprintf( pErr, "Empty network.\n" ); + return 1; + } + if ( Abc_NtkLatchNum(pNtk) == 0 ) + { + fprintf( stdout, "The current network has no latches.\n" ); + return 0; + } + if ( !Abc_NtkIsAig(pNtk) ) + { + fprintf( stdout, "This command works only for AIGs.\n" ); + return 0; + } + if ( !Abc_NtkExtractSequentialDcs( pNtk, fVerbose ) ) + { + fprintf( stdout, "Extracting sequential don't-cares has failed.\n" ); + return 1; + } + return 0; + +usage: + fprintf( pErr, "usage: ext_seq_dcs [-vh]\n" ); + fprintf( pErr, "\t create EXDC network using unreachable states\n" ); + fprintf( pErr, "\t-v : prints verbose information [default = %s]\n", fVerbose? "yes": "no" ); + fprintf( pErr, "\t-h : print the command usage\n"); + return 1; +} + @@ -1309,7 +1691,7 @@ usage: SeeAlso [] ***********************************************************************/ -int Ntk_CommandFraig( Abc_Frame_t * pAbc, int argc, char ** argv ) +int Abc_CommandFraig( Abc_Frame_t * pAbc, int argc, char ** argv ) { char Buffer[100]; Fraig_Params_t Params; @@ -1419,7 +1801,7 @@ int Ntk_CommandFraig( Abc_Frame_t * pAbc, int argc, char ** argv ) pNtkRes = Abc_NtkFraig( pNtk, &Params, fAllNodes ); else { - pNtk = Abc_NtkStrash( pNtk ); + pNtk = Abc_NtkStrash( pNtk, 0 ); pNtkRes = Abc_NtkFraig( pNtk, &Params, fAllNodes ); Abc_NtkDelete( pNtk ); } @@ -1464,7 +1846,7 @@ usage: SeeAlso [] ***********************************************************************/ -int Ntk_CommandFraigTrust( Abc_Frame_t * pAbc, int argc, char ** argv ) +int Abc_CommandFraigTrust( Abc_Frame_t * pAbc, int argc, char ** argv ) { FILE * pOut, * pErr; Abc_Ntk_t * pNtk, * pNtkRes; @@ -1528,7 +1910,7 @@ usage: SeeAlso [] ***********************************************************************/ -int Ntk_CommandFraigStore( Abc_Frame_t * pAbc, int argc, char ** argv ) +int Abc_CommandFraigStore( Abc_Frame_t * pAbc, int argc, char ** argv ) { FILE * pOut, * pErr; Abc_Ntk_t * pNtk; @@ -1589,7 +1971,7 @@ usage: SeeAlso [] ***********************************************************************/ -int Ntk_CommandFraigRestore( Abc_Frame_t * pAbc, int argc, char ** argv ) +int Abc_CommandFraigRestore( Abc_Frame_t * pAbc, int argc, char ** argv ) { FILE * pOut, * pErr; Abc_Ntk_t * pNtk, * pNtkRes; @@ -1653,7 +2035,7 @@ usage: SeeAlso [] ***********************************************************************/ -int Ntk_CommandFraigClean( Abc_Frame_t * pAbc, int argc, char ** argv ) +int Abc_CommandFraigClean( Abc_Frame_t * pAbc, int argc, char ** argv ) { FILE * pOut, * pErr; Abc_Ntk_t * pNtk; @@ -1702,7 +2084,7 @@ usage: SeeAlso [] ***********************************************************************/ -int Ntk_CommandFraigSweep( Abc_Frame_t * pAbc, int argc, char ** argv ) +int Abc_CommandFraigSweep( Abc_Frame_t * pAbc, int argc, char ** argv ) { FILE * pOut, * pErr; Abc_Ntk_t * pNtk; @@ -1779,7 +2161,7 @@ usage: SeeAlso [] ***********************************************************************/ -int Ntk_CommandMap( Abc_Frame_t * pAbc, int argc, char ** argv ) +int Abc_CommandMap( Abc_Frame_t * pAbc, int argc, char ** argv ) { FILE * pOut, * pErr; Abc_Ntk_t * pNtk, * pNtkRes; @@ -1840,7 +2222,7 @@ int Ntk_CommandMap( Abc_Frame_t * pAbc, int argc, char ** argv ) if ( !Abc_NtkIsAig(pNtk) ) { - pNtk = Abc_NtkStrash( pNtk ); + pNtk = Abc_NtkStrash( pNtk, 0 ); if ( pNtk == NULL ) { fprintf( pErr, "Strashing before mapping has failed.\n" ); @@ -1909,7 +2291,7 @@ usage: SeeAlso [] ***********************************************************************/ -int Ntk_CommandUnmap( Abc_Frame_t * pAbc, int argc, char ** argv ) +int Abc_CommandUnmap( Abc_Frame_t * pAbc, int argc, char ** argv ) { FILE * pOut, * pErr; Abc_Ntk_t * pNtk; @@ -1970,7 +2352,7 @@ usage: SeeAlso [] ***********************************************************************/ -int Ntk_CommandAttach( Abc_Frame_t * pAbc, int argc, char ** argv ) +int Abc_CommandAttach( Abc_Frame_t * pAbc, int argc, char ** argv ) { FILE * pOut, * pErr; Abc_Ntk_t * pNtk; @@ -2033,7 +2415,7 @@ usage: SeeAlso [] ***********************************************************************/ -int Ntk_CommandSuperChoice( Abc_Frame_t * pAbc, int argc, char ** argv ) +int Abc_CommandSuperChoice( Abc_Frame_t * pAbc, int argc, char ** argv ) { FILE * pOut, * pErr; Abc_Ntk_t * pNtk, * pNtkRes; @@ -2098,7 +2480,7 @@ usage: SeeAlso [] ***********************************************************************/ -int Ntk_CommandFpga( Abc_Frame_t * pAbc, int argc, char ** argv ) +int Abc_CommandFpga( Abc_Frame_t * pAbc, int argc, char ** argv ) { FILE * pOut, * pErr; Abc_Ntk_t * pNtk, * pNtkRes; @@ -2141,7 +2523,7 @@ int Ntk_CommandFpga( Abc_Frame_t * pAbc, int argc, char ** argv ) if ( !Abc_NtkIsAig(pNtk) ) { // strash and balance the network - pNtk = Abc_NtkStrash( pNtk ); + pNtk = Abc_NtkStrash( pNtk, 0 ); if ( pNtk == NULL ) { fprintf( pErr, "Strashing before FPGA mapping has failed.\n" ); @@ -2202,7 +2584,7 @@ usage: SeeAlso [] ***********************************************************************/ -int Ntk_CommandCec( Abc_Frame_t * pAbc, int argc, char ** argv ) +int Abc_CommandCec( Abc_Frame_t * pAbc, int argc, char ** argv ) { FILE * pOut, * pErr; Abc_Ntk_t * pNtk, * pNtk1, * pNtk2; @@ -2273,7 +2655,7 @@ usage: SeeAlso [] ***********************************************************************/ -int Ntk_CommandSec( Abc_Frame_t * pAbc, int argc, char ** argv ) +int Abc_CommandSec( Abc_Frame_t * pAbc, int argc, char ** argv ) { FILE * pOut, * pErr; Abc_Ntk_t * pNtk, * pNtk1, * pNtk2; diff --git a/src/base/abc/abc.h b/src/base/abc/abc.h index 35fa85e9..9b9bd81e 100644 --- a/src/base/abc/abc.h +++ b/src/base/abc/abc.h @@ -21,25 +21,6 @@ #ifndef __ABC_H__ #define __ABC_H__ -/* - In the netlist, the PI/PO arrays store PI/PO nets. - The names belongs to the nets and are stored in pNet->pData. - When a netlist is made combinational: - - LO/LI nets are added to PI/PO arrays, - - the array of latches is temporarily stored in vLatch2, - - the original number of PIs/POs is remembered in nPisOld/nPosOld. - - In a logic network, the PI/PO arrays store PI/PO nodes. - The PO nodes have only one fanin edge, which can be complemented. - The arrays vNamesPi/vNamesPo/vNamesLatch store PI/PO/latch names. - The internal nodes are nameless. - When a logic network is made combinational: - - laches are added to the PI/PO arrays, - - the arrays of names are not changed, - - the array of latches is temporarily stored in vLatch2, - - the original number of PIs/POs is remembered in nPisOld/nPosOld. -*/ - //////////////////////////////////////////////////////////////////////// /// INCLUDES /// //////////////////////////////////////////////////////////////////////// @@ -103,6 +84,7 @@ typedef struct Abc_Obj_t_ Abc_Obj_t; typedef struct Abc_Ntk_t_ Abc_Ntk_t; typedef struct Abc_Aig_t_ Abc_Aig_t; typedef struct Abc_ManTime_t_ Abc_ManTime_t; +typedef struct Abc_ManRes_t_ Abc_ManRes_t; typedef struct Abc_Time_t_ Abc_Time_t; struct Abc_Time_t_ @@ -182,6 +164,30 @@ struct Abc_Ntk_t_ Extra_MmStep_t * pMmStep; // memory manager for arrays }; +struct Abc_ManRes_t_ +{ + // user specified parameters + int nNodeSizeMax; // the limit on the size of the supernode + int nConeSizeMax; // the limit on the size of the containing cone + int fVerbose; // the verbosity flag + // internal parameters + DdManager * dd; // the BDD manager + DdNode * bCubeX; // the cube of PI variables + Abc_Obj_t * pNode; // the node currently considered + Vec_Ptr_t * vFaninsNode; // fanins of the supernode + Vec_Ptr_t * vInsideNode; // inside of the supernode + Vec_Ptr_t * vFaninsCone; // fanins of the containing cone + Vec_Ptr_t * vInsideCone; // inside of the containing cone + Vec_Ptr_t * vVisited; // the visited nodes + Vec_Str_t * vCube; // temporary cube for generating covers + Vec_Int_t * vForm; // the factored form (temporary) + // runtime statistics + int time1; + int time2; + int time3; + int time4; +}; + //////////////////////////////////////////////////////////////////////// /// MACRO DEFITIONS /// //////////////////////////////////////////////////////////////////////// @@ -380,11 +386,12 @@ extern bool Abc_NtkCheck( Abc_Ntk_t * pNtk ); extern bool Abc_NtkCompareSignals( Abc_Ntk_t * pNtk1, Abc_Ntk_t * pNtk2, int fComb ); /*=== abcCollapse.c ==========================================================*/ extern Abc_Ntk_t * Abc_NtkCollapse( Abc_Ntk_t * pNtk, int fVerbose ); +extern DdManager * Abc_NtkGlobalBdds( Abc_Ntk_t * pNtk, int fLatchOnly ); +extern void Abc_NtkFreeGlobalBdds( DdManager * dd, Abc_Ntk_t * pNtk ); /*=== abcCreate.c ==========================================================*/ extern Abc_Ntk_t * Abc_NtkAlloc( Abc_NtkType_t Type ); extern Abc_Ntk_t * Abc_NtkStartFrom( Abc_Ntk_t * pNtk, Abc_NtkType_t Type ); extern void Abc_NtkFinalize( Abc_Ntk_t * pNtk, Abc_Ntk_t * pNtkNew ); -extern void Abc_NtkFinalizeRegular( Abc_Ntk_t * pNtk, Abc_Ntk_t * pNtkNew ); extern Abc_Ntk_t * Abc_NtkDup( Abc_Ntk_t * pNtk ); extern void Abc_NtkDelete( Abc_Ntk_t * pNtk ); extern Abc_Obj_t * Abc_NtkDupObj( Abc_Ntk_t * pNtkNew, Abc_Obj_t * pObj ); @@ -407,6 +414,7 @@ extern Abc_Obj_t * Abc_NodeCreateBuf( Abc_Ntk_t * pNtk, Abc_Obj_t * pFani extern Abc_Obj_t * Abc_NodeCreateAnd( Abc_Ntk_t * pNtk, Vec_Ptr_t * vFanins ); extern Abc_Obj_t * Abc_NodeCreateOr( Abc_Ntk_t * pNtk, Vec_Ptr_t * vFanins ); extern Abc_Obj_t * Abc_NodeCreateMux( Abc_Ntk_t * pNtk, Abc_Obj_t * pNodeC, Abc_Obj_t * pNode1, Abc_Obj_t * pNode0 ); +extern Abc_Obj_t * Abc_NodeClone( Abc_Obj_t * pNode ); /*=== abcDfs.c ==========================================================*/ extern Vec_Ptr_t * Abc_NtkDfs( Abc_Ntk_t * pNtk ); extern Vec_Ptr_t * Abc_AigDfs( Abc_Ntk_t * pNtk ); @@ -415,6 +423,7 @@ extern bool Abc_NtkIsAcyclic( Abc_Ntk_t * pNtk ); /*=== abcFanio.c ==========================================================*/ extern void Abc_ObjAddFanin( Abc_Obj_t * pObj, Abc_Obj_t * pFanin ); extern void Abc_ObjDeleteFanin( Abc_Obj_t * pObj, Abc_Obj_t * pFanin ); +extern void Abc_ObjRemoveFanins( Abc_Obj_t * pObj ); extern void Abc_ObjPatchFanin( Abc_Obj_t * pObj, Abc_Obj_t * pFaninOld, Abc_Obj_t * pFaninNew ); extern void Abc_ObjTransferFanout( Abc_Obj_t * pObjOld, Abc_Obj_t * pObjNew ); extern void Abc_ObjReplace( Abc_Obj_t * pObjOld, Abc_Obj_t * pObjNew ); @@ -426,7 +435,7 @@ extern Abc_Ntk_t * Abc_NtkFraigRestore(); extern void Abc_NtkFraigStoreClean(); /*=== abcFunc.c ==========================================================*/ extern int Abc_NtkSopToBdd( Abc_Ntk_t * pNtk ); -extern char * Abc_ConvertBddToSop( Extra_MmFlex_t * pMan, DdManager * dd, DdNode * bFunc, int nFanins, Vec_Str_t * vCube, int fMode ); +extern char * Abc_ConvertBddToSop( Extra_MmFlex_t * pMan, DdManager * dd, DdNode * bFuncOn, DdNode * bFuncOnDc, int nFanins, Vec_Str_t * vCube, int fMode ); extern int Abc_NtkBddToSop( Abc_Ntk_t * pNtk ); extern void Abc_NodeBddToCnf( Abc_Obj_t * pNode, Extra_MmFlex_t * pMmMan, Vec_Str_t * vCube, char ** ppSop0, char ** ppSop1 ); extern int Abc_CountZddCubes( DdManager * dd, DdNode * zCover ); @@ -475,6 +484,9 @@ extern int Abc_NodeMffcRemove( Abc_Obj_t * pNode ); /*=== abcRenode.c ==========================================================*/ extern Abc_Ntk_t * Abc_NtkRenode( Abc_Ntk_t * pNtk, int nThresh, int nFaninMax, int fCnf, int fMulti, int fSimple ); extern DdNode * Abc_NtkRenodeDeriveBdd( DdManager * dd, Abc_Obj_t * pNodeOld, Vec_Ptr_t * vFaninsOld ); +/*=== abcRes.c ==========================================================*/ +extern Abc_ManRes_t * Abc_NtkManResStart(); +extern void Abc_NtkManResStop( Abc_ManRes_t * p ); /*=== abcSat.c ==========================================================*/ extern bool Abc_NtkMiterSat( Abc_Ntk_t * pNtk, int fVerbose ); extern solver * Abc_NtkMiterSatCreate( Abc_Ntk_t * pNtk ); @@ -497,7 +509,7 @@ extern bool Abc_SopCheck( char * pSop, int nFanins ); extern void Abc_SopWriteCnf( FILE * pFile, char * pClauses, Vec_Int_t * vVars ); extern void Abc_SopAddCnfToSolver( solver * pSat, char * pClauses, Vec_Int_t * vVars, Vec_Int_t * vTemp ); /*=== abcStrash.c ==========================================================*/ -extern Abc_Ntk_t * Abc_NtkStrash( Abc_Ntk_t * pNtk ); +extern Abc_Ntk_t * Abc_NtkStrash( Abc_Ntk_t * pNtk, bool fAllNodes ); extern int Abc_NtkAppend( Abc_Ntk_t * pNtk1, Abc_Ntk_t * pNtk2 ); extern Abc_Ntk_t * Abc_NtkBalance( Abc_Ntk_t * pNtk, bool fDuplicate ); /*=== abcSweep.c ==========================================================*/ @@ -512,7 +524,7 @@ extern void Abc_NtkTimeSetDefaultArrival( Abc_Ntk_t * pNtk, float extern void Abc_NtkTimeSetDefaultRequired( Abc_Ntk_t * pNtk, float Rise, float Fall ); extern void Abc_NtkTimeSetArrival( Abc_Ntk_t * pNtk, int ObjId, float Rise, float Fall ); extern void Abc_NtkTimeSetRequired( Abc_Ntk_t * pNtk, int ObjId, float Rise, float Fall ); -extern void Abc_NtkTimeFinalize( Abc_Ntk_t * pNtk ); +extern void Abc_NtkTimeInitialize( Abc_Ntk_t * pNtk ); extern void Abc_ManTimeStop( Abc_ManTime_t * p ); extern void Abc_ManTimeDup( Abc_Ntk_t * pNtkOld, Abc_Ntk_t * pNtkNew ); extern void Abc_NtkSetNodeLevelsArrival( Abc_Ntk_t * pNtk ); @@ -549,6 +561,9 @@ extern void Abc_NodeCollectFanouts( Abc_Obj_t * pNode, Vec_Ptr_t * extern int Abc_NodeCompareLevelsIncrease( Abc_Obj_t ** pp1, Abc_Obj_t ** pp2 ); extern int Abc_NodeCompareLevelsDecrease( Abc_Obj_t ** pp1, Abc_Obj_t ** pp2 ); extern Vec_Ptr_t * Abc_AigCollectAll( Abc_Ntk_t * pNtk ); +extern Vec_Ptr_t * Abc_NodeGetFaninNames( Abc_Obj_t * pNode ); +extern void Abc_NodeFreeFaninNames( Vec_Ptr_t * vNames ); + //////////////////////////////////////////////////////////////////////// /// END OF FILE /// diff --git a/src/base/abc/abcCheck.c b/src/base/abc/abcCheck.c index 67cfe9df..6a733185 100644 --- a/src/base/abc/abcCheck.c +++ b/src/base/abc/abcCheck.c @@ -108,11 +108,11 @@ bool Abc_NtkCheck( Abc_Ntk_t * pNtk ) // check the EXDC network if present if ( pNtk->pExdc ) { - if ( pNtk->Type != pNtk->pExdc->Type ) - { - fprintf( stdout, "NetworkCheck: Network and its EXDC have different types.\n" ); - return 0; - } +// if ( pNtk->Type != pNtk->pExdc->Type ) +// { +// fprintf( stdout, "NetworkCheck: Network and its EXDC have different types.\n" ); +// return 0; +// } return Abc_NtkCheck( pNtk->pExdc ); } return 1; diff --git a/src/base/abc/abcCollapse.c b/src/base/abc/abcCollapse.c index 372b1553..3ee086c0 100644 --- a/src/base/abc/abcCollapse.c +++ b/src/base/abc/abcCollapse.c @@ -24,7 +24,6 @@ /// DECLARATIONS /// //////////////////////////////////////////////////////////////////////// -static DdManager * Abc_NtkGlobalBdds( Abc_Ntk_t * pNtk ); static DdNode * Abc_NtkGlobalBdds_rec( DdManager * dd, Abc_Obj_t * pNode ); static Abc_Ntk_t * Abc_NtkFromGlobalBdds( DdManager * dd, Abc_Ntk_t * pNtk ); static Abc_Obj_t * Abc_NodeFromGlobalBdds( Abc_Ntk_t * pNtkNew, DdManager * dd, DdNode * bFunc ); @@ -52,33 +51,16 @@ Abc_Ntk_t * Abc_NtkCollapse( Abc_Ntk_t * pNtk, int fVerbose ) assert( Abc_NtkIsAig(pNtk) ); - // perform FPGA mapping - dd = Abc_NtkGlobalBdds( pNtk ); + // compute the global BDDs + dd = Abc_NtkGlobalBdds( pNtk, 0 ); if ( dd == NULL ) return NULL; if ( fVerbose ) printf( "The shared BDD size is %d nodes.\n", Cudd_ReadKeys(dd) - Cudd_ReadDead(dd) ); -/* - { - Abc_Obj_t * pNode; - int i; - Abc_NtkForEachPo( pNtk, pNode, i ) - { - Cudd_RecursiveDeref( dd, (DdNode *)pNode->pNext ); - pNode->pNext = NULL; - } - Abc_NtkForEachLatch( pNtk, pNode, i ) - { - Cudd_RecursiveDeref( dd, (DdNode *)pNode->pNext ); - pNode->pNext = NULL; - } - } - Extra_StopManager( dd ); - return NULL; -*/ - // transform the result of mapping into a BDD network + // create the new network pNtkNew = Abc_NtkFromGlobalBdds( dd, pNtk ); + Abc_NtkFreeGlobalBdds( dd, pNtk ); if ( pNtkNew == NULL ) { Cudd_Quit( dd ); @@ -110,8 +92,9 @@ Abc_Ntk_t * Abc_NtkCollapse( Abc_Ntk_t * pNtk, int fVerbose ) SeeAlso [] ***********************************************************************/ -DdManager * Abc_NtkGlobalBdds( Abc_Ntk_t * pNtk ) +DdManager * Abc_NtkGlobalBdds( Abc_Ntk_t * pNtk, int fLatchOnly ) { + int fReorder = 1; ProgressBar * pProgress; Abc_Obj_t * pNode; DdNode * bFunc; @@ -120,7 +103,8 @@ DdManager * Abc_NtkGlobalBdds( Abc_Ntk_t * pNtk ) // start the manager dd = Cudd_Init( Abc_NtkCiNum(pNtk), 0, CUDD_UNIQUE_SLOTS, CUDD_CACHE_SLOTS, 0 ); - Cudd_AutodynEnable( dd, CUDD_REORDER_SYMM_SIFT ); + if ( fReorder ) + Cudd_AutodynEnable( dd, CUDD_REORDER_SYMM_SIFT ); // set the elementary variables Abc_NtkCleanCopy( pNtk ); @@ -130,31 +114,60 @@ DdManager * Abc_NtkGlobalBdds( Abc_Ntk_t * pNtk ) pNode = Abc_AigConst1( pNtk->pManFunc ); pNode->pCopy = (Abc_Obj_t *)dd->one; Cudd_Ref( dd->one ); - // construct the BDDs - pProgress = Extra_ProgressBarStart( stdout, Abc_NtkCoNum(pNtk) ); - Abc_NtkForEachCo( pNtk, pNode, i ) + if ( fLatchOnly ) { - Extra_ProgressBarUpdate( pProgress, i, NULL ); - bFunc = Abc_NtkGlobalBdds_rec( dd, Abc_ObjFanin0(pNode) ); - if ( bFunc == NULL ) + // construct the BDDs + pProgress = Extra_ProgressBarStart( stdout, Abc_NtkLatchNum(pNtk) ); + Abc_NtkForEachLatch( pNtk, pNode, i ) { - printf( "Constructing global BDDs timed out.\n" ); - Extra_ProgressBarStop( pProgress ); - Cudd_Quit( dd ); - return NULL; + Extra_ProgressBarUpdate( pProgress, i, NULL ); + bFunc = Abc_NtkGlobalBdds_rec( dd, Abc_ObjFanin0(pNode) ); + if ( bFunc == NULL ) + { + printf( "Constructing global BDDs timed out.\n" ); + Extra_ProgressBarStop( pProgress ); + Cudd_Quit( dd ); + return NULL; + } + bFunc = Cudd_NotCond( bFunc, Abc_ObjFaninC0(pNode) ); + pNode->pNext = (Abc_Obj_t *)bFunc; Cudd_Ref( bFunc ); } - bFunc = Cudd_NotCond( bFunc, Abc_ObjFaninC0(pNode) ); - pNode->pNext = (Abc_Obj_t *)bFunc; Cudd_Ref( bFunc ); + Extra_ProgressBarStop( pProgress ); + } + else + { + // construct the BDDs + pProgress = Extra_ProgressBarStart( stdout, Abc_NtkCoNum(pNtk) ); + Abc_NtkForEachCo( pNtk, pNode, i ) + { + Extra_ProgressBarUpdate( pProgress, i, NULL ); + bFunc = Abc_NtkGlobalBdds_rec( dd, Abc_ObjFanin0(pNode) ); + if ( bFunc == NULL ) + { + printf( "Constructing global BDDs timed out.\n" ); + Extra_ProgressBarStop( pProgress ); + Cudd_Quit( dd ); + return NULL; + } + bFunc = Cudd_NotCond( bFunc, Abc_ObjFaninC0(pNode) ); + pNode->pNext = (Abc_Obj_t *)bFunc; Cudd_Ref( bFunc ); + } + Extra_ProgressBarStop( pProgress ); } - Extra_ProgressBarStop( pProgress ); // derefence the intermediate BDDs Abc_NtkForEachNode( pNtk, pNode, i ) if ( pNode->pCopy ) + { Cudd_RecursiveDeref( dd, (DdNode *)pNode->pCopy ); - Abc_NtkCleanCopy( pNtk ); + pNode->pCopy = NULL; + } // reorder one more time - Cudd_ReduceHeap( dd, CUDD_REORDER_SYMM_SIFT, 0 ); + if ( fReorder ) + { + Cudd_ReduceHeap( dd, CUDD_REORDER_SYMM_SIFT, 1 ); + Cudd_AutodynDisable( dd ); + } return dd; } @@ -227,9 +240,6 @@ Abc_Ntk_t * Abc_NtkFromGlobalBdds( DdManager * dd, Abc_Ntk_t * pNtk ) Extra_ProgressBarUpdate( pProgress, i, NULL ); pNodeNew = Abc_NodeFromGlobalBdds( pNtkNew, dd, (DdNode *)pNode->pNext ); Abc_ObjAddFanin( pNode->pCopy, pNodeNew ); - // deref the BDD of the PO - Cudd_RecursiveDeref( dd, (DdNode *)pNode->pNext ); - pNode->pNext = NULL; } Extra_ProgressBarStop( pProgress ); // transfer the names @@ -263,6 +273,30 @@ Abc_Obj_t * Abc_NodeFromGlobalBdds( Abc_Ntk_t * pNtkNew, DdManager * dd, DdNode return pNodeNew; } +/**Function************************************************************* + + Synopsis [Dereferences global functions of the network.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Abc_NtkFreeGlobalBdds( DdManager * dd, Abc_Ntk_t * pNtk ) +{ + Abc_Obj_t * pNode; + int i; + Abc_NtkForEachCo( pNtk, pNode, i ) + { + if ( pNode->pNext == NULL ) + continue; + Cudd_RecursiveDeref( dd, (DdNode *)pNode->pNext ); + pNode->pNext = NULL; + } +} + //////////////////////////////////////////////////////////////////////// /// END OF FILE /// diff --git a/src/base/abc/abcCreate.c b/src/base/abc/abcCreate.c index e4cfb7e3..5049a72e 100644 --- a/src/base/abc/abcCreate.c +++ b/src/base/abc/abcCreate.c @@ -157,34 +157,6 @@ void Abc_NtkFinalize( Abc_Ntk_t * pNtk, Abc_Ntk_t * pNtkNew ) /**Function************************************************************* - Synopsis [Finalizes the network using the existing network as a model.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -void Abc_NtkFinalizeRegular( Abc_Ntk_t * pNtk, Abc_Ntk_t * pNtkNew ) -{ - Abc_Obj_t * pObj, * pDriver, * pDriverNew; - int i; - assert( !Abc_NtkIsNetlist(pNtk) ); - // set the COs of the strashed network - Abc_NtkForEachCo( pNtk, pObj, i ) - { - pDriver = Abc_ObjFanin0(pObj); - pDriverNew = pDriver->pCopy; - Abc_ObjAddFanin( pObj->pCopy, pDriverNew ); - } - // transfer the names - Abc_NtkDupNameArrays( pNtk, pNtkNew ); - Abc_ManTimeDup( pNtk, pNtkNew ); -} - -/**Function************************************************************* - Synopsis [Duplicate the Ntk.] Description [] @@ -635,7 +607,58 @@ void Abc_NtkRemovePoNode( Abc_Obj_t * pNode ) ***********************************************************************/ Abc_Obj_t * Abc_NtkFindNode( Abc_Ntk_t * pNtk, char * pName ) { - return NULL; + Abc_Obj_t * pNode, * pDriver; + int i, Num; + // check if the node is among CIs + Abc_NtkForEachCi( pNtk, pNode, i ) + { + if ( strcmp( Abc_NtkNameCi(pNtk,i), pName ) == 0 ) + { + if ( i < Abc_NtkPiNum(pNtk) ) + printf( "Node \"%s\" is a primary input.\n", pName ); + else + printf( "Node \"%s\" is a latch output.\n", pName ); + return NULL; + } + } + // search the node among COs + Abc_NtkForEachCo( pNtk, pNode, i ) + { + if ( strcmp( Abc_NtkNameCo(pNtk,i), pName ) == 0 ) + { + pDriver = Abc_ObjFanin0(pNode); + if ( !Abc_ObjIsNode(pDriver) ) + { + printf( "Node \"%s\" does not have logic associated with it.\n", pName ); + return NULL; + } + return pDriver; + } + } + // find the internal node + if ( pName[0] != '[' || pName[strlen(pName)-1] != ']' ) + { + printf( "Node \"%s\" has non-standard name (expected name is \"[integer]\").\n", pName ); + return NULL; + } + Num = atoi( pName + 1 ); + if ( Num < 0 || Num > Abc_NtkObjNum(pNtk) ) + { + printf( "The node \"%s\" with ID %d is not in the current network.\n", pName, Num ); + return NULL; + } + pNode = Abc_NtkObj( pNtk, Num ); + if ( pNode == NULL ) + { + printf( "The node \"%s\" with ID %d has been removed from the current network.\n", pName, Num ); + return NULL; + } + if ( !Abc_ObjIsNode(pNode) ) + { + printf( "Object with ID %d is not a node.\n", Num ); + return NULL; + } + return pNode; } /**Function************************************************************* @@ -997,6 +1020,27 @@ Abc_Obj_t * Abc_NodeCreateMux( Abc_Ntk_t * pNtk, Abc_Obj_t * pNodeC, Abc_Obj_t * return pNode; } +/**Function************************************************************* + + Synopsis [Clones the given node but does not assign the function.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Abc_Obj_t * Abc_NodeClone( Abc_Obj_t * pNode ) +{ + Abc_Obj_t * pClone, * pFanin; + int i; + assert( Abc_ObjIsNode(pNode) ); + pClone = Abc_NtkCreateNode( pNode->pNtk ); + Abc_ObjForEachFanin( pNode, pFanin, i ) + Abc_ObjAddFanin( pClone, pFanin ); + return pClone; +} diff --git a/src/base/abc/abcDsd.c b/src/base/abc/abcDsd.c index 47b288d3..c9adab38 100644 --- a/src/base/abc/abcDsd.c +++ b/src/base/abc/abcDsd.c @@ -19,18 +19,443 @@ ***********************************************************************/ #include "abc.h" +#include "dsd.h" //////////////////////////////////////////////////////////////////////// /// DECLARATIONS /// //////////////////////////////////////////////////////////////////////// +static Abc_Ntk_t * Abc_NtkDsdInternal( DdManager * dd, Abc_Ntk_t * pNtk, bool fVerbose, bool fPrint, bool fShort ); +static Dsd_Manager_t * Abc_NtkDsdPerform( DdManager * dd, Abc_Ntk_t * pNtk, bool fVerbose ); +static void Abc_NtkDsdConstruct( Dsd_Manager_t * pManDsd, Abc_Ntk_t * pNtk, Abc_Ntk_t * pNtkNew ); +static Abc_Obj_t * Abc_NtkDsdConstructNode( Dsd_Manager_t * pManDsd, Dsd_Node_t * pNodeDsd, Abc_Ntk_t * pNtkNew ); + +static Vec_Ptr_t * Abc_NtkCollectNodesForDsd( Abc_Ntk_t * pNtk ); +static void Abc_NodeDecompDsdAndMux( Abc_Obj_t * pNode, Vec_Ptr_t * vNodes, Dsd_Manager_t * pManDsd ); +static bool Abc_NodeIsForDsd( Abc_Obj_t * pNode ); +static int Abc_NodeFindMuxVar( DdManager * dd, DdNode * bFunc, int nVars ); + //////////////////////////////////////////////////////////////////////// /// FUNCTION DEFITIONS /// //////////////////////////////////////////////////////////////////////// /**Function************************************************************* - Synopsis [Decomposes the network using disjoint-support decomposition.] + Synopsis [Derives the DSD network.] + + Description [Takes the strashed network (pNtk), derives global BDDs for + the combinational outputs of this network, and decomposes these BDDs using + disjoint support decomposition. Finally, constructs and return a new + network, which is topologically equivalent to the decomposition tree. + Allocates and frees a new BDD manager and a new DSD manager.] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Abc_Ntk_t * Abc_NtkDsdGlobal( Abc_Ntk_t * pNtk, bool fVerbose, bool fPrint, bool fShort ) +{ + int fCheck = 1; + Abc_Ntk_t * pNtkNew; + DdManager * dd; + + assert( Abc_NtkIsAig(pNtk) ); + + // perform FPGA mapping + dd = Abc_NtkGlobalBdds( pNtk, 0 ); + if ( dd == NULL ) + return NULL; + if ( fVerbose ) + printf( "The shared BDD size is %d nodes.\n", Cudd_ReadKeys(dd) - Cudd_ReadDead(dd) ); + + // transform the result of mapping into a BDD network + pNtkNew = Abc_NtkDsdInternal( dd, pNtk, fVerbose, fPrint, fShort ); + if ( pNtkNew == NULL ) + { + Cudd_Quit( dd ); + return NULL; + } + Extra_StopManager( dd ); + + // make sure that everything is okay + if ( fCheck && !Abc_NtkCheck( pNtkNew ) ) + { + printf( "Abc_NtkDsdGlobal: The network check has failed.\n" ); + Abc_NtkDelete( pNtkNew ); + return NULL; + } + return pNtkNew; +} + +/**Function************************************************************* + + Synopsis [Constructs the decomposed network.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Abc_Ntk_t * Abc_NtkDsdInternal( DdManager * dd, Abc_Ntk_t * pNtk, bool fVerbose, bool fPrint, bool fShort ) +{ + Dsd_Manager_t * pManDsd; + Abc_Ntk_t * pNtkNew; + + // perform the decomposition + pManDsd = Abc_NtkDsdPerform( dd, pNtk, fVerbose ); + Abc_NtkFreeGlobalBdds( dd, pNtk ); + if ( pManDsd == NULL ) + return NULL; + + // start the new network + pNtkNew = Abc_NtkStartFrom( pNtk, ABC_NTK_LOGIC_BDD ); + // make sure the new manager has enough inputs + Cudd_bddIthVar( pNtkNew->pManFunc, dd->size-1 ); + // put the results into the new network (save new CO drivers in old CO drivers) + Abc_NtkDsdConstruct( pManDsd, pNtk, pNtkNew ); + // finalize the new network + Abc_NtkFinalize( pNtk, pNtkNew ); + + if ( fPrint ) + Dsd_TreePrint( stdout, pManDsd, (char **)pNtk->vNamesPi->pArray, (char **)pNtk->vNamesPo->pArray, fShort, -1 ); + + // stop the DSD manager + Dsd_ManagerStop( pManDsd ); + return pNtkNew; +} + +/**Function************************************************************* + + Synopsis [Performs DSD by creating the manager and decomposing the functions.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Dsd_Manager_t * Abc_NtkDsdPerform( DdManager * dd, Abc_Ntk_t * pNtk, bool fVerbose ) +{ + Dsd_Manager_t * pManDsd; + DdNode ** pbFuncsGlo; + Abc_Obj_t * pNode; + int i; + + // collect global functions into the array + pbFuncsGlo = ALLOC( DdNode *, Abc_NtkCoNum(pNtk) ); + Abc_NtkForEachCo( pNtk, pNode, i ) + { + pbFuncsGlo[i] = Cudd_NotCond( pNode->pNext, Abc_ObjFaninC0(pNode) ); +//printf( "Output %3d : Support size = %3d. Nodes = %5d.\n", i, Cudd_SupportSize(dd, pbFuncsGlo[i]), Cudd_DagSize(pbFuncsGlo[i]) ); + } + + // start the DSD manager and decompose global functions + pManDsd = Dsd_ManagerStart( dd, Abc_NtkCiNum(pNtk), fVerbose ); + Dsd_Decompose( pManDsd, pbFuncsGlo, Abc_NtkCoNum(pNtk) ); + FREE( pbFuncsGlo ); + return pManDsd; +} + +/**Function************************************************************* + + Synopsis [Constructs the decomposed network.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Abc_NtkDsdConstruct( Dsd_Manager_t * pManDsd, Abc_Ntk_t * pNtk, Abc_Ntk_t * pNtkNew ) +{ + Dsd_Node_t ** ppNodesDsd; + Dsd_Node_t * pNodeDsd; + Abc_Obj_t * pNode, * pNodeNew, * pDriver, * pConst1; + int i, nNodesDsd; + + // save the CI nodes in the DSD nodes + Abc_NtkForEachCi( pNtk, pNode, i ) + { + pNodeDsd = Dsd_ManagerReadInput( pManDsd, i ); + Dsd_NodeSetMark( pNodeDsd, (int)pNode->pCopy ); + } + // set the constant node + pConst1 = Abc_AigConst1(pNtk->pManFunc); + if ( Abc_ObjFanoutNum(pConst1) > 0 ) + pConst1->pCopy = Abc_NodeCreateConst1(pNtkNew); + + // collect DSD nodes in DFS order (leaves and const1 are not collected) + ppNodesDsd = Dsd_TreeCollectNodesDfs( pManDsd, &nNodesDsd ); + for ( i = 0; i < nNodesDsd; i++ ) + Abc_NtkDsdConstructNode( pManDsd, ppNodesDsd[i], pNtkNew ); + free( ppNodesDsd ); + + // set the pointers to the CO drivers + Abc_NtkForEachCo( pNtk, pNode, i ) + { + pDriver = Abc_ObjFanin0( pNode ); + if ( !Abc_ObjIsNode(pDriver) ) + continue; + pNodeDsd = Dsd_ManagerReadRoot( pManDsd, i ); + pNodeNew = (Abc_Obj_t *)Dsd_NodeReadMark( Dsd_Regular(pNodeDsd) ); + assert( !Abc_ObjIsComplement(pNodeNew) ); + pDriver->pCopy = Abc_ObjNotCond( pNodeNew, Dsd_IsComplement(pNodeDsd) ); + } +} + +/**Function************************************************************* + + Synopsis [Performs DSD using the manager.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Abc_Obj_t * Abc_NtkDsdConstructNode( Dsd_Manager_t * pManDsd, Dsd_Node_t * pNodeDsd, Abc_Ntk_t * pNtkNew ) +{ + DdManager * ddDsd = Dsd_ManagerReadDd( pManDsd ); + DdManager * ddNew = pNtkNew->pManFunc; + Dsd_Node_t * pFaninDsd; + Abc_Obj_t * pNodeNew, * pFanin; + DdNode * bLocal, * bTemp, * bVar; + Dsd_Type_t Type; + int i, nDecs; + + // create the new node + pNodeNew = Abc_NtkCreateNode( pNtkNew ); + // add the fanins + Type = Dsd_NodeReadType( pNodeDsd ); + nDecs = Dsd_NodeReadDecsNum( pNodeDsd ); + assert( nDecs > 1 ); + for ( i = 0; i < nDecs; i++ ) + { + pFaninDsd = Dsd_NodeReadDec( pNodeDsd, i ); + pFanin = (Abc_Obj_t *)Dsd_NodeReadMark(Dsd_Regular(pFaninDsd)); + Abc_ObjAddFanin( pNodeNew, pFanin ); + assert( Type == DSD_NODE_OR || !Dsd_IsComplement(pFaninDsd) ); + } + + // create the local function depending on the type of the node + ddNew = pNtkNew->pManFunc; + switch ( Type ) + { + case DSD_NODE_CONST1: + { + bLocal = ddNew->one; Cudd_Ref( bLocal ); + break; + } + case DSD_NODE_OR: + { + bLocal = Cudd_Not(ddNew->one); Cudd_Ref( bLocal ); + for ( i = 0; i < nDecs; i++ ) + { + pFaninDsd = Dsd_NodeReadDec( pNodeDsd, i ); + bVar = Cudd_NotCond( ddNew->vars[i], Dsd_IsComplement(pFaninDsd) ); + bLocal = Cudd_bddOr( ddNew, bTemp = bLocal, bVar ); Cudd_Ref( bLocal ); + Cudd_RecursiveDeref( ddNew, bTemp ); + } + break; + } + case DSD_NODE_EXOR: + { + bLocal = Cudd_Not(ddNew->one); Cudd_Ref( bLocal ); + for ( i = 0; i < nDecs; i++ ) + { + bLocal = Cudd_bddXor( ddNew, bTemp = bLocal, ddNew->vars[i] ); Cudd_Ref( bLocal ); + Cudd_RecursiveDeref( ddNew, bTemp ); + } + break; + } + case DSD_NODE_PRIME: + { + bLocal = Dsd_TreeGetPrimeFunction( ddDsd, pNodeDsd ); Cudd_Ref( bLocal ); + bLocal = Extra_TransferLevelByLevel( ddDsd, ddNew, bTemp = bLocal ); Cudd_Ref( bLocal ); + Cudd_RecursiveDeref( ddDsd, bTemp ); + // bLocal is now in the new BDD manager + break; + } + default: + { + assert( 0 ); + break; + } + } + pNodeNew->pData = bLocal; + Dsd_NodeSetMark( pNodeDsd, (int)pNodeNew ); + return pNodeNew; +} + + + + + + +/**Function************************************************************* + + Synopsis [Recursively decomposes internal nodes.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Abc_NtkDsdRecursive( Abc_Ntk_t * pNtk, bool fVerbose ) +{ + int fCheck = 1; + Dsd_Manager_t * pManDsd; + DdManager * dd = pNtk->pManFunc; + Vec_Ptr_t * vNodes; + int i; + + assert( Abc_NtkIsLogicBdd(pNtk) ); + + // make the network minimum base + Abc_NtkMinimumBase( pNtk ); + + // start the DSD manager + pManDsd = Dsd_ManagerStart( dd, dd->size, 0 ); + + // collect nodes for decomposition + vNodes = Abc_NtkCollectNodesForDsd( pNtk ); + for ( i = 0; i < vNodes->nSize; i++ ) + Abc_NodeDecompDsdAndMux( vNodes->pArray[i], vNodes, pManDsd ); + Vec_PtrFree( vNodes ); + + // stop the DSD manager + Dsd_ManagerStop( pManDsd ); + + // make sure everything is okay + if ( fCheck && !Abc_NtkCheck( pNtk ) ) + { + printf( "Abc_NtkDsdRecursive: The network check has failed.\n" ); + return 0; + } + return 1; +} + +/**Function************************************************************* + + Synopsis [Collects the nodes that may need decomposition.] + + Description [The nodes that do not need decomposition are those + whose BDD has more internal nodes than the support size.] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Vec_Ptr_t * Abc_NtkCollectNodesForDsd( Abc_Ntk_t * pNtk ) +{ + Vec_Ptr_t * vNodes; + Abc_Obj_t * pNode; + int i; + vNodes = Vec_PtrAlloc( 100 ); + Abc_NtkForEachNode( pNtk, pNode, i ) + { + if ( Abc_NodeIsForDsd(pNode) ) + Vec_PtrPush( vNodes, pNode ); + } + return vNodes; +} + +/**Function************************************************************* + + Synopsis [Performs decomposition of one node.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Abc_NodeDecompDsdAndMux( Abc_Obj_t * pNode, Vec_Ptr_t * vNodes, Dsd_Manager_t * pManDsd ) +{ + DdManager * dd = pNode->pNtk->pManFunc; + Abc_Obj_t * pRoot, * pFanin, * pNode1, * pNode2, * pNodeC; + Dsd_Node_t ** ppNodesDsd, * pNodeDsd, * pFaninDsd; + int i, nNodesDsd, iVar, fCompl; + + // try disjoint support decomposition + pNodeDsd = Dsd_DecomposeOne( pManDsd, pNode->pData ); + fCompl = Dsd_IsComplement( pNodeDsd ); + pNodeDsd = Dsd_Regular( pNodeDsd ); + + // determine what decomposition to use + if ( Dsd_NodeReadDecsNum(pNodeDsd) != Abc_ObjFaninNum(pNode) ) + { // perform DSD + + // set the inputs + Abc_ObjForEachFanin( pNode, pFanin, i ) + { + pFaninDsd = Dsd_ManagerReadInput( pManDsd, i ); + Dsd_NodeSetMark( pFaninDsd, (int)pFanin ); + } + + // construct the intermediate nodes + ppNodesDsd = Dsd_TreeCollectNodesDfsOne( pManDsd, pNodeDsd, &nNodesDsd ); + for ( i = 0; i < nNodesDsd; i++ ) + { + pRoot = Abc_NtkDsdConstructNode( pManDsd, ppNodesDsd[i], pNode->pNtk ); + if ( Abc_NodeIsForDsd(pRoot) ) + Vec_PtrPush( vNodes, pRoot ); + } + free( ppNodesDsd ); + + // remove the current fanins + Abc_ObjRemoveFanins( pNode ); + // add fanin to the root + Abc_ObjAddFanin( pNode, pRoot ); + // update the function to be that of buffer + Cudd_RecursiveDeref( dd, pNode->pData ); + pNode->pData = Cudd_NotCond( dd->vars[0], fCompl ); Cudd_Ref( pNode->pData ); + } + else // perform MUX-decomposition + { + // get the cofactoring variable + iVar = Abc_NodeFindMuxVar( dd, pNode->pData, Abc_ObjFaninNum(pNode) ); + pNodeC = Abc_ObjFanin( pNode, iVar ); + + // get the negative cofactor + pNode1 = Abc_NodeClone( pNode ); + pNode1->pData = Cudd_Cofactor( dd, pNode->pData, Cudd_Not(dd->vars[iVar]) ); Cudd_Ref( pNode1->pData ); + Abc_NodeMinimumBase( pNode1 ); + if ( Abc_NodeIsForDsd(pNode1) ) + Vec_PtrPush( vNodes, pNode1 ); + + // get the positive cofactor + pNode2 = Abc_NodeClone( pNode ); + pNode2->pData = Cudd_Cofactor( dd, pNode->pData, dd->vars[iVar] ); Cudd_Ref( pNode2->pData ); + Abc_NodeMinimumBase( pNode2 ); + if ( Abc_NodeIsForDsd(pNode2) ) + Vec_PtrPush( vNodes, pNode2 ); + + // remove the current fanins + Abc_ObjRemoveFanins( pNode ); + // add new fanins + Abc_ObjAddFanin( pNode, pNodeC ); + Abc_ObjAddFanin( pNode, pNode2 ); + Abc_ObjAddFanin( pNode, pNode1 ); + // update the function to be that of MUX + Cudd_RecursiveDeref( dd, pNode->pData ); + pNode->pData = Cudd_bddIte( dd, dd->vars[0], dd->vars[1], dd->vars[2] ); Cudd_Ref( pNode->pData ); + } +} + +/**Function************************************************************* + + Synopsis [Performs decomposition of one node.] Description [] @@ -39,7 +464,64 @@ SeeAlso [] ***********************************************************************/ +bool Abc_NodeIsForDsd( Abc_Obj_t * pNode ) +{ + assert( Abc_ObjIsNode(pNode) ); + if ( Cudd_DagSize(pNode->pData)-1 > Abc_ObjFaninNum(pNode) ) + return 1; + return 0; +} + +/**Function************************************************************* + + Synopsis [Determines a cofactoring variable.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Abc_NodeFindMuxVar( DdManager * dd, DdNode * bFunc, int nVars ) +{ + DdNode * bVar, * bCof0, * bCof1; + int SuppSumMin = 1000000; + int i, nSSD, nSSQ, iVar; + +// printf( "\n\nCofactors:\n\n" ); + iVar = -1; + for ( i = 0; i < nVars; i++ ) + { + bVar = dd->vars[i]; + + bCof0 = Cudd_Cofactor( dd, bFunc, Cudd_Not(bVar) ); Cudd_Ref( bCof0 ); + bCof1 = Cudd_Cofactor( dd, bFunc, bVar ); Cudd_Ref( bCof1 ); + +// nodD = Cudd_DagSize(bCof0); +// nodQ = Cudd_DagSize(bCof1); +// printf( "+%02d: D=%2d. Q=%2d. ", i, nodD, nodQ ); +// printf( "S=%2d. D=%2d. ", nodD + nodQ, abs(nodD-nodQ) ); + + nSSD = Cudd_SupportSize( dd, bCof0 ); + nSSQ = Cudd_SupportSize( dd, bCof1 ); + +// printf( "SD=%2d. SQ=%2d. ", nSSD, nSSQ ); +// printf( "S=%2d. D=%2d. ", nSSD + nSSQ, abs(nSSD - nSSQ) ); +// printf( "Cost=%3d. ", Cost(nodD,nodQ,nSSD,nSSQ) ); +// printf( "\n" ); + + Cudd_RecursiveDeref( dd, bCof0 ); + Cudd_RecursiveDeref( dd, bCof1 ); + if ( SuppSumMin > nSSD + nSSQ ) + { + SuppSumMin = nSSD + nSSQ; + iVar = i; + } + } + return iVar; +} //////////////////////////////////////////////////////////////////////// /// END OF FILE /// diff --git a/src/base/abc/abcFanio.c b/src/base/abc/abcFanio.c index 51fc73ce..866c6e5d 100644 --- a/src/base/abc/abcFanio.c +++ b/src/base/abc/abcFanio.c @@ -85,6 +85,32 @@ void Abc_ObjDeleteFanin( Abc_Obj_t * pObj, Abc_Obj_t * pFanin ) } } + +/**Function************************************************************* + + Synopsis [Destroys fanout/fanin relationship between the nodes.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Abc_ObjRemoveFanins( Abc_Obj_t * pObj ) +{ + Vec_Fan_t * vFaninsOld; + Abc_Obj_t * pFanin; + int k; + // remove old fanins + vFaninsOld = &pObj->vFanins; + for ( k = vFaninsOld->nSize - 1; k >= 0; k-- ) + { + pFanin = Abc_NtkObj( pObj->pNtk, vFaninsOld->pArray[k].iFan ); + Abc_ObjDeleteFanin( pObj, pFanin ); + } +} + /**Function************************************************************* Synopsis [Replaces a fanin of the node.] diff --git a/src/base/abc/abcFraig.c b/src/base/abc/abcFraig.c index 85dba6f3..75c5c290 100644 --- a/src/base/abc/abcFraig.c +++ b/src/base/abc/abcFraig.c @@ -435,7 +435,7 @@ int Abc_NtkFraigStore( Abc_Ntk_t * pNtk ) if ( pStore == NULL ) { // start the stored network - pStore = Abc_NtkStrash( pNtk ); + pStore = Abc_NtkStrash( pNtk, 0 ); if ( pStore == NULL ) { printf( "Abc_NtkFraigStore: Initial strashing has failed.\n" ); diff --git a/src/base/abc/abcFunc.c b/src/base/abc/abcFunc.c index 59f0dc34..a040758e 100644 --- a/src/base/abc/abcFunc.c +++ b/src/base/abc/abcFunc.c @@ -166,7 +166,7 @@ int Abc_NtkBddToSop( Abc_Ntk_t * pNtk ) assert( pNode->pData ); bFunc = pNode->pData; //Extra_bddPrint( dd, bFunc ); printf( "\n" ); printf( "\n" ); - pNode->pData = Abc_ConvertBddToSop( pNtk->pManFunc, dd, bFunc, Abc_ObjFaninNum(pNode), vCube, -1 ); + pNode->pData = Abc_ConvertBddToSop( pNtk->pManFunc, dd, bFunc, bFunc, Abc_ObjFaninNum(pNode), vCube, -1 ); if ( pNode->pData == NULL ) return 0; Cudd_RecursiveDeref( dd, bFunc ); @@ -193,18 +193,20 @@ int Abc_NtkBddToSop( Abc_Ntk_t * pNtk ) SeeAlso [] ***********************************************************************/ -char * Abc_ConvertBddToSop( Extra_MmFlex_t * pMan, DdManager * dd, DdNode * bFunc, int nFanins, Vec_Str_t * vCube, int fMode ) +char * Abc_ConvertBddToSop( Extra_MmFlex_t * pMan, DdManager * dd, DdNode * bFuncOn, DdNode * bFuncOnDc, int nFanins, Vec_Str_t * vCube, int fMode ) { + int fVerify = 1; char * pSop; DdNode * bFuncNew, * bCover, * zCover, * zCover0, * zCover1; int nCubes, nCubes0, nCubes1, fPhase; - if ( Cudd_IsConstant(bFunc) ) + assert( bFuncOn == bFuncOnDc || Cudd_bddLeq( dd, bFuncOn, bFuncOnDc ) ); + if ( Cudd_IsConstant(bFuncOn) || Cudd_IsConstant(bFuncOnDc) ) { Vec_StrFill( vCube, nFanins, '-' ); Vec_StrPush( vCube, '\0' ); pSop = Extra_MmFlexEntryFetch( pMan, nFanins + 4 ); - if ( bFunc == Cudd_ReadLogicZero(dd) ) + if ( bFuncOn == Cudd_ReadLogicZero(dd) ) sprintf( pSop, "%s 0\n", vCube->pArray ); else sprintf( pSop, "%s 1\n", vCube->pArray ); @@ -216,14 +218,14 @@ char * Abc_ConvertBddToSop( Extra_MmFlex_t * pMan, DdManager * dd, DdNode * bFun { // try both phases // get the ZDD of the negative polarity - bCover = Cudd_zddIsop( dd, Cudd_Not(bFunc), Cudd_Not(bFunc), &zCover0 ); + bCover = Cudd_zddIsop( dd, Cudd_Not(bFuncOnDc), Cudd_Not(bFuncOn), &zCover0 ); Cudd_Ref( zCover0 ); Cudd_Ref( bCover ); Cudd_RecursiveDeref( dd, bCover ); nCubes0 = Abc_CountZddCubes( dd, zCover0 ); // get the ZDD of the positive polarity - bCover = Cudd_zddIsop( dd, bFunc, bFunc, &zCover1 ); + bCover = Cudd_zddIsop( dd, bFuncOn, bFuncOnDc, &zCover1 ); Cudd_Ref( zCover1 ); Cudd_Ref( bCover ); Cudd_RecursiveDeref( dd, bCover ); @@ -248,7 +250,7 @@ char * Abc_ConvertBddToSop( Extra_MmFlex_t * pMan, DdManager * dd, DdNode * bFun else if ( fMode == 0 ) { // get the ZDD of the positive polarity - bCover = Cudd_zddIsop( dd, Cudd_Not(bFunc), Cudd_Not(bFunc), &zCover ); + bCover = Cudd_zddIsop( dd, Cudd_Not(bFuncOnDc), Cudd_Not(bFuncOn), &zCover ); Cudd_Ref( zCover ); Cudd_Ref( bCover ); Cudd_RecursiveDeref( dd, bCover ); @@ -258,7 +260,7 @@ char * Abc_ConvertBddToSop( Extra_MmFlex_t * pMan, DdManager * dd, DdNode * bFun else if ( fMode == 1 ) { // get the ZDD of the positive polarity - bCover = Cudd_zddIsop( dd, bFunc, bFunc, &zCover ); + bCover = Cudd_zddIsop( dd, bFuncOn, bFuncOnDc, &zCover ); Cudd_Ref( zCover ); Cudd_Ref( bCover ); Cudd_RecursiveDeref( dd, bCover ); @@ -271,7 +273,10 @@ char * Abc_ConvertBddToSop( Extra_MmFlex_t * pMan, DdManager * dd, DdNode * bFun } // allocate memory for the cover - pSop = Extra_MmFlexEntryFetch( pMan, (nFanins + 3) * nCubes + 1 ); + if ( pMan ) + pSop = Extra_MmFlexEntryFetch( pMan, (nFanins + 3) * nCubes + 1 ); + else + pSop = ALLOC( char, (nFanins + 3) * nCubes + 1 ); pSop[(nFanins + 3) * nCubes] = 0; // create the SOP Vec_StrFill( vCube, nFanins, '-' ); @@ -280,12 +285,21 @@ char * Abc_ConvertBddToSop( Extra_MmFlex_t * pMan, DdManager * dd, DdNode * bFun Cudd_RecursiveDerefZdd( dd, zCover ); // verify - bFuncNew = Abc_ConvertSopToBdd( dd, pSop, nFanins ); Cudd_Ref( bFuncNew ); -//Extra_bddPrint( dd, bFunc ); -//Extra_bddPrint( dd, bFuncNew ); - if ( bFuncNew != bFunc ) - printf( "Verification failed.\n" ); - Cudd_RecursiveDeref( dd, bFuncNew ); + if ( fVerify ) + { + bFuncNew = Abc_ConvertSopToBdd( dd, pSop, nFanins ); Cudd_Ref( bFuncNew ); + if ( bFuncOn == bFuncOnDc ) + { + if ( bFuncNew != bFuncOn ) + printf( "Verification failed.\n" ); + } + else + { + if ( !Cudd_bddLeq(dd, bFuncOn, bFuncNew) || !Cudd_bddLeq(dd, bFuncNew, bFuncOnDc) ) + printf( "Verification failed.\n" ); + } + Cudd_RecursiveDeref( dd, bFuncNew ); + } return pSop; } @@ -359,8 +373,8 @@ int Abc_ConvertZddToSop( DdManager * dd, DdNode * zCover, char * pSop, int nFani void Abc_NodeBddToCnf( Abc_Obj_t * pNode, Extra_MmFlex_t * pMmMan, Vec_Str_t * vCube, char ** ppSop0, char ** ppSop1 ) { assert( Abc_NtkIsLogicBdd(pNode->pNtk) ); - *ppSop0 = Abc_ConvertBddToSop( pMmMan, pNode->pNtk->pManFunc, pNode->pData, Abc_ObjFaninNum(pNode), vCube, 0 ); - *ppSop1 = Abc_ConvertBddToSop( pMmMan, pNode->pNtk->pManFunc, pNode->pData, Abc_ObjFaninNum(pNode), vCube, 1 ); + *ppSop0 = Abc_ConvertBddToSop( pMmMan, pNode->pNtk->pManFunc, pNode->pData, pNode->pData, Abc_ObjFaninNum(pNode), vCube, 0 ); + *ppSop1 = Abc_ConvertBddToSop( pMmMan, pNode->pNtk->pManFunc, pNode->pData, pNode->pData, Abc_ObjFaninNum(pNode), vCube, 1 ); } diff --git a/src/base/abc/abcFxu.c b/src/base/abc/abcFxu.c index 99f37dfc..bbfef208 100644 --- a/src/base/abc/abcFxu.c +++ b/src/base/abc/abcFxu.c @@ -52,6 +52,8 @@ static void Abc_NtkFxuReconstruct( Abc_Ntk_t * pNtk, Fxu_Data_t * p ); ***********************************************************************/ bool Abc_NtkFastExtract( Abc_Ntk_t * pNtk, Fxu_Data_t * p ) { + int fCheck = 1; + assert( Abc_NtkIsLogicBdd(pNtk) || Abc_NtkIsLogicSop(pNtk) ); // convert nodes to SOPs if ( Abc_NtkIsLogicBdd(pNtk) ) @@ -70,20 +72,19 @@ bool Abc_NtkFastExtract( Abc_Ntk_t * pNtk, Fxu_Data_t * p ) // sweep removes useless nodes Abc_NtkCleanup( pNtk, 0 ); // collect information about the covers - // make sure all covers are SCC free - // allocate literal array for each cover Abc_NtkFxuCollectInfo( pNtk, p ); // call the fast extract procedure - // returns the number of divisor extracted if ( Fxu_FastExtract(p) > 0 ) { // update the network Abc_NtkFxuReconstruct( pNtk, p ); // make sure everything is okay - if ( !Abc_NtkCheck( pNtk ) ) + if ( fCheck && !Abc_NtkCheck( pNtk ) ) printf( "Abc_NtkFastExtract: The network check has failed.\n" ); return 1; } + else + printf( "Warning: The network has not been changed by \"fx\".\n" ); return 0; } @@ -199,7 +200,6 @@ void Abc_NtkFxuFreeInfo( Fxu_Data_t * p ) ***********************************************************************/ void Abc_NtkFxuReconstruct( Abc_Ntk_t * pNtk, Fxu_Data_t * p ) { - Vec_Fan_t * vFaninsOld; Vec_Int_t * vFanins; Abc_Obj_t * pNode, * pFanin; int i, k; @@ -221,12 +221,7 @@ void Abc_NtkFxuReconstruct( Abc_Ntk_t * pNtk, Fxu_Data_t * p ) continue; // remove old fanins pNode = Abc_NtkObj( pNtk, i ); - vFaninsOld = &pNode->vFanins; - for ( k = vFaninsOld->nSize - 1; k >= 0; k-- ) - { - pFanin = Abc_NtkObj( pNtk, vFaninsOld->pArray[k].iFan ); - Abc_ObjDeleteFanin( pNode, pFanin ); - } + Abc_ObjRemoveFanins( pNode ); // add new fanins vFanins = p->vFaninsNew->pArray[i]; for ( k = 0; k < vFanins->nSize; k++ ) diff --git a/src/base/abc/abcMap.c b/src/base/abc/abcMap.c index 7289b47b..e5f4e104 100644 --- a/src/base/abc/abcMap.c +++ b/src/base/abc/abcMap.c @@ -353,7 +353,7 @@ Abc_Obj_t * Abc_NodeFromMapSuper_rec( Abc_Ntk_t * pNtkNew, Map_Node_t * pNodeMap } else { - assert( 0 ); +// assert( 0 ); /* It might happen that a super gate with 5 inputs is constructed that * actually depends only on the first four variables; i.e the fifth is a * don't care -- in that case we connect constant node for the fifth diff --git a/src/base/abc/abcMiter.c b/src/base/abc/abcMiter.c index f1037dd2..f72fab0f 100644 --- a/src/base/abc/abcMiter.c +++ b/src/base/abc/abcMiter.c @@ -51,8 +51,8 @@ Abc_Ntk_t * Abc_NtkMiter( Abc_Ntk_t * pNtk1, Abc_Ntk_t * pNtk2, int fComb ) Abc_Ntk_t * pTemp = NULL; int fRemove1, fRemove2; // make sure the circuits are strashed - fRemove1 = (!Abc_NtkIsAig(pNtk1)) && (pNtk1 = Abc_NtkStrash(pNtk1)); - fRemove2 = (!Abc_NtkIsAig(pNtk2)) && (pNtk2 = Abc_NtkStrash(pNtk2)); + fRemove1 = (!Abc_NtkIsAig(pNtk1)) && (pNtk1 = Abc_NtkStrash(pNtk1, 0)); + fRemove2 = (!Abc_NtkIsAig(pNtk2)) && (pNtk2 = Abc_NtkStrash(pNtk2, 0)); if ( pNtk1 && pNtk2 ) { // check that the networks have the same PIs/POs/latches diff --git a/src/base/abc/abcPrint.c b/src/base/abc/abcPrint.c index 49b6db72..c3e3107c 100644 --- a/src/base/abc/abcPrint.c +++ b/src/base/abc/abcPrint.c @@ -52,7 +52,10 @@ void Abc_NtkPrintStats( FILE * pFile, Abc_Ntk_t * pNtk ) fprintf( pFile, " nd = %5d", Abc_NtkNodeNum(pNtk) ); } else if ( Abc_NtkIsAig(pNtk) ) + { fprintf( pFile, " and = %5d", Abc_NtkNodeNum(pNtk) ); + fprintf( pFile, " choice = %5d", Abc_NtkCountChoiceNodes(pNtk) ); + } else fprintf( pFile, " nd = %5d", Abc_NtkNodeNum(pNtk) ); @@ -86,19 +89,19 @@ void Abc_NtkPrintStats( FILE * pFile, Abc_Ntk_t * pNtk ) ***********************************************************************/ void Abc_NtkPrintIo( FILE * pFile, Abc_Ntk_t * pNtk ) { - Abc_Obj_t * pNet, * pLatch; + Abc_Obj_t * pObj, * pLatch; int i; if ( Abc_NtkIsNetlist(pNtk) ) { fprintf( pFile, "Primary inputs (%d): ", Abc_NtkPiNum(pNtk) ); - Abc_NtkForEachPi( pNtk, pNet, i ) - fprintf( pFile, " %s", Abc_ObjName(pNet) ); + Abc_NtkForEachPi( pNtk, pObj, i ) + fprintf( pFile, " %s", Abc_ObjName(pObj) ); fprintf( pFile, "\n" ); fprintf( pFile, "Primary outputs (%d):", Abc_NtkPoNum(pNtk) ); - Abc_NtkForEachPo( pNtk, pNet, i ) - fprintf( pFile, " %s", Abc_ObjName(pNet) ); + Abc_NtkForEachPo( pNtk, pObj, i ) + fprintf( pFile, " %s", Abc_ObjName(pObj) ); fprintf( pFile, "\n" ); fprintf( pFile, "Latches (%d): ", Abc_NtkLatchNum(pNtk) ); @@ -109,12 +112,12 @@ void Abc_NtkPrintIo( FILE * pFile, Abc_Ntk_t * pNtk ) else { fprintf( pFile, "Primary inputs (%d): ", Abc_NtkPiNum(pNtk) ); - Abc_NtkForEachPi( pNtk, pNet, i ) + Abc_NtkForEachPi( pNtk, pObj, i ) fprintf( pFile, " %s", pNtk->vNamesPi->pArray[i] ); fprintf( pFile, "\n" ); fprintf( pFile, "Primary outputs (%d):", Abc_NtkPoNum(pNtk) ); - Abc_NtkForEachPo( pNtk, pNet, i ) + Abc_NtkForEachPo( pNtk, pObj, i ) fprintf( pFile, " %s", pNtk->vNamesPo->pArray[i] ); fprintf( pFile, "\n" ); @@ -280,7 +283,6 @@ void Abc_NodePrintFactor( FILE * pFile, Abc_Obj_t * pNode ) Vec_IntFree( vFactor ); } - //////////////////////////////////////////////////////////////////////// /// END OF FILE /// //////////////////////////////////////////////////////////////////////// diff --git a/src/base/abc/abcRes.c b/src/base/abc/abcRes.c new file mode 100644 index 00000000..658c8229 --- /dev/null +++ b/src/base/abc/abcRes.c @@ -0,0 +1,537 @@ +/**CFile**************************************************************** + + FileName [abcRes.c] + + SystemName [ABC: Logic synthesis and verification system.] + + PackageName [Network and node package.] + + Synopsis [Technology-independent resynthesis of the AIG.] + + Author [Alan Mishchenko] + + Affiliation [UC Berkeley] + + Date [Ver. 1.0. Started - June 20, 2005.] + + Revision [$Id: abcRes.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $] + +***********************************************************************/ + +#include "abc.h" +#include "ft.h" + +//////////////////////////////////////////////////////////////////////// +/// DECLARATIONS /// +//////////////////////////////////////////////////////////////////////// + +static void Abc_NodeResyn( Abc_ManRes_t * p ); + +static void Abc_NodeFindCut( Abc_ManRes_t * p ); +static int Abc_NodeFindCut_int( Vec_Ptr_t * vInside, Vec_Ptr_t * vFanins, int nSizeLimit ); +static int Abc_NodeGetFaninCost( Abc_Obj_t * pNode ); +static void Abc_NodeConeMarkCollect_rec( Abc_Obj_t * pNode, Vec_Ptr_t * vVisited ); +static void Abc_NodeConeMark( Vec_Ptr_t * vVisited ); +static void Abc_NodeConeUnmark( Vec_Ptr_t * vVisited ); + +static Vec_Int_t * Abc_NodeRefactor( Abc_ManRes_t * p ); +static DdNode * Abc_NodeConeBdd( DdManager * dd, DdNode ** pbVars, Abc_Obj_t * pNode, Vec_Ptr_t * vFanins, Vec_Ptr_t * vVisited ); + +static int Abc_NodeDecide( Abc_ManRes_t * p ); +static void Abc_NodeUpdate( Abc_ManRes_t * p ); + +//////////////////////////////////////////////////////////////////////// +/// FUNCTION DEFITIONS /// +//////////////////////////////////////////////////////////////////////// + +/**Function************************************************************* + + Synopsis [Performs incremental resynthesis of the AIG.] + + Description [Starting from each node, computes a reconvergence-driven cut, + derives BDD of the cut function, constructs ISOP, factors the cover, + and replaces the current implementation of the MFFC of the cut by the + new factored form if the number of AIG nodes is reduced. Returns the + number of AIG nodes saved.] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Abc_NtkAigResynthesize( Abc_Ntk_t * pNtk, Abc_ManRes_t * p ) +{ + int fCheck = 1; + ProgressBar * pProgress; + Abc_Obj_t * pNode; + int i, Counter, Approx; + + assert( Abc_NtkIsAig(pNtk) ); + + // start the BDD manager + p->dd = Cudd_Init( p->nNodeSizeMax + p->nConeSizeMax, 0, CUDD_UNIQUE_SLOTS, CUDD_CACHE_SLOTS, 0 ); + Cudd_zddVarsFromBddVars( p->dd, 2 ); + p->bCubeX = Extra_bddComputeRangeCube( p->dd, p->nNodeSizeMax, p->dd->size ); Cudd_Ref( p->bCubeX ); + + // remember the number of nodes + Counter = Abc_NtkNodeNum( pNtk ); + // resynthesize each node + pProgress = Extra_ProgressBarStart( stdout, 100 ); + Abc_NtkForEachNode( pNtk, pNode, i ) + { + Approx = (int)(100.0 * i / pNtk->vObjs->nSize ); + Extra_ProgressBarUpdate( pProgress, Approx, NULL ); + p->pNode = pNode; + Abc_NodeResyn( p ); + } + Extra_ProgressBarStop( pProgress ); + Abc_NtkManResStop( p ); + + // check + if ( fCheck && !Abc_NtkCheck( pNtk ) ) + { + printf( "Abc_NtkAigResynthesize: The network check has failed.\n" ); + return -1; + } + return Abc_NtkNodeNum(pNtk) - Counter; +} + +/**Function************************************************************* + + Synopsis [Performs resynthesis of one node.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Abc_NodeResyn( Abc_ManRes_t * p ) +{ + int RetValue; + int clk; + + assert( Abc_ObjIsNode(p->pNode) ); + +clk = clock(); + // detect the cut + Abc_NodeFindCut( p ); +p->time1 += clock() - clk; + + // refactor the cut +clk = clock(); + p->vForm = Abc_NodeRefactor( p ); +p->time2 += clock() - clk; + + // accept or reject the factored form +clk = clock(); + RetValue = Abc_NodeDecide( p ); +p->time3 += clock() - clk; + + // modify the network +clk = clock(); + if ( RetValue ) + Abc_NodeUpdate( p ); +p->time4 += clock() - clk; + + // cleanup + Vec_IntFree( p->vForm ); + p->vForm = NULL; +} + +/**Function************************************************************* + + Synopsis [Finds a reconvergence-driven cut.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Abc_NodeFindCut( Abc_ManRes_t * p ) +{ + Abc_Obj_t * pNode = p->pNode; + int i; + + // mark TFI using fMarkA + Vec_PtrClear( p->vVisited ); + Abc_NodeConeMarkCollect_rec( pNode, p->vVisited ); + + // start the reconvergence-driven node + Vec_PtrClear( p->vInsideNode ); + Vec_PtrClear( p->vFaninsNode ); + Vec_PtrPush( p->vFaninsNode, pNode ); + pNode->fMarkB = 1; + + // compute reconvergence-driven node + while ( Abc_NodeFindCut_int( p->vInsideNode, p->vFaninsNode, p->nNodeSizeMax ) ); + + // compute reconvergence-driven cone + Vec_PtrClear( p->vInsideCone ); + Vec_PtrClear( p->vFaninsCone ); + if ( p->nConeSizeMax > p->nNodeSizeMax ) + { + // copy the node into the cone + Vec_PtrForEachEntry( p->vInsideNode, pNode, i ) + Vec_PtrPush( p->vInsideCone, pNode ); + Vec_PtrForEachEntry( p->vFaninsNode, pNode, i ) + Vec_PtrPush( p->vFaninsCone, pNode ); + // compute reconvergence-driven cone + while ( Abc_NodeFindCut_int( p->vInsideCone, p->vFaninsCone, p->nConeSizeMax ) ); + // unmark the nodes of the sets + Vec_PtrForEachEntry( p->vInsideCone, pNode, i ) + pNode->fMarkB = 0; + Vec_PtrForEachEntry( p->vFaninsCone, pNode, i ) + pNode->fMarkB = 0; + } + else + { + // unmark the nodes of the sets + Vec_PtrForEachEntry( p->vInsideNode, pNode, i ) + pNode->fMarkB = 0; + Vec_PtrForEachEntry( p->vFaninsNode, pNode, i ) + pNode->fMarkB = 0; + } + + // unmark TFI using fMarkA + Abc_NodeConeUnmark( p->vVisited ); +} + +/**Function************************************************************* + + Synopsis [Finds a reconvergence-driven cut.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Abc_NodeFindCut_int( Vec_Ptr_t * vInside, Vec_Ptr_t * vFanins, int nSizeLimit ) +{ + Abc_Obj_t * pNode, * pFaninBest, * pNext; + int CostBest, CostCur, i; + // find the best fanin + CostBest = 100; + pFaninBest = NULL; + Vec_PtrForEachEntry( vFanins, pNode, i ) + { + CostCur = Abc_NodeGetFaninCost( pNode ); + if ( CostBest > CostCur ) + { + CostBest = CostCur; + pFaninBest = pNode; + } + } + if ( pFaninBest == NULL ) + return 0; + assert( CostBest < 3 ); + if ( vFanins->nSize - 1 + CostBest > nSizeLimit ) + return 0; + assert( Abc_ObjIsNode(pFaninBest) ); + // remove the node from the array + Vec_PtrRemove( vFanins, pFaninBest ); + // add the node to the set + Vec_PtrPush( vInside, pFaninBest ); + // add the left child to the fanins + pNext = Abc_ObjFanin0(pFaninBest); + if ( !pNext->fMarkB ) + { + pNext->fMarkB = 1; + Vec_PtrPush( vFanins, pNext ); + } + // add the right child to the fanins + pNext = Abc_ObjFanin1(pFaninBest); + if ( !pNext->fMarkB ) + { + pNext->fMarkB = 1; + Vec_PtrPush( vFanins, pNext ); + } + assert( vFanins->nSize <= nSizeLimit ); + // keep doing this + return 1; +} + +/**Function************************************************************* + + Synopsis [Evaluate the fanin cost.] + + Description [Returns the number of fanins that will be brought in. + Returns large number if the node cannot be added.] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Abc_NodeGetFaninCost( Abc_Obj_t * pNode ) +{ + Abc_Obj_t * pFanout; + int i; + assert( pNode->fMarkA == 1 ); // this node is in the TFI + assert( pNode->fMarkB == 1 ); // this node is in the constructed cone + // check the PI node + if ( !Abc_ObjIsNode(pNode) ) + return 999; + // check the fanouts + Abc_ObjForEachFanout( pNode, pFanout, i ) + if ( pFanout->fMarkA && pFanout->fMarkB == 0 ) // in the cone but not in the set + return 999; + // the fanouts are in the TFI and inside the constructed cone + // return the number of fanins that will be on the boundary if this node is added + return (!Abc_ObjFanin0(pNode)->fMarkB) + (!Abc_ObjFanin1(pNode)->fMarkB); +} + +/**Function************************************************************* + + Synopsis [Marks the TFI cone.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Abc_NodeConeMarkCollect_rec( Abc_Obj_t * pNode, Vec_Ptr_t * vVisited ) +{ + if ( pNode->fMarkA == 1 ) + return; + // visit transitive fanin + if ( Abc_ObjIsNode(pNode) ) + { + Abc_NodeConeMarkCollect_rec( Abc_ObjFanin0(pNode), vVisited ); + Abc_NodeConeMarkCollect_rec( Abc_ObjFanin1(pNode), vVisited ); + } + assert( pNode->fMarkA == 0 ); + pNode->fMarkA = 1; + Vec_PtrPush( vVisited, pNode ); +} + +/**Function************************************************************* + + Synopsis [Unmarks the TFI cone.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Abc_NodeConeMark( Vec_Ptr_t * vVisited ) +{ + int i; + for ( i = 0; i < vVisited->nSize; i++ ) + ((Abc_Obj_t *)vVisited->pArray)->fMarkA = 1; +} + +/**Function************************************************************* + + Synopsis [Unmarks the TFI cone.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Abc_NodeConeUnmark( Vec_Ptr_t * vVisited ) +{ + int i; + for ( i = 0; i < vVisited->nSize; i++ ) + ((Abc_Obj_t *)vVisited->pArray)->fMarkA = 0; +} + + +/**Function************************************************************* + + Synopsis [Derives the factored form of the node.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Vec_Int_t * Abc_NodeRefactor( Abc_ManRes_t * p ) +{ + Vec_Int_t * vForm; + DdManager * dd = p->dd; + DdNode * bFuncNode, * bFuncCone, * bCare, * bFuncOn, * bFuncOnDc; + char * pSop; + int nFanins; + + assert( p->vFaninsNode->nSize < p->nNodeSizeMax ); + assert( p->vFaninsCone->nSize < p->nConeSizeMax ); + + // get the function of the node + bFuncNode = Abc_NodeConeBdd( dd, p->dd->vars, p->pNode, p->vFaninsNode, p->vVisited ); + Cudd_Ref( bFuncNode ); + nFanins = p->vFaninsNode->nSize; + if ( p->nConeSizeMax > p->nNodeSizeMax ) + { + // get the function of the cone + bFuncCone = Abc_NodeConeBdd( dd, p->dd->vars + p->nNodeSizeMax, p->pNode, p->vFaninsCone, p->vVisited ); + Cudd_Ref( bFuncCone ); + // get the care set + bCare = Cudd_bddXorExistAbstract( p->dd, Cudd_Not(bFuncNode), bFuncCone, p->bCubeX ); Cudd_Ref( bCare ); + Cudd_RecursiveDeref( dd, bFuncCone ); + // compute the on-set and off-set of the function of the node + bFuncOn = Cudd_bddAnd( dd, bFuncNode, bCare ); Cudd_Ref( bFuncOn ); + bFuncOnDc = Cudd_bddAnd( dd, Cudd_Not(bFuncNode), bCare ); Cudd_Ref( bFuncOnDc ); + bFuncOnDc = Cudd_Not( bFuncOnDc ); + Cudd_RecursiveDeref( dd, bCare ); + // get the cover + pSop = Abc_ConvertBddToSop( NULL, dd, bFuncOn, bFuncOnDc, nFanins, p->vCube, -1 ); + Cudd_RecursiveDeref( dd, bFuncOn ); + Cudd_RecursiveDeref( dd, bFuncOnDc ); + } + else + { + // get the cover + pSop = Abc_ConvertBddToSop( NULL, dd, bFuncNode, bFuncNode, nFanins, p->vCube, -1 ); + } + Cudd_RecursiveDeref( dd, bFuncNode ); + // derive the factored form + vForm = Ft_Factor( pSop ); + free( pSop ); + return vForm; +} + +/**Function************************************************************* + + Synopsis [Returns BDD representing the logic function of the cone.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +DdNode * Abc_NodeConeBdd( DdManager * dd, DdNode ** pbVars, Abc_Obj_t * pNode, Vec_Ptr_t * vFanins, Vec_Ptr_t * vVisited ) +{ + DdNode * bFunc0, * bFunc1, * bFunc; + int i; + // mark the fanins of the cone + Abc_NodeConeMark( vFanins ); + // collect the nodes in the DFS order + Vec_PtrClear( vVisited ); + Abc_NodeConeMarkCollect_rec( pNode, vVisited ); + // unmark both sets + Abc_NodeConeUnmark( vFanins ); + Abc_NodeConeUnmark( vVisited ); + // set the elementary BDDs + Vec_PtrForEachEntry( vFanins, pNode, i ) + pNode->pCopy = (Abc_Obj_t *)pbVars[i]; + // compute the BDDs for the collected nodes + Vec_PtrForEachEntry( vVisited, pNode, i ) + { + bFunc0 = Cudd_NotCond( Abc_ObjFanin0(pNode)->pCopy, Abc_ObjFaninC0(pNode) ); + bFunc1 = Cudd_NotCond( Abc_ObjFanin1(pNode)->pCopy, Abc_ObjFaninC1(pNode) ); + bFunc = Cudd_bddAnd( dd, bFunc0, bFunc1 ); Cudd_Ref( bFunc ); + pNode->pCopy = (Abc_Obj_t *)bFunc; + } + Cudd_Ref( bFunc ); + // dereference the intermediate ones + Vec_PtrForEachEntry( vVisited, pNode, i ) + Cudd_RecursiveDeref( dd, (DdNode *)pNode->pCopy ); + Cudd_Deref( bFunc ); + return bFunc; +} + + +/**Function************************************************************* + + Synopsis [Decides whether to accept the given factored form.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Abc_NodeDecide( Abc_ManRes_t * p ) +{ + return 0; +} + +/**Function************************************************************* + + Synopsis [Replaces MFFC of the node by the new factored.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Abc_NodeUpdate( Abc_ManRes_t * p ) +{ +} + + + + +/**Function************************************************************* + + Synopsis [Starts the resynthesis manager.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Abc_ManRes_t * Abc_NtkManResStart() +{ + Abc_ManRes_t * p; + p = ALLOC( Abc_ManRes_t, 1 ); + p->vFaninsNode = Vec_PtrAlloc( 100 ); + p->vInsideNode = Vec_PtrAlloc( 100 ); + p->vFaninsCone = Vec_PtrAlloc( 100 ); + p->vInsideCone = Vec_PtrAlloc( 100 ); + p->vVisited = Vec_PtrAlloc( 100 ); + p->vCube = Vec_StrAlloc( 100 ); + return p; +} + +/**Function************************************************************* + + Synopsis [Stops the resynthesis manager.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Abc_NtkManResStop( Abc_ManRes_t * p ) +{ + if ( p->bCubeX ) Cudd_RecursiveDeref( p->dd, p->bCubeX ); + if ( p->dd ) Extra_StopManager( p->dd ); + Vec_PtrFree( p->vFaninsNode ); + Vec_PtrFree( p->vInsideNode ); + Vec_PtrFree( p->vFaninsCone ); + Vec_PtrFree( p->vInsideCone ); + Vec_PtrFree( p->vVisited ); + Vec_StrFree( p->vCube ); + free( p ); +} + +//////////////////////////////////////////////////////////////////////// +/// END OF FILE /// +//////////////////////////////////////////////////////////////////////// + + diff --git a/src/base/abc/abcShow.c b/src/base/abc/abcShow.c new file mode 100644 index 00000000..2ddd2a79 --- /dev/null +++ b/src/base/abc/abcShow.c @@ -0,0 +1,167 @@ +/**CFile**************************************************************** + + FileName [abcShow.c] + + SystemName [ABC: Logic synthesis and verification system.] + + PackageName [Network and node package.] + + Synopsis [Visualization procedures using DOT software and GSView.] + + Author [Alan Mishchenko] + + Affiliation [UC Berkeley] + + Date [Ver. 1.0. Started - June 20, 2005.] + + Revision [$Id: abcShow.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $] + +***********************************************************************/ + +#include "abc.h" +#ifdef WIN32 +#include "process.h" +#endif + +//////////////////////////////////////////////////////////////////////// +/// DECLARATIONS /// +//////////////////////////////////////////////////////////////////////// + +//////////////////////////////////////////////////////////////////////// +/// FUNCTION DEFITIONS /// +//////////////////////////////////////////////////////////////////////// + +/**Function************************************************************* + + Synopsis [Prints the factored form of one node.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Abc_NodePrintBdd( Abc_Obj_t * pNode ) +{ + FILE * pFile; + Vec_Ptr_t * vNamesIn; + char * FileNameIn; + char * FileNameOut; + char * FileGeneric; + char * pCur, * pNameOut; + char FileNameDot[200]; + char FileNamePs[200]; + char CommandDot[1000]; +#ifndef WIN32 + char CommandPs[1000]; +#endif + char * pProgDotName; + char * pProgGsViewName; + int RetValue; + + assert( Abc_NtkIsLogicBdd(pNode->pNtk) ); + +#ifdef WIN32 + pProgDotName = "dot.exe"; + pProgGsViewName = NULL; +#else + pProgDotName = "dot"; + pProgGsViewName = "gv"; +#endif + + FileNameIn = NULL; + FileNameOut = NULL; + + // get the generic file name + pNode->pCopy = NULL; + FileGeneric = Abc_ObjName(pNode); + // get rid of not-alpha-numeric characters + for ( pCur = FileGeneric; *pCur; pCur++ ) + if ( !((*pCur >= '0' && *pCur <= '9') || (*pCur >= 'a' && *pCur <= 'z') || (*pCur >= 'A' && *pCur <= 'Z')) ) + *pCur = '_'; + // create the file names + sprintf( FileNameDot, "%s.dot", FileGeneric ); + sprintf( FileNamePs, "%s.ps", FileGeneric ); + + // write the DOT file + if ( (pFile = fopen( FileNameDot, "w" )) == NULL ) + { + fprintf( stdout, "Cannot open the intermediate file \"%s\".\n", FileNameDot ); + return; + } + // set the node names + Abc_NtkLogicTransferNames( pNode->pNtk ); + vNamesIn = Abc_NodeGetFaninNames( pNode ); + pNameOut = Abc_ObjName(pNode); + Cudd_DumpDot( pNode->pNtk->pManFunc, 1, (DdNode **)&pNode->pData, (char **)vNamesIn->pArray, &pNameOut, pFile ); + Abc_NodeFreeFaninNames( vNamesIn ); + Abc_NtkCleanCopy( pNode->pNtk ); + fclose( pFile ); + + // check that the input file is okay + if ( (pFile = fopen( FileNameDot, "r" )) == NULL ) + { + fprintf( stdout, "Cannot open the intermediate file \"%s\".\n", FileNameDot ); + return; + } + fclose( pFile ); + + // generate the DOT file + sprintf( CommandDot, "%s -Tps -o %s %s", pProgDotName, FileNamePs, FileNameDot ); + RetValue = system( CommandDot ); +#ifdef WIN32 + _unlink( FileNameDot ); +#else + unlink( FileNameDot ); +#endif + if ( RetValue == -1 ) + { + fprintf( stdout, "Cannot find \"%s\".\n", pProgDotName ); + return; + } + + // check that the input file is okay + if ( (pFile = fopen( FileNamePs, "r" )) == NULL ) + { + fprintf( stdout, "Cannot open intermediate file \"%s\".\n", FileNamePs ); + return; + } + fclose( pFile ); + +#ifdef WIN32 + if ( _spawnl( _P_NOWAIT, "gsview32.exe", "gsview32.exe", FileNamePs, NULL ) == -1 ) + if ( _spawnl( _P_NOWAIT, "C:\\Program Files\\Ghostgum\\gsview\\gsview32.exe", + "C:\\Program Files\\Ghostgum\\gsview\\gsview32.exe", FileNamePs, NULL ) == -1 ) + { + fprintf( stdout, "Cannot find \"%s\".\n", "gsview32.exe" ); + return; + } +#else + sprintf( CommandPs, "%s %s &", pProgGsViewName, FileNamePs ); + if ( system( CommandPs ) == -1 ) + { + fprintf( stdout, "Cannot execute \"%s\".\n", FileNamePs ); + return; + } +#endif +} + + +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ + +//////////////////////////////////////////////////////////////////////// +/// END OF FILE /// +//////////////////////////////////////////////////////////////////////// + + diff --git a/src/base/abc/abcStrash.c b/src/base/abc/abcStrash.c index fcfeefda..bf494767 100644 --- a/src/base/abc/abcStrash.c +++ b/src/base/abc/abcStrash.c @@ -27,7 +27,7 @@ //////////////////////////////////////////////////////////////////////// // static functions -static void Abc_NtkStrashPerform( Abc_Ntk_t * pNtk, Abc_Ntk_t * pNtkAig ); +static void Abc_NtkStrashPerform( Abc_Ntk_t * pNtk, Abc_Ntk_t * pNtkAig, bool fAllNodes ); static Abc_Obj_t * Abc_NodeStrash( Abc_Aig_t * pMan, Abc_Obj_t * pNode ); static Abc_Obj_t * Abc_NodeStrashSop( Abc_Aig_t * pMan, Abc_Obj_t * pNode, char * pSop ); static Abc_Obj_t * Abc_NodeStrashFactor( Abc_Aig_t * pMan, Abc_Obj_t * pNode, char * pSop ); @@ -53,7 +53,7 @@ extern char * Mio_GateReadSop( void * pGate ); SeeAlso [] ***********************************************************************/ -Abc_Ntk_t * Abc_NtkStrash( Abc_Ntk_t * pNtk ) +Abc_Ntk_t * Abc_NtkStrash( Abc_Ntk_t * pNtk, bool fAllNodes ) { int fCheck = 1; Abc_Ntk_t * pNtkAig; @@ -68,14 +68,14 @@ Abc_Ntk_t * Abc_NtkStrash( Abc_Ntk_t * pNtk ) printf( "Warning: The choice nodes in the initial AIG are removed by strashing.\n" ); // perform strashing pNtkAig = Abc_NtkStartFrom( pNtk, ABC_NTK_AIG ); - Abc_NtkStrashPerform( pNtk, pNtkAig ); + Abc_NtkStrashPerform( pNtk, pNtkAig, fAllNodes ); Abc_NtkFinalize( pNtk, pNtkAig ); // print warning about self-feed latches if ( Abc_NtkCountSelfFeedLatches(pNtkAig) ) printf( "The network has %d self-feeding latches.\n", Abc_NtkCountSelfFeedLatches(pNtkAig) ); // duplicate EXDC if ( pNtk->pExdc ) - pNtkAig->pExdc = Abc_NtkStrash( pNtk->pExdc ); + pNtkAig->pExdc = Abc_NtkStrash( pNtk->pExdc, 0 ); // make sure everything is okay if ( fCheck && !Abc_NtkCheck( pNtkAig ) ) { @@ -97,7 +97,7 @@ Abc_Ntk_t * Abc_NtkStrash( Abc_Ntk_t * pNtk ) SeeAlso [] ***********************************************************************/ -void Abc_NtkStrashPerform( Abc_Ntk_t * pNtk, Abc_Ntk_t * pNtkNew ) +void Abc_NtkStrashPerform( Abc_Ntk_t * pNtk, Abc_Ntk_t * pNtkNew, bool fAllNodes ) { ProgressBar * pProgress; Abc_Aig_t * pMan = pNtkNew->pManFunc; @@ -106,8 +106,10 @@ void Abc_NtkStrashPerform( Abc_Ntk_t * pNtk, Abc_Ntk_t * pNtkNew ) int i; // perform strashing - vNodes = Abc_NtkDfs( pNtk ); -// vNodes = Abc_AigCollectAll( pNtk ); + if ( fAllNodes ) + vNodes = Abc_AigCollectAll( pNtk ); + else + vNodes = Abc_NtkDfs( pNtk ); pProgress = Extra_ProgressBarStart( stdout, vNodes->nSize ); for ( i = 0; i < vNodes->nSize; i++ ) { @@ -255,7 +257,7 @@ Abc_Obj_t * Abc_NodeStrashFactor( Abc_Aig_t * pMan, Abc_Obj_t * pRoot, char * pS assert( vForm->nSize > nVars ); assert( nVars == Abc_ObjFaninNum(pRoot) ); - // check for constant Andtion + // check for constant function pFtNode = Ft_NodeRead( vForm, 0 ); if ( pFtNode->fConst ) { @@ -268,7 +270,7 @@ Abc_Obj_t * Abc_NodeStrashFactor( Abc_Aig_t * pMan, Abc_Obj_t * pRoot, char * pS Abc_ObjForEachFanin( pRoot, pFanin, i ) Vec_PtrPush( vAnds, pFanin->pCopy ); - // compute the Andtions of other nodes + // compute the function of other nodes for ( i = nVars; i < vForm->nSize; i++ ) { pFtNode = Ft_NodeRead( vForm, i ); @@ -322,7 +324,7 @@ int Abc_NtkAppend( Abc_Ntk_t * pNtk1, Abc_Ntk_t * pNtk2 ) Abc_NtkForEachCi( pNtk2, pObj, i ) pObj->pCopy = Abc_NtkCi(pNtk1, i); // add pNtk2 to pNtk1 while strashing - Abc_NtkStrashPerform( pNtk2, pNtk1 ); + Abc_NtkStrashPerform( pNtk2, pNtk1, 1 ); // make sure that everything is okay if ( fCheck && !Abc_NtkCheck( pNtk1 ) ) { diff --git a/src/base/abc/abcSweep.c b/src/base/abc/abcSweep.c index 6890fc57..495bf1eb 100644 --- a/src/base/abc/abcSweep.c +++ b/src/base/abc/abcSweep.c @@ -61,7 +61,7 @@ bool Abc_NtkFraigSweep( Abc_Ntk_t * pNtk, int fUseInv, int fVerbose ) assert( !Abc_NtkIsAig(pNtk) ); // derive the AIG - pNtkAig = Abc_NtkStrash( pNtk ); + pNtkAig = Abc_NtkStrash( pNtk, 0 ); // perform fraiging of the AIG Fraig_ParamsSetDefault( &Params ); pMan = Abc_NtkToFraig( pNtkAig, &Params, 0 ); diff --git a/src/base/abc/abcTiming.c b/src/base/abc/abcTiming.c index f017d93c..861a1b14 100644 --- a/src/base/abc/abcTiming.c +++ b/src/base/abc/abcTiming.c @@ -228,7 +228,7 @@ void Abc_NtkTimeSetRequired( Abc_Ntk_t * pNtk, int ObjId, float Rise, float Fall SeeAlso [] ***********************************************************************/ -void Abc_NtkTimeFinalize( Abc_Ntk_t * pNtk ) +void Abc_NtkTimeInitialize( Abc_Ntk_t * pNtk ) { Abc_Obj_t * pObj; Abc_Time_t ** ppTimes, * pTime; @@ -283,11 +283,12 @@ void Abc_NtkTimePrepare( Abc_Ntk_t * pNtk ) if ( pNtk->pManTime == NULL ) { pNtk->pManTime = Abc_ManTimeStart(); - Abc_NtkTimeFinalize( pNtk ); + Abc_NtkTimeInitialize( pNtk ); return; } - // if timing manager is given, clean arrivals except for PIs - // and required except for POs + // if timing manager is given, expand it if necessary + Abc_ManTimeExpand( pNtk->pManTime, Abc_NtkObjNum(pNtk), 0 ); + // clean arrivals except for PIs ppTimes = (Abc_Time_t **)pNtk->pManTime->vArrs->pArray; Abc_NtkForEachNode( pNtk, pObj, i ) { @@ -299,6 +300,7 @@ void Abc_NtkTimePrepare( Abc_Ntk_t * pNtk ) pTime = ppTimes[pObj->Id]; pTime->Fall = pTime->Rise = pTime->Worst = -ABC_INFINITY; } + // clean required except for POs } @@ -392,7 +394,7 @@ void Abc_ManTimeDup( Abc_Ntk_t * pNtkOld, Abc_Ntk_t * pNtkNew ) /**Function************************************************************* - Synopsis [] + Synopsis [Expends the storage for timing information.] Description [] diff --git a/src/base/abc/abcUnreach.c b/src/base/abc/abcUnreach.c new file mode 100644 index 00000000..5d5a759b --- /dev/null +++ b/src/base/abc/abcUnreach.c @@ -0,0 +1,328 @@ +/**CFile**************************************************************** + + FileName [abcUnreach.c] + + SystemName [ABC: Logic synthesis and verification system.] + + PackageName [Network and node package.] + + Synopsis [Computes unreachable states for small benchmarks.] + + Author [Alan Mishchenko] + + Affiliation [UC Berkeley] + + Date [Ver. 1.0. Started - June 20, 2005.] + + Revision [$Id: abcUnreach.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $] + +***********************************************************************/ + +#include "abc.h" + +//////////////////////////////////////////////////////////////////////// +/// DECLARATIONS /// +//////////////////////////////////////////////////////////////////////// + +static DdNode * Abc_NtkTransitionRelation( DdManager * dd, Abc_Ntk_t * pNtk, int fVerbose ); +static DdNode * Abc_NtkInitStateAndVarMap( DdManager * dd, Abc_Ntk_t * pNtk, int fVerbose ); +static DdNode * Abc_NtkComputeUnreachable( DdManager * dd, Abc_Ntk_t * pNtk, DdNode * bRelation, DdNode * bInitial, bool fVerbose ); +static Abc_Ntk_t * Abc_NtkConstructExdc ( DdManager * dd, Abc_Ntk_t * pNtk, DdNode * bUnreach ); + +//////////////////////////////////////////////////////////////////////// +/// FUNCTION DEFITIONS /// +//////////////////////////////////////////////////////////////////////// + +/**Function************************************************************* + + Synopsis [Extracts sequential DCs of the network.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Abc_NtkExtractSequentialDcs( Abc_Ntk_t * pNtk, bool fVerbose ) +{ + int fCheck = 1; + int fReorder = 1; + DdManager * dd; + DdNode * bRelation, * bInitial, * bUnreach; + + // remove EXDC network if present + if ( pNtk->pExdc ) + { + Abc_NtkDelete( pNtk->pExdc ); + pNtk->pExdc = NULL; + } + + // compute the global BDDs of the latches + dd = Abc_NtkGlobalBdds( pNtk, 1 ); + if ( dd == NULL ) + return 0; + if ( fVerbose ) + printf( "The shared BDD size is %d nodes.\n", Cudd_ReadKeys(dd) - Cudd_ReadDead(dd) ); + + // create the transition relation (dereferenced global BDDs) + bRelation = Abc_NtkTransitionRelation( dd, pNtk, fVerbose ); Cudd_Ref( bRelation ); + // create the initial state and the variable map + bInitial = Abc_NtkInitStateAndVarMap( dd, pNtk, fVerbose ); Cudd_Ref( bInitial ); + // compute the unreachable states + bUnreach = Abc_NtkComputeUnreachable( dd, pNtk, bRelation, bInitial, fVerbose ); Cudd_Ref( bUnreach ); + Cudd_RecursiveDeref( dd, bRelation ); + Cudd_RecursiveDeref( dd, bInitial ); + + // reorder and disable reordering + if ( fReorder ) + { + if ( fVerbose ) + fprintf( stdout, "BDD nodes in the unreachable states before reordering %d.\n", Cudd_DagSize(bUnreach) ); + Cudd_ReduceHeap( dd, CUDD_REORDER_SYMM_SIFT, 1 ); + Cudd_AutodynDisable( dd ); + if ( fVerbose ) + fprintf( stdout, "BDD nodes in the unreachable states after reordering %d.\n", Cudd_DagSize(bUnreach) ); + } + + // allocate ZDD variables + Cudd_zddVarsFromBddVars( dd, 2 ); + // create the EXDC network representing the unreachable states + pNtk->pExdc = Abc_NtkConstructExdc( dd, pNtk, bUnreach ); + Cudd_RecursiveDeref( dd, bUnreach ); + Extra_StopManager( dd ); + + // make sure that everything is okay + if ( fCheck && !Abc_NtkCheck( pNtk->pExdc ) ) + { + printf( "Abc_NtkExtractSequentialDcs: The network check has failed.\n" ); + Abc_NtkDelete( pNtk->pExdc ); + return 0; + } + return 1; +} + +/**Function************************************************************* + + Synopsis [Computes the transition relation of the network.] + + Description [Assumes that the global BDDs are computed.] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +DdNode * Abc_NtkTransitionRelation( DdManager * dd, Abc_Ntk_t * pNtk, int fVerbose ) +{ + DdNode * bRel, * bTemp, * bProd, * bVar, * bInputs; + Abc_Obj_t * pNode; + int fReorder = 1; + int i; + + // extand the BDD manager to represent NS variables + assert( dd->size == Abc_NtkCiNum(pNtk) ); + Cudd_bddIthVar( dd, Abc_NtkCiNum(pNtk) + Abc_NtkLatchNum(pNtk) - 1 ); + + // enable reordering + if ( fReorder ) + Cudd_AutodynEnable( dd, CUDD_REORDER_SYMM_SIFT ); + else + Cudd_AutodynDisable( dd ); + + // compute the transition relation + bRel = b1; Cudd_Ref( bRel ); + Abc_NtkForEachLatch( pNtk, pNode, i ) + { + bVar = Cudd_bddIthVar( dd, Abc_NtkCiNum(pNtk) + i ); + bProd = Cudd_bddXnor( dd, bVar, (DdNode *)pNode->pNext ); Cudd_Ref( bProd ); + bRel = Cudd_bddAnd( dd, bTemp = bRel, bProd ); Cudd_Ref( bRel ); + Cudd_RecursiveDeref( dd, bTemp ); + Cudd_RecursiveDeref( dd, bProd ); + } + // free the global BDDs + Abc_NtkFreeGlobalBdds( dd, pNtk ); + + // quantify the PI variables + bInputs = Extra_bddComputeRangeCube( dd, 0, Abc_NtkPiNum(pNtk) ); Cudd_Ref( bInputs ); + bRel = Cudd_bddExistAbstract( dd, bTemp = bRel, bInputs ); Cudd_Ref( bRel ); + Cudd_RecursiveDeref( dd, bTemp ); + Cudd_RecursiveDeref( dd, bInputs ); + + // reorder and disable reordering + if ( fReorder ) + { + if ( fVerbose ) + fprintf( stdout, "BDD nodes in the transition relation before reordering %d.\n", Cudd_DagSize(bRel) ); + Cudd_ReduceHeap( dd, CUDD_REORDER_SYMM_SIFT, 100 ); + Cudd_AutodynDisable( dd ); + if ( fVerbose ) + fprintf( stdout, "BDD nodes in the transition relation after reordering %d.\n", Cudd_DagSize(bRel) ); + } + Cudd_Deref( bRel ); + return bRel; +} + +/**Function************************************************************* + + Synopsis [Computes the initial state and sets up the variable map.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +DdNode * Abc_NtkInitStateAndVarMap( DdManager * dd, Abc_Ntk_t * pNtk, int fVerbose ) +{ + DdNode ** pbVarsX, ** pbVarsY; + DdNode * bTemp, * bProd, * bVar; + Abc_Obj_t * pLatch; + int i; + + // set the variable mapping for Cudd_bddVarMap() + pbVarsX = ALLOC( DdNode *, dd->size ); + pbVarsY = ALLOC( DdNode *, dd->size ); + bProd = b1; Cudd_Ref( bProd ); + Abc_NtkForEachLatch( pNtk, pLatch, i ) + { + pbVarsX[i] = dd->vars[ Abc_NtkPiNum(pNtk) + i ]; + pbVarsY[i] = dd->vars[ Abc_NtkCiNum(pNtk) + i ]; + // get the initial value of the latch + bVar = Cudd_NotCond( pbVarsX[i], (((int)pLatch->pData) != 1) ); + bProd = Cudd_bddAnd( dd, bTemp = bProd, bVar ); Cudd_Ref( bProd ); + Cudd_RecursiveDeref( dd, bTemp ); + } + Cudd_SetVarMap( dd, pbVarsX, pbVarsY, Abc_NtkLatchNum(pNtk) ); + FREE( pbVarsX ); + FREE( pbVarsY ); + + Cudd_Deref( bProd ); + return bProd; +} + +/**Function************************************************************* + + Synopsis [Computes the set of unreachable states.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +DdNode * Abc_NtkComputeUnreachable( DdManager * dd, Abc_Ntk_t * pNtk, DdNode * bTrans, DdNode * bInitial, bool fVerbose ) +{ + DdNode * bRelation, * bReached, * bCubeCs; + DdNode * bCurrent, * bNext, * bTemp; + int nIters; + + // perform reachability analisys + bCurrent = bInitial; Cudd_Ref( bCurrent ); + bReached = bInitial; Cudd_Ref( bReached ); + bRelation = bTrans; Cudd_Ref( bRelation ); + bCubeCs = Extra_bddComputeRangeCube( dd, Abc_NtkPiNum(pNtk), Abc_NtkCiNum(pNtk) ); Cudd_Ref( bCubeCs ); + for ( nIters = 1; ; nIters++ ) + { + // compute the next states + bNext = Cudd_bddAndAbstract( dd, bRelation, bCurrent, bCubeCs ); Cudd_Ref( bNext ); + Cudd_RecursiveDeref( dd, bCurrent ); + // remap these states into the current state vars + bNext = Cudd_bddVarMap( dd, bTemp = bNext ); Cudd_Ref( bNext ); + Cudd_RecursiveDeref( dd, bTemp ); + // check if there are any new states + if ( Cudd_bddLeq( dd, bNext, bReached ) ) + break; + // get the new states + bCurrent = Cudd_bddAnd( dd, bNext, Cudd_Not(bReached) ); Cudd_Ref( bCurrent ); + // minimize the new states with the reached states +// bCurrent = Cudd_bddConstrain( dd, bTemp = bCurrent, Cudd_Not(bReached) ); Cudd_Ref( bCurrent ); +// Cudd_RecursiveDeref( dd, bTemp ); + // add to the reached states + bReached = Cudd_bddOr( dd, bTemp = bReached, bNext ); Cudd_Ref( bReached ); + Cudd_RecursiveDeref( dd, bTemp ); + Cudd_RecursiveDeref( dd, bNext ); + // minimize the transition relation +// bRelation = Cudd_bddConstrain( dd, bTemp = bRelation, Cudd_Not(bReached) ); Cudd_Ref( bRelation ); +// Cudd_RecursiveDeref( dd, bTemp ); + } + Cudd_RecursiveDeref( dd, bRelation ); + Cudd_RecursiveDeref( dd, bCubeCs ); + Cudd_RecursiveDeref( dd, bNext ); + // report the stats + if ( fVerbose ) + { + fprintf( stdout, "Reachability analysis completed in %d iterations.\n", nIters ); + fprintf( stdout, "The number of minterms in the reachable state set = %d.\n", + (int)Cudd_CountMinterm(dd, bReached, Abc_NtkLatchNum(pNtk) ) ); + } +//PRB( dd, bReached ); + Cudd_Deref( bReached ); + return Cudd_Not( bReached ); +} + +/**Function************************************************************* + + Synopsis [Creates the EXDC network.] + + Description [The set of unreachable states depends on CS variables.] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Abc_Ntk_t * Abc_NtkConstructExdc( DdManager * dd, Abc_Ntk_t * pNtk, DdNode * bUnreach ) +{ + Abc_Ntk_t * pNtkNew; + Abc_Obj_t * pNode, * pNodeNew; + int * pPermute; + int i; + + // start the new network + pNtkNew = Abc_NtkAlloc( ABC_NTK_LOGIC_BDD ); + // create PIs corresponding to LOs + Abc_NtkForEachLatch( pNtk, pNode, i ) + pNode->pCopy = Abc_NtkCreateTermPi(pNtkNew); + + // create a new node + pNodeNew = Abc_NtkCreateNode(pNtkNew); + // add the fanins corresponding to latch outputs + Abc_NtkForEachLatch( pNtk, pNode, i ) + Abc_ObjAddFanin( pNodeNew, pNode->pCopy ); + + // create the logic function + pPermute = ALLOC( int, dd->size ); + for ( i = 0; i < dd->size; i++ ) + pPermute[i] = -1; + Abc_NtkForEachLatch( pNtk, pNode, i ) + pPermute[Abc_NtkPiNum(pNtk) + i] = i; + // remap the functions + pNodeNew->pData = Extra_TransferPermute( dd, pNtkNew->pManFunc, bUnreach, pPermute ); Cudd_Ref( pNodeNew->pData ); + free( pPermute ); + Abc_NodeMinimumBase( pNodeNew ); + + // make the new node drive all the COs + Abc_NtkForEachCo( pNtk, pNode, i ) + Abc_ObjAddFanin( Abc_NtkCreateTermPo(pNtkNew), pNodeNew ); + + // copy the CI/CO names + Abc_NtkForEachLatch( pNtk, pNode, i ) + Abc_NtkLogicStoreName( pNtkNew->vPis->pArray[i], Abc_NtkNameLatch(pNtk, i) ); + Abc_NtkForEachPo( pNtk, pNode, i ) + Abc_NtkLogicStoreName( pNtkNew->vPos->pArray[i], Abc_NtkNamePo(pNtk, i) ); + Abc_NtkForEachLatch( pNtk, pNode, i ) + Abc_NtkLogicStoreName( pNtkNew->vPos->pArray[Abc_NtkPoNum(pNtk) + i], Abc_NtkNameLatchInput(pNtk, i) ); + + // transform the network to the SOP representation + Abc_NtkBddToSop( pNtkNew ); + return pNtkNew; +} + +//////////////////////////////////////////////////////////////////////// +/// END OF FILE /// +//////////////////////////////////////////////////////////////////////// + + diff --git a/src/base/abc/abcUtil.c b/src/base/abc/abcUtil.c index e971ca18..001a7231 100644 --- a/src/base/abc/abcUtil.c +++ b/src/base/abc/abcUtil.c @@ -777,6 +777,47 @@ Vec_Ptr_t * Abc_AigCollectAll( Abc_Ntk_t * pNtk ) return vNodes; } +/**Function************************************************************* + + Synopsis [Gets fanin node names.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Vec_Ptr_t * Abc_NodeGetFaninNames( Abc_Obj_t * pNode ) +{ + Vec_Ptr_t * vNodes; + Abc_Obj_t * pFanin; + int i; + vNodes = Vec_PtrAlloc( 100 ); + Abc_ObjForEachFanin( pNode, pFanin, i ) + Vec_PtrPush( vNodes, util_strsav(Abc_ObjName(pFanin)) ); + return vNodes; +} + +/**Function************************************************************* + + Synopsis [Gets fanin node names.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Abc_NodeFreeFaninNames( Vec_Ptr_t * vNames ) +{ + int i; + for ( i = 0; i < vNames->nSize; i++ ) + free( vNames->pArray[i] ); + Vec_PtrFree( vNames ); +} + //////////////////////////////////////////////////////////////////////// /// END OF FILE /// diff --git a/src/base/abc/module.make b/src/base/abc/module.make index 1eb88224..f698d167 100644 --- a/src/base/abc/module.make +++ b/src/base/abc/module.make @@ -10,6 +10,7 @@ SRC += src/base/abc/abc.c \ src/base/abc/abcFpga.c \ src/base/abc/abcFraig.c \ src/base/abc/abcFunc.c \ + src/base/abc/abcFxu.c \ src/base/abc/abcLatch.c \ src/base/abc/abcMap.c \ src/base/abc/abcMinBase.c \ @@ -19,10 +20,13 @@ SRC += src/base/abc/abc.c \ src/base/abc/abcPrint.c \ src/base/abc/abcRefs.c \ src/base/abc/abcRenode.c \ + src/base/abc/abcRes.c \ src/base/abc/abcSat.c \ + src/base/abc/abcShow.c \ src/base/abc/abcSop.c \ src/base/abc/abcStrash.c \ src/base/abc/abcSweep.c \ src/base/abc/abcTiming.c \ + src/base/abc/abcUnreach.c \ src/base/abc/abcUtil.c \ src/base/abc/abcVerify.c diff --git a/src/base/io/ioReadBlif.c b/src/base/io/ioReadBlif.c index 6d9c2347..10346729 100644 --- a/src/base/io/ioReadBlif.c +++ b/src/base/io/ioReadBlif.c @@ -88,7 +88,7 @@ Abc_Ntk_t * Io_ReadBlif( char * pFileName, int fCheck ) Io_ReadBlifFree( p ); return NULL; } - Abc_NtkTimeFinalize( pNtk ); + Abc_NtkTimeInitialize( pNtk ); // read the EXDC network if ( p->fParsingExdc ) diff --git a/src/base/main/main.h b/src/base/main/main.h index c5d6a0c8..da47f154 100644 --- a/src/base/main/main.h +++ b/src/base/main/main.h @@ -84,6 +84,7 @@ extern void Abc_FrameRestart( Abc_Frame_t * p ); extern void Abc_FrameSetCurrentNetwork( Abc_Frame_t * p, Abc_Ntk_t * pNet ); extern void Abc_FrameSwapCurrentAndBackup( Abc_Frame_t * p ); extern void Abc_FrameReplaceCurrentNetwork( Abc_Frame_t * p, Abc_Ntk_t * pNet ); +extern void Abc_FrameUnmapAllNetworks( Abc_Frame_t * p ); extern void Abc_FrameDeleteAllNetworks( Abc_Frame_t * p ); extern void Abc_FrameSetGlobalFrame( Abc_Frame_t * p ); diff --git a/src/base/main/mainFrame.c b/src/base/main/mainFrame.c index 0b0cbbbd..38574883 100644 --- a/src/base/main/mainFrame.c +++ b/src/base/main/mainFrame.c @@ -205,19 +205,19 @@ bool Abc_FrameSetMode( Abc_Frame_t * p, bool fNameMode ) SeeAlso [] ***********************************************************************/ -void Abc_FrameSetCurrentNetwork( Abc_Frame_t * p, Abc_Ntk_t * pNetNew ) +void Abc_FrameSetCurrentNetwork( Abc_Frame_t * p, Abc_Ntk_t * pNtkNew ) { - Abc_Ntk_t * pNet, * pNet2, * pNet3; + Abc_Ntk_t * pNtk, * pNtk2, * pNtk3; int nNetsPresent; int nNetsToSave; char * pValue; // link it to the previous network - Abc_NtkSetBackup( pNetNew, p->pNtkCur ); + Abc_NtkSetBackup( pNtkNew, p->pNtkCur ); // set the step of this network - Abc_NtkSetStep( pNetNew, ++p->nSteps ); + Abc_NtkSetStep( pNtkNew, ++p->nSteps ); // set this network to be the current network - p->pNtkCur = pNetNew; + p->pNtkCur = pNtkNew; // remove any extra network that may happen to be in the stack pValue = Cmd_FlagReadByName( p, "savesteps" ); @@ -229,20 +229,20 @@ void Abc_FrameSetCurrentNetwork( Abc_Frame_t * p, Abc_Ntk_t * pNetNew ) // count the network, remember the last one, and the one before the last one nNetsPresent = 0; - pNet2 = pNet3 = NULL; - for ( pNet = p->pNtkCur; pNet; pNet = Abc_NtkBackup(pNet2) ) + pNtk2 = pNtk3 = NULL; + for ( pNtk = p->pNtkCur; pNtk; pNtk = Abc_NtkBackup(pNtk2) ) { nNetsPresent++; - pNet3 = pNet2; - pNet2 = pNet; + pNtk3 = pNtk2; + pNtk2 = pNtk; } // remove the earliest backup network if it is more steps away than we store if ( nNetsPresent - 1 > nNetsToSave ) { // delete the last network - Abc_NtkDelete( pNet2 ); + Abc_NtkDelete( pNtk2 ); // clean the pointer of the network before the last one - Abc_NtkSetBackup( pNet3, NULL ); + Abc_NtkSetBackup( pNtk3, NULL ); } } @@ -259,31 +259,31 @@ void Abc_FrameSetCurrentNetwork( Abc_Frame_t * p, Abc_Ntk_t * pNetNew ) ***********************************************************************/ void Abc_FrameSwapCurrentAndBackup( Abc_Frame_t * p ) { - Abc_Ntk_t * pNtkCur, * pNetBack, * pNetBack2; + Abc_Ntk_t * pNtkCur, * pNtkBack, * pNtkBack2; int iStepCur, iStepBack; pNtkCur = p->pNtkCur; - pNetBack = Abc_NtkBackup( pNtkCur ); + pNtkBack = Abc_NtkBackup( pNtkCur ); iStepCur = Abc_NtkStep ( pNtkCur ); // if there is no backup nothing to reset - if ( pNetBack == NULL ) + if ( pNtkBack == NULL ) return; // remember the backup of the backup - pNetBack2 = Abc_NtkBackup( pNetBack ); - iStepBack = Abc_NtkStep ( pNetBack ); + pNtkBack2 = Abc_NtkBackup( pNtkBack ); + iStepBack = Abc_NtkStep ( pNtkBack ); // set pNtkCur to be the next after the backup's backup - Abc_NtkSetBackup( pNtkCur, pNetBack2 ); + Abc_NtkSetBackup( pNtkCur, pNtkBack2 ); Abc_NtkSetStep ( pNtkCur, iStepBack ); // set pNtkCur to be the next after the backup - Abc_NtkSetBackup( pNetBack, pNtkCur ); - Abc_NtkSetStep ( pNetBack, iStepCur ); + Abc_NtkSetBackup( pNtkBack, pNtkCur ); + Abc_NtkSetStep ( pNtkBack, iStepCur ); // set the current network - p->pNtkCur = pNetBack; + p->pNtkCur = pNtkBack; } @@ -299,26 +299,45 @@ void Abc_FrameSwapCurrentAndBackup( Abc_Frame_t * p ) SeeAlso [] ***********************************************************************/ -void Abc_FrameReplaceCurrentNetwork( Abc_Frame_t * p, Abc_Ntk_t * pNet ) +void Abc_FrameReplaceCurrentNetwork( Abc_Frame_t * p, Abc_Ntk_t * pNtk ) { - if ( pNet == NULL ) + if ( pNtk == NULL ) return; // transfer the parameters to the new network if ( p->pNtkCur ) { - Abc_NtkSetBackup( pNet, Abc_NtkBackup(p->pNtkCur) ); - Abc_NtkSetStep( pNet, Abc_NtkStep(p->pNtkCur) ); + Abc_NtkSetBackup( pNtk, Abc_NtkBackup(p->pNtkCur) ); + Abc_NtkSetStep( pNtk, Abc_NtkStep(p->pNtkCur) ); // delete the current network Abc_NtkDelete( p->pNtkCur ); } else { - Abc_NtkSetBackup( pNet, NULL ); - Abc_NtkSetStep( pNet, ++p->nSteps ); + Abc_NtkSetBackup( pNtk, NULL ); + Abc_NtkSetStep( pNtk, ++p->nSteps ); } // set the new current network - p->pNtkCur = pNet; + p->pNtkCur = pNtk; +} + +/**Function************************************************************* + + Synopsis [Removes library binding of all currently stored networks.] + + Description [This procedure is called when the library is freed.] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Abc_FrameUnmapAllNetworks( Abc_Frame_t * p ) +{ + Abc_Ntk_t * pNtk; + for ( pNtk = p->pNtkCur; pNtk; pNtk = Abc_NtkBackup(pNtk) ) + if ( Abc_NtkIsLogicMap(pNtk) ) + Abc_NtkUnmap( pNtk ); } /**Function************************************************************* @@ -334,14 +353,14 @@ void Abc_FrameReplaceCurrentNetwork( Abc_Frame_t * p, Abc_Ntk_t * pNet ) ***********************************************************************/ void Abc_FrameDeleteAllNetworks( Abc_Frame_t * p ) { - Abc_Ntk_t * pNet, * pNet2; + Abc_Ntk_t * pNtk, * pNtk2; // delete all the currently saved networks - for ( pNet = p->pNtkCur, - pNet2 = pNet? Abc_NtkBackup(pNet): NULL; - pNet; - pNet = pNet2, - pNet2 = pNet? Abc_NtkBackup(pNet): NULL ) - Abc_NtkDelete( pNet ); + for ( pNtk = p->pNtkCur, + pNtk2 = pNtk? Abc_NtkBackup(pNtk): NULL; + pNtk; + pNtk = pNtk2, + pNtk2 = pNtk? Abc_NtkBackup(pNtk): NULL ) + Abc_NtkDelete( pNtk ); // set the current network empty p->pNtkCur = NULL; fprintf( p->Out, "All networks have been deleted.\n" ); diff --git a/src/bdd/dsd/dsd.h b/src/bdd/dsd/dsd.h index 60cf4a4e..5396bacd 100644 --- a/src/bdd/dsd/dsd.h +++ b/src/bdd/dsd/dsd.h @@ -88,6 +88,7 @@ extern Dsd_Node_t * Dsd_NodeReadDec ( Dsd_Node_t * p, int i ); extern int Dsd_NodeReadDecsNum( Dsd_Node_t * p ); extern int Dsd_NodeReadMark( Dsd_Node_t * p ); extern void Dsd_NodeSetMark( Dsd_Node_t * p, int Mark ); +extern DdManager * Dsd_ManagerReadDd( Dsd_Manager_t * pMan ); extern Dsd_Node_t * Dsd_ManagerReadRoot( Dsd_Manager_t * pMan, int i ); extern Dsd_Node_t * Dsd_ManagerReadInput( Dsd_Manager_t * pMan, int i ); /*=== dsdMan.c =======================================================*/ @@ -95,6 +96,7 @@ extern Dsd_Manager_t * Dsd_ManagerStart( DdManager * dd, int nSuppMax, int fVerb extern void Dsd_ManagerStop( Dsd_Manager_t * dMan ); /*=== dsdProc.c =======================================================*/ extern void Dsd_Decompose( Dsd_Manager_t * dMan, DdNode ** pbFuncs, int nFuncs ); +extern Dsd_Node_t * Dsd_DecomposeOne( Dsd_Manager_t * pDsdMan, DdNode * bFunc ); /*=== dsdTree.c =======================================================*/ extern void Dsd_TreeNodeGetInfo( Dsd_Manager_t * dMan, int * DepthMax, int * GateSizeMax ); extern void Dsd_TreeNodeGetInfoOne( Dsd_Node_t * pNode, int * DepthMax, int * GateSizeMax ); @@ -104,6 +106,7 @@ extern int Dsd_TreeCountPrimeNodes( Dsd_Manager_t * pDsdMan ); extern int Dsd_TreeCountPrimeNodesOne( Dsd_Node_t * pRoot ); extern int Dsd_TreeCollectDecomposableVars( Dsd_Manager_t * dMan, int * pVars ); extern Dsd_Node_t ** Dsd_TreeCollectNodesDfs( Dsd_Manager_t * dMan, int * pnNodes ); +extern Dsd_Node_t ** Dsd_TreeCollectNodesDfsOne( Dsd_Manager_t * pDsdMan, Dsd_Node_t * pNode, int * pnNodes ); extern void Dsd_TreePrint( FILE * pFile, Dsd_Manager_t * dMan, char * pInputNames[], char * pOutputNames[], int fShortNames, int Output ); /*=== dsdLocal.c =======================================================*/ extern DdNode * Dsd_TreeGetPrimeFunction( DdManager * dd, Dsd_Node_t * pNode ); diff --git a/src/bdd/dsd/dsdApi.c b/src/bdd/dsd/dsdApi.c index f2269092..daf3080f 100644 --- a/src/bdd/dsd/dsdApi.c +++ b/src/bdd/dsd/dsdApi.c @@ -89,6 +89,7 @@ void Dsd_NodeSetMark( Dsd_Node_t * p, int Mark ){ p->Mark = Mark; } ***********************************************************************/ Dsd_Node_t * Dsd_ManagerReadRoot( Dsd_Manager_t * pMan, int i ) { return pMan->pRoots[i]; } Dsd_Node_t * Dsd_ManagerReadInput( Dsd_Manager_t * pMan, int i ) { return pMan->pInputs[i]; } +DdManager * Dsd_ManagerReadDd( Dsd_Manager_t * pMan ) { return pMan->dd; } //////////////////////////////////////////////////////////////////////// /// END OF FILE /// diff --git a/src/bdd/dsd/dsdInt.h b/src/bdd/dsd/dsdInt.h index 81440460..5008c24e 100644 --- a/src/bdd/dsd/dsdInt.h +++ b/src/bdd/dsd/dsdInt.h @@ -61,6 +61,8 @@ struct Dsd_Node_t_ /// MACRO DEFITIONS /// //////////////////////////////////////////////////////////////////////// +#define MAXINPUTS 1000 + //////////////////////////////////////////////////////////////////////// /// PARAMETERS /// //////////////////////////////////////////////////////////////////////// diff --git a/src/bdd/dsd/dsdProc.c b/src/bdd/dsd/dsdProc.c index 38cdc2b8..08c029e1 100644 --- a/src/bdd/dsd/dsdProc.c +++ b/src/bdd/dsd/dsdProc.c @@ -225,6 +225,22 @@ s_Loops2Useless = 0; /**Function************************************************************* + Synopsis [Performs decomposition for one function.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Dsd_Node_t * Dsd_DecomposeOne( Dsd_Manager_t * pDsdMan, DdNode * bFunc ) +{ + return dsdKernelDecompose_rec( pDsdMan, bFunc ); +} + +/**Function************************************************************* + Synopsis [The main function of this module. Recursive implementation of DSD.] Description [] @@ -1053,7 +1069,7 @@ if ( s_Show ) // go through the decomposition list of pPrev and find components // whose support does not overlap with supp(Lower) - Dsd_Node_t ** pNonOverlap = ALLOC( Dsd_Node_t *, dd->size ); + static Dsd_Node_t * pNonOverlap[MAXINPUTS]; int i, nNonOverlap = 0; for ( i = 0; i < pPrev->nDecs; i++ ) { @@ -1089,7 +1105,6 @@ if ( s_Show ) // assign the support to be subtracted from both components bSuppSubract = pDENew->S; } - free( pNonOverlap ); } // subtract its support from the support of upper component @@ -1106,8 +1121,8 @@ if ( s_Show ) } // end of if ( !fEqualLevel ) else // if ( fEqualLevel ) -- they have the same top level var { - Dsd_Node_t ** pMarkedLeft = ALLOC( Dsd_Node_t *, dd->size ); // the pointers to the marked blocks - char * pMarkedPols = ALLOC( char, dd->size ); // polarities of the marked blocks + static Dsd_Node_t * pMarkedLeft[MAXINPUTS]; // the pointers to the marked blocks + static char pMarkedPols[MAXINPUTS]; // polarities of the marked blocks int nMarkedLeft = 0; int fPolarity = 0; @@ -1198,9 +1213,6 @@ if ( s_Show ) SuppH = Cudd_bddExistAbstract( dd, bTemp = SuppH, bSuppSubract ), Cudd_Ref( SuppH ); Cudd_RecursiveDeref(dd, bTemp); - free( pMarkedLeft ); - free( pMarkedPols ); - } // end of if ( fEqualLevel ) } // end of decomposition list comparison @@ -1333,7 +1345,7 @@ Dsd_Node_t * dsdKernelFindContainingComponent( Dsd_Manager_t * pDsdMan, Dsd_Node ***********************************************************************/ int dsdKernelFindCommonComponents( Dsd_Manager_t * pDsdMan, Dsd_Node_t * pL, Dsd_Node_t * pH, Dsd_Node_t *** pCommon, Dsd_Node_t ** pLastDiffL, Dsd_Node_t ** pLastDiffH ) { - Dsd_Node_t ** Common = ALLOC( Dsd_Node_t *, pDsdMan->dd->size ); + static Dsd_Node_t * Common[MAXINPUTS]; int nCommon = 0; // pointers to the current decomposition entries @@ -1402,7 +1414,6 @@ int dsdKernelFindCommonComponents( Dsd_Manager_t * pDsdMan, Dsd_Node_t * pL, Dsd // return the pointer to the array *pCommon = Common; // return the number of common components - free( Common ); return nCommon; } @@ -1567,7 +1578,7 @@ int dsdKernelVerifyDecomposition( Dsd_Manager_t * pDsdMan, Dsd_Node_t * pDE ) else if ( pR->Type == DSD_NODE_PRIME ) { int i; - DdNode ** bGVars = ALLOC( DdNode *, dd->size ); + static DdNode * bGVars[MAXINPUTS]; // transform the function of this block, so that it depended on inputs // corresponding to the formal inputs DdNode * bNewFunc = Dsd_TreeGetPrimeFunctionOld( dd, pR, 1 ); Cudd_Ref( bNewFunc ); @@ -1589,7 +1600,6 @@ int dsdKernelVerifyDecomposition( Dsd_Manager_t * pDsdMan, Dsd_Node_t * pDE ) RetValue = (int)( bRes == pR->G );//|| bRes == Cudd_Not(pR->G) ); ///////////////////////////////////////////////////////// Cudd_Deref( bRes ); - free( bGVars ); } else { diff --git a/src/bdd/dsd/dsdTree.c b/src/bdd/dsd/dsdTree.c index b1532715..7905cbdd 100644 --- a/src/bdd/dsd/dsdTree.c +++ b/src/bdd/dsd/dsdTree.c @@ -517,6 +517,33 @@ Dsd_Node_t ** Dsd_TreeCollectNodesDfs( Dsd_Manager_t * pDsdMan, int * pnNodes ) return ppNodes; } +/**Function************************************************************* + + Synopsis [Creates the DFS ordered array of DSD nodes in the tree.] + + Description [The collected nodes do not include the terminal nodes + and the constant 1 node. The array of nodes is returned. The number + of entries in the array is returned in the variale pnNodes.] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Dsd_Node_t ** Dsd_TreeCollectNodesDfsOne( Dsd_Manager_t * pDsdMan, Dsd_Node_t * pNode, int * pnNodes ) +{ + Dsd_Node_t ** ppNodes; + int nNodes, nNodesAlloc; + nNodesAlloc = Dsd_TreeCountNonTerminalNodesOne(pNode); + nNodes = 0; + ppNodes = ALLOC( Dsd_Node_t *, nNodesAlloc ); + Dsd_TreeCollectNodesDfs_rec( Dsd_Regular(pNode), ppNodes, &nNodes ); + Dsd_TreeUnmark_rec(Dsd_Regular(pNode)); + assert( nNodesAlloc == nNodes ); + *pnNodes = nNodes; + return ppNodes; +} + /**Function************************************************************* @@ -777,9 +804,7 @@ DdNode * Dsd_TreeGetPrimeFunctionOld( DdManager * dd, Dsd_Node_t * pNode, int fR DdNode * bCof0, * bCof1, * bCube0, * bCube1, * bNewFunc, * bTemp; int i; int fAllBuffs = 1; - int * pPermute; - - pPermute = ALLOC( int, dd->size ); + static int Permute[MAXINPUTS]; assert( pNode ); assert( !Dsd_IsComplement( pNode ) ); @@ -821,14 +846,13 @@ DdNode * Dsd_TreeGetPrimeFunctionOld( DdManager * dd, Dsd_Node_t * pNode, int fR // remap the function to the first variables of the manager for ( i = 0; i < pNode->nDecs; i++ ) // Permute[ pNode->pDecs[i]->S->index ] = dd->invperm[i]; - pPermute[ pNode->pDecs[i]->S->index ] = i; + Permute[ pNode->pDecs[i]->S->index ] = i; - bNewFunc = Cudd_bddPermute( dd, bTemp = bNewFunc, pPermute ); Cudd_Ref( bNewFunc ); + bNewFunc = Cudd_bddPermute( dd, bTemp = bNewFunc, Permute ); Cudd_Ref( bNewFunc ); Cudd_RecursiveDeref( dd, bTemp ); } Cudd_Deref( bNewFunc ); - free( pPermute ); return bNewFunc; } diff --git a/src/map/fpga/fpgaCreate.c b/src/map/fpga/fpgaCreate.c index fc6577fa..aae49f4c 100644 --- a/src/map/fpga/fpgaCreate.c +++ b/src/map/fpga/fpgaCreate.c @@ -172,7 +172,7 @@ Fpga_Man_t * Fpga_ManCreate( int nInputs, int nOutputs, int fVerbose ) p->fAreaRecovery = 1; p->fTree = 0; p->fRefCount = 1; - p->fEpsilon = (float)0.00001; + p->fEpsilon = (float)0.001; Fpga_TableCreate( p ); //if ( p->fVerbose ) diff --git a/src/map/mapper/mapperCreate.c b/src/map/mapper/mapperCreate.c index 4d7ca7d0..826d6287 100644 --- a/src/map/mapper/mapperCreate.c +++ b/src/map/mapper/mapperCreate.c @@ -193,7 +193,6 @@ Map_Man_t * Map_ManCreate( int nInputs, int nOutputs, int fVerbose ) p->pSuperLib = Abc_FrameReadLibSuper(Abc_FrameGetGlobalFrame()); p->nVarsMax = p->pSuperLib->nVarsMax; p->fVerbose = fVerbose; -// p->fEpsilon = (float)0.00001; p->fEpsilon = (float)0.001; assert( p->nVarsMax > 0 ); diff --git a/src/map/mio/mioFunc.c b/src/map/mio/mioFunc.c index 88a7c89c..24b2fecb 100644 --- a/src/map/mio/mioFunc.c +++ b/src/map/mio/mioFunc.c @@ -213,7 +213,7 @@ int Mio_GateParseFormula( Mio_Gate_t * pGate ) Cudd_Ref( pGate->bFunc ); // derive the cover (SOP) - pGate->pSop = Abc_ConvertBddToSop( pGate->pLib->pMmFlex, dd, pGate->bFunc, nPins, pGate->pLib->vCube, -1 ); + pGate->pSop = Abc_ConvertBddToSop( pGate->pLib->pMmFlex, dd, pGate->bFunc, pGate->bFunc, nPins, pGate->pLib->vCube, -1 ); return 0; } diff --git a/src/map/mio/mioUtils.c b/src/map/mio/mioUtils.c index aa373783..15f32890 100644 --- a/src/map/mio/mioUtils.c +++ b/src/map/mio/mioUtils.c @@ -48,7 +48,7 @@ void Mio_LibraryDelete( Mio_Library_t * pLib ) if ( pLib == NULL ) return; // free the bindings of nodes to gates from this library for all networks -// Mv_FrameFreeNetworkBindings( Mv_FrameGetGlobalFrame() ); + Abc_FrameUnmapAllNetworks( Abc_FrameGetGlobalFrame() ); // free the library FREE( pLib->pName ); Mio_LibraryForEachGateSafe( pLib, pGate, pGate2 ) diff --git a/src/misc/extra/extra.h b/src/misc/extra/extra.h index ec4023b0..568eef7d 100644 --- a/src/misc/extra/extra.h +++ b/src/misc/extra/extra.h @@ -111,6 +111,7 @@ extern int * Extra_SupportArray( DdManager * dd, DdNode * F, int * suppor extern int * Extra_VectorSupportArray( DdManager * dd, DdNode ** F, int n, int * support ); extern DdNode * Extra_bddFindOneCube( DdManager * dd, DdNode * bF ); extern DdNode * Extra_bddGetOneCube( DdManager * dd, DdNode * bFunc ); +extern DdNode * Extra_bddComputeRangeCube( DdManager * dd, int iStart, int iStop ); /*=== extraUtilFile.c ========================================================*/ diff --git a/src/misc/extra/extraUtilBdd.c b/src/misc/extra/extraUtilBdd.c index 32fdca2c..38e3345c 100644 --- a/src/misc/extra/extraUtilBdd.c +++ b/src/misc/extra/extraUtilBdd.c @@ -656,6 +656,34 @@ DdNode * Extra_bddGetOneCube( DdManager * dd, DdNode * bFunc ) return bRes; } +/**Function******************************************************************** + + Synopsis [Performs the reordering-sensitive step of Extra_bddMove().] + + Description [] + + SideEffects [] + + SeeAlso [] + +******************************************************************************/ +DdNode * Extra_bddComputeRangeCube( DdManager * dd, int iStart, int iStop ) +{ + DdNode * bTemp, * bProd; + int i; + assert( iStart <= iStop ); + assert( iStart >= 0 && iStart <= dd->size ); + assert( iStop >= 0 && iStop <= dd->size ); + bProd = b1; Cudd_Ref( bProd ); + for ( i = iStart; i < iStop; i++ ) + { + bProd = Cudd_bddAnd( dd, bTemp = bProd, dd->vars[i] ); Cudd_Ref( bProd ); + Cudd_RecursiveDeref( dd, bTemp ); + } + Cudd_Deref( bProd ); + return bProd; +} + /*---------------------------------------------------------------------------*/ /* Definition of internal functions */ /*---------------------------------------------------------------------------*/ diff --git a/src/misc/vec/vecFan.h b/src/misc/vec/vecFan.h index 7bfded4a..451724d6 100644 --- a/src/misc/vec/vecFan.h +++ b/src/misc/vec/vecFan.h @@ -57,6 +57,8 @@ struct Vec_Fan_t_ /// MACRO DEFITIONS /// //////////////////////////////////////////////////////////////////////// +#define Vec_FanForEachEntry( vVec, Entry, i ) \ + for ( i = 0; (i < Vec_FanSize(vVec)) && (((Entry) = Vec_FanEntry(vVec, i)), 1); i++ ) //////////////////////////////////////////////////////////////////////// /// FUNCTION DEFITIONS /// diff --git a/src/misc/vec/vecInt.h b/src/misc/vec/vecInt.h index 8cca2b29..975b61cf 100644 --- a/src/misc/vec/vecInt.h +++ b/src/misc/vec/vecInt.h @@ -48,6 +48,9 @@ struct Vec_Int_t_ /// MACRO DEFITIONS /// //////////////////////////////////////////////////////////////////////// +#define Vec_IntForEachEntry( vVec, Entry, i ) \ + for ( i = 0; (i < Vec_IntSize(vVec)) && (((Entry) = Vec_IntEntry(vVec, i)), 1); i++ ) + //////////////////////////////////////////////////////////////////////// /// FUNCTION DEFITIONS /// //////////////////////////////////////////////////////////////////////// diff --git a/src/misc/vec/vecPtr.h b/src/misc/vec/vecPtr.h index 0ba1bdc5..eb551d1c 100644 --- a/src/misc/vec/vecPtr.h +++ b/src/misc/vec/vecPtr.h @@ -48,6 +48,9 @@ struct Vec_Ptr_t_ /// MACRO DEFITIONS /// //////////////////////////////////////////////////////////////////////// +#define Vec_PtrForEachEntry( vVec, pEntry, i ) \ + for ( i = 0; (i < Vec_PtrSize(vVec)) && (((pEntry) = Vec_PtrEntry(vVec, i)), 1); i++ ) + //////////////////////////////////////////////////////////////////////// /// FUNCTION DEFITIONS /// //////////////////////////////////////////////////////////////////////// @@ -418,6 +421,29 @@ static inline void * Vec_PtrPop( Vec_Ptr_t * p ) /**Function************************************************************* + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +static inline void Vec_PtrRemove( Vec_Ptr_t * p, void * Entry ) +{ + int i; + for ( i = 0; i < p->nSize; i++ ) + if ( p->pArray[i] == Entry ) + break; + assert( i < p->nSize ); + for ( i++; i < p->nSize; i++ ) + p->pArray[i-1] = p->pArray[i]; + p->nSize--; +} + +/**Function************************************************************* + Synopsis [Moves the first nItems to the end.] Description [] diff --git a/src/misc/vec/vecStr.h b/src/misc/vec/vecStr.h index 367304d4..33be5f1d 100644 --- a/src/misc/vec/vecStr.h +++ b/src/misc/vec/vecStr.h @@ -48,6 +48,9 @@ struct Vec_Str_t_ /// MACRO DEFITIONS /// //////////////////////////////////////////////////////////////////////// +#define Vec_StrForEachEntry( vVec, Entry, i ) \ + for ( i = 0; (i < Vec_StrSize(vVec)) && (((Entry) = Vec_StrEntry(vVec, i)), 1); i++ ) + //////////////////////////////////////////////////////////////////////// /// FUNCTION DEFITIONS /// //////////////////////////////////////////////////////////////////////// diff --git a/src/opt/fxu/fxu.c b/src/opt/fxu/fxu.c index 4b95b5a5..46f7ca1a 100644 --- a/src/opt/fxu/fxu.c +++ b/src/opt/fxu/fxu.c @@ -39,21 +39,14 @@ static int s_MemoryPeak; Synopsis [Performs fast_extract on a set of covers.] - Description [All the covers are given in the array p->ppCovers. - The resulting covers are returned in the array p->ppCoversNew. - The number of entries in both cover arrays is equal to the number - of all values in the current nodes plus the max expected number - of extracted nodes (p->nValuesCi + p->nValuesInt + p->nValuesExtMax). - The first p->nValuesCi entries, corresponding to the CI nodes, are NULL. - The next p->nValuesInt entries, corresponding to the int nodes, are covers - from which the divisors are extracted. The last p->nValuesExtMax entries - are reserved for the new covers to be extracted. The number of extracted - covers is returned. This number does not exceed the given number (p->nNodesExt). + Description [All the covers are given in the array p->vSops. + The resulting covers are returned in the array p->vSopsNew. + The entries in these arrays correspond to objects in the network. + The entries corresponding to the PI and objects with trivial covers are NULL. + The number of extracted covers (not exceeding p->nNodesExt) is returned. Two other things are important for the correct operation of this procedure: - (1) The input covers should be SCC-free. (2) The literal array (pCover->pLits) - is allocated in each cover. The i-th entry in the literal array of a cover - is the number of the cover in the array p->ppCovers, which represents this - literal (variable value) in the given cover.] + (1) The input covers do not have duplicated fanins and are SCC-free. + (2) The fanins array contains the numbers of the fanin objects.] SideEffects [] diff --git a/src/opt/fxu/fxu.h b/src/opt/fxu/fxu.h index 5bc1e75f..e9f63ea3 100644 --- a/src/opt/fxu/fxu.h +++ b/src/opt/fxu/fxu.h @@ -48,37 +48,8 @@ struct FxuDataStruct bool fUse0; // set to 1 to have 0-weight also extracted bool fUseCompl; // set to 1 to have complement taken into account bool fVerbose; // set to 1 to have verbose output - int nPairsMax; // the maximum number of cube pairs to consider -/* - // parameters of the network - int fMvNetwork; // the network has some MV nodes - // the information about nodes - int nNodesCi; // the number of CI nodes of the network - int nNodesInt; // the number of internal nodes of the network - int nNodesOld; // the number of CI and int nodes - int nNodesNew; // the number of added nodes - int nNodesExt; // the max number of (binary) nodes to be added by FX - int nNodesAlloc; // the total number of all nodes - int * pNode2Value; // for each node, the number of its first value - // the information about values - int nValuesCi; // the total number of values of CI nodes - int nValuesInt; // the total number of values of int nodes - int nValuesOld; // the number of CI and int values - int nValuesNew; // the number of values added nodes - int nValuesExt; // the total number of values of the added nodes - int nValuesAlloc; // the total number of all values of all nodes - int * pValue2Node; // for each value, the number of its node - // the information about covers - Mvc_Cover_t ** ppCovers; // for each value, the corresponding cover - Mvc_Cover_t ** ppCoversNew; // for each value, the corresponding cover after FX - // the MVC manager - Mvc_Manager_t * pManMvc; -*/ - // statistics - int nNodesOld; // the old number of nodes int nNodesExt; // the number of divisors to extract - int nNodesNew; // the number of divisors extracted - + int nPairsMax; // the maximum number of cube pairs to consider // the input information Vec_Ptr_t * vSops; // the SOPs for each node in the network Vec_Ptr_t * vFanins; // the fanins of each node in the network @@ -87,6 +58,9 @@ struct FxuDataStruct Vec_Ptr_t * vFaninsNew; // the fanins of each node in the network after extraction // the SOP manager Extra_MmFlex_t * pManSop; + // statistics + int nNodesOld; // the old number of nodes + int nNodesNew; // the number of divisors actually extracted }; //////////////////////////////////////////////////////////////////////// diff --git a/src/opt/fxu/fxuCreate.c b/src/opt/fxu/fxuCreate.c index 04b23fce..b061f53d 100644 --- a/src/opt/fxu/fxuCreate.c +++ b/src/opt/fxu/fxuCreate.c @@ -24,21 +24,21 @@ /// DECLARATIONS /// //////////////////////////////////////////////////////////////////////// -extern int Fxu_PreprocessCubePairs( Fxu_Matrix * p, Vec_Ptr_t * vCovers, int nPairsTotal, int nPairsMax ); - static void Fxu_CreateMatrixAddCube( Fxu_Matrix * p, Fxu_Cube * pCube, char * pSopCube, Vec_Fan_t * vFanins, int * pOrder ); static int Fxu_CreateMatrixLitCompare( int * ptrX, int * ptrY ); static void Fxu_CreateCoversNode( Fxu_Matrix * p, Fxu_Data_t * pData, int iNode, Fxu_Cube * pCubeFirst, Fxu_Cube * pCubeNext ); static Fxu_Cube * Fxu_CreateCoversFirstCube( Fxu_Matrix * p, Fxu_Data_t * pData, int iNode ); static Abc_Fan_t * s_pLits; +extern int Fxu_PreprocessCubePairs( Fxu_Matrix * p, Vec_Ptr_t * vCovers, int nPairsTotal, int nPairsMax ); + //////////////////////////////////////////////////////////////////////// /// FUNCTION DEFITIONS /// //////////////////////////////////////////////////////////////////////// /**Function************************************************************* - Synopsis [Creates the sparse matrix from the array of Sop covers.] + Synopsis [Creates the sparse matrix from the array of SOPs.] Description [] @@ -53,6 +53,7 @@ Fxu_Matrix * Fxu_CreateMatrix( Fxu_Data_t * pData ) Fxu_Var * pVar; Fxu_Cube * pCubeFirst, * pCubeNew; Fxu_Cube * pCube1, * pCube2; + Vec_Fan_t * vFanins; char * pSopCover; char * pSopCube; int * pOrder, nBitsMax; @@ -63,12 +64,11 @@ Fxu_Matrix * Fxu_CreateMatrix( Fxu_Data_t * pData ) int nCubes; int iCube, iPair; int nFanins; - Vec_Fan_t * vFanins; // collect all sorts of statistics - nCubesTotal = 0; - nPairsTotal = 0; - nPairsStore = 0; + nCubesTotal = 0; + nPairsTotal = 0; + nPairsStore = 0; nBitsMax = -1; for ( i = 0; i < pData->nNodesOld; i++ ) if ( pSopCover = pData->vSops->pArray[i] ) @@ -158,12 +158,11 @@ Fxu_Matrix * Fxu_CreateMatrix( Fxu_Data_t * pData ) Abc_SopForEachCube( pSopCover, nFanins, pSopCube ) { // create the cube - pCubeNew = Fxu_MatrixAddCube( p, pVar, c ); + pCubeNew = Fxu_MatrixAddCube( p, pVar, c++ ); Fxu_CreateMatrixAddCube( p, pCubeNew, pSopCube, vFanins, pOrder ); if ( pCubeFirst == NULL ) pCubeFirst = pCubeNew; pCubeNew->pFirst = pCubeFirst; - c++; } // set the first cube of this var pVar->pFirst = pCubeFirst; @@ -185,10 +184,7 @@ Fxu_Matrix * Fxu_CreateMatrix( Fxu_Data_t * pData ) // add the var pairs to the heap Fxu_MatrixComputeSingles( p ); - // allocate temporary storage for pairs - if ( pData->nPairsMax < 1000 ) - pData->nPairsMax = 1000; - p->pPairsTemp = ALLOC( Fxu_Pair *, pData->nPairsMax * 10 + 100 ); + // print stats if ( pData->fVerbose ) { double Density; @@ -254,8 +250,8 @@ void Fxu_CreateMatrixAddCube( Fxu_Matrix * p, Fxu_Cube * pCube, char * pSopCube, void Fxu_CreateCovers( Fxu_Matrix * p, Fxu_Data_t * pData ) { Fxu_Cube * pCube, * pCubeFirst, * pCubeNext; - int iNode, n; char * pSopCover; + int iNode, n; // get the first cube of the first internal node pCubeFirst = Fxu_CreateCoversFirstCube( p, pData, 0 ); @@ -306,13 +302,11 @@ void Fxu_CreateCovers( Fxu_Matrix * p, Fxu_Data_t * pData ) void Fxu_CreateCoversNode( Fxu_Matrix * p, Fxu_Data_t * pData, int iNode, Fxu_Cube * pCubeFirst, Fxu_Cube * pCubeNext ) { Vec_Int_t * vInputsNew; - char * pSopCover; - char * pSopCube; + char * pSopCover, * pSopCube; Fxu_Var * pVar; Fxu_Cube * pCube; Fxu_Lit * pLit; int iNum, nCubes, v; - int fEmptyCube; // collect positive polarity variable in the cubes between pCubeFirst and pCubeNext Fxu_MatrixRingVarsStart( p ); @@ -362,7 +356,6 @@ void Fxu_CreateCoversNode( Fxu_Matrix * p, Fxu_Data_t * pData, int iNode, Fxu_Cu // get hold of the SOP cube pSopCube = pSopCover + nCubes * (vInputsNew->nSize + 3); // insert literals - fEmptyCube = 1; for ( pLit = pCube->lLits.pHead; pLit; pLit = pLit->pHNext ) { iNum = pLit->pVar->lLits.nItems; // hack - reuse lLits.nItems @@ -371,14 +364,13 @@ void Fxu_CreateCoversNode( Fxu_Matrix * p, Fxu_Data_t * pData, int iNode, Fxu_Cu pSopCube[iNum] = (pLit->pVar->iVar & 1)? '0' : '1'; // reverse CST else pSopCube[iNum] = (pLit->pVar->iVar & 1)? '1' : '0'; // no CST - fEmptyCube = 0; } - assert( !fEmptyCube ); // count the cube nCubes++; } assert( nCubes == Abc_SopGetCubeNum(pSopCover) ); + // set the new cover and the array of fanins pData->vSopsNew->pArray[iNode] = pSopCover; pData->vFaninsNew->pArray[iNode] = vInputsNew; } diff --git a/src/opt/fxu/fxuInt.h b/src/opt/fxu/fxuInt.h index 1f5a19b8..59b2df6d 100644 --- a/src/opt/fxu/fxuInt.h +++ b/src/opt/fxu/fxuInt.h @@ -25,6 +25,7 @@ #include "util.h" #include "extra.h" +#include "vec.h" //////////////////////////////////////////////////////////////////////// /// PARAMETERS /// @@ -158,9 +159,6 @@ struct FxuHeapSingle // sparse matrix struct FxuMatrix // ~ 30 words { - // information about the network -// int fMvNetwork; // set to 1 if the network has MV nodes -// int * pValue2Node; // the mapping of values into nodes // the cubes Fxu_ListCube lCubes; // the double linked list of cubes // the values (binary literals) @@ -185,9 +183,7 @@ struct FxuMatrix // ~ 30 words Fxu_Var * pOrderVars; Fxu_Var ** ppTailVars; // temporary storage for pairs - Fxu_Pair ** pPairsTemp; - int nPairsTemp; -// int nPairsMax; + Vec_Ptr_t * vPairs; // statistics int nEntries; // the total number of entries in the sparse matrix int nDivs1; // the single cube divisors taken diff --git a/src/opt/fxu/fxuMatrix.c b/src/opt/fxu/fxuMatrix.c index 0b732aef..503ba2f1 100644 --- a/src/opt/fxu/fxuMatrix.c +++ b/src/opt/fxu/fxuMatrix.c @@ -77,6 +77,7 @@ Fxu_Matrix * Fxu_MatrixAllocate() #endif p->pHeapDouble = Fxu_HeapDoubleStart(); p->pHeapSingle = Fxu_HeapSingleStart(); + p->vPairs = Vec_PtrAlloc( 100 ); return p; } @@ -132,9 +133,10 @@ void Fxu_MatrixDelete( Fxu_Matrix * p ) Extra_MmFixedStop( p->pMemMan, 0 ); #endif + Vec_PtrFree( p->vPairs ); FREE( p->pppPairs ); FREE( p->ppPairs ); - FREE( p->pPairsTemp ); +// FREE( p->pPairsTemp ); FREE( p->pTable ); FREE( p->ppVars ); FREE( p ); @@ -305,20 +307,8 @@ void Fxu_MatrixAddDivisor( Fxu_Matrix * p, Fxu_Cube * pCube1, Fxu_Cube * pCube2 // canonicize the pair Fxu_PairCanonicize( &pCube1, &pCube2 ); - -/* // compute the hash key - if ( p->fMvNetwork ) -// if ( 0 ) - { // in case of MV network, if all the values in the cube-free divisor - // belong to the same MV variable, this cube pair is not a divisor - Key = Fxu_PairHashKeyMv( p, pCube1, pCube2, &nBase, &nLits1, &nLits2 ); - if ( Key == 0 ) - return; - } - else -*/ - Key = Fxu_PairHashKey( p, pCube1, pCube2, &nBase, &nLits1, &nLits2 ); + Key = Fxu_PairHashKey( p, pCube1, pCube2, &nBase, &nLits1, &nLits2 ); // create the cube pair pPair = Fxu_PairAlloc( p, pCube1, pCube2 ); @@ -330,11 +320,13 @@ void Fxu_MatrixAddDivisor( Fxu_Matrix * p, Fxu_Cube * pCube1, Fxu_Cube * pCube2 fFound = 0; Key %= p->nTableSize; Fxu_TableForEachDouble( p, Key, pDiv ) + { if ( Fxu_PairCompare( pPair, pDiv->lPairs.pTail ) ) // they are equal { fFound = 1; break; } + } if ( !fFound ) { // create the new divisor diff --git a/src/opt/fxu/fxuUpdate.c b/src/opt/fxu/fxuUpdate.c index b781e0b1..4006bc76 100644 --- a/src/opt/fxu/fxuUpdate.c +++ b/src/opt/fxu/fxuUpdate.c @@ -287,10 +287,12 @@ void Fxu_UpdateDoublePairs( Fxu_Matrix * p, Fxu_Double * pDouble, Fxu_Var * pVar // collect and sort the pairs Fxu_UpdatePairsSort( p, pDouble ); - for ( i = 0; i < p->nPairsTemp; i++ ) +// for ( i = 0; i < p->nPairsTemp; i++ ) + for ( i = 0; i < p->vPairs->nSize; i++ ) { // get the pair - pPair = p->pPairsTemp[i]; +// pPair = p->pPairsTemp[i]; + pPair = p->vPairs->pArray[i]; // out of the two cubes, select the one which comes earlier pCubeUse = Fxu_PairMinCube( pPair ); pCubeRem = Fxu_PairMaxCube( pPair ); @@ -312,7 +314,7 @@ void Fxu_UpdateDoublePairs( Fxu_Matrix * p, Fxu_Double * pDouble, Fxu_Var * pVar // remove the pair MEM_FREE_FXU( p, Fxu_Pair, 1, pPair ); } - p->nPairsTemp = 0; + p->vPairs->nSize = 0; } /**Function************************************************************* @@ -575,18 +577,17 @@ void Fxu_UpdateMatrixSingleClean( Fxu_Matrix * p, Fxu_Var * pVar1, Fxu_Var * pVa void Fxu_UpdatePairsSort( Fxu_Matrix * p, Fxu_Double * pDouble ) { Fxu_Pair * pPair; - // order the pairs by the first cube to ensure that - // new literals are added to the matrix from top to bottom - // collect pairs into the array - p->nPairsTemp = 0; + // order the pairs by the first cube to ensure that new literals are added + // to the matrix from top to bottom - collect pairs into the array + p->vPairs->nSize = 0; Fxu_DoubleForEachPair( pDouble, pPair ) - p->pPairsTemp[ p->nPairsTemp++ ] = pPair; - if ( p->nPairsTemp > 1 ) - { // sort - qsort( (void *)p->pPairsTemp, p->nPairsTemp, sizeof(Fxu_Pair *), - (int (*)(const void *, const void *)) Fxu_UpdatePairCompare ); - assert( Fxu_UpdatePairCompare( p->pPairsTemp, p->pPairsTemp + p->nPairsTemp - 1 ) < 0 ); - } + Vec_PtrPush( p->vPairs, pPair ); + if ( p->vPairs->nSize < 2 ) + return; + // sort + qsort( (void *)p->vPairs->pArray, p->vPairs->nSize, sizeof(Fxu_Pair *), + (int (*)(const void *, const void *)) Fxu_UpdatePairCompare ); + assert( Fxu_UpdatePairCompare( (Fxu_Pair**)p->vPairs->pArray, (Fxu_Pair**)p->vPairs->pArray + p->vPairs->nSize - 1 ) < 0 ); } /**Function************************************************************* diff --git a/src/opt/module.make b/src/opt/module.make deleted file mode 100644 index d6d908e7..00000000 --- a/src/opt/module.make +++ /dev/null @@ -1 +0,0 @@ -SRC += |