Function check_functional_equiv 

pub fn check_functional_equiv<A: AbstractionView>(
    hir: FrozenHir,
    abs: &mut A,
    stimuli: impl IntoIterator<Item = PortValues>,
) -> EquivStatus

Drive the same stimulus on FrozenHir tick and a functional view (handwritten or generated AbstractionView). Consistent PortValues → Pass; first divergence → Fail.