Formal Verification of FPGA Based Systems
Honghan Deng · MacSphere (McMaster University) · 2011
In design verication, although simulation is still a widely used verication technique in FPGA design, formal verication is obtaining greater acceptance as the complexity of designs increases. In the simulation method, for a circuit with n inputs and m registers an exhaustive test vector will have as many as 2(m+n) elements making it impractical for many modern circuits. Therefore this method is incomplete, i.e., it may fail to catch some design errors due to the lack of complete test coverage. Formal verication can be introduced as a complement to traditional verication techniques. The primary objectives of this thesis are determining: (i) how to for- malize FPGA implementations at dierent levels of abstraction, and (ii) how to prove their functional correctness. This thesis explores two variations of a formal verication framework by proving the functional correctness of several FPGA implementations of commonly used safety subsystem components us- ing the theorem prover PVS. We formalize components at the netlist level and the Verilog Register Transfer HDL level, preserving their functional semantics. Based on these formal models, we prove correctness conditions for the com- ponents using PVS. Finally, we present some techniques which can facilitate the proving process and describe some general strategies which can be used to prove properties of a synchronous circuit design.