diff options
| -rw-r--r-- | .github/workflows/test-linux.yml | 2 | ||||
| -rw-r--r-- | .github/workflows/test-macos.yml | 4 | ||||
| -rw-r--r-- | CHANGELOG | 31 | ||||
| -rw-r--r-- | Makefile | 4 | ||||
| -rw-r--r-- | frontends/ast/genrtlil.cc | 11 | ||||
| -rw-r--r-- | frontends/ast/simplify.cc | 127 | ||||
| -rw-r--r-- | kernel/log.cc | 22 | ||||
| -rw-r--r-- | passes/opt/opt_dff.cc | 2 | ||||
| -rwxr-xr-x | tests/various/logger_fail.sh | 42 | ||||
| -rw-r--r-- | tests/verilog/always_comb_latch_1.ys | 13 | ||||
| -rw-r--r-- | tests/verilog/always_comb_latch_2.ys | 15 | ||||
| -rw-r--r-- | tests/verilog/always_comb_latch_3.ys | 20 | ||||
| -rw-r--r-- | tests/verilog/always_comb_latch_4.ys | 17 | ||||
| -rw-r--r-- | tests/verilog/always_comb_nolatch_1.ys | 16 | ||||
| -rw-r--r-- | tests/verilog/always_comb_nolatch_2.ys | 17 | ||||
| -rw-r--r-- | tests/verilog/always_comb_nolatch_3.ys | 21 | ||||
| -rw-r--r-- | tests/verilog/always_comb_nolatch_4.ys | 16 | ||||
| -rw-r--r-- | tests/verilog/size_cast.sv | 140 | ||||
| -rw-r--r-- | tests/verilog/size_cast.ys | 5 |
19 files changed, 501 insertions, 24 deletions
diff --git a/.github/workflows/test-linux.yml b/.github/workflows/test-linux.yml index ef47d4dca..9aa952e45 100644 --- a/.github/workflows/test-linux.yml +++ b/.github/workflows/test-linux.yml @@ -85,7 +85,7 @@ jobs: - name: Get iverilog shell: bash run: | - git clone git://github.com/steveicarus/iverilog.git + git clone https://github.com/steveicarus/iverilog.git - name: Cache iverilog id: cache-iverilog diff --git a/.github/workflows/test-macos.yml b/.github/workflows/test-macos.yml index 8a7804907..09ab382bf 100644 --- a/.github/workflows/test-macos.yml +++ b/.github/workflows/test-macos.yml @@ -40,7 +40,7 @@ jobs: - name: Get iverilog shell: bash run: | - git clone git://github.com/steveicarus/iverilog.git + git clone https://github.com/steveicarus/iverilog.git - name: Cache iverilog id: cache-iverilog @@ -122,7 +122,7 @@ jobs: - name: Get iverilog shell: bash run: | - git clone git://github.com/steveicarus/iverilog.git + git clone https://github.com/steveicarus/iverilog.git - name: Cache iverilog id: cache-iverilog-homebrew @@ -2,22 +2,43 @@ List of major changes and improvements between releases ======================================================= -Yosys 0.12 .. Yosys 0.12-dev +Yosys 0.13 .. Yosys 0.13-dev -------------------------- -Yosys 0.11 .. Yosys 0.12 +Yosys 0.12 .. Yosys 0.13 -------------------------- * Various - - Added iopadmap native support for negative-polarity output enable - - ABC update + - Use "read" command to parse HDL files from Yosys command-line + - Added "yosys -r <topmodule>" command line option + - write_verilog: dump zero width sigspecs correctly * SystemVerilog - - Support parameters using struct as a wiretype - Fixed regression preventing the use array querying functions in case expressions and case item expressions - Fixed static size casts inadvertently limiting the result width of binary operations + - Fixed static size casts ignoring expression signedness + - Fixed static size casts not extending unbased unsized literals + - Added automatic `nosync` inference for local variables in `always_comb` + procedures which are always assigned before they are used to avoid errant + latch inference + + * New commands and options + - Added "clean_zerowidth" pass + + * Verific support + - Add YOSYS to the implicitly defined verilog macros in verific + +Yosys 0.11 .. Yosys 0.12 +-------------------------- + + * Various + - Added iopadmap native support for negative-polarity output enable + - ABC update + + * SystemVerilog + - Support parameters using struct as a wiretype * New commands and options - Added "-genlib" option to "abc" pass @@ -129,12 +129,12 @@ LDFLAGS += -rdynamic LDLIBS += -lrt endif -YOSYS_VER := 0.12+50 +YOSYS_VER := 0.13+3 GIT_REV := $(shell git -C $(YOSYS_SRC) rev-parse --short HEAD 2> /dev/null || echo UNKNOWN) OBJS = kernel/version_$(GIT_REV).o bumpversion: - sed -i "/^YOSYS_VER := / s/+[0-9][0-9]*$$/+`git log --oneline 2156e20.. | wc -l`/;" Makefile + sed -i "/^YOSYS_VER := / s/+[0-9][0-9]*$$/+`git log --oneline 8b1eafc.. | wc -l`/;" Makefile # set 'ABCREV = default' to use abc/ as it is # diff --git a/frontends/ast/genrtlil.cc b/frontends/ast/genrtlil.cc index 2788a850f..4c25287ad 100644 --- a/frontends/ast/genrtlil.cc +++ b/frontends/ast/genrtlil.cc @@ -1531,13 +1531,20 @@ RTLIL::SigSpec AstNode::genRTLIL(int width_hint, bool sign_hint) // changing the size of signal can be done directly using RTLIL::SigSpec case AST_CAST_SIZE: { RTLIL::SigSpec size = children[0]->genRTLIL(); - RTLIL::SigSpec sig = children[1]->genRTLIL(); if (!size.is_fully_const()) log_file_error(filename, location.first_line, "Static cast with non constant expression!\n"); int width = size.as_int(); if (width <= 0) log_file_error(filename, location.first_line, "Static cast with zero or negative size!\n"); - sig.extend_u0(width, sign_hint); + // determine the *signedness* of the expression + int sub_width_hint = -1; + bool sub_sign_hint = true; + children[1]->detectSignWidth(sub_width_hint, sub_sign_hint); + // generate the signal given the *cast's* size and the + // *expression's* signedness + RTLIL::SigSpec sig = children[1]->genWidthRTLIL(width, sub_sign_hint); + // context may effect this node's signedness, but not that of the + // casted expression is_signed = sign_hint; return sig; } diff --git a/frontends/ast/simplify.cc b/frontends/ast/simplify.cc index cb47e641a..18b1e1e11 100644 --- a/frontends/ast/simplify.cc +++ b/frontends/ast/simplify.cc @@ -673,6 +673,118 @@ void add_wire_for_ref(const RTLIL::Wire *ref, const std::string &str) current_scope[str] = wire; } +enum class IdentUsage { + NotReferenced, // target variable is neither read or written in the block + Assigned, // target variable is always assigned before use + SyncRequired, // target variable may be used before it has been assigned +}; + +// determines whether a local variable a block is always assigned before it is +// used, meaning the nosync attribute can automatically be added to that +// variable +static IdentUsage always_asgn_before_use(const AstNode *node, const std::string &target) +{ + // This variable has been referenced before it has necessarily been assigned + // a value in this procedure. + if (node->type == AST_IDENTIFIER && node->str == target) + return IdentUsage::SyncRequired; + + // For case statements (which are also used for if/else), we check each + // possible branch. If the variable is assigned in all branches, then it is + // assigned, and a sync isn't required. If it used before assignment in any + // branch, then a sync is required. + if (node->type == AST_CASE) { + bool all_defined = true; + bool any_used = false; + bool has_default = false; + for (const AstNode *child : node->children) { + if (child->type == AST_COND && child->children.at(0)->type == AST_DEFAULT) + has_default = true; + IdentUsage nested = always_asgn_before_use(child, target); + if (nested != IdentUsage::Assigned && child->type == AST_COND) + all_defined = false; + if (nested == IdentUsage::SyncRequired) + any_used = true; + } + if (any_used) + return IdentUsage::SyncRequired; + else if (all_defined && has_default) + return IdentUsage::Assigned; + else + return IdentUsage::NotReferenced; + } + + // Check if this is an assignment to the target variable. For simplicity, we + // don't analyze sub-ranges of the variable. + if (node->type == AST_ASSIGN_EQ) { + const AstNode *ident = node->children.at(0); + if (ident->type == AST_IDENTIFIER && ident->str == target) + return IdentUsage::Assigned; + } + + for (const AstNode *child : node->children) { + IdentUsage nested = always_asgn_before_use(child, target); + if (nested != IdentUsage::NotReferenced) + return nested; + } + return IdentUsage::NotReferenced; +} + +static const std::string auto_nosync_prefix = "\\AutoNosync"; + +// mark a local variable in an always_comb block for automatic nosync +// consideration +static void mark_auto_nosync(AstNode *block, const AstNode *wire) +{ + log_assert(block->type == AST_BLOCK); + log_assert(wire->type == AST_WIRE); + block->attributes[auto_nosync_prefix + wire->str] = AstNode::mkconst_int(1, + false); +} + +// check a procedural block for auto-nosync markings, remove them, and add +// nosync to local variables as necessary +static void check_auto_nosync(AstNode *node) +{ + std::vector<RTLIL::IdString> attrs_to_drop; + for (const auto& elem : node->attributes) { + // skip attributes that don't begin with the prefix + if (elem.first.compare(0, auto_nosync_prefix.size(), + auto_nosync_prefix.c_str())) + continue; + + // delete and remove the attribute once we're done iterating + attrs_to_drop.push_back(elem.first); + + // find the wire based on the attribute + std::string wire_name = elem.first.substr(auto_nosync_prefix.size()); + auto it = current_scope.find(wire_name); + if (it == current_scope.end()) + continue; + + // analyze the usage of the local variable in this block + IdentUsage ident_usage = always_asgn_before_use(node, wire_name); + if (ident_usage != IdentUsage::Assigned) + continue; + + // mark the wire with `nosync` + AstNode *wire = it->second; + log_assert(wire->type == AST_WIRE); + wire->attributes[ID::nosync] = AstNode::mkconst_int(1, false); + } + + // remove the attributes we've "consumed" + for (const RTLIL::IdString &str : attrs_to_drop) { + auto it = node->attributes.find(str); + delete it->second; + node->attributes.erase(it); + } + + // check local variables in any nested blocks + for (AstNode *child : node->children) + check_auto_nosync(child); +} + // convert the AST into a simpler AST that has all parameters substituted by their // values, unrolled for-loops, expanded generate blocks, etc. when this function // is done with an AST it can be converted into RTLIL using genRTLIL(). @@ -980,6 +1092,11 @@ bool AstNode::simplify(bool const_fold, bool at_zero, bool in_lvalue, int stage, } } } + + for (AstNode *child : children) + if (child->type == AST_ALWAYS && + child->attributes.count(ID::always_comb)) + check_auto_nosync(child); } // create name resolution entries for all objects with names @@ -2224,6 +2341,16 @@ bool AstNode::simplify(bool const_fold, bool at_zero, bool in_lvalue, int stage, { expand_genblock(str + "."); + // if this is an autonamed block is in an always_comb + if (current_always && current_always->attributes.count(ID::always_comb) + && str.at(0) == '$') + // track local variables in this block so we can consider adding + // nosync once the block has been fully elaborated + for (AstNode *child : children) + if (child->type == AST_WIRE && + !child->attributes.count(ID::nosync)) + mark_auto_nosync(this, child); + std::vector<AstNode*> new_children; for (size_t i = 0; i < children.size(); i++) if (children[i]->type == AST_WIRE || children[i]->type == AST_MEMORY || children[i]->type == AST_PARAMETER || children[i]->type == AST_LOCALPARAM || children[i]->type == AST_TYPEDEF) { diff --git a/kernel/log.cc b/kernel/log.cc index e7ce4cc46..4bcce3b28 100644 --- a/kernel/log.cc +++ b/kernel/log.cc @@ -71,7 +71,6 @@ int string_buf_index = -1; static struct timeval initial_tv = { 0, 0 }; static bool next_print_log = false; static int log_newline_count = 0; -static bool display_error_log_msg = true; static void log_id_cache_clear() { @@ -338,8 +337,7 @@ static void logv_error_with_prefix(const char *prefix, f = stderr; log_last_error = vstringf(format, ap); - if (display_error_log_msg) - log("%s%s", prefix, log_last_error.c_str()); + log("%s%s", prefix, log_last_error.c_str()); log_flush(); log_make_debug = bak_log_make_debug; @@ -665,7 +663,14 @@ void log_wire(RTLIL::Wire *wire, std::string indent) void log_check_expected() { - for (auto &item : log_expect_warning) { + // copy out all of the expected logs so that they cannot be re-checked + // or match against themselves + dict<std::string, LogExpectedItem> expect_log, expect_warning, expect_error; + std::swap(expect_warning, log_expect_warning); + std::swap(expect_log, log_expect_log); + std::swap(expect_error, log_expect_error); + + for (auto &item : expect_warning) { if (item.second.current_count == 0) { log_warn_regexes.clear(); log_error("Expected warning pattern '%s' not found !\n", item.first.c_str()); @@ -677,7 +682,7 @@ void log_check_expected() } } - for (auto &item : log_expect_log) { + for (auto &item : expect_log) { if (item.second.current_count == 0) { log_warn_regexes.clear(); log_error("Expected log pattern '%s' not found !\n", item.first.c_str()); @@ -689,7 +694,7 @@ void log_check_expected() } } - for (auto &item : log_expect_error) + for (auto &item : expect_error) if (item.second.current_count == item.second.expected_count) { log_warn_regexes.clear(); log("Expected error pattern '%s' found !!!\n", item.first.c_str()); @@ -701,14 +706,9 @@ void log_check_expected() _Exit(0); #endif } else { - display_error_log_msg = false; log_warn_regexes.clear(); log_error("Expected error pattern '%s' not found !\n", item.first.c_str()); } - - log_expect_warning.clear(); - log_expect_log.clear(); - log_expect_error.clear(); } // --------------------------------------------------- diff --git a/passes/opt/opt_dff.cc b/passes/opt/opt_dff.cc index 38faba15a..98b66dee3 100644 --- a/passes/opt/opt_dff.cc +++ b/passes/opt/opt_dff.cc @@ -557,7 +557,7 @@ struct OptDffWorker // The D input path is effectively useless, so remove it (this will be a const-input D latch, SR latch, or a const driver). log("Handling D = Q on %s (%s) from module %s (removing D path).\n", log_id(cell), log_id(cell->type), log_id(module)); - ff.has_clk = ff.has_ce = ff.has_clk = false; + ff.has_clk = ff.has_ce = false; changed = true; } } diff --git a/tests/various/logger_fail.sh b/tests/various/logger_fail.sh new file mode 100755 index 000000000..19b650007 --- /dev/null +++ b/tests/various/logger_fail.sh @@ -0,0 +1,42 @@ +#!/bin/bash + +fail() { + echo "$1" >&2 + exit 1 +} + +runTest() { + desc="$1" + want="$2" + shift 2 + echo "running '$desc' with args $@" + output=`../../yosys -q "$@" 2>&1` + if [ $? -ne 1 ]; then + fail "exit code for '$desc' was not 1" + fi + if [ "$output" != "$want" ]; then + fail "output for '$desc' did not match" + fi +} + +unmet() { + kind=$1 + runTest "unmet $kind" \ + "ERROR: Expected $kind pattern 'foobar' not found !" \ + -p "logger -expect $kind \"foobar\" 1" +} + +unmet log +unmet warning +unmet error + +runTest "too many logs" \ + "ERROR: Expected log pattern 'statistics' found 2 time(s), instead of 1 time(s) !" \ + -p "logger -expect log \"statistics\" 1" -p stat -p stat + +runTest "too many warnings" \ + "Warning: Found log message matching -W regex: +Printing statistics. +ERROR: Expected warning pattern 'statistics' found 2 time(s), instead of 1 time(s) !" \ + -p "logger -warn \"Printing statistics\"" \ + -p "logger -expect warning \"statistics\" 1" -p stat -p stat diff --git a/tests/verilog/always_comb_latch_1.ys b/tests/verilog/always_comb_latch_1.ys new file mode 100644 index 000000000..c98c79fa2 --- /dev/null +++ b/tests/verilog/always_comb_latch_1.ys @@ -0,0 +1,13 @@ +read_verilog -sv <<EOF +module top; +logic x; +always_comb begin + logic y; + if (x) + y = 1; + x = y; +end +endmodule +EOF +logger -expect error "^Latch inferred for signal `\\top\.\$unnamed_block\$1\.y' from always_comb process" 1 +proc diff --git a/tests/verilog/always_comb_latch_2.ys b/tests/verilog/always_comb_latch_2.ys new file mode 100644 index 000000000..567205a53 --- /dev/null +++ b/tests/verilog/always_comb_latch_2.ys @@ -0,0 +1,15 @@ +read_verilog -sv <<EOF +module top; +logic x; +always_comb begin + logic y; + if (x) + x = 1; + else + y = 1; + x = y; +end +endmodule +EOF +logger -expect error "^Latch inferred for signal `\\top\.\$unnamed_block\$1\.y' from always_comb process" 1 +proc diff --git a/tests/verilog/always_comb_latch_3.ys b/tests/verilog/always_comb_latch_3.ys new file mode 100644 index 000000000..b9b028ac7 --- /dev/null +++ b/tests/verilog/always_comb_latch_3.ys @@ -0,0 +1,20 @@ +read_verilog -sv <<EOF +module top; +logic x; +logic z; +assign z = 1'b1; +always_comb begin + logic y; + case (x) + 1'b0: + y = 1; + endcase + if (z) + x = y; + else + x = 1'b0; +end +endmodule +EOF +logger -expect error "^Latch inferred for signal `\\top\.\$unnamed_block\$1\.y' from always_comb process" 1 +proc diff --git a/tests/verilog/always_comb_latch_4.ys b/tests/verilog/always_comb_latch_4.ys new file mode 100644 index 000000000..46b78801b --- /dev/null +++ b/tests/verilog/always_comb_latch_4.ys @@ -0,0 +1,17 @@ +read_verilog -sv <<EOF +module top; +parameter AVOID_LATCH = 0; +logic x, z; +assign z = 1'b1; +always_comb begin + logic y; + if (z) + y = 0; + for (int i = 1; i == AVOID_LATCH; i++) + y = 1; + x = z ? y : 1'b0; +end +endmodule +EOF +logger -expect error "^Latch inferred for signal `\\top\.\$unnamed_block\$3\.y' from always_comb process" 1 +proc diff --git a/tests/verilog/always_comb_nolatch_1.ys b/tests/verilog/always_comb_nolatch_1.ys new file mode 100644 index 000000000..4d1952b52 --- /dev/null +++ b/tests/verilog/always_comb_nolatch_1.ys @@ -0,0 +1,16 @@ +read_verilog -sv <<EOF +module top; +logic [4:0] x; +logic z; +assign z = 1'b1; +always_comb begin + x = '0; + if (z) begin + for (int i = 0; i < 5; i++) begin + x[i] = 1'b1; + end + end +end +endmodule +EOF +proc diff --git a/tests/verilog/always_comb_nolatch_2.ys b/tests/verilog/always_comb_nolatch_2.ys new file mode 100644 index 000000000..2ec6ca0f4 --- /dev/null +++ b/tests/verilog/always_comb_nolatch_2.ys @@ -0,0 +1,17 @@ +read_verilog -sv <<EOF +module top; +logic [4:0] x; +logic z; +assign z = 1'b1; +always_comb begin + x = '0; + if (z) begin + int i; + for (i = 0; i < 5; i++) begin + x[i] = 1'b1; + end + end +end +endmodule +EOF +proc diff --git a/tests/verilog/always_comb_nolatch_3.ys b/tests/verilog/always_comb_nolatch_3.ys new file mode 100644 index 000000000..33f9833a2 --- /dev/null +++ b/tests/verilog/always_comb_nolatch_3.ys @@ -0,0 +1,21 @@ +read_verilog -sv <<EOF +module top; +logic x; +logic z; +assign z = 1'b1; +always_comb begin + logic y; + case (x) + 1'b0: + y = 1; + default: + y = 0; + endcase + if (z) + x = y; + else + x = 1'b0; +end +endmodule +EOF +proc diff --git a/tests/verilog/always_comb_nolatch_4.ys b/tests/verilog/always_comb_nolatch_4.ys new file mode 100644 index 000000000..bc29b2771 --- /dev/null +++ b/tests/verilog/always_comb_nolatch_4.ys @@ -0,0 +1,16 @@ +read_verilog -sv <<EOF +module top; +parameter AVOID_LATCH = 1; +logic x, z; +assign z = 1'b1; +always_comb begin + logic y; + if (z) + y = 0; + for (int i = 1; i == AVOID_LATCH; i++) + y = 1; + x = z ? y : 1'b0; +end +endmodule +EOF +proc diff --git a/tests/verilog/size_cast.sv b/tests/verilog/size_cast.sv new file mode 100644 index 000000000..1636f8d70 --- /dev/null +++ b/tests/verilog/size_cast.sv @@ -0,0 +1,140 @@ +module top; + logic L1b0 = 0; + logic L1b1 = 1; + + logic signed L1sb0 = 0; + logic signed L1sb1 = 1; + + logic [1:0] L2b00 = 0; + logic [1:0] L2b01 = 1; + logic [1:0] L2b10 = 2; + logic [1:0] L2b11 = 3; + + logic signed [1:0] L2sb00 = 0; + logic signed [1:0] L2sb01 = 1; + logic signed [1:0] L2sb10 = 2; + logic signed [1:0] L2sb11 = 3; + + logic y = 1; + + always @* begin + + assert (1'(L1b0 ) == 1'b0); + assert (1'(L1b1 ) == 1'b1); + assert (1'(L1sb0 ) == 1'b0); + assert (1'(L1sb1 ) == 1'b1); + assert (1'(L2b00 ) == 1'b0); + assert (1'(L2b01 ) == 1'b1); + assert (1'(L2b10 ) == 1'b0); + assert (1'(L2b11 ) == 1'b1); + assert (1'(L2sb00) == 1'b0); + assert (1'(L2sb01) == 1'b1); + assert (1'(L2sb10) == 1'b0); + assert (1'(L2sb11) == 1'b1); + + assert (2'(L1b0 ) == 2'b00); + assert (2'(L1b1 ) == 2'b01); + assert (2'(L1sb0 ) == 2'b00); + assert (2'(L1sb1 ) == 2'b11); + assert (2'(L2b00 ) == 2'b00); + assert (2'(L2b01 ) == 2'b01); + assert (2'(L2b10 ) == 2'b10); + assert (2'(L2b11 ) == 2'b11); + assert (2'(L2sb00) == 2'b00); + assert (2'(L2sb01) == 2'b01); + assert (2'(L2sb10) == 2'b10); + assert (2'(L2sb11) == 2'b11); + + assert (3'(L1b0 ) == 3'b000); + assert (3'(L1b1 ) == 3'b001); + assert (3'(L1sb0 ) == 3'b000); + assert (3'(L1sb1 ) == 3'b111); + assert (3'(L2b00 ) == 3'b000); + assert (3'(L2b01 ) == 3'b001); + assert (3'(L2b10 ) == 3'b010); + assert (3'(L2b11 ) == 3'b011); + assert (3'(L2sb00) == 3'b000); + assert (3'(L2sb01) == 3'b001); + assert (3'(L2sb10) == 3'b110); + assert (3'(L2sb11) == 3'b111); + + assert (3'(L1b0 | '1) == 3'b111); + assert (3'(L1b1 | '1) == 3'b111); + assert (3'(L1sb0 | '1) == 3'b111); + assert (3'(L1sb1 | '1) == 3'b111); + assert (3'(L2b00 | '1) == 3'b111); + assert (3'(L2b01 | '1) == 3'b111); + assert (3'(L2b10 | '1) == 3'b111); + assert (3'(L2b11 | '1) == 3'b111); + assert (3'(L2sb00 | '1) == 3'b111); + assert (3'(L2sb01 | '1) == 3'b111); + assert (3'(L2sb10 | '1) == 3'b111); + assert (3'(L2sb11 | '1) == 3'b111); + + assert (3'(L1b0 | '0) == 3'b000); + assert (3'(L1b1 | '0) == 3'b001); + assert (3'(L1sb0 | '0) == 3'b000); + assert (3'(L1sb1 | '0) == 3'b001); + assert (3'(L2b00 | '0) == 3'b000); + assert (3'(L2b01 | '0) == 3'b001); + assert (3'(L2b10 | '0) == 3'b010); + assert (3'(L2b11 | '0) == 3'b011); + assert (3'(L2sb00 | '0) == 3'b000); + assert (3'(L2sb01 | '0) == 3'b001); + assert (3'(L2sb10 | '0) == 3'b010); + assert (3'(L2sb11 | '0) == 3'b011); + + assert (3'(y ? L1b0 : '1) == 3'b000); + assert (3'(y ? L1b1 : '1) == 3'b001); + assert (3'(y ? L1sb0 : '1) == 3'b000); + assert (3'(y ? L1sb1 : '1) == 3'b001); + assert (3'(y ? L2b00 : '1) == 3'b000); + assert (3'(y ? L2b01 : '1) == 3'b001); + assert (3'(y ? L2b10 : '1) == 3'b010); + assert (3'(y ? L2b11 : '1) == 3'b011); + assert (3'(y ? L2sb00 : '1) == 3'b000); + assert (3'(y ? L2sb01 : '1) == 3'b001); + assert (3'(y ? L2sb10 : '1) == 3'b010); + assert (3'(y ? L2sb11 : '1) == 3'b011); + + assert (3'(y ? L1b0 : '0) == 3'b000); + assert (3'(y ? L1b1 : '0) == 3'b001); + assert (3'(y ? L1sb0 : '0) == 3'b000); + assert (3'(y ? L1sb1 : '0) == 3'b001); + assert (3'(y ? L2b00 : '0) == 3'b000); + assert (3'(y ? L2b01 : '0) == 3'b001); + assert (3'(y ? L2b10 : '0) == 3'b010); + assert (3'(y ? L2b11 : '0) == 3'b011); + assert (3'(y ? L2sb00 : '0) == 3'b000); + assert (3'(y ? L2sb01 : '0) == 3'b001); + assert (3'(y ? L2sb10 : '0) == 3'b010); + assert (3'(y ? L2sb11 : '0) == 3'b011); + + assert (3'(y ? L1b0 : 1'sb0) == 3'b000); + assert (3'(y ? L1b1 : 1'sb0) == 3'b001); + assert (3'(y ? L1sb0 : 1'sb0) == 3'b000); + assert (3'(y ? L1sb1 : 1'sb0) == 3'b111); + assert (3'(y ? L2b00 : 1'sb0) == 3'b000); + assert (3'(y ? L2b01 : 1'sb0) == 3'b001); + assert (3'(y ? L2b10 : 1'sb0) == 3'b010); + assert (3'(y ? L2b11 : 1'sb0) == 3'b011); + assert (3'(y ? L2sb00 : 1'sb0) == 3'b000); + assert (3'(y ? L2sb01 : 1'sb0) == 3'b001); + assert (3'(y ? L2sb10 : 1'sb0) == 3'b110); + assert (3'(y ? L2sb11 : 1'sb0) == 3'b111); + + assert (3'(y ? L1b0 : 1'sb1) == 3'b000); + assert (3'(y ? L1b1 : 1'sb1) == 3'b001); + assert (3'(y ? L1sb0 : 1'sb1) == 3'b000); + assert (3'(y ? L1sb1 : 1'sb1) == 3'b111); + assert (3'(y ? L2b00 : 1'sb1) == 3'b000); + assert (3'(y ? L2b01 : 1'sb1) == 3'b001); + assert (3'(y ? L2b10 : 1'sb1) == 3'b010); + assert (3'(y ? L2b11 : 1'sb1) == 3'b011); + assert (3'(y ? L2sb00 : 1'sb1) == 3'b000); + assert (3'(y ? L2sb01 : 1'sb1) == 3'b001); + assert (3'(y ? L2sb10 : 1'sb1) == 3'b110); + assert (3'(y ? L2sb11 : 1'sb1) == 3'b111); + + end +endmodule diff --git a/tests/verilog/size_cast.ys b/tests/verilog/size_cast.ys new file mode 100644 index 000000000..6890cd2d5 --- /dev/null +++ b/tests/verilog/size_cast.ys @@ -0,0 +1,5 @@ +read_verilog -sv size_cast.sv +proc +opt -full +select -module top +sat -verify -prove-asserts -show-all |