diff options
Diffstat (limited to 'tests')
40 files changed, 331 insertions, 92 deletions
diff --git a/tests/arch/fabulous/.gitignore b/tests/arch/fabulous/.gitignore new file mode 100644 index 000000000..9a71dca69 --- /dev/null +++ b/tests/arch/fabulous/.gitignore @@ -0,0 +1,4 @@ +*.log +/run-test.mk ++*_synth.v ++*_testbench diff --git a/tests/arch/fabulous/complexflop.ys b/tests/arch/fabulous/complexflop.ys new file mode 100644 index 000000000..13f4522b9 --- /dev/null +++ b/tests/arch/fabulous/complexflop.ys @@ -0,0 +1,37 @@ +read_verilog <<EOT +module top ( input d0, d1, d2, d3, ce, sr, clk, output reg q0, q1, q2, q3 ); + always @(posedge clk) + begin + if (sr) begin + q0 <= 1'b0; + q1 <= 1'b1; + end else begin + q0 <= d0; + q1 <= d1; + end + if (ce) begin + if (sr) begin + q2 <= 1'b0; + q3 <= 1'b1; + end else begin + q2 <= d2; + q3 <= d3; + end + end + end +endmodule +EOT + +hierarchy -top top +proc +flatten +equiv_opt -assert -map +/fabulous/prims.v synth_fabulous -complex-dff # equivalency check +design -load postopt # load the post-opt design (otherwise equiv_opt loads the pre-opt design) +cd top # Constrain all select calls below inside the top module + +select -assert-count 1 t:LUTFF_SR +select -assert-count 1 t:LUTFF_SS +select -assert-count 1 t:LUTFF_ESR +select -assert-count 1 t:LUTFF_ESS + +select -assert-none t:LUTFF_SR t:LUTFF_SS t:LUTFF_ESR t:LUTFF_ESS %% t:* %D diff --git a/tests/arch/fabulous/counter.ys b/tests/arch/fabulous/counter.ys new file mode 100644 index 000000000..d79b378a6 --- /dev/null +++ b/tests/arch/fabulous/counter.ys @@ -0,0 +1,26 @@ +read_verilog <<EOT +module top ( out, clk, reset ); + output [7:0] out; + input clk, reset; + reg [7:0] out; + + always @(posedge clk) + if (reset) + out <= 8'b0; + else + out <= out + 1; +endmodule +EOT + +hierarchy -top top +proc +flatten +equiv_opt -assert -map +/fabulous/prims.v synth_fabulous # equivalency check +design -load postopt # load the post-opt design (otherwise equiv_opt loads the pre-opt design) +cd top # Constrain all select calls below inside the top module + +select -assert-count 1 t:LUT2 +select -assert-count 7 t:LUT3 +select -assert-count 4 t:LUT4 +select -assert-count 8 t:LUTFF +select -assert-none t:LUT2 t:LUT3 t:LUT4 t:LUTFF %% t:* %D diff --git a/tests/arch/fabulous/custom_map.v b/tests/arch/fabulous/custom_map.v new file mode 100644 index 000000000..1538e837b --- /dev/null +++ b/tests/arch/fabulous/custom_map.v @@ -0,0 +1,3 @@ +module AND(input [7:0] A, B, output [7:0] Y); + ALU #(.MODE("AND")) _TECHMAP_REPLACE_ (.A(A), .B(B), .Y(Y)); +endmodule diff --git a/tests/arch/fabulous/custom_prims.v b/tests/arch/fabulous/custom_prims.v new file mode 100644 index 000000000..4989188e2 --- /dev/null +++ b/tests/arch/fabulous/custom_prims.v @@ -0,0 +1,8 @@ +(* blackbox *) +module AND(input [7:0] A, B, output [7:0] Y); +endmodule + +(* blackbox *) +module ALU(input [7:0] A, B, output [7:0] Y); +parameter MODE = ""; +endmodule diff --git a/tests/arch/fabulous/customisation.ys b/tests/arch/fabulous/customisation.ys new file mode 100644 index 000000000..0e78d2e56 --- /dev/null +++ b/tests/arch/fabulous/customisation.ys @@ -0,0 +1,10 @@ +read_verilog <<EOT +module prim_test(input [7:0] a, b, output [7:0] q); + AND and_i (.A(a), .B(b), .Y(q)); +endmodule +EOT + +# Test adding custom primitives and techmap rules +synth_fabulous -top prim_test -extra-plib custom_prims.v -extra-map custom_map.v +cd prim_test +select -assert-count 1 t:ALU diff --git a/tests/arch/fabulous/fsm.ys b/tests/arch/fabulous/fsm.ys new file mode 100644 index 000000000..9c3831682 --- /dev/null +++ b/tests/arch/fabulous/fsm.ys @@ -0,0 +1,19 @@ +read_verilog ../common/fsm.v +hierarchy -top fsm +proc +flatten + +equiv_opt -run :prove -map +/fabulous/prims.v synth_fabulous +async2sync +miter -equiv -make_assert -flatten gold gate miter +stat +sat -verify -prove-asserts -show-public -set-at 1 in_reset 1 -seq 20 -prove-skip 1 miter + +design -load postopt # load the post-opt design (otherwise equiv_opt loads the pre-opt design) +cd fsm # Constrain all select calls below inside the top module + +select -assert-count 6 t:LUTFF +select -assert-max 4 t:LUT2 +select -assert-max 2 t:LUT3 +select -assert-max 9 t:LUT4 +select -assert-none t:LUT2 t:LUT3 t:LUT4 t:LUTFF %% t:* %D diff --git a/tests/arch/fabulous/logic.ys b/tests/arch/fabulous/logic.ys new file mode 100644 index 000000000..730d9ab54 --- /dev/null +++ b/tests/arch/fabulous/logic.ys @@ -0,0 +1,10 @@ +read_verilog ../common/logic.v +hierarchy -top top +proc +equiv_opt -assert -map +/fabulous/prims.v synth_fabulous # equivalency check +design -load postopt # load the post-opt design (otherwise equiv_opt loads the pre-opt design) +cd top # Constrain all select calls below inside the top module +select -assert-max 1 t:LUT1 +select -assert-max 6 t:LUT2 +select -assert-max 2 t:LUT4 +select -assert-none t:LUT1 t:LUT2 t:LUT4 %% t:* %D diff --git a/tests/arch/fabulous/regfile.ys b/tests/arch/fabulous/regfile.ys new file mode 100644 index 000000000..8d1eedef0 --- /dev/null +++ b/tests/arch/fabulous/regfile.ys @@ -0,0 +1,33 @@ +read_verilog <<EOT +module sync_sync(input clk, we, input [4:0] aw, aa, ab, input [3:0] wd, output reg [3:0] ra, rb); + reg [3:0] mem[0:31]; + always @(posedge clk) + if (we) mem[aw] <= wd; + always @(posedge clk) + ra <= mem[aa]; + always @(posedge clk) + rb <= mem[ab]; +endmodule +EOT + +synth_fabulous -top sync_sync +cd sync_sync +select -assert-count 1 t:RegFile_32x4 + +design -reset + +read_verilog <<EOT +module async_sync(input clk, we, input [4:0] aw, aa, ab, input [3:0] wd, output reg [3:0] ra, rb); + reg [3:0] mem[0:31]; + always @(posedge clk) + if (we) mem[aw] <= wd; + always @(posedge clk) + ra <= mem[aa]; + always @(*) + rb <= mem[ab]; +endmodule +EOT + +synth_fabulous -top async_sync +cd async_sync +select -assert-count 1 t:RegFile_32x4 diff --git a/tests/arch/fabulous/tribuf.ys b/tests/arch/fabulous/tribuf.ys new file mode 100644 index 000000000..0dcf1cbab --- /dev/null +++ b/tests/arch/fabulous/tribuf.ys @@ -0,0 +1,12 @@ +read_verilog ../common/tribuf.v +hierarchy -top tristate +proc +tribuf +flatten +synth +equiv_opt -assert -map +/fabulous/prims.v -map +/simcells.v synth_fabulous -iopad # equivalency check +design -load postopt # load the post-opt design (otherwise equiv_opt loads the pre-opt design) +cd tristate # Constrain all select calls below inside the top module +select -assert-count 3 t:IO_1_bidirectional_frame_config_pass +select -assert-max 1 t:LUT1 +select -assert-none t:IO_1_bidirectional_frame_config_pass t:LUT1 %% t:* %D diff --git a/tests/arch/ice40/bug1597.ys b/tests/arch/ice40/bug1597.ys index b7983cfa4..c1509cabc 100644 --- a/tests/arch/ice40/bug1597.ys +++ b/tests/arch/ice40/bug1597.ys @@ -3,7 +3,7 @@ module top ( input CLK, PIN_1, PIN_2, PIN_3, PIN_4, PIN_5, PIN_6, PIN_7, PIN_8, PIN_9, PIN_10, PIN_11, PIN_12, PIN_13, PIN_25, output USBPU, PIN_14, PIN_15, PIN_16, PIN_17, PIN_18, - PIN_19, PIN_20, PIN_21, PIN_22, PIN_23, PIN_24, + PIN_19, ); assign USBPU = 0; @@ -67,6 +67,7 @@ module SSCounter6o (input wire rst, clk, adv, jmp, input wire [5:0] in, output w SB_LUT4 #(.LUT_INIT(16'h8BB8)) l5 (lo[5], in[5], jmp, out[5], co[4]); endmodule EOT +read_verilog -lib +/ice40/cells_sim.v hierarchy -top top flatten -equiv_opt -multiclock -map +/ice40/cells_sim.v synth_ice40 +equiv_opt -assert -multiclock -map +/ice40/cells_sim.v synth_ice40 diff --git a/tests/arch/ice40/ice40_opt.ys b/tests/arch/ice40/ice40_opt.ys index 71b68431e..e779ab207 100644 --- a/tests/arch/ice40/ice40_opt.ys +++ b/tests/arch/ice40/ice40_opt.ys @@ -21,6 +21,7 @@ module top(input CI, I0, output [1:0] CO, output O); endmodule EOT +read_verilog -icells -lib +/ice40/abc9_model.v +/ice40/cells_sim.v equiv_opt -assert -map +/ice40/abc9_model.v -map +/ice40/cells_sim.v ice40_opt design -load postopt select -assert-count 1 t:* diff --git a/tests/arch/intel_alm/counter.ys b/tests/arch/intel_alm/counter.ys index 56c9cabb3..0a5b9356a 100644 --- a/tests/arch/intel_alm/counter.ys +++ b/tests/arch/intel_alm/counter.ys @@ -2,7 +2,7 @@ read_verilog ../common/counter.v hierarchy -top top proc flatten -equiv_opt -async2sync -map +/intel_alm/common/alm_sim.v -map +/intel_alm/common/dff_sim.v synth_intel_alm -family cyclonev -noiopad -noclkbuf # equivalency check +equiv_opt -assert -async2sync -map +/intel_alm/common/alm_sim.v -map +/intel_alm/common/dff_sim.v synth_intel_alm -family cyclonev -noiopad -noclkbuf # equivalency check design -load postopt # load the post-opt design (otherwise equiv_opt loads the pre-opt design) cd top # Constrain all select calls below inside the top module @@ -17,7 +17,7 @@ read_verilog ../common/counter.v hierarchy -top top proc flatten -equiv_opt -async2sync -map +/intel_alm/common/alm_sim.v -map +/intel_alm/common/dff_sim.v synth_intel_alm -family cyclone10gx -noiopad -noclkbuf # equivalency check +equiv_opt -assert -async2sync -map +/intel_alm/common/alm_sim.v -map +/intel_alm/common/dff_sim.v synth_intel_alm -family cyclone10gx -noiopad -noclkbuf # equivalency check design -load postopt # load the post-opt design (otherwise equiv_opt loads the pre-opt design) cd top # Constrain all select calls below inside the top module diff --git a/tests/arch/xilinx/abc9_dff.ys b/tests/arch/xilinx/abc9_dff.ys index 0ba3901f7..79e5a322c 100644 --- a/tests/arch/xilinx/abc9_dff.ys +++ b/tests/arch/xilinx/abc9_dff.ys @@ -12,6 +12,7 @@ FDCE_1 #(.INIT(0)) fd7(.C(C), .CE(1'b1), .D(D), .CLR(1'b1), .Q(Q[6])); FDPE_1 #(.INIT(0)) fd8(.C(C), .CE(1'b1), .D(D), .PRE(1'b1), .Q(Q[7])); endmodule EOT +read_verilog -lib +/xilinx/cells_sim.v equiv_opt -assert -multiclock -map +/xilinx/cells_sim.v synth_xilinx -abc9 -dff -noiopad -noclkbuf design -load postopt select -assert-count 6 t:FD* @@ -31,6 +32,7 @@ FDCE_1 #(.INIT(0)) fd7(.C(C), .CE(1'b0), .D(D), .CLR(1'b0), .Q(Q[6])); FDPE_1 #(.INIT(0)) fd8(.C(C), .CE(1'b0), .D(D), .PRE(1'b0), .Q(Q[7])); endmodule EOT +read_verilog -lib +/xilinx/cells_sim.v equiv_opt -assert -multiclock -map +/xilinx/cells_sim.v synth_xilinx -abc9 -dff -noiopad -noclkbuf design -load postopt select -assert-count 4 t:FD* @@ -54,6 +56,7 @@ logger -expect warning "Whitebox '\$paramod\\FDRE\\INIT=.*1' with \(\* abc9_flop logger -expect warning "Whitebox '\$paramod\\FDRE_1\\INIT=.*1' with \(\* abc9_flop \*\) contains a \$dff cell with non-zero initial state -- this is not supported for ABC9 sequential synthesis. Treating as a blackbox\." 1 logger -expect warning "Whitebox 'FDSE' with \(\* abc9_flop \*\) contains a \$dff cell with non-zero initial state -- this is not supported for ABC9 sequential synthesis. Treating as a blackbox\." 1 logger -expect warning "Whitebox '\$paramod\\FDSE_1\\INIT=.*1' with \(\* abc9_flop \*\) contains a \$dff cell with non-zero initial state -- this is not supported for ABC9 sequential synthesis. Treating as a blackbox\." 1 +read_verilog -lib +/xilinx/cells_sim.v equiv_opt -assert -multiclock -map +/xilinx/cells_sim.v synth_xilinx -abc9 -dff -noiopad -noclkbuf design -load postopt select -assert-count 8 t:FD* @@ -75,6 +78,7 @@ always @(posedge clk or posedge pre) endmodule EOT proc +read_verilog -lib +/xilinx/cells_sim.v equiv_opt -assert -multiclock -map +/xilinx/cells_sim.v synth_xilinx -abc9 -dff -noiopad -noclkbuf design -load postopt select -assert-count 1 t:FDCE @@ -94,6 +98,7 @@ assign q = ~r; endmodule EOT proc +read_verilog -lib +/xilinx/cells_sim.v equiv_opt -assert -multiclock -map +/xilinx/cells_sim.v synth_xilinx -abc9 -dff -noiopad -noclkbuf design -load postopt select -assert-count 1 t:FDRE %co w:r %i @@ -111,6 +116,7 @@ assign q2 = r; endmodule EOT proc +read_verilog -lib +/xilinx/cells_sim.v equiv_opt -assert -multiclock -map +/xilinx/cells_sim.v synth_xilinx -abc9 -dff -noiopad -noclkbuf design -load postopt select -assert-count 1 t:FDRE %co %a w:r %i @@ -128,6 +134,7 @@ assign o = r1 | r2; endmodule EOT proc +read_verilog -lib +/xilinx/cells_sim.v equiv_opt -assert -multiclock -map +/xilinx/cells_sim.v synth_xilinx -abc9 -dff -noiopad -noclkbuf diff --git a/tests/arch/xilinx/opt_lut_ins.ys b/tests/arch/xilinx/opt_lut_ins.ys index a01d02179..2328919a3 100644 --- a/tests/arch/xilinx/opt_lut_ins.ys +++ b/tests/arch/xilinx/opt_lut_ins.ys @@ -18,6 +18,7 @@ end EOF +read_verilog -lib +/xilinx/cells_sim.v equiv_opt -assert -map +/xilinx/cells_sim.v opt_lut_ins -tech xilinx design -load postopt diff --git a/tests/arch/xilinx/xilinx_dffopt.ys b/tests/arch/xilinx/xilinx_dffopt.ys index c09699411..9f0b27ced 100644 --- a/tests/arch/xilinx/xilinx_dffopt.ys +++ b/tests/arch/xilinx/xilinx_dffopt.ys @@ -5,7 +5,7 @@ read_verilog << EOT module t0 (...); input wire clk; input wire [7:0] i; -output wire [7:0] o; +output wire [0:0] o; wire [7:0] tmp ; @@ -52,7 +52,7 @@ read_verilog << EOT module t0 (...); input wire clk; input wire [7:0] i; -output wire [7:0] o; +output wire [0:0] o; wire [7:0] tmp ; @@ -100,7 +100,7 @@ read_verilog << EOT module t0 (...); input wire clk; input wire [7:0] i; -output wire [7:0] o; +output wire [0:0] o; wire [7:0] tmp ; @@ -137,7 +137,7 @@ read_verilog << EOT module t0 (...); input wire clk; input wire [7:0] i; -output wire [7:0] o; +output wire [0:0] o; wire [7:0] tmp ; @@ -183,7 +183,7 @@ read_verilog << EOT module t0 (...); input wire clk; input wire [7:0] i; -output wire [7:0] o; +output wire [0:0] o; wire [7:0] tmp ; @@ -232,7 +232,7 @@ read_verilog << EOT module t0 (...); input wire clk; input wire [7:0] i; -output wire [7:0] o; +output wire [0:0] o; wire [7:0] tmp ; diff --git a/tests/blif/bug3385.ys b/tests/blif/bug3385.ys new file mode 100644 index 000000000..e1e45983d --- /dev/null +++ b/tests/blif/bug3385.ys @@ -0,0 +1,9 @@ +logger -expect error "Syntax error in line 4: names' input plane must have fewer than 13 signals." 1 +read_blif <<EOF +.model test +.inputs w0 w1 w2 w3 w4 w5 w6 w7 w8 w9 w10 w11 w12 w13 w14 w15 w16 w17 w18 w19 w20 w21 w22 w23 w24 w25 w26 w27 w28 w29 w30 +.outputs out +.names w0 w1 w2 w3 w4 w5 w6 w7 w8 w9 w10 w11 w12 w13 w14 w15 w16 w17 w18 w19 w20 w21 w22 w23 w24 w25 w26 w27 w28 w29 w30 out +1101010001100110010001100111001 0 +.end +EOF diff --git a/tests/opt/opt_dff_en.ys b/tests/opt/opt_dff_en.ys index 06ee6c63d..9538afcc2 100644 --- a/tests/opt/opt_dff_en.ys +++ b/tests/opt/opt_dff_en.ys @@ -6,7 +6,7 @@ module top(...); input CLK; input [1:0] D; -output [15:0] Q; +output [11:0] Q; input SRST; input ARST; input [1:0] CLR; diff --git a/tests/opt/opt_dff_mux.ys b/tests/opt/opt_dff_mux.ys index ed01bed59..f21f9e9b8 100644 --- a/tests/opt/opt_dff_mux.ys +++ b/tests/opt/opt_dff_mux.ys @@ -7,7 +7,7 @@ module top(...); input CLK; input NE, NS; input EN; -output [23:0] Q; +output [17:0] Q; input [23:0] D; input SRST; input ARST; diff --git a/tests/opt/opt_dff_qd.ys b/tests/opt/opt_dff_qd.ys index afc96c42f..7b0b4c224 100644 --- a/tests/opt/opt_dff_qd.ys +++ b/tests/opt/opt_dff_qd.ys @@ -7,7 +7,7 @@ module top(...); input CLK; input EN; (* init = 24'h555555 *) -output [23:0] Q; +output [19:0] Q; input SRST; input ARST; input [1:0] CLR; diff --git a/tests/opt/opt_dff_sr.ys b/tests/opt/opt_dff_sr.ys index 0961cb11e..1d3fd300e 100644 --- a/tests/opt/opt_dff_sr.ys +++ b/tests/opt/opt_dff_sr.ys @@ -22,10 +22,9 @@ EOT design -save orig -# Equivalence check will fail for unmapped adlatch and dlatchsr due to negative hold hack. -#equiv_opt -undef -assert -multiclock opt_dff -#design -load postopt -opt_dff +equiv_opt -undef -assert -multiclock opt_dff +design -load postopt + select -assert-count 1 t:$dffsr select -assert-count 1 t:$dffsr r:WIDTH=2 %i select -assert-count 1 t:$dffsre @@ -36,9 +35,9 @@ select -assert-none t:$sr design -load orig -#equiv_opt -undef -assert -multiclock opt_dff -keepdc -#design -load postopt -opt_dff -keepdc +equiv_opt -undef -assert -multiclock opt_dff -keepdc +design -load postopt + select -assert-count 1 t:$dffsr select -assert-count 1 t:$dffsr r:WIDTH=4 %i select -assert-count 1 t:$dffsre @@ -51,9 +50,9 @@ select -assert-count 1 t:$sr r:WIDTH=4 %i design -load orig simplemap -#equiv_opt -undef -assert -multiclock opt_dff -#design -load postopt -opt_dff +equiv_opt -undef -assert -multiclock opt_dff +design -load postopt + select -assert-count 1 t:$_DFF_PP0_ select -assert-count 1 t:$_DFF_PP1_ select -assert-count 1 t:$_DFFE_PN0P_ @@ -65,9 +64,9 @@ select -assert-none t:$_DFF_PP0_ t:$_DFF_PP1_ t:$_DFFE_PN0P_ t:$_DFFE_PN1P_ t:$_ design -load orig simplemap -#equiv_opt -undef -assert -multiclock opt_dff -keepdc -#design -load postopt -opt_dff -keepdc +equiv_opt -undef -assert -multiclock opt_dff -keepdc +design -load postopt + select -assert-count 1 t:$_DFF_PP0_ select -assert-count 1 t:$_DFF_PP1_ select -assert-count 2 t:$_DFFSR_PPP_ diff --git a/tests/opt/opt_expr_xor.ys b/tests/opt/opt_expr_xor.ys index a879f3ec9..8874f2775 100644 --- a/tests/opt/opt_expr_xor.ys +++ b/tests/opt/opt_expr_xor.ys @@ -10,7 +10,7 @@ design -save read select -assert-count 2 t:$xor select -assert-count 2 t:$xnor -equiv_opt opt_expr +equiv_opt -assert opt_expr design -load postopt select -assert-none t:$xor select -assert-none t:$xnor @@ -19,7 +19,7 @@ select -assert-count 2 t:$not design -load read simplemap -equiv_opt opt_expr +equiv_opt -assert opt_expr design -load postopt select -assert-none t:$_XOR_ select -assert-none t:$_XNOR_ # NB: simplemap does $xnor -> $_XOR_+$_NOT_ @@ -34,7 +34,7 @@ $_XNOR_ u1(.A(1'b1), .B(a), .Y(y[1])); endmodule EOT select -assert-count 2 t:$_XNOR_ -equiv_opt opt_expr +equiv_opt -assert opt_expr design -load postopt select -assert-none t:$_XNOR_ # NB: simplemap does $xnor -> $_XOR_+$_NOT_ select -assert-count 1 t:$_NOT_ @@ -49,7 +49,7 @@ assign y = a~^1'b0; assign z = a~^1'b1; endmodule EOT -equiv_opt opt_expr +equiv_opt -assert opt_expr # Single-bit $xor diff --git a/tests/sim/run-test.sh b/tests/sim/run-test.sh index d34d1f3c9..a5120e77e 100755 --- a/tests/sim/run-test.sh +++ b/tests/sim/run-test.sh @@ -3,7 +3,7 @@ set -eu source ../gen-tests-makefile.sh echo "Generate FST for sim models" find tb/* -name tb*.v | while read name; do - test_name=$(basename -s .v $name) + test_name=$(basename $name .v) echo "Test $test_name" verilog_name=${test_name:3}.v iverilog -o tb/$test_name.out $name $verilog_name diff --git a/tests/simple/memory.v b/tests/simple/memory.v index f38bdafd3..b478d9409 100644 --- a/tests/simple/memory.v +++ b/tests/simple/memory.v @@ -137,8 +137,13 @@ endmodule // ---------------------------------------------------------- -module memtest06_sync(input clk, input rst, input [2:0] idx, input [7:0] din, output [7:0] dout); +module memtest06_sync(clk, rst, idx, din, dout); + input clk; + input rst; (* gentb_constant=0 *) wire rst; + input [2:0] idx; + input [7:0] din; + output [7:0] dout; reg [7:0] test [0:7]; integer i; always @(posedge clk) begin @@ -156,8 +161,13 @@ module memtest06_sync(input clk, input rst, input [2:0] idx, input [7:0] din, ou assign dout = test[idx]; endmodule -module memtest06_async(input clk, input rst, input [2:0] idx, input [7:0] din, output [7:0] dout); +module memtest06_async(clk, rst, idx, din, dout); + input clk; + input rst; (* gentb_constant=0 *) wire rst; + input [2:0] idx; + input [7:0] din; + output [7:0] dout; reg [7:0] test [0:7]; integer i; always @(posedge clk or posedge rst) begin diff --git a/tests/simple/module_scope_func.v b/tests/simple/module_scope_func.v new file mode 100644 index 000000000..928078da4 --- /dev/null +++ b/tests/simple/module_scope_func.v @@ -0,0 +1,45 @@ +// Some strict implementatins either forbid hierarchical identifiers within +// constant expressions, or forbid declaring functions in generate blocks, or +// both. Yosys and Iverilog are not strict in either of these ways. +module module_scope_func_top( + input wire inp, + output wire [31:0] out1, out2, out4, out5, out7, out8, + output reg [31:0] out3, out6, out9 +); + function automatic integer incr; + input integer value; + incr = value + 1; + endfunction + task send; + output integer out; + out = 55; + endtask + + assign out1 = module_scope_func_top.incr(inp); + localparam C = module_scope_func_top.incr(10); + assign out2 = C; + initial module_scope_func_top.send(out3); + + if (1) begin : blk + // shadows module_scope_func_top.incr + function automatic integer incr; + input integer value; + incr = value * 2; + endfunction + // shadows module_scope_func_top.send + task send; + output integer out; + out = 66; + endtask + + assign out4 = module_scope_func_top.incr(inp); + localparam D = module_scope_func_top.incr(20); + assign out5 = D; + initial module_scope_func_top.send(out6); + + assign out7 = incr(inp); + localparam E = incr(30); + assign out8 = E; + initial send(out9); + end +endmodule diff --git a/tests/techmap/adff2dff.ys b/tests/techmap/adff2dff.ys index 53f7d2f08..6d03d1963 100644 --- a/tests/techmap/adff2dff.ys +++ b/tests/techmap/adff2dff.ys @@ -16,4 +16,4 @@ EOT proc -equiv_opt -async2sync techmap -map +/adff2dff.v +#equiv_opt -assert -async2sync techmap -map +/adff2dff.v diff --git a/tests/techmap/dff2ff.ys b/tests/techmap/dff2ff.ys index 5adf14b07..6e7e6082b 100644 --- a/tests/techmap/dff2ff.ys +++ b/tests/techmap/dff2ff.ys @@ -13,4 +13,4 @@ EOT proc -equiv_opt techmap -map +/dff2ff.v +equiv_opt -assert techmap -map +/dff2ff.v diff --git a/tests/techmap/dfflegalize_adlatch.ys b/tests/techmap/dfflegalize_adlatch.ys index b242cc809..559363301 100644 --- a/tests/techmap/dfflegalize_adlatch.ys +++ b/tests/techmap/dfflegalize_adlatch.ys @@ -12,7 +12,7 @@ $_DLATCH_PN1_ ff1 (.E(E), .R(R), .D(D), .Q(Q[1])); $_DLATCH_NP1_ ff2 (.E(E), .R(R), .D(D), .Q(Q[2])); endmodule -module top(input C, E, R, D, output [13:0] Q); +module top(input C, E, R, D, output [5:0] Q); adlatch0 adlatch0_(.E(E), .R(R), .D(D), .Q(Q[2:0])); adlatch1 adlatch1_(.E(E), .R(R), .D(D), .Q(Q[5:3])); endmodule diff --git a/tests/techmap/dfflegalize_adlatch_init.ys b/tests/techmap/dfflegalize_adlatch_init.ys index a55082d1d..8e371c528 100644 --- a/tests/techmap/dfflegalize_adlatch_init.ys +++ b/tests/techmap/dfflegalize_adlatch_init.ys @@ -12,7 +12,7 @@ $_DLATCH_PN1_ ff1 (.E(E), .R(R), .D(D), .Q(Q[1])); $_DLATCH_NP1_ ff2 (.E(E), .R(R), .D(D), .Q(Q[2])); endmodule -module top(input C, E, R, D, output [13:0] Q); +module top(input C, E, R, D, output [5:0] Q); adlatch0 adlatch0_(.E(E), .R(R), .D(D), .Q(Q[2:0])); adlatch1 adlatch1_(.E(E), .R(R), .D(D), .Q(Q[5:3])); endmodule diff --git a/tests/techmap/dfflegalize_aldff.ys b/tests/techmap/dfflegalize_aldff.ys index 1ee9e3af6..5be3e9742 100644 --- a/tests/techmap/dfflegalize_aldff.ys +++ b/tests/techmap/dfflegalize_aldff.ys @@ -24,8 +24,8 @@ design -save orig flatten equiv_opt -assert -multiclock dfflegalize -cell $_ALDFF_PP_ x equiv_opt -assert -multiclock dfflegalize -cell $_ALDFFE_PPP_ x -#equiv_opt -assert -multiclock dfflegalize -cell $_DFFSR_PPP_ x -#equiv_opt -assert -multiclock dfflegalize -cell $_DFFSRE_PPPP_ x +equiv_opt -assert -multiclock dfflegalize -cell $_DFFSR_PPP_ x +equiv_opt -assert -multiclock dfflegalize -cell $_DFFSRE_PPPP_ x # Convert everything to ALDFFs. diff --git a/tests/techmap/dfflegalize_aldff_init.ys b/tests/techmap/dfflegalize_aldff_init.ys index f4db8dd32..ffa7cbf16 100644 --- a/tests/techmap/dfflegalize_aldff_init.ys +++ b/tests/techmap/dfflegalize_aldff_init.ys @@ -26,10 +26,10 @@ equiv_opt -assert -multiclock dfflegalize -cell $_ALDFF_PP_ 0 equiv_opt -assert -multiclock dfflegalize -cell $_ALDFF_PP_ 1 equiv_opt -assert -multiclock dfflegalize -cell $_ALDFFE_PPP_ 0 equiv_opt -assert -multiclock dfflegalize -cell $_ALDFFE_PPP_ 1 -#equiv_opt -assert -multiclock dfflegalize -cell $_DFFSR_PPP_ 0 -#equiv_opt -assert -multiclock dfflegalize -cell $_DFFSR_PPP_ 1 -#equiv_opt -assert -multiclock dfflegalize -cell $_DFFSRE_PPPP_ 0 -#equiv_opt -assert -multiclock dfflegalize -cell $_DFFSRE_PPPP_ 1 +equiv_opt -assert -multiclock dfflegalize -cell $_DFFSR_PPP_ 0 +equiv_opt -assert -multiclock dfflegalize -cell $_DFFSR_PPP_ 1 +equiv_opt -assert -multiclock dfflegalize -cell $_DFFSRE_PPPP_ 0 +equiv_opt -assert -multiclock dfflegalize -cell $_DFFSRE_PPPP_ 1 # Convert everything to ALDFFs. diff --git a/tests/techmap/dfflegalize_dffsr_init.ys b/tests/techmap/dfflegalize_dffsr_init.ys index ce5a32f76..b6160bb87 100644 --- a/tests/techmap/dfflegalize_dffsr_init.ys +++ b/tests/techmap/dfflegalize_dffsr_init.ys @@ -41,18 +41,18 @@ EOT design -save orig flatten -#equiv_opt -assert -multiclock dfflegalize -cell $_DFF_PP0_ 0 -cell $_SR_PP_ 0 -#equiv_opt -assert -multiclock dfflegalize -cell $_DFF_PP0_ 1 -cell $_SR_PP_ 0 -#equiv_opt -assert -multiclock dfflegalize -cell $_DFF_PP1_ 0 -cell $_SR_PP_ 0 -#equiv_opt -assert -multiclock dfflegalize -cell $_DFF_PP1_ 1 -cell $_SR_PP_ 0 -#equiv_opt -assert -multiclock dfflegalize -cell $_DFFE_PP0P_ 0 -cell $_SR_PP_ 0 -#equiv_opt -assert -multiclock dfflegalize -cell $_DFFE_PP0P_ 1 -cell $_SR_PP_ 0 -#equiv_opt -assert -multiclock dfflegalize -cell $_DFFE_PP1P_ 0 -cell $_SR_PP_ 0 -#equiv_opt -assert -multiclock dfflegalize -cell $_DFFE_PP1P_ 1 -cell $_SR_PP_ 0 -#equiv_opt -assert -multiclock dfflegalize -cell $_DFFSR_PPP_ 0 -#equiv_opt -assert -multiclock dfflegalize -cell $_DFFSR_PPP_ 1 -#equiv_opt -assert -multiclock dfflegalize -cell $_DFFSRE_PPPP_ 0 -#equiv_opt -assert -multiclock dfflegalize -cell $_DFFSRE_PPPP_ 1 +equiv_opt -assert -multiclock dfflegalize -cell $_DFF_PP0_ 0 -cell $_SR_PP_ 0 +equiv_opt -assert -multiclock dfflegalize -cell $_DFF_PP0_ 1 -cell $_SR_PP_ 0 +equiv_opt -assert -multiclock dfflegalize -cell $_DFF_PP1_ 0 -cell $_SR_PP_ 0 +equiv_opt -assert -multiclock dfflegalize -cell $_DFF_PP1_ 1 -cell $_SR_PP_ 0 +equiv_opt -assert -multiclock dfflegalize -cell $_DFFE_PP0P_ 0 -cell $_SR_PP_ 0 +equiv_opt -assert -multiclock dfflegalize -cell $_DFFE_PP0P_ 1 -cell $_SR_PP_ 0 +equiv_opt -assert -multiclock dfflegalize -cell $_DFFE_PP1P_ 0 -cell $_SR_PP_ 0 +equiv_opt -assert -multiclock dfflegalize -cell $_DFFE_PP1P_ 1 -cell $_SR_PP_ 0 +equiv_opt -assert -multiclock dfflegalize -cell $_DFFSR_PPP_ 0 +equiv_opt -assert -multiclock dfflegalize -cell $_DFFSR_PPP_ 1 +equiv_opt -assert -multiclock dfflegalize -cell $_DFFSRE_PPPP_ 0 +equiv_opt -assert -multiclock dfflegalize -cell $_DFFSRE_PPPP_ 1 # Convert everything to ADFFs. diff --git a/tests/techmap/dfflegalize_dlatchsr_init.ys b/tests/techmap/dfflegalize_dlatchsr_init.ys index b38a9eb3b..da4ca164e 100644 --- a/tests/techmap/dfflegalize_dlatchsr_init.ys +++ b/tests/techmap/dfflegalize_dlatchsr_init.ys @@ -14,7 +14,7 @@ $_DLATCHSR_PNP_ ff2 (.E(E), .R(R), .S(S), .D(D), .Q(Q[2])); $_DLATCHSR_NPP_ ff3 (.E(E), .R(R), .S(S), .D(D), .Q(Q[3])); endmodule -module top(input C, E, R, S, D, output [17:0] Q); +module top(input C, E, R, S, D, output [7:0] Q); dlatchsr0 dlatchsr0_(.E(E), .R(R), .S(S), .D(D), .Q(Q[3:0])); dlatchsr1 dlatchsr1_(.E(E), .R(R), .S(S), .D(D), .Q(Q[7:4])); endmodule @@ -23,12 +23,12 @@ EOT design -save orig flatten -#equiv_opt -assert -multiclock dfflegalize -cell $_DLATCH_PP0_ 0 -#equiv_opt -assert -multiclock dfflegalize -cell $_DLATCH_PP0_ 1 -#equiv_opt -assert -multiclock dfflegalize -cell $_DLATCH_PP1_ 0 -#equiv_opt -assert -multiclock dfflegalize -cell $_DLATCH_PP1_ 1 -#equiv_opt -assert -multiclock dfflegalize -cell $_DLATCHSR_PPP_ 0 -#equiv_opt -assert -multiclock dfflegalize -cell $_DLATCHSR_PPP_ 1 +equiv_opt -assert -multiclock dfflegalize -cell $_DLATCH_PP0_ 0 +equiv_opt -assert -multiclock dfflegalize -cell $_DLATCH_PP0_ 1 +equiv_opt -assert -multiclock dfflegalize -cell $_DLATCH_PP1_ 0 +equiv_opt -assert -multiclock dfflegalize -cell $_DLATCH_PP1_ 1 +equiv_opt -assert -multiclock dfflegalize -cell $_DLATCHSR_PPP_ 0 +equiv_opt -assert -multiclock dfflegalize -cell $_DLATCHSR_PPP_ 1 # Convert everything to ADLATCHs. diff --git a/tests/techmap/dfflegalize_sr_init.ys b/tests/techmap/dfflegalize_sr_init.ys index 9d724de29..7cb1c629d 100644 --- a/tests/techmap/dfflegalize_sr_init.ys +++ b/tests/techmap/dfflegalize_sr_init.ys @@ -21,18 +21,18 @@ EOT design -save orig flatten -#equiv_opt -assert -multiclock dfflegalize -cell $_SR_PP_ 0 -#equiv_opt -assert -multiclock dfflegalize -cell $_SR_PP_ 1 -#equiv_opt -assert -multiclock dfflegalize -cell $_DLATCH_PP0_ 0 -#equiv_opt -assert -multiclock dfflegalize -cell $_DLATCH_PP0_ 1 -#equiv_opt -assert -multiclock dfflegalize -cell $_DLATCH_PP1_ 0 -#equiv_opt -assert -multiclock dfflegalize -cell $_DLATCH_PP1_ 1 -#equiv_opt -assert -multiclock dfflegalize -cell $_DLATCHSR_PPP_ 0 -#equiv_opt -assert -multiclock dfflegalize -cell $_DLATCHSR_PPP_ 1 -#equiv_opt -assert -multiclock dfflegalize -cell $_DFFSR_PPP_ 0 -#equiv_opt -assert -multiclock dfflegalize -cell $_DFFSR_PPP_ 1 -#equiv_opt -assert -multiclock dfflegalize -cell $_DFFSRE_PPPP_ 0 -#equiv_opt -assert -multiclock dfflegalize -cell $_DFFSRE_PPPP_ 1 +equiv_opt -assert -multiclock dfflegalize -cell $_SR_PP_ 0 +equiv_opt -assert -multiclock dfflegalize -cell $_SR_PP_ 1 +equiv_opt -assert -multiclock dfflegalize -cell $_DLATCH_PP0_ 0 +equiv_opt -assert -multiclock dfflegalize -cell $_DLATCH_PP0_ 1 +equiv_opt -assert -multiclock dfflegalize -cell $_DLATCH_PP1_ 0 +equiv_opt -assert -multiclock dfflegalize -cell $_DLATCH_PP1_ 1 +equiv_opt -assert -multiclock dfflegalize -cell $_DLATCHSR_PPP_ 0 +equiv_opt -assert -multiclock dfflegalize -cell $_DLATCHSR_PPP_ 1 +equiv_opt -assert -multiclock dfflegalize -cell $_DFFSR_PPP_ 0 +equiv_opt -assert -multiclock dfflegalize -cell $_DFFSR_PPP_ 1 +equiv_opt -assert -multiclock dfflegalize -cell $_DFFSRE_PPPP_ 0 +equiv_opt -assert -multiclock dfflegalize -cell $_DFFSRE_PPPP_ 1 # Convert everything to SRs. diff --git a/tests/techmap/dfflibmap.ys b/tests/techmap/dfflibmap.ys index 04477eb14..b0a7d6b7e 100644 --- a/tests/techmap/dfflibmap.ys +++ b/tests/techmap/dfflibmap.ys @@ -17,9 +17,11 @@ EOT simplemap design -save orig +read_liberty -lib dfflibmap.lib + +equiv_opt -map dfflibmap-sim.v -assert -multiclock dfflibmap -liberty dfflibmap.lib +equiv_opt -map dfflibmap-sim.v -assert -multiclock dfflibmap -prepare -liberty dfflibmap.lib -#equiv_opt -map dfflibmap-sim.v -assert -multiclock dfflibmap -liberty dfflibmap.lib -#equiv_opt -map dfflibmap-sim.v -assert -multiclock dfflibmap -prepare -liberty dfflibmap.lib dfflibmap -prepare -liberty dfflibmap.lib equiv_opt -map dfflibmap-sim.v -assert -multiclock dfflibmap -map-only -liberty dfflibmap.lib diff --git a/tests/techmap/dffunmap.ys b/tests/techmap/dffunmap.ys index b813078ee..247699f80 100644 --- a/tests/techmap/dffunmap.ys +++ b/tests/techmap/dffunmap.ys @@ -4,7 +4,7 @@ module top(...); input C, R, E, S; input [1:0] D; -output [20:0] Q; +output [17:0] Q; $dff #(.CLK_POLARITY(1'b0), .WIDTH(2)) ff0 (.CLK(C), .D(D), .Q(Q[1:0])); $dffe #(.CLK_POLARITY(1'b0), .EN_POLARITY(1'b0), .WIDTH(2)) ff1 (.CLK(C), .EN(E), .D(D), .Q(Q[3:2])); diff --git a/tests/techmap/pmux2mux.ys b/tests/techmap/pmux2mux.ys index 1714a6b87..1e08485ef 100644 --- a/tests/techmap/pmux2mux.ys +++ b/tests/techmap/pmux2mux.ys @@ -12,4 +12,4 @@ output [3:0] O; endmodule EOT -equiv_opt techmap -map +/pmux2mux.v +equiv_opt -assert techmap -map +/pmux2mux.v diff --git a/tests/techmap/shiftx2mux.ys b/tests/techmap/shiftx2mux.ys index f749e79b2..680681297 100644 --- a/tests/techmap/shiftx2mux.ys +++ b/tests/techmap/shiftx2mux.ys @@ -106,4 +106,4 @@ endmodule EOT opt wreduce -equiv_opt techmap +equiv_opt -assert techmap diff --git a/tests/techmap/zinit.ys b/tests/techmap/zinit.ys index bc07f40e6..562db0776 100644 --- a/tests/techmap/zinit.ys +++ b/tests/techmap/zinit.ys @@ -13,6 +13,8 @@ $_DFF_PN1_ dff5 (.C(C), .D(D[0]), .R(R), .Q(Q[5])); $_DFF_PP0_ dff6 (.C(C), .D(D[0]), .R(R), .Q(Q[6])); $_DFF_PP1_ dff7 (.C(C), .D(D[0]), .R(R), .Q(Q[7])); +assign Q[8] = 0; + $adff #(.WIDTH(2), .CLK_POLARITY(1), .ARST_POLARITY(1'b0), .ARST_VALUE(2'b10)) dff8 (.CLK(C), .ARST(R), .D(D), .Q(Q[10:9])); $adff #(.WIDTH(2), .CLK_POLARITY(0), .ARST_POLARITY(1'b1), .ARST_VALUE(2'b01)) dff9 (.CLK(C), .ARST(R), .D(D), .Q(Q[12:11])); endmodule @@ -44,6 +46,8 @@ $_DFF_PN1_ dff5 (.C(C), .D(D[0]), .R(R), .Q(Q[5])); $_DFF_PP0_ dff6 (.C(C), .D(D[0]), .R(R), .Q(Q[6])); $_DFF_PP1_ dff7 (.C(C), .D(D[0]), .R(R), .Q(Q[7])); +assign Q[8] = 0; + $adff #(.WIDTH(2), .CLK_POLARITY(1), .ARST_POLARITY(1'b0), .ARST_VALUE(2'b10)) dff8 (.CLK(C), .ARST(R), .D(D), .Q(Q[10:9])); $adff #(.WIDTH(2), .CLK_POLARITY(0), .ARST_POLARITY(1'b1), .ARST_VALUE(2'b01)) dff9 (.CLK(C), .ARST(R), .D(D), .Q(Q[12:11])); endmodule @@ -91,9 +95,8 @@ $_SDFFE_PP1P_ dff23(.C(C), .D(D[0]),.E(E), .R(R), .Q(Q[23])); endmodule EOT -#equiv_opt -assert -multiclock zinit -#design -load postopt -zinit +equiv_opt -assert -multiclock zinit +design -load postopt select -assert-count 48 t:$_NOT_ select -assert-count 0 w:Q a:init %i @@ -138,9 +141,8 @@ $_SDFFE_PP1P_ dff23(.C(C), .D(D[0]),.E(E), .R(R), .Q(Q[23])); endmodule EOT -#equiv_opt -assert -multiclock zinit -#design -load postopt -zinit +equiv_opt -assert -multiclock zinit +design -load postopt select -assert-count 0 t:$_NOT_ select -assert-count 1 w:Q a:init=24'b0 %i diff --git a/tests/various/smtlib2_module-expected.smt2 b/tests/various/smtlib2_module-expected.smt2 index 74e2f3fca..494e7cda0 100644 --- a/tests/various/smtlib2_module-expected.smt2 +++ b/tests/various/smtlib2_module-expected.smt2 @@ -4,14 +4,14 @@ (declare-fun |smtlib2_is| (|smtlib2_s|) Bool) (declare-fun |smtlib2#0| (|smtlib2_s|) (_ BitVec 8)) ; \a ; yosys-smt2-input a 8 -; yosys-smt2-witness {"offset": 0, "path": ["\\a"], "smtname": "a", "type": "input", "width": 8} +; yosys-smt2-witness {"offset": 0, "path": ["\\a"], "smtname": "a", "smtoffset": 0, "type": "input", "width": 8} (define-fun |smtlib2_n a| ((state |smtlib2_s|)) (_ BitVec 8) (|smtlib2#0| state)) (declare-fun |smtlib2#1| (|smtlib2_s|) (_ BitVec 8)) ; \b ; yosys-smt2-input b 8 -; yosys-smt2-witness {"offset": 0, "path": ["\\b"], "smtname": "b", "type": "input", "width": 8} +; yosys-smt2-witness {"offset": 0, "path": ["\\b"], "smtname": "b", "smtoffset": 0, "type": "input", "width": 8} (define-fun |smtlib2_n b| ((state |smtlib2_s|)) (_ BitVec 8) (|smtlib2#1| state)) ; yosys-smt2-output add 8 -; yosys-smt2-witness {"offset": 0, "path": ["\\add"], "smtname": "add", "type": "blackbox", "width": 8} +; yosys-smt2-witness {"offset": 0, "path": ["\\add"], "smtname": "add", "smtoffset": 0, "type": "blackbox", "width": 8} (define-fun |smtlib2_n add| ((state |smtlib2_s|)) (_ BitVec 8) (let ( (|a| (|smtlib2_n a| state)) (|b| (|smtlib2_n b| state)) @@ -19,7 +19,7 @@ (bvadd a b) )) ; yosys-smt2-output eq 1 -; yosys-smt2-witness {"offset": 0, "path": ["\\eq"], "smtname": "eq", "type": "blackbox", "width": 1} +; yosys-smt2-witness {"offset": 0, "path": ["\\eq"], "smtname": "eq", "smtoffset": 0, "type": "blackbox", "width": 1} (define-fun |smtlib2_n eq| ((state |smtlib2_s|)) Bool (let ( (|a| (|smtlib2_n a| state)) (|b| (|smtlib2_n b| state)) @@ -27,7 +27,7 @@ (= a b) )) ; yosys-smt2-output sub 8 -; yosys-smt2-witness {"offset": 0, "path": ["\\sub"], "smtname": "sub", "type": "blackbox", "width": 8} +; yosys-smt2-witness {"offset": 0, "path": ["\\sub"], "smtname": "sub", "smtoffset": 0, "type": "blackbox", "width": 8} (define-fun |smtlib2_n sub| ((state |smtlib2_s|)) (_ BitVec 8) (let ( (|a| (|smtlib2_n a| state)) (|b| (|smtlib2_n b| state)) @@ -49,10 +49,10 @@ (declare-fun |uut#2| (|uut_s|) (_ BitVec 8)) ; \sub (declare-fun |uut_h s| (|uut_s|) |smtlib2_s|) ; yosys-smt2-anyconst uut#3 8 smtlib2_module.v:14.17-14.26 -; yosys-smt2-witness {"offset": 0, "path": ["\\a"], "smtname": 3, "type": "init", "width": 8} +; yosys-smt2-witness {"offset": 0, "path": ["\\a"], "smtname": 3, "smtoffset": 0, "type": "init", "width": 8} (declare-fun |uut#3| (|uut_s|) (_ BitVec 8)) ; \a ; yosys-smt2-anyconst uut#4 8 smtlib2_module.v:14.32-14.41 -; yosys-smt2-witness {"offset": 0, "path": ["\\b"], "smtname": 4, "type": "init", "width": 8} +; yosys-smt2-witness {"offset": 0, "path": ["\\b"], "smtname": 4, "smtoffset": 0, "type": "init", "width": 8} (declare-fun |uut#4| (|uut_s|) (_ BitVec 8)) ; \b (define-fun |uut#5| ((state |uut_s|)) (_ BitVec 8) (bvadd (|uut#3| state) (|uut#4| state))) ; \add2 (define-fun |uut#6| ((state |uut_s|)) Bool (= (|uut#0| state) (|uut#5| state))) ; $0$formal$smtlib2_module.v:28$1_CHECK[0:0]$9 |