From c975230114caebe442e0ec403796771caf70925d Mon Sep 17 00:00:00 2001
From: Xiretza <xiretza@xiretza.xyz>
Date: Sat, 21 Mar 2020 20:51:03 +0100
Subject: Add min/max gates

---
 src/ghdl.cc                            | 21 +++++++++++++
 testsuite/formal/gates/test_minmax.sby | 12 +++++++
 testsuite/formal/gates/test_minmax.vhd | 57 ++++++++++++++++++++++++++++++++++
 testsuite/formal/gates/testsuite.sh    |  2 +-
 4 files changed, 91 insertions(+), 1 deletion(-)
 create mode 100644 testsuite/formal/gates/test_minmax.sby
 create mode 100644 testsuite/formal/gates/test_minmax.vhd

diff --git a/src/ghdl.cc b/src/ghdl.cc
index 9322ad8..28107d4 100644
--- a/src/ghdl.cc
+++ b/src/ghdl.cc
@@ -563,6 +563,10 @@ static void import_module(RTLIL::Design *design, GhdlSynth::Module m)
 		case Id_Lsr:
 		case Id_Lsl:
 		case Id_Asr:
+		case Id_Smin:
+		case Id_Umin:
+		case Id_Smax:
+		case Id_Umax:
 		case Id_Smul:
 		case Id_Umul:
 		case Id_Sdiv:
@@ -733,6 +737,23 @@ static void import_module(RTLIL::Design *design, GhdlSynth::Module m)
 		case Id_Asr:
 			module->addSshr(to_str(iname), IN(0), IN(1), OUT(0), true);
 			break;
+		case Id_Smin:
+		case Id_Umin:
+		case Id_Smax:
+		case Id_Umax:
+			{
+				bool is_signed = (id == Id_Smin || id == Id_Smax);
+
+				RTLIL::Wire *select_rhs = module->addWire(NEW_ID);
+				if (id == Id_Smin || id == Id_Umin) {
+					module->addGt(NEW_ID, IN(0), IN(1), select_rhs, is_signed);
+				} else {
+					module->addLt(NEW_ID, IN(0), IN(1), select_rhs, is_signed);
+				}
+
+				module->addMux(to_str(iname), IN(0), IN(1), select_rhs, OUT(0));
+			}
+			break;
 		case Id_Smul:
 			module->addMul(to_str(iname), IN(0), IN(1), OUT(0), true);
 			break;
diff --git a/testsuite/formal/gates/test_minmax.sby b/testsuite/formal/gates/test_minmax.sby
new file mode 100644
index 0000000..c7d103a
--- /dev/null
+++ b/testsuite/formal/gates/test_minmax.sby
@@ -0,0 +1,12 @@
+[options]
+mode prove
+
+[engines]
+smtbmc z3
+
+[script]
+ghdl --std=08 test_minmax.vhd -e ent
+prep -top ent
+
+[files]
+test_minmax.vhd
diff --git a/testsuite/formal/gates/test_minmax.vhd b/testsuite/formal/gates/test_minmax.vhd
new file mode 100644
index 0000000..8cd760c
--- /dev/null
+++ b/testsuite/formal/gates/test_minmax.vhd
@@ -0,0 +1,57 @@
+library ieee;
+use ieee.std_logic_1164.all;
+use ieee.numeric_std.all;
+
+entity ent is
+	port (
+		clk : in std_logic;
+		a : in std_logic_vector(7 downto 0);
+		b : in std_logic_vector(7 downto 0);
+		min_sgn : out signed(7 downto 0);
+		max_sgn : out signed(7 downto 0);
+		min_uns : out unsigned(7 downto 0);
+		max_uns : out unsigned(7 downto 0)
+	);
+end;
+
+architecture a of ent is
+begin
+	process(clk)
+	begin
+		if rising_edge(clk) then
+			min_sgn <= minimum(signed(a), signed(b));
+			max_sgn <= maximum(signed(a), signed(b));
+
+			min_uns <= minimum(unsigned(a), unsigned(b));
+			max_uns <= maximum(unsigned(a), unsigned(b));
+		end if;
+	end process;
+
+	formal: block
+		signal prev_a : std_logic_vector(7 downto 0);
+		signal prev_b : std_logic_vector(7 downto 0);
+		signal has_run : std_logic := '0';
+	begin
+		process(clk)
+		begin
+			if rising_edge(clk) then
+				has_run <= '1';
+				prev_a <= a;
+				prev_b <= b;
+			end if;
+		end process;
+
+		default clock is rising_edge(clk);
+		assert eventually! has_run;
+
+		assert always has_run and signed(prev_a) <= signed(prev_b) ->
+			min_sgn = signed(prev_a) and max_sgn = signed(prev_b);
+		assert always has_run and signed(prev_a) >= signed(prev_b) ->
+			min_sgn = signed(prev_b) and max_sgn = signed(prev_a);
+
+		assert always has_run and unsigned(prev_a) <= unsigned(prev_b) ->
+			min_uns = unsigned(prev_a) and max_uns = unsigned(prev_b);
+		assert always has_run and unsigned(prev_a) >= unsigned(prev_b) ->
+			min_uns = unsigned(prev_b) and max_uns = unsigned(prev_a);
+	end block;
+end;
diff --git a/testsuite/formal/gates/testsuite.sh b/testsuite/formal/gates/testsuite.sh
index 7986d8c..d4bcf98 100755
--- a/testsuite/formal/gates/testsuite.sh
+++ b/testsuite/formal/gates/testsuite.sh
@@ -3,7 +3,7 @@
 topdir=../..
 . $topdir/testenv.sh
 
-for f in abs lsl lsr asr; do
+for f in abs minmax lsl lsr asr; do
   formal "test_${f}"
 done
 
-- 
cgit v1.2.3