fault_injection_controller.psl 11.2 KB
Newer Older
1
--------------------------------------------------------------------------------
2
3
4
-- Fault InJection Instrumenter (FIJI)
-- https://embsys.technikum-wien.at/projects/vecs/fiji
--
5
6
7
8
-- The creation of this file has been supported by the publicly funded
-- R&D project Josef Ressel Center for Verification of Embedded Computing
-- Systems (VECS) managed by the Christian Doppler Gesellschaft (CDG).
--
9
10
11
-- Authors:
-- Christian Fibich <fibich@technikum-wien.at>
-- Stefan Tauner <tauner@technikum-wien.at>
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
--
-- Copyright and related rights are licensed under the Solderpad Hardware
-- License, Version 0.51 (the "License"); you may not use this file except
-- in compliance with the License. You may obtain a copy of the License at
-- http://solderpad.org/licenses/SHL-0.51. Unless required by applicable
-- law or agreed to in writing, software, hardware and materials
-- distributed under this License is distributed on an "AS IS" BASIS,
-- WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either expressed or
-- implied. See the License for the specific language governing
-- permissions and limitations under the License.
--
-- See the LICENSE file for more details.
--
-- Description:
--  Assertions specifying the behavior of the FIC
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
--------------------------------------------------------------------------------

library ieee;
    use ieee.math_real.all;

library work;
    use work.fault_injection_controller_pkg.all;
    use work.public_config_pkg.c_id;
    use work.public_config_pkg.c_lfsr_width;
    use work.public_config_pkg.c_lfsr_poly;
    use work.public_config_pkg.c_lfsr_seed;
    use work.public_config_pkg.c_timer_width;
    use work.public_config_pkg.c_trigger_ext_active;
    use work.public_config_pkg.c_trigger_dut_active;
    use work.public_config_pkg.c_reset_dut_in_duration;
    use work.public_config_pkg.c_reset_dut_in_active;
    use work.public_config_pkg.c_fiu_config;
    use work.private_config_pkg.c_crc8_initial;
    use work.private_config_pkg.c_crc8_poly;
    use work.private_config_pkg.c_pattern_bits;
    use work.private_config_pkg.c_config_width;
    use work.private_config_pkg.c_id_width;
    use work.private_config_pkg.c_num_patterns;
    use work.private_config_pkg.c_num_select_bits;

