Research | Jonathan Certes

Home / Research / Abstraction of Verilog HDL at netlist level

Abstract

This tool is part of An Automated Framework Towards Widespread Formal Verification of Complex Hardware Designs, technical insights are provided here. It automates the abstraction of Verilog HDL at netlist level and feeds model-checking software.

Source code of the whole automated framework is available here . A use-case example for abstraction of Verilog HDL is available here . In this webpage, we describe this example.

Prerequisites

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
python3
iverilog
vvp
iverilog-vpi
verilog2smv
NuSMV

Also, python package pynusmv must be available.

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

verilog2smv can be downloaded here
NuSMV can be downloaded here
pynusmv can be downloaded here

Description

The example illustrates the approach through the verification of an ARM CoreSight trace decompresser using symbolic model-checking of temporal logic and automatic theorem proving.

The goal is to ensure, with model-checking, that abstract models verify temporal properties and are simulated by the concrete model.

Script nusmvAll.tcl automatizes this approach and proceeds as follows:

for each property, a Verilog wrapper is automatically created where all the module outputs which do not appear in the property are left unconnected.
verilog2smv synthesizes and translates the Verilog model, extended with the previously generated wrapper, and converts it to SMV. Optimizations step from yosys proceeds to a localization reduction of the model which is dedicated to verify the property.
NuSMV is used independently to verify that a property holds on its dedicated abstract model. This operation is repeated for each property.

Here is the pinout of the ARM CoreSight trace decompresser written with Verilog syntax:

module packets_decompresser
(
  input       nrst,       //!< low level active reset
  input       clk,        //!< clock
  input [7:0] trace_data, //!< data input
  input       trace_ctl,  //!< enable bit, active when 0
  output [3:0] decompressed_packet, //!< indicates which packet is currently decompressing
  output ready,                     //!< packet decompression has terminated
  output [3:0] data_size,           //!< number of useful bytes trace_data data
  output [7:0] data__0,   //!< one byte of output data, index  0
  output [7:0] data__1,   //!< one byte of output data, index  1
  output [7:0] data__2,   //!< one byte of output data, index  2
  output [7:0] data__3,   //!< one byte of output data, index  3
  output [7:0] data__4,   //!< one byte of output data, index  4
  output [7:0] data__5,   //!< one byte of output data, index  5
  output [7:0] data__6,   //!< one byte of output data, index  6
  output [7:0] data__7,   //!< one byte of output data, index  7
  output [7:0] data__8,   //!< one byte of output data, index  8
  output [7:0] data__9,   //!< one byte of output data, index  9
  output [7:0] data_10,   //!< one byte of output data, index 10
  output [7:0] data_11,   //!< one byte of output data, index 11
  output [7:0] data_12,   //!< one byte of output data, index 12
  output [7:0] data_13,   //!< one byte of output data, index 13
  output [7:0] data_14    //!< one byte of output data, index 14
);

Temporal properties are available in files property_*.smv.

To verify with model-checking, we must verify all 7 properties. This is long if not running on a computer cluster and can be done by running make full.
To only run a proof-of-concept, we can only verify one property available in file property_0.smv. This is quicker if running on a single computer and can be done by running make.

Here is a temporal property to verify written in PSL with SMV syntax:

PSLSPEC
  NAME "When ready, received bytes are copied in order on output vectors.
        Case of data_0." :=
forall i_0 in {0:255} :
  always(
     -- starting from a reset or the end of a packet:
     ( ("clk" && !"nrst") || ("clk" && ("ready" == 0ub1_1)) )
     -- no reset until a new packet is decompressed:
  && ( next( "nrst" until ("clk" && ("ready" == 0ub1_1)) ))
     -- received byte (with index 1) is equal to i_0:
  && ( next( next_event(  "clk" && ("ready" == 0ub1_1)) ("data_size" >= 0ud4_1) ))
  && ( next( next_event_a("clk" && !"trace_ctl")[1:1] (("trace_data" & 0ub8_00000001) == 0ub8_00000001) )) -- branch packet
  && ( next( next_event_a("clk" && !"trace_ctl")[1:1] ("trace_data" == uwconst(i_0, 8)) ))
  ->
     ( next( next_event(  "clk" && ("ready" == 0ub1_1)) ("data__0" == uwconst(i_0, 8)) ))
  );

A property that does not hold on the concrete model is available in file wrong_property.smv. We can verify that a VCD file is generated from a counterexample. This can be done by running make wrong_property.

Recorded presentation

ERTS 2022: An Automated Framework Towards Widespread Formal Verification of Complex Hardware Designs (replay)

Associated publications

Jonathan Certes, Benoît Morgan, An Automated Framework Towards Widespread Formal Verification of Complex Hardware Designs, ERTS 2022
Jonathan Certes, Méthodes et modèles pour la vérification formelle de l'attestation à distance sur microprocesseur (French), 2023

        no cookie, no javascript, no external resource, KISS!
      