Skip to main content

litex/verify/
verify_not_forall_fact.rs

1use crate::prelude::*;
2use std::result::Result;
3
4impl Runtime {
5    pub fn verify_not_forall_fact(
6        &mut self,
7        not_forall: &NotForallFact,
8        verify_state: &VerifyState,
9    ) -> Result<StmtResult, RuntimeError> {
10        if !verify_state.well_defined_already_verified {
11            self.verify_not_forall_fact_well_defined(not_forall, verify_state)?;
12        }
13
14        if let Some(cached_result) =
15            self.verify_fact_from_cache_using_display_string(&not_forall.clone().into())
16        {
17            return Ok(cached_result);
18        }
19
20        Ok(StmtUnknown::new().into())
21    }
22}