diff options
author | Ruben Undheim <ruben.undheim@gmail.com> | 2016-11-03 23:18:00 +0100 |
---|---|---|
committer | Ruben Undheim <ruben.undheim@gmail.com> | 2016-11-03 23:18:00 +0100 |
commit | fefe0fc0430f4f173a25e674708aa0f4f0854b31 (patch) | |
tree | adb13b830212c269d58031f900d652f29013d2d7 | |
parent | 4f096fe65b77435daba019248273e547fa18d167 (diff) |
Imported yosys 0.7
69 files changed, 2188 insertions, 307 deletions
@@ -3,6 +3,105 @@ List of major changes and improvements between releases ======================================================= +Yosys 0.6 .. Yosys 0.7 +---------------------- + + * Various + - Added "yosys -D" feature + - Added support for installed plugins in $(DATDIR)/plugins/ + - Renamed opt_const to opt_expr + - Renamed opt_share to opt_merge + - Added "prep -flatten" and "synth -flatten" + - Added "prep -auto-top" and "synth -auto-top" + - Using "mfs" and "lutpack" in ABC lut mapping + - Support for abstract modules in chparam + - Cleanup abstract modules at end of "hierarchy -top" + - Added tristate buffer support to iopadmap + - Added opt_expr support for div/mod by power-of-two + - Added "select -assert-min <N> -assert-max <N>" + - Added "attrmvcp" pass + - Added "attrmap" command + - Added "tee +INT -INT" + - Added "zinit" pass + - Added "setparam -type" + - Added "shregmap" pass + - Added "setundef -init" + - Added "nlutmap -assert" + - Added $sop cell type and "abc -sop -I <num> -P <num>" + - Added "dc2" to default ABC scripts + - Added "deminout" + - Added "insbuf" command + - Added "prep -nomem" + - Added "opt_rmdff -keepdc" + - Added "prep -nokeepdc" + - Added initial version of "synth_gowin" + - Added "fsm_expand -full" + - Added support for fsm_encoding="user" + - Many improvements in GreenPAK4 support + - Added black box modules for all Xilinx 7-series lib cells + - Added synth_ice40 support for latches via logic loops + - Fixed ice40_opt lut unmapping, added "ice40_opt -unlut" + + * Build System + - Added ABCEXTERNAL and ABCURL make variables + - Added BINDIR, LIBDIR, and DATDIR make variables + - Added PKG_CONFIG make variable + - Added SEED make variable (for "make test") + - Added YOSYS_VER_STR make variable + - Updated min GCC requirement to GCC 4.8 + - Updated required Bison version to Bison 3.x + + * Internal APIs + - Added ast.h to exported headers + - Added ScriptPass helper class for script-like passes + - Added CellEdgesDatabase API + + * Front-ends and Back-ends + - Added filename glob support to all front-ends + - Added avail (black-box) module params to ilang format + - Added $display %m support + - Added support for $stop Verilog system task + - Added support for SystemVerilog packages + - Fixed procedural assignments to non-unique lvalues, e.g. {y,y} = {a,b} + - Added support for "active high" and "active low" latches in read_blif and write_blif + - Use init value "2" for all uninitialized FFs in BLIF back-end + - Added "read_blif -sop" + - Added "write_blif -noalias" + - Added various write_blif options for VTR support + - write_json: also write module attributes. + - Added "write_verilog -nodec -nostr -defparam" + - Added "read_verilog -norestrict -assume-asserts" + - Added support for bus interfaces to "read_liberty -lib" + - Added liberty parser support for types within cell decls + - Added "write_verilog -renameprefix -v" + - Added "write_edif -nogndvcc" + + * Formal Verification + - Support for hierarchical designs in smt2 back-end + - Yosys-smtbmc: Support for hierarchical VCD dumping + - Added $initstate cell type and vlog function + - Added $anyconst and $anyseq cell types and vlog functions + - Added printing of code loc of failed asserts to yosys-smtbmc + - Added memory_memx pass, "memory -memx", and "prep -memx" + - Added "proc_mux -ifx" + - Added "yosys-smtbmc -g" + - Deprecated "write_smt2 -regs" (by default on now) + - Made "write_smt2 -bv -mem" default, added "write_smt2 -nobv -nomem" + - Added support for memories to smtio.py + - Added "yosys-smtbmc --dump-vlogtb" + - Added "yosys-smtbmc --smtc --dump-smtc" + - Added "yosys-smtbmc --dump-all" + - Added assertpmux command + - Added "yosys-smtbmc --unroll" + - Added $past, $stable, $rose, $fell SVA functions + - Added "yosys-smtbmc --noinfo and --dummy" + - Added "yosys-smtbmc --noincr" + - Added "yosys-smtbmc --cex <filename>" + - Added $ff and $_FF_ cell types + - Added $global_clock verilog syntax support for creating $ff cells + - Added clk2fflogic + + Yosys 0.5 .. Yosys 0.6 ---------------------- @@ -72,7 +72,7 @@ else LDLIBS += -lrt endif -YOSYS_VER := 0.6+$(shell test -e .git && { git log --author=clifford@clifford.at --oneline 5869d26da021.. | wc -l; }) +YOSYS_VER := 0.7 GIT_REV := $(shell cd $(YOSYS_SRC) && git rev-parse --short HEAD 2> /dev/null || echo UNKNOWN) OBJS = kernel/version_$(GIT_REV).o @@ -82,14 +82,14 @@ OBJS = kernel/version_$(GIT_REV).o # is just a symlink to your actual ABC working directory, as 'make mrproper' # will remove the 'abc' directory and you do not want to accidentally # delete your work on ABC.. -ABCREV = 8e08604f8ad3 +ABCREV = eb6eca6807cc ABCPULL = 1 ABCURL ?= https://bitbucket.org/alanmi/abc ABCMKARGS = CC="$(CXX)" CXX="$(CXX)" # set ABCEXTERNAL = <abc-command> to use an external ABC instance # Note: The in-tree ABC (yosys-abc) will not be installed when ABCEXTERNAL is set. -ABCEXTERNAL = +ABCEXTERNAL ?= define newline @@ -370,10 +370,12 @@ libyosys.so: $(filter-out kernel/driver.o,$(OBJS)) $(Q) mkdir -p $(dir $@) $(P) $(CXX) -o $@ -c $(CPPFLAGS) $(CXXFLAGS) $< +YOSYS_VER_STR := Yosys $(YOSYS_VER) (git sha1 $(GIT_REV), $(notdir $(CXX)) $(shell \ + $(CXX) --version | tr ' ()' '\n' | grep '^[0-9]' | head -n1) $(filter -f% -m% -O% -DNDEBUG,$(CXXFLAGS))) + kernel/version_$(GIT_REV).cc: $(YOSYS_SRC)/Makefile $(P) rm -f kernel/version_*.o kernel/version_*.d kernel/version_*.cc - $(Q) mkdir -p kernel && echo "namespace Yosys { extern const char *yosys_version_str; const char *yosys_version_str=\"Yosys $(YOSYS_VER) (git sha1 $(GIT_REV), $(notdir $(CXX)) ` \ - $(CXX) --version | tr ' ()' '\n' | grep '^[0-9]' | head -n1` $(filter -f% -m% -O% -DNDEBUG,$(CXXFLAGS)))\"; }" > kernel/version_$(GIT_REV).cc + $(Q) mkdir -p kernel && echo "namespace Yosys { extern const char *yosys_version_str; const char *yosys_version_str=\"$(YOSYS_VER_STR)\"; }" > kernel/version_$(GIT_REV).cc yosys-config: misc/yosys-config.in $(P) $(SED) -e 's#@CXXFLAGS@#$(subst -I. -I"$(YOSYS_SRC)",-I"$(DATDIR)/include",$(CXXFLAGS))#;' \ @@ -404,16 +406,22 @@ endif yosys-abc$(EXE): abc/abc-$(ABCREV)$(EXE) $(P) cp abc/abc-$(ABCREV)$(EXE) yosys-abc$(EXE) +ifneq ($(SEED),) +SEEDOPT="-S $(SEED)" +else +SEEDOPT="" +endif + test: $(TARGETS) $(EXTRA_TARGETS) - +cd tests/simple && bash run-test.sh - +cd tests/hana && bash run-test.sh - +cd tests/asicworld && bash run-test.sh - +cd tests/realmath && bash run-test.sh - +cd tests/share && bash run-test.sh - +cd tests/fsm && bash run-test.sh + +cd tests/simple && bash run-test.sh $(SEEDOPT) + +cd tests/hana && bash run-test.sh $(SEEDOPT) + +cd tests/asicworld && bash run-test.sh $(SEEDOPT) + +cd tests/realmath && bash run-test.sh $(SEEDOPT) + +cd tests/share && bash run-test.sh $(SEEDOPT) + +cd tests/fsm && bash run-test.sh $(SEEDOPT) +cd tests/techmap && bash run-test.sh - +cd tests/memories && bash run-test.sh - +cd tests/bram && bash run-test.sh + +cd tests/memories && bash run-test.sh $(SEEDOPT) + +cd tests/bram && bash run-test.sh $(SEEDOPT) +cd tests/various && bash run-test.sh +cd tests/sat && bash run-test.sh @echo "" @@ -374,6 +374,27 @@ Verilog Attributes and non-standard features and constant values). The intended use for this is synthesis-time DRC. +Non-standard or SystemVerilog features for formal verification +============================================================== + +- Support for "assert", "assume", and "restrict" is enabled when + read_verilog is called with -formal. + +- The system task $initstate evaluates to 1 in the initial state and + to 0 otherwise. + +- The system task $anyconst evaluates to any constant value. + +- The system task $anyseq evaluates to any value, possibly a different + value in each cycle. + +- The SystemVerilog tasks $past, $stable, $rose and $fell are supported + in any clocked block. + +- The syntax @($global_clock) can be used to create FFs that have no + explicit clock input ($ff cells). + + Supported features from SystemVerilog ===================================== @@ -384,8 +405,8 @@ from SystemVerilog: form. In module context: "assert property (<expression>);" and within an always block: "assert(<expression>);". It is transformed to a $assert cell. -- The "assume" statements from SystemVerilog are also supported. The same - limitations as with the "assert" statement apply. +- The "assume" and "restrict" statements from SystemVerilog are also + supported. The same limitations as with the "assert" statement apply. - The keywords "always_comb", "always_ff" and "always_latch", "logic" and "bit" are supported. diff --git a/backends/blif/blif.cc b/backends/blif/blif.cc index 6a379e67..d9d0cc17 100644 --- a/backends/blif/blif.cc +++ b/backends/blif/blif.cc @@ -77,9 +77,6 @@ struct BlifDumper case State::S1: init_bits[initsig[i]] = 1; break; - case State::Sx: - init_bits[initsig[i]] = 2; - break; default: break; } @@ -126,7 +123,7 @@ struct BlifDumper sigmap.apply(sig); if (init_bits.count(sig) == 0) - return ""; + return " 2"; string str = stringf(" %d", init_bits.at(sig)); @@ -315,6 +312,12 @@ struct BlifDumper continue; } + if (!config->icells_mode && cell->type == "$_FF_") { + f << stringf(".latch %s %s%s\n", cstr(cell->getPort("\\D")), cstr(cell->getPort("\\Q")), + cstr_init(cell->getPort("\\Q"))); + continue; + } + if (!config->icells_mode && cell->type == "$_DFF_N_") { f << stringf(".latch %s %s fe %s%s\n", cstr(cell->getPort("\\D")), cstr(cell->getPort("\\Q")), cstr(cell->getPort("\\C")), cstr_init(cell->getPort("\\Q"))); diff --git a/backends/ilang/ilang_backend.cc b/backends/ilang/ilang_backend.cc index 03e29c52..16d1a97f 100644 --- a/backends/ilang/ilang_backend.cc +++ b/backends/ilang/ilang_backend.cc @@ -228,6 +228,7 @@ void ILANG_BACKEND::dump_proc_sync(std::ostream &f, std::string indent, const RT f << stringf("\n"); break; case RTLIL::STa: f << stringf("always\n"); break; + case RTLIL::STg: f << stringf("global\n"); break; case RTLIL::STi: f << stringf("init\n"); break; } @@ -277,6 +278,13 @@ void ILANG_BACKEND::dump_module(std::ostream &f, std::string indent, RTLIL::Modu } f << stringf("%s" "module %s\n", indent.c_str(), module->name.c_str()); + + if (!module->avail_parameters.empty()) { + if (only_selected) + f << stringf("\n"); + for (auto &p : module->avail_parameters) + f << stringf("%s" " parameter %s\n", indent.c_str(), p.c_str()); + } } if (print_body) diff --git a/backends/smt2/smt2.cc b/backends/smt2/smt2.cc index 9a25f3a2..ddac6900 100644 --- a/backends/smt2/smt2.cc +++ b/backends/smt2/smt2.cc @@ -379,7 +379,7 @@ struct Smt2Worker return; } - if (cell->type == "$_DFF_P_" || cell->type == "$_DFF_N_") + if (cell->type.in("$_FF_", "$_DFF_P_", "$_DFF_N_")) { registers.insert(cell); decls.push_back(stringf("(declare-fun |%s#%d| (|%s_s|) Bool) ; %s\n", @@ -407,7 +407,7 @@ struct Smt2Worker if (bvmode) { - if (cell->type == "$dff") + if (cell->type.in("$ff", "$dff")) { registers.insert(cell); decls.push_back(stringf("(declare-fun |%s#%d| (|%s_s|) (_ BitVec %d)) ; %s\n", @@ -417,7 +417,7 @@ struct Smt2Worker return; } - if (cell->type == "$anyconst") + if (cell->type.in("$anyconst", "$anyseq")) { registers.insert(cell); decls.push_back(stringf("; yosys-smt2-%s %s#%d %s\n", cell->type.c_str() + 1, get_id(module), idcounter, @@ -586,7 +586,7 @@ struct Smt2Worker return; } - log_error("Unsupported cell type %s for cell %s.%s. (Maybe this cell type would be supported in -bv or -mem mode?)\n", + log_error("Unsupported cell type %s for cell %s.%s.\n", log_id(cell->type), log_id(module), log_id(cell)); } @@ -596,7 +596,7 @@ struct Smt2Worker pool<SigBit> reg_bits; for (auto cell : module->cells()) - if (cell->type.in("$_DFF_P_", "$_DFF_N_", "$dff")) { + if (cell->type.in("$ff", "$dff", "$_FF_", "$_DFF_P_", "$_DFF_N_")) { // not using sigmap -- we want the net directly at the dff output for (auto bit : cell->getPort("\\Q")) reg_bits.insert(bit); @@ -674,14 +674,14 @@ struct Smt2Worker for (auto cell : this_regs) { - if (cell->type == "$_DFF_P_" || cell->type == "$_DFF_N_") + if (cell->type.in("$_FF_", "$_DFF_P_", "$_DFF_N_")) { std::string expr_d = get_bool(cell->getPort("\\D")); std::string expr_q = get_bool(cell->getPort("\\Q"), "next_state"); trans.push_back(stringf(" (= %s %s) ; %s %s\n", expr_d.c_str(), expr_q.c_str(), get_id(cell), log_signal(cell->getPort("\\Q")))); } - if (cell->type == "$dff") + if (cell->type.in("$ff", "$dff")) { std::string expr_d = get_bv(cell->getPort("\\D")); std::string expr_q = get_bv(cell->getPort("\\Q"), "next_state"); diff --git a/backends/smt2/smtbmc.py b/backends/smt2/smtbmc.py index bb763647..04c25f91 100644 --- a/backends/smt2/smtbmc.py +++ b/backends/smt2/smtbmc.py @@ -26,6 +26,7 @@ skip_steps = 0 step_size = 1 num_steps = 20 vcdfile = None +cexfile = None vlogtbfile = None inconstr = list() outconstr = None @@ -61,6 +62,9 @@ yosys-smtbmc [options] <yosys_smt2_output> --smtc <constr_filename> read constraints file + --cex <cex_filename> + read cex file as written by ABC's "write_cex -n" + --noinfo only run the core proof, do not collect and print any additional information (e.g. which assert failed) @@ -94,7 +98,7 @@ yosys-smtbmc [options] <yosys_smt2_output> try: opts, args = getopt.getopt(sys.argv[1:], so.shortopts + "t:igm:", so.longopts + - ["final-only", "assume-skipped=", "smtc=", "dump-vcd=", "dump-vlogtb=", "dump-smtc=", "dump-all", "noinfo"]) + ["final-only", "assume-skipped=", "smtc=", "cex=", "dump-vcd=", "dump-vlogtb=", "dump-smtc=", "dump-all", "noinfo"]) except: usage() @@ -118,6 +122,8 @@ for o, a in opts: final_only = True elif o == "--smtc": inconstr.append(a) + elif o == "--cex": + cexfile = a elif o == "--dump-vcd": vcdfile = a elif o == "--dump-vlogtb": @@ -146,6 +152,7 @@ if len(args) != 1: constr_final_start = None constr_asserts = defaultdict(list) constr_assumes = defaultdict(list) +constr_write = list() for fn in inconstr: current_states = None @@ -229,6 +236,14 @@ for fn in inconstr: continue + if tokens[0] == "write": + constr_write.append(" ".join(tokens[1:])) + continue + + if tokens[0] == "logic": + so.logic = " ".join(tokens[1:]) + continue + assert 0 @@ -240,7 +255,7 @@ def get_constr_expr(db, state, final=False, getvalues=False): if state not in db: return ([], [], []) if getvalues else "true" - netref_regex = re.compile(r'(^|[( ])\[(-?[0-9]+:|)([^\]]+)\](?=[ )]|$)') + netref_regex = re.compile(r'(^|[( ])\[(-?[0-9]+:|)([^\]]*)\](?=[ )]|$)') def replace_netref(match): state_sel = match.group(2) @@ -280,6 +295,9 @@ def get_constr_expr(db, state, final=False, getvalues=False): smt = SmtIo(opts=so) +if noinfo and vcdfile is None and vlogtbfile is None and outconstr is None: + smt.produce_models = False + def print_msg(msg): print("%s %s" % (smt.timestamp(), msg)) sys.stdout.flush() @@ -290,12 +308,46 @@ with open(args[0], "r") as f: for line in f: smt.write(line) +for line in constr_write: + smt.write(line) + if topmod is None: topmod = smt.topmod assert topmod is not None assert topmod in smt.modinfo +if cexfile is not None: + with open(cexfile, "r") as f: + cex_regex = re.compile(r'([^\[@=]+)(\[\d+\])?([^@=]*)(@\d+)=([01])') + for entry in f.read().split(): + match = cex_regex.match(entry) + assert match + + name, bit, extra_name, step, val = match.group(1), match.group(2), match.group(3), match.group(4), match.group(5) + + if extra_name != "": + continue + + if name not in smt.modinfo[topmod].inputs: + continue + + if bit is None: + bit = 0 + else: + bit = int(bit[1:-1]) + + step = int(step[1:]) + val = int(val) + + if smt.modinfo[topmod].wsize[name] == 1: + assert bit == 0 + smtexpr = "(= [%s] %s)" % (name, "true" if val else "false") + else: + smtexpr = "(= ((_ extract %d %d) [%s]) #b%d)" % (bit, bit, name, val) + + # print("cex@%d: %s" % (step, smtexpr)) + constr_assumes[step].append((cexfile, smtexpr)) def write_vcd_trace(steps_start, steps_stop, index): filename = vcdfile.replace("%", index) @@ -625,9 +677,10 @@ else: # not tempind smt.write("(pop 1)") - for i in range(step, last_check_step+1): - smt.write("(assert (|%s_a| s%d))" % (topmod, i)) - smt.write("(assert %s)" % get_constr_expr(constr_asserts, i)) + if (constr_final_start is not None) or (last_check_step+1 != num_steps): + for i in range(step, last_check_step+1): + smt.write("(assert (|%s_a| s%d))" % (topmod, i)) + smt.write("(assert %s)" % get_constr_expr(constr_asserts, i)) if constr_final_start is not None: for i in range(step, last_check_step+1): diff --git a/backends/smt2/smtio.py b/backends/smt2/smtio.py index 58554572..865eed1f 100644 --- a/backends/smt2/smtio.py +++ b/backends/smt2/smtio.py @@ -53,6 +53,9 @@ class SmtIo: self.logic_ax = True self.logic_uf = True self.logic_bv = True + self.produce_models = True + self.smt2cache = [list()] + self.p = None if opts is not None: self.logic = opts.logic @@ -62,6 +65,9 @@ class SmtIo: self.dummy_file = opts.dummy_file self.timeinfo = opts.timeinfo self.unroll = opts.unroll + self.noincr = opts.noincr + self.info_stmts = opts.info_stmts + self.nocomments = opts.nocomments else: self.solver = "z3" @@ -70,30 +76,40 @@ class SmtIo: self.dummy_file = None self.timeinfo = True self.unroll = False + self.noincr = False + self.info_stmts = list() + self.nocomments = False if self.solver == "yices": - popen_vargs = ['yices-smt2', '--incremental'] + self.popen_vargs = ['yices-smt2', '--incremental'] if self.solver == "z3": - popen_vargs = ['z3', '-smt2', '-in'] + self.popen_vargs = ['z3', '-smt2', '-in'] if self.solver == "cvc4": - popen_vargs = ['cvc4', '--incremental', '--lang', 'smt2'] + self.popen_vargs = ['cvc4', '--incremental', '--lang', 'smt2'] if self.solver == "mathsat": - popen_vargs = ['mathsat'] + self.popen_vargs = ['mathsat'] if self.solver == "boolector": - popen_vargs = ['boolector', '--smt2', '-i'] + self.popen_vargs = ['boolector', '--smt2', '-i'] self.unroll = True + if self.solver == "abc": + self.popen_vargs = ['yosys-abc', '-S', '%blast; &sweep -C 5000; &syn4; &cec -s -m -C 2000'] + self.logic_ax = False + self.unroll = True + self.noincr = True + if self.solver == "dummy": assert self.dummy_file is not None self.dummy_fd = open(self.dummy_file, "r") else: if self.dummy_file is not None: self.dummy_fd = open(self.dummy_file, "w") - self.p = subprocess.Popen(popen_vargs, stdin=subprocess.PIPE, stdout=subprocess.PIPE, stderr=subprocess.STDOUT) + if not self.noincr: + self.p = subprocess.Popen(self.popen_vargs, stdin=subprocess.PIPE, stdout=subprocess.PIPE, stderr=subprocess.STDOUT) if self.unroll: self.logic_uf = False @@ -123,9 +139,15 @@ class SmtIo: if self.logic_bv: self.logic += "BV" self.setup_done = True - self.write("(set-option :produce-models true)") + + if self.produce_models: + self.write("(set-option :produce-models true)") + self.write("(set-logic %s)" % self.logic) + for stmt in self.info_stmts: + self.write(stmt) + def timestamp(self): secs = int(time() - self.start_time) return "## %6d %3d:%02d:%02d " % (secs, secs // (60*60), (secs // 60) % 60, secs % 60) @@ -187,11 +209,12 @@ class SmtIo: stmt = stmt.strip() - if unroll and self.unroll: + if self.nocomments or self.unroll: if stmt.startswith(";"): return - stmt = re.sub(r" ;.*", "", stmt) + + if unroll and self.unroll: stmt = self.unroll_buffer + stmt self.unroll_buffer = "" @@ -246,8 +269,22 @@ class SmtIo: self.debug_file.flush() if self.solver != "dummy": - self.p.stdin.write(bytes(stmt + "\n", "ascii")) - self.p.stdin.flush() + if self.noincr: + if self.p is not None and not stmt.startswith("(get-"): + self.p.stdin.close() + self.p = None + if stmt == "(push 1)": + self.smt2cache.append(list()) + elif stmt == "(pop 1)": + self.smt2cache.pop() + else: + if self.p is not None: + self.p.stdin.write(bytes(stmt + "\n", "ascii")) + self.p.stdin.flush() + self.smt2cache[-1].append(stmt) + else: + self.p.stdin.write(bytes(stmt + "\n", "ascii")) + self.p.stdin.flush() def info(self, stmt): if not stmt.startswith("; yosys-smt2-"): @@ -355,11 +392,20 @@ class SmtIo: def check_sat(self): if self.debug_print: print("> (check-sat)") - if self.debug_file: + if self.debug_file and not self.nocomments: print("; running check-sat..", file=self.debug_file) self.debug_file.flush() if self.solver != "dummy": + if self.noincr: + if self.p is not None: + self.p.stdin.close() + self.p = None + self.p = subprocess.Popen(self.popen_vargs, stdin=subprocess.PIPE, stdout=subprocess.PIPE, stderr=subprocess.STDOUT) + for cache_ctx in self.smt2cache: + for cache_stmt in cache_ctx: + self.p.stdin.write(bytes(cache_stmt + "\n", "ascii")) + self.p.stdin.write(bytes("(check-sat)\n", "ascii")) self.p.stdin.flush() @@ -495,6 +541,10 @@ class SmtIo: def net_expr(self, mod, base, path): if len(path) == 1: assert mod in self.modinfo + if path[0] == "": + return base + if path[0] in self.modinfo[mod].cells: + return "(|%s_h %s| %s)" % (mod, path[0], base) if path[0] in self.modinfo[mod].wsize: return "(|%s_n %s| %s)" % (mod, path[0], base) if path[0] in self.modinfo[mod].memories: @@ -555,21 +605,24 @@ class SmtIo: return [self.bv2bin(v) for v in self.get_net_list(mod_name, net_path_list, state_name)] def wait(self): - if self.solver != "dummy": + if self.p is not None: self.p.wait() class SmtOpts: def __init__(self): self.shortopts = "s:v" - self.longopts = ["unroll", "no-progress", "dump-smt2=", "logic=", "dummy="] + self.longopts = ["unroll", "noincr", "noprogress", "dump-smt2=", "logic=", "dummy=", "info=", "nocomments"] self.solver = "z3" self.debug_print = False self.debug_file = None self.dummy_file = None self.unroll = False + self.noincr = False self.timeinfo = True self.logic = None + self.info_stmts = list() + self.nocomments = False def handle(self, o, a): if o == "-s": @@ -578,7 +631,9 @@ class SmtOpts: self.debug_print = True elif o == "--unroll": self.unroll = True - elif o == "--no-progress": + elif o == "--noincr": + self.noincr = True + elif o == "--noprogress": self.timeinfo = True elif o == "--dump-smt2": self.debug_file = open(a, "w") @@ -586,6 +641,10 @@ class SmtOpts: self.logic = a elif o == "--dummy": self.dummy_file = a + elif o == "--info": + self.info_stmts.append(a) + elif o == "--nocomments": + self.nocomments = True else: return False return True @@ -609,11 +668,21 @@ class SmtOpts: --unroll unroll uninterpreted functions - --no-progress + --noincr + don't use incremental solving, instead restart solver for + each (check-sat). This also avoids (push) and (pop). + + --noprogress disable timer display during solving --dump-smt2 <filename> write smt2 statements to file + + --info <smt2-info-stmt> + include the specified smt2 info statement in the smt2 output + + --nocomments + strip all comments from the generated smt2 code """ diff --git a/backends/verilog/verilog_backend.cc b/backends/verilog/verilog_backend.cc index 52cf861d..a617215f 100644 --- a/backends/verilog/verilog_backend.cc +++ b/backends/verilog/verilog_backend.cc @@ -33,10 +33,11 @@ USING_YOSYS_NAMESPACE PRIVATE_NAMESPACE_BEGIN -bool norename, noattr, attr2comment, noexpr, nodec, nostr, defparam; +bool verbose, norename, noattr, attr2comment, noexpr, nodec, nostr, defparam; int auto_name_counter, auto_name_offset, auto_name_digits; std::map<RTLIL::IdString, int> auto_name_map; std::set<RTLIL::IdString> reg_wires, reg_ct; +std::string auto_prefix; RTLIL::Module *active_module; @@ -85,13 +86,14 @@ void reset_auto_counter(RTLIL::Module *module) for (size_t i = 10; i < auto_name_offset + auto_name_map.size(); i = i*10) auto_name_digits++; - for (auto it = auto_name_map.begin(); it != auto_name_map.end(); ++it) - log(" renaming `%s' to `_%0*d_'.\n", it->first.c_str(), auto_name_digits, auto_name_offset + it->second); + if (verbose) + for (auto it = auto_name_map.begin(); it != auto_name_map.end(); ++it) + log(" renaming `%s' to `%s_%0*d_'.\n", it->first.c_str(), auto_prefix.c_str(), auto_name_digits, auto_name_offset + it->second); } std::string next_auto_id() { - return stringf("_%0*d_", auto_name_digits, auto_name_offset + auto_name_counter++); + return stringf("%s_%0*d_", auto_prefix.c_str(), auto_name_digits, auto_name_offset + auto_name_counter++); } std::string id(RTLIL::IdString internal_id, bool may_rename = true) @@ -100,7 +102,7 @@ std::string id(RTLIL::IdString internal_id, bool may_rename = true) bool do_escape = false; if (may_rename && auto_name_map.count(internal_id) != 0) - return stringf("_%0*d_", auto_name_digits, auto_name_offset + auto_name_map[internal_id]); + return stringf("%s_%0*d_", auto_prefix.c_str(), auto_name_digits, auto_name_offset + auto_name_map[internal_id]); if (*str == '\\') str++; @@ -1342,6 +1344,9 @@ struct VerilogBackend : public Backend { log(" instead of a backslash prefix) are changed to short names in the\n"); log(" format '_<number>_'.\n"); log("\n"); + log(" -renameprefix <prefix>\n"); + log(" insert this prefix in front of auto-generated instance names\n"); + log("\n"); log(" -noattr\n"); log(" with this option no attributes are included in the output\n"); log("\n"); @@ -1376,6 +1381,9 @@ struct VerilogBackend : public Backend { log(" only write selected modules. modules must be selected entirely or\n"); log(" not at all.\n"); log("\n"); + log(" -v\n"); + log(" verbose output (print new names of all renamed wires and cells)\n"); + log("\n"); log("Note that RTLIL processes can't always be mapped directly to Verilog\n"); log("always blocks. This frontend should only be used to export an RTLIL\n"); log("netlist, i.e. after the \"proc\" pass has been used to convert all\n"); @@ -1387,6 +1395,7 @@ struct VerilogBackend : public Backend { { log_header(design, "Executing Verilog backend.\n"); + verbose = false; norename = false; noattr = false; attr2comment = false; @@ -1394,6 +1403,7 @@ struct VerilogBackend : public Backend { nodec = false; nostr = false; defparam = false; + auto_prefix = ""; bool blackboxes = false; bool selected = false; @@ -1431,6 +1441,10 @@ struct VerilogBackend : public Backend { norename = true; continue; } + if (arg == "-renameprefix" && argidx+1 < args.size()) { + auto_prefix = args[++argidx]; + continue; + } if (arg == "-noattr") { noattr = true; continue; @@ -1463,6 +1477,10 @@ struct VerilogBackend : public Backend { selected = true; continue; } + if (arg == "-v") { + verbose = true; + continue; + } break; } extra_args(f, filename, args, argidx); diff --git a/examples/smtbmc/demo7.v b/examples/smtbmc/demo7.v index 75b3865c..63f6272f 100644 --- a/examples/smtbmc/demo7.v +++ b/examples/smtbmc/demo7.v @@ -1,6 +1,7 @@ // Demo for memory initialization -module demo7 (input [2:0] addr); +module demo7; + wire [2:0] addr = $anyseq; reg [15:0] memory [0:7]; initial begin diff --git a/frontends/ast/ast.cc b/frontends/ast/ast.cc index fd272400..92513a24 100644 --- a/frontends/ast/ast.cc +++ b/frontends/ast/ast.cc @@ -934,10 +934,15 @@ static AstModule* process_module(AstNode *ast, bool defer) if (flag_lib) { std::vector<AstNode*> new_children; for (auto child : ast->children) { - if (child->type == AST_WIRE && (child->is_input || child->is_output)) + if (child->type == AST_WIRE && (child->is_input || child->is_output)) { new_children.push_back(child); - else + } else if (child->type == AST_PARAMETER) { + child->delete_children(); + child->children.push_back(AstNode::mkconst_int(0, false, 0)); + new_children.push_back(child); + } else { delete child; + } } ast->children.swap(new_children); ast->attributes["\\blackbox"] = AstNode::mkconst_int(1, false); diff --git a/frontends/ast/genrtlil.cc b/frontends/ast/genrtlil.cc index 3c57162a..db8d7409 100644 --- a/frontends/ast/genrtlil.cc +++ b/frontends/ast/genrtlil.cc @@ -220,12 +220,19 @@ struct AST_INTERNAL::ProcessGenerator subst_lvalue_to = new_temp_signal(subst_lvalue_from); subst_lvalue_map = subst_lvalue_from.to_sigbit_map(subst_lvalue_to); + bool found_global_syncs = false; bool found_anyedge_syncs = false; for (auto child : always->children) - if (child->type == AST_EDGE) - found_anyedge_syncs = true; + if (child->type == AST_EDGE) { + if (GetSize(child->children) == 1 && child->children.at(0)->type == AST_IDENTIFIER && child->children.at(0)->str == "\\$global_clock") + found_global_syncs = true; + else + found_anyedge_syncs = true; + } if (found_anyedge_syncs) { + if (found_global_syncs) + log_error("Found non-synthesizable event list at %s:%d!\n", always->filename.c_str(), always->linenum); log("Note: Assuming pure combinatorial block at %s:%d in\n", always->filename.c_str(), always->linenum); log("compliance with IEC 62142(E):2005 / IEEE Std. 1364.1(E):2002. Recommending\n"); log("use of @* instead of @(...) for better match of synthesis and simulation.\n"); @@ -236,7 +243,7 @@ struct AST_INTERNAL::ProcessGenerator for (auto child : always->children) if (child->type == AST_POSEDGE || child->type == AST_NEGEDGE) { found_clocked_sync = true; - if (found_anyedge_syncs) + if (found_global_syncs || found_anyedge_syncs) log_error("Found non-synthesizable event list at %s:%d!\n", always->filename.c_str(), always->linenum); RTLIL::SyncRule *syncrule = new RTLIL::SyncRule; syncrule->type = child->type == AST_POSEDGE ? RTLIL::STp : RTLIL::STn; @@ -248,7 +255,7 @@ struct AST_INTERNAL::ProcessGenerator } if (proc->syncs.empty()) { RTLIL::SyncRule *syncrule = new RTLIL::SyncRule; - syncrule->type = RTLIL::STa; + syncrule->type = found_global_syncs ? RTLIL::STg : RTLIL::STa; syncrule->signal = RTLIL::SigSpec(); addChunkActions(syncrule->actions, subst_lvalue_from, subst_lvalue_to, true); proc->syncs.push_back(syncrule); @@ -755,7 +762,7 @@ void AstNode::detectSignWidthWorker(int &width_hint, bool &sign_hint, bool *foun break; case AST_FCALL: - if (str == "\\$anyconst") { + if (str == "\\$anyconst" || str == "\\$anyseq") { if (GetSize(children) == 1) { while (children[0]->simplify(true, false, false, 1, -1, false, true) == true) { } if (children[0]->type != AST_CONSTANT) @@ -1264,6 +1271,7 @@ RTLIL::SigSpec AstNode::genRTLIL(int width_hint, bool sign_hint) wire->attributes["\\src"] = stringf("%s:%d", filename.c_str(), linenum); int mem_width, mem_size, addr_bits; + is_signed = id2ast->is_signed; id2ast->meminfo(mem_width, mem_size, addr_bits); RTLIL::SigSpec addr_sig = children[0]->genRTLIL(); @@ -1458,7 +1466,7 @@ RTLIL::SigSpec AstNode::genRTLIL(int width_hint, bool sign_hint) } break; case AST_FCALL: { - if (str == "\\$anyconst") + if (str == "\\$anyconst" || str == "\\$anyseq") { string myid = stringf("%s$%d", str.c_str() + 1, autoidx++); int width = width_hint; diff --git a/frontends/ast/simplify.cc b/frontends/ast/simplify.cc index 57aa648c..9d5c75fe 100644 --- a/frontends/ast/simplify.cc +++ b/frontends/ast/simplify.cc @@ -1510,6 +1510,7 @@ skip_dynamic_range_lvalue_expansion:; } int mem_width, mem_size, addr_bits; + bool mem_signed = children[0]->id2ast->is_signed; children[0]->id2ast->meminfo(mem_width, mem_size, addr_bits); int data_range_left = children[0]->id2ast->children[0]->range_left; @@ -1529,6 +1530,7 @@ skip_dynamic_range_lvalue_expansion:; AstNode *wire_data = new AstNode(AST_WIRE, new AstNode(AST_RANGE, mkconst_int(mem_width-1, true), mkconst_int(0, true))); wire_data->str = id_data; + wire_data->is_signed = mem_signed; current_ast_mod->children.push_back(wire_data); current_scope[wire_data->str] = wire_data; while (wire_data->simplify(true, false, false, 1, -1, false, false)) { } @@ -1807,8 +1809,8 @@ skip_dynamic_range_lvalue_expansion:; goto apply_newNode; } - // $anyconst is mapped in AstNode::genRTLIL() - if (str == "\\$anyconst") { + // $anyconst and $anyseq are mapped in AstNode::genRTLIL() + if (str == "\\$anyconst" || str == "\\$anyseq") { recursion_counter--; return false; } @@ -2894,6 +2896,7 @@ bool AstNode::mem2reg_as_needed_pass2(pool<AstNode*> &mem2reg_set, AstNode *mod, std::string id_addr = sstr.str() + "_ADDR", id_data = sstr.str() + "_DATA"; int mem_width, mem_size, addr_bits; + bool mem_signed = children[0]->id2ast->is_signed; children[0]->id2ast->meminfo(mem_width, mem_size, addr_bits); AstNode *wire_addr = new AstNode(AST_WIRE, new AstNode(AST_RANGE, mkconst_int(addr_bits-1, true), mkconst_int(0, true))); @@ -2906,6 +2909,7 @@ bool AstNode::mem2reg_as_needed_pass2(pool<AstNode*> &mem2reg_set, AstNode *mod, AstNode *wire_data = new AstNode(AST_WIRE, new AstNode(AST_RANGE, mkconst_int(mem_width-1, true), mkconst_int(0, true))); wire_data->str = id_data; wire_data->is_reg = true; + wire_data->is_signed = mem_signed; wire_data->attributes["\\nosync"] = AstNode::mkconst_int(1, false); mod->children.push_back(wire_data); while (wire_data->simplify(true, false, false, 1, -1, false, false)) { } @@ -2967,6 +2971,7 @@ bool AstNode::mem2reg_as_needed_pass2(pool<AstNode*> &mem2reg_set, AstNode *mod, std::string id_addr = sstr.str() + "_ADDR", id_data = sstr.str() + "_DATA"; int mem_width, mem_size, addr_bits; + bool mem_signed = id2ast->is_signed; id2ast->meminfo(mem_width, mem_size, addr_bits); AstNode *wire_addr = new AstNode(AST_WIRE, new AstNode(AST_RANGE, mkconst_int(addr_bits-1, true), mkconst_int(0, true))); @@ -2980,6 +2985,7 @@ bool AstNode::mem2reg_as_needed_pass2(pool<AstNode*> &mem2reg_set, AstNode *mod, AstNode *wire_data = new AstNode(AST_WIRE, new AstNode(AST_RANGE, mkconst_int(mem_width-1, true), mkconst_int(0, true))); wire_data->str = id_data; wire_data->is_reg = true; + wire_data->is_signed = mem_signed; if (block) wire_data->attributes["\\nosync"] = AstNode::mkconst_int(1, false); mod->children.push_back(wire_data); diff --git a/frontends/blif/blifparse.cc b/frontends/blif/blifparse.cc index 3717a1e5..6d4d6087 100644 --- a/frontends/blif/blifparse.cc +++ b/frontends/blif/blifparse.cc @@ -23,6 +23,7 @@ YOSYS_NAMESPACE_BEGIN static bool read_next_line(char *&buffer, size_t &buffer_size, int &line_count, std::istream &f) { + string strbuf; int buffer_len = 0; buffer[0] = 0; @@ -42,8 +43,13 @@ static bool read_next_line(char *&buffer, size_t &buffer_size, int &line_count, if (buffer_len > 0 && buffer[buffer_len-1] == '\\') buffer[--buffer_len] = 0; line_count++; - if (!f.getline(buffer+buffer_len, buffer_size-buffer_len)) + if (!std::getline(f, strbuf)) return false; + while (buffer_size-buffer_len < strbuf.size()+1) { + buffer_size *= 2; + buffer = (char*)realloc(buffer, buffer_size); + } + strcpy(buffer+buffer_len, strbuf.c_str()); } else return true; } @@ -256,9 +262,13 @@ void parse_blif(RTLIL::Design *design, std::istream &f, std::string dff_name, bo cell = module->addDlatch(NEW_ID, blif_wire(clock), blif_wire(d), blif_wire(q), false); else { no_latch_clock: - cell = module->addCell(NEW_ID, dff_name); - cell->setPort("\\D", blif_wire(d)); - cell->setPort("\\Q", blif_wire(q)); + if (dff_name.empty()) { + cell = module->addFf(NEW_ID, blif_wire(d), blif_wire(q)); + } else { + cell = module->addCell(NEW_ID, dff_name); + cell->setPort("\\D", blif_wire(d)); + cell->setPort("\\Q", blif_wire(q)); + } } obj_attributes = &cell->attributes; @@ -477,7 +487,7 @@ struct BlifFrontend : public Frontend { } extra_args(f, filename, args, argidx); - parse_blif(design, *f, "\\DFF", true, sop_mode); + parse_blif(design, *f, "", true, sop_mode); } } BlifFrontend; diff --git a/frontends/ilang/ilang_lexer.l b/frontends/ilang/ilang_lexer.l index 415de74e..84238854 100644 --- a/frontends/ilang/ilang_lexer.l +++ b/frontends/ilang/ilang_lexer.l @@ -74,6 +74,7 @@ USING_YOSYS_NAMESPACE "negedge" { return TOK_NEGEDGE; } "edge" { return TOK_EDGE; } "always" { return TOK_ALWAYS; } +"global" { return TOK_GLOBAL; } "init" { return TOK_INIT; } "update" { return TOK_UPDATE; } "process" { return TOK_PROCESS; } diff --git a/frontends/ilang/ilang_parser.y b/frontends/ilang/ilang_parser.y index cc31c864..bfc062fe 100644 --- a/frontends/ilang/ilang_parser.y +++ b/frontends/ilang/ilang_parser.y @@ -57,7 +57,7 @@ USING_YOSYS_NAMESPACE %token <integer> TOK_INT %token TOK_AUTOIDX TOK_MODULE TOK_WIRE TOK_WIDTH TOK_INPUT TOK_OUTPUT TOK_INOUT %token TOK_CELL TOK_CONNECT TOK_SWITCH TOK_CASE TOK_ASSIGN TOK_SYNC -%token TOK_LOW TOK_HIGH TOK_POSEDGE TOK_NEGEDGE TOK_EDGE TOK_ALWAYS TOK_INIT +%token TOK_LOW TOK_HIGH TOK_POSEDGE TOK_NEGEDGE TOK_EDGE TOK_ALWAYS TOK_GLOBAL TOK_INIT %token TOK_UPDATE TOK_PROCESS TOK_END TOK_INVALID TOK_EOL TOK_OFFSET %token TOK_PARAMETER TOK_ATTRIBUTE TOK_MEMORY TOK_SIZE TOK_SIGNED TOK_UPTO @@ -112,7 +112,13 @@ module_body: /* empty */; module_stmt: - attr_stmt | wire_stmt | memory_stmt | cell_stmt | proc_stmt | conn_stmt; + param_stmt | attr_stmt | wire_stmt | memory_stmt | cell_stmt | proc_stmt | conn_stmt; + +param_stmt: + TOK_PARAMETER TOK_ID EOL { + current_module->avail_parameters.insert($2); + free($2); + }; attr_stmt: TOK_ATTRIBUTE TOK_ID constant EOL { @@ -301,6 +307,12 @@ sync_list: rule->signal = RTLIL::SigSpec(); current_process->syncs.push_back(rule); } update_list | + sync_list TOK_SYNC TOK_GLOBAL EOL { + RTLIL::SyncRule *rule = new RTLIL::SyncRule; + rule->type = RTLIL::SyncType::STg; + rule->signal = RTLIL::SigSpec(); + current_process->syncs.push_back(rule); + } update_list | sync_list TOK_SYNC TOK_INIT EOL { RTLIL::SyncRule *rule = new RTLIL::SyncRule; rule->type = RTLIL::SyncType::STi; diff --git a/frontends/liberty/liberty.cc b/frontends/liberty/liberty.cc index 73d927fa..4666c818 100644 --- a/frontends/liberty/liberty.cc +++ b/frontends/liberty/liberty.cc @@ -401,6 +401,47 @@ static void create_latch(RTLIL::Module *module, LibertyAst *node) cell->setPort("\\E", enable_sig); } +void parse_type_map(std::map<std::string, std::tuple<int, int, bool>> &type_map, LibertyAst *ast) +{ + for (auto type_node : ast->children) + { + if (type_node->id != "type" || type_node->args.size() != 1) + continue; + + std::string type_name = type_node->args.at(0); + int bit_width = -1, bit_from = -1, bit_to = -1; + bool upto = false; + + for (auto child : type_node->children) + { + if (child->id == "base_type" && child->value != "array") + goto next_type; + + if (child->id == "data_type" && child->value != "bit") + goto next_type; + + if (child->id == "bit_width") + bit_width = atoi(child->value.c_str()); + + if (child->id == "bit_from") + bit_from = atoi(child->value.c_str()); + + if (child->id == "bit_to") + bit_to = atoi(child->value.c_str()); + + if (child->id == "downto" && (child->value == "0" || child->value == "false" || child->value == "FALSE")) + upto = true; + } + + if (bit_width != (std::max(bit_from, bit_to) - std::min(bit_from, bit_to) + 1)) + log_error("Incompatible array type '%s': bit_width=%d, bit_from=%d, bit_to=%d.\n", + type_name.c_str(), bit_width, bit_from, bit_to); + + type_map[type_name] = std::tuple<int, int, bool>(bit_width, std::min(bit_from, bit_to), upto); + next_type:; + } +} + struct LibertyFrontend : public Frontend { LibertyFrontend() : Frontend("liberty", "read cells from liberty file") { } virtual void help() @@ -469,45 +510,8 @@ struct LibertyFrontend : public Frontend { LibertyParser parser(*f); int cell_count = 0; - std::map<std::string, std::tuple<int, int, bool>> type_map; - - for (auto type_node : parser.ast->children) - { - if (type_node->id != "type" || type_node->args.size() != 1) - continue; - - std::string type_name = type_node->args.at(0); - int bit_width = -1, bit_from = -1, bit_to = -1; - bool upto = false; - - for (auto child : type_node->children) - { - if (child->id == "base_type" && child->value != "array") - goto next_type; - - if (child->id == "data_type" && child->value != "bit") - goto next_type; - - if (child->id == "bit_width") - bit_width = atoi(child->value.c_str()); - - if (child->id == "bit_from") - bit_from = atoi(child->value.c_str()); - - if (child->id == "bit_to") - bit_to = atoi(child->value.c_str()); - - if (child->id == "downto" && (child->value == "0" || child->value == "false" || child->value == "FALSE")) - upto = true; - } - - if (bit_width != (std::max(bit_from, bit_to) - std::min(bit_from, bit_to) + 1)) - log_error("Incompatible array type '%s': bit_width=%d, bit_from=%d, bit_to=%d.\n", - type_name.c_str(), bit_width, bit_from, bit_to); - - type_map[type_name] = std::tuple<int, int, bool>(bit_width, std::min(bit_from, bit_to), upto); - next_type:; - } + std::map<std::string, std::tuple<int, int, bool>> global_type_map; + parse_type_map(global_type_map, parser.ast); for (auto cell : parser.ast->children) { @@ -524,6 +528,9 @@ struct LibertyFrontend : public Frontend { // log("Processing cell type %s.\n", RTLIL::unescape_id(cell_name).c_str()); + std::map<std::string, std::tuple<int, int, bool>> type_map = global_type_map; + parse_type_map(type_map, cell); + RTLIL::Module *module = new RTLIL::Module; module->name = cell_name; diff --git a/frontends/verilog/verilog_parser.y b/frontends/verilog/verilog_parser.y index c730ce5b..5bbda535 100644 --- a/frontends/verilog/verilog_parser.y +++ b/frontends/verilog/verilog_parser.y @@ -1229,7 +1229,7 @@ rvalue: $$ = new AstNode(AST_IDENTIFIER, $2); $$->str = *$1; delete $1; - if ($2 == nullptr && formal_mode && ($$->str == "\\$initstate" || $$->str == "\\$anyconst")) + if ($2 == nullptr && formal_mode && ($$->str == "\\$initstate" || $$->str == "\\$anyconst" || $$->str == "\\$anyseq")) $$->type = AST_FCALL; } | hierarchical_id non_opt_multirange { diff --git a/kernel/celltypes.h b/kernel/celltypes.h index 900c12d0..f0ead1e8 100644 --- a/kernel/celltypes.h +++ b/kernel/celltypes.h @@ -118,6 +118,7 @@ struct CellTypes setup_type("$assume", {A, EN}, pool<RTLIL::IdString>(), true); setup_type("$initstate", pool<RTLIL::IdString>(), {Y}, true); setup_type("$anyconst", pool<RTLIL::IdString>(), {Y}, true); + setup_type("$anyseq", pool<RTLIL::IdString>(), {Y}, true); setup_type("$equiv", {A, B}, {Y}, true); } @@ -130,6 +131,7 @@ struct CellTypes IdString CTRL_IN = "\\CTRL_IN", CTRL_OUT = "\\CTRL_OUT"; setup_type("$sr", {SET, CLR}, {Q}); + setup_type("$ff", {D}, {Q}); setup_type("$dff", {CLK, D}, {Q}); setup_type("$dffe", {CLK, EN, D}, {Q}); setup_type("$dffsr", {CLK, SET, CLR, D}, {Q}); @@ -184,6 +186,8 @@ struct CellTypes for (auto c2 : list_np) setup_type(stringf("$_SR_%c%c_", c1, c2), {S, R}, {Q}); + setup_type("$_FF_", {D}, {Q}); + for (auto c1 : list_np) setup_type(stringf("$_DFF_%c_", c1), {C, D}, {Q}); diff --git a/kernel/driver.cc b/kernel/driver.cc index 5cfc4171..f8d00c38 100644 --- a/kernel/driver.cc +++ b/kernel/driver.cc @@ -510,7 +510,9 @@ int main(int argc, char **argv) #endif log_flush(); -#ifdef _WIN32 +#if defined(_MSC_VER) + _exit(0); +#elif defined(_WIN32) _Exit(0); #endif diff --git a/kernel/log.cc b/kernel/log.cc index 3f1d8881..abc401f5 100644 --- a/kernel/log.cc +++ b/kernel/log.cc @@ -207,6 +207,8 @@ void logv_error(const char *format, va_list ap) #ifdef EMSCRIPTEN log_files = backup_log_files; throw 0; +#elif defined(_MSC_VER) + _exit(1); #else _Exit(1); #endif diff --git a/kernel/rtlil.cc b/kernel/rtlil.cc index 32efe4f0..66bbf042 100644 --- a/kernel/rtlil.cc +++ b/kernel/rtlil.cc @@ -866,6 +866,13 @@ namespace { return; } + if (cell->type == "$ff") { + port("\\D", param("\\WIDTH")); + port("\\Q", param("\\WIDTH")); + check_expected(); + return; + } + if (cell->type == "$dff") { param_bool("\\CLK_POLARITY"); port("\\CLK", 1); @@ -1030,7 +1037,7 @@ namespace { return; } - if (cell->type == "$anyconst") { + if (cell->type.in("$anyconst", "$anyseq")) { port("\\Y", param("\\WIDTH")); check_expected(); return; @@ -1069,6 +1076,7 @@ namespace { if (cell->type == "$_SR_PN_") { check_gate("SRQ"); return; } if (cell->type == "$_SR_PP_") { check_gate("SRQ"); return; } + if (cell->type == "$_FF_") { check_gate("DQ"); return; } if (cell->type == "$_DFF_N_") { check_gate("DQC"); return; } if (cell->type == "$_DFF_P_") { check_gate("DQC"); return; } @@ -1830,6 +1838,15 @@ RTLIL::Cell* RTLIL::Module::addSr(RTLIL::IdString name, RTLIL::SigSpec sig_set, return cell; } +RTLIL::Cell* RTLIL::Module::addFf(RTLIL::IdString name, RTLIL::SigSpec sig_d, RTLIL::SigSpec sig_q) +{ + RTLIL::Cell *cell = addCell(name, "$ff"); + cell->parameters["\\WIDTH"] = sig_q.size(); + cell->setPort("\\D", sig_d); + cell->setPort("\\Q", sig_q); + return cell; +} + RTLIL::Cell* RTLIL::Module::addDff(RTLIL::IdString name, RTLIL::SigSpec sig_clk, RTLIL::SigSpec sig_d, RTLIL::SigSpec sig_q, bool clk_polarity) { RTLIL::Cell *cell = addCell(name, "$dff"); @@ -1912,6 +1929,14 @@ RTLIL::Cell* RTLIL::Module::addDlatchsr(RTLIL::IdString name, RTLIL::SigSpec sig return cell; } +RTLIL::Cell* RTLIL::Module::addFfGate(RTLIL::IdString name, RTLIL::SigSpec sig_d, RTLIL::SigSpec sig_q) +{ + RTLIL::Cell *cell = addCell(name, "$_FF_"); + cell->setPort("\\D", sig_d); + cell->setPort("\\Q", sig_q); + return cell; +} + RTLIL::Cell* RTLIL::Module::addDffGate(RTLIL::IdString name, RTLIL::SigSpec sig_clk, RTLIL::SigSpec sig_d, RTLIL::SigSpec sig_q, bool clk_polarity) { RTLIL::Cell *cell = addCell(name, stringf("$_DFF_%c_", clk_polarity ? 'P' : 'N')); @@ -1984,6 +2009,15 @@ RTLIL::SigSpec RTLIL::Module::Anyconst(RTLIL::IdString name, int width) return sig; } +RTLIL::SigSpec RTLIL::Module::Anyseq(RTLIL::IdString name, int width) +{ + RTLIL::SigSpec sig = addWire(NEW_ID, width); + Cell *cell = addCell(name, "$anyseq"); + cell->setParam("\\WIDTH", width); + cell->setPort("\\Y", sig); + return sig; +} + RTLIL::SigSpec RTLIL::Module::Initstate(RTLIL::IdString name) { RTLIL::SigSpec sig = addWire(NEW_ID); diff --git a/kernel/rtlil.h b/kernel/rtlil.h index a426e0bd..9430dcb3 100644 --- a/kernel/rtlil.h +++ b/kernel/rtlil.h @@ -42,7 +42,8 @@ namespace RTLIL STn = 3, // edge sensitive: negedge STe = 4, // edge sensitive: both edges STa = 5, // always active - STi = 6 // init + STg = 6, // global clock + STi = 7 // init }; enum ConstFlags : unsigned char { @@ -1008,6 +1009,7 @@ public: RTLIL::Cell* addEquiv (RTLIL::IdString name, RTLIL::SigSpec sig_a, RTLIL::SigSpec sig_b, RTLIL::SigSpec sig_y); RTLIL::Cell* addSr (RTLIL::IdString name, RTLIL::SigSpec sig_set, RTLIL::SigSpec sig_clr, RTLIL::SigSpec sig_q, bool set_polarity = true, bool clr_polarity = true); + RTLIL::Cell* addFf (RTLIL::IdString name, RTLIL::SigSpec sig_d, RTLIL::SigSpec sig_q); RTLIL::Cell* addDff (RTLIL::IdString name, RTLIL::SigSpec sig_clk, RTLIL::SigSpec sig_d, RTLIL::SigSpec sig_q, bool clk_polarity = true); RTLIL::Cell* addDffe (RTLIL::IdString name, RTLIL::SigSpec sig_clk, RTLIL::SigSpec sig_en, RTLIL::SigSpec sig_d, RTLIL::SigSpec sig_q, bool clk_polarity = true, bool en_polarity = true); RTLIL::Cell* addDffsr (RTLIL::IdString name, RTLIL::SigSpec sig_clk, RTLIL::SigSpec sig_set, RTLIL::SigSpec sig_clr, @@ -1032,6 +1034,7 @@ public: RTLIL::Cell* addAoi4Gate (RTLIL::IdString name, RTLIL::SigBit sig_a, RTLIL::SigBit sig_b, RTLIL::SigBit sig_c, RTLIL::SigBit sig_d, RTLIL::SigBit sig_y); RTLIL::Cell* addOai4Gate (RTLIL::IdString name, RTLIL::SigBit sig_a, RTLIL::SigBit sig_b, RTLIL::SigBit sig_c, RTLIL::SigBit sig_d, RTLIL::SigBit sig_y); + RTLIL::Cell* addFfGate (RTLIL::IdString name, RTLIL::SigSpec sig_d, RTLIL::SigSpec sig_q); RTLIL::Cell* addDffGate (RTLIL::IdString name, RTLIL::SigSpec sig_clk, RTLIL::SigSpec sig_d, RTLIL::SigSpec sig_q, bool clk_polarity = true); RTLIL::Cell* addDffeGate (RTLIL::IdString name, RTLIL::SigSpec sig_clk, RTLIL::SigSpec sig_en, RTLIL::SigSpec sig_d, RTLIL::SigSpec sig_q, bool clk_polarity = true, bool en_polarity = true); RTLIL::Cell* addDffsrGate (RTLIL::IdString name, RTLIL::SigSpec sig_clk, RTLIL::SigSpec sig_set, RTLIL::SigSpec sig_clr, @@ -1105,6 +1108,7 @@ public: RTLIL::SigBit Oai4Gate (RTLIL::IdString name, RTLIL::SigBit sig_a, RTLIL::SigBit sig_b, RTLIL::SigBit sig_c, RTLIL::SigBit sig_d); RTLIL::SigSpec Anyconst (RTLIL::IdString name, int width = 1); + RTLIL::SigSpec Anyseq (RTLIL::IdString name, int width = 1); RTLIL::SigSpec Initstate (RTLIL::IdString name); }; diff --git a/kernel/satgen.h b/kernel/satgen.h index 0a65b490..690f8e33 100644 --- a/kernel/satgen.h +++ b/kernel/satgen.h @@ -1293,7 +1293,7 @@ struct SatGen return true; } - if (timestep > 0 && (cell->type == "$dff" || cell->type == "$_DFF_N_" || cell->type == "$_DFF_P_")) + if (timestep > 0 && cell->type.in("$ff", "$dff", "$_FF_", "$_DFF_N_", "$_DFF_P_")) { if (timestep == 1) { @@ -1332,8 +1332,8 @@ struct SatGen if (model_undef) { - std::vector<int> undef_d = importUndefSigSpec(cell->getPort("\\D"), timestep-1); - std::vector<int> undef_q = importUndefSigSpec(cell->getPort("\\Q"), timestep); + std::vector<int> undef_d = importUndefSigSpec(cell->getPort("\\Y"), timestep-1); + std::vector<int> undef_q = importUndefSigSpec(cell->getPort("\\Y"), timestep); ez->assume(ez->vec_eq(undef_d, undef_q)); undefGating(q, qq, undef_q); @@ -1341,6 +1341,11 @@ struct SatGen return true; } + if (cell->type == "$anyseq") + { + return true; + } + if (cell->type == "$_BUF_" || cell->type == "$equiv") { std::vector<int> a = importDefSigSpec(cell->getPort("\\A"), timestep); diff --git a/kernel/yosys.h b/kernel/yosys.h index aab6b584..ae73146b 100644 --- a/kernel/yosys.h +++ b/kernel/yosys.h @@ -64,6 +64,7 @@ #include <string.h> #include <stdint.h> #include <stdio.h> +#include <limits.h> #ifndef _YOSYS_ # error It looks like you are trying to build Yosys without the config defines set. \ @@ -100,6 +101,10 @@ # endif #endif +#ifndef PATH_MAX +# define PATH_MAX 4096 +#endif + #define PRIVATE_NAMESPACE_BEGIN namespace { #define PRIVATE_NAMESPACE_END } #define YOSYS_NAMESPACE_BEGIN namespace Yosys { diff --git a/manual/CHAPTER_CellLib.tex b/manual/CHAPTER_CellLib.tex index bd73ae23..a831fdf3 100644 --- a/manual/CHAPTER_CellLib.tex +++ b/manual/CHAPTER_CellLib.tex @@ -421,7 +421,7 @@ pass. The combinatorial logic cells can be mapped to physical cells from a Liber using the {\tt abc} pass. \begin{fixme} -Add information about {\tt \$assert}, {\tt \$assume}, {\tt \$equiv}, {\tt \$initstate}, and {\tt \$anyconst} cells. +Add information about {\tt \$assert}, {\tt \$assume}, {\tt \$equiv}, {\tt \$initstate}, {\tt \$anyconst}, and {\tt \$anyseq} cells. \end{fixme} \begin{fixme} @@ -437,6 +437,10 @@ Add information about {\tt \$alu}, {\tt \$macc}, {\tt \$fa}, and {\tt \$lcu} cel \end{fixme} \begin{fixme} +Add information about {\tt \$ff} and {\tt \$\_FF\_} cells. +\end{fixme} + +\begin{fixme} Add information about {\tt \$dffe}, {\tt \$dffsr}, {\tt \$dlatch}, and {\tt \$dlatchsr} cells. \end{fixme} diff --git a/manual/command-reference-manual.tex b/manual/command-reference-manual.tex index 425d89b6..8af8ccdd 100644 --- a/manual/command-reference-manual.tex +++ b/manual/command-reference-manual.tex @@ -9,7 +9,7 @@ This pass uses the ABC tool [1] for technology mapping of yosys's internal gate library to a target architecture. -exe <command> - use the specified command name instead of "yosys-abc" to execute ABC. + use the specified command instead of "<yosys-bindir>/yosys-abc" to execute ABC. This can e.g. be used to call a specific version of ABC or a wrapper. -script <file> @@ -23,33 +23,45 @@ library to a target architecture. if no -script parameter is given, the following scripts are used: for -liberty without -constr: - strash; scorr; ifraig; retime {D}; strash; dch -f; map {D} + strash; dc2; scorr; ifraig; retime -o {D}; strash; dch -f; + map {D} for -liberty with -constr: - strash; scorr; ifraig; retime {D}; strash; dch -f; map {D}; - buffer; upsize {D}; dnsize {D}; stime -p + strash; dc2; scorr; ifraig; retime -o {D}; strash; dch -f; + map {D}; buffer; upsize {D}; dnsize {D}; stime -p - for -lut: - strash; scorr; ifraig; retime; strash; dch -f; if + for -lut/-luts (only one LUT size): + strash; dc2; scorr; ifraig; retime -o; strash; dch -f; if; mfs; + lutpack + + for -lut/-luts (different LUT sizes): + strash; dc2; scorr; ifraig; retime -o; strash; dch -f; if; mfs + + for -sop: + strash; dc2; scorr; ifraig; retime -o; strash; dch -f; + cover {I} {P} otherwise: - strash; scorr; ifraig; retime; strash; dch -f; map + strash; dc2; scorr; ifraig; retime -o; strash; dch -f; map -fast use different default scripts that are slightly faster (at the cost of output quality): for -liberty without -constr: - retime {D}; map {D} + retime -o {D}; map {D} for -liberty with -constr: - retime {D}; map {D}; buffer; upsize {D}; dnsize {D}; stime -p + retime -o {D}; map {D}; buffer; upsize {D}; dnsize {D}; stime -p - for -lut: - retime; if + for -lut/-luts: + retime -o; if + + for -sop: + retime -o; cover -I {I} -P {P} otherwise: - retime; map + retime -o; map -liberty <file> generate netlists for the specified cell library (using the liberty @@ -70,6 +82,14 @@ library to a target architecture. set delay target. the string {D} in the default scripts above is replaced by this option when used, and an empty string otherwise. + -I <num> + maximum number of SOP inputs. + (replaces {I} in the default scripts above) + + -P <num> + maximum number of SOP products. + (replaces {P} in the default scripts above) + -lut <width> generate netlist using luts of (max) the specified width. @@ -83,6 +103,9 @@ library to a target architecture. generate netlist using luts. Use the specified costs for luts with 1, 2, 3, .. inputs. + -sop + map to sum-of-product cells and inverters + -g type1,type2,... Map the the specified list of gate types. Supported gates types are: AND, NAND, OR, NOR, XOR, XNOR, MUX, AOI3, OAI3, AOI4, OAI4. @@ -166,6 +189,85 @@ This pass translates arithmetic operations like $add, $mul, $lt, etc. to $alu and $macc cells. \end{lstlisting} +\section{assertpmux -- convert internal signals to module ports} +\label{cmd:assertpmux} +\begin{lstlisting}[numbers=left,frame=single] + assertpmux [options] [selection] + +This command adds asserts to the design that assert that all parallel muxes +($pmux cells) have a maximum of one of their inputs enable at any time. + + -noinit + do not enforce the pmux condition during the init state + + -always + usually the $pmux condition is only checked when the $pmux output + is used be the mux tree it drives. this option will deactivate this + additional constrained and check the $pmux condition always. +\end{lstlisting} + +\section{attrmap -- renaming attributes} +\label{cmd:attrmap} +\begin{lstlisting}[numbers=left,frame=single] + attrmap [options] [selection] + +This command renames attributes and/or mapps key/value pairs to +other key/value pairs. + + -tocase <name> + Match attribute names case-insensitively and set it to the specified + name. + + -rename <old_name> <new_name> + Rename attributes as specified + + -map <old_name>=<old_value> <new_name>=<new_value> + Map key/value pairs as indicated. + + -imap <old_name>=<old_value> <new_name>=<new_value> + Like -map, but use case-insensitive match for <old_value> when + it is a string value. + + -remove <name>=<value> + Remove attributes matching this pattern. + + -modattr + Operate on module attributes instead of attributes on wires and cells. + +For example, mapping Xilinx-style "keep" attributes to Yosys-style: + + attrmap -tocase keep -imap keep="true" keep=1 \ + -imap keep="false" keep=0 -remove keep=0 +\end{lstlisting} + +\section{attrmvcp -- move or copy attributes from wires to driving cells} +\label{cmd:attrmvcp} +\begin{lstlisting}[numbers=left,frame=single] + attrmvcp [options] [selection] + +Move or copy attributes on wires to the cells driving them. + + -copy + By default, attributes are moved. This will only add + the attribute to the cell, without removing it from + the wire. + + -purge + If no selected cell consumes the attribute, then it is + left on the wire by default. This option will cause the + attribute to be removed from the wire, even if no selected + cell takes it. + + -driven + By default, attriburtes are moved to the cell driving the + wire. With this option set it will be moved to the cell + driven by the wire instead. + + -attr <attrname> + Move or copy this attribute. This option can be used + multiple times. +\end{lstlisting} + \section{cd -- a shortcut for 'select -module <name>'} \label{cmd:cd} \begin{lstlisting}[numbers=left,frame=single] @@ -233,6 +335,16 @@ When commands are separated using the ';;;' token, this command will be executed in -purge mode between the commands. \end{lstlisting} +\section{clk2fflogic -- convert clocked FFs to generic \$ff cells} +\label{cmd:clk2fflogic} +\begin{lstlisting}[numbers=left,frame=single] + clk2fflogic [options] [selection] + +This command replaces clocked flip-flops with generic $ff cells that use the +implicit global clock. This is useful for formal verification of designs with +multiple clocks. +\end{lstlisting} + \section{connect -- create or remove connections} \label{cmd:connect} \begin{lstlisting}[numbers=left,frame=single] @@ -356,6 +468,14 @@ Does not delete any object but removes the input and/or output flag on the selected wires, thus 'deleting' module ports. \end{lstlisting} +\section{deminout -- demote inout ports to input or output} +\label{cmd:deminout} +\begin{lstlisting}[numbers=left,frame=single] + deminout [options] [selection] + +"Demote" inout ports to input or output ports, if possible. +\end{lstlisting} + \section{design -- save, restore and reset current design} \label{cmd:design} \begin{lstlisting}[numbers=left,frame=single] @@ -910,6 +1030,9 @@ Options: -expand, -norecode, -export, -nomap enable or disable passes as indicated above + -fullexpand + call expand with -full option + -encoding type -fm_set_fsm_file file -encfile file @@ -934,11 +1057,14 @@ Signals can be protected from being detected by this pass by setting the \section{fsm\_expand -- expand FSM cells by merging logic into it} \label{cmd:fsm_expand} \begin{lstlisting}[numbers=left,frame=single] - fsm_expand [selection] + fsm_expand [-full] [selection] The fsm_extract pass is conservative about the cells that belong to a finite state machine. This pass can be used to merge additional auxiliary gates into the finite state machine. + +By default, fsm_expand is still a bit conservative regarding merging larger +word-wide cells. Call with -full to consider all cells for merging. \end{lstlisting} \section{fsm\_export -- exporting FSMs to KISS2 files} @@ -1029,6 +1155,23 @@ one-hot encoding and binary encoding is supported. .map <old_bitpattern> <new_bitpattern> \end{lstlisting} +\section{greenpak4\_counters -- Extract GreenPak4 counter cells} +\label{cmd:greenpak4_counters} +\begin{lstlisting}[numbers=left,frame=single] + greenpak4_counters [options] [selection] + +This pass converts non-resettable or async resettable down counters to GreenPak4 +counter cells (All other GreenPak4 counter modes must be instantiated manually.) +\end{lstlisting} + +\section{greenpak4\_dffinv -- merge greenpak4 inverters and DFFs} +\label{cmd:greenpak4_dffinv} +\begin{lstlisting}[numbers=left,frame=single] + greenpak4_dffinv [options] [selection] + +Merge GP_INV cells with GP_DFF* cells. +\end{lstlisting} + \section{help -- display help messages} \label{cmd:help} \begin{lstlisting}[numbers=left,frame=single] @@ -1157,11 +1300,26 @@ This command executes the following script: do <ice40 specific optimizations> - opt_const -mux_undef -undriven [-full] - opt_share + opt_expr -mux_undef -undriven [-full] + opt_merge opt_rmdff opt_clean while <changed design> + +When called with the option -unlut, this command will transform all already +mapped SB_LUT4 cells back to logic. +\end{lstlisting} + +\section{insbuf -- insert buffer cells for connected wires} +\label{cmd:insbuf} +\begin{lstlisting}[numbers=left,frame=single] + insbuf [options] [selection] + +Insert buffer cells into the design for directly connected wires. + + -buf <celltype> <in-portname> <out-portname> + Use the given cell type instead of $_BUF_. (Notice that the next + call to "clean" will remove all $_BUF_ in the design.) \end{lstlisting} \section{iopadmap -- technology mapping of i/o pads (or buffers)} @@ -1177,12 +1335,23 @@ the resulting cells to more sophisticated PAD cells. Map module input ports to the given cell type with the given output port name. if a 2nd portname is given, the signal is passed through the pad call, using the 2nd - portname as input. + portname as the port facing the module port. -outpad <celltype> <portname>[:<portname>] -inoutpad <celltype> <portname>[:<portname>] Similar to -inpad, but for output and inout ports. + -toutpad <celltype> <portname>:<portname>[:<portname>] + Merges $_TBUF_ cells into the output pad cell. This takes precedence + over the other -outpad cell. The first portname is the enable input + of the tristate driver. + + -tinoutpad <celltype> <portname>:<portname>:<portname>[:<portname>] + Merges $_TBUF_ cells into the inout pad cell. This takes precedence + over the other -inoutpad cell. The first portname is the enable input + of the tristate driver and the 2nd portname is the internal output + buffering the external signal. + -widthparam <param_name> Use the specified parameter name to set the port width. @@ -1193,6 +1362,8 @@ the resulting cells to more sophisticated PAD cells. create individual bit-wide buffers even for ports that are wider. (the default behavior is to create word-wide buffers using -widthparam to set the word size on the cell.) + +Tristate PADS (-toutpad, -tinoutpad) always operate in -bits mode. \end{lstlisting} \section{json -- write design in JSON format} @@ -1265,14 +1436,15 @@ is used then the $macc cell is mapped to $add, $sub, etc. cells instead. \section{memory -- translate memories to basic cells} \label{cmd:memory} \begin{lstlisting}[numbers=left,frame=single] - memory [-nomap] [-nordff] [-bram <bram_rules>] [selection] + memory [-nomap] [-nordff] [-memx] [-bram <bram_rules>] [selection] This pass calls all the other memory_* passes in a useful order: - memory_dff [-nordff] + memory_dff [-nordff] (-memx implies -nordff) opt_clean memory_share opt_clean + memory_memx (when called with -memx) memory_collect memory_bram -rules <bram_rules> (when called with -bram) memory_map (skipped if called with -nomap) @@ -1401,6 +1573,15 @@ This pass converts multiport memory cells as generated by the memory_collect pass to word-wide DFFs and address decoders. \end{lstlisting} +\section{memory\_memx -- emulate vlog sim behavior for mem ports} +\label{cmd:memory_memx} +\begin{lstlisting}[numbers=left,frame=single] + memory_memx [selection] + +This pass adds additional circuitry that emulates the Verilog simulation +behavior for out-of-bounds memory reads and writes. +\end{lstlisting} + \section{memory\_share -- consolidate memory ports} \label{cmd:memory_share} \begin{lstlisting}[numbers=left,frame=single] @@ -1423,7 +1604,7 @@ The following methods are used to consolidate the number of memory ports: Note that in addition to the algorithms implemented in this pass, the $memrd and $memwr cells are also subject to generic resource sharing passes (and other -optimizations) such as opt_share. +optimizations) such as "share" and "opt_merge". \end{lstlisting} \section{memory\_unpack -- unpack multi-port memory cells} @@ -1461,7 +1642,7 @@ detected. also create an 'assert' cell that checks if trigger is always low. -flatten - call 'flatten; opt_const -keepdc -undriven;;' on the miter circuit. + call 'flatten; opt_expr -keepdc -undriven;;' on the miter circuit. miter -assert [options] module [miter_name] @@ -1475,7 +1656,7 @@ module is modified. keep module output ports. -flatten - call 'flatten; opt_const -keepdc -undriven;;' on the miter circuit. + call 'flatten; opt_expr -keepdc -undriven;;' on the miter circuit. \end{lstlisting} \section{muxcover -- cover trees of MUX cells with wider MUXes} @@ -1507,6 +1688,9 @@ provides a small number of differently sized LUTs. The number of LUTs with 1, 2, 3, ... inputs that are available in the target architecture. + -assert + Create an error if not all logic can be mapped + Excess logic that does not fit into the specified LUTs is mapped back to generic logic gates ($_AND_, etc.). \end{lstlisting} @@ -1520,24 +1704,24 @@ This pass calls all the other opt_* passes in a useful order. This performs a series of trivial optimizations and cleanups. This pass executes the other passes in the following order: - opt_const [-mux_undef] [-mux_bool] [-undriven] [-clkinv] [-fine] [-full] [-keepdc] - opt_share [-share_all] -nomux + opt_expr [-mux_undef] [-mux_bool] [-undriven] [-clkinv] [-fine] [-full] [-keepdc] + opt_merge [-share_all] -nomux do opt_muxtree opt_reduce [-fine] [-full] - opt_share [-share_all] - opt_rmdff + opt_merge [-share_all] + opt_rmdff [-keepdc] opt_clean [-purge] - opt_const [-mux_undef] [-mux_bool] [-undriven] [-clkinv] [-fine] [-full] [-keepdc] + opt_expr [-mux_undef] [-mux_bool] [-undriven] [-clkinv] [-fine] [-full] [-keepdc] while <changed design> When called with -fast the following script is used instead: do - opt_const [-mux_undef] [-mux_bool] [-undriven] [-clkinv] [-fine] [-full] [-keepdc] - opt_share [-share_all] - opt_rmdff + opt_expr [-mux_undef] [-mux_bool] [-undriven] [-clkinv] [-fine] [-full] [-keepdc] + opt_merge [-share_all] + opt_rmdff [-keepdc] opt_clean [-purge] while <changed design in opt_rmdff> @@ -1561,12 +1745,13 @@ This pass only operates on completely selected modules without processes. also remove internal nets if they have a public name \end{lstlisting} -\section{opt\_const -- perform const folding} -\label{cmd:opt_const} +\section{opt\_expr -- perform const folding and simple expression rewriting} +\label{cmd:opt_expr} \begin{lstlisting}[numbers=left,frame=single] - opt_const [options] [selection] + opt_expr [options] [selection] This pass performs const folding on internal cell types with constant inputs. +It also performs some simple expression rewritring. -mux_undef remove 'undef' inputs from $mux, $pmux and $_MUX_ cells @@ -1593,6 +1778,21 @@ This pass performs const folding on internal cell types with constant inputs. replaced by 'a'. the -keepdc option disables all such optimizations. \end{lstlisting} +\section{opt\_merge -- consolidate identical cells} +\label{cmd:opt_merge} +\begin{lstlisting}[numbers=left,frame=single] + opt_merge [options] [selection] + +This pass identifies cells with identical type and input signals. Such cells +are then merged to one cell. + + -nomux + Do not merge MUX cells. + + -share_all + Operate on all cell types, not just built-in types. +\end{lstlisting} + \section{opt\_muxtree -- eliminate dead trees in multiplexer trees} \label{cmd:opt_muxtree} \begin{lstlisting}[numbers=left,frame=single] @@ -1628,27 +1828,12 @@ input with the original control signals OR'ed together. \section{opt\_rmdff -- remove DFFs with constant inputs} \label{cmd:opt_rmdff} \begin{lstlisting}[numbers=left,frame=single] - opt_rmdff [selection] + opt_rmdff [-keepdc] [selection] This pass identifies flip-flops with constant inputs and replaces them with a constant driver. \end{lstlisting} -\section{opt\_share -- consolidate identical cells} -\label{cmd:opt_share} -\begin{lstlisting}[numbers=left,frame=single] - opt_share [options] [selection] - -This pass identifies cells with identical type and input signals. Such cells -are then merged to one cell. - - -nomux - Do not merge MUX cells. - - -share_all - Operate on all cell types, not just built-in types. -\end{lstlisting} - \section{plugin -- load and list loaded plugins} \label{cmd:plugin} \begin{lstlisting}[numbers=left,frame=single] @@ -1686,9 +1871,30 @@ on partly selected designs. -top <module> use the specified module as top module (default='top') + -auto-top + automatically determine the top of the design hierarchy + + -flatten + flatten the design before synthesis. this will pass '-auto-top' to + 'hierarchy' if no top module is specified. + + -ifx + passed to 'proc'. uses verilog simulation behavior for verilog if/case + undef handling. this also prevents 'wreduce' from being run. + + -memx + simulate verilog simulation behavior for out-of-bounds memory accesses + using the 'memory_memx' pass. This option implies -nordff. + + -nomem + do not run any of the memory_* passes + -nordff passed to 'memory_dff'. prohibits merging of FFs into memory read ports + -nokeepdc + do not call opt_* with -keepdc + -run <from_label>[:<to_label>] only run the commands between the labels (see below). an empty from label is synonymous to 'begin', and empty to label is @@ -1698,16 +1904,18 @@ on partly selected designs. The following commands are executed by this synthesis command: begin: - hierarchy -check [-top <top>] + hierarchy -check [-top <top> | -auto-top] - prep: - proc - opt_const + coarse: + proc [-ifx] + flatten (if -flatten) + opt_expr -keepdc opt_clean check opt -keepdc - wreduce + wreduce [-memx] memory_dff [-nordff] + memory_memx (if -memx) opt_clean memory_collect opt -keepdc -fast @@ -1740,6 +1948,10 @@ The following options are supported: -global_arst [!]<netname> This option is passed through to proc_arst. + + -ifx + This option is passed through to proc_mux. proc_rmdead is not + executed in -ifx mode. \end{lstlisting} \section{proc\_arst -- detect asynchronous resets} @@ -1799,10 +2011,14 @@ respective wire. \section{proc\_mux -- convert decision trees to multiplexers} \label{cmd:proc_mux} \begin{lstlisting}[numbers=left,frame=single] - proc_mux [selection] + proc_mux [options] [selection] This pass converts the decision trees in processes (originating from if-else and case statements) to trees of multiplexer cells. + + -ifx + Use Verilog simulation behavior with respect to undef values in + 'case' expressions and 'if' conditions. \end{lstlisting} \section{proc\_rmdead -- eliminate dead trees in decision trees} @@ -1835,6 +2051,9 @@ annotates the cells in the design with 'qwp_position' attributes. -dump <html_file_name> Dump a protocol of the placement algorithm to the html file. + -v + Verbose solver output for profiling or debugging + Note: This implementation of a quadratic wirelength placer uses exact dense matrix operations. It is only a toy-placer for small circuits. \end{lstlisting} @@ -1845,6 +2064,9 @@ dense matrix operations. It is only a toy-placer for small circuits. read_blif [filename] Load modules from a BLIF file into the current design. + + -sop + Create $sop cells instead of $lut cells \end{lstlisting} \section{read\_ilang -- read modules from ilang file} @@ -1894,9 +2116,15 @@ Verilog-2005 is supported. of SystemVerilog is supported) -formal - enable support for assert() and assume() from SystemVerilog + enable support for SystemVerilog assertions and some Yosys extensions replace the implicit -D SYNTHESIS with -D FORMAL + -norestrict + ignore restrict() assertions + + -assume-asserts + treat all assert() statements like assume() statements + -dump_ast1 dump abstract syntax tree (before simplification) @@ -1906,6 +2134,9 @@ Verilog-2005 is supported. -dump_vlog dump ast as Verilog code (after simplification) + -dump_rtlil + dump generated RTLIL netlist + -yydebug enable parser debug output @@ -1989,6 +2220,9 @@ Note that the Verilog frontend does a pretty good job of processing valid verilog input, but has not very good error reporting. It generally is recommended to use a simulator (for example Icarus Verilog) for checking the syntax of the code, rather than to rely on read_verilog for that. + +See the Yosys README file for a list of non-standard Verilog features +supported by the Yosys Verilog front-end. \end{lstlisting} \section{rename -- rename object in the design} @@ -2254,7 +2488,7 @@ marked with that label (until the next label) is executed. \label{cmd:select} \begin{lstlisting}[numbers=left,frame=single] select [ -add | -del | -set <name> ] {-read <filename> | <selection>} - select [ -assert-none | -assert-any ] {-read <filename> | <selection>} + select [ <assert_option> ] {-read <filename> | <selection>} select [ -list | -write <filename> | -count | -clear ] select -module <modname> @@ -2290,6 +2524,14 @@ described here. do not modify the current selection. instead assert that the given selection contains exactly N objects. + -assert-max N + do not modify the current selection. instead assert that the given + selection contains less than or exactly N objects. + + -assert-min N + do not modify the current selection. instead assert that the given + selection contains at least N objects. + -list list all objects in the current selection @@ -2473,10 +2715,12 @@ instead of objects within modules. \section{setparam -- set/unset parameters on objects} \label{cmd:setparam} \begin{lstlisting}[numbers=left,frame=single] - setparam [ -set name value | -unset name ]... [selection] + setparam [ -type cell_type ] [ -set name value | -unset name ]... [selection] Set/unset the given parameters on the selected cells. String values must be passed in double quotes ("). + +The -type option can be used to change the cell type of the selected cells. \end{lstlisting} \section{setundef -- replace undef values with defined constants} @@ -2498,6 +2742,9 @@ This command replaced undef (x) constants with defined (0/1) constants. -random <seed> replace with random bits using the specified integer als seed value for the random number generator. + + -init + also create/update init values for flip-flops \end{lstlisting} \section{share -- perform sat-based resource sharing} @@ -2576,8 +2823,9 @@ to a graphics file (usually SVG or PostScript). Run the specified command with the graphics file as parameter. -format <format> - Generate a graphics file in the specified format. - Usually <format> is 'svg' or 'ps'. + Generate a graphics file in the specified format. Use 'dot' to just + generate a .dot file, or other <format> strings such as 'svg' or 'ps' + to generate files in other formats (this calls the 'dot' command). -lib <verilog_or_ilang_file> Use the specified library file for determining whether cell ports are @@ -2640,7 +2888,65 @@ The generated output files are '~/.yosys_show.dot' and '~/.yosys_show.<format>', unless another prefix is specified using -prefix <prefix>. Yosys on Windows and YosysJS use different defaults: The output is written -to 'show.dot' in the current directory and new viewer is launched. +to 'show.dot' in the current directory and new viewer is launched each time +the 'show' command is executed. +\end{lstlisting} + +\section{shregmap -- map shift registers} +\label{cmd:shregmap} +\begin{lstlisting}[numbers=left,frame=single] + shregmap [options] [selection] + +This pass converts chains of $_DFF_[NP]_ gates to target specific shift register +primitives. The generated shift register will be of type $__SHREG_DFF_[NP]_ and +will use the same interface as the original $_DFF_*_ cells. The cell parameter +'DEPTH' will contain the depth of the shift register. Use a target-specific +'techmap' map file to convert those cells to the actual target cells. + + -minlen N + minimum length of shift register (default = 2) + (this is the length after -keep_before and -keep_after) + + -maxlen N + maximum length of shift register (default = no limit) + larger chains will be mapped to multiple shift register instances + + -keep_before N + number of DFFs to keep before the shift register (default = 0) + + -keep_after N + number of DFFs to keep after the shift register (default = 0) + + -clkpol pos|neg|any + limit match to only positive or negative edge clocks. (default = any) + + -enpol pos|neg|none|any_or_none|any + limit match to FFs with the specified enable polarity. (default = none) + + -match <cell_type>[:<d_port_name>:<q_port_name>] + match the specified cells instead of $_DFF_N_ and $_DFF_P_. If + ':<d_port_name>:<q_port_name>' is omitted then 'D' and 'Q' is used + by default. E.g. the option '-clkpol pos' is just an alias for + '-match $_DFF_P_', which is an alias for '-match $_DFF_P_:D:Q'. + + -params + instead of encoding the clock and enable polarity in the cell name by + deriving from the original cell name, simply name all generated cells + $__SHREG_ and use CLKPOL and ENPOL parameters. An ENPOL value of 2 is + used to denote cells without enable input. The ENPOL parameter is + omitted when '-enpol none' (or no -enpol option) is passed. + + -zinit + assume the shift register is automatically zero-initialized, so it + becomes legal to merge zero initialized FFs into the shift register. + + -init + map initialized registers to the shift reg, add an INIT parameter to + generated cells with the initialization value. (first bit to shift out + in LSB position) + + -tech greenpak4 + map to greenpak4 shift registers. \end{lstlisting} \section{simplemap -- mapping simple coarse-grain cells} @@ -2654,7 +2960,7 @@ primitives. The following internal cell types are mapped by this pass: $not, $pos, $and, $or, $xor, $xnor $reduce_and, $reduce_or, $reduce_xor, $reduce_xnor, $reduce_bool $logic_not, $logic_and, $logic_or, $mux, $tribuf - $sr, $dff, $dffsr, $adff, $dlatch + $sr, $ff, $dff, $dffsr, $adff, $dlatch \end{lstlisting} \section{singleton -- create singleton modules} @@ -2793,6 +3099,13 @@ on partly selected designs. -top <module> use the specified module as top module (default='top') + -auto-top + automatically determine the top of the design hierarchy + + -flatten + flatten the design before synthesis. this will pass '-auto-top' to + 'hierarchy' if no top module is specified. + -encfile <file> passed to 'fsm_recode' via 'fsm' @@ -2818,11 +3131,12 @@ on partly selected designs. The following commands are executed by this synthesis command: begin: - hierarchy -check [-top <top>] + hierarchy -check [-top <top> | -auto-top] coarse: proc - opt_const + flatten (if -flatten) + opt_expr opt_clean check opt @@ -2850,6 +3164,73 @@ The following commands are executed by this synthesis command: check \end{lstlisting} +\section{synth\_gowin -- synthesis for Gowin FPGAs} +\label{cmd:synth_gowin} +\begin{lstlisting}[numbers=left,frame=single] + synth_gowin [options] + +This command runs synthesis for Gowin FPGAs. This work is experimental. + + -top <module> + use the specified module as top module (default='top') + + -vout <file> + write the design to the specified Verilog netlist file. writing of an + output file is omitted if this parameter is not specified. + + -run <from_label>:<to_label> + only run the commands between the labels (see below). an empty + from label is synonymous to 'begin', and empty to label is + synonymous to the end of the command list. + + -retime + run 'abc' with -dff option + + +The following commands are executed by this synthesis command: + + begin: + read_verilog -lib +/gowin/cells_sim.v + hierarchy -check -top <top> + + flatten: + proc + flatten + tribuf -logic + deminout + + coarse: + synth -run coarse + + fine: + opt -fast -mux_undef -undriven -fine + memory_map + opt -undriven -fine + techmap + clean -purge + splitnets -ports + setundef -undriven -zero + abc -dff (only if -retime) + + map_luts: + abc -lut 4 + clean + + map_cells: + techmap -map +/gowin/cells_map.v + hilomap -hicell VCC V -locell GND G + iopadmap -inpad IBUF O:I -outpad OBUF I:O + clean -purge + + check: + hierarchy -check + stat + check -noinit + + vout: + write_verilog -attr2comment -defparam -renameprefix gen <file-name> +\end{lstlisting} + \section{synth\_greenpak4 -- synthesis for GreenPAK4 FPGAs} \label{cmd:synth_greenpak4} \begin{lstlisting}[numbers=left,frame=single] @@ -2860,12 +3241,12 @@ This command runs synthesis for GreenPAK4 FPGAs. This work is experimental. -top <module> use the specified module as top module (default='top') - -blif <file> - write the design to the specified BLIF file. writing of an output file - is omitted if this parameter is not specified. + -part <part> + synthesize for the specified part. Valid values are SLG46140V, + SLG46620V, and SLG46621V (default). - -edif <file> - write the design to the specified edif file. writing of an output file + -json <file> + write the design to the specified JSON file. writing of an output file is omitted if this parameter is not specified. -run <from_label>:<to_label> @@ -2886,7 +3267,7 @@ The following commands are executed by this synthesis command: read_verilog -lib +/greenpak4/cells_sim.v hierarchy -check -top <top> - flatten: (unless -noflatten) + flatten: (unless -noflatten) proc flatten tribuf -logic @@ -2895,20 +3276,34 @@ The following commands are executed by this synthesis command: synth -run coarse fine: + greenpak4_counters + clean opt -fast -mux_undef -undriven -fine memory_map opt -undriven -fine techmap dfflibmap -prepare -liberty +/greenpak4/gp_dff.lib opt -fast - abc -dff (only if -retime) + abc -dff (only if -retime) map_luts: - nlutmap -luts 0,8,16,2 + nlutmap -assert -luts 0,6,8,2 (for -part SLG46140V) + nlutmap -assert -luts 2,8,16,2 (for -part SLG46620V) + nlutmap -assert -luts 2,8,16,2 (for -part SLG46621V) clean map_cells: + shregmap -tech greenpak4 + dfflibmap -liberty +/greenpak4/gp_dff.lib + dffinit -ff GP_DFF Q INIT + dffinit -ff GP_DFFR Q INIT + dffinit -ff GP_DFFS Q INIT + dffinit -ff GP_DFFSR Q INIT + iopadmap -bits -inpad GP_IBUF OUT:IN -outpad GP_OBUF IN:OUT -inoutpad GP_OBUF OUT:IN -toutpad GP_OBUFT OE:IN:OUT -tinoutpad GP_IOBUF OE:OUT:IN:IO + attrmvcp -attr src -attr LOC t:GP_OBUF t:GP_OBUFT t:GP_IOBUF n:* + attrmvcp -attr src -attr LOC -driven t:GP_IBUF n:* techmap -map +/greenpak4/cells_map.v + greenpak4_dffinv clean check: @@ -2916,11 +3311,8 @@ The following commands are executed by this synthesis command: stat check -noinit - blif: - write_blif -gates -attr -param <file-name> - - edif: - write_edif <file-name> + json: + write_json <file-name> \end{lstlisting} \section{synth\_ice40 -- synthesis for iCE40 FPGAs} @@ -2928,7 +3320,7 @@ The following commands are executed by this synthesis command: \begin{lstlisting}[numbers=left,frame=single] synth_ice40 [options] -This command runs synthesis for iCE40 FPGAs. This work is experimental. +This command runs synthesis for iCE40 FPGAs. -top <module> use the specified module as top module (default='top') @@ -2968,15 +3360,16 @@ The following commands are executed by this synthesis command: read_verilog -lib +/ice40/cells_sim.v hierarchy -check -top <top> - flatten: (unless -noflatten) + flatten: (unless -noflatten) proc flatten tribuf -logic + deminout coarse: synth -run coarse - bram: (skip if -nobram) + bram: (skip if -nobram) memory_bram -rules +/ice40/brams.txt techmap -map +/ice40/brams_map.v @@ -2984,15 +3377,15 @@ The following commands are executed by this synthesis command: opt -fast -mux_undef -undriven -fine memory_map opt -undriven -fine - techmap -map +/techmap.v [-map +/ice40/arith_map.v] - abc -dff (only if -retime) + techmap -map +/techmap.v -map +/ice40/arith_map.v + abc -dff (only if -retime) ice40_opt map_ffs: dffsr2dff dff2dffe -direct-match $_DFF_* techmap -map +/ice40/cells_map.v - opt_const -mux_undef + opt_expr -mux_undef simplemap ice40_ffinit ice40_ffssr @@ -3001,6 +3394,7 @@ The following commands are executed by this synthesis command: map_luts: abc (only if -abc2) ice40_opt (only if -abc2) + techmap -map +/ice40/latches_map.v abc -lut 4 clean @@ -3052,6 +3446,7 @@ The following commands are executed by this synthesis command: begin: read_verilog -lib +/xilinx/cells_sim.v + read_verilog -lib +/xilinx/cells_xtra.v read_verilog -lib +/xilinx/brams_bb.v read_verilog -lib +/xilinx/drams_bb.v hierarchy -check -top <top> @@ -3258,6 +3653,9 @@ specified logfile(s). -a logfile Write output to this file, append if exists. + + +INT, -INT + Add/subract INT from the -v setting for this command. \end{lstlisting} \section{test\_abcloop -- automatically test handling of loops in abc command} @@ -3326,7 +3724,7 @@ cell types. Use for example 'all /$add' for all cell types except $add. pass this option to techmap. -simlib - use "techmap -map +/simlib.v -max_iter 2 -autoproc" + use "techmap -D SIMLIB_NOCHECKS -map +/simlib.v -max_iter 2 -autoproc" -aigmap instead of calling "techmap", call "aigmap" @@ -3347,6 +3745,9 @@ cell types. Use for example 'all /$add' for all cell types except $add. -noeval do not check const-eval models + -edges + test cell edges db creator against sat-based implementation + -v print additional debug information to the console @@ -3425,10 +3826,13 @@ Add the specified options to the list of default options to read_verilog. verilog_defaults -clear + Clear the list of Verilog default options. - verilog_defaults -push verilog_defaults -pop + verilog_defaults -push + verilog_defaults -pop + Push or pop the list of default options to a stack. Note that -push does not imply -clear. \end{lstlisting} @@ -3480,6 +3884,12 @@ the 32 bit adders in the following code with adders of more appropriate widths: module test(input [3:0] a, b, c, output [7:0] y); assign y = a + b + c + 1; endmodule + +Options: + + -memx + Do not change the width of memory address ports. Use this options in + flows that use the 'memory_memx' pass. \end{lstlisting} \section{write\_blif -- write design to BLIF file} @@ -3505,7 +3915,14 @@ Write the current design to an BLIF file. use the specified cell types to drive nets that are constant 1, 0, or undefined. when '-' is used as <cell-type>, then <out-port> specifies the wire name to be used for the constant signal and no cell driving - that wire is generated. + that wire is generated. when '+' is used as <cell-type>, then <out-port> + specifies the wire name to be used for the constant signal and a .names + statement is generated to drive the wire. + + -noalias + if a net name is aliasing another net name, then by default a net + without fanout is created that is driven by the other net. This option + suppresses the generation of this nets without fanout. The following options can be useful when the generated file is not going to be read by a BLIF parser but a custom tool. It is recommended to not name the output @@ -3557,6 +3974,11 @@ Write the current design to an EDIF netlist file. -top top_module set the specified module as design top module + -nogndvcc + do not create "GND" and "VCC" cells. (this will produce an error + if the design contains constant nets. use "hilomap" to map to custom + constant drivers first) + Unfortunately there are different "flavors" of the EDIF file format. This command generates EDIF files for the Xilinx place&route tools. It might be necessary to make small modifications to this command when a different tool @@ -3831,10 +4253,10 @@ functions operating on that state. The '<mod>_s' sort represents a module state. Additional '<mod>_n' functions are provided that can be used to access the values of the signals in the module. -Only ports, and signals with the 'keep' attribute set are made available via -such functions. Without the -bv option, multi-bit wires are exported as -separate functions of type Bool for the individual bits. With the -bv option -multi-bit wires are exported as single functions of type BitVec. +By default only ports, registers, and wires with the 'keep' attribute set are +made available via such functions. With the -nobv option, multi-bit wires are +exported as separate functions of type Bool for the individual bits. Without +-nobv multi-bit wires are exported as single functions of type BitVec. The '<mod>_t' function evaluates to 'true' when the given pair of states describes a valid state transition. @@ -3846,29 +4268,33 @@ The '<mod>_u' function evaluates to 'true' when the given state satisfies the assumptions in the module. The '<mod>_i' function evaluates to 'true' when the given state conforms -to the initial state. +to the initial state. Furthermore the '<mod>_is' function should be asserted +to be true for initial states in addition to '<mod>_i', and should be +asserted to be false for non-initial states. + +For hierarchical designs, the '<mod>_h' function must be asserted for each +state to establish the design hierarchy. The '<mod>_h <cellname>' function +evaluates to the state corresponding to the given cell within <mod>. -verbose this will print the recursive walk used to export the modules. - -bv - enable support for BitVec (FixedSizeBitVectors theory). with this - option set multi-bit wires are represented using the BitVec sort and + -nobv + disable support for BitVec (FixedSizeBitVectors theory). without this + option multi-bit wires are represented using the BitVec sort and support for coarse grain cells (incl. arithmetic) is enabled. - -mem - enable support for memories (via ArraysEx theory). this option - also implies -bv. only $mem cells without merged registers in + -nomem + disable support for memories (via ArraysEx theory). this option is + implied by -nobv. only $mem cells without merged registers in read ports are supported. call "memory" with -nordff to make sure that no registers are merged into $mem read ports. '<mod>_m' functions will be generated for accessing the arrays that are used to represent memories. - -regs - also create '<mod>_n' functions for all registers. - -wires - also create '<mod>_n' functions for all public wires. + create '<mod>_n' functions for all public wires. by default only ports, + registers, and wires with the 'keep' attribute are exported. -tpl <template_file> use the given template file. the line containing only the token '%%' @@ -3960,6 +4386,10 @@ Write the current design to an SPICE netlist file. -nc_prefix prefix for not-connected nets (default: _NC) + -inames + include names of internal ($-prefixed) nets in outputs + (default is to use net numbers instead) + -top top_module set the specified module as design top module \end{lstlisting} @@ -3976,6 +4406,9 @@ Write the current design to a Verilog file. instead of a backslash prefix) are changed to short names in the format '_<number>_'. + -renameprefix <prefix> + insert this prefix in front of auto-generated instance names + -noattr with this option no attributes are included in the output @@ -3986,6 +4419,21 @@ Write the current design to a Verilog file. without this option all internal cells are converted to Verilog expressions. + -nodec + 32-bit constant values are by default dumped as decimal numbers, + not bit pattern. This option decativates this feature and instead + will write out all constants in binary. + + -nostr + Parameters and attributes that are specified as strings in the + original input will be output as strings by this back-end. This + decativates this feature and instead will write string constants + as binary numbers. + + -defparam + Use 'defparam' statements instead of the Verilog-2001 syntax for + cell parameters. + -blackboxes usually modules with the 'blackbox' attribute are ignored. with this option set only the modules with the 'blackbox' attribute @@ -3994,5 +4442,25 @@ Write the current design to a Verilog file. -selected only write selected modules. modules must be selected entirely or not at all. + + -v + verbose output (print new names of all renamed wires and cells) + +Note that RTLIL processes can't always be mapped directly to Verilog +always blocks. This frontend should only be used to export an RTLIL +netlist, i.e. after the "proc" pass has been used to convert all +processes to logic networks and registers. A warning is generated when +this command is called on a design with RTLIL processes. +\end{lstlisting} + +\section{zinit -- add inverters so all FF are zero-initialized} +\label{cmd:zinit} +\begin{lstlisting}[numbers=left,frame=single] + zinit [options] [selection] + +Add inverters as needed to make all FFs zero-initialized. + + -all + also add zero initialization to uninitialized FFs \end{lstlisting} diff --git a/passes/cmds/setattr.cc b/passes/cmds/setattr.cc index 9b05ae32..689e3148 100644 --- a/passes/cmds/setattr.cc +++ b/passes/cmds/setattr.cc @@ -134,15 +134,18 @@ struct SetparamPass : public Pass { { // |---v---|---v---|---v---|---v---|---v---|---v---|---v---|---v---|---v---|---v---| log("\n"); - log(" setparam [ -set name value | -unset name ]... [selection]\n"); + log(" setparam [ -type cell_type ] [ -set name value | -unset name ]... [selection]\n"); log("\n"); log("Set/unset the given parameters on the selected cells. String values must be\n"); log("passed in double quotes (\").\n"); log("\n"); + log("The -type option can be used to change the cell type of the selected cells.\n"); + log("\n"); } virtual void execute(std::vector<std::string> args, RTLIL::Design *design) { - std::vector<setunset_t> setunset_list; + vector<setunset_t> setunset_list; + string new_cell_type; size_t argidx; for (argidx = 1; argidx < args.size(); argidx++) @@ -158,6 +161,10 @@ struct SetparamPass : public Pass { setunset_list.push_back(setunset_t(args[++argidx])); continue; } + if (arg == "-type" && argidx+1 < args.size()) { + new_cell_type = RTLIL::escape_id(args[++argidx]); + continue; + } break; } extra_args(args, argidx, design); @@ -170,8 +177,11 @@ struct SetparamPass : public Pass { continue; for (auto &it : module->cells_) - if (design->selected(module, it.second)) + if (design->selected(module, it.second)) { + if (!new_cell_type.empty()) + it.second->type = new_cell_type; do_setunset(it.second->parameters, setunset_list); + } } } } SetparamPass; diff --git a/passes/fsm/fsm.cc b/passes/fsm/fsm.cc index 3b537ecd..997558b8 100644 --- a/passes/fsm/fsm.cc +++ b/passes/fsm/fsm.cc @@ -59,6 +59,9 @@ struct FsmPass : public Pass { log(" -expand, -norecode, -export, -nomap\n"); log(" enable or disable passes as indicated above\n"); log("\n"); + log(" -fullexpand\n"); + log(" call expand with -full option\n"); + log("\n"); log(" -encoding type\n"); log(" -fm_set_fsm_file file\n"); log(" -encfile file\n"); @@ -71,6 +74,7 @@ struct FsmPass : public Pass { bool flag_norecode = false; bool flag_nodetect = false; bool flag_expand = false; + bool flag_fullexpand = false; bool flag_export = false; std::string fm_set_fsm_file_opt; std::string encfile_opt; @@ -110,6 +114,10 @@ struct FsmPass : public Pass { flag_expand = true; continue; } + if (arg == "-fullexpand") { + flag_fullexpand = true; + continue; + } if (arg == "-export") { flag_export = true; continue; @@ -126,8 +134,8 @@ struct FsmPass : public Pass { Pass::call(design, "opt_clean"); Pass::call(design, "fsm_opt"); - if (flag_expand) { - Pass::call(design, "fsm_expand"); + if (flag_expand || flag_fullexpand) { + Pass::call(design, flag_fullexpand ? "fsm_expand -full" : "fsm_expand"); Pass::call(design, "opt_clean"); Pass::call(design, "fsm_opt"); } diff --git a/passes/fsm/fsm_expand.cc b/passes/fsm/fsm_expand.cc index 3ded3f37..e7b9dcf9 100644 --- a/passes/fsm/fsm_expand.cc +++ b/passes/fsm/fsm_expand.cc @@ -32,6 +32,8 @@ struct FsmExpand { RTLIL::Module *module; RTLIL::Cell *fsm_cell; + bool full_mode; + SigMap assign_map; SigSet<RTLIL::Cell*, RTLIL::sort_by_name_id<RTLIL::Cell>> sig2driver, sig2user; CellTypes ct; @@ -45,6 +47,9 @@ struct FsmExpand bool is_cell_merge_candidate(RTLIL::Cell *cell) { + if (full_mode || cell->type == "$_MUX_") + return true; + if (cell->type == "$mux" || cell->type == "$pmux") if (cell->getPort("\\A").size() < 2) return true; @@ -68,17 +73,6 @@ struct FsmExpand if (new_signals.size() > 3) return false; - if (cell->hasPort("\\Y")) { - new_signals.append(assign_map(cell->getPort("\\Y"))); - new_signals.sort_and_unify(); - new_signals.remove_const(); - new_signals.remove(assign_map(fsm_cell->getPort("\\CTRL_IN"))); - new_signals.remove(assign_map(fsm_cell->getPort("\\CTRL_OUT"))); - } - - if (new_signals.size() > 2) - return false; - return true; } @@ -200,13 +194,15 @@ struct FsmExpand fsm_data.copy_to_cell(fsm_cell); } - FsmExpand(RTLIL::Cell *cell, RTLIL::Design *design, RTLIL::Module *mod) + FsmExpand(RTLIL::Cell *cell, RTLIL::Design *design, RTLIL::Module *mod, bool full) { module = mod; fsm_cell = cell; + full_mode = full; assign_map.set(module); ct.setup_internals(); + ct.setup_stdcells(); for (auto &cell_it : module->cells_) { RTLIL::Cell *c = cell_it.second; @@ -249,17 +245,31 @@ struct FsmExpandPass : public Pass { { // |---v---|---v---|---v---|---v---|---v---|---v---|---v---|---v---|---v---|---v---| log("\n"); - log(" fsm_expand [selection]\n"); + log(" fsm_expand [-full] [selection]\n"); log("\n"); log("The fsm_extract pass is conservative about the cells that belong to a finite\n"); log("state machine. This pass can be used to merge additional auxiliary gates into\n"); log("the finite state machine.\n"); log("\n"); + log("By default, fsm_expand is still a bit conservative regarding merging larger\n"); + log("word-wide cells. Call with -full to consider all cells for merging.\n"); + log("\n"); } virtual void execute(std::vector<std::string> args, RTLIL::Design *design) { + bool full_mode = false; + log_header(design, "Executing FSM_EXPAND pass (merging auxiliary logic into FSMs).\n"); - extra_args(args, 1, design); + + size_t argidx; + for (argidx = 1; argidx < args.size(); argidx++) { + if (args[argidx] == "-full") { + full_mode = true; + continue; + } + break; + } + extra_args(args, argidx, design); for (auto &mod_it : design->modules_) { if (!design->selected(mod_it.second)) @@ -269,7 +279,7 @@ struct FsmExpandPass : public Pass { if (cell_it.second->type == "$fsm" && design->selected(mod_it.second, cell_it.second)) fsm_cells.push_back(cell_it.second); for (auto c : fsm_cells) { - FsmExpand fsm_expand(c, design, mod_it.second); + FsmExpand fsm_expand(c, design, mod_it.second, full_mode); fsm_expand.execute(); } } diff --git a/passes/fsm/fsm_map.cc b/passes/fsm/fsm_map.cc index 5b32ed59..c4230375 100644 --- a/passes/fsm/fsm_map.cc +++ b/passes/fsm/fsm_map.cc @@ -272,7 +272,8 @@ static void map_fsm(RTLIL::Cell *fsm_cell, RTLIL::Module *module) } else { - RTLIL::SigSpec sig_a, sig_b, sig_s; + RTLIL::SigSpec sig_a(RTLIL::State::Sx, next_state_wire->width); + RTLIL::SigSpec sig_b, sig_s; int reset_state = fsm_data.reset_state; if (reset_state < 0) reset_state = 0; diff --git a/passes/fsm/fsm_recode.cc b/passes/fsm/fsm_recode.cc index 5102d833..e1bde728 100644 --- a/passes/fsm/fsm_recode.cc +++ b/passes/fsm/fsm_recode.cc @@ -57,13 +57,13 @@ static void fsm_recode(RTLIL::Cell *cell, RTLIL::Module *module, FILE *fm_set_fs log("Recoding FSM `%s' from module `%s' using `%s' encoding:\n", cell->name.c_str(), module->name.c_str(), encoding.c_str()); - if (encoding != "none" && encoding != "one-hot" && encoding != "binary" && encoding != "auto") { + if (encoding != "none" && encoding != "user" && encoding != "one-hot" && encoding != "binary" && encoding != "auto") { log(" unknown encoding `%s': using auto instead.\n", encoding.c_str()); encoding = "auto"; } - if (encoding == "none") { - log(" nothing to do for encoding `none'.\n"); + if (encoding == "none" || encoding == "user") { + log(" nothing to do for encoding `%s'.\n", encoding.c_str()); return; } diff --git a/passes/hierarchy/hierarchy.cc b/passes/hierarchy/hierarchy.cc index 4d1e3987..e21a7a4e 100644 --- a/passes/hierarchy/hierarchy.cc +++ b/passes/hierarchy/hierarchy.cc @@ -212,6 +212,10 @@ bool expand_module(RTLIL::Design *design, RTLIL::Module *module, bool flag_check } else if (mod->wire(conn.first) == nullptr || mod->wire(conn.first)->port_id == 0) log_error("Module `%s' referenced in module `%s' in cell `%s' does not have a port named '%s'.\n", log_id(cell->type), log_id(module), log_id(cell), log_id(conn.first)); + for (auto ¶m : cell->parameters) + if (mod->avail_parameters.count(param.first) == 0 && param.first[0] != '$') + log_error("Module `%s' referenced in module `%s' in cell `%s' does not have a parameter named '%s'.\n", + log_id(cell->type), log_id(module), log_id(cell), log_id(param.first)); } if (cell->parameters.size() == 0) diff --git a/passes/opt/opt.cc b/passes/opt/opt.cc index 13ea5469..021c1a03 100644 --- a/passes/opt/opt.cc +++ b/passes/opt/opt.cc @@ -44,7 +44,7 @@ struct OptPass : public Pass { log(" opt_muxtree\n"); log(" opt_reduce [-fine] [-full]\n"); log(" opt_merge [-share_all]\n"); - log(" opt_rmdff\n"); + log(" opt_rmdff [-keepdc]\n"); log(" opt_clean [-purge]\n"); log(" opt_expr [-mux_undef] [-mux_bool] [-undriven] [-clkinv] [-fine] [-full] [-keepdc]\n"); log(" while <changed design>\n"); @@ -54,7 +54,7 @@ struct OptPass : public Pass { log(" do\n"); log(" opt_expr [-mux_undef] [-mux_bool] [-undriven] [-clkinv] [-fine] [-full] [-keepdc]\n"); log(" opt_merge [-share_all]\n"); - log(" opt_rmdff\n"); + log(" opt_rmdff [-keepdc]\n"); log(" opt_clean [-purge]\n"); log(" while <changed design in opt_rmdff>\n"); log("\n"); @@ -69,6 +69,7 @@ struct OptPass : public Pass { std::string opt_expr_args; std::string opt_reduce_args; std::string opt_merge_args; + std::string opt_rmdff_args; bool fast_mode = false; log_header(design, "Executing OPT pass (performing simple optimizations).\n"); @@ -108,6 +109,7 @@ struct OptPass : public Pass { } if (args[argidx] == "-keepdc") { opt_expr_args += " -keepdc"; + opt_rmdff_args += " -keepdc"; continue; } if (args[argidx] == "-share_all") { @@ -128,7 +130,7 @@ struct OptPass : public Pass { Pass::call(design, "opt_expr" + opt_expr_args); Pass::call(design, "opt_merge" + opt_merge_args); design->scratchpad_unset("opt.did_something"); - Pass::call(design, "opt_rmdff"); + Pass::call(design, "opt_rmdff" + opt_rmdff_args); if (design->scratchpad_get_bool("opt.did_something") == false) break; Pass::call(design, "opt_clean" + opt_clean_args); @@ -145,7 +147,7 @@ struct OptPass : public Pass { Pass::call(design, "opt_muxtree"); Pass::call(design, "opt_reduce" + opt_reduce_args); Pass::call(design, "opt_merge" + opt_merge_args); - Pass::call(design, "opt_rmdff"); + Pass::call(design, "opt_rmdff" + opt_rmdff_args); Pass::call(design, "opt_clean" + opt_clean_args); Pass::call(design, "opt_expr" + opt_expr_args); if (design->scratchpad_get_bool("opt.did_something") == false) diff --git a/passes/opt/opt_rmdff.cc b/passes/opt/opt_rmdff.cc index fa954afa..922f086f 100644 --- a/passes/opt/opt_rmdff.cc +++ b/passes/opt/opt_rmdff.cc @@ -29,6 +29,7 @@ PRIVATE_NAMESPACE_BEGIN SigMap assign_map, dff_init_map; SigSet<RTLIL::Cell*> mux_drivers; dict<SigBit, pool<SigBit>> init_attributes; +bool keepdc; void remove_init_attr(SigSpec sig) { @@ -71,7 +72,11 @@ bool handle_dff(RTLIL::Module *mod, RTLIL::Cell *dff) RTLIL::SigSpec sig_d, sig_q, sig_c, sig_r; RTLIL::Const val_cp, val_rp, val_rv; - if (dff->type == "$_DFF_N_" || dff->type == "$_DFF_P_") { + if (dff->type == "$_FF_") { + sig_d = dff->getPort("\\D"); + sig_q = dff->getPort("\\Q"); + } + else if (dff->type == "$_DFF_N_" || dff->type == "$_DFF_P_") { sig_d = dff->getPort("\\D"); sig_q = dff->getPort("\\Q"); sig_c = dff->getPort("\\C"); @@ -89,6 +94,10 @@ bool handle_dff(RTLIL::Module *mod, RTLIL::Cell *dff) val_rp = RTLIL::Const(dff->type[7] == 'P', 1); val_rv = RTLIL::Const(dff->type[8] == '1', 1); } + else if (dff->type == "$ff") { + sig_d = dff->getPort("\\D"); + sig_q = dff->getPort("\\Q"); + } else if (dff->type == "$dff") { sig_d = dff->getPort("\\D"); sig_q = dff->getPort("\\Q"); @@ -115,12 +124,12 @@ bool handle_dff(RTLIL::Module *mod, RTLIL::Cell *dff) bool has_init = false; RTLIL::Const val_init; for (auto bit : dff_init_map(sig_q).to_sigbit_vector()) { - if (bit.wire == NULL) + if (bit.wire == NULL || keepdc) has_init = true; val_init.bits.push_back(bit.wire == NULL ? bit.data : RTLIL::State::Sx); } - if (dff->type == "$dff" && mux_drivers.has(sig_d)) { + if (dff->type.in("$ff", "$dff") && mux_drivers.has(sig_d)) { std::set<RTLIL::Cell*> muxes; mux_drivers.find(sig_d, muxes); for (auto mux : muxes) { @@ -137,7 +146,7 @@ bool handle_dff(RTLIL::Module *mod, RTLIL::Cell *dff) } } - if (sig_c.is_fully_const() && (!sig_r.size() || !has_init || val_init == val_rv)) { + if (!sig_c.empty() && sig_c.is_fully_const() && (!sig_r.size() || !has_init || val_init == val_rv)) { if (val_rv.bits.size() == 0) val_rv = val_init; mod->connect(sig_q, val_rv); @@ -182,7 +191,7 @@ struct OptRmdffPass : public Pass { { // |---v---|---v---|---v---|---v---|---v---|---v---|---v---|---v---|---v---|---v---| log("\n"); - log(" opt_rmdff [selection]\n"); + log(" opt_rmdff [-keepdc] [selection]\n"); log("\n"); log("This pass identifies flip-flops with constant inputs and replaces them with\n"); log("a constant driver.\n"); @@ -193,7 +202,17 @@ struct OptRmdffPass : public Pass { int total_count = 0, total_initdrv = 0; log_header(design, "Executing OPT_RMDFF pass (remove dff with constant values).\n"); - extra_args(args, 1, design); + keepdc = false; + + size_t argidx; + for (argidx = 1; argidx < args.size(); argidx++) { + if (args[argidx] == "-keepdc") { + keepdc = true; + continue; + } + break; + } + extra_args(args, argidx, design); for (auto module : design->selected_modules()) { @@ -243,10 +262,10 @@ struct OptRmdffPass : public Pass { if (!design->selected(module, cell)) continue; - if (cell->type.in("$_DFF_N_", "$_DFF_P_", + if (cell->type.in("$_FF_", "$_DFF_N_", "$_DFF_P_", "$_DFF_NN0_", "$_DFF_NN1_", "$_DFF_NP0_", "$_DFF_NP1_", "$_DFF_PN0_", "$_DFF_PN1_", "$_DFF_PP0_", "$_DFF_PP1_", - "$dff", "$adff")) + "$ff", "$dff", "$adff")) dff_list.push_back(cell->name); if (cell->type == "$dlatch") diff --git a/passes/proc/proc_dff.cc b/passes/proc/proc_dff.cc index f532990c..98653dc6 100644 --- a/passes/proc/proc_dff.cc +++ b/passes/proc/proc_dff.cc @@ -196,7 +196,7 @@ void gen_dff(RTLIL::Module *mod, RTLIL::SigSpec sig_in, RTLIL::Const val_rst, RT std::stringstream sstr; sstr << "$procdff$" << (autoidx++); - RTLIL::Cell *cell = mod->addCell(sstr.str(), arst ? "$adff" : "$dff"); + RTLIL::Cell *cell = mod->addCell(sstr.str(), clk.empty() ? "$ff" : arst ? "$adff" : "$dff"); cell->attributes = proc->attributes; cell->parameters["\\WIDTH"] = RTLIL::Const(sig_in.size()); @@ -204,15 +204,21 @@ void gen_dff(RTLIL::Module *mod, RTLIL::SigSpec sig_in, RTLIL::Const val_rst, RT cell->parameters["\\ARST_POLARITY"] = RTLIL::Const(arst_polarity, 1); cell->parameters["\\ARST_VALUE"] = val_rst; } - cell->parameters["\\CLK_POLARITY"] = RTLIL::Const(clk_polarity, 1); + if (!clk.empty()) { + cell->parameters["\\CLK_POLARITY"] = RTLIL::Const(clk_polarity, 1); + } cell->setPort("\\D", sig_in); cell->setPort("\\Q", sig_out); if (arst) cell->setPort("\\ARST", *arst); - cell->setPort("\\CLK", clk); + if (!clk.empty()) + cell->setPort("\\CLK", clk); - log(" created %s cell `%s' with %s edge clock", cell->type.c_str(), cell->name.c_str(), clk_polarity ? "positive" : "negative"); + if (!clk.empty()) + log(" created %s cell `%s' with %s edge clock", cell->type.c_str(), cell->name.c_str(), clk_polarity ? "positive" : "negative"); + else + log(" created %s cell `%s' with global clock", cell->type.c_str(), cell->name.c_str()); if (arst) log(" and %s level reset", arst_polarity ? "positive" : "negative"); log(".\n"); @@ -236,6 +242,7 @@ void proc_dff(RTLIL::Module *mod, RTLIL::Process *proc, ConstEval &ce) RTLIL::SyncRule *sync_level = NULL; RTLIL::SyncRule *sync_edge = NULL; RTLIL::SyncRule *sync_always = NULL; + bool global_clock = false; std::map<RTLIL::SigSpec, std::set<RTLIL::SyncRule*>> many_async_rules; @@ -267,6 +274,10 @@ void proc_dff(RTLIL::Module *mod, RTLIL::Process *proc, ConstEval &ce) sig.replace(action.first, action.second, &insig); sync_always = sync; } + else if (sync->type == RTLIL::SyncType::STg) { + sig.replace(action.first, action.second, &insig); + global_clock = true; + } else { log_error("Event with any-edge sensitivity found for this signal!\n"); } @@ -328,7 +339,7 @@ void proc_dff(RTLIL::Module *mod, RTLIL::Process *proc, ConstEval &ce) continue; } - if (!sync_edge) + if (!sync_edge && !global_clock) log_error("Missing edge-sensitive event for this signal!\n"); if (many_async_rules.size() > 0) @@ -346,9 +357,10 @@ void proc_dff(RTLIL::Module *mod, RTLIL::Process *proc, ConstEval &ce) } else gen_dff(mod, insig, rstval.as_const(), sig, - sync_edge->type == RTLIL::SyncType::STp, + sync_edge && sync_edge->type == RTLIL::SyncType::STp, sync_level && sync_level->type == RTLIL::SyncType::ST1, - sync_edge->signal, sync_level ? &sync_level->signal : NULL, proc); + sync_edge ? sync_edge->signal : SigSpec(), + sync_level ? &sync_level->signal : NULL, proc); if (free_sync_level) delete sync_level; diff --git a/passes/sat/Makefile.inc b/passes/sat/Makefile.inc index 0c5f6fc6..6785b750 100644 --- a/passes/sat/Makefile.inc +++ b/passes/sat/Makefile.inc @@ -5,4 +5,5 @@ OBJS += passes/sat/eval.o OBJS += passes/sat/miter.o OBJS += passes/sat/expose.o OBJS += passes/sat/assertpmux.o +OBJS += passes/sat/clk2fflogic.o diff --git a/passes/sat/clk2fflogic.cc b/passes/sat/clk2fflogic.cc new file mode 100644 index 00000000..ef6d5dd7 --- /dev/null +++ b/passes/sat/clk2fflogic.cc @@ -0,0 +1,226 @@ +/* + * yosys -- Yosys Open SYnthesis Suite + * + * Copyright (C) 2012 Clifford Wolf <clifford@clifford.at> + * + * Permission to use, copy, modify, and/or distribute this software for any + * purpose with or without fee is hereby granted, provided that the above + * copyright notice and this permission notice appear in all copies. + * + * THE SOFTWARE IS PROVIDED "AS IS" AND THE AUTHOR DISCLAIMS ALL WARRANTIES + * WITH REGARD TO THIS SOFTWARE INCLUDING ALL IMPLIED WARRANTIES OF + * MERCHANTABILITY AND FITNESS. IN NO EVENT SHALL THE AUTHOR BE LIABLE FOR + * ANY SPECIAL, DIRECT, INDIRECT, OR CONSEQUENTIAL DAMAGES OR ANY DAMAGES + * WHATSOEVER RESULTING FROM LOSS OF USE, DATA OR PROFITS, WHETHER IN AN + * ACTION OF CONTRACT, NEGLIGENCE OR OTHER TORTIOUS ACTION, ARISING OUT OF + * OR IN CONNECTION WITH THE USE OR PERFORMANCE OF THIS SOFTWARE. + * + */ + +#include "kernel/yosys.h" +#include "kernel/sigtools.h" + +USING_YOSYS_NAMESPACE +PRIVATE_NAMESPACE_BEGIN + +struct Clk2fflogicPass : public Pass { + Clk2fflogicPass() : Pass("clk2fflogic", "convert clocked FFs to generic $ff cells") { } + virtual void help() + { + // |---v---|---v---|---v---|---v---|---v---|---v---|---v---|---v---|---v---|---v---| + log("\n"); + log(" clk2fflogic [options] [selection]\n"); + log("\n"); + log("This command replaces clocked flip-flops with generic $ff cells that use the\n"); + log("implicit global clock. This is useful for formal verification of designs with\n"); + log("multiple clocks.\n"); + log("\n"); + } + virtual void execute(std::vector<std::string> args, RTLIL::Design *design) + { + // bool flag_noinit = false; + + log_header(design, "Executing CLK2FFLOGIC pass (convert clocked FFs to generic $ff cells).\n"); + + size_t argidx; + for (argidx = 1; argidx < args.size(); argidx++) + { + // if (args[argidx] == "-noinit") { + // flag_noinit = true; + // continue; + // } + break; + } + extra_args(args, argidx, design); + + for (auto module : design->selected_modules()) + { + SigMap sigmap(module); + dict<SigBit, State> initbits; + pool<SigBit> del_initbits; + + for (auto wire : module->wires()) + if (wire->attributes.count("\\init") > 0) + { + Const initval = wire->attributes.at("\\init"); + SigSpec initsig = sigmap(wire); + + for (int i = 0; i < GetSize(initval) && i < GetSize(initsig); i++) + if (initval[i] == State::S0 || initval[i] == State::S1) + initbits[initsig[i]] = initval[i]; + } + + for (auto cell : vector<Cell*>(module->selected_cells())) + { + if (cell->type.in("$dlatch")) + { + bool enpol = cell->parameters["\\EN_POLARITY"].as_bool(); + + SigSpec sig_en = cell->getPort("\\EN"); + SigSpec sig_d = cell->getPort("\\D"); + SigSpec sig_q = cell->getPort("\\Q"); + + log("Replacing %s.%s (%s): EN=%s, D=%s, Q=%s\n", + log_id(module), log_id(cell), log_id(cell->type), + log_signal(sig_en), log_signal(sig_d), log_signal(sig_q)); + + Wire *past_q = module->addWire(NEW_ID, GetSize(sig_q)); + module->addFf(NEW_ID, sig_q, past_q); + + if (enpol) + module->addMux(NEW_ID, past_q, sig_d, sig_en, sig_q); + else + module->addMux(NEW_ID, sig_d, past_q, sig_en, sig_q); + + Const initval; + bool assign_initval = false; + for (int i = 0; i < GetSize(sig_d); i++) { + SigBit qbit = sigmap(sig_q[i]); + if (initbits.count(qbit)) { + initval.bits.push_back(initbits.at(qbit)); + del_initbits.insert(qbit); + } else + initval.bits.push_back(State::Sx); + if (initval.bits.back() != State::Sx) + assign_initval = true; + } + + if (assign_initval) + past_q->attributes["\\init"] = initval; + + module->remove(cell); + continue; + } + + if (cell->type.in("$dff", "$adff", "$dffsr")) + { + bool clkpol = cell->parameters["\\CLK_POLARITY"].as_bool(); + + SigSpec clk = cell->getPort("\\CLK"); + Wire *past_clk = module->addWire(NEW_ID); + past_clk->attributes["\\init"] = clkpol ? State::S1 : State::S0; + module->addFf(NEW_ID, clk, past_clk); + + SigSpec sig_d = cell->getPort("\\D"); + SigSpec sig_q = cell->getPort("\\Q"); + + log("Replacing %s.%s (%s): CLK=%s, D=%s, Q=%s\n", + log_id(module), log_id(cell), log_id(cell->type), + log_signal(clk), log_signal(sig_d), log_signal(sig_q)); + + SigSpec clock_edge_pattern; + + if (clkpol) { + clock_edge_pattern.append_bit(State::S0); + clock_edge_pattern.append_bit(State::S1); + } else { + clock_edge_pattern.append_bit(State::S1); + clock_edge_pattern.append_bit(State::S0); + } + + SigSpec clock_edge = module->Eqx(NEW_ID, {clk, SigSpec(past_clk)}, clock_edge_pattern); + + Wire *past_d = module->addWire(NEW_ID, GetSize(sig_d)); + Wire *past_q = module->addWire(NEW_ID, GetSize(sig_q)); + module->addFf(NEW_ID, sig_d, past_d); + module->addFf(NEW_ID, sig_q, past_q); + + if (cell->type == "$adff") + { + SigSpec arst = cell->getPort("\\ARST"); + SigSpec qval = module->Mux(NEW_ID, past_q, past_d, clock_edge); + Const rstval = cell->parameters["\\ARST_VALUE"]; + + if (cell->parameters["\\ARST_POLARITY"].as_bool()) + module->addMux(NEW_ID, qval, rstval, arst, sig_q); + else + module->addMux(NEW_ID, rstval, qval, arst, sig_q); + } + else + if (cell->type == "$dffsr") + { + SigSpec qval = module->Mux(NEW_ID, past_q, past_d, clock_edge); + SigSpec setval = cell->getPort("\\SET"); + SigSpec clrval = cell->getPort("\\CLR"); + + if (!cell->parameters["\\SET_POLARITY"].as_bool()) + setval = module->Not(NEW_ID, setval); + + if (cell->parameters["\\CLR_POLARITY"].as_bool()) + clrval = module->Not(NEW_ID, clrval); + + qval = module->Or(NEW_ID, qval, setval); + module->addAnd(NEW_ID, qval, clrval, sig_q); + } + else + { + module->addMux(NEW_ID, past_q, past_d, clock_edge, sig_q); + } + + Const initval; + bool assign_initval = false; + for (int i = 0; i < GetSize(sig_d); i++) { + SigBit qbit = sigmap(sig_q[i]); + if (initbits.count(qbit)) { + initval.bits.push_back(initbits.at(qbit)); + del_initbits.insert(qbit); + } else + initval.bits.push_back(State::Sx); + if (initval.bits.back() != State::Sx) + assign_initval = true; + } + + if (assign_initval) { + past_d->attributes["\\init"] = initval; + past_q->attributes["\\init"] = initval; + } + + module->remove(cell); + continue; + } + } + + for (auto wire : module->wires()) + if (wire->attributes.count("\\init") > 0) + { + bool delete_initattr = true; + Const initval = wire->attributes.at("\\init"); + SigSpec initsig = sigmap(wire); + + for (int i = 0; i < GetSize(initval) && i < GetSize(initsig); i++) + if (del_initbits.count(initsig[i]) > 0) + initval[i] = State::Sx; + else if (initval[i] != State::Sx) + delete_initattr = false; + + if (delete_initattr) + wire->attributes.erase("\\init"); + else + wire->attributes.at("\\init") = initval; + } + } + + } +} Clk2fflogicPass; + +PRIVATE_NAMESPACE_END diff --git a/passes/sat/miter.cc b/passes/sat/miter.cc index 4854e19b..9e150b60 100644 --- a/passes/sat/miter.cc +++ b/passes/sat/miter.cc @@ -312,18 +312,42 @@ void create_miter_assert(struct Pass *that, std::vector<std::string> args, RTLIL log_pop(); } - SigSpec or_signals; + SigSpec assert_signals, assume_signals; vector<Cell*> cell_list = module->cells(); - for (auto cell : cell_list) { + for (auto cell : cell_list) + { + if (!cell->type.in("$assert", "$assume")) + continue; + + SigBit is_active = module->Nex(NEW_ID, cell->getPort("\\A"), State::S1); + SigBit is_enabled = module->Eqx(NEW_ID, cell->getPort("\\EN"), State::S1); + if (cell->type == "$assert") { - SigBit is_active = module->Nex(NEW_ID, cell->getPort("\\A"), State::S1); - SigBit is_enabled = module->Eqx(NEW_ID, cell->getPort("\\EN"), State::S1); - or_signals.append(module->And(NEW_ID, is_active, is_enabled)); - module->remove(cell); + assert_signals.append(module->And(NEW_ID, is_active, is_enabled)); + } else { + assume_signals.append(module->And(NEW_ID, is_active, is_enabled)); } + + module->remove(cell); } - module->addReduceOr(NEW_ID, or_signals, trigger); + if (assume_signals.empty()) + { + module->addReduceOr(NEW_ID, assert_signals, trigger); + } + else + { + Wire *assume_q = module->addWire(NEW_ID); + assume_q->attributes["\\init"] = State::S0; + assume_signals.append(assume_q); + + SigSpec assume_nok = module->ReduceOr(NEW_ID, assume_signals); + SigSpec assume_ok = module->Not(NEW_ID, assume_nok); + module->addFf(NEW_ID, assume_nok, assume_q); + + SigSpec assert_fail = module->ReduceOr(NEW_ID, assert_signals); + module->addAnd(NEW_ID, assert_fail, assume_ok, trigger); + } if (flag_flatten) { log_push(); diff --git a/passes/techmap/Makefile.inc b/passes/techmap/Makefile.inc index b5024fa9..311a1af9 100644 --- a/passes/techmap/Makefile.inc +++ b/passes/techmap/Makefile.inc @@ -31,6 +31,7 @@ OBJS += passes/techmap/deminout.o OBJS += passes/techmap/insbuf.o OBJS += passes/techmap/attrmvcp.o OBJS += passes/techmap/attrmap.o +OBJS += passes/techmap/zinit.o endif GENFILES += passes/techmap/techmap.inc diff --git a/passes/techmap/attrmap.cc b/passes/techmap/attrmap.cc index f715b63e..dec81d21 100644 --- a/passes/techmap/attrmap.cc +++ b/passes/techmap/attrmap.cc @@ -33,13 +33,32 @@ Const make_value(string &value) return sig.as_const(); } +bool string_compare_nocase(const string &str1, const string &str2) +{ + if (str1.size() != str2.size()) + return false; + + for (size_t i = 0; i < str1.size(); i++) + { + char ch1 = str1[i], ch2 = str2[i]; + if ('a' <= ch1 && ch1 <= 'z') + ch1 -= 'a' - 'A'; + if ('a' <= ch2 && ch2 <= 'z') + ch2 -= 'a' - 'A'; + if (ch1 != ch2) + return false; + } + + return true; +} + bool match_name(string &name, IdString &id, bool ignore_case=false) { string str1 = RTLIL::escape_id(name); string str2 = id.str(); if (ignore_case) - return !strcasecmp(str1.c_str(), str2.c_str()); + return string_compare_nocase(str1, str2); return str1 == str2; } @@ -49,7 +68,7 @@ bool match_value(string &value, Const &val, bool ignore_case=false) if (ignore_case && ((val.flags & RTLIL::CONST_FLAG_STRING) != 0) && GetSize(value) && value.front() == '"' && value.back() == '"') { string str1 = value.substr(1, GetSize(value)-2); string str2 = val.decode_string(); - return !strcasecmp(str1.c_str(), str2.c_str()); + return string_compare_nocase(str1, str2); } return make_value(value) == val; diff --git a/passes/techmap/attrmvcp.cc b/passes/techmap/attrmvcp.cc index 50eaf61d..1537def0 100644 --- a/passes/techmap/attrmvcp.cc +++ b/passes/techmap/attrmvcp.cc @@ -93,6 +93,7 @@ struct AttrmvcpPass : public Pass { for (auto cell : module->selected_cells()) for (auto &conn : cell->connections()) + { if (driven_mode) { if (cell->input(conn.first)) for (auto bit : sigmap(conn.second)) @@ -102,6 +103,7 @@ struct AttrmvcpPass : public Pass { for (auto bit : sigmap(conn.second)) net2cells[bit].insert(cell); } + } for (auto wire : module->selected_wires()) { diff --git a/passes/techmap/simplemap.cc b/passes/techmap/simplemap.cc index 0fb64734..c6b932bd 100644 --- a/passes/techmap/simplemap.cc +++ b/passes/techmap/simplemap.cc @@ -388,6 +388,23 @@ void simplemap_sr(RTLIL::Module *module, RTLIL::Cell *cell) } } +void simplemap_ff(RTLIL::Module *module, RTLIL::Cell *cell) +{ + int width = cell->parameters.at("\\WIDTH").as_int(); + + RTLIL::SigSpec sig_d = cell->getPort("\\D"); + RTLIL::SigSpec sig_q = cell->getPort("\\Q"); + + std::string gate_type = "$_FF_"; + + for (int i = 0; i < width; i++) { + RTLIL::Cell *gate = module->addCell(NEW_ID, gate_type); + gate->add_strpool_attribute("\\src", cell->get_strpool_attribute("\\src")); + gate->setPort("\\D", sig_d[i]); + gate->setPort("\\Q", sig_q[i]); + } +} + void simplemap_dff(RTLIL::Module *module, RTLIL::Cell *cell) { int width = cell->parameters.at("\\WIDTH").as_int(); @@ -532,6 +549,7 @@ void simplemap_get_mappers(std::map<RTLIL::IdString, void(*)(RTLIL::Module*, RTL mappers["$slice"] = simplemap_slice; mappers["$concat"] = simplemap_concat; mappers["$sr"] = simplemap_sr; + mappers["$ff"] = simplemap_ff; mappers["$dff"] = simplemap_dff; mappers["$dffe"] = simplemap_dffe; mappers["$dffsr"] = simplemap_dffsr; @@ -569,7 +587,7 @@ struct SimplemapPass : public Pass { log(" $not, $pos, $and, $or, $xor, $xnor\n"); log(" $reduce_and, $reduce_or, $reduce_xor, $reduce_xnor, $reduce_bool\n"); log(" $logic_not, $logic_and, $logic_or, $mux, $tribuf\n"); - log(" $sr, $dff, $dffsr, $adff, $dlatch\n"); + log(" $sr, $ff, $dff, $dffsr, $adff, $dlatch\n"); log("\n"); } virtual void execute(std::vector<std::string> args, RTLIL::Design *design) diff --git a/passes/techmap/techmap.cc b/passes/techmap/techmap.cc index b2cc492b..6784f48c 100644 --- a/passes/techmap/techmap.cc +++ b/passes/techmap/techmap.cc @@ -345,6 +345,12 @@ struct TechmapWorker c->setParam("\\MEMID", Const(memory_renames[memid].str())); } + if (c->type == "$mem") { + string memid = c->getParam("\\MEMID").decode_string(); + apply_prefix(cell->name.str(), memid); + c->setParam("\\MEMID", Const(memid)); + } + if (c->attributes.count("\\src")) c->add_strpool_attribute("\\src", extra_src_attrs); } @@ -1164,8 +1170,9 @@ struct FlattenPass : public Pass { worker.flatten_do_list.erase(mod->name); } } else { - for (auto mod : vector<Module*>(design->modules())) + for (auto mod : vector<Module*>(design->modules())) { while (worker.techmap_module(design, mod, design, handled_cells, celltypeMap, false)) { } + } } log("No more expansions possible.\n"); diff --git a/passes/techmap/zinit.cc b/passes/techmap/zinit.cc new file mode 100644 index 00000000..a577e123 --- /dev/null +++ b/passes/techmap/zinit.cc @@ -0,0 +1,151 @@ +/* + * yosys -- Yosys Open SYnthesis Suite + * + * Copyright (C) 2012 Clifford Wolf <clifford@clifford.at> + * + * Permission to use, copy, modify, and/or distribute this software for any + * purpose with or without fee is hereby granted, provided that the above + * copyright notice and this permission notice appear in all copies. + * + * THE SOFTWARE IS PROVIDED "AS IS" AND THE AUTHOR DISCLAIMS ALL WARRANTIES + * WITH REGARD TO THIS SOFTWARE INCLUDING ALL IMPLIED WARRANTIES OF + * MERCHANTABILITY AND FITNESS. IN NO EVENT SHALL THE AUTHOR BE LIABLE FOR + * ANY SPECIAL, DIRECT, INDIRECT, OR CONSEQUENTIAL DAMAGES OR ANY DAMAGES + * WHATSOEVER RESULTING FROM LOSS OF USE, DATA OR PROFITS, WHETHER IN AN + * ACTION OF CONTRACT, NEGLIGENCE OR OTHER TORTIOUS ACTION, ARISING OUT OF + * OR IN CONNECTION WITH THE USE OR PERFORMANCE OF THIS SOFTWARE. + * + */ + +#include "kernel/yosys.h" +#include "kernel/sigtools.h" + +USING_YOSYS_NAMESPACE +PRIVATE_NAMESPACE_BEGIN + +struct ZinitPass : public Pass { + ZinitPass() : Pass("zinit", "add inverters so all FF are zero-initialized") { } + virtual void help() + { + // |---v---|---v---|---v---|---v---|---v---|---v---|---v---|---v---|---v---|---v---| + log("\n"); + log(" zinit [options] [selection]\n"); + log("\n"); + log("Add inverters as needed to make all FFs zero-initialized.\n"); + log("\n"); + log(" -all\n"); + log(" also add zero initialization to uninitialized FFs\n"); + log("\n"); + } + virtual void execute(std::vector<std::string> args, RTLIL::Design *design) + { + bool all_mode = false; + + log_header(design, "Executing ZINIT pass (make all FFs zero-initialized).\n"); + + size_t argidx; + for (argidx = 1; argidx < args.size(); argidx++) + { + if (args[argidx] == "-singleton") { + all_mode = true; + continue; + } + break; + } + extra_args(args, argidx, design); + + for (auto module : design->selected_modules()) + { + SigMap sigmap(module); + dict<SigBit, State> initbits; + pool<SigBit> donebits; + + for (auto wire : module->selected_wires()) + { + if (wire->attributes.count("\\init") == 0) + continue; + + SigSpec wirebits = sigmap(wire); + Const initval = wire->attributes.at("\\init"); + wire->attributes.erase("\\init"); + + for (int i = 0; i < GetSize(wirebits) && i < GetSize(initval); i++) + { + SigBit bit = wirebits[i]; + State val = initval[i]; + + if (val != State::S0 && val != State::S1 && bit.wire != nullptr) + continue; + + if (initbits.count(bit)) { + if (initbits.at(bit) != val) + log_error("Conflicting init values for signal %s (%s = %s != %s).\n", + log_signal(bit), log_signal(SigBit(wire, i)), + log_signal(val), log_signal(initbits.at(bit))); + continue; + } + + initbits[bit] = val; + } + } + + pool<IdString> dff_types = { + "$ff", "$dff", "$dffe", "$dffsr", "$adff", + "$_FF_", "$_DFFE_NN_", "$_DFFE_NP_", "$_DFFE_PN_", "$_DFFE_PP_", + "$_DFFSR_NNN_", "$_DFFSR_NNP_", "$_DFFSR_NPN_", "$_DFFSR_NPP_", + "$_DFFSR_PNN_", "$_DFFSR_PNP_", "$_DFFSR_PPN_", "$_DFFSR_PPP_", + "$_DFF_N_", "$_DFF_NN0_", "$_DFF_NN1_", "$_DFF_NP0_", "$_DFF_NP1_", + "$_DFF_P_", "$_DFF_PN0_", "$_DFF_PN1_", "$_DFF_PP0_", "$_DFF_PP1_" + }; + + for (auto cell : module->selected_cells()) + { + if (!dff_types.count(cell->type)) + continue; + + SigSpec sig_d = sigmap(cell->getPort("\\D")); + SigSpec sig_q = sigmap(cell->getPort("\\Q")); + + if (GetSize(sig_d) < 1 || GetSize(sig_q) < 1) + continue; + + Const initval; + + for (int i = 0; i < GetSize(sig_q); i++) { + if (initbits.count(sig_q[i])) { + initval.bits.push_back(initbits.at(sig_q[i])); + donebits.insert(sig_q[i]); + } else + initval.bits.push_back(all_mode ? State::S0 : State::Sx); + } + + Wire *initwire = module->addWire(NEW_ID, GetSize(initval)); + initwire->attributes["\\init"] = initval; + + for (int i = 0; i < GetSize(initwire); i++) + if (initval.bits.at(i) == State::S1) + { + sig_d[i] = module->NotGate(NEW_ID, sig_d[i]); + module->addNotGate(NEW_ID, SigSpec(initwire, i), sig_q[i]); + initwire->attributes["\\init"].bits.at(i) = State::S0; + } + else + { + module->connect(sig_q[i], SigSpec(initwire, i)); + } + + log("FF init value for cell %s (%s): %s = %s\n", log_id(cell), log_id(cell->type), + log_signal(sig_q), log_signal(initval)); + + cell->setPort("\\D", sig_d); + cell->setPort("\\Q", initwire); + } + + for (auto &it : initbits) + if (donebits.count(it.first) == 0) + log_error("Failed to handle init bit %s = %s.\n", log_signal(it.first), log_signal(it.second)); + } + } +} ZinitPass; + +PRIVATE_NAMESPACE_END diff --git a/techlibs/common/prep.cc b/techlibs/common/prep.cc index fac6c4ba..71534983 100644 --- a/techlibs/common/prep.cc +++ b/techlibs/common/prep.cc @@ -63,6 +63,9 @@ struct PrepPass : public ScriptPass log(" -nordff\n"); log(" passed to 'memory_dff'. prohibits merging of FFs into memory read ports\n"); log("\n"); + log(" -nokeepdc\n"); + log(" do not call opt_* with -keepdc\n"); + log("\n"); log(" -run <from_label>[:<to_label>]\n"); log(" only run the commands between the labels (see below). an empty\n"); log(" from label is synonymous to 'begin', and empty to label is\n"); @@ -75,7 +78,7 @@ struct PrepPass : public ScriptPass } string top_module, fsm_opts, memory_opts; - bool autotop, flatten, ifxmode, memxmode, nomemmode; + bool autotop, flatten, ifxmode, memxmode, nomemmode, nokeepdc; virtual void clear_flags() YS_OVERRIDE { @@ -87,6 +90,7 @@ struct PrepPass : public ScriptPass ifxmode = false; memxmode = false; nomemmode = false; + nokeepdc = false; } virtual void execute(std::vector<std::string> args, RTLIL::Design *design) YS_OVERRIDE @@ -136,6 +140,10 @@ struct PrepPass : public ScriptPass memory_opts += " -nordff"; continue; } + if (args[argidx] == "-nokeepdc") { + nokeepdc = true; + continue; + } break; } extra_args(args, argidx, design); @@ -177,10 +185,10 @@ struct PrepPass : public ScriptPass run(ifxmode ? "proc -ifx" : "proc"); if (help_mode || flatten) run("flatten", "(if -flatten)"); - run("opt_expr -keepdc"); + run(nokeepdc ? "opt_expr" : "opt_expr -keepdc"); run("opt_clean"); run("check"); - run("opt -keepdc"); + run(nokeepdc ? "opt" : "opt -keepdc"); if (!ifxmode) { if (help_mode) run("wreduce [-memx]"); @@ -194,7 +202,7 @@ struct PrepPass : public ScriptPass run("opt_clean"); run("memory_collect"); } - run("opt -keepdc -fast"); + run(nokeepdc ? "opt -fast" : "opt -keepdc -fast"); } if (check_label("check")) diff --git a/techlibs/common/simcells.v b/techlibs/common/simcells.v index c4f170a3..e770c545 100644 --- a/techlibs/common/simcells.v +++ b/techlibs/common/simcells.v @@ -495,6 +495,23 @@ always @(posedge S, posedge R) begin end endmodule +`ifdef SIMCELLS_FF +// |---v---|---v---|---v---|---v---|---v---|---v---|---v---|---v---|---v---|---v---| +//- +//- $_FF_ (D, Q) +//- +//- A D-type flip-flop that is clocked from the implicit global clock. (This cell +//- type is usually only used in netlists for formal verification.) +//- +module \$_FF_ (D, Q); +input D; +output reg Q; +always @($global_clock) begin + Q <= D; +end +endmodule +`endif + // |---v---|---v---|---v---|---v---|---v---|---v---|---v---|---v---|---v---|---v---| //- //- $_DFF_N_ (D, C, Q) diff --git a/techlibs/common/simlib.v b/techlibs/common/simlib.v index 922a47ca..2c4db1ac 100644 --- a/techlibs/common/simlib.v +++ b/techlibs/common/simlib.v @@ -1334,6 +1334,18 @@ endmodule // -------------------------------------------------------- +module \$anyseq (Y); + +parameter WIDTH = 0; + +output [WIDTH-1:0] Y; + +assign Y = 'bx; + +endmodule + +// -------------------------------------------------------- + module \$equiv (A, B, Y); input A, B; @@ -1382,6 +1394,23 @@ endmodule `endif // -------------------------------------------------------- +`ifdef SIMLIB_FF + +module \$ff (D, Q); + +parameter WIDTH = 0; + +input [WIDTH-1:0] D; +output reg [WIDTH-1:0] Q; + +always @($global_clk) begin + Q <= D; +end + +endmodule + +`endif +// -------------------------------------------------------- module \$dff (CLK, D, Q); diff --git a/techlibs/common/techmap.v b/techlibs/common/techmap.v index 90c4ed7e..d7ec3947 100644 --- a/techlibs/common/techmap.v +++ b/techlibs/common/techmap.v @@ -64,7 +64,7 @@ module _90_simplemap_various; endmodule (* techmap_simplemap *) -(* techmap_celltype = "$sr $dff $dffe $adff $dffsr $dlatch" *) +(* techmap_celltype = "$sr $ff $dff $dffe $adff $dffsr $dlatch" *) module _90_simplemap_registers; endmodule diff --git a/techlibs/gowin/Makefile.inc b/techlibs/gowin/Makefile.inc new file mode 100644 index 00000000..679d7eff --- /dev/null +++ b/techlibs/gowin/Makefile.inc @@ -0,0 +1,6 @@ + +OBJS += techlibs/gowin/synth_gowin.o + +$(eval $(call add_share_file,share/gowin,techlibs/gowin/cells_map.v)) +$(eval $(call add_share_file,share/gowin,techlibs/gowin/cells_sim.v)) + diff --git a/techlibs/gowin/cells_map.v b/techlibs/gowin/cells_map.v new file mode 100644 index 00000000..e1f85eff --- /dev/null +++ b/techlibs/gowin/cells_map.v @@ -0,0 +1,31 @@ +module \$_DFF_N_ (input D, C, output Q); DFFN _TECHMAP_REPLACE_ (.D(D), .Q(Q), .CLK(C)); endmodule +module \$_DFF_P_ (input D, C, output Q); DFF _TECHMAP_REPLACE_ (.D(D), .Q(Q), .CLK(C)); endmodule + +module \$lut (A, Y); + parameter WIDTH = 0; + parameter LUT = 0; + + input [WIDTH-1:0] A; + output Y; + + generate + if (WIDTH == 1) begin + LUT1 #(.INIT(LUT)) _TECHMAP_REPLACE_ (.F(Y), + .I0(A[0])); + end else + if (WIDTH == 2) begin + LUT2 #(.INIT(LUT)) _TECHMAP_REPLACE_ (.F(Y), + .I0(A[0]), .I1(A[1])); + end else + if (WIDTH == 3) begin + LUT3 #(.INIT(LUT)) _TECHMAP_REPLACE_ (.F(Y), + .I0(A[0]), .I1(A[1]), .I2(A[2])); + end else + if (WIDTH == 4) begin + LUT4 #(.INIT(LUT)) _TECHMAP_REPLACE_ (.F(Y), + .I0(A[0]), .I1(A[1]), .I2(A[2]), .I3(A[3])); + end else begin + wire _TECHMAP_FAIL_ = 1; + end + endgenerate +endmodule diff --git a/techlibs/gowin/cells_sim.v b/techlibs/gowin/cells_sim.v new file mode 100644 index 00000000..3a09c157 --- /dev/null +++ b/techlibs/gowin/cells_sim.v @@ -0,0 +1,51 @@ +module LUT1(output F, input I0); + parameter [1:0] INIT = 0; + assign F = I0 ? INIT[1] : INIT[0]; +endmodule + +module LUT2(output F, input I0, I1); + parameter [3:0] INIT = 0; + wire [ 1: 0] s1 = I1 ? INIT[ 3: 2] : INIT[ 1: 0]; + assign F = I0 ? s1[1] : s1[0]; +endmodule + +module LUT3(output F, input I0, I1, I2); + parameter [7:0] INIT = 0; + wire [ 3: 0] s2 = I2 ? INIT[ 7: 4] : INIT[ 3: 0]; + wire [ 1: 0] s1 = I1 ? s2[ 3: 2] : s2[ 1: 0]; + assign F = I0 ? s1[1] : s1[0]; +endmodule + +module LUT4(output F, input I0, I1, I2, I3); + parameter [15:0] INIT = 0; + wire [ 7: 0] s3 = I3 ? INIT[15: 8] : INIT[ 7: 0]; + wire [ 3: 0] s2 = I2 ? s3[ 7: 4] : s3[ 3: 0]; + wire [ 1: 0] s1 = I1 ? s2[ 3: 2] : s2[ 1: 0]; + assign F = I0 ? s1[1] : s1[0]; +endmodule + +module DFF (output reg Q, input CLK, D); + always @(posedge C) + Q <= D; +endmodule + +module DFFN (output reg Q, input CLK, D); + always @(negedge C) + Q <= D; +endmodule + +module VCC(output V); + assign V = 1; +endmodule + +module GND(output G); + assign G = 0; +endmodule + +module IBUF(output O, input I); + assign O = I; +endmodule + +module OBUF(output O, input I); + assign O = I; +endmodule diff --git a/techlibs/gowin/synth_gowin.cc b/techlibs/gowin/synth_gowin.cc new file mode 100644 index 00000000..129ab839 --- /dev/null +++ b/techlibs/gowin/synth_gowin.cc @@ -0,0 +1,178 @@ +/* + * yosys -- Yosys Open SYnthesis Suite + * + * Copyright (C) 2012 Clifford Wolf <clifford@clifford.at> + * + * Permission to use, copy, modify, and/or distribute this software for any + * purpose with or without fee is hereby granted, provided that the above + * copyright notice and this permission notice appear in all copies. + * + * THE SOFTWARE IS PROVIDED "AS IS" AND THE AUTHOR DISCLAIMS ALL WARRANTIES + * WITH REGARD TO THIS SOFTWARE INCLUDING ALL IMPLIED WARRANTIES OF + * MERCHANTABILITY AND FITNESS. IN NO EVENT SHALL THE AUTHOR BE LIABLE FOR + * ANY SPECIAL, DIRECT, INDIRECT, OR CONSEQUENTIAL DAMAGES OR ANY DAMAGES + * WHATSOEVER RESULTING FROM LOSS OF USE, DATA OR PROFITS, WHETHER IN AN + * ACTION OF CONTRACT, NEGLIGENCE OR OTHER TORTIOUS ACTION, ARISING OUT OF + * OR IN CONNECTION WITH THE USE OR PERFORMANCE OF THIS SOFTWARE. + * + */ + +#include "kernel/register.h" +#include "kernel/celltypes.h" +#include "kernel/rtlil.h" +#include "kernel/log.h" + +USING_YOSYS_NAMESPACE +PRIVATE_NAMESPACE_BEGIN + +struct SynthGowinPass : public ScriptPass +{ + SynthGowinPass() : ScriptPass("synth_gowin", "synthesis for Gowin FPGAs") { } + + virtual void help() YS_OVERRIDE + { + // |---v---|---v---|---v---|---v---|---v---|---v---|---v---|---v---|---v---|---v---| + log("\n"); + log(" synth_gowin [options]\n"); + log("\n"); + log("This command runs synthesis for Gowin FPGAs. This work is experimental.\n"); + log("\n"); + log(" -top <module>\n"); + log(" use the specified module as top module (default='top')\n"); + log("\n"); + log(" -vout <file>\n"); + log(" write the design to the specified Verilog netlist file. writing of an\n"); + log(" output file is omitted if this parameter is not specified.\n"); + log("\n"); + log(" -run <from_label>:<to_label>\n"); + log(" only run the commands between the labels (see below). an empty\n"); + log(" from label is synonymous to 'begin', and empty to label is\n"); + log(" synonymous to the end of the command list.\n"); + log("\n"); + log(" -retime\n"); + log(" run 'abc' with -dff option\n"); + log("\n"); + log("\n"); + log("The following commands are executed by this synthesis command:\n"); + help_script(); + log("\n"); + } + + string top_opt, vout_file; + bool retime; + + virtual void clear_flags() YS_OVERRIDE + { + top_opt = "-auto-top"; + vout_file = ""; + retime = false; + } + + virtual void execute(std::vector<std::string> args, RTLIL::Design *design) YS_OVERRIDE + { + string run_from, run_to; + clear_flags(); + + size_t argidx; + for (argidx = 1; argidx < args.size(); argidx++) + { + if (args[argidx] == "-top" && argidx+1 < args.size()) { + top_opt = "-top " + args[++argidx]; + continue; + } + if (args[argidx] == "-vout" && argidx+1 < args.size()) { + vout_file = args[++argidx]; + continue; + } + if (args[argidx] == "-run" && argidx+1 < args.size()) { + size_t pos = args[argidx+1].find(':'); + if (pos == std::string::npos) + break; + run_from = args[++argidx].substr(0, pos); + run_to = args[argidx].substr(pos+1); + continue; + } + if (args[argidx] == "-retime") { + retime = true; + continue; + } + break; + } + extra_args(args, argidx, design); + + if (!design->full_selection()) + log_cmd_error("This comannd only operates on fully selected designs!\n"); + + log_header(design, "Executing SYNTH_GOWIN pass.\n"); + log_push(); + + run_script(design, run_from, run_to); + + log_pop(); + } + + virtual void script() YS_OVERRIDE + { + if (check_label("begin")) + { + run("read_verilog -lib +/gowin/cells_sim.v"); + run(stringf("hierarchy -check %s", help_mode ? "-top <top>" : top_opt.c_str())); + } + + if (check_label("flatten")) + { + run("proc"); + run("flatten"); + run("tribuf -logic"); + run("deminout"); + } + + if (check_label("coarse")) + { + run("synth -run coarse"); + } + + if (check_label("fine")) + { + run("opt -fast -mux_undef -undriven -fine"); + run("memory_map"); + run("opt -undriven -fine"); + run("techmap"); + run("clean -purge"); + run("splitnets -ports"); + run("setundef -undriven -zero"); + if (retime || help_mode) + run("abc -dff", "(only if -retime)"); + } + + if (check_label("map_luts")) + { + run("abc -lut 4"); + run("clean"); + } + + if (check_label("map_cells")) + { + run("techmap -map +/gowin/cells_map.v"); + run("hilomap -hicell VCC V -locell GND G"); + run("iopadmap -inpad IBUF O:I -outpad OBUF I:O"); + run("clean -purge"); + } + + if (check_label("check")) + { + run("hierarchy -check"); + run("stat"); + run("check -noinit"); + } + + if (check_label("vout")) + { + if (!vout_file.empty() || help_mode) + run(stringf("write_verilog -attr2comment -defparam -renameprefix gen %s", + help_mode ? "<file-name>" : vout_file.c_str())); + } + } +} SynthGowinPass; + +PRIVATE_NAMESPACE_END diff --git a/techlibs/greenpak4/cells_sim.v b/techlibs/greenpak4/cells_sim.v index 6ae9ae79..80746be0 100644 --- a/techlibs/greenpak4/cells_sim.v +++ b/techlibs/greenpak4/cells_sim.v @@ -131,9 +131,8 @@ endmodule module GP_DELAY(input IN, output reg OUT); parameter DELAY_STEPS = 1; - - //TODO: additional delay/glitch filter mode - + parameter GLITCH_FILTER = 0; + initial OUT = 0; generate @@ -241,6 +240,16 @@ module GP_DFFSRI(input D, CLK, nSR, output reg nQ); end endmodule +module GP_EDGEDET(input IN, output reg OUT); + + parameter EDGE_DIRECTION = "RISING"; + parameter DELAY_STEPS = 1; + parameter GLITCH_FILTER = 0; + + //not implemented for simulation + +endmodule + module GP_IBUF(input IN, output OUT); assign OUT = IN; endmodule @@ -296,6 +305,27 @@ module GP_PGA(input wire VIN_P, input wire VIN_N, input wire VIN_SEL, output reg endmodule +module GP_PGEN(input wire nRST, input wire CLK, output reg OUT); + initial OUT = 0; + parameter PATTERN_DATA = 16'h0; + parameter PATTERN_LEN = 5'd16; + + reg[3:0] count = 0; + always @(posedge CLK) begin + if(!nRST) + OUT <= PATTERN_DATA[0]; + + else begin + count <= count + 1; + OUT <= PATTERN_DATA[count]; + + if( (count + 1) == PATTERN_LEN) + count <= 0; + end + end + +endmodule + module GP_POR(output reg RST_DONE); parameter POR_TIME = 500; @@ -409,7 +439,8 @@ endmodule //keep constraint needed to prevent optimization since we have no outputs (* keep *) module GP_SYSRESET(input RST); - parameter RESET_MODE = "RISING"; + parameter RESET_MODE = "EDGE"; + parameter EDGE_SPEED = 4; //cannot simulate whole system reset diff --git a/techlibs/ice40/synth_ice40.cc b/techlibs/ice40/synth_ice40.cc index 38a9cf9d..2533d3af 100644 --- a/techlibs/ice40/synth_ice40.cc +++ b/techlibs/ice40/synth_ice40.cc @@ -35,7 +35,7 @@ struct SynthIce40Pass : public ScriptPass log("\n"); log(" synth_ice40 [options]\n"); log("\n"); - log("This command runs synthesis for iCE40 FPGAs. This work is experimental.\n"); + log("This command runs synthesis for iCE40 FPGAs.\n"); log("\n"); log(" -top <module>\n"); log(" use the specified module as top module (default='top')\n"); diff --git a/tests/asicworld/run-test.sh b/tests/asicworld/run-test.sh index 24983f1a..d5708c45 100755 --- a/tests/asicworld/run-test.sh +++ b/tests/asicworld/run-test.sh @@ -1,2 +1,14 @@ #!/bin/bash -exec ${MAKE:-make} -f ../tools/autotest.mk EXTRA_FLAGS="-e" *.v + +OPTIND=1 +seed="" # default to no seed specified +while getopts "S:" opt +do + case "$opt" in + S) arg="${OPTARG#"${OPTARG%%[![:space:]]*}"}" # remove leading space + seed="SEED=$arg" ;; + esac +done +shift "$((OPTIND-1))" + +exec ${MAKE:-make} -f ../tools/autotest.mk $seed EXTRA_FLAGS="-e" *.v diff --git a/tests/bram/generate.py b/tests/bram/generate.py index 05a7ed02..def0b23c 100644 --- a/tests/bram/generate.py +++ b/tests/bram/generate.py @@ -1,11 +1,11 @@ #!/usr/bin/env python3 +import argparse import os import sys import random debug_mode = False -seed = (int(os.times()[4]*100) + os.getpid()) % 900000 + 100000 def create_bram(dsc_f, sim_f, ref_f, tb_f, k1, k2, or_next): while True: @@ -25,12 +25,15 @@ def create_bram(dsc_f, sim_f, ref_f, tb_f, k1, k2, or_next): if wrmode.count(0) == 0: continue break - if random.randrange(2) or True: + if random.randrange(2): maxpol = 4 maxtransp = 1 + maxclocks = 4 else: - maxpol = 2 + maxpol = None + clkpol = random.randrange(4) maxtransp = 2 + maxclocks = 1 def generate_enable(i): if wrmode[i]: @@ -45,11 +48,16 @@ def create_bram(dsc_f, sim_f, ref_f, tb_f, k1, k2, or_next): return random.randrange(maxtransp) return 0 - ports = [ random.randrange(1, 3) for i in range(groups) ] - enable = [ generate_enable(i) for i in range(groups) ] - transp = [ generate_transp(i) for i in range(groups) ] - clocks = [ random.randrange(1, 4) for i in range(groups) ] - clkpol = [ random.randrange(maxpol) for i in range(groups) ] + def generate_clkpol(i): + if maxpol is None: + return clkpol + return random.randrange(maxpol) + + ports = [ random.randrange(1, 3) for i in range(groups) ] + enable = [ generate_enable(i) for i in range(groups) ] + transp = [ generate_transp(i) for i in range(groups) ] + clocks = [ random.randrange(maxclocks)+1 for i in range(groups) ] + clkpol = [ generate_clkpol(i) for i in range(groups) ] break print("bram bram_%02d_%02d" % (k1, k2), file=dsc_f) @@ -109,11 +117,13 @@ def create_bram(dsc_f, sim_f, ref_f, tb_f, k1, k2, or_next): if clocks[p1] and not ("CLK%d" % clocks[p1]) in v_ports: v_ports.add("CLK%d" % clocks[p1]) v_stmts.append("input CLK%d;" % clocks[p1]) - tb_decls.append("reg CLK%d;" % clocks[p1]) + tb_decls.append("reg CLK%d = 0;" % clocks[p1]) tb_clocks.append("CLK%d" % clocks[p1]) v_ports.add("%sADDR" % pf) v_stmts.append("input [%d:0] %sADDR;" % (abits-1, pf)) + if transp[p1]: + v_stmts.append("reg [%d:0] %sADDR_Q;" % (abits-1, pf)) tb_decls.append("reg [%d:0] %sADDR;" % (abits-1, pf)) tb_addr.append("%sADDR" % pf) @@ -159,8 +169,11 @@ def create_bram(dsc_f, sim_f, ref_f, tb_f, k1, k2, or_next): for i in range(enable[p1]): enrange = "[%d:%d]" % ((i+1)*dbits/enable[p1]-1, i*dbits/enable[p1]) v_always[last_always_hdr].append((portindex, pf, "if (%sEN[%d]) memory[%sADDR]%s = %sDATA%s;" % (pf, i, pf, enrange, pf, enrange))) + elif transp[p1]: + v_always[last_always_hdr].append((sum(ports)+1, pf, "%sADDR_Q %s %sADDR;" % (pf, assign_op, pf))) + v_stmts.append("always @* %sDATA = memory[%sADDR_Q];" % (pf, pf)) else: - v_always[last_always_hdr].append((sum(ports)+1 if transp[p1] else 0, pf, "%sDATA %s memory[%sADDR];" % (pf, assign_op, pf))) + v_always[last_always_hdr].append((0, pf, "%sDATA %s memory[%sADDR];" % (pf, assign_op, pf))) for always_hdr in sorted(v_always): v_stmts.append(always_hdr[1]) @@ -243,10 +256,23 @@ def create_bram(dsc_f, sim_f, ref_f, tb_f, k1, k2, or_next): print(" end", file=tb_f) print("endmodule", file=tb_f) -print("Rng seed: %d" % seed) +parser = argparse.ArgumentParser(formatter_class = argparse.ArgumentDefaultsHelpFormatter) +parser.add_argument('-S', '--seed', type = int, help = 'seed for PRNG') +parser.add_argument('-c', '--count', type = int, default = 5, help = 'number of test cases to generate') +parser.add_argument('-d', '--debug', action='store_true') +args = parser.parse_args() + +debug_mode = args.debug + +if args.seed is not None: + seed = args.seed +else: + seed = (int(os.times()[4]*100) + os.getpid()) % 900000 + 100000 + +print("PRNG seed: %d" % seed) random.seed(seed) -for k1 in range(5): +for k1 in range(args.count): dsc_f = open("temp/brams_%02d.txt" % k1, "w") sim_f = open("temp/brams_%02d.v" % k1, "w") ref_f = open("temp/brams_%02d_ref.v" % k1, "w") diff --git a/tests/bram/run-single.sh b/tests/bram/run-single.sh index 19a235c7..98a45b61 100644 --- a/tests/bram/run-single.sh +++ b/tests/bram/run-single.sh @@ -2,7 +2,7 @@ set -e ../../yosys -qq -p "proc; opt; memory -nomap -bram temp/brams_${2}.txt; opt -fast -full" \ -l temp/synth_${1}_${2}.log -o temp/synth_${1}_${2}.v temp/brams_${1}.v -iverilog -Dvcd_file=\"temp/tb_${1}_${2}.vcd\" -DSIMLIB_MEMDELAY=1ns -o temp/tb_${1}_${2}.tb temp/brams_${1}_tb.v \ +iverilog -Dvcd_file=\"temp/tb_${1}_${2}.vcd\" -DSIMLIB_MEMDELAY=1 -o temp/tb_${1}_${2}.tb temp/brams_${1}_tb.v \ temp/brams_${1}_ref.v temp/synth_${1}_${2}.v temp/brams_${2}.v ../../techlibs/common/simlib.v temp/tb_${1}_${2}.tb > temp/tb_${1}_${2}.txt if grep -q ERROR temp/tb_${1}_${2}.txt; then diff --git a/tests/bram/run-test.sh b/tests/bram/run-test.sh index f0bf0131..d6ba0de4 100755 --- a/tests/bram/run-test.sh +++ b/tests/bram/run-test.sh @@ -4,11 +4,26 @@ # MAKE="make -j8" time bash -c 'for ((i=0; i<100; i++)); do echo "-- $i --"; bash run-test.sh || exit 1; done' set -e + +OPTIND=1 +count=5 +seed="" # default to no seed specified +debug="" +while getopts "c:dS:" opt +do + case "$opt" in + c) count="$OPTARG" ;; + d) debug="-d" ;; + S) seed="-S $OPTARG" ;; + esac +done +shift "$((OPTIND-1))" + rm -rf temp mkdir -p temp echo "generating tests.." -python3 generate.py +python3 generate.py $debug -c $count $seed { echo -n "all:" diff --git a/tests/fsm/generate.py b/tests/fsm/generate.py index 8757d474..c8eda0cd 100644 --- a/tests/fsm/generate.py +++ b/tests/fsm/generate.py @@ -1,5 +1,6 @@ #!/usr/bin/env python3 +import argparse import sys import random from contextlib import contextmanager @@ -30,7 +31,16 @@ def random_expr(variables): return "%d'd%s" % (bits, random.randint(0, 2**bits-1)) raise AssertionError -for idx in range(50): +parser = argparse.ArgumentParser(formatter_class = argparse.ArgumentDefaultsHelpFormatter) +parser.add_argument('-S', '--seed', type = int, help = 'seed for PRNG') +parser.add_argument('-c', '--count', type = int, default = 50, help = 'number of test cases to generate') +args = parser.parse_args() + +if args.seed is not None: + print("PRNG seed: %d" % args.seed) + random.seed(args.seed) + +for idx in range(args.count): with open('temp/uut_%05d.v' % idx, 'w') as f: with redirect_stdout(f): rst2 = random.choice([False, True]) diff --git a/tests/fsm/run-test.sh b/tests/fsm/run-test.sh index 42389233..cf506470 100755 --- a/tests/fsm/run-test.sh +++ b/tests/fsm/run-test.sh @@ -5,10 +5,22 @@ set -e +OPTIND=1 +count=100 +seed="" # default to no seed specified +while getopts "c:S:" opt +do + case "$opt" in + c) count="$OPTARG" ;; + S) seed="-S $OPTARG" ;; + esac +done +shift "$((OPTIND-1))" + rm -rf temp mkdir -p temp echo "generating tests.." -python3 generate.py +python3 generate.py -c $count $seed { all_targets="all_targets:" diff --git a/tests/hana/run-test.sh b/tests/hana/run-test.sh index fb766eec..878c80b3 100755 --- a/tests/hana/run-test.sh +++ b/tests/hana/run-test.sh @@ -1,2 +1,14 @@ #!/bin/bash -exec ${MAKE:-make} -f ../tools/autotest.mk EXTRA_FLAGS="-l hana_vlib.v -n 300 -e" test_*.v + +OPTIND=1 +seed="" # default to no seed specified +while getopts "S:" opt +do + case "$opt" in + S) arg="${OPTARG#"${OPTARG%%[![:space:]]*}"}" # remove leading space + seed="SEED=$arg" ;; + esac +done +shift "$((OPTIND-1))" + +exec ${MAKE:-make} -f ../tools/autotest.mk $seed EXTRA_FLAGS="-l hana_vlib.v -n 300 -e" test_*.v diff --git a/tests/memories/run-test.sh b/tests/memories/run-test.sh index c3b19618..734a9668 100755 --- a/tests/memories/run-test.sh +++ b/tests/memories/run-test.sh @@ -1,7 +1,18 @@ #!/bin/bash set -e -bash ../tools/autotest.sh -G *.v + +OPTIND=1 +seed="" # default to no seed specified +while getopts "S:" opt +do + case "$opt" in + S) seed="-S $OPTARG" ;; + esac +done +shift "$((OPTIND-1))" + +bash ../tools/autotest.sh $seed -G *.v for f in `egrep -l 'expect-(wr|rd)-ports' *.v`; do echo -n "Testing expectations for $f .." diff --git a/tests/realmath/generate.py b/tests/realmath/generate.py index 19d01c7c..2bedf38e 100644 --- a/tests/realmath/generate.py +++ b/tests/realmath/generate.py @@ -1,5 +1,6 @@ #!/usr/bin/env python3 +import argparse import sys import random from contextlib import contextmanager @@ -36,7 +37,16 @@ def random_expression(depth = 3, maxparam = 0): return op + '(' + recursion() + ', ' + recursion() + ')' raise -for idx in range(100): +parser = argparse.ArgumentParser(formatter_class = argparse.ArgumentDefaultsHelpFormatter) +parser.add_argument('-S', '--seed', type = int, help = 'seed for PRNG') +parser.add_argument('-c', '--count', type = int, default = 100, help = 'number of test cases to generate') +args = parser.parse_args() + +if args.seed is not None: + print("PRNG seed: %d" % args.seed) + random.seed(args.seed) + +for idx in range(args.count): with open('temp/uut_%05d.v' % idx, 'w') as f: with redirect_stdout(f): print('module uut_%05d(output [63:0] %s);\n' % (idx, ', '.join(['y%02d' % i for i in range(100)]))) diff --git a/tests/realmath/run-test.sh b/tests/realmath/run-test.sh index f1ec5476..e1a36c69 100755 --- a/tests/realmath/run-test.sh +++ b/tests/realmath/run-test.sh @@ -1,14 +1,26 @@ #!/bin/bash set -e +OPTIND=1 +count=100 +seed="" # default to no seed specified +while getopts "c:S:" opt +do + case "$opt" in + c) count="$OPTARG" ;; + S) seed="-S $OPTARG" ;; + esac +done +shift "$((OPTIND-1))" + rm -rf temp mkdir -p temp echo "generating tests.." -python3 generate.py +python3 generate.py -c $count $seed cd temp echo "running tests.." -for ((i = 0; i < 100; i++)); do +for ((i = 0; i < $count; i++)); do echo -n "[$i]" idx=$( printf "%05d" $i ) ../../../yosys -qq uut_${idx}.ys diff --git a/tests/share/generate.py b/tests/share/generate.py index 01a19a8d..7e87bd64 100644 --- a/tests/share/generate.py +++ b/tests/share/generate.py @@ -1,5 +1,6 @@ #!/usr/bin/env python3 +import argparse import sys import random from contextlib import contextmanager @@ -21,7 +22,16 @@ def maybe_plus_x(expr): else: return expr -for idx in range(100): +parser = argparse.ArgumentParser(formatter_class = argparse.ArgumentDefaultsHelpFormatter) +parser.add_argument('-S', '--seed', type = int, help = 'seed for PRNG') +parser.add_argument('-c', '--count', type = int, default = 100, help = 'number of test cases to generate') +args = parser.parse_args() + +if args.seed is not None: + print("PRNG seed: %d" % args.seed) + random.seed(args.seed) + +for idx in range(args.count): with open('temp/uut_%05d.v' % idx, 'w') as f: with redirect_stdout(f): if random.choice(['bin', 'uni']) == 'bin': diff --git a/tests/share/run-test.sh b/tests/share/run-test.sh index 18dbbc27..1bcd8e42 100755 --- a/tests/share/run-test.sh +++ b/tests/share/run-test.sh @@ -5,10 +5,22 @@ set -e +OPTIND=1 +count=100 +seed="" # default to no seed specified +while getopts "c:S:" opt +do + case "$opt" in + c) count="$OPTARG" ;; + S) seed="-S $OPTARG" ;; + esac +done +shift "$((OPTIND-1))" + rm -rf temp mkdir -p temp echo "generating tests.." -python3 generate.py +python3 generate.py -c $count $seed echo "running tests.." for i in $( ls temp/*.ys | sed 's,[^0-9],,g; s,^0*\(.\),\1,g;' ); do diff --git a/tests/simple/run-test.sh b/tests/simple/run-test.sh index 6531d51a..aaa1cf94 100755 --- a/tests/simple/run-test.sh +++ b/tests/simple/run-test.sh @@ -1,9 +1,20 @@ #!/bin/bash +OPTIND=1 +seed="" # default to no seed specified +while getopts "S:" opt +do + case "$opt" in + S) arg="${OPTARG#"${OPTARG%%[![:space:]]*}"}" # remove leading space + seed="SEED=$arg" ;; + esac +done +shift "$((OPTIND-1))" + # check for Icarus Verilog if ! which iverilog > /dev/null ; then echo "$0: Error: Icarus Verilog 'iverilog' not found." exit 1 fi -exec ${MAKE:-make} -f ../tools/autotest.mk *.v +exec ${MAKE:-make} -f ../tools/autotest.mk $seed *.v diff --git a/tests/tools/autotest.mk b/tests/tools/autotest.mk index f65002ce..c6867892 100644 --- a/tests/tools/autotest.mk +++ b/tests/tools/autotest.mk @@ -1,8 +1,13 @@ EXTRA_FLAGS= +SEED= + +ifneq ($(strip $(SEED)),) +SEEDOPT=-S$(SEED) +endif $(MAKECMDGOALS): - @$(basename $(MAKEFILE_LIST)).sh -G -j $(EXTRA_FLAGS) $@ + @$(basename $(MAKEFILE_LIST)).sh -G -j $(SEEDOPT) $(EXTRA_FLAGS) $@ .PHONY: $(MAKECMDGOALS) |