Formal Verification Using SymbiYosys: Tutorial

Formal verification uses SystemVerilog Assertions (SVAs) to model the behavior of the design. Using the properties described by SVAs, the formal tool uses a suite of mathematical solvers to generate the input stimulus and exhaustively verify the design.

In short, we use SVA assume() and assert() to model the input generation and output checking. As a general approach, assumption is mostly used to describe the input behavior, i.e., we are telling the formal solver to generate the inputs that follow the intended behavior described in the form of SVA properties, and we assume the behavior. While for the outputs we want to check for correctness, we assert the properties to make sure the design follows the specification provided.

Here, we use the Formal EDA provided by SymbiYosys, the free version, to model the verification for a counter. In the free version, we can only use immediate assertions, so we have to describe our temporal properties differently. This requires more practice as it is not what one will do when using any commercial formal tool. But, Yosys is the only free formal tool available, so why not use it.

Zipcpu blog implements many such formal properties using immediate assertions and also uses the Yosys formal tool. It is also a great site to check out if you are interested in using Yosys for your projects. I certainly found it helpful.

My approach is to describe the properties using the concurrent assertions, then I model them in the immediate version. Doing so helps to learn the right way of learning SVAs and then how to use Yosys using the immediate form.

First Comes The Design: DUT

The design is a counter that counts down from a start value to zero. The start value is fixed and is set to 4'ha. The counter follows a ready/valid protocol at the input interface. The interface for the module is shown below. Quickly here's the Github link for the code [Github Repository]

module counter_ready_valid (

input logic clk,

input logic rst,

// Input interface

input logic valid_in,

output logic ready_out,

// Output interface

output logic [3:0] counter_out

);

valid_in is high for valid input requests. ready_out indicates if the counter can accept the incoming request. The counter starts from a fixed value of 4'ha and decrements every clock cycle until it goes to 0. While the counter is busy, it should pull the ready_out line low. At the core we can build the RTL for the counter as shown below:

We are busy if the counter is counting down. The input is accepted if both valid_in and ready_out are high on a clock cycle.


