Skip to main content

discharge_reverse_module

logicaffeine_compile::codegen_sva::reverse_module

Function discharge_reverse_module 

Source 
pub fn discharge_reverse_module(
    name: &str,
    n: u32,
    truth_table: &[usize],
    linear_rows: Option<&[u64]>,
) -> Result<ReverseModuleObligation, String>
Expand description

Discharge the reverse-module obligation for the n-bit combinational unit truth_table. Proves reversibility by exhaustive bit-blast AND — when linear_rows (the GF(2) transfer matrix) is given — the algebraic GF(2) certificate, and REQUIRES the two verdicts to agree. On success returns the reverse module + SVA property; on failure names the erasure or the method disagreement.