Version abc60611

Makefile

@@ -9,14 +9,15 @@ PROG := abc
 MODULES := src/base/abc src/base/abci src/base/seq src/base/cmd src/base/io src/base/main \
            src/bdd/cudd src/bdd/dsd src/bdd/epd src/bdd/mtr src/bdd/parse src/bdd/reo \
            src/map/fpga src/map/pga src/map/mapper src/map/mio src/map/super \
-           src/misc/extra src/misc/mvc src/misc/st src/misc/util src/misc/espresso src/misc/vec \
+           src/misc/extra src/misc/mvc src/misc/st src/misc/util src/misc/espresso src/misc/nm src/misc/vec \
 	   src/opt/cut src/opt/dec src/opt/fxu src/opt/rwr src/opt/sim \
+	   src/temp/esop src/temp/ivy src/temp/player \
            src/sat/asat src/sat/csat src/sat/msat src/sat/fraig
 
 default: $(PROG)
 
-OPTFLAGS  := -DNDEBUG -O3
-#OPTFLAGS  := -g -O
+#OPTFLAGS  := -DNDEBUG -O3
+OPTFLAGS  := -g -O
 
 CFLAGS   += -Wall -Wno-unused-function $(OPTFLAGS) $(patsubst %, -I%, $(MODULES)) 
 CXXFLAGS += $(CFLAGS) 

abc.dsp

@@ -42,7 +42,7 @@ RSC=rc.exe
 # PROP Ignore_Export_Lib 0
 # PROP Target_Dir ""
 # ADD BASE CPP /nologo /W3 /GX /O2 /D "WIN32" /D "NDEBUG" /D "_CONSOLE" /D "_MBCS" /YX /FD /c
-# ADD CPP /nologo /W3 /GX /O2 /I "src\base\abc" /I "src\base\abci" /I "src\base\abcs" /I "src\base\seq" /I "src\base\cmd" /I "src\base\io" /I "src\base\main" /I "src\bdd\cudd" /I "src\bdd\epd" /I "src\bdd\mtr" /I "src\bdd\parse" /I "src\bdd\dsd" /I "src\bdd\reo" /I "src\sop\ft" /I "src\sat\aig" /I "src\sat\asat" /I "src\sat\msat" /I "src\sat\fraig" /I "src\opt\cut" /I "src\opt\dec" /I "src\opt\fxu" /I "src\opt\sim" /I "src\opt\rwr" /I "src\map\fpga" /I "src\map\pga" /I "src\map\mapper" /I "src\map\mio" /I "src\map\super" /I "src\misc\extra" /I "src\misc\st" /I "src\misc\mvc" /I "src\misc\util" /I "src\misc\npn" /I "src\misc\vec" /I "src\misc\espresso" /I "src\misc\nm" /D "WIN32" /D "NDEBUG" /D "_CONSOLE" /D "_MBCS" /D "__STDC__" /FR /YX /FD /c
+# ADD CPP /nologo /W3 /GX /O2 /I "src\base\abc" /I "src\base\abci" /I "src\base\abcs" /I "src\base\seq" /I "src\base\cmd" /I "src\base\io" /I "src\base\main" /I "src\bdd\cudd" /I "src\bdd\epd" /I "src\bdd\mtr" /I "src\bdd\parse" /I "src\bdd\dsd" /I "src\bdd\reo" /I "src\sop\ft" /I "src\sat\aig" /I "src\sat\asat" /I "src\sat\msat" /I "src\sat\fraig" /I "src\opt\cut" /I "src\opt\dec" /I "src\opt\fxu" /I "src\opt\sim" /I "src\opt\rwr" /I "src\map\fpga" /I "src\map\pga" /I "src\map\mapper" /I "src\map\mio" /I "src\map\super" /I "src\misc\extra" /I "src\misc\st" /I "src\misc\mvc" /I "src\misc\util" /I "src\misc\npn" /I "src\misc\vec" /I "src\misc\espresso" /I "src\misc\nm" /I "src\temp\ivy" /I "src\temp\esop" /D "WIN32" /D "NDEBUG" /D "_CONSOLE" /D "_MBCS" /D "__STDC__" /FR /YX /FD /c
 # ADD BASE RSC /l 0x409 /d "NDEBUG"
 # ADD RSC /l 0x409 /d "NDEBUG"
 BSC32=bscmake.exe
@@ -66,7 +66,7 @@ LINK32=link.exe
 # PROP Ignore_Export_Lib 0
 # PROP Target_Dir ""
 # ADD BASE CPP /nologo /W3 /Gm /GX /ZI /Od /D "WIN32" /D "_DEBUG" /D "_CONSOLE" /D "_MBCS" /YX /FD /GZ /c
-# ADD CPP /nologo /W3 /Gm /GX /ZI /Od /I "src\base\abc" /I "src\base\abci" /I "src\base\abcs" /I "src\base\seq" /I "src\base\cmd" /I "src\base\io" /I "src\base\main" /I "src\bdd\cudd" /I "src\bdd\epd" /I "src\bdd\mtr" /I "src\bdd\parse" /I "src\bdd\dsd" /I "src\bdd\reo" /I "src\sop\ft" /I "src\sat\aig" /I "src\sat\asat" /I "src\sat\msat" /I "src\sat\fraig" /I "src\opt\cut" /I "src\opt\dec" /I "src\opt\fxu" /I "src\opt\sim" /I "src\opt\rwr" /I "src\map\fpga" /I "src\map\pga" /I "src\map\mapper" /I "src\map\mio" /I "src\map\super" /I "src\misc\extra" /I "src\misc\st" /I "src\misc\mvc" /I "src\misc\util" /I "src\misc\npn" /I "src\misc\vec" /I "src\misc\espresso" /I "src\misc\nm" /D "WIN32" /D "_DEBUG" /D "_CONSOLE" /D "_MBCS" /D "__STDC__" /FR /YX /FD /GZ /c
+# ADD CPP /nologo /W3 /Gm /GX /ZI /Od /I "src\base\abc" /I "src\base\abci" /I "src\base\abcs" /I "src\base\seq" /I "src\base\cmd" /I "src\base\io" /I "src\base\main" /I "src\bdd\cudd" /I "src\bdd\epd" /I "src\bdd\mtr" /I "src\bdd\parse" /I "src\bdd\dsd" /I "src\bdd\reo" /I "src\sop\ft" /I "src\sat\aig" /I "src\sat\asat" /I "src\sat\msat" /I "src\sat\fraig" /I "src\opt\cut" /I "src\opt\dec" /I "src\opt\fxu" /I "src\opt\sim" /I "src\opt\rwr" /I "src\map\fpga" /I "src\map\pga" /I "src\map\mapper" /I "src\map\mio" /I "src\map\super" /I "src\misc\extra" /I "src\misc\st" /I "src\misc\mvc" /I "src\misc\util" /I "src\misc\npn" /I "src\misc\vec" /I "src\misc\espresso" /I "src\misc\nm" /I "src\temp\ivy" /I "src\temp\esop" /D "WIN32" /D "_DEBUG" /D "_CONSOLE" /D "_MBCS" /D "__STDC__" /FR /YX /FD /GZ /c
 # SUBTRACT CPP /X
 # ADD BASE RSC /l 0x409 /d "_DEBUG"
 # ADD RSC /l 0x409 /d "_DEBUG"
@@ -218,6 +218,10 @@ SOURCE=.\src\base\abci\abcGen.c
 # End Source File
 # Begin Source File
 
+SOURCE=.\src\base\abci\abcIvy.c
+# End Source File
+# Begin Source File
+
 SOURCE=.\src\base\abci\abcMap.c
 # End Source File
 # Begin Source File
@@ -226,6 +230,10 @@ SOURCE=.\src\base\abci\abcMiter.c
 # End Source File
 # Begin Source File
 
+SOURCE=.\src\base\abci\abcMv.c
+# End Source File
+# Begin Source File
+
 SOURCE=.\src\base\abci\abcNtbdd.c
 # End Source File
 # Begin Source File
@@ -1286,6 +1294,10 @@ SOURCE=.\src\opt\rwr\rwrPrint.c
 # End Source File
 # Begin Source File
 
+SOURCE=.\src\opt\rwr\rwrTemp.c
+# End Source File
+# Begin Source File
+
 SOURCE=.\src\opt\rwr\rwrUtil.c
 # End Source File
 # End Group
@@ -1421,50 +1433,6 @@ SOURCE=.\src\opt\sim\simSymStr.c
 SOURCE=.\src\opt\sim\simUtils.c
 # End Source File
 # End Group
-# Begin Group "xyz"
-
-# PROP Default_Filter ""
-# Begin Source File
-
-SOURCE=.\src\opt\xyz\xyz.h
-# End Source File
-# Begin Source File
-
-SOURCE=.\src\opt\xyz\xyzBuild.c
-# End Source File
-# Begin Source File
-
-SOURCE=.\src\opt\xyz\xyzCore.c
-# End Source File
-# Begin Source File
-
-SOURCE=.\src\opt\xyz\xyzInt.h
-# End Source File
-# Begin Source File
-
-SOURCE=.\src\opt\xyz\xyzMan.c
-# End Source File
-# Begin Source File
-
-SOURCE=.\src\opt\xyz\xyzMinEsop.c
-# End Source File
-# Begin Source File
-
-SOURCE=.\src\opt\xyz\xyzMinMan.c
-# End Source File
-# Begin Source File
-
-SOURCE=.\src\opt\xyz\xyzMinSop.c
-# End Source File
-# Begin Source File
-
-SOURCE=.\src\opt\xyz\xyzMinUtil.c
-# End Source File
-# Begin Source File
-
-SOURCE=.\src\opt\xyz\xyzTest.c
-# End Source File
-# End Group
 # End Group
 # Begin Group "map"
 
@@ -2098,6 +2066,174 @@ SOURCE=.\src\misc\nm\nmTable.c
 # End Source File
 # End Group
 # End Group
+# Begin Group "temp"
+
+# PROP Default_Filter ""
+# Begin Group "ivy"
+
+# PROP Default_Filter ""
+# Begin Source File
+
+SOURCE=.\src\temp\ivy\ivy.h
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\temp\ivy\ivyBalance.c
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\temp\ivy\ivyCanon.c
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\temp\ivy\ivyCheck.c
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\temp\ivy\ivyCut.c
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\temp\ivy\ivyDfs.c
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\temp\ivy\ivyDsd.c
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\temp\ivy\ivyMan.c
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\temp\ivy\ivyMulti.c
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\temp\ivy\ivyObj.c
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\temp\ivy\ivyOper.c
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\temp\ivy\ivyRewrite.c
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\temp\ivy\ivySeq.c
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\temp\ivy\ivyTable.c
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\temp\ivy\ivyUndo.c
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\temp\ivy\ivyUtil.c
+# End Source File
+# End Group
+# Begin Group "player"
+
+# PROP Default_Filter ""
+# Begin Source File
+
+SOURCE=.\src\temp\player\player.h
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\temp\player\playerAbc.c
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\temp\player\playerBuild.c
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\temp\player\playerCore.c
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\temp\player\playerMan.c
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\temp\player\playerUtil.c
+# End Source File
+# End Group
+# Begin Group "esop"
+
+# PROP Default_Filter ""
+# Begin Source File
+
+SOURCE=.\src\temp\esop\esop.h
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\temp\esop\esopMan.c
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\temp\esop\esopMem.c
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\temp\esop\esopMin.c
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\temp\esop\esopUtil.c
+# End Source File
+# End Group
+# Begin Group "xyz"
+
+# PROP Default_Filter ""
+# Begin Source File
+
+SOURCE=.\src\temp\xyz\xyz.h
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\temp\xyz\xyzBuild.c
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\temp\xyz\xyzCore.c
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\temp\xyz\xyzInt.h
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\temp\xyz\xyzMan.c
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\temp\xyz\xyzMinEsop.c
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\temp\xyz\xyzMinMan.c
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\temp\xyz\xyzMinSop.c
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\temp\xyz\xyzMinUtil.c
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\temp\xyz\xyzTest.c
+# End Source File
+# End Group
+# End Group
 # End Group
 # Begin Group "Header Files"
 

abc.rc

@@ -80,6 +80,7 @@ alias sharem      "b; ren -m; fx; b"
 alias sharedsd    "b; ren; dsd -g; sw; fx; b"
 alias resyn       "b; rw; rwz; b; rwz; b"
 alias resyn2      "b; rw; rf; b; rw; rwz; b; rfz; rwz; b"
+alias resyn2a     "b; rw; b; rw; rwz; b; rwz; b"
 alias resyn3      "b; rs; rs -K 6; b; rsz; rsz -K 6; b; rsz -K 5; b"
 alias compress    "b -l; rw -l; rwz -l; b -l; rwz -l; b -l"
 alias compress2   "b -l; rw -l; rf -l; b -l; rw -l; rwz -l; b -l; rfz -l; rwz -l; b -l"

examples/s444.blif

+.model s444
+.inputs G0 G1 G2
+.outputs G118 G167 G107 G119 G168 G108
+
+.latch     G11_in        G11  0
+.latch     G12_in        G12  0
+.latch     G13_in        G13  0
+.latch     G14_in        G14  0
+.latch     G15_in        G15  0
+.latch     G16_in        G16  0
+.latch     G17_in        G17  0
+.latch     G18_in        G18  0
+.latch     G19_in        G19  0
+.latch     G20_in        G20  0
+.latch     G21_in        G21  0
+.latch     G22_in        G22  0
+.latch     G23_in        G23  0
+.latch     G24_in        G24  0
+.latch     G25_in        G25  0
+.latch     G26_in        G26  0
+.latch     G27_in        G27  0
+.latch     G28_in        G28  0
+.latch     G29_in        G29  0
+.latch     G30_in        G30  0
+.latch     G31_in        G31  0
+
+.names G12 G13 [25]
+00 1
+.names G11 [25] [26]
+01 1
+.names G14 [26] [27]
+10 1
+.names G0 G11 [28]
+00 1
+.names [27] [28] G11_in
+01 1
+.names G11 G12 [30]
+11 1
+.names G12 [30] [31]
+10 1
+.names G11 [30] [32]
+10 1
+.names [31] [32] [33]
+00 1
+.names G0 [33] [34]
+00 1
+.names [27] [34] G12_in
+01 1
+.names G13 [30] [36]
+11 1
+.names G13 [36] [37]
+10 1
+.names [30] [36] [38]
+10 1
+.names [37] [38] [39]
+00 1
+.names G0 [39] [40]
+00 1
+.names [27] [40] G13_in
+01 1
+.names G12 G13 [42]
+11 1
+.names G11 [42] [43]
+11 1
+.names G14 [43] [44]
+11 1
+.names G14 [44] [45]
+10 1
+.names [43] [44] [46]
+10 1
+.names [45] [46] [47]
+00 1
+.names G0 [47] [48]
+00 1
+.names [27] [48] G14_in
+01 1
+.names G31 [27] [50]
+00 1
+.names G16 G17 [51]
+00 1
+.names G15 [51] [52]
+01 1
+.names [50] [52] [53]
+00 1
+.names G18 [53] [54]
+11 1
+.names G15 [50] [55]
+10 1
+.names G15 [55] [56]
+10 1
+.names [50] [55] [57]
+00 1
+.names [56] [57] [58]
+00 1
+.names G0 [58] [59]
+00 1
+.names [54] [59] G15_in
+01 1
+.names G16 [55] [61]
+11 1
+.names G16 [61] [62]
+10 1
+.names [55] [61] [63]
+10 1
+.names [62] [63] [64]
+00 1
+.names G0 [64] [65]
+00 1
+.names [54] [65] G16_in
+01 1
+.names G16 [50] [67]
+10 1
+.names G15 [67] [68]
+11 1
+.names G17 [68] [69]
+11 1
+.names G17 [69] [70]
+10 1
+.names [68] [69] [71]
+10 1
+.names [70] [71] [72]
+00 1
+.names G0 [72] [73]
+00 1
+.names [54] [73] G17_in
+01 1
+.names G15 G16 [75]
+11 1
+.names G17 [50] [76]
+10 1
+.names [75] [76] [77]
+11 1
+.names G18 [77] [78]
+11 1
+.names G18 [78] [79]
+10 1
+.names [77] [78] [80]
+10 1
+.names [79] [80] [81]
+00 1
+.names G0 [81] [82]
+00 1
+.names [54] [82] G18_in
+01 1
+.names G20 G21 [84]
+00 1
+.names G19 [84] [85]
+01 1
+.names [54] [85] [86]
+10 1
+.names G22 [86] [87]
+11 1
+.names G19 [54] [88]
+11 1
+.names G19 [88] [89]
+10 1
+.names [54] [88] [90]
+10 1
+.names [89] [90] [91]
+00 1
+.names G0 [91] [92]
+00 1
+.names [87] [92] G19_in
+01 1
+.names G20 [88] [94]
+11 1
+.names G20 [94] [95]
+10 1
+.names [88] [94] [96]
+10 1
+.names [95] [96] [97]
+00 1
+.names G0 [97] [98]
+00 1
+.names [87] [98] G20_in
+01 1
+.names G20 [54] [100]
+11 1
+.names G19 [100] [101]
+11 1
+.names G21 [101] [102]
+11 1
+.names G21 [102] [103]
+10 1
+.names [101] [102] [104]
+10 1
+.names [103] [104] [105]
+00 1
+.names G0 [105] [106]
+00 1
+.names [87] [106] G21_in
+01 1
+.names G19 G20 [108]
+11 1
+.names G21 [54] [109]
+11 1
+.names [108] [109] [110]
+11 1
+.names G22 [110] [111]
+11 1
+.names G22 [111] [112]
+10 1
+.names [110] [111] [113]
+10 1
+.names [112] [113] [114]
+00 1
+.names G0 [114] [115]
+00 1
+.names [87] [115] G22_in
+01 1
+.names G2 G23 [117]
+00 1
+.names G2 G23 [118]
+11 1
+.names [117] [118] [119]
+00 1
+.names G0 [119] G23_in
+01 1
+.names G20 G21 [121]
+01 1
+.names G0 G23 [122]
+01 1
+.names [121] [122] [123]
+11 1
+.names G19 [123] [124]
+01 1
+.names G21 G22 [126]
+10 1
+.names G19 G20 [125]
+10 1
+.names G23 [125] [127]
+01 1
+.names [126] [127] [128]
+11 1
+.names G0 G24 [129]
+01 1
+.names [128] [129] [130]
+01 1
+.names [124] [130] [131]
+00 1
+.names G22 G23 [132]
+00 1
+.names [125] [132] [133]
+11 1
+.names G24 [133] [134]
+10 1
+.names G19 G20 [135]
+00 1
+.names G23 [135] [136]
+11 1
+.names G22 G23 [137]
+11 1
+.names [136] [137] [138]
+00 1
+.names G0 G21 [139]
+01 1
+.names [138] [139] [140]
+11 1
+.names [134] [140] G25_in
+01 1
+.names G19 G22 [142]
+01 1
+.names G0 [142] [143]
+01 1
+.names G0 [108] [144]
+01 1
+.names [143] [144] [145]
+00 1
+.names [129] [139] [146]
+00 1
+.names [145] [146] G26_in
+11 1
+.names G21 G24 [148]
+00 1
+.names [125] [148] [149]
+11 1
+.names G21 G22 [150]
+00 1
+.names G24 [150] [151]
+01 1
+.names G0 [151] [152]
+00 1
+.names [149] [152] [153]
+01 1
+.names G0 G22 [154]
+01 1
+.names [135] [154] [155]
+11 1
+.names [146] [155] [156]
+10 1
+.names [131] [156] [157]
+00 1
+.names G17 [157] [158]
+01 1
+.names [131] [156] [159]
+10 1
+.names [158] [159] G28_in
+00 1
+.names [122] [126] [161]
+11 1
+.names G21 G22 [162]
+01 1
+.names G0 [162] [163]
+01 1
+.names [161] [163] [164]
+00 1
+.names G20 [164] [165]
+00 1
+.names G19 [165] [166]
+01 1
+.names [130] [166] [167]
+00 1
+.names [131] [167] [168]
+00 1
+.names G17 [168] [169]
+01 1
+.names [131] [167] [170]
+10 1
+.names [169] [170] G29_in
+00 1
+.names G20 G21 [172]
+10 1
+.names G0 G24 [173]
+00 1
+.names [172] [173] [174]
+11 1
+.names G19 [174] G30_in
+11 1
+.names G1 G31 [176]
+00 1
+.names G1 G31 [177]
+11 1
+.names [176] [177] [178]
+00 1
+.names G0 [178] G31_in
+01 1
+.names [131] G24_in
+0 1
+.names [153] G27_in
+0 1
+.names G27 G118
+1 1
+.names G29 G167
+0 1
+.names G25 G107
+1 1
+.names G28 G119
+0 1
+.names G30 G168
+1 1
+.names G26 G108
+1 1
+.end

readme

@@ -4,15 +4,20 @@ The following steps may be needed to compile it on UNIX:
 >> dos2unix Makefile Makefile
 >> dos2unix depends.sh depends.sh
 >> chmod 755 depends.sh
->> make 
+>> make  // on Solaris, try "gmake"
 
 If compiling as a static library, it is necessary to uncomment
 #define _LIB in "src/abc/main/main.c"
 
-
 Several things to try if it does not compile on your platform:
-- Try running all code through dos2unix (Solaris)
-- Try removing flags from the libs line (LIBS :=) in Makefile (Mac)
+- Try running all code (not only Makefile and depends.sh) through dos2unix
+- Try the following actions:
+  (a) Remove flags from the libs line (LIBS :=) in Makefile
+  (b) Remove "src\base\main\libSupport.c" from "src\base\main\module.make"
+  (c) Comment calls to Libs_Init() and Libs_End() in "src\base\main\mainInit.c"
+- Try linking with gcc (rather than g++)
+  For this replace "LD   := g++" with "LD   := gcc -lm" in Makefile
+
 
 Finally, run regression test:
 abc>>> so regtest.script

regtest_output2.txt

+UC Berkeley, ABC 1.01 (compiled May  9 2006 09:22:13)
+abc 02> so regtest.script
+abc - > r examples/apex4.pla;    resyn; sharem; fpga; cec; ps;  clp; share; resyn; map; cec; ps
+Networks are equivalent.
+examples/apex4: i/o =    9/  19  lat =    0  nd =  1183  cube =  2195  lev =   7
+The shared BDD size is 900 nodes.
+A simple supergate library is derived from gate library "mcnc_temp.genlib".
+Loaded 20 unique 5-input supergates from "mcnc_temp.super".  Time =   0.03 sec
+Networks are equivalent.
+examples/apex4: i/o =    9/  19  lat =    0  nd =  1789  area = 4554.00  delay = 11.50  lev =  11
+abc - > r examples/C2670.blif;   resyn; fpga; cec; ps;          u; map; cec; ps
+Networks are equivalent.
+C2670.iscas  : i/o =  233/ 140  lat =    0  nd =   218  cube =   444  lev =   7
+Networks are equivalent.
+C2670.iscas  : i/o =  233/ 140  lat =    0  nd =   471  area = 1166.00  delay = 15.50  lev =  14
+abc - > r examples/frg2.blif;    dsd; muxes; cec; clp; share; resyn; map; cec; ps
+Networks are equivalent.
+The shared BDD size is 1111 nodes.
+Networks are equivalent.
+frg2         : i/o =  143/ 139  lat =    0  nd =   540  area = 1373.00  delay =  9.70  lev =   9
+abc - > r examples/pj1.blif;     resyn; fpga; cec; ps;          u; map; cec; ps
+Networks are equivalent.
+exCombCkt    : i/o = 1769/1063  lat =    0  nd =  5582  cube = 10389  lev =  15
+Networks are equivalent.
+exCombCkt    : i/o = 1769/1063  lat =    0  nd = 10291  area = 24781.00  delay = 29.80  lev =  27
+abc - > r examples/s38584.bench; resyn; fpga; cec; ps;          u; map; cec; ps
+Networks are equivalent.
+examples/s38584: i/o =   12/ 278  lat = 1452  nd =  4404  cube =  7515  lev =   9
+Networks are equivalent.
+examples/s38584: i/o =   12/ 278  lat = 1452  nd =  8506  area = 19313.00  delay = 20.60  lev =  17
+abc - > r examples/ac.v;         resyn; fpga; cec; ps;          u; map; cec; ps
+Networks are equivalent.
+ac97_ctrl    : i/o =   84/  48  lat = 2199  nd =  4082  cube =  7776  lev =   4
+Networks are equivalent.
+ac97_ctrl    : i/o =   84/  48  lat = 2199  nd =  8274  area = 19707.00  delay =  8.10  lev =   8
+abc - > r examples/s444.blif;    b; esd -v; dsd; cec; ps
+The shared BDD size is 181 nodes.
+BDD nodes in the transition relation before reordering 557.
+BDD nodes in the transition relation after reordering 456.
+Reachability analysis completed in 151 iterations.
+The number of minterms in the reachable state set = 8865.
+BDD nodes in the unreachable states before reordering 124.
+BDD nodes in the unreachable states after reordering 113.
+Networks are equivalent.
+s444         : i/o =    3/   6  lat =   21  nd =    81  cube =   119  lev =   7
+abc - > r examples/i10.blif;     fpga; cec; ps;                 u; map; cec; ps
+The network was strashed and balanced before FPGA mapping.
+Networks are equivalent.
+i10          : i/o =  257/ 224  lat =    0  nd =   890  cube =  1593  lev =  13
+The network was strashed and balanced before mapping.
+Networks are equivalent.
+i10          : i/o =  257/ 224  lat =    0  nd =  1700  area = 4245.00  delay = 30.80  lev =  28
+abc - > r examples/i10.blif;     choice; fpga; cec; ps;         u; map; cec; ps
+Currently stored 3 networks with 5794 nodes will be fraiged.
+Total fraiging time =   0.74 sec
+Performing FPGA mapping with choices.
+Networks are equivalent.
+i10          : i/o =  257/ 224  lat =    0  nd =   799  cube =  1484  lev =  12
+Performing mapping with choices.
+Networks are equivalent.
+i10          : i/o =  257/ 224  lat =    0  nd =  1485  area = 3528.00  delay = 25.40  lev =  23
+abc - > r examples/s6669.blif;   fpga; ps; sec; u;   sfpga; ps; sec; u;   fpga; ret; ps; sec
+The network was strashed and balanced before FPGA mapping.
+s6669        : i/o =   83/  55  lat =  239  nd =   679  bdd  =  3060  lev =  20
+Networks are equivalent after fraiging.
+The network was strashed and balanced before FPGA mapping/retiming.
+The number of LUTs with incompatible edges = 25.
+The number of LUTs with more than 4 inputs = 18.
+s6669        : i/o =   83/  55  lat =  404  nd =   829  bdd  =  3867  lev =   6
+Networks are equivalent after fraiging.
+The network was strashed and balanced before FPGA mapping.
+s6669        : i/o =   83/  55  lat =  347  nd =   773  bdd  =  3262  lev =   9
+Networks are equivalent after fraiging.
+abc - > r examples/s5378.blif;   map -s; ps; sec; u; smap; ps; sec; u;    map; ret; ps; sec
+The network was strashed and balanced before mapping.
+s5378        : i/o =   35/  49  lat =  164  nd =  1009  area = 2352.00  delay = 12.40  lev =  11
+Networks are equivalent after fraiging.
+The number of nodes with equal fanins = 5.
+The network was strashed and balanced before SC mapping/retiming.
+The mininum clock period computed is 10.00.
+The resulting network is derived as BDD logic network (this is temporary).
+s5378        : i/o =   35/  49  lat =  399  nd =  1230  bdd  =  4548  lev =   7
+Networks are equivalent after fraiging.
+The network was strashed and balanced before mapping.
+s5378        : i/o =   35/  49  lat =  359  nd =  1083  area = 2426.00  delay = 13.00  lev =  11
+Networks are equivalent after fraiging.
+abc - > time
+elapse: 188.97 seconds, total: 188.97 seconds
+abc 123>
+
+
+
+
+
+
+
+

