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

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

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