litex/verify/
verify_atomic_fact.rs

1use crate::prelude::*;
2
3impl Runtime {
4    pub fn verify_atomic_fact(
5        &mut self,
6        fact: &AtomicFact,
7        verify_state: &VerifyState,
8    ) -> Result<StmtResult, RuntimeError> {
9        if let Some(cached_result) =
10            self.verify_fact_from_cache_using_display_string(&fact.clone().into())
11        {
12            return Ok(cached_result);
13        }
14
15        if !verify_state.well_defined_already_verified {
16            if let Err(e) = self.verify_atomic_fact_well_defined(fact, verify_state) {
17                return Err({
18                    VerifyRuntimeError(RuntimeErrorStruct::new(
19                        Some(Fact::from(fact.clone()).into_stmt()),
20                        String::new(),
21                        fact.line_file(),
22                        Some(e),
23                        vec![],
24                    ))
25                    .into()
26                });
27            }
28        }
29
30        let next_verify_state = verify_state.make_state_with_req_ok_set_to_true();
31
32        match fact {
33            AtomicFact::EqualFact(equal_fact) => {
34                self.verify_equal_fact(equal_fact, &next_verify_state)
35            }
36            _ => self.verify_non_equational_atomic_fact(fact, &next_verify_state, true),
37        }
38    }
39}
litex/verify/verify_atomic_fact.rs

litex/verify/
verify_atomic_fact.rs
