Jonathan Certes

Home / Resources / Verify LTL properties on Verilog models with Verilog2SMV

Introduction

NuSMV is an open-source model checker which implements symbolic model-checking, using a fixed point algorithm with Binary Decision Diagrams (BDD), where a set of states is represented by a BDD instead of an exhaustive list of individual states. Models are described in SMV language and NuSMV supports the analysis of specifications expressed as invariants or in temporal logics, including LTL and PSL.

Automatic translation tool Verilog2SMV converts Verilog to SMV language, which supports similar high-level types of state variables as Hardware Description Languages (HDL) for wires and registers. In particular, Verilog2SMV aims at handling designs with memories efficiently. Verilog2SMV is built on top of Yosys, a free Verilog synthesis suite. It first flattens the Verilog high-level design, synthesizes the RTL circuit while providing optimizations and then translates the output into a corresponding SMV model.

Here is shown how to formally verify LTL properties on Verilog models with NuSMV and Verilog2SMV.

Verilog

First, we write our Verilog model. For instance, a 4-bits counter with asynchronous reset.

Let's write this in a file called counter.v:

module up_counter(
  input clk,
  input reset,
  output[3:0] counter
);
  reg [3:0] counter_up;

  always @( posedge(clk) or posedge(reset) )
  begin
    if ( reset ) begin
      counter_up <= 4'd0;
    end
    else begin
      counter_up <= counter_up + 4'd1;
    end
  end

  assign counter = counter_up;
endmodule

LTL

Then, we write our property in SMV language. In this case, this is a liveness property to verify that maximum value for the counter can be reached.

This property does not hold: a reset can be triggered at any time and maximum value may never be reached.

Let's write this in a file called spec.smv:

LTLSPEC F ("counter" = 0ub4_1111);

Makefile

Now, we must call Verilog2SMV to convert our Verilog model to a Büchi automaton described in SMV language. Then, we add our LTL property to the file and call NuSMV.

Here is a Makefile that provides the recipe (make sure to indent with tabulations):

HDL = counter.v
LTL = spec.smv

all : ${HDL} ${LTL}
    verilog2smv ${HDL} counter.smv up_counter
    cat counter.smv ${LTL} > temp.smv
    NuSMV temp.smv

clean :
    ${RM} counter.smv temp.smv

Once again, we expect NuSMV to provide a counterexample since this LTL property does not hold: a reset can be triggered at any time and maximum value may never be reached.

Associated resources

Here is an archive with more Verilog models and LTL properties to illustrate several examples:

• To show that having a reset with no constraint can lead to never reaching the maximum value (what we just described).
• To show that, with no reset and a FAIRNESS constraint on clk, maximum is always reached.
• To show that, with no FAIRNESS for clk, we may never reach the counter maximum, even with no reset.
• To show that posedge operators are not handled by Verilog2SMV, having a boolean that is always set to 1 produces the same effect.

---