Add PSL checkers, refactoring

* Add some simple PSL checkers & coverage to aes_enc & aes_dec
* Add generating of PSL coverage report
* Add report outputs to testbench

aes/rtl/vhdl/aes_dec.vhd

@@ -1,7 +1,6 @@
 -- ======================================================================
--- AES decryption
--- algorithm according to FIPS 197 specification
--- Copyright (C) 2011 Torsten Meissner
+-- AES encryption/decryption
+-- Copyright (C) 2019 Torsten Meissner
 -------------------------------------------------------------------------
 -- This program is free software; you can redistribute it and/or modify
 -- it under the terms of the GNU General Public License as published by
@@ -34,11 +33,11 @@ entity aes_dec is
   port (
     reset_i     : in  std_logic;                   -- async reset
     clk_i       : in  std_logic;                   -- clock
-    key_i       : in  std_logic_vector(0 TO 127);  -- key input
-    data_i      : in  std_logic_vector(0 TO 127);  -- data input
+    key_i       : in  std_logic_vector(0 to 127);  -- key input
+    data_i      : in  std_logic_vector(0 to 127);  -- data input
     valid_i     : in  std_logic;                   -- input key/data valid flag
     accept_o    : out std_logic;
-    data_o      : out std_logic_vector(0 TO 127);  -- data output
+    data_o      : out std_logic_vector(0 to 127);  -- data output
     valid_o     : out std_logic;                   -- output data valid flag
     accept_i    : in  std_logic
   );
@@ -70,10 +69,13 @@ architecture rtl of aes_dec is
 begin
 
 
+  -- psl default clock is rising_edge(Clk_i);
+
+
   IterG : if design_type = "ITER" generate
 
 
-    signal s_round : natural range t_rounds'low to t_rounds'high+1;
+    signal s_round : t_dec_rounds;
 
 
   begin
@@ -133,7 +135,22 @@ 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);
+
+    -- psl cover valid_o and not accept_i;
+    -- psl assert always (valid_o and not accept_i -> next data_o'stable);
+
+
   end generate IterG;
+  
 
 
 end architecture rtl;
+

aes/rtl/vhdl/aes_enc.vhd

@@ -1,7 +1,6 @@
 -- ======================================================================
 -- AES encryption/decryption
--- algorithm according to FIPS 197 specification
--- Copyright (C) 2011 Torsten Meissner
+-- Copyright (C) 2019 Torsten Meissner
 -------------------------------------------------------------------------
 -- This program is free software; you can redistribute it and/or modify
 -- it under the terms of the GNU General Public License as published by
@@ -34,11 +33,11 @@ entity aes_enc is
   port (
     reset_i     : in  std_logic;                   -- async reset
     clk_i       : in  std_logic;                   -- clock
-    key_i       : in  std_logic_vector(0 TO 127);  -- key input
-    data_i      : in  std_logic_vector(0 TO 127);  -- data input
+    key_i       : in  std_logic_vector(0 to 127);  -- key input
+    data_i      : in  std_logic_vector(0 to 127);  -- data input
     valid_i     : in  std_logic;                   -- input key/data valid flag
     accept_o    : out std_logic;
-    data_o      : out std_logic_vector(0 TO 127);  -- data output
+    data_o      : out std_logic_vector(0 to 127);  -- data output
     valid_o     : out std_logic;                   -- output data valid flag
     accept_i    : in  std_logic
   );
@@ -70,12 +69,15 @@ architecture rtl of aes_enc is
 begin
 
 
-  IterG : if design_type = "ITER" generate
-
-
-    signal s_round : natural range t_rounds'low to t_rounds'high+1;
+  -- psl default clock is rising_edge(Clk_i);
 
 
+  IterG : if design_type = "ITER" generate
+  
+  
+    signal s_round : t_enc_rounds;
+  
+  
   begin
 
 
@@ -133,7 +135,22 @@ 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);
+    
+    -- 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 data_o'stable);
+
+
   end generate IterG;
+  
 
 
 end architecture rtl;
+

aes/rtl/vhdl/aes_pkg.vhd

@@ -1,7 +1,6 @@
 -- ======================================================================
 -- AES encryption/decryption
--- package file with functions
--- Copyright (C) 2011 Torsten Meissner
+-- Copyright (C) 2019 Torsten Meissner
 -------------------------------------------------------------------------
 -- This program is free software; you can redistribute it and/or modify
 -- it under the terms of the GNU General Public License as published by
@@ -18,6 +17,7 @@
 -- Foundation, Inc., 51 Franklin St, Fifth Floor, Boston, MA  02110-1301  USA
 -- ======================================================================
 
