aboutsummaryrefslogtreecommitdiffstats
diff options
context:
space:
mode:
Diffstat
-rw-r--r--.github/ISSUE_TEMPLATE/bug_report.yml14
-rw-r--r--.github/workflows/codeql.yml2
-rw-r--r--.github/workflows/emcc.yml6
-rw-r--r--.github/workflows/test-linux.yml4
-rw-r--r--.github/workflows/test-macos.yml4
-rw-r--r--.github/workflows/version.yml6
-rw-r--r--.github/workflows/vs.yml8
-rw-r--r--Makefile2
-rw-r--r--backends/smt2/smt2.cc13
-rw-r--r--backends/smt2/smtbmc.py42
-rw-r--r--backends/smt2/smtio.py11
-rw-r--r--frontends/verific/verific.cc32
-rw-r--r--kernel/log.h12
-rw-r--r--tests/various/smtlib2_module-expected.smt214
14 files changed, 138 insertions, 32 deletions
diff --git a/.github/ISSUE_TEMPLATE/bug_report.yml b/.github/ISSUE_TEMPLATE/bug_report.yml
index ca9cb4811..27cfd09b7 100644
--- a/.github/ISSUE_TEMPLATE/bug_report.yml
+++ b/.github/ISSUE_TEMPLATE/bug_report.yml
@@ -25,6 +25,19 @@ body:
validations:
required: true
+ - type: dropdown
+ id: os
+ attributes:
+ label: On which OS did this happen?
+ options:
+ - Linux
+ - macOS
+ - Windows
+ - BSD
+ multiple: true
+ validations:
+ required: true
+
- type: markdown
attributes:
value: >
@@ -60,4 +73,3 @@ body:
description: "Please describe how the behavior you see differs from the expected behavior."
validations:
required: true
-
diff --git a/.github/workflows/codeql.yml b/.github/workflows/codeql.yml
index 57cbe5010..2a046703b 100644
--- a/.github/workflows/codeql.yml
+++ b/.github/workflows/codeql.yml
@@ -14,7 +14,7 @@ jobs:
run: sudo apt-get install bison flex libreadline-dev tcl-dev libffi-dev
- name: Checkout repository
- uses: actions/checkout@v3.0.0
+ uses: actions/checkout@v3
- name: Initialize CodeQL
uses: github/codeql-action/init@v2
diff --git a/.github/workflows/emcc.yml b/.github/workflows/emcc.yml
index f1cc4b3e7..7a9a6064f 100644
--- a/.github/workflows/emcc.yml
+++ b/.github/workflows/emcc.yml
@@ -7,10 +7,10 @@ jobs:
runs-on: ubuntu-latest
steps:
- uses: mymindstorm/setup-emsdk@v11
- - uses: actions/checkout@v2
+ - uses: actions/checkout@v3
- name: Cache sources
id: cache-sources
- uses: actions/cache@v2
+ uses: actions/cache@v3
with:
path: .
key: cache-yosys
@@ -18,7 +18,7 @@ jobs:
run: |
make config-emcc
make YOSYS_VER=latest
- - uses: actions/upload-artifact@v2
+ - uses: actions/upload-artifact@v3
with:
name: yosysjs
path: yosysjs-latest.zip
diff --git a/.github/workflows/test-linux.yml b/.github/workflows/test-linux.yml
index e27ea37d2..b974757c4 100644
--- a/.github/workflows/test-linux.yml
+++ b/.github/workflows/test-linux.yml
@@ -84,7 +84,7 @@ jobs:
$CXX --version
- name: Checkout Yosys
- uses: actions/checkout@v2
+ uses: actions/checkout@v3
- name: Get iverilog
shell: bash
@@ -93,7 +93,7 @@ jobs:
- name: Cache iverilog
id: cache-iverilog
- uses: actions/cache@v2
+ uses: actions/cache@v3
with:
path: .local/
key: ${{ matrix.os.id }}-${{ hashFiles('iverilog/.git/refs/heads/master') }}
diff --git a/.github/workflows/test-macos.yml b/.github/workflows/test-macos.yml
index 22cf5e658..048457234 100644
--- a/.github/workflows/test-macos.yml
+++ b/.github/workflows/test-macos.yml
@@ -35,7 +35,7 @@ jobs:
cc --version
- name: Checkout Yosys
- uses: actions/checkout@v2
+ uses: actions/checkout@v3
- name: Get iverilog
shell: bash
@@ -44,7 +44,7 @@ jobs:
- name: Cache iverilog
id: cache-iverilog
- uses: actions/cache@v2
+ uses: actions/cache@v3
with:
path: .local/
key: ${{ matrix.os.id }}-${{ hashFiles('iverilog/.git/refs/heads/master') }}
diff --git a/.github/workflows/version.yml b/.github/workflows/version.yml
index c6f4da30d..c2a1756e9 100644
--- a/.github/workflows/version.yml
+++ b/.github/workflows/version.yml
@@ -10,15 +10,15 @@ jobs:
runs-on: ubuntu-latest
steps:
- name: Checkout
- uses: actions/checkout@v2
+ uses: actions/checkout@v3
with:
fetch-depth: 0
- name: Take last commit
id: log
- run: echo "::set-output name=message::$(git log --no-merges -1 --oneline)"
+ run: echo "message=$(git log --no-merges -1 --oneline)" >> $GITHUB_OUTPUT
- name: Take repository
id: repo
- run: echo "::set-output name=message::$GITHUB_REPOSITORY"
+ run: echo "message=$GITHUB_REPOSITORY" >> $GITHUB_OUTPUT
- name: Bump version
if: "!contains(steps.log.outputs.message, 'Bump version') && contains(steps.repo.outputs.message, 'YosysHQ/yosys')"
run: |
diff --git a/.github/workflows/vs.yml b/.github/workflows/vs.yml
index 79a8401d6..744ad5677 100644
--- a/.github/workflows/vs.yml
+++ b/.github/workflows/vs.yml
@@ -6,16 +6,16 @@ jobs:
yosys-vcxsrc:
runs-on: ubuntu-latest
steps:
- - uses: actions/checkout@v2
+ - uses: actions/checkout@v3
- name: Cache sources
id: cache-sources
- uses: actions/cache@v2
+ uses: actions/cache@v3
with:
path: .
key: cache-yosys
- name: Build
run: make vcxsrc YOSYS_VER=latest
- - uses: actions/upload-artifact@v2
+ - uses: actions/upload-artifact@v3
with:
name: vcxsrc
path: yosys-win32-vcxsrc-latest.zip
@@ -24,7 +24,7 @@ jobs:
runs-on: windows-2019
needs: yosys-vcxsrc
steps:
- - uses: actions/download-artifact@v2
+ - uses: actions/download-artifact@v3
with:
name: vcxsrc
path: .
diff --git a/Makefile b/Makefile
index 3b682b752..7802a3cc3 100644
--- a/Makefile
+++ b/Makefile
@@ -131,7 +131,7 @@ LDLIBS += -lrt
endif
endif
-YOSYS_VER := 0.22+17
+YOSYS_VER := 0.22+42
# Note: We arrange for .gitcommit to contain the (short) commit hash in
# tarballs generated with git-archive(1) using .gitattributes. The git repo
diff --git a/backends/smt2/smt2.cc b/backends/smt2/smt2.cc
index 54783cf1b..7434b13da 100644
--- a/backends/smt2/smt2.cc
+++ b/backends/smt2/smt2.cc
@@ -559,6 +559,9 @@ struct Smt2Worker
if (cell->type.in(ID($_FF_), ID($_DFF_P_), ID($_DFF_N_)))
{
registers.insert(cell);
+ SigBit q_bit = cell->getPort(ID::Q);
+ if (q_bit.is_wire())
+ decls.push_back(witness_signal("reg", 1, 0, "", idcounter, q_bit.wire));
makebits(stringf("%s#%d", get_id(module), idcounter), 0, log_signal(cell->getPort(ID::Q)));
register_bool(cell->getPort(ID::Q), idcounter++);
recursive_cells.erase(cell);
@@ -589,9 +592,12 @@ struct Smt2Worker
if (cell->type.in(ID($ff), ID($dff)))
{
registers.insert(cell);
- for (auto chunk : cell->getPort(ID::Q).chunks())
+ int smtoffset = 0;
+ for (auto chunk : cell->getPort(ID::Q).chunks()) {
if (chunk.is_wire())
- decls.push_back(witness_signal("reg", chunk.width, chunk.offset, "", idcounter, chunk.wire));
+ decls.push_back(witness_signal("reg", chunk.width, chunk.offset, "", idcounter, chunk.wire, smtoffset));
+ smtoffset += chunk.width;
+ }
makebits(stringf("%s#%d", get_id(module), idcounter), GetSize(cell->getPort(ID::Q)), log_signal(cell->getPort(ID::Q)));
register_bv(cell->getPort(ID::Q), idcounter++);
recursive_cells.erase(cell);
@@ -1490,7 +1496,7 @@ struct Smt2Worker
return path;
}
- std::string witness_signal(const char *type, int width, int offset, const std::string &smtname, int smtid, RTLIL::Wire *wire)
+ std::string witness_signal(const char *type, int width, int offset, const std::string &smtname, int smtid, RTLIL::Wire *wire, int smtoffset = 0)
{
std::vector<std::string> hiername;
const char *wire_name = wire->name.c_str();
@@ -1508,6 +1514,7 @@ struct Smt2Worker
{ "offset", offset },
{ "width", width },
{ "smtname", smtname.empty() ? json11::Json(smtid) : json11::Json(smtname) },
+ { "smtoffset", smtoffset },
{ "path", witness_path(wire) },
}}).dump(line);
line += "\n";
diff --git a/backends/smt2/smtbmc.py b/backends/smt2/smtbmc.py
index 5f05287de..4c1f07229 100644
--- a/backends/smt2/smtbmc.py
+++ b/backends/smt2/smtbmc.py
@@ -55,6 +55,7 @@ noinit = False
binarymode = False
keep_going = False
check_witness = False
+detect_loops = False
so = SmtOpts()
@@ -175,6 +176,10 @@ def usage():
check that the used witness file contains sufficient
constraints to force an assertion failure.
+ --detect-loops
+ check if states are unique in temporal induction counter examples
+ (this feature is experimental and incomplete)
+
""" + so.helpmsg())
sys.exit(1)
@@ -183,7 +188,7 @@ try:
opts, args = getopt.getopt(sys.argv[1:], so.shortopts + "t:igcm:", so.longopts +
["final-only", "assume-skipped=", "smtc=", "cex=", "aig=", "aig-noheader", "yw=", "btorwit=", "presat",
"dump-vcd=", "dump-yw=", "dump-vlogtb=", "vlogtb-top=", "dump-smtc=", "dump-all", "noinfo", "append=",
- "smtc-init", "smtc-top=", "noinit", "binary", "keep-going", "check-witness"])
+ "smtc-init", "smtc-top=", "noinit", "binary", "keep-going", "check-witness", "detect-loops"])
except:
usage()
@@ -264,6 +269,8 @@ for o, a in opts:
keep_going = True
elif o == "--check-witness":
check_witness = True
+ elif o == "--detect-loops":
+ detect_loops = True
elif so.handle(o, a):
pass
else:
@@ -669,7 +676,7 @@ if inywfile is not None:
if common_end <= common_offset:
continue
- smt_expr = smt.net_expr(topmod, f"s{t}", wire["smtpath"])
+ smt_expr = smt.witness_net_expr(topmod, f"s{t}", wire)
if not smt_bool:
slice_high = common_end - offset - 1
@@ -969,6 +976,30 @@ def write_vcd_trace(steps_start, steps_stop, index):
vcd.set_time(steps_stop)
+def detect_state_loop(steps_start, steps_stop):
+ print_msg(f"Checking for loops in found induction counter example")
+ print_msg(f"This feature is experimental and incomplete")
+
+ path_list = sorted(smt.hiernets(topmod, regs_only=True))
+
+ mem_trace_data = collect_mem_trace_data(steps_start, steps_stop)
+
+ # Map state to index of step when it occurred
+ states = dict()
+
+ for i in range(steps_start, steps_stop):
+ value_list = smt.get_net_bin_list(topmod, path_list, "s%d" % i)
+ mem_state = sorted(
+ [(tuple(path), addr, data)
+ for path, addr, data in mem_trace_data.get(i, [])])
+ state = tuple(value_list), tuple(mem_state)
+ if state in states:
+ return (i, states[state])
+ else:
+ states[state] = i
+
+ return None
+
def char_ok_in_verilog(c,i):
if ('A' <= c <= 'Z'): return True
if ('a' <= c <= 'z'): return True
@@ -1267,7 +1298,8 @@ def write_yw_trace(steps_start, steps_stop, index, allregs=False):
sigs = seqs
for sig in sigs:
- step_values[sig["sig"]] = smt.bv2bin(smt.get(smt.net_expr(topmod, f"s{k}", sig["smtpath"])))
+ value = smt.bv2bin(smt.get(smt.witness_net_expr(topmod, f"s{k}", sig)))
+ step_values[sig["sig"]] = value
yw.step(step_values)
yw.end_trace()
@@ -1596,6 +1628,10 @@ if tempind:
print_anyconsts(num_steps)
print_failed_asserts(num_steps)
write_trace(step, num_steps+1, '%', allregs=True)
+ if detect_loops:
+ loop = detect_state_loop(step, num_steps+1)
+ if loop:
+ print_msg(f"Loop detected, increasing induction depth will not help. Step {loop[0]} = step {loop[1]}")
elif dumpall:
print_anyconsts(num_steps)
diff --git a/backends/smt2/smtio.py b/backends/smt2/smtio.py
index 9af454cca..a73745896 100644
--- a/backends/smt2/smtio.py
+++ b/backends/smt2/smtio.py
@@ -701,7 +701,7 @@ class SmtIo:
if witness["type"] == "mem":
if allregs and not witness["rom"]:
width, size = witness["width"], witness["size"]
- witness = {**witness, "uninitialized": {"width": width * size, "offset": 0}}
+ witness = {**witness, "uninitialized": [{"width": width * size, "offset": 0}]}
if not witness["uninitialized"]:
continue
@@ -958,6 +958,15 @@ class SmtIo:
nextbase = "(|%s_h %s| %s)" % (mod, path[0], base)
return self.net_expr(nextmod, nextbase, path[1:])
+ def witness_net_expr(self, mod, base, witness):
+ net = self.net_expr(mod, base, witness["smtpath"])
+ is_bool = self.net_width(mod, witness["smtpath"]) == 1
+ if is_bool:
+ assert witness["width"] == 1
+ assert witness["smtoffset"] == 0
+ return net
+ return "((_ extract %d %d) %s)" % (witness["smtoffset"] + witness["width"] - 1, witness["smtoffset"], net)
+
def net_width(self, mod, net_path):
for i in range(len(net_path)-1):
assert mod in self.modinfo
diff --git a/frontends/verific/verific.cc b/frontends/verific/verific.cc
index 1b9db8772..71b87755d 100644
--- a/frontends/verific/verific.cc
+++ b/frontends/verific/verific.cc
@@ -2533,6 +2533,10 @@ struct VerificPass : public Pass {
log(" -fullinit\n");
log(" Keep all register initializations, even those for non-FF registers.\n");
log("\n");
+ log(" -cells\n");
+ log(" Import all cell definitions from Verific loaded libraries even if they are\n");
+ log(" unused in design. Useful with \"-edif\" option.\n");
+ log("\n");
log(" -chparam name value \n");
log(" Elaborate the specified top modules (all modules when -all given) using\n");
log(" this parameter value. Modules on which this parameter does not exist will\n");
@@ -3052,7 +3056,7 @@ struct VerificPass : public Pass {
bool mode_all = false, mode_gates = false, mode_keep = false;
bool mode_nosva = false, mode_names = false, mode_verific = false;
bool mode_autocover = false, mode_fullinit = false;
- bool flatten = false, extnets = false;
+ bool flatten = false, extnets = false, mode_cells = false;
string dumpfile;
string ppfile;
Map parameters(STRING_HASH);
@@ -3098,6 +3102,10 @@ struct VerificPass : public Pass {
mode_fullinit = true;
continue;
}
+ if (args[argidx] == "-cells") {
+ mode_cells = true;
+ continue;
+ }
if (args[argidx] == "-chparam" && argidx+2 < GetSize(args)) {
const std::string &key = args[++argidx];
const std::string &value = args[++argidx];
@@ -3218,6 +3226,28 @@ struct VerificPass : public Pass {
}
delete netlists;
}
+ if (mode_cells) {
+ log("Importing all cells.\n");
+ Libset *gls = Libset::Global() ;
+ MapIter it ;
+ Library *l ;
+ FOREACH_LIBRARY_OF_LIBSET(gls,it,l) {
+ MapIter mi ;
+ Verific::Cell *c ;
+ FOREACH_CELL_OF_LIBRARY(l,mi,c) {
+ if (!mode_verific && (l == Library::Primitives() || l == Library::Operators())) continue;
+ MapIter ni ;
+ if (c->NumOfNetlists() == 1) {
+ c->GetFirstNetlist()->SetName("");
+ }
+ Netlist *nl;
+ FOREACH_NETLIST_OF_CELL(c, ni, nl) {
+ if (nl)
+ nl_todo.emplace(nl->CellBaseName(), nl);
+ }
+ }
+ }
+ }
if (!verific_error_msg.empty())
goto check_error;
diff --git a/kernel/log.h b/kernel/log.h
index 3bc9fd978..8ef6e6d0e 100644
--- a/kernel/log.h
+++ b/kernel/log.h
@@ -419,6 +419,18 @@ static inline void log_dump_val_worker(pool<K, OPS> &v) {
log(" }");
}
+template<typename K>
+static inline void log_dump_val_worker(std::vector<K> &v) {
+ log("{");
+ bool first = true;
+ for (auto &it : v) {
+ log(first ? " " : ", ");
+ log_dump_val_worker(it);
+ first = false;
+ }
+ log(" }");
+}
+
template<typename T>
static inline void log_dump_val_worker(T *ptr) { log("%p", ptr); }
diff --git a/tests/various/smtlib2_module-expected.smt2 b/tests/various/smtlib2_module-expected.smt2
index 74e2f3fca..494e7cda0 100644
--- a/tests/various/smtlib2_module-expected.smt2
+++ b/tests/various/smtlib2_module-expected.smt2
@@ -4,14 +4,14 @@
(declare-fun |smtlib2_is| (|smtlib2_s|) Bool)
(declare-fun |smtlib2#0| (|smtlib2_s|) (_ BitVec 8)) ; \a
; yosys-smt2-input a 8
-; yosys-smt2-witness {"offset": 0, "path": ["\\a"], "smtname": "a", "type": "input", "width": 8}
+; yosys-smt2-witness {"offset": 0, "path": ["\\a"], "smtname": "a", "smtoffset": 0, "type": "input", "width": 8}
(define-fun |smtlib2_n a| ((state |smtlib2_s|)) (_ BitVec 8) (|smtlib2#0| state))
(declare-fun |smtlib2#1| (|smtlib2_s|) (_ BitVec 8)) ; \b
; yosys-smt2-input b 8
-; yosys-smt2-witness {"offset": 0, "path": ["\\b"], "smtname": "b", "type": "input", "width": 8}
+; yosys-smt2-witness {"offset": 0, "path": ["\\b"], "smtname": "b", "smtoffset": 0, "type": "input", "width": 8}
(define-fun |smtlib2_n b| ((state |smtlib2_s|)) (_ BitVec 8) (|smtlib2#1| state))
; yosys-smt2-output add 8
-; yosys-smt2-witness {"offset": 0, "path": ["\\add"], "smtname": "add", "type": "blackbox", "width": 8}
+; yosys-smt2-witness {"offset": 0, "path": ["\\add"], "smtname": "add", "smtoffset": 0, "type": "blackbox", "width": 8}
(define-fun |smtlib2_n add| ((state |smtlib2_s|)) (_ BitVec 8) (let (
(|a| (|smtlib2_n a| state))
(|b| (|smtlib2_n b| state))
@@ -19,7 +19,7 @@
(bvadd a b)
))
; yosys-smt2-output eq 1
-; yosys-smt2-witness {"offset": 0, "path": ["\\eq"], "smtname": "eq", "type": "blackbox", "width": 1}
+; yosys-smt2-witness {"offset": 0, "path": ["\\eq"], "smtname": "eq", "smtoffset": 0, "type": "blackbox", "width": 1}
(define-fun |smtlib2_n eq| ((state |smtlib2_s|)) Bool (let (
(|a| (|smtlib2_n a| state))
(|b| (|smtlib2_n b| state))
@@ -27,7 +27,7 @@
(= a b)
))
; yosys-smt2-output sub 8
-; yosys-smt2-witness {"offset": 0, "path": ["\\sub"], "smtname": "sub", "type": "blackbox", "width": 8}
+; yosys-smt2-witness {"offset": 0, "path": ["\\sub"], "smtname": "sub", "smtoffset": 0, "type": "blackbox", "width": 8}
(define-fun |smtlib2_n sub| ((state |smtlib2_s|)) (_ BitVec 8) (let (
(|a| (|smtlib2_n a| state))
(|b| (|smtlib2_n b| state))
@@ -49,10 +49,10 @@
(declare-fun |uut#2| (|uut_s|) (_ BitVec 8)) ; \sub
(declare-fun |uut_h s| (|uut_s|) |smtlib2_s|)
; yosys-smt2-anyconst uut#3 8 smtlib2_module.v:14.17-14.26
-; yosys-smt2-witness {"offset": 0, "path": ["\\a"], "smtname": 3, "type": "init", "width": 8}
+; yosys-smt2-witness {"offset": 0, "path": ["\\a"], "smtname": 3, "smtoffset": 0, "type": "init", "width": 8}
(declare-fun |uut#3| (|uut_s|) (_ BitVec 8)) ; \a
; yosys-smt2-anyconst uut#4 8 smtlib2_module.v:14.32-14.41
-; yosys-smt2-witness {"offset": 0, "path": ["\\b"], "smtname": 4, "type": "init", "width": 8}
+; yosys-smt2-witness {"offset": 0, "path": ["\\b"], "smtname": 4, "smtoffset": 0, "type": "init", "width": 8}
(declare-fun |uut#4| (|uut_s|) (_ BitVec 8)) ; \b
(define-fun |uut#5| ((state |uut_s|)) (_ BitVec 8) (bvadd (|uut#3| state) (|uut#4| state))) ; \add2
(define-fun |uut#6| ((state |uut_s|)) Bool (= (|uut#0| state) (|uut#5| state))) ; $0$formal$smtlib2_module.v:28$1_CHECK[0:0]$9
generated by cgit v1.2.3 (git 2.25.1) at 2025-04-25 05:06:21 +0000