System verilog assertion

SystemVerilog
1

I have a signal ‘a’ asserts and then after 10 clock cycles signal’b’ assets(stays high for one clock cycle).Once signal ‘b’ asserts after 10 clock cycles signal ‘c’ shall never assert(signal ‘c’ is by default ‘0’)
I had written like below

property exp;
   @(posedge clk) disable iff (~resetn)
    $rose(a) |-> ##[1:10] $rose (b) |-> ##[1:10] (c !== 1'b1);
  endproperty
  a_exp : assert property (exp) else $fatal("error in assertion");

The above isn’t firing if c asserts
Could you please help what’s wrong in it

Thanks

2

In reply to mahe424:

Requirements:

  • ‘a’ asserts and then after 10 clock cycles signal’b’ assets to 1
  • Once signal ‘b’ asserts after 10 clock cycles signal ‘c’ shall always be 0

// Option 1
property exp;
   @(posedge clk) disable iff (~resetn)
    first_match($rose(a) ##[1:10] $rose (b))|-> always (c !== 1'b1);
  endproperty
  a_exp : assert property (exp) else $fatal("error in assertion");

// Option 2
property exp;
   @(posedge clk) disable iff (~resetn)
     ($rose(a) |-> ##[1:10] $rose (b)) #-# always (c !== 1'b1);
  endproperty
  a_exp : assert property (exp) else $fatal("error in assertion");
// The #-# is the followed-by operator. 

// Option 3, without first_match, which is strongly disliked by my colleague) 
property exp;
   @(posedge clk) disable iff (~resetn)
    ($rose(a) ##[1:10] $rose (b)) intersect b[->1] |-> always (c !== 1'b1);
  endproperty
  a_exp : assert property (exp) else $fatal("error in assertion");

Ben Cohen
Ben@systemverilog.us
Link to the list of papers and books that I wrote, many are now donated.

or Cohen_Links_to_papers_books - Google Docs

Getting started with verification with SystemVerilog

3

In reply to ben@SystemVerilog.us:

If you want to test an assert statement about option 2.

// Option 2
property exp;
   @(posedge clk) disable iff (~resetn)
     ($rose(a) |-> ##[1:10] $rose (b)) #-# always (c !== 1'b1);
  endproperty
  a_exp : assert property (exp) else $fatal("error in assertion");
// The #-# is the followed-by operator.

What approach is proper for you? I want to learn from it.

4

In reply to UVM_LOVE:

In reply to ben@SystemVerilog.us:
If you want to test an assert statement about option 2.

// Option 2
property exp;
@(posedge clk) disable iff (~resetn)
$rose(a) |-> (##[1:10] $rose (b)) #-# always (c !== 1'b1);
endproperty
a_exp : assert property (exp) else $fatal("error in assertion");
// The #-# is the followed-by operator.

What approach is proper for you? I want to learn from it.

I prefer option 2 because the assertion will fail if rose(a)==1 and rose(b) does not occur within 10 cycles.
To test it, write a TB with a small set of directed test vectors.
Ben

5

In reply to ben@SystemVerilog.us:

To test it, write a TB with a small set of directed test vectors.

Could you please let me know how you test with a small set of directed test vector?

6

In reply to UVM_LOVE:
Thank you for your interest in SystemVerilog directed tests. It’s a fundamental skill for working with hardware design and verification. If you’re not familiar with writing simple directed tests in SystemVerilog, I encourage you to explore online resources and tutorials to enhance your understanding. There are many helpful guides available that can provide step-by-step instructions. Developing a strong foundation in this area will greatly benefit your work in the field. Best of luck with your learning journey!

After that, you should start studying constrained-random-tests (CRT), but this is another story.

Ben

7

In reply to ben@SystemVerilog.us:

In reply to mahe424:
// Option 2
property exp;
@(posedge clk) disable iff (~resetn)
($rose(a) |-> ##[1:10] $rose (b)) #-# always (c !== 1’b1);
endproperty
a_exp : assert property (exp) else $fatal(“error in assertion”);
// The #-# is the followed-by operator.

Thanks Ben. If signal ‘c’ shall not assert only for sometime how to add clock cycles to always?

8

In reply to mahe424:

If signal ‘c’ shall not assert only for sometime how to add clock cycles to always?

Your question is ambiguous.

  1. signal c==0 for 30 clocks and then c is a don’t care.
    ($rose(a) |-> ##[1:10] $rose (b)) #-# s_always[0:19] (c !== 1’b1);
  2. signal c==0 for unknown number of cycles until it becomes 1 once
    $rose(a) |-> ##[1:10] $rose (b) ##1 c[->1]
  3. signal c==0 for unknown number of cycles until it becomes 1 once;
    it then stays a c==0
    $rose(a) |-> (##[1:10] $rose (b) ##1 c[->1]) #-# always (c !== 1’b1);

Ben