SVA

SystemVerilog
1

Write an assertion when A goes high,we have to look for value of rose of b or rose of c , during a is high.

basically if a is high from 2ns to 20ns and then falls ,in between 2 ns-20ns we need to check either b or c goes high .If either of two goes high for once the assertions passes if neither of them goes high it fails.
clk time period is 1ns

code attempted

property check;
@(posedge clk) disable iff (reset==0)
a && rose(a) |-> (b | c) ["0:] ##0 a within (a==1);

please suggest
As this code is not executing
As we want the assertion to trigger at when a is high,but check within a is high for b or c.

I do understand that $rose is edge trigger but I want to check at level which is a equal to 1 and show result at edge.

will lock concept work here.

Please advice as requirement is suppose is a is high consider it be request then there should be any response be it dataread or daatawrite which is b and c here.

@

2

In reply to bhajanpreetsinght:

Formal Verification -


// add glue code
logic flg;
always@(posedge clk) begin 
       if(~reset | ~a)
          flg <=0 ;
       else flg <= (b|c) ? 1 : flg;
end
AST_check : assert property (
    @(posedge clk) disable iff (reset==0)
       $fell(a) |-> flg
);
3

In reply to Anjan@FV:

[quote]In reply to bhajanpreetsinght:

Formal Verification -


// add glue code
logic flg;
always@(posedge clk) begin 
       if(~reset | ~a)
          flg <=0 ;
       else flg <= (b|c);
end
AST_check : assert property (
    @(posedge clk) disable iff (reset==0)
       $fell(a) |-> flg
);

[/quote
Hi Anjan,

This code is not working as when will be set to set to 0 initially it doesn’t change

4

In reply to bhajanpreetsinght:

[quote]In reply to Anjan@FV:

Hi Anjan,

This code is not working as when will be set to set to 0 initially it doesn’t change

Hi Bhajanpreet,

It works fine, do check reset. Even if ‘a’ starts from time 0, reset few initial cycles. Else you can modify glue code based on your design specifications.
Your response is unclear; please provide further clarification.

5

In reply to Anjan@FV:

[quote]In reply to bhajanpreetsinght:

I mean it is failing as flag variable goes low initially and then newer changes I am running regularly have you ran this one if so request you to provide simulation or waves result