aboutsummaryrefslogtreecommitdiffstats
diff options
context:
space:
mode:
-rw-r--r--Makefile2
-rw-r--r--backends/smt2/smtbmc.py40
-rw-r--r--frontends/ast/ast.cc6
-rw-r--r--frontends/ast/ast.h1
-rw-r--r--frontends/ast/simplify.cc122
-rw-r--r--frontends/verific/verific.cc118
-rw-r--r--frontends/verilog/verilog_parser.y3
-rw-r--r--passes/opt/opt_clean.cc53
-rwxr-xr-xtests/arch/anlogic/run-test.sh22
-rwxr-xr-xtests/arch/ecp5/run-test.sh22
-rwxr-xr-xtests/arch/efinix/run-test.sh22
-rwxr-xr-xtests/arch/gowin/run-test.sh22
-rwxr-xr-xtests/arch/ice40/run-test.sh22
-rwxr-xr-xtests/arch/intel_alm/run-test.sh22
-rwxr-xr-xtests/arch/xilinx/run-test.sh22
-rwxr-xr-xtests/gen-tests-makefile.sh94
-rwxr-xr-xtests/memories/run-test.sh4
-rw-r--r--tests/opt/.gitignore1
-rw-r--r--tests/opt/opt_clean_mem.ys49
-rwxr-xr-xtests/opt/run-test.sh8
-rwxr-xr-xtests/opt_share/run-test.sh21
-rw-r--r--tests/sat/.gitignore1
-rwxr-xr-xtests/sat/run-test.sh10
-rw-r--r--tests/sat/sizebits.sv61
-rwxr-xr-xtests/simple/run-test.sh1
-rwxr-xr-xtests/svtypes/run-test.sh22
-rw-r--r--tests/techmap/mem_simple_4x1_runtest.sh2
-rw-r--r--tests/techmap/recursive_runtest.sh2
-rwxr-xr-xtests/techmap/run-test.sh22
-rwxr-xr-xtests/various/run-test.sh22
-rw-r--r--tests/verilog/.gitignore2
-rwxr-xr-xtests/verilog/run-test.sh22
32 files changed, 545 insertions, 298 deletions
diff --git a/Makefile b/Makefile
index 8b3ac2445..be34b82fd 100644
--- a/Makefile
+++ b/Makefile
@@ -123,7 +123,7 @@ LDFLAGS += -rdynamic
LDLIBS += -lrt
endif
-YOSYS_VER := 0.9+3599
+YOSYS_VER := 0.9+3624
GIT_REV := $(shell cd $(YOSYS_SRC) && git rev-parse --short HEAD 2> /dev/null || echo UNKNOWN)
OBJS = kernel/version_$(GIT_REV).o
diff --git a/backends/smt2/smtbmc.py b/backends/smt2/smtbmc.py
index 69dab5590..da5a7f57e 100644
--- a/backends/smt2/smtbmc.py
+++ b/backends/smt2/smtbmc.py
@@ -817,6 +817,24 @@ def write_vcd_trace(steps_start, steps_stop, index):
vcd.set_time(steps_stop)
+def char_ok_in_verilog(c,i):
+ if ('A' <= c <= 'Z'): return True
+ if ('a' <= c <= 'z'): return True
+ if ('0' <= c <= '9' and i>0): return True
+ if (c == '_'): return True
+ if (c == '$'): return True
+ return False
+
+def escape_identifier(identifier):
+ if type(identifier) is list:
+ return map(escape_identifier, identifier)
+ if "." in identifier:
+ return ".".join(escape_identifier(identifier.split(".")))
+ if (all(char_ok_in_verilog(identifier[i],i) for i in range(0, len(identifier)))):
+ return identifier
+ return "\\"+identifier+" "
+
+
def write_vlogtb_trace(steps_start, steps_stop, index):
filename = vlogtbfile.replace("%", index)
@@ -858,12 +876,12 @@ def write_vlogtb_trace(steps_start, steps_stop, index):
for name, width in primary_inputs:
if name in clock_inputs:
- print(" wire [%d:0] PI_%s = clock;" % (width-1, name), file=f)
+ print(" wire [%d:0] %s = clock;" % (width-1, escape_identifier("PI_"+name)), file=f)
else:
- print(" reg [%d:0] PI_%s;" % (width-1, name), file=f)
+ print(" reg [%d:0] %s;" % (width-1, escape_identifier("PI_"+name)), file=f)
- print(" %s UUT (" % vlogtb_topmod, file=f)
- print(",\n".join(" .{name}(PI_{name})".format(name=name) for name, _ in primary_inputs), file=f)
+ print(" %s UUT (" % escape_identifier(vlogtb_topmod), file=f)
+ print(",\n".join(" .%s(%s)" % (escape_identifier(name), escape_identifier("PI_"+name)) for name, _ in primary_inputs), file=f)
print(" );", file=f)
print("`ifndef VERILATOR", file=f)
@@ -893,14 +911,14 @@ def write_vlogtb_trace(steps_start, steps_stop, index):
for n in reg:
if n.startswith("$"):
hidden_net = True
- print(" %sUUT.%s = %d'b%s;" % ("// " if hidden_net else "", ".".join(reg), len(val), val), file=f)
+ print(" %sUUT.%s = %d'b%s;" % ("// " if hidden_net else "", ".".join(escape_identifier(reg)), len(val), val), file=f)
anyconsts = sorted(smt.hieranyconsts(vlogtb_topmod))
for info in anyconsts:
if info[3] is not None:
modstate = smt.net_expr(vlogtb_topmod, vlogtb_state.replace("@@step_idx@@", str(steps_start)), info[0])
value = smt.bv2bin(smt.get("(|%s| %s)" % (info[1], modstate)))
- print(" UUT.%s = %d'b%s;" % (".".join(info[0] + [info[3]]), len(value), value), file=f);
+ print(" UUT.%s = %d'b%s;" % (".".join(escape_identifier(info[0] + [info[3]])), len(value), value), file=f);
mems = sorted(smt.hiermems(vlogtb_topmod))
for mempath in mems:
@@ -924,7 +942,7 @@ def write_vlogtb_trace(steps_start, steps_stop, index):
addr_data[addr] = data
for addr, data in addr_data.items():
- print(" UUT.%s[%d'b%s] = %d'b%s;" % (".".join(mempath), len(addr), addr, len(data), data), file=f)
+ print(" UUT.%s[%d'b%s] = %d'b%s;" % (".".join(escape_identifier(mempath)), len(addr), addr, len(data), data), file=f)
print("", file=f)
anyseqs = sorted(smt.hieranyseqs(vlogtb_topmod))
@@ -940,18 +958,18 @@ def write_vlogtb_trace(steps_start, steps_stop, index):
for name, val in zip(pi_names, pi_values):
if i > 0:
- print(" PI_%s <= %d'b%s;" % (".".join(name), len(val), val), file=f)
+ print(" %s <= %d'b%s;" % (escape_identifier("PI_"+".".join(name)), len(val), val), file=f)
else:
- print(" PI_%s = %d'b%s;" % (".".join(name), len(val), val), file=f)
+ print(" %s = %d'b%s;" % (escape_identifier("PI_"+".".join(name)), len(val), val), file=f)
for info in anyseqs:
if info[3] is not None:
modstate = smt.net_expr(vlogtb_topmod, vlogtb_state.replace("@@step_idx@@", str(i)), info[0])
value = smt.bv2bin(smt.get("(|%s| %s)" % (info[1], modstate)))
if i > 0:
- print(" UUT.%s <= %d'b%s;" % (".".join(info[0] + [info[3]]), len(value), value), file=f);
+ print(" UUT.%s <= %d'b%s;" % (".".join(escape_identifier(info[0] + [info[3]])), len(value), value), file=f);
else:
- print(" UUT.%s = %d'b%s;" % (".".join(info[0] + [info[3]]), len(value), value), file=f);
+ print(" UUT.%s = %d'b%s;" % (".".join(escape_identifier(info[0] + [info[3]])), len(value), value), file=f);
if i > 0:
print(" end", file=f)
diff --git a/frontends/ast/ast.cc b/frontends/ast/ast.cc
index 9520ae32c..c8183580b 100644
--- a/frontends/ast/ast.cc
+++ b/frontends/ast/ast.cc
@@ -336,6 +336,12 @@ void AstNode::dumpAst(FILE *f, std::string indent) const
fprintf(f, " %d", v);
fprintf(f, " ]");
}
+ if (!multirange_swapped.empty()) {
+ fprintf(f, " multirange_swapped=[");
+ for (auto v : multirange_swapped)
+ fprintf(f, " %d", v);
+ fprintf(f, " ]");
+ }
if (is_enum) {
fprintf(f, " type=enum");
}
diff --git a/frontends/ast/ast.h b/frontends/ast/ast.h
index 203b50021..1b8ed22ca 100644
--- a/frontends/ast/ast.h
+++ b/frontends/ast/ast.h
@@ -202,6 +202,7 @@ namespace AST
// if this is a multirange memory then this vector contains offset and length of each dimension
std::vector<int> multirange_dimensions;
+ std::vector<bool> multirange_swapped; // true if range is swapped, not used for structs
// this is set by simplify and used during RTLIL generation
AstNode *id2ast;
diff --git a/frontends/ast/simplify.cc b/frontends/ast/simplify.cc
index 153a42e19..fb6623f02 100644
--- a/frontends/ast/simplify.cc
+++ b/frontends/ast/simplify.cc
@@ -1504,11 +1504,13 @@ bool AstNode::simplify(bool const_fold, bool at_zero, bool in_lvalue, int stage,
{
int total_size = 1;
multirange_dimensions.clear();
+ multirange_swapped.clear();
for (auto range : children[1]->children) {
if (!range->range_valid)
log_file_error(filename, location.first_line, "Non-constant range on memory decl.\n");
multirange_dimensions.push_back(min(range->range_left, range->range_right));
multirange_dimensions.push_back(max(range->range_left, range->range_right) - min(range->range_left, range->range_right) + 1);
+ multirange_swapped.push_back(range->range_swapped);
total_size *= multirange_dimensions.back();
}
delete children[1];
@@ -1521,6 +1523,7 @@ bool AstNode::simplify(bool const_fold, bool at_zero, bool in_lvalue, int stage,
{
AstNode *index_expr = nullptr;
+ integer = children[0]->children.size(); // save original number of dimensions for $size() etc.
for (int i = 0; 2*i < GetSize(id2ast->multirange_dimensions); i++)
{
if (GetSize(children[0]->children) <= i)
@@ -1719,6 +1722,7 @@ bool AstNode::simplify(bool const_fold, bool at_zero, bool in_lvalue, int stage,
newNode = new AstNode(AST_IDENTIFIER, children[1]->clone());
newNode->str = wire_id;
+ newNode->integer = integer; // save original number of dimensions for $size() etc.
newNode->id2ast = wire;
goto apply_newNode;
}
@@ -2831,26 +2835,28 @@ skip_dynamic_range_lvalue_expansion:;
goto apply_newNode;
}
- if (str == "\\$size" || str == "\\$bits")
+ if (str == "\\$size" || str == "\\$bits" || str == "\\$high" || str == "\\$low" || str == "\\$left" || str == "\\$right")
{
- if (str == "\\$bits" && children.size() != 1)
- log_file_error(filename, location.first_line, "System function %s got %d arguments, expected 1.\n",
- RTLIL::unescape_id(str).c_str(), int(children.size()));
-
- if (str == "\\$size" && children.size() != 1 && children.size() != 2)
- log_file_error(filename, location.first_line, "System function %s got %d arguments, expected 1 or 2.\n",
- RTLIL::unescape_id(str).c_str(), int(children.size()));
-
int dim = 1;
- if (str == "\\$size" && children.size() == 2) {
- AstNode *buf = children[1]->clone();
- // Evaluate constant expression
- while (buf->simplify(true, false, false, stage, width_hint, sign_hint, false)) { }
- dim = buf->asInt(false);
- delete buf;
+ if (str == "\\$bits") {
+ if (children.size() != 1)
+ log_file_error(filename, location.first_line, "System function %s got %d arguments, expected 1.\n",
+ RTLIL::unescape_id(str).c_str(), int(children.size()));
+ } else {
+ if (children.size() != 1 && children.size() != 2)
+ log_file_error(filename, location.first_line, "System function %s got %d arguments, expected 1 or 2.\n",
+ RTLIL::unescape_id(str).c_str(), int(children.size()));
+ if (children.size() == 2) {
+ AstNode *buf = children[1]->clone();
+ // Evaluate constant expression
+ while (buf->simplify(true, false, false, stage, width_hint, sign_hint, false)) { }
+ dim = buf->asInt(false);
+ delete buf;
+ }
}
AstNode *buf = children[0]->clone();
int mem_depth = 1;
+ int result, high = 0, low = 0, left = 0, right = 0, width = 1; // defaults for a simple wire
AstNode *id_ast = NULL;
// Is this needed?
@@ -2863,6 +2869,31 @@ skip_dynamic_range_lvalue_expansion:;
id_ast = current_scope.at(buf->str);
if (!id_ast)
log_file_error(filename, location.first_line, "Failed to resolve identifier %s for width detection!\n", buf->str.c_str());
+ // a slice of our identifier means we advance to the next dimension, e.g. $size(a[3])
+ if (buf->children.size() > 0) {
+ // something is hanging below this identifier
+ if (buf->children[0]->type == AST_RANGE && buf->integer == 0)
+ // if integer == 0, this node was originally created as AST_RANGE so it's dimension is 1
+ dim++;
+ // more than one range, e.g. $size(a[3][2])
+ else // created an AST_MULTIRANGE, converted to AST_RANGE, but original dimension saved in 'integer' field
+ dim += buf->integer; // increment by multirange size
+ }
+ // We have 4 cases:
+ // wire x; ==> AST_WIRE, no AST_RANGE children
+ // wire [1:0]x; ==> AST_WIRE, AST_RANGE children
+ // wire [1:0]x[1:0]; ==> AST_MEMORY, two AST_RANGE children (1st for packed, 2nd for unpacked)
+ // wire [1:0]x[1:0][1:0]; ==> AST_MEMORY, one AST_RANGE child (0) for packed, then AST_MULTIRANGE child (1) for unpacked
+ // (updated: actually by the time we are here, AST_MULTIRANGE is converted into one big AST_RANGE)
+ // case 0 handled by default
+ if ((id_ast->type == AST_WIRE || id_ast->type == AST_MEMORY) && id_ast->children.size() > 0) {
+ // handle packed array left/right for case 1, and cases 2/3 when requesting the last dimension (packed side)
+ AstNode *wire_range = id_ast->children[0];
+ left = wire_range->children[0]->integer;
+ right = wire_range->children[1]->integer;
+ high = max(left, right);
+ low = min(left, right);
+ }
if (id_ast->type == AST_MEMORY) {
// We got here only if the argument is a memory
// Otherwise $size() and $bits() return the expression width
@@ -2875,29 +2906,58 @@ skip_dynamic_range_lvalue_expansion:;
} else
log_file_error(filename, location.first_line, "Unknown memory depth AST type in `%s'!\n", buf->str.c_str());
} else {
- // $size()
+ // $size(), $left(), $right(), $high(), $low()
+ int dims = 1;
if (mem_range->type == AST_RANGE) {
- if (!mem_range->range_valid)
- log_file_error(filename, location.first_line, "Failed to detect width of memory access `%s'!\n", buf->str.c_str());
- int dims;
- if (id_ast->multirange_dimensions.empty())
- dims = 1;
- else
+ if (id_ast->multirange_dimensions.empty()) {
+ if (!mem_range->range_valid)
+ log_file_error(filename, location.first_line, "Failed to detect width of memory access `%s'!\n", buf->str.c_str());
+ if (dim == 1) {
+ left = mem_range->range_right;
+ right = mem_range->range_left;
+ high = max(left, right);
+ low = min(left, right);
+ }
+ } else {
dims = GetSize(id_ast->multirange_dimensions)/2;
- if (dim == 1)
- width_hint = (dims > 1) ? id_ast->multirange_dimensions[1] : (mem_range->range_left - mem_range->range_right + 1);
- else if (dim <= dims) {
- width_hint = id_ast->multirange_dimensions[2*dim-1];
- } else if ((dim > dims+1) || (dim < 0))
- log_file_error(filename, location.first_line, "Dimension %d out of range in `%s', as it only has dimensions 1..%d!\n", dim, buf->str.c_str(), dims+1);
- } else
+ if (dim <= dims) {
+ width_hint = id_ast->multirange_dimensions[2*dim-1];
+ high = id_ast->multirange_dimensions[2*dim-2] + id_ast->multirange_dimensions[2*dim-1] - 1;
+ low = id_ast->multirange_dimensions[2*dim-2];
+ if (id_ast->multirange_swapped[dim-1]) {
+ left = low;
+ right = high;
+ } else {
+ right = low;
+ left = high;
+ }
+ } else if ((dim > dims+1) || (dim < 0))
+ log_file_error(filename, location.first_line, "Dimension %d out of range in `%s', as it only has dimensions 1..%d!\n", dim, buf->str.c_str(), dims+1);
+ }
+ } else {
log_file_error(filename, location.first_line, "Unknown memory depth AST type in `%s'!\n", buf->str.c_str());
+ }
}
}
+ width = high - low + 1;
+ } else {
+ width = width_hint;
}
delete buf;
-
- newNode = mkconst_int(width_hint * mem_depth, false);
+ if (str == "\\$high")
+ result = high;
+ else if (str == "\\$low")
+ result = low;
+ else if (str == "\\$left")
+ result = left;
+ else if (str == "\\$right")
+ result = right;
+ else if (str == "\\$size")
+ result = width;
+ else {
+ result = width * mem_depth;
+ }
+ newNode = mkconst_int(result, false);
goto apply_newNode;
}
diff --git a/frontends/verific/verific.cc b/frontends/verific/verific.cc
index 7bbda9d49..e236aaaf2 100644
--- a/frontends/verific/verific.cc
+++ b/frontends/verific/verific.cc
@@ -21,6 +21,7 @@
#include "kernel/sigtools.h"
#include "kernel/celltypes.h"
#include "kernel/log.h"
+#include "libs/sha1/sha1.h"
#include <stdlib.h>
#include <stdio.h>
#include <string.h>
@@ -54,7 +55,7 @@ USING_YOSYS_NAMESPACE
# error "Only Symbiotic EDA flavored Verific is supported. Please contact office@symbioticeda.com for commercial support for Yosys+Verific."
#endif
-#if SYMBIOTIC_VERIFIC_API_VERSION < 20200801
+#if SYMBIOTIC_VERIFIC_API_VERSION < 20200902
# error "Please update your version of Symbiotic EDA flavored Verific."
#endif
@@ -864,6 +865,21 @@ void VerificImporter::merge_past_ffs(pool<RTLIL::Cell*> &candidates)
merge_past_ffs_clock(it.second, it.first.first, it.first.second);
}
+static std::string sha1_if_contain_spaces(std::string str)
+{
+ if(str.find_first_of(' ') != std::string::npos) {
+ std::size_t open = str.find_first_of('(');
+ std::size_t closed = str.find_last_of(')');
+ if (open != std::string::npos && closed != std::string::npos) {
+ std::string content = str.substr(open + 1, closed - open - 1);
+ return str.substr(0, open + 1) + sha1(content) + str.substr(closed);
+ } else {
+ return sha1(str);
+ }
+ }
+ return str;
+}
+
void VerificImporter::import_netlist(RTLIL::Design *design, Netlist *nl, std::set<Netlist*> &nl_todo, bool norename)
{
std::string netlist_name = nl->GetAtt(" \\top") ? nl->CellBaseName() : nl->Owner()->Name();
@@ -877,7 +893,7 @@ void VerificImporter::import_netlist(RTLIL::Design *design, Netlist *nl, std::se
module_name += nl->Name();
module_name += ")";
}
- module_name = "\\" + module_name;
+ module_name = "\\" + sha1_if_contain_spaces(module_name);
}
netlist = nl;
@@ -1512,7 +1528,7 @@ void VerificImporter::import_netlist(RTLIL::Design *design, Netlist *nl, std::se
inst_type += inst->View()->Name();
inst_type += ")";
}
- inst_type = "\\" + inst_type;
+ inst_type = "\\" + sha1_if_contain_spaces(inst_type);
}
RTLIL::Cell *cell = module->addCell(inst_name, inst_type);
@@ -2187,6 +2203,9 @@ struct VerificPass : public Pass {
log("\n");
log("Application options:\n");
log("\n");
+ log(" -module <module>\n");
+ log(" Run formal application only on specified module.\n");
+ log("\n");
log(" -blacklist <filename[:lineno]>\n");
log(" Do not run application on modules from files that match the filename\n");
log(" or filename and line number if provided in such format.\n");
@@ -2475,8 +2494,11 @@ struct VerificPass : public Pass {
goto check_error;
}
- if (argidx+1 < GetSize(args) && args[argidx] == "-app")
+ if (argidx < GetSize(args) && args[argidx] == "-app")
{
+ if (!(argidx+1 < GetSize(args)))
+ cmd_error(args, argidx, "No formal application specified.\n");
+
VerificFormalApplications vfa;
auto apps = vfa.GetApps();
std::string app = args[++argidx];
@@ -2484,15 +2506,42 @@ struct VerificPass : public Pass {
if (apps.find(app) == apps.end())
log_cmd_error("Application '%s' does not exist.\n", app.c_str());
+ FormalApplication *application = apps[app];
+ application->setLogger([](std::string msg) { log("%s",msg.c_str()); } );
+ VeriModule *selected_module = nullptr;
+
for (argidx++; argidx < GetSize(args); argidx++) {
- if (args[argidx] == "-blacklist" && argidx+1 < GetSize(args)) {
+ std::string error;
+ if (application->checkParams(args, argidx, error)) {
+ if (!error.empty())
+ cmd_error(args, argidx, error);
+ continue;
+ }
+
+ if (args[argidx] == "-module" && argidx < GetSize(args)) {
+ if (!(argidx+1 < GetSize(args)))
+ cmd_error(args, argidx+1, "No module name specified.\n");
+ std::string module = args[++argidx];
+ VeriLibrary* veri_lib = veri_file::GetLibrary(work.c_str(), 1);
+ selected_module = veri_lib ? veri_lib->GetModule(module.c_str(), 1) : nullptr;
+ if (!selected_module) {
+ log_error("Can't find module '%s'.\n", module.c_str());
+ }
+ continue;
+ }
+ if (args[argidx] == "-blacklist" && argidx < GetSize(args)) {
+ if (!(argidx+1 < GetSize(args)))
+ cmd_error(args, argidx+1, "No blacklist specified.\n");
+
std::string line = args[++argidx];
std::string p;
while (!(p = next_token(line, ",\t\r\n ")).empty())
blacklists.push_back(p);
continue;
}
- if (args[argidx] == "-blfile" && argidx+1 < GetSize(args)) {
+ if (args[argidx] == "-blfile" && argidx < GetSize(args)) {
+ if (!(argidx+1 < GetSize(args)))
+ cmd_error(args, argidx+1, "No blacklist file specified.\n");
std::string fn = args[++argidx];
std::ifstream f(fn);
if (f.fail())
@@ -2509,12 +2558,32 @@ struct VerificPass : public Pass {
}
if (argidx < GetSize(args))
cmd_error(args, argidx, "unknown option/parameter");
+
+ application->setBlacklists(&blacklists);
+ application->setSingleModuleMode(selected_module!=nullptr);
+
+ const char *err = application->validate();
+ if (err)
+ cmd_error(args, argidx, err);
+
MapIter mi;
- VeriModule *module ;
VeriLibrary *veri_lib = veri_file::GetLibrary(work.c_str(), 1);
log("Running formal application '%s'.\n", app.c_str());
- FOREACH_VERILOG_MODULE_IN_LIBRARY(veri_lib, mi, module) {
- vfa.Run(module,apps[app],blacklists);
+
+ if (selected_module) {
+ std::string out;
+ if (!application->execute(selected_module, out))
+ log_error("%s", out.c_str());
+ }
+ else {
+ VeriModule *module ;
+ FOREACH_VERILOG_MODULE_IN_LIBRARY(veri_lib, mi, module) {
+ std::string out;
+ if (!application->execute(module, out)) {
+ log_error("%s", out.c_str());
+ break;
+ }
+ }
}
goto check_error;
}
@@ -2563,8 +2632,8 @@ struct VerificPass : public Pass {
if (argidx < GetSize(args) && args[argidx] == "-template")
{
- if (!(argidx < GetSize(args)))
- cmd_error(args, argidx, "No template type specified.\n");
+ if (!(argidx+1 < GetSize(args)))
+ cmd_error(args, argidx+1, "No template type specified.\n");
VerificTemplateGenerator vfg;
auto gens = vfg.GetGenerators();
@@ -2572,8 +2641,9 @@ struct VerificPass : public Pass {
if (gens.find(app) == gens.end())
log_cmd_error("Template generator '%s' does not exist.\n", app.c_str());
TemplateGenerator *generator = gens[app];
- if (!(argidx < GetSize(args)))
- cmd_error(args, argidx, "No top module specified.\n");
+ if (!(argidx+1 < GetSize(args)))
+ cmd_error(args, argidx+1, "No top module specified.\n");
+ generator->setLogger([](std::string msg) { log("%s",msg.c_str()); } );
std::string module = args[++argidx];
VeriLibrary* veri_lib = veri_file::GetLibrary(work.c_str(), 1);
@@ -2588,9 +2658,19 @@ struct VerificPass : public Pass {
const char *out_filename = nullptr;
for (argidx++; argidx < GetSize(args); argidx++) {
- if (generator->checkParams(args, argidx))
+ std::string error;
+ if (generator->checkParams(args, argidx, error)) {
+ if (!error.empty())
+ cmd_error(args, argidx, error);
continue;
- if (args[argidx] == "-chparam" && argidx+2 < GetSize(args)) {
+ }
+
+ if (args[argidx] == "-chparam" && argidx < GetSize(args)) {
+ if (!(argidx+1 < GetSize(args)))
+ cmd_error(args, argidx+1, "No param name specified.\n");
+ if (!(argidx+2 < GetSize(args)))
+ cmd_error(args, argidx+2, "No param value specified.\n");
+
const std::string &key = args[++argidx];
const std::string &value = args[++argidx];
unsigned new_insertion = parameters.Insert(key.c_str(), value.c_str(),
@@ -2600,7 +2680,9 @@ struct VerificPass : public Pass {
continue;
}
- if (args[argidx] == "-out" && argidx+1 < GetSize(args)) {
+ if (args[argidx] == "-out" && argidx < GetSize(args)) {
+ if (!(argidx+1 < GetSize(args)))
+ cmd_error(args, argidx+1, "No output file specified.\n");
out_filename = args[++argidx].c_str();
continue;
}
@@ -2614,7 +2696,9 @@ struct VerificPass : public Pass {
if (err)
cmd_error(args, argidx, err);
- std::string val = generator->generate(veri_module, &parameters);
+ std::string val;
+ if (!generator->generate(veri_module, val, &parameters))
+ log_error("%s", val.c_str());
FILE *of = stdout;
if (out_filename) {
diff --git a/frontends/verilog/verilog_parser.y b/frontends/verilog/verilog_parser.y
index 8e5236639..678ce6c87 100644
--- a/frontends/verilog/verilog_parser.y
+++ b/frontends/verilog/verilog_parser.y
@@ -1891,6 +1891,9 @@ cell_parameter:
astbuf1->children.push_back(node);
node->children.push_back($1);
} |
+ '.' TOK_ID '(' ')' {
+ // just ignore empty parameters
+ } |
'.' TOK_ID '(' expr ')' {
AstNode *node = new AstNode(AST_PARASET);
node->str = *$2;
diff --git a/passes/opt/opt_clean.cc b/passes/opt/opt_clean.cc
index bd9856e81..883374cf6 100644
--- a/passes/opt/opt_clean.cc
+++ b/passes/opt/opt_clean.cc
@@ -55,7 +55,7 @@ struct keep_cache_t
if (!module->get_bool_attribute(ID::keep)) {
bool found_keep = false;
for (auto cell : module->cells())
- if (query(cell, true /* ignore_specify_mem */)) {
+ if (query(cell, true /* ignore_specify */)) {
found_keep = true;
break;
}
@@ -70,12 +70,12 @@ struct keep_cache_t
return cache[module];
}
- bool query(Cell *cell, bool ignore_specify_mem = false)
+ bool query(Cell *cell, bool ignore_specify = false)
{
if (cell->type.in(ID($assert), ID($assume), ID($live), ID($fair), ID($cover)))
return true;
- if (!ignore_specify_mem && cell->type.in(ID($memwr), ID($meminit), ID($specify2), ID($specify3), ID($specrule)))
+ if (!ignore_specify && cell->type.in(ID($specify2), ID($specify3), ID($specrule)))
return true;
if (cell->has_keep_attr())
@@ -95,6 +95,8 @@ int count_rm_cells, count_rm_wires;
void rmunused_module_cells(Module *module, bool verbose)
{
SigMap sigmap(module);
+ dict<IdString, pool<Cell*>> mem2cells;
+ pool<IdString> mem_unused;
pool<Cell*> queue, unused;
pool<SigBit> used_raw_bits;
dict<SigBit, pool<Cell*>> wire2driver;
@@ -108,6 +110,17 @@ void rmunused_module_cells(Module *module, bool verbose)
}
}
+ for (auto &it : module->memories) {
+ mem_unused.insert(it.first);
+ }
+
+ for (Cell *cell : module->cells()) {
+ if (cell->type.in(ID($memwr), ID($meminit))) {
+ IdString mem_id = cell->getParam(ID::MEMID).decode_string();
+ mem2cells[mem_id].insert(cell);
+ }
+ }
+
for (auto &it : module->cells_) {
Cell *cell = it.second;
for (auto &it2 : cell->connections()) {
@@ -145,17 +158,33 @@ void rmunused_module_cells(Module *module, bool verbose)
while (!queue.empty())
{
pool<SigBit> bits;
- for (auto cell : queue)
- for (auto &it : cell->connections())
- if (!ct_all.cell_known(cell->type) || ct_all.cell_input(cell->type, it.first))
- for (auto bit : sigmap(it.second))
- bits.insert(bit);
+ pool<IdString> mems;
+ for (auto cell : queue) {
+ for (auto &it : cell->connections())
+ if (!ct_all.cell_known(cell->type) || ct_all.cell_input(cell->type, it.first))
+ for (auto bit : sigmap(it.second))
+ bits.insert(bit);
+
+ if (cell->type == ID($memrd)) {
+ IdString mem_id = cell->getParam(ID::MEMID).decode_string();
+ if (mem_unused.count(mem_id)) {
+ mem_unused.erase(mem_id);
+ mems.insert(mem_id);
+ }
+ }
+ }
queue.clear();
+
for (auto bit : bits)
for (auto c : wire2driver[bit])
if (unused.count(c))
queue.insert(c), unused.erase(c);
+
+ for (auto mem : mems)
+ for (auto c : mem2cells[mem])
+ if (unused.count(c))
+ queue.insert(c), unused.erase(c);
}
unused.sort(RTLIL::sort_by_name_id<RTLIL::Cell>());
@@ -168,6 +197,14 @@ void rmunused_module_cells(Module *module, bool verbose)
count_rm_cells++;
}
+ for (auto it : mem_unused)
+ {
+ if (verbose)
+ log_debug(" removing unused memory `%s'.\n", it.c_str());
+ delete module->memories.at(it);
+ module->memories.erase(it);
+ }
+
for (auto &it : module->cells_) {
Cell *cell = it.second;
for (auto &it2 : cell->connections()) {
diff --git a/tests/arch/anlogic/run-test.sh b/tests/arch/anlogic/run-test.sh
index bf19b887d..4be4b70ae 100755
--- a/tests/arch/anlogic/run-test.sh
+++ b/tests/arch/anlogic/run-test.sh
@@ -1,20 +1,4 @@
#!/usr/bin/env bash
-set -e
-{
-echo "all::"
-for x in *.ys; do
- echo "all:: run-$x"
- echo "run-$x:"
- echo " @echo 'Running $x..'"
- echo " @../../../yosys -ql ${x%.ys}.log -w 'Yosys has only limited support for tri-state logic at the moment.' $x"
-done
-for s in *.sh; do
- if [ "$s" != "run-test.sh" ]; then
- echo "all:: run-$s"
- echo "run-$s:"
- echo " @echo 'Running $s..'"
- echo " @bash $s"
- fi
-done
-} > run-test.mk
-exec ${MAKE:-make} -f run-test.mk
+set -eu
+source ../../gen-tests-makefile.sh
+run_tests --yosys-scripts --bash --yosys-args "-w 'Yosys has only limited support for tri-state logic at the moment.'"
diff --git a/tests/arch/ecp5/run-test.sh b/tests/arch/ecp5/run-test.sh
index bf19b887d..4be4b70ae 100755
--- a/tests/arch/ecp5/run-test.sh
+++ b/tests/arch/ecp5/run-test.sh
@@ -1,20 +1,4 @@
#!/usr/bin/env bash
-set -e
-{
-echo "all::"
-for x in *.ys; do
- echo "all:: run-$x"
- echo "run-$x:"
- echo " @echo 'Running $x..'"
- echo " @../../../yosys -ql ${x%.ys}.log -w 'Yosys has only limited support for tri-state logic at the moment.' $x"
-done
-for s in *.sh; do
- if [ "$s" != "run-test.sh" ]; then
- echo "all:: run-$s"
- echo "run-$s:"
- echo " @echo 'Running $s..'"
- echo " @bash $s"
- fi
-done
-} > run-test.mk
-exec ${MAKE:-make} -f run-test.mk
+set -eu
+source ../../gen-tests-makefile.sh
+run_tests --yosys-scripts --bash --yosys-args "-w 'Yosys has only limited support for tri-state logic at the moment.'"
diff --git a/tests/arch/efinix/run-test.sh b/tests/arch/efinix/run-test.sh
index bf19b887d..4be4b70ae 100755
--- a/tests/arch/efinix/run-test.sh
+++ b/tests/arch/efinix/run-test.sh
@@ -1,20 +1,4 @@
#!/usr/bin/env bash
-set -e
-{
-echo "all::"
-for x in *.ys; do
- echo "all:: run-$x"
- echo "run-$x:"
- echo " @echo 'Running $x..'"
- echo " @../../../yosys -ql ${x%.ys}.log -w 'Yosys has only limited support for tri-state logic at the moment.' $x"
-done
-for s in *.sh; do
- if [ "$s" != "run-test.sh" ]; then
- echo "all:: run-$s"
- echo "run-$s:"
- echo " @echo 'Running $s..'"
- echo " @bash $s"
- fi
-done
-} > run-test.mk
-exec ${MAKE:-make} -f run-test.mk
+set -eu
+source ../../gen-tests-makefile.sh
+run_tests --yosys-scripts --bash --yosys-args "-w 'Yosys has only limited support for tri-state logic at the moment.'"
diff --git a/tests/arch/gowin/run-test.sh b/tests/arch/gowin/run-test.sh
index bf19b887d..4be4b70ae 100755
--- a/tests/arch/gowin/run-test.sh
+++ b/tests/arch/gowin/run-test.sh
@@ -1,20 +1,4 @@
#!/usr/bin/env bash
-set -e
-{
-echo "all::"
-for x in *.ys; do
- echo "all:: run-$x"
- echo "run-$x:"
- echo " @echo 'Running $x..'"
- echo " @../../../yosys -ql ${x%.ys}.log -w 'Yosys has only limited support for tri-state logic at the moment.' $x"
-done
-for s in *.sh; do
- if [ "$s" != "run-test.sh" ]; then
- echo "all:: run-$s"
- echo "run-$s:"
- echo " @echo 'Running $s..'"
- echo " @bash $s"
- fi
-done
-} > run-test.mk
-exec ${MAKE:-make} -f run-test.mk
+set -eu
+source ../../gen-tests-makefile.sh
+run_tests --yosys-scripts --bash --yosys-args "-w 'Yosys has only limited support for tri-state logic at the moment.'"
diff --git a/tests/arch/ice40/run-test.sh b/tests/arch/ice40/run-test.sh
index bf19b887d..4be4b70ae 100755
--- a/tests/arch/ice40/run-test.sh
+++ b/tests/arch/ice40/run-test.sh
@@ -1,20 +1,4 @@
#!/usr/bin/env bash
-set -e
-{
-echo "all::"
-for x in *.ys; do
- echo "all:: run-$x"
- echo "run-$x:"
- echo " @echo 'Running $x..'"
- echo " @../../../yosys -ql ${x%.ys}.log -w 'Yosys has only limited support for tri-state logic at the moment.' $x"
-done
-for s in *.sh; do
- if [ "$s" != "run-test.sh" ]; then
- echo "all:: run-$s"
- echo "run-$s:"
- echo " @echo 'Running $s..'"
- echo " @bash $s"
- fi
-done
-} > run-test.mk
-exec ${MAKE:-make} -f run-test.mk
+set -eu
+source ../../gen-tests-makefile.sh
+run_tests --yosys-scripts --bash --yosys-args "-w 'Yosys has only limited support for tri-state logic at the moment.'"
diff --git a/tests/arch/intel_alm/run-test.sh b/tests/arch/intel_alm/run-test.sh
index bf19b887d..4be4b70ae 100755
--- a/tests/arch/intel_alm/run-test.sh
+++ b/tests/arch/intel_alm/run-test.sh
@@ -1,20 +1,4 @@
#!/usr/bin/env bash
-set -e
-{
-echo "all::"
-for x in *.ys; do
- echo "all:: run-$x"
- echo "run-$x:"
- echo " @echo 'Running $x..'"
- echo " @../../../yosys -ql ${x%.ys}.log -w 'Yosys has only limited support for tri-state logic at the moment.' $x"
-done
-for s in *.sh; do
- if [ "$s" != "run-test.sh" ]; then
- echo "all:: run-$s"
- echo "run-$s:"
- echo " @echo 'Running $s..'"
- echo " @bash $s"
- fi
-done
-} > run-test.mk
-exec ${MAKE:-make} -f run-test.mk
+set -eu
+source ../../gen-tests-makefile.sh
+run_tests --yosys-scripts --bash --yosys-args "-w 'Yosys has only limited support for tri-state logic at the moment.'"
diff --git a/tests/arch/xilinx/run-test.sh b/tests/arch/xilinx/run-test.sh
index bf19b887d..4be4b70ae 100755
--- a/tests/arch/xilinx/run-test.sh
+++ b/tests/arch/xilinx/run-test.sh
@@ -1,20 +1,4 @@
#!/usr/bin/env bash
-set -e
-{
-echo "all::"
-for x in *.ys; do
- echo "all:: run-$x"
- echo "run-$x:"
- echo " @echo 'Running $x..'"
- echo " @../../../yosys -ql ${x%.ys}.log -w 'Yosys has only limited support for tri-state logic at the moment.' $x"
-done
-for s in *.sh; do
- if [ "$s" != "run-test.sh" ]; then
- echo "all:: run-$s"
- echo "run-$s:"
- echo " @echo 'Running $s..'"
- echo " @bash $s"
- fi
-done
-} > run-test.mk
-exec ${MAKE:-make} -f run-test.mk
+set -eu
+source ../../gen-tests-makefile.sh
+run_tests --yosys-scripts --bash --yosys-args "-w 'Yosys has only limited support for tri-state logic at the moment.'"
diff --git a/tests/gen-tests-makefile.sh b/tests/gen-tests-makefile.sh
new file mode 100755
index 000000000..ab8fb7013
--- /dev/null
+++ b/tests/gen-tests-makefile.sh
@@ -0,0 +1,94 @@
+set -eu
+
+YOSYS_BASEDIR="$(cd "$(dirname "${BASH_SOURCE[0]}")"/../ >/dev/null 2>&1 && pwd)"
+
+# $ generate_target target_name test_command
+generate_target() {
+ target_name=$1
+ test_command=$2
+ echo "all: $target_name"
+ echo ".PHONY: $target_name"
+ echo "$target_name:"
+ printf "\t@%s\n" "$test_command"
+ printf "\t@echo 'Passed %s'\n" "$target_name"
+}
+
+# $ generate_ys_test ys_file [yosys_args]
+generate_ys_test() {
+ ys_file=$1
+ yosys_args=${2:-}
+ generate_target "$ys_file" "$YOSYS_BASEDIR/yosys -ql ${ys_file%.*}.log $yosys_args $ys_file"
+}
+
+# $ generate_bash_test bash_file
+generate_bash_test() {
+ bash_file=$1
+ generate_target "$bash_file" "bash -v $bash_file >${bash_file%.*}.log 2>&1"
+}
+
+# $ generate_tests [-y|--yosys-scripts] [-s|--prove-sv] [-b|--bash] [-a|--yosys-args yosys_args]
+generate_tests() {
+ do_ys=false
+ do_sv=false
+ do_sh=false
+ yosys_args=""
+
+ while [[ $# -gt 0 ]]; do
+ arg="$1"
+ case "$arg" in
+ -y|--yosys-scripts)
+ do_ys=true
+ shift
+ ;;
+ -s|--prove-sv)
+ do_sv=true
+ shift
+ ;;
+ -b|--bash)
+ do_sh=true
+ shift
+ ;;
+ -a|--yosys-args)
+ yosys_args+="$2"
+ shift
+ shift
+ ;;
+ *)
+ echo >&2 "Unknown argument: $1"
+ exit 1
+ esac
+ done
+
+ if [[ ! ( $do_ys = true || $do_sv = true || $do_sh = true ) ]]; then
+ echo >&2 "Error: No file types selected"
+ exit 1
+ fi
+
+ echo ".PHONY: all"
+ echo "all:"
+
+ if [[ $do_ys = true ]]; then
+ for x in *.ys; do
+ generate_ys_test "$x" "$yosys_args"
+ done
+ fi;
+ if [[ $do_sv = true ]]; then
+ for x in *.sv; do
+ if [ ! -f "${x%.sv}.ys" ]; then
+ generate_ys_test "$x" "-p \"prep -top top; sat -verify -prove-asserts\" $yosys_args"
+ fi;
+ done
+ fi;
+ if [[ $do_sh == true ]]; then
+ for s in *.sh; do
+ if [ "$s" != "run-test.sh" ]; then
+ generate_bash_test "$s"
+ fi
+ done
+ fi
+}
+
+run_tests() {
+ generate_tests "$@" > run-test.mk
+ exec ${MAKE:-make} -f run-test.mk
+}
diff --git a/tests/memories/run-test.sh b/tests/memories/run-test.sh
index 8d1a8b413..376f5bf79 100755
--- a/tests/memories/run-test.sh
+++ b/tests/memories/run-test.sh
@@ -9,12 +9,12 @@ while getopts "A:S:" opt
do
case "$opt" in
A) abcopt="-A $OPTARG" ;;
- S) seed="-S $OPTARG" ;;
+ S) seed="$OPTARG" ;;
esac
done
shift "$((OPTIND-1))"
-bash ../tools/autotest.sh $abcopt $seed -G *.v
+${MAKE:-make} -f ../tools/autotest.mk SEED="$seed" EXTRA_FLAGS="$abcopt" *.v
for f in `egrep -l 'expect-(wr-ports|rd-ports|rd-clk)' *.v`; do
echo -n "Testing expectations for $f .."
diff --git a/tests/opt/.gitignore b/tests/opt/.gitignore
index 397b4a762..8355de9dc 100644
--- a/tests/opt/.gitignore
+++ b/tests/opt/.gitignore
@@ -1 +1,2 @@
*.log
+run-test.mk
diff --git a/tests/opt/opt_clean_mem.ys b/tests/opt/opt_clean_mem.ys
new file mode 100644
index 000000000..b35b15871
--- /dev/null
+++ b/tests/opt/opt_clean_mem.ys
@@ -0,0 +1,49 @@
+read_verilog <<EOT
+module top(...);
+
+input [7:0] wa;
+input [7:0] ra1;
+input [7:0] ra2;
+input [7:0] wd;
+input clk;
+wire [7:0] rd1;
+wire [7:0] rd2;
+
+reg [7:0] mem[0:7];
+
+always @(posedge clk)
+ mem[wa] <= wd;
+assign rd1 = mem[ra1];
+assign rd2 = mem[ra2];
+
+initial mem[8'h12] = 8'h34;
+
+endmodule
+EOT
+
+proc
+memory_dff
+
+select -assert-count 2 t:$memrd
+select -assert-count 1 t:$memwr
+select -assert-count 1 t:$meminit
+design -save orig
+
+opt_clean
+select -assert-none t:$memrd
+select -assert-none t:$memwr
+select -assert-none t:$meminit
+
+design -load orig
+expose top/rd1
+opt_clean
+select -assert-count 1 t:$memrd
+select -assert-count 1 t:$memwr
+select -assert-count 1 t:$meminit
+
+design -load orig
+expose top/rd1 top/rd2
+opt_clean
+select -assert-count 2 t:$memrd
+select -assert-count 1 t:$memwr
+select -assert-count 1 t:$meminit
diff --git a/tests/opt/run-test.sh b/tests/opt/run-test.sh
index 44ce7e674..2007cd6e4 100755
--- a/tests/opt/run-test.sh
+++ b/tests/opt/run-test.sh
@@ -1,6 +1,4 @@
#!/bin/bash
-set -e
-for x in *.ys; do
- echo "Running $x.."
- ../../yosys -ql ${x%.ys}.log $x
-done
+set -eu
+source ../gen-tests-makefile.sh
+run_tests --yosys-scripts
diff --git a/tests/opt_share/run-test.sh b/tests/opt_share/run-test.sh
index e01552646..e0008a259 100755
--- a/tests/opt_share/run-test.sh
+++ b/tests/opt_share/run-test.sh
@@ -22,12 +22,23 @@ mkdir -p temp
echo "generating tests.."
python3 generate.py -c $count $seed
+{
+ echo ".PHONY: all"
+ echo "all:"
+
+ for i in $( ls temp/*.ys | sed 's,[^0-9],,g; s,^0*\(.\),\1,g;' ); do
+ idx=$( printf "%05d" $i )
+ echo ".PHONY: test-$idx"
+ echo "all: test-$idx"
+ echo "test-$idx:"
+ printf "\t@%s\n" \
+ "echo -n [$i]" \
+ "../../yosys -ql temp/uut_${idx}.log temp/uut_${idx}.ys"
+ done
+} > temp/makefile
+
echo "running tests.."
-for i in $( ls temp/*.ys | sed 's,[^0-9],,g; s,^0*\(.\),\1,g;' ); do
- echo -n "[$i]"
- idx=$( printf "%05d" $i )
- ../../yosys -ql temp/uut_${idx}.log temp/uut_${idx}.ys
-done
+${MAKE:-make} -f temp/makefile
echo
failed_share=$( echo $( gawk '/^#job#/ { j=$2; db[j]=0; } /^Removing [246] cells/ { delete db[j]; } END { for (j in db) print(j); }' temp/all_share_log.txt ) )
diff --git a/tests/sat/.gitignore b/tests/sat/.gitignore
index 397b4a762..8355de9dc 100644
--- a/tests/sat/.gitignore
+++ b/tests/sat/.gitignore
@@ -1 +1,2 @@
*.log
+run-test.mk
diff --git a/tests/sat/run-test.sh b/tests/sat/run-test.sh
index 67e1beb23..74589dfeb 100755
--- a/tests/sat/run-test.sh
+++ b/tests/sat/run-test.sh
@@ -1,6 +1,4 @@
-#!/bin/bash
-set -e
-for x in *.ys; do
- echo "Running $x.."
- ../../yosys -ql ${x%.ys}.log $x
-done
+#!/usr/bin/env bash
+set -eu
+source ../gen-tests-makefile.sh
+run_tests --yosys-scripts
diff --git a/tests/sat/sizebits.sv b/tests/sat/sizebits.sv
index d7ce2326e..87fa08f89 100644
--- a/tests/sat/sizebits.sv
+++ b/tests/sat/sizebits.sv
@@ -1,5 +1,6 @@
module functions01;
+wire t;
wire [5:2]x;
wire [3:0]y[2:7];
wire [3:0]z[7:2][2:9];
@@ -9,24 +10,84 @@ wire [3:0]z[7:2][2:9];
//wire [$size(y)-1:0]y_size;
//wire [$size(z)-1:0]z_size;
+assert property ($size(t) == 1);
assert property ($size(x) == 4);
assert property ($size({3{x}}) == 3*4);
assert property ($size(y) == 6);
assert property ($size(y, 1) == 6);
assert property ($size(y, (1+1)) == 4);
+// This is unsupported at the moment
+//assert property ($size(y[2], 1) == 4);
+//assert property ($size(y[2][1], 1) == 1);
assert property ($size(z) == 6);
assert property ($size(z, 1) == 6);
assert property ($size(z, 2) == 8);
assert property ($size(z, 3) == 4);
+// This is unsupported at the moment
+assert property ($size(z[3], 1) == 8);
+assert property ($size(z[3][3], 1) == 4);
+//assert property ($size(z[3][3][3], 1) == 1);
// This should trigger an error if enabled (it does).
//assert property ($size(z, 4) == 4);
//wire [$bits(x)-1:0]x_bits;
//wire [$bits({x, x})-1:0]xx_bits;
+assert property ($bits(t) == 1);
assert property ($bits(x) == 4);
assert property ($bits(y) == 4*6);
assert property ($bits(z) == 4*6*8);
+assert property ($high(x) == 5);
+assert property ($high(y) == 7);
+assert property ($high(y, 1) == 7);
+assert property ($high(y, (1+1)) == 3);
+
+assert property ($high(z) == 7);
+assert property ($high(z, 1) == 7);
+assert property ($high(z, 2) == 9);
+assert property ($high(z, 3) == 3);
+assert property ($high(z[3]) == 9);
+assert property ($high(z[3][3]) == 3);
+assert property ($high(z[3], 2) == 3);
+
+assert property ($low(x) == 2);
+assert property ($low(y) == 2);
+assert property ($low(y, 1) == 2);
+assert property ($low(y, (1+1)) == 0);
+
+assert property ($low(z) == 2);
+assert property ($low(z, 1) == 2);
+assert property ($low(z, 2) == 2);
+assert property ($low(z, 3) == 0);
+assert property ($low(z[3]) == 2);
+assert property ($low(z[3][3]) == 0);
+assert property ($low(z[3], 2) == 0);
+
+assert property ($left(x) == 5);
+assert property ($left(y) == 2);
+assert property ($left(y, 1) == 2);
+assert property ($left(y, (1+1)) == 3);
+
+assert property ($left(z) == 7);
+assert property ($left(z, 1) == 7);
+assert property ($left(z, 2) == 2);
+assert property ($left(z, 3) == 3);
+assert property ($left(z[3]) == 2);
+assert property ($left(z[3][3]) == 3);
+assert property ($left(z[3], 2) == 3);
+
+assert property ($right(x) == 2);
+assert property ($right(y) == 7);
+assert property ($right(y, 1) == 7);
+assert property ($right(y, (1+1)) == 0);
+
+assert property ($right(z) == 2);
+assert property ($right(z, 1) == 2);
+assert property ($right(z, 2) == 9);
+assert property ($right(z, 3) == 0);
+assert property ($right(z[3]) == 9);
+assert property ($right(z[3][3]) == 0);
+assert property ($right(z[3], 2) == 0);
endmodule
diff --git a/tests/simple/run-test.sh b/tests/simple/run-test.sh
index f20fd0d30..47bcfd6da 100755
--- a/tests/simple/run-test.sh
+++ b/tests/simple/run-test.sh
@@ -17,5 +17,4 @@ if ! command -v iverilog > /dev/null ; then
exit 1
fi
-shopt -s nullglob
exec ${MAKE:-make} -f ../tools/autotest.mk $seed *.{sv,v}
diff --git a/tests/svtypes/run-test.sh b/tests/svtypes/run-test.sh
index 09a30eed1..91ceae227 100755
--- a/tests/svtypes/run-test.sh
+++ b/tests/svtypes/run-test.sh
@@ -1,20 +1,4 @@
#!/usr/bin/env bash
-set -e
-{
-echo "all::"
-for x in *.ys; do
- echo "all:: run-$x"
- echo "run-$x:"
- echo " @echo 'Running $x..'"
- echo " @../../yosys -ql ${x%.ys}.log $x"
-done
-for x in *.sv; do
- if [ ! -f "${x%.sv}.ys" ]; then
- echo "all:: check-$x"
- echo "check-$x:"
- echo " @echo 'Checking $x..'"
- echo " @../../yosys -ql ${x%.sv}.log -p \"prep -top top; sat -verify -prove-asserts\" $x"
- fi
-done
-} > run-test.mk
-exec ${MAKE:-make} -f run-test.mk
+set -eu
+source ../gen-tests-makefile.sh
+run_tests --yosys-scripts --prove-sv
diff --git a/tests/techmap/mem_simple_4x1_runtest.sh b/tests/techmap/mem_simple_4x1_runtest.sh
index e2c6303da..9c41fa56a 100644
--- a/tests/techmap/mem_simple_4x1_runtest.sh
+++ b/tests/techmap/mem_simple_4x1_runtest.sh
@@ -1,6 +1,6 @@
#!/bin/bash
-set -ev
+set -e
../../yosys -b 'verilog -noattr' -o mem_simple_4x1_synth.v -p 'proc; opt; memory -nomap; techmap -map mem_simple_4x1_map.v;; techmap; opt; abc;; stat' mem_simple_4x1_uut.v
diff --git a/tests/techmap/recursive_runtest.sh b/tests/techmap/recursive_runtest.sh
index 30c79bf03..0725ccf40 100644
--- a/tests/techmap/recursive_runtest.sh
+++ b/tests/techmap/recursive_runtest.sh
@@ -1,3 +1,3 @@
-set -ev
+set -e
../../yosys -p 'hierarchy -top top; techmap -map recursive_map.v -max_iter 1; select -assert-count 2 t:sub; select -assert-count 2 t:bar' recursive.v
diff --git a/tests/techmap/run-test.sh b/tests/techmap/run-test.sh
index c16f204d9..581847ab0 100755
--- a/tests/techmap/run-test.sh
+++ b/tests/techmap/run-test.sh
@@ -1,20 +1,4 @@
#!/usr/bin/env bash
-set -e
-{
-echo "all::"
-for x in *.ys; do
- echo "all:: run-$x"
- echo "run-$x:"
- echo " @echo 'Running $x..'"
- echo " @../../yosys -ql ${x%.ys}.log -e 'select out of bounds' $x"
-done
-for s in *.sh; do
- if [ "$s" != "run-test.sh" ]; then
- echo "all:: run-$s"
- echo "run-$s:"
- echo " @echo 'Running $s..'"
- echo " @bash $s > ${s%.sh}.log 2>&1"
- fi
-done
-} > run-test.mk
-exec ${MAKE:-make} -f run-test.mk
+set -eu
+source ../gen-tests-makefile.sh
+run_tests --yosys-scripts --bash --yosys-args "-e 'select out of bounds'"
diff --git a/tests/various/run-test.sh b/tests/various/run-test.sh
index ea56b70f0..2f91cf0fd 100755
--- a/tests/various/run-test.sh
+++ b/tests/various/run-test.sh
@@ -1,20 +1,4 @@
#!/usr/bin/env bash
-set -e
-{
-echo "all::"
-for x in *.ys; do
- echo "all:: run-$x"
- echo "run-$x:"
- echo " @echo 'Running $x..'"
- echo " @../../yosys -ql ${x%.ys}.log $x"
-done
-for s in *.sh; do
- if [ "$s" != "run-test.sh" ]; then
- echo "all:: run-$s"
- echo "run-$s:"
- echo " @echo 'Running $s..'"
- echo " @bash $s"
- fi
-done
-} > run-test.mk
-exec ${MAKE:-make} -f run-test.mk
+set -eu
+source ../gen-tests-makefile.sh
+run_tests --yosys-scripts --bash
diff --git a/tests/verilog/.gitignore b/tests/verilog/.gitignore
index b48f808a1..34da23437 100644
--- a/tests/verilog/.gitignore
+++ b/tests/verilog/.gitignore
@@ -1,3 +1,5 @@
/*.log
/*.out
/run-test.mk
+/const_arst.v
+/const_sr.v
diff --git a/tests/verilog/run-test.sh b/tests/verilog/run-test.sh
index ea56b70f0..2f91cf0fd 100755
--- a/tests/verilog/run-test.sh
+++ b/tests/verilog/run-test.sh
@@ -1,20 +1,4 @@
#!/usr/bin/env bash
-set -e
-{
-echo "all::"
-for x in *.ys; do
- echo "all:: run-$x"
- echo "run-$x:"
- echo " @echo 'Running $x..'"
- echo " @../../yosys -ql ${x%.ys}.log $x"
-done
-for s in *.sh; do
- if [ "$s" != "run-test.sh" ]; then
- echo "all:: run-$s"
- echo "run-$s:"
- echo " @echo 'Running $s..'"
- echo " @bash $s"
- fi
-done
-} > run-test.mk
-exec ${MAKE:-make} -f run-test.mk
+set -eu
+source ../gen-tests-makefile.sh
+run_tests --yosys-scripts --bash