+
 -- aes implementation
 -- key length: 128 bit -> Nk = 4
 -- data width: 128 bit -> Nb = 4
@@ -77,6 +77,8 @@ package aes_pkg is
 
   subtype t_rounds is natural range 0 to c_nr + 1;
   subtype t_key_rounds is natural range c_nk to c_nb * (c_nr + 1);
+  subtype t_enc_rounds is natural range t_rounds'low to t_rounds'high+1;
+  subtype t_dec_rounds is natural range t_rounds'low to t_rounds'high+1;
 
   type t_datatable1d is array (0 to 3) of std_logic_vector(7 downto 0);
   type t_datatable2d is array (0 to 3) of t_datatable1d;

aes/sim/vhdl/Makefile

@@ -1,7 +1,6 @@
 # ======================================================================
 # AES encryption/decryption
-# algorithm according to FIPS 197 specification
-# Copyright (C) 2011 Torsten Meissner
+# Copyright (C) 2019 Torsten Meissner
 #-----------------------------------------------------------------------
 # This program is free software; you can redistribute it and/or modify
 # it under the terms of the GNU General Public License as published by
@@ -19,23 +18,45 @@
 # ======================================================================
 
 
-all : sim
+RTL_SRC := \
+  ../../rtl/vhdl/aes_pkg.vhd \
+  ../../rtl/vhdl/aes.vhd     \
+  ../../rtl/vhdl/aes_enc.vhd \
+  ../../rtl/vhdl/aes_dec.vhd
 
-sim : tb_aes.ghw
+SIM_SRC := \
+  tb_aes.vhd
 
-compile : ../../rtl/vhdl/*.vhd tb_aes.vhd
-	ghdl -a --std=08 ../../rtl/vhdl/aes_pkg.vhd ../../rtl/vhdl/aes.vhd ../../rtl/vhdl/aes_enc.vhd ../../rtl/vhdl/aes_dec.vhd tb_aes.vhd
-	ghdl -e --std=08 tb_aes
 
-tb_aes.ghw : compile
-	ghdl -r tb_aes --wave=tb_aes.ghw --assert-level=error --stop-time=10us
+.PHONY: sim
+sim: tb_aes.ghw
 
-wave : tb_aes.ghw
+
+.PHONY: compile
+compile: tb_aes
+
+
+tb_aes: ${RTL_SRC} ${SIM_SRC}
+	ghdl -a --std=08 -fpsl ${RTL_SRC} ${SIM_SRC}
+	ghdl -e --std=08 -fpsl $@
+
+
+tb_aes.ghw: tb_aes
+	ghdl -r tb_aes --wave=tb_aes.ghw --assert-level=error \
+	  --psl-report=$(basename $@)_psl_coverage_report.json
+
+
+.PHONY: wave
+wave: tb_aes.ghw
 	gtkwave -S tb_aes.tcl tb_aes.ghw
 
-clean :
+
+.PHONY: clean
+clean:
 	echo "# cleaning simulation files"
 	rm -f tb_aes
 	rm -f tb_aes.ghw
 	rm -f *.cf
 	rm -f *.o
+	rm -f *.json
+

aes/sim/vhdl/tb_aes.vhd

@@ -1,7 +1,6 @@
 -- ======================================================================
--- AES encryption/decryption testbench
--- tests according to NIST special publication
--- Copyright (C) 2011 Torsten Meissner
+-- AES encryption/decryption
+-- Copyright (C) 2019 Torsten Meissner
 -------------------------------------------------------------------------
 -- This program is free software; you can redistribute it and/or modify
 -- it under the terms of the GNU General Public License as published by
@@ -19,7 +18,6 @@
 -- ======================================================================
 
 
-
 library ieee;
 use ieee.std_logic_1164.all;
 use ieee.numeric_std.all;
@@ -94,6 +92,7 @@ begin
   begin
     wait until s_reset = '1';
     -- ENCRYPTION TEST
+    report "Test encryption";
     wait until rising_edge(s_clk);
     s_validin_enc <= '1';
     s_datain <= x"3243f6a8885a308d313198a2e0370734";
@@ -108,6 +107,7 @@ begin
     wait until rising_edge(s_clk);
     s_acceptin_enc <= '0';
     -- DECRYPTION TEST
+    report "Test decryption";
     wait until rising_edge(s_clk);
     s_validin_dec <= '1';
     wait until s_acceptout_dec = '1' and rising_edge(s_clk);
@@ -120,6 +120,7 @@ begin
     wait until rising_edge(s_clk);
     s_acceptin_dec <= '0';
     wait for 100 ns;
+    report "Tests successful";
     finish(0);
   end process;