Our paper "KAIROS: Incremental Verification in High-Level Synthesis through Latency-Insensitive Design" has been accepted for publication in the proceedings of ACM Formal Methods in Computer-Aided Design. The paper is available here. The slides are available here.

The paper describes KAIROS, an automatic methodology for incremental formal verification in high-level synthesis (HLS). KAIROS verifies the equivalence of the RTL implementations the designer subsequently derives from the same HLS-ready specification by applying code manipulations and knobs. We evaluate KAIROS by checking the equivalence of multiple RTL implementations of a hardware module and a RISC-V processor designed with HLS: KAIROS quickly detects bugs caused by wrong code manipulations and knob applications.