diff options
author | N. Engelhardt <nak@symbioticeda.com> | 2020-01-03 12:28:48 +0100 |
---|---|---|
committer | N. Engelhardt <nak@symbioticeda.com> | 2020-01-03 12:28:48 +0100 |
commit | 341fd872b59e8f95aa14afd9f17225d2c03a4283 (patch) | |
tree | 21802e73ca767d124971d43d3f78d9f4cf7d62e2 /tests/various | |
parent | c8bc1793a4e8230c29fca4a34862414e8ab8722b (diff) | |
parent | f8d5920a7e61f78873b7bf49dd7e8f3a83f7adf3 (diff) | |
download | yosys-341fd872b59e8f95aa14afd9f17225d2c03a4283.tar.gz yosys-341fd872b59e8f95aa14afd9f17225d2c03a4283.tar.bz2 yosys-341fd872b59e8f95aa14afd9f17225d2c03a4283.zip |
Merge branch 'master' of https://github.com/YosysHQ/yosys into abc_scratchpad_script
Diffstat (limited to 'tests/various')
-rw-r--r-- | tests/various/bug1531.ys | 34 | ||||
-rw-r--r-- | tests/various/scratchpad.ys | 5 |
2 files changed, 39 insertions, 0 deletions
diff --git a/tests/various/bug1531.ys b/tests/various/bug1531.ys new file mode 100644 index 000000000..542223030 --- /dev/null +++ b/tests/various/bug1531.ys @@ -0,0 +1,34 @@ +read_verilog <<EOT +module top (y, clk, w); + output reg y = 1'b0; + input clk, w; + reg [1:0] i = 2'b00; + always @(posedge clk) + // If the constant below is set to 2'b00, the correct output is generated. + // vvvv + for (i = 1'b0; i < 2'b01; i = i + 2'b01) + y <= w || i[1:1]; +endmodule +EOT + +synth +design -stash gate + +read_verilog <<EOT +module gold (y, clk, w); + input clk; + wire [1:0] i; + input w; + output y; + reg y = 1'h0; + always @(posedge clk) + y <= w; + assign i = 2'h0; +endmodule +EOT +proc gold + +design -import gate -as gate + +miter -equiv -flatten -make_assert -make_outputs gold gate miter +sat -seq 10 -verify -prove-asserts -show-ports miter diff --git a/tests/various/scratchpad.ys b/tests/various/scratchpad.ys new file mode 100644 index 000000000..dc94081ea --- /dev/null +++ b/tests/various/scratchpad.ys @@ -0,0 +1,5 @@ +scratchpad -set foo "bar baz" +scratchpad -copy foo oof +scratchpad -unset foo +scratchpad -assert oof "bar baz" +scratchpad -assert-unset foo |