From 6c78bd36372b0f38ea18cacf60996778448fe48e Mon Sep 17 00:00:00 2001
From: "Emil J. Tywoniak" <emil@tywoniak.eu>
Date: Thu, 28 Nov 2024 15:13:51 +0100
Subject: [PATCH 1/8] techmap: add a Han-Carlson option for `$lcu` mapping

---
 techlibs/common/Makefile.inc          |  1 +
 techlibs/common/choices/han-carlson.v | 57 +++++++++++++++++++++++++++
 2 files changed, 58 insertions(+)
 create mode 100644 techlibs/common/choices/han-carlson.v

diff --git a/techlibs/common/Makefile.inc b/techlibs/common/Makefile.inc
index fa5c2a825..cb67d6329 100644
--- a/techlibs/common/Makefile.inc
+++ b/techlibs/common/Makefile.inc
@@ -36,3 +36,4 @@ $(eval $(call add_share_file,share,techlibs/common/abc9_unmap.v))
 $(eval $(call add_share_file,share,techlibs/common/cmp2lcu.v))
 $(eval $(call add_share_file,share,techlibs/common/cmp2softlogic.v))
 $(eval $(call add_share_file,share/choices,techlibs/common/choices/kogge-stone.v))
+$(eval $(call add_share_file,share/choices,techlibs/common/choices/han-carlson.v))
diff --git a/techlibs/common/choices/han-carlson.v b/techlibs/common/choices/han-carlson.v
new file mode 100644
index 000000000..4c93c6f7e
--- /dev/null
+++ b/techlibs/common/choices/han-carlson.v
@@ -0,0 +1,57 @@
+(* techmap_celltype = "$lcu" *)
+module _85_lcu_han_carlson (P, G, CI, CO);
+	parameter WIDTH = 2;
+
+	(* force_downto *)
+	input [WIDTH-1:0] P, G;
+	input CI;
+
+	(* force_downto *)
+	output [WIDTH-1:0] CO;
+
+	integer i, j;
+	(* force_downto *)
+	reg [WIDTH-1:0] p, g;
+
+	always @* begin
+		i = 0;
+		p = P;
+		g = G;
+
+		// in almost all cases CI will be constant zero
+		g[0] = g[0] | (p[0] & CI);
+		if (i < $clog2(WIDTH)) begin
+
+			// First layer: BK
+			for (j = WIDTH - 1; j >= 0; j = j - 1) begin
+				if (j % 2 == 1) begin
+					g[j] = g[j] | p[j] & g[j - 1];
+					p[j] = p[j] & p[j - 1];
+				end
+			end
+
+			// Inner (log(WIDTH) - 1) layers: KS
+			for (i = 1; i < $clog2(WIDTH); i = i + 1) begin
+				for (j = WIDTH - 1; j >= 2**i; j = j - 1) begin
+					if (j % 2 == 1) begin
+						g[j] = g[j] | p[j] & g[j - 2**i];
+						p[j] = p[j] & p[j - 2**i];
+					end
+				end
+			end
+
+			// Last layer: BK
+			if (i < ($clog2(WIDTH) + 1)) begin
+				for (j = WIDTH - 1; j >= 0; j = j - 1) begin
+					if ((j % 2 == 0) && (j > 0)) begin
+						g[j] = g[j] | p[j] & g[j - 1];
+						p[j] = p[j] & p[j - 1];
+					end
+				end
+			end
+
+		end
+	end
+
+	assign CO = g;
+endmodule

From 289673a807817692489243355588639bdaba46e9 Mon Sep 17 00:00:00 2001
From: "Emil J. Tywoniak" <emil@tywoniak.eu>
Date: Thu, 28 Nov 2024 15:14:15 +0100
Subject: [PATCH 2/8] tests: add support for tcl tests

---
 tests/gen-tests-makefile.sh | 19 ++++++++++++++++++-
 1 file changed, 18 insertions(+), 1 deletion(-)

diff --git a/tests/gen-tests-makefile.sh b/tests/gen-tests-makefile.sh
index 2b26d8c98..b997fa12d 100755
--- a/tests/gen-tests-makefile.sh
+++ b/tests/gen-tests-makefile.sh
@@ -20,6 +20,13 @@ generate_ys_test() {
 	generate_target "$ys_file" "\"$YOSYS_BASEDIR/yosys\" -ql ${ys_file%.*}.log $yosys_args_ $ys_file"
 }
 
