Timing Assertions.

Question

The following scenario should give errors as assertions should be violated (on purpose). But, the check is extending from one "run" to the next, and the assertion is being checked as valid.

I've used $rose(valid) so that the assertion begins only when valid has asserted HIGH, not for every clock cycle it finds valid to be high. Is there a better way to do this?? as this makes the assertion start at 20ns, while valid was asserted HIGH at 10ns.

module assertions_1;
    bit valid, ready, clk;
 
    always #5 clk = ~clk;
 
    initial begin
        repeat (5) run();
        repeat (5) begin @(negedge clk); 
        end 
        $finish;
    end
 
    task run();
        @(negedge clk) valid = 1;
        repeat ($urandom_range(1,4)) begin 
            @(negedge clk);
        end 
        ready = 1;
        @(negedge clk) ready = 0; valid = 0;
    endtask
 
    property RUN;
        @(negedge clk) $rose(valid) |-> valid ##[6:10] $stable(valid) && ready;
    endproperty
 
    assert property(RUN) $display($time, "ns Signal Transition is ok");
        else $error($time, "ns Signal Transition has Issues");
 
endmodule

Answer 1

ben@SystemVerilog.us

Full Access

2600 posts

January 03, 2023 at 9:50 am

In reply to Husni Mahdi:
1) You need the $rose(valid). I don't see any issue with your assertion. On your TB, I prefer to use nonblocking assignments as a style, though the model would work.
2) $rose(valid) |-> valid // at $rose(valid) valid==1, thus the valid in the consequent is not needed

task run();
        @(negedge clk) valid <= 1; 
// the valid=1 works because signals are sampled and 
//   use the values of the Preponed region of the time stamp.
        repeat ($urandom_range(1,4)) begin 
            @(negedge clk);
        end 
        ready <= 1;
        @(negedge clk) ready <= 0; valid <= 0;
    endtask
 
property RUN;
        @(negedge clk) $rose(valid) |-> ##[6:10] $stable(valid) && ready;
    endproperty

