diff options
Diffstat (limited to 'backends')
| -rw-r--r-- | backends/smt2/Makefile.inc | 13 | ||||
| -rw-r--r-- | backends/smt2/example.v | 11 | ||||
| -rw-r--r-- | backends/smt2/example.ys | 3 | ||||
| -rw-r--r-- | backends/smt2/smt2.cc | 31 | ||||
| -rw-r--r-- | backends/smt2/smtbmc.py | 196 | ||||
| -rw-r--r-- | backends/smt2/smtio.py | 325 | ||||
| -rw-r--r-- | backends/smv/smv.cc | 10 | ||||
| -rw-r--r-- | backends/verilog/verilog_backend.cc | 15 |
8 files changed, 582 insertions, 22 deletions
diff --git a/backends/smt2/Makefile.inc b/backends/smt2/Makefile.inc index 4e0a393a8..eacda2734 100644 --- a/backends/smt2/Makefile.inc +++ b/backends/smt2/Makefile.inc @@ -1,3 +1,16 @@ OBJS += backends/smt2/smt2.o +ifneq ($(CONFIG),mxe) +ifneq ($(CONFIG),emcc) +TARGETS += yosys-smtbmc + +yosys-smtbmc: backends/smt2/smtbmc.py + $(P) sed 's|##yosys-sys-path##|sys.path += [os.path.dirname(__file__) + p for p in ["/share/python3", "/../share/yosys/python3"]]|;' < $< > $@.new + $(Q) chmod +x $@.new + $(Q) mv $@.new $@ + +$(eval $(call add_share_file,share/python3,backends/smt2/smtio.py)) +endif +endif + diff --git a/backends/smt2/example.v b/backends/smt2/example.v new file mode 100644 index 000000000..b195266eb --- /dev/null +++ b/backends/smt2/example.v @@ -0,0 +1,11 @@ +module main(input clk); + reg [3:0] counter = 0; + always @(posedge clk) begin + if (counter == 10) + counter <= 0; + else + counter <= counter + 1; + end + assert property (counter != 15); + // assert property (counter <= 10); +endmodule diff --git a/backends/smt2/example.ys b/backends/smt2/example.ys new file mode 100644 index 000000000..6fccb344f --- /dev/null +++ b/backends/smt2/example.ys @@ -0,0 +1,3 @@ +read_verilog -formal example.v +hierarchy; proc; opt; memory -nordff -nomap; opt -fast +write_smt2 -bv -mem -wires example.smt2 diff --git a/backends/smt2/smt2.cc b/backends/smt2/smt2.cc index 1e00ac718..c852921ee 100644 --- a/backends/smt2/smt2.cc +++ b/backends/smt2/smt2.cc @@ -32,7 +32,7 @@ struct Smt2Worker CellTypes ct; SigMap sigmap; RTLIL::Module *module; - bool bvmode, memmode, regsmode, verbose; + bool bvmode, memmode, regsmode, wiresmode, verbose; int idcounter; std::vector<std::string> decls, trans; @@ -44,8 +44,9 @@ struct Smt2Worker std::map<Cell*, int> memarrays; std::map<int, int> bvsizes; - Smt2Worker(RTLIL::Module *module, bool bvmode, bool memmode, bool regsmode, bool verbose) : - ct(module->design), sigmap(module), module(module), bvmode(bvmode), memmode(memmode), regsmode(regsmode), verbose(verbose), idcounter(0) + Smt2Worker(RTLIL::Module *module, bool bvmode, bool memmode, bool regsmode, bool wiresmode, bool verbose) : + ct(module->design), sigmap(module), module(module), bvmode(bvmode), memmode(memmode), + regsmode(regsmode), wiresmode(wiresmode), verbose(verbose), idcounter(0) { decls.push_back(stringf("(declare-sort |%s_s| 0)\n", log_id(module))); @@ -132,7 +133,7 @@ struct Smt2Worker std::string get_bool(RTLIL::SigSpec sig, const char *state_name = "state") { - return get_bool(sig.to_single_sigbit(), state_name); + return get_bool(sig.as_bit(), state_name); } std::string get_bv(RTLIL::SigSpec sig, const char *state_name = "state") @@ -215,7 +216,7 @@ struct Smt2Worker void export_gate(RTLIL::Cell *cell, std::string expr) { - RTLIL::SigBit bit = sigmap(cell->getPort("\\Y").to_single_sigbit()); + RTLIL::SigBit bit = sigmap(cell->getPort("\\Y").as_bit()); std::string processed_expr; for (char ch : expr) { @@ -243,8 +244,8 @@ struct Smt2Worker int width = GetSize(sig_y); if (type == 's' || type == 'd' || type == 'b') { - width = std::max(width, GetSize(cell->getPort("\\A"))); - width = std::max(width, GetSize(cell->getPort("\\B"))); + width = max(width, GetSize(cell->getPort("\\A"))); + width = max(width, GetSize(cell->getPort("\\B"))); } if (cell->hasPort("\\A")) { @@ -488,7 +489,7 @@ struct Smt2Worker for (auto bit : SigSpec(wire)) if (reg_bits.count(bit)) is_register = true; - if (wire->port_id || is_register || wire->get_bool_attribute("\\keep")) { + if (wire->port_id || is_register || wire->get_bool_attribute("\\keep") || (wiresmode && wire->name[0] == '\\')) { RTLIL::SigSpec sig = sigmap(wire); if (wire->port_input) decls.push_back(stringf("; yosys-smt2-input %s %d\n", log_id(wire), wire->width)); @@ -496,6 +497,8 @@ struct Smt2Worker decls.push_back(stringf("; yosys-smt2-output %s %d\n", log_id(wire), wire->width)); if (is_register) decls.push_back(stringf("; yosys-smt2-register %s %d\n", log_id(wire), wire->width)); + if (wire->get_bool_attribute("\\keep") || (wiresmode && wire->name[0] == '\\')) + decls.push_back(stringf("; yosys-smt2-wire %s %d\n", log_id(wire), wire->width)); if (bvmode && GetSize(sig) > 1) { decls.push_back(stringf("(define-fun |%s_n %s| ((state |%s_s|)) (_ BitVec %d) %s)\n", log_id(module), log_id(wire), log_id(module), GetSize(sig), get_bv(sig).c_str())); @@ -628,6 +631,7 @@ struct Smt2Worker for (auto it : decls) f << it; + f << stringf("; yosys-smt2-module %s\n", log_id(module)); f << stringf("(define-fun |%s_t| ((state |%s_s|) (next_state |%s_s|)) Bool ", log_id(module), log_id(module), log_id(module)); if (GetSize(trans) > 1) { f << "(and\n"; @@ -693,6 +697,9 @@ struct Smt2Backend : public Backend { log(" -regs\n"); log(" also create '<mod>_n' functions for all registers.\n"); log("\n"); + log(" -wires\n"); + log(" also create '<mod>_n' functions for all public wires.\n"); + log("\n"); log(" -tpl <template_file>\n"); log(" use the given template file. the line containing only the token '%%%%'\n"); log(" is replaced with the regular output of this command.\n"); @@ -749,7 +756,7 @@ struct Smt2Backend : public Backend { virtual void execute(std::ostream *&f, std::string filename, std::vector<std::string> args, RTLIL::Design *design) { std::ifstream template_f; - bool bvmode = false, memmode = false, regsmode = false, verbose = false; + bool bvmode = false, memmode = false, regsmode = false, wiresmode = false, verbose = false; log_header("Executing SMT2 backend.\n"); @@ -775,6 +782,10 @@ struct Smt2Backend : public Backend { regsmode = true; continue; } + if (args[argidx] == "-wires") { + wiresmode = true; + continue; + } if (args[argidx] == "-verbose") { verbose = true; continue; @@ -804,7 +815,7 @@ struct Smt2Backend : public Backend { log("Creating SMT-LIBv2 representation of module %s.\n", log_id(module)); - Smt2Worker worker(module, bvmode, memmode, regsmode, verbose); + Smt2Worker worker(module, bvmode, memmode, regsmode, wiresmode, verbose); worker.run(); worker.write(*f); } diff --git a/backends/smt2/smtbmc.py b/backends/smt2/smtbmc.py new file mode 100644 index 000000000..db0bce4bb --- /dev/null +++ b/backends/smt2/smtbmc.py @@ -0,0 +1,196 @@ +#!/usr/bin/env python3 +# +# yosys -- Yosys Open SYnthesis Suite +# +# Copyright (C) 2012 Clifford Wolf <clifford@clifford.at> +# +# Permission to use, copy, modify, and/or distribute this software for any +# purpose with or without fee is hereby granted, provided that the above +# copyright notice and this permission notice appear in all copies. +# +# THE SOFTWARE IS PROVIDED "AS IS" AND THE AUTHOR DISCLAIMS ALL WARRANTIES +# WITH REGARD TO THIS SOFTWARE INCLUDING ALL IMPLIED WARRANTIES OF +# MERCHANTABILITY AND FITNESS. IN NO EVENT SHALL THE AUTHOR BE LIABLE FOR +# ANY SPECIAL, DIRECT, INDIRECT, OR CONSEQUENTIAL DAMAGES OR ANY DAMAGES +# WHATSOEVER RESULTING FROM LOSS OF USE, DATA OR PROFITS, WHETHER IN AN +# ACTION OF CONTRACT, NEGLIGENCE OR OTHER TORTIOUS ACTION, ARISING OUT OF +# OR IN CONNECTION WITH THE USE OR PERFORMANCE OF THIS SOFTWARE. +# + +import os, sys, getopt, re +##yosys-sys-path## +from smtio import smtio, smtopts, mkvcd + +skip_steps = 0 +num_steps = 20 +vcdfile = None +tempind = False +assume_skipped = None +topmod = None +so = smtopts() + + +def usage(): + print(""" +yosys-smtbmc [options] <yosys_smt2_output> + + -t <num_steps>, -t <skip_steps>:<num_steps> + default: skip_steps=0, num_steps=20 + + -u <start_step> + assume asserts in skipped steps in BMC + + -c <vcd_filename> + write counter-example to this VCD file + (hint: use 'write_smt2 -wires' for maximum + coverage of signals in generated VCD file) + + -i + instead of BMC run temporal induction + + -m <module_name> + name of the top module +""" + so.helpmsg()) + sys.exit(1) + + +try: + opts, args = getopt.getopt(sys.argv[1:], so.optstr + "t:u:c:im:") +except: + usage() + +for o, a in opts: + if o == "-t": + match = re.match(r"(\d+):(.*)", a) + if match: + skip_steps = int(match.group(1)) + num_steps = int(match.group(2)) + else: + num_steps = int(a) + elif o == "-u": + assume_skipped = int(a) + elif o == "-c": + vcdfile = a + elif o == "-i": + tempind = True + elif o == "-m": + topmod = a + elif so.handle(o, a): + pass + else: + usage() + +if len(args) != 1: + usage() + + +smt = smtio(opts=so) + +print("%s Solver: %s" % (smt.timestamp(), so.solver)) +smt.setup("QF_AUFBV") + +debug_nets = set() +debug_nets_re = re.compile(r"^; yosys-smt2-(input|output|register|wire) (\S+) (\d+)") + +with open(args[0], "r") as f: + for line in f: + match = debug_nets_re.match(line) + if match: + debug_nets.add(match.group(2)) + if line.startswith("; yosys-smt2-module") and topmod is None: + topmod = line.split()[2] + smt.write(line) + +assert topmod is not None + + +def write_vcd_model(steps): + print("%s Writing model to VCD file." % smt.timestamp()) + + vcd = mkvcd(open(vcdfile, "w")) + for netname in sorted(debug_nets): + width = len(smt.get_net_bin(topmod, netname, "s0")) + vcd.add_net(netname, width) + + for i in range(steps): + vcd.set_time(i) + for netname in debug_nets: + vcd.set_net(netname, smt.get_net_bin(topmod, netname, "s%d" % i)) + + vcd.set_time(steps) + + +if tempind: + retstatus = False + for step in range(num_steps, -1, -1): + smt.write("(declare-fun s%d () %s_s)" % (step, topmod)) + smt.write("(assert (%s_u s%d))" % (topmod, step)) + + if step == num_steps: + smt.write("(assert (not (%s_a s%d)))" % (topmod, step)) + + else: + smt.write("(assert (%s_t s%d s%d))" % (topmod, step, step+1)) + smt.write("(assert (%s_a s%d))" % (topmod, step)) + + if step > num_steps-skip_steps: + print("%s Skipping induction in step %d.." % (smt.timestamp(), step)) + continue + + print("%s Trying induction in step %d.." % (smt.timestamp(), step)) + + if smt.check_sat() == "sat": + if step == 0: + print("%s Temporal induction failed!" % smt.timestamp()) + if vcdfile is not None: + write_vcd_model(num_steps+1) + + else: + print("%s Temporal induction successful." % smt.timestamp()) + retstatus = True + break + + +else: # not tempind + retstatus = True + for step in range(num_steps+1): + smt.write("(declare-fun s%d () %s_s)" % (step, topmod)) + smt.write("(assert (%s_u s%d))" % (topmod, step)) + + if step == 0: + smt.write("(assert (%s_i s0))" % (topmod)) + + else: + smt.write("(assert (%s_t s%d s%d))" % (topmod, step-1, step)) + + if step < skip_steps: + if assume_skipped is not None and step >= assume_skipped: + print("%s Skipping step %d (and assuming pass).." % (smt.timestamp(), step)) + smt.write("(assert (%s_a s%d))" % (topmod, step)) + else: + print("%s Skipping step %d.." % (smt.timestamp(), step)) + continue + + print("%s Checking asserts in step %d.." % (smt.timestamp(), step)) + smt.write("(push 1)") + + smt.write("(assert (not (%s_a s%d)))" % (topmod, step)) + + if smt.check_sat() == "sat": + print("%s BMC failed!" % smt.timestamp()) + if vcdfile is not None: + write_vcd_model(step+1) + retstatus = False + break + + else: # unsat + smt.write("(pop 1)") + smt.write("(assert (%s_a s%d))" % (topmod, step)) + + +smt.write("(exit)") +smt.wait() + +print("%s Status: %s" % (smt.timestamp(), "PASSED" if retstatus else "FAILED (!)")) +sys.exit(0 if retstatus else 1) + diff --git a/backends/smt2/smtio.py b/backends/smt2/smtio.py new file mode 100644 index 000000000..6e8bded77 --- /dev/null +++ b/backends/smt2/smtio.py @@ -0,0 +1,325 @@ +#!/usr/bin/env python3 +# +# yosys -- Yosys Open SYnthesis Suite +# +# Copyright (C) 2012 Clifford Wolf <clifford@clifford.at> +# +# Permission to use, copy, modify, and/or distribute this software for any +# purpose with or without fee is hereby granted, provided that the above +# copyright notice and this permission notice appear in all copies. +# +# THE SOFTWARE IS PROVIDED "AS IS" AND THE AUTHOR DISCLAIMS ALL WARRANTIES +# WITH REGARD TO THIS SOFTWARE INCLUDING ALL IMPLIED WARRANTIES OF +# MERCHANTABILITY AND FITNESS. IN NO EVENT SHALL THE AUTHOR BE LIABLE FOR +# ANY SPECIAL, DIRECT, INDIRECT, OR CONSEQUENTIAL DAMAGES OR ANY DAMAGES +# WHATSOEVER RESULTING FROM LOSS OF USE, DATA OR PROFITS, WHETHER IN AN +# ACTION OF CONTRACT, NEGLIGENCE OR OTHER TORTIOUS ACTION, ARISING OUT OF +# OR IN CONNECTION WITH THE USE OR PERFORMANCE OF THIS SOFTWARE. +# + +import sys +import subprocess +from select import select +from time import time + +class smtio: + def __init__(self, solver=None, debug_print=None, debug_file=None, timeinfo=None, opts=None): + if opts is not None: + self.solver = opts.solver + self.debug_print = opts.debug_print + self.debug_file = opts.debug_file + self.timeinfo = opts.timeinfo + + else: + self.solver = "z3" + self.debug_print = False + self.debug_file = None + self.timeinfo = True + + if solver is not None: + self.solver = solver + + if debug_print is not None: + self.debug_print = debug_print + + if debug_file is not None: + self.debug_file = debug_file + + if timeinfo is not None: + self.timeinfo = timeinfo + + if self.solver == "yices": + popen_vargs = ['yices-smt2', '--incremental'] + + if self.solver == "z3": + popen_vargs = ['z3', '-smt2', '-in'] + + if self.solver == "cvc4": + popen_vargs = ['cvc4', '--incremental', '--lang', 'smt2'] + + if self.solver == "mathsat": + popen_vargs = ['mathsat'] + + self.p = subprocess.Popen(popen_vargs, stdin=subprocess.PIPE, stdout=subprocess.PIPE, stderr=subprocess.STDOUT) + self.start_time = time() + + def setup(self, logic="ALL", info=None): + self.write("(set-logic %s)" % logic) + if info is not None: + self.write("(set-info :source |%s|)" % info) + self.write("(set-info :smt-lib-version 2.5)") + self.write("(set-info :category \"industrial\")") + + def timestamp(self): + secs = int(time() - self.start_time) + return "## %6d %3d:%02d:%02d " % (secs, secs // (60*60), (secs // 60) % 60, secs % 60) + + def write(self, stmt): + stmt = stmt.strip() + if self.debug_print: + print("> %s" % stmt) + if self.debug_file: + print(stmt, file=self.debug_file) + self.debug_file.flush() + self.p.stdin.write(bytes(stmt + "\n", "ascii")) + self.p.stdin.flush() + + def read(self): + stmt = [] + count_brackets = 0 + + while True: + line = self.p.stdout.readline().decode("ascii").strip() + count_brackets += line.count("(") + count_brackets -= line.count(")") + stmt.append(line) + if self.debug_print: + print("< %s" % line) + if count_brackets == 0: + break + if not self.p.poll(): + print("SMT Solver terminated unexpectedly: %s" % "".join(stmt)) + sys.exit(1) + + stmt = "".join(stmt) + if stmt.startswith("(error"): + print("SMT Solver Error: %s" % stmt, file=sys.stderr) + sys.exit(1) + + return stmt + + def check_sat(self): + if self.debug_print: + print("> (check-sat)") + if self.debug_file: + print("; running check-sat..", file=self.debug_file) + self.debug_file.flush() + + self.p.stdin.write(bytes("(check-sat)\n", "ascii")) + self.p.stdin.flush() + + if self.timeinfo: + i = 0 + s = "/-\|" + + count = 0 + num_bs = 0 + while select([self.p.stdout], [], [], 0.1) == ([], [], []): + count += 1 + + if count < 25: + continue + + if count % 10 == 0 or count == 25: + secs = count // 10 + + if secs < 60: + m = "(%d seconds)" % secs + elif secs < 60*60: + m = "(%d seconds -- %d:%02d)" % (secs, secs // 60, secs % 60) + else: + m = "(%d seconds -- %d:%02d:%02d)" % (secs, secs // (60*60), (secs // 60) % 60, secs % 60) + + print("%s %s %c" % ("\b \b" * num_bs, m, s[i]), end="", file=sys.stderr) + num_bs = len(m) + 3 + + else: + print("\b" + s[i], end="", file=sys.stderr) + + sys.stderr.flush() + i = (i + 1) % len(s) + + if num_bs != 0: + print("\b \b" * num_bs, end="", file=sys.stderr) + sys.stderr.flush() + + result = self.read() + if self.debug_file: + print("(set-info :status %s)" % result, file=self.debug_file) + print("(check-sat)", file=self.debug_file) + self.debug_file.flush() + return result + + def parse(self, stmt): + def worker(stmt): + if stmt[0] == '(': + expr = [] + cursor = 1 + while stmt[cursor] != ')': + el, le = worker(stmt[cursor:]) + expr.append(el) + cursor += le + return expr, cursor+1 + + if stmt[0] == '|': + expr = "|" + cursor = 1 + while stmt[cursor] != '|': + expr += stmt[cursor] + cursor += 1 + expr += "|" + return expr, cursor+1 + + if stmt[0] in [" ", "\t", "\r", "\n"]: + el, le = worker(stmt[1:]) + return el, le+1 + + expr = "" + cursor = 0 + while stmt[cursor] not in ["(", ")", "|", " ", "\t", "\r", "\n"]: + expr += stmt[cursor] + cursor += 1 + return expr, cursor + return worker(stmt)[0] + + def bv2hex(self, v): + h = "" + v = bv2bin(v) + while len(v) > 0: + d = 0 + if len(v) > 0 and v[-1] == "1": d += 1 + if len(v) > 1 and v[-2] == "1": d += 2 + if len(v) > 2 and v[-3] == "1": d += 4 + if len(v) > 3 and v[-4] == "1": d += 8 + h = hex(d)[2:] + h + if len(v) < 4: break + v = v[:-4] + return h + + def bv2bin(self, v): + if v == "true": return "1" + if v == "false": return "0" + if v.startswith("#b"): + return v[2:] + if v.startswith("#x"): + digits = [] + for d in v[2:]: + if d == "0": digits.append("0000") + if d == "1": digits.append("0001") + if d == "2": digits.append("0010") + if d == "3": digits.append("0011") + if d == "4": digits.append("0100") + if d == "5": digits.append("0101") + if d == "6": digits.append("0110") + if d == "7": digits.append("0111") + if d == "8": digits.append("1000") + if d == "9": digits.append("1001") + if d in ("a", "A"): digits.append("1010") + if d in ("b", "B"): digits.append("1011") + if d in ("c", "C"): digits.append("1100") + if d in ("d", "D"): digits.append("1101") + if d in ("e", "E"): digits.append("1110") + if d in ("f", "F"): digits.append("1111") + return "".join(digits) + assert False + + def get(self, expr): + self.write("(get-value (%s))" % (expr)) + return self.parse(self.read())[0][1] + + def get_net(self, mod_name, net_name, state_name): + return self.get("(|%s_n %s| %s)" % (mod_name, net_name, state_name)) + + def get_net_bool(self, mod_name, net_name, state_name): + v = self.get_net(mod_name, net_name, state_name) + assert v in ["true", "false"] + return 1 if v == "true" else 0 + + def get_net_hex(self, mod_name, net_name, state_name): + return self.bv2hex(self.get_net(mod_name, net_name, state_name)) + + def get_net_bin(self, mod_name, net_name, state_name): + return self.bv2bin(self.get_net(mod_name, net_name, state_name)) + + def wait(self): + self.p.wait() + + +class smtopts: + def __init__(self): + self.optstr = "s:d:vp" + self.solver = "z3" + self.debug_print = False + self.debug_file = None + self.timeinfo = True + + def handle(self, o, a): + if o == "-s": + self.solver = a + elif o == "-v": + self.debug_print = True + elif o == "-p": + self.timeinfo = True + elif o == "-d": + self.debug_file = open(a, "w") + else: + return False + return True + + def helpmsg(self): + return """ + -s <solver> + set SMT solver: z3, cvc4, yices, mathsat + default: z3 + + -v + enable debug output + + -p + disable timer display during solving + + -d <filename> + write smt2 statements to file +""" + + +class mkvcd: + def __init__(self, f): + self.f = f + self.t = -1 + self.nets = dict() + + def add_net(self, name, width): + assert self.t == -1 + key = "n%d" % len(self.nets) + self.nets[name] = (key, width) + + def set_net(self, name, bits): + assert name in self.nets + assert self.t >= 0 + print("b%s %s" % (bits, self.nets[name][0]), file=self.f) + + def set_time(self, t): + assert t >= self.t + if t != self.t: + if self.t == -1: + print("$var event 1 ! smt_clock $end", file=self.f) + for name in sorted(self.nets): + key, width = self.nets[name] + print("$var wire %d %s %s $end" % (width, key, name), file=self.f) + print("$enddefinitions $end", file=self.f) + self.t = t + assert self.t >= 0 + print("#%d" % self.t, file=self.f) + print("1!", file=self.f) + diff --git a/backends/smv/smv.cc b/backends/smv/smv.cc index fdf022c5a..b29a88ac2 100644 --- a/backends/smv/smv.cc +++ b/backends/smv/smv.cc @@ -244,13 +244,13 @@ struct SmvWorker int width_y = GetSize(cell->getPort("\\Y")); int shift_b_width = GetSize(sig_b); - int width_ay = std::max(GetSize(sig_a), width_y); + int width_ay = max(GetSize(sig_a), width_y); int width = width_ay; for (int i = 1, j = 0;; i <<= 1, j++) if (width_ay < i) { width = i-1; - shift_b_width = std::min(shift_b_width, j); + shift_b_width = min(shift_b_width, j); break; } @@ -361,8 +361,8 @@ struct SmvWorker if (cell->type.in("$div", "$mod")) { int width_y = GetSize(cell->getPort("\\Y")); - int width = std::max(width_y, GetSize(cell->getPort("\\A"))); - width = std::max(width, GetSize(cell->getPort("\\B"))); + int width = max(width_y, GetSize(cell->getPort("\\A"))); + width = max(width, GetSize(cell->getPort("\\B"))); string expr_a, expr_b, op; if (cell->type == "$div") op = "/"; @@ -384,7 +384,7 @@ struct SmvWorker if (cell->type.in("$eq", "$ne", "$eqx", "$nex", "$lt", "$le", "$ge", "$gt")) { - int width = std::max(GetSize(cell->getPort("\\A")), GetSize(cell->getPort("\\B"))); + int width = max(GetSize(cell->getPort("\\A")), GetSize(cell->getPort("\\B"))); string expr_a, expr_b, op; if (cell->type == "$eq") op = "="; diff --git a/backends/verilog/verilog_backend.cc b/backends/verilog/verilog_backend.cc index c04389f63..10f10e3cd 100644 --- a/backends/verilog/verilog_backend.cc +++ b/backends/verilog/verilog_backend.cc @@ -165,12 +165,13 @@ void dump_const(std::ostream &f, const RTLIL::Const &data, int width = -1, int o log_assert(i < (int)data.bits.size()); if (data.bits[i] != RTLIL::S0 && data.bits[i] != RTLIL::S1) goto dump_bits; - if (data.bits[i] == RTLIL::S1 && (i - offset) == 31) - goto dump_bits; if (data.bits[i] == RTLIL::S1) val |= 1 << (i - offset); } - f << stringf("32'%sd %d", set_signed ? "s" : "", val); + if (set_signed && val < 0) + f << stringf("-32'sd %u", -val); + else + f << stringf("32'%sd %u", set_signed ? "s" : "", val); } else { dump_bits: f << stringf("%d'%sb", width, set_signed ? "s" : ""); @@ -805,15 +806,15 @@ bool dump_cell_expr(std::ostream &f, std::string indent, RTLIL::Cell *cell) // initial begin // memid[0] <= ... // end - int mem_val; f << stringf("%s" "reg [%d:%d] %s [%d:%d];\n", indent.c_str(), width-1, 0, mem_id.c_str(), size-1, 0); if (use_init) { f << stringf("%s" "initial begin\n", indent.c_str()); for (int i=0; i<size; i++) { - mem_val = cell->parameters["\\INIT"].extract(i*width, width).as_int(); - f << stringf("%s" " %s[%d] <= %d'd%d;\n", indent.c_str(), mem_id.c_str(), i, width, mem_val); + f << stringf("%s" " %s[%d] <= ", indent.c_str(), mem_id.c_str(), i); + dump_const(f, cell->parameters["\\INIT"].extract(i*width, width)); + f << stringf(";\n"); } f << stringf("%s" "end\n", indent.c_str()); } @@ -884,7 +885,7 @@ bool dump_cell_expr(std::ostream &f, std::string indent, RTLIL::Cell *cell) std::ostringstream os; dump_sigspec(os, sig_rd_data); std::string line = stringf("assign %s = %s[%s];\n", os.str().c_str(), mem_id.c_str(), temp_id.c_str()); - clk_to_lof_body[clk_domain_str].push_back(line); + clk_to_lof_body[""].push_back(line); } } else { // for non-clocked read-ports make something like: |