Version abc50916

abc.plg

@@ -6,313 +6,13 @@
 --------------------Configuration: abc - Win32 Release--------------------
 </h3>
 <h3>Command Lines</h3>
-Creating temporary file "C:\DOCUME~1\alanmi\LOCALS~1\Temp\RSP211A.tmp" with contents
+Creating temporary file "C:\DOCUME~1\alanmi\LOCALS~1\Temp\RSP23BD.tmp" with contents
 [
 /nologo /ML /W3 /GX /O2 /I "src\base\abc" /I "src\base\abci" /I "src\base\abcs" /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\msat" /I "src\sat\fraig" /I "src\opt\cut" /I "src\opt\dec" /I "src\opt\fxu" /I "src\opt\rwr" /I "src\map\fpga" /I "src\map\pga" /I "src\map\mapper" /I "src\map\mapp" /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\vec" /D "WIN32" /D "NDEBUG" /D "_CONSOLE" /D "_MBCS" /D "__STDC__" /D "HAVE_ASSERT_H" /FR"Release/" /Fp"Release/abc.pch" /YX /Fo"Release/" /Fd"Release/" /FD /c 
-"C:\_projects\abc\src\base\abc\abcAig.c"
-"C:\_projects\abc\src\base\abc\abcCheck.c"
-"C:\_projects\abc\src\base\abc\abcDfs.c"
-"C:\_projects\abc\src\base\abc\abcFanio.c"
-"C:\_projects\abc\src\base\abc\abcFunc.c"
-"C:\_projects\abc\src\base\abc\abcLatch.c"
-"C:\_projects\abc\src\base\abc\abcMinBase.c"
-"C:\_projects\abc\src\base\abc\abcNames.c"
-"C:\_projects\abc\src\base\abc\abcNetlist.c"
-"C:\_projects\abc\src\base\abc\abcNtk.c"
-"C:\_projects\abc\src\base\abc\abcObj.c"
-"C:\_projects\abc\src\base\abc\abcRefs.c"
-"C:\_projects\abc\src\base\abc\abcShow.c"
-"C:\_projects\abc\src\base\abc\abcSop.c"
-"C:\_projects\abc\src\base\abc\abcUtil.c"
 "C:\_projects\abc\src\base\abci\abc.c"
-"C:\_projects\abc\src\base\abci\abcAttach.c"
-"C:\_projects\abc\src\base\abci\abcBalance.c"
-"C:\_projects\abc\src\base\abci\abcCollapse.c"
-"C:\_projects\abc\src\base\abci\abcCut.c"
-"C:\_projects\abc\src\base\abci\abcDsd.c"
-"C:\_projects\abc\src\base\abci\abcFpga.c"
-"C:\_projects\abc\src\base\abci\abcFraig.c"
-"C:\_projects\abc\src\base\abci\abcFxu.c"
-"C:\_projects\abc\src\base\abci\abcMap.c"
-"C:\_projects\abc\src\base\abci\abcMiter.c"
-"C:\_projects\abc\src\base\abci\abcNtbdd.c"
-"C:\_projects\abc\src\base\abci\abcPga.c"
-"C:\_projects\abc\src\base\abci\abcPrint.c"
-"C:\_projects\abc\src\base\abci\abcReconv.c"
-"C:\_projects\abc\src\base\abci\abcRefactor.c"
-"C:\_projects\abc\src\base\abci\abcRenode.c"
-"C:\_projects\abc\src\base\abci\abcRewrite.c"
-"C:\_projects\abc\src\base\abci\abcSat.c"
-"C:\_projects\abc\src\base\abci\abcStrash.c"
-"C:\_projects\abc\src\base\abci\abcSweep.c"
-"C:\_projects\abc\src\base\abci\abcSymm.c"
-"C:\_projects\abc\src\base\abci\abcTiming.c"
-"C:\_projects\abc\src\base\abci\abcUnreach.c"
-"C:\_projects\abc\src\base\abci\abcVerify.c"
-"C:\_projects\abc\src\base\abcs\abcRetCore.c"
-"C:\_projects\abc\src\base\abcs\abcRetDelay.c"
-"C:\_projects\abc\src\base\abcs\abcRetImpl.c"
-"C:\_projects\abc\src\base\abcs\abcRetUtil.c"
-"C:\_projects\abc\src\base\abcs\abcSeq.c"
-"C:\_projects\abc\src\base\abcs\abcShare.c"
-"C:\_projects\abc\src\base\abcs\abcUtils.c"
-"C:\_projects\abc\src\base\cmd\cmd.c"
-"C:\_projects\abc\src\base\cmd\cmdAlias.c"
-"C:\_projects\abc\src\base\cmd\cmdApi.c"
-"C:\_projects\abc\src\base\cmd\cmdFlag.c"
-"C:\_projects\abc\src\base\cmd\cmdHist.c"
-"C:\_projects\abc\src\base\cmd\cmdUtils.c"
-"C:\_projects\abc\src\base\io\io.c"
-"C:\_projects\abc\src\base\io\ioRead.c"
-"C:\_projects\abc\src\base\io\ioReadBench.c"
-"C:\_projects\abc\src\base\io\ioReadBlif.c"
-"C:\_projects\abc\src\base\io\ioReadEdif.c"
-"C:\_projects\abc\src\base\io\ioReadEqn.c"
-"C:\_projects\abc\src\base\io\ioReadPla.c"
-"C:\_projects\abc\src\base\io\ioReadVerilog.c"
-"C:\_projects\abc\src\base\io\ioUtil.c"
-"C:\_projects\abc\src\base\io\ioWriteBench.c"
-"C:\_projects\abc\src\base\io\ioWriteBlif.c"
-"C:\_projects\abc\src\base\io\ioWriteCnf.c"
-"C:\_projects\abc\src\base\io\ioWriteDot.c"
-"C:\_projects\abc\src\base\io\ioWriteEqn.c"
-"C:\_projects\abc\src\base\io\ioWriteGml.c"
-"C:\_projects\abc\src\base\io\ioWritePla.c"
-"C:\_projects\abc\src\base\main\main.c"
-"C:\_projects\abc\src\base\main\mainFrame.c"
-"C:\_projects\abc\src\base\main\mainInit.c"
-"C:\_projects\abc\src\base\main\mainUtils.c"
-"C:\_projects\abc\src\bdd\cudd\cuddAddAbs.c"
-"C:\_projects\abc\src\bdd\cudd\cuddAddApply.c"
-"C:\_projects\abc\src\bdd\cudd\cuddAddFind.c"
-"C:\_projects\abc\src\bdd\cudd\cuddAddInv.c"
-"C:\_projects\abc\src\bdd\cudd\cuddAddIte.c"
-"C:\_projects\abc\src\bdd\cudd\cuddAddNeg.c"
-"C:\_projects\abc\src\bdd\cudd\cuddAddWalsh.c"
-"C:\_projects\abc\src\bdd\cudd\cuddAndAbs.c"
-"C:\_projects\abc\src\bdd\cudd\cuddAnneal.c"
-"C:\_projects\abc\src\bdd\cudd\cuddApa.c"
-"C:\_projects\abc\src\bdd\cudd\cuddAPI.c"
-"C:\_projects\abc\src\bdd\cudd\cuddApprox.c"
-"C:\_projects\abc\src\bdd\cudd\cuddBddAbs.c"
-"C:\_projects\abc\src\bdd\cudd\cuddBddCorr.c"
-"C:\_projects\abc\src\bdd\cudd\cuddBddIte.c"
-"C:\_projects\abc\src\bdd\cudd\cuddBridge.c"
-"C:\_projects\abc\src\bdd\cudd\cuddCache.c"
-"C:\_projects\abc\src\bdd\cudd\cuddCheck.c"
-"C:\_projects\abc\src\bdd\cudd\cuddClip.c"
-"C:\_projects\abc\src\bdd\cudd\cuddCof.c"
-"C:\_projects\abc\src\bdd\cudd\cuddCompose.c"
-"C:\_projects\abc\src\bdd\cudd\cuddDecomp.c"
-"C:\_projects\abc\src\bdd\cudd\cuddEssent.c"
-"C:\_projects\abc\src\bdd\cudd\cuddExact.c"
-"C:\_projects\abc\src\bdd\cudd\cuddExport.c"
-"C:\_projects\abc\src\bdd\cudd\cuddGenCof.c"
-"C:\_projects\abc\src\bdd\cudd\cuddGenetic.c"
-"C:\_projects\abc\src\bdd\cudd\cuddGroup.c"
-"C:\_projects\abc\src\bdd\cudd\cuddHarwell.c"
-"C:\_projects\abc\src\bdd\cudd\cuddInit.c"
-"C:\_projects\abc\src\bdd\cudd\cuddInteract.c"
-"C:\_projects\abc\src\bdd\cudd\cuddLCache.c"
-"C:\_projects\abc\src\bdd\cudd\cuddLevelQ.c"
-"C:\_projects\abc\src\bdd\cudd\cuddLinear.c"
-"C:\_projects\abc\src\bdd\cudd\cuddLiteral.c"
-"C:\_projects\abc\src\bdd\cudd\cuddMatMult.c"
-"C:\_projects\abc\src\bdd\cudd\cuddPriority.c"
-"C:\_projects\abc\src\bdd\cudd\cuddRead.c"
-"C:\_projects\abc\src\bdd\cudd\cuddRef.c"
-"C:\_projects\abc\src\bdd\cudd\cuddReorder.c"
-"C:\_projects\abc\src\bdd\cudd\cuddSat.c"
-"C:\_projects\abc\src\bdd\cudd\cuddSign.c"
-"C:\_projects\abc\src\bdd\cudd\cuddSolve.c"
-"C:\_projects\abc\src\bdd\cudd\cuddSplit.c"
-"C:\_projects\abc\src\bdd\cudd\cuddSubsetHB.c"
-"C:\_projects\abc\src\bdd\cudd\cuddSubsetSP.c"
-"C:\_projects\abc\src\bdd\cudd\cuddSymmetry.c"
-"C:\_projects\abc\src\bdd\cudd\cuddTable.c"
-"C:\_projects\abc\src\bdd\cudd\cuddUtil.c"
-"C:\_projects\abc\src\bdd\cudd\cuddWindow.c"
-"C:\_projects\abc\src\bdd\cudd\cuddZddCount.c"
-"C:\_projects\abc\src\bdd\cudd\cuddZddFuncs.c"
-"C:\_projects\abc\src\bdd\cudd\cuddZddGroup.c"
-"C:\_projects\abc\src\bdd\cudd\cuddZddIsop.c"
-"C:\_projects\abc\src\bdd\cudd\cuddZddLin.c"
-"C:\_projects\abc\src\bdd\cudd\cuddZddMisc.c"
-"C:\_projects\abc\src\bdd\cudd\cuddZddPort.c"
-"C:\_projects\abc\src\bdd\cudd\cuddZddReord.c"
-"C:\_projects\abc\src\bdd\cudd\cuddZddSetop.c"
-"C:\_projects\abc\src\bdd\cudd\cuddZddSymm.c"
-"C:\_projects\abc\src\bdd\cudd\cuddZddUtil.c"
-"C:\_projects\abc\src\bdd\epd\epd.c"
-"C:\_projects\abc\src\bdd\mtr\mtrBasic.c"
-"C:\_projects\abc\src\bdd\mtr\mtrGroup.c"
-"C:\_projects\abc\src\bdd\parse\parseCore.c"
-"C:\_projects\abc\src\bdd\parse\parseStack.c"
-"C:\_projects\abc\src\bdd\dsd\dsdApi.c"
-"C:\_projects\abc\src\bdd\dsd\dsdCheck.c"
-"C:\_projects\abc\src\bdd\dsd\dsdLocal.c"
-"C:\_projects\abc\src\bdd\dsd\dsdMan.c"
-"C:\_projects\abc\src\bdd\dsd\dsdProc.c"
-"C:\_projects\abc\src\bdd\dsd\dsdTree.c"
-"C:\_projects\abc\src\bdd\reo\reoApi.c"
-"C:\_projects\abc\src\bdd\reo\reoCore.c"
-"C:\_projects\abc\src\bdd\reo\reoProfile.c"
-"C:\_projects\abc\src\bdd\reo\reoSift.c"
-"C:\_projects\abc\src\bdd\reo\reoSwap.c"
-"C:\_projects\abc\src\bdd\reo\reoTest.c"
-"C:\_projects\abc\src\bdd\reo\reoTransfer.c"
-"C:\_projects\abc\src\bdd\reo\reoUnits.c"
-"C:\_projects\abc\src\sat\asat\added.c"
-"C:\_projects\abc\src\sat\asat\solver.c"
-"C:\_projects\abc\src\sat\msat\msatActivity.c"
-"C:\_projects\abc\src\sat\msat\msatClause.c"
-"C:\_projects\abc\src\sat\msat\msatClauseVec.c"
-"C:\_projects\abc\src\sat\msat\msatMem.c"
-"C:\_projects\abc\src\sat\msat\msatOrderJ.c"
-"C:\_projects\abc\src\sat\msat\msatQueue.c"
-"C:\_projects\abc\src\sat\msat\msatRead.c"
-"C:\_projects\abc\src\sat\msat\msatSolverApi.c"
-"C:\_projects\abc\src\sat\msat\msatSolverCore.c"
-"C:\_projects\abc\src\sat\msat\msatSolverIo.c"
-"C:\_projects\abc\src\sat\msat\msatSolverSearch.c"
-"C:\_projects\abc\src\sat\msat\msatSort.c"
-"C:\_projects\abc\src\sat\msat\msatVec.c"
-"C:\_projects\abc\src\sat\fraig\fraigApi.c"
-"C:\_projects\abc\src\sat\fraig\fraigCanon.c"
-"C:\_projects\abc\src\sat\fraig\fraigFanout.c"
-"C:\_projects\abc\src\sat\fraig\fraigFeed.c"
-"C:\_projects\abc\src\sat\fraig\fraigMan.c"
-"C:\_projects\abc\src\sat\fraig\fraigMem.c"
-"C:\_projects\abc\src\sat\fraig\fraigNode.c"
-"C:\_projects\abc\src\sat\fraig\fraigPrime.c"
-"C:\_projects\abc\src\sat\fraig\fraigSat.c"
-"C:\_projects\abc\src\sat\fraig\fraigTable.c"
-"C:\_projects\abc\src\sat\fraig\fraigUtil.c"
-"C:\_projects\abc\src\sat\fraig\fraigVec.c"
-"C:\_projects\abc\src\sat\csat\csat_apis.c"
-"C:\_projects\abc\src\opt\fxu\fxu.c"
-"C:\_projects\abc\src\opt\fxu\fxuCreate.c"
-"C:\_projects\abc\src\opt\fxu\fxuHeapD.c"
-"C:\_projects\abc\src\opt\fxu\fxuHeapS.c"
-"C:\_projects\abc\src\opt\fxu\fxuList.c"
-"C:\_projects\abc\src\opt\fxu\fxuMatrix.c"
-"C:\_projects\abc\src\opt\fxu\fxuPair.c"
-"C:\_projects\abc\src\opt\fxu\fxuPrint.c"
-"C:\_projects\abc\src\opt\fxu\fxuReduce.c"
-"C:\_projects\abc\src\opt\fxu\fxuSelect.c"
-"C:\_projects\abc\src\opt\fxu\fxuSingle.c"
-"C:\_projects\abc\src\opt\fxu\fxuUpdate.c"
-"C:\_projects\abc\src\opt\rwr\rwrDec.c"
-"C:\_projects\abc\src\opt\rwr\rwrEva.c"
-"C:\_projects\abc\src\opt\rwr\rwrExp.c"
-"C:\_projects\abc\src\opt\rwr\rwrLib.c"
-"C:\_projects\abc\src\opt\rwr\rwrMan.c"
-"C:\_projects\abc\src\opt\rwr\rwrPrint.c"
-"C:\_projects\abc\src\opt\rwr\rwrUtil.c"
-"C:\_projects\abc\src\opt\cut\cutApi.c"
-"C:\_projects\abc\src\opt\cut\cutCut.c"
-"C:\_projects\abc\src\opt\cut\cutMan.c"
-"C:\_projects\abc\src\opt\cut\cutMerge.c"
-"C:\_projects\abc\src\opt\cut\cutNode.c"
-"C:\_projects\abc\src\opt\cut\cutSeq.c"
-"C:\_projects\abc\src\opt\cut\cutTruth.c"
-"C:\_projects\abc\src\opt\dec\decAbc.c"
-"C:\_projects\abc\src\opt\dec\decFactor.c"
-"C:\_projects\abc\src\opt\dec\decMan.c"
-"C:\_projects\abc\src\opt\dec\decPrint.c"
-"C:\_projects\abc\src\opt\dec\decUtil.c"
-"C:\_projects\abc\src\opt\sim\simMan.c"
-"C:\_projects\abc\src\opt\sim\simSat.c"
-"C:\_projects\abc\src\opt\sim\simSupp.c"
-"C:\_projects\abc\src\opt\sim\simSwitch.c"
-"C:\_projects\abc\src\opt\sim\simSym.c"
-"C:\_projects\abc\src\opt\sim\simSymSat.c"
-"C:\_projects\abc\src\opt\sim\simSymSim.c"
-"C:\_projects\abc\src\opt\sim\simSymStr.c"
-"C:\_projects\abc\src\opt\sim\simUtils.c"
-"C:\_projects\abc\src\map\fpga\fpga.c"
-"C:\_projects\abc\src\map\fpga\fpgaCore.c"
-"C:\_projects\abc\src\map\fpga\fpgaCreate.c"
-"C:\_projects\abc\src\map\fpga\fpgaCut.c"
-"C:\_projects\abc\src\map\fpga\fpgaCutUtils.c"
-"C:\_projects\abc\src\map\fpga\fpgaFanout.c"
-"C:\_projects\abc\src\map\fpga\fpgaLib.c"
-"C:\_projects\abc\src\map\fpga\fpgaMatch.c"
-"C:\_projects\abc\src\map\fpga\fpgaSwitch.c"
-"C:\_projects\abc\src\map\fpga\fpgaTime.c"
-"C:\_projects\abc\src\map\fpga\fpgaTruth.c"
-"C:\_projects\abc\src\map\fpga\fpgaUtils.c"
-"C:\_projects\abc\src\map\fpga\fpgaVec.c"
-"C:\_projects\abc\src\map\mapper\mapper.c"
-"C:\_projects\abc\src\map\mapper\mapperCanon.c"
-"C:\_projects\abc\src\map\mapper\mapperCore.c"
-"C:\_projects\abc\src\map\mapper\mapperCreate.c"
-"C:\_projects\abc\src\map\mapper\mapperCut.c"
-"C:\_projects\abc\src\map\mapper\mapperCutUtils.c"
-"C:\_projects\abc\src\map\mapper\mapperFanout.c"
-"C:\_projects\abc\src\map\mapper\mapperLib.c"
-"C:\_projects\abc\src\map\mapper\mapperMatch.c"
-"C:\_projects\abc\src\map\mapper\mapperRefs.c"
-"C:\_projects\abc\src\map\mapper\mapperSuper.c"
-"C:\_projects\abc\src\map\mapper\mapperSwitch.c"
-"C:\_projects\abc\src\map\mapper\mapperTable.c"
-"C:\_projects\abc\src\map\mapper\mapperTime.c"
-"C:\_projects\abc\src\map\mapper\mapperTree.c"
-"C:\_projects\abc\src\map\mapper\mapperTruth.c"
-"C:\_projects\abc\src\map\mapper\mapperUtils.c"
-"C:\_projects\abc\src\map\mapper\mapperVec.c"
-"C:\_projects\abc\src\map\mio\mio.c"
-"C:\_projects\abc\src\map\mio\mioApi.c"
-"C:\_projects\abc\src\map\mio\mioFunc.c"
-"C:\_projects\abc\src\map\mio\mioRead.c"
-"C:\_projects\abc\src\map\mio\mioUtils.c"
-"C:\_projects\abc\src\map\super\super.c"
-"C:\_projects\abc\src\map\super\superAnd.c"
-"C:\_projects\abc\src\map\super\superGate.c"
-"C:\_projects\abc\src\map\super\superWrite.c"
-"C:\_projects\abc\src\map\pga\pgaCore.c"
-"C:\_projects\abc\src\map\pga\pgaMan.c"
-"C:\_projects\abc\src\map\pga\pgaMatch.c"
-"C:\_projects\abc\src\map\pga\pgaUtil.c"
-"C:\_projects\abc\src\misc\extra\extraBddMisc.c"
-"C:\_projects\abc\src\misc\extra\extraBddSymm.c"
-"C:\_projects\abc\src\misc\extra\extraUtilBitMatrix.c"
-"C:\_projects\abc\src\misc\extra\extraUtilCanon.c"
-"C:\_projects\abc\src\misc\extra\extraUtilFile.c"
-"C:\_projects\abc\src\misc\extra\extraUtilMemory.c"
-"C:\_projects\abc\src\misc\extra\extraUtilMisc.c"
-"C:\_projects\abc\src\misc\extra\extraUtilProgress.c"
-"C:\_projects\abc\src\misc\extra\extraUtilReader.c"
-"C:\_projects\abc\src\misc\st\st.c"
-"C:\_projects\abc\src\misc\st\stmm.c"
-"C:\_projects\abc\src\misc\util\cpu_stats.c"
-"C:\_projects\abc\src\misc\util\cpu_time.c"
-"C:\_projects\abc\src\misc\util\datalimit.c"
-"C:\_projects\abc\src\misc\util\getopt.c"
-"C:\_projects\abc\src\misc\util\pathsearch.c"
-"C:\_projects\abc\src\misc\util\safe_mem.c"
-"C:\_projects\abc\src\misc\util\strsav.c"
-"C:\_projects\abc\src\misc\util\texpand.c"
-"C:\_projects\abc\src\misc\mvc\mvc.c"
-"C:\_projects\abc\src\misc\mvc\mvcApi.c"
-"C:\_projects\abc\src\misc\mvc\mvcCompare.c"
-"C:\_projects\abc\src\misc\mvc\mvcContain.c"
-"C:\_projects\abc\src\misc\mvc\mvcCover.c"
-"C:\_projects\abc\src\misc\mvc\mvcCube.c"
-"C:\_projects\abc\src\misc\mvc\mvcDivide.c"
-"C:\_projects\abc\src\misc\mvc\mvcDivisor.c"
-"C:\_projects\abc\src\misc\mvc\mvcList.c"
-"C:\_projects\abc\src\misc\mvc\mvcLits.c"
-"C:\_projects\abc\src\misc\mvc\mvcMan.c"
-"C:\_projects\abc\src\misc\mvc\mvcOpAlg.c"
-"C:\_projects\abc\src\misc\mvc\mvcOpBool.c"
-"C:\_projects\abc\src\misc\mvc\mvcPrint.c"
-"C:\_projects\abc\src\misc\mvc\mvcSort.c"
-"C:\_projects\abc\src\misc\mvc\mvcUtils.c"
-"C:\_projects\abc\src\base\main\libSupport.c"
 ]
