From 51d7b485b9b6e28233901a25b24cac0933d422b5 Mon Sep 17 00:00:00 2001 From: tmeissner Date: Wed, 15 Jul 2020 16:17:42 +0200 Subject: [PATCH] Make PSL compatible with simulation & synthesis --- aes/rtl/vhdl/aes_enc.vhd | 75 ++++++++++++++++------------------------ aes/sim/vhdl/tb_aes.tcl | 9 ++--- 2 files changed, 34 insertions(+), 50 deletions(-) diff --git a/aes/rtl/vhdl/aes_enc.vhd b/aes/rtl/vhdl/aes_enc.vhd index ec102b5..bf8aef2 100644 --- a/aes/rtl/vhdl/aes_enc.vhd +++ b/aes/rtl/vhdl/aes_enc.vhd @@ -28,9 +28,7 @@ use work.aes_pkg.all; entity aes_enc is generic ( - design_type : string := "ITER"; - formal : boolean := false; - simulation : boolean := false + design_type : string := "ITER" ); port ( reset_i : in std_logic; -- async reset @@ -121,63 +119,48 @@ begin end process CryptP; - formalG : if formal generate + psl : block is + + signal s_key , s_din, s_dout : std_logic_vector(0 to 127) := (others => '0'); begin - default clock is rising_edge(Clk_i); + process (clk_i) is + begin + if (rising_edge(clk_i)) then + s_key <= key_i; + s_din <= data_i; + s_dout <= data_o; + end if; + end process; + + default clock is rising_edge(clk_i); -- initial reset restrict {not reset_i; reset_i[+]}[*1]; -- constraints - assume always (valid_i and not accept_o -> next stable(valid_i)); - assume always (valid_i and not accept_o -> next stable(key_i)); - assume always (valid_i and not accept_o -> next stable(data_i)); - - -- interface asserts - assert always (accept_o -> s_round = 0); - - assert always (valid_i and accept_o -> next not accept_o); - - assert always (valid_o -> s_round = t_enc_rounds'high); - - assert always (valid_o and accept_i -> next not valid_o); - - assert always (valid_o and not accept_i -> next stable(valid_o)); - assert always (valid_o and not accept_i -> next stable(data_o)); - - end generate formalG; - - - simulationG : if simulation generate - - 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'; - - default clock is rising_edge(Clk_i); + assume always (valid_i and not accept_o -> next valid_i); + assume always (valid_i and not accept_o -> next key_i = s_key); + assume always (valid_i and not accept_o -> next data_i = s_din); - cover {accept_o}; - assert always (accept_o -> s_round = 0); + ACCEPTO_c : cover {accept_o}; + ACCEPT_IN_ROUND_0_ONLY_a : assert always (accept_o -> s_round = 0); - cover {valid_i and accept_o}; - assert always (valid_i and accept_o -> next not accept_o); + VALIDI_AND_ACCEPTO_c : cover {valid_i and accept_o}; + ACCEPT_OFF_WHEN_VALID_a : assert always (valid_i and accept_o -> next not accept_o); - cover {valid_o}; - assert always (valid_o -> s_round = t_enc_rounds'high); + VALIDO_c : cover {valid_o}; + VALID_IN_LAST_ROUND_ONLY_a : assert always (valid_o -> s_round = t_enc_rounds'high); - cover {valid_o and accept_i}; - assert always (valid_o and accept_i -> next not valid_o); + VALIDO_AND_ACCEPTI_c : cover {valid_o and accept_i}; + VALID_OFF_WHEN_ACCEPTED_a : assert always (valid_o and accept_i -> next not valid_o); - cover {valid_o and not accept_i}; - assert always (valid_o and not accept_i -> next valid_o); - assert always (valid_o and not accept_i -> next data_o = s_data); + VALIDO_AND_NOT_ACCEPTI_c : cover {valid_o and not accept_i}; + VALID_STABLE_WHEN_NOT_ACCEPTED_a : assert always (valid_o and not accept_i -> next valid_o); + DATA_STABLE_WHEN_NOT_ACCEPTED_a : assert always (valid_o and not accept_i -> next data_o = s_dout); - end generate simulationG; + end block psl; end generate IterG; diff --git a/aes/sim/vhdl/tb_aes.tcl b/aes/sim/vhdl/tb_aes.tcl index 4dbd99e..4562d87 100644 --- a/aes/sim/vhdl/tb_aes.tcl +++ b/aes/sim/vhdl/tb_aes.tcl @@ -1,10 +1,11 @@ set signals [list] lappend signals "top.tb_aes.s_reset" lappend signals "top.tb_aes.s_clk" -lappend signals "top.tb_aes.s_validin" -lappend signals "top.tb_aes.s_mode" +lappend signals "top.tb_aes.s_validin_enc" +lappend signals "top.tb_aes.s_acceptout_enc" lappend signals "top.tb_aes.s_key" lappend signals "top.tb_aes.s_datain" -lappend signals "top.tb_aes.s_validout" -lappend signals "top.tb_aes.s_dataout" +lappend signals "top.tb_aes.s_validout_enc" +lappend signals "top.tb_aes.s_acceptin_enc" +lappend signals "top.tb_aes.s_dataout_enc" set num_added [ gtkwave::addSignalsFromList $signals ]