From 2d771a352ef87b69275ef2ba832e58236b5248bf Mon Sep 17 00:00:00 2001
From: Akash Levy <akashlevy@gmail.com>
Date: Mon, 23 Sep 2024 04:05:08 -0700
Subject: [PATCH] Clean up Verific tests

---
 tests/verific/README.md                       |  18 ++
 .../{bounds.ys.fail => bounds.ys.skip}        |   0
 tests/verific/case.gate.v                     | 115 +++++++++
 tests/verific/case.gold.v                     |  56 +++++
 tests/verific/{case.ys => case.ys.fail}       |   0
 ..._semantics.ys => memory_semantics.ys.skip} |   2 +-
 tests/verific/miter.flatten.v                 | 238 ++++++++++++++++++
 tests/verific/miter.v                         | 140 +++++++++++
 tests/verific/range_case.ys                   |  16 --
 .../{rom_case.ys.fail => rom_case.ys.skip}    |   0
 10 files changed, 568 insertions(+), 17 deletions(-)
 create mode 100644 tests/verific/README.md
 rename tests/verific/{bounds.ys.fail => bounds.ys.skip} (100%)
 create mode 100644 tests/verific/case.gate.v
 create mode 100644 tests/verific/case.gold.v
 rename tests/verific/{case.ys => case.ys.fail} (100%)
 rename tests/verific/{memory_semantics.ys => memory_semantics.ys.skip} (99%)
 create mode 100644 tests/verific/miter.flatten.v
 create mode 100644 tests/verific/miter.v
 delete mode 100644 tests/verific/range_case.ys
 rename tests/verific/{rom_case.ys.fail => rom_case.ys.skip} (100%)

