Version abc51128

20 files changed, 2341 insertions, 203 deletions

diff --git a/abc.opt b/abc.opt
index 64bbad68..680f3fd7 100644
--- a/abc.opt
+++ b/abc.opt
diff --git a/abc.plg b/abc.plg
index 632ed572..a05b9353 100644
--- a/abc.plg
+++ b/abc.plg
@@ -3,9 +3,694 @@
 <pre>
 <h1>Build Log</h1>
 <h3>
---------------------Configuration: abc - Win32 Debug--------------------
+--------------------Configuration: abc - Win32 Release--------------------
 </h3>
 <h3>Command Lines</h3>
+Creating temporary file "C:\DOCUME~1\alanmi\LOCALS~1\Temp\RSP1FA3.tmp" with contents
+[
+/nologo /ML /W3 /GX /O2 /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\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\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\npn" /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\abcFanio.c"
+"C:\_projects\abc\src\base\abc\abcNtk.c"
+"C:\_projects\abc\src\base\abci\abcCut.c"
+"C:\_projects\abc\src\base\seq\seqAigCore.c"
+"C:\_projects\abc\src\base\seq\seqAigIter.c"
+"C:\_projects\abc\src\base\seq\seqCreate.c"
+"C:\_projects\abc\src\base\seq\seqFpgaCore.c"
+"C:\_projects\abc\src\base\seq\seqFpgaIter.c"
+"C:\_projects\abc\src\base\seq\seqLatch.c"
+"C:\_projects\abc\src\base\seq\seqMan.c"
+"C:\_projects\abc\src\base\seq\seqMapCore.c"
+"C:\_projects\abc\src\base\seq\seqMapIter.c"
+"C:\_projects\abc\src\base\seq\seqRetCore.c"
+"C:\_projects\abc\src\base\seq\seqRetIter.c"
+"C:\_projects\abc\src\base\seq\seqShare.c"
+"C:\_projects\abc\src\base\seq\seqUtil.c"
+"C:\_projects\abc\src\base\io\ioWriteDot.c"
+"C:\_projects\abc\src\base\io\ioWriteList.c"
+]
+Creating command line "cl.exe @C:\DOCUME~1\alanmi\LOCALS~1\Temp\RSP1FA3.tmp" 
+Creating temporary file "C:\DOCUME~1\alanmi\LOCALS~1\Temp\RSP1FA4.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
+.\Release\abcCheck.obj
+.\Release\abcDfs.obj
+.\Release\abcFanio.obj
+.\Release\abcFunc.obj
+.\Release\abcLatch.obj
+.\Release\abcMinBase.obj
+.\Release\abcNames.obj
+.\Release\abcNetlist.obj
+.\Release\abcNtk.obj
+.\Release\abcObj.obj
+.\Release\abcRefs.obj
+.\Release\abcShow.obj
+.\Release\abcSop.obj
+.\Release\abcUtil.obj
+.\Release\abc.obj
+.\Release\abcAttach.obj
+.\Release\abcBalance.obj
+.\Release\abcCollapse.obj
+.\Release\abcCut.obj
+.\Release\abcDsd.obj
+.\Release\abcFpga.obj
+.\Release\abcFraig.obj
+.\Release\abcFxu.obj
+.\Release\abcMap.obj
+.\Release\abcMiter.obj
+.\Release\abcNtbdd.obj
+.\Release\abcPga.obj
+.\Release\abcPrint.obj
+.\Release\abcReconv.obj
+.\Release\abcRefactor.obj
+.\Release\abcRenode.obj
+.\Release\abcRewrite.obj
+.\Release\abcSat.obj
+.\Release\abcStrash.obj
+.\Release\abcSweep.obj
+.\Release\abcSymm.obj
+.\Release\abcTiming.obj
+.\Release\abcUnreach.obj
+.\Release\abcVanEijk.obj
+.\Release\abcVanImp.obj
+.\Release\abcVerify.obj
+.\Release\seqAigCore.obj
+.\Release\seqAigIter.obj
+.\Release\seqCreate.obj
+.\Release\seqFpgaCore.obj
+.\Release\seqFpgaIter.obj
+.\Release\seqLatch.obj
+.\Release\seqMan.obj
+.\Release\seqMapCore.obj
+.\Release\seqMapIter.obj
+.\Release\seqRetCore.obj
+.\Release\seqRetIter.obj
+.\Release\seqShare.obj
+.\Release\seqUtil.obj
+.\Release\cmd.obj
+.\Release\cmdAlias.obj
+.\Release\cmdApi.obj
+.\Release\cmdFlag.obj
+.\Release\cmdHist.obj
+.\Release\cmdUtils.obj
+.\Release\io.obj
+.\Release\ioRead.obj
+.\Release\ioReadBaf.obj
+.\Release\ioReadBench.obj
+.\Release\ioReadBlif.obj
+.\Release\ioReadEdif.obj
+.\Release\ioReadEqn.obj
+.\Release\ioReadPla.obj
+.\Release\ioReadVerilog.obj
+.\Release\ioUtil.obj
+.\Release\ioWriteBaf.obj
+.\Release\ioWriteBench.obj
+.\Release\ioWriteBlif.obj
+.\Release\ioWriteCnf.obj
+.\Release\ioWriteDot.obj
+.\Release\ioWriteEqn.obj
+.\Release\ioWriteGml.obj
+.\Release\ioWriteList.obj
+.\Release\ioWritePla.obj
+.\Release\libSupport.obj
+.\Release\main.obj
+.\Release\mainFrame.obj
+.\Release\mainInit.obj
+.\Release\mainUtils.obj
+.\Release\cuddAddAbs.obj
+.\Release\cuddAddApply.obj
+.\Release\cuddAddFind.obj
+.\Release\cuddAddInv.obj
+.\Release\cuddAddIte.obj
+.\Release\cuddAddNeg.obj
+.\Release\cuddAddWalsh.obj
+.\Release\cuddAndAbs.obj
+.\Release\cuddAnneal.obj
+.\Release\cuddApa.obj
+.\Release\cuddAPI.obj
+.\Release\cuddApprox.obj
+.\Release\cuddBddAbs.obj
+.\Release\cuddBddCorr.obj
+.\Release\cuddBddIte.obj
+.\Release\cuddBridge.obj
+.\Release\cuddCache.obj
+.\Release\cuddCheck.obj
+.\Release\cuddClip.obj
+.\Release\cuddCof.obj
+.\Release\cuddCompose.obj
+.\Release\cuddDecomp.obj
+.\Release\cuddEssent.obj
+.\Release\cuddExact.obj
+.\Release\cuddExport.obj
+.\Release\cuddGenCof.obj
+.\Release\cuddGenetic.obj
+.\Release\cuddGroup.obj
+.\Release\cuddHarwell.obj
+.\Release\cuddInit.obj
+.\Release\cuddInteract.obj
+.\Release\cuddLCache.obj
+.\Release\cuddLevelQ.obj
+.\Release\cuddLinear.obj
+.\Release\cuddLiteral.obj
+.\Release\cuddMatMult.obj
+.\Release\cuddPriority.obj
+.\Release\cuddRead.obj
+.\Release\cuddRef.obj
+.\Release\cuddReorder.obj
+.\Release\cuddSat.obj
+.\Release\cuddSign.obj
+.\Release\cuddSolve.obj
+.\Release\cuddSplit.obj
+.\Release\cuddSubsetHB.obj
+.\Release\cuddSubsetSP.obj
+.\Release\cuddSymmetry.obj
+.\Release\cuddTable.obj
+.\Release\cuddUtil.obj
+.\Release\cuddWindow.obj
+.\Release\cuddZddCount.obj
+.\Release\cuddZddFuncs.obj
+.\Release\cuddZddGroup.obj
+.\Release\cuddZddIsop.obj
+.\Release\cuddZddLin.obj
+.\Release\cuddZddMisc.obj
+.\Release\cuddZddPort.obj
+.\Release\cuddZddReord.obj
+.\Release\cuddZddSetop.obj
+.\Release\cuddZddSymm.obj
+.\Release\cuddZddUtil.obj
+.\Release\epd.obj
+.\Release\mtrBasic.obj
+.\Release\mtrGroup.obj
+.\Release\parseCore.obj
+.\Release\parseStack.obj
+.\Release\dsdApi.obj
+.\Release\dsdCheck.obj
+.\Release\dsdLocal.obj
+.\Release\dsdMan.obj
+.\Release\dsdProc.obj
+.\Release\dsdTree.obj
+.\Release\reoApi.obj
+.\Release\reoCore.obj
+.\Release\reoProfile.obj
+.\Release\reoSift.obj
+.\Release\reoSwap.obj
+.\Release\reoTest.obj
+.\Release\reoTransfer.obj
+.\Release\reoUnits.obj
+.\Release\added.obj
+.\Release\solver.obj
+.\Release\msatActivity.obj
+.\Release\msatClause.obj
+.\Release\msatClauseVec.obj
+.\Release\msatMem.obj
+.\Release\msatOrderH.obj
+.\Release\msatQueue.obj
+.\Release\msatRead.obj
+.\Release\msatSolverApi.obj
+.\Release\msatSolverCore.obj
+.\Release\msatSolverIo.obj
+.\Release\msatSolverSearch.obj
+.\Release\msatSort.obj
+.\Release\msatVec.obj
+.\Release\fraigApi.obj
+.\Release\fraigCanon.obj
+.\Release\fraigFanout.obj
+.\Release\fraigFeed.obj
+.\Release\fraigMan.obj
+.\Release\fraigMem.obj
+.\Release\fraigNode.obj
+.\Release\fraigPrime.obj
+.\Release\fraigSat.obj
+.\Release\fraigTable.obj
+.\Release\fraigUtil.obj
+.\Release\fraigVec.obj
+.\Release\csat_apis.obj
+.\Release\fxu.obj
+.\Release\fxuCreate.obj
+.\Release\fxuHeapD.obj
+.\Release\fxuHeapS.obj
+.\Release\fxuList.obj
+.\Release\fxuMatrix.obj
+.\Release\fxuPair.obj
+.\Release\fxuPrint.obj
+.\Release\fxuReduce.obj
+.\Release\fxuSelect.obj
+.\Release\fxuSingle.obj
+.\Release\fxuUpdate.obj
+.\Release\rwrDec.obj
+.\Release\rwrEva.obj
+.\Release\rwrExp.obj
+.\Release\rwrLib.obj
+.\Release\rwrMan.obj
+.\Release\rwrPrint.obj
+.\Release\rwrUtil.obj
+.\Release\cutApi.obj
+.\Release\cutCut.obj
+.\Release\cutMan.obj
+.\Release\cutMerge.obj
+.\Release\cutNode.obj
+.\Release\cutOracle.obj
+.\Release\cutSeq.obj
+.\Release\cutTruth.obj
+.\Release\decAbc.obj
+.\Release\decFactor.obj
+.\Release\decMan.obj
+.\Release\decPrint.obj
+.\Release\decUtil.obj
+.\Release\simMan.obj
+.\Release\simSat.obj
+.\Release\simSeq.obj
+.\Release\simSupp.obj
+.\Release\simSwitch.obj
+.\Release\simSym.obj
+.\Release\simSymSat.obj
+.\Release\simSymSim.obj
+.\Release\simSymStr.obj
+.\Release\simUtils.obj
+.\Release\fpga.obj
+.\Release\fpgaCore.obj
+.\Release\fpgaCreate.obj
+.\Release\fpgaCut.obj
+.\Release\fpgaCutUtils.obj
+.\Release\fpgaFanout.obj
+.\Release\fpgaLib.obj
+.\Release\fpgaMatch.obj
+.\Release\fpgaSwitch.obj
+.\Release\fpgaTime.obj
+.\Release\fpgaTruth.obj
+.\Release\fpgaUtils.obj
+.\Release\fpgaVec.obj
+.\Release\mapper.obj
+.\Release\mapperCanon.obj
+.\Release\mapperCore.obj
+.\Release\mapperCreate.obj
+.\Release\mapperCut.obj
+.\Release\mapperCutUtils.obj
+.\Release\mapperFanout.obj
+.\Release\mapperLib.obj
+.\Release\mapperMatch.obj
+.\Release\mapperRefs.obj
+.\Release\mapperSuper.obj
+.\Release\mapperSwitch.obj
+.\Release\mapperTable.obj
+.\Release\mapperTime.obj
+.\Release\mapperTree.obj
+.\Release\mapperTruth.obj
+.\Release\mapperUtils.obj
+.\Release\mapperVec.obj
+.\Release\mio.obj
+.\Release\mioApi.obj
+.\Release\mioFunc.obj
+.\Release\mioRead.obj
+.\Release\mioUtils.obj
+.\Release\super.obj
+.\Release\superAnd.obj
+.\Release\superGate.obj
+.\Release\superWrite.obj
+.\Release\pgaCore.obj
+.\Release\pgaMan.obj
+.\Release\pgaMatch.obj
+.\Release\pgaUtil.obj
+.\Release\extraBddKmap.obj
+.\Release\extraBddMisc.obj
+.\Release\extraBddSymm.obj
+.\Release\extraUtilBitMatrix.obj
+.\Release\extraUtilCanon.obj
+.\Release\extraUtilFile.obj
+.\Release\extraUtilMemory.obj
+.\Release\extraUtilMisc.obj
+.\Release\extraUtilProgress.obj
+.\Release\extraUtilReader.obj
+.\Release\st.obj
+.\Release\stmm.obj
+.\Release\cpu_stats.obj
+.\Release\cpu_time.obj
+.\Release\datalimit.obj
+.\Release\getopt.obj
+.\Release\pathsearch.obj
+.\Release\safe_mem.obj
+.\Release\strsav.obj
+.\Release\texpand.obj
+.\Release\mvc.obj
+.\Release\mvcApi.obj
+.\Release\mvcCompare.obj
+.\Release\mvcContain.obj
+.\Release\mvcCover.obj
+.\Release\mvcCube.obj
+.\Release\mvcDivide.obj
+.\Release\mvcDivisor.obj
+.\Release\mvcList.obj
+.\Release\mvcLits.obj
+.\Release\mvcMan.obj
+.\Release\mvcOpAlg.obj
+.\Release\mvcOpBool.obj
+.\Release\mvcPrint.obj
+.\Release\mvcSort.obj
+.\Release\mvcUtils.obj
+]
+Creating command line "link.exe @C:\DOCUME~1\alanmi\LOCALS~1\Temp\RSP1FA4.tmp"
+<h3>Output Window</h3>
+Compiling...
+abcFanio.c
+abcNtk.c
+abcCut.c
+seqAigCore.c
+seqAigIter.c
+seqCreate.c
+seqFpgaCore.c
+seqFpgaIter.c
+seqLatch.c
+seqMan.c
+seqMapCore.c
+seqMapIter.c
+seqRetCore.c
+seqRetIter.c
+seqShare.c
+seqUtil.c
+ioWriteDot.c
+ioWriteList.c
+Linking...
+Creating temporary file "C:\DOCUME~1\alanmi\LOCALS~1\Temp\RSP1FA6.tmp" with contents
+[
+/nologo /o"Release/abc.bsc" 
+.\Release\abcAig.sbr
+.\Release\abcCheck.sbr
+.\Release\abcDfs.sbr
+.\Release\abcFanio.sbr
+.\Release\abcFunc.sbr
+.\Release\abcLatch.sbr
+.\Release\abcMinBase.sbr
+.\Release\abcNames.sbr
+.\Release\abcNetlist.sbr
+.\Release\abcNtk.sbr
+.\Release\abcObj.sbr
+.\Release\abcRefs.sbr
+.\Release\abcShow.sbr
+.\Release\abcSop.sbr
+.\Release\abcUtil.sbr
+.\Release\abc.sbr
+.\Release\abcAttach.sbr
+.\Release\abcBalance.sbr
+.\Release\abcCollapse.sbr
+.\Release\abcCut.sbr
+.\Release\abcDsd.sbr
+.\Release\abcFpga.sbr
+.\Release\abcFraig.sbr
+.\Release\abcFxu.sbr
+.\Release\abcMap.sbr
+.\Release\abcMiter.sbr
+.\Release\abcNtbdd.sbr
+.\Release\abcPga.sbr
+.\Release\abcPrint.sbr
+.\Release\abcReconv.sbr
+.\Release\abcRefactor.sbr
+.\Release\abcRenode.sbr
+.\Release\abcRewrite.sbr
+.\Release\abcSat.sbr
+.\Release\abcStrash.sbr
+.\Release\abcSweep.sbr
+.\Release\abcSymm.sbr
+.\Release\abcTiming.sbr
+.\Release\abcUnreach.sbr
+.\Release\abcVanEijk.sbr
+.\Release\abcVanImp.sbr
+.\Release\abcVerify.sbr
+.\Release\seqAigCore.sbr
+.\Release\seqAigIter.sbr
+.\Release\seqCreate.sbr
+.\Release\seqFpgaCore.sbr
+.\Release\seqFpgaIter.sbr
+.\Release\seqLatch.sbr
+.\Release\seqMan.sbr
+.\Release\seqMapCore.sbr
+.\Release\seqMapIter.sbr
+.\Release\seqRetCore.sbr
+.\Release\seqRetIter.sbr
+.\Release\seqShare.sbr
+.\Release\seqUtil.sbr
+.\Release\cmd.sbr
+.\Release\cmdAlias.sbr
+.\Release\cmdApi.sbr
+.\Release\cmdFlag.sbr
+.\Release\cmdHist.sbr
+.\Release\cmdUtils.sbr
+.\Release\io.sbr
+.\Release\ioRead.sbr
+.\Release\ioReadBaf.sbr
+.\Release\ioReadBench.sbr
+.\Release\ioReadBlif.sbr
+.\Release\ioReadEdif.sbr
+.\Release\ioReadEqn.sbr
+.\Release\ioReadPla.sbr
+.\Release\ioReadVerilog.sbr
+.\Release\ioUtil.sbr
+.\Release\ioWriteBaf.sbr
+.\Release\ioWriteBench.sbr
+.\Release\ioWriteBlif.sbr
+.\Release\ioWriteCnf.sbr
+.\Release\ioWriteDot.sbr
+.\Release\ioWriteEqn.sbr
+.\Release\ioWriteGml.sbr
+.\Release\ioWriteList.sbr
+.\Release\ioWritePla.sbr
+.\Release\libSupport.sbr
+.\Release\main.sbr
+.\Release\mainFrame.sbr
+.\Release\mainInit.sbr
+.\Release\mainUtils.sbr
+.\Release\cuddAddAbs.sbr
+.\Release\cuddAddApply.sbr
+.\Release\cuddAddFind.sbr
+.\Release\cuddAddInv.sbr
+.\Release\cuddAddIte.sbr
+.\Release\cuddAddNeg.sbr
+.\Release\cuddAddWalsh.sbr
+.\Release\cuddAndAbs.sbr
+.\Release\cuddAnneal.sbr
+.\Release\cuddApa.sbr
+.\Release\cuddAPI.sbr
+.\Release\cuddApprox.sbr
+.\Release\cuddBddAbs.sbr
+.\Release\cuddBddCorr.sbr
+.\Release\cuddBddIte.sbr
+.\Release\cuddBridge.sbr
+.\Release\cuddCache.sbr
+.\Release\cuddCheck.sbr
+.\Release\cuddClip.sbr
+.\Release\cuddCof.sbr
+.\Release\cuddCompose.sbr
+.\Release\cuddDecomp.sbr
+.\Release\cuddEssent.sbr
+.\Release\cuddExact.sbr
+.\Release\cuddExport.sbr
+.\Release\cuddGenCof.sbr
+.\Release\cuddGenetic.sbr
+.\Release\cuddGroup.sbr
+.\Release\cuddHarwell.sbr
+.\Release\cuddInit.sbr
+.\Release\cuddInteract.sbr
+.\Release\cuddLCache.sbr
+.\Release\cuddLevelQ.sbr
+.\Release\cuddLinear.sbr
+.\Release\cuddLiteral.sbr
+.\Release\cuddMatMult.sbr
+.\Release\cuddPriority.sbr
+.\Release\cuddRead.sbr
+.\Release\cuddRef.sbr
+.\Release\cuddReorder.sbr
+.\Release\cuddSat.sbr
+.\Release\cuddSign.sbr
+.\Release\cuddSolve.sbr
+.\Release\cuddSplit.sbr
+.\Release\cuddSubsetHB.sbr
+.\Release\cuddSubsetSP.sbr
+.\Release\cuddSymmetry.sbr
+.\Release\cuddTable.sbr
+.\Release\cuddUtil.sbr
+.\Release\cuddWindow.sbr
+.\Release\cuddZddCount.sbr
+.\Release\cuddZddFuncs.sbr
+.\Release\cuddZddGroup.sbr
+.\Release\cuddZddIsop.sbr
+.\Release\cuddZddLin.sbr
+.\Release\cuddZddMisc.sbr
+.\Release\cuddZddPort.sbr
+.\Release\cuddZddReord.sbr
+.\Release\cuddZddSetop.sbr
+.\Release\cuddZddSymm.sbr
+.\Release\cuddZddUtil.sbr
+.\Release\epd.sbr
+.\Release\mtrBasic.sbr
+.\Release\mtrGroup.sbr
+.\Release\parseCore.sbr
+.\Release\parseStack.sbr
+.\Release\dsdApi.sbr
+.\Release\dsdCheck.sbr
+.\Release\dsdLocal.sbr
+.\Release\dsdMan.sbr
+.\Release\dsdProc.sbr
+.\Release\dsdTree.sbr
+.\Release\reoApi.sbr
+.\Release\reoCore.sbr
+.\Release\reoProfile.sbr
+.\Release\reoSift.sbr
+.\Release\reoSwap.sbr
+.\Release\reoTest.sbr
+.\Release\reoTransfer.sbr
+.\Release\reoUnits.sbr
+.\Release\added.sbr
+.\Release\solver.sbr
+.\Release\msatActivity.sbr
+.\Release\msatClause.sbr
+.\Release\msatClauseVec.sbr
+.\Release\msatMem.sbr
+.\Release\msatOrderH.sbr
+.\Release\msatQueue.sbr
+.\Release\msatRead.sbr
+.\Release\msatSolverApi.sbr
+.\Release\msatSolverCore.sbr
+.\Release\msatSolverIo.sbr
+.\Release\msatSolverSearch.sbr
+.\Release\msatSort.sbr
+.\Release\msatVec.sbr
+.\Release\fraigApi.sbr
+.\Release\fraigCanon.sbr
+.\Release\fraigFanout.sbr
+.\Release\fraigFeed.sbr
+.\Release\fraigMan.sbr
+.\Release\fraigMem.sbr
+.\Release\fraigNode.sbr
+.\Release\fraigPrime.sbr
+.\Release\fraigSat.sbr
+.\Release\fraigTable.sbr
+.\Release\fraigUtil.sbr
+.\Release\fraigVec.sbr
+.\Release\csat_apis.sbr
+.\Release\fxu.sbr
+.\Release\fxuCreate.sbr
+.\Release\fxuHeapD.sbr
+.\Release\fxuHeapS.sbr
+.\Release\fxuList.sbr
+.\Release\fxuMatrix.sbr
+.\Release\fxuPair.sbr
+.\Release\fxuPrint.sbr
+.\Release\fxuReduce.sbr
+.\Release\fxuSelect.sbr
+.\Release\fxuSingle.sbr
+.\Release\fxuUpdate.sbr
+.\Release\rwrDec.sbr
+.\Release\rwrEva.sbr
+.\Release\rwrExp.sbr
+.\Release\rwrLib.sbr
+.\Release\rwrMan.sbr
+.\Release\rwrPrint.sbr
+.\Release\rwrUtil.sbr
+.\Release\cutApi.sbr
+.\Release\cutCut.sbr
+.\Release\cutMan.sbr
+.\Release\cutMerge.sbr
+.\Release\cutNode.sbr
+.\Release\cutOracle.sbr
+.\Release\cutSeq.sbr
+.\Release\cutTruth.sbr
+.\Release\decAbc.sbr
+.\Release\decFactor.sbr
+.\Release\decMan.sbr
+.\Release\decPrint.sbr
+.\Release\decUtil.sbr
+.\Release\simMan.sbr
+.\Release\simSat.sbr
+.\Release\simSeq.sbr
+.\Release\simSupp.sbr
+.\Release\simSwitch.sbr
+.\Release\simSym.sbr
+.\Release\simSymSat.sbr
+.\Release\simSymSim.sbr
+.\Release\simSymStr.sbr
+.\Release\simUtils.sbr
+.\Release\fpga.sbr
+.\Release\fpgaCore.sbr
+.\Release\fpgaCreate.sbr
+.\Release\fpgaCut.sbr
+.\Release\fpgaCutUtils.sbr
+.\Release\fpgaFanout.sbr
+.\Release\fpgaLib.sbr
+.\Release\fpgaMatch.sbr
+.\Release\fpgaSwitch.sbr
+.\Release\fpgaTime.sbr
+.\Release\fpgaTruth.sbr
+.\Release\fpgaUtils.sbr
+.\Release\fpgaVec.sbr
+.\Release\mapper.sbr
+.\Release\mapperCanon.sbr
+.\Release\mapperCore.sbr
+.\Release\mapperCreate.sbr
+.\Release\mapperCut.sbr
+.\Release\mapperCutUtils.sbr
+.\Release\mapperFanout.sbr
+.\Release\mapperLib.sbr
+.\Release\mapperMatch.sbr
+.\Release\mapperRefs.sbr
+.\Release\mapperSuper.sbr
+.\Release\mapperSwitch.sbr
+.\Release\mapperTable.sbr
+.\Release\mapperTime.sbr
+.\Release\mapperTree.sbr
+.\Release\mapperTruth.sbr
+.\Release\mapperUtils.sbr
+.\Release\mapperVec.sbr
+.\Release\mio.sbr
+.\Release\mioApi.sbr
+.\Release\mioFunc.sbr
+.\Release\mioRead.sbr
+.\Release\mioUtils.sbr
+.\Release\super.sbr
+.\Release\superAnd.sbr
+.\Release\superGate.sbr
+.\Release\superWrite.sbr
+.\Release\pgaCore.sbr
+.\Release\pgaMan.sbr
+.\Release\pgaMatch.sbr
+.\Release\pgaUtil.sbr
+.\Release\extraBddKmap.sbr
+.\Release\extraBddMisc.sbr
+.\Release\extraBddSymm.sbr
+.\Release\extraUtilBitMatrix.sbr
+.\Release\extraUtilCanon.sbr
+.\Release\extraUtilFile.sbr
+.\Release\extraUtilMemory.sbr
+.\Release\extraUtilMisc.sbr
+.\Release\extraUtilProgress.sbr
+.\Release\extraUtilReader.sbr
+.\Release\st.sbr
+.\Release\stmm.sbr
+.\Release\cpu_stats.sbr
+.\Release\cpu_time.sbr
+.\Release\datalimit.sbr
+.\Release\getopt.sbr
+.\Release\pathsearch.sbr
+.\Release\safe_mem.sbr
+.\Release\strsav.sbr
+.\Release\texpand.sbr
+.\Release\mvc.sbr
+.\Release\mvcApi.sbr
+.\Release\mvcCompare.sbr
+.\Release\mvcContain.sbr
+.\Release\mvcCover.sbr
+.\Release\mvcCube.sbr
+.\Release\mvcDivide.sbr
+.\Release\mvcDivisor.sbr
+.\Release\mvcList.sbr
+.\Release\mvcLits.sbr
+.\Release\mvcMan.sbr
+.\Release\mvcOpAlg.sbr
+.\Release\mvcOpBool.sbr
+.\Release\mvcPrint.sbr
+.\Release\mvcSort.sbr
+.\Release\mvcUtils.sbr]
+Creating command line "bscmake.exe @C:\DOCUME~1\alanmi\LOCALS~1\Temp\RSP1FA6.tmp"
+Creating browse info file...
+<h3>Output Window</h3>
 
 
 