src/base/abc/abcCheck.c

@@ -92,7 +92,8 @@ bool Abc_NtkDoCheck( Abc_Ntk_t * pNtk )
     Abc_Obj_t * pObj, * pNet, * pNode;
     int i;
 
-    if ( !Abc_NtkIsNetlist(pNtk) && !Abc_NtkIsLogic(pNtk) && !Abc_NtkIsStrash(pNtk) && !Abc_NtkIsSeq(pNtk) && !Abc_NtkIsBlackbox(pNtk) )
+    // check network types
+    if ( !Abc_NtkIsNetlist(pNtk) && !Abc_NtkIsLogic(pNtk) && !Abc_NtkIsStrash(pNtk) && !Abc_NtkIsSeq(pNtk) )
     {
         fprintf( stdout, "NetworkCheck: Unknown network type.\n" );
         return 0;
@@ -111,6 +112,22 @@ bool Abc_NtkDoCheck( Abc_Ntk_t * pNtk )
         }
     }
 
+    // check CI/CO numbers
+    if ( Abc_NtkPiNum(pNtk) + Abc_NtkLatchNum(pNtk) != Abc_NtkCiNum(pNtk) )
+    {
+        fprintf( stdout, "NetworkCheck: Number of CIs does not match number of PIs and latches.\n" );
+        fprintf( stdout, "One possible reason is that latches are added twice:\n" );
+        fprintf( stdout, "in procedure Abc_ObjAdd() and in the user's code.\n" );
+        return 0;
+    }
+    if ( Abc_NtkPoNum(pNtk) + Abc_NtkAssertNum(pNtk) + Abc_NtkLatchNum(pNtk) != Abc_NtkCoNum(pNtk) )
+    {
+        fprintf( stdout, "NetworkCheck: Number of COs does not match number of POs, asserts, and latches.\n" );
+        fprintf( stdout, "One possible reason is that latches are added twice:\n" );
+        fprintf( stdout, "in procedure Abc_ObjAdd() and in the user's code.\n" );
+        return 0;
+    }
+
     // check the names
     if ( !Abc_NtkCheckNames( pNtk ) )
         return 0;
@@ -181,14 +198,7 @@ bool Abc_NtkDoCheck( Abc_Ntk_t * pNtk )
 
     // check the EXDC network if present
     if ( pNtk->pExdc )
-    {
-//        if ( pNtk->Type != pNtk->pExdc->Type )
-//        {
-//            fprintf( stdout, "NetworkCheck: Network and its EXDC have different types.\n" );
-//            return 0;
-//        }
-        return Abc_NtkCheck( pNtk->pExdc );
-    }
+        Abc_NtkCheck( pNtk->pExdc );
 
     // check the hierarchy
     if ( Abc_NtkIsNetlist(pNtk) && pNtk->tName2Model )
@@ -226,76 +236,60 @@ bool Abc_NtkDoCheck( Abc_Ntk_t * pNtk )
 ***********************************************************************/
 bool Abc_NtkCheckNames( Abc_Ntk_t * pNtk )
 {
-    stmm_generator * gen;
-    Abc_Obj_t * pNet, * pNet2, * pObj;
+    Abc_Obj_t * pObj;
+    Vec_Int_t * vNameIds;
     char * pName;
-    int i;
+    int i, NameId;
 
-    if ( Abc_NtkIsNetlist(pNtk) )
+    // check that each CI/CO has a name
+    Abc_NtkForEachCi( pNtk, pObj, i )
     {
-/*
-        // check that the nets in the table are also in the network
-        stmm_foreach_item( pNtk->tName2Net, gen, &pName, (char**)&pNet )
+        pObj = Abc_ObjFanout0Ntk(pObj);
+        if ( Nm_ManFindNameById(pObj->pNtk->pManName, pObj->Id) == NULL )
         {
-            if ( pNet->pData != pName )
-            {
-                fprintf( stdout, "NetworkCheck: Net \"%s\" has different name compared to the one in the name table.\n", pNet->pData );
-                return 0;
-            }
-        }
-        // check that the nets with names are also in the table
-        Abc_NtkForEachNet( pNtk, pNet, i )
-        {
-            if ( pNet->pData && !stmm_lookup( pNtk->tName2Net, pNet->pData, (char**)&pNet2 ) )
-            {
-                fprintf( stdout, "NetworkCheck: Net \"%s\" is in the network but not in the name table.\n", pNet->pData );
-                return 0;
-            }
+            fprintf( stdout, "NetworkCheck: CI with ID %d is in the network but not in the name table.\n", pObj->Id );
+            return 0;
         }
-*/
     }
-/*
-    // check PI/PO/latch names
-    Abc_NtkForEachPi( pNtk, pObj, i )
+    Abc_NtkForEachCo( pNtk, pObj, i )
     {
-        if ( !stmm_lookup( pNtk->tObj2Name, (char *)pObj, &pName ) )
-        {
-            fprintf( stdout, "NetworkCheck: PI \"%s\" is in the network but not in the name table.\n", Abc_ObjName(pObj) );
-            return 0;
-        }
-        if ( Abc_NtkIsNetlist(pNtk) && strcmp( Abc_ObjName(Abc_ObjFanout0(pObj)), pName ) )
+        if ( Abc_ObjIsLatch(pObj) )
+            continue;
+        pObj = Abc_ObjFanin0Ntk(pObj);
+        if ( Nm_ManFindNameById(pObj->pNtk->pManName, pObj->Id) == NULL )
         {
-            fprintf( stdout, "NetworkCheck: PI \"%s\" has a different name compared to its net.\n", Abc_ObjName(pObj) );
+            fprintf( stdout, "NetworkCheck: CO with ID %d is in the network but not in the name table.\n", pObj->Id );
             return 0;
         }
     }
-    Abc_NtkForEachPo( pNtk, pObj, i )
+
+    if ( Abc_NtkIsNetlist(pNtk) )
     {
-        if ( !stmm_lookup( pNtk->tObj2Name, (char *)pObj, &pName ) )
-        {
-            fprintf( stdout, "NetworkCheck: PO \"%s\" is in the network but not in the name table.\n", Abc_ObjName(pObj) );
-            return 0;
-        }
-        if ( Abc_NtkIsNetlist(pNtk) && strcmp( Abc_ObjName(Abc_ObjFanin0(pObj)), pName ) )
+        Abc_NtkForEachNet( pNtk, pObj, i )
         {
-            fprintf( stdout, "NetworkCheck: PO \"%s\" has a different name compared to its net.\n", Abc_ObjName(pObj) );
-            return 0;
+            pName = Nm_ManFindNameById(pObj->pNtk->pManName, pObj->Id);
+            if ( pObj->pData && strcmp( pName, pObj->pData ) != 0 )
+            {
+                fprintf( stdout, "NetworkCheck: Net \"%s\" has different name in the name table and at the data pointer.\n", pObj->pData );
+                return 0;
+            }
         }
     }
-    Abc_NtkForEachLatch( pNtk, pObj, i )
+
+    // return the array of all IDs, which have names
+    vNameIds = Nm_ManReturnNameIds( pNtk->pManName );
+    // make sure that these IDs correspond to live objects
+    Vec_IntForEachEntry( vNameIds, NameId, i )
     {
-        if ( !stmm_lookup( pNtk->tObj2Name, (char *)pObj, &pName ) )
-        {
-            fprintf( stdout, "NetworkCheck: Latch \"%s\" is in the network but not in the name table.\n", Abc_ObjName(pObj) );
-            return 0;
-        }
-        if ( Abc_NtkIsNetlist(pNtk) && strcmp( Abc_ObjName(Abc_ObjFanout0(pObj)), pName ) )
+        if ( Vec_PtrEntry( pNtk->vObjs, NameId ) == NULL )
         {
-            fprintf( stdout, "NetworkCheck: Latch \"%s\" has a different name compared to its net.\n", Abc_ObjName(pObj) );
+            Vec_IntFree( vNameIds );
+            pName = Nm_ManFindNameById(pObj->pNtk->pManName, NameId);
+            fprintf( stdout, "NetworkCheck: Object with ID %d is deleted but its name \"%s\" remains in the name table.\n", NameId, pName );
             return 0;
         }
     }
-*/
+    Vec_IntFree( vNameIds );
     return 1;
 }
 
@@ -316,12 +310,6 @@ bool Abc_NtkCheckPis( Abc_Ntk_t * pNtk )
     Abc_Obj_t * pObj;
     int i;
 
