Browse Source

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
T. Meissner 4 months ago
parent
commit
77f87536c9
2 changed files with 65 additions and 25 deletions
  1. 33
    13
      aes/rtl/vhdl/aes_dec.vhd
  2. 32
    12
      aes/rtl/vhdl/aes_enc.vhd

+ 33
- 13
aes/rtl/vhdl/aes_dec.vhd View File

@@ -108,19 +108,22 @@ begin
108 108
             v_state := addroundkey(v_state, s_round_key);
109 109
             s_round <= s_round + 1;
110 110
 
111
-          when t_rounds'high =>
111
+          when t_dec_rounds'high-1 =>
112 112
             v_state := invshiftrow(v_state);
113 113
             v_state := invsubbytes(v_state);
114 114
             v_state := addroundkey(v_state, s_round_key);
115 115
             s_round <= s_round + 1;
116
-
117
-          when t_rounds'high+1 =>
116
+            -- set data & valid to save one cycle
118 117
             valid_o <= '1';
119 118
             data_o  <= get_state(v_state);
119
+
120
+          when t_dec_rounds'high =>
120 121
             if (valid_o = '1' and accept_i = '1') then
121 122
               valid_o <= '0';
122 123
               data_o  <= (others => '0');
123 124
               s_round <= 0;
125
+              -- Set accept to save one cycle
126
+              accept_o <= '1';
124 127
             end if;
125 128
 
126 129
           when others =>
@@ -135,17 +138,34 @@ begin
135 138
     end process DeCryptP;
136 139
 
137 140
 
138
-    -- psl cover accept_o;
139
-    -- psl assert always (accept_o -> s_round = 0);
140
-    
141
-    -- psl cover valid_i and accept_o;
142
-    -- psl assert always (valid_i and accept_o -> next not accept_o);
143
-    
144
-    -- psl cover valid_o and accept_i;
145
-    -- psl assert always (valid_o and accept_i -> next not valid_o);
141
+    -- synthesis off
142
+    verification : block is
143
+
144
+      signal s_data : std_logic_vector(0 to 127);
145
+
146
+    begin
147
+
148
+      s_data <= data_o  when rising_edge(clk_i) else
149
+                128x"0" when reset_i = '0';
150
+
151
+      -- psl cover accept_o;
152
+      -- psl assert always (accept_o -> s_round = 0);
153
+
154
+      -- psl cover valid_i and accept_o;
155
+      -- psl assert always (valid_i and accept_o -> next not accept_o);
156
+
157
+      -- psl cover valid_o;
158
+      -- psl assert always (valid_o -> s_round = t_dec_rounds'high);
159
+
160
+      -- psl cover valid_o and accept_i;
161
+      -- psl assert always (valid_o and accept_i -> next not valid_o);
162
+
163
+      -- psl cover valid_o and not accept_i;
164
+      -- psl assert always (valid_o and not accept_i -> next valid_o);
165
+      -- psl assert always (valid_o and not accept_i -> next data_o = s_data);
146 166
 
147
-    -- psl cover valid_o and not accept_i;
148
-    -- psl assert always (valid_o and not accept_i -> next data_o'stable);
167
+    end block verification;
168
+    -- synthesis on
149 169
 
150 170
 
151 171
   end generate IterG;

+ 32
- 12
aes/rtl/vhdl/aes_enc.vhd View File

@@ -108,19 +108,22 @@ begin
108 108
             v_state := addroundkey(v_state, s_round_key);
109 109
             s_round <= s_round + 1;
110 110
 
111
-          when t_rounds'high =>
111
+          when t_enc_rounds'high-1 =>
112 112
             v_state := subbytes(v_state);
113 113
             v_state := shiftrow(v_state);
114 114
             v_state := addroundkey(v_state, s_round_key);
115 115
             s_round <= s_round + 1;
116
-
117
-          when t_rounds'high+1 =>
116
+            -- set data & valid to save one cycle
118 117
             valid_o <= '1';
119 118
             data_o  <= get_state(v_state);
119
+
120
+          when t_enc_rounds'high =>
120 121
             if (valid_o = '1' and accept_i = '1') then
121 122
               valid_o <= '0';
122 123
               data_o  <= (others => '0');
123 124
               s_round <= 0;
125
+              -- Set accept to save one cycle
126
+              accept_o <= '1';
124 127
             end if;
125 128
 
126 129
           when others =>
@@ -135,17 +138,34 @@ begin
135 138
     end process CryptP;
136 139
 
137 140
 
138
-    -- psl cover accept_o;
139
-    -- psl assert always (accept_o -> s_round = 0);
140
-    
141
-    -- psl cover valid_i and accept_o;
142
-    -- psl assert always (valid_i and accept_o -> next not accept_o);
141
+    -- synthesis off
142
+    verification : block is
143
+
144
+      signal s_data : std_logic_vector(0 to 127);
145
+
146
+    begin
147
+
148
+      s_data <= data_o  when rising_edge(clk_i) else
149
+                128x"0" when reset_i = '0';
150
+
151
+      -- psl cover accept_o;
152
+      -- psl assert always (accept_o -> s_round = 0);
143 153
     
144
-    -- psl cover valid_o and accept_i;
145
-    -- psl assert always (valid_o and accept_i -> next not valid_o);
154
+      -- psl cover valid_i and accept_o;
155
+      -- psl assert always (valid_i and accept_o -> next not accept_o);
156
+
157
+      -- psl cover valid_o;
158
+      -- psl assert always (valid_o -> s_round = t_enc_rounds'high);
159
+
160
+      -- psl cover valid_o and accept_i;
161
+      -- psl assert always (valid_o and accept_i -> next not valid_o);
162
+
163
+      -- psl cover valid_o and not accept_i;
164
+      -- psl assert always (valid_o and not accept_i -> next valid_o);
165
+      -- psl assert always (valid_o and not accept_i -> next data_o = s_data);
146 166
 
147
-    -- psl cover valid_o and not accept_i;
148
-    -- psl assert always (valid_o and not accept_i -> next data_o'stable);
167
+    end block verification;
168
+    -- synthesis on
149 169
 
150 170
 
151 171
   end generate IterG;