Skip to main content

grid_output_to_bounded

Function grid_output_to_bounded 

Source
pub fn grid_output_to_bounded(
    g: &Grid,
    which: usize,
    width: u32,
    name_in: &dyn Fn(usize) -> String,
) -> BoundedExpr
Expand description

Lower output which (in all_outs order) to a BoundedExpr at width, naming global inputs via name_in — so the placed+routed array can be proven EQUAL to a reference expressed in the SAME variable namespace (e.g. a loop body’s s0/iv/inv0), exhaustively.