aboutsummaryrefslogtreecommitdiffstats
path: root/tests/sat/initval.ys
diff options
context:
space:
mode:
Diffstat (limited to 'tests/sat/initval.ys')
-rw-r--r--tests/sat/initval.ys11
1 files changed, 11 insertions, 0 deletions
diff --git a/tests/sat/initval.ys b/tests/sat/initval.ys
index 2079d2f34..1436724b0 100644
--- a/tests/sat/initval.ys
+++ b/tests/sat/initval.ys
@@ -2,3 +2,14 @@ read_verilog -sv initval.v
proc;;
sat -seq 10 -prove-asserts
+
+design -reset
+read_verilog -icells <<EOT
+module top(input clk, i, output [1:0] o);
+(* init = 2'bx0 *)
+wire [1:0] o;
+assign o[1] = o[0];
+$_DFF_P_ dff (.C(clk), .D(i), .Q(o[0]));
+endmodule
+EOT
+sat -seq 1