diff options
author | Eddie Hung <eddie@fpgeh.com> | 2019-06-21 17:43:29 -0700 |
---|---|---|
committer | Eddie Hung <eddie@fpgeh.com> | 2019-06-21 17:43:29 -0700 |
commit | 1abe93e48d8bb78cd0753d46dfbe1885a1e803eb (patch) | |
tree | ecaa95a9e3b9c87a528a6939a36053012cbea563 /tests/various/signext.ys | |
parent | 0f300e75c07dbcf21ab2d6128ef8af9ca6a98892 (diff) | |
parent | e01bab6c6437f7e3072e10beaec558d3f71c3e9e (diff) | |
download | yosys-1abe93e48d8bb78cd0753d46dfbe1885a1e803eb.tar.gz yosys-1abe93e48d8bb78cd0753d46dfbe1885a1e803eb.tar.bz2 yosys-1abe93e48d8bb78cd0753d46dfbe1885a1e803eb.zip |
Merge remote-tracking branch 'origin/master' into xaig
Diffstat (limited to 'tests/various/signext.ys')
-rw-r--r-- | tests/various/signext.ys | 33 |
1 files changed, 33 insertions, 0 deletions
diff --git a/tests/various/signext.ys b/tests/various/signext.ys new file mode 100644 index 000000000..0c8d671e7 --- /dev/null +++ b/tests/various/signext.ys @@ -0,0 +1,33 @@ + +read_verilog -formal <<EOT +module gate(input clk, output [32:0] o, p, q, r, s, t, u); +assign o = 'bx; +assign p = 1'bx; +assign q = 'bz; +assign r = 1'bz; +assign s = 1'b0; +assign t = 'b1; +assign u = -'sb1; +endmodule +EOT + +proc + +## Equivalence checking + +read_verilog -formal <<EOT +module gold(input clk, output [32:0] o, p, q, r, s, t, u); +assign o = {33{1'bx}}; +assign p = {{32{1'b0}}, 1'bx}; +assign q = {33{1'bz}}; +assign r = {{32{1'b0}}, 1'bz}; +assign s = {33{1'b0}}; +assign t = {{32{1'b0}}, 1'b1}; +assign u = {33{1'b1}}; +endmodule +EOT + +proc + +miter -equiv -flatten -make_assert -make_outputs gold gate miter +sat -verify -prove-asserts -show-ports -enable_undef miter |