-Creating command line "cl.exe @C:\DOCUME~1\alanmi\LOCALS~1\Temp\RSP211A.tmp" 
+Creating command line "cl.exe @C:\DOCUME~1\alanmi\LOCALS~1\Temp\RSP23BD.tmp" 
-Creating temporary file "C:\DOCUME~1\alanmi\LOCALS~1\Temp\RSP211B.tmp" with contents
+Creating temporary file "C:\DOCUME~1\alanmi\LOCALS~1\Temp\RSP23BE.tmp" with contents
 [
 kernel32.lib user32.lib gdi32.lib winspool.lib comdlg32.lib advapi32.lib shell32.lib ole32.lib oleaut32.lib uuid.lib odbc32.lib odbccp32.lib kernel32.lib user32.lib gdi32.lib winspool.lib comdlg32.lib advapi32.lib shell32.lib ole32.lib oleaut32.lib uuid.lib odbc32.lib odbccp32.lib /nologo /subsystem:console /incremental:no /pdb:"Release/abc.pdb" /machine:I386 /out:"_TEST/abc.exe" 
 .\Release\abcAig.obj
@@ -384,6 +84,7 @@ kernel32.lib user32.lib gdi32.lib winspool.lib comdlg32.lib advapi32.lib shell32
 .\Release\ioWriteEqn.obj
 .\Release\ioWriteGml.obj
 .\Release\ioWritePla.obj
+.\Release\libSupport.obj
 .\Release\main.obj
 .\Release\mainFrame.obj
 .\Release\mainInit.obj
@@ -615,329 +316,13 @@ kernel32.lib user32.lib gdi32.lib winspool.lib comdlg32.lib advapi32.lib shell32
 .\Release\mvcPrint.obj
 .\Release\mvcSort.obj
 .\Release\mvcUtils.obj
-.\Release\libSupport.obj
 ]
-Creating command line "link.exe @C:\DOCUME~1\alanmi\LOCALS~1\Temp\RSP211B.tmp"
+Creating command line "link.exe @C:\DOCUME~1\alanmi\LOCALS~1\Temp\RSP23BE.tmp"
 <h3>Output Window</h3>
 Compiling...
-abcAig.c
-abcCheck.c
-abcDfs.c
-abcFanio.c
-abcFunc.c
-abcLatch.c
-abcMinBase.c
-abcNames.c
-abcNetlist.c
-abcNtk.c
-abcObj.c
-abcRefs.c
-abcShow.c
-abcSop.c
-abcUtil.c
 abc.c
