Assertion for check between signals changing on different edges of same clock

Question

Hi All,

How to write an assertion for following case-
There are 2 signals a, b. Signal a is synchronous to negedge of clk and Signal b synchronous to posedge of clk.
Whenever signal a falls at a negedge of clk, at the immediate following posedge of clk,signal b should fall.
clk is same for a, b.

Any alternative to assertion will also be helpful.

Any help would be appreciated

Answer 1

ben@SystemVerilog.us

Full Access

2988 posts

June 19, 2020 at 4:01 pm

In reply to verif4life:
As an educator, I am reluctant to answer what you can easily write yourself and learn something in the process. Thus, I suggest that you look into 1800'2017: 16.13.1 Multiclocked sequences. Your requirements are a simple application of that along with the use of the implication operator (|->).
Ben Cohen
http://www.systemverilog.us/
For training, consulting, services: contact http://cvcblr.com/home
* SVA Handbook 4th Edition, 2016 ISBN 978-1518681448
* A Pragmatic Approach to VMM Adoption 2006 ISBN 0-9705394-9-5
* Using PSL/SUGAR for Formal and Dynamic Verification 2nd Edition, 2004, ISBN 0-9705394-6-0
* Real Chip Design and Verification Using Verilog and VHDL, 2002 isbn 978-1539769712
* Component Design by Example ", 2001 ISBN 0-9705394-0-1
* VHDL Coding Styles and Methodologies, 2nd Edition, 1999 ISBN 0-7923-8474-1
* VHDL Answers to Frequently Asked Questions, 2nd Edition ISBN 0-7923-8115
--------------------------------------------------------------------------
1) SVA Alternative for Complex Assertions
https://verificationacademy.com/news/verification-horizons-march-2018-issue
2) https://verificationacademy.com/forums/systemverilog/sva-package-dynamic-and-range-delays-and-repeats
3) 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

Answer 2

verif4life

Full Access

9 posts

June 20, 2020 at 11:56 am

In reply to ben@SystemVerilog.us:

Hi Ben,
This is working in my case.
Can you please check this.
Additionally can you give any way to implement this without assertions.For checking signal fell it checks on two consecutive clock edges, for signal 'a' in my case it is two consecutive negedge, by the time I get a 2nd negedge my signal b falls at posedge. so I am not getting when to start the check on signal b

property p1;
 // @(negedge clk)  !a |-> @(posedge clk)  !b ;  does not actually checks the falling edge
    @(negedge clk)  $fell(a)  |-> @(posedge clk)  $fell(b)  ;
endproperty
 
assert property (p1) ;

Answer 3

rag123

Full Access

237 posts

June 20, 2020 at 12:01 pm

Try this (Haven't tested)

//  There are 2 signals a, b. Signal a is synchronous to negedge of clk and Signal b synchronous to posedge of clk.
//Whenever signal a falls at a negedge of clk, at the immediate following posedge of clk,signal b should fall.
//clk is same for a, b.
 
 ap_arbiter: assert property(first_match(@(negedge clk) $fell (a)) |-> (@(posedge clk) $fell (b)))
            $display ("Assertion passed",$time);
            else $display ("Assertion failed",$time);

Answer 4

verif4life

Full Access

9 posts

June 20, 2020 at 12:41 pm

In reply to rag123:

Thanks for your reply. It is working.
Can you provide a way so that it does not throw an error for the first clock edge??
Here the clock starts after power on reset so cannot use disable iff (rst).. and default value of signal is x and sampled value at first clocking event is 0. So $fell will be true and hence the antecedent..

Also cannot change signal 'a' to bit type because it is an internal DUT signal.. is it good way to take variable in assertion interface as bit type so that it would be automatically typecast x, z to 0???

Answer 5

rag123

Full Access

237 posts

June 20, 2020 at 1:43 pm

In reply to verif4life:

Two options:
1) you can use ##1 delay to avoid the first clocking event.

ap_arbiter: assert property(first_match(@(negedge clk) ##1 $fell (a)) |-> (@(posedge clk) $fell (b)))
2) Use tasks recommended by Ben.
https://verificationacademy.com/forums/systemverilog/paper-understanding-sva-engine-simple-alternate-solutions

For casting, It is always better to do typecast first.

Answer 6

verif4life

Full Access

9 posts

June 20, 2020 at 3:27 pm

In reply to rag123:

Thanks a lot

Answer 7

ben@SystemVerilog.us

Full Access

2988 posts

June 20, 2020 at 4:25 pm

In reply to rag123:

first_match is NOT NEEDED in a single threaded antecedent.
Let's not the kitchen sink at an assertion and hope that it works.
Ben systemverilog.us

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

Portfolio

Explore

Siemens

Contact