diff options
| -rw-r--r-- | backends/smt2/smt2.cc | 8 | ||||
| -rw-r--r-- | backends/smt2/smtbmc.py | 52 | ||||
| -rw-r--r-- | backends/smt2/smtio.py | 161 | ||||
| -rw-r--r-- | frontends/ast/genrtlil.cc | 10 | ||||
| -rw-r--r-- | frontends/ast/simplify.cc | 133 | ||||
| -rw-r--r-- | frontends/liberty/liberty.cc | 78 | ||||
| -rw-r--r-- | passes/tests/test_autotb.cc | 18 | ||||
| -rwxr-xr-x | tests/tools/autotest.sh | 35 |
8 files changed, 388 insertions, 107 deletions
diff --git a/backends/smt2/smt2.cc b/backends/smt2/smt2.cc index e07515133..9a25f3a23 100644 --- a/backends/smt2/smt2.cc +++ b/backends/smt2/smt2.cc @@ -998,7 +998,7 @@ struct Smt2Backend : public Backend { continue; } if (args[argidx] == "-nomem") { - bvmode = false; + memmode = false; continue; } if (args[argidx] == "-wires") { @@ -1027,6 +1027,12 @@ struct Smt2Backend : public Backend { *f << stringf("; SMT-LIBv2 description generated by %s\n", yosys_version_str); + if (!bvmode) + *f << stringf("; yosys-smt2-nobv\n"); + + if (!memmode) + *f << stringf("; yosys-smt2-nomem\n"); + std::vector<RTLIL::Module*> sorted_modules; // extract module dependencies diff --git a/backends/smt2/smtbmc.py b/backends/smt2/smtbmc.py index fa4966089..bb763647c 100644 --- a/backends/smt2/smtbmc.py +++ b/backends/smt2/smtbmc.py @@ -35,6 +35,7 @@ dumpall = False assume_skipped = None final_only = False topmod = None +noinfo = False so = SmtOpts() @@ -60,6 +61,10 @@ yosys-smtbmc [options] <yosys_smt2_output> --smtc <constr_filename> read constraints file + --noinfo + only run the core proof, do not collect and print any + additional information (e.g. which assert failed) + --final-only only check final constraints, assume base case @@ -89,7 +94,7 @@ yosys-smtbmc [options] <yosys_smt2_output> try: opts, args = getopt.getopt(sys.argv[1:], so.shortopts + "t:igm:", so.longopts + - ["final-only", "assume-skipped=", "smtc=", "dump-vcd=", "dump-vlogtb=", "dump-smtc=", "dump-all"]) + ["final-only", "assume-skipped=", "smtc=", "dump-vcd=", "dump-vlogtb=", "dump-smtc=", "dump-all", "noinfo"]) except: usage() @@ -121,6 +126,8 @@ for o, a in opts: outconstr = a elif o == "--dump-all": dumpall = True + elif o == "--noinfo": + noinfo = True elif o == "-i": tempind = True elif o == "-g": @@ -136,11 +143,6 @@ if len(args) != 1: usage() -if tempind and len(inconstr) != 0: - print("Error: options -i and --smtc are exclusive.") - sys.exit(1) - - constr_final_start = None constr_asserts = defaultdict(list) constr_assumes = defaultdict(list) @@ -163,7 +165,8 @@ for fn in inconstr: if tokens[0] == "initial": current_states = set() - current_states.add(0) + if not tempind: + current_states.add(0) continue if tokens[0] == "final": @@ -182,20 +185,21 @@ for fn in inconstr: if tokens[0] == "state": current_states = set() - for token in tokens[1:]: - tok = token.split(":") - if len(tok) == 1: - current_states.add(int(token)) - elif len(tok) == 2: - lower = int(tok[0]) - if tok[1] == "*": - upper = num_steps + if not tempind: + for token in tokens[1:]: + tok = token.split(":") + if len(tok) == 1: + current_states.add(int(token)) + elif len(tok) == 2: + lower = int(tok[0]) + if tok[1] == "*": + upper = num_steps + else: + upper = int(tok[1]) + for i in range(lower, upper+1): + current_states.add(i) else: - upper = int(tok[1]) - for i in range(lower, upper+1): - current_states.add(i) - else: - assert 0 + assert 0 continue if tokens[0] == "always": @@ -281,12 +285,10 @@ def print_msg(msg): sys.stdout.flush() print_msg("Solver: %s" % (so.solver)) -smt.setup("QF_AUFBV") with open(args[0], "r") as f: for line in f: smt.write(line) - smt.info(line) if topmod is None: topmod = smt.topmod @@ -490,6 +492,7 @@ def print_failed_asserts_worker(mod, state, path): def print_failed_asserts(state, final=False): + if noinfo: return loc_list, expr_list, value_list = get_constr_expr(constr_asserts, state, final=final, getvalues=True) for loc, expr, value in zip(loc_list, expr_list, value_list): @@ -511,6 +514,7 @@ def print_anyconsts_worker(mod, state, path): def print_anyconsts(state): + if noinfo: return print_anyconsts_worker(topmod, "s%d" % state, topmod) @@ -522,13 +526,15 @@ if tempind: smt.write("(assert (|%s_u| s%d))" % (topmod, step)) smt.write("(assert (|%s_h| s%d))" % (topmod, step)) smt.write("(assert (not (|%s_is| s%d)))" % (topmod, step)) + smt.write("(assert %s)" % get_constr_expr(constr_assumes, step)) if step == num_steps: - smt.write("(assert (not (|%s_a| s%d)))" % (topmod, step)) + smt.write("(assert (not (and (|%s_a| s%d) %s)))" % (topmod, step, get_constr_expr(constr_asserts, step))) else: smt.write("(assert (|%s_t| s%d s%d))" % (topmod, step, step+1)) smt.write("(assert (|%s_a| s%d))" % (topmod, step)) + smt.write("(assert %s)" % get_constr_expr(constr_asserts, step)) if step > num_steps-skip_steps: print_msg("Skipping induction in step %d.." % (step)) diff --git a/backends/smt2/smtio.py b/backends/smt2/smtio.py index 5d0a78485..58554572d 100644 --- a/backends/smt2/smtio.py +++ b/backends/smt2/smtio.py @@ -47,11 +47,19 @@ class SmtModInfo: class SmtIo: - def __init__(self, solver=None, debug_print=None, debug_file=None, timeinfo=None, unroll=None, opts=None): + def __init__(self, opts=None): + self.logic = None + self.logic_qf = True + self.logic_ax = True + self.logic_uf = True + self.logic_bv = True + if opts is not None: + self.logic = opts.logic self.solver = opts.solver self.debug_print = opts.debug_print self.debug_file = opts.debug_file + self.dummy_file = opts.dummy_file self.timeinfo = opts.timeinfo self.unroll = opts.unroll @@ -59,24 +67,10 @@ class SmtIo: self.solver = "z3" self.debug_print = False self.debug_file = None + self.dummy_file = None self.timeinfo = True self.unroll = False - 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 unroll is not None: - self.unroll = unroll - if self.solver == "yices": popen_vargs = ['yices-smt2', '--incremental'] @@ -93,7 +87,16 @@ class SmtIo: popen_vargs = ['boolector', '--smt2', '-i'] self.unroll = True + if self.solver == "dummy": + assert self.dummy_file is not None + self.dummy_fd = open(self.dummy_file, "r") + else: + if self.dummy_file is not None: + self.dummy_fd = open(self.dummy_file, "w") + self.p = subprocess.Popen(popen_vargs, stdin=subprocess.PIPE, stdout=subprocess.PIPE, stderr=subprocess.STDOUT) + if self.unroll: + self.logic_uf = False self.unroll_idcnt = 0 self.unroll_buffer = "" self.unroll_sorts = set() @@ -102,20 +105,26 @@ class SmtIo: self.unroll_cache = dict() self.unroll_stack = list() - self.p = subprocess.Popen(popen_vargs, stdin=subprocess.PIPE, stdout=subprocess.PIPE, stderr=subprocess.STDOUT) self.start_time = time() self.modinfo = dict() self.curmod = None self.topmod = None + self.setup_done = False + + def setup(self): + assert not self.setup_done + + if self.logic is None: + self.logic = "" + if self.logic_qf: self.logic += "QF_" + if self.logic_ax: self.logic += "A" + if self.logic_uf: self.logic += "UF" + if self.logic_bv: self.logic += "BV" - def setup(self, logic="ALL", info=None): + self.setup_done = True self.write("(set-option :produce-models true)") - 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\")") + self.write("(set-logic %s)" % self.logic) def timestamp(self): secs = int(time() - self.start_time) @@ -171,6 +180,11 @@ class SmtIo: return stmt def write(self, stmt, unroll=True): + if stmt.startswith(";"): + self.info(stmt) + elif not self.setup_done: + self.setup() + stmt = stmt.strip() if unroll and self.unroll: @@ -231,8 +245,9 @@ class SmtIo: print(stmt, file=self.debug_file) self.debug_file.flush() - self.p.stdin.write(bytes(stmt + "\n", "ascii")) - self.p.stdin.flush() + if self.solver != "dummy": + self.p.stdin.write(bytes(stmt + "\n", "ascii")) + self.p.stdin.flush() def info(self, stmt): if not stmt.startswith("; yosys-smt2-"): @@ -240,6 +255,14 @@ class SmtIo: fields = stmt.split() + if fields[1] == "yosys-smt2-nomem": + if self.logic is None: + self.logic_ax = False + + if fields[1] == "yosys-smt2-nobv": + if self.logic is None: + self.logic_bv = False + if fields[1] == "yosys-smt2-module": self.curmod = fields[2] self.modinfo[self.curmod] = SmtModInfo() @@ -303,15 +326,22 @@ class SmtIo: count_brackets = 0 while True: - line = self.p.stdout.readline().decode("ascii").strip() + if self.solver == "dummy": + line = self.dummy_fd.readline().strip() + else: + line = self.p.stdout.readline().decode("ascii").strip() + if self.dummy_file is not None: + self.dummy_fd.write(line + "\n") + count_brackets += line.count("(") count_brackets -= line.count(")") stmt.append(line) + if self.debug_print: print("< %s" % line) if count_brackets == 0: break - if self.p.poll(): + if self.solver != "dummy" and self.p.poll(): print("SMT Solver terminated unexpectedly: %s" % "".join(stmt)) sys.exit(1) @@ -329,43 +359,44 @@ class SmtIo: 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.solver != "dummy": + self.p.stdin.write(bytes("(check-sat)\n", "ascii")) + self.p.stdin.flush() - if self.timeinfo: - i = 0 - s = "/-\|" + if self.timeinfo: + i = 0 + s = "/-\|" - count = 0 - num_bs = 0 - while select([self.p.stdout], [], [], 0.1) == ([], [], []): - count += 1 + count = 0 + num_bs = 0 + while select([self.p.stdout], [], [], 0.1) == ([], [], []): + count += 1 - if count < 25: - continue + if count < 25: + continue - if count % 10 == 0 or count == 25: - secs = count // 10 + 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) + 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 + 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) + else: + print("\b" + s[i], end="", file=sys.stderr) - sys.stderr.flush() - i = (i + 1) % len(s) + sys.stderr.flush() + i = (i + 1) % len(s) - if num_bs != 0: - print("\b \b" * num_bs, end="", file=sys.stderr) - sys.stderr.flush() + if num_bs != 0: + print("\b \b" * num_bs, end="", file=sys.stderr) + sys.stderr.flush() result = self.read() if self.debug_file: @@ -524,18 +555,21 @@ class SmtIo: return [self.bv2bin(v) for v in self.get_net_list(mod_name, net_path_list, state_name)] def wait(self): - self.p.wait() + if self.solver != "dummy": + self.p.wait() class SmtOpts: def __init__(self): self.shortopts = "s:v" - self.longopts = ["unroll", "no-progress", "dump-smt2="] + self.longopts = ["unroll", "no-progress", "dump-smt2=", "logic=", "dummy="] self.solver = "z3" self.debug_print = False self.debug_file = None + self.dummy_file = None self.unroll = False self.timeinfo = True + self.logic = None def handle(self, o, a): if o == "-s": @@ -548,6 +582,10 @@ class SmtOpts: self.timeinfo = True elif o == "--dump-smt2": self.debug_file = open(a, "w") + elif o == "--logic": + self.logic = a + elif o == "--dummy": + self.dummy_file = a else: return False return True @@ -555,9 +593,16 @@ class SmtOpts: def helpmsg(self): return """ -s <solver> - set SMT solver: z3, cvc4, yices, mathsat + set SMT solver: z3, cvc4, yices, mathsat, boolector, dummy default: z3 + --logic <smt2_logic> + use the specified SMT2 logic (e.g. QF_AUFBV) + + --dummy <filename> + if solver is "dummy", read solver output from that file + otherwise: write solver output to that file + -v enable debug output diff --git a/frontends/ast/genrtlil.cc b/frontends/ast/genrtlil.cc index d00738ecd..3c57162aa 100644 --- a/frontends/ast/genrtlil.cc +++ b/frontends/ast/genrtlil.cc @@ -765,6 +765,16 @@ void AstNode::detectSignWidthWorker(int &width_hint, bool &sign_hint, bool *foun } break; } + if (str == "\\$past") { + if (GetSize(children) > 0) { + sub_width_hint = 0; + sub_sign_hint = true; + children.at(0)->detectSignWidthWorker(sub_width_hint, sub_sign_hint); + width_hint = max(width_hint, sub_width_hint); + sign_hint = false; + } + break; + } /* fall through */ // everything should have been handled above -> print error if not. diff --git a/frontends/ast/simplify.cc b/frontends/ast/simplify.cc index 8387c11c6..57aa648ce 100644 --- a/frontends/ast/simplify.cc +++ b/frontends/ast/simplify.cc @@ -63,7 +63,7 @@ bool AstNode::simplify(bool const_fold, bool at_zero, bool in_lvalue, int stage, #if 0 log("-------------\n"); - log("AST simplify[%d] depth %d at %s:%d,\n", stage, recursion_counter, filename.c_str(), linenum); + log("AST simplify[%d] depth %d at %s:%d on %s %p:\n", stage, recursion_counter, filename.c_str(), linenum, type2str(type).c_str(), this); log("const_fold=%d, at_zero=%d, in_lvalue=%d, stage=%d, width_hint=%d, sign_hint=%d, in_param=%d\n", int(const_fold), int(at_zero), int(in_lvalue), int(stage), int(width_hint), int(sign_hint), int(in_param)); // dumpAst(NULL, "> "); @@ -522,6 +522,11 @@ bool AstNode::simplify(bool const_fold, bool at_zero, bool in_lvalue, int stage, children_are_self_determined = true; break; + case AST_FCALL: + case AST_TCALL: + children_are_self_determined = true; + break; + default: width_hint = -1; sign_hint = false; @@ -537,6 +542,9 @@ bool AstNode::simplify(bool const_fold, bool at_zero, bool in_lvalue, int stage, detectSignWidth(width_hint, sign_hint); } + if (type == AST_FCALL && str == "\\$past") + detectSignWidth(width_hint, sign_hint); + if (type == AST_TERNARY) { int width_hint_left, width_hint_right; bool sign_hint_left, sign_hint_right; @@ -1682,9 +1690,128 @@ skip_dynamic_range_lvalue_expansion:; goto apply_newNode; } + if (str == "\\$past") + { + if (width_hint <= 0) + goto replace_fcall_later; + + int num_steps = 1; + + if (GetSize(children) != 1 && GetSize(children) != 2) + log_error("System function %s got %d arguments, expected 1 or 2 at %s:%d.\n", + RTLIL::unescape_id(str).c_str(), int(children.size()), filename.c_str(), linenum); + + if (!current_always_clocked) + log_error("System function %s is only allowed in clocked blocks at %s:%d.\n", + RTLIL::unescape_id(str).c_str(), filename.c_str(), linenum); + + if (GetSize(children) == 2) + { + AstNode *buf = children[1]->clone(); + while (buf->simplify(true, false, false, stage, width_hint, sign_hint, false)) { } + if (buf->type != AST_CONSTANT) + log_error("Failed to evaluate system function `%s' with non-constant value at %s:%d.\n", str.c_str(), filename.c_str(), linenum); + + num_steps = buf->asInt(true); + delete buf; + } + + AstNode *block = nullptr; + + for (auto child : current_always->children) + if (child->type == AST_BLOCK) + block = child; + + log_assert(block != nullptr); + + int myidx = autoidx++; + AstNode *outreg = nullptr; + + for (int i = 0; i < num_steps; i++) + { + AstNode *reg = new AstNode(AST_WIRE, new AstNode(AST_RANGE, + mkconst_int(width_hint-1, true), mkconst_int(0, true))); + + reg->str = stringf("$past$%s:%d$%d$%d", filename.c_str(), linenum, myidx, i); + reg->is_reg = true; + + current_ast_mod->children.push_back(reg); + + while (reg->simplify(true, false, false, 1, -1, false, false)) { } + + AstNode *regid = new AstNode(AST_IDENTIFIER); + regid->str = reg->str; + regid->id2ast = reg; + + AstNode *rhs = nullptr; + + if (outreg == nullptr) { + rhs = children.at(0)->clone(); + } else { + rhs = new AstNode(AST_IDENTIFIER); + rhs->str = outreg->str; + rhs->id2ast = outreg; + } + + block->children.push_back(new AstNode(AST_ASSIGN_LE, regid, rhs)); + outreg = reg; + } + + newNode = new AstNode(AST_IDENTIFIER); + newNode->str = outreg->str; + newNode->id2ast = outreg; + goto apply_newNode; + } + + if (str == "\\$stable" || str == "\\$rose" || str == "\\$fell") + { + if (GetSize(children) != 1) + log_error("System function %s got %d arguments, expected 1 at %s:%d.\n", + RTLIL::unescape_id(str).c_str(), int(children.size()), filename.c_str(), linenum); + + if (!current_always_clocked) + log_error("System function %s is only allowed in clocked blocks at %s:%d.\n", + RTLIL::unescape_id(str).c_str(), filename.c_str(), linenum); + + AstNode *present = children.at(0)->clone(); + AstNode *past = clone(); + past->str = "\\$past"; + + if (str == "\\$stable") + newNode = new AstNode(AST_EQ, past, present); + + else if (str == "\\$rose") + newNode = new AstNode(AST_LOGIC_AND, new AstNode(AST_LOGIC_NOT, past), present); + + else if (str == "\\$fell") + newNode = new AstNode(AST_LOGIC_AND, past, new AstNode(AST_LOGIC_NOT, present)); + + else + log_abort(); + + goto apply_newNode; + } + + if (str == "\\$rose" || str == "\\$fell") + { + if (GetSize(children) != 1) + log_error("System function %s got %d arguments, expected 1 at %s:%d.\n", + RTLIL::unescape_id(str).c_str(), int(children.size()), filename.c_str(), linenum); + + if (!current_always_clocked) + log_error("System function %s is only allowed in clocked blocks at %s:%d.\n", + RTLIL::unescape_id(str).c_str(), filename.c_str(), linenum); + + newNode = new AstNode(AST_EQ, children.at(0)->clone(), clone()); + newNode->children.at(1)->str = "\\$past"; + goto apply_newNode; + } + // $anyconst is mapped in AstNode::genRTLIL() - if (str == "\\$anyconst") + if (str == "\\$anyconst") { + recursion_counter--; return false; + } if (str == "\\$clog2") { @@ -2092,6 +2219,8 @@ skip_dynamic_range_lvalue_expansion:; did_something = true; } +replace_fcall_later:; + // perform const folding when activated if (const_fold) { diff --git a/frontends/liberty/liberty.cc b/frontends/liberty/liberty.cc index 0be58b6da..73d927fab 100644 --- a/frontends/liberty/liberty.cc +++ b/frontends/liberty/liberty.cc @@ -469,6 +469,46 @@ struct LibertyFrontend : public Frontend { LibertyParser parser(*f); int cell_count = 0; + std::map<std::string, std::tuple<int, int, bool>> type_map; + + for (auto type_node : parser.ast->children) + { + if (type_node->id != "type" || type_node->args.size() != 1) + continue; + + std::string type_name = type_node->args.at(0); + int bit_width = -1, bit_from = -1, bit_to = -1; + bool upto = false; + + for (auto child : type_node->children) + { + if (child->id == "base_type" && child->value != "array") + goto next_type; + + if (child->id == "data_type" && child->value != "bit") + goto next_type; + + if (child->id == "bit_width") + bit_width = atoi(child->value.c_str()); + + if (child->id == "bit_from") + bit_from = atoi(child->value.c_str()); + + if (child->id == "bit_to") + bit_to = atoi(child->value.c_str()); + + if (child->id == "downto" && (child->value == "0" || child->value == "false" || child->value == "FALSE")) + upto = true; + } + + if (bit_width != (std::max(bit_from, bit_to) - std::min(bit_from, bit_to) + 1)) + log_error("Incompatible array type '%s': bit_width=%d, bit_from=%d, bit_to=%d.\n", + type_name.c_str(), bit_width, bit_from, bit_to); + + type_map[type_name] = std::tuple<int, int, bool>(bit_width, std::min(bit_from, bit_to), upto); + next_type:; + } + for (auto cell : parser.ast->children) { if (cell->id != "cell" || cell->args.size() != 1) @@ -494,13 +534,14 @@ struct LibertyFrontend : public Frontend { module->attributes[attr] = 1; for (auto node : cell->children) + { if (node->id == "pin" && node->args.size() == 1) { LibertyAst *dir = node->find("direction"); if (!dir || (dir->value != "input" && dir->value != "output" && dir->value != "inout" && dir->value != "internal")) { if (!flag_ignore_miss_dir) { - log_error("Missing or invalid direction for pin %s of cell %s.\n", node->args.at(0).c_str(), log_id(module->name)); + log_error("Missing or invalid direction for pin %s on cell %s.\n", node->args.at(0).c_str(), log_id(module->name)); } else { log("Ignoring cell %s with missing or invalid direction for pin %s.\n", log_id(module->name), node->args.at(0).c_str()); delete module; @@ -511,6 +552,41 @@ struct LibertyFrontend : public Frontend { module->addWire(RTLIL::escape_id(node->args.at(0))); } + if (node->id == "bus" && node->args.size() == 1) + { + if (!flag_lib) + log_error("Error in cell %s: bus interfaces are only supported in -lib mode.\n", log_id(cell_name)); + + LibertyAst *dir = node->find("direction"); + + if (!dir || (dir->value != "input" && dir->value != "output" && dir->value != "inout" && dir->value != "internal")) + log_error("Missing or invalid direction for bus %s on cell %s.\n", node->args.at(0).c_str(), log_id(module->name)); + + if (dir->value == "internal") + continue; + + LibertyAst *bus_type_node = node->find("bus_type"); + + if (!bus_type_node || !type_map.count(bus_type_node->value)) + log_error("Unkown or unsupported type for bus interface %s on cell %s.\n", + node->args.at(0).c_str(), log_id(cell_name)); + + int bus_type_width = std::get<0>(type_map.at(bus_type_node->value)); + int bus_type_offset = std::get<1>(type_map.at(bus_type_node->value)); + bool bus_type_upto = std::get<2>(type_map.at(bus_type_node->value)); + + Wire *wire = module->addWire(RTLIL::escape_id(node->args.at(0)), bus_type_width); + wire->start_offset = bus_type_offset; + wire->upto = bus_type_upto; + + if (dir->value == "input" || dir->value == "inout") + wire->port_input = true; + + if (dir->value == "output" || dir->value == "inout") + wire->port_output = true; + } + } + for (auto node : cell->children) { if (!flag_lib) { diff --git a/passes/tests/test_autotb.cc b/passes/tests/test_autotb.cc index 69e2e76d7..cb31056f4 100644 --- a/passes/tests/test_autotb.cc +++ b/passes/tests/test_autotb.cc @@ -220,59 +220,65 @@ static void autotest(std::ostream &f, RTLIL::Design *design, int num_iter, int s for (auto it = signal_in.begin(); it != signal_in.end(); it++) { f << stringf("%s %s", it == signal_in.begin() ? "" : ",", it->first.c_str()); int len = it->second; + header2 += ", \""; if (len > 1) header2 += "/", len--; while (len > 1) header2 += "-", len--; if (len > 0) header2 += shorthand, len--; + header2 += "\""; header1.push_back(" " + it->first); header1.back()[0] = shorthand; shorthand = shorthand == 'Z' ? 'A' : shorthand+1; } else { f << stringf(" 1'bx"); - header2 += "#"; + header2 += ", \"#\""; } f << stringf(" }, {"); - header2 += " "; + header2 += ", \" \""; if (signal_clk.size()) { for (auto it = signal_clk.begin(); it != signal_clk.end(); it++) { f << stringf("%s %s", it == signal_clk.begin() ? "" : ",", it->first.c_str()); int len = it->second; + header2 += ", \""; if (len > 1) header2 += "/", len--; while (len > 1) header2 += "-", len--; if (len > 0) header2 += shorthand, len--; + header2 += "\""; header1.push_back(" " + it->first); header1.back()[0] = shorthand; shorthand = shorthand == 'Z' ? 'A' : shorthand+1; } } else { f << stringf(" 1'bx"); - header2 += "#"; + header2 += ", \"#\""; } f << stringf(" }, {"); - header2 += " "; + header2 += ", \" \""; if (signal_out.size()) { for (auto it = signal_out.begin(); it != signal_out.end(); it++) { f << stringf("%s %s", it == signal_out.begin() ? "" : ",", it->first.c_str()); int len = it->second; + header2 += ", \""; if (len > 1) header2 += "/", len--; while (len > 1) header2 += "-", len--; if (len > 0) header2 += shorthand, len--; + header2 += "\""; header1.push_back(" " + it->first); header1.back()[0] = shorthand; shorthand = shorthand == 'Z' ? 'A' : shorthand+1; } } else { f << stringf(" 1'bx"); - header2 += "#"; + header2 += ", \"#\""; } f << stringf(" }, $time, i);\n"); f << stringf("end\n"); @@ -284,7 +290,7 @@ static void autotest(std::ostream &f, RTLIL::Design *design, int num_iter, int s for (auto &hdr : header1) f << stringf("\t$fdisplay(file, \"#OUT# %s\");\n", hdr.c_str()); f << stringf("\t$fdisplay(file, \"#OUT#\");\n"); - f << stringf("\t$fdisplay(file, \"#OUT# %s\");\n", header2.c_str()); + f << stringf("\t$fdisplay(file, {\"#OUT# \"%s});\n", header2.c_str()); f << stringf("end\n"); f << stringf("endtask\n\n"); diff --git a/tests/tools/autotest.sh b/tests/tools/autotest.sh index a0ed976fd..d0b0a89d7 100755 --- a/tests/tools/autotest.sh +++ b/tests/tools/autotest.sh @@ -10,6 +10,9 @@ makejmode=false frontend="verilog" backend_opts="-noattr -noexpr" autotb_opts="" +include_opts="" +xinclude_opts="" +minclude_opts="" scriptfiles="" scriptopt="" toolsdir="$(cd $(dirname $0); pwd)" @@ -19,7 +22,7 @@ if [ ! -f $toolsdir/cmp_tbdata -o $toolsdir/cmp_tbdata.c -nt $toolsdir/cmp_tbdat ( set -ex; ${CC:-gcc} -Wall -o $toolsdir/cmp_tbdata $toolsdir/cmp_tbdata.c; ) || exit 1 fi -while getopts xmGl:wkjvref:s:p:n:S: opt; do +while getopts xmGl:wkjvref:s:p:n:S:I: opt; do case "$opt" in x) use_xsim=true ;; @@ -52,8 +55,12 @@ while getopts xmGl:wkjvref:s:p:n:S: opt; do autotb_opts="$autotb_opts -n $OPTARG" ;; S) autotb_opts="$autotb_opts -seed $OPTARG" ;; + I) + include_opts="$include_opts -I $OPTARG" + xinclude_opts="$xinclude_opts -i $OPTARG" + minclude_opts="$minclude_opts +incdir+$OPTARG" ;; *) - echo "Usage: $0 [-x|-m] [-G] [-w] [-k] [-j] [-v] [-r] [-e] [-l libs] [-f frontend] [-s script] [-p cmdstring] [-n iters] [-S seed] verilog-files\n" >&2 + echo "Usage: $0 [-x|-m] [-G] [-w] [-k] [-j] [-v] [-r] [-e] [-l libs] [-f frontend] [-s script] [-p cmdstring] [-n iters] [-S seed] [-I incdir] verilog-files\n" >&2 exit 1 esac done @@ -63,18 +70,14 @@ compile_and_run() { if $use_modelsim; then altver=$( ls -v /opt/altera/ | grep '^[0-9]' | tail -n1; ) /opt/altera/$altver/modelsim_ase/bin/vlib work - /opt/altera/$altver/modelsim_ase/bin/vlog +define+outfile=\"$output\" "$@" + /opt/altera/$altver/modelsim_ase/bin/vlog $minclude_opts +define+outfile=\"$output\" "$@" /opt/altera/$altver/modelsim_ase/bin/vsim -c -do 'run -all; exit;' testbench elif $use_xsim; then - ( - set +x - files=( "$@" ) - xilver=$( ls -v /opt/Xilinx/Vivado/ | grep '^[0-9]' | tail -n1; ) - /opt/Xilinx/Vivado/$xilver/bin/xvlog -d outfile=\"$output\" "${files[@]}" - /opt/Xilinx/Vivado/$xilver/bin/xelab -R work.testbench - ) + xilver=$( ls -v /opt/Xilinx/Vivado/ | grep '^[0-9]' | tail -n1; ) + /opt/Xilinx/Vivado/$xilver/bin/xvlog $xinclude_opts -d outfile=\"$output\" "$@" + /opt/Xilinx/Vivado/$xilver/bin/xelab -R work.testbench else - iverilog -Doutfile=\"$output\" -s testbench -o "$exe" "$@" + iverilog $include_opts -Doutfile=\"$output\" -s testbench -o "$exe" "$@" vvp -n "$exe" fi } @@ -109,7 +112,7 @@ do egrep -v '^\s*`timescale' ../$fn > ${bn}_ref.v if [ ! -f ../${bn}_tb.v ]; then - "$toolsdir"/../../yosys -b "test_autotb $autotb_opts" -o ${bn}_tb.v ${bn}_ref.v + "$toolsdir"/../../yosys -f "$frontend $include_opts" -b "test_autotb $autotb_opts" -o ${bn}_tb.v ${bn}_ref.v else cp ../${bn}_tb.v ${bn}_tb.v fi @@ -135,16 +138,16 @@ do fi if [ -n "$scriptfiles" ]; then - test_passes ${bn}_ref.v $scriptfiles + test_passes -f "$frontend $include_opts" ${bn}_ref.v $scriptfiles elif [ -n "$scriptopt" ]; then - test_passes -f "$frontend" -p "$scriptopt" ${bn}_ref.v + test_passes -f "$frontend $include_opts" -p "$scriptopt" ${bn}_ref.v elif [ "$frontend" = "verific" ]; then test_passes -p "verific -vlog2k ${bn}_ref.v; verific -import -all; opt; memory;;" elif [ "$frontend" = "verific_gates" ]; then test_passes -p "verific -vlog2k ${bn}_ref.v; verific -import -gates -all; opt; memory;;" else - test_passes -f "$frontend" -p "hierarchy; proc; opt; memory; opt; fsm; opt -full -fine" ${bn}_ref.v - test_passes -f "$frontend" -p "hierarchy; synth -run coarse; techmap; opt; abc -dff" ${bn}_ref.v + test_passes -f "$frontend $include_opts" -p "hierarchy; proc; opt; memory; opt; fsm; opt -full -fine" ${bn}_ref.v + test_passes -f "$frontend $include_opts" -p "hierarchy; synth -run coarse; techmap; opt; abc -dff" ${bn}_ref.v fi touch ../${bn}.log } |