assign ready_out = (counter_out == '0);

always_ff @ (posedge clk)

if (rst)

counter_out <= '0;

else begin

if (valid_in && ready_out) begin

counter_out <= 4'ha;

end

else if (counter_out != '0) begin

counter_out <= counter_out - 1;

end

Formal Verification Test Plan

Next, we move towards writing down the test plan for verifying the design using formal properties. We will again follow the process previously detailed in how to write a formal test plan. Using the approach we write the properties based on counter specification.

  1. Reset value checks: After reset, the outputs should default to reset values.

  2. Ready/Valid interface: We will follow the ready/valid specification for the input interface.

  3. DUT Functionality: When the counter accepts a valid input request it should start with the correct start value and decrement until it goes to 0. Should not accept any new incoming requests when it is busy.

  4. Data Integrity: For this design, we don't have data integrity verification.

Now, let's move to the fun part by actually writing the properties. Here, I first describe the SVAs using properties and sequences, and then I show the implementation using immediate assertions. As free version on Yosys only supports immediate assertions.We first begin by assuming initial reset state. This is done within initial block as shown below.


initial begin

assume(rst);

assume (!valid_in);

end


// 1

After reset, the counter should default to reset value. In our case it should be ready to accept input requests and counter output should be zero. Also, note I am not using the clock and reset inside my properties as it is defined outside as defaults. This property will be asserted as we are checking the outputs.


property reset_value_check_P;

rst |-> ##1 (ready_out) && (counter_out == '0);

endproperty


In the immediate version we use an additional flag called past_check which gets set after first clock edge so we can safely use the $past operator.


always_ff @ (posedge clk)

if (past_check && $past(rst))

assert(ready_out);

assert(counter_out == '0);


// 2

Input requests should remain asserted until accepted by the counter. This property will be an assume() as we expect the input behavior. The formal tool will generate the stimulus based on our assumptions.


property stable_input_req_P;

valid_in && !ready_out |-> ##1 valid_in;

endproperty


In the immediate version, we use the $past() to indicate if the condition was met in the previous cycle.


always_ff @ (posedge clk)

if (past_check && !rst && $past(valid_in) && $past(!ready_out))

assume(valid_in);


// 3

We also want to ensure all valid input requests get accepted in the desired time frame, which in this example is 10 clock cycles.


property all_input_req_gets_accepted_P;

valid_in && !ready_out |-> ##[1:10] ready_out;

endproperty


This property will require additional auxiliary code to capture the delay using a delay count variable to convert it into immediate.



always_ff @ (posedge clk)

if (rst) req_delay <= '0;

else if ((valid_in) && (ready_out))

req_delay <= '0;

else if((valid_in) && !(ready_out))

req_delay <= req_delay + 1;


// We want to accept within 10 clock cycles

always_ff @ (posedge clk)

if (past_check && !$past(rst) && $past(valid_in) && !$past(ready_out))

assert(req_delay <= 4'd10);


// 4

Now we check counter specification. The counter should be decrementing if it has accepted a valid input previously. During which the readu_out should be low.


property counter_operation_P;

!ready_out |-> ##1 counter_out == $past(counter_out) - 1;

endproperty

This is easy to write suing immediate assertion.


if(past_check && !$past(rst) && !$past(ready_out))

assert(counter_out == $past(counter_out) - 1 );


// 5

We also want to make sure the counter starts with correct start value.


property counter_start_value_P;

valid_in && ready_out |-> ##1 (!ready_out) && (counter_out == 4'ha);

endproperty


The immediate version will again use the past operator and assert the requirements.


if (past_check && !$past(rst) && $past(valid_in) && $past(ready_out))

assert(counter_out == 4'ha);

assert(!ready_out);


// 6

Also, counter output can never be higher than 4'ha and can never be lower than 0.


always_ff @ (posedge clk)

if (past_valid)

assert(counter_out >= '0);

assert(counter_out <= 4'ha);


This should ensure the correct behavior of our counter logic and if our logic is buggy, then we will find Counter-Examples (CEX) with the formal analysis. Note the passing of our assertion properties does not result in a waveform, only a failure results in waveform output in the form of CEX.

Cover Properties

Next, we move to cover statements. Cover properties are a great way to ensure we have not over-constrained our inputs and also to see some waveforms for corner cases. Let's write two of them here. In the first case, we cover the scenario when our ready_out is low and in the next cycle, it goes to high. This will generate the waveform covering one full counter operation. The second cover statement will check our request delay count, req_delay, and we can generate the case to see if the input waits for two clocks before getting accepted. Isn't that nice!


always_ff @ (posedge clk)

if (!$past(rst) && past_check)

cover( $past(!ready_out) && ready_out);

cover($past(req_delay == 4'd2) && (req_delay == '0));


Time for some waveform checking. Let's start by looking at our cover waveforms for the above two cover statements. In the first figure below, we see the waveform generated for our first cover statement. The red marker shows the start of the valid request and in the next cycle the counter started with a start value of 4'ha and the ready_out line goes to zero. Finally, after the counter is finished counting down, the ready_out line goes high in the same cycle.

The second waveform below shows the second cover statement, where we want to see our input request wait for two clock cycles before getting accepted. The marker shows the cycle the wait time of two cycles and in the next cycle the request gets accepted and the counter load to start value of 4'ha. We also observe valid_in remains stable until it gets accepted. This follows the input assumption that we made previously.

Assertion Failure CEX

As mentioned previously, the passing of assertions does not result in a waveform. But it would be nice to see if the design has a bug the assertions catch them. So let's purposely introduce bugs in the design and look at the results.

First I change the counter start value in the RTL and see if property counter_start_value_P catches that or not. We see that running the formal tool results in failure and generates a counterexample in the form of a waveform as shown below. The waveform shows an incorrect start value of counter_out, it should be 4'ha not 4'h7.

In another example, here I introduce a bug for where the counter decrements by two. Running the formal analysis results in a failure and generates counterexample with waveform. The waveform below shows the counter starts correctly but then decrements to 4'h8 instead of 4'h9.