diff --git a/abc.rc b/abc.rc
index 605f2b14..607946e3 100644
--- a/abc.rc
+++ b/abc.rc
@@ -71,9 +71,6 @@ alias resynl   "b; rw -l; rwz -l; b; rwz -l; b"
 alias resyn2   "b; rw; rf; b; rw; rwz; b; rfz; rwz; b"
 alias resyn2l  "b; rw -l; rf -l; b; rw -l; rwz -l; b; rfz -l; rwz -l; b"
 alias thin     "rwz; rfz; b; ps"
-alias reti     "st; seq; ret; unseq; st"
-alias retis    "st; seq; ret; unseq -s; st"
-alias choice   "fraig_store; resyn; fraig_store; resyn2; fraig_store; fraig_restore"
-alias stest    "st; ps; seq; ps; unseq; st; ps; sec"
-alias t        "r pan2.blif; st; seq; sfpga; sec"
+alias choice   "fsto; resynl; fsto; resyn2l; fsto; fres"
+alias t        "r iscas2/s3330_edf.blif; st; seq; smap"
 
diff --git a/src/base/abc/abcNtk.c b/src/base/abc/abcNtk.c
index 6fae871d..8383251a 100644
--- a/src/base/abc/abcNtk.c
+++ b/src/base/abc/abcNtk.c
@@ -235,8 +235,8 @@ Abc_Ntk_t * Abc_NtkStartRead( char * pName )
     // allocate the empty network
     pNtkNew = Abc_NtkAlloc( ABC_NTK_NETLIST, ABC_FUNC_SOP );
     // set the specs
-    pNtkNew->pName = util_strsav( pName );
-    pNtkNew->pSpec = util_strsav( pName );
+    pNtkNew->pName = util_strsav( Extra_FileNameGeneric(pName) );
+    pNtkNew->pSpec = util_strsav( Extra_FileNameGeneric(pName) );
     return pNtkNew;
 }
 
@@ -313,7 +313,11 @@ Abc_Ntk_t * Abc_NtkDup( Abc_Ntk_t * pNtk )
         // copy the nodes
         Abc_NtkForEachObj( pNtk, pObj, i )
             if ( pObj->pCopy == NULL )
