summaryrefslogtreecommitdiffstats
diff options
context:
space:
mode:
authorAlan Mishchenko <alanmi@berkeley.edu>2007-02-06 08:01:00 -0800
committerAlan Mishchenko <alanmi@berkeley.edu>2007-02-06 08:01:00 -0800
commita13c64a5b4164b5a10943c0d5283260252be30d0 (patch)
tree790d3d526396ef0ea7f00dddb99283e73e94e00e
parent8da52b6f202444711da6b1f1baac92e0a516c8e6 (diff)
downloadabc-a13c64a5b4164b5a10943c0d5283260252be30d0.tar.gz
abc-a13c64a5b4164b5a10943c0d5283260252be30d0.tar.bz2
abc-a13c64a5b4164b5a10943c0d5283260252be30d0.zip
Version abc70206
Diffstat
-rw-r--r--abc.dsp12
-rw-r--r--abc.plg25
-rw-r--r--abclib.plg903
-rw-r--r--abctestlib.plg35
-rw-r--r--src/base/abc/abc.h10
-rw-r--r--src/base/abc/abcHie.c309
-rw-r--r--src/base/abc/abcNetlist.c160
-rw-r--r--src/base/abc/abcObj.c4
-rw-r--r--src/base/abci/abc.c21
-rw-r--r--src/base/io/ioReadBlifMv.c4
-rw-r--r--src/misc/extra/extra.h4
-rw-r--r--src/opt/bdc/bdc.h6
-rw-r--r--src/opt/bdc/bdcCore.c92
-rw-r--r--src/opt/bdc/bdcDec.c415
-rw-r--r--src/opt/bdc/bdcInt.h62
-rw-r--r--src/opt/bdc/bdcTable.c140
-rw-r--r--src/opt/bdc/bdc_.c1
-rw-r--r--src/opt/kit/kit.h20
-rw-r--r--src/opt/kit/kitTruth.c150
-rw-r--r--src/opt/res/res.h2
-rw-r--r--src/opt/res/resCore.c102
-rw-r--r--src/opt/res/resDivs.c10
-rw-r--r--src/opt/res/resFilter.c147
-rw-r--r--src/opt/res/resInt.h16
-rw-r--r--src/opt/res/resSat.c163
-rw-r--r--src/opt/res/resSim.c505
-rw-r--r--src/opt/res/resSim_old.c521
-rw-r--r--src/opt/res/resWin.c13
-rw-r--r--src/sat/bsat/satSolver.c8
-rw-r--r--src/sat/bsat/satSolver.h2
30 files changed, 3445 insertions, 417 deletions
diff --git a/abc.dsp b/abc.dsp
index 62245a6d..e8fa05ad 100644
--- a/abc.dsp
+++ b/abc.dsp
@@ -1706,8 +1706,20 @@ SOURCE=.\src\opt\bdc\bdc.h
# End Source File
# Begin Source File
+SOURCE=.\src\opt\bdc\bdcCore.c
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\opt\bdc\bdcDec.c
+# End Source File
+# Begin Source File
+
SOURCE=.\src\opt\bdc\bdcInt.h
# End Source File
+# Begin Source File
+
+SOURCE=.\src\opt\bdc\bdcTable.c
+# End Source File
# End Group
# End Group
# Begin Group "map"
diff --git a/abc.plg b/abc.plg
new file mode 100644
index 00000000..6cb57990
--- /dev/null
+++ b/abc.plg
@@ -0,0 +1,25 @@
+<html>
+<body>
+<pre>
+<h1>Build Log</h1>
+<h3>
+--------------------Configuration: abc - Win32 Debug--------------------
+</h3>
+<h3>Command Lines</h3>
+Creating temporary file "C:\DOCUME~1\alanmi\LOCALS~1\Temp\RSP83C.tmp" with contents
+[
+/nologo /MLd /W3 /Gm /GX /ZI /Od /I "src\base\abc" /I "src\base\abci" /I "src\base\abcs" /I "src\base\seq" /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\ft" /I "src\sat\asat" /I "src\sat\bsat" /I "src\sat\msat" /I "src\sat\fraig" /I "src\opt\cut" /I "src\opt\dec" /I "src\opt\fxu" /I "src\opt\sim" /I "src\opt\rwr" /I "src\opt\kit" /I "src\opt\res" /I "src\map\fpga" /I "src\map\if" /I "src\map\mapper" /I "src\map\mio" /I "src\map\super" /I "src\misc\extra" /I "src\misc\st" /I "src\misc\mvc" /I "src\misc\util" /I "src\misc\npn" /I "src\misc\vec" /I "src\misc\espresso" /I "src\misc\nm" /I "src\misc\hash" /I "src\aig\ivy" /I "src\aig\hop" /I "src\aig\rwt" /I "src\aig\deco" /I "src\aig\mem" /I "src\temp\esop" /D "WIN32" /D "_DEBUG" /D "_CONSOLE" /D "_MBCS" /D "__STDC__" /FR"Debug/" /Fp"Debug/abc.pch" /YX /Fo"Debug/" /Fd"Debug/" /FD /GZ /c
+"C:\_projects\abc\src\base\abc\abcObj.c"
+]
+Creating command line "cl.exe @C:\DOCUME~1\alanmi\LOCALS~1\Temp\RSP83C.tmp"
+<h3>Output Window</h3>
+Compiling...
+abcObj.c
+
+
+
+<h3>Results</h3>
+abcObj.obj - 0 error(s), 0 warning(s)
+</pre>
+</body>
+</html>
diff --git a/abclib.plg b/abclib.plg
new file mode 100644
index 00000000..11a53466
--- /dev/null
+++ b/abclib.plg
@@ -0,0 +1,903 @@
+<html>
+<body>
+<pre>
+<h1>Build Log</h1>
+<h3>
+--------------------Configuration: abclib - Win32 Debug--------------------
+</h3>
+<h3>Command Lines</h3>
+Creating temporary file "C:\DOCUME~1\alanmi\LOCALS~1\Temp\RSP137A.tmp" with contents
+[
+/nologo /MLd /W3 /Gm /GX /ZI /Od /I "src\base\abc" /I "src\base\abci" /I "src\base\abcs" /I "src\base\seq" /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\ft" /I "src\sat\asat" /I "src\sat\bsat" /I "src\sat\msat" /I "src\sat\fraig" /I "src\opt\cut" /I "src\opt\dec" /I "src\opt\fxu" /I "src\opt\sim" /I "src\opt\rwr" /I "src\opt\kit" /I "src\map\fpga" /I "src\map\if" /I "src\map\mapper" /I "src\map\mio" /I "src\map\super" /I "src\misc\extra" /I "src\misc\st" /I "src\misc\mvc" /I "src\misc\util" /I "src\misc\npn" /I "src\misc\vec" /I "src\misc\espresso" /I "src\misc\nm" /I "src\misc\hash" /I "src\aig\ivy" /I "src\aig\hop" /I "src\aig\rwt" /I "src\aig\deco" /I "src\aig\mem" /I "src\temp\esop" /D "WIN32" /D "_DEBUG" /D "_MBCS" /D "_LIB" /D "__STDC__" /D "HAVE_ASSERT_H" /FR"abclib\DebugLib/" /Fp"abclib\DebugLib/abclib.pch" /YX /Fo"abclib\DebugLib/" /Fd"abclib\DebugLib/" /FD /GZ /c
+"C:\_projects\abc\src\sat\asat\jfront.c"
+]
+Creating command line "cl.exe @C:\DOCUME~1\alanmi\LOCALS~1\Temp\RSP137A.tmp"
+Creating temporary file "C:\DOCUME~1\alanmi\LOCALS~1\Temp\RSP137B.tmp" with contents
+[
+/nologo /out:"abclib\abclib_debug.lib"
+.\abclib\DebugLib\abcAig.obj
+.\abclib\DebugLib\abcCheck.obj
+.\abclib\DebugLib\abcDfs.obj
+.\abclib\DebugLib\abcFanio.obj
+.\abclib\DebugLib\abcFunc.obj
+.\abclib\DebugLib\abcLatch.obj
+.\abclib\DebugLib\abcLib.obj
+.\abclib\DebugLib\abcMinBase.obj
+.\abclib\DebugLib\abcNames.obj
+.\abclib\DebugLib\abcNetlist.obj
+.\abclib\DebugLib\abcNtk.obj
+.\abclib\DebugLib\abcObj.obj
+.\abclib\DebugLib\abcRefs.obj
+.\abclib\DebugLib\abcShow.obj
+.\abclib\DebugLib\abcSop.obj
+.\abclib\DebugLib\abcUtil.obj
+.\abclib\DebugLib\abc.obj
+.\abclib\DebugLib\abcAttach.obj
+.\abclib\DebugLib\abcAuto.obj
+.\abclib\DebugLib\abcBalance.obj
+.\abclib\DebugLib\abcBmc.obj
+.\abclib\DebugLib\abcClpBdd.obj
+.\abclib\DebugLib\abcClpSop.obj
+.\abclib\DebugLib\abcCut.obj
+.\abclib\DebugLib\abcDebug.obj
+.\abclib\DebugLib\abcDress.obj
+.\abclib\DebugLib\abcDsd.obj
+.\abclib\DebugLib\abcEspresso.obj
+.\abclib\DebugLib\abcExtract.obj
+.\abclib\DebugLib\abcFpga.obj
+.\abclib\DebugLib\abcFpgaFast.obj
+.\abclib\DebugLib\abcFraig.obj
+.\abclib\DebugLib\abcFxu.obj
+.\abclib\DebugLib\abcGen.obj
+.\abclib\DebugLib\abcIf.obj
+.\abclib\DebugLib\abcIvy.obj
+.\abclib\DebugLib\abcLut.obj
+.\abclib\DebugLib\abcMap.obj
+.\abclib\DebugLib\abcMini.obj
+.\abclib\DebugLib\abcMiter.obj
+.\abclib\DebugLib\abcMulti.obj
+.\abclib\DebugLib\abcMv.obj
+.\abclib\DebugLib\abcNtbdd.obj
+.\abclib\DebugLib\abcOrder.obj
+.\abclib\DebugLib\abcPrint.obj
+.\abclib\DebugLib\abcProve.obj
+.\abclib\DebugLib\abcReconv.obj
+.\abclib\DebugLib\abcRefactor.obj
+.\abclib\DebugLib\abcRenode.obj
+.\abclib\DebugLib\abcReorder.obj
+.\abclib\DebugLib\abcRestruct.obj
+.\abclib\DebugLib\abcResub.obj
+.\abclib\DebugLib\abcRewrite.obj
+.\abclib\DebugLib\abcRr.obj
+.\abclib\DebugLib\abcSat.obj
+.\abclib\DebugLib\abcStrash.obj
+.\abclib\DebugLib\abcSweep.obj
+.\abclib\DebugLib\abcSymm.obj
+.\abclib\DebugLib\abcTiming.obj
+.\abclib\DebugLib\abcUnate.obj
+.\abclib\DebugLib\abcUnreach.obj
+.\abclib\DebugLib\abcVerify.obj
+.\abclib\DebugLib\abcXsim.obj
+.\abclib\DebugLib\cmd.obj
+.\abclib\DebugLib\cmdAlias.obj
+.\abclib\DebugLib\cmdApi.obj
+.\abclib\DebugLib\cmdFlag.obj
+.\abclib\DebugLib\cmdHist.obj
+.\abclib\DebugLib\cmdUtils.obj
+.\abclib\DebugLib\io.obj
+.\abclib\DebugLib\ioReadAiger.obj
+.\abclib\DebugLib\ioReadBaf.obj
+.\abclib\DebugLib\ioReadBench.obj
+.\abclib\DebugLib\ioReadBlif.obj
+.\abclib\DebugLib\ioReadBlifAig.obj
+.\abclib\DebugLib\ioReadEdif.obj
+.\abclib\DebugLib\ioReadEqn.obj
+.\abclib\DebugLib\ioReadPla.obj
+.\abclib\DebugLib\ioUtil.obj
+.\abclib\DebugLib\ioWriteAiger.obj
+.\abclib\DebugLib\ioWriteBaf.obj
+.\abclib\DebugLib\ioWriteBench.obj
+.\abclib\DebugLib\ioWriteBlif.obj
+.\abclib\DebugLib\ioWriteCnf.obj
+.\abclib\DebugLib\ioWriteDot.obj
+.\abclib\DebugLib\ioWriteEqn.obj
+.\abclib\DebugLib\ioWriteGml.obj
+.\abclib\DebugLib\ioWriteList.obj
+.\abclib\DebugLib\ioWritePla.obj
+.\abclib\DebugLib\ioWriteVer.obj
+.\abclib\DebugLib\ioWriteVerAux.obj
+.\abclib\DebugLib\libSupport.obj
+.\abclib\DebugLib\main.obj
+.\abclib\DebugLib\mainFrame.obj
+.\abclib\DebugLib\mainInit.obj
+.\abclib\DebugLib\mainUtils.obj
+.\abclib\DebugLib\verCore.obj
+.\abclib\DebugLib\verFormula.obj
+.\abclib\DebugLib\verParse.obj
+.\abclib\DebugLib\verStream.obj
+.\abclib\DebugLib\verWords.obj
+.\abclib\DebugLib\cuddAddAbs.obj
+.\abclib\DebugLib\cuddAddApply.obj
+.\abclib\DebugLib\cuddAddFind.obj
+.\abclib\DebugLib\cuddAddInv.obj
+.\abclib\DebugLib\cuddAddIte.obj
+.\abclib\DebugLib\cuddAddNeg.obj
+.\abclib\DebugLib\cuddAddWalsh.obj
+.\abclib\DebugLib\cuddAndAbs.obj
+.\abclib\DebugLib\cuddAnneal.obj
+.\abclib\DebugLib\cuddApa.obj
+.\abclib\DebugLib\cuddAPI.obj
+.\abclib\DebugLib\cuddApprox.obj
+.\abclib\DebugLib\cuddBddAbs.obj
+.\abclib\DebugLib\cuddBddCorr.obj
+.\abclib\DebugLib\cuddBddIte.obj
+.\abclib\DebugLib\cuddBridge.obj
+.\abclib\DebugLib\cuddCache.obj
+.\abclib\DebugLib\cuddCheck.obj
+.\abclib\DebugLib\cuddClip.obj
+.\abclib\DebugLib\cuddCof.obj
+.\abclib\DebugLib\cuddCompose.obj
+.\abclib\DebugLib\cuddDecomp.obj
+.\abclib\DebugLib\cuddEssent.obj
+.\abclib\DebugLib\cuddExact.obj
+.\abclib\DebugLib\cuddExport.obj
+.\abclib\DebugLib\cuddGenCof.obj
+.\abclib\DebugLib\cuddGenetic.obj
+.\abclib\DebugLib\cuddGroup.obj
+.\abclib\DebugLib\cuddHarwell.obj
+.\abclib\DebugLib\cuddInit.obj
+.\abclib\DebugLib\cuddInteract.obj
+.\abclib\DebugLib\cuddLCache.obj
+.\abclib\DebugLib\cuddLevelQ.obj
+.\abclib\DebugLib\cuddLinear.obj
+.\abclib\DebugLib\cuddLiteral.obj
+.\abclib\DebugLib\cuddMatMult.obj
+.\abclib\DebugLib\cuddPriority.obj
+.\abclib\DebugLib\cuddRead.obj
+.\abclib\DebugLib\cuddRef.obj
+.\abclib\DebugLib\cuddReorder.obj
+.\abclib\DebugLib\cuddSat.obj
+.\abclib\DebugLib\cuddSign.obj
+.\abclib\DebugLib\cuddSolve.obj
+.\abclib\DebugLib\cuddSplit.obj
+.\abclib\DebugLib\cuddSubsetHB.obj
+.\abclib\DebugLib\cuddSubsetSP.obj
+.\abclib\DebugLib\cuddSymmetry.obj
+.\abclib\DebugLib\cuddTable.obj
+.\abclib\DebugLib\cuddUtil.obj
+.\abclib\DebugLib\cuddWindow.obj
+.\abclib\DebugLib\cuddZddCount.obj
+.\abclib\DebugLib\cuddZddFuncs.obj
+.\abclib\DebugLib\cuddZddGroup.obj
+.\abclib\DebugLib\cuddZddIsop.obj
+.\abclib\DebugLib\cuddZddLin.obj
+.\abclib\DebugLib\cuddZddMisc.obj
+.\abclib\DebugLib\cuddZddPort.obj
+.\abclib\DebugLib\cuddZddReord.obj
+.\abclib\DebugLib\cuddZddSetop.obj
+.\abclib\DebugLib\cuddZddSymm.obj
+.\abclib\DebugLib\cuddZddUtil.obj
+.\abclib\DebugLib\epd.obj
+.\abclib\DebugLib\mtrBasic.obj
+.\abclib\DebugLib\mtrGroup.obj
+.\abclib\DebugLib\parseCore.obj
+.\abclib\DebugLib\parseEqn.obj
+.\abclib\DebugLib\parseStack.obj
+.\abclib\DebugLib\dsdApi.obj
+.\abclib\DebugLib\dsdCheck.obj
+.\abclib\DebugLib\dsdLocal.obj
+.\abclib\DebugLib\dsdMan.obj
+.\abclib\DebugLib\dsdProc.obj
+.\abclib\DebugLib\dsdTree.obj
+.\abclib\DebugLib\reoApi.obj
+.\abclib\DebugLib\reoCore.obj
+.\abclib\DebugLib\reoProfile.obj
+.\abclib\DebugLib\reoSift.obj
+.\abclib\DebugLib\reoSwap.obj
+.\abclib\DebugLib\reoTest.obj
+.\abclib\DebugLib\reoTransfer.obj
+.\abclib\DebugLib\reoUnits.obj
+.\abclib\DebugLib\added.obj
+.\abclib\DebugLib\asatmem.obj
+.\abclib\DebugLib\solver.obj
+.\abclib\DebugLib\msatActivity.obj
+.\abclib\DebugLib\msatClause.obj
+.\abclib\DebugLib\msatClauseVec.obj
+.\abclib\DebugLib\msatMem.obj
+.\abclib\DebugLib\msatOrderH.obj
+.\abclib\DebugLib\msatQueue.obj
+.\abclib\DebugLib\msatRead.obj
+.\abclib\DebugLib\msatSolverApi.obj
+.\abclib\DebugLib\msatSolverCore.obj
+.\abclib\DebugLib\msatSolverIo.obj
+.\abclib\DebugLib\msatSolverSearch.obj
+.\abclib\DebugLib\msatSort.obj
+.\abclib\DebugLib\msatVec.obj
+.\abclib\DebugLib\fraigApi.obj
+.\abclib\DebugLib\fraigCanon.obj
+.\abclib\DebugLib\fraigChoice.obj
+.\abclib\DebugLib\fraigFanout.obj
+.\abclib\DebugLib\fraigFeed.obj
+.\abclib\DebugLib\fraigMan.obj
+.\abclib\DebugLib\fraigMem.obj
+.\abclib\DebugLib\fraigNode.obj
+.\abclib\DebugLib\fraigPrime.obj
+.\abclib\DebugLib\fraigSat.obj
+.\abclib\DebugLib\fraigTable.obj
+.\abclib\DebugLib\fraigUtil.obj
+.\abclib\DebugLib\fraigVec.obj
+.\abclib\DebugLib\csat_apis.obj
+.\abclib\DebugLib\satMem.obj
+.\abclib\DebugLib\satSolver.obj
+.\abclib\DebugLib\satUtil.obj
+.\abclib\DebugLib\fxu.obj
+.\abclib\DebugLib\fxuCreate.obj
+.\abclib\DebugLib\fxuHeapD.obj
+.\abclib\DebugLib\fxuHeapS.obj
+.\abclib\DebugLib\fxuList.obj
+.\abclib\DebugLib\fxuMatrix.obj
+.\abclib\DebugLib\fxuPair.obj
+.\abclib\DebugLib\fxuPrint.obj
+.\abclib\DebugLib\fxuReduce.obj
+.\abclib\DebugLib\fxuSelect.obj
+.\abclib\DebugLib\fxuSingle.obj
+.\abclib\DebugLib\fxuUpdate.obj
+.\abclib\DebugLib\rwrDec.obj
+.\abclib\DebugLib\rwrEva.obj
+.\abclib\DebugLib\rwrExp.obj
+.\abclib\DebugLib\rwrLib.obj
+.\abclib\DebugLib\rwrMan.obj
+.\abclib\DebugLib\rwrPrint.obj
+.\abclib\DebugLib\rwrTemp.obj
+.\abclib\DebugLib\rwrUtil.obj
+.\abclib\DebugLib\cutApi.obj
+.\abclib\DebugLib\cutCut.obj
+.\abclib\DebugLib\cutExpand.obj
+.\abclib\DebugLib\cutMan.obj
+.\abclib\DebugLib\cutMerge.obj
+.\abclib\DebugLib\cutNode.obj
+.\abclib\DebugLib\cutOracle.obj
+.\abclib\DebugLib\cutPre22.obj
+.\abclib\DebugLib\cutSeq.obj
+.\abclib\DebugLib\cutTruth.obj
+.\abclib\DebugLib\decAbc.obj
+.\abclib\DebugLib\decFactor.obj
+.\abclib\DebugLib\decMan.obj
+.\abclib\DebugLib\decPrint.obj
+.\abclib\DebugLib\decUtil.obj
+.\abclib\DebugLib\simMan.obj
+.\abclib\DebugLib\simSat.obj
+.\abclib\DebugLib\simSeq.obj
+.\abclib\DebugLib\simSupp.obj
+.\abclib\DebugLib\simSwitch.obj
+.\abclib\DebugLib\simSym.obj
+.\abclib\DebugLib\simSymSat.obj
+.\abclib\DebugLib\simSymSim.obj
+.\abclib\DebugLib\simSymStr.obj
+.\abclib\DebugLib\simUtils.obj
+.\abclib\DebugLib\retArea.obj
+.\abclib\DebugLib\retCore.obj
+.\abclib\DebugLib\retDelay.obj
+.\abclib\DebugLib\retFlow.obj
+.\abclib\DebugLib\retIncrem.obj
+.\abclib\DebugLib\retInit.obj
+.\abclib\DebugLib\retLvalue.obj
+.\abclib\DebugLib\kitBdd.obj
+.\abclib\DebugLib\kitFactor.obj
+.\abclib\DebugLib\kitGraph.obj
+.\abclib\DebugLib\kitHop.obj
+.\abclib\DebugLib\kitIsop.obj
+.\abclib\DebugLib\kitSop.obj
+.\abclib\DebugLib\kitTruth.obj
+.\abclib\DebugLib\fpga.obj
+.\abclib\DebugLib\fpgaCore.obj
+.\abclib\DebugLib\fpgaCreate.obj
+.\abclib\DebugLib\fpgaCut.obj
+.\abclib\DebugLib\fpgaCutUtils.obj
+.\abclib\DebugLib\fpgaFanout.obj
+.\abclib\DebugLib\fpgaLib.obj
+.\abclib\DebugLib\fpgaMatch.obj
+.\abclib\DebugLib\fpgaSwitch.obj
+.\abclib\DebugLib\fpgaTime.obj
+.\abclib\DebugLib\fpgaTruth.obj
+.\abclib\DebugLib\fpgaUtils.obj
+.\abclib\DebugLib\fpgaVec.obj
+.\abclib\DebugLib\mapper.obj
+.\abclib\DebugLib\mapperCanon.obj
+.\abclib\DebugLib\mapperCore.obj
+.\abclib\DebugLib\mapperCreate.obj
+.\abclib\DebugLib\mapperCut.obj
+.\abclib\DebugLib\mapperCutUtils.obj
+.\abclib\DebugLib\mapperFanout.obj
+.\abclib\DebugLib\mapperLib.obj
+.\abclib\DebugLib\mapperMatch.obj
+.\abclib\DebugLib\mapperRefs.obj
+.\abclib\DebugLib\mapperSuper.obj
+.\abclib\DebugLib\mapperSwitch.obj
+.\abclib\DebugLib\mapperTable.obj
+.\abclib\DebugLib\mapperTime.obj
+.\abclib\DebugLib\mapperTree.obj
+.\abclib\DebugLib\mapperTruth.obj
+.\abclib\DebugLib\mapperUtils.obj
+.\abclib\DebugLib\mapperVec.obj
+.\abclib\DebugLib\mio.obj
+.\abclib\DebugLib\mioApi.obj
+.\abclib\DebugLib\mioFunc.obj
+.\abclib\DebugLib\mioRead.obj
+.\abclib\DebugLib\mioUtils.obj
+.\abclib\DebugLib\super.obj
+.\abclib\DebugLib\superAnd.obj
+.\abclib\DebugLib\superGate.obj
+.\abclib\DebugLib\superWrite.obj
+.\abclib\DebugLib\ifCore.obj
+.\abclib\DebugLib\ifCut.obj
+.\abclib\DebugLib\ifMan.obj
+.\abclib\DebugLib\ifMap.obj
+.\abclib\DebugLib\ifPrepro.obj
+.\abclib\DebugLib\ifReduce.obj
+.\abclib\DebugLib\ifSeq.obj
+.\abclib\DebugLib\ifTime.obj
+.\abclib\DebugLib\ifTruth.obj
+.\abclib\DebugLib\ifUtil.obj
+.\abclib\DebugLib\extraBddAuto.obj
+.\abclib\DebugLib\extraBddKmap.obj
+.\abclib\DebugLib\extraBddMisc.obj
+.\abclib\DebugLib\extraBddSymm.obj
+.\abclib\DebugLib\extraBddUnate.obj
+.\abclib\DebugLib\extraUtilBitMatrix.obj
+.\abclib\DebugLib\extraUtilCanon.obj
+.\abclib\DebugLib\extraUtilFile.obj
+.\abclib\DebugLib\extraUtilMemory.obj
+.\abclib\DebugLib\extraUtilMisc.obj
+.\abclib\DebugLib\extraUtilProgress.obj
+.\abclib\DebugLib\extraUtilReader.obj
+.\abclib\DebugLib\extraUtilTruth.obj
+.\abclib\DebugLib\extraUtilUtil.obj
+.\abclib\DebugLib\st.obj
+.\abclib\DebugLib\stmm.obj
+.\abclib\DebugLib\mvc.obj
+.\abclib\DebugLib\mvcApi.obj
+.\abclib\DebugLib\mvcCompare.obj
+.\abclib\DebugLib\mvcContain.obj
+.\abclib\DebugLib\mvcCover.obj
+.\abclib\DebugLib\mvcCube.obj
+.\abclib\DebugLib\mvcDivide.obj
+.\abclib\DebugLib\mvcDivisor.obj
+.\abclib\DebugLib\mvcList.obj
+.\abclib\DebugLib\mvcLits.obj
+.\abclib\DebugLib\mvcMan.obj
+.\abclib\DebugLib\mvcOpAlg.obj
+.\abclib\DebugLib\mvcOpBool.obj
+.\abclib\DebugLib\mvcPrint.obj
+.\abclib\DebugLib\mvcSort.obj
+.\abclib\DebugLib\mvcUtils.obj
+.\abclib\DebugLib\cofactor.obj
+.\abclib\DebugLib\cols.obj
+.\abclib\DebugLib\compl.obj
+.\abclib\DebugLib\contain.obj
+.\abclib\DebugLib\cubehack.obj
+.\abclib\DebugLib\cubestr.obj
+.\abclib\DebugLib\cvrin.obj
+.\abclib\DebugLib\cvrm.obj
+.\abclib\DebugLib\cvrmisc.obj
+.\abclib\DebugLib\cvrout.obj
+.\abclib\DebugLib\dominate.obj
+.\abclib\DebugLib\equiv.obj
+.\abclib\DebugLib\espresso.obj
+.\abclib\DebugLib\essen.obj
+.\abclib\DebugLib\exact.obj
+.\abclib\DebugLib\expand.obj
+.\abclib\DebugLib\gasp.obj
+.\abclib\DebugLib\gimpel.obj
+.\abclib\DebugLib\globals.obj
+.\abclib\DebugLib\hack.obj
+.\abclib\DebugLib\indep.obj
+.\abclib\DebugLib\irred.obj
+.\abclib\DebugLib\map.obj
+.\abclib\DebugLib\matrix.obj
+.\abclib\DebugLib\mincov.obj
+.\abclib\DebugLib\opo.obj
+.\abclib\DebugLib\pair.obj
+.\abclib\DebugLib\part.obj
+.\abclib\DebugLib\primes.obj
+.\abclib\DebugLib\reduce.obj
+.\abclib\DebugLib\rows.obj
+.\abclib\DebugLib\set.obj
+.\abclib\DebugLib\setc.obj
+.\abclib\DebugLib\sharp.obj
+.\abclib\DebugLib\sminterf.obj
+.\abclib\DebugLib\solution.obj
+.\abclib\DebugLib\sparse.obj
+.\abclib\DebugLib\unate.obj
+.\abclib\DebugLib\verify.obj
+.\abclib\DebugLib\nmApi.obj
+.\abclib\DebugLib\nmTable.obj
+.\abclib\DebugLib\hopBalance.obj
+.\abclib\DebugLib\hopCheck.obj
+.\abclib\DebugLib\hopDfs.obj
+.\abclib\DebugLib\hopMan.obj
+.\abclib\DebugLib\hopMem.obj
+.\abclib\DebugLib\hopObj.obj
+.\abclib\DebugLib\hopOper.obj
+.\abclib\DebugLib\hopTable.obj
+.\abclib\DebugLib\hopUtil.obj
+.\abclib\DebugLib\ivyBalance.obj
+.\abclib\DebugLib\ivyCanon.obj
+.\abclib\DebugLib\ivyCheck.obj
+.\abclib\DebugLib\ivyCut.obj
+.\abclib\DebugLib\ivyCutTrav.obj
+.\abclib\DebugLib\ivyDfs.obj
+.\abclib\DebugLib\ivyDsd.obj
+.\abclib\DebugLib\ivyFanout.obj
+.\abclib\DebugLib\ivyFastMap.obj
+.\abclib\DebugLib\ivyFraig.obj
+.\abclib\DebugLib\ivyHaig.obj
+.\abclib\DebugLib\ivyMan.obj
+.\abclib\DebugLib\ivyMem.obj
+.\abclib\DebugLib\ivyMulti.obj
+.\abclib\DebugLib\ivyObj.obj
+.\abclib\DebugLib\ivyOper.obj
+.\abclib\DebugLib\ivyResyn.obj
+.\abclib\DebugLib\ivyRwr.obj
+.\abclib\DebugLib\ivySeq.obj
+.\abclib\DebugLib\ivyShow.obj
+.\abclib\DebugLib\ivyTable.obj
+.\abclib\DebugLib\ivyUtil.obj
+.\abclib\DebugLib\rwtDec.obj
+.\abclib\DebugLib\rwtMan.obj
+.\abclib\DebugLib\rwtUtil.obj
+.\abclib\DebugLib\mem.obj
+.\abclib\DebugLib\jfront.obj
+]
+Creating command line "link.exe -lib @C:\DOCUME~1\alanmi\LOCALS~1\Temp\RSP137B.tmp"
+<h3>Output Window</h3>
+Compiling...
+jfront.c
+Creating library...
+Creating temporary file "C:\DOCUME~1\alanmi\LOCALS~1\Temp\RSP137C.tmp" with contents
+[
+/nologo /o"abclib\DebugLib/abclib.bsc"
+.\abclib\DebugLib\abcAig.sbr
+.\abclib\DebugLib\abcCheck.sbr
+.\abclib\DebugLib\abcDfs.sbr
+.\abclib\DebugLib\abcFanio.sbr
+.\abclib\DebugLib\abcFunc.sbr
+.\abclib\DebugLib\abcLatch.sbr
+.\abclib\DebugLib\abcLib.sbr
+.\abclib\DebugLib\abcMinBase.sbr
+.\abclib\DebugLib\abcNames.sbr
+.\abclib\DebugLib\abcNetlist.sbr
+.\abclib\DebugLib\abcNtk.sbr
+.\abclib\DebugLib\abcObj.sbr
+.\abclib\DebugLib\abcRefs.sbr
+.\abclib\DebugLib\abcShow.sbr
+.\abclib\DebugLib\abcSop.sbr
+.\abclib\DebugLib\abcUtil.sbr
+.\abclib\DebugLib\abc.sbr
+.\abclib\DebugLib\abcAttach.sbr
+.\abclib\DebugLib\abcAuto.sbr
+.\abclib\DebugLib\abcBalance.sbr
+.\abclib\DebugLib\abcBmc.sbr
+.\abclib\DebugLib\abcClpBdd.sbr
+.\abclib\DebugLib\abcClpSop.sbr
+.\abclib\DebugLib\abcCut.sbr
+.\abclib\DebugLib\abcDebug.sbr
+.\abclib\DebugLib\abcDress.sbr
+.\abclib\DebugLib\abcDsd.sbr
+.\abclib\DebugLib\abcEspresso.sbr
+.\abclib\DebugLib\abcExtract.sbr
+.\abclib\DebugLib\abcFpga.sbr
+.\abclib\DebugLib\abcFpgaFast.sbr
+.\abclib\DebugLib\abcFraig.sbr
+.\abclib\DebugLib\abcFxu.sbr
+.\abclib\DebugLib\abcGen.sbr
+.\abclib\DebugLib\abcIf.sbr
+.\abclib\DebugLib\abcIvy.sbr
+.\abclib\DebugLib\abcLut.sbr
+.\abclib\DebugLib\abcMap.sbr
+.\abclib\DebugLib\abcMini.sbr
+.\abclib\DebugLib\abcMiter.sbr
+.\abclib\DebugLib\abcMulti.sbr
+.\abclib\DebugLib\abcMv.sbr
+.\abclib\DebugLib\abcNtbdd.sbr
+.\abclib\DebugLib\abcOrder.sbr
+.\abclib\DebugLib\abcPrint.sbr
+.\abclib\DebugLib\abcProve.sbr
+.\abclib\DebugLib\abcReconv.sbr
+.\abclib\DebugLib\abcRefactor.sbr
+.\abclib\DebugLib\abcRenode.sbr
+.\abclib\DebugLib\abcReorder.sbr
+.\abclib\DebugLib\abcRestruct.sbr
+.\abclib\DebugLib\abcResub.sbr
+.\abclib\DebugLib\abcRewrite.sbr
+.\abclib\DebugLib\abcRr.sbr
+.\abclib\DebugLib\abcSat.sbr
+.\abclib\DebugLib\abcStrash.sbr
+.\abclib\DebugLib\abcSweep.sbr
+.\abclib\DebugLib\abcSymm.sbr
+.\abclib\DebugLib\abcTiming.sbr
+.\abclib\DebugLib\abcUnate.sbr
+.\abclib\DebugLib\abcUnreach.sbr
+.\abclib\DebugLib\abcVerify.sbr
+.\abclib\DebugLib\abcXsim.sbr
+.\abclib\DebugLib\cmd.sbr
+.\abclib\DebugLib\cmdAlias.sbr
+.\abclib\DebugLib\cmdApi.sbr
+.\abclib\DebugLib\cmdFlag.sbr
+.\abclib\DebugLib\cmdHist.sbr
+.\abclib\DebugLib\cmdUtils.sbr
+.\abclib\DebugLib\io.sbr
+.\abclib\DebugLib\ioReadAiger.sbr
+.\abclib\DebugLib\ioReadBaf.sbr
+.\abclib\DebugLib\ioReadBench.sbr
+.\abclib\DebugLib\ioReadBlif.sbr
+.\abclib\DebugLib\ioReadBlifAig.sbr
+.\abclib\DebugLib\ioReadEdif.sbr
+.\abclib\DebugLib\ioReadEqn.sbr
+.\abclib\DebugLib\ioReadPla.sbr
+.\abclib\DebugLib\ioUtil.sbr
+.\abclib\DebugLib\ioWriteAiger.sbr
+.\abclib\DebugLib\ioWriteBaf.sbr
+.\abclib\DebugLib\ioWriteBench.sbr
+.\abclib\DebugLib\ioWriteBlif.sbr
+.\abclib\DebugLib\ioWriteCnf.sbr
+.\abclib\DebugLib\ioWriteDot.sbr
+.\abclib\DebugLib\ioWriteEqn.sbr
+.\abclib\DebugLib\ioWriteGml.sbr
+.\abclib\DebugLib\ioWriteList.sbr
+.\abclib\DebugLib\ioWritePla.sbr
+.\abclib\DebugLib\ioWriteVer.sbr
+.\abclib\DebugLib\ioWriteVerAux.sbr
+.\abclib\DebugLib\libSupport.sbr
+.\abclib\DebugLib\main.sbr
+.\abclib\DebugLib\mainFrame.sbr
+.\abclib\DebugLib\mainInit.sbr
+.\abclib\DebugLib\mainUtils.sbr
+.\abclib\DebugLib\verCore.sbr
+.\abclib\DebugLib\verFormula.sbr
+.\abclib\DebugLib\verParse.sbr
+.\abclib\DebugLib\verStream.sbr
+.\abclib\DebugLib\verWords.sbr
+.\abclib\DebugLib\cuddAddAbs.sbr
+.\abclib\DebugLib\cuddAddApply.sbr
+.\abclib\DebugLib\cuddAddFind.sbr
+.\abclib\DebugLib\cuddAddInv.sbr
+.\abclib\DebugLib\cuddAddIte.sbr
+.\abclib\DebugLib\cuddAddNeg.sbr
+.\abclib\DebugLib\cuddAddWalsh.sbr
+.\abclib\DebugLib\cuddAndAbs.sbr
+.\abclib\DebugLib\cuddAnneal.sbr
+.\abclib\DebugLib\cuddApa.sbr
+.\abclib\DebugLib\cuddAPI.sbr
+.\abclib\DebugLib\cuddApprox.sbr
+.\abclib\DebugLib\cuddBddAbs.sbr
+.\abclib\DebugLib\cuddBddCorr.sbr
+.\abclib\DebugLib\cuddBddIte.sbr
+.\abclib\DebugLib\cuddBridge.sbr
+.\abclib\DebugLib\cuddCache.sbr
+.\abclib\DebugLib\cuddCheck.sbr
+.\abclib\DebugLib\cuddClip.sbr
+.\abclib\DebugLib\cuddCof.sbr
+.\abclib\DebugLib\cuddCompose.sbr
+.\abclib\DebugLib\cuddDecomp.sbr
+.\abclib\DebugLib\cuddEssent.sbr
+.\abclib\DebugLib\cuddExact.sbr
+.\abclib\DebugLib\cuddExport.sbr
+.\abclib\DebugLib\cuddGenCof.sbr
+.\abclib\DebugLib\cuddGenetic.sbr
+.\abclib\DebugLib\cuddGroup.sbr
+.\abclib\DebugLib\cuddHarwell.sbr
+.\abclib\DebugLib\cuddInit.sbr
+.\abclib\DebugLib\cuddInteract.sbr
+.\abclib\DebugLib\cuddLCache.sbr
+.\abclib\DebugLib\cuddLevelQ.sbr
+.\abclib\DebugLib\cuddLinear.sbr
+.\abclib\DebugLib\cuddLiteral.sbr
+.\abclib\DebugLib\cuddMatMult.sbr
+.\abclib\DebugLib\cuddPriority.sbr
+.\abclib\DebugLib\cuddRead.sbr
+.\abclib\DebugLib\cuddRef.sbr
+.\abclib\DebugLib\cuddReorder.sbr
+.\abclib\DebugLib\cuddSat.sbr
+.\abclib\DebugLib\cuddSign.sbr
+.\abclib\DebugLib\cuddSolve.sbr
+.\abclib\DebugLib\cuddSplit.sbr
+.\abclib\DebugLib\cuddSubsetHB.sbr
+.\abclib\DebugLib\cuddSubsetSP.sbr
+.\abclib\DebugLib\cuddSymmetry.sbr
+.\abclib\DebugLib\cuddTable.sbr
+.\abclib\DebugLib\cuddUtil.sbr
+.\abclib\DebugLib\cuddWindow.sbr
+.\abclib\DebugLib\cuddZddCount.sbr
+.\abclib\DebugLib\cuddZddFuncs.sbr
+.\abclib\DebugLib\cuddZddGroup.sbr
+.\abclib\DebugLib\cuddZddIsop.sbr
+.\abclib\DebugLib\cuddZddLin.sbr
+.\abclib\DebugLib\cuddZddMisc.sbr
+.\abclib\DebugLib\cuddZddPort.sbr
+.\abclib\DebugLib\cuddZddReord.sbr
+.\abclib\DebugLib\cuddZddSetop.sbr
+.\abclib\DebugLib\cuddZddSymm.sbr
+.\abclib\DebugLib\cuddZddUtil.sbr
+.\abclib\DebugLib\epd.sbr
+.\abclib\DebugLib\mtrBasic.sbr
+.\abclib\DebugLib\mtrGroup.sbr
+.\abclib\DebugLib\parseCore.sbr
+.\abclib\DebugLib\parseEqn.sbr
+.\abclib\DebugLib\parseStack.sbr
+.\abclib\DebugLib\dsdApi.sbr
+.\abclib\DebugLib\dsdCheck.sbr
+.\abclib\DebugLib\dsdLocal.sbr
+.\abclib\DebugLib\dsdMan.sbr
+.\abclib\DebugLib\dsdProc.sbr
+.\abclib\DebugLib\dsdTree.sbr
+.\abclib\DebugLib\reoApi.sbr
+.\abclib\DebugLib\reoCore.sbr
+.\abclib\DebugLib\reoProfile.sbr
+.\abclib\DebugLib\reoSift.sbr
+.\abclib\DebugLib\reoSwap.sbr
+.\abclib\DebugLib\reoTest.sbr
+.\abclib\DebugLib\reoTransfer.sbr
+.\abclib\DebugLib\reoUnits.sbr
+.\abclib\DebugLib\added.sbr
+.\abclib\DebugLib\asatmem.sbr
+.\abclib\DebugLib\solver.sbr
+.\abclib\DebugLib\msatActivity.sbr
+.\abclib\DebugLib\msatClause.sbr
+.\abclib\DebugLib\msatClauseVec.sbr
+.\abclib\DebugLib\msatMem.sbr
+.\abclib\DebugLib\msatOrderH.sbr
+.\abclib\DebugLib\msatQueue.sbr
+.\abclib\DebugLib\msatRead.sbr
+.\abclib\DebugLib\msatSolverApi.sbr
+.\abclib\DebugLib\msatSolverCore.sbr
+.\abclib\DebugLib\msatSolverIo.sbr
+.\abclib\DebugLib\msatSolverSearch.sbr
+.\abclib\DebugLib\msatSort.sbr
+.\abclib\DebugLib\msatVec.sbr
+.\abclib\DebugLib\fraigApi.sbr
+.\abclib\DebugLib\fraigCanon.sbr
+.\abclib\DebugLib\fraigChoice.sbr
+.\abclib\DebugLib\fraigFanout.sbr
+.\abclib\DebugLib\fraigFeed.sbr
+.\abclib\DebugLib\fraigMan.sbr
+.\abclib\DebugLib\fraigMem.sbr
+.\abclib\DebugLib\fraigNode.sbr
+.\abclib\DebugLib\fraigPrime.sbr
+.\abclib\DebugLib\fraigSat.sbr
+.\abclib\DebugLib\fraigTable.sbr
+.\abclib\DebugLib\fraigUtil.sbr
+.\abclib\DebugLib\fraigVec.sbr
+.\abclib\DebugLib\csat_apis.sbr
+.\abclib\DebugLib\satMem.sbr
+.\abclib\DebugLib\satSolver.sbr
+.\abclib\DebugLib\satUtil.sbr
+.\abclib\DebugLib\fxu.sbr
+.\abclib\DebugLib\fxuCreate.sbr
+.\abclib\DebugLib\fxuHeapD.sbr
+.\abclib\DebugLib\fxuHeapS.sbr
+.\abclib\DebugLib\fxuList.sbr
+.\abclib\DebugLib\fxuMatrix.sbr
+.\abclib\DebugLib\fxuPair.sbr
+.\abclib\DebugLib\fxuPrint.sbr
+.\abclib\DebugLib\fxuReduce.sbr
+.\abclib\DebugLib\fxuSelect.sbr
+.\abclib\DebugLib\fxuSingle.sbr
+.\abclib\DebugLib\fxuUpdate.sbr
+.\abclib\DebugLib\rwrDec.sbr
+.\abclib\DebugLib\rwrEva.sbr
+.\abclib\DebugLib\rwrExp.sbr
+.\abclib\DebugLib\rwrLib.sbr
+.\abclib\DebugLib\rwrMan.sbr
+.\abclib\DebugLib\rwrPrint.sbr
+.\abclib\DebugLib\rwrTemp.sbr
+.\abclib\DebugLib\rwrUtil.sbr
+.\abclib\DebugLib\cutApi.sbr
+.\abclib\DebugLib\cutCut.sbr
+.\abclib\DebugLib\cutExpand.sbr
+.\abclib\DebugLib\cutMan.sbr
+.\abclib\DebugLib\cutMerge.sbr
+.\abclib\DebugLib\cutNode.sbr
+.\abclib\DebugLib\cutOracle.sbr
+.\abclib\DebugLib\cutPre22.sbr
+.\abclib\DebugLib\cutSeq.sbr
+.\abclib\DebugLib\cutTruth.sbr
+.\abclib\DebugLib\decAbc.sbr
+.\abclib\DebugLib\decFactor.sbr
+.\abclib\DebugLib\decMan.sbr
+.\abclib\DebugLib\decPrint.sbr
+.\abclib\DebugLib\decUtil.sbr
+.\abclib\DebugLib\simMan.sbr
+.\abclib\DebugLib\simSat.sbr
+.\abclib\DebugLib\simSeq.sbr
+.\abclib\DebugLib\simSupp.sbr
+.\abclib\DebugLib\simSwitch.sbr
+.\abclib\DebugLib\simSym.sbr
+.\abclib\DebugLib\simSymSat.sbr
+.\abclib\DebugLib\simSymSim.sbr
+.\abclib\DebugLib\simSymStr.sbr
+.\abclib\DebugLib\simUtils.sbr
+.\abclib\DebugLib\retArea.sbr
+.\abclib\DebugLib\retCore.sbr
+.\abclib\DebugLib\retDelay.sbr
+.\abclib\DebugLib\retFlow.sbr
+.\abclib\DebugLib\retIncrem.sbr
+.\abclib\DebugLib\retInit.sbr
+.\abclib\DebugLib\retLvalue.sbr
+.\abclib\DebugLib\kitBdd.sbr
+.\abclib\DebugLib\kitFactor.sbr
+.\abclib\DebugLib\kitGraph.sbr
+.\abclib\DebugLib\kitHop.sbr
+.\abclib\DebugLib\kitIsop.sbr
+.\abclib\DebugLib\kitSop.sbr
+.\abclib\DebugLib\kitTruth.sbr
+.\abclib\DebugLib\fpga.sbr
+.\abclib\DebugLib\fpgaCore.sbr
+.\abclib\DebugLib\fpgaCreate.sbr
+.\abclib\DebugLib\fpgaCut.sbr
+.\abclib\DebugLib\fpgaCutUtils.sbr
+.\abclib\DebugLib\fpgaFanout.sbr
+.\abclib\DebugLib\fpgaLib.sbr
+.\abclib\DebugLib\fpgaMatch.sbr
+.\abclib\DebugLib\fpgaSwitch.sbr
+.\abclib\DebugLib\fpgaTime.sbr
+.\abclib\DebugLib\fpgaTruth.sbr
+.\abclib\DebugLib\fpgaUtils.sbr
+.\abclib\DebugLib\fpgaVec.sbr
+.\abclib\DebugLib\mapper.sbr
+.\abclib\DebugLib\mapperCanon.sbr
+.\abclib\DebugLib\mapperCore.sbr
+.\abclib\DebugLib\mapperCreate.sbr
+.\abclib\DebugLib\mapperCut.sbr
+.\abclib\DebugLib\mapperCutUtils.sbr
+.\abclib\DebugLib\mapperFanout.sbr
+.\abclib\DebugLib\mapperLib.sbr
+.\abclib\DebugLib\mapperMatch.sbr
+.\abclib\DebugLib\mapperRefs.sbr
+.\abclib\DebugLib\mapperSuper.sbr
+.\abclib\DebugLib\mapperSwitch.sbr
+.\abclib\DebugLib\mapperTable.sbr
+.\abclib\DebugLib\mapperTime.sbr
+.\abclib\DebugLib\mapperTree.sbr
+.\abclib\DebugLib\mapperTruth.sbr
+.\abclib\DebugLib\mapperUtils.sbr
+.\abclib\DebugLib\mapperVec.sbr
+.\abclib\DebugLib\mio.sbr
+.\abclib\DebugLib\mioApi.sbr
+.\abclib\DebugLib\mioFunc.sbr
+.\abclib\DebugLib\mioRead.sbr
+.\abclib\DebugLib\mioUtils.sbr
+.\abclib\DebugLib\super.sbr
+.\abclib\DebugLib\superAnd.sbr
+.\abclib\DebugLib\superGate.sbr
+.\abclib\DebugLib\superWrite.sbr
+.\abclib\DebugLib\ifCore.sbr
+.\abclib\DebugLib\ifCut.sbr
+.\abclib\DebugLib\ifMan.sbr
+.\abclib\DebugLib\ifMap.sbr
+.\abclib\DebugLib\ifPrepro.sbr
+.\abclib\DebugLib\ifReduce.sbr
+.\abclib\DebugLib\ifSeq.sbr
+.\abclib\DebugLib\ifTime.sbr
+.\abclib\DebugLib\ifTruth.sbr
+.\abclib\DebugLib\ifUtil.sbr
+.\abclib\DebugLib\extraBddAuto.sbr
+.\abclib\DebugLib\extraBddKmap.sbr
+.\abclib\DebugLib\extraBddMisc.sbr
+.\abclib\DebugLib\extraBddSymm.sbr
+.\abclib\DebugLib\extraBddUnate.sbr
+.\abclib\DebugLib\extraUtilBitMatrix.sbr
+.\abclib\DebugLib\extraUtilCanon.sbr
+.\abclib\DebugLib\extraUtilFile.sbr
+.\abclib\DebugLib\extraUtilMemory.sbr
+.\abclib\DebugLib\extraUtilMisc.sbr
+.\abclib\DebugLib\extraUtilProgress.sbr
+.\abclib\DebugLib\extraUtilReader.sbr
+.\abclib\DebugLib\extraUtilTruth.sbr
+.\abclib\DebugLib\extraUtilUtil.sbr
+.\abclib\DebugLib\st.sbr
+.\abclib\DebugLib\stmm.sbr
+.\abclib\DebugLib\mvc.sbr
+.\abclib\DebugLib\mvcApi.sbr
+.\abclib\DebugLib\mvcCompare.sbr
+.\abclib\DebugLib\mvcContain.sbr
+.\abclib\DebugLib\mvcCover.sbr
+.\abclib\DebugLib\mvcCube.sbr
+.\abclib\DebugLib\mvcDivide.sbr
+.\abclib\DebugLib\mvcDivisor.sbr
+.\abclib\DebugLib\mvcList.sbr
+.\abclib\DebugLib\mvcLits.sbr
+.\abclib\DebugLib\mvcMan.sbr
+.\abclib\DebugLib\mvcOpAlg.sbr
+.\abclib\DebugLib\mvcOpBool.sbr
+.\abclib\DebugLib\mvcPrint.sbr
+.\abclib\DebugLib\mvcSort.sbr
+.\abclib\DebugLib\mvcUtils.sbr
+.\abclib\DebugLib\cofactor.sbr
+.\abclib\DebugLib\cols.sbr
+.\abclib\DebugLib\compl.sbr
+.\abclib\DebugLib\contain.sbr
+.\abclib\DebugLib\cubehack.sbr
+.\abclib\DebugLib\cubestr.sbr
+.\abclib\DebugLib\cvrin.sbr
+.\abclib\DebugLib\cvrm.sbr
+.\abclib\DebugLib\cvrmisc.sbr
+.\abclib\DebugLib\cvrout.sbr
+.\abclib\DebugLib\dominate.sbr
+.\abclib\DebugLib\equiv.sbr
+.\abclib\DebugLib\espresso.sbr
+.\abclib\DebugLib\essen.sbr
+.\abclib\DebugLib\exact.sbr
+.\abclib\DebugLib\expand.sbr
+.\abclib\DebugLib\gasp.sbr
+.\abclib\DebugLib\gimpel.sbr
+.\abclib\DebugLib\globals.sbr
+.\abclib\DebugLib\hack.sbr
+.\abclib\DebugLib\indep.sbr
+.\abclib\DebugLib\irred.sbr
+.\abclib\DebugLib\map.sbr
+.\abclib\DebugLib\matrix.sbr
+.\abclib\DebugLib\mincov.sbr
+.\abclib\DebugLib\opo.sbr
+.\abclib\DebugLib\pair.sbr
+.\abclib\DebugLib\part.sbr
+.\abclib\DebugLib\primes.sbr
+.\abclib\DebugLib\reduce.sbr
+.\abclib\DebugLib\rows.sbr
+.\abclib\DebugLib\set.sbr
+.\abclib\DebugLib\setc.sbr
+.\abclib\DebugLib\sharp.sbr
+.\abclib\DebugLib\sminterf.sbr
+.\abclib\DebugLib\solution.sbr
+.\abclib\DebugLib\sparse.sbr
+.\abclib\DebugLib\unate.sbr
+.\abclib\DebugLib\verify.sbr
+.\abclib\DebugLib\nmApi.sbr
+.\abclib\DebugLib\nmTable.sbr
+.\abclib\DebugLib\hopBalance.sbr
+.\abclib\DebugLib\hopCheck.sbr
+.\abclib\DebugLib\hopDfs.sbr
+.\abclib\DebugLib\hopMan.sbr
+.\abclib\DebugLib\hopMem.sbr
+.\abclib\DebugLib\hopObj.sbr
+.\abclib\DebugLib\hopOper.sbr
+.\abclib\DebugLib\hopTable.sbr
+.\abclib\DebugLib\hopUtil.sbr
+.\abclib\DebugLib\ivyBalance.sbr
+.\abclib\DebugLib\ivyCanon.sbr
+.\abclib\DebugLib\ivyCheck.sbr
+.\abclib\DebugLib\ivyCut.sbr
+.\abclib\DebugLib\ivyCutTrav.sbr
+.\abclib\DebugLib\ivyDfs.sbr
+.\abclib\DebugLib\ivyDsd.sbr
+.\abclib\DebugLib\ivyFanout.sbr
+.\abclib\DebugLib\ivyFastMap.sbr
+.\abclib\DebugLib\ivyFraig.sbr
+.\abclib\DebugLib\ivyHaig.sbr
+.\abclib\DebugLib\ivyMan.sbr
+.\abclib\DebugLib\ivyMem.sbr
+.\abclib\DebugLib\ivyMulti.sbr
+.\abclib\DebugLib\ivyObj.sbr
+.\abclib\DebugLib\ivyOper.sbr
+.\abclib\DebugLib\ivyResyn.sbr
+.\abclib\DebugLib\ivyRwr.sbr
+.\abclib\DebugLib\ivySeq.sbr
+.\abclib\DebugLib\ivyShow.sbr
+.\abclib\DebugLib\ivyTable.sbr
+.\abclib\DebugLib\ivyUtil.sbr
+.\abclib\DebugLib\rwtDec.sbr
+.\abclib\DebugLib\rwtMan.sbr
+.\abclib\DebugLib\rwtUtil.sbr
+.\abclib\DebugLib\mem.sbr
+.\abclib\DebugLib\jfront.sbr]
+Creating command line "bscmake.exe @C:\DOCUME~1\alanmi\LOCALS~1\Temp\RSP137C.tmp"
+Creating browse info file...
+<h3>Output Window</h3>
+
+
+
+<h3>Results</h3>
+abclib_debug.lib - 0 error(s), 0 warning(s)
+</pre>
+</body>
+</html>
diff --git a/abctestlib.plg b/abctestlib.plg
new file mode 100644
index 00000000..0d4fd935
--- /dev/null
+++ b/abctestlib.plg
@@ -0,0 +1,35 @@
+<html>
+<body>
+<pre>
+<h1>Build Log</h1>
+<h3>
+--------------------Configuration: abctestlib - Win32 Debug--------------------
+</h3>
+<h3>Command Lines</h3>
+Creating temporary file "C:\DOCUME~1\alanmi\LOCALS~1\Temp\RSP1389.tmp" with contents
+[
+/nologo /MLd /W3 /Gm /GX /ZI /Od /D "WIN32" /D "_DEBUG" /D "_CONSOLE" /D "_MBCS" /FR"Debug/" /Fp"Debug/abctestlib.pch" /YX /Fo"Debug/" /Fd"Debug/" /FD /GZ /c
+"C:\_projects\abc\demo.c"
+]
+Creating command line "cl.exe @C:\DOCUME~1\alanmi\LOCALS~1\Temp\RSP1389.tmp"
+Creating temporary file "C:\DOCUME~1\alanmi\LOCALS~1\Temp\RSP138A.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 C:\_projects\abc\abclib\abclib_debug.lib /nologo /subsystem:console /incremental:yes /pdb:"Debug/abctestlib.pdb" /debug /machine:I386 /out:"_TEST/abctestlib.exe" /pdbtype:sept
+.\Debug\demo.obj
+]
+Creating command line "link.exe @C:\DOCUME~1\alanmi\LOCALS~1\Temp\RSP138A.tmp"
+<h3>Output Window</h3>
+Compiling...
+demo.c
+Linking...
+Creating command line "bscmake.exe /nologo /o"Debug/abctestlib.bsc" .\Debug\demo.sbr"
+Creating browse info file...
+<h3>Output Window</h3>
+
+
+
+<h3>Results</h3>
+abctestlib.exe - 0 error(s), 0 warning(s)
+</pre>
+</body>
+</html>
diff --git a/src/base/abc/abc.h b/src/base/abc/abc.h
index 3d46cdf0..62aac927 100644
--- a/src/base/abc/abc.h
+++ b/src/base/abc/abc.h
@@ -197,6 +197,7 @@ struct Abc_Ntk_t_
Extra_MmFixed_t * pMmObj; // memory manager for objects
Extra_MmStep_t * pMmStep; // memory manager for arrays
void * pManFunc; // functionality manager (AIG manager, BDD manager, or memory manager for SOPs)
+ Abc_Lib_t * pDesign;
// Abc_Lib_t * pVerLib; // for structural verilog designs
Abc_ManTime_t * pManTime; // the timing manager (for mapped networks) stores arrival/required times for all nodes
void * pManCut; // the cut manager (for AIGs) stores information about the cuts computed for the nodes
@@ -244,10 +245,11 @@ static inline void Abc_InfoFill( unsigned * p, int nWords ) { memset( p
static inline void Abc_InfoNot( unsigned * p, int nWords ) { int i; for ( i = nWords - 1; i >= 0; i-- ) p[i] = ~p[i]; }
static inline int Abc_InfoIsZero( unsigned * p, int nWords ) { int i; for ( i = nWords - 1; i >= 0; i-- ) if ( p[i] ) return 0; return 1; }
static inline int Abc_InfoIsOne( unsigned * p, int nWords ) { int i; for ( i = nWords - 1; i >= 0; i-- ) if ( ~p[i] ) return 0; return 1; }
-static inline void Abc_InfoCopy( unsigned * p, unsigned * q, int nWords ) { int i; for ( i = nWords - 1; i >= 0; i-- ) p[i] = q[i]; }
-static inline void Abc_InfoAnd( unsigned * p, unsigned * q, int nWords ) { int i; for ( i = nWords - 1; i >= 0; i-- ) p[i] &= q[i]; }
-static inline void Abc_InfoOr( unsigned * p, unsigned * q, int nWords ) { int i; for ( i = nWords - 1; i >= 0; i-- ) p[i] |= q[i]; }
-static inline void Abc_InfoXor( unsigned * p, unsigned * q, int nWords ) { int i; for ( i = nWords - 1; i >= 0; i-- ) p[i] ^= q[i]; }
+static inline void Abc_InfoCopy( unsigned * p, unsigned * q, int nWords ) { int i; for ( i = nWords - 1; i >= 0; i-- ) p[i] = q[i]; }
+static inline void Abc_InfoAnd( unsigned * p, unsigned * q, int nWords ) { int i; for ( i = nWords - 1; i >= 0; i-- ) p[i] &= q[i]; }
+static inline void Abc_InfoOr( unsigned * p, unsigned * q, int nWords ) { int i; for ( i = nWords - 1; i >= 0; i-- ) p[i] |= q[i]; }
+static inline void Abc_InfoXor( unsigned * p, unsigned * q, int nWords ) { int i; for ( i = nWords - 1; i >= 0; i-- ) p[i] ^= q[i]; }
+static inline int Abc_InfoIsOrOne( unsigned * p, unsigned * q, int nWords ){ int i; for ( i = nWords - 1; i >= 0; i-- ) if ( ~(p[i] | q[i]) ) return 0; return 1; }
// checking the network type
static inline bool Abc_NtkIsNetlist( Abc_Ntk_t * pNtk ) { return pNtk->ntkType == ABC_NTK_NETLIST; }
diff --git a/src/base/abc/abcHie.c b/src/base/abc/abcHie.c
index 9c9d8a56..c42cff45 100644
--- a/src/base/abc/abcHie.c
+++ b/src/base/abc/abcHie.c
@@ -6,7 +6,7 @@
PackageName [Network and node package.]
- Synopsis [Hierarchy manager.]
+ Synopsis [Procedures to handle hierarchy.]
Author [Alan Mishchenko]
@@ -23,14 +23,12 @@
////////////////////////////////////////////////////////////////////////
/// DECLARATIONS ///
////////////////////////////////////////////////////////////////////////
-
-typedef struct Abc_Hie_t_ Abc_Hie_t;
-struct Abc_Hie_t_
-{
- Vec_Ptr_t * vTops;
- Vec_Ptr_t * vModels;
- stmm_table * vNameToModel;
-};
+
+extern Abc_Ntk_t * Abc_NtkFlattenLogicHierarchy( Abc_Ntk_t * pNtk );
+extern Abc_Ntk_t * Abc_NtkConvertBlackboxes( Abc_Ntk_t * pNtk );
+extern void Abc_NtkInsertNewLogic( Abc_Ntk_t * pNtkHie, Abc_Ntk_t * pNtk );
+
+static void Abc_NtkFlattenLogicHierarchy_rec( Abc_Ntk_t * pNtkNew, Abc_Ntk_t * pNtkOld, int * pCounter );
////////////////////////////////////////////////////////////////////////
/// FUNCTION DEFINITIONS ///
@@ -38,7 +36,131 @@ struct Abc_Hie_t_
/**Function*************************************************************
- Synopsis []
+ Synopsis [Flattens the logic hierarchy of the netlist.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+Abc_Ntk_t * Abc_NtkFlattenLogicHierarchy( Abc_Ntk_t * pNtk )
+{
+ Abc_Ntk_t * pNtkNew;
+ Abc_Obj_t * pObj, * pNet;
+ int i, Counter = 0;
+ assert( Abc_NtkIsNetlist(pNtk) );
+ // start the network
+ pNtkNew = Abc_NtkAlloc( pNtk->ntkType, pNtk->ntkFunc, 1 );
+ // duplicate the name and the spec
+ pNtkNew->pName = Extra_UtilStrsav(pNtk->pName);
+ pNtkNew->pSpec = Extra_UtilStrsav(pNtk->pSpec);
+ // clean the node copy fields
+ Abc_NtkCleanCopy( pNtk );
+ // duplicate PIs/POs and their nets
+ Abc_NtkForEachPi( pNtk, pObj, i )
+ {
+ Abc_NtkDupObj( pNtkNew, pObj, 0 );
+ pNet = Abc_ObjFanout0( pObj );
+ Abc_NtkDupObj( pNtkNew, pNet, 1 );
+ Abc_ObjAddFanin( pNet->pCopy, pObj->pCopy );
+ }
+ Abc_NtkForEachPo( pNtk, pObj, i )
+ {
+ Abc_NtkDupObj( pNtkNew, pObj, 0 );
+ pNet = Abc_ObjFanin0( pObj );
+ pNet->pCopy = Abc_NtkFindOrCreateNet( pNtkNew, Abc_ObjName(pNet) );
+ Abc_ObjAddFanin( pObj->pCopy, pNet->pCopy );
+ }
+ // recursively flatten hierarchy, create internal logic, add new PI/PO names if there are black boxes
+ Abc_NtkFlattenLogicHierarchy_rec( pNtkNew, pNtk, &Counter );
+ printf( "Abc_NtkFlattenLogicHierarchy(): Flattened %d logic boxes. Left %d block boxes.\n",
+ Counter - 1, Abc_NtkBlackboxNum(pNtkNew) );
+ // copy the timing information
+// Abc_ManTimeDup( pNtk, pNtkNew );
+ // duplicate EXDC
+ if ( pNtk->pExdc )
+ printf( "EXDC is not transformed.\n" );
+ if ( !Abc_NtkCheck( pNtkNew ) )
+ fprintf( stdout, "Abc_NtkFlattenLogicHierarchy(): Network check has failed.\n" );
+ return pNtkNew;
+}
+
+/**Function*************************************************************
+
+ Synopsis [Recursively flattens the logic hierarchy of the netlist.]
+
+ Description [When this procedure is called, the PI/PO nets of the netlist
+ are already assigned.]
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+void Abc_NtkFlattenLogicHierarchy_rec( Abc_Ntk_t * pNtkNew, Abc_Ntk_t * pNtkOld, int * pCounter )
+{
+ Vec_Ptr_t * vNodes;
+ Abc_Ntk_t * pNtkModel;
+ Abc_Obj_t * pObj, * pTerm, * pFanin, * pNet;
+ int i, k;
+ (*pCounter)++;
+ // collect nodes and boxes in topological order
+ vNodes = Abc_NtkDfs( pNtkOld, 0 );
+ // duplicate nodes and blackboxes, call recursively for logic boxes
+ Vec_PtrForEachEntry( vNodes, pObj, i )
+ {
+ if ( Abc_ObjIsNode(pObj) )
+ {
+ // duplicate the node
+ Abc_NtkDupObj( pNtkNew, pObj, 0 );
+ Abc_ObjForEachFanin( pObj, pNet, k )
+ Abc_ObjAddFanin( pObj->pCopy, pNet->pCopy );
+ // duplicate the net
+ pNet = Abc_ObjFanout0( pObj );
+ pNet->pCopy = Abc_NtkFindOrCreateNet( pNtkNew, Abc_ObjName(pNet) );
+ Abc_ObjAddFanin( pNet->pCopy, pObj->pCopy );
+ continue;
+ }
+ if ( Abc_ObjIsBlackbox(pObj) )
+ {
+ // duplicate the box
+ Abc_NtkDupObj( pNtkNew, pObj, 1 );
+ // connect the fanins
+ Abc_ObjForEachFanin( pObj, pNet, k )
+ Abc_ObjAddFanin( pObj->pCopy, pNet->pCopy );
+ // duplicate fanout nets and connect them
+ Abc_ObjForEachFanout( pObj, pNet, i )
+ {
+ pNet->pCopy = Abc_NtkFindOrCreateNet( pNtkNew, Abc_ObjName(pNet) );
+ Abc_ObjAddFanin( pNet->pCopy, pObj->pCopy );
+ }
+ continue;
+ }
+ assert( Abc_ObjIsBox(pObj) );
+ pNtkModel = pObj->pData;
+ assert( pNtkModel && !Abc_NtkHasBlackbox(pNtkModel) );
+ // clean the node copy fields
+ Abc_NtkCleanCopy( pNtkModel );
+ // consider this blackbox
+ // copy the PIs/POs of the box
+ Abc_NtkForEachPi( pNtkModel, pTerm, k )
+ Abc_ObjFanout(pTerm, k)->pCopy = Abc_ObjFanin(pObj, k);
+ Abc_NtkForEachPo( pNtkModel, pTerm, k )
+ Abc_ObjFanin(pTerm, k)->pCopy = Abc_ObjFanout(pObj, k);
+ // call recursively
+ Abc_NtkFlattenLogicHierarchy_rec( pNtkNew, pNtkModel, pCounter );
+ }
+ // connect the POs
+ Abc_NtkForEachPo( pNtkOld, pTerm, k )
+ pTerm->pCopy = Abc_ObjFanin0(pTerm)->pCopy;
+ Vec_PtrFree( vNodes );
+}
+
+/**Function*************************************************************
+
+ Synopsis [Extracts blackboxes by making them into additional PIs/POs.]
Description []
@@ -47,6 +169,173 @@ struct Abc_Hie_t_
SeeAlso []
***********************************************************************/
+Abc_Ntk_t * Abc_NtkConvertBlackboxes( Abc_Ntk_t * pNtk )
+{
+ Abc_Ntk_t * pNtkNew;
+ Abc_Obj_t * pObj, * pNet;
+ int i, k;
+ assert( Abc_NtkIsNetlist(pNtk) );
+ assert( Abc_NtkBlackboxNum(pNtk) == Abc_NtkBoxNum(pNtk) - Abc_NtkLatchNum(pNtk) );
+ // start the network
+ pNtkNew = Abc_NtkAlloc( pNtk->ntkType, pNtk->ntkFunc, 1 );
+ // duplicate the name and the spec
+ pNtkNew->pName = Extra_UtilStrsav( pNtk->pName );
+ pNtkNew->pSpec = Extra_UtilStrsav( pNtk->pSpec );
+ // clean the node copy fields
+ Abc_NtkCleanCopy( pNtk );
+ // create PIs/POs for the box inputs outputs
+ Abc_NtkForEachBlackbox( pNtk, pObj, i )
+ {
+ pObj->pCopy = pObj; // placeholder
+ Abc_ObjForEachFanout( pObj, pNet, k )
+ {
+ if ( pNet->pCopy )
+ continue;
+ pNet->pCopy = Abc_NtkCreatePi( pNtkNew );
+ Abc_ObjAssignName( pNet->pCopy, Abc_ObjName(pNet), NULL );
+ }
+ Abc_ObjForEachFanin( pObj, pNet, k )
+ {
+ if ( pNet->pCopy )
+ continue;
+ pNet->pCopy = Abc_NtkCreatePo( pNtkNew );
+ Abc_ObjAssignName( pNet->pCopy, Abc_ObjName(pNet), NULL );
+ }
+ }
+ // duplicate other objects
+ Abc_NtkForEachObj( pNtk, pObj, i )
+ if ( pObj->pCopy == NULL )
+ Abc_NtkDupObj( pNtkNew, pObj, Abc_ObjIsNet(pObj) );
+ // connect all objects
+
+
+
+
+
+ // duplicate all objects besides the boxes
+ Abc_NtkForEachObj( pNtk, pObj, i )
+ if ( !Abc_ObjIsBlackbox(pObj) )
+ Abc_NtkDupObj( pNtkNew, pObj, Abc_ObjIsNet(pObj) );
+ // create PIs/POs for the nets belonging to the boxes
+ Abc_NtkForEachBlackbox( pNtk, pObj, i )
+ {
+ Abc_ObjForEachFanin( pObj, pNet, k )
+ if ( !Abc_ObjIsPi(Abc_ObjFanin0(pNet)) )
+ Abc_NtkCreatePi(pNtkNew)
+
+ }
+ // connect all objects, besides blackboxes
+ Abc_NtkForEachObj( pNtk, pObj, i )
+ {
+ if ( !Abc_ObjIsBlackbox(pObj) )
+ continue;
+ Abc_ObjForEachFanin( pObj, pNet, k )
+ Abc_ObjAddFanin( pObj->pCopy, pNet->pCopy );
+ }
+ if ( !Abc_NtkCheck( pNtkHie ) )
+ fprintf( stdout, "Abc_NtkInsertNewLogic(): Network check has failed.\n" );
+ return pNtkNew;
+}
+
+/**Function*************************************************************
+
+ Synopsis [Inserts blackboxes into the netlist.]
+
+ Description [The first arg is the netlist with blackboxes without logic hierarchy.
+ The second arg is a non-hierarchical netlist derived from logic network after processing.
+ This procedure inserts the logic back into the original hierarhical netlist.
+ The result is updated original hierarchical netlist.]
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+int Abc_NtkInsertNewLogic( Abc_Ntk_t * pNtkHie, Abc_Ntk_t * pNtk )
+{
+ Abc_Obj_t * pObj, * pNet, * pNetLogic;
+ int i, k;
+ assert( Abc_NtkIsNetlist(pNtkHie) );
+ assert( Abc_NtkIsNetlist(pNtk) );
+ assert( Abc_NtkBlackboxNum(pNtk) == 0 );
+ Abc_NtkCleanCopy( pNtk );
+ // mark PIs/POs/blackboxes and their nets
+ // map the nets into the corresponding nets of the logic design
+ Abc_NtkForEachPi( pNtkHie, pObj, i )
+ {
+ pObj->fMarkA = 1;
+ pNet = Abc_ObjFanout0(pObj);
+ pNet->fMarkA = 1;
+ pNetLogic = Abc_NtkFindNet( pNtk, Abc_ObjName(pNet) );
+ assert( pNetLogic );
+ pNetLogic->pCopy = pNet;
+ }
+ Abc_NtkForEachPo( pNtkHie, pObj, i )
+ {
+ pObj->fMarkA = 1;
+ pNet = Abc_ObjFanin0(pObj);
+ pNet->fMarkA = 1;
+ pNetLogic = Abc_NtkFindNet( pNtk, Abc_ObjName(pNet) );
+ assert( pNetLogic );
+ pNetLogic->pCopy = pNet;
+ }
+ Abc_NtkForEachBlackbox( pNtkHie, pObj, i )
+ {
+ pObj->fMarkA = 1;
+ Abc_ObjForEachFanin( pObj, pNet, k )
+ {
+ pNet->fMarkA = 1;
+ pNetLogic = Abc_NtkFindNet( pNtk, Abc_ObjName(pNet) );
+ assert( pNetLogic );
+ pNetLogic->pCopy = pNet;
+ }
+ Abc_ObjForEachFanout( pObj, pNet, k )
+ {
+ pNet->fMarkA = 1;
+ pNetLogic = Abc_NtkFindNet( pNtk, Abc_ObjName(pNet) );
+ assert( pNetLogic );
+ pNetLogic->pCopy = pNet;
+ }
+ }
+ // remove all other logic fro the hierarchical netlist
+ Abc_NtkForEachObj( pNtkHie, pObj, i )
+ {
+ if ( pObj->fMarkA )
+ pObj->fMarkA = 0;
+ else
+ Abc_NtkDeleteObj( pObj );
+ }
+ // mark PI/PO nets of the network
+ Abc_NtkForEachPi( pNtk, pObj, i )
+ Abc_ObjFanout0(pObj)->fMarkA = 1;
+ Abc_NtkForEachPo( pNtk, pObj, i )
+ Abc_ObjFanin0(pObj)->fMarkA = 1;
+ // make sure only these nodes are assigned the copy
+ Abc_NtkForEachObj( pNtk, pObj, i )
+ {
+ assert( pObj->fMarkA == (pObj->pCopy != NULL) );
+ pObj->fMarkA = 0;
+ if ( pObj->pCopy )
+ continue;
+ if ( Abc_ObjIsPi(pObj) || Abc_ObjIsPi(pObj) )
+ continue;
+ Abc_NtkDupObj( pNtkHie, pObj, 0 );
+ }
+ // connect all the nodes, except the PIs and POs
+ Abc_NtkForEachObj( pNtk, pObj, i )
+ {
+ if ( Abc_ObjIsPi(pObj) || Abc_ObjIsPi(pObj) )
+ continue;
+ Abc_ObjForEachFanin( pObj, pNet, k )
+ Abc_ObjAddFanin( pObj->pCopy, pNet->pCopy );
+ }
+ if ( !Abc_NtkCheck( pNtkHie ) )
+ {
+ fprintf( stdout, "Abc_NtkInsertNewLogic(): Network check has failed.\n" );
+ return 0;
+ }
+ return 1;
+}
////////////////////////////////////////////////////////////////////////
/// END OF FILE ///
diff --git a/src/base/abc/abcNetlist.c b/src/base/abc/abcNetlist.c
index 040a33df..2a20617c 100644
--- a/src/base/abc/abcNetlist.c
+++ b/src/base/abc/abcNetlist.c
@@ -25,8 +25,6 @@
/// DECLARATIONS ///
////////////////////////////////////////////////////////////////////////
-static Abc_Ntk_t * Abc_NtkNetlistToLogicHie( Abc_Ntk_t * pNtk );
-static void Abc_NtkNetlistToLogicHie_rec( Abc_Ntk_t * pNtkNew, Abc_Ntk_t * pNtkOld, int * pCounter );
static void Abc_NtkAddPoBuffers( Abc_Ntk_t * pNtk );
////////////////////////////////////////////////////////////////////////
@@ -51,8 +49,9 @@ Abc_Ntk_t * Abc_NtkNetlistToLogic( Abc_Ntk_t * pNtk )
int i, k;
assert( Abc_NtkIsNetlist(pNtk) );
// consider simple case when there is hierarchy
- if ( pNtk->tName2Model )
- return Abc_NtkNetlistToLogicHie( pNtk );
+ assert( pNtk->tName2Model == NULL );
+// if ( pNtk->tName2Model )
+// return Abc_NtkNetlistToLogicHie( pNtk );
// start the network
if ( Abc_NtkHasMapping(pNtk) )
pNtkNew = Abc_NtkStartFrom( pNtk, ABC_NTK_LOGIC, ABC_FUNC_MAP );
@@ -79,159 +78,6 @@ Abc_Ntk_t * Abc_NtkNetlistToLogic( Abc_Ntk_t * pNtk )
/**Function*************************************************************
- Synopsis [Transform the netlist into a logic network.]
-
- Description []
-
- SideEffects []
-
- SeeAlso []
-
-***********************************************************************/
-Abc_Ntk_t * Abc_NtkNetlistToLogicHie( Abc_Ntk_t * pNtk )
-{
- Abc_Ntk_t * pNtkNew;
- Abc_Obj_t * pObj;
- int i, Counter = 0;
- assert( Abc_NtkIsNetlist(pNtk) );
- // start the network
-// pNtkNew = Abc_NtkAlloc( Type, Func, 1 );
- if ( !Abc_NtkHasMapping(pNtk) )
- pNtkNew = Abc_NtkAlloc( ABC_NTK_LOGIC, ABC_FUNC_SOP, 1 );
- else
- pNtkNew = Abc_NtkAlloc( ABC_NTK_LOGIC, ABC_FUNC_MAP, 1 );
- // duplicate the name and the spec
- pNtkNew->pName = Extra_UtilStrsav(pNtk->pName);
- pNtkNew->pSpec = Extra_UtilStrsav(pNtk->pSpec);
- // clean the node copy fields
- Abc_NtkForEachNode( pNtk, pObj, i )
- pObj->pCopy = NULL;
- // clone PIs/POs/latches and make old nets point to new terminals; create names
- Abc_NtkForEachCi( pNtk, pObj, i )
- {
- Abc_ObjFanout0(pObj)->pCopy = Abc_NtkDupObj(pNtkNew, pObj, 0);
- Abc_ObjAssignName( pObj->pCopy, Abc_ObjName(Abc_ObjFanout0(pObj)), NULL );
- }
- Abc_NtkForEachPo( pNtk, pObj, i )
- {
- Abc_NtkDupObj(pNtkNew, pObj, 0);
- Abc_ObjAssignName( pObj->pCopy, Abc_ObjName(Abc_ObjFanin0(pObj)), NULL );
- }
- // recursively flatten hierarchy, create internal logic, add new PI/PO names if there are black boxes
- Abc_NtkNetlistToLogicHie_rec( pNtkNew, pNtk, &Counter );
- if ( Counter )
- printf( "Warning: The total of %d block boxes are transformed into PI/PO pairs.\n", Counter );
- // connect the CO nodes
- Abc_NtkForEachCo( pNtk, pObj, i )
- Abc_ObjAddFanin( pObj->pCopy, Abc_ObjFanin0(pObj)->pCopy );
- // copy the timing information
- Abc_ManTimeDup( pNtk, pNtkNew );
- // fix the problem with CO pointing directly to CIs
- Abc_NtkLogicMakeSimpleCos( pNtkNew, 0 );
- // duplicate EXDC
- if ( pNtk->pExdc )
- pNtkNew->pExdc = Abc_NtkNetlistToLogic( pNtk->pExdc );
- if ( !Abc_NtkCheck( pNtkNew ) )
- fprintf( stdout, "Abc_NtkNetlistToLogic(): Network check has failed.\n" );
- return pNtkNew;
-}
-
-/**Function*************************************************************
-
- Synopsis [Transform the netlist into a logic network.]
-
- Description []
-
- SideEffects []
-
- SeeAlso []
-
-***********************************************************************/
-void Abc_NtkNetlistToLogicHie_rec( Abc_Ntk_t * pNtkNew, Abc_Ntk_t * pNtkOld, int * pCounter )
-{
- char Prefix[1000];
- Vec_Ptr_t * vNodes;
- Abc_Ntk_t * pNtkModel;
- Abc_Obj_t * pNode, * pObj, * pFanin;
- int i, k;
- // collect nodes and boxes in topological order
- vNodes = Abc_NtkDfs( pNtkOld, 0 );
- // duplicate nodes, create PIs/POs corresponding to blackboxes
- // have to do it first if blackboxes break combinational loops
- // (current we do not allow whiteboxes to break combinational loops)
- Vec_PtrForEachEntry( vNodes, pNode, i )
- {
- if ( Abc_ObjIsNode(pNode) )
- {
- // duplicate the node and save it in the fanout net
- Abc_NtkDupObj( pNtkNew, pNode, 0 );
- Abc_ObjFanout0(pNode)->pCopy = pNode->pCopy;
- continue;
- }
- assert( Abc_ObjIsBox(pNode) );
- pNtkModel = pNode->pData;
- if ( !Abc_NtkHasBlackbox(pNtkModel) )
- continue;
- // consider this blockbox
- if ( pNtkNew->pBlackBoxes == NULL )
- {
- pNtkNew->pBlackBoxes = Vec_IntAlloc( 10 );
- Vec_IntPush( pNtkNew->pBlackBoxes, (Abc_NtkPiNum(pNtkNew) << 16) | Abc_NtkPoNum(pNtkNew) );
- }
- sprintf( Prefix, "%s_%d_", Abc_NtkName(pNtkModel), *pCounter );
- // create new PIs from the POs of the box
- Abc_NtkForEachPo( pNtkModel, pObj, k )
- {
- pObj->pCopy = Abc_NtkCreatePi( pNtkNew );
- Abc_ObjFanout(pNode, k)->pCopy = pObj->pCopy;
- Abc_ObjAssignName( pObj->pCopy, Prefix, Abc_ObjName(Abc_ObjFanin0(pObj)) );
- }
- // create new POs from the PIs of the box
- Abc_NtkForEachPi( pNtkModel, pObj, k )
- {
- pObj->pCopy = Abc_NtkCreatePo( pNtkNew );
-// Abc_ObjAddFanin( pObj->pCopy, Abc_ObjFanin(pNode, k)->pCopy );
- Abc_ObjAssignName( pObj->pCopy, Prefix, Abc_ObjName(Abc_ObjFanout0(pObj)) );
- }
- (*pCounter)++;
- Vec_IntPush( pNtkNew->pBlackBoxes, (Abc_NtkPiNum(pNtkNew) << 16) | Abc_NtkPoNum(pNtkNew) );
- }
- // connect nodes and boxes
- Vec_PtrForEachEntry( vNodes, pNode, i )
- {
- if ( Abc_ObjIsNode(pNode) )
- {
-// printf( "adding node %s\n", Abc_ObjName(Abc_ObjFanout0(pNode)) );
- Abc_ObjForEachFanin( pNode, pFanin, k )
- Abc_ObjAddFanin( pNode->pCopy, pFanin->pCopy );
- continue;
- }
- assert( Abc_ObjIsBox(pNode) );
- pNtkModel = pNode->pData;
-// printf( "adding model %s\n", Abc_NtkName(pNtkModel) );
- // consider the case of the black box
- if ( Abc_NtkHasBlackbox(pNtkModel) )
- {
- // create new POs from the PIs of the box
- Abc_NtkForEachPi( pNtkModel, pObj, k )
- Abc_ObjAddFanin( pObj->pCopy, Abc_ObjFanin(pNode, k)->pCopy );
- continue;
- }
- // transfer the nodes to the box inputs
- Abc_NtkForEachPi( pNtkModel, pObj, k )
- Abc_ObjFanout0(pObj)->pCopy = Abc_ObjFanin(pNode, k)->pCopy;
- // construct recursively
- Abc_NtkNetlistToLogicHie_rec( pNtkNew, pNtkModel, pCounter );
- // transfer the results back
- Abc_NtkForEachPo( pNtkModel, pObj, k )
- Abc_ObjFanout(pNode, k)->pCopy = Abc_ObjFanin0(pObj)->pCopy;
- }
- Vec_PtrFree( vNodes );
-}
-
-
-/**Function*************************************************************
-
Synopsis [Transform the logic network into a netlist.]
Description []
diff --git a/src/base/abc/abcObj.c b/src/base/abc/abcObj.c
index e434a51b..8d347404 100644
--- a/src/base/abc/abcObj.c
+++ b/src/base/abc/abcObj.c
@@ -327,7 +327,7 @@ Abc_Obj_t * Abc_NtkDupObj( Abc_Ntk_t * pNtkNew, Abc_Obj_t * pObj, int fCopyName
Abc_ObjAssignName( pObjNew, Abc_ObjName(Abc_ObjFanout0Ntk(pObj)), NULL );
else if ( Abc_ObjIsCo(pObj) )
Abc_ObjAssignName( pObjNew, Abc_ObjName(Abc_ObjFanin0Ntk(pObj)), NULL );
- else if ( Abc_ObjIsBox(pObj) )
+ else if ( Abc_ObjIsBox(pObj) || Abc_ObjIsNet(pObj) )
Abc_ObjAssignName( pObjNew, Abc_ObjName(pObj), NULL );
}
// copy functionality/names
@@ -350,8 +350,6 @@ Abc_Obj_t * Abc_NtkDupObj( Abc_Ntk_t * pNtkNew, Abc_Obj_t * pObj, int fCopyName
}
else if ( Abc_ObjIsNet(pObj) ) // copy the name
{
- assert( 0 );
-// pObjNew->pData = Nm_ManStoreIdName( pNtkNew->pManName, pObjNew->Id, pObj->pData, NULL );
}
else if ( Abc_ObjIsLatch(pObj) ) // copy the reset value
pObjNew->pData = pObj->pData;
diff --git a/src/base/abci/abc.c b/src/base/abci/abc.c
index 3a6874ca..f1ec7920 100644
--- a/src/base/abci/abc.c
+++ b/src/base/abci/abc.c
@@ -2577,13 +2577,14 @@ int Abc_CommandMfs( Abc_Frame_t * pAbc, int argc, char ** argv )
pErr = Abc_FrameReadErr(pAbc);
// set defaults
- pPars->nWindow = 33;
- pPars->nCands = 3;
- pPars->nSimWords = 8;
- pPars->fVerbose = 1;
+ pPars->nWindow = 62;
+ pPars->nCands = 5;
+ pPars->nSimWords = 4;
+ pPars->fArea = 0;
+ pPars->fVerbose = 0;
pPars->fVeryVerbose = 0;
Extra_UtilGetoptReset();
- while ( ( c = Extra_UtilGetopt( argc, argv, "WSvwh" ) ) != EOF )
+ while ( ( c = Extra_UtilGetopt( argc, argv, "WSavwh" ) ) != EOF )
{
switch ( c )
{
@@ -2609,6 +2610,9 @@ int Abc_CommandMfs( Abc_Frame_t * pAbc, int argc, char ** argv )
if ( pPars->nSimWords < 1 || pPars->nSimWords > 256 )
goto usage;
break;
+ case 'a':
+ pPars->fArea ^= 1;
+ break;
case 'v':
pPars->fVerbose ^= 1;
break;
@@ -2627,9 +2631,9 @@ int Abc_CommandMfs( Abc_Frame_t * pAbc, int argc, char ** argv )
fprintf( pErr, "Empty network.\n" );
return 1;
}
- if ( !Abc_NtkHasAig(pNtk) )
+ if ( !Abc_NtkIsLogic(pNtk) )
{
- fprintf( pErr, "This command can only be applied to AIG logic network (run \"aig\").\n" );
+ fprintf( pErr, "This command can only be applied to a logic network.\n" );
return 1;
}
@@ -2642,10 +2646,11 @@ int Abc_CommandMfs( Abc_Frame_t * pAbc, int argc, char ** argv )
return 0;
usage:
- fprintf( pErr, "usage: mfs [-W <NM>] [-S <num>] [-vwh]\n" );
+ fprintf( pErr, "usage: mfs [-W <NM>] [-S <num>] [-avwh]\n" );
fprintf( pErr, "\t performs resubstitution-based resynthesis with don't-cares\n" );
fprintf( pErr, "\t-W <NM> : Fanin/Fanout levels (NxM) of the window (00 <= NM <= 99) [default = %d%d]\n", pPars->nWindow/10, pPars->nWindow%10 );
fprintf( pErr, "\t-S <num> : the number of simulation words (1 <= n <= 256) [default = %d]\n", pPars->nSimWords );
+ fprintf( pErr, "\t-a : toggle optimization for area only [default = %s]\n", pPars->fArea? "yes": "no" );
fprintf( pErr, "\t-v : toggle verbose printout [default = %s]\n", pPars->fVerbose? "yes": "no" );
fprintf( pErr, "\t-w : toggle printout subgraph statistics [default = %s]\n", pPars->fVeryVerbose? "yes": "no" );
fprintf( pErr, "\t-h : print the command usage\n");
diff --git a/src/base/io/ioReadBlifMv.c b/src/base/io/ioReadBlifMv.c
index c55cc4c9..e6831dba 100644
--- a/src/base/io/ioReadBlifMv.c
+++ b/src/base/io/ioReadBlifMv.c
@@ -176,6 +176,8 @@ Abc_Lib_t * Io_ReadBlifMv( char * pFileName, int fBlifMv, int fCheck )
}
}
}
+// pDesign should be linked to all models of the design
+
Io_WriteBlifMvDesign( pDesign, "_temp_.mv" );
Abc_LibPrint( pDesign );
Abc_LibFree( pDesign );
@@ -637,7 +639,7 @@ static void Io_MvReadInterfaces( Io_MvMan_t * p )
/**Function*************************************************************
- Synopsis [Reads the AIG in the binary AIGER format.]
+ Synopsis []
Description []
diff --git a/src/misc/extra/extra.h b/src/misc/extra/extra.h
index 9dd494eb..0b48364d 100644
--- a/src/misc/extra/extra.h
+++ b/src/misc/extra/extra.h
@@ -112,6 +112,10 @@ typedef unsigned long long uint64;
#define PRT(a,t) printf("%s = ", (a)); printf("%6.2f sec\n", (float)(t)/(float)(CLOCKS_PER_SEC))
#endif
+#ifndef PRTP
+#define PRTP(a,t,T) printf("%s = ", (a)); printf("%6.2f sec (%6.2f %%)\n", (float)(t)/(float)(CLOCKS_PER_SEC), 100.0*(t)/(T))
+#endif
+
/*===========================================================================*/
/* Various Utilities */
/*===========================================================================*/
diff --git a/src/opt/bdc/bdc.h b/src/opt/bdc/bdc.h
index f0976bfe..71875edb 100644
--- a/src/opt/bdc/bdc.h
+++ b/src/opt/bdc/bdc.h
@@ -20,7 +20,7 @@
#ifndef __BDC_H__
#define __BDC_H__
-
+
#ifdef __cplusplus
extern "C" {
#endif
@@ -57,8 +57,8 @@ struct Bdc_Par_t_
/*=== bdcCore.c ==========================================================*/
extern Bdc_Man_t * Bdc_ManAlloc( Bdc_Par_t * pPars );
-extern void Bdc_ManAlloc( Bdc_Man_t * p );
-extern int Bdc_ManDecompose( Bdc_Man_t * p, unsigned * puFunc, unsigned * puCare, int nVars, Vec_Ptr_t * vDivs, int nNodeLimit );
+extern void Bdc_ManFree( Bdc_Man_t * p );
+extern int Bdc_ManDecompose( Bdc_Man_t * p, unsigned * puFunc, unsigned * puCare, int nVars, Vec_Ptr_t * vDivs, int nNodesLimit );
#ifdef __cplusplus
diff --git a/src/opt/bdc/bdcCore.c b/src/opt/bdc/bdcCore.c
index f120ac3f..157927b1 100644
--- a/src/opt/bdc/bdcCore.c
+++ b/src/opt/bdc/bdcCore.c
@@ -18,7 +18,6 @@
***********************************************************************/
-#include "abc.h"
#include "bdcInt.h"
////////////////////////////////////////////////////////////////////////
@@ -43,32 +42,50 @@
Bdc_Man_t * Bdc_ManAlloc( Bdc_Par_t * pPars )
{
Bdc_Man_t * p;
- int i;
+ unsigned * pData;
+ int i, k, nBits;
p = ALLOC( Bdc_Man_t, 1 );
memset( p, 0, sizeof(Bdc_Man_t) );
assert( pPars->nVarsMax > 3 && pPars->nVarsMax < 16 );
p->pPars = pPars;
+ p->nWords = Kit_TruthWordNum( pPars->nVarsMax );
+ p->nDivsLimit = 200;
+ p->nNodesLimit = 0; // will be set later
// memory
p->vMemory = Vec_IntStart( 1 << 16 );
// internal nodes
- p->nNodesAlloc = 256;
+ p->nNodesAlloc = 512;
p->pNodes = ALLOC( Bdc_Fun_t, p->nNodesAlloc );
// set up hash table
p->nTableSize = (1 << p->pPars->nVarsMax);
p->pTable = ALLOC( Bdc_Fun_t *, p->nTableSize );
memset( p->pTable, 0, sizeof(Bdc_Fun_t *) * p->nTableSize );
p->vSpots = Vec_IntAlloc( 256 );
- // set up constant 1 and elementary variables
- for ( i = 0; i < pPars->nVarsMax; i++ )
+ // truth tables
+ p->vTruths = Vec_PtrAllocSimInfo( pPars->nVarsMax + 5, p->nWords );
+ // set elementary truth tables
+ nBits = (1 << pPars->nVarsMax);
+ Kit_TruthFill( Vec_PtrEntry(p->vTruths, 0), p->nVars );
+ for ( k = 0; k < pPars->nVarsMax; k++ )
{
+ pData = Vec_PtrEntry( p->vTruths, k+1 );
+ Kit_TruthClear( pData, p->nVars );
+ for ( i = 0; i < nBits; i++ )
+ if ( i & (1 << k) )
+ pData[i>>5] |= (1 << (i&31));
}
- p->nNodes = pPars->nVarsMax + 1;
- // remember the current place in memory
- p->nMemStart = Vec_IntSize( p->vMemory );
+ p->puTemp1 = Vec_PtrEntry( p->vTruths, pPars->nVarsMax + 1 );
+ p->puTemp2 = Vec_PtrEntry( p->vTruths, pPars->nVarsMax + 2 );
+ p->puTemp3 = Vec_PtrEntry( p->vTruths, pPars->nVarsMax + 3 );
+ p->puTemp4 = Vec_PtrEntry( p->vTruths, pPars->nVarsMax + 4 );
+ // start the internal ISFs
+ p->pIsfOL = &p->IsfOL; Bdc_IsfStart( p, p->pIsfOL );
+ p->pIsfOR = &p->IsfOR; Bdc_IsfStart( p, p->pIsfOR );
+ p->pIsfAL = &p->IsfAL; Bdc_IsfStart( p, p->pIsfAL );
+ p->pIsfAR = &p->IsfAR; Bdc_IsfStart( p, p->pIsfAR );
return p;
}
-
/**Function*************************************************************
Synopsis [Deallocate resynthesis manager.]
@@ -80,15 +97,21 @@ Bdc_Man_t * Bdc_ManAlloc( Bdc_Par_t * pPars )
SeeAlso []
***********************************************************************/
-void Bdc_ManAlloc( Bdc_Man_t * p )
+void Bdc_ManFree( Bdc_Man_t * p )
{
+ Vec_IntFree( p->vMemory );
+ Vec_IntFree( p->vSpots );
+ Vec_PtrFree( p->vTruths );
+ free( p->pNodes );
+ free( p->pTable );
+ free( p );
}
/**Function*************************************************************
- Synopsis [Sets up the divisors.]
+ Synopsis [Clears the manager.]
- Description [The first n+1 entries are const1 and elem variables.]
+ Description []
SideEffects []
@@ -97,23 +120,31 @@ void Bdc_ManAlloc( Bdc_Man_t * p )
***********************************************************************/
void Bdc_ManPrepare( Bdc_Man_t * p, Vec_Ptr_t * vDivs )
{
- Bdc_Fun_t ** pSpot, * pFunc;
unsigned * puTruth;
+ Bdc_Fun_t * pNode;
int i;
- // clean hash table
- Vec_PtrForEachEntry( p->vSpots, pSpot, i )
- *pSpot = NULL;
- // reset nodes
- p->nNodes = p->pPars->nVarsMax + 1;
- // reset memory
- Vec_IntShrink( p->vMemory, p->nMemStart );
- // add new nodes to the hash table
+ Bdc_TableClear( p );
+ Vec_IntClear( p->vMemory );
+ // add constant 1 and elementary vars
+ p->nNodes = p->nNodesNew = 0;
+ for ( i = 0; i <= p->pPars->nVarsMax; i++ )
+ {
+ pNode = Bdc_FunNew( p );
+ pNode->Type = BDC_TYPE_PI;
+ pNode->puFunc = Vec_PtrEntry( p->vTruths, i );
+ pNode->uSupp = i? (1 << (i-1)) : 0;
+ Bdc_TableAdd( p, pNode );
+ }
+ // add the divisors
Vec_PtrForEachEntry( vDivs, puTruth, i )
{
- pFunc = Bdc_ManNewNode( p );
- pFunc->Type = BDC_TYPE_PI;
- pFunc->puFunc = puTruth;
- pFunc->uSupp = Kit_TruthSupport( puTruth, p->nVars );
+ pNode = Bdc_FunNew( p );
+ pNode->Type = BDC_TYPE_PI;
+ pNode->puFunc = puTruth;
+ pNode->uSupp = Kit_TruthSupport( puTruth, p->nVars );
+ Bdc_TableAdd( p, pNode );
+ if ( i == p->nDivsLimit )
+ break;
}
}
@@ -128,25 +159,26 @@ void Bdc_ManPrepare( Bdc_Man_t * p, Vec_Ptr_t * vDivs )
SeeAlso []
***********************************************************************/
-int Bdc_ManDecompose( Bdc_Man_t * p, unsigned * puFunc, unsigned * puCare, int nVars, Vec_Ptr_t * vDivs, int nNodeLimit )
+int Bdc_ManDecompose( Bdc_Man_t * p, unsigned * puFunc, unsigned * puCare, int nVars, Vec_Ptr_t * vDivs, int nNodesMax )
{
Bdc_Isf_t Isf, * pIsf = &Isf;
// set current manager parameters
p->nVars = nVars;
p->nWords = Kit_TruthWordNum( nVars );
- p->nNodeLimit = nNodeLimit;
Bdc_ManPrepare( p, vDivs );
+ p->nNodesLimit = (p->nNodes + nNodesMax < p->nNodesAlloc)? p->nNodes + nNodesMax : p->nNodesAlloc;
// copy the function
+ Bdc_IsfStart( p, pIsf );
+ Bdc_IsfClean( pIsf );
pIsf->uSupp = Kit_TruthSupport( puFunc, p->nVars ) | Kit_TruthSupport( puCare, p->nVars );
- pIsf->puOn = Vec_IntFetch( p->vMemory, p->nWords );
- pIsf->puOff = Vec_IntFetch( p->vMemory, p->nWords );
Kit_TruthAnd( pIsf->puOn, puCare, puFunc, p->nVars );
Kit_TruthSharp( pIsf->puOff, puCare, puFunc, p->nVars );
// call decomposition
+ Bdc_SuppMinimize( p, pIsf );
p->pRoot = Bdc_ManDecompose_rec( p, pIsf );
if ( p->pRoot == NULL )
return -1;
- return p->nNodes - (p->pPars->nVarsMax + 1);
+ return p->nNodesNew;
}
diff --git a/src/opt/bdc/bdcDec.c b/src/opt/bdc/bdcDec.c
index 1fbea911..747fcb14 100644
--- a/src/opt/bdc/bdcDec.c
+++ b/src/opt/bdc/bdcDec.c
@@ -1,12 +1,12 @@
/**CFile****************************************************************
- FileName [bdc_.c]
+ FileName [bdcDec.c]
SystemName [ABC: Logic synthesis and verification system.]
PackageName [Truth-table-based bi-decomposition engine.]
- Synopsis []
+ Synopsis [Decomposition procedures.]
Author [Alan Mishchenko]
@@ -14,17 +14,19 @@
Date [Ver. 1.0. Started - January 30, 2007.]
- Revision [$Id: bdc_.c,v 1.00 2007/01/30 00:00:00 alanmi Exp $]
+ Revision [$Id: bdcDec.c,v 1.00 2007/01/30 00:00:00 alanmi Exp $]
***********************************************************************/
-#include "abc.h"
#include "bdcInt.h"
////////////////////////////////////////////////////////////////////////
/// DECLARATIONS ///
////////////////////////////////////////////////////////////////////////
+static Bdc_Type_t Bdc_DecomposeStep( Bdc_Man_t * p, Bdc_Isf_t * pIsf, Bdc_Isf_t * pIsfL, Bdc_Isf_t * pIsfR );
+static int Bdc_DecomposeUpdateRight( Bdc_Man_t * p, Bdc_Isf_t * pIsf, Bdc_Isf_t * pIsfL, Bdc_Isf_t * pIsfR, unsigned * puTruth, Bdc_Type_t Type );
+
////////////////////////////////////////////////////////////////////////
/// FUNCTION DEFINITIONS ///
////////////////////////////////////////////////////////////////////////
@@ -43,31 +45,414 @@
Bdc_Fun_t * Bdc_ManDecompose_rec( Bdc_Man_t * p, Bdc_Isf_t * pIsf )
{
Bdc_Fun_t * pFunc;
- Bdc_Isf_t IsfA, * pIsfA = &IsfA;
- Bdc_Isf_t IsfB, * pIsfB = &IsfB;
- int Type;
- Bdc_SuppMinimize( p, pIsf );
+ Bdc_Isf_t IsfL, * pIsfL = &IsfL;
+ Bdc_Isf_t IsfB, * pIsfR = &IsfB;
+ // check computed results
if ( pFunc = Bdc_TableLookup( p, pIsf ) )
return pFunc;
- pFunc = Bdc_ManNewNode( p );
- pFunc->Type = Bdc_DecomposeStep( p, pIsf, pIsfA, pIsfB );
- pFunc->pFan0 = Bdc_ManDecompose_rec( p, pIsfA );
- if ( Bdc_DecomposeUpdateRight( p, pIsf, pIsfA, pIsfB, pFunc->pFan0->puFunc ) )
+ // decide on the decomposition type
+ pFunc = Bdc_FunNew( p );
+ if ( pFunc == NULL )
+ return NULL;
+ pFunc->Type = Bdc_DecomposeStep( p, pIsf, pIsfL, pIsfR );
+ // decompose the left branch
+ pFunc->pFan0 = Bdc_ManDecompose_rec( p, pIsfL );
+ if ( pFunc->pFan0 == NULL )
+ return NULL;
+ // decompose the right branch
+ if ( Bdc_DecomposeUpdateRight( p, pIsf, pIsfL, pIsfR, pFunc->pFan0->puFunc, pFunc->Type ) )
{
p->nNodes--;
return pFunc->pFan0;
}
- pFunc->pFan1 = Bdc_ManDecompose_rec( p, pIsfA );
- pFunc->puFunc = Vec_IntFetch( p->vMemory, p->nWords );
- pFunc->puFunc =
+ pFunc->pFan1 = Bdc_ManDecompose_rec( p, pIsfL );
+ if ( pFunc->pFan1 == NULL )
+ return NULL;
+ // compute the function of node
+ pFunc->puFunc = (unsigned *)Vec_IntFetch(p->vMemory, p->nWords);
+ if ( pFunc->Type == BDC_TYPE_AND )
+ Kit_TruthAnd( pFunc->puFunc, pFunc->pFan0->puFunc, pFunc->pFan1->puFunc, p->nVars );
+ else if ( pFunc->Type == BDC_TYPE_OR )
+ Kit_TruthOr( pFunc->puFunc, pFunc->pFan0->puFunc, pFunc->pFan1->puFunc, p->nVars );
+ else
+ assert( 0 );
+ // verify correctness
+ assert( Bdc_TableCheckContainment(p, pIsf, pFunc->puFunc) );
+ // convert from OR to AND
+ if ( pFunc->Type == BDC_TYPE_OR )
+ {
+ pFunc->Type = BDC_TYPE_AND;
+ pFunc->pFan0 = Bdc_Not(pFunc->pFan0);
+ pFunc->pFan1 = Bdc_Not(pFunc->pFan1);
+ Kit_TruthNot( pFunc->puFunc, pFunc->puFunc, p->nVars );
+ pFunc = Bdc_Not(pFunc);
+ }
+ Bdc_TableAdd( p, Bdc_Regular(pFunc) );
+ return pFunc;
+}
+
+/**Function*************************************************************
+
+ Synopsis [Updates the ISF of the right after the left was decompoosed.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+int Bdc_DecomposeUpdateRight( Bdc_Man_t * p, Bdc_Isf_t * pIsf, Bdc_Isf_t * pIsfL, Bdc_Isf_t * pIsfR, unsigned * puTruth, Bdc_Type_t Type )
+{
+ if ( Type == BDC_TYPE_OR )
+ {
+// Right.Q = bdd_appex( Q, CompSpecLeftF, bddop_diff, setRightRes );
+// Right.R = bdd_exist( R, setRightRes );
+
+// if ( pR->Q ) Cudd_RecursiveDeref( dd, pR->Q );
+// if ( pR->R ) Cudd_RecursiveDeref( dd, pR->R );
+// pR->Q = Cudd_bddAndAbstract( dd, pF->Q, Cudd_Not(CompSpecF), pL->V ); Cudd_Ref( pR->Q );
+// pR->R = Cudd_bddExistAbstract( dd, pF->R, pL->V ); Cudd_Ref( pR->R );
+
+// assert( pR->R != b0 );
+// return (int)( pR->Q == b0 );
+
+ Kit_TruthSharp( pIsfR->puOn, pIsf->puOn, puTruth, p->nVars );
+ Kit_TruthExistSet( pIsfR->puOn, pIsfR->puOn, p->nVars, pIsfL->uSupp );
+ Kit_TruthExistSet( pIsfR->puOff, pIsf->puOff, p->nVars, pIsfL->uSupp );
+ assert( !Kit_TruthIsConst0(pIsfR->puOff, p->nVars) );
+ return Kit_TruthIsConst0(pIsfR->puOn, p->nVars);
+ }
+ else if ( Type == BDC_TYPE_AND )
+ {
+// Right.R = bdd_appex( R, CompSpecLeftF, bddop_and, setRightRes );
+// Right.Q = bdd_exist( Q, setRightRes );
+
+// if ( pR->Q ) Cudd_RecursiveDeref( dd, pR->Q );
+// if ( pR->R ) Cudd_RecursiveDeref( dd, pR->R );
+// pR->R = Cudd_bddAndAbstract( dd, pF->R, CompSpecF, pL->V ); Cudd_Ref( pR->R );
+// pR->Q = Cudd_bddExistAbstract( dd, pF->Q, pL->V ); Cudd_Ref( pR->Q );
+
+// assert( pR->Q != b0 );
+// return (int)( pR->R == b0 );
+
+ Kit_TruthSharp( pIsfR->puOn, pIsf->puOn, puTruth, p->nVars );
+ Kit_TruthExistSet( pIsfR->puOn, pIsfR->puOn, p->nVars, pIsfL->uSupp );
+ Kit_TruthExistSet( pIsfR->puOff, pIsf->puOff, p->nVars, pIsfL->uSupp );
+ assert( !Kit_TruthIsConst0(pIsfR->puOff, p->nVars) );
+ return Kit_TruthIsConst0(pIsfR->puOn, p->nVars);
+ }
+ return 0;
+}
+
+/**Function*************************************************************
+
+ Synopsis [Checks existence of OR-bidecomposition.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+static inline int Bdc_DecomposeGetCost( Bdc_Man_t * p, int nLeftVars, int nRightVars )
+{
+ assert( nLeftVars > 0 );
+ assert( nRightVars > 0 );
+ // compute the decomposition coefficient
+ if ( nLeftVars >= nRightVars )
+ return BDC_SCALE * (p->nVars * nRightVars + nLeftVars);
+ else // if ( nLeftVars < nRightVars )
+ return BDC_SCALE * (p->nVars * nLeftVars + nRightVars);
+}
+
+/**Function*************************************************************
+
+ Synopsis [Checks existence of weak OR-bidecomposition.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+int Bdc_DecomposeFindInitialVarSet( Bdc_Man_t * p, Bdc_Isf_t * pIsf, Bdc_Isf_t * pIsfL, Bdc_Isf_t * pIsfR )
+{
+ char pVars[16];
+ int v, nVars, Beg, End;
+
+ assert( pIsfL->uSupp == 0 );
+ assert( pIsfR->uSupp == 0 );
+
+ // fill in the variables
+ nVars = 0;
+ for ( v = 0; v < p->nVars; v++ )
+ if ( pIsf->uSupp & (1 << v) )
+ pVars[nVars++] = v;
+
+ // try variable pairs
+ for ( Beg = 0; Beg < nVars; Beg++ )
+ {
+ Kit_TruthExistNew( p->puTemp1, pIsf->puOff, p->nVars, pVars[Beg] );
+ for ( End = nVars - 1; End > Beg; End-- )
+ {
+ Kit_TruthExistNew( p->puTemp2, pIsf->puOff, p->nVars, pVars[End] );
+ if ( Kit_TruthIsDisjoint3(pIsf->puOn, p->puTemp1, p->puTemp2, p->nVars) )
+ {
+ pIsfL->uSupp = (1 << Beg);
+ pIsfR->uSupp = (1 << End);
+ pIsfL->Var = Beg;
+ pIsfR->Var = End;
+ return 1;
+ }
+ }
+ }
+ return 0;
+}
+
+/**Function*************************************************************
+
+ Synopsis [Checks existence of weak OR-bidecomposition.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+int Bdc_DecomposeWeakOr( Bdc_Man_t * p, Bdc_Isf_t * pIsf, Bdc_Isf_t * pIsfL, Bdc_Isf_t * pIsfR )
+{
+ int v, VarCost, VarBest, Cost, VarCostBest = 0;
+
+ for ( v = 0; v < p->nVars; v++ )
+ {
+ Kit_TruthExistNew( p->puTemp1, pIsf->puOff, p->nVars, v );
+// if ( (Q & !bdd_exist( R, VarSetXa )) != bddfalse )
+// Exist = Cudd_bddExistAbstract( dd, pF->R, Var ); Cudd_Ref( Exist );
+// if ( Cudd_bddIteConstant( dd, pF->Q, Cudd_Not(Exist), b0 ) != b0 )
+ if ( !Kit_TruthIsImply( pIsf->puOn, p->puTemp1, p->nVars ) )
+ {
+ // measure the cost of this variable
+// VarCost = bdd_satcountset( bdd_forall( Q, VarSetXa ), VarCube );
+
+// Univ = Cudd_bddUnivAbstract( dd, pF->Q, Var ); Cudd_Ref( Univ );
+// VarCost = Kit_TruthCountOnes( Univ, p->nVars );
+// Cudd_RecursiveDeref( dd, Univ );
+
+ Kit_TruthForallNew( p->puTemp2, pIsf->puOn, p->nVars, v );
+ VarCost = Kit_TruthCountOnes( p->puTemp2, p->nVars );
+ if ( VarCost == 0 )
+ VarCost = 1;
+ if ( VarCostBest < VarCost )
+ {
+ VarCostBest = VarCost;
+ VarBest = v;
+ }
+ }
+ }
+
+ // derive the components for weak-bi-decomposition if the variable is found
+ if ( VarCostBest )
+ {
+// funQLeftRes = Q & bdd_exist( R, setRightORweak );
+
+// Temp = Cudd_bddExistAbstract( dd, pF->R, VarBest ); Cudd_Ref( Temp );
+// pL->Q = Cudd_bddAnd( dd, pF->Q, Temp ); Cudd_Ref( pL->Q );
+// Cudd_RecursiveDeref( dd, Temp );
+
+ Kit_TruthExistNew( p->puTemp1, pIsf->puOff, p->nVars, VarBest );
+ Kit_TruthAnd( pIsfL->puOn, pIsf->puOn, p->puTemp1, p->nVars );
+
+// pL->R = pF->R; Cudd_Ref( pL->R );
+// pL->V = VarBest; Cudd_Ref( pL->V );
+ Kit_TruthCopy( pIsfL->puOff, pIsf->puOff, p->nVars );
+ pIsfL->Var = VarBest;
+
+// assert( pL->Q != b0 );
+// assert( pL->R != b0 );
+// assert( Cudd_bddIteConstant( dd, pL->Q, pL->R, b0 ) == b0 );
+
+ // express cost in percents of the covered boolean space
+ Cost = VarCostBest * BDC_SCALE / (1<<p->nVars);
+ if ( Cost == 0 )
+ Cost = 1;
+ return Cost;
+ }
+ return 0;
+}
+
+/**Function*************************************************************
+
+ Synopsis [Checks existence of OR-bidecomposition.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+int Bdc_DecomposeOr( Bdc_Man_t * p, Bdc_Isf_t * pIsf, Bdc_Isf_t * pIsfL, Bdc_Isf_t * pIsfR )
+{
+ unsigned uSuppRem;
+ int v, nLeftVars = 1, nRightVars = 1;
+ // clean the var sets
+ Bdc_IsfClean( pIsfL );
+ Bdc_IsfClean( pIsfR );
+ // find initial variable sets
+ if ( !Bdc_DecomposeFindInitialVarSet( p, pIsf, pIsfL, pIsfR ) )
+ return Bdc_DecomposeWeakOr( p, pIsf, pIsfL, pIsfR );
+ // prequantify the variables in the offset
+ Kit_TruthExistNew( p->puTemp1, pIsf->puOff, p->nVars, pIsfL->Var );
+ Kit_TruthExistNew( p->puTemp2, pIsf->puOff, p->nVars, pIsfR->Var );
+ // go through the remaining variables
+ uSuppRem = pIsf->uSupp & ~pIsfL->uSupp & ~pIsfR->uSupp;
+ assert( Kit_WordCountOnes(uSuppRem) > 0 );
+ for ( v = 0; v < p->nVars; v++ )
+ {
+ if ( (uSuppRem & (1 << v)) == 0 )
+ continue;
+ // prequantify this variable
+ Kit_TruthExistNew( p->puTemp3, p->puTemp1, p->nVars, v );
+ Kit_TruthExistNew( p->puTemp4, p->puTemp2, p->nVars, v );
+ if ( nLeftVars < nRightVars )
+ {
+// if ( (Q & bdd_exist( pF->R, pL->V & VarNew ) & bdd_exist( pF->R, pR->V )) == bddfalse )
+// if ( VerifyORCondition( dd, pF->Q, pF->R, pL->V, pR->V, VarNew ) )
+ if ( Kit_TruthIsDisjoint3(pIsf->puOn, p->puTemp3, p->puTemp2, p->nVars) )
+ {
+// pL->V &= VarNew;
+ pIsfL->uSupp |= (1 << v);
+ nLeftVars++;
+ }
+// else if ( (Q & bdd_exist( pF->R, pR->V & VarNew ) & bdd_exist( pF->R, pL->V )) == bddfalse )
+ else if ( Kit_TruthIsDisjoint3(pIsf->puOn, p->puTemp4, p->puTemp1, p->nVars) )
+ {
+// pR->V &= VarNew;
+ pIsfR->uSupp |= (1 << v);
+ nRightVars++;
+ }
+ }
+ else
+ {
+// if ( (Q & bdd_exist( pF->R, pR->V & VarNew ) & bdd_exist( pF->R, pL->V )) == bddfalse )
+ if ( Kit_TruthIsDisjoint3(pIsf->puOn, p->puTemp4, p->puTemp1, p->nVars) )
+ {
+// pR->V &= VarNew;
+ pIsfR->uSupp |= (1 << v);
+ nRightVars++;
+ }
+// else if ( (Q & bdd_exist( pF->R, pL->V & VarNew ) & bdd_exist( pF->R, pR->V )) == bddfalse )
+ else if ( Kit_TruthIsDisjoint3(pIsf->puOn, p->puTemp3, p->puTemp2, p->nVars) )
+ {
+// pL->V &= VarNew;
+ pIsfL->uSupp |= (1 << v);
+ nLeftVars++;
+ }
+ }
+ }
+
+ // derive the functions Q and R for the left branch
+// pL->Q = bdd_appex( pF->Q, bdd_exist( pF->R, pL->V ), bddop_and, pR->V );
+// pL->R = bdd_exist( pF->R, pR->V );
+// Temp = Cudd_bddExistAbstract( dd, pF->R, pL->V ); Cudd_Ref( Temp );
+// pL->Q = Cudd_bddAndAbstract( dd, pF->Q, Temp, pR->V ); Cudd_Ref( pL->Q );
+// Cudd_RecursiveDeref( dd, Temp );
+// pL->R = Cudd_bddExistAbstract( dd, pF->R, pR->V ); Cudd_Ref( pL->R );
+ Kit_TruthAnd( pIsfL->puOn, pIsf->puOn, p->puTemp1, p->nVars );
+ Kit_TruthExistSet( pIsfL->puOn, pIsfL->puOn, p->nVars, pIsfR->uSupp );
+ Kit_TruthCopy( pIsfL->puOff, p->puTemp2, p->nVars );
+ // derive the functions Q and R for the right branch
+// Temp = Cudd_bddExistAbstract( dd, pF->R, pR->V ); Cudd_Ref( Temp );
+// pR->Q = Cudd_bddAndAbstract( dd, pF->Q, Temp, pL->V ); Cudd_Ref( pR->Q );
+// Cudd_RecursiveDeref( dd, Temp );
+// pR->R = Cudd_bddExistAbstract( dd, pF->R, pL->V ); Cudd_Ref( pR->R );
+/*
+ Kit_TruthAnd( pIsfR->puOn, pIsf->puOn, p->puTemp2, p->nVars );
+ Kit_TruthExistSet( pIsfR->puOn, pIsfR->puOn, p->nVars, pIsfL->uSupp );
+ Kit_TruthCopy( pIsfR->puOff, p->puTemp1, p->nVars );
+*/
+// assert( pL->Q != b0 );
+// assert( pL->R != b0 );
+// assert( Cudd_bddIteConstant( dd, pL->Q, pL->R, b0 ) == b0 );
+ assert( !Kit_TruthIsConst0(pIsfL->puOn, p->nVars) );
+ assert( !Kit_TruthIsConst0(pIsfL->puOff, p->nVars) );
+ assert( Kit_TruthIsDisjoint(pIsfL->puOn, pIsfL->puOff, p->nVars) );
+
+ return Bdc_DecomposeGetCost( p, nLeftVars, nRightVars );
}
+/**Function*************************************************************
+
+ Synopsis [Performs one step of bi-decomposition.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+***********************************************************************/
+Bdc_Type_t Bdc_DecomposeStep( Bdc_Man_t * p, Bdc_Isf_t * pIsf, Bdc_Isf_t * pIsfL, Bdc_Isf_t * pIsfR )
+{
+ int CostOr, CostAnd, CostOrL, CostOrR, CostAndL, CostAndR;
+
+ Bdc_IsfClean( p->pIsfOL );
+ Bdc_IsfClean( p->pIsfOR );
+ Bdc_IsfClean( p->pIsfAL );
+ Bdc_IsfClean( p->pIsfAR );
+
+ // perform OR decomposition
+ CostOr = Bdc_DecomposeOr( p, pIsf, p->pIsfOL, p->pIsfOR );
+
+ // perform AND decomposition
+ Bdc_IsfNot( pIsf );
+ CostAnd = Bdc_DecomposeOr( p, pIsf, p->pIsfAL, p->pIsfAR );
+ Bdc_IsfNot( pIsf );
+ Bdc_IsfNot( p->pIsfAL );
+ Bdc_IsfNot( p->pIsfAR );
+
+ // check the hash table
+ Bdc_SuppMinimize( p, p->pIsfOL );
+ CostOrL = (Bdc_TableLookup(p, p->pIsfOL) != NULL);
+ Bdc_SuppMinimize( p, p->pIsfOR );
+ CostOrR = (Bdc_TableLookup(p, p->pIsfOR) != NULL);
+ Bdc_SuppMinimize( p, p->pIsfAL );
+ CostAndL = (Bdc_TableLookup(p, p->pIsfAL) != NULL);
+ Bdc_SuppMinimize( p, p->pIsfAR );
+ CostAndR = (Bdc_TableLookup(p, p->pIsfAR) != NULL);
+
+ // check if there is any reuse for the components
+ if ( CostOrL + CostOrR < CostAndL + CostAndR )
+ {
+ Bdc_IsfCopy( pIsfL, p->pIsfOL );
+ Bdc_IsfCopy( pIsfR, p->pIsfOR );
+ return BDC_TYPE_OR;
+ }
+ if ( CostOrL + CostOrR > CostAndL + CostAndR )
+ {
+ Bdc_IsfCopy( pIsfL, p->pIsfAL );
+ Bdc_IsfCopy( pIsfR, p->pIsfAR );
+ return BDC_TYPE_AND;
+ }
+
+ // compare the two-component costs
+ if ( CostOr < CostAnd )
+ {
+ Bdc_IsfCopy( pIsfL, p->pIsfOL );
+ Bdc_IsfCopy( pIsfR, p->pIsfOR );
+ return BDC_TYPE_OR;
+ }
+ return BDC_TYPE_AND;
+}
////////////////////////////////////////////////////////////////////////
/// END OF FILE ///
diff --git a/src/opt/bdc/bdcInt.h b/src/opt/bdc/bdcInt.h
index 39d50ae9..65ab9d27 100644
--- a/src/opt/bdc/bdcInt.h
+++ b/src/opt/bdc/bdcInt.h
@@ -29,13 +29,15 @@ extern "C" {
/// INCLUDES ///
////////////////////////////////////////////////////////////////////////
-#include "dec.h"
+#include "kit.h"
#include "bdc.h"
////////////////////////////////////////////////////////////////////////
/// PARAMETERS ///
////////////////////////////////////////////////////////////////////////
+#define BDC_SCALE 100 // value used to compute the cost
+
////////////////////////////////////////////////////////////////////////
/// BASIC TYPES ///
////////////////////////////////////////////////////////////////////////
@@ -46,18 +48,19 @@ typedef enum {
BDC_TYPE_CONST1, // 1: constant 1
BDC_TYPE_PI, // 2: primary input
BDC_TYPE_AND, // 4: AND-gate
- BDC_TYPE_XOR, // 5: XOR-gate
- BDC_TYPE_MUX, // 6: MUX-gate
- BDC_TYPE_OTHER // 7: unused
+ BDC_TYPE_OR, // 5: OR-gate (temporary)
+ BDC_TYPE_XOR, // 6: XOR-gate
+ BDC_TYPE_MUX, // 7: MUX-gate
+ BDC_TYPE_OTHER // 8: unused
} Bdc_Type_t;
typedef struct Bdc_Fun_t_ Bdc_Fun_t;
struct Bdc_Fun_t_
{
int Type; // Const1, PI, AND, XOR, MUX
- Bdc_Fun_t * pFan0; // next function with same support
- Bdc_Fun_t * pFan1; // next function with same support
- Bdc_Fun_t * pFan2; // next function with same support
+ Bdc_Fun_t * pFan0; // fanin of the given node
+ Bdc_Fun_t * pFan1; // fanin of the given node
+ Bdc_Fun_t * pFan2; // fanin of the given node
unsigned uSupp; // bit mask of current support
unsigned * puFunc; // the function of the node
Bdc_Fun_t * pNext; // next function with same support
@@ -67,11 +70,10 @@ struct Bdc_Fun_t_
typedef struct Bdc_Isf_t_ Bdc_Isf_t;
struct Bdc_Isf_t_
{
- unsigned uSupp; // bit mask of current support
- unsigned uUnique; // bit mask of unique support
+ int Var; // the first variable assigned
+ unsigned uSupp; // the current support
unsigned * puOn; // on-set
unsigned * puOff; // off-set
- int Cost; // cost of this component
};
typedef struct Bdc_Man_t_ Bdc_Man_t;
@@ -81,25 +83,44 @@ struct Bdc_Man_t_
Bdc_Par_t * pPars; // parameter set
int nVars; // the number of variables
int nWords; // the number of words
- int nNodeLimit; // the limit on the number of new nodes
+ int nNodesLimit; // the limit on the number of new nodes
+ int nDivsLimit; // the limit on the number of divisors
// internal nodes
Bdc_Fun_t * pNodes; // storage for decomposition nodes
int nNodes; // the number of nodes used
+ int nNodesNew; // the number of nodes used
int nNodesAlloc; // the number of nodes allocated
Bdc_Fun_t * pRoot; // the root node
// resub candidates
Bdc_Fun_t ** pTable; // hash table of candidates
int nTableSize; // hash table size (1 << nVarsMax)
+ Vec_Int_t * vSpots; // the occupied spots in the table
+ // elementary truth tables
+ Vec_Ptr_t * vTruths; // for const 1 and elementary variables
+ unsigned * puTemp1; // temporary truth table
+ unsigned * puTemp2; // temporary truth table
+ unsigned * puTemp3; // temporary truth table
+ unsigned * puTemp4; // temporary truth table
+ // temporary ISFs
+ Bdc_Isf_t * pIsfOL, IsfOL;
+ Bdc_Isf_t * pIsfOR, IsfOR;
+ Bdc_Isf_t * pIsfAL, IsfAL;
+ Bdc_Isf_t * pIsfAR, IsfAR;
// internal memory manager
Vec_Int_t * vMemory; // memory for internal truth tables
- int nMemStart; // the starting memory size
};
// working with complemented attributes of objects
-static inline bool Bdc_IsComplement( Bdc_Fun_t * p ) { return (bool)((unsigned long)p & (unsigned long)01); }
-static inline Bdc_Fun_t * Bdc_Regular( Bdc_Fun_t * p ) { return (Bdc_Fun_t *)((unsigned long)p & ~(unsigned long)01); }
-static inline Bdc_Fun_t * Bdc_Not( Bdc_Fun_t * p ) { return (Bdc_Fun_t *)((unsigned long)p ^ (unsigned long)01); }
-static inline Bdc_Fun_t * Bdc_NotCond( Bdc_Fun_t * p, int c ) { return (Bdc_Fun_t *)((unsigned long)p ^ (unsigned long)(c!=0)); }
+static inline int Bdc_IsComplement( Bdc_Fun_t * p ) { return (int)((unsigned long)p & (unsigned long)01); }
+static inline Bdc_Fun_t * Bdc_Regular( Bdc_Fun_t * p ) { return (Bdc_Fun_t *)((unsigned long)p & ~(unsigned long)01); }
+static inline Bdc_Fun_t * Bdc_Not( Bdc_Fun_t * p ) { return (Bdc_Fun_t *)((unsigned long)p ^ (unsigned long)01); }
+static inline Bdc_Fun_t * Bdc_NotCond( Bdc_Fun_t * p, int c ) { return (Bdc_Fun_t *)((unsigned long)p ^ (unsigned long)(c!=0)); }
+
+static inline Bdc_Fun_t * Bdc_FunNew( Bdc_Man_t * p ) { Bdc_Fun_t * pRes; if ( p->nNodes == p->nNodesLimit ) return NULL; pRes = p->pNodes + p->nNodes++; memset( pRes, 0, sizeof(Bdc_Fun_t) ); p->nNodesNew++; return pRes; }
+static inline void Bdc_IsfStart( Bdc_Man_t * p, Bdc_Isf_t * pF ) { pF->puOn = Vec_IntFetch( p->vMemory, p->nWords ); pF->puOff = Vec_IntFetch( p->vMemory, p->nWords ); }
+static inline void Bdc_IsfClean( Bdc_Isf_t * p ) { p->uSupp = 0; p->Var = 0; }
+static inline void Bdc_IsfCopy( Bdc_Isf_t * p, Bdc_Isf_t * q ) { Bdc_Isf_t T = *p; *p = *q; *q = T; }
+static inline void Bdc_IsfNot( Bdc_Isf_t * p ) { unsigned * puT = p->puOn; p->puOn = p->puOff; p->puOff = puT; }
////////////////////////////////////////////////////////////////////////
/// MACRO DEFINITIONS ///
@@ -109,11 +130,14 @@ static inline Bdc_Fun_t * Bdc_NotCond( Bdc_Fun_t * p, int c ) { return (Bdc_
/// FUNCTION DECLARATIONS ///
////////////////////////////////////////////////////////////////////////
-/*=== bdcSupp.c ==========================================================*/
-extern int Bdc_SuppMinimize( Bdc_Man_t * p, Bdc_Isf_t * pIsf );
+/*=== bdcDec.c ==========================================================*/
+extern Bdc_Fun_t * Bdc_ManDecompose_rec( Bdc_Man_t * p, Bdc_Isf_t * pIsf );
/*=== bdcTable.c ==========================================================*/
extern Bdc_Fun_t * Bdc_TableLookup( Bdc_Man_t * p, Bdc_Isf_t * pIsf );
-
+extern void Bdc_TableAdd( Bdc_Man_t * p, Bdc_Fun_t * pFunc );
+extern void Bdc_TableClear( Bdc_Man_t * p );
+extern void Bdc_SuppMinimize( Bdc_Man_t * p, Bdc_Isf_t * pIsf );
+extern int Bdc_TableCheckContainment( Bdc_Man_t * p, Bdc_Isf_t * pIsf, unsigned * puTruth );
#ifdef __cplusplus
}
diff --git a/src/opt/bdc/bdcTable.c b/src/opt/bdc/bdcTable.c
new file mode 100644
index 00000000..d86a938d
--- /dev/null
+++ b/src/opt/bdc/bdcTable.c
@@ -0,0 +1,140 @@
+/**CFile****************************************************************
+
+ FileName [bdcTable.c]
+
+ SystemName [ABC: Logic synthesis and verification system.]
+
+ PackageName [Truth-table-based bi-decomposition engine.]
+
+ Synopsis [Hash table for intermediate nodes.]
+
+ Author [Alan Mishchenko]
+
+ Affiliation [UC Berkeley]
+
+ Date [Ver. 1.0. Started - January 30, 2007.]
+
+ Revision [$Id: bdcTable.c,v 1.00 2007/01/30 00:00:00 alanmi Exp $]
+
+***********************************************************************/
+
+#include "bdcInt.h"
+
+////////////////////////////////////////////////////////////////////////
+/// DECLARATIONS ///
+////////////////////////////////////////////////////////////////////////
+
+////////////////////////////////////////////////////////////////////////
+/// FUNCTION DEFINITIONS ///
+////////////////////////////////////////////////////////////////////////
+
+/**Function*************************************************************
+
+ Synopsis [Minimizes the support of the ISF.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+void Bdc_SuppMinimize( Bdc_Man_t * p, Bdc_Isf_t * pIsf )
+{
+ int v;
+ // go through the support variables
+ for ( v = 0; v < p->nVars; v++ )
+ {
+ if ( (pIsf->uSupp & (1 << v)) == 0 )
+ continue;
+ Kit_TruthExistNew( p->puTemp1, pIsf->puOn, p->nVars, v );
+ Kit_TruthExistNew( p->puTemp2, pIsf->puOff, p->nVars, v );
+ if ( !Kit_TruthIsDisjoint( p->puTemp1, p->puTemp2, p->nVars ) )
+ continue;
+ // remove the variable
+ Kit_TruthCopy( pIsf->puOn, p->puTemp1, p->nVars );
+ Kit_TruthCopy( pIsf->puOff, p->puTemp2, p->nVars );
+ pIsf->uSupp &= ~(1 << v);
+ }
+}
+
+/**Function*************************************************************
+
+ Synopsis [Checks containment of the function in the ISF.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+int Bdc_TableCheckContainment( Bdc_Man_t * p, Bdc_Isf_t * pIsf, unsigned * puTruth )
+{
+ return Kit_TruthIsImply( pIsf->puOn, puTruth, p->nVars ) &&
+ Kit_TruthIsDisjoint( pIsf->puOff, puTruth, p->nVars );
+}
+
+/**Function*************************************************************
+
+ Synopsis [Adds the new entry to the hash table.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+Bdc_Fun_t * Bdc_TableLookup( Bdc_Man_t * p, Bdc_Isf_t * pIsf )
+{
+ Bdc_Fun_t * pFunc;
+ for ( pFunc = p->pTable[pIsf->uSupp]; pFunc; pFunc = pFunc->pNext )
+ if ( Bdc_TableCheckContainment( p, pIsf, pFunc->puFunc ) )
+ return pFunc;
+ return NULL;
+}
+
+/**Function*************************************************************
+
+ Synopsis [Adds the new entry to the hash table.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+void Bdc_TableAdd( Bdc_Man_t * p, Bdc_Fun_t * pFunc )
+{
+ if ( p->pTable[pFunc->uSupp] == NULL )
+ Vec_IntPush( p->vSpots, pFunc->uSupp );
+ pFunc->pNext = p->pTable[pFunc->uSupp];
+ p->pTable[pFunc->uSupp] = pFunc;
+}
+
+/**Function*************************************************************
+
+ Synopsis [Adds the new entry to the hash table.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+void Bdc_TableClear( Bdc_Man_t * p )
+{
+ int Spot, i;
+ Vec_IntForEachEntry( p->vSpots, Spot, i )
+ p->pTable[Spot] = NULL;
+ Vec_IntClear( p->vSpots );
+}
+
+////////////////////////////////////////////////////////////////////////
+/// END OF FILE ///
+////////////////////////////////////////////////////////////////////////
+
+
diff --git a/src/opt/bdc/bdc_.c b/src/opt/bdc/bdc_.c
index 0fa51092..9d0a9462 100644
--- a/src/opt/bdc/bdc_.c
+++ b/src/opt/bdc/bdc_.c
@@ -18,7 +18,6 @@
***********************************************************************/
-#include "abc.h"
#include "bdcInt.h"
////////////////////////////////////////////////////////////////////////
diff --git a/src/opt/kit/kit.h b/src/opt/kit/kit.h
index 58c55cd2..ed2745e3 100644
--- a/src/opt/kit/kit.h
+++ b/src/opt/kit/kit.h
@@ -207,6 +207,22 @@ static inline int Kit_TruthIsImply( unsigned * pIn1, unsigned * pIn2, int nVars
return 0;
return 1;
}
+static inline int Kit_TruthIsDisjoint( unsigned * pIn1, unsigned * pIn2, int nVars )
+{
+ int w;
+ for ( w = Kit_TruthWordNum(nVars)-1; w >= 0; w-- )
+ if ( pIn1[w] & pIn2[w] )
+ return 0;
+ return 1;
+}
+static inline int Kit_TruthIsDisjoint3( unsigned * pIn1, unsigned * pIn2, unsigned * pIn3, int nVars )
+{
+ int w;
+ for ( w = Kit_TruthWordNum(nVars)-1; w >= 0; w-- )
+ if ( pIn1[w] & pIn2[w] & pIn3[w] )
+ return 0;
+ return 1;
+}
static inline void Kit_TruthCopy( unsigned * pOut, unsigned * pIn, int nVars )
{
int w;
@@ -320,7 +336,11 @@ extern int Kit_TruthSupport( unsigned * pTruth, int nVars );
extern void Kit_TruthCofactor0( unsigned * pTruth, int nVars, int iVar );
extern void Kit_TruthCofactor1( unsigned * pTruth, int nVars, int iVar );
extern void Kit_TruthExist( unsigned * pTruth, int nVars, int iVar );
+extern void Kit_TruthExistNew( unsigned * pRes, unsigned * pTruth, int nVars, int iVar );
+extern void Kit_TruthExistSet( unsigned * pRes, unsigned * pTruth, int nVars, unsigned uMask );
extern void Kit_TruthForall( unsigned * pTruth, int nVars, int iVar );
+extern void Kit_TruthForallNew( unsigned * pRes, unsigned * pTruth, int nVars, int iVar );
+extern void Kit_TruthForallSet( unsigned * pRes, unsigned * pTruth, int nVars, unsigned uMask );
extern void Kit_TruthMux( unsigned * pOut, unsigned * pCof0, unsigned * pCof1, int nVars, int iVar );
extern void Kit_TruthChangePhase( unsigned * pTruth, int nVars, int iVar );
extern int Kit_TruthMinCofSuppOverlap( unsigned * pTruth, int nVars, int * pVarMin );
diff --git a/src/opt/kit/kitTruth.c b/src/opt/kit/kitTruth.c
index 5df10d63..429875bc 100644
--- a/src/opt/kit/kitTruth.c
+++ b/src/opt/kit/kitTruth.c
@@ -490,6 +490,81 @@ void Kit_TruthExist( unsigned * pTruth, int nVars, int iVar )
SeeAlso []
***********************************************************************/
+void Kit_TruthExistNew( unsigned * pRes, unsigned * pTruth, int nVars, int iVar )
+{
+ int nWords = Kit_TruthWordNum( nVars );
+ int i, k, Step;
+
+ assert( iVar < nVars );
+ switch ( iVar )
+ {
+ case 0:
+ for ( i = 0; i < nWords; i++ )
+ pRes[i] = pTruth[i] | ((pTruth[i] & 0xAAAAAAAA) >> 1) | ((pTruth[i] & 0x55555555) << 1);
+ return;
+ case 1:
+ for ( i = 0; i < nWords; i++ )
+ pRes[i] = pTruth[i] | ((pTruth[i] & 0xCCCCCCCC) >> 2) | ((pTruth[i] & 0x33333333) << 2);
+ return;
+ case 2:
+ for ( i = 0; i < nWords; i++ )
+ pRes[i] = pTruth[i] | ((pTruth[i] & 0xF0F0F0F0) >> 4) | ((pTruth[i] & 0x0F0F0F0F) << 4);
+ return;
+ case 3:
+ for ( i = 0; i < nWords; i++ )
+ pRes[i] = pTruth[i] | ((pTruth[i] & 0xFF00FF00) >> 8) | ((pTruth[i] & 0x00FF00FF) << 8);
+ return;
+ case 4:
+ for ( i = 0; i < nWords; i++ )
+ pRes[i] = pTruth[i] | ((pTruth[i] & 0xFFFF0000) >> 16) | ((pTruth[i] & 0x0000FFFF) << 16);
+ return;
+ default:
+ Step = (1 << (iVar - 5));
+ for ( k = 0; k < nWords; k += 2*Step )
+ {
+ for ( i = 0; i < Step; i++ )
+ {
+ pRes[i] = pTruth[i] | pTruth[Step+i];
+ pRes[Step+i] = pRes[i];
+ }
+ pRes += 2*Step;
+ pTruth += 2*Step;
+ }
+ return;
+ }
+}
+
+/**Function*************************************************************
+
+ Synopsis [Existantially quantifies the set of variables.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+void Kit_TruthExistSet( unsigned * pRes, unsigned * pTruth, int nVars, unsigned uMask )
+{
+ int v;
+ Kit_TruthCopy( pRes, pTruth, nVars );
+ for ( v = 0; v < nVars; v++ )
+ if ( uMask & (1 << v) )
+ Kit_TruthExist( pRes, nVars, v );
+}
+
+/**Function*************************************************************
+
+ Synopsis [Unversally quantifies the variable.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
void Kit_TruthForall( unsigned * pTruth, int nVars, int iVar )
{
int nWords = Kit_TruthWordNum( nVars );
@@ -533,6 +608,81 @@ void Kit_TruthForall( unsigned * pTruth, int nVars, int iVar )
}
}
+/**Function*************************************************************
+
+ Synopsis [Universally quantifies the variable.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+void Kit_TruthForallNew( unsigned * pRes, unsigned * pTruth, int nVars, int iVar )
+{
+ int nWords = Kit_TruthWordNum( nVars );
+ int i, k, Step;
+
+ assert( iVar < nVars );
+ switch ( iVar )
+ {
+ case 0:
+ for ( i = 0; i < nWords; i++ )
+ pRes[i] = pTruth[i] & (((pTruth[i] & 0xAAAAAAAA) >> 1) | ((pTruth[i] & 0x55555555) << 1));
+ return;
+ case 1:
+ for ( i = 0; i < nWords; i++ )
+ pRes[i] = pTruth[i] & (((pTruth[i] & 0xCCCCCCCC) >> 2) | ((pTruth[i] & 0x33333333) << 2));
+ return;
+ case 2:
+ for ( i = 0; i < nWords; i++ )
+ pRes[i] = pTruth[i] & (((pTruth[i] & 0xF0F0F0F0) >> 4) | ((pTruth[i] & 0x0F0F0F0F) << 4));
+ return;
+ case 3:
+ for ( i = 0; i < nWords; i++ )
+ pRes[i] = pTruth[i] & (((pTruth[i] & 0xFF00FF00) >> 8) | ((pTruth[i] & 0x00FF00FF) << 8));
+ return;
+ case 4:
+ for ( i = 0; i < nWords; i++ )
+ pRes[i] = pTruth[i] & (((pTruth[i] & 0xFFFF0000) >> 16) | ((pTruth[i] & 0x0000FFFF) << 16));
+ return;
+ default:
+ Step = (1 << (iVar - 5));
+ for ( k = 0; k < nWords; k += 2*Step )
+ {
+ for ( i = 0; i < Step; i++ )
+ {
+ pRes[i] = pTruth[i] & pTruth[Step+i];
+ pRes[Step+i] = pRes[i];
+ }
+ pRes += 2*Step;
+ pTruth += 2*Step;
+ }
+ return;
+ }
+}
+
+/**Function*************************************************************
+
+ Synopsis [Universally quantifies the set of variables.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+void Kit_TruthForallSet( unsigned * pRes, unsigned * pTruth, int nVars, unsigned uMask )
+{
+ int v;
+ Kit_TruthCopy( pRes, pTruth, nVars );
+ for ( v = 0; v < nVars; v++ )
+ if ( uMask & (1 << v) )
+ Kit_TruthForall( pRes, nVars, v );
+}
+
/**Function*************************************************************
diff --git a/src/opt/res/res.h b/src/opt/res/res.h
index fda35b89..3c963e99 100644
--- a/src/opt/res/res.h
+++ b/src/opt/res/res.h
@@ -44,6 +44,8 @@ struct Res_Par_t_
int nWindow; // window size
int nSimWords; // the number of simulation words
int nCands; // the number of candidates to try
+ int fArea; // performs optimization for area
+ int fDelay; // performs optimization for delay
int fVerbose; // enable basic stats
int fVeryVerbose; // enable detailed stats
};
diff --git a/src/opt/res/resCore.c b/src/opt/res/resCore.c
index 609addf9..95728e9a 100644
--- a/src/opt/res/resCore.c
+++ b/src/opt/res/resCore.c
@@ -48,17 +48,24 @@ struct Res_Man_t_
int nDivNodes; // the total number of divisors
int nWinsTriv; // the total number of trivial windows
int nWinsUsed; // the total number of useful windows (with at least one candidate)
+ int nConstsUsed; // the total number of constant nodes under ODC
int nCandSets; // the total number of candidates
int nProvedSets; // the total number of proved groups
int nSimEmpty; // the empty simulation info
int nTotalNets; // the total number of nets
+ int nTotalNodes; // the total number of nodess
+ int nTotalNets2; // the total number of nets
+ int nTotalNodes2; // the total number of nodess
// runtime
int timeWin; // windowing
int timeDiv; // divisors
int timeAig; // strashing
int timeSim; // simulation
int timeCand; // resubstitution candidates
- int timeSat; // SAT solving
+ int timeSatTotal; // SAT solving total
+ int timeSatSat; // SAT solving (sat calls)
+ int timeSatUnsat; // SAT solving (unsat calls)
+ int timeSatSim; // SAT solving (simulation)
int timeInt; // interpolation
int timeUpd; // updating
int timeTotal; // total runtime
@@ -120,19 +127,30 @@ void Res_ManFree( Res_Man_t * p )
printf( "\n" );
printf( "WinsTriv = %d. ", p->nWinsTriv );
printf( "SimsEmpt = %d. ", p->nSimEmpty );
+ printf( "Const = %d. ", p->nConstsUsed );
printf( "WindUsed = %d. ", p->nWinsUsed );
printf( "Cands = %d. ", p->nCandSets );
- printf( "Proved = %d. (%.2f %%)", p->nProvedSets, 100.0*p->nProvedSets/p->nTotalNets );
+ printf( "Proved = %d.", p->nProvedSets );
+ printf( "\n" );
+ printf( "Reduction in nodes = %d. (%.2f %%) ",
+ p->nTotalNodes-p->nTotalNodes2,
+ 100.0*(p->nTotalNodes-p->nTotalNodes2)/p->nTotalNodes );
+ printf( "Reduction in nets = %d. (%.2f %%) ",
+ p->nTotalNets-p->nTotalNets2,
+ 100.0*(p->nTotalNets-p->nTotalNets2)/p->nTotalNets );
printf( "\n" );
- PRT( "Windowing ", p->timeWin );
- PRT( "Divisors ", p->timeDiv );
- PRT( "Strashing ", p->timeAig );
- PRT( "Simulation ", p->timeSim );
- PRT( "Candidates ", p->timeCand );
- PRT( "SAT solver ", p->timeSat );
- PRT( "Interpol ", p->timeInt );
- PRT( "Undating ", p->timeUpd );
+ PRTP( "Windowing ", p->timeWin, p->timeTotal );
+ PRTP( "Divisors ", p->timeDiv, p->timeTotal );
+ PRTP( "Strashing ", p->timeAig, p->timeTotal );
+ PRTP( "Simulation ", p->timeSim, p->timeTotal );
+ PRTP( "Candidates ", p->timeCand, p->timeTotal );
+ PRTP( "SAT solver ", p->timeSatTotal, p->timeTotal );
+ PRTP( " sat ", p->timeSatSat, p->timeTotal );
+ PRTP( " unsat ", p->timeSatUnsat, p->timeTotal );
+ PRTP( " simul ", p->timeSatSim, p->timeTotal );
+ PRTP( "Interpol ", p->timeInt, p->timeTotal );
+ PRTP( "Undating ", p->timeUpd, p->timeTotal );
PRT( "TOTAL ", p->timeTotal );
}
Res_WinFree( p->pWin );
@@ -160,6 +178,7 @@ void Res_ManFree( Res_Man_t * p )
***********************************************************************/
int Abc_NtkResynthesize( Abc_Ntk_t * pNtk, Res_Par_t * pPars )
{
+ ProgressBar * pProgress;
Res_Man_t * p;
Abc_Obj_t * pObj;
Hop_Obj_t * pFunc;
@@ -168,18 +187,33 @@ int Abc_NtkResynthesize( Abc_Ntk_t * pNtk, Res_Par_t * pPars )
unsigned * puTruth;
int i, k, RetValue, nNodesOld, nFanins;
int clk, clkTotal = clock();
- assert( Abc_NtkHasAig(pNtk) );
// start the manager
p = Res_ManAlloc( pPars );
p->nTotalNets = Abc_NtkGetTotalFanins(pNtk);
+ p->nTotalNodes = Abc_NtkNodeNum(pNtk);
+
+ // perform the network sweep
+ Abc_NtkSweep( pNtk, 0 );
+
+ // convert into the AIG
+ if ( !Abc_NtkLogicToAig(pNtk) )
+ {
+ fprintf( stdout, "Converting to BDD has failed.\n" );
+ Res_ManFree( p );
+ return 0;
+ }
+ assert( Abc_NtkHasAig(pNtk) );
+
// set the number of levels
Abc_NtkLevel( pNtk );
// try resynthesizing nodes in the topological order
nNodesOld = Abc_NtkObjNumMax(pNtk);
+ pProgress = Extra_ProgressBarStart( stdout, nNodesOld );
Abc_NtkForEachObj( pNtk, pObj, i )
{
+ Extra_ProgressBarUpdate( pProgress, i, NULL );
if ( !Abc_ObjIsNode(pObj) )
continue;
if ( pObj->Id > nNodesOld )
@@ -205,7 +239,7 @@ p->timeWin += clock() - clk;
// collect the divisors
clk = clock();
- Res_WinDivisors( p->pWin, pObj->Level - 1 );
+ Res_WinDivisors( p->pWin, pObj->Level + 2 ); //- 1 );
p->timeDiv += clock() - clk;
p->nWins++;
@@ -232,7 +266,7 @@ p->timeAig += clock() - clk;
// prepare simulation info
clk = clock();
- RetValue = Res_SimPrepare( p->pSim, p->pAig );
+ RetValue = Res_SimPrepare( p->pSim, p->pAig, Vec_PtrSize(p->pWin->vLeaves), 0 ); //p->pPars->fVerbose );
p->timeSim += clock() - clk;
if ( !RetValue )
{
@@ -240,14 +274,33 @@ p->timeSim += clock() - clk;
continue;
}
+ // consider the case of constant node
+ if ( p->pSim->fConst0 || p->pSim->fConst1 )
+ {
+ p->nConstsUsed++;
+
+ pFunc = p->pSim->fConst1? Hop_ManConst1(pNtk->pManFunc) : Hop_ManConst0(pNtk->pManFunc);
+ vFanins = Vec_VecEntry( p->vResubsW, 0 );
+ Vec_PtrClear( vFanins );
+ Res_UpdateNetwork( pObj, vFanins, pFunc, p->vLevels );
+ continue;
+ }
+
+// printf( " " );
+
// find resub candidates for the node
clk = clock();
- RetValue = Res_FilterCandidates( p->pWin, p->pAig, p->pSim, p->vResubs, p->vResubsW );
+ if ( p->pPars->fArea )
+ RetValue = Res_FilterCandidatesArea( p->pWin, p->pAig, p->pSim, p->vResubs, p->vResubsW );
+ else
+ RetValue = Res_FilterCandidatesNets( p->pWin, p->pAig, p->pSim, p->vResubs, p->vResubsW );
p->timeCand += clock() - clk;
p->nCandSets += RetValue;
if ( RetValue == 0 )
continue;
+// printf( "%d(%d) ", Vec_PtrSize(p->pWin->vDivs), RetValue );
+
p->nWinsUsed++;
// iterate through candidate resubstitutions
@@ -260,15 +313,20 @@ p->timeCand += clock() - clk;
clk = clock();
if ( p->pCnf ) Sto_ManFree( p->pCnf );
p->pCnf = Res_SatProveUnsat( p->pAig, vFanins );
-p->timeSat += clock() - clk;
if ( p->pCnf == NULL )
{
+p->timeSatSat += clock() - clk;
// printf( " Sat\n" );
+// printf( "-" );
continue;
}
+p->timeSatUnsat += clock() - clk;
+// printf( "+" );
+
p->nProvedSets++;
// printf( " Unsat\n" );
// continue;
+// printf( "Proved %d.\n", k );
// write it into a file
// Sto_ManDumpClauses( p->pCnf, "trace.cnf" );
@@ -277,10 +335,11 @@ p->timeSat += clock() - clk;
clk = clock();
nFanins = Int_ManInterpolate( p->pMan, p->pCnf, 0, &puTruth );
p->timeInt += clock() - clk;
- assert( nFanins == Vec_PtrSize(vFanins) - 2 );
+ if ( nFanins != Vec_PtrSize(vFanins) - 2 )
+ continue;
assert( puTruth );
// Extra_PrintBinary( stdout, puTruth, 1 << nFanins ); printf( "\n" );
-
+
// transform interpolant into the AIG
pGraph = Kit_TruthToGraph( puTruth, nFanins, p->vMem );
@@ -294,8 +353,15 @@ clk = clock();
p->timeUpd += clock() - clk;
break;
}
-
+// printf( "\n" );
}
+ Extra_ProgressBarStop( pProgress );
+
+p->timeSatSim += p->pSim->timeSat;
+p->timeSatTotal = p->timeSatSat + p->timeSatUnsat + p->timeSatSim;
+
+ p->nTotalNets2 = Abc_NtkGetTotalFanins(pNtk);
+ p->nTotalNodes2 = Abc_NtkNodeNum(pNtk);
// quit resubstitution manager
p->timeTotal = clock() - clkTotal;
diff --git a/src/opt/res/resDivs.c b/src/opt/res/resDivs.c
index af30592c..38294428 100644
--- a/src/opt/res/resDivs.c
+++ b/src/opt/res/resDivs.c
@@ -26,7 +26,6 @@
////////////////////////////////////////////////////////////////////////
static void Res_WinMarkTfi( Res_Win_t * p );
-static int Res_WinVisitMffc( Res_Win_t * p );
////////////////////////////////////////////////////////////////////////
/// FUNCTION DEFINITIONS ///
@@ -61,7 +60,7 @@ void Res_WinDivisors( Res_Win_t * p, int nLevDivMax )
// (3) the node's fanins (these are treated as a special case)
Abc_NtkIncrementTravId( p->pNode->pNtk );
Res_WinSweepLeafTfo_rec( p->pNode, p->nLevDivMax );
- Res_WinVisitMffc( p );
+ Res_WinVisitMffc( p->pNode );
Abc_ObjForEachFanin( p->pNode, pObj, k )
Abc_NodeSetTravIdCurrent( pObj );
@@ -260,13 +259,14 @@ int Res_NodeRef_rec( Abc_Obj_t * pNode )
SeeAlso []
***********************************************************************/
-int Res_WinVisitMffc( Res_Win_t * p )
+int Res_WinVisitMffc( Abc_Obj_t * pNode )
{
int Count1, Count2;
+ assert( Abc_ObjIsNode(pNode) );
// dereference the node (mark with the current trav ID)
- Count1 = Res_NodeDeref_rec( p->pNode );
+ Count1 = Res_NodeDeref_rec( pNode );
// reference it back
- Count2 = Res_NodeRef_rec( p->pNode );
+ Count2 = Res_NodeRef_rec( pNode );
assert( Count1 == Count2 );
return Count1;
}
diff --git a/src/opt/res/resFilter.c b/src/opt/res/resFilter.c
index 38f64815..afbbbe42 100644
--- a/src/opt/res/resFilter.c
+++ b/src/opt/res/resFilter.c
@@ -26,6 +26,7 @@
////////////////////////////////////////////////////////////////////////
static unsigned * Res_FilterCollectFaninInfo( Res_Win_t * pWin, Res_Sim_t * pSim, unsigned uMask );
+static int Res_FilterCriticalFanin( Abc_Obj_t * pNode );
////////////////////////////////////////////////////////////////////////
/// FUNCTION DEFINITIONS ///
@@ -42,7 +43,7 @@ static unsigned * Res_FilterCollectFaninInfo( Res_Win_t * pWin, Res_Sim_t * pSim
SeeAlso []
***********************************************************************/
-int Res_FilterCandidates( Res_Win_t * pWin, Abc_Ntk_t * pAig, Res_Sim_t * pSim, Vec_Vec_t * vResubs, Vec_Vec_t * vResubsW )
+int Res_FilterCandidatesNets( Res_Win_t * pWin, Abc_Ntk_t * pAig, Res_Sim_t * pSim, Vec_Vec_t * vResubs, Vec_Vec_t * vResubsW )
{
Abc_Obj_t * pFanin, * pFanin2;
unsigned * pInfo;
@@ -52,13 +53,19 @@ int Res_FilterCandidates( Res_Win_t * pWin, Abc_Ntk_t * pAig, Res_Sim_t * pSim,
pInfo = Vec_PtrEntry( pSim->vOuts, 1 );
RetValue = Abc_InfoIsOne( pInfo, pSim->nWordsOut );
if ( RetValue == 0 )
- printf( "Failed 1!\n" );
+ {
+// printf( "Failed 1!\n" );
+ return 0;
+ }
// collect the fanin info
pInfo = Res_FilterCollectFaninInfo( pWin, pSim, ~0 );
RetValue = Abc_InfoIsOne( pInfo, pSim->nWordsOut );
if ( RetValue == 0 )
- printf( "Failed 2!\n" );
+ {
+// printf( "Failed 2!\n" );
+ return 0;
+ }
// try removing fanins
// printf( "Fanins: " );
@@ -71,7 +78,7 @@ int Res_FilterCandidates( Res_Win_t * pWin, Abc_Ntk_t * pAig, Res_Sim_t * pSim,
RetValue = Abc_InfoIsOne( pInfo, pSim->nWordsOut );
if ( RetValue )
{
-// printf( "Node %4d. Removing fanin %4d.\n", pWin->pNode->Id, Abc_ObjFaninId(pWin->pNode, i) );
+// printf( "Node %4d. Candidate fanin %4d.\n", pWin->pNode->Id, pFanin->Id );
// collect the nodes
Vec_VecPush( vResubs, Counter, Abc_NtkPo(pAig,0) );
@@ -94,6 +101,104 @@ int Res_FilterCandidates( Res_Win_t * pWin, Abc_Ntk_t * pAig, Res_Sim_t * pSim,
return Counter;
}
+
+/**Function*************************************************************
+
+ Synopsis [Finds sets of feasible candidates.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+int Res_FilterCandidatesArea( Res_Win_t * pWin, Abc_Ntk_t * pAig, Res_Sim_t * pSim, Vec_Vec_t * vResubs, Vec_Vec_t * vResubsW )
+{
+ Abc_Obj_t * pFanin;
+ unsigned * pInfo, * pInfo2;
+ int Counter, RetValue, i, k, iBest;
+
+ // check that the info the node is one
+ pInfo = Vec_PtrEntry( pSim->vOuts, 1 );
+ RetValue = Abc_InfoIsOne( pInfo, pSim->nWordsOut );
+ if ( RetValue == 0 )
+ {
+// printf( "Failed 1!\n" );
+ return 0;
+ }
+
+ // collect the fanin info
+ pInfo = Res_FilterCollectFaninInfo( pWin, pSim, ~0 );
+ RetValue = Abc_InfoIsOne( pInfo, pSim->nWordsOut );
+ if ( RetValue == 0 )
+ {
+// printf( "Failed 2!\n" );
+ return 0;
+ }
+
+ // try removing fanins
+// printf( "Fanins: " );
+ Counter = 0;
+ Vec_VecClear( vResubs );
+ Vec_VecClear( vResubsW );
+ // get the best fanins
+ iBest = Res_FilterCriticalFanin( pWin->pNode );
+ if ( iBest == -1 )
+ return 0;
+
+ // get the info without the critical fanin
+ pInfo = Res_FilterCollectFaninInfo( pWin, pSim, ~(1 << iBest) );
+ RetValue = Abc_InfoIsOne( pInfo, pSim->nWordsOut );
+ if ( RetValue )
+ {
+// printf( "Can be done without one!\n" );
+ // collect the nodes
+ Vec_VecPush( vResubs, Counter, Abc_NtkPo(pAig,0) );
+ Vec_VecPush( vResubs, Counter, Abc_NtkPo(pAig,1) );
+ Abc_ObjForEachFanin( pWin->pNode, pFanin, k )
+ {
+ if ( k != iBest )
+ {
+ Vec_VecPush( vResubs, Counter, Abc_NtkPo(pAig,2+k) );
+ Vec_VecPush( vResubsW, Counter, pFanin );
+ }
+ }
+ Counter++;
+// printf( "*" );
+ return Counter;
+ }
+
+ // go through the divisors
+ for ( i = Abc_ObjFaninNum(pWin->pNode) + 2; i < Abc_NtkPoNum(pAig); i++ )
+ {
+ pInfo2 = Vec_PtrEntry( pSim->vOuts, i );
+ if ( !Abc_InfoIsOrOne( pInfo, pInfo2, pSim->nWordsOut ) )
+ continue;
+ // collect the nodes
+ Vec_VecPush( vResubs, Counter, Abc_NtkPo(pAig,0) );
+ Vec_VecPush( vResubs, Counter, Abc_NtkPo(pAig,1) );
+ // collect the remaning fanins and the divisor
+ Abc_ObjForEachFanin( pWin->pNode, pFanin, k )
+ {
+ if ( k != iBest )
+ {
+ Vec_VecPush( vResubs, Counter, Abc_NtkPo(pAig,2+k) );
+ Vec_VecPush( vResubsW, Counter, pFanin );
+ }
+ }
+ // collect the divisor
+ Vec_VecPush( vResubs, Counter, Abc_NtkPo(pAig,i) );
+ Vec_VecPush( vResubsW, Counter, Vec_PtrEntry(pWin->vDivs, i-2-Abc_ObjFaninNum(pWin->pNode)) );
+ Counter++;
+
+ if ( Counter == Vec_VecSize(vResubs) )
+ break;
+ }
+ return Counter;
+}
+
+
/**Function*************************************************************
Synopsis [Finds sets of feasible candidates.]
@@ -121,6 +226,40 @@ unsigned * Res_FilterCollectFaninInfo( Res_Win_t * pWin, Res_Sim_t * pSim, unsig
}
+/**Function*************************************************************
+
+ Synopsis [Returns the index of the most critical fanin.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+int Res_FilterCriticalFanin( Abc_Obj_t * pNode )
+{
+ Abc_Obj_t * pFanin;
+ int i, iBest = -1, CostMax = 0, CostCur;
+ Abc_ObjForEachFanin( pNode, pFanin, i )
+ {
+ if ( !Abc_ObjIsNode(pFanin) )
+ continue;
+ if ( Abc_ObjFanoutNum(pFanin) > 1 )
+ continue;
+ CostCur = Res_WinVisitMffc( pFanin );
+ if ( CostMax < CostCur )
+ {
+ CostMax = CostCur;
+ iBest = i;
+ }
+ }
+// if ( CostMax > 0 )
+// printf( "<%d>", CostMax );
+ return iBest;
+}
+
+
////////////////////////////////////////////////////////////////////////
/// END OF FILE ///
////////////////////////////////////////////////////////////////////////
diff --git a/src/opt/res/resInt.h b/src/opt/res/resInt.h
index 9d17cb1c..10e312b3 100644
--- a/src/opt/res/resInt.h
+++ b/src/opt/res/resInt.h
@@ -68,9 +68,15 @@ typedef struct Res_Sim_t_ Res_Sim_t;
struct Res_Sim_t_
{
Abc_Ntk_t * pAig; // AIG for simulation
+ int nTruePis; // the number of true PIs of the window
+ int fConst0; // the node can be replaced by constant 0
+ int fConst1; // the node can be replaced by constant 0
// simulation parameters
int nWords; // the number of simulation words
int nPats; // the number of patterns
+ int nWordsIn; // the number of simulation words in the input patterns
+ int nPatsIn; // the number of patterns in the input patterns
+ int nBytesIn; // the number of bytes in the input patterns
int nWordsOut; // the number of simulation words in the output patterns
int nPatsOut; // the number of patterns in the output patterns
// simulation info
@@ -82,6 +88,8 @@ struct Res_Sim_t_
int nPats1; // the number of 1-patterns accumulated
// resub candidates
Vec_Vec_t * vCands; // resubstitution candidates
+ // statistics
+ int timeSat;
};
////////////////////////////////////////////////////////////////////////
@@ -95,15 +103,17 @@ struct Res_Sim_t_
/*=== resDivs.c ==========================================================*/
extern void Res_WinDivisors( Res_Win_t * p, int nLevDivMax );
extern void Res_WinSweepLeafTfo_rec( Abc_Obj_t * pObj, int nLevelLimit );
+extern int Res_WinVisitMffc( Abc_Obj_t * pNode );
/*=== resFilter.c ==========================================================*/
-extern int Res_FilterCandidates( Res_Win_t * pWin, Abc_Ntk_t * pAig, Res_Sim_t * pSim, Vec_Vec_t * vResubs, Vec_Vec_t * vResubsW );
+extern int Res_FilterCandidatesNets( Res_Win_t * pWin, Abc_Ntk_t * pAig, Res_Sim_t * pSim, Vec_Vec_t * vResubs, Vec_Vec_t * vResubsW );
+extern int Res_FilterCandidatesArea( Res_Win_t * pWin, Abc_Ntk_t * pAig, Res_Sim_t * pSim, Vec_Vec_t * vResubs, Vec_Vec_t * vResubsW );
/*=== resSat.c ==========================================================*/
extern void * Res_SatProveUnsat( Abc_Ntk_t * pAig, Vec_Ptr_t * vFanins );
-extern void * Res_SatSimulateConstr( Abc_Ntk_t * pAig, Vec_Ptr_t * vFanins );
+extern int Res_SatSimulate( Res_Sim_t * p, int nPats, int fOnSet );
/*=== resSim.c ==========================================================*/
extern Res_Sim_t * Res_SimAlloc( int nWords );
extern void Res_SimFree( Res_Sim_t * p );
-extern int Res_SimPrepare( Res_Sim_t * p, Abc_Ntk_t * pAig );
+extern int Res_SimPrepare( Res_Sim_t * p, Abc_Ntk_t * pAig, int nTruePis, int fVerbose );
/*=== resStrash.c ==========================================================*/
extern Abc_Ntk_t * Res_WndStrash( Res_Win_t * p );
/*=== resWnd.c ==========================================================*/
diff --git a/src/opt/res/resSat.c b/src/opt/res/resSat.c
index f9558c97..dd0e7a23 100644
--- a/src/opt/res/resSat.c
+++ b/src/opt/res/resSat.c
@@ -128,25 +128,27 @@ void * Res_SatProveUnsat( Abc_Ntk_t * pAig, Vec_Ptr_t * vFanins )
Synopsis [Loads AIG into the SAT solver for constrained simulation.]
- Description [The array of fanins contains exactly two entries: the
- care set and the functions.]
+ Description []
SideEffects []
SeeAlso []
***********************************************************************/
-void * Res_SatSimulateConstr( Abc_Ntk_t * pAig, Vec_Ptr_t * vFanins )
+void * Res_SatSimulateConstr( Abc_Ntk_t * pAig, int fOnSet )
{
sat_solver * pSat;
+ Vec_Ptr_t * vFanins;
Vec_Ptr_t * vNodes;
Abc_Obj_t * pObj;
int i, nNodes;
- // make sure fanins contain POs of the AIG
- pObj = Vec_PtrEntry( vFanins, 0 );
- assert( pObj->pNtk == pAig && Abc_ObjIsPo(pObj) );
- assert( Vec_PtrSize(vFanins) == 2 );
+ // start the array
+ vFanins = Vec_PtrAlloc( 2 );
+ pObj = Abc_NtkPo( pAig, 0 );
+ Vec_PtrPush( vFanins, pObj );
+ pObj = Abc_NtkPo( pAig, 1 );
+ Vec_PtrPush( vFanins, pObj );
// collect reachable nodes
vNodes = Abc_NtkDfsNodes( pAig, (Abc_Obj_t **)vFanins->pArray, vFanins->nSize );
@@ -171,21 +173,154 @@ void * Res_SatSimulateConstr( Abc_Ntk_t * pAig, Vec_Ptr_t * vFanins )
Res_SatAddAnd( pSat, (int)pObj->pCopy,
(int)Abc_ObjFanin0(pObj)->pCopy, (int)Abc_ObjFanin1(pObj)->pCopy, Abc_ObjFaninC0(pObj), Abc_ObjFaninC1(pObj) );
Vec_PtrFree( vNodes );
- // add clauses for POs
- Vec_PtrForEachEntry( vFanins, pObj, i )
- Res_SatAddEqual( pSat, (int)pObj->pCopy,
- (int)Abc_ObjFanin0(pObj)->pCopy, Abc_ObjFaninC0(pObj) );
+ // add clauses for the first PO
+ pObj = Abc_NtkPo( pAig, 0 );
+ Res_SatAddEqual( pSat, (int)pObj->pCopy,
+ (int)Abc_ObjFanin0(pObj)->pCopy, Abc_ObjFaninC0(pObj) );
+ // add clauses for the second PO
+ pObj = Abc_NtkPo( pAig, 1 );
+ Res_SatAddEqual( pSat, (int)pObj->pCopy,
+ (int)Abc_ObjFanin0(pObj)->pCopy, Abc_ObjFaninC0(pObj) );
// add trivial clauses
- pObj = Vec_PtrEntry(vFanins, 0);
+ pObj = Abc_NtkPo( pAig, 0 );
Res_SatAddConst1( pSat, (int)pObj->pCopy, 0 ); // care-set
- pObj = Vec_PtrEntry(vFanins, 1);
- Res_SatAddConst1( pSat, (int)pObj->pCopy, 0 ); // on-set
+
+ pObj = Abc_NtkPo( pAig, 1 );
+ Res_SatAddConst1( pSat, (int)pObj->pCopy, !fOnSet ); // on-set
+
+ Vec_PtrFree( vFanins );
return pSat;
}
/**Function*************************************************************
+ Synopsis [Loads AIG into the SAT solver for constrained simulation.]
+
+ Description [Returns 1 if the required number of patterns are found.
+ Returns 0 if the solver ran out of time or proved a constant.
+ In the latter, case one of the flags, fConst0 or fConst1, are set to 1.]
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+int Res_SatSimulate( Res_Sim_t * p, int nPatsLimit, int fOnSet )
+{
+ Vec_Int_t * vLits;
+ Vec_Ptr_t * vPats;
+ sat_solver * pSat;
+ int RetValue, i, k, value, status, Lit, Var, iPat;
+ int clk = clock();
+
+//printf( "Looking for %s: ", fOnSet? "onset " : "offset" );
+
+ // decide what problem should be solved
+ Lit = toLitCond( (int)Abc_NtkPo(p->pAig,1)->pCopy, !fOnSet );
+ if ( fOnSet )
+ {
+ iPat = p->nPats1;
+ vPats = p->vPats1;
+ }
+ else
+ {
+ iPat = p->nPats0;
+ vPats = p->vPats0;
+ }
+ assert( iPat < nPatsLimit );
+
+ // derive the SAT solver
+ pSat = Res_SatSimulateConstr( p->pAig, fOnSet );
+ pSat->fSkipSimplify = 1;
+ status = sat_solver_simplify( pSat );
+ if ( status == 0 )
+ {
+ if ( iPat == 0 )
+ {
+// if ( fOnSet )
+// p->fConst0 = 1;
+// else
+// p->fConst1 = 1;
+ RetValue = 0;
+ }
+ goto finish;
+ }
+
+ // enumerate through the SAT assignments
+ RetValue = 1;
+ vLits = Vec_IntAlloc( 32 );
+ for ( k = iPat; k < nPatsLimit; k++ )
+ {
+ // solve with the assumption
+// status = sat_solver_solve( pSat, &Lit, &Lit + 1, (sint64)10000, (sint64)0, (sint64)0, (sint64)0 );
+ status = sat_solver_solve( pSat, NULL, NULL, (sint64)10000, (sint64)0, (sint64)0, (sint64)0 );
+ if ( status == l_False )
+ {
+//printf( "Const %d\n", !fOnSet );
+ if ( k == 0 )
+ {
+ if ( fOnSet )
+ p->fConst0 = 1;
+ else
+ p->fConst1 = 1;
+ RetValue = 0;
+ }
+ break;
+ }
+ else if ( status == l_True )
+ {
+ // save the pattern
+ Vec_IntClear( vLits );
+ for ( i = 0; i < p->nTruePis; i++ )
+ {
+ Var = (int)Abc_NtkPi(p->pAig,i)->pCopy;
+ value = (int)(pSat->model.ptr[Var] == l_True);
+ if ( value )
+ Abc_InfoSetBit( Vec_PtrEntry(vPats, i), k );
+ Lit = toLitCond( Var, value );
+ Vec_IntPush( vLits, Lit );
+// printf( "%d", value );
+ }
+// printf( "\n" );
+
+ status = sat_solver_addclause( pSat, Vec_IntArray(vLits), Vec_IntArray(vLits) + Vec_IntSize(vLits) );
+ if ( status == 0 )
+ {
+ k++;
+ RetValue = 1;
+ break;
+ }
+ }
+ else
+ {
+//printf( "Undecided\n" );
+ if ( k == 0 )
+ RetValue = 0;
+ else
+ RetValue = 1;
+ break;
+ }
+ }
+ Vec_IntFree( vLits );
+//printf( "Found %d patterns\n", k - iPat );
+
+ // set the new number of patterns
+ if ( fOnSet )
+ p->nPats1 = k;
+ else
+ p->nPats0 = k;
+
+finish:
+
+ sat_solver_delete( pSat );
+p->timeSat += clock() - clk;
+ return RetValue;
+}
+
+
+/**Function*************************************************************
+
Synopsis [Asserts equality of the variable to a constant.]
Description []
diff --git a/src/opt/res/resSim.c b/src/opt/res/resSim.c
index cc896ec0..5c1dd2b6 100644
--- a/src/opt/res/resSim.c
+++ b/src/opt/res/resSim.c
@@ -47,14 +47,17 @@ Res_Sim_t * Res_SimAlloc( int nWords )
memset( p, 0, sizeof(Res_Sim_t) );
// simulation parameters
p->nWords = nWords;
- p->nPats = 8 * sizeof(unsigned) * p->nWords;
+ p->nPats = p->nWords * 8 * sizeof(unsigned);
+ p->nWordsIn = p->nPats;
+ p->nBytesIn = p->nPats * sizeof(unsigned);
+ p->nPatsIn = p->nPats * 8 * sizeof(unsigned);
p->nWordsOut = p->nPats * p->nWords;
p->nPatsOut = p->nPats * p->nPats;
// simulation info
- p->vPats = Vec_PtrAllocSimInfo( 1024, p->nWords );
- p->vPats0 = Vec_PtrAllocSimInfo( 128, p->nWords );
- p->vPats1 = Vec_PtrAllocSimInfo( 128, p->nWords );
- p->vOuts = Vec_PtrAllocSimInfo( 128, p->nWordsOut );
+ p->vPats = Vec_PtrAllocSimInfo( 1024, p->nWordsIn );
+ p->vPats0 = Vec_PtrAllocSimInfo( 128, p->nWords );
+ p->vPats1 = Vec_PtrAllocSimInfo( 128, p->nWords );
+ p->vOuts = Vec_PtrAllocSimInfo( 128, p->nWordsOut );
// resub candidates
p->vCands = Vec_VecStart( 16 );
return p;
@@ -71,26 +74,27 @@ Res_Sim_t * Res_SimAlloc( int nWords )
SeeAlso []
***********************************************************************/
-void Res_SimAdjust( Res_Sim_t * p, Abc_Ntk_t * pAig )
+void Res_SimAdjust( Res_Sim_t * p, Abc_Ntk_t * pAig, int nTruePis )
{
srand( 0xABC );
assert( Abc_NtkIsStrash(pAig) );
p->pAig = pAig;
+ p->nTruePis = nTruePis;
if ( Vec_PtrSize(p->vPats) < Abc_NtkObjNumMax(pAig)+1 )
{
Vec_PtrFree( p->vPats );
- p->vPats = Vec_PtrAllocSimInfo( Abc_NtkObjNumMax(pAig)+1, p->nWords );
+ p->vPats = Vec_PtrAllocSimInfo( Abc_NtkObjNumMax(pAig)+1, p->nWordsIn );
}
- if ( Vec_PtrSize(p->vPats0) < Abc_NtkPiNum(pAig) )
+ if ( Vec_PtrSize(p->vPats0) < nTruePis )
{
Vec_PtrFree( p->vPats0 );
- p->vPats0 = Vec_PtrAllocSimInfo( Abc_NtkPiNum(pAig), p->nWords );
+ p->vPats0 = Vec_PtrAllocSimInfo( nTruePis, p->nWords );
}
- if ( Vec_PtrSize(p->vPats1) < Abc_NtkPiNum(pAig) )
+ if ( Vec_PtrSize(p->vPats1) < nTruePis )
{
Vec_PtrFree( p->vPats1 );
- p->vPats1 = Vec_PtrAllocSimInfo( Abc_NtkPiNum(pAig), p->nWords );
+ p->vPats1 = Vec_PtrAllocSimInfo( nTruePis, p->nWords );
}
if ( Vec_PtrSize(p->vOuts) < Abc_NtkPoNum(pAig) )
{
@@ -98,10 +102,12 @@ void Res_SimAdjust( Res_Sim_t * p, Abc_Ntk_t * pAig )
p->vOuts = Vec_PtrAllocSimInfo( Abc_NtkPoNum(pAig), p->nWordsOut );
}
// clean storage info for patterns
- Abc_InfoClear( Vec_PtrEntry(p->vPats0,0), p->nWords * Abc_NtkPiNum(pAig) );
- Abc_InfoClear( Vec_PtrEntry(p->vPats1,0), p->nWords * Abc_NtkPiNum(pAig) );
+ Abc_InfoClear( Vec_PtrEntry(p->vPats0,0), p->nWords * nTruePis );
+ Abc_InfoClear( Vec_PtrEntry(p->vPats1,0), p->nWords * nTruePis );
p->nPats0 = 0;
p->nPats1 = 0;
+ p->fConst0 = 0;
+ p->fConst1 = 0;
}
/**Function*************************************************************
@@ -137,7 +143,32 @@ void Res_SimFree( Res_Sim_t * p )
SeeAlso []
***********************************************************************/
-void Res_SimSetRandom( Res_Sim_t * p )
+void Abc_InfoRandomBytes( unsigned * p, int nWords )
+{
+ int i, Num;
+ for ( i = nWords - 1; i >= 0; i-- )
+ {
+ Num = rand();
+ p[i] = (Num & 1)? 0xff : 0;
+ p[i] = (p[i] << 8) | ((Num & 2)? 0xff : 0);
+ p[i] = (p[i] << 8) | ((Num & 4)? 0xff : 0);
+ p[i] = (p[i] << 8) | ((Num & 8)? 0xff : 0);
+ }
+// Extra_PrintBinary( stdout, p, 32 ); printf( "\n" );
+}
+
+/**Function*************************************************************
+
+ Synopsis [Sets random PI simulation info.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+void Res_SimSetRandomBytes( Res_Sim_t * p )
{
Abc_Obj_t * pObj;
unsigned * pInfo;
@@ -145,8 +176,155 @@ void Res_SimSetRandom( Res_Sim_t * p )
Abc_NtkForEachPi( p->pAig, pObj, i )
{
pInfo = Vec_PtrEntry( p->vPats, pObj->Id );
- Abc_InfoRandom( pInfo, p->nWords );
+ if ( i < p->nTruePis )
+ Abc_InfoRandomBytes( pInfo, p->nWordsIn );
+ else
+ Abc_InfoRandom( pInfo, p->nWordsIn );
}
+/*
+ // double-check that all are byte-patterns
+ Abc_NtkForEachPi( p->pAig, pObj, i )
+ {
+ if ( i == p->nTruePis )
+ break;
+ pInfoC = (unsigned char *)Vec_PtrEntry( p->vPats, pObj->Id );
+ for ( k = 0; k < p->nBytesIn; k++ )
+ assert( pInfoC[k] == 0 || pInfoC[k] == 0xff );
+ }
+*/
+}
+
+/**Function*************************************************************
+
+ Synopsis [Sets random PI simulation info.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+void Res_SimSetDerivedBytes( Res_Sim_t * p, int fUseWalk )
+{
+ Vec_Ptr_t * vPatsSource[2];
+ int nPatsSource[2];
+ Abc_Obj_t * pObj;
+ unsigned char * pInfo;
+ int i, k, z, s, nPats;
+
+ // set several random patterns
+ assert( p->nBytesIn % 32 == 0 );
+ nPats = p->nBytesIn/8;
+ Abc_NtkForEachPi( p->pAig, pObj, i )
+ {
+ if ( i == p->nTruePis )
+ break;
+ Abc_InfoRandomBytes( Vec_PtrEntry(p->vPats, pObj->Id), nPats/4 );
+ }
+
+ // set special patterns
+ if ( fUseWalk )
+ {
+ for ( z = 0; z < 2; z++ )
+ {
+ // set the zero pattern
+ Abc_NtkForEachPi( p->pAig, pObj, i )
+ {
+ if ( i == p->nTruePis )
+ break;
+ pInfo = (unsigned char *)Vec_PtrEntry( p->vPats, pObj->Id );
+ pInfo[nPats] = z ? 0xff : 0;
+ }
+ if ( ++nPats == p->nBytesIn )
+ return;
+ // set the walking zero pattern
+ for ( k = 0; k < p->nTruePis; k++ )
+ {
+ Abc_NtkForEachPi( p->pAig, pObj, i )
+ {
+ if ( i == p->nTruePis )
+ break;
+ pInfo = (unsigned char *)Vec_PtrEntry( p->vPats, pObj->Id );
+ pInfo[nPats] = ((i == k) ^ z) ? 0xff : 0;
+ }
+ if ( ++nPats == p->nBytesIn )
+ return;
+ }
+ }
+ }
+
+ // decide what patterns to set first
+ if ( p->nPats0 < p->nPats1 )
+ {
+ nPatsSource[0] = p->nPats0;
+ vPatsSource[0] = p->vPats0;
+ nPatsSource[1] = p->nPats1;
+ vPatsSource[1] = p->vPats1;
+ }
+ else
+ {
+ nPatsSource[0] = p->nPats1;
+ vPatsSource[0] = p->vPats1;
+ nPatsSource[1] = p->nPats0;
+ vPatsSource[1] = p->vPats0;
+ }
+ for ( z = 0; z < 2; z++ )
+ {
+ for ( s = nPatsSource[z] - 1; s >= 0; s-- )
+ {
+// if ( s == 0 )
+// printf( "Patterns:\n" );
+ // set the given source pattern
+ for ( k = 0; k < p->nTruePis; k++ )
+ {
+ Abc_NtkForEachPi( p->pAig, pObj, i )
+ {
+ if ( i == p->nTruePis )
+ break;
+ pInfo = (unsigned char *)Vec_PtrEntry( p->vPats, pObj->Id );
+ if ( (i == k) ^ Abc_InfoHasBit( Vec_PtrEntry(vPatsSource[z], i), s ) )
+ {
+ pInfo[nPats] = 0xff;
+// if ( s == 0 )
+// printf( "1" );
+ }
+ else
+ {
+ pInfo[nPats] = 0;
+// if ( s == 0 )
+// printf( "0" );
+ }
+ }
+// if ( s == 0 )
+// printf( "\n" );
+ if ( ++nPats == p->nBytesIn )
+ return;
+ }
+ }
+ }
+ // clean the rest
+ for ( z = nPats; z < p->nBytesIn; z++ )
+ {
+ Abc_NtkForEachPi( p->pAig, pObj, i )
+ {
+ if ( i == p->nTruePis )
+ break;
+ pInfo = (unsigned char *)Vec_PtrEntry( p->vPats, pObj->Id );
+ memset( pInfo + nPats, 0, p->nBytesIn - nPats );
+ }
+ }
+/*
+ // double-check that all are byte-patterns
+ Abc_NtkForEachPi( p->pAig, pObj, i )
+ {
+ if ( i == p->nTruePis )
+ break;
+ pInfo = (unsigned char *)Vec_PtrEntry( p->vPats, pObj->Id );
+ for ( k = 0; k < p->nBytesIn; k++ )
+ assert( pInfo[k] == 0 || pInfo[k] == 0xff );
+ }
+*/
}
/**Function*************************************************************
@@ -167,6 +345,8 @@ void Res_SimSetGiven( Res_Sim_t * p, Vec_Ptr_t * vInfo )
int i, w;
Abc_NtkForEachPi( p->pAig, pObj, i )
{
+ if ( i == p->nTruePis )
+ break;
pInfo = Vec_PtrEntry( p->vPats, pObj->Id );
pInfo2 = Vec_PtrEntry( vInfo, i );
for ( w = 0; w < p->nWords; w++ )
@@ -249,64 +429,17 @@ void Res_SimTransferOne( Abc_Obj_t * pNode, Vec_Ptr_t * vSimInfo, int nSimWords
SeeAlso []
***********************************************************************/
-void Res_SimPerformRound( Res_Sim_t * p )
+void Res_SimPerformRound( Res_Sim_t * p, int nWords )
{
Abc_Obj_t * pObj;
int i;
- Abc_InfoFill( Vec_PtrEntry(p->vPats,0), p->nWords );
+ Abc_InfoFill( Vec_PtrEntry(p->vPats,0), nWords );
Abc_AigForEachAnd( p->pAig, pObj, i )
- Res_SimPerformOne( pObj, p->vPats, p->nWords );
+ Res_SimPerformOne( pObj, p->vPats, nWords );
Abc_NtkForEachPo( p->pAig, pObj, i )
- Res_SimTransferOne( pObj, p->vPats, p->nWords );
+ Res_SimTransferOne( pObj, p->vPats, nWords );
}
-/**Function*************************************************************
-
- Synopsis [Processes simulation patterns.]
-
- Description []
-
- SideEffects []
-
- SeeAlso []
-
-***********************************************************************/
-void Res_SimProcessPats( Res_Sim_t * p )
-{
- Abc_Obj_t * pObj;
- unsigned * pInfoCare, * pInfoNode;
- int i, j, nDcs = 0;
- pInfoCare = Vec_PtrEntry( p->vPats, Abc_NtkPo(p->pAig, 0)->Id );
- pInfoNode = Vec_PtrEntry( p->vPats, Abc_NtkPo(p->pAig, 1)->Id );
- for ( i = 0; i < p->nPats; i++ )
- {
- // skip don't-care patterns
- if ( !Abc_InfoHasBit(pInfoCare, i) )
- {
- nDcs++;
- continue;
- }
- // separate offset and onset patterns
- if ( !Abc_InfoHasBit(pInfoNode, i) )
- {
- if ( p->nPats0 >= p->nPats )
- continue;
- Abc_NtkForEachPi( p->pAig, pObj, j )
- if ( Abc_InfoHasBit( Vec_PtrEntry(p->vPats, pObj->Id), i ) )
- Abc_InfoSetBit( Vec_PtrEntry(p->vPats0, j), p->nPats0 );
- p->nPats0++;
- }
- else
- {
- if ( p->nPats1 >= p->nPats )
- continue;
- Abc_NtkForEachPi( p->pAig, pObj, j )
- if ( Abc_InfoHasBit( Vec_PtrEntry(p->vPats, pObj->Id), i ) )
- Abc_InfoSetBit( Vec_PtrEntry(p->vPats1, j), p->nPats1 );
- p->nPats1++;
- }
- }
-}
/**Function*************************************************************
@@ -396,7 +529,50 @@ void Res_SimDeriveInfoComplement( Res_Sim_t * p )
/**Function*************************************************************
- Synopsis [Free simulation engine.]
+ Synopsis [Prints output patterns.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+void Res_SimPrintOutPatterns( Res_Sim_t * p, Abc_Ntk_t * pAig )
+{
+ Abc_Obj_t * pObj;
+ unsigned * pInfo2;
+ int i;
+ Abc_NtkForEachPo( pAig, pObj, i )
+ {
+ pInfo2 = Vec_PtrEntry( p->vOuts, i );
+ Extra_PrintBinary( stdout, pInfo2, p->nPatsOut );
+ printf( "\n" );
+ }
+}
+
+/**Function*************************************************************
+
+ Synopsis [Prints output patterns.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+void Res_SimPrintNodePatterns( Res_Sim_t * p, Abc_Ntk_t * pAig )
+{
+ unsigned * pInfo;
+ pInfo = Vec_PtrEntry( p->vPats, Abc_NtkPo(p->pAig, 1)->Id );
+ Extra_PrintBinary( stdout, pInfo, p->nPats );
+ printf( "\n" );
+}
+
+/**Function*************************************************************
+
+ Synopsis [Counts the number of patters of different type.]
Description []
@@ -405,40 +581,102 @@ void Res_SimDeriveInfoComplement( Res_Sim_t * p )
SeeAlso []
***********************************************************************/
-void Res_SimReportOne( Res_Sim_t * p )
+void Res_SimCountResults( Res_Sim_t * p, int * pnDcs, int * pnOnes, int * pnZeros, int fVerbose )
{
- unsigned * pInfoCare, * pInfoNode;
- int i, nDcs, nOnes, nZeros;
- pInfoCare = Vec_PtrEntry( p->vPats, Abc_NtkPo(p->pAig, 0)->Id );
- pInfoNode = Vec_PtrEntry( p->vPats, Abc_NtkPo(p->pAig, 1)->Id );
- nDcs = nOnes = nZeros = 0;
- for ( i = 0; i < p->nPats; i++ )
+ unsigned char * pInfoCare, * pInfoNode;
+ int i, nTotal = 0;
+ pInfoCare = (unsigned char *)Vec_PtrEntry( p->vPats, Abc_NtkPo(p->pAig, 0)->Id );
+ pInfoNode = (unsigned char *)Vec_PtrEntry( p->vPats, Abc_NtkPo(p->pAig, 1)->Id );
+ for ( i = 0; i < p->nBytesIn; i++ )
+ {
+ if ( !pInfoCare[i] )
+ (*pnDcs)++;
+ else if ( !pInfoNode[i] )
+ (*pnZeros)++;
+ else
+ (*pnOnes)++;
+ }
+ nTotal += *pnDcs;
+ nTotal += *pnZeros;
+ nTotal += *pnOnes;
+ if ( fVerbose )
+ {
+ printf( "Dc = %7.2f %% ", 100.0*(*pnDcs) /nTotal );
+ printf( "On = %7.2f %% ", 100.0*(*pnOnes) /nTotal );
+ printf( "Off = %7.2f %% ", 100.0*(*pnZeros)/nTotal );
+ }
+}
+
+/**Function*************************************************************
+
+ Synopsis [Counts the number of patters of different type.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+void Res_SimCollectPatterns( Res_Sim_t * p, int fVerbose )
+{
+ Abc_Obj_t * pObj;
+ unsigned char * pInfoCare, * pInfoNode, * pInfo;
+ int i, j;
+ pInfoCare = (unsigned char *)Vec_PtrEntry( p->vPats, Abc_NtkPo(p->pAig, 0)->Id );
+ pInfoNode = (unsigned char *)Vec_PtrEntry( p->vPats, Abc_NtkPo(p->pAig, 1)->Id );
+ for ( i = 0; i < p->nBytesIn; i++ )
{
// skip don't-care patterns
- if ( !Abc_InfoHasBit(pInfoCare, i) )
- {
- nDcs++;
+ if ( !pInfoCare[i] )
continue;
- }
// separate offset and onset patterns
- if ( !Abc_InfoHasBit(pInfoNode, i) )
- nZeros++;
+ assert( pInfoNode[i] == 0 || pInfoNode[i] == 0xff );
+ if ( !pInfoNode[i] )
+ {
+ if ( p->nPats0 >= p->nPats )
+ continue;
+ Abc_NtkForEachPi( p->pAig, pObj, j )
+ {
+ if ( j == p->nTruePis )
+ break;
+ pInfo = (unsigned char *)Vec_PtrEntry( p->vPats, pObj->Id );
+ assert( pInfo[i] == 0 || pInfo[i] == 0xff );
+ if ( pInfo[i] )
+ Abc_InfoSetBit( Vec_PtrEntry(p->vPats0, j), p->nPats0 );
+ }
+ p->nPats0++;
+ }
else
- nOnes++;
+ {
+ if ( p->nPats1 >= p->nPats )
+ continue;
+ Abc_NtkForEachPi( p->pAig, pObj, j )
+ {
+ if ( j == p->nTruePis )
+ break;
+ pInfo = (unsigned char *)Vec_PtrEntry( p->vPats, pObj->Id );
+ assert( pInfo[i] == 0 || pInfo[i] == 0xff );
+ if ( pInfo[i] )
+ Abc_InfoSetBit( Vec_PtrEntry(p->vPats1, j), p->nPats1 );
+ }
+ p->nPats1++;
+ }
+ if ( p->nPats0 >= p->nPats && p->nPats1 >= p->nPats )
+ break;
+ }
+ if ( fVerbose )
+ {
+ printf( "| " );
+ printf( "On = %3d ", p->nPats1 );
+ printf( "Off = %3d ", p->nPats0 );
+ printf( "\n" );
}
- printf( "On = %3d (%7.2f %%) ", nOnes, 100.0*nOnes/p->nPats );
- printf( "Off = %3d (%7.2f %%) ", nZeros, 100.0*nZeros/p->nPats );
- printf( "Dc = %3d (%7.2f %%) ", nDcs, 100.0*nDcs/p->nPats );
- printf( "P0 = %3d ", p->nPats0 );
- printf( "P1 = %3d ", p->nPats1 );
- if ( p->nPats0 < 4 || p->nPats1 < 4 )
- printf( "*" );
- printf( "\n" );
}
/**Function*************************************************************
- Synopsis [Prints output patterns.]
+ Synopsis [Verifies the last pattern.]
Description []
@@ -447,17 +685,33 @@ void Res_SimReportOne( Res_Sim_t * p )
SeeAlso []
***********************************************************************/
-void Res_SimPrintOutPatterns( Res_Sim_t * p, Abc_Ntk_t * pAig )
+int Res_SimVerifyValue( Res_Sim_t * p, int fOnSet )
{
Abc_Obj_t * pObj;
- unsigned * pInfo2;
- int i;
- Abc_NtkForEachPo( pAig, pObj, i )
+ unsigned * pInfo, * pInfo2;
+ int i, value;
+ Abc_NtkForEachPi( p->pAig, pObj, i )
{
- pInfo2 = Vec_PtrEntry( p->vOuts, i );
- Extra_PrintBinary( stdout, pInfo2, p->nPatsOut );
- printf( "\n" );
+ if ( i == p->nTruePis )
+ break;
+ if ( fOnSet )
+ {
+ pInfo2 = Vec_PtrEntry( p->vPats1, i );
+ value = Abc_InfoHasBit( pInfo2, p->nPats1 - 1 );
+ }
+ else
+ {
+ pInfo2 = Vec_PtrEntry( p->vPats0, i );
+ value = Abc_InfoHasBit( pInfo2, p->nPats0 - 1 );
+ }
+ pInfo = Vec_PtrEntry( p->vPats, pObj->Id );
+ pInfo[0] = value ? ~0 : 0;
}
+ Res_SimPerformRound( p, 1 );
+ pObj = Abc_NtkPo( p->pAig, 1 );
+ pInfo = Vec_PtrEntry( p->vPats, pObj->Id );
+ assert( pInfo[0] == 0 || pInfo[0] == ~0 );
+ return pInfo[0] > 0;
}
/**Function*************************************************************
@@ -471,30 +725,43 @@ void Res_SimPrintOutPatterns( Res_Sim_t * p, Abc_Ntk_t * pAig )
SeeAlso []
***********************************************************************/
-int Res_SimPrepare( Res_Sim_t * p, Abc_Ntk_t * pAig )
+int Res_SimPrepare( Res_Sim_t * p, Abc_Ntk_t * pAig, int nTruePis, int fVerbose )
{
- int Limit;
+ int i, nOnes = 0, nZeros = 0, nDcs = 0;
+ if ( fVerbose )
+ printf( "\n" );
// prepare the manager
- Res_SimAdjust( p, pAig );
- // collect 0/1 simulation info
- for ( Limit = 0; Limit < 10; Limit++ )
+ Res_SimAdjust( p, pAig, nTruePis );
+ // estimate the number of patterns
+ Res_SimSetRandomBytes( p );
+ Res_SimPerformRound( p, p->nWordsIn );
+ Res_SimCountResults( p, &nDcs, &nOnes, &nZeros, fVerbose );
+ // collect the patterns
+ Res_SimCollectPatterns( p, fVerbose );
+ // add more patterns using constraint simulation
+ if ( p->nPats0 < 8 )
{
- Res_SimSetRandom( p );
- Res_SimPerformRound( p );
- Res_SimProcessPats( p );
- if ( !(p->nPats0 < p->nPats || p->nPats1 < p->nPats) )
- break;
+ if ( !Res_SatSimulate( p, 16, 0 ) )
+ return p->fConst0 || p->fConst1;
+// return 0;
+// printf( "Value0 = %d\n", Res_SimVerifyValue( p, 0 ) );
}
-// printf( "%d ", Limit );
- // report the last set of patterns
-// Res_SimReportOne( p );
-// printf( "\n" );
- // quit if there is not enough
-// if ( p->nPats0 < 4 || p->nPats1 < 4 )
- if ( p->nPats0 < 4 || p->nPats1 < 4 )
+ if ( p->nPats1 < 8 )
{
-// Res_SimReportOne( p );
- return 0;
+ if ( !Res_SatSimulate( p, 16, 1 ) )
+ return p->fConst0 || p->fConst1;
+// return 0;
+// printf( "Value1 = %d\n", Res_SimVerifyValue( p, 1 ) );
+ }
+ // generate additional patterns
+ for ( i = 0; i < 2; i++ )
+ {
+ if ( p->nPats0 > p->nPats*7/8 && p->nPats1 > p->nPats*7/8 )
+ break;
+ Res_SimSetDerivedBytes( p, i==0 );
+ Res_SimPerformRound( p, p->nWordsIn );
+ Res_SimCountResults( p, &nDcs, &nOnes, &nZeros, fVerbose );
+ Res_SimCollectPatterns( p, fVerbose );
}
// create bit-matrix info
if ( p->nPats0 < p->nPats )
@@ -503,11 +770,13 @@ int Res_SimPrepare( Res_Sim_t * p, Abc_Ntk_t * pAig )
Res_SimPadSimInfo( p->vPats1, p->nPats1, p->nWords );
// resimulate 0-patterns
Res_SimSetGiven( p, p->vPats0 );
- Res_SimPerformRound( p );
+ Res_SimPerformRound( p, p->nWords );
+//Res_SimPrintNodePatterns( p, pAig );
Res_SimDeriveInfoReplicate( p );
// resimulate 1-patterns
Res_SimSetGiven( p, p->vPats1 );
- Res_SimPerformRound( p );
+ Res_SimPerformRound( p, p->nWords );
+//Res_SimPrintNodePatterns( p, pAig );
Res_SimDeriveInfoComplement( p );
// print output patterns
// Res_SimPrintOutPatterns( p, pAig );
diff --git a/src/opt/res/resSim_old.c b/src/opt/res/resSim_old.c
new file mode 100644
index 00000000..23ce29e4
--- /dev/null
+++ b/src/opt/res/resSim_old.c
@@ -0,0 +1,521 @@
+/**CFile****************************************************************
+
+ FileName [resSim.c]
+
+ SystemName [ABC: Logic synthesis and verification system.]
+
+ PackageName [Resynthesis package.]
+
+ Synopsis [Simulation engine.]
+
+ Author [Alan Mishchenko]
+
+ Affiliation [UC Berkeley]
+
+ Date [Ver. 1.0. Started - January 15, 2007.]
+
+ Revision [$Id: resSim.c,v 1.00 2007/01/15 00:00:00 alanmi Exp $]
+
+***********************************************************************/
+
+#include "abc.h"
+#include "resInt.h"
+
+////////////////////////////////////////////////////////////////////////
+/// DECLARATIONS ///
+////////////////////////////////////////////////////////////////////////
+
+////////////////////////////////////////////////////////////////////////
+/// FUNCTION DEFINITIONS ///
+////////////////////////////////////////////////////////////////////////
+
+/**Function*************************************************************
+
+ Synopsis [Allocate simulation engine.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+Res_Sim_t * Res_SimAlloc( int nWords )
+{
+ Res_Sim_t * p;
+ p = ALLOC( Res_Sim_t, 1 );
+ memset( p, 0, sizeof(Res_Sim_t) );
+ // simulation parameters
+ p->nWords = nWords;
+ p->nPats = 8 * sizeof(unsigned) * p->nWords;
+ p->nWordsOut = p->nPats * p->nWords;
+ p->nPatsOut = p->nPats * p->nPats;
+ // simulation info
+ p->vPats = Vec_PtrAllocSimInfo( 1024, p->nWords );
+ p->vPats0 = Vec_PtrAllocSimInfo( 128, p->nWords );
+ p->vPats1 = Vec_PtrAllocSimInfo( 128, p->nWords );
+ p->vOuts = Vec_PtrAllocSimInfo( 128, p->nWordsOut );
+ // resub candidates
+ p->vCands = Vec_VecStart( 16 );
+ return p;
+}
+
+/**Function*************************************************************
+
+ Synopsis [Allocate simulation engine.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+void Res_SimAdjust( Res_Sim_t * p, Abc_Ntk_t * pAig )
+{
+ srand( 0xABC );
+
+ assert( Abc_NtkIsStrash(pAig) );
+ p->pAig = pAig;
+ if ( Vec_PtrSize(p->vPats) < Abc_NtkObjNumMax(pAig)+1 )
+ {
+ Vec_PtrFree( p->vPats );
+ p->vPats = Vec_PtrAllocSimInfo( Abc_NtkObjNumMax(pAig)+1, p->nWords );
+ }
+ if ( Vec_PtrSize(p->vPats0) < Abc_NtkPiNum(pAig) )
+ {
+ Vec_PtrFree( p->vPats0 );
+ p->vPats0 = Vec_PtrAllocSimInfo( Abc_NtkPiNum(pAig), p->nWords );
+ }
+ if ( Vec_PtrSize(p->vPats1) < Abc_NtkPiNum(pAig) )
+ {
+ Vec_PtrFree( p->vPats1 );
+ p->vPats1 = Vec_PtrAllocSimInfo( Abc_NtkPiNum(pAig), p->nWords );
+ }
+ if ( Vec_PtrSize(p->vOuts) < Abc_NtkPoNum(pAig) )
+ {
+ Vec_PtrFree( p->vOuts );
+ p->vOuts = Vec_PtrAllocSimInfo( Abc_NtkPoNum(pAig), p->nWordsOut );
+ }
+ // clean storage info for patterns
+ Abc_InfoClear( Vec_PtrEntry(p->vPats0,0), p->nWords * Abc_NtkPiNum(pAig) );
+ Abc_InfoClear( Vec_PtrEntry(p->vPats1,0), p->nWords * Abc_NtkPiNum(pAig) );
+ p->nPats0 = 0;
+ p->nPats1 = 0;
+}
+
+/**Function*************************************************************
+
+ Synopsis [Free simulation engine.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+void Res_SimFree( Res_Sim_t * p )
+{
+ Vec_PtrFree( p->vPats );
+ Vec_PtrFree( p->vPats0 );
+ Vec_PtrFree( p->vPats1 );
+ Vec_PtrFree( p->vOuts );
+ Vec_VecFree( p->vCands );
+ free( p );
+}
+
+
+/**Function*************************************************************
+
+ Synopsis [Sets random PI simulation info.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+void Res_SimSetRandom( Res_Sim_t * p )
+{
+ Abc_Obj_t * pObj;
+ unsigned * pInfo;
+ int i;
+ Abc_NtkForEachPi( p->pAig, pObj, i )
+ {
+ pInfo = Vec_PtrEntry( p->vPats, pObj->Id );
+ Abc_InfoRandom( pInfo, p->nWords );
+ }
+}
+
+/**Function*************************************************************
+
+ Synopsis [Sets given PI simulation info.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+void Res_SimSetGiven( Res_Sim_t * p, Vec_Ptr_t * vInfo )
+{
+ Abc_Obj_t * pObj;
+ unsigned * pInfo, * pInfo2;
+ int i, w;
+ Abc_NtkForEachPi( p->pAig, pObj, i )
+ {
+ pInfo = Vec_PtrEntry( p->vPats, pObj->Id );
+ pInfo2 = Vec_PtrEntry( vInfo, i );
+ for ( w = 0; w < p->nWords; w++ )
+ pInfo[w] = pInfo2[w];
+ }
+}
+
+/**Function*************************************************************
+
+ Synopsis [Simulates one node.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+void Res_SimPerformOne( Abc_Obj_t * pNode, Vec_Ptr_t * vSimInfo, int nSimWords )
+{
+ unsigned * pInfo, * pInfo1, * pInfo2;
+ int k, fComp1, fComp2;
+ // simulate the internal nodes
+ assert( Abc_ObjIsNode(pNode) );
+ pInfo = Vec_PtrEntry(vSimInfo, pNode->Id);
+ pInfo1 = Vec_PtrEntry(vSimInfo, Abc_ObjFaninId0(pNode));
+ pInfo2 = Vec_PtrEntry(vSimInfo, Abc_ObjFaninId1(pNode));
+ fComp1 = Abc_ObjFaninC0(pNode);
+ fComp2 = Abc_ObjFaninC1(pNode);
+ if ( fComp1 && fComp2 )
+ for ( k = 0; k < nSimWords; k++ )
+ pInfo[k] = ~pInfo1[k] & ~pInfo2[k];
+ else if ( fComp1 && !fComp2 )
+ for ( k = 0; k < nSimWords; k++ )
+ pInfo[k] = ~pInfo1[k] & pInfo2[k];
+ else if ( !fComp1 && fComp2 )
+ for ( k = 0; k < nSimWords; k++ )
+ pInfo[k] = pInfo1[k] & ~pInfo2[k];
+ else // if ( fComp1 && fComp2 )
+ for ( k = 0; k < nSimWords; k++ )
+ pInfo[k] = pInfo1[k] & pInfo2[k];
+}
+
+/**Function*************************************************************
+
+ Synopsis [Simulates one CO node.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+void Res_SimTransferOne( Abc_Obj_t * pNode, Vec_Ptr_t * vSimInfo, int nSimWords )
+{
+ unsigned * pInfo, * pInfo1;
+ int k, fComp1;
+ // simulate the internal nodes
+ assert( Abc_ObjIsCo(pNode) );
+ pInfo = Vec_PtrEntry(vSimInfo, pNode->Id);
+ pInfo1 = Vec_PtrEntry(vSimInfo, Abc_ObjFaninId0(pNode));
+ fComp1 = Abc_ObjFaninC0(pNode);
+ if ( fComp1 )
+ for ( k = 0; k < nSimWords; k++ )
+ pInfo[k] = ~pInfo1[k];
+ else
+ for ( k = 0; k < nSimWords; k++ )
+ pInfo[k] = pInfo1[k];
+}
+
+/**Function*************************************************************
+
+ Synopsis [Performs one round of simulation.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+void Res_SimPerformRound( Res_Sim_t * p )
+{
+ Abc_Obj_t * pObj;
+ int i;
+ Abc_InfoFill( Vec_PtrEntry(p->vPats,0), p->nWords );
+ Abc_AigForEachAnd( p->pAig, pObj, i )
+ Res_SimPerformOne( pObj, p->vPats, p->nWords );
+ Abc_NtkForEachPo( p->pAig, pObj, i )
+ Res_SimTransferOne( pObj, p->vPats, p->nWords );
+}
+
+/**Function*************************************************************
+
+ Synopsis [Processes simulation patterns.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+void Res_SimProcessPats( Res_Sim_t * p )
+{
+ Abc_Obj_t * pObj;
+ unsigned * pInfoCare, * pInfoNode;
+ int i, j, nDcs = 0;
+ pInfoCare = Vec_PtrEntry( p->vPats, Abc_NtkPo(p->pAig, 0)->Id );
+ pInfoNode = Vec_PtrEntry( p->vPats, Abc_NtkPo(p->pAig, 1)->Id );
+ for ( i = 0; i < p->nPats; i++ )
+ {
+ // skip don't-care patterns
+ if ( !Abc_InfoHasBit(pInfoCare, i) )
+ {
+ nDcs++;
+ continue;
+ }
+ // separate offset and onset patterns
+ if ( !Abc_InfoHasBit(pInfoNode, i) )
+ {
+ if ( p->nPats0 >= p->nPats )
+ continue;
+ Abc_NtkForEachPi( p->pAig, pObj, j )
+ if ( Abc_InfoHasBit( Vec_PtrEntry(p->vPats, pObj->Id), i ) )
+ Abc_InfoSetBit( Vec_PtrEntry(p->vPats0, j), p->nPats0 );
+ p->nPats0++;
+ }
+ else
+ {
+ if ( p->nPats1 >= p->nPats )
+ continue;
+ Abc_NtkForEachPi( p->pAig, pObj, j )
+ if ( Abc_InfoHasBit( Vec_PtrEntry(p->vPats, pObj->Id), i ) )
+ Abc_InfoSetBit( Vec_PtrEntry(p->vPats1, j), p->nPats1 );
+ p->nPats1++;
+ }
+ }
+}
+
+/**Function*************************************************************
+
+ Synopsis [Pads the extra space with duplicated simulation info.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+void Res_SimPadSimInfo( Vec_Ptr_t * vPats, int nPats, int nWords )
+{
+ unsigned * pInfo;
+ int i, w, iWords;
+ assert( nPats > 0 && nPats < nWords * 8 * (int) sizeof(unsigned) );
+ // pad the first word
+ if ( nPats < 8 * sizeof(unsigned) )
+ {
+ Vec_PtrForEachEntry( vPats, pInfo, i )
+ if ( pInfo[0] & 1 )
+ pInfo[0] |= ((~0) << nPats);
+ nPats = 8 * sizeof(unsigned);
+ }
+ // pad the empty words
+ iWords = nPats / (8 * sizeof(unsigned));
+ Vec_PtrForEachEntry( vPats, pInfo, i )
+ {
+ for ( w = iWords; w < nWords; w++ )
+ pInfo[w] = pInfo[0];
+ }
+}
+
+/**Function*************************************************************
+
+ Synopsis [Duplicates the simulation info to fill the space.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+void Res_SimDeriveInfoReplicate( Res_Sim_t * p )
+{
+ unsigned * pInfo, * pInfo2;
+ Abc_Obj_t * pObj;
+ int i, j, w;
+ Abc_NtkForEachPo( p->pAig, pObj, i )
+ {
+ pInfo = Vec_PtrEntry( p->vPats, pObj->Id );
+ pInfo2 = Vec_PtrEntry( p->vOuts, i );
+ for ( j = 0; j < p->nPats; j++ )
+ for ( w = 0; w < p->nWords; w++ )
+ *pInfo2++ = pInfo[w];
+ }
+}
+
+/**Function*************************************************************
+
+ Synopsis [Complement the simulation info if necessary.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+void Res_SimDeriveInfoComplement( Res_Sim_t * p )
+{
+ unsigned * pInfo, * pInfo2;
+ Abc_Obj_t * pObj;
+ int i, j, w;
+ Abc_NtkForEachPo( p->pAig, pObj, i )
+ {
+ pInfo = Vec_PtrEntry( p->vPats, pObj->Id );
+ pInfo2 = Vec_PtrEntry( p->vOuts, i );
+ for ( j = 0; j < p->nPats; j++, pInfo2 += p->nWords )
+ if ( Abc_InfoHasBit( pInfo, j ) )
+ for ( w = 0; w < p->nWords; w++ )
+ pInfo2[w] = ~pInfo2[w];
+ }
+}
+
+/**Function*************************************************************
+
+ Synopsis [Free simulation engine.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+void Res_SimReportOne( Res_Sim_t * p )
+{
+ unsigned * pInfoCare, * pInfoNode;
+ int i, nDcs, nOnes, nZeros;
+ pInfoCare = Vec_PtrEntry( p->vPats, Abc_NtkPo(p->pAig, 0)->Id );
+ pInfoNode = Vec_PtrEntry( p->vPats, Abc_NtkPo(p->pAig, 1)->Id );
+ nDcs = nOnes = nZeros = 0;
+ for ( i = 0; i < p->nPats; i++ )
+ {
+ // skip don't-care patterns
+ if ( !Abc_InfoHasBit(pInfoCare, i) )
+ {
+ nDcs++;
+ continue;
+ }
+ // separate offset and onset patterns
+ if ( !Abc_InfoHasBit(pInfoNode, i) )
+ nZeros++;
+ else
+ nOnes++;
+ }
+ printf( "On = %3d (%7.2f %%) ", nOnes, 100.0*nOnes/p->nPats );
+ printf( "Off = %3d (%7.2f %%) ", nZeros, 100.0*nZeros/p->nPats );
+ printf( "Dc = %3d (%7.2f %%) ", nDcs, 100.0*nDcs/p->nPats );
+ printf( "P0 = %3d ", p->nPats0 );
+ printf( "P1 = %3d ", p->nPats1 );
+ if ( p->nPats0 < 4 || p->nPats1 < 4 )
+ printf( "*" );
+ printf( "\n" );
+}
+
+/**Function*************************************************************
+
+ Synopsis [Prints output patterns.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+void Res_SimPrintOutPatterns( Res_Sim_t * p, Abc_Ntk_t * pAig )
+{
+ Abc_Obj_t * pObj;
+ unsigned * pInfo2;
+ int i;
+ Abc_NtkForEachPo( pAig, pObj, i )
+ {
+ pInfo2 = Vec_PtrEntry( p->vOuts, i );
+ Extra_PrintBinary( stdout, pInfo2, p->nPatsOut );
+ printf( "\n" );
+ }
+}
+
+/**Function*************************************************************
+
+ Synopsis [Prepares simulation info for candidate filtering.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+int Res_SimPrepare( Res_Sim_t * p, Abc_Ntk_t * pAig, int nTruePis, int fVerbose )
+{
+ int Limit;
+ // prepare the manager
+ Res_SimAdjust( p, pAig );
+ // collect 0/1 simulation info
+ for ( Limit = 0; Limit < 10; Limit++ )
+ {
+ Res_SimSetRandom( p );
+ Res_SimPerformRound( p );
+ Res_SimProcessPats( p );
+ if ( !(p->nPats0 < p->nPats || p->nPats1 < p->nPats) )
+ break;
+ }
+// printf( "%d ", Limit );
+ // report the last set of patterns
+// Res_SimReportOne( p );
+// printf( "\n" );
+ // quit if there is not enough
+// if ( p->nPats0 < 4 || p->nPats1 < 4 )
+ if ( p->nPats0 < 4 || p->nPats1 < 4 )
+ {
+// Res_SimReportOne( p );
+ return 0;
+ }
+ // create bit-matrix info
+ if ( p->nPats0 < p->nPats )
+ Res_SimPadSimInfo( p->vPats0, p->nPats0, p->nWords );
+ if ( p->nPats1 < p->nPats )
+ Res_SimPadSimInfo( p->vPats1, p->nPats1, p->nWords );
+ // resimulate 0-patterns
+ Res_SimSetGiven( p, p->vPats0 );
+ Res_SimPerformRound( p );
+ Res_SimDeriveInfoReplicate( p );
+ // resimulate 1-patterns
+ Res_SimSetGiven( p, p->vPats1 );
+ Res_SimPerformRound( p );
+ Res_SimDeriveInfoComplement( p );
+ // print output patterns
+// Res_SimPrintOutPatterns( p, pAig );
+ return 1;
+}
+
+////////////////////////////////////////////////////////////////////////
+/// END OF FILE ///
+////////////////////////////////////////////////////////////////////////
+
+
diff --git a/src/opt/res/resWin.c b/src/opt/res/resWin.c
index 80a65ea8..a3648925 100644
--- a/src/opt/res/resWin.c
+++ b/src/opt/res/resWin.c
@@ -94,7 +94,7 @@ void Res_WinFree( Res_Win_t * p )
SeeAlso []
***********************************************************************/
-void Res_WinCollectLeavesAndNodes( Res_Win_t * p )
+int Res_WinCollectLeavesAndNodes( Res_Win_t * p )
{
Vec_Ptr_t * vFront;
Abc_Obj_t * pObj, * pTemp;
@@ -127,7 +127,8 @@ void Res_WinCollectLeavesAndNodes( Res_Win_t * p )
}
}
}
- assert( Vec_PtrSize(p->vLeaves) > 0 );
+ if ( Vec_PtrSize(p->vLeaves) == 0 )
+ return 0;
// collect the nodes in the reverse order
Vec_PtrClear( p->vNodes );
@@ -146,6 +147,7 @@ void Res_WinCollectLeavesAndNodes( Res_Win_t * p )
// set minimum traversal level
p->nLevTravMin = ABC_MAX( ((int)p->pNode->Level) - p->nWinTfiMax - p->nLevTfiMinus, p->nLevLeafMin );
assert( p->nLevTravMin >= 0 );
+ return 1;
}
@@ -371,6 +373,7 @@ void Res_WinAddMissing_rec( Res_Win_t * p, Abc_Obj_t * pObj, int nLevTravMin )
// if this is not an internal node - make it a new branch
if ( !Abc_NodeIsTravIdPrevious(pObj) )
{
+ assert( Vec_PtrFind(p->vLeaves, pObj) == -1 );
Abc_NodeSetTravIdCurrent( pObj );
Vec_PtrPush( p->vBranches, pObj );
return;
@@ -452,11 +455,15 @@ int Res_WinCompute( Abc_Obj_t * pNode, int nWinTfiMax, int nWinTfoMax, Res_Win_t
p->pNode = pNode;
p->nWinTfiMax = nWinTfiMax;
p->nWinTfoMax = nWinTfoMax;
+
+ Vec_PtrClear( p->vBranches );
+ Vec_PtrClear( p->vDivs );
Vec_PtrClear( p->vRoots );
Vec_PtrPush( p->vRoots, pNode );
// compute the leaves
- Res_WinCollectLeavesAndNodes( p );
+ if ( !Res_WinCollectLeavesAndNodes( p ) )
+ return 0;
// compute the candidate roots
if ( p->nWinTfoMax > 0 && Res_WinComputeRoots(p) )
diff --git a/src/sat/bsat/satSolver.c b/src/sat/bsat/satSolver.c
index c4847be4..5c9294b0 100644
--- a/src/sat/bsat/satSolver.c
+++ b/src/sat/bsat/satSolver.c
@@ -457,6 +457,12 @@ static inline void sat_solver_canceluntil(sat_solver* s, int level) {
reasons = s->reasons;
bound = (veci_begin(&s->trail_lim))[level];
+ ////////////////////////////////////////
+ // added to cancel all assignments
+// if ( level == -1 )
+// bound = 0;
+ ////////////////////////////////////////
+
for (c = s->qtail-1; c >= bound; c--) {
int x = lit_var(trail[c]);
values [x] = l_Undef;
@@ -881,7 +887,7 @@ static lbool sat_solver_search(sat_solver* s, sint64 nof_conflicts, sint64 nof_l
return l_Undef;
}
- if (sat_solver_dlevel(s) == 0)
+ if (sat_solver_dlevel(s) == 0 && !s->fSkipSimplify)
// Simplify the set of problem clauses:
sat_solver_simplify(s);
diff --git a/src/sat/bsat/satSolver.h b/src/sat/bsat/satSolver.h
index 8f71370f..986e48d5 100644
--- a/src/sat/bsat/satSolver.h
+++ b/src/sat/bsat/satSolver.h
@@ -170,6 +170,8 @@ struct sat_solver_t
Sat_MmStep_t * pMem;
+ int fSkipSimplify; // set to one to skip simplification of the clause database
+
// clause store
void * pStore;
generated by cgit v1.2.3 (git 2.25.1) at 2024-07-04 18:17:45 +0000