summaryrefslogtreecommitdiff
path: root/examples/smtbmc/demo6.v
diff options
context:
space:
mode:
Diffstat (limited to 'examples/smtbmc/demo6.v')
-rw-r--r--examples/smtbmc/demo6.v14
1 files changed, 14 insertions, 0 deletions
diff --git a/examples/smtbmc/demo6.v b/examples/smtbmc/demo6.v
new file mode 100644
index 00000000..62a72e2a
--- /dev/null
+++ b/examples/smtbmc/demo6.v
@@ -0,0 +1,14 @@
+// Demo for assertpmux
+
+module demo6 (input A, B, C, D, E, output reg Y);
+ always @* begin
+ Y = 0;
+ if (A != B) begin
+ (* parallel_case *)
+ case (C)
+ A: Y = D;
+ B: Y = E;
+ endcase
+ end
+ end
+endmodule