An Automated Framework Towards Widespread Formal Verification of Complex Hardware Designs

Framework:

The source code is written using Tool Command Language (TCL) and Python 3, part is an extension for Icarus based on Verilog Programming Interface (VPI).

In order to work properly, the following commands must be available:

• tclsh
• verilog2smv
• NuSMV
• iverilog
• vvp
• iverilog-vpi

Also, python package pynusmv must be available.

Debian package tcl provides tclsh.

verilog2smv can be downloaded here

NuSMV can be downloaded here

pynusmv can be downloaded here

Debian package iverilog provides iverilog, vvp and iverilog-vpi.

Example:

We illustrate the approach through the verification of temporal properties and proof of a lemma on a CoreSight trace decompresser. This is achieved using symbolic model-checking of temporal logic and automatic theorem proving.

Details are provided in paper An Automated Framework Towards Widespread Formal Verification of Complex Hardware Designs, ERTS 2022: Embedded Real Time Systems, 30-31 March 2022, Toulouse, France

To reproduce the experiment, unzip the archive and follow the instructions from files:

• ./02_proof/README
• ./03_model-checking/README

In case of a hurry, just run:

• make -C ./02_proof/
• make -C ./03_model-checking/