Version abc71225

31 files changed, 1762 insertions, 111 deletions

diff --git a/Makefile b/Makefile
index 9d42e6bc..c98ffa4e 100644
--- a/Makefile
+++ b/Makefile
@@ -19,7 +19,7 @@ MODULES := src/base/abc src/base/abci src/base/cmd \
 	src/aig/ivy src/aig/hop src/aig/rwt src/aig/deco \
 	src/aig/mem src/aig/dar src/aig/fra src/aig/cnf \
 	src/aig/csw src/aig/ioa src/aig/aig src/aig/kit \
-	src/aig/bdc src/aig/bar
+	src/aig/bdc src/aig/bar src/aig/ntl
 
 default: $(PROG)
 
diff --git a/abc.dsp b/abc.dsp
index b8db46a4..a1a6a7a1 100644
--- a/abc.dsp
+++ b/abc.dsp
@@ -978,6 +978,10 @@ SOURCE=.\src\bdd\reo\reoProfile.c
 # End Source File
 # Begin Source File
 
+SOURCE=.\src\bdd\reo\reoShuffle.c
+# End Source File
+# Begin Source File
+
 SOURCE=.\src\bdd\reo\reoSift.c
 # End Source File
 # Begin Source File
@@ -2978,6 +2982,10 @@ SOURCE=.\src\aig\ntl\ntlTable.c
 # End Source File
 # Begin Source File
 
+SOURCE=.\src\aig\ntl\ntlTime.c
+# End Source File
+# Begin Source File
+
 SOURCE=.\src\aig\ntl\ntlWriteBlif.c
 # End Source File
 # End Group
diff --git a/abc.rc b/abc.rc
index ce5b1240..88e14e25 100644
--- a/abc.rc
+++ b/abc.rc
@@ -25,6 +25,7 @@ alias b balance
 alias cl cleanup
 alias clp collapse
 alias esd ext_seq_dcs
+alias el eliminate
 alias f fraig
 alias fs fraig_sweep
 alias fsto fraig_store
@@ -44,15 +45,17 @@ alias psy print_symm
 alias pun print_unate
 alias q quit
 alias r read
+alias ra read_aiger
 alias r3 retime -M 3
 alias r3f retime -M 3 -f
 alias r3b retime -M 3 -b
+alias r1 retime -M 1
+alias r2 retime -M 2
 alias ren renode
 alias rh read_hie
 alias rl read_blif
 alias rb read_bench
 alias ret retime
-alias dret dretime
 alias rp read_pla
 alias rt read_truth
 alias rv read_verilog
@@ -68,7 +71,9 @@ alias re restructure
 alias rez restructure -z
 alias rs resub
 alias rsz resub -z
+alias rt3 "retime -M 3 -f"
 alias sa set autoexec ps
+alias ua set autoexec
 alias scl scleanup
 alias sif if -s
 alias so source -x
@@ -89,18 +94,22 @@ alias wp write_pla
 alias wv write_verilog
 
 # standard scripts
+alias share       "b; multi; 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"
 alias choice      "fraig_store; resyn; fraig_store; resyn2; fraig_store; fraig_restore"
 alias choice2     "fraig_store; balance; fraig_store; resyn; fraig_store; resyn2; fraig_store; resyn2; fraig_store; fraig_restore"
 alias rwsat       "st; rw -l; b -l; rw -l; rf -l"
 alias rwsat2      "st; rw -l; b -l; rw -l; rf -l; fraig; rw -l; b -l; rw -l; rf -l"
 alias shake       "st; ps; sat -C 5000; rw -l; ps; sat -C 5000; b -l; rf -l; ps; sat -C 5000; rfz -l; ps; sat -C 5000; rwz -l; ps; sat -C 5000; rfz -l; ps; sat -C 5000"
-alias share       "st; multi -m; fx; resyn2"
+
+alias snap fraig_store
+alias unsnap fraig_restore
 
 # resubstitution scripts for the IWLS paper
 alias src_rw      "st; rw -l; rwz -l; rwz -l" 
@@ -108,21 +117,74 @@ alias src_rs      "st; rs -K 6 -N 2 -l; rs -K 9 -N 2 -l; rs -K 12 -N 2 -l"
 alias src_rws     "st; rw -l; rs -K 6 -N 2 -l; rwz -l; rs -K 9 -N 2 -l; rwz -l; rs -K 12 -N 2 -l" 
 alias resyn2rs    "b; rs -K 6; rw; rs -K 6 -N 2; rf; rs -K 8; b; rs -K 8 -N 2; rw; rs -K 10; rwz; rs -K 10 -N 2; b; rs -K 12; rfz; rs -K 12 -N 2; rwz; b"
 alias compress2rs "b -l; rs -K 6 -l; rw -l; rs -K 6 -N 2 -l; rf -l; rs -K 8 -l; b -l; rs -K 8 -N 2 -l; rw -l; rs -K 10 -l; rwz -l; rs -K 10 -N 2 -l; b -l; rs -K 12 -l; rfz -l; rs -K 12 -N 2 -l; rwz -l; b -l"
+alias c2 "ua; compress2rs; sa"
+alias ic "indcut -v"
+alias lp "lutpack"
+alias c "ua; compress; sa"
+alias c1 "ua; compress;b -l; rs -K 6 -l; rw -l; rs -K 6 -N 2 -l; rf -l; rs -K 8 -l; b -l; sa" 
 
 # experimental implementation of don't-cares
 alias resyn2rsdc    "b; rs -K 6 -F 2; rw; rs -K 6 -N 2 -F 2; rf; rs -K 8 -F 2; b; rs -K 8 -N 2 -F 2; rw; rs -K 10 -F 2; rwz; rs -K 10 -N 2 -F 2; b; rs -K 12 -F 2; rfz; rs -K 12 -N 2 -F 2; rwz; b"
 alias compress2rsdc "b -l; rs -K 6 -F 2 -l; rw -l; rs -K 6 -N 2 -F 2 -l; rf -l; rs -K 8 -F 2 -l; b -l; rs -K 8 -N 2 -F 2 -l; rw -l; rs -K 10 -F 2 -l; rwz -l; rs -K 10 -N 2 -F 2 -l; b -l; rs -K 12 -F 2 -l; rfz -l; rs -K 12 -N 2 -F 2 -l; rwz -l; b -l"
 
+# minimizing for FF literals
+alias fflitmin    "compress2rs; ren; sop; ps -f"
+
 # temporaries
+#alias t        "rvl th/lib.v; rvv th/t2.v"
+#alias t        "so c/pure_sat/test.c"
+#alias t        "r c/14/csat_998.bench; st; ps"
+#alias t0        "r res.blif; aig; mfs"  
+#alias t        "r res2.blif; aig; mfs"  
+
+#alias tt       "r a/quip_opt/nut_001_opt.blif"
+#alias ttb      "wh a/quip_opt/nut_001_opt.blif 1.blif"
+#alias ttv      "wh a/quip_opt/nut_001_opt.blif 1.v"
+
 alias reach    "st; ps; compress2; ps; qrel; ps; compress2; ps; qreach -v; ps"
+
+alias qs1      "qvar -I 96 -u; ps; qbf -P 96" 
+alias qs2      "qvar -I 96 -u; qvar -I 97 -u; ps; qbf -P 96" 
+alias qs3      "qvar -I 96 -u; qvar -I 97 -u; qvar -I 98 -u; ps; qbf -P 96" 
+alias qs4      "qvar -I 96 -u; qvar -I 97 -u; qvar -I 98 -u; qvar -I 99 -u; ps; qbf -P 96" 
+alias qs5      "qvar -I 96 -u; qvar -I 97 -u; qvar -I 98 -u; qvar -I 99 -u; qvar -I 100 -u; ps; qbf -P 96" 
+alias qs6      "qvar -I 96 -u; qvar -I 97 -u; qvar -I 98 -u; qvar -I 99 -u; qvar -I 100 -u; qvar -I 101 -u; ps; qbf -P 96" 
+alias qs7      "qvar -I 96 -u; qvar -I 97 -u; qvar -I 98 -u; qvar -I 99 -u; qvar -I 100 -u; qvar -I 101 -u; qvar -I 102 -u; ps; qbf -P 96" 
+alias qs8      "qvar -I 96 -u; qvar -I 97 -u; qvar -I 98 -u; qvar -I 99 -u; qvar -I 100 -u; qvar -I 101 -u; qvar -I 102 -u; qvar -I 103 -u; ps; qbf -P 96" 
+alias qs9      "qvar -I 96 -u; qvar -I 97 -u; qvar -I 98 -u; qvar -I 99 -u; qvar -I 100 -u; qvar -I 101 -u; qvar -I 102 -u; qvar -I 103 -u; qvar -I 104 -u; ps; qbf -P 96" 
+alias qsA      "qvar -I 96 -u; qvar -I 97 -u; qvar -I 98 -u; qvar -I 99 -u; qvar -I 100 -u; qvar -I 101 -u; qvar -I 102 -u; qvar -I 103 -u; qvar -I 104 -u; qvar -I 105 -u; ps; qbf -P 96" 
+
 alias chnew    "st; haig_start; resyn2; haig_use"
 alias chnewrs  "st; haig_start; resyn2rs; haig_use"
+
 alias stdsd    "r test/6in.blif; st; ps; u; bdd; dsd -g; st; ps"
 alias trec     "rec_start; r c.blif; st; rec_add; rec_use"
 alias trec4    "rec_start -K 4; r i10.blif; st; rec_add; rec_use"
-alias bmc2     "frames -i -F 10; orpos; iprove"
+alias trec5    "rec_start -K 5; r i10.blif; st; rec_add; rec_use"
+alias trec6    "rec_start -K 6; r i10.blif; st; rec_add; rec_use"
+alias trec7    "rec_start -K 7; r i10.blif; st; rec_add; rec_use"
+alias trec8    "rec_start -K 8; r i10.blif; st; rec_add; rec_use"
+alias trec10   "rec_start -K 10; r i10.blif; st; rec_add; rec_use"
+alias trec12   "rec_start -K 12; r i10.blif; st; rec_add; rec_use"
+
+#alias tsh      "r i10_if.blif; st; ps; u; sw; st; ps; cec"
+alias tst4     "r i10_if4.blif; st; ps; r x/rec4_.blif; st; rec_start; r i10_if4.blif; st -r; ps; cec"
+alias tst4n    "r i10_if4.blif; st; ps; r 5npn/all_functions.aig; st; rec_start; r i10_if4.blif; st -r; ps; cec"
+alias tst6     "r i10_if6.blif; st; ps; r x/rec6_16_.blif; st; rec_start; r i10_if6.blif; st -r; ps; cec"
+
+#alias t        "r c.blif; st; wc c.cnf"
+#alias t        "r test/dsdmap6.blif; lutpack -vw; cec"
+#alias t        "r i10_if4.blif; lp"
+#alias t1        "r pj1_if4.blif; lp"
+#alias t2        "r pj1_if6.blif; lp"
+#alias t        "r pj/pj1.blif; st; dfraig -v"
+#alias t        "r c/16/csat_2.bench; st; dfraig -C 100 -v -r"
+#alias t        "r c/16/csat_147.bench; st; dfraig -C 10 -v -r"
+#alias t        "r i10.blif; st; ps; csweep; ps; cec"
+#alias t        "r c/5/csat_777.bench; st; csweep -v"
+#alias t        "r i10.blif; st; drw -v"
+alias t        "r c.blif; st; drf"
+
+
 
-alias t0       "r test/mc1.blif; st; test"
-alias t1       "r s27mc2.blif; st; test"
-alias t2       "r i/intel_001.aig; ps; indcut -v"
 
diff --git a/abc_old.rc b/abc_old.rc
new file mode 100644
index 00000000..ce5b1240
--- /dev/null
+++ b/abc_old.rc
@@ -0,0 +1,128 @@
+# global parameters
+set check         # checks intermediate networks
+#set checkfio      # prints warnings when fanins/fanouts are duplicated
+set checkread     # checks new networks after reading from file
+set backup        # saves backup networks retrived by "undo" and "recall"
+set savesteps 1   # sets the maximum number of backup networks to save 
+set progressbar   # display the progress bar
+
+# program names for internal calls
+set dotwin dot.exe
+set dotunix dot
+set gsviewwin gsview32.exe
+set gsviewunix gv
+set siswin sis.exe
+set sisunix sis
+set mvsiswin mvsis.exe
+set mvsisunix mvsis
+set capowin MetaPl-Capo10.1-Win32.exe
+set capounix MetaPl-Capo10.1
+set gnuplotwin wgnuplot.exe
+set gnuplotunix gnuplot
+
+# standard aliases
+alias b balance
+alias cl cleanup
+alias clp collapse
+alias esd ext_seq_dcs
+alias f fraig
+alias fs fraig_sweep
+alias fsto fraig_store
+alias fres fraig_restore
+alias ft fraig_trust
+alias lp lutpack
+alias pd print_dsd
+alias pex print_exdc -d
+alias pf print_factor
+alias pfan print_fanio
+alias pl print_level
+alias pio print_io
+alias pk print_kmap
+alias ps print_stats 
+alias psu print_supp
+alias psy print_symm
+alias pun print_unate
+alias q quit
+alias r read
+alias r3 retime -M 3
+alias r3f retime -M 3 -f
+alias r3b retime -M 3 -b
+alias ren renode
+alias rh read_hie
+alias rl read_blif
+alias rb read_bench
+alias ret retime
+alias dret dretime
+alias rp read_pla
+alias rt read_truth
+alias rv read_verilog
+alias rvl read_verlib
+alias rsup read_super mcnc5_old.super
+alias rlib read_library
+alias rlibc read_library cadence.genlib
+alias rw rewrite
+alias rwz rewrite -z
+alias rf refactor
+alias rfz refactor -z
+alias re restructure
+alias rez restructure -z
+alias rs resub
+alias rsz resub -z
+alias sa set autoexec ps
+alias scl scleanup
+alias sif if -s
+alias so source -x
+alias st strash
+alias sw sweep
+alias ssw ssweep
+alias tr0 trace_start
+alias tr1 trace_check
+alias trt "r c.blif; st; tr0; b; tr1"
+alias u undo
+alias w write
+alias wa write_aiger
+alias wb write_bench
+alias wc write_cnf
+alias wh write_hie
+alias wl write_blif
+alias wp write_pla
+alias wv write_verilog
+
+# standard scripts
+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"
+alias choice      "fraig_store; resyn; fraig_store; resyn2; fraig_store; fraig_restore"
+alias choice2     "fraig_store; balance; fraig_store; resyn; fraig_store; resyn2; fraig_store; resyn2; fraig_store; fraig_restore"
+alias rwsat       "st; rw -l; b -l; rw -l; rf -l"
+alias rwsat2      "st; rw -l; b -l; rw -l; rf -l; fraig; rw -l; b -l; rw -l; rf -l"
+alias shake       "st; ps; sat -C 5000; rw -l; ps; sat -C 5000; b -l; rf -l; ps; sat -C 5000; rfz -l; ps; sat -C 5000; rwz -l; ps; sat -C 5000; rfz -l; ps; sat -C 5000"
+alias share       "st; multi -m; fx; resyn2"
+
+# resubstitution scripts for the IWLS paper
+alias src_rw      "st; rw -l; rwz -l; rwz -l" 
+alias src_rs      "st; rs -K 6 -N 2 -l; rs -K 9 -N 2 -l; rs -K 12 -N 2 -l" 
+alias src_rws     "st; rw -l; rs -K 6 -N 2 -l; rwz -l; rs -K 9 -N 2 -l; rwz -l; rs -K 12 -N 2 -l" 
+alias resyn2rs    "b; rs -K 6; rw; rs -K 6 -N 2; rf; rs -K 8; b; rs -K 8 -N 2; rw; rs -K 10; rwz; rs -K 10 -N 2; b; rs -K 12; rfz; rs -K 12 -N 2; rwz; b"
+alias compress2rs "b -l; rs -K 6 -l; rw -l; rs -K 6 -N 2 -l; rf -l; rs -K 8 -l; b -l; rs -K 8 -N 2 -l; rw -l; rs -K 10 -l; rwz -l; rs -K 10 -N 2 -l; b -l; rs -K 12 -l; rfz -l; rs -K 12 -N 2 -l; rwz -l; b -l"
+
+# experimental implementation of don't-cares
+alias resyn2rsdc    "b; rs -K 6 -F 2; rw; rs -K 6 -N 2 -F 2; rf; rs -K 8 -F 2; b; rs -K 8 -N 2 -F 2; rw; rs -K 10 -F 2; rwz; rs -K 10 -N 2 -F 2; b; rs -K 12 -F 2; rfz; rs -K 12 -N 2 -F 2; rwz; b"
+alias compress2rsdc "b -l; rs -K 6 -F 2 -l; rw -l; rs -K 6 -N 2 -F 2 -l; rf -l; rs -K 8 -F 2 -l; b -l; rs -K 8 -N 2 -F 2 -l; rw -l; rs -K 10 -F 2 -l; rwz -l; rs -K 10 -N 2 -F 2 -l; b -l; rs -K 12 -F 2 -l; rfz -l; rs -K 12 -N 2 -F 2 -l; rwz -l; b -l"
+
+# temporaries
+alias reach    "st; ps; compress2; ps; qrel; ps; compress2; ps; qreach -v; ps"
+alias chnew    "st; haig_start; resyn2; haig_use"
+alias chnewrs  "st; haig_start; resyn2rs; haig_use"
+alias stdsd    "r test/6in.blif; st; ps; u; bdd; dsd -g; st; ps"
+alias trec     "rec_start; r c.blif; st; rec_add; rec_use"
+alias trec4    "rec_start -K 4; r i10.blif; st; rec_add; rec_use"
+alias bmc2     "frames -i -F 10; orpos; iprove"
+
+alias t0       "r test/mc1.blif; st; test"
+alias t1       "r s27mc2.blif; st; test"
+alias t2       "r i/intel_001.aig; ps; indcut -v"
+
diff --git a/src/aig/aig/aig.h b/src/aig/aig/aig.h
index 6b34e853..28bae70f 100644
--- a/src/aig/aig/aig.h
+++ b/src/aig/aig/aig.h
@@ -388,6 +388,7 @@ extern void            Aig_ManCheckMarkA( Aig_Man_t * p );
 extern void            Aig_ManCheckPhase( Aig_Man_t * p );
 /*=== aigDfs.c ==========================================================*/
 extern Vec_Ptr_t *     Aig_ManDfs( Aig_Man_t * p );
