3 files changed, 0 insertions, 59 deletions
diff --git a/testsuite/formal/abs/test_abs.sby b/testsuite/formal/abs/test_abs.sby
deleted file mode 100644
index 0e4bc7c..0000000
--- a/testsuite/formal/abs/test_abs.sby
+++ /dev/null
@@ -1,13 +0,0 @@
-[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
deleted file mode 100644
index 3e711b2..0000000
--- a/testsuite/formal/abs/test_abs.vhd
+++ /dev/null
@@ -1,37 +0,0 @@
-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
deleted file mode 100755
index 10ec36d..0000000
--- a/testsuite/formal/abs/testsuite.sh
+++ /dev/null
@@ -1,9 +0,0 @@
-#!/bin/sh
-
-topdir=../..
-. $topdir/testenv.sh
-
-formal "test_abs"
-
-clean
-echo OK