diff --git a/tests/verific/README.md b/tests/verific/README.md
new file mode 100644
index 000000000..a3424eea8
--- /dev/null
+++ b/tests/verific/README.md
@@ -0,0 +1,18 @@
+# Verific Test Cases
+
+## Yosys Built-In
+
+### Working
+
+- `clocking`
+- `enum`
+
+### Skipped
+
+- `bounds`: checks top and bottom bound attributes, which are removed to avoid OpenSTA issues
+- `memory_semantics`: relies on initial values being retained, which is disabled
+- `rom_case`: relies on using Verific's frontend rather than GHDL, which is what we are using
+
+### Failing
+
+- `case`: checks that miter works with abstract case synthesis, but runs into issues with function
diff --git a/tests/verific/bounds.ys.fail b/tests/verific/bounds.ys.skip
similarity index 100%
rename from tests/verific/bounds.ys.fail
rename to tests/verific/bounds.ys.skip
diff --git a/tests/verific/case.gate.v b/tests/verific/case.gate.v
new file mode 100644
index 000000000..e9c783837
--- /dev/null
+++ b/tests/verific/case.gate.v
@@ -0,0 +1,115 @@
+/* Generated by Preqorsor 0.45+139 (git sha1 2c3d2b3ec, c++ 15.0.0 -fPIC -O3) */
+
+(* \library  = "work" *)
+(* hdlname = "top" *)
+(* src = "case.sv:1.8-1.11" *)
+module gate(clk, o, currentstate);
+  wire _00_;
+  wire _01_;
+  wire _02_;
+  wire _03_;
+  wire _04_;
+  wire _05_;
+  wire _06_;
+  wire _07_;
+  wire _08_;
+  wire _09_;
+  wire _10_;
+  (* src = "case.sv:2.8-2.11" *)
+  input clk;
+  wire clk;
+  (* src = "case.sv:3.14-3.26" *)
+  input [5:0] currentstate;
+  wire [5:0] currentstate;
+  (* src = "case.sv:4.19-4.20" *)
+  output [1:0] o;
+  reg [1:0] o;
+  assign _02_ = | { _07_, _06_, _05_ };
+  assign _03_ = | { _04_, _10_, _09_ };
+  (* src = "case.sv:6.9-26.5" *)
+  always @(posedge clk)
+    o[1] <= _00_;
+  (* src = "case.sv:6.9-26.5" *)
+  always @(posedge clk)
+    o[0] <= _01_;
+  assign _04_ = currentstate == (* full_case = 32'd1 *) 3'h7;
+  function [1:0] _16_;
+    input [1:0] a;
+    input [5:0] b;
+    input [2:0] s;
+    (* full_case = 32'd1 *)
+    (* parallel_case *)
+    casez (s)
+      3'b??1:
+        _16_ = b[1:0];
+      3'b?1?:
+        _16_ = b[3:2];
+      3'b1??:
+        _16_ = b[5:4];
+      default:
+        _16_ = a;
+    endcase
+  endfunction
+  assign { _00_, _01_ } = _16_(2'h0, 6'h39, { _03_, _08_, _02_ });
+  assign _05_ = currentstate == (* full_case = 32'd1 *) 1'h1;
+  assign _06_ = currentstate == (* full_case = 32'd1 *) 2'h2;
+  assign _07_ = currentstate == (* full_case = 32'd1 *) 2'h3;
+  assign _08_ = currentstate == (* full_case = 32'd1 *) 3'h4;
+  assign _09_ = currentstate == (* full_case = 32'd1 *) 3'h5;
+  assign _10_ = currentstate == (* full_case = 32'd1 *) 3'h6;
+endmodule
+
+(* \library  = "work" *)
+(* hdlname = "top" *)
+(* src = "case.sv:1.8-1.11" *)
+module gold(clk, o, currentstate);
+  wire _00_;
+  wire _01_;
+  wire _02_;
+  wire _03_;
+  wire [1:0] _04_;
+  wire _05_;
+  wire _06_;
+  wire _07_;
+  wire _08_;
+  wire _09_;
+  (* src = "case.sv:2.8-2.11" *)
+  input clk;
+  wire clk;
+  (* src = "case.sv:3.14-3.26" *)
+  input [5:0] currentstate;
+  wire [5:0] currentstate;
+  (* src = "case.sv:4.19-4.20" *)
+  output [1:0] o;
+  reg [1:0] o;
+  assign _01_ = currentstate == (* src = "case.sv:17.4-17.8" *) 3'h7;
+  assign _05_ = currentstate == (* src = "case.sv:9.4-9.8" *) 1'h1;
+  assign _06_ = currentstate == (* src = "case.sv:9.4-9.8" *) 2'h2;
+  assign _07_ = currentstate == (* src = "case.sv:9.4-9.8" *) 2'h3;
+  assign _08_ = currentstate == (* src = "case.sv:13.4-13.8" *) 3'h4;
+  assign _09_ = currentstate == (* src = "case.sv:17.4-17.8" *) 3'h5;
+  assign _00_ = currentstate == (* src = "case.sv:17.4-17.8" *) 3'h6;
+  (* src = "case.sv:6.9-26.5" *)
+  always @(posedge clk)
+    o <= _04_;
+  assign _02_ = | (* src = "case.sv:8.3-25.10" *) { _07_, _06_, _05_ };
+  assign _03_ = | (* src = "case.sv:8.3-25.10" *) { _01_, _00_, _09_ };
+  function [1:0] _20_;
+    input [1:0] a;
+    input [5:0] b;
+    input [2:0] s;
+    (* src = "case.sv:8.3-25.10" *)
+    (* parallel_case *)
+    casez (s)
+      3'b??1:
+        _20_ = b[1:0];
+      3'b?1?:
+        _20_ = b[3:2];
+      3'b1??:
+        _20_ = b[5:4];
+      default:
+        _20_ = a;
+    endcase
+  endfunction
+  assign _04_ = _20_(2'h0, 6'h1b, { _02_, _08_, _03_ });
+endmodule
diff --git a/tests/verific/case.gold.v b/tests/verific/case.gold.v
new file mode 100644
index 000000000..e60f003e0
--- /dev/null
+++ b/tests/verific/case.gold.v
@@ -0,0 +1,56 @@
+/* Generated by Preqorsor 0.45+139 (git sha1 2c3d2b3ec, c++ 15.0.0 -fPIC -O3) */
+
+(* \library  = "work" *)
+(* hdlname = "top" *)
+(* src = "case.sv:1.8-1.11" *)
+module gold(clk, o, currentstate);
+  wire _00_;
+  wire _01_;
+  wire _02_;
+  wire _03_;
+  wire [1:0] _04_;
+  wire _05_;
+  wire _06_;
+  wire _07_;
+  wire _08_;
+  wire _09_;
+  (* src = "case.sv:2.8-2.11" *)
+  input clk;
+  wire clk;
+  (* src = "case.sv:3.14-3.26" *)
+  input [5:0] currentstate;
+  wire [5:0] currentstate;
+  (* src = "case.sv:4.19-4.20" *)
+  output [1:0] o;
+  reg [1:0] o;
+  assign _01_ = currentstate == (* src = "case.sv:17.4-17.8" *) 3'h7;
+  assign _05_ = currentstate == (* src = "case.sv:9.4-9.8" *) 1'h1;
+  assign _06_ = currentstate == (* src = "case.sv:9.4-9.8" *) 2'h2;
+  assign _07_ = currentstate == (* src = "case.sv:9.4-9.8" *) 2'h3;
+  assign _08_ = currentstate == (* src = "case.sv:13.4-13.8" *) 3'h4;
+  assign _09_ = currentstate == (* src = "case.sv:17.4-17.8" *) 3'h5;
+  assign _00_ = currentstate == (* src = "case.sv:17.4-17.8" *) 3'h6;
+  (* src = "case.sv:6.9-26.5" *)
+  always @(posedge clk)
+    o <= _04_;
+  assign _02_ = | (* src = "case.sv:8.3-25.10" *) { _07_, _06_, _05_ };
+  assign _03_ = | (* src = "case.sv:8.3-25.10" *) { _01_, _00_, _09_ };
+  function [1:0] _20_;
+    input [1:0] a;
+    input [5:0] b;
+    input [2:0] s;
+    (* src = "case.sv:8.3-25.10" *)
+    (* parallel_case *)
+    casez (s)
+      3'b??1:
+        _20_ = b[1:0];
+      3'b?1?:
+        _20_ = b[3:2];
+      3'b1??:
+        _20_ = b[5:4];
+      default:
+        _20_ = a;
+    endcase
+  endfunction
+  assign _04_ = _20_(2'h0, 6'h1b, { _02_, _08_, _03_ });
+endmodule
diff --git a/tests/verific/case.ys b/tests/verific/case.ys.fail
similarity index 100%
rename from tests/verific/case.ys
rename to tests/verific/case.ys.fail
diff --git a/tests/verific/memory_semantics.ys b/tests/verific/memory_semantics.ys.skip
similarity index 99%
rename from tests/verific/memory_semantics.ys
rename to tests/verific/memory_semantics.ys.skip
index 9e61ba841..b21ec7c59 100644
--- a/tests/verific/memory_semantics.ys
+++ b/tests/verific/memory_semantics.ys.skip
@@ -1,4 +1,4 @@
-import -sv <<EOF
+import -formal <<EOF
 
 module top(clk);
 input wire clk;
diff --git a/tests/verific/miter.flatten.v b/tests/verific/miter.flatten.v
new file mode 100644
index 000000000..e65f9d4eb
--- /dev/null
+++ b/tests/verific/miter.flatten.v
@@ -0,0 +1,238 @@
+/* Generated by Preqorsor 0.45+139 (git sha1 2c3d2b3ec, c++ 15.0.0 -fPIC -O3) */
+
+(* \library  = "work" *)
+(* hdlname = "top" *)
+(* src = "case.sv:1.8-1.11" *)
+module gate(clk, o, currentstate);
+  wire _00_;
+  wire _01_;
+  wire _02_;
+  wire _03_;
+  wire _04_;
+  wire _05_;
+  wire _06_;
+  wire _07_;
+  wire _08_;
+  wire _09_;
+  wire _10_;
+  (* src = "case.sv:2.8-2.11" *)
+  input clk;
+  wire clk;
+  (* src = "case.sv:3.14-3.26" *)
+  input [5:0] currentstate;
+  wire [5:0] currentstate;
+  (* src = "case.sv:4.19-4.20" *)
+  output [1:0] o;
+  reg [1:0] o;
+  assign _02_ = | { _07_, _06_, _05_ };
+  assign _03_ = | { _04_, _10_, _09_ };
+  (* src = "case.sv:6.9-26.5" *)
+  always @(posedge clk)
+    o[1] <= _00_;
+  (* src = "case.sv:6.9-26.5" *)
+  always @(posedge clk)
+    o[0] <= _01_;
+  assign _04_ = currentstate == (* full_case = 32'd1 *) 3'h7;
+  function [1:0] _16_;
+    input [1:0] a;
+    input [5:0] b;
+    input [2:0] s;
+    (* full_case = 32'd1 *)
+    (* parallel_case *)
+    casez (s)
+      3'b??1:
+        _16_ = b[1:0];
+      3'b?1?:
+        _16_ = b[3:2];
+      3'b1??:
+        _16_ = b[5:4];
+      default:
+        _16_ = a;
+    endcase
+  endfunction
+  assign { _00_, _01_ } = _16_(2'h0, 6'h39, { _03_, _08_, _02_ });
+  assign _05_ = currentstate == (* full_case = 32'd1 *) 1'h1;
+  assign _06_ = currentstate == (* full_case = 32'd1 *) 2'h2;
+  assign _07_ = currentstate == (* full_case = 32'd1 *) 2'h3;
+  assign _08_ = currentstate == (* full_case = 32'd1 *) 3'h4;
+  assign _09_ = currentstate == (* full_case = 32'd1 *) 3'h5;
+  assign _10_ = currentstate == (* full_case = 32'd1 *) 3'h6;
+endmodule
+
+(* \library  = "work" *)
+(* hdlname = "top" *)
+(* src = "case.sv:1.8-1.11" *)
+module gold(clk, o, currentstate);
+  wire _00_;
+  wire _01_;
+  wire _02_;
+  wire _03_;
+  wire [1:0] _04_;
+  wire _05_;
+  wire _06_;
+  wire _07_;
+  wire _08_;
+  wire _09_;
+  (* src = "case.sv:2.8-2.11" *)
+  input clk;
+  wire clk;
+  (* src = "case.sv:3.14-3.26" *)
+  input [5:0] currentstate;
+  wire [5:0] currentstate;
+  (* src = "case.sv:4.19-4.20" *)
+  output [1:0] o;
+  reg [1:0] o;
+  assign _01_ = currentstate == (* src = "case.sv:17.4-17.8" *) 3'h7;
+  assign _05_ = currentstate == (* src = "case.sv:9.4-9.8" *) 1'h1;
+  assign _06_ = currentstate == (* src = "case.sv:9.4-9.8" *) 2'h2;
+  assign _07_ = currentstate == (* src = "case.sv:9.4-9.8" *) 2'h3;
+  assign _08_ = currentstate == (* src = "case.sv:13.4-13.8" *) 3'h4;
+  assign _09_ = currentstate == (* src = "case.sv:17.4-17.8" *) 3'h5;
+  assign _00_ = currentstate == (* src = "case.sv:17.4-17.8" *) 3'h6;
+  (* src = "case.sv:6.9-26.5" *)
+  always @(posedge clk)
+    o <= _04_;
+  assign _02_ = | (* src = "case.sv:8.3-25.10" *) { _07_, _06_, _05_ };
+  assign _03_ = | (* src = "case.sv:8.3-25.10" *) { _01_, _00_, _09_ };
+  function [1:0] _20_;
+    input [1:0] a;
+    input [5:0] b;
+    input [2:0] s;
+    (* src = "case.sv:8.3-25.10" *)
+    (* parallel_case *)
+    casez (s)
+      3'b??1:
+        _20_ = b[1:0];
+      3'b?1?:
+        _20_ = b[3:2];
+      3'b1??:
+        _20_ = b[5:4];
+      default:
+        _20_ = a;
+    endcase
+  endfunction
+  assign _04_ = _20_(2'h0, 6'h1b, { _02_, _08_, _03_ });
+endmodule
+
+module miter(in_clk, in_currentstate, trigger);
+  wire _0_;
+  wire \gate.$$n5 ;
+  wire \gate.$$n6 ;
+  wire \gate.$auto$opt_reduce.cc:134:opt_pmux$12 ;
+  wire \gate.$auto$opt_reduce.cc:134:opt_pmux$14 ;
+  wire \gate.$procmux$10_CMP ;
+  wire \gate.$procmux$4_CMP ;
+  wire \gate.$procmux$5_CMP ;
+  wire \gate.$procmux$6_CMP ;
+  wire \gate.$procmux$7_CMP ;
+  wire \gate.$procmux$8_CMP ;
+  wire \gate.$procmux$9_CMP ;
+  (* hdlname = "gate clk" *)
+  (* src = "case.sv:2.8-2.11" *)
+  wire \gate.clk ;
+  (* hdlname = "gate currentstate" *)
+  (* src = "case.sv:3.14-3.26" *)
+  wire [5:0] \gate.currentstate ;
+  (* hdlname = "gate o" *)
+  (* src = "case.sv:4.19-4.20" *)
+  reg [1:0] \gate.o ;
+  wire [1:0] gate_o;
+  wire \gold.$n10 ;
+  wire \gold.$n11 ;
+  wire \gold.$n13 ;
+  wire \gold.$n14 ;
+  wire [1:0] \gold.$n15 ;
+  wire \gold.$n5 ;
+  wire \gold.$n6 ;
+  wire \gold.$n7 ;
+  wire \gold.$n8 ;
+  wire \gold.$n9 ;
+  (* hdlname = "gold clk" *)
+  (* src = "case.sv:2.8-2.11" *)
+  wire \gold.clk ;
+  (* hdlname = "gold currentstate" *)
+  (* src = "case.sv:3.14-3.26" *)
+  wire [5:0] \gold.currentstate ;
+  (* hdlname = "gold o" *)
+  (* src = "case.sv:4.19-4.20" *)
+  reg [1:0] \gold.o ;
+  wire [1:0] gold_o;
+  input in_clk;
+  wire in_clk;
+  input [5:0] in_currentstate;
+  wire [5:0] in_currentstate;
+  output trigger;
+  wire trigger;
+  assign _0_ = gold_o === gate_o;
+  always @* if (1'h1) assert(_0_);
+  assign trigger = ~ _0_;
+  assign \gate.$auto$opt_reduce.cc:134:opt_pmux$12  = | { \gate.$procmux$6_CMP , \gate.$procmux$5_CMP , \gate.$procmux$4_CMP  };
+  assign \gate.$auto$opt_reduce.cc:134:opt_pmux$14  = | { \gate.$procmux$10_CMP , \gate.$procmux$9_CMP , \gate.$procmux$8_CMP  };
+  (* src = "case.sv:6.9-26.5" *)
+  always @(posedge \gate.clk )
+    \gate.o [1] <= \gate.$$n5 ;
+  (* src = "case.sv:6.9-26.5" *)
+  always @(posedge \gate.clk )
+    \gate.o [0] <= \gate.$$n6 ;
+  assign \gate.$procmux$10_CMP  = \gate.currentstate  == (* full_case = 32'd1 *) 3'h7;
+  function [1:0] \gate.$procmux$3 ;
+    input [1:0] a;
+    input [5:0] b;
+    input [2:0] s;
+    (* full_case = 32'd1 *)
+    (* parallel_case *)
+    casez (s)
+      3'b??1:
+        \gate.$procmux$3  = b[1:0];
+      3'b?1?:
+        \gate.$procmux$3  = b[3:2];
+      3'b1??:
+        \gate.$procmux$3  = b[5:4];
+      default:
+        \gate.$procmux$3  = a;
+    endcase
+  endfunction
+  assign { \gate.$$n5 , \gate.$$n6  } = \gate.$procmux$3 (2'h0, 6'h39, { \gate.$auto$opt_reduce.cc:134:opt_pmux$14 , \gate.$procmux$7_CMP , \gate.$auto$opt_reduce.cc:134:opt_pmux$12  });
+  assign \gate.$procmux$4_CMP  = \gate.currentstate  == (* full_case = 32'd1 *) 1'h1;
+  assign \gate.$procmux$5_CMP  = \gate.currentstate  == (* full_case = 32'd1 *) 2'h2;
+  assign \gate.$procmux$6_CMP  = \gate.currentstate  == (* full_case = 32'd1 *) 2'h3;
+  assign \gate.$procmux$7_CMP  = \gate.currentstate  == (* full_case = 32'd1 *) 3'h4;
+  assign \gate.$procmux$8_CMP  = \gate.currentstate  == (* full_case = 32'd1 *) 3'h5;
+  assign \gate.$procmux$9_CMP  = \gate.currentstate  == (* full_case = 32'd1 *) 3'h6;
+  assign \gold.$n11  = \gold.currentstate  == (* src = "case.sv:17.4-17.8" *) 3'h7;
+  assign \gold.$n5  = \gold.currentstate  == (* src = "case.sv:9.4-9.8" *) 1'h1;
+  assign \gold.$n6  = \gold.currentstate  == (* src = "case.sv:9.4-9.8" *) 2'h2;
+  assign \gold.$n7  = \gold.currentstate  == (* src = "case.sv:9.4-9.8" *) 2'h3;
+  assign \gold.$n8  = \gold.currentstate  == (* src = "case.sv:13.4-13.8" *) 3'h4;
+  assign \gold.$n9  = \gold.currentstate  == (* src = "case.sv:17.4-17.8" *) 3'h5;
+  assign \gold.$n10  = \gold.currentstate  == (* src = "case.sv:17.4-17.8" *) 3'h6;
+  (* src = "case.sv:6.9-26.5" *)
+  always @(posedge \gold.clk )
+    \gold.o  <= \gold.$n15 ;
+  assign \gold.$n13  = | (* src = "case.sv:8.3-25.10" *) { \gold.$n7 , \gold.$n6 , \gold.$n5  };
+  assign \gold.$n14  = | (* src = "case.sv:8.3-25.10" *) { \gold.$n11 , \gold.$n10 , \gold.$n9  };
+  function [1:0] \gold.$select_14 ;
+    input [1:0] a;
+    input [5:0] b;
+    input [2:0] s;
+    (* src = "case.sv:8.3-25.10" *)
+    (* parallel_case *)
+    casez (s)
+      3'b??1:
+        \gold.$select_14  = b[1:0];
+      3'b?1?:
+        \gold.$select_14  = b[3:2];
+      3'b1??:
+        \gold.$select_14  = b[5:4];
+      default:
+        \gold.$select_14  = a;
+    endcase
+  endfunction
+  assign \gold.$n15  = \gold.$select_14 (2'h0, 6'h1b, { \gold.$n13 , \gold.$n8 , \gold.$n14  });
+  assign \gold.clk  = in_clk;
+  assign \gold.currentstate  = in_currentstate;
+  assign gold_o = \gold.o ;
+  assign \gate.clk  = in_clk;
+  assign \gate.currentstate  = in_currentstate;
+  assign gate_o = \gate.o ;
+endmodule
diff --git a/tests/verific/miter.v b/tests/verific/miter.v
new file mode 100644
index 000000000..11b7103ae
--- /dev/null
+++ b/tests/verific/miter.v
@@ -0,0 +1,140 @@
+/* Generated by Preqorsor 0.45+139 (git sha1 2c3d2b3ec, c++ 15.0.0 -fPIC -O3) */
+
+(* \library  = "work" *)
+(* hdlname = "top" *)
+(* src = "case.sv:1.8-1.11" *)
+module gate(clk, o, currentstate);
+  wire _00_;
+  wire _01_;
+  wire _02_;
+  wire _03_;
+  wire _04_;
+  wire _05_;
+  wire _06_;
+  wire _07_;
+  wire _08_;
+  wire _09_;
+  wire _10_;
+  (* src = "case.sv:2.8-2.11" *)
+  input clk;
+  wire clk;
+  (* src = "case.sv:3.14-3.26" *)
+  input [5:0] currentstate;
+  wire [5:0] currentstate;
+  (* src = "case.sv:4.19-4.20" *)
+  output [1:0] o;
+  reg [1:0] o;
+  assign _02_ = | { _07_, _06_, _05_ };
+  assign _03_ = | { _04_, _10_, _09_ };
+  (* src = "case.sv:6.9-26.5" *)
+  always @(posedge clk)
+    o[1] <= _00_;
+  (* src = "case.sv:6.9-26.5" *)
+  always @(posedge clk)
+    o[0] <= _01_;
+  assign _04_ = currentstate == (* full_case = 32'd1 *) 3'h7;
+  function [1:0] _16_;
+    input [1:0] a;
+    input [5:0] b;
+    input [2:0] s;
+    (* full_case = 32'd1 *)
+    (* parallel_case *)
+    casez (s)
+      3'b??1:
+        _16_ = b[1:0];
+      3'b?1?:
+        _16_ = b[3:2];
+      3'b1??:
+        _16_ = b[5:4];
+      default:
+        _16_ = a;
+    endcase
+  endfunction
+  assign { _00_, _01_ } = _16_(2'h0, 6'h39, { _03_, _08_, _02_ });
+  assign _05_ = currentstate == (* full_case = 32'd1 *) 1'h1;
+  assign _06_ = currentstate == (* full_case = 32'd1 *) 2'h2;
+  assign _07_ = currentstate == (* full_case = 32'd1 *) 2'h3;
+  assign _08_ = currentstate == (* full_case = 32'd1 *) 3'h4;
+  assign _09_ = currentstate == (* full_case = 32'd1 *) 3'h5;
+  assign _10_ = currentstate == (* full_case = 32'd1 *) 3'h6;
+endmodule
+
+(* \library  = "work" *)
+(* hdlname = "top" *)
+(* src = "case.sv:1.8-1.11" *)
+module gold(clk, o, currentstate);
+  wire _00_;
+  wire _01_;
+  wire _02_;
+  wire _03_;
+  wire [1:0] _04_;
+  wire _05_;
+  wire _06_;
+  wire _07_;
+  wire _08_;
+  wire _09_;
+  (* src = "case.sv:2.8-2.11" *)
+  input clk;
+  wire clk;
+  (* src = "case.sv:3.14-3.26" *)
+  input [5:0] currentstate;
+  wire [5:0] currentstate;
+  (* src = "case.sv:4.19-4.20" *)
+  output [1:0] o;
+  reg [1:0] o;
+  assign _01_ = currentstate == (* src = "case.sv:17.4-17.8" *) 3'h7;
+  assign _05_ = currentstate == (* src = "case.sv:9.4-9.8" *) 1'h1;
+  assign _06_ = currentstate == (* src = "case.sv:9.4-9.8" *) 2'h2;
+  assign _07_ = currentstate == (* src = "case.sv:9.4-9.8" *) 2'h3;
+  assign _08_ = currentstate == (* src = "case.sv:13.4-13.8" *) 3'h4;
+  assign _09_ = currentstate == (* src = "case.sv:17.4-17.8" *) 3'h5;
+  assign _00_ = currentstate == (* src = "case.sv:17.4-17.8" *) 3'h6;
+  (* src = "case.sv:6.9-26.5" *)
+  always @(posedge clk)
+    o <= _04_;
+  assign _02_ = | (* src = "case.sv:8.3-25.10" *) { _07_, _06_, _05_ };
+  assign _03_ = | (* src = "case.sv:8.3-25.10" *) { _01_, _00_, _09_ };
+  function [1:0] _20_;
+    input [1:0] a;
+    input [5:0] b;
+    input [2:0] s;
+    (* src = "case.sv:8.3-25.10" *)
+    (* parallel_case *)
+    casez (s)
+      3'b??1:
+        _20_ = b[1:0];
+      3'b?1?:
+        _20_ = b[3:2];
+      3'b1??:
+        _20_ = b[5:4];
+      default:
+        _20_ = a;
+    endcase
+  endfunction
+  assign _04_ = _20_(2'h0, 6'h1b, { _02_, _08_, _03_ });
+endmodule
+
+module miter(in_clk, in_currentstate, trigger);
+  wire _0_;
+  wire [1:0] gate_o;
+  wire [1:0] gold_o;
+  input in_clk;
+  wire in_clk;
+  input [5:0] in_currentstate;
+  wire [5:0] in_currentstate;
+  output trigger;
+  wire trigger;
+  assign _0_ = gold_o === gate_o;
+  always @* if (1'h1) assert(_0_);
+  assign trigger = ~ _0_;
+  gate gate (
+    .clk(in_clk),
+    .currentstate(in_currentstate),
+    .o(gate_o)
+  );
+  gold gold (
+    .clk(in_clk),
+    .currentstate(in_currentstate),
+    .o(gold_o)
+  );
+endmodule
diff --git a/tests/verific/range_case.ys b/tests/verific/range_case.ys
deleted file mode 100644
index 99909af36..000000000
--- a/tests/verific/range_case.ys
+++ /dev/null
@@ -1,16 +0,0 @@
-import -cfg db_abstract_case_statement_synthesis 0
-read -sv range_case.sv
-import -import top 
-proc
-rename top gold
-
-import -cfg db_abstract_case_statement_synthesis 1
-read -sv range_case.sv
-import -import top 
-proc
-rename top gate
-
-miter -equiv -flatten -make_assert gold gate miter
-prep -top miter
-clk2fflogic
-sat -set-init-zero -tempinduct -prove-asserts -verify
diff --git a/tests/verific/rom_case.ys.fail b/tests/verific/rom_case.ys.skip
similarity index 100%
rename from tests/verific/rom_case.ys.fail
rename to tests/verific/rom_case.ys.skip