Skip to main content

certify_gates

logicaffeine_compile::codegen_sva::pnr_certificate

Function certify_gates 

Source 
pub fn certify_gates(
    grid: &Word,
    datapath: &Word,
) -> Option<PlacementCertificate>
Expand description

Certify a placement whose grid and datapath are ALREADY blasted into the shared gate DAG — the path that never materialises a ProofExpr tree, and therefore the only one that can certify a reconvergent datapath (a multiply chain’s tree is exponentially larger than its circuit). Fail-closed exactly like certify_mapping: a grid that is not equivalent to its spec earns no certificate.