diff options
| author | Alan Mishchenko <alanmi@berkeley.edu> | 2005-09-02 08:01:00 -0700 |
|---|---|---|
| committer | Alan Mishchenko <alanmi@berkeley.edu> | 2005-09-02 08:01:00 -0700 |
| commit | dce73ade2fa0c7a01b58d4a6c592e0e07cbb5499 (patch) | |
| tree | 3563fd4a27d3b0faea3ca590d6243fb4590d8214 | |
| parent | 9c98ba1794a2422f1be8202d615633e1c8e74b10 (diff) | |
| download | abc-dce73ade2fa0c7a01b58d4a6c592e0e07cbb5499.tar.gz abc-dce73ade2fa0c7a01b58d4a6c592e0e07cbb5499.tar.bz2 abc-dce73ade2fa0c7a01b58d4a6c592e0e07cbb5499.zip | |
Version abc50902
42 files changed, 2113 insertions, 2620 deletions
@@ -13,11 +13,14 @@ MODULES := src/base/abc src/base/cmd src/base/io src/base/main \ 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 + src/sop/mvc default: $(PROG) -CFLAGS += -Wall -Wno-unused-function -g -O $(patsubst %, -I%, $(MODULES)) +OPTFLAGS := -DNDEBUG -O3 +#OPTFLAGS := -g -O + +CFLAGS += -Wall -Wno-unused-function $(OPTFLAGS) $(patsubst %, -I%, $(MODULES)) CXXFLAGS += $(CFLAGS) LIBS := @@ -865,22 +865,6 @@ SOURCE=.\src\sop\mvc\mvcSort.c SOURCE=.\src\sop\mvc\mvcUtils.c # End Source File # End Group -# Begin Group "ft" - -# PROP Default_Filter "" -# Begin Source File - -SOURCE=.\src\sop\ft\ft.h -# End Source File -# Begin Source File - -SOURCE=.\src\sop\ft\ftFactor.c -# End Source File -# Begin Source File - -SOURCE=.\src\sop\ft\ftPrint.c -# End Source File -# End Group # End Group # Begin Group "sat" @@ -1220,6 +1204,26 @@ SOURCE=.\src\opt\cut\cutTruth.c SOURCE=.\src\opt\dec\dec.h # End Source File +# Begin Source File + +SOURCE=.\src\opt\dec\decAbc.c +# End Source File +# Begin Source File + +SOURCE=.\src\opt\dec\decFactor.c +# End Source File +# Begin Source File + +SOURCE=.\src\opt\dec\decMan.c +# End Source File +# Begin Source File + +SOURCE=.\src\opt\dec\decPrint.c +# End Source File +# Begin Source File + +SOURCE=.\src\opt\dec\decUtil.c +# End Source File # End Group # End Group # Begin Group "map" Binary files differ@@ -6,292 +6,13 @@ --------------------Configuration: abc - Win32 Debug-------------------- </h3> <h3>Command Lines</h3> -Creating temporary file "C:\DOCUME~1\alanmi\LOCALS~1\Temp\RSP37EA.tmp" with contents +Creating temporary file "C:\DOCUME~1\alanmi\LOCALS~1\Temp\RSP6D.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\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\RSP37EA.tmp" -Creating temporary file "C:\DOCUME~1\alanmi\LOCALS~1\Temp\RSP37EB.tmp" with contents +Creating command line "cl.exe @C:\DOCUME~1\alanmi\LOCALS~1\Temp\RSP6D.tmp" +Creating temporary file "C:\DOCUME~1\alanmi\LOCALS~1\Temp\RSP6E.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 @@ -456,8 +177,6 @@ kernel32.lib user32.lib gdi32.lib winspool.lib comdlg32.lib advapi32.lib shell32 .\Debug\mvcPrint.obj .\Debug\mvcSort.obj .\Debug\mvcUtils.obj -.\Debug\ftFactor.obj -.\Debug\ftPrint.obj .\Debug\added.obj .\Debug\solver.obj .\Debug\msatActivity.obj @@ -517,6 +236,11 @@ kernel32.lib user32.lib gdi32.lib winspool.lib comdlg32.lib advapi32.lib shell32 .\Debug\cutSeq.obj .\Debug\cutTable.obj .\Debug\cutTruth.obj +.\Debug\decAbc.obj +.\Debug\decFactor.obj +.\Debug\decMan.obj +.\Debug\decPrint.obj +.\Debug\decUtil.obj .\Debug\fpga.obj .\Debug\fpgaCore.obj .\Debug\fpgaCreate.obj @@ -575,304 +299,12 @@ kernel32.lib user32.lib gdi32.lib winspool.lib comdlg32.lib advapi32.lib shell32 .\Debug\strsav.obj .\Debug\texpand.obj ] -Creating command line "link.exe @C:\DOCUME~1\alanmi\LOCALS~1\Temp\RSP37EB.tmp" +Creating command line "link.exe @C:\DOCUME~1\alanmi\LOCALS~1\Temp\RSP6E.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\RSP37ED.tmp" with contents +Creating temporary file "C:\DOCUME~1\alanmi\LOCALS~1\Temp\RSP6F.tmp" with contents [ /nologo /o"Debug/abc.bsc" .\Debug\abc.sbr @@ -1037,8 +469,6 @@ Creating temporary file "C:\DOCUME~1\alanmi\LOCALS~1\Temp\RSP37ED.tmp" with cont .\Debug\mvcPrint.sbr .\Debug\mvcSort.sbr .\Debug\mvcUtils.sbr -.\Debug\ftFactor.sbr -.\Debug\ftPrint.sbr .\Debug\added.sbr .\Debug\solver.sbr .\Debug\msatActivity.sbr @@ -1098,6 +528,11 @@ Creating temporary file "C:\DOCUME~1\alanmi\LOCALS~1\Temp\RSP37ED.tmp" with cont .\Debug\cutSeq.sbr .\Debug\cutTable.sbr .\Debug\cutTruth.sbr +.\Debug\decAbc.sbr +.\Debug\decFactor.sbr +.\Debug\decMan.sbr +.\Debug\decPrint.sbr +.\Debug\decUtil.sbr .\Debug\fpga.sbr .\Debug\fpgaCore.sbr .\Debug\fpgaCreate.sbr @@ -1155,14 +590,14 @@ Creating temporary file "C:\DOCUME~1\alanmi\LOCALS~1\Temp\RSP37ED.tmp" with cont .\Debug\safe_mem.sbr .\Debug\strsav.sbr .\Debug\texpand.sbr] -Creating command line "bscmake.exe @C:\DOCUME~1\alanmi\LOCALS~1\Temp\RSP37ED.tmp" +Creating command line "bscmake.exe @C:\DOCUME~1\alanmi\LOCALS~1\Temp\RSP6F.tmp" Creating browse info file... <h3>Output Window</h3> <h3>Results</h3> -abc.exe - 0 error(s), 13 warning(s) +abc.exe - 0 error(s), 0 warning(s) </pre> </body> </html> diff --git a/src/base/abc/abc.c b/src/base/abc/abc.c index 97e5663f..dca80ca5 100644 --- a/src/base/abc/abc.c +++ b/src/base/abc/abc.c @@ -20,7 +20,6 @@ #include "abc.h" #include "mainInt.h" -#include "ft.h" #include "fraig.h" #include "fxu.h" #include "cut.h" @@ -162,7 +161,6 @@ void Abc_Init( Abc_Frame_t * pAbc ) Cmd_CommandAdd( pAbc, "Verification", "cec", Abc_CommandCec, 0 ); Cmd_CommandAdd( pAbc, "Verification", "sec", Abc_CommandSec, 0 ); - Ft_FactorStartMan(); // Rwt_Man4ExploreStart(); // Map_Var3Print(); // Map_Var4Test(); @@ -181,7 +179,6 @@ void Abc_Init( Abc_Frame_t * pAbc ) ***********************************************************************/ void Abc_End() { - Ft_FactorStopMan(); Abc_NtkFraigStoreClean(); // Rwt_Man4ExplorePrint(); } @@ -1707,7 +1704,7 @@ int Abc_CommandRewrite( Abc_Frame_t * pAbc, int argc, char ** argv ) fprintf( pErr, "This command can only be applied to an AIG.\n" ); return 1; } - if ( Abc_NtkCountChoiceNodes(pNtk) ) + if ( Abc_NtkGetChoiceNum(pNtk) ) { fprintf( pErr, "AIG resynthesis cannot be applied to AIGs with choice nodes.\n" ); return 1; @@ -1816,7 +1813,7 @@ int Abc_CommandRefactor( Abc_Frame_t * pAbc, int argc, char ** argv ) fprintf( pErr, "This command can only be applied to an AIG.\n" ); return 1; } - if ( Abc_NtkCountChoiceNodes(pNtk) ) + if ( Abc_NtkGetChoiceNum(pNtk) ) { fprintf( pErr, "AIG resynthesis cannot be applied to AIGs with choice nodes.\n" ); return 1; @@ -1957,7 +1954,7 @@ int Abc_CommandMiter( Abc_Frame_t * pAbc, int argc, char ** argv ) pArgvNew = argv + util_optind; nArgcNew = argc - util_optind; - if ( !Abc_NtkPrepareCommand( pErr, pNtk, pArgvNew, nArgcNew, &pNtk1, &pNtk2, &fDelete1, &fDelete2 ) ) + if ( !Abc_NtkPrepareTwoNtks( pErr, pNtk, pArgvNew, nArgcNew, &pNtk1, &pNtk2, &fDelete1, &fDelete2 ) ) return 1; // compute the miter @@ -3858,7 +3855,7 @@ int Abc_CommandCec( Abc_Frame_t * pAbc, int argc, char ** argv ) pArgvNew = argv + util_optind; nArgcNew = argc - util_optind; - if ( !Abc_NtkPrepareCommand( pErr, pNtk, pArgvNew, nArgcNew, &pNtk1, &pNtk2, &fDelete1, &fDelete2 ) ) + if ( !Abc_NtkPrepareTwoNtks( pErr, pNtk, pArgvNew, nArgcNew, &pNtk1, &pNtk2, &fDelete1, &fDelete2 ) ) return 1; // perform equivalence checking @@ -3943,7 +3940,7 @@ int Abc_CommandSec( Abc_Frame_t * pAbc, int argc, char ** argv ) pArgvNew = argv + util_optind; nArgcNew = argc - util_optind; - if ( !Abc_NtkPrepareCommand( pErr, pNtk, pArgvNew, nArgcNew, &pNtk1, &pNtk2, &fDelete1, &fDelete2 ) ) + if ( !Abc_NtkPrepareTwoNtks( pErr, pNtk, pArgvNew, nArgcNew, &pNtk1, &pNtk2, &fDelete1, &fDelete2 ) ) return 1; // perform equivalence checking diff --git a/src/base/abc/abc.h b/src/base/abc/abc.h index c779230a..81a1c328 100644 --- a/src/base/abc/abc.h +++ b/src/base/abc/abc.h @@ -476,6 +476,7 @@ extern Abc_Ntk_t * Abc_NtkFraigRestore(); extern void Abc_NtkFraigStoreClean(); /*=== abcFunc.c ==========================================================*/ extern int Abc_NtkSopToBdd( Abc_Ntk_t * pNtk ); +extern DdNode * Abc_ConvertSopToBdd( DdManager * dd, char * pSop ); extern char * Abc_ConvertBddToSop( Extra_MmFlex_t * pMan, DdManager * dd, DdNode * bFuncOn, DdNode * bFuncOnDc, int nFanins, Vec_Str_t * vCube, int fMode ); extern int Abc_NtkBddToSop( Abc_Ntk_t * pNtk ); extern void Abc_NodeBddToCnf( Abc_Obj_t * pNode, Extra_MmFlex_t * pMmMan, Vec_Str_t * vCube, char ** ppSop0, char ** ppSop1 ); @@ -509,6 +510,13 @@ extern char * Abc_NtkLogicStoreName( Abc_Obj_t * pNodeNew, char * pN extern char * Abc_NtkLogicStoreNamePlus( Abc_Obj_t * pNodeNew, char * pNameOld, char * pSuffix ); extern void Abc_NtkCreateCioNamesTable( Abc_Ntk_t * pNtk ); extern void Abc_NtkDupCioNamesTable( Abc_Ntk_t * pNtk, Abc_Ntk_t * pNtkNew ); +extern Vec_Ptr_t * Abc_NodeGetFaninNames( Abc_Obj_t * pNode ); +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 int Abc_NodeCompareNames( Abc_Obj_t ** pp1, Abc_Obj_t ** pp2 ); +extern void Abc_NtkOrderObjsByName( Abc_Ntk_t * pNtk, int fComb ); +extern void Abc_NtkShortNames( Abc_Ntk_t * pNtk ); /*=== abcNetlist.c ==========================================================*/ extern Abc_Ntk_t * Abc_NtkNetlistToLogic( Abc_Ntk_t * pNtk ); extern Abc_Ntk_t * Abc_NtkLogicToNetlist( Abc_Ntk_t * pNtk ); @@ -546,7 +554,6 @@ 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 ); /*=== abcRenode.c ==========================================================*/ extern Abc_Ntk_t * Abc_NtkRenode( Abc_Ntk_t * pNtk, int nThresh, int nFaninMax, int fCnf, int fMulti, int fSimple ); extern DdNode * Abc_NtkRenodeDeriveBdd( DdManager * dd, Abc_Obj_t * pNodeOld, Vec_Ptr_t * vFaninsOld ); @@ -594,8 +601,6 @@ extern void Abc_SopAddCnfToSolver( solver * pSat, char * pClauses, /*=== abcStrash.c ==========================================================*/ extern Abc_Ntk_t * Abc_NtkStrash( Abc_Ntk_t * pNtk, bool fAllNodes, bool fCleanup ); extern Abc_Obj_t * Abc_NodeStrash( Abc_Aig_t * pMan, Abc_Obj_t * pNode ); -extern Abc_Obj_t * Abc_NodeStrashDec( Abc_Aig_t * pMan, Vec_Ptr_t * vFanins, Vec_Int_t * vForm ); -extern int Abc_NodeStrashDecCount( Abc_Aig_t * pMan, Abc_Obj_t * pRoot, Vec_Ptr_t * vFanins, Vec_Int_t * vForm, Vec_Int_t * vLevels, int NodeMax, int LevelMax ); 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 ); @@ -622,13 +627,6 @@ extern void Abc_NtkStopReverseLevels( Abc_Ntk_t * pNtk ); extern void Abc_NodeSetReverseLevel( Abc_Obj_t * pObj, int LevelR ); extern int Abc_NodeReadReverseLevel( Abc_Obj_t * pObj ); extern int Abc_NodeReadRequiredLevel( Abc_Obj_t * pObj ); -/*=== abcTravId.c ==========================================================*/ -extern void Abc_NtkIncrementTravId( Abc_Ntk_t * pNtk ); -extern void Abc_NodeSetTravId( Abc_Obj_t * pObj, int TravId ); -extern void Abc_NodeSetTravIdCurrent( Abc_Obj_t * pObj ); -extern void Abc_NodeSetTravIdPrevious( Abc_Obj_t * pObj ); -extern bool Abc_NodeIsTravIdCurrent( Abc_Obj_t * pObj ); -extern bool Abc_NodeIsTravIdPrevious( Abc_Obj_t * pObj ); /*=== abcUtil.c ==========================================================*/ extern void Abc_NtkIncrementTravId( Abc_Ntk_t * pNtk ); extern int Abc_NtkGetCubeNum( Abc_Ntk_t * pNtk ); @@ -637,28 +635,22 @@ extern int Abc_NtkGetLitFactNum( Abc_Ntk_t * pNtk ); extern int Abc_NtkGetBddNodeNum( Abc_Ntk_t * pNtk ); extern int Abc_NtkGetClauseNum( Abc_Ntk_t * pNtk ); extern double Abc_NtkGetMappedArea( Abc_Ntk_t * pNtk ); +extern int Abc_NtkGetExorNum( Abc_Ntk_t * pNtk ); +extern int Abc_NtkGetChoiceNum( Abc_Ntk_t * pNtk ); extern int Abc_NtkGetFaninMax( Abc_Ntk_t * pNtk ); extern void Abc_NtkCleanCopy( Abc_Ntk_t * pNtk ); extern Abc_Obj_t * Abc_NodeHasUniqueCoFanout( Abc_Obj_t * pNode ); extern bool Abc_NtkLogicHasSimpleCos( Abc_Ntk_t * pNtk ); extern int Abc_NtkLogicMakeSimpleCos( Abc_Ntk_t * pNtk, bool fDuplicate ); extern void Abc_VecObjPushUniqueOrderByLevel( Vec_Ptr_t * p, Abc_Obj_t * pNode ); -extern int Abc_NtkCountExors( Abc_Ntk_t * pNtk ); extern bool Abc_NodeIsExorType( Abc_Obj_t * pNode ); extern bool Abc_NodeIsMuxType( Abc_Obj_t * pNode ); extern Abc_Obj_t * Abc_NodeRecognizeMux( Abc_Obj_t * pNode, Abc_Obj_t ** ppNodeT, Abc_Obj_t ** ppNodeE ); -extern int Abc_NtkCountChoiceNodes( Abc_Ntk_t * pNtk ); -extern int Abc_NtkPrepareCommand( FILE * pErr, Abc_Ntk_t * pNtk, char ** argv, int argc, Abc_Ntk_t ** ppNtk1, Abc_Ntk_t ** ppNtk2, int * pfDelete1, int * pfDelete2 ); +extern int Abc_NtkPrepareTwoNtks( FILE * pErr, Abc_Ntk_t * pNtk, char ** argv, int argc, Abc_Ntk_t ** ppNtk1, Abc_Ntk_t ** ppNtk2, int * pfDelete1, int * pfDelete2 ); extern void Abc_NodeCollectFanins( Abc_Obj_t * pNode, Vec_Ptr_t * vNodes ); extern void Abc_NodeCollectFanouts( Abc_Obj_t * pNode, Vec_Ptr_t * vNodes ); 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 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 ); extern Vec_Int_t * Abc_NtkFanoutCounts( Abc_Ntk_t * pNtk ); extern Vec_Ptr_t * Abc_NtkCollectObjects( Abc_Ntk_t * pNtk ); diff --git a/src/base/abc/abcCheck.c b/src/base/abc/abcCheck.c index 9b9e9ee2..c5f644d2 100644 --- a/src/base/abc/abcCheck.c +++ b/src/base/abc/abcCheck.c @@ -661,8 +661,8 @@ bool Abc_NtkCompareLatches( Abc_Ntk_t * pNtk1, Abc_Ntk_t * pNtk2, int fComb ) ***********************************************************************/ bool Abc_NtkCompareSignals( Abc_Ntk_t * pNtk1, Abc_Ntk_t * pNtk2, int fComb ) { - Abc_NtkAlphaOrderSignals( pNtk1, fComb ); - Abc_NtkAlphaOrderSignals( pNtk2, fComb ); + Abc_NtkOrderObjsByName( pNtk1, fComb ); + Abc_NtkOrderObjsByName( pNtk2, fComb ); if ( !Abc_NtkCompareLatches( pNtk1, pNtk2, fComb ) ) return 0; if ( !Abc_NtkComparePis( pNtk1, pNtk2, fComb ) ) diff --git a/src/base/abc/abcFpga.c b/src/base/abc/abcFpga.c index 2316e934..ad411aa5 100644 --- a/src/base/abc/abcFpga.c +++ b/src/base/abc/abcFpga.c @@ -53,7 +53,7 @@ Abc_Ntk_t * Abc_NtkFpga( Abc_Ntk_t * pNtk, int fRecovery, int fVerbose ) assert( Abc_NtkIsStrash(pNtk) ); // print a warning about choice nodes - if ( Abc_NtkCountChoiceNodes( pNtk ) ) + if ( Abc_NtkGetChoiceNum( pNtk ) ) printf( "Performing FPGA mapping with choices.\n" ); // perform FPGA mapping diff --git a/src/base/abc/abcFraig.c b/src/base/abc/abcFraig.c index 83735e47..ef4746d5 100644 --- a/src/base/abc/abcFraig.c +++ b/src/base/abc/abcFraig.c @@ -267,7 +267,7 @@ Abc_Ntk_t * Abc_NtkFraigTrust( Abc_Ntk_t * pNtk ) Abc_NtkFinalize( pNtk, pNtkNew ); // print a warning about choice nodes - printf( "Warning: The resulting AIG contains %d choice nodes.\n", Abc_NtkCountChoiceNodes( pNtkNew ) ); + printf( "Warning: The resulting AIG contains %d choice nodes.\n", Abc_NtkGetChoiceNum( pNtkNew ) ); // make sure that everything is okay if ( fCheck && !Abc_NtkCheck( pNtkNew ) ) diff --git a/src/base/abc/abcFunc.c b/src/base/abc/abcFunc.c index 44acb699..e5af1829 100644 --- a/src/base/abc/abcFunc.c +++ b/src/base/abc/abcFunc.c @@ -24,7 +24,6 @@ /// DECLARATIONS /// //////////////////////////////////////////////////////////////////////// -static DdNode * Abc_ConvertSopToBdd( DdManager * dd, char * pSop, int nFanins ); static int Abc_ConvertZddToSop( DdManager * dd, DdNode * zCover, char * pSop, int nFanins, Vec_Str_t * vCube, int fPhase ); //////////////////////////////////////////////////////////////////////// @@ -61,7 +60,7 @@ int Abc_NtkSopToBdd( Abc_Ntk_t * pNtk ) Abc_NtkForEachNode( pNtk, pNode, i ) { assert( pNode->pData ); - pNode->pData = Abc_ConvertSopToBdd( dd, pNode->pData, Abc_ObjFaninNum(pNode) ); + pNode->pData = Abc_ConvertSopToBdd( dd, pNode->pData ); if ( pNode->pData == NULL ) { printf( "Abc_NtkSopToBdd: Error while converting SOP into BDD.\n" ); @@ -89,43 +88,37 @@ int Abc_NtkSopToBdd( Abc_Ntk_t * pNtk ) SeeAlso [] ***********************************************************************/ -DdNode * Abc_ConvertSopToBdd( DdManager * dd, char * pSop, int nFanins ) +DdNode * Abc_ConvertSopToBdd( DdManager * dd, char * pSop ) { - DdNode * bCube, * bTemp, * bVar, * bRes; + DdNode * bSum, * bCube, * bTemp, * bVar; char * pCube; - int i, c; - - bRes = Cudd_Not(dd->one); Cudd_Ref( bRes ); - for ( c = 0; ; c++ ) + int nVars, Value, v; + // start the cover + nVars = Abc_SopGetVarNum(pSop); + // check the logic function of the node + bSum = Cudd_ReadLogicZero(dd); Cudd_Ref( bSum ); + Abc_SopForEachCube( pSop, nVars, pCube ) { - // get the cube - pCube = pSop + c * (nFanins + 3); - if ( *pCube == 0 ) - break; - // construct BDD for the cube - bCube = dd->one; Cudd_Ref( bCube ); - for ( i = 0; i < nFanins; i++ ) + bCube = Cudd_ReadOne(dd); Cudd_Ref( bCube ); + Abc_CubeForEachVar( pCube, Value, v ) { - if ( pCube[i] == '0' ) - bVar = Cudd_Not( dd->vars[i] ); - else if ( pCube[i] == '1' ) - bVar = dd->vars[i]; + if ( Value == '0' ) + bVar = Cudd_Not( Cudd_bddIthVar( dd, v ) ); + else if ( Value == '1' ) + bVar = Cudd_bddIthVar( dd, v ); else continue; bCube = Cudd_bddAnd( dd, bTemp = bCube, bVar ); Cudd_Ref( bCube ); Cudd_RecursiveDeref( dd, bTemp ); } - bRes = Cudd_bddOr( dd, bTemp = bRes, bCube ); Cudd_Ref( bRes ); + bSum = Cudd_bddOr( dd, bTemp = bSum, bCube ); Cudd_Ref( bSum ); Cudd_RecursiveDeref( dd, bTemp ); Cudd_RecursiveDeref( dd, bCube ); } - // decide if we need to complement the result - pCube = pSop + nFanins + 1; - assert( *pCube == '0' || *pCube == '1' ); - if ( *pCube == '0' ) - bRes = Cudd_Not(bRes); - Cudd_Deref( bRes ); - return bRes; + // complement the result if necessary + bSum = Cudd_NotCond( bSum, !Abc_SopGetPhase(pSop) ); + Cudd_Deref( bSum ); + return bSum; } /**Function************************************************************* @@ -171,7 +164,7 @@ void Abc_NtkLogicMakeDirectSops( Abc_Ntk_t * pNtk ) Abc_NtkForEachNode( pNtk, pNode, i ) if ( Abc_SopIsComplement(pNode->pData) ) { - bFunc = Abc_ConvertSopToBdd( dd, pNode->pData, Abc_ObjFaninNum(pNode) ); Cudd_Ref( bFunc ); + bFunc = Abc_ConvertSopToBdd( dd, pNode->pData ); Cudd_Ref( bFunc ); pNode->pData = Abc_ConvertBddToSop( pNtk->pManFunc, dd, bFunc, bFunc, Abc_ObjFaninNum(pNode), vCube, 1 ); Cudd_RecursiveDeref( dd, bFunc ); assert( !Abc_SopIsComplement(pNode->pData) ); @@ -340,7 +333,7 @@ char * Abc_ConvertBddToSop( Extra_MmFlex_t * pMan, DdManager * dd, DdNode * bFun // verify if ( fVerify ) { - bFuncNew = Abc_ConvertSopToBdd( dd, pSop, nFanins ); Cudd_Ref( bFuncNew ); + bFuncNew = Abc_ConvertSopToBdd( dd, pSop ); Cudd_Ref( bFuncNew ); if ( bFuncOn == bFuncOnDc ) { if ( bFuncNew != bFuncOn ) diff --git a/src/base/abc/abcMap.c b/src/base/abc/abcMap.c index f847aa40..28853c8d 100644 --- a/src/base/abc/abcMap.c +++ b/src/base/abc/abcMap.c @@ -79,7 +79,7 @@ Abc_Ntk_t * Abc_NtkMap( Abc_Ntk_t * pNtk, double DelayTarget, int fRecovery, int } // print a warning about choice nodes - if ( Abc_NtkCountChoiceNodes( pNtk ) ) + if ( Abc_NtkGetChoiceNum( pNtk ) ) printf( "Performing mapping with choices.\n" ); // perform the mapping @@ -442,7 +442,7 @@ Abc_Ntk_t * Abc_NtkSuperChoice( Abc_Ntk_t * pNtk ) } // print a warning about choice nodes - if ( Abc_NtkCountChoiceNodes( pNtk ) ) + if ( Abc_NtkGetChoiceNum( pNtk ) ) printf( "Performing mapping with choices.\n" ); // perform the mapping diff --git a/src/base/abc/abcNames.c b/src/base/abc/abcNames.c index 088dc855..2bf6461b 100644 --- a/src/base/abc/abcNames.c +++ b/src/base/abc/abcNames.c @@ -269,6 +269,233 @@ void Abc_NtkDupCioNamesTable( Abc_Ntk_t * pNtk, Abc_Ntk_t * pNtkNew ) Abc_NtkLogicStoreName( Abc_NtkLatch(pNtkNew,i), Abc_ObjName(pObj) ); } +/**Function************************************************************* + + Synopsis [Gets fanin node names.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Vec_Ptr_t * Abc_NodeGetFaninNames( Abc_Obj_t * pNode ) +{ + Vec_Ptr_t * vNodes; + Abc_Obj_t * pFanin; + int i; + vNodes = Vec_PtrAlloc( 100 ); + Abc_ObjForEachFanin( pNode, pFanin, i ) + Vec_PtrPush( vNodes, util_strsav(Abc_ObjName(pFanin)) ); + return vNodes; +} + +/**Function************************************************************* + + Synopsis [Gets fanin node names.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +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 ); +} + +/**Function************************************************************* + + Synopsis [Collects the CI or CO names.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +char ** Abc_NtkCollectCioNames( Abc_Ntk_t * pNtk, int fCollectCos ) +{ + Abc_Obj_t * pObj; + char ** ppNames; + int i; + if ( fCollectCos ) + { + ppNames = ALLOC( char *, Abc_NtkCoNum(pNtk) ); + Abc_NtkForEachCo( pNtk, pObj, i ) + ppNames[i] = Abc_ObjName(pObj); + } + else + { + ppNames = ALLOC( char *, Abc_NtkCiNum(pNtk) ); + Abc_NtkForEachCi( pNtk, pObj, i ) + ppNames[i] = Abc_ObjName(pObj); + } + return ppNames; +} + +/**Function************************************************************* + + Synopsis [Procedure used for sorting the nodes in decreasing order of levels.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Abc_NodeCompareNames( Abc_Obj_t ** pp1, Abc_Obj_t ** pp2 ) +{ + int Diff = strcmp( (char *)(*pp1)->pCopy, (char *)(*pp2)->pCopy ); + if ( Diff < 0 ) + return -1; + if ( Diff > 0 ) + return 1; + return 0; +} + +/**Function************************************************************* + + Synopsis [Orders PIs/POs/latches alphabetically.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Abc_NtkOrderObjsByName( Abc_Ntk_t * pNtk, int fComb ) +{ + Abc_Obj_t * pObj; + int i; + // temporarily store the names in the copy field + Abc_NtkForEachPi( pNtk, pObj, i ) + pObj->pCopy = (Abc_Obj_t *)Abc_ObjName(pObj); + Abc_NtkForEachPo( pNtk, pObj, i ) + pObj->pCopy = (Abc_Obj_t *)Abc_ObjName(pObj); + Abc_NtkForEachLatch( pNtk, pObj, i ) + pObj->pCopy = (Abc_Obj_t *)Abc_ObjName(pObj); + // order objects alphabetically + qsort( pNtk->vCis->pArray, pNtk->nPis, sizeof(Abc_Obj_t *), + (int (*)(const void *, const void *)) Abc_NodeCompareNames ); + qsort( pNtk->vCos->pArray, pNtk->nPos, sizeof(Abc_Obj_t *), + (int (*)(const void *, const void *)) Abc_NodeCompareNames ); + // if the comparison if combinational (latches as PIs/POs), order them too + if ( fComb ) + { + qsort( pNtk->vLats->pArray, pNtk->nLatches, sizeof(Abc_Obj_t *), + (int (*)(const void *, const void *)) Abc_NodeCompareNames ); + // add latches to make COs + Abc_NtkForEachLatch( pNtk, pObj, i ) + { + Vec_PtrWriteEntry( pNtk->vCis, pNtk->nPis + i, pObj ); + Vec_PtrWriteEntry( pNtk->vCos, pNtk->nPos + i, pObj ); + } + } + // clean the copy fields + Abc_NtkForEachPi( pNtk, pObj, i ) + pObj->pCopy = NULL; + Abc_NtkForEachPo( pNtk, pObj, i ) + pObj->pCopy = NULL; + Abc_NtkForEachLatch( pNtk, pObj, i ) + pObj->pCopy = NULL; +} + +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Abc_NtkShortNames( Abc_Ntk_t * pNtk ) +{ + stmm_table * tObj2NameNew; + Abc_Obj_t * pObj; + char Buffer[100]; + char * pNameNew; + int Length, i; + + tObj2NameNew = stmm_init_table(stmm_ptrcmp, stmm_ptrhash); + // create new names and add them to the table + Length = Extra_Base10Log( Abc_NtkPiNum(pNtk) ); + Abc_NtkForEachPi( pNtk, pObj, i ) + { + sprintf( Buffer, "pi%0*d", Length, i ); + pNameNew = Abc_NtkRegisterName( pNtk, Buffer ); + stmm_insert( tObj2NameNew, (char *)pObj, pNameNew ); + } + // create new names and add them to the table + Length = Extra_Base10Log( Abc_NtkPoNum(pNtk) ); + Abc_NtkForEachPo( pNtk, pObj, i ) + { + sprintf( Buffer, "po%0*d", Length, i ); + pNameNew = Abc_NtkRegisterName( pNtk, Buffer ); + stmm_insert( tObj2NameNew, (char *)pObj, pNameNew ); + } + // create new names and add them to the table + Length = Extra_Base10Log( Abc_NtkLatchNum(pNtk) ); + Abc_NtkForEachLatch( pNtk, pObj, i ) + { + sprintf( Buffer, "lat%0*d", Length, i ); + pNameNew = Abc_NtkRegisterName( pNtk, Buffer ); + stmm_insert( tObj2NameNew, (char *)pObj, pNameNew ); + } + stmm_free_table( pNtk->tObj2Name ); + pNtk->tObj2Name = tObj2NameNew; +} + //////////////////////////////////////////////////////////////////////// /// END OF FILE /// //////////////////////////////////////////////////////////////////////// diff --git a/src/base/abc/abcNetlist.c b/src/base/abc/abcNetlist.c index f7eb0804..77fbeb38 100644 --- a/src/base/abc/abcNetlist.c +++ b/src/base/abc/abcNetlist.c @@ -313,7 +313,7 @@ Abc_Ntk_t * Abc_NtkAigToLogicSopBench( Abc_Ntk_t * pNtk ) Vec_Ptr_t * vNodes; int i, k; assert( Abc_NtkIsStrash(pNtk) ); - if ( Abc_NtkCountChoiceNodes(pNtk) ) + if ( Abc_NtkGetChoiceNum(pNtk) ) printf( "Warning: Choice nodes are skipped.\n" ); // start the network pNtkNew = Abc_NtkStartFrom( pNtk, ABC_TYPE_LOGIC, ABC_FUNC_SOP ); diff --git a/src/base/abc/abcPrint.c b/src/base/abc/abcPrint.c index 4f8b4aeb..41b9288e 100644 --- a/src/base/abc/abcPrint.c +++ b/src/base/abc/abcPrint.c @@ -19,7 +19,7 @@ ***********************************************************************/ #include "abc.h" -#include "ft.h" +#include "dec.h" //////////////////////////////////////////////////////////////////////// /// DECLARATIONS /// @@ -60,9 +60,9 @@ void Abc_NtkPrintStats( FILE * pFile, Abc_Ntk_t * pNtk, int fFactored ) else if ( Abc_NtkIsStrash(pNtk) ) { fprintf( pFile, " and = %5d", Abc_NtkNodeNum(pNtk) ); - if ( Num = Abc_NtkCountChoiceNodes(pNtk) ) + if ( Num = Abc_NtkGetChoiceNum(pNtk) ) fprintf( pFile, " (choice = %d)", Num ); - if ( Num = Abc_NtkCountExors(pNtk) ) + if ( Num = Abc_NtkGetExorNum(pNtk) ) fprintf( pFile, " (exor = %d)", Num ); } else if ( Abc_NtkIsSeq(pNtk) ) @@ -332,7 +332,7 @@ void Abc_NtkPrintFactor( FILE * pFile, Abc_Ntk_t * pNtk, int fUseRealNames ) ***********************************************************************/ void Abc_NodePrintFactor( FILE * pFile, Abc_Obj_t * pNode, int fUseRealNames ) { - Vec_Int_t * vFactor; + Dec_Graph_t * pGraph; Vec_Ptr_t * vNamesIn; if ( Abc_ObjIsCo(pNode) ) pNode = Abc_ObjFanin0(pNode); @@ -347,16 +347,16 @@ void Abc_NodePrintFactor( FILE * pFile, Abc_Obj_t * pNode, int fUseRealNames ) return; } assert( Abc_ObjIsNode(pNode) ); - vFactor = Ft_Factor( pNode->pData ); + pGraph = Dec_Factor( pNode->pData ); if ( fUseRealNames ) { vNamesIn = Abc_NodeGetFaninNames(pNode); - Ft_FactorPrint( stdout, vFactor, (char **)vNamesIn->pArray, Abc_ObjName(pNode) ); + Dec_GraphPrint( stdout, pGraph, (char **)vNamesIn->pArray, Abc_ObjName(pNode) ); Abc_NodeFreeNames( vNamesIn ); } else - Ft_FactorPrint( stdout, vFactor, (char **)NULL, Abc_ObjName(pNode) ); - Vec_IntFree( vFactor ); + Dec_GraphPrint( stdout, pGraph, (char **)NULL, Abc_ObjName(pNode) ); + Dec_GraphFree( pGraph ); } diff --git a/src/base/abc/abcReconv.c b/src/base/abc/abcReconv.c index ea662799..766c14f3 100644 --- a/src/base/abc/abcReconv.c +++ b/src/base/abc/abcReconv.c @@ -19,7 +19,6 @@ ***********************************************************************/ #include "abc.h" -#include "ft.h" //////////////////////////////////////////////////////////////////////// /// DECLARATIONS /// diff --git a/src/base/abc/abcRefactor.c b/src/base/abc/abcRefactor.c index 1524489d..791d2d53 100644 --- a/src/base/abc/abcRefactor.c +++ b/src/base/abc/abcRefactor.c @@ -19,7 +19,7 @@ ***********************************************************************/ #include "abc.h" -#include "ft.h" +#include "dec.h" //////////////////////////////////////////////////////////////////////// /// DECLARATIONS /// @@ -34,10 +34,8 @@ struct Abc_ManRef_t_ int fVerbose; // the verbosity flag // internal data structures DdManager * dd; // the BDD manager -// Vec_Int_t * vReqTimes; // required times for each node Vec_Str_t * vCube; // temporary Vec_Int_t * vForm; // temporary - Vec_Int_t * vLevNums; // temporary Vec_Ptr_t * vVisited; // temporary Vec_Ptr_t * vLeaves; // temporary // node statistics @@ -60,7 +58,7 @@ struct Abc_ManRef_t_ static void Abc_NtkManRefPrintStats( Abc_ManRef_t * p ); static Abc_ManRef_t * Abc_NtkManRefStart( int nNodeSizeMax, int nConeSizeMax, bool fUseDcs, bool fVerbose ); static void Abc_NtkManRefStop( Abc_ManRef_t * p ); -static Vec_Int_t * Abc_NodeRefactor( Abc_ManRef_t * p, Abc_Obj_t * pNode, Vec_Ptr_t * vFanins, bool fUseZeros, bool fUseDcs, bool fVerbose ); +static Dec_Graph_t * Abc_NodeRefactor( Abc_ManRef_t * p, Abc_Obj_t * pNode, Vec_Ptr_t * vFanins, bool fUseZeros, bool fUseDcs, bool fVerbose ); //////////////////////////////////////////////////////////////////////// /// FUNCTION DEFITIONS /// @@ -88,11 +86,11 @@ int Abc_NtkRefactor( Abc_Ntk_t * pNtk, int nNodeSizeMax, int nConeSizeMax, bool ProgressBar * pProgress; Abc_ManRef_t * pManRef; Abc_ManCut_t * pManCut; + Dec_Graph_t * pFForm; Vec_Ptr_t * vFanins; - Vec_Int_t * vForm; Abc_Obj_t * pNode; - int i, nNodes; int clk, clkStart = clock(); + int i, nNodes; assert( Abc_NtkIsStrash(pNtk) ); // cleanup the AIG @@ -109,27 +107,27 @@ int Abc_NtkRefactor( Abc_Ntk_t * pNtk, int nNodeSizeMax, int nConeSizeMax, bool Abc_NtkForEachNode( pNtk, pNode, i ) { Extra_ProgressBarUpdate( pProgress, i, NULL ); - // stop if all nodes have been tried once - if ( i >= nNodes ) - break; // skip the constant node if ( Abc_NodeIsConst(pNode) ) continue; + // stop if all nodes have been tried once + if ( i >= nNodes ) + break; // compute a reconvergence-driven cut clk = clock(); vFanins = Abc_NodeFindCut( pManCut, pNode, fUseDcs ); pManRef->timeCut += clock() - clk; // evaluate this cut clk = clock(); - vForm = Abc_NodeRefactor( pManRef, pNode, vFanins, fUseZeros, fUseDcs, fVerbose ); + pFForm = Abc_NodeRefactor( pManRef, pNode, vFanins, fUseZeros, fUseDcs, fVerbose ); pManRef->timeRes += clock() - clk; - if ( vForm == NULL ) + if ( pFForm == NULL ) continue; // acceptable replacement found, update the graph clk = clock(); - Abc_NodeUpdate( pNode, vFanins, vForm, pManRef->nLastGain ); + Dec_GraphUpdateNetwork( pNode, pFForm, pManRef->nLastGain ); pManRef->timeNtk += clock() - clk; - Vec_IntFree( vForm ); + Dec_GraphFree( pFForm ); } Extra_ProgressBarStop( pProgress ); pManRef->timeTotal = clock() - clkStart; @@ -161,40 +159,33 @@ pManRef->timeTotal = clock() - clkStart; SeeAlso [] ***********************************************************************/ -Vec_Int_t * Abc_NodeRefactor( Abc_ManRef_t * p, Abc_Obj_t * pNode, Vec_Ptr_t * vFanins, bool fUseZeros, bool fUseDcs, bool fVerbose ) +Dec_Graph_t * Abc_NodeRefactor( Abc_ManRef_t * p, Abc_Obj_t * pNode, Vec_Ptr_t * vFanins, bool fUseZeros, bool fUseDcs, bool fVerbose ) { int fVeryVerbose = 0; Abc_Obj_t * pFanin; - Vec_Int_t * vForm; - DdNode * bNodeFunc, * bNodeDc, * bNodeOn, * bNodeOnDc; + Dec_Graph_t * pFForm; + DdNode * bNodeFunc; + int nNodesSaved, nNodesAdded, i, clk; char * pSop; - int nBddNodes, nFtNodes, nNodesSaved, nNodesAdded; - int i, Required, clk; p->nNodesConsidered++; - // get the required level of this node - Required = Abc_NodeReadRequiredLevel( pNode ); - // get the function of the cut clk = clock(); bNodeFunc = Abc_NodeConeBdd( p->dd, p->dd->vars, pNode, vFanins, p->vVisited ); Cudd_Ref( bNodeFunc ); p->timeBdd += clock() - clk; - nBddNodes = Cudd_DagSize(bNodeFunc); // if don't-care are used, transform the function into ISOP if ( fUseDcs ) { + DdNode * bNodeDc, * bNodeOn, * bNodeOnDc; int nMints, nMintsDc; - clk = clock(); // get the don't-cares bNodeDc = Abc_NodeConeDcs( p->dd, p->dd->vars + vFanins->nSize, p->dd->vars, p->vLeaves, vFanins, p->vVisited ); Cudd_Ref( bNodeDc ); - nMints = (1 << vFanins->nSize); nMintsDc = (int)Cudd_CountMinterm( p->dd, bNodeDc, vFanins->nSize ); // printf( "Percentage of minterms = %5.2f.\n", 100.0 * nMintsDc / nMints ); - // get the ISF bNodeOn = Cudd_bddAnd( p->dd, bNodeFunc, Cudd_Not(bNodeDc) ); Cudd_Ref( bNodeOn ); bNodeOnDc = Cudd_bddOr ( p->dd, bNodeFunc, bNodeDc ); Cudd_Ref( bNodeOnDc ); @@ -207,58 +198,52 @@ clk = clock(); p->timeDcs += clock() - clk; } -//Extra_bddPrint( p->dd, bNodeFunc ); printf( "\n" ); // always accept the case of constant node if ( Cudd_IsConstant(bNodeFunc) ) { p->nLastGain = Abc_NodeMffcSize( pNode ); p->nNodesGained += p->nLastGain; p->nNodesRefactored++; - // get the constant node -// pFanin = Abc_ObjNotCond( Abc_AigConst1(pNode->pNtk->pManFunc), Cudd_IsComplement(bNodeFunc) ); -// Abc_AigReplace( pNode->pNtk->pManFunc, pNode, pFanin ); -// Cudd_RecursiveDeref( p->dd, bNodeFunc ); -//printf( "Gain = %d.\n", p->nLastGain ); Cudd_RecursiveDeref( p->dd, bNodeFunc ); - return Ft_FactorConst( !Cudd_IsComplement(bNodeFunc) ); + if ( Cudd_IsComplement(bNodeFunc) ) + return Dec_GraphCreateConst0(); + return Dec_GraphCreateConst1(); } // get the SOP of the cut clk = clock(); pSop = Abc_ConvertBddToSop( NULL, p->dd, bNodeFunc, bNodeFunc, vFanins->nSize, p->vCube, -1 ); p->timeSop += clock() - clk; - Cudd_RecursiveDeref( p->dd, bNodeFunc ); // get the factored form clk = clock(); - vForm = Ft_Factor( pSop ); -p->timeFact += clock() - clk; - nFtNodes = Ft_FactorGetNumNodes( vForm ); + pFForm = Dec_Factor( pSop ); free( pSop ); -//Ft_FactorPrint( stdout, vForm, NULL, NULL ); +p->timeFact += clock() - clk; // mark the fanin boundary - // (can mark only essential fanins, belonging to bNodeFunc!!!) + // (can mark only essential fanins, belonging to bNodeFunc!) Vec_PtrForEachEntry( vFanins, pFanin, i ) pFanin->vFanouts.nSize++; - // label MFFC with current traversal ID Abc_NtkIncrementTravId( pNode->pNtk ); nNodesSaved = Abc_NodeMffcLabel( pNode ); - - // unmark the fanin boundary + // unmark the fanin boundary and set the fanins as leaves in the form Vec_PtrForEachEntry( vFanins, pFanin, i ) + { pFanin->vFanouts.nSize--; + Dec_GraphNode(pFForm, i)->pFunc = pFanin; + } // detect how many new nodes will be added (while taking into account reused nodes) clk = clock(); - nNodesAdded = Abc_NodeStrashDecCount( pNode->pNtk->pManFunc, pNode, vFanins, vForm, - p->vLevNums, nNodesSaved, Required ); + nNodesAdded = Dec_GraphToNetworkCount( pNode, pFForm, nNodesSaved, Abc_NodeReadRequiredLevel(pNode) ); p->timeEval += clock() - clk; // quit if there is no improvement if ( nNodesAdded == -1 || nNodesAdded == nNodesSaved && !fUseZeros ) { - Vec_IntFree( vForm ); + Cudd_RecursiveDeref( p->dd, bNodeFunc ); + Dec_GraphFree( pFForm ); return NULL; } @@ -272,14 +257,15 @@ p->timeEval += clock() - clk; { printf( "Node %6s : ", Abc_ObjName(pNode) ); printf( "Cone = %2d. ", vFanins->nSize ); - printf( "BDD = %2d. ", nBddNodes ); - printf( "FF = %2d. ", nFtNodes ); + printf( "BDD = %2d. ", Cudd_DagSize(bNodeFunc) ); + printf( "FF = %2d. ", 1 + Dec_GraphNodeNum(pFForm) ); printf( "MFFC = %2d. ", nNodesSaved ); printf( "Add = %2d. ", nNodesAdded ); printf( "GAIN = %2d. ", p->nLastGain ); printf( "\n" ); } - return vForm; + Cudd_RecursiveDeref( p->dd, bNodeFunc ); + return pFForm; } @@ -300,7 +286,6 @@ Abc_ManRef_t * Abc_NtkManRefStart( int nNodeSizeMax, int nConeSizeMax, bool fUse p = ALLOC( Abc_ManRef_t, 1 ); memset( p, 0, sizeof(Abc_ManRef_t) ); p->vCube = Vec_StrAlloc( 100 ); - p->vLevNums = Vec_IntAlloc( 100 ); p->vVisited = Vec_PtrAlloc( 100 ); p->nNodeSizeMax = nNodeSizeMax; p->nConeSizeMax = nConeSizeMax; @@ -328,9 +313,7 @@ Abc_ManRef_t * Abc_NtkManRefStart( int nNodeSizeMax, int nConeSizeMax, bool fUse void Abc_NtkManRefStop( Abc_ManRef_t * p ) { Extra_StopManager( p->dd ); -// Vec_IntFree( p->vReqTimes ); Vec_PtrFree( p->vVisited ); - Vec_IntFree( p->vLevNums ); Vec_StrFree( p->vCube ); free( p ); } diff --git a/src/base/abc/abcRefs.c b/src/base/abc/abcRefs.c index 5cfa23ba..47618bf4 100644 --- a/src/base/abc/abcRefs.c +++ b/src/base/abc/abcRefs.c @@ -221,37 +221,6 @@ int Abc_NodeRefDerefStop( Abc_Obj_t * pNode, bool fReference ) return Counter; } -/**Function************************************************************* - - Synopsis [Replaces MFFC of the node by the new factored form.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -void Abc_NodeUpdate( Abc_Obj_t * pNode, Vec_Ptr_t * vFanins, Vec_Int_t * vForm, int nGain ) -{ - Abc_Ntk_t * pNtk = pNode->pNtk; - Abc_Obj_t * pNodeNew; - int nNodesNew, nNodesOld; - nNodesOld = Abc_NtkNodeNum(pNtk); - // create the new structure of nodes - assert( vForm->nSize == 1 || Vec_PtrSize(vFanins) < Vec_IntSize(vForm) ); - pNodeNew = Abc_NodeStrashDec( pNtk->pManFunc, vFanins, vForm ); - // in some cases, the new node may have a minor redundancy - // (has to do with the precomputed subgraph library) - if ( !Abc_AigNodeIsAcyclic( Abc_ObjRegular(pNodeNew), pNode ) ) - return; - // remove the old nodes - Abc_AigReplace( pNtk->pManFunc, pNode, pNodeNew ); - // compare the gains - nNodesNew = Abc_NtkNodeNum(pNtk); - assert( nGain <= nNodesOld - nNodesNew ); -} - //////////////////////////////////////////////////////////////////////// /// END OF FILE /// //////////////////////////////////////////////////////////////////////// diff --git a/src/base/abc/abcRenode.c b/src/base/abc/abcRenode.c index b17e2394..c77c0d70 100644 --- a/src/base/abc/abcRenode.c +++ b/src/base/abc/abcRenode.c @@ -60,7 +60,7 @@ Abc_Ntk_t * Abc_NtkRenode( Abc_Ntk_t * pNtk, int nThresh, int nFaninMax, int fCn assert( nFaninMax > 1 ); // print a warning about choice nodes - if ( Abc_NtkCountChoiceNodes( pNtk ) ) + if ( Abc_NtkGetChoiceNum( pNtk ) ) printf( "Warning: The choice nodes in the AIG are removed by renoding.\n" ); // define the boundary diff --git a/src/base/abc/abcRewrite.c b/src/base/abc/abcRewrite.c index f28aaa42..75fe1627 100644 --- a/src/base/abc/abcRewrite.c +++ b/src/base/abc/abcRewrite.c @@ -20,7 +20,7 @@ #include "abc.h" #include "rwr.h" -#include "ft.h" +#include "dec.h" //////////////////////////////////////////////////////////////////////// /// DECLARATIONS /// @@ -85,13 +85,12 @@ Rwr_ManAddTimeCuts( pManRwr, clock() - clk ); nGain = Rwr_NodeRewrite( pManRwr, pManCut, pNode, fUseZeros ); if ( nGain > 0 || nGain == 0 && fUseZeros ) { - Vec_Int_t * vForm = Rwr_ManReadDecs(pManRwr); - Vec_Ptr_t * vFanins = Rwr_ManReadFanins(pManRwr); - int fCompl = Rwr_ManReadCompl(pManRwr); + Dec_Graph_t * pGraph = Rwr_ManReadDecs(pManRwr); + int fCompl = Rwr_ManReadCompl(pManRwr); // complement the FF if needed - if ( fCompl ) Ft_FactorComplement( vForm ); - Abc_NodeUpdate( pNode, vFanins, vForm, nGain ); - if ( fCompl ) Ft_FactorComplement( vForm ); + if ( fCompl ) Dec_GraphComplement( pGraph ); + Dec_GraphUpdateNetwork( pNode, pGraph, nGain ); + if ( fCompl ) Dec_GraphComplement( pGraph ); } } Extra_ProgressBarStop( pProgress ); diff --git a/src/base/abc/abcShow.c b/src/base/abc/abcShow.c index a3e522cb..ee59cf43 100644 --- a/src/base/abc/abcShow.c +++ b/src/base/abc/abcShow.c @@ -55,7 +55,7 @@ void Abc_NodeShowBdd( Abc_Obj_t * pNode ) char * pNameOut; assert( Abc_NtkIsBddLogic(pNode->pNtk) ); - // create the file names + // create the file name Abc_ShowGetFileName( Abc_ObjName(pNode), FileNameDot ); // check that the file can be opened if ( (pFile = fopen( FileNameDot, "w" )) == NULL ) @@ -96,7 +96,7 @@ void Abc_NtkShowAig( Abc_Ntk_t * pNtk ) int i; assert( Abc_NtkIsStrash(pNtk) ); - // create the file names + // create the file name Abc_ShowGetFileName( pNtk->pName, FileNameDot ); // check that the file can be opened if ( (pFile = fopen( FileNameDot, "w" )) == NULL ) @@ -119,7 +119,7 @@ void Abc_NtkShowAig( Abc_Ntk_t * pNtk ) /**Function************************************************************* - Synopsis [Visualizes reconvergence driven cut at the node.] + Synopsis [Visualizes a reconvergence driven cut at the node.] Description [] @@ -158,7 +158,7 @@ void Abc_NodeShowCut( Abc_Obj_t * pNode, int nNodeSizeMax, int nConeSizeMax ) Vec_PtrForEachEntry( vNodesTfo, pTemp, i ) Vec_PtrPushUnique( vInside, pTemp ); - // create the file names + // create the file name Abc_ShowGetFileName( Abc_ObjName(pNode), FileNameDot ); // check that the file can be opened if ( (pFile = fopen( FileNameDot, "w" )) == NULL ) diff --git a/src/base/abc/abcStrash.c b/src/base/abc/abcStrash.c index 0a28c3c1..935f1300 100644 --- a/src/base/abc/abcStrash.c +++ b/src/base/abc/abcStrash.c @@ -20,7 +20,7 @@ #include "abc.h" #include "extra.h" -#include "ft.h" +#include "dec.h" //////////////////////////////////////////////////////////////////////// /// DECLARATIONS /// @@ -59,7 +59,7 @@ Abc_Ntk_t * Abc_NtkStrash( Abc_Ntk_t * pNtk, bool fAllNodes, bool fCleanup ) if ( Abc_NtkIsBddLogic(pNtk) ) Abc_NtkBddToSop(pNtk); // print warning about choice nodes - if ( Abc_NtkCountChoiceNodes( pNtk ) ) + if ( Abc_NtkGetChoiceNum( pNtk ) ) printf( "Warning: The choice nodes in the initial AIG are removed by strashing.\n" ); // perform strashing pNtkAig = Abc_NtkStartFrom( pNtk, ABC_TYPE_STRASH, ABC_FUNC_AIG ); @@ -188,9 +188,6 @@ Abc_Obj_t * Abc_NodeStrash( Abc_Aig_t * pMan, Abc_Obj_t * pNode ) // consider the case when the graph is an AIG if ( Abc_NtkIsStrash(pNode->pNtk) ) { -// Abc_Obj_t * pChild0, * pChild1; -// pChild0 = Abc_ObjFanin0(pNode); -// pChild1 = Abc_ObjFanin1(pNode); if ( Abc_NodeIsConst(pNode) ) return Abc_AigConst1(pMan); return Abc_AigAnd( pMan, Abc_ObjChild0Copy(pNode), Abc_ObjChild1Copy(pNode) ); @@ -202,14 +199,9 @@ Abc_Obj_t * Abc_NodeStrash( Abc_Aig_t * pMan, Abc_Obj_t * pNode ) else pSop = pNode->pData; - // consider the cconstant node + // consider the constant node if ( Abc_NodeIsConst(pNode) ) - { - // check if the SOP is constant - if ( Abc_SopIsConst1(pSop) ) - return Abc_AigConst1(pMan); - return Abc_ObjNot( Abc_AigConst1(pMan) ); - } + return Abc_ObjNotCond( Abc_AigConst1(pMan), Abc_SopIsConst0(pSop) ); // decide when to use factoring if ( fUseFactor && Abc_ObjFaninNum(pNode) > 2 && Abc_SopGetCubeNum(pSop) > 1 ) @@ -273,199 +265,21 @@ Abc_Obj_t * Abc_NodeStrashSop( Abc_Aig_t * pMan, Abc_Obj_t * pNode, char * pSop ***********************************************************************/ Abc_Obj_t * Abc_NodeStrashFactor( Abc_Aig_t * pMan, Abc_Obj_t * pRoot, char * pSop ) { - Vec_Int_t * vForm; - Vec_Ptr_t * vAnds; - Abc_Obj_t * pAnd, * pFanin; + Dec_Graph_t * pFForm; + Dec_Node_t * pNode; + Abc_Obj_t * pAnd; int i; - // derive the factored form - vForm = Ft_Factor( pSop ); + // perform factoring + pFForm = Dec_Factor( pSop ); // collect the fanins - vAnds = Vec_PtrAlloc( 20 ); - Abc_ObjForEachFanin( pRoot, pFanin, i ) - Vec_PtrPush( vAnds, pFanin->pCopy ); + Dec_GraphForEachLeaf( pFForm, pNode, i ) + pNode->pFunc = Abc_ObjFanin(pRoot,i)->pCopy; // perform strashing - pAnd = Abc_NodeStrashDec( pMan, vAnds, vForm ); - Vec_PtrFree( vAnds ); - Vec_IntFree( vForm ); - return pAnd; -} - -/**Function************************************************************* - - Synopsis [Strashes the factored form into the AIG.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -Abc_Obj_t * Abc_NodeStrashDec( Abc_Aig_t * pMan, Vec_Ptr_t * vFanins, Vec_Int_t * vForm ) -{ - Abc_Obj_t * pAnd, * pAnd0, * pAnd1; - Ft_Node_t * pFtNode; - int i, nVars; - - // sanity checks - nVars = Ft_FactorGetNumVars( vForm ); - assert( nVars >= 0 ); - assert( vForm->nSize > nVars ); - - // check for constant function - pFtNode = Ft_NodeRead( vForm, 0 ); - if ( pFtNode->fConst ) - return Abc_ObjNotCond( Abc_AigConst1(pMan), pFtNode->fCompl ); - assert( nVars == vFanins->nSize ); - - // compute the function of other nodes - for ( i = nVars; i < vForm->nSize; i++ ) - { - pFtNode = Ft_NodeRead( vForm, i ); - pAnd0 = Abc_ObjNotCond( vFanins->pArray[pFtNode->iFanin0], pFtNode->fCompl0 ); - pAnd1 = Abc_ObjNotCond( vFanins->pArray[pFtNode->iFanin1], pFtNode->fCompl1 ); - pAnd = Abc_AigAnd( pMan, pAnd0, pAnd1 ); - Vec_PtrPush( vFanins, pAnd ); -//printf( "Adding " ); Abc_AigPrintNode( pAnd ); - } - assert( vForm->nSize = vFanins->nSize ); - - // complement the result if necessary - pFtNode = Ft_NodeReadLast( vForm ); - pAnd = Abc_ObjNotCond( pAnd, pFtNode->fCompl ); + pAnd = Dec_GraphToNetwork( pMan, pFForm ); + Dec_GraphFree( pFForm ); return pAnd; } -/**Function************************************************************* - - Synopsis [Counts the number of new nodes added when using this factored form,] - - Description [Returns NodeMax + 1 if the number of nodes and levels exceeded - the given limit or the number of levels exceeded the maximum allowed level.] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -int Abc_NodeStrashDecCount( Abc_Aig_t * pMan, Abc_Obj_t * pRoot, Vec_Ptr_t * vFanins, Vec_Int_t * vForm, Vec_Int_t * vLevels, int NodeMax, int LevelMax ) -{ - Abc_Obj_t * pAnd, * pAnd0, * pAnd1, * pTop; - Ft_Node_t * pFtNode; - int i, nVars, LevelNew, LevelOld, Counter; - - // sanity checks - nVars = Ft_FactorGetNumVars( vForm ); - assert( nVars >= 0 ); - assert( vForm->nSize > nVars ); - - // check for constant function - pFtNode = Ft_NodeRead( vForm, 0 ); - if ( pFtNode->fConst ) - return 0; - assert( nVars == vFanins->nSize ); - - // set the levels - Vec_IntClear( vLevels ); - Vec_PtrForEachEntry( vFanins, pAnd, i ) - Vec_IntPush( vLevels, Abc_ObjRegular(pAnd)->Level ); - - // compute the function of other nodes - Counter = 0; - for ( i = nVars; i < vForm->nSize; i++ ) - { - pFtNode = Ft_NodeRead( vForm, i ); - // check for buffer/inverter - if ( pFtNode->iFanin0 == pFtNode->iFanin1 ) - { - assert( vForm->nSize == nVars + 1 ); - pAnd = Vec_PtrEntry(vFanins, pFtNode->iFanin0); - pAnd = Abc_ObjNotCond( pAnd, pFtNode->fCompl ); - Vec_PtrPush( vFanins, pAnd ); - break; - } - - pAnd0 = Vec_PtrEntry(vFanins, pFtNode->iFanin0); - pAnd1 = Vec_PtrEntry(vFanins, pFtNode->iFanin1); - if ( pAnd0 && pAnd1 ) - { - pAnd0 = Abc_ObjNotCond( pAnd0, pFtNode->fCompl0 ); - pAnd1 = Abc_ObjNotCond( pAnd1, pFtNode->fCompl1 ); - pAnd = Abc_AigAndLookup( pMan, pAnd0, pAnd1 ); - } - else - pAnd = NULL; - // count the number of added nodes - if ( pAnd == NULL || Abc_NodeIsTravIdCurrent( Abc_ObjRegular(pAnd) ) ) - { - if ( pAnd ) - { -//printf( "Reusing labeled " ); Abc_AigPrintNode( pAnd ); - } - Counter++; - if ( Counter > NodeMax ) - { - Vec_PtrShrink( vFanins, nVars ); - return -1; - } - } - else - { -//printf( "Reusing " ); Abc_AigPrintNode( pAnd ); - } - - // count the number of new levels - LevelNew = -1; - if ( pAnd ) - { - if ( Abc_ObjRegular(pAnd) == Abc_AigConst1(pMan) ) - LevelNew = 0; - else if ( Abc_ObjRegular(pAnd) == Abc_ObjRegular(pAnd0) ) - LevelNew = (int)Abc_ObjRegular(pAnd0)->Level; - else if ( Abc_ObjRegular(pAnd) == Abc_ObjRegular(pAnd1) ) - LevelNew = (int)Abc_ObjRegular(pAnd1)->Level; - } - if ( LevelNew == -1 ) - LevelNew = 1 + ABC_MAX( Vec_IntEntry(vLevels, pFtNode->iFanin0), Vec_IntEntry(vLevels, pFtNode->iFanin1) ); - -// assert( pAnd == NULL || LevelNew == LevelOld ); - if ( pAnd ) - { - LevelOld = (int)Abc_ObjRegular(pAnd)->Level; - if ( LevelNew != LevelOld ) - { - int x = 0; - Abc_Obj_t * pFanin0, * pFanin1; - pFanin0 = Abc_ObjFanin0( Abc_ObjRegular(pAnd) ); - pFanin1 = Abc_ObjFanin1( Abc_ObjRegular(pAnd) ); - x = 0; - } - } - - if ( LevelNew > LevelMax ) - { - Vec_PtrShrink( vFanins, nVars ); - return -1; - } - Vec_PtrPush( vFanins, pAnd ); - Vec_IntPush( vLevels, LevelNew ); - } - assert( vForm->nSize = vFanins->nSize ); - - // check if this is the same form - pTop = Vec_PtrEntryLast(vFanins); - if ( Abc_ObjRegular(pTop) == pRoot ) - { - assert( !Abc_ObjIsComplement(pTop) ); - Vec_PtrShrink( vFanins, nVars ); - return -1; - } - Vec_PtrShrink( vFanins, nVars ); - return Counter; -} - - - //////////////////////////////////////////////////////////////////////// /// END OF FILE /// //////////////////////////////////////////////////////////////////////// diff --git a/src/base/abc/abcTiming.c b/src/base/abc/abcTiming.c index 032d074c..b8524bd5 100644 --- a/src/base/abc/abcTiming.c +++ b/src/base/abc/abcTiming.c @@ -252,7 +252,7 @@ void Abc_NtkTimeInitialize( Abc_Ntk_t * pNtk ) pTime = ppTimes[pObj->Id]; if ( pTime->Worst != -ABC_INFINITY ) continue; - *pTime = pNtk->pManTime->tArrDef; + *pTime = pNtk->pManTime->tReqDef; } // set the 0 arrival times for latches and constant nodes ppTimes = (Abc_Time_t **)pNtk->pManTime->vArrs->pArray; @@ -380,16 +380,16 @@ void Abc_ManTimeDup( Abc_Ntk_t * pNtkOld, Abc_Ntk_t * pNtkNew ) // set the default timing pNtkNew->pManTime->tArrDef = pNtkOld->pManTime->tArrDef; pNtkNew->pManTime->tReqDef = pNtkOld->pManTime->tReqDef; - // set the PI timing + // set the CI timing ppTimesOld = (Abc_Time_t **)pNtkOld->pManTime->vArrs->pArray; ppTimesNew = (Abc_Time_t **)pNtkNew->pManTime->vArrs->pArray; - Abc_NtkForEachPi( pNtkOld, pObj, i ) - *ppTimesNew[ Abc_NtkPi(pNtkNew,i)->Id ] = *ppTimesOld[ pObj->Id ]; - // set the PO timing + Abc_NtkForEachCi( pNtkOld, pObj, i ) + *ppTimesNew[ Abc_NtkCi(pNtkNew,i)->Id ] = *ppTimesOld[ pObj->Id ]; + // set the CO timing ppTimesOld = (Abc_Time_t **)pNtkOld->pManTime->vReqs->pArray; ppTimesNew = (Abc_Time_t **)pNtkNew->pManTime->vReqs->pArray; - Abc_NtkForEachPo( pNtkOld, pObj, i ) - *ppTimesNew[ Abc_NtkPo(pNtkNew,i)->Id ] = *ppTimesOld[ pObj->Id ]; + Abc_NtkForEachCo( pNtkOld, pObj, i ) + *ppTimesNew[ Abc_NtkCo(pNtkNew,i)->Id ] = *ppTimesOld[ pObj->Id ]; } /**Function************************************************************* diff --git a/src/base/abc/abcUtil.c b/src/base/abc/abcUtil.c index 2c460301..7a6a705d 100644 --- a/src/base/abc/abcUtil.c +++ b/src/base/abc/abcUtil.c @@ -21,7 +21,7 @@ #include "abc.h" #include "main.h" #include "mio.h" -#include "ft.h" +#include "dec.h" //////////////////////////////////////////////////////////////////////// /// DECLARATIONS /// @@ -118,16 +118,18 @@ int Abc_NtkGetLitNum( Abc_Ntk_t * pNtk ) ***********************************************************************/ int Abc_NtkGetLitFactNum( Abc_Ntk_t * pNtk ) { - Vec_Int_t * vFactor; + Dec_Graph_t * pFactor; Abc_Obj_t * pNode; int nNodes, i; assert( Abc_NtkHasSop(pNtk) ); nNodes = 0; Abc_NtkForEachNode( pNtk, pNode, i ) { - vFactor = Ft_Factor( pNode->pData ); - nNodes += Ft_FactorGetNumNodes(vFactor); - Vec_IntFree( vFactor ); + if ( Abc_NodeIsConst(pNode) ) + continue; + pFactor = Dec_Factor( pNode->pData ); + nNodes += 1 + Dec_GraphNodeNum(pFactor); + Dec_GraphFree( pFactor ); } return nNodes; } @@ -224,6 +226,49 @@ double Abc_NtkGetMappedArea( Abc_Ntk_t * pNtk ) /**Function************************************************************* + Synopsis [Counts the number of exors.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Abc_NtkGetExorNum( Abc_Ntk_t * pNtk ) +{ + Abc_Obj_t * pNode; + int i, Counter = 0; + Abc_NtkForEachNode( pNtk, pNode, i ) + Counter += pNode->fExor; + return Counter; +} + +/**Function************************************************************* + + Synopsis [Returns 1 if it is an AIG with choice nodes.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Abc_NtkGetChoiceNum( Abc_Ntk_t * pNtk ) +{ + Abc_Obj_t * pNode; + int i, Counter; + if ( !Abc_NtkIsStrash(pNtk) ) + return 0; + Counter = 0; + Abc_NtkForEachNode( pNtk, pNode, i ) + Counter += Abc_NodeIsAigChoice( pNode ); + return Counter; +} + +/**Function************************************************************* + Synopsis [Reads the maximum number of fanins.] Description [] @@ -451,26 +496,6 @@ void Abc_VecObjPushUniqueOrderByLevel( Vec_Ptr_t * p, Abc_Obj_t * pNode ) /**Function************************************************************* - Synopsis [Marks and counts the number of exors.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -int Abc_NtkCountExors( Abc_Ntk_t * pNtk ) -{ - Abc_Obj_t * pNode; - int i, Counter = 0; - Abc_NtkForEachNode( pNtk, pNode, i ) - Counter += pNode->fExor; - return Counter; -} - -/**Function************************************************************* - Synopsis [Returns 1 if the node is the root of EXOR/NEXOR.] Description [] @@ -634,29 +659,6 @@ Abc_Obj_t * Abc_NodeRecognizeMux( Abc_Obj_t * pNode, Abc_Obj_t ** ppNodeT, Abc_O /**Function************************************************************* - Synopsis [Returns 1 if it is an AIG with choice nodes.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -int Abc_NtkCountChoiceNodes( Abc_Ntk_t * pNtk ) -{ - Abc_Obj_t * pNode; - int i, Counter; - if ( !Abc_NtkIsStrash(pNtk) ) - return 0; - Counter = 0; - Abc_NtkForEachNode( pNtk, pNode, i ) - Counter += Abc_NodeIsAigChoice( pNode ); - return Counter; -} - -/**Function************************************************************* - Synopsis [Prepares two network for a two-argument command similar to "verify".] Description [] @@ -666,7 +668,7 @@ int Abc_NtkCountChoiceNodes( Abc_Ntk_t * pNtk ) SeeAlso [] ***********************************************************************/ -int Abc_NtkPrepareCommand( FILE * pErr, Abc_Ntk_t * pNtk, char ** argv, int argc, +int Abc_NtkPrepareTwoNtks( FILE * pErr, Abc_Ntk_t * pNtk, char ** argv, int argc, Abc_Ntk_t ** ppNtk1, Abc_Ntk_t ** ppNtk2, int * pfDelete1, int * pfDelete2 ) { int fCheck = 1; @@ -837,234 +839,6 @@ int Abc_NodeCompareLevelsDecrease( Abc_Obj_t ** pp1, Abc_Obj_t ** pp2 ) /**Function************************************************************* - Synopsis [Procedure used for sorting the nodes in decreasing order of levels.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -int Abc_NodeCompareNames( Abc_Obj_t ** pp1, Abc_Obj_t ** pp2 ) -{ - int Diff = strcmp( (char *)(*pp1)->pCopy, (char *)(*pp2)->pCopy ); - if ( Diff < 0 ) - return -1; - if ( Diff > 0 ) - return 1; - return 0; -} - - -/**Function************************************************************* - - Synopsis [Gets fanin node names.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -Vec_Ptr_t * Abc_NodeGetFaninNames( Abc_Obj_t * pNode ) -{ - Vec_Ptr_t * vNodes; - Abc_Obj_t * pFanin; - int i; - vNodes = Vec_PtrAlloc( 100 ); - Abc_ObjForEachFanin( pNode, pFanin, i ) - Vec_PtrPush( vNodes, util_strsav(Abc_ObjName(pFanin)) ); - return vNodes; -} - -/**Function************************************************************* - - Synopsis [Gets fanin node names.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -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 ); -} - -/**Function************************************************************* - - Synopsis [Collects the CI or CO names.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -char ** Abc_NtkCollectCioNames( Abc_Ntk_t * pNtk, int fCollectCos ) -{ - Abc_Obj_t * pObj; - char ** ppNames; - int i; - if ( fCollectCos ) - { - ppNames = ALLOC( char *, Abc_NtkCoNum(pNtk) ); - Abc_NtkForEachCo( pNtk, pObj, i ) - ppNames[i] = Abc_ObjName(pObj); - } - else - { - ppNames = ALLOC( char *, Abc_NtkCiNum(pNtk) ); - Abc_NtkForEachCi( pNtk, pObj, i ) - ppNames[i] = Abc_ObjName(pObj); - } - return ppNames; -} - -/**Function************************************************************* - - Synopsis [Orders PIs/POs/latches alphabetically.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -void Abc_NtkAlphaOrderSignals( Abc_Ntk_t * pNtk, int fComb ) -{ - Abc_Obj_t * pObj; - int i; - // temporarily store the names in the copy field - Abc_NtkForEachPi( pNtk, pObj, i ) - pObj->pCopy = (Abc_Obj_t *)Abc_ObjName(pObj); - Abc_NtkForEachPo( pNtk, pObj, i ) - pObj->pCopy = (Abc_Obj_t *)Abc_ObjName(pObj); - Abc_NtkForEachLatch( pNtk, pObj, i ) - pObj->pCopy = (Abc_Obj_t *)Abc_ObjName(pObj); - // order objects alphabetically - qsort( pNtk->vCis->pArray, pNtk->nPis, sizeof(Abc_Obj_t *), - (int (*)(const void *, const void *)) Abc_NodeCompareNames ); - qsort( pNtk->vCos->pArray, pNtk->nPos, sizeof(Abc_Obj_t *), - (int (*)(const void *, const void *)) Abc_NodeCompareNames ); - // if the comparison if combinational (latches as PIs/POs), order them too - if ( fComb ) - { - qsort( pNtk->vLats->pArray, pNtk->nLatches, sizeof(Abc_Obj_t *), - (int (*)(const void *, const void *)) Abc_NodeCompareNames ); - // add latches to make COs - Abc_NtkForEachLatch( pNtk, pObj, i ) - { - Vec_PtrWriteEntry( pNtk->vCis, pNtk->nPis + i, pObj ); - Vec_PtrWriteEntry( pNtk->vCos, pNtk->nPos + i, pObj ); - } - } - // clean the copy fields - Abc_NtkForEachPi( pNtk, pObj, i ) - pObj->pCopy = NULL; - Abc_NtkForEachPo( pNtk, pObj, i ) - pObj->pCopy = NULL; - Abc_NtkForEachLatch( pNtk, pObj, i ) - pObj->pCopy = NULL; -} - -/**Function************************************************************* - - Synopsis [] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -void Abc_NtkShortNames( Abc_Ntk_t * pNtk ) -{ - stmm_table * tObj2NameNew; - Abc_Obj_t * pObj; - char Buffer[100]; - char * pNameNew; - int Length, i; - - tObj2NameNew = stmm_init_table(stmm_ptrcmp, stmm_ptrhash); - // create new names and add them to the table - Length = Extra_Base10Log( Abc_NtkPiNum(pNtk) ); - Abc_NtkForEachPi( pNtk, pObj, i ) - { - sprintf( Buffer, "pi%0*d", Length, i ); - pNameNew = Abc_NtkRegisterName( pNtk, Buffer ); - stmm_insert( tObj2NameNew, (char *)pObj, pNameNew ); - } - // create new names and add them to the table - Length = Extra_Base10Log( Abc_NtkPoNum(pNtk) ); - Abc_NtkForEachPo( pNtk, pObj, i ) - { - sprintf( Buffer, "po%0*d", Length, i ); - pNameNew = Abc_NtkRegisterName( pNtk, Buffer ); - stmm_insert( tObj2NameNew, (char *)pObj, pNameNew ); - } - // create new names and add them to the table - Length = Extra_Base10Log( Abc_NtkLatchNum(pNtk) ); - Abc_NtkForEachLatch( pNtk, pObj, i ) - { - sprintf( Buffer, "lat%0*d", Length, i ); - pNameNew = Abc_NtkRegisterName( pNtk, Buffer ); - stmm_insert( tObj2NameNew, (char *)pObj, pNameNew ); - } - stmm_free_table( pNtk->tObj2Name ); - pNtk->tObj2Name = tObj2NameNew; -} - -/**Function************************************************************* - Synopsis [Creates the array of fanout counters.] Description [] diff --git a/src/base/io/ioWriteDot.c b/src/base/io/ioWriteDot.c index 7d88e52d..97258c81 100644 --- a/src/base/io/ioWriteDot.c +++ b/src/base/io/ioWriteDot.c @@ -45,7 +45,7 @@ void Io_WriteDot( Abc_Ntk_t * pNtk, Vec_Ptr_t * vNodes, Vec_Ptr_t * vNodesShow, FILE * pFile; Abc_Obj_t * pNode, * pTemp, * pPrev; int LevelMin, LevelMax, fHasCos, Level, i; - int Limit = 200; + int Limit = 300; if ( vNodes->nSize < 1 ) { @@ -109,8 +109,10 @@ void Io_WriteDot( Abc_Ntk_t * pNtk, Vec_Ptr_t * vNodes, Vec_Ptr_t * vNodesShow, // fprintf( pFile, "ranksep = 0.5;\n" ); // fprintf( pFile, "nodesep = 0.5;\n" ); fprintf( pFile, "center = true;\n" ); +// fprintf( pFile, "orientation = landscape;\n" ); // fprintf( pFile, "edge [fontsize = 10];\n" ); // fprintf( pFile, "edge [dir = none];\n" ); + fprintf( pFile, "edge [dir = back];\n" ); fprintf( pFile, "\n" ); // labels on the left of the picture @@ -194,8 +196,9 @@ void Io_WriteDot( Abc_Ntk_t * pNtk, Vec_Ptr_t * vNodes, Vec_Ptr_t * vNodesShow, { if ( !Abc_ObjIsCo(pNode) ) continue; - fprintf( pFile, " Node%d [label = \"%s\"", pNode->Id, Abc_ObjName(pNode) ); - fprintf( pFile, ", shape = invtriangle" ); + fprintf( pFile, " Node%d%s [label = \"%s%s\"", pNode->Id, + (Abc_ObjIsLatch(pNode)? "_in":""), Abc_ObjName(pNode), (Abc_ObjIsLatch(pNode)? "_in":"") ); + fprintf( pFile, ", shape = %s", (Abc_ObjIsLatch(pNode)? "box":"invtriangle") ); if ( pNode->fMarkB ) fprintf( pFile, ", style = filled" ); fprintf( pFile, ", color = coral, fillcolor = coral" ); @@ -240,8 +243,9 @@ void Io_WriteDot( Abc_Ntk_t * pNtk, Vec_Ptr_t * vNodes, Vec_Ptr_t * vNodesShow, { if ( !Abc_ObjIsCi(pNode) ) continue; - fprintf( pFile, " Node%d [label = \"%s\"", pNode->Id, Abc_ObjName(pNode) ); - fprintf( pFile, ", shape = triangle" ); + fprintf( pFile, " Node%d%s [label = \"%s%s\"", pNode->Id, + (Abc_ObjIsLatch(pNode)? "_out":""), Abc_ObjName(pNode), (Abc_ObjIsLatch(pNode)? "_out":"") ); + fprintf( pFile, ", shape = %s", (Abc_ObjIsLatch(pNode)? "box":"triangle") ); if ( pNode->fMarkB ) fprintf( pFile, ", style = filled" ); fprintf( pFile, ", color = coral, fillcolor = coral" ); @@ -258,7 +262,8 @@ void Io_WriteDot( Abc_Ntk_t * pNtk, Vec_Ptr_t * vNodes, Vec_Ptr_t * vNodesShow, { if ( (int)pNode->Level != LevelMax ) continue; - fprintf( pFile, "title2 -> Node%d [style = invis];\n", pNode->Id ); + fprintf( pFile, "title2 -> Node%d%s [style = invis];\n", pNode->Id, + (Abc_ObjIsLatch(pNode)? "_in":"") ); } // generate edges @@ -269,10 +274,10 @@ void Io_WriteDot( Abc_Ntk_t * pNtk, Vec_Ptr_t * vNodes, Vec_Ptr_t * vNodesShow, // generate the edge from this node to the next if ( Abc_ObjFanin0(pNode)->fMarkC ) { - fprintf( pFile, "Node%d", pNode->Id ); + fprintf( pFile, "Node%d%s", pNode->Id, (Abc_ObjIsLatch(pNode)? "_in":"") ); fprintf( pFile, " -> " ); - fprintf( pFile, "Node%d", Abc_ObjFaninId0(pNode) ); - fprintf( pFile, " [style = %s]", Abc_ObjFaninC0(pNode)? "dashed" : "bold" ); + fprintf( pFile, "Node%d%s", Abc_ObjFaninId0(pNode), (Abc_ObjIsLatch(Abc_ObjFanin0(pNode))? "_out":"") ); + fprintf( pFile, " [style = %s]", Abc_ObjFaninC0(pNode)? "dotted" : "bold" ); fprintf( pFile, ";\n" ); } if ( Abc_ObjFaninNum(pNode) == 1 ) @@ -282,8 +287,8 @@ void Io_WriteDot( Abc_Ntk_t * pNtk, Vec_Ptr_t * vNodes, Vec_Ptr_t * vNodesShow, { fprintf( pFile, "Node%d", pNode->Id ); fprintf( pFile, " -> " ); - fprintf( pFile, "Node%d", Abc_ObjFaninId1(pNode) ); - fprintf( pFile, " [style = %s]", Abc_ObjFaninC1(pNode)? "dashed" : "bold" ); + fprintf( pFile, "Node%d%s", Abc_ObjFaninId1(pNode), (Abc_ObjIsLatch(Abc_ObjFanin1(pNode))? "_out":"") ); + fprintf( pFile, " [style = %s]", Abc_ObjFaninC1(pNode)? "dotted" : "bold" ); fprintf( pFile, ";\n" ); } // generate the edges between the equivalent nodes @@ -295,7 +300,7 @@ void Io_WriteDot( Abc_Ntk_t * pNtk, Vec_Ptr_t * vNodes, Vec_Ptr_t * vNodesShow, fprintf( pFile, "Node%d", pPrev->Id ); fprintf( pFile, " -> " ); fprintf( pFile, "Node%d", pTemp->Id ); - fprintf( pFile, " [style = %s]", (pPrev->fPhase ^ pTemp->fPhase)? "dashed" : "bold" ); + fprintf( pFile, " [style = %s]", (pPrev->fPhase ^ pTemp->fPhase)? "dotted" : "bold" ); fprintf( pFile, ";\n" ); pPrev = pTemp; } diff --git a/src/base/io/ioWriteDot_old.c b/src/base/io/ioWriteDot_old.c new file mode 100644 index 00000000..59bbbde3 --- /dev/null +++ b/src/base/io/ioWriteDot_old.c @@ -0,0 +1,325 @@ +/**CFile**************************************************************** + + FileName [ioWriteDot.c] + + SystemName [ABC: Logic synthesis and verification system.] + + PackageName [Command processing package.] + + Synopsis [Procedures to write the graph structure of AIG in DOT.] + + Author [Alan Mishchenko] + + Affiliation [UC Berkeley] + + Date [Ver. 1.0. Started - June 20, 2005.] + + Revision [$Id: ioWriteDot.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $] + +***********************************************************************/ + +#include "io.h" + +//////////////////////////////////////////////////////////////////////// +/// DECLARATIONS /// +//////////////////////////////////////////////////////////////////////// + +//////////////////////////////////////////////////////////////////////// +/// FUNCTION DEFITIONS /// +//////////////////////////////////////////////////////////////////////// + +/**Function************************************************************* + + Synopsis [Writes the graph structure of AIG in DOT.] + + Description [Useful for graph visualization using tools such as GraphViz: + http://www.graphviz.org/] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Io_WriteDot( Abc_Ntk_t * pNtk, Vec_Ptr_t * vNodes, Vec_Ptr_t * vNodesShow, char * pFileName ) +{ + FILE * pFile; + Abc_Obj_t * pNode, * pFanin, * pPrev, * pTemp; + int LevelMin, LevelMax, fHasCos, Level, i; + int Limit = 200; + + if ( vNodes->nSize < 1 ) + { + printf( "The set has no nodes. DOT file is not written.\n" ); + return; + } + + if ( vNodes->nSize > Limit ) + { + printf( "The set has more than %d nodes. DOT file is not written.\n", Limit ); + return; + } + + // start the output file + if ( (pFile = fopen( pFileName, "w" )) == NULL ) + { + fprintf( stdout, "Cannot open the intermediate file \"%s\".\n", pFileName ); + return; + } + + // mark the nodes from the set + Vec_PtrForEachEntry( vNodes, pNode, i ) + pNode->fMarkC = 1; + if ( vNodesShow ) + Vec_PtrForEachEntry( vNodesShow, pNode, i ) + pNode->fMarkB = 1; + + // find the largest and the smallest levels + LevelMin = 10000; + LevelMax = -1; + fHasCos = 0; + Vec_PtrForEachEntry( vNodes, pNode, i ) + { + if ( Abc_ObjIsCo(pNode) ) + { + fHasCos = 1; + continue; + } + if ( LevelMin > (int)pNode->Level ) + LevelMin = pNode->Level; + if ( LevelMax < (int)pNode->Level ) + LevelMax = pNode->Level; + } + + // set the level of the CO nodes + if ( fHasCos ) + { + LevelMax++; + Vec_PtrForEachEntry( vNodes, pNode, i ) + { + if ( Abc_ObjIsCo(pNode) ) + pNode->Level = LevelMax; + } + } + + // write the DOT header + fprintf( pFile, "# %s\n", "AIG generated by ABC" ); + fprintf( pFile, "\n" ); + fprintf( pFile, "digraph AIG {\n" ); + fprintf( pFile, "size = \"7.5,10\";\n" ); +// fprintf( pFile, "ranksep = 0.5;\n" ); +// fprintf( pFile, "nodesep = 0.5;\n" ); + fprintf( pFile, "center = true;\n" ); +// fprintf( pFile, "edge [fontsize = 10];\n" ); +// fprintf( pFile, "edge [dir = back];\n" ); +// fprintf( pFile, "edge [dir = none];\n" ); + fprintf( pFile, "\n" ); + + // labels on the left of the picture + fprintf( pFile, "{\n" ); + fprintf( pFile, " node [shape = plaintext];\n" ); + fprintf( pFile, " edge [style = invis];\n" ); + fprintf( pFile, " LevelTitle1 [label=\"\"];\n" ); + fprintf( pFile, " LevelTitle2 [label=\"\"];\n" ); + // generate node names with labels + for ( Level = LevelMax; Level >= LevelMin; Level-- ) + { + // the visible node name + fprintf( pFile, " Level%d", Level ); + fprintf( pFile, " [label = " ); + // label name + fprintf( pFile, "\"" ); + fprintf( pFile, "\"" ); + fprintf( pFile, "];\n" ); + } + + // genetate the sequence of visible/invisible nodes to mark levels + fprintf( pFile, " LevelTitle1 -> LevelTitle2 ->" ); + for ( Level = LevelMax; Level >= LevelMin; Level-- ) + { + // the visible node name + fprintf( pFile, " Level%d", Level ); + // the connector + if ( Level != LevelMin ) + fprintf( pFile, " ->" ); + else + fprintf( pFile, ";" ); + } + fprintf( pFile, "\n" ); + fprintf( pFile, "}" ); + fprintf( pFile, "\n" ); + fprintf( pFile, "\n" ); + + // generate title box on top + fprintf( pFile, "{\n" ); + fprintf( pFile, " rank = same;\n" ); + fprintf( pFile, " LevelTitle1;\n" ); + fprintf( pFile, " title1 [shape=plaintext,\n" ); + fprintf( pFile, " fontsize=20,\n" ); + fprintf( pFile, " fontname = \"Times-Roman\",\n" ); + fprintf( pFile, " label=\"" ); + fprintf( pFile, "%s", "AIG generated by ABC" ); + fprintf( pFile, "\\n" ); + fprintf( pFile, "Benchmark \\\"%s\\\". ", pNtk->pName ); + fprintf( pFile, "Time was %s. ", Extra_TimeStamp() ); + fprintf( pFile, "\"\n" ); + fprintf( pFile, " ];\n" ); + fprintf( pFile, "}" ); + fprintf( pFile, "\n" ); + fprintf( pFile, "\n" ); + + // generate statistics box + fprintf( pFile, "{\n" ); + fprintf( pFile, " rank = same;\n" ); + fprintf( pFile, " LevelTitle2;\n" ); + fprintf( pFile, " title2 [shape=plaintext,\n" ); + fprintf( pFile, " fontsize=18,\n" ); + fprintf( pFile, " fontname = \"Times-Roman\",\n" ); + fprintf( pFile, " label=\"" ); + fprintf( pFile, "The set contains %d nodes and spans %d levels.", vNodes->nSize, LevelMax - LevelMin ); + fprintf( pFile, "\\n" ); + fprintf( pFile, "\"\n" ); + fprintf( pFile, " ];\n" ); + fprintf( pFile, "}" ); + fprintf( pFile, "\n" ); + fprintf( pFile, "\n" ); + + // generate the POs + if ( fHasCos ) + { + fprintf( pFile, "{\n" ); + fprintf( pFile, " rank = same;\n" ); + // the labeling node of this level + fprintf( pFile, " Level%d;\n", LevelMax ); + // generat the PO nodes + Vec_PtrForEachEntry( vNodes, pNode, i ) + { + if ( !Abc_ObjIsCo(pNode) ) + continue; + fprintf( pFile, " Node%d%s [label = \"%s\"", pNode->Id, (Abc_ObjIsLatch(pNode)? "Top":""), Abc_ObjName(pNode) ); + fprintf( pFile, ", shape = invtriangle" ); + if ( pNode->fMarkB ) + fprintf( pFile, ", style = filled" ); + fprintf( pFile, ", color = coral, fillcolor = coral" ); + fprintf( pFile, "];\n" ); + } + fprintf( pFile, "}" ); + fprintf( pFile, "\n" ); + fprintf( pFile, "\n" ); + } + + // generate nodes of each rank + for ( Level = LevelMax - fHasCos; Level >= LevelMin && Level > 0; Level-- ) + { + fprintf( pFile, "{\n" ); + fprintf( pFile, " rank = same;\n" ); + // the labeling node of this level + fprintf( pFile, " Level%d;\n", Level ); + Vec_PtrForEachEntry( vNodes, pNode, i ) + { + if ( (int)pNode->Level != Level ) + continue; + fprintf( pFile, " Node%d [label = \"%d\"", pNode->Id, pNode->Id ); + fprintf( pFile, ", shape = ellipse" ); + if ( pNode->fMarkB ) + fprintf( pFile, ", style = filled" ); + fprintf( pFile, "];\n" ); + } + fprintf( pFile, "}" ); + fprintf( pFile, "\n" ); + fprintf( pFile, "\n" ); + } + + // generate the PI nodes if any + if ( LevelMin == 0 ) + { + fprintf( pFile, "{\n" ); + fprintf( pFile, " rank = same;\n" ); + // the labeling node of this level + fprintf( pFile, " Level%d;\n", LevelMin ); + // generat the PO nodes + Vec_PtrForEachEntry( vNodes, pNode, i ) + { + if ( !Abc_ObjIsCi(pNode) ) + continue; + fprintf( pFile, " Node%d%s [label = \"%s\"", pNode->Id, (Abc_ObjIsLatch(pNode)? "Bot":""), Abc_ObjName(pNode) ); + fprintf( pFile, ", shape = triangle" ); + if ( pNode->fMarkB ) + fprintf( pFile, ", style = filled" ); + fprintf( pFile, ", color = coral, fillcolor = coral" ); + fprintf( pFile, "];\n" ); + } + fprintf( pFile, "}" ); + fprintf( pFile, "\n" ); + fprintf( pFile, "\n" ); + } + + // generate invisible edges from the square down + fprintf( pFile, "title1 -> title2 [style = invis];\n" ); + Vec_PtrForEachEntry( vNodes, pNode, i ) + { + if ( (int)pNode->Level != LevelMax ) + continue; + fprintf( pFile, "title2 -> Node%d%s [style = invis];\n", pNode->Id ); + } + + // generate edges + Vec_PtrForEachEntry( vNodes, pNode, i ) + { + if ( Abc_ObjFaninNum(pNode) == 0 ) + continue; + // generate the edge from this node to the next + pFanin = Abc_ObjFanin0(pNode); + if ( pFanin->fMarkC ) + { + fprintf( pFile, "Node%d%s", pNode->Id, (Abc_ObjIsLatch(pNode)? "Top":"") ); + fprintf( pFile, " -> " ); + fprintf( pFile, "Node%d%s", pFanin->Id, (Abc_ObjIsLatch(pFanin)? "Bot":"") ); + fprintf( pFile, " [style = %s]", Abc_ObjFaninC0(pNode)? "dashed" : "bold" ); + fprintf( pFile, ";\n" ); + } + if ( Abc_ObjFaninNum(pNode) == 1 ) + continue; + // generate the edge from this node to the next + pFanin = Abc_ObjFanin1(pNode); + if ( pFanin->fMarkC ) + { + fprintf( pFile, "Node%d", pNode->Id ); + fprintf( pFile, " -> " ); + fprintf( pFile, "Node%d%s", pFanin->Id, (Abc_ObjIsLatch(pFanin)? "Bot":"") ); + fprintf( pFile, " [style = %s]", Abc_ObjFaninC1(pNode)? "dashed" : "bold" ); + fprintf( pFile, ";\n" ); + } + // generate the edges between the equivalent nodes + pPrev = pNode; + for ( pTemp = pNode->pData; pTemp; pTemp = pTemp->pData ) + { + if ( pTemp->fMarkC ) + { + fprintf( pFile, "Node%d", pPrev->Id ); + fprintf( pFile, " -> " ); + fprintf( pFile, "Node%d", pTemp->Id ); + fprintf( pFile, " [style = %s]", (pPrev->fPhase ^ pTemp->fPhase)? "dashed" : "bold" ); + fprintf( pFile, ";\n" ); + pPrev = pTemp; + } + } + } + + fprintf( pFile, "}" ); + fprintf( pFile, "\n" ); + fprintf( pFile, "\n" ); + fclose( pFile ); + + // unmark the nodes from the set + Vec_PtrForEachEntry( vNodes, pNode, i ) + pNode->fMarkC = 0; + if ( vNodesShow ) + Vec_PtrForEachEntry( vNodesShow, pNode, i ) + pNode->fMarkB = 0; +} + +//////////////////////////////////////////////////////////////////////// +/// END OF FILE /// +//////////////////////////////////////////////////////////////////////// + + diff --git a/src/base/main/main.h b/src/base/main/main.h index da47f154..72eec599 100644 --- a/src/base/main/main.h +++ b/src/base/main/main.h @@ -102,6 +102,9 @@ extern void Abc_FrameSetLibLut ( Abc_Frame_t * pFrame, void extern void Abc_FrameSetLibGen ( Abc_Frame_t * pFrame, void * pLib ); extern void Abc_FrameSetLibSuper ( Abc_Frame_t * pFrame, void * pLib ); +extern void * Abc_FrameReadManDd ( Abc_Frame_t * pFrame ); +extern void * Abc_FrameReadManDec ( Abc_Frame_t * pFrame ); + //////////////////////////////////////////////////////////////////////// /// END OF FILE /// diff --git a/src/base/main/mainFrame.c b/src/base/main/mainFrame.c index 2e9d9d41..09a750ea 100644 --- a/src/base/main/mainFrame.c +++ b/src/base/main/mainFrame.c @@ -20,6 +20,7 @@ #include "mainInt.h" #include "abc.h" +#include "dec.h" //////////////////////////////////////////////////////////////////////// /// DECLARATIONS /// @@ -58,6 +59,9 @@ Abc_Frame_t * Abc_FrameAllocate() // set the starting step p->nSteps = 1; p->fBatchMode = 0; + // initialize decomposition manager + p->pManDec = Dec_ManStart(); + p->dd = Cudd_Init( 0, 0, CUDD_UNIQUE_SLOTS, CUDD_CACHE_SLOTS, 0 ); return p; } @@ -75,6 +79,8 @@ Abc_Frame_t * Abc_FrameAllocate() ***********************************************************************/ void Abc_FrameDeallocate( Abc_Frame_t * p ) { + Dec_ManStop( p->pManDec ); + Extra_StopManager( p->dd ); Abc_FrameDeleteAllNetworks( p ); free( p ); p = NULL; @@ -417,17 +423,20 @@ Abc_Frame_t * Abc_FrameGetGlobalFrame() SeeAlso [] ***********************************************************************/ -Abc_Ntk_t * Abc_FrameReadNtkStore ( Abc_Frame_t * pFrame ) { return pFrame->pStored; } -int Abc_FrameReadNtkStoreSize ( Abc_Frame_t * pFrame ) { return pFrame->nStored; } -void Abc_FrameSetNtkStore ( Abc_Frame_t * pFrame, Abc_Ntk_t * pNtk ) { pFrame->pStored = pNtk; } -void Abc_FrameSetNtkStoreSize ( Abc_Frame_t * pFrame, int nStored ) { pFrame->nStored = nStored; } +Abc_Ntk_t * Abc_FrameReadNtkStore ( Abc_Frame_t * pFrame ) { return pFrame->pStored; } +int Abc_FrameReadNtkStoreSize ( Abc_Frame_t * pFrame ) { return pFrame->nStored; } +void Abc_FrameSetNtkStore ( Abc_Frame_t * pFrame, Abc_Ntk_t * pNtk ) { pFrame->pStored = pNtk; } +void Abc_FrameSetNtkStoreSize ( Abc_Frame_t * pFrame, int nStored ) { pFrame->nStored = nStored;} void * Abc_FrameReadLibLut ( Abc_Frame_t * pFrame ) { return pFrame->pLibLut; } void * Abc_FrameReadLibGen ( Abc_Frame_t * pFrame ) { return pFrame->pLibGen; } void * Abc_FrameReadLibSuper ( Abc_Frame_t * pFrame ) { return pFrame->pLibSuper; } -void Abc_FrameSetLibLut ( Abc_Frame_t * pFrame, void * pLib ) { pFrame->pLibLut = pLib; } -void Abc_FrameSetLibGen ( Abc_Frame_t * pFrame, void * pLib ) { pFrame->pLibGen = pLib; } -void Abc_FrameSetLibSuper ( Abc_Frame_t * pFrame, void * pLib ) { pFrame->pLibSuper = pLib; } +void Abc_FrameSetLibLut ( Abc_Frame_t * pFrame, void * pLib ) { pFrame->pLibLut = pLib; } +void Abc_FrameSetLibGen ( Abc_Frame_t * pFrame, void * pLib ) { pFrame->pLibGen = pLib; } +void Abc_FrameSetLibSuper ( Abc_Frame_t * pFrame, void * pLib ) { pFrame->pLibSuper = pLib; } + +void * Abc_FrameReadManDd ( Abc_Frame_t * pFrame ) { return pFrame->dd; } +void * Abc_FrameReadManDec ( Abc_Frame_t * pFrame ) { return pFrame->pManDec; } //////////////////////////////////////////////////////////////////////// /// END OF FILE /// diff --git a/src/base/main/mainInt.h b/src/base/main/mainInt.h index 557c4e2f..95d5b22d 100644 --- a/src/base/main/mainInt.h +++ b/src/base/main/mainInt.h @@ -66,6 +66,9 @@ struct Abc_Frame_t_ // temporary storage for structural choices Abc_Ntk_t * pStored; // the stored networks int nStored; // the number of stored networks + // decomposition package + DdManager * dd; // temporary BDD package + void * pManDec; // decomposition manager void * pLibLut; // the current LUT library void * pLibGen; // the current genlib diff --git a/src/opt/dec/dec.h b/src/opt/dec/dec.h index 26af6b1c..6ecc9678 100644 --- a/src/opt/dec/dec.h +++ b/src/opt/dec/dec.h @@ -33,83 +33,89 @@ /// BASIC TYPES /// //////////////////////////////////////////////////////////////////////// +typedef struct Dec_Edge_t_ Dec_Edge_t; +struct Dec_Edge_t_ +{ + unsigned fCompl : 1; // the complemented bit + unsigned Node : 30; // the decomposition node pointed by the edge +}; + 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 + Dec_Edge_t eEdge0; // the left child of the node + Dec_Edge_t eEdge1; // the right child of the node // 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 + void * pFunc; // the function of the node (BDD or AIG) + unsigned Level : 16; // the level of this node in the global AIG + // printing info + unsigned fNodeOr : 1; // marks the original OR node + unsigned fCompl0 : 1; // marks the original complemented edge + unsigned fCompl1 : 1; // marks the original complemented edge +}; + +typedef struct Dec_Graph_t_ Dec_Graph_t; +struct Dec_Graph_t_ +{ + int fConst; // marks the constant 1 graph + int nLeaves; // the number of leaves + int nSize; // the number of nodes (including the leaves) + int nCap; // the number of allocated nodes + Dec_Node_t * pNodes; // the array of leaves and internal nodes + Dec_Edge_t eRoot; // the pointer to the topmost node +}; + +typedef struct Dec_Man_t_ Dec_Man_t; +struct Dec_Man_t_ +{ + void * pMvcMem; // memory manager for MVC cover (used for factoring) + Vec_Int_t * vCubes; // storage for cubes + Vec_Int_t * vLits; // storage for literals + // precomputation information about 4-variable functions + unsigned short * puCanons; // canonical forms + char * pPhases; // canonical phases + char * pPerms; // canonical permutations + unsigned char * pMap; // mapping of functions into class numbers }; -/* - 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 /// +/// ITERATORS /// //////////////////////////////////////////////////////////////////////// +// interator throught the leaves +#define Dec_GraphForEachLeaf( pGraph, pLeaf, i ) \ + for ( i = 0; (i < (pGraph)->nLeaves) && (((pLeaf) = Dec_GraphNode(pGraph, i)), 1); i++ ) +// interator throught the internal nodes +#define Dec_GraphForEachNode( pGraph, pAnd, i ) \ + for ( i = (pGraph)->nLeaves; (i < (pGraph)->nSize) && (((pAnd) = Dec_GraphNode(pGraph, i)), 1); i++ ) + //////////////////////////////////////////////////////////////////////// /// FUNCTION DECLARATIONS /// //////////////////////////////////////////////////////////////////////// +/*=== decAbc.c ========================================================*/ +extern Abc_Obj_t * Dec_GraphToNetwork( Abc_Aig_t * pMan, Dec_Graph_t * pGraph ); +extern int Dec_GraphToNetworkCount( Abc_Obj_t * pRoot, Dec_Graph_t * pGraph, int NodeMax, int LevelMax ); +extern void Dec_GraphUpdateNetwork( Abc_Obj_t * pRoot, Dec_Graph_t * pGraph, int nGain ); +/*=== decFactor.c ========================================================*/ +extern Dec_Graph_t * Dec_Factor( char * pSop ); +/*=== decMan.c ========================================================*/ +extern Dec_Man_t * Dec_ManStart(); +extern void Dec_ManStop( Dec_Man_t * p ); +/*=== decPrint.c ========================================================*/ +extern void Dec_GraphPrint( FILE * pFile, Dec_Graph_t * pGraph, char * pNamesIn[], char * pNameOut ); +/*=== decUtil.c ========================================================*/ +extern DdNode * Dec_GraphDeriveBdd( DdManager * dd, Dec_Graph_t * pGraph ); +extern unsigned Dec_GraphDeriveTruth( Dec_Graph_t * pGraph ); + +//////////////////////////////////////////////////////////////////////// +/// FUNCTION DEFITIONS /// +//////////////////////////////////////////////////////////////////////// + /**Function************************************************************* - Synopsis [Cleans the decomposition node.] + Synopsis [Creates an edge pointing to the node in the given polarity.] Description [] @@ -117,12 +123,16 @@ struct Dec_Node_t_ SeeAlso [] -***********************************************************************/ -static inline void Dec_NodeClean( Dec_Node_t * pNode ) { *((int *)pNode) = 0; } +***********************************************************************/ +static inline Dec_Edge_t Dec_EdgeCreate( int Node, int fCompl ) +{ + Dec_Edge_t eEdge = { fCompl, Node }; + return eEdge; +} /**Function************************************************************* - Synopsis [Convert between an interger and an decomposition node.] + Synopsis [Converts the edge into unsigned integer.] Description [] @@ -131,12 +141,14 @@ static inline void Dec_NodeClean( Dec_Node_t * pNode ) { *((int * 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); } +static inline unsigned Dec_EdgeToInt( Dec_Edge_t eEdge ) +{ + return (eEdge.Node << 1) | eEdge.fCompl; +} /**Function************************************************************* - Synopsis [Returns the pointer to the i-th decomposition node.] + Synopsis [Converts unsigned integer into the edge.] Description [] @@ -145,11 +157,14 @@ static inline int Dec_Node2Int( Dec_Node_t Node ) { return * SeeAlso [] ***********************************************************************/ -static inline Dec_Node_t * Dec_NodeRead( Vec_Int_t * vDec, int i ) { return (Dec_Node_t *)vDec->pArray + i; } +static inline Dec_Edge_t Dec_IntToEdge( unsigned Edge ) +{ + return Dec_EdgeCreate( Edge >> 1, Edge & 1 ); +} /**Function************************************************************* - Synopsis [Returns the pointer to the last decomposition node.] + Synopsis [Converts the edge into unsigned integer.] Description [] @@ -158,11 +173,14 @@ static inline Dec_Node_t * Dec_NodeRead( Vec_Int_t * vDec, int i ) { return ( SeeAlso [] ***********************************************************************/ -static inline Dec_Node_t * Dec_NodeReadLast( Vec_Int_t * vDec ) { return (Dec_Node_t *)vDec->pArray + vDec->nSize - 1; } +static inline unsigned Dec_EdgeToInt_( Dec_Edge_t eEdge ) +{ + return *(unsigned *)&eEdge; +} /**Function************************************************************* - Synopsis [Returns the pointer to the fanins of the i-th decomposition node.] + Synopsis [Converts unsigned integer into the edge.] Description [] @@ -171,12 +189,14 @@ static inline Dec_Node_t * Dec_NodeReadLast( Vec_Int_t * vDec ) { return ( 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; } +static inline Dec_Edge_t Dec_IntToEdge_( unsigned Edge ) +{ + return *(Dec_Edge_t *)&Edge; +} /**Function************************************************************* - Synopsis [Returns the complemented attributes of the i-th decomposition node.] + Synopsis [Creates a graph with the given number of leaves.] Description [] @@ -185,12 +205,22 @@ static inline Dec_Node_t * Dec_NodeFanin1( Vec_Int_t * vDec, int i ) { assert( D 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; } +static inline Dec_Graph_t * Dec_GraphCreate( int nLeaves ) +{ + Dec_Graph_t * pGraph; + pGraph = ALLOC( Dec_Graph_t, 1 ); + memset( pGraph, 0, sizeof(Dec_Graph_t) ); + pGraph->nLeaves = nLeaves; + pGraph->nSize = nLeaves; + pGraph->nCap = 2 * nLeaves + 50; + pGraph->pNodes = ALLOC( Dec_Node_t, pGraph->nCap ); + memset( pGraph->pNodes, 0, sizeof(Dec_Node_t) * pGraph->nSize ); + return pGraph; +} /**Function************************************************************* - Synopsis [Returns the number of leaf variables.] + Synopsis [Creates constant 0 graph.] Description [] @@ -199,18 +229,19 @@ static inline bool Dec_NodeFaninC1( Vec_Int_t * vDec, int i ) { assert( SeeAlso [] ***********************************************************************/ -static inline int Dec_TreeNumVars( Vec_Int_t * vDec ) +static inline Dec_Graph_t * Dec_GraphCreateConst0() { - int i; - for ( i = 0; i < vDec->nSize; i++ ) - if ( vDec->pArray[i] ) - break; - return i; + Dec_Graph_t * pGraph; + pGraph = ALLOC( Dec_Graph_t, 1 ); + memset( pGraph, 0, sizeof(Dec_Graph_t) ); + pGraph->fConst = 1; + pGraph->eRoot.fCompl = 1; + return pGraph; } /**Function************************************************************* - Synopsis [Returns the number of AND nodes in the tree.] + Synopsis [Creates constant 1 graph.] Description [] @@ -219,20 +250,56 @@ static inline int Dec_TreeNumVars( Vec_Int_t * vDec ) SeeAlso [] ***********************************************************************/ -static int Dec_TreeNumAnds( Vec_Int_t * vDec ) +static inline Dec_Graph_t * Dec_GraphCreateConst1() { - 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); + Dec_Graph_t * pGraph; + pGraph = ALLOC( Dec_Graph_t, 1 ); + memset( pGraph, 0, sizeof(Dec_Graph_t) ); + pGraph->fConst = 1; + return pGraph; +} + +/**Function************************************************************* + + Synopsis [Creates the literal graph.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +static inline Dec_Graph_t * Dec_GraphCreateLeaf( int iLeaf, int nLeaves, int fCompl ) +{ + Dec_Graph_t * pGraph; + assert( 0 <= iLeaf && iLeaf < nLeaves ); + pGraph = Dec_GraphCreate( nLeaves ); + pGraph->eRoot.Node = iLeaf; + pGraph->eRoot.fCompl = fCompl; + return pGraph; +} + +/**Function************************************************************* + + Synopsis [Creates a graph with the given number of leaves.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +static inline void Dec_GraphFree( Dec_Graph_t * pGraph ) +{ + FREE( pGraph->pNodes ); + free( pGraph ); } /**Function************************************************************* - Synopsis [Returns the number of literals in the factored form.] + Synopsis [Returns 1 if the graph is a constant.] Description [] @@ -241,16 +308,30 @@ static int Dec_TreeNumAnds( Vec_Int_t * vDec ) SeeAlso [] ***********************************************************************/ -static inline int Dec_TreeNumFFLits( Vec_Int_t * vDec ) +static inline bool Dec_GraphIsConst( Dec_Graph_t * pGraph ) { - return 1 + Dec_TreeNumAnds( vDec ); + return pGraph->fConst; } +/**Function************************************************************* + Synopsis [Returns 1 if the graph is constant 0.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +static inline bool Dec_GraphIsConst0( Dec_Graph_t * pGraph ) +{ + return pGraph->fConst && pGraph->eRoot.fCompl; +} /**Function************************************************************* - Synopsis [Checks if the output node of the decomposition tree is complemented.] + Synopsis [Returns 1 if the graph is constant 1.] Description [] @@ -259,11 +340,14 @@ static inline int Dec_TreeNumFFLits( Vec_Int_t * vDec ) SeeAlso [] ***********************************************************************/ -static inline bool Dec_TreeIsComplement( Vec_Int_t * vForm ) { return Dec_NodeReadLast(vForm)->fCompl; } +static inline bool Dec_GraphIsConst1( Dec_Graph_t * pGraph ) +{ + return pGraph->fConst && !pGraph->eRoot.fCompl; +} /**Function************************************************************* - Synopsis [Complements the output node of the decomposition tree.] + Synopsis [Returns 1 if the graph is complemented.] Description [] @@ -272,12 +356,31 @@ static inline bool Dec_TreeIsComplement( Vec_Int_t * vForm ) { return Dec_NodeR SeeAlso [] ***********************************************************************/ -static inline void Dec_TreeComplement( Vec_Int_t * vForm ) { Dec_NodeReadLast(vForm)->fCompl ^= 1; } +static inline bool Dec_GraphIsComplement( Dec_Graph_t * pGraph ) +{ + return pGraph->eRoot.fCompl; +} + +/**Function************************************************************* + + Synopsis [Checks if the graph is complemented.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +static inline void Dec_GraphComplement( Dec_Graph_t * pGraph ) +{ + pGraph->eRoot.fCompl ^= 1; +} /**Function************************************************************* - Synopsis [Checks if the output node is a constant.] + Synopsis [Returns the number of leaves.] Description [] @@ -286,13 +389,14 @@ static inline void Dec_TreeComplement( Vec_Int_t * vForm ) { Dec_NodeReadLas 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; } +static inline int Dec_GraphLeaveNum( Dec_Graph_t * pGraph ) +{ + return pGraph->nLeaves; +} /**Function************************************************************* - Synopsis [Creates a constant 0 decomposition tree.] + Synopsis [Returns the number of internal nodes.] Description [] @@ -301,23 +405,14 @@ static inline bool Dec_TreeIsConst1( Vec_Int_t * vForm ) { return D SeeAlso [] ***********************************************************************/ -static inline Vec_Int_t * Dec_TreeCreateConst0() +static inline int Dec_GraphNodeNum( Dec_Graph_t * pGraph ) { - 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; + return pGraph->nSize - pGraph->nLeaves; } /**Function************************************************************* - Synopsis [Creates a constant 1 decomposition tree.] + Synopsis [Returns the pointer to the node.] Description [] @@ -326,24 +421,30 @@ static inline Vec_Int_t * Dec_TreeCreateConst0() SeeAlso [] ***********************************************************************/ -static inline Vec_Int_t * Dec_TreeCreateConst1() +static inline Dec_Node_t * Dec_GraphNode( Dec_Graph_t * pGraph, int i ) { - 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; + return pGraph->pNodes + i; } +/**Function************************************************************* + + Synopsis [Returns the pointer to the node.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +static inline Dec_Node_t * Dec_GraphNodeLast( Dec_Graph_t * pGraph ) +{ + return pGraph->pNodes + pGraph->nSize - 1; +} /**Function************************************************************* - Synopsis [Checks if the decomposition tree is an elementary var.] + Synopsis [Returns the number of the given node.] Description [] @@ -352,14 +453,14 @@ static inline Vec_Int_t * Dec_TreeCreateConst1() SeeAlso [] ***********************************************************************/ -static inline bool Dec_TreeIsVar( Vec_Int_t * vForm ) +static inline int Dec_GraphNodeInt( Dec_Graph_t * pGraph, Dec_Node_t * pNode ) { - return Dec_NodeReadLast(vForm)->iFanin0 == Dec_NodeReadLast(vForm)->iFanin1; + return pNode - pGraph->pNodes; } /**Function************************************************************* - Synopsis [Creates the decomposition tree to represent an elementary var.] + Synopsis [Check if the graph represents elementary variable.] Description [] @@ -368,19 +469,177 @@ static inline bool Dec_TreeIsVar( Vec_Int_t * vForm ) SeeAlso [] ***********************************************************************/ -static inline Vec_Int_t * Dec_TreeCreateVar( int iVar, int nVars, int fCompl ) +static inline bool Dec_GraphIsVar( Dec_Graph_t * pGraph ) +{ + return pGraph->eRoot.Node < (unsigned)pGraph->nLeaves; +} + +/**Function************************************************************* + + Synopsis [Check if the graph represents elementary variable.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +static inline bool Dec_GraphNodeIsVar( Dec_Graph_t * pGraph, Dec_Node_t * pNode ) +{ + return Dec_GraphNodeInt(pGraph,pNode) < pGraph->nLeaves; +} + +/**Function************************************************************* + + Synopsis [Returns the elementary variable elementary variable.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +static inline Dec_Node_t * Dec_GraphVar( Dec_Graph_t * pGraph ) +{ + assert( Dec_GraphIsVar( pGraph ) ); + return Dec_GraphNode( pGraph, pGraph->eRoot.Node ); +} + +/**Function************************************************************* + + Synopsis [Returns the number of the elementary variable.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +static inline int Dec_GraphVarInt( Dec_Graph_t * pGraph ) +{ + assert( Dec_GraphIsVar( pGraph ) ); + return Dec_GraphNodeInt( pGraph, Dec_GraphVar(pGraph) ); +} + +/**Function************************************************************* + + Synopsis [Sets the root of the graph.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +static inline void Dec_GraphSetRoot( Dec_Graph_t * pGraph, Dec_Edge_t eRoot ) +{ + pGraph->eRoot = eRoot; +} + +/**Function************************************************************* + + Synopsis [Appends a new node to the graph.] + + Description [This procedure is meant for internal use.] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +static inline Dec_Node_t * Dec_GraphAppendNode( Dec_Graph_t * pGraph ) +{ + Dec_Node_t * pNode; + if ( pGraph->nSize == pGraph->nCap ) + { + pGraph->pNodes = REALLOC( Dec_Node_t, pGraph->pNodes, 2 * pGraph->nCap ); + pGraph->nCap = 2 * pGraph->nCap; + } + pNode = pGraph->pNodes + pGraph->nSize++; + memset( pNode, 0, sizeof(Dec_Node_t) ); + return pNode; +} + +/**Function************************************************************* + + Synopsis [Creates an AND node.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +static inline Dec_Edge_t Dec_GraphAddNodeAnd( Dec_Graph_t * pGraph, Dec_Edge_t eEdge0, Dec_Edge_t eEdge1 ) +{ + Dec_Node_t * pNode; + // get the new node + pNode = Dec_GraphAppendNode( pGraph ); + // set the inputs and other info + pNode->eEdge0 = eEdge0; + pNode->eEdge1 = eEdge1; + pNode->fCompl0 = eEdge0.fCompl; + pNode->fCompl1 = eEdge1.fCompl; + return Dec_EdgeCreate( pGraph->nSize - 1, 0 ); +} + +/**Function************************************************************* + + Synopsis [Creates an OR node.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +static inline Dec_Edge_t Dec_GraphAddNodeOr( Dec_Graph_t * pGraph, Dec_Edge_t eEdge0, Dec_Edge_t eEdge1 ) { - 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; + // get the new node + pNode = Dec_GraphAppendNode( pGraph ); + // set the inputs and other info + pNode->eEdge0 = eEdge0; + pNode->eEdge1 = eEdge1; + pNode->fCompl0 = eEdge0.fCompl; + pNode->fCompl1 = eEdge1.fCompl; + // make adjustments for the OR gate + pNode->fNodeOr = 1; + pNode->eEdge0.fCompl = !pNode->eEdge0.fCompl; + pNode->eEdge1.fCompl = !pNode->eEdge1.fCompl; + return Dec_EdgeCreate( pGraph->nSize - 1, 1 ); +} + +/**Function************************************************************* + + Synopsis [Creates an XOR node.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +static inline Dec_Edge_t Dec_GraphAddNodeXor( Dec_Graph_t * pGraph, Dec_Edge_t eEdge0, Dec_Edge_t eEdge1 ) +{ + Dec_Edge_t eNode0, eNode1; + // derive the first AND + eEdge0.fCompl = !eEdge0.fCompl; + eNode0 = Dec_GraphAddNodeAnd( pGraph, eEdge0, eEdge1 ); + eEdge0.fCompl = !eEdge0.fCompl; + // derive the second AND + eEdge1.fCompl = !eEdge1.fCompl; + eNode1 = Dec_GraphAddNodeAnd( pGraph, eEdge0, eEdge1 ); + eEdge1.fCompl = !eEdge1.fCompl; + // derive the final OR + return Dec_GraphAddNodeOr( pGraph, eNode0, eNode1 ); } //////////////////////////////////////////////////////////////////////// diff --git a/src/opt/dec/decAbc.c b/src/opt/dec/decAbc.c new file mode 100644 index 00000000..9931b136 --- /dev/null +++ b/src/opt/dec/decAbc.c @@ -0,0 +1,170 @@ +/**CFile**************************************************************** + + FileName [decAbc.c] + + PackageName [MVSIS 2.0: Multi-valued logic synthesis system.] + + Synopsis [Interface between the decomposition package and ABC network.] + + Author [MVSIS Group] + + Affiliation [UC Berkeley] + + Date [Ver. 1.0. Started - February 1, 2003.] + + Revision [$Id: decAbc.c,v 1.1 2003/05/22 19:20:05 alanmi Exp $] + +***********************************************************************/ + +#include "abc.h" +#include "dec.h" + +//////////////////////////////////////////////////////////////////////// +/// DECLARATIONS /// +//////////////////////////////////////////////////////////////////////// + +//////////////////////////////////////////////////////////////////////// +/// FUNCTION DEFITIONS /// +//////////////////////////////////////////////////////////////////////// + +/**Function************************************************************* + + Synopsis [Transforms the decomposition graph into the AIG.] + + Description [AIG nodes for the fanins should be assigned to pNode->pFunc + of the leaves of the graph before calling this procedure.] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Abc_Obj_t * Dec_GraphToNetwork( Abc_Aig_t * pMan, Dec_Graph_t * pGraph ) +{ + Abc_Obj_t * pAnd0, * pAnd1; + Dec_Node_t * pNode; + int i; + // check for constant function + if ( Dec_GraphIsConst(pGraph) ) + return Abc_ObjNotCond( Abc_AigConst1(pMan), Dec_GraphIsComplement(pGraph) ); + // check for a literal + if ( Dec_GraphIsVar(pGraph) ) + return Abc_ObjNotCond( Dec_GraphVar(pGraph)->pFunc, Dec_GraphIsComplement(pGraph) ); + // build the AIG nodes corresponding to the AND gates of the graph + Dec_GraphForEachNode( pGraph, pNode, i ) + { + pAnd0 = Abc_ObjNotCond( Dec_GraphNode(pGraph, pNode->eEdge0.Node)->pFunc, pNode->eEdge0.fCompl ); + pAnd1 = Abc_ObjNotCond( Dec_GraphNode(pGraph, pNode->eEdge1.Node)->pFunc, pNode->eEdge1.fCompl ); + pNode->pFunc = Abc_AigAnd( pMan, pAnd0, pAnd1 ); + } + // complement the result if necessary + return Abc_ObjNotCond( pNode->pFunc, Dec_GraphIsComplement(pGraph) ); +} + +/**Function************************************************************* + + Synopsis [Counts the number of new nodes added when using this graph.] + + Description [AIG nodes for the fanins should be assigned to pNode->pFunc + of the leaves of the graph before calling this procedure. + Returns -1 if the number of nodes and levels exceeded the given limit or + the number of levels exceeded the maximum allowed level.] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Dec_GraphToNetworkCount( Abc_Obj_t * pRoot, Dec_Graph_t * pGraph, int NodeMax, int LevelMax ) +{ + Abc_Aig_t * pMan = pRoot->pNtk->pManFunc; + Dec_Node_t * pNode, * pNode0, * pNode1; + Abc_Obj_t * pAnd, * pAnd0, * pAnd1; + int i, Counter, LevelNew, LevelOld; + // check for constant function or a literal + if ( Dec_GraphIsConst(pGraph) || Dec_GraphIsVar(pGraph) ) + return 0; + // set the levels of the leaves + Dec_GraphForEachLeaf( pGraph, pNode, i ) + pNode->Level = Abc_ObjRegular(pNode->pFunc)->Level; + // compute the AIG size after adding the internal nodes + Counter = 0; + Dec_GraphForEachNode( pGraph, pNode, i ) + { + // get the children of this node + pNode0 = Dec_GraphNode( pGraph, pNode->eEdge0.Node ); + pNode1 = Dec_GraphNode( pGraph, pNode->eEdge1.Node ); + // get the AIG nodes corresponding to the children + pAnd0 = pNode0->pFunc; + pAnd1 = pNode1->pFunc; + if ( pAnd0 && pAnd1 ) + { + // if they are both present, find the resulting node + pAnd0 = Abc_ObjNotCond( pAnd0, pNode->eEdge0.fCompl ); + pAnd1 = Abc_ObjNotCond( pAnd1, pNode->eEdge1.fCompl ); + pAnd = Abc_AigAndLookup( pMan, pAnd0, pAnd1 ); + // return -1 if the node is the same as the original root + if ( Abc_ObjRegular(pAnd) == pRoot ) + return -1; + } + else + pAnd = NULL; + // count the number of added nodes + if ( pAnd == NULL || Abc_NodeIsTravIdCurrent(Abc_ObjRegular(pAnd)) ) + { + if ( ++Counter > NodeMax ) + return -1; + } + // count the number of new levels + LevelNew = 1 + ABC_MAX( pNode0->Level, pNode1->Level ); + if ( pAnd ) + { + if ( Abc_ObjRegular(pAnd) == Abc_AigConst1(pMan) ) + LevelNew = 0; + else if ( Abc_ObjRegular(pAnd) == Abc_ObjRegular(pAnd0) ) + LevelNew = (int)Abc_ObjRegular(pAnd0)->Level; + else if ( Abc_ObjRegular(pAnd) == Abc_ObjRegular(pAnd1) ) + LevelNew = (int)Abc_ObjRegular(pAnd1)->Level; + LevelOld = (int)Abc_ObjRegular(pAnd)->Level; + assert( LevelNew == LevelOld ); + } + if ( LevelNew > LevelMax ) + return -1; + pNode->pFunc = pAnd; + pNode->Level = LevelNew; + } + return Counter; +} + + +/**Function************************************************************* + + Synopsis [Replaces MFFC of the node by the new factored form.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Dec_GraphUpdateNetwork( Abc_Obj_t * pRoot, Dec_Graph_t * pGraph, int nGain ) +{ + Abc_Obj_t * pRootNew; + Abc_Ntk_t * pNtk = pRoot->pNtk; + int nNodesNew, nNodesOld; + nNodesOld = Abc_NtkNodeNum(pNtk); + // create the new structure of nodes + pRootNew = Dec_GraphToNetwork( pNtk->pManFunc, pGraph ); + // remove the old nodes + Abc_AigReplace( pNtk->pManFunc, pRoot, pRootNew ); + // compare the gains + nNodesNew = Abc_NtkNodeNum(pNtk); + assert( nGain <= nNodesOld - nNodesNew ); +} + +//////////////////////////////////////////////////////////////////////// +/// END OF FILE /// +//////////////////////////////////////////////////////////////////////// + + diff --git a/src/opt/dec/decFactor.c b/src/opt/dec/decFactor.c new file mode 100644 index 00000000..f6654476 --- /dev/null +++ b/src/opt/dec/decFactor.c @@ -0,0 +1,393 @@ +/**CFile**************************************************************** + + FileName [ftFactor.c] + + PackageName [MVSIS 2.0: Multi-valued logic synthesis system.] + + Synopsis [Procedures for algebraic factoring.] + + Author [MVSIS Group] + + Affiliation [UC Berkeley] + + Date [Ver. 1.0. Started - February 1, 2003.] + + Revision [$Id: ftFactor.c,v 1.3 2003/09/01 04:56:43 alanmi Exp $] + +***********************************************************************/ + +#include "abc.h" +#include "main.h" +#include "mvc.h" +#include "dec.h" + +//////////////////////////////////////////////////////////////////////// +/// DECLARATIONS /// +//////////////////////////////////////////////////////////////////////// + +static Dec_Edge_t Dec_Factor_rec( Dec_Graph_t * pFForm, Mvc_Cover_t * pCover ); +static Dec_Edge_t Dec_FactorLF_rec( Dec_Graph_t * pFForm, Mvc_Cover_t * pCover, Mvc_Cover_t * pSimple ); +static Dec_Edge_t Dec_FactorTrivial( Dec_Graph_t * pFForm, Mvc_Cover_t * pCover ); +static Dec_Edge_t Dec_FactorTrivialCube( Dec_Graph_t * pFForm, Mvc_Cover_t * pCover, Mvc_Cube_t * pCube, Vec_Int_t * vEdgeLits ); +static Dec_Edge_t Dec_FactorTrivialTree_rec( Dec_Graph_t * pFForm, Dec_Edge_t * peNodes, int nNodes, int fNodeOr ); +static int Dec_FactorVerify( char * pSop, Dec_Graph_t * pFForm ); +static Mvc_Cover_t * Dec_ConvertSopToMvc( char * pSop ); + +//////////////////////////////////////////////////////////////////////// +/// FUNCTION DEFITIONS /// +//////////////////////////////////////////////////////////////////////// + +/**Function************************************************************* + + Synopsis [Factors the cover.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Dec_Graph_t * Dec_Factor( char * pSop ) +{ + Mvc_Cover_t * pCover; + Dec_Graph_t * pFForm; + Dec_Edge_t eRoot; + + // derive the cover from the SOP representation + pCover = Dec_ConvertSopToMvc( pSop ); + + // make sure the cover is CCS free (should be done before CST) + Mvc_CoverContain( pCover ); + // check for trivial functions + if ( Mvc_CoverIsEmpty(pCover) ) + { + Mvc_CoverFree( pCover ); + return Dec_GraphCreateConst0(); + } + if ( Mvc_CoverIsTautology(pCover) ) + { + Mvc_CoverFree( pCover ); + return Dec_GraphCreateConst1(); + } + + // perform CST + Mvc_CoverInverse( pCover ); // CST + // start the factored form + pFForm = Dec_GraphCreate( Abc_SopGetVarNum(pSop) ); + // factor the cover + eRoot = Dec_Factor_rec( pFForm, pCover ); + // finalize the factored form + Dec_GraphSetRoot( pFForm, eRoot ); + // complement the factored form if SOP is complemented + if ( Abc_SopIsComplement(pSop) ) + Dec_GraphComplement( pFForm ); + // verify the factored form +// if ( !Dec_FactorVerify( pSop, pFForm ) ) +// printf( "Verification has failed.\n" ); +// Mvc_CoverInverse( pCover ); // undo CST + Mvc_CoverFree( pCover ); + return pFForm; +} + +/**Function************************************************************* + + Synopsis [Internal recursive factoring procedure.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Dec_Edge_t Dec_Factor_rec( Dec_Graph_t * pFForm, Mvc_Cover_t * pCover ) +{ + Mvc_Cover_t * pDiv, * pQuo, * pRem, * pCom; + Dec_Edge_t eNodeDiv, eNodeQuo, eNodeRem; + Dec_Edge_t eNodeAnd, eNode; + + // make sure the cover contains some cubes + assert( Mvc_CoverReadCubeNum(pCover) ); + + // get the divisor + pDiv = Mvc_CoverDivisor( pCover ); + if ( pDiv == NULL ) + return Dec_FactorTrivial( pFForm, pCover ); + + // divide the cover by the divisor + Mvc_CoverDivideInternal( pCover, pDiv, &pQuo, &pRem ); + assert( Mvc_CoverReadCubeNum(pQuo) ); + + Mvc_CoverFree( pDiv ); + Mvc_CoverFree( pRem ); + + // check the trivial case + if ( Mvc_CoverReadCubeNum(pQuo) == 1 ) + { + eNode = Dec_FactorLF_rec( pFForm, pCover, pQuo ); + Mvc_CoverFree( pQuo ); + return eNode; + } + + // make the quotient cube free + Mvc_CoverMakeCubeFree( pQuo ); + + // divide the cover by the quotient + Mvc_CoverDivideInternal( pCover, pQuo, &pDiv, &pRem ); + + // check the trivial case + if ( Mvc_CoverIsCubeFree( pDiv ) ) + { + eNodeDiv = Dec_Factor_rec( pFForm, pDiv ); + eNodeQuo = Dec_Factor_rec( pFForm, pQuo ); + Mvc_CoverFree( pDiv ); + Mvc_CoverFree( pQuo ); + eNodeAnd = Dec_GraphAddNodeAnd( pFForm, eNodeDiv, eNodeQuo ); + if ( Mvc_CoverReadCubeNum(pRem) == 0 ) + { + Mvc_CoverFree( pRem ); + return eNodeAnd; + } + else + { + eNodeRem = Dec_Factor_rec( pFForm, pRem ); + Mvc_CoverFree( pRem ); + return Dec_GraphAddNodeOr( pFForm, eNodeAnd, eNodeRem ); + } + } + + // get the common cube + pCom = Mvc_CoverCommonCubeCover( pDiv ); + Mvc_CoverFree( pDiv ); + Mvc_CoverFree( pQuo ); + Mvc_CoverFree( pRem ); + + // solve the simple problem + eNode = Dec_FactorLF_rec( pFForm, pCover, pCom ); + Mvc_CoverFree( pCom ); + return eNode; +} + + +/**Function************************************************************* + + Synopsis [Internal recursive factoring procedure for the leaf case.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Dec_Edge_t Dec_FactorLF_rec( Dec_Graph_t * pFForm, Mvc_Cover_t * pCover, Mvc_Cover_t * pSimple ) +{ + Dec_Man_t * pManDec = Abc_FrameReadManDec(Abc_FrameGetGlobalFrame()); + Vec_Int_t * vEdgeLits = pManDec->vLits; + Mvc_Cover_t * pDiv, * pQuo, * pRem; + Dec_Edge_t eNodeDiv, eNodeQuo, eNodeRem; + Dec_Edge_t eNodeAnd; + + // get the most often occurring literal + pDiv = Mvc_CoverBestLiteralCover( pCover, pSimple ); + // divide the cover by the literal + Mvc_CoverDivideByLiteral( pCover, pDiv, &pQuo, &pRem ); + // get the node pointer for the literal + eNodeDiv = Dec_FactorTrivialCube( pFForm, pDiv, Mvc_CoverReadCubeHead(pDiv), vEdgeLits ); + Mvc_CoverFree( pDiv ); + // factor the quotient and remainder + eNodeQuo = Dec_Factor_rec( pFForm, pQuo ); + Mvc_CoverFree( pQuo ); + eNodeAnd = Dec_GraphAddNodeAnd( pFForm, eNodeDiv, eNodeQuo ); + if ( Mvc_CoverReadCubeNum(pRem) == 0 ) + { + Mvc_CoverFree( pRem ); + return eNodeAnd; + } + else + { + eNodeRem = Dec_Factor_rec( pFForm, pRem ); + Mvc_CoverFree( pRem ); + return Dec_GraphAddNodeOr( pFForm, eNodeAnd, eNodeRem ); + } +} + + + +/**Function************************************************************* + + Synopsis [Factoring the cover, which has no algebraic divisors.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Dec_Edge_t Dec_FactorTrivial( Dec_Graph_t * pFForm, Mvc_Cover_t * pCover ) +{ + Dec_Man_t * pManDec = Abc_FrameReadManDec(Abc_FrameGetGlobalFrame()); + Vec_Int_t * vEdgeCubes = pManDec->vCubes; + Vec_Int_t * vEdgeLits = pManDec->vLits; + Mvc_Manager_t * pMem = pManDec->pMvcMem; + Dec_Edge_t eNode; + Mvc_Cube_t * pCube; + // create the factored form for each cube + Vec_IntClear( vEdgeCubes ); + Mvc_CoverForEachCube( pCover, pCube ) + { + eNode = Dec_FactorTrivialCube( pFForm, pCover, pCube, vEdgeLits ); + Vec_IntPush( vEdgeCubes, Dec_EdgeToInt_(eNode) ); + } + // balance the factored forms + return Dec_FactorTrivialTree_rec( pFForm, (Dec_Edge_t *)vEdgeCubes->pArray, vEdgeCubes->nSize, 1 ); +} + +/**Function************************************************************* + + Synopsis [Factoring the cube.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Dec_Edge_t Dec_FactorTrivialCube( Dec_Graph_t * pFForm, Mvc_Cover_t * pCover, Mvc_Cube_t * pCube, Vec_Int_t * vEdgeLits ) +{ +// Dec_Edge_t eNode; + int iBit, Value; + // create the factored form for each literal + Vec_IntClear( vEdgeLits ); + Mvc_CubeForEachBit( pCover, pCube, iBit, Value ) + if ( Value ) + { +// eNode = Dec_EdgeCreate( iBit/2, iBit%2 ); // CST +// Vec_IntPush( vEdgeLits, Dec_EdgeToInt_(eNode) ); + Vec_IntPush( vEdgeLits, iBit ); + } + // balance the factored forms + return Dec_FactorTrivialTree_rec( pFForm, (Dec_Edge_t *)vEdgeLits->pArray, vEdgeLits->nSize, 0 ); +} + +/**Function************************************************************* + + Synopsis [Create the well-balanced tree of nodes.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Dec_Edge_t Dec_FactorTrivialTree_rec( Dec_Graph_t * pFForm, Dec_Edge_t * peNodes, int nNodes, int fNodeOr ) +{ + Dec_Edge_t eNode1, eNode2; + int nNodes1, nNodes2; + + if ( nNodes == 1 ) + return peNodes[0]; + + // split the nodes into two parts + nNodes1 = nNodes/2; + nNodes2 = nNodes - nNodes1; +// nNodes2 = nNodes/2; +// nNodes1 = nNodes - nNodes2; + + // recursively construct the tree for the parts + eNode1 = Dec_FactorTrivialTree_rec( pFForm, peNodes, nNodes1, fNodeOr ); + eNode2 = Dec_FactorTrivialTree_rec( pFForm, peNodes + nNodes1, nNodes2, fNodeOr ); + + if ( fNodeOr ) + return Dec_GraphAddNodeOr( pFForm, eNode1, eNode2 ); + else + return Dec_GraphAddNodeAnd( pFForm, eNode1, eNode2 ); +} + + + +/**Function************************************************************* + + Synopsis [Converts SOP into MVC.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Mvc_Cover_t * Dec_ConvertSopToMvc( char * pSop ) +{ + Dec_Man_t * pManDec = Abc_FrameReadManDec(Abc_FrameGetGlobalFrame()); + Mvc_Manager_t * pMem = pManDec->pMvcMem; + Mvc_Cover_t * pMvc; + Mvc_Cube_t * pMvcCube; + char * pCube; + int nVars, Value, v; + + // start the cover + nVars = Abc_SopGetVarNum(pSop); + pMvc = Mvc_CoverAlloc( pMem, nVars * 2 ); + // check the logic function of the node + Abc_SopForEachCube( pSop, nVars, pCube ) + { + // create and add the cube + pMvcCube = Mvc_CubeAlloc( pMvc ); + Mvc_CoverAddCubeTail( pMvc, pMvcCube ); + // fill in the literals + Mvc_CubeBitFill( pMvcCube ); + Abc_CubeForEachVar( pCube, Value, v ) + { + if ( Value == '0' ) + Mvc_CubeBitRemove( pMvcCube, v * 2 + 1 ); + else if ( Value == '1' ) + Mvc_CubeBitRemove( pMvcCube, v * 2 ); + } + } + return pMvc; +} + +/**Function************************************************************* + + Synopsis [Verifies that the factoring is correct.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Dec_FactorVerify( char * pSop, Dec_Graph_t * pFForm ) +{ + DdManager * dd = Abc_FrameReadManDd( Abc_FrameGetGlobalFrame() ); + DdNode * bFunc1, * bFunc2; + int RetValue; + bFunc1 = Abc_ConvertSopToBdd( dd, pSop ); Cudd_Ref( bFunc1 ); + bFunc2 = Dec_GraphDeriveBdd( dd, pFForm ); Cudd_Ref( bFunc2 ); +//Extra_bddPrint( dd, bFunc1 ); printf("\n"); +//Extra_bddPrint( dd, bFunc2 ); printf("\n"); + RetValue = (bFunc1 == bFunc2); + if ( bFunc1 != bFunc2 ) + { + int s; + Extra_bddPrint( dd, bFunc1 ); printf("\n"); + Extra_bddPrint( dd, bFunc2 ); printf("\n"); + s = 0; + } + Cudd_RecursiveDeref( dd, bFunc1 ); + Cudd_RecursiveDeref( dd, bFunc2 ); + return RetValue; +} + + +//////////////////////////////////////////////////////////////////////// +/// END OF FILE /// +//////////////////////////////////////////////////////////////////////// + + diff --git a/src/opt/dec/decMan.c b/src/opt/dec/decMan.c new file mode 100644 index 00000000..1d44d5cb --- /dev/null +++ b/src/opt/dec/decMan.c @@ -0,0 +1,83 @@ +/**CFile**************************************************************** + + FileName [decMan.c] + + PackageName [MVSIS 2.0: Multi-valued logic synthesis system.] + + Synopsis [Decomposition manager.] + + Author [MVSIS Group] + + Affiliation [UC Berkeley] + + Date [Ver. 1.0. Started - February 1, 2003.] + + Revision [$Id: decMan.c,v 1.1 2003/05/22 19:20:05 alanmi Exp $] + +***********************************************************************/ + +#include "abc.h" +#include "mvc.h" +#include "dec.h" + +//////////////////////////////////////////////////////////////////////// +/// DECLARATIONS /// +//////////////////////////////////////////////////////////////////////// + +//////////////////////////////////////////////////////////////////////// +/// FUNCTION DEFITIONS /// +//////////////////////////////////////////////////////////////////////// + +/**Function************************************************************* + + Synopsis [Start the MVC manager used in the factoring package.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Dec_Man_t * Dec_ManStart() +{ + Dec_Man_t * p; + int clk = clock(); + p = ALLOC( Dec_Man_t, 1 ); + p->pMvcMem = Mvc_ManagerStart(); + p->vCubes = Vec_IntAlloc( 8 ); + p->vLits = Vec_IntAlloc( 8 ); + // canonical forms, phases, perms + Extra_Truth4VarNPN( &p->puCanons, &p->pPhases, &p->pPerms, &p->pMap ); +//PRT( "NPN classes precomputation time", clock() - clk ); + return p; +} + +/**Function************************************************************* + + Synopsis [Stops the MVC maanager used in the factoring package.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Dec_ManStop( Dec_Man_t * p ) +{ + Mvc_ManagerFree( p->pMvcMem ); + Vec_IntFree( p->vCubes ); + Vec_IntFree( p->vLits ); + free( p->puCanons ); + free( p->pPhases ); + free( p->pPerms ); + free( p->pMap ); + free( p ); +} + +//////////////////////////////////////////////////////////////////////// +/// END OF FILE /// +//////////////////////////////////////////////////////////////////////// + + diff --git a/src/sop/ft/ftPrint.c b/src/opt/dec/decPrint.c index 78f91b8f..6fb20327 100644 --- a/src/sop/ft/ftPrint.c +++ b/src/opt/dec/decPrint.c @@ -1,10 +1,10 @@ /**CFile**************************************************************** - FileName [ftPrint.c] + FileName [decPrint.c] PackageName [MVSIS 2.0: Multi-valued logic synthesis system.] - Synopsis [Procedures to print the factored tree.] + Synopsis [Procedures to print the decomposition graphs (factored forms).] Author [MVSIS Group] @@ -12,21 +12,21 @@ Date [Ver. 1.0. Started - February 1, 2003.] - Revision [$Id: ftPrint.c,v 1.1 2003/05/22 19:20:05 alanmi Exp $] + Revision [$Id: decPrint.c,v 1.1 2003/05/22 19:20:05 alanmi Exp $] ***********************************************************************/ #include "abc.h" -#include "ft.h" +#include "dec.h" //////////////////////////////////////////////////////////////////////// /// DECLARATIONS /// //////////////////////////////////////////////////////////////////////// -static void Ft_FactorPrint_rec( FILE * pFile, Vec_Int_t * vForm, Ft_Node_t * pNode, int fCompl, char * pNamesIn[], int * pPos, int LitSizeMax ); -static int Ft_FactorPrintGetLeafName( FILE * pFile, Vec_Int_t * vForm, Ft_Node_t * pNode, int fCompl, char * pNamesIn[] ); -static void Ft_FactorPrintUpdatePos( FILE * pFile, int * pPos, int LitSizeMax ); -static int Ft_FactorPrintOutputName( FILE * pFile, char * pNameOut, int fCompl ); +static void Dec_GraphPrint_rec( FILE * pFile, Dec_Graph_t * pGraph, Dec_Node_t * pNode, int fCompl, char * pNamesIn[], int * pPos, int LitSizeMax ); +static int Dec_GraphPrintGetLeafName( FILE * pFile, int iLeaf, int fCompl, char * pNamesIn[] ); +static void Dec_GraphPrintUpdatePos( FILE * pFile, int * pPos, int LitSizeMax ); +static int Dec_GraphPrintOutputName( FILE * pFile, char * pNameOut, int fCompl ); //////////////////////////////////////////////////////////////////////// /// FUNCTION DEFITIONS /// @@ -34,7 +34,7 @@ static int Ft_FactorPrintOutputName( FILE * pFile, char * pNameOut, int fComp /**Function************************************************************* - Synopsis [] + Synopsis [Prints the decomposition graph.] Description [] @@ -43,21 +43,15 @@ static int Ft_FactorPrintOutputName( FILE * pFile, char * pNameOut, int fComp SeeAlso [] ***********************************************************************/ -void Ft_FactorPrint( FILE * pFile, Vec_Int_t * vForm, char * pNamesIn[], char * pNameOut ) +void Dec_GraphPrint( FILE * pFile, Dec_Graph_t * pGraph, char * pNamesIn[], char * pNameOut ) { - Ft_Node_t * pNode; Vec_Ptr_t * vNamesIn = NULL; - int LitSizeMax, LitSizeCur, nVars, Pos, i; - - // sanity checks - nVars = Ft_FactorGetNumVars( vForm ); - assert( nVars >= 0 ); - assert( vForm->nSize > nVars ); + int LitSizeMax, LitSizeCur, Pos, i; // create the names if not given by the user if ( pNamesIn == NULL ) { - vNamesIn = Abc_NodeGetFakeNames( nVars ); + vNamesIn = Abc_NodeGetFakeNames( Dec_GraphLeaveNum(pGraph) ); pNamesIn = (char **)vNamesIn->pArray; } if ( pNameOut == NULL ) @@ -65,7 +59,7 @@ void Ft_FactorPrint( FILE * pFile, Vec_Int_t * vForm, char * pNamesIn[], char * // get the size of the longest literal LitSizeMax = 0; - for ( i = 0; i < nVars; i++ ) + for ( i = 0; i < Dec_GraphLeaveNum(pGraph); i++ ) { LitSizeCur = strlen(pNamesIn[i]); if ( LitSizeMax < LitSizeCur ) @@ -74,17 +68,21 @@ void Ft_FactorPrint( FILE * pFile, Vec_Int_t * vForm, char * pNamesIn[], char * if ( LitSizeMax > 50 ) LitSizeMax = 20; - // print the output name - pNode = Ft_NodeReadLast(vForm); - if ( !pNode->fConst && pNode->iFanin0 == pNode->iFanin1 ) // literal + // write the decomposition graph (factored form) + if ( Dec_GraphIsConst(pGraph) ) // constant { - Pos = Ft_FactorPrintOutputName( pFile, pNameOut, 0 ); - Ft_FactorPrintGetLeafName( pFile, vForm, Ft_NodeFanin0(vForm,pNode), pNode->fCompl, pNamesIn ); + Pos = Dec_GraphPrintOutputName( pFile, pNameOut, 0 ); + fprintf( pFile, "Constant %d", !Dec_GraphIsComplement(pGraph) ); } - else // constant or non-trivial form + else if ( Dec_GraphIsVar(pGraph) ) // literal { - Pos = Ft_FactorPrintOutputName( pFile, pNameOut, pNode->fCompl ); - Ft_FactorPrint_rec( pFile, vForm, pNode, 0, pNamesIn, &Pos, LitSizeMax ); + Pos = Dec_GraphPrintOutputName( pFile, pNameOut, 0 ); + Dec_GraphPrintGetLeafName( pFile, Dec_GraphVarInt(pGraph), Dec_GraphIsComplement(pGraph), pNamesIn ); + } + else + { + Pos = Dec_GraphPrintOutputName( pFile, pNameOut, Dec_GraphIsComplement(pGraph) ); + Dec_GraphPrint_rec( pFile, pGraph, Dec_GraphNodeLast(pGraph), 0, pNamesIn, &Pos, LitSizeMax ); } fprintf( pFile, "\n" ); @@ -103,50 +101,40 @@ void Ft_FactorPrint( FILE * pFile, Vec_Int_t * vForm, char * pNamesIn[], char * SeeAlso [] ***********************************************************************/ -void Ft_FactorPrint_rec( FILE * pFile, Vec_Int_t * vForm, Ft_Node_t * pNode, int fCompl, char * pNamesIn[], int * pPos, int LitSizeMax ) +void Dec_GraphPrint_rec( FILE * pFile, Dec_Graph_t * pGraph, Dec_Node_t * pNode, int fCompl, char * pNamesIn[], int * pPos, int LitSizeMax ) { - Ft_Node_t * pNode0, * pNode1; - - if ( pNode->fConst ) // FT_NODE_0 ) + Dec_Node_t * pNode0, * pNode1; + pNode0 = Dec_GraphNode(pGraph, pNode->eEdge0.Node); + pNode1 = Dec_GraphNode(pGraph, pNode->eEdge1.Node); + if ( Dec_GraphNodeIsVar(pGraph, pNode) ) // FT_NODE_LEAF ) { - if ( fCompl ) - fprintf( pFile, "Constant 0" ); - else - fprintf( pFile, "Constant 1" ); + (*pPos) += Dec_GraphPrintGetLeafName( pFile, Dec_GraphNodeInt(pGraph,pNode), fCompl, pNamesIn ); return; } - if ( !pNode->fIntern ) // FT_NODE_LEAF ) - { - (*pPos) += Ft_FactorPrintGetLeafName( pFile, vForm, pNode, fCompl, pNamesIn ); - return; - } - - pNode0 = Ft_NodeFanin0( vForm, pNode ); - pNode1 = Ft_NodeFanin1( vForm, pNode ); if ( !pNode->fNodeOr ) // FT_NODE_AND ) { if ( !pNode0->fNodeOr ) // != FT_NODE_OR ) - Ft_FactorPrint_rec( pFile, vForm, pNode0, pNode->fEdge0, pNamesIn, pPos, LitSizeMax ); + Dec_GraphPrint_rec( pFile, pGraph, pNode0, pNode->fCompl0, pNamesIn, pPos, LitSizeMax ); else { fprintf( pFile, "(" ); (*pPos)++; - Ft_FactorPrint_rec( pFile, vForm, pNode0, pNode->fEdge0, pNamesIn, pPos, LitSizeMax ); + Dec_GraphPrint_rec( pFile, pGraph, pNode0, pNode->fCompl0, pNamesIn, pPos, LitSizeMax ); fprintf( pFile, ")" ); (*pPos)++; } fprintf( pFile, " " ); (*pPos)++; - Ft_FactorPrintUpdatePos( pFile, pPos, LitSizeMax ); + Dec_GraphPrintUpdatePos( pFile, pPos, LitSizeMax ); if ( !pNode1->fNodeOr ) // != FT_NODE_OR ) - Ft_FactorPrint_rec( pFile, vForm, pNode1, pNode->fEdge1, pNamesIn, pPos, LitSizeMax ); + Dec_GraphPrint_rec( pFile, pGraph, pNode1, pNode->fCompl1, pNamesIn, pPos, LitSizeMax ); else { fprintf( pFile, "(" ); (*pPos)++; - Ft_FactorPrint_rec( pFile, vForm, pNode1, pNode->fEdge1, pNamesIn, pPos, LitSizeMax ); + Dec_GraphPrint_rec( pFile, pGraph, pNode1, pNode->fCompl1, pNamesIn, pPos, LitSizeMax ); fprintf( pFile, ")" ); (*pPos)++; } @@ -154,13 +142,13 @@ void Ft_FactorPrint_rec( FILE * pFile, Vec_Int_t * vForm, Ft_Node_t * pNode, int } if ( pNode->fNodeOr ) // FT_NODE_OR ) { - Ft_FactorPrint_rec( pFile, vForm, pNode0, pNode->fEdge0, pNamesIn, pPos, LitSizeMax ); + Dec_GraphPrint_rec( pFile, pGraph, pNode0, pNode->fCompl0, pNamesIn, pPos, LitSizeMax ); fprintf( pFile, " + " ); (*pPos) += 3; - Ft_FactorPrintUpdatePos( pFile, pPos, LitSizeMax ); + Dec_GraphPrintUpdatePos( pFile, pPos, LitSizeMax ); - Ft_FactorPrint_rec( pFile, vForm, pNode1, pNode->fEdge1, pNamesIn, pPos, LitSizeMax ); + Dec_GraphPrint_rec( pFile, pGraph, pNode1, pNode->fCompl1, pNamesIn, pPos, LitSizeMax ); return; } assert( 0 ); @@ -177,13 +165,10 @@ void Ft_FactorPrint_rec( FILE * pFile, Vec_Int_t * vForm, Ft_Node_t * pNode, int SeeAlso [] ***********************************************************************/ -int Ft_FactorPrintGetLeafName( FILE * pFile, Vec_Int_t * vForm, Ft_Node_t * pNode, int fCompl, char * pNamesIn[] ) +int Dec_GraphPrintGetLeafName( FILE * pFile, int iLeaf, int fCompl, char * pNamesIn[] ) { static char Buffer[100]; - int iVar; - assert( !Ptr_IsComplement(pNode) ); - iVar = (Ft_Node_t *)pNode - (Ft_Node_t *)vForm->pArray; - sprintf( Buffer, "%s%s", pNamesIn[iVar], fCompl? "\'" : "" ); + sprintf( Buffer, "%s%s", pNamesIn[iLeaf], fCompl? "\'" : "" ); fprintf( pFile, "%s", Buffer ); return strlen( Buffer ); } @@ -199,7 +184,7 @@ int Ft_FactorPrintGetLeafName( FILE * pFile, Vec_Int_t * vForm, Ft_Node_t * pNod SeeAlso [] ***********************************************************************/ -void Ft_FactorPrintUpdatePos( FILE * pFile, int * pPos, int LitSizeMax ) +void Dec_GraphPrintUpdatePos( FILE * pFile, int * pPos, int LitSizeMax ) { int i; if ( *pPos + LitSizeMax < 77 ) @@ -212,7 +197,7 @@ void Ft_FactorPrintUpdatePos( FILE * pFile, int * pPos, int LitSizeMax ) /**Function************************************************************* - Synopsis [Starts the printout for a factored form or cover.] + Synopsis [Starts the printout for a decomposition graph.] Description [] @@ -221,7 +206,7 @@ void Ft_FactorPrintUpdatePos( FILE * pFile, int * pPos, int LitSizeMax ) SeeAlso [] ***********************************************************************/ -int Ft_FactorPrintOutputName( FILE * pFile, char * pNameOut, int fCompl ) +int Dec_GraphPrintOutputName( FILE * pFile, char * pNameOut, int fCompl ) { if ( pNameOut == NULL ) return 0; diff --git a/src/opt/dec/decUtil.c b/src/opt/dec/decUtil.c new file mode 100644 index 00000000..02c3346e --- /dev/null +++ b/src/opt/dec/decUtil.c @@ -0,0 +1,134 @@ +/**CFile**************************************************************** + + FileName [decUtil.c] + + PackageName [MVSIS 2.0: Multi-valued logic synthesis system.] + + Synopsis [Decomposition unitilies.] + + Author [MVSIS Group] + + Affiliation [UC Berkeley] + + Date [Ver. 1.0. Started - February 1, 2003.] + + Revision [$Id: decUtil.c,v 1.1 2003/05/22 19:20:05 alanmi Exp $] + +***********************************************************************/ + +#include "abc.h" +#include "dec.h" + +//////////////////////////////////////////////////////////////////////// +/// DECLARATIONS /// +//////////////////////////////////////////////////////////////////////// + +//////////////////////////////////////////////////////////////////////// +/// FUNCTION DEFITIONS /// +//////////////////////////////////////////////////////////////////////// + +/**Function************************************************************* + + Synopsis [Converts graph to BDD.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +DdNode * Dec_GraphDeriveBdd( DdManager * dd, Dec_Graph_t * pGraph ) +{ + DdNode * bFunc, * bFunc0, * bFunc1; + Dec_Node_t * pNode; + int i; + + // sanity checks + assert( Dec_GraphLeaveNum(pGraph) >= 0 ); + assert( Dec_GraphLeaveNum(pGraph) <= pGraph->nSize ); + + // check for constant function + if ( Dec_GraphIsConst(pGraph) ) + return Cudd_NotCond( b1, Dec_GraphIsComplement(pGraph) ); + // check for a literal + if ( Dec_GraphIsVar(pGraph) ) + return Cudd_NotCond( Cudd_bddIthVar(dd, Dec_GraphVarInt(pGraph)), Dec_GraphIsComplement(pGraph) ); + + // assign the elementary variables + Dec_GraphForEachLeaf( pGraph, pNode, i ) + pNode->pFunc = Cudd_bddIthVar( dd, i ); + + // compute the function for each internal node + Dec_GraphForEachNode( pGraph, pNode, i ) + { + bFunc0 = Cudd_NotCond( Dec_GraphNode(pGraph, pNode->eEdge0.Node)->pFunc, pNode->eEdge0.fCompl ); + bFunc1 = Cudd_NotCond( Dec_GraphNode(pGraph, pNode->eEdge1.Node)->pFunc, pNode->eEdge1.fCompl ); + pNode->pFunc = Cudd_bddAnd( dd, bFunc0, bFunc1 ); Cudd_Ref( pNode->pFunc ); + } + + // deref the intermediate results + bFunc = pNode->pFunc; Cudd_Ref( bFunc ); + Dec_GraphForEachNode( pGraph, pNode, i ) + Cudd_RecursiveDeref( dd, pNode->pFunc ); + Cudd_Deref( bFunc ); + + // complement the result if necessary + return Cudd_NotCond( bFunc, Dec_GraphIsComplement(pGraph) ); +} + +/**Function************************************************************* + + Synopsis [Derives the truth table.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +unsigned Dec_GraphDeriveTruth( Dec_Graph_t * pGraph ) +{ + unsigned uTruths[5] = { 0xAAAAAAAA, 0xCCCCCCCC, 0xF0F0F0F0, 0xFF00FF00, 0xFFFF0000 }; + unsigned uTruth, uTruth0, uTruth1; + Dec_Node_t * pNode; + int i; + + // sanity checks + assert( Dec_GraphLeaveNum(pGraph) >= 0 ); + assert( Dec_GraphLeaveNum(pGraph) <= pGraph->nSize ); + assert( Dec_GraphLeaveNum(pGraph) <= 5 ); + + // check for constant function + if ( Dec_GraphIsConst(pGraph) ) + return Dec_GraphIsComplement(pGraph)? 0 : ~((unsigned)0); + // check for a literal + if ( Dec_GraphIsVar(pGraph) ) + return Dec_GraphIsComplement(pGraph)? ~uTruths[Dec_GraphVarInt(pGraph)] : uTruths[Dec_GraphVarInt(pGraph)]; + + // assign the elementary variables + Dec_GraphForEachLeaf( pGraph, pNode, i ) + pNode->pFunc = (void *)uTruths[i]; + + // compute the function for each internal node + Dec_GraphForEachNode( pGraph, pNode, i ) + { + uTruth0 = (unsigned)Dec_GraphNode(pGraph, pNode->eEdge0.Node)->pFunc; + uTruth1 = (unsigned)Dec_GraphNode(pGraph, pNode->eEdge1.Node)->pFunc; + uTruth0 = pNode->eEdge0.fCompl? ~uTruth0 : uTruth0; + uTruth1 = pNode->eEdge1.fCompl? ~uTruth1 : uTruth1; + uTruth = uTruth0 & uTruth1; + pNode->pFunc = (void *)uTruth; + } + + // complement the result if necessary + return Dec_GraphIsComplement(pGraph)? ~uTruth : uTruth; +} + + +//////////////////////////////////////////////////////////////////////// +/// END OF FILE /// +//////////////////////////////////////////////////////////////////////// + + diff --git a/src/opt/dec/module.make b/src/opt/dec/module.make index d6d908e7..1e0722d5 100644 --- a/src/opt/dec/module.make +++ b/src/opt/dec/module.make @@ -1 +1,5 @@ -SRC += +SRC += src/opt/dec/decAbc.c \ + src/opt/dec/decFactor.c \ + src/opt/dec/decMan.c \ + src/opt/dec/decPrint.c \ + src/opt/dec/decUtil.c diff --git a/src/opt/rwr/rwr.h b/src/opt/rwr/rwr.h index b9bab47f..6d1a6c06 100644 --- a/src/opt/rwr/rwr.h +++ b/src/opt/rwr/rwr.h @@ -63,7 +63,7 @@ struct Rwr_Man_t_ int nClasses; // the number of NN classes // the result of resynthesis int fCompl; // indicates if the output of FF should be complemented - Vec_Int_t * vForm; // the decomposition tree (temporary) + void * pGraph; // the decomposition tree (temporary) Vec_Ptr_t * vFanins; // the fanins array (temporary) Vec_Ptr_t * vFaninsCur; // the fanins array (temporary) Vec_Int_t * vLevNums; // the array of levels (temporary) @@ -125,8 +125,7 @@ extern void Rwr_ManIncTravId( Rwr_Man_t * p ); extern Rwr_Man_t * Rwr_ManStart( bool fPrecompute ); extern void Rwr_ManStop( Rwr_Man_t * p ); extern void Rwr_ManPrintStats( Rwr_Man_t * p ); -extern Vec_Ptr_t * Rwr_ManReadFanins( Rwr_Man_t * p ); -extern Vec_Int_t * Rwr_ManReadDecs( Rwr_Man_t * p ); +extern void * Rwr_ManReadDecs( Rwr_Man_t * p ); extern int Rwr_ManReadCompl( Rwr_Man_t * p ); extern void Rwr_ManAddTimeCuts( Rwr_Man_t * p, int Time ); extern void Rwr_ManAddTimeTotal( Rwr_Man_t * p, int Time ); diff --git a/src/opt/rwr/rwrDec.c b/src/opt/rwr/rwrDec.c index 9cfc9659..d072879d 100644 --- a/src/opt/rwr/rwrDec.c +++ b/src/opt/rwr/rwrDec.c @@ -19,15 +19,14 @@ ***********************************************************************/ #include "rwr.h" -#include "ft.h" +#include "dec.h" //////////////////////////////////////////////////////////////////////// /// DECLARATIONS /// //////////////////////////////////////////////////////////////////////// -static Vec_Int_t * Rwr_NodePreprocess( Rwr_Man_t * p, Rwr_Node_t * pNode ); -static int Rwr_TravCollect_rec( Rwr_Man_t * p, Rwr_Node_t * pNode, Vec_Int_t * vForm ); -static void Rwr_FactorVerify( Vec_Int_t * vForm, unsigned uTruth ); +static Dec_Graph_t * Rwr_NodePreprocess( Rwr_Man_t * p, Rwr_Node_t * pNode ); +static Dec_Edge_t Rwr_TravCollect_rec( Rwr_Man_t * p, Rwr_Node_t * pNode, Dec_Graph_t * pGraph ); //////////////////////////////////////////////////////////////////////// /// FUNCTION DEFITIONS /// @@ -46,6 +45,7 @@ static void Rwr_FactorVerify( Vec_Int_t * vForm, unsigned uTruth ); ***********************************************************************/ void Rwr_ManPreprocess( Rwr_Man_t * p ) { + Dec_Graph_t * pGraph; Rwr_Node_t * pNode; int i, k; // put the nodes into the structure @@ -62,9 +62,13 @@ void Rwr_ManPreprocess( Rwr_Man_t * p ) Vec_VecPush( p->vClasses, p->pMap[pNode->uTruth], pNode ); } } - // compute decomposition forms for each node + // compute decomposition forms for each node and verify them Vec_VecForEachEntry( p->vClasses, pNode, i, k ) - pNode->pNext = (Rwr_Node_t *)Rwr_NodePreprocess( p, pNode ); + { + pGraph = Rwr_NodePreprocess( p, pNode ); + pNode->pNext = (Rwr_Node_t *)pGraph; + assert( pNode->uTruth == (Dec_GraphDeriveTruth(pGraph) & 0xFFFF) ); + } } /**Function************************************************************* @@ -78,28 +82,24 @@ void Rwr_ManPreprocess( Rwr_Man_t * p ) SeeAlso [] ***********************************************************************/ -Vec_Int_t * Rwr_NodePreprocess( Rwr_Man_t * p, Rwr_Node_t * pNode ) +Dec_Graph_t * Rwr_NodePreprocess( Rwr_Man_t * p, Rwr_Node_t * pNode ) { - Vec_Int_t * vForm; - int i, Root; + Dec_Graph_t * pGraph; + Dec_Edge_t eRoot; + assert( !Rwr_IsComplement(pNode) ); // consider constant if ( pNode->uTruth == 0 ) - return Ft_FactorConst( 0 ); + return Dec_GraphCreateConst0(); // consider the case of elementary var if ( pNode->uTruth == 0x00FF ) - return Ft_FactorVar( 3, 4, 1 ); - // start the factored form - vForm = Vec_IntAlloc( 10 ); - for ( i = 0; i < 4; i++ ) - Vec_IntPush( vForm, 0 ); + return Dec_GraphCreateLeaf( 3, 4, 1 ); + // start the subgraphs + pGraph = Dec_GraphCreate( 4 ); // collect the nodes Rwr_ManIncTravId( p ); - Root = Rwr_TravCollect_rec( p, pNode, vForm ); - if ( Root & 1 ) - Ft_FactorComplement( vForm ); - // verify the factored form - Rwr_FactorVerify( vForm, pNode->uTruth ); - return vForm; + eRoot = Rwr_TravCollect_rec( p, pNode, pGraph ); + Dec_GraphSetRoot( pGraph, eRoot ); + return pGraph; } /**Function************************************************************* @@ -113,115 +113,31 @@ Vec_Int_t * Rwr_NodePreprocess( Rwr_Man_t * p, Rwr_Node_t * pNode ) SeeAlso [] ***********************************************************************/ -int Rwr_TravCollect_rec( Rwr_Man_t * p, Rwr_Node_t * pNode, Vec_Int_t * vForm ) +Dec_Edge_t Rwr_TravCollect_rec( Rwr_Man_t * p, Rwr_Node_t * pNode, Dec_Graph_t * pGraph ) { - Ft_Node_t Node, NodeA, NodeB; - int Node0, Node1; + Dec_Edge_t eNode0, eNode1, eNode; // elementary variable if ( pNode->fUsed ) - return ((pNode->Id - 1) << 1); + return Dec_EdgeCreate( pNode->Id - 1, 0 ); // previously visited node if ( pNode->TravId == p->nTravIds ) - return pNode->Volume; + return Dec_IntToEdge( pNode->Volume ); pNode->TravId = p->nTravIds; // solve for children - Node0 = Rwr_TravCollect_rec( p, Rwr_Regular(pNode->p0), vForm ); - Node1 = Rwr_TravCollect_rec( p, Rwr_Regular(pNode->p1), vForm ); + eNode0 = Rwr_TravCollect_rec( p, Rwr_Regular(pNode->p0), pGraph ); + if ( Rwr_IsComplement(pNode->p0) ) + eNode0.fCompl = !eNode0.fCompl; + eNode1 = Rwr_TravCollect_rec( p, Rwr_Regular(pNode->p1), pGraph ); + if ( Rwr_IsComplement(pNode->p1) ) + eNode1.fCompl = !eNode1.fCompl; // create the decomposition node(s) if ( pNode->fExor ) - { - assert( !Rwr_IsComplement(pNode->p0) ); - assert( !Rwr_IsComplement(pNode->p1) ); - NodeA.fIntern = 1; - NodeA.fConst = 0; - NodeA.fCompl = 0; - NodeA.fCompl0 = !(Node0 & 1); - NodeA.fCompl1 = (Node1 & 1); - NodeA.iFanin0 = (Node0 >> 1); - NodeA.iFanin1 = (Node1 >> 1); - Vec_IntPush( vForm, Ft_Node2Int(NodeA) ); - - NodeB.fIntern = 1; - NodeB.fConst = 0; - NodeB.fCompl = 0; - NodeB.fCompl0 = (Node0 & 1); - NodeB.fCompl1 = !(Node1 & 1); - NodeB.iFanin0 = (Node0 >> 1); - NodeB.iFanin1 = (Node1 >> 1); - Vec_IntPush( vForm, Ft_Node2Int(NodeB) ); - - Node.fIntern = 1; - Node.fConst = 0; - Node.fCompl = 0; - Node.fCompl0 = 1; - Node.fCompl1 = 1; - Node.iFanin0 = vForm->nSize - 2; - Node.iFanin1 = vForm->nSize - 1; - Vec_IntPush( vForm, Ft_Node2Int(Node) ); - } + eNode = Dec_GraphAddNodeXor( pGraph, eNode0, eNode1 ); else - { - Node.fIntern = 1; - Node.fConst = 0; - Node.fCompl = 0; - Node.fCompl0 = Rwr_IsComplement(pNode->p0) ^ (Node0 & 1); - Node.fCompl1 = Rwr_IsComplement(pNode->p1) ^ (Node1 & 1); - Node.iFanin0 = (Node0 >> 1); - Node.iFanin1 = (Node1 >> 1); - Vec_IntPush( vForm, Ft_Node2Int(Node) ); - } - // save the number of this node - pNode->Volume = ((vForm->nSize - 1) << 1) | pNode->fExor; - return pNode->Volume; -} - -/**Function************************************************************* - - Synopsis [Verifies the factored form.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -void Rwr_FactorVerify( Vec_Int_t * vForm, unsigned uTruthGold ) -{ - Ft_Node_t * pFtNode; - Vec_Int_t * vTruths; - unsigned uTruth, uTruth0, uTruth1; - int i; - - vTruths = Vec_IntAlloc( vForm->nSize ); - Vec_IntPush( vTruths, 0xAAAA ); - Vec_IntPush( vTruths, 0xCCCC ); - Vec_IntPush( vTruths, 0xF0F0 ); - Vec_IntPush( vTruths, 0xFF00 ); - - assert( Ft_FactorGetNumVars( vForm ) == 4 ); - for ( i = 4; i < vForm->nSize; i++ ) - { - pFtNode = Ft_NodeRead( vForm, i ); - // make sure there are no elementary variables - assert( pFtNode->iFanin0 != pFtNode->iFanin1 ); - - uTruth0 = vTruths->pArray[pFtNode->iFanin0]; - uTruth0 = pFtNode->fCompl0? ~uTruth0 : uTruth0; - - uTruth1 = vTruths->pArray[pFtNode->iFanin1]; - uTruth1 = pFtNode->fCompl1? ~uTruth1 : uTruth1; - - uTruth = uTruth0 & uTruth1; - Vec_IntPush( vTruths, uTruth ); - } - // complement if necessary - if ( pFtNode->fCompl ) - uTruth = ~uTruth; - uTruth &= 0xFFFF; - if ( uTruth != uTruthGold ) - printf( "Verification failed\n" ); - Vec_IntFree( vTruths ); + eNode = Dec_GraphAddNodeAnd( pGraph, eNode0, eNode1 ); + // save the result + pNode->Volume = Dec_EdgeToInt( eNode ); + return eNode; } //////////////////////////////////////////////////////////////////////// diff --git a/src/opt/rwr/rwrEva.c b/src/opt/rwr/rwrEva.c index 735232af..c934dfd8 100644 --- a/src/opt/rwr/rwrEva.c +++ b/src/opt/rwr/rwrEva.c @@ -19,13 +19,13 @@ ***********************************************************************/ #include "rwr.h" -#include "ft.h" +#include "dec.h" //////////////////////////////////////////////////////////////////////// /// DECLARATIONS /// //////////////////////////////////////////////////////////////////////// -static Vec_Int_t * Rwr_CutEvaluate( Rwr_Man_t * p, Abc_Obj_t * pRoot, Cut_Cut_t * pCut, Vec_Ptr_t * vFaninsCur, int nNodesSaved, int LevelMax, int * pGainBest ); +static Dec_Graph_t * Rwr_CutEvaluate( Rwr_Man_t * p, Abc_Obj_t * pRoot, Cut_Cut_t * pCut, Vec_Ptr_t * vFaninsCur, int nNodesSaved, int LevelMax, int * pGainBest ); //////////////////////////////////////////////////////////////////////// /// FUNCTION DEFITIONS /// @@ -40,8 +40,8 @@ static Vec_Int_t * Rwr_CutEvaluate( Rwr_Man_t * p, Abc_Obj_t * pRoot, Cut_Cut_t structures precomputed and stored in the RWR manager. Determines the best rewriting and computes the gain in the number of AIG nodes in the final network. In the end, p->vFanins contains information - about the best cut that can be used for rewriting, while p->vForm gives - the decomposition tree (represented using factored form data structure). + about the best cut that can be used for rewriting, while p->pGraph gives + the decomposition dag (represented using decomposition graph data structure). Returns gain in the number of nodes or -1 if node cannot be rewritten.] SideEffects [] @@ -52,14 +52,14 @@ static Vec_Int_t * Rwr_CutEvaluate( Rwr_Man_t * p, Abc_Obj_t * pRoot, Cut_Cut_t int Rwr_NodeRewrite( Rwr_Man_t * p, Cut_Man_t * pManCut, Abc_Obj_t * pNode, int fUseZeros ) { int fVeryVerbose = 0; - Vec_Int_t * vForm; + Dec_Graph_t * pGraph; Cut_Cut_t * pCut; Abc_Obj_t * pFanin; unsigned uPhase, uTruthBest; char * pPerm; int Required, nNodesSaved; int i, GainCur, GainBest = -1; - int clk; + int clk, clk2; p->nNodesConsidered++; // get the required times @@ -109,14 +109,16 @@ clk = clock(); Abc_ObjRegular(pFanin)->vFanouts.nSize--; // evaluate the cut - vForm = Rwr_CutEvaluate( p, pNode, pCut, p->vFaninsCur, nNodesSaved, Required, &GainCur ); +clk2 = clock(); + pGraph = Rwr_CutEvaluate( p, pNode, pCut, p->vFaninsCur, nNodesSaved, Required, &GainCur ); +p->timeEval += clock() - clk2; // check if the cut is better than the current best one - if ( vForm != NULL && GainBest < GainCur ) + if ( pGraph != NULL && GainBest < GainCur ) { // save this form GainBest = GainCur; - p->vForm = vForm; + p->pGraph = pGraph; p->fCompl = ((uPhase & (1<<4)) > 0); uTruthBest = pCut->uTruth; // collect fanins in the @@ -127,8 +129,12 @@ clk = clock(); } p->timeRes += clock() - clk; - if ( GainBest == -1 || GainBest == 0 && !fUseZeros ) - return GainBest; + if ( GainBest == -1 ) + return -1; + + // copy the leaves + Vec_PtrForEachEntry( p->vFanins, pFanin, i ) + Dec_GraphNode(p->pGraph, i)->pFunc = pFanin; p->nScores[p->pMap[uTruthBest]]++; p->nNodesRewritten++; @@ -139,7 +145,7 @@ p->timeRes += clock() - clk; { printf( "Node %6s : ", Abc_ObjName(pNode) ); printf( "Fanins = %d. ", p->vFanins->nSize ); - printf( "Cone = %2d. ", p->vForm->nSize - 4 ); + printf( "Cone = %2d. ", Dec_GraphNodeNum(p->pGraph) ); printf( "GAIN = %2d. ", GainBest ); printf( "\n" ); } @@ -157,37 +163,40 @@ p->timeRes += clock() - clk; SeeAlso [] ***********************************************************************/ -Vec_Int_t * Rwr_CutEvaluate( Rwr_Man_t * p, Abc_Obj_t * pRoot, Cut_Cut_t * pCut, Vec_Ptr_t * vFaninsCur, int nNodesSaved, int LevelMax, int * pGainBest ) +Dec_Graph_t * Rwr_CutEvaluate( Rwr_Man_t * p, Abc_Obj_t * pRoot, Cut_Cut_t * pCut, Vec_Ptr_t * vFaninsCur, int nNodesSaved, int LevelMax, int * pGainBest ) { Vec_Ptr_t * vSubgraphs; - Vec_Int_t * vFormBest; - Rwr_Node_t * pNode; - int nNodesAdded, GainBest = -1, i; - int clk = clock(); + Dec_Graph_t * pGraphBest, * pGraphCur; + Rwr_Node_t * pNode, * pFanin; + int nNodesAdded, GainBest, i, k; // find the matching class of subgraphs vSubgraphs = Vec_VecEntry( p->vClasses, p->pMap[pCut->uTruth] ); p->nSubgraphs += vSubgraphs->nSize; // determine the best subgraph + GainBest = -1; Vec_PtrForEachEntry( vSubgraphs, pNode, i ) { + // get the current graph + pGraphCur = (Dec_Graph_t *)pNode->pNext; + // copy the leaves + Vec_PtrForEachEntry( vFaninsCur, pFanin, k ) + Dec_GraphNode(pGraphCur, k)->pFunc = pFanin; // detect how many unlabeled nodes will be reused - nNodesAdded = Abc_NodeStrashDecCount( pRoot->pNtk->pManFunc, pRoot, vFaninsCur, - (Vec_Int_t *)pNode->pNext, p->vLevNums, nNodesSaved, LevelMax ); + nNodesAdded = Dec_GraphToNetworkCount( pRoot, pGraphCur, nNodesSaved, LevelMax ); if ( nNodesAdded == -1 ) continue; assert( nNodesSaved >= nNodesAdded ); // count the gain at this node if ( GainBest < nNodesSaved - nNodesAdded ) { - GainBest = nNodesSaved - nNodesAdded; - vFormBest = (Vec_Int_t *)pNode->pNext; + GainBest = nNodesSaved - nNodesAdded; + pGraphBest = pGraphCur; } } -p->timeEval += clock() - clk; if ( GainBest == -1 ) return NULL; *pGainBest = GainBest; - return vFormBest; + return pGraphBest; } //////////////////////////////////////////////////////////////////////// diff --git a/src/opt/rwr/rwrMan.c b/src/opt/rwr/rwrMan.c index d4772812..e7d6fec6 100644 --- a/src/opt/rwr/rwrMan.c +++ b/src/opt/rwr/rwrMan.c @@ -19,6 +19,8 @@ ***********************************************************************/ #include "rwr.h" +#include "main.h" +#include "dec.h" //////////////////////////////////////////////////////////////////////// /// DECLARATIONS /// @@ -41,15 +43,18 @@ ***********************************************************************/ Rwr_Man_t * Rwr_ManStart( bool fPrecompute ) { + Dec_Man_t * pManDec; Rwr_Man_t * p; int clk = clock(); +clk = clock(); p = ALLOC( Rwr_Man_t, 1 ); memset( p, 0, sizeof(Rwr_Man_t) ); p->nFuncs = (1<<16); - // canonical forms, phases, perms -clk = clock(); - Extra_Truth4VarNPN( &p->puCanons, &p->pPhases, &p->pPerms, &p->pMap ); -//PRT( "NPN classes precomputation time", clock() - clk ); + pManDec = Abc_FrameReadManDec(Abc_FrameGetGlobalFrame()); + p->puCanons = pManDec->puCanons; + p->pPhases = pManDec->pPhases; + p->pPerms = pManDec->pPerms; + p->pMap = pManDec->pMap; // initialize practical NPN classes p->pPractical = Rwr_ManGetPractical( p ); // create the table @@ -104,7 +109,7 @@ void Rwr_ManStop( Rwr_Man_t * p ) Rwr_Node_t * pNode; int i, k; Vec_VecForEachEntry( p->vClasses, pNode, i, k ) - Vec_IntFree( (Vec_Int_t *)pNode->pNext ); + Dec_GraphFree( (Dec_Graph_t *)pNode->pNext ); } if ( p->vClasses ) Vec_VecFree( p->vClasses ); Vec_PtrFree( p->vForest ); @@ -115,10 +120,6 @@ void Rwr_ManStop( Rwr_Man_t * p ) free( p->pTable ); free( p->pPractical ); free( p->pPerms4 ); - free( p->puCanons ); - free( p->pPhases ); - free( p->pPerms ); - free( p->pMap ); free( p ); } @@ -173,25 +174,9 @@ void Rwr_ManPrintStats( Rwr_Man_t * p ) SeeAlso [] ***********************************************************************/ -Vec_Ptr_t * Rwr_ManReadFanins( Rwr_Man_t * p ) -{ - return p->vFanins; -} - -/**Function************************************************************* - - Synopsis [Stops the resynthesis manager.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -Vec_Int_t * Rwr_ManReadDecs( Rwr_Man_t * p ) +void * Rwr_ManReadDecs( Rwr_Man_t * p ) { - return p->vForm; + return p->pGraph; } /**Function************************************************************* diff --git a/src/sop/ft/ft.h b/src/sop/ft/ft.h deleted file mode 100644 index da162e99..00000000 --- a/src/sop/ft/ft.h +++ /dev/null @@ -1,109 +0,0 @@ -/**CFile**************************************************************** - - FileName [ft.h] - - PackageName [MVSIS 2.0: Multi-valued logic synthesis system.] - - Synopsis [Data structure for algebraic factoring.] - - Author [MVSIS Group] - - Affiliation [UC Berkeley] - - Date [Ver. 1.0. Started - February 1, 2003.] - - Revision [$Id: ft.h,v 1.1 2003/05/22 19:20:04 alanmi Exp $] - -***********************************************************************/ - -#ifndef __FT_H__ -#define __FT_H__ - -//////////////////////////////////////////////////////////////////////// -/// INCLUDES /// -//////////////////////////////////////////////////////////////////////// - -//////////////////////////////////////////////////////////////////////// -/// PARAMETERS /// -//////////////////////////////////////////////////////////////////////// - -//////////////////////////////////////////////////////////////////////// -/// STRUCTURE DEFINITIONS /// -//////////////////////////////////////////////////////////////////////// - -typedef struct Ft_Node_t_ Ft_Node_t; -struct Ft_Node_t_ -{ - // the first child - unsigned fCompl0 : 1; // complemented attribute - unsigned iFanin0 : 11; // fanin number - // the second child - unsigned fCompl1 : 1; // complemented attribute - unsigned iFanin1 : 11; // fanin number (1-based) - // other info - unsigned fIntern : 1; // marks any node that is not an elementary var - unsigned fConst : 1; // marks the constant 1 function - unsigned fCompl : 1; // marks the complement of topmost node - // printing info - 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 unused -}; - -/* - The factored form of an SOP is an array (Vec_Int_t) of entries of type Ft_Node_t. - If the SOP has n input variables (some of them may not be in the true support) - the first n entries of the factored form array are zeros. The other entries of the array - represent the internal AND nodes of the factored form, and possibly the constant node. - This representation makes it easy to translate the factored form into an AIG. - The factored AND nodes contains fanins of the node and their complemented attributes - (using AIG semantics). The elementary variable (buffer or interver) are represented - as a node with the same fanins. For example: x' = AND( x', x' ). - The constant node is represented a special node with the constant flag set. - If the constant node and the elementary variable are present, no other internal - AND nodes are allowed in the factored form. -*/ - -// working with complemented attributes of objects -static inline bool Ptr_IsComplement( void * p ) { return (bool)(((unsigned)p) & 01); } -static inline void * Ptr_Regular( void * p ) { return (void *)((unsigned)(p) & ~01); } -static inline void * Ptr_Not( void * p ) { return (void *)((unsigned)(p) ^ 01); } -static inline void * Ptr_NotCond( void * p, int c ) { return (void *)((unsigned)(p) ^ (c)); } - -static inline Ft_Node_t * Ft_NodeRead( Vec_Int_t * vForm, int i ) { return (Ft_Node_t *)vForm->pArray + i; } -static inline Ft_Node_t * Ft_NodeReadLast( Vec_Int_t * vForm ) { return (Ft_Node_t *)vForm->pArray + vForm->nSize - 1; } -static inline Ft_Node_t * Ft_NodeFanin0( Vec_Int_t * vForm, Ft_Node_t * pNode ) { assert( pNode->fIntern ); return (Ft_Node_t *)vForm->pArray + pNode->iFanin0; } -static inline Ft_Node_t * Ft_NodeFanin1( Vec_Int_t * vForm, Ft_Node_t * pNode ) { assert( pNode->fIntern ); return (Ft_Node_t *)vForm->pArray + pNode->iFanin1; } - -static inline Ft_Node_t Ft_Int2Node( int Num ) { return *((Ft_Node_t *)&Num); } -static inline int Ft_Node2Int( Ft_Node_t Node ) { return *((int *)&Node); } -static inline void Ft_NodeClean( Ft_Node_t * pNode ) { *((int *)pNode) = 0; } - -//////////////////////////////////////////////////////////////////////// -/// MACRO DEFITIONS /// -//////////////////////////////////////////////////////////////////////// - -//////////////////////////////////////////////////////////////////////// -/// FUNCTION DEFITIONS /// -//////////////////////////////////////////////////////////////////////// - -/*=== ftFactor.c =====================================================*/ -extern void Ft_FactorStartMan(); -extern void Ft_FactorStopMan(); -extern Vec_Int_t * Ft_Factor( char * pSop ); -extern int Ft_FactorGetNumNodes( Vec_Int_t * vForm ); -extern int Ft_FactorGetNumVars( Vec_Int_t * vForm ); -extern void Ft_FactorComplement( Vec_Int_t * vForm ); -extern Vec_Int_t * Ft_FactorConst( int fConst1 ); -extern Vec_Int_t * Ft_FactorVar( int iVar, int nVars, int fCompl ); -/*=== ftPrint.c =====================================================*/ -extern void Ft_FactorPrint( FILE * pFile, Vec_Int_t * vForm, char * pNamesIn[], char * pNameOut ); - - -//////////////////////////////////////////////////////////////////////// -/// END OF FILE /// -//////////////////////////////////////////////////////////////////////// - -#endif - diff --git a/src/sop/ft/ftFactor.c b/src/sop/ft/ftFactor.c deleted file mode 100644 index 0a32e1c8..00000000 --- a/src/sop/ft/ftFactor.c +++ /dev/null @@ -1,867 +0,0 @@ -/**CFile**************************************************************** - - FileName [ftFactor.c] - - PackageName [MVSIS 2.0: Multi-valued logic synthesis system.] - - Synopsis [Procedures for algebraic factoring.] - - Author [MVSIS Group] - - Affiliation [UC Berkeley] - - Date [Ver. 1.0. Started - February 1, 2003.] - - Revision [$Id: ftFactor.c,v 1.3 2003/09/01 04:56:43 alanmi Exp $] - -***********************************************************************/ - -#include "abc.h" -#include "mvc.h" -#include "ft.h" -#include "dec.h" - -//////////////////////////////////////////////////////////////////////// -/// DECLARATIONS /// -//////////////////////////////////////////////////////////////////////// - -// the types of nodes in FFs -enum { FT_NODE_NONE, FT_NODE_AND, FT_NODE_OR, FT_NODE_INV, FT_NODE_LEAF, FT_NODE_0, FT_NODE_1 }; - -static Ft_Node_t * Ft_Factor_rec( Vec_Int_t * vForm, Mvc_Cover_t * pCover ); -static Ft_Node_t * Ft_FactorLF_rec( Vec_Int_t * vForm, Mvc_Cover_t * pCover, Mvc_Cover_t * pSimple ); - -static Ft_Node_t * Ft_FactorTrivial( Vec_Int_t * vForm, Mvc_Cover_t * pCover ); -static Ft_Node_t * Ft_FactorTrivialCube( Vec_Int_t * vForm, Mvc_Cover_t * pCover, Mvc_Cube_t * pCube ); -static Ft_Node_t * Ft_FactorTrivialTree_rec( Vec_Int_t * vForm, Ft_Node_t ** ppNodes, int nNodes, int fAnd ); -static Ft_Node_t * Ft_FactorTrivialCascade( Vec_Int_t * vForm, Mvc_Cover_t * pCover ); -static Ft_Node_t * Ft_FactorTrivialCubeCascade( Vec_Int_t * vForm, Mvc_Cover_t * pCover, Mvc_Cube_t * pCube ); - -static Ft_Node_t * Ft_FactorNodeCreate( Vec_Int_t * vForm, int Type, Ft_Node_t * pNode1, Ft_Node_t * pNode2 ); -static Ft_Node_t * Ft_FactorLeafCreate( Vec_Int_t * vForm, int iLit ); -static void Ft_FactorFinalize( Vec_Int_t * vForm, Ft_Node_t * pNode, int nVars ); - -// temporary procedures that work with the covers -static Mvc_Cover_t * Ft_ConvertSopToMvc( char * pSop ); -static int Ft_FactorVerify( char * pSop, Vec_Int_t * vForm ); - -// temporary managers -static Mvc_Manager_t * pMem = NULL; -static DdManager * dd = NULL; - -//////////////////////////////////////////////////////////////////////// -/// FUNCTION DEFITIONS /// -//////////////////////////////////////////////////////////////////////// - -/**Function************************************************************* - - Synopsis [Factors the cover.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -Vec_Int_t * Ft_Factor( char * pSop ) -{ - Vec_Int_t * vForm; - Ft_Node_t * pNode; - Mvc_Cover_t * pCover; - int nVars = Abc_SopGetVarNum( pSop ); - - // derive the cover from the SOP representation - pCover = Ft_ConvertSopToMvc( pSop ); - - // make sure the cover is CCS free (should be done before CST) - Mvc_CoverContain( pCover ); - // check for trivial functions - if ( Mvc_CoverIsEmpty(pCover) ) - { - Mvc_CoverFree( pCover ); - return Ft_FactorConst( 0 ); - } - if ( Mvc_CoverIsTautology(pCover) ) - { - Mvc_CoverFree( pCover ); - return Ft_FactorConst( 1 ); - } - - // perform CST - Mvc_CoverInverse( pCover ); // CST - - // start the factored form - vForm = Vec_IntAlloc( 1000 ); - Vec_IntFill( vForm, nVars, 0 ); - // factor the cover - pNode = Ft_Factor_rec( vForm, pCover ); - // finalize the factored form - Ft_FactorFinalize( vForm, pNode, nVars ); - // check if the cover was originally complented - if ( Abc_SopGetPhase(pSop) == 0 ) - Ft_FactorComplement( vForm ); - - // verify the factored form -// if ( !Ft_FactorVerify( pSop, vForm ) ) -// printf( "Verification has failed.\n" ); - -// Mvc_CoverInverse( pCover ); // undo CST - Mvc_CoverFree( pCover ); - return vForm; -} - -/**Function************************************************************* - - Synopsis [Internal recursive factoring procedure.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -Ft_Node_t * Ft_Factor_rec( Vec_Int_t * vForm, Mvc_Cover_t * pCover ) -{ - Mvc_Cover_t * pDiv, * pQuo, * pRem, * pCom; - Ft_Node_t * pNodeDiv, * pNodeQuo, * pNodeRem; - Ft_Node_t * pNodeAnd, * pNode; - - // make sure the cover contains some cubes - assert( Mvc_CoverReadCubeNum(pCover) ); - - // get the divisor - pDiv = Mvc_CoverDivisor( pCover ); - if ( pDiv == NULL ) - return Ft_FactorTrivial( vForm, pCover ); - - // divide the cover by the divisor - Mvc_CoverDivideInternal( pCover, pDiv, &pQuo, &pRem ); - assert( Mvc_CoverReadCubeNum(pQuo) ); - - Mvc_CoverFree( pDiv ); - Mvc_CoverFree( pRem ); - - // check the trivial case - if ( Mvc_CoverReadCubeNum(pQuo) == 1 ) - { - pNode = Ft_FactorLF_rec( vForm, pCover, pQuo ); - Mvc_CoverFree( pQuo ); - return pNode; - } - - // make the quotient cube free - Mvc_CoverMakeCubeFree( pQuo ); - - // divide the cover by the quotient - Mvc_CoverDivideInternal( pCover, pQuo, &pDiv, &pRem ); - - // check the trivial case - if ( Mvc_CoverIsCubeFree( pDiv ) ) - { - pNodeDiv = Ft_Factor_rec( vForm, pDiv ); - pNodeQuo = Ft_Factor_rec( vForm, pQuo ); - Mvc_CoverFree( pDiv ); - Mvc_CoverFree( pQuo ); - pNodeAnd = Ft_FactorNodeCreate( vForm, FT_NODE_AND, pNodeDiv, pNodeQuo ); - if ( Mvc_CoverReadCubeNum(pRem) == 0 ) - { - Mvc_CoverFree( pRem ); - return pNodeAnd; - } - else - { - pNodeRem = Ft_Factor_rec( vForm, pRem ); - Mvc_CoverFree( pRem ); - return Ft_FactorNodeCreate( vForm, FT_NODE_OR, pNodeAnd, pNodeRem ); - } - } - - // get the common cube - pCom = Mvc_CoverCommonCubeCover( pDiv ); - Mvc_CoverFree( pDiv ); - Mvc_CoverFree( pQuo ); - Mvc_CoverFree( pRem ); - - // solve the simple problem - pNode = Ft_FactorLF_rec( vForm, pCover, pCom ); - Mvc_CoverFree( pCom ); - return pNode; -} - - -/**Function************************************************************* - - Synopsis [Internal recursive factoring procedure for the leaf case.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -Ft_Node_t * Ft_FactorLF_rec( Vec_Int_t * vForm, Mvc_Cover_t * pCover, Mvc_Cover_t * pSimple ) -{ - Mvc_Cover_t * pDiv, * pQuo, * pRem; - Ft_Node_t * pNodeDiv, * pNodeQuo, * pNodeRem; - Ft_Node_t * pNodeAnd; - - // get the most often occurring literal - pDiv = Mvc_CoverBestLiteralCover( pCover, pSimple ); - // divide the cover by the literal - Mvc_CoverDivideByLiteral( pCover, pDiv, &pQuo, &pRem ); - // get the node pointer for the literal - pNodeDiv = Ft_FactorTrivialCube( vForm, pDiv, Mvc_CoverReadCubeHead(pDiv) ); - Mvc_CoverFree( pDiv ); - // factor the quotient and remainder - pNodeQuo = Ft_Factor_rec( vForm, pQuo ); - Mvc_CoverFree( pQuo ); - pNodeAnd = Ft_FactorNodeCreate( vForm, FT_NODE_AND, pNodeDiv, pNodeQuo ); - if ( Mvc_CoverReadCubeNum(pRem) == 0 ) - { - Mvc_CoverFree( pRem ); - return pNodeAnd; - } - else - { - pNodeRem = Ft_Factor_rec( vForm, pRem ); - Mvc_CoverFree( pRem ); - return Ft_FactorNodeCreate( vForm, FT_NODE_OR, pNodeAnd, pNodeRem ); - } -} - - - -/**Function************************************************************* - - Synopsis [Factoring the cover, which has no algebraic divisors.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -Ft_Node_t * Ft_FactorTrivial( Vec_Int_t * vForm, Mvc_Cover_t * pCover ) -{ - Ft_Node_t ** ppNodes; - Ft_Node_t * pNode; - Mvc_Cube_t * pCube; - int i, nNodes; - - // create space to put the cubes - nNodes = Mvc_CoverReadCubeNum(pCover); - assert( nNodes > 0 ); - ppNodes = ALLOC( Ft_Node_t *, nNodes ); - // create the factored form for each cube - i = 0; - Mvc_CoverForEachCube( pCover, pCube ) - ppNodes[i++] = Ft_FactorTrivialCube( vForm, pCover, pCube ); - assert( i == nNodes ); - // balance the factored forms - pNode = Ft_FactorTrivialTree_rec( vForm, ppNodes, nNodes, 0 ); - free( ppNodes ); - return pNode; -} - -/**Function************************************************************* - - Synopsis [Factoring the cube.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -Ft_Node_t * Ft_FactorTrivialCube( Vec_Int_t * vForm, Mvc_Cover_t * pCover, Mvc_Cube_t * pCube ) -{ - Ft_Node_t ** ppNodes; - Ft_Node_t * pNode; - int iBit, Value, i; - - // create space to put each literal - ppNodes = ALLOC( Ft_Node_t *, pCover->nBits ); - // create the factored form for each literal - i = 0; - Mvc_CubeForEachBit( pCover, pCube, iBit, Value ) - { - if ( Value ) - ppNodes[i++] = Ft_FactorLeafCreate( vForm, iBit ); - } - assert( i > 0 && i < pCover->nBits ); - // balance the factored forms - pNode = Ft_FactorTrivialTree_rec( vForm, ppNodes, i, 1 ); - free( ppNodes ); - return pNode; -} - -/**Function************************************************************* - - Synopsis [Create the well-balanced tree of nodes.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -Ft_Node_t * Ft_FactorTrivialTree_rec( Vec_Int_t * vForm, Ft_Node_t ** ppNodes, int nNodes, int fAnd ) -{ - Ft_Node_t * pNode1, * pNode2; - int nNodes1, nNodes2; - - if ( nNodes == 1 ) - return ppNodes[0]; - - // split the nodes into two parts - nNodes1 = nNodes/2; - nNodes2 = nNodes - nNodes1; -// nNodes2 = nNodes/2; -// nNodes1 = nNodes - nNodes2; - - // recursively construct the tree for the parts - pNode1 = Ft_FactorTrivialTree_rec( vForm, ppNodes, nNodes1, fAnd ); - pNode2 = Ft_FactorTrivialTree_rec( vForm, ppNodes + nNodes1, nNodes2, fAnd ); - - return Ft_FactorNodeCreate( vForm, fAnd? FT_NODE_AND : FT_NODE_OR, pNode1, pNode2 ); -} - - - -/**Function************************************************************* - - Synopsis [Factoring the cover, which has no algebraic divisors.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -Ft_Node_t * Ft_FactorTrivialCascade( Vec_Int_t * vForm, Mvc_Cover_t * pCover ) -{ - Ft_Node_t * pNode; - Mvc_Cube_t * pCube; - - // iterate through the cubes - pNode = NULL; - Mvc_CoverForEachCube( pCover, pCube ) - { - if ( pNode == NULL ) - pNode = Ft_FactorTrivialCube( vForm, pCover, pCube ); - else - pNode = Ft_FactorNodeCreate( vForm, FT_NODE_OR, pNode, Ft_FactorTrivialCubeCascade( vForm, pCover, pCube ) ); - } - assert( pNode ); // if this assertion fails, the input cover is not SCC-free - return pNode; -} - -/**Function************************************************************* - - Synopsis [Factoring the cube.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -Ft_Node_t * Ft_FactorTrivialCubeCascade( Vec_Int_t * vForm, Mvc_Cover_t * pCover, Mvc_Cube_t * pCube ) -{ - Ft_Node_t * pNode; - int iBit, Value; - - // iterate through the literals - pNode = NULL; - Mvc_CubeForEachBit( pCover, pCube, iBit, Value ) - { - if ( Value ) - { - if ( pNode == NULL ) - pNode = Ft_FactorLeafCreate( vForm, iBit ); - else - pNode = Ft_FactorNodeCreate( vForm, FT_NODE_AND, pNode, Ft_FactorLeafCreate( vForm, iBit ) ); - } - } - assert( pNode ); // if this assertion fails, the input cover is not SCC-free - return pNode; -} - -/**Function************************************************************* - - Synopsis [] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -Ft_Node_t * Ft_FactorNodeCreate( Vec_Int_t * vForm, int Type, Ft_Node_t * pNode1, Ft_Node_t * pNode2 ) -{ - Ft_Node_t * pNode; - // get the new node - Vec_IntPush( vForm, 0 ); - pNode = Ft_NodeReadLast( vForm ); - // set the inputs and other info - pNode->iFanin0 = (Ft_Node_t *)Ptr_Regular(pNode1) - (Ft_Node_t *)vForm->pArray; - pNode->iFanin1 = (Ft_Node_t *)Ptr_Regular(pNode2) - (Ft_Node_t *)vForm->pArray; - assert( pNode->iFanin0 < (unsigned)vForm->nSize ); - assert( pNode->iFanin1 < (unsigned)vForm->nSize ); - pNode->fIntern = 1; - pNode->fCompl = 0; - pNode->fConst = 0; - pNode->fEdge0 = Ptr_IsComplement(pNode1); - pNode->fEdge1 = Ptr_IsComplement(pNode2); - // consider specific gates - if ( Type == FT_NODE_OR ) - { - pNode->fCompl0 = !Ptr_IsComplement(pNode1); - pNode->fCompl1 = !Ptr_IsComplement(pNode2); - pNode->fNodeOr = 1; - return Ptr_Not( pNode ); - } - if ( Type == FT_NODE_AND ) - { - pNode->fCompl0 = Ptr_IsComplement(pNode1); - pNode->fCompl1 = Ptr_IsComplement(pNode2); - pNode->fNodeOr = 0; - return pNode; - } - assert( 0 ); - return NULL; - -/* - Vec_Int_t * vForm; - assert( pNode1 && pNode2 ); - pNode = MEM_ALLOC( vForm->pMem, void, 1 ); - memset( pNode, 0, sizeof(void) ); - pNode->Type = Type; - pNode->pOne = pNode1; - pNode->pTwo = pNode2; - // update FF statistics - if ( pNode->Type == FT_NODE_LEAF ) - vForm->nNodes++; - return pNode; -*/ -} - -/**Function************************************************************* - - Synopsis [Factoring the cube.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -Ft_Node_t * Ft_FactorLeafCreate( Vec_Int_t * vForm, int iLit ) -{ - return Ptr_NotCond( Ft_NodeRead(vForm, iLit/2), iLit%2 ); // using CST - -/* - Vm_VarMap_t * pVm; - int * pValuesFirst, * pValues; - int nValuesIn, nVarsIn; - Vec_Int_t * vForm; - int iVar; - pVm = vForm->pVm; - pValues = Vm_VarMapReadValuesArray(pVm); - pValuesFirst = Vm_VarMapReadValuesFirstArray(pVm); - nValuesIn = Vm_VarMapReadValuesInNum(pVm); - nVarsIn = Vm_VarMapReadVarsInNum(pVm); - assert( iLit < nValuesIn ); - for ( iVar = 0; iVar < nVarsIn; iVar++ ) - if ( iLit < pValuesFirst[iVar] + pValues[iVar] ) - break; - assert( iVar < nVarsIn ); - pNode = Ft_FactorNodeCreate( vForm, FT_NODE_LEAF, NULL, NULL ); - pNode->VarNum = iVar; - pNode->nValues = pValues[iVar]; - pNode->uData = FT_MV_MASK(pNode->nValues) ^ (1 << (iLit - pValuesFirst[iVar])); - return pNode; -*/ -} - - -/**Function************************************************************* - - Synopsis [Adds a single-variable literal if necessary.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -void Ft_FactorFinalize( Vec_Int_t * vForm, Ft_Node_t * pRoot, int nVars ) -{ - Ft_Node_t * pRootR = Ptr_Regular(pRoot); - int iNode = pRootR - (Ft_Node_t *)vForm->pArray; - Ft_Node_t * pNode; - if ( iNode >= nVars ) - { - // set the complemented attribute - pRootR->fCompl = Ptr_IsComplement(pRoot); - return; - } - // create a new node - Vec_IntPush( vForm, 0 ); - pNode = Ft_NodeReadLast( vForm ); - pNode->iFanin0 = iNode; - pNode->iFanin1 = iNode; - pNode->fIntern = 1; - pNode->fCompl = Ptr_IsComplement(pRoot); -} - -/**Function************************************************************* - - Synopsis [Computes the number of variables in the factored form.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -int Ft_FactorGetNumVars( Vec_Int_t * vForm ) -{ - int i; - for ( i = 0; i < vForm->nSize; i++ ) - if ( vForm->pArray[i] ) - break; - return i; -} - -/**Function************************************************************* - - Synopsis [Computes the number of variables in the factored form.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -int Ft_FactorGetNumNodes( Vec_Int_t * vForm ) -{ - Ft_Node_t * pNode; - int i; - pNode = Ft_NodeReadLast(vForm); - if ( pNode->fConst ) - return 0; - if ( !pNode->fConst && pNode->iFanin0 == pNode->iFanin1 ) // literal - return 1; - for ( i = 0; i < vForm->nSize; i++ ) - if ( vForm->pArray[i] ) - break; - return vForm->nSize - i + 1; -} - -/**Function************************************************************* - - Synopsis [Complements the factored form.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -void Ft_FactorComplement( Vec_Int_t * vForm ) -{ - Ft_Node_t * pNode; - pNode = Ft_NodeReadLast(vForm); - pNode->fCompl ^= 1; -} - -/**Function************************************************************* - - Synopsis [Creates a constant 0 or 1 factored form.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -Vec_Int_t * Ft_FactorConst( int fConst1 ) -{ - Vec_Int_t * vForm; - Ft_Node_t * pNode; - // create the constant node - vForm = Vec_IntAlloc( 1 ); - Vec_IntPush( vForm, 0 ); - pNode = Ft_NodeReadLast( vForm ); - pNode->fIntern = 1; - pNode->fConst = 1; - pNode->fCompl = !fConst1; - return vForm; -} - -/**Function************************************************************* - - Synopsis [Creates a constant 0 or 1 factored form.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -Vec_Int_t * Ft_FactorVar( int iVar, int nVars, int fCompl ) -{ - Vec_Int_t * vForm; - Ft_Node_t * pNode; - // create the elementary variable node - vForm = Vec_IntAlloc( nVars + 1 ); - Vec_IntFill( vForm, nVars + 1, 0 ); - pNode = Ft_NodeReadLast( vForm ); - pNode->iFanin0 = iVar; - pNode->iFanin1 = iVar; - pNode->fIntern = 1; - pNode->fCompl = fCompl; - return vForm; -} - - - - - - -/**Function************************************************************* - - Synopsis [Start the MVC manager used in the factoring package.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -void Ft_FactorStartMan() -{ - assert( pMem == NULL ); - pMem = Mvc_ManagerStart(); - dd = Cudd_Init( 0, 0, CUDD_UNIQUE_SLOTS, CUDD_CACHE_SLOTS, 0 ); -} - -/**Function************************************************************* - - Synopsis [Stops the MVC maanager used in the factoring package.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -void Ft_FactorStopMan() -{ - assert( pMem ); - Mvc_ManagerFree( pMem ); - Cudd_Quit( dd ); - pMem = NULL; - dd = NULL; -} - - - - - -/**Function************************************************************* - - Synopsis [Converts SOP into MVC.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -Mvc_Cover_t * Ft_ConvertSopToMvc( char * pSop ) -{ - Mvc_Cover_t * pMvc; - Mvc_Cube_t * pMvcCube; - char * pCube; - int nVars, Value, v; - - // start the cover - nVars = Abc_SopGetVarNum(pSop); - pMvc = Mvc_CoverAlloc( pMem, nVars * 2 ); - // check the logic function of the node - Abc_SopForEachCube( pSop, nVars, pCube ) - { - // create and add the cube - pMvcCube = Mvc_CubeAlloc( pMvc ); - Mvc_CoverAddCubeTail( pMvc, pMvcCube ); - // fill in the literals - Mvc_CubeBitFill( pMvcCube ); - Abc_CubeForEachVar( pCube, Value, v ) - { - if ( Value == '0' ) - Mvc_CubeBitRemove( pMvcCube, v * 2 + 1 ); - else if ( Value == '1' ) - Mvc_CubeBitRemove( pMvcCube, v * 2 ); - } - } -//Mvc_CoverPrint( pMvc ); - return pMvc; -} - - - -/**Function************************************************************* - - Synopsis [Converts SOP into BDD.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -DdNode * Ft_ConvertSopToBdd( DdManager * dd, char * pSop ) -{ - DdNode * bSum, * bCube, * bTemp, * bVar; - char * pCube; - int nVars, Value, v; - // start the cover - nVars = Abc_SopGetVarNum(pSop); - // check the logic function of the node - bSum = Cudd_ReadLogicZero(dd); Cudd_Ref( bSum ); - Abc_SopForEachCube( pSop, nVars, pCube ) - { - bCube = Cudd_ReadOne(dd); Cudd_Ref( bCube ); - Abc_CubeForEachVar( pCube, Value, v ) - { - if ( Value == '0' ) - bVar = Cudd_Not( Cudd_bddIthVar( dd, v ) ); - else if ( Value == '1' ) - bVar = Cudd_bddIthVar( dd, v ); - else - continue; - bCube = Cudd_bddAnd( dd, bTemp = bCube, bVar ); Cudd_Ref( bCube ); - Cudd_RecursiveDeref( dd, bTemp ); - } - bSum = Cudd_bddOr( dd, bTemp = bSum, bCube ); Cudd_Ref( bSum ); - Cudd_RecursiveDeref( dd, bTemp ); - Cudd_RecursiveDeref( dd, bCube ); - } - // complement the result if necessary - bSum = Cudd_NotCond( bSum, !Abc_SopGetPhase(pSop) ); - Cudd_Deref( bSum ); - return bSum; -} - -/**Function************************************************************* - - Synopsis [Converts SOP into BDD.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -DdNode * Ft_ConvertFormToBdd( DdManager * dd, Vec_Int_t * vForm ) -{ - Vec_Ptr_t * vFuncs; - DdNode * bFunc, * bFunc0, * bFunc1; - Ft_Node_t * pNode; - int i, nVars; - - // sanity checks - nVars = Ft_FactorGetNumVars( vForm ); - assert( nVars >= 0 ); - assert( vForm->nSize > nVars ); - - // check for constant function - pNode = Ft_NodeRead( vForm, 0 ); - if ( pNode->fConst ) - return Cudd_NotCond( dd->one, pNode->fCompl ); - - // start the array of elementary variables - vFuncs = Vec_PtrAlloc( 20 ); - for ( i = 0; i < nVars; i++ ) - Vec_PtrPush( vFuncs, Cudd_bddIthVar(dd, i) ); - - // compute the functions of other nodes - for ( i = nVars; i < vForm->nSize; i++ ) - { - pNode = Ft_NodeRead( vForm, i ); - bFunc0 = Cudd_NotCond( vFuncs->pArray[pNode->iFanin0], pNode->fCompl0 ); - bFunc1 = Cudd_NotCond( vFuncs->pArray[pNode->iFanin1], pNode->fCompl1 ); - bFunc = Cudd_bddAnd( dd, bFunc0, bFunc1 ); Cudd_Ref( bFunc ); - Vec_PtrPush( vFuncs, bFunc ); - } - assert( vForm->nSize = vFuncs->nSize ); - - // deref the intermediate results - for ( i = nVars; i < vForm->nSize-1; i++ ) - Cudd_RecursiveDeref( dd, (DdNode *)vFuncs->pArray[i] ); - Vec_PtrFree( vFuncs ); - - // complement the result if necessary - pNode = Ft_NodeReadLast( vForm ); - bFunc = Cudd_NotCond( bFunc, pNode->fCompl ); - - // return the result - Cudd_Deref( bFunc ); - return bFunc; -} - - -/**Function************************************************************* - - Synopsis [Verifies that the factoring is correct.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -int Ft_FactorVerify( char * pSop, Vec_Int_t * vForm ) -{ - DdNode * bFunc1, * bFunc2; - int RetValue; - bFunc1 = Ft_ConvertSopToBdd( dd, pSop ); Cudd_Ref( bFunc1 ); - bFunc2 = Ft_ConvertFormToBdd( dd, vForm ); Cudd_Ref( bFunc2 ); -//Extra_bddPrint( dd, bFunc1 ); printf("\n"); -//Extra_bddPrint( dd, bFunc2 ); printf("\n"); - RetValue = (bFunc1 == bFunc2); - Cudd_RecursiveDeref( dd, bFunc1 ); - Cudd_RecursiveDeref( dd, bFunc2 ); - return RetValue; -} - - -//////////////////////////////////////////////////////////////////////// -/// END OF FILE /// -//////////////////////////////////////////////////////////////////////// - - diff --git a/src/sop/ft/module.make b/src/sop/ft/module.make deleted file mode 100644 index 37e78ce6..00000000 --- a/src/sop/ft/module.make +++ /dev/null @@ -1,2 +0,0 @@ -SRC += src/sop/ft/ftFactor.c \ - src/sop/ft/ftPrint.c |