diff options
author | Clifford Wolf <clifford@clifford.at> | 2015-02-26 19:02:55 +0100 |
---|---|---|
committer | Clifford Wolf <clifford@clifford.at> | 2015-02-26 19:02:55 +0100 |
commit | 5d4f513c3bfa3848765daeb3e1cd9c937650231e (patch) | |
tree | 5cc80637b39c8be9ebe274eb14d480f23406e918 /backends/smt2 | |
parent | 1f1deda888ea32ade2478fca9fcb510ada477606 (diff) | |
download | yosys-5d4f513c3bfa3848765daeb3e1cd9c937650231e.tar.gz yosys-5d4f513c3bfa3848765daeb3e1cd9c937650231e.tar.bz2 yosys-5d4f513c3bfa3848765daeb3e1cd9c937650231e.zip |
Added $assume support to write_smt2
Diffstat (limited to 'backends/smt2')
-rw-r--r-- | backends/smt2/smt2.cc | 23 |
1 files changed, 19 insertions, 4 deletions
diff --git a/backends/smt2/smt2.cc b/backends/smt2/smt2.cc index 1525d32ff..3d872c63a 100644 --- a/backends/smt2/smt2.cc +++ b/backends/smt2/smt2.cc @@ -470,14 +470,17 @@ struct Smt2Worker if (verbose) log("=> export logic driving asserts\n"); - vector<int> assert_list; + vector<int> assert_list, assume_list; for (auto cell : module->cells()) - if (cell->type == "$assert") { + if (cell->type.in("$assert", "$assume")) { string name_a = get_bool(cell->getPort("\\A")); string name_en = get_bool(cell->getPort("\\EN")); decls.push_back(stringf("(define-fun |%s#%d| ((state |%s_s|)) Bool (or %s (not %s))) ; %s\n", log_id(module), idcounter, log_id(module), name_a.c_str(), name_en.c_str(), log_id(cell))); - assert_list.push_back(idcounter++); + if (cell->type == "$assert") + assert_list.push_back(idcounter++); + else + assume_list.push_back(idcounter++); } for (int iter = 1; !registers.empty(); iter++) @@ -510,6 +513,15 @@ struct Smt2Worker decls.push_back(stringf("(define-fun |%s_a| ((state |%s_s|)) Bool %s)\n", log_id(module), log_id(module), assert_expr.c_str())); + string assume_expr = assume_list.empty() ? "true" : "(and"; + if (!assume_list.empty()) { + for (int i : assume_list) + assume_expr += stringf(" (|%s#%d| state)", log_id(module), i); + assume_expr += ")"; + } + decls.push_back(stringf("(define-fun |%s_u| ((state |%s_s|)) Bool %s)\n", + log_id(module), log_id(module), assume_expr.c_str())); + string init_expr = init_list.empty() ? "true" : "(and"; if (!init_list.empty()) { for (auto &str : init_list) @@ -550,7 +562,7 @@ struct Smt2Backend : public Backend { log("\n"); log("Write a SMT-LIBv2 [1] description of the current design. For a module with name\n"); log("'<mod>' this will declare the sort '<mod>_s' (state of the module) and the\n"); - log("functions '<mod>_t' (transition), '<mod>_a' (asserts), and '<mod>_i' (init).\n"); + log("functions operating on that state.\n"); log("\n"); log("The '<mod>_s' sort represents a module state. Additional '<mod>_n' functions\n"); log("are provided that can be used to access the values of the signals in the module.\n"); @@ -565,6 +577,9 @@ struct Smt2Backend : public Backend { log("The '<mod>_a' function evaluates to 'true' when the given state satisfies\n"); log("the asserts in the module.\n"); log("\n"); + log("The '<mod>_u' function evaluates to 'true' when the given state satisfies\n"); + log("the assumptions in the module.\n"); + log("\n"); log("The '<mod>_i' function evaluates to 'true' when the given state conforms\n"); log("to the initial state.\n"); log("\n"); |