Verifying Without Loss of Generality

A recent surge in custom silicon design for general purpose CPUs, as well as accelerators, led to an increased demand for rigorous and scalable verification techniques. Formal verification can provide strong correctness guarantees and is widely deployed in electronic design automation. However, automated formal verification techniques (such as model checking) suffer from scalability challenges. Whenever these techniques time out or run out of memory, no guarantees are obtained. Tools often feature hard-coded search heuristics and reductions that can alleviate this issue, so long as they can automatically identify the right reduction.
Crucially, this approach fails to leverage the expertise of chip designers, whose deep understanding of their design can aid the verification process. We argue that using the engineer's insight, it is often possible to narrow the search "without loss of generality" (WLOG), thus increasing scalability significantly. Off-the-shelf model checking tools, however, do not provide means to deploy non-standard reductions that are not already built-in. Technically, the developer could modify the original design to obtain a reduced model - at the risk of introducing errors or pruning relevant cases.
To enable the developer to safely exploit their insights about the design, we will (1) extend existing high-level description languages (e.g., Verilog) to enable engineers to express WLOG in a familiar language, and (2) provide tools and techniques to rigorously and automatically validate the assumptions underlying the WLOG reduction (as failure to do so may lead to incorrect verification verdicts). Finally, we will (3) evaluate our approach using existing openly available designs and model checking tools.