Assertion

SystemVerilog
,
1

Hi All,
I am writing a assertion for “a” signal should valid until “b” signal set to the value 8’hF. This “b” signal set to any clock we cannot determine. Then “c” signal must be to 8’hF.

  property test;
    @(posedge)  clk
   (a && (##[1:$]b==8'hF) |-> c==8'hF;
  endproperty

  test_checker : assert property(test)
  else
   $error("test property failed");

But i am facing the compilation error. Any one suggest me to how to write the assertion for this scenario.

Thanks in Advance
Rajaraman R

2

In reply to Rajaraman Rak7:


 @(posedge)  clk
   first_match(a[*1:$] ##1 b==8'hF) |-> c==8'hF;

All signals will be sampled @(posedge) clk
Ben systemverilog.us

3

In reply to ben@SystemVerilog.us:

Added the first_match because for the assertion to complete, all threads of the antecedent must be tested.
Ben systemverilog.us

4

Thnks Ben,
Now it’s properly working.
But i need more clarification about the “first_match”.

5

In reply to Rajaraman Rak7:
From my sva book

694×590 47.6 KB

Ben Cohen
http://www.systemverilog.us/ ben@systemverilog.us
For training, consulting, services: contact http://cvcblr.com/home

  1. VF Horizons:PAPER: SVA Alternative for Complex Assertions - SystemVerilog - Verification Academy
  2. http://systemverilog.us/vf/SolvingComplexUsersAssertions.pdf
  3. “Using SVA for scoreboarding and TB designs”
    http://systemverilog.us/papers/sva4scoreboarding.pdf
  4. “Assertions Instead of FSMs/logic for Scoreboarding and Verification”
    https://verificationacademy.com/verification-horizons/october-2013-volume-9-issue-3
  5. 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