litex/verify/
verify_fact.rs

1use crate::prelude::*;
2use std::result::Result;
3
4impl Runtime {
5    pub fn verify_fact_return_err_if_not_true(
6        &mut self,
7        fact: &Fact,
8        verify_state: &VerifyState,
9    ) -> Result<StmtResult, RuntimeError> {
10        let result = match fact {
11            Fact::AtomicFact(atomic_fact) => self.verify_atomic_fact(atomic_fact, verify_state),
12            Fact::AndFact(and_fact) => self.verify_and_fact(and_fact, verify_state),
13            Fact::ChainFact(chain_fact) => self.verify_chain_fact(chain_fact, verify_state),
14            Fact::ForallFact(forall_fact) => self.verify_forall_fact(forall_fact, verify_state),
15            Fact::ForallFactWithIff(forall_fact_with_iff) => {
16                self.verify_forall_fact_with_iff(forall_fact_with_iff, verify_state)
17            }
18            Fact::NotForall(not_forall) => self.verify_not_forall_fact(not_forall, verify_state),
19            Fact::ExistFact(exists_fact) => self.verify_exist_fact(exists_fact, verify_state),
20            Fact::OrFact(or_fact) => self.verify_or_fact(or_fact, verify_state),
21        }?;
22
23        if result.is_unknown() {
24            let fact_owned = fact.clone();
25            let line_file = fact_owned.line_file();
26            let unknown_detail = if let StmtResult::StmtUnknown(u) = &result {
27                u.detail_for_display()
28            } else {
29                String::new()
30            };
31            return Err(RuntimeError::from(VerifyRuntimeError(
32                RuntimeErrorStruct::new(
33                    Some(fact_owned.clone().into_stmt()),
34                    "verification failed".to_string(),
35                    line_file.clone(),
36                    Some(RuntimeError::from(UnknownRuntimeError(
37                        RuntimeErrorStruct::new(
38                            Some(fact_owned.into_stmt()),
39                            unknown_detail,
40                            line_file,
41                            None,
42                            vec![],
43                        ),
44                    ))),
45                    vec![],
46                ),
47            )));
48        } else {
49            Ok(result)
50        }
51    }
52}
53
54impl Runtime {
55    pub fn verify_exist_or_and_chain_atomic_fact(
56        &mut self,
57        exist_or_and_chain_atomic_fact: &ExistOrAndChainAtomicFact,
58        verify_state: &VerifyState,
59    ) -> Result<StmtResult, RuntimeError> {
60        match exist_or_and_chain_atomic_fact {
61            ExistOrAndChainAtomicFact::AtomicFact(atomic_fact) => {
62                self.verify_atomic_fact(atomic_fact, verify_state)
63            }
64            ExistOrAndChainAtomicFact::AndFact(and_fact) => {
65                self.verify_and_fact(and_fact, verify_state)
66            }
67            ExistOrAndChainAtomicFact::ChainFact(chain_fact) => {
68                self.verify_chain_fact(chain_fact, verify_state)
69            }
70            ExistOrAndChainAtomicFact::OrFact(or_fact) => {
71                self.verify_or_fact(or_fact, verify_state)
72            }
73            ExistOrAndChainAtomicFact::ExistFact(exist_fact) => {
74                self.verify_exist_fact(exist_fact, verify_state)
75            }
76        }
77    }
78
79    pub fn verify_or_and_chain_atomic_fact(
80        &mut self,
81        or_and_chain_atomic_fact: &OrAndChainAtomicFact,
82        verify_state: &VerifyState,
83    ) -> Result<StmtResult, RuntimeError> {
84        match or_and_chain_atomic_fact {
85            OrAndChainAtomicFact::AtomicFact(atomic_fact) => {
86                self.verify_atomic_fact(atomic_fact, verify_state)
87            }
88            OrAndChainAtomicFact::AndFact(and_fact) => self.verify_and_fact(and_fact, verify_state),
89            OrAndChainAtomicFact::ChainFact(chain_fact) => {
90                self.verify_chain_fact(chain_fact, verify_state)
91            }
92            OrAndChainAtomicFact::OrFact(or_fact) => self.verify_or_fact(or_fact, verify_state),
93        }
94    }
95
96    pub fn verify_and_chain_atomic_fact(
97        &mut self,
98        and_chain_atomic_fact: &AndChainAtomicFact,
99        verify_state: &VerifyState,
100    ) -> Result<StmtResult, RuntimeError> {
101        match and_chain_atomic_fact {
102            AndChainAtomicFact::AtomicFact(atomic_fact) => {
103                self.verify_atomic_fact(atomic_fact, verify_state)
104            }
105            AndChainAtomicFact::AndFact(and_fact) => self.verify_and_fact(and_fact, verify_state),
106            AndChainAtomicFact::ChainFact(chain_fact) => {
107                self.verify_chain_fact(chain_fact, verify_state)
108            }
109        }
110    }
111}
litex/verify/verify_fact.rs

litex/verify/
verify_fact.rs
