litex/verify/
verify_state.rs

1pub struct VerifyState {
2    pub round: u8,
3    pub well_defined_already_verified: bool,
4    pub equality_can_use_known_forall: bool,
5}
6
7impl VerifyState {
8    pub fn new(round: u8, well_defined_already_verified: bool) -> Self {
9        VerifyState {
10            round,
11            well_defined_already_verified,
12            equality_can_use_known_forall: true,
13        }
14    }
15
16    pub fn is_final_round(&self) -> bool {
17        self.round >= 2
18    }
19
20    pub fn new_state_with_round_increased(&self) -> Self {
21        return Self {
22            round: self.round + 1,
23            well_defined_already_verified: self.well_defined_already_verified,
24            equality_can_use_known_forall: self.equality_can_use_known_forall,
25        };
26    }
27
28    pub fn make_state_with_req_ok_set_to_true(&self) -> Self {
29        return Self {
30            round: self.round,
31            well_defined_already_verified: true,
32            equality_can_use_known_forall: self.equality_can_use_known_forall,
33        };
34    }
35
36    pub fn is_round_0(&self) -> bool {
37        self.round == 0
38    }
39
40    pub fn make_final_round_state(&self) -> Self {
41        return Self {
42            round: 2,
43            well_defined_already_verified: self.well_defined_already_verified,
44            equality_can_use_known_forall: self.equality_can_use_known_forall,
45        };
46    }
47
48    pub fn new_with_final_round(well_defined_already_verified: bool) -> Self {
49        return Self::new(2, well_defined_already_verified);
50    }
51
52    pub fn without_known_forall_for_equality(&self) -> Self {
53        return Self {
54            round: self.round,
55            well_defined_already_verified: self.well_defined_already_verified,
56            equality_can_use_known_forall: false,
57        };
58    }
59}
litex/verify/verify_state.rs

litex/verify/
verify_state.rs
