Clean up Verific tests

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

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

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

tests/verific/memory_semantics.ys → tests/verific/memory_semantics.ys.skip

@@ -1,4 +1,4 @@
-import -sv <<EOF
+import -formal <<EOF
 
 module top(clk);
 input wire clk;