fault_injection_top.psl 2.24 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
--------------------------------------------------------------------------------


library work;
    use work.public_config_pkg.c_fault_detect_invert_mask;
    use work.private_config_pkg.c_num_fault_detect_nets;

vunit fit (fault_injection_top(struc)) {

    default clock is rising_edge(s_fiji_clk_i);

    property p_fd is forall i in {0 to c_num_fault_detect_nets-1}:
        s_fault_detect(i) = '0' until (s_fiji_fault_detect_i(i) /= 
                                              c_fault_detect_invert_mask(i));

    property p_fd2 is forall i in {0 to c_num_fault_detect_nets-1}:
        always (s_fault_detect(i) = '0' and s_fiji_fault_detect_i(i) /= c_fault_detect_invert_mask(i) and s_reset_n = '1') -> next 
        s_fault_detect(i) = '1';

    property p_fd3 is forall i in {0 to c_num_fault_detect_nets-1}:
        always (s_fault_detect(i) = '1') -> next s_fault_detect(i) = '1';

    assert p_fd  report "Invalid fault detect value.";
    assert p_fd2 report "Invalid fault detect value.";
    assert p_fd3 report "Invalid fault detect value.";
}