bitloom_sim/
equiv.rs

1//! Dual-view equivalence: functional vs cycle-accurate `tick` (FR30).
2//!
3//! Handwritten views remain supported. **P3 product acceptance** uses the FR47
4//! **generated** path via [`check_functional_equiv_generated`].
5
6use bitloom_hir::{FrozenHir, PortValues};
7
8use crate::{AbstractionView, PortMismatch, Sim, check_mixed_both};
9
10/// Result of a bounded functional ↔ tick equivalence run.
11#[derive(Debug, Clone, PartialEq, Eq)]
12pub enum EquivStatus {
13    Pass {
14        cycles: usize,
15    },
16    Fail {
17        cycle: usize,
18        mismatches: Vec<PortMismatch>,
19    },
20}
21
22impl EquivStatus {
23    pub fn is_pass(&self) -> bool {
24        matches!(self, Self::Pass { .. })
25    }
26}
27
28/// Drive the same stimulus on FrozenHir `tick` and a functional view
29/// (handwritten **or** generated `AbstractionView`).
30/// Consistent PortValues → `Pass`; first divergence → `Fail`.
31pub fn check_functional_equiv<A: AbstractionView>(
32    hir: FrozenHir,
33    abs: &mut A,
34    stimuli: impl IntoIterator<Item = PortValues>,
35) -> EquivStatus {
36    let mut sim = Sim::new(hir);
37    let mut cycles = 0usize;
38    for inputs in stimuli {
39        match check_mixed_both(&mut sim, abs, inputs) {
40            Ok(()) => cycles += 1,
41            Err(mismatches) => {
42                return EquivStatus::Fail {
43                    cycle: cycles,
44                    mismatches,
45                };
46            }
47        }
48    }
49    EquivStatus::Pass { cycles }
50}
51
52/// FR30 on the **generated** path (P3 acceptance): `GeneratedFunctional` vs `tick`.
53///
54/// Alias of [`crate::check_generated_bridge`]. Handwritten `check_functional_equiv`
55/// remains available but is not the P3 gate.
56pub fn check_functional_equiv_generated(
57    hir: FrozenHir,
58    stimuli: impl IntoIterator<Item = PortValues>,
59) -> EquivStatus {
60    crate::check_generated_bridge(hir, stimuli)
61}
62
63/// Reset-high one cycle, then `n` cycles with `rst=0`.
64pub fn reset_then_run(n: usize) -> Vec<PortValues> {
65    let mut out = Vec::with_capacity(n + 1);
66    let mut rst = PortValues::default();
67    rst.set("rst", 1);
68    out.push(rst);
69    for _ in 0..n {
70        let mut pv = PortValues::default();
71        pv.set("rst", 0);
72        out.push(pv);
73    }
74    out
75}
bitloom_sim/equiv.rs

bitloom_sim/
equiv.rs
