Skip to main content

while_next_to_bounded

logicaffeine_compile::codegen_sva::fabric_rtl

Function while_next_to_bounded 

Source 
pub fn while_next_to_bounded(
    wf: &WhileFabric,
    which: usize,
    width: u32,
) -> BoundedExpr
Expand description

Lower ONE while-body state register’s next-state to a BoundedExpr (over s0.., inv0..) for the certified body step. No induction variable in the body-input convention.