Assertion for conditional sgnal monitoring

SystemVerilog
1

Hi all, I want to implement below specification using assertion .

I have four signals: sig_a, sig_b, sig_c, and sig_d. Each can be masked/unmasked and has a 2-bit setting for each signals specifying one of these conditions: Level 1, Level 0, Posedge, or Negedge.

When enable is triggered, monitor only the unmasked signals and ensure they meet their specified conditions based on their setting. The ready signal must stay low until all the unmasked signals are triggered.

Note: There will be always one unmask signal after enable is triggered.

2

Your requirements are very ambiguous.
I have NO idea as to what you are talking about. I tried perplexity.ai and it gave me the following, which confused me even more.

To implement the described requirements, you'll need to create a monitoring system with the following components:
Four signals: sig_a, sig_b, sig_c, and sig_d
A mask for each signal (4 mask bits total)
A 2-bit setting for each signal (8 bits total)
An enable signal
A ready signal
Signal Settings
Each signal has a 2-bit setting that specifies one of four conditions:
Setting	Condition
00	Level 1
01	Level 0
10	Posedge
11	Negedge
Monitoring Logic
When the enable signal is triggered, the system should:
Identify which signals are unmasked
Monitor only the unmasked signals
Check if each unmasked signal meets its specified condition
The ready signal should:
Stay low until all unmasked signals have met their conditions
Go high once all conditions are met
There will always be at least one unmasked signal after enable is triggered
3

There are four signals: sig_a, sig_b, sig_c, and sig_d, each with:

  1. A mask configuration (sig_a_mask, sig_b_mask, sig_c_mask, sig_d_mask) to determine whether the signal is considered (1 = active, 0 = ignored).
  2. A setting configuration (sig_a_cfg[1:0], sig_b_cfg[1:0], sig_c_cfg[1:0], sig_d_cfg[1:0]) specifying the trigger condition:
  • 00: Wait for Level 1
  • 01: Wait for Level 0
  • 10: Wait for Posedge
  • 11: Wait for Negedge

Example1:

  • Mask values: sig_a_mask = 1, sig_b_mask = 0, sig_c_mask = 1, sig_d_mask = 1.
  • Configuration values: sig_a_cfg = 2'b01, sig_b_cfg = 2'b10, sig_c_cfg = 2'b00, sig_d_cfg = 2'b11.

Since sig_b_mask = 0, sig_b is ignored, and only sig_a, sig_c, and sig_d are considered.

Requirement:

Once enable is triggered, the ready signal must remain 0 until:

  • sig_a sees a Level 0 (cfg = 01),
  • sig_c sees a Level 1 (cfg = 00), and
  • sig_d sees a Negedge (cfg = 11).

Example2:

  • Mask values:
    sig_a_mask = 0, sig_b_mask = 1, sig_c_mask = 1, sig_d_mask = 0.
  • Configuration values:
    sig_a_cfg = 2'b10, sig_b_cfg = 2'b11, sig_c_cfg = 2'b00, sig_d_cfg = 2'b01.

Since sig_a_mask = 0 and sig_d_mask = 0, both sig_a and sig_d are ignored. Only sig_b and sig_c are considered:

  • sig_b_cfg = 2'b11: Wait for a Negedge on sig_b.
  • sig_c_cfg = 2'b00: Wait for Level 1 on sig_c

Requirement:

Once enable is triggered, the ready signal must remain 0 until:

  1. A Negedge occurs on sig_b (because sig_b_cfg = 11), and
  2. A Level 1 occurs on sig_c (because sig_c_cfg = 00).
1 Like
4

we can use for loop to write assertion for each signal. if each assertion is pass, then ready signal remain 0 until all unmasked signals are triggered.

sequence seq1(setting, signal);
if(setting == 0)
signal_wait_for_level1;
else if(setting == 1)
signal_wait_for_level2;
else if(setting == 2)
$rose(signal);
else if (setting == 3)
$fell(signal);
endsequence

property P1(mask, setting, signal);
@(posedge clk)
(enable && mask) |=> (ready == 0) until seq1(setting, signal).triggered[->1];
endproperty

generate
for (genvar i =0; i<4; i++)
assert property (P1(mask[i], setting[i], signal[i]));
endgenerate

5

Thanks @flyant . This will work i think. I have thought of another method:

sequence s1;
(sig_a_mask && ( ((sig_a_cfg == 2'b00) && sig_a) || ((sig_a_cfg == 2'b01) && !sig_a) || ((sig_a_cfg == 2'b10) && $rose(sig_a)) || ((sig_a_cfg == 2'b11) && $fell(sig_a))) || !sig_a_mask) [->1];
endsequence : s1

Similar sequence for sig_b,sig_c,sig_d.

Then using all these sequences in the final property as :

property sig_monitor;
 $rose(enable) |-> !ready throughout (s1 and s2 and s3 and s4);
endproperty

What is your opinion about this method?

6

it only works if s1, s2, s3 and s4 finish at the same time.

7

Why? When we use and operator , the endpoint for different sequence can be different right(So in this sequence s1,s2,s3,s4 can have different endpoints)?

8

I just feel confused.

If s1 finishes at 10ns, s2 finishes at 15ns, s3 finishes at 20ns, s4 finishes at 25ns

what’s the endpoint for (s1 and s2 and s3 and s4)?

9

So endpoints for s1 will 10ns, for s2 it will be 15ns, for s3 it will be 20ns and for s4 it will be 25ns and the consequent (s1 and s2 and s3 and s4) will finally match at 25ns

10

I find the same question. AND operation on sequences in assertions - #5 by sasi_8985

yes, you are right. I think your assertion should work. thanks for let me know. I never used “sequence and” before.

11

I would prefer Separate throughout assertions, one for each sequence;
It’s clearer and easier to debug.
Might also be better for Formal.
I never used this “and” with the intersect or throughout.
See my paper

12

Thanks Ben, I will look into it.