aboutsummaryrefslogtreecommitdiffstats
path: root/tests
diff options
context:
space:
mode:
authorEddie Hung <eddie@fpgeh.com>2019-06-20 10:10:43 -0700
committerEddie Hung <eddie@fpgeh.com>2019-06-20 10:13:52 -0700
commitb98276fa61be7a1c589d6dac661d31982cfab16b (patch)
treee127e7cd7d007372c223c4b26c159de716393574 /tests
parent0221f3e1c5b427678c5679027ee47ec7c0b8321d (diff)
downloadyosys-b98276fa61be7a1c589d6dac661d31982cfab16b.tar.gz
yosys-b98276fa61be7a1c589d6dac661d31982cfab16b.tar.bz2
yosys-b98276fa61be7a1c589d6dac661d31982cfab16b.zip
Add test
Diffstat (limited to 'tests')
-rw-r--r--tests/various/signext.ys24
1 files changed, 24 insertions, 0 deletions
diff --git a/tests/various/signext.ys b/tests/various/signext.ys
new file mode 100644
index 000000000..26dab13a6
--- /dev/null
+++ b/tests/various/signext.ys
@@ -0,0 +1,24 @@
+
+read_verilog -formal <<EOT
+module gate(input clk, output [1:0] o);
+assign o = 1'bx;
+endmodule
+EOT
+
+
+## Example usage for "pmuxtree" and "muxcover"
+
+proc
+
+## Equivalence checking
+
+read_verilog -formal <<EOT
+module gold(input clk, output [1:0] o);
+assign o = 2'bxx;
+endmodule
+EOT
+
+proc
+
+miter -equiv -flatten -make_assert -make_outputs gold gate miter
+sat -verify -prove-asserts -show-ports -enable_undef miter