+extern Vec_Ptr_t *     Aig_ManDfsPio( Aig_Man_t * p );
 extern Vec_Ptr_t *     Aig_ManDfsNodes( Aig_Man_t * p, Aig_Obj_t ** ppNodes, int nNodes );
 extern Vec_Ptr_t *     Aig_ManDfsChoices( Aig_Man_t * p );
 extern Vec_Ptr_t *     Aig_ManDfsReverse( Aig_Man_t * p );
@@ -555,16 +556,17 @@ extern int             Aig_MmStepReadMemUsage( Aig_MmStep_t * p );
 /*=== aigTime.c ===========================================================*/
 extern Aig_TMan_t *    Aig_TManStart( int nPis, int nPos );
 extern void            Aig_TManStop( Aig_TMan_t * p );
-extern void            Aig_TManCreateBox( Aig_TMan_t * p, int * pPis, int nPis, int * pPos, int nPos, float * pPiTimes, float * pPoTimes );
-extern void            Aig_TManSetPiDelay( Aig_TMan_t * p, int iPi, float Delay );
-extern void            Aig_TManSetPoDelay( Aig_TMan_t * p, int iPo, float Delay );
-extern void            Aig_TManSetPiArrival( Aig_TMan_t * p, int iPi, float Delay );
-extern void            Aig_TManSetPoRequired( Aig_TMan_t * p, int iPo, float Delay );
+extern void            Aig_TManSetDelayTables( Aig_TMan_t * p, Vec_Ptr_t * vDelayTables );
+extern void            Aig_TManCreateBox( Aig_TMan_t * p, int * pIns, int nIns, int * pOuts, int nOuts, float * pDelayTable );
+extern void            Aig_TManCreateBoxFirst( Aig_TMan_t * p, int firstIn, int nIns, int firstOut, int nOuts, float * pDelayTable );
 extern void            Aig_TManIncrementTravId( Aig_TMan_t * p );
+extern void            Aig_TManInitPiArrival( Aig_TMan_t * p, int iPi, float Delay );
+extern void            Aig_TManInitPoRequired( Aig_TMan_t * p, int iPo, float Delay );
+extern void            Aig_TManSetPoArrival( Aig_TMan_t * p, int iPo, float Delay );
+extern void            Aig_TManSetPiRequired( Aig_TMan_t * p, int iPi, float Delay );
 extern float           Aig_TManGetPiArrival( Aig_TMan_t * p, int iPi );
 extern float           Aig_TManGetPoRequired( Aig_TMan_t * p, int iPo );
 
-
 #ifdef __cplusplus
 }
 #endif
diff --git a/src/aig/aig/aigDfs.c b/src/aig/aig/aigDfs.c
index dedfeb4a..c7488487 100644
--- a/src/aig/aig/aigDfs.c
+++ b/src/aig/aig/aigDfs.c
@@ -46,7 +46,7 @@ void Aig_ManDfs_rec( Aig_Man_t * p, Aig_Obj_t * pObj, Vec_Ptr_t * vNodes )
     assert( !Aig_IsComplement(pObj) );
     if ( Aig_ObjIsTravIdCurrent(p, pObj) )
         return;
-    assert( Aig_ObjIsNode(pObj) || Aig_ObjIsBuf(pObj) );
+//    assert( Aig_ObjIsNode(pObj) || Aig_ObjIsBuf(pObj) );
     Aig_ManDfs_rec( p, Aig_ObjFanin0(pObj), vNodes );
     Aig_ManDfs_rec( p, Aig_ObjFanin1(pObj), vNodes );
     assert( !Aig_ObjIsTravIdCurrent(p, pObj) ); // loop detection
@@ -99,6 +99,29 @@ Vec_Ptr_t * Aig_ManDfs( Aig_Man_t * p )
   SeeAlso     []
 
 ***********************************************************************/
