bitloom_sim/
equiv.rs

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

bitloom_sim/
equiv.rs
