From ab7cb9c6ad52934b80e44f2bb5ae94049a5a4ae5 Mon Sep 17 00:00:00 2001 From: Alan Mishchenko Date: Wed, 31 Aug 2005 08:01:00 -0700 Subject: Version abc50831 --- abc.dsp | 26 +- abc.opt | Bin 52736 -> 52736 bytes abc.plg | 579 +++++++++++++++ abc.rc | 7 +- src/base/abc/abc.c | 281 +++++++- src/base/abc/abc.h | 25 +- src/base/abc/abcAig.c | 55 ++ src/base/abc/abcCollapse.c | 53 +- src/base/abc/abcCreate.c | 2 +- src/base/abc/abcDsd.c | 74 +- src/base/abc/abcFraig.c | 2 +- src/base/abc/abcFunc.c | 51 ++ src/base/abc/abcMiter.c | 4 +- src/base/abc/abcPrint.c | 4 +- src/base/abc/abcReconv.c | 430 ++++++++--- src/base/abc/abcRefactor.c | 4 +- src/base/abc/abcRefs.c | 4 + src/base/abc/abcShow.c | 211 ++++-- src/base/abc/abcStrash.c | 6 +- src/base/abc/abcSweep.c | 2 +- src/base/abc/abcSymm.c | 202 ++++++ src/base/abc/abcUnreach.c | 7 +- src/base/abc/abcUtil.c | 23 + src/base/abc/module.make | 1 + src/base/io/io.c | 295 +++++++- src/base/io/io.h | 8 + src/base/io/ioRead.c | 2 + src/base/io/ioReadEqn.c | 254 +++++++ src/base/io/ioWriteBlif.c | 5 +- src/base/io/ioWriteCnf.c | 4 +- src/base/io/ioWriteDot.c | 322 +++++++++ src/base/io/ioWriteEqn.c | 261 +++++++ src/base/io/ioWriteGml.c | 116 +++ src/base/io/module.make | 4 + src/map/fpga/fpgaCore.c | 2 +- src/misc/extra/extra.h | 51 ++ src/misc/extra/extraBddMisc.c | 1046 +++++++++++++++++++++++++++ src/misc/extra/extraBddSymm.c | 1469 ++++++++++++++++++++++++++++++++++++++ src/misc/extra/extraUtilBdd.c | 1046 --------------------------- src/misc/extra/extraUtilReader.c | 1 + src/misc/extra/module.make | 3 +- src/misc/vec/vecVec.h | 21 +- 42 files changed, 5635 insertions(+), 1328 deletions(-) create mode 100644 src/base/abc/abcSymm.c create mode 100644 src/base/io/ioReadEqn.c create mode 100644 src/base/io/ioWriteDot.c create mode 100644 src/base/io/ioWriteEqn.c create mode 100644 src/base/io/ioWriteGml.c create mode 100644 src/misc/extra/extraBddMisc.c create mode 100644 src/misc/extra/extraBddSymm.c delete mode 100644 src/misc/extra/extraUtilBdd.c diff --git a/abc.dsp b/abc.dsp index 65c1eb1a..12d5516e 100644 --- a/abc.dsp +++ b/abc.dsp @@ -237,6 +237,10 @@ SOURCE=.\src\base\abc\abcSweep.c # End Source File # Begin Source File +SOURCE=.\src\base\abc\abcSymm.c +# End Source File +# Begin Source File + SOURCE=.\src\base\abc\abcTiming.c # End Source File # Begin Source File @@ -321,6 +325,10 @@ SOURCE=.\src\base\io\ioReadEdif.c # End Source File # Begin Source File +SOURCE=.\src\base\io\ioReadEqn.c +# End Source File +# Begin Source File + SOURCE=.\src\base\io\ioReadPla.c # End Source File # Begin Source File @@ -345,6 +353,18 @@ SOURCE=.\src\base\io\ioWriteCnf.c # End Source File # Begin Source File +SOURCE=.\src\base\io\ioWriteDot.c +# End Source File +# Begin Source File + +SOURCE=.\src\base\io\ioWriteEqn.c +# End Source File +# Begin Source File + +SOURCE=.\src\base\io\ioWriteGml.c +# End Source File +# Begin Source File + SOURCE=.\src\base\io\ioWritePla.c # End Source File # End Group @@ -1413,7 +1433,11 @@ SOURCE=.\src\misc\extra\extra.h # End Source File # Begin Source File -SOURCE=.\src\misc\extra\extraUtilBdd.c +SOURCE=.\src\misc\extra\extraBddMisc.c +# End Source File +# Begin Source File + +SOURCE=.\src\misc\extra\extraBddSymm.c # End Source File # Begin Source File diff --git a/abc.opt b/abc.opt index de47a195..79f5aae4 100644 Binary files a/abc.opt and b/abc.opt differ diff --git a/abc.plg b/abc.plg index 632ed572..c0749e50 100644 --- a/abc.plg +++ b/abc.plg @@ -6,6 +6,585 @@ --------------------Configuration: abc - Win32 Debug--------------------

Command Lines

+Creating temporary file "C:\DOCUME~1\alanmi\LOCALS~1\Temp\RSP358F.tmp" with contents +[ +/nologo /MLd /W3 /Gm /GX /ZI /Od /I "src\base\abc" /I "src\base\cmd" /I "src\base\io" /I "src\base\main" /I "src\bdd\cudd" /I "src\bdd\epd" /I "src\bdd\mtr" /I "src\bdd\parse" /I "src\bdd\dsd" /I "src\bdd\reo" /I "src\sop\mvc" /I "src\sop\ft" /I "src\sat\asat" /I "src\sat\msat" /I "src\sat\fraig" /I "src\opt\fxa" /I "src\opt\fxu" /I "src\opt\rwr" /I "src\opt\cut" /I "src\map\fpga" /I "src\map\mapper" /I "src\map\mio" /I "src\map\super" /I "src\misc\extra" /I "src\misc\st" /I "src\misc\util" /I "src\misc\vec" /D "WIN32" /D "_DEBUG" /D "_CONSOLE" /D "_MBCS" /D "__STDC__" /D "HAVE_ASSERT_H" /FR"Debug/" /Fp"Debug/abc.pch" /YX /Fo"Debug/" /Fd"Debug/" /FD /GZ /c +"C:\_projects\abc\src\base\abc\abc.c" +] +Creating command line "cl.exe @C:\DOCUME~1\alanmi\LOCALS~1\Temp\RSP358F.tmp" +Creating temporary file "C:\DOCUME~1\alanmi\LOCALS~1\Temp\RSP3590.tmp" with contents +[ +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 +.\Debug\abcAig.obj +.\Debug\abcAttach.obj +.\Debug\abcBalance.obj +.\Debug\abcCheck.obj +.\Debug\abcCollapse.obj +.\Debug\abcCreate.obj +.\Debug\abcCut.obj +.\Debug\abcDfs.obj +.\Debug\abcDsd.obj +.\Debug\abcFanio.obj +.\Debug\abcFpga.obj +.\Debug\abcFraig.obj +.\Debug\abcFunc.obj +.\Debug\abcFxu.obj +.\Debug\abcLatch.obj +.\Debug\abcMap.obj +.\Debug\abcMinBase.obj +.\Debug\abcMiter.obj +.\Debug\abcNames.obj +.\Debug\abcNetlist.obj +.\Debug\abcPrint.obj +.\Debug\abcReconv.obj +.\Debug\abcRefactor.obj +.\Debug\abcRefs.obj +.\Debug\abcRenode.obj +.\Debug\abcRewrite.obj +.\Debug\abcSat.obj +.\Debug\abcSeq.obj +.\Debug\abcSeqRetime.obj +.\Debug\abcShow.obj +.\Debug\abcSop.obj +.\Debug\abcStrash.obj +.\Debug\abcSweep.obj +.\Debug\abcSymm.obj +.\Debug\abcTiming.obj +.\Debug\abcUnreach.obj +.\Debug\abcUtil.obj +.\Debug\abcVerify.obj +.\Debug\cmd.obj +.\Debug\cmdAlias.obj +.\Debug\cmdApi.obj +.\Debug\cmdFlag.obj +.\Debug\cmdHist.obj +.\Debug\cmdUtils.obj +.\Debug\io.obj +.\Debug\ioRead.obj +.\Debug\ioReadBench.obj +.\Debug\ioReadBlif.obj +.\Debug\ioReadEdif.obj +.\Debug\ioReadPla.obj +.\Debug\ioReadVerilog.obj +.\Debug\ioUtil.obj +.\Debug\ioWriteBench.obj +.\Debug\ioWriteBlif.obj +.\Debug\ioWriteCnf.obj +.\Debug\ioWritePla.obj +.\Debug\main.obj +.\Debug\mainFrame.obj +.\Debug\mainInit.obj +.\Debug\mainUtils.obj +.\Debug\cuddAddAbs.obj +.\Debug\cuddAddApply.obj +.\Debug\cuddAddFind.obj +.\Debug\cuddAddInv.obj +.\Debug\cuddAddIte.obj +.\Debug\cuddAddNeg.obj +.\Debug\cuddAddWalsh.obj +.\Debug\cuddAndAbs.obj +.\Debug\cuddAnneal.obj +.\Debug\cuddApa.obj +.\Debug\cuddAPI.obj +.\Debug\cuddApprox.obj +.\Debug\cuddBddAbs.obj +.\Debug\cuddBddCorr.obj +.\Debug\cuddBddIte.obj +.\Debug\cuddBridge.obj +.\Debug\cuddCache.obj +.\Debug\cuddCheck.obj +.\Debug\cuddClip.obj +.\Debug\cuddCof.obj +.\Debug\cuddCompose.obj +.\Debug\cuddDecomp.obj +.\Debug\cuddEssent.obj +.\Debug\cuddExact.obj +.\Debug\cuddExport.obj +.\Debug\cuddGenCof.obj +.\Debug\cuddGenetic.obj +.\Debug\cuddGroup.obj +.\Debug\cuddHarwell.obj +.\Debug\cuddInit.obj +.\Debug\cuddInteract.obj +.\Debug\cuddLCache.obj +.\Debug\cuddLevelQ.obj +.\Debug\cuddLinear.obj +.\Debug\cuddLiteral.obj +.\Debug\cuddMatMult.obj +.\Debug\cuddPriority.obj +.\Debug\cuddRead.obj +.\Debug\cuddRef.obj +.\Debug\cuddReorder.obj +.\Debug\cuddSat.obj +.\Debug\cuddSign.obj +.\Debug\cuddSolve.obj +.\Debug\cuddSplit.obj +.\Debug\cuddSubsetHB.obj +.\Debug\cuddSubsetSP.obj +.\Debug\cuddSymmetry.obj +.\Debug\cuddTable.obj +.\Debug\cuddUtil.obj +.\Debug\cuddWindow.obj +.\Debug\cuddZddCount.obj +.\Debug\cuddZddFuncs.obj +.\Debug\cuddZddGroup.obj +.\Debug\cuddZddIsop.obj +.\Debug\cuddZddLin.obj +.\Debug\cuddZddMisc.obj +.\Debug\cuddZddPort.obj +.\Debug\cuddZddReord.obj +.\Debug\cuddZddSetop.obj +.\Debug\cuddZddSymm.obj +.\Debug\cuddZddUtil.obj +.\Debug\epd.obj +.\Debug\mtrBasic.obj +.\Debug\mtrGroup.obj +.\Debug\parseCore.obj +.\Debug\parseStack.obj +.\Debug\dsdApi.obj +.\Debug\dsdCheck.obj +.\Debug\dsdLocal.obj +.\Debug\dsdMan.obj +.\Debug\dsdProc.obj +.\Debug\dsdTree.obj +.\Debug\reoApi.obj +.\Debug\reoCore.obj +.\Debug\reoProfile.obj +.\Debug\reoSift.obj +.\Debug\reoSwap.obj +.\Debug\reoTest.obj +.\Debug\reoTransfer.obj +.\Debug\reoUnits.obj +.\Debug\mvc.obj +.\Debug\mvcApi.obj +.\Debug\mvcCompare.obj +.\Debug\mvcContain.obj +.\Debug\mvcCover.obj +.\Debug\mvcCube.obj +.\Debug\mvcDivide.obj +.\Debug\mvcDivisor.obj +.\Debug\mvcList.obj +.\Debug\mvcLits.obj +.\Debug\mvcMan.obj +.\Debug\mvcOpAlg.obj +.\Debug\mvcOpBool.obj +.\Debug\mvcPrint.obj +.\Debug\mvcSort.obj +.\Debug\mvcUtils.obj +.\Debug\ftFactor.obj +.\Debug\ftPrint.obj +.\Debug\added.obj +.\Debug\solver.obj +.\Debug\msatActivity.obj +.\Debug\msatClause.obj +.\Debug\msatClauseVec.obj +.\Debug\msatMem.obj +.\Debug\msatOrderJ.obj +.\Debug\msatQueue.obj +.\Debug\msatRead.obj +.\Debug\msatSolverApi.obj +.\Debug\msatSolverCore.obj +.\Debug\msatSolverIo.obj +.\Debug\msatSolverSearch.obj +.\Debug\msatSort.obj +.\Debug\msatVec.obj +.\Debug\fraigApi.obj +.\Debug\fraigCanon.obj +.\Debug\fraigFanout.obj +.\Debug\fraigFeed.obj +.\Debug\fraigMan.obj +.\Debug\fraigMem.obj +.\Debug\fraigNode.obj +.\Debug\fraigPrime.obj +.\Debug\fraigSat.obj +.\Debug\fraigTable.obj +.\Debug\fraigUtil.obj +.\Debug\fraigVec.obj +.\Debug\simMan.obj +.\Debug\simSat.obj +.\Debug\simSupp.obj +.\Debug\simSym.obj +.\Debug\simUnate.obj +.\Debug\simUtils.obj +.\Debug\csat_apis.obj +.\Debug\fxu.obj +.\Debug\fxuCreate.obj +.\Debug\fxuHeapD.obj +.\Debug\fxuHeapS.obj +.\Debug\fxuList.obj +.\Debug\fxuMatrix.obj +.\Debug\fxuPair.obj +.\Debug\fxuPrint.obj +.\Debug\fxuReduce.obj +.\Debug\fxuSelect.obj +.\Debug\fxuSingle.obj +.\Debug\fxuUpdate.obj +.\Debug\rwrDec.obj +.\Debug\rwrEva.obj +.\Debug\rwrExp.obj +.\Debug\rwrLib.obj +.\Debug\rwrMan.obj +.\Debug\rwrPrint.obj +.\Debug\rwrUtil.obj +.\Debug\cutMan.obj +.\Debug\cutMerge.obj +.\Debug\cutNode.obj +.\Debug\cutSeq.obj +.\Debug\cutTable.obj +.\Debug\cutTruth.obj +.\Debug\fpga.obj +.\Debug\fpgaCore.obj +.\Debug\fpgaCreate.obj +.\Debug\fpgaCut.obj +.\Debug\fpgaCutUtils.obj +.\Debug\fpgaFanout.obj +.\Debug\fpgaLib.obj +.\Debug\fpgaMatch.obj +.\Debug\fpgaTime.obj +.\Debug\fpgaTruth.obj +.\Debug\fpgaUtils.obj +.\Debug\fpgaVec.obj +.\Debug\mapper.obj +.\Debug\mapperCanon.obj +.\Debug\mapperCore.obj +.\Debug\mapperCreate.obj +.\Debug\mapperCut.obj +.\Debug\mapperCutUtils.obj +.\Debug\mapperFanout.obj +.\Debug\mapperLib.obj +.\Debug\mapperMatch.obj +.\Debug\mapperRefs.obj +.\Debug\mapperSuper.obj +.\Debug\mapperTable.obj +.\Debug\mapperTime.obj +.\Debug\mapperTree.obj +.\Debug\mapperTruth.obj +.\Debug\mapperUtils.obj +.\Debug\mapperVec.obj +.\Debug\mio.obj +.\Debug\mioApi.obj +.\Debug\mioFunc.obj +.\Debug\mioRead.obj +.\Debug\mioUtils.obj +.\Debug\super.obj +.\Debug\superAnd.obj +.\Debug\superGate.obj +.\Debug\superWrite.obj +.\Debug\extraBddMisc.obj +.\Debug\extraBddSymm.obj +.\Debug\extraUtilBitMatrix.obj +.\Debug\extraUtilCanon.obj +.\Debug\extraUtilFile.obj +.\Debug\extraUtilMemory.obj +.\Debug\extraUtilMisc.obj +.\Debug\extraUtilProgress.obj +.\Debug\extraUtilReader.obj +.\Debug\st.obj +.\Debug\stmm.obj +.\Debug\cpu_stats.obj +.\Debug\cpu_time.obj +.\Debug\datalimit.obj +.\Debug\getopt.obj +.\Debug\pathsearch.obj +.\Debug\safe_mem.obj +.\Debug\strsav.obj +.\Debug\texpand.obj +.\Debug\ioWriteGml.obj +.\Debug\ioWriteEqn.obj +.\Debug\ioWriteDot.obj +.\Debug\ioReadEqn.obj +] +Creating command line "link.exe @C:\DOCUME~1\alanmi\LOCALS~1\Temp\RSP3590.tmp" +

Output Window

+Compiling... +abc.c +Linking... +Creating temporary file "C:\DOCUME~1\alanmi\LOCALS~1\Temp\RSP3591.tmp" with contents +[ +/nologo /o"Debug/abc.bsc" +.\Debug\abc.sbr +.\Debug\abcAig.sbr +.\Debug\abcAttach.sbr +.\Debug\abcBalance.sbr +.\Debug\abcCheck.sbr +.\Debug\abcCollapse.sbr +.\Debug\abcCreate.sbr +.\Debug\abcCut.sbr +.\Debug\abcDfs.sbr +.\Debug\abcDsd.sbr +.\Debug\abcFanio.sbr +.\Debug\abcFpga.sbr +.\Debug\abcFraig.sbr +.\Debug\abcFunc.sbr +.\Debug\abcFxu.sbr +.\Debug\abcLatch.sbr +.\Debug\abcMap.sbr +.\Debug\abcMinBase.sbr +.\Debug\abcMiter.sbr +.\Debug\abcNames.sbr +.\Debug\abcNetlist.sbr +.\Debug\abcPrint.sbr +.\Debug\abcReconv.sbr +.\Debug\abcRefactor.sbr +.\Debug\abcRefs.sbr +.\Debug\abcRenode.sbr +.\Debug\abcRewrite.sbr +.\Debug\abcSat.sbr +.\Debug\abcSeq.sbr +.\Debug\abcSeqRetime.sbr +.\Debug\abcShow.sbr +.\Debug\abcSop.sbr +.\Debug\abcStrash.sbr +.\Debug\abcSweep.sbr +.\Debug\abcSymm.sbr +.\Debug\abcTiming.sbr +.\Debug\abcUnreach.sbr +.\Debug\abcUtil.sbr +.\Debug\abcVerify.sbr +.\Debug\cmd.sbr +.\Debug\cmdAlias.sbr +.\Debug\cmdApi.sbr +.\Debug\cmdFlag.sbr +.\Debug\cmdHist.sbr +.\Debug\cmdUtils.sbr +.\Debug\io.sbr +.\Debug\ioRead.sbr +.\Debug\ioReadBench.sbr +.\Debug\ioReadBlif.sbr +.\Debug\ioReadEdif.sbr +.\Debug\ioReadPla.sbr +.\Debug\ioReadVerilog.sbr +.\Debug\ioUtil.sbr +.\Debug\ioWriteBench.sbr +.\Debug\ioWriteBlif.sbr +.\Debug\ioWriteCnf.sbr +.\Debug\ioWritePla.sbr +.\Debug\main.sbr +.\Debug\mainFrame.sbr +.\Debug\mainInit.sbr +.\Debug\mainUtils.sbr +.\Debug\cuddAddAbs.sbr +.\Debug\cuddAddApply.sbr +.\Debug\cuddAddFind.sbr +.\Debug\cuddAddInv.sbr +.\Debug\cuddAddIte.sbr +.\Debug\cuddAddNeg.sbr +.\Debug\cuddAddWalsh.sbr +.\Debug\cuddAndAbs.sbr +.\Debug\cuddAnneal.sbr +.\Debug\cuddApa.sbr +.\Debug\cuddAPI.sbr +.\Debug\cuddApprox.sbr +.\Debug\cuddBddAbs.sbr +.\Debug\cuddBddCorr.sbr +.\Debug\cuddBddIte.sbr +.\Debug\cuddBridge.sbr +.\Debug\cuddCache.sbr +.\Debug\cuddCheck.sbr +.\Debug\cuddClip.sbr +.\Debug\cuddCof.sbr +.\Debug\cuddCompose.sbr +.\Debug\cuddDecomp.sbr +.\Debug\cuddEssent.sbr +.\Debug\cuddExact.sbr +.\Debug\cuddExport.sbr +.\Debug\cuddGenCof.sbr +.\Debug\cuddGenetic.sbr +.\Debug\cuddGroup.sbr +.\Debug\cuddHarwell.sbr +.\Debug\cuddInit.sbr +.\Debug\cuddInteract.sbr +.\Debug\cuddLCache.sbr +.\Debug\cuddLevelQ.sbr +.\Debug\cuddLinear.sbr +.\Debug\cuddLiteral.sbr +.\Debug\cuddMatMult.sbr +.\Debug\cuddPriority.sbr +.\Debug\cuddRead.sbr +.\Debug\cuddRef.sbr +.\Debug\cuddReorder.sbr +.\Debug\cuddSat.sbr +.\Debug\cuddSign.sbr +.\Debug\cuddSolve.sbr +.\Debug\cuddSplit.sbr +.\Debug\cuddSubsetHB.sbr +.\Debug\cuddSubsetSP.sbr +.\Debug\cuddSymmetry.sbr +.\Debug\cuddTable.sbr +.\Debug\cuddUtil.sbr +.\Debug\cuddWindow.sbr +.\Debug\cuddZddCount.sbr +.\Debug\cuddZddFuncs.sbr +.\Debug\cuddZddGroup.sbr +.\Debug\cuddZddIsop.sbr +.\Debug\cuddZddLin.sbr +.\Debug\cuddZddMisc.sbr +.\Debug\cuddZddPort.sbr +.\Debug\cuddZddReord.sbr +.\Debug\cuddZddSetop.sbr +.\Debug\cuddZddSymm.sbr +.\Debug\cuddZddUtil.sbr +.\Debug\epd.sbr +.\Debug\mtrBasic.sbr +.\Debug\mtrGroup.sbr +.\Debug\parseCore.sbr +.\Debug\parseStack.sbr +.\Debug\dsdApi.sbr +.\Debug\dsdCheck.sbr +.\Debug\dsdLocal.sbr +.\Debug\dsdMan.sbr +.\Debug\dsdProc.sbr +.\Debug\dsdTree.sbr +.\Debug\reoApi.sbr +.\Debug\reoCore.sbr +.\Debug\reoProfile.sbr +.\Debug\reoSift.sbr +.\Debug\reoSwap.sbr +.\Debug\reoTest.sbr +.\Debug\reoTransfer.sbr +.\Debug\reoUnits.sbr +.\Debug\mvc.sbr +.\Debug\mvcApi.sbr +.\Debug\mvcCompare.sbr +.\Debug\mvcContain.sbr +.\Debug\mvcCover.sbr +.\Debug\mvcCube.sbr +.\Debug\mvcDivide.sbr +.\Debug\mvcDivisor.sbr +.\Debug\mvcList.sbr +.\Debug\mvcLits.sbr +.\Debug\mvcMan.sbr +.\Debug\mvcOpAlg.sbr +.\Debug\mvcOpBool.sbr +.\Debug\mvcPrint.sbr +.\Debug\mvcSort.sbr +.\Debug\mvcUtils.sbr +.\Debug\ftFactor.sbr +.\Debug\ftPrint.sbr +.\Debug\added.sbr +.\Debug\solver.sbr +.\Debug\msatActivity.sbr +.\Debug\msatClause.sbr +.\Debug\msatClauseVec.sbr +.\Debug\msatMem.sbr +.\Debug\msatOrderJ.sbr +.\Debug\msatQueue.sbr +.\Debug\msatRead.sbr +.\Debug\msatSolverApi.sbr +.\Debug\msatSolverCore.sbr +.\Debug\msatSolverIo.sbr +.\Debug\msatSolverSearch.sbr +.\Debug\msatSort.sbr +.\Debug\msatVec.sbr +.\Debug\fraigApi.sbr +.\Debug\fraigCanon.sbr +.\Debug\fraigFanout.sbr +.\Debug\fraigFeed.sbr +.\Debug\fraigMan.sbr +.\Debug\fraigMem.sbr +.\Debug\fraigNode.sbr +.\Debug\fraigPrime.sbr +.\Debug\fraigSat.sbr +.\Debug\fraigTable.sbr +.\Debug\fraigUtil.sbr +.\Debug\fraigVec.sbr +.\Debug\simMan.sbr +.\Debug\simSat.sbr +.\Debug\simSupp.sbr +.\Debug\simSym.sbr +.\Debug\simUnate.sbr +.\Debug\simUtils.sbr +.\Debug\csat_apis.sbr +.\Debug\fxu.sbr +.\Debug\fxuCreate.sbr +.\Debug\fxuHeapD.sbr +.\Debug\fxuHeapS.sbr +.\Debug\fxuList.sbr +.\Debug\fxuMatrix.sbr +.\Debug\fxuPair.sbr +.\Debug\fxuPrint.sbr +.\Debug\fxuReduce.sbr +.\Debug\fxuSelect.sbr +.\Debug\fxuSingle.sbr +.\Debug\fxuUpdate.sbr +.\Debug\rwrDec.sbr +.\Debug\rwrEva.sbr +.\Debug\rwrExp.sbr +.\Debug\rwrLib.sbr +.\Debug\rwrMan.sbr +.\Debug\rwrPrint.sbr +.\Debug\rwrUtil.sbr +.\Debug\cutMan.sbr +.\Debug\cutMerge.sbr +.\Debug\cutNode.sbr +.\Debug\cutSeq.sbr +.\Debug\cutTable.sbr +.\Debug\cutTruth.sbr +.\Debug\fpga.sbr +.\Debug\fpgaCore.sbr +.\Debug\fpgaCreate.sbr +.\Debug\fpgaCut.sbr +.\Debug\fpgaCutUtils.sbr +.\Debug\fpgaFanout.sbr +.\Debug\fpgaLib.sbr +.\Debug\fpgaMatch.sbr +.\Debug\fpgaTime.sbr +.\Debug\fpgaTruth.sbr +.\Debug\fpgaUtils.sbr +.\Debug\fpgaVec.sbr +.\Debug\mapper.sbr +.\Debug\mapperCanon.sbr +.\Debug\mapperCore.sbr +.\Debug\mapperCreate.sbr +.\Debug\mapperCut.sbr +.\Debug\mapperCutUtils.sbr +.\Debug\mapperFanout.sbr +.\Debug\mapperLib.sbr +.\Debug\mapperMatch.sbr +.\Debug\mapperRefs.sbr +.\Debug\mapperSuper.sbr +.\Debug\mapperTable.sbr +.\Debug\mapperTime.sbr +.\Debug\mapperTree.sbr +.\Debug\mapperTruth.sbr +.\Debug\mapperUtils.sbr +.\Debug\mapperVec.sbr +.\Debug\mio.sbr +.\Debug\mioApi.sbr +.\Debug\mioFunc.sbr +.\Debug\mioRead.sbr +.\Debug\mioUtils.sbr +.\Debug\super.sbr +.\Debug\superAnd.sbr +.\Debug\superGate.sbr +.\Debug\superWrite.sbr +.\Debug\extraBddMisc.sbr +.\Debug\extraBddSymm.sbr +.\Debug\extraUtilBitMatrix.sbr +.\Debug\extraUtilCanon.sbr +.\Debug\extraUtilFile.sbr +.\Debug\extraUtilMemory.sbr +.\Debug\extraUtilMisc.sbr +.\Debug\extraUtilProgress.sbr +.\Debug\extraUtilReader.sbr +.\Debug\st.sbr +.\Debug\stmm.sbr +.\Debug\cpu_stats.sbr +.\Debug\cpu_time.sbr +.\Debug\datalimit.sbr +.\Debug\getopt.sbr +.\Debug\pathsearch.sbr +.\Debug\safe_mem.sbr +.\Debug\strsav.sbr +.\Debug\texpand.sbr +.\Debug\ioWriteGml.sbr +.\Debug\ioWriteEqn.sbr +.\Debug\ioWriteDot.sbr +.\Debug\ioReadEqn.sbr] +Creating command line "bscmake.exe @C:\DOCUME~1\alanmi\LOCALS~1\Temp\RSP3591.tmp" +Creating browse info file... +

Output Window

