Add formal test for pmux gate

3 files changed, 59 insertions, 1 deletions

diff --git a/testsuite/formal/gates/test_pmux.sby b/testsuite/formal/gates/test_pmux.sby
new file mode 100644
index 0000000..c35817a
--- /dev/null
+++ b/testsuite/formal/gates/test_pmux.sby
@@ -0,0 +1,12 @@
+[options]
+mode prove
+
+[engines]
+smtbmc z3
+
+[script]
+ghdl --std=08 test_pmux.vhd -e ent
+prep -top ent
+
+[files]
+test_pmux.vhd
diff --git a/testsuite/formal/gates/test_pmux.vhd b/testsuite/formal/gates/test_pmux.vhd
new file mode 100644
index 0000000..b3901f4
--- /dev/null
+++ b/testsuite/formal/gates/test_pmux.vhd
@@ -0,0 +1,46 @@
+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(1 downto 0);
+		b : out std_logic_vector(1 downto 0)
+	);
+end entity;
+
+architecture a of ent is
+begin
+	process(clk)
+	begin
+		if rising_edge(clk) then
+			case a is
+				when "00" =>
+					b <= "01";
+				when "01" =>
+					b <= "10";
+				when "11" =>
+					b <= "00";
+				when others =>
+					b <= "11";
+			end case;
+		end if;
+	end process;
+
+	formal: block
+		signal has_run : std_logic := '0';
+		signal prev_a : std_logic_vector(1 downto 0);
+	begin
+		process(clk)
+		begin
+			if rising_edge(clk) then
+				prev_a <= a;
+				has_run <= '1';
+			end if;
+		end process;
+
+		default clock is rising_edge(clk);
+		assert always has_run -> unsigned(prev_a) + 1 = unsigned(b);
+	end block;
+end architecture;
diff --git a/testsuite/formal/gates/testsuite.sh b/testsuite/formal/gates/testsuite.sh
index d4bcf98..e74df99 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 minmax lsl lsr asr; do
+for f in abs minmax pmux lsl lsr asr; do
   formal "test_${f}"
 done