diff options
author | Alan Mishchenko <alanmi@berkeley.edu> | 2007-12-25 08:01:00 -0800 |
---|---|---|
committer | Alan Mishchenko <alanmi@berkeley.edu> | 2007-12-25 08:01:00 -0800 |
commit | 00e9c3d06b590b0aac04bafddfd14115d14760f8 (patch) | |
tree | ac9b977538874c9f3b16ac03de0fd7265d19e025 | |
parent | 14c01eaccab87d14d1bd0eaa3fc491026349665e (diff) | |
download | abc-00e9c3d06b590b0aac04bafddfd14115d14760f8.tar.gz abc-00e9c3d06b590b0aac04bafddfd14115d14760f8.tar.bz2 abc-00e9c3d06b590b0aac04bafddfd14115d14760f8.zip |
Version abc71225
31 files changed, 1762 insertions, 111 deletions
@@ -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) @@ -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 @@ -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 ); |