diff options
| author | Eddie Hung <eddie@fpgeh.com> | 2019-10-02 14:52:40 -0700 |
|---|---|---|
| committer | Eddie Hung <eddie@fpgeh.com> | 2019-10-02 14:52:40 -0700 |
| commit | c28d4b804720c2cf0086e921748219150e9631b5 (patch) | |
| tree | 3389b73c06ba6913a2e65c72fae28d405d8c164a /tests/sat | |
| parent | 6028f5df1a7f86e73028c6a0c2b63ab16a1335d6 (diff) | |
| download | yosys-c28d4b804720c2cf0086e921748219150e9631b5.tar.gz yosys-c28d4b804720c2cf0086e921748219150e9631b5.tar.bz2 yosys-c28d4b804720c2cf0086e921748219150e9631b5.zip | |
Add test that is expecting to fail
Diffstat (limited to 'tests/sat')
| -rw-r--r-- | tests/sat/initval.ys | 20 |
1 files changed, 20 insertions, 0 deletions
diff --git a/tests/sat/initval.ys b/tests/sat/initval.ys index 2079d2f34..1627a37e3 100644 --- a/tests/sat/initval.ys +++ b/tests/sat/initval.ys @@ -2,3 +2,23 @@ read_verilog -sv initval.v proc;; sat -seq 10 -prove-asserts + +read_verilog <<EOT +module gold(input clk, input i, output reg [1:0] o); +initial o = 2'b10; +always @(posedge clk) + o[0] <= {i,i}; +endmodule + +module gate(input clk, input i, output reg [1:0] o); +initial o = 2'b10; +always @(posedge clk) + o[0] <= i; +always @* + o[1] <= o[0]; +endmodule +EOT + +proc +miter -equiv -flatten -make_assert -make_outputs gold gate miter +sat -seq 1 -falsify -prove-asserts -show-ports miter |