+Vec_Ptr_t * Aig_ManDfsPio( Aig_Man_t * p )
+{
+    Vec_Ptr_t * vNodes;
+    Aig_Obj_t * pObj;
+    int i;
+    Aig_ManIncrementTravId( p );
+    vNodes = Vec_PtrAlloc( Aig_ManObjNumMax(p) );
+    Aig_ManForEachPo( p, pObj, i )
+        Aig_ManDfs_rec( p, pObj, vNodes );
+    return vNodes;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Collects internal nodes in the DFS order.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
 Vec_Ptr_t * Aig_ManDfsNodes( Aig_Man_t * p, Aig_Obj_t ** ppNodes, int nNodes )
 {
     Vec_Ptr_t * vNodes;
diff --git a/src/aig/aig/aigTime.c b/src/aig/aig/aigTime.c
index 42f5f575..1544a15b 100644
--- a/src/aig/aig/aigTime.c
+++ b/src/aig/aig/aigTime.c
@@ -31,6 +31,7 @@ typedef struct Aig_TObj_t_           Aig_TObj_t;
 struct Aig_TMan_t_
 {
     Vec_Ptr_t *      vBoxes;         // the timing boxes
+    Vec_Ptr_t *      vDelayTables;   // pointers to the delay tables
     Aig_MmFlex_t *   pMemObj;        // memory manager for boxes
     int              nTravIds;       // traversal ID of the manager
     int              nPis;           // the number of PIs
@@ -44,17 +45,20 @@ struct Aig_TBox_t_
 {
     int              iBox;           // the unique ID of this box
     int              TravId;         // traversal ID of this box
-    int              nInputs;        // the number of box inputs 
-    int              nOutputs;       // the number of box outputs
+    int              nInputs;        // the number of box inputs (POs)
+    int              nOutputs;       // the number of box outputs (PIs)
+    float *          pDelayTable;    // delay for each input->output path
     int              Inouts[0];      // the int numbers of PIs and POs
 };
 
 // timing object
 struct Aig_TObj_t_
 {
+    int              TravId;         // traversal ID of this object
     int              iObj2Box;       // mapping of the object into its box
-    float            timeOffset;     // the static timing of the node
-    float            timeActual;     // the actual timing of the node
+    int              iObj2Num;       // mapping of the object into its number in the box
+    float            timeArr;        // arrival time of the object
+    float            timeReq;        // required time of the object
 };
 
 ////////////////////////////////////////////////////////////////////////
@@ -88,9 +92,9 @@ Aig_TMan_t * Aig_TManStart( int nPis, int nPos )
     p->pPos = ALLOC( Aig_TObj_t, nPos );
     memset( p->pPos, 0, sizeof(Aig_TObj_t) * nPos );
     for ( i = 0; i < nPis; i++ )
-        p->pPis[i].iObj2Box = -1;
+        p->pPis[i].iObj2Box = p->pPis[i].iObj2Num = -1;
     for ( i = 0; i < nPos; i++ )
-        p->pPos[i].iObj2Box = -1;
+        p->pPos[i].iObj2Box = p->pPos[i].iObj2Num = -1;
     return p;
 }
 
@@ -107,6 +111,14 @@ Aig_TMan_t * Aig_TManStart( int nPis, int nPos )
 ***********************************************************************/
 void Aig_TManStop( Aig_TMan_t * p )
 {
+    float * pTable;
+    int i;
+    if ( p->vDelayTables )
+    {
+        Vec_PtrForEachEntry( p->vDelayTables, pTable, i )
+            FREE( pTable );
+        Vec_PtrFree( p->vDelayTables );
+    }
     Vec_PtrFree( p->vBoxes );
     Aig_MmFlexStop( p->pMemObj, 0 );
     free( p->pPis );
@@ -116,6 +128,23 @@ void Aig_TManStop( Aig_TMan_t * p )
 
 /**Function*************************************************************
 
+  Synopsis    [Increments the trav ID of the manager.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Aig_TManSetDelayTables( Aig_TMan_t * p, Vec_Ptr_t * vDelayTables )
+{
+    assert( p->vDelayTables == NULL );
+    p->vDelayTables = vDelayTables;
+}
+
+/**Function*************************************************************
+
   Synopsis    [Creates the new timing box.]
 
   Description []
@@ -125,29 +154,30 @@ void Aig_TManStop( Aig_TMan_t * p )
   SeeAlso     []
 
 ***********************************************************************/
-void Aig_TManCreateBox( Aig_TMan_t * p, int * pPis, int nPis, int * pPos, int nPos, float * pPiTimes, float * pPoTimes )
+void Aig_TManCreateBox( Aig_TMan_t * p, int * pIns, int nIns, int * pOuts, int nOuts, float * pDelayTable )
 {
     Aig_TBox_t * pBox;
     int i;
-    pBox = (Aig_TBox_t *)Aig_MmFlexEntryFetch( p->pMemObj, sizeof(Aig_TBox_t) + sizeof(int) * (nPis+nPos) );
+    pBox = (Aig_TBox_t *)Aig_MmFlexEntryFetch( p->pMemObj, sizeof(Aig_TBox_t) + sizeof(int) * (nIns+nOuts) );
     memset( pBox, 0, sizeof(Aig_TBox_t) );
     pBox->iBox = Vec_PtrSize( p->vBoxes );
     Vec_PtrPush( p->vBoxes, pBox );
-    pBox->nInputs = nPis;
-    pBox->nOutputs = nPos;
-    for ( i = 0; i < nPis; i++ )
+    pBox->pDelayTable = pDelayTable;
+    pBox->nInputs  = nIns;
+    pBox->nOutputs = nOuts;
+    for ( i = 0; i < nIns; i++ )
     {
-        assert( pPis[i] < p->nPis );
-        pBox->Inouts[i] = pPis[i];
-        Aig_TManSetPiArrival( p, pPis[i], pPiTimes[i] );
-        p->pPis[pPis[i]].iObj2Box = pBox->iBox;
+        assert( pIns[i] < p->nPos );
+        pBox->Inouts[i] = pIns[i];
+        p->pPos[pIns[i]].iObj2Box = pBox->iBox;
+        p->pPos[pIns[i]].iObj2Num = i;
     }
-    for ( i = 0; i < nPos; i++ )
+    for ( i = 0; i < nOuts; i++ )
     {
-        assert( pPos[i] < p->nPos );
-        pBox->Inouts[nPis+i] = pPos[i];
-        Aig_TManSetPoRequired( p, pPos[i], pPoTimes[i] );
-        p->pPos[pPos[i]].iObj2Box = pBox->iBox;
+        assert( pOuts[i] < p->nPis );
+        pBox->Inouts[nIns+i] = pOuts[i];
+        p->pPis[pOuts[i]].iObj2Box = pBox->iBox;
+        p->pPis[pOuts[i]].iObj2Num = i;
     }
 }
 
@@ -162,15 +192,38 @@ void Aig_TManCreateBox( Aig_TMan_t * p, int * pPis, int nPis, int * pPos, int nP
   SeeAlso     []
 
 ***********************************************************************/
-void Aig_TManSetPiDelay( Aig_TMan_t * p, int iPi, float Delay )
+void Aig_TManCreateBoxFirst( Aig_TMan_t * p, int firstIn, int nIns, int firstOut, int nOuts, float * pDelayTable )
 {
-    assert( iPi < p->nPis );
-    p->pPis[iPi].timeActual = Delay;
+    Aig_TBox_t * pBox;
+    int i;
+    pBox = (Aig_TBox_t *)Aig_MmFlexEntryFetch( p->pMemObj, sizeof(Aig_TBox_t) + sizeof(int) * (nIns+nOuts) );
+    memset( pBox, 0, sizeof(Aig_TBox_t) );
+    pBox->iBox = Vec_PtrSize( p->vBoxes );
+    Vec_PtrPush( p->vBoxes, pBox );
+    pBox->pDelayTable = pDelayTable;
+    pBox->nInputs  = nIns;
+    pBox->nOutputs = nOuts;
+    for ( i = 0; i < nIns; i++ )
+    {
+        assert( firstIn+i < p->nPos );
+        pBox->Inouts[i] = firstIn+i;
+        p->pPos[firstIn+i].iObj2Box = pBox->iBox;
+        p->pPos[firstIn+i].iObj2Num = i;
+    }
+    for ( i = 0; i < nOuts; i++ )
+    {
+        assert( firstOut+i < p->nPis );
+        pBox->Inouts[nIns+i] = firstOut+i;
+        p->pPis[firstOut+i].iObj2Box = pBox->iBox;
+        p->pPis[firstOut+i].iObj2Num = i;
+    }
 }
 
+
+
 /**Function*************************************************************
 
-  Synopsis    [Creates the new timing box.]
+  Synopsis    [Increments the trav ID of the manager.]
 
   Description []
                
@@ -179,10 +232,9 @@ void Aig_TManSetPiDelay( Aig_TMan_t * p, int iPi, float Delay )
   SeeAlso     []
 
 ***********************************************************************/
-void Aig_TManSetPoDelay( Aig_TMan_t * p, int iPo, float Delay )
+void Aig_TManIncrementTravId( Aig_TMan_t * p )
 {
-    assert( iPo < p->nPos );
-    p->pPos[iPo].timeActual = Delay;
+    p->nTravIds++;
 }
 
 /**Function*************************************************************
@@ -196,10 +248,10 @@ void Aig_TManSetPoDelay( Aig_TMan_t * p, int iPo, float Delay )
   SeeAlso     []
 
 ***********************************************************************/
-void Aig_TManSetPiArrival( Aig_TMan_t * p, int iPi, float Delay )
+void Aig_TManInitPiArrival( Aig_TMan_t * p, int iPi, float Delay )
 {
     assert( iPi < p->nPis );
-    p->pPis[iPi].timeOffset = Delay;
+    p->pPis[iPi].timeArr = Delay;
 }
 
 /**Function*************************************************************
@@ -213,15 +265,15 @@ void Aig_TManSetPiArrival( Aig_TMan_t * p, int iPi, float Delay )
   SeeAlso     []
 
 ***********************************************************************/
-void Aig_TManSetPoRequired( Aig_TMan_t * p, int iPo, float Delay )
+void Aig_TManInitPoRequired( Aig_TMan_t * p, int iPo, float Delay )
 {
     assert( iPo < p->nPos );
-    p->pPos[iPo].timeOffset = Delay;
+    p->pPos[iPo].timeArr = Delay;
 }
 
 /**Function*************************************************************
 
-  Synopsis    [Increments the trav ID of the manager.]
+  Synopsis    [Creates the new timing box.]
 
   Description []
                
@@ -230,9 +282,12 @@ void Aig_TManSetPoRequired( Aig_TMan_t * p, int iPo, float Delay )
   SeeAlso     []
 
 ***********************************************************************/
-void Aig_TManIncrementTravId( Aig_TMan_t * p )
+void Aig_TManSetPoArrival( Aig_TMan_t * p, int iPo, float Delay )
 {
-    p->nTravIds++;
+    assert( iPo < p->nPos );
+    assert( p->pPos[iPo].TravId != p->nTravIds );
+    p->pPos[iPo].timeArr = Delay;
+    p->pPos[iPo].TravId = p->nTravIds;
 }
 
 /**Function*************************************************************
@@ -250,29 +305,62 @@ float Aig_TManGetPiArrival( Aig_TMan_t * p, int iPi )
 {
     Aig_TBox_t * pBox;
     Aig_TObj_t * pObj;
+    float * pDelays;
     float DelayMax;
-    int i;
+    int i, k;
     assert( iPi < p->nPis );
     if ( p->pPis[iPi].iObj2Box < 0 )
-        return p->pPis[iPi].timeOffset;
+        return p->pPis[iPi].timeArr;
     pBox = Vec_PtrEntry( p->vBoxes, p->pPis[iPi].iObj2Box );
     // check if box timing is updated
     if ( pBox->TravId == p->nTravIds )
-        return p->pPis[iPi].timeOffset;
+    {
+        assert( pBox->TravId == p->nTravIds );
+        return p->pPis[iPi].timeArr;
+    }
     pBox->TravId = p->nTravIds;
     // update box timing
-    DelayMax = -1.0e+20F;
-    for ( i = 0; i < pBox->nOutputs; i++ )
+    // get the arrival times of the inputs of the box (POs)
+    for ( i = 0; i < pBox->nInputs; i++ )
     {
-        pObj = p->pPos + pBox->Inouts[pBox->nInputs+i];
-        DelayMax = AIG_MAX( DelayMax, pObj->timeActual + pObj->timeOffset );
+        pObj = p->pPos + pBox->Inouts[i];
+        if ( pObj->TravId != p->nTravIds )
+            printf( "Aig_TManGetPiArrival(): PO arrival times of the box are not up to date!\n" );
     }
-    for ( i = 0; i < pBox->nInputs; i++ )
+    // compute the required times for each output of the box (PIs)
+    for ( i = 0; i < pBox->nOutputs; i++ )
     {
-        pObj = p->pPis + pBox->Inouts[i];
-        pObj->timeActual = DelayMax + pObj->timeOffset;
+        pDelays = pBox->pDelayTable + i * pBox->nInputs;
+        DelayMax = -AIG_INFINITY;
+        for ( k = 0; k < pBox->nInputs; k++ )
+        {
+            pObj = p->pPos + pBox->Inouts[k];
+            DelayMax = AIG_MAX( DelayMax, pObj->timeArr + pDelays[k] );
+        }
+        pObj = p->pPis + pBox->Inouts[pBox->nInputs+i];
+        pObj->timeArr = DelayMax;
+        pObj->TravId = p->nTravIds;
     }
-    return p->pPis[iPi].timeActual;
+    return p->pPis[iPi].timeArr;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Returns PO required time.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Aig_TManSetPiRequired( Aig_TMan_t * p, int iPi, float Delay )
+{
+    assert( iPi < p->nPis );
+    assert( p->pPis[iPi].TravId != p->nTravIds );
+    p->pPis[iPi].timeReq = Delay;
+    p->pPis[iPi].TravId = p->nTravIds;
 }
 
 /**Function*************************************************************
diff --git a/src/aig/ntl/module.make b/src/aig/ntl/module.make
index ea6070a4..f47108a4 100644
--- a/src/aig/ntl/module.make
+++ b/src/aig/ntl/module.make
@@ -1,10 +1,11 @@
-SRC +=    src/aig/mem/ntlAig.c \
-    src/aig/mem/ntlCheck.c \
-    src/aig/mem/ntlDfs.c \
-    src/aig/mem/ntlMan.c \
-    src/aig/mem/ntlMap.c \
-    src/aig/mem/ntlObj.c \
-    src/aig/mem/ntlReadBlif.c \
-    src/aig/mem/ntlTable.c \
-    src/aig/mem/ntlWriteBlif.c
+SRC +=    src/aig/ntl/ntlAig.c \
+    src/aig/ntl/ntlCheck.c \
+    src/aig/ntl/ntlDfs.c \
+    src/aig/ntl/ntlMan.c \
+    src/aig/ntl/ntlMap.c \
+    src/aig/ntl/ntlObj.c \
+    src/aig/ntl/ntlReadBlif.c \
+    src/aig/ntl/ntlTable.c \
+    src/aig/ntl/ntlTime.c \
+    src/aig/ntl/ntlWriteBlif.c
 
diff --git a/src/aig/ntl/ntl.h b/src/aig/ntl/ntl.h
index af1e114d..ab93895d 100644
--- a/src/aig/ntl/ntl.h
+++ b/src/aig/ntl/ntl.h
@@ -47,13 +47,13 @@ typedef struct Ntl_Lut_t_    Ntl_Lut_t;
 
 // object types
 typedef enum { 
-    NTL_OBJ_NONE,                     // 0: non-existent object
-    NTL_OBJ_PI,                       // 1: primary input
-    NTL_OBJ_PO,                       // 2: primary output
-    NTL_OBJ_LATCH,                    // 3: latch node
-    NTL_OBJ_NODE,                     // 4: logic node
-    NTL_OBJ_BOX,                      // 5: white box or black box
-    NTL_OBJ_VOID                      // 6: unused object
+    NTL_OBJ_NONE,                      // 0: non-existent object
+    NTL_OBJ_PI,                        // 1: primary input
+    NTL_OBJ_PO,                        // 2: primary output
+    NTL_OBJ_LATCH,                     // 3: latch node
+    NTL_OBJ_NODE,                      // 4: logic node
+    NTL_OBJ_BOX,                       // 5: white box or black box
+    NTL_OBJ_VOID                       // 6: unused object
 } Ntl_Type_t;
 
 struct Ntl_Man_t_
@@ -88,6 +88,9 @@ struct Ntl_Mod_t_
     int                nEntries;       // the number of entries in the hash table
     // delay information
     Vec_Int_t *        vDelays;
+    Vec_Int_t *        vArrivals;
+    Vec_Int_t *        vRequireds;
+    float *            pDelayTable;   
 }; 
 
 struct Ntl_Obj_t_
@@ -148,8 +151,8 @@ static inline char *      Ntl_ModelPoName( Ntl_Mod_t * p, int i ) { return Ntl_M
 
 static inline int         Ntl_ModelIsBlackBox( Ntl_Mod_t * p )    { return Ntl_ModelPiNum(p) + Ntl_ModelPoNum(p) == Vec_PtrSize(p->vObjs); } 
 
-static inline int         Ntl_ObjNumFanins( Ntl_Obj_t * p )       { return p->nFanins;                          } 
-static inline int         Ntl_ObjNumFanouts( Ntl_Obj_t * p )      { return p->nFanouts;                         } 
+static inline int         Ntl_ObjFaninNum( Ntl_Obj_t * p )        { return p->nFanins;                          } 
+static inline int         Ntl_ObjFanoutNum( Ntl_Obj_t * p )       { return p->nFanouts;                         } 
 
 static inline int         Ntl_ObjIsPi( Ntl_Obj_t * p )            { return p->Type == NTL_OBJ_PI;               } 
 static inline int         Ntl_ObjIsPo( Ntl_Obj_t * p )            { return p->Type == NTL_OBJ_PO;               } 
@@ -224,8 +227,9 @@ extern void            Ntl_ModelFixNonDrivenNets( Ntl_Mod_t * pModel );
 extern int             Ntl_ManDfs( Ntl_Man_t * p );
 /*=== ntlMan.c ============================================================*/
 extern Ntl_Man_t *     Ntl_ManAlloc( char * pFileName );
-extern Ntl_Mod_t *     Ntl_ManFindModel( Ntl_Man_t * p, char * pName );
 extern void            Ntl_ManFree( Ntl_Man_t * p );
+extern Ntl_Mod_t *     Ntl_ManFindModel( Ntl_Man_t * p, char * pName );
+extern void            Ntl_ManPrintStats( Ntl_Man_t * p );
 extern Ntl_Mod_t *     Ntl_ModelAlloc( Ntl_Man_t * pMan, char * pName );
 extern void            Ntl_ModelFree( Ntl_Mod_t * p );
 /*=== ntlMap.c ============================================================*/
diff --git a/src/aig/ntl/ntlDfs.c b/src/aig/ntl/ntlDfs.c
index 6b5dc407..41867b29 100644
--- a/src/aig/ntl/ntlDfs.c
+++ b/src/aig/ntl/ntlDfs.c
@@ -100,7 +100,7 @@ int Ntl_ManDfs( Ntl_Man_t * p )
     // collect primary inputs
     Ntl_ModelForEachPi( pRoot, pObj, i )
     {
-        assert( Ntl_ObjNumFanouts(pObj) == 1 );
+        assert( Ntl_ObjFanoutNum(pObj) == 1 );
         pNet = Ntl_ObjFanout0(pObj);
         Vec_PtrPush( p->vCis, pNet );
         if ( pNet->nVisits )
@@ -113,7 +113,7 @@ int Ntl_ManDfs( Ntl_Man_t * p )
     // collect latch outputs
     Ntl_ModelForEachLatch( pRoot, pObj, i )
     {
-        assert( Ntl_ObjNumFanouts(pObj) == 1 );
+        assert( Ntl_ObjFanoutNum(pObj) == 1 );
         pNet = Ntl_ObjFanout0(pObj);
         Vec_PtrPush( p->vCis, pNet );
         if ( pNet->nVisits )
diff --git a/src/aig/ntl/ntlMan.c b/src/aig/ntl/ntlMan.c
index 6d71adb2..ce008c9c 100644
--- a/src/aig/ntl/ntlMan.c
+++ b/src/aig/ntl/ntlMan.c
@@ -111,6 +111,31 @@ Ntl_Mod_t * Ntl_ManFindModel( Ntl_Man_t * p, char * pName )
 
 /**Function*************************************************************
 
+  Synopsis    [Deallocates the netlist manager.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Ntl_ManPrintStats( Ntl_Man_t * p )
+{
+    Ntl_Mod_t * pRoot;
+    pRoot = Vec_PtrEntry( p->vModels, 0 );
+    printf( "%-15s : ",       p->pName );
+    printf( "pi = %5d  ",    Ntl_ModelPiNum(pRoot) );
+    printf( "po = %5d  ",    Ntl_ModelPoNum(pRoot) );
+    printf( "latch = %5d  ", Ntl_ModelLatchNum(pRoot) );
+    printf( "node = %5d  ",  Ntl_ModelNodeNum(pRoot) );
+    printf( "box = %4d  ",   Ntl_ModelBoxNum(pRoot) );
+    printf( "model = %3d",   Vec_PtrSize(p->vModels) );
+    printf( "\n" );
+}
+
+/**Function*************************************************************
+
   Synopsis    [Allocates the model.]
 
   Description []
@@ -152,7 +177,9 @@ Ntl_Mod_t * Ntl_ModelAlloc( Ntl_Man_t * pMan, char * pName )
 ***********************************************************************/
 void Ntl_ModelFree( Ntl_Mod_t * p )
 {
-    if ( p->vDelays ) Vec_IntFree( p->vDelays );
+    if ( p->vRequireds )  Vec_IntFree( p->vRequireds );
+    if ( p->vArrivals )   Vec_IntFree( p->vArrivals );
+    if ( p->vDelays )     Vec_IntFree( p->vDelays );
     Vec_PtrFree( p->vObjs );
     Vec_PtrFree( p->vPis );
     Vec_PtrFree( p->vPos );
diff --git a/src/aig/ntl/ntlMap.c b/src/aig/ntl/ntlMap.c
index 1d8443b4..7ee0fba0 100644
--- a/src/aig/ntl/ntlMap.c
+++ b/src/aig/ntl/ntlMap.c
@@ -19,6 +19,7 @@
 ***********************************************************************/
 
 #include "ntl.h"
+#include "kit.h"
 
 ////////////////////////////////////////////////////////////////////////
 ///                        DECLARATIONS                              ///
@@ -103,6 +104,443 @@ Vec_Ptr_t * Ntl_MappingFromAig( Aig_Man_t * p )
     return vMapping;
 }
 
+
+#include "fpgaInt.h"
+
+/**Function*************************************************************
+
+  Synopsis    [Recursively derives the truth table for the cut.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+unsigned * Ntl_FpgaComputeTruth_rec( Fpga_Cut_t * pCut, Vec_Ptr_t * vTruthElem, Vec_Ptr_t * vTruthStore, Vec_Ptr_t * vVisited, int nVars, int * pnCounter )
+{
+    unsigned * pTruth, * pTruth0, * pTruth1;
+    assert( !Fpga_IsComplement(pCut) );
+    // if the cut is visited, return the result
+    if ( pCut->pRoot )
+        return (unsigned *)pCut->pRoot;
+    // compute the functions of the children
+    pTruth0 = Ntl_FpgaComputeTruth_rec( Fpga_CutRegular(pCut->pOne), vTruthElem, vTruthStore, vVisited, nVars, pnCounter );  
+    if ( Fpga_CutIsComplement(pCut->pOne) )
+        Kit_TruthNot( pTruth0, pTruth0, nVars );
+    pTruth1 = Ntl_FpgaComputeTruth_rec( Fpga_CutRegular(pCut->pTwo), vTruthElem, vTruthStore, vVisited, nVars, pnCounter );   
+    if ( Fpga_CutIsComplement(pCut->pTwo) )
+        Kit_TruthNot( pTruth1, pTruth1, nVars );
+    // get the function of the cut
+    pTruth = Vec_PtrEntry( vTruthStore, (*pnCounter)++ );
+    Kit_TruthAnd( pTruth, pTruth0, pTruth1, nVars );
+    if ( pCut->Phase )
+        Kit_TruthNot( pTruth, pTruth, nVars );
+    assert( pCut->pRoot == NULL );
+    pCut->pRoot = (Fpga_Node_t *)pTruth;
+    // add this cut to the visited list
+    Vec_PtrPush( vVisited, pCut );
+    return pTruth;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Derives the truth table for one cut.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+unsigned * Ntl_FpgaComputeTruth( Fpga_Cut_t * pCut, Vec_Ptr_t * vTruthElem, Vec_Ptr_t * vTruthStore, Vec_Ptr_t * vVisited, int nVars )
+{
+    unsigned * pTruth;
+    int i, nCounter = 0;
+    assert( pCut->nLeaves > 1 );
+    // set the leaf variables
+    for ( i = 0; i < pCut->nLeaves; i++ )
+        pCut->ppLeaves[i]->pCuts->pRoot = (Fpga_Node_t *)Vec_PtrEntry( vTruthElem, i );
+    // recursively compute the function
+    Vec_PtrClear( vVisited );
+    pTruth = Ntl_FpgaComputeTruth_rec( pCut, vTruthElem, vTruthStore, vVisited, nVars, &nCounter ); 
+    // clean the intermediate BDDs
+    for ( i = 0; i < pCut->nLeaves; i++ )
+        pCut->ppLeaves[i]->pCuts->pRoot = NULL;
+    Vec_PtrForEachEntry( vVisited, pCut, i )
+        pCut->pRoot = NULL;
+    return pTruth;
+}
+
+
+/**Function*************************************************************
+
+  Synopsis    [Load the network into FPGA manager.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Fpga_Man_t * Ntl_ManToFpga( Aig_Man_t * p )
+{
+    Fpga_Man_t * pMan;
+    Aig_Obj_t * pNode;//, * pFanin, * pPrev;
+    float * pfArrivals;
+    int i;
+    // start the mapping manager and set its parameters
+    pMan = Fpga_ManCreate( Aig_ManPiNum(p), Aig_ManPoNum(p), 0 );
+    if ( pMan == NULL )
+        return NULL;
+    // set the arrival times
+    pfArrivals = ALLOC( float, Aig_ManPiNum(p) );
+    memset( pfArrivals, 0, sizeof(float) * Aig_ManPiNum(p) );
+    Fpga_ManSetInputArrivals( pMan, pfArrivals );
+    // create PIs and remember them in the old nodes
+    Aig_ManConst1(p)->pData = Fpga_ManReadConst1(pMan);
+    Aig_ManForEachPi( p, pNode, i )
+        pNode->pData = Fpga_ManReadInputs(pMan)[i];
+    // load the AIG into the mapper
+    Aig_ManForEachNode( p, pNode, i )
+    {
+        pNode->pData = Fpga_NodeAnd( pMan, 
+            Fpga_NotCond( Aig_ObjFanin0(pNode)->pData, Aig_ObjFaninC0(pNode) ),
+            Fpga_NotCond( Aig_ObjFanin1(pNode)->pData, Aig_ObjFaninC1(pNode) ) );
+        // set up the choice node
+//        if ( Aig_AigNodeIsChoice( pNode ) )
+//            for ( pPrev = pNode, pFanin = pNode->pData; pFanin; pPrev = pFanin, pFanin = pFanin->pData )
+//            {
+//                Fpga_NodeSetNextE( (If_Obj_t *)pPrev->pData, (If_Obj_t *)pFanin->pData );
+//                Fpga_NodeSetRepr( (If_Obj_t *)pFanin->pData, (If_Obj_t *)pNode->pData );
+//            }
+    }
+    // set the primary outputs while copying the phase
+    Aig_ManForEachPo( p, pNode, i )
+        Fpga_ManReadOutputs(pMan)[i] = Fpga_NotCond( Aig_ObjFanin0(pNode)->pData, Aig_ObjFaninC0(pNode) );
+    assert( Fpga_NodeVecReadSize(pMan->vAnds) == Aig_ManNodeNum(p) );
+    return pMan;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Creates the mapped network.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Vec_Ptr_t * Ntl_ManFromFpga( Aig_Man_t * p, Fpga_Man_t * pMan )
+{
+    Fpga_NodeVec_t * vFpgaMap;
+    Fpga_Node_t ** ppLeaves, * pNode; 
+    Fpga_Cut_t * pCutBest;
+    Vec_Ptr_t * vTruthElem, * vTruthStore, * vVisited, * vMapping;
+    Vec_Int_t * vFpgaToAig;
+    Aig_Obj_t * pObj;
+    Ntl_Lut_t * pLut;
+    unsigned * pTruth;
+    int i, k = 0, nLeaves, nWords, nVarsMax;
+    // create mapping of FPGA nodes into AIG nodes
+    vFpgaToAig = Vec_IntStart( Aig_ManObjNumMax(p) );
+    Vec_IntFill( vFpgaToAig, Aig_ManObjNumMax(p), -1 );
+    Aig_ManForEachObj( p, pObj, i )
+    {
+        if ( Aig_ObjIsPo(pObj) )
+            continue;
+        pNode = pObj->pData;
+        assert( pNode != NULL );
+        Vec_IntWriteEntry( vFpgaToAig, Fpga_NodeReadNum(pNode), pObj->Id );
+    }
+    // create the mapping
+    nVarsMax = Fpga_ManReadVarMax( pMan );
+    nWords   = Aig_TruthWordNum( nVarsMax );
+    vFpgaMap = Fpga_ManReadMapping( pMan );
+    vMapping = Ntl_MappingAlloc( vFpgaMap->nSize + (int)(Aig_ManConst1(p)->nRefs > 0), nVarsMax );
+    if ( Aig_ManConst1(p)->nRefs > 0 )
+    {
+        pLut = Vec_PtrEntry( vMapping, k++ );
+        pLut->Id = 0;
+        pLut->nFanins = 0;
+        memset( pLut->pTruth, 0xFF, 4 * nWords );
+    }
+    vVisited    = Vec_PtrAlloc( 1000 );
+    vTruthElem  = Vec_PtrAllocTruthTables( nVarsMax );
+    vTruthStore = Vec_PtrAllocSimInfo( 256, nWords );
+    for ( i = 0; i < vFpgaMap->nSize; i++ )
+    {
+        // get the best cut
+        pNode    = vFpgaMap->pArray[i];
+        pCutBest = Fpga_NodeReadCutBest( pNode );
+        nLeaves  = Fpga_CutReadLeavesNum( pCutBest ); 
+        ppLeaves = Fpga_CutReadLeaves( pCutBest );
+        // fill the LUT
+        pLut = Vec_PtrEntry( vMapping, k++ );
+        pLut->Id = Vec_IntEntry( vFpgaToAig, Fpga_NodeReadNum(pNode) );
+        pLut->nFanins = nLeaves;
+        for ( k = 0; k < nLeaves; k++ )
+            pLut->pFanins[k] = Vec_IntEntry( vFpgaToAig, Fpga_NodeReadNum(ppLeaves[k]) );
+        // compute the truth table
+        pTruth = Ntl_FpgaComputeTruth( pCutBest, vTruthElem, vTruthStore, vVisited, nVarsMax );
+        memcpy( pLut->pTruth, pTruth, 4 * nWords );
+    }
+    assert( k == Vec_PtrSize(vMapping) );
+    Vec_IntFree( vFpgaToAig );
+    Vec_PtrFree( vVisited );
+    Vec_PtrFree( vTruthElem );
+    Vec_PtrFree( vTruthStore );
+    return vMapping;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Interface with the FPGA mapping package.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Vec_Ptr_t * Ntl_ManFpga( Aig_Man_t * p )
+{
+    Vec_Ptr_t * vMapping;
+    Fpga_Man_t * pMan;
+    // print a warning about choice nodes
+    if ( p->pEquivs )
+        printf( "Ntl_ManFpga(): Performing FPGA mapping with choices.\n" );
+    // perform FPGA mapping
+    pMan = Ntl_ManToFpga( p );    
+    if ( pMan == NULL )
+        return NULL;
+    if ( !Fpga_Mapping( pMan ) )
+    {
+        Fpga_ManFree( pMan );
+        return NULL;
+    }
+    // transform the result of mapping into a BDD network
+    vMapping = Ntl_ManFromFpga( p, pMan );
+    Fpga_ManFree( pMan );
+    if ( vMapping == NULL )
+        return NULL;
+    return vMapping;
+}
+
+
+
+
+#include "if.h"
+
+/**Function*************************************************************
+
+  Synopsis    [Load the network into FPGA manager.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Ntk_ManSetIfParsDefault( If_Par_t * pPars )
+{
+    extern void * Abc_FrameReadLibLut();
+    // set defaults
+    memset( pPars, 0, sizeof(If_Par_t) );
+    // user-controlable paramters
+    pPars->nLutSize    = -1;
+    pPars->nCutsMax    =  8;
+    pPars->nFlowIters  =  1;
+    pPars->nAreaIters  =  2;
+    pPars->DelayTarget = -1;
+    pPars->fPreprocess =  1;
+    pPars->fArea       =  0;
+    pPars->fFancy      =  0;
+    pPars->fExpRed     =  1;
+    pPars->fLatchPaths =  0;
+    pPars->fEdge       =  1;
+    pPars->fCutMin     =  1;
+    pPars->fSeqMap     =  0;
+    pPars->fVerbose    =  0;
+    // internal parameters
+    pPars->fTruth      =  1;
+    pPars->nLatches    =  0;
+    pPars->fLiftLeaves =  0;
+    pPars->pLutLib     =  Abc_FrameReadLibLut();
+    pPars->pTimesArr   =  NULL; 
+    pPars->pTimesArr   =  NULL;   
+    pPars->pFuncCost   =  NULL;   
+
+    if ( pPars->nLutSize == -1 )
+    {
+        if ( pPars->pLutLib == NULL )
+        {
+            printf( "The LUT library is not given.\n" );
+            return;
+        }
+        // get LUT size from the library
+        pPars->nLutSize = pPars->pLutLib->LutMax;
+    }
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Load the network into FPGA manager.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+If_Man_t * Ntk_ManToIf( Aig_Man_t * p, If_Par_t * pPars )
+{
+    If_Man_t * pIfMan;
+    Aig_Obj_t * pNode;//, * pFanin, * pPrev;
+    Vec_Ptr_t * vNodes;
+    int i;
+    // start the mapping manager and set its parameters
+    pIfMan = If_ManStart( pPars );
+    // print warning about excessive memory usage
+    if ( 1.0 * Aig_ManObjNum(p) * pIfMan->nObjBytes / (1<<30) > 1.0 )
+        printf( "Warning: The mapper will allocate %.1f Gb for to represent the subject graph with %d AIG nodes.\n", 
+            1.0 * Aig_ManObjNum(p) * pIfMan->nObjBytes / (1<<30), Aig_ManObjNum(p) );
+    // load the AIG into the mapper
+    vNodes = Aig_ManDfsPio( p );
+    Vec_PtrForEachEntry( vNodes, pNode, i )
+    {
+        if ( Aig_ObjIsConst1(pNode) )
+            Aig_ManConst1(p)->pData = If_ManConst1( pIfMan );
+        else if ( Aig_ObjIsPi(pNode) )
+            pNode->pData = If_ManCreateCi( pIfMan );
+        else if ( Aig_ObjIsPo(pNode) )
+            If_ManCreateCo( pIfMan, If_NotCond( Aig_ObjFanin0(pNode)->pData, Aig_ObjFaninC0(pNode) ) );
+        else // add the node to the mapper
+            pNode->pData = (Aig_Obj_t *)If_ManCreateAnd( pIfMan, 
+                If_NotCond( (If_Obj_t *)Aig_ObjFanin0(pNode)->pData, Aig_ObjFaninC0(pNode) ), 
+                If_NotCond( (If_Obj_t *)Aig_ObjFanin1(pNode)->pData, Aig_ObjFaninC1(pNode) ) );
+        // set up the choice node
+//        if ( Aig_AigNodeIsChoice( pNode ) )
+//        {
+//            pIfMan->nChoices++;
+//            for ( pPrev = pNode, pFanin = pNode->pData; pFanin; pPrev = pFanin, pFanin = pFanin->pData )
+//                If_ObjSetChoice( (If_Obj_t *)pPrev->pData, (If_Obj_t *)pFanin->pData );
+//            If_ManCreateChoice( pIfMan, (If_Obj_t *)pNode->pData );
+//        }
+    }
+    Vec_PtrFree( vNodes );
+    return pIfMan;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Creates the mapped network.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Vec_Ptr_t * Ntk_ManFromIf( Aig_Man_t * p, If_Man_t * pMan )
+{
+    Vec_Ptr_t * vIfMap;
+    If_Obj_t * pNode, * pLeaf; 
+    If_Cut_t * pCutBest;
+    Vec_Ptr_t * vMapping;
+    Vec_Int_t * vIfToAig;
+    Aig_Obj_t * pObj;
+    Ntl_Lut_t * pLut;
+    int * ppLeaves;
+    int i, k = 0, nLeaves, nWords, nVarsMax;
+    // create mapping of If nodes into AIG nodes
+    vIfToAig = Vec_IntStart( Aig_ManObjNumMax(p) );
+    Vec_IntFill( vIfToAig, Aig_ManObjNumMax(p), -1 );
+    Aig_ManForEachObj( p, pObj, i )
+    {
+        if ( Aig_ObjIsPo(pObj) )
+            continue;
+        pNode = pObj->pData;
+        assert( pNode != NULL );
+        Vec_IntWriteEntry( vIfToAig, pNode->Id, pObj->Id );
+    }
+    // create the mapping
+    nVarsMax = pMan->pPars->nLutSize;
+    nWords   = Aig_TruthWordNum( nVarsMax );
+    vIfMap   = pMan->vMapped;
+    vMapping = Ntl_MappingAlloc( Vec_PtrSize(vIfMap) + (int)(Aig_ManConst1(p)->nRefs > 0), nVarsMax );
+    if ( Aig_ManConst1(p)->nRefs > 0 )
+    {
+        pLut = Vec_PtrEntry( vMapping, k++ );
+        pLut->Id = 0;
+        pLut->nFanins = 0;
+        memset( pLut->pTruth, 0xFF, 4 * nWords );
+    }
+    Vec_PtrForEachEntry( vIfMap, pNode, i )
+    {
+        // get the best cut
+        pCutBest = If_ObjCutBest(pNode);
+        nLeaves  = If_CutLeaveNum( pCutBest ); 
+        ppLeaves = If_CutLeaves( pCutBest );
+        // fill the LUT
+        pLut = Vec_PtrEntry( vMapping, k++ );
+        pLut->Id = Vec_IntEntry( vIfToAig, pNode->Id );
+        pLut->nFanins = nLeaves;
+        If_CutForEachLeaf( pMan, pCutBest, pLeaf, k )
+            pLut->pFanins[k] = Vec_IntEntry( vIfToAig, pLeaf->Id );
+        // compute the truth table
+        memcpy( pLut->pTruth, If_CutTruth(pCutBest), 4 * nWords );
+    }
+    assert( k == Vec_PtrSize(vMapping) );
+    Vec_IntFree( vIfToAig );
+    return vMapping;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Interface with the FPGA mapping package.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Vec_Ptr_t * Ntk_ManIf( Aig_Man_t * p )
+{
+    Vec_Ptr_t * vMapping;
+    If_Par_t Pars, * pPars = &Pars;
+    If_Man_t * pIfMan;
+    // perform FPGA mapping
+    Ntk_ManSetIfParsDefault( pPars );
+    pIfMan = Ntk_ManToIf( p, pPars );    
+    if ( pIfMan == NULL )
+        return NULL;
+    if ( !If_ManPerformMapping( pIfMan ) )
+    {
+        If_ManStop( pIfMan );
+        return NULL;
+    }
+    // transform the result of mapping into the new network
+    vMapping = Ntk_ManFromIf( p, pIfMan );
+    If_ManStop( pIfMan );
+    if ( vMapping == NULL )
+        return NULL;
+    return vMapping;
+}
+
+
+
 ////////////////////////////////////////////////////////////////////////
 ///                       END OF FILE                                ///
 ////////////////////////////////////////////////////////////////////////
diff --git a/src/aig/ntl/ntlReadBlif.c b/src/aig/ntl/ntlReadBlif.c
index 7c6ed069..d085b5e6 100644
--- a/src/aig/ntl/ntlReadBlif.c
+++ b/src/aig/ntl/ntlReadBlif.c
@@ -37,6 +37,8 @@ struct Ioa_ReadMod_t_
     Vec_Ptr_t *          vNames;       // .names lines
     Vec_Ptr_t *          vSubckts;     // .subckt lines
     Vec_Ptr_t *          vDelays;      // .delay lines
+    Vec_Ptr_t *          vArrivals;    // .input_arrival lines
+    Vec_Ptr_t *          vRequireds;   // .output_required lines
     int                  fBlackBox;    // indicates blackbox model
     // the resulting network
     Ntl_Mod_t *          pNtk;   
@@ -73,7 +75,7 @@ static Ioa_ReadMod_t *   Ioa_ReadModAlloc();
 static void              Ioa_ReadModFree( Ioa_ReadMod_t * p );
 static char *            Ioa_ReadLoadFile( char * pFileName );
 static void              Ioa_ReadReadPreparse( Ioa_ReadMan_t * p );
-static void              Ioa_ReadReadInterfaces( Ioa_ReadMan_t * p );
+static int               Ioa_ReadReadInterfaces( Ioa_ReadMan_t * p );
 static Ntl_Man_t *       Ioa_ReadParse( Ioa_ReadMan_t * p );
 static int               Ioa_ReadParseLineModel( Ioa_ReadMod_t * p, char * pLine );
 static int               Ioa_ReadParseLineInputs( Ioa_ReadMod_t * p, char * pLine );
@@ -81,6 +83,7 @@ static int               Ioa_ReadParseLineOutputs( Ioa_ReadMod_t * p, char * pLi
 static int               Ioa_ReadParseLineLatch( Ioa_ReadMod_t * p, char * pLine );
 static int               Ioa_ReadParseLineSubckt( Ioa_ReadMod_t * p, char * pLine );
 static int               Ioa_ReadParseLineDelay( Ioa_ReadMod_t * p, char * pLine );
+static int               Ioa_ReadParseLineTimes( Ioa_ReadMod_t * p, char * pLine, int fOutput );
 static int               Ioa_ReadParseLineNamesBlif( Ioa_ReadMod_t * p, char * pLine );
 
 static int               Ioa_ReadCharIsSpace( char s )   { return s == ' ' || s == '\t' || s == '\r' || s == '\n';             }
@@ -132,13 +135,22 @@ Ntl_Man_t * Ioa_ReadBlif( char * pFileName, int fCheck )
     // prepare the file for parsing
     Ioa_ReadReadPreparse( p );
     // parse interfaces of each network
-    Ioa_ReadReadInterfaces( p );
+    if ( !Ioa_ReadReadInterfaces( p ) )
+    {
+        if ( p->sError[0] )
+            fprintf( stdout, "%s\n", p->sError );
+        Ioa_ReadFree( p );
+        return NULL;
+    }
     // construct the network
     pDesign = Ioa_ReadParse( p );
     if ( p->sError[0] )
         fprintf( stdout, "%s\n", p->sError );
     if ( pDesign == NULL )
+    {
+        Ioa_ReadFree( p );
         return NULL;
+    }
     p->pDesign = NULL;
     Ioa_ReadFree( p );
 // pDesign should be linked to all models of the design
@@ -248,6 +260,8 @@ static Ioa_ReadMod_t * Ioa_ReadModAlloc()
     p->vNames   = Vec_PtrAlloc( 512 );
     p->vSubckts = Vec_PtrAlloc( 512 );
     p->vDelays  = Vec_PtrAlloc( 512 );
+    p->vArrivals  = Vec_PtrAlloc( 512 );
+    p->vRequireds = Vec_PtrAlloc( 512 );
     return p;
 }
 
@@ -270,6 +284,8 @@ static void Ioa_ReadModFree( Ioa_ReadMod_t * p )
     Vec_PtrFree( p->vNames );
     Vec_PtrFree( p->vSubckts );
     Vec_PtrFree( p->vDelays );
+    Vec_PtrFree( p->vArrivals );
+    Vec_PtrFree( p->vRequireds );
     free( p );
 }
 
@@ -498,6 +514,10 @@ static void Ioa_ReadReadPreparse( Ioa_ReadMan_t * p )
             Vec_PtrPush( p->pLatest->vSubckts, pCur );
         else if ( !strncmp(pCur, "delay", 5) )
             Vec_PtrPush( p->pLatest->vDelays, pCur );
+        else if ( !strncmp(pCur, "input_arrival", 13) )
+            Vec_PtrPush( p->pLatest->vArrivals, pCur );
+        else if ( !strncmp(pCur, "output_required", 15) )
+            Vec_PtrPush( p->pLatest->vRequireds, pCur );
         else if ( !strncmp(pCur, "blackbox", 8) )
             p->pLatest->fBlackBox = 1;
         else if ( !strncmp(pCur, "model", 5) ) 
@@ -538,7 +558,7 @@ static void Ioa_ReadReadPreparse( Ioa_ReadMan_t * p )
   SeeAlso     []
 
 ***********************************************************************/
-static void Ioa_ReadReadInterfaces( Ioa_ReadMan_t * p )
+static int Ioa_ReadReadInterfaces( Ioa_ReadMan_t * p )
 {
     Ioa_ReadMod_t * pMod;
     char * pLine;
@@ -548,20 +568,27 @@ static void Ioa_ReadReadInterfaces( Ioa_ReadMan_t * p )
     {
         // parse the model
         if ( !Ioa_ReadParseLineModel( pMod, pMod->pFirst ) )
-            return;
+            return 0;
         // parse the inputs
         Vec_PtrForEachEntry( pMod->vInputs, pLine, k )
             if ( !Ioa_ReadParseLineInputs( pMod, pLine ) )
-                return;
+                return 0;
         // parse the outputs
         Vec_PtrForEachEntry( pMod->vOutputs, pLine, k )
             if ( !Ioa_ReadParseLineOutputs( pMod, pLine ) )
-                return;
+                return 0;
         // parse the delay info
         Vec_PtrForEachEntry( pMod->vDelays, pLine, k )
             if ( !Ioa_ReadParseLineDelay( pMod, pLine ) )
-                return;
+                return 0;
+        Vec_PtrForEachEntry( pMod->vArrivals, pLine, k )
+            if ( !Ioa_ReadParseLineTimes( pMod, pLine, 0 ) )
+                return 0;
+        Vec_PtrForEachEntry( pMod->vRequireds, pLine, k )
+            if ( !Ioa_ReadParseLineTimes( pMod, pLine, 1 ) )
+                return 0;
     }
+    return 1;
 }
 
 
@@ -626,7 +653,7 @@ static int Ioa_ReadParseLineModel( Ioa_ReadMod_t * p, char * pLine )
     assert( !strcmp(pToken, "model") );
     if ( Vec_PtrSize(vTokens) != 2 )
     {
-        sprintf( p->pMan->sError, "Line %d: Model line has %d entries while it should have 2.", Ioa_ReadGetLine(p->pMan, pToken), Vec_PtrSize(vTokens) );
+        sprintf( p->pMan->sError, "Line %d: The number of entries in .model line (%d) is different from two.", Ioa_ReadGetLine(p->pMan, pToken), Vec_PtrSize(vTokens) );
         return 0;
     }
     p->pNtk = Ntl_ModelAlloc( p->pMan->pDesign, Vec_PtrEntry(vTokens, 1) );
@@ -866,7 +893,7 @@ static int Ioa_ReadParseLineDelay( Ioa_ReadMod_t * p, char * pLine )
 {
     Vec_Ptr_t * vTokens = p->pMan->vTokens;
     int RetValue1, RetValue2, Number1, Number2, Temp;
-    char * pToken;
+    char * pToken, * pTokenNum;
     float Delay;
     assert( sizeof(float) == sizeof(int) );
     Ioa_ReadSplitIntoTokens( vTokens, pLine, '\0' );
@@ -878,8 +905,9 @@ static int Ioa_ReadParseLineDelay( Ioa_ReadMod_t * p, char * pLine )
         return 0;
     }
     // find the delay number
-    Delay = atof( Vec_PtrEntryLast(vTokens) );
-    if ( Delay < 0.0 )
+    pTokenNum = Vec_PtrEntryLast(vTokens);
+    Delay = atof( pTokenNum );
+    if ( Delay == 0.0 && pTokenNum[0] != '0' )
     {
         sprintf( p->pMan->sError, "Line %d: Delay value (%s) appears to be invalid.", Ioa_ReadGetLine(p->pMan, pToken), Vec_PtrEntryLast(vTokens) );
         return 0;
@@ -927,6 +955,80 @@ static int Ioa_ReadParseLineDelay( Ioa_ReadMod_t * p, char * pLine )
     return 1;
 }
 
+/**Function*************************************************************
+
+  Synopsis    [Parses the subckt line.]
+
+  Description []
+  
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+static int Ioa_ReadParseLineTimes( Ioa_ReadMod_t * p, char * pLine, int fOutput )
+{
+    Vec_Ptr_t * vTokens = p->pMan->vTokens;
+    int RetValue, Number;
+    char * pToken, * pTokenNum;
+    float Delay;
+    assert( sizeof(float) == sizeof(int) );
+    Ioa_ReadSplitIntoTokens( vTokens, pLine, '\0' );
+    pToken = Vec_PtrEntry(vTokens,0);
+    if ( fOutput )
+        assert( !strcmp(pToken, "output_required") );
+    else
+        assert( !strcmp(pToken, "input_arrival") );
+    if ( Vec_PtrSize(vTokens) != 3 )
+    {
+        sprintf( p->pMan->sError, "Line %d: Delay line does not have a valid number of parameters (3).", Ioa_ReadGetLine(p->pMan, pToken) );
+        return 0;
+    }
+    // find the delay number
+    pTokenNum = Vec_PtrEntryLast(vTokens);
+    if ( !strcmp( pTokenNum, "-inf" ) )
+        Delay = -AIG_INFINITY;
+    else if ( !strcmp( pTokenNum, "inf" ) ) 
+        Delay = AIG_INFINITY;
+    else
+        Delay = atof( pTokenNum );
+    if ( Delay == 0.0 && pTokenNum[0] != '0' )
+    {
+        sprintf( p->pMan->sError, "Line %d: Delay value (%s) appears to be invalid.", Ioa_ReadGetLine(p->pMan, pToken), Vec_PtrEntryLast(vTokens) );
+        return 0;
+    }
+    // find the PI/PO numbers
+    if ( fOutput )
+    {
+        RetValue = Ntl_ModelFindPioNumber( p->pNtk, Vec_PtrEntry(vTokens, 1), &Number );
+        if ( RetValue == 0 )
+        {
+            sprintf( p->pMan->sError, "Line %d: Cannot find signal \"%s\" among POs.", Ioa_ReadGetLine(p->pMan, pToken), Vec_PtrEntry(vTokens, 1) );
+            return 0;
+        }
+        // store the values
+        if ( p->pNtk->vRequireds == NULL )
+            p->pNtk->vRequireds = Vec_IntAlloc( 100 );
+        Vec_IntPush( p->pNtk->vRequireds, Number );
+        Vec_IntPush( p->pNtk->vRequireds, Aig_Float2Int(Delay) );        
+    }
+    else
+    {
+        RetValue = Ntl_ModelFindPioNumber( p->pNtk, Vec_PtrEntry(vTokens, 1), &Number );
+        if ( RetValue == 0 )
+        {
+            sprintf( p->pMan->sError, "Line %d: Cannot find signal \"%s\" among PIs.", Ioa_ReadGetLine(p->pMan, pToken), Vec_PtrEntry(vTokens, 1) );
+            return 0;
+        }
+        // store the values
+        if ( p->pNtk->vArrivals == NULL )
+            p->pNtk->vArrivals = Vec_IntAlloc( 100 );
+        Vec_IntPush( p->pNtk->vArrivals, Number );
+        Vec_IntPush( p->pNtk->vArrivals, Aig_Float2Int(Delay) );        
+    }
+    return 1;
+}
+
 
 /**Function*************************************************************
 
diff --git a/src/aig/ntl/ntlTime.c b/src/aig/ntl/ntlTime.c
new file mode 100644
index 00000000..d4bd1375
--- /dev/null
+++ b/src/aig/ntl/ntlTime.c
@@ -0,0 +1,134 @@
+/**CFile****************************************************************
+
+  FileName    [ntlTime.c]
+
+  SystemName  [ABC: Logic synthesis and verification system.]
+
+  PackageName [Netlist representation.]
+
+  Synopsis    [Creates timing manager.]
+
+  Author      [Alan Mishchenko]
+  
+  Affiliation [UC Berkeley]
+
+  Date        [Ver. 1.0. Started - June 20, 2005.]
+
+  Revision    [$Id: ntlTime.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
+
+***********************************************************************/
+
+#include "ntl.h"
+
+////////////////////////////////////////////////////////////////////////
+///                        DECLARATIONS                              ///
+////////////////////////////////////////////////////////////////////////
+
+////////////////////////////////////////////////////////////////////////
+///                     FUNCTION DEFINITIONS                         ///
+////////////////////////////////////////////////////////////////////////
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+float * Ntl_ManCreateDelayTable( Vec_Int_t * vDelays, int nIns, int nOuts )
+{
+    float * pDelayTable, Delay;
+    int iIn, iOut, i, k;
+    assert( Vec_IntSize(vDelays) % 3 == 0 );
+    pDelayTable = ALLOC( float, nIns * nOuts );
+    memset( pDelayTable, 0, sizeof(float) * nIns * nOuts );
+    Vec_IntForEachEntry( vDelays, iIn, i )
+    {
+        iOut = Vec_IntEntry(vDelays, ++i);
+        Delay = Aig_Int2Float( Vec_IntEntry(vDelays, ++i) );
+        if ( iIn == -1 && iOut == -1 )
+            for ( k = 0; k < nIns * nOuts; k++ )
+                pDelayTable[k] = Delay;
+        else if ( iIn == -1 )
+            for ( k = 0; k < nIns; k++ )
+                pDelayTable[iOut * nIns + k] = Delay;
+        else if ( iOut == -1 )
+            for ( k = 0; k < nOuts; k++ )
+                pDelayTable[k * nIns + iIn] = Delay;
+        else 
+            pDelayTable[iOut * nIns + iIn] = Delay;
+    }
+    return pDelayTable;
+}
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Aig_TMan_t * Ntl_ManCreateTiming( Ntl_Man_t * p )
+{
+    Aig_TMan_t * pMan;
+    Vec_Ptr_t * vDelayTables;
+    Ntl_Mod_t * pRoot, * pModel;
+    Ntl_Obj_t * pObj;
+    int i, curPi, curPo, Entry;
+    assert( p->pAig != NULL );
+    // start the timing manager
+    pMan = Aig_TManStart( Aig_ManPiNum(p->pAig), Aig_ManPoNum(p->pAig) );
+    // add arrival time info for the true PIs
+    pRoot = Vec_PtrEntry( p->vModels, 0 );
+    Ntl_ModelForEachPi( pRoot, pObj, i )
+        Aig_TManInitPiArrival( pMan, i, 0.0 );
+    // unpack the data in the arrival times
+    if ( pRoot->vArrivals )
+        Vec_IntForEachEntry( pRoot->vArrivals, Entry, i )
+            Aig_TManInitPiArrival( pMan, Entry, Vec_IntEntry(pRoot->vArrivals,++i) );
+    // add the required time into for the true POs
+    pRoot = Vec_PtrEntry( p->vModels, 0 );
+    Ntl_ModelForEachPo( pRoot, pObj, i )
+        Aig_TManInitPoRequired( pMan, i, AIG_INFINITY );
+    // unpack the data in the required times
+    if ( pRoot->vRequireds )
+        Vec_IntForEachEntry( pRoot->vRequireds, Entry, i )
+            Aig_TManInitPoRequired( pMan, Entry, Vec_IntEntry(pRoot->vRequireds,++i) );
+    // derive timing tables
+    vDelayTables = Vec_PtrAlloc( Vec_PtrSize(p->vModels) );
+    Ntl_ManForEachModel( p, pModel, i )
+    {
+        if ( pModel->vDelays )
+            pModel->pDelayTable = Ntl_ManCreateDelayTable( pModel->vDelays, Ntl_ModelPiNum(pModel), Ntl_ModelPoNum(pModel) );
+        Vec_PtrPush( vDelayTables, pModel->pDelayTable );
+    }
+    Aig_TManSetDelayTables( pMan, vDelayTables );
+    // set up the boxes
+    curPi = Ntl_ModelPiNum(pRoot);
+    curPo = Ntl_ModelPoNum(pRoot);
+    Ntl_ManForEachBox( p, pObj, i )
+    {
+        Aig_TManCreateBoxFirst( pMan, curPo, Ntl_ObjFanoutNum(pObj), curPi, Ntl_ObjFaninNum(pObj), pObj->pImplem->pDelayTable );
+        curPo += Ntl_ObjFanoutNum(pObj);
+        curPi += Ntl_ObjFaninNum(pObj);
+    }
+    // forget refs to the delay tables in the network
+    Ntl_ManForEachModel( p, pModel, i )
+        pModel->pDelayTable = NULL;
+    return pMan;
+}
+
+
+////////////////////////////////////////////////////////////////////////
+///                       END OF FILE                                ///
+////////////////////////////////////////////////////////////////////////
+
+
diff --git a/src/base/abc/abcLib.c b/src/base/abc/abcLib.c
index f5b90e90..feff1478 100644
--- a/src/base/abc/abcLib.c
+++ b/src/base/abc/abcLib.c
@@ -78,10 +78,9 @@ void Abc_LibFree( Abc_Lib_t * pLib, Abc_Ntk_t * pNtkSave )
     {
         Vec_PtrForEachEntry( pLib->vModules, pNtk, i )
         {
-//            pNtk->pManFunc = NULL;
             if ( pNtk == pNtkSave )
                 continue;
-            pNtk->pManFunc = NULL;
+//            pNtk->pManFunc = NULL;
             pNtk->pDesign = NULL;
             Abc_NtkDelete( pNtk );
         }
diff --git a/src/base/abc/abcMinBase.c b/src/base/abc/abcMinBase.c
index 13f422f4..e1c0f4fd 100644
--- a/src/base/abc/abcMinBase.c
+++ b/src/base/abc/abcMinBase.c
@@ -249,6 +249,256 @@ int Abc_NodeSupport( DdNode * bFunc, Vec_Str_t * vSupport, int nVars )
     return Counter;
 }
 
+
+
+/**Function*************************************************************
+
+  Synopsis    [Find the number of unique variables after collapsing.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Abc_NodeCheckDupFanin( Abc_Obj_t * pFanin, Abc_Obj_t * pFanout, int * piFanin )
+{
+    Abc_Obj_t * pObj;
+    int i, Counter = 0;
+    Abc_ObjForEachFanin( pFanout, pObj, i )
+        if ( pObj == pFanin )
+        {
+            if ( piFanin )
+                *piFanin = i;
+            Counter++;
+        }
+    return Counter;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Find the number of unique variables after collapsing.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Abc_NodeCollapseSuppSize( Abc_Obj_t * pFanin, Abc_Obj_t * pFanout, Vec_Ptr_t * vFanins )
+{
+    Abc_Obj_t * pObj;
+    int i;
+    Vec_PtrClear( vFanins );
+    Abc_ObjForEachFanin( pFanout, pObj, i )
+        if ( pObj != pFanin )
+            Vec_PtrPushUnique( vFanins, pObj );
+    Abc_ObjForEachFanin( pFanin, pObj, i )
+        Vec_PtrPushUnique( vFanins, pObj );
+    return Vec_PtrSize( vFanins );
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Returns the index of the new fanin.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Abc_ObjFaninNumberNew( Vec_Ptr_t * vFanins, Abc_Obj_t * pFanin )
+{
+    Abc_Obj_t * pObj;
+    int i;
+    Vec_PtrForEachEntry( vFanins, pObj, i )
+        if ( pObj == pFanin )
+            return i;
+    return -1;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Find the permutation map for the given node into the new order.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Abc_NodeCollapsePermMap( Abc_Obj_t * pNode, Abc_Obj_t * pSkip, Vec_Ptr_t * vFanins, int * pPerm )
+{
+    Abc_Obj_t * pFanin;
+    int i;
+    for ( i = 0; i < Vec_PtrSize(vFanins); i++ )
+        pPerm[i] = i;
+    Abc_ObjForEachFanin( pNode, pFanin, i )
+    {
+        if ( pFanin == pSkip )
+            continue;
+        pPerm[i] = Abc_ObjFaninNumberNew( vFanins, pFanin );
+        if ( pPerm[i] == -1 )
+            return 0;
+    }
+    return 1;
+}
+
+
+/**Function*************************************************************
+
+  Synopsis    [Computes support of the node.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+DdNode * Abc_NodeCollapseFunc( Abc_Obj_t * pFanin, Abc_Obj_t * pFanout, Vec_Ptr_t * vFanins, int * pPermFanin, int * pPermFanout )
+{
+    DdManager * dd = pFanin->pNtk->pManFunc;
+    DdNode * bVar, * bFunc0, * bFunc1, * bTemp, * bFanin, * bFanout;
+    int RetValue, nSize, iFanin;
+    // can only eliminate if fanin occurs in the fanin list of the fanout exactly once
+    if ( Abc_NodeCheckDupFanin( pFanin, pFanout, &iFanin ) != 1 )
+        return NULL;
+    // find the new number of fanins after collapsing
+    nSize = Abc_NodeCollapseSuppSize( pFanin, pFanout, vFanins );
+    bVar = Cudd_bddIthVar( dd, nSize - 1 );
+    assert( nSize <= dd->size );
+    // find the permutation after collapsing
+    RetValue = Abc_NodeCollapsePermMap( pFanin, NULL, vFanins, pPermFanin );
+    assert( RetValue );
+    RetValue = Abc_NodeCollapsePermMap( pFanout, pFanin, vFanins, pPermFanout );
+    assert( RetValue );
+    // cofactor the local function of the node
+    bVar   = Cudd_bddIthVar( dd, iFanin );
+    bFunc0 = Cudd_Cofactor( dd, pFanout->pData, Cudd_Not(bVar) ); Cudd_Ref( bFunc0 );
+    bFunc1 = Cudd_Cofactor( dd, pFanout->pData, bVar );           Cudd_Ref( bFunc1 );
+    // find the permutation after collapsing
+    bFunc0 = Cudd_bddPermute( dd, bTemp = bFunc0, pPermFanout );  Cudd_Ref( bFunc0 );
+    Cudd_RecursiveDeref( dd, bTemp ); 
+    bFunc1 = Cudd_bddPermute( dd, bTemp = bFunc1, pPermFanout );  Cudd_Ref( bFunc1 );
+    Cudd_RecursiveDeref( dd, bTemp );
+    bFanin = Cudd_bddPermute( dd, pFanin->pData, pPermFanin );    Cudd_Ref( bFanin );
+    // create the new function
+    bFanout = Cudd_bddIte( dd, bFanin, bFunc1, bFunc0 );          Cudd_Ref( bFanout );
+    Cudd_RecursiveDeref( dd, bFanin );
+    Cudd_RecursiveDeref( dd, bFunc1 );
+    Cudd_RecursiveDeref( dd, bFunc0 );
+    Cudd_Deref( bFanout );
+    return bFanout;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Collapses one node into its fanout.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Abc_NodeCollapse( Abc_Obj_t * pFanin, Abc_Obj_t * pFanout, Vec_Ptr_t * vFanins, int * pPermFanin, int * pPermFanout )
+{
+    Abc_Obj_t * pFanoutNew, * pObj;
+    DdNode * bFanoutNew;
+    int i;
+    assert( Abc_NtkIsBddLogic(pFanin->pNtk) );
+    assert( Abc_ObjIsNode(pFanin) );
+    assert( Abc_ObjIsNode(pFanout) );
+    bFanoutNew = Abc_NodeCollapseFunc( pFanin, pFanout, vFanins, pPermFanin, pPermFanout );  
+    if ( bFanoutNew == NULL )
+        return 0;
+    Cudd_Ref( bFanoutNew );
+    // create the new node
+    pFanoutNew = Abc_NtkCreateNode( pFanin->pNtk );
+    Vec_PtrForEachEntry( vFanins, pObj, i )
+        Abc_ObjAddFanin( pFanoutNew, pObj );
+    pFanoutNew->pData = bFanoutNew;
+    // minimize the node
+    Abc_NodeMinimumBase( pFanoutNew );
+    // transfer the fanout
+    Abc_ObjTransferFanout( pFanout, pFanoutNew );
+    assert( Abc_ObjFanoutNum( pFanout ) == 0 );
+    Abc_NtkDeleteObj_rec( pFanout, 1 );
+    return 1;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Eliminates the nodes into their fanouts if the node size does not exceed this number.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Abc_NtkEliminate( Abc_Ntk_t * pNtk, int nMaxSize, int fReverse, int fVerbose )
+{
+    extern void Abc_NtkBddReorder( Abc_Ntk_t * pNtk, int fVerbose );
+    Vec_Ptr_t * vFanouts, * vFanins, * vNodes;
+    Abc_Obj_t * pNode, * pFanout;
+    int * pPermFanin, * pPermFanout;
+    int RetValue, i, k;
+    assert( nMaxSize > 0 );
+    assert( Abc_NtkIsLogic(pNtk) ); 
+    // convert network to BDD representation
+    if ( !Abc_NtkToBdd(pNtk) )
+    {
+        fprintf( stdout, "Converting to BDD has failed.\n" );
+        return 0;
+    }
+    // prepare nodes for sweeping
+    Abc_NtkRemoveDupFanins( pNtk );
+    Abc_NtkMinimumBase( pNtk );
+    Abc_NtkCleanup( pNtk, 0 );
+    // get the nodes in the given order
+    vNodes = fReverse? Abc_NtkDfsReverse( pNtk ) : Abc_NtkDfs( pNtk, 0 );
+    // go through the nodes and decide is they can be eliminated
+    pPermFanin = ALLOC( int, nMaxSize + 100 );
+    pPermFanout = ALLOC( int, nMaxSize + 100 );
+    vFanins = Vec_PtrAlloc( 100 );
+    vFanouts = Vec_PtrAlloc( 100 );
+    Vec_PtrForEachEntry( vNodes, pNode, i )
+    {
+        if ( Abc_NodeFindCoFanout(pNode) != NULL )
+            continue;
+        if ( Abc_ObjFaninNum(pNode) > nMaxSize )
+            continue;
+        Abc_ObjForEachFanout( pNode, pFanout, k )
+            if ( Abc_NodeCollapseSuppSize(pNode, pFanout, vFanins) > nMaxSize )
+                break;
+        if ( k < Abc_ObjFanoutNum(pNode) )
+            continue;
+        // perform elimination
+        Abc_NodeCollectFanouts( pNode, vFanouts );
+        Vec_PtrForEachEntry( vFanouts, pFanout, k )
+        {
+            RetValue = Abc_NodeCollapse( pNode, pFanout, vFanins, pPermFanin, pPermFanout );
+            assert( RetValue );
+        }
+    }
+    Abc_NtkBddReorder( pNtk, 0 );
+    Vec_PtrFree( vFanins );
+    Vec_PtrFree( vFanouts );
+    Vec_PtrFree( vNodes );
+    free( pPermFanin );
+    free( pPermFanout );
+    return 1;
+}
+
 ////////////////////////////////////////////////////////////////////////
 ///                       END OF FILE                                ///
 ////////////////////////////////////////////////////////////////////////
diff --git a/src/base/abci/abc.c b/src/base/abci/abc.c
index f4ad2eaf..da07a936 100644
--- a/src/base/abci/abc.c
+++ b/src/base/abci/abc.c
@@ -64,6 +64,7 @@ static int Abc_CommandRenode         ( Abc_Frame_t * pAbc, int argc, char ** arg
 static int Abc_CommandCleanup        ( Abc_Frame_t * pAbc, int argc, char ** argv );
 static int Abc_CommandSweep          ( Abc_Frame_t * pAbc, int argc, char ** argv );
 static int Abc_CommandFastExtract    ( Abc_Frame_t * pAbc, int argc, char ** argv );
+static int Abc_CommandEliminate      ( Abc_Frame_t * pAbc, int argc, char ** argv );
 static int Abc_CommandDisjoint       ( Abc_Frame_t * pAbc, int argc, char ** argv );
 static int Abc_CommandImfs           ( Abc_Frame_t * pAbc, int argc, char ** argv );
 static int Abc_CommandLutpack        ( Abc_Frame_t * pAbc, int argc, char ** argv );
@@ -239,6 +240,7 @@ void Abc_Init( Abc_Frame_t * pAbc )
     Cmd_CommandAdd( pAbc, "Synthesis",    "cleanup",       Abc_CommandCleanup,          1 );
     Cmd_CommandAdd( pAbc, "Synthesis",    "sweep",         Abc_CommandSweep,            1 );
     Cmd_CommandAdd( pAbc, "Synthesis",    "fx",            Abc_CommandFastExtract,      1 );
+    Cmd_CommandAdd( pAbc, "Synthesis",    "eliminate",     Abc_CommandEliminate,        1 );
     Cmd_CommandAdd( pAbc, "Synthesis",    "dsd",           Abc_CommandDisjoint,         1 );
     Cmd_CommandAdd( pAbc, "Synthesis",    "imfs",          Abc_CommandImfs,             1 );
     Cmd_CommandAdd( pAbc, "Synthesis",    "lutpack",       Abc_CommandLutpack,          1 );
@@ -2727,6 +2729,97 @@ usage:
   SeeAlso     []
 
 ***********************************************************************/
+int Abc_CommandEliminate( Abc_Frame_t * pAbc, int argc, char ** argv )
+{
+    Abc_Ntk_t * pNtk;
+    FILE * pOut, * pErr;
+    int nMaxSize;
+    int fReverse;
+    int fVerbose;
+    int c;
+    extern int Abc_NtkEliminate( Abc_Ntk_t * pNtk, int nMaxSize, int fReverse, int fVerbose );
+
+    pNtk = Abc_FrameReadNtk(pAbc);
+    pOut = Abc_FrameReadOut(pAbc);
+    pErr = Abc_FrameReadErr(pAbc);
+
+    // set the defaults
+    nMaxSize  = 8;
+    fReverse  = 0;
+    fVerbose  = 0;
+    Extra_UtilGetoptReset();
+    while ( (c = Extra_UtilGetopt(argc, argv, "Nrvh")) != EOF ) 
+    {
+        switch (c) 
+        {
+            case 'N':
+                if ( globalUtilOptind >= argc )
+                {
+                    fprintf( pErr, "Command line switch \"-N\" should be followed by a positive integer.\n" );
+                    goto usage;
+                }
+                nMaxSize = atoi(argv[globalUtilOptind]);
+                globalUtilOptind++;
+                if ( nMaxSize <= 0 ) 
+                    goto usage;
+                break;
+            case 'r':
+                fReverse ^= 1;
+                break;
+            case 'v':
+                fVerbose ^= 1;
+                break;
+            case 'h':
+                goto usage;
+                break;
+            default:
+                goto usage;
+        }
+    } 
+
+    if ( pNtk == NULL )
+    {
+        fprintf( pErr, "Empty network.\n" );
+        return 1;
+    }
+
+    if ( Abc_NtkNodeNum(pNtk) == 0 )
+    {
+        fprintf( pErr, "The network does not have internal nodes.\n" );
+        return 1;
+    }
+
+    if ( !Abc_NtkIsLogic(pNtk) )
+    {
+        fprintf( pErr, "This command can only be applied to a logic network (run \"renode\" or \"if\").\n" );
+        return 1;
+    }
+
+    // the nodes to be merged are linked into the special linked list
+    Abc_NtkEliminate( pNtk, nMaxSize, fReverse, fVerbose );
+    return 0;
+
+usage:
+    fprintf( pErr, "usage: eliminate [-N num] [-rvh]\n");
+    fprintf( pErr, "\t         greedily eliminates nodes by collapsing them into fanouts\n");
+    fprintf( pErr, "\t-N num : the maximum support size after collapsing [default = %d]\n", nMaxSize );  
+    fprintf( pErr, "\t-r     : use the reverse topological order [default = %s]\n", fReverse? "yes": "no" );  
+    fprintf( pErr, "\t-v     : print verbose information [default = %s]\n", fVerbose? "yes": "no" ); 
+    fprintf( pErr, "\t-h     : print the command usage\n");
+    return 1;       
+}
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
 int Abc_CommandDisjoint( Abc_Frame_t * pAbc, int argc, char ** argv )
 {
     FILE * pOut, * pErr;
@@ -2958,6 +3051,7 @@ int Abc_CommandImfs( Abc_Frame_t * pAbc, int argc, char ** argv )
 usage:
     fprintf( pErr, "usage: imfs [-W <NM>] [-L <num>] [-C <num>] [-S <num>] [-avwh]\n" );
     fprintf( pErr, "\t           performs resubstitution-based resynthesis with interpolation\n" );
+    fprintf( pErr, "\t           (there is another command for resynthesis after LUT mapping, \"lutpack\")\n" );
     fprintf( pErr, "\t-W <NM>  : fanin/fanout levels (NxM) of the window (00 <= NM <= 99) [default = %d%d]\n", pPars->nWindow/10, pPars->nWindow%10 );
     fprintf( pErr, "\t-C <num> : the max number of resub candidates (1 <= n) [default = %d]\n", pPars->nCands );
     fprintf( pErr, "\t-S <num> : the number of simulation words (1 <= n <= 256) [default = %d]\n", pPars->nSimWords );
@@ -3106,6 +3200,7 @@ usage:
     fprintf( pErr, "\t           performs \"rewriting\" for LUT networks;\n" );
     fprintf( pErr, "\t           determines LUT size as the max fanin count of a node;\n" );
     fprintf( pErr, "\t           if the network is not LUT-mapped, packs it into 6-LUTs\n" );
+    fprintf( pErr, "\t           (there is another command for resynthesis after LUT mapping, \"imfs\")\n" );
     fprintf( pErr, "\t-N <num> : the max number of LUTs in the structure (2 <= num) [default = %d]\n", pPars->nLutsMax );
     fprintf( pErr, "\t-Q <num> : the max number of LUTs not in MFFC (0 <= num) [default = %d]\n", pPars->nLutsOver );
     fprintf( pErr, "\t-S <num> : the max number of LUT inputs shared (0 <= num <= 3) [default = %d]\n", pPars->nVarsShared );
@@ -6213,7 +6308,7 @@ int Abc_CommandTest( Abc_Frame_t * pAbc, int argc, char ** argv )
     extern Abc_Ntk_t * Abc_NtkDar( Abc_Ntk_t * pNtk );
     extern Abc_Ntk_t * Abc_NtkDarToCnf( Abc_Ntk_t * pNtk, char * pFileName );
     extern Abc_Ntk_t * Abc_NtkFilter( Abc_Ntk_t * pNtk );
-    extern Abc_Ntk_t * Abc_NtkDarRetime( Abc_Ntk_t * pNtk, int nStepsMax, int fVerbose );
+//    extern Abc_Ntk_t * Abc_NtkDarRetime( Abc_Ntk_t * pNtk, int nStepsMax, int fVerbose );
     extern Abc_Ntk_t * Abc_NtkPcmTest( Abc_Ntk_t * pNtk, int fVerbose );
     extern Abc_NtkDarHaigRecord( Abc_Ntk_t * pNtk );
     extern void Abc_NtkDarTestBlif( char * pFileName );
@@ -6222,8 +6317,8 @@ int Abc_CommandTest( Abc_Frame_t * pAbc, int argc, char ** argv )
     pOut = Abc_FrameReadOut(pAbc);
     pErr = Abc_FrameReadErr(pAbc);
 
-    printf( "This command is temporarily disabled.\n" );
-    return 0;
+//    printf( "This command is temporarily disabled.\n" );
+//    return 0;
 
     // set defaults
     fVeryVerbose = 0;
@@ -8399,6 +8494,7 @@ usage:
     sprintf( Buffer, "%d", pParams->nBTLimit );
     fprintf( pErr, "usage: fraig [-R num] [-D num] [-C num] [-rscpvtah]\n" );
     fprintf( pErr, "\t         transforms a logic network into a functionally reduced AIG\n" );
+    fprintf( pErr, "\t         (there are also newer fraiging commands, \"ifraig\" and \"dfraig\")\n" );
     fprintf( pErr, "\t-R num : number of random patterns (127 < num < 32769) [default = %d]\n",     pParams->nPatsRand );
     fprintf( pErr, "\t-D num : number of systematic patterns (127 < num < 32769) [default = %d]\n", pParams->nPatsDyna );
     fprintf( pErr, "\t-C num : number of backtracks for one SAT problem [default = %s]\n",    pParams->nBTLimit==-1? "infinity" : Buffer );
@@ -10891,6 +10987,7 @@ int Abc_CommandDRetime( Abc_Frame_t * pAbc, int argc, char ** argv )
     int fFastAlgo;
     int fVerbose;
     int c;
+    extern Abc_Ntk_t * Abc_NtkDarRetime( Abc_Ntk_t * pNtk, int nStepsMax, int fVerbose );
     extern Abc_Ntk_t * Abc_NtkDarRetimeF( Abc_Ntk_t * pNtk, int nStepsMax, int fVerbose );
 
     pNtk = Abc_FrameReadNtk(pAbc);
@@ -12290,6 +12387,7 @@ int Abc_CommandSec( Abc_Frame_t * pAbc, int argc, char ** argv )
 usage:
     fprintf( pErr, "usage: sec [-F num] [-T num] [-C num] [-I num] [-srvh] <file1> <file2>\n" );
     fprintf( pErr, "\t         performs bounded sequential equivalence checking\n" );
+    fprintf( pErr, "\t         (there is also an unbounded SEC commands, \"dsec\" and \"dprove\")\n" );
     fprintf( pErr, "\t-s     : toggle \"SAT only\" and \"FRAIG + SAT\" [default = %s]\n", fSat? "SAT only": "FRAIG + SAT" );
     fprintf( pErr, "\t-r     : toggles retiming verification [default = %s]\n", fVerbose? "yes": "no" );
     fprintf( pErr, "\t-v     : toggles verbose output [default = %s]\n", fVerbose? "yes": "no" );
@@ -12616,6 +12714,7 @@ usage:
     fprintf( pErr, "usage: sat [-C num] [-I num] [-vh]\n" );
     fprintf( pErr, "\t         solves the combinational miter using SAT solver MiniSat-1.14\n" );
     fprintf( pErr, "\t         derives CNF from the current network and leave it unchanged\n" );
+    fprintf( pErr, "\t         (there is also a newer SAT solving command \"dsat\")\n" );
     fprintf( pErr, "\t-C num : limit on the number of conflicts [default = %d]\n",    nConfLimit );
     fprintf( pErr, "\t-I num : limit on the number of inspections [default = %d]\n", nInsLimit );
     fprintf( pErr, "\t-v     : prints verbose information [default = %s]\n", fVerbose? "yes": "no" );  
@@ -12912,6 +13011,7 @@ usage:
     fprintf( pErr, "usage: prove [-N num] [-C num] [-F num] [-L num] [-I num] [-rfbvh]\n" );
     fprintf( pErr, "\t         solves combinational miter by rewriting, FRAIGing, and SAT\n" );
     fprintf( pErr, "\t         replaces the current network by the cone modified by rewriting\n" );
+    fprintf( pErr, "\t         (there are also newer CEC commands, \"iprove\" and \"dprove\")\n" );
     fprintf( pErr, "\t-N num : max number of iterations [default = %d]\n", pParams->nItersMax );
     fprintf( pErr, "\t-C num : max starting number of conflicts in mitering [default = %d]\n", pParams->nMiteringLimitStart );
     fprintf( pErr, "\t-F num : max starting number of conflicts in fraiging [default = %d]\n", pParams->nFraigingLimitStart );
diff --git a/src/base/abci/abcClpBdd.c b/src/base/abci/abcClpBdd.c
index 341ff5b0..a6b3a770 100644
--- a/src/base/abci/abcClpBdd.c
+++ b/src/base/abci/abcClpBdd.c
@@ -19,6 +19,7 @@
 ***********************************************************************/
 
 #include "abc.h"
+//#include "reo.h"
 
 ////////////////////////////////////////////////////////////////////////
 ///                        DECLARATIONS                              ///
@@ -87,6 +88,9 @@ Abc_Ntk_t * Abc_NtkCollapse( Abc_Ntk_t * pNtk, int fBddSizeMax, int fDualRail, i
     return pNtkNew;
 }
 
+
+//int runtime1, runtime2;
+
 /**Function*************************************************************
 
   Synopsis    [Derives the network with the given global BDD.]
@@ -100,12 +104,19 @@ Abc_Ntk_t * Abc_NtkCollapse( Abc_Ntk_t * pNtk, int fBddSizeMax, int fDualRail, i
 ***********************************************************************/
 Abc_Ntk_t * Abc_NtkFromGlobalBdds( Abc_Ntk_t * pNtk )
 {
+//    extern void Extra_ShuffleTest( reo_man * p, DdManager * dd, DdNode * Func );
+//    reo_man * pReo;
+
     ProgressBar * pProgress;
     Abc_Ntk_t * pNtkNew;
     Abc_Obj_t * pNode, * pDriver, * pNodeNew;
 //    DdManager * dd = pNtk->pManGlob;
     DdManager * dd = Abc_NtkGlobalBddMan( pNtk );
     int i;
+
+//    pReo = Extra_ReorderInit( Abc_NtkCiNum(pNtk), 1000 );
+//    runtime1 = runtime2 = 0;
+
     // start the new network
     pNtkNew = Abc_NtkStartFrom( pNtk, ABC_NTK_LOGIC, ABC_FUNC_BDD );
     // make sure the new manager has the same number of inputs
@@ -124,8 +135,16 @@ Abc_Ntk_t * Abc_NtkFromGlobalBdds( Abc_Ntk_t * pNtk )
 //        pNodeNew = Abc_NodeFromGlobalBdds( pNtkNew, dd, Vec_PtrEntry(pNtk->vFuncsGlob, i) );
         pNodeNew = Abc_NodeFromGlobalBdds( pNtkNew, dd, Abc_ObjGlobalBdd(pNode) );
         Abc_ObjAddFanin( pNode->pCopy, pNodeNew );
+
+//        Extra_ShuffleTest( pReo, dd, Abc_ObjGlobalBdd(pNode) );
+
     }
     Extra_ProgressBarStop( pProgress );
+
+//    Extra_ReorderQuit( pReo );
+//PRT( "Reo ", runtime1 );
+//PRT( "Cudd", runtime2 );
+
     return pNtkNew;
 }
 
diff --git a/src/base/abci/abcDar.c b/src/base/abci/abcDar.c
index 3729fef8..29b1ea14 100644
--- a/src/base/abci/abcDar.c
+++ b/src/base/abci/abcDar.c
@@ -1506,12 +1506,16 @@ void Abc_NtkDarTestBlif( char * pFileName )
         printf( "Abc_NtkDarTestBlif(): Reading BLIF has failed.\n" );
         return;
     }
+    Ntl_ManPrintStats( p );
+/*
     if ( !Ntl_ManInsertTest( p ) )
     {
         printf( "Abc_NtkDarTestBlif(): Tranformation of the netlist has failed.\n" );
         return;
     }
-    sprintf( Buffer, "%s_.blif", p->pName );
+*/
+//    sprintf( Buffer, "%s_.blif", p->pName );
+    sprintf( Buffer, "test_.blif", p->pName );
     Ioa_WriteBlif( p, Buffer );
     Ntl_ManFree( p );
 }
diff --git a/src/base/abci/abcReorder.c b/src/base/abci/abcReorder.c
index d6dee49b..182780cd 100644
--- a/src/base/abci/abcReorder.c
+++ b/src/base/abci/abcReorder.c
@@ -77,6 +77,8 @@ void Abc_NtkBddReorder( Abc_Ntk_t * pNtk, int fVerbose )
     reo_man * p;
     Abc_Obj_t * pNode;
     int i;
+    Abc_NtkRemoveDupFanins( pNtk );
+    Abc_NtkMinimumBase( pNtk );
     p = Extra_ReorderInit( Abc_NtkGetFaninMax(pNtk), 100 );
     Abc_NtkForEachNode( pNtk, pNode, i )
     {
diff --git a/src/base/abci/abcXsim.c b/src/base/abci/abcXsim.c
index 5d9e4634..e5656170 100644
--- a/src/base/abci/abcXsim.c
+++ b/src/base/abci/abcXsim.c
@@ -190,28 +190,25 @@ void Abc_NtkXValueSimulate( Abc_Ntk_t * pNtk, int nFrames, int fXInputs, int fXS
 
 ***********************************************************************/
 void Abc_NtkCycleInitState( Abc_Ntk_t * pNtk, int nFrames, int fVerbose )
-{
+{ 
     Abc_Obj_t * pObj;
     int i, f;
     assert( Abc_NtkIsStrash(pNtk) );
     srand( 0x12341234 );
     // initialize the values
     Abc_ObjSetXsim( Abc_AigConst1(pNtk), XVS1 );
-    Abc_NtkForEachPi( pNtk, pObj, i )
-        Abc_ObjSetXsim( pObj, Abc_XsimRand2() );
     Abc_NtkForEachLatch( pNtk, pObj, i )
-        Abc_ObjSetXsim( Abc_ObjFanout0(pObj), Abc_LatchIsInit1(pObj)? XVS1 : XVS0 );
+//        Abc_ObjSetXsim( Abc_ObjFanout0(pObj), Abc_LatchIsInit1(pObj)? XVS1 : XVS0 );
+        Abc_ObjSetXsim( Abc_ObjFanout0(pObj), Abc_LatchInit(pObj) );
     // simulate for the given number of timeframes
     for ( f = 0; f < nFrames; f++ )
     {
+        Abc_NtkForEachPi( pNtk, pObj, i )
+            Abc_ObjSetXsim( pObj, Abc_XsimRand2() );
         Abc_AigForEachAnd( pNtk, pObj, i )
             Abc_ObjSetXsim( pObj, Abc_XsimAnd(Abc_ObjGetXsimFanin0(pObj), Abc_ObjGetXsimFanin1(pObj)) );
         Abc_NtkForEachCo( pNtk, pObj, i )
             Abc_ObjSetXsim( pObj, Abc_ObjGetXsimFanin0(pObj) );
-        // assign input values
-        Abc_NtkForEachPi( pNtk, pObj, i )
-            Abc_ObjSetXsim( pObj, Abc_XsimRand2() );
-        // transfer the latch values
         Abc_NtkForEachLatch( pNtk, pObj, i )
             Abc_ObjSetXsim( Abc_ObjFanout0(pObj), Abc_ObjGetXsim(Abc_ObjFanin0(pObj)) );
     }
diff --git a/src/base/io/ioReadBlifMv.c b/src/base/io/ioReadBlifMv.c
index 18578cbb..97f2fbf3 100644
--- a/src/base/io/ioReadBlifMv.c
+++ b/src/base/io/ioReadBlifMv.c
@@ -167,9 +167,9 @@ Abc_Ntk_t * Io_ReadBlifMv( char * pFileName, int fBlifMv, int fCheck )
     pDesign = Io_MvParse( p );
     if ( p->sError[0] )
         fprintf( stdout, "%s\n", p->sError );
+    Io_MvFree( p );
     if ( pDesign == NULL )
         return NULL;
-    Io_MvFree( p );
 // pDesign should be linked to all models of the design
 
     // make sure that everything is okay with the network structure
@@ -619,6 +619,12 @@ static void Io_MvReadPreparse( Io_MvMan_t * p )
             fprintf( stdout, "Line %d: Skipping EXDC network.\n", Io_MvGetLine(p, pCur) );
             break;
         }
+        else if ( !strncmp(pCur, "delay", 5) )
+        {}
+        else if ( !strncmp(pCur, "input_arrival", 13) )
+        {}
+        else if ( !strncmp(pCur, "output_required", 15) )
+        {}
         else
         {
             pCur--;
@@ -863,7 +869,7 @@ static int Io_MvParseLineLatch( Io_MvMod_t * p, char * pLine )
         else
         {
             if ( Vec_PtrSize(vTokens) > 3 )
-                Init = atoi( Vec_PtrEntry(vTokens,3) );
+                Init = atoi( Vec_PtrEntryLast(vTokens) );
             else
                 Init = 2;
             if ( Init < 0 || Init > 2 )
diff --git a/src/bdd/reo/module.make b/src/bdd/reo/module.make
index 7eb41e0e..3a636980 100644
--- a/src/bdd/reo/module.make
+++ b/src/bdd/reo/module.make
@@ -1,6 +1,7 @@
 SRC +=    src/bdd/reo/reoApi.c \
     src/bdd/reo/reoCore.c \
     src/bdd/reo/reoProfile.c \
+    src/bdd/reo/reoShuffle.c \
     src/bdd/reo/reoSift.c \
     src/bdd/reo/reoSwap.c \
     src/bdd/reo/reoTransfer.c \
diff --git a/src/bdd/reo/reoShuffle.c b/src/bdd/reo/reoShuffle.c
new file mode 100644
index 00000000..8dab67a4
--- /dev/null
+++ b/src/bdd/reo/reoShuffle.c
@@ -0,0 +1,224 @@
+/**CFile****************************************************************
+
+  FileName    [reoShuffle.c]
+
+  PackageName [REO: A specialized DD reordering engine.]
+
+  Synopsis    [Implementation of the two-variable swap.]
+
+  Author      [Alan Mishchenko]
+  
+  Affiliation [UC Berkeley]
+
+  Date        [Ver. 1.0. Started - October 15, 2002.]
+
+  Revision    [$Id: reoShuffle.c,v 1.0 2002/15/10 03:00:00 alanmi Exp $]
+
+***********************************************************************/
+
+#include "reo.h"
+
+////////////////////////////////////////////////////////////////////////
+///                        DECLARATIONS                              ///
+////////////////////////////////////////////////////////////////////////
+
+////////////////////////////////////////////////////////////////////////
+///                    FUNCTION DEFINITIONS                          ///
+////////////////////////////////////////////////////////////////////////
+
+/**Function*************************************************************
+
+  Synopsis    [This procedure is similar to Cudd_ShuffleHeap() and Cudd_bddPermute().]
+
+  Description [The first argument is the REO manager. The 2nd/3d
+  arguments are the function and its CUDD manager. The last argument
+  is the permutation to be implemented. The i-th entry of the permutation 
+  array contains the index of the variable that should be brought to the 
+  i-th level.  The size of the array should be equal or greater to 
+  the number of variables currently in use (that is, the size of CUDD
+  manager and the size of REO manager).]
+
+  SideEffects [Note that the resulting BDD is not referenced.]
+
+  SeeAlso     []
+
+***********************************************************************/
+DdNode * reoShuffle( reo_man * p, DdManager * dd, DdNode * bFunc, int * pPerm, int * pPermInv )
+{
+    DdNode * bFuncRes = NULL;
+    int i, k, v;
+
+    if ( Cudd_IsConstant(bFunc) )
+        return bFunc;
+
+    // set the initial parameters
+    p->dd    = dd;
+    p->nSupp = Cudd_SupportSize( dd, bFunc );
+    p->nTops = 1;
+//    p->nNodesBeg = Cudd_DagSize( bFunc );
+
+    // set the starting permutation
+    for ( i = 0; i < p->nSupp; i++ )
+    {
+        p->pOrderInt[i] = i;
+        p->pMapToPlanes[ dd->invperm[i] ] = i;
+        p->pMapToDdVarsFinal[i] = dd->invperm[i];
+    }
+
+    // set the initial parameters
+    p->nUnitsUsed = 0;
+    p->nNodesCur  = 0;
+    p->fThisIsAdd = 0;
+    p->Signature++;
+
+    // transfer the function from the CUDD package into REO's internal data structure
+    p->pTops[0] = reoTransferNodesToUnits_rec( p, bFunc );
+//    assert( p->nNodesBeg == p->nNodesCur );
+
+    // reorder one variable at a time
+    for ( i = 0; i < p->nSupp; i++ )
+    {
+        if ( p->pOrderInt[i] == pPerm[i] )
+            continue;
+        // find where is variable number pPerm[i]
+        for ( k = i + 1; k < p->nSupp; k++ )
+            if ( pPerm[i] == p->pOrderInt[k] )
+                break;
+        if ( k == p->nSupp )
+        {
+            printf( "reoShuffle() Error: Cannot find a variable.\n" );
+            goto finish;
+        }
+        // move the variable up
+        for ( v = k - 1; v >= i; v-- )
+        {
+            reoReorderSwapAdjacentVars( p, v, 1 );
+            // check if the number of nodes is not too large
+            if ( p->nNodesCur > 10000 )
+            {
+                printf( "reoShuffle() Error: BDD size is too large.\n" );
+                goto finish;
+            }
+        }
+        assert( p->pOrderInt[i] == pPerm[i] );
+    }
+
+    // set the initial parameters
+    p->nRefNodes  = 0;
+    p->nNodesCur  = 0;
+    p->Signature++;
+    // transfer the BDDs from REO's internal data structure to CUDD
+    bFuncRes = reoTransferUnitsToNodes_rec( p, p->pTops[0] ); Cudd_Ref( bFuncRes );
+    // undo the DDs referenced for storing in the cache
+    for ( i = 0; i < p->nRefNodes; i++ )
+        Cudd_RecursiveDeref( dd, p->pRefNodes[i] );
+
+    // verify zero refs of the terminal nodes
+//    assert( reoRecursiveDeref( p->pTops[0] ) );
+//    assert( reoCheckZeroRefs( &(p->pPlanes[p->nSupp]) ) );
+
+    // perform verification
+    if ( p->fVerify )
+    {
+        DdNode * bFuncPerm;
+        bFuncPerm = Cudd_bddPermute( dd, bFunc, pPermInv );  Cudd_Ref( bFuncPerm );
+        if ( bFuncPerm != bFuncRes )
+        {
+            printf( "REO: Internal verification has failed!\n" );
+            fflush( stdout );
+        }
+        Cudd_RecursiveDeref( dd, bFuncPerm );
+    }
+
+    // recycle the data structure
+    for ( i = 0; i <= p->nSupp; i++ )
+        reoUnitsRecycleUnitList( p, p->pPlanes + i );
+
+finish :
+    if ( bFuncRes )
+        Cudd_Deref( bFuncRes );
+    return bFuncRes;
+}
+
+
+
+/**Function*************************************************************
+
+  Synopsis    [Reorders the DD using REO and CUDD.]
+
+  Description [This function can be used to test the performance of the reordering package.]
+
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Extra_ShuffleTest( reo_man * pReo, DdManager * dd, DdNode * Func )
+{
+//    extern int runtime1, runtime2;
+
+    DdNode * Temp, * bRemap;
+    int nSuppSize, OffSet, Num, i, clk;
+    int pOrder[1000], pOrderInv[1000];
+    assert( dd->size < 1000 );
+
+    srand( 0x12341234 );
+    nSuppSize = Cudd_SupportSize( dd, Func );
+    if ( nSuppSize < 2 )
+        return;
+
+    for ( i = 0; i < nSuppSize; i++ )
+        pOrder[i] = i;
+    for ( i = 0; i < 120; i++ )
+    {
+        OffSet = rand() % (nSuppSize - 1);
+        Num = pOrder[OffSet];
+        pOrder[OffSet] = pOrder[OffSet+1];
+        pOrder[OffSet+1] = Num;
+    }
+    for ( i = 0; i < nSuppSize; i++ )
+        pOrderInv[pOrder[i]] = i;
+
+/*
+    printf( "Permutation: " );
+    for ( i = 0; i < nSuppSize; i++ )
+        printf( "%d ", pOrder[i] );
+    printf( "\n" );
+    printf( "Inverse permutation: " );
+    for ( i = 0; i < nSuppSize; i++ )
+        printf( "%d ", pOrderInv[i] );
+    printf( "\n" );
+*/
+
+    // create permutation
+//    Extra_ReorderSetVerification( pReo, 1 );
+    bRemap = Extra_bddRemapUp( dd, Func );  Cudd_Ref( bRemap );
+
+clk = clock();
+    Temp  = reoShuffle( pReo, dd, bRemap, pOrder, pOrderInv );  Cudd_Ref( Temp );
+//runtime1 += clock() - clk;
+
+//printf( "Initial = %d. Final = %d.\n", Cudd_DagSize(bRemap), Cudd_DagSize(Temp)  );
+
+    {
+        DdNode * bFuncPerm;
+clk = clock();
+        bFuncPerm = Cudd_bddPermute( dd, bRemap, pOrderInv );  Cudd_Ref( bFuncPerm );
+//runtime2 += clock() - clk;
+        if ( bFuncPerm != Temp )
+        {
+            printf( "REO: Internal verification has failed!\n" );
+            fflush( stdout );
+        }
+        Cudd_RecursiveDeref( dd, bFuncPerm );
+    }
+
+    Cudd_RecursiveDeref( dd, Temp );
+    Cudd_RecursiveDeref( dd, bRemap );
+}
+
+
+////////////////////////////////////////////////////////////////////////
+///                         END OF FILE                              ///
+////////////////////////////////////////////////////////////////////////
+
diff --git a/src/map/fpga/fpga.h b/src/map/fpga/fpga.h
index 188420b1..708cf385 100644
--- a/src/map/fpga/fpga.h
+++ b/src/map/fpga/fpga.h
@@ -78,7 +78,9 @@ extern Fpga_Node_t **  Fpga_ManReadOutputs( Fpga_Man_t * p );
 extern Fpga_Node_t *   Fpga_ManReadConst1 ( Fpga_Man_t * p );
 extern float *         Fpga_ManReadInputArrivals( Fpga_Man_t * p );
 extern int             Fpga_ManReadVerbose( Fpga_Man_t * p );
+extern int             Fpga_ManReadVarMax( Fpga_Man_t * p );
 extern float *         Fpga_ManReadLutAreas( Fpga_Man_t * p );
+extern Fpga_NodeVec_t* Fpga_ManReadMapping( Fpga_Man_t * p );
 extern void            Fpga_ManSetTimeToMap( Fpga_Man_t * p, int Time );
 extern void            Fpga_ManSetTimeToNet( Fpga_Man_t * p, int Time );
 extern void            Fpga_ManSetTimeTotal( Fpga_Man_t * p, int Time );
@@ -141,6 +143,7 @@ extern int             Fpga_Mapping( Fpga_Man_t * p );
 /*=== fpgaCut.c ===============================================================*/
 extern void            Fpga_MappingCreatePiCuts( Fpga_Man_t * p );
 extern void            Fpga_CutsCleanSign( Fpga_Man_t * pMan );
+extern void            Fpga_CutsCleanRoot( Fpga_Man_t * pMan );
 /*=== fpgaCutUtils.c =============================================================*/
 extern void            Fpga_CutCreateFromNode( Fpga_Man_t * p, int iRoot, int * pLeaves, int nLeaves );
 extern void            Fpga_MappingSetUsedCuts( Fpga_Man_t * p );
diff --git a/src/map/fpga/fpgaCreate.c b/src/map/fpga/fpgaCreate.c
index fa0f80d1..be71d74e 100644
--- a/src/map/fpga/fpgaCreate.c
+++ b/src/map/fpga/fpgaCreate.c
@@ -52,7 +52,9 @@ Fpga_Node_t **  Fpga_ManReadOutputs( Fpga_Man_t * p )                     { retu
 Fpga_Node_t *   Fpga_ManReadConst1 ( Fpga_Man_t * p )                     { return p->pConst1;    }
 float *         Fpga_ManReadInputArrivals( Fpga_Man_t * p )               { return p->pInputArrivals;}
 int             Fpga_ManReadVerbose( Fpga_Man_t * p )                     { return p->fVerbose;   }
+int             Fpga_ManReadVarMax( Fpga_Man_t * p )                      { return p->pLutLib->LutMax;     }
 float *         Fpga_ManReadLutAreas( Fpga_Man_t * p )                    { return p->pLutLib->pLutAreas;  }
+Fpga_NodeVec_t* Fpga_ManReadMapping( Fpga_Man_t * p )                     { return p->vMapping;   }
 void            Fpga_ManSetTimeToMap( Fpga_Man_t * p, int Time )          { p->timeToMap = Time;  }
 void            Fpga_ManSetTimeToNet( Fpga_Man_t * p, int Time )          { p->timeToNet = Time;  }
 void            Fpga_ManSetTimeTotal( Fpga_Man_t * p, int Time )          { p->timeTotal = Time;  }
diff --git a/src/map/fpga/fpgaCut.c b/src/map/fpga/fpgaCut.c
index a5505e72..ce688179 100644
--- a/src/map/fpga/fpgaCut.c
+++ b/src/map/fpga/fpgaCut.c
@@ -802,6 +802,28 @@ void Fpga_CutsCleanSign( Fpga_Man_t * pMan )
                 pCut->uSign = 0;
 }
 
+/**Function*************************************************************
+
+  Synopsis    [Clean the signatures.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Fpga_CutsCleanRoot( Fpga_Man_t * pMan )
+{
+    Fpga_Node_t * pNode;
+    Fpga_Cut_t * pCut;
+    int i;
+    for ( i = 0; i < pMan->nBins; i++ )
+        for ( pNode = pMan->pBins[i]; pNode; pNode = pNode->pNext )
+            for ( pCut = pNode->pCuts; pCut; pCut = pCut->pNext )
+                pCut->pRoot = NULL;
+}
+
 
 
 /**Function*************************************************************
diff --git a/src/map/fpga/fpgaSwitch.c b/src/map/fpga/fpgaSwitch.c
index c93e0de4..5e881959 100644
--- a/src/map/fpga/fpgaSwitch.c
+++ b/src/map/fpga/fpgaSwitch.c
@@ -139,8 +139,8 @@ float Fpga_MappingGetSwitching( Fpga_Man_t * pMan, Fpga_NodeVec_t * vMapping )
     }
     // add buffer for each CO driven by a CI
     for ( i = 0; i < pMan->nOutputs; i++ )
-        if ( Fpga_NodeIsVar(pMan->pOutputs[i]) && !Fpga_IsComplement(pMan->pOutputs[i]) )
-            Switch += pMan->pOutputs[i]->Switching;
+        if ( Fpga_NodeIsVar(Fpga_Regular(pMan->pOutputs[i])) && !Fpga_IsComplement(pMan->pOutputs[i]) )
+            Switch += Fpga_Regular(pMan->pOutputs[i])->Switching;
     return Switch;
 }
 
diff --git a/src/map/if/if.h b/src/map/if/if.h
index 3f3badf6..1b82f9a0 100644
--- a/src/map/if/if.h
+++ b/src/map/if/if.h
@@ -261,6 +261,7 @@ static inline void *     If_CutData( If_Cut_t * pCut )                       { r
 static inline void       If_CutSetData( If_Cut_t * pCut, void * pData )      { *(void **)pCut = pData;               }
 
 static inline int        If_CutLeaveNum( If_Cut_t * pCut )                   { return pCut->nLeaves;                             }
+static inline int *      If_CutLeaves( If_Cut_t * pCut )                     { return pCut->pLeaves;                             }
 static inline unsigned * If_CutTruth( If_Cut_t * pCut )                      { return pCut->pTruth;                              }
 static inline unsigned   If_CutSuppMask( If_Cut_t * pCut )                   { return (~(unsigned)0) >> (32-pCut->nLeaves);      }
 static inline int        If_CutTruthWords( int nVarsMax )                    { return nVarsMax <= 5 ? 1 : (1 << (nVarsMax - 5)); }
diff --git a/src/opt/lpk/lpkCore.c b/src/opt/lpk/lpkCore.c
index acea4866..e819a7fb 100644
--- a/src/opt/lpk/lpkCore.c
+++ b/src/opt/lpk/lpkCore.c
@@ -502,7 +502,7 @@ int Lpk_Resynthesize( Abc_Ntk_t * pNtk, Lpk_Par_t * pPars )
     double Delta;
     int i, Iter, nNodes, nNodesPrev, clk = clock();
     assert( Abc_NtkIsLogic(pNtk) );
-
+ 
     // sweep dangling nodes as a preprocessing step
     Abc_NtkSweep( pNtk, 0 );
 
@@ -510,6 +510,8 @@ int Lpk_Resynthesize( Abc_Ntk_t * pNtk, Lpk_Par_t * pPars )
     pPars->nLutSize = Abc_NtkGetFaninMax( pNtk );
     if ( pPars->nLutSize > 6 )
         pPars->nLutSize = 6;
+    if ( pPars->nLutSize < 3 )
+        pPars->nLutSize = 3;
     // adjust the number of crossbars based on LUT size
     if ( pPars->nVarsShared > pPars->nLutSize - 2 )
         pPars->nVarsShared = pPars->nLutSize - 2;
diff --git a/src/opt/res/resCore.c b/src/opt/res/resCore.c
index aa0eaeec..b22f0f5e 100644
--- a/src/opt/res/resCore.c
+++ b/src/opt/res/resCore.c
@@ -221,6 +221,8 @@ int Abc_NtkResynthesize( Abc_Ntk_t * pNtk, Res_Par_t * pPars )
     p->nTotalNets = Abc_NtkGetTotalFanins(pNtk);
     p->nTotalNodes = Abc_NtkNodeNum(pNtk);
     nFaninsMax = Abc_NtkGetFaninMax(pNtk);
+    if ( nFaninsMax > 8 )
+        nFaninsMax = 8;
 
     // perform the network sweep
     Abc_NtkSweep( pNtk, 0 );