Skip to main content

certify_mapping_bounded

logicaffeine_compile::codegen_sva::pnr_certificate

Function certify_mapping_bounded 

Source 
pub fn certify_mapping_bounded(
    grid: BoundedExpr,
    datapath: BoundedExpr,
) -> Result<PlacementCertificate, CertifyRefusal>
Expand description

certify_mapping with the refusal NAMED. The obligation is PRICED in the shared gate DAG before any ProofExpr is materialised, so an encoding too big to hold fails as a typed refusal in milliseconds instead of walking the allocator off a cliff.