Ben Cohen
http://www.systemverilog.us/
** SVA Handbook 4th Edition, 2016 ISBN 978-1518681448
...
1) SVA Package: Dynamic and range delays and repeats https://rb.gy/a89jlh
2) Free books:
* Component Design by Example https://rb.gy/9tcbhl
* Real Chip Design and Verification Using Verilog and VHDL($3) https://rb.gy/cwy7nb
* A Pragmatic Approach to VMM Adoption
http://SystemVerilog.us/vf/VMM/VMM_pdf_release070506.zip
http://SystemVerilog.us/vf/VMM/VMM_code_release_071806.tar
3) Papers:
Understanding the SVA Engine,
https://verificationacademy.com/verification-horizons/july-2020-volume-16-issue-2
Reflections on Users’ Experiences with SVA, part 1
https://verificationacademy.com/verification-horizons/march-2022-volume-18-issue-1/reflections-on-users-experiences-with-systemverilog-assertions-sva
Reflections on Users’ Experiences with SVA, part 2
https://verificationacademy.com/verification-horizons/july-2022-volume-18-issue-2/reflections-on-users-experiences-with-sva-part-2
Understanding and Using Immediate Assertions
https://verificationacademy.com/verification-horizons/december-2022-volume-18-issue-3/understanding-and-using-immediate-assertions
SUPPORT LOGIC AND THE ALWAYS PROPERTY
http://systemverilog.us/vf/support_logic_always.pdf
SVA Alternative for Complex Assertions
https://verificationacademy.com/news/verification-horizons-march-2018-issue
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
SVA for statistical analysis of a weighted work-conserving prioritized round-robin arbiter.
https://verificationacademy.com/forums/coverage/sva-statistical-analysis-weighted-work-conserving-prioritized-round-robin-arbiter.
Udemy courses by Srinivasan Venkataramanan (http://cvcblr.com/home.html)
https://www.udemy.com/course/sva-basic/
https://www.udemy.com/course/sv-pre-uvm/

Answer 2

Solution

dave_59

Forum Moderator

10661 posts

January 03, 2023 at 11:56 am

In reply to Husni Mahdi:

By saying you don't want the assertion checking "from one "run" to the next", I think you want this to fail if valid falls and ready has not been asserted. I think you might look to see if this meets your needs:

$rose(valid) |-> ready[=1] within valid[*6:10];

— Dave Rich, Verification Architect, Siemens EDA

Answer 3

Husni Mahdi

Full Access

16 posts

January 08, 2023 at 8:41 pm

In reply to dave_59:

Thank You Mr. Dave,
This was what I was looking for.

But there remains an issue, I made slight changes, so that ready triggers, 4 to 7 clocks cycles after valid is HIGH. And the assertion will pass for when ready is triggered 6:10 cycles after valid.

    task run();
        @(negedge clk) valid <= 1;
        repeat ($urandom_range(4,7)) begin 
            @(negedge clk);
        end 
        ready <= 1;
        @(negedge clk) ready <= 0; valid <= 0;
    endtask
 
    property RUN;
//        @(negedge clk) $rose(valid) |-> ##[6:10] $stable(valid) && ready;
        @(negedge clk) $rose(valid) |-> ready[=1] within valid[*6:10];
    endproperty

In this case, it shows error for 4 cycle delay. And shows passed for 6 and 7 cycle delays i.e., as we want it to behave.

But for delays of 5 cycle it shows passed, but that should also state an error, as the least delay should be 6 cycles.

Answer 4

Husni Mahdi

Full Access

16 posts

January 08, 2023 at 9:02 pm

In reply to dave_59:
Also, in case of $rose(valid) will start the assertion the next clock after the valid has actually gone HIGH. While stating only "valid" starts the assertion on every negative clock edge it finds valid to be HIGH.

Is there any way to start the assertion on exactly the time valid has gone HIGH and only then not every time the edge finds valid HIGH??

Answer 5

Mrutunjay

Full Access

4 posts

February 23, 2023 at 2:02 am

In reply to ben@SystemVerilog.us:

Write assertion for signal "B" will be low after the start bit becomes high within the range of [4:15] clock cycles. "B" will be high at posedge of "A" till this time "B" should be low. See the below diagram for reference.

Answer 6

Shubhabrata

Forum Access

94 posts

February 23, 2023 at 2:19 am

In reply to Mrutunjay:

clocking df_clk @(posedge clk);
endclocking
default clocking df_clk;
property p1;
$rose(start)|-> ##[4:15] $fell(B) ##0 !B[*1:$] ##1 $rose(A) ##0 B;
endproperty
assert property (p1);

- I guess this will satiate your requirement. I am unsure whether I should use first_match over here cause I am assuming the tool will automatically defenestrate other possible scenarios.

Answer 7

Husni Mahdi

Full Access

16 posts

February 23, 2023 at 9:05 am

In reply to Shubhabrata:

What is the purpose of the clocking block here.

Answer 8

kddholak

Full Access

101 posts

February 23, 2023 at 10:02 am

In reply to Mrutunjay:

property check_b ;
 start && b && !a|-> ##[4:15] !b ;
endproperty 
 
property check_a_b ;
 start && a |-> b ;
endproperty 
 
property check_a_b ;
 start && a && $fell(b) |-> what will happen to a ? ;
endproperty

Answer 9

Shubhabrata

Forum Access

94 posts

February 23, 2023 at 9:57 pm

In reply to Husni Mahdi:

Nothing special. I used a default clocking for this assertion. It id one of the ways to mention clocking edge.

Languages & Standards

Methodologies

Techniques & Tools

Universal Verification Methodology (UVM)

Featured Courses

Additional Courses

Formal-Based Techniques

Analog/Mixed Signal

UVM Forum

SystemVerilog Forum

Coverage Forum

Additional Forums

Implementation Patterns

Specification Patterns

Pattern Resources

UVM Cookbook

Coding Guidelines & Deployment

Coverage Cookbook

Featured & On-Demand

On-Demand Library

Recording Archive

Conferences & WRG

Siemens EDA Learning Center

Blog & News

Verification Horizons Publication

About Us

Training

Solution

Portfolio

Explore

Siemens

Contact