Version abc50831

This commit is contained in:
Alan Mishchenko 2005-08-31 08:01:00 -07:00
parent 2b85f5ba64
commit ab7cb9c6ad
41 changed files with 4619 additions and 312 deletions

26
abc.dsp
View File

@ -237,6 +237,10 @@ SOURCE=.\src\base\abc\abcSweep.c
# End Source File
# Begin Source File
SOURCE=.\src\base\abc\abcSymm.c
# End Source File
# Begin Source File
SOURCE=.\src\base\abc\abcTiming.c
# End Source File
# Begin Source File
@ -321,6 +325,10 @@ SOURCE=.\src\base\io\ioReadEdif.c
# End Source File
# Begin Source File
SOURCE=.\src\base\io\ioReadEqn.c
# End Source File
# Begin Source File
SOURCE=.\src\base\io\ioReadPla.c
# End Source File
# Begin Source File
@ -345,6 +353,18 @@ SOURCE=.\src\base\io\ioWriteCnf.c
# End Source File
# Begin Source File
SOURCE=.\src\base\io\ioWriteDot.c
# End Source File
# Begin Source File
SOURCE=.\src\base\io\ioWriteEqn.c
# End Source File
# Begin Source File
SOURCE=.\src\base\io\ioWriteGml.c
# End Source File
# Begin Source File
SOURCE=.\src\base\io\ioWritePla.c
# End Source File
# End Group
@ -1413,7 +1433,11 @@ SOURCE=.\src\misc\extra\extra.h
# End Source File
# Begin Source File
SOURCE=.\src\misc\extra\extraUtilBdd.c
SOURCE=.\src\misc\extra\extraBddMisc.c
# End Source File
# Begin Source File
SOURCE=.\src\misc\extra\extraBddSymm.c
# End Source File
# Begin Source File

BIN
abc.opt

Binary file not shown.

579
abc.plg
View File

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

7
abc.rc
View File

@ -11,6 +11,7 @@ alias pl print_level
alias pio print_io
alias ps print_stats
alias psu print_supp
alias psy print_symm
alias q quit
alias r read
alias rl read_blif
@ -32,7 +33,7 @@ alias wl write_blif
alias wp write_pla
alias cnf "st; renode -c; write_cnf"
alias prove "st; renode -c; sat"
alias opt "b; renode; b; ps"
alias share "b; renode -m; fx; b; ps"
alias resyn "b; rw; rf; b; rwz; rfz; b; ps"
alias opt "b; renode; b"
alias share "b; renode -m; fx; b"
alias resyn "b; rw; rf; b; rw; rwz; b; rfz; rwz; b"

View File

