External clk to Assertion inside SV bind construct

SystemVerilog
,
1

Hello,

I am using SV assertions inside a module which I then “bind” to the RTL module to validate some protocol.

The problem is the the clock inside the module is gated and does not arrive at the fixed time. So that causes the assertion to be a hit and miss as sometimes they don’t fire at all.

This block is instantiated a lot throughout the code and I really need a reliable clock for synchronization.

Is there a way to pass a “clk” as signal at higher level than the instance to which the bind module is hooked on?

For e.g.,

**bind leaf check check_i ();
**
top
|__ non-leaf
|__ leaf

Can I use the clk at non-leaf for my assertions inside the check module hooked at leaf?

Thanks.

2

In reply to cooltoad:

Am I missing something here.?
When you do the bind of check to the DUT, you are passing as arguments the desired clk as an actual to the formal of the check clk.
Hierarchical paths can be used.
Clarify your question.
Ben Ben@systemverilog.us

3

Okay, I was under the impression that if bind happens to a particular instance, you cannot access signal in a module above that instance in the hierarchy.

But it seems that can be done.

I have a follow-up question though, I don’t think clock is my issue at all.

I have the following assertion,

@(posedge clk)
req ##[] en1 ##[] en2 ## [*] en3 |-> grant

Basically, if there is a request, provide grant exactly in the same cycle when all enables, en1, en2, en3 are valid. They could toggle independently of each other.

I also tried writing it in a different way,

@(posedge clk)
req ##[*] ((en1 & en2 & en3) === 1’b1) |-> grant

The assertion fires at req and fails one cycle after all enables become high.

Can you help me understand what I might be missing here?

4

In reply to cooltoad:
from my SVA Handbook 4th Edition, 2016

  • An antecedent with an infinite range (delay range or repetition range) will initiate an infinite number of threads. For the assertion to not fail, all threads of the antecedent and and their corresponding consequents must be evaluated. Since there are an infinite number of threads to be tested, the assertion can never successfully terminate. However, a failure of a matched antecedent / consequent pair will cause the assertion to fail.
  • An assertion of a property that has an antecedent with an infinite range, and without a first_match operator, will never succeed, but can fail (a first_match ignores the other matches). Consider the following example:
 ap_never_succeed_multithreaded_and_not_unique: assert property( a ##[2:$] b |=> c);
ap_can_succeed_and_unique: assert property(first_match($rose(a) ##[2:$] b) |=> c); //
// Also OK, and stylish
ap_can_succeed_and_unique2: assert property($rose(a) ##2 1'b1 ##0 b[->1] |=> c); //
// b[->1] is equivalent to: !b[*0:$] ##1 b
  • Guideline: 1) When defining sequences that are used as antecedents, insure uniqueness in its triggering condition to avoid unexpected results, such as assertions that can never succeed or fail in unintended situations. For example, if only a new occurrence of a signal is needed to start the evaluation of an assertion use of an edge detect (e.g., $rose(signal) of the first element of the sequence or a single trigger pulse condition, such as a one clock enable signal.

For your assertion do one of the following:


// req ##[*] ((en1 & en2 & en3) === 1'b1) |-> grant;
$rose(req)##1 (en1 && en2 && en3)[->1]  |-> grant // use the $rose
// If the enables are independent and at different times, then 
$rose(req) ##1 (en1[->1] and en2[->1] and en3[->1])  |-> grant;
// or 
$rose(req) ##0 first_match(##[*](en1 && en2 && en3))  |-> grant;
// Use the && logical ANDing

Ben Cohen
http://www.systemverilog.us/ ben@systemverilog.us
For training, consulting, services: contact Home - My cvcblr

5

Thanks a lot. That helped!