+            {
                 Abc_NtkDupObj(pNtkNew, pObj);
+                pObj->pCopy->Level = pObj->Level;
+                pObj->pCopy->fPhase = pObj->fPhase;
+            }
         // connect the nodes
         Abc_NtkForEachObj( pNtk, pObj, i )
         {
diff --git a/src/base/abci/abc.c b/src/base/abci/abc.c
index db2d08a7..91adbabc 100644
--- a/src/base/abci/abc.c
+++ b/src/base/abci/abc.c
@@ -5100,17 +5100,16 @@ int Abc_CommandRetime( Abc_Frame_t * pAbc, int argc, char ** argv )
 
     if ( Abc_NtkHasAig(pNtk) )
     {
+        // quit if there are choice nodes
+        if ( Abc_NtkGetChoiceNum(pNtk) )
+        {
+            fprintf( pErr, "Currently cannot retime networks with choice nodes.\n" );
+            return 0;
+        }
         if ( Abc_NtkIsStrash(pNtk) )
             pNtkRes = Abc_NtkAigToSeq(pNtk);
         else
-        {
-            if ( Abc_NtkGetChoiceNum(pNtk) )
-            {
-                fprintf( pErr, "Currently cannot retime networks with choice nodes.\n" );
-                return 0;
-            }
             pNtkRes = Abc_NtkDup(pNtk);
-        }
         // retime the network
         if ( fForward )
             Seq_NtkSeqRetimeForward( pNtkRes, fInitial, fVerbose );
@@ -5118,11 +5117,13 @@ int Abc_CommandRetime( Abc_Frame_t * pAbc, int argc, char ** argv )
             Seq_NtkSeqRetimeBackward( pNtkRes, fInitial, fVerbose );
         else
             Seq_NtkSeqRetimeDelay( pNtkRes, nMaxIters, fInitial, fVerbose );
-        // convert from the sequential AIG
+        // if the network is an AIG, convert the result into an AIG
         if ( Abc_NtkIsStrash(pNtk) )
         {
             pNtkRes = Abc_NtkSeqToLogicSop( pNtkTemp = pNtkRes );
             Abc_NtkDelete( pNtkTemp );
+            pNtkRes = Abc_NtkStrash( pNtkTemp = pNtkRes, 0, 0 );
+            Abc_NtkDelete( pNtkTemp );
         }
     }
     else
@@ -5162,7 +5163,7 @@ usage:
 int Abc_CommandSeqFpga( Abc_Frame_t * pAbc, int argc, char ** argv )
 {
     FILE * pOut, * pErr;
-    Abc_Ntk_t * pNtk, * pNtkRes;
+    Abc_Ntk_t * pNtk, * pNtkNew, * pNtkRes;
     int c, nMaxIters;
     int fVerbose;
 
@@ -5205,26 +5206,65 @@ int Abc_CommandSeqFpga( Abc_Frame_t * pAbc, int argc, char ** argv )
         return 1;
     }
 
-    if ( !Abc_NtkIsSeq(pNtk) )
+    if ( Abc_NtkHasAig(pNtk) )
     {
-        fprintf( pErr, "Sequential FPGA mapping works only for sequential AIG (run \"seq\").\n" );
-        return 0;
+        // quit if there are choice nodes
+        if ( Abc_NtkGetChoiceNum(pNtk) )
+        {
+            fprintf( pErr, "Currently cannot map/retime networks with choice nodes.\n" );
+            return 0;
+        }
+        if ( Abc_NtkIsStrash(pNtk) )
+            pNtkNew = Abc_NtkAigToSeq(pNtk);
+        else
+            pNtkNew = Abc_NtkDup(pNtk);
+    }
+    else
+    {
+        // strash and balance the network
+        pNtkNew = Abc_NtkStrash( pNtk, 0, 0 );
+        if ( pNtkNew == NULL )
+        {
+            fprintf( pErr, "Strashing before FPGA mapping/retiming has failed.\n" );
+            return 1;
+        }
+
+        pNtkNew = Abc_NtkBalance( pNtkRes = pNtkNew, 0 );
+        Abc_NtkDelete( pNtkRes );
+        if ( pNtkNew == NULL )
+        {
+            fprintf( pErr, "Balancing before FPGA mapping has failed.\n" );
+            return 1;
+        }
+
+        // convert into a sequential AIG
+        pNtkNew = Abc_NtkAigToSeq( pNtkRes = pNtkNew );
+        Abc_NtkDelete( pNtkRes );
+        if ( pNtkNew == NULL )
+        {
+            fprintf( pErr, "Converting into a seq AIG before FPGA mapping/retiming has failed.\n" );
+            return 1;
+        }
+
+        fprintf( pOut, "The network was strashed and balanced before FPGA mapping/retiming.\n" );
     }
 
     // get the new network
-    pNtkRes = Seq_NtkFpgaMapRetime( pNtk, nMaxIters, fVerbose );
+    pNtkRes = Seq_NtkFpgaMapRetime( pNtkNew, nMaxIters, fVerbose );
     if ( pNtkRes == NULL )
     {
         fprintf( pErr, "Sequential FPGA mapping has failed.\n" );
+        Abc_NtkDelete( pNtkNew );
         return 0;
     }
+    Abc_NtkDelete( pNtkNew );
     // replace the current network
     Abc_FrameReplaceCurrentNetwork( pAbc, pNtkRes );
     return 0;
 
 usage:
     fprintf( pErr, "usage: sfpga [-I num] [-vh]\n" );
-    fprintf( pErr, "\t         performs integrated sequential FPGA mapping\n" );
+    fprintf( pErr, "\t         performs integrated sequential FPGA mapping/retiming\n" );
     fprintf( pErr, "\t-I num : max number of iterations of l-value computation [default = %d]\n", nMaxIters );
     fprintf( pErr, "\t-v     : toggle verbose output [default = %s]\n", fVerbose? "yes": "no" );
     fprintf( pErr, "\t-h     : print the command usage\n");
@@ -5245,7 +5285,7 @@ usage:
 int Abc_CommandSeqMap( Abc_Frame_t * pAbc, int argc, char ** argv )
 {
     FILE * pOut, * pErr;
-    Abc_Ntk_t * pNtk, * pNtkRes;
+    Abc_Ntk_t * pNtk, * pNtkNew, * pNtkRes;
     int c, nMaxIters;
     int fVerbose;
 
@@ -5255,7 +5295,7 @@ int Abc_CommandSeqMap( Abc_Frame_t * pAbc, int argc, char ** argv )
 
     // set defaults
     nMaxIters = 15;
-    fVerbose  =  1;
+    fVerbose  =  0;
     util_getopt_reset();
     while ( ( c = util_getopt( argc, argv, "Ivh" ) ) != EOF )
     {
@@ -5288,28 +5328,66 @@ int Abc_CommandSeqMap( Abc_Frame_t * pAbc, int argc, char ** argv )
         return 1;
     }
 
-    if ( !Abc_NtkIsSeq(pNtk) )
+    if ( Abc_NtkHasAig(pNtk) )
     {
-        fprintf( pErr, "Sequential standard cell mapping works only for sequential AIG (run \"seq\").\n" );
-        return 1;
+        // quit if there are choice nodes
+        if ( Abc_NtkGetChoiceNum(pNtk) )
+        {
+            fprintf( pErr, "Currently cannot map/retime networks with choice nodes.\n" );
+            return 0;
+        }
+        if ( Abc_NtkIsStrash(pNtk) )
+            pNtkNew = Abc_NtkAigToSeq(pNtk);
+        else
+            pNtkNew = Abc_NtkDup(pNtk);
+    }
+    else
+    {
+        // strash and balance the network
+        pNtkNew = Abc_NtkStrash( pNtk, 0, 0 );
+        if ( pNtkNew == NULL )
+        {
+            fprintf( pErr, "Strashing before SC mapping/retiming has failed.\n" );
+            return 1;
+        }
+
+        pNtkNew = Abc_NtkBalance( pNtkRes = pNtkNew, 0 );
+        Abc_NtkDelete( pNtkRes );
+        if ( pNtkNew == NULL )
+        {
+            fprintf( pErr, "Balancing before SC mapping/retiming has failed.\n" );
+            return 1;
+        }
+
+        // convert into a sequential AIG
+        pNtkNew = Abc_NtkAigToSeq( pNtkRes = pNtkNew );
+        Abc_NtkDelete( pNtkRes );
+        if ( pNtkNew == NULL )
+        {
+            fprintf( pErr, "Converting into a seq AIG before SC mapping/retiming has failed.\n" );
+            return 1;
+        }
+
+        fprintf( pOut, "The network was strashed and balanced before SC mapping/retiming.\n" );
     }
-//    printf( "This command is not yet implemented.\n" );
-//    return 0;
 
     // get the new network
-    pNtkRes = Seq_MapRetime( pNtk, nMaxIters, fVerbose );
+    pNtkRes = Seq_MapRetime( pNtkNew, nMaxIters, fVerbose );
     if ( pNtkRes == NULL )
     {
-        fprintf( pErr, "Sequential standard-cell mapping has failed.\n" );
+        fprintf( pErr, "Sequential FPGA mapping has failed.\n" );
+        Abc_NtkDelete( pNtkNew );
         return 1;
     }
+    Abc_NtkDelete( pNtkNew );
+
     // replace the current network
     Abc_FrameReplaceCurrentNetwork( pAbc, pNtkRes );
     return 0;
 
 usage:
     fprintf( pErr, "usage: smap [-I num] [-vh]\n" );
-    fprintf( pErr, "\t         performs integrated sequential standard-cell mapping" );
+    fprintf( pErr, "\t         performs integrated sequential standard-cell mapping/retiming\n" );
     fprintf( pErr, "\t-I num : max number of iterations of l-value computation [default = %d]\n", nMaxIters );
     fprintf( pErr, "\t-v     : toggle verbose output [default = %s]\n", fVerbose? "yes": "no" );
     fprintf( pErr, "\t-h     : print the command usage\n");
diff --git a/src/base/io/ioWriteDot.c b/src/base/io/ioWriteDot.c
index d00b265a..373c4636 100644
--- a/src/base/io/ioWriteDot.c
+++ b/src/base/io/ioWriteDot.c
@@ -26,6 +26,7 @@
 ////////////////////////////////////////////////////////////////////////
 
 static char * Abc_NtkPrintSop( char * pSop );
+static int    Abc_NtkCountLogicNodes( Vec_Ptr_t * vNodes );
 
 ////////////////////////////////////////////////////////////////////////
 ///                     FUNCTION DEFINITIONS                         ///
@@ -181,7 +182,7 @@ void Io_WriteDotAig( Abc_Ntk_t * pNtk, Vec_Ptr_t * vNodes, Vec_Ptr_t * vNodesSho
     fprintf( pFile, "          fontsize=18,\n" );
     fprintf( pFile, "          fontname = \"Times-Roman\",\n" );
     fprintf( pFile, "          label=\"" );
-    fprintf( pFile, "The set contains %d nodes and spans %d levels.", vNodes->nSize, LevelMax - LevelMin + 1 );
+    fprintf( pFile, "The set contains %d logic nodes and spans %d levels.", Abc_NtkCountLogicNodes(vNodes), LevelMax - LevelMin + 1 );
     fprintf( pFile, "\\n" );
     fprintf( pFile, "\"\n" );
     fprintf( pFile, "         ];\n" );
@@ -526,7 +527,7 @@ void Io_WriteDotNtk( Abc_Ntk_t * pNtk, Vec_Ptr_t * vNodes, Vec_Ptr_t * vNodesSho
     fprintf( pFile, "          fontsize=18,\n" );
     fprintf( pFile, "          fontname = \"Times-Roman\",\n" );
     fprintf( pFile, "          label=\"" );
-    fprintf( pFile, "The set contains %d nodes and spans %d levels.", vNodes->nSize, LevelMax - LevelMin + 1 );
+    fprintf( pFile, "The set contains %d logic nodes and spans %d levels.", Abc_NtkCountLogicNodes(vNodes), LevelMax - LevelMin + 1 );
     fprintf( pFile, "\\n" );
     fprintf( pFile, "\"\n" );
     fprintf( pFile, "         ];\n" );
@@ -701,6 +702,32 @@ char * Abc_NtkPrintSop( char * pSop )
     return Buffer;
 }
 
+/**Function*************************************************************
+
+  Synopsis    [Computes the printable SOP form.]
+
+  Description []
+  
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Abc_NtkCountLogicNodes( Vec_Ptr_t * vNodes )
+{
+    Abc_Obj_t * pObj;
+    int i, Counter = 0;
+    Vec_PtrForEachEntry( vNodes, pObj, i )
+    {
+        if ( !Abc_ObjIsNode(pObj) )
+            continue;
+        if ( Abc_ObjFaninNum(pObj) == 0 && Abc_ObjFanoutNum(pObj) == 0 )
+            continue;
+        Counter ++;
+    }
+    return Counter;
+}
+
 ////////////////////////////////////////////////////////////////////////
 ///                       END OF FILE                                ///
 ////////////////////////////////////////////////////////////////////////
diff --git a/src/base/seq/seq.h b/src/base/seq/seq.h
index a644303f..323466a0 100644
--- a/src/base/seq/seq.h
+++ b/src/base/seq/seq.h
@@ -67,7 +67,7 @@ extern bool            Abc_NtkSeqCheck( Abc_Ntk_t * pNtk );
 /*=== seqShare.c =============================================================*/
 extern void            Seq_NtkShareFanouts( Abc_Ntk_t * pNtk );
 extern void            Seq_NtkShareLatches( Abc_Ntk_t * pNtkNew, Abc_Ntk_t * pNtk );
-extern void            Seq_NtkShareLatchesFpga( Abc_Ntk_t * pNtkNew, Abc_Ntk_t * pNtk, Vec_Ptr_t * vMapAnds );
+extern void            Seq_NtkShareLatchesMapping( Abc_Ntk_t * pNtkNew, Abc_Ntk_t * pNtk, Vec_Ptr_t * vMapAnds, int fFpga );
 extern void            Seq_NtkShareLatchesClean( Abc_Ntk_t * pNtk );
 /*=== seqUtil.c ==============================================================*/
 extern char *          Seq_ObjFaninGetInitPrintable( Abc_Obj_t * pObj, int Edge );
@@ -78,6 +78,7 @@ extern int             Seq_NtkLatchNumShared( Abc_Ntk_t * pNtk );
 extern void            Seq_NtkLatchGetInitNums( Abc_Ntk_t * pNtk, int * pInits );
 extern int             Seq_NtkLatchGetEqualFaninNum( Abc_Ntk_t * pNtk );
 extern int             Seq_NtkCountNodesAboveLimit( Abc_Ntk_t * pNtk, int Limit );
+extern int             Seq_MapComputeAreaFlows( Abc_Ntk_t * pNtk, int fVerbose );
 
 ////////////////////////////////////////////////////////////////////////
 ///                       END OF FILE                                ///
diff --git a/src/base/seq/seqAigCore.c b/src/base/seq/seqAigCore.c
index 5dca2e86..9b1e69a5 100644
--- a/src/base/seq/seqAigCore.c
+++ b/src/base/seq/seqAigCore.c
@@ -815,14 +815,14 @@ Vec_Ptr_t * Abc_NtkUtilRetimingGetMoves( Abc_Ntk_t * pNtk, Vec_Int_t * vSteps, b
         if ( !fChange )
         {
             printf( "Warning: %d strange steps (a minor bug to be fixed later).\n", Vec_IntSize(vSteps) );
-/*            
+/*
             Vec_IntForEachEntry( vSteps, Number, i )
             {
                 RetStep = Seq_Int2RetStep( Number );
                 printf( "%d(%d) ", RetStep.iNode, RetStep.nLatches );
             }
             printf( "\n" );
-*/            
+*/
             break;
         }
     }
diff --git a/src/base/seq/seqFpgaCore.c b/src/base/seq/seqFpgaCore.c
index 030efd80..705f553d 100644
--- a/src/base/seq/seqFpgaCore.c
+++ b/src/base/seq/seqFpgaCore.c
@@ -82,6 +82,7 @@ Abc_Ntk_t * Seq_NtkFpgaMapRetime( Abc_Ntk_t * pNtk, int nMaxIters, int fVerbose
     // check the compatibility of initial states computed
     if ( RetValue = Seq_NtkFpgaInitCompatible( pNtkNew, fVerbose ) )
         printf( "The number of LUTs with incompatible edges = %d.\n", RetValue );
+
     // create the final mapped network
     pNtkMap = Seq_NtkSeqFpgaMapped( pNtkNew );
     Abc_NtkDelete( pNtkNew );
@@ -142,8 +143,6 @@ Abc_Ntk_t * Seq_NtkFpgaDup( Abc_Ntk_t * pNtk )
     // transfer the mapping info to the new manager
     Vec_PtrForEachEntry( p->vMapAnds, pObj, i )
     {
-        // convert the root node
-        Vec_PtrWriteEntry( p->vMapAnds, i, pObj->pCopy );
         // get the leaves of the cut
         vLeaves = Vec_VecEntry( p->vMapCuts, i );
         // convert the leaf nodes
@@ -151,13 +150,14 @@ Abc_Ntk_t * Seq_NtkFpgaDup( Abc_Ntk_t * pNtk )
         {
             SeqEdge = (unsigned)pLeaf;
             pLeaf = Abc_NtkObj( pNtk, SeqEdge >> 8 );
-//            Lag = (SeqEdge & 255);// + Seq_NodeGetLag(pObj) - Seq_NodeGetLag(pLeaf);
             Lag = (SeqEdge & 255) + Seq_NodeGetLag(pObj) - Seq_NodeGetLag(pLeaf);
             assert( Lag >= 0 );
             // translate the old leaf into the leaf in the new network
             Vec_PtrWriteEntry( vLeaves, k, (void *)((pLeaf->pCopy->Id << 8) | Lag) );
 //            printf( "%d -> %d\n", pLeaf->Id, pLeaf->pCopy->Id );
         }
+        // convert the root node
+        Vec_PtrWriteEntry( p->vMapAnds, i, pObj->pCopy );
     }
     pNew = pNtkNew->pManFunc;
     pNew->nVarsMax  = p->nVarsMax;
@@ -290,8 +290,9 @@ Abc_Ntk_t * Seq_NtkSeqFpgaMapped( Abc_Ntk_t * pNtk )
     // duplicate the nodes used in the mapping
     Vec_PtrForEachEntry( p->vMapAnds, pObj, i )
         pObj->pCopy = Abc_NtkCreateNode( pNtkMap );
+
     // create and share the latches
-    Seq_NtkShareLatchesFpga( pNtkMap, pNtk, p->vMapAnds );
+    Seq_NtkShareLatchesMapping( pNtkMap, pNtk, p->vMapAnds, 1 );
 
     // connect the nodes
     Vec_PtrForEachEntry( p->vMapAnds, pObj, i )
diff --git a/src/base/seq/seqFpgaIter.c b/src/base/seq/seqFpgaIter.c
index 9d4002bc..96874db3 100644
--- a/src/base/seq/seqFpgaIter.c
+++ b/src/base/seq/seqFpgaIter.c
@@ -73,6 +73,9 @@ p->timeCuts = clock() - clk;
     if ( fVerbose )
     Cut_ManPrintStats( p->pCutMan );
 
+    // compute area flows
+//    Seq_MapComputeAreaFlows( pNtk, fVerbose );
+
     // compute the delays
 clk = clock();
     Seq_AigRetimeDelayLags( pNtk, fVerbose );
@@ -170,6 +173,7 @@ Cut_Cut_t * Seq_FpgaMappingSelectCut( Abc_Obj_t * pAnd )
             if ( Abc_NodeIsTravIdCurrent(pFanin) )
                 continue;
             CostCur += (float)(1.0 / Abc_ObjFanoutNum(pFanin));
+//            CostCur += Seq_NodeGetFlow( pFanin );
         }
         if ( CostMin > CostCur )
         {
diff --git a/src/base/seq/seqInt.h b/src/base/seq/seqInt.h
index c0f3e907..5532b490 100644
--- a/src/base/seq/seqInt.h
+++ b/src/base/seq/seqInt.h
@@ -64,6 +64,7 @@ struct Abc_Seq_t_
     Cut_Man_t *         pCutMan;        // cut manager
     Map_SuperLib_t *    pSuperLib;      // the current supergate library
     // sequential arrival time computation
+    Vec_Int_t *         vAFlows;        // the area flow of each cut
     Vec_Int_t *         vLValues;       // the arrival times (L-Values of nodes)
     Vec_Int_t *         vLValuesN;      // the arrival times (L-Values of nodes)
     Vec_Str_t *         vLags;          // the lags of the mapped nodes
@@ -73,6 +74,7 @@ struct Abc_Seq_t_
     Vec_Ptr_t *         vMapAnds;       // nodes visible in the mapping 
     Vec_Vec_t *         vMapCuts;       // best cuts for each node 
     Vec_Vec_t *         vMapDelays;     // the delay of each fanin
+    Vec_Vec_t *         vMapFanins;     // the delay of each fanin
     // runtime stats
     int                 timeCuts;       // runtime to compute the cuts
     int                 timeDelay;      // runtime to compute the L-values
@@ -117,7 +119,8 @@ struct Seq_Match_t_ // 3 words
     unsigned            fCompl  :  1;   // the polarity of the AND gate
     unsigned            fCutInv :  1;   // the polarity of the cut
     unsigned            PolUse  :  2;   // the polarity use of this node
-    unsigned            uPhase  : 28;   // the phase assignment at the boundary
+    unsigned            uPhase  : 14;   // the phase assignment at the boundary
+    unsigned            uPhaseR : 14;   // the real phase assignment at the boundary
 };
 
 ////////////////////////////////////////////////////////////////////////
@@ -157,8 +160,11 @@ static inline float          Seq_NodeGetLValueP( Abc_Obj_t * pNode )
 static inline float          Seq_NodeGetLValueN( Abc_Obj_t * pNode )                 { return Abc_Int2Float( Vec_IntEntry( Seq_NodeLValuesN(pNode), (pNode)->Id ) );       }
 static inline void           Seq_NodeSetLValueP( Abc_Obj_t * pNode, float Value )    { Vec_IntWriteEntry( Seq_NodeLValues(pNode), (pNode)->Id, Abc_Float2Int(Value) );     }
 static inline void           Seq_NodeSetLValueN( Abc_Obj_t * pNode, float Value )    { Vec_IntWriteEntry( Seq_NodeLValuesN(pNode), (pNode)->Id, Abc_Float2Int(Value) );    }
-static inline int            Seq_NodeComputeLag( int LValue, int Fi )                { return (LValue + 1024*Fi)/Fi - 1024 - (int)(LValue % Fi == 0);     }
-static inline int            Seq_NodeComputeLagFloat( float LValue, float Fi )       { return ((int)ceil(LValue/Fi)) - 1;                                        }
+
+// reading area flows
+static inline Vec_Int_t *    Seq_NodeFlow( Abc_Obj_t * pNode )                       { return ((Abc_Seq_t *)(pNode)->pNtk->pManFunc)->vAFlows;                        }
+static inline float          Seq_NodeGetFlow( Abc_Obj_t * pNode )                    { return Abc_Int2Float( Vec_IntEntry( Seq_NodeFlow(pNode), (pNode)->Id ) );      }
+static inline void           Seq_NodeSetFlow( Abc_Obj_t * pNode, float Value )       { Vec_IntWriteEntry( Seq_NodeFlow(pNode), (pNode)->Id, Abc_Float2Int(Value) );   }
 
 // reading the contents of the lat
 static inline Abc_InitType_t Seq_LatInit( Seq_Lat_t * pLat )  { return ((unsigned)pLat->pPrev) & 3;                                 }
@@ -178,6 +184,8 @@ static inline char           Seq_NodeGetLag( Abc_Obj_t * pNode )
 static inline char           Seq_NodeGetLagN( Abc_Obj_t * pNode )                     { return Vec_StrEntry( Seq_NodeLagsN(pNode), (pNode)->Id );        }
 static inline void           Seq_NodeSetLag( Abc_Obj_t * pNode, char Value )          { Vec_StrWriteEntry( Seq_NodeLags(pNode), (pNode)->Id, (Value) );  }
 static inline void           Seq_NodeSetLagN( Abc_Obj_t * pNode, char Value )         { Vec_StrWriteEntry( Seq_NodeLagsN(pNode), (pNode)->Id, (Value) ); }
+static inline int            Seq_NodeComputeLag( int LValue, int Fi )                 { return (LValue + 1024*Fi)/Fi - 1024 - (int)(LValue % Fi == 0);     }
+static inline int            Seq_NodeComputeLagFloat( float LValue, float Fi )        { return ((int)ceil(LValue/Fi)) - 1;                                        }
 
 // phase usage
 static inline Vec_Str_t *    Seq_NodeUses( Abc_Obj_t * pNode )                        { return ((Abc_Seq_t *)(pNode)->pNtk->pManFunc)->vUses;            }
diff --git a/src/base/seq/seqMan.c b/src/base/seq/seqMan.c
index 7dae5b23..405eeb39 100644
--- a/src/base/seq/seqMan.c
+++ b/src/base/seq/seqMan.c
@@ -58,6 +58,7 @@ Abc_Seq_t * Seq_Create( Abc_Ntk_t * pNtk )
     p->vLValues  = Vec_IntStart( p->nSize ); 
     p->vLags     = Vec_StrStart( p->nSize ); 
     p->vLValuesN = Vec_IntStart( p->nSize ); 
+    p->vAFlows   = Vec_IntStart( p->nSize ); 
     p->vLagsN    = Vec_StrStart( p->nSize ); 
     p->vUses     = Vec_StrStart( p->nSize ); 
     return p;
@@ -84,6 +85,7 @@ void Seq_Resize( Abc_Seq_t * p, int nMaxId )
     Vec_IntFill( p->vLValues,  p->nSize, 0 ); 
     Vec_StrFill( p->vLags,     p->nSize, 0 ); 
     Vec_IntFill( p->vLValuesN, p->nSize, 0 ); 
+    Vec_IntFill( p->vAFlows,   p->nSize, 0 ); 
     Vec_StrFill( p->vLagsN,    p->nSize, 0 ); 
     Vec_StrFill( p->vUses,     p->nSize, 0 ); 
 }
@@ -102,21 +104,24 @@ void Seq_Resize( Abc_Seq_t * p, int nMaxId )
 ***********************************************************************/
 void Seq_Delete( Abc_Seq_t * p )
 {
-    if ( p->fStandCells )
+    if ( p->fStandCells && p->vMapAnds )
     {
         void * pVoid; int i;
         Vec_PtrForEachEntry( p->vMapAnds, pVoid, i )
             free( pVoid );
     }
-    if ( p->vMapAnds )  Vec_PtrFree( p->vMapAnds );  // the nodes used in the mapping
-    if ( p->vMapCuts )  Vec_VecFree( p->vMapCuts );  // the cuts used in the mapping
-    if ( p->vLValues )  Vec_IntFree( p->vLValues );  // the arrival times (L-Values of nodes)
-    if ( p->vLags )     Vec_StrFree( p->vLags );     // the lags of the mapped nodes
-    if ( p->vLValuesN ) Vec_IntFree( p->vLValuesN ); // the arrival times (L-Values of nodes)
-    if ( p->vLagsN )    Vec_StrFree( p->vLagsN );    // the lags of the mapped nodes
-    if ( p->vUses )     Vec_StrFree( p->vUses );     // the uses of phases
-    if ( p->vInits )    Vec_PtrFree( p->vInits );    // the initial values of the latches
-    if ( p->vNums )     Vec_IntFree( p->vNums );     // the numbers of latches
+    if ( p->vMapDelays )  Vec_VecFree( p->vMapDelays );  // the nodes used in the mapping
+    if ( p->vMapFanins )  Vec_VecFree( p->vMapFanins );  // the cuts used in the mapping
+    if ( p->vMapAnds )    Vec_PtrFree( p->vMapAnds );    // the nodes used in the mapping
+    if ( p->vMapCuts )    Vec_VecFree( p->vMapCuts );    // the cuts used in the mapping
+    if ( p->vLValues )    Vec_IntFree( p->vLValues );    // the arrival times (L-Values of nodes)
+    if ( p->vLags )       Vec_StrFree( p->vLags );       // the lags of the mapped nodes
+    if ( p->vLValuesN )   Vec_IntFree( p->vLValuesN );   // the arrival times (L-Values of nodes)
+    if ( p->vAFlows )     Vec_IntFree( p->vAFlows );     // the arrival times (L-Values of nodes)
+    if ( p->vLagsN )      Vec_StrFree( p->vLagsN );      // the lags of the mapped nodes
+    if ( p->vUses )       Vec_StrFree( p->vUses );       // the uses of phases
+    if ( p->vInits )      Vec_PtrFree( p->vInits );      // the initial values of the latches
+    if ( p->vNums )       Vec_IntFree( p->vNums );       // the numbers of latches
     Extra_MmFixedStop( p->pMmInits, 0 );
     free( p );
 }
diff --git a/src/base/seq/seqMapCore.c b/src/base/seq/seqMapCore.c
index 4f5a5e73..bbcc9a7c 100644
--- a/src/base/seq/seqMapCore.c
+++ b/src/base/seq/seqMapCore.c
@@ -33,13 +33,12 @@ extern Abc_Ntk_t *  Seq_NtkSeqMapMapped( Abc_Ntk_t * pNtk );
 
 static int          Seq_MapMappingCount( Abc_Ntk_t * pNtk );
 static int          Seq_MapMappingCount_rec( Abc_Ntk_t * pNtk, unsigned SeqEdge, Vec_Ptr_t * vLeaves );
-static Abc_Obj_t *  Seq_MapMappingBuild_rec( Abc_Ntk_t * pNtkNew, Abc_Ntk_t * pNtk, unsigned SeqEdge, int fTop, int LagCut, Vec_Ptr_t * vLeaves );
+static Abc_Obj_t *  Seq_MapMappingBuild_rec( Abc_Ntk_t * pNtkNew, Abc_Ntk_t * pNtk, unsigned SeqEdge, int fTop, int fCompl, int LagCut, Vec_Ptr_t * vLeaves, unsigned uPhase );
 static DdNode *     Seq_MapMappingBdd_rec( DdManager * dd, Abc_Ntk_t * pNtk, unsigned SeqEdge, Vec_Ptr_t * vLeaves );
 static void         Seq_MapMappingEdges_rec( Abc_Ntk_t * pNtk, unsigned SeqEdge, Abc_Obj_t * pPrev, Vec_Ptr_t * vLeaves, Vec_Vec_t * vMapEdges );
 static void         Seq_MapMappingConnect_rec( Abc_Ntk_t * pNtk, unsigned SeqEdge, Abc_Obj_t * pPrev, int Edge, Abc_Obj_t * pRoot, Vec_Ptr_t * vLeaves );
 static DdNode *     Seq_MapMappingConnectBdd_rec( Abc_Ntk_t * pNtk, unsigned SeqEdge, Abc_Obj_t * pPrev, int Edge, Abc_Obj_t * pRoot, Vec_Ptr_t * vLeaves );
 
-
 ////////////////////////////////////////////////////////////////////////
 ///                     FUNCTION DEFINITIONS                         ///
 ////////////////////////////////////////////////////////////////////////
@@ -81,25 +80,19 @@ Abc_Ntk_t * Seq_MapRetime( Abc_Ntk_t * pNtk, int nMaxIters, int fVerbose )
         printf( "The network has %d choices. Deriving the resulting network is skipped.\n", RetValue );
         return NULL;
     }
-    return NULL;
 
     // duplicate the nodes contained in multiple cuts
     pNtkNew = Seq_NtkMapDup( pNtk );
-//    return pNtkNew;
     
     // implement the retiming
     RetValue = Seq_NtkImplementRetiming( pNtkNew, ((Abc_Seq_t *)pNtkNew->pManFunc)->vLags, fVerbose );
     if ( RetValue == 0 )
         printf( "Retiming completed but initial state computation has failed.\n" );
-//    return pNtkNew;
 
     // check the compatibility of initial states computed
     if ( RetValue = Seq_NtkMapInitCompatible( pNtkNew, fVerbose ) )
-    {
         printf( "The number of LUTs with incompatible edges = %d.\n", RetValue );
-        Abc_NtkDelete( pNtkNew );
-        return NULL;
-    }
+//    return pNtkNew;
 
     // create the final mapped network
     pNtkMap = Seq_NtkSeqMapMapped( pNtkNew );
@@ -124,7 +117,7 @@ Abc_Ntk_t * Seq_NtkMapDup( Abc_Ntk_t * pNtk )
     Abc_Seq_t * pNew, * p = pNtk->pManFunc;
     Seq_Match_t * pMatch;
     Abc_Ntk_t * pNtkNew; 
-    Abc_Obj_t * pObj, * pLeaf, * pDriver, * pDriverNew;
+    Abc_Obj_t * pObj, * pFanin, * pFaninNew, * pLeaf;
     Vec_Ptr_t * vLeaves;
     unsigned SeqEdge;
     int i, k, nObjsNew, Lag;
@@ -133,7 +126,7 @@ Abc_Ntk_t * Seq_NtkMapDup( Abc_Ntk_t * pNtk )
 
     // start the expanded network
     pNtkNew = Abc_NtkStartFrom( pNtk, pNtk->ntkType, pNtk->ntkFunc );
-    Abc_NtkCleanNext( pNtk );
+    Abc_NtkCleanNext(pNtk);
 
     // start the new sequential AIG manager
     nObjsNew = 1 + Abc_NtkPiNum(pNtk) + Abc_NtkPoNum(pNtk) + Seq_MapMappingCount(pNtk);
@@ -141,25 +134,71 @@ Abc_Ntk_t * Seq_NtkMapDup( Abc_Ntk_t * pNtk )
 
     // duplicate the nodes in the mapping
     Vec_PtrForEachEntry( p->vMapAnds, pMatch, i )
-        if ( pMatch->fCompl )
-            pMatch->pAnd->pNext = Abc_NtkCreateNode( pNtkNew );
-        else
+    {
+//        Abc_NtkDupObj( pNtkNew, pMatch->pAnd );
+        if ( !pMatch->fCompl )
             pMatch->pAnd->pCopy = Abc_NtkCreateNode( pNtkNew );
+        else
+            pMatch->pAnd->pNext = Abc_NtkCreateNode( pNtkNew );
+    }
+
+    // compute the real phase assignment
+    Vec_PtrForEachEntry( p->vMapAnds, pMatch, i )
+    {
+        pMatch->uPhaseR = 0;
+        // get the leaves of the cut
+        vLeaves = Vec_VecEntry( p->vMapCuts, i );
+        // convert the leaf nodes
+        Vec_PtrForEachEntry( vLeaves, pLeaf, k )
+        {
+            SeqEdge = (unsigned)pLeaf;
+            pLeaf = Abc_NtkObj( pNtk, SeqEdge >> 8 );
+
+            // set the phase
+            if ( pMatch->uPhase & (1 << k) ) // neg is required
+            {
+                if ( pLeaf->pNext ) // neg is available
+                    pMatch->uPhaseR |= (1 << k); // neg is used
+//                else
+//                    Seq_NodeSetLag( pLeaf, Seq_NodeGetLagN(pLeaf) );
+            }
+            else // pos is required
+            {
+                if ( pLeaf->pCopy == NULL ) // pos is not available
+                    pMatch->uPhaseR |= (1 << k); // neg is used
+//                else
+//                    Seq_NodeSetLagN( pLeaf, Seq_NodeGetLag(pLeaf) );
+            }
+        }
+    }
+
 
     // recursively construct the internals of each node
-    Vec_PtrForEachEntry( p->vMapAnds, pObj, i )
+    Vec_PtrForEachEntry( p->vMapAnds, pMatch, i )
     {
+//        if ( pMatch->pSuper == NULL )
+//        {
+//            int x = 0;
+//        }
         vLeaves = Vec_VecEntry( p->vMapCuts, i );
-        Seq_MapMappingBuild_rec( pNtkNew, pNtk, pObj->Id << 8, 1, Seq_NodeGetLag(pObj), vLeaves );
+        if ( !pMatch->fCompl )
+            Seq_MapMappingBuild_rec( pNtkNew, pNtk, pMatch->pAnd->Id << 8, 1, pMatch->fCompl, Seq_NodeGetLag(pMatch->pAnd), vLeaves, pMatch->uPhaseR );
+        else
+            Seq_MapMappingBuild_rec( pNtkNew, pNtk, pMatch->pAnd->Id << 8, 1, pMatch->fCompl, Seq_NodeGetLagN(pMatch->pAnd), vLeaves, pMatch->uPhaseR );
     }
     assert( nObjsNew == pNtkNew->nObjs );
 
     // set the POs
-    Abc_NtkForEachCo( pNtk, pObj, i )
+//    Abc_NtkFinalize( pNtk, pNtkNew );
+    Abc_NtkForEachPo( pNtk, pObj, i )
     {
-        pDriver    = Abc_ObjFanin0(pObj);
-        pDriverNew = Abc_ObjFaninC0(pObj)? pDriver->pNext : pDriver->pCopy;
-        Abc_ObjAddFanin( pObj->pCopy, pDriverNew );
+        pFanin = Abc_ObjFanin0(pObj);
+        if ( Abc_ObjFaninC0(pObj) )
+            pFaninNew = pFanin->pNext ? pFanin->pNext : pFanin->pCopy;
+        else
+            pFaninNew = pFanin->pCopy ? pFanin->pCopy : pFanin->pNext;
+        pFaninNew = Abc_ObjNotCond( pFaninNew, Abc_ObjFaninC0(pObj) );
+        Abc_ObjAddFanin( pObj->pCopy, pFaninNew );
     }
 
     // duplicate the latches on the PO edges
@@ -169,9 +208,6 @@ Abc_Ntk_t * Seq_NtkMapDup( Abc_Ntk_t * pNtk )
     // transfer the mapping info to the new manager
     Vec_PtrForEachEntry( p->vMapAnds, pMatch, i )
     {
-        // convert the root node
-//        Vec_PtrWriteEntry( p->vMapAnds, i, pObj->pCopy );
-        pMatch->pAnd = pMatch->pAnd->pCopy;
         // get the leaves of the cut
         vLeaves = Vec_VecEntry( p->vMapCuts, i );
         // convert the leaf nodes
@@ -179,25 +215,46 @@ Abc_Ntk_t * Seq_NtkMapDup( Abc_Ntk_t * pNtk )
         {
             SeqEdge = (unsigned)pLeaf;
             pLeaf = Abc_NtkObj( pNtk, SeqEdge >> 8 );
-//            Lag = (SeqEdge & 255);// + Seq_NodeGetLag(pObj) - Seq_NodeGetLag(pLeaf);
-            Lag = (SeqEdge & 255) + Seq_NodeGetLag(pObj) - Seq_NodeGetLag(pLeaf);
+
+//            Lag = (SeqEdge & 255) + Seq_NodeGetLag(pMatch->pAnd) - Seq_NodeGetLag(pLeaf);
+            Lag = (SeqEdge & 255) + 
+                (pMatch->fCompl?                     Seq_NodeGetLagN(pMatch->pAnd) : Seq_NodeGetLag(pMatch->pAnd)) - 
+                (((pMatch->uPhaseR & (1 << k)) > 0)? Seq_NodeGetLagN(pLeaf)        : Seq_NodeGetLag(pLeaf)       );
+
             assert( Lag >= 0 );
+
+            // translate the old leaf into the leaf in the new network
+//            if ( pMatch->uPhase & (1 << k) ) // negative phase is required
+//                pFaninNew = pLeaf->pNext? pLeaf->pNext : pLeaf->pCopy;
+//            else // positive phase is required
+//                pFaninNew = pLeaf->pCopy? pLeaf->pCopy : pLeaf->pNext;
+
             // translate the old leaf into the leaf in the new network
-            Vec_PtrWriteEntry( vLeaves, k, (void *)((pLeaf->pCopy->Id << 8) | Lag) );
+            if ( pMatch->uPhaseR & (1 << k) ) // negative phase is required
+                pFaninNew = pLeaf->pNext;
+            else // positive phase is required
+                pFaninNew = pLeaf->pCopy;
+
+            Vec_PtrWriteEntry( vLeaves, k, (void *)((pFaninNew->Id << 8) | Lag) );
 //            printf( "%d -> %d\n", pLeaf->Id, pLeaf->pCopy->Id );
+
+            // UPDATE PHASE!!!   leaving only those bits that require inverters
         }
+        // convert the root node
+//        Vec_PtrWriteEntry( p->vMapAnds, i, pObj->pCopy );
+        pMatch->pAnd = pMatch->fCompl? pMatch->pAnd->pNext : pMatch->pAnd->pCopy;
     }
     pNew = pNtkNew->pManFunc;
-    pNew->nVarsMax  = p->nVarsMax;
-    pNew->vMapAnds  = p->vMapAnds;   p->vMapAnds  = NULL;
-    pNew->vMapCuts  = p->vMapCuts;   p->vMapCuts  = NULL;
+    pNew->nVarsMax    = p->nVarsMax;
+    pNew->vMapAnds    = p->vMapAnds;     p->vMapAnds    = NULL;
+    pNew->vMapCuts    = p->vMapCuts;     p->vMapCuts    = NULL;
+    pNew->fStandCells = p->fStandCells;  p->fStandCells = 0;
 
     if ( !Abc_NtkCheck( pNtkNew ) )
         fprintf( stdout, "Seq_NtkMapDup(): Network check has failed.\n" );
     return pNtkNew;
 }
 
