Skip to main content

loop_next_to_bounded

logicaffeine_compile::codegen_sva::fabric_rtl

Function loop_next_to_bounded 

Source 
pub fn loop_next_to_bounded(
    lf: &LoopFabric,
    which: usize,
    width: u32,
) -> BoundedExpr
Expand description

Lower ONE loop-carried state register’s next-state (next[which]) to a BoundedExpr over the body inputs s0.., iv, inv0.. at the given width — so our certified SAT can prove the induction STEP (the body transition ≡ the VM’s per-iteration semantics) exhaustively.