@ -36,8 +36,11 @@ static int Abc_CommandPrintFanio ( Abc_Frame_t * pAbc, int argc, char ** argv
static int Abc_CommandPrintFactor ( Abc_Frame_t * pAbc, int argc, char ** argv );
static int Abc_CommandPrintLevel ( Abc_Frame_t * pAbc, int argc, char ** argv );
static int Abc_CommandPrintSupport ( Abc_Frame_t * pAbc, int argc, char ** argv );
static int Abc_CommandPrintSymms ( Abc_Frame_t * pAbc, int argc, char ** argv );
static int Abc_CommandShowBdd ( Abc_Frame_t * pAbc, int argc, char ** argv );
static int Abc_CommandShowCut ( Abc_Frame_t * pAbc, int argc, char ** argv );
static int Abc_CommandShowAig ( Abc_Frame_t * pAbc, int argc, char ** argv );
static int Abc_CommandCollapse ( Abc_Frame_t * pAbc, int argc, char ** argv );
static int Abc_CommandStrash ( Abc_Frame_t * pAbc, int argc, char ** argv );
@ -105,8 +108,11 @@ void Abc_Init( Abc_Frame_t * pAbc )
Cmd_CommandAdd( pAbc, "Printing", "print_factor", Abc_CommandPrintFactor, 0 );
Cmd_CommandAdd( pAbc, "Printing", "print_level", Abc_CommandPrintLevel, 0 );
Cmd_CommandAdd( pAbc, "Printing", "print_supp", Abc_CommandPrintSupport, 0 );
Cmd_CommandAdd( pAbc, "Printing", "print_symm", Abc_CommandPrintSymms, 0 );
Cmd_CommandAdd( pAbc, "Printing", "show_bdd", Abc_CommandShowBdd, 0 );
Cmd_CommandAdd( pAbc, "Printing", "show_cut", Abc_CommandShowCut, 0 );
Cmd_CommandAdd( pAbc, "Printing", "show_aig", Abc_CommandShowAig, 0 );
Cmd_CommandAdd( pAbc, "Synthesis", "collapse", Abc_CommandCollapse, 1 );
Cmd_CommandAdd( pAbc, "Synthesis", "strash", Abc_CommandStrash, 1 );
@ -297,9 +303,10 @@ int Abc_CommandPrintIo( Abc_Frame_t * pAbc, int argc, char ** argv )
return 0;
usage:
fprintf( pErr, "usage: print_io [-h]\n" );
fprintf( pErr, "usage: print_io [-h] <node>\n" );
fprintf( pErr, "\t prints the PIs/POs or fanins/fanouts of a node\n" );
fprintf( pErr, "\t-h : print the command usage\n");
fprintf( pErr, "\tnode : the node to print fanins/fanouts\n");
return 1;
}
@ -618,6 +625,78 @@ usage:
return 1;
}
/**Function*************************************************************
Synopsis []
Description []
SideEffects []
SeeAlso []
***********************************************************************/
int Abc_CommandPrintSymms( Abc_Frame_t * pAbc, int argc, char ** argv )
{
FILE * pOut, * pErr;
Abc_Ntk_t * pNtk;
int c;
int fUseBdds;
int fNaive;
int fVerbose;
extern void Abc_NtkSymmetries( Abc_Ntk_t * pNtk, int fUseBdds, int fNaive, int fVerbose );
pNtk = Abc_FrameReadNet(pAbc);
pOut = Abc_FrameReadOut(pAbc);
pErr = Abc_FrameReadErr(pAbc);
// set defaults
fUseBdds = 1;
fNaive = 0;
fVerbose = 0;
util_getopt_reset();
while ( ( c = util_getopt( argc, argv, "bnvh" ) ) != EOF )
{
switch ( c )
{
case 'b':
fUseBdds ^= 1;
break;
case 'n':
fNaive ^= 1;
break;
case 'v':
fVerbose ^= 1;
break;
case 'h':
goto usage;
default:
goto usage;
}
}
if ( pNtk == NULL )
{
fprintf( pErr, "Empty network.\n" );
return 1;
}
if ( !Abc_NtkIsStrash(pNtk) )
{
fprintf( pErr, "This command works only for AIGs.\n" );
return 1;
}
Abc_NtkSymmetries( pNtk, fUseBdds, fNaive, fVerbose );
return 0;
usage:
fprintf( pErr, "usage: print_symm [-nbvh]\n" );
fprintf( pErr, "\t computes symmetries of the PO functions\n" );
fprintf( pErr, "\t-b : enable efficient BDD-based computation [default = %s].\n", fUseBdds? "yes": "no" );
fprintf( pErr, "\t-n : enable naive BDD-based computation [default = %s].\n", fNaive? "yes": "no" );
fprintf( pErr, "\t-v : enable verbose output [default = %s].\n", fVerbose? "yes": "no" );
fprintf( pErr, "\t-h : print the command usage\n");
return 1;
}
/**Function*************************************************************
Synopsis []
@ -635,7 +714,7 @@ int Abc_CommandShowBdd( Abc_Frame_t * pAbc, int argc, char ** argv )
Abc_Ntk_t * pNtk;
Abc_Obj_t * pNode;
int c;
extern void Abc_NodePrintBdd( Abc_Obj_t * pNode );
extern void Abc_NodeShowBdd( Abc_Obj_t * pNode );
pNtk = Abc_FrameReadNet(pAbc);
pOut = Abc_FrameReadOut(pAbc);
@ -662,7 +741,7 @@ int Abc_CommandShowBdd( Abc_Frame_t * pAbc, int argc, char ** argv )
if ( !Abc_NtkIsBddLogic(pNtk) )
{
fprintf( pErr, "Printing BDDs can only be done for logic BDD networks.\n" );
fprintf( pErr, "Visualizing BDDs can only be done for logic BDD networks.\n" );
return 1;
}
@ -678,7 +757,7 @@ int Abc_CommandShowBdd( Abc_Frame_t * pAbc, int argc, char ** argv )
fprintf( pErr, "Cannot find node \"%s\".\n", argv[util_optind] );
return 1;
}
Abc_NodePrintBdd( pNode );
Abc_NodeShowBdd( pNode );
return 0;
usage:
@ -693,6 +772,168 @@ usage:
return 1;
}
/**Function*************************************************************
Synopsis []
Description []
SideEffects []
SeeAlso []
***********************************************************************/
int Abc_CommandShowCut( Abc_Frame_t * pAbc, int argc, char ** argv )
{
FILE * pOut, * pErr;
Abc_Ntk_t * pNtk;
Abc_Obj_t * pNode;
int c;
int nNodeSizeMax;
int nConeSizeMax;
extern void Abc_NodeShowCut( Abc_Obj_t * pNode, int nNodeSizeMax, int nConeSizeMax );
pNtk = Abc_FrameReadNet(pAbc);
pOut = Abc_FrameReadOut(pAbc);
pErr = Abc_FrameReadErr(pAbc);
// set defaults
nNodeSizeMax = 10;
nConeSizeMax = ABC_INFINITY;
util_getopt_reset();
while ( ( c = util_getopt( argc, argv, "NCh" ) ) != EOF )
{
switch ( c )
{
case 'N':
if ( util_optind >= argc )
{
fprintf( pErr, "Command line switch \"-N\" should be followed by an integer.\n" );
goto usage;
}
nNodeSizeMax = atoi(argv[util_optind]);
util_optind++;
if ( nNodeSizeMax < 0 )
goto usage;
break;
case 'C':
if ( util_optind >= argc )
{
fprintf( pErr, "Command line switch \"-C\" should be followed by an integer.\n" );
goto usage;
}
nConeSizeMax = atoi(argv[util_optind]);
util_optind++;
if ( nConeSizeMax < 0 )
goto usage;
break;
case 'h':
goto usage;
default:
goto usage;
}
}
if ( pNtk == NULL )
{
fprintf( pErr, "Empty network.\n" );
return 1;
}
if ( !Abc_NtkIsStrash(pNtk) )
{
fprintf( pErr, "Visualizing cuts only works for AIGs.\n" );
return 1;
}
if ( argc != util_optind + 1 )
{
fprintf( pErr, "Wrong number of auguments.\n" );
goto usage;
}
pNode = Abc_NtkFindNode( pNtk, argv[util_optind] );
if ( pNode == NULL )
{
fprintf( pErr, "Cannot find node \"%s\".\n", argv[util_optind] );
return 1;
}
Abc_NodeShowCut( pNode, nNodeSizeMax, nConeSizeMax );
return 0;
usage:
fprintf( pErr, "usage: show_cut [-N num] [-C num] [-h] <node>\n" );
fprintf( pErr, " visualizes the cut of a node using DOT and GSVIEW\n" );
#ifdef WIN32
fprintf( pErr, " \"dot.exe\" and \"gsview32.exe\" should be set in the paths\n" );
fprintf( pErr, " (\"gsview32.exe\" may be in \"C:\\Program Files\\Ghostgum\\gsview\\\")\n" );
#endif
fprintf( pErr, "\t-N num : the max size of the cut to be computed [default = %d]\n", nNodeSizeMax );
fprintf( pErr, "\t-C num : the max support of the containing cone [default = %d]\n", nConeSizeMax );
fprintf( pErr, "\tnode : the node to consider\n");
fprintf( pErr, "\t-h : print the command usage\n");
return 1;
}
/**Function*************************************************************
Synopsis []
Description []
SideEffects []
SeeAlso []
***********************************************************************/
int Abc_CommandShowAig( Abc_Frame_t * pAbc, int argc, char ** argv )
{
FILE * pOut, * pErr;
Abc_Ntk_t * pNtk;
int c;
extern void Abc_NtkShowAig( Abc_Ntk_t * pNtk );
pNtk = Abc_FrameReadNet(pAbc);
pOut = Abc_FrameReadOut(pAbc);
pErr = Abc_FrameReadErr(pAbc);
// set defaults
util_getopt_reset();
while ( ( c = util_getopt( argc, argv, "h" ) ) != EOF )
{
switch ( c )
{
case 'h':
goto usage;
default:
goto usage;
}
}
if ( pNtk == NULL )
{
fprintf( pErr, "Empty network.\n" );
return 1;
}
if ( !Abc_NtkIsStrash(pNtk) )
{
fprintf( pErr, "Visualizing AIG can only be done for AIGs.\n" );
return 1;
}
Abc_NtkShowAig( pNtk );
return 0;
usage:
fprintf( pErr, "usage: show_aig [-h]\n" );
fprintf( pErr, " visualizes the AIG with choices using DOT and GSVIEW\n" );
#ifdef WIN32
fprintf( pErr, " \"dot.exe\" and \"gsview32.exe\" should be set in the paths\n" );
fprintf( pErr, " (\"gsview32.exe\" may be in \"C:\\Program Files\\Ghostgum\\gsview\\\")\n" );
#endif
fprintf( pErr, "\t-h : print the command usage\n");
return 1;
}
/**Function*************************************************************
@ -745,7 +986,7 @@ int Abc_CommandCollapse( Abc_Frame_t * pAbc, int argc, char ** argv )
pNtkRes = Abc_NtkCollapse( pNtk, 1 );
else
{
pNtk = Abc_NtkStrash( pNtk, 0 );
pNtk = Abc_NtkStrash( pNtk, 0, 0 );
pNtkRes = Abc_NtkCollapse( pNtk, 1 );
Abc_NtkDelete( pNtk );
}
@ -783,6 +1024,7 @@ int Abc_CommandStrash( Abc_Frame_t * pAbc, int argc, char ** argv )
Abc_Ntk_t * pNtk, * pNtkRes;
int c;
int fAllNodes;
int fCleanup;
pNtk = Abc_FrameReadNet(pAbc);
pOut = Abc_FrameReadOut(pAbc);
@ -790,14 +1032,18 @@ int Abc_CommandStrash( Abc_Frame_t * pAbc, int argc, char ** argv )
// set defaults
fAllNodes = 0;
fCleanup = 1;
util_getopt_reset();
while ( ( c = util_getopt( argc, argv, "ah" ) ) != EOF )
while ( ( c = util_getopt( argc, argv, "ach" ) ) != EOF )
{
switch ( c )
{
case 'a':
fAllNodes ^= 1;
break;
case 'c':
fCleanup ^= 1;
break;
case 'h':
goto usage;
default:
@ -812,7 +1058,7 @@ int Abc_CommandStrash( Abc_Frame_t * pAbc, int argc, char ** argv )
}
// get the new network
pNtkRes = Abc_NtkStrash( pNtk, fAllNodes );
pNtkRes = Abc_NtkStrash( pNtk, fAllNodes, fCleanup );
if ( pNtkRes == NULL )
{
fprintf( pErr, "Strashing has failed.\n" );
@ -823,9 +1069,10 @@ int Abc_CommandStrash( Abc_Frame_t * pAbc, int argc, char ** argv )
return 0;
usage:
fprintf( pErr, "usage: strash [-ah]\n" );
fprintf( pErr, "usage: strash [-ach]\n" );
fprintf( pErr, "\t transforms combinational logic into an AIG\n" );
fprintf( pErr, "\t-a : toggles between using all nodes and DFS nodes [default = %s]\n", fAllNodes? "all": "DFS" );
fprintf( pErr, "\t-c : toggles cleanup to remove the dagling AIG nodes [default = %s]\n", fCleanup? "all": "DFS" );
fprintf( pErr, "\t-h : print the command usage\n");
return 1;
}
@ -882,7 +1129,7 @@ int Abc_CommandBalance( Abc_Frame_t * pAbc, int argc, char ** argv )
}
else
{
pNtkTemp = Abc_NtkStrash( pNtk, 0 );
pNtkTemp = Abc_NtkStrash( pNtk, 0, 0 );
if ( pNtkTemp == NULL )
{
fprintf( pErr, "Strashing before balancing has failed.\n" );
@ -1274,7 +1521,7 @@ int Abc_CommandDisjoint( Abc_Frame_t * pAbc, int argc, char ** argv )
// get the new network
if ( !Abc_NtkIsStrash(pNtk) )
{
pNtkNew = Abc_NtkStrash( pNtk, 0 );
pNtkNew = Abc_NtkStrash( pNtk, 0, 0 );
pNtkRes = Abc_NtkDsdGlobal( pNtkNew, fVerbose, fPrint, fShort );
Abc_NtkDelete( pNtkNew );
}
@ -1732,7 +1979,7 @@ int Abc_CommandFrames( Abc_Frame_t * pAbc, int argc, char ** argv )
// get the new network
if ( !Abc_NtkIsStrash(pNtk) )
{
pNtkTemp = Abc_NtkStrash( pNtk, 0 );
pNtkTemp = Abc_NtkStrash( pNtk, 0, 0 );
pNtkRes = Abc_NtkFrames( pNtkTemp, nFrames, fInitial );
Abc_NtkDelete( pNtkTemp );
}
@ -2424,7 +2671,7 @@ int Abc_CommandFraig( Abc_Frame_t * pAbc, int argc, char ** argv )
pNtkRes = Abc_NtkFraig( pNtk, &Params, fAllNodes );
else
{
pNtk = Abc_NtkStrash( pNtk, 0 );
pNtk = Abc_NtkStrash( pNtk, fAllNodes, !fAllNodes );
pNtkRes = Abc_NtkFraig( pNtk, &Params, fAllNodes );
Abc_NtkDelete( pNtk );
}
@ -2845,7 +3092,7 @@ int Abc_CommandMap( Abc_Frame_t * pAbc, int argc, char ** argv )
if ( !Abc_NtkIsStrash(pNtk) )
{
pNtk = Abc_NtkStrash( pNtk, 0 );
pNtk = Abc_NtkStrash( pNtk, 0, 0 );
if ( pNtk == NULL )
{
fprintf( pErr, "Strashing before mapping has failed.\n" );
@ -3087,8 +3334,10 @@ int Abc_CommandSuperChoice( Abc_Frame_t * pAbc, int argc, char ** argv )
usage:
fprintf( pErr, "usage: sc [-h]\n" );
fprintf( pErr, "\t performs superchoicing\n" );
fprintf( pErr, "\t-h : print the command usage\n");
fprintf( pErr, "\t performs superchoicing\n" );
fprintf( pErr, "\t (accumulate: \"r file.blif; rsup; b; sc; f -ac; wb file_sc.blif\")\n" );
fprintf( pErr, "\t (map without supergate library: \"r file_sc.blif; ft; map\")\n" );
fprintf( pErr, "\t-h : print the command usage\n");
return 1;
}
@ -3146,7 +3395,7 @@ int Abc_CommandFpga( Abc_Frame_t * pAbc, int argc, char ** argv )
if ( !Abc_NtkIsStrash(pNtk) )
{
// strash and balance the network
pNtk = Abc_NtkStrash( pNtk, 0 );
pNtk = Abc_NtkStrash( pNtk, 0, 0 );
if ( pNtk == NULL )
{
fprintf( pErr, "Strashing before FPGA mapping has failed.\n" );

View File

@ -51,7 +51,7 @@ typedef enum {
ABC_TYPE_OTHER // 5: unused
} Abc_NtkType_t;
// functionality types
// network functionality
typedef enum {
ABC_FUNC_NONE, // 0: unknown
ABC_FUNC_SOP, // 1: sum-of-products
@ -155,13 +155,16 @@ struct Abc_Ntk_t_
int nPos; // the number of primary outputs
// the functionality manager
void * pManFunc; // AIG manager, BDD manager, or memory manager for SOPs
// the global functions (BDDs)
void * pManGlob; // the BDD manager
Vec_Ptr_t * vFuncsGlob; // the BDDs of CO functions
// the timing manager (for mapped networks)
Abc_ManTime_t * pManTime; // stores arrival/required times for all nodes
// the cut manager (for AIGs)
void * pManCut; // stores information about the cuts computed for the nodes
// level information (for AIGs)
int LevelMax; // maximum number of levels
Vec_Int_t * vLevelsR; // level in the reverse topological order
Vec_Int_t * vLevelsR; // level in the reverse topological order
// the external don't-care if given
Abc_Ntk_t * pExdc; // the EXDC network
// miscellaneous data members
@ -401,8 +404,11 @@ extern void Abc_AigDeleteNode( Abc_Aig_t * pMan, Abc_Obj_t * pOld
extern bool Abc_AigNodeHasComplFanoutEdge( Abc_Obj_t * pNode );
extern bool Abc_AigNodeHasComplFanoutEdgeTrav( Abc_Obj_t * pNode );
extern void Abc_AigPrintNode( Abc_Obj_t * pNode );
extern bool Abc_AigNodeIsAcyclic( Abc_Obj_t * pNode, Abc_Obj_t * pRoot );
/*=== abcAttach.c ==========================================================*/
extern int Abc_NtkAttach( Abc_Ntk_t * pNtk );
/*=== abcBalance.c ==========================================================*/
extern Abc_Ntk_t * Abc_NtkBalance( Abc_Ntk_t * pNtk, bool fDuplicate );
/*=== abcCheck.c ==========================================================*/
extern bool Abc_NtkCheck( Abc_Ntk_t * pNtk );
extern bool Abc_NtkCheckObj( Abc_Ntk_t * pNtk, Abc_Obj_t * pObj );
@ -410,7 +416,7 @@ extern bool Abc_NtkCompareSignals( Abc_Ntk_t * pNtk1, Abc_Ntk_t *
/*=== abcCollapse.c ==========================================================*/
extern Abc_Ntk_t * Abc_NtkCollapse( Abc_Ntk_t * pNtk, int fVerbose );
extern DdManager * Abc_NtkGlobalBdds( Abc_Ntk_t * pNtk, int fLatchOnly );
extern void Abc_NtkFreeGlobalBdds( DdManager * dd, Abc_Ntk_t * pNtk );
extern void Abc_NtkFreeGlobalBdds( Abc_Ntk_t * pNtk );
/*=== abcCreate.c ==========================================================*/
extern Abc_Ntk_t * Abc_NtkAlloc( Abc_NtkType_t Type, Abc_NtkFunc_t Func );
extern Abc_Ntk_t * Abc_NtkStartFrom( Abc_Ntk_t * pNtk, Abc_NtkType_t Type, Abc_NtkFunc_t Func );
@ -475,6 +481,7 @@ extern char * Abc_ConvertBddToSop( Extra_MmFlex_t * pMan, DdManager
extern int Abc_NtkBddToSop( Abc_Ntk_t * pNtk );
extern void Abc_NodeBddToCnf( Abc_Obj_t * pNode, Extra_MmFlex_t * pMmMan, Vec_Str_t * vCube, char ** ppSop0, char ** ppSop1 );
extern int Abc_CountZddCubes( DdManager * dd, DdNode * zCover );
extern void Abc_NtkLogicMakeDirectSops( Abc_Ntk_t * pNtk );
/*=== abcLatch.c ==========================================================*/
extern bool Abc_NtkLatchIsSelfFeed( Abc_Obj_t * pLatch );
extern int Abc_NtkCountSelfFeedLatches( Abc_Ntk_t * pNtk );
@ -519,13 +526,15 @@ extern void Abc_NodePrintFactor( FILE * pFile, Abc_Obj_t * pNode )
extern void Abc_NtkPrintLevel( FILE * pFile, Abc_Ntk_t * pNtk, int fProfile );
extern void Abc_NodePrintLevel( FILE * pFile, Abc_Obj_t * pNode );
/*=== abcReconv.c ==========================================================*/
extern Abc_ManCut_t * Abc_NtkManCutStart( int nNodeSizeMax, int nConeSizeMax );
extern Abc_ManCut_t * Abc_NtkManCutStart( int nNodeSizeMax, int nConeSizeMax, int nNodeFanStop, int nConeFanStop );
extern void Abc_NtkManCutStop( Abc_ManCut_t * p );
extern Vec_Ptr_t * Abc_NtkManCutReadLeaves( Abc_ManCut_t * p );
extern Vec_Ptr_t * Abc_NtkManCutReadCutLarge( Abc_ManCut_t * p );
extern Vec_Ptr_t * Abc_NtkManCutReadVisited( Abc_ManCut_t * p );
extern Vec_Ptr_t * Abc_NodeFindCut( Abc_ManCut_t * p, Abc_Obj_t * pRoot, bool fContain );
extern void Abc_NodeConeCollect( Abc_Obj_t ** ppRoots, int nRoots, Vec_Ptr_t * vFanins, Vec_Ptr_t * vVisited, int fIncludeFanins );
extern DdNode * Abc_NodeConeBdd( DdManager * dd, DdNode ** pbVars, Abc_Obj_t * pNode, Vec_Ptr_t * vFanins, Vec_Ptr_t * vVisited );
extern DdNode * Abc_NodeConeDcs( DdManager * dd, DdNode ** pbVarsX, DdNode ** pbVarsY, Vec_Ptr_t * vLeaves, Vec_Ptr_t * vRoots, Vec_Ptr_t * vVisited );
extern void Abc_NodeCollectTfoCands( Abc_Ntk_t * pNtk, Abc_Obj_t * pRoot, Vec_Ptr_t * vFanins, int LevelMax, Vec_Vec_t * vLevels, Vec_Ptr_t * vResult );
extern Vec_Ptr_t * Abc_NodeCollectTfoCands( Abc_ManCut_t * p, Abc_Obj_t * pRoot, Vec_Ptr_t * vFanins, int LevelMax );
/*=== abcRefs.c ==========================================================*/
extern int Abc_NodeMffcSize( Abc_Obj_t * pNode );
extern int Abc_NodeMffcLabel( Abc_Obj_t * pNode );
@ -576,12 +585,11 @@ extern bool Abc_SopCheck( char * pSop, int nFanins );
extern void Abc_SopWriteCnf( FILE * pFile, char * pClauses, Vec_Int_t * vVars );
extern void Abc_SopAddCnfToSolver( solver * pSat, char * pClauses, Vec_Int_t * vVars, Vec_Int_t * vTemp );
/*=== abcStrash.c ==========================================================*/
extern Abc_Ntk_t * Abc_NtkStrash( Abc_Ntk_t * pNtk, bool fAllNodes );
extern Abc_Ntk_t * Abc_NtkStrash( Abc_Ntk_t * pNtk, bool fAllNodes, bool fCleanup );
extern Abc_Obj_t * Abc_NodeStrash( Abc_Aig_t * pMan, Abc_Obj_t * pNode );
extern Abc_Obj_t * Abc_NodeStrashDec( Abc_Aig_t * pMan, Vec_Ptr_t * vFanins, Vec_Int_t * vForm );
extern int Abc_NodeStrashDecCount( Abc_Aig_t * pMan, Abc_Obj_t * pRoot, Vec_Ptr_t * vFanins, Vec_Int_t * vForm, Vec_Int_t * vLevels, int NodeMax, int LevelMax );
extern int Abc_NtkAppend( Abc_Ntk_t * pNtk1, Abc_Ntk_t * pNtk2 );
extern Abc_Ntk_t * Abc_NtkBalance( Abc_Ntk_t * pNtk, bool fDuplicate );
/*=== abcSweep.c ==========================================================*/
extern bool Abc_NtkFraigSweep( Abc_Ntk_t * pNtk, int fUseInv, int fVerbose );
extern int Abc_NtkCleanup( Abc_Ntk_t * pNtk, int fVerbose );
@ -643,6 +651,7 @@ extern char ** Abc_NtkCollectCioNames( Abc_Ntk_t * pNtk, int fCollect
extern void Abc_NtkAlphaOrderSignals( Abc_Ntk_t * pNtk, int fComb );
extern void Abc_NtkShortNames( Abc_Ntk_t * pNtk );
extern Vec_Int_t * Abc_NtkFanoutCounts( Abc_Ntk_t * pNtk );
extern Vec_Ptr_t * Abc_NtkCollectObjects( Abc_Ntk_t * pNtk );
////////////////////////////////////////////////////////////////////////
/// END OF FILE ///

View File

@ -705,8 +705,10 @@ void Abc_AigReplace_int( Abc_Aig_t * pMan )
assert( iFanin == 0 || iFanin == 1 );
// get the new fanin
pFanin1 = Abc_ObjNotCond( pNew, Abc_ObjFaninC(pFanout, iFanin) );
assert( Abc_ObjRegular(pFanin1) != pFanout );
// get another fanin
pFanin2 = Abc_ObjChild( pFanout, iFanin ^ 1 );
assert( Abc_ObjRegular(pFanin2) != pFanout );
// check if the node with these fanins exists
if ( pFanoutNew = Abc_AigAndLookup( pMan, pFanin1, pFanin2 ) )
{ // such node exists (it may be a constant)
@ -732,6 +734,7 @@ void Abc_AigReplace_int( Abc_Aig_t * pMan )
Abc_ObjRemoveFanins( pFanout );
// recreate the old fanout with new fanins and add it to the table
Abc_AigAndCreateFrom( pMan, pFanin1, pFanin2, pFanout );
assert( Abc_AigNodeIsAcyclic(pFanout, pFanout) );
// schedule the updated fanout for updating direct level
assert( pFanout->fMarkA == 0 );
@ -876,6 +879,7 @@ void Abc_AigUpdateLevel_int( Abc_Aig_t * pMan )
if ( pNode == NULL )
continue;
assert( Abc_ObjIsNode(pNode) );
assert( (int)pNode->Level == i );
// clean the mark
assert( pNode->fMarkA == 1 );
pNode->fMarkA = 0;
@ -931,6 +935,7 @@ void Abc_AigUpdateLevelR_int( Abc_Aig_t * pMan )
if ( pNode == NULL )
continue;
assert( Abc_ObjIsNode(pNode) );
assert( Abc_NodeReadReverseLevel(pNode) == i );
// clean the mark
assert( pNode->fMarkB == 1 );
pNode->fMarkB = 0;
@ -1113,6 +1118,56 @@ void Abc_AigPrintNode( Abc_Obj_t * pNode )
printf( "\n" );
}
/**Function*************************************************************
Synopsis [Check if the node has a combination loop of depth 1 or 2.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
bool Abc_AigNodeIsAcyclic( Abc_Obj_t * pNode, Abc_Obj_t * pRoot )
{
Abc_Obj_t * pFanin0, * pFanin1;
Abc_Obj_t * pChild00, * pChild01;
Abc_Obj_t * pChild10, * pChild11;
if ( !Abc_NodeIsAigAnd(pNode) )
return 1;
pFanin0 = Abc_ObjFanin0(pNode);
pFanin1 = Abc_ObjFanin1(pNode);
if ( pRoot == pFanin0 || pRoot == pFanin1 )
return 0;
if ( Abc_ObjIsCi(pFanin0) )
{
pChild00 = NULL;
pChild01 = NULL;
}
else
{
pChild00 = Abc_ObjFanin0(pFanin0);
pChild01 = Abc_ObjFanin1(pFanin0);
if ( pRoot == pChild00 || pRoot == pChild01 )
return 0;
}
if ( Abc_ObjIsCi(pFanin1) )
{
pChild10 = NULL;
pChild11 = NULL;
}
else
{
pChild10 = Abc_ObjFanin0(pFanin1);
pChild11 = Abc_ObjFanin1(pFanin1);
if ( pRoot == pChild10 || pRoot == pChild11 )
return 0;
}
return 1;
}
////////////////////////////////////////////////////////////////////////
/// END OF FILE ///
////////////////////////////////////////////////////////////////////////

View File

@ -25,7 +25,7 @@
////////////////////////////////////////////////////////////////////////
static DdNode * Abc_NtkGlobalBdds_rec( DdManager * dd, Abc_Obj_t * pNode );
static Abc_Ntk_t * Abc_NtkFromGlobalBdds( DdManager * dd, Abc_Ntk_t * pNtk );
static Abc_Ntk_t * Abc_NtkFromGlobalBdds( Abc_Ntk_t * pNtk );
static Abc_Obj_t * Abc_NodeFromGlobalBdds( Abc_Ntk_t * pNtkNew, DdManager * dd, DdNode * bFunc );
////////////////////////////////////////////////////////////////////////
@ -47,26 +47,26 @@ Abc_Ntk_t * Abc_NtkCollapse( Abc_Ntk_t * pNtk, int fVerbose )
{
int fCheck = 1;
Abc_Ntk_t * pNtkNew;
DdManager * dd;
assert( Abc_NtkIsStrash(pNtk) );
// compute the global BDDs
dd = Abc_NtkGlobalBdds( pNtk, 0 );
if ( dd == NULL )
if ( Abc_NtkGlobalBdds(pNtk, 0) == NULL )
return NULL;
if ( fVerbose )
printf( "The shared BDD size is %d nodes.\n", Cudd_ReadKeys(dd) - Cudd_ReadDead(dd) );
printf( "The shared BDD size is %d nodes.\n", Cudd_ReadKeys(pNtk->pManGlob) - Cudd_ReadDead(pNtk->pManGlob) );
// create the new network
pNtkNew = Abc_NtkFromGlobalBdds( dd, pNtk );
Abc_NtkFreeGlobalBdds( dd, pNtk );
pNtkNew = Abc_NtkFromGlobalBdds( pNtk );
Abc_NtkFreeGlobalBdds( pNtk );
if ( pNtkNew == NULL )
{
Cudd_Quit( dd );
Cudd_Quit( pNtk->pManGlob );
pNtk->pManGlob = NULL;
return NULL;
}
Extra_StopManager( dd );
Extra_StopManager( pNtk->pManGlob );
pNtk->pManGlob = NULL;
// make the network minimum base
Abc_NtkMinimumBase( pNtkNew );
@ -96,12 +96,14 @@ DdManager * Abc_NtkGlobalBdds( Abc_Ntk_t * pNtk, int fLatchOnly )
{
int fReorder = 1;
ProgressBar * pProgress;
Vec_Ptr_t * vFuncsGlob;
Abc_Obj_t * pNode;
DdNode * bFunc;
DdManager * dd;
int i;
// start the manager
assert( pNtk->pManGlob == NULL );
dd = Cudd_Init( Abc_NtkCiNum(pNtk), 0, CUDD_UNIQUE_SLOTS, CUDD_CACHE_SLOTS, 0 );
if ( fReorder )
Cudd_AutodynEnable( dd, CUDD_REORDER_SYMM_SIFT );
@ -114,6 +116,7 @@ DdManager * Abc_NtkGlobalBdds( Abc_Ntk_t * pNtk, int fLatchOnly )
pNode = Abc_AigConst1( pNtk->pManFunc );
pNode->pCopy = (Abc_Obj_t *)dd->one; Cudd_Ref( dd->one );
vFuncsGlob = Vec_PtrAlloc( 100 );
if ( fLatchOnly )
{
// construct the BDDs
@ -129,8 +132,8 @@ DdManager * Abc_NtkGlobalBdds( Abc_Ntk_t * pNtk, int fLatchOnly )
Cudd_Quit( dd );
return NULL;
}
bFunc = Cudd_NotCond( bFunc, Abc_ObjFaninC0(pNode) );
pNode->pNext = (Abc_Obj_t *)bFunc; Cudd_Ref( bFunc );
bFunc = Cudd_NotCond( bFunc, Abc_ObjFaninC0(pNode) ); Cudd_Ref( bFunc );
Vec_PtrPush( vFuncsGlob, bFunc );
}
Extra_ProgressBarStop( pProgress );
}
@ -149,8 +152,8 @@ DdManager * Abc_NtkGlobalBdds( Abc_Ntk_t * pNtk, int fLatchOnly )
Cudd_Quit( dd );
return NULL;
}
bFunc = Cudd_NotCond( bFunc, Abc_ObjFaninC0(pNode) );
pNode->pNext = (Abc_Obj_t *)bFunc; Cudd_Ref( bFunc );
bFunc = Cudd_NotCond( bFunc, Abc_ObjFaninC0(pNode) ); Cudd_Ref( bFunc );
Vec_PtrPush( vFuncsGlob, bFunc );
}
Extra_ProgressBarStop( pProgress );
}
@ -168,6 +171,8 @@ DdManager * Abc_NtkGlobalBdds( Abc_Ntk_t * pNtk, int fLatchOnly )
Cudd_ReduceHeap( dd, CUDD_REORDER_SYMM_SIFT, 1 );
Cudd_AutodynDisable( dd );
}
pNtk->pManGlob = dd;
pNtk->vFuncsGlob = vFuncsGlob;
return dd;
}
@ -223,11 +228,12 @@ DdNode * Abc_NtkGlobalBdds_rec( DdManager * dd, Abc_Obj_t * pNode )
SeeAlso []
***********************************************************************/
Abc_Ntk_t * Abc_NtkFromGlobalBdds( DdManager * dd, Abc_Ntk_t * pNtk )
Abc_Ntk_t * Abc_NtkFromGlobalBdds( Abc_Ntk_t * pNtk )
{
ProgressBar * pProgress;
Abc_Ntk_t * pNtkNew;
Abc_Obj_t * pNode, * pNodeNew;
DdManager * dd = pNtk->pManGlob;
int i;
// start the new network
pNtkNew = Abc_NtkStartFrom( pNtk, ABC_TYPE_LOGIC, ABC_FUNC_BDD );
@ -238,7 +244,7 @@ Abc_Ntk_t * Abc_NtkFromGlobalBdds( DdManager * dd, Abc_Ntk_t * pNtk )
Abc_NtkForEachCo( pNtk, pNode, i )
{
Extra_ProgressBarUpdate( pProgress, i, NULL );
pNodeNew = Abc_NodeFromGlobalBdds( pNtkNew, dd, (DdNode *)pNode->pNext );
pNodeNew = Abc_NodeFromGlobalBdds( pNtkNew, dd, Vec_PtrEntry(pNtk->vFuncsGlob, i) );
Abc_ObjAddFanin( pNode->pCopy, pNodeNew );
}
Extra_ProgressBarStop( pProgress );
@ -281,17 +287,16 @@ Abc_Obj_t * Abc_NodeFromGlobalBdds( Abc_Ntk_t * pNtkNew, DdManager * dd, DdNode
SeeAlso []
***********************************************************************/
void Abc_NtkFreeGlobalBdds( DdManager * dd, Abc_Ntk_t * pNtk )
void Abc_NtkFreeGlobalBdds( Abc_Ntk_t * pNtk )
{
Abc_Obj_t * pNode;
DdNode * bFunc;
int i;
Abc_NtkForEachCo( pNtk, pNode, i )
{
if ( pNode->pNext == NULL )
continue;
Cudd_RecursiveDeref( dd, (DdNode *)pNode->pNext );
pNode->pNext = NULL;
}
assert( pNtk->pManGlob );
assert( pNtk->vFuncsGlob );
Vec_PtrForEachEntry( pNtk->vFuncsGlob, bFunc, i )
Cudd_RecursiveDeref( pNtk->pManGlob, bFunc );
Vec_PtrFree( pNtk->vFuncsGlob );
pNtk->vFuncsGlob = NULL;
}

View File

@ -818,7 +818,7 @@ Abc_Obj_t * Abc_NtkFindNode( Abc_Ntk_t * pNtk, char * pName )
// find the internal node
if ( pName[0] != '[' || pName[strlen(pName)-1] != ']' )
{
printf( "Node \"%s\" has non-standard name (expected name is \"[integer]\").\n", pName );
printf( "Name \"%s\" is not found among CIs/COs (internal name looks like this: \"[integer]\").\n", pName );
return NULL;
}
Num = atoi( pName + 1 );

View File

@ -25,8 +25,7 @@
/// DECLARATIONS ///
////////////////////////////////////////////////////////////////////////
static Abc_Ntk_t * Abc_NtkDsdInternal( DdManager * dd, Abc_Ntk_t * pNtk, bool fVerbose, bool fPrint, bool fShort );
static Dsd_Manager_t * Abc_NtkDsdPerform( DdManager * dd, Abc_Ntk_t * pNtk, bool fVerbose );
static Abc_Ntk_t * Abc_NtkDsdInternal( Abc_Ntk_t * pNtk, bool fVerbose, bool fPrint, bool fShort );
static void Abc_NtkDsdConstruct( Dsd_Manager_t * pManDsd, Abc_Ntk_t * pNtk, Abc_Ntk_t * pNtkNew );
static Abc_Obj_t * Abc_NtkDsdConstructNode( Dsd_Manager_t * pManDsd, Dsd_Node_t * pNodeDsd, Abc_Ntk_t * pNtkNew );
@ -58,25 +57,25 @@ Abc_Ntk_t * Abc_NtkDsdGlobal( Abc_Ntk_t * pNtk, bool fVerbose, bool fPrint, bool
{
int fCheck = 1;
Abc_Ntk_t * pNtkNew;
DdManager * dd;
assert( Abc_NtkIsStrash(pNtk) );
// perform FPGA mapping
dd = Abc_NtkGlobalBdds( pNtk, 0 );
if ( dd == NULL )
if ( Abc_NtkGlobalBdds(pNtk, 0) == NULL )
return NULL;
if ( fVerbose )
printf( "The shared BDD size is %d nodes.\n", Cudd_ReadKeys(dd) - Cudd_ReadDead(dd) );
printf( "The shared BDD size is %d nodes.\n", Cudd_ReadKeys(pNtk->pManGlob) - Cudd_ReadDead(pNtk->pManGlob) );
// transform the result of mapping into a BDD network
pNtkNew = Abc_NtkDsdInternal( dd, pNtk, fVerbose, fPrint, fShort );
pNtkNew = Abc_NtkDsdInternal( pNtk, fVerbose, fPrint, fShort );
if ( pNtkNew == NULL )
{
Cudd_Quit( dd );
Cudd_Quit( pNtk->pManGlob );
pNtk->pManGlob = NULL;
return NULL;
}
Extra_StopManager( dd );
Extra_StopManager( pNtk->pManGlob );
pNtk->pManGlob = NULL;
// make sure that everything is okay
if ( fCheck && !Abc_NtkCheck( pNtkNew ) )
@ -99,17 +98,33 @@ Abc_Ntk_t * Abc_NtkDsdGlobal( Abc_Ntk_t * pNtk, bool fVerbose, bool fPrint, bool
SeeAlso []
***********************************************************************/
Abc_Ntk_t * Abc_NtkDsdInternal( DdManager * dd, Abc_Ntk_t * pNtk, bool fVerbose, bool fPrint, bool fShort )
Abc_Ntk_t * Abc_NtkDsdInternal( Abc_Ntk_t * pNtk, bool fVerbose, bool fPrint, bool fShort )
{
DdManager * dd = pNtk->pManGlob;
Dsd_Manager_t * pManDsd;
Abc_Ntk_t * pNtkNew;
DdNode * bFunc;
char ** ppNamesCi, ** ppNamesCo;
Abc_Obj_t * pObj;
int i;
// complement the global functions
Abc_NtkForEachCo( pNtk, pObj, i )
{
bFunc = Vec_PtrEntry(pNtk->vFuncsGlob, i);
Vec_PtrWriteEntry(pNtk->vFuncsGlob, i, Cudd_NotCond(bFunc, Abc_ObjFaninC0(pObj)) );
}
// perform the decomposition
pManDsd = Abc_NtkDsdPerform( dd, pNtk, fVerbose );
Abc_NtkFreeGlobalBdds( dd, pNtk );
assert( Vec_PtrSize(pNtk->vFuncsGlob) == Abc_NtkCoNum(pNtk) );
pManDsd = Dsd_ManagerStart( dd, Abc_NtkCiNum(pNtk), fVerbose );
Dsd_Decompose( pManDsd, (DdNode **)pNtk->vFuncsGlob->pArray, Abc_NtkCoNum(pNtk) );
Abc_NtkFreeGlobalBdds( pNtk );
if ( pManDsd == NULL )
{
Cudd_Quit( dd );
return NULL;
}
// start the new network
pNtkNew = Abc_NtkStartFrom( pNtk, ABC_TYPE_LOGIC, ABC_FUNC_BDD );
@ -119,6 +134,8 @@ Abc_Ntk_t * Abc_NtkDsdInternal( DdManager * dd, Abc_Ntk_t * pNtk, bool fVerbose,
Abc_NtkDsdConstruct( pManDsd, pNtk, pNtkNew );
// finalize the new network
Abc_NtkFinalize( pNtk, pNtkNew );
// fix the problem with complemented and duplicated CO edges
Abc_NtkLogicMakeSimpleCos( pNtkNew, 0 );
if ( fPrint )
{
@ -134,39 +151,6 @@ Abc_Ntk_t * Abc_NtkDsdInternal( DdManager * dd, Abc_Ntk_t * pNtk, bool fVerbose,
return pNtkNew;
}
/**Function*************************************************************
Synopsis [Performs DSD by creating the manager and decomposing the functions.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
Dsd_Manager_t * Abc_NtkDsdPerform( DdManager * dd, Abc_Ntk_t * pNtk, bool fVerbose )
{
Dsd_Manager_t * pManDsd;
DdNode ** pbFuncsGlo;
Abc_Obj_t * pNode;
int i;
// collect global functions into the array
pbFuncsGlo = ALLOC( DdNode *, Abc_NtkCoNum(pNtk) );
Abc_NtkForEachCo( pNtk, pNode, i )
{
pbFuncsGlo[i] = Cudd_NotCond( pNode->pNext, Abc_ObjFaninC0(pNode) );
//printf( "Output %3d : Support size = %3d. Nodes = %5d.\n", i, Cudd_SupportSize(dd, pbFuncsGlo[i]), Cudd_DagSize(pbFuncsGlo[i]) );
}
// start the DSD manager and decompose global functions
pManDsd = Dsd_ManagerStart( dd, Abc_NtkCiNum(pNtk), fVerbose );
Dsd_Decompose( pManDsd, pbFuncsGlo, Abc_NtkCoNum(pNtk) );
FREE( pbFuncsGlo );
return pManDsd;
}
/**Function*************************************************************
Synopsis [Constructs the decomposed network.]

View File

@ -433,7 +433,7 @@ int Abc_NtkFraigStore( Abc_Ntk_t * pNtk )
if ( pStore == NULL )
{
// start the stored network
pStore = Abc_NtkStrash( pNtk, 0 );
pStore = Abc_NtkStrash( pNtk, 0, 0 );
if ( pStore == NULL )
{
printf( "Abc_NtkFraigStore: Initial strashing has failed.\n" );

View File

@ -128,6 +128,57 @@ DdNode * Abc_ConvertSopToBdd( DdManager * dd, char * pSop, int nFanins )
return bRes;
}
/**Function*************************************************************
Synopsis [Removes complemented SOP covers.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
void Abc_NtkLogicMakeDirectSops( Abc_Ntk_t * pNtk )
{
DdManager * dd;
DdNode * bFunc;
Vec_Str_t * vCube;
Abc_Obj_t * pNode;
int nFaninsMax, fFound, i;
assert( Abc_NtkIsSopLogic(pNtk) );
// check if there are nodes with complemented SOPs
fFound = 0;
Abc_NtkForEachNode( pNtk, pNode, i )
if ( Abc_SopIsComplement(pNode->pData) )
{
fFound = 1;
break;
}
if ( !fFound )
return;
// start the BDD package
nFaninsMax = Abc_NtkGetFaninMax( pNtk );
if ( nFaninsMax == 0 )
printf( "Warning: The network has only constant nodes.\n" );
dd = Cudd_Init( nFaninsMax, 0, CUDD_UNIQUE_SLOTS, CUDD_CACHE_SLOTS, 0 );
// change the cover of negated nodes
vCube = Vec_StrAlloc( 100 );
Abc_NtkForEachNode( pNtk, pNode, i )
if ( Abc_SopIsComplement(pNode->pData) )
{
bFunc = Abc_ConvertSopToBdd( dd, pNode->pData, Abc_ObjFaninNum(pNode) ); Cudd_Ref( bFunc );
pNode->pData = Abc_ConvertBddToSop( pNtk->pManFunc, dd, bFunc, bFunc, Abc_ObjFaninNum(pNode), vCube, 1 );
Cudd_RecursiveDeref( dd, bFunc );
assert( !Abc_SopIsComplement(pNode->pData) );
}
Vec_StrFree( vCube );
Extra_StopManager( dd );
}

View File

@ -55,8 +55,8 @@ Abc_Ntk_t * Abc_NtkMiter( Abc_Ntk_t * pNtk1, Abc_Ntk_t * pNtk2, int fComb )
if ( !Abc_NtkCompareSignals( pNtk1, pNtk2, fComb ) )
return NULL;
// make sure the circuits are strashed
fRemove1 = (!Abc_NtkIsStrash(pNtk1)) && (pNtk1 = Abc_NtkStrash(pNtk1, 0));
fRemove2 = (!Abc_NtkIsStrash(pNtk2)) && (pNtk2 = Abc_NtkStrash(pNtk2, 0));
fRemove1 = (!Abc_NtkIsStrash(pNtk1)) && (pNtk1 = Abc_NtkStrash(pNtk1, 0, 0));
fRemove2 = (!Abc_NtkIsStrash(pNtk2)) && (pNtk2 = Abc_NtkStrash(pNtk2, 0, 0));
if ( pNtk1 && pNtk2 )
pTemp = Abc_NtkMiterInt( pNtk1, pNtk2, fComb );
if ( fRemove1 ) Abc_NtkDelete( pNtk1 );

View File

@ -44,8 +44,8 @@ void Abc_NtkPrintStats( FILE * pFile, Abc_Ntk_t * pNtk, int fFactored )
{
int Num;
fprintf( pFile, "%-15s:", pNtk->pName );
fprintf( pFile, " i/o = %4d/%4d", Abc_NtkPiNum(pNtk), Abc_NtkPoNum(pNtk) );
fprintf( pFile, "%-13s:", pNtk->pName );
fprintf( pFile, " i/o = %4d/%4d", Abc_NtkPiNum(pNtk), Abc_NtkPoNum(pNtk) );
if ( !Abc_NtkIsSeq(pNtk) )
fprintf( pFile, " lat = %4d", Abc_NtkLatchNum(pNtk) );

View File

@ -30,14 +30,19 @@ struct Abc_ManCut_t_
// user specified parameters
int nNodeSizeMax; // the limit on the size of the supernode
int nConeSizeMax; // the limit on the size of the containing cone
int nNodeFanStop; // the limit on the size of the supernode
int nConeFanStop; // the limit on the size of the containing cone
// internal parameters
Vec_Ptr_t * vFaninsNode; // fanins of the supernode
Vec_Ptr_t * vFaninsCone; // fanins of the containing cone
Vec_Ptr_t * vNodeLeaves; // fanins of the collapsed node (the cut)
Vec_Ptr_t * vConeLeaves; // fanins of the containing cone
Vec_Ptr_t * vVisited; // the visited nodes
Vec_Vec_t * vLevels; // the data structure to compute TFO nodes
Vec_Ptr_t * vNodesTfo; // the nodes in the TFO of the cut
};
static int Abc_NodeFindCut_int( Vec_Ptr_t * vFanins, int nSizeLimit );
static void Abc_NodesMarkCollect_rec( Abc_Obj_t * pNode, Vec_Ptr_t * vVisited );
static int Abc_NodeBuildCutLevelOne_int( Vec_Ptr_t * vVisited, Vec_Ptr_t * vLeaves, int nSizeLimit, int nFaninLimit );
static int Abc_NodeBuildCutLevelTwo_int( Vec_Ptr_t * vVisited, Vec_Ptr_t * vLeaves, int nFaninLimit );
static void Abc_NodeConeMarkCollect_rec( Abc_Obj_t * pNode, Vec_Ptr_t * vVisited );
////////////////////////////////////////////////////////////////////////
/// FUNCTION DEFITIONS ///
@ -92,45 +97,142 @@ static inline void Abc_NodesUnmark( Vec_Ptr_t * vVisited )
SeeAlso []
***********************************************************************/
static inline void Abc_NodesUnmarkBoth( Vec_Ptr_t * vVisited )
static inline void Abc_NodesUnmarkB( Vec_Ptr_t * vVisited )
{
Abc_Obj_t * pNode;
int i;
Vec_PtrForEachEntry( vVisited, pNode, i )
pNode->fMarkA = pNode->fMarkB = 0;
pNode->fMarkB = 0;
}
/**Function*************************************************************
Synopsis [Evaluate the fanin cost.]
Synopsis [Evaluate the cost of removing the node from the set of leaves.]
Description [Returns the number of fanins that will be brought in.
Returns large number if the node cannot be added.]
Description [Returns the number of new leaves that will be brought in.
Returns large number if the node cannot be removed from the set of leaves.]
SideEffects []
SeeAlso []
***********************************************************************/
static inline int Abc_NodeGetFaninCost( Abc_Obj_t * pNode )
static inline int Abc_NodeGetLeafCostOne( Abc_Obj_t * pNode, int nFaninLimit )
{
Abc_Obj_t * pFanout;
int i;
assert( pNode->fMarkA == 1 ); // this node is in the TFI
assert( pNode->fMarkB == 1 ); // this node is in the constructed cone
// check the PI node
int Cost;
// make sure the node is in the construction zone
assert( pNode->fMarkB == 1 );
// cannot expand over the PI node
if ( Abc_ObjIsCi(pNode) )
return 999;
// get the cost of the cone
Cost = (!Abc_ObjFanin0(pNode)->fMarkB) + (!Abc_ObjFanin1(pNode)->fMarkB);
// always accept if the number of leaves does not increase
if ( Cost < 2 )
return Cost;
// skip nodes with many fanouts
if ( Abc_ObjFanoutNum(pNode) > nFaninLimit )
return 999;
// return the number of nodes that will be on the leaves if this node is removed
return Cost;
}
/**Function*************************************************************
Synopsis [Evaluate the cost of removing the node from the set of leaves.]
Description [Returns the number of new leaves that will be brought in.
Returns large number if the node cannot be removed from the set of leaves.]
SideEffects []
SeeAlso []
***********************************************************************/
static inline int Abc_NodeGetLeafCostTwo( Abc_Obj_t * pNode, int nFaninLimit,
Abc_Obj_t ** ppLeafToAdd, Abc_Obj_t ** pNodeToMark1, Abc_Obj_t ** pNodeToMark2 )
{
Abc_Obj_t * pFanin0, * pFanin1, * pTemp;
Abc_Obj_t * pGrand, * pGrandToAdd;
// make sure the node is in the construction zone
assert( pNode->fMarkB == 1 );
// cannot expand over the PI node
if ( Abc_ObjIsCi(pNode) )
return 999;
// skip nodes with many fanouts
if ( Abc_ObjFanoutNum(pNode) > 5 )
// if ( Abc_ObjFanoutNum(pNode) > nFaninLimit )
// return 999;
// get the children
pFanin0 = Abc_ObjFanin0(pNode);
pFanin1 = Abc_ObjFanin1(pNode);
assert( !pFanin0->fMarkB && !pFanin1->fMarkB );
// count the number of unique grandchildren that will be included
// return infinite cost if this number if more than 1
if ( Abc_ObjIsCi(pFanin0) && Abc_ObjIsCi(pFanin1) )
return 999;
// check the fanouts
Abc_ObjForEachFanout( pNode, pFanout, i )
if ( pFanout->fMarkA && pFanout->fMarkB == 0 ) // the fanout is in the TFI but not in the cone
// consider the special case when a non-CI fanin can be dropped
if ( !Abc_ObjIsCi(pFanin0) && Abc_ObjFanin0(pFanin0)->fMarkB && Abc_ObjFanin1(pFanin0)->fMarkB )
{
*ppLeafToAdd = pFanin1;
*pNodeToMark1 = pFanin0;
*pNodeToMark2 = NULL;
return 1;
}
if ( !Abc_ObjIsCi(pFanin1) && Abc_ObjFanin0(pFanin1)->fMarkB && Abc_ObjFanin1(pFanin1)->fMarkB )
{
*ppLeafToAdd = pFanin0;
*pNodeToMark1 = pFanin1;
*pNodeToMark2 = NULL;
return 1;
}
// make the first node CI if any
if ( Abc_ObjIsCi(pFanin1) )
pTemp = pFanin0, pFanin0 = pFanin1, pFanin1 = pTemp;
// consider the first node
pGrandToAdd = NULL;
if ( Abc_ObjIsCi(pFanin0) )
{
*pNodeToMark1 = NULL;
pGrandToAdd = pFanin0;
}
else
{
*pNodeToMark1 = pFanin0;
pGrand = Abc_ObjFanin0(pFanin0);
if ( !pGrand->fMarkB )
{
if ( pGrandToAdd && pGrandToAdd != pGrand )
return 999;
pGrandToAdd = pGrand;
}
pGrand = Abc_ObjFanin1(pFanin0);
if ( !pGrand->fMarkB )
{
if ( pGrandToAdd && pGrandToAdd != pGrand )
return 999;
pGrandToAdd = pGrand;
}
}
// consider the second node
*pNodeToMark2 = pFanin1;
pGrand = Abc_ObjFanin0(pFanin1);
if ( !pGrand->fMarkB )
{
if ( pGrandToAdd && pGrandToAdd != pGrand )
return 999;
// the fanouts are in the TFI and inside the constructed cone
// return the number of fanins that will be on the boundary if this node is added
return (!Abc_ObjFanin0(pNode)->fMarkB) + (!Abc_ObjFanin1(pNode)->fMarkB);
pGrandToAdd = pGrand;
}
pGrand = Abc_ObjFanin1(pFanin1);
if ( !pGrand->fMarkB )
{
if ( pGrandToAdd && pGrandToAdd != pGrand )
return 999;
pGrandToAdd = pGrand;
}
assert( pGrandToAdd != NULL );
*ppLeafToAdd = pGrandToAdd;
return 1;
}
@ -153,47 +255,176 @@ Vec_Ptr_t * Abc_NodeFindCut( Abc_ManCut_t * p, Abc_Obj_t * pRoot, bool fContain
assert( !Abc_ObjIsComplement(pRoot) );
assert( Abc_ObjIsNode(pRoot) );
// mark TFI using fMarkA
// start the visited nodes and mark them
Vec_PtrClear( p->vVisited );
Abc_NodesMarkCollect_rec( pRoot, p->vVisited );
// start the cut
Vec_PtrClear( p->vFaninsNode );
Vec_PtrPush( p->vFaninsNode, Abc_ObjFanin0(pRoot) );
Vec_PtrPush( p->vFaninsNode, Abc_ObjFanin1(pRoot) );
Vec_PtrPush( p->vVisited, pRoot );
Vec_PtrPush( p->vVisited, Abc_ObjFanin0(pRoot) );
Vec_PtrPush( p->vVisited, Abc_ObjFanin1(pRoot) );
pRoot->fMarkB = 1;
Abc_ObjFanin0(pRoot)->fMarkB = 1;
Abc_ObjFanin1(pRoot)->fMarkB = 1;
// start the cut
Vec_PtrClear( p->vNodeLeaves );
Vec_PtrPush( p->vNodeLeaves, Abc_ObjFanin0(pRoot) );
Vec_PtrPush( p->vNodeLeaves, Abc_ObjFanin1(pRoot) );
// compute the cut
while ( Abc_NodeFindCut_int( p->vFaninsNode, p->nNodeSizeMax ) );
assert( Vec_PtrSize(p->vFaninsNode) <= p->nNodeSizeMax );
while ( Abc_NodeBuildCutLevelOne_int( p->vVisited, p->vNodeLeaves, p->nNodeSizeMax, p->nNodeFanStop ) );
assert( Vec_PtrSize(p->vNodeLeaves) <= p->nNodeSizeMax );
// return if containing cut is not requested
if ( !fContain )
{
// unmark TFI using fMarkA and fMarkB
Abc_NodesUnmarkBoth( p->vVisited );
return p->vFaninsNode;
// unmark both fMarkA and fMarkB in tbe TFI
Abc_NodesUnmarkB( p->vVisited );
return p->vNodeLeaves;
}
//printf( "\n\n\n" );
// compute the containing cut
assert( p->nNodeSizeMax < p->nConeSizeMax );
// copy the current boundary
Vec_PtrClear( p->vFaninsCone );
Vec_PtrForEachEntry( p->vFaninsNode, pNode, i )
Vec_PtrPush( p->vFaninsCone, pNode );
Vec_PtrClear( p->vConeLeaves );
Vec_PtrForEachEntry( p->vNodeLeaves, pNode, i )
Vec_PtrPush( p->vConeLeaves, pNode );
// compute the containing cut
while ( Abc_NodeFindCut_int( p->vFaninsCone, p->nConeSizeMax ) );
assert( Vec_PtrSize(p->vFaninsCone) <= p->nConeSizeMax );
while ( Abc_NodeBuildCutLevelOne_int( p->vVisited, p->vConeLeaves, p->nConeSizeMax, p->nConeFanStop ) );
assert( Vec_PtrSize(p->vConeLeaves) <= p->nConeSizeMax );
// unmark TFI using fMarkA and fMarkB
Abc_NodesUnmarkBoth( p->vVisited );
return p->vFaninsNode;
Abc_NodesUnmarkB( p->vVisited );
return p->vNodeLeaves;
}
/**Function*************************************************************
Synopsis [Finds a reconvergence-driven cut.]
Synopsis [Builds reconvergence-driven cut by changing one leaf at a time.]
Description [This procedure looks at the current leaves and tries to change
one leaf at a time in such a way that the cut grows as little as possible.
In evaluating the fanins, this procedure looks only at their immediate
predecessors (this is why it is called a one-level construction procedure).]
SideEffects []
SeeAlso []
***********************************************************************/
int Abc_NodeBuildCutLevelOne_int( Vec_Ptr_t * vVisited, Vec_Ptr_t * vLeaves, int nSizeLimit, int nFaninLimit )
{
Abc_Obj_t * pNode, * pFaninBest, * pNext;
int CostBest, CostCur, i;
// find the best fanin
CostBest = 100;
pFaninBest = NULL;
//printf( "Evaluating fanins of the cut:\n" );
Vec_PtrForEachEntry( vLeaves, pNode, i )
{
CostCur = Abc_NodeGetLeafCostOne( pNode, nFaninLimit );
//printf( " Fanin %s has cost %d.\n", Abc_ObjName(pNode), CostCur );
if ( CostBest > CostCur )
{
CostBest = CostCur;
pFaninBest = pNode;
}
if ( CostBest == 0 )
break;
}
if ( pFaninBest == NULL )
return 0;
// return Abc_NodeBuildCutLevelTwo_int( vVisited, vLeaves, nFaninLimit );
assert( CostBest < 3 );
if ( vLeaves->nSize - 1 + CostBest > nSizeLimit )
return 0;
// return Abc_NodeBuildCutLevelTwo_int( vVisited, vLeaves, nFaninLimit );
assert( Abc_ObjIsNode(pFaninBest) );
// remove the node from the array
Vec_PtrRemove( vLeaves, pFaninBest );
//printf( "Removing fanin %s.\n", Abc_ObjName(pFaninBest) );
// add the left child to the fanins
pNext = Abc_ObjFanin0(pFaninBest);
if ( !pNext->fMarkB )
{
//printf( "Adding fanin %s.\n", Abc_ObjName(pNext) );
pNext->fMarkB = 1;
Vec_PtrPush( vLeaves, pNext );
Vec_PtrPush( vVisited, pNext );
}
// add the right child to the fanins
pNext = Abc_ObjFanin1(pFaninBest);
if ( !pNext->fMarkB )
{
//printf( "Adding fanin %s.\n", Abc_ObjName(pNext) );
pNext->fMarkB = 1;
Vec_PtrPush( vLeaves, pNext );
Vec_PtrPush( vVisited, pNext );
}
assert( vLeaves->nSize <= nSizeLimit );
// keep doing this
return 1;
}
/**Function*************************************************************
Synopsis [Builds reconvergence-driven cut by changing one leaf at a time.]
Description [This procedure looks at the current leaves and tries to change
one leaf at a time in such a way that the cut grows as little as possible.
In evaluating the fanins, this procedure looks across two levels of fanins
(this is why it is called a two-level construction procedure).]
SideEffects []
SeeAlso []
***********************************************************************/
int Abc_NodeBuildCutLevelTwo_int( Vec_Ptr_t * vVisited, Vec_Ptr_t * vLeaves, int nFaninLimit )
{
Abc_Obj_t * pNode, * pLeafToAdd, * pNodeToMark1, * pNodeToMark2;
int CostCur, i;
// find the best fanin
Vec_PtrForEachEntry( vLeaves, pNode, i )
{
CostCur = Abc_NodeGetLeafCostTwo( pNode, nFaninLimit, &pLeafToAdd, &pNodeToMark1, &pNodeToMark2 );
if ( CostCur < 2 )
break;
}
if ( CostCur > 2 )
return 0;
// remove the node from the array
Vec_PtrRemove( vLeaves, pNode );
// add the node to the leaves
if ( pLeafToAdd )
{
assert( !pLeafToAdd->fMarkB );
pLeafToAdd->fMarkB = 1;
Vec_PtrPush( vLeaves, pLeafToAdd );
Vec_PtrPush( vVisited, pLeafToAdd );
}
// mark the other nodes
if ( pNodeToMark1 )
{
assert( !pNodeToMark1->fMarkB );
pNodeToMark1->fMarkB = 1;
Vec_PtrPush( vVisited, pNodeToMark1 );
}
if ( pNodeToMark2 )
{
assert( !pNodeToMark2->fMarkB );
pNodeToMark2->fMarkB = 1;
Vec_PtrPush( vVisited, pNodeToMark2 );
}
// keep doing this
return 1;
}
/**Function*************************************************************
Synopsis [Get the nodes contained in the cut.]
Description []
@ -202,64 +433,24 @@ Vec_Ptr_t * Abc_NodeFindCut( Abc_ManCut_t * p, Abc_Obj_t * pRoot, bool fContain
SeeAlso []
***********************************************************************/
int Abc_NodeFindCut_int( Vec_Ptr_t * vFanins, int nSizeLimit )
void Abc_NodeConeCollect( Abc_Obj_t ** ppRoots, int nRoots, Vec_Ptr_t * vLeaves, Vec_Ptr_t * vVisited, int fIncludeFanins )
{
Abc_Obj_t * pNode, * pFaninBest, * pNext;
int CostBest, CostCur, i;
// int fFlagProb = (rand() & 1);
int fFlagProb = 1;
// find the best fanin
CostBest = 100;
pFaninBest = NULL;
if ( fFlagProb )
{
Vec_PtrForEachEntry( vFanins, pNode, i )
{
CostCur = Abc_NodeGetFaninCost( pNode );
if ( CostBest > CostCur )
{
CostBest = CostCur;
pFaninBest = pNode;
}
}
}
else
{
Vec_PtrForEachEntry( vFanins, pNode, i )
{
CostCur = Abc_NodeGetFaninCost( pNode );
if ( CostBest >= CostCur )
{
CostBest = CostCur;
pFaninBest = pNode;
}
}
}
if ( pFaninBest == NULL )
return 0;
assert( CostBest < 3 );
if ( vFanins->nSize - 1 + CostBest > nSizeLimit )
return 0;
assert( Abc_ObjIsNode(pFaninBest) );
// remove the node from the array
Vec_PtrRemove( vFanins, pFaninBest );
// add the left child to the fanins
pNext = Abc_ObjFanin0(pFaninBest);
if ( !pNext->fMarkB )
{
pNext->fMarkB = 1;
Vec_PtrPush( vFanins, pNext );
}
// add the right child to the fanins
pNext = Abc_ObjFanin1(pFaninBest);
if ( !pNext->fMarkB )
{
pNext->fMarkB = 1;
Vec_PtrPush( vFanins, pNext );
}
assert( vFanins->nSize <= nSizeLimit );
// keep doing this
return 1;
Abc_Obj_t * pTemp;
int i;
// mark the fanins of the cone
Abc_NodesMark( vLeaves );
// collect the nodes in the DFS order
Vec_PtrClear( vVisited );
// add the fanins
if ( fIncludeFanins )
Vec_PtrForEachEntry( vLeaves, pTemp, i )
Vec_PtrPush( vVisited, pTemp );
// add other nodes
for ( i = 0; i < nRoots; i++ )
Abc_NodeConeMarkCollect_rec( ppRoots[i], vVisited );
// unmark both sets
Abc_NodesUnmark( vLeaves );
Abc_NodesUnmark( vVisited );
}
/**Function*************************************************************
@ -273,22 +464,21 @@ int Abc_NodeFindCut_int( Vec_Ptr_t * vFanins, int nSizeLimit )
SeeAlso []
***********************************************************************/
void Abc_NodesMarkCollect_rec( Abc_Obj_t * pNode, Vec_Ptr_t * vVisited )
void Abc_NodeConeMarkCollect_rec( Abc_Obj_t * pNode, Vec_Ptr_t * vVisited )
{
if ( pNode->fMarkA == 1 )
return;
// visit transitive fanin
if ( Abc_ObjIsNode(pNode) )
{
Abc_NodesMarkCollect_rec( Abc_ObjFanin0(pNode), vVisited );
Abc_NodesMarkCollect_rec( Abc_ObjFanin1(pNode), vVisited );
Abc_NodeConeMarkCollect_rec( Abc_ObjFanin0(pNode), vVisited );
Abc_NodeConeMarkCollect_rec( Abc_ObjFanin1(pNode), vVisited );
}
assert( pNode->fMarkA == 0 );
pNode->fMarkA = 1;
Vec_PtrPush( vVisited, pNode );
}
/**Function*************************************************************
Synopsis [Returns BDD representing the logic function of the cone.]
@ -300,20 +490,14 @@ void Abc_NodesMarkCollect_rec( Abc_Obj_t * pNode, Vec_Ptr_t * vVisited )
SeeAlso []
***********************************************************************/
DdNode * Abc_NodeConeBdd( DdManager * dd, DdNode ** pbVars, Abc_Obj_t * pNode, Vec_Ptr_t * vFanins, Vec_Ptr_t * vVisited )
DdNode * Abc_NodeConeBdd( DdManager * dd, DdNode ** pbVars, Abc_Obj_t * pNode, Vec_Ptr_t * vLeaves, Vec_Ptr_t * vVisited )
{
DdNode * bFunc0, * bFunc1, * bFunc;
int i;
// mark the fanins of the cone
Abc_NodesMark( vFanins );
// collect the nodes in the DFS order
Vec_PtrClear( vVisited );
Abc_NodesMarkCollect_rec( pNode, vVisited );
// unmark both sets
Abc_NodesUnmark( vFanins );
Abc_NodesUnmark( vVisited );
// get the nodes in the cut without fanins in the DFS order
Abc_NodeConeCollect( &pNode, 1, vLeaves, vVisited, 0 );
// set the elementary BDDs
Vec_PtrForEachEntry( vFanins, pNode, i )
Vec_PtrForEachEntry( vLeaves, pNode, i )
pNode->pCopy = (Abc_Obj_t *)pbVars[i];
// compute the BDDs for the collected nodes
Vec_PtrForEachEntry( vVisited, pNode, i )
@ -347,15 +531,8 @@ DdNode * Abc_NodeConeDcs( DdManager * dd, DdNode ** pbVarsX, DdNode ** pbVarsY,
DdNode * bFunc0, * bFunc1, * bFunc, * bTrans, * bTemp, * bCube, * bResult;
Abc_Obj_t * pNode;
int i;
// mark the fanins of the cone
Abc_NodesMark( vLeaves );
// collect the nodes in the DFS order
Vec_PtrClear( vVisited );
Vec_PtrForEachEntry( vRoots, pNode, i )
Abc_NodesMarkCollect_rec( pNode, vVisited );
// unmark both sets
Abc_NodesUnmark( vLeaves );
Abc_NodesUnmark( vVisited );
// get the nodes in the cut without fanins in the DFS order
Abc_NodeConeCollect( (Abc_Obj_t **)vRoots->pArray, vRoots->nSize, vLeaves, vVisited, 0 );
// set the elementary BDDs
Vec_PtrForEachEntry( vLeaves, pNode, i )
pNode->pCopy = (Abc_Obj_t *)pbVarsX[i];
@ -400,16 +577,20 @@ DdNode * Abc_NodeConeDcs( DdManager * dd, DdNode ** pbVarsX, DdNode ** pbVarsY,
SeeAlso []
***********************************************************************/
Abc_ManCut_t * Abc_NtkManCutStart( int nNodeSizeMax, int nConeSizeMax )
Abc_ManCut_t * Abc_NtkManCutStart( int nNodeSizeMax, int nConeSizeMax, int nNodeFanStop, int nConeFanStop )
{
Abc_ManCut_t * p;
p = ALLOC( Abc_ManCut_t, 1 );
memset( p, 0, sizeof(Abc_ManCut_t) );
p->vFaninsNode = Vec_PtrAlloc( 100 );
p->vFaninsCone = Vec_PtrAlloc( 100 );
p->vNodeLeaves = Vec_PtrAlloc( 100 );
p->vConeLeaves = Vec_PtrAlloc( 100 );
p->vVisited = Vec_PtrAlloc( 100 );
p->vLevels = Vec_VecAlloc( 100 );
p->vNodesTfo = Vec_PtrAlloc( 100 );
p->nNodeSizeMax = nNodeSizeMax;
p->nConeSizeMax = nConeSizeMax;
p->nNodeFanStop = nNodeFanStop;
p->nConeFanStop = nConeFanStop;
return p;
}
@ -426,9 +607,11 @@ Abc_ManCut_t * Abc_NtkManCutStart( int nNodeSizeMax, int nConeSizeMax )
***********************************************************************/
void Abc_NtkManCutStop( Abc_ManCut_t * p )
{
Vec_PtrFree( p->vFaninsNode );
Vec_PtrFree( p->vFaninsCone );
Vec_PtrFree( p->vNodeLeaves );
Vec_PtrFree( p->vConeLeaves );
Vec_PtrFree( p->vVisited );
Vec_VecFree( p->vLevels );
Vec_PtrFree( p->vNodesTfo );
free( p );
}
@ -443,9 +626,25 @@ void Abc_NtkManCutStop( Abc_ManCut_t * p )
SeeAlso []
***********************************************************************/
Vec_Ptr_t * Abc_NtkManCutReadLeaves( Abc_ManCut_t * p )
Vec_Ptr_t * Abc_NtkManCutReadCutLarge( Abc_ManCut_t * p )
{
return p->vFaninsCone;
return p->vConeLeaves;
}
/**Function*************************************************************
Synopsis [Returns the leaves of the cone.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
Vec_Ptr_t * Abc_NtkManCutReadVisited( Abc_ManCut_t * p )
{
return p->vVisited;
}
@ -466,27 +665,27 @@ Vec_Ptr_t * Abc_NtkManCutReadLeaves( Abc_ManCut_t * p )
SeeAlso []
***********************************************************************/
void Abc_NodeCollectTfoCands( Abc_Ntk_t * pNtk, Abc_Obj_t * pRoot,
Vec_Ptr_t * vFanins, int LevelMax, Vec_Vec_t * vLevels, Vec_Ptr_t * vResult )
Vec_Ptr_t * Abc_NodeCollectTfoCands( Abc_ManCut_t * p, Abc_Obj_t * pRoot, Vec_Ptr_t * vLeaves, int LevelMax )
{
Abc_Ntk_t * pNtk = pRoot->pNtk;
Vec_Ptr_t * vVec;
Abc_Obj_t * pNode, * pFanout;
int i, k, v, LevelMin;
assert( Abc_NtkIsStrash(pNtk) );
// assuming that the structure is clean
Vec_VecForEachLevel( vLevels, vVec, i )
Vec_VecForEachLevel( p->vLevels, vVec, i )
assert( vVec->nSize == 0 );
// put fanins into the structure while labeling them
Abc_NtkIncrementTravId( pNtk );
LevelMin = ABC_INFINITY;
Vec_PtrForEachEntry( vFanins, pNode, i )
LevelMin = -1;
Vec_PtrForEachEntry( vLeaves, pNode, i )
{
if ( pNode->Level > (unsigned)LevelMax )
continue;
Abc_NodeSetTravIdCurrent( pNode );
Vec_VecPush( vLevels, pNode->Level, pNode );
Vec_VecPush( p->vLevels, pNode->Level, pNode );
if ( LevelMin < (int)pNode->Level )
LevelMin = pNode->Level;
}
@ -497,9 +696,11 @@ void Abc_NodeCollectTfoCands( Abc_Ntk_t * pNtk, Abc_Obj_t * pRoot,
Abc_NodeMffcLabel( pRoot );
// go through the levels up
Vec_PtrClear( vResult );
Vec_VecForEachEntryStartStop( vLevels, pNode, i, k, LevelMin, LevelMax )
Vec_PtrClear( p->vNodesTfo );
Vec_VecForEachEntryStart( p->vLevels, pNode, i, k, LevelMin )
{
if ( i > LevelMax )
break;
// if the node is not marked, it is not a fanin
if ( !Abc_NodeIsTravIdCurrent(pNode) )
{
@ -508,7 +709,7 @@ void Abc_NodeCollectTfoCands( Abc_Ntk_t * pNtk, Abc_Obj_t * pRoot,
!Abc_NodeIsTravIdCurrent(Abc_ObjFanin1(pNode)) )
continue;
// save the node in the TFO and label it
Vec_PtrPush( vResult, pNode );
Vec_PtrPush( p->vNodesTfo, pNode );
Abc_NodeSetTravIdCurrent( pNode );
}
// go through the fanouts and add them to the structure if they meet the conditions
@ -521,13 +722,18 @@ void Abc_NodeCollectTfoCands( Abc_Ntk_t * pNtk, Abc_Obj_t * pRoot,
if ( Abc_NodeIsTravIdCurrent(pFanout) )
continue;
// add it to the structure but do not mark it (until tested later)
Vec_VecPush( vLevels, pFanout->Level, pFanout );
Vec_VecPushUnique( p->vLevels, pFanout->Level, pFanout );
}
}
// clear the levelized structure
Vec_VecForEachLevelStartStop( vLevels, vVec, i, LevelMin, LevelMax )
Vec_VecForEachLevelStart( p->vLevels, vVec, i, LevelMin )
{
if ( i > LevelMax )
break;
Vec_PtrClear( vVec );
}
return p->vNodesTfo;
}
////////////////////////////////////////////////////////////////////////

View File

@ -96,9 +96,9 @@ int Abc_NtkRefactor( Abc_Ntk_t * pNtk, int nNodeSizeMax, int nConeSizeMax, bool
assert( Abc_NtkIsStrash(pNtk) );
// start the managers
pManCut = Abc_NtkManCutStart( nNodeSizeMax, nConeSizeMax );
pManCut = Abc_NtkManCutStart( nNodeSizeMax, nConeSizeMax, 2, 1000 );
pManRef = Abc_NtkManRefStart( nNodeSizeMax, nConeSizeMax, fUseDcs, fVerbose );
pManRef->vLeaves = Abc_NtkManCutReadLeaves( pManCut );
pManRef->vLeaves = Abc_NtkManCutReadCutLarge( pManCut );
Abc_NtkStartReverseLevels( pNtk );
// resynthesize each node once

View File

@ -174,6 +174,10 @@ void Abc_NodeUpdate( Abc_Obj_t * pNode, Vec_Ptr_t * vFanins, Vec_Int_t * vForm,
// create the new structure of nodes
assert( vForm->nSize == 1 || Vec_PtrSize(vFanins) < Vec_IntSize(vForm) );
pNodeNew = Abc_NodeStrashDec( pNtk->pManFunc, vFanins, vForm );
// in some cases, the new node may have a minor redundancy
// (has to do with the precomputed subgraph library)
if ( !Abc_AigNodeIsAcyclic( Abc_ObjRegular(pNodeNew), pNode ) )
return;
// remove the old nodes
Abc_AigReplace( pNtk->pManFunc, pNode, pNodeNew );
// compare the gains

View File

@ -18,22 +18,27 @@
***********************************************************************/
#include "abc.h"
#ifdef WIN32
#include "process.h"
#include <process.h>
#endif
#include "abc.h"
#include "io.h"
////////////////////////////////////////////////////////////////////////
/// DECLARATIONS ///
////////////////////////////////////////////////////////////////////////
static void Abc_ShowFile( char * FileNameDot );
static void Abc_ShowGetFileName( char * pName, char * pBuffer );
////////////////////////////////////////////////////////////////////////
/// FUNCTION DEFITIONS ///
////////////////////////////////////////////////////////////////////////
/**Function*************************************************************
Synopsis [Prints the factored form of one node.]
Synopsis [Visualizes BDD of the node.]
Description []
@ -42,15 +47,152 @@
SeeAlso []
***********************************************************************/
void Abc_NodePrintBdd( Abc_Obj_t * pNode )
void Abc_NodeShowBdd( Abc_Obj_t * pNode )
{
FILE * pFile;
Vec_Ptr_t * vNamesIn;
char * FileNameIn;
char * FileNameOut;
char * FileGeneric;
char * pCur, * pNameOut;
char FileNameDot[200];
char * pNameOut;
assert( Abc_NtkIsBddLogic(pNode->pNtk) );
// create the file names
Abc_ShowGetFileName( Abc_ObjName(pNode), FileNameDot );
// check that the file can be opened
if ( (pFile = fopen( FileNameDot, "w" )) == NULL )
{
fprintf( stdout, "Cannot open the intermediate file \"%s\".\n", FileNameDot );
return;
}
// set the node names
vNamesIn = Abc_NodeGetFaninNames( pNode );
pNameOut = Abc_ObjName(pNode);
Cudd_DumpDot( pNode->pNtk->pManFunc, 1, (DdNode **)&pNode->pData, (char **)vNamesIn->pArray, &pNameOut, pFile );
Abc_NodeFreeFaninNames( vNamesIn );
Abc_NtkCleanCopy( pNode->pNtk );
fclose( pFile );
// visualize the file
Abc_ShowFile( FileNameDot );
}
/**Function*************************************************************
Synopsis [Visualizes AIG with choices.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
void Abc_NtkShowAig( Abc_Ntk_t * pNtk )
{
FILE * pFile;
Abc_Obj_t * pNode;
Vec_Ptr_t * vNodes;
char FileNameDot[200];
int i;
assert( Abc_NtkIsStrash(pNtk) );
// create the file names
Abc_ShowGetFileName( pNtk->pName, FileNameDot );
// check that the file can be opened
if ( (pFile = fopen( FileNameDot, "w" )) == NULL )
{
fprintf( stdout, "Cannot open the intermediate file \"%s\".\n", FileNameDot );
return;
}
// collect all nodes in the network
vNodes = Vec_PtrAlloc( 100 );
Abc_NtkForEachObj( pNtk, pNode, i )
Vec_PtrPush( vNodes, pNode );
// write the DOT file
Io_WriteDot( pNtk, vNodes, NULL, FileNameDot );
Vec_PtrFree( vNodes );
// visualize the file
Abc_ShowFile( FileNameDot );
}
/**Function*************************************************************
Synopsis [Visualizes reconvergence driven cut at the node.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
void Abc_NodeShowCut( Abc_Obj_t * pNode, int nNodeSizeMax, int nConeSizeMax )
{
FILE * pFile;
char FileNameDot[200];
Abc_ManCut_t * p;
Vec_Ptr_t * vCutSmall;
Vec_Ptr_t * vCutLarge;
Vec_Ptr_t * vInside;
Vec_Ptr_t * vNodesTfo;
Abc_Obj_t * pTemp;
int i;
assert( Abc_NtkIsStrash(pNode->pNtk) );
// start the cut computation manager
p = Abc_NtkManCutStart( nNodeSizeMax, nConeSizeMax, 2, ABC_INFINITY );
// get the recovergence driven cut
vCutSmall = Abc_NodeFindCut( p, pNode, 1 );
// get the containing cut
vCutLarge = Abc_NtkManCutReadCutLarge( p );
// get the array for the inside nodes
vInside = Abc_NtkManCutReadVisited( p );
// get the inside nodes of the containing cone
Abc_NodeConeCollect( &pNode, 1, vCutLarge, vInside, 1 );
// add the nodes in the TFO
vNodesTfo = Abc_NodeCollectTfoCands( p, pNode, vCutSmall, ABC_INFINITY );
Vec_PtrForEachEntry( vNodesTfo, pTemp, i )
Vec_PtrPushUnique( vInside, pTemp );
// create the file names
Abc_ShowGetFileName( Abc_ObjName(pNode), FileNameDot );
// check that the file can be opened
if ( (pFile = fopen( FileNameDot, "w" )) == NULL )
{
fprintf( stdout, "Cannot open the intermediate file \"%s\".\n", FileNameDot );
return;
}
// add the root node to the cone (for visualization)
Vec_PtrPush( vCutSmall, pNode );
// write the DOT file
Io_WriteDot( pNode->pNtk, vInside, vCutSmall, FileNameDot );
// stop the cut computation manager
Abc_NtkManCutStop( p );
// visualize the file
Abc_ShowFile( FileNameDot );
}
/**Function*************************************************************
Synopsis [Shows the given DOT file.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
void Abc_ShowFile( char * FileNameDot )
{
FILE * pFile;
char * FileGeneric;
char FileNamePs[200];
char CommandDot[1000];
#ifndef WIN32
@ -60,8 +202,6 @@ void Abc_NodePrintBdd( Abc_Obj_t * pNode )
char * pProgGsViewName;
int RetValue;
assert( Abc_NtkIsBddLogic(pNode->pNtk) );
#ifdef WIN32
pProgDotName = "dot.exe";
pProgGsViewName = NULL;
@ -70,34 +210,6 @@ void Abc_NodePrintBdd( Abc_Obj_t * pNode )
pProgGsViewName = "gv";
#endif
FileNameIn = NULL;
FileNameOut = NULL;
// get the generic file name
pNode->pCopy = NULL;
FileGeneric = Abc_ObjName(pNode);
// get rid of not-alpha-numeric characters
for ( pCur = FileGeneric; *pCur; pCur++ )
if ( !((*pCur >= '0' && *pCur <= '9') || (*pCur >= 'a' && *pCur <= 'z') || (*pCur >= 'A' && *pCur <= 'Z')) )
*pCur = '_';
// create the file names
sprintf( FileNameDot, "%s.dot", FileGeneric );
sprintf( FileNamePs, "%s.ps", FileGeneric );
// write the DOT file
if ( (pFile = fopen( FileNameDot, "w" )) == NULL )
{
fprintf( stdout, "Cannot open the intermediate file \"%s\".\n", FileNameDot );
return;
}
// set the node names
vNamesIn = Abc_NodeGetFaninNames( pNode );
pNameOut = Abc_ObjName(pNode);
Cudd_DumpDot( pNode->pNtk->pManFunc, 1, (DdNode **)&pNode->pData, (char **)vNamesIn->pArray, &pNameOut, pFile );
Abc_NodeFreeFaninNames( vNamesIn );
Abc_NtkCleanCopy( pNode->pNtk );
fclose( pFile );
// check that the input file is okay
if ( (pFile = fopen( FileNameDot, "r" )) == NULL )
{
@ -106,6 +218,12 @@ void Abc_NodePrintBdd( Abc_Obj_t * pNode )
}
fclose( pFile );
// get the generic file name
FileGeneric = Extra_FileNameGeneric( FileNameDot );
// create the PostScript file name
sprintf( FileNamePs, "%s.ps", FileGeneric );
free( FileGeneric );
// generate the DOT file
sprintf( CommandDot, "%s -Tps -o %s %s", pProgDotName, FileNamePs, FileNameDot );
RetValue = system( CommandDot );
@ -146,10 +264,9 @@ void Abc_NodePrintBdd( Abc_Obj_t * pNode )
#endif
}
/**Function*************************************************************
Synopsis []
Synopsis [Derives the DOT file name.]
Description []
@ -158,6 +275,18 @@ void Abc_NodePrintBdd( Abc_Obj_t * pNode )
SeeAlso []
***********************************************************************/
void Abc_ShowGetFileName( char * pName, char * pBuffer )
{
char * pCur;
// creat the file name
sprintf( pBuffer, "%s.dot", pName );
// get rid of not-alpha-numeric characters
for ( pCur = pBuffer; *pCur; pCur++ )
if ( !((*pCur >= '0' && *pCur <= '9') || (*pCur >= 'a' && *pCur <= 'z') ||
(*pCur >= 'A' && *pCur <= 'Z') || (*pCur == '.')) )
*pCur = '_';
}
////////////////////////////////////////////////////////////////////////
/// END OF FILE ///

View File

@ -49,7 +49,7 @@ extern char * Mio_GateReadSop( void * pGate );
SeeAlso []
***********************************************************************/
Abc_Ntk_t * Abc_NtkStrash( Abc_Ntk_t * pNtk, bool fAllNodes )
Abc_Ntk_t * Abc_NtkStrash( Abc_Ntk_t * pNtk, bool fAllNodes, bool fCleanup )
{
int fCheck = 1;
Abc_Ntk_t * pNtkAig;
@ -68,11 +68,11 @@ Abc_Ntk_t * Abc_NtkStrash( Abc_Ntk_t * pNtk, bool fAllNodes )
// print warning about self-feed latches
if ( Abc_NtkCountSelfFeedLatches(pNtkAig) )
printf( "The network has %d self-feeding latches.\n", Abc_NtkCountSelfFeedLatches(pNtkAig) );
if ( nNodes = Abc_AigCleanup(pNtkAig->pManFunc) )
if ( fCleanup && (nNodes = Abc_AigCleanup(pNtkAig->pManFunc)) )
printf( "Cleanup has removed %d nodes.\n", nNodes );
// duplicate EXDC
if ( pNtk->pExdc )
pNtkAig->pExdc = Abc_NtkStrash( pNtk->pExdc, 0 );
pNtkAig->pExdc = Abc_NtkStrash( pNtk->pExdc, 0, 1 );
// make sure everything is okay
if ( fCheck && !Abc_NtkCheck( pNtkAig ) )
{

View File

@ -61,7 +61,7 @@ bool Abc_NtkFraigSweep( Abc_Ntk_t * pNtk, int fUseInv, int fVerbose )
assert( !Abc_NtkIsStrash(pNtk) );
// derive the AIG
pNtkAig = Abc_NtkStrash( pNtk, 0 );
pNtkAig = Abc_NtkStrash( pNtk, 0, 1 );
// perform fraiging of the AIG
Fraig_ParamsSetDefault( &Params );
pMan = Abc_NtkToFraig( pNtkAig, &Params, 0 );

202
src/base/abc/abcSymm.c Normal file
View File

@ -0,0 +1,202 @@
/**CFile****************************************************************
FileName [abcSymm.c]
SystemName [ABC: Logic synthesis and verification system.]
PackageName [Network and node package.]
Synopsis [Computation of two-variable symmetries.]
Author [Alan Mishchenko]
Affiliation [UC Berkeley]
Date [Ver. 1.0. Started - June 20, 2005.]
Revision [$Id: abcSymm.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
***********************************************************************/
#include "abc.h"
////////////////////////////////////////////////////////////////////////
/// DECLARATIONS ///
////////////////////////////////////////////////////////////////////////
static void Abc_NtkSymmetriesUsingBdds( Abc_Ntk_t * pNtk, int fNaive, int fVerbose );
static void Ntk_NetworkSymmsBdd( DdManager * dd, Abc_Ntk_t * pNtk, int fNaive, int fVerbose );
static void Ntk_NetworkSymmsPrint( Abc_Ntk_t * pNtk, Extra_SymmInfo_t * pSymms );
////////////////////////////////////////////////////////////////////////
/// FUNCTION DEFITIONS ///
////////////////////////////////////////////////////////////////////////
/**Function*************************************************************
Synopsis [The top level procedure to compute symmetries.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
void Abc_NtkSymmetries( Abc_Ntk_t * pNtk, int fUseBdds, int fNaive, int fVerbose )
{
if ( fUseBdds || fNaive )
Abc_NtkSymmetriesUsingBdds( pNtk, fNaive, fVerbose );
else
printf( "This option is currently not implemented.\n" );
}
/**Function*************************************************************
Synopsis [Symmetry computation using BDDs (both naive and smart).]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
void Abc_NtkSymmetriesUsingBdds( Abc_Ntk_t * pNtk, int fNaive, int fVerbose )
{
DdManager * dd;
int clk, clkBdd, clkSym;
// compute the global functions
clk = clock();
dd = Abc_NtkGlobalBdds( pNtk, 0 );
Cudd_AutodynDisable( dd );
Cudd_zddVarsFromBddVars( dd, 2 );
clkBdd = clock() - clk;
// create the collapsed network
clk = clock();
Ntk_NetworkSymmsBdd( dd, pNtk, fNaive, fVerbose );
clkSym = clock() - clk;
// undo the global functions
Abc_NtkFreeGlobalBdds( pNtk );
Extra_StopManager( dd );
pNtk->pManGlob = NULL;
PRT( "Constructing BDDs", clkBdd );
PRT( "Computing symms ", clkSym );
PRT( "TOTAL ", clkBdd + clkSym );
}
/**Function*************************************************************
Synopsis [Symmetry computation using BDDs (both naive and smart).]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
void Ntk_NetworkSymmsBdd( DdManager * dd, Abc_Ntk_t * pNtk, int fNaive, int fVerbose )
{
Extra_SymmInfo_t * pSymms;
Abc_Obj_t * pNode;
DdNode * bFunc;
int nSymms = 0;
int i;
// compute symmetry info for each PO
Abc_NtkForEachCo( pNtk, pNode, i )
{
bFunc = pNtk->vFuncsGlob->pArray[i];
if ( Cudd_IsConstant(bFunc) )
continue;
if ( fNaive )
pSymms = Extra_SymmPairsComputeNaive( dd, bFunc );
else
pSymms = Extra_SymmPairsCompute( dd, bFunc );
nSymms += pSymms->nSymms;
if ( fVerbose )
{
printf( "Output %6s (%d): ", Abc_ObjName(pNode), pSymms->nSymms );
Ntk_NetworkSymmsPrint( pNtk, pSymms );
}
//Extra_SymmPairsPrint( pSymms );
Extra_SymmPairsDissolve( pSymms );
}
printf( "The total number of symmetries is %d.\n", nSymms );
}
/**Function*************************************************************
Synopsis [Printing symmetry groups from the symmetry data structure.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
void Ntk_NetworkSymmsPrint( Abc_Ntk_t * pNtk, Extra_SymmInfo_t * pSymms )
{
char ** pInputNames;
int * pVarTaken;
int i, k, nVars, nSize, fStart;
// get variable names
nVars = Abc_NtkCiNum(pNtk);
pInputNames = Abc_NtkCollectCioNames( pNtk, 0 );
// alloc the array of marks
pVarTaken = ALLOC( int, nVars );
memset( pVarTaken, 0, sizeof(int) * nVars );
// print the groups
fStart = 1;
nSize = pSymms->nVars;
for ( i = 0; i < nSize; i++ )
{
// skip the variable already considered
if ( pVarTaken[i] )
continue;
// find all the vars symmetric with this one
for ( k = 0; k < nSize; k++ )
{
if ( k == i )
continue;
if ( pSymms->pSymms[i][k] == 0 )
continue;
// vars i and k are symmetric
assert( pVarTaken[k] == 0 );
// there is a new symmetry pair
if ( fStart == 1 )
{ // start a new symmetry class
fStart = 0;
printf( " { %s", pInputNames[ pSymms->pVars[i] ] );
// mark the var as taken
pVarTaken[i] = 1;
}
printf( " %s", pInputNames[ pSymms->pVars[k] ] );
// mark the var as taken
pVarTaken[k] = 1;
}
if ( fStart == 0 )
{
printf( " }" );
fStart = 1;
}
}
printf( "\n" );
free( pInputNames );
free( pVarTaken );
}
////////////////////////////////////////////////////////////////////////
/// END OF FILE ///
////////////////////////////////////////////////////////////////////////

View File

@ -91,6 +91,7 @@ int Abc_NtkExtractSequentialDcs( Abc_Ntk_t * pNtk, bool fVerbose )
pNtk->pExdc = Abc_NtkConstructExdc( dd, pNtk, bUnreach );
Cudd_RecursiveDeref( dd, bUnreach );
Extra_StopManager( dd );
pNtk->pManGlob = NULL;
// make sure that everything is okay
if ( fCheck && !Abc_NtkCheck( pNtk->pExdc ) )
@ -135,13 +136,13 @@ DdNode * Abc_NtkTransitionRelation( DdManager * dd, Abc_Ntk_t * pNtk, int fVerbo
Abc_NtkForEachLatch( pNtk, pNode, i )
{
bVar = Cudd_bddIthVar( dd, Abc_NtkCiNum(pNtk) + i );
bProd = Cudd_bddXnor( dd, bVar, (DdNode *)pNode->pNext ); Cudd_Ref( bProd );
bRel = Cudd_bddAnd( dd, bTemp = bRel, bProd ); Cudd_Ref( bRel );
bProd = Cudd_bddXnor( dd, bVar, pNtk->vFuncsGlob->pArray[i] ); Cudd_Ref( bProd );
bRel = Cudd_bddAnd( dd, bTemp = bRel, bProd ); Cudd_Ref( bRel );
Cudd_RecursiveDeref( dd, bTemp );
Cudd_RecursiveDeref( dd, bProd );
}
// free the global BDDs
Abc_NtkFreeGlobalBdds( dd, pNtk );
Abc_NtkFreeGlobalBdds( pNtk );
// quantify the PI variables
bInputs = Extra_bddComputeRangeCube( dd, 0, Abc_NtkPiNum(pNtk) ); Cudd_Ref( bInputs );

View File

@ -1046,6 +1046,29 @@ Vec_Int_t * Abc_NtkFanoutCounts( Abc_Ntk_t * pNtk )
return vFanNums;
}
/**Function*************************************************************
Synopsis [Collects all objects into one array.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
Vec_Ptr_t * Abc_NtkCollectObjects( Abc_Ntk_t * pNtk )
{
Vec_Ptr_t * vNodes;
Abc_Obj_t * pNode;
int i;
vNodes = Vec_PtrAlloc( 100 );
Abc_NtkForEachObj( pNtk, pNode, i )
Vec_PtrPush( vNodes, pNode );
return vNodes;
}
////////////////////////////////////////////////////////////////////////
/// END OF FILE ///
////////////////////////////////////////////////////////////////////////

View File

@ -32,6 +32,7 @@ SRC += src/base/abc/abc.c \
src/base/abc/abcSop.c \
src/base/abc/abcStrash.c \
src/base/abc/abcSweep.c \
src/base/abc/abcSymm.c \
src/base/abc/abcTiming.c \
src/base/abc/abcUnreach.c \
src/base/abc/abcUtil.c \

View File

@ -29,12 +29,16 @@ static int IoCommandRead ( Abc_Frame_t * pAbc, int argc, char **argv );
static int IoCommandReadBlif ( Abc_Frame_t * pAbc, int argc, char **argv );
static int IoCommandReadBench ( Abc_Frame_t * pAbc, int argc, char **argv );
static int IoCommandReadEdif ( Abc_Frame_t * pAbc, int argc, char **argv );
static int IoCommandReadEqn ( Abc_Frame_t * pAbc, int argc, char **argv );
static int IoCommandReadVerilog ( Abc_Frame_t * pAbc, int argc, char **argv );
static int IoCommandReadPla ( Abc_Frame_t * pAbc, int argc, char **argv );
static int IoCommandWriteBlif ( Abc_Frame_t * pAbc, int argc, char **argv );
static int IoCommandWriteBench ( Abc_Frame_t * pAbc, int argc, char **argv );
static int IoCommandWriteCnf ( Abc_Frame_t * pAbc, int argc, char **argv );
static int IoCommandWriteDot ( Abc_Frame_t * pAbc, int argc, char **argv );
static int IoCommandWriteEqn ( Abc_Frame_t * pAbc, int argc, char **argv );
static int IoCommandWriteGml ( Abc_Frame_t * pAbc, int argc, char **argv );
static int IoCommandWritePla ( Abc_Frame_t * pAbc, int argc, char **argv );
////////////////////////////////////////////////////////////////////////
@ -58,12 +62,16 @@ void Io_Init( Abc_Frame_t * pAbc )
Cmd_CommandAdd( pAbc, "I/O", "read_blif", IoCommandReadBlif, 1 );
Cmd_CommandAdd( pAbc, "I/O", "read_bench", IoCommandReadBench, 1 );
Cmd_CommandAdd( pAbc, "I/O", "read_edif", IoCommandReadEdif, 1 );
Cmd_CommandAdd( pAbc, "I/O", "read_eqn", IoCommandReadEqn, 1 );
Cmd_CommandAdd( pAbc, "I/O", "read_verilog", IoCommandReadVerilog, 1 );
Cmd_CommandAdd( pAbc, "I/O", "read_pla", IoCommandReadPla, 1 );
Cmd_CommandAdd( pAbc, "I/O", "write_blif", IoCommandWriteBlif, 0 );
Cmd_CommandAdd( pAbc, "I/O", "write_bench", IoCommandWriteBench, 0 );
Cmd_CommandAdd( pAbc, "I/O", "write_cnf", IoCommandWriteCnf, 0 );
Cmd_CommandAdd( pAbc, "I/O", "write_dot", IoCommandWriteDot, 0 );
Cmd_CommandAdd( pAbc, "I/O", "write_eqn", IoCommandWriteEqn, 0 );
Cmd_CommandAdd( pAbc, "I/O", "write_gml", IoCommandWriteGml, 0 );
Cmd_CommandAdd( pAbc, "I/O", "write_pla", IoCommandWritePla, 0 );
}
@ -127,7 +135,7 @@ int IoCommandRead( Abc_Frame_t * pAbc, int argc, char ** argv )
if ( (pFile = fopen( FileName, "r" )) == NULL )
{
fprintf( pAbc->Err, "Cannot open input file \"%s\". ", FileName );
if ( FileName = Extra_FileGetSimilarName( FileName, ".mv", ".blif", ".pla", ".mvpla", NULL ) )
if ( FileName = Extra_FileGetSimilarName( FileName, ".mv", ".blif", ".pla", ".eqn", ".bench" ) )
fprintf( pAbc->Err, "Did you mean \"%s\"?", FileName );
fprintf( pAbc->Err, "\n" );
return 1;
@ -199,7 +207,7 @@ int IoCommandReadBlif( Abc_Frame_t * pAbc, int argc, char ** argv )
if ( (pFile = fopen( FileName, "r" )) == NULL )
{
fprintf( pAbc->Err, "Cannot open input file \"%s\". ", FileName );
if ( FileName = Extra_FileGetSimilarName( FileName, ".mv", ".blif", ".pla", ".mvpla", NULL ) )
if ( FileName = Extra_FileGetSimilarName( FileName, ".mv", ".blif", ".pla", ".eqn", ".bench" ) )
fprintf( pAbc->Err, "Did you mean \"%s\"?", FileName );
fprintf( pAbc->Err, "\n" );
return 1;
@ -280,7 +288,7 @@ int IoCommandReadBench( Abc_Frame_t * pAbc, int argc, char ** argv )
if ( (pFile = fopen( FileName, "r" )) == NULL )
{
fprintf( pAbc->Err, "Cannot open input file \"%s\". ", FileName );
if ( FileName = Extra_FileGetSimilarName( FileName, ".mv", ".blif", ".pla", ".mvpla", NULL ) )
if ( FileName = Extra_FileGetSimilarName( FileName, ".mv", ".blif", ".pla", ".eqn", ".bench" ) )
fprintf( pAbc->Err, "Did you mean \"%s\"?", FileName );
fprintf( pAbc->Err, "\n" );
return 1;
@ -360,7 +368,7 @@ int IoCommandReadEdif( Abc_Frame_t * pAbc, int argc, char ** argv )
if ( (pFile = fopen( FileName, "r" )) == NULL )
{
fprintf( pAbc->Err, "Cannot open input file \"%s\". ", FileName );
if ( FileName = Extra_FileGetSimilarName( FileName, ".mv", ".blif", ".pla", ".mvpla", NULL ) )
if ( FileName = Extra_FileGetSimilarName( FileName, ".mv", ".blif", ".pla", ".eqn", ".bench" ) )
fprintf( pAbc->Err, "Did you mean \"%s\"?", FileName );
fprintf( pAbc->Err, "\n" );
return 1;
@ -395,6 +403,86 @@ usage:
return 1;
}
/**Function*************************************************************
Synopsis []
Description []
SideEffects []
SeeAlso []
***********************************************************************/
int IoCommandReadEqn( Abc_Frame_t * pAbc, int argc, char ** argv )
{
Abc_Ntk_t * pNtk, * pTemp;
char * FileName;
FILE * pFile;
int fCheck;
int c;
fCheck = 1;
util_getopt_reset();
while ( ( c = util_getopt( argc, argv, "ch" ) ) != EOF )
{
switch ( c )
{
case 'c':
fCheck ^= 1;
break;
case 'h':
goto usage;
default:
goto usage;
}
}
if ( argc != util_optind + 1 )
{
goto usage;
}
// get the input file name
FileName = argv[util_optind];
if ( (pFile = fopen( FileName, "r" )) == NULL )
{
fprintf( pAbc->Err, "Cannot open input file \"%s\". ", FileName );
if ( FileName = Extra_FileGetSimilarName( FileName, ".mv", ".blif", ".pla", ".eqn", ".bench" ) )
fprintf( pAbc->Err, "Did you mean \"%s\"?", FileName );
fprintf( pAbc->Err, "\n" );
return 1;
}
fclose( pFile );
// set the new network
pNtk = Io_ReadEqn( FileName, fCheck );
if ( pNtk == NULL )
{
fprintf( pAbc->Err, "Reading network from the equation file has failed.\n" );
return 1;
}
pNtk = Abc_NtkNetlistToLogic( pTemp = pNtk );
Abc_NtkDelete( pTemp );
if ( pNtk == NULL )
{
fprintf( pAbc->Err, "Converting to logic network after reading has failed.\n" );
return 1;
}
// replace the current network
Abc_FrameReplaceCurrentNetwork( pAbc, pNtk );
return 0;
usage:
fprintf( pAbc->Err, "usage: read_eqn [-ch] <file>\n" );
fprintf( pAbc->Err, "\t read the network in equation format\n" );
fprintf( pAbc->Err, "\t-c : toggle network check after reading [default = %s]\n", fCheck? "yes":"no" );
fprintf( pAbc->Err, "\t-h : prints the command summary\n" );
fprintf( pAbc->Err, "\tfile : the name of a file to read\n" );
return 1;
}
/**Function*************************************************************
Synopsis []
@ -440,7 +528,7 @@ int IoCommandReadVerilog( Abc_Frame_t * pAbc, int argc, char ** argv )
if ( (pFile = fopen( FileName, "r" )) == NULL )
{
fprintf( pAbc->Err, "Cannot open input file \"%s\". ", FileName );
if ( FileName = Extra_FileGetSimilarName( FileName, ".mv", ".blif", ".pla", ".mvpla", NULL ) )
if ( FileName = Extra_FileGetSimilarName( FileName, ".mv", ".blif", ".pla", ".eqn", ".bench" ) )
fprintf( pAbc->Err, "Did you mean \"%s\"?", FileName );
fprintf( pAbc->Err, "\n" );
return 1;
@ -451,7 +539,7 @@ int IoCommandReadVerilog( Abc_Frame_t * pAbc, int argc, char ** argv )
pNtk = Io_ReadVerilog( FileName, fCheck );
if ( pNtk == NULL )
{
fprintf( pAbc->Err, "Reading network from Verilog file has failed.\n" );
fprintf( pAbc->Err, "Reading network from the verilog file has failed.\n" );
return 1;
}
@ -520,7 +608,7 @@ int IoCommandReadPla( Abc_Frame_t * pAbc, int argc, char ** argv )
if ( (pFile = fopen( FileName, "r" )) == NULL )
{
fprintf( pAbc->Err, "Cannot open input file \"%s\". ", FileName );
if ( FileName = Extra_FileGetSimilarName( FileName, ".mv", ".blif", ".pla", ".mvpla", NULL ) )
if ( FileName = Extra_FileGetSimilarName( FileName, ".mv", ".blif", ".pla", ".eqn", ".bench" ) )
fprintf( pAbc->Err, "Did you mean \"%s\"?", FileName );
fprintf( pAbc->Err, "\n" );
return 1;
@ -753,6 +841,199 @@ usage:
return 1;
}
/**Function*************************************************************
Synopsis []
Description []
SideEffects []
SeeAlso []
***********************************************************************/
int IoCommandWriteDot( Abc_Frame_t * pAbc, int argc, char **argv )
{
char * FileName;
Vec_Ptr_t * vNodes;
int c;
util_getopt_reset();
while ( ( c = util_getopt( argc, argv, "h" ) ) != EOF )
{
switch ( c )
{
case 'h':
goto usage;
default:
goto usage;
}
}
if ( pAbc->pNtkCur == NULL )
{
fprintf( pAbc->Out, "Empty network.\n" );
return 0;
}
if ( !Abc_NtkIsStrash(pAbc->pNtkCur) )
{
fprintf( stdout, "IoCommandWriteDot(): Currently can only process logic networks with BDDs.\n" );
return 0;
}
if ( argc != util_optind + 1 )
{
goto usage;
}
// get the input file name
FileName = argv[util_optind];
// write the file
vNodes = Abc_NtkCollectObjects( pAbc->pNtkCur );
Io_WriteDot( pAbc->pNtkCur, vNodes, NULL, FileName );
Vec_PtrFree( vNodes );
return 0;
usage:
fprintf( pAbc->Err, "usage: write_dot [-h] <file>\n" );
fprintf( pAbc->Err, "\t write the AIG into a DOT file\n" );
fprintf( pAbc->Err, "\t-h : print the help massage\n" );
fprintf( pAbc->Err, "\tfile : the name of the file to write\n" );
return 1;
}
/**Function*************************************************************
Synopsis []
Description []
SideEffects []
SeeAlso []
***********************************************************************/
int IoCommandWriteEqn( Abc_Frame_t * pAbc, int argc, char **argv )
{
Abc_Ntk_t * pNtk, * pNtkTemp;
char * FileName;
int c;
util_getopt_reset();
while ( ( c = util_getopt( argc, argv, "h" ) ) != EOF )
{
switch ( c )
{
case 'h':
goto usage;
default:
goto usage;
}
}
pNtk = pAbc->pNtkCur;
if ( pNtk == NULL )
{
fprintf( pAbc->Out, "Empty network.\n" );
return 0;
}
if ( argc != util_optind + 1 )
{
goto usage;
}
if ( !Abc_NtkIsLogic(pNtk) && !Abc_NtkIsStrash(pNtk) )
{
fprintf( stdout, "IoCommandWriteGml(): Currently can only process logic networks with BDDs.\n" );
return 0;
}
// get the input file name
FileName = argv[util_optind];
// write the file
// get rid of complemented covers if present
if ( Abc_NtkIsSopLogic(pNtk) )
Abc_NtkLogicMakeDirectSops(pNtk);
// derive the netlist
pNtkTemp = Abc_NtkLogicToNetlist(pNtk);
if ( pNtkTemp == NULL )
{
fprintf( pAbc->Out, "Writing BENCH has failed.\n" );
return 0;
}
Io_WriteEqn( pNtkTemp, FileName );
Abc_NtkDelete( pNtkTemp );
return 0;
usage:
fprintf( pAbc->Err, "usage: write_eqn [-h] <file>\n" );
fprintf( pAbc->Err, "\t write the current network in the equation format\n" );
fprintf( pAbc->Err, "\t-h : print the help massage\n" );
fprintf( pAbc->Err, "\tfile : the name of the file to write\n" );
return 1;
}
/**Function*************************************************************
Synopsis []
Description []
SideEffects []
SeeAlso []
***********************************************************************/
int IoCommandWriteGml( Abc_Frame_t * pAbc, int argc, char **argv )
{
char * FileName;
int c;
util_getopt_reset();
while ( ( c = util_getopt( argc, argv, "h" ) ) != EOF )
{
switch ( c )
{
case 'h':
goto usage;
default:
goto usage;
}
}
if ( pAbc->pNtkCur == NULL )
{
fprintf( pAbc->Out, "Empty network.\n" );
return 0;
}
if ( !Abc_NtkIsLogic(pAbc->pNtkCur) && !Abc_NtkIsStrash(pAbc->pNtkCur) )
{
fprintf( stdout, "IoCommandWriteGml(): Currently can only process logic networks with BDDs.\n" );
return 0;
}
if ( argc != util_optind + 1 )
{
goto usage;
}
// get the input file name
FileName = argv[util_optind];
// write the file
Io_WriteGml( pAbc->pNtkCur, FileName );
return 0;
usage:
fprintf( pAbc->Err, "usage: write_gml [-h] <file>\n" );
fprintf( pAbc->Err, "\t write network using graph representation formal GML\n" );
fprintf( pAbc->Err, "\t-h : print the help massage\n" );
fprintf( pAbc->Err, "\tfile : the name of the file to write\n" );
return 1;
}
/**Function*************************************************************
Synopsis []

View File

@ -53,6 +53,8 @@ extern Abc_Ntk_t * Io_ReadBlif( char * pFileName, int fCheck );
extern Abc_Ntk_t * Io_ReadBench( char * pFileName, int fCheck );
/*=== abcReadEdif.c ==========================================================*/
extern Abc_Ntk_t * Io_ReadEdif( char * pFileName, int fCheck );
/*=== abcReadEqn.c ==========================================================*/
extern Abc_Ntk_t * Io_ReadEqn( char * pFileName, int fCheck );
/*=== abcReadVerilog.c ==========================================================*/
extern Abc_Ntk_t * Io_ReadVerilog( char * pFileName, int fCheck );
/*=== abcReadPla.c ==========================================================*/
@ -73,6 +75,12 @@ extern void Io_WriteTimingInfo( FILE * pFile, Abc_Ntk_t * pNtk );
extern int Io_WriteBench( Abc_Ntk_t * pNtk, char * FileName );
/*=== abcWriteCnf.c ==========================================================*/
extern int Io_WriteCnf( Abc_Ntk_t * pNtk, char * FileName );
/*=== abcWriteDot.c ==========================================================*/
extern void Io_WriteDot( Abc_Ntk_t * pNtk, Vec_Ptr_t * vNodes, Vec_Ptr_t * vNodesShow, char * pFileName );
/*=== abcWriteEqn.c ==========================================================*/
extern void Io_WriteEqn( Abc_Ntk_t * pNtk, char * pFileName );
/*=== abcWriteGml.c ==========================================================*/
extern void Io_WriteGml( Abc_Ntk_t * pNtk, char * pFileName );
/*=== abcWritePla.c ==========================================================*/
extern int Io_WritePla( Abc_Ntk_t * pNtk, char * FileName );

View File

@ -53,6 +53,8 @@ Abc_Ntk_t * Io_Read( char * pFileName, int fCheck )
pNtk = Io_ReadEdif( pFileName, fCheck );
else if ( Extra_FileNameCheckExtension( pFileName, "pla" ) )
pNtk = Io_ReadPla( pFileName, fCheck );
else if ( Extra_FileNameCheckExtension( pFileName, "eqn" ) )
pNtk = Io_ReadEqn( pFileName, fCheck );
else
{
fprintf( stderr, "Unknown file format\n" );

254
src/base/io/ioReadEqn.c Normal file
View File

@ -0,0 +1,254 @@
/**CFile****************************************************************
FileName [ioReadEqn.c]
SystemName [ABC: Logic synthesis and verification system.]
PackageName [Command processing package.]
Synopsis [Procedures to read equation format files.]
Author [Alan Mishchenko]
Affiliation [UC Berkeley]
Date [Ver. 1.0. Started - June 20, 2005.]
Revision [$Id: ioReadEqn.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
***********************************************************************/
#include "io.h"
////////////////////////////////////////////////////////////////////////
/// DECLARATIONS ///
////////////////////////////////////////////////////////////////////////
static Abc_Ntk_t * Io_ReadEqnNetwork( Extra_FileReader_t * p );
static void Io_ReadEqnStrCompact( char * pStr );
static int Io_ReadEqnStrFind( Vec_Ptr_t * vTokens, char * pName );
static void Io_ReadEqnStrCutAt( char * pStr, char * pStop, int fUniqueOnly, Vec_Ptr_t * vTokens );
////////////////////////////////////////////////////////////////////////
/// FUNCTION DEFITIONS ///
////////////////////////////////////////////////////////////////////////
/**Function*************************************************************
Synopsis [Reads the network from a BENCH file.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
Abc_Ntk_t * Io_ReadEqn( char * pFileName, int fCheck )
{
Extra_FileReader_t * p;
Abc_Ntk_t * pNtk;
// start the file
p = Extra_FileReaderAlloc( pFileName, "#", ";", "=" );
if ( p == NULL )
return NULL;
// read the network
pNtk = Io_ReadEqnNetwork( p );
Extra_FileReaderFree( p );
if ( pNtk == NULL )
return NULL;
// make sure that everything is okay with the network structure
if ( fCheck && !Abc_NtkCheck( pNtk ) )
{
printf( "Io_ReadEqn: The network check has failed.\n" );
Abc_NtkDelete( pNtk );
return NULL;
}
return pNtk;
}
/**Function*************************************************************
Synopsis []
Description []
SideEffects []
SeeAlso []
***********************************************************************/
Abc_Ntk_t * Io_ReadEqnNetwork( Extra_FileReader_t * p )
{
ProgressBar * pProgress;
Vec_Ptr_t * vTokens;
Vec_Ptr_t * vCubes, * vLits, * vVars;
Abc_Ntk_t * pNtk;
Abc_Obj_t * pNode;
char * pCubesCopy, * pSopCube, * pVarName;
int iLine, iNum, i, k;
// allocate the empty network
pNtk = Abc_NtkStartRead( Extra_FileReaderGetFileName(p) );
// go through the lines of the file
vCubes = Vec_PtrAlloc( 100 );
vVars = Vec_PtrAlloc( 100 );
vLits = Vec_PtrAlloc( 100 );
pProgress = Extra_ProgressBarStart( stdout, Extra_FileReaderGetFileSize(p) );
for ( iLine = 0; vTokens = Extra_FileReaderGetTokens(p); iLine++ )
{
Extra_ProgressBarUpdate( pProgress, Extra_FileReaderGetCurPosition(p), NULL );
// check if the first token contains anything
Io_ReadEqnStrCompact( vTokens->pArray[0] );
if ( strlen(vTokens->pArray[0]) == 0 )
break;
// if the number of tokens is different from two, error
if ( vTokens->nSize != 2 )
{
printf( "%s: Wrong input file format.\n", Extra_FileReaderGetFileName(p) );
Abc_NtkDelete( pNtk );
return NULL;
}
// get the type of the line
if ( strncmp( vTokens->pArray[0], "INORDER", 7 ) == 0 )
{
Io_ReadEqnStrCutAt( vTokens->pArray[1], " \n\r\t", 0, vVars );
Vec_PtrForEachEntry( vVars, pVarName, i )
Io_ReadCreatePi( pNtk, pVarName );
}
else if ( strncmp( vTokens->pArray[0], "OUTORDER", 8 ) == 0 )
{
Io_ReadEqnStrCutAt( vTokens->pArray[1], " \n\r\t", 0, vVars );
Vec_PtrForEachEntry( vVars, pVarName, i )
Io_ReadCreatePo( pNtk, pVarName );
}
else
{
// remove spaces
pCubesCopy = vTokens->pArray[1];
Io_ReadEqnStrCompact( pCubesCopy );
// consider the case of the constant node
if ( (pCubesCopy[0] == '0' || pCubesCopy[0] == '1') && pCubesCopy[1] == 0 )
{
pNode = Io_ReadCreateNode( pNtk, vTokens->pArray[0], NULL, 0 );
if ( pCubesCopy[0] == '0' )
pNode->pData = Abc_SopCreateConst0( pNtk->pManFunc );
else
pNode->pData = Abc_SopCreateConst1( pNtk->pManFunc );
continue;
}
// determine unique variables
pCubesCopy = util_strsav( pCubesCopy );
// find the names of the fanins of this node
Io_ReadEqnStrCutAt( pCubesCopy, "!*+", 1, vVars );
// create the node
pNode = Io_ReadCreateNode( pNtk, vTokens->pArray[0], (char **)vVars->pArray, vVars->nSize );
// split the string into cubes
Io_ReadEqnStrCutAt( vTokens->pArray[1], "+", 0, vCubes );
// start the sop
pNode->pData = Abc_SopStart( pNtk->pManFunc, vCubes->nSize, vVars->nSize );
// read the cubes
i = 0;
Abc_SopForEachCube( pNode->pData, vVars->nSize, pSopCube )
{
// split this cube into lits
Io_ReadEqnStrCutAt( vCubes->pArray[i], "*", 0, vLits );
// read the literals
Vec_PtrForEachEntry( vLits, pVarName, k )
{
iNum = Io_ReadEqnStrFind( vVars, pVarName + (pVarName[0] == '!') );
assert( iNum >= 0 );
pSopCube[iNum] = '1' - (pVarName[0] == '!');
}
i++;
}
assert( i == vCubes->nSize );
// remove the cubes
free( pCubesCopy );
}
}
Extra_ProgressBarStop( pProgress );
Vec_PtrFree( vCubes );
Vec_PtrFree( vLits );
Vec_PtrFree( vVars );
Abc_NtkFinalizeRead( pNtk );
return pNtk;
}
/**Function*************************************************************
Synopsis [Compacts the string by throwing away space-like chars.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
void Io_ReadEqnStrCompact( char * pStr )
{
char * pCur, * pNew;
for ( pNew = pCur = pStr; *pCur; pCur++ )
if ( !(*pCur == ' ' || *pCur == '\n' || *pCur == '\r' || *pCur == '\t') )
*pNew++ = *pCur;
*pNew = 0;
}
/**Function*************************************************************
Synopsis [Determines unique variables in the string.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
int Io_ReadEqnStrFind( Vec_Ptr_t * vTokens, char * pName )
{
char * pToken;
int i;
Vec_PtrForEachEntry( vTokens, pToken, i )
if ( strcmp( pToken, pName ) == 0 )
return i;
return -1;
}
/**Function*************************************************************
Synopsis [Cuts the string into pieces using stop chars.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
void Io_ReadEqnStrCutAt( char * pStr, char * pStop, int fUniqueOnly, Vec_Ptr_t * vTokens )
{
char * pToken;
Vec_PtrClear( vTokens );
for ( pToken = strtok( pStr, pStop ); pToken; pToken = strtok( NULL, pStop ) )
if ( !fUniqueOnly || Io_ReadEqnStrFind( vTokens, pToken ) == -1 )
Vec_PtrPush( vTokens, pToken );
}
////////////////////////////////////////////////////////////////////////
/// END OF FILE ///
////////////////////////////////////////////////////////////////////////

View File

@ -107,10 +107,7 @@ void Io_WriteBlif( Abc_Ntk_t * pNtk, char * FileName, int fWriteLatches )
Synopsis [Write one network.]
Description [Writes a network composed of PIs, POs, internal nodes,
and latches. The following rules are used to print the names of
internal nodes:
]
Description []
SideEffects []

View File

@ -6,7 +6,7 @@
PackageName [Command processing package.]
Synopsis [Procedures to CNF of the miter cone.]
Synopsis [Procedures to output CNF of the miter cone.]
Author [Alan Mishchenko]
@ -24,8 +24,6 @@
/// DECLARATIONS ///
////////////////////////////////////////////////////////////////////////
static void Io_WriteCnfInt( FILE * pFile, Abc_Ntk_t * pNtk );
////////////////////////////////////////////////////////////////////////
/// FUNCTION DEFITIONS ///
////////////////////////////////////////////////////////////////////////

322
src/base/io/ioWriteDot.c Normal file
View File

@ -0,0 +1,322 @@
/**CFile****************************************************************
FileName [ioWriteDot.c]
SystemName [ABC: Logic synthesis and verification system.]
PackageName [Command processing package.]
Synopsis [Procedures to write the graph structure of AIG in DOT.]
Author [Alan Mishchenko]
Affiliation [UC Berkeley]
Date [Ver. 1.0. Started - June 20, 2005.]
Revision [$Id: ioWriteDot.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
***********************************************************************/
#include "io.h"
////////////////////////////////////////////////////////////////////////
/// DECLARATIONS ///
////////////////////////////////////////////////////////////////////////
////////////////////////////////////////////////////////////////////////
/// FUNCTION DEFITIONS ///
////////////////////////////////////////////////////////////////////////
/**Function*************************************************************
Synopsis [Writes the graph structure of AIG in DOT.]
Description [Useful for graph visualization using tools such as GraphViz:
http://www.graphviz.org/]
SideEffects []
SeeAlso []
***********************************************************************/
void Io_WriteDot( Abc_Ntk_t * pNtk, Vec_Ptr_t * vNodes, Vec_Ptr_t * vNodesShow, char * pFileName )
{
FILE * pFile;
Abc_Obj_t * pNode, * pTemp, * pPrev;
int LevelMin, LevelMax, fHasCos, Level, i;
int Limit = 200;
if ( vNodes->nSize < 1 )
{
printf( "The set has no nodes. DOT file is not written.\n" );
return;
}
if ( vNodes->nSize > Limit )
{
printf( "The set has more than %d nodes. DOT file is not written.\n", Limit );
return;
}
// start the stream
if ( (pFile = fopen( pFileName, "w" )) == NULL )
{
fprintf( stdout, "Cannot open the intermediate file \"%s\".\n", pFileName );
return;
}
// mark the nodes from the set
Vec_PtrForEachEntry( vNodes, pNode, i )
pNode->fMarkC = 1;
if ( vNodesShow )
Vec_PtrForEachEntry( vNodesShow, pNode, i )
pNode->fMarkB = 1;
// find the largest and the smallest levels
LevelMin = 10000;
LevelMax = -1;
fHasCos = 0;
Vec_PtrForEachEntry( vNodes, pNode, i )
{
if ( Abc_ObjIsCo(pNode) )
{
fHasCos = 1;
continue;
}
if ( LevelMin > (int)pNode->Level )
LevelMin = pNode->Level;
if ( LevelMax < (int)pNode->Level )
LevelMax = pNode->Level;
}
// set the level of the CO nodes
if ( fHasCos )
{
LevelMax++;
Vec_PtrForEachEntry( vNodes, pNode, i )
{
if ( Abc_ObjIsCo(pNode) )
pNode->Level = LevelMax;
}
}
// write the DOT header
fprintf( pFile, "# %s\n", "AIG generated by ABC" );
fprintf( pFile, "\n" );
fprintf( pFile, "digraph AIG {\n" );
fprintf( pFile, "size = \"7.5,10\";\n" );
// fprintf( pFile, "ranksep = 0.5;\n" );
// fprintf( pFile, "nodesep = 0.5;\n" );
fprintf( pFile, "center = true;\n" );
// fprintf( pFile, "edge [fontsize = 10];\n" );
// fprintf( pFile, "edge [dir = none];\n" );
fprintf( pFile, "\n" );
// labels on the left of the picture
fprintf( pFile, "{\n" );
fprintf( pFile, " node [shape = plaintext];\n" );
fprintf( pFile, " edge [style = invis];\n" );
fprintf( pFile, " LevelTitle1 [label=\"\"];\n" );
fprintf( pFile, " LevelTitle2 [label=\"\"];\n" );
// generate node names with labels
for ( Level = LevelMax; Level >= LevelMin; Level-- )
{
// the visible node name
fprintf( pFile, " Level%d", Level );
fprintf( pFile, " [label = " );
// label name
fprintf( pFile, "\"" );
fprintf( pFile, "\"" );
fprintf( pFile, "];\n" );
}
// genetate the sequence of visible/invisible nodes to mark levels
fprintf( pFile, " LevelTitle1 -> LevelTitle2 ->" );
for ( Level = LevelMax; Level >= LevelMin; Level-- )
{
// the visible node name
fprintf( pFile, " Level%d", Level );
// the connector
if ( Level != LevelMin )
fprintf( pFile, " ->" );
else
fprintf( pFile, ";" );
}
fprintf( pFile, "\n" );
fprintf( pFile, "}" );
fprintf( pFile, "\n" );
fprintf( pFile, "\n" );
// generate title box on top
fprintf( pFile, "{\n" );
fprintf( pFile, " rank = same;\n" );
fprintf( pFile, " LevelTitle1;\n" );
fprintf( pFile, " title1 [shape=plaintext,\n" );
fprintf( pFile, " fontsize=20,\n" );
fprintf( pFile, " fontname = \"Times-Roman\",\n" );
fprintf( pFile, " label=\"" );
fprintf( pFile, "%s", "AIG generated by ABC" );
fprintf( pFile, "\\n" );
fprintf( pFile, "Benchmark \\\"%s\\\". ", pNtk->pName );
fprintf( pFile, "Time was %s. ", Extra_TimeStamp() );
fprintf( pFile, "\"\n" );
fprintf( pFile, " ];\n" );
fprintf( pFile, "}" );
fprintf( pFile, "\n" );
fprintf( pFile, "\n" );
// generate statistics box
fprintf( pFile, "{\n" );
fprintf( pFile, " rank = same;\n" );
fprintf( pFile, " LevelTitle2;\n" );
fprintf( pFile, " title2 [shape=plaintext,\n" );
fprintf( pFile, " fontsize=18,\n" );
fprintf( pFile, " fontname = \"Times-Roman\",\n" );
fprintf( pFile, " label=\"" );
fprintf( pFile, "The set contains %d nodes and spans %d levels.", vNodes->nSize, LevelMax - LevelMin );
fprintf( pFile, "\\n" );
fprintf( pFile, "\"\n" );
fprintf( pFile, " ];\n" );
fprintf( pFile, "}" );
fprintf( pFile, "\n" );
fprintf( pFile, "\n" );
// generate the POs
if ( fHasCos )
{
fprintf( pFile, "{\n" );
fprintf( pFile, " rank = same;\n" );
// the labeling node of this level
fprintf( pFile, " Level%d;\n", LevelMax );
// generat the PO nodes
Vec_PtrForEachEntry( vNodes, pNode, i )
{
if ( !Abc_ObjIsCo(pNode) )
continue;
fprintf( pFile, " Node%d [label = \"%s\"", pNode->Id, Abc_ObjName(pNode) );
fprintf( pFile, ", shape = invtriangle" );
if ( pNode->fMarkB )
fprintf( pFile, ", style = filled" );
fprintf( pFile, ", color = coral, fillcolor = coral" );
fprintf( pFile, "];\n" );
}
fprintf( pFile, "}" );
fprintf( pFile, "\n" );
fprintf( pFile, "\n" );
}
// generate nodes of each rank
for ( Level = LevelMax - fHasCos; Level >= LevelMin && Level > 0; Level-- )
{
fprintf( pFile, "{\n" );
fprintf( pFile, " rank = same;\n" );
// the labeling node of this level
fprintf( pFile, " Level%d;\n", Level );
Vec_PtrForEachEntry( vNodes, pNode, i )
{
if ( (int)pNode->Level != Level )
continue;
fprintf( pFile, " Node%d [label = \"%d\"", pNode->Id, pNode->Id );
fprintf( pFile, ", shape = ellipse" );
if ( pNode->fMarkB )
fprintf( pFile, ", style = filled" );
fprintf( pFile, "];\n" );
}
fprintf( pFile, "}" );
fprintf( pFile, "\n" );
fprintf( pFile, "\n" );
}
// generate the PI nodes if any
if ( LevelMin == 0 )
{
fprintf( pFile, "{\n" );
fprintf( pFile, " rank = same;\n" );
// the labeling node of this level
fprintf( pFile, " Level%d;\n", LevelMin );
// generat the PO nodes
Vec_PtrForEachEntry( vNodes, pNode, i )
{
if ( !Abc_ObjIsCi(pNode) )
continue;
fprintf( pFile, " Node%d [label = \"%s\"", pNode->Id, Abc_ObjName(pNode) );
fprintf( pFile, ", shape = triangle" );
if ( pNode->fMarkB )
fprintf( pFile, ", style = filled" );
fprintf( pFile, ", color = coral, fillcolor = coral" );
fprintf( pFile, "];\n" );
}
fprintf( pFile, "}" );
fprintf( pFile, "\n" );
fprintf( pFile, "\n" );
}
// generate invisible edges from the square down
fprintf( pFile, "title1 -> title2 [style = invis];\n" );
Vec_PtrForEachEntry( vNodes, pNode, i )
{
if ( (int)pNode->Level != LevelMax )
continue;
fprintf( pFile, "title2 -> Node%d [style = invis];\n", pNode->Id );
}
// generate edges
Vec_PtrForEachEntry( vNodes, pNode, i )
{
if ( Abc_ObjFaninNum(pNode) == 0 )
continue;
// generate the edge from this node to the next
if ( Abc_ObjFanin0(pNode)->fMarkC )
{
fprintf( pFile, "Node%d", pNode->Id );
fprintf( pFile, " -> " );
fprintf( pFile, "Node%d", Abc_ObjFaninId0(pNode) );
fprintf( pFile, " [style = %s]", Abc_ObjFaninC0(pNode)? "dashed" : "bold" );
fprintf( pFile, ";\n" );
}
if ( Abc_ObjFaninNum(pNode) == 1 )
continue;
// generate the edge from this node to the next
if ( Abc_ObjFanin1(pNode)->fMarkC )
{
fprintf( pFile, "Node%d", pNode->Id );
fprintf( pFile, " -> " );
fprintf( pFile, "Node%d", Abc_ObjFaninId1(pNode) );
fprintf( pFile, " [style = %s]", Abc_ObjFaninC1(pNode)? "dashed" : "bold" );
fprintf( pFile, ";\n" );
}
// generate the edges between the equivalent nodes
pPrev = pNode;
for ( pTemp = pNode->pData; pTemp; pTemp = pTemp->pData )
{
if ( pTemp->fMarkC )
{
fprintf( pFile, "Node%d", pPrev->Id );
fprintf( pFile, " -> " );
fprintf( pFile, "Node%d", pTemp->Id );
fprintf( pFile, " [style = %s]", (pPrev->fPhase ^ pTemp->fPhase)? "dashed" : "bold" );
fprintf( pFile, ";\n" );
pPrev = pTemp;
}
}
}
fprintf( pFile, "}" );
fprintf( pFile, "\n" );
fprintf( pFile, "\n" );
fclose( pFile );
// unmark the nodes from the set
Vec_PtrForEachEntry( vNodes, pNode, i )
pNode->fMarkC = 0;
if ( vNodesShow )
Vec_PtrForEachEntry( vNodesShow, pNode, i )
pNode->fMarkB = 0;
}
////////////////////////////////////////////////////////////////////////
/// END OF FILE ///
////////////////////////////////////////////////////////////////////////

261
src/base/io/ioWriteEqn.c Normal file
View File

@ -0,0 +1,261 @@
/**CFile****************************************************************
FileName [ioWriteEqn.c]
SystemName [ABC: Logic synthesis and verification system.]
PackageName [Command processing package.]
Synopsis [Procedures to write equation representation of the network.]
Author [Alan Mishchenko]
Affiliation [UC Berkeley]
Date [Ver. 1.0. Started - June 20, 2005.]
Revision [$Id: ioWriteEqn.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
***********************************************************************/
#include "io.h"
////////////////////////////////////////////////////////////////////////
/// DECLARATIONS ///
////////////////////////////////////////////////////////////////////////
static void Io_NtkWriteEqnOne( FILE * pFile, Abc_Ntk_t * pNtk );
static void Io_NtkWriteEqnPis( FILE * pFile, Abc_Ntk_t * pNtk );
static void Io_NtkWriteEqnPos( FILE * pFile, Abc_Ntk_t * pNtk );
static void Io_NtkWriteEqnNode( FILE * pFile, Abc_Obj_t * pNode );
////////////////////////////////////////////////////////////////////////
/// FUNCTION DEFITIONS ///
////////////////////////////////////////////////////////////////////////
/**Function*************************************************************
Synopsis [Writes the logic network in the equation format.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
void Io_WriteEqn( Abc_Ntk_t * pNtk, char * pFileName )
{
FILE * pFile;
assert( Abc_NtkIsSopNetlist(pNtk) );
if ( Abc_NtkLatchNum(pNtk) > 0 )
printf( "Warning: only combinational portion is being written.\n" );
// start the output stream
pFile = fopen( pFileName, "w" );
if ( pFile == NULL )
{
fprintf( stdout, "Io_WriteEqn(): Cannot open the output file \"%s\".\n", pFileName );
return;
}
fprintf( pFile, "# Equations for \"%s\" written by ABC on %s\n", pNtk->pName, Extra_TimeStamp() );
// write the equations for the network
Io_NtkWriteEqnOne( pFile, pNtk );
fprintf( pFile, "\n" );
fclose( pFile );
}
/**Function*************************************************************
Synopsis [Write one network.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
void Io_NtkWriteEqnOne( FILE * pFile, Abc_Ntk_t * pNtk )
{
ProgressBar * pProgress;
Abc_Obj_t * pNode;
int i;
// write the PIs
fprintf( pFile, "INORDER =" );
Io_NtkWriteEqnPis( pFile, pNtk );
fprintf( pFile, ";\n" );
// write the POs
fprintf( pFile, "OUTORDER =" );
Io_NtkWriteEqnPos( pFile, pNtk );
fprintf( pFile, ";\n" );
// write each internal node
pProgress = Extra_ProgressBarStart( stdout, Abc_NtkObjNumMax(pNtk) );
Abc_NtkForEachNode( pNtk, pNode, i )
{
Extra_ProgressBarUpdate( pProgress, i, NULL );
Io_NtkWriteEqnNode( pFile, pNode );
}
Extra_ProgressBarStop( pProgress );
}
/**Function*************************************************************
Synopsis [Writes the primary input list.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
void Io_NtkWriteEqnPis( FILE * pFile, Abc_Ntk_t * pNtk )
{
Abc_Obj_t * pTerm, * pNet;
int LineLength;
int AddedLength;
int NameCounter;
int i;
LineLength = 9;
NameCounter = 0;
Abc_NtkForEachCi( pNtk, pTerm, i )
{
pNet = Abc_ObjFanout0(pTerm);
// get the line length after this name is written
AddedLength = strlen(Abc_ObjName(pNet)) + 1;
if ( NameCounter && LineLength + AddedLength + 3 > IO_WRITE_LINE_LENGTH )
{ // write the line extender
fprintf( pFile, " \n" );
// reset the line length
LineLength = 0;
NameCounter = 0;
}
fprintf( pFile, " %s", Abc_ObjName(pNet) );
LineLength += AddedLength;
NameCounter++;
}
}
/**Function*************************************************************
Synopsis [Writes the primary input list.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
void Io_NtkWriteEqnPos( FILE * pFile, Abc_Ntk_t * pNtk )
{
Abc_Obj_t * pTerm, * pNet;
int LineLength;
int AddedLength;
int NameCounter;
int i;
LineLength = 10;
NameCounter = 0;
Abc_NtkForEachCo( pNtk, pTerm, i )
{
pNet = Abc_ObjFanin0(pTerm);
// get the line length after this name is written
AddedLength = strlen(Abc_ObjName(pNet)) + 1;
if ( NameCounter && LineLength + AddedLength + 3 > IO_WRITE_LINE_LENGTH )
{ // write the line extender
fprintf( pFile, " \n" );
// reset the line length
LineLength = 0;
NameCounter = 0;
}
fprintf( pFile, " %s", Abc_ObjName(pNet) );
LineLength += AddedLength;
NameCounter++;
}
}
/**Function*************************************************************
Synopsis [Write the node into a file.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
void Io_NtkWriteEqnNode( FILE * pFile, Abc_Obj_t * pNode )
{
Abc_Obj_t * pNet;
int LineLength;
int AddedLength;
int NameCounter;
char * pCube;
int Value, fFirstLit, i;
fprintf( pFile, "%s = ", Abc_ObjName(pNode) );
if ( Abc_SopIsConst0(pNode->pData) )
{
fprintf( pFile, "0;\n" );
return;
}
if ( Abc_SopIsConst1(pNode->pData) )
{
fprintf( pFile, "1;\n" );
return;
}
NameCounter = 0;
LineLength = strlen(Abc_ObjName(pNode)) + 3;
Abc_SopForEachCube( pNode->pData, Abc_ObjFaninNum(pNode), pCube )
{
if ( pCube != pNode->pData )
{
fprintf( pFile, " + " );
LineLength += 3;
}
// add the cube
fFirstLit = 1;
Abc_CubeForEachVar( pCube, Value, i )
{
if ( Value == '-' )
continue;
pNet = Abc_ObjFanin( pNode, i );
// get the line length after this name is written
AddedLength = !fFirstLit + (Value == '0') + strlen(Abc_ObjName(pNet));
if ( NameCounter && LineLength + AddedLength + 6 > IO_WRITE_LINE_LENGTH )
{ // write the line extender
fprintf( pFile, " \n " );
// reset the line length
LineLength = 0;
NameCounter = 0;
}
fprintf( pFile, "%s%s%s", (fFirstLit? "": "*"), ((Value == '0')? "!":""), Abc_ObjName(pNet) );
LineLength += AddedLength;
NameCounter++;
fFirstLit = 0;
}
}
fprintf( pFile, ";\n" );
}
////////////////////////////////////////////////////////////////////////
/// END OF FILE ///
////////////////////////////////////////////////////////////////////////

116
src/base/io/ioWriteGml.c Normal file
View File

@ -0,0 +1,116 @@
/**CFile****************************************************************
FileName [ioWriteGml.c]
SystemName [ABC: Logic synthesis and verification system.]
PackageName [Command processing package.]
Synopsis [Procedures to write the graph structure of AIG in GML.]
Author [Alan Mishchenko]
Affiliation [UC Berkeley]
Date [Ver. 1.0. Started - June 20, 2005.]
Revision [$Id: ioWriteGml.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
***********************************************************************/
#include "io.h"
////////////////////////////////////////////////////////////////////////
/// DECLARATIONS ///
////////////////////////////////////////////////////////////////////////
////////////////////////////////////////////////////////////////////////
/// FUNCTION DEFITIONS ///
////////////////////////////////////////////////////////////////////////
/**Function*************************************************************
Synopsis [Writes the graph structure of AIG in GML.]
Description [Useful for graph visualization using tools such as yEd:
http://www.yworks.com/]
SideEffects []
SeeAlso []
***********************************************************************/
void Io_WriteGml( Abc_Ntk_t * pNtk, char * pFileName )
{
FILE * pFile;
Abc_Obj_t * pObj, * pFanin;
int i, k;
assert( Abc_NtkIsStrash(pNtk) || Abc_NtkIsLogic(pNtk) );
// start the output stream
pFile = fopen( pFileName, "w" );
if ( pFile == NULL )
{
fprintf( stdout, "Io_WriteGml(): Cannot open the output file \"%s\".\n", pFileName );
return;
}
fprintf( pFile, "# GML for \"%s\" written by ABC on %s\n", pNtk->pName, Extra_TimeStamp() );
fprintf( pFile, "graph [\n" );
// output the POs
fprintf( pFile, "\n" );
Abc_NtkForEachPo( pNtk, pObj, i )
{
fprintf( pFile, " node [ id %5d label \"%s\"\n", pObj->Id, Abc_ObjName(pObj) );
fprintf( pFile, " graphics [ type \"triangle\" fill \"#00FFFF\" ]\n" ); // blue
fprintf( pFile, " ]\n" );
}
// output the PIs
fprintf( pFile, "\n" );
Abc_NtkForEachPi( pNtk, pObj, i )
{
fprintf( pFile, " node [ id %5d label \"%s\"\n", pObj->Id, Abc_ObjName(pObj) );
fprintf( pFile, " graphics [ type \"triangle\" fill \"#00FF00\" ]\n" ); // green
fprintf( pFile, " ]\n" );
}
// output the latches
fprintf( pFile, "\n" );
Abc_NtkForEachLatch( pNtk, pObj, i )
{
fprintf( pFile, " node [ id %5d label \"%s\"\n", pObj->Id, Abc_ObjName(pObj) );
fprintf( pFile, " graphics [ type \"rectangle\" fill \"#FF0000\" ]\n" ); // red
fprintf( pFile, " ]\n" );
}
// output the nodes
fprintf( pFile, "\n" );
Abc_NtkForEachNode( pNtk, pObj, i )
{
fprintf( pFile, " node [ id %5d label \"%s\"\n", pObj->Id, Abc_ObjName(pObj) );
fprintf( pFile, " graphics [ type \"ellipse\" fill \"#CCCCFF\" ]\n" ); // grey
fprintf( pFile, " ]\n" );
}
// output the edges
fprintf( pFile, "\n" );
Abc_NtkForEachObj( pNtk, pObj, i )
{
Abc_ObjForEachFanin( pObj, pFanin, k )
{
fprintf( pFile, " edge [ source %5d target %5d\n", pObj->Id, pFanin->Id );
fprintf( pFile, " graphics [ type \"line\" arrow \"first\" ]\n" );
fprintf( pFile, " ]\n" );
}
}
fprintf( pFile, "]\n" );
fprintf( pFile, "\n" );
fclose( pFile );
}
////////////////////////////////////////////////////////////////////////
/// END OF FILE ///
////////////////////////////////////////////////////////////////////////

View File

@ -3,10 +3,14 @@ SRC += src/base/io/io.c \
src/base/io/ioReadBench.c \
src/base/io/ioReadBlif.c \
src/base/io/ioReadEdif.c \
src/base/io/ioReadEqn.c \
src/base/io/ioReadPla.c \
src/base/io/ioReadVerilog.c \
src/base/io/ioUtil.c \
src/base/io/ioWriteBench.c \
src/base/io/ioWriteBlif.c \
src/base/io/ioWriteCnf.c \
src/base/io/ioWriteDot.c \
src/base/io/ioWriteEqn.c \
src/base/io/ioWriteGml.c \
src/base/io/ioWritePla.c

View File

@ -71,7 +71,7 @@ int Fpga_Mapping( Fpga_Man_t * p )
return 0;
p->timeRecover = clock() - clk;
}
PRT( "Total mapping time", clock() - clkTotal );
//PRT( "Total mapping time", clock() - clkTotal );
// print the AI-graph used for mapping
//Fpga_ManShow( p, "test" );

View File

@ -117,6 +117,57 @@ extern DdNode * Extra_bddFindOneCube( DdManager * dd, DdNode * bF );
extern DdNode * Extra_bddGetOneCube( DdManager * dd, DdNode * bFunc );
extern DdNode * Extra_bddComputeRangeCube( DdManager * dd, int iStart, int iStop );
/*=== extraBddSymm.c =================================================================*/
typedef struct Extra_SymmInfo_t_ Extra_SymmInfo_t;
struct Extra_SymmInfo_t_ {
int nVars; // the number of variables in the support
int nVarsMax; // the number of variables in the DD manager
int nSymms; // the number of pair-wise symmetries
int nNodes; // the number of nodes in a ZDD (if applicable)
int * pVars; // the list of all variables present in the support
char ** pSymms; // the symmetry information
};
/* computes the classical symmetry information for the function - recursive */
extern Extra_SymmInfo_t * Extra_SymmPairsCompute( DdManager * dd, DdNode * bFunc );
/* computes the classical symmetry information for the function - using naive approach */
extern Extra_SymmInfo_t * Extra_SymmPairsComputeNaive( DdManager * dd, DdNode * bFunc );
extern int Extra_bddCheckVarsSymmetricNaive( DdManager * dd, DdNode * bF, int iVar1, int iVar2 );
/* allocates the data structure */
extern Extra_SymmInfo_t * Extra_SymmPairsAllocate( int nVars );
/* deallocates the data structure */
extern void Extra_SymmPairsDissolve( Extra_SymmInfo_t * );
/* print the contents the data structure */
extern void Extra_SymmPairsPrint( Extra_SymmInfo_t * );
/* converts the ZDD into the Extra_SymmInfo_t structure */
extern Extra_SymmInfo_t * Extra_SymmPairsCreateFromZdd( DdManager * dd, DdNode * zPairs, DdNode * bVars );
/* computes the classical symmetry information as a ZDD */
extern DdNode * Extra_zddSymmPairsCompute( DdManager * dd, DdNode * bF, DdNode * bVars );
extern DdNode * extraZddSymmPairsCompute( DdManager * dd, DdNode * bF, DdNode * bVars );
/* returns a singleton-set ZDD containing all variables that are symmetric with the given one */
extern DdNode * Extra_zddGetSymmetricVars( DdManager * dd, DdNode * bF, DdNode * bG, DdNode * bVars );
extern DdNode * extraZddGetSymmetricVars( DdManager * dd, DdNode * bF, DdNode * bG, DdNode * bVars );
/* converts a set of variables into a set of singleton subsets */
extern DdNode * Extra_zddGetSingletons( DdManager * dd, DdNode * bVars );
extern DdNode * extraZddGetSingletons( DdManager * dd, DdNode * bVars );
/* filters the set of variables using the support of the function */
extern DdNode * Extra_bddReduceVarSet( DdManager * dd, DdNode * bVars, DdNode * bF );
extern DdNode * extraBddReduceVarSet( DdManager * dd, DdNode * bVars, DdNode * bF );
/* checks the possibility that the two vars are symmetric */
extern int Extra_bddCheckVarsSymmetric( DdManager * dd, DdNode * bF, int iVar1, int iVar2 );
extern DdNode * extraBddCheckVarsSymmetric( DdManager * dd, DdNode * bF, DdNode * bVars );
/* build the set of all tuples of K variables out of N from the BDD cube */
extern DdNode * Extra_zddTuplesFromBdd( DdManager * dd, int K, DdNode * bVarsN );
extern DdNode * extraZddTuplesFromBdd( DdManager * dd, DdNode * bVarsK, DdNode * bVarsN );
/* selects one subset from a ZDD representing the set of subsets */
extern DdNode * Extra_zddSelectOneSubset( DdManager * dd, DdNode * zS );
extern DdNode * extraZddSelectOneSubset( DdManager * dd, DdNode * zS );
/*=== extraUtilBitMatrix.c ================================================================*/
typedef struct Extra_BitMat_t_ Extra_BitMat_t;

View File

@ -1,6 +1,6 @@
/**CFile****************************************************************
FileName [extraUtilBdd.c]
FileName [extraBddMisc.c]
SystemName [ABC: Logic synthesis and verification system.]
@ -14,7 +14,7 @@
Date [Ver. 1.0. Started - June 20, 2005.]
Revision [$Id: extraUtilBdd.c,v 1.0 2003/09/01 00:00:00 alanmi Exp $]
Revision [$Id: extraBddMisc.c,v 1.0 2003/09/01 00:00:00 alanmi Exp $]
***********************************************************************/

File diff suppressed because it is too large Load Diff

View File

@ -321,6 +321,7 @@ void * Extra_FileReaderGetTokens_int( Extra_FileReader_t * p )
// through EXTRA_OFFSET_SIZE chars till the end of the buffer
if ( p->pBufferStop == p->pBufferEnd ) // end of file
{
*pChar = 0;
p->fStop = 1;
return p->vTokens;
}

View File

@ -1,4 +1,5 @@
SRC += src/misc/extra/extraUtilBdd.c \
SRC += src/misc/extra/extraBddMisc.c \
src/misc/extra/extraBddSymm.c \
src/misc/extra/extraUtilBitMatrix.c \
src/misc/extra/extraUtilCanon.c \
src/misc/extra/extraUtilFile.c \

View File

@ -52,7 +52,7 @@ struct Vec_Vec_t_
#define Vec_VecForEachLevel( vGlob, vVec, i ) \
for ( i = 0; (i < Vec_VecSize(vGlob)) && (((vVec) = Vec_VecEntry(vGlob, i)), 1); i++ )
#define Vec_VecForEachLevelStart( vGlob, vVec, i, LevelStart ) \
for ( i = LevelStart; (i < Vec_PtrSize(vGlob)) && (((vVec) = Vec_VecEntry(vGlob, i)), 1); i++ )
for ( i = LevelStart; (i < Vec_VecSize(vGlob)) && (((vVec) = Vec_VecEntry(vGlob, i)), 1); i++ )
#define Vec_VecForEachLevelStartStop( vGlob, vVec, i, LevelStart, LevelStop ) \
for ( i = LevelStart; (i <= LevelStop) && (((vVec) = Vec_VecEntry(vGlob, i)), 1); i++ )
#define Vec_VecForEachLevelReverse( vGlob, vVec, i ) \
@ -234,6 +234,25 @@ static inline void Vec_VecPush( Vec_Vec_t * p, int Level, void * Entry )
Vec_PtrPush( p->pArray[Level], Entry );
}
/**Function*************************************************************
Synopsis []
Description []
SideEffects []
SeeAlso []
***********************************************************************/
static inline void Vec_VecPushUnique( Vec_Vec_t * p, int Level, void * Entry )
{
if ( p->nSize < Level + 1 )
Vec_VecPush( p, Level, Entry );
else
Vec_PtrPushUnique( p->pArray[Level], Entry );
}
////////////////////////////////////////////////////////////////////////
/// END OF FILE ///
////////////////////////////////////////////////////////////////////////