aboutsummaryrefslogtreecommitdiffstats
diff options
context:
space:
mode:
Diffstat
-rw-r--r--Makefile2
-rw-r--r--backends/btor/btor.cc22
-rw-r--r--backends/smt2/smtbmc.py105
-rw-r--r--frontends/verific/verific.cc53
-rw-r--r--passes/opt/opt_expr.cc2
-rw-r--r--passes/opt/opt_lut.cc35
-rw-r--r--tests/opt/opt_lut_port.il18
-rw-r--r--tests/opt/opt_lut_port.ys2
-rw-r--r--tests/svinterfaces/.gitignore8
9 files changed, 177 insertions, 70 deletions
diff --git a/Makefile b/Makefile
index 053796e9d..8da6315fb 100644
--- a/Makefile
+++ b/Makefile
@@ -357,7 +357,7 @@ endif
ifeq ($(ENABLE_VERIFIC),1)
VERIFIC_DIR ?= /usr/local/src/verific_lib_eval
-VERIFIC_COMPONENTS ?= verilog vhdl database util containers sdf hier_tree
+VERIFIC_COMPONENTS ?= verilog vhdl database util containers hier_tree
CXXFLAGS += $(patsubst %,-I$(VERIFIC_DIR)/%,$(VERIFIC_COMPONENTS)) -DYOSYS_ENABLE_VERIFIC
ifeq ($(OS), Darwin)
LDLIBS += $(patsubst %,$(VERIFIC_DIR)/%/*-mac.a,$(VERIFIC_COMPONENTS)) -lz
diff --git a/backends/btor/btor.cc b/backends/btor/btor.cc
index 58d2a8625..ab2702807 100644
--- a/backends/btor/btor.cc
+++ b/backends/btor/btor.cc
@@ -506,6 +506,18 @@ struct BtorWorker
}
}
+ Const initval;
+ for (int i = 0; i < GetSize(sig_q); i++)
+ if (initbits.count(sig_q[i]))
+ initval.bits.push_back(initbits.at(sig_q[i]) ? State::S1 : State::S0);
+ else
+ initval.bits.push_back(State::Sx);
+
+ int nid_init_val = -1;
+
+ if (!initval.is_fully_undef())
+ nid_init_val = get_sig_nid(initval);
+
int sid = get_bv_sid(GetSize(sig_q));
int nid = next_nid++;
@@ -514,15 +526,7 @@ struct BtorWorker
else
btorf("%d state %d %s\n", nid, sid, log_id(symbol));
- Const initval;
- for (int i = 0; i < GetSize(sig_q); i++)
- if (initbits.count(sig_q[i]))
- initval.bits.push_back(initbits.at(sig_q[i]) ? State::S1 : State::S0);
- else
- initval.bits.push_back(State::Sx);
-
- if (!initval.is_fully_undef()) {
- int nid_init_val = get_sig_nid(initval);
+ if (nid_init_val >= 0) {
int nid_init = next_nid++;
if (verbose)
btorf("; initval = %s\n", log_signal(initval));
diff --git a/backends/smt2/smtbmc.py b/backends/smt2/smtbmc.py
index b944ee004..721a395e3 100644
--- a/backends/smt2/smtbmc.py
+++ b/backends/smt2/smtbmc.py
@@ -32,6 +32,7 @@ cexfile = None
aimfile = None
aiwfile = None
aigheader = True
+btorwitfile = None
vlogtbfile = None
vlogtbtop = None
inconstr = list()
@@ -92,6 +93,9 @@ yosys-smtbmc [options] <yosys_smt2_output>
the AIGER witness file does not include the status and
properties lines.
+ --btorwit <btor_witness_filename>
+ read a BTOR witness.
+
--noinfo
only run the core proof, do not collect and print any
additional information (e.g. which assert failed)
@@ -152,7 +156,7 @@ yosys-smtbmc [options] <yosys_smt2_output>
try:
opts, args = getopt.getopt(sys.argv[1:], so.shortopts + "t:igcm:", so.longopts +
- ["final-only", "assume-skipped=", "smtc=", "cex=", "aig=", "aig-noheader", "presat",
+ ["final-only", "assume-skipped=", "smtc=", "cex=", "aig=", "aig-noheader", "btorwit=", "presat",
"dump-vcd=", "dump-vlogtb=", "vlogtb-top=", "dump-smtc=", "dump-all", "noinfo", "append=",
"smtc-init", "smtc-top=", "noinit"])
except:
@@ -189,6 +193,8 @@ for o, a in opts:
aiwfile = a + ".aiw"
elif o == "--aig-noheader":
aigheader = False
+ elif o == "--btorwit":
+ btorwitfile = a
elif o == "--dump-vcd":
vcdfile = a
elif o == "--dump-vlogtb":
@@ -575,6 +581,103 @@ if aimfile is not None:
num_steps = max(num_steps, step+1)
step += 1
+if btorwitfile is not None:
+ with open(btorwitfile, "r") as f:
+ step = None
+ suffix = None
+ altsuffix = None
+ header_okay = False
+
+ for line in f:
+ line = line.strip()
+
+ if line == "sat":
+ header_okay = True
+ continue
+
+ if not header_okay:
+ continue
+
+ if line == "" or line[0] == "b" or line[0] == "j":
+ continue
+
+ if line == ".":
+ break
+
+ if line[0] == '#' or line[0] == '@':
+ step = int(line[1:])
+ suffix = line
+ altsuffix = suffix
+ if suffix[0] == "@":
+ altsuffix = "#" + suffix[1:]
+ else:
+ altsuffix = "@" + suffix[1:]
+ continue
+
+ line = line.split()
+
+ if len(line) == 0:
+ continue
+
+ if line[-1].endswith(suffix):
+ line[-1] = line[-1][0:len(line[-1]) - len(suffix)]
+
+ if line[-1].endswith(altsuffix):
+ line[-1] = line[-1][0:len(line[-1]) - len(altsuffix)]
+
+ if line[-1][0] == "$":
+ continue
+
+ # BV assignments
+ if len(line) == 3 and line[1][0] != "[":
+ value = line[1]
+ name = line[2]
+
+ path = smt.get_path(topmod, name)
+
+ if not smt.net_exists(topmod, path):
+ continue
+
+ width = smt.net_width(topmod, path)
+
+ if width == 1:
+ assert value in ["0", "1"]
+ value = "true" if value == "1" else "false"
+ else:
+ value = "#b" + value
+
+ smtexpr = "(= [%s] %s)" % (name, value)
+ constr_assumes[step].append((btorwitfile, smtexpr))
+
+ # Array assignments
+ if len(line) == 4 and line[1][0] == "[":
+ index = line[1]
+ value = line[2]
+ name = line[3]
+
+ path = smt.get_path(topmod, name)
+
+ if not smt.mem_exists(topmod, path):
+ continue
+
+ meminfo = smt.mem_info(topmod, path)
+
+ if meminfo[1] == 1:
+ assert value in ["0", "1"]
+ value = "true" if value == "1" else "false"
+ else:
+ value = "#b" + value
+
+ assert index[0] == "["
+ assert index[-1] == "]"
+ index = "#b" + index[1:-1]
+
+ smtexpr = "(= (select [%s] %s) %s)" % (name, index, value)
+ constr_assumes[step].append((btorwitfile, smtexpr))
+
+ skip_steps = step
+ num_steps = step+1
+
def write_vcd_trace(steps_start, steps_stop, index):
filename = vcdfile.replace("%", index)
print_msg("Writing trace to VCD file: %s" % (filename))
diff --git a/frontends/verific/verific.cc b/frontends/verific/verific.cc
index 971f0b24a..bc035c31a 100644
--- a/frontends/verific/verific.cc
+++ b/frontends/verific/verific.cc
@@ -2094,42 +2094,6 @@ struct VerificPass : public Pass {
if (mode_all)
{
-#if 0
- log("Running veri_file::ElaborateAll().\n");
- if (!veri_file::ElaborateAll())
- log_cmd_error("Elaboration of Verilog modules failed.\n");
-
- log("Running vhdl_file::ElaborateAll().\n");
- if (!vhdl_file::ElaborateAll())
- log_cmd_error("Elaboration of VHDL modules failed.\n");
-
- Library *lib = Netlist::PresentDesign()->Owner()->Owner();
-
- if (argidx == GetSize(args))
- {
- MapIter iter;
- char *iter_name;
- Verific::Cell *iter_cell;
-
- FOREACH_MAP_ITEM(lib->GetCells(), iter, &iter_name, &iter_cell) {
- if (*iter_name != '$')
- nl_todo.insert(iter_cell->GetFirstNetlist());
- }
- }
- else
- {
- for (; argidx < GetSize(args); argidx++)
- {
- Verific::Cell *cell = lib->GetCell(args[argidx].c_str());
-
- if (cell == nullptr)
- log_cmd_error("Module not found: %s\n", args[argidx].c_str());
-
- nl_todo.insert(cell->GetFirstNetlist());
- cell->GetFirstNetlist()->SetPresentDesign();
- }
- }
-#else
log("Running hier_tree::ElaborateAll().\n");
VhdlLibrary *vhdl_lib = vhdl_file::GetLibrary(work.c_str(), 1);
@@ -2146,28 +2110,12 @@ struct VerificPass : public Pass {
FOREACH_ARRAY_ITEM(netlists, i, nl)
nl_todo.insert(nl);
delete netlists;
-#endif
}
else
{
if (argidx == GetSize(args))
log_cmd_error("No top module specified.\n");
-#if 0
- for (; argidx < GetSize(args); argidx++) {
- if (veri_file::GetModule(args[argidx].c_str())) {
- log("Running veri_file::Elaborate(\"%s\").\n", args[argidx].c_str());
- if (!veri_file::Elaborate(args[argidx].c_str()))
- log_cmd_error("Elaboration of top module `%s' failed.\n", args[argidx].c_str());
- nl_todo.insert(Netlist::PresentDesign());
- } else {
- log("Running vhdl_file::Elaborate(\"%s\").\n", args[argidx].c_str());
- if (!vhdl_file::Elaborate(args[argidx].c_str()))
- log_cmd_error("Elaboration of top module `%s' failed.\n", args[argidx].c_str());
- nl_todo.insert(Netlist::PresentDesign());
- }
- }
-#else
Array veri_modules, vhdl_units;
for (; argidx < GetSize(args); argidx++)
{
@@ -2199,7 +2147,6 @@ struct VerificPass : public Pass {
FOREACH_ARRAY_ITEM(netlists, i, nl)
nl_todo.insert(nl);
delete netlists;
-#endif
}
if (!verific_error_msg.empty())
diff --git a/passes/opt/opt_expr.cc b/passes/opt/opt_expr.cc
index 0ba233c62..610edc5e9 100644
--- a/passes/opt/opt_expr.cc
+++ b/passes/opt/opt_expr.cc
@@ -1406,7 +1406,7 @@ void replace_const_cells(RTLIL::Design *design, RTLIL::Module *module, bool cons
if (sigConst.is_fully_const() && sigConst.is_fully_def() && var_signed == false)
{
if (sigConst.is_fully_zero()) {
- RTLIL::SigSpec a_prime(RTLIL::State::S0, 1);
+ RTLIL::SigSpec a_prime(RTLIL::State::S0, GetSize(cell->getPort("\\Y")));
if (is_lt) {
log("Replacing %s cell `%s' (implementing unsigned X<0) with constant false.\n",
log_id(cell->type), log_id(cell));
diff --git a/passes/opt/opt_lut.cc b/passes/opt/opt_lut.cc
index 3c4cb95bb..be050c713 100644
--- a/passes/opt/opt_lut.cc
+++ b/passes/opt/opt_lut.cc
@@ -93,7 +93,7 @@ struct OptLutWorker
}
}
- OptLutWorker(dict<IdString, dict<int, IdString>> &dlogic, RTLIL::Module *module) :
+ OptLutWorker(dict<IdString, dict<int, IdString>> &dlogic, RTLIL::Module *module, int limit) :
dlogic(dlogic), module(module), index(module), sigmap(module)
{
log("Discovering LUTs.\n");
@@ -192,6 +192,12 @@ struct OptLutWorker
pool<RTLIL::Cell*> worklist = luts;
while (worklist.size())
{
+ if (limit == 0)
+ {
+ log("Limit reached.\n");
+ break;
+ }
+
auto lutA = worklist.pop();
SigSpec lutA_input = sigmap(lutA->getPort("\\A"));
SigSpec lutA_output = sigmap(lutA->getPort("\\Y")[0]);
@@ -219,6 +225,12 @@ struct OptLutWorker
log("Found %s.%s (cell A) feeding %s.%s (cell B).\n", log_id(module), log_id(lutA), log_id(module), log_id(lutB));
+ if (index.query_is_output(lutA->getPort("\\Y")))
+ {
+ log(" Not combining LUTs (cascade connection feeds module output).\n");
+ continue;
+ }
+
pool<SigBit> lutA_inputs;
pool<SigBit> lutB_inputs;
for (auto &bit : lutA_input)
@@ -382,8 +394,9 @@ struct OptLutWorker
lutM_new_table[eval] = (RTLIL::State) evaluate_lut(lutB, eval_inputs);
}
- log(" Old truth table: %s.\n", lutM->getParam("\\LUT").as_string().c_str());
- log(" New truth table: %s.\n", lutM_new_table.as_string().c_str());
+ log(" Cell A truth table: %s.\n", lutA->getParam("\\LUT").as_string().c_str());
+ log(" Cell B truth table: %s.\n", lutB->getParam("\\LUT").as_string().c_str());
+ log(" Merged truth table: %s.\n", lutM_new_table.as_string().c_str());
lutM->setParam("\\LUT", lutM_new_table);
lutM->setPort("\\A", lutM_new_inputs);
@@ -398,6 +411,8 @@ struct OptLutWorker
worklist.erase(lutR);
combined_count++;
+ if (limit > 0)
+ limit--;
}
}
}
@@ -431,17 +446,22 @@ struct OptLutPass : public Pass {
log(" the case where both LUT and dedicated logic input are connected to\n");
log(" the same constant.\n");
log("\n");
+ log(" -limit N\n");
+ log(" only perform the first N combines, then stop. useful for debugging.\n");
+ log("\n");
}
void execute(std::vector<std::string> args, RTLIL::Design *design) YS_OVERRIDE
{
log_header(design, "Executing OPT_LUT pass (optimize LUTs).\n");
dict<IdString, dict<int, IdString>> dlogic;
+ int limit = -1;
size_t argidx;
for (argidx = 1; argidx < args.size(); argidx++)
{
- if (args[argidx] == "-dlogic" && argidx+1 < args.size()) {
+ if (args[argidx] == "-dlogic" && argidx+1 < args.size())
+ {
std::vector<std::string> tokens;
split(tokens, args[++argidx], ':');
if (tokens.size() < 2)
@@ -458,6 +478,11 @@ struct OptLutPass : public Pass {
}
continue;
}
+ if (args[argidx] == "-limit" && argidx + 1 < args.size())
+ {
+ limit = atoi(args[++argidx].c_str());
+ continue;
+ }
break;
}
extra_args(args, argidx, design);
@@ -465,7 +490,7 @@ struct OptLutPass : public Pass {
int total_count = 0;
for (auto module : design->selected_modules())
{
- OptLutWorker worker(dlogic, module);
+ OptLutWorker worker(dlogic, module, limit - total_count);
total_count += worker.combined_count;
}
if (total_count)
diff --git a/tests/opt/opt_lut_port.il b/tests/opt/opt_lut_port.il
new file mode 100644
index 000000000..7eb71890f
--- /dev/null
+++ b/tests/opt/opt_lut_port.il
@@ -0,0 +1,18 @@
+module $1
+ wire width 4 input 2 \_0_
+ wire output 4 \_1_
+ wire input 3 \_2_
+ wire output 1 \o
+ cell $lut \_3_
+ parameter \LUT 16'0011000000000011
+ parameter \WIDTH 4
+ connect \A { \_0_ [3] \o 2'00 }
+ connect \Y \_1_
+ end
+ cell $lut \_4_
+ parameter \LUT 4'0001
+ parameter \WIDTH 4
+ connect \A { 3'000 \_2_ }
+ connect \Y \o
+ end
+end
diff --git a/tests/opt/opt_lut_port.ys b/tests/opt/opt_lut_port.ys
new file mode 100644
index 000000000..51dfd988b
--- /dev/null
+++ b/tests/opt/opt_lut_port.ys
@@ -0,0 +1,2 @@
+read_ilang opt_lut_port.il
+select -assert-count 2 t:$lut
diff --git a/tests/svinterfaces/.gitignore b/tests/svinterfaces/.gitignore
new file mode 100644
index 000000000..a5b7927d1
--- /dev/null
+++ b/tests/svinterfaces/.gitignore
@@ -0,0 +1,8 @@
+/a.out
+/dut_result.txt
+/reference_result.txt
+/*.diff
+/*.log_stderr
+/*.log_stdout
+/*_ref_syn.v
+/*_syn.v
generated by cgit v1.2.3 (git 2.25.1) at 2025-05-02 11:21:58 +0000