[SVA] How to write assertion including all below requirements in single assertion

SystemVerilog
,
1

Hi,

Can someone help me with this requirement.

My requirements for this checker are:

  1. Once request asserted with in 250us ack should get asserted.
    2.ack should be 1 throught req is 1.
    I had tried to write code using throught/until_with constructs…but there is something missing, My assertion is failing.
    3.then ack should deassert when req gets deasserted.

I gave some of the tries as below:
property assert_chk1(req,ack);
@(posedge test_clk)
//($rose(ack) && req== 'h1) |-> $stable(ack) throughout (!(req)[->1]); //250us
//($rose(ack) && req== 'h1) |-> ack until_with !req; //250us
//($rose(ack) && req== 'h1) |-> ack throught !req; //250us
$rose(ack) && req== 'h1) |-> $fell(ack) throught !req; //250us
endproperty

2

In reply to BhaRath@Intel:

Hi
Probably below assertion could work.
Property assert_chk1(req,ack);
@(posedge test_clk)
$rose(req) |-> ##[1:250] ack ##1 ack throughout req ##1 !ack && !req ;
endproperty

3

In reply to Nishikant Tayde:
Hi Nishikant,

Good try…

I had tried your code but ended up with below compilation error:

**Error-[SVATHTLHS] Temporal LHS of ‘throughout’ operator.
stability_chk.sv, 5
A temporal LHS is not allowed with the ‘throughout’ operator.
Expression: (( ##[1:250] ack) ##1 ack throughout req ##1 ((!ack) && (!req)))

Please correct and try again.**

I had updated the code and ran like below,



module stability_chk;

  logic clk,rst,req=0,ack=0;

        property assert_chk1(req,ack);
          @(posedge clk)
          $rose(req) |-> ##[1:250] ack ##1 ($stable(ack) throughout (req[->1])) ##1 (!ack && !req) ;
            //$rose(req) |-> ##[1:250] ack ##1 ack throughout req ##1 (!ack && !req) ;
            //$rose(req) |-> ##[1:250] ack ##1 ack throughout req ##1 !ack && !req ;
        endproperty
      STABILITY_CHK:assert property (@(posedge clk) disable iff(rst)    assert_chk1(req,ack));


  initial begin
    clk=0;
    forever #5 clk=~clk;
  end
  initial begin
   #10 req=1; 
   #5 ack=1;
   #50 req=0; ack=0;
   #100;
   $finish;
  end
endmodule

Now I see assertion is shown as “No Match”. Please help me to resolve this issue.

Regards
Bharath

4

In reply to BhaRath@Intel:

I had updated my checker as below, Now I can see assertion is failing at least.

But it is failing immediately after req asserted and it is failing in the next clock where it is finding ack asserted.

$rose(req) |-> ($rose(ack),cnt=0) ##1 (stable(ack) && cnt<200,cnt+=1) ##[0:] req[->1] ##1 (!ack && !req) ;

actually, 1.my expectation is to make sure ack is stable until req is high.
2. ack should be asserted once req asserted within specific clocks.

5

In reply to BhaRath@Intel:

In reply to BhaRath@Intel:
I had updated my checker as below, Now I can see assertion is failing at least.
But it is failing immediately after req asserted and it is failing in the next clock where it is finding ack asserted.
$rose(req) |-> ($rose(ack),cnt=0) ##1 (stable(ack) && cnt<200,cnt+=1) ##[0:] req[->1] ##1 (!ack && !req) ;
Below logic helped me for to check if 1.ack is stable or not after req asserted and once ack asserted.

  1. My question is that does this checkers fail is ack doesn’t assert?
    3.##[1:250]-> How can I avoid this delay before ack assertion check?
    $rose(req) |-> ##[1:250] ($rose(ack),cnt=0) ##1 (stable(ack) && cnt<200,cnt+=1) ##[1:] !req[->1];
    actually, 1.my expectation is to make sure ack is stable until req is high.
  2. ack should be asserted once req asserted within specific clocks.

Thank you for your help in advance.

6

In reply to BhaRath@Intel:

You can try any one of these two properties, I tried it locally seems to be working, feel free to improvise


  property REQ_ACK1(clk, rst, req, ack); 
    @(posedge clk) disable iff (rst) $rose(req)|-> ((req throughout ack[->1]) intersect 1[*1:250]) ##1 (!req && !ack);
  endproperty

    property REQ_ACK(clk, rst, req, ack);
    int count; 
      @(posedge clk) disable iff (rst) ($rose(req), count = 0) |-> (((req, count++) throughout ack[->1]) ##0 (count < 251)) ##1 (!req && !ack) ##0 (1, $display("The value of count is %d", count));
  endproperty
  
  assert property(REQ_ACK(clk, rst, req, ack));

Here is the EDA link Edit code - EDA Playground