diff options
| author | Eddie Hung <eddie@fpgeh.com> | 2019-10-02 18:07:38 -0700 |
|---|---|---|
| committer | Eddie Hung <eddie@fpgeh.com> | 2019-10-02 18:07:38 -0700 |
| commit | c6a55d948aebc8993cc3e33372b9c403b0b90554 (patch) | |
| tree | 9806b6ff139a604e8c89ea5b8972a755f15e0fb2 /tests | |
| parent | f6fabc8fda1eb00b0227f1a91d85b837a0609728 (diff) | |
| parent | f46ac1df9f8847dac9d9851f2f948d93a1064ff1 (diff) | |
| download | yosys-c6a55d948aebc8993cc3e33372b9c403b0b90554.tar.gz yosys-c6a55d948aebc8993cc3e33372b9c403b0b90554.tar.bz2 yosys-c6a55d948aebc8993cc3e33372b9c403b0b90554.zip | |
Merge branch 'eddie/fix_sat_init' into eddie/fix1427
Diffstat (limited to 'tests')
| -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 |