From 0f96ae599037a945967070211676e32d6e50714d Mon Sep 17 00:00:00 2001
From: Jannis Harder <me@jix.one>
Date: Thu, 20 Oct 2022 15:41:17 +0200
Subject: [PATCH] Add smtmap.v describing the smt2 backend's behavior for undef
 bits

Some builtin cells have an undefined (x) output even when all inputs are
defined. This is not natively supported by the formal backends which
will produce a fully defined value instead. This can lead to issues when
combining different backends in a formal flow. To work around these,
this adds a file containing verilog implementation of cells matching the
fully defined behavior implemented by the smt2 backend.
---
 techlibs/common/Makefile.inc |  1 +
 techlibs/common/smtmap.v     | 28 ++++++++++++++++++++++++++++
 2 files changed, 29 insertions(+)
 create mode 100644 techlibs/common/smtmap.v

diff --git a/techlibs/common/Makefile.inc b/techlibs/common/Makefile.inc
index 607e772a2..47f1ed604 100644
--- a/techlibs/common/Makefile.inc
+++ b/techlibs/common/Makefile.inc
@@ -22,6 +22,7 @@ kernel/register.o: techlibs/common/simlib_help.inc techlibs/common/simcells_help
 $(eval $(call add_share_file,share,techlibs/common/simlib.v))
 $(eval $(call add_share_file,share,techlibs/common/simcells.v))
 $(eval $(call add_share_file,share,techlibs/common/techmap.v))
+$(eval $(call add_share_file,share,techlibs/common/smtmap.v))
 $(eval $(call add_share_file,share,techlibs/common/pmux2mux.v))
 $(eval $(call add_share_file,share,techlibs/common/adff2dff.v))
 $(eval $(call add_share_file,share,techlibs/common/dff2ff.v))
diff --git a/techlibs/common/smtmap.v b/techlibs/common/smtmap.v
new file mode 100644
index 000000000..8c7503dc8
--- /dev/null
+++ b/techlibs/common/smtmap.v
@@ -0,0 +1,28 @@
+(* techmap_celltype = "$pmux" *)
+module smt_pmux (A, B, S, Y);
+	parameter WIDTH = 1;
+	parameter S_WIDTH = 1;
+
+	(* force_downto *)
+	input [WIDTH-1:0] A;
+	(* force_downto *)
+	input [WIDTH*S_WIDTH-1:0] B;
+	(* force_downto *)
+	input [S_WIDTH-1:0] S;
+	(* force_downto *)
+	output [WIDTH-1:0] Y;
+
+	(* force_downto *)
+	wire [WIDTH-1:0] Y_B;
+
+	genvar i, j;
+	generate
+		(* force_downto *)
+		wire [WIDTH*(S_WIDTH+1)-1:0] C;
+
+		assign C[WIDTH-1:0] = A;
+		for (i = 0; i < S_WIDTH; i = i + 1)
+			assign C[WIDTH*(i+2)-1:WIDTH*(i+1)] = S[i] ? B[WIDTH*(i+1)-1:WIDTH*i] : C[WIDTH*(i+1)-1:WIDTH*i];
+		assign Y = C[WIDTH*(S_WIDTH+1)-1:WIDTH*S_WIDTH];
+	endgenerate
+endmodule