From c8553539866128279897336795f00248eb527ffa Mon Sep 17 00:00:00 2001 From: Clifford Wolf Date: Sat, 4 Mar 2017 23:41:54 +0100 Subject: [PATCH] Improve smt2 encodings of assert/assume/cover, better wire_smt2 help msg --- backends/smt2/smt2.cc | 116 ++++++++++++++++++++++++++++++----------- backends/smt2/smtio.py | 4 +- 2 files changed, 87 insertions(+), 33 deletions(-) diff --git a/backends/smt2/smt2.cc b/backends/smt2/smt2.cc index b550a40bd..9d07a1216 100644 --- a/backends/smt2/smt2.cc +++ b/backends/smt2/smt2.cc @@ -735,26 +735,41 @@ struct Smt2Worker if (verbose) log("=> export logic driving asserts\n"); + int assert_id = 0, assume_id = 0, cover_id = 0; vector assert_list, assume_list, cover_list; + for (auto cell : module->cells()) - if (cell->type.in("$assert", "$assume", "$cover")) { + { + if (cell->type.in("$assert", "$assume", "$cover")) + { + int &id = cell->type == "$assert" ? assert_id : + cell->type == "$assume" ? assume_id : + cell->type == "$cover" ? cover_id : *(int*)nullptr; + + char postfix = cell->type == "$assert" ? 'a' : + cell->type == "$assume" ? 'u' : + cell->type == "$cover" ? 'c' : 0; + 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, + decls.push_back(stringf("; yosys-smt2-%s %d %s\n", cell->type.c_str() + 1, id, cell->attributes.count("\\src") ? cell->attributes.at("\\src").decode_string().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))); + decls.push_back(stringf("(define-fun |%s_%c %d| ((state |%s_s|)) Bool (and %s %s)) ; %s\n", + get_id(module), postfix, id, 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))); + decls.push_back(stringf("(define-fun |%s_%c %d| ((state |%s_s|)) Bool (or %s (not %s))) ; %s\n", + get_id(module), postfix, id, 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++)); + assert_list.push_back(stringf("(|%s_a %d| state)", get_id(module), id)); 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++)); + assume_list.push_back(stringf("(|%s_u %d| state)", get_id(module), id)); + + id++; } + } for (int iter = 1; !registers.empty(); iter++) { @@ -1036,33 +1051,72 @@ struct Smt2Backend : public Backend { log(" write_smt2 [options] [filename]\n"); log("\n"); log("Write a SMT-LIBv2 [1] description of the current design. For a module with name\n"); - log("'' this will declare the sort '_s' (state of the module) and the\n"); - log("functions operating on that state.\n"); + log("'' this will declare the sort '_s' (state of the module) and will\n"); + log("define and declare functions operating on that state.\n"); + log("\n"); + log("The following SMT2 functions are generated for a module with name ''.\n"); + log("Some declarations/definitions are printed with a special comment. A prover\n"); + log("using the SMT2 files can use those comments to collect all relevant metadata\n"); + log("about the design.\n"); + log("\n"); + log(" ; yosys-smt2-module \n"); + log(" (declare-sort |_s| 0)\n"); + log(" The sort representing a state of module .\n"); + log("\n"); + log(" (define-fun |_h| ((state |_s|)) Bool (...))\n"); + log(" This function must be asserted for each state to establish the\n"); + log(" design hierarchy.\n"); + log("\n"); + log(" ; yosys-smt2-input \n"); + log(" ; yosys-smt2-output \n"); + log(" ; yosys-smt2-register \n"); + log(" ; yosys-smt2-wire \n"); + log(" (define-fun |_n | (|_s|) (_ BitVec ))\n"); + log(" (define-fun |_n | (|_s|) Bool)\n"); + log(" For each port, register, and wire with the 'keep' attribute set an\n"); + log(" accessor function is generated. Single-bit wires are returned as Bool,\n"); + log(" multi-bit wires as BitVec.\n"); + log("\n"); + log(" ; yosys-smt2-cell \n"); + log(" (declare-fun |_h | (|_s|) |_s|)\n"); + log(" There is a function like that for each hierarchical instance. It\n"); + log(" returns the sort that represents the state of the sub-module that\n"); + log(" implements the instance.\n"); + log("\n"); + log(" (declare-fun |_is| (|_s|) Bool)\n"); + log(" This function must be asserted 'true' for initial states, and 'false'\n"); + log(" otherwise.\n"); + log("\n"); + log(" (define-fun |_i| ((state |_s|)) Bool (...))\n"); + log(" This function must be asserted 'true' for initial states. For\n"); + log(" non-initial states it must be left unconstrained.\n"); + log("\n"); + log(" (define-fun |_t| ((state |_s|) (next_state |_s|)) Bool (...))\n"); + log(" This function evaluates to 'true' if the states 'state' and\n"); + log(" 'next_state' form a valid state transition.\n"); log("\n"); - log("The '_s' sort represents a module state. Additional '_n' functions\n"); - log("are provided that can be used to access the values of the signals in the module.\n"); - log("By default only ports, registers, and wires with the 'keep' attribute set are\n"); - log("made available via such functions. With the -nobv option, multi-bit wires are\n"); - log("exported as separate functions of type Bool for the individual bits. Without\n"); - log("-nobv multi-bit wires are exported as single functions of type BitVec.\n"); + log(" (define-fun |_a| ((state |_s|)) Bool (...))\n"); + log(" This function evaluates to 'true' if all assertions hold in the state.\n"); log("\n"); - log("The '_t' function evaluates to 'true' when the given pair of states\n"); - log("describes a valid state transition.\n"); + log(" (define-fun |_u| ((state |_s|)) Bool (...))\n"); + log(" This function evaluates to 'true' if all assumptions hold in the state.\n"); log("\n"); - log("The '_a' function evaluates to 'true' when the given state satisfies\n"); - log("the asserts in the module.\n"); + log(" ; yosys-smt2-assert \n"); + log(" (define-fun |_a | ((state |_s|)) Bool (...))\n"); + log(" Each $assert cell is converted into one of this functions. The function\n"); + log(" evaluates to 'true' if the assert statement holds in the state.\n"); log("\n"); - log("The '_u' function evaluates to 'true' when the given state satisfies\n"); - log("the assumptions in the module.\n"); + log(" ; yosys-smt2-assume \n"); + log(" (define-fun |_u | ((state |_s|)) Bool (...))\n"); + log(" Each $assume cell is converted into one of this functions. The function\n"); + log(" evaluates to 'true' if the assume statement holds in the state.\n"); log("\n"); - log("The '_i' function evaluates to 'true' when the given state conforms\n"); - log("to the initial state. Furthermore the '_is' function should be asserted\n"); - log("to be true for initial states in addition to '_i', and should be\n"); - log("asserted to be false for non-initial states.\n"); + log(" ; yosys-smt2-cover \n"); + log(" (define-fun |_c | ((state |_s|)) Bool (...))\n"); + log(" Each $cover cell is converted into one of this functions. The function\n"); + log(" evaluates to 'true' if the cover statement is activated in the state.\n"); log("\n"); - log("For hierarchical designs, the '_h' function must be asserted for each\n"); - log("state to establish the design hierarchy. The '_h ' function\n"); - log("evaluates to the state corresponding to the given cell within .\n"); + log("Options:\n"); log("\n"); log(" -verbose\n"); log(" this will print the recursive walk used to export the modules.\n"); diff --git a/backends/smt2/smtio.py b/backends/smt2/smtio.py index 1278d00aa..38e3f3119 100644 --- a/backends/smt2/smtio.py +++ b/backends/smt2/smtio.py @@ -334,10 +334,10 @@ class SmtIo: self.modinfo[self.curmod].wsize[fields[2]] = int(fields[3]) if fields[1] == "yosys-smt2-assert": - self.modinfo[self.curmod].asserts[fields[2]] = fields[3] + self.modinfo[self.curmod].asserts["%s_a %s" % (self.curmod, fields[2])] = fields[3] if fields[1] == "yosys-smt2-cover": - self.modinfo[self.curmod].covers[fields[2]] = fields[3] + self.modinfo[self.curmod].covers["%s_c %s" % (self.curmod, fields[2])] = fields[3] if fields[1] == "yosys-smt2-anyconst": self.modinfo[self.curmod].anyconsts[fields[2]] = fields[3] -- 2.30.2