Struct FormalEquivProduct 

pub struct FormalEquivProduct {
    pub seed: u64,
    pub random_cycles: usize,
    /* private fields */
}

Product entry for FR100 automatic compare + bounded formal equivalence.

Not a rename of crate::SharedStimulusScoreboard: random sampling and bounded exhaustive exploration are distinct surfaces; only the latter is the F1-(i) formal product entry.

Fields

seed: u64

Deterministic seed for Self::check_random_compare.

random_cycles: usize

Number of stimulus frames for the random/compare companion path.

Implementations

impl FormalEquivProduct

pub fn new(seed: u64, random_cycles: usize) -> Self

Build with seed + random cycle count; default alphabet empty until Self::with_boolean_ports.

pub fn with_boolean_ports(self, ports: &[&str]) -> Self

Pin boolean ports that form the exhaustive / random alphabet.

pub fn with_exhaustive_depth(self, depth: usize) -> Self

Set bounded-exhaustive sequence depth (F1-(i) / F4 fixture scale).

pub fn alphabet(&self) -> Vec<PortValues>

Alphabet of single-frame PortValues (cartesian product of 0/1 on each boolean port). Empty ports → one default empty frame.

pub fn random_stimuli(&self) -> Vec<PortValues>

Deterministic random stimuli from the alphabet (LCG; companion F3 path).

pub fn check_random_compare(&self, hir: FrozenHir) -> EquivStatus

F3 companion: automatic random PortValues compare (generated FL vs tick).

Reproducible for a fixed seed. Not sufficient alone to close FR100 (F5).

pub fn check_random_compare_with<A: AbstractionView>( &self, hir: FrozenHir, abs: &mut A, ) -> EquivStatus

Same as Self::check_random_compare with an arbitrary functional view (deliberate-mismatch ATDD).

pub fn check_bounded_exhaustive(&self, hir: FrozenHir) -> EquivStatus

F1-(i) product entry: exhaustive FL≡tick over all alphabet^depth sequences.

Beyond random scoreboard sampling: every sequence of length exhaustive_depth drawn from the pinned alphabet is checked. First failing sequence returns Fail with readable PortMismatchs.

pub fn check_bounded_exhaustive_with<A: AbstractionView>( &self, hir: FrozenHir, abs: &mut A, ) -> EquivStatus

Bounded exhaustive with an arbitrary functional view (mismatch ATDD).

pub fn exhaustive_sequences(&self) -> Vec<Vec<PortValues>>

All sequences of length exhaustive_depth over Self::alphabet.

Trait Implementations

impl Clone for FormalEquivProduct

fn clone(&self) -> FormalEquivProduct

Returns a duplicate of the value.

fn clone_from(&mut self, source: &Self)

Performs copy-assignment from source.

impl Debug for FormalEquivProduct

fn fmt(&self, f: &mut Formatter<'_>) -> Result

Formats the value using the given formatter.