Formal Hardware Verification with Bounded Model Checking And Temporal Induction

Abstract

Digital hardware systems are all around us, powering the devices we have come to take for granted. The most common way of verifying that these systems work correctly has been by modelling them as computer programs and testing their behaviour on well-formed sets of inputs, a method known as simulation-based verification. Formal verification is an alternative verification method that has been growing in popularity. It promises to free the engineer from defining representative input test sets by exploring the entire input and state spaces of a design.

This thesis investigates bounded model checking and temporal induction---two techniques of formal property verification, a subset of formal verification using the model checking algorithm---as an alternative to a simulated testbench in the verification of an audio controller module. A property set was formulated in the Property Specification Language and verified against the module with SymbiYosys, an open-source formal tool.

It was determined that while formal verification offers significant advantages over simulation, its longer execution time and intrusive nature make it unsuitable as a drop-in replacement for simulation. Instead, this thesis suggests a verification flow comprising of both methods.