A Formal Verification Methodology for FPGA-Based Stepper Motor Control

Abstract

Stepper motors are electric motors that are used extensively in safety-critical applications such as auto, medical devices, and surgical robots. A popular trend is the use of FPGA-based digital control for stepper motors. We present a formal verification methodology for 6 types of stepper motor (SM) control. Our methodology is based on the theory of Well-Founded Equivalence Bisimulation refinement , where both formal specifications and implementations are treated as transition systems. We define formal specifications for six types of Stepper Motor control. We also develop correctness proof obligations for FPGA implementations of stepper motor control. The methods are demonstrated using six case studies. The specifications are simple, with less than 50 transitions. We have used our methodology to verify FPGA controllers with millions of transitions against these simple specifications.