Merge branch 'YosysHQ:main' into main

tests/opt/opt_hier.tcl

@@ -0,0 +1,34 @@
+yosys -import
+
+# per each opt_hier_*.v source file, confirm flattening and hieropt+flattening
+# are combinationally equivalent
+foreach fn [glob opt_hier_*.v] {
+	log -header "Test $fn"
+	log -push
+	design -reset
+
+	read_verilog $fn
+	hierarchy -auto-top
+	prep -top top
+	design -save start
+	flatten
+	design -save gold
+	design -load start
+	opt -hier
+	# check any instances marked `should_get_optimized_out` were
+	# indeed optimized out
+	select -assert-none a:should_get_optimized_out
+	dump
+	flatten
+	design -save gate
+
+	design -reset
+	design -copy-from gold -as gold A:top
+	design -copy-from gate -as gate A:top
+	yosys rename -hide
+	equiv_make gold gate equiv
+	equiv_induct equiv
+	equiv_status -assert equiv
+
+	log -pop
+}

tests/opt/opt_hier_simple1.v

@@ -0,0 +1,8 @@
+module m(input a, output y1, output y2);
+	assign y1 = a;
+	assign y2 = a;
+endmodule
+
+module top(input a, output y2, output y1);
+	m inst(.a(a), .y1(y1), .y2(y2));
+endmodule

tests/opt/opt_hier_simple2.v

@@ -0,0 +1,7 @@
+module m(input [3:0] i, output [3:0] y);
+	assign y = i + 1;
+endmodule
+
+module top(output [3:0] y);
+	m inst(.i(4), .y(y));
+endmodule

tests/opt/opt_hier_test1.v

@@ -0,0 +1,22 @@
+(* blackbox *)
+module bb(output y);
+endmodule
+
+// all instances of `m` tie together a[1], a[2]
+// this can be used to conclude y[0]=0
+module m(input [3:0] a, output [1:0] y, output x);
+	assign y[0] = a[1] != a[2];
+	assign x = a[0] ^ a[3];
+	(* should_get_optimized_out *)
+	bb bb1(.y(y[1]));
+endmodule
+
+module top(input j, output z, output [2:0] x);
+	wire [1:0] y1;
+	wire [1:0] y2;
+	wire [1:0] y3;
+	m inst1(.a(0), .y(y1), .x(x[0]));
+	m inst2(.a(15), .y(y2), .x(x[1]));
+	m inst3(.a({1'b1, j, j, 1'b0}), .y(y3), .x(x[2]));
+	assign z = (&y1) ^ (&y2) ^ (&y3);
+endmodule

tests/opt/run-test.sh

@@ -1,4 +1,4 @@
 #!/usr/bin/env bash
 set -eu
 source ../gen-tests-makefile.sh
-generate_mk --yosys-scripts
+generate_mk --yosys-scripts --tcl-scripts

tests/various/lcov.gold

@@ -0,0 +1,44 @@
+SF:lcov.v
+DA:2,1
+DA:3,1
+DA:4,1
+DA:5,1
+DA:6,1
+DA:7,1
+DA:8,1
+DA:9,0
+DA:13,1
+DA:14,1
+DA:17,1
+DA:18,1
+DA:19,1
+DA:21,0
+DA:22,0
+DA:23,0
+DA:24,0
+DA:25,0
+DA:26,0
+DA:27,0
+DA:28,0
+DA:29,0
+DA:30,0
+DA:32,1
+DA:33,1
+DA:36,0
+DA:37,0
+DA:38,0
+DA:40,0
+DA:41,0
+DA:42,0
+DA:43,0
+DA:44,0
+DA:45,0
+DA:46,0
+DA:48,0
+DA:49,0
+DA:52,1
+DA:53,0
+DA:56,1
+LF:40
+LH:16
+end_of_record

tests/various/lcov.v

@@ -0,0 +1,59 @@
+module top (
+    input  wire        clk,
+    input  wire        rst,
+    input  wire [7:0]  a,
+    input  wire [7:0]  b,
+    input  wire [3:0]  c,
+    input  wire        en,
+    output wire [7:0]  out1,
+    output wire [7:0]  out2
+);
+
+    // Shared intermediate signal
+    wire [7:0] ab_sum;
+    assign ab_sum = a + b;
+
+    // Logic cone for out1
+    wire [7:0] cone1_1, cone1_2;
+    assign cone1_1 = ab_sum ^ {4{c[1:0]}};
+    assign cone1_2 = (a & b) | {4{c[3:2]}};
+
+    reg  [7:0] reg1, reg2; // only reg1 feeds into out1, but both share a source location
+    always @(posedge clk or posedge rst) begin
+        if (rst) begin
+            reg1 <= 8'h00;
+            reg2 <= 8'hFF;
+        end else if (en) begin
+            reg1 <= cone1_1 + cone1_2;
+            reg2 <= cone1_2 - cone1_1;
+        end
+    end
+
+    wire [7:0] cone1_3;
+    assign cone1_3 = reg1 & ~a[0];
+
+    // Logic cone for out2
+    wire [7:0] cone2_1, cone2_2;
+    assign cone2_1 = (ab_sum << 1) | (a >> 2);
+    assign cone2_2 = (b ^ {4{c[2:0]}}) & 8'hAA;
+
+    reg  [7:0] reg3;
+    always @(posedge clk or posedge rst) begin
+        if (rst)
+            reg3 <= 8'h0F;
+        else
+            reg3 <= cone2_1 ^ cone2_2 ^ reg1[7:0];
+    end
+
+    wire [7:0] cone2_3;
+    assign cone2_3 = reg3 | (reg2 ^ 8'h55);
+
+    // Outputs
+    assign out1 = cone1_3 | (reg1 ^ 8'hA5);
+    assign out2 = cone2_3 & (reg3 | 8'h5A);
+
+    always @(posedge clk) begin
+        assert (out1 == 8'h42);
+    end
+
+endmodule

tests/various/lcov.ys

@@ -0,0 +1,8 @@
+read_verilog -formal lcov.v
+prep -top top
+async2sync
+chformal -lower
+select -set covered t:$assert %ci*
+select -set irrelevant o:* %ci* %n
+linecoverage -lcov lcov.out @covered @irrelevant %u
+exec -expect-return 0 -- diff -q lcov.out lcov.gold