Formal Property Verification: Property uncoverable if signal used in always block

SystemVerilog
, ,
1

Hello,

I have a SystemVerilog module containing concurrent assertions for formal property verification that is bound to a VHDL design under verification.
I wanted to use some Verilog code in this module to support my assertions. I tried 2 different versions of always blocks. The one using $rose allows the cover property to be coverable. The one using posedge makes the cover property uncoverable.
There are no assumptions, no other assertions or cover properties. testSignal is connected to a input of the VHDL block. etCount is a dummy int variable.

default disable iff(rst);
default clocking c0 @(posedge clk); endclocking

initial begin
etCount = 0;
end

cover property (##[0:$]$rose(testSignal));

// with this block the cover property is coverable
always @($rose(testSignal)) begin
etCount <= 0;
end

// with this block the cover property is uncoverable
always @(posedge testSignal) begin
etCount <= 0;
end

Can someone explain this behaviour?

Thank you in advance!
K.

2

In reply to katce:
A few comments and observations:

[list=1]
[*] On cover property (##[0:$]rose(testSignal));* You do not need the ##[0:]
[] There is a big difference between always @($rose(testSignal)) and always @(posedge testSignal) and always @(posedge clk) if($rose…
The correct way to code the supporting code is:


// Correct way 
    always  @(posedge clk) begin 
        if ($rose(testSignal)) begin 
               -> e_clk;
             #2 etCount_clk <= etCount_clk+1'b1; 
        end
    end

Below is an image of the test result that explains the difference. Code is at http://systemverilog.us/vf/explain.sv
image at http://systemverilog.us/vf/explain.png

1306×666 52.1 KB

Ben Cohen
http://www.systemverilog.us/ ben@systemverilog.us
For training, consulting, services: contact http://cvcblr.com/home

  1. VF Horizons:PAPER: SVA Alternative for Complex Assertions - SystemVerilog - Verification Academy
  2. http://systemverilog.us/vf/SolvingComplexUsersAssertions.pdf
  3. “Using SVA for scoreboarding and TB designs”
    http://systemverilog.us/papers/sva4scoreboarding.pdf
  4. “Assertions Instead of FSMs/logic for Scoreboarding and Verification”
    https://verificationacademy.com/verification-horizons/october-2013-volume-9-issue-3
  5. SVA in a UVM Class-based Environment
    https://verificationacademy.com/verification-horizons/february-2013-volume-9-issue-1/SVA-in-a-UVM-Class-based-Environment

FREE BOOK: Component Design by Example
… A Step-by-Step Process Using VHDL with UART as Vehicle

3

In reply to ben@SystemVerilog.us:

Dear Ben,

thank you for your example and explanation.

Can you please explain me why e_rose is generated two times each time the testSignal rose? When the clocking event is specified to @(posedge clk), I would have expected that it only happens at the positive clock edge, not at the positive edge of testSignal.

I put this code into a module for formal verification. I was actually surprised that I can use $rose outside a property, because I thought the always blocks would be synthesized. I am not sure how $rose is behaving in synthesized code.

And then I am wondering how using the signal in an always block can have an influence on the coverability of the cover property. Do you know that?

Thank you,
K.

4

In reply to katce:

Because @(expr) means suspend the process until the expression changes. So the event e_rose gets generated when $rose goes from 0 to 1 and 1 to 0. You would really need

@(posedge $rose(testSignal, @(posedge clk)))

You can use $rose, $fell, etc. outside a property. See 16.9.3 Sampled value functions in the 1800-2017 LRM. But using $rose inside a procedural event control statement makes for a very unclear clocking context.

Use Ben’s solution.

5

Ż*In reply to dave_59:*

On always @($rose(testSignal, @(posedge clk)))
I see it triggering when testsignal rises 2ns after the posedge clk.
But the $rose should be tested @posedge clk.
Question: why then is the always @($rose(testSignal, @(posedge clk)))triggering?
At that time (2ns after the posedge of clk) there is no $rose tested in the clk edge that occurred 2ns before the testsignal changes.
Looks like the $rose is ignoring the specified clk edge.
Agree, this is a very unusual way of using the $rose.
Ben

6

In reply to ben@SystemVerilog.us:

As $rose is being used as a function inside an event expression, the expression triggers when the inputs to the function change.