-
 /**Function*************************************************************
 
   Synopsis    [Checks if the initial states are compatible.]
@@ -214,7 +271,82 @@ Abc_Ntk_t * Seq_NtkMapDup( Abc_Ntk_t * pNtk )
 ***********************************************************************/
 int Seq_NtkMapInitCompatible( Abc_Ntk_t * pNtk, int fVerbose )
 {
-    return 1;
+    Abc_Seq_t * p = pNtk->pManFunc;
+    Seq_Match_t * pMatch;
+    Abc_Obj_t * pAnd, * pLeaf, * pFanout0, * pFanout1;
+    Vec_Vec_t * vTotalEdges;
+    Vec_Ptr_t * vLeaves, * vEdges;
+    int i, k, m, Edge0, Edge1, nLatchAfter, nLatches1, nLatches2;
+    unsigned SeqEdge;
+    int CountBad = 0, CountAll = 0;
+
+    vTotalEdges = Vec_VecStart( p->nVarsMax );
+    // go through all the nodes (cuts) used in the mapping
+    Vec_PtrForEachEntry( p->vMapAnds, pMatch, i )
+    {
+        pAnd = pMatch->pAnd;
+//        printf( "*** Node %d.\n", pAnd->Id );
+
+        // get the cut of this gate
+        vLeaves = Vec_VecEntry( p->vMapCuts, i );
+
+        // get the edges pointing to the leaves
+        Vec_VecClear( vTotalEdges );
+        Seq_MapMappingEdges_rec( pNtk, pAnd->Id << 8, NULL, vLeaves, vTotalEdges );
+
+        // for each leaf, consider its edges
+        Vec_PtrForEachEntry( vLeaves, pLeaf, k )
+        {
+            SeqEdge = (unsigned)pLeaf;
+            pLeaf = Abc_NtkObj( pNtk, SeqEdge >> 8 );
+            nLatchAfter = SeqEdge & 255;
+            if ( nLatchAfter == 0 )
+                continue;
+
+            // go through the edges
+            vEdges = Vec_VecEntry( vTotalEdges, k );
+            pFanout0 = NULL;
+            Vec_PtrForEachEntry( vEdges, pFanout1, m )
+            {
+                Edge1    = Abc_ObjIsComplement(pFanout1);
+                pFanout1 = Abc_ObjRegular(pFanout1);
+//printf( "Fanin = %d. Fanout = %d.\n", pLeaf->Id, pFanout1->Id );
+
+                // make sure this is the same fanin
+                if ( Edge1 )
+                    assert( pLeaf == Abc_ObjFanin1(pFanout1) );
+                else
+                    assert( pLeaf == Abc_ObjFanin0(pFanout1) );
+
+                // save the first one
+                if ( pFanout0 == NULL )
+                {
+                    pFanout0 = pFanout1;
+                    Edge0    = Edge1;
+                    continue;
+                }
+                // compare the rings
+                // if they have different number of latches, this is the bug
+                nLatches1 = Seq_NodeCountLats(pFanout0, Edge0);
+                nLatches2 = Seq_NodeCountLats(pFanout1, Edge1);
+                assert( nLatches1 == nLatches2 );
+                assert( nLatches1 == nLatchAfter );
+                assert( nLatches1 > 0 );
+
+                // if they have different initial states, this is the problem
+                if ( !Seq_NodeCompareLats(pFanout0, Edge0, pFanout1, Edge1) )
+                {
+                    CountBad++;
+                    break;
+                }
+                CountAll++;
+            }
+        }
+    }
+    if ( fVerbose )
+        printf( "The number of pairs of edges checked = %d.\n", CountAll );
+    Vec_VecFree( vTotalEdges );
+    return CountBad;
 }
 
 /**Function*************************************************************
@@ -230,7 +362,65 @@ int Seq_NtkMapInitCompatible( Abc_Ntk_t * pNtk, int fVerbose )
 ***********************************************************************/
 Abc_Ntk_t * Seq_NtkSeqMapMapped( Abc_Ntk_t * pNtk )
 {
-    return NULL;
+    Abc_Seq_t * p = pNtk->pManFunc;
+    Seq_Match_t * pMatch;
+    Abc_Ntk_t * pNtkMap; 
+    Vec_Ptr_t * vLeaves;
+    Abc_Obj_t * pObj, * pLatch, * pFaninNew;
+    Seq_Lat_t * pRing;
+    int i;
+
+    assert( Abc_NtkIsSeq(pNtk) );
+
+    // start the network
+    pNtkMap = Abc_NtkStartFrom( pNtk, ABC_NTK_LOGIC, ABC_FUNC_BDD );
+
+    // duplicate the nodes used in the mapping
+    Vec_PtrForEachEntry( p->vMapAnds, pMatch, i )
+        pMatch->pAnd->pCopy = Abc_NtkCreateNode( pNtkMap );
+
+    // create and share the latches
+    Seq_NtkShareLatchesMapping( pNtkMap, pNtk, p->vMapAnds, 0 );
+
+    // connect the nodes
+    Vec_PtrForEachEntry( p->vMapAnds, pMatch, i )
+    {
+        pObj = pMatch->pAnd;
+        // get the leaves of this gate
+        vLeaves = Vec_VecEntry( p->vMapCuts, i );
+        // get the BDD of the node
+        pObj->pCopy->pData = Seq_MapMappingConnectBdd_rec( pNtk, pObj->Id << 8, NULL, -1, pObj, vLeaves );
+        Cudd_Ref( pObj->pCopy->pData );
+        // complement the BDD of the cut if it came from the opposite polarity choice cut
+//        if ( Vec_StrEntry(p->vPhase, i) )
+//            pObj->pCopy->pData = Cudd_Not( pObj->pCopy->pData );
+    }
+
+    // set the POs
+    Abc_NtkForEachPo( pNtk, pObj, i )
+    {
+        if ( pRing = Seq_NodeGetRing(pObj,0) )
+            pFaninNew = pRing->pLatch;
+        else
+            pFaninNew = Abc_ObjFanin0(pObj)->pCopy;
+        pFaninNew = Abc_ObjNotCond( pFaninNew, Abc_ObjFaninC0(pObj) );
+        Abc_ObjAddFanin( pObj->pCopy, pFaninNew );
+    }
+
+    // add the latches and their names
+    Abc_NtkAddDummyLatchNames( pNtkMap );
+    Abc_NtkForEachLatch( pNtkMap, pLatch, i )
+    {
+        Vec_PtrPush( pNtkMap->vCis, pLatch );
+        Vec_PtrPush( pNtkMap->vCos, pLatch );
+    }
+    // fix the problem with complemented and duplicated CO edges
+    Abc_NtkLogicMakeSimpleCos( pNtkMap, 1 );
+    // make the network minimum base
+    Abc_NtkMinimumBase( pNtkMap );
+    if ( !Abc_NtkCheck( pNtkMap ) )
+        fprintf( stdout, "Seq_NtkSeqFpgaMapped(): Network check has failed.\n" );
+    return pNtkMap;
 }
 
 
@@ -250,12 +440,12 @@ int Seq_MapMappingCount( Abc_Ntk_t * pNtk )
 {
     Abc_Seq_t * p = pNtk->pManFunc;
     Vec_Ptr_t * vLeaves;
-    Abc_Obj_t * pAnd;
+    Seq_Match_t * pMatch;
     int i, Counter = 0;
-    Vec_PtrForEachEntry( p->vMapAnds, pAnd, i )
+    Vec_PtrForEachEntry( p->vMapAnds, pMatch, i )
     {
         vLeaves = Vec_VecEntry( p->vMapCuts, i );
-        Counter += Seq_MapMappingCount_rec( pNtk, pAnd->Id << 8, vLeaves );
+        Counter += Seq_MapMappingCount_rec( pNtk, pMatch->pAnd->Id << 8, vLeaves );
     }
     return Counter;
 }
