diff options
29 files changed, 1257 insertions, 712 deletions
@@ -86,7 +86,7 @@ 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 = f8cadfe3861f +ABCREV = a2fcd1cc61a6 ABCPULL = 1 ABCURL ?= https://bitbucket.org/alanmi/abc ABCMKARGS = CC="$(CXX)" CXX="$(CXX)" @@ -46,7 +46,7 @@ Getting Started You need a C++ compiler with C++11 support (up-to-date CLANG or GCC is recommended) and some standard tools such as GNU Flex, GNU Bison, and GNU Make. -TCL, readline and libffi are optional (see ENABLE_* settings in Makefile). +TCL, readline and libffi are optional (see ``ENABLE_*`` settings in Makefile). Xdot (graphviz) is used by the ``show`` command in yosys to display schematics. For example on Ubuntu Linux 16.04 LTS the following commands will install all prerequisites for building yosys: @@ -372,16 +372,17 @@ Verilog Attributes and non-standard features Non-standard or SystemVerilog features for formal verification ============================================================== -- Support for ``assert``, ``assume``, and ``restrict`` is enabled when - ``read_verilog`` is called with ``-formal``. +- Support for ``assert``, ``assume``, ``restrict``, and ``cover'' 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 ``$anyconst`` evaluates to any constant value. This is + equivalent to declaring a reg as ``const rand``. - The system task ``$anyseq`` evaluates to any value, possibly a different - value in each cycle. + value in each cycle. This is equivalent to declaring a reg as ``rand``. - The SystemVerilog tasks ``$past``, ``$stable``, ``$rose`` and ``$fell`` are supported in any clocked block. @@ -400,12 +401,14 @@ 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`` and ``restrict`` statements from SystemVerilog are also - supported. The same limitations as with the ``assert`` statement apply. +- The ``assume``, ``restrict``, and ``cover`` 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. +- Declaring free variables with ``rand`` and ``const rand`` is supported. + - SystemVerilog packages are supported. Once a SystemVerilog file is read into a design with ``read_verilog``, all its packages are available to SystemVerilog files being read into the same design afterwards. diff --git a/backends/smt2/smt2.cc b/backends/smt2/smt2.cc index e0daae728..932f5cd68 100644 --- a/backends/smt2/smt2.cc +++ b/backends/smt2/smt2.cc @@ -662,19 +662,25 @@ struct Smt2Worker if (verbose) log("=> export logic driving asserts\n"); - vector<string> assert_list, assume_list; + vector<string> assert_list, assume_list, cover_list; for (auto cell : module->cells()) - if (cell->type.in("$assert", "$assume")) { + if (cell->type.in("$assert", "$assume", "$cover")) { string name_a = get_bool(cell->getPort("\\A")); string name_en = get_bool(cell->getPort("\\EN")); decls.push_back(stringf("; yosys-smt2-%s %s#%d %s\n", cell->type.c_str() + 1, get_id(module), idcounter, cell->attributes.count("\\src") ? cell->attributes.at("\\src").decode_string().c_str() : get_id(cell))); - decls.push_back(stringf("(define-fun |%s#%d| ((state |%s_s|)) Bool (or %s (not %s))) ; %s\n", - get_id(module), idcounter, get_id(module), name_a.c_str(), name_en.c_str(), get_id(cell))); + if (cell->type == "$cover") + decls.push_back(stringf("(define-fun |%s#%d| ((state |%s_s|)) Bool (and %s %s)) ; %s\n", + get_id(module), idcounter, get_id(module), name_a.c_str(), name_en.c_str(), get_id(cell))); + else + decls.push_back(stringf("(define-fun |%s#%d| ((state |%s_s|)) Bool (or %s (not %s))) ; %s\n", + get_id(module), idcounter, get_id(module), name_a.c_str(), name_en.c_str(), get_id(cell))); if (cell->type == "$assert") assert_list.push_back(stringf("(|%s#%d| state)", get_id(module), idcounter++)); - else + else if (cell->type == "$assume") assume_list.push_back(stringf("(|%s#%d| state)", get_id(module), idcounter++)); + else if (cell->type == "$cover") + cover_list.push_back(stringf("(|%s#%d| state)", get_id(module), idcounter++)); } for (int iter = 1; !registers.empty(); iter++) diff --git a/backends/smt2/smtbmc.py b/backends/smt2/smtbmc.py index ecee6795e..d8b47504c 100644 --- a/backends/smt2/smtbmc.py +++ b/backends/smt2/smtbmc.py @@ -29,11 +29,14 @@ num_steps = 20 append_steps = 0 vcdfile = None cexfile = None -aigprefix = None +aimfile = None +aiwfile = None +aigheader = True vlogtbfile = None inconstr = list() outconstr = None gentrace = False +covermode = False tempind = False dumpall = False assume_skipped = None @@ -59,6 +62,9 @@ yosys-smtbmc [options] <yosys_smt2_output> -i instead of BMC run temporal induction + -c + instead of regular BMC run cover analysis + -m <module_name> name of the top module @@ -73,6 +79,14 @@ yosys-smtbmc [options] <yosys_smt2_output> and AIGER witness file. The file names are <prefix>.aim for the map file and <prefix>.aiw for the witness file. + --aig <aim_filename>:<aiw_filename> + like above, but for map files and witness files that do not + share a filename prefix (or use differen file extensions). + + --aig-noheader + the AIGER witness file does not include the status and + properties lines. + --noinfo only run the core proof, do not collect and print any additional information (e.g. which assert failed) @@ -110,8 +124,8 @@ 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=", "cex=", "aig=", + opts, args = getopt.getopt(sys.argv[1:], so.shortopts + "t:igcm:", so.longopts + + ["final-only", "assume-skipped=", "smtc=", "cex=", "aig=", "aig-noheader", "dump-vcd=", "dump-vlogtb=", "dump-smtc=", "dump-all", "noinfo", "append="]) except: usage() @@ -140,7 +154,13 @@ for o, a in opts: elif o == "--cex": cexfile = a elif o == "--aig": - aigprefix = a + if ":" in a: + aimfile, aiwfile = a.split(":") + else: + aimfile = a + ".aim" + aiwfile = a + ".aiw" + elif o == "--aig-noheader": + aigheader = False elif o == "--dump-vcd": vcdfile = a elif o == "--dump-vlogtb": @@ -157,6 +177,8 @@ for o, a in opts: tempind = True elif o == "-g": gentrace = True + elif o == "-c": + covermode = True elif o == "-m": topmod = a elif so.handle(o, a): @@ -167,6 +189,8 @@ for o, a in opts: if len(args) != 1: usage() +if sum([tempind, gentrace, covermode]) > 1: + usage() constr_final_start = None constr_asserts = defaultdict(list) @@ -375,7 +399,7 @@ if cexfile is not None: skip_steps = max(skip_steps, step) num_steps = max(num_steps, step+1) -if aigprefix is not None: +if aimfile is not None: input_map = dict() init_map = dict() latch_map = dict() @@ -385,7 +409,7 @@ if aigprefix is not None: skip_steps = 0 num_steps = 0 - with open(aigprefix + ".aim", "r") as f: + with open(aimfile, "r") as f: for entry in f.read().splitlines(): entry = entry.split() @@ -406,11 +430,14 @@ if aigprefix is not None: assert False - with open(aigprefix + ".aiw", "r") as f: + with open(aiwfile, "r") as f: got_state = False got_ffinit = False step = 0 + if not aigheader: + got_state = True + for entry in f.read().splitlines(): if len(entry) == 0 or entry[0] in "bcjfu.": continue @@ -458,13 +485,30 @@ if aigprefix is not None: bitidx = init_map[i][1] path = smt.get_path(topmod, name) - width = smt.net_width(topmod, path) + + if not smt.net_exists(topmod, path): + match = re.match(r"(.*)\[(\d+)\]$", path[-1]) + if match: + path[-1] = match.group(1) + addr = int(match.group(2)) + + if not match or not smt.mem_exists(topmod, path): + print_msg("Ignoring init value for unknown net: %s" % (name)) + continue + + meminfo = smt.mem_info(topmod, path) + smtexpr = "(select [%s] #b%s)" % (".".join(path), bin(addr)[2:].zfill(meminfo[0])) + width = meminfo[1] + + else: + smtexpr = "[%s]" % name + width = smt.net_width(topmod, path) if width == 1: assert bitidx == 0 - smtexpr = "(= [%s] %s)" % (name, "true" if value else "false") + smtexpr = "(= %s %s)" % (smtexpr, "true" if value else "false") else: - smtexpr = "(= ((_ extract %d %d) [%s]) #b%d)" % (bitidx, bitidx, name, value) + smtexpr = "(= ((_ extract %d %d) %s) #b%d)" % (bitidx, bitidx, smtexpr, value) constr_assumes[0].append((cexfile, smtexpr)) @@ -569,7 +613,7 @@ def write_vlogtb_trace(steps_start, steps_stop, index): mems = sorted(smt.hiermems(topmod)) for mempath in mems: - abits, width, ports = smt.mem_info(topmod, "s%d" % steps_start, mempath) + abits, width, ports = smt.mem_info(topmod, mempath) mem = smt.mem_expr(topmod, "s%d" % steps_start, mempath) addr_expr_list = list() @@ -630,7 +674,7 @@ def write_constr_trace(steps_start, steps_stop, index): mems = sorted(smt.hiermems(topmod)) for mempath in mems: - abits, width, ports = smt.mem_info(topmod, "s%d" % steps_start, mempath) + abits, width, ports = smt.mem_info(topmod, mempath) mem = smt.mem_expr(topmod, "s%d" % steps_start, mempath) addr_expr_list = list() @@ -669,30 +713,40 @@ def write_trace(steps_start, steps_stop, index): write_constr_trace(steps_start, steps_stop, index) -def print_failed_asserts_worker(mod, state, path): +def print_failed_asserts_worker(mod, state, path, extrainfo): assert mod in smt.modinfo + found_failed_assert = False if smt.get("(|%s_a| %s)" % (mod, state)) in ["true", "#b1"]: return for cellname, celltype in smt.modinfo[mod].cells.items(): - print_failed_asserts_worker(celltype, "(|%s_h %s| %s)" % (mod, cellname, state), path + "." + cellname) + if print_failed_asserts_worker(celltype, "(|%s_h %s| %s)" % (mod, cellname, state), path + "." + cellname, extrainfo): + found_failed_assert = True for assertfun, assertinfo in smt.modinfo[mod].asserts.items(): if smt.get("(|%s| %s)" % (assertfun, state)) in ["false", "#b0"]: - print_msg("Assert failed in %s: %s" % (path, assertinfo)) + print_msg("Assert failed in %s: %s%s" % (path, assertinfo, extrainfo)) + found_failed_assert = True + return found_failed_assert -def print_failed_asserts(state, final=False): + +def print_failed_asserts(state, final=False, extrainfo=""): if noinfo: return loc_list, expr_list, value_list = get_constr_expr(constr_asserts, state, final=final, getvalues=True) + found_failed_assert = False for loc, expr, value in zip(loc_list, expr_list, value_list): if smt.bv2int(value) == 0: - print_msg("Assert %s failed: %s" % (loc, expr)) + print_msg("Assert %s failed: %s%s" % (loc, expr, extrainfo)) + found_failed_assert = True if not final: - print_failed_asserts_worker(topmod, "s%d" % state, topmod) + if print_failed_asserts_worker(topmod, "s%d" % state, topmod, extrainfo): + found_failed_assert = True + + return found_failed_assert def print_anyconsts_worker(mod, state, path): @@ -710,6 +764,24 @@ def print_anyconsts(state): print_anyconsts_worker(topmod, "s%d" % state, topmod) +def get_cover_list(mod, base): + assert mod in smt.modinfo + + cover_expr = list() + cover_desc = list() + + for expr, desc in smt.modinfo[mod].covers.items(): + cover_expr.append("(ite (|%s| %s) #b1 #b0)" % (expr, base)) + cover_desc.append(desc) + + for cell, submod in smt.modinfo[mod].cells.items(): + e, d = get_cover_list(submod, "(|%s_h %s| %s)" % (mod, cell, base)) + cover_expr += e + cover_desc += d + + return cover_expr, cover_desc + + if tempind: retstatus = False skip_counter = step_size @@ -757,8 +829,92 @@ if tempind: retstatus = True break +elif covermode: + cover_expr, cover_desc = get_cover_list(topmod, "state") + cover_mask = "1" * len(cover_desc) + + if len(cover_expr) > 1: + cover_expr = "(concat %s)" % " ".join(cover_expr) + elif len(cover_expr) == 1: + cover_expr = cover_expr[0] + else: + cover_expr = "#b0" + + coveridx = 0 + smt.write("(define-fun covers_0 ((state |%s_s|)) (_ BitVec %d) %s)" % (topmod, len(cover_desc), cover_expr)) + + step = 0 + retstatus = False + found_failed_assert = False + + assert step_size == 1 + + while step < num_steps: + smt.write("(declare-fun s%d () |%s_s|)" % (step, topmod)) + smt.write("(assert (|%s_u| s%d))" % (topmod, step)) + smt.write("(assert (|%s_h| s%d))" % (topmod, step)) + smt.write("(assert %s)" % get_constr_expr(constr_assumes, step)) + + if step == 0: + smt.write("(assert (|%s_i| s0))" % (topmod)) + smt.write("(assert (|%s_is| s0))" % (topmod)) + + else: + smt.write("(assert (|%s_t| s%d s%d))" % (topmod, step-1, step)) + smt.write("(assert (not (|%s_is| s%d)))" % (topmod, step)) + + while "1" in cover_mask: + print_msg("Checking cover reachability in step %d.." % (step)) + smt.write("(push 1)") + smt.write("(assert (distinct (covers_%d s%d) #b%s))" % (coveridx, step, "0" * len(cover_desc))) + + if smt.check_sat() == "unsat": + smt.write("(pop 1)") + break + + reached_covers = smt.bv2bin(smt.get("(covers_%d s%d)" % (coveridx, step))) + assert len(reached_covers) == len(cover_desc) + + new_cover_mask = [] + + for i in range(len(reached_covers)): + if reached_covers[i] == "0": + new_cover_mask.append(cover_mask[i]) + continue + + print_msg("Reached cover statement at %s in step %d." % (cover_desc[i], step)) + new_cover_mask.append("0") + + cover_mask = "".join(new_cover_mask) + + for i in range(step+1): + if print_failed_asserts(i, extrainfo=" (step %d)" % i): + found_failed_assert = True + + write_trace(0, step+1, "%d" % coveridx) + + if found_failed_assert: + break + + coveridx += 1 + smt.write("(pop 1)") + smt.write("(define-fun covers_%d ((state |%s_s|)) (_ BitVec %d) (bvand (covers_%d state) #b%s))" % (coveridx, topmod, len(cover_desc), coveridx-1, cover_mask)) + + if found_failed_assert: + break + + if "1" not in cover_mask: + retstatus = True + break + + step += 1 + + if "1" in cover_mask: + for i in range(len(cover_mask)): + if cover_mask[i] == "1": + print_msg("Unreached cover statement at %s." % cover_desc[i]) -else: # not tempind +else: # not tempind, covermode step = 0 retstatus = True while step < num_steps: diff --git a/backends/smt2/smtio.py b/backends/smt2/smtio.py index 497b72db8..dda804efb 100644 --- a/backends/smt2/smtio.py +++ b/backends/smt2/smtio.py @@ -42,6 +42,7 @@ class SmtModInfo: self.wsize = dict() self.cells = dict() self.asserts = dict() + self.covers = dict() self.anyconsts = dict() @@ -331,6 +332,9 @@ class SmtIo: if fields[1] == "yosys-smt2-assert": self.modinfo[self.curmod].asserts[fields[2]] = fields[3] + if fields[1] == "yosys-smt2-cover": + self.modinfo[self.curmod].covers[fields[2]] = fields[3] + if fields[1] == "yosys-smt2-anyconst": self.modinfo[self.curmod].anyconsts[fields[2]] = fields[3] @@ -567,6 +571,26 @@ class SmtIo: assert net_path[-1] in self.modinfo[mod].wsize return self.modinfo[mod].wsize[net_path[-1]] + def net_exists(self, mod, net_path): + for i in range(len(net_path)-1): + if mod not in self.modinfo: return False + if net_path[i] not in self.modinfo[mod].cells: return False + mod = self.modinfo[mod].cells[net_path[i]] + + if mod not in self.modinfo: return False + if net_path[-1] not in self.modinfo[mod].wsize: return False + return True + + def mem_exists(self, mod, mem_path): + for i in range(len(mem_path)-1): + if mod not in self.modinfo: return False + if mem_path[i] not in self.modinfo[mod].cells: return False + mod = self.modinfo[mod].cells[mem_path[i]] + + if mod not in self.modinfo: return False + if mem_path[-1] not in self.modinfo[mod].memories: return False + return True + def mem_expr(self, mod, base, path, portidx=None, infomode=False): if len(path) == 1: assert mod in self.modinfo @@ -582,8 +606,8 @@ class SmtIo: nextbase = "(|%s_h %s| %s)" % (mod, path[0], base) return self.mem_expr(nextmod, nextbase, path[1:], portidx=portidx, infomode=infomode) - def mem_info(self, mod, base, path): - return self.mem_expr(mod, base, path, infomode=True) + def mem_info(self, mod, path): + return self.mem_expr(mod, "", path, infomode=True) def get_net(self, mod_name, net_path, state_name): return self.get(self.net_expr(mod_name, state_name, net_path)) diff --git a/frontends/ast/ast.cc b/frontends/ast/ast.cc index 2d58c682f..38a19a36f 100644 --- a/frontends/ast/ast.cc +++ b/frontends/ast/ast.cc @@ -84,6 +84,7 @@ std::string AST::type2str(AstNodeType type) X(AST_PREFIX) X(AST_ASSERT) X(AST_ASSUME) + X(AST_COVER) X(AST_FCALL) X(AST_TO_BITS) X(AST_TO_SIGNED) diff --git a/frontends/ast/ast.h b/frontends/ast/ast.h index cd6e264e6..0b9116d39 100644 --- a/frontends/ast/ast.h +++ b/frontends/ast/ast.h @@ -65,6 +65,7 @@ namespace AST AST_PREFIX, AST_ASSERT, AST_ASSUME, + AST_COVER, AST_FCALL, AST_TO_BITS, diff --git a/frontends/ast/genrtlil.cc b/frontends/ast/genrtlil.cc index db8d7409f..bdac4de00 100644 --- a/frontends/ast/genrtlil.cc +++ b/frontends/ast/genrtlil.cc @@ -1336,9 +1336,11 @@ RTLIL::SigSpec AstNode::genRTLIL(int width_hint, bool sign_hint) // generate $assert cells case AST_ASSERT: case AST_ASSUME: + case AST_COVER: { const char *celltype = "$assert"; if (type == AST_ASSUME) celltype = "$assume"; + if (type == AST_COVER) celltype = "$cover"; log_assert(children.size() == 2); diff --git a/frontends/ast/simplify.cc b/frontends/ast/simplify.cc index c1e77c6ec..eecc04132 100644 --- a/frontends/ast/simplify.cc +++ b/frontends/ast/simplify.cc @@ -1400,7 +1400,7 @@ bool AstNode::simplify(bool const_fold, bool at_zero, bool in_lvalue, int stage, } skip_dynamic_range_lvalue_expansion:; - if (stage > 1 && (type == AST_ASSERT || type == AST_ASSUME) && current_block != NULL) + if (stage > 1 && (type == AST_ASSERT || type == AST_ASSUME || type == AST_COVER) && current_block != NULL) { std::stringstream sstr; sstr << "$formal$" << filename << ":" << linenum << "$" << (autoidx++); @@ -1462,7 +1462,7 @@ skip_dynamic_range_lvalue_expansion:; goto apply_newNode; } - if (stage > 1 && (type == AST_ASSERT || type == AST_ASSUME) && children.size() == 1) + if (stage > 1 && (type == AST_ASSERT || type == AST_ASSUME || type == AST_COVER) && children.size() == 1) { children.push_back(mkconst_int(1, false, 1)); did_something = true; diff --git a/frontends/blif/blifparse.cc b/frontends/blif/blifparse.cc index 6d4d60870..f610a25c3 100644 --- a/frontends/blif/blifparse.cc +++ b/frontends/blif/blifparse.cc @@ -55,7 +55,30 @@ static bool read_next_line(char *&buffer, size_t &buffer_size, int &line_count, } } -void parse_blif(RTLIL::Design *design, std::istream &f, std::string dff_name, bool run_clean, bool sop_mode) +static std::pair<RTLIL::IdString, int> wideports_split(std::string name) +{ + int pos = -1; + + if (name.empty() || name.back() != ']') + goto failed; + + for (int i = 0; i+1 < GetSize(name); i++) { + if (name[i] == '[') + pos = i; + else if (name[i] < '0' || name[i] > '9') + pos = -1; + else if (i == pos+1 && name[i] == '0') + pos = -1; + } + + if (pos >= 0) + return std::pair<RTLIL::IdString, int>("\\" + name.substr(0, pos), atoi(name.c_str() + pos+1)+1); + +failed: + return std::pair<RTLIL::IdString, int>("\\" + name, 0); +} + +void parse_blif(RTLIL::Design *design, std::istream &f, std::string dff_name, bool run_clean, bool sop_mode, bool wideports) { RTLIL::Module *module = nullptr; RTLIL::Const *lutptr = NULL; @@ -96,6 +119,8 @@ void parse_blif(RTLIL::Design *design, std::istream &f, std::string dff_name, bo dict<RTLIL::IdString, RTLIL::Const> *obj_attributes = nullptr; dict<RTLIL::IdString, RTLIL::Const> *obj_parameters = nullptr; + dict<RTLIL::IdString, std::pair<int, bool>> wideports_cache; + size_t buffer_size = 4096; char *buffer = (char*)malloc(buffer_size); int line_count = 0; @@ -148,7 +173,32 @@ void parse_blif(RTLIL::Design *design, std::istream &f, std::string dff_name, bo if (!strcmp(cmd, ".end")) { + for (auto &wp : wideports_cache) + { + auto name = wp.first; + int width = wp.second.first; + bool isinput = wp.second.second; + + RTLIL::Wire *wire = module->addWire(name, width); + wire->port_input = isinput; + wire->port_output = !isinput; + + for (int i = 0; i < width; i++) { + RTLIL::IdString other_name = name.str() + stringf("[%d]", i); + RTLIL::Wire *other_wire = module->wire(other_name); + if (other_wire) { + other_wire->port_input = false; + other_wire->port_output = false; + if (isinput) + module->connect(other_wire, SigSpec(wire, i)); + else + module->connect(SigSpec(wire, i), other_wire); + } + } + } + module->fixup_ports(); + wideports_cache.clear(); if (run_clean) { @@ -187,9 +237,11 @@ void parse_blif(RTLIL::Design *design, std::istream &f, std::string dff_name, bo continue; } - if (!strcmp(cmd, ".inputs") || !strcmp(cmd, ".outputs")) { + if (!strcmp(cmd, ".inputs") || !strcmp(cmd, ".outputs")) + { char *p; - while ((p = strtok(NULL, " \t\r\n")) != NULL) { + while ((p = strtok(NULL, " \t\r\n")) != NULL) + { RTLIL::IdString wire_name(stringf("\\%s", p)); RTLIL::Wire *wire = module->wire(wire_name); if (wire == nullptr) @@ -198,6 +250,14 @@ void parse_blif(RTLIL::Design *design, std::istream &f, std::string dff_name, bo wire->port_input = true; else wire->port_output = true; + + if (wideports) { + std::pair<RTLIL::IdString, int> wp = wideports_split(p); + if (wp.second > 0) { + wideports_cache[wp.first].first = std::max(wideports_cache[wp.first].first, wp.second); + wideports_cache[wp.first].second = !strcmp(cmd, ".inputs"); + } + } } obj_attributes = nullptr; obj_parameters = nullptr; @@ -452,6 +512,8 @@ void parse_blif(RTLIL::Design *design, std::istream &f, std::string dff_name, bo } } + return; + error: log_error("Syntax error in line %d!\n", line_count); } @@ -469,10 +531,15 @@ struct BlifFrontend : public Frontend { log(" -sop\n"); log(" Create $sop cells instead of $lut cells\n"); log("\n"); + log(" -wideports\n"); + log(" Merge ports that match the pattern 'name[int]' into a single\n"); + log(" multi-bit port 'name'.\n"); + log("\n"); } virtual void execute(std::istream *&f, std::string filename, std::vector<std::string> args, RTLIL::Design *design) { bool sop_mode = false; + bool wideports = false; log_header(design, "Executing BLIF frontend.\n"); @@ -483,11 +550,15 @@ struct BlifFrontend : public Frontend { sop_mode = true; continue; } + if (arg == "-wideports") { + wideports = true; + continue; + } break; } extra_args(f, filename, args, argidx); - parse_blif(design, *f, "", true, sop_mode); + parse_blif(design, *f, "", true, sop_mode, wideports); } } BlifFrontend; diff --git a/frontends/blif/blifparse.h b/frontends/blif/blifparse.h index 058087d81..955b6aacf 100644 --- a/frontends/blif/blifparse.h +++ b/frontends/blif/blifparse.h @@ -24,7 +24,8 @@ YOSYS_NAMESPACE_BEGIN -extern void parse_blif(RTLIL::Design *design, std::istream &f, std::string dff_name, bool run_clean = false, bool sop_mode = false); +extern void parse_blif(RTLIL::Design *design, std::istream &f, std::string dff_name, + bool run_clean = false, bool sop_mode = false, bool wideports = false); YOSYS_NAMESPACE_END diff --git a/frontends/verific/build_amd64.txt b/frontends/verific/build_amd64.txt index d6952820e..95d618ecc 100644 --- a/frontends/verific/build_amd64.txt +++ b/frontends/verific/build_amd64.txt @@ -6,7 +6,7 @@ only have the i386 eval version of Verific: 1.) Use a Makefile.conf like the following one: --snip-- -CONFIG := clang +CONFIG := gcc ENABLE_TCL := 0 ENABLE_PLUGINS := 0 ENABLE_VERIFIC := 1 diff --git a/frontends/verific/verific.cc b/frontends/verific/verific.cc index 7dd36a747..f3b997dc5 100644 --- a/frontends/verific/verific.cc +++ b/frontends/verific/verific.cc @@ -49,7 +49,13 @@ USING_YOSYS_NAMESPACE using namespace Verific ; #endif -static void msg_func(msg_type_t msg_type, const char *message_id, linefile_type linefile, const char *msg, va_list args) +#endif + +PRIVATE_NAMESPACE_BEGIN + +#ifdef YOSYS_ENABLE_VERIFIC + +void msg_func(msg_type_t msg_type, const char *message_id, linefile_type linefile, const char *msg, va_list args) { log("VERIFIC-%s [%s] ", msg_type == VERIFIC_NONE ? "NONE" : @@ -65,775 +71,829 @@ static void msg_func(msg_type_t msg_type, const char *message_id, linefile_type log("\n"); } -static void import_attributes(dict<RTLIL::IdString, RTLIL::Const> &attributes, DesignObj *obj) +struct VerificImporter { - MapIter mi; - Att *attr; - - if (obj->Linefile()) - attributes["\\src"] = stringf("%s:%d", LineFile::GetFileName(obj->Linefile()), LineFile::GetLineNo(obj->Linefile())); - - // FIXME: Parse numeric attributes - FOREACH_ATTRIBUTE(obj, mi, attr) - attributes[RTLIL::escape_id(attr->Key())] = RTLIL::Const(std::string(attr->Value())); -} + RTLIL::Module *module; + std::map<Net*, RTLIL::SigBit> net_map; + std::map<Net*, Net*> sva_posedge_map; -static RTLIL::SigSpec operatorInput(Instance *inst, std::map<Net*, RTLIL::SigBit> &net_map) -{ - RTLIL::SigSpec sig; - for (int i = int(inst->InputSize())-1; i >= 0; i--) - if (inst->GetInputBit(i)) - sig.append(net_map.at(inst->GetInputBit(i))); - else - sig.append(RTLIL::State::Sz); - return sig; -} + void import_attributes(dict<RTLIL::IdString, RTLIL::Const> &attributes, DesignObj *obj) + { + MapIter mi; + Att *attr; -static RTLIL::SigSpec operatorInput1(Instance *inst, std::map<Net*, RTLIL::SigBit> &net_map) -{ - RTLIL::SigSpec sig; - for (int i = int(inst->Input1Size())-1; i >= 0; i--) - if (inst->GetInput1Bit(i)) - sig.append(net_map.at(inst->GetInput1Bit(i))); - else - sig.append(RTLIL::State::Sz); - return sig; -} + if (obj->Linefile()) + attributes["\\src"] = stringf("%s:%d", LineFile::GetFileName(obj->Linefile()), LineFile::GetLineNo(obj->Linefile())); -static RTLIL::SigSpec operatorInput2(Instance *inst, std::map<Net*, RTLIL::SigBit> &net_map) -{ - RTLIL::SigSpec sig; - for (int i = int(inst->Input2Size())-1; i >= 0; i--) - if (inst->GetInput2Bit(i)) - sig.append(net_map.at(inst->GetInput2Bit(i))); - else - sig.append(RTLIL::State::Sz); - return sig; -} + // FIXME: Parse numeric attributes + FOREACH_ATTRIBUTE(obj, mi, attr) + attributes[RTLIL::escape_id(attr->Key())] = RTLIL::Const(std::string(attr->Value())); + } -static RTLIL::SigSpec operatorInport(Instance *inst, const char *portname, std::map<Net*, RTLIL::SigBit> &net_map) -{ - PortBus *portbus = inst->View()->GetPortBus(portname); - if (portbus) { + RTLIL::SigSpec operatorInput(Instance *inst) + { RTLIL::SigSpec sig; - for (unsigned i = 0; i < portbus->Size(); i++) { - Net *net = inst->GetNet(portbus->ElementAtIndex(i)); - if (net) { - if (net->IsGnd()) - sig.append(RTLIL::State::S0); - else if (net->IsPwr()) - sig.append(RTLIL::State::S1); - else - sig.append(net_map.at(net)); - } else + for (int i = int(inst->InputSize())-1; i >= 0; i--) + if (inst->GetInputBit(i)) + sig.append(net_map.at(inst->GetInputBit(i))); + else sig.append(RTLIL::State::Sz); - } return sig; - } else { - Port *port = inst->View()->GetPort(portname); - log_assert(port != NULL); - Net *net = inst->GetNet(port); - return net_map.at(net); } -} -static RTLIL::SigSpec operatorOutput(Instance *inst, std::map<Net*, RTLIL::SigBit> &net_map, RTLIL::Module *module) -{ - RTLIL::SigSpec sig; - RTLIL::Wire *dummy_wire = NULL; - for (int i = int(inst->OutputSize())-1; i >= 0; i--) - if (inst->GetOutputBit(i)) { - sig.append(net_map.at(inst->GetOutputBit(i))); - dummy_wire = NULL; - } else { - if (dummy_wire == NULL) - dummy_wire = module->addWire(NEW_ID); + RTLIL::SigSpec operatorInput1(Instance *inst) + { + RTLIL::SigSpec sig; + for (int i = int(inst->Input1Size())-1; i >= 0; i--) + if (inst->GetInput1Bit(i)) + sig.append(net_map.at(inst->GetInput1Bit(i))); else - dummy_wire->width++; - sig.append(RTLIL::SigSpec(dummy_wire, dummy_wire->width - 1)); - } - return sig; -} - -static bool import_netlist_instance_gates(RTLIL::Module *module, std::map<Net*, RTLIL::SigBit> &net_map, Instance *inst) -{ - if (inst->Type() == PRIM_AND) { - module->addAndGate(RTLIL::escape_id(inst->Name()), net_map.at(inst->GetInput1()), net_map.at(inst->GetInput2()), net_map.at(inst->GetOutput())); - return true; - } - - if (inst->Type() == PRIM_NAND) { - RTLIL::SigSpec tmp = module->addWire(NEW_ID); - module->addAndGate(NEW_ID, net_map.at(inst->GetInput1()), net_map.at(inst->GetInput2()), tmp); - module->addNotGate(RTLIL::escape_id(inst->Name()), tmp, net_map.at(inst->GetOutput())); - return true; - } - - if (inst->Type() == PRIM_OR) { - module->addOrGate(RTLIL::escape_id(inst->Name()), net_map.at(inst->GetInput1()), net_map.at(inst->GetInput2()), net_map.at(inst->GetOutput())); - return true; + sig.append(RTLIL::State::Sz); + return sig; } - if (inst->Type() == PRIM_NOR) { - RTLIL::SigSpec tmp = module->addWire(NEW_ID); - module->addOrGate(NEW_ID, net_map.at(inst->GetInput1()), net_map.at(inst->GetInput2()), tmp); - module->addNotGate(RTLIL::escape_id(inst->Name()), tmp, net_map.at(inst->GetOutput())); - return true; + RTLIL::SigSpec operatorInput2(Instance *inst) + { + RTLIL::SigSpec sig; + for (int i = int(inst->Input2Size())-1; i >= 0; i--) + if (inst->GetInput2Bit(i)) + sig.append(net_map.at(inst->GetInput2Bit(i))); + else + sig.append(RTLIL::State::Sz); + return sig; } - if (inst->Type() == PRIM_XOR) { - module->addXorGate(RTLIL::escape_id(inst->Name()), net_map.at(inst->GetInput1()), net_map.at(inst->GetInput2()), net_map.at(inst->GetOutput())); - return true; + RTLIL::SigSpec operatorInport(Instance *inst, const char *portname) + { + PortBus *portbus = inst->View()->GetPortBus(portname); + if (portbus) { + RTLIL::SigSpec sig; + for (unsigned i = 0; i < portbus->Size(); i++) { + Net *net = inst->GetNet(portbus->ElementAtIndex(i)); + if (net) { + if (net->IsGnd()) + sig.append(RTLIL::State::S0); + else if (net->IsPwr()) + sig.append(RTLIL::State::S1); + else + sig.append(net_map.at(net)); + } else + sig.append(RTLIL::State::Sz); + } + return sig; + } else { + Port *port = inst->View()->GetPort(portname); + log_assert(port != NULL); + Net *net = inst->GetNet(port); + return net_map.at(net); + } } - if (inst->Type() == PRIM_XNOR) { - module->addXnorGate(RTLIL::escape_id(inst->Name()), net_map.at(inst->GetInput1()), net_map.at(inst->GetInput2()), net_map.at(inst->GetOutput())); - return true; + RTLIL::SigSpec operatorOutput(Instance *inst) + { + RTLIL::SigSpec sig; + RTLIL::Wire *dummy_wire = NULL; + for (int i = int(inst->OutputSize())-1; i >= 0; i--) + if (inst->GetOutputBit(i)) { + sig.append(net_map.at(inst->GetOutputBit(i))); + dummy_wire = NULL; + } else { + if (dummy_wire == NULL) + dummy_wire = module->addWire(NEW_ID); + else + dummy_wire->width++; + sig.append(RTLIL::SigSpec(dummy_wire, dummy_wire->width - 1)); + } + return sig; } - if (inst->Type() == PRIM_BUF) { - module->addBufGate(RTLIL::escape_id(inst->Name()), net_map.at(inst->GetInput()), net_map.at(inst->GetOutput())); - return true; - } + bool import_netlist_instance_gates(Instance *inst) + { + if (inst->Type() == PRIM_AND) { + module->addAndGate(RTLIL::escape_id(inst->Name()), net_map.at(inst->GetInput1()), net_map.at(inst->GetInput2()), net_map.at(inst->GetOutput())); + return true; + } - if (inst->Type() == PRIM_INV) { - module->addNotGate(RTLIL::escape_id(inst->Name()), net_map.at(inst->GetInput()), net_map.at(inst->GetOutput())); - return true; - } + if (inst->Type() == PRIM_NAND) { + RTLIL::SigSpec tmp = module->addWire(NEW_ID); + module->addAndGate(NEW_ID, net_map.at(inst->GetInput1()), net_map.at(inst->GetInput2()), tmp); + module->addNotGate(RTLIL::escape_id(inst->Name()), tmp, net_map.at(inst->GetOutput())); + return true; + } - if (inst->Type() == PRIM_MUX) { - module->addMuxGate(RTLIL::escape_id(inst->Name()), net_map.at(inst->GetInput1()), net_map.at(inst->GetInput2()), net_map.at(inst->GetControl()), net_map.at(inst->GetOutput())); - return true; - } + if (inst->Type() == PRIM_OR) { + module->addOrGate(RTLIL::escape_id(inst->Name()), net_map.at(inst->GetInput1()), net_map.at(inst->GetInput2()), net_map.at(inst->GetOutput())); + return true; + } - if (inst->Type() == PRIM_TRI) { - module->addMuxGate(RTLIL::escape_id(inst->Name()), RTLIL::State::Sz, net_map.at(inst->GetInput()), net_map.at(inst->GetControl()), net_map.at(inst->GetOutput())); - return true; - } + if (inst->Type() == PRIM_NOR) { + RTLIL::SigSpec tmp = module->addWire(NEW_ID); + module->addOrGate(NEW_ID, net_map.at(inst->GetInput1()), net_map.at(inst->GetInput2()), tmp); + module->addNotGate(RTLIL::escape_id(inst->Name()), tmp, net_map.at(inst->GetOutput())); + return true; + } - if (inst->Type() == PRIM_FADD) - { - RTLIL::SigSpec a = net_map.at(inst->GetInput1()), b = net_map.at(inst->GetInput2()), c = net_map.at(inst->GetCin()); - RTLIL::SigSpec x = inst->GetCout() ? net_map.at(inst->GetCout()) : module->addWire(NEW_ID); - RTLIL::SigSpec y = inst->GetOutput() ? net_map.at(inst->GetOutput()) : module->addWire(NEW_ID); - RTLIL::SigSpec tmp1 = module->addWire(NEW_ID); - RTLIL::SigSpec tmp2 = module->addWire(NEW_ID); - RTLIL::SigSpec tmp3 = module->addWire(NEW_ID); - module->addXorGate(NEW_ID, a, b, tmp1); - module->addXorGate(RTLIL::escape_id(inst->Name()), tmp1, c, y); - module->addAndGate(NEW_ID, tmp1, c, tmp2); - module->addAndGate(NEW_ID, a, b, tmp3); - module->addOrGate(NEW_ID, tmp2, tmp3, x); - return true; - } + if (inst->Type() == PRIM_XOR) { + module->addXorGate(RTLIL::escape_id(inst->Name()), net_map.at(inst->GetInput1()), net_map.at(inst->GetInput2()), net_map.at(inst->GetOutput())); + return true; + } - if (inst->Type() == PRIM_DFFRS) - { - if (inst->GetSet()->IsGnd() && inst->GetReset()->IsGnd()) - module->addDffGate(RTLIL::escape_id(inst->Name()), net_map.at(inst->GetClock()), net_map.at(inst->GetInput()), net_map.at(inst->GetOutput())); - else if (inst->GetSet()->IsGnd()) - module->addAdffGate(RTLIL::escape_id(inst->Name()), net_map.at(inst->GetClock()), net_map.at(inst->GetReset()), - net_map.at(inst->GetInput()), net_map.at(inst->GetOutput()), false); - else if (inst->GetReset()->IsGnd()) - module->addAdffGate(RTLIL::escape_id(inst->Name()), net_map.at(inst->GetClock()), net_map.at(inst->GetSet()), - net_map.at(inst->GetInput()), net_map.at(inst->GetOutput()), true); - else - module->addDffsrGate(RTLIL::escape_id(inst->Name()), net_map.at(inst->GetClock()), net_map.at(inst->GetSet()), net_map.at(inst->GetReset()), - net_map.at(inst->GetInput()), net_map.at(inst->GetOutput())); - return true; - } + if (inst->Type() == PRIM_XNOR) { + module->addXnorGate(RTLIL::escape_id(inst->Name()), net_map.at(inst->GetInput1()), net_map.at(inst->GetInput2()), net_map.at(inst->GetOutput())); + return true; + } - return false; -} + if (inst->Type() == PRIM_BUF) { + module->addBufGate(RTLIL::escape_id(inst->Name()), net_map.at(inst->GetInput()), net_map.at(inst->GetOutput())); + return true; + } -static bool import_netlist_instance_cells(RTLIL::Module *module, std::map<Net*, RTLIL::SigBit> &net_map, Instance *inst) -{ - if (inst->Type() == PRIM_AND) { - module->addAnd(RTLIL::escape_id(inst->Name()), net_map.at(inst->GetInput1()), net_map.at(inst->GetInput2()), net_map.at(inst->GetOutput())); - return true; - } + if (inst->Type() == PRIM_INV) { + module->addNotGate(RTLIL::escape_id(inst->Name()), net_map.at(inst->GetInput()), net_map.at(inst->GetOutput())); + return true; + } - if (inst->Type() == PRIM_NAND) { - RTLIL::SigSpec tmp = module->addWire(NEW_ID); - module->addAnd(NEW_ID, net_map.at(inst->GetInput1()), net_map.at(inst->GetInput2()), tmp); - module->addNot(RTLIL::escape_id(inst->Name()), tmp, net_map.at(inst->GetOutput())); - return true; - } + if (inst->Type() == PRIM_MUX) { + module->addMuxGate(RTLIL::escape_id(inst->Name()), net_map.at(inst->GetInput1()), net_map.at(inst->GetInput2()), net_map.at(inst->GetControl()), net_map.at(inst->GetOutput())); + return true; + } - if (inst->Type() == PRIM_OR) { - module->addOr(RTLIL::escape_id(inst->Name()), net_map.at(inst->GetInput1()), net_map.at(inst->GetInput2()), net_map.at(inst->GetOutput())); - return true; - } + if (inst->Type() == PRIM_TRI) { + module->addMuxGate(RTLIL::escape_id(inst->Name()), RTLIL::State::Sz, net_map.at(inst->GetInput()), net_map.at(inst->GetControl()), net_map.at(inst->GetOutput())); + return true; + } - if (inst->Type() == PRIM_NOR) { - RTLIL::SigSpec tmp = module->addWire(NEW_ID); - module->addOr(NEW_ID, net_map.at(inst->GetInput1()), net_map.at(inst->GetInput2()), tmp); - module->addNot(RTLIL::escape_id(inst->Name()), tmp, net_map.at(inst->GetOutput())); - return true; - } + if (inst->Type() == PRIM_FADD) + { + RTLIL::SigSpec a = net_map.at(inst->GetInput1()), b = net_map.at(inst->GetInput2()), c = net_map.at(inst->GetCin()); + RTLIL::SigSpec x = inst->GetCout() ? net_map.at(inst->GetCout()) : module->addWire(NEW_ID); + RTLIL::SigSpec y = inst->GetOutput() ? net_map.at(inst->GetOutput()) : module->addWire(NEW_ID); + RTLIL::SigSpec tmp1 = module->addWire(NEW_ID); + RTLIL::SigSpec tmp2 = module->addWire(NEW_ID); + RTLIL::SigSpec tmp3 = module->addWire(NEW_ID); + module->addXorGate(NEW_ID, a, b, tmp1); + module->addXorGate(RTLIL::escape_id(inst->Name()), tmp1, c, y); + module->addAndGate(NEW_ID, tmp1, c, tmp2); + module->addAndGate(NEW_ID, a, b, tmp3); + module->addOrGate(NEW_ID, tmp2, tmp3, x); + return true; + } - if (inst->Type() == PRIM_XOR) { - module->addXor(RTLIL::escape_id(inst->Name()), net_map.at(inst->GetInput1()), net_map.at(inst->GetInput2()), net_map.at(inst->GetOutput())); - return true; - } + if (inst->Type() == PRIM_DFFRS) + { + if (inst->GetSet()->IsGnd() && inst->GetReset()->IsGnd()) + module->addDffGate(RTLIL::escape_id(inst->Name()), net_map.at(inst->GetClock()), net_map.at(inst->GetInput()), net_map.at(inst->GetOutput())); + else if (inst->GetSet()->IsGnd()) + module->addAdffGate(RTLIL::escape_id(inst->Name()), net_map.at(inst->GetClock()), net_map.at(inst->GetReset()), + net_map.at(inst->GetInput()), net_map.at(inst->GetOutput()), false); + else if (inst->GetReset()->IsGnd()) + module->addAdffGate(RTLIL::escape_id(inst->Name()), net_map.at(inst->GetClock()), net_map.at(inst->GetSet()), + net_map.at(inst->GetInput()), net_map.at(inst->GetOutput()), true); + else + module->addDffsrGate(RTLIL::escape_id(inst->Name()), net_map.at(inst->GetClock()), net_map.at(inst->GetSet()), net_map.at(inst->GetReset()), + net_map.at(inst->GetInput()), net_map.at(inst->GetOutput())); + return true; + } - if (inst->Type() == PRIM_XNOR) { - module->addXnor(RTLIL::escape_id(inst->Name()), net_map.at(inst->GetInput1()), net_map.at(inst->GetInput2()), net_map.at(inst->GetOutput())); - return true; + return false; } - if (inst->Type() == PRIM_INV) { - module->addNot(RTLIL::escape_id(inst->Name()), net_map.at(inst->GetInput()), net_map.at(inst->GetOutput())); - return true; - } + bool import_netlist_instance_cells(Instance *inst) + { + if (inst->Type() == PRIM_AND) { + module->addAnd(RTLIL::escape_id(inst->Name()), net_map.at(inst->GetInput1()), net_map.at(inst->GetInput2()), net_map.at(inst->GetOutput())); + return true; + } - if (inst->Type() == PRIM_MUX) { - module->addMux(RTLIL::escape_id(inst->Name()), net_map.at(inst->GetInput1()), net_map.at(inst->GetInput2()), net_map.at(inst->GetControl()), net_map.at(inst->GetOutput())); - return true; - } + if (inst->Type() == PRIM_NAND) { + RTLIL::SigSpec tmp = module->addWire(NEW_ID); + module->addAnd(NEW_ID, net_map.at(inst->GetInput1()), net_map.at(inst->GetInput2()), tmp); + module->addNot(RTLIL::escape_id(inst->Name()), tmp, net_map.at(inst->GetOutput())); + return true; + } - if (inst->Type() == PRIM_TRI) { - module->addMux(RTLIL::escape_id(inst->Name()), RTLIL::State::Sz, net_map.at(inst->GetInput()), net_map.at(inst->GetControl()), net_map.at(inst->GetOutput())); - return true; - } + if (inst->Type() == PRIM_OR) { + module->addOr(RTLIL::escape_id(inst->Name()), net_map.at(inst->GetInput1()), net_map.at(inst->GetInput2()), net_map.at(inst->GetOutput())); + return true; + } - if (inst->Type() == PRIM_FADD) - { - RTLIL::SigSpec a_plus_b = module->addWire(NEW_ID, 2); - RTLIL::SigSpec y = inst->GetOutput() ? net_map.at(inst->GetOutput()) : module->addWire(NEW_ID); - if (inst->GetCout()) - y.append(net_map.at(inst->GetCout())); - module->addAdd(NEW_ID, net_map.at(inst->GetInput1()), net_map.at(inst->GetInput2()), a_plus_b); - module->addAdd(RTLIL::escape_id(inst->Name()), a_plus_b, net_map.at(inst->GetCin()), y); - return true; - } + if (inst->Type() == PRIM_NOR) { + RTLIL::SigSpec tmp = module->addWire(NEW_ID); + module->addOr(NEW_ID, net_map.at(inst->GetInput1()), net_map.at(inst->GetInput2()), tmp); + module->addNot(RTLIL::escape_id(inst->Name()), tmp, net_map.at(inst->GetOutput())); + return true; + } - if (inst->Type() == PRIM_DFFRS) - { - if (inst->GetSet()->IsGnd() && inst->GetReset()->IsGnd()) - module->addDff(RTLIL::escape_id(inst->Name()), net_map.at(inst->GetClock()), net_map.at(inst->GetInput()), net_map.at(inst->GetOutput())); - else if (inst->GetSet()->IsGnd()) - module->addAdff(RTLIL::escape_id(inst->Name()), net_map.at(inst->GetClock()), net_map.at(inst->GetReset()), - net_map.at(inst->GetInput()), net_map.at(inst->GetOutput()), RTLIL::State::S0); - else if (inst->GetReset()->IsGnd()) - module->addAdff(RTLIL::escape_id(inst->Name()), net_map.at(inst->GetClock()), net_map.at(inst->GetSet()), - net_map.at(inst->GetInput()), net_map.at(inst->GetOutput()), RTLIL::State::S1); - else - module->addDffsr(RTLIL::escape_id(inst->Name()), net_map.at(inst->GetClock()), net_map.at(inst->GetSet()), net_map.at(inst->GetReset()), - net_map.at(inst->GetInput()), net_map.at(inst->GetOutput())); - return true; - } + if (inst->Type() == PRIM_XOR) { + module->addXor(RTLIL::escape_id(inst->Name()), net_map.at(inst->GetInput1()), net_map.at(inst->GetInput2()), net_map.at(inst->GetOutput())); + return true; + } - if (inst->Type() == PRIM_DLATCHRS) - { - if (inst->GetSet()->IsGnd() && inst->GetReset()->IsGnd()) - module->addDlatch(RTLIL::escape_id(inst->Name()), net_map.at(inst->GetControl()), net_map.at(inst->GetInput()), net_map.at(inst->GetOutput())); - else - module->addDlatchsr(RTLIL::escape_id(inst->Name()), net_map.at(inst->GetControl()), net_map.at(inst->GetSet()), net_map.at(inst->GetReset()), - net_map.at(inst->GetInput()), net_map.at(inst->GetOutput())); - return true; - } + if (inst->Type() == PRIM_XNOR) { + module->addXnor(RTLIL::escape_id(inst->Name()), net_map.at(inst->GetInput1()), net_map.at(inst->GetInput2()), net_map.at(inst->GetOutput())); + return true; + } - #define IN operatorInput(inst, net_map) - #define IN1 operatorInput1(inst, net_map) - #define IN2 operatorInput2(inst, net_map) - #define OUT operatorOutput(inst, net_map, module) - #define SIGNED inst->View()->IsSigned() - - if (inst->Type() == OPER_ADDER) { - RTLIL::SigSpec out = OUT; - if (inst->GetCout() != NULL) - out.append(net_map.at(inst->GetCout())); - if (inst->GetCin()->IsGnd()) { - module->addAdd(RTLIL::escape_id(inst->Name()), IN1, IN2, out, SIGNED); - } else { - RTLIL::SigSpec tmp = module->addWire(NEW_ID, GetSize(out)); - module->addAdd(NEW_ID, IN1, IN2, tmp, SIGNED); - module->addAdd(RTLIL::escape_id(inst->Name()), tmp, net_map.at(inst->GetCin()), out, false); + if (inst->Type() == PRIM_INV) { + module->addNot(RTLIL::escape_id(inst->Name()), net_map.at(inst->GetInput()), net_map.at(inst->GetOutput())); + return true; } - return true; - } - if (inst->Type() == OPER_MULTIPLIER) { - module->addMul(RTLIL::escape_id(inst->Name()), IN1, IN2, OUT, SIGNED); - return true; - } + if (inst->Type() == PRIM_MUX) { + module->addMux(RTLIL::escape_id(inst->Name()), net_map.at(inst->GetInput1()), net_map.at(inst->GetInput2()), net_map.at(inst->GetControl()), net_map.at(inst->GetOutput())); + return true; + } - if (inst->Type() == OPER_DIVIDER) { - module->addDiv(RTLIL::escape_id(inst->Name()), IN1, IN2, OUT, SIGNED); - return true; - } + if (inst->Type() == PRIM_TRI) { + module->addMux(RTLIL::escape_id(inst->Name()), RTLIL::State::Sz, net_map.at(inst->GetInput()), net_map.at(inst->GetControl()), net_map.at(inst->GetOutput())); + return true; + } - if (inst->Type() == OPER_MODULO) { - module->addMod(RTLIL::escape_id(inst->Name()), IN1, IN2, OUT, SIGNED); - return true; - } + if (inst->Type() == PRIM_FADD) + { + RTLIL::SigSpec a_plus_b = module->addWire(NEW_ID, 2); + RTLIL::SigSpec y = inst->GetOutput() ? net_map.at(inst->GetOutput()) : module->addWire(NEW_ID); + if (inst->GetCout()) + y.append(net_map.at(inst->GetCout())); + module->addAdd(NEW_ID, net_map.at(inst->GetInput1()), net_map.at(inst->GetInput2()), a_plus_b); + module->addAdd(RTLIL::escape_id(inst->Name()), a_plus_b, net_map.at(inst->GetCin()), y); + return true; + } - if (inst->Type() == OPER_REMAINDER) { - module->addMod(RTLIL::escape_id(inst->Name()), IN1, IN2, OUT, SIGNED); - return true; - } + if (inst->Type() == PRIM_DFFRS) + { + if (inst->GetSet()->IsGnd() && inst->GetReset()->IsGnd()) + module->addDff(RTLIL::escape_id(inst->Name()), net_map.at(inst->GetClock()), net_map.at(inst->GetInput()), net_map.at(inst->GetOutput())); + else if (inst->GetSet()->IsGnd()) + module->addAdff(RTLIL::escape_id(inst->Name()), net_map.at(inst->GetClock()), net_map.at(inst->GetReset()), + net_map.at(inst->GetInput()), net_map.at(inst->GetOutput()), RTLIL::State::S0); + else if (inst->GetReset()->IsGnd()) + module->addAdff(RTLIL::escape_id(inst->Name()), net_map.at(inst->GetClock()), net_map.at(inst->GetSet()), + net_map.at(inst->GetInput()), net_map.at(inst->GetOutput()), RTLIL::State::S1); + else + module->addDffsr(RTLIL::escape_id(inst->Name()), net_map.at(inst->GetClock()), net_map.at(inst->GetSet()), net_map.at(inst->GetReset()), + net_map.at(inst->GetInput()), net_map.at(inst->GetOutput())); + return true; + } - if (inst->Type() == OPER_SHIFT_LEFT) { - module->addShl(RTLIL::escape_id(inst->Name()), IN1, IN2, OUT, false); - return true; - } + if (inst->Type() == PRIM_DLATCHRS) + { + if (inst->GetSet()->IsGnd() && inst->GetReset()->IsGnd()) + module->addDlatch(RTLIL::escape_id(inst->Name()), net_map.at(inst->GetControl()), net_map.at(inst->GetInput()), net_map.at(inst->GetOutput())); + else + module->addDlatchsr(RTLIL::escape_id(inst->Name()), net_map.at(inst->GetControl()), net_map.at(inst->GetSet()), net_map.at(inst->GetReset()), + net_map.at(inst->GetInput()), net_map.at(inst->GetOutput())); + return true; + } - if (inst->Type() == OPER_ENABLED_DECODER) { - RTLIL::SigSpec vec; - vec.append(net_map.at(inst->GetControl())); - for (unsigned i = 1; i < inst->OutputSize(); i++) { - vec.append(RTLIL::State::S0); + #define IN operatorInput(inst) + #define IN1 operatorInput1(inst) + #define IN2 operatorInput2(inst) + #define OUT operatorOutput(inst) + #define SIGNED inst->View()->IsSigned() + + if (inst->Type() == OPER_ADDER) { + RTLIL::SigSpec out = OUT; + if (inst->GetCout() != NULL) + out.append(net_map.at(inst->GetCout())); + if (inst->GetCin()->IsGnd()) { + module->addAdd(RTLIL::escape_id(inst->Name()), IN1, IN2, out, SIGNED); + } else { + RTLIL::SigSpec tmp = module->addWire(NEW_ID, GetSize(out)); + module->addAdd(NEW_ID, IN1, IN2, tmp, SIGNED); + module->addAdd(RTLIL::escape_id(inst->Name()), tmp, net_map.at(inst->GetCin()), out, false); + } + return true; } - module->addShl(RTLIL::escape_id(inst->Name()), vec, IN, OUT, false); - return true; - } - if (inst->Type() == OPER_DECODER) { - RTLIL::SigSpec vec; - vec.append(RTLIL::State::S1); - for (unsigned i = 1; i < inst->OutputSize(); i++) { - vec.append(RTLIL::State::S0); + if (inst->Type() == OPER_MULTIPLIER) { + module->addMul(RTLIL::escape_id(inst->Name()), IN1, IN2, OUT, SIGNED); + return true; } - module->addShl(RTLIL::escape_id(inst->Name()), vec, IN, OUT, false); - return true; - } - if (inst->Type() == OPER_SHIFT_RIGHT) { - Net *net_cin = inst->GetCin(); - Net *net_a_msb = inst->GetInput1Bit(0); - if (net_cin->IsGnd()) - module->addShr(RTLIL::escape_id(inst->Name()), IN1, IN2, OUT, false); - else if (net_cin == net_a_msb) - module->addSshr(RTLIL::escape_id(inst->Name()), IN1, IN2, OUT, true); - else - log_error("Can't import Verific OPER_SHIFT_RIGHT instance %s: carry_in is neither 0 nor msb of left input\n", inst->Name()); - return true; - } + if (inst->Type() == OPER_DIVIDER) { + module->addDiv(RTLIL::escape_id(inst->Name()), IN1, IN2, OUT, SIGNED); + return true; + } - if (inst->Type() == OPER_REDUCE_AND) { - module->addReduceAnd(RTLIL::escape_id(inst->Name()), IN, net_map.at(inst->GetOutput()), SIGNED); - return true; - } + if (inst->Type() == OPER_MODULO) { + module->addMod(RTLIL::escape_id(inst->Name()), IN1, IN2, OUT, SIGNED); + return true; + } - if (inst->Type() == OPER_REDUCE_OR) { - module->addReduceOr(RTLIL::escape_id(inst->Name()), IN, net_map.at(inst->GetOutput()), SIGNED); - return true; - } + if (inst->Type() == OPER_REMAINDER) { + module->addMod(RTLIL::escape_id(inst->Name()), IN1, IN2, OUT, SIGNED); + return true; + } - if (inst->Type() == OPER_REDUCE_XOR) { - module->addReduceXor(RTLIL::escape_id(inst->Name()), IN, net_map.at(inst->GetOutput()), SIGNED); - return true; - } + if (inst->Type() == OPER_SHIFT_LEFT) { + module->addShl(RTLIL::escape_id(inst->Name()), IN1, IN2, OUT, false); + return true; + } - if (inst->Type() == OPER_REDUCE_XNOR) { - module->addReduceXnor(RTLIL::escape_id(inst->Name()), IN, net_map.at(inst->GetOutput()), SIGNED); - return true; - } + if (inst->Type() == OPER_ENABLED_DECODER) { + RTLIL::SigSpec vec; + vec.append(net_map.at(inst->GetControl())); + for (unsigned i = 1; i < inst->OutputSize(); i++) { + vec.append(RTLIL::State::S0); + } + module->addShl(RTLIL::escape_id(inst->Name()), vec, IN, OUT, false); + return true; + } - if (inst->Type() == OPER_LESSTHAN) { - Net *net_cin = inst->GetCin(); - if (net_cin->IsGnd()) - module->addLt(RTLIL::escape_id(inst->Name()), IN1, IN2, net_map.at(inst->GetOutput()), SIGNED); - else if (net_cin->IsPwr()) - module->addLe(RTLIL::escape_id(inst->Name()), IN1, IN2, net_map.at(inst->GetOutput()), SIGNED); - else - log_error("Can't import Verific OPER_LESSTHAN instance %s: carry_in is neither 0 nor 1\n", inst->Name()); - return true; - } + if (inst->Type() == OPER_DECODER) { + RTLIL::SigSpec vec; + vec.append(RTLIL::State::S1); + for (unsigned i = 1; i < inst->OutputSize(); i++) { + vec.append(RTLIL::State::S0); + } + module->addShl(RTLIL::escape_id(inst->Name()), vec, IN, OUT, false); + return true; + } - if (inst->Type() == OPER_WIDE_AND) { - module->addAnd(RTLIL::escape_id(inst->Name()), IN1, IN2, OUT, SIGNED); - return true; - } + if (inst->Type() == OPER_SHIFT_RIGHT) { + Net *net_cin = inst->GetCin(); + Net *net_a_msb = inst->GetInput1Bit(0); + if (net_cin->IsGnd()) + module->addShr(RTLIL::escape_id(inst->Name()), IN1, IN2, OUT, false); + else if (net_cin == net_a_msb) + module->addSshr(RTLIL::escape_id(inst->Name()), IN1, IN2, OUT, true); + else + log_error("Can't import Verific OPER_SHIFT_RIGHT instance %s: carry_in is neither 0 nor msb of left input\n", inst->Name()); + return true; + } - if (inst->Type() == OPER_WIDE_OR) { - module->addOr(RTLIL::escape_id(inst->Name()), IN1, IN2, OUT, SIGNED); - return true; - } + if (inst->Type() == OPER_REDUCE_AND) { + module->addReduceAnd(RTLIL::escape_id(inst->Name()), IN, net_map.at(inst->GetOutput()), SIGNED); + return true; + } - if (inst->Type() == OPER_WIDE_XOR) { - module->addXor(RTLIL::escape_id(inst->Name()), IN1, IN2, OUT, SIGNED); - return true; - } + if (inst->Type() == OPER_REDUCE_OR) { + module->addReduceOr(RTLIL::escape_id(inst->Name()), IN, net_map.at(inst->GetOutput()), SIGNED); + return true; + } - if (inst->Type() == OPER_WIDE_XNOR) { - module->addXnor(RTLIL::escape_id(inst->Name()), IN1, IN2, OUT, SIGNED); - return true; - } + if (inst->Type() == OPER_REDUCE_XOR) { + module->addReduceXor(RTLIL::escape_id(inst->Name()), IN, net_map.at(inst->GetOutput()), SIGNED); + return true; + } - if (inst->Type() == OPER_WIDE_BUF) { - module->addPos(RTLIL::escape_id(inst->Name()), IN, OUT, SIGNED); - return true; - } + if (inst->Type() == OPER_REDUCE_XNOR) { + module->addReduceXnor(RTLIL::escape_id(inst->Name()), IN, net_map.at(inst->GetOutput()), SIGNED); + return true; + } - if (inst->Type() == OPER_WIDE_INV) { - module->addNot(RTLIL::escape_id(inst->Name()), IN, OUT, SIGNED); - return true; - } + if (inst->Type() == OPER_LESSTHAN) { + Net *net_cin = inst->GetCin(); + if (net_cin->IsGnd()) + module->addLt(RTLIL::escape_id(inst->Name()), IN1, IN2, net_map.at(inst->GetOutput()), SIGNED); + else if (net_cin->IsPwr()) + module->addLe(RTLIL::escape_id(inst->Name()), IN1, IN2, net_map.at(inst->GetOutput()), SIGNED); + else + log_error("Can't import Verific OPER_LESSTHAN instance %s: carry_in is neither 0 nor 1\n", inst->Name()); + return true; + } - if (inst->Type() == OPER_MINUS) { - module->addSub(RTLIL::escape_id(inst->Name()), IN1, IN2, OUT, SIGNED); - return true; - } + if (inst->Type() == OPER_WIDE_AND) { + module->addAnd(RTLIL::escape_id(inst->Name()), IN1, IN2, OUT, SIGNED); + return true; + } - if (inst->Type() == OPER_UMINUS) { - module->addNeg(RTLIL::escape_id(inst->Name()), IN, OUT, SIGNED); - return true; - } + if (inst->Type() == OPER_WIDE_OR) { + module->addOr(RTLIL::escape_id(inst->Name()), IN1, IN2, OUT, SIGNED); + return true; + } - if (inst->Type() == OPER_EQUAL) { - module->addEq(RTLIL::escape_id(inst->Name()), IN1, IN2, net_map.at(inst->GetOutput()), SIGNED); - return true; - } + if (inst->Type() == OPER_WIDE_XOR) { + module->addXor(RTLIL::escape_id(inst->Name()), IN1, IN2, OUT, SIGNED); + return true; + } - if (inst->Type() == OPER_NEQUAL) { - module->addNe(RTLIL::escape_id(inst->Name()), IN1, IN2, net_map.at(inst->GetOutput()), SIGNED); - return true; - } + if (inst->Type() == OPER_WIDE_XNOR) { + module->addXnor(RTLIL::escape_id(inst->Name()), IN1, IN2, OUT, SIGNED); + return true; + } - if (inst->Type() == OPER_WIDE_MUX) { - module->addMux(RTLIL::escape_id(inst->Name()), IN1, IN2, net_map.at(inst->GetControl()), OUT); - return true; - } + if (inst->Type() == OPER_WIDE_BUF) { + module->addPos(RTLIL::escape_id(inst->Name()), IN, OUT, SIGNED); + return true; + } - if (inst->Type() == OPER_WIDE_TRI) { - module->addMux(RTLIL::escape_id(inst->Name()), RTLIL::SigSpec(RTLIL::State::Sz, inst->OutputSize()), IN, net_map.at(inst->GetControl()), OUT); - return true; - } + if (inst->Type() == OPER_WIDE_INV) { + module->addNot(RTLIL::escape_id(inst->Name()), IN, OUT, SIGNED); + return true; + } - if (inst->Type() == OPER_WIDE_DFFRS) { - RTLIL::SigSpec sig_set = operatorInport(inst, "set", net_map); - RTLIL::SigSpec sig_reset = operatorInport(inst, "reset", net_map); - if (sig_set.is_fully_const() && !sig_set.as_bool() && sig_reset.is_fully_const() && !sig_reset.as_bool()) - module->addDff(RTLIL::escape_id(inst->Name()), net_map.at(inst->GetClock()), IN, OUT); - else - module->addDffsr(RTLIL::escape_id(inst->Name()), net_map.at(inst->GetClock()), sig_set, sig_reset, IN, OUT); - return true; - } + if (inst->Type() == OPER_MINUS) { + module->addSub(RTLIL::escape_id(inst->Name()), IN1, IN2, OUT, SIGNED); + return true; + } - #undef IN - #undef IN1 - #undef IN2 - #undef OUT - #undef SIGNED + if (inst->Type() == OPER_UMINUS) { + module->addNeg(RTLIL::escape_id(inst->Name()), IN, OUT, SIGNED); + return true; + } - return false; -} + if (inst->Type() == OPER_EQUAL) { + module->addEq(RTLIL::escape_id(inst->Name()), IN1, IN2, net_map.at(inst->GetOutput()), SIGNED); + return true; + } -static void import_netlist(RTLIL::Design *design, Netlist *nl, std::set<Netlist*> &nl_todo, bool mode_gates) -{ - std::string module_name = nl->IsOperator() ? std::string("$verific$") + nl->Owner()->Name() : RTLIL::escape_id(nl->Owner()->Name()); + if (inst->Type() == OPER_NEQUAL) { + module->addNe(RTLIL::escape_id(inst->Name()), IN1, IN2, net_map.at(inst->GetOutput()), SIGNED); + return true; + } - if (design->has(module_name)) { - if (!nl->IsOperator()) - log_cmd_error("Re-definition of module `%s'.\n", nl->Owner()->Name()); - return; - } + if (inst->Type() == OPER_WIDE_MUX) { + module->addMux(RTLIL::escape_id(inst->Name()), IN1, IN2, net_map.at(inst->GetControl()), OUT); + return true; + } - RTLIL::Module *module = new RTLIL::Module; - module->name = module_name; - design->add(module); + if (inst->Type() == OPER_WIDE_TRI) { + module->addMux(RTLIL::escape_id(inst->Name()), RTLIL::SigSpec(RTLIL::State::Sz, inst->OutputSize()), IN, net_map.at(inst->GetControl()), OUT); + return true; + } - log("Importing module %s.\n", RTLIL::id2cstr(module->name)); + if (inst->Type() == OPER_WIDE_DFFRS) { + RTLIL::SigSpec sig_set = operatorInport(inst, "set"); + RTLIL::SigSpec sig_reset = operatorInport(inst, "reset"); + if (sig_set.is_fully_const() && !sig_set.as_bool() && sig_reset.is_fully_const() && !sig_reset.as_bool()) + module->addDff(RTLIL::escape_id(inst->Name()), net_map.at(inst->GetClock()), IN, OUT); + else + module->addDffsr(RTLIL::escape_id(inst->Name()), net_map.at(inst->GetClock()), sig_set, sig_reset, IN, OUT); + return true; + } - std::map<Net*, RTLIL::SigBit> net_map; + #undef IN + #undef IN1 + #undef IN2 + #undef OUT + #undef SIGNED - SetIter si; - MapIter mi, mi2; - Port *port; - PortBus *portbus; - Net *net; - NetBus *netbus; - Instance *inst; - PortRef *pr; + return false; + } - FOREACH_PORT_OF_NETLIST(nl, mi, port) + void import_netlist(RTLIL::Design *design, Netlist *nl, std::set<Netlist*> &nl_todo, bool mode_gates) { - if (port->Bus()) - continue; + std::string module_name = nl->IsOperator() ? std::string("$verific$") + nl->Owner()->Name() : RTLIL::escape_id(nl->Owner()->Name()); - // log(" importing port %s.\n", port->Name()); + if (design->has(module_name)) { + if (!nl->IsOperator()) + log_cmd_error("Re-definition of module `%s'.\n", nl->Owner()->Name()); + return; + } - RTLIL::Wire *wire = module->addWire(RTLIL::escape_id(port->Name())); - import_attributes(wire->attributes, port); + module = new RTLIL::Module; + module->name = module_name; + design->add(module); - wire->port_id = nl->IndexOf(port) + 1; + log("Importing module %s.\n", RTLIL::id2cstr(module->name)); - if (port->GetDir() == DIR_INOUT || port->GetDir() == DIR_IN) - wire->port_input = true; - if (port->GetDir() == DIR_INOUT || port->GetDir() == DIR_OUT) - wire->port_output = true; + SetIter si; + MapIter mi, mi2; + Port *port; + PortBus *portbus; + Net *net; + NetBus *netbus; + Instance *inst; + PortRef *pr; - if (port->GetNet()) { - net = port->GetNet(); - if (net_map.count(net) == 0) - net_map[net] = wire; - else if (wire->port_input) - module->connect(net_map.at(net), wire); - else - module->connect(wire, net_map.at(net)); - } - } + FOREACH_PORT_OF_NETLIST(nl, mi, port) + { + if (port->Bus()) + continue; - FOREACH_PORTBUS_OF_NETLIST(nl, mi, portbus) - { - // log(" importing portbus %s.\n", portbus->Name()); + // log(" importing port %s.\n", port->Name()); + + RTLIL::Wire *wire = module->addWire(RTLIL::escape_id(port->Name())); + import_attributes(wire->attributes, port); - RTLIL::Wire *wire = module->addWire(RTLIL::escape_id(portbus->Name()), portbus->Size()); - wire->start_offset = min(portbus->LeftIndex(), portbus->RightIndex()); - import_attributes(wire->attributes, portbus); + wire->port_id = nl->IndexOf(port) + 1; - if (portbus->GetDir() == DIR_INOUT || portbus->GetDir() == DIR_IN) - wire->port_input = true; - if (portbus->GetDir() == DIR_INOUT || portbus->GetDir() == DIR_OUT) - wire->port_output = true; + if (port->GetDir() == DIR_INOUT || port->GetDir() == DIR_IN) + wire->port_input = true; + if (port->GetDir() == DIR_INOUT || port->GetDir() == DIR_OUT) + wire->port_output = true; - for (int i = portbus->LeftIndex();; i += portbus->IsUp() ? +1 : -1) { - if (portbus->ElementAtIndex(i) && portbus->ElementAtIndex(i)->GetNet()) { - net = portbus->ElementAtIndex(i)->GetNet(); - RTLIL::SigBit bit(wire, i - wire->start_offset); + if (port->GetNet()) { + net = port->GetNet(); if (net_map.count(net) == 0) - net_map[net] = bit; + net_map[net] = wire; else if (wire->port_input) - module->connect(net_map.at(net), bit); + module->connect(net_map.at(net), wire); else - module->connect(bit, net_map.at(net)); + module->connect(wire, net_map.at(net)); } - if (i == portbus->RightIndex()) - break; } - } - module->fixup_ports(); - - FOREACH_NET_OF_NETLIST(nl, mi, net) - { - if (net->IsRamNet()) + FOREACH_PORTBUS_OF_NETLIST(nl, mi, portbus) { - RTLIL::Memory *memory = new RTLIL::Memory; - memory->name = RTLIL::escape_id(net->Name()); - log_assert(module->count_id(memory->name) == 0); - module->memories[memory->name] = memory; - - int number_of_bits = net->Size(); - int bits_in_word = number_of_bits; - FOREACH_PORTREF_OF_NET(net, si, pr) { - if (pr->GetInst()->Type() == OPER_READ_PORT) { - bits_in_word = min<int>(bits_in_word, pr->GetInst()->OutputSize()); - continue; - } - if (pr->GetInst()->Type() == OPER_WRITE_PORT || pr->GetInst()->Type() == OPER_CLOCKED_WRITE_PORT) { - bits_in_word = min<int>(bits_in_word, pr->GetInst()->Input2Size()); - continue; + // log(" importing portbus %s.\n", portbus->Name()); + + RTLIL::Wire *wire = module->addWire(RTLIL::escape_id(portbus->Name()), portbus->Size()); + wire->start_offset = min(portbus->LeftIndex(), portbus->RightIndex()); + import_attributes(wire->attributes, portbus); + + if (portbus->GetDir() == DIR_INOUT || portbus->GetDir() == DIR_IN) + wire->port_input = true; + if (portbus->GetDir() == DIR_INOUT || portbus->GetDir() == DIR_OUT) + wire->port_output = true; + + for (int i = portbus->LeftIndex();; i += portbus->IsUp() ? +1 : -1) { + if (portbus->ElementAtIndex(i) && portbus->ElementAtIndex(i)->GetNet()) { + net = portbus->ElementAtIndex(i)->GetNet(); + RTLIL::SigBit bit(wire, i - wire->start_offset); + if (net_map.count(net) == 0) + net_map[net] = bit; + else if (wire->port_input) + module->connect(net_map.at(net), bit); + else + module->connect(bit, net_map.at(net)); } - log_error("Verific RamNet %s is connected to unsupported instance type %s (%s).\n", - net->Name(), pr->GetInst()->View()->Owner()->Name(), pr->GetInst()->Name()); + if (i == portbus->RightIndex()) + break; } - - memory->width = bits_in_word; - memory->size = number_of_bits / bits_in_word; - continue; } - if (net_map.count(net)) { - // log(" skipping net %s.\n", net->Name()); - continue; - } + module->fixup_ports(); + + FOREACH_NET_OF_NETLIST(nl, mi, net) + { + if (net->IsRamNet()) + { + RTLIL::Memory *memory = new RTLIL::Memory; + memory->name = RTLIL::escape_id(net->Name()); + log_assert(module->count_id(memory->name) == 0); + module->memories[memory->name] = memory; + + int number_of_bits = net->Size(); + int bits_in_word = number_of_bits; + FOREACH_PORTREF_OF_NET(net, si, pr) { + if (pr->GetInst()->Type() == OPER_READ_PORT) { + bits_in_word = min<int>(bits_in_word, pr->GetInst()->OutputSize()); + continue; + } + if (pr->GetInst()->Type() == OPER_WRITE_PORT || pr->GetInst()->Type() == OPER_CLOCKED_WRITE_PORT) { + bits_in_word = min<int>(bits_in_word, pr->GetInst()->Input2Size()); + continue; + } + log_error("Verific RamNet %s is connected to unsupported instance type %s (%s).\n", + net->Name(), pr->GetInst()->View()->Owner()->Name(), pr->GetInst()->Name()); + } + + memory->width = bits_in_word; + memory->size = number_of_bits / bits_in_word; + continue; + } - if (net->Bus()) - continue; + if (net_map.count(net)) { + // log(" skipping net %s.\n", net->Name()); + continue; + } - // log(" importing net %s.\n", net->Name()); + if (net->Bus()) + continue; - RTLIL::IdString wire_name = module->uniquify(RTLIL::escape_id(net->Name())); - RTLIL::Wire *wire = module->addWire(wire_name); - import_attributes(wire->attributes, net); + // log(" importing net %s.\n", net->Name()); - net_map[net] = wire; - } + RTLIL::IdString wire_name = module->uniquify(RTLIL::escape_id(net->Name())); + RTLIL::Wire *wire = module->addWire(wire_name); + import_attributes(wire->attributes, net); - FOREACH_NETBUS_OF_NETLIST(nl, mi, netbus) - { - bool found_new_net = false; - for (int i = netbus->LeftIndex();; i += netbus->IsUp() ? +1 : -1) { - net = netbus->ElementAtIndex(i); - if (net_map.count(net) == 0) - found_new_net = true; - if (i == netbus->RightIndex()) - break; + net_map[net] = wire; } - if (found_new_net) + FOREACH_NETBUS_OF_NETLIST(nl, mi, netbus) { - // log(" importing netbus %s.\n", netbus->Name()); - - RTLIL::IdString wire_name = module->uniquify(RTLIL::escape_id(netbus->Name())); - RTLIL::Wire *wire = module->addWire(wire_name, netbus->Size()); - wire->start_offset = min(netbus->LeftIndex(), netbus->RightIndex()); - import_attributes(wire->attributes, netbus); - + bool found_new_net = false; for (int i = netbus->LeftIndex();; i += netbus->IsUp() ? +1 : -1) { - if (netbus->ElementAtIndex(i)) { - net = netbus->ElementAtIndex(i); - RTLIL::SigBit bit(wire, i - wire->start_offset); - if (net_map.count(net) == 0) - net_map[net] = bit; - else - module->connect(bit, net_map.at(net)); - } + net = netbus->ElementAtIndex(i); + if (net_map.count(net) == 0) + found_new_net = true; if (i == netbus->RightIndex()) break; } + + if (found_new_net) + { + // log(" importing netbus %s.\n", netbus->Name()); + + RTLIL::IdString wire_name = module->uniquify(RTLIL::escape_id(netbus->Name())); + RTLIL::Wire *wire = module->addWire(wire_name, netbus->Size()); + wire->start_offset = min(netbus->LeftIndex(), netbus->RightIndex()); + import_attributes(wire->attributes, netbus); + + for (int i = netbus->LeftIndex();; i += netbus->IsUp() ? +1 : -1) { + if (netbus->ElementAtIndex(i)) { + net = netbus->ElementAtIndex(i); + RTLIL::SigBit bit(wire, i - wire->start_offset); + if (net_map.count(net) == 0) + net_map[net] = bit; + else + module->connect(bit, net_map.at(net)); + } + if (i == netbus->RightIndex()) + break; + } + } + else + { + // log(" skipping netbus %s.\n", netbus->Name()); + } } - else + + FOREACH_INSTANCE_OF_NETLIST(nl, mi, inst) { - // log(" skipping netbus %s.\n", netbus->Name()); + if (inst->Type() == PRIM_SVA_POSEDGE) { + Net *in_net = inst->GetInput(); + Net *out_net = inst->GetOutput(); + sva_posedge_map[out_net] = in_net; + continue; + } } - } - FOREACH_INSTANCE_OF_NETLIST(nl, mi, inst) - { - // log(" importing cell %s (%s).\n", inst->Name(), inst->View()->Owner()->Name()); + FOREACH_INSTANCE_OF_NETLIST(nl, mi, inst) + { + if (inst->Type() == PRIM_SVA_POSEDGE) + continue; - if (inst->Type() == PRIM_PWR) { - module->connect(net_map.at(inst->GetOutput()), RTLIL::State::S1); - continue; - } + // log(" importing cell %s (%s).\n", inst->Name(), inst->View()->Owner()->Name()); - if (inst->Type() == PRIM_GND) { - module->connect(net_map.at(inst->GetOutput()), RTLIL::State::S0); - continue; - } + if (inst->Type() == PRIM_SVA_AT) + { + Net *in1 = inst->GetInput1(); + Net *in2 = inst->GetInput2(); + Net *out = inst->GetOutput(); - if (inst->Type() == PRIM_BUF) { - module->addBufGate(RTLIL::escape_id(inst->Name()), net_map.at(inst->GetInput()), net_map.at(inst->GetOutput())); - continue; - } + if (sva_posedge_map.count(in2)) + std::swap(in1, in2); - if (inst->Type() == PRIM_X) { - module->connect(net_map.at(inst->GetOutput()), RTLIL::State::Sx); - continue; - } + log_assert(sva_posedge_map.count(in1)); + Net *clk = sva_posedge_map.at(in1); - if (inst->Type() == PRIM_Z) { - module->connect(net_map.at(inst->GetOutput()), RTLIL::State::Sz); - continue; - } + SigBit outsig = net_map.at(out); + log_assert(outsig.wire && GetSize(outsig.wire) == 1); + outsig.wire->attributes["\\init"] == Const(0, 1); - if (inst->Type() == OPER_READ_PORT) - { - RTLIL::Memory *memory = module->memories.at(RTLIL::escape_id(inst->GetInput()->Name())); - if (memory->width != int(inst->OutputSize())) - log_error("Import of asymetric memories from Verific is not supported yet: %s %s\n", inst->Name(), inst->GetInput()->Name()); - - RTLIL::SigSpec addr = operatorInput1(inst, net_map); - RTLIL::SigSpec data = operatorOutput(inst, net_map, module); - - RTLIL::Cell *cell = module->addCell(RTLIL::escape_id(inst->Name()), "$memrd"); - cell->parameters["\\MEMID"] = memory->name.str(); - cell->parameters["\\CLK_ENABLE"] = false; - cell->parameters["\\CLK_POLARITY"] = true; - cell->parameters["\\TRANSPARENT"] = false; - cell->parameters["\\ABITS"] = GetSize(addr); - cell->parameters["\\WIDTH"] = GetSize(data); - cell->setPort("\\CLK", RTLIL::State::Sx); - cell->setPort("\\EN", RTLIL::State::Sx); - cell->setPort("\\ADDR", addr); - cell->setPort("\\DATA", data); - continue; - } - - if (inst->Type() == OPER_WRITE_PORT || inst->Type() == OPER_CLOCKED_WRITE_PORT) - { - RTLIL::Memory *memory = module->memories.at(RTLIL::escape_id(inst->GetOutput()->Name())); - if (memory->width != int(inst->Input2Size())) - log_error("Import of asymetric memories from Verific is not supported yet: %s %s\n", inst->Name(), inst->GetInput()->Name()); - - RTLIL::SigSpec addr = operatorInput1(inst, net_map); - RTLIL::SigSpec data = operatorInput2(inst, net_map); - - RTLIL::Cell *cell = module->addCell(RTLIL::escape_id(inst->Name()), "$memwr"); - cell->parameters["\\MEMID"] = memory->name.str(); - cell->parameters["\\CLK_ENABLE"] = false; - cell->parameters["\\CLK_POLARITY"] = true; - cell->parameters["\\PRIORITY"] = 0; - cell->parameters["\\ABITS"] = GetSize(addr); - cell->parameters["\\WIDTH"] = GetSize(data); - cell->setPort("\\EN", RTLIL::SigSpec(net_map.at(inst->GetControl())).repeat(GetSize(data))); - cell->setPort("\\CLK", RTLIL::State::S0); - cell->setPort("\\ADDR", addr); - cell->setPort("\\DATA", data); - - if (inst->Type() == OPER_CLOCKED_WRITE_PORT) { - cell->parameters["\\CLK_ENABLE"] = true; - cell->setPort("\\CLK", net_map.at(inst->GetClock())); + module->addDff(NEW_ID, net_map.at(clk), net_map.at(in2), net_map.at(out)); + continue; } - continue; - } - if (!mode_gates) { - if (import_netlist_instance_cells(module, net_map, inst)) + if (inst->Type() == PRIM_SVA_IMMEDIATE_ASSERT || inst->Type() == PRIM_SVA_ASSERT) { + Net *in = inst->GetInput(); + module->addAssert(NEW_ID, net_map.at(in), State::S1); continue; - if (inst->IsOperator()) - log_warning("Unsupported Verific operator: %s (fallback to gate level implementation provided by verific)\n", inst->View()->Owner()->Name()); - } else { - if (import_netlist_instance_gates(module, net_map, inst)) + } + + if (inst->Type() == PRIM_SVA_IMMEDIATE_ASSUME || inst->Type() == PRIM_SVA_ASSUME) { + Net *in = inst->GetInput(); + module->addAssume(NEW_ID, net_map.at(in), State::S1); continue; - } + } - if (inst->IsPrimitive()) - log_error("Unsupported Verific primitive %s of type %s\n", inst->Name(), inst->View()->Owner()->Name()); + if (inst->Type() == PRIM_SVA_IMMEDIATE_COVER || inst->Type() == PRIM_SVA_COVER) { + Net *in = inst->GetInput(); + module->addCover(NEW_ID, net_map.at(in), State::S1); + continue; + } - nl_todo.insert(inst->View()); + if (inst->Type() == PRIM_PWR) { + module->connect(net_map.at(inst->GetOutput()), RTLIL::State::S1); + continue; + } - RTLIL::Cell *cell = module->addCell(RTLIL::escape_id(inst->Name()), inst->IsOperator() ? - std::string("$verific$") + inst->View()->Owner()->Name() : RTLIL::escape_id(inst->View()->Owner()->Name())); + if (inst->Type() == PRIM_GND) { + module->connect(net_map.at(inst->GetOutput()), RTLIL::State::S0); + continue; + } - dict<IdString, vector<SigBit>> cell_port_conns; + if (inst->Type() == PRIM_BUF) { + module->addBufGate(RTLIL::escape_id(inst->Name()), net_map.at(inst->GetInput()), net_map.at(inst->GetOutput())); + continue; + } - FOREACH_PORTREF_OF_INST(inst, mi2, pr) { - // log(" .%s(%s)\n", pr->GetPort()->Name(), pr->GetNet()->Name()); - const char *port_name = pr->GetPort()->Name(); - int port_offset = 0; - if (pr->GetPort()->Bus()) { - port_name = pr->GetPort()->Bus()->Name(); - port_offset = pr->GetPort()->Bus()->IndexOf(pr->GetPort()) - - min(pr->GetPort()->Bus()->LeftIndex(), pr->GetPort()->Bus()->RightIndex()); + if (inst->Type() == PRIM_X) { + module->connect(net_map.at(inst->GetOutput()), RTLIL::State::Sx); + continue; } - IdString port_name_id = RTLIL::escape_id(port_name); - auto &sigvec = cell_port_conns[port_name_id]; - if (GetSize(sigvec) <= port_offset) { - SigSpec zwires = module->addWire(NEW_ID, port_offset+1-GetSize(sigvec)); - for (auto bit : zwires) - sigvec.push_back(bit); + + if (inst->Type() == PRIM_Z) { + module->connect(net_map.at(inst->GetOutput()), RTLIL::State::Sz); + continue; } - sigvec[port_offset] = net_map.at(pr->GetNet()); - } - for (auto &it : cell_port_conns) { - // log(" .%s(%s)\n", log_id(it.first), log_signal(it.second)); - cell->setPort(it.first, it.second); + if (inst->Type() == OPER_READ_PORT) + { + RTLIL::Memory *memory = module->memories.at(RTLIL::escape_id(inst->GetInput()->Name())); + if (memory->width != int(inst->OutputSize())) + log_error("Import of asymetric memories from Verific is not supported yet: %s %s\n", inst->Name(), inst->GetInput()->Name()); + + RTLIL::SigSpec addr = operatorInput1(inst); + RTLIL::SigSpec data = operatorOutput(inst); + + RTLIL::Cell *cell = module->addCell(RTLIL::escape_id(inst->Name()), "$memrd"); + cell->parameters["\\MEMID"] = memory->name.str(); + cell->parameters["\\CLK_ENABLE"] = false; + cell->parameters["\\CLK_POLARITY"] = true; + cell->parameters["\\TRANSPARENT"] = false; + cell->parameters["\\ABITS"] = GetSize(addr); + cell->parameters["\\WIDTH"] = GetSize(data); + cell->setPort("\\CLK", RTLIL::State::Sx); + cell->setPort("\\EN", RTLIL::State::Sx); + cell->setPort("\\ADDR", addr); + cell->setPort("\\DATA", data); + continue; + } + + if (inst->Type() == OPER_WRITE_PORT || inst->Type() == OPER_CLOCKED_WRITE_PORT) + { + RTLIL::Memory *memory = module->memories.at(RTLIL::escape_id(inst->GetOutput()->Name())); + if (memory->width != int(inst->Input2Size())) + log_error("Import of asymetric memories from Verific is not supported yet: %s %s\n", inst->Name(), inst->GetInput()->Name()); + + RTLIL::SigSpec addr = operatorInput1(inst); + RTLIL::SigSpec data = operatorInput2(inst); + + RTLIL::Cell *cell = module->addCell(RTLIL::escape_id(inst->Name()), "$memwr"); + cell->parameters["\\MEMID"] = memory->name.str(); + cell->parameters["\\CLK_ENABLE"] = false; + cell->parameters["\\CLK_POLARITY"] = true; + cell->parameters["\\PRIORITY"] = 0; + cell->parameters["\\ABITS"] = GetSize(addr); + cell->parameters["\\WIDTH"] = GetSize(data); + cell->setPort("\\EN", RTLIL::SigSpec(net_map.at(inst->GetControl())).repeat(GetSize(data))); + cell->setPort("\\CLK", RTLIL::State::S0); + cell->setPort("\\ADDR", addr); + cell->setPort("\\DATA", data); + + if (inst->Type() == OPER_CLOCKED_WRITE_PORT) { + cell->parameters["\\CLK_ENABLE"] = true; + cell->setPort("\\CLK", net_map.at(inst->GetClock())); + } + continue; + } + + if (!mode_gates) { + if (import_netlist_instance_cells(inst)) + continue; + if (inst->IsOperator()) + log_warning("Unsupported Verific operator: %s (fallback to gate level implementation provided by verific)\n", inst->View()->Owner()->Name()); + } else { + if (import_netlist_instance_gates(inst)) + continue; + } + + if (inst->IsPrimitive()) + log_error("Unsupported Verific primitive %s of type %s\n", inst->Name(), inst->View()->Owner()->Name()); + + nl_todo.insert(inst->View()); + + RTLIL::Cell *cell = module->addCell(RTLIL::escape_id(inst->Name()), inst->IsOperator() ? + std::string("$verific$") + inst->View()->Owner()->Name() : RTLIL::escape_id(inst->View()->Owner()->Name())); + + dict<IdString, vector<SigBit>> cell_port_conns; + + FOREACH_PORTREF_OF_INST(inst, mi2, pr) { + // log(" .%s(%s)\n", pr->GetPort()->Name(), pr->GetNet()->Name()); + const char *port_name = pr->GetPort()->Name(); + int port_offset = 0; + if (pr->GetPort()->Bus()) { + port_name = pr->GetPort()->Bus()->Name(); + port_offset = pr->GetPort()->Bus()->IndexOf(pr->GetPort()) - + min(pr->GetPort()->Bus()->LeftIndex(), pr->GetPort()->Bus()->RightIndex()); + } + IdString port_name_id = RTLIL::escape_id(port_name); + auto &sigvec = cell_port_conns[port_name_id]; + if (GetSize(sigvec) <= port_offset) { + SigSpec zwires = module->addWire(NEW_ID, port_offset+1-GetSize(sigvec)); + for (auto bit : zwires) + sigvec.push_back(bit); + } + sigvec[port_offset] = net_map.at(pr->GetNet()); + } + + for (auto &it : cell_port_conns) { + // log(" .%s(%s)\n", log_id(it.first), log_signal(it.second)); + cell->setPort(it.first, it.second); + } } } -} +}; #endif /* YOSYS_ENABLE_VERIFIC */ -YOSYS_NAMESPACE_BEGIN - struct VerificPass : public Pass { VerificPass() : Pass("verific", "load Verilog and VHDL designs using Verific") { } virtual void help() { // |---v---|---v---|---v---|---v---|---v---|---v---|---v---|---v---|---v---|---v---| log("\n"); - log(" verific {-vlog95|-vlog2k|-sv2005|-sv2009|-sv} <verilog-file>..\n"); + log(" verific {-vlog95|-vlog2k|-sv2005|-sv2009|-sv|-vlpsl} <verilog-file>..\n"); log("\n"); log("Load the specified Verilog/SystemVerilog files into Verific.\n"); log("\n"); log("\n"); - log(" verific {-vhdl87|-vhdl93|-vhdl2k|-vhdl2008} <vhdl-file>..\n"); + log(" verific {-vhdl87|-vhdl93|-vhdl2k|-vhdl2008|-vhdpsl} <vhdl-file>..\n"); log("\n"); log("Load the specified VHDL files into Verific.\n"); log("\n"); @@ -890,6 +950,13 @@ struct VerificPass : public Pass { return; } + if (args.size() > 1 && args[1] == "-vlpsl") { + for (size_t argidx = 2; argidx < args.size(); argidx++) + if (!veri_file::Analyze(args[argidx].c_str(), veri_file::VERILOG_PSL)) + log_cmd_error("Reading `%s' in VERILOG_PSL mode failed.\n", args[argidx].c_str()); + return; + } + if (args.size() > 1 && args[1] == "-vhdl87") { vhdl_file::SetDefaultLibraryPath((proc_share_dirname() + "verific/vhdl_vdbs_1987").c_str()); for (size_t argidx = 2; argidx < args.size(); argidx++) @@ -922,6 +989,14 @@ struct VerificPass : public Pass { return; } + if (args.size() > 1 && args[1] == "-vhdpsl") { + vhdl_file::SetDefaultLibraryPath((proc_share_dirname() + "verific/vhdl_vdbs_2008").c_str()); + for (size_t argidx = 2; argidx < args.size(); argidx++) + if (!vhdl_file::Analyze(args[argidx].c_str(), "work", vhdl_file::VHDL_PSL)) + log_cmd_error("Reading `%s' in VHDL_PSL mode failed.\n", args[argidx].c_str()); + return; + } + if (args.size() > 1 && args[1] == "-import") { std::set<Netlist*> nl_todo, nl_done; @@ -982,8 +1057,10 @@ struct VerificPass : public Pass { while (!nl_todo.empty()) { Netlist *nl = *nl_todo.begin(); - if (nl_done.count(nl) == 0) - import_netlist(design, nl, nl_todo, mode_gates); + if (nl_done.count(nl) == 0) { + VerificImporter importer; + importer.import_netlist(design, nl, nl_todo, mode_gates); + } nl_todo.erase(nl); nl_done.insert(nl); } @@ -1001,5 +1078,5 @@ struct VerificPass : public Pass { #endif } VerificPass; -YOSYS_NAMESPACE_END +PRIVATE_NAMESPACE_END diff --git a/frontends/verilog/verilog_lexer.l b/frontends/verilog/verilog_lexer.l index 405aeb975..97af0ae2d 100644 --- a/frontends/verilog/verilog_lexer.l +++ b/frontends/verilog/verilog_lexer.l @@ -177,8 +177,11 @@ YOSYS_NAMESPACE_END "assert" { if (formal_mode) return TOK_ASSERT; SV_KEYWORD(TOK_ASSERT); } "assume" { if (formal_mode) return TOK_ASSUME; SV_KEYWORD(TOK_ASSUME); } +"cover" { if (formal_mode) return TOK_COVER; SV_KEYWORD(TOK_COVER); } "restrict" { if (formal_mode) return TOK_RESTRICT; SV_KEYWORD(TOK_RESTRICT); } "property" { if (formal_mode) return TOK_PROPERTY; SV_KEYWORD(TOK_PROPERTY); } +"rand" { if (formal_mode) return TOK_RAND; SV_KEYWORD(TOK_RAND); } +"const" { if (formal_mode) return TOK_CONST; SV_KEYWORD(TOK_CONST); } "logic" { SV_KEYWORD(TOK_REG); } "bit" { SV_KEYWORD(TOK_REG); } @@ -192,14 +195,17 @@ YOSYS_NAMESPACE_END "genvar" { return TOK_GENVAR; } "real" { return TOK_REAL; } +"enum" { SV_KEYWORD(TOK_ENUM); } +"typedef" { SV_KEYWORD(TOK_TYPEDEF); } + [0-9][0-9_]* { frontend_verilog_yylval.string = new std::string(yytext); - return TOK_CONST; + return TOK_CONSTVAL; } [0-9]*[ \t]*\'s?[bodhBODH][ \t\r\n]*[0-9a-fA-FzxZX?_]+ { frontend_verilog_yylval.string = new std::string(yytext); - return TOK_CONST; + return TOK_CONSTVAL; } [0-9][0-9_]*\.[0-9][0-9_]*([eE][-+]?[0-9_]+)? { diff --git a/frontends/verilog/verilog_parser.y b/frontends/verilog/verilog_parser.y index 607c48a81..3eb03dfd8 100644 --- a/frontends/verilog/verilog_parser.y +++ b/frontends/verilog/verilog_parser.y @@ -59,6 +59,7 @@ namespace VERILOG_FRONTEND { bool default_nettype_wire; bool sv_mode, formal_mode, lib_mode; bool norestrict_mode, assume_asserts_mode; + bool current_wire_rand, current_wire_const; std::istream *lexin; } YOSYS_NAMESPACE_END @@ -100,7 +101,7 @@ static void free_attr(std::map<std::string, AstNode*> *al) bool boolean; } -%token <string> TOK_STRING TOK_ID TOK_CONST TOK_REALVAL TOK_PRIMITIVE +%token <string> TOK_STRING TOK_ID TOK_CONSTVAL TOK_REALVAL TOK_PRIMITIVE %token ATTR_BEGIN ATTR_END DEFATTR_BEGIN DEFATTR_END %token TOK_MODULE TOK_ENDMODULE TOK_PARAMETER TOK_LOCALPARAM TOK_DEFPARAM %token TOK_PACKAGE TOK_ENDPACKAGE TOK_PACKAGESEP @@ -114,7 +115,8 @@ static void free_attr(std::map<std::string, AstNode*> *al) %token TOK_SYNOPSYS_FULL_CASE TOK_SYNOPSYS_PARALLEL_CASE %token TOK_SUPPLY0 TOK_SUPPLY1 TOK_TO_SIGNED TOK_TO_UNSIGNED %token TOK_POS_INDEXED TOK_NEG_INDEXED TOK_ASSERT TOK_ASSUME -%token TOK_RESTRICT TOK_PROPERTY +%token TOK_RESTRICT TOK_COVER TOK_PROPERTY TOK_ENUM TOK_TYPEDEF +%token TOK_RAND TOK_CONST %type <ast> range range_or_multirange non_opt_range non_opt_multirange range_or_signed_int %type <ast> wire_type expr basic_expr concat_list rvalue lvalue lvalue_concat_list @@ -355,6 +357,8 @@ delay: wire_type: { astbuf3 = new AstNode(AST_WIRE); + current_wire_rand = false; + current_wire_const = false; } wire_type_token_list delay { $$ = astbuf3; }; @@ -392,6 +396,12 @@ wire_type_token: } | TOK_SIGNED { astbuf3->is_signed = true; + } | + TOK_RAND { + current_wire_rand = true; + } | + TOK_CONST { + current_wire_const = true; }; non_opt_range: @@ -730,7 +740,15 @@ wire_name_list: wire_name_and_opt_assign | wire_name_list ',' wire_name_and_opt_assign; wire_name_and_opt_assign: - wire_name | + wire_name { + if (current_wire_rand) { + AstNode *wire = new AstNode(AST_IDENTIFIER); + AstNode *fcall = new AstNode(AST_FCALL); + wire->str = ast_stack.back()->children.back()->str; + fcall->str = current_wire_const ? "\\$anyconst" : "\\$anyseq"; + ast_stack.back()->children.push_back(new AstNode(AST_ASSIGN, wire, fcall)); + } + } | wire_name '=' expr { AstNode *wire = new AstNode(AST_IDENTIFIER); wire->str = ast_stack.back()->children.back()->str; @@ -1000,6 +1018,15 @@ assert: TOK_ASSUME '(' expr ')' ';' { ast_stack.back()->children.push_back(new AstNode(AST_ASSUME, $3)); } | + TOK_COVER '(' expr ')' ';' { + ast_stack.back()->children.push_back(new AstNode(AST_COVER, $3)); + } | + TOK_COVER '(' ')' ';' { + ast_stack.back()->children.push_back(new AstNode(AST_COVER, AstNode::mkconst_int(1, false))); + } | + TOK_COVER ';' { + ast_stack.back()->children.push_back(new AstNode(AST_COVER, AstNode::mkconst_int(1, false))); + } | TOK_RESTRICT '(' expr ')' ';' { if (norestrict_mode) delete $3; @@ -1014,6 +1041,9 @@ assert_property: TOK_ASSUME TOK_PROPERTY '(' expr ')' ';' { ast_stack.back()->children.push_back(new AstNode(AST_ASSUME, $4)); } | + TOK_COVER TOK_PROPERTY '(' expr ')' ';' { + ast_stack.back()->children.push_back(new AstNode(AST_COVER, $4)); + } | TOK_RESTRICT TOK_PROPERTY '(' expr ')' ';' { if (norestrict_mode) delete $4; @@ -1350,7 +1380,7 @@ basic_expr: rvalue { $$ = $1; } | - '(' expr ')' TOK_CONST { + '(' expr ')' TOK_CONSTVAL { if ($4->substr(0, 1) != "'") frontend_verilog_yyerror("Syntax error."); AstNode *bits = $2; @@ -1360,7 +1390,7 @@ basic_expr: $$ = new AstNode(AST_TO_BITS, bits, val); delete $4; } | - hierarchical_id TOK_CONST { + hierarchical_id TOK_CONSTVAL { if ($2->substr(0, 1) != "'") frontend_verilog_yyerror("Syntax error."); AstNode *bits = new AstNode(AST_IDENTIFIER); @@ -1372,14 +1402,14 @@ basic_expr: delete $1; delete $2; } | - TOK_CONST TOK_CONST { + TOK_CONSTVAL TOK_CONSTVAL { $$ = const2ast(*$1 + *$2, case_type_stack.size() == 0 ? 0 : case_type_stack.back(), !lib_mode); if ($$ == NULL || (*$2)[0] != '\'') log_error("Value conversion failed: `%s%s'\n", $1->c_str(), $2->c_str()); delete $1; delete $2; } | - TOK_CONST { + TOK_CONSTVAL { $$ = const2ast(*$1, case_type_stack.size() == 0 ? 0 : case_type_stack.back(), !lib_mode); if ($$ == NULL) log_error("Value conversion failed: `%s'\n", $1->c_str()); diff --git a/kernel/celltypes.h b/kernel/celltypes.h index f0ead1e89..04db5125e 100644 --- a/kernel/celltypes.h +++ b/kernel/celltypes.h @@ -116,6 +116,7 @@ struct CellTypes setup_type("$assert", {A, EN}, pool<RTLIL::IdString>(), true); setup_type("$assume", {A, EN}, pool<RTLIL::IdString>(), true); + setup_type("$cover", {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); diff --git a/kernel/rtlil.cc b/kernel/rtlil.cc index 40ad8ca13..978a7a537 100644 --- a/kernel/rtlil.cc +++ b/kernel/rtlil.cc @@ -1026,7 +1026,7 @@ namespace { return; } - if (cell->type.in("$assert", "$assume")) { + if (cell->type.in("$assert", "$assume", "$cover")) { port("\\A", 1); port("\\EN", 1); check_expected(); @@ -1819,6 +1819,14 @@ RTLIL::Cell* RTLIL::Module::addAssume(RTLIL::IdString name, RTLIL::SigSpec sig_a return cell; } +RTLIL::Cell* RTLIL::Module::addCover(RTLIL::IdString name, RTLIL::SigSpec sig_a, RTLIL::SigSpec sig_en) +{ + RTLIL::Cell *cell = addCell(name, "$cover"); + cell->setPort("\\A", sig_a); + cell->setPort("\\EN", sig_en); + return cell; +} + RTLIL::Cell* RTLIL::Module::addEquiv(RTLIL::IdString name, RTLIL::SigSpec sig_a, RTLIL::SigSpec sig_b, RTLIL::SigSpec sig_y) { RTLIL::Cell *cell = addCell(name, "$equiv"); @@ -2050,6 +2058,7 @@ RTLIL::Memory::Memory() hashidx_ = hashidx_count; width = 1; + start_offset = 0; size = 0; } diff --git a/kernel/rtlil.h b/kernel/rtlil.h index 8dd8fcca3..7a6f5717d 100644 --- a/kernel/rtlil.h +++ b/kernel/rtlil.h @@ -1007,6 +1007,7 @@ public: RTLIL::Cell* addTribuf (RTLIL::IdString name, RTLIL::SigSpec sig_a, RTLIL::SigSpec sig_en, RTLIL::SigSpec sig_y); RTLIL::Cell* addAssert (RTLIL::IdString name, RTLIL::SigSpec sig_a, RTLIL::SigSpec sig_en); RTLIL::Cell* addAssume (RTLIL::IdString name, RTLIL::SigSpec sig_a, RTLIL::SigSpec sig_en); + RTLIL::Cell* addCover (RTLIL::IdString name, RTLIL::SigSpec sig_a, RTLIL::SigSpec sig_en); 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); diff --git a/kernel/satgen.h b/kernel/satgen.h index 690f8e337..25a22fd8a 100644 --- a/kernel/satgen.h +++ b/kernel/satgen.h @@ -507,11 +507,7 @@ struct SatGen std::vector<int> undef_s = importUndefSigSpec(cell->getPort("\\S"), timestep); std::vector<int> undef_y = importUndefSigSpec(cell->getPort("\\Y"), timestep); - int maybe_one_hot = ez->CONST_FALSE; - int maybe_many_hot = ez->CONST_FALSE; - - int sure_one_hot = ez->CONST_FALSE; - int sure_many_hot = ez->CONST_FALSE; + int maybe_a = ez->CONST_TRUE; std::vector<int> bits_set = std::vector<int>(undef_y.size(), ez->CONST_FALSE); std::vector<int> bits_clr = std::vector<int>(undef_y.size(), ez->CONST_FALSE); @@ -524,18 +520,12 @@ struct SatGen int maybe_s = ez->OR(s.at(i), undef_s.at(i)); int sure_s = ez->AND(s.at(i), ez->NOT(undef_s.at(i))); - maybe_one_hot = ez->OR(maybe_one_hot, maybe_s); - maybe_many_hot = ez->OR(maybe_many_hot, ez->AND(maybe_one_hot, maybe_s)); - - sure_one_hot = ez->OR(sure_one_hot, sure_s); - sure_many_hot = ez->OR(sure_many_hot, ez->AND(sure_one_hot, sure_s)); + maybe_a = ez->AND(maybe_a, ez->NOT(sure_s)); - bits_set = ez->vec_ite(maybe_s, ez->vec_or(bits_set, ez->vec_or(bits_set, ez->vec_or(part_of_b, part_of_undef_b))), bits_set); - bits_clr = ez->vec_ite(maybe_s, ez->vec_or(bits_clr, ez->vec_or(bits_clr, ez->vec_or(ez->vec_not(part_of_b), part_of_undef_b))), bits_clr); + bits_set = ez->vec_ite(maybe_s, ez->vec_or(bits_set, ez->vec_or(part_of_b, part_of_undef_b)), bits_set); + bits_clr = ez->vec_ite(maybe_s, ez->vec_or(bits_clr, ez->vec_or(ez->vec_not(part_of_b), part_of_undef_b)), bits_clr); } - int maybe_a = ez->NOT(maybe_one_hot); - bits_set = ez->vec_ite(maybe_a, ez->vec_or(bits_set, ez->vec_or(bits_set, ez->vec_or(a, undef_a))), bits_set); bits_clr = ez->vec_ite(maybe_a, ez->vec_or(bits_clr, ez->vec_or(bits_clr, ez->vec_or(ez->vec_not(a), undef_a))), bits_clr); diff --git a/manual/CHAPTER_CellLib.tex b/manual/CHAPTER_CellLib.tex index a831fdf33..7686f5963 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}, {\tt \$anyconst}, and {\tt \$anyseq} cells. +Add information about {\tt \$assert}, {\tt \$assume}, {\tt \$cover}, {\tt \$equiv}, {\tt \$initstate}, {\tt \$anyconst}, and {\tt \$anyseq} cells. \end{fixme} \begin{fixme} diff --git a/manual/clean.sh b/manual/clean.sh index 11c2e7bf2..addc34ed1 100755 --- a/manual/clean.sh +++ b/manual/clean.sh @@ -1,2 +1,2 @@ #!/bin/bash -for f in $( find . -name .gitignore ); do sed -re "s,^,find ${f%.gitignore} -name ',; s,$,' | xargs rm -f,;" $f; done | bash -v +for f in $( find . -name .gitignore ); do sed -Ee "s,^,find ${f%.gitignore} -name ',; s,$,' | xargs rm -f,;" $f; done | bash -v diff --git a/passes/equiv/equiv_simple.cc b/passes/equiv/equiv_simple.cc index 49963ed68..270200c34 100644 --- a/passes/equiv/equiv_simple.cc +++ b/passes/equiv/equiv_simple.cc @@ -59,7 +59,7 @@ struct EquivSimpleWorker for (auto &conn : cell->connections()) if (yosys_celltypes.cell_input(cell->type, conn.first)) for (auto bit : sigmap(conn.second)) { - if (cell->type.in("$dff", "$_DFF_P_", "$_DFF_N_")) { + if (cell->type.in("$dff", "$_DFF_P_", "$_DFF_N_", "$ff", "$_FF_")) { if (!conn.first.in("\\CLK", "\\C")) next_seed.insert(bit); } else @@ -329,7 +329,7 @@ struct EquivSimplePass : public Pass { unproven_cells_counter, GetSize(unproven_equiv_cells), log_id(module)); for (auto cell : module->cells()) { - if (!ct.cell_known(cell->type) && !cell->type.in("$dff", "$_DFF_P_", "$_DFF_N_")) + if (!ct.cell_known(cell->type) && !cell->type.in("$dff", "$_DFF_P_", "$_DFF_N_", "$ff", "$_FF_")) continue; for (auto &conn : cell->connections()) if (yosys_celltypes.cell_output(cell->type, conn.first)) diff --git a/passes/fsm/fsm_expand.cc b/passes/fsm/fsm_expand.cc index e7b9dcf90..2c344a1c1 100644 --- a/passes/fsm/fsm_expand.cc +++ b/passes/fsm/fsm_expand.cc @@ -54,13 +54,27 @@ struct FsmExpand if (cell->getPort("\\A").size() < 2) return true; + int in_bits = 0; RTLIL::SigSpec new_signals; - if (cell->hasPort("\\A")) + + if (cell->hasPort("\\A")) { + in_bits += GetSize(cell->getPort("\\A")); new_signals.append(assign_map(cell->getPort("\\A"))); - if (cell->hasPort("\\B")) + } + + if (cell->hasPort("\\B")) { + in_bits += GetSize(cell->getPort("\\B")); new_signals.append(assign_map(cell->getPort("\\B"))); - if (cell->hasPort("\\S")) + } + + if (cell->hasPort("\\S")) { + in_bits += GetSize(cell->getPort("\\S")); new_signals.append(assign_map(cell->getPort("\\S"))); + } + + if (in_bits > 8) + return false; + if (cell->hasPort("\\Y")) new_signals.append(assign_map(cell->getPort("\\Y"))); @@ -173,6 +187,16 @@ struct FsmExpand new_ctrl_out.append(output_sig); fsm_cell->setPort("\\CTRL_OUT", new_ctrl_out); + if (GetSize(input_sig) > 10) + log_warning("Cell %s.%s (%s) has %d input bits, merging into FSM %s.%s might be problematic.\n", + log_id(cell->module), log_id(cell), log_id(cell->type), + GetSize(input_sig), log_id(fsm_cell->module), log_id(fsm_cell)); + + if (GetSize(fsm_data.transition_table) > 10000) + log_warning("Transition table for FSM %s.%s already has %d rows, merging more cells " + "into this FSM might be problematic.\n", log_id(fsm_cell->module), log_id(fsm_cell), + GetSize(fsm_data.transition_table)); + std::vector<FsmData::transition_t> new_transition_table; for (auto &tr : fsm_data.transition_table) { for (int i = 0; i < (1 << input_sig.size()); i++) { diff --git a/passes/hierarchy/hierarchy.cc b/passes/hierarchy/hierarchy.cc index 337af7fd7..4786aacaf 100644 --- a/passes/hierarchy/hierarchy.cc +++ b/passes/hierarchy/hierarchy.cc @@ -175,16 +175,12 @@ bool expand_module(RTLIL::Design *design, RTLIL::Module *module, bool flag_check { filename = dir + "/" + RTLIL::unescape_id(cell->type) + ".v"; if (check_file_exists(filename)) { - std::vector<std::string> args; - args.push_back(filename); Frontend::frontend_call(design, NULL, filename, "verilog"); goto loaded_module; } filename = dir + "/" + RTLIL::unescape_id(cell->type) + ".il"; if (check_file_exists(filename)) { - std::vector<std::string> args; - args.push_back(filename); Frontend::frontend_call(design, NULL, filename, "ilang"); goto loaded_module; } @@ -317,7 +313,7 @@ bool set_keep_assert(std::map<RTLIL::Module*, bool> &cache, RTLIL::Module *mod) if (cache.count(mod) == 0) for (auto c : mod->cells()) { RTLIL::Module *m = mod->design->module(c->type); - if ((m != nullptr && set_keep_assert(cache, m)) || c->type.in("$assert", "$assume")) + if ((m != nullptr && set_keep_assert(cache, m)) || c->type.in("$assert", "$assume", "$cover")) return cache[mod] = true; } return cache[mod]; diff --git a/passes/opt/opt_clean.cc b/passes/opt/opt_clean.cc index 6600ffa25..65944caec 100644 --- a/passes/opt/opt_clean.cc +++ b/passes/opt/opt_clean.cc @@ -64,7 +64,7 @@ struct keep_cache_t bool query(Cell *cell) { - if (cell->type.in("$memwr", "$meminit", "$assert", "$assume")) + if (cell->type.in("$memwr", "$meminit", "$assert", "$assume", "$cover")) return true; if (cell->has_keep_attr()) diff --git a/passes/opt/opt_expr.cc b/passes/opt/opt_expr.cc index b62eae285..b3f2e87ed 100644 --- a/passes/opt/opt_expr.cc +++ b/passes/opt/opt_expr.cc @@ -259,6 +259,29 @@ bool is_one_or_minus_one(const Const &value, bool is_signed, bool &is_negative) return last_bit_one; } +// if the signal has only one bit set, return the index of that bit. +// otherwise return -1 +int get_onehot_bit_index(RTLIL::SigSpec signal) +{ + int bit_index = -1; + + for (int i = 0; i < GetSize(signal); i++) + { + if (signal[i] == RTLIL::State::S0) + continue; + + if (signal[i] != RTLIL::State::S1) + return -1; + + if (bit_index != -1) + return -1; + + bit_index = i; + } + + return bit_index; +} + void replace_const_cells(RTLIL::Design *design, RTLIL::Module *module, bool consume_x, bool mux_undef, bool mux_bool, bool do_fine, bool keepdc, bool clkinv) { if (!design->selected(module)) @@ -1167,6 +1190,103 @@ void replace_const_cells(RTLIL::Design *design, RTLIL::Module *module, bool cons } } + // replace a<0 or a>=0 with the top bit of a + if (do_fine && (cell->type == "$lt" || cell->type == "$ge" || cell->type == "$gt" || cell->type == "$le")) + { + //used to decide whether the signal needs to be negated + bool is_lt = false; + + //references the variable signal in the comparison + RTLIL::SigSpec sigVar; + + //references the constant signal in the comparison + RTLIL::SigSpec sigConst; + + // note that this signal must be constant for the optimization + // to take place, but it is not checked beforehand. + // If new passes are added, this signal must be checked for const-ness + + //width of the variable port + int width; + + bool var_signed; + + if (cell->type == "$lt" || cell->type == "$ge") { + is_lt = cell->type == "$lt" ? 1 : 0; + sigVar = cell->getPort("\\A"); + sigConst = cell->getPort("\\B"); + width = cell->parameters["\\A_WIDTH"].as_int(); + var_signed = cell->parameters["\\A_SIGNED"].as_bool(); + } else + if (cell->type == "$gt" || cell->type == "$le") { + is_lt = cell->type == "$gt" ? 1 : 0; + sigVar = cell->getPort("\\B"); + sigConst = cell->getPort("\\A"); + width = cell->parameters["\\B_WIDTH"].as_int(); + var_signed = cell->parameters["\\B_SIGNED"].as_bool(); + } + + // replace a(signed) < 0 with the high bit of a + if (sigConst.is_fully_const() && sigConst.is_fully_zero() && var_signed == true) + { + RTLIL::SigSpec a_prime(RTLIL::State::S0, cell->parameters["\\Y_WIDTH"].as_int()); + a_prime[0] = sigVar[width - 1]; + if (is_lt) { + log("Replacing %s cell `%s' (implementing X<0) with X[%d]: %s\n", + log_id(cell->type), log_id(cell), width-1, log_signal(a_prime)); + module->connect(cell->getPort("\\Y"), a_prime); + module->remove(cell); + } else { + log("Replacing %s cell `%s' (implementing X>=0) with ~X[%d]: %s\n", + log_id(cell->type), log_id(cell), width-1, log_signal(a_prime)); + module->addNot(NEW_ID, a_prime, cell->getPort("\\Y")); + module->remove(cell); + } + did_something = true; + goto next_cell; + } else + if (sigConst.is_fully_const() && sigConst.is_fully_def() && var_signed == false) + { + if (sigConst.is_fully_zero()) { + RTLIL::SigSpec a_prime(RTLIL::State::S0, 1); + if (is_lt) { + log("Replacing %s cell `%s' (implementing unsigned X<0) with constant false.\n", + log_id(cell->type), log_id(cell)); + a_prime[0] = RTLIL::State::S0; + } else { + log("Replacing %s cell `%s' (implementing unsigned X>=0) with constant true.\n", + log_id(cell->type), log_id(cell)); + a_prime[0] = RTLIL::State::S1; + } + module->connect(cell->getPort("\\Y"), a_prime); + module->remove(cell); + did_something = true; + goto next_cell; + } + + int const_bit_set = get_onehot_bit_index(sigConst); + if (const_bit_set >= 0) { + int bit_set = const_bit_set; + RTLIL::SigSpec a_prime(RTLIL::State::S0, width - bit_set); + for (int i = bit_set; i < width; i++) { + a_prime[i - bit_set] = sigVar[i]; + } + if (is_lt) { + log("Replacing %s cell `%s' (implementing unsigned X<%s) with !X[%d:%d]: %s.\n", + log_id(cell->type), log_id(cell), log_signal(sigConst), width - 1, bit_set, log_signal(a_prime)); + module->addLogicNot(NEW_ID, a_prime, cell->getPort("\\Y")); + } else { + log("Replacing %s cell `%s' (implementing unsigned X>=%s) with |X[%d:%d]: %s.\n", + log_id(cell->type), log_id(cell), log_signal(sigConst), width - 1, bit_set, log_signal(a_prime)); + module->addReduceOr(NEW_ID, a_prime, cell->getPort("\\Y")); + } + module->remove(cell); + did_something = true; + goto next_cell; + } + } + } + next_cell:; #undef ACTION_DO #undef ACTION_DO_Y diff --git a/passes/opt/opt_rmdff.cc b/passes/opt/opt_rmdff.cc index 922f086f1..00094738c 100644 --- a/passes/opt/opt_rmdff.cc +++ b/passes/opt/opt_rmdff.cc @@ -41,9 +41,27 @@ void remove_init_attr(SigSpec sig) bool handle_dlatch(RTLIL::Module *mod, RTLIL::Cell *dlatch) { - SigSpec sig_e = dlatch->getPort("\\EN"); + SigSpec sig_e; + State on_state, off_state; + + if (dlatch->type == "$dlatch") { + sig_e = assign_map(dlatch->getPort("\\EN")); + on_state = dlatch->getParam("\\EN_POLARITY").as_bool() ? State::S1 : State::S0; + off_state = dlatch->getParam("\\EN_POLARITY").as_bool() ? State::S0 : State::S1; + } else + if (dlatch->type == "$_DLATCH_P_") { + sig_e = assign_map(dlatch->getPort("\\E")); + on_state = State::S1; + off_state = State::S0; + } else + if (dlatch->type == "$_DLATCH_N_") { + sig_e = assign_map(dlatch->getPort("\\E")); + on_state = State::S0; + off_state = State::S1; + } else + log_abort(); - if (sig_e == State::S0) + if (sig_e == off_state) { RTLIL::Const val_init; for (auto bit : dff_init_map(dlatch->getPort("\\Q"))) @@ -52,7 +70,7 @@ bool handle_dlatch(RTLIL::Module *mod, RTLIL::Cell *dlatch) goto delete_dlatch; } - if (sig_e == State::S1) + if (sig_e == on_state) { mod->connect(dlatch->getPort("\\Q"), dlatch->getPort("\\D")); goto delete_dlatch; @@ -268,7 +286,7 @@ struct OptRmdffPass : public Pass { "$ff", "$dff", "$adff")) dff_list.push_back(cell->name); - if (cell->type == "$dlatch") + if (cell->type.in("$dlatch", "$_DLATCH_P_", "$_DLATCH_N_")) dlatch_list.push_back(cell->name); } diff --git a/passes/techmap/abc.cc b/passes/techmap/abc.cc index 9b829f435..a1cea3aaf 100644 --- a/passes/techmap/abc.cc +++ b/passes/techmap/abc.cc @@ -29,11 +29,11 @@ // Kahn, Arthur B. (1962), "Topological sorting of large networks", Communications of the ACM 5 (11): 558-562, doi:10.1145/368996.369025 // http://en.wikipedia.org/wiki/Topological_sorting -#define ABC_COMMAND_LIB "strash; ifraig; scorr; dc2; dretime; strash; dch -f; map {D}" -#define ABC_COMMAND_CTR "strash; ifraig; scorr; dc2; dretime; strash; dch -f; map {D}; buffer; upsize {D}; dnsize {D}; stime -p" +#define ABC_COMMAND_LIB "strash; ifraig; scorr; dc2; dretime; strash; &get -n; &dch -f; &nf {D}; &put" +#define ABC_COMMAND_CTR "strash; ifraig; scorr; dc2; dretime; strash; &get -n; &dch -f; &nf {D}; &put; buffer; upsize {D}; dnsize {D}; stime -p" #define ABC_COMMAND_LUT "strash; ifraig; scorr; dc2; dretime; strash; dch -f; if; mfs2" #define ABC_COMMAND_SOP "strash; ifraig; scorr; dc2; dretime; strash; dch -f; cover {I} {P}" -#define ABC_COMMAND_DFL "strash; ifraig; scorr; dc2; dretime; strash; dch -f; map" +#define ABC_COMMAND_DFL "strash; ifraig; scorr; dc2; dretime; strash; &get -n; &dch -f; &nf {D}; &put" #define ABC_FAST_COMMAND_LIB "strash; dretime; map {D}" #define ABC_FAST_COMMAND_CTR "strash; dretime; map {D}; buffer; upsize {D}; dnsize {D}; stime -p" diff --git a/techlibs/common/simlib.v b/techlibs/common/simlib.v index 2c4db1ac6..d0abd3b34 100644 --- a/techlibs/common/simlib.v +++ b/techlibs/common/simlib.v @@ -1305,6 +1305,14 @@ endmodule // -------------------------------------------------------- +module \$cover (A, EN); + +input A, EN; + +endmodule + +// -------------------------------------------------------- + module \$initstate (Y); output reg Y = 1; |