-    if ( Abc_NtkCiNum(pNtk) != Abc_NtkPiNum(pNtk) + Abc_NtkLatchNum(pNtk) )
-    {
-        fprintf( stdout, "NetworkCheck: Incorrect size of the PI array.\n" );
-        return 0;
-    }
-
     // check that PIs are indeed PIs
     Abc_NtkForEachPi( pNtk, pObj, i )
     {
@@ -370,12 +358,6 @@ bool Abc_NtkCheckPos( Abc_Ntk_t * pNtk )
     Abc_Obj_t * pObj;
     int i;
 
-    if ( Abc_NtkCoNum(pNtk) != Abc_NtkPoNum(pNtk) + Abc_NtkLatchNum(pNtk) )
-    {
-        fprintf( stdout, "NetworkCheck: Incorrect size of the PO array.\n" );
-        return 0;
-    }
-
     // check that POs are indeed POs
     Abc_NtkForEachPo( pNtk, pObj, i )
     {
@@ -582,7 +564,7 @@ bool Abc_NtkCheckNode( Abc_Ntk_t * pNtk, Abc_Obj_t * pNode )
 bool Abc_NtkCheckLatch( Abc_Ntk_t * pNtk, Abc_Obj_t * pLatch )
 {
     int Value = 1;
-    if ( pNtk->vLats->nSize != Abc_NtkLatchNum(pNtk) )
+    if ( pNtk->vLatches->nSize != Abc_NtkLatchNum(pNtk) )
     {
         fprintf( stdout, "NetworkCheck: Incorrect size of the latch array.\n" );
         return 0;
@@ -759,7 +741,7 @@ int Abc_NtkIsAcyclicHierarchy_rec( Abc_Ntk_t * pNtk )
         return 1;
     pNtk->fHieVisited = 1;
     // return if black box
-    if ( Abc_NtkIsBlackbox(pNtk) )
+    if ( Abc_NtkHasBlackbox(pNtk) )
         return 1;
     assert( Abc_NtkIsNetlist(pNtk) );
     // go through all the children networks

src/base/abc/abcDfs.c

@@ -579,7 +579,7 @@ bool Abc_NtkIsAcyclic_rec( Abc_Obj_t * pNode )
     Abc_Obj_t * pFanin;
     int fAcyclic, i;
     assert( !Abc_ObjIsNet(pNode) );
-    if ( Abc_ObjIsCi(pNode) )
+    if ( Abc_ObjIsCi(pNode) || Abc_ObjIsBox(pNode) )
         return 1;
     assert( Abc_ObjIsNode( pNode ) || Abc_ObjIsBox( pNode ) );
     // make sure the node is not visited
@@ -607,7 +607,7 @@ bool Abc_NtkIsAcyclic_rec( Abc_Obj_t * pNode )
         if ( fAcyclic = Abc_NtkIsAcyclic_rec(pFanin) )
             continue;
         // return as soon as the loop is detected
-        fprintf( stdout, " <-- %s", Abc_ObjName(pNode) );
+        fprintf( stdout, " <-- %s", Abc_ObjName(Abc_ObjFanout0(pFanin)) );
         return 0;
     }
     // mark this node as a visited node

src/base/abc/abcFanio.c

@@ -50,7 +50,7 @@ void Abc_ObjAddFanin( Abc_Obj_t * pObj, Abc_Obj_t * pFanin )
     Vec_IntPushMem( pObj->pNtk->pMmStep, &pFaninR->vFanouts, pObj->Id    );
     if ( Abc_ObjIsComplement(pFanin) )
         Abc_ObjSetFaninC( pObj, Abc_ObjFaninNum(pObj)-1 );
-    Abc_HManAddFanin( pObj, pFanin );
+//    Abc_HManAddFanin( pObj, pFanin );
 }
 
 
@@ -179,7 +179,7 @@ void Abc_ObjPatchFanin( Abc_Obj_t * pObj, Abc_Obj_t * pFaninOld, Abc_Obj_t * pFa
 ***********************************************************************/
 void Abc_ObjTransferFanout( Abc_Obj_t * pNodeFrom, Abc_Obj_t * pNodeTo )
 {
-    Vec_Ptr_t * vFanouts = pNodeFrom->pNtk->vPtrTemp;
+    Vec_Ptr_t * vFanouts;
     int nFanoutsOld, i;
     assert( !Abc_ObjIsComplement(pNodeFrom) );
     assert( !Abc_ObjIsComplement(pNodeTo) );
@@ -190,12 +190,14 @@ void Abc_ObjTransferFanout( Abc_Obj_t * pNodeFrom, Abc_Obj_t * pNodeTo )
     assert( Abc_ObjFanoutNum(pNodeFrom) > 0 );
     // get the fanouts of the old node
     nFanoutsOld = Abc_ObjFanoutNum(pNodeTo);
+    vFanouts = Vec_PtrAlloc( nFanoutsOld );
     Abc_NodeCollectFanouts( pNodeFrom, vFanouts );
     // patch the fanin of each of them
     for ( i = 0; i < vFanouts->nSize; i++ )
         Abc_ObjPatchFanin( vFanouts->pArray[i], pNodeFrom, pNodeTo );
     assert( Abc_ObjFanoutNum(pNodeFrom) == 0 );
     assert( Abc_ObjFanoutNum(pNodeTo) == nFanoutsOld + vFanouts->nSize );
+    Vec_PtrFree( vFanouts );
 }
 
 /**Function*************************************************************

src/base/abc/abcLatch.c

@@ -155,9 +155,6 @@ void Abc_NtkLatchPipe( Abc_Ntk_t * pNtk, int nLatches )
             pLatch = Abc_NtkCreateLatch( pNtk );
             Abc_ObjAddFanin( pLatch, pFanin );
             Abc_LatchSetInitDc( pLatch );
-            // add the latch to the CI/CO lists
-            Vec_PtrPush( pNtk->vCis, pLatch );
-            Vec_PtrPush( pNtk->vCos, pLatch );
             // create the name of the new latch
             Abc_NtkLogicStoreName( pLatch, Abc_ObjNameDummy("LL", i*nLatches + k, nDigits) );
         }

src/base/abc/abcMinBase.c

@@ -65,8 +65,8 @@ int Abc_NtkMinimumBase( Abc_Ntk_t * pNtk )
 ***********************************************************************/
 int Abc_NodeMinimumBase( Abc_Obj_t * pNode )
 {
-    Vec_Str_t * vSupport = pNode->pNtk->vStrTemp;
-    Vec_Ptr_t * vFanins = pNode->pNtk->vPtrTemp;
+    Vec_Str_t * vSupport;
+    Vec_Ptr_t * vFanins;
     DdNode * bTemp;
     int i, nVars;
 
@@ -74,11 +74,16 @@ int Abc_NodeMinimumBase( Abc_Obj_t * pNode )
     assert( Abc_ObjIsNode(pNode) );
 
     // compute support
+    vSupport = Vec_StrAlloc( 10 );
     nVars = Abc_NodeSupport( Cudd_Regular(pNode->pData), vSupport, Abc_ObjFaninNum(pNode) );
     if ( nVars == Abc_ObjFaninNum(pNode) )
+    {
+        Vec_StrFree( vSupport );
         return 0;
+    }
 
     // remove unused fanins
+    vFanins = Vec_PtrAlloc( Abc_ObjFaninNum(pNode) );
     Abc_NodeCollectFanins( pNode, vFanins );
     for ( i = 0; i < vFanins->nSize; i++ )
         if ( vSupport->pArray[i] == 0 )
@@ -88,6 +93,8 @@ int Abc_NodeMinimumBase( Abc_Obj_t * pNode )
     // update the function of the node
     pNode->pData = Extra_bddRemapUp( pNode->pNtk->pManFunc, bTemp = pNode->pData );   Cudd_Ref( pNode->pData );
     Cudd_RecursiveDeref( pNode->pNtk->pManFunc, bTemp );
+    Vec_PtrFree( vFanins );
+    Vec_StrFree( vSupport );
     return 1;
 }
 

src/base/abc/abcNames.c

@@ -30,55 +30,6 @@
 
 /**Function*************************************************************
 
-  Synopsis    [Registers the name with the string memory manager.]
-
-  Description [This function should be used to register all names
-  permanentsly stored with the network. The pointer returned by
-  this procedure contains the copy of the name, which should be used
-  in all network manipulation procedures.]
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-char * Abc_NtkRegisterName( Abc_Ntk_t * pNtk, char * pName )
-{
-/*
-    char * pRegName;
-    if ( pName == NULL ) return NULL;
-    pRegName = Extra_MmFlexEntryFetch( pNtk->pMmNames, strlen(pName) + 1 );
-    strcpy( pRegName, pName );
-    return pRegName;
-*/
-    return NULL;
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Registers the name with the string memory manager.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-char * Abc_NtkRegisterNamePlus( Abc_Ntk_t * pNtk, char * pName, char * pSuffix )
-{
-/*
-    char * pRegName;
-    assert( pName && pSuffix );
-    pRegName = Extra_MmFlexEntryFetch( pNtk->pMmNames, strlen(pName) + strlen(pSuffix) + 1 );
-    sprintf( pRegName, "%s%s", pName, pSuffix );
-    return pRegName;
-*/
-    return NULL;
-}
-
-/**Function*************************************************************
-
   Synopsis    [Gets the long name of the object.]
 
   Description [The temporary name is stored in a static buffer inside this
@@ -176,20 +127,7 @@ char * Abc_ObjNameDummy( char * pPrefix, int Num, int nDigits )
 ***********************************************************************/
 char * Abc_NtkLogicStoreName( Abc_Obj_t * pObjNew, char * pNameOld )
 {
-/*
-    char * pNewName;
-    assert( Abc_ObjIsCio(pObjNew) );
-    // get the new name
-    pNewName = Abc_NtkRegisterName( pObjNew->pNtk, pNameOld );
-    // add the name to the table
-    if ( stmm_insert( pObjNew->pNtk->tObj2Name, (char *)pObjNew, pNewName ) )
-    {
-        assert( 0 ); // the object is added for the second time
-    }
-    return pNewName;
-*/
-    Nm_ManStoreIdName( pObjNew->pNtk->pManName, pObjNew->Id, pNameOld, NULL );
-    return NULL;
+    return Nm_ManStoreIdName( pObjNew->pNtk->pManName, pObjNew->Id, pNameOld, NULL );
 }
 
 /**Function*************************************************************
@@ -205,21 +143,7 @@ char * Abc_NtkLogicStoreName( Abc_Obj_t * pObjNew, char * pNameOld )
 ***********************************************************************/
 char * Abc_NtkLogicStoreNamePlus( Abc_Obj_t * pObjNew, char * pNameOld, char * pSuffix )
 {
-/*
-    char * pNewName;
-    assert( pSuffix );
-    assert( Abc_ObjIsCio(pObjNew) );
-    // get the new name
-    pNewName = Abc_NtkRegisterNamePlus( pObjNew->pNtk, pNameOld, pSuffix );
-    // add the name to the table
-    if ( stmm_insert( pObjNew->pNtk->tObj2Name, (char *)pObjNew, pNewName ) )
-    {
-        assert( 0 ); // the object is added for the second time
-    }
-    return pNewName;
-*/
-    Nm_ManStoreIdName( pObjNew->pNtk->pManName, pObjNew->Id, pNameOld, pSuffix );
-    return NULL;
+    return Nm_ManStoreIdName( pObjNew->pNtk->pManName, pObjNew->Id, pNameOld, pSuffix );
 }
 
 /**Function*************************************************************
@@ -239,17 +163,20 @@ void Abc_NtkDupCioNamesTable( Abc_Ntk_t * pNtk, Abc_Ntk_t * pNtkNew )
     int i;
     assert( Abc_NtkPiNum(pNtk) == Abc_NtkPiNum(pNtkNew) );
     assert( Abc_NtkPoNum(pNtk) == Abc_NtkPoNum(pNtkNew) );
+    assert( Abc_NtkAssertNum(pNtk) == Abc_NtkAssertNum(pNtkNew) );
     assert( Abc_NtkLatchNum(pNtk) == Abc_NtkLatchNum(pNtkNew) );
-//    assert( st_count(pNtk->tObj2Name) > 0 );
-//    assert( st_count(pNtkNew->tObj2Name) == 0 );
+    assert( Nm_ManNumEntries(pNtk->pManName) > 0 );
+    assert( Nm_ManNumEntries(pNtkNew->pManName) == 0 );
     // copy the CI/CO names if given
     Abc_NtkForEachPi( pNtk, pObj, i )
-        Abc_NtkLogicStoreName( Abc_NtkPi(pNtkNew,i),    Abc_ObjName(Abc_ObjFanout0Ntk(pObj)) );
+        Abc_NtkLogicStoreName( Abc_NtkPi(pNtkNew,i),      Abc_ObjName(Abc_ObjFanout0Ntk(pObj)) );
     Abc_NtkForEachPo( pNtk, pObj, i ) 
-        Abc_NtkLogicStoreName( Abc_NtkPo(pNtkNew,i),    Abc_ObjName(Abc_ObjFanin0Ntk(pObj)) );
+        Abc_NtkLogicStoreName( Abc_NtkPo(pNtkNew,i),      Abc_ObjName(Abc_ObjFanin0Ntk(pObj)) );
+    Abc_NtkForEachAssert( pNtk, pObj, i ) 
+        Abc_NtkLogicStoreName( Abc_NtkAssert(pNtkNew,i),  Abc_ObjName(Abc_ObjFanin0Ntk(pObj)) );
     if ( !Abc_NtkIsSeq(pNtk) )
     Abc_NtkForEachLatch( pNtk, pObj, i )
-        Abc_NtkLogicStoreName( Abc_NtkLatch(pNtkNew,i), Abc_ObjName(Abc_ObjFanout0Ntk(pObj)) );
+        Abc_NtkLogicStoreName( Abc_NtkLatch(pNtkNew,i),   Abc_ObjName(Abc_ObjFanout0Ntk(pObj)) );
 }
 
 /**Function*************************************************************
@@ -270,8 +197,8 @@ void Abc_NtkDupCioNamesTableDual( Abc_Ntk_t * pNtk, Abc_Ntk_t * pNtkNew )
     assert( Abc_NtkPiNum(pNtk) == Abc_NtkPiNum(pNtkNew) );
     assert( Abc_NtkPoNum(pNtk) * 2 == Abc_NtkPoNum(pNtkNew) );
     assert( Abc_NtkLatchNum(pNtk) == Abc_NtkLatchNum(pNtkNew) );
-//    assert( st_count(pNtk->tObj2Name) > 0 );
-//    assert( st_count(pNtkNew->tObj2Name) == 0 );
+    assert( Nm_ManNumEntries(pNtk->pManName) > 0 );
+    assert( Nm_ManNumEntries(pNtkNew->pManName) == 0 );
     // copy the CI/CO names if given
     Abc_NtkForEachPi( pNtk, pObj, i )
         Abc_NtkLogicStoreName( Abc_NtkPi(pNtkNew,i),    Abc_ObjName(pObj) );
@@ -280,6 +207,8 @@ void Abc_NtkDupCioNamesTableDual( Abc_Ntk_t * pNtk, Abc_Ntk_t * pNtkNew )
         Abc_NtkLogicStoreNamePlus( Abc_NtkPo(pNtkNew,2*i+0),    Abc_ObjName(pObj), "_pos" );
         Abc_NtkLogicStoreNamePlus( Abc_NtkPo(pNtkNew,2*i+1),    Abc_ObjName(pObj), "_neg" );
     }
+    Abc_NtkForEachAssert( pNtk, pObj, i ) 
+        Abc_NtkLogicStoreName( Abc_NtkAssert(pNtkNew,i),  Abc_ObjName(pObj) );
     if ( !Abc_NtkIsSeq(pNtk) )
     Abc_NtkForEachLatch( pNtk, pObj, i )
         Abc_NtkLogicStoreName( Abc_NtkLatch(pNtkNew,i), Abc_ObjName(pObj) );
@@ -439,22 +368,16 @@ void Abc_NtkOrderObjsByName( Abc_Ntk_t * pNtk, int fComb )
     Abc_NtkForEachLatch( pNtk, pObj, i )
         pObj->pCopy = (Abc_Obj_t *)Abc_ObjName(pObj);
     // order objects alphabetically
-    qsort( pNtk->vCis->pArray, pNtk->nPis, sizeof(Abc_Obj_t *), 
+    qsort( (void *)Vec_PtrArray(pNtk->vPis), Vec_PtrSize(pNtk->vPis), sizeof(Abc_Obj_t *), 
         (int (*)(const void *, const void *)) Abc_NodeCompareNames );
-    qsort( pNtk->vCos->pArray, pNtk->nPos, sizeof(Abc_Obj_t *), 
+    qsort( (void *)Vec_PtrArray(pNtk->vPos), Vec_PtrSize(pNtk->vPos), sizeof(Abc_Obj_t *), 
         (int (*)(const void *, const void *)) Abc_NodeCompareNames );
     // if the comparison if combinational (latches as PIs/POs), order them too
     if ( fComb )
-    {
-        qsort( pNtk->vLats->pArray, pNtk->nLatches, sizeof(Abc_Obj_t *), 
+        qsort( (void *)Vec_PtrArray(pNtk->vLatches), Vec_PtrSize(pNtk->vLatches), sizeof(Abc_Obj_t *), 
             (int (*)(const void *, const void *)) Abc_NodeCompareNames );
-        // add latches to make COs
-        Abc_NtkForEachLatch( pNtk, pObj, i )
-        {
-            Vec_PtrWriteEntry( pNtk->vCis, pNtk->nPis + i, pObj );
-            Vec_PtrWriteEntry( pNtk->vCos, pNtk->nPos + i, pObj );
-        }
-    }
+    // order CIs/COs first PIs/POs(Asserts) then latches
+    Abc_NtkOrderCisCos( pNtk );
     // clean the copy fields
     Abc_NtkForEachPi( pNtk, pObj, i )
         pObj->pCopy = NULL;
@@ -515,6 +438,26 @@ void Abc_NtkAddDummyPoNames( Abc_Ntk_t * pNtk )
   SeeAlso     []
 
 ***********************************************************************/
+void Abc_NtkAddDummyAssertNames( Abc_Ntk_t * pNtk )
+{
+    Abc_Obj_t * pObj;
+    int nDigits, i;
+    nDigits = Extra_Base10Log( Abc_NtkAssertNum(pNtk) );
+    Abc_NtkForEachAssert( pNtk, pObj, i )
+        Abc_NtkLogicStoreName( pObj, Abc_ObjNameDummy("a", i, nDigits) );
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Adds dummy names.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
 void Abc_NtkAddDummyLatchNames( Abc_Ntk_t * pNtk )
 {
     Abc_Obj_t * pObj;
@@ -537,13 +480,11 @@ void Abc_NtkAddDummyLatchNames( Abc_Ntk_t * pNtk )
 ***********************************************************************/
 void Abc_NtkShortNames( Abc_Ntk_t * pNtk )
 {
-//    stmm_free_table( pNtk->tObj2Name );
-//    pNtk->tObj2Name = stmm_init_table(stmm_ptrcmp, stmm_ptrhash);
     Nm_ManFree( pNtk->pManName );
-    pNtk->pManName = Nm_ManCreate( Abc_NtkPiNum(pNtk) + Abc_NtkPoNum(pNtk) + Abc_NtkLatchNum(pNtk) + 10 );
-
+    pNtk->pManName = Nm_ManCreate( Abc_NtkCiNum(pNtk) + Abc_NtkCoNum(pNtk) - Abc_NtkLatchNum(pNtk) + 10 );
     Abc_NtkAddDummyPiNames( pNtk );
     Abc_NtkAddDummyPoNames( pNtk );
+    Abc_NtkAddDummyAssertNames( pNtk );
     Abc_NtkAddDummyLatchNames( pNtk );
 }
 

src/base/abc/abcNetlist.c

@@ -106,33 +106,22 @@ Abc_Ntk_t * Abc_NtkNetlistToLogicHie( Abc_Ntk_t * pNtk )
     // clean the node copy fields
     Abc_NtkForEachNode( pNtk, pObj, i )
         pObj->pCopy = NULL;
-    // map the constant nodes
-    if ( Abc_NtkConst1(pNtk) )
-        Abc_NtkConst1(pNtk)->pCopy = Abc_NtkConst1(pNtkNew);
-    // clone PIs/POs and make old nets point to new terminals; create PI/PO names
-    Abc_NtkForEachPi( pNtk, pObj, i )
+    // clone PIs/POs/latches and make old nets point to new terminals; create names
+    Abc_NtkForEachCi( pNtk, pObj, i )
     {
         Abc_ObjFanout0(pObj)->pCopy = Abc_NtkDupObj(pNtkNew, pObj);
-        Abc_NtkLogicStoreName( pObj->pCopy, Abc_ObjName(pObj) );
+        Abc_NtkLogicStoreName( pObj->pCopy, Abc_ObjName(Abc_ObjFanout0(pObj)) );
     }
     Abc_NtkForEachPo( pNtk, pObj, i )
     {
         Abc_NtkDupObj(pNtkNew, pObj);
-        Abc_NtkLogicStoreName( pObj->pCopy, Abc_ObjName(pObj) );
+        Abc_NtkLogicStoreName( pObj->pCopy, Abc_ObjName(Abc_ObjFanin0(pObj)) );
     }
     // recursively flatten hierarchy, create internal logic, add new PI/PO names if there are black boxes
     Abc_NtkNetlistToLogicHie_rec( pNtkNew, pNtk, &Counter );
     if ( Counter )
         printf( "Warning: The total of %d block boxes are transformed into PI/PO pairs.\n", Counter );
-    // add latches
-    Abc_NtkForEachLatch( pNtk, pObj, i )
-    {
-        Abc_ObjFanout0(pObj)->pCopy = Abc_NtkDupObj(pNtkNew, pObj);
-        Vec_PtrPush( pNtkNew->vCis, pObj->pCopy );
-        Vec_PtrPush( pNtkNew->vCos, pObj->pCopy );
-        Abc_NtkLogicStoreName( Abc_NtkLatch(pNtkNew,i), Abc_ObjName(pObj) );
-    }
-    // collect the CO nodes
+    // connect the CO nodes
     Abc_NtkForEachCo( pNtk, pObj, i )
         Abc_ObjAddFanin( pObj->pCopy, Abc_ObjFanin0(pObj)->pCopy );
     // copy the timing information
@@ -167,62 +156,75 @@ void Abc_NtkNetlistToLogicHie_rec( Abc_Ntk_t * pNtkNew, Abc_Ntk_t * pNtkOld, int
     int i, k;
     // collect nodes and boxes in topological order
     vNodes = Abc_NtkDfs( pNtkOld, 0 );
-    // create logic for nodes and boxes
+    // duplicate nodes, create PIs/POs corresponding to blackboxes
+    // have to do it first if blackboxes break combinational loops
+    // (current we do not allow whiteboxes to break combinational loops)
     Vec_PtrForEachEntry( vNodes, pNode, i )
     {
-        if ( Abc_ObjFaninNum(pNode) == 0 )
-            continue;
         if ( Abc_ObjIsNode(pNode) )
         {
             // duplicate the node and save it in the fanout net
             Abc_NtkDupObj( pNtkNew, pNode );
+            Abc_ObjFanout0(pNode)->pCopy = pNode->pCopy;
+            continue;
+        }
+        assert( Abc_ObjIsBox(pNode) );
+        pNtkModel = pNode->pData;
+        if ( !Abc_NtkHasBlackbox(pNtkModel) )
+            continue;
+        // consider this blockbox
+        if ( pNtkNew->pBlackBoxes == NULL )
+        {
+            pNtkNew->pBlackBoxes = Vec_IntAlloc( 10 );
+            Vec_IntPush( pNtkNew->pBlackBoxes, (Abc_NtkPiNum(pNtkNew) << 16) | Abc_NtkPoNum(pNtkNew) );
+        }
+        sprintf( Prefix, "%s_%d_", Abc_NtkName(pNtkModel), *pCounter );
+        // create new PIs from the POs of the box
+        Abc_NtkForEachPo( pNtkModel, pObj, k )
+        {
+            pObj->pCopy = Abc_NtkCreatePi( pNtkNew );
+            Abc_ObjFanout(pNode, k)->pCopy = pObj->pCopy;
+            Abc_NtkLogicStoreNamePlus( pObj->pCopy, Prefix, Abc_ObjName(Abc_ObjFanin0(pObj)) );
+        }
+        // create new POs from the PIs of the box
+        Abc_NtkForEachPi( pNtkModel, pObj, k )
+        {
+            pObj->pCopy = Abc_NtkCreatePo( pNtkNew );
+//            Abc_ObjAddFanin( pObj->pCopy, Abc_ObjFanin(pNode, k)->pCopy );
+            Abc_NtkLogicStoreNamePlus( pObj->pCopy, Prefix, Abc_ObjName(Abc_ObjFanout0(pObj)) );
+        }
+        (*pCounter)++;
+        Vec_IntPush( pNtkNew->pBlackBoxes, (Abc_NtkPiNum(pNtkNew) << 16) | Abc_NtkPoNum(pNtkNew) );
+    }
+    // connect nodes and boxes
+    Vec_PtrForEachEntry( vNodes, pNode, i )
+    {
+        if ( Abc_ObjIsNode(pNode) )
+        {
+//            printf( "adding node %s\n", Abc_ObjName(Abc_ObjFanout0(pNode)) );
             Abc_ObjForEachFanin( pNode, pFanin, k )
                 Abc_ObjAddFanin( pNode->pCopy, pFanin->pCopy );
-            Abc_ObjFanout0(pNode)->pCopy = pNode->pCopy;
             continue;
         }
         assert( Abc_ObjIsBox(pNode) );
         pNtkModel = pNode->pData;
+//        printf( "adding model %s\n", Abc_NtkName(pNtkModel) );
         // consider the case of the black box
-        if ( Abc_NtkIsBlackbox(pNtkModel) )
+        if ( Abc_NtkHasBlackbox(pNtkModel) )
         {
-            if ( pNtkNew->pBlackBoxes == NULL )
-            {
-                pNtkNew->pBlackBoxes = Vec_IntAlloc( 10 );
-                Vec_IntPush( pNtkNew->pBlackBoxes, (Abc_NtkPiNum(pNtkNew) << 16) | Abc_NtkPoNum(pNtkNew) );
-            }
-            sprintf( Prefix, "%s_%d_", Abc_NtkName(pNtkModel), *pCounter );
-            // create new PIs from the POs of the box
-            Abc_NtkForEachPo( pNtkModel, pObj, k )
-            {
-                pObj->pCopy = Abc_NtkCreatePi( pNtkNew );
-                Abc_ObjFanout(pNode, k)->pCopy = pObj->pCopy;
-                Abc_NtkLogicStoreNamePlus( pObj->pCopy, Prefix, Abc_ObjName(pObj) );
-            }
             // create new POs from the PIs of the box
             Abc_NtkForEachPi( pNtkModel, pObj, k )
-            {
-                pObj->pCopy = Abc_NtkCreatePo( pNtkNew );
                 Abc_ObjAddFanin( pObj->pCopy, Abc_ObjFanin(pNode, k)->pCopy );
-                Abc_NtkLogicStoreNamePlus( pObj->pCopy, Prefix, Abc_ObjName(pObj) );
-            }
-            (*pCounter)++;
-            Vec_IntPush( pNtkNew->pBlackBoxes, (Abc_NtkPiNum(pNtkNew) << 16) | Abc_NtkPoNum(pNtkNew) );
-        }
-        else
-        {
-            // map the constant nodes
-            if ( Abc_NtkConst1(pNtkModel) )
-                Abc_NtkConst1(pNtkModel)->pCopy = Abc_NtkConst1(pNtkNew);
-            // transfer the nodes to the box inputs
-            Abc_NtkForEachPi( pNtkModel, pObj, k )
-                Abc_ObjFanout0(pObj)->pCopy = Abc_ObjFanin(pNode, k)->pCopy;
-            // construct recursively
-            Abc_NtkNetlistToLogicHie_rec( pNtkNew, pNtkModel, pCounter );
-            // transfer the results back
-            Abc_NtkForEachPo( pNtkModel, pObj, k )
-                Abc_ObjFanout(pNode, k)->pCopy = Abc_ObjFanin0(pObj)->pCopy;    
+            continue;
         }
+        // transfer the nodes to the box inputs
+        Abc_NtkForEachPi( pNtkModel, pObj, k )
+            Abc_ObjFanout0(pObj)->pCopy = Abc_ObjFanin(pNode, k)->pCopy;
+        // construct recursively
+        Abc_NtkNetlistToLogicHie_rec( pNtkNew, pNtkModel, pCounter );
+        // transfer the results back
+        Abc_NtkForEachPo( pNtkModel, pObj, k )
+            Abc_ObjFanout(pNode, k)->pCopy = Abc_ObjFanin0(pObj)->pCopy;    
     }
     Vec_PtrFree( vNodes );
 }
@@ -352,7 +354,7 @@ Abc_Ntk_t * Abc_NtkLogicSopToNetlist( Abc_Ntk_t * pNtk )
         // the driver is a node
 
         // get the CO name
-        pNameCo = Abc_ObjIsPo(pObj)? Abc_ObjName(pObj) : Abc_ObjNameSuffix( pObj, "_in" );
+        pNameCo = Abc_ObjIsLatch(pObj)? Abc_ObjNameSuffix( pObj, "_in" ) : Abc_ObjName(pObj);
         // make sure CO has a unique name
         assert( Abc_NtkFindNet( pNtkNew, pNameCo ) == NULL );
         // create the CO net and connect it to CO
@@ -401,6 +403,7 @@ Abc_Ntk_t * Abc_NtkAigToLogicSop( Abc_Ntk_t * pNtk )
 {
     Abc_Ntk_t * pNtkNew; 
     Abc_Obj_t * pObj, * pFanin, * pNodeNew;
+    Vec_Int_t * vInts;
     int i, k;
     assert( Abc_NtkIsStrash(pNtk) );
     // start the network
@@ -423,16 +426,17 @@ Abc_Ntk_t * Abc_NtkAigToLogicSop( Abc_Ntk_t * pNtk )
         // create an OR gate
         pNodeNew = Abc_NtkCreateNode(pNtkNew);
         // add fanins
-        Vec_IntClear( pNtk->vIntTemp );
+        vInts = Vec_IntAlloc( 10 );
         for ( pFanin = pObj; pFanin; pFanin = pFanin->pData )
         {
-            Vec_IntPush( pNtk->vIntTemp, (int)(pObj->fPhase != pFanin->fPhase) );
+            Vec_IntPush( vInts, (int)(pObj->fPhase != pFanin->fPhase) );
             Abc_ObjAddFanin( pNodeNew, pFanin->pCopy );
         }
         // create the logic function
-        pNodeNew->pData = Abc_SopCreateOrMultiCube( pNtkNew->pManFunc, pNtk->vIntTemp->nSize, pNtk->vIntTemp->pArray );
+        pNodeNew->pData = Abc_SopCreateOrMultiCube( pNtkNew->pManFunc, Vec_IntSize(vInts), Vec_IntArray(vInts) );
         // set the new node
         pObj->pCopy->pCopy = pNodeNew;
+        Vec_IntFree( vInts );
     }
     // connect the internal nodes
     Abc_NtkForEachNode( pNtk, pObj, i )

src/base/abc/abcNtk.c

@@ -53,19 +53,14 @@ Abc_Ntk_t * Abc_NtkAlloc( Abc_NtkType_t Type, Abc_NtkFunc_t Func )
     pNtk->Id          = !Abc_HManIsRunning()? 0 : Abc_HManGetNewNtkId();
     // start the object storage
     pNtk->vObjs       = Vec_PtrAlloc( 100 );
-    pNtk->vLats       = Vec_PtrAlloc( 100 );
-    pNtk->vCutSet     = Vec_PtrAlloc( 100 );
+    pNtk->vLatches    = Vec_PtrAlloc( 100 );
+    pNtk->vAsserts    = Vec_PtrAlloc( 100 );
+    pNtk->vPis        = Vec_PtrAlloc( 100 );
+    pNtk->vPos        = Vec_PtrAlloc( 100 );
     pNtk->vCis        = Vec_PtrAlloc( 100 );
     pNtk->vCos        = Vec_PtrAlloc( 100 );
-    pNtk->vAsserts    = Vec_PtrAlloc( 100 );
-    pNtk->vPtrTemp    = Vec_PtrAlloc( 100 );
-    pNtk->vIntTemp    = Vec_IntAlloc( 100 );
-    pNtk->vStrTemp    = Vec_StrAlloc( 100 );
-    // start the hash table
-//    pNtk->tName2Net   = stmm_init_table(strcmp, stmm_strhash);
-//    pNtk->tObj2Name   = stmm_init_table(stmm_ptrcmp, stmm_ptrhash);
+    pNtk->vCutSet     = Vec_PtrAlloc( 100 );
     // start the memory managers
-//    pNtk->pMmNames    = Extra_MmFlexStart();
     pNtk->pMmObj      = Extra_MmFixedStart( sizeof(Abc_Obj_t) );
     pNtk->pMmStep     = Extra_MmStepStart( ABC_NUM_STEPS );
     // get ready to assign the first Obj ID
@@ -115,7 +110,7 @@ Abc_Ntk_t * Abc_NtkAlloc( Abc_NtkType_t Type, Abc_NtkFunc_t Func )
 Abc_Ntk_t * Abc_NtkStartFrom( Abc_Ntk_t * pNtk, Abc_NtkType_t Type, Abc_NtkFunc_t Func )
 {
     Abc_Ntk_t * pNtkNew; 
-    Abc_Obj_t * pObj, * pObjNew;
+    Abc_Obj_t * pObj;
     int i;
     if ( pNtk == NULL )
         return NULL;
@@ -135,12 +130,10 @@ Abc_Ntk_t * Abc_NtkStartFrom( Abc_Ntk_t * pNtk, Abc_NtkType_t Type, Abc_NtkFunc_
         Abc_NtkDupObj(pNtkNew, pObj);
     Abc_NtkForEachPo( pNtk, pObj, i )
         Abc_NtkDupObj(pNtkNew, pObj);
+    Abc_NtkForEachAssert( pNtk, pObj, i )
+        Abc_NtkDupObj(pNtkNew, pObj);
     Abc_NtkForEachLatch( pNtk, pObj, i )
-    {
-        pObjNew = Abc_NtkDupObj(pNtkNew, pObj);
-        Vec_PtrPush( pNtkNew->vCis, pObjNew );
-        Vec_PtrPush( pNtkNew->vCos, pObjNew );
-    }
+        Abc_NtkDupObj(pNtkNew, pObj);
     if ( Abc_NtkIsStrash(pNtk) && Abc_HManIsRunning() )
     {
         Abc_HManAddProto( Abc_NtkConst1(pNtk)->pCopy, Abc_NtkConst1(pNtk) );
@@ -202,15 +195,12 @@ Abc_Ntk_t * Abc_NtkStartFromDual( Abc_Ntk_t * pNtk, Abc_NtkType_t Type, Abc_NtkF
         // collect first to old
         pObj->pCopy = pObjNew;
     }
+    Abc_NtkForEachAssert( pNtk, pObj, i )
+        Abc_NtkDupObj(pNtkNew, pObj);
     Abc_NtkForEachLatch( pNtk, pObj, i )
-    {
-        pObjNew = Abc_NtkDupObj(pNtkNew, pObj);
-        Vec_PtrPush( pNtkNew->vCis, pObjNew );
-        Vec_PtrPush( pNtkNew->vCos, pObjNew );
-    }
+        Abc_NtkDupObj(pNtkNew, pObj);
     // transfer the names
     Abc_NtkDupCioNamesTableDual( pNtk, pNtkNew );
-//    Abc_ManTimeDup( pNtk, pNtkNew );
     // check that the CI/CO/latches are copied correctly
     assert( Abc_NtkCiNum(pNtk)    == Abc_NtkCiNum(pNtkNew) );
     assert( Abc_NtkCoNum(pNtk)* 2 == Abc_NtkCoNum(pNtkNew) );
@@ -244,54 +234,6 @@ void Abc_NtkFinalize( Abc_Ntk_t * pNtk, Abc_Ntk_t * pNtkNew )
 
 /**Function*************************************************************
 
-  Synopsis    [Finalizes the network using the existing network as a model.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-void Abc_NtkFinalizeRegular( Abc_Ntk_t * pNtk, Abc_Ntk_t * pNtkNew )
-{
-    Abc_Obj_t * pObj, * pDriver, * pDriverNew;
-    int i;
-    // set the COs of the strashed network
-    Abc_NtkForEachCo( pNtk, pObj, i )
-    {
-        pDriver    = Abc_ObjFanin0Ntk( Abc_ObjFanin0(pObj) );
-        pDriverNew = pDriver->pCopy;
-        Abc_ObjAddFanin( pObj->pCopy, pDriverNew );
-    }
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Finalizes the network adding latches to CI/CO lists and creates their names.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-void Abc_NtkFinalizeLatches( Abc_Ntk_t * pNtk )
-{
-    Abc_Obj_t * pLatch;
-    int i;
-    // set the COs of the strashed network
-    Abc_NtkForEachLatch( pNtk, pLatch, i )
-    {
-        Vec_PtrPush( pNtk->vCis, pLatch );
-        Vec_PtrPush( pNtk->vCos, pLatch );
-        Abc_NtkLogicStoreName( pLatch, Abc_ObjNameSuffix(pLatch, "L") );
-    }
-}
-
-/**Function*************************************************************
-
   Synopsis    [Starts a new network using existing network as a model.]
 
   Description []
@@ -325,9 +267,9 @@ Abc_Ntk_t * Abc_NtkStartRead( char * pName )
 ***********************************************************************/
 void Abc_NtkFinalizeRead( Abc_Ntk_t * pNtk )
 {
-    Abc_Obj_t * pLatch, * pBox, * pObj;
+    Abc_Obj_t * pBox, * pObj;
     int i;
-    if ( pNtk->ntkType == ABC_NTK_BLACKBOX )
+    if ( Abc_NtkHasBlackbox(pNtk) )
     {
         pBox = Abc_NtkCreateBox(pNtk);
         Abc_NtkForEachPi( pNtk, pObj, i )
@@ -339,14 +281,8 @@ void Abc_NtkFinalizeRead( Abc_Ntk_t * pNtk )
     assert( Abc_NtkIsNetlist(pNtk) );
     // fix the net drivers
     Abc_NtkFixNonDrivenNets( pNtk );
-    // create the names table
-//    Abc_NtkCreateCioNamesTable( pNtk );
-    // add latches to the CI/CO arrays
-    Abc_NtkForEachLatch( pNtk, pLatch, i )
-    {
-        Vec_PtrPush( pNtk->vCis, pLatch );
-        Vec_PtrPush( pNtk->vCos, pLatch );
-    }
+    // reorder the CI/COs to PI/POs first
+    Abc_NtkOrderCisCos( pNtk );
 }
 
 /**Function*************************************************************
@@ -740,7 +676,6 @@ void Abc_NtkDelete( Abc_Ntk_t * pNtk )
     int LargePiece = (4 << ABC_NUM_STEPS);
     if ( pNtk == NULL )
         return;
-//printf( "Deleted newtork %p\n", pNtk );
     // make sure all the marks are clean
     Abc_NtkForEachObj( pNtk, pObj, i )
     {
@@ -765,26 +700,20 @@ void Abc_NtkDelete( Abc_Ntk_t * pNtk )
     if ( pNtk->pExdc )
         Abc_NtkDelete( pNtk->pExdc );
     // free the arrays
+    Vec_PtrFree( pNtk->vPis );
+    Vec_PtrFree( pNtk->vPos );
     Vec_PtrFree( pNtk->vCis );
     Vec_PtrFree( pNtk->vCos );
     Vec_PtrFree( pNtk->vAsserts );
+    Vec_PtrFree( pNtk->vLatches );
     Vec_PtrFree( pNtk->vObjs );
-    Vec_PtrFree( pNtk->vLats );
     Vec_PtrFree( pNtk->vCutSet );
-    Vec_PtrFree( pNtk->vPtrTemp );
-    Vec_IntFree( pNtk->vIntTemp );
-    Vec_StrFree( pNtk->vStrTemp );
     if ( pNtk->pModel ) free( pNtk->pModel );
-    // free the hash table of Obj name into Obj ID
-//    stmm_free_table( pNtk->tName2Net );
-//    stmm_free_table( pNtk->tObj2Name );
     TotalMemory  = 0;
-//    TotalMemory += Extra_MmFlexReadMemUsage(pNtk->pMmNames);
     TotalMemory += Extra_MmFixedReadMemUsage(pNtk->pMmObj);
     TotalMemory += Extra_MmStepReadMemUsage(pNtk->pMmStep);
 //    fprintf( stdout, "The total memory allocated internally by the network = %0.2f Mb.\n", ((double)TotalMemory)/(1<<20) );
     // free the storage 
-//    Extra_MmFlexStop ( pNtk->pMmNames, 0 );
     Extra_MmFixedStop( pNtk->pMmObj,   0 );
     Extra_MmStepStop ( pNtk->pMmStep,  0 );
     // free the timing manager
@@ -802,7 +731,7 @@ void Abc_NtkDelete( Abc_Ntk_t * pNtk )
         else
             Seq_Delete( pNtk->pManFunc );
     }
-    else if ( !Abc_NtkHasMapping(pNtk) )
+    else if ( !Abc_NtkHasMapping(pNtk) && !Abc_NtkHasBlackbox(pNtk) )
         assert( 0 );
     // name manager
     Nm_ManFree( pNtk->pManName );
@@ -815,9 +744,9 @@ void Abc_NtkDelete( Abc_Ntk_t * pNtk )
         stmm_foreach_item( pNtk->tName2Model, gen, &pName, (char **)&pNtkTemp )
             Abc_NtkDelete( pNtkTemp );
         stmm_free_table( pNtk->tName2Model );
-        if ( pNtk->pBlackBoxes ) 
-            Vec_IntFree( pNtk->pBlackBoxes );
     }
+    if ( pNtk->pBlackBoxes ) 
+        Vec_IntFree( pNtk->pBlackBoxes );
     free( pNtk );
 }
 

src/base/abc/abcObj.c

@@ -101,34 +101,32 @@ void Abc_ObjAdd( Abc_Obj_t * pObj )
     // perform specialized operations depending on the object type
     if ( Abc_ObjIsNet(pObj) )
     {
-/*
-        // add the name to the table
-        if ( pObj->pData && stmm_insert( pNtk->tName2Net, pObj->pData, (char *)pObj ) )
-        {
-            printf( "Error: The net is already in the table...\n" );
-            assert( 0 );
-        }
-*/
         pNtk->nNets++;
     }
     else if ( Abc_ObjIsNode(pObj) )
     {
         pNtk->nNodes++;
     }
-    else if ( Abc_ObjIsLatch(pObj) )
-    {
-        Vec_PtrPush( pNtk->vLats, pObj );
-        pNtk->nLatches++;
-    }
     else if ( Abc_ObjIsPi(pObj) )
     {
+        Vec_PtrPush( pNtk->vPis, pObj );
         Vec_PtrPush( pNtk->vCis, pObj );
-        pNtk->nPis++;
     }
     else if ( Abc_ObjIsPo(pObj) )
     {
+        Vec_PtrPush( pNtk->vPos, pObj );
+        Vec_PtrPush( pNtk->vCos, pObj );
+    }
+    else if ( Abc_ObjIsLatch(pObj) )
+    {
+        Vec_PtrPush( pNtk->vLatches, pObj );
+        Vec_PtrPush( pNtk->vCis, pObj );
+        Vec_PtrPush( pNtk->vCos, pObj );
+    }
+    else if ( Abc_ObjIsAssert(pObj) )
+    {
+        Vec_PtrPush( pNtk->vAsserts, pObj );
         Vec_PtrPush( pNtk->vCos, pObj );
-        pNtk->nPos++;
     }
     else if ( Abc_ObjIsBox(pObj) )
     {
@@ -138,7 +136,6 @@ void Abc_ObjAdd( Abc_Obj_t * pObj )
     {
         assert( 0 );
     }
-    assert( pObj->Id >= 0 );
 }
 
 /**Function*************************************************************
@@ -155,7 +152,11 @@ void Abc_ObjAdd( Abc_Obj_t * pObj )
 Abc_Obj_t * Abc_NtkDupObj( Abc_Ntk_t * pNtkNew, Abc_Obj_t * pObj )
 {
     Abc_Obj_t * pObjNew;
+    // create the new object
     pObjNew = Abc_ObjAlloc( pNtkNew, pObj->Type );
+    // add the object to the network
+    Abc_ObjAdd( pObjNew );
+    // copy functionality/names
     if ( Abc_ObjIsNode(pObj) ) // copy the function if functionality is compatible
     {
         if ( pNtkNew->ntkFunc == pObj->pNtk->ntkFunc ) 
@@ -172,18 +173,11 @@ Abc_Obj_t * Abc_NtkDupObj( Abc_Ntk_t * pNtkNew, Abc_Obj_t * pObj )
     }
     else if ( Abc_ObjIsNet(pObj) ) // copy the name
     {
-//        pObjNew->pData = Abc_NtkRegisterName( pNtkNew, pObj->pData );
+        pObjNew->pData = Nm_ManStoreIdName( pNtkNew->pManName, pObjNew->Id, pObj->pData, NULL );
     }
     else if ( Abc_ObjIsLatch(pObj) ) // copy the reset value
         pObjNew->pData = pObj->pData;
     pObj->pCopy = pObjNew;
-    // add the object to the network
-    Abc_ObjAdd( pObjNew );
-
-
-    if ( Abc_ObjIsNet(pObj) )
-        pObjNew->pData = Nm_ManStoreIdName( pNtkNew->pManName, pObjNew->Id, pObj->pData, NULL );
-        
     return pObjNew;
 }
 
@@ -201,37 +195,34 @@ Abc_Obj_t * Abc_NtkDupObj( Abc_Ntk_t * pNtkNew, Abc_Obj_t * pObj )
 ***********************************************************************/
 void Abc_NtkDeleteObj( Abc_Obj_t * pObj )
 {
-    Vec_Ptr_t * vNodes = pObj->pNtk->vPtrTemp;
     Abc_Ntk_t * pNtk = pObj->pNtk;
+    Vec_Ptr_t * vNodes;
     int i;
 
     assert( !Abc_ObjIsComplement(pObj) );
 
     // delete fanins and fanouts
+    vNodes = Vec_PtrAlloc( 100 );
     Abc_NodeCollectFanouts( pObj, vNodes );
     for ( i = 0; i < vNodes->nSize; i++ )
         Abc_ObjDeleteFanin( vNodes->pArray[i], pObj );
     Abc_NodeCollectFanins( pObj, vNodes );
     for ( i = 0; i < vNodes->nSize; i++ )
         Abc_ObjDeleteFanin( pObj, vNodes->pArray[i] );
+    Vec_PtrFree( vNodes );
 
     // remove from the list of objects
     Vec_PtrWriteEntry( pNtk->vObjs, pObj->Id, NULL );
     pObj->Id = (1<<26)-1;
     pNtk->nObjs--;
 
+    // remove from the table of names
+    if ( Nm_ManFindNameById(pObj->pNtk->pManName, pObj->Id) )
+        Nm_ManDeleteIdName(pObj->pNtk->pManName, pObj->Id);
+
     // perform specialized operations depending on the object type
     if ( Abc_ObjIsNet(pObj) )
     {
-        assert( 0 );
-/*
-        // remove the net from the hash table of nets
-        if ( pObj->pData && !stmm_delete( pNtk->tName2Net, (char **)&pObj->pData, (char **)&pObj ) )
-        {
-            printf( "Error: The net is not in the table...\n" );
-            assert( 0 );
-        }
-*/
         pObj->pData = NULL;
         pNtk->nNets--;
     }
@@ -239,26 +230,33 @@ void Abc_NtkDeleteObj( Abc_Obj_t * pObj )
     {
         if ( Abc_NtkHasBdd(pNtk) )
             Cudd_RecursiveDeref( pNtk->pManFunc, pObj->pData );
+        pObj->pData = NULL;
         pNtk->nNodes--;
     }
     else if ( Abc_ObjIsLatch(pObj) )
     {
-        pNtk->nLatches--;
+        Vec_PtrRemove( pNtk->vLatches, pObj );
+        Vec_PtrRemove( pNtk->vCis, pObj );
+        Vec_PtrRemove( pNtk->vCos, pObj );
+    }
+    else if ( Abc_ObjIsPi(pObj) )
+    {
+        Vec_PtrRemove( pObj->pNtk->vPis, pObj );
+        Vec_PtrRemove( pObj->pNtk->vCis, pObj );
     }
     else if ( Abc_ObjIsPo(pObj) )
     {
-        assert( Abc_NtkPoNum(pObj->pNtk) > 0 );
+        Vec_PtrRemove( pObj->pNtk->vPos, pObj );
         Vec_PtrRemove( pObj->pNtk->vCos, pObj );
-        pObj->pNtk->nPos--;
-
-        assert( 0 );
-/*
-        // add the name to the table
-        if ( !stmm_delete( pObj->pNtk->tObj2Name, (char **)&pObj, NULL ) )
-        {
-            assert( 0 ); // the PO is not in the table
-        }
-*/
+    }
+    else if ( Abc_ObjIsAssert(pObj) )
+    {
+        Vec_PtrRemove( pObj->pNtk->vAsserts, pObj );
+        Vec_PtrRemove( pObj->pNtk->vCos, pObj );
+    }
+    else if ( Abc_ObjIsBox(pObj) )
+    {
+        pNtk->nBoxes--;
     }
     else
         assert( 0 );
@@ -377,9 +375,6 @@ Abc_Obj_t * Abc_NtkFindNet( Abc_Ntk_t * pNtk, char * pName )
     Abc_Obj_t * pNet;
     int ObjId;
     assert( Abc_NtkIsNetlist(pNtk) );
-//    if ( stmm_lookup( pNtk->tName2Net, pName, (char**)&pNet ) )
-//        return pNet;
-//    return NULL;
     ObjId = Nm_ManFindIdByName( pNtk->pManName, pName, NULL );
     if ( ObjId == -1 )
         return NULL;
@@ -406,7 +401,6 @@ Abc_Obj_t * Abc_NtkFindOrCreateNet( Abc_Ntk_t * pNtk, char * pName )
         return pNet;
     // create a new net
     pNet = Abc_ObjAlloc( pNtk, ABC_OBJ_NET );
-//    pNet->pData = Abc_NtkRegisterName( pNtk, pName );
     Abc_ObjAdd( pNet );
     pNet->pData = Nm_ManStoreIdName( pNtk->pManName, pNet->Id, pName, NULL );
     return pNet;
@@ -510,6 +504,25 @@ Abc_Obj_t * Abc_NtkCreateLatch( Abc_Ntk_t * pNtk )
 
 /**Function*************************************************************
 
+  Synopsis    [Create the new node.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Abc_Obj_t * Abc_NtkCreateAssert( Abc_Ntk_t * pNtk )
+{
+    Abc_Obj_t * pObj;
+    pObj = Abc_ObjAlloc( pNtk, ABC_OBJ_ASSERT );     
+    Abc_ObjAdd( pObj );
+    return pObj;
+}
+
+/**Function*************************************************************
+
   Synopsis    [Creates inverter.]
 
   Description []

src/base/abc/abcSop.c

@@ -360,6 +360,44 @@ char * Abc_SopCreateBuf( Extra_MmFlex_t * pMan )
     return Abc_SopRegister(pMan, "1 1\n");
 }
 
+/**Function*************************************************************
+
+  Synopsis    [Creates the arbitrary cover from the truth table.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+char * Abc_SopCreateFromTruth( Extra_MmFlex_t * pMan, int nVars, unsigned * pTruth )
+{
+    char * pSop, * pCube;
+    int nMints, Counter, i, k;
+    // count the number of true minterms
+    Counter = 0;
+    nMints = (1 << nVars);
+    for ( i = 0; i < nMints; i++ )
+        Counter += ((pTruth[i>>5] & (1 << (i&31))) > 0);
+    // SOP is not well-defined if the truth table is constant 0
+    assert( Counter > 0 );
+    if ( Counter == 0 )
+        return NULL;
+    // start the cover
+    pSop = Abc_SopStart( pMan, Counter, nVars );
+    // create true minterms
+    Counter = 0;
+    for ( i = 0; i < nMints; i++ )
+        if ( (pTruth[i>>5] & (1 << (i&31))) > 0 )
+        {
+            pCube = pSop + Counter * (nVars + 3);
+            for ( k = 0; k < nVars; k++ )
+                pCube[k] = '0' + ((i & (1 << k)) > 0);
+            Counter++;
+        }
+    return pSop;
+}
 
 /**Function*************************************************************
 

src/base/abc/abcUtil.c

@@ -47,7 +47,7 @@ void Abc_NtkIncrementTravId( Abc_Ntk_t * pNtk )
 {
     Abc_Obj_t * pObj;
     int i;
-    if ( pNtk->nTravIds == (1<<10)-1 )
+    if ( pNtk->nTravIds == (1<<9)-1 )
     {
         pNtk->nTravIds = 0;
         Abc_NtkForEachObj( pNtk, pObj, i )
@@ -58,6 +58,36 @@ void Abc_NtkIncrementTravId( Abc_Ntk_t * pNtk )
 
 /**Function*************************************************************
 
+  Synopsis    [Order CI/COs.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Abc_NtkOrderCisCos( Abc_Ntk_t * pNtk )
+{
+    Abc_Obj_t * pObj;
+    int i;
+    Vec_PtrClear( pNtk->vCis );
+    Vec_PtrClear( pNtk->vCos );
+    Abc_NtkForEachPi( pNtk, pObj, i )
+        Vec_PtrPush( pNtk->vCis, pObj );
+    Abc_NtkForEachPo( pNtk, pObj, i )
+        Vec_PtrPush( pNtk->vCos, pObj );
+    Abc_NtkForEachAssert( pNtk, pObj, i )
+        Vec_PtrPush( pNtk->vCos, pObj );
+    Abc_NtkForEachLatch( pNtk, pObj, i )
+    {
+        Vec_PtrPush( pNtk->vCis, pObj );
+        Vec_PtrPush( pNtk->vCos, pObj );
+    }
+}
+
+/**Function*************************************************************
+
   Synopsis    [Reads the number of cubes of the node.]
 
   Description []
@@ -84,7 +114,7 @@ int Abc_NtkGetCubeNum( Abc_Ntk_t * pNtk )
 
 /**Function*************************************************************
 
-  Synopsis    [Reads the number of cubes of the node.]
+  Synopsis    [Reads the number of literals in the SOPs of the nodes.]
 
   Description []
                
@@ -1029,6 +1059,12 @@ void Abc_NtkReassignIds( Abc_Ntk_t * pNtk )
         pNode->Id = Vec_PtrSize( vObjsNew );
         Vec_PtrPush( vObjsNew, pNode );
     }
+    // put assert nodes next
+    Abc_NtkForEachAssert( pNtk, pNode, i )
+    {
+        pNode->Id = Vec_PtrSize( vObjsNew );
+        Vec_PtrPush( vObjsNew, pNode );
+    }
     // put latches next
     Abc_NtkForEachLatch( pNtk, pNode, i )
     {

src/base/abci/abcAttach.c

@@ -387,13 +387,13 @@ void Abc_TruthPermute( char * pPerm, int nVars, unsigned * uTruthNode, unsigned
     nMints = (1 << nVars);
     for ( iMint = 0; iMint < nMints; iMint++ )
     {
-        if ( (uTruthNode[iMint/32] & (1 << (iMint%32))) == 0 )
+        if ( (uTruthNode[iMint>>5] & (1 << (iMint&31))) == 0 )
             continue;
         iMintPerm = 0;
         for ( v = 0; v < nVars; v++ )
             if ( iMint & (1 << v) )
                 iMintPerm |= (1 << pPerm[v]);
-        uTruthPerm[iMintPerm/32] |= (1 << (iMintPerm%32));     
+        uTruthPerm[iMintPerm>>5] |= (1 << (iMintPerm&31));     
     }
 }
 

src/base/abci/abcMiter.c

@@ -81,7 +81,7 @@ Abc_Ntk_t * Abc_NtkMiter( Abc_Ntk_t * pNtk1, Abc_Ntk_t * pNtk2, int fComb )
 ***********************************************************************/
 Abc_Ntk_t * Abc_NtkMiterInt( Abc_Ntk_t * pNtk1, Abc_Ntk_t * pNtk2, int fComb )
 {
-    char Buffer[100];
+    char Buffer[1000];
     Abc_Ntk_t * pNtkMiter;
 
     assert( Abc_NtkIsStrash(pNtk1) );
@@ -168,16 +168,12 @@ void Abc_NtkMiterPrepare( Abc_Ntk_t * pNtk1, Abc_Ntk_t * pNtk2, Abc_Ntk_t * pNtk
         Abc_NtkForEachLatch( pNtk1, pObj, i )
         {
             pObjNew = Abc_NtkDupObj( pNtkMiter, pObj );
-            Vec_PtrPush( pNtkMiter->vCis, pObjNew );
-            Vec_PtrPush( pNtkMiter->vCos, pObjNew );
             // add name
             Abc_NtkLogicStoreNamePlus( pObjNew, Abc_ObjName(pObj), "_1" );
         }
         Abc_NtkForEachLatch( pNtk2, pObj, i )
         {
             pObjNew = Abc_NtkDupObj( pNtkMiter, pObj );
-            Vec_PtrPush( pNtkMiter->vCis, pObjNew );
-            Vec_PtrPush( pNtkMiter->vCos, pObjNew );
             // add name
             Abc_NtkLogicStoreNamePlus( pObjNew, Abc_ObjName(pObj), "_2" );
         }
@@ -295,7 +291,7 @@ void Abc_NtkMiterFinalize( Abc_Ntk_t * pNtk1, Abc_Ntk_t * pNtk2, Abc_Ntk_t * pNt
 ***********************************************************************/
 Abc_Ntk_t * Abc_NtkMiterAnd( Abc_Ntk_t * pNtk1, Abc_Ntk_t * pNtk2 )
 {
-    char Buffer[100];
+    char Buffer[1000];
     Abc_Ntk_t * pNtkMiter;
     Abc_Obj_t * pOutput1, * pOutput2;
     Abc_Obj_t * pRoot1, * pRoot2, * pMiter;
@@ -352,7 +348,7 @@ Abc_Ntk_t * Abc_NtkMiterAnd( Abc_Ntk_t * pNtk1, Abc_Ntk_t * pNtk2 )
 ***********************************************************************/
 Abc_Ntk_t * Abc_NtkMiterCofactor( Abc_Ntk_t * pNtk, Vec_Int_t * vPiValues )
 {
-    char Buffer[100];
+    char Buffer[1000];
     Abc_Ntk_t * pNtkMiter;
     Abc_Obj_t * pRoot, * pOutput1;
     int Value, i;
@@ -418,7 +414,7 @@ Abc_Ntk_t * Abc_NtkMiterCofactor( Abc_Ntk_t * pNtk, Vec_Int_t * vPiValues )
 ***********************************************************************/
 Abc_Ntk_t * Abc_NtkMiterForCofactors( Abc_Ntk_t * pNtk, int Out, int In1, int In2 )
 {
-    char Buffer[100];
+    char Buffer[1000];
     Abc_Ntk_t * pNtkMiter;
     Abc_Obj_t * pRoot, * pOutput1, * pOutput2, * pMiter;
 
@@ -665,7 +661,7 @@ void Abc_NtkMiterReport( Abc_Ntk_t * pMiter )
 ***********************************************************************/
 Abc_Ntk_t * Abc_NtkFrames( Abc_Ntk_t * pNtk, int nFrames, int fInitial )
 {
-    char Buffer[100];
+    char Buffer[1000];
     ProgressBar * pProgress;
     Abc_Ntk_t * pNtkFrames;
     Abc_Obj_t * pLatch, * pLatchNew;
@@ -717,8 +713,6 @@ Abc_Ntk_t * Abc_NtkFrames( Abc_Ntk_t * pNtk, int nFrames, int fInitial )
         {
             pLatchNew = Abc_NtkLatch(pNtkFrames, i);
             Abc_ObjAddFanin( pLatchNew, pLatch->pCopy );
-            Vec_PtrPush( pNtkFrames->vCis, pLatchNew );
-            Vec_PtrPush( pNtkFrames->vCos, pLatchNew );
             Abc_NtkLogicStoreName( pLatchNew, Abc_ObjName(pLatch) );
         }
     }
@@ -728,6 +722,9 @@ Abc_Ntk_t * Abc_NtkFrames( Abc_Ntk_t * pNtk, int nFrames, int fInitial )
     // remove dangling nodes
     Abc_AigCleanup( pNtkFrames->pManFunc );
 
+    // reorder the latches
+    Abc_NtkOrderCisCos( pNtkFrames );
+
     // make sure that everything is okay
     if ( !Abc_NtkCheck( pNtkFrames ) )
     {
@@ -773,6 +770,12 @@ void Abc_NtkAddFrame( Abc_Ntk_t * pNtkFrames, Abc_Ntk_t * pNtk, int iFrame )
         Abc_NtkLogicStoreNamePlus( Abc_NtkDupObj(pNtkFrames, pNode), Abc_ObjName(pNode), Buffer );
         Abc_ObjAddFanin( pNode->pCopy, Abc_ObjChild0Copy(pNode) );
     }
+    // add the new asserts
+    Abc_NtkForEachAssert( pNtk, pNode, i )
+    {
+        Abc_NtkLogicStoreNamePlus( Abc_NtkDupObj(pNtkFrames, pNode), Abc_ObjName(pNode), Buffer );
+        Abc_ObjAddFanin( pNode->pCopy, Abc_ObjChild0Copy(pNode) );
+    }
     // transfer the implementation of the latch drivers to the latches
     Abc_NtkForEachLatch( pNtk, pLatch, i )
         pLatch->pNext = Abc_ObjChild0Copy(pLatch);
@@ -795,7 +798,7 @@ void Abc_NtkAddFrame( Abc_Ntk_t * pNtkFrames, Abc_Ntk_t * pNtk, int iFrame )
 ***********************************************************************/
 Abc_Ntk_t * Abc_NtkFrames2( Abc_Ntk_t * pNtk, int nFrames, int fInitial, AddFrameMapping addFrameMapping, void* arg )
 {
-    char Buffer[100];
+    char Buffer[1000];
     ProgressBar * pProgress;
     Abc_Ntk_t * pNtkFrames;
     Vec_Ptr_t * vNodes;
@@ -854,9 +857,6 @@ Abc_Ntk_t * Abc_NtkFrames2( Abc_Ntk_t * pNtk, int nFrames, int fInitial, AddFram
         {
             pLatchNew = Abc_NtkLatch(pNtkFrames, i);
             Abc_ObjAddFanin( pLatchNew, pLatch->pCopy );
-
-            Vec_PtrPush( pNtkFrames->vCis, pLatchNew );
-            Vec_PtrPush( pNtkFrames->vCos, pLatchNew );
             Abc_NtkLogicStoreName( pLatchNew, Abc_ObjName(pLatch) );
         }
     }
@@ -865,6 +865,9 @@ Abc_Ntk_t * Abc_NtkFrames2( Abc_Ntk_t * pNtk, int nFrames, int fInitial, AddFram
 
     // remove dangling nodes
     Abc_AigCleanup( pNtkFrames->pManFunc );
+
+    // reorder the latches
+    Abc_NtkOrderCisCos( pNtkFrames );
     
     // make sure that everything is okay
     if ( !Abc_NtkCheck( pNtkFrames ) )

src/base/abci/abcPrint.c

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

src/base/abci/abcProve.c

@@ -30,7 +30,7 @@ extern int  Abc_NtkRewrite( Abc_Ntk_t * pNtk, int fUpdateLevel, int fUseZeros, i
 extern int  Abc_NtkRefactor( Abc_Ntk_t * pNtk, int nNodeSizeMax, int nConeSizeMax, bool fUpdateLevel, bool fUseZeros, bool fUseDcs, bool fVerbose );
 extern Abc_Ntk_t * Abc_NtkFromFraig( Fraig_Man_t * pMan, Abc_Ntk_t * pNtk );
 
-static Abc_Ntk_t * Abc_NtkMiterFraig( Abc_Ntk_t * pNtk, int nBTLimit, int * pRetValue, int * pNumFails );
+static Abc_Ntk_t * Abc_NtkMiterFraig( Abc_Ntk_t * pNtk, int nBTLimit, sint64 nInspLimit, int * pRetValue, int * pNumFails, sint64 * pNumConfs, sint64 * pNumInspects );
 static void Abc_NtkMiterPrint( Abc_Ntk_t * pNtk, char * pString, int clk, int fVerbose );
 
 
@@ -56,13 +56,14 @@ int Abc_NtkMiterProve( Abc_Ntk_t ** ppNtk, void * pPars )
 {
     Prove_Params_t * pParams = pPars;
     Abc_Ntk_t * pNtk, * pNtkTemp;
-    int RetValue, nIter, Counter, clk, timeStart = clock();
+    int RetValue, nIter, nSatFails, Counter, clk, timeStart = clock();
+    sint64 nSatConfs, nSatInspects, nInspectLimit;
 
     // get the starting network
     pNtk = *ppNtk;
     assert( Abc_NtkIsStrash(pNtk) );
     assert( Abc_NtkPoNum(pNtk) == 1 );
-
+ 
     if ( pParams->fVerbose )
     {
         printf( "RESOURCE LIMITS: Iterations = %d. Rewriting = %s. Fraiging = %s.\n",
@@ -79,7 +80,7 @@ int Abc_NtkMiterProve( Abc_Ntk_t ** ppNtk, void * pPars )
     if ( !pParams->fUseRewriting && !pParams->fUseFraiging )
     {
         clk = clock();
-        RetValue = Abc_NtkMiterSat( pNtk, pParams->nMiteringLimitLast, 0, 0, 0 );
+        RetValue = Abc_NtkMiterSat( pNtk, (sint64)pParams->nMiteringLimitLast, (sint64)0, 0, 0, NULL, NULL );
         Abc_NtkMiterPrint( pNtk, "SAT solving", clk, pParams->fVerbose );
         *ppNtk = pNtk;
         return RetValue;
@@ -98,11 +99,24 @@ int Abc_NtkMiterProve( Abc_Ntk_t ** ppNtk, void * pPars )
 
         // try brute-force SAT
         clk = clock();
-        RetValue = Abc_NtkMiterSat( pNtk, (int)(pParams->nMiteringLimitStart * pow(pParams->nMiteringLimitMulti,nIter)), 0, 0, 0 );
+        nInspectLimit = pParams->nTotalInspectLimit? pParams->nTotalInspectLimit - pParams->nTotalInspectsMade : 0;
+        RetValue = Abc_NtkMiterSat( pNtk, (sint64)(pParams->nMiteringLimitStart * pow(pParams->nMiteringLimitMulti,nIter)), (sint64)nInspectLimit, 0, 0, &nSatConfs, &nSatInspects );
         Abc_NtkMiterPrint( pNtk, "SAT solving", clk, pParams->fVerbose );
         if ( RetValue >= 0 )
             break;
 
+        // add to the number of backtracks and inspects
+        pParams->nTotalBacktracksMade += nSatConfs;
+        pParams->nTotalInspectsMade   += nSatInspects;
+        // check if global resource limit is reached
+        if ( (pParams->nTotalBacktrackLimit && pParams->nTotalBacktracksMade >= pParams->nTotalBacktrackLimit) ||
+             (pParams->nTotalInspectLimit   && pParams->nTotalInspectsMade   >= pParams->nTotalInspectLimit) )
+        {
+            printf( "Reached global limit on conflicts/inspects. Quitting.\n" );
+            *ppNtk = pNtk;
+            return -1;
+        }
+
         // try rewriting
         if ( pParams->fUseRewriting )
         {
@@ -131,18 +145,30 @@ int Abc_NtkMiterProve( Abc_Ntk_t ** ppNtk, void * pPars )
  
         if ( pParams->fUseFraiging )
         {
-            int nSatFails;
             // try FRAIGing
             clk = clock();
-            pNtk = Abc_NtkMiterFraig( pNtkTemp = pNtk, (int)(pParams->nFraigingLimitStart * pow(pParams->nFraigingLimitMulti,nIter)), &RetValue, &nSatFails );  Abc_NtkDelete( pNtkTemp );
+            nInspectLimit = pParams->nTotalInspectLimit? pParams->nTotalInspectLimit - pParams->nTotalInspectsMade : 0;
+            pNtk = Abc_NtkMiterFraig( pNtkTemp = pNtk, (int)(pParams->nFraigingLimitStart * pow(pParams->nFraigingLimitMulti,nIter)), nInspectLimit, &RetValue, &nSatFails, &nSatConfs, &nSatInspects );  Abc_NtkDelete( pNtkTemp );
             Abc_NtkMiterPrint( pNtk, "FRAIGing   ", clk, pParams->fVerbose );
 //            printf( "NumFails = %d\n", nSatFails );
             if ( RetValue >= 0 )
                 break;
+
+            // add to the number of backtracks and inspects
+            pParams->nTotalBacktracksMade += nSatConfs;
+            pParams->nTotalInspectsMade += nSatInspects;
+            // check if global resource limit is reached
+            if ( (pParams->nTotalBacktrackLimit && pParams->nTotalBacktracksMade >= pParams->nTotalBacktrackLimit) ||
+                 (pParams->nTotalInspectLimit   && pParams->nTotalInspectsMade   >= pParams->nTotalInspectLimit) )
+            {
+                printf( "Reached global limit on conflicts/inspects. Quitting.\n" );
+                *ppNtk = pNtk;
+                return -1;
+            }
         }
 
     }    
-/*
+
     // try to prove it using brute force SAT
     if ( RetValue < 0 && pParams->fUseBdds )
     {
@@ -162,7 +188,6 @@ int Abc_NtkMiterProve( Abc_Ntk_t ** ppNtk, void * pPars )
             pNtk = pNtkTemp;
         Abc_NtkMiterPrint( pNtk, "BDD building", clk, pParams->fVerbose );
     }
-*/
 
     if ( RetValue < 0 )
     {
@@ -172,7 +197,8 @@ int Abc_NtkMiterProve( Abc_Ntk_t ** ppNtk, void * pPars )
             fflush( stdout );
         }
         clk = clock();
-        RetValue = Abc_NtkMiterSat( pNtk, pParams->nMiteringLimitLast, 0, 0, 0 );
+        nInspectLimit = pParams->nTotalInspectLimit? pParams->nTotalInspectLimit - pParams->nTotalInspectsMade : 0;
+        RetValue = Abc_NtkMiterSat( pNtk, (sint64)pParams->nMiteringLimitLast, (sint64)nInspectLimit, 0, 0, NULL, NULL );
         Abc_NtkMiterPrint( pNtk, "SAT solving", clk, pParams->fVerbose );
     }
 
@@ -197,7 +223,7 @@ int Abc_NtkMiterProve( Abc_Ntk_t ** ppNtk, void * pPars )
   SeeAlso     []
 
 ***********************************************************************/
-Abc_Ntk_t * Abc_NtkMiterFraig( Abc_Ntk_t * pNtk, int nBTLimit, int * pRetValue, int * pNumFails )
+Abc_Ntk_t * Abc_NtkMiterFraig( Abc_Ntk_t * pNtk, int nBTLimit, sint64 nInspLimit, int * pRetValue, int * pNumFails, sint64 * pNumConfs, sint64 * pNumInspects )
 {
     Abc_Ntk_t * pNtkNew;
     Fraig_Params_t Params, * pParams = &Params;
@@ -222,6 +248,7 @@ Abc_Ntk_t * Abc_NtkMiterFraig( Abc_Ntk_t * pNtk, int nBTLimit, int * pRetValue,
     pParams->fTryProve  = 0;              // do not try to prove the final miter
     pParams->fDoSparse  = 1;              // try proving sparse functions
     pParams->fVerbose   = 0;
+    pParams->nInspLimit = nInspLimit;
 
     // transform the target into a fraig
     pMan = Abc_NtkToFraig( pNtk, pParams, 0, 0 ); 
@@ -243,6 +270,8 @@ Abc_Ntk_t * Abc_NtkMiterFraig( Abc_Ntk_t * pNtk, int nBTLimit, int * pRetValue,
     // save the return values
     *pRetValue = RetValue;
     *pNumFails = Fraig_ManReadSatFails( pMan );
+    *pNumConfs = Fraig_ManReadConflicts( pMan );
+    *pNumInspects = Fraig_ManReadInspects( pMan );
 
     // delete the fraig manager
     Fraig_ManFree( pMan );

src/base/abci/abcRefactor.c

@@ -111,6 +111,9 @@ int Abc_NtkRefactor( Abc_Ntk_t * pNtk, int nNodeSizeMax, int nConeSizeMax, bool
         // skip the constant node
         if ( Abc_NodeIsConst(pNode) )
             continue;
+        // skip persistant nodes
+        if ( Abc_NodeIsPersistant(pNode) )
+            continue;
         // skip the nodes with many fanouts
         if ( Abc_ObjFanoutNum(pNode) > 1000 )
             continue;

src/base/abci/abcRenode.c

@@ -377,7 +377,7 @@ int Abc_NtkRenodeLimit( Abc_Obj_t * pNode, Vec_Ptr_t * vCone, int nFaninMax )
 ***********************************************************************/
 void Abc_NtkRenodeSetBounds( Abc_Ntk_t * pNtk, int nThresh, int nFaninMax )
 {
-    Vec_Ptr_t * vCone = pNtk->vPtrTemp;
+    Vec_Ptr_t * vCone = Vec_PtrAlloc(10);
     Abc_Obj_t * pNode;
     int i, nFanouts, nConeSize;
 
@@ -414,6 +414,7 @@ void Abc_NtkRenodeSetBounds( Abc_Ntk_t * pNtk, int nThresh, int nFaninMax )
         while ( Abc_NtkRenodeLimit(pNode, vCone, nFaninMax) );
         assert( vCone->nSize <= nFaninMax );  
     }
+    Vec_PtrFree(vCone);
 /*
     // make sure the fanin limit is met
     Abc_NtkForEachNode( pNtk, pNode, i )

src/base/abci/abcRestruct.c

@@ -134,6 +134,9 @@ pManRst->timeCut += clock() - clk;
         // skip the constant node
         if ( Abc_NodeIsConst(pNode) )
             continue;
+        // skip persistant nodes
+        if ( Abc_NodeIsPersistant(pNode) )
+            continue;
         // skip the node if it is inside the tree
 //        if ( Abc_ObjFanoutNum(pNode) < 2 )
 //            continue;

src/base/abci/abcResub.c

@@ -160,6 +160,9 @@ int Abc_NtkResubstitute( Abc_Ntk_t * pNtk, int nCutMax, int nStepsMax, bool fUpd
         // skip the constant node
         if ( Abc_NodeIsConst(pNode) )
             continue;
+        // skip persistant nodes
+        if ( Abc_NodeIsPersistant(pNode) )
+            continue;
         // skip the nodes with many fanouts
         if ( Abc_ObjFanoutNum(pNode) > 1000 )
             continue;
@@ -278,7 +281,7 @@ Abc_ManRes_t * Abc_ManResubStart( int nLeavesMax, int nDivsMax )
         pData = p->vSims->pArray[k];
         for ( i = 0; i < p->nBits; i++ )
             if ( i & (1 << k) )
-                pData[i/32] |= (1 << (i%32));
+                pData[i>>5] |= (1 << (i&31));
     }
     // create the remaining divisors
     p->vDivs1UP  = Vec_PtrAlloc( p->nDivsMax );

src/base/abci/abcRewrite.c

@@ -34,6 +34,7 @@
 
 static Cut_Man_t * Abc_NtkStartCutManForRewrite( Abc_Ntk_t * pNtk );
 static void        Abc_NodePrintCuts( Abc_Obj_t * pNode );
+static void        Abc_ManShowCutCone( Abc_Obj_t * pNode, Vec_Ptr_t * vLeaves );
 
 ////////////////////////////////////////////////////////////////////////
 ///                     FUNCTION DEFINITIONS                         ///
@@ -87,15 +88,39 @@ Rwr_ManAddTimeCuts( pManRwr, clock() - clk );
         // skip the constant node
         if ( Abc_NodeIsConst(pNode) )
             continue;
+        // skip persistant nodes
+        if ( Abc_NodeIsPersistant(pNode) )
+            continue;
         // skip the nodes with many fanouts
         if ( Abc_ObjFanoutNum(pNode) > 1000 )
             continue;
+//printf( "*******Node %d: \n", pNode->Id );
+
         // for each cut, try to resynthesize it
         nGain = Rwr_NodeRewrite( pManRwr, pManCut, pNode, fUpdateLevel, fUseZeros );
         if ( nGain > 0 || nGain == 0 && fUseZeros )
         {
+//            extern void Abc_RwrExpWithCut( Abc_Obj_t * pNode, Vec_Ptr_t * vLeaves );
+
             Dec_Graph_t * pGraph = Rwr_ManReadDecs(pManRwr);
             int fCompl           = Rwr_ManReadCompl(pManRwr);
+
+//            Abc_RwrExpWithCut( pNode, Rwr_ManReadLeaves(pManRwr) );
+
+/*
+            {
+                Abc_Obj_t * pObj;
+                int i;
+                printf( "USING: (" );
+                Vec_PtrForEachEntry( Rwr_ManReadLeaves(pManRwr), pObj, i )
+                    printf( "%d ", Abc_ObjFanoutNum(Abc_ObjRegular(pObj)) );
+                printf( ")   Gain = %d.\n", nGain );
+            }
+*/
+            
+//            if ( nGain > 0 )
+//                Abc_ManShowCutCone( pNode, Rwr_ManReadLeaves(pManRwr) );
+
 /*
             if ( nGain > 0 )
             { // print stats on the MFFC
@@ -209,6 +234,163 @@ void Abc_NodePrintCuts( Abc_Obj_t * pNode )
     }
 }
 
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Abc_ManRewritePrintDivs( Vec_Ptr_t * vDivs, int nLeaves )
+{
+    Abc_Obj_t * pFanin, * pNode, * pRoot;
+    int i, k;
+    pRoot = Vec_PtrEntryLast(vDivs);
+    // print the nodes
+    Vec_PtrForEachEntry( vDivs, pNode, i )
+    {
+        if ( i < nLeaves )
+        {
+            printf( "%6d : %c\n", pNode->Id, 'a'+i );
+            continue;
+        }
+        printf( "%6d : %2d = ", pNode->Id, i );
+        // find the first fanin
+        Vec_PtrForEachEntry( vDivs, pFanin, k )
+            if ( Abc_ObjFanin0(pNode) == pFanin )
+                break;
+        if ( k < nLeaves )
+            printf( "%c", 'a' + k );
+        else
+            printf( "%d", k );
+        printf( "%s ", Abc_ObjFaninC0(pNode)? "\'" : "" );
+        // find the second fanin
+        Vec_PtrForEachEntry( vDivs, pFanin, k )
+            if ( Abc_ObjFanin1(pNode) == pFanin )
+                break;
+        if ( k < nLeaves )
+            printf( "%c", 'a' + k );
+        else
+            printf( "%d", k );
+        printf( "%s ", Abc_ObjFaninC1(pNode)? "\'" : "" );
+        if ( pNode == pRoot )
+            printf( " root" );
+        printf( "\n" );
+    }
+    printf( "\n" );
+}
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Abc_ManShowCutCone_rec( Abc_Obj_t * pNode, Vec_Ptr_t * vDivs )
+{
+    if ( Abc_NodeIsTravIdCurrent(pNode) )
+        return;
+    Abc_NodeSetTravIdCurrent(pNode);
+    Abc_ManShowCutCone_rec( Abc_ObjFanin0(pNode), vDivs );
+    Abc_ManShowCutCone_rec( Abc_ObjFanin1(pNode), vDivs );
+    Vec_PtrPush( vDivs, pNode );
+}
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Abc_ManShowCutCone( Abc_Obj_t * pNode, Vec_Ptr_t * vLeaves )
+{
+    Abc_Ntk_t * pNtk = pNode->pNtk;
+    Abc_Obj_t * pObj;
+    Vec_Ptr_t * vDivs;
+    int i;
+    vDivs = Vec_PtrAlloc( 100 );
+    Abc_NtkIncrementTravId( pNtk );
+    Vec_PtrForEachEntry( vLeaves, pObj, i )
+    {
+        Abc_NodeSetTravIdCurrent( Abc_ObjRegular(pObj) );
+        Vec_PtrPush( vDivs, Abc_ObjRegular(pObj) );
+    }
+    Abc_ManShowCutCone_rec( pNode, vDivs );
+    Abc_ManRewritePrintDivs( vDivs, Vec_PtrSize(vLeaves) );
+    Vec_PtrFree( vDivs );
+}
+
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Abc_RwrExpWithCut_rec( Abc_Obj_t * pNode, Vec_Ptr_t * vLeaves, int fUseA )
+{
+    if ( Vec_PtrFind(vLeaves, pNode) >= 0 || Vec_PtrFind(vLeaves, Abc_ObjNot(pNode)) >= 0 )
+    {
+        if ( fUseA )
+            Abc_ObjRegular(pNode)->fMarkA = 1;
+        else
+            Abc_ObjRegular(pNode)->fMarkB = 1;
+        return;
+    }
+    assert( Abc_ObjIsNode(pNode) );
+    Abc_RwrExpWithCut_rec( Abc_ObjFanin0(pNode), vLeaves, fUseA );
+    Abc_RwrExpWithCut_rec( Abc_ObjFanin1(pNode), vLeaves, fUseA );
+}
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Abc_RwrExpWithCut( Abc_Obj_t * pNode, Vec_Ptr_t * vLeaves )
+{
+    Abc_Obj_t * pObj;
+    int i, CountA, CountB;
+    Abc_RwrExpWithCut_rec( Abc_ObjFanin0(pNode), vLeaves, 1 );
+    Abc_RwrExpWithCut_rec( Abc_ObjFanin1(pNode), vLeaves, 0 );
+    CountA = CountB = 0;
+    Vec_PtrForEachEntry( vLeaves, pObj, i )
+    {
+        CountA += Abc_ObjRegular(pObj)->fMarkA;
+        CountB += Abc_ObjRegular(pObj)->fMarkB;
+        Abc_ObjRegular(pObj)->fMarkA = 0;
+        Abc_ObjRegular(pObj)->fMarkB = 0;
+    }
+    printf( "(%d,%d:%d) ", CountA, CountB, CountA+CountB-Vec_PtrSize(vLeaves) );
+}
+
+
 ////////////////////////////////////////////////////////////////////////
 ///                       END OF FILE                                ///
 ////////////////////////////////////////////////////////////////////////

src/base/abci/abcRr.c

@@ -105,6 +105,9 @@ int Abc_NtkRR( Abc_Ntk_t * pNtk, int nFaninLevels, int nFanoutLevels, int fUseFa
     p->nFanoutLevels = nFanoutLevels;
     p->nNodesOld     = Abc_NtkNodeNum(pNtk);
     p->nLevelsOld    = Abc_AigGetLevelNum(pNtk);
+    // remember latch values
+    Abc_NtkForEachLatch( pNtk, pNode, i )
+        pNode->pNext = pNode->pData;
     // go through the nodes
     Abc_NtkCleanCopy(pNtk);
     nNodes = Abc_NtkObjNumMax(pNtk);
@@ -119,6 +122,9 @@ int Abc_NtkRR( Abc_Ntk_t * pNtk, int nFaninLevels, int nFanoutLevels, int fUseFa
         // skip the constant node
         if ( Abc_NodeIsConst(pNode) )
             continue;
+        // skip persistant nodes
+        if ( Abc_NodeIsPersistant(pNode) )
+            continue;
         // skip the nodes with many fanouts
         if ( Abc_ObjFanoutNum(pNode) > 1000 )
             continue;
@@ -209,6 +215,9 @@ int Abc_NtkRR( Abc_Ntk_t * pNtk, int nFaninLevels, int nFanoutLevels, int fUseFa
     if ( fVerbose )
         Abc_RRManPrintStats( p );
     Abc_RRManStop( p );
+    // restore latch values
+    Abc_NtkForEachLatch( pNtk, pNode, i )
+        pNode->pData = pNode->pNext, pNode->pNext = NULL;
     // put the nodes into the DFS order and reassign their IDs
     Abc_NtkReassignIds( pNtk );
     Abc_NtkGetLevelNum( pNtk );
@@ -692,6 +701,7 @@ Abc_Ntk_t * Abc_NtkWindow( Abc_Ntk_t * pNtk, Vec_Ptr_t * vLeaves, Vec_Ptr_t * vC
     // add the PI/PO names
     Abc_NtkAddDummyPiNames( pNtkNew );
     Abc_NtkAddDummyPoNames( pNtkNew );
+    Abc_NtkAddDummyAssertNames( pNtkNew );
     // check
     if ( fCheck && !Abc_NtkCheck( pNtkNew ) )
     {

src/base/abci/abcSat.c

@@ -42,12 +42,17 @@ static nMuxes;
   SeeAlso     []
 
 ***********************************************************************/
-int Abc_NtkMiterSat( Abc_Ntk_t * pNtk, int nConfLimit, int nImpLimit, int fJFront, int fVerbose )
+int Abc_NtkMiterSat( Abc_Ntk_t * pNtk, sint64 nConfLimit, sint64 nInsLimit, int fJFront, int fVerbose, sint64 * pNumConfs, sint64 * pNumInspects )
 {
     solver * pSat;
     lbool   status;
     int RetValue, clk;
 
+    if ( pNumConfs )
+        *pNumConfs = 0;
+    if ( pNumInspects )
+        *pNumInspects = 0;
+
     assert( Abc_NtkIsStrash(pNtk) );
     assert( Abc_NtkLatchNum(pNtk) == 0 );
 
@@ -78,7 +83,7 @@ int Abc_NtkMiterSat( Abc_Ntk_t * pNtk, int nConfLimit, int nImpLimit, int fJFron
     clk = clock();
     if ( fVerbose )
         pSat->verbosity = 1;
-    status = solver_solve( pSat, NULL, NULL, nConfLimit, nImpLimit );
+    status = solver_solve( pSat, NULL, NULL, (sint64)nConfLimit, (sint64)nInsLimit );
     if ( status == l_Undef )
     {
 //        printf( "The problem timed out.\n" );
@@ -97,6 +102,7 @@ int Abc_NtkMiterSat( Abc_Ntk_t * pNtk, int nConfLimit, int nImpLimit, int fJFron
     else
         assert( 0 );
 //    PRT( "SAT solver time", clock() - clk );
+//    printf( "The number of conflicts = %d.\n", (int)pSat->solver_stats.conflicts );
 
     // if the problem is SAT, get the counterexample
     if ( status == l_True )
@@ -109,6 +115,12 @@ int Abc_NtkMiterSat( Abc_Ntk_t * pNtk, int nConfLimit, int nImpLimit, int fJFron
     // free the solver
     if ( fVerbose )
         Asat_SatPrintStats( stdout, pSat );
+
+    if ( pNumConfs )
+        *pNumConfs = (int)pSat->solver_stats.conflicts;
+    if ( pNumInspects )
+        *pNumInspects = (int)pSat->solver_stats.inspects;
+
     solver_delete( pSat );
     return RetValue;
 }
@@ -401,6 +413,7 @@ int Abc_NtkMiterSatCreateInt( solver * pSat, Abc_Ntk_t * pNtk, int fJFront )
     Vec_Vec_t * vCircuit;
     int i, k, fUseMuxes = 1;
     int clk1 = clock(), clk;
+    int fOrderCiVarsFirst = 0;
 
     assert( Abc_NtkIsStrash(pNtk) );
 
@@ -431,6 +444,7 @@ int Abc_NtkMiterSatCreateInt( solver * pSat, Abc_Ntk_t * pNtk, int fJFront )
         Vec_PtrPush( vNodes, pNode );
     }
 */
+
     // collect the nodes that need clauses and top-level assignments
     Abc_NtkForEachCo( pNtk, pNode, i )
     {
@@ -526,6 +540,21 @@ int Abc_NtkMiterSatCreateInt( solver * pSat, Abc_Ntk_t * pNtk, int fJFront )
         }
     }
 
+    // set preferred variables
+    if ( fOrderCiVarsFirst )
+    {
+        int * pPrefVars = ALLOC( int, Abc_NtkCiNum(pNtk) );
+        int nVars = 0;
+        Abc_NtkForEachCi( pNtk, pNode, i )
+        {
+            if ( pNode->fMarkA == 0 )
+                continue;
+            pPrefVars[nVars++] = (int)pNode->pCopy;
+        }
+        nVars = ABC_MIN( nVars, 10 );
+        Asat_SolverSetPrefVars( pSat, pPrefVars, nVars );
+    }
+
     // create the variable order
     if ( fJFront )
     {

src/base/abci/abcSweep.c

@@ -571,12 +571,13 @@ int Abc_NtkSweep( Abc_Ntk_t * pNtk, int fVerbose )
 ***********************************************************************/
 void Abc_NodeSweep( Abc_Obj_t * pNode, int fVerbose )
 {
-    Vec_Ptr_t * vFanout = pNode->pNtk->vPtrTemp;
     Abc_Obj_t * pFanout, * pDriver;
+    Vec_Ptr_t * vFanout;
     int i;
     assert( Abc_ObjFaninNum(pNode) < 2 );
     assert( Abc_ObjFanoutNum(pNode) > 0 );
     // iterate through the fanouts
+    vFanout = Vec_PtrAlloc( Abc_ObjFanoutNum(pNode) );
     Abc_NodeCollectFanouts( pNode, vFanout );
     Vec_PtrForEachEntry( vFanout, pFanout, i )
     {
@@ -607,6 +608,7 @@ void Abc_NodeSweep( Abc_Obj_t * pNode, int fVerbose )
             Abc_ObjPatchFanin( pFanout, pNode, pDriver );
         }
     }
+    Vec_PtrFree( vFanout );
 }
 
 /**Function*************************************************************

src/base/abci/abcTrace.c

@@ -148,7 +148,7 @@ void Abc_HManStart()
         pData = p->vSims->pArray[k];
         for ( i = 0; i < p->nBits; i++ )
             if ( i & (1 << k) )
-                pData[i/32] |= (1 << (i%32));
+                pData[i>>5] |= (1 << (i&31));
     }
     // allocate storage for the nodes
     p->pMmObj = Extra_MmFixedStart( sizeof(Abc_HObj_t) );

src/base/abci/abcVanEijk.c

@@ -544,8 +544,6 @@ Abc_Ntk_t * Abc_NtkVanEijkFrames( Abc_Ntk_t * pNtk, Vec_Ptr_t * vCorresp, int nF
     {
         pLatchNew = Abc_NtkLatch(pNtkFrames, i);
         Abc_ObjAddFanin( pLatchNew, pLatch->pCopy );
-        Vec_PtrPush( pNtkFrames->vCis, pLatchNew );
-        Vec_PtrPush( pNtkFrames->vCos, pLatchNew );
         Abc_NtkLogicStoreName( pLatchNew, Abc_ObjName(pLatch) );
         pLatch->pNext = NULL;
     }

src/base/abci/abcVerify.c

@@ -44,7 +44,7 @@ static void  Abc_NtkVerifyReportErrorSeq( Abc_Ntk_t * pNtk1, Abc_Ntk_t * pNtk2,
   SeeAlso     []
 
 ***********************************************************************/
-void Abc_NtkCecSat( Abc_Ntk_t * pNtk1, Abc_Ntk_t * pNtk2, int nConfLimit, int nImpLimit )
+void Abc_NtkCecSat( Abc_Ntk_t * pNtk1, Abc_Ntk_t * pNtk2, int nConfLimit, int nInsLimit )
 {
     Abc_Ntk_t * pMiter;
     Abc_Ntk_t * pCnf;
@@ -85,7 +85,7 @@ void Abc_NtkCecSat( Abc_Ntk_t * pNtk1, Abc_Ntk_t * pNtk2, int nConfLimit, int nI
     }
 
     // solve the CNF using the SAT solver
-    RetValue = Abc_NtkMiterSat( pCnf, nConfLimit, nImpLimit, 0, 0 );
+    RetValue = Abc_NtkMiterSat( pCnf, (sint64)nConfLimit, (sint64)nInsLimit, 0, 0, NULL, NULL );
     if ( RetValue == -1 )
         printf( "Networks are undecided (SAT solver timed out).\n" );
     else if ( RetValue == 0 )
@@ -178,7 +178,14 @@ void Abc_NtkCecFraig( Abc_Ntk_t * pNtk1, Abc_Ntk_t * pNtk2, int nSeconds, int fV
     if ( RetValue == -1 )
         printf( "Networks are undecided (resource limits is reached).\n" );
     else if ( RetValue == 0 )
-        printf( "Networks are NOT EQUIVALENT.\n" );
+    {
+        int * pSimInfo = Abc_NtkVerifySimulatePattern( pMiter, pMiter->pModel );
+        if ( pSimInfo[0] != 1 )
+            printf( "ERROR in Abc_NtkMiterProve(): Generated counter-example is invalid.\n" );
+        else
+            printf( "Networks are NOT EQUIVALENT.\n" );
+        free( pSimInfo );
+    }
     else
         printf( "Networks are equivalent.\n" );
     if ( pMiter->pModel )
@@ -197,7 +204,7 @@ void Abc_NtkCecFraig( Abc_Ntk_t * pNtk1, Abc_Ntk_t * pNtk2, int nSeconds, int fV
   SeeAlso     []
 
 ***********************************************************************/
-void Abc_NtkSecSat( Abc_Ntk_t * pNtk1, Abc_Ntk_t * pNtk2, int nConfLimit, int nImpLimit, int nFrames )
+void Abc_NtkSecSat( Abc_Ntk_t * pNtk1, Abc_Ntk_t * pNtk2, int nConfLimit, int nInsLimit, int nFrames )
 {
     Abc_Ntk_t * pMiter;
     Abc_Ntk_t * pFrames;
@@ -257,7 +264,7 @@ void Abc_NtkSecSat( Abc_Ntk_t * pNtk1, Abc_Ntk_t * pNtk2, int nConfLimit, int nI
     }
 
     // solve the CNF using the SAT solver
-    RetValue = Abc_NtkMiterSat( pCnf, nConfLimit, nImpLimit, 0, 0 );
+    RetValue = Abc_NtkMiterSat( pCnf, (sint64)nConfLimit, (sint64)nInsLimit, 0, 0, NULL, NULL );
     if ( RetValue == -1 )
         printf( "Networks are undecided (SAT solver timed out).\n" );
     else if ( RetValue == 0 )
@@ -709,6 +716,52 @@ void Abc_NtkVerifyReportErrorSeq( Abc_Ntk_t * pNtk1, Abc_Ntk_t * pNtk2, int * pM
     if ( fRemove2 ) Abc_NtkDelete( pNtk2 );
 }
 
+/**Function*************************************************************
+
+  Synopsis    [Simulates buggy miter emailed by Mike.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Abc_NtkSimulteBuggyMiter( Abc_Ntk_t * pNtk )
+{
+    Abc_Obj_t * pObj;
+    int i;
+    int * pModel1, * pModel2, * pResult1, * pResult2;
+    char * vPiValues1 = "01001011100000000011010110101000000";
+    char * vPiValues2 = "11001101011101011111110100100010001";
+
+    assert( strlen(vPiValues1) == (unsigned)Abc_NtkPiNum(pNtk) );
+    assert( 1 == Abc_NtkPoNum(pNtk) );
+
+    pModel1 = ALLOC( int, Abc_NtkCiNum(pNtk) );
+    Abc_NtkForEachPi( pNtk, pObj, i )
+        pModel1[i] = vPiValues1[i] - '0';
+    Abc_NtkForEachLatch( pNtk, pObj, i )
+        pModel1[Abc_NtkPiNum(pNtk)+i] = ((int)pObj->pData) - 1;
+
+    pResult1 = Abc_NtkVerifySimulatePattern( pNtk, pModel1 );
+    printf( "Value = %d\n", pResult1[0] );
+
+    pModel2 = ALLOC( int, Abc_NtkCiNum(pNtk) );
+    Abc_NtkForEachPi( pNtk, pObj, i )
+        pModel2[i] = vPiValues2[i] - '0';
+    Abc_NtkForEachLatch( pNtk, pObj, i )
+        pModel2[Abc_NtkPiNum(pNtk)+i] = pResult1[Abc_NtkPoNum(pNtk)+i];
+
+    pResult2 = Abc_NtkVerifySimulatePattern( pNtk, pModel2 );
+    printf( "Value = %d\n", pResult2[0] );
+
+    free( pModel1 );
+    free( pModel2 );
+    free( pResult1 );
+    free( pResult2 );
+}
+
 
 ////////////////////////////////////////////////////////////////////////
 ///                       END OF FILE                                ///

src/base/abci/module.make

@@ -11,6 +11,7 @@ SRC +=    src/base/abci/abc.c \
     src/base/abci/abcFraig.c \
         src/base/abci/abcFxu.c \
         src/base/abci/abcGen.c \
+    src/base/abci/abcIvy.c \
     src/base/abci/abcMap.c \
     src/base/abci/abcMiter.c \
     src/base/abci/abcNtbdd.c \

src/base/io/io.h

@@ -68,6 +68,7 @@ extern Abc_Ntk_t *        Io_ReadPla( char * pFileName, int fCheck );
 /*=== abcUtil.c ==========================================================*/
 extern Abc_Obj_t *        Io_ReadCreatePi( Abc_Ntk_t * pNtk, char * pName );
 extern Abc_Obj_t *        Io_ReadCreatePo( Abc_Ntk_t * pNtk, char * pName );
+extern Abc_Obj_t *        Io_ReadCreateAssert( Abc_Ntk_t * pNtk, char * pName );
 extern Abc_Obj_t *        Io_ReadCreateLatch( Abc_Ntk_t * pNtk, char * pNetLI, char * pNetLO );
 extern Abc_Obj_t *        Io_ReadCreateNode( Abc_Ntk_t * pNtk, char * pNameOut, char * pNamesIn[], int nInputs );
 extern Abc_Obj_t *        Io_ReadCreateConst( Abc_Ntk_t * pNtk, char * pName, bool fConst1 );

src/base/io/ioReadBaf.c

@@ -100,8 +100,6 @@ Abc_Ntk_t * Io_ReadBaf( char * pFileName, int fCheck )
         pObj = Abc_NtkCreateLatch(pNtkNew);
         Abc_NtkLogicStoreName( pObj, pCur );  while ( *pCur++ ); 
         Vec_PtrPush( vNodes, pObj );
-        Vec_PtrPush( pNtkNew->vCis, pObj );
-        Vec_PtrPush( pNtkNew->vCos, pObj );
     }
 
     // get the pointer to the beginning of the node array

src/base/io/ioReadBlif.c

@@ -33,6 +33,7 @@ struct Io_ReadBlif_t_
     char *               pFileName;    // the name of the file
     Extra_FileReader_t * pReader;      // the input file reader
     // current processing info
+    Abc_Ntk_t *          pNtkMaster;   // the primary network
     Abc_Ntk_t *          pNtkCur;      // the primary network
     int                  LineCur;      // the line currently parsed
     // temporary storage for tokens
@@ -54,6 +55,7 @@ static Abc_Ntk_t * Io_ReadBlifNetwork( Io_ReadBlif_t * p );
 static Abc_Ntk_t * Io_ReadBlifNetworkOne( Io_ReadBlif_t * p );
 static int Io_ReadBlifNetworkInputs( Io_ReadBlif_t * p, Vec_Ptr_t * vTokens );
 static int Io_ReadBlifNetworkOutputs( Io_ReadBlif_t * p, Vec_Ptr_t * vTokens );
+static int Io_ReadBlifNetworkAsserts( Io_ReadBlif_t * p, Vec_Ptr_t * vTokens );
 static int Io_ReadBlifNetworkLatch( Io_ReadBlif_t * p, Vec_Ptr_t * vTokens );
 static int Io_ReadBlifNetworkNames( Io_ReadBlif_t * p, Vec_Ptr_t ** pvTokens );
 static int Io_ReadBlifNetworkGate( Io_ReadBlif_t * p, Vec_Ptr_t * vTokens );
@@ -151,7 +153,7 @@ Abc_Ntk_t * Io_ReadBlifNetwork( Io_ReadBlif_t * p )
         // add this network as part of the hierarchy
         if ( pNtkMaster == NULL ) // no master network so far
         {
-            pNtkMaster = pNtk;
+            p->pNtkMaster = pNtkMaster = pNtk;
             continue;
         }
         // make sure hierarchy does not have the network with this name
@@ -222,11 +224,12 @@ Abc_Ntk_t * Io_ReadBlifNetworkOne( Io_ReadBlif_t * p )
     }
 
     // read the inputs/outputs
+    if ( p->pNtkMaster == NULL )
     pProgress = Extra_ProgressBarStart( stdout, Extra_FileReaderGetFileSize(p->pReader) );
     fTokensReady = fStatus = 0;
     for ( iLine = 0; fTokensReady || (p->vTokens = Io_ReadBlifGetTokens(p)); iLine++ )
     {
-        if ( iLine % 1000 == 0 )
+        if ( p->pNtkMaster == NULL && iLine % 1000 == 0 )
         Extra_ProgressBarUpdate( pProgress, Extra_FileReaderGetCurPosition(p->pReader), NULL );
 
         // consider different line types
@@ -242,6 +245,8 @@ Abc_Ntk_t * Io_ReadBlifNetworkOne( Io_ReadBlif_t * p )
             fStatus = Io_ReadBlifNetworkInputs( p, p->vTokens );
         else if ( !strcmp( pDirective, ".outputs" ) )
             fStatus = Io_ReadBlifNetworkOutputs( p, p->vTokens );
+        else if ( !strcmp( pDirective, ".asserts" ) )
+            fStatus = Io_ReadBlifNetworkAsserts( p, p->vTokens );
         else if ( !strcmp( pDirective, ".input_arrival" ) )
             fStatus = Io_ReadBlifNetworkInputArrival( p, p->vTokens );
         else if ( !strcmp( pDirective, ".default_input_arrival" ) )
@@ -257,8 +262,10 @@ Abc_Ntk_t * Io_ReadBlifNetworkOne( Io_ReadBlif_t * p )
         }
         else if ( !strcmp( pDirective, ".blackbox" ) )
         {
-            pNtk->ntkType = ABC_NTK_BLACKBOX;
+            pNtk->ntkType = ABC_NTK_NETLIST;
             pNtk->ntkFunc = ABC_FUNC_BLACKBOX;
+            Extra_MmFlexStop( pNtk->pManFunc, 0 );
+            pNtk->pManFunc = NULL;
         }
         else
             printf( "%s (line %d): Skipping directive \"%s\".\n", p->pFileName, 
@@ -268,6 +275,7 @@ Abc_Ntk_t * Io_ReadBlifNetworkOne( Io_ReadBlif_t * p )
         if ( fStatus == 1 )
             return NULL;
     }
+    if ( p->pNtkMaster == NULL )
     Extra_ProgressBarStop( pProgress );
     return pNtk;
 }
@@ -321,6 +329,25 @@ int Io_ReadBlifNetworkOutputs( Io_ReadBlif_t * p, Vec_Ptr_t * vTokens )
   SeeAlso     []
 
 ***********************************************************************/
+int Io_ReadBlifNetworkAsserts( Io_ReadBlif_t * p, Vec_Ptr_t * vTokens )
+{
+    int i;
+    for ( i = 1; i < vTokens->nSize; i++ )
+        Io_ReadCreateAssert( p->pNtkCur, vTokens->pArray[i] );
+    return 0;
+}
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
 int Io_ReadBlifNetworkLatch( Io_ReadBlif_t * p, Vec_Ptr_t * vTokens )
 {
     Abc_Ntk_t * pNtk = p->pNtkCur;
@@ -340,7 +367,7 @@ int Io_ReadBlifNetworkLatch( Io_ReadBlif_t * p, Vec_Ptr_t * vTokens )
         Abc_LatchSetInitDc( pLatch );
     else
     {
-        ResetValue = atoi(vTokens->pArray[3]);
+        ResetValue = atoi(vTokens->pArray[vTokens->nSize-1]);
         if ( ResetValue != 0 && ResetValue != 1 && ResetValue != 2 )
         {
             p->LineCur = Extra_FileReaderGetLineNumber(p->pReader, 0);
@@ -870,50 +897,55 @@ int Io_ReadBlifNetworkConnectBoxesOneBox( Io_ReadBlif_t * p, Abc_Obj_t * pBox, s
     // create the fanins of the box
     Abc_NtkForEachPi( pNtkModel, pObj, i )
         pObj->pCopy = NULL;
-    Vec_PtrForEachEntryStart( pNames, pName, i, 1 )
+    if ( Abc_NtkPiNum(pNtkModel) == 0 )
+        Start = 1;
+    else
     {
-        pActual = Io_ReadBlifCleanName(pName);
-        if ( pActual == NULL )
-        {
-            p->LineCur = (int)pBox->pCopy;
-            sprintf( p->sError, "Cannot parse formal/actual name pair \"%s\".", pName );
-            Io_ReadBlifPrintErrorMessage( p );
-            return 1;
-        }
-        Length = pActual - pName - 1;
-        pName[Length] = 0;
-        // find the PI net with this name
-        pObj = Abc_NtkFindNet( pNtkModel, pName );
-        if ( pObj == NULL )
-        {
-            p->LineCur = (int)pBox->pCopy;
-            sprintf( p->sError, "Cannot find formal input \"%s\" as an PI of model \"%s\".", pName, Vec_PtrEntry(pNames, 0) );
-            Io_ReadBlifPrintErrorMessage( p );
-            return 1;
-        }
-        // get the PI
-        pObj = Abc_ObjFanin0(pObj);
-        // quit if this is not a PI net
-        if ( !Abc_ObjIsPi(pObj) )
-        {
-            pName[Length] = '=';
-            Start = i;
-            break;
-        }
-        // remember the actual name in the net
-        if ( pObj->pCopy != NULL )
-        {
-            p->LineCur = (int)pBox->pCopy;
-            sprintf( p->sError, "Formal input \"%s\" is used more than once.", pName );
-            Io_ReadBlifPrintErrorMessage( p );
-            return 1;
-        }
-        pObj->pCopy = (void *)pActual;
-        // quit if we processed all PIs
-        if ( i == Abc_NtkPiNum(pNtkModel) )
+        Vec_PtrForEachEntryStart( pNames, pName, i, 1 )
         {
-            Start = i+1;
-            break;
+            pActual = Io_ReadBlifCleanName(pName);
+            if ( pActual == NULL )
+            {
+                p->LineCur = (int)pBox->pCopy;
+                sprintf( p->sError, "Cannot parse formal/actual name pair \"%s\".", pName );
+                Io_ReadBlifPrintErrorMessage( p );
+                return 1;
+            }
+            Length = pActual - pName - 1;
+            pName[Length] = 0;
+            // find the PI net with this name
+            pObj = Abc_NtkFindNet( pNtkModel, pName );
+            if ( pObj == NULL )
+            {
+                p->LineCur = (int)pBox->pCopy;
+                sprintf( p->sError, "Cannot find formal input \"%s\" as an PI of model \"%s\".", pName, Vec_PtrEntry(pNames, 0) );
+                Io_ReadBlifPrintErrorMessage( p );
+                return 1;
+            }
+            // get the PI
+            pObj = Abc_ObjFanin0(pObj);
+            // quit if this is not a PI net
+            if ( !Abc_ObjIsPi(pObj) )
+            {
+                pName[Length] = '=';
+                Start = i;
+                break;
+            }
+            // remember the actual name in the net
+            if ( pObj->pCopy != NULL )
+            {
+                p->LineCur = (int)pBox->pCopy;
+                sprintf( p->sError, "Formal input \"%s\" is used more than once.", pName );
+                Io_ReadBlifPrintErrorMessage( p );
+                return 1;
+            }
+            pObj->pCopy = (void *)pActual;
+            // quit if we processed all PIs
+            if ( i == Abc_NtkPiNum(pNtkModel) )
+            {
+                Start = i+1;
+                break;
+            }
         }
     }
     // create the fanins of the box
@@ -986,6 +1018,8 @@ int Io_ReadBlifNetworkConnectBoxesOneBox( Io_ReadBlif_t * p, Abc_Obj_t * pBox, s
         pObj->pCopy = NULL;
 
     // remove the array of names, assign the pointer to the model
+    Vec_PtrForEachEntry( pBox->pData, pName, i )
+        free( pName );
     Vec_PtrFree( pBox->pData );
     pBox->pData = pNtkModel;
     return 0;

src/base/io/ioUtil.c

@@ -80,6 +80,31 @@ Abc_Obj_t * Io_ReadCreatePo( Abc_Ntk_t * pNtk, char * pName )
 
 /**Function*************************************************************
 
+  Synopsis    [Creates PO terminal and net.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Abc_Obj_t * Io_ReadCreateAssert( Abc_Ntk_t * pNtk, char * pName )
+{
+    Abc_Obj_t * pNet, * pTerm;
+    // get the PO net
+    pNet  = Abc_NtkFindNet( pNtk, pName );
+    if ( pNet && Abc_ObjFaninNum(pNet) == 0 )
+        printf( "Warning: Assert \"%s\" appears twice in the list.\n", pName );
+    pNet  = Abc_NtkFindOrCreateNet( pNtk, pName );
+    // add the PO node
+    pTerm = Abc_NtkCreateAssert( pNtk );
+    Abc_ObjAddFanin( pTerm, pNet );
+    return pTerm;
+}
+
+/**Function*************************************************************
+
   Synopsis    [Create a latch with the given input/output.]
 
   Description [By default, the latch value is unknown (ABC_INIT_NONE).]

src/base/io/ioWriteBlif.c

@@ -30,6 +30,7 @@ static void Io_NtkWrite( FILE * pFile, Abc_Ntk_t * pNtk, int fWriteLatches );
 static void Io_NtkWriteOne( FILE * pFile, Abc_Ntk_t * pNtk, int fWriteLatches );
 static void Io_NtkWritePis( FILE * pFile, Abc_Ntk_t * pNtk, int fWriteLatches );
 static void Io_NtkWritePos( FILE * pFile, Abc_Ntk_t * pNtk, int fWriteLatches );
+static void Io_NtkWriteAsserts( FILE * pFile, Abc_Ntk_t * pNtk );
 static void Io_NtkWriteNodeGate( FILE * pFile, Abc_Obj_t * pNode );
 static void Io_NtkWriteNodeFanins( FILE * pFile, Abc_Obj_t * pNode );
 static void Io_NtkWriteNode( FILE * pFile, Abc_Obj_t * pNode );
@@ -115,7 +116,7 @@ void Io_WriteBlifNetlist( Abc_Ntk_t * pNtk, char * FileName, int fWriteLatches )
 void Io_NtkWrite( FILE * pFile, Abc_Ntk_t * pNtk, int fWriteLatches )
 {
     Abc_Ntk_t * pExdc;
-    assert( Abc_NtkIsNetlist(pNtk) || Abc_NtkIsBlackbox(pNtk) );
+    assert( Abc_NtkIsNetlist(pNtk) );
     // write the model name
     fprintf( pFile, ".model %s\n", Abc_NtkName(pNtk) );
     // write the network
@@ -159,8 +160,16 @@ void Io_NtkWriteOne( FILE * pFile, Abc_Ntk_t * pNtk, int fWriteLatches )
     Io_NtkWritePos( pFile, pNtk, fWriteLatches );
     fprintf( pFile, "\n" );
 
+    // write the assertions
+    if ( Abc_NtkAssertNum(pNtk) )
+    {
+        fprintf( pFile, ".asserts" );
+        Io_NtkWriteAsserts( pFile, pNtk );
+        fprintf( pFile, "\n" );
+    }
+
     // write the blackbox
-    if ( Abc_NtkIsBlackbox( pNtk ) )
+    if ( Abc_NtkHasBlackbox( pNtk ) )
     {
         fprintf( pFile, ".blackbox\n" );
         return;
@@ -296,6 +305,8 @@ void Io_NtkWritePos( FILE * pFile, Abc_Ntk_t * pNtk, int fWriteLatches )
     {
         Abc_NtkForEachCo( pNtk, pTerm, i )
         {
+            if ( Abc_ObjIsAssert(pTerm) )
+                continue;
             pNet = Abc_ObjFanin0(pTerm);
             // get the line length after this name is written
             AddedLength = strlen(Abc_ObjName(pNet)) + 1;
@@ -313,6 +324,45 @@ void Io_NtkWritePos( FILE * pFile, Abc_Ntk_t * pNtk, int fWriteLatches )
     }
 }
 
+/**Function*************************************************************
+
+  Synopsis    [Writes the assertion list.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Io_NtkWriteAsserts( FILE * pFile, Abc_Ntk_t * pNtk )
+{
+    Abc_Obj_t * pTerm, * pNet;
+    int LineLength;
+    int AddedLength;
+    int NameCounter;
+    int i;
+
+    LineLength  = 8;
+    NameCounter = 0;
+
+    Abc_NtkForEachAssert( 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*************************************************************
 

src/base/io/ioWriteVer.c

@@ -33,7 +33,6 @@ static void Io_WriteVerilogWires( FILE * pFile, Abc_Ntk_t * pNtk, int Start );
 static void Io_WriteVerilogRegs( FILE * pFile, Abc_Ntk_t * pNtk, int Start );
 static void Io_WriteVerilogGates( FILE * pFile, Abc_Ntk_t * pNtk );
 static void Io_WriteVerilogNodes( FILE * pFile, Abc_Ntk_t * pNtk );
-static void Io_WriteVerilogArgs( FILE * pFile, Abc_Obj_t * pObj, int nInMax, int fPadZeros );
 static void Io_WriteVerilogLatches( FILE * pFile, Abc_Ntk_t * pNtk );
 static int Io_WriteVerilogCheckNtk( Abc_Ntk_t * pNtk );
 static char * Io_WriteVerilogGetName( Abc_Obj_t * pObj );
@@ -225,7 +224,7 @@ void Io_WriteVerilogWires( FILE * pFile, Abc_Ntk_t * pNtk, int Start )
     int i, Counter, nNodes;
 
     // count the number of wires
-    nNodes = 0;
+    nNodes = Abc_NtkLatchNum(pNtk);
     Abc_NtkForEachNode( pNtk, pTerm, i )
     {
         if ( i == 0 ) 
@@ -261,6 +260,24 @@ void Io_WriteVerilogWires( FILE * pFile, Abc_Ntk_t * pNtk, int Start )
         LineLength += AddedLength;
         NameCounter++;
     }
+    Abc_NtkForEachLatch( pNtk, pTerm, i )
+    {
+        pNet = Abc_ObjFanin0(pTerm);
+        Counter++;
+        // get the line length after this name is written
+        AddedLength = strlen(Abc_ObjName(pNet)) + 2;
+        if ( NameCounter && LineLength + AddedLength + 3 > IO_WRITE_LINE_LENGTH )
+        { // write the line extender
+            fprintf( pFile, "\n   " );
+            // reset the line length
+            LineLength  = 3;
+            NameCounter = 0;
+        }
+        fprintf( pFile, " %s%s", Io_WriteVerilogGetName(pNet), (Counter==nNodes)? "" : "," );
+        LineLength += AddedLength;
+        NameCounter++;
+    }
+    assert( Counter == nNodes );
 }
 
 /**Function*************************************************************
@@ -325,12 +342,15 @@ void Io_WriteVerilogLatches( FILE * pFile, Abc_Ntk_t * pNtk )
     int i;
     Abc_NtkForEachLatch( pNtk, pLatch, i )
     {
+//        fprintf( pFile, "  always@(posedge  gclk) begin %s",     Abc_ObjName(Abc_ObjFanout0(pLatch)) );
+        fprintf( pFile, "  always begin %s",     Abc_ObjName(Abc_ObjFanout0(pLatch)) );
+        fprintf( pFile, " = %s; end\n", Abc_ObjName(Abc_ObjFanin0(pLatch)) );
         if ( Abc_LatchInit(pLatch) == ABC_INIT_ZERO )
-            fprintf( pFile, "  initial begin %s = 1\'b0; end\n", Abc_ObjName(Abc_ObjFanout0(pLatch)) );
+//            fprintf( pFile, "  initial begin %s = 1\'b0; end\n", Abc_ObjName(Abc_ObjFanout0(pLatch)) );
+            fprintf( pFile, "  initial begin %s = 0; end\n", Abc_ObjName(Abc_ObjFanout0(pLatch)) );
         else if ( Abc_LatchInit(pLatch) == ABC_INIT_ONE )
-            fprintf( pFile, "  initial begin %s = 1\'b1; end\n", Abc_ObjName(Abc_ObjFanout0(pLatch)) );
-        fprintf( pFile, "  always@(posedge  gclk) begin %s",     Abc_ObjName(Abc_ObjFanout0(pLatch)) );
-        fprintf( pFile, " = %s; end\n", Abc_ObjName(Abc_ObjFanin0(pLatch)) );
+//            fprintf( pFile, "  initial begin %s = 1\'b1; end\n", Abc_ObjName(Abc_ObjFanout0(pLatch)) );
+            fprintf( pFile, "  initial begin %s = 1; end\n", Abc_ObjName(Abc_ObjFanout0(pLatch)) );
     }
 }
 
@@ -378,7 +398,7 @@ void Io_WriteVerilogGates( FILE * pFile, Abc_Ntk_t * pNtk )
   SeeAlso     []
 
 ***********************************************************************/
-void Io_WriteVerilogNodes( FILE * pFile, Abc_Ntk_t * pNtk )
+void Io_WriteVerilogNodes2( FILE * pFile, Abc_Ntk_t * pNtk )
 {
     Abc_Obj_t * pObj, * pFanin;
     int i, k, nFanins;
@@ -390,7 +410,8 @@ void Io_WriteVerilogNodes( FILE * pFile, Abc_Ntk_t * pNtk )
         nFanins = Abc_ObjFaninNum(pObj);
         if ( nFanins == 0 )
         {
-            fprintf( pFile, "  assign %s = 1'b%d;\n", Io_WriteVerilogGetName(Abc_ObjFanout0(pObj)), !Abc_SopIsComplement(pObj->pData) );
+//            fprintf( pFile, "  assign %s = 1'b%d;\n", Io_WriteVerilogGetName(Abc_ObjFanout0(pObj)), !Abc_SopIsComplement(pObj->pData) );
+            fprintf( pFile, "  assign %s = %d;\n", Io_WriteVerilogGetName(Abc_ObjFanout0(pObj)), !Abc_SopIsComplement(pObj->pData) );
             continue;
         }
         if ( nFanins == 1 )
@@ -410,7 +431,7 @@ void Io_WriteVerilogNodes( FILE * pFile, Abc_Ntk_t * pNtk )
 
 /**Function*************************************************************
 
-  Synopsis    [Writes the inputs.]
+  Synopsis    [Writes the nodes.]
 
   Description []
                
@@ -419,24 +440,32 @@ void Io_WriteVerilogNodes( FILE * pFile, Abc_Ntk_t * pNtk )
   SeeAlso     []
 
 ***********************************************************************/
-void Io_WriteVerilogArgs( FILE * pFile, Abc_Obj_t * pObj, int nInMax, int fPadZeros )
+void Io_WriteVerilogNodes( FILE * pFile, Abc_Ntk_t * pNtk )
 {
-    Abc_Obj_t * pFanin;
-    int i, Counter = 2;
-    fprintf( pFile, "(.z (%s)", Io_WriteVerilogGetName(Abc_ObjFanout0(pObj)) );
-    Abc_ObjForEachFanin( pObj, pFanin, i )
-    {
-        if ( Counter++ % 4 == 0 )
-            fprintf( pFile, "\n   " );
-        fprintf( pFile, " .i%d (%s)", i+1, Io_WriteVerilogGetName(Abc_ObjFanin(pObj,i)) );
-    }
-    for ( ; i < nInMax; i++ )
+    Abc_Obj_t * pObj, * pFanin;
+    int i, k, nFanins;
+    char pOper[] = " ? ", Symb;
+    Abc_NtkForEachNode( pNtk, pObj, i )
     {
-        if ( Counter++ % 4 == 0 )
-            fprintf( pFile, "\n   " );
-        fprintf( pFile, " .i%d (%s)", i+1, fPadZeros? "1\'b0" : "1\'b1" );
+        assert( Abc_SopGetCubeNum(pObj->pData) == 1 );
+        nFanins = Abc_ObjFaninNum(pObj);
+        if ( nFanins == 0 )
+        {
+            fprintf( pFile, "  assign %s = 1'b%d;\n", Io_WriteVerilogGetName(Abc_ObjFanout0(pObj)), !Abc_SopIsComplement(pObj->pData) );
+            continue;
+        }
+        fprintf( pFile, "  assign %s = ", Io_WriteVerilogGetName(Abc_ObjFanout0(pObj)) );
+        pOper[1] = Abc_SopIsComplement(pObj->pData) ? '|' : '&';
+        Abc_ObjForEachFanin( pObj, pFanin, k )
+        {
+            Symb = ((char*)pObj->pData)[k];
+            assert( Symb == '0' || Symb == '1' );
+            if ( Symb == '0' )
+                fprintf( pFile, "~" );
+            fprintf( pFile, "%s%s", Io_WriteVerilogGetName(pFanin), (k==nFanins-1? "" : pOper) );
+        }
+        fprintf( pFile, ";\n" );
     }
-    fprintf( pFile, ");\n" );
 }
 
 /**Function*************************************************************

src/base/main/mainFrame.c

@@ -446,7 +446,7 @@ void Abc_FrameDeleteAllNetworks( Abc_Frame_t * p )
         Abc_NtkDelete( pNtk );
     // set the current network empty
     p->pNtkCur = NULL;
-    fprintf( p->Out, "All networks have been deleted.\n" );
+//    fprintf( p->Out, "All networks have been deleted.\n" );
 }
 
 /**Function*************************************************************

src/base/main/module.make

 SRC +=  src/base/main/main.c \
     src/base/main/mainFrame.c \
     src/base/main/mainInit.c \
-    src/base/main/mainUtils.c \
-    src/base/main/libSupport.c
+    src/base/main/libSupport.c \
+    src/base/main/mainUtils.c

src/base/seq/seqAigCore.c

@@ -319,6 +319,7 @@ int Seq_NtkImplementRetimingBackward( Abc_Ntk_t * pNtk, Vec_Ptr_t * vMoves, int
     // add the PI/PO names
     Abc_NtkAddDummyPiNames( pNtkProb );
     Abc_NtkAddDummyPoNames( pNtkProb );
+    Abc_NtkAddDummyAssertNames( pNtkProb );
 
     // make sure everything is okay with the network structure
     if ( !Abc_NtkDoCheck( pNtkProb ) )
@@ -358,7 +359,7 @@ int Seq_NtkImplementRetimingBackward( Abc_Ntk_t * pNtk, Vec_Ptr_t * vMoves, int
     // solve the miter
 clk = clock();
 //    RetValue = Abc_NtkMiterSat_OldAndRusty( pNtkCnf, 30, 0 );
-    RetValue = Abc_NtkMiterSat( pNtkCnf, 500000, 50000000, 0, 0 );
+    RetValue = Abc_NtkMiterSat( pNtkCnf, (sint64)500000, (sint64)50000000, 0, 0, NULL, NULL );
 if ( fVerbose )
 if ( clock() - clk > 100 )
 {

src/base/seq/seqCreate.c

@@ -110,17 +110,23 @@ Abc_Ntk_t * Abc_NtkAigToSeq( Abc_Ntk_t * pNtk )
         pNtkNew->nObjs++;
     }
     pNtkNew->nNodes = pNtk->nNodes;
-    pNtkNew->nPis   = pNtk->nPis;
-    pNtkNew->nPos   = pNtk->nPos;
 
     // create PI/PO and their names
     Abc_NtkForEachPi( pNtk, pObj, i )
     {
+        Vec_PtrPush( pNtkNew->vPis, pObj->pCopy );
         Vec_PtrPush( pNtkNew->vCis, pObj->pCopy );
         Abc_NtkLogicStoreName( pObj->pCopy, Abc_ObjName(pObj) );
     }
     Abc_NtkForEachPo( pNtk, pObj, i ) 
     {
+        Vec_PtrPush( pNtkNew->vPos, pObj->pCopy );
+        Vec_PtrPush( pNtkNew->vCos, pObj->pCopy );
+        Abc_NtkLogicStoreName( pObj->pCopy, Abc_ObjName(pObj) );
+    }
+    Abc_NtkForEachAssert( pNtk, pObj, i ) 
+    {
+        Vec_PtrPush( pNtkNew->vAsserts, pObj->pCopy );
         Vec_PtrPush( pNtkNew->vCos, pObj->pCopy );
         Abc_NtkLogicStoreName( pObj->pCopy, Abc_ObjName(pObj) );
     }
@@ -252,7 +258,7 @@ void Abc_NtkAigCutsetCopy( Abc_Ntk_t * pNtk )
 Abc_Ntk_t * Abc_NtkSeqToLogicSop( Abc_Ntk_t * pNtk )
 {
     Abc_Ntk_t * pNtkNew; 
-    Abc_Obj_t * pObj, * pObjNew, * pFaninNew;
+    Abc_Obj_t * pObj, * pFaninNew;
     Seq_Lat_t * pRing;
     int i;
 
@@ -297,11 +303,7 @@ Abc_Ntk_t * Abc_NtkSeqToLogicSop( Abc_Ntk_t * pNtk )
 
     // add the latches and their names
     Abc_NtkAddDummyLatchNames( pNtkNew );
-    Abc_NtkForEachLatch( pNtkNew, pObjNew, i )
-    {
-        Vec_PtrPush( pNtkNew->vCis, pObjNew );
-        Vec_PtrPush( pNtkNew->vCos, pObjNew );
-    }
+    Abc_NtkOrderCisCos( pNtkNew );
     // fix the problem with complemented and duplicated CO edges
     Abc_NtkLogicMakeSimpleCos( pNtkNew, 0 );
     if ( !Abc_NtkCheck( pNtkNew ) )
@@ -324,7 +326,7 @@ Abc_Ntk_t * Abc_NtkSeqToLogicSop( Abc_Ntk_t * pNtk )
 Abc_Ntk_t * Abc_NtkSeqToLogicSop_old( Abc_Ntk_t * pNtk )
 {
     Abc_Ntk_t * pNtkNew; 
-    Abc_Obj_t * pObj, * pObjNew, * pFaninNew;
+    Abc_Obj_t * pObj, * pFaninNew;
     int i;
 
     assert( Abc_NtkIsSeq(pNtk) );
@@ -371,11 +373,7 @@ Abc_Ntk_t * Abc_NtkSeqToLogicSop_old( Abc_Ntk_t * pNtk )
     }
     // add the latches and their names
     Abc_NtkAddDummyLatchNames( pNtkNew );
-    Abc_NtkForEachLatch( pNtkNew, pObjNew, i )
-    {
-        Vec_PtrPush( pNtkNew->vCis, pObjNew );
-        Vec_PtrPush( pNtkNew->vCos, pObjNew );
-    }
+    Abc_NtkOrderCisCos( pNtkNew );
     // fix the problem with complemented and duplicated CO edges
     Abc_NtkLogicMakeSimpleCos( pNtkNew, 0 );
     if ( !Abc_NtkCheck( pNtkNew ) )

src/base/seq/seqFpgaCore.c

@@ -280,7 +280,7 @@ Abc_Ntk_t * Seq_NtkSeqFpgaMapped( Abc_Ntk_t * pNtk )
     Abc_Seq_t * p = pNtk->pManFunc;
     Abc_Ntk_t * pNtkMap; 
     Vec_Ptr_t * vLeaves;
-    Abc_Obj_t * pObj, * pLatch, * pFaninNew;
+    Abc_Obj_t * pObj, * pFaninNew;
     Seq_Lat_t * pRing;
     int i;
 
@@ -322,11 +322,7 @@ Abc_Ntk_t * Seq_NtkSeqFpgaMapped( Abc_Ntk_t * pNtk )
 
     // add the latches and their names
     Abc_NtkAddDummyLatchNames( pNtkMap );
-    Abc_NtkForEachLatch( pNtkMap, pLatch, i )
-    {
-        Vec_PtrPush( pNtkMap->vCis, pLatch );
-        Vec_PtrPush( pNtkMap->vCos, pLatch );
-    }
+    Abc_NtkOrderCisCos( pNtkMap );
     // fix the problem with complemented and duplicated CO edges
     Abc_NtkLogicMakeSimpleCos( pNtkMap, 1 );
     // make the network minimum base

src/base/seq/seqMapCore.c

@@ -370,7 +370,7 @@ Abc_Ntk_t * Seq_NtkSeqMapMapped( Abc_Ntk_t * pNtk )
     Seq_Match_t * pMatch;
     Abc_Ntk_t * pNtkMap; 
     Vec_Ptr_t * vLeaves;
-    Abc_Obj_t * pObj, * pLatch, * pFaninNew;
+    Abc_Obj_t * pObj, * pFaninNew;
     Seq_Lat_t * pRing;
     int i;
 
@@ -413,11 +413,7 @@ Abc_Ntk_t * Seq_NtkSeqMapMapped( Abc_Ntk_t * pNtk )
 
     // add the latches and their names
     Abc_NtkAddDummyLatchNames( pNtkMap );
-    Abc_NtkForEachLatch( pNtkMap, pLatch, i )
-    {
-        Vec_PtrPush( pNtkMap->vCis, pLatch );
-        Vec_PtrPush( pNtkMap->vCos, pLatch );
-    }
+    Abc_NtkOrderCisCos( pNtkMap );
     // fix the problem with complemented and duplicated CO edges
     Abc_NtkLogicMakeSimpleCos( pNtkMap, 1 );
     // make the network minimum base

src/base/seq/seqRetCore.c

@@ -327,7 +327,7 @@ Abc_Ntk_t * Seq_NtkRetimeReconstruct( Abc_Ntk_t * pNtkOld, Abc_Ntk_t * pNtkSeq )
     Abc_Seq_t * p = pNtkSeq->pManFunc;
     Seq_Lat_t * pRing0, * pRing1;
     Abc_Ntk_t * pNtkNew;
-    Abc_Obj_t * pObj, * pObjNew, * pFanin, * pFaninNew, * pMirror;
+    Abc_Obj_t * pObj, * pFanin, * pFaninNew, * pMirror;
     Vec_Ptr_t * vMirrors;
     int i, k;
 
@@ -408,11 +408,7 @@ Abc_Ntk_t * Seq_NtkRetimeReconstruct( Abc_Ntk_t * pNtkOld, Abc_Ntk_t * pNtkSeq )
 
     // add the latches and their names
     Abc_NtkAddDummyLatchNames( pNtkNew );
-    Abc_NtkForEachLatch( pNtkNew, pObjNew, i )
-    {
-        Vec_PtrPush( pNtkNew->vCis, pObjNew );
-        Vec_PtrPush( pNtkNew->vCos, pObjNew );
-    }
+    Abc_NtkOrderCisCos( pNtkNew );
     // fix the problem with complemented and duplicated CO edges
     Abc_NtkLogicMakeSimpleCos( pNtkNew, 1 );
     if ( !Abc_NtkCheck( pNtkNew ) )

src/map/fpga/fpgaCut.c

@@ -1082,7 +1082,7 @@ Fpga_Cut_t * Fpga_CutSortCuts( Fpga_Man_t * pMan, Fpga_CutTable_t * p, Fpga_Cut_
     nCuts = Fpga_CutList2Array( p->pCuts1, pList );
     assert( nCuts <= FPGA_CUTS_MAX_COMPUTE );
     // sort the cuts
-    qsort( (void *)p->pCuts1, nCuts, sizeof(Fpga_Cut_t *), 
+    qsort( (void *)p->pCuts1, nCuts, sizeof(void *), 
             (int (*)(const void *, const void *)) Fpga_CutSortCutsCompare );
     // move them back into the list
     if ( nCuts > FPGA_CUTS_MAX_USE - 1 )

src/map/mapper/mapperTable.c

@@ -325,7 +325,7 @@ void Map_SuperTableSortSupergates( Map_HashTable_t * p, int nSupersMax )
                 ppSupers[nSupers++] = pSuper;
 
     // sort by usage
-    qsort( (void *)ppSupers, nSupers, sizeof(int), 
+    qsort( (void *)ppSupers, nSupers, sizeof(Map_Super_t *), 
             (int (*)(const void *, const void *)) Map_SuperTableCompareSupergates );
     assert( Map_SuperTableCompareSupergates( ppSupers, ppSupers + nSupers - 1 ) <= 0 );
 
@@ -380,7 +380,7 @@ void Map_SuperTableSortSupergatesByDelay( Map_HashTable_t * p, int nSupersMax )
             if ( nSupers == 0 )
                 continue;
             // sort the gates by delay
-            qsort( (void *)ppSupers, nSupers, sizeof(int), 
+            qsort( (void *)ppSupers, nSupers, sizeof(Map_Super_t *), 
                     (int (*)(const void *, const void *)) Map_SuperTableCompareGatesInList );
             assert( Map_SuperTableCompareGatesInList( ppSupers, ppSupers + nSupers - 1 ) <= 0 );
             // link them in the reverse order

src/map/mapper/mapperTruth.c

@@ -89,14 +89,15 @@ void Map_MappingTruths( Map_Man_t * pMan )
 
 ***********************************************************************/
 void Map_TruthsCut( Map_Man_t * p, Map_Cut_t * pCut )
-{
+{ 
 //    unsigned uCanon1, uCanon2;
     unsigned uTruth[2], uCanon[2];
     unsigned char uPhases[16];
     unsigned * uCanon2;
     char * pPhases2;
-    int fUseFast = 0;
-    int fUseRec = 1;
+    int fUseFast = 1;
+    int fUseSlow = 0;
+    int fUseRec = 0; // this does not work for Solaris
 
     extern int Map_CanonCompute( int nVarsMax, int nVarsReal, unsigned * pt, unsigned ** pptRes, char ** ppfRes );
  
@@ -117,6 +118,8 @@ void Map_TruthsCut( Map_Man_t * p, Map_Cut_t * pCut )
     // compute the canonical form for the positive phase
     if ( fUseFast )
         Map_CanonComputeFast( p, p->nVarsMax, pCut->nLeaves, uTruth, uPhases, uCanon );
+    else if ( fUseSlow )
+        Map_CanonComputeSlow( p->uTruths, p->nVarsMax, pCut->nLeaves, uTruth, uPhases, uCanon );
     else if ( fUseRec )
     {
 //        Map_CanonComputeSlow( p->uTruths, p->nVarsMax, pCut->nLeaves, uTruth, uPhases, uCanon );
@@ -145,6 +148,8 @@ void Map_TruthsCut( Map_Man_t * p, Map_Cut_t * pCut )
     uTruth[1] = ~uTruth[1];
     if ( fUseFast )
         Map_CanonComputeFast( p, p->nVarsMax, pCut->nLeaves, uTruth, uPhases, uCanon );
+    else if ( fUseSlow )
+        Map_CanonComputeSlow( p->uTruths, p->nVarsMax, pCut->nLeaves, uTruth, uPhases, uCanon );
     else if ( fUseRec )
     {
 //        Map_CanonComputeSlow( p->uTruths, p->nVarsMax, pCut->nLeaves, uTruth, uPhases, uCanon );

src/misc/extra/extra.h

@@ -464,9 +464,8 @@ extern unsigned Extra_TruthSemiCanonicize( unsigned * pInOut, unsigned * pAux, i
 #define ALLOC(type, num)     ((type *) malloc(sizeof(type) * (num)))
 #define FREE(obj)             ((obj) ? (free((char *) (obj)), (obj) = 0) : 0)
 #define REALLOC(type, obj, num)    \
-        (obj) ? ((type *) realloc((char *) obj, sizeof(type) * (num))) : \
-        ((type *) malloc(sizeof(type) * (num)))
-
+        ((obj) ? ((type *) realloc((char *)(obj), sizeof(type) * (num))) : \
+         ((type *) malloc(sizeof(type) * (num))))
 
 extern long        Extra_CpuTime();
 extern int         Extra_GetSoftDataLimit();

src/misc/extra/extraUtilBitMatrix.c

@@ -348,7 +348,7 @@ int Extra_BitMatrixCountOnesUpper( Extra_BitMat_t * p )
     int i, k, nTotal = 0;
     for ( i = 0; i < p->nSize; i++ )
         for ( k = i + 1; k < p->nSize; k++ )
-            nTotal += ( (p->ppData[i][k/32] & (1 << (k%32))) > 0 );
+            nTotal += ( (p->ppData[i][k>>5] & (1 << (k&31))) > 0 );
     return nTotal;
 }
 

src/misc/extra/extraUtilMisc.c

@@ -1323,9 +1323,9 @@ void Extra_TruthExpand( int nVars, int nWords, unsigned * puTruth, unsigned uPha
         { 0xF0F0F0F0,0xF0F0F0F0,0xF0F0F0F0,0xF0F0F0F0,0xF0F0F0F0,0xF0F0F0F0,0xF0F0F0F0,0xF0F0F0F0 },
         { 0xFF00FF00,0xFF00FF00,0xFF00FF00,0xFF00FF00,0xFF00FF00,0xFF00FF00,0xFF00FF00,0xFF00FF00 },
         { 0xFFFF0000,0xFFFF0000,0xFFFF0000,0xFFFF0000,0xFFFF0000,0xFFFF0000,0xFFFF0000,0xFFFF0000 }, 
-        { 0xFFFFFFFF,0x00000000,0xFFFFFFFF,0x00000000,0xFFFFFFFF,0x00000000,0xFFFFFFFF,0x00000000 }, 
-        { 0xFFFFFFFF,0xFFFFFFFF,0x00000000,0x00000000,0xFFFFFFFF,0xFFFFFFFF,0x00000000,0x00000000 }, 
-        { 0xFFFFFFFF,0xFFFFFFFF,0xFFFFFFFF,0xFFFFFFFF,0x00000000,0x00000000,0x00000000,0x00000000 } 
+        { 0x00000000,0xFFFFFFFF,0x00000000,0xFFFFFFFF,0x00000000,0xFFFFFFFF,0x00000000,0xFFFFFFFF }, 
+        { 0x00000000,0x00000000,0xFFFFFFFF,0xFFFFFFFF,0x00000000,0x00000000,0xFFFFFFFF,0xFFFFFFFF }, 
+        { 0x00000000,0x00000000,0x00000000,0x00000000,0xFFFFFFFF,0xFFFFFFFF,0xFFFFFFFF,0xFFFFFFFF } 
     };
     static char Cases[256] = {
          0, // 00000000
@@ -1922,12 +1922,12 @@ void Extra_TruthExpand( int nVars, int nWords, unsigned * puTruth, unsigned uPha
             puTruthR[i] = 0;
         nMints = (1 << nVars);
         for ( i = 0; i < nMints; i++ )
-            if ( puTruth[i/32] & (1 << (i%32)) )
+            if ( puTruth[i>>5] & (1 << (i&31)) )
             {
                 for ( iRes = 0, k = 0; k < 5; k++ )
                     if ( i & (1 << pPerm[k]) )
                         iRes |= (1 << k);
-                puTruthR[iRes/32] |= (1 << (iRes%32));
+                puTruthR[iRes>>5] |= (1 << (iRes&31));
             }
     }
 }
@@ -2058,9 +2058,9 @@ unsigned ** Extra_Truths8()
         { 0xF0F0F0F0,0xF0F0F0F0,0xF0F0F0F0,0xF0F0F0F0,0xF0F0F0F0,0xF0F0F0F0,0xF0F0F0F0,0xF0F0F0F0 },
         { 0xFF00FF00,0xFF00FF00,0xFF00FF00,0xFF00FF00,0xFF00FF00,0xFF00FF00,0xFF00FF00,0xFF00FF00 },
         { 0xFFFF0000,0xFFFF0000,0xFFFF0000,0xFFFF0000,0xFFFF0000,0xFFFF0000,0xFFFF0000,0xFFFF0000 }, 
-        { 0xFFFFFFFF,0x00000000,0xFFFFFFFF,0x00000000,0xFFFFFFFF,0x00000000,0xFFFFFFFF,0x00000000 }, 
-        { 0xFFFFFFFF,0xFFFFFFFF,0x00000000,0x00000000,0xFFFFFFFF,0xFFFFFFFF,0x00000000,0x00000000 }, 
-        { 0xFFFFFFFF,0xFFFFFFFF,0xFFFFFFFF,0xFFFFFFFF,0x00000000,0x00000000,0x00000000,0x00000000 } 
+        { 0x00000000,0xFFFFFFFF,0x00000000,0xFFFFFFFF,0x00000000,0xFFFFFFFF,0x00000000,0xFFFFFFFF }, 
+        { 0x00000000,0x00000000,0xFFFFFFFF,0xFFFFFFFF,0x00000000,0x00000000,0xFFFFFFFF,0xFFFFFFFF }, 
+        { 0x00000000,0x00000000,0x00000000,0x00000000,0xFFFFFFFF,0xFFFFFFFF,0xFFFFFFFF,0xFFFFFFFF } 
     };
     static unsigned * puResult[8] = {
         uTruths[0], uTruths[1], uTruths[2], uTruths[3], uTruths[4], uTruths[5], uTruths[6], uTruths[7] 

src/misc/extra/extraUtilTruth.c

@@ -264,15 +264,15 @@ DdNode * Extra_TruthToBdd_rec( DdManager * dd, unsigned * pTruth, int iBit, int
     DdNode * bF0, * bF1, * bF;
     if ( nVars == 0 )
     {
-        if ( pTruth[iBit/32] & (1 << iBit%32) )
+        if ( pTruth[iBit>>5] & (1 << iBit&31) )
             return b1;
         return b0;
     }
     if ( nVars == 5 )
     {
-        if ( pTruth[iBit/32] == 0xFFFFFFFF )
+        if ( pTruth[iBit>>5] == 0xFFFFFFFF )
             return b1;
-        if ( pTruth[iBit/32] == 0 )
+        if ( pTruth[iBit>>5] == 0 )
             return b0;
     }
     // other special cases can be added

src/misc/mvc/mvc.h

@@ -49,7 +49,7 @@
 ////////////////////////////////////////////////////////////////////////
 
 // cube/list/cover/data
-typedef unsigned long              Mvc_CubeWord_t;
+typedef unsigned int               Mvc_CubeWord_t;
 typedef struct MvcCubeStruct       Mvc_Cube_t;
 typedef struct MvcListStruct       Mvc_List_t;
 typedef struct MvcCoverStruct      Mvc_Cover_t;

src/misc/nm/module.make

+SRC +=  src/misc/nm/nmApi.c \
+    src/misc/nm/nmTable.c

src/misc/nm/nm.h

@@ -52,10 +52,12 @@ extern Nm_Man_t *   Nm_ManCreate( int nSize );
 extern void         Nm_ManFree( Nm_Man_t * p );
 extern int          Nm_ManNumEntries( Nm_Man_t * p );
 extern char *       Nm_ManStoreIdName( Nm_Man_t * p, int ObjId, char * pName, char * pSuffix );
+extern void         Nm_ManDeleteIdName( Nm_Man_t * p, int ObjId );
 extern char *       Nm_ManCreateUniqueName( Nm_Man_t * p, int ObjId );
 extern char *       Nm_ManFindNameById( Nm_Man_t * p, int ObjId );
 extern int          Nm_ManFindIdByName( Nm_Man_t * p, char * pName, int * pSecond );
 extern void         Nm_ManPrintTables( Nm_Man_t * p );
+extern Vec_Int_t *  Nm_ManReturnNameIds( Nm_Man_t * p );
 
 #ifdef __cplusplus
 }

src/misc/nm/nmApi.c

@@ -135,6 +135,31 @@ char * Nm_ManStoreIdName( Nm_Man_t * p, int ObjId, char * pName, char * pSuffix
     return pEntry->Name;
 }
 
+/**Function*************************************************************
+
+  Synopsis    [Creates a new entry in the name manager.]
+
+  Description [Returns 1 if the entry with the given object ID
+  already exists in the name manager.]
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Nm_ManDeleteIdName( Nm_Man_t * p, int ObjId )
+{
+    Nm_Entry_t * pEntry;
+    pEntry = Nm_ManTableLookupId(p, ObjId);
+    if ( pEntry == NULL )
+    {
+        printf( "Nm_ManDeleteIdName(): This entry is not in the table.\n" );
+        return;
+    }
+    // remove entry from the table
+    Nm_ManTableDelete( p, pEntry );
+}
+
 
 /**Function*************************************************************
 
@@ -255,6 +280,28 @@ void Nm_ManPrintTables( Nm_Man_t * p )
     printf( "\n" );
 }
 
+/**Function*************************************************************
+
+  Synopsis    [Return the IDs of objects with names.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Vec_Int_t * Nm_ManReturnNameIds( Nm_Man_t * p )
+{
+    Vec_Int_t * vNameIds;
+    int i;
+    vNameIds = Vec_IntAlloc( p->nEntries );
+    for ( i = 0; i < p->nBins; i++ )
+        if ( p->pBinsI2N[i] )
+            Vec_IntPush( vNameIds, p->pBinsI2N[i]->ObjId );
+    return vNameIds;
+}
+
 ////////////////////////////////////////////////////////////////////////
 ///                       END OF FILE                                ///
 ////////////////////////////////////////////////////////////////////////

src/misc/nm/nmInt.h

@@ -30,6 +30,7 @@ extern "C" {
 ////////////////////////////////////////////////////////////////////////
 
 #include "extra.h"
+#include "vec.h"
 #include "nm.h"
 
 ////////////////////////////////////////////////////////////////////////

src/misc/util/util_hack.h

@@ -73,8 +73,8 @@ extern "C" {
 #define ALLOC(type, num)       ((type *) malloc(sizeof(type) * (num)))
 #define FREE(obj)              ((obj) ? (free((char *) (obj)), (obj) = 0) : 0)
 #define REALLOC(type, obj, num) \
-        (obj) ? ((type *) realloc((char *) obj, sizeof(type) * (num))) : \
-        ((type *) malloc(sizeof(type) * (num)))
+        ((obj) ? ((type *) realloc((char *)(obj), sizeof(type) * (num))) : \
+        ((type *) malloc(sizeof(type) * (num))))
 
 extern long        Extra_CpuTime();
 extern int         Extra_GetSoftDataLimit();

src/misc/vec/vecInt.h

@@ -540,6 +540,27 @@ static inline void Vec_IntPushOrder( Vec_Int_t * p, int Entry )
 
 /**Function*************************************************************
 
+  Synopsis    [Inserts the entry while preserving the increasing order.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+static inline int Vec_IntPushUniqueOrder( Vec_Int_t * p, int Entry )
+{
+    int i;
+    for ( i = 0; i < p->nSize; i++ )
+        if ( p->pArray[i] == Entry )
+            return 1;
+    Vec_IntPushOrder( p, Entry );
+    return 0;
+}
+
+/**Function*************************************************************
+
   Synopsis    []
 
   Description []

src/misc/vec/vecPtr.h

@@ -472,6 +472,26 @@ static inline void * Vec_PtrPop( Vec_Ptr_t * p )
 
 /**Function*************************************************************
 
+  Synopsis    [Find entry.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+static inline int Vec_PtrFind( Vec_Ptr_t * p, void * Entry )
+{
+    int i;
+    for ( i = 0; i < p->nSize; i++ )
+        if ( p->pArray[i] == Entry )
+            return i;
+    return -1;
+}
+
+/**Function*************************************************************
+
   Synopsis    []
 
   Description []

src/misc/vec/vecStr.h

@@ -494,10 +494,10 @@ static inline int Vec_StrSortCompare2( char * pp1, char * pp2 )
 static inline void Vec_StrSort( Vec_Str_t * p, int fReverse )
 {
     if ( fReverse ) 
-        qsort( (void *)p->pArray, p->nSize, sizeof(int), 
+        qsort( (void *)p->pArray, p->nSize, sizeof(char), 
                 (int (*)(const void *, const void *)) Vec_StrSortCompare2 );
     else
-        qsort( (void *)p->pArray, p->nSize, sizeof(int), 
+        qsort( (void *)p->pArray, p->nSize, sizeof(char), 
                 (int (*)(const void *, const void *)) Vec_StrSortCompare1 );
 }
 

src/opt/cut/cutMan.c

@@ -45,6 +45,8 @@ Cut_Man_t * Cut_ManStart( Cut_Params_t * pParams )
 {
     Cut_Man_t * p;
     int clk = clock();
+//    extern int nTruthDsd;
+//    nTruthDsd = 0;
     assert( pParams->nVarsMax >= 3 && pParams->nVarsMax <= CUT_SIZE_MAX );
     p = ALLOC( Cut_Man_t, 1 );
     memset( p, 0, sizeof(Cut_Man_t) );
@@ -114,6 +116,9 @@ void Cut_ManStop( Cut_Man_t * p )
 {
     Cut_Cut_t * pCut;
     int i;
+//    extern int nTruthDsd;
+//    printf( "Decomposable cuts = %d.\n", nTruthDsd );
+
     Vec_PtrForEachEntry( p->vCutsNew, pCut, i )
         if ( pCut != NULL )
         {

src/opt/cut/cutPre22.c

@@ -779,7 +779,7 @@ Cut_CMan_t * Cut_CManStart()
     for ( k = 0; k < CUT_CELL_MVAR; k++ )
         for ( i = 0; i < (1<<CUT_CELL_MVAR); i++ )
             if ( i & (1 << k) )
-                p->uInputs[k][i/32] |= (1 << (i%32));
+                p->uInputs[k][i>>5] |= (1 << (i&31));
     s_pCMan = p;
     return p;
 }

src/opt/cut/cutTruth.c

@@ -189,6 +189,9 @@ void Cut_TruthCompute( Cut_Man_t * p, Cut_Cut_t * pCut, Cut_Cut_t * pCut0, Cut_C
         Extra_TruthNand( Cut_CutReadTruth(pCut), p->puTemp[2], p->puTemp[3], pCut->nVarsMax );
     else
         Extra_TruthAnd( Cut_CutReadTruth(pCut), p->puTemp[2], p->puTemp[3], pCut->nVarsMax );
+
+//    Ivy_TruthTestOne( *Cut_CutReadTruth(pCut) );
+
     // quit if no fancy computation is needed
     if ( !p->pParams->fFancy )
         return;

src/opt/dec/decAbc.c

@@ -19,6 +19,7 @@
 #include "abc.h"
 #include "dec.h"
 //#include "aig.h"
+#include "ivy.h"
 
 ////////////////////////////////////////////////////////////////////////
 ///                        DECLARATIONS                              ///
@@ -238,6 +239,41 @@ Aig_Node_t * Dec_GraphToNetworkAig( Aig_Man_t * pMan, Dec_Graph_t * pGraph )
 }
 */
 
+/**Function*************************************************************
+
+  Synopsis    [Transforms the decomposition graph into the AIG.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+
+Ivy_Obj_t * Dec_GraphToNetworkIvy( Ivy_Man_t * pMan, Dec_Graph_t * pGraph )
+{
+    Dec_Node_t * pNode;
+    Ivy_Obj_t * pAnd0, * pAnd1;
+    int i;
+    // check for constant function
+    if ( Dec_GraphIsConst(pGraph) )
+        return Ivy_NotCond( Ivy_ManConst1(pMan), Dec_GraphIsComplement(pGraph) );
+    // check for a literal
+    if ( Dec_GraphIsVar(pGraph) )
+        return Ivy_NotCond( Dec_GraphVar(pGraph)->pFunc, Dec_GraphIsComplement(pGraph) );
+    // build the AIG nodes corresponding to the AND gates of the graph
+    Dec_GraphForEachNode( pGraph, pNode, i )
+    {
+        pAnd0 = Ivy_NotCond( Dec_GraphNode(pGraph, pNode->eEdge0.Node)->pFunc, pNode->eEdge0.fCompl ); 
+        pAnd1 = Ivy_NotCond( Dec_GraphNode(pGraph, pNode->eEdge1.Node)->pFunc, pNode->eEdge1.fCompl ); 
+        pNode->pFunc = Ivy_And( pAnd0, pAnd1 );
+    }
+    // complement the result if necessary
+    return Ivy_NotCond( pNode->pFunc, Dec_GraphIsComplement(pGraph) );
+}
+
+
 ////////////////////////////////////////////////////////////////////////
 ///                       END OF FILE                                ///
 ////////////////////////////////////////////////////////////////////////

src/opt/dec/decFactor.c

@@ -258,16 +258,15 @@ Dec_Edge_t Dec_FactorTrivial( Dec_Graph_t * pFForm, Mvc_Cover_t * pCover )
 ***********************************************************************/
 Dec_Edge_t Dec_FactorTrivialCube( Dec_Graph_t * pFForm, Mvc_Cover_t * pCover, Mvc_Cube_t * pCube, Vec_Int_t * vEdgeLits )
 {
-//    Dec_Edge_t eNode;
+    Dec_Edge_t eNode;
     int iBit, Value;
     // create the factored form for each literal
     Vec_IntClear( vEdgeLits );
     Mvc_CubeForEachBit( pCover, pCube, iBit, Value )
         if ( Value )
         {
-//            eNode = Dec_EdgeCreate( iBit/2, iBit%2 ); // CST
-//            Vec_IntPush( vEdgeLits, Dec_EdgeToInt_(eNode) );
-            Vec_IntPush( vEdgeLits, iBit );
+            eNode = Dec_EdgeCreate( iBit/2, iBit%2 ); // CST
+            Vec_IntPush( vEdgeLits, Dec_EdgeToInt_(eNode) );
         }
     // balance the factored forms
     return Dec_FactorTrivialTree_rec( pFForm, (Dec_Edge_t *)vEdgeLits->pArray, vEdgeLits->nSize, 0 );

src/opt/fxu/fxu.h

@@ -37,9 +37,11 @@ extern "C" {
 ///                    STRUCTURE DEFINITIONS                         ///
 ////////////////////////////////////////////////////////////////////////
 
+#ifndef __cplusplus
 #ifndef bool
 #define bool int
 #endif
+#endif
 
 typedef struct FxuDataStruct   Fxu_Data_t;
 

src/opt/rwr/rwr.h

@@ -135,6 +135,7 @@ extern void              Rwr_ManStop( Rwr_Man_t * p );
 extern void              Rwr_ManPrintStats( Rwr_Man_t * p );
 extern void              Rwr_ManPrintStatsFile( Rwr_Man_t * p );
 extern void *            Rwr_ManReadDecs( Rwr_Man_t * p );
+extern Vec_Ptr_t *       Rwr_ManReadLeaves( Rwr_Man_t * p );
 extern int               Rwr_ManReadCompl( Rwr_Man_t * p );
 extern void              Rwr_ManAddTimeCuts( Rwr_Man_t * p, int Time );
 extern void              Rwr_ManAddTimeUpdate( Rwr_Man_t * p, int Time );

src/opt/rwr/rwrEva.c

@@ -100,9 +100,16 @@ clk = clock();
         p->nCutsGood++;
 
 clk2 = clock();
+/*
+        printf( "Considering: (" );
+        Vec_PtrForEachEntry( p->vFaninsCur, pFanin, i )
+            printf( "%d ", Abc_ObjFanoutNum(Abc_ObjRegular(pFanin)) );
+        printf( ")\n" );
+*/
         // mark the fanin boundary 
         Vec_PtrForEachEntry( p->vFaninsCur, pFanin, i )
             Abc_ObjRegular(pFanin)->vFanouts.nSize++;
+
         // label MFFC with current ID
         Abc_NtkIncrementTravId( pNode->pNtk );
         nNodesSaved = Abc_NodeMffcLabel( pNode );
@@ -136,6 +143,8 @@ p->timeRes += clock() - clk;
     if ( GainBest == -1 )
         return -1;
 
+//    printf( "%d", nNodesSaveCur - GainBest );
+
     // copy the leaves
     Vec_PtrForEachEntry( p->vFanins, pFanin, i )
         Dec_GraphNode(p->pGraph, i)->pFunc = pFanin;

src/opt/rwr/rwrMan.c

@@ -163,7 +163,11 @@ void Rwr_ManPrintStats( Rwr_Man_t * p )
     printf( "The scores are:\n" );
     for ( i = 0; i < 222; i++ )
         if ( p->nScores[i] > 0 )
-            printf( "%3d = %8d  canon = %5d\n", i, p->nScores[i], p->pMapInv[i] );
+        {
+            extern void Ivy_TruthDsdComputePrint( unsigned uTruth );
+            printf( "%3d = %8d  canon = %5d  ", i, p->nScores[i], p->pMapInv[i] );
+            Ivy_TruthDsdComputePrint( (unsigned)p->pMapInv[i] | ((unsigned)p->pMapInv[i] << 16) );
+        }
     printf( "\n" );
 
 }
@@ -218,6 +222,22 @@ void * Rwr_ManReadDecs( Rwr_Man_t * p )
   SeeAlso     []
 
 ***********************************************************************/
+Vec_Ptr_t * Rwr_ManReadLeaves( Rwr_Man_t * p )
+{
+    return p->vFanins;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Stops the resynthesis manager.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
 int Rwr_ManReadCompl( Rwr_Man_t * p )
 {
     return p->fCompl;

src/opt/rwr/rwrTemp.c

+/**CFile****************************************************************
+
+  FileName    [rwrCut.c]
+
+  SystemName  [ABC: Logic synthesis and verification system.]
+
+  PackageName [DAG-aware AIG rewriting package.]
+
+  Synopsis    [Cut computation.]
+
+  Author      [Alan Mishchenko]
+  
+  Affiliation [UC Berkeley]
+
+  Date        [Ver. 1.0. Started - June 20, 2005.]
+
+  Revision    [$Id: rwrCut.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
+
+***********************************************************************/
+
+#include "rwr.h"
+
+////////////////////////////////////////////////////////////////////////
+///                        DECLARATIONS                              ///
+////////////////////////////////////////////////////////////////////////
+
+static int pTruths[13719];
+static int pFreqs[13719];
+static int pPerm[13719];
+
+////////////////////////////////////////////////////////////////////////
+///                     FUNCTION DEFINITIONS                         ///
+////////////////////////////////////////////////////////////////////////
+ 
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Rwr_TempCompare( int * pNum1, int * pNum2 )
+{
+    int Freq1 = pFreqs[*pNum1];
+    int Freq2 = pFreqs[*pNum2];
+    if ( Freq1 < Freq2 )
+        return 1;
+    if ( Freq1 > Freq2 )
+        return -1;
+    return 0; 
+}
+ 
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Rwr_Temp()
+{
+    char Buffer[32];
+    int nFuncs = 13719;
+    int nEntries = 100;
+    unsigned uTruth;
+    int i, k;
+    FILE * pFile;
+
+    pFile = fopen( "nnclass_stats5.txt", "r" );
+    for ( i = 0; i < 13719; i++ )
+    {
+        fscanf( pFile, "%s%d", Buffer, &pFreqs[i] );
+        Extra_ReadHexadecimal( &uTruth, Buffer+2, 5 );
+        pTruths[i] = uTruth;
+    }
+    fclose( pFile );
+
+    for ( i = 0; i < 13719; i++ )
+        pPerm[i] = i;
+
+    qsort( (void *)pPerm, 13719, sizeof(int), 
+            (int (*)(const void *, const void *)) Rwr_TempCompare );
+
+
+    pFile = fopen( "5npn_100.blif", "w" );
+    fprintf( pFile, "# Most frequent NPN classes of 5 vars.\n" );
+    fprintf( pFile, ".model 5npn\n" );
+    fprintf( pFile, ".inputs a b c d e\n" );
+    fprintf( pFile, ".outputs" );
+    for ( i = 0; i < nEntries; i++ )
+        fprintf( pFile, " %02d", i );
+    fprintf( pFile, "\n" );
+
+    for ( i = 0; i < nEntries; i++ )
+    {
+        fprintf( pFile, ".names a b c d e %02d\n", i );
+        uTruth = pTruths[pPerm[i]];
+        for ( k = 0; k < 32; k++ )
+            if ( uTruth & (1 << k) )
+            {
+                Extra_PrintBinary( pFile, &k, 5 );
+                fprintf( pFile, " 1\n" );
+            }
+    }
+    fprintf( pFile, ".end\n" );
+    fclose( pFile );
+}
+
+////////////////////////////////////////////////////////////////////////
+///                       END OF FILE                                ///
+////////////////////////////////////////////////////////////////////////
+
+

src/opt/sim/sim.h

@@ -143,8 +143,8 @@ struct Sim_Pat_t_
 ///                      MACRO DEFINITIONS                           ///
 ////////////////////////////////////////////////////////////////////////
 
-#define SIM_NUM_WORDS(n)      ((n)/32 + (((n)%32) > 0))
-#define SIM_LAST_BITS(n)      ((((n)%32) > 0)? (n)%32 : 32)
+#define SIM_NUM_WORDS(n)      (((n)>>5) + (((n)&31) > 0))
+#define SIM_LAST_BITS(n)      ((((n)&31) > 0)? (n)&31 : 32)
 
 #define SIM_MASK_FULL         (0xFFFFFFFF)
 #define SIM_MASK_BEG(n)       (SIM_MASK_FULL >> (32-n))

src/opt/xyz/module.make

-SRC +=    src/opt/xyz/xyzBuild.c \
-    src/opt/xyz/xyzCore.c \
-    src/opt/xyz/xyzMan.c \
-    src/opt/xyz/xyzMinEsop.c \
-    src/opt/xyz/xyzMinMan.c \
-    src/opt/xyz/xyzMinSop.c \
-    src/opt/xyz/xyzMinUtil.c \
-    src/opt/xyz/xyzTest.c 

src/opt/xyz/xyz.h

-/**CFile****************************************************************
-
-  FileName    [xyz.h]
-
-  SystemName  [ABC: Logic synthesis and verification system.]
-
-  PackageName [Cover manipulation package.]
-
-  Synopsis    [External declarations.]
-
-  Author      [Alan Mishchenko]
-  
-  Affiliation [UC Berkeley]
-
-  Date        [Ver. 1.0. Started - June 20, 2005.]
-
-  Revision    [$Id: xyz.h,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
-
-***********************************************************************/
-
-#ifndef __XYZ_H__
-#define __XYZ_H__
-
-#ifdef __cplusplus
-extern "C" {
-#endif
-
-#include "abc.h"
-#include "xyzInt.h"
-
-////////////////////////////////////////////////////////////////////////
-///                        DECLARATIONS                              ///
-////////////////////////////////////////////////////////////////////////
-
-typedef struct Xyz_Man_t_  Xyz_Man_t;
-typedef struct Xyz_Obj_t_  Xyz_Obj_t;
-
-// storage for node information
-struct Xyz_Obj_t_
-{
-    Min_Cube_t *      pCover[3];    // pos/neg/esop
-    Vec_Int_t *       vSupp;        // computed support (all nodes except CIs)
-};
-
-// storage for additional information
-struct Xyz_Man_t_
-{
-    // general characteristics
-    int               nFaninMax;    // the number of vars
-    int               nCubesMax;    // the limit on the number of cubes in the intermediate covers
-    int               nWords;       // the number of words
-    Vec_Int_t *       vFanCounts;   // fanout counts
-    Vec_Ptr_t *       vObjStrs;     // object structures
-    void *            pMemory;      // memory for the internal data strctures
-    Min_Man_t *       pManMin;      // the cub manager
-    int               fUseEsop;     // enables ESOPs
-    int               fUseSop;      // enables SOPs
-    // arrays to map local variables
-    Vec_Int_t *       vComTo0;      // mapping of common variables into first fanin
-    Vec_Int_t *       vComTo1;      // mapping of common variables into second fanin
-    Vec_Int_t *       vPairs0;      // the first var in each pair of common vars
-    Vec_Int_t *       vPairs1;      // the second var in each pair of common vars
-    Vec_Int_t *       vTriv0;       // trival support of the first node
-    Vec_Int_t *       vTriv1;       // trival support of the second node
-    // statistics
-    int               nSupps;       // supports created
-    int               nSuppsMax;    // the maximum number of supports
-    int               nBoundary;    // the boundary size
-    int               nNodes;       // the number of nodes processed
-};
-
-static inline Xyz_Obj_t *  Abc_ObjGetStr( Abc_Obj_t * pObj )                       { return Vec_PtrEntry(((Xyz_Man_t *)pObj->pNtk->pManCut)->vObjStrs, pObj->Id); }
-
-static inline void         Abc_ObjSetSupp( Abc_Obj_t * pObj, Vec_Int_t * vVec )    { Abc_ObjGetStr(pObj)->vSupp = vVec;   }
-static inline Vec_Int_t *  Abc_ObjGetSupp( Abc_Obj_t * pObj )                      { return Abc_ObjGetStr(pObj)->vSupp;   }
-
-static inline void         Abc_ObjSetCover2( Abc_Obj_t * pObj, Min_Cube_t * pCov ) { Abc_ObjGetStr(pObj)->pCover[2] = pCov; }
-static inline Min_Cube_t * Abc_ObjGetCover2( Abc_Obj_t * pObj )                    { return Abc_ObjGetStr(pObj)->pCover[2]; }
-
-static inline void         Abc_ObjSetCover( Abc_Obj_t * pObj, Min_Cube_t * pCov, int Pol ) { Abc_ObjGetStr(pObj)->pCover[Pol] = pCov; }
-static inline Min_Cube_t * Abc_ObjGetCover( Abc_Obj_t * pObj, int Pol )                    { return Abc_ObjGetStr(pObj)->pCover[Pol]; }
-
-////////////////////////////////////////////////////////////////////////
-///                     FUNCTION DEFINITIONS                         ///
-////////////////////////////////////////////////////////////////////////
-
-/*=== xyzBuild.c ==========================================================*/
-extern Abc_Ntk_t * Abc_NtkXyzDerive( Xyz_Man_t * p, Abc_Ntk_t * pNtk );
-extern Abc_Ntk_t * Abc_NtkXyzDeriveClean( Xyz_Man_t * p, Abc_Ntk_t * pNtk );
-/*=== xyzCore.c ===========================================================*/
-extern Abc_Ntk_t * Abc_NtkXyz( Abc_Ntk_t * pNtk, int nFaninMax, bool fUseEsop, bool fUseSop, bool fUseInvs, bool fVerbose );
-/*=== xyzMan.c ============================================================*/
-extern Xyz_Man_t * Xyz_ManAlloc( Abc_Ntk_t * pNtk, int nFaninMax );
-extern void        Xyz_ManFree( Xyz_Man_t * p );
-extern void        Abc_NodeXyzDropData( Xyz_Man_t * p, Abc_Obj_t * pObj );
-/*=== xyzTest.c ===========================================================*/
-extern Abc_Ntk_t * Abc_NtkXyzTestSop( Abc_Ntk_t * pNtk );
-
-#ifdef __cplusplus
-}
-#endif
-
-#endif
-
-////////////////////////////////////////////////////////////////////////
-///                       END OF FILE                                ///
-////////////////////////////////////////////////////////////////////////
-
-
-

src/opt/xyz/xyzMan.c

-/**CFile****************************************************************
-
-  FileName    [xyzMan.c]
-
-  SystemName  [ABC: Logic synthesis and verification system.]
-
-  PackageName [Cover manipulation package.]
-
-  Synopsis    [Decomposition manager.]
-
-  Author      [Alan Mishchenko]
-  
-  Affiliation [UC Berkeley]
-
-  Date        [Ver. 1.0. Started - June 20, 2005.]
-
-  Revision    [$Id: xyzMan.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
-
-***********************************************************************/
-
-#include "xyz.h"
-
-////////////////////////////////////////////////////////////////////////
-///                        DECLARATIONS                              ///
-////////////////////////////////////////////////////////////////////////
-
-////////////////////////////////////////////////////////////////////////
-///                     FUNCTION DEFINITIONS                         ///
-////////////////////////////////////////////////////////////////////////
-
-/**Function*************************************************************
-
-  Synopsis    []
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-Xyz_Man_t * Xyz_ManAlloc( Abc_Ntk_t * pNtk, int nFaninMax )
-{
-    Xyz_Man_t * pMan;
-    Xyz_Obj_t * pMem;
-    Abc_Obj_t * pObj;
-    int i;
-    assert( pNtk->pManCut == NULL );
-
-    // start the manager
-    pMan = ALLOC( Xyz_Man_t, 1 );
-    memset( pMan, 0, sizeof(Xyz_Man_t) );
-    pMan->nFaninMax = nFaninMax;
-    pMan->nCubesMax = 2 * pMan->nFaninMax;
-    pMan->nWords    = Abc_BitWordNum( nFaninMax * 2 );
-
-    // get the cubes
-    pMan->vComTo0 = Vec_IntAlloc( 2*nFaninMax );
-    pMan->vComTo1 = Vec_IntAlloc( 2*nFaninMax );
-    pMan->vPairs0 = Vec_IntAlloc( nFaninMax );
-    pMan->vPairs1 = Vec_IntAlloc( nFaninMax );
-    pMan->vTriv0  = Vec_IntAlloc( 1 );  Vec_IntPush( pMan->vTriv0, -1 ); 
-    pMan->vTriv1  = Vec_IntAlloc( 1 );  Vec_IntPush( pMan->vTriv1, -1 ); 
-
-    // allocate memory for object structures
-    pMan->pMemory = pMem = ALLOC( Xyz_Obj_t, sizeof(Xyz_Obj_t) * Abc_NtkObjNumMax(pNtk) );
-    memset( pMem, 0, sizeof(Xyz_Obj_t) * Abc_NtkObjNumMax(pNtk) );
-    // allocate storage for the pointers to the memory
-    pMan->vObjStrs = Vec_PtrAlloc( Abc_NtkObjNumMax(pNtk) );
-    Vec_PtrFill( pMan->vObjStrs, Abc_NtkObjNumMax(pNtk), NULL );
-    Abc_NtkForEachObj( pNtk, pObj, i )
-        Vec_PtrWriteEntry( pMan->vObjStrs, i, pMem + i );
-    // create the cube manager
-    pMan->pManMin = Min_ManAlloc( nFaninMax );
-    return pMan;
-}
-
-/**Function*************************************************************
-
-  Synopsis    []
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-void Xyz_ManFree( Xyz_Man_t * p )
-{
-    Vec_Int_t * vSupp;
-    int i;
-    for ( i = 0; i < p->vObjStrs->nSize; i++ )
-    {
-        vSupp = ((Xyz_Obj_t *)p->vObjStrs->pArray[i])->vSupp;
-        if ( vSupp ) Vec_IntFree( vSupp );
-    }
-
-    Min_ManFree( p->pManMin );
-    Vec_PtrFree( p->vObjStrs );
-    Vec_IntFree( p->vFanCounts );
-    Vec_IntFree( p->vTriv0 );
-    Vec_IntFree( p->vTriv1 );
-    Vec_IntFree( p->vComTo0 );
-    Vec_IntFree( p->vComTo1 );
-    Vec_IntFree( p->vPairs0 );
-    Vec_IntFree( p->vPairs1 );
-    free( p->pMemory );
-    free( p );
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Drop the covers at the node.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-void Abc_NodeXyzDropData( Xyz_Man_t * p, Abc_Obj_t * pObj )
-{
-    int nFanouts;
-    assert( p->vFanCounts );
-    nFanouts = Vec_IntEntry( p->vFanCounts, pObj->Id );
-    assert( nFanouts > 0 );
-    if ( --nFanouts == 0 )
-    {
-        Vec_IntFree( Abc_ObjGetSupp(pObj) );
-        Abc_ObjSetSupp( pObj, NULL );
-        Min_CoverRecycle( p->pManMin, Abc_ObjGetCover2(pObj) );
-        Abc_ObjSetCover2( pObj, NULL );
-        p->nSupps--;
-    }
-    Vec_IntWriteEntry( p->vFanCounts, pObj->Id, nFanouts );
-}
-
-////////////////////////////////////////////////////////////////////////
-///                       END OF FILE                                ///
-////////////////////////////////////////////////////////////////////////
-
-

src/sat/aig/aig.h

@@ -64,9 +64,11 @@ extern "C" {
 ////////////////////////////////////////////////////////////////////////
 
 //typedef int                   bool;
+#ifndef __cplusplus
 #ifndef bool
 #define bool int
 #endif
+#endif
 
 typedef struct Aig_Param_t_     Aig_Param_t;
 typedef struct Aig_Man_t_       Aig_Man_t;
@@ -215,7 +217,7 @@ struct Aig_SimInfo_t_
 ///                      MACRO DEFINITIONS                           ///
 ////////////////////////////////////////////////////////////////////////
 
-static inline int          Aig_BitWordNum( int nBits )            { return nBits/32 + ((nBits%32) > 0);       }
+static inline int          Aig_BitWordNum( int nBits )            { return (nBits>>5) + ((nBits&31) > 0);     }
 static inline int          Aig_InfoHasBit( unsigned * p, int i )  { return (p[(i)>>5] & (1<<((i) & 31))) > 0; }
 static inline void         Aig_InfoSetBit( unsigned * p, int i )  { p[(i)>>5] |= (1<<((i) & 31));             }
 static inline void         Aig_InfoXorBit( unsigned * p, int i )  { p[(i)>>5] ^= (1<<((i) & 31));             }

src/sat/aig/fraigCore.c

@@ -92,7 +92,7 @@ Aig_ProofType_t Aig_FraigProveOutput( Aig_Man_t * pMan )
     // solve the miter
     clk = clock();
     pMan->pSat->verbosity = pMan->pParam->fSatVerbose;
-    status = solver_solve( pMan->pSat, NULL, NULL, 0, 0 );//pMan->pParam->nConfLimit, pMan->pParam->nImpLimit );
+    status = solver_solve( pMan->pSat, NULL, NULL, 0, 0 );//pMan->pParam->nConfLimit, pMan->pParam->nInsLimit );
     if ( status == l_Undef )
     {
 //        printf( "The problem timed out.\n" );

src/sat/aig/rwrTruth.c

@@ -167,7 +167,7 @@ void Aig_TruthCount( Aig_Truth_t * p )
 ***********************************************************************/
 static inline unsigned Aig_WordGetPart( unsigned * p, int Start, int Size )
 {
-    return (p[Start/5] >> (Start%32)) & (~0u >> (32-Size));
+    return (p[Start/5] >> (Start&31)) & (~0u >> (32-Size));
 }
 
 /**Function*************************************************************
@@ -183,7 +183,7 @@ static inline unsigned Aig_WordGetPart( unsigned * p, int Start, int Size )
 ***********************************************************************/
 static inline void Aig_WordSetPart( unsigned * p, int Start, unsigned Part )
 {
-    p[Start/5] |= (Part << (Start%32));
+    p[Start/5] |= (Part << (Start&31));
 }
 
 /**Function*************************************************************
@@ -254,7 +254,7 @@ DdNode * Aig_TruthToBdd_rec( DdManager * dd, unsigned * pTruth, int Shift, int n
     }
     if ( nVars == 5 )
     {
-        unsigned * pWord = pTruth + Shift/32;
+        unsigned * pWord = pTruth + (Shift>>5);
         assert( Shift % 32 == 0 );
         if ( *pWord == 0 )
             return Cudd_ReadLogicZero(dd);

src/sat/asat/added.c

@@ -158,7 +158,7 @@ int * solver_get_model( solver * p, int * pVars, int nVars )
     for ( i = 0; i < nVars; i++ )
     {
         assert( pVars[i] >= 0 && pVars[i] < p->size );
-        pModel[i] = (int)(p->model.ptr[pVars[i]] == (void *)l_True);
+        pModel[i] = (int)(p->model.ptr[pVars[i]] == l_True);
     }
     return pModel;    
 }
@@ -188,6 +188,28 @@ void Asat_SatPrintStats( FILE * pFile, solver * p )
         (float)(p->timeUpdate)/(float)(CLOCKS_PER_SEC) );
 }
 
+/**Function*************************************************************
+
+  Synopsis    [Sets the preferred variables.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Asat_SolverSetPrefVars(solver * s, int * pPrefVars, int nPrefVars)
+{
+    int i;
+    assert( s->pPrefVars == NULL );
+    for ( i = 0; i < nPrefVars; i++ )
+        assert( pPrefVars[i] < s->size );
+    s->pPrefVars = pPrefVars;
+    s->nPrefVars = nPrefVars;
+}
+
+
 ////////////////////////////////////////////////////////////////////////
 ///                       END OF FILE                                ///
 ////////////////////////////////////////////////////////////////////////