@@ -306,7 +496,7 @@ int Seq_MapMappingCount_rec( Abc_Ntk_t * pNtk, unsigned SeqEdge, Vec_Ptr_t * vLe
   SeeAlso     []
 
 ***********************************************************************/
-Abc_Obj_t * Seq_MapMappingBuild_rec( Abc_Ntk_t * pNtkNew, Abc_Ntk_t * pNtk, unsigned SeqEdge, int fTop, int LagCut, Vec_Ptr_t * vLeaves )
+Abc_Obj_t * Seq_MapMappingBuild_rec( Abc_Ntk_t * pNtkNew, Abc_Ntk_t * pNtk, unsigned SeqEdge, int fTop, int fCompl, int LagCut, Vec_Ptr_t * vLeaves, unsigned uPhase )
 {
     Abc_Obj_t * pObj, * pObjNew, * pLeaf, * pFaninNew0, * pFaninNew1;
     unsigned SeqEdge0, SeqEdge1;
@@ -317,7 +507,17 @@ Abc_Obj_t * Seq_MapMappingBuild_rec( Abc_Ntk_t * pNtkNew, Abc_Ntk_t * pNtk, unsi
     // if the node is the fanin of the cut, return
     Vec_PtrForEachEntry( vLeaves, pLeaf, i )
         if ( SeqEdge == (unsigned)pLeaf )
-            return pObj->pCopy;
+        {
+//            if ( uPhase & (1 << i) ) // negative phase is required
+//                return pObj->pNext? pObj->pNext : pObj->pCopy;
+//            else // positive phase is required
+//                return pObj->pCopy? pObj->pCopy : pObj->pNext;
+
+            if ( uPhase & (1 << i) ) // negative phase is required
+                return pObj->pNext;
+            else // positive phase is required
+                return pObj->pCopy;
+        }
     // continue unfolding
     assert( Abc_NodeIsAigAnd(pObj) );
     // get new sequential edges
@@ -326,10 +526,10 @@ Abc_Obj_t * Seq_MapMappingBuild_rec( Abc_Ntk_t * pNtkNew, Abc_Ntk_t * pNtk, unsi
     SeqEdge0 = (Abc_ObjFanin0(pObj)->Id << 8) + Lag + Seq_ObjFaninL0(pObj);
     SeqEdge1 = (Abc_ObjFanin1(pObj)->Id << 8) + Lag + Seq_ObjFaninL1(pObj);
     // call for the children    
-    pObjNew = fTop? pObj->pCopy : Abc_NtkCreateNode( pNtkNew );
+    pObjNew = fTop? (fCompl? pObj->pNext : pObj->pCopy) : Abc_NtkCreateNode( pNtkNew );
     // solve subproblems
-    pFaninNew0 = Seq_MapMappingBuild_rec( pNtkNew, pNtk, SeqEdge0, 0, LagCut, vLeaves );
-    pFaninNew1 = Seq_MapMappingBuild_rec( pNtkNew, pNtk, SeqEdge1, 0, LagCut, vLeaves );
+    pFaninNew0 = Seq_MapMappingBuild_rec( pNtkNew, pNtk, SeqEdge0, 0, fCompl, LagCut, vLeaves, uPhase );
+    pFaninNew1 = Seq_MapMappingBuild_rec( pNtkNew, pNtk, SeqEdge1, 0, fCompl, LagCut, vLeaves, uPhase );
     // add the fanins to the node
     Abc_ObjAddFanin( pObjNew, Abc_ObjNotCond( pFaninNew0, Abc_ObjFaninC0(pObj) ) );
     Abc_ObjAddFanin( pObjNew, Abc_ObjNotCond( pFaninNew1, Abc_ObjFaninC1(pObj) ) );
@@ -342,6 +542,109 @@ Abc_Obj_t * Seq_MapMappingBuild_rec( Abc_Ntk_t * pNtkNew, Abc_Ntk_t * pNtk, unsi
 }
 
 
+/**Function*************************************************************
+
+  Synopsis    [Collects the edges pointing to the leaves of the cut.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Seq_MapMappingEdges_rec( Abc_Ntk_t * pNtk, unsigned SeqEdge, Abc_Obj_t * pPrev, Vec_Ptr_t * vLeaves, Vec_Vec_t * vMapEdges )
+{
+    Abc_Obj_t * pObj, * pLeaf;
+    unsigned SeqEdge0, SeqEdge1;
+    int Lag, i;
+    // get the object and the lag
+    pObj = Abc_NtkObj( pNtk, SeqEdge >> 8 );
+    Lag  = SeqEdge & 255;
+    // if the node is the fanin of the cut, return
+    Vec_PtrForEachEntry( vLeaves, pLeaf, i )
+    {
+        if ( SeqEdge == (unsigned)pLeaf )
+        {
+            assert( pPrev != NULL );
+            Vec_VecPush( vMapEdges, i, pPrev );
+            return;
+        }
+    }
+    // continue unfolding
+    assert( Abc_NodeIsAigAnd(pObj) );
+    // get new sequential edges
+    assert( Lag + Seq_ObjFaninL0(pObj) < 255 );
+    assert( Lag + Seq_ObjFaninL1(pObj) < 255 );
+    SeqEdge0 = (Abc_ObjFanin0(pObj)->Id << 8) + Lag + Seq_ObjFaninL0(pObj);
+    SeqEdge1 = (Abc_ObjFanin1(pObj)->Id << 8) + Lag + Seq_ObjFaninL1(pObj);
+    // call for the children    
+    Seq_MapMappingEdges_rec( pNtk, SeqEdge0, pObj            , vLeaves, vMapEdges );
+    Seq_MapMappingEdges_rec( pNtk, SeqEdge1, Abc_ObjNot(pObj), vLeaves, vMapEdges );
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Collects the edges pointing to the leaves of the cut.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+DdNode * Seq_MapMappingConnectBdd_rec( Abc_Ntk_t * pNtk, unsigned SeqEdge, Abc_Obj_t * pPrev, int Edge, Abc_Obj_t * pRoot, Vec_Ptr_t * vLeaves )
+{
+    Seq_Lat_t * pRing;
+    Abc_Obj_t * pObj, * pLeaf, * pFanin, * pFaninNew;
+    unsigned SeqEdge0, SeqEdge1;
+    DdManager * dd = pRoot->pCopy->pNtk->pManFunc;
+    DdNode * bFunc, * bFunc0, * bFunc1;
+    int Lag, i, k;
+    // get the object and the lag
+    pObj = Abc_NtkObj( pNtk, SeqEdge >> 8 );
+    Lag  = SeqEdge & 255;
+    // if the node is the fanin of the cut, add the connection and return
+    Vec_PtrForEachEntry( vLeaves, pLeaf, i )
+    {
+        if ( SeqEdge == (unsigned)pLeaf )
+        {
+            assert( pPrev != NULL );
+            if ( pRing = Seq_NodeGetRing(pPrev,Edge) )
+                pFaninNew = pRing->pLatch;
+            else
+                pFaninNew = Abc_ObjFanin(pPrev,Edge)->pCopy;
+
+            // check if the root already has this fanin
+            Abc_ObjForEachFanin( pRoot->pCopy, pFanin, k )
+                if ( pFanin == pFaninNew )
+                    return Cudd_bddIthVar( dd, k );
+            Abc_ObjAddFanin( pRoot->pCopy, pFaninNew );
+            return Cudd_bddIthVar( dd, k );
+        }
+    }
+    // continue unfolding
+    assert( Abc_NodeIsAigAnd(pObj) );
+    // get new sequential edges
+    assert( Lag + Seq_ObjFaninL0(pObj) < 255 );
+    assert( Lag + Seq_ObjFaninL1(pObj) < 255 );
+    SeqEdge0 = (Abc_ObjFanin0(pObj)->Id << 8) + Lag + Seq_ObjFaninL0(pObj);
+    SeqEdge1 = (Abc_ObjFanin1(pObj)->Id << 8) + Lag + Seq_ObjFaninL1(pObj);
+    // call for the children    
+    bFunc0 = Seq_MapMappingConnectBdd_rec( pNtk, SeqEdge0, pObj, 0, pRoot, vLeaves );    Cudd_Ref( bFunc0 );
+    bFunc1 = Seq_MapMappingConnectBdd_rec( pNtk, SeqEdge1, pObj, 1, pRoot, vLeaves );    Cudd_Ref( bFunc1 );
+    bFunc0 = Cudd_NotCond( bFunc0, Abc_ObjFaninC0(pObj) );
+    bFunc1 = Cudd_NotCond( bFunc1, Abc_ObjFaninC1(pObj) );
+    // get the BDD of the node
+    bFunc  = Cudd_bddAnd( dd, bFunc0, bFunc1 );  Cudd_Ref( bFunc );
+    Cudd_RecursiveDeref( dd, bFunc0 );
+    Cudd_RecursiveDeref( dd, bFunc1 );
+    // return the BDD
+    Cudd_Deref( bFunc );
+    return bFunc;
+}
+
 ////////////////////////////////////////////////////////////////////////
 ///                       END OF FILE                                ///
 ////////////////////////////////////////////////////////////////////////
diff --git a/src/base/seq/seqMapCore_old.c b/src/base/seq/seqMapCore_old.c
new file mode 100644
index 00000000..cc31de10
--- /dev/null
+++ b/src/base/seq/seqMapCore_old.c
@@ -0,0 +1,361 @@
+/**CFile****************************************************************
+
+  FileName    [seqMapCore.c]
+
+  SystemName  [ABC: Logic synthesis and verification system.]
+
+  PackageName [Construction and manipulation of sequential AIGs.]
+
+  Synopsis    [The core of SC mapping/retiming package.]
+
+  Author      [Alan Mishchenko]
+  
+  Affiliation [UC Berkeley]
+
+  Date        [Ver. 1.0. Started - June 20, 2005.]
+
+  Revision    [$Id: seqMapCore.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
+
+***********************************************************************/
+
+#include "seqInt.h"
+#include "main.h"
+#include "mio.h"
+#include "mapper.h"
+
+////////////////////////////////////////////////////////////////////////
+///                        DECLARATIONS                              ///
+////////////////////////////////////////////////////////////////////////
+
+extern Abc_Ntk_t *  Seq_NtkMapDup( Abc_Ntk_t * pNtk );
+extern int          Seq_NtkMapInitCompatible( Abc_Ntk_t * pNtk, int fVerbose );
+extern Abc_Ntk_t *  Seq_NtkSeqMapMapped( Abc_Ntk_t * pNtk );
+
+static int          Seq_MapMappingCount( Abc_Ntk_t * pNtk );
+static int          Seq_MapMappingCount_rec( Abc_Ntk_t * pNtk, unsigned SeqEdge, Vec_Ptr_t * vLeaves );
+static Abc_Obj_t *  Seq_MapMappingBuild_rec( Abc_Ntk_t * pNtkNew, Abc_Ntk_t * pNtk, unsigned SeqEdge, int fTop, int fCompl, int LagCut, Vec_Ptr_t * vLeaves, unsigned uPhase );
+static DdNode *     Seq_MapMappingBdd_rec( DdManager * dd, Abc_Ntk_t * pNtk, unsigned SeqEdge, Vec_Ptr_t * vLeaves );
+static void         Seq_MapMappingEdges_rec( Abc_Ntk_t * pNtk, unsigned SeqEdge, Abc_Obj_t * pPrev, Vec_Ptr_t * vLeaves, Vec_Vec_t * vMapEdges );
+static void         Seq_MapMappingConnect_rec( Abc_Ntk_t * pNtk, unsigned SeqEdge, Abc_Obj_t * pPrev, int Edge, Abc_Obj_t * pRoot, Vec_Ptr_t * vLeaves );
+static DdNode *     Seq_MapMappingConnectBdd_rec( Abc_Ntk_t * pNtk, unsigned SeqEdge, Abc_Obj_t * pPrev, int Edge, Abc_Obj_t * pRoot, Vec_Ptr_t * vLeaves );
+
+
+////////////////////////////////////////////////////////////////////////
+///                     FUNCTION DEFINITIONS                         ///
+////////////////////////////////////////////////////////////////////////
+
+/**Function*************************************************************
+
+  Synopsis    [Performs Map mapping and retiming.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Abc_Ntk_t * Seq_MapRetime( Abc_Ntk_t * pNtk, int nMaxIters, int fVerbose )
+{
+    Abc_Seq_t * p = pNtk->pManFunc;
+    Abc_Ntk_t * pNtkNew;
+    Abc_Ntk_t * pNtkMap;
+    int RetValue;
+
+    // derive the supergate library
+    if ( Abc_FrameReadLibSuper() == NULL && Abc_FrameReadLibGen() )
+    {
+        printf( "A simple supergate library is derived from gate library \"%s\".\n", 
+            Mio_LibraryReadName(Abc_FrameReadLibGen()) );
+        Map_SuperLibDeriveFromGenlib( Abc_FrameReadLibGen() );
+    }
+    p->pSuperLib   = Abc_FrameReadLibSuper();
+    p->nVarsMax    = Map_SuperLibReadVarsMax(p->pSuperLib);
+    p->nMaxIters   = nMaxIters;
+    p->fStandCells = 1;
+
+    // find the best mapping and retiming for all nodes (p->vLValues, p->vBestCuts, p->vLags)
+    Seq_MapRetimeDelayLags( pNtk, fVerbose );
+    if ( RetValue = Abc_NtkGetChoiceNum(pNtk) )
+    {
+        printf( "The network has %d choices. Deriving the resulting network is skipped.\n", RetValue );
+        return NULL;
+    }
+
+    // duplicate the nodes contained in multiple cuts
+    pNtkNew = Seq_NtkMapDup( pNtk );
+    return pNtkNew;
+    
+    // implement the retiming
+    RetValue = Seq_NtkImplementRetiming( pNtkNew, ((Abc_Seq_t *)pNtkNew->pManFunc)->vLags, fVerbose );
+    if ( RetValue == 0 )
+        printf( "Retiming completed but initial state computation has failed.\n" );
+//    return pNtkNew;
+
+    // check the compatibility of initial states computed
+    if ( RetValue = Seq_NtkMapInitCompatible( pNtkNew, fVerbose ) )
+    {
+        printf( "The number of LUTs with incompatible edges = %d.\n", RetValue );
+        Abc_NtkDelete( pNtkNew );
+        return NULL;
+    }
+
+    // create the final mapped network
+    pNtkMap = Seq_NtkSeqMapMapped( pNtkNew );
+    Abc_NtkDelete( pNtkNew );
+    return pNtkMap;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Derives the network by duplicating some of the nodes.]
+
+  Description [Information about mapping is given as mapping nodes (p->vMapAnds)
+  and best cuts for each node (p->vMapCuts).]
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Abc_Ntk_t * Seq_NtkMapDup( Abc_Ntk_t * pNtk )
+{
+    Abc_Seq_t * pNew, * p = pNtk->pManFunc;
+    Seq_Match_t * pMatch;
+    Abc_Ntk_t * pNtkNew; 
+    Abc_Obj_t * pObj, * pFanin, * pFaninNew, * pLeaf;
+    Vec_Ptr_t * vLeaves;
+    unsigned SeqEdge;
+    int i, k, nObjsNew, Lag;
+    
+    assert( Abc_NtkIsSeq(pNtk) );
+
+    // start the expanded network
+    pNtkNew = Abc_NtkStartFrom( pNtk, pNtk->ntkType, pNtk->ntkFunc );
+    Abc_NtkCleanNext(pNtk);
+
+    // start the new sequential AIG manager
+    nObjsNew = 1 + Abc_NtkPiNum(pNtk) + Abc_NtkPoNum(pNtk) + Seq_MapMappingCount(pNtk);
+    Seq_Resize( pNtkNew->pManFunc, nObjsNew );
+
+    // duplicate the nodes in the mapping
+    Vec_PtrForEachEntry( p->vMapAnds, pMatch, i )
+    {
+//        Abc_NtkDupObj( pNtkNew, pMatch->pAnd );
+        if ( !pMatch->fCompl )
+            pMatch->pAnd->pCopy = Abc_NtkCreateNode( pNtkNew );
+        else
+            pMatch->pAnd->pNext = Abc_NtkCreateNode( pNtkNew );
+    }
+
+    // recursively construct the internals of each node
+    Vec_PtrForEachEntry( p->vMapAnds, pMatch, i )
+    {
+        vLeaves = Vec_VecEntry( p->vMapCuts, i );
+        Seq_MapMappingBuild_rec( pNtkNew, pNtk, pMatch->pAnd->Id << 8, 1, pMatch->fCompl, Seq_NodeGetLag(pMatch->pAnd), vLeaves, pMatch->uPhase );
+    }
+    assert( nObjsNew == pNtkNew->nObjs );
+
+    // set the POs
+//    Abc_NtkFinalize( pNtk, pNtkNew );
+    Abc_NtkForEachPo( pNtk, pObj, i )
+    {
+        pFanin = Abc_ObjFanin0(pObj);
+        if ( Abc_ObjFaninC0(pObj) )
+            pFaninNew = pFanin->pNext ? pFanin->pNext : Abc_ObjNot(pFanin->pCopy);
+        else
+            pFaninNew = pFanin->pCopy ? pFanin->pCopy : Abc_ObjNot(pFanin->pNext);
+        Abc_ObjAddFanin( pObj->pCopy, pFaninNew );
+    }
+
+    // duplicate the latches on the PO edges
+    Abc_NtkForEachPo( pNtk, pObj, i )
+        Seq_NodeDupLats( pObj->pCopy, pObj, 0 );
+
+    // transfer the mapping info to the new manager
+    Vec_PtrForEachEntry( p->vMapAnds, pMatch, i )
+    {
+        // get the leaves of the cut
+        vLeaves = Vec_VecEntry( p->vMapCuts, i );
+        // convert the leaf nodes
+        Vec_PtrForEachEntry( vLeaves, pLeaf, k )
+        {
+            SeqEdge = (unsigned)pLeaf;
+            pLeaf = Abc_NtkObj( pNtk, SeqEdge >> 8 );
+            Lag = (SeqEdge & 255) + Seq_NodeGetLag(pMatch->pAnd) - Seq_NodeGetLag(pLeaf);
+            assert( Lag >= 0 );
+            // translate the old leaf into the leaf in the new network
+//            Vec_PtrWriteEntry( vLeaves, k, (void *)((pLeaf->pCopy->Id << 8) | Lag) );
+
+//            printf( "%d -> %d\n", pLeaf->Id, pLeaf->pCopy->Id );
+        }
+        // convert the root node
+//        Vec_PtrWriteEntry( p->vMapAnds, i, pObj->pCopy );
+        pMatch->pAnd = pMatch->pAnd->pCopy;
+    }
+    pNew = pNtkNew->pManFunc;
+    pNew->nVarsMax  = p->nVarsMax;
+    pNew->vMapAnds  = p->vMapAnds;   p->vMapAnds  = NULL;
+    pNew->vMapCuts  = p->vMapCuts;   p->vMapCuts  = NULL;
+
+    if ( !Abc_NtkCheck( pNtkNew ) )
+        fprintf( stdout, "Seq_NtkMapDup(): Network check has failed.\n" );
+    return pNtkNew;
+}
+
+
+/**Function*************************************************************
+
+  Synopsis    [Checks if the initial states are compatible.]
+
+  Description [Checks of all the initial states on the fanins edges
+  of the cut have compatible number of latches and initial states.
+  If this is not true, then the mapped network with the does not have initial 
+  state. Returns the number of LUTs with incompatible edges.]
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Seq_NtkMapInitCompatible( Abc_Ntk_t * pNtk, int fVerbose )
+{
+    return 1;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Derives the final mapped network.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Abc_Ntk_t * Seq_NtkSeqMapMapped( Abc_Ntk_t * pNtk )
+{
+    return NULL;
+}
+
+
+
+/**Function*************************************************************
+
+  Synopsis    [Counts the number of nodes in the bag.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Seq_MapMappingCount( Abc_Ntk_t * pNtk )
+{
+    Abc_Seq_t * p = pNtk->pManFunc;
+    Vec_Ptr_t * vLeaves;
+    Seq_Match_t * pMatch;
+    int i, Counter = 0;
+    Vec_PtrForEachEntry( p->vMapAnds, pMatch, i )
+    {
+        vLeaves = Vec_VecEntry( p->vMapCuts, i );
+        Counter += Seq_MapMappingCount_rec( pNtk, pMatch->pAnd->Id << 8, vLeaves );
+    }
+    return Counter;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Counts the number of nodes in the bag.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Seq_MapMappingCount_rec( Abc_Ntk_t * pNtk, unsigned SeqEdge, Vec_Ptr_t * vLeaves )
+{
+    Abc_Obj_t * pObj, * pLeaf;
+    unsigned SeqEdge0, SeqEdge1;
+    int Lag, i;
+    // get the object and the lag
+    pObj = Abc_NtkObj( pNtk, SeqEdge >> 8 );
+    Lag  = SeqEdge & 255;
+    // if the node is the fanin of the cut, return
+    Vec_PtrForEachEntry( vLeaves, pLeaf, i )
+        if ( SeqEdge == (unsigned)pLeaf )
+            return 0;
+    // continue unfolding
+    assert( Abc_NodeIsAigAnd(pObj) );
+    // get new sequential edges
+    assert( Lag + Seq_ObjFaninL0(pObj) < 255 );
+    assert( Lag + Seq_ObjFaninL1(pObj) < 255 );
+    SeqEdge0 = (Abc_ObjFanin0(pObj)->Id << 8) + Lag + Seq_ObjFaninL0(pObj);
+    SeqEdge1 = (Abc_ObjFanin1(pObj)->Id << 8) + Lag + Seq_ObjFaninL1(pObj);
+    // call for the children
+    return 1 + Seq_MapMappingCount_rec( pNtk, SeqEdge0, vLeaves ) + 
+        Seq_MapMappingCount_rec( pNtk, SeqEdge1, vLeaves );
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Collects the edges pointing to the leaves of the cut.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Abc_Obj_t * Seq_MapMappingBuild_rec( Abc_Ntk_t * pNtkNew, Abc_Ntk_t * pNtk, unsigned SeqEdge, int fTop, int fCompl, int LagCut, Vec_Ptr_t * vLeaves, unsigned uPhase )
+{
+    Abc_Obj_t * pObj, * pObjNew, * pLeaf, * pFaninNew0, * pFaninNew1;
+    unsigned SeqEdge0, SeqEdge1;
+    int Lag, i;
+    // get the object and the lag
+    pObj = Abc_NtkObj( pNtk, SeqEdge >> 8 );
+    Lag  = SeqEdge & 255;
+    // if the node is the fanin of the cut, return
+    Vec_PtrForEachEntry( vLeaves, pLeaf, i )
+        if ( SeqEdge == (unsigned)pLeaf )
+        {
+//            if ( uPhase & (1 << i) ) // negative phase is required
+//                return pObj->pNext? pObj->pNext : Abc_ObjNot(pObj->pCopy);
+//            else // positive phase is required
+//                return pObj->pCopy? pObj->pCopy : Abc_ObjNot(pObj->pNext);
+            return pObj->pCopy? pObj->pCopy : Abc_ObjNot(pObj->pNext);
+        }
+    // continue unfolding
+    assert( Abc_NodeIsAigAnd(pObj) );
+    // get new sequential edges
+    assert( Lag + Seq_ObjFaninL0(pObj) < 255 );
+    assert( Lag + Seq_ObjFaninL1(pObj) < 255 );
+    SeqEdge0 = (Abc_ObjFanin0(pObj)->Id << 8) + Lag + Seq_ObjFaninL0(pObj);
+    SeqEdge1 = (Abc_ObjFanin1(pObj)->Id << 8) + Lag + Seq_ObjFaninL1(pObj);
+    // call for the children    
+    pObjNew = fTop? (fCompl? pObj->pNext : pObj->pCopy) : Abc_NtkCreateNode( pNtkNew );
+    // solve subproblems
+    pFaninNew0 = Seq_MapMappingBuild_rec( pNtkNew, pNtk, SeqEdge0, 0, fCompl, LagCut, vLeaves, uPhase );
+    pFaninNew1 = Seq_MapMappingBuild_rec( pNtkNew, pNtk, SeqEdge1, 0, fCompl, LagCut, vLeaves, uPhase );
+    // add the fanins to the node
+    Abc_ObjAddFanin( pObjNew, Abc_ObjNotCond( pFaninNew0, Abc_ObjFaninC0(pObj) ) );
+    Abc_ObjAddFanin( pObjNew, Abc_ObjNotCond( pFaninNew1, Abc_ObjFaninC1(pObj) ) );
+    Seq_NodeDupLats( pObjNew, pObj, 0 );
+    Seq_NodeDupLats( pObjNew, pObj, 1 );
+    // set the lag of the new node equal to the internal lag plus mapping/retiming lag
+    Seq_NodeSetLag( pObjNew, (char)(Lag + LagCut) );
+//    Seq_NodeSetLag( pObjNew, (char)(Lag) );
+    return pObjNew;
+}
+
+
+////////////////////////////////////////////////////////////////////////
+///                       END OF FILE                                ///
+////////////////////////////////////////////////////////////////////////
+
+
diff --git a/src/base/seq/seqMapIter.c b/src/base/seq/seqMapIter.c
index 284fd27d..b93e5dbe 100644
--- a/src/base/seq/seqMapIter.c
+++ b/src/base/seq/seqMapIter.c
@@ -75,11 +75,18 @@ p->timeCuts = clock() - clk;
     // compute canonical forms of the truth tables of the cuts
     Seq_MapCanonicizeTruthTables( pNtk );
 
+    // compute area flows
+//    Seq_MapComputeAreaFlows( pNtk, fVerbose );
+
     // compute the delays
 clk = clock();
     FiBest = Seq_MapRetimeDelayLagsInternal( pNtk, fVerbose );
 p->timeDelay = clock() - clk;
 
+    // clean the marks
+    Abc_NtkForEachObj( pNtk, pObj, i )
+        assert( !pObj->fMarkA && !pObj->fMarkB );
+
     // collect the nodes and cuts used in the mapping
     p->vMapAnds = Vec_PtrAlloc( 1000 );
     p->vMapCuts = Vec_VecAlloc( 1000 );
@@ -133,7 +140,7 @@ float Seq_MapRetimeDelayLagsInternal( Abc_Ntk_t * pNtk, int fVerbose )
     }
 
     // get the upper bound on the clock period
-    FiMax = Delta * (2 + Seq_NtkLevelMax(pNtk));
+    FiMax = Delta * (5 + Seq_NtkLevelMax(pNtk));
     Delta /= 2;
 
     // make sure this clock period is feasible
@@ -155,11 +162,17 @@ float Seq_MapRetimeDelayLagsInternal( Abc_Ntk_t * pNtk, int fVerbose )
         Seq_NodeSetLag( pNode, NodeLag );
         NodeLag = Seq_NodeComputeLagFloat( Seq_NodeGetLValueN(pNode), FiBest );
         Seq_NodeSetLagN( pNode, NodeLag );
+//printf( "%6d=(%d,%d) ", pNode->Id, Seq_NodeGetLag(pNode), Seq_NodeGetLagN(pNode) );
+//        if ( Seq_NodeGetLag(pNode) != Seq_NodeGetLagN(pNode) )
+//        {
+//printf( "%6d=(%d,%d) ", pNode->Id, Seq_NodeGetLag(pNode), Seq_NodeGetLagN(pNode) );
+//        }
     }
+//printf( "\n\n" );
 
     // print the result
-    if ( fVerbose )
-    printf( "The best clock period is %6.2f.\n", FiBest );
+//    if ( fVerbose )
+    printf( "The best clock period after mapping/retiming is %6.2f.\n", FiBest );
     return FiBest;
 }
 
@@ -209,7 +222,7 @@ int Seq_MapRetimeForPeriod( Abc_Ntk_t * pNtk, float Fi, int fVerbose )
     // set l-values of all nodes to be minus infinity
     Vec_IntFill( p->vLValues,  p->nSize, Abc_Float2Int( (float)-ABC_INFINITY ) );
     Vec_IntFill( p->vLValuesN, p->nSize, Abc_Float2Int( (float)-ABC_INFINITY ) );
-    Vec_StrFill( p->vUses,     p->nSize, 0             );
+    Vec_StrFill( p->vUses,     p->nSize, 0 );
 
     // set l-values of constants and PIs
     pObj = Abc_NtkObj( pNtk, 0 );
@@ -243,6 +256,7 @@ int Seq_MapRetimeForPeriod( Abc_Ntk_t * pNtk, float Fi, int fVerbose )
             break;
         if ( fChange == 0 )
             break;
+//printf( "\n\n" );
     }
     if ( c == p->nMaxIters )
     {
@@ -265,7 +279,6 @@ int Seq_MapRetimeForPeriod( Abc_Ntk_t * pNtk, float Fi, int fVerbose )
 
 
 
-
 /**Function*************************************************************
 
   Synopsis    [Computes the l-value of the cut.]
@@ -325,6 +338,15 @@ float Seq_MapNodeComputeCut(  Abc_Obj_t * pObj, Cut_Cut_t * pCut, int fCompl, fl
     assert( pCut->nLeaves < 6 );
     // get the canonical truth table of this cut
     uCanon[0] = uCanon[1] = (fCompl? pCut->uCanon0 : pCut->uCanon1);
+    if ( uCanon[0] == 0 || ~uCanon[0] == 0 )
+    {
+        if ( pMatchBest )
+        {
+            memset( pMatchBest, 0, sizeof(Seq_Match_t) );
+            pMatchBest->pCut = pCut;
+        }
+        return (float)0.0;
+    }
     // match the given phase of the cut
     pSuperList = Map_SuperTableLookupC( p->pSuperLib, uCanon );
     // compute the arrival times of each supergate
@@ -340,7 +362,7 @@ float Seq_MapNodeComputeCut(  Abc_Obj_t * pObj, Cut_Cut_t * pCut, int fCompl, fl
             pMatchCur->uPhase = (fCompl? pCut->Num0 : pCut->Num1) ^ pSuper->uPhases[i];
             // find the arrival time of this match
             lValueCur = Seq_MapSuperGetArrival( pObj, Fi, pMatchCur, lValueBest );
-            if ( lValueBest > lValueCur )
+            if ( lValueBest > lValueCur )//&& lValueCur > -ABC_INFINITY/2 )
             {
                 lValueBest = lValueCur;
                 if ( pMatchBest )
@@ -348,6 +370,7 @@ float Seq_MapNodeComputeCut(  Abc_Obj_t * pObj, Cut_Cut_t * pCut, int fCompl, fl
             }
         }
     }
+//    assert( lValueBest < ABC_INFINITY/2 );
     return lValueBest;
 }
 
@@ -366,22 +389,23 @@ float Seq_MapNodeComputePhase( Abc_Obj_t * pObj, int fCompl, float Fi, Seq_Match
 {
     Seq_Match_t Match, * pMatchCur = &Match;
     Cut_Cut_t * pList, * pCut;
-    float lValueNew, lValueCut;
+    float lValueBest, lValueCut;
     // get the list of cuts
     pList = Abc_NodeReadCuts( Seq_NodeCutMan(pObj), pObj );
     // get the arrival time of the best non-trivial cut
-    lValueNew = ABC_INFINITY;
+    lValueBest = ABC_INFINITY;
     for ( pCut = pList->pNext; pCut; pCut = pCut->pNext )
     {
         lValueCut = Seq_MapNodeComputeCut( pObj, pCut, fCompl, Fi, pMatchBest? pMatchCur : NULL );
-        if ( lValueNew > lValueCut )
+        if ( lValueBest > lValueCut )
         {
-            lValueNew = lValueCut;
+            lValueBest = lValueCut;
             if ( pMatchBest )
                 *pMatchBest = *pMatchCur;
         }
     }
-    return lValueNew;
+//    assert( lValueBest < ABC_INFINITY/2 );
+    return lValueBest;
 }
 
 /**Function*************************************************************
@@ -434,11 +458,14 @@ int Seq_MapNodeUpdateLValue( Abc_Obj_t * pObj, float Fi, float DelayInv )
     // compare 
     if ( lValue0 <= lValueOld0 + p->fEpsilon && lValue1 <= lValueOld1 + p->fEpsilon )
         return SEQ_UPDATE_NO;
+    assert( lValue0 < ABC_INFINITY/2 );
+    assert( lValue1 < ABC_INFINITY/2 );
     // update the values
     if ( lValue0 > lValueOld0 + p->fEpsilon )
         Seq_NodeSetLValueN( pObj, lValue0 );
     if ( lValue1 > lValueOld1 + p->fEpsilon )
         Seq_NodeSetLValueP( pObj, lValue1 );
+//printf( "%6d=(%4.2f,%4.2f) ", pObj->Id, Seq_NodeGetLValueP(pObj), Seq_NodeGetLValueN(pObj) );
     return SEQ_UPDATE_YES;
 }
 
@@ -460,6 +487,7 @@ float Seq_MapCollectNode_rec( Abc_Obj_t * pAnd, float FiBest, Vec_Ptr_t * vMappi
     Seq_Match_t * pMatch;
     Abc_Obj_t * pFanin;
     int k, fCompl, Use;
+    float AreaInv = Mio_LibraryReadAreaInv(Abc_FrameReadLibGen());
     float Area;
 
     // get the polarity of the node
@@ -467,42 +495,44 @@ float Seq_MapCollectNode_rec( Abc_Obj_t * pAnd, float FiBest, Vec_Ptr_t * vMappi
     pAnd   = Abc_ObjRegular(pAnd);
 
     // skip visited nodes
-    if ( fCompl )
-    {
-        if ( pAnd->fMarkB )
+    if ( !fCompl )
+    {  // need the positive polarity
+        if ( pAnd->fMarkA )
             return 0.0;
-        pAnd->fMarkB = 1;
+        pAnd->fMarkA = 1;
     }
     else
-    {
-        if ( pAnd->fMarkA )
+    {   // need the negative polarity
+        if ( pAnd->fMarkB )
             return 0.0;
-        pAnd->fMarkA = 1;
+        pAnd->fMarkB = 1;
     }
 
-    // skip if this is a non-PI node
+    // skip if this is a PI or a constant
     if ( !Abc_NodeIsAigAnd(pAnd) )
     {
         if ( Abc_ObjIsPi(pAnd) && fCompl )
-            return Mio_LibraryReadAreaInv(Abc_FrameReadLibGen());   
+            return AreaInv;   
         return 0.0;
     }
 
     // check the uses of this node
     Use = Seq_NodeGetUses( pAnd );
-    if ( fCompl && Use == 2 )  // the neg phase is required; the pos phase is used
+    if ( !fCompl && Use == 1 )  // the pos phase is required; only the neg phase is used
     {
-        Area = Seq_MapCollectNode_rec( pAnd, FiBest, vMapping, vMapCuts );
-        return Area + Mio_LibraryReadAreaInv(Abc_FrameReadLibGen()); 
+        Area = Seq_MapCollectNode_rec( Abc_ObjNot(pAnd), FiBest, vMapping, vMapCuts );
+        return Area + AreaInv; 
     }
-    if ( !fCompl && Use == 1 )  // the pos phase is required; the neg phase is used
+    if ( fCompl && Use == 2 )  // the neg phase is required; only the pos phase is used
     {
-        Area = Seq_MapCollectNode_rec( Abc_ObjNot(pAnd), FiBest, vMapping, vMapCuts );
-        return Area + Mio_LibraryReadAreaInv(Abc_FrameReadLibGen()); 
+        Area = Seq_MapCollectNode_rec( pAnd, FiBest, vMapping, vMapCuts );
+        return Area + AreaInv; 
     }
+    // both phases are used; the needed one can be selected
 
     // get the best match
     pMatch = ALLOC( Seq_Match_t, 1 );
+    memset( pMatch, 1, sizeof(Seq_Match_t) );
     Seq_MapNodeComputePhase( pAnd, fCompl, FiBest, pMatch );
     pMatch->pAnd    = pAnd;
     pMatch->fCompl  = fCompl;
@@ -510,7 +540,7 @@ float Seq_MapCollectNode_rec( Abc_Obj_t * pAnd, float FiBest, Vec_Ptr_t * vMappi
     pMatch->PolUse  = Use;
 
     // call for the fanin cuts
-    Area = pMatch->pSuper->Area;
+    Area = pMatch->pSuper? pMatch->pSuper->Area : (float)0.0;
     for ( k = 0; k < (int)pMatch->pCut->nLeaves; k++ )
     {
         pFanin = Abc_NtkObj( pAnd->pNtk, pMatch->pCut->pLeaves[k] >> 8 );
@@ -524,6 +554,9 @@ float Seq_MapCollectNode_rec( Abc_Obj_t * pAnd, float FiBest, Vec_Ptr_t * vMappi
     for ( k = 0; k < (int)pMatch->pCut->nLeaves; k++ )
         Vec_VecPush( vMapCuts, Vec_PtrSize(vMapping)-1, (void *)pMatch->pCut->pLeaves[k] );
 
+    // the cut will become unavailable when the cuts are deallocated
+    pMatch->pCut = NULL;
+
     return Area;
 }
 
@@ -551,6 +584,7 @@ void Seq_MapCanonicizeTruthTables( Abc_Ntk_t * pNtk )
     }
 }
 
+
 ////////////////////////////////////////////////////////////////////////
 ///                       END OF FILE                                ///
 ////////////////////////////////////////////////////////////////////////
diff --git a/src/base/seq/seqRetCore.c b/src/base/seq/seqRetCore.c
index 154f8dad..f989eefb 100644
--- a/src/base/seq/seqRetCore.c
+++ b/src/base/seq/seqRetCore.c
@@ -26,8 +26,7 @@
 ////////////////////////////////////////////////////////////////////////
 
 static Abc_Ntk_t * Seq_NtkRetimeDerive( Abc_Ntk_t * pNtk, int fVerbose );
-static Abc_Obj_t * Seq_NodeRetimeDerive( Abc_Ntk_t * pNtkNew, Abc_Obj_t * pNode, char * pSop );
-static void        Seq_NodeAddEdges_rec( Abc_Obj_t * pGoal, Abc_Obj_t * pNode, Abc_InitType_t Init );
+static Abc_Obj_t * Seq_NodeRetimeDerive( Abc_Ntk_t * pNtkNew, Abc_Obj_t * pNode, char * pSop, Vec_Ptr_t * vFanins );
 static Abc_Ntk_t * Seq_NtkRetimeReconstruct( Abc_Ntk_t * pNtkOld, Abc_Ntk_t * pNtkSeq );
 static Abc_Obj_t * Seq_EdgeReconstruct_rec( Abc_Obj_t * pGoal, Abc_Obj_t * pNode );
 static Abc_Obj_t * Seq_EdgeReconstructPO( Abc_Obj_t * pNode );
@@ -66,7 +65,6 @@ Abc_Ntk_t * Seq_NtkRetime( Abc_Ntk_t * pNtk, int nMaxIters, int fInitial, int fV
     RetValue = Seq_NtkImplementRetiming( pNtkSeq, p->vLags, fVerbose );
     if ( RetValue == 0 )
         printf( "Retiming completed but initial state computation has failed.\n" );
-
 //return pNtkSeq;
 
     // create the final mapped network
@@ -90,7 +88,9 @@ Abc_Ntk_t * Seq_NtkRetimeDerive( Abc_Ntk_t * pNtk, int fVerbose )
 {
     Abc_Seq_t * p;
     Abc_Ntk_t * pNtkNew;
-    Abc_Obj_t * pObj, * pFanin, * pFanout;
+    Abc_Obj_t * pObj, * pFanin, * pMirror;
+    Vec_Ptr_t * vMapAnds, * vMirrors;
+    Vec_Vec_t * vMapFanins;
     int i, k, RetValue, fHasBdds;
     char * pSop;
 
@@ -126,14 +126,22 @@ Abc_Ntk_t * Seq_NtkRetimeDerive( Abc_Ntk_t * pNtk, int fVerbose )
     Abc_NtkForEachPo( pNtk, pObj, i )
         Abc_NtkLogicStoreName( pObj->pCopy, Abc_ObjName(pObj) );
 
-    // create one AND for each logic node
-    Abc_NtkForEachNode( pNtk, pObj, i )
+    // create one AND for each logic node in the topological order
+    vMapAnds = Abc_NtkDfs( pNtk, 0 );
+    Vec_PtrForEachEntry( vMapAnds, pObj, i )
     {
-        if ( Abc_ObjFaninNum(pObj) == 0 && Abc_ObjFanoutNum(pObj) == 0 )
+        if ( pObj->Id == 0 )
+        {
+            pObj->pCopy = Abc_NtkConst1(pNtkNew);
             continue;
+        }
         pObj->pCopy = Abc_NtkCreateNode( pNtkNew );
-        pObj->pCopy->pCopy = pObj;
     }
+
+    // make the new seq AIG point to the old network through pNext
+    Abc_NtkForEachObj( pNtk, pObj, i )
+        if ( pObj->pCopy ) pObj->pCopy->pNext = pObj;
+
     // make latches point to the latch fanins
     Abc_NtkForEachLatch( pNtk, pObj, i )
     {
@@ -142,16 +150,15 @@ Abc_Ntk_t * Seq_NtkRetimeDerive( Abc_Ntk_t * pNtk, int fVerbose )
     }
 
     // create internal AND nodes w/o strashing for each logic node (including constants)
-    Abc_NtkForEachNode( pNtk, pObj, i )
+    vMapFanins = Vec_VecStart( Vec_PtrSize(vMapAnds) );
+    Vec_PtrForEachEntry( vMapAnds, pObj, i )
     {
-        if ( Abc_ObjFaninNum(pObj) == 0 && Abc_ObjFanoutNum(pObj) == 0 )
-            continue;
         // get the SOP of the node
         if ( Abc_NtkHasMapping(pNtk) )
             pSop = Mio_GateReadSop(pObj->pData);
         else
             pSop = pObj->pData;
-        pFanin = Seq_NodeRetimeDerive( pNtkNew, pObj, pSop );
+        pFanin = Seq_NodeRetimeDerive( pNtkNew, pObj, pSop, Vec_VecEntry(vMapFanins, i) );
         Abc_ObjAddFanin( pObj->pCopy, pFanin );
         Abc_ObjAddFanin( pObj->pCopy, pFanin );
     }
@@ -164,20 +171,31 @@ Abc_Ntk_t * Seq_NtkRetimeDerive( Abc_Ntk_t * pNtk, int fVerbose )
     Seq_Resize( p, Abc_NtkObjNumMax(pNtkNew) );
 
     // add the sequential edges
-    Abc_NtkForEachLatch( pNtk, pObj, i )
-        Abc_ObjForEachFanout( pObj, pFanout, k )
+    Vec_PtrForEachEntry( vMapAnds, pObj, i )
+    {
+        vMirrors = Vec_VecEntry( vMapFanins, i );
+        Abc_ObjForEachFanin( pObj, pFanin, k )
         {
-            if ( pObj->pCopy == Abc_ObjFanin0(pFanout->pCopy) )
+            pMirror = Vec_PtrEntry( vMirrors, k );
+            if ( Abc_ObjIsLatch(pFanin) )
             {
-                Seq_NodeInsertFirst( pFanout->pCopy, 0, Abc_LatchInit(pObj) );
-                Seq_NodeInsertFirst( pFanout->pCopy, 1, Abc_LatchInit(pObj) );
-                continue;
+                Seq_NodeInsertFirst( pMirror, 0, Abc_LatchInit(pFanin) );
+                Seq_NodeInsertFirst( pMirror, 1, Abc_LatchInit(pFanin) );
             }
-            Seq_NodeAddEdges_rec( pObj->pCopy, Abc_ObjFanin0(pFanout->pCopy), Abc_LatchInit(pObj) );
         }
+    }
+    // add the sequential edges to the POs
+    Abc_NtkForEachPo( pNtk, pObj, i )
+    {
+        pFanin = Abc_ObjFanin0(pObj);
+        if ( Abc_ObjIsLatch(pFanin) )
+            Seq_NodeInsertFirst( pObj->pCopy, 0, Abc_LatchInit(pFanin) );
+    }
+
 
-    // collect the nodes in the topological order
-    p->vMapAnds   = Abc_NtkDfs( pNtk, 0 );
+    // save the fanin/delay info
+    p->vMapAnds   = vMapAnds;
+    p->vMapFanins = vMapFanins;
     p->vMapCuts   = Vec_VecStart( Vec_PtrSize(p->vMapAnds) );
     p->vMapDelays = Vec_VecStart( Vec_PtrSize(p->vMapAnds) );
     Vec_PtrForEachEntry( p->vMapAnds, pObj, i )
@@ -224,37 +242,6 @@ Abc_Ntk_t * Seq_NtkRetimeDerive( Abc_Ntk_t * pNtk, int fVerbose )
     return pNtkNew;
 }
 
-/**Function*************************************************************
-
-  Synopsis    [Add sequential edges.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-void Seq_NodeAddEdges_rec( Abc_Obj_t * pGoal, Abc_Obj_t * pNode, Abc_InitType_t Init )
-{
-    Abc_Obj_t * pFanin;
-    assert( !Abc_ObjIsLatch(pNode) );
-    if ( !Abc_NodeIsAigAnd(pNode) )
-        return;
-    // consider the first fanin
-    pFanin = Abc_ObjFanin0(pNode);
-    if ( pFanin->pCopy == NULL ) // internal node
-        Seq_NodeAddEdges_rec( pGoal, pFanin, Init );
-    else if ( pFanin == pGoal )
-        Seq_NodeInsertFirst( pNode, 0, Init );
-    // consider the second fanin
-    pFanin = Abc_ObjFanin1(pNode);
-    if ( pFanin->pCopy == NULL ) // internal node
-        Seq_NodeAddEdges_rec( pGoal, pFanin, Init );
-    else if ( pFanin == pGoal )
-        Seq_NodeInsertFirst( pNode, 1, Init );
-}
-
 
 /**Function*************************************************************
 
@@ -267,11 +254,11 @@ void Seq_NodeAddEdges_rec( Abc_Obj_t * pGoal, Abc_Obj_t * pNode, Abc_InitType_t
   SeeAlso     []
 
 ***********************************************************************/
-Abc_Obj_t * Seq_NodeRetimeDerive( Abc_Ntk_t * pNtkNew, Abc_Obj_t * pRoot, char * pSop )
+Abc_Obj_t * Seq_NodeRetimeDerive( Abc_Ntk_t * pNtkNew, Abc_Obj_t * pRoot, char * pSop, Vec_Ptr_t * vFanins )
 {
     Dec_Graph_t * pFForm;
     Dec_Node_t * pNode;
-    Abc_Obj_t * pAnd;
+    Abc_Obj_t * pResult, * pFanin, * pMirror;
     int i, nFanins;
 
     // get the number of node's fanins
@@ -280,26 +267,39 @@ Abc_Obj_t * Seq_NodeRetimeDerive( Abc_Ntk_t * pNtkNew, Abc_Obj_t * pRoot, char *
     if ( nFanins < 2 )
     {
         if ( Abc_SopIsConst1(pSop) )
-            return Abc_NtkConst1(pNtkNew);
+            pFanin = Abc_NtkConst1(pNtkNew);
         else if ( Abc_SopIsConst0(pSop) )
-            return Abc_ObjNot( Abc_NtkConst1(pNtkNew) );
+            pFanin = Abc_ObjNot( Abc_NtkConst1(pNtkNew) );
         else if ( Abc_SopIsBuf(pSop) )
-            return Abc_ObjFanin0(pRoot)->pCopy;
+            pFanin = Abc_ObjFanin0(pRoot)->pCopy;
         else if ( Abc_SopIsInv(pSop) )
-            return Abc_ObjNot( Abc_ObjFanin0(pRoot)->pCopy );
-        assert( 0 );
-        return NULL;
+            pFanin = Abc_ObjNot( Abc_ObjFanin0(pRoot)->pCopy );
+        else
+            assert( 0 );
+        // create the node with these fanins
+        pMirror = Abc_NtkCreateNode( pNtkNew );
+        Abc_ObjAddFanin( pMirror, pFanin );
+        Abc_ObjAddFanin( pMirror, pFanin );
+        Vec_PtrPush( vFanins, pMirror );
+        return pMirror;
     }
 
     // perform factoring
     pFForm = Dec_Factor( pSop );
     // collect the fanins
     Dec_GraphForEachLeaf( pFForm, pNode, i )
-        pNode->pFunc = Abc_ObjFanin(pRoot,i)->pCopy;
+    {
+        pFanin = Abc_ObjFanin(pRoot,i)->pCopy;
+        pMirror = Abc_NtkCreateNode( pNtkNew );
+        Abc_ObjAddFanin( pMirror, pFanin );
+        Abc_ObjAddFanin( pMirror, pFanin );
+        Vec_PtrPush( vFanins, pMirror );
+        pNode->pFunc = pMirror;
+    }
     // perform strashing
-    pAnd = Dec_GraphToNetworkNoStrash( pNtkNew, pFForm );
+    pResult = Dec_GraphToNetworkNoStrash( pNtkNew, pFForm );
     Dec_GraphFree( pFForm );
-    return pAnd;
+    return pResult;
 }
 
 
@@ -317,8 +317,10 @@ Abc_Obj_t * Seq_NodeRetimeDerive( Abc_Ntk_t * pNtkNew, Abc_Obj_t * pRoot, char *
 Abc_Ntk_t * Seq_NtkRetimeReconstruct( Abc_Ntk_t * pNtkOld, Abc_Ntk_t * pNtkSeq )
 {
     Abc_Seq_t * p = pNtkSeq->pManFunc;
+    Seq_Lat_t * pRing0, * pRing1;
     Abc_Ntk_t * pNtkNew;
-    Abc_Obj_t * pObj, * pObjNew, * pFanin, * pFaninNew;
+    Abc_Obj_t * pObj, * pObjNew, * pFanin, * pFaninNew, * pMirror;
+    Vec_Ptr_t * vMirrors;
     int i, k;
 
     assert( !Abc_NtkIsSeq(pNtkOld) );
@@ -331,6 +333,14 @@ Abc_Ntk_t * Seq_NtkRetimeReconstruct( Abc_Ntk_t * pNtkOld, Abc_Ntk_t * pNtkSeq )
     // start the final network
     pNtkNew = Abc_NtkStartFrom( pNtkSeq, pNtkOld->ntkType, pNtkOld->ntkFunc );
 
+    // transfer the pointers to the old network
+    if ( Abc_NtkConst1(pNtkOld) ) 
+        Abc_NtkConst1(pNtkOld)->pCopy = Abc_NtkConst1(pNtkNew);
+    Abc_NtkForEachPi( pNtkOld, pObj, i )
+        pObj->pCopy = pObj->pNext->pCopy;
+    Abc_NtkForEachPo( pNtkOld, pObj, i )
+        pObj->pCopy = pObj->pNext->pCopy;
+
     // copy the internal nodes of the old network into the new network
     // transfer the pointers pNktOld->pNtkNew to pNtkSeq->pNtkNew
     Abc_NtkForEachNode( pNtkOld, pObj, i )
@@ -339,25 +349,50 @@ Abc_Ntk_t * Seq_NtkRetimeReconstruct( Abc_Ntk_t * pNtkOld, Abc_Ntk_t * pNtkSeq )
         Abc_NtkDupObj( pNtkNew, pObj );
         pObj->pNext->pCopy = pObj->pCopy;
     }
+    Abc_NtkForEachLatch( pNtkOld, pObj, i )
+        pObj->pCopy = Abc_ObjFanin0(pObj)->pCopy;
 
     // share the latches
     Seq_NtkShareLatches( pNtkNew, pNtkSeq );
 
     // connect the objects
-    Abc_NtkForEachNode( pNtkOld, pObj, i )
+//    Abc_NtkForEachNode( pNtkOld, pObj, i )
+    Vec_PtrForEachEntry( p->vMapAnds, pObj, i )
+    {
+        // pObj is from pNtkSeq - transform to pNtkOld
+        pObj = pObj->pNext;
+        // iterate through the fanins of this node in the old network
+        vMirrors = Vec_VecEntry( p->vMapFanins, i );
         Abc_ObjForEachFanin( pObj, pFanin, k )
         {
-            pFaninNew = Seq_EdgeReconstruct_rec( pFanin->pNext, pObj->pNext );
-            assert( pFaninNew != NULL );
-            Abc_ObjAddFanin( pObj->pCopy, pFaninNew );
+            pMirror = Vec_PtrEntry( vMirrors, k );
+            assert( Seq_ObjFaninL0(pMirror) == Seq_ObjFaninL1(pMirror) );
+            pRing0 = Seq_NodeGetRing( pMirror, 0 );
+            pRing1 = Seq_NodeGetRing( pMirror, 1 );
+            if ( pRing0 == NULL )
+            {
+                Abc_ObjAddFanin( pObj->pCopy, pFanin->pCopy );
+                continue;
+            }
+//            assert( pRing0->pLatch == pRing1->pLatch );
+            if ( pRing0->pLatch->pData > pRing1->pLatch->pData )
+                Abc_ObjAddFanin( pObj->pCopy, pRing0->pLatch );
+            else
+                Abc_ObjAddFanin( pObj->pCopy, pRing1->pLatch );
         }
+    }
 
     // connect the POs
     Abc_NtkForEachPo( pNtkOld, pObj, i )
     {
-        pFaninNew = Seq_EdgeReconstructPO( pObj->pNext );
+        pFanin = Abc_ObjFanin0(pObj);
+        pRing0 = Seq_NodeGetRing( Abc_NtkPo(pNtkSeq, i), 0 );
+        if ( pRing0 )
+            pFaninNew = pRing0->pLatch;
+        else 
+            pFaninNew = pFanin->pCopy;
         assert( pFaninNew != NULL );
-        Abc_ObjAddFanin( pObj->pNext->pCopy, pFaninNew );
+        Abc_ObjAddFanin( pObj->pCopy, pFaninNew );
     }
 
     // clean the result of latch sharing
diff --git a/src/base/seq/seqRetCore_old.c b/src/base/seq/seqRetCore_old.c
new file mode 100644
index 00000000..154f8dad
--- /dev/null
+++ b/src/base/seq/seqRetCore_old.c
@@ -0,0 +1,453 @@
+/**CFile****************************************************************
+
+  FileName    [seqRetCore.c]
+
+  SystemName  [ABC: Logic synthesis and verification system.]
+
+  PackageName [Construction and manipulation of sequential AIGs.]
+
+  Synopsis    [The core of FPGA mapping/retiming package.]
+
+  Author      [Alan Mishchenko]
+  
+  Affiliation [UC Berkeley]
+
+  Date        [Ver. 1.0. Started - June 20, 2005.]
+
+  Revision    [$Id: seqRetCore.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
+
+***********************************************************************/
+
+#include "seqInt.h"
+#include "dec.h"
+
+////////////////////////////////////////////////////////////////////////
+///                        DECLARATIONS                              ///
+////////////////////////////////////////////////////////////////////////
+
+static Abc_Ntk_t * Seq_NtkRetimeDerive( Abc_Ntk_t * pNtk, int fVerbose );
+static Abc_Obj_t * Seq_NodeRetimeDerive( Abc_Ntk_t * pNtkNew, Abc_Obj_t * pNode, char * pSop );
+static void        Seq_NodeAddEdges_rec( Abc_Obj_t * pGoal, Abc_Obj_t * pNode, Abc_InitType_t Init );
+static Abc_Ntk_t * Seq_NtkRetimeReconstruct( Abc_Ntk_t * pNtkOld, Abc_Ntk_t * pNtkSeq );
+static Abc_Obj_t * Seq_EdgeReconstruct_rec( Abc_Obj_t * pGoal, Abc_Obj_t * pNode );
+static Abc_Obj_t * Seq_EdgeReconstructPO( Abc_Obj_t * pNode );
+
+////////////////////////////////////////////////////////////////////////
+///                     FUNCTION DEFINITIONS                         ///
+////////////////////////////////////////////////////////////////////////
+
+/**Function*************************************************************
+
+  Synopsis    [Performs FPGA mapping and retiming.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Abc_Ntk_t * Seq_NtkRetime( Abc_Ntk_t * pNtk, int nMaxIters, int fInitial, int fVerbose )
+{
+    Abc_Seq_t * p;
+    Abc_Ntk_t * pNtkSeq, * pNtkNew;
+    int RetValue;
+    assert( !Abc_NtkHasAig(pNtk) );
+    // derive the isomorphic seq AIG
+    pNtkSeq = Seq_NtkRetimeDerive( pNtk, fVerbose );
+    p = pNtkSeq->pManFunc;
+    p->nMaxIters = nMaxIters;
+
+    if ( !fInitial )
+        Seq_NtkLatchSetValues( pNtkSeq, ABC_INIT_DC );
+    // find the best mapping and retiming 
+    Seq_NtkRetimeDelayLags( pNtk, pNtkSeq, fVerbose );
+    // implement the retiming
+    RetValue = Seq_NtkImplementRetiming( pNtkSeq, p->vLags, fVerbose );
+    if ( RetValue == 0 )
+        printf( "Retiming completed but initial state computation has failed.\n" );
+
+//return pNtkSeq;
+
+    // create the final mapped network
+    pNtkNew = Seq_NtkRetimeReconstruct( pNtk, pNtkSeq );
+    Abc_NtkDelete( pNtkSeq );
+    return pNtkNew;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Derives the isomorphic seq AIG.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Abc_Ntk_t * Seq_NtkRetimeDerive( Abc_Ntk_t * pNtk, int fVerbose )
+{
+    Abc_Seq_t * p;
+    Abc_Ntk_t * pNtkNew;
+    Abc_Obj_t * pObj, * pFanin, * pFanout;
+    int i, k, RetValue, fHasBdds;
+    char * pSop;
+
+    // make sure it is an AIG without self-feeding latches
+    assert( !Abc_NtkHasAig(pNtk) );
+    if ( RetValue = Abc_NtkRemoveSelfFeedLatches(pNtk) )
+        printf( "Modified %d self-feeding latches. The result will not verify.\n", RetValue );
+    assert( Abc_NtkCountSelfFeedLatches(pNtk) == 0 );
+
+    // remove the dangling nodes
+    Abc_NtkCleanup( pNtk, fVerbose );
+
+    // transform logic functions from BDD to SOP
+    if ( fHasBdds = Abc_NtkIsBddLogic(pNtk) )
+        Abc_NtkBddToSop(pNtk);
+
+    // start the network
+    pNtkNew = Abc_NtkAlloc( ABC_NTK_SEQ, ABC_FUNC_AIG );
+    // duplicate the name and the spec
+    pNtkNew->pName = util_strsav(pNtk->pName);
+    pNtkNew->pSpec = util_strsav(pNtk->pSpec);
+
+    // map the constant nodes
+    Abc_NtkCleanCopy( pNtk );
+    // clone the PIs/POs/latches
+    Abc_NtkForEachPi( pNtk, pObj, i )
+        Abc_NtkDupObj( pNtkNew, pObj );
+    Abc_NtkForEachPo( pNtk, pObj, i )
+        Abc_NtkDupObj( pNtkNew, pObj );
+    // copy the names
+    Abc_NtkForEachPi( pNtk, pObj, i )
+        Abc_NtkLogicStoreName( pObj->pCopy, Abc_ObjName(pObj) );
+    Abc_NtkForEachPo( pNtk, pObj, i )
+        Abc_NtkLogicStoreName( pObj->pCopy, Abc_ObjName(pObj) );
+
+    // create one AND for each logic node
+    Abc_NtkForEachNode( pNtk, pObj, i )
+    {
+        if ( Abc_ObjFaninNum(pObj) == 0 && Abc_ObjFanoutNum(pObj) == 0 )
+            continue;
+        pObj->pCopy = Abc_NtkCreateNode( pNtkNew );
+        pObj->pCopy->pCopy = pObj;
+    }
+    // make latches point to the latch fanins
+    Abc_NtkForEachLatch( pNtk, pObj, i )
+    {
+        assert( !Abc_ObjIsLatch(Abc_ObjFanin0(pObj)) );
+        pObj->pCopy = Abc_ObjFanin0(pObj)->pCopy;
+    }
+
+    // create internal AND nodes w/o strashing for each logic node (including constants)
+    Abc_NtkForEachNode( pNtk, pObj, i )
+    {
+        if ( Abc_ObjFaninNum(pObj) == 0 && Abc_ObjFanoutNum(pObj) == 0 )
+            continue;
+        // get the SOP of the node
+        if ( Abc_NtkHasMapping(pNtk) )
+            pSop = Mio_GateReadSop(pObj->pData);
+        else
+            pSop = pObj->pData;
+        pFanin = Seq_NodeRetimeDerive( pNtkNew, pObj, pSop );
+        Abc_ObjAddFanin( pObj->pCopy, pFanin );
+        Abc_ObjAddFanin( pObj->pCopy, pFanin );
+    }
+    // connect the POs
+    Abc_NtkForEachPo( pNtk, pObj, i )
+        Abc_ObjAddFanin( pObj->pCopy, Abc_ObjFanin0(pObj)->pCopy );
+    
+    // start the storage for initial states
+    p = pNtkNew->pManFunc;
+    Seq_Resize( p, Abc_NtkObjNumMax(pNtkNew) );
+
+    // add the sequential edges
+    Abc_NtkForEachLatch( pNtk, pObj, i )
+        Abc_ObjForEachFanout( pObj, pFanout, k )
+        {
+            if ( pObj->pCopy == Abc_ObjFanin0(pFanout->pCopy) )
+            {
+                Seq_NodeInsertFirst( pFanout->pCopy, 0, Abc_LatchInit(pObj) );
+                Seq_NodeInsertFirst( pFanout->pCopy, 1, Abc_LatchInit(pObj) );
+                continue;
+            }
+            Seq_NodeAddEdges_rec( pObj->pCopy, Abc_ObjFanin0(pFanout->pCopy), Abc_LatchInit(pObj) );
+        }
+
+    // collect the nodes in the topological order
+    p->vMapAnds   = Abc_NtkDfs( pNtk, 0 );
+    p->vMapCuts   = Vec_VecStart( Vec_PtrSize(p->vMapAnds) );
+    p->vMapDelays = Vec_VecStart( Vec_PtrSize(p->vMapAnds) );
+    Vec_PtrForEachEntry( p->vMapAnds, pObj, i )
+    {
+        // change the node to be the new one
+        Vec_PtrWriteEntry( p->vMapAnds, i, pObj->pCopy );
+        // collect the new fanins of this node
+        Abc_ObjForEachFanin( pObj, pFanin, k )
+            Vec_VecPush( p->vMapCuts, i, (void *)( (pFanin->pCopy->Id << 8) | Abc_ObjIsLatch(pFanin) ) );
+        // collect the delay info
+        if ( !Abc_NtkHasMapping(pNtk) )
+        {
+            Abc_ObjForEachFanin( pObj, pFanin, k )
+                Vec_VecPush( p->vMapDelays, i, (void *)Abc_Float2Int(1.0) );
+        }
+        else
+        {
+            Mio_Pin_t * pPin = Mio_GateReadPins(pObj->pData);
+            float Max, tDelayBlockRise, tDelayBlockFall;
+            Abc_ObjForEachFanin( pObj, pFanin, k )
+            {
+                tDelayBlockRise = (float)Mio_PinReadDelayBlockRise( pPin );  
+                tDelayBlockFall = (float)Mio_PinReadDelayBlockFall( pPin ); 
+                Max = ABC_MAX( tDelayBlockRise, tDelayBlockFall );
+                Vec_VecPush( p->vMapDelays, i, (void *)Abc_Float2Int(Max) );
+                pPin = Mio_PinReadNext(pPin);
+            }
+        }
+    }
+
+    // set the cutset composed of latch drivers
+//    Abc_NtkAigCutsetCopy( pNtk );
+//    Seq_NtkLatchGetEqualFaninNum( pNtkNew );
+
+    // convert the network back into BDDs if this is how it was
+    if ( fHasBdds )
+        Abc_NtkSopToBdd(pNtk);
+
+    // copy EXDC and check correctness
+    if ( pNtk->pExdc )
+        fprintf( stdout, "Warning: EXDC is not copied when converting to sequential AIG.\n" );
+    if ( !Abc_NtkCheck( pNtkNew ) )
+        fprintf( stdout, "Seq_NtkRetimeDerive(): Network check has failed.\n" );
+    return pNtkNew;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Add sequential edges.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Seq_NodeAddEdges_rec( Abc_Obj_t * pGoal, Abc_Obj_t * pNode, Abc_InitType_t Init )
+{
+    Abc_Obj_t * pFanin;
+    assert( !Abc_ObjIsLatch(pNode) );
+    if ( !Abc_NodeIsAigAnd(pNode) )
+        return;
+    // consider the first fanin
+    pFanin = Abc_ObjFanin0(pNode);
+    if ( pFanin->pCopy == NULL ) // internal node
+        Seq_NodeAddEdges_rec( pGoal, pFanin, Init );
+    else if ( pFanin == pGoal )
+        Seq_NodeInsertFirst( pNode, 0, Init );
+    // consider the second fanin
+    pFanin = Abc_ObjFanin1(pNode);
+    if ( pFanin->pCopy == NULL ) // internal node
+        Seq_NodeAddEdges_rec( pGoal, pFanin, Init );
+    else if ( pFanin == pGoal )
+        Seq_NodeInsertFirst( pNode, 1, Init );
+}
+
+
+/**Function*************************************************************
+
+  Synopsis    [Strashes one logic node using its SOP.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Abc_Obj_t * Seq_NodeRetimeDerive( Abc_Ntk_t * pNtkNew, Abc_Obj_t * pRoot, char * pSop )
+{
+    Dec_Graph_t * pFForm;
+    Dec_Node_t * pNode;
+    Abc_Obj_t * pAnd;
+    int i, nFanins;
+
+    // get the number of node's fanins
+    nFanins = Abc_ObjFaninNum( pRoot );
+    assert( nFanins == Abc_SopGetVarNum(pSop) );
+    if ( nFanins < 2 )
+    {
+        if ( Abc_SopIsConst1(pSop) )
+            return Abc_NtkConst1(pNtkNew);
+        else if ( Abc_SopIsConst0(pSop) )
+            return Abc_ObjNot( Abc_NtkConst1(pNtkNew) );
+        else if ( Abc_SopIsBuf(pSop) )
+            return Abc_ObjFanin0(pRoot)->pCopy;
+        else if ( Abc_SopIsInv(pSop) )
+            return Abc_ObjNot( Abc_ObjFanin0(pRoot)->pCopy );
+        assert( 0 );
+        return NULL;
+    }
+
+    // perform factoring
+    pFForm = Dec_Factor( pSop );
+    // collect the fanins
+    Dec_GraphForEachLeaf( pFForm, pNode, i )
+        pNode->pFunc = Abc_ObjFanin(pRoot,i)->pCopy;
+    // perform strashing
+    pAnd = Dec_GraphToNetworkNoStrash( pNtkNew, pFForm );
+    Dec_GraphFree( pFForm );
+    return pAnd;
+}
+
+
+/**Function*************************************************************
+
+  Synopsis    [Reconstructs the network after retiming.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Abc_Ntk_t * Seq_NtkRetimeReconstruct( Abc_Ntk_t * pNtkOld, Abc_Ntk_t * pNtkSeq )
+{
+    Abc_Seq_t * p = pNtkSeq->pManFunc;
+    Abc_Ntk_t * pNtkNew;
+    Abc_Obj_t * pObj, * pObjNew, * pFanin, * pFaninNew;
+    int i, k;
+
+    assert( !Abc_NtkIsSeq(pNtkOld) );
+    assert( Abc_NtkIsSeq(pNtkSeq) );
+
+    // transfer the pointers pNtkOld->pNtkSeq from pCopy to pNext
+    Abc_NtkForEachObj( pNtkOld, pObj, i )
+        pObj->pNext = pObj->pCopy;
+
+    // start the final network
+    pNtkNew = Abc_NtkStartFrom( pNtkSeq, pNtkOld->ntkType, pNtkOld->ntkFunc );
+
+    // copy the internal nodes of the old network into the new network
+    // transfer the pointers pNktOld->pNtkNew to pNtkSeq->pNtkNew
+    Abc_NtkForEachNode( pNtkOld, pObj, i )
+    {
+        if ( i == 0 ) continue;
+        Abc_NtkDupObj( pNtkNew, pObj );
+        pObj->pNext->pCopy = pObj->pCopy;
+    }
+
+    // share the latches
+    Seq_NtkShareLatches( pNtkNew, pNtkSeq );
+
+    // connect the objects
+    Abc_NtkForEachNode( pNtkOld, pObj, i )
+        Abc_ObjForEachFanin( pObj, pFanin, k )
+        {
+            pFaninNew = Seq_EdgeReconstruct_rec( pFanin->pNext, pObj->pNext );
+            assert( pFaninNew != NULL );
+            Abc_ObjAddFanin( pObj->pCopy, pFaninNew );
+        }
+
+    // connect the POs
+    Abc_NtkForEachPo( pNtkOld, pObj, i )
+    {
+        pFaninNew = Seq_EdgeReconstructPO( pObj->pNext );
+        assert( pFaninNew != NULL );
+        Abc_ObjAddFanin( pObj->pNext->pCopy, pFaninNew );
+    }
+
+    // clean the result of latch sharing
+    Seq_NtkShareLatchesClean( pNtkSeq );
+
+    // add the latches and their names
+    Abc_NtkAddDummyLatchNames( pNtkNew );
+    Abc_NtkForEachLatch( pNtkNew, pObjNew, i )
+    {
+        Vec_PtrPush( pNtkNew->vCis, pObjNew );
+        Vec_PtrPush( pNtkNew->vCos, pObjNew );
+    }
+    // fix the problem with complemented and duplicated CO edges
+    Abc_NtkLogicMakeSimpleCos( pNtkNew, 1 );
+    if ( !Abc_NtkCheck( pNtkNew ) )
+        fprintf( stdout, "Seq_NtkRetimeReconstruct(): Network check has failed.\n" );
+    return pNtkNew;
+
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Reconstructs the network after retiming.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Abc_Obj_t * Seq_EdgeReconstruct_rec( Abc_Obj_t * pGoal, Abc_Obj_t * pNode )
+{
+    Seq_Lat_t * pRing;
+    Abc_Obj_t * pFanin, * pRes = NULL;
+
+    if ( !Abc_NodeIsAigAnd(pNode) )
+        return NULL;
+
+    // consider the first fanin
+    pFanin = Abc_ObjFanin0(pNode);
+    if ( pFanin->pCopy == NULL ) // internal node
+        pRes = Seq_EdgeReconstruct_rec( pGoal, pFanin );
+    else if ( pFanin == pGoal )
+    {
+        if ( pRing = Seq_NodeGetRing( pNode, 0 ) )
+            pRes = pRing->pLatch;
+        else
+            pRes = pFanin->pCopy;
+    }
+    if ( pRes != NULL )
+        return pRes;
+
+    // consider the second fanin
+    pFanin = Abc_ObjFanin1(pNode);
+    if ( pFanin->pCopy == NULL ) // internal node
+        pRes = Seq_EdgeReconstruct_rec( pGoal, pFanin );
+    else if ( pFanin == pGoal )
+    {
+        if ( pRing = Seq_NodeGetRing( pNode, 1 ) )
+            pRes = pRing->pLatch;
+        else
+            pRes = pFanin->pCopy;
+    }
+    return pRes;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Reconstructs the network after retiming.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Abc_Obj_t * Seq_EdgeReconstructPO( Abc_Obj_t * pNode )
+{
+    Seq_Lat_t * pRing;
+    assert( Abc_ObjIsPo(pNode) );
+    if ( pRing = Seq_NodeGetRing( pNode, 0 ) )
+        return pRing->pLatch;
+    else
+        return Abc_ObjFanin0(pNode)->pCopy;
+}
+
+////////////////////////////////////////////////////////////////////////
+///                       END OF FILE                                ///
+////////////////////////////////////////////////////////////////////////
+
+
diff --git a/src/base/seq/seqRetIter.c b/src/base/seq/seqRetIter.c
index 1b8ac71c..6fe571f0 100644
--- a/src/base/seq/seqRetIter.c
+++ b/src/base/seq/seqRetIter.c
@@ -31,6 +31,9 @@ static int   Seq_NtkMappingForPeriod( Abc_Ntk_t * pNtk, float Fi, int fVerbose )
 static int   Seq_NtkNodeUpdateLValue( Abc_Obj_t * pObj, float Fi, Vec_Ptr_t * vLeaves, Vec_Ptr_t * vDelays );
 static void  Seq_NodeRetimeSetLag_rec( Abc_Obj_t * pNode, char Lag );
 
+static void  Seq_NodePrintInfo( Abc_Obj_t * pNode );
+static void  Seq_NodePrintInfoPlus( Abc_Obj_t * pNode );
+
 ////////////////////////////////////////////////////////////////////////
 ///                     FUNCTION DEFINITIONS                         ///
 ////////////////////////////////////////////////////////////////////////
@@ -60,6 +63,7 @@ void Seq_NtkRetimeDelayLags( Abc_Ntk_t * pNtkOld, Abc_Ntk_t * pNtk, int fVerbose
     assert( p->vMapAnds );
     assert( p->vMapCuts );
     assert( p->vMapDelays );
+    assert( p->vMapFanins );
 
     // guess the upper bound on the clock period
     if ( Abc_NtkHasMapping(pNtkOld) )
@@ -107,6 +111,11 @@ void Seq_NtkRetimeDelayLags( Abc_Ntk_t * pNtkOld, Abc_Ntk_t * pNtk, int fVerbose
     Vec_StrFill( p->vLags,  p->nSize, 0 );
     Vec_PtrForEachEntry( p->vMapAnds, pNode, i )
     {
+        if ( Vec_PtrSize( Vec_VecEntry(p->vMapCuts, i) ) == 0 )
+        {
+            Seq_NodeSetLag( pNode, 0 );
+            continue;
+        }
         NodeLag = Seq_NodeComputeLagFloat( Seq_NodeGetLValueP(pNode), FiBest );
         Seq_NodeRetimeSetLag_rec( pNode, NodeLag );
     }
@@ -117,6 +126,8 @@ void Seq_NtkRetimeDelayLags( Abc_Ntk_t * pNtkOld, Abc_Ntk_t * pNtk, int fVerbose
     // print the result
     if ( fVerbose )
         printf( "The best clock period is %6.2f.\n", FiBest );
+
+//    Seq_NodePrintInfo( Abc_NtkObj(pNtk, 847) );
 }
 
 /**Function*************************************************************
@@ -181,6 +192,11 @@ int Seq_NtkMappingForPeriod( Abc_Ntk_t * pNtk, float Fi, int fVerbose )
             Counter++;
             vLeaves = Vec_VecEntry( p->vMapCuts, i );
             vDelays = Vec_VecEntry( p->vMapDelays, i );
+            if ( Vec_PtrSize(vLeaves) == 0 )
+            {
+                Seq_NodeSetLValueP( pObj, 0.0 );
+                continue;
+            }
             RetValue = Seq_NtkNodeUpdateLValue( pObj, Fi, vLeaves, vDelays );
             if ( RetValue == SEQ_UPDATE_YES ) 
                 fChange = 1;
@@ -293,6 +309,72 @@ void Seq_NodeRetimeSetLag_rec( Abc_Obj_t * pNode, char Lag )
 }
 
 
+/**Function*************************************************************
+
+  Synopsis    [Add sequential edges.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Seq_NodePrintInfo( Abc_Obj_t * pNode )
+{
+    Abc_Seq_t * p = pNode->pNtk->pManFunc;
+    Abc_Obj_t * pFanin, * pObj, * pLeaf;
+    Vec_Ptr_t * vLeaves;
+    unsigned SeqEdge;
+    int i, Number;
+
+    // print the node
+    printf( "    Node      = %6d.  LValue = %7.2f.  Lag = %2d.\n", 
+        pNode->Id, Seq_NodeGetLValueP(pNode), Seq_NodeGetLag(pNode) );
+
+    // find the number
+    Vec_PtrForEachEntry( p->vMapAnds, pObj, Number )
+        if ( pObj == pNode )
+            break;
+
+    // get the leaves
+    vLeaves = Vec_VecEntry( p->vMapCuts, Number );
+
+    // print the leaves
+    Vec_PtrForEachEntry( vLeaves, pLeaf, i )
+    {
+        SeqEdge   = (unsigned)pLeaf;
+        pFanin    = Abc_NtkObj( pNode->pNtk, SeqEdge >> 8 );
+        // print the leaf
+        printf( "    Fanin%d(%d) = %6d.  LValue = %7.2f.  Lag = %2d.\n", i, SeqEdge & 255,
+            pFanin->Id, Seq_NodeGetLValueP(pFanin), Seq_NodeGetLag(pFanin) );
+    }
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Add sequential edges.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Seq_NodePrintInfoPlus( Abc_Obj_t * pNode )
+{
+    Abc_Obj_t * pFanout;
+    int i;
+    printf( "CENTRAL NODE:\n" );
+    Seq_NodePrintInfo( pNode );
+    Abc_ObjForEachFanout( pNode, pFanout, i )
+    {
+        printf( "FANOUT%d:\n", i );
+        Seq_NodePrintInfo( pFanout );
+    }
+}
+
 ////////////////////////////////////////////////////////////////////////
 ///                       END OF FILE                                ///
 ////////////////////////////////////////////////////////////////////////
diff --git a/src/base/seq/seqShare.c b/src/base/seq/seqShare.c
index 417dcc83..fd2e8189 100644
--- a/src/base/seq/seqShare.c
+++ b/src/base/seq/seqShare.c
@@ -275,15 +275,17 @@ Abc_Obj_t * Seq_NtkShareLatches_rec( Abc_Ntk_t * pNtk, Abc_Obj_t * pObj, Seq_Lat
 ***********************************************************************/
 void Seq_NtkShareLatches( Abc_Ntk_t * pNtkNew, Abc_Ntk_t * pNtk )
 { 
-    Abc_Obj_t * pObj;
+    Abc_Obj_t * pObj, * pFanin;
     stmm_table * tLatchMap;
     int i;
     assert( Abc_NtkIsSeq( pNtk ) );
     tLatchMap = stmm_init_table( stmm_ptrcmp, stmm_ptrhash );
     Abc_AigForEachAnd( pNtk, pObj, i )
     {
-        Seq_NtkShareLatches_rec( pNtkNew, Abc_ObjFanin0(pObj)->pCopy, Seq_NodeGetRing(pObj,0), Seq_NodeCountLats(pObj,0), tLatchMap );
-        Seq_NtkShareLatches_rec( pNtkNew, Abc_ObjFanin1(pObj)->pCopy, Seq_NodeGetRing(pObj,1), Seq_NodeCountLats(pObj,1), tLatchMap );
+        pFanin = Abc_ObjFanin0(pObj);
+        Seq_NtkShareLatches_rec( pNtkNew, pFanin->pCopy, Seq_NodeGetRing(pObj,0), Seq_NodeCountLats(pObj,0), tLatchMap );
+        pFanin = Abc_ObjFanin1(pObj);
+        Seq_NtkShareLatches_rec( pNtkNew, pFanin->pCopy, Seq_NodeGetRing(pObj,1), Seq_NodeCountLats(pObj,1), tLatchMap );
     }
     Abc_NtkForEachPo( pNtk, pObj, i )
         Seq_NtkShareLatches_rec( pNtkNew, Abc_ObjFanin0(pObj)->pCopy, Seq_NodeGetRing(pObj,0), Seq_NodeCountLats(pObj,0), tLatchMap );
@@ -303,22 +305,36 @@ void Seq_NtkShareLatches( Abc_Ntk_t * pNtkNew, Abc_Ntk_t * pNtk )
   SeeAlso     []
 
 ***********************************************************************/
-void Seq_NtkShareLatchesFpga( Abc_Ntk_t * pNtkNew, Abc_Ntk_t * pNtk, Vec_Ptr_t * vMapAnds )
+void Seq_NtkShareLatchesMapping( Abc_Ntk_t * pNtkNew, Abc_Ntk_t * pNtk, Vec_Ptr_t * vMapAnds, int fFpga )
 { 
+    Seq_Match_t * pMatch;
     Abc_Obj_t * pObj, * pFanout;
     stmm_table * tLatchMap;
-    int i, k, nOldNodes;
+    Vec_Ptr_t * vNodes;
+    int i, k;
     assert( Abc_NtkIsSeq( pNtk ) );
+
     // start the table
     tLatchMap = stmm_init_table( stmm_ptrcmp, stmm_ptrhash );
-    // remember the old nodes
-    nOldNodes = Vec_PtrSize( vMapAnds );
-    // add constant and PIs
-    Vec_PtrPush( vMapAnds, Abc_NtkConst1(pNtk) );
+
+    // create the array of all nodes with sharable fanouts
+    vNodes = Vec_PtrAlloc( 100 );
+    Vec_PtrPush( vNodes, Abc_NtkConst1(pNtk) );
     Abc_NtkForEachPi( pNtk, pObj, i )
-        Vec_PtrPush( vMapAnds, pObj );
+        Vec_PtrPush( vNodes, pObj );
+    if ( fFpga )
+    {
+        Vec_PtrForEachEntry( vMapAnds, pObj, i )
+            Vec_PtrPush( vNodes, pObj );
+    }
+    else 
+    {
+        Vec_PtrForEachEntry( vMapAnds, pMatch, i )
+            Vec_PtrPush( vNodes, pMatch->pAnd );
+    }
+
     // process nodes used in the mapping
-    Vec_PtrForEachEntry( vMapAnds, pObj, i )
+    Vec_PtrForEachEntry( vNodes, pObj, i )
     {
         // make sure the label is clean
         Abc_ObjForEachFanout( pObj, pFanout, k )
@@ -339,7 +355,7 @@ void Seq_NtkShareLatchesFpga( Abc_Ntk_t * pNtkNew, Abc_Ntk_t * pNtk, Vec_Ptr_t *
     }
     stmm_free_table( tLatchMap );
     // return to the old array
-    Vec_PtrShrink( vMapAnds, nOldNodes );
+    Vec_PtrFree( vNodes );
 }
 
 /**Function*************************************************************
diff --git a/src/base/seq/seqUtil.c b/src/base/seq/seqUtil.c
index a3b8bc84..d9fad0ea 100644
--- a/src/base/seq/seqUtil.c
+++ b/src/base/seq/seqUtil.c
@@ -417,6 +417,50 @@ int Seq_NtkCountNodesAboveLimit( Abc_Ntk_t * pNtk, int Limit )
     return Counter;
 }
 
+/**Function*************************************************************
+
+  Synopsis    [Computes area flows.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Seq_MapComputeAreaFlows( Abc_Ntk_t * pNtk, int fVerbose )
+{
+    Abc_Seq_t * p = pNtk->pManFunc;
+    Abc_Obj_t * pObj;
+    float AFlow;
+    int i, c;
+
+    assert( Abc_NtkIsSeq(pNtk) );
+
+    Vec_IntFill( p->vAFlows, p->nSize, Abc_Float2Int( (float)0.0 ) );
+
+    // update all values iteratively
+    for ( c = 0; c < 7; c++ )
+    {
+        Abc_AigForEachAnd( pNtk, pObj, i )
+        {
+            AFlow = (float)1.0 + Seq_NodeGetFlow( Abc_ObjFanin0(pObj) ) + Seq_NodeGetFlow( Abc_ObjFanin1(pObj) );
+            AFlow /= Abc_ObjFanoutNum(pObj);
+            pObj->pNext = (void *)Abc_Float2Int( AFlow );
+        }
+        Abc_AigForEachAnd( pNtk, pObj, i )
+        {
+            AFlow = Abc_Int2Float( (int)pObj->pNext );
+            pObj->pNext = NULL;
+            Seq_NodeSetFlow( pObj, AFlow );
+
+//            printf( "%5d : %6.1f\n", pObj->Id, Seq_NodeGetFlow(pObj) );
+        }
+//        printf( "\n" );
+    }
+    return 1;
+}
+
 ////////////////////////////////////////////////////////////////////////
 ///                       END OF FILE                                ///
 ////////////////////////////////////////////////////////////////////////