-abcAttach.c
-abcBalance.c
-abcCollapse.c
-abcCut.c
-abcDsd.c
-abcFpga.c
-abcFraig.c
-abcFxu.c
-abcMap.c
-abcMiter.c
-abcNtbdd.c
-abcPga.c
-abcPrint.c
-abcReconv.c
-abcRefactor.c
-abcRenode.c
-abcRewrite.c
-abcSat.c
-abcStrash.c
-abcSweep.c
-abcSymm.c
-abcTiming.c
-abcUnreach.c
-abcVerify.c
-abcRetCore.c
-abcRetDelay.c
-abcRetImpl.c
-abcRetUtil.c
-abcSeq.c
-abcShare.c
-abcUtils.c
-cmd.c
-cmdAlias.c
-cmdApi.c
-cmdFlag.c
-cmdHist.c
-cmdUtils.c
-io.c
-ioRead.c
-ioReadBench.c
-ioReadBlif.c
-ioReadEdif.c
-ioReadEqn.c
-ioReadPla.c
-ioReadVerilog.c
-ioUtil.c
-ioWriteBench.c
-ioWriteBlif.c
-ioWriteCnf.c
-ioWriteDot.c
-ioWriteEqn.c
-ioWriteGml.c
-ioWritePla.c
-main.c
-mainFrame.c
-mainInit.c
-mainUtils.c
-cuddAddAbs.c
-cuddAddApply.c
-cuddAddFind.c
-cuddAddInv.c
-cuddAddIte.c
-cuddAddNeg.c
-cuddAddWalsh.c
-cuddAndAbs.c
-cuddAnneal.c
-cuddApa.c
-C:\_projects\abc\src\bdd\cudd\cuddApa.c(181) : warning C4244: 'return' : conversion from 'unsigned long ' to 'unsigned short ', possible loss of data
-C:\_projects\abc\src\bdd\cudd\cuddApa.c(213) : warning C4244: 'return' : conversion from 'unsigned long ' to 'unsigned short ', possible loss of data
-C:\_projects\abc\src\bdd\cudd\cuddApa.c(530) : warning C4244: '=' : conversion from 'unsigned short ' to 'unsigned char ', possible loss of data
-C:\_projects\abc\src\bdd\cudd\cuddApa.c(588) : warning C4244: '=' : conversion from 'unsigned short ' to 'unsigned char ', possible loss of data
-cuddAPI.c
-cuddApprox.c
-cuddBddAbs.c
-cuddBddCorr.c
-cuddBddIte.c
-cuddBridge.c
-cuddCache.c
-C:\_projects\abc\src\bdd\cudd\cuddCache.c(902) : warning C4146: unary minus operator applied to unsigned type, result still unsigned
-cuddCheck.c
-cuddClip.c
-cuddCof.c
-cuddCompose.c
-cuddDecomp.c
-cuddEssent.c
-cuddExact.c
-cuddExport.c
-cuddGenCof.c
-cuddGenetic.c
-cuddGroup.c
-C:\_projects\abc\src\bdd\cudd\cuddGroup.c(2062) : warning C4018: '<=' : signed/unsigned mismatch
-cuddHarwell.c
-cuddInit.c
-cuddInteract.c
-cuddLCache.c
-C:\_projects\abc\src\bdd\cudd\cuddLCache.c(1387) : warning C4146: unary minus operator applied to unsigned type, result still unsigned
-cuddLevelQ.c
-cuddLinear.c
-cuddLiteral.c
-cuddMatMult.c
-cuddPriority.c
-cuddRead.c
-cuddRef.c
-cuddReorder.c
-C:\_projects\abc\src\bdd\cudd\cuddReorder.c(395) : warning C4146: unary minus operator applied to unsigned type, result still unsigned
-cuddSat.c
-C:\_projects\abc\src\bdd\cudd\cuddReorder.c(2016) : warning C4700: local variable 'minLevel' used without having been initialized
-C:\_projects\abc\src\bdd\cudd\cuddReorder.c(2020) : warning C4700: local variable 'maxLevel' used without having been initialized
-cuddSign.c
-cuddSolve.c
-cuddSplit.c
-cuddSubsetHB.c
-cuddSubsetSP.c
-cuddSymmetry.c
-cuddTable.c
-C:\_projects\abc\src\bdd\cudd\cuddTable.c(1822) : warning C4018: '<' : signed/unsigned mismatch
-C:\_projects\abc\src\bdd\cudd\cuddTable.c(1927) : warning C4018: '<' : signed/unsigned mismatch
-C:\_projects\abc\src\bdd\cudd\cuddTable.c(2235) : warning C4018: '<' : signed/unsigned mismatch
-C:\_projects\abc\src\bdd\cudd\cuddTable.c(2303) : warning C4018: '<' : signed/unsigned mismatch
-C:\_projects\abc\src\bdd\cudd\cuddTable.c(2358) : warning C4146: unary minus operator applied to unsigned type, result still unsigned
-cuddUtil.c
-cuddWindow.c
-cuddZddCount.c
-cuddZddFuncs.c
-cuddZddGroup.c
-cuddZddIsop.c
-cuddZddLin.c
-cuddZddMisc.c
-cuddZddPort.c
-cuddZddReord.c
-cuddZddSetop.c
-cuddZddSymm.c
-cuddZddUtil.c
-epd.c
-mtrBasic.c
-mtrGroup.c
-parseCore.c
-parseStack.c
-dsdApi.c
-dsdCheck.c
-dsdLocal.c
-dsdMan.c
-dsdProc.c
-dsdTree.c
-reoApi.c
-reoCore.c
-reoProfile.c
-reoSift.c
-reoSwap.c
-reoTest.c
-reoTransfer.c
-reoUnits.c
-added.c
-solver.c
-msatActivity.c
-msatClause.c
-msatClauseVec.c
-msatMem.c
-msatOrderJ.c
-msatQueue.c
-msatRead.c
-msatSolverApi.c
-msatSolverCore.c
-msatSolverIo.c
-msatSolverSearch.c
-msatSort.c
-msatVec.c
-fraigApi.c
-fraigCanon.c
-fraigFanout.c
-fraigFeed.c
-fraigMan.c
-fraigMem.c
-fraigNode.c
-fraigPrime.c
-fraigSat.c
-fraigTable.c
-fraigUtil.c
-fraigVec.c
-csat_apis.c
-fxu.c
-fxuCreate.c
-fxuHeapD.c
-fxuHeapS.c
-fxuList.c
-fxuMatrix.c
-fxuPair.c
-fxuPrint.c
-fxuReduce.c
-fxuSelect.c
-fxuSingle.c
-fxuUpdate.c
-rwrDec.c
-rwrEva.c
-rwrExp.c
-rwrLib.c
-rwrMan.c
-rwrPrint.c
-rwrUtil.c
-cutApi.c
-cutCut.c
-cutMan.c
-cutMerge.c
-cutNode.c
-cutSeq.c
-cutTruth.c
-decAbc.c
-decFactor.c
-decMan.c
-decPrint.c
-decUtil.c
-simMan.c
-simSat.c
-simSupp.c
-simSwitch.c
-simSym.c
-simSymSat.c
-simSymSim.c
-simSymStr.c
-simUtils.c
-fpga.c
-fpgaCore.c
-fpgaCreate.c
-fpgaCut.c
-fpgaCutUtils.c
-fpgaFanout.c
-fpgaLib.c
-fpgaMatch.c
-fpgaSwitch.c
-fpgaTime.c
-fpgaTruth.c
-fpgaUtils.c
-fpgaVec.c
-mapper.c
-mapperCanon.c
-mapperCore.c
-mapperCreate.c
-mapperCut.c
-mapperCutUtils.c
-mapperFanout.c
-mapperLib.c
-mapperMatch.c
-mapperRefs.c
-mapperSuper.c
-mapperSwitch.c
-mapperTable.c
-mapperTime.c
-mapperTree.c
-mapperTruth.c
-mapperUtils.c
-mapperVec.c
-mio.c
-mioApi.c
-mioFunc.c
-mioRead.c
-mioUtils.c
-super.c
-superAnd.c
-superGate.c
-superWrite.c
-pgaCore.c
-pgaMan.c
-pgaMatch.c
-pgaUtil.c
-extraBddMisc.c
-extraBddSymm.c
-extraUtilBitMatrix.c
-extraUtilCanon.c
-extraUtilFile.c
-extraUtilMemory.c
-extraUtilMisc.c
-extraUtilProgress.c
-extraUtilReader.c
-st.c
-stmm.c
-cpu_stats.c
-cpu_time.c
-datalimit.c
-getopt.c
-pathsearch.c
-safe_mem.c
-strsav.c
-texpand.c
-mvc.c
-mvcApi.c
-mvcCompare.c
-mvcContain.c
-mvcCover.c
-mvcCube.c
-mvcDivide.c
-mvcDivisor.c
-mvcList.c
-mvcLits.c
-mvcMan.c
-mvcOpAlg.c
-mvcOpBool.c
-mvcPrint.c
-mvcSort.c
-mvcUtils.c
-libSupport.c
 Linking...
-Creating temporary file "C:\DOCUME~1\alanmi\LOCALS~1\Temp\RSP211D.tmp" with contents
+Creating temporary file "C:\DOCUME~1\alanmi\LOCALS~1\Temp\RSP23C0.tmp" with contents
 [
 /nologo /o"Release/abc.bsc" 
 .\Release\abcAig.sbr
@@ -1009,6 +394,7 @@ Creating temporary file "C:\DOCUME~1\alanmi\LOCALS~1\Temp\RSP211D.tmp" with cont
 .\Release\ioWriteEqn.sbr
 .\Release\ioWriteGml.sbr
 .\Release\ioWritePla.sbr
+.\Release\libSupport.sbr
 .\Release\main.sbr
 .\Release\mainFrame.sbr
 .\Release\mainInit.sbr
@@ -1239,16 +625,15 @@ Creating temporary file "C:\DOCUME~1\alanmi\LOCALS~1\Temp\RSP211D.tmp" with cont
 .\Release\mvcOpBool.sbr
 .\Release\mvcPrint.sbr
 .\Release\mvcSort.sbr
-.\Release\mvcUtils.sbr
+.\Release\mvcUtils.sbr]
-.\Release\libSupport.sbr]
+Creating command line "bscmake.exe @C:\DOCUME~1\alanmi\LOCALS~1\Temp\RSP23C0.tmp"
-Creating command line "bscmake.exe @C:\DOCUME~1\alanmi\LOCALS~1\Temp\RSP211D.tmp"
 Creating browse info file...
 <h3>Output Window</h3>
 
 
 
 <h3>Results</h3>
-abc.exe - 0 error(s), 15 warning(s)
+abc.exe - 0 error(s), 0 warning(s)
 </pre>
 </body>
 </html>

abc.rc

@@ -64,3 +64,5 @@ alias sharedsd "b; ren; dsd -g; sw; fx; b"
 alias resyn    "b; rw; rwz; b; rwz; b"
 alias resyn2   "b; rw; rf; b; rw; rwz; b; rfz; rwz; b"
 alias thin     "rwz; rfz; b; ps"
+alias reti     "st; seq; ret; unseq; st"
+alias retis    "st; seq; ret; unseq -s; st"

src/base/abc/abc.h

@@ -343,9 +343,11 @@ static inline bool        Abc_NodeIsTravIdCurrent( Abc_Obj_t * pNode )       { r
 static inline bool        Abc_NodeIsTravIdPrevious( Abc_Obj_t * pNode )      { return (bool)(pNode->TravId == pNode->pNtk->nTravIds - 1); }
 
 // checking initial state of the latches
+static inline void        Abc_LatchSetInitNone( Abc_Obj_t * pLatch ) { assert(Abc_ObjIsLatch(pLatch)); pLatch->pData = (void *)ABC_INIT_NONE;         }
 static inline void        Abc_LatchSetInit0( Abc_Obj_t * pLatch )    { assert(Abc_ObjIsLatch(pLatch)); pLatch->pData = (void *)ABC_INIT_ZERO;         }
 static inline void        Abc_LatchSetInit1( Abc_Obj_t * pLatch )    { assert(Abc_ObjIsLatch(pLatch)); pLatch->pData = (void *)ABC_INIT_ONE;          }
 static inline void        Abc_LatchSetInitDc( Abc_Obj_t * pLatch )   { assert(Abc_ObjIsLatch(pLatch)); pLatch->pData = (void *)ABC_INIT_DC;           }
+static inline bool        Abc_LatchIsInitNone( Abc_Obj_t * pLatch )  { assert(Abc_ObjIsLatch(pLatch)); return pLatch->pData == (void *)ABC_INIT_NONE; }
 static inline bool        Abc_LatchIsInit0( Abc_Obj_t * pLatch )     { assert(Abc_ObjIsLatch(pLatch)); return pLatch->pData == (void *)ABC_INIT_ZERO; }
 static inline bool        Abc_LatchIsInit1( Abc_Obj_t * pLatch )     { assert(Abc_ObjIsLatch(pLatch)); return pLatch->pData == (void *)ABC_INIT_ONE;  }
 static inline bool        Abc_LatchIsInitDc( Abc_Obj_t * pLatch )    { assert(Abc_ObjIsLatch(pLatch)); return pLatch->pData == (void *)ABC_INIT_DC;   }
@@ -528,6 +530,9 @@ extern void               Abc_NodeFreeNames( Vec_Ptr_t * vNames );
 extern char **            Abc_NtkCollectCioNames( Abc_Ntk_t * pNtk, int fCollectCos );
 extern int                Abc_NodeCompareNames( Abc_Obj_t ** pp1, Abc_Obj_t ** pp2 );
 extern void               Abc_NtkOrderObjsByName( Abc_Ntk_t * pNtk, int fComb );
+extern void               Abc_NtkAddDummyPiNames( Abc_Ntk_t * pNtk );
+extern void               Abc_NtkAddDummyPoNames( Abc_Ntk_t * pNtk );
+extern void               Abc_NtkAddDummyLatchNames( Abc_Ntk_t * pNtk );
 extern void               Abc_NtkShortNames( Abc_Ntk_t * pNtk );
 /*=== abcNetlist.c ==========================================================*/
 extern Abc_Ntk_t *        Abc_NtkNetlistToLogic( Abc_Ntk_t * pNtk );

src/base/abc/abcLatch.c

@@ -93,6 +93,50 @@ int Abc_NtkCountSelfFeedLatches( Abc_Ntk_t * pNtk )
     return Counter;
 }
 
+/**Function*************************************************************
+
+  Synopsis    [Pipelines the network with latches.]
+
+  Description []
+               
+  SideEffects [Does not check the names of the added latches!!!]
+
+  SeeAlso     []
+
+***********************************************************************/
+void Abc_NtkLatchPipe( Abc_Ntk_t * pNtk, int nLatches )
+{
+    Vec_Ptr_t * vNodes;
+    Abc_Obj_t * pObj, * pLatch, * pFanin, * pFanout;
+    int i, k, nTotal, nDigits;
+    if ( nLatches < 1 )
+        return;
+    nTotal = nLatches * Abc_NtkPiNum(pNtk);
+    nDigits = Extra_Base10Log( nTotal );
+    vNodes = Vec_PtrAlloc( 100 );
+    Abc_NtkForEachPi( pNtk, pObj, i )
+    {
+        // remember current fanins of the PI
+        Abc_NodeCollectFanouts( pObj, vNodes );
+        // create the latches
+        for ( pFanin = pObj, k = 0; k < nLatches; k++, pFanin = pLatch )
+        {
+            pLatch = Abc_NtkCreateLatch( pNtk );
+            Abc_ObjAddFanin( pLatch, pFanin );
+            Abc_LatchSetInitDc( pLatch );
+            // add the latch to the CI/CO lists
+            Vec_PtrPush( pNtk->vCis, pLatch );
+            Vec_PtrPush( pNtk->vCos, pLatch );
+            // create the name of the new latch
+            Abc_NtkLogicStoreName( pLatch, Abc_ObjNameDummy("LL", i*nLatches + k, nDigits) );
+        }
+        // patch the PI fanouts
+        Vec_PtrForEachEntry( vNodes, pFanout, k )
+            Abc_ObjPatchFanin( pFanout, pObj, pFanin );
+    }
+    Vec_PtrFree( vNodes );
+    Abc_NtkLogicMakeSimpleCos( pNtk, 0 );
+}
 
 
 ////////////////////////////////////////////////////////////////////////

src/base/abc/abcNames.c

@@ -469,7 +469,67 @@ void Abc_NtkOrderObjsByName( Abc_Ntk_t * pNtk, int fComb )
 
 /**Function*************************************************************
 
-  Synopsis    []
+  Synopsis    [Adds dummy names.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Abc_NtkAddDummyPiNames( Abc_Ntk_t * pNtk )
+{
+    Abc_Obj_t * pObj;
+    int nDigits, i;
+    nDigits = Extra_Base10Log( Abc_NtkPiNum(pNtk) );
+    Abc_NtkForEachPi( pNtk, pObj, i )
+        Abc_NtkLogicStoreName( pObj, Abc_ObjNameDummy("pi", i, nDigits) );
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Adds dummy names.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Abc_NtkAddDummyPoNames( Abc_Ntk_t * pNtk )
+{
+    Abc_Obj_t * pObj;
+    int nDigits, i;
+    nDigits = Extra_Base10Log( Abc_NtkPoNum(pNtk) );
+    Abc_NtkForEachPo( pNtk, pObj, i )
+        Abc_NtkLogicStoreName( pObj, Abc_ObjNameDummy("po", i, nDigits) );
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Adds dummy names.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Abc_NtkAddDummyLatchNames( Abc_Ntk_t * pNtk )
+{
+    Abc_Obj_t * pObj;
+    int nDigits, i;
+    nDigits = Extra_Base10Log( Abc_NtkLatchNum(pNtk) );
+    Abc_NtkForEachLatch( pNtk, pObj, i )
+        Abc_NtkLogicStoreName( pObj, Abc_ObjNameDummy("L", i, nDigits) );
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Replaces names by short names.]
 
   Description []
                
@@ -480,39 +540,11 @@ void Abc_NtkOrderObjsByName( Abc_Ntk_t * pNtk, int fComb )
 ***********************************************************************/
 void Abc_NtkShortNames( Abc_Ntk_t * pNtk )
 {
-    stmm_table * tObj2NameNew;
-    Abc_Obj_t * pObj;
-    char Buffer[100];
-    char * pNameNew;
-    int Length, i;
-
-    tObj2NameNew = stmm_init_table(stmm_ptrcmp, stmm_ptrhash);
-    // create new names and add them to the table
-    Length = Extra_Base10Log( Abc_NtkPiNum(pNtk) );
-    Abc_NtkForEachPi( pNtk, pObj, i )
-    {
-        sprintf( Buffer, "pi%0*d", Length, i );
-        pNameNew = Abc_NtkRegisterName( pNtk, Buffer );
-        stmm_insert( tObj2NameNew, (char *)pObj, pNameNew );
-    }
-    // create new names and add them to the table
-    Length = Extra_Base10Log( Abc_NtkPoNum(pNtk) );
-    Abc_NtkForEachPo( pNtk, pObj, i )
-    {
-        sprintf( Buffer, "po%0*d", Length, i );
-        pNameNew = Abc_NtkRegisterName( pNtk, Buffer );
-        stmm_insert( tObj2NameNew, (char *)pObj, pNameNew );
-    }
-    // create new names and add them to the table
-    Length = Extra_Base10Log( Abc_NtkLatchNum(pNtk) );
-    Abc_NtkForEachLatch( pNtk, pObj, i )
-    {
-        sprintf( Buffer, "lat%0*d", Length, i );
-        pNameNew = Abc_NtkRegisterName( pNtk, Buffer );
-        stmm_insert( tObj2NameNew, (char *)pObj, pNameNew );
-    }
     stmm_free_table( pNtk->tObj2Name );
-    pNtk->tObj2Name = tObj2NameNew;
+    pNtk->tObj2Name = stmm_init_table(stmm_ptrcmp, stmm_ptrhash);
+    Abc_NtkAddDummyPiNames( pNtk );
+    Abc_NtkAddDummyPoNames( pNtk );
+    Abc_NtkAddDummyLatchNames( pNtk );
 }
 
 ////////////////////////////////////////////////////////////////////////

