mirror of
https://github.com/YosysHQ/yosys
synced 2025-04-23 17:15:33 +00:00
Clean up Verific tests
This commit is contained in:
Akash Levy
parent
2c3d2b3ec6
commit
2d771a352e
10 changed files with 568 additions and 17 deletions
18
tests/verific/README.md
Normal file
18
tests/verific/README.md
Normal file
|
|
@ -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
|
||||
115
tests/verific/case.gate.v
Normal file
115
tests/verific/case.gate.v
Normal file
|
|
@ -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
|
||||
56
tests/verific/case.gold.v
Normal file
56
tests/verific/case.gold.v
Normal file
|
|
@ -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
|
||||
|
|
@ -1,4 +1,4 @@
|
|||
import -sv <<EOF
|
||||
import -formal <<EOF
|
||||
|
||||
module top(clk);
|
||||
input wire clk;
|
||||
238
tests/verific/miter.flatten.v
Normal file
238
tests/verific/miter.flatten.v
Normal file
|
|
@ -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
|
||||
140
tests/verific/miter.v
Normal file
140
tests/verific/miter.v
Normal file
|
|
@ -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
|
||||
|
|
@ -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
|
||||
Loading…
Add table
Add a link
Reference in a new issue