Assertion to check async signals toggling

SystemVerilog
1

Hi,

I have a signal “a” which toggles asynchronously. based on signal “a” toggling, signals “b”, “c”, “d” toggles exactly like “a”. There are some signals “x”, “y”, “z” do not affect that is they are stable. How do I write an assertion/checker to check signals “b”, “c”, “d”, “x”, “y”, “z” behaviour based on signal “a”?

Thanks,
AJ

2

[code]In reply to Anudeep J:
Unchecked code:
You can do something like this


 
module m;
  bit a, b, x, a_ocr, b_ocr, x_ocr; // ocr for occurred
  always @(posedge b) begin b_ocr=1; #1 b_ocr=0; end 
  always @(posedge x) begin x_ocr=1; #1 x_ocr=0; end 
  always @(posedge a) begin a_ocr=1; #1 a_ocr=0; end 
  always_comb 
     assert #0 (a_ocr && b_ocr && !x_ocr); else $display("Error in abx");
endmodule
3

In reply to Anudeep J:

Try


  always @(a) begin
    chk_b_same_as_a : assert (a <-> b);
  End

Cheers
Srini

4

In reply to Srini @ CVCblr.com:
**always @(a) chk_b_same_as_a : assert (a ↔ b);
**
Works if a and b togle at the same frequency.
If a toggles at half the rate as b, it would not catch the error.
It’s the aliasing effect.
What is the aliasing effect? The aliasing effect is a measurement error in the signal occurring due to an incorrectly set sampling rate. If the sampling rate is too low, the Nyquist-Shannon sampling theorem is not observed and thus the measurement signal is not acquired correctly.

How about
always @(a or b) chk_b_same_as_a : assert (a==b); // (a ↔ b);

Ben

5

In reply to ben@SystemVerilog.us:

OP wrote:

toggles exactly like “a”.

So I would guess the FREQ is also same.

Regards
Srini

6

I tried the below code for signal following:

always @(a) begin
  a1: assert (b === c) else $error("error");
  a2: assert (a === c) else $error("error");
end

But the above code fails at my first instant where a and b is going from x → 0. In the waveform, they are actually following, all the three signals are same including the toggles. But in the else part when I try printing the values, they are displayed differently. Any idea on why is this happening?

7

In reply to Anudeep J:

Try


always @(a or b or c) begin
  a1: assert final (b === c) else $error("error");
  a2: assert final (a === c) else $error("error");
end

Can use assert #0 instead. Note:
Deferred assertions use #0 (for an Observed deferred assertion) or final (for a final deferred assertion in the Postponed region) after the verification directive.

8

In reply to ben@SystemVerilog.us:

Thanks Ben,

But I want assertion to happen whenever only a changes. It Should not trigger whenever b or c changes.

9

In reply to ben@SystemVerilog.us:

And Also, When we use final or deferred assertion, its the order of execution varies but not sampled value of signals.

10

In reply to Anudeep J:
Your requirements are not clear.

When we use final or deferred assertion, its the order of execution varies but not sampled value of signals.

Now you say the signals are sampled, meaning you have a controlling clock?
Originally, you wrote

I have a signal “a” which toggles asynchronously. based on signal “a” toggling, signals “b”, “c”, “d” toggles exactly like “a”. There are some signals “x”, “y”, “z” do not affect that is they are stable. How do I write an assertion/checker to check signals “b”, “c”, “d”, “x”, “y”, “z” behaviour based on signal “a”?

What issues you see with


always @(a) begin
  a1: assert final (b === c) else $error("error");
  a2: assert final (a === c) else $error("error");
end
11

In reply to ben@SystemVerilog.us:

This is actually throwing an error(value doesnot match) when a,b,c transition exactly at same time. When I print the values both are getting different values. For Eg: If a and b move from x to 1, a gets 1 and b gets x. and its throwing an error

12

In reply to Anudeep J:

Sounds like you may have events triggering event scheduled at different time slot regions.
For example, in relation to signal w, a changes in w’s active region, but b changes in w’s Reactive region. I wrote this test that certainly provided strange results.

How are these signals generated in relation to the SV scheduling? If I pick one signal (e.g., b or clk), in what regions are these other signals generated?

13

In reply to ben@SystemVerilog.us:

Thanks for the update Ben.

The signals are internal to design. There is no clock controlling it and all are asynchronous signals. Iam just taking design hierarchies to assign the values and using them.
I have 3 signals A,B,C. A is driven from Testbench, based on A, B changes and once the B changes, C also changes. I wanted to check these transitions. I hope if I write final, it should work as everything is stabilized at the end of time stamp. But it is not.

14

In reply to Anudeep J:

A is driven from Testbench, based on A, B changes and once the B changes, C also changes. I wanted to check these transitions

When A changes at time t, the simulator iterates thru all these timing slots. All scheduled events at a specific time form an event queue at that time slot. Simulation proceeds by executing and removing all events in the event queue in the current simulation time slot before moving on to the next non-empty time slot, in time order.

at my first instant where a and b is going from x → 0. In the waveform, they are actually following, all the three signals are same including the toggles. But in the else part when I try printing the values, they are displayed differently. Any idea on why is this happening?

No I do not understand why unless when A changes B changes after a small delay and the C also changes after another delay. This would be true in a hardware implementation with gate delays.
The resolution on the waveforms may limit the view of those delays. A solution:


// Adding a delay, something like #1 or #2 or #3 maybe needed to allow the 
// asynchronous machine to settle after the gate delays
always @(a) begin
 fork 
  #1 a1: assert (b === c) else $error("error"); // final may not be needed
  #1 a2: assert (a === c) else $error("error");
 join_none
end