mirrors/yosys
3
0
Fork 0
mirror of https://github.com/YosysHQ/yosys synced 2025-08-04 10:20:24 +00:00
Code Activity

Merge branch 'main' of https://github.com/YosysHQ/yosys

Browse source
This commit is contained in:
Matt Young 2025-07-31 16:30:54 +10:00
commit ddc99a3b97
690 changed files with 39993 additions and 13636 deletions
Download patch file Download diff file Expand all files Collapse all files

24
backends/smt2/smt2.cc
View file

@ -24,6 +24,7 @@
#include "kernel/log.h"
#include "kernel/mem.h"
#include "libs/json11/json11.hpp"
#include "kernel/utils.h"
#include <string>
USING_YOSYS_NAMESPACE
@ -329,13 +330,14 @@ struct Smt2Worker
{
sigmap.apply(bit);
if (bit_driver.count(bit)) {
export_cell(bit_driver.at(bit));
sigmap.apply(bit);
}
if (bit.wire == nullptr)
return bit == RTLIL::State::S1 ? "true" : "false";
if (bit_driver.count(bit))
export_cell(bit_driver.at(bit));
sigmap.apply(bit);
if (fcache.count(bit) == 0) {
if (verbose) log("%*s-> external bool: %s\n", 2+2*GetSize(recursive_cells), "",
log_signal(bit));
@ -1077,14 +1079,14 @@ struct Smt2Worker
RTLIL::SigSpec sig = sigmap(wire);
Const val = wire->attributes.at(ID::init);
val.bits.resize(GetSize(sig), State::Sx);
val.bits().resize(GetSize(sig), State::Sx);
if (bvmode && GetSize(sig) > 1) {
Const mask(State::S1, GetSize(sig));
bool use_mask = false;
for (int i = 0; i < GetSize(sig); i++)
if (val[i] != State::S0 && val[i] != State::S1) {
val[i] = State::S0;
mask[i] = State::S0;
val.bits()[i] = State::S0;
mask.bits()[i] = State::S0;
use_mask = true;
}
if (use_mask)
@ -1359,10 +1361,10 @@ struct Smt2Worker
for (int k = 0; k < GetSize(initword); k++) {
if (initword[k] == State::S0 || initword[k] == State::S1) {
gen_init_constr = true;
initmask[k] = State::S1;
initmask.bits()[k] = State::S1;
} else {
initmask[k] = State::S0;
initword[k] = State::S0;
initmask.bits()[k] = State::S0;
initword.bits()[k] = State::S0;
}
}
@ -1829,7 +1831,7 @@ struct Smt2Backend : public Backend {
}
}
*f << stringf("; SMT-LIBv2 description generated by %s\n", yosys_version_str);
*f << stringf("; SMT-LIBv2 description generated by %s\n", yosys_maybe_version());
if (!bvmode)
*f << stringf("; yosys-smt2-nobv\n");

27
backends/smt2/smtbmc.py
View file

@ -1454,6 +1454,10 @@ def write_trace(steps_start, steps_stop, index, allregs=False):
if outywfile is not None:
write_yw_trace(steps, index, allregs)
def escape_path_segment(segment):
if "." in segment:
return f"\\{segment} "
return segment
def print_failed_asserts_worker(mod, state, path, extrainfo, infomap, infokey=()):
assert mod in smt.modinfo
@ -1464,7 +1468,8 @@ def print_failed_asserts_worker(mod, state, path, extrainfo, infomap, infokey=()
for cellname, celltype in smt.modinfo[mod].cells.items():
cell_infokey = (mod, cellname, infokey)
if print_failed_asserts_worker(celltype, "(|%s_h %s| %s)" % (mod, cellname, state), path + "." + cellname, extrainfo, infomap, cell_infokey):
cell_path = path + "." + escape_path_segment(cellname)
if print_failed_asserts_worker(celltype, "(|%s_h %s| %s)" % (mod, cellname, state), cell_path, extrainfo, infomap, cell_infokey):
found_failed_assert = True
for assertfun, assertinfo in smt.modinfo[mod].asserts.items():
@ -1497,7 +1502,7 @@ def print_anyconsts_worker(mod, state, path):
assert mod in smt.modinfo
for cellname, celltype in smt.modinfo[mod].cells.items():
print_anyconsts_worker(celltype, "(|%s_h %s| %s)" % (mod, cellname, state), path + "." + cellname)
print_anyconsts_worker(celltype, "(|%s_h %s| %s)" % (mod, cellname, state), path + "." + escape_path_segment(cellname))
for fun, info in smt.modinfo[mod].anyconsts.items():
if info[1] is None:
@ -1517,18 +1522,21 @@ def print_anyconsts(state):
print_anyconsts_worker(topmod, "s%d" % state, topmod)
def get_cover_list(mod, base):
def get_cover_list(mod, base, path=None):
path = path or mod
assert mod in smt.modinfo
cover_expr = list()
# A tuple of path and cell name
cover_desc = list()
for expr, desc in smt.modinfo[mod].covers.items():
cover_expr.append("(ite (|%s| %s) #b1 #b0)" % (expr, base))
cover_desc.append(desc)
cover_desc.append((path, desc))
for cell, submod in smt.modinfo[mod].cells.items():
e, d = get_cover_list(submod, "(|%s_h %s| %s)" % (mod, cell, base))
cell_path = path + "." + escape_path_segment(cell)
e, d = get_cover_list(submod, "(|%s_h %s| %s)" % (mod, cell, base), cell_path)
cover_expr += e
cover_desc += d
@ -1544,7 +1552,8 @@ def get_assert_map(mod, base, path, key_base=()):
assert_map[(expr, key_base)] = ("(|%s| %s)" % (expr, base), path, desc)
for cell, submod in smt.modinfo[mod].cells.items():
assert_map.update(get_assert_map(submod, "(|%s_h %s| %s)" % (mod, cell, base), path + "." + cell, (mod, cell, key_base)))
cell_path = path + "." + escape_path_segment(cell)
assert_map.update(get_assert_map(submod, "(|%s_h %s| %s)" % (mod, cell, base), cell_path, (mod, cell, key_base)))
return assert_map
@ -1903,7 +1912,9 @@ elif covermode:
new_cover_mask.append(cover_mask[i])
continue
print_msg("Reached cover statement at %s in step %d." % (cover_desc[i], step))
path = cover_desc[i][0]
name = cover_desc[i][1]
print_msg("Reached cover statement in step %d at %s: %s" % (step, path, name))
new_cover_mask.append("0")
cover_mask = "".join(new_cover_mask)
@ -1933,7 +1944,7 @@ elif covermode:
if "1" in cover_mask:
for i in range(len(cover_mask)):
if cover_mask[i] == "1":
print_msg("Unreached cover statement at %s." % cover_desc[i])
print_msg("Unreached cover statement at %s: %s" % (cover_desc[i][0], cover_desc[i][1]))
else: # not tempind, covermode
active_assert_keys = get_assert_keys()

2
backends/smt2/smtio.py
View file

@ -1217,7 +1217,7 @@ class SmtOpts:
def helpmsg(self):
return """
-s <solver>
set SMT solver: z3, yices, boolector, bitwuzla, cvc4, mathsat, dummy
set SMT solver: z3, yices, boolector, bitwuzla, cvc4, cvc5, mathsat, dummy
default: yices
-S <opt>

2
backends/smt2/test_cells.sh
View file

@ -21,7 +21,7 @@ EOT
for x in $(set +x; ls test_*.il | sort -R); do
x=${x%.il}
cat > $x.ys <<- EOT
read_ilang $x.il
read_rtlil $x.il
copy gold gate
cd gate