From 3e621b02e940b1d5a5e7779561878b0d5792dcb6 Mon Sep 17 00:00:00 2001
From: tmeissner <programming@goodcleanfun.de>
Date: Mon, 24 Feb 2020 11:21:44 +0100
Subject: [PATCH] Add alu checks

* Add asserts for correct behaviour of Overflow flag
* Switch to smtbmc engine in prove mode (much faster than abc)
---
 alu/alu.vhd        | 34 +++++++++++++++++++++++++++++-----
 alu/symbiyosys.sby |  4 ++--
 2 files changed, 31 insertions(+), 7 deletions(-)

diff --git a/alu/alu.vhd b/alu/alu.vhd
index e9aac0d..7b701b0 100644
--- a/alu/alu.vhd
+++ b/alu/alu.vhd
@@ -66,6 +66,15 @@ begin
     signal s_dina : std_logic_vector(DinA_i'range);
     signal s_dinb : std_logic_vector(DinB_i'range);
 
+    function max(a, b: std_logic_vector) return unsigned is
+    begin
+      if unsigned(a) > unsigned(b) then
+        return unsigned(a);
+      else
+        return unsigned(b);
+      end if;
+    end function max;
+
   begin
 
     -- VHDL helper logic
@@ -80,16 +89,31 @@ begin
     default clock is rising_edge(Clk_i);
 
     AFTER_RESET : assert always
-      not Reset_n_i -> Dout_o = x"00" and OverFlow_o = '0';
+      not Reset_n_i -> Dout_o = (Dout_o'range => '0') and OverFlow_o = '0';
+
+    ADD_OP : assert Reset_n_i and Opc_i = c_add ->
+      next unsigned(Dout_o) = unsigned(s_dina) + unsigned(s_dinb) abort not Reset_n_i;
+
+    SUB_OP : assert Reset_n_i and Opc_i = c_sub ->
+      next unsigned(Dout_o) = unsigned(s_dina) - unsigned(s_dinb) abort not Reset_n_i;
+
+    AND_OP : assert Reset_n_i and Opc_i = c_and ->
+      next Dout_o = (s_dina and s_dinb) abort not Reset_n_i;
 
+    OR_OP :  assert Reset_n_i and Opc_i = c_or ->
+      next Dout_o = (s_dina or s_dinb) abort not Reset_n_i;
 
-    ADD_OP : assert Reset_n_i and Opc_i = c_add -> next unsigned(Dout_o) = unsigned(s_dina) + unsigned(s_dinb) abort not Reset_n_i;
+    OVERFLOW_ADD : assert Reset_n_i and Opc_i = c_add and (unsigned(DinA_i) + unsigned(DinB_i)) < max(DinA_i, DinB_i) ->
+      next OverFlow_o abort not Reset_n_i;
 
-    SUB_OP : assert Reset_n_i and Opc_i = c_sub -> next unsigned(Dout_o) = unsigned(s_dina) - unsigned(s_dinb) abort not Reset_n_i;
+    NOT_OVERFLOW_ADD : assert Reset_n_i and Opc_i = c_add and (unsigned(DinA_i) + unsigned(DinB_i)) >= max(DinA_i, DinB_i) ->
+      next not OverFlow_o abort not Reset_n_i;
 
-    AND_OP : assert Reset_n_i and Opc_i = c_and -> next Dout_o = (s_dina and s_dinb) abort not Reset_n_i;
+    OVERFLOW_SUB : assert Reset_n_i and Opc_i = c_sub and (unsigned(DinA_i) - unsigned(DinB_i)) > unsigned(DinA_i) ->
+      next OverFlow_o abort not Reset_n_i;
 
-    OR_OP :  assert Reset_n_i and Opc_i = c_or  -> next Dout_o = (s_dina or s_dinb) abort not Reset_n_i;
+    NOT_OVERFLOW_SUB : assert Reset_n_i and Opc_i = c_sub and (unsigned(DinA_i) - unsigned(DinB_i)) <= unsigned(DinA_i) ->
+      next not OverFlow_o abort not Reset_n_i;
 
   end generate FormalG;
 
diff --git a/alu/symbiyosys.sby b/alu/symbiyosys.sby
index 3aed69d..f3f73d4 100644
--- a/alu/symbiyosys.sby
+++ b/alu/symbiyosys.sby
@@ -12,10 +12,10 @@ prove: mode prove
 [engines]
 cover: smtbmc z3
 bmc: abc bmc3
-prove: abc pdr
+prove: smtbmc z3
 
 [script]
-ghdl --std=08 -fpsl alu.vhd -e alu
+ghdl --std=08 -gWidth=16 -gFormal=true alu.vhd -e alu
 prep -auto-top
 
 [files]