SVA - reverse evaluate

SystemVerilog
,
1

Hi
For some reasons I need to evaluate sequence from the end to the start.
if “target” changed from '0 to '1, so:
a) “clear” was '0 in the previous clock cycle.
b) “enable” was '1 in the previous clock cycle.
c) “rstn_a” must be '1 all over the flow.
d) when “d_in” changed from '0 to '1, “rstn_b” have to be '1, until the clock cycle where “enable” should be '1 (one cycle before “target” changed to '1 from '0).

Again, the assert start only after I know that target rise.

Do you have any suggestion?

Thanks a lot!

2

Did you consider $past usage? I suggest you break your above steps to a few simple SVAs and code, as an example:

/*if “target” changed from '0 to '1, so:
a) “clear” was '0 in the previous clock cycle. */

  $rose(target) |-> !$past(clear)

Good luck

3

thanks
can I use $past for unknown amount of time?
section “d” above require rely on the other parts - the number of clocks is unknown, I just know that now target rise, so clock before enable were '1, and all the time before the enable condition, since d_in came, rstn_b must be '1…

4 
 “target” changed from '0 to '1, so:
a) “clear” was '0 in the previous clock cycles (over the flow)
b) “enable” was '1 in the previous clock cycle.
c) “rstn_a” must be '1 all over the flow.
sequence s_clear; 
 @(posedge clk) clear[->1] intersect rstn_a[*1:$]; 
endsequence
assert property(@(posedge clk) $rose(clear) |-> 
                      s_clear.triggered && $past(enb));

[You] d) when “d_in” changed from '0 to '1, “rstn_b” have to be '1,
 until the clock cycle where “enable” should be '1 (one cycle before “target” changed to '1 from '0).
 [Ben]  ?? 
 sequence s_enb; 
    @(posedge clk)  rstn_b[*1:$] interesect enb[->1] ##1 1;
 endsequence 
assert property(@(posedge clk) $rose(din) |-> s_enb.triggered);

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

5

Hi Ben
Thanks for your reply.
I can’t see where, in your code, is there a reference to “target”, and to the fact that the entire check is performed on the time prior to its increase.
Thanks again

6 
sequence s_clear; 
 @(posedge clk) clear && target [->1] intersect rstn_a[*1:$]; 
endsequence
assert property(@(posedge clk) $rose(target) |-> 
                      s_clear.triggered && $past(enb));

WOuld that work?
Othewise, you can use the same framework or approach to add the endpoint od target.