diff options
| author | Eddie Hung <eddie@fpgeh.com> | 2019-12-20 13:56:13 -0800 |
|---|---|---|
| committer | Eddie Hung <eddie@fpgeh.com> | 2019-12-20 13:56:13 -0800 |
| commit | 1ea1e8e54f33e4a048c1343959e20e8f1c8ad73b (patch) | |
| tree | a5ac3ee416f3c74c7e842a88c691a61588c49c01 /tests/various | |
| parent | 45f0f1486bbe30cdbf22c94b165879568af1a37a (diff) | |
| parent | 7928eb113c5a310924f4bb8ab26d0dafe902d6ec (diff) | |
| download | yosys-1ea1e8e54f33e4a048c1343959e20e8f1c8ad73b.tar.gz yosys-1ea1e8e54f33e4a048c1343959e20e8f1c8ad73b.tar.bz2 yosys-1ea1e8e54f33e4a048c1343959e20e8f1c8ad73b.zip | |
Merge remote-tracking branch 'origin/master' into xaig_dff
Diffstat (limited to 'tests/various')
| -rw-r--r-- | tests/various/bug1531.ys | 34 |
1 files changed, 34 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 |