+# $ generate_tcl_test tcl_file [yosys_args]
+generate_tcl_test() {
+	tcl_file=$1
+	yosys_args_=${2:-}
+	generate_target "$tcl_file" "\"$YOSYS_BASEDIR/yosys\" -ql ${tcl_file%.*}.log $yosys_args_ $tcl_file"
+}
+
 # $ generate_bash_test bash_file
 generate_bash_test() {
 	bash_file=$1
@@ -29,6 +36,7 @@ generate_bash_test() {
 # $ generate_tests [-y|--yosys-scripts] [-s|--prove-sv] [-b|--bash] [-a|--yosys-args yosys_args]
 generate_tests() {
 	do_ys=false
+	do_tcl=false
 	do_sv=false
 	do_sh=false
 	yosys_args=""
@@ -40,6 +48,10 @@ generate_tests() {
 				do_ys=true
 				shift
 				;;
+			-t|--tcl-scripts)
+				do_tcl=true
+				shift
+				;;
 			-s|--prove-sv)
 				do_sv=true
 				shift
@@ -59,7 +71,7 @@ generate_tests() {
 		esac
 	done
 
-	if [[ ! ( $do_ys = true || $do_sv = true || $do_sh = true ) ]]; then
+	if [[ ! ( $do_ys = true || $do_tcl = true || $do_sv = true || $do_sh = true ) ]]; then
 		echo >&2 "Error: No file types selected"
 		exit 1
 	fi
@@ -72,6 +84,11 @@ generate_tests() {
 			generate_ys_test "$x" "$yosys_args"
 		done
 	fi;
+	if [[ $do_tcl = true ]]; then
+		for x in *.tcl; do
+			generate_tcl_test "$x" "$yosys_args"
+		done
+	fi;
 	if [[ $do_sv = true ]]; then
 		for x in *.sv; do
 			if [ ! -f "${x%.sv}.ys"  ]; then

From 1a562f9605aa689f634e3c8c5ed0b7ec2d82352c Mon Sep 17 00:00:00 2001
From: "Emil J. Tywoniak" <emil@tywoniak.eu>
Date: Thu, 28 Nov 2024 15:16:48 +0100
Subject: [PATCH 3/8] techmap: add TCL test for Han-Carlson adder

---
 tests/techmap/han-carlson.nomatch |  2 ++
 tests/techmap/han-carlson.tcl     | 14 ++++++++++++++
 tests/techmap/lcu_refined.v       | 20 ++++++++++++++++++++
 tests/techmap/run-test.sh         |  2 +-
 4 files changed, 37 insertions(+), 1 deletion(-)
 create mode 100644 tests/techmap/han-carlson.nomatch
 create mode 100644 tests/techmap/han-carlson.tcl
 create mode 100644 tests/techmap/lcu_refined.v

diff --git a/tests/techmap/han-carlson.nomatch b/tests/techmap/han-carlson.nomatch
new file mode 100644
index 000000000..142d509b3
--- /dev/null
+++ b/tests/techmap/han-carlson.nomatch
@@ -0,0 +1,2 @@
+i
+j
\ No newline at end of file
diff --git a/tests/techmap/han-carlson.tcl b/tests/techmap/han-carlson.tcl
new file mode 100644
index 000000000..114ebe4dc
--- /dev/null
+++ b/tests/techmap/han-carlson.tcl
@@ -0,0 +1,14 @@
+yosys -import
+
+read_verilog +/choices/han-carlson.v
+read_verilog lcu_refined.v
+design -save init
+
+for {set i 1} {$i <= 16} {incr i} {
+    design -load init
+    chparam -set WIDTH $i
+    yosys proc
+    equiv_make -blacklist han-carlson.nomatch lcu _85_lcu_han_carlson equiv
+    equiv_simple equiv
+    equiv_status -assert equiv
+}
diff --git a/tests/techmap/lcu_refined.v b/tests/techmap/lcu_refined.v
new file mode 100644
index 000000000..9187f68fe
--- /dev/null
+++ b/tests/techmap/lcu_refined.v
@@ -0,0 +1,20 @@
+// Copied from techlibs/common/simlib.v
+// with this condition removed: (^{P, G, CI} !== 1'bx)
+module lcu (P, G, CI, CO);
+
+parameter WIDTH = 2;
+
+input [WIDTH-1:0] P;    // Propagate
+input [WIDTH-1:0] G;    // Generate
+input CI;               // Carry-in
+
+output reg [WIDTH-1:0] CO; // Carry-out
+
+integer i;
+always @* begin
+	CO[0] = G[0] || (P[0] && CI);
+	for (i = 1; i < WIDTH; i = i+1)
+		CO[i] = G[i] || (P[i] && CO[i-1]);
+end
+
+endmodule
diff --git a/tests/techmap/run-test.sh b/tests/techmap/run-test.sh
index 581847ab0..16741cace 100755
--- a/tests/techmap/run-test.sh
+++ b/tests/techmap/run-test.sh
@@ -1,4 +1,4 @@
 #!/usr/bin/env bash
 set -eu
 source ../gen-tests-makefile.sh
-run_tests --yosys-scripts --bash --yosys-args "-e 'select out of bounds'"
+run_tests --yosys-scripts --tcl-scripts --bash --yosys-args "-e 'select out of bounds'"

From 3f078d9afa464e3495fb657084beaf53d95a5297 Mon Sep 17 00:00:00 2001
From: "Emil J. Tywoniak" <emil@tywoniak.eu>
Date: Thu, 28 Nov 2024 15:19:15 +0100
Subject: [PATCH 4/8] tests: rework Kogge-Stone test consistently with
 Han-Carlson

---
 tests/techmap/han-carlson.tcl                      |  2 +-
 tests/techmap/kogge-stone.tcl                      | 14 ++++++++++++++
 tests/techmap/kogge-stone.ys                       |  1 -
 tests/techmap/{han-carlson.nomatch => ppa.nomatch} |  2 +-
 4 files changed, 16 insertions(+), 3 deletions(-)
 create mode 100644 tests/techmap/kogge-stone.tcl
 delete mode 100644 tests/techmap/kogge-stone.ys
 rename tests/techmap/{han-carlson.nomatch => ppa.nomatch} (50%)

diff --git a/tests/techmap/han-carlson.tcl b/tests/techmap/han-carlson.tcl
index 114ebe4dc..0b5460be8 100644
--- a/tests/techmap/han-carlson.tcl
+++ b/tests/techmap/han-carlson.tcl
@@ -8,7 +8,7 @@ for {set i 1} {$i <= 16} {incr i} {
     design -load init
     chparam -set WIDTH $i
     yosys proc
-    equiv_make -blacklist han-carlson.nomatch lcu _85_lcu_han_carlson equiv
+    equiv_make -blacklist ppa.nomatch lcu _85_lcu_han_carlson equiv
     equiv_simple equiv
     equiv_status -assert equiv
 }
diff --git a/tests/techmap/kogge-stone.tcl b/tests/techmap/kogge-stone.tcl
new file mode 100644
index 000000000..e5f4e812c
--- /dev/null
+++ b/tests/techmap/kogge-stone.tcl
@@ -0,0 +1,14 @@
+yosys -import
+
+read_verilog +/choices/kogge-stone.v
+read_verilog lcu_refined.v
+design -save init
+
+for {set i 1} {$i <= 16} {incr i} {
+    design -load init
+    chparam -set WIDTH $i
+    yosys proc
+    equiv_make -blacklist ppa.nomatch lcu _80_lcu_kogge_stone equiv
+    equiv_simple equiv
+    equiv_status -assert equiv
+}
diff --git a/tests/techmap/kogge-stone.ys b/tests/techmap/kogge-stone.ys
deleted file mode 100644
index fc3637f10..000000000
--- a/tests/techmap/kogge-stone.ys
+++ /dev/null
@@ -1 +0,0 @@
-test_cell -s 1711533949 -n 10 -map +/techmap.v -map +/choices/kogge-stone.v $lcu
diff --git a/tests/techmap/han-carlson.nomatch b/tests/techmap/ppa.nomatch
similarity index 50%
rename from tests/techmap/han-carlson.nomatch
rename to tests/techmap/ppa.nomatch
index 142d509b3..7388135e1 100644
--- a/tests/techmap/han-carlson.nomatch
+++ b/tests/techmap/ppa.nomatch
@@ -1,2 +1,2 @@
 i
-j
\ No newline at end of file
+j

From 4bf3677640eac18b5afd2df63f11c56659194a9c Mon Sep 17 00:00:00 2001
From: "Emil J. Tywoniak" <emil@tywoniak.eu>
Date: Thu, 28 Nov 2024 23:54:00 +0100
Subject: [PATCH 5/8] techmap: set Han-Carlson adder priority consistent with
 Kogge-Stone

---
 techlibs/common/choices/han-carlson.v | 2 +-
 tests/techmap/han-carlson.tcl         | 2 +-
 2 files changed, 2 insertions(+), 2 deletions(-)

diff --git a/techlibs/common/choices/han-carlson.v b/techlibs/common/choices/han-carlson.v
index 4c93c6f7e..2ddcf75e9 100644
--- a/techlibs/common/choices/han-carlson.v
+++ b/techlibs/common/choices/han-carlson.v
@@ -1,5 +1,5 @@
 (* techmap_celltype = "$lcu" *)
-module _85_lcu_han_carlson (P, G, CI, CO);
+module _80_lcu_han_carlson (P, G, CI, CO);
 	parameter WIDTH = 2;
 
 	(* force_downto *)
diff --git a/tests/techmap/han-carlson.tcl b/tests/techmap/han-carlson.tcl
index 0b5460be8..56a671ae6 100644
--- a/tests/techmap/han-carlson.tcl
+++ b/tests/techmap/han-carlson.tcl
@@ -8,7 +8,7 @@ for {set i 1} {$i <= 16} {incr i} {
     design -load init
     chparam -set WIDTH $i
     yosys proc
-    equiv_make -blacklist ppa.nomatch lcu _85_lcu_han_carlson equiv
+    equiv_make -blacklist ppa.nomatch lcu _80_lcu_han_carlson equiv
     equiv_simple equiv
     equiv_status -assert equiv
 }

From a41ef0271ce922a9a945e5c97a65ca68b8a2df22 Mon Sep 17 00:00:00 2001
From: "Emil J. Tywoniak" <emil@tywoniak.eu>
Date: Fri, 29 Nov 2024 00:03:49 +0100
Subject: [PATCH 6/8] techmap: remove ppa.nomatch by purging internal signals

---
 tests/techmap/han-carlson.tcl | 3 ++-
 tests/techmap/kogge-stone.tcl | 3 ++-
 tests/techmap/ppa.nomatch     | 2 --
 3 files changed, 4 insertions(+), 4 deletions(-)
 delete mode 100644 tests/techmap/ppa.nomatch

diff --git a/tests/techmap/han-carlson.tcl b/tests/techmap/han-carlson.tcl
index 56a671ae6..3d32c7e02 100644
--- a/tests/techmap/han-carlson.tcl
+++ b/tests/techmap/han-carlson.tcl
@@ -8,7 +8,8 @@ for {set i 1} {$i <= 16} {incr i} {
     design -load init
     chparam -set WIDTH $i
     yosys proc
-    equiv_make -blacklist ppa.nomatch lcu _80_lcu_han_carlson equiv
+    opt_clean -purge
+    equiv_make lcu _80_lcu_han_carlson equiv
     equiv_simple equiv
     equiv_status -assert equiv
 }
diff --git a/tests/techmap/kogge-stone.tcl b/tests/techmap/kogge-stone.tcl
index e5f4e812c..243706284 100644
--- a/tests/techmap/kogge-stone.tcl
+++ b/tests/techmap/kogge-stone.tcl
@@ -8,7 +8,8 @@ for {set i 1} {$i <= 16} {incr i} {
     design -load init
     chparam -set WIDTH $i
     yosys proc
-    equiv_make -blacklist ppa.nomatch lcu _80_lcu_kogge_stone equiv
+    opt_clean -purge
+    equiv_make lcu _80_lcu_kogge_stone equiv
     equiv_simple equiv
     equiv_status -assert equiv
 }
diff --git a/tests/techmap/ppa.nomatch b/tests/techmap/ppa.nomatch
deleted file mode 100644
index 7388135e1..000000000
--- a/tests/techmap/ppa.nomatch
+++ /dev/null
@@ -1,2 +0,0 @@
-i
-j

From 91844968fd7565c4e31ce127b75730864e2331e2 Mon Sep 17 00:00:00 2001
From: "Emil J. Tywoniak" <emil@tywoniak.eu>
Date: Fri, 29 Nov 2024 00:13:21 +0100
Subject: [PATCH 7/8] techmap: wrap builtin $lcu as golden module in PPA tests

---
 tests/techmap/han-carlson.tcl |  2 +-
 tests/techmap/kogge-stone.tcl |  2 +-
 tests/techmap/lcu_refined.v   | 19 ++++++-------------
 3 files changed, 8 insertions(+), 15 deletions(-)

diff --git a/tests/techmap/han-carlson.tcl b/tests/techmap/han-carlson.tcl
index 3d32c7e02..7029be57f 100644
--- a/tests/techmap/han-carlson.tcl
+++ b/tests/techmap/han-carlson.tcl
@@ -1,7 +1,7 @@
 yosys -import
 
 read_verilog +/choices/han-carlson.v
-read_verilog lcu_refined.v
+read_verilog -icells lcu_refined.v
 design -save init
 
 for {set i 1} {$i <= 16} {incr i} {
diff --git a/tests/techmap/kogge-stone.tcl b/tests/techmap/kogge-stone.tcl
index 243706284..b6a4ef54e 100644
--- a/tests/techmap/kogge-stone.tcl
+++ b/tests/techmap/kogge-stone.tcl
@@ -1,7 +1,7 @@
 yosys -import
 
 read_verilog +/choices/kogge-stone.v
-read_verilog lcu_refined.v
+read_verilog -icells lcu_refined.v
 design -save init
 
 for {set i 1} {$i <= 16} {incr i} {
diff --git a/tests/techmap/lcu_refined.v b/tests/techmap/lcu_refined.v
index 9187f68fe..e0747f3f2 100644
--- a/tests/techmap/lcu_refined.v
+++ b/tests/techmap/lcu_refined.v
@@ -1,20 +1,13 @@
-// Copied from techlibs/common/simlib.v
-// with this condition removed: (^{P, G, CI} !== 1'bx)
 module lcu (P, G, CI, CO);
+	parameter WIDTH = 2;
 
-parameter WIDTH = 2;
+	input [WIDTH-1:0] P, G;
+	input CI;
 
-input [WIDTH-1:0] P;    // Propagate
-input [WIDTH-1:0] G;    // Generate
-input CI;               // Carry-in
+	output [WIDTH-1:0] CO;
 
-output reg [WIDTH-1:0] CO; // Carry-out
+	reg [WIDTH-1:0] p, g;
 
-integer i;
-always @* begin
-	CO[0] = G[0] || (P[0] && CI);
-	for (i = 1; i < WIDTH; i = i+1)
-		CO[i] = G[i] || (P[i] && CO[i-1]);
-end
+	\$lcu #(.WIDTH(WIDTH)) impl (.P(P), .G(G), .CI(CI), .CO(CO));
 
 endmodule

From 3ebc714dbc6a3247edd08ed9828d3ea56c2d3641 Mon Sep 17 00:00:00 2001
From: "Emil J. Tywoniak" <emil@tywoniak.eu>
Date: Fri, 29 Nov 2024 00:15:02 +0100
Subject: [PATCH 8/8] techmap: test consistently with other equiv_make tests

---
 tests/techmap/han-carlson.tcl | 2 +-
 tests/techmap/kogge-stone.tcl | 2 +-
 2 files changed, 2 insertions(+), 2 deletions(-)

diff --git a/tests/techmap/han-carlson.tcl b/tests/techmap/han-carlson.tcl
index 7029be57f..0d9068b5e 100644
--- a/tests/techmap/han-carlson.tcl
+++ b/tests/techmap/han-carlson.tcl
@@ -8,7 +8,7 @@ for {set i 1} {$i <= 16} {incr i} {
     design -load init
     chparam -set WIDTH $i
     yosys proc
-    opt_clean -purge
+    opt_clean
     equiv_make lcu _80_lcu_han_carlson equiv
     equiv_simple equiv
     equiv_status -assert equiv
diff --git a/tests/techmap/kogge-stone.tcl b/tests/techmap/kogge-stone.tcl
index b6a4ef54e..1209b1338 100644
--- a/tests/techmap/kogge-stone.tcl
+++ b/tests/techmap/kogge-stone.tcl
@@ -8,7 +8,7 @@ for {set i 1} {$i <= 16} {incr i} {
     design -load init
     chparam -set WIDTH $i
     yosys proc
-    opt_clean -purge
+    opt_clean
     equiv_make lcu _80_lcu_kogge_stone equiv
     equiv_simple equiv
     equiv_status -assert equiv