From 77f87536c90908cff5a27330301f14c48c1d458b Mon Sep 17 00:00:00 2001
From: Torsten Meissner <programming@goodcleanfun.de>
Date: Tue, 12 Mar 2019 13:59:45 +0100
Subject: [PATCH] FSM optimizations; PSL enhancements

* Optimize setting of valid/data outputs to save
  one cycle
* Replace not working PSL stable assertion by
  seperate helper register and equal compare
---
 aes/rtl/vhdl/aes_dec.vhd | 46 ++++++++++++++++++++++++++++------------
 aes/rtl/vhdl/aes_enc.vhd | 44 +++++++++++++++++++++++++++-----------
 2 files changed, 65 insertions(+), 25 deletions(-)

diff --git a/aes/rtl/vhdl/aes_dec.vhd b/aes/rtl/vhdl/aes_dec.vhd
index 45bf366..bb8f8b4 100644
--- a/aes/rtl/vhdl/aes_dec.vhd
+++ b/aes/rtl/vhdl/aes_dec.vhd
@@ -108,19 +108,22 @@ begin
             v_state := addroundkey(v_state, s_round_key);
             s_round <= s_round + 1;
 
-          when t_rounds'high =>
+          when t_dec_rounds'high-1 =>
             v_state := invshiftrow(v_state);
             v_state := invsubbytes(v_state);
             v_state := addroundkey(v_state, s_round_key);
             s_round <= s_round + 1;
-
-          when t_rounds'high+1 =>
+            -- set data & valid to save one cycle
             valid_o <= '1';
             data_o  <= get_state(v_state);
+
+          when t_dec_rounds'high =>
             if (valid_o = '1' and accept_i = '1') then
               valid_o <= '0';
               data_o  <= (others => '0');
               s_round <= 0;
+              -- Set accept to save one cycle
+              accept_o <= '1';
             end if;
 
           when others =>
@@ -135,17 +138,34 @@ begin
     end process DeCryptP;
 
 
-    -- psl cover accept_o;
-    -- psl assert always (accept_o -> s_round = 0);
-    
-    -- psl cover valid_i and accept_o;
-    -- psl assert always (valid_i and accept_o -> next not accept_o);
-    
-    -- psl cover valid_o and accept_i;
-    -- psl assert always (valid_o and accept_i -> next not valid_o);
+    -- synthesis off
+    verification : block is
+
+      signal s_data : std_logic_vector(0 to 127);
+
+    begin
+
+      s_data <= data_o  when rising_edge(clk_i) else
+                128x"0" when reset_i = '0';
+
+      -- psl cover accept_o;
+      -- psl assert always (accept_o -> s_round = 0);
+
+      -- psl cover valid_i and accept_o;
+      -- psl assert always (valid_i and accept_o -> next not accept_o);
+
+      -- psl cover valid_o;
+      -- psl assert always (valid_o -> s_round = t_dec_rounds'high);
+
+      -- psl cover valid_o and accept_i;
+      -- psl assert always (valid_o and accept_i -> next not valid_o);
+
+      -- psl cover valid_o and not accept_i;
+      -- psl assert always (valid_o and not accept_i -> next valid_o);
+      -- psl assert always (valid_o and not accept_i -> next data_o = s_data);
 
-    -- psl cover valid_o and not accept_i;
-    -- psl assert always (valid_o and not accept_i -> next data_o'stable);
+    end block verification;
+    -- synthesis on
 
 
   end generate IterG;
diff --git a/aes/rtl/vhdl/aes_enc.vhd b/aes/rtl/vhdl/aes_enc.vhd
index d0a7823..22cc7b4 100644
--- a/aes/rtl/vhdl/aes_enc.vhd
+++ b/aes/rtl/vhdl/aes_enc.vhd
@@ -108,19 +108,22 @@ begin
             v_state := addroundkey(v_state, s_round_key);
             s_round <= s_round + 1;
 
-          when t_rounds'high =>
+          when t_enc_rounds'high-1 =>
             v_state := subbytes(v_state);
             v_state := shiftrow(v_state);
             v_state := addroundkey(v_state, s_round_key);
             s_round <= s_round + 1;
-
-          when t_rounds'high+1 =>
+            -- set data & valid to save one cycle
             valid_o <= '1';
             data_o  <= get_state(v_state);
+
+          when t_enc_rounds'high =>
             if (valid_o = '1' and accept_i = '1') then
               valid_o <= '0';
               data_o  <= (others => '0');
               s_round <= 0;
+              -- Set accept to save one cycle
+              accept_o <= '1';
             end if;
 
           when others =>
@@ -135,17 +138,34 @@ begin
     end process CryptP;
 
 
-    -- psl cover accept_o;
-    -- psl assert always (accept_o -> s_round = 0);
-    
-    -- psl cover valid_i and accept_o;
-    -- psl assert always (valid_i and accept_o -> next not accept_o);
+    -- synthesis off
+    verification : block is
+
+      signal s_data : std_logic_vector(0 to 127);
+
+    begin
+
+      s_data <= data_o  when rising_edge(clk_i) else
+                128x"0" when reset_i = '0';
+
+      -- psl cover accept_o;
+      -- psl assert always (accept_o -> s_round = 0);
     
-    -- psl cover valid_o and accept_i;
-    -- psl assert always (valid_o and accept_i -> next not valid_o);
+      -- psl cover valid_i and accept_o;
+      -- psl assert always (valid_i and accept_o -> next not accept_o);
+
+      -- psl cover valid_o;
+      -- psl assert always (valid_o -> s_round = t_enc_rounds'high);
+
+      -- psl cover valid_o and accept_i;
+      -- psl assert always (valid_o and accept_i -> next not valid_o);
+
+      -- psl cover valid_o and not accept_i;
+      -- psl assert always (valid_o and not accept_i -> next valid_o);
+      -- psl assert always (valid_o and not accept_i -> next data_o = s_data);
 
-    -- psl cover valid_o and not accept_i;
-    -- psl assert always (valid_o and not accept_i -> next data_o'stable);
+    end block verification;
+    -- synthesis on
 
 
   end generate IterG;