Verifying Digital Systems with MATLAB
For verification engineers, this toolbox makes formal verification accessible for fixed-point digital systems, but the contribution is incremental as it is a front-end to an existing tool.
The paper presents a MATLAB toolbox that checks design errors in fixed-point digital systems, including overflow, limit cycle, quantization, stability, and minimum phase errors, by acting as a front-end to the Digital-System Verifier. The toolbox provides both command-line and GUI interfaces, demonstrating the applicability of verification to real-world systems.
A MATLAB toolbox is presented, with the goal of checking occurrences of design errors typically found in fixed-point digital systems, considering finite word-length effects. In particular, the present toolbox works as a front-end to a recently introduced verification tool, known as Digital-System Verifier, and checks overflow, limit cycle, quantization, stability, and minimum phase errors, in digital systems represented by transfer-function and state-space equations. It provides a command-line version, with simplified access to specific functions, and a graphical-user interface, which was developed as a MATLAB application. The resulting toolbox is important for the verification community, since it shows the applicability of verification to real-world systems.