diff options
| -rw-r--r-- | Makefile | 2 | ||||
| -rw-r--r-- | abc.dsp | 21 | ||||
| -rw-r--r-- | abc.opt | bin | 52736 -> 51712 bytes | |||
| -rw-r--r-- | abc.plg | 607 | ||||
| -rw-r--r-- | abc.rc | 15 | ||||
| -rw-r--r-- | src/base/abc/abc.c | 298 | ||||
| -rw-r--r-- | src/base/abc/abc.h | 19 | ||||
| -rw-r--r-- | src/base/abc/abcCheck.c | 6 | ||||
| -rw-r--r-- | src/base/abc/abcCollapse.c | 160 | ||||
| -rw-r--r-- | src/base/abc/abcCreate.c | 40 | ||||
| -rw-r--r-- | src/base/abc/abcDsd.c | 34 | ||||
| -rw-r--r-- | src/base/abc/abcMinBase.c | 65 | ||||
| -rw-r--r-- | src/base/abc/abcNtbdd.c | 402 | ||||
| -rw-r--r-- | src/base/abc/abcPrint.c | 16 | ||||
| -rw-r--r-- | src/base/abc/abcRefactor.c | 2 | ||||
| -rw-r--r-- | src/base/abc/abcRefs.c | 75 | ||||
| -rw-r--r-- | src/base/abc/abcRenode.c | 27 | ||||
| -rw-r--r-- | src/base/abc/abcRewrite.c | 2 | ||||
| -rw-r--r-- | src/base/abc/abcShow.c | 2 | ||||
| -rw-r--r-- | src/base/abc/abcSweep.c | 175 | ||||
| -rw-r--r-- | src/base/abc/abcUtil.c | 47 | ||||
| -rw-r--r-- | src/base/abc/module.make | 1 | ||||
| -rw-r--r-- | src/opt/dec/dec.h | 391 | ||||
| -rw-r--r-- | src/opt/dec/module.make | 1 | ||||
| -rw-r--r-- | src/sat/fraig/fraigSat.c | 2 | ||||
| -rw-r--r-- | src/sop/ft/ftFactor.c | 1 | ||||
| -rw-r--r-- | src/sop/ft/ftPrint.c | 35 |
27 files changed, 2144 insertions, 302 deletions
@@ -10,7 +10,7 @@ MODULES := src/base/abc src/base/cmd src/base/io src/base/main \ 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/cut src/opt/fxu src/opt/rwr \ + src/opt/cut src/opt/dec src/opt/fxu src/opt/rwr \ src/sat/asat src/sat/csat src/sat/msat src/sat/fraig src/sat/sim \ src/seq \ src/sop/ft src/sop/mvc @@ -42,7 +42,7 @@ RSC=rc.exe # PROP Ignore_Export_Lib 0 # PROP Target_Dir "" # ADD BASE CPP /nologo /W3 /GX /O2 /D "WIN32" /D "NDEBUG" /D "_CONSOLE" /D "_MBCS" /YX /FD /c -# ADD CPP /nologo /W3 /GX /O2 /I "src\base\abc" /I "src\base\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\opt\rwr" /I "src\opt\cut" /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 "NDEBUG" /D "_CONSOLE" /D "_MBCS" /D "__STDC__" /D "HAVE_ASSERT_H" /FR /YX /FD /c +# ADD CPP /nologo /W3 /GX /O2 /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\cut" /I "src\opt\dec" /I "src\opt\fxu" /I "src\opt\rwr" /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 "NDEBUG" /D "_CONSOLE" /D "_MBCS" /D "__STDC__" /D "HAVE_ASSERT_H" /FR /YX /FD /c # ADD BASE RSC /l 0x409 /d "NDEBUG" # ADD RSC /l 0x409 /d "NDEBUG" BSC32=bscmake.exe @@ -66,7 +66,8 @@ LINK32=link.exe # PROP Ignore_Export_Lib 0 # PROP Target_Dir "" # ADD BASE CPP /nologo /W3 /Gm /GX /ZI /Od /D "WIN32" /D "_DEBUG" /D "_CONSOLE" /D "_MBCS" /YX /FD /GZ /c -# ADD CPP /nologo /W3 /Gm /GX /ZI /Od /I "src\base\abc" /I "src\base\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\opt\rwr" /I "src\opt\cut" /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 /YX /FD /GZ /c +# ADD CPP /nologo /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\cut" /I "src\opt\dec" /I "src\opt\fxu" /I "src\opt\rwr" /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 /YX /FD /GZ /c +# SUBTRACT CPP /X # ADD BASE RSC /l 0x409 /d "_DEBUG" # ADD RSC /l 0x409 /d "_DEBUG" BSC32=bscmake.exe @@ -185,6 +186,10 @@ SOURCE=.\src\base\abc\abcNetlist.c # End Source File # Begin Source File +SOURCE=.\src\base\abc\abcNtbdd.c +# End Source File +# Begin Source File + SOURCE=.\src\base\abc\abcPrint.c # End Source File # Begin Source File @@ -1072,10 +1077,6 @@ SOURCE=.\src\sat\csat\csat_apis.h # Begin Group "opt" # PROP Default_Filter "" -# Begin Group "fxa" - -# PROP Default_Filter "" -# End Group # Begin Group "fxu" # PROP Default_Filter "" @@ -1212,6 +1213,14 @@ SOURCE=.\src\opt\cut\cutTable.c SOURCE=.\src\opt\cut\cutTruth.c # End Source File # End Group +# Begin Group "dec" + +# PROP Default_Filter "" +# Begin Source File + +SOURCE=.\src\opt\dec\dec.h +# End Source File +# End Group # End Group # Begin Group "map" @@ -6,13 +6,292 @@ --------------------Configuration: abc - Win32 Debug-------------------- </h3> <h3>Command Lines</h3> -Creating temporary file "C:\DOCUME~1\alanmi\LOCALS~1\Temp\RSP358F.tmp" with contents +Creating temporary file "C:\DOCUME~1\alanmi\LOCALS~1\Temp\RSP37EA.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\opt\rwr" /I "src\opt\cut" /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 +/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\cut" /I "src\opt\dec" /I "src\opt\fxu" /I "src\opt\rwr" /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\base\abc\abc.c" +"C:\_projects\abc\src\base\abc\abcAig.c" +"C:\_projects\abc\src\base\abc\abcAttach.c" +"C:\_projects\abc\src\base\abc\abcBalance.c" +"C:\_projects\abc\src\base\abc\abcCheck.c" +"C:\_projects\abc\src\base\abc\abcCollapse.c" +"C:\_projects\abc\src\base\abc\abcCreate.c" +"C:\_projects\abc\src\base\abc\abcCut.c" +"C:\_projects\abc\src\base\abc\abcDfs.c" +"C:\_projects\abc\src\base\abc\abcDsd.c" +"C:\_projects\abc\src\base\abc\abcFanio.c" +"C:\_projects\abc\src\base\abc\abcFpga.c" +"C:\_projects\abc\src\base\abc\abcFraig.c" +"C:\_projects\abc\src\base\abc\abcFunc.c" +"C:\_projects\abc\src\base\abc\abcFxu.c" +"C:\_projects\abc\src\base\abc\abcLatch.c" +"C:\_projects\abc\src\base\abc\abcMap.c" +"C:\_projects\abc\src\base\abc\abcMinBase.c" +"C:\_projects\abc\src\base\abc\abcMiter.c" +"C:\_projects\abc\src\base\abc\abcNames.c" +"C:\_projects\abc\src\base\abc\abcNetlist.c" +"C:\_projects\abc\src\base\abc\abcNtbdd.c" +"C:\_projects\abc\src\base\abc\abcPrint.c" +"C:\_projects\abc\src\base\abc\abcReconv.c" +"C:\_projects\abc\src\base\abc\abcRefactor.c" +"C:\_projects\abc\src\base\abc\abcRefs.c" +"C:\_projects\abc\src\base\abc\abcRenode.c" +"C:\_projects\abc\src\base\abc\abcRewrite.c" +"C:\_projects\abc\src\base\abc\abcSat.c" +"C:\_projects\abc\src\base\abc\abcSeq.c" +"C:\_projects\abc\src\base\abc\abcSeqRetime.c" +"C:\_projects\abc\src\base\abc\abcShow.c" +"C:\_projects\abc\src\base\abc\abcSop.c" +"C:\_projects\abc\src\base\abc\abcStrash.c" +"C:\_projects\abc\src\base\abc\abcSweep.c" +"C:\_projects\abc\src\base\abc\abcSymm.c" +"C:\_projects\abc\src\base\abc\abcTiming.c" +"C:\_projects\abc\src\base\abc\abcUnreach.c" +"C:\_projects\abc\src\base\abc\abcUtil.c" +"C:\_projects\abc\src\base\abc\abcVerify.c" +"C:\_projects\abc\src\base\cmd\cmd.c" +"C:\_projects\abc\src\base\cmd\cmdAlias.c" +"C:\_projects\abc\src\base\cmd\cmdApi.c" +"C:\_projects\abc\src\base\cmd\cmdFlag.c" +"C:\_projects\abc\src\base\cmd\cmdHist.c" +"C:\_projects\abc\src\base\cmd\cmdUtils.c" +"C:\_projects\abc\src\base\io\io.c" +"C:\_projects\abc\src\base\io\ioRead.c" +"C:\_projects\abc\src\base\io\ioReadBench.c" +"C:\_projects\abc\src\base\io\ioReadBlif.c" +"C:\_projects\abc\src\base\io\ioReadEdif.c" +"C:\_projects\abc\src\base\io\ioReadEqn.c" +"C:\_projects\abc\src\base\io\ioReadPla.c" +"C:\_projects\abc\src\base\io\ioReadVerilog.c" +"C:\_projects\abc\src\base\io\ioUtil.c" +"C:\_projects\abc\src\base\io\ioWriteBench.c" +"C:\_projects\abc\src\base\io\ioWriteBlif.c" +"C:\_projects\abc\src\base\io\ioWriteCnf.c" +"C:\_projects\abc\src\base\io\ioWriteDot.c" +"C:\_projects\abc\src\base\io\ioWriteEqn.c" +"C:\_projects\abc\src\base\io\ioWriteGml.c" +"C:\_projects\abc\src\base\io\ioWritePla.c" +"C:\_projects\abc\src\base\main\main.c" +"C:\_projects\abc\src\base\main\mainFrame.c" +"C:\_projects\abc\src\base\main\mainInit.c" +"C:\_projects\abc\src\base\main\mainUtils.c" +"C:\_projects\abc\src\bdd\cudd\cuddAddAbs.c" +"C:\_projects\abc\src\bdd\cudd\cuddAddApply.c" +"C:\_projects\abc\src\bdd\cudd\cuddAddFind.c" +"C:\_projects\abc\src\bdd\cudd\cuddAddInv.c" +"C:\_projects\abc\src\bdd\cudd\cuddAddIte.c" +"C:\_projects\abc\src\bdd\cudd\cuddAddNeg.c" +"C:\_projects\abc\src\bdd\cudd\cuddAddWalsh.c" +"C:\_projects\abc\src\bdd\cudd\cuddAndAbs.c" +"C:\_projects\abc\src\bdd\cudd\cuddAnneal.c" +"C:\_projects\abc\src\bdd\cudd\cuddApa.c" +"C:\_projects\abc\src\bdd\cudd\cuddAPI.c" +"C:\_projects\abc\src\bdd\cudd\cuddApprox.c" +"C:\_projects\abc\src\bdd\cudd\cuddBddAbs.c" +"C:\_projects\abc\src\bdd\cudd\cuddBddCorr.c" +"C:\_projects\abc\src\bdd\cudd\cuddBddIte.c" +"C:\_projects\abc\src\bdd\cudd\cuddBridge.c" +"C:\_projects\abc\src\bdd\cudd\cuddCache.c" +"C:\_projects\abc\src\bdd\cudd\cuddCheck.c" +"C:\_projects\abc\src\bdd\cudd\cuddClip.c" +"C:\_projects\abc\src\bdd\cudd\cuddCof.c" +"C:\_projects\abc\src\bdd\cudd\cuddCompose.c" +"C:\_projects\abc\src\bdd\cudd\cuddDecomp.c" +"C:\_projects\abc\src\bdd\cudd\cuddEssent.c" +"C:\_projects\abc\src\bdd\cudd\cuddExact.c" +"C:\_projects\abc\src\bdd\cudd\cuddExport.c" +"C:\_projects\abc\src\bdd\cudd\cuddGenCof.c" +"C:\_projects\abc\src\bdd\cudd\cuddGenetic.c" +"C:\_projects\abc\src\bdd\cudd\cuddGroup.c" +"C:\_projects\abc\src\bdd\cudd\cuddHarwell.c" +"C:\_projects\abc\src\bdd\cudd\cuddInit.c" +"C:\_projects\abc\src\bdd\cudd\cuddInteract.c" +"C:\_projects\abc\src\bdd\cudd\cuddLCache.c" +"C:\_projects\abc\src\bdd\cudd\cuddLevelQ.c" +"C:\_projects\abc\src\bdd\cudd\cuddLinear.c" +"C:\_projects\abc\src\bdd\cudd\cuddLiteral.c" +"C:\_projects\abc\src\bdd\cudd\cuddMatMult.c" +"C:\_projects\abc\src\bdd\cudd\cuddPriority.c" +"C:\_projects\abc\src\bdd\cudd\cuddRead.c" +"C:\_projects\abc\src\bdd\cudd\cuddRef.c" +"C:\_projects\abc\src\bdd\cudd\cuddReorder.c" +"C:\_projects\abc\src\bdd\cudd\cuddSat.c" +"C:\_projects\abc\src\bdd\cudd\cuddSign.c" +"C:\_projects\abc\src\bdd\cudd\cuddSolve.c" +"C:\_projects\abc\src\bdd\cudd\cuddSplit.c" +"C:\_projects\abc\src\bdd\cudd\cuddSubsetHB.c" +"C:\_projects\abc\src\bdd\cudd\cuddSubsetSP.c" +"C:\_projects\abc\src\bdd\cudd\cuddSymmetry.c" +"C:\_projects\abc\src\bdd\cudd\cuddTable.c" +"C:\_projects\abc\src\bdd\cudd\cuddUtil.c" +"C:\_projects\abc\src\bdd\cudd\cuddWindow.c" +"C:\_projects\abc\src\bdd\cudd\cuddZddCount.c" +"C:\_projects\abc\src\bdd\cudd\cuddZddFuncs.c" +"C:\_projects\abc\src\bdd\cudd\cuddZddGroup.c" +"C:\_projects\abc\src\bdd\cudd\cuddZddIsop.c" +"C:\_projects\abc\src\bdd\cudd\cuddZddLin.c" +"C:\_projects\abc\src\bdd\cudd\cuddZddMisc.c" +"C:\_projects\abc\src\bdd\cudd\cuddZddPort.c" +"C:\_projects\abc\src\bdd\cudd\cuddZddReord.c" +"C:\_projects\abc\src\bdd\cudd\cuddZddSetop.c" +"C:\_projects\abc\src\bdd\cudd\cuddZddSymm.c" +"C:\_projects\abc\src\bdd\cudd\cuddZddUtil.c" +"C:\_projects\abc\src\bdd\epd\epd.c" +"C:\_projects\abc\src\bdd\mtr\mtrBasic.c" +"C:\_projects\abc\src\bdd\mtr\mtrGroup.c" +"C:\_projects\abc\src\bdd\parse\parseCore.c" +"C:\_projects\abc\src\bdd\parse\parseStack.c" +"C:\_projects\abc\src\bdd\dsd\dsdApi.c" +"C:\_projects\abc\src\bdd\dsd\dsdCheck.c" +"C:\_projects\abc\src\bdd\dsd\dsdLocal.c" +"C:\_projects\abc\src\bdd\dsd\dsdMan.c" +"C:\_projects\abc\src\bdd\dsd\dsdProc.c" +"C:\_projects\abc\src\bdd\dsd\dsdTree.c" +"C:\_projects\abc\src\bdd\reo\reoApi.c" +"C:\_projects\abc\src\bdd\reo\reoCore.c" +"C:\_projects\abc\src\bdd\reo\reoProfile.c" +"C:\_projects\abc\src\bdd\reo\reoSift.c" +"C:\_projects\abc\src\bdd\reo\reoSwap.c" +"C:\_projects\abc\src\bdd\reo\reoTest.c" +"C:\_projects\abc\src\bdd\reo\reoTransfer.c" +"C:\_projects\abc\src\bdd\reo\reoUnits.c" +"C:\_projects\abc\src\sop\mvc\mvc.c" +"C:\_projects\abc\src\sop\mvc\mvcApi.c" +"C:\_projects\abc\src\sop\mvc\mvcCompare.c" +"C:\_projects\abc\src\sop\mvc\mvcContain.c" +"C:\_projects\abc\src\sop\mvc\mvcCover.c" +"C:\_projects\abc\src\sop\mvc\mvcCube.c" +"C:\_projects\abc\src\sop\mvc\mvcDivide.c" +"C:\_projects\abc\src\sop\mvc\mvcDivisor.c" +"C:\_projects\abc\src\sop\mvc\mvcList.c" +"C:\_projects\abc\src\sop\mvc\mvcLits.c" +"C:\_projects\abc\src\sop\mvc\mvcMan.c" +"C:\_projects\abc\src\sop\mvc\mvcOpAlg.c" +"C:\_projects\abc\src\sop\mvc\mvcOpBool.c" +"C:\_projects\abc\src\sop\mvc\mvcPrint.c" +"C:\_projects\abc\src\sop\mvc\mvcSort.c" +"C:\_projects\abc\src\sop\mvc\mvcUtils.c" +"C:\_projects\abc\src\sop\ft\ftFactor.c" +"C:\_projects\abc\src\sop\ft\ftPrint.c" +"C:\_projects\abc\src\sat\asat\added.c" +"C:\_projects\abc\src\sat\asat\solver.c" +"C:\_projects\abc\src\sat\msat\msatActivity.c" +"C:\_projects\abc\src\sat\msat\msatClause.c" +"C:\_projects\abc\src\sat\msat\msatClauseVec.c" +"C:\_projects\abc\src\sat\msat\msatMem.c" +"C:\_projects\abc\src\sat\msat\msatOrderJ.c" +"C:\_projects\abc\src\sat\msat\msatQueue.c" +"C:\_projects\abc\src\sat\msat\msatRead.c" +"C:\_projects\abc\src\sat\msat\msatSolverApi.c" +"C:\_projects\abc\src\sat\msat\msatSolverCore.c" +"C:\_projects\abc\src\sat\msat\msatSolverIo.c" +"C:\_projects\abc\src\sat\msat\msatSolverSearch.c" +"C:\_projects\abc\src\sat\msat\msatSort.c" +"C:\_projects\abc\src\sat\msat\msatVec.c" +"C:\_projects\abc\src\sat\fraig\fraigApi.c" +"C:\_projects\abc\src\sat\fraig\fraigCanon.c" +"C:\_projects\abc\src\sat\fraig\fraigFanout.c" +"C:\_projects\abc\src\sat\fraig\fraigFeed.c" +"C:\_projects\abc\src\sat\fraig\fraigMan.c" +"C:\_projects\abc\src\sat\fraig\fraigMem.c" +"C:\_projects\abc\src\sat\fraig\fraigNode.c" +"C:\_projects\abc\src\sat\fraig\fraigPrime.c" +"C:\_projects\abc\src\sat\fraig\fraigSat.c" +"C:\_projects\abc\src\sat\fraig\fraigTable.c" +"C:\_projects\abc\src\sat\fraig\fraigUtil.c" +"C:\_projects\abc\src\sat\fraig\fraigVec.c" +"C:\_projects\abc\src\sat\sim\simMan.c" +"C:\_projects\abc\src\sat\sim\simSat.c" +"C:\_projects\abc\src\sat\sim\simSupp.c" +"C:\_projects\abc\src\sat\sim\simSym.c" +"C:\_projects\abc\src\sat\sim\simUnate.c" +"C:\_projects\abc\src\sat\sim\simUtils.c" +"C:\_projects\abc\src\sat\csat\csat_apis.c" +"C:\_projects\abc\src\opt\fxu\fxu.c" +"C:\_projects\abc\src\opt\fxu\fxuCreate.c" +"C:\_projects\abc\src\opt\fxu\fxuHeapD.c" +"C:\_projects\abc\src\opt\fxu\fxuHeapS.c" +"C:\_projects\abc\src\opt\fxu\fxuList.c" +"C:\_projects\abc\src\opt\fxu\fxuMatrix.c" +"C:\_projects\abc\src\opt\fxu\fxuPair.c" +"C:\_projects\abc\src\opt\fxu\fxuPrint.c" +"C:\_projects\abc\src\opt\fxu\fxuReduce.c" +"C:\_projects\abc\src\opt\fxu\fxuSelect.c" +"C:\_projects\abc\src\opt\fxu\fxuSingle.c" +"C:\_projects\abc\src\opt\fxu\fxuUpdate.c" +"C:\_projects\abc\src\opt\rwr\rwrDec.c" +"C:\_projects\abc\src\opt\rwr\rwrEva.c" +"C:\_projects\abc\src\opt\rwr\rwrExp.c" +"C:\_projects\abc\src\opt\rwr\rwrLib.c" +"C:\_projects\abc\src\opt\rwr\rwrMan.c" +"C:\_projects\abc\src\opt\rwr\rwrPrint.c" +"C:\_projects\abc\src\opt\rwr\rwrUtil.c" +"C:\_projects\abc\src\opt\cut\cutMan.c" +"C:\_projects\abc\src\opt\cut\cutMerge.c" +"C:\_projects\abc\src\opt\cut\cutNode.c" +"C:\_projects\abc\src\opt\cut\cutSeq.c" +"C:\_projects\abc\src\opt\cut\cutTable.c" +"C:\_projects\abc\src\opt\cut\cutTruth.c" +"C:\_projects\abc\src\map\fpga\fpga.c" +"C:\_projects\abc\src\map\fpga\fpgaCore.c" +"C:\_projects\abc\src\map\fpga\fpgaCreate.c" +"C:\_projects\abc\src\map\fpga\fpgaCut.c" +"C:\_projects\abc\src\map\fpga\fpgaCutUtils.c" +"C:\_projects\abc\src\map\fpga\fpgaFanout.c" +"C:\_projects\abc\src\map\fpga\fpgaLib.c" +"C:\_projects\abc\src\map\fpga\fpgaMatch.c" +"C:\_projects\abc\src\map\fpga\fpgaTime.c" +"C:\_projects\abc\src\map\fpga\fpgaTruth.c" +"C:\_projects\abc\src\map\fpga\fpgaUtils.c" +"C:\_projects\abc\src\map\fpga\fpgaVec.c" +"C:\_projects\abc\src\map\mapper\mapper.c" +"C:\_projects\abc\src\map\mapper\mapperCanon.c" +"C:\_projects\abc\src\map\mapper\mapperCore.c" +"C:\_projects\abc\src\map\mapper\mapperCreate.c" +"C:\_projects\abc\src\map\mapper\mapperCut.c" +"C:\_projects\abc\src\map\mapper\mapperCutUtils.c" +"C:\_projects\abc\src\map\mapper\mapperFanout.c" +"C:\_projects\abc\src\map\mapper\mapperLib.c" +"C:\_projects\abc\src\map\mapper\mapperMatch.c" +"C:\_projects\abc\src\map\mapper\mapperRefs.c" +"C:\_projects\abc\src\map\mapper\mapperSuper.c" +"C:\_projects\abc\src\map\mapper\mapperTable.c" +"C:\_projects\abc\src\map\mapper\mapperTime.c" +"C:\_projects\abc\src\map\mapper\mapperTree.c" +"C:\_projects\abc\src\map\mapper\mapperTruth.c" +"C:\_projects\abc\src\map\mapper\mapperUtils.c" +"C:\_projects\abc\src\map\mapper\mapperVec.c" +"C:\_projects\abc\src\map\mio\mio.c" +"C:\_projects\abc\src\map\mio\mioApi.c" +"C:\_projects\abc\src\map\mio\mioFunc.c" +"C:\_projects\abc\src\map\mio\mioRead.c" +"C:\_projects\abc\src\map\mio\mioUtils.c" +"C:\_projects\abc\src\map\super\super.c" +"C:\_projects\abc\src\map\super\superAnd.c" +"C:\_projects\abc\src\map\super\superGate.c" +"C:\_projects\abc\src\map\super\superWrite.c" +"C:\_projects\abc\src\misc\extra\extraBddMisc.c" +"C:\_projects\abc\src\misc\extra\extraBddSymm.c" +"C:\_projects\abc\src\misc\extra\extraUtilBitMatrix.c" +"C:\_projects\abc\src\misc\extra\extraUtilCanon.c" +"C:\_projects\abc\src\misc\extra\extraUtilFile.c" +"C:\_projects\abc\src\misc\extra\extraUtilMemory.c" +"C:\_projects\abc\src\misc\extra\extraUtilMisc.c" +"C:\_projects\abc\src\misc\extra\extraUtilProgress.c" +"C:\_projects\abc\src\misc\extra\extraUtilReader.c" +"C:\_projects\abc\src\misc\st\st.c" +"C:\_projects\abc\src\misc\st\stmm.c" +"C:\_projects\abc\src\misc\util\cpu_stats.c" +"C:\_projects\abc\src\misc\util\cpu_time.c" +"C:\_projects\abc\src\misc\util\datalimit.c" +"C:\_projects\abc\src\misc\util\getopt.c" +"C:\_projects\abc\src\misc\util\pathsearch.c" +"C:\_projects\abc\src\misc\util\safe_mem.c" +"C:\_projects\abc\src\misc\util\strsav.c" +"C:\_projects\abc\src\misc\util\texpand.c" ] -Creating command line "cl.exe @C:\DOCUME~1\alanmi\LOCALS~1\Temp\RSP358F.tmp" -Creating temporary file "C:\DOCUME~1\alanmi\LOCALS~1\Temp\RSP3590.tmp" with contents +Creating command line "cl.exe @C:\DOCUME~1\alanmi\LOCALS~1\Temp\RSP37EA.tmp" +Creating temporary file "C:\DOCUME~1\alanmi\LOCALS~1\Temp\RSP37EB.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 @@ -36,6 +315,7 @@ kernel32.lib user32.lib gdi32.lib winspool.lib comdlg32.lib advapi32.lib shell32 .\Debug\abcMiter.obj .\Debug\abcNames.obj .\Debug\abcNetlist.obj +.\Debug\abcNtbdd.obj .\Debug\abcPrint.obj .\Debug\abcReconv.obj .\Debug\abcRefactor.obj @@ -65,12 +345,16 @@ kernel32.lib user32.lib gdi32.lib winspool.lib comdlg32.lib advapi32.lib shell32 .\Debug\ioReadBench.obj .\Debug\ioReadBlif.obj .\Debug\ioReadEdif.obj +.\Debug\ioReadEqn.obj .\Debug\ioReadPla.obj .\Debug\ioReadVerilog.obj .\Debug\ioUtil.obj .\Debug\ioWriteBench.obj .\Debug\ioWriteBlif.obj .\Debug\ioWriteCnf.obj +.\Debug\ioWriteDot.obj +.\Debug\ioWriteEqn.obj +.\Debug\ioWriteGml.obj .\Debug\ioWritePla.obj .\Debug\main.obj .\Debug\mainFrame.obj @@ -290,17 +574,305 @@ kernel32.lib user32.lib gdi32.lib winspool.lib comdlg32.lib advapi32.lib shell32 .\Debug\safe_mem.obj .\Debug\strsav.obj .\Debug\texpand.obj -.\Debug\ioWriteGml.obj -.\Debug\ioWriteEqn.obj -.\Debug\ioWriteDot.obj -.\Debug\ioReadEqn.obj ] -Creating command line "link.exe @C:\DOCUME~1\alanmi\LOCALS~1\Temp\RSP3590.tmp" +Creating command line "link.exe @C:\DOCUME~1\alanmi\LOCALS~1\Temp\RSP37EB.tmp" <h3>Output Window</h3> Compiling... abc.c +abcAig.c +abcAttach.c +abcBalance.c +abcCheck.c +abcCollapse.c +abcCreate.c +abcCut.c +abcDfs.c +abcDsd.c +abcFanio.c +abcFpga.c +abcFraig.c +abcFunc.c +abcFxu.c +abcLatch.c +abcMap.c +abcMinBase.c +abcMiter.c +abcNames.c +abcNetlist.c +abcNtbdd.c +abcPrint.c +abcReconv.c +abcRefactor.c +abcRefs.c +abcRenode.c +abcRewrite.c +abcSat.c +abcSeq.c +abcSeqRetime.c +abcShow.c +abcSop.c +abcStrash.c +abcSweep.c +abcSymm.c +abcTiming.c +abcUnreach.c +abcUtil.c +abcVerify.c +cmd.c +cmdAlias.c +cmdApi.c +cmdFlag.c +cmdHist.c +cmdUtils.c +io.c +ioRead.c +ioReadBench.c +ioReadBlif.c +ioReadEdif.c +ioReadEqn.c +ioReadPla.c +ioReadVerilog.c +ioUtil.c +ioWriteBench.c +ioWriteBlif.c +ioWriteCnf.c +ioWriteDot.c +ioWriteEqn.c +ioWriteGml.c +ioWritePla.c +main.c +mainFrame.c +mainInit.c +mainUtils.c +cuddAddAbs.c +cuddAddApply.c +cuddAddFind.c +cuddAddInv.c +cuddAddIte.c +cuddAddNeg.c +cuddAddWalsh.c +cuddAndAbs.c +cuddAnneal.c +cuddApa.c +C:\_projects\abc\src\bdd\cudd\cuddApa.c(181) : warning C4244: 'return' : conversion from 'unsigned long ' to 'unsigned short ', possible loss of data +C:\_projects\abc\src\bdd\cudd\cuddApa.c(213) : warning C4244: 'return' : conversion from 'unsigned long ' to 'unsigned short ', possible loss of data +C:\_projects\abc\src\bdd\cudd\cuddApa.c(530) : warning C4244: '=' : conversion from 'unsigned short ' to 'unsigned char ', possible loss of data +C:\_projects\abc\src\bdd\cudd\cuddApa.c(588) : warning C4244: '=' : conversion from 'unsigned short ' to 'unsigned char ', possible loss of data +cuddAPI.c +cuddApprox.c +cuddBddAbs.c +cuddBddCorr.c +cuddBddIte.c +cuddBridge.c +cuddCache.c +C:\_projects\abc\src\bdd\cudd\cuddCache.c(902) : warning C4146: unary minus operator applied to unsigned type, result still unsigned +cuddCheck.c +cuddClip.c +cuddCof.c +cuddCompose.c +cuddDecomp.c +cuddEssent.c +cuddExact.c +cuddExport.c +cuddGenCof.c +cuddGenetic.c +cuddGroup.c +C:\_projects\abc\src\bdd\cudd\cuddGroup.c(2062) : warning C4018: '<=' : signed/unsigned mismatch +cuddHarwell.c +cuddInit.c +cuddInteract.c +cuddLCache.c +c:\_projects\abc\src\bdd\cudd\cuddlcache.c(1387) : warning C4146: unary minus operator applied to unsigned type, result still unsigned +cuddLevelQ.c +cuddLinear.c +cuddLiteral.c +cuddMatMult.c +cuddPriority.c +cuddRead.c +cuddRef.c +cuddReorder.c +C:\_projects\abc\src\bdd\cudd\cuddReorder.c(395) : warning C4146: unary minus operator applied to unsigned type, result still unsigned +cuddSat.c +cuddSign.c +cuddSolve.c +cuddSplit.c +cuddSubsetHB.c +cuddSubsetSP.c +cuddSymmetry.c +cuddTable.c +C:\_projects\abc\src\bdd\cudd\cuddTable.c(1822) : warning C4018: '<' : signed/unsigned mismatch +C:\_projects\abc\src\bdd\cudd\cuddTable.c(1927) : warning C4018: '<' : signed/unsigned mismatch +C:\_projects\abc\src\bdd\cudd\cuddTable.c(2235) : warning C4018: '<' : signed/unsigned mismatch +C:\_projects\abc\src\bdd\cudd\cuddTable.c(2303) : warning C4018: '<' : signed/unsigned mismatch +C:\_projects\abc\src\bdd\cudd\cuddTable.c(2358) : warning C4146: unary minus operator applied to unsigned type, result still unsigned +cuddUtil.c +cuddWindow.c +cuddZddCount.c +cuddZddFuncs.c +cuddZddGroup.c +cuddZddIsop.c +cuddZddLin.c +cuddZddMisc.c +cuddZddPort.c +cuddZddReord.c +cuddZddSetop.c +cuddZddSymm.c +cuddZddUtil.c +epd.c +mtrBasic.c +mtrGroup.c +parseCore.c +parseStack.c +dsdApi.c +dsdCheck.c +dsdLocal.c +dsdMan.c +dsdProc.c +dsdTree.c +reoApi.c +reoCore.c +reoProfile.c +reoSift.c +reoSwap.c +reoTest.c +reoTransfer.c +reoUnits.c +mvc.c +mvcApi.c +mvcCompare.c +mvcContain.c +mvcCover.c +mvcCube.c +mvcDivide.c +mvcDivisor.c +mvcList.c +mvcLits.c +mvcMan.c +mvcOpAlg.c +mvcOpBool.c +mvcPrint.c +mvcSort.c +mvcUtils.c +ftFactor.c +ftPrint.c +added.c +solver.c +msatActivity.c +msatClause.c +msatClauseVec.c +msatMem.c +msatOrderJ.c +msatQueue.c +msatRead.c +msatSolverApi.c +msatSolverCore.c +msatSolverIo.c +msatSolverSearch.c +msatSort.c +msatVec.c +fraigApi.c +fraigCanon.c +fraigFanout.c +fraigFeed.c +fraigMan.c +fraigMem.c +fraigNode.c +fraigPrime.c +fraigSat.c +fraigTable.c +fraigUtil.c +fraigVec.c +simMan.c +simSat.c +simSupp.c +simSym.c +simUnate.c +simUtils.c +csat_apis.c +fxu.c +fxuCreate.c +fxuHeapD.c +fxuHeapS.c +fxuList.c +fxuMatrix.c +fxuPair.c +fxuPrint.c +fxuReduce.c +fxuSelect.c +fxuSingle.c +fxuUpdate.c +rwrDec.c +rwrEva.c +rwrExp.c +rwrLib.c +rwrMan.c +rwrPrint.c +rwrUtil.c +cutMan.c +cutMerge.c +cutNode.c +cutSeq.c +cutTable.c +cutTruth.c +fpga.c +fpgaCore.c +fpgaCreate.c +fpgaCut.c +fpgaCutUtils.c +fpgaFanout.c +fpgaLib.c +fpgaMatch.c +fpgaTime.c +fpgaTruth.c +fpgaUtils.c +fpgaVec.c +mapper.c +mapperCanon.c +mapperCore.c +mapperCreate.c +mapperCut.c +mapperCutUtils.c +mapperFanout.c +mapperLib.c +mapperMatch.c +mapperRefs.c +mapperSuper.c +mapperTable.c +mapperTime.c +mapperTree.c +mapperTruth.c +mapperUtils.c +mapperVec.c +mio.c +mioApi.c +mioFunc.c +mioRead.c +mioUtils.c +super.c +superAnd.c +superGate.c +superWrite.c +extraBddMisc.c +extraBddSymm.c +extraUtilBitMatrix.c +extraUtilCanon.c +extraUtilFile.c +extraUtilMemory.c +extraUtilMisc.c +extraUtilProgress.c +extraUtilReader.c +st.c +stmm.c +cpu_stats.c +cpu_time.c +datalimit.c +getopt.c +pathsearch.c +safe_mem.c +strsav.c +texpand.c Linking... -Creating temporary file "C:\DOCUME~1\alanmi\LOCALS~1\Temp\RSP3591.tmp" with contents +Creating temporary file "C:\DOCUME~1\alanmi\LOCALS~1\Temp\RSP37ED.tmp" with contents [ /nologo /o"Debug/abc.bsc" .\Debug\abc.sbr @@ -324,6 +896,7 @@ Creating temporary file "C:\DOCUME~1\alanmi\LOCALS~1\Temp\RSP3591.tmp" with cont .\Debug\abcMiter.sbr .\Debug\abcNames.sbr .\Debug\abcNetlist.sbr +.\Debug\abcNtbdd.sbr .\Debug\abcPrint.sbr .\Debug\abcReconv.sbr .\Debug\abcRefactor.sbr @@ -353,12 +926,16 @@ Creating temporary file "C:\DOCUME~1\alanmi\LOCALS~1\Temp\RSP3591.tmp" with cont .\Debug\ioReadBench.sbr .\Debug\ioReadBlif.sbr .\Debug\ioReadEdif.sbr +.\Debug\ioReadEqn.sbr .\Debug\ioReadPla.sbr .\Debug\ioReadVerilog.sbr .\Debug\ioUtil.sbr .\Debug\ioWriteBench.sbr .\Debug\ioWriteBlif.sbr .\Debug\ioWriteCnf.sbr +.\Debug\ioWriteDot.sbr +.\Debug\ioWriteEqn.sbr +.\Debug\ioWriteGml.sbr .\Debug\ioWritePla.sbr .\Debug\main.sbr .\Debug\mainFrame.sbr @@ -577,19 +1154,15 @@ Creating temporary file "C:\DOCUME~1\alanmi\LOCALS~1\Temp\RSP3591.tmp" with cont .\Debug\pathsearch.sbr .\Debug\safe_mem.sbr .\Debug\strsav.sbr -.\Debug\texpand.sbr -.\Debug\ioWriteGml.sbr -.\Debug\ioWriteEqn.sbr -.\Debug\ioWriteDot.sbr -.\Debug\ioReadEqn.sbr] -Creating command line "bscmake.exe @C:\DOCUME~1\alanmi\LOCALS~1\Temp\RSP3591.tmp" +.\Debug\texpand.sbr] +Creating command line "bscmake.exe @C:\DOCUME~1\alanmi\LOCALS~1\Temp\RSP37ED.tmp" Creating browse info file... <h3>Output Window</h3> <h3>Results</h3> -abc.exe - 0 error(s), 0 warning(s) +abc.exe - 0 error(s), 13 warning(s) </pre> </body> </html> @@ -1,4 +1,5 @@ alias b balance +alias cl cleanup alias clp collapse alias esd ext_seq_dcs alias f fraig @@ -14,6 +15,7 @@ alias psu print_supp alias psy print_symm alias q quit alias r read +alias ren renode alias rl read_blif alias rb read_bench alias rp read_pla @@ -27,13 +29,16 @@ alias rfz refactor -z alias sa set autoexec ps alias so source -x alias st strash +alias sw sweep alias u undo alias wb write_blif alias wl write_blif alias wp write_pla -alias cnf "st; renode -c; write_cnf" -alias prove "st; renode -c; sat" -alias opt "b; renode; b" -alias share "b; renode -m; fx; b" -alias resyn "b; rw; rf; b; rw; rwz; b; rfz; rwz; b" +alias cnf "st; renode -c; write_cnf" +alias prove "st; renode -c; sat" +alias opt "b; renode; b" +alias share "b; renode; fx; b" +alias sharem "b; renode -m; fx; b" +alias sharedsd "b; renode; dsd -g; sw; fx; b" +alias resyn "b; rw; rf; b; rw; rwz; b; rfz; rwz; b" diff --git a/src/base/abc/abc.c b/src/base/abc/abc.c index 0d911e79..97e5663f 100644 --- a/src/base/abc/abc.c +++ b/src/base/abc/abc.c @@ -47,6 +47,7 @@ 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_CommandSweep ( 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 ); @@ -58,11 +59,13 @@ 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_CommandMuxes ( 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_CommandSplit ( Abc_Frame_t * pAbc, int argc, char ** argv ); +static int Abc_CommandOneOutput ( Abc_Frame_t * pAbc, int argc, char ** argv ); +static int Abc_CommandOneNode ( Abc_Frame_t * pAbc, int argc, char ** argv ); static int Abc_CommandShortNames ( Abc_Frame_t * pAbc, int argc, char ** argv ); -static int Abc_CommandCut ( Abc_Frame_t * pAbc, int argc, char ** argv ); +static int Abc_CommandCut ( 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 ); @@ -119,6 +122,7 @@ void Abc_Init( Abc_Frame_t * pAbc ) 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", "sweep", Abc_CommandSweep, 1 ); Cmd_CommandAdd( pAbc, "Synthesis", "fx", Abc_CommandFastExtract, 1 ); Cmd_CommandAdd( pAbc, "Synthesis", "dsd", Abc_CommandDisjoint, 1 ); @@ -130,9 +134,11 @@ void Abc_Init( Abc_Frame_t * pAbc ) 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", "muxes", Abc_CommandMuxes, 1 ); Cmd_CommandAdd( pAbc, "Various", "sat", Abc_CommandSat, 0 ); Cmd_CommandAdd( pAbc, "Various", "ext_seq_dcs", Abc_CommandExtSeqDcs, 0 ); - Cmd_CommandAdd( pAbc, "Various", "split", Abc_CommandSplit, 1 ); + Cmd_CommandAdd( pAbc, "Various", "one_output", Abc_CommandOneOutput, 1 ); + Cmd_CommandAdd( pAbc, "Various", "one_node", Abc_CommandOneNode, 1 ); Cmd_CommandAdd( pAbc, "Various", "short_names", Abc_CommandShortNames, 0 ); Cmd_CommandAdd( pAbc, "Various", "cut", Abc_CommandCut, 0 ); @@ -428,17 +434,22 @@ int Abc_CommandPrintFactor( Abc_Frame_t * pAbc, int argc, char ** argv ) Abc_Ntk_t * pNtk; Abc_Obj_t * pNode; int c; + int fUseRealNames; pNtk = Abc_FrameReadNet(pAbc); pOut = Abc_FrameReadOut(pAbc); pErr = Abc_FrameReadErr(pAbc); // set defaults + fUseRealNames = 1; util_getopt_reset(); - while ( ( c = util_getopt( argc, argv, "h" ) ) != EOF ) + while ( ( c = util_getopt( argc, argv, "nh" ) ) != EOF ) { switch ( c ) { + case 'n': + fUseRealNames ^= 1; + break; case 'h': goto usage; default: @@ -472,18 +483,19 @@ int Abc_CommandPrintFactor( Abc_Frame_t * pAbc, int argc, char ** argv ) fprintf( pErr, "Cannot find node \"%s\".\n", argv[util_optind] ); return 1; } - Abc_NodePrintFactor( pOut, pNode ); + Abc_NodePrintFactor( pOut, pNode, fUseRealNames ); return 0; } // print the nodes - Abc_NtkPrintFactor( pOut, pNtk ); + Abc_NtkPrintFactor( pOut, pNtk, fUseRealNames ); return 0; usage: - fprintf( pErr, "usage: print_factor [-h] <node>\n" ); + fprintf( pErr, "usage: print_factor [-nh] <node>\n" ); fprintf( pErr, "\t prints the factored forms of nodes\n" ); - fprintf( pErr, "\tnode : (optional) one node to consider\n"); + fprintf( pErr, "\t-n : toggles real/dummy fanin names [default = %s]\n", fUseRealNames? "real": "dummy" ); fprintf( pErr, "\t-h : print the command usage\n"); + fprintf( pErr, "\tnode : (optional) one node to consider\n"); return 1; } @@ -1182,7 +1194,7 @@ int Abc_CommandRenode( Abc_Frame_t * pAbc, int argc, char ** argv ) pErr = Abc_FrameReadErr(pAbc); // set defaults - nThresh = 0; + nThresh = 1; nFaninMax = 20; fCnf = 0; fMulti = 0; @@ -1255,11 +1267,14 @@ int Abc_CommandRenode( Abc_Frame_t * pAbc, int argc, char ** argv ) usage: fprintf( pErr, "usage: renode [-T num] [-F num] [-cmsh]\n" ); fprintf( pErr, "\t transforms an AIG into a logic network by creating larger nodes\n" ); - fprintf( pErr, "\t-T num : the threshold for AIG node duplication [default = %d]\n", nThresh ); fprintf( pErr, "\t-F num : the maximum fanin size after renoding [default = %d]\n", nFaninMax ); - fprintf( pErr, "\t-c : performs renoding to derive the CNF [default = %s]\n", fCnf? "yes": "no" ); + fprintf( pErr, "\t-T num : the threshold for AIG node duplication [default = %d]\n", nThresh ); + fprintf( pErr, "\t (an AIG node is the root of a new node after renoding\n" ); + fprintf( pErr, "\t if doing so prevents duplication of more than %d AIG nodes,\n", nThresh ); + fprintf( pErr, "\t that is, if [(numFanouts(Node)-1) * size(MFFC(Node))] > %d)\n", nThresh ); fprintf( pErr, "\t-m : creates multi-input AND graph [default = %s]\n", fMulti? "yes": "no" ); fprintf( pErr, "\t-s : creates a simple AIG (no renoding) [default = %s]\n", fSimple? "yes": "no" ); + fprintf( pErr, "\t-c : performs renoding to derive the CNF [default = %s]\n", fCnf? "yes": "no" ); fprintf( pErr, "\t-h : print the command usage\n"); return 1; } @@ -1280,22 +1295,17 @@ int Abc_CommandCleanup( Abc_Frame_t * pAbc, int argc, char ** argv ) FILE * pOut, * pErr; Abc_Ntk_t * pNtk; int c; - int fDuplicate; pNtk = Abc_FrameReadNet(pAbc); pOut = Abc_FrameReadOut(pAbc); pErr = Abc_FrameReadErr(pAbc); // set defaults - fDuplicate = 0; util_getopt_reset(); - while ( ( c = util_getopt( argc, argv, "dh" ) ) != EOF ) + while ( ( c = util_getopt( argc, argv, "h" ) ) != EOF ) { switch ( c ) { - case 'd': - fDuplicate ^= 1; - break; case 'h': goto usage; default: @@ -1313,7 +1323,6 @@ int Abc_CommandCleanup( Abc_Frame_t * pAbc, int argc, char ** argv ) fprintf( pErr, "Cleanup cannot be performed on the AIG.\n" ); return 1; } - // modify the current network Abc_NtkCleanup( pNtk, 0 ); return 0; @@ -1321,7 +1330,61 @@ int Abc_CommandCleanup( Abc_Frame_t * pAbc, int argc, char ** argv ) usage: fprintf( pErr, "usage: cleanup [-h]\n" ); fprintf( pErr, "\t removes dangling nodes\n" ); -// fprintf( pErr, "\t-d : toggle duplication of logic [default = %s]\n", fDuplicate? "yes": "no" ); + fprintf( pErr, "\t-h : print the command usage\n"); + return 1; +} + +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Abc_CommandSweep( Abc_Frame_t * pAbc, int argc, char ** argv ) +{ + FILE * pOut, * pErr; + Abc_Ntk_t * pNtk; + int c; + + 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_NtkIsSopLogic(pNtk) && !Abc_NtkIsBddLogic(pNtk) ) + { + fprintf( pErr, "Sweep cannot be performed on an AIG or a mapped network (unmap it first).\n" ); + return 1; + } + // modify the current network + Abc_NtkSweep( pNtk, 0 ); + return 0; + +usage: + fprintf( pErr, "usage: sweep [-h]\n" ); + fprintf( pErr, "\t removes dangling nodes; propagates constant, buffers, inverters\n" ); fprintf( pErr, "\t-h : print the command usage\n"); return 1; } @@ -1426,6 +1489,14 @@ int Abc_CommandFastExtract( Abc_Frame_t * pAbc, int argc, char ** argv ) return 1; } + if ( !Abc_NtkIsLogic(pNtk) ) + { + fprintf( pErr, "Fast extract can only be applied to a logic network.\n" ); + Abc_NtkFxuFreeInfo( p ); + return 1; + } + + // the nodes to be merged are linked into the special linked list Abc_NtkFastExtract( pNtk, p ); Abc_NtkFxuFreeInfo( p ); @@ -1464,7 +1535,7 @@ int Abc_CommandDisjoint( Abc_Frame_t * pAbc, int argc, char ** argv ) 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 ); + extern int Abc_NtkDsdLocal( Abc_Ntk_t * pNtk, bool fVerbose, bool fRecursive ); pNtk = Abc_FrameReadNet(pAbc); pOut = Abc_FrameReadOut(pAbc); @@ -1510,14 +1581,9 @@ int Abc_CommandDisjoint( Abc_Frame_t * pAbc, int argc, char ** argv ) return 1; } - if ( !fGlobal && !fRecursive ) - { - fprintf( pErr, "Decomposition should be either global or recursive.\n" ); - return 1; - } - if ( fGlobal ) { +// fprintf( stdout, "Performing DSD of global functions of the network.\n" ); // get the new network if ( !Abc_NtkIsStrash(pNtk) ) { @@ -1531,18 +1597,9 @@ int Abc_CommandDisjoint( Abc_Frame_t * pAbc, int argc, char ** argv ) } if ( pNtkRes == NULL ) { - fprintf( pErr, "Global disjoint support decomposition has failed.\n" ); + fprintf( pErr, "Global DSD 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 ); } @@ -1553,16 +1610,28 @@ int Abc_CommandDisjoint( Abc_Frame_t * pAbc, int argc, char ** argv ) 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" ); + fprintf( stdout, "Performing recursive DSD and MUX decomposition of local functions.\n" ); + if ( !Abc_NtkDsdLocal( pNtk, fVerbose, fRecursive ) ) + fprintf( pErr, "Recursive DSD has failed.\n" ); + } + else + { + if ( !Abc_NtkIsBddLogic( pNtk ) ) + { + fprintf( pErr, "This command is only applicable to logic BDD networks.\n" ); + return 1; + } + fprintf( stdout, "Performing simple non-recursive DSD of local functions.\n" ); + if ( !Abc_NtkDsdLocal( pNtk, fVerbose, fRecursive ) ) + fprintf( pErr, "Simple DSD of local functions 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-g : toggle DSD of global and local functions [default = %s]\n", fGlobal? "global": "local" ); + fprintf( pErr, "\t-r : toggle recursive DSD/MUX and simple DSD [default = %s]\n", fRecursive? "recursive DSD/MUX": "simple DSD" ); 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" ); @@ -2135,6 +2204,71 @@ usage: SeeAlso [] ***********************************************************************/ +int Abc_CommandMuxes( Abc_Frame_t * pAbc, int argc, char ** argv ) +{ + FILE * pOut, * pErr; + Abc_Ntk_t * pNtk, * pNtkRes; + int c; + + 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_NtkIsBddLogic(pNtk) ) + { + fprintf( pErr, "Only a BDD logic network can be converted to MUXes.\n" ); + return 1; + } + + // get the new network + pNtkRes = Abc_NtkBddToMuxes( pNtk ); + if ( pNtkRes == NULL ) + { + fprintf( pErr, "Converting to MUXes has failed.\n" ); + return 1; + } + // replace the current network + Abc_FrameReplaceCurrentNetwork( pAbc, pNtkRes ); + return 0; + +usage: + fprintf( pErr, "usage: muxes [-h]\n" ); + fprintf( pErr, "\t converts the current network by a network derived by\n" ); + fprintf( pErr, "\t replacing all nodes by DAGs isomorphic to the local BDDs\n" ); + fprintf( pErr, "\t-h : print the command usage\n"); + return 1; +} + +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ int Abc_CommandSat( Abc_Frame_t * pAbc, int argc, char ** argv ) { FILE * pOut, * pErr; @@ -2279,7 +2413,7 @@ usage: SeeAlso [] ***********************************************************************/ -int Abc_CommandSplit( Abc_Frame_t * pAbc, int argc, char ** argv ) +int Abc_CommandOneOutput( Abc_Frame_t * pAbc, int argc, char ** argv ) { FILE * pOut, * pErr; Abc_Ntk_t * pNtk, * pNtkRes; @@ -2373,7 +2507,7 @@ int Abc_CommandSplit( Abc_Frame_t * pAbc, int argc, char ** argv ) return 0; usage: - fprintf( pErr, "usage: split [-O num] [-ah] <name>\n" ); + fprintf( pErr, "usage: one_output [-O num] [-ah] <name>\n" ); fprintf( pErr, "\t replaces the current network by the logic cone of one output\n" ); fprintf( pErr, "\t-a : toggle writing all CIs or structral support only [default = %s]\n", fUseAllCis? "all": "structural" ); fprintf( pErr, "\t-h : print the command usage\n"); @@ -2382,6 +2516,86 @@ usage: return 1; } +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Abc_CommandOneNode( Abc_Frame_t * pAbc, int argc, char ** argv ) +{ + FILE * pOut, * pErr; + Abc_Ntk_t * pNtk, * pNtkRes; + Abc_Obj_t * pNode; + int c; + + 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_NtkIsLogic(pNtk) ) + { + fprintf( pErr, "Currently can only be applied to a logic network.\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; + } + + pNtkRes = Abc_NtkSplitNode( pNtk, pNode ); +// pNtkRes = Abc_NtkDeriveFromBdd( pNtk->pManFunc, pNode->pData, NULL, NULL ); + if ( pNtkRes == NULL ) + { + fprintf( pErr, "Splitting one node has failed.\n" ); + return 1; + } + // replace the current network + Abc_FrameReplaceCurrentNetwork( pAbc, pNtkRes ); + return 0; + +usage: + fprintf( pErr, "usage: one_node [-h] <name>\n" ); + fprintf( pErr, "\t replaces the current network by the network composed of one node\n" ); + fprintf( pErr, "\t-h : print the command usage\n"); + fprintf( pErr, "\tname : the node name\n"); + return 1; +} + + /**Function************************************************************* diff --git a/src/base/abc/abc.h b/src/base/abc/abc.h index ab457cc9..c779230a 100644 --- a/src/base/abc/abc.h +++ b/src/base/abc/abc.h @@ -415,8 +415,6 @@ extern bool Abc_NtkCheckObj( Abc_Ntk_t * pNtk, Abc_Obj_t * pObj ); 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( Abc_Ntk_t * pNtk ); /*=== abcCreate.c ==========================================================*/ extern Abc_Ntk_t * Abc_NtkAlloc( Abc_NtkType_t Type, Abc_NtkFunc_t Func ); extern Abc_Ntk_t * Abc_NtkStartFrom( Abc_Ntk_t * pNtk, Abc_NtkType_t Type, Abc_NtkFunc_t Func ); @@ -427,6 +425,7 @@ extern void Abc_NtkFinalizeRead( Abc_Ntk_t * pNtk ); extern Abc_Ntk_t * Abc_NtkDup( Abc_Ntk_t * pNtk ); extern Abc_Ntk_t * Abc_NtkSplitOutput( Abc_Ntk_t * pNtk, Abc_Obj_t * pNode, int fUseAllCis ); extern Abc_Ntk_t * Abc_NtkCreateCone( Abc_Ntk_t * pNtk, Vec_Ptr_t * vRoots, Vec_Int_t * vValues ); +extern Abc_Ntk_t * Abc_NtkSplitNode( Abc_Ntk_t * pNtk, Abc_Obj_t * pNode ); extern void Abc_NtkDelete( Abc_Ntk_t * pNtk ); extern void Abc_NtkFixNonDrivenNets( Abc_Ntk_t * pNtk ); extern Abc_Obj_t * Abc_NtkDupObj( Abc_Ntk_t * pNtkNew, Abc_Obj_t * pObj ); @@ -491,6 +490,8 @@ extern int Abc_NtkUnmap( Abc_Ntk_t * pNtk ); /*=== abcMiter.c ==========================================================*/ extern int Abc_NtkMinimumBase( Abc_Ntk_t * pNtk ); extern int Abc_NodeMinimumBase( Abc_Obj_t * pNode ); +extern int Abc_NtkRemoveDupFanins( Abc_Ntk_t * pNtk ); +extern int Abc_NodeRemoveDupFanins( Abc_Obj_t * pNode ); /*=== abcMiter.c ==========================================================*/ extern Abc_Ntk_t * Abc_NtkMiter( Abc_Ntk_t * pNtk1, Abc_Ntk_t * pNtk2, int fComb ); extern Abc_Ntk_t * Abc_NtkMiterOne( Abc_Ntk_t * pNtk, int Out, int In1, int In2 ); @@ -515,14 +516,19 @@ extern Abc_Ntk_t * Abc_NtkLogicToNetlistBench( Abc_Ntk_t * pNtk ); extern Abc_Ntk_t * Abc_NtkLogicSopToNetlist( Abc_Ntk_t * pNtk ); extern Abc_Ntk_t * Abc_NtkAigToLogicSop( Abc_Ntk_t * pNtk ); extern Abc_Ntk_t * Abc_NtkAigToLogicSopBench( Abc_Ntk_t * pNtk ); +/*=== abcNtbdd.c ==========================================================*/ +extern Abc_Ntk_t * Abc_NtkDeriveFromBdd( DdManager * dd, DdNode * bFunc, char * pNamePo, Vec_Ptr_t * vNamesPi ); +extern Abc_Ntk_t * Abc_NtkBddToMuxes( Abc_Ntk_t * pNtk ); +extern DdManager * Abc_NtkGlobalBdds( Abc_Ntk_t * pNtk, int fLatchOnly ); +extern void Abc_NtkFreeGlobalBdds( Abc_Ntk_t * pNtk ); /*=== abcPrint.c ==========================================================*/ extern void Abc_NtkPrintStats( FILE * pFile, Abc_Ntk_t * pNtk, int fFactored ); extern void Abc_NtkPrintIo( FILE * pFile, Abc_Ntk_t * pNtk ); extern void Abc_NtkPrintLatch( FILE * pFile, Abc_Ntk_t * pNtk ); extern void Abc_NtkPrintFanio( FILE * pFile, Abc_Ntk_t * pNtk ); extern void Abc_NodePrintFanio( FILE * pFile, Abc_Obj_t * pNode ); -extern void Abc_NtkPrintFactor( FILE * pFile, Abc_Ntk_t * pNtk ); -extern void Abc_NodePrintFactor( FILE * pFile, Abc_Obj_t * pNode ); +extern void Abc_NtkPrintFactor( FILE * pFile, Abc_Ntk_t * pNtk, int fUseRealNames ); +extern void Abc_NodePrintFactor( FILE * pFile, Abc_Obj_t * pNode, int fUseRealNames ); extern void Abc_NtkPrintLevel( FILE * pFile, Abc_Ntk_t * pNtk, int fProfile ); extern void Abc_NodePrintLevel( FILE * pFile, Abc_Obj_t * pNode ); /*=== abcReconv.c ==========================================================*/ @@ -537,6 +543,7 @@ extern DdNode * Abc_NodeConeDcs( DdManager * dd, DdNode ** pbVarsX, Dd extern Vec_Ptr_t * Abc_NodeCollectTfoCands( Abc_ManCut_t * p, Abc_Obj_t * pRoot, Vec_Ptr_t * vFanins, int LevelMax ); /*=== abcRefs.c ==========================================================*/ extern int Abc_NodeMffcSize( Abc_Obj_t * pNode ); +extern int Abc_NodeMffcSizeStop( Abc_Obj_t * pNode ); extern int Abc_NodeMffcLabel( Abc_Obj_t * pNode ); extern Vec_Ptr_t * Abc_NodeMffcCollect( Abc_Obj_t * pNode ); extern void Abc_NodeUpdate( Abc_Obj_t * pNode, Vec_Ptr_t * vFanins, Vec_Int_t * vForm, int nGain ); @@ -593,6 +600,7 @@ extern int Abc_NtkAppend( Abc_Ntk_t * pNtk1, Abc_Ntk_t * pNtk2 ); /*=== abcSweep.c ==========================================================*/ extern bool Abc_NtkFraigSweep( Abc_Ntk_t * pNtk, int fUseInv, int fVerbose ); extern int Abc_NtkCleanup( Abc_Ntk_t * pNtk, int fVerbose ); +extern int Abc_NtkSweep( Abc_Ntk_t * pNtk, int fVerbose ); /*=== abcTiming.c ==========================================================*/ extern Abc_Time_t * Abc_NodeReadArrival( Abc_Obj_t * pNode ); extern Abc_Time_t * Abc_NodeReadRequired( Abc_Obj_t * pNode ); @@ -646,7 +654,8 @@ 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_NodeGetFaninNames( Abc_Obj_t * pNode ); -extern void Abc_NodeFreeFaninNames( Vec_Ptr_t * vNames ); +extern Vec_Ptr_t * Abc_NodeGetFakeNames( int nNames ); +extern void Abc_NodeFreeNames( Vec_Ptr_t * vNames ); extern char ** Abc_NtkCollectCioNames( Abc_Ntk_t * pNtk, int fCollectCos ); extern void Abc_NtkAlphaOrderSignals( Abc_Ntk_t * pNtk, int fComb ); extern void Abc_NtkShortNames( Abc_Ntk_t * pNtk ); diff --git a/src/base/abc/abcCheck.c b/src/base/abc/abcCheck.c index 25d1c86c..9b9e9ee2 100644 --- a/src/base/abc/abcCheck.c +++ b/src/base/abc/abcCheck.c @@ -367,7 +367,7 @@ bool Abc_NtkCheckObj( Abc_Ntk_t * pNtk, Abc_Obj_t * pObj ) { Abc_Obj_t * pFanin, * pFanout; int i, Value = 1; -// int k; + int k; // check the network if ( pObj->pNtk != pNtk ) @@ -401,7 +401,7 @@ bool Abc_NtkCheckObj( Abc_Ntk_t * pNtk, Abc_Obj_t * pObj ) Value = 0; } } -/* + // make sure fanins are not duplicated for ( i = 0; i < pObj->vFanins.nSize; i++ ) for ( k = i + 1; k < pObj->vFanins.nSize; k++ ) @@ -423,7 +423,7 @@ bool Abc_NtkCheckObj( Abc_Ntk_t * pNtk, Abc_Obj_t * pObj ) printf( "Warning: Node %s has", Abc_ObjName(pObj) ); printf( " duplicated fanout %s.\n", Abc_ObjName(Abc_ObjFanout(pObj,k)) ); } -*/ + return Value; } diff --git a/src/base/abc/abcCollapse.c b/src/base/abc/abcCollapse.c index a6eda7b3..4e359506 100644 --- a/src/base/abc/abcCollapse.c +++ b/src/base/abc/abcCollapse.c @@ -24,7 +24,6 @@ /// DECLARATIONS /// //////////////////////////////////////////////////////////////////////// -static DdNode * Abc_NtkGlobalBdds_rec( DdManager * dd, Abc_Obj_t * pNode ); static Abc_Ntk_t * Abc_NtkFromGlobalBdds( Abc_Ntk_t * pNtk ); static Abc_Obj_t * Abc_NodeFromGlobalBdds( Abc_Ntk_t * pNtkNew, DdManager * dd, DdNode * bFunc ); @@ -83,142 +82,6 @@ Abc_Ntk_t * Abc_NtkCollapse( Abc_Ntk_t * pNtk, int fVerbose ) /**Function************************************************************* - Synopsis [Derives global BDDs for the node function.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -DdManager * Abc_NtkGlobalBdds( Abc_Ntk_t * pNtk, int fLatchOnly ) -{ - int fReorder = 1; - ProgressBar * pProgress; - Vec_Ptr_t * vFuncsGlob; - Abc_Obj_t * pNode; - DdNode * bFunc; - DdManager * dd; - int i; - - // start the manager - assert( pNtk->pManGlob == NULL ); - dd = Cudd_Init( Abc_NtkCiNum(pNtk), 0, CUDD_UNIQUE_SLOTS, CUDD_CACHE_SLOTS, 0 ); - if ( fReorder ) - Cudd_AutodynEnable( dd, CUDD_REORDER_SYMM_SIFT ); - - // set the elementary variables - Abc_NtkCleanCopy( pNtk ); - Abc_NtkForEachCi( pNtk, pNode, i ) - pNode->pCopy = (Abc_Obj_t *)dd->vars[i]; - // assign the constant node BDD - pNode = Abc_AigConst1( pNtk->pManFunc ); - pNode->pCopy = (Abc_Obj_t *)dd->one; Cudd_Ref( dd->one ); - - vFuncsGlob = Vec_PtrAlloc( 100 ); - if ( fLatchOnly ) - { - // construct the BDDs - pProgress = Extra_ProgressBarStart( stdout, Abc_NtkLatchNum(pNtk) ); - Abc_NtkForEachLatch( 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) ); Cudd_Ref( bFunc ); - Vec_PtrPush( vFuncsGlob, 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) ); Cudd_Ref( bFunc ); - Vec_PtrPush( vFuncsGlob, bFunc ); - } - Extra_ProgressBarStop( pProgress ); - } - - // derefence the intermediate BDDs - Abc_NtkForEachNode( pNtk, pNode, i ) - if ( pNode->pCopy ) - { - Cudd_RecursiveDeref( dd, (DdNode *)pNode->pCopy ); - pNode->pCopy = NULL; - } - // reorder one more time - if ( fReorder ) - { - Cudd_ReduceHeap( dd, CUDD_REORDER_SYMM_SIFT, 1 ); - Cudd_AutodynDisable( dd ); - } - pNtk->pManGlob = dd; - pNtk->vFuncsGlob = vFuncsGlob; - return dd; -} - -/**Function************************************************************* - - Synopsis [Derives the global BDD of the node.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -DdNode * Abc_NtkGlobalBdds_rec( DdManager * dd, Abc_Obj_t * pNode ) -{ - DdNode * bFunc, * bFunc0, * bFunc1; - assert( !Abc_ObjIsComplement(pNode) ); - if ( Cudd_ReadKeys(dd) > 500000 ) - return NULL; - // if the result is available return - if ( pNode->pCopy ) - return (DdNode *)pNode->pCopy; - // compute the result for both branches - bFunc0 = Abc_NtkGlobalBdds_rec( dd, Abc_ObjFanin(pNode,0) ); - if ( bFunc0 == NULL ) - return NULL; - Cudd_Ref( bFunc0 ); - bFunc1 = Abc_NtkGlobalBdds_rec( dd, Abc_ObjFanin(pNode,1) ); - if ( bFunc1 == NULL ) - return NULL; - Cudd_Ref( bFunc1 ); - bFunc0 = Cudd_NotCond( bFunc0, Abc_ObjFaninC0(pNode) ); - bFunc1 = Cudd_NotCond( bFunc1, Abc_ObjFaninC1(pNode) ); - // get the final result - bFunc = Cudd_bddAnd( dd, bFunc0, bFunc1 ); Cudd_Ref( bFunc ); - Cudd_RecursiveDeref( dd, bFunc0 ); - Cudd_RecursiveDeref( dd, bFunc1 ); - // set the result - assert( pNode->pCopy == NULL ); - pNode->pCopy = (Abc_Obj_t *)bFunc; - return bFunc; -} - -/**Function************************************************************* - Synopsis [Derives the network with the given global BDD.] Description [] @@ -276,29 +139,6 @@ 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( Abc_Ntk_t * pNtk ) -{ - DdNode * bFunc; - int i; - assert( pNtk->pManGlob ); - assert( pNtk->vFuncsGlob ); - Vec_PtrForEachEntry( pNtk->vFuncsGlob, bFunc, i ) - Cudd_RecursiveDeref( pNtk->pManGlob, bFunc ); - Vec_PtrFree( pNtk->vFuncsGlob ); - pNtk->vFuncsGlob = NULL; -} - //////////////////////////////////////////////////////////////////////// /// END OF FILE /// diff --git a/src/base/abc/abcCreate.c b/src/base/abc/abcCreate.c index d6500803..16d5ec05 100644 --- a/src/base/abc/abcCreate.c +++ b/src/base/abc/abcCreate.c @@ -406,6 +406,44 @@ Abc_Ntk_t * Abc_NtkCreateCone( Abc_Ntk_t * pNtk, Vec_Ptr_t * vRoots, Vec_Int_t * SeeAlso [] ***********************************************************************/ +Abc_Ntk_t * Abc_NtkSplitNode( Abc_Ntk_t * pNtk, Abc_Obj_t * pNode ) +{ + Abc_Ntk_t * pNtkNew; + Abc_Obj_t * pFanin, * pNodePo; + int i; + // start the network + pNtkNew = Abc_NtkAlloc( pNtk->ntkType, pNtk->ntkFunc ); + pNtkNew->pName = util_strsav(Abc_ObjName(pNode)); + // add the PIs corresponding to the fanins of the node + Abc_ObjForEachFanin( pNode, pFanin, i ) + { + pFanin->pCopy = Abc_NtkCreatePi( pNtkNew ); + Abc_NtkLogicStoreName( pFanin->pCopy, Abc_ObjName(pFanin) ); + } + // duplicate and connect the node + pNode->pCopy = Abc_NtkDupObj( pNtkNew, pNode ); + Abc_ObjForEachFanin( pNode, pFanin, i ) + Abc_ObjAddFanin( pNode->pCopy, pFanin->pCopy ); + // create the only PO + pNodePo = Abc_NtkCreatePo( pNtkNew ); + Abc_ObjAddFanin( pNodePo, pNode->pCopy ); + Abc_NtkLogicStoreName( pNodePo, Abc_ObjName(pNode) ); + if ( !Abc_NtkCheck( pNtkNew ) ) + fprintf( stdout, "Abc_NtkSplitNode(): Network check has failed.\n" ); + return pNtkNew; +} + +/**Function************************************************************* + + Synopsis [Deletes the Ntk.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ void Abc_NtkDelete( Abc_Ntk_t * pNtk ) { Abc_Obj_t * pObj; @@ -758,6 +796,8 @@ void Abc_NtkDeleteObj( Abc_Obj_t * pObj ) } else if ( Abc_ObjIsNode(pObj) ) { + if ( Abc_NtkHasBdd(pNtk) ) + Cudd_RecursiveDeref( pNtk->pManFunc, pObj->pData ); pNtk->nNodes--; } else if ( Abc_ObjIsLatch(pObj) ) diff --git a/src/base/abc/abcDsd.c b/src/base/abc/abcDsd.c index ccb52ffa..013b7ac4 100644 --- a/src/base/abc/abcDsd.c +++ b/src/base/abc/abcDsd.c @@ -30,7 +30,7 @@ static void Abc_NtkDsdConstruct( Dsd_Manager_t * pManDsd, Abc_Ntk_t * 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 void Abc_NodeDecompDsdAndMux( Abc_Obj_t * pNode, Vec_Ptr_t * vNodes, Dsd_Manager_t * pManDsd, bool fRecursive ); static bool Abc_NodeIsForDsd( Abc_Obj_t * pNode ); static int Abc_NodeFindMuxVar( DdManager * dd, DdNode * bFunc, int nVars ); @@ -192,6 +192,8 @@ void Abc_NtkDsdConstruct( Dsd_Manager_t * pManDsd, Abc_Ntk_t * pNtk, Abc_Ntk_t * pDriver = Abc_ObjFanin0( pNode ); if ( !Abc_ObjIsNode(pDriver) ) continue; + if ( !Abc_NodeIsAigAnd(pDriver) ) + continue; pNodeDsd = Dsd_ManagerReadRoot( pManDsd, i ); pNodeNew = (Abc_Obj_t *)Dsd_NodeReadMark( Dsd_Regular(pNodeDsd) ); assert( !Abc_ObjIsComplement(pNodeNew) ); @@ -300,7 +302,7 @@ Abc_Obj_t * Abc_NtkDsdConstructNode( Dsd_Manager_t * pManDsd, Dsd_Node_t * pNode SeeAlso [] ***********************************************************************/ -int Abc_NtkDsdRecursive( Abc_Ntk_t * pNtk, bool fVerbose ) +int Abc_NtkDsdLocal( Abc_Ntk_t * pNtk, bool fVerbose, bool fRecursive ) { int fCheck = 1; Dsd_Manager_t * pManDsd; @@ -319,7 +321,7 @@ int Abc_NtkDsdRecursive( Abc_Ntk_t * pNtk, bool fVerbose ) // collect nodes for decomposition vNodes = Abc_NtkCollectNodesForDsd( pNtk ); for ( i = 0; i < vNodes->nSize; i++ ) - Abc_NodeDecompDsdAndMux( vNodes->pArray[i], vNodes, pManDsd ); + Abc_NodeDecompDsdAndMux( vNodes->pArray[i], vNodes, pManDsd, fRecursive ); Vec_PtrFree( vNodes ); // stop the DSD manager @@ -371,7 +373,7 @@ Vec_Ptr_t * Abc_NtkCollectNodesForDsd( Abc_Ntk_t * pNtk ) SeeAlso [] ***********************************************************************/ -void Abc_NodeDecompDsdAndMux( Abc_Obj_t * pNode, Vec_Ptr_t * vNodes, Dsd_Manager_t * pManDsd ) +void Abc_NodeDecompDsdAndMux( Abc_Obj_t * pNode, Vec_Ptr_t * vNodes, Dsd_Manager_t * pManDsd, bool fRecursive ) { DdManager * dd = pNode->pNtk->pManFunc; Abc_Obj_t * pRoot, * pFanin, * pNode1, * pNode2, * pNodeC; @@ -384,7 +386,7 @@ void Abc_NodeDecompDsdAndMux( Abc_Obj_t * pNode, Vec_Ptr_t * vNodes, Dsd_Manager pNodeDsd = Dsd_Regular( pNodeDsd ); // determine what decomposition to use - if ( Dsd_NodeReadDecsNum(pNodeDsd) != Abc_ObjFaninNum(pNode) ) + if ( !fRecursive || Dsd_NodeReadDecsNum(pNodeDsd) != Abc_ObjFaninNum(pNode) ) { // perform DSD // set the inputs @@ -399,7 +401,7 @@ void Abc_NodeDecompDsdAndMux( Abc_Obj_t * pNode, Vec_Ptr_t * vNodes, Dsd_Manager for ( i = 0; i < nNodesDsd; i++ ) { pRoot = Abc_NtkDsdConstructNode( pManDsd, ppNodesDsd[i], pNode->pNtk ); - if ( Abc_NodeIsForDsd(pRoot) ) + if ( Abc_NodeIsForDsd(pRoot) && fRecursive ) Vec_PtrPush( vNodes, pRoot ); } free( ppNodesDsd ); @@ -457,9 +459,24 @@ void Abc_NodeDecompDsdAndMux( Abc_Obj_t * pNode, Vec_Ptr_t * vNodes, Dsd_Manager ***********************************************************************/ bool Abc_NodeIsForDsd( Abc_Obj_t * pNode ) { + DdManager * dd = pNode->pNtk->pManFunc; + DdNode * bFunc, * bFunc0, * bFunc1; assert( Abc_ObjIsNode(pNode) ); - if ( Cudd_DagSize(pNode->pData)-1 > Abc_ObjFaninNum(pNode) ) - return 1; +// if ( Cudd_DagSize(pNode->pData)-1 > Abc_ObjFaninNum(pNode) ) +// return 1; +// return 0; + + for ( bFunc = Cudd_Regular(pNode->pData); !cuddIsConstant(bFunc); ) + { + bFunc0 = Cudd_Regular( cuddE(bFunc) ); + bFunc1 = cuddT(bFunc); + if ( bFunc0 == b1 ) + bFunc = bFunc1; + else if ( bFunc1 == b1 || bFunc0 == bFunc1 ) + bFunc = bFunc0; + else + return 1; + } return 0; } @@ -514,6 +531,7 @@ int Abc_NodeFindMuxVar( DdManager * dd, DdNode * bFunc, int nVars ) return iVar; } + //////////////////////////////////////////////////////////////////////// /// END OF FILE /// //////////////////////////////////////////////////////////////////////// diff --git a/src/base/abc/abcMinBase.c b/src/base/abc/abcMinBase.c index 2a018e35..e143ba7b 100644 --- a/src/base/abc/abcMinBase.c +++ b/src/base/abc/abcMinBase.c @@ -93,6 +93,71 @@ int Abc_NodeMinimumBase( Abc_Obj_t * pNode ) /**Function************************************************************* + Synopsis [Makes nodes of the network fanin-dup-free.] + + Description [Returns the number of pairs of duplicated fanins.] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Abc_NtkRemoveDupFanins( Abc_Ntk_t * pNtk ) +{ + Abc_Obj_t * pNode; + int i, Counter, fChanged; + assert( Abc_NtkIsBddLogic(pNtk) ); + Counter = 0; + Abc_NtkForEachNode( pNtk, pNode, i ) + while ( fChanged = Abc_NodeRemoveDupFanins(pNode) ) + Counter += fChanged; + return Counter; +} + +/**Function************************************************************* + + Synopsis [Removes one pair of duplicated fanins if present.] + + Description [Returns 1 if the node is changed.] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Abc_NodeRemoveDupFanins( Abc_Obj_t * pNode ) +{ + Abc_Obj_t * pFanin1, * pFanin2; + int i, k; + assert( Abc_NtkIsBddLogic(pNode->pNtk) ); + assert( Abc_ObjIsNode(pNode) ); + // make sure fanins are not duplicated + Abc_ObjForEachFanin( pNode, pFanin2, i ) + { + Abc_ObjForEachFanin( pNode, pFanin1, k ) + { + if ( k >= i ) + break; + if ( pFanin1 == pFanin2 ) + { + DdManager * dd = pNode->pNtk->pManFunc; + DdNode * bVar1 = Cudd_bddIthVar( dd, i ); + DdNode * bVar2 = Cudd_bddIthVar( dd, k ); + DdNode * bTrans, * bTemp; + bTrans = Cudd_bddXnor( dd, bVar1, bVar2 ); Cudd_Ref( bTrans ); + pNode->pData = Cudd_bddAndAbstract( dd, bTemp = pNode->pData, bTrans, bVar2 ); Cudd_Ref( pNode->pData ); + Cudd_RecursiveDeref( dd, bTemp ); + Cudd_RecursiveDeref( dd, bTrans ); + Abc_NodeMinimumBase( pNode ); + return 1; + } + } + } + return 0; +} + +/**Function************************************************************* + Synopsis [Computes support of the node.] Description [] diff --git a/src/base/abc/abcNtbdd.c b/src/base/abc/abcNtbdd.c new file mode 100644 index 00000000..61c1a110 --- /dev/null +++ b/src/base/abc/abcNtbdd.c @@ -0,0 +1,402 @@ +/**CFile**************************************************************** + + FileName [abcNtbdd.c] + + SystemName [ABC: Logic synthesis and verification system.] + + PackageName [Network and node package.] + + Synopsis [Procedures to translate between the BDD and the network.] + + Author [Alan Mishchenko] + + Affiliation [UC Berkeley] + + Date [Ver. 1.0. Started - June 20, 2005.] + + Revision [$Id: abcNtbdd.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $] + +***********************************************************************/ + +#include "abc.h" + +//////////////////////////////////////////////////////////////////////// +/// DECLARATIONS /// +//////////////////////////////////////////////////////////////////////// + +static void Abc_NtkBddToMuxesPerform( Abc_Ntk_t * pNtk, Abc_Ntk_t * pNtkNew ); +static Abc_Obj_t * Abc_NodeBddToMuxes( Abc_Obj_t * pNodeOld, Abc_Ntk_t * pNtkNew, Abc_Obj_t * pConst1 ); +static Abc_Obj_t * Abc_NodeBddToMuxes_rec( DdManager * dd, DdNode * bFunc, Abc_Ntk_t * pNtkNew, st_table * tBdd2Node ); +static DdNode * Abc_NodeGlobalBdds_rec( DdManager * dd, Abc_Obj_t * pNode ); + +//////////////////////////////////////////////////////////////////////// +/// FUNCTION DEFITIONS /// +//////////////////////////////////////////////////////////////////////// + +/**Function************************************************************* + + Synopsis [Constructs the network isomorphic to the given BDD.] + + Description [Assumes that the BDD depends on the variables whose indexes + correspond to the names in the array (pNamesPi). Otherwise, returns NULL. + The resulting network comes with one node, whose functionality is + equal to the given BDD. To decompose this BDD into the network of + multiplexers use Abc_NtkBddToMuxes(). To decompose this BDD into + an And-Inverter Graph, use Abc_NtkStrash().] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Abc_Ntk_t * Abc_NtkDeriveFromBdd( DdManager * dd, DdNode * bFunc, char * pNamePo, Vec_Ptr_t * vNamesPi ) +{ + Abc_Ntk_t * pNtk; + Vec_Ptr_t * vNamesPiFake = NULL; + Abc_Obj_t * pNode, * pNodePi, * pNodePo; + DdNode * bSupp, * bTemp; + char * pName; + int i; + + // supply fake names if real names are not given + if ( pNamePo == NULL ) + pNamePo = "F"; + if ( vNamesPi == NULL ) + { + vNamesPiFake = Abc_NodeGetFakeNames( dd->size ); + vNamesPi = vNamesPiFake; + } + + // make sure BDD depends on the variables whose index + // does not exceed the size of the array with PI names + bSupp = Cudd_Support( dd, bFunc ); Cudd_Ref( bSupp ); + for ( bTemp = bSupp; bTemp != Cudd_ReadOne(dd); bTemp = cuddT(bTemp) ) + if ( (int)Cudd_NodeReadIndex(bTemp) >= Vec_PtrSize(vNamesPi) ) + break; + Cudd_RecursiveDeref( dd, bSupp ); + if ( bTemp != Cudd_ReadOne(dd) ) + return NULL; + + // start the network + pNtk = Abc_NtkAlloc( ABC_TYPE_LOGIC, ABC_FUNC_BDD ); + pNtk->pName = util_strsav(pNamePo); + // make sure the new manager has enough inputs + Cudd_bddIthVar( pNtk->pManFunc, Vec_PtrSize(vNamesPi) ); + // add the PIs corresponding to the names + Vec_PtrForEachEntry( vNamesPi, pName, i ) + Abc_NtkLogicStoreName( Abc_NtkCreatePi(pNtk), pName ); + // create the node + pNode = Abc_NtkCreateNode( pNtk ); + pNode->pData = Cudd_bddTransfer( dd, pNtk->pManFunc, bFunc ); Cudd_Ref(pNode->pData); + Abc_NtkForEachPi( pNtk, pNodePi, i ) + Abc_ObjAddFanin( pNode, pNodePi ); + // create the only PO + pNodePo = Abc_NtkCreatePo( pNtk ); + Abc_ObjAddFanin( pNodePo, pNode ); + Abc_NtkLogicStoreName( pNodePo, pNamePo ); + // make the network minimum base + Abc_NtkMinimumBase( pNtk ); + if ( vNamesPiFake ) + Abc_NodeFreeNames( vNamesPiFake ); + if ( !Abc_NtkCheck( pNtk ) ) + fprintf( stdout, "Abc_NtkDeriveFromBdd(): Network check has failed.\n" ); + return pNtk; +} + + + +/**Function************************************************************* + + Synopsis [Creates the network isomorphic to the union of local BDDs of the nodes.] + + Description [The nodes of the local BDDs are converted into the network nodes + with logic functions equal to the MUX.] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Abc_Ntk_t * Abc_NtkBddToMuxes( Abc_Ntk_t * pNtk ) +{ + int fCheck = 1; + Abc_Ntk_t * pNtkNew; + assert( Abc_NtkIsBddLogic(pNtk) ); + pNtkNew = Abc_NtkStartFrom( pNtk, ABC_TYPE_LOGIC, ABC_FUNC_SOP ); + Abc_NtkBddToMuxesPerform( pNtk, pNtkNew ); + Abc_NtkFinalize( pNtk, pNtkNew ); + // make sure everything is okay + if ( fCheck && !Abc_NtkCheck( pNtkNew ) ) + { + printf( "Abc_NtkBddToMuxes: The network check has failed.\n" ); + Abc_NtkDelete( pNtkNew ); + return NULL; + } + return pNtkNew; +} + +/**Function************************************************************* + + Synopsis [Converts the network to MUXes.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Abc_NtkBddToMuxesPerform( Abc_Ntk_t * pNtk, Abc_Ntk_t * pNtkNew ) +{ + ProgressBar * pProgress; + DdManager * dd = pNtk->pManFunc; + Abc_Obj_t * pNode, * pNodeNew, * pConst1; + Vec_Ptr_t * vNodes; + int i; + // create the constant one node + pConst1 = Abc_NodeCreateConst1( pNtkNew ); + // perform conversion in the topological order + vNodes = Abc_NtkDfs( pNtk, 0 ); + pProgress = Extra_ProgressBarStart( stdout, vNodes->nSize ); + Vec_PtrForEachEntry( vNodes, pNode, i ) + { + Extra_ProgressBarUpdate( pProgress, i, NULL ); + // convert one node + assert( Abc_ObjIsNode(pNode) ); + pNodeNew = Abc_NodeBddToMuxes( pNode, pNtkNew, pConst1 ); + // mark the old node with the new one + assert( pNode->pCopy == NULL ); + pNode->pCopy = pNodeNew; + } + Vec_PtrFree( vNodes ); + Extra_ProgressBarStop( pProgress ); +} + +/**Function************************************************************* + + Synopsis [Converts the node to MUXes.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Abc_Obj_t * Abc_NodeBddToMuxes( Abc_Obj_t * pNodeOld, Abc_Ntk_t * pNtkNew, Abc_Obj_t * pConst1 ) +{ + DdManager * dd = pNodeOld->pNtk->pManFunc; + DdNode * bFunc = pNodeOld->pData; + Abc_Obj_t * pFaninOld, * pNodeNew; + st_table * tBdd2Node; + int i; + // create the table mapping BDD nodes into the ABC nodes + tBdd2Node = st_init_table( st_ptrcmp, st_ptrhash ); + // add the constant and the elementary vars + st_insert( tBdd2Node, (char *)b1, (char *)pConst1 ); + Abc_ObjForEachFanin( pNodeOld, pFaninOld, i ) + st_insert( tBdd2Node, (char *)Cudd_bddIthVar(dd, i), (char *)pFaninOld->pCopy ); + // create the new nodes recursively + pNodeNew = Abc_NodeBddToMuxes_rec( dd, Cudd_Regular(bFunc), pNtkNew, tBdd2Node ); + st_free_table( tBdd2Node ); + if ( Cudd_IsComplement(bFunc) ) + pNodeNew = Abc_NodeCreateInv( pNtkNew, pNodeNew ); + return pNodeNew; +} + +/**Function************************************************************* + + Synopsis [Converts the node to MUXes.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Abc_Obj_t * Abc_NodeBddToMuxes_rec( DdManager * dd, DdNode * bFunc, Abc_Ntk_t * pNtkNew, st_table * tBdd2Node ) +{ + Abc_Obj_t * pNodeNew, * pNodeNew0, * pNodeNew1, * pNodeNewC; + assert( !Cudd_IsComplement(bFunc) ); + if ( st_lookup( tBdd2Node, (char *)bFunc, (char **)&pNodeNew ) ) + return pNodeNew; + // solve for the children nodes + pNodeNew0 = Abc_NodeBddToMuxes_rec( dd, Cudd_Regular(cuddE(bFunc)), pNtkNew, tBdd2Node ); + if ( Cudd_IsComplement(cuddE(bFunc)) ) + pNodeNew0 = Abc_NodeCreateInv( pNtkNew, pNodeNew0 ); + pNodeNew1 = Abc_NodeBddToMuxes_rec( dd, cuddT(bFunc), pNtkNew, tBdd2Node ); + if ( !st_lookup( tBdd2Node, (char *)Cudd_bddIthVar(dd, bFunc->index), (char **)&pNodeNewC ) ) + assert( 0 ); + // create the MUX node + pNodeNew = Abc_NodeCreateMux( pNtkNew, pNodeNewC, pNodeNew1, pNodeNew0 ); + st_insert( tBdd2Node, (char *)bFunc, (char *)pNodeNew ); + return pNodeNew; +} + + +/**Function************************************************************* + + Synopsis [Derives global BDDs for the COs of the network.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +DdManager * Abc_NtkGlobalBdds( Abc_Ntk_t * pNtk, int fLatchOnly ) +{ + int fReorder = 1; + ProgressBar * pProgress; + Vec_Ptr_t * vFuncsGlob; + Abc_Obj_t * pNode; + DdNode * bFunc; + DdManager * dd; + int i; + + // start the manager + assert( pNtk->pManGlob == NULL ); + dd = Cudd_Init( Abc_NtkCiNum(pNtk), 0, CUDD_UNIQUE_SLOTS, CUDD_CACHE_SLOTS, 0 ); + if ( fReorder ) + Cudd_AutodynEnable( dd, CUDD_REORDER_SYMM_SIFT ); + + // set the elementary variables + Abc_NtkCleanCopy( pNtk ); + Abc_NtkForEachCi( pNtk, pNode, i ) + pNode->pCopy = (Abc_Obj_t *)dd->vars[i]; + // assign the constant node BDD + pNode = Abc_AigConst1( pNtk->pManFunc ); + pNode->pCopy = (Abc_Obj_t *)dd->one; Cudd_Ref( dd->one ); + + // collect the global functions of the COs + vFuncsGlob = Vec_PtrAlloc( 100 ); + if ( fLatchOnly ) + { + // construct the BDDs + pProgress = Extra_ProgressBarStart( stdout, Abc_NtkLatchNum(pNtk) ); + Abc_NtkForEachLatch( pNtk, pNode, i ) + { + Extra_ProgressBarUpdate( pProgress, i, NULL ); + bFunc = Abc_NodeGlobalBdds_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) ); Cudd_Ref( bFunc ); + Vec_PtrPush( vFuncsGlob, 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_NodeGlobalBdds_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) ); Cudd_Ref( bFunc ); + Vec_PtrPush( vFuncsGlob, bFunc ); + } + Extra_ProgressBarStop( pProgress ); + } + + // derefence the intermediate BDDs + Abc_NtkForEachNode( pNtk, pNode, i ) + if ( pNode->pCopy ) + { + Cudd_RecursiveDeref( dd, (DdNode *)pNode->pCopy ); + pNode->pCopy = NULL; + } + // reorder one more time + if ( fReorder ) + { + Cudd_ReduceHeap( dd, CUDD_REORDER_SYMM_SIFT, 1 ); + Cudd_AutodynDisable( dd ); + } + pNtk->pManGlob = dd; + pNtk->vFuncsGlob = vFuncsGlob; + return dd; +} + +/**Function************************************************************* + + Synopsis [Derives the global BDD for one AIG node.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +DdNode * Abc_NodeGlobalBdds_rec( DdManager * dd, Abc_Obj_t * pNode ) +{ + DdNode * bFunc, * bFunc0, * bFunc1; + assert( !Abc_ObjIsComplement(pNode) ); + if ( Cudd_ReadKeys(dd) > 500000 ) + return NULL; + // if the result is available return + if ( pNode->pCopy ) + return (DdNode *)pNode->pCopy; + // compute the result for both branches + bFunc0 = Abc_NodeGlobalBdds_rec( dd, Abc_ObjFanin(pNode,0) ); + if ( bFunc0 == NULL ) + return NULL; + Cudd_Ref( bFunc0 ); + bFunc1 = Abc_NodeGlobalBdds_rec( dd, Abc_ObjFanin(pNode,1) ); + if ( bFunc1 == NULL ) + return NULL; + Cudd_Ref( bFunc1 ); + bFunc0 = Cudd_NotCond( bFunc0, Abc_ObjFaninC0(pNode) ); + bFunc1 = Cudd_NotCond( bFunc1, Abc_ObjFaninC1(pNode) ); + // get the final result + bFunc = Cudd_bddAnd( dd, bFunc0, bFunc1 ); Cudd_Ref( bFunc ); + Cudd_RecursiveDeref( dd, bFunc0 ); + Cudd_RecursiveDeref( dd, bFunc1 ); + // set the result + assert( pNode->pCopy == NULL ); + pNode->pCopy = (Abc_Obj_t *)bFunc; + return bFunc; +} + +/**Function************************************************************* + + Synopsis [Dereferences global BDDs of the network.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Abc_NtkFreeGlobalBdds( Abc_Ntk_t * pNtk ) +{ + DdNode * bFunc; + int i; + assert( pNtk->pManGlob ); + assert( pNtk->vFuncsGlob ); + Vec_PtrForEachEntry( pNtk->vFuncsGlob, bFunc, i ) + Cudd_RecursiveDeref( pNtk->pManGlob, bFunc ); + Vec_PtrFree( pNtk->vFuncsGlob ); + pNtk->vFuncsGlob = NULL; +} + +//////////////////////////////////////////////////////////////////////// +/// END OF FILE /// +//////////////////////////////////////////////////////////////////////// + + diff --git a/src/base/abc/abcPrint.c b/src/base/abc/abcPrint.c index c7599f11..4f8b4aeb 100644 --- a/src/base/abc/abcPrint.c +++ b/src/base/abc/abcPrint.c @@ -310,13 +310,13 @@ void Abc_NodePrintFanio( FILE * pFile, Abc_Obj_t * pNode ) SeeAlso [] ***********************************************************************/ -void Abc_NtkPrintFactor( FILE * pFile, Abc_Ntk_t * pNtk ) +void Abc_NtkPrintFactor( FILE * pFile, Abc_Ntk_t * pNtk, int fUseRealNames ) { Abc_Obj_t * pNode; int i; assert( Abc_NtkIsSopLogic(pNtk) ); Abc_NtkForEachNode( pNtk, pNode, i ) - Abc_NodePrintFactor( pFile, pNode ); + Abc_NodePrintFactor( pFile, pNode, fUseRealNames ); } /**Function************************************************************* @@ -330,9 +330,10 @@ void Abc_NtkPrintFactor( FILE * pFile, Abc_Ntk_t * pNtk ) SeeAlso [] ***********************************************************************/ -void Abc_NodePrintFactor( FILE * pFile, Abc_Obj_t * pNode ) +void Abc_NodePrintFactor( FILE * pFile, Abc_Obj_t * pNode, int fUseRealNames ) { Vec_Int_t * vFactor; + Vec_Ptr_t * vNamesIn; if ( Abc_ObjIsCo(pNode) ) pNode = Abc_ObjFanin0(pNode); if ( Abc_ObjIsPi(pNode) ) @@ -347,7 +348,14 @@ void Abc_NodePrintFactor( FILE * pFile, Abc_Obj_t * pNode ) } assert( Abc_ObjIsNode(pNode) ); vFactor = Ft_Factor( pNode->pData ); - Ft_FactorPrint( stdout, vFactor, NULL, Abc_ObjName(pNode) ); + if ( fUseRealNames ) + { + vNamesIn = Abc_NodeGetFaninNames(pNode); + Ft_FactorPrint( stdout, vFactor, (char **)vNamesIn->pArray, Abc_ObjName(pNode) ); + Abc_NodeFreeNames( vNamesIn ); + } + else + Ft_FactorPrint( stdout, vFactor, (char **)NULL, Abc_ObjName(pNode) ); Vec_IntFree( vFactor ); } diff --git a/src/base/abc/abcRefactor.c b/src/base/abc/abcRefactor.c index 9a413bb1..1524489d 100644 --- a/src/base/abc/abcRefactor.c +++ b/src/base/abc/abcRefactor.c @@ -95,6 +95,8 @@ int Abc_NtkRefactor( Abc_Ntk_t * pNtk, int nNodeSizeMax, int nConeSizeMax, bool int clk, clkStart = clock(); assert( Abc_NtkIsStrash(pNtk) ); + // cleanup the AIG + Abc_AigCleanup(pNtk->pManFunc); // start the managers pManCut = Abc_NtkManCutStart( nNodeSizeMax, nConeSizeMax, 2, 1000 ); pManRef = Abc_NtkManRefStart( nNodeSizeMax, nConeSizeMax, fUseDcs, fVerbose ); diff --git a/src/base/abc/abcRefs.c b/src/base/abc/abcRefs.c index dfcc3ae5..5cfa23ba 100644 --- a/src/base/abc/abcRefs.c +++ b/src/base/abc/abcRefs.c @@ -6,7 +6,7 @@ PackageName [Network and node package.] - Synopsis [Reference counting of the nodes.] + Synopsis [Procedures using reference counting of the AIG nodes.] Author [Alan Mishchenko] @@ -25,6 +25,7 @@ //////////////////////////////////////////////////////////////////////// static int Abc_NodeRefDeref( Abc_Obj_t * pNode, bool fReference, bool fLabel, Vec_Ptr_t * vNodes ); +static int Abc_NodeRefDerefStop( Abc_Obj_t * pNode, bool fReference ); //////////////////////////////////////////////////////////////////////// /// FUNCTION DEFITIONS /// @@ -32,7 +33,7 @@ static int Abc_NodeRefDeref( Abc_Obj_t * pNode, bool fReference, bool fLabel, Ve /**Function************************************************************* - Synopsis [Procedure returns the size of the MFFC of the node.] + Synopsis [Returns the MFFC size.] Description [] @@ -57,6 +58,31 @@ int Abc_NodeMffcSize( Abc_Obj_t * pNode ) /**Function************************************************************* + Synopsis [Returns the MFFC size while stopping at the complemented edges.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Abc_NodeMffcSizeStop( Abc_Obj_t * pNode ) +{ + int nConeSize1, nConeSize2; + assert( !Abc_ObjIsComplement( pNode ) ); + assert( Abc_ObjIsNode( pNode ) ); + if ( Abc_ObjFaninNum(pNode) == 0 ) + return 0; + nConeSize1 = Abc_NodeRefDerefStop( pNode, 0 ); // dereference + nConeSize2 = Abc_NodeRefDerefStop( pNode, 1 ); // reference + assert( nConeSize1 == nConeSize2 ); + assert( nConeSize1 > 0 ); + return nConeSize1; +} + +/**Function************************************************************* + Synopsis [Labels MFFC with the current traversal ID.] Description [] @@ -132,8 +158,8 @@ int Abc_NodeRefDeref( Abc_Obj_t * pNode, bool fReference, bool fLabel, Vec_Ptr_t if ( Abc_ObjIsCi(pNode) ) return 0; // process the internal node - pNode0 = Abc_ObjFanin( pNode, 0 ); - pNode1 = Abc_ObjFanin( pNode, 1 ); + pNode0 = Abc_ObjFanin0(pNode); + pNode1 = Abc_ObjFanin1(pNode); Counter = 1; if ( fReference ) { @@ -156,6 +182,47 @@ int Abc_NodeRefDeref( Abc_Obj_t * pNode, bool fReference, bool fLabel, Vec_Ptr_t /**Function************************************************************* + Synopsis [References/references the node and returns MFFC size.] + + Description [Stops at the complemented edges.] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Abc_NodeRefDerefStop( Abc_Obj_t * pNode, bool fReference ) +{ + Abc_Obj_t * pNode0, * pNode1; + int Counter; + // skip the CI + if ( Abc_ObjIsCi(pNode) ) + return 0; + // process the internal node + pNode0 = Abc_ObjFanin0(pNode); + pNode1 = Abc_ObjFanin1(pNode); + Counter = 1; + if ( fReference ) + { + if ( pNode0->vFanouts.nSize++ == 0 && !Abc_ObjFaninC0(pNode) ) + Counter += Abc_NodeRefDerefStop( pNode0, fReference ); + if ( pNode1->vFanouts.nSize++ == 0 && !Abc_ObjFaninC1(pNode) ) + Counter += Abc_NodeRefDerefStop( pNode1, fReference ); + } + else + { + assert( pNode0->vFanouts.nSize > 0 ); + assert( pNode1->vFanouts.nSize > 0 ); + if ( --pNode0->vFanouts.nSize == 0 && !Abc_ObjFaninC0(pNode) ) + Counter += Abc_NodeRefDerefStop( pNode0, fReference ); + if ( --pNode1->vFanouts.nSize == 0 && !Abc_ObjFaninC1(pNode) ) + Counter += Abc_NodeRefDerefStop( pNode1, fReference ); + } + return Counter; +} + +/**Function************************************************************* + Synopsis [Replaces MFFC of the node by the new factored form.] Description [] diff --git a/src/base/abc/abcRenode.c b/src/base/abc/abcRenode.c index c45f9763..b17e2394 100644 --- a/src/base/abc/abcRenode.c +++ b/src/base/abc/abcRenode.c @@ -31,7 +31,7 @@ static DdNode * Abc_NtkRenodeDeriveBdd_rec( DdManager * dd, Abc_Obj_t * pNode static void Abc_NtkRenodeSetBounds( Abc_Ntk_t * pNtk, int nThresh, int nFaninMax ); static void Abc_NtkRenodeSetBoundsCnf( Abc_Ntk_t * pNtk ); -static void Abc_NtkRenodeSetBoundsMulti( Abc_Ntk_t * pNtk ); +static void Abc_NtkRenodeSetBoundsMulti( Abc_Ntk_t * pNtk, int nThresh ); static void Abc_NtkRenodeSetBoundsSimple( Abc_Ntk_t * pNtk ); static void Abc_NtkRenodeCone( Abc_Obj_t * pNode, Vec_Ptr_t * vCone ); @@ -67,7 +67,7 @@ Abc_Ntk_t * Abc_NtkRenode( Abc_Ntk_t * pNtk, int nThresh, int nFaninMax, int fCn if ( fCnf ) Abc_NtkRenodeSetBoundsCnf( pNtk ); else if ( fMulti ) - Abc_NtkRenodeSetBoundsMulti( pNtk ); + Abc_NtkRenodeSetBoundsMulti( pNtk, nThresh ); else if ( fSimple ) Abc_NtkRenodeSetBoundsSimple( pNtk ); else @@ -393,9 +393,7 @@ void Abc_NtkRenodeSetBounds( Abc_Ntk_t * pNtk, int nThresh, int nFaninMax ) } // mark the PO drivers - Abc_NtkForEachPo( pNtk, pNode, i ) - Abc_ObjFanin0(pNode)->fMarkA = 1; - Abc_NtkForEachLatch( pNtk, pNode, i ) + Abc_NtkForEachCo( pNtk, pNode, i ) Abc_ObjFanin0(pNode)->fMarkA = 1; // make sure the fanin limit is met @@ -474,9 +472,7 @@ void Abc_NtkRenodeSetBoundsCnf( Abc_Ntk_t * pNtk ) } // mark the PO drivers - Abc_NtkForEachPo( pNtk, pNode, i ) - Abc_ObjFanin0(pNode)->fMarkA = 1; - Abc_NtkForEachLatch( pNtk, pNode, i ) + Abc_NtkForEachCo( pNtk, pNode, i ) Abc_ObjFanin0(pNode)->fMarkA = 1; // count the number of MUXes @@ -505,10 +501,10 @@ void Abc_NtkRenodeSetBoundsCnf( Abc_Ntk_t * pNtk ) SeeAlso [] ***********************************************************************/ -void Abc_NtkRenodeSetBoundsMulti( Abc_Ntk_t * pNtk ) +void Abc_NtkRenodeSetBoundsMulti( Abc_Ntk_t * pNtk, int nThresh ) { Abc_Obj_t * pNode; - int i; + int i, nFanouts, nConeSize; // make sure the mark is not set Abc_NtkForEachObj( pNtk, pNode, i ) @@ -521,7 +517,12 @@ void Abc_NtkRenodeSetBoundsMulti( Abc_Ntk_t * pNtk ) if ( Abc_NodeIsConst(pNode) ) continue; // mark the nodes with multiple fanouts - if ( Abc_ObjFanoutNum(pNode) > 1 ) +// if ( Abc_ObjFanoutNum(pNode) > 1 ) +// pNode->fMarkA = 1; + // mark the nodes with multiple fanouts + nFanouts = Abc_ObjFanoutNum(pNode); + nConeSize = Abc_NodeMffcSizeStop(pNode); + if ( (nFanouts - 1) * nConeSize > nThresh ) pNode->fMarkA = 1; // mark the children if they are pointed by the complemented edges if ( Abc_ObjFaninC0(pNode) ) @@ -531,9 +532,7 @@ void Abc_NtkRenodeSetBoundsMulti( Abc_Ntk_t * pNtk ) } // mark the PO drivers - Abc_NtkForEachPo( pNtk, pNode, i ) - Abc_ObjFanin0(pNode)->fMarkA = 1; - Abc_NtkForEachLatch( pNtk, pNode, i ) + Abc_NtkForEachCo( pNtk, pNode, i ) Abc_ObjFanin0(pNode)->fMarkA = 1; } diff --git a/src/base/abc/abcRewrite.c b/src/base/abc/abcRewrite.c index 62e506bb..f28aaa42 100644 --- a/src/base/abc/abcRewrite.c +++ b/src/base/abc/abcRewrite.c @@ -56,6 +56,8 @@ int Abc_NtkRewrite( Abc_Ntk_t * pNtk, int fUseZeros, int fVerbose ) int clk, clkStart = clock(); assert( Abc_NtkIsStrash(pNtk) ); + // cleanup the AIG + Abc_AigCleanup(pNtk->pManFunc); // start the rewriting manager pManRwr = Rwr_ManStart( 0 ); if ( pManRwr == NULL ) diff --git a/src/base/abc/abcShow.c b/src/base/abc/abcShow.c index 38840de0..a3e522cb 100644 --- a/src/base/abc/abcShow.c +++ b/src/base/abc/abcShow.c @@ -68,7 +68,7 @@ void Abc_NodeShowBdd( Abc_Obj_t * pNode ) 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_NodeFreeNames( vNamesIn ); Abc_NtkCleanCopy( pNode->pNtk ); fclose( pFile ); diff --git a/src/base/abc/abcSweep.c b/src/base/abc/abcSweep.c index 61d65ce3..ca9bd34e 100644 --- a/src/base/abc/abcSweep.c +++ b/src/base/abc/abcSweep.c @@ -25,13 +25,17 @@ /// DECLARATIONS /// //////////////////////////////////////////////////////////////////////// +extern Fraig_Man_t * Abc_NtkToFraig( Abc_Ntk_t * pNtk, Fraig_Params_t * pParams, int fAllNodes ); + static stmm_table * Abc_NtkFraigEquiv( Fraig_Man_t * p, Abc_Ntk_t * pNtk, int fUseInv, bool fVerbose ); static void Abc_NtkFraigTransform( Abc_Ntk_t * pNtk, stmm_table * tEquiv, int fUseInv, bool fVerbose ); static void Abc_NtkFraigMergeClassMapped( Abc_Ntk_t * pNtk, Abc_Obj_t * pChain, int fVerbose, int fUseInv ); static void Abc_NtkFraigMergeClass( Abc_Ntk_t * pNtk, Abc_Obj_t * pChain, int fVerbose, int fUseInv ); static int Abc_NodeDroppingCost( Abc_Obj_t * pNode ); -extern Fraig_Man_t * Abc_NtkToFraig( Abc_Ntk_t * pNtk, Fraig_Params_t * pParams, int fAllNodes ); +static void Abc_NodeSweep( Abc_Obj_t * pNode, int fVerbose ); +static void Abc_NodeConstantInput( Abc_Obj_t * pNode, Abc_Obj_t * pFanin, bool fConst0 ); +static void Abc_NodeComplementInput( Abc_Obj_t * pNode, Abc_Obj_t * pFanin ); //////////////////////////////////////////////////////////////////////// /// FUNCTION DEFITIONS /// @@ -427,6 +431,175 @@ int Abc_NtkCleanup( Abc_Ntk_t * pNtk, int fVerbose ) return Counter; } + + + +/**Function************************************************************* + + Synopsis [Tranditional sweep of the network.] + + Description [Propagates constant and single-input node, removes dangling nodes.] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Abc_NtkSweep( Abc_Ntk_t * pNtk, int fVerbose ) +{ + int fCheck = 1; + Abc_Obj_t * pNode; + int i, fConvert, nSwept, nSweptNew; + assert( Abc_NtkIsSopLogic(pNtk) || Abc_NtkIsBddLogic(pNtk) ); + // convert to the BDD representation + fConvert = 0; + if ( Abc_NtkIsSopLogic(pNtk) ) + Abc_NtkSopToBdd(pNtk), fConvert = 1; + // perform cleanup to get rid of dangling nodes + nSwept = Abc_NtkCleanup( pNtk, 0 ); + // make the network minimum base + Abc_NtkRemoveDupFanins(pNtk); + Abc_NtkMinimumBase(pNtk); + do + { + // sweep constants and single-input nodes + Abc_NtkForEachNode( pNtk, pNode, i ) + if ( Abc_ObjFaninNum(pNode) < 2 ) + Abc_NodeSweep( pNode, fVerbose ); + // make the network minimum base + Abc_NtkRemoveDupFanins(pNtk); + Abc_NtkMinimumBase(pNtk); + // perform final clean up (in case new danglies are created) + nSweptNew = Abc_NtkCleanup( pNtk, 0 ); + nSwept += nSweptNew; + } + while ( nSweptNew ); + // conver back to BDD + if ( fConvert ) + Abc_NtkBddToSop(pNtk); + // report + if ( fVerbose ) + printf( "Sweep removed %d nodes.\n", nSwept ); + // check + if ( fCheck && !Abc_NtkCheck( pNtk ) ) + { + printf( "Abc_NtkSweep: The network check has failed.\n" ); + return -1; + } + return nSwept; +} + +/**Function************************************************************* + + Synopsis [Tranditional sweep of the network.] + + Description [Propagates constant and single-input node, removes dangling nodes.] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Abc_NodeSweep( Abc_Obj_t * pNode, int fVerbose ) +{ + Vec_Ptr_t * vFanout = pNode->pNtk->vPtrTemp; + Abc_Obj_t * pFanout, * pDriver; + int i; + assert( Abc_ObjFaninNum(pNode) < 2 ); + assert( Abc_ObjFanoutNum(pNode) > 0 ); + // iterate through the fanouts + Abc_NodeCollectFanouts( pNode, vFanout ); + Vec_PtrForEachEntry( vFanout, pFanout, i ) + { + if ( Abc_ObjIsCo(pFanout) ) + { + if ( Abc_ObjFaninNum(pNode) == 1 ) + { + pDriver = Abc_ObjFanin0(pNode); + if ( Abc_ObjIsCi(pDriver) || Abc_ObjFanoutNum(pDriver) > 1 || Abc_ObjFanoutNum(pNode) > 1 ) + continue; + // the driver is a node and its only fanout is this node + if ( Abc_NodeIsInv(pNode) ) + pDriver->pData = Cudd_Not(pDriver->pData); + // replace the fanin of the fanout + Abc_ObjPatchFanin( pFanout, pNode, pDriver ); + } + continue; + } + // the fanout is a regular node + if ( Abc_ObjFaninNum(pNode) == 0 ) + Abc_NodeConstantInput( pFanout, pNode, Abc_NodeIsConst0(pNode) ); + else + { + assert( Abc_ObjFaninNum(pNode) == 1 ); + pDriver = Abc_ObjFanin0(pNode); + if ( Abc_NodeIsInv(pNode) ) + Abc_NodeComplementInput( pFanout, pNode ); + Abc_ObjPatchFanin( pFanout, pNode, pDriver ); + } + } +} + +/**Function************************************************************* + + Synopsis [Replaces the local function by its cofactor.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Abc_NodeConstantInput( Abc_Obj_t * pNode, Abc_Obj_t * pFanin, bool fConst0 ) +{ + DdManager * dd = pNode->pNtk->pManFunc; + DdNode * bVar, * bTemp; + int iFanin; + assert( Abc_NtkIsBddLogic(pNode->pNtk) ); + if ( (iFanin = Vec_FanFindEntry( &pNode->vFanins, pFanin->Id )) == -1 ) + { + printf( "Node %s should be among", Abc_ObjName(pFanin) ); + printf( " the fanins of node %s...\n", Abc_ObjName(pNode) ); + return; + } + bVar = Cudd_NotCond( Cudd_bddIthVar(dd, iFanin), fConst0 ); + pNode->pData = Cudd_Cofactor( dd, bTemp = pNode->pData, bVar ); Cudd_Ref( pNode->pData ); + Cudd_RecursiveDeref( dd, bTemp ); +} + +/**Function************************************************************* + + Synopsis [Changes the polarity of one fanin.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Abc_NodeComplementInput( Abc_Obj_t * pNode, Abc_Obj_t * pFanin ) +{ + DdManager * dd = pNode->pNtk->pManFunc; + DdNode * bVar, * bCof0, * bCof1; + int iFanin; + assert( Abc_NtkIsBddLogic(pNode->pNtk) ); + if ( (iFanin = Vec_FanFindEntry( &pNode->vFanins, pFanin->Id )) == -1 ) + { + printf( "Node %s should be among", Abc_ObjName(pFanin) ); + printf( " the fanins of node %s...\n", Abc_ObjName(pNode) ); + return; + } + bVar = Cudd_bddIthVar( dd, iFanin ); + bCof0 = Cudd_Cofactor( dd, pNode->pData, Cudd_Not(bVar) ); Cudd_Ref( bCof0 ); + bCof1 = Cudd_Cofactor( dd, pNode->pData, bVar ); Cudd_Ref( bCof1 ); + Cudd_RecursiveDeref( dd, pNode->pData ); + pNode->pData = Cudd_bddIte( dd, bVar, bCof0, bCof1 ); Cudd_Ref( pNode->pData ); + Cudd_RecursiveDeref( dd, bCof0 ); + Cudd_RecursiveDeref( dd, bCof1 ); +} + //////////////////////////////////////////////////////////////////////// /// END OF FILE /// //////////////////////////////////////////////////////////////////////// diff --git a/src/base/abc/abcUtil.c b/src/base/abc/abcUtil.c index 9a2acc32..2c460301 100644 --- a/src/base/abc/abcUtil.c +++ b/src/base/abc/abcUtil.c @@ -1,6 +1,6 @@ /**CFile**************************************************************** - FileName [abcUtils.c] + FileName [abcUtil.c] SystemName [ABC: Logic synthesis and verification system.] @@ -14,7 +14,7 @@ Date [Ver. 1.0. Started - June 20, 2005.] - Revision [$Id: abcUtils.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $] + Revision [$Id: abcUtil.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $] ***********************************************************************/ @@ -410,6 +410,9 @@ int Abc_NtkLogicMakeSimpleCos( Abc_Ntk_t * pNtk, bool fDuplicate ) Abc_ObjPatchFanin( pNode, pDriver, pDriverNew ); assert( Abc_ObjFanoutNum(pDriverNew) == 1 ); nDupGates++; + // remove the old driver if it dangles + if ( Abc_ObjFanoutNum(pDriver) == 0 ) + Abc_NtkDeleteObj( pDriver ); } assert( Abc_NtkLogicHasSimpleCos(pNtk) ); return nDupGates; @@ -887,9 +890,47 @@ Vec_Ptr_t * Abc_NodeGetFaninNames( Abc_Obj_t * pNode ) SeeAlso [] ***********************************************************************/ -void Abc_NodeFreeFaninNames( Vec_Ptr_t * vNames ) +Vec_Ptr_t * Abc_NodeGetFakeNames( int nNames ) { + Vec_Ptr_t * vNames; + char Buffer[5]; int i; + + vNames = Vec_PtrAlloc( nNames ); + for ( i = 0; i < nNames; i++ ) + { + if ( nNames < 26 ) + { + Buffer[0] = 'a' + i; + Buffer[1] = 0; + } + else + { + Buffer[0] = 'a' + i%26; + Buffer[1] = '0' + i/26; + Buffer[2] = 0; + } + Vec_PtrPush( vNames, util_strsav(Buffer) ); + } + return vNames; +} + +/**Function************************************************************* + + Synopsis [Gets fanin node names.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Abc_NodeFreeNames( Vec_Ptr_t * vNames ) +{ + int i; + if ( vNames == NULL ) + return; for ( i = 0; i < vNames->nSize; i++ ) free( vNames->pArray[i] ); Vec_PtrFree( vNames ); diff --git a/src/base/abc/module.make b/src/base/abc/module.make index d3d4091b..695e056b 100644 --- a/src/base/abc/module.make +++ b/src/base/abc/module.make @@ -19,6 +19,7 @@ SRC += src/base/abc/abc.c \ src/base/abc/abcMiter.c \ src/base/abc/abcNames.c \ src/base/abc/abcNetlist.c \ + src/base/abc/abcNtbdd.c \ src/base/abc/abcPrint.c \ src/base/abc/abcReconv.c \ src/base/abc/abcRefactor.c \ diff --git a/src/opt/dec/dec.h b/src/opt/dec/dec.h new file mode 100644 index 00000000..26af6b1c --- /dev/null +++ b/src/opt/dec/dec.h @@ -0,0 +1,391 @@ +/**CFile**************************************************************** + + FileName [dec.h] + + SystemName [ABC: Logic synthesis and verification system.] + + PackageName [A simple decomposition tree/node data structure and its APIs.] + + Synopsis [External declarations.] + + Author [Alan Mishchenko] + + Affiliation [UC Berkeley] + + Date [Ver. 1.0. Started - June 20, 2005.] + + Revision [$Id: dec.h,v 1.00 2005/06/20 00:00:00 alanmi Exp $] + +***********************************************************************/ + +#ifndef __DEC_H__ +#define __DEC_H__ + +//////////////////////////////////////////////////////////////////////// +/// INCLUDES /// +//////////////////////////////////////////////////////////////////////// + +//////////////////////////////////////////////////////////////////////// +/// PARAMETERS /// +//////////////////////////////////////////////////////////////////////// + +//////////////////////////////////////////////////////////////////////// +/// BASIC TYPES /// +//////////////////////////////////////////////////////////////////////// + +typedef struct Dec_Node_t_ Dec_Node_t; +struct Dec_Node_t_ +{ + // the first child + unsigned fCompl0 : 1; // complemented attribute of the first fanin + unsigned iFanin0 : 11; // the number of the first fanin + // the second child + unsigned fCompl1 : 1; // complemented attribute of the second fanin + unsigned iFanin1 : 11; // the number of the second fanin + // other info + unsigned fIntern : 1; // marks all internal nodes (to distinquish them from elementary vars) + unsigned fConst : 1; // marks the constant 1 function (topmost node only) + unsigned fCompl : 1; // marks the complement of topmost node (topmost node only) + // printing info (factored forms only) + unsigned fNodeOr : 1; // marks the original OR node + unsigned fEdge0 : 1; // marks the original complemented edge + unsigned fEdge1 : 1; // marks the original complemented edge + // some bits are left unused +}; + +/* + The decomposition tree data structure is designed to represent relatively small + (up to 100 nodes) AIGs used for factoring, rewriting, and decomposition. + + For simplicity, the nodes of the decomposition tree are written in DFS order + into an integer vector (Vec_Int_t). The decomposition node (Dec_Node_t) + is typecast into an integer when written into the array. + + This representation can be readily translated into the main AIG represented + in the ABC network. Because of the linear order of the decomposition nodes + in the array, it is easy to put the existing AIG nodes in correspondence with + them. This process begins by first putting leaves of the decomposition tree + in correpondence with the fanins of the cut used to derive the function, + which was decomposed. Next for each internal node of the decomposition tree, + we find or create a corresponding node in the AIG. Finally, the root node of + the tree replaces the original root node of the cut, which was decomposed. + + To achieve the above scenario, we reserve the first n entries for the array + to the fanins of the cut (the number of fanins is n). These entries are left + empty in the array (that is, they are represented by 0 integer). Each entry + after the fanins is an internal node (flag fIntern is set to 1). The internal + nodes can have complemented inputs (denoted by flags fComp0 and fCompl1). + The last node can be complemented (fCompl), which is true if the root node + of the decomposition tree is represented by a complemented AIG node. + + Two cases have to be specially considered: a constant function and a function + equal to an elementary variables (possibly complemented). In these two cases, + the decomposition tree/array has exactly n+1 nodes, where n in the number of + fanins. (A constant function may depend on n variable, in which case these + are redundant variables. Similarly, a function can be a function in n-D space + but in fact depend only on one variable in this space.) + + When the function is a constant, the last node has a flag fConst set to 1. + In this case the complemented flag (fCompl) shows the value of the constant. + (fCompl = 0 means costant 1; fCompl = 1 means constant 0). + When the function if an elementary variable, the last node has both pointers + pointing to the same elementary node, while the complemented flag (fCompl) + shows whether the variable is complemented. For example: x' = Not( AND(x, x) ). + + When manipulating the decomposition tree, it is convenient to return the + intermediate results of decomposition as an integer, which includes the number + of the Dec_Node_t in the array of decomposition nodes and the complemented flag. + Factoring is a special case of decomposition, which demonstrates this kind + of manipulation. +*/ + +//////////////////////////////////////////////////////////////////////// +/// MACRO DEFITIONS /// +//////////////////////////////////////////////////////////////////////// + +//////////////////////////////////////////////////////////////////////// +/// FUNCTION DECLARATIONS /// +//////////////////////////////////////////////////////////////////////// + +/**Function************************************************************* + + Synopsis [Cleans the decomposition node.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +static inline void Dec_NodeClean( Dec_Node_t * pNode ) { *((int *)pNode) = 0; } + +/**Function************************************************************* + + Synopsis [Convert between an interger and an decomposition node.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +static inline Dec_Node_t Dec_Int2Node( int Num ) { return *((Dec_Node_t *)&Num); } +static inline int Dec_Node2Int( Dec_Node_t Node ) { return *((int *)&Node); } + +/**Function************************************************************* + + Synopsis [Returns the pointer to the i-th decomposition node.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +static inline Dec_Node_t * Dec_NodeRead( Vec_Int_t * vDec, int i ) { return (Dec_Node_t *)vDec->pArray + i; } + +/**Function************************************************************* + + Synopsis [Returns the pointer to the last decomposition node.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +static inline Dec_Node_t * Dec_NodeReadLast( Vec_Int_t * vDec ) { return (Dec_Node_t *)vDec->pArray + vDec->nSize - 1; } + +/**Function************************************************************* + + Synopsis [Returns the pointer to the fanins of the i-th decomposition node.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +static inline Dec_Node_t * Dec_NodeFanin0( Vec_Int_t * vDec, int i ) { assert( Dec_NodeRead(vDec,i)->fIntern ); return (Dec_Node_t *)vDec->pArray + Dec_NodeRead(vDec,i)->iFanin0; } +static inline Dec_Node_t * Dec_NodeFanin1( Vec_Int_t * vDec, int i ) { assert( Dec_NodeRead(vDec,i)->fIntern ); return (Dec_Node_t *)vDec->pArray + Dec_NodeRead(vDec,i)->iFanin1; } + +/**Function************************************************************* + + Synopsis [Returns the complemented attributes of the i-th decomposition node.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +static inline bool Dec_NodeFaninC0( Vec_Int_t * vDec, int i ) { assert( Dec_NodeRead(vDec,i)->fIntern ); return (bool)Dec_NodeRead(vDec,i)->fCompl0; } +static inline bool Dec_NodeFaninC1( Vec_Int_t * vDec, int i ) { assert( Dec_NodeRead(vDec,i)->fIntern ); return (bool)Dec_NodeRead(vDec,i)->fCompl1; } + +/**Function************************************************************* + + Synopsis [Returns the number of leaf variables.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +static inline int Dec_TreeNumVars( Vec_Int_t * vDec ) +{ + int i; + for ( i = 0; i < vDec->nSize; i++ ) + if ( vDec->pArray[i] ) + break; + return i; +} + +/**Function************************************************************* + + Synopsis [Returns the number of AND nodes in the tree.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +static int Dec_TreeNumAnds( Vec_Int_t * vDec ) +{ + Dec_Node_t * pNode; + pNode = Dec_NodeReadLast(vDec); + if ( pNode->fConst ) // constant + return 0; + if ( pNode->iFanin0 == pNode->iFanin1 ) // literal + return 0; + return vDec->nSize - Dec_TreeNumVars(vDec); +} + +/**Function************************************************************* + + Synopsis [Returns the number of literals in the factored form.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +static inline int Dec_TreeNumFFLits( Vec_Int_t * vDec ) +{ + return 1 + Dec_TreeNumAnds( vDec ); +} + + + +/**Function************************************************************* + + Synopsis [Checks if the output node of the decomposition tree is complemented.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +static inline bool Dec_TreeIsComplement( Vec_Int_t * vForm ) { return Dec_NodeReadLast(vForm)->fCompl; } + +/**Function************************************************************* + + Synopsis [Complements the output node of the decomposition tree.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +static inline void Dec_TreeComplement( Vec_Int_t * vForm ) { Dec_NodeReadLast(vForm)->fCompl ^= 1; } + + +/**Function************************************************************* + + Synopsis [Checks if the output node is a constant.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +static inline bool Dec_TreeIsConst( Vec_Int_t * vForm ) { return Dec_NodeReadLast(vForm)->fConst; } +static inline bool Dec_TreeIsConst0( Vec_Int_t * vForm ) { return Dec_NodeReadLast(vForm)->fConst && Dec_NodeReadLast(vForm)->fCompl; } +static inline bool Dec_TreeIsConst1( Vec_Int_t * vForm ) { return Dec_NodeReadLast(vForm)->fConst && !Dec_NodeReadLast(vForm)->fCompl; } + +/**Function************************************************************* + + Synopsis [Creates a constant 0 decomposition tree.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +static inline Vec_Int_t * Dec_TreeCreateConst0() +{ + Vec_Int_t * vForm; + Dec_Node_t * pNode; + // create the constant node + vForm = Vec_IntAlloc( 1 ); + Vec_IntPush( vForm, 0 ); + pNode = Dec_NodeReadLast( vForm ); + pNode->fIntern = 1; + pNode->fConst = 1; + pNode->fCompl = 1; + return vForm; +} + +/**Function************************************************************* + + Synopsis [Creates a constant 1 decomposition tree.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +static inline Vec_Int_t * Dec_TreeCreateConst1() +{ + Vec_Int_t * vForm; + Dec_Node_t * pNode; + // create the constant node + vForm = Vec_IntAlloc( 1 ); + Vec_IntPush( vForm, 0 ); + pNode = Dec_NodeReadLast( vForm ); + pNode->fIntern = 1; + pNode->fConst = 1; + pNode->fCompl = 0; + return vForm; +} + + +/**Function************************************************************* + + Synopsis [Checks if the decomposition tree is an elementary var.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +static inline bool Dec_TreeIsVar( Vec_Int_t * vForm ) +{ + return Dec_NodeReadLast(vForm)->iFanin0 == Dec_NodeReadLast(vForm)->iFanin1; +} + +/**Function************************************************************* + + Synopsis [Creates the decomposition tree to represent an elementary var.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +static inline Vec_Int_t * Dec_TreeCreateVar( int iVar, int nVars, int fCompl ) +{ + Vec_Int_t * vForm; + Dec_Node_t * pNode; + // create the elementary variable node + vForm = Vec_IntAlloc( nVars + 1 ); + Vec_IntFill( vForm, nVars + 1, 0 ); + pNode = Dec_NodeReadLast( vForm ); + pNode->iFanin0 = iVar; + pNode->iFanin1 = iVar; + pNode->fIntern = 1; + pNode->fCompl = fCompl; + return vForm; +} + +//////////////////////////////////////////////////////////////////////// +/// END OF FILE /// +//////////////////////////////////////////////////////////////////////// + +#endif + diff --git a/src/opt/dec/module.make b/src/opt/dec/module.make new file mode 100644 index 00000000..d6d908e7 --- /dev/null +++ b/src/opt/dec/module.make @@ -0,0 +1 @@ +SRC += diff --git a/src/sat/fraig/fraigSat.c b/src/sat/fraig/fraigSat.c index 13c09a9e..da9e8e2b 100644 --- a/src/sat/fraig/fraigSat.c +++ b/src/sat/fraig/fraigSat.c @@ -83,7 +83,7 @@ void Fraig_ManProveMiter( Fraig_Man_t * p ) if ( !p->fTryProve ) return; - + clk = clock(); // consider all outputs of the multi-output miter for ( i = 0; i < p->vOutputs->nSize; i++ ) diff --git a/src/sop/ft/ftFactor.c b/src/sop/ft/ftFactor.c index 19f70e36..0a32e1c8 100644 --- a/src/sop/ft/ftFactor.c +++ b/src/sop/ft/ftFactor.c @@ -19,6 +19,7 @@ #include "abc.h" #include "mvc.h" #include "ft.h" +#include "dec.h" //////////////////////////////////////////////////////////////////////// /// DECLARATIONS /// diff --git a/src/sop/ft/ftPrint.c b/src/sop/ft/ftPrint.c index e08ceaae..78f91b8f 100644 --- a/src/sop/ft/ftPrint.c +++ b/src/sop/ft/ftPrint.c @@ -46,9 +46,8 @@ static int Ft_FactorPrintOutputName( FILE * pFile, char * pNameOut, int fComp void Ft_FactorPrint( FILE * pFile, Vec_Int_t * vForm, char * pNamesIn[], char * pNameOut ) { Ft_Node_t * pNode; - char Buffer[5]; - int Pos, i, LitSizeMax, LitSizeCur, nVars; - int fMadeupNames; + Vec_Ptr_t * vNamesIn = NULL; + int LitSizeMax, LitSizeCur, nVars, Pos, i; // sanity checks nVars = Ft_FactorGetNumVars( vForm ); @@ -56,27 +55,13 @@ void Ft_FactorPrint( FILE * pFile, Vec_Int_t * vForm, char * pNamesIn[], char * assert( vForm->nSize > nVars ); // create the names if not given by the user - fMadeupNames = 0; if ( pNamesIn == NULL ) { - fMadeupNames = 1; - pNamesIn = ALLOC( char *, nVars ); - for ( i = 0; i < nVars; i++ ) - { - if ( nVars < 26 ) - { - Buffer[0] = 'a' + i; - Buffer[1] = 0; - } - else - { - Buffer[0] = 'a' + i%26; - Buffer[1] = '0' + i/26; - Buffer[2] = 0; - } - pNamesIn[i] = util_strsav( Buffer ); - } + vNamesIn = Abc_NodeGetFakeNames( nVars ); + pNamesIn = (char **)vNamesIn->pArray; } + if ( pNameOut == NULL ) + pNameOut = "F"; // get the size of the longest literal LitSizeMax = 0; @@ -103,12 +88,8 @@ void Ft_FactorPrint( FILE * pFile, Vec_Int_t * vForm, char * pNamesIn[], char * } fprintf( pFile, "\n" ); - if ( fMadeupNames ) - { - for ( i = 0; i < nVars; i++ ) - free( pNamesIn[i] ); - free( pNamesIn ); - } + if ( vNamesIn ) + Abc_NodeFreeNames( vNamesIn ); } /**Function************************************************************* |