vunit fic (fault_injection_controller(rtl)) {

    constant c_num_recv_bits : positive := integer(ceil(real(c_fiu_config'length)*real(c_num_select_bits)/8.0))*8*c_num_patterns +
                                           c_timer_width*8*c_num_patterns +
                                           c_config_width +
                                           c_id_width + 
                                           8;                                   -- CRC



    default clock is rising_edge(s_clk_i);
    -- single tc


    -- receiving
67
    property prop_states_recv is {s_controller_state=CONTROL_FSM_WAIT_FOR_CFG and s_data_valid_i='1'} |=> 
Christian Fibich's avatar
Christian Fibich committed
68
                                 {{s_data_valid_i='0'[*];s_data_valid_i='1'}[*c_num_recv_bits-1];
69
70
71
72
73
74
75
76
                                  s_controller_state=CONTROL_FSM_CHECK};

    -- states, when OK
    -- no trigger, no reset
    property prop_states_nerr_ntr_nrst is {s_controller_state=CONTROL_FSM_WAIT_TIMER_IDLE and 
                                s_config_recv(c_config_bit_te) = '0' and 
                                s_config_recv(c_config_bit_r)  = '0' and
                                (s_timer_idle = '1' or s_timer_finished='1')} |=> {
77
78
                                s_controller_state=CONTROL_FSM_WAIT_DURS[+];
                                s_controller_state=CONTROL_FSM_WAIT_FOR_CFG};
79
80
81
82
83
84
85
86

    -- trigger, no reset
    property prop_states_nerr_tr_nrst is {s_controller_state=CONTROL_FSM_WAIT_TIMER_IDLE and 
                                s_config_recv(c_config_bit_te) = '1' and 
                                s_config_recv(c_config_bit_r)  = '0' and
                                (s_timer_idle = '1' or s_timer_finished='1')} |=> {
                                s_controller_state=CONTROL_FSM_WAIT_TRIGGER and s_trigger_edge='0'[*];
                                s_controller_state=CONTROL_FSM_WAIT_TRIGGER and s_trigger_edge='1';
87
88
                                s_controller_state=CONTROL_FSM_WAIT_DURS[+];
                                s_controller_state=CONTROL_FSM_WAIT_FOR_CFG};
89
90
91
92
93
94

    property prop_states_nerr_ntr_rst is {s_controller_state=CONTROL_FSM_WAIT_TIMER_IDLE and 
                                s_config_recv(c_config_bit_te) = '0' and 
                                s_config_recv(c_config_bit_r)  = '1' and
                                (s_timer_idle = '1' or s_timer_finished='1')} |=> {
                                s_controller_state=CONTROL_FSM_APPLY_RESET[+];
95
96
                                s_controller_state=CONTROL_FSM_WAIT_DURS[+];
                                s_controller_state=CONTROL_FSM_WAIT_FOR_CFG};
97
98
99
100
101
102
103
104
105

    -- trigger, no reset
    property prop_states_nerr_tr_rst is {s_controller_state=CONTROL_FSM_WAIT_TIMER_IDLE and 
                                s_config_recv(c_config_bit_te) = '1' and 
                                s_config_recv(c_config_bit_r)  = '1' and
                                (s_timer_idle = '1' or s_timer_finished='1')} |=> {
                                s_controller_state=CONTROL_FSM_WAIT_TRIGGER and s_trigger_edge='0'[*];
                                s_controller_state=CONTROL_FSM_WAIT_TRIGGER and s_trigger_edge='1';
                                s_controller_state=CONTROL_FSM_APPLY_RESET[+];
106
107
                                s_controller_state=CONTROL_FSM_WAIT_DURS[+];
                                s_controller_state=CONTROL_FSM_WAIT_FOR_CFG};
108
109
110
111

    -- states, when NOK
    property prop_states_err is s_controller_state=CONTROL_FSM_CHECK and (s_id_recv /= c_id or
                                  (s_crc_calc /= std_logic_vector(to_unsigned(0, 8))) or
112
                                   s_uart_error = '1') -> next s_controller_state=CONTROL_FSM_WAIT_FOR_CFG;
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150

    -- patterns, when OK
    -- no trigger, no reset
    property prop_patterns_nerr_ntr_nrst is {s_controller_state=CONTROL_FSM_WAIT_TIMER_IDLE and 
                                  s_config_recv(c_config_bit_te) = '0' and 
                                  s_config_recv(c_config_bit_r)  = '0' and
                                  (s_timer_idle = '1' or s_timer_finished='1')} |=> {
                                  s_fi_pattern="1" and s_timer_finished='0' and s_update_fius_o ='0'[*];
                                  s_fi_pattern="1" and s_timer_finished='1' and s_update_fius_o ='1';
                                  s_fi_pattern="0" and s_timer_finished='0' and s_update_fius_o ='0'[*];
                                  s_fi_pattern="0" and s_timer_finished='1' and s_update_fius_o ='0';
                                  s_fi_pattern="1"};

    -- trigger, no reset
    property prop_patterns_nerr_tr_nrst is {stable(s_controller_state) = false and 
                                            s_controller_state=CONTROL_FSM_WAIT_TRIGGER and  
                                            s_config_recv(c_config_bit_r)  = '0'} |-> {
                                  {{s_trigger_edge='0'[*]; s_trigger_edge='1'} && s_fi_pattern="1"[+]};
                                  s_fi_pattern="1" and s_timer_finished='0' and s_update_fius_o ='0'[*];
                                  s_fi_pattern="1" and s_timer_finished='1' and s_update_fius_o ='1';
                                  s_fi_pattern="0" and s_timer_finished='0' and s_update_fius_o ='0'[*];
                                  s_fi_pattern="0" and s_timer_finished='1' and s_update_fius_o ='0';
                                  s_fi_pattern="1"};

    -- control signals when OK
    -- no trigger, no reset
    property prop_patterns_nerr_ntr_rst is {s_controller_state=CONTROL_FSM_WAIT_TIMER_IDLE and 
                                  s_config_recv(c_config_bit_te) = '0' and 
                                  s_config_recv(c_config_bit_r)  = '1'} |=> {
                                  s_controller_state=CONTROL_FSM_APPLY_RESET and s_fi_pattern="1"[+];
                                  s_fi_pattern="1" and s_timer_finished='0' and s_update_fius_o ='0'[*];
                                  s_fi_pattern="1" and s_timer_finished='1' and s_update_fius_o ='1';
                                  s_fi_pattern="0" and s_timer_finished='0' and s_update_fius_o ='0'[*];
                                  s_fi_pattern="0" and s_timer_finished='1' and s_update_fius_o ='0';
                                  s_fi_pattern="1"};

    -- only the config done message
    property prop_msg_conf_done is s_controller_state=CONTROL_FSM_CHECK ->                   -- when in CHECK state
151
                                {s_msg_data_o(c_msg_bit_type1 downto c_msg_bit_type0) = c_msg_type_conf_done and s_send_msg_o = '1'; -- a CONF_DONE / READY message should be sent
152
153
154
155
                                 s_send_msg_o='0'}; 

    -- temporal order of messages
    property prop_msg_order is (s_controller_state=CONTROL_FSM_CHECK and s_id_error_comb = '0' and 
156
                                s_crc_error_comb = '0' and s_uart_error = '0' and s_config_recv(c_config_bit_n) = '0') -> next -- if there were no errors + no update message
157
                                 {s_send_msg_o='0'[+];
158
                                  s_send_msg_o='1' -> (s_controller_state=CONTROL_FSM_WAIT_DURS and
159
160
161
162
163
164
165
166
167
168
                                                       s_msg_data_o(c_msg_bit_type1 downto c_msg_bit_type0) = c_msg_type_ready); -- the next message should be a READY message
                                  s_send_msg_o='0'[*];
                                  (s_send_msg_o='1' and s_controller_state /= CONTROL_FSM_CHECK) -> --optionally, an UNDERRUN message can be sent
                                    s_msg_data_o(c_msg_bit_type1 downto c_msg_bit_type0) = c_msg_type_underrun};

    property prop_msg_underrun is (s_timer_finished='1' and s_fi_pattern="0" and s_controller_state /= CONTROL_FSM_WAIT_TIMER_IDLE) -> 
                                  (s_send_msg_o='1' and s_msg_data_o(c_msg_bit_type1 downto c_msg_bit_type0) = c_msg_type_underrun);
                                                       

    -- timers must always be completed
169
    property prop_timer_completion is ({s_timer_load='1'} |=> {s_timer_idle='0' and s_timer_finished='0'[*];
170
171
                                                                       s_timer_finished='1'});
    -- if no reload, timer must go to idle
172
    property prop_timer_idle is (s_timer_finished='1' and s_timer_load='0' -> next s_timer_idle = '1');
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189

    states_recv:            assert always prop_states_recv;
    states_nerr_ntr_nrst:   assert always prop_states_nerr_ntr_nrst;
    states_nerr_tr_nrst:    assert always prop_states_nerr_tr_nrst;
    states_nerr_ntr_rst:    assert always prop_states_nerr_ntr_rst;
    states_nerr_tr_rst:     assert always prop_states_nerr_tr_rst;
    states_err:             assert always prop_states_err;

    patterns_nerr_ntr_nrst: assert always prop_patterns_nerr_ntr_nrst;
    patterns_nerr_tr_nrst : assert always prop_patterns_nerr_tr_nrst;

    msg_conf_done:          assert always prop_msg_conf_done;
    msg_order:              assert always prop_msg_order;
    msg_underrun:           assert always prop_msg_underrun;

    timer_completion:       assert always prop_timer_completion;
    timer_idle:             assert always prop_timer_idle;
190
}