src/base/abc/abcUtil.c

@@ -771,7 +771,7 @@ void Abc_NodeCollectFanins( Abc_Obj_t * pNode, Vec_Ptr_t * vNodes )
 {
     Abc_Obj_t * pFanin;
     int i;
-    vNodes->nSize = 0;
+    Vec_PtrClear(vNodes);
     Abc_ObjForEachFanin( pNode, pFanin, i )
         Vec_PtrPush( vNodes, pFanin );
 }
@@ -791,7 +791,7 @@ void Abc_NodeCollectFanouts( Abc_Obj_t * pNode, Vec_Ptr_t * vNodes )
 {
     Abc_Obj_t * pFanout;
     int i;
-    vNodes->nSize = 0;
+    Vec_PtrClear(vNodes);
     Abc_ObjForEachFanout( pNode, pFanout, i )
         Vec_PtrPush( vNodes, pFanout );
 }

src/base/abci/abc.c

@@ -85,6 +85,9 @@ static int Abc_CommandSuperChoice  ( Abc_Frame_t * pAbc, int argc, char ** argv
 static int Abc_CommandFpga         ( Abc_Frame_t * pAbc, int argc, char ** argv );
 static int Abc_CommandPga          ( Abc_Frame_t * pAbc, int argc, char ** argv );
 
+static int Abc_CommandScut         ( Abc_Frame_t * pAbc, int argc, char ** argv );
+static int Abc_CommandInit         ( Abc_Frame_t * pAbc, int argc, char ** argv );
+static int Abc_CommandPipe         ( Abc_Frame_t * pAbc, int argc, char ** argv );
 static int Abc_CommandSeq          ( Abc_Frame_t * pAbc, int argc, char ** argv );
 static int Abc_CommandUnseq        ( Abc_Frame_t * pAbc, int argc, char ** argv );
 static int Abc_CommandRetime       ( Abc_Frame_t * pAbc, int argc, char ** argv );
@@ -163,6 +166,9 @@ void Abc_Init( Abc_Frame_t * pAbc )
     Cmd_CommandAdd( pAbc, "FPGA mapping", "fpga",          Abc_CommandFpga,             1 );
     Cmd_CommandAdd( pAbc, "FPGA mapping", "pga",           Abc_CommandPga,              1 );
 
+    Cmd_CommandAdd( pAbc, "Sequential",   "scut",          Abc_CommandScut,             0 );
+    Cmd_CommandAdd( pAbc, "Sequential",   "init",          Abc_CommandInit,             1 );
+    Cmd_CommandAdd( pAbc, "Sequential",   "pipe",          Abc_CommandPipe,             1 );
     Cmd_CommandAdd( pAbc, "Sequential",   "seq",           Abc_CommandSeq,              1 );
     Cmd_CommandAdd( pAbc, "Sequential",   "unseq",         Abc_CommandUnseq,            1 );
     Cmd_CommandAdd( pAbc, "Sequential",   "retime",        Abc_CommandRetime,           1 );
@@ -2725,15 +2731,15 @@ int Abc_CommandCut( Abc_Frame_t * pAbc, int argc, char ** argv )
     pErr = Abc_FrameReadErr(pAbc);
 
     // set defaults
+    memset( pParams, 0, sizeof(Cut_Params_t) );
     pParams->nVarsMax  = 5;     // the max cut size ("k" of the k-feasible cuts)
     pParams->nKeepMax  = 250;   // the max number of cuts kept at a node
     pParams->fTruth    = 0;     // compute truth tables
     pParams->fFilter   = 1;     // filter dominated cuts
-    pParams->fSeq      = 0;     // compute sequential cuts
     pParams->fDrop     = 0;     // drop cuts on the fly
     pParams->fVerbose  = 0;     // the verbosiness flag
     util_getopt_reset();
-    while ( ( c = util_getopt( argc, argv, "KMtfsdvh" ) ) != EOF )
+    while ( ( c = util_getopt( argc, argv, "KMtfdvh" ) ) != EOF )
     {
         switch ( c )
         {
@@ -2765,9 +2771,6 @@ int Abc_CommandCut( Abc_Frame_t * pAbc, int argc, char ** argv )
         case 'f':
             pParams->fFilter ^= 1;
             break;
-        case 's':
-            pParams->fSeq ^= 1;
-            break;
         case 'd':
             pParams->fDrop ^= 1;
             break;
@@ -2797,19 +2800,116 @@ int Abc_CommandCut( Abc_Frame_t * pAbc, int argc, char ** argv )
     return 0;
 
 usage:
-    fprintf( pErr, "usage: cut [-K num] [-M num] [-tfsdvh]\n" );
+    fprintf( pErr, "usage: cut [-K num] [-M num] [-tfdvh]\n" );
     fprintf( pErr, "\t         computes k-feasible cuts for the AIG\n" );
     fprintf( pErr, "\t-K num : max number of leaves (4 <= num <= 6) [default = %d]\n",     pParams->nVarsMax );
     fprintf( pErr, "\t-M num : max number of cuts stored at a node [default = %d]\n",      pParams->nKeepMax );
     fprintf( pErr, "\t-t     : toggle truth table computation [default = %s]\n",           pParams->fTruth? "yes": "no" );
     fprintf( pErr, "\t-f     : toggle filtering of duplicated/dominated [default = %s]\n", pParams->fFilter? "yes": "no" );
-    fprintf( pErr, "\t-s     : toggle sequential cut computation [default = %s]\n",        pParams->fSeq? "yes": "no" );
     fprintf( pErr, "\t-d     : toggle dropping when fanouts are done [default = %s]\n",    pParams->fDrop? "yes": "no" );
     fprintf( pErr, "\t-v     : toggle printing verbose information [default = %s]\n",      pParams->fVerbose? "yes": "no" );
     fprintf( pErr, "\t-h     : print the command usage\n");
     return 1;
 }
 
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Abc_CommandScut( Abc_Frame_t * pAbc, int argc, char ** argv )
+{
+    Cut_Params_t Params, * pParams = &Params;
+    Cut_Man_t * pCutMan;
+    FILE * pOut, * pErr;
+    Abc_Ntk_t * pNtk;
+    int c;
+    extern Cut_Man_t * Abc_NtkSeqCuts( Abc_Ntk_t * pNtk, Cut_Params_t * pParams );
+
+    pNtk = Abc_FrameReadNet(pAbc);
+    pOut = Abc_FrameReadOut(pAbc);
+    pErr = Abc_FrameReadErr(pAbc);
+
+    // set defaults
+    memset( pParams, 0, sizeof(Cut_Params_t) );
+    pParams->nVarsMax  = 5;     // the max cut size ("k" of the k-feasible cuts)
+    pParams->nKeepMax  = 250;   // the max number of cuts kept at a node
+    pParams->fTruth    = 0;     // compute truth tables
+    pParams->fFilter   = 0;     // filter dominated cuts
+    pParams->fSeq      = 1;     // compute sequential cuts
+    pParams->fVerbose  = 0;     // the verbosiness flag
+    util_getopt_reset();
+    while ( ( c = util_getopt( argc, argv, "KMtvh" ) ) != EOF )
+    {
+        switch ( c )
+        {
+        case 'K':
+            if ( util_optind >= argc )
+            {
+                fprintf( pErr, "Command line switch \"-K\" should be followed by an integer.\n" );
+                goto usage;
+            }
+            pParams->nVarsMax = atoi(argv[util_optind]);
+            util_optind++;
+            if ( pParams->nVarsMax < 0 ) 
+                goto usage;
+            break;
+        case 'M':
+            if ( util_optind >= argc )
+            {
+                fprintf( pErr, "Command line switch \"-M\" should be followed by an integer.\n" );
+                goto usage;
+            }
+            pParams->nKeepMax = atoi(argv[util_optind]);
+            util_optind++;
+            if ( pParams->nKeepMax < 0 ) 
+                goto usage;
+            break;
+        case 't':
+            pParams->fTruth ^= 1;
+            break;
+        case 'v':
+            pParams->fVerbose ^= 1;
+            break;
+        case 'h':
+            goto usage;
+        default:
+            goto usage;
+        }
+    }
+
+    if ( pNtk == NULL )
+    {
+        fprintf( pErr, "Empty network.\n" );
+        return 1;
+    }
+    if ( !Abc_NtkIsSeq(pNtk) )
+    {
+        fprintf( pErr, "Sequential cuts can be computed for sequential AIGs (run \"seq\").\n" );
+        return 1;
+    }
+    pCutMan = Abc_NtkSeqCuts( pNtk, pParams );
+    Cut_ManPrintStats( pCutMan );
+    Cut_ManStop( pCutMan );
+    return 0;
+
+usage:
+    fprintf( pErr, "usage: scut [-K num] [-M num] [-tvh]\n" );
+    fprintf( pErr, "\t         computes k-feasible cuts for the sequential AIG\n" );
+    fprintf( pErr, "\t-K num : max number of leaves (4 <= num <= 6) [default = %d]\n",     pParams->nVarsMax );
+    fprintf( pErr, "\t-M num : max number of cuts stored at a node [default = %d]\n",      pParams->nKeepMax );
+    fprintf( pErr, "\t-t     : toggle truth table computation [default = %s]\n",           pParams->fTruth? "yes": "no" );
+    fprintf( pErr, "\t-v     : toggle printing verbose information [default = %s]\n",      pParams->fVerbose? "yes": "no" );
+    fprintf( pErr, "\t-h     : print the command usage\n");
+    return 1;
+}
+
 /**Function*************************************************************
 
   Synopsis    []
@@ -3892,6 +3992,195 @@ usage:
 
 
 
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Abc_CommandInit( Abc_Frame_t * pAbc, int argc, char ** argv )
+{
+    FILE * pOut, * pErr;
+    Abc_Ntk_t * pNtk;
+    Abc_Obj_t * pObj;
+    int c, i;
+    int fZeros;
+    int fOnes;
+    int fRandom;
+    int fDontCare;
+
+    pNtk = Abc_FrameReadNet(pAbc);
+    pOut = Abc_FrameReadOut(pAbc);
+    pErr = Abc_FrameReadErr(pAbc);
+
+    // set defaults
+    fZeros    = 0;
+    fOnes     = 0;
+    fRandom   = 0;
+    fDontCare = 0;
+    util_getopt_reset();
+    while ( ( c = util_getopt( argc, argv, "zordh" ) ) != EOF )
+    {
+        switch ( c )
+        {
+        case 'z':
+            fZeros ^= 1;
+            break;
+        case 'o':
+            fOnes ^= 1;
+            break;
+        case 'r':
+            fRandom ^= 1;
+            break;
+        case 'd':
+            fDontCare ^= 1;
+            break;
+        case 'h':
+            goto usage;
+        default:
+            goto usage;
+        }
+    }
+
+    if ( pNtk == NULL )
+    {
+        fprintf( pErr, "Empty network.\n" );
+        return 1;
+    }
+
+    if ( Abc_NtkIsSeq(pNtk) )
+    {
+        fprintf( pErr, "Does not work for a sequentail AIG (run \"unseq\").\n" );
+        return 1;
+    }
+
+    if ( Abc_NtkIsComb(pNtk) )
+    {
+        fprintf( pErr, "The current network is combinational.\n" );
+        return 1;
+    }
+
+    if ( fZeros )
+    {
+        Abc_NtkForEachLatch( pNtk, pObj, i )
+            Abc_LatchSetInit0( pObj );
+    }
+    else if ( fOnes )
+    {
+        Abc_NtkForEachLatch( pNtk, pObj, i )
+            Abc_LatchSetInit1( pObj );
+    }
+    else if ( fRandom )
+    {
+        Abc_NtkForEachLatch( pNtk, pObj, i )
+            if ( rand() & 1 )
+                Abc_LatchSetInit1( pObj );
+            else
+                Abc_LatchSetInit0( pObj );
+    }
+    else if ( fDontCare )
+    {
+        Abc_NtkForEachLatch( pNtk, pObj, i )
+            Abc_LatchSetInitDc( pObj );
+    }
+    else
+        printf( "The initial states remain unchanged.\n" );
+    return 0;
+
+usage:
+    fprintf( pErr, "usage: init [-zordh]\n" );
+    fprintf( pErr, "\t        resets initial states of all latches\n" );
+    fprintf( pErr, "\t-z    : set zeros initial states [default = %s]\n", fZeros? "yes": "no" );
+    fprintf( pErr, "\t-o    : set ones initial states [default = %s]\n", fOnes? "yes": "no" );
+    fprintf( pErr, "\t-d    : set don't-care initial states [default = %s]\n", fDontCare? "yes": "no" );
+    fprintf( pErr, "\t-r    : set random initial states [default = %s]\n", fRandom? "yes": "no" );
+    fprintf( pErr, "\t-h    : print the command usage\n");
+    return 1;
+}
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Abc_CommandPipe( Abc_Frame_t * pAbc, int argc, char ** argv )
+{
+    FILE * pOut, * pErr;
+    Abc_Ntk_t * pNtk;
+    int c;
+    int nLatches;
+    extern void Abc_NtkLatchPipe( Abc_Ntk_t * pNtk, int nLatches );
+
+    pNtk = Abc_FrameReadNet(pAbc);
+    pOut = Abc_FrameReadOut(pAbc);
+    pErr = Abc_FrameReadErr(pAbc);
+
+    // set defaults
+    nLatches = 5;
+    util_getopt_reset();
+    while ( ( c = util_getopt( argc, argv, "Lh" ) ) != EOF )
+    {
+        switch ( c )
+        {
+        case 'L':
+            if ( util_optind >= argc )
+            {
+                fprintf( pErr, "Command line switch \"-L\" should be followed by a positive integer.\n" );
+                goto usage;
+            }
+            nLatches = atoi(argv[util_optind]);
+            util_optind++;
+            if ( nLatches < 0 ) 
+                goto usage;
+            break;
+        case 'h':
+            goto usage;
+        default:
+            goto usage;
+        }
+    }
+
+    if ( pNtk == NULL )
+    {
+        fprintf( pErr, "Empty network.\n" );
+        return 1;
+    }
+
+    if ( Abc_NtkIsSeq(pNtk) )
+    {
+        fprintf( pErr, "Does not work for a sequentail AIG (run \"unseq\").\n" );
+        return 1;
+    }
+
+    if ( Abc_NtkIsComb(pNtk) )
+    {
+        fprintf( pErr, "The current network is combinational.\n" );
+        return 1;
+    }
+
+    // update the network
+    Abc_NtkLatchPipe( pNtk, nLatches );
+    return 0;
+
+usage:
+    fprintf( pErr, "usage: pipe [-L num] [-h]\n" );
+    fprintf( pErr, "\t         inserts the given number of latches at the PIs\n" );
+    fprintf( pErr, "\t-L num : the number of latches to insert [default = %d]\n", nLatches );
+    fprintf( pErr, "\t-h     : print the command usage\n");
+    return 1;
+}
+
 /**Function*************************************************************
 
   Synopsis    []
@@ -4066,7 +4355,7 @@ int Abc_CommandRetime( Abc_Frame_t * pAbc, int argc, char ** argv )
     pErr = Abc_FrameReadErr(pAbc);
 
     // set defaults
-    fForward  = 1;
+    fForward  = 0;
     fBackward = 0;
     fInitial  = 0;
     util_getopt_reset();
@@ -4098,7 +4387,7 @@ int Abc_CommandRetime( Abc_Frame_t * pAbc, int argc, char ** argv )
 
     if ( !Abc_NtkIsSeq(pNtk) )
     {
-        fprintf( pErr, "Works only for sequential AIG.\n" );
+        fprintf( pErr, "Works only for sequential AIG (run \"seq\").\n" );
         return 1;
     }
 
@@ -4114,11 +4403,11 @@ int Abc_CommandRetime( Abc_Frame_t * pAbc, int argc, char ** argv )
     return 0;
 
 usage:
-    fprintf( pErr, "usage: retime [-fbih]\n" );
+    fprintf( pErr, "usage: retime [-fbh]\n" );
     fprintf( pErr, "\t        retimes sequential AIG (default is Pan's delay-optimal retiming)\n" );
     fprintf( pErr, "\t-f    : toggle forward retiming [default = %s]\n", fForward? "yes": "no" );
     fprintf( pErr, "\t-b    : toggle backward retiming [default = %s]\n", fBackward? "yes": "no" );
-    fprintf( pErr, "\t-i    : toggle retiming for initial state [default = %s]\n", fInitial? "yes": "no" );
+//    fprintf( pErr, "\t-i    : toggle retiming for initial state [default = %s]\n", fInitial? "yes": "no" );
     fprintf( pErr, "\t-h    : print the command usage\n");
     return 1;
 }

src/base/abci/abcCut.c

@@ -43,7 +43,7 @@
 Cut_Man_t * Abc_NtkCuts( Abc_Ntk_t * pNtk, Cut_Params_t * pParams )
 {
     Cut_Man_t *  p;
-    Abc_Obj_t * pObj, * pDriver, * pNode;
+    Abc_Obj_t * pObj, * pNode;
     Vec_Ptr_t * vNodes;
     Vec_Int_t * vChoices;
     int i;
@@ -86,30 +86,26 @@ Cut_Man_t * Abc_NtkCuts( Abc_Ntk_t * pNtk, Cut_Params_t * pParams )
             Cut_NodeUnionCuts( p, vChoices );
         }
     }
-    if ( !pParams->fSeq )
-    {
     Vec_PtrFree( vNodes );
     Vec_IntFree( vChoices );
 PRT( "Total", clock() - clk );
     return p;
 }
-    assert( 0 );
 
-    // compute sequential cuts
+/**Function*************************************************************
-    Abc_NtkIncrementTravId( pNtk );
+
-    Abc_NtkForEachLatch( pNtk, pObj, i )
+  Synopsis    [Computes the cuts for the network.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Cut_Man_t * Abc_NtkSeqCuts( Abc_Ntk_t * pNtk, Cut_Params_t * pParams )
 {
-        pDriver = Abc_ObjFanin0(pObj);
+    return NULL;
-        if ( !Abc_ObjIsNode(pDriver) )
-            continue;
-        if ( Abc_NodeIsTravIdCurrent(pDriver) )
-            continue;
-        Abc_NodeSetTravIdCurrent(pDriver);
-    }
-    // compute as long as new cuts appear
-
-
-    return p;
 }
 
 /**Function*************************************************************

src/base/abci/abcMiter.c

@@ -491,7 +491,7 @@ Abc_Ntk_t * Abc_NtkFrames( Abc_Ntk_t * pNtk, int nFrames, int fInitial )
         Counter = 0;
         Abc_NtkForEachLatch( pNtk, pLatch, i )
         {
-            if ( Abc_LatchIsInitDc(pLatch) ) // don't-care initial value - create a new PI
+            if ( Abc_LatchIsInitNone(pLatch) || Abc_LatchIsInitDc(pLatch) ) // don't-care initial value - create a new PI
             {
                 pLatch->pCopy = Abc_NtkCreatePi(pNtkFrames);
                 Abc_NtkLogicStoreName( pLatch->pCopy, Abc_ObjName(pLatch) );

src/base/abci/abcPrint.c

@@ -145,7 +145,17 @@ void Abc_NtkPrintLatch( FILE * pFile, Abc_Ntk_t * pNtk )
 {
     Abc_Obj_t * pLatch, * pFanin;
     int i, Counter0, Counter1, Counter2;
-    int Init0, Init1, Init2;
+    int InitNums[4], Init;
+
+    assert( !Abc_NtkIsNetlist(pNtk) );
+    if ( Abc_NtkIsSeq(pNtk) )
+    {
+        Abc_NtkSeqLatchGetInitNums( pNtk, InitNums );
+        fprintf( pFile, "%-15s:  ", pNtk->pName );
+        fprintf( pFile, "Latch = %6d. No = %4d. Zero = %4d. One = %4d. DC = %4d.\n", 
+            Abc_NtkLatchNum(pNtk), InitNums[0], InitNums[1], InitNums[2], InitNums[3] );
+        return;
+    }
 
     if ( Abc_NtkLatchNum(pNtk) == 0 )
     {
@@ -153,21 +163,14 @@ void Abc_NtkPrintLatch( FILE * pFile, Abc_Ntk_t * pNtk )
         return;
     }
 
-    assert( !Abc_NtkIsNetlist(pNtk) );
+    for ( i = 0; i < 4; i++ )    
-
+        InitNums[i] = 0;
-    Init0 = Init1 = Init2 = 0;
     Counter0 = Counter1 = Counter2 = 0;
-
     Abc_NtkForEachLatch( pNtk, pLatch, i )
     {
-        if ( Abc_LatchIsInit0(pLatch) )
+        Init = Abc_LatchInit( pLatch );
-            Init0++;
+        assert( Init < 4 );
-        else if ( Abc_LatchIsInit1(pLatch) )
+        InitNums[Init]++;
-            Init1++;
-        else if ( Abc_LatchIsInitDc(pLatch) )
-            Init2++;
-        else
-            assert( 0 );
 
         pFanin = Abc_ObjFanin0(pLatch);
         if ( !Abc_ObjIsNode(pFanin) || !Abc_NodeIsConst(pFanin) )
@@ -192,14 +195,11 @@ void Abc_NtkPrintLatch( FILE * pFile, Abc_Ntk_t * pNtk )
                 Counter2++;
         }
     }
-//    fprintf( pFile, "%-15s: ", pNtk->pName );
-//    fprintf( pFile, "L = %5d: 0 = %4d. 1 = %3d. DC = %4d. ", Abc_NtkLatchNum(pNtk), Init0, Init1, Init2 );
-//    fprintf( pFile, "Con = %3d. DC = %3d. Mat = %3d. ", Counter0, Counter1, Counter2 );
-//    fprintf( pFile, "SFeed = %2d.\n", Abc_NtkCountSelfFeedLatches(pNtk) );
     fprintf( pFile, "%-15s:  ", pNtk->pName );
-    fprintf( pFile, "Lat = %5d: 0 = %4d. 1 = %3d. DC = %4d. \n", Abc_NtkLatchNum(pNtk), Init0, Init1, Init2 );
+    fprintf( pFile, "Latch = %6d. No = %4d. Zero = %4d. One = %4d. DC = %4d.\n", 
-    fprintf( pFile, "Con = %3d. DC = %3d. Mat = %3d. ", Counter0, Counter1, Counter2 );
+        Abc_NtkLatchNum(pNtk), InitNums[0], InitNums[1], InitNums[2], InitNums[3] );
-    fprintf( pFile, "SFeed = %2d.\n", Abc_NtkCountSelfFeedLatches(pNtk) );
+    fprintf( pFile, "Const fanin = %3d. DC init = %3d. Matching init = %3d. ", Counter0, Counter1, Counter2 );
+    fprintf( pFile, "Self-feed latches = %2d.\n", Abc_NtkCountSelfFeedLatches(pNtk) );
 }
 
 /**Function*************************************************************

src/base/abcs/abcRetDelay.c

@@ -27,6 +27,8 @@
 // storing arrival times in the nodes
 static inline int  Abc_NodeReadLValue( Abc_Obj_t * pNode )            { return Vec_IntEntry( (pNode)->pNtk->pData, (pNode)->Id );           }
 static inline void Abc_NodeSetLValue( Abc_Obj_t * pNode, int Value )  { Vec_IntWriteEntry( (pNode)->pNtk->pData, (pNode)->Id, (Value) );    }
+//static inline int  Abc_NodeGetLag( int LValue, int Fi )               { return LValue/Fi - (int)(LValue % Fi == 0); }
+static inline int  Abc_NodeGetLag( int LValue, int Fi )               { return (LValue + 256*Fi)/Fi - 256 - (int)(LValue % Fi == 0); }
 
 // the internal procedures
 static int Abc_NtkRetimeSearch_rec( Abc_Ntk_t * pNtk, int FiMin, int FiMax );
@@ -36,6 +38,8 @@ static int Abc_NodeUpdateLValue( Abc_Obj_t * pObj, int Fi );
 // node status after updating its arrival time
 enum { ABC_UPDATE_FAIL, ABC_UPDATE_NO, ABC_UPDATE_YES };
 
+static void Abc_RetimingExperiment( Abc_Ntk_t * pNtk, Vec_Str_t * vLags );
+
 ////////////////////////////////////////////////////////////////////////
 ///                     FUNCTION DEFITIONS                           ///
 ////////////////////////////////////////////////////////////////////////
@@ -59,11 +63,16 @@ Vec_Str_t * Abc_NtkSeqRetimeDelayLags( Abc_Ntk_t * pNtk )
     assert( Abc_NtkIsSeq( pNtk ) );
 
     // start storage for sequential arrival times
-    assert( pNtk->pData == NULL );
+//    assert( pNtk->pData == NULL );
     pNtk->pData = Vec_IntAlloc( 0 );
 
-    // get the maximum possible clock
+    // get the upper bound on the clock period
-    FiMax = Abc_NtkNodeNum(pNtk);
+//    FiMax = Abc_NtkNodeNum(pNtk);
+    FiMax = 0;
+    Abc_AigForEachAnd( pNtk, pNode, i )
+        if ( FiMax < (int)pNode->Level )
+            FiMax = pNode->Level;
+    FiMax += 2;
 
     // make sure this clock period is feasible
     assert( Abc_NtkRetimeForPeriod( pNtk, FiMax ) );
@@ -76,7 +85,23 @@ Vec_Str_t * Abc_NtkSeqRetimeDelayLags( Abc_Ntk_t * pNtk )
     // convert to lags
     vLags = Vec_StrStart( Abc_NtkObjNumMax(pNtk) );
     Abc_AigForEachAnd( pNtk, pNode, i )
-        Vec_StrWriteEntry( vLags, i, (char)(Abc_NodeReadLValue(pNode) / FiBest) );
+        Vec_StrWriteEntry( vLags, i, (char)Abc_NodeGetLag(Abc_NodeReadLValue(pNode), FiBest) );
+/*
+    printf( "LValues : " );
+    Abc_AigForEachAnd( pNtk, pNode, i )
+        printf( "%d=%d ", i, Abc_NodeReadLValue(pNode) );
+    printf( "\n" );
+*/
+
+/*
+    printf( "Lags : " );
+    Abc_AigForEachAnd( pNtk, pNode, i )
+        if ( Vec_StrEntry(vLags,i) != 0 )
+            printf( "%d=%d(%d)(%d) ", i, Vec_StrEntry(vLags,i), Abc_NodeReadLValue(pNode), Abc_NodeReadLValue(pNode) - FiBest * Vec_StrEntry(vLags,i) );
+    printf( "\n" );
+*/
+
+//    Abc_RetimingExperiment( pNtk, vLags );
 
     // free storage
     Vec_IntFree( pNtk->pData );
@@ -98,13 +123,10 @@ Vec_Str_t * Abc_NtkSeqRetimeDelayLags( Abc_Ntk_t * pNtk )
 int Abc_NtkRetimeSearch_rec( Abc_Ntk_t * pNtk, int FiMin, int FiMax )
 {
     int Median;
-
     assert( FiMin < FiMax );
     if ( FiMin + 1 == FiMax )
         return FiMax;
-
     Median = FiMin + (FiMax - FiMin)/2;
-
     if ( Abc_NtkRetimeForPeriod( pNtk, Median ) )
         return Abc_NtkRetimeSearch_rec( pNtk, FiMin, Median ); // Median is feasible
     else 
@@ -122,17 +144,30 @@ int Abc_NtkRetimeSearch_rec( Abc_Ntk_t * pNtk, int FiMin, int FiMax )
   SeeAlso     []
 
 ***********************************************************************/
-int Abc_NtkRetimeForPeriod( Abc_Ntk_t * pNtk, int Fi )
+int Abc_NtkRetimeForPeriod2( Abc_Ntk_t * pNtk, int Fi )
 {
     Vec_Ptr_t * vFrontier;
     Abc_Obj_t * pObj, * pFanout;
+    char * pReason = "";
     int RetValue, i, k;
+    int Limit;
 
     // set l-values of all nodes to be minus infinity
     Vec_IntFill( pNtk->pData, Abc_NtkObjNumMax(pNtk), -ABC_INFINITY );
 
-    // start the frontier by including PI fanouts
+    // start the frontier by setting PI l-values to 0 and including PI fanouts
     vFrontier = Vec_PtrAlloc( 100 );
+    pObj = Abc_NtkObj( pNtk, 0 );
+    if ( Abc_ObjFanoutNum(pObj) > 0 )
+    {
+        Abc_NodeSetLValue( pObj, 0 );
+        Abc_ObjForEachFanout( pObj, pFanout, k )
+            if ( pFanout->fMarkA == 0 )
+            {   
+                Vec_PtrPush( vFrontier, pFanout );
+                pFanout->fMarkA = 1;
+            }
+    }
     Abc_NtkForEachPi( pNtk, pObj, i )
     {
         Abc_NodeSetLValue( pObj, 0 );
@@ -145,19 +180,25 @@ int Abc_NtkRetimeForPeriod( Abc_Ntk_t * pNtk, int Fi )
     }
 
     // iterate until convergence
+    Limit = Abc_NtkObjNumMax(pNtk) * 20;
     Vec_PtrForEachEntry( vFrontier, pObj, i )
     {
+        pObj->fMarkA = 0;
         RetValue = Abc_NodeUpdateLValue( pObj, Fi );
         if ( RetValue == ABC_UPDATE_FAIL )
             break;
-        // unmark the node as processed
+        if ( i == Limit )
-        pObj->fMarkA = 0;
+        {
+            RetValue = ABC_UPDATE_FAIL;
+            pReason = "(timeout)";
+            break;
+        }
         if ( RetValue == ABC_UPDATE_NO ) 
             continue;
         assert( RetValue == ABC_UPDATE_YES );
         // arrival times have changed - add fanouts to the frontier
         Abc_ObjForEachFanout( pObj, pFanout, k )
-            if ( pFanout->fMarkA == 0 )
+            if ( pFanout->fMarkA == 0 && pFanout != pObj )
             {   
                 Vec_PtrPush( vFrontier, pFanout );
                 pFanout->fMarkA = 1;
@@ -169,16 +210,16 @@ int Abc_NtkRetimeForPeriod( Abc_Ntk_t * pNtk, int Fi )
 
   // report the results
     if ( RetValue == ABC_UPDATE_FAIL )
-        printf( "Period = %3d.  Updated nodes = %6d.    Infeasible\n", Fi, vFrontier->nSize );
+        printf( "Period = %3d.  Updated nodes = %6d.    Infeasible %s\n", Fi, vFrontier->nSize, pReason );
     else
         printf( "Period = %3d.  Updated nodes = %6d.    Feasible\n",   Fi, vFrontier->nSize );
-    Vec_PtrFree( vFrontier );
+//    Vec_PtrFree( vFrontier );
     return RetValue != ABC_UPDATE_FAIL;
 }
 
 /**Function*************************************************************
 
-  Synopsis    [Computes the l-value of the node.]
+  Synopsis    [Returns 1 if retiming with this clock period is feasible.]
 
   Description []
                
@@ -186,25 +227,277 @@ int Abc_NtkRetimeForPeriod( Abc_Ntk_t * pNtk, int Fi )
 
   SeeAlso     []
 
+***********************************************************************/
+int Abc_NtkRetimeForPeriod( Abc_Ntk_t * pNtk, int Fi )
+{
+    Abc_Obj_t * pObj;
+    int i, c, RetValue, fChange, Counter;
+    char * pReason = "";
+
+    // set l-values of all nodes to be minus infinity
+    Vec_IntFill( pNtk->pData, Abc_NtkObjNumMax(pNtk), -ABC_INFINITY );
+
+    pObj = Abc_NtkObj( pNtk, 0 );
+    Abc_NodeSetLValue( pObj, 0 );
+    Abc_NtkForEachPi( pNtk, pObj, i )
+        Abc_NodeSetLValue( pObj, 0 );
+
+    Counter = 0;
+    for ( c = 0; c < 20; c++ )
+    {
+        fChange = 0;
+        Abc_NtkForEachObj( pNtk, pObj, i )
+        {
+            if ( Abc_ObjIsPi(pObj) )
+                continue;
+            if ( Abc_ObjFaninNum(pObj) == 0 )
+                continue;
+            RetValue = Abc_NodeUpdateLValue( pObj, Fi );
+            Counter++;
+            if ( RetValue == ABC_UPDATE_FAIL )
+                break;
+            if ( RetValue == ABC_UPDATE_NO ) 
+                continue;
+            fChange = 1;
+        }
+        if ( RetValue == ABC_UPDATE_FAIL )
+            break;
+        if ( fChange == 0 )
+            break;
+    }
+    if ( c == 20 )
+    {
+        RetValue = ABC_UPDATE_FAIL;
+        pReason = "(timeout)";
+    }
+
+    // report the results
+    if ( RetValue == ABC_UPDATE_FAIL )
+        printf( "Period = %3d.  Iterations = %3d.  Updates = %6d.  Infeasible %s\n", Fi, c, Counter, pReason );
+    else
+        printf( "Period = %3d.  Iterations = %3d.  Updates = %6d.  Feasible\n",   Fi, c, Counter );
+    return RetValue != ABC_UPDATE_FAIL;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Computes the l-value of the node.]
+
+  Description [The node can be internal or a PO.]
+               
+  SideEffects []
+
+  SeeAlso     []
+
 ***********************************************************************/
 int Abc_NodeUpdateLValue( Abc_Obj_t * pObj, int Fi )
 {
-    int lValueNew, lValue0, lValue1;
+    int lValueNew, lValueOld, lValue0, lValue1;
     assert( !Abc_ObjIsPi(pObj) );
+    assert( Abc_ObjFaninNum(pObj) > 0 );
     lValue0 = Abc_NodeReadLValue(Abc_ObjFanin0(pObj)) - Fi * Abc_ObjFaninL0(pObj);
+    if ( Abc_ObjIsPo(pObj) )
+        return (lValue0 > Fi)? ABC_UPDATE_FAIL : ABC_UPDATE_NO;
     if ( Abc_ObjFaninNum(pObj) == 2 )
         lValue1 = Abc_NodeReadLValue(Abc_ObjFanin1(pObj)) - Fi * Abc_ObjFaninL1(pObj);
     else
         lValue1 = -ABC_INFINITY;
     lValueNew = 1 + ABC_MAX( lValue0, lValue1 );
-    if ( Abc_ObjIsPo(pObj) && lValueNew > Fi )
+    lValueOld = Abc_NodeReadLValue(pObj);
-        return ABC_UPDATE_FAIL;
+//    if ( lValueNew == lValueOld )
-    if ( lValueNew == Abc_NodeReadLValue(pObj) )
+    if ( lValueNew <= lValueOld )
         return ABC_UPDATE_NO;
     Abc_NodeSetLValue( pObj, lValueNew );
     return ABC_UPDATE_YES;
 }
 
+
+
+
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Abc_RetimingPrint_rec( Abc_Obj_t * pObj )
+{
+    Abc_Obj_t * pFanin0, * pFanin1;
+    int Depth0, Depth1;
+
+    if ( Abc_ObjIsPi(pObj) )
+    {
+        printf( "%d -> ", pObj->Id );
+        return 0;
+    }
+    
+    pFanin0 = Abc_ObjFanin0(pObj);
+    pFanin1 = Abc_ObjFanin1(pObj);
+
+    if ( Abc_ObjFaninL0(pObj) == 0 && Abc_ObjFaninL1(pObj) > 0 )
+        Abc_RetimingPrint_rec( pFanin0 );
+    else if ( Abc_ObjFaninL1(pObj) == 0 && Abc_ObjFaninL0(pObj) > 0 )
+        Abc_RetimingPrint_rec( pFanin1 );
+    else if ( Abc_ObjFaninL0(pObj) == 0 && Abc_ObjFaninL1(pObj) == 0 )
+    {
+        Depth0 = (int)pFanin0->pCopy;
+        Depth1 = (int)pFanin1->pCopy;
+
+        if ( Depth0 > Depth1 )
+            Abc_RetimingPrint_rec( pFanin0 );
+        else
+            Abc_RetimingPrint_rec( pFanin1 );
+    }
+
+    printf( "%d (%d) -> ", pObj->Id, (int)pObj->pCopy );
+    return 0;
+}
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Abc_Retiming_rec( Abc_Obj_t * pObj )
+{
+    int Depth0, Depth1, Depth;
+    if ( Abc_ObjIsPi(pObj) )
+    {
+        pObj->pCopy = 0;
+        return 0;
+    }
+    // if this node is already visited, skip
+    if ( Abc_NodeIsTravIdCurrent( pObj ) )
+        return (int)pObj->pCopy;
+    // mark the node as visited
+    Abc_NodeSetTravIdCurrent( pObj );
+    if ( Abc_ObjFaninL0(pObj) == 0 )
+        Depth0 = Abc_Retiming_rec( Abc_ObjFanin0(pObj) );
+    else
+        Depth0 = 0;
+    if ( Abc_ObjFaninL1(pObj) == 0 )
+        Depth1 = Abc_Retiming_rec( Abc_ObjFanin1(pObj) );
+    else
+        Depth1 = 0;
+    Depth = 1 + ABC_MAX( Depth0, Depth1 );
+    pObj->pCopy = (void *)Depth;
+    return Depth;
+}
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Abc_NtkRetiming( Abc_Ntk_t * pNtk )
+{
+    Abc_Obj_t * pObj;
+    int i, Depth;
+    Abc_NtkForEachObj( pNtk, pObj, i )
+    {
+        if ( Abc_ObjFaninNum(pObj) != 2 )
+            continue;
+        if ( Abc_ObjFaninL0(pObj) > 0 )
+        {
+            Abc_NtkIncrementTravId(pNtk);
+            Depth = Abc_Retiming_rec( Abc_ObjFanin0(pObj) );
+            if ( Depth > 30 )
+            {
+                printf( "Depth is %d.   ", Depth );
+                Abc_RetimingPrint_rec( Abc_ObjFanin0(pObj) );
+                printf( "\n\n" );
+            }
+        }
+        if ( Abc_ObjFaninL1(pObj) > 0 )
+        {
+            Abc_NtkIncrementTravId(pNtk);
+            Depth = Abc_Retiming_rec( Abc_ObjFanin1(pObj) );
+            if ( Depth > 30 )
+            {
+                printf( "Depth is %d.   ", Depth );
+                Abc_RetimingPrint_rec( Abc_ObjFanin1(pObj) );
+                printf( "\n\n" );
+            }
+        }
+    }
+    return 0;
+}
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Abc_RetimingExperiment( Abc_Ntk_t * pNtk, Vec_Str_t * vLags )
+{
+    Abc_Obj_t * pObj;
+    char Lag;
+    int i;
+
+    Vec_StrForEachEntry( vLags, Lag, i )
+    {
+        if ( Lag == 0 )
+            continue;
+        pObj = Abc_NtkObj( pNtk, i );
+        if ( Lag < 0 )
+            Abc_ObjRetimeForwardTry( pObj, -Lag );
+        else
+            Abc_ObjRetimeBackwardTry( pObj, Lag );
+    }
+
+    // make sure there are no negative latches
+    Abc_NtkForEachObj( pNtk, pObj, i )
+    {
+        if ( Abc_ObjFaninNum(pObj) == 0 )
+            continue;
+        assert( Abc_ObjFaninL0(pObj) >= 0 );
+        if ( Abc_ObjFaninNum(pObj) == 1 )
+            continue;
+        assert( Abc_ObjFaninL1(pObj) >= 0 );
+//        printf( "%d=(%d,%d) ", i, Abc_ObjFaninL0(pObj), Abc_ObjFaninL1(pObj) );
+    }
+//    printf( "\n" );
+
+    Abc_NtkRetiming( pNtk );
+
+    Vec_StrForEachEntry( vLags, Lag, i )
+    {
+        if ( Lag == 0 )
+            continue;
+        pObj = Abc_NtkObj( pNtk, i );
+        if ( Lag < 0 )
+            Abc_ObjRetimeBackwardTry( pObj, -Lag );
+        else
+            Abc_ObjRetimeForwardTry( pObj, Lag );
+    }
+
+//    Abc_NtkSeqRetimeDelayLags( pNtk );
+}
+
 ////////////////////////////////////////////////////////////////////////
 ///                       END OF FILE                                ///
 ////////////////////////////////////////////////////////////////////////

src/base/abcs/abcRetImpl.c

@@ -26,6 +26,8 @@
 
 static void Abc_ObjRetimeForward( Abc_Obj_t * pObj );
 static int  Abc_ObjRetimeBackward( Abc_Obj_t * pObj, Abc_Ntk_t * pNtk, stmm_table * tTable, Vec_Int_t * vValues );
+static void Abc_ObjRetimeBackwardUpdateEdge( Abc_Obj_t * pObj, int Edge, stmm_table * tTable );
+static void Abc_NtkRetimeSetInitialValues( Abc_Ntk_t * pNtk, stmm_table * tTable, int * pModel );
  
 ////////////////////////////////////////////////////////////////////////
 ///                     FUNCTION DEFITIONS                           ///
@@ -51,7 +53,9 @@ int Abc_NtkImplementRetiming( Abc_Ntk_t * pNtk, Vec_Str_t * vLags )
     // forward retiming
     vSteps = Abc_NtkUtilRetimingSplit( vLags, 1 );
     // translate each set of steps into moves
+    printf( "The number of forward steps  = %6d.\n", Vec_IntSize(vSteps) );
     vMoves = Abc_NtkUtilRetimingGetMoves( pNtk, vSteps, 1 );
+    printf( "The number of forward moves  = %6d.\n", Vec_PtrSize(vMoves) );
     // implement this retiming
     Abc_NtkImplementRetimingForward( pNtk, vMoves );
     Vec_IntFree( vSteps );
@@ -60,7 +64,9 @@ int Abc_NtkImplementRetiming( Abc_Ntk_t * pNtk, Vec_Str_t * vLags )
     // backward retiming
     vSteps = Abc_NtkUtilRetimingSplit( vLags, 0 );
     // translate each set of steps into moves
+    printf( "The number of backward steps = %6d.\n", Vec_IntSize(vSteps) );
     vMoves = Abc_NtkUtilRetimingGetMoves( pNtk, vSteps, 0 );
+    printf( "The number of backward moves = %6d.\n", Vec_PtrSize(vMoves) );
     // implement this retiming
     RetValue = Abc_NtkImplementRetimingBackward( pNtk, vMoves );
     Vec_IntFree( vSteps );
@@ -87,96 +93,6 @@ void Abc_NtkImplementRetimingForward( Abc_Ntk_t * pNtk, Vec_Ptr_t * vMoves )
         Abc_ObjRetimeForward( pNode );
 }
 
-/**Function*************************************************************
-
-  Synopsis    [Implements the given retiming on the sequential AIG.]
-
-  Description [Returns 0 of initial state computation fails.]
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-int Abc_NtkImplementRetimingBackward( Abc_Ntk_t * pNtk, Vec_Ptr_t * vMoves )
-{
-    Abc_RetEdge_t RetEdge;
-    stmm_table * tTable;
-    stmm_generator * gen;
-    Vec_Int_t * vValues;
-    Abc_Ntk_t * pNtkProb, * pNtkMiter, * pNtkCnf;
-    Abc_Obj_t * pNode, * pNodeNew;
-    int * pModel, Init, nDigits, RetValue, i;
-
-    // return if the retiming is trivial
-    if ( Vec_PtrSize(vMoves) == 0 )
-        return 1;
-
-    // start the table and the array of PO values
-    tTable = stmm_init_table( stmm_numcmp, stmm_numhash );
-    vValues = Vec_IntAlloc( 100 );
-
-    // create the network for the initial state computation
-    pNtkProb = Abc_NtkAlloc( ABC_NTK_LOGIC, ABC_FUNC_SOP );
-
-    // perform the backward moves and build the network
-    Vec_PtrForEachEntry( vMoves, pNode, i )
-        Abc_ObjRetimeBackward( pNode, pNtkProb, tTable, vValues );
-
-    // add the PIs corresponding to the white spots
-    stmm_foreach_item( tTable, gen, (char **)&RetEdge, (char **)&pNodeNew )
-        Abc_ObjAddFanin( pNodeNew, Abc_NtkCreatePi(pNtkProb) );
-
-    // add the PI/PO names
-    nDigits = Extra_Base10Log( Abc_NtkPiNum(pNtkProb) );
-    Abc_NtkForEachPi( pNtkProb, pNodeNew, i )
-        Abc_NtkLogicStoreName( pNodeNew, Abc_ObjNameDummy("pi", i, nDigits) );
-    nDigits = Extra_Base10Log( Abc_NtkPoNum(pNtkProb) );
-    Abc_NtkForEachPo( pNtkProb, pNodeNew, i )
-        Abc_NtkLogicStoreName( pNodeNew, Abc_ObjNameDummy("po", i, nDigits) );
-
-    // make sure everything is okay with the network structure
-    if ( !Abc_NtkDoCheck( pNtkProb ) )
-    {
-        printf( "Abc_NtkImplementRetimingBackward: The internal network check has failed.\n" );
-        return 0;
-    }
-
-    // get the miter cone
-    pNtkMiter = Abc_NtkCreateCone( pNtkProb, pNtkProb->vCos, vValues );
-    Abc_NtkDelete( pNtkProb );
-    Vec_IntFree( vValues );
-
-    // transform the miter into a logic network for efficient CNF construction
-    pNtkCnf = Abc_NtkRenode( pNtkMiter, 0, 100, 1, 0, 0 );
-    Abc_NtkDelete( pNtkMiter );
-
-    // solve the miter
-    RetValue = Abc_NtkMiterSat( pNtkCnf, 30, 0 );
-    pModel = pNtkCnf->pModel;  pNtkCnf->pModel = NULL;
-    Abc_NtkDelete( pNtkCnf );
-
-    // analyze the result
-    if ( RetValue == -1 || RetValue == 1 )
-    {
-        stmm_free_table( tTable );
-        return 0;
-    }
-
-    // set the values of the latches
-    i = 0;
-    stmm_foreach_item( tTable, gen, (char **)&RetEdge, (char **)&pNodeNew )
-    {
-        pNode = Abc_NtkObj( pNtk, RetEdge.iNode );
-        Init = pModel[i]? ABC_INIT_ONE : ABC_INIT_ZERO;
-        Abc_ObjFaninLSetInitOne( pNode, RetEdge.iEdge, RetEdge.iLatch, Init );
-        i++;
-    }
-    stmm_free_table( tTable );
-    free( pModel );
-    return 1;
-}
-
 /**Function*************************************************************
 
   Synopsis    [Retimes node forward by one latch.]
@@ -227,11 +143,120 @@ void Abc_ObjRetimeForward( Abc_Obj_t * pObj )
         Abc_ObjFaninLInsertLast( pFanout, Abc_ObjEdgeNum(pObj, pFanout), Init );
 }
 
+
+
+/**Function*************************************************************
+
+  Synopsis    [Implements the given retiming on the sequential AIG.]
+
+  Description [Returns 0 of initial state computation fails.]
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Abc_NtkImplementRetimingBackward( Abc_Ntk_t * pNtk, Vec_Ptr_t * vMoves )
+{
+    Abc_RetEdge_t RetEdge;
+    stmm_table * tTable;
+    stmm_generator * gen;
+    Vec_Int_t * vValues;
+    Abc_Ntk_t * pNtkProb, * pNtkMiter, * pNtkCnf;
+    Abc_Obj_t * pNode, * pNodeNew;
+    int * pModel, RetValue, i, clk;
+
+    // return if the retiming is trivial
+    if ( Vec_PtrSize(vMoves) == 0 )
+        return 1;
+
+    // create the network for the initial state computation
+    // start the table and the array of PO values
+    pNtkProb = Abc_NtkAlloc( ABC_NTK_LOGIC, ABC_FUNC_SOP );
+    tTable   = stmm_init_table( stmm_numcmp, stmm_numhash );
+    vValues  = Vec_IntAlloc( 100 );
+
+    // perform the backward moves and build the network for initial state computation
+    RetValue = 0;
+    Vec_PtrForEachEntry( vMoves, pNode, i )
+        RetValue |= Abc_ObjRetimeBackward( pNode, pNtkProb, tTable, vValues );
+
+    // add the PIs corresponding to the white spots
+    stmm_foreach_item( tTable, gen, (char **)&RetEdge, (char **)&pNodeNew )
+        Abc_ObjAddFanin( pNodeNew, Abc_NtkCreatePi(pNtkProb) );
+
+    // add the PI/PO names
+    Abc_NtkAddDummyPiNames( pNtkProb );
+    Abc_NtkAddDummyPoNames( pNtkProb );
+
+    // make sure everything is okay with the network structure
+    if ( !Abc_NtkDoCheck( pNtkProb ) )
+    {
+        printf( "Abc_NtkImplementRetimingBackward: The internal network check has failed.\n" );
+        Abc_NtkRetimeSetInitialValues( pNtk, tTable, NULL );
+        Abc_NtkDelete( pNtkProb );
+        stmm_free_table( tTable );
+        Vec_IntFree( vValues );
+        return 0;
+    }
+
+    // check if conflict is found
+    if ( RetValue )
+    {
+        printf( "Abc_NtkImplementRetimingBackward: A top level conflict is detected. DC latch values are used.\n" );
+        Abc_NtkRetimeSetInitialValues( pNtk, tTable, NULL );
+        Abc_NtkDelete( pNtkProb );
+        stmm_free_table( tTable );
+        Vec_IntFree( vValues );
+        return 0;
+    }
+
+    // get the miter cone
+    pNtkMiter = Abc_NtkCreateCone( pNtkProb, pNtkProb->vCos, vValues );
+    Abc_NtkDelete( pNtkProb );
+    Vec_IntFree( vValues );
+
+    printf( "The number of ANDs in the AIG = %5d.\n", Abc_NtkNodeNum(pNtkMiter) );
+
+    // transform the miter into a logic network for efficient CNF construction
+    pNtkCnf = Abc_NtkRenode( pNtkMiter, 0, 100, 1, 0, 0 );
+    Abc_NtkDelete( pNtkMiter );
+
+    // solve the miter
+clk = clock();
+    RetValue = Abc_NtkMiterSat( pNtkCnf, 30, 0 );
+if ( clock() - clk > 500 )
+{
+PRT( "SAT solving time", clock() - clk );
+}
+    pModel = pNtkCnf->pModel;  pNtkCnf->pModel = NULL;
+    Abc_NtkDelete( pNtkCnf );
+
+    // analyze the result
+    if ( RetValue == -1 || RetValue == 1 )
+    {
+        Abc_NtkRetimeSetInitialValues( pNtk, tTable, NULL );
+        if ( RetValue == 1 )
+            printf( "Abc_NtkImplementRetimingBackward: The problem is unsatisfiable. DC latch values are used.\n" );
+        else
+            printf( "Abc_NtkImplementRetimingBackward: The SAT problem timed out. DC latch values are used.\n" );
+        stmm_free_table( tTable );
+        return 0;
+    }
+
+    // set the values of the latches
+    Abc_NtkRetimeSetInitialValues( pNtk, tTable, pModel );
+    stmm_free_table( tTable );
+    free( pModel );
+    return 1;
+}
+
 /**Function*************************************************************
 
   Synopsis    [Retimes node backward by one latch.]
 
-  Description [Constructs the problem for initial state computation.]
+  Description [Constructs the problem for initial state computation.
+  Returns 1 if the conflict is found.]
                
   SideEffects []
 
@@ -242,15 +267,14 @@ int Abc_ObjRetimeBackward( Abc_Obj_t * pObj, Abc_Ntk_t * pNtkNew, stmm_table * t
 {
     Abc_Obj_t * pFanout;
     Abc_InitType_t Init, Value;
-    Abc_RetEdge_t Edge;
+    Abc_RetEdge_t RetEdge;
-    Abc_Obj_t * pNodeNew, * pFanoutNew, * pBuf;
+    Abc_Obj_t * pNodeNew, * pFanoutNew, * pBuffer;
-    unsigned Entry;
+    int i, Edge, fMet0, fMet1, fMetN;
-    int i, fMet0, fMet1, fMetX;
 
     // make sure the node can be retimed
     assert( Abc_ObjFanoutLMin(pObj) > 0 );
     // get the fanout values
-    fMet0 = fMet1 = fMetX = 0;
+    fMet0 = fMet1 = fMetN = 0;
     Abc_ObjForEachFanout( pObj, pFanout, i )
     {
         Init = Abc_ObjFaninLGetInitLast( pFanout, Abc_ObjEdgeNum(pObj, pFanout) );
@@ -259,101 +283,159 @@ int Abc_ObjRetimeBackward( Abc_Obj_t * pObj, Abc_Ntk_t * pNtkNew, stmm_table * t
         else if ( Init == ABC_INIT_ONE )
             fMet1 = 1;
         else if ( Init == ABC_INIT_NONE )
-            fMetX = 1;
+            fMetN = 1;
     }
-    // quit if conflict is found
-    if ( fMet0 && fMet1 )
-        return 0;
 
-    // get the new initial value
+    // consider the case when all fanout latchs have don't-care values
-    if ( !fMet0 && !fMet1 && !fMetX )
+    // the new values on the fanin edges will be don't-cares
+    if ( !fMet0 && !fMet1 && !fMetN )
    {
-        Init = ABC_INIT_DC;
+        // update the fanout edges
-        // do not add the node
+        Abc_ObjForEachFanout( pObj, pFanout, i )
-        pNodeNew = NULL;
+            Abc_ObjFaninLDeleteLast( pFanout, Abc_ObjEdgeNum(pObj, pFanout) );
+        // update the fanin edges
+        Abc_ObjRetimeBackwardUpdateEdge( pObj, 0, tTable );
+        Abc_ObjRetimeBackwardUpdateEdge( pObj, 1, tTable );
+        Abc_ObjFaninLInsertFirst( pObj, 0, ABC_INIT_DC );
+        Abc_ObjFaninLInsertFirst( pObj, 1, ABC_INIT_DC );
+        return 0;
     }
-    else
+    // the initial values on the fanout edges contain 0, 1, or unknown
-    {
+    // the new values on the fanin edges will be unknown
-        Init = ABC_INIT_NONE;
+
-        // add the node to the network
+    // add new AND-gate to the network
     pNodeNew = Abc_NtkCreateNode( pNtkNew );
     pNodeNew->pData = Abc_SopCreateAnd2( pNtkNew->pManFunc, Abc_ObjFaninC0(pObj), Abc_ObjFaninC1(pObj) );
+
+    // add PO fanouts if any
+    if ( fMet0 )
+    {
+        Abc_ObjAddFanin( Abc_NtkCreatePo(pNtkNew), pNodeNew );
+        Vec_IntPush( vValues, 0 );
+    }
+    if ( fMet1 )
+    {
+        Abc_ObjAddFanin( Abc_NtkCreatePo(pNtkNew), pNodeNew );
+        Vec_IntPush( vValues, 1 );
     }
 
     // perform the changes
     Abc_ObjForEachFanout( pObj, pFanout, i )
     {
-        Edge.iNode = pFanout->Id;
+        Edge = Abc_ObjEdgeNum( pObj, pFanout );
-        Edge.iEdge = Abc_ObjEdgeNum(pObj, pFanout);
+        Value = Abc_ObjFaninLDeleteLast( pFanout, Edge );
-        Edge.iLatch = Abc_ObjFaninL( pFanout, Edge.iEdge ) - 1;
+        if ( Value != ABC_INIT_NONE )
-        // try to delete this edge
+            continue;
-        stmm_delete( tTable, (char **)&Edge, (char **)&pFanoutNew );
+        // value is unknown, remove it from the table
-        // delete the entry
+        RetEdge.iNode  = pFanout->Id;
-        Value = Abc_ObjFaninLDeleteLast( pFanout, Edge.iEdge );
+        RetEdge.iEdge  = Edge;
-        if ( Value == ABC_INIT_NONE )
+        RetEdge.iLatch = Abc_ObjFaninL( pFanout, Edge ); // after edge is removed
+        if ( !stmm_delete( tTable, (char **)&RetEdge, (char **)&pFanoutNew ) )
+            assert( 0 );
+        // create the fanout of the AND gate
         Abc_ObjAddFanin( pFanoutNew, pNodeNew );
     }
 
-    // update the table for each of the edges
+    // update the fanin edges
-    Abc_ObjFaninLForEachValue( pObj, 0, Entry, i, Value )
+    Abc_ObjRetimeBackwardUpdateEdge( pObj, 0, tTable );
-    {
+    Abc_ObjRetimeBackwardUpdateEdge( pObj, 1, tTable );
-        if ( Value != ABC_INIT_NONE )
+    Abc_ObjFaninLInsertFirst( pObj, 0, ABC_INIT_NONE );
-            continue;
+    Abc_ObjFaninLInsertFirst( pObj, 1, ABC_INIT_NONE );
-        if ( !stmm_delete( tTable, (char **)&Edge, (char **)&pFanoutNew ) )
-            assert( 0 );
-        Edge.iLatch++;
-        if ( stmm_insert( tTable, (char *)Abc_RetEdge2Int(Edge), (char *)pFanoutNew ) )
-            assert( 0 );
-    }
-    Abc_ObjFaninLForEachValue( pObj, 1, Entry, i, Value )
-    {
-        if ( Value != ABC_INIT_NONE )
-            continue;
-        if ( !stmm_delete( tTable, (char **)&Edge, (char **)&pFanoutNew ) )
-            assert( 0 );
-        Edge.iLatch++;
-        if ( stmm_insert( tTable, (char *)Abc_RetEdge2Int(Edge), (char *)pFanoutNew ) )
-            assert( 0 );
-    }
-    Abc_ObjFaninLInsertFirst( pObj, 0, Init );
-    Abc_ObjFaninLInsertFirst( pObj, 1, Init );
-
-    // do not insert the don't-care node into the network
-    if ( Init == ABC_INIT_DC )
-        return 1;
 
     // add the buffer
-    pBuf = Abc_NtkCreateNode( pNtkNew );
+    pBuffer = Abc_NtkCreateNode( pNtkNew );
-    pBuf->pData = Abc_SopCreateBuf( pNtkNew->pManFunc );
+    pBuffer->pData = Abc_SopCreateBuf( pNtkNew->pManFunc );
-    Abc_ObjAddFanin( pNodeNew, pBuf );
+    Abc_ObjAddFanin( pNodeNew, pBuffer );
     // point to it from the table
-    Edge.iNode = pObj->Id;
+    RetEdge.iNode  = pObj->Id;
-    Edge.iEdge = 0;
+    RetEdge.iEdge  = 0;
-    Edge.iLatch = 0;
+    RetEdge.iLatch = 0;
-    if ( stmm_insert( tTable, (char *)Abc_RetEdge2Int(Edge), (char *)pBuf ) )
+    if ( stmm_insert( tTable, (char *)Abc_RetEdge2Int(RetEdge), (char *)pBuffer ) )
         assert( 0 );
 
     // add the buffer
-    pBuf = Abc_NtkCreateNode( pNtkNew );
+    pBuffer = Abc_NtkCreateNode( pNtkNew );
-    pBuf->pData = Abc_SopCreateBuf( pNtkNew->pManFunc );
+    pBuffer->pData = Abc_SopCreateBuf( pNtkNew->pManFunc );
-    Abc_ObjAddFanin( pNodeNew, pBuf );
+    Abc_ObjAddFanin( pNodeNew, pBuffer );
     // point to it from the table
-    Edge.iNode = pObj->Id;
+    RetEdge.iNode  = pObj->Id;
-    Edge.iEdge = 1;
+    RetEdge.iEdge  = 1;
-    Edge.iLatch = 0;
+    RetEdge.iLatch = 0;
-    if ( stmm_insert( tTable, (char *)Abc_RetEdge2Int(Edge), (char *)pBuf ) )
+    if ( stmm_insert( tTable, (char *)Abc_RetEdge2Int(RetEdge), (char *)pBuffer ) )
         assert( 0 );
 
-    // check if the output value is required
+    // report conflict is found
-    if ( fMet0 || fMet1 )
+    return fMet0 && fMet1;
-    {
-        // add the PO and the value
-        Abc_ObjAddFanin( Abc_NtkCreatePo(pNtkNew), pNodeNew );
-        Vec_IntPush( vValues, fMet1 );
-    }
-    return 1;
 }
 
+/**Function*************************************************************
+
+  Synopsis    [Generates the printable edge label with the initial state.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Abc_ObjRetimeBackwardUpdateEdge( Abc_Obj_t * pObj, int Edge, stmm_table * tTable )
+{
+    Abc_Obj_t * pFanoutNew;
+    Abc_RetEdge_t RetEdge;
+    Abc_InitType_t Init;
+    int nLatches, i;
+
+    // get the number of latches on the edge
+    nLatches = Abc_ObjFaninL( pObj, Edge );
+    assert( nLatches <= ABC_MAX_EDGE_LATCH );
+    for ( i = nLatches - 1; i >= 0; i-- )
+    {
+        // get the value of this latch
+        Init = Abc_ObjFaninLGetInitOne( pObj, Edge, i );
+        if ( Init != ABC_INIT_NONE )
+            continue;
+        // get the retiming edge
+        RetEdge.iNode  = pObj->Id;
+        RetEdge.iEdge  = Edge;
+        RetEdge.iLatch = i;
+        // remove entry from table and add it with a different key
+        if ( !stmm_delete( tTable, (char **)&RetEdge, (char **)&pFanoutNew ) )
+            assert( 0 );
+        RetEdge.iLatch++;
+        if ( stmm_insert( tTable, (char *)Abc_RetEdge2Int(RetEdge), (char *)pFanoutNew ) )
+            assert( 0 );
+    }
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Sets the initial values.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Abc_NtkRetimeSetInitialValues( Abc_Ntk_t * pNtk, stmm_table * tTable, int * pModel )
+{
+    Abc_Obj_t * pNode;
+    stmm_generator * gen;
+    Abc_RetEdge_t RetEdge;
+    Abc_InitType_t Init;
+    int i;
+
+    i = 0;
+    stmm_foreach_item( tTable, gen, (char **)&RetEdge, NULL )
+    {
+        pNode = Abc_NtkObj( pNtk, RetEdge.iNode );
+        Init = pModel? (pModel[i]? ABC_INIT_ONE : ABC_INIT_ZERO) : ABC_INIT_DC;
+        Abc_ObjFaninLSetInitOne( pNode, RetEdge.iEdge, RetEdge.iLatch, Init );
+        i++;
+    }
+}
 
 ////////////////////////////////////////////////////////////////////////
 ///                       END OF FILE                                ///

src/base/abcs/abcRetUtil.c

@@ -127,12 +127,14 @@ Vec_Ptr_t * Abc_NtkUtilRetimingGetMoves( Abc_Ntk_t * pNtk, Vec_Int_t * vSteps, b
     Vec_Ptr_t * vMoves;
     Abc_Obj_t * pNode;
     int i, k, iNode, nLatches, Number;
+    int fChange;
     assert( Abc_NtkIsSeq( pNtk ) );
     // process the nodes
     vMoves = Vec_PtrAlloc( 100 );
     while ( Vec_IntSize(vSteps) > 0 )
     {
         iNode = 0;
+        fChange = 0;
         Vec_IntForEachEntry( vSteps, Number, i )
         {
             // get the retiming step
@@ -151,6 +153,7 @@ Vec_Ptr_t * Abc_NtkUtilRetimingGetMoves( Abc_Ntk_t * pNtk, Vec_Int_t * vSteps, b
                 continue;
             }
             assert( nLatches > 0 );
+            fChange = 1;
             // get the number of latches to be retimed over this node
             nLatches = ABC_MIN( nLatches, (int)RetStep.nLatches );
             // retime the latches forward
@@ -169,6 +172,11 @@ Vec_Ptr_t * Abc_NtkUtilRetimingGetMoves( Abc_Ntk_t * pNtk, Vec_Int_t * vSteps, b
         }
         // reduce the array
         Vec_IntShrink( vSteps, iNode );
+        if ( !fChange )
+        {
+            printf( "Warning: %d strange steps.\n", Vec_IntSize(vSteps) );
+            break;
+        }
     }
     // undo the tentative retiming
     if ( fForward )
@@ -204,6 +212,7 @@ Vec_Int_t * Abc_NtkUtilRetimingSplit( Vec_Str_t * vLags, int fForward )
     vNodes = Vec_IntAlloc( 100 );
     Vec_StrForEachEntry( vLags, Value, i )
     {
+//        assert( Value <= ABC_MAX_EDGE_LATCH );
         if ( Value < 0 && fForward )
         {
             RetStep.iNode = i;

src/base/abcs/abcSeq.c

@@ -92,6 +92,8 @@ Abc_Ntk_t * Abc_NtkAigToSeq( Abc_Ntk_t * pNtk )
         Abc_NtkDupObj(pNtkNew, pObj);
     Abc_NtkForEachPo( pNtk, pObj, i )
         Abc_NtkDupObj(pNtkNew, pObj);
+//    Abc_NtkForEachLatch( pNtk, pObj, i )
+//        Vec_PtrPush( pNtkNew->vObjs, NULL );
     // copy the PI/PO names
     Abc_NtkForEachPi( pNtk, pObj, i )
         Abc_NtkLogicStoreName( Abc_NtkPi(pNtkNew,i), Abc_ObjName(pObj) );
@@ -104,6 +106,7 @@ Abc_Ntk_t * Abc_NtkAigToSeq( Abc_Ntk_t * pNtk )
         if ( Abc_ObjFaninNum(pObj) != 2 )
             continue;
         Abc_NtkDupObj(pNtkNew, pObj);
+//        assert( pObj->Id == pObj->pCopy->Id );
         pObj->pCopy->fPhase = pObj->fPhase; // needed for choices
         pObj->pCopy->Level = pObj->Level; 
     }
@@ -248,7 +251,7 @@ Abc_Ntk_t * Abc_NtkSeqToLogicSop( Abc_Ntk_t * pNtk )
 {
     Abc_Ntk_t * pNtkNew; 
     Abc_Obj_t * pObj, * pObjNew, * pFaninNew, * pConst1;
-    int i, nCutNodes, nDigits;
+    int i, nCutNodes;
     unsigned Init;
     int nLatchMax = 0;
 
@@ -311,17 +314,13 @@ Abc_Ntk_t * Abc_NtkSeqToLogicSop( Abc_Ntk_t * pNtk )
         Abc_ObjAddFanin( pObj->pCopy, pFaninNew );
         // the complemented edges are subsumed by the node function
     }
-    printf( "The max edge latch num = %d.\n", nLatchMax );
+//    printf( "The max edge latch num = %d.\n", nLatchMax );
-    // count the number of digits in the latch names
-    nDigits = Extra_Base10Log( Abc_NtkLatchNum(pNtkNew) );
     // add the latches and their names
+    Abc_NtkAddDummyLatchNames( pNtkNew );
     Abc_NtkForEachLatch( pNtkNew, pObjNew, i )
     {
-        // add the latch to the CI/CO arrays
         Vec_PtrPush( pNtkNew->vCis, pObjNew );
         Vec_PtrPush( pNtkNew->vCos, pObjNew );
-        // create latch name
-        Abc_NtkLogicStoreName( pObjNew, Abc_ObjNameDummy("L", i, nDigits) );
     }
     // fix the problem with complemented and duplicated CO edges
     Abc_NtkLogicMakeSimpleCos( pNtkNew, 0 );

src/base/abcs/abcShare.c

@@ -48,6 +48,10 @@ void Abc_NtkSeqShareFanouts( Abc_Ntk_t * pNtk )
     Abc_Obj_t * pObj;
     int i;
     vNodes = Vec_PtrAlloc( 10 );
+    // share the PI latches
+    Abc_NtkForEachPi( pNtk, pObj, i )
+        Abc_NodeSeqShareFanouts( pObj, vNodes );
+    // share the node latches
     Abc_NtkForEachNode( pNtk, pObj, i )
         Abc_NodeSeqShareFanouts( pObj, vNodes );
     Vec_PtrFree( vNodes );

src/base/abcs/abcUtils.c

@@ -76,6 +76,59 @@ int Abc_NtkSeqLatchNumShared( Abc_Ntk_t * pNtk )
     return Counter;
 }
 
+/**Function*************************************************************
+
+  Synopsis    [Counts the number of latches in the sequential AIG.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Abc_ObjLatchGetInitNums( Abc_Obj_t * pObj, int Edge, int * pInits )
+{
+    Abc_InitType_t Init;
+    int nLatches, i;
+    nLatches = Abc_ObjFaninL( pObj, Edge );
+    assert( nLatches <= ABC_MAX_EDGE_LATCH );
+    for ( i = 0; i < nLatches; i++ )
+    {
+        Init = Abc_ObjFaninLGetInitOne( pObj, Edge, i );
+        pInits[Init]++;
+    }
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Counts the number of latches in the sequential AIG.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Abc_NtkSeqLatchGetInitNums( Abc_Ntk_t * pNtk, int * pInits )
+{
+    Abc_Obj_t * pObj;
+    int i;
+    assert( Abc_NtkIsSeq( pNtk ) );
+    for ( i = 0; i < 4; i++ )    
+        pInits[i] = 0;
+    Abc_NtkForEachPo( pNtk, pObj, i )
+        Abc_ObjLatchGetInitNums( pObj, 0, pInits );
+    Abc_NtkForEachNode( pNtk, pObj, i )
+    {
+        if ( Abc_ObjFaninNum(pObj) > 0 )
+            Abc_ObjLatchGetInitNums( pObj, 0, pInits );
+        if ( Abc_ObjFaninNum(pObj) > 1 )
+            Abc_ObjLatchGetInitNums( pObj, 1, pInits );
+    }
+}
+
 /**Function*************************************************************
 
   Synopsis    [Generates the printable edge label with the initial state.]

src/base/abcs/abcs.h

@@ -104,6 +104,8 @@ static inline int Abc_ObjFanoutLMax( Abc_Obj_t * pObj )
 {
     Abc_Obj_t * pFanout;
     int i, nLatchCur, nLatchRes;
+    if ( Abc_ObjFanoutNum(pObj) == 0 )
+        return 0;
     nLatchRes = 0;
     Abc_ObjForEachFanout( pObj, pFanout, i )
     {
@@ -120,6 +122,8 @@ static inline int Abc_ObjFanoutLMin( Abc_Obj_t * pObj )
 {
     Abc_Obj_t * pFanout;
     int i, nLatchCur, nLatchRes;
+    if ( Abc_ObjFanoutNum(pObj) == 0 )
+        return 0;
     nLatchRes = ABC_INFINITY;
     Abc_ObjForEachFanout( pObj, pFanout, i )
     {
@@ -246,8 +250,8 @@ static inline void Abc_ObjRetimeForwardTry( Abc_Obj_t * pObj, int nLatches )
     // make sure it is an AND gate
     assert( Abc_ObjFaninNum(pObj) == 2 );
     // make sure it has enough latches
-    assert( Abc_ObjFaninL0(pObj) >= nLatches );
+//    assert( Abc_ObjFaninL0(pObj) >= nLatches );
-    assert( Abc_ObjFaninL1(pObj) >= nLatches );
+//    assert( Abc_ObjFaninL1(pObj) >= nLatches );
     // subtract these latches on the fanin side
     Abc_ObjAddFaninL0( pObj, -nLatches );
     Abc_ObjAddFaninL1( pObj, -nLatches );
@@ -266,7 +270,7 @@ static inline void Abc_ObjRetimeBackwardTry( Abc_Obj_t * pObj, int nLatches )
     // subtract these latches on the fanout side
     Abc_ObjForEachFanout( pObj, pFanout, i )
     {
-        assert( Abc_ObjFanoutL(pObj, pFanout) >= nLatches );
+//        assert( Abc_ObjFanoutL(pObj, pFanout) >= nLatches );
         Abc_ObjAddFanoutL( pObj, pFanout, -nLatches );
     }
     // add these latches on the fanin size
@@ -282,7 +286,7 @@ static inline void Abc_ObjRetimeBackwardTry( Abc_Obj_t * pObj, int nLatches )
 // iterating through the initial values of the edge
 #define Abc_ObjFaninLForEachValue( pObj, Edge, Init, i, Value ) \
     for ( i = 0, Init = Abc_ObjFaninLGetInit(pObj, Edge); \
-          i < Abc_ObjFaninL(pObj, Edge) && ((Value = ((Init >> i) & 3)), 1); i++ ) 
+          i < Abc_ObjFaninL(pObj, Edge) && ((Value = ((Init >> (2*i)) & 0x3)), 1); i++ ) 
 
 ////////////////////////////////////////////////////////////////////////
 ///                    FUNCTION DECLARATIONS                         ///
@@ -311,6 +315,7 @@ extern void               Abc_NtkSeqShareFanouts( Abc_Ntk_t * pNtk );
 /*=== abcUtil.c ==============================================================*/
 extern int                Abc_NtkSeqLatchNum( Abc_Ntk_t * pNtk );
 extern int                Abc_NtkSeqLatchNumShared( Abc_Ntk_t * pNtk );
+extern void               Abc_NtkSeqLatchGetInitNums( Abc_Ntk_t * pNtk, int * pInits );
 extern char *             Abc_ObjFaninGetInitPrintable( Abc_Obj_t * pObj, int Edge );
 
 ////////////////////////////////////////////////////////////////////////