Add abs gate (#91)

5 files changed, 69 insertions, 0 deletions

diff --git a/.gitignore b/.gitignore
index 3e4a084..2929063 100644
--- a/.gitignore
+++ b/.gitignore
@@ -8,3 +8,4 @@
 *.o
 *.so
 
+testsuite/**/work/
diff --git a/src/ghdl.cc b/src/ghdl.cc
index 18facfe..9322ad8 100644
--- a/src/ghdl.cc
+++ b/src/ghdl.cc
@@ -557,6 +557,7 @@ static void import_module(RTLIL::Design *design, GhdlSynth::Module m)
 		case Id_Sgt:
 		case Id_Sge:
 		case Id_Not:
+		case Id_Abs:
 		case Id_Red_Or:
 		case Id_Red_And:
 		case Id_Lsr:
@@ -679,6 +680,14 @@ static void import_module(RTLIL::Design *design, GhdlSynth::Module m)
 		case Id_Not:
 			module->addNot(to_str(iname), IN(0), OUT(0));
 			break;
+		case Id_Abs:
+			{
+				SigSpec isNegative = IN(0).extract(IN(0).size() - 1, 1);
+				RTLIL::Wire *negated = module->addWire(NEW_ID, IN(0).size());
+				module->addNeg(NEW_ID, IN(0), negated);
+				module->addMux(NEW_ID, IN(0), negated, isNegative, OUT(0));
+			}
+			break;
 		case Id_Eq:
 			module->addEq(to_str(iname), IN(0), IN(1), OUT(0));
 			break;
diff --git a/testsuite/formal/abs/test_abs.sby b/testsuite/formal/abs/test_abs.sby
new file mode 100644
index 0000000..0e4bc7c
--- /dev/null
+++ b/testsuite/formal/abs/test_abs.sby
@@ -0,0 +1,13 @@
+[options]
+#depth 6
+mode prove
+
+[engines]
+smtbmc z3
+
+[script]
+ghdl --std=08 test_abs.vhd -e ent
+prep -top ent
+
+[files]
+test_abs.vhd
diff --git a/testsuite/formal/abs/test_abs.vhd b/testsuite/formal/abs/test_abs.vhd
new file mode 100644
index 0000000..3e711b2
--- /dev/null
+++ b/testsuite/formal/abs/test_abs.vhd
@@ -0,0 +1,37 @@
+library ieee;
+use ieee.std_logic_1164.all;
+use ieee.numeric_std.all;
+
+entity ent is
+	port (
+		clk : in std_logic;
+		a : in signed(7 downto 0);
+		b : out signed(7 downto 0)
+	);
+end;
+
+architecture a of ent is
+begin
+	process(clk)
+	begin
+		if rising_edge(clk) then
+			b <= abs a;
+		end if;
+	end process;
+
+	formal: block
+		signal last_a : signed(7 downto 0);
+		signal has_run : std_logic := '0';
+	begin
+		process(clk)
+		begin
+			if rising_edge(clk) then
+				has_run <= '1';
+				last_a <= a;
+			end if;
+		end process;
+
+		default clock is rising_edge(clk);
+		assert always has_run -> b >= 0 or (last_a = x"80" and last_a = b);
+	end block;
+end;
diff --git a/testsuite/formal/abs/testsuite.sh b/testsuite/formal/abs/testsuite.sh
new file mode 100755
index 0000000..10ec36d
--- /dev/null
+++ b/testsuite/formal/abs/testsuite.sh
@@ -0,0 +1,9 @@
+#!/bin/sh
+
+topdir=../..
+. $topdir/testenv.sh
+
+formal "test_abs"
+
+clean
+echo OK