diff --git a/abc.rc b/abc.rc index cf648fcb..6dd07dd1 100644 --- a/abc.rc +++ b/abc.rc @@ -11,6 +11,7 @@ alias pl print_level alias pio print_io alias ps print_stats alias psu print_supp +alias psy print_symm alias q quit alias r read alias rl read_blif @@ -32,7 +33,7 @@ alias wl write_blif alias wp write_pla alias cnf "st; renode -c; write_cnf" alias prove "st; renode -c; sat" -alias opt "b; renode; b; ps" -alias share "b; renode -m; fx; b; ps" -alias resyn "b; rw; rf; b; rwz; rfz; b; ps" +alias opt "b; renode; b" +alias share "b; renode -m; fx; b" +alias resyn "b; rw; rf; b; rw; rwz; b; rfz; rwz; b" diff --git a/src/base/abc/abc.c b/src/base/abc/abc.c index 7c949ee0..0d911e79 100644 --- a/src/base/abc/abc.c +++ b/src/base/abc/abc.c @@ -36,8 +36,11 @@ static int Abc_CommandPrintFanio ( Abc_Frame_t * pAbc, int argc, char ** argv static int Abc_CommandPrintFactor ( Abc_Frame_t * pAbc, int argc, char ** argv ); static int Abc_CommandPrintLevel ( Abc_Frame_t * pAbc, int argc, char ** argv ); static int Abc_CommandPrintSupport ( Abc_Frame_t * pAbc, int argc, char ** argv ); +static int Abc_CommandPrintSymms ( Abc_Frame_t * pAbc, int argc, char ** argv ); static int Abc_CommandShowBdd ( Abc_Frame_t * pAbc, int argc, char ** argv ); +static int Abc_CommandShowCut ( Abc_Frame_t * pAbc, int argc, char ** argv ); +static int Abc_CommandShowAig ( Abc_Frame_t * pAbc, int argc, char ** argv ); static int Abc_CommandCollapse ( Abc_Frame_t * pAbc, int argc, char ** argv ); static int Abc_CommandStrash ( Abc_Frame_t * pAbc, int argc, char ** argv ); @@ -105,8 +108,11 @@ void Abc_Init( Abc_Frame_t * pAbc ) Cmd_CommandAdd( pAbc, "Printing", "print_factor", Abc_CommandPrintFactor, 0 ); Cmd_CommandAdd( pAbc, "Printing", "print_level", Abc_CommandPrintLevel, 0 ); Cmd_CommandAdd( pAbc, "Printing", "print_supp", Abc_CommandPrintSupport, 0 ); + Cmd_CommandAdd( pAbc, "Printing", "print_symm", Abc_CommandPrintSymms, 0 ); Cmd_CommandAdd( pAbc, "Printing", "show_bdd", Abc_CommandShowBdd, 0 ); + Cmd_CommandAdd( pAbc, "Printing", "show_cut", Abc_CommandShowCut, 0 ); + Cmd_CommandAdd( pAbc, "Printing", "show_aig", Abc_CommandShowAig, 0 ); Cmd_CommandAdd( pAbc, "Synthesis", "collapse", Abc_CommandCollapse, 1 ); Cmd_CommandAdd( pAbc, "Synthesis", "strash", Abc_CommandStrash, 1 ); @@ -297,9 +303,10 @@ int Abc_CommandPrintIo( Abc_Frame_t * pAbc, int argc, char ** argv ) return 0; usage: - fprintf( pErr, "usage: print_io [-h]\n" ); + fprintf( pErr, "usage: print_io [-h] \n" ); fprintf( pErr, "\t prints the PIs/POs or fanins/fanouts of a node\n" ); fprintf( pErr, "\t-h : print the command usage\n"); + fprintf( pErr, "\tnode : the node to print fanins/fanouts\n"); return 1; } @@ -618,6 +625,78 @@ usage: return 1; } +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Abc_CommandPrintSymms( Abc_Frame_t * pAbc, int argc, char ** argv ) +{ + FILE * pOut, * pErr; + Abc_Ntk_t * pNtk; + int c; + int fUseBdds; + int fNaive; + int fVerbose; + extern void Abc_NtkSymmetries( Abc_Ntk_t * pNtk, int fUseBdds, int fNaive, int fVerbose ); + + pNtk = Abc_FrameReadNet(pAbc); + pOut = Abc_FrameReadOut(pAbc); + pErr = Abc_FrameReadErr(pAbc); + + // set defaults + fUseBdds = 1; + fNaive = 0; + fVerbose = 0; + util_getopt_reset(); + while ( ( c = util_getopt( argc, argv, "bnvh" ) ) != EOF ) + { + switch ( c ) + { + case 'b': + fUseBdds ^= 1; + break; + case 'n': + fNaive ^= 1; + break; + case 'v': + fVerbose ^= 1; + break; + case 'h': + goto usage; + default: + goto usage; + } + } + if ( pNtk == NULL ) + { + fprintf( pErr, "Empty network.\n" ); + return 1; + } + if ( !Abc_NtkIsStrash(pNtk) ) + { + fprintf( pErr, "This command works only for AIGs.\n" ); + return 1; + } + Abc_NtkSymmetries( pNtk, fUseBdds, fNaive, fVerbose ); + return 0; + +usage: + fprintf( pErr, "usage: print_symm [-nbvh]\n" ); + fprintf( pErr, "\t computes symmetries of the PO functions\n" ); + fprintf( pErr, "\t-b : enable efficient BDD-based computation [default = %s].\n", fUseBdds? "yes": "no" ); + fprintf( pErr, "\t-n : enable naive BDD-based computation [default = %s].\n", fNaive? "yes": "no" ); + fprintf( pErr, "\t-v : enable verbose output [default = %s].\n", fVerbose? "yes": "no" ); + fprintf( pErr, "\t-h : print the command usage\n"); + return 1; +} + /**Function************************************************************* Synopsis [] @@ -635,7 +714,7 @@ int Abc_CommandShowBdd( Abc_Frame_t * pAbc, int argc, char ** argv ) Abc_Ntk_t * pNtk; Abc_Obj_t * pNode; int c; - extern void Abc_NodePrintBdd( Abc_Obj_t * pNode ); + extern void Abc_NodeShowBdd( Abc_Obj_t * pNode ); pNtk = Abc_FrameReadNet(pAbc); pOut = Abc_FrameReadOut(pAbc); @@ -662,7 +741,7 @@ int Abc_CommandShowBdd( Abc_Frame_t * pAbc, int argc, char ** argv ) if ( !Abc_NtkIsBddLogic(pNtk) ) { - fprintf( pErr, "Printing BDDs can only be done for logic BDD networks.\n" ); + fprintf( pErr, "Visualizing BDDs can only be done for logic BDD networks.\n" ); return 1; } @@ -678,7 +757,7 @@ int Abc_CommandShowBdd( Abc_Frame_t * pAbc, int argc, char ** argv ) fprintf( pErr, "Cannot find node \"%s\".\n", argv[util_optind] ); return 1; } - Abc_NodePrintBdd( pNode ); + Abc_NodeShowBdd( pNode ); return 0; usage: @@ -693,6 +772,168 @@ usage: return 1; } +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Abc_CommandShowCut( Abc_Frame_t * pAbc, int argc, char ** argv ) +{ + FILE * pOut, * pErr; + Abc_Ntk_t * pNtk; + Abc_Obj_t * pNode; + int c; + int nNodeSizeMax; + int nConeSizeMax; + extern void Abc_NodeShowCut( Abc_Obj_t * pNode, int nNodeSizeMax, int nConeSizeMax ); + + pNtk = Abc_FrameReadNet(pAbc); + pOut = Abc_FrameReadOut(pAbc); + pErr = Abc_FrameReadErr(pAbc); + + // set defaults + nNodeSizeMax = 10; + nConeSizeMax = ABC_INFINITY; + util_getopt_reset(); + while ( ( c = util_getopt( argc, argv, "NCh" ) ) != EOF ) + { + switch ( c ) + { + case 'N': + if ( util_optind >= argc ) + { + fprintf( pErr, "Command line switch \"-N\" should be followed by an integer.\n" ); + goto usage; + } + nNodeSizeMax = atoi(argv[util_optind]); + util_optind++; + if ( nNodeSizeMax < 0 ) + goto usage; + break; + case 'C': + if ( util_optind >= argc ) + { + fprintf( pErr, "Command line switch \"-C\" should be followed by an integer.\n" ); + goto usage; + } + nConeSizeMax = atoi(argv[util_optind]); + util_optind++; + if ( nConeSizeMax < 0 ) + goto usage; + break; + case 'h': + goto usage; + default: + goto usage; + } + } + + if ( pNtk == NULL ) + { + fprintf( pErr, "Empty network.\n" ); + return 1; + } + + if ( !Abc_NtkIsStrash(pNtk) ) + { + fprintf( pErr, "Visualizing cuts only works for AIGs.\n" ); + return 1; + } + if ( argc != util_optind + 1 ) + { + fprintf( pErr, "Wrong number of auguments.\n" ); + goto usage; + } + + pNode = Abc_NtkFindNode( pNtk, argv[util_optind] ); + if ( pNode == NULL ) + { + fprintf( pErr, "Cannot find node \"%s\".\n", argv[util_optind] ); + return 1; + } + Abc_NodeShowCut( pNode, nNodeSizeMax, nConeSizeMax ); + return 0; + +usage: + fprintf( pErr, "usage: show_cut [-N num] [-C num] [-h] \n" ); + fprintf( pErr, " visualizes the cut of a node using DOT and GSVIEW\n" ); +#ifdef WIN32 + fprintf( pErr, " \"dot.exe\" and \"gsview32.exe\" should be set in the paths\n" ); + fprintf( pErr, " (\"gsview32.exe\" may be in \"C:\\Program Files\\Ghostgum\\gsview\\\")\n" ); +#endif + fprintf( pErr, "\t-N num : the max size of the cut to be computed [default = %d]\n", nNodeSizeMax ); + fprintf( pErr, "\t-C num : the max support of the containing cone [default = %d]\n", nConeSizeMax ); + fprintf( pErr, "\tnode : the node to consider\n"); + fprintf( pErr, "\t-h : print the command usage\n"); + return 1; +} + +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Abc_CommandShowAig( Abc_Frame_t * pAbc, int argc, char ** argv ) +{ + FILE * pOut, * pErr; + Abc_Ntk_t * pNtk; + int c; + extern void Abc_NtkShowAig( Abc_Ntk_t * pNtk ); + + pNtk = Abc_FrameReadNet(pAbc); + pOut = Abc_FrameReadOut(pAbc); + pErr = Abc_FrameReadErr(pAbc); + + // set defaults + util_getopt_reset(); + while ( ( c = util_getopt( argc, argv, "h" ) ) != EOF ) + { + switch ( c ) + { + case 'h': + goto usage; + default: + goto usage; + } + } + + if ( pNtk == NULL ) + { + fprintf( pErr, "Empty network.\n" ); + return 1; + } + + if ( !Abc_NtkIsStrash(pNtk) ) + { + fprintf( pErr, "Visualizing AIG can only be done for AIGs.\n" ); + return 1; + } + Abc_NtkShowAig( pNtk ); + return 0; + +usage: + fprintf( pErr, "usage: show_aig [-h]\n" ); + fprintf( pErr, " visualizes the AIG with choices using DOT and GSVIEW\n" ); +#ifdef WIN32 + fprintf( pErr, " \"dot.exe\" and \"gsview32.exe\" should be set in the paths\n" ); + fprintf( pErr, " (\"gsview32.exe\" may be in \"C:\\Program Files\\Ghostgum\\gsview\\\")\n" ); +#endif + fprintf( pErr, "\t-h : print the command usage\n"); + return 1; +} + /**Function************************************************************* @@ -745,7 +986,7 @@ int Abc_CommandCollapse( Abc_Frame_t * pAbc, int argc, char ** argv ) pNtkRes = Abc_NtkCollapse( pNtk, 1 ); else { - pNtk = Abc_NtkStrash( pNtk, 0 ); + pNtk = Abc_NtkStrash( pNtk, 0, 0 ); pNtkRes = Abc_NtkCollapse( pNtk, 1 ); Abc_NtkDelete( pNtk ); } @@ -783,6 +1024,7 @@ int Abc_CommandStrash( Abc_Frame_t * pAbc, int argc, char ** argv ) Abc_Ntk_t * pNtk, * pNtkRes; int c; int fAllNodes; + int fCleanup; pNtk = Abc_FrameReadNet(pAbc); pOut = Abc_FrameReadOut(pAbc); @@ -790,14 +1032,18 @@ int Abc_CommandStrash( Abc_Frame_t * pAbc, int argc, char ** argv ) // set defaults fAllNodes = 0; + fCleanup = 1; util_getopt_reset(); - while ( ( c = util_getopt( argc, argv, "ah" ) ) != EOF ) + while ( ( c = util_getopt( argc, argv, "ach" ) ) != EOF ) { switch ( c ) { case 'a': fAllNodes ^= 1; break; + case 'c': + fCleanup ^= 1; + break; case 'h': goto usage; default: @@ -812,7 +1058,7 @@ int Abc_CommandStrash( Abc_Frame_t * pAbc, int argc, char ** argv ) } // get the new network - pNtkRes = Abc_NtkStrash( pNtk, fAllNodes ); + pNtkRes = Abc_NtkStrash( pNtk, fAllNodes, fCleanup ); if ( pNtkRes == NULL ) { fprintf( pErr, "Strashing has failed.\n" ); @@ -823,9 +1069,10 @@ int Abc_CommandStrash( Abc_Frame_t * pAbc, int argc, char ** argv ) return 0; usage: - fprintf( pErr, "usage: strash [-ah]\n" ); + fprintf( pErr, "usage: strash [-ach]\n" ); fprintf( pErr, "\t transforms combinational logic into an AIG\n" ); fprintf( pErr, "\t-a : toggles between using all nodes and DFS nodes [default = %s]\n", fAllNodes? "all": "DFS" ); + fprintf( pErr, "\t-c : toggles cleanup to remove the dagling AIG nodes [default = %s]\n", fCleanup? "all": "DFS" ); fprintf( pErr, "\t-h : print the command usage\n"); return 1; } @@ -882,7 +1129,7 @@ int Abc_CommandBalance( Abc_Frame_t * pAbc, int argc, char ** argv ) } else { - pNtkTemp = Abc_NtkStrash( pNtk, 0 ); + pNtkTemp = Abc_NtkStrash( pNtk, 0, 0 ); if ( pNtkTemp == NULL ) { fprintf( pErr, "Strashing before balancing has failed.\n" ); @@ -1274,7 +1521,7 @@ int Abc_CommandDisjoint( Abc_Frame_t * pAbc, int argc, char ** argv ) // get the new network if ( !Abc_NtkIsStrash(pNtk) ) { - pNtkNew = Abc_NtkStrash( pNtk, 0 ); + pNtkNew = Abc_NtkStrash( pNtk, 0, 0 ); pNtkRes = Abc_NtkDsdGlobal( pNtkNew, fVerbose, fPrint, fShort ); Abc_NtkDelete( pNtkNew ); } @@ -1732,7 +1979,7 @@ int Abc_CommandFrames( Abc_Frame_t * pAbc, int argc, char ** argv ) // get the new network if ( !Abc_NtkIsStrash(pNtk) ) { - pNtkTemp = Abc_NtkStrash( pNtk, 0 ); + pNtkTemp = Abc_NtkStrash( pNtk, 0, 0 ); pNtkRes = Abc_NtkFrames( pNtkTemp, nFrames, fInitial ); Abc_NtkDelete( pNtkTemp ); } @@ -2424,7 +2671,7 @@ int Abc_CommandFraig( Abc_Frame_t * pAbc, int argc, char ** argv ) pNtkRes = Abc_NtkFraig( pNtk, &Params, fAllNodes ); else { - pNtk = Abc_NtkStrash( pNtk, 0 ); + pNtk = Abc_NtkStrash( pNtk, fAllNodes, !fAllNodes ); pNtkRes = Abc_NtkFraig( pNtk, &Params, fAllNodes ); Abc_NtkDelete( pNtk ); } @@ -2845,7 +3092,7 @@ int Abc_CommandMap( Abc_Frame_t * pAbc, int argc, char ** argv ) if ( !Abc_NtkIsStrash(pNtk) ) { - pNtk = Abc_NtkStrash( pNtk, 0 ); + pNtk = Abc_NtkStrash( pNtk, 0, 0 ); if ( pNtk == NULL ) { fprintf( pErr, "Strashing before mapping has failed.\n" ); @@ -3087,8 +3334,10 @@ int Abc_CommandSuperChoice( Abc_Frame_t * pAbc, int argc, char ** argv ) usage: fprintf( pErr, "usage: sc [-h]\n" ); - fprintf( pErr, "\t performs superchoicing\n" ); - fprintf( pErr, "\t-h : print the command usage\n"); + fprintf( pErr, "\t performs superchoicing\n" ); + fprintf( pErr, "\t (accumulate: \"r file.blif; rsup; b; sc; f -ac; wb file_sc.blif\")\n" ); + fprintf( pErr, "\t (map without supergate library: \"r file_sc.blif; ft; map\")\n" ); + fprintf( pErr, "\t-h : print the command usage\n"); return 1; } @@ -3146,7 +3395,7 @@ int Abc_CommandFpga( Abc_Frame_t * pAbc, int argc, char ** argv ) if ( !Abc_NtkIsStrash(pNtk) ) { // strash and balance the network - pNtk = Abc_NtkStrash( pNtk, 0 ); + pNtk = Abc_NtkStrash( pNtk, 0, 0 ); if ( pNtk == NULL ) { fprintf( pErr, "Strashing before FPGA mapping has failed.\n" ); diff --git a/src/base/abc/abc.h b/src/base/abc/abc.h index a3f7ddb7..ab457cc9 100644 --- a/src/base/abc/abc.h +++ b/src/base/abc/abc.h @@ -51,7 +51,7 @@ typedef enum { ABC_TYPE_OTHER // 5: unused } Abc_NtkType_t; -// functionality types +// network functionality typedef enum { ABC_FUNC_NONE, // 0: unknown ABC_FUNC_SOP, // 1: sum-of-products @@ -155,13 +155,16 @@ struct Abc_Ntk_t_ int nPos; // the number of primary outputs // the functionality manager void * pManFunc; // AIG manager, BDD manager, or memory manager for SOPs + // the global functions (BDDs) + void * pManGlob; // the BDD manager + Vec_Ptr_t * vFuncsGlob; // the BDDs of CO functions // the timing manager (for mapped networks) Abc_ManTime_t * pManTime; // stores arrival/required times for all nodes // the cut manager (for AIGs) void * pManCut; // stores information about the cuts computed for the nodes // level information (for AIGs) int LevelMax; // maximum number of levels - Vec_Int_t * vLevelsR; // level in the reverse topological order + Vec_Int_t * vLevelsR; // level in the reverse topological order // the external don't-care if given Abc_Ntk_t * pExdc; // the EXDC network // miscellaneous data members @@ -401,8 +404,11 @@ extern void Abc_AigDeleteNode( Abc_Aig_t * pMan, Abc_Obj_t * pOld extern bool Abc_AigNodeHasComplFanoutEdge( Abc_Obj_t * pNode ); extern bool Abc_AigNodeHasComplFanoutEdgeTrav( Abc_Obj_t * pNode ); extern void Abc_AigPrintNode( Abc_Obj_t * pNode ); +extern bool Abc_AigNodeIsAcyclic( Abc_Obj_t * pNode, Abc_Obj_t * pRoot ); /*=== abcAttach.c ==========================================================*/ extern int Abc_NtkAttach( Abc_Ntk_t * pNtk ); +/*=== abcBalance.c ==========================================================*/ +extern Abc_Ntk_t * Abc_NtkBalance( Abc_Ntk_t * pNtk, bool fDuplicate ); /*=== abcCheck.c ==========================================================*/ extern bool Abc_NtkCheck( Abc_Ntk_t * pNtk ); extern bool Abc_NtkCheckObj( Abc_Ntk_t * pNtk, Abc_Obj_t * pObj ); @@ -410,7 +416,7 @@ extern bool Abc_NtkCompareSignals( Abc_Ntk_t * pNtk1, Abc_Ntk_t * /*=== abcCollapse.c ==========================================================*/ extern Abc_Ntk_t * Abc_NtkCollapse( Abc_Ntk_t * pNtk, int fVerbose ); extern DdManager * Abc_NtkGlobalBdds( Abc_Ntk_t * pNtk, int fLatchOnly ); -extern void Abc_NtkFreeGlobalBdds( DdManager * dd, Abc_Ntk_t * pNtk ); +extern void Abc_NtkFreeGlobalBdds( Abc_Ntk_t * pNtk ); /*=== abcCreate.c ==========================================================*/ extern Abc_Ntk_t * Abc_NtkAlloc( Abc_NtkType_t Type, Abc_NtkFunc_t Func ); extern Abc_Ntk_t * Abc_NtkStartFrom( Abc_Ntk_t * pNtk, Abc_NtkType_t Type, Abc_NtkFunc_t Func ); @@ -475,6 +481,7 @@ extern char * Abc_ConvertBddToSop( Extra_MmFlex_t * pMan, DdManager extern int Abc_NtkBddToSop( Abc_Ntk_t * pNtk ); extern void Abc_NodeBddToCnf( Abc_Obj_t * pNode, Extra_MmFlex_t * pMmMan, Vec_Str_t * vCube, char ** ppSop0, char ** ppSop1 ); extern int Abc_CountZddCubes( DdManager * dd, DdNode * zCover ); +extern void Abc_NtkLogicMakeDirectSops( Abc_Ntk_t * pNtk ); /*=== abcLatch.c ==========================================================*/ extern bool Abc_NtkLatchIsSelfFeed( Abc_Obj_t * pLatch ); extern int Abc_NtkCountSelfFeedLatches( Abc_Ntk_t * pNtk ); @@ -519,13 +526,15 @@ extern void Abc_NodePrintFactor( FILE * pFile, Abc_Obj_t * pNode ) extern void Abc_NtkPrintLevel( FILE * pFile, Abc_Ntk_t * pNtk, int fProfile ); extern void Abc_NodePrintLevel( FILE * pFile, Abc_Obj_t * pNode ); /*=== abcReconv.c ==========================================================*/ -extern Abc_ManCut_t * Abc_NtkManCutStart( int nNodeSizeMax, int nConeSizeMax ); +extern Abc_ManCut_t * Abc_NtkManCutStart( int nNodeSizeMax, int nConeSizeMax, int nNodeFanStop, int nConeFanStop ); extern void Abc_NtkManCutStop( Abc_ManCut_t * p ); -extern Vec_Ptr_t * Abc_NtkManCutReadLeaves( Abc_ManCut_t * p ); +extern Vec_Ptr_t * Abc_NtkManCutReadCutLarge( Abc_ManCut_t * p ); +extern Vec_Ptr_t * Abc_NtkManCutReadVisited( Abc_ManCut_t * p ); extern Vec_Ptr_t * Abc_NodeFindCut( Abc_ManCut_t * p, Abc_Obj_t * pRoot, bool fContain ); +extern void Abc_NodeConeCollect( Abc_Obj_t ** ppRoots, int nRoots, Vec_Ptr_t * vFanins, Vec_Ptr_t * vVisited, int fIncludeFanins ); extern DdNode * Abc_NodeConeBdd( DdManager * dd, DdNode ** pbVars, Abc_Obj_t * pNode, Vec_Ptr_t * vFanins, Vec_Ptr_t * vVisited ); extern DdNode * Abc_NodeConeDcs( DdManager * dd, DdNode ** pbVarsX, DdNode ** pbVarsY, Vec_Ptr_t * vLeaves, Vec_Ptr_t * vRoots, Vec_Ptr_t * vVisited ); -extern void Abc_NodeCollectTfoCands( Abc_Ntk_t * pNtk, Abc_Obj_t * pRoot, Vec_Ptr_t * vFanins, int LevelMax, Vec_Vec_t * vLevels, Vec_Ptr_t * vResult ); +extern Vec_Ptr_t * Abc_NodeCollectTfoCands( Abc_ManCut_t * p, Abc_Obj_t * pRoot, Vec_Ptr_t * vFanins, int LevelMax ); /*=== abcRefs.c ==========================================================*/ extern int Abc_NodeMffcSize( Abc_Obj_t * pNode ); extern int Abc_NodeMffcLabel( Abc_Obj_t * pNode ); @@ -576,12 +585,11 @@ extern bool Abc_SopCheck( char * pSop, int nFanins ); extern void Abc_SopWriteCnf( FILE * pFile, char * pClauses, Vec_Int_t * vVars ); extern void Abc_SopAddCnfToSolver( solver * pSat, char * pClauses, Vec_Int_t * vVars, Vec_Int_t * vTemp ); /*=== abcStrash.c ==========================================================*/ -extern Abc_Ntk_t * Abc_NtkStrash( Abc_Ntk_t * pNtk, bool fAllNodes ); +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 ); -extern Abc_Ntk_t * Abc_NtkBalance( Abc_Ntk_t * pNtk, bool fDuplicate ); /*=== abcSweep.c ==========================================================*/ extern bool Abc_NtkFraigSweep( Abc_Ntk_t * pNtk, int fUseInv, int fVerbose ); extern int Abc_NtkCleanup( Abc_Ntk_t * pNtk, int fVerbose ); @@ -643,6 +651,7 @@ extern char ** Abc_NtkCollectCioNames( Abc_Ntk_t * pNtk, int fCollect 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 ); //////////////////////////////////////////////////////////////////////// /// END OF FILE /// diff --git a/src/base/abc/abcAig.c b/src/base/abc/abcAig.c index f71c0a15..9588f1e0 100644 --- a/src/base/abc/abcAig.c +++ b/src/base/abc/abcAig.c @@ -705,8 +705,10 @@ void Abc_AigReplace_int( Abc_Aig_t * pMan ) assert( iFanin == 0 || iFanin == 1 ); // get the new fanin pFanin1 = Abc_ObjNotCond( pNew, Abc_ObjFaninC(pFanout, iFanin) ); + assert( Abc_ObjRegular(pFanin1) != pFanout ); // get another fanin pFanin2 = Abc_ObjChild( pFanout, iFanin ^ 1 ); + assert( Abc_ObjRegular(pFanin2) != pFanout ); // check if the node with these fanins exists if ( pFanoutNew = Abc_AigAndLookup( pMan, pFanin1, pFanin2 ) ) { // such node exists (it may be a constant) @@ -732,6 +734,7 @@ void Abc_AigReplace_int( Abc_Aig_t * pMan ) Abc_ObjRemoveFanins( pFanout ); // recreate the old fanout with new fanins and add it to the table Abc_AigAndCreateFrom( pMan, pFanin1, pFanin2, pFanout ); + assert( Abc_AigNodeIsAcyclic(pFanout, pFanout) ); // schedule the updated fanout for updating direct level assert( pFanout->fMarkA == 0 ); @@ -876,6 +879,7 @@ void Abc_AigUpdateLevel_int( Abc_Aig_t * pMan ) if ( pNode == NULL ) continue; assert( Abc_ObjIsNode(pNode) ); + assert( (int)pNode->Level == i ); // clean the mark assert( pNode->fMarkA == 1 ); pNode->fMarkA = 0; @@ -931,6 +935,7 @@ void Abc_AigUpdateLevelR_int( Abc_Aig_t * pMan ) if ( pNode == NULL ) continue; assert( Abc_ObjIsNode(pNode) ); + assert( Abc_NodeReadReverseLevel(pNode) == i ); // clean the mark assert( pNode->fMarkB == 1 ); pNode->fMarkB = 0; @@ -1113,6 +1118,56 @@ void Abc_AigPrintNode( Abc_Obj_t * pNode ) printf( "\n" ); } + +/**Function************************************************************* + + Synopsis [Check if the node has a combination loop of depth 1 or 2.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +bool Abc_AigNodeIsAcyclic( Abc_Obj_t * pNode, Abc_Obj_t * pRoot ) +{ + Abc_Obj_t * pFanin0, * pFanin1; + Abc_Obj_t * pChild00, * pChild01; + Abc_Obj_t * pChild10, * pChild11; + if ( !Abc_NodeIsAigAnd(pNode) ) + return 1; + pFanin0 = Abc_ObjFanin0(pNode); + pFanin1 = Abc_ObjFanin1(pNode); + if ( pRoot == pFanin0 || pRoot == pFanin1 ) + return 0; + if ( Abc_ObjIsCi(pFanin0) ) + { + pChild00 = NULL; + pChild01 = NULL; + } + else + { + pChild00 = Abc_ObjFanin0(pFanin0); + pChild01 = Abc_ObjFanin1(pFanin0); + if ( pRoot == pChild00 || pRoot == pChild01 ) + return 0; + } + if ( Abc_ObjIsCi(pFanin1) ) + { + pChild10 = NULL; + pChild11 = NULL; + } + else + { + pChild10 = Abc_ObjFanin0(pFanin1); + pChild11 = Abc_ObjFanin1(pFanin1); + if ( pRoot == pChild10 || pRoot == pChild11 ) + return 0; + } + return 1; +} + //////////////////////////////////////////////////////////////////////// /// END OF FILE /// //////////////////////////////////////////////////////////////////////// diff --git a/src/base/abc/abcCollapse.c b/src/base/abc/abcCollapse.c index e07636cc..a6eda7b3 100644 --- a/src/base/abc/abcCollapse.c +++ b/src/base/abc/abcCollapse.c @@ -25,7 +25,7 @@ //////////////////////////////////////////////////////////////////////// static DdNode * Abc_NtkGlobalBdds_rec( DdManager * dd, Abc_Obj_t * pNode ); -static Abc_Ntk_t * Abc_NtkFromGlobalBdds( DdManager * dd, Abc_Ntk_t * pNtk ); +static Abc_Ntk_t * Abc_NtkFromGlobalBdds( Abc_Ntk_t * pNtk ); static Abc_Obj_t * Abc_NodeFromGlobalBdds( Abc_Ntk_t * pNtkNew, DdManager * dd, DdNode * bFunc ); //////////////////////////////////////////////////////////////////////// @@ -47,26 +47,26 @@ Abc_Ntk_t * Abc_NtkCollapse( Abc_Ntk_t * pNtk, int fVerbose ) { int fCheck = 1; Abc_Ntk_t * pNtkNew; - DdManager * dd; assert( Abc_NtkIsStrash(pNtk) ); // compute the global BDDs - dd = Abc_NtkGlobalBdds( pNtk, 0 ); - if ( dd == NULL ) + if ( Abc_NtkGlobalBdds(pNtk, 0) == NULL ) return NULL; if ( fVerbose ) - printf( "The shared BDD size is %d nodes.\n", Cudd_ReadKeys(dd) - Cudd_ReadDead(dd) ); + printf( "The shared BDD size is %d nodes.\n", Cudd_ReadKeys(pNtk->pManGlob) - Cudd_ReadDead(pNtk->pManGlob) ); // create the new network - pNtkNew = Abc_NtkFromGlobalBdds( dd, pNtk ); - Abc_NtkFreeGlobalBdds( dd, pNtk ); + pNtkNew = Abc_NtkFromGlobalBdds( pNtk ); + Abc_NtkFreeGlobalBdds( pNtk ); if ( pNtkNew == NULL ) { - Cudd_Quit( dd ); + Cudd_Quit( pNtk->pManGlob ); + pNtk->pManGlob = NULL; return NULL; } - Extra_StopManager( dd ); + Extra_StopManager( pNtk->pManGlob ); + pNtk->pManGlob = NULL; // make the network minimum base Abc_NtkMinimumBase( pNtkNew ); @@ -96,12 +96,14 @@ DdManager * Abc_NtkGlobalBdds( Abc_Ntk_t * pNtk, int fLatchOnly ) { int fReorder = 1; ProgressBar * pProgress; + Vec_Ptr_t * vFuncsGlob; Abc_Obj_t * pNode; DdNode * bFunc; DdManager * dd; int i; // start the manager + assert( pNtk->pManGlob == NULL ); dd = Cudd_Init( Abc_NtkCiNum(pNtk), 0, CUDD_UNIQUE_SLOTS, CUDD_CACHE_SLOTS, 0 ); if ( fReorder ) Cudd_AutodynEnable( dd, CUDD_REORDER_SYMM_SIFT ); @@ -114,6 +116,7 @@ DdManager * Abc_NtkGlobalBdds( Abc_Ntk_t * pNtk, int fLatchOnly ) pNode = Abc_AigConst1( pNtk->pManFunc ); pNode->pCopy = (Abc_Obj_t *)dd->one; Cudd_Ref( dd->one ); + vFuncsGlob = Vec_PtrAlloc( 100 ); if ( fLatchOnly ) { // construct the BDDs @@ -129,8 +132,8 @@ DdManager * Abc_NtkGlobalBdds( Abc_Ntk_t * pNtk, int fLatchOnly ) Cudd_Quit( dd ); return NULL; } - bFunc = Cudd_NotCond( bFunc, Abc_ObjFaninC0(pNode) ); - pNode->pNext = (Abc_Obj_t *)bFunc; Cudd_Ref( bFunc ); + bFunc = Cudd_NotCond( bFunc, Abc_ObjFaninC0(pNode) ); Cudd_Ref( bFunc ); + Vec_PtrPush( vFuncsGlob, bFunc ); } Extra_ProgressBarStop( pProgress ); } @@ -149,8 +152,8 @@ DdManager * Abc_NtkGlobalBdds( Abc_Ntk_t * pNtk, int fLatchOnly ) Cudd_Quit( dd ); return NULL; } - bFunc = Cudd_NotCond( bFunc, Abc_ObjFaninC0(pNode) ); - pNode->pNext = (Abc_Obj_t *)bFunc; Cudd_Ref( bFunc ); + bFunc = Cudd_NotCond( bFunc, Abc_ObjFaninC0(pNode) ); Cudd_Ref( bFunc ); + Vec_PtrPush( vFuncsGlob, bFunc ); } Extra_ProgressBarStop( pProgress ); } @@ -168,6 +171,8 @@ DdManager * Abc_NtkGlobalBdds( Abc_Ntk_t * pNtk, int fLatchOnly ) Cudd_ReduceHeap( dd, CUDD_REORDER_SYMM_SIFT, 1 ); Cudd_AutodynDisable( dd ); } + pNtk->pManGlob = dd; + pNtk->vFuncsGlob = vFuncsGlob; return dd; } @@ -223,11 +228,12 @@ DdNode * Abc_NtkGlobalBdds_rec( DdManager * dd, Abc_Obj_t * pNode ) SeeAlso [] ***********************************************************************/ -Abc_Ntk_t * Abc_NtkFromGlobalBdds( DdManager * dd, Abc_Ntk_t * pNtk ) +Abc_Ntk_t * Abc_NtkFromGlobalBdds( Abc_Ntk_t * pNtk ) { ProgressBar * pProgress; Abc_Ntk_t * pNtkNew; Abc_Obj_t * pNode, * pNodeNew; + DdManager * dd = pNtk->pManGlob; int i; // start the new network pNtkNew = Abc_NtkStartFrom( pNtk, ABC_TYPE_LOGIC, ABC_FUNC_BDD ); @@ -238,7 +244,7 @@ Abc_Ntk_t * Abc_NtkFromGlobalBdds( DdManager * dd, Abc_Ntk_t * pNtk ) Abc_NtkForEachCo( pNtk, pNode, i ) { Extra_ProgressBarUpdate( pProgress, i, NULL ); - pNodeNew = Abc_NodeFromGlobalBdds( pNtkNew, dd, (DdNode *)pNode->pNext ); + pNodeNew = Abc_NodeFromGlobalBdds( pNtkNew, dd, Vec_PtrEntry(pNtk->vFuncsGlob, i) ); Abc_ObjAddFanin( pNode->pCopy, pNodeNew ); } Extra_ProgressBarStop( pProgress ); @@ -281,17 +287,16 @@ Abc_Obj_t * Abc_NodeFromGlobalBdds( Abc_Ntk_t * pNtkNew, DdManager * dd, DdNode SeeAlso [] ***********************************************************************/ -void Abc_NtkFreeGlobalBdds( DdManager * dd, Abc_Ntk_t * pNtk ) +void Abc_NtkFreeGlobalBdds( Abc_Ntk_t * pNtk ) { - Abc_Obj_t * pNode; + DdNode * bFunc; int i; - Abc_NtkForEachCo( pNtk, pNode, i ) - { - if ( pNode->pNext == NULL ) - continue; - Cudd_RecursiveDeref( dd, (DdNode *)pNode->pNext ); - pNode->pNext = NULL; - } + assert( pNtk->pManGlob ); + assert( pNtk->vFuncsGlob ); + Vec_PtrForEachEntry( pNtk->vFuncsGlob, bFunc, i ) + Cudd_RecursiveDeref( pNtk->pManGlob, bFunc ); + Vec_PtrFree( pNtk->vFuncsGlob ); + pNtk->vFuncsGlob = NULL; } diff --git a/src/base/abc/abcCreate.c b/src/base/abc/abcCreate.c index 9186ec5a..d6500803 100644 --- a/src/base/abc/abcCreate.c +++ b/src/base/abc/abcCreate.c @@ -818,7 +818,7 @@ Abc_Obj_t * Abc_NtkFindNode( Abc_Ntk_t * pNtk, char * pName ) // find the internal node if ( pName[0] != '[' || pName[strlen(pName)-1] != ']' ) { - printf( "Node \"%s\" has non-standard name (expected name is \"[integer]\").\n", pName ); + printf( "Name \"%s\" is not found among CIs/COs (internal name looks like this: \"[integer]\").\n", pName ); return NULL; } Num = atoi( pName + 1 ); diff --git a/src/base/abc/abcDsd.c b/src/base/abc/abcDsd.c index d1445e75..ccb52ffa 100644 --- a/src/base/abc/abcDsd.c +++ b/src/base/abc/abcDsd.c @@ -25,8 +25,7 @@ /// DECLARATIONS /// //////////////////////////////////////////////////////////////////////// -static Abc_Ntk_t * Abc_NtkDsdInternal( DdManager * dd, Abc_Ntk_t * pNtk, bool fVerbose, bool fPrint, bool fShort ); -static Dsd_Manager_t * Abc_NtkDsdPerform( DdManager * dd, Abc_Ntk_t * pNtk, bool fVerbose ); +static Abc_Ntk_t * Abc_NtkDsdInternal( Abc_Ntk_t * pNtk, bool fVerbose, bool fPrint, bool fShort ); static void Abc_NtkDsdConstruct( Dsd_Manager_t * pManDsd, Abc_Ntk_t * pNtk, Abc_Ntk_t * pNtkNew ); static Abc_Obj_t * Abc_NtkDsdConstructNode( Dsd_Manager_t * pManDsd, Dsd_Node_t * pNodeDsd, Abc_Ntk_t * pNtkNew ); @@ -58,25 +57,25 @@ Abc_Ntk_t * Abc_NtkDsdGlobal( Abc_Ntk_t * pNtk, bool fVerbose, bool fPrint, bool { int fCheck = 1; Abc_Ntk_t * pNtkNew; - DdManager * dd; assert( Abc_NtkIsStrash(pNtk) ); // perform FPGA mapping - dd = Abc_NtkGlobalBdds( pNtk, 0 ); - if ( dd == NULL ) + if ( Abc_NtkGlobalBdds(pNtk, 0) == NULL ) return NULL; if ( fVerbose ) - printf( "The shared BDD size is %d nodes.\n", Cudd_ReadKeys(dd) - Cudd_ReadDead(dd) ); + printf( "The shared BDD size is %d nodes.\n", Cudd_ReadKeys(pNtk->pManGlob) - Cudd_ReadDead(pNtk->pManGlob) ); // transform the result of mapping into a BDD network - pNtkNew = Abc_NtkDsdInternal( dd, pNtk, fVerbose, fPrint, fShort ); + pNtkNew = Abc_NtkDsdInternal( pNtk, fVerbose, fPrint, fShort ); if ( pNtkNew == NULL ) { - Cudd_Quit( dd ); + Cudd_Quit( pNtk->pManGlob ); + pNtk->pManGlob = NULL; return NULL; } - Extra_StopManager( dd ); + Extra_StopManager( pNtk->pManGlob ); + pNtk->pManGlob = NULL; // make sure that everything is okay if ( fCheck && !Abc_NtkCheck( pNtkNew ) ) @@ -99,17 +98,33 @@ Abc_Ntk_t * Abc_NtkDsdGlobal( Abc_Ntk_t * pNtk, bool fVerbose, bool fPrint, bool SeeAlso [] ***********************************************************************/ -Abc_Ntk_t * Abc_NtkDsdInternal( DdManager * dd, Abc_Ntk_t * pNtk, bool fVerbose, bool fPrint, bool fShort ) +Abc_Ntk_t * Abc_NtkDsdInternal( Abc_Ntk_t * pNtk, bool fVerbose, bool fPrint, bool fShort ) { + DdManager * dd = pNtk->pManGlob; Dsd_Manager_t * pManDsd; Abc_Ntk_t * pNtkNew; + DdNode * bFunc; char ** ppNamesCi, ** ppNamesCo; + Abc_Obj_t * pObj; + int i; + + // complement the global functions + Abc_NtkForEachCo( pNtk, pObj, i ) + { + bFunc = Vec_PtrEntry(pNtk->vFuncsGlob, i); + Vec_PtrWriteEntry(pNtk->vFuncsGlob, i, Cudd_NotCond(bFunc, Abc_ObjFaninC0(pObj)) ); + } // perform the decomposition - pManDsd = Abc_NtkDsdPerform( dd, pNtk, fVerbose ); - Abc_NtkFreeGlobalBdds( dd, pNtk ); + assert( Vec_PtrSize(pNtk->vFuncsGlob) == Abc_NtkCoNum(pNtk) ); + pManDsd = Dsd_ManagerStart( dd, Abc_NtkCiNum(pNtk), fVerbose ); + Dsd_Decompose( pManDsd, (DdNode **)pNtk->vFuncsGlob->pArray, Abc_NtkCoNum(pNtk) ); + Abc_NtkFreeGlobalBdds( pNtk ); if ( pManDsd == NULL ) + { + Cudd_Quit( dd ); return NULL; + } // start the new network pNtkNew = Abc_NtkStartFrom( pNtk, ABC_TYPE_LOGIC, ABC_FUNC_BDD ); @@ -119,6 +134,8 @@ Abc_Ntk_t * Abc_NtkDsdInternal( DdManager * dd, Abc_Ntk_t * pNtk, bool fVerbose, Abc_NtkDsdConstruct( pManDsd, pNtk, pNtkNew ); // finalize the new network Abc_NtkFinalize( pNtk, pNtkNew ); + // fix the problem with complemented and duplicated CO edges + Abc_NtkLogicMakeSimpleCos( pNtkNew, 0 ); if ( fPrint ) { @@ -134,39 +151,6 @@ Abc_Ntk_t * Abc_NtkDsdInternal( DdManager * dd, Abc_Ntk_t * pNtk, bool fVerbose, return pNtkNew; } -/**Function************************************************************* - - Synopsis [Performs DSD by creating the manager and decomposing the functions.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -Dsd_Manager_t * Abc_NtkDsdPerform( DdManager * dd, Abc_Ntk_t * pNtk, bool fVerbose ) -{ - Dsd_Manager_t * pManDsd; - DdNode ** pbFuncsGlo; - Abc_Obj_t * pNode; - int i; - - // collect global functions into the array - pbFuncsGlo = ALLOC( DdNode *, Abc_NtkCoNum(pNtk) ); - Abc_NtkForEachCo( pNtk, pNode, i ) - { - pbFuncsGlo[i] = Cudd_NotCond( pNode->pNext, Abc_ObjFaninC0(pNode) ); -//printf( "Output %3d : Support size = %3d. Nodes = %5d.\n", i, Cudd_SupportSize(dd, pbFuncsGlo[i]), Cudd_DagSize(pbFuncsGlo[i]) ); - } - - // start the DSD manager and decompose global functions - pManDsd = Dsd_ManagerStart( dd, Abc_NtkCiNum(pNtk), fVerbose ); - Dsd_Decompose( pManDsd, pbFuncsGlo, Abc_NtkCoNum(pNtk) ); - FREE( pbFuncsGlo ); - return pManDsd; -} - /**Function************************************************************* Synopsis [Constructs the decomposed network.] diff --git a/src/base/abc/abcFraig.c b/src/base/abc/abcFraig.c index bb7d8cfa..83735e47 100644 --- a/src/base/abc/abcFraig.c +++ b/src/base/abc/abcFraig.c @@ -433,7 +433,7 @@ int Abc_NtkFraigStore( Abc_Ntk_t * pNtk ) if ( pStore == NULL ) { // start the stored network - pStore = Abc_NtkStrash( pNtk, 0 ); + pStore = Abc_NtkStrash( pNtk, 0, 0 ); if ( pStore == NULL ) { printf( "Abc_NtkFraigStore: Initial strashing has failed.\n" ); diff --git a/src/base/abc/abcFunc.c b/src/base/abc/abcFunc.c index f616a258..44acb699 100644 --- a/src/base/abc/abcFunc.c +++ b/src/base/abc/abcFunc.c @@ -128,6 +128,57 @@ DdNode * Abc_ConvertSopToBdd( DdManager * dd, char * pSop, int nFanins ) return bRes; } +/**Function************************************************************* + + Synopsis [Removes complemented SOP covers.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Abc_NtkLogicMakeDirectSops( Abc_Ntk_t * pNtk ) +{ + DdManager * dd; + DdNode * bFunc; + Vec_Str_t * vCube; + Abc_Obj_t * pNode; + int nFaninsMax, fFound, i; + + assert( Abc_NtkIsSopLogic(pNtk) ); + + // check if there are nodes with complemented SOPs + fFound = 0; + Abc_NtkForEachNode( pNtk, pNode, i ) + if ( Abc_SopIsComplement(pNode->pData) ) + { + fFound = 1; + break; + } + if ( !fFound ) + return; + + // start the BDD package + nFaninsMax = Abc_NtkGetFaninMax( pNtk ); + if ( nFaninsMax == 0 ) + printf( "Warning: The network has only constant nodes.\n" ); + dd = Cudd_Init( nFaninsMax, 0, CUDD_UNIQUE_SLOTS, CUDD_CACHE_SLOTS, 0 ); + + // change the cover of negated nodes + vCube = Vec_StrAlloc( 100 ); + Abc_NtkForEachNode( pNtk, pNode, i ) + if ( Abc_SopIsComplement(pNode->pData) ) + { + bFunc = Abc_ConvertSopToBdd( dd, pNode->pData, Abc_ObjFaninNum(pNode) ); 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) ); + } + Vec_StrFree( vCube ); + Extra_StopManager( dd ); +} diff --git a/src/base/abc/abcMiter.c b/src/base/abc/abcMiter.c index b8bcec4d..a0426dc2 100644 --- a/src/base/abc/abcMiter.c +++ b/src/base/abc/abcMiter.c @@ -55,8 +55,8 @@ Abc_Ntk_t * Abc_NtkMiter( Abc_Ntk_t * pNtk1, Abc_Ntk_t * pNtk2, int fComb ) if ( !Abc_NtkCompareSignals( pNtk1, pNtk2, fComb ) ) return NULL; // make sure the circuits are strashed - fRemove1 = (!Abc_NtkIsStrash(pNtk1)) && (pNtk1 = Abc_NtkStrash(pNtk1, 0)); - fRemove2 = (!Abc_NtkIsStrash(pNtk2)) && (pNtk2 = Abc_NtkStrash(pNtk2, 0)); + fRemove1 = (!Abc_NtkIsStrash(pNtk1)) && (pNtk1 = Abc_NtkStrash(pNtk1, 0, 0)); + fRemove2 = (!Abc_NtkIsStrash(pNtk2)) && (pNtk2 = Abc_NtkStrash(pNtk2, 0, 0)); if ( pNtk1 && pNtk2 ) pTemp = Abc_NtkMiterInt( pNtk1, pNtk2, fComb ); if ( fRemove1 ) Abc_NtkDelete( pNtk1 ); diff --git a/src/base/abc/abcPrint.c b/src/base/abc/abcPrint.c index 337dd43b..c7599f11 100644 --- a/src/base/abc/abcPrint.c +++ b/src/base/abc/abcPrint.c @@ -44,8 +44,8 @@ void Abc_NtkPrintStats( FILE * pFile, Abc_Ntk_t * pNtk, int fFactored ) { int Num; - fprintf( pFile, "%-15s:", pNtk->pName ); - fprintf( pFile, " i/o = %4d/%4d", Abc_NtkPiNum(pNtk), Abc_NtkPoNum(pNtk) ); + fprintf( pFile, "%-13s:", pNtk->pName ); + fprintf( pFile, " i/o = %4d/%4d", Abc_NtkPiNum(pNtk), Abc_NtkPoNum(pNtk) ); if ( !Abc_NtkIsSeq(pNtk) ) fprintf( pFile, " lat = %4d", Abc_NtkLatchNum(pNtk) ); diff --git a/src/base/abc/abcReconv.c b/src/base/abc/abcReconv.c index e02ccba0..ea662799 100644 --- a/src/base/abc/abcReconv.c +++ b/src/base/abc/abcReconv.c @@ -30,14 +30,19 @@ struct Abc_ManCut_t_ // user specified parameters int nNodeSizeMax; // the limit on the size of the supernode int nConeSizeMax; // the limit on the size of the containing cone + int nNodeFanStop; // the limit on the size of the supernode + int nConeFanStop; // the limit on the size of the containing cone // internal parameters - Vec_Ptr_t * vFaninsNode; // fanins of the supernode - Vec_Ptr_t * vFaninsCone; // fanins of the containing cone + Vec_Ptr_t * vNodeLeaves; // fanins of the collapsed node (the cut) + Vec_Ptr_t * vConeLeaves; // fanins of the containing cone Vec_Ptr_t * vVisited; // the visited nodes + Vec_Vec_t * vLevels; // the data structure to compute TFO nodes + Vec_Ptr_t * vNodesTfo; // the nodes in the TFO of the cut }; -static int Abc_NodeFindCut_int( Vec_Ptr_t * vFanins, int nSizeLimit ); -static void Abc_NodesMarkCollect_rec( Abc_Obj_t * pNode, Vec_Ptr_t * vVisited ); +static int Abc_NodeBuildCutLevelOne_int( Vec_Ptr_t * vVisited, Vec_Ptr_t * vLeaves, int nSizeLimit, int nFaninLimit ); +static int Abc_NodeBuildCutLevelTwo_int( Vec_Ptr_t * vVisited, Vec_Ptr_t * vLeaves, int nFaninLimit ); +static void Abc_NodeConeMarkCollect_rec( Abc_Obj_t * pNode, Vec_Ptr_t * vVisited ); //////////////////////////////////////////////////////////////////////// /// FUNCTION DEFITIONS /// @@ -92,45 +97,142 @@ static inline void Abc_NodesUnmark( Vec_Ptr_t * vVisited ) SeeAlso [] ***********************************************************************/ -static inline void Abc_NodesUnmarkBoth( Vec_Ptr_t * vVisited ) +static inline void Abc_NodesUnmarkB( Vec_Ptr_t * vVisited ) { Abc_Obj_t * pNode; int i; Vec_PtrForEachEntry( vVisited, pNode, i ) - pNode->fMarkA = pNode->fMarkB = 0; + pNode->fMarkB = 0; } /**Function************************************************************* - Synopsis [Evaluate the fanin cost.] + Synopsis [Evaluate the cost of removing the node from the set of leaves.] - Description [Returns the number of fanins that will be brought in. - Returns large number if the node cannot be added.] + Description [Returns the number of new leaves that will be brought in. + Returns large number if the node cannot be removed from the set of leaves.] SideEffects [] SeeAlso [] ***********************************************************************/ -static inline int Abc_NodeGetFaninCost( Abc_Obj_t * pNode ) +static inline int Abc_NodeGetLeafCostOne( Abc_Obj_t * pNode, int nFaninLimit ) { - Abc_Obj_t * pFanout; - int i; - assert( pNode->fMarkA == 1 ); // this node is in the TFI - assert( pNode->fMarkB == 1 ); // this node is in the constructed cone - // check the PI node + int Cost; + // make sure the node is in the construction zone + assert( pNode->fMarkB == 1 ); + // cannot expand over the PI node + if ( Abc_ObjIsCi(pNode) ) + return 999; + // get the cost of the cone + Cost = (!Abc_ObjFanin0(pNode)->fMarkB) + (!Abc_ObjFanin1(pNode)->fMarkB); + // always accept if the number of leaves does not increase + if ( Cost < 2 ) + return Cost; + // skip nodes with many fanouts + if ( Abc_ObjFanoutNum(pNode) > nFaninLimit ) + return 999; + // return the number of nodes that will be on the leaves if this node is removed + return Cost; +} + +/**Function************************************************************* + + Synopsis [Evaluate the cost of removing the node from the set of leaves.] + + Description [Returns the number of new leaves that will be brought in. + Returns large number if the node cannot be removed from the set of leaves.] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +static inline int Abc_NodeGetLeafCostTwo( Abc_Obj_t * pNode, int nFaninLimit, + Abc_Obj_t ** ppLeafToAdd, Abc_Obj_t ** pNodeToMark1, Abc_Obj_t ** pNodeToMark2 ) +{ + Abc_Obj_t * pFanin0, * pFanin1, * pTemp; + Abc_Obj_t * pGrand, * pGrandToAdd; + // make sure the node is in the construction zone + assert( pNode->fMarkB == 1 ); + // cannot expand over the PI node if ( Abc_ObjIsCi(pNode) ) return 999; // skip nodes with many fanouts - if ( Abc_ObjFanoutNum(pNode) > 5 ) +// if ( Abc_ObjFanoutNum(pNode) > nFaninLimit ) +// return 999; + // get the children + pFanin0 = Abc_ObjFanin0(pNode); + pFanin1 = Abc_ObjFanin1(pNode); + assert( !pFanin0->fMarkB && !pFanin1->fMarkB ); + // count the number of unique grandchildren that will be included + // return infinite cost if this number if more than 1 + if ( Abc_ObjIsCi(pFanin0) && Abc_ObjIsCi(pFanin1) ) return 999; - // check the fanouts - Abc_ObjForEachFanout( pNode, pFanout, i ) - if ( pFanout->fMarkA && pFanout->fMarkB == 0 ) // the fanout is in the TFI but not in the cone + // consider the special case when a non-CI fanin can be dropped + if ( !Abc_ObjIsCi(pFanin0) && Abc_ObjFanin0(pFanin0)->fMarkB && Abc_ObjFanin1(pFanin0)->fMarkB ) + { + *ppLeafToAdd = pFanin1; + *pNodeToMark1 = pFanin0; + *pNodeToMark2 = NULL; + return 1; + } + if ( !Abc_ObjIsCi(pFanin1) && Abc_ObjFanin0(pFanin1)->fMarkB && Abc_ObjFanin1(pFanin1)->fMarkB ) + { + *ppLeafToAdd = pFanin0; + *pNodeToMark1 = pFanin1; + *pNodeToMark2 = NULL; + return 1; + } + + // make the first node CI if any + if ( Abc_ObjIsCi(pFanin1) ) + pTemp = pFanin0, pFanin0 = pFanin1, pFanin1 = pTemp; + // consider the first node + pGrandToAdd = NULL; + if ( Abc_ObjIsCi(pFanin0) ) + { + *pNodeToMark1 = NULL; + pGrandToAdd = pFanin0; + } + else + { + *pNodeToMark1 = pFanin0; + pGrand = Abc_ObjFanin0(pFanin0); + if ( !pGrand->fMarkB ) + { + if ( pGrandToAdd && pGrandToAdd != pGrand ) + return 999; + pGrandToAdd = pGrand; + } + pGrand = Abc_ObjFanin1(pFanin0); + if ( !pGrand->fMarkB ) + { + if ( pGrandToAdd && pGrandToAdd != pGrand ) + return 999; + pGrandToAdd = pGrand; + } + } + // consider the second node + *pNodeToMark2 = pFanin1; + pGrand = Abc_ObjFanin0(pFanin1); + if ( !pGrand->fMarkB ) + { + if ( pGrandToAdd && pGrandToAdd != pGrand ) + return 999; + pGrandToAdd = pGrand; + } + pGrand = Abc_ObjFanin1(pFanin1); + if ( !pGrand->fMarkB ) + { + if ( pGrandToAdd && pGrandToAdd != pGrand ) return 999; - // the fanouts are in the TFI and inside the constructed cone - // return the number of fanins that will be on the boundary if this node is added - return (!Abc_ObjFanin0(pNode)->fMarkB) + (!Abc_ObjFanin1(pNode)->fMarkB); + pGrandToAdd = pGrand; + } + assert( pGrandToAdd != NULL ); + *ppLeafToAdd = pGrandToAdd; + return 1; } @@ -153,115 +255,204 @@ Vec_Ptr_t * Abc_NodeFindCut( Abc_ManCut_t * p, Abc_Obj_t * pRoot, bool fContain assert( !Abc_ObjIsComplement(pRoot) ); assert( Abc_ObjIsNode(pRoot) ); - // mark TFI using fMarkA + // start the visited nodes and mark them Vec_PtrClear( p->vVisited ); - Abc_NodesMarkCollect_rec( pRoot, p->vVisited ); - - // start the cut - Vec_PtrClear( p->vFaninsNode ); - Vec_PtrPush( p->vFaninsNode, Abc_ObjFanin0(pRoot) ); - Vec_PtrPush( p->vFaninsNode, Abc_ObjFanin1(pRoot) ); + Vec_PtrPush( p->vVisited, pRoot ); + Vec_PtrPush( p->vVisited, Abc_ObjFanin0(pRoot) ); + Vec_PtrPush( p->vVisited, Abc_ObjFanin1(pRoot) ); pRoot->fMarkB = 1; Abc_ObjFanin0(pRoot)->fMarkB = 1; Abc_ObjFanin1(pRoot)->fMarkB = 1; + // start the cut + Vec_PtrClear( p->vNodeLeaves ); + Vec_PtrPush( p->vNodeLeaves, Abc_ObjFanin0(pRoot) ); + Vec_PtrPush( p->vNodeLeaves, Abc_ObjFanin1(pRoot) ); + // compute the cut - while ( Abc_NodeFindCut_int( p->vFaninsNode, p->nNodeSizeMax ) ); - assert( Vec_PtrSize(p->vFaninsNode) <= p->nNodeSizeMax ); + while ( Abc_NodeBuildCutLevelOne_int( p->vVisited, p->vNodeLeaves, p->nNodeSizeMax, p->nNodeFanStop ) ); + assert( Vec_PtrSize(p->vNodeLeaves) <= p->nNodeSizeMax ); // return if containing cut is not requested if ( !fContain ) { - // unmark TFI using fMarkA and fMarkB - Abc_NodesUnmarkBoth( p->vVisited ); - return p->vFaninsNode; + // unmark both fMarkA and fMarkB in tbe TFI + Abc_NodesUnmarkB( p->vVisited ); + return p->vNodeLeaves; } +//printf( "\n\n\n" ); // compute the containing cut assert( p->nNodeSizeMax < p->nConeSizeMax ); // copy the current boundary - Vec_PtrClear( p->vFaninsCone ); - Vec_PtrForEachEntry( p->vFaninsNode, pNode, i ) - Vec_PtrPush( p->vFaninsCone, pNode ); + Vec_PtrClear( p->vConeLeaves ); + Vec_PtrForEachEntry( p->vNodeLeaves, pNode, i ) + Vec_PtrPush( p->vConeLeaves, pNode ); // compute the containing cut - while ( Abc_NodeFindCut_int( p->vFaninsCone, p->nConeSizeMax ) ); - assert( Vec_PtrSize(p->vFaninsCone) <= p->nConeSizeMax ); + while ( Abc_NodeBuildCutLevelOne_int( p->vVisited, p->vConeLeaves, p->nConeSizeMax, p->nConeFanStop ) ); + assert( Vec_PtrSize(p->vConeLeaves) <= p->nConeSizeMax ); // unmark TFI using fMarkA and fMarkB - Abc_NodesUnmarkBoth( p->vVisited ); - return p->vFaninsNode; + Abc_NodesUnmarkB( p->vVisited ); + return p->vNodeLeaves; } /**Function************************************************************* - Synopsis [Finds a reconvergence-driven cut.] + Synopsis [Builds reconvergence-driven cut by changing one leaf at a time.] - Description [] + Description [This procedure looks at the current leaves and tries to change + one leaf at a time in such a way that the cut grows as little as possible. + In evaluating the fanins, this procedure looks only at their immediate + predecessors (this is why it is called a one-level construction procedure).] SideEffects [] SeeAlso [] ***********************************************************************/ -int Abc_NodeFindCut_int( Vec_Ptr_t * vFanins, int nSizeLimit ) +int Abc_NodeBuildCutLevelOne_int( Vec_Ptr_t * vVisited, Vec_Ptr_t * vLeaves, int nSizeLimit, int nFaninLimit ) { Abc_Obj_t * pNode, * pFaninBest, * pNext; int CostBest, CostCur, i; -// int fFlagProb = (rand() & 1); - int fFlagProb = 1; // find the best fanin CostBest = 100; pFaninBest = NULL; - if ( fFlagProb ) - { - Vec_PtrForEachEntry( vFanins, pNode, i ) - { - CostCur = Abc_NodeGetFaninCost( pNode ); - if ( CostBest > CostCur ) - { - CostBest = CostCur; - pFaninBest = pNode; - } - } - } - else +//printf( "Evaluating fanins of the cut:\n" ); + Vec_PtrForEachEntry( vLeaves, pNode, i ) { - Vec_PtrForEachEntry( vFanins, pNode, i ) + CostCur = Abc_NodeGetLeafCostOne( pNode, nFaninLimit ); +//printf( " Fanin %s has cost %d.\n", Abc_ObjName(pNode), CostCur ); + if ( CostBest > CostCur ) { - CostCur = Abc_NodeGetFaninCost( pNode ); - if ( CostBest >= CostCur ) - { - CostBest = CostCur; - pFaninBest = pNode; - } + CostBest = CostCur; + pFaninBest = pNode; } + if ( CostBest == 0 ) + break; } if ( pFaninBest == NULL ) return 0; +// return Abc_NodeBuildCutLevelTwo_int( vVisited, vLeaves, nFaninLimit ); + assert( CostBest < 3 ); - if ( vFanins->nSize - 1 + CostBest > nSizeLimit ) + if ( vLeaves->nSize - 1 + CostBest > nSizeLimit ) return 0; +// return Abc_NodeBuildCutLevelTwo_int( vVisited, vLeaves, nFaninLimit ); + assert( Abc_ObjIsNode(pFaninBest) ); // remove the node from the array - Vec_PtrRemove( vFanins, pFaninBest ); + Vec_PtrRemove( vLeaves, pFaninBest ); +//printf( "Removing fanin %s.\n", Abc_ObjName(pFaninBest) ); + // add the left child to the fanins pNext = Abc_ObjFanin0(pFaninBest); if ( !pNext->fMarkB ) { +//printf( "Adding fanin %s.\n", Abc_ObjName(pNext) ); pNext->fMarkB = 1; - Vec_PtrPush( vFanins, pNext ); + Vec_PtrPush( vLeaves, pNext ); + Vec_PtrPush( vVisited, pNext ); } // add the right child to the fanins pNext = Abc_ObjFanin1(pFaninBest); if ( !pNext->fMarkB ) { +//printf( "Adding fanin %s.\n", Abc_ObjName(pNext) ); pNext->fMarkB = 1; - Vec_PtrPush( vFanins, pNext ); + Vec_PtrPush( vLeaves, pNext ); + Vec_PtrPush( vVisited, pNext ); } - assert( vFanins->nSize <= nSizeLimit ); + assert( vLeaves->nSize <= nSizeLimit ); // keep doing this return 1; } +/**Function************************************************************* + + Synopsis [Builds reconvergence-driven cut by changing one leaf at a time.] + + Description [This procedure looks at the current leaves and tries to change + one leaf at a time in such a way that the cut grows as little as possible. + In evaluating the fanins, this procedure looks across two levels of fanins + (this is why it is called a two-level construction procedure).] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Abc_NodeBuildCutLevelTwo_int( Vec_Ptr_t * vVisited, Vec_Ptr_t * vLeaves, int nFaninLimit ) +{ + Abc_Obj_t * pNode, * pLeafToAdd, * pNodeToMark1, * pNodeToMark2; + int CostCur, i; + // find the best fanin + Vec_PtrForEachEntry( vLeaves, pNode, i ) + { + CostCur = Abc_NodeGetLeafCostTwo( pNode, nFaninLimit, &pLeafToAdd, &pNodeToMark1, &pNodeToMark2 ); + if ( CostCur < 2 ) + break; + } + if ( CostCur > 2 ) + return 0; + // remove the node from the array + Vec_PtrRemove( vLeaves, pNode ); + // add the node to the leaves + if ( pLeafToAdd ) + { + assert( !pLeafToAdd->fMarkB ); + pLeafToAdd->fMarkB = 1; + Vec_PtrPush( vLeaves, pLeafToAdd ); + Vec_PtrPush( vVisited, pLeafToAdd ); + } + // mark the other nodes + if ( pNodeToMark1 ) + { + assert( !pNodeToMark1->fMarkB ); + pNodeToMark1->fMarkB = 1; + Vec_PtrPush( vVisited, pNodeToMark1 ); + } + if ( pNodeToMark2 ) + { + assert( !pNodeToMark2->fMarkB ); + pNodeToMark2->fMarkB = 1; + Vec_PtrPush( vVisited, pNodeToMark2 ); + } + // keep doing this + return 1; +} + + +/**Function************************************************************* + + Synopsis [Get the nodes contained in the cut.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Abc_NodeConeCollect( Abc_Obj_t ** ppRoots, int nRoots, Vec_Ptr_t * vLeaves, Vec_Ptr_t * vVisited, int fIncludeFanins ) +{ + Abc_Obj_t * pTemp; + int i; + // mark the fanins of the cone + Abc_NodesMark( vLeaves ); + // collect the nodes in the DFS order + Vec_PtrClear( vVisited ); + // add the fanins + if ( fIncludeFanins ) + Vec_PtrForEachEntry( vLeaves, pTemp, i ) + Vec_PtrPush( vVisited, pTemp ); + // add other nodes + for ( i = 0; i < nRoots; i++ ) + Abc_NodeConeMarkCollect_rec( ppRoots[i], vVisited ); + // unmark both sets + Abc_NodesUnmark( vLeaves ); + Abc_NodesUnmark( vVisited ); +} + /**Function************************************************************* Synopsis [Marks the TFI cone.] @@ -273,22 +464,21 @@ int Abc_NodeFindCut_int( Vec_Ptr_t * vFanins, int nSizeLimit ) SeeAlso [] ***********************************************************************/ -void Abc_NodesMarkCollect_rec( Abc_Obj_t * pNode, Vec_Ptr_t * vVisited ) +void Abc_NodeConeMarkCollect_rec( Abc_Obj_t * pNode, Vec_Ptr_t * vVisited ) { if ( pNode->fMarkA == 1 ) return; // visit transitive fanin if ( Abc_ObjIsNode(pNode) ) { - Abc_NodesMarkCollect_rec( Abc_ObjFanin0(pNode), vVisited ); - Abc_NodesMarkCollect_rec( Abc_ObjFanin1(pNode), vVisited ); + Abc_NodeConeMarkCollect_rec( Abc_ObjFanin0(pNode), vVisited ); + Abc_NodeConeMarkCollect_rec( Abc_ObjFanin1(pNode), vVisited ); } assert( pNode->fMarkA == 0 ); pNode->fMarkA = 1; Vec_PtrPush( vVisited, pNode ); } - /**Function************************************************************* Synopsis [Returns BDD representing the logic function of the cone.] @@ -300,20 +490,14 @@ void Abc_NodesMarkCollect_rec( Abc_Obj_t * pNode, Vec_Ptr_t * vVisited ) SeeAlso [] ***********************************************************************/ -DdNode * Abc_NodeConeBdd( DdManager * dd, DdNode ** pbVars, Abc_Obj_t * pNode, Vec_Ptr_t * vFanins, Vec_Ptr_t * vVisited ) +DdNode * Abc_NodeConeBdd( DdManager * dd, DdNode ** pbVars, Abc_Obj_t * pNode, Vec_Ptr_t * vLeaves, Vec_Ptr_t * vVisited ) { DdNode * bFunc0, * bFunc1, * bFunc; int i; - // mark the fanins of the cone - Abc_NodesMark( vFanins ); - // collect the nodes in the DFS order - Vec_PtrClear( vVisited ); - Abc_NodesMarkCollect_rec( pNode, vVisited ); - // unmark both sets - Abc_NodesUnmark( vFanins ); - Abc_NodesUnmark( vVisited ); + // get the nodes in the cut without fanins in the DFS order + Abc_NodeConeCollect( &pNode, 1, vLeaves, vVisited, 0 ); // set the elementary BDDs - Vec_PtrForEachEntry( vFanins, pNode, i ) + Vec_PtrForEachEntry( vLeaves, pNode, i ) pNode->pCopy = (Abc_Obj_t *)pbVars[i]; // compute the BDDs for the collected nodes Vec_PtrForEachEntry( vVisited, pNode, i ) @@ -347,15 +531,8 @@ DdNode * Abc_NodeConeDcs( DdManager * dd, DdNode ** pbVarsX, DdNode ** pbVarsY, DdNode * bFunc0, * bFunc1, * bFunc, * bTrans, * bTemp, * bCube, * bResult; Abc_Obj_t * pNode; int i; - // mark the fanins of the cone - Abc_NodesMark( vLeaves ); - // collect the nodes in the DFS order - Vec_PtrClear( vVisited ); - Vec_PtrForEachEntry( vRoots, pNode, i ) - Abc_NodesMarkCollect_rec( pNode, vVisited ); - // unmark both sets - Abc_NodesUnmark( vLeaves ); - Abc_NodesUnmark( vVisited ); + // get the nodes in the cut without fanins in the DFS order + Abc_NodeConeCollect( (Abc_Obj_t **)vRoots->pArray, vRoots->nSize, vLeaves, vVisited, 0 ); // set the elementary BDDs Vec_PtrForEachEntry( vLeaves, pNode, i ) pNode->pCopy = (Abc_Obj_t *)pbVarsX[i]; @@ -400,16 +577,20 @@ DdNode * Abc_NodeConeDcs( DdManager * dd, DdNode ** pbVarsX, DdNode ** pbVarsY, SeeAlso [] ***********************************************************************/ -Abc_ManCut_t * Abc_NtkManCutStart( int nNodeSizeMax, int nConeSizeMax ) +Abc_ManCut_t * Abc_NtkManCutStart( int nNodeSizeMax, int nConeSizeMax, int nNodeFanStop, int nConeFanStop ) { Abc_ManCut_t * p; p = ALLOC( Abc_ManCut_t, 1 ); memset( p, 0, sizeof(Abc_ManCut_t) ); - p->vFaninsNode = Vec_PtrAlloc( 100 ); - p->vFaninsCone = Vec_PtrAlloc( 100 ); + p->vNodeLeaves = Vec_PtrAlloc( 100 ); + p->vConeLeaves = Vec_PtrAlloc( 100 ); p->vVisited = Vec_PtrAlloc( 100 ); + p->vLevels = Vec_VecAlloc( 100 ); + p->vNodesTfo = Vec_PtrAlloc( 100 ); p->nNodeSizeMax = nNodeSizeMax; p->nConeSizeMax = nConeSizeMax; + p->nNodeFanStop = nNodeFanStop; + p->nConeFanStop = nConeFanStop; return p; } @@ -426,9 +607,11 @@ Abc_ManCut_t * Abc_NtkManCutStart( int nNodeSizeMax, int nConeSizeMax ) ***********************************************************************/ void Abc_NtkManCutStop( Abc_ManCut_t * p ) { - Vec_PtrFree( p->vFaninsNode ); - Vec_PtrFree( p->vFaninsCone ); + Vec_PtrFree( p->vNodeLeaves ); + Vec_PtrFree( p->vConeLeaves ); Vec_PtrFree( p->vVisited ); + Vec_VecFree( p->vLevels ); + Vec_PtrFree( p->vNodesTfo ); free( p ); } @@ -443,9 +626,25 @@ void Abc_NtkManCutStop( Abc_ManCut_t * p ) SeeAlso [] ***********************************************************************/ -Vec_Ptr_t * Abc_NtkManCutReadLeaves( Abc_ManCut_t * p ) +Vec_Ptr_t * Abc_NtkManCutReadCutLarge( Abc_ManCut_t * p ) +{ + return p->vConeLeaves; +} + +/**Function************************************************************* + + Synopsis [Returns the leaves of the cone.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Vec_Ptr_t * Abc_NtkManCutReadVisited( Abc_ManCut_t * p ) { - return p->vFaninsCone; + return p->vVisited; } @@ -466,27 +665,27 @@ Vec_Ptr_t * Abc_NtkManCutReadLeaves( Abc_ManCut_t * p ) SeeAlso [] ***********************************************************************/ -void Abc_NodeCollectTfoCands( Abc_Ntk_t * pNtk, Abc_Obj_t * pRoot, - Vec_Ptr_t * vFanins, int LevelMax, Vec_Vec_t * vLevels, Vec_Ptr_t * vResult ) +Vec_Ptr_t * Abc_NodeCollectTfoCands( Abc_ManCut_t * p, Abc_Obj_t * pRoot, Vec_Ptr_t * vLeaves, int LevelMax ) { + Abc_Ntk_t * pNtk = pRoot->pNtk; Vec_Ptr_t * vVec; Abc_Obj_t * pNode, * pFanout; int i, k, v, LevelMin; assert( Abc_NtkIsStrash(pNtk) ); // assuming that the structure is clean - Vec_VecForEachLevel( vLevels, vVec, i ) + Vec_VecForEachLevel( p->vLevels, vVec, i ) assert( vVec->nSize == 0 ); // put fanins into the structure while labeling them Abc_NtkIncrementTravId( pNtk ); - LevelMin = ABC_INFINITY; - Vec_PtrForEachEntry( vFanins, pNode, i ) + LevelMin = -1; + Vec_PtrForEachEntry( vLeaves, pNode, i ) { if ( pNode->Level > (unsigned)LevelMax ) continue; Abc_NodeSetTravIdCurrent( pNode ); - Vec_VecPush( vLevels, pNode->Level, pNode ); + Vec_VecPush( p->vLevels, pNode->Level, pNode ); if ( LevelMin < (int)pNode->Level ) LevelMin = pNode->Level; } @@ -497,9 +696,11 @@ void Abc_NodeCollectTfoCands( Abc_Ntk_t * pNtk, Abc_Obj_t * pRoot, Abc_NodeMffcLabel( pRoot ); // go through the levels up - Vec_PtrClear( vResult ); - Vec_VecForEachEntryStartStop( vLevels, pNode, i, k, LevelMin, LevelMax ) + Vec_PtrClear( p->vNodesTfo ); + Vec_VecForEachEntryStart( p->vLevels, pNode, i, k, LevelMin ) { + if ( i > LevelMax ) + break; // if the node is not marked, it is not a fanin if ( !Abc_NodeIsTravIdCurrent(pNode) ) { @@ -508,7 +709,7 @@ void Abc_NodeCollectTfoCands( Abc_Ntk_t * pNtk, Abc_Obj_t * pRoot, !Abc_NodeIsTravIdCurrent(Abc_ObjFanin1(pNode)) ) continue; // save the node in the TFO and label it - Vec_PtrPush( vResult, pNode ); + Vec_PtrPush( p->vNodesTfo, pNode ); Abc_NodeSetTravIdCurrent( pNode ); } // go through the fanouts and add them to the structure if they meet the conditions @@ -521,13 +722,18 @@ void Abc_NodeCollectTfoCands( Abc_Ntk_t * pNtk, Abc_Obj_t * pRoot, if ( Abc_NodeIsTravIdCurrent(pFanout) ) continue; // add it to the structure but do not mark it (until tested later) - Vec_VecPush( vLevels, pFanout->Level, pFanout ); + Vec_VecPushUnique( p->vLevels, pFanout->Level, pFanout ); } } // clear the levelized structure - Vec_VecForEachLevelStartStop( vLevels, vVec, i, LevelMin, LevelMax ) + Vec_VecForEachLevelStart( p->vLevels, vVec, i, LevelMin ) + { + if ( i > LevelMax ) + break; Vec_PtrClear( vVec ); + } + return p->vNodesTfo; } //////////////////////////////////////////////////////////////////////// diff --git a/src/base/abc/abcRefactor.c b/src/base/abc/abcRefactor.c index 7e387b47..9a413bb1 100644 --- a/src/base/abc/abcRefactor.c +++ b/src/base/abc/abcRefactor.c @@ -96,9 +96,9 @@ int Abc_NtkRefactor( Abc_Ntk_t * pNtk, int nNodeSizeMax, int nConeSizeMax, bool assert( Abc_NtkIsStrash(pNtk) ); // start the managers - pManCut = Abc_NtkManCutStart( nNodeSizeMax, nConeSizeMax ); + pManCut = Abc_NtkManCutStart( nNodeSizeMax, nConeSizeMax, 2, 1000 ); pManRef = Abc_NtkManRefStart( nNodeSizeMax, nConeSizeMax, fUseDcs, fVerbose ); - pManRef->vLeaves = Abc_NtkManCutReadLeaves( pManCut ); + pManRef->vLeaves = Abc_NtkManCutReadCutLarge( pManCut ); Abc_NtkStartReverseLevels( pNtk ); // resynthesize each node once diff --git a/src/base/abc/abcRefs.c b/src/base/abc/abcRefs.c index 081ccfaa..dfcc3ae5 100644 --- a/src/base/abc/abcRefs.c +++ b/src/base/abc/abcRefs.c @@ -174,6 +174,10 @@ void Abc_NodeUpdate( Abc_Obj_t * pNode, Vec_Ptr_t * vFanins, Vec_Int_t * vForm, // 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 diff --git a/src/base/abc/abcShow.c b/src/base/abc/abcShow.c index 730aca90..38840de0 100644 --- a/src/base/abc/abcShow.c +++ b/src/base/abc/abcShow.c @@ -18,22 +18,27 @@ ***********************************************************************/ -#include "abc.h" #ifdef WIN32 -#include "process.h" +#include #endif +#include "abc.h" +#include "io.h" + //////////////////////////////////////////////////////////////////////// /// DECLARATIONS /// //////////////////////////////////////////////////////////////////////// - + +static void Abc_ShowFile( char * FileNameDot ); +static void Abc_ShowGetFileName( char * pName, char * pBuffer ); + //////////////////////////////////////////////////////////////////////// /// FUNCTION DEFITIONS /// //////////////////////////////////////////////////////////////////////// /**Function************************************************************* - Synopsis [Prints the factored form of one node.] + Synopsis [Visualizes BDD of the node.] Description [] @@ -42,15 +47,152 @@ SeeAlso [] ***********************************************************************/ -void Abc_NodePrintBdd( Abc_Obj_t * pNode ) +void Abc_NodeShowBdd( Abc_Obj_t * pNode ) { FILE * pFile; Vec_Ptr_t * vNamesIn; - char * FileNameIn; - char * FileNameOut; - char * FileGeneric; - char * pCur, * pNameOut; char FileNameDot[200]; + char * pNameOut; + + assert( Abc_NtkIsBddLogic(pNode->pNtk) ); + // create the file names + Abc_ShowGetFileName( Abc_ObjName(pNode), FileNameDot ); + // check that the file can be opened + if ( (pFile = fopen( FileNameDot, "w" )) == NULL ) + { + fprintf( stdout, "Cannot open the intermediate file \"%s\".\n", FileNameDot ); + return; + } + + // set the node names + vNamesIn = Abc_NodeGetFaninNames( pNode ); + pNameOut = Abc_ObjName(pNode); + Cudd_DumpDot( pNode->pNtk->pManFunc, 1, (DdNode **)&pNode->pData, (char **)vNamesIn->pArray, &pNameOut, pFile ); + Abc_NodeFreeFaninNames( vNamesIn ); + Abc_NtkCleanCopy( pNode->pNtk ); + fclose( pFile ); + + // visualize the file + Abc_ShowFile( FileNameDot ); +} + +/**Function************************************************************* + + Synopsis [Visualizes AIG with choices.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Abc_NtkShowAig( Abc_Ntk_t * pNtk ) +{ + FILE * pFile; + Abc_Obj_t * pNode; + Vec_Ptr_t * vNodes; + char FileNameDot[200]; + int i; + + assert( Abc_NtkIsStrash(pNtk) ); + // create the file names + Abc_ShowGetFileName( pNtk->pName, FileNameDot ); + // check that the file can be opened + if ( (pFile = fopen( FileNameDot, "w" )) == NULL ) + { + fprintf( stdout, "Cannot open the intermediate file \"%s\".\n", FileNameDot ); + return; + } + + // collect all nodes in the network + vNodes = Vec_PtrAlloc( 100 ); + Abc_NtkForEachObj( pNtk, pNode, i ) + Vec_PtrPush( vNodes, pNode ); + // write the DOT file + Io_WriteDot( pNtk, vNodes, NULL, FileNameDot ); + Vec_PtrFree( vNodes ); + + // visualize the file + Abc_ShowFile( FileNameDot ); +} + +/**Function************************************************************* + + Synopsis [Visualizes reconvergence driven cut at the node.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Abc_NodeShowCut( Abc_Obj_t * pNode, int nNodeSizeMax, int nConeSizeMax ) +{ + FILE * pFile; + char FileNameDot[200]; + Abc_ManCut_t * p; + Vec_Ptr_t * vCutSmall; + Vec_Ptr_t * vCutLarge; + Vec_Ptr_t * vInside; + Vec_Ptr_t * vNodesTfo; + Abc_Obj_t * pTemp; + int i; + + assert( Abc_NtkIsStrash(pNode->pNtk) ); + + // start the cut computation manager + p = Abc_NtkManCutStart( nNodeSizeMax, nConeSizeMax, 2, ABC_INFINITY ); + // get the recovergence driven cut + vCutSmall = Abc_NodeFindCut( p, pNode, 1 ); + // get the containing cut + vCutLarge = Abc_NtkManCutReadCutLarge( p ); + // get the array for the inside nodes + vInside = Abc_NtkManCutReadVisited( p ); + // get the inside nodes of the containing cone + Abc_NodeConeCollect( &pNode, 1, vCutLarge, vInside, 1 ); + + // add the nodes in the TFO + vNodesTfo = Abc_NodeCollectTfoCands( p, pNode, vCutSmall, ABC_INFINITY ); + Vec_PtrForEachEntry( vNodesTfo, pTemp, i ) + Vec_PtrPushUnique( vInside, pTemp ); + + // create the file names + Abc_ShowGetFileName( Abc_ObjName(pNode), FileNameDot ); + // check that the file can be opened + if ( (pFile = fopen( FileNameDot, "w" )) == NULL ) + { + fprintf( stdout, "Cannot open the intermediate file \"%s\".\n", FileNameDot ); + return; + } + // add the root node to the cone (for visualization) + Vec_PtrPush( vCutSmall, pNode ); + // write the DOT file + Io_WriteDot( pNode->pNtk, vInside, vCutSmall, FileNameDot ); + // stop the cut computation manager + Abc_NtkManCutStop( p ); + + // visualize the file + Abc_ShowFile( FileNameDot ); +} + + +/**Function************************************************************* + + Synopsis [Shows the given DOT file.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Abc_ShowFile( char * FileNameDot ) +{ + FILE * pFile; + char * FileGeneric; char FileNamePs[200]; char CommandDot[1000]; #ifndef WIN32 @@ -60,8 +202,6 @@ void Abc_NodePrintBdd( Abc_Obj_t * pNode ) char * pProgGsViewName; int RetValue; - assert( Abc_NtkIsBddLogic(pNode->pNtk) ); - #ifdef WIN32 pProgDotName = "dot.exe"; pProgGsViewName = NULL; @@ -70,34 +210,6 @@ void Abc_NodePrintBdd( Abc_Obj_t * pNode ) pProgGsViewName = "gv"; #endif - FileNameIn = NULL; - FileNameOut = NULL; - - // get the generic file name - pNode->pCopy = NULL; - FileGeneric = Abc_ObjName(pNode); - // get rid of not-alpha-numeric characters - for ( pCur = FileGeneric; *pCur; pCur++ ) - if ( !((*pCur >= '0' && *pCur <= '9') || (*pCur >= 'a' && *pCur <= 'z') || (*pCur >= 'A' && *pCur <= 'Z')) ) - *pCur = '_'; - // create the file names - sprintf( FileNameDot, "%s.dot", FileGeneric ); - sprintf( FileNamePs, "%s.ps", FileGeneric ); - - // write the DOT file - if ( (pFile = fopen( FileNameDot, "w" )) == NULL ) - { - fprintf( stdout, "Cannot open the intermediate file \"%s\".\n", FileNameDot ); - return; - } - // set the node names - vNamesIn = Abc_NodeGetFaninNames( pNode ); - pNameOut = Abc_ObjName(pNode); - Cudd_DumpDot( pNode->pNtk->pManFunc, 1, (DdNode **)&pNode->pData, (char **)vNamesIn->pArray, &pNameOut, pFile ); - Abc_NodeFreeFaninNames( vNamesIn ); - Abc_NtkCleanCopy( pNode->pNtk ); - fclose( pFile ); - // check that the input file is okay if ( (pFile = fopen( FileNameDot, "r" )) == NULL ) { @@ -106,6 +218,12 @@ void Abc_NodePrintBdd( Abc_Obj_t * pNode ) } fclose( pFile ); + // get the generic file name + FileGeneric = Extra_FileNameGeneric( FileNameDot ); + // create the PostScript file name + sprintf( FileNamePs, "%s.ps", FileGeneric ); + free( FileGeneric ); + // generate the DOT file sprintf( CommandDot, "%s -Tps -o %s %s", pProgDotName, FileNamePs, FileNameDot ); RetValue = system( CommandDot ); @@ -146,10 +264,9 @@ void Abc_NodePrintBdd( Abc_Obj_t * pNode ) #endif } - /**Function************************************************************* - Synopsis [] + Synopsis [Derives the DOT file name.] Description [] @@ -158,6 +275,18 @@ void Abc_NodePrintBdd( Abc_Obj_t * pNode ) SeeAlso [] ***********************************************************************/ +void Abc_ShowGetFileName( char * pName, char * pBuffer ) +{ + char * pCur; + // creat the file name + sprintf( pBuffer, "%s.dot", pName ); + // get rid of not-alpha-numeric characters + for ( pCur = pBuffer; *pCur; pCur++ ) + if ( !((*pCur >= '0' && *pCur <= '9') || (*pCur >= 'a' && *pCur <= 'z') || + (*pCur >= 'A' && *pCur <= 'Z') || (*pCur == '.')) ) + *pCur = '_'; +} + //////////////////////////////////////////////////////////////////////// /// END OF FILE /// diff --git a/src/base/abc/abcStrash.c b/src/base/abc/abcStrash.c index 19394fb3..0a28c3c1 100644 --- a/src/base/abc/abcStrash.c +++ b/src/base/abc/abcStrash.c @@ -49,7 +49,7 @@ extern char * Mio_GateReadSop( void * pGate ); SeeAlso [] ***********************************************************************/ -Abc_Ntk_t * Abc_NtkStrash( Abc_Ntk_t * pNtk, bool fAllNodes ) +Abc_Ntk_t * Abc_NtkStrash( Abc_Ntk_t * pNtk, bool fAllNodes, bool fCleanup ) { int fCheck = 1; Abc_Ntk_t * pNtkAig; @@ -68,11 +68,11 @@ Abc_Ntk_t * Abc_NtkStrash( Abc_Ntk_t * pNtk, bool fAllNodes ) // print warning about self-feed latches if ( Abc_NtkCountSelfFeedLatches(pNtkAig) ) printf( "The network has %d self-feeding latches.\n", Abc_NtkCountSelfFeedLatches(pNtkAig) ); - if ( nNodes = Abc_AigCleanup(pNtkAig->pManFunc) ) + if ( fCleanup && (nNodes = Abc_AigCleanup(pNtkAig->pManFunc)) ) printf( "Cleanup has removed %d nodes.\n", nNodes ); // duplicate EXDC if ( pNtk->pExdc ) - pNtkAig->pExdc = Abc_NtkStrash( pNtk->pExdc, 0 ); + pNtkAig->pExdc = Abc_NtkStrash( pNtk->pExdc, 0, 1 ); // make sure everything is okay if ( fCheck && !Abc_NtkCheck( pNtkAig ) ) { diff --git a/src/base/abc/abcSweep.c b/src/base/abc/abcSweep.c index 47565241..61d65ce3 100644 --- a/src/base/abc/abcSweep.c +++ b/src/base/abc/abcSweep.c @@ -61,7 +61,7 @@ bool Abc_NtkFraigSweep( Abc_Ntk_t * pNtk, int fUseInv, int fVerbose ) assert( !Abc_NtkIsStrash(pNtk) ); // derive the AIG - pNtkAig = Abc_NtkStrash( pNtk, 0 ); + pNtkAig = Abc_NtkStrash( pNtk, 0, 1 ); // perform fraiging of the AIG Fraig_ParamsSetDefault( &Params ); pMan = Abc_NtkToFraig( pNtkAig, &Params, 0 ); diff --git a/src/base/abc/abcSymm.c b/src/base/abc/abcSymm.c new file mode 100644 index 00000000..8df3a837 --- /dev/null +++ b/src/base/abc/abcSymm.c @@ -0,0 +1,202 @@ +/**CFile**************************************************************** + + FileName [abcSymm.c] + + SystemName [ABC: Logic synthesis and verification system.] + + PackageName [Network and node package.] + + Synopsis [Computation of two-variable symmetries.] + + Author [Alan Mishchenko] + + Affiliation [UC Berkeley] + + Date [Ver. 1.0. Started - June 20, 2005.] + + Revision [$Id: abcSymm.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $] + +***********************************************************************/ + +#include "abc.h" + +//////////////////////////////////////////////////////////////////////// +/// DECLARATIONS /// +//////////////////////////////////////////////////////////////////////// + +static void Abc_NtkSymmetriesUsingBdds( Abc_Ntk_t * pNtk, int fNaive, int fVerbose ); +static void Ntk_NetworkSymmsBdd( DdManager * dd, Abc_Ntk_t * pNtk, int fNaive, int fVerbose ); +static void Ntk_NetworkSymmsPrint( Abc_Ntk_t * pNtk, Extra_SymmInfo_t * pSymms ); + +//////////////////////////////////////////////////////////////////////// +/// FUNCTION DEFITIONS /// +//////////////////////////////////////////////////////////////////////// + +/**Function************************************************************* + + Synopsis [The top level procedure to compute symmetries.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Abc_NtkSymmetries( Abc_Ntk_t * pNtk, int fUseBdds, int fNaive, int fVerbose ) +{ + if ( fUseBdds || fNaive ) + Abc_NtkSymmetriesUsingBdds( pNtk, fNaive, fVerbose ); + else + printf( "This option is currently not implemented.\n" ); +} + +/**Function************************************************************* + + Synopsis [Symmetry computation using BDDs (both naive and smart).] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Abc_NtkSymmetriesUsingBdds( Abc_Ntk_t * pNtk, int fNaive, int fVerbose ) +{ + DdManager * dd; + int clk, clkBdd, clkSym; + + // compute the global functions +clk = clock(); + dd = Abc_NtkGlobalBdds( pNtk, 0 ); + Cudd_AutodynDisable( dd ); + Cudd_zddVarsFromBddVars( dd, 2 ); +clkBdd = clock() - clk; + // create the collapsed network +clk = clock(); + Ntk_NetworkSymmsBdd( dd, pNtk, fNaive, fVerbose ); +clkSym = clock() - clk; + // undo the global functions + Abc_NtkFreeGlobalBdds( pNtk ); + Extra_StopManager( dd ); + pNtk->pManGlob = NULL; + +PRT( "Constructing BDDs", clkBdd ); +PRT( "Computing symms ", clkSym ); +PRT( "TOTAL ", clkBdd + clkSym ); +} + +/**Function************************************************************* + + Synopsis [Symmetry computation using BDDs (both naive and smart).] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Ntk_NetworkSymmsBdd( DdManager * dd, Abc_Ntk_t * pNtk, int fNaive, int fVerbose ) +{ + Extra_SymmInfo_t * pSymms; + Abc_Obj_t * pNode; + DdNode * bFunc; + int nSymms = 0; + int i; + + // compute symmetry info for each PO + Abc_NtkForEachCo( pNtk, pNode, i ) + { + bFunc = pNtk->vFuncsGlob->pArray[i]; + if ( Cudd_IsConstant(bFunc) ) + continue; + if ( fNaive ) + pSymms = Extra_SymmPairsComputeNaive( dd, bFunc ); + else + pSymms = Extra_SymmPairsCompute( dd, bFunc ); + nSymms += pSymms->nSymms; + if ( fVerbose ) + { + printf( "Output %6s (%d): ", Abc_ObjName(pNode), pSymms->nSymms ); + Ntk_NetworkSymmsPrint( pNtk, pSymms ); + } +//Extra_SymmPairsPrint( pSymms ); + Extra_SymmPairsDissolve( pSymms ); + } + printf( "The total number of symmetries is %d.\n", nSymms ); +} + +/**Function************************************************************* + + Synopsis [Printing symmetry groups from the symmetry data structure.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Ntk_NetworkSymmsPrint( Abc_Ntk_t * pNtk, Extra_SymmInfo_t * pSymms ) +{ + char ** pInputNames; + int * pVarTaken; + int i, k, nVars, nSize, fStart; + + // get variable names + nVars = Abc_NtkCiNum(pNtk); + pInputNames = Abc_NtkCollectCioNames( pNtk, 0 ); + + // alloc the array of marks + pVarTaken = ALLOC( int, nVars ); + memset( pVarTaken, 0, sizeof(int) * nVars ); + + // print the groups + fStart = 1; + nSize = pSymms->nVars; + for ( i = 0; i < nSize; i++ ) + { + // skip the variable already considered + if ( pVarTaken[i] ) + continue; + // find all the vars symmetric with this one + for ( k = 0; k < nSize; k++ ) + { + if ( k == i ) + continue; + if ( pSymms->pSymms[i][k] == 0 ) + continue; + // vars i and k are symmetric + assert( pVarTaken[k] == 0 ); + // there is a new symmetry pair + if ( fStart == 1 ) + { // start a new symmetry class + fStart = 0; + printf( " { %s", pInputNames[ pSymms->pVars[i] ] ); + // mark the var as taken + pVarTaken[i] = 1; + } + printf( " %s", pInputNames[ pSymms->pVars[k] ] ); + // mark the var as taken + pVarTaken[k] = 1; + } + if ( fStart == 0 ) + { + printf( " }" ); + fStart = 1; + } + } + printf( "\n" ); + + free( pInputNames ); + free( pVarTaken ); +} + + +//////////////////////////////////////////////////////////////////////// +/// END OF FILE /// +//////////////////////////////////////////////////////////////////////// + + diff --git a/src/base/abc/abcUnreach.c b/src/base/abc/abcUnreach.c index 04e5c96c..0fe3ec63 100644 --- a/src/base/abc/abcUnreach.c +++ b/src/base/abc/abcUnreach.c @@ -91,6 +91,7 @@ int Abc_NtkExtractSequentialDcs( Abc_Ntk_t * pNtk, bool fVerbose ) pNtk->pExdc = Abc_NtkConstructExdc( dd, pNtk, bUnreach ); Cudd_RecursiveDeref( dd, bUnreach ); Extra_StopManager( dd ); + pNtk->pManGlob = NULL; // make sure that everything is okay if ( fCheck && !Abc_NtkCheck( pNtk->pExdc ) ) @@ -135,13 +136,13 @@ DdNode * Abc_NtkTransitionRelation( DdManager * dd, Abc_Ntk_t * pNtk, int fVerbo Abc_NtkForEachLatch( pNtk, pNode, i ) { bVar = Cudd_bddIthVar( dd, Abc_NtkCiNum(pNtk) + i ); - bProd = Cudd_bddXnor( dd, bVar, (DdNode *)pNode->pNext ); Cudd_Ref( bProd ); - bRel = Cudd_bddAnd( dd, bTemp = bRel, bProd ); Cudd_Ref( bRel ); + bProd = Cudd_bddXnor( dd, bVar, pNtk->vFuncsGlob->pArray[i] ); Cudd_Ref( bProd ); + bRel = Cudd_bddAnd( dd, bTemp = bRel, bProd ); Cudd_Ref( bRel ); Cudd_RecursiveDeref( dd, bTemp ); Cudd_RecursiveDeref( dd, bProd ); } // free the global BDDs - Abc_NtkFreeGlobalBdds( dd, pNtk ); + Abc_NtkFreeGlobalBdds( pNtk ); // quantify the PI variables bInputs = Extra_bddComputeRangeCube( dd, 0, Abc_NtkPiNum(pNtk) ); Cudd_Ref( bInputs ); diff --git a/src/base/abc/abcUtil.c b/src/base/abc/abcUtil.c index 7d2ca107..9a2acc32 100644 --- a/src/base/abc/abcUtil.c +++ b/src/base/abc/abcUtil.c @@ -1046,6 +1046,29 @@ Vec_Int_t * Abc_NtkFanoutCounts( Abc_Ntk_t * pNtk ) return vFanNums; } +/**Function************************************************************* + + Synopsis [Collects all objects into one array.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Vec_Ptr_t * Abc_NtkCollectObjects( Abc_Ntk_t * pNtk ) +{ + Vec_Ptr_t * vNodes; + Abc_Obj_t * pNode; + int i; + vNodes = Vec_PtrAlloc( 100 ); + Abc_NtkForEachObj( pNtk, pNode, i ) + Vec_PtrPush( vNodes, pNode ); + return vNodes; +} + + //////////////////////////////////////////////////////////////////////// /// END OF FILE /// //////////////////////////////////////////////////////////////////////// diff --git a/src/base/abc/module.make b/src/base/abc/module.make index d9bed264..d3d4091b 100644 --- a/src/base/abc/module.make +++ b/src/base/abc/module.make @@ -32,6 +32,7 @@ SRC += src/base/abc/abc.c \ src/base/abc/abcSop.c \ src/base/abc/abcStrash.c \ src/base/abc/abcSweep.c \ + src/base/abc/abcSymm.c \ src/base/abc/abcTiming.c \ src/base/abc/abcUnreach.c \ src/base/abc/abcUtil.c \ diff --git a/src/base/io/io.c b/src/base/io/io.c index 9ffbc3cf..89703214 100644 --- a/src/base/io/io.c +++ b/src/base/io/io.c @@ -29,12 +29,16 @@ static int IoCommandRead ( Abc_Frame_t * pAbc, int argc, char **argv ); static int IoCommandReadBlif ( Abc_Frame_t * pAbc, int argc, char **argv ); static int IoCommandReadBench ( Abc_Frame_t * pAbc, int argc, char **argv ); static int IoCommandReadEdif ( Abc_Frame_t * pAbc, int argc, char **argv ); +static int IoCommandReadEqn ( Abc_Frame_t * pAbc, int argc, char **argv ); static int IoCommandReadVerilog ( Abc_Frame_t * pAbc, int argc, char **argv ); static int IoCommandReadPla ( Abc_Frame_t * pAbc, int argc, char **argv ); static int IoCommandWriteBlif ( Abc_Frame_t * pAbc, int argc, char **argv ); static int IoCommandWriteBench ( Abc_Frame_t * pAbc, int argc, char **argv ); static int IoCommandWriteCnf ( Abc_Frame_t * pAbc, int argc, char **argv ); +static int IoCommandWriteDot ( Abc_Frame_t * pAbc, int argc, char **argv ); +static int IoCommandWriteEqn ( Abc_Frame_t * pAbc, int argc, char **argv ); +static int IoCommandWriteGml ( Abc_Frame_t * pAbc, int argc, char **argv ); static int IoCommandWritePla ( Abc_Frame_t * pAbc, int argc, char **argv ); //////////////////////////////////////////////////////////////////////// @@ -58,12 +62,16 @@ void Io_Init( Abc_Frame_t * pAbc ) Cmd_CommandAdd( pAbc, "I/O", "read_blif", IoCommandReadBlif, 1 ); Cmd_CommandAdd( pAbc, "I/O", "read_bench", IoCommandReadBench, 1 ); Cmd_CommandAdd( pAbc, "I/O", "read_edif", IoCommandReadEdif, 1 ); + Cmd_CommandAdd( pAbc, "I/O", "read_eqn", IoCommandReadEqn, 1 ); Cmd_CommandAdd( pAbc, "I/O", "read_verilog", IoCommandReadVerilog, 1 ); Cmd_CommandAdd( pAbc, "I/O", "read_pla", IoCommandReadPla, 1 ); Cmd_CommandAdd( pAbc, "I/O", "write_blif", IoCommandWriteBlif, 0 ); Cmd_CommandAdd( pAbc, "I/O", "write_bench", IoCommandWriteBench, 0 ); Cmd_CommandAdd( pAbc, "I/O", "write_cnf", IoCommandWriteCnf, 0 ); + Cmd_CommandAdd( pAbc, "I/O", "write_dot", IoCommandWriteDot, 0 ); + Cmd_CommandAdd( pAbc, "I/O", "write_eqn", IoCommandWriteEqn, 0 ); + Cmd_CommandAdd( pAbc, "I/O", "write_gml", IoCommandWriteGml, 0 ); Cmd_CommandAdd( pAbc, "I/O", "write_pla", IoCommandWritePla, 0 ); } @@ -127,7 +135,7 @@ int IoCommandRead( Abc_Frame_t * pAbc, int argc, char ** argv ) if ( (pFile = fopen( FileName, "r" )) == NULL ) { fprintf( pAbc->Err, "Cannot open input file \"%s\". ", FileName ); - if ( FileName = Extra_FileGetSimilarName( FileName, ".mv", ".blif", ".pla", ".mvpla", NULL ) ) + if ( FileName = Extra_FileGetSimilarName( FileName, ".mv", ".blif", ".pla", ".eqn", ".bench" ) ) fprintf( pAbc->Err, "Did you mean \"%s\"?", FileName ); fprintf( pAbc->Err, "\n" ); return 1; @@ -199,7 +207,7 @@ int IoCommandReadBlif( Abc_Frame_t * pAbc, int argc, char ** argv ) if ( (pFile = fopen( FileName, "r" )) == NULL ) { fprintf( pAbc->Err, "Cannot open input file \"%s\". ", FileName ); - if ( FileName = Extra_FileGetSimilarName( FileName, ".mv", ".blif", ".pla", ".mvpla", NULL ) ) + if ( FileName = Extra_FileGetSimilarName( FileName, ".mv", ".blif", ".pla", ".eqn", ".bench" ) ) fprintf( pAbc->Err, "Did you mean \"%s\"?", FileName ); fprintf( pAbc->Err, "\n" ); return 1; @@ -280,7 +288,7 @@ int IoCommandReadBench( Abc_Frame_t * pAbc, int argc, char ** argv ) if ( (pFile = fopen( FileName, "r" )) == NULL ) { fprintf( pAbc->Err, "Cannot open input file \"%s\". ", FileName ); - if ( FileName = Extra_FileGetSimilarName( FileName, ".mv", ".blif", ".pla", ".mvpla", NULL ) ) + if ( FileName = Extra_FileGetSimilarName( FileName, ".mv", ".blif", ".pla", ".eqn", ".bench" ) ) fprintf( pAbc->Err, "Did you mean \"%s\"?", FileName ); fprintf( pAbc->Err, "\n" ); return 1; @@ -360,7 +368,7 @@ int IoCommandReadEdif( Abc_Frame_t * pAbc, int argc, char ** argv ) if ( (pFile = fopen( FileName, "r" )) == NULL ) { fprintf( pAbc->Err, "Cannot open input file \"%s\". ", FileName ); - if ( FileName = Extra_FileGetSimilarName( FileName, ".mv", ".blif", ".pla", ".mvpla", NULL ) ) + if ( FileName = Extra_FileGetSimilarName( FileName, ".mv", ".blif", ".pla", ".eqn", ".bench" ) ) fprintf( pAbc->Err, "Did you mean \"%s\"?", FileName ); fprintf( pAbc->Err, "\n" ); return 1; @@ -395,6 +403,86 @@ usage: return 1; } +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int IoCommandReadEqn( Abc_Frame_t * pAbc, int argc, char ** argv ) +{ + Abc_Ntk_t * pNtk, * pTemp; + char * FileName; + FILE * pFile; + int fCheck; + int c; + + fCheck = 1; + util_getopt_reset(); + while ( ( c = util_getopt( argc, argv, "ch" ) ) != EOF ) + { + switch ( c ) + { + case 'c': + fCheck ^= 1; + break; + case 'h': + goto usage; + default: + goto usage; + } + } + + if ( argc != util_optind + 1 ) + { + goto usage; + } + + // get the input file name + FileName = argv[util_optind]; + if ( (pFile = fopen( FileName, "r" )) == NULL ) + { + fprintf( pAbc->Err, "Cannot open input file \"%s\". ", FileName ); + if ( FileName = Extra_FileGetSimilarName( FileName, ".mv", ".blif", ".pla", ".eqn", ".bench" ) ) + fprintf( pAbc->Err, "Did you mean \"%s\"?", FileName ); + fprintf( pAbc->Err, "\n" ); + return 1; + } + fclose( pFile ); + + // set the new network + pNtk = Io_ReadEqn( FileName, fCheck ); + if ( pNtk == NULL ) + { + fprintf( pAbc->Err, "Reading network from the equation file has failed.\n" ); + return 1; + } + + pNtk = Abc_NtkNetlistToLogic( pTemp = pNtk ); + Abc_NtkDelete( pTemp ); + if ( pNtk == NULL ) + { + fprintf( pAbc->Err, "Converting to logic network after reading has failed.\n" ); + return 1; + } + // replace the current network + Abc_FrameReplaceCurrentNetwork( pAbc, pNtk ); + return 0; + +usage: + fprintf( pAbc->Err, "usage: read_eqn [-ch] \n" ); + fprintf( pAbc->Err, "\t read the network in equation format\n" ); + fprintf( pAbc->Err, "\t-c : toggle network check after reading [default = %s]\n", fCheck? "yes":"no" ); + fprintf( pAbc->Err, "\t-h : prints the command summary\n" ); + fprintf( pAbc->Err, "\tfile : the name of a file to read\n" ); + return 1; +} + /**Function************************************************************* Synopsis [] @@ -440,7 +528,7 @@ int IoCommandReadVerilog( Abc_Frame_t * pAbc, int argc, char ** argv ) if ( (pFile = fopen( FileName, "r" )) == NULL ) { fprintf( pAbc->Err, "Cannot open input file \"%s\". ", FileName ); - if ( FileName = Extra_FileGetSimilarName( FileName, ".mv", ".blif", ".pla", ".mvpla", NULL ) ) + if ( FileName = Extra_FileGetSimilarName( FileName, ".mv", ".blif", ".pla", ".eqn", ".bench" ) ) fprintf( pAbc->Err, "Did you mean \"%s\"?", FileName ); fprintf( pAbc->Err, "\n" ); return 1; @@ -451,7 +539,7 @@ int IoCommandReadVerilog( Abc_Frame_t * pAbc, int argc, char ** argv ) pNtk = Io_ReadVerilog( FileName, fCheck ); if ( pNtk == NULL ) { - fprintf( pAbc->Err, "Reading network from Verilog file has failed.\n" ); + fprintf( pAbc->Err, "Reading network from the verilog file has failed.\n" ); return 1; } @@ -520,7 +608,7 @@ int IoCommandReadPla( Abc_Frame_t * pAbc, int argc, char ** argv ) if ( (pFile = fopen( FileName, "r" )) == NULL ) { fprintf( pAbc->Err, "Cannot open input file \"%s\". ", FileName ); - if ( FileName = Extra_FileGetSimilarName( FileName, ".mv", ".blif", ".pla", ".mvpla", NULL ) ) + if ( FileName = Extra_FileGetSimilarName( FileName, ".mv", ".blif", ".pla", ".eqn", ".bench" ) ) fprintf( pAbc->Err, "Did you mean \"%s\"?", FileName ); fprintf( pAbc->Err, "\n" ); return 1; @@ -753,6 +841,199 @@ usage: return 1; } +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int IoCommandWriteDot( Abc_Frame_t * pAbc, int argc, char **argv ) +{ + char * FileName; + Vec_Ptr_t * vNodes; + int c; + + util_getopt_reset(); + while ( ( c = util_getopt( argc, argv, "h" ) ) != EOF ) + { + switch ( c ) + { + case 'h': + goto usage; + default: + goto usage; + } + } + + if ( pAbc->pNtkCur == NULL ) + { + fprintf( pAbc->Out, "Empty network.\n" ); + return 0; + } + + if ( !Abc_NtkIsStrash(pAbc->pNtkCur) ) + { + fprintf( stdout, "IoCommandWriteDot(): Currently can only process logic networks with BDDs.\n" ); + return 0; + } + + if ( argc != util_optind + 1 ) + { + goto usage; + } + + // get the input file name + FileName = argv[util_optind]; + // write the file + vNodes = Abc_NtkCollectObjects( pAbc->pNtkCur ); + Io_WriteDot( pAbc->pNtkCur, vNodes, NULL, FileName ); + Vec_PtrFree( vNodes ); + return 0; + +usage: + fprintf( pAbc->Err, "usage: write_dot [-h] \n" ); + fprintf( pAbc->Err, "\t write the AIG into a DOT file\n" ); + fprintf( pAbc->Err, "\t-h : print the help massage\n" ); + fprintf( pAbc->Err, "\tfile : the name of the file to write\n" ); + return 1; +} + +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int IoCommandWriteEqn( Abc_Frame_t * pAbc, int argc, char **argv ) +{ + Abc_Ntk_t * pNtk, * pNtkTemp; + char * FileName; + int c; + + util_getopt_reset(); + while ( ( c = util_getopt( argc, argv, "h" ) ) != EOF ) + { + switch ( c ) + { + case 'h': + goto usage; + default: + goto usage; + } + } + + pNtk = pAbc->pNtkCur; + if ( pNtk == NULL ) + { + fprintf( pAbc->Out, "Empty network.\n" ); + return 0; + } + + if ( argc != util_optind + 1 ) + { + goto usage; + } + + if ( !Abc_NtkIsLogic(pNtk) && !Abc_NtkIsStrash(pNtk) ) + { + fprintf( stdout, "IoCommandWriteGml(): Currently can only process logic networks with BDDs.\n" ); + return 0; + } + + // get the input file name + FileName = argv[util_optind]; + // write the file + // get rid of complemented covers if present + if ( Abc_NtkIsSopLogic(pNtk) ) + Abc_NtkLogicMakeDirectSops(pNtk); + // derive the netlist + pNtkTemp = Abc_NtkLogicToNetlist(pNtk); + if ( pNtkTemp == NULL ) + { + fprintf( pAbc->Out, "Writing BENCH has failed.\n" ); + return 0; + } + Io_WriteEqn( pNtkTemp, FileName ); + Abc_NtkDelete( pNtkTemp ); + return 0; + +usage: + fprintf( pAbc->Err, "usage: write_eqn [-h] \n" ); + fprintf( pAbc->Err, "\t write the current network in the equation format\n" ); + fprintf( pAbc->Err, "\t-h : print the help massage\n" ); + fprintf( pAbc->Err, "\tfile : the name of the file to write\n" ); + return 1; +} + +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int IoCommandWriteGml( Abc_Frame_t * pAbc, int argc, char **argv ) +{ + char * FileName; + int c; + + util_getopt_reset(); + while ( ( c = util_getopt( argc, argv, "h" ) ) != EOF ) + { + switch ( c ) + { + case 'h': + goto usage; + default: + goto usage; + } + } + + if ( pAbc->pNtkCur == NULL ) + { + fprintf( pAbc->Out, "Empty network.\n" ); + return 0; + } + + if ( !Abc_NtkIsLogic(pAbc->pNtkCur) && !Abc_NtkIsStrash(pAbc->pNtkCur) ) + { + fprintf( stdout, "IoCommandWriteGml(): Currently can only process logic networks with BDDs.\n" ); + return 0; + } + + if ( argc != util_optind + 1 ) + { + goto usage; + } + + // get the input file name + FileName = argv[util_optind]; + // write the file + Io_WriteGml( pAbc->pNtkCur, FileName ); + return 0; + +usage: + fprintf( pAbc->Err, "usage: write_gml [-h] \n" ); + fprintf( pAbc->Err, "\t write network using graph representation formal GML\n" ); + fprintf( pAbc->Err, "\t-h : print the help massage\n" ); + fprintf( pAbc->Err, "\tfile : the name of the file to write\n" ); + return 1; +} + /**Function************************************************************* Synopsis [] diff --git a/src/base/io/io.h b/src/base/io/io.h index d45b7b1b..6bf3a85c 100644 --- a/src/base/io/io.h +++ b/src/base/io/io.h @@ -53,6 +53,8 @@ extern Abc_Ntk_t * Io_ReadBlif( char * pFileName, int fCheck ); extern Abc_Ntk_t * Io_ReadBench( char * pFileName, int fCheck ); /*=== abcReadEdif.c ==========================================================*/ extern Abc_Ntk_t * Io_ReadEdif( char * pFileName, int fCheck ); +/*=== abcReadEqn.c ==========================================================*/ +extern Abc_Ntk_t * Io_ReadEqn( char * pFileName, int fCheck ); /*=== abcReadVerilog.c ==========================================================*/ extern Abc_Ntk_t * Io_ReadVerilog( char * pFileName, int fCheck ); /*=== abcReadPla.c ==========================================================*/ @@ -73,6 +75,12 @@ extern void Io_WriteTimingInfo( FILE * pFile, Abc_Ntk_t * pNtk ); extern int Io_WriteBench( Abc_Ntk_t * pNtk, char * FileName ); /*=== abcWriteCnf.c ==========================================================*/ extern int Io_WriteCnf( Abc_Ntk_t * pNtk, char * FileName ); +/*=== abcWriteDot.c ==========================================================*/ +extern void Io_WriteDot( Abc_Ntk_t * pNtk, Vec_Ptr_t * vNodes, Vec_Ptr_t * vNodesShow, char * pFileName ); +/*=== abcWriteEqn.c ==========================================================*/ +extern void Io_WriteEqn( Abc_Ntk_t * pNtk, char * pFileName ); +/*=== abcWriteGml.c ==========================================================*/ +extern void Io_WriteGml( Abc_Ntk_t * pNtk, char * pFileName ); /*=== abcWritePla.c ==========================================================*/ extern int Io_WritePla( Abc_Ntk_t * pNtk, char * FileName ); diff --git a/src/base/io/ioRead.c b/src/base/io/ioRead.c index 75c87a80..acf4deda 100644 --- a/src/base/io/ioRead.c +++ b/src/base/io/ioRead.c @@ -53,6 +53,8 @@ Abc_Ntk_t * Io_Read( char * pFileName, int fCheck ) pNtk = Io_ReadEdif( pFileName, fCheck ); else if ( Extra_FileNameCheckExtension( pFileName, "pla" ) ) pNtk = Io_ReadPla( pFileName, fCheck ); + else if ( Extra_FileNameCheckExtension( pFileName, "eqn" ) ) + pNtk = Io_ReadEqn( pFileName, fCheck ); else { fprintf( stderr, "Unknown file format\n" ); diff --git a/src/base/io/ioReadEqn.c b/src/base/io/ioReadEqn.c new file mode 100644 index 00000000..54890729 --- /dev/null +++ b/src/base/io/ioReadEqn.c @@ -0,0 +1,254 @@ +/**CFile**************************************************************** + + FileName [ioReadEqn.c] + + SystemName [ABC: Logic synthesis and verification system.] + + PackageName [Command processing package.] + + Synopsis [Procedures to read equation format files.] + + Author [Alan Mishchenko] + + Affiliation [UC Berkeley] + + Date [Ver. 1.0. Started - June 20, 2005.] + + Revision [$Id: ioReadEqn.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $] + +***********************************************************************/ + +#include "io.h" + +//////////////////////////////////////////////////////////////////////// +/// DECLARATIONS /// +//////////////////////////////////////////////////////////////////////// + +static Abc_Ntk_t * Io_ReadEqnNetwork( Extra_FileReader_t * p ); +static void Io_ReadEqnStrCompact( char * pStr ); +static int Io_ReadEqnStrFind( Vec_Ptr_t * vTokens, char * pName ); +static void Io_ReadEqnStrCutAt( char * pStr, char * pStop, int fUniqueOnly, Vec_Ptr_t * vTokens ); + +//////////////////////////////////////////////////////////////////////// +/// FUNCTION DEFITIONS /// +//////////////////////////////////////////////////////////////////////// + +/**Function************************************************************* + + Synopsis [Reads the network from a BENCH file.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Abc_Ntk_t * Io_ReadEqn( char * pFileName, int fCheck ) +{ + Extra_FileReader_t * p; + Abc_Ntk_t * pNtk; + + // start the file + p = Extra_FileReaderAlloc( pFileName, "#", ";", "=" ); + if ( p == NULL ) + return NULL; + + // read the network + pNtk = Io_ReadEqnNetwork( p ); + Extra_FileReaderFree( p ); + if ( pNtk == NULL ) + return NULL; + + // make sure that everything is okay with the network structure + if ( fCheck && !Abc_NtkCheck( pNtk ) ) + { + printf( "Io_ReadEqn: The network check has failed.\n" ); + Abc_NtkDelete( pNtk ); + return NULL; + } + return pNtk; +} + +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Abc_Ntk_t * Io_ReadEqnNetwork( Extra_FileReader_t * p ) +{ + ProgressBar * pProgress; + Vec_Ptr_t * vTokens; + Vec_Ptr_t * vCubes, * vLits, * vVars; + Abc_Ntk_t * pNtk; + Abc_Obj_t * pNode; + char * pCubesCopy, * pSopCube, * pVarName; + int iLine, iNum, i, k; + + // allocate the empty network + pNtk = Abc_NtkStartRead( Extra_FileReaderGetFileName(p) ); + + // go through the lines of the file + vCubes = Vec_PtrAlloc( 100 ); + vVars = Vec_PtrAlloc( 100 ); + vLits = Vec_PtrAlloc( 100 ); + pProgress = Extra_ProgressBarStart( stdout, Extra_FileReaderGetFileSize(p) ); + for ( iLine = 0; vTokens = Extra_FileReaderGetTokens(p); iLine++ ) + { + Extra_ProgressBarUpdate( pProgress, Extra_FileReaderGetCurPosition(p), NULL ); + + // check if the first token contains anything + Io_ReadEqnStrCompact( vTokens->pArray[0] ); + if ( strlen(vTokens->pArray[0]) == 0 ) + break; + + // if the number of tokens is different from two, error + if ( vTokens->nSize != 2 ) + { + printf( "%s: Wrong input file format.\n", Extra_FileReaderGetFileName(p) ); + Abc_NtkDelete( pNtk ); + return NULL; + } + + // get the type of the line + if ( strncmp( vTokens->pArray[0], "INORDER", 7 ) == 0 ) + { + Io_ReadEqnStrCutAt( vTokens->pArray[1], " \n\r\t", 0, vVars ); + Vec_PtrForEachEntry( vVars, pVarName, i ) + Io_ReadCreatePi( pNtk, pVarName ); + } + else if ( strncmp( vTokens->pArray[0], "OUTORDER", 8 ) == 0 ) + { + Io_ReadEqnStrCutAt( vTokens->pArray[1], " \n\r\t", 0, vVars ); + Vec_PtrForEachEntry( vVars, pVarName, i ) + Io_ReadCreatePo( pNtk, pVarName ); + } + else + { + // remove spaces + pCubesCopy = vTokens->pArray[1]; + Io_ReadEqnStrCompact( pCubesCopy ); + // consider the case of the constant node + if ( (pCubesCopy[0] == '0' || pCubesCopy[0] == '1') && pCubesCopy[1] == 0 ) + { + pNode = Io_ReadCreateNode( pNtk, vTokens->pArray[0], NULL, 0 ); + if ( pCubesCopy[0] == '0' ) + pNode->pData = Abc_SopCreateConst0( pNtk->pManFunc ); + else + pNode->pData = Abc_SopCreateConst1( pNtk->pManFunc ); + continue; + } + // determine unique variables + pCubesCopy = util_strsav( pCubesCopy ); + // find the names of the fanins of this node + Io_ReadEqnStrCutAt( pCubesCopy, "!*+", 1, vVars ); + // create the node + pNode = Io_ReadCreateNode( pNtk, vTokens->pArray[0], (char **)vVars->pArray, vVars->nSize ); + // split the string into cubes + Io_ReadEqnStrCutAt( vTokens->pArray[1], "+", 0, vCubes ); + // start the sop + pNode->pData = Abc_SopStart( pNtk->pManFunc, vCubes->nSize, vVars->nSize ); + // read the cubes + i = 0; + Abc_SopForEachCube( pNode->pData, vVars->nSize, pSopCube ) + { + // split this cube into lits + Io_ReadEqnStrCutAt( vCubes->pArray[i], "*", 0, vLits ); + // read the literals + Vec_PtrForEachEntry( vLits, pVarName, k ) + { + iNum = Io_ReadEqnStrFind( vVars, pVarName + (pVarName[0] == '!') ); + assert( iNum >= 0 ); + pSopCube[iNum] = '1' - (pVarName[0] == '!'); + } + i++; + } + assert( i == vCubes->nSize ); + // remove the cubes + free( pCubesCopy ); + } + } + Extra_ProgressBarStop( pProgress ); + Vec_PtrFree( vCubes ); + Vec_PtrFree( vLits ); + Vec_PtrFree( vVars ); + Abc_NtkFinalizeRead( pNtk ); + return pNtk; +} + + + +/**Function************************************************************* + + Synopsis [Compacts the string by throwing away space-like chars.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Io_ReadEqnStrCompact( char * pStr ) +{ + char * pCur, * pNew; + for ( pNew = pCur = pStr; *pCur; pCur++ ) + if ( !(*pCur == ' ' || *pCur == '\n' || *pCur == '\r' || *pCur == '\t') ) + *pNew++ = *pCur; + *pNew = 0; +} + +/**Function************************************************************* + + Synopsis [Determines unique variables in the string.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Io_ReadEqnStrFind( Vec_Ptr_t * vTokens, char * pName ) +{ + char * pToken; + int i; + Vec_PtrForEachEntry( vTokens, pToken, i ) + if ( strcmp( pToken, pName ) == 0 ) + return i; + return -1; +} + +/**Function************************************************************* + + Synopsis [Cuts the string into pieces using stop chars.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Io_ReadEqnStrCutAt( char * pStr, char * pStop, int fUniqueOnly, Vec_Ptr_t * vTokens ) +{ + char * pToken; + Vec_PtrClear( vTokens ); + for ( pToken = strtok( pStr, pStop ); pToken; pToken = strtok( NULL, pStop ) ) + if ( !fUniqueOnly || Io_ReadEqnStrFind( vTokens, pToken ) == -1 ) + Vec_PtrPush( vTokens, pToken ); +} + + +//////////////////////////////////////////////////////////////////////// +/// END OF FILE /// +//////////////////////////////////////////////////////////////////////// + + + diff --git a/src/base/io/ioWriteBlif.c b/src/base/io/ioWriteBlif.c index 5135105f..7d6815b9 100644 --- a/src/base/io/ioWriteBlif.c +++ b/src/base/io/ioWriteBlif.c @@ -107,10 +107,7 @@ void Io_WriteBlif( Abc_Ntk_t * pNtk, char * FileName, int fWriteLatches ) Synopsis [Write one network.] - Description [Writes a network composed of PIs, POs, internal nodes, - and latches. The following rules are used to print the names of - internal nodes: - ] + Description [] SideEffects [] diff --git a/src/base/io/ioWriteCnf.c b/src/base/io/ioWriteCnf.c index bb216bb6..09824f38 100644 --- a/src/base/io/ioWriteCnf.c +++ b/src/base/io/ioWriteCnf.c @@ -6,7 +6,7 @@ PackageName [Command processing package.] - Synopsis [Procedures to CNF of the miter cone.] + Synopsis [Procedures to output CNF of the miter cone.] Author [Alan Mishchenko] @@ -24,8 +24,6 @@ /// DECLARATIONS /// //////////////////////////////////////////////////////////////////////// -static void Io_WriteCnfInt( FILE * pFile, Abc_Ntk_t * pNtk ); - //////////////////////////////////////////////////////////////////////// /// FUNCTION DEFITIONS /// //////////////////////////////////////////////////////////////////////// diff --git a/src/base/io/ioWriteDot.c b/src/base/io/ioWriteDot.c new file mode 100644 index 00000000..7d88e52d --- /dev/null +++ b/src/base/io/ioWriteDot.c @@ -0,0 +1,322 @@ +/**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, * pTemp, * pPrev; + 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 stream + 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 = 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 [label = \"%s\"", pNode->Id, 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 [label = \"%s\"", pNode->Id, 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 [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 + if ( Abc_ObjFanin0(pNode)->fMarkC ) + { + fprintf( pFile, "Node%d", pNode->Id ); + fprintf( pFile, " -> " ); + fprintf( pFile, "Node%d", Abc_ObjFaninId0(pNode) ); + 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 + if ( Abc_ObjFanin1(pNode)->fMarkC ) + { + 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, ";\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/io/ioWriteEqn.c b/src/base/io/ioWriteEqn.c new file mode 100644 index 00000000..6c2893b5 --- /dev/null +++ b/src/base/io/ioWriteEqn.c @@ -0,0 +1,261 @@ +/**CFile**************************************************************** + + FileName [ioWriteEqn.c] + + SystemName [ABC: Logic synthesis and verification system.] + + PackageName [Command processing package.] + + Synopsis [Procedures to write equation representation of the network.] + + Author [Alan Mishchenko] + + Affiliation [UC Berkeley] + + Date [Ver. 1.0. Started - June 20, 2005.] + + Revision [$Id: ioWriteEqn.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $] + +***********************************************************************/ + +#include "io.h" + +//////////////////////////////////////////////////////////////////////// +/// DECLARATIONS /// +//////////////////////////////////////////////////////////////////////// + +static void Io_NtkWriteEqnOne( FILE * pFile, Abc_Ntk_t * pNtk ); +static void Io_NtkWriteEqnPis( FILE * pFile, Abc_Ntk_t * pNtk ); +static void Io_NtkWriteEqnPos( FILE * pFile, Abc_Ntk_t * pNtk ); +static void Io_NtkWriteEqnNode( FILE * pFile, Abc_Obj_t * pNode ); + +//////////////////////////////////////////////////////////////////////// +/// FUNCTION DEFITIONS /// +//////////////////////////////////////////////////////////////////////// + +/**Function************************************************************* + + Synopsis [Writes the logic network in the equation format.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Io_WriteEqn( Abc_Ntk_t * pNtk, char * pFileName ) +{ + FILE * pFile; + + assert( Abc_NtkIsSopNetlist(pNtk) ); + if ( Abc_NtkLatchNum(pNtk) > 0 ) + printf( "Warning: only combinational portion is being written.\n" ); + + // start the output stream + pFile = fopen( pFileName, "w" ); + if ( pFile == NULL ) + { + fprintf( stdout, "Io_WriteEqn(): Cannot open the output file \"%s\".\n", pFileName ); + return; + } + fprintf( pFile, "# Equations for \"%s\" written by ABC on %s\n", pNtk->pName, Extra_TimeStamp() ); + + // write the equations for the network + Io_NtkWriteEqnOne( pFile, pNtk ); + fprintf( pFile, "\n" ); + fclose( pFile ); +} + +/**Function************************************************************* + + Synopsis [Write one network.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Io_NtkWriteEqnOne( FILE * pFile, Abc_Ntk_t * pNtk ) +{ + ProgressBar * pProgress; + Abc_Obj_t * pNode; + int i; + + // write the PIs + fprintf( pFile, "INORDER =" ); + Io_NtkWriteEqnPis( pFile, pNtk ); + fprintf( pFile, ";\n" ); + + // write the POs + fprintf( pFile, "OUTORDER =" ); + Io_NtkWriteEqnPos( pFile, pNtk ); + fprintf( pFile, ";\n" ); + + // write each internal node + pProgress = Extra_ProgressBarStart( stdout, Abc_NtkObjNumMax(pNtk) ); + Abc_NtkForEachNode( pNtk, pNode, i ) + { + Extra_ProgressBarUpdate( pProgress, i, NULL ); + Io_NtkWriteEqnNode( pFile, pNode ); + } + Extra_ProgressBarStop( pProgress ); +} + + +/**Function************************************************************* + + Synopsis [Writes the primary input list.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Io_NtkWriteEqnPis( FILE * pFile, Abc_Ntk_t * pNtk ) +{ + Abc_Obj_t * pTerm, * pNet; + int LineLength; + int AddedLength; + int NameCounter; + int i; + + LineLength = 9; + NameCounter = 0; + + Abc_NtkForEachCi( pNtk, pTerm, i ) + { + pNet = Abc_ObjFanout0(pTerm); + // get the line length after this name is written + AddedLength = strlen(Abc_ObjName(pNet)) + 1; + if ( NameCounter && LineLength + AddedLength + 3 > IO_WRITE_LINE_LENGTH ) + { // write the line extender + fprintf( pFile, " \n" ); + // reset the line length + LineLength = 0; + NameCounter = 0; + } + fprintf( pFile, " %s", Abc_ObjName(pNet) ); + LineLength += AddedLength; + NameCounter++; + } +} + +/**Function************************************************************* + + Synopsis [Writes the primary input list.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Io_NtkWriteEqnPos( FILE * pFile, Abc_Ntk_t * pNtk ) +{ + Abc_Obj_t * pTerm, * pNet; + int LineLength; + int AddedLength; + int NameCounter; + int i; + + LineLength = 10; + NameCounter = 0; + + Abc_NtkForEachCo( pNtk, pTerm, i ) + { + pNet = Abc_ObjFanin0(pTerm); + // get the line length after this name is written + AddedLength = strlen(Abc_ObjName(pNet)) + 1; + if ( NameCounter && LineLength + AddedLength + 3 > IO_WRITE_LINE_LENGTH ) + { // write the line extender + fprintf( pFile, " \n" ); + // reset the line length + LineLength = 0; + NameCounter = 0; + } + fprintf( pFile, " %s", Abc_ObjName(pNet) ); + LineLength += AddedLength; + NameCounter++; + } +} + +/**Function************************************************************* + + Synopsis [Write the node into a file.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Io_NtkWriteEqnNode( FILE * pFile, Abc_Obj_t * pNode ) +{ + Abc_Obj_t * pNet; + int LineLength; + int AddedLength; + int NameCounter; + char * pCube; + int Value, fFirstLit, i; + + fprintf( pFile, "%s = ", Abc_ObjName(pNode) ); + + if ( Abc_SopIsConst0(pNode->pData) ) + { + fprintf( pFile, "0;\n" ); + return; + } + if ( Abc_SopIsConst1(pNode->pData) ) + { + fprintf( pFile, "1;\n" ); + return; + } + + NameCounter = 0; + LineLength = strlen(Abc_ObjName(pNode)) + 3; + Abc_SopForEachCube( pNode->pData, Abc_ObjFaninNum(pNode), pCube ) + { + if ( pCube != pNode->pData ) + { + fprintf( pFile, " + " ); + LineLength += 3; + } + + // add the cube + fFirstLit = 1; + Abc_CubeForEachVar( pCube, Value, i ) + { + if ( Value == '-' ) + continue; + pNet = Abc_ObjFanin( pNode, i ); + // get the line length after this name is written + AddedLength = !fFirstLit + (Value == '0') + strlen(Abc_ObjName(pNet)); + if ( NameCounter && LineLength + AddedLength + 6 > IO_WRITE_LINE_LENGTH ) + { // write the line extender + fprintf( pFile, " \n " ); + // reset the line length + LineLength = 0; + NameCounter = 0; + } + fprintf( pFile, "%s%s%s", (fFirstLit? "": "*"), ((Value == '0')? "!":""), Abc_ObjName(pNet) ); + LineLength += AddedLength; + NameCounter++; + fFirstLit = 0; + } + } + fprintf( pFile, ";\n" ); +} + + +//////////////////////////////////////////////////////////////////////// +/// END OF FILE /// +//////////////////////////////////////////////////////////////////////// + + diff --git a/src/base/io/ioWriteGml.c b/src/base/io/ioWriteGml.c new file mode 100644 index 00000000..ab9f1143 --- /dev/null +++ b/src/base/io/ioWriteGml.c @@ -0,0 +1,116 @@ +/**CFile**************************************************************** + + FileName [ioWriteGml.c] + + SystemName [ABC: Logic synthesis and verification system.] + + PackageName [Command processing package.] + + Synopsis [Procedures to write the graph structure of AIG in GML.] + + Author [Alan Mishchenko] + + Affiliation [UC Berkeley] + + Date [Ver. 1.0. Started - June 20, 2005.] + + Revision [$Id: ioWriteGml.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 GML.] + + Description [Useful for graph visualization using tools such as yEd: + http://www.yworks.com/] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Io_WriteGml( Abc_Ntk_t * pNtk, char * pFileName ) +{ + FILE * pFile; + Abc_Obj_t * pObj, * pFanin; + int i, k; + + assert( Abc_NtkIsStrash(pNtk) || Abc_NtkIsLogic(pNtk) ); + + // start the output stream + pFile = fopen( pFileName, "w" ); + if ( pFile == NULL ) + { + fprintf( stdout, "Io_WriteGml(): Cannot open the output file \"%s\".\n", pFileName ); + return; + } + fprintf( pFile, "# GML for \"%s\" written by ABC on %s\n", pNtk->pName, Extra_TimeStamp() ); + fprintf( pFile, "graph [\n" ); + + // output the POs + fprintf( pFile, "\n" ); + Abc_NtkForEachPo( pNtk, pObj, i ) + { + fprintf( pFile, " node [ id %5d label \"%s\"\n", pObj->Id, Abc_ObjName(pObj) ); + fprintf( pFile, " graphics [ type \"triangle\" fill \"#00FFFF\" ]\n" ); // blue + fprintf( pFile, " ]\n" ); + } + // output the PIs + fprintf( pFile, "\n" ); + Abc_NtkForEachPi( pNtk, pObj, i ) + { + fprintf( pFile, " node [ id %5d label \"%s\"\n", pObj->Id, Abc_ObjName(pObj) ); + fprintf( pFile, " graphics [ type \"triangle\" fill \"#00FF00\" ]\n" ); // green + fprintf( pFile, " ]\n" ); + } + // output the latches + fprintf( pFile, "\n" ); + Abc_NtkForEachLatch( pNtk, pObj, i ) + { + fprintf( pFile, " node [ id %5d label \"%s\"\n", pObj->Id, Abc_ObjName(pObj) ); + fprintf( pFile, " graphics [ type \"rectangle\" fill \"#FF0000\" ]\n" ); // red + fprintf( pFile, " ]\n" ); + } + // output the nodes + fprintf( pFile, "\n" ); + Abc_NtkForEachNode( pNtk, pObj, i ) + { + fprintf( pFile, " node [ id %5d label \"%s\"\n", pObj->Id, Abc_ObjName(pObj) ); + fprintf( pFile, " graphics [ type \"ellipse\" fill \"#CCCCFF\" ]\n" ); // grey + fprintf( pFile, " ]\n" ); + } + + // output the edges + fprintf( pFile, "\n" ); + Abc_NtkForEachObj( pNtk, pObj, i ) + { + Abc_ObjForEachFanin( pObj, pFanin, k ) + { + fprintf( pFile, " edge [ source %5d target %5d\n", pObj->Id, pFanin->Id ); + fprintf( pFile, " graphics [ type \"line\" arrow \"first\" ]\n" ); + fprintf( pFile, " ]\n" ); + } + } + + fprintf( pFile, "]\n" ); + fprintf( pFile, "\n" ); + fclose( pFile ); +} + + +//////////////////////////////////////////////////////////////////////// +/// END OF FILE /// +//////////////////////////////////////////////////////////////////////// + + diff --git a/src/base/io/module.make b/src/base/io/module.make index cb39c481..34582473 100644 --- a/src/base/io/module.make +++ b/src/base/io/module.make @@ -3,10 +3,14 @@ SRC += src/base/io/io.c \ src/base/io/ioReadBench.c \ src/base/io/ioReadBlif.c \ src/base/io/ioReadEdif.c \ + src/base/io/ioReadEqn.c \ src/base/io/ioReadPla.c \ src/base/io/ioReadVerilog.c \ src/base/io/ioUtil.c \ src/base/io/ioWriteBench.c \ src/base/io/ioWriteBlif.c \ src/base/io/ioWriteCnf.c \ + src/base/io/ioWriteDot.c \ + src/base/io/ioWriteEqn.c \ + src/base/io/ioWriteGml.c \ src/base/io/ioWritePla.c diff --git a/src/map/fpga/fpgaCore.c b/src/map/fpga/fpgaCore.c index b181e997..0fc90228 100644 --- a/src/map/fpga/fpgaCore.c +++ b/src/map/fpga/fpgaCore.c @@ -71,7 +71,7 @@ int Fpga_Mapping( Fpga_Man_t * p ) return 0; p->timeRecover = clock() - clk; } -PRT( "Total mapping time", clock() - clkTotal ); +//PRT( "Total mapping time", clock() - clkTotal ); // print the AI-graph used for mapping //Fpga_ManShow( p, "test" ); diff --git a/src/misc/extra/extra.h b/src/misc/extra/extra.h index d298a204..14a3d950 100644 --- a/src/misc/extra/extra.h +++ b/src/misc/extra/extra.h @@ -117,6 +117,57 @@ extern DdNode * Extra_bddFindOneCube( DdManager * dd, DdNode * bF ); extern DdNode * Extra_bddGetOneCube( DdManager * dd, DdNode * bFunc ); extern DdNode * Extra_bddComputeRangeCube( DdManager * dd, int iStart, int iStop ); +/*=== extraBddSymm.c =================================================================*/ + +typedef struct Extra_SymmInfo_t_ Extra_SymmInfo_t; +struct Extra_SymmInfo_t_ { + int nVars; // the number of variables in the support + int nVarsMax; // the number of variables in the DD manager + int nSymms; // the number of pair-wise symmetries + int nNodes; // the number of nodes in a ZDD (if applicable) + int * pVars; // the list of all variables present in the support + char ** pSymms; // the symmetry information +}; + +/* computes the classical symmetry information for the function - recursive */ +extern Extra_SymmInfo_t * Extra_SymmPairsCompute( DdManager * dd, DdNode * bFunc ); +/* computes the classical symmetry information for the function - using naive approach */ +extern Extra_SymmInfo_t * Extra_SymmPairsComputeNaive( DdManager * dd, DdNode * bFunc ); +extern int Extra_bddCheckVarsSymmetricNaive( DdManager * dd, DdNode * bF, int iVar1, int iVar2 ); + +/* allocates the data structure */ +extern Extra_SymmInfo_t * Extra_SymmPairsAllocate( int nVars ); +/* deallocates the data structure */ +extern void Extra_SymmPairsDissolve( Extra_SymmInfo_t * ); +/* print the contents the data structure */ +extern void Extra_SymmPairsPrint( Extra_SymmInfo_t * ); +/* converts the ZDD into the Extra_SymmInfo_t structure */ +extern Extra_SymmInfo_t * Extra_SymmPairsCreateFromZdd( DdManager * dd, DdNode * zPairs, DdNode * bVars ); + +/* computes the classical symmetry information as a ZDD */ +extern DdNode * Extra_zddSymmPairsCompute( DdManager * dd, DdNode * bF, DdNode * bVars ); +extern DdNode * extraZddSymmPairsCompute( DdManager * dd, DdNode * bF, DdNode * bVars ); +/* returns a singleton-set ZDD containing all variables that are symmetric with the given one */ +extern DdNode * Extra_zddGetSymmetricVars( DdManager * dd, DdNode * bF, DdNode * bG, DdNode * bVars ); +extern DdNode * extraZddGetSymmetricVars( DdManager * dd, DdNode * bF, DdNode * bG, DdNode * bVars ); +/* converts a set of variables into a set of singleton subsets */ +extern DdNode * Extra_zddGetSingletons( DdManager * dd, DdNode * bVars ); +extern DdNode * extraZddGetSingletons( DdManager * dd, DdNode * bVars ); +/* filters the set of variables using the support of the function */ +extern DdNode * Extra_bddReduceVarSet( DdManager * dd, DdNode * bVars, DdNode * bF ); +extern DdNode * extraBddReduceVarSet( DdManager * dd, DdNode * bVars, DdNode * bF ); + +/* checks the possibility that the two vars are symmetric */ +extern int Extra_bddCheckVarsSymmetric( DdManager * dd, DdNode * bF, int iVar1, int iVar2 ); +extern DdNode * extraBddCheckVarsSymmetric( DdManager * dd, DdNode * bF, DdNode * bVars ); + +/* build the set of all tuples of K variables out of N from the BDD cube */ +extern DdNode * Extra_zddTuplesFromBdd( DdManager * dd, int K, DdNode * bVarsN ); +extern DdNode * extraZddTuplesFromBdd( DdManager * dd, DdNode * bVarsK, DdNode * bVarsN ); +/* selects one subset from a ZDD representing the set of subsets */ +extern DdNode * Extra_zddSelectOneSubset( DdManager * dd, DdNode * zS ); +extern DdNode * extraZddSelectOneSubset( DdManager * dd, DdNode * zS ); + /*=== extraUtilBitMatrix.c ================================================================*/ typedef struct Extra_BitMat_t_ Extra_BitMat_t; diff --git a/src/misc/extra/extraBddMisc.c b/src/misc/extra/extraBddMisc.c new file mode 100644 index 00000000..373ce5c5 --- /dev/null +++ b/src/misc/extra/extraBddMisc.c @@ -0,0 +1,1046 @@ +/**CFile**************************************************************** + + FileName [extraBddMisc.c] + + SystemName [ABC: Logic synthesis and verification system.] + + PackageName [extra] + + Synopsis [DD-based utilities.] + + Author [Alan Mishchenko] + + Affiliation [UC Berkeley] + + Date [Ver. 1.0. Started - June 20, 2005.] + + Revision [$Id: extraBddMisc.c,v 1.0 2003/09/01 00:00:00 alanmi Exp $] + +***********************************************************************/ + +#include "extra.h" + +/*---------------------------------------------------------------------------*/ +/* Constant declarations */ +/*---------------------------------------------------------------------------*/ + +/*---------------------------------------------------------------------------*/ +/* Stucture declarations */ +/*---------------------------------------------------------------------------*/ + +/*---------------------------------------------------------------------------*/ +/* Type declarations */ +/*---------------------------------------------------------------------------*/ + +/*---------------------------------------------------------------------------*/ +/* Variable declarations */ +/*---------------------------------------------------------------------------*/ + +/*---------------------------------------------------------------------------*/ +/* Macro declarations */ +/*---------------------------------------------------------------------------*/ + + +/**AutomaticStart*************************************************************/ + +/*---------------------------------------------------------------------------*/ +/* Static function prototypes */ +/*---------------------------------------------------------------------------*/ + +// file "extraDdTransfer.c" +static DdNode * extraTransferPermuteRecur( DdManager * ddS, DdManager * ddD, DdNode * f, st_table * table, int * Permute ); +static DdNode * extraTransferPermute( DdManager * ddS, DdManager * ddD, DdNode * f, int * Permute ); + +// file "cuddUtils.c" +static void ddSupportStep ARGS((DdNode *f, int *support)); +static void ddClearFlag ARGS((DdNode *f)); + +/**AutomaticEnd***************************************************************/ + +/*---------------------------------------------------------------------------*/ +/* Definition of exported functions */ +/*---------------------------------------------------------------------------*/ + +/**Function******************************************************************** + + Synopsis [Convert a {A,B}DD from a manager to another with variable remapping.] + + Description [Convert a {A,B}DD from a manager to another one. The orders of the + variables in the two managers may be different. Returns a + pointer to the {A,B}DD in the destination manager if successful; NULL + otherwise. The i-th entry in the array Permute tells what is the index + of the i-th variable from the old manager in the new manager.] + + SideEffects [None] + + SeeAlso [] + +******************************************************************************/ +DdNode * Extra_TransferPermute( DdManager * ddSource, DdManager * ddDestination, DdNode * f, int * Permute ) +{ + DdNode * bRes; + do + { + ddDestination->reordered = 0; + bRes = extraTransferPermute( ddSource, ddDestination, f, Permute ); + } + while ( ddDestination->reordered == 1 ); + return ( bRes ); + +} /* end of Extra_TransferPermute */ + +/**Function******************************************************************** + + Synopsis [Transfers the BDD from one manager into another level by level.] + + Description [Transfers the BDD from one manager into another while + preserving the correspondence between variables level by level.] + + SideEffects [None] + + SeeAlso [] + +******************************************************************************/ +DdNode * Extra_TransferLevelByLevel( DdManager * ddSource, DdManager * ddDestination, DdNode * f ) +{ + DdNode * bRes; + int * pPermute; + int nMin, nMax, i; + + nMin = ddMin(ddSource->size, ddDestination->size); + nMax = ddMax(ddSource->size, ddDestination->size); + pPermute = ALLOC( int, nMax ); + // set up the variable permutation + for ( i = 0; i < nMin; i++ ) + pPermute[ ddSource->invperm[i] ] = ddDestination->invperm[i]; + if ( ddSource->size > ddDestination->size ) + { + for ( ; i < nMax; i++ ) + pPermute[ ddSource->invperm[i] ] = -1; + } + bRes = Extra_TransferPermute( ddSource, ddDestination, f, pPermute ); + FREE( pPermute ); + return bRes; +} + +/**Function******************************************************************** + + Synopsis [Remaps the function to depend on the topmost variables on the manager.] + + Description [] + + SideEffects [] + + SeeAlso [] + +******************************************************************************/ +DdNode * Extra_bddRemapUp( + DdManager * dd, + DdNode * bF ) +{ + int * pPermute; + DdNode * bSupp, * bTemp, * bRes; + int Counter; + + pPermute = ALLOC( int, dd->size ); + + // get support + bSupp = Cudd_Support( dd, bF ); Cudd_Ref( bSupp ); + + // create the variable map + // to remap the DD into the upper part of the manager + Counter = 0; + for ( bTemp = bSupp; bTemp != dd->one; bTemp = cuddT(bTemp) ) + pPermute[bTemp->index] = dd->invperm[Counter++]; + + // transfer the BDD and remap it + bRes = Cudd_bddPermute( dd, bF, pPermute ); Cudd_Ref( bRes ); + + // remove support + Cudd_RecursiveDeref( dd, bSupp ); + + // return + Cudd_Deref( bRes ); + free( pPermute ); + return bRes; +} + +/**Function******************************************************************** + + Synopsis [Moves the BDD by the given number of variables up or down.] + + Description [] + + SideEffects [] + + SeeAlso [Extra_bddShift] + +******************************************************************************/ +DdNode * Extra_bddMove( + DdManager * dd, /* the DD manager */ + DdNode * bF, + int nVars) +{ + DdNode * res; + DdNode * bVars; + if ( nVars == 0 ) + return bF; + if ( Cudd_IsConstant(bF) ) + return bF; + assert( nVars <= dd->size ); + if ( nVars > 0 ) + bVars = dd->vars[nVars]; + else + bVars = Cudd_Not(dd->vars[-nVars]); + + do { + dd->reordered = 0; + res = extraBddMove( dd, bF, bVars ); + } while (dd->reordered == 1); + return(res); + +} /* end of Extra_bddMove */ + +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Extra_StopManager( DdManager * dd ) +{ + int RetValue; + // check for remaining references in the package + RetValue = Cudd_CheckZeroRef( dd ); + if ( RetValue > 0 ) + printf( "\nThe number of referenced nodes = %d\n\n", RetValue ); +// Cudd_PrintInfo( dd, stdout ); + Cudd_Quit( dd ); +} + +/**Function******************************************************************** + + Synopsis [Outputs the BDD in a readable format.] + + Description [] + + SideEffects [None] + + SeeAlso [] + +******************************************************************************/ +void Extra_bddPrint( DdManager * dd, DdNode * F ) +{ + DdGen * Gen; + int * Cube; + CUDD_VALUE_TYPE Value; + int nVars = dd->size; + int fFirstCube = 1; + int i; + + if ( F == NULL ) + { + printf("NULL"); + return; + } + if ( F == b0 ) + { + printf("Constant 0"); + return; + } + if ( F == b1 ) + { + printf("Constant 1"); + return; + } + + Cudd_ForeachCube( dd, F, Gen, Cube, Value ) + { + if ( fFirstCube ) + fFirstCube = 0; + else +// Output << " + "; + printf( " + " ); + + for ( i = 0; i < nVars; i++ ) + if ( Cube[i] == 0 ) + printf( "[%d]'", i ); +// printf( "%c'", (char)('a'+i) ); + else if ( Cube[i] == 1 ) + printf( "[%d]", i ); +// printf( "%c", (char)('a'+i) ); + } + +// printf("\n"); +} +/**Function******************************************************************** + + Synopsis [Returns the size of the support.] + + Description [] + + SideEffects [] + + SeeAlso [] + +******************************************************************************/ +int Extra_bddSuppSize( DdManager * dd, DdNode * bSupp ) +{ + int Counter = 0; + while ( bSupp != b1 ) + { + assert( !Cudd_IsComplement(bSupp) ); + assert( cuddE(bSupp) == b0 ); + + bSupp = cuddT(bSupp); + Counter++; + } + return Counter; +} + +/**Function******************************************************************** + + Synopsis [Returns 1 if the support contains the given BDD variable.] + + Description [] + + SideEffects [] + + SeeAlso [] + +******************************************************************************/ +int Extra_bddSuppContainVar( DdManager * dd, DdNode * bS, DdNode * bVar ) +{ + for( ; bS != b1; bS = cuddT(bS) ) + if ( bS->index == bVar->index ) + return 1; + return 0; +} + +/**Function******************************************************************** + + Synopsis [Returns 1 if two supports represented as BDD cubes are overlapping.] + + Description [] + + SideEffects [] + + SeeAlso [] + +******************************************************************************/ +int Extra_bddSuppOverlapping( DdManager * dd, DdNode * S1, DdNode * S2 ) +{ + while ( S1->index != CUDD_CONST_INDEX && S2->index != CUDD_CONST_INDEX ) + { + // if the top vars are the same, they intersect + if ( S1->index == S2->index ) + return 1; + // if the top vars are different, skip the one, which is higher + if ( dd->perm[S1->index] < dd->perm[S2->index] ) + S1 = cuddT(S1); + else + S2 = cuddT(S2); + } + return 0; +} + +/**Function******************************************************************** + + Synopsis [Returns the number of different vars in two supports.] + + Description [Counts the number of variables that appear in one support and + does not appear in other support. If the number exceeds DiffMax, returns DiffMax.] + + SideEffects [] + + SeeAlso [] + +******************************************************************************/ +int Extra_bddSuppDifferentVars( DdManager * dd, DdNode * S1, DdNode * S2, int DiffMax ) +{ + int Result = 0; + while ( S1->index != CUDD_CONST_INDEX && S2->index != CUDD_CONST_INDEX ) + { + // if the top vars are the same, this var is the same + if ( S1->index == S2->index ) + { + S1 = cuddT(S1); + S2 = cuddT(S2); + continue; + } + // the top var is different + Result++; + + if ( Result >= DiffMax ) + return DiffMax; + + // if the top vars are different, skip the one, which is higher + if ( dd->perm[S1->index] < dd->perm[S2->index] ) + S1 = cuddT(S1); + else + S2 = cuddT(S2); + } + + // consider the remaining variables + if ( S1->index != CUDD_CONST_INDEX ) + Result += Extra_bddSuppSize(dd,S1); + else if ( S2->index != CUDD_CONST_INDEX ) + Result += Extra_bddSuppSize(dd,S2); + + if ( Result >= DiffMax ) + return DiffMax; + return Result; +} + + +/**Function******************************************************************** + + Synopsis [Checks the support containment.] + + Description [This function returns 1 if one support is contained in another. + In this case, bLarge (bSmall) is assigned to point to the larger (smaller) support. + If the supports are identical, return 0 and does not assign the supports!] + + SideEffects [] + + SeeAlso [] + +******************************************************************************/ +int Extra_bddSuppCheckContainment( DdManager * dd, DdNode * bL, DdNode * bH, DdNode ** bLarge, DdNode ** bSmall ) +{ + DdNode * bSL = bL; + DdNode * bSH = bH; + int fLcontainsH = 1; + int fHcontainsL = 1; + int TopVar; + + if ( bSL == bSH ) + return 0; + + while ( bSL != b1 || bSH != b1 ) + { + if ( bSL == b1 ) + { // Low component has no vars; High components has some vars + fLcontainsH = 0; + if ( fHcontainsL == 0 ) + return 0; + else + break; + } + + if ( bSH == b1 ) + { // similarly + fHcontainsL = 0; + if ( fLcontainsH == 0 ) + return 0; + else + break; + } + + // determine the topmost var of the supports by comparing their levels + if ( dd->perm[bSL->index] < dd->perm[bSH->index] ) + TopVar = bSL->index; + else + TopVar = bSH->index; + + if ( TopVar == bSL->index && TopVar == bSH->index ) + { // they are on the same level + // it does not tell us anything about their containment + // skip this var + bSL = cuddT(bSL); + bSH = cuddT(bSH); + } + else if ( TopVar == bSL->index ) // and TopVar != bSH->index + { // Low components is higher and contains more vars + // it is not possible that High component contains Low + fHcontainsL = 0; + // skip this var + bSL = cuddT(bSL); + } + else // if ( TopVar == bSH->index ) // and TopVar != bSL->index + { // similarly + fLcontainsH = 0; + // skip this var + bSH = cuddT(bSH); + } + + // check the stopping condition + if ( !fHcontainsL && !fLcontainsH ) + return 0; + } + // only one of them can be true at the same time + assert( !fHcontainsL || !fLcontainsH ); + if ( fHcontainsL ) + { + *bLarge = bH; + *bSmall = bL; + } + else // fLcontainsH + { + *bLarge = bL; + *bSmall = bH; + } + return 1; +} + + +/**Function******************************************************************** + + Synopsis [Finds variables on which the DD depends and returns them as am array.] + + Description [Finds the variables on which the DD depends. Returns an array + with entries set to 1 for those variables that belong to the support; + NULL otherwise. The array is allocated by the user and should have at least + as many entries as the maximum number of variables in BDD and ZDD parts of + the manager.] + + SideEffects [None] + + SeeAlso [Cudd_Support Cudd_VectorSupport Cudd_ClassifySupport] + +******************************************************************************/ +int * +Extra_SupportArray( + DdManager * dd, /* manager */ + DdNode * f, /* DD whose support is sought */ + int * support ) /* array allocated by the user */ +{ + int i, size; + + /* Initialize support array for ddSupportStep. */ + size = ddMax(dd->size, dd->sizeZ); + for (i = 0; i < size; i++) + support[i] = 0; + + /* Compute support and clean up markers. */ + ddSupportStep(Cudd_Regular(f),support); + ddClearFlag(Cudd_Regular(f)); + + return(support); + +} /* end of Extra_SupportArray */ + +/**Function******************************************************************** + + Synopsis [Finds the variables on which a set of DDs depends.] + + Description [Finds the variables on which a set of DDs depends. + The set must contain either BDDs and ADDs, or ZDDs. + Returns a BDD consisting of the product of the variables if + successful; NULL otherwise.] + + SideEffects [None] + + SeeAlso [Cudd_Support Cudd_ClassifySupport] + +******************************************************************************/ +int * +Extra_VectorSupportArray( + DdManager * dd, /* manager */ + DdNode ** F, /* array of DDs whose support is sought */ + int n, /* size of the array */ + int * support ) /* array allocated by the user */ +{ + int i, size; + + /* Allocate and initialize support array for ddSupportStep. */ + size = ddMax( dd->size, dd->sizeZ ); + for ( i = 0; i < size; i++ ) + support[i] = 0; + + /* Compute support and clean up markers. */ + for ( i = 0; i < n; i++ ) + ddSupportStep( Cudd_Regular(F[i]), support ); + for ( i = 0; i < n; i++ ) + ddClearFlag( Cudd_Regular(F[i]) ); + + return support; +} + +/**Function******************************************************************** + + Synopsis [Find any cube belonging to the on-set of the function.] + + Description [] + + SideEffects [] + + SeeAlso [] + +******************************************************************************/ +DdNode * Extra_bddFindOneCube( DdManager * dd, DdNode * bF ) +{ + char * s_Temp; + DdNode * bCube, * bTemp; + int v; + + // get the vector of variables in the cube + s_Temp = ALLOC( char, dd->size ); + Cudd_bddPickOneCube( dd, bF, s_Temp ); + + // start the cube + bCube = b1; Cudd_Ref( bCube ); + for ( v = 0; v < dd->size; v++ ) + if ( s_Temp[v] == 0 ) + { +// Cube &= !s_XVars[v]; + bCube = Cudd_bddAnd( dd, bTemp = bCube, Cudd_Not(dd->vars[v]) ); Cudd_Ref( bCube ); + Cudd_RecursiveDeref( dd, bTemp ); + } + else if ( s_Temp[v] == 1 ) + { +// Cube &= s_XVars[v]; + bCube = Cudd_bddAnd( dd, bTemp = bCube, dd->vars[v] ); Cudd_Ref( bCube ); + Cudd_RecursiveDeref( dd, bTemp ); + } + Cudd_Deref(bCube); + free( s_Temp ); + return bCube; +} + +/**Function******************************************************************** + + Synopsis [Returns one cube contained in the given BDD.] + + Description [This function returns the cube with the smallest + bits-to-integer value.] + + SideEffects [] + +******************************************************************************/ +DdNode * Extra_bddGetOneCube( DdManager * dd, DdNode * bFunc ) +{ + DdNode * bFuncR, * bFunc0, * bFunc1; + DdNode * bRes0, * bRes1, * bRes; + + bFuncR = Cudd_Regular(bFunc); + if ( cuddIsConstant(bFuncR) ) + return bFunc; + + // cofactor + if ( Cudd_IsComplement(bFunc) ) + { + bFunc0 = Cudd_Not( cuddE(bFuncR) ); + bFunc1 = Cudd_Not( cuddT(bFuncR) ); + } + else + { + bFunc0 = cuddE(bFuncR); + bFunc1 = cuddT(bFuncR); + } + + // try to find the cube with the negative literal + bRes0 = Extra_bddGetOneCube( dd, bFunc0 ); Cudd_Ref( bRes0 ); + + if ( bRes0 != b0 ) + { + bRes = Cudd_bddAnd( dd, bRes0, Cudd_Not(dd->vars[bFuncR->index]) ); Cudd_Ref( bRes ); + Cudd_RecursiveDeref( dd, bRes0 ); + } + else + { + Cudd_RecursiveDeref( dd, bRes0 ); + // try to find the cube with the positive literal + bRes1 = Extra_bddGetOneCube( dd, bFunc1 ); Cudd_Ref( bRes1 ); + assert( bRes1 != b0 ); + bRes = Cudd_bddAnd( dd, bRes1, dd->vars[bFuncR->index] ); Cudd_Ref( bRes ); + Cudd_RecursiveDeref( dd, bRes1 ); + } + + Cudd_Deref( bRes ); + return bRes; +} + +/**Function******************************************************************** + + Synopsis [Performs the reordering-sensitive step of Extra_bddMove().] + + Description [] + + SideEffects [] + + SeeAlso [] + +******************************************************************************/ +DdNode * Extra_bddComputeRangeCube( DdManager * dd, int iStart, int iStop ) +{ + DdNode * bTemp, * bProd; + int i; + assert( iStart <= iStop ); + assert( iStart >= 0 && iStart <= dd->size ); + assert( iStop >= 0 && iStop <= dd->size ); + bProd = b1; Cudd_Ref( bProd ); + for ( i = iStart; i < iStop; i++ ) + { + bProd = Cudd_bddAnd( dd, bTemp = bProd, dd->vars[i] ); Cudd_Ref( bProd ); + Cudd_RecursiveDeref( dd, bTemp ); + } + Cudd_Deref( bProd ); + return bProd; +} + +/*---------------------------------------------------------------------------*/ +/* Definition of internal functions */ +/*---------------------------------------------------------------------------*/ + +/**Function******************************************************************** + + Synopsis [Performs the reordering-sensitive step of Extra_bddMove().] + + Description [] + + SideEffects [] + + SeeAlso [] + +******************************************************************************/ +DdNode * extraBddMove( + DdManager * dd, /* the DD manager */ + DdNode * bF, + DdNode * bDist) +{ + DdNode * bRes; + + if ( Cudd_IsConstant(bF) ) + return bF; + + if ( bRes = cuddCacheLookup2(dd, extraBddMove, bF, bDist) ) + return bRes; + else + { + DdNode * bRes0, * bRes1; + DdNode * bF0, * bF1; + DdNode * bFR = Cudd_Regular(bF); + int VarNew; + + if ( Cudd_IsComplement(bDist) ) + VarNew = bFR->index - Cudd_Not(bDist)->index; + else + VarNew = bFR->index + bDist->index; + assert( VarNew < dd->size ); + + // cofactor the functions + if ( bFR != bF ) // bFunc is complemented + { + bF0 = Cudd_Not( cuddE(bFR) ); + bF1 = Cudd_Not( cuddT(bFR) ); + } + else + { + bF0 = cuddE(bFR); + bF1 = cuddT(bFR); + } + + bRes0 = extraBddMove( dd, bF0, bDist ); + if ( bRes0 == NULL ) + return NULL; + cuddRef( bRes0 ); + + bRes1 = extraBddMove( dd, bF1, bDist ); + if ( bRes1 == NULL ) + { + Cudd_RecursiveDeref( dd, bRes0 ); + return NULL; + } + cuddRef( bRes1 ); + + /* only bRes0 and bRes1 are referenced at this point */ + bRes = cuddBddIteRecur( dd, dd->vars[VarNew], bRes1, bRes0 ); + if ( bRes == NULL ) + { + Cudd_RecursiveDeref( dd, bRes0 ); + Cudd_RecursiveDeref( dd, bRes1 ); + return NULL; + } + cuddRef( bRes ); + Cudd_RecursiveDeref( dd, bRes0 ); + Cudd_RecursiveDeref( dd, bRes1 ); + + /* insert the result into cache */ + cuddCacheInsert2( dd, extraBddMove, bF, bDist, bRes ); + cuddDeref( bRes ); + return bRes; + } +} /* end of extraBddMove */ + + +/**Function******************************************************************** + + Synopsis [Finds three cofactors of the cover w.r.t. to the topmost variable.] + + Description [Finds three cofactors of the cover w.r.t. to the topmost variable. + Does not check the cover for being a constant. Assumes that ZDD variables encoding + positive and negative polarities are adjacent in the variable order. Is different + from cuddZddGetCofactors3() in that it does not compute the cofactors w.r.t. the + given variable but takes the cofactors with respent to the topmost variable. + This function is more efficient when used in recursive procedures because it does + not require referencing of the resulting cofactors (compare cuddZddProduct() + and extraZddPrimeProduct()).] + + SideEffects [None] + + SeeAlso [cuddZddGetCofactors3] + +******************************************************************************/ +void +extraDecomposeCover( + DdManager* dd, /* the manager */ + DdNode* zC, /* the cover */ + DdNode** zC0, /* the pointer to the negative var cofactor */ + DdNode** zC1, /* the pointer to the positive var cofactor */ + DdNode** zC2 ) /* the pointer to the cofactor without var */ +{ + if ( (zC->index & 1) == 0 ) + { /* the top variable is present in positive polarity and maybe in negative */ + + DdNode *Temp = cuddE( zC ); + *zC1 = cuddT( zC ); + if ( cuddIZ(dd,Temp->index) == cuddIZ(dd,zC->index) + 1 ) + { /* Temp is not a terminal node + * top var is present in negative polarity */ + *zC2 = cuddE( Temp ); + *zC0 = cuddT( Temp ); + } + else + { /* top var is not present in negative polarity */ + *zC2 = Temp; + *zC0 = dd->zero; + } + } + else + { /* the top variable is present only in negative */ + *zC1 = dd->zero; + *zC2 = cuddE( zC ); + *zC0 = cuddT( zC ); + } +} /* extraDecomposeCover */ + +/*---------------------------------------------------------------------------*/ +/* Definition of static Functions */ +/*---------------------------------------------------------------------------*/ + +/**Function******************************************************************** + + Synopsis [Convert a BDD from a manager to another one.] + + Description [Convert a BDD from a manager to another one. Returns a + pointer to the BDD in the destination manager if successful; NULL + otherwise.] + + SideEffects [None] + + SeeAlso [Extra_TransferPermute] + +******************************************************************************/ +DdNode * extraTransferPermute( DdManager * ddS, DdManager * ddD, DdNode * f, int * Permute ) +{ + DdNode *res; + st_table *table = NULL; + st_generator *gen = NULL; + DdNode *key, *value; + + table = st_init_table( st_ptrcmp, st_ptrhash ); + if ( table == NULL ) + goto failure; + res = extraTransferPermuteRecur( ddS, ddD, f, table, Permute ); + if ( res != NULL ) + cuddRef( res ); + + /* Dereference all elements in the table and dispose of the table. + ** This must be done also if res is NULL to avoid leaks in case of + ** reordering. */ + gen = st_init_gen( table ); + if ( gen == NULL ) + goto failure; + while ( st_gen( gen, ( char ** ) &key, ( char ** ) &value ) ) + { + Cudd_RecursiveDeref( ddD, value ); + } + st_free_gen( gen ); + gen = NULL; + st_free_table( table ); + table = NULL; + + if ( res != NULL ) + cuddDeref( res ); + return ( res ); + + failure: + if ( table != NULL ) + st_free_table( table ); + if ( gen != NULL ) + st_free_gen( gen ); + return ( NULL ); + +} /* end of extraTransferPermute */ + + +/**Function******************************************************************** + + Synopsis [Performs the recursive step of Extra_TransferPermute.] + + Description [Performs the recursive step of Extra_TransferPermute. + Returns a pointer to the result if successful; NULL otherwise.] + + SideEffects [None] + + SeeAlso [extraTransferPermute] + +******************************************************************************/ +static DdNode * +extraTransferPermuteRecur( + DdManager * ddS, + DdManager * ddD, + DdNode * f, + st_table * table, + int * Permute ) +{ + DdNode *ft, *fe, *t, *e, *var, *res; + DdNode *one, *zero; + int index; + int comple = 0; + + statLine( ddD ); + one = DD_ONE( ddD ); + comple = Cudd_IsComplement( f ); + + /* Trivial cases. */ + if ( Cudd_IsConstant( f ) ) + return ( Cudd_NotCond( one, comple ) ); + + + /* Make canonical to increase the utilization of the cache. */ + f = Cudd_NotCond( f, comple ); + /* Now f is a regular pointer to a non-constant node. */ + + /* Check the cache. */ + if ( st_lookup( table, ( char * ) f, ( char ** ) &res ) ) + return ( Cudd_NotCond( res, comple ) ); + + /* Recursive step. */ + if ( Permute ) + index = Permute[f->index]; + else + index = f->index; + + ft = cuddT( f ); + fe = cuddE( f ); + + t = extraTransferPermuteRecur( ddS, ddD, ft, table, Permute ); + if ( t == NULL ) + { + return ( NULL ); + } + cuddRef( t ); + + e = extraTransferPermuteRecur( ddS, ddD, fe, table, Permute ); + if ( e == NULL ) + { + Cudd_RecursiveDeref( ddD, t ); + return ( NULL ); + } + cuddRef( e ); + + zero = Cudd_Not(ddD->one); + var = cuddUniqueInter( ddD, index, one, zero ); + if ( var == NULL ) + { + Cudd_RecursiveDeref( ddD, t ); + Cudd_RecursiveDeref( ddD, e ); + return ( NULL ); + } + res = cuddBddIteRecur( ddD, var, t, e ); + + if ( res == NULL ) + { + Cudd_RecursiveDeref( ddD, t ); + Cudd_RecursiveDeref( ddD, e ); + return ( NULL ); + } + cuddRef( res ); + Cudd_RecursiveDeref( ddD, t ); + Cudd_RecursiveDeref( ddD, e ); + + if ( st_add_direct( table, ( char * ) f, ( char * ) res ) == + ST_OUT_OF_MEM ) + { + Cudd_RecursiveDeref( ddD, res ); + return ( NULL ); + } + return ( Cudd_NotCond( res, comple ) ); + +} /* end of extraTransferPermuteRecur */ + +/**Function******************************************************************** + + Synopsis [Performs the recursive step of Cudd_Support.] + + Description [Performs the recursive step of Cudd_Support. Performs a + DFS from f. The support is accumulated in supp as a side effect. Uses + the LSB of the then pointer as visited flag.] + + SideEffects [None] + + SeeAlso [ddClearFlag] + +******************************************************************************/ +static void +ddSupportStep( + DdNode * f, + int * support) +{ + if (cuddIsConstant(f) || Cudd_IsComplement(f->next)) { + return; + } + + support[f->index] = 1; + ddSupportStep(cuddT(f),support); + ddSupportStep(Cudd_Regular(cuddE(f)),support); + /* Mark as visited. */ + f->next = Cudd_Not(f->next); + return; + +} /* end of ddSupportStep */ + + +/**Function******************************************************************** + + Synopsis [Performs a DFS from f, clearing the LSB of the next + pointers.] + + Description [] + + SideEffects [None] + + SeeAlso [ddSupportStep ddDagInt] + +******************************************************************************/ +static void +ddClearFlag( + DdNode * f) +{ + if (!Cudd_IsComplement(f->next)) { + return; + } + /* Clear visited flag. */ + f->next = Cudd_Regular(f->next); + if (cuddIsConstant(f)) { + return; + } + ddClearFlag(cuddT(f)); + ddClearFlag(Cudd_Regular(cuddE(f))); + return; + +} /* end of ddClearFlag */ + + +//////////////////////////////////////////////////////////////////////// +/// END OF FILE /// +//////////////////////////////////////////////////////////////////////// + + diff --git a/src/misc/extra/extraBddSymm.c b/src/misc/extra/extraBddSymm.c new file mode 100644 index 00000000..474f663f --- /dev/null +++ b/src/misc/extra/extraBddSymm.c @@ -0,0 +1,1469 @@ +/**CFile**************************************************************** + + FileName [extraBddSymm.c] + + PackageName [extra] + + Synopsis [Efficient methods to compute the information about + symmetric variables using the algorithm presented in the paper: + A. Mishchenko. Fast Computation of Symmetries in Boolean Functions. + Transactions on CAD, Nov. 2003.] + + Author [Alan Mishchenko] + + Affiliation [UC Berkeley] + + Date [Ver. 2.0. Started - September 1, 2003.] + + Revision [$Id: extraBddSymm.c,v 1.0 2003/09/01 00:00:00 alanmi Exp $] + +***********************************************************************/ + +#include "extra.h" + +/*---------------------------------------------------------------------------*/ +/* Constant declarations */ +/*---------------------------------------------------------------------------*/ + +/*---------------------------------------------------------------------------*/ +/* Stucture declarations */ +/*---------------------------------------------------------------------------*/ + +/*---------------------------------------------------------------------------*/ +/* Type declarations */ +/*---------------------------------------------------------------------------*/ + +/*---------------------------------------------------------------------------*/ +/* Variable declarations */ +/*---------------------------------------------------------------------------*/ + +/*---------------------------------------------------------------------------*/ +/* Macro declarations */ +/*---------------------------------------------------------------------------*/ + +#define DD_GET_SYMM_VARS_TAG 0x0a /* former DD_BDD_XOR_EXIST_ABSTRACT_TAG */ + +/**AutomaticStart*************************************************************/ + +/*---------------------------------------------------------------------------*/ +/* Static function prototypes */ +/*---------------------------------------------------------------------------*/ + +/**AutomaticEnd***************************************************************/ + +/*---------------------------------------------------------------------------*/ +/* Definition of exported functions */ +/*---------------------------------------------------------------------------*/ + +/**Function******************************************************************** + + Synopsis [Computes the classical symmetry information for the function.] + + Description [Returns the symmetry information in the form of Extra_SymmInfo_t structure.] + + SideEffects [If the ZDD variables are not derived from BDD variables with + multiplicity 2, this function may derive them in a wrong way.] + + SeeAlso [] + +******************************************************************************/ +Extra_SymmInfo_t * Extra_SymmPairsCompute( + DdManager * dd, /* the manager */ + DdNode * bFunc) /* the function whose symmetries are computed */ +{ + DdNode * bSupp; + DdNode * zRes; + Extra_SymmInfo_t * p; + + bSupp = Cudd_Support( dd, bFunc ); Cudd_Ref( bSupp ); + zRes = Extra_zddSymmPairsCompute( dd, bFunc, bSupp ); Cudd_Ref( zRes ); + + p = Extra_SymmPairsCreateFromZdd( dd, zRes, bSupp ); + + Cudd_RecursiveDeref( dd, bSupp ); + Cudd_RecursiveDerefZdd( dd, zRes ); + + return p; + +} /* end of Extra_SymmPairsCompute */ + + +/**Function******************************************************************** + + Synopsis [Computes the classical symmetry information as a ZDD.] + + Description [] + + SideEffects [] + + SeeAlso [] + +******************************************************************************/ +DdNode * Extra_zddSymmPairsCompute( + DdManager * dd, /* the DD manager */ + DdNode * bF, + DdNode * bVars) +{ + DdNode * res; + do { + dd->reordered = 0; + res = extraZddSymmPairsCompute( dd, bF, bVars ); + } while (dd->reordered == 1); + return(res); + +} /* end of Extra_zddSymmPairsCompute */ + +/**Function******************************************************************** + + Synopsis [Returns a singleton-set ZDD containing all variables that are symmetric with the given one.] + + Description [] + + SideEffects [] + + SeeAlso [] + +******************************************************************************/ +DdNode * Extra_zddGetSymmetricVars( + DdManager * dd, /* the DD manager */ + DdNode * bF, /* the first function - originally, the positive cofactor */ + DdNode * bG, /* the second fucntion - originally, the negative cofactor */ + DdNode * bVars) /* the set of variables, on which F and G depend */ +{ + DdNode * res; + do { + dd->reordered = 0; + res = extraZddGetSymmetricVars( dd, bF, bG, bVars ); + } while (dd->reordered == 1); + return(res); + +} /* end of Extra_zddGetSymmetricVars */ + + +/**Function******************************************************************** + + Synopsis [Converts a set of variables into a set of singleton subsets.] + + Description [] + + SideEffects [] + + SeeAlso [] + +******************************************************************************/ +DdNode * Extra_zddGetSingletons( + DdManager * dd, /* the DD manager */ + DdNode * bVars) /* the set of variables */ +{ + DdNode * res; + do { + dd->reordered = 0; + res = extraZddGetSingletons( dd, bVars ); + } while (dd->reordered == 1); + return(res); + +} /* end of Extra_zddGetSingletons */ + +/**Function******************************************************************** + + Synopsis [Filters the set of variables using the support of the function.] + + Description [] + + SideEffects [] + + SeeAlso [] + +******************************************************************************/ +DdNode * Extra_bddReduceVarSet( + DdManager * dd, /* the DD manager */ + DdNode * bVars, /* the set of variables to be reduced */ + DdNode * bF) /* the function whose support is used for reduction */ +{ + DdNode * res; + do { + dd->reordered = 0; + res = extraBddReduceVarSet( dd, bVars, bF ); + } while (dd->reordered == 1); + return(res); + +} /* end of Extra_bddReduceVarSet */ + + +/**Function******************************************************************** + + Synopsis [Allocates symmetry information structure.] + + Description [] + + SideEffects [] + + SeeAlso [] + +******************************************************************************/ +Extra_SymmInfo_t * Extra_SymmPairsAllocate( int nVars ) +{ + int i; + Extra_SymmInfo_t * p; + + // allocate and clean the storage for symmetry info + p = ALLOC( Extra_SymmInfo_t, 1 ); + memset( p, 0, sizeof(Extra_SymmInfo_t) ); + p->nVars = nVars; + p->pVars = ALLOC( int, nVars ); + p->pSymms = ALLOC( char *, nVars ); + p->pSymms[0] = ALLOC( char , nVars * nVars ); + memset( p->pSymms[0], 0, nVars * nVars * sizeof(char) ); + + for ( i = 1; i < nVars; i++ ) + p->pSymms[i] = p->pSymms[i-1] + nVars; + + return p; +} /* end of Extra_SymmPairsAllocate */ + +/**Function******************************************************************** + + Synopsis [Delocates symmetry information structure.] + + Description [] + + SideEffects [] + + SeeAlso [] + +******************************************************************************/ +void Extra_SymmPairsDissolve( Extra_SymmInfo_t * p ) +{ + free( p->pVars ); + free( p->pSymms[0] ); + free( p->pSymms ); + free( p ); +} /* end of Extra_SymmPairsDissolve */ + +/**Function******************************************************************** + + Synopsis [Allocates symmetry information structure.] + + Description [] + + SideEffects [] + + SeeAlso [] + +******************************************************************************/ +void Extra_SymmPairsPrint( Extra_SymmInfo_t * p ) +{ + int i, k; + printf( "\n" ); + for ( i = 0; i < p->nVars; i++ ) + { + for ( k = 0; k <= i; k++ ) + printf( " " ); + for ( k = i+1; k < p->nVars; k++ ) + if ( p->pSymms[i][k] ) + printf( "1" ); + else + printf( "." ); + printf( "\n" ); + } +} /* end of Extra_SymmPairsPrint */ + + +/**Function******************************************************************** + + Synopsis [Creates the symmetry information structure from ZDD.] + + Description [ZDD representation of symmetries is the set of cubes, each + of which has two variables in the positive polarity. These variables correspond + to the symmetric variable pair.] + + SideEffects [] + + SeeAlso [] + +******************************************************************************/ +Extra_SymmInfo_t * Extra_SymmPairsCreateFromZdd( DdManager * dd, DdNode * zPairs, DdNode * bSupp ) +{ + int i; + int nSuppSize; + Extra_SymmInfo_t * p; + int * pMapVars2Nums; + DdNode * bTemp; + DdNode * zSet, * zCube, * zTemp; + int iVar1, iVar2; + + nSuppSize = Extra_bddSuppSize( dd, bSupp ); + + // allocate and clean the storage for symmetry info + p = Extra_SymmPairsAllocate( nSuppSize ); + + // allocate the storage for the temporary map + pMapVars2Nums = ALLOC( int, dd->size ); + memset( pMapVars2Nums, 0, dd->size * sizeof(int) ); + + // assign the variables + p->nVarsMax = dd->size; +// p->nNodes = Cudd_DagSize( zPairs ); + p->nNodes = 0; + for ( i = 0, bTemp = bSupp; bTemp != b1; bTemp = cuddT(bTemp), i++ ) + { + p->pVars[i] = bTemp->index; + pMapVars2Nums[bTemp->index] = i; + } + + // write the symmetry info into the structure + zSet = zPairs; Cudd_Ref( zSet ); + while ( zSet != z0 ) + { + // get the next cube + zCube = Extra_zddSelectOneSubset( dd, zSet ); Cudd_Ref( zCube ); + + // add these two variables to the data structure + assert( cuddT( cuddT(zCube) ) == z1 ); + iVar1 = zCube->index/2; + iVar2 = cuddT(zCube)->index/2; + if ( pMapVars2Nums[iVar1] < pMapVars2Nums[iVar2] ) + p->pSymms[ pMapVars2Nums[iVar1] ][ pMapVars2Nums[iVar2] ] = 1; + else + p->pSymms[ pMapVars2Nums[iVar2] ][ pMapVars2Nums[iVar1] ] = 1; + // count the symmetric pairs + p->nSymms ++; + + // update the cuver and deref the cube + zSet = Cudd_zddDiff( dd, zTemp = zSet, zCube ); Cudd_Ref( zSet ); + Cudd_RecursiveDerefZdd( dd, zTemp ); + Cudd_RecursiveDerefZdd( dd, zCube ); + + } // for each cube + Cudd_RecursiveDerefZdd( dd, zSet ); + + FREE( pMapVars2Nums ); + return p; + +} /* end of Extra_SymmPairsCreateFromZdd */ + + +/**Function******************************************************************** + + Synopsis [Checks the possibility of two variables being symmetric.] + + Description [Returns 0 if vars are not symmetric. Return 1 if vars can be symmetric.] + + SideEffects [] + + SeeAlso [] + +******************************************************************************/ +int Extra_bddCheckVarsSymmetric( + DdManager * dd, /* the DD manager */ + DdNode * bF, + int iVar1, + int iVar2) +{ + DdNode * bVars; + int Res; + +// return 1; + + assert( iVar1 != iVar2 ); + assert( iVar1 < dd->size ); + assert( iVar2 < dd->size ); + + bVars = Cudd_bddAnd( dd, dd->vars[iVar1], dd->vars[iVar2] ); Cudd_Ref( bVars ); + + Res = (int)( extraBddCheckVarsSymmetric( dd, bF, bVars ) == b1 ); + + Cudd_RecursiveDeref( dd, bVars ); + + return Res; +} /* end of Extra_bddCheckVarsSymmetric */ + + +/**Function******************************************************************** + + Synopsis [Computes the classical symmetry information for the function.] + + Description [Uses the naive way of comparing cofactors.] + + SideEffects [] + + SeeAlso [] + +******************************************************************************/ +Extra_SymmInfo_t * Extra_SymmPairsComputeNaive( DdManager * dd, DdNode * bFunc ) +{ + DdNode * bSupp, * bTemp; + int nSuppSize; + Extra_SymmInfo_t * p; + int i, k; + + // compute the support + bSupp = Cudd_Support( dd, bFunc ); Cudd_Ref( bSupp ); + nSuppSize = Extra_bddSuppSize( dd, bSupp ); +//printf( "Support = %d. ", nSuppSize ); +//Extra_bddPrint( dd, bSupp ); +//printf( "%d ", nSuppSize ); + + // allocate the storage for symmetry info + p = Extra_SymmPairsAllocate( nSuppSize ); + + // assign the variables + p->nVarsMax = dd->size; + for ( i = 0, bTemp = bSupp; bTemp != b1; bTemp = cuddT(bTemp), i++ ) + p->pVars[i] = bTemp->index; + + // go through the candidate pairs and check using Idea1 + for ( i = 0; i < nSuppSize; i++ ) + for ( k = i+1; k < nSuppSize; k++ ) + { + p->pSymms[k][i] = p->pSymms[i][k] = Extra_bddCheckVarsSymmetricNaive( dd, bFunc, p->pVars[i], p->pVars[k] ); + if ( p->pSymms[i][k] ) + p->nSymms++; + } + + Cudd_RecursiveDeref( dd, bSupp ); + return p; + +} /* end of Extra_SymmPairsComputeNaive */ + +/**Function******************************************************************** + + Synopsis [Checks if the two variables are symmetric.] + + Description [Returns 0 if vars are not symmetric. Return 1 if vars are symmetric.] + + SideEffects [] + + SeeAlso [] + +******************************************************************************/ +int Extra_bddCheckVarsSymmetricNaive( + DdManager * dd, /* the DD manager */ + DdNode * bF, + int iVar1, + int iVar2) +{ + DdNode * bCube1, * bCube2; + DdNode * bCof01, * bCof10; + int Res; + + assert( iVar1 != iVar2 ); + assert( iVar1 < dd->size ); + assert( iVar2 < dd->size ); + + bCube1 = Cudd_bddAnd( dd, Cudd_Not( dd->vars[iVar1] ), dd->vars[iVar2] ); Cudd_Ref( bCube1 ); + bCube2 = Cudd_bddAnd( dd, Cudd_Not( dd->vars[iVar2] ), dd->vars[iVar1] ); Cudd_Ref( bCube2 ); + + bCof01 = Cudd_Cofactor( dd, bF, bCube1 ); Cudd_Ref( bCof01 ); + bCof10 = Cudd_Cofactor( dd, bF, bCube2 ); Cudd_Ref( bCof10 ); + + Res = (int)( bCof10 == bCof01 ); + + Cudd_RecursiveDeref( dd, bCof01 ); + Cudd_RecursiveDeref( dd, bCof10 ); + Cudd_RecursiveDeref( dd, bCube1 ); + Cudd_RecursiveDeref( dd, bCube2 ); + + return Res; +} /* end of Extra_bddCheckVarsSymmetricNaive */ + + +/**Function******************************************************************** + + Synopsis [Builds ZDD representing the set of fixed-size variable tuples.] + + Description [Creates ZDD of all combinations of variables in Support that + is represented by a BDD.] + + SideEffects [New ZDD variables are created if indices of the variables + present in the combination are larger than the currently + allocated number of ZDD variables.] + + SeeAlso [] + +******************************************************************************/ +DdNode* Extra_zddTuplesFromBdd( + DdManager * dd, /* the DD manager */ + int K, /* the number of variables in tuples */ + DdNode * bVarsN) /* the set of all variables represented as a BDD */ +{ + DdNode *zRes; + int autoDynZ; + + autoDynZ = dd->autoDynZ; + dd->autoDynZ = 0; + + do { + /* transform the numeric arguments (K) into a DdNode* argument; + * this allows us to use the standard internal CUDD cache */ + DdNode *bVarSet = bVarsN, *bVarsK = bVarsN; + int nVars = 0, i; + + /* determine the number of variables in VarSet */ + while ( bVarSet != b1 ) + { + nVars++; + /* make sure that the VarSet is a cube */ + if ( cuddE( bVarSet ) != b0 ) + return NULL; + bVarSet = cuddT( bVarSet ); + } + /* make sure that the number of variables in VarSet is less or equal + that the number of variables that should be present in the tuples + */ + if ( K > nVars ) + return NULL; + + /* the second argument in the recursive call stannds for ; + /* reate the first argument, which stands for + * as when we are talking about the tuple of out of */ + for ( i = 0; i < nVars-K; i++ ) + bVarsK = cuddT( bVarsK ); + + dd->reordered = 0; + zRes = extraZddTuplesFromBdd(dd, bVarsK, bVarsN ); + + } while (dd->reordered == 1); + dd->autoDynZ = autoDynZ; + return zRes; + +} /* end of Extra_zddTuplesFromBdd */ + +/**Function******************************************************************** + + Synopsis [Selects one subset from the set of subsets represented by a ZDD.] + + Description [] + + SideEffects [None] + + SeeAlso [] + +******************************************************************************/ +DdNode* Extra_zddSelectOneSubset( + DdManager * dd, /* the DD manager */ + DdNode * zS) /* the ZDD */ +{ + DdNode *res; + do { + dd->reordered = 0; + res = extraZddSelectOneSubset(dd, zS); + } while (dd->reordered == 1); + return(res); + +} /* end of Extra_zddSelectOneSubset */ + + +/*---------------------------------------------------------------------------*/ +/* Definition of internal functions */ +/*---------------------------------------------------------------------------*/ + +/**Function******************************************************************** + + Synopsis [Performs a recursive step of Extra_SymmPairsCompute.] + + Description [Returns the set of symmetric variable pairs represented as a set + of two-literal ZDD cubes. Both variables always appear in the positive polarity + in the cubes. This function works without building new BDD nodes. Some relatively + small number of ZDD nodes may be built to ensure proper bookkeeping of the + symmetry information.] + + SideEffects [] + + SeeAlso [] + +******************************************************************************/ +DdNode * +extraZddSymmPairsCompute( + DdManager * dd, /* the manager */ + DdNode * bFunc, /* the function whose symmetries are computed */ + DdNode * bVars ) /* the set of variables on which this function depends */ +{ + DdNode * zRes; + DdNode * bFR = Cudd_Regular(bFunc); + + if ( cuddIsConstant(bFR) ) + { + int nVars, i; + + // determine how many vars are in the bVars + nVars = Extra_bddSuppSize( dd, bVars ); + if ( nVars < 2 ) + return z0; + else + { + DdNode * bVarsK; + + // create the BDD bVarsK corresponding to K = 2; + bVarsK = bVars; + for ( i = 0; i < nVars-2; i++ ) + bVarsK = cuddT( bVarsK ); + return extraZddTuplesFromBdd( dd, bVarsK, bVars ); + } + } + assert( bVars != b1 ); + + if ( zRes = cuddCacheLookup2Zdd(dd, extraZddSymmPairsCompute, bFunc, bVars) ) + return zRes; + else + { + DdNode * zRes0, * zRes1; + DdNode * zTemp, * zPlus, * zSymmVars; + DdNode * bF0, * bF1; + DdNode * bVarsNew; + int nVarsExtra; + int LevelF; + + // every variable in bF should be also in bVars, therefore LevelF cannot be above LevelV + // if LevelF is below LevelV, scroll through the vars in bVars to the same level as F + // count how many extra vars are there in bVars + nVarsExtra = 0; + LevelF = dd->perm[bFR->index]; + for ( bVarsNew = bVars; LevelF > dd->perm[bVarsNew->index]; bVarsNew = cuddT(bVarsNew) ) + nVarsExtra++; + // the indexes (level) of variables should be synchronized now + assert( bFR->index == bVarsNew->index ); + + // cofactor the function + if ( bFR != bFunc ) // bFunc is complemented + { + bF0 = Cudd_Not( cuddE(bFR) ); + bF1 = Cudd_Not( cuddT(bFR) ); + } + else + { + bF0 = cuddE(bFR); + bF1 = cuddT(bFR); + } + + // solve subproblems + zRes0 = extraZddSymmPairsCompute( dd, bF0, cuddT(bVarsNew) ); + if ( zRes0 == NULL ) + return NULL; + cuddRef( zRes0 ); + + // if there is no symmetries in the negative cofactor + // there is no need to test the positive cofactor + if ( zRes0 == z0 ) + zRes = zRes0; // zRes takes reference + else + { + zRes1 = extraZddSymmPairsCompute( dd, bF1, cuddT(bVarsNew) ); + if ( zRes1 == NULL ) + { + Cudd_RecursiveDerefZdd( dd, zRes0 ); + return NULL; + } + cuddRef( zRes1 ); + + // only those variables are pair-wise symmetric + // that are pair-wise symmetric in both cofactors + // therefore, intersect the solutions + zRes = cuddZddIntersect( dd, zRes0, zRes1 ); + if ( zRes == NULL ) + { + Cudd_RecursiveDerefZdd( dd, zRes0 ); + Cudd_RecursiveDerefZdd( dd, zRes1 ); + return NULL; + } + cuddRef( zRes ); + Cudd_RecursiveDerefZdd( dd, zRes0 ); + Cudd_RecursiveDerefZdd( dd, zRes1 ); + } + + // consider the current top-most variable and find all the vars + // that are pairwise symmetric with it + // these variables are returned as a set of ZDD singletons + zSymmVars = extraZddGetSymmetricVars( dd, bF1, bF0, cuddT(bVarsNew) ); + if ( zSymmVars == NULL ) + { + Cudd_RecursiveDerefZdd( dd, zRes ); + return NULL; + } + cuddRef( zSymmVars ); + + // attach the topmost variable to the set, to get the variable pairs + // use the positive polarity ZDD variable for the purpose + + // there is no need to do so, if zSymmVars is empty + if ( zSymmVars == z0 ) + Cudd_RecursiveDerefZdd( dd, zSymmVars ); + else + { + zPlus = cuddZddGetNode( dd, 2*bFR->index, zSymmVars, z0 ); + if ( zPlus == NULL ) + { + Cudd_RecursiveDerefZdd( dd, zRes ); + Cudd_RecursiveDerefZdd( dd, zSymmVars ); + return NULL; + } + cuddRef( zPlus ); + cuddDeref( zSymmVars ); + + // add these variable pairs to the result + zRes = cuddZddUnion( dd, zTemp = zRes, zPlus ); + if ( zRes == NULL ) + { + Cudd_RecursiveDerefZdd( dd, zTemp ); + Cudd_RecursiveDerefZdd( dd, zPlus ); + return NULL; + } + cuddRef( zRes ); + Cudd_RecursiveDerefZdd( dd, zTemp ); + Cudd_RecursiveDerefZdd( dd, zPlus ); + } + + // only zRes is referenced at this point + + // if we skipped some variables, these variables cannot be symmetric with + // any variables that are currently in the support of bF, but they can be + // symmetric with the variables that are in bVars but not in the support of bF + if ( nVarsExtra ) + { + // it is possible to improve this step: + // (1) there is no need to enter here, if nVarsExtra < 2 + + // create the set of topmost nVarsExtra in bVars + DdNode * bVarsExtra; + int nVars; + + // remove from bVars all the variable that are in the support of bFunc + bVarsExtra = extraBddReduceVarSet( dd, bVars, bFunc ); + if ( bVarsExtra == NULL ) + { + Cudd_RecursiveDerefZdd( dd, zRes ); + return NULL; + } + cuddRef( bVarsExtra ); + + // determine how many vars are in the bVarsExtra + nVars = Extra_bddSuppSize( dd, bVarsExtra ); + if ( nVars < 2 ) + { + Cudd_RecursiveDeref( dd, bVarsExtra ); + } + else + { + int i; + DdNode * bVarsK; + + // create the BDD bVarsK corresponding to K = 2; + bVarsK = bVarsExtra; + for ( i = 0; i < nVars-2; i++ ) + bVarsK = cuddT( bVarsK ); + + // create the 2 variable tuples + zPlus = extraZddTuplesFromBdd( dd, bVarsK, bVarsExtra ); + if ( zPlus == NULL ) + { + Cudd_RecursiveDeref( dd, bVarsExtra ); + Cudd_RecursiveDerefZdd( dd, zRes ); + return NULL; + } + cuddRef( zPlus ); + Cudd_RecursiveDeref( dd, bVarsExtra ); + + // add these to the result + zRes = cuddZddUnion( dd, zTemp = zRes, zPlus ); + if ( zRes == NULL ) + { + Cudd_RecursiveDerefZdd( dd, zTemp ); + Cudd_RecursiveDerefZdd( dd, zPlus ); + return NULL; + } + cuddRef( zRes ); + Cudd_RecursiveDerefZdd( dd, zTemp ); + Cudd_RecursiveDerefZdd( dd, zPlus ); + } + } + cuddDeref( zRes ); + + + /* insert the result into cache */ + cuddCacheInsert2(dd, extraZddSymmPairsCompute, bFunc, bVars, zRes); + return zRes; + } +} /* end of extraZddSymmPairsCompute */ + +/**Function******************************************************************** + + Synopsis [Performs a recursive step of Extra_zddGetSymmetricVars.] + + Description [Returns the set of ZDD singletons, containing those positive + ZDD variables that correspond to BDD variables x, for which it is true + that bF(x=0) == bG(x=1).] + + SideEffects [] + + SeeAlso [] + +******************************************************************************/ +DdNode * extraZddGetSymmetricVars( + DdManager * dd, /* the DD manager */ + DdNode * bF, /* the first function - originally, the positive cofactor */ + DdNode * bG, /* the second function - originally, the negative cofactor */ + DdNode * bVars) /* the set of variables, on which F and G depend */ +{ + DdNode * zRes; + DdNode * bFR = Cudd_Regular(bF); + DdNode * bGR = Cudd_Regular(bG); + + if ( cuddIsConstant(bFR) && cuddIsConstant(bGR) ) + { + if ( bF == bG ) + return extraZddGetSingletons( dd, bVars ); + else + return z0; + } + assert( bVars != b1 ); + + if ( zRes = cuddCacheLookupZdd(dd, DD_GET_SYMM_VARS_TAG, bF, bG, bVars) ) + return zRes; + else + { + DdNode * zRes0, * zRes1; + DdNode * zPlus, * zTemp; + DdNode * bF0, * bF1; + DdNode * bG0, * bG1; + DdNode * bVarsNew; + + int LevelF = cuddI(dd,bFR->index); + int LevelG = cuddI(dd,bGR->index); + int LevelFG; + + if ( LevelF < LevelG ) + LevelFG = LevelF; + else + LevelFG = LevelG; + + // at least one of the arguments is not a constant + assert( LevelFG < dd->size ); + + // every variable in bF and bG should be also in bVars, therefore LevelFG cannot be above LevelV + // if LevelFG is below LevelV, scroll through the vars in bVars to the same level as LevelFG + for ( bVarsNew = bVars; LevelFG > dd->perm[bVarsNew->index]; bVarsNew = cuddT(bVarsNew) ); + assert( LevelFG == dd->perm[bVarsNew->index] ); + + // cofactor the functions + if ( LevelF == LevelFG ) + { + if ( bFR != bF ) // bF is complemented + { + bF0 = Cudd_Not( cuddE(bFR) ); + bF1 = Cudd_Not( cuddT(bFR) ); + } + else + { + bF0 = cuddE(bFR); + bF1 = cuddT(bFR); + } + } + else + bF0 = bF1 = bF; + + if ( LevelG == LevelFG ) + { + if ( bGR != bG ) // bG is complemented + { + bG0 = Cudd_Not( cuddE(bGR) ); + bG1 = Cudd_Not( cuddT(bGR) ); + } + else + { + bG0 = cuddE(bGR); + bG1 = cuddT(bGR); + } + } + else + bG0 = bG1 = bG; + + // solve subproblems + zRes0 = extraZddGetSymmetricVars( dd, bF0, bG0, cuddT(bVarsNew) ); + if ( zRes0 == NULL ) + return NULL; + cuddRef( zRes0 ); + + // if there is not symmetries in the negative cofactor + // there is no need to test the positive cofactor + if ( zRes0 == z0 ) + zRes = zRes0; // zRes takes reference + else + { + zRes1 = extraZddGetSymmetricVars( dd, bF1, bG1, cuddT(bVarsNew) ); + if ( zRes1 == NULL ) + { + Cudd_RecursiveDerefZdd( dd, zRes0 ); + return NULL; + } + cuddRef( zRes1 ); + + // only those variables should belong to the resulting set + // for which the property is true for both cofactors + zRes = cuddZddIntersect( dd, zRes0, zRes1 ); + if ( zRes == NULL ) + { + Cudd_RecursiveDerefZdd( dd, zRes0 ); + Cudd_RecursiveDerefZdd( dd, zRes1 ); + return NULL; + } + cuddRef( zRes ); + Cudd_RecursiveDerefZdd( dd, zRes0 ); + Cudd_RecursiveDerefZdd( dd, zRes1 ); + } + + // add one more singleton if the property is true for this variable + if ( bF0 == bG1 ) + { + zPlus = cuddZddGetNode( dd, 2*bVarsNew->index, z1, z0 ); + if ( zPlus == NULL ) + { + Cudd_RecursiveDerefZdd( dd, zRes ); + return NULL; + } + cuddRef( zPlus ); + + // add these variable pairs to the result + zRes = cuddZddUnion( dd, zTemp = zRes, zPlus ); + if ( zRes == NULL ) + { + Cudd_RecursiveDerefZdd( dd, zTemp ); + Cudd_RecursiveDerefZdd( dd, zPlus ); + return NULL; + } + cuddRef( zRes ); + Cudd_RecursiveDerefZdd( dd, zTemp ); + Cudd_RecursiveDerefZdd( dd, zPlus ); + } + + if ( bF == bG && bVars != bVarsNew ) + { + // if the functions are equal, so are their cofactors + // add those variables from V that are above F and G + + DdNode * bVarsExtra; + + assert( LevelFG > dd->perm[bVars->index] ); + + // create the BDD of the extra variables + bVarsExtra = cuddBddExistAbstractRecur( dd, bVars, bVarsNew ); + if ( bVarsExtra == NULL ) + { + Cudd_RecursiveDerefZdd( dd, zRes ); + return NULL; + } + cuddRef( bVarsExtra ); + + zPlus = extraZddGetSingletons( dd, bVarsExtra ); + if ( zPlus == NULL ) + { + Cudd_RecursiveDeref( dd, bVarsExtra ); + Cudd_RecursiveDerefZdd( dd, zRes ); + return NULL; + } + cuddRef( zPlus ); + Cudd_RecursiveDeref( dd, bVarsExtra ); + + // add these to the result + zRes = cuddZddUnion( dd, zTemp = zRes, zPlus ); + if ( zRes == NULL ) + { + Cudd_RecursiveDerefZdd( dd, zTemp ); + Cudd_RecursiveDerefZdd( dd, zPlus ); + return NULL; + } + cuddRef( zRes ); + Cudd_RecursiveDerefZdd( dd, zTemp ); + Cudd_RecursiveDerefZdd( dd, zPlus ); + } + cuddDeref( zRes ); + + cuddCacheInsert( dd, DD_GET_SYMM_VARS_TAG, bF, bG, bVars, zRes ); + return zRes; + } +} /* end of extraZddGetSymmetricVars */ + + +/**Function******************************************************************** + + Synopsis [Performs a recursive step of Extra_zddGetSingletons.] + + Description [Returns the set of ZDD singletons, containing those positive + polarity ZDD variables that correspond to the BDD variables in bVars.] + + SideEffects [] + + SeeAlso [] + +******************************************************************************/ +DdNode * extraZddGetSingletons( + DdManager * dd, /* the DD manager */ + DdNode * bVars) /* the set of variables */ +{ + DdNode * zRes; + + if ( bVars == b1 ) +// if ( bVars == b0 ) // bug fixed by Jin Zhang, Jan 23, 2004 + return z1; + + if ( zRes = cuddCacheLookup1Zdd(dd, extraZddGetSingletons, bVars) ) + return zRes; + else + { + DdNode * zTemp, * zPlus; + + // solve subproblem + zRes = extraZddGetSingletons( dd, cuddT(bVars) ); + if ( zRes == NULL ) + return NULL; + cuddRef( zRes ); + + zPlus = cuddZddGetNode( dd, 2*bVars->index, z1, z0 ); + if ( zPlus == NULL ) + { + Cudd_RecursiveDerefZdd( dd, zRes ); + return NULL; + } + cuddRef( zPlus ); + + // add these to the result + zRes = cuddZddUnion( dd, zTemp = zRes, zPlus ); + if ( zRes == NULL ) + { + Cudd_RecursiveDerefZdd( dd, zTemp ); + Cudd_RecursiveDerefZdd( dd, zPlus ); + return NULL; + } + cuddRef( zRes ); + Cudd_RecursiveDerefZdd( dd, zTemp ); + Cudd_RecursiveDerefZdd( dd, zPlus ); + cuddDeref( zRes ); + + cuddCacheInsert1( dd, extraZddGetSingletons, bVars, zRes ); + return zRes; + } +} /* end of extraZddGetSingletons */ + + +/**Function******************************************************************** + + Synopsis [Performs a recursive step of Extra_bddReduceVarSet.] + + Description [Returns the set of all variables in the given set that are not in the + support of the given function.] + + SideEffects [] + + SeeAlso [] + +******************************************************************************/ +DdNode * extraBddReduceVarSet( + DdManager * dd, /* the DD manager */ + DdNode * bVars, /* the set of variables to be reduced */ + DdNode * bF) /* the function whose support is used for reduction */ +{ + DdNode * bRes; + DdNode * bFR = Cudd_Regular(bF); + + if ( cuddIsConstant(bFR) || bVars == b1 ) + return bVars; + + if ( bRes = cuddCacheLookup2(dd, extraBddReduceVarSet, bVars, bF) ) + return bRes; + else + { + DdNode * bF0, * bF1; + DdNode * bVarsThis, * bVarsLower, * bTemp; + int LevelF; + + // if LevelF is below LevelV, scroll through the vars in bVars + LevelF = dd->perm[bFR->index]; + for ( bVarsThis = bVars; LevelF > cuddI(dd,bVarsThis->index); bVarsThis = cuddT(bVarsThis) ); + // scroll also through the current var, because it should be not be added + if ( LevelF == cuddI(dd,bVarsThis->index) ) + bVarsLower = cuddT(bVarsThis); + else + bVarsLower = bVarsThis; + + // cofactor the function + if ( bFR != bF ) // bFunc is complemented + { + bF0 = Cudd_Not( cuddE(bFR) ); + bF1 = Cudd_Not( cuddT(bFR) ); + } + else + { + bF0 = cuddE(bFR); + bF1 = cuddT(bFR); + } + + // solve subproblems + bRes = extraBddReduceVarSet( dd, bVarsLower, bF0 ); + if ( bRes == NULL ) + return NULL; + cuddRef( bRes ); + + bRes = extraBddReduceVarSet( dd, bTemp = bRes, bF1 ); + if ( bRes == NULL ) + { + Cudd_RecursiveDeref( dd, bTemp ); + return NULL; + } + cuddRef( bRes ); + Cudd_RecursiveDeref( dd, bTemp ); + + // the current var should not be added + // add the skipped vars + if ( bVarsThis != bVars ) + { + DdNode * bVarsExtra; + + // extract the skipped variables + bVarsExtra = cuddBddExistAbstractRecur( dd, bVars, bVarsThis ); + if ( bVarsExtra == NULL ) + { + Cudd_RecursiveDeref( dd, bRes ); + return NULL; + } + cuddRef( bVarsExtra ); + + // add these variables + bRes = cuddBddAndRecur( dd, bTemp = bRes, bVarsExtra ); + if ( bRes == NULL ) + { + Cudd_RecursiveDeref( dd, bTemp ); + Cudd_RecursiveDeref( dd, bVarsExtra ); + return NULL; + } + cuddRef( bRes ); + Cudd_RecursiveDeref( dd, bTemp ); + Cudd_RecursiveDeref( dd, bVarsExtra ); + } + cuddDeref( bRes ); + + cuddCacheInsert2( dd, extraBddReduceVarSet, bVars, bF, bRes ); + return bRes; + } +} /* end of extraBddReduceVarSet */ + + +/**Function******************************************************************** + + Synopsis [Performs the recursive step of Extra_bddCheckVarsSymmetric().] + + Description [Returns b0 if the variables are not symmetric. Returns b1 if the + variables can be symmetric. The variables are represented in the form of a + two-variable cube. In case the cube contains one variable (below Var1 level), + the cube's pointer is complemented if the variable Var1 occurred on the + current path; otherwise, the cube's pointer is regular. Uses additional + complemented bit (Hash_Not) to mark the result if in the BDD rooted that this + node there is a branch passing though the node labeled with Var2.] + + SideEffects [] + + SeeAlso [] + +******************************************************************************/ +DdNode * extraBddCheckVarsSymmetric( + DdManager * dd, /* the DD manager */ + DdNode * bF, + DdNode * bVars) +{ + DdNode * bRes; + + if ( bF == b0 ) + return b1; + + assert( bVars != b1 ); + + if ( bRes = cuddCacheLookup2(dd, extraBddCheckVarsSymmetric, bF, bVars) ) + return bRes; + else + { + DdNode * bRes0, * bRes1; + DdNode * bF0, * bF1; + DdNode * bFR = Cudd_Regular(bF); + int LevelF = cuddI(dd,bFR->index); + + DdNode * bVarsR = Cudd_Regular(bVars); + int fVar1Pres; + int iLev1; + int iLev2; + + if ( bVarsR != bVars ) // cube's pointer is complemented + { + assert( cuddT(bVarsR) == b1 ); + fVar1Pres = 1; // the first var is present on the path + iLev1 = -1; // we are already below the first var level + iLev2 = dd->perm[bVarsR->index]; // the level of the second var + } + else // cube's pointer is NOT complemented + { + fVar1Pres = 0; // the first var is absent on the path + if ( cuddT(bVars) == b1 ) + { + iLev1 = -1; // we are already below the first var level + iLev2 = dd->perm[bVars->index]; // the level of the second var + } + else + { + assert( cuddT(cuddT(bVars)) == b1 ); + iLev1 = dd->perm[bVars->index]; // the level of the first var + iLev2 = dd->perm[cuddT(bVars)->index]; // the level of the second var + } + } + + // cofactor the function + // the cofactors are needed only if we are above the second level + if ( LevelF < iLev2 ) + { + if ( bFR != bF ) // bFunc is complemented + { + bF0 = Cudd_Not( cuddE(bFR) ); + bF1 = Cudd_Not( cuddT(bFR) ); + } + else + { + bF0 = cuddE(bFR); + bF1 = cuddT(bFR); + } + } + else + bF0 = bF1 = NULL; + + // consider five cases: + // (1) F is above iLev1 + // (2) F is on the level iLev1 + // (3) F is between iLev1 and iLev2 + // (4) F is on the level iLev2 + // (5) F is below iLev2 + + // (1) F is above iLev1 + if ( LevelF < iLev1 ) + { + // the returned result cannot have the hash attribute + // because we still did not reach the level of Var1; + // the attribute never travels above the level of Var1 + bRes0 = extraBddCheckVarsSymmetric( dd, bF0, bVars ); +// assert( !Hash_IsComplement( bRes0 ) ); + assert( bRes0 != z0 ); + if ( bRes0 == b0 ) + bRes = b0; + else + bRes = extraBddCheckVarsSymmetric( dd, bF1, bVars ); +// assert( !Hash_IsComplement( bRes ) ); + assert( bRes != z0 ); + } + // (2) F is on the level iLev1 + else if ( LevelF == iLev1 ) + { + bRes0 = extraBddCheckVarsSymmetric( dd, bF0, Cudd_Not( cuddT(bVars) ) ); + if ( bRes0 == b0 ) + bRes = b0; + else + { + bRes1 = extraBddCheckVarsSymmetric( dd, bF1, Cudd_Not( cuddT(bVars) ) ); + if ( bRes1 == b0 ) + bRes = b0; + else + { +// if ( Hash_IsComplement( bRes0 ) || Hash_IsComplement( bRes1 ) ) + if ( bRes0 == z0 || bRes1 == z0 ) + bRes = b1; + else + bRes = b0; + } + } + } + // (3) F is between iLev1 and iLev2 + else if ( LevelF < iLev2 ) + { + bRes0 = extraBddCheckVarsSymmetric( dd, bF0, bVars ); + if ( bRes0 == b0 ) + bRes = b0; + else + { + bRes1 = extraBddCheckVarsSymmetric( dd, bF1, bVars ); + if ( bRes1 == b0 ) + bRes = b0; + else + { +// if ( Hash_IsComplement( bRes0 ) || Hash_IsComplement( bRes1 ) ) +// bRes = Hash_Not( b1 ); + if ( bRes0 == z0 || bRes1 == z0 ) + bRes = z0; + else + bRes = b1; + } + } + } + // (4) F is on the level iLev2 + else if ( LevelF == iLev2 ) + { + // this is the only place where the hash attribute (Hash_Not) can be added + // to the result; it can be added only if the path came through the node + // lebeled with Var1; therefore, the hash attribute cannot be returned + // to the caller function + if ( fVar1Pres ) +// bRes = Hash_Not( b1 ); + bRes = z0; + else + bRes = b0; + } + // (5) F is below iLev2 + else // if ( LevelF > iLev2 ) + { + // it is possible that the path goes through the node labeled by Var1 + // and still everything is okay; we do not label with Hash_Not here + // because the path does not go through node labeled by Var2 + bRes = b1; + } + + cuddCacheInsert2(dd, extraBddCheckVarsSymmetric, bF, bVars, bRes); + return bRes; + } +} /* end of extraBddCheckVarsSymmetric */ + +/**Function******************************************************************** + + Synopsis [Performs the reordering-sensitive step of Extra_zddTupleFromBdd().] + + Description [Generates in a bottom-up fashion ZDD for all combinations + composed of k variables out of variables belonging to Support.] + + SideEffects [] + + SeeAlso [] + +******************************************************************************/ +DdNode* extraZddTuplesFromBdd( + DdManager * dd, /* the DD manager */ + DdNode * bVarsK, /* the number of variables in tuples */ + DdNode * bVarsN) /* the set of all variables */ +{ + DdNode *zRes, *zRes0, *zRes1; + statLine(dd); + + /* terminal cases */ +/* if ( k < 0 || k > n ) + * return dd->zero; + * if ( n == 0 ) + * return dd->one; + */ + if ( cuddI( dd, bVarsK->index ) < cuddI( dd, bVarsN->index ) ) + return z0; + if ( bVarsN == b1 ) + return z1; + + /* check cache */ + zRes = cuddCacheLookup2Zdd(dd, extraZddTuplesFromBdd, bVarsK, bVarsN); + if (zRes) + return(zRes); + + /* ZDD in which this variable is 0 */ +/* zRes0 = extraZddTuplesFromBdd( dd, k, n-1 ); */ + zRes0 = extraZddTuplesFromBdd( dd, bVarsK, cuddT(bVarsN) ); + if ( zRes0 == NULL ) + return NULL; + cuddRef( zRes0 ); + + /* ZDD in which this variable is 1 */ +/* zRes1 = extraZddTuplesFromBdd( dd, k-1, n-1 ); */ + if ( bVarsK == b1 ) + { + zRes1 = z0; + cuddRef( zRes1 ); + } + else + { + zRes1 = extraZddTuplesFromBdd( dd, cuddT(bVarsK), cuddT(bVarsN) ); + if ( zRes1 == NULL ) + { + Cudd_RecursiveDerefZdd( dd, zRes0 ); + return NULL; + } + cuddRef( zRes1 ); + } + + /* compose Res0 and Res1 with the given ZDD variable */ + zRes = cuddZddGetNode( dd, 2*bVarsN->index, zRes1, zRes0 ); + if ( zRes == NULL ) + { + Cudd_RecursiveDerefZdd( dd, zRes0 ); + Cudd_RecursiveDerefZdd( dd, zRes1 ); + return NULL; + } + cuddDeref( zRes0 ); + cuddDeref( zRes1 ); + + /* insert the result into cache */ + cuddCacheInsert2(dd, extraZddTuplesFromBdd, bVarsK, bVarsN, zRes); + return zRes; + +} /* end of extraZddTuplesFromBdd */ + + +/**Function******************************************************************** + + Synopsis [Performs the recursive step of Extra_zddSelectOneSubset.] + + Description [] + + SideEffects [None] + + SeeAlso [] + +******************************************************************************/ +DdNode * extraZddSelectOneSubset( + DdManager * dd, + DdNode * zS ) +// selects one subset from the ZDD zS +// returns z0 if and only if zS is an empty set of cubes +{ + DdNode * zRes; + + if ( zS == z0 ) return z0; + if ( zS == z1 ) return z1; + + // check cache + if ( zRes = cuddCacheLookup1Zdd( dd, extraZddSelectOneSubset, zS ) ) + return zRes; + else + { + DdNode * zS0, * zS1, * zTemp; + + zS0 = cuddE(zS); + zS1 = cuddT(zS); + + if ( zS0 != z0 ) + { + zRes = extraZddSelectOneSubset( dd, zS0 ); + if ( zRes == NULL ) + return NULL; + } + else // if ( zS0 == z0 ) + { + assert( zS1 != z0 ); + zRes = extraZddSelectOneSubset( dd, zS1 ); + if ( zRes == NULL ) + return NULL; + cuddRef( zRes ); + + zRes = cuddZddGetNode( dd, zS->index, zTemp = zRes, z0 ); + if ( zRes == NULL ) + { + Cudd_RecursiveDerefZdd( dd, zTemp ); + return NULL; + } + cuddDeref( zTemp ); + } + + // insert the result into cache + cuddCacheInsert1( dd, extraZddSelectOneSubset, zS, zRes ); + return zRes; + } +} /* end of extraZddSelectOneSubset */ + + +/*---------------------------------------------------------------------------*/ +/* Definition of static Functions */ +/*---------------------------------------------------------------------------*/ diff --git a/src/misc/extra/extraUtilBdd.c b/src/misc/extra/extraUtilBdd.c deleted file mode 100644 index 38e3345c..00000000 --- a/src/misc/extra/extraUtilBdd.c +++ /dev/null @@ -1,1046 +0,0 @@ -/**CFile**************************************************************** - - FileName [extraUtilBdd.c] - - SystemName [ABC: Logic synthesis and verification system.] - - PackageName [extra] - - Synopsis [DD-based utilities.] - - Author [Alan Mishchenko] - - Affiliation [UC Berkeley] - - Date [Ver. 1.0. Started - June 20, 2005.] - - Revision [$Id: extraUtilBdd.c,v 1.0 2003/09/01 00:00:00 alanmi Exp $] - -***********************************************************************/ - -#include "extra.h" - -/*---------------------------------------------------------------------------*/ -/* Constant declarations */ -/*---------------------------------------------------------------------------*/ - -/*---------------------------------------------------------------------------*/ -/* Stucture declarations */ -/*---------------------------------------------------------------------------*/ - -/*---------------------------------------------------------------------------*/ -/* Type declarations */ -/*---------------------------------------------------------------------------*/ - -/*---------------------------------------------------------------------------*/ -/* Variable declarations */ -/*---------------------------------------------------------------------------*/ - -/*---------------------------------------------------------------------------*/ -/* Macro declarations */ -/*---------------------------------------------------------------------------*/ - - -/**AutomaticStart*************************************************************/ - -/*---------------------------------------------------------------------------*/ -/* Static function prototypes */ -/*---------------------------------------------------------------------------*/ - -// file "extraDdTransfer.c" -static DdNode * extraTransferPermuteRecur( DdManager * ddS, DdManager * ddD, DdNode * f, st_table * table, int * Permute ); -static DdNode * extraTransferPermute( DdManager * ddS, DdManager * ddD, DdNode * f, int * Permute ); - -// file "cuddUtils.c" -static void ddSupportStep ARGS((DdNode *f, int *support)); -static void ddClearFlag ARGS((DdNode *f)); - -/**AutomaticEnd***************************************************************/ - -/*---------------------------------------------------------------------------*/ -/* Definition of exported functions */ -/*---------------------------------------------------------------------------*/ - -/**Function******************************************************************** - - Synopsis [Convert a {A,B}DD from a manager to another with variable remapping.] - - Description [Convert a {A,B}DD from a manager to another one. The orders of the - variables in the two managers may be different. Returns a - pointer to the {A,B}DD in the destination manager if successful; NULL - otherwise. The i-th entry in the array Permute tells what is the index - of the i-th variable from the old manager in the new manager.] - - SideEffects [None] - - SeeAlso [] - -******************************************************************************/ -DdNode * Extra_TransferPermute( DdManager * ddSource, DdManager * ddDestination, DdNode * f, int * Permute ) -{ - DdNode * bRes; - do - { - ddDestination->reordered = 0; - bRes = extraTransferPermute( ddSource, ddDestination, f, Permute ); - } - while ( ddDestination->reordered == 1 ); - return ( bRes ); - -} /* end of Extra_TransferPermute */ - -/**Function******************************************************************** - - Synopsis [Transfers the BDD from one manager into another level by level.] - - Description [Transfers the BDD from one manager into another while - preserving the correspondence between variables level by level.] - - SideEffects [None] - - SeeAlso [] - -******************************************************************************/ -DdNode * Extra_TransferLevelByLevel( DdManager * ddSource, DdManager * ddDestination, DdNode * f ) -{ - DdNode * bRes; - int * pPermute; - int nMin, nMax, i; - - nMin = ddMin(ddSource->size, ddDestination->size); - nMax = ddMax(ddSource->size, ddDestination->size); - pPermute = ALLOC( int, nMax ); - // set up the variable permutation - for ( i = 0; i < nMin; i++ ) - pPermute[ ddSource->invperm[i] ] = ddDestination->invperm[i]; - if ( ddSource->size > ddDestination->size ) - { - for ( ; i < nMax; i++ ) - pPermute[ ddSource->invperm[i] ] = -1; - } - bRes = Extra_TransferPermute( ddSource, ddDestination, f, pPermute ); - FREE( pPermute ); - return bRes; -} - -/**Function******************************************************************** - - Synopsis [Remaps the function to depend on the topmost variables on the manager.] - - Description [] - - SideEffects [] - - SeeAlso [] - -******************************************************************************/ -DdNode * Extra_bddRemapUp( - DdManager * dd, - DdNode * bF ) -{ - int * pPermute; - DdNode * bSupp, * bTemp, * bRes; - int Counter; - - pPermute = ALLOC( int, dd->size ); - - // get support - bSupp = Cudd_Support( dd, bF ); Cudd_Ref( bSupp ); - - // create the variable map - // to remap the DD into the upper part of the manager - Counter = 0; - for ( bTemp = bSupp; bTemp != dd->one; bTemp = cuddT(bTemp) ) - pPermute[bTemp->index] = dd->invperm[Counter++]; - - // transfer the BDD and remap it - bRes = Cudd_bddPermute( dd, bF, pPermute ); Cudd_Ref( bRes ); - - // remove support - Cudd_RecursiveDeref( dd, bSupp ); - - // return - Cudd_Deref( bRes ); - free( pPermute ); - return bRes; -} - -/**Function******************************************************************** - - Synopsis [Moves the BDD by the given number of variables up or down.] - - Description [] - - SideEffects [] - - SeeAlso [Extra_bddShift] - -******************************************************************************/ -DdNode * Extra_bddMove( - DdManager * dd, /* the DD manager */ - DdNode * bF, - int nVars) -{ - DdNode * res; - DdNode * bVars; - if ( nVars == 0 ) - return bF; - if ( Cudd_IsConstant(bF) ) - return bF; - assert( nVars <= dd->size ); - if ( nVars > 0 ) - bVars = dd->vars[nVars]; - else - bVars = Cudd_Not(dd->vars[-nVars]); - - do { - dd->reordered = 0; - res = extraBddMove( dd, bF, bVars ); - } while (dd->reordered == 1); - return(res); - -} /* end of Extra_bddMove */ - -/**Function************************************************************* - - Synopsis [] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -void Extra_StopManager( DdManager * dd ) -{ - int RetValue; - // check for remaining references in the package - RetValue = Cudd_CheckZeroRef( dd ); - if ( RetValue > 0 ) - printf( "\nThe number of referenced nodes = %d\n\n", RetValue ); -// Cudd_PrintInfo( dd, stdout ); - Cudd_Quit( dd ); -} - -/**Function******************************************************************** - - Synopsis [Outputs the BDD in a readable format.] - - Description [] - - SideEffects [None] - - SeeAlso [] - -******************************************************************************/ -void Extra_bddPrint( DdManager * dd, DdNode * F ) -{ - DdGen * Gen; - int * Cube; - CUDD_VALUE_TYPE Value; - int nVars = dd->size; - int fFirstCube = 1; - int i; - - if ( F == NULL ) - { - printf("NULL"); - return; - } - if ( F == b0 ) - { - printf("Constant 0"); - return; - } - if ( F == b1 ) - { - printf("Constant 1"); - return; - } - - Cudd_ForeachCube( dd, F, Gen, Cube, Value ) - { - if ( fFirstCube ) - fFirstCube = 0; - else -// Output << " + "; - printf( " + " ); - - for ( i = 0; i < nVars; i++ ) - if ( Cube[i] == 0 ) - printf( "[%d]'", i ); -// printf( "%c'", (char)('a'+i) ); - else if ( Cube[i] == 1 ) - printf( "[%d]", i ); -// printf( "%c", (char)('a'+i) ); - } - -// printf("\n"); -} -/**Function******************************************************************** - - Synopsis [Returns the size of the support.] - - Description [] - - SideEffects [] - - SeeAlso [] - -******************************************************************************/ -int Extra_bddSuppSize( DdManager * dd, DdNode * bSupp ) -{ - int Counter = 0; - while ( bSupp != b1 ) - { - assert( !Cudd_IsComplement(bSupp) ); - assert( cuddE(bSupp) == b0 ); - - bSupp = cuddT(bSupp); - Counter++; - } - return Counter; -} - -/**Function******************************************************************** - - Synopsis [Returns 1 if the support contains the given BDD variable.] - - Description [] - - SideEffects [] - - SeeAlso [] - -******************************************************************************/ -int Extra_bddSuppContainVar( DdManager * dd, DdNode * bS, DdNode * bVar ) -{ - for( ; bS != b1; bS = cuddT(bS) ) - if ( bS->index == bVar->index ) - return 1; - return 0; -} - -/**Function******************************************************************** - - Synopsis [Returns 1 if two supports represented as BDD cubes are overlapping.] - - Description [] - - SideEffects [] - - SeeAlso [] - -******************************************************************************/ -int Extra_bddSuppOverlapping( DdManager * dd, DdNode * S1, DdNode * S2 ) -{ - while ( S1->index != CUDD_CONST_INDEX && S2->index != CUDD_CONST_INDEX ) - { - // if the top vars are the same, they intersect - if ( S1->index == S2->index ) - return 1; - // if the top vars are different, skip the one, which is higher - if ( dd->perm[S1->index] < dd->perm[S2->index] ) - S1 = cuddT(S1); - else - S2 = cuddT(S2); - } - return 0; -} - -/**Function******************************************************************** - - Synopsis [Returns the number of different vars in two supports.] - - Description [Counts the number of variables that appear in one support and - does not appear in other support. If the number exceeds DiffMax, returns DiffMax.] - - SideEffects [] - - SeeAlso [] - -******************************************************************************/ -int Extra_bddSuppDifferentVars( DdManager * dd, DdNode * S1, DdNode * S2, int DiffMax ) -{ - int Result = 0; - while ( S1->index != CUDD_CONST_INDEX && S2->index != CUDD_CONST_INDEX ) - { - // if the top vars are the same, this var is the same - if ( S1->index == S2->index ) - { - S1 = cuddT(S1); - S2 = cuddT(S2); - continue; - } - // the top var is different - Result++; - - if ( Result >= DiffMax ) - return DiffMax; - - // if the top vars are different, skip the one, which is higher - if ( dd->perm[S1->index] < dd->perm[S2->index] ) - S1 = cuddT(S1); - else - S2 = cuddT(S2); - } - - // consider the remaining variables - if ( S1->index != CUDD_CONST_INDEX ) - Result += Extra_bddSuppSize(dd,S1); - else if ( S2->index != CUDD_CONST_INDEX ) - Result += Extra_bddSuppSize(dd,S2); - - if ( Result >= DiffMax ) - return DiffMax; - return Result; -} - - -/**Function******************************************************************** - - Synopsis [Checks the support containment.] - - Description [This function returns 1 if one support is contained in another. - In this case, bLarge (bSmall) is assigned to point to the larger (smaller) support. - If the supports are identical, return 0 and does not assign the supports!] - - SideEffects [] - - SeeAlso [] - -******************************************************************************/ -int Extra_bddSuppCheckContainment( DdManager * dd, DdNode * bL, DdNode * bH, DdNode ** bLarge, DdNode ** bSmall ) -{ - DdNode * bSL = bL; - DdNode * bSH = bH; - int fLcontainsH = 1; - int fHcontainsL = 1; - int TopVar; - - if ( bSL == bSH ) - return 0; - - while ( bSL != b1 || bSH != b1 ) - { - if ( bSL == b1 ) - { // Low component has no vars; High components has some vars - fLcontainsH = 0; - if ( fHcontainsL == 0 ) - return 0; - else - break; - } - - if ( bSH == b1 ) - { // similarly - fHcontainsL = 0; - if ( fLcontainsH == 0 ) - return 0; - else - break; - } - - // determine the topmost var of the supports by comparing their levels - if ( dd->perm[bSL->index] < dd->perm[bSH->index] ) - TopVar = bSL->index; - else - TopVar = bSH->index; - - if ( TopVar == bSL->index && TopVar == bSH->index ) - { // they are on the same level - // it does not tell us anything about their containment - // skip this var - bSL = cuddT(bSL); - bSH = cuddT(bSH); - } - else if ( TopVar == bSL->index ) // and TopVar != bSH->index - { // Low components is higher and contains more vars - // it is not possible that High component contains Low - fHcontainsL = 0; - // skip this var - bSL = cuddT(bSL); - } - else // if ( TopVar == bSH->index ) // and TopVar != bSL->index - { // similarly - fLcontainsH = 0; - // skip this var - bSH = cuddT(bSH); - } - - // check the stopping condition - if ( !fHcontainsL && !fLcontainsH ) - return 0; - } - // only one of them can be true at the same time - assert( !fHcontainsL || !fLcontainsH ); - if ( fHcontainsL ) - { - *bLarge = bH; - *bSmall = bL; - } - else // fLcontainsH - { - *bLarge = bL; - *bSmall = bH; - } - return 1; -} - - -/**Function******************************************************************** - - Synopsis [Finds variables on which the DD depends and returns them as am array.] - - Description [Finds the variables on which the DD depends. Returns an array - with entries set to 1 for those variables that belong to the support; - NULL otherwise. The array is allocated by the user and should have at least - as many entries as the maximum number of variables in BDD and ZDD parts of - the manager.] - - SideEffects [None] - - SeeAlso [Cudd_Support Cudd_VectorSupport Cudd_ClassifySupport] - -******************************************************************************/ -int * -Extra_SupportArray( - DdManager * dd, /* manager */ - DdNode * f, /* DD whose support is sought */ - int * support ) /* array allocated by the user */ -{ - int i, size; - - /* Initialize support array for ddSupportStep. */ - size = ddMax(dd->size, dd->sizeZ); - for (i = 0; i < size; i++) - support[i] = 0; - - /* Compute support and clean up markers. */ - ddSupportStep(Cudd_Regular(f),support); - ddClearFlag(Cudd_Regular(f)); - - return(support); - -} /* end of Extra_SupportArray */ - -/**Function******************************************************************** - - Synopsis [Finds the variables on which a set of DDs depends.] - - Description [Finds the variables on which a set of DDs depends. - The set must contain either BDDs and ADDs, or ZDDs. - Returns a BDD consisting of the product of the variables if - successful; NULL otherwise.] - - SideEffects [None] - - SeeAlso [Cudd_Support Cudd_ClassifySupport] - -******************************************************************************/ -int * -Extra_VectorSupportArray( - DdManager * dd, /* manager */ - DdNode ** F, /* array of DDs whose support is sought */ - int n, /* size of the array */ - int * support ) /* array allocated by the user */ -{ - int i, size; - - /* Allocate and initialize support array for ddSupportStep. */ - size = ddMax( dd->size, dd->sizeZ ); - for ( i = 0; i < size; i++ ) - support[i] = 0; - - /* Compute support and clean up markers. */ - for ( i = 0; i < n; i++ ) - ddSupportStep( Cudd_Regular(F[i]), support ); - for ( i = 0; i < n; i++ ) - ddClearFlag( Cudd_Regular(F[i]) ); - - return support; -} - -/**Function******************************************************************** - - Synopsis [Find any cube belonging to the on-set of the function.] - - Description [] - - SideEffects [] - - SeeAlso [] - -******************************************************************************/ -DdNode * Extra_bddFindOneCube( DdManager * dd, DdNode * bF ) -{ - char * s_Temp; - DdNode * bCube, * bTemp; - int v; - - // get the vector of variables in the cube - s_Temp = ALLOC( char, dd->size ); - Cudd_bddPickOneCube( dd, bF, s_Temp ); - - // start the cube - bCube = b1; Cudd_Ref( bCube ); - for ( v = 0; v < dd->size; v++ ) - if ( s_Temp[v] == 0 ) - { -// Cube &= !s_XVars[v]; - bCube = Cudd_bddAnd( dd, bTemp = bCube, Cudd_Not(dd->vars[v]) ); Cudd_Ref( bCube ); - Cudd_RecursiveDeref( dd, bTemp ); - } - else if ( s_Temp[v] == 1 ) - { -// Cube &= s_XVars[v]; - bCube = Cudd_bddAnd( dd, bTemp = bCube, dd->vars[v] ); Cudd_Ref( bCube ); - Cudd_RecursiveDeref( dd, bTemp ); - } - Cudd_Deref(bCube); - free( s_Temp ); - return bCube; -} - -/**Function******************************************************************** - - Synopsis [Returns one cube contained in the given BDD.] - - Description [This function returns the cube with the smallest - bits-to-integer value.] - - SideEffects [] - -******************************************************************************/ -DdNode * Extra_bddGetOneCube( DdManager * dd, DdNode * bFunc ) -{ - DdNode * bFuncR, * bFunc0, * bFunc1; - DdNode * bRes0, * bRes1, * bRes; - - bFuncR = Cudd_Regular(bFunc); - if ( cuddIsConstant(bFuncR) ) - return bFunc; - - // cofactor - if ( Cudd_IsComplement(bFunc) ) - { - bFunc0 = Cudd_Not( cuddE(bFuncR) ); - bFunc1 = Cudd_Not( cuddT(bFuncR) ); - } - else - { - bFunc0 = cuddE(bFuncR); - bFunc1 = cuddT(bFuncR); - } - - // try to find the cube with the negative literal - bRes0 = Extra_bddGetOneCube( dd, bFunc0 ); Cudd_Ref( bRes0 ); - - if ( bRes0 != b0 ) - { - bRes = Cudd_bddAnd( dd, bRes0, Cudd_Not(dd->vars[bFuncR->index]) ); Cudd_Ref( bRes ); - Cudd_RecursiveDeref( dd, bRes0 ); - } - else - { - Cudd_RecursiveDeref( dd, bRes0 ); - // try to find the cube with the positive literal - bRes1 = Extra_bddGetOneCube( dd, bFunc1 ); Cudd_Ref( bRes1 ); - assert( bRes1 != b0 ); - bRes = Cudd_bddAnd( dd, bRes1, dd->vars[bFuncR->index] ); Cudd_Ref( bRes ); - Cudd_RecursiveDeref( dd, bRes1 ); - } - - Cudd_Deref( bRes ); - return bRes; -} - -/**Function******************************************************************** - - Synopsis [Performs the reordering-sensitive step of Extra_bddMove().] - - Description [] - - SideEffects [] - - SeeAlso [] - -******************************************************************************/ -DdNode * Extra_bddComputeRangeCube( DdManager * dd, int iStart, int iStop ) -{ - DdNode * bTemp, * bProd; - int i; - assert( iStart <= iStop ); - assert( iStart >= 0 && iStart <= dd->size ); - assert( iStop >= 0 && iStop <= dd->size ); - bProd = b1; Cudd_Ref( bProd ); - for ( i = iStart; i < iStop; i++ ) - { - bProd = Cudd_bddAnd( dd, bTemp = bProd, dd->vars[i] ); Cudd_Ref( bProd ); - Cudd_RecursiveDeref( dd, bTemp ); - } - Cudd_Deref( bProd ); - return bProd; -} - -/*---------------------------------------------------------------------------*/ -/* Definition of internal functions */ -/*---------------------------------------------------------------------------*/ - -/**Function******************************************************************** - - Synopsis [Performs the reordering-sensitive step of Extra_bddMove().] - - Description [] - - SideEffects [] - - SeeAlso [] - -******************************************************************************/ -DdNode * extraBddMove( - DdManager * dd, /* the DD manager */ - DdNode * bF, - DdNode * bDist) -{ - DdNode * bRes; - - if ( Cudd_IsConstant(bF) ) - return bF; - - if ( bRes = cuddCacheLookup2(dd, extraBddMove, bF, bDist) ) - return bRes; - else - { - DdNode * bRes0, * bRes1; - DdNode * bF0, * bF1; - DdNode * bFR = Cudd_Regular(bF); - int VarNew; - - if ( Cudd_IsComplement(bDist) ) - VarNew = bFR->index - Cudd_Not(bDist)->index; - else - VarNew = bFR->index + bDist->index; - assert( VarNew < dd->size ); - - // cofactor the functions - if ( bFR != bF ) // bFunc is complemented - { - bF0 = Cudd_Not( cuddE(bFR) ); - bF1 = Cudd_Not( cuddT(bFR) ); - } - else - { - bF0 = cuddE(bFR); - bF1 = cuddT(bFR); - } - - bRes0 = extraBddMove( dd, bF0, bDist ); - if ( bRes0 == NULL ) - return NULL; - cuddRef( bRes0 ); - - bRes1 = extraBddMove( dd, bF1, bDist ); - if ( bRes1 == NULL ) - { - Cudd_RecursiveDeref( dd, bRes0 ); - return NULL; - } - cuddRef( bRes1 ); - - /* only bRes0 and bRes1 are referenced at this point */ - bRes = cuddBddIteRecur( dd, dd->vars[VarNew], bRes1, bRes0 ); - if ( bRes == NULL ) - { - Cudd_RecursiveDeref( dd, bRes0 ); - Cudd_RecursiveDeref( dd, bRes1 ); - return NULL; - } - cuddRef( bRes ); - Cudd_RecursiveDeref( dd, bRes0 ); - Cudd_RecursiveDeref( dd, bRes1 ); - - /* insert the result into cache */ - cuddCacheInsert2( dd, extraBddMove, bF, bDist, bRes ); - cuddDeref( bRes ); - return bRes; - } -} /* end of extraBddMove */ - - -/**Function******************************************************************** - - Synopsis [Finds three cofactors of the cover w.r.t. to the topmost variable.] - - Description [Finds three cofactors of the cover w.r.t. to the topmost variable. - Does not check the cover for being a constant. Assumes that ZDD variables encoding - positive and negative polarities are adjacent in the variable order. Is different - from cuddZddGetCofactors3() in that it does not compute the cofactors w.r.t. the - given variable but takes the cofactors with respent to the topmost variable. - This function is more efficient when used in recursive procedures because it does - not require referencing of the resulting cofactors (compare cuddZddProduct() - and extraZddPrimeProduct()).] - - SideEffects [None] - - SeeAlso [cuddZddGetCofactors3] - -******************************************************************************/ -void -extraDecomposeCover( - DdManager* dd, /* the manager */ - DdNode* zC, /* the cover */ - DdNode** zC0, /* the pointer to the negative var cofactor */ - DdNode** zC1, /* the pointer to the positive var cofactor */ - DdNode** zC2 ) /* the pointer to the cofactor without var */ -{ - if ( (zC->index & 1) == 0 ) - { /* the top variable is present in positive polarity and maybe in negative */ - - DdNode *Temp = cuddE( zC ); - *zC1 = cuddT( zC ); - if ( cuddIZ(dd,Temp->index) == cuddIZ(dd,zC->index) + 1 ) - { /* Temp is not a terminal node - * top var is present in negative polarity */ - *zC2 = cuddE( Temp ); - *zC0 = cuddT( Temp ); - } - else - { /* top var is not present in negative polarity */ - *zC2 = Temp; - *zC0 = dd->zero; - } - } - else - { /* the top variable is present only in negative */ - *zC1 = dd->zero; - *zC2 = cuddE( zC ); - *zC0 = cuddT( zC ); - } -} /* extraDecomposeCover */ - -/*---------------------------------------------------------------------------*/ -/* Definition of static Functions */ -/*---------------------------------------------------------------------------*/ - -/**Function******************************************************************** - - Synopsis [Convert a BDD from a manager to another one.] - - Description [Convert a BDD from a manager to another one. Returns a - pointer to the BDD in the destination manager if successful; NULL - otherwise.] - - SideEffects [None] - - SeeAlso [Extra_TransferPermute] - -******************************************************************************/ -DdNode * extraTransferPermute( DdManager * ddS, DdManager * ddD, DdNode * f, int * Permute ) -{ - DdNode *res; - st_table *table = NULL; - st_generator *gen = NULL; - DdNode *key, *value; - - table = st_init_table( st_ptrcmp, st_ptrhash ); - if ( table == NULL ) - goto failure; - res = extraTransferPermuteRecur( ddS, ddD, f, table, Permute ); - if ( res != NULL ) - cuddRef( res ); - - /* Dereference all elements in the table and dispose of the table. - ** This must be done also if res is NULL to avoid leaks in case of - ** reordering. */ - gen = st_init_gen( table ); - if ( gen == NULL ) - goto failure; - while ( st_gen( gen, ( char ** ) &key, ( char ** ) &value ) ) - { - Cudd_RecursiveDeref( ddD, value ); - } - st_free_gen( gen ); - gen = NULL; - st_free_table( table ); - table = NULL; - - if ( res != NULL ) - cuddDeref( res ); - return ( res ); - - failure: - if ( table != NULL ) - st_free_table( table ); - if ( gen != NULL ) - st_free_gen( gen ); - return ( NULL ); - -} /* end of extraTransferPermute */ - - -/**Function******************************************************************** - - Synopsis [Performs the recursive step of Extra_TransferPermute.] - - Description [Performs the recursive step of Extra_TransferPermute. - Returns a pointer to the result if successful; NULL otherwise.] - - SideEffects [None] - - SeeAlso [extraTransferPermute] - -******************************************************************************/ -static DdNode * -extraTransferPermuteRecur( - DdManager * ddS, - DdManager * ddD, - DdNode * f, - st_table * table, - int * Permute ) -{ - DdNode *ft, *fe, *t, *e, *var, *res; - DdNode *one, *zero; - int index; - int comple = 0; - - statLine( ddD ); - one = DD_ONE( ddD ); - comple = Cudd_IsComplement( f ); - - /* Trivial cases. */ - if ( Cudd_IsConstant( f ) ) - return ( Cudd_NotCond( one, comple ) ); - - - /* Make canonical to increase the utilization of the cache. */ - f = Cudd_NotCond( f, comple ); - /* Now f is a regular pointer to a non-constant node. */ - - /* Check the cache. */ - if ( st_lookup( table, ( char * ) f, ( char ** ) &res ) ) - return ( Cudd_NotCond( res, comple ) ); - - /* Recursive step. */ - if ( Permute ) - index = Permute[f->index]; - else - index = f->index; - - ft = cuddT( f ); - fe = cuddE( f ); - - t = extraTransferPermuteRecur( ddS, ddD, ft, table, Permute ); - if ( t == NULL ) - { - return ( NULL ); - } - cuddRef( t ); - - e = extraTransferPermuteRecur( ddS, ddD, fe, table, Permute ); - if ( e == NULL ) - { - Cudd_RecursiveDeref( ddD, t ); - return ( NULL ); - } - cuddRef( e ); - - zero = Cudd_Not(ddD->one); - var = cuddUniqueInter( ddD, index, one, zero ); - if ( var == NULL ) - { - Cudd_RecursiveDeref( ddD, t ); - Cudd_RecursiveDeref( ddD, e ); - return ( NULL ); - } - res = cuddBddIteRecur( ddD, var, t, e ); - - if ( res == NULL ) - { - Cudd_RecursiveDeref( ddD, t ); - Cudd_RecursiveDeref( ddD, e ); - return ( NULL ); - } - cuddRef( res ); - Cudd_RecursiveDeref( ddD, t ); - Cudd_RecursiveDeref( ddD, e ); - - if ( st_add_direct( table, ( char * ) f, ( char * ) res ) == - ST_OUT_OF_MEM ) - { - Cudd_RecursiveDeref( ddD, res ); - return ( NULL ); - } - return ( Cudd_NotCond( res, comple ) ); - -} /* end of extraTransferPermuteRecur */ - -/**Function******************************************************************** - - Synopsis [Performs the recursive step of Cudd_Support.] - - Description [Performs the recursive step of Cudd_Support. Performs a - DFS from f. The support is accumulated in supp as a side effect. Uses - the LSB of the then pointer as visited flag.] - - SideEffects [None] - - SeeAlso [ddClearFlag] - -******************************************************************************/ -static void -ddSupportStep( - DdNode * f, - int * support) -{ - if (cuddIsConstant(f) || Cudd_IsComplement(f->next)) { - return; - } - - support[f->index] = 1; - ddSupportStep(cuddT(f),support); - ddSupportStep(Cudd_Regular(cuddE(f)),support); - /* Mark as visited. */ - f->next = Cudd_Not(f->next); - return; - -} /* end of ddSupportStep */ - - -/**Function******************************************************************** - - Synopsis [Performs a DFS from f, clearing the LSB of the next - pointers.] - - Description [] - - SideEffects [None] - - SeeAlso [ddSupportStep ddDagInt] - -******************************************************************************/ -static void -ddClearFlag( - DdNode * f) -{ - if (!Cudd_IsComplement(f->next)) { - return; - } - /* Clear visited flag. */ - f->next = Cudd_Regular(f->next); - if (cuddIsConstant(f)) { - return; - } - ddClearFlag(cuddT(f)); - ddClearFlag(Cudd_Regular(cuddE(f))); - return; - -} /* end of ddClearFlag */ - - -//////////////////////////////////////////////////////////////////////// -/// END OF FILE /// -//////////////////////////////////////////////////////////////////////// - - diff --git a/src/misc/extra/extraUtilReader.c b/src/misc/extra/extraUtilReader.c index 2dc597bf..042dfaca 100644 --- a/src/misc/extra/extraUtilReader.c +++ b/src/misc/extra/extraUtilReader.c @@ -321,6 +321,7 @@ void * Extra_FileReaderGetTokens_int( Extra_FileReader_t * p ) // through EXTRA_OFFSET_SIZE chars till the end of the buffer if ( p->pBufferStop == p->pBufferEnd ) // end of file { + *pChar = 0; p->fStop = 1; return p->vTokens; } diff --git a/src/misc/extra/module.make b/src/misc/extra/module.make index 3098a23c..6cbf5d2c 100644 --- a/src/misc/extra/module.make +++ b/src/misc/extra/module.make @@ -1,4 +1,5 @@ -SRC += src/misc/extra/extraUtilBdd.c \ +SRC += src/misc/extra/extraBddMisc.c \ + src/misc/extra/extraBddSymm.c \ src/misc/extra/extraUtilBitMatrix.c \ src/misc/extra/extraUtilCanon.c \ src/misc/extra/extraUtilFile.c \ diff --git a/src/misc/vec/vecVec.h b/src/misc/vec/vecVec.h index bb911bfe..af7ca571 100644 --- a/src/misc/vec/vecVec.h +++ b/src/misc/vec/vecVec.h @@ -52,7 +52,7 @@ struct Vec_Vec_t_ #define Vec_VecForEachLevel( vGlob, vVec, i ) \ for ( i = 0; (i < Vec_VecSize(vGlob)) && (((vVec) = Vec_VecEntry(vGlob, i)), 1); i++ ) #define Vec_VecForEachLevelStart( vGlob, vVec, i, LevelStart ) \ - for ( i = LevelStart; (i < Vec_PtrSize(vGlob)) && (((vVec) = Vec_VecEntry(vGlob, i)), 1); i++ ) + for ( i = LevelStart; (i < Vec_VecSize(vGlob)) && (((vVec) = Vec_VecEntry(vGlob, i)), 1); i++ ) #define Vec_VecForEachLevelStartStop( vGlob, vVec, i, LevelStart, LevelStop ) \ for ( i = LevelStart; (i <= LevelStop) && (((vVec) = Vec_VecEntry(vGlob, i)), 1); i++ ) #define Vec_VecForEachLevelReverse( vGlob, vVec, i ) \ @@ -234,6 +234,25 @@ static inline void Vec_VecPush( Vec_Vec_t * p, int Level, void * Entry ) Vec_PtrPush( p->pArray[Level], Entry ); } +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +static inline void Vec_VecPushUnique( Vec_Vec_t * p, int Level, void * Entry ) +{ + if ( p->nSize < Level + 1 ) + Vec_VecPush( p, Level, Entry ); + else + Vec_PtrPushUnique( p->pArray[Level], Entry ); +} + //////////////////////////////////////////////////////////////////////// /// END OF FILE /// //////////////////////////////////////////////////////////////////////// -- cgit v1.2.3