Write an SVA - if signal b rose high then in the past {x:y] cycle signal a should be high . I am only aware of $past which checks at a particular cycle in the past , how to take care in case we need to check for few cycles in the past

SystemVerilog
2

https://www.perplexity.ai/search/write-an-sva-for-a-scenario-if-s2m4Dw.JSXCGhbABrLofjA
.```
Write an SVA for a scenario - if signal ‘b’ rose high then in the past {x:y] cycle signal ‘a’ should be high . Don’t want the check in the reverse way

I am only aware of $past which checks at a particular cycle in the past , how to take care in case we need to check for few cycles in the past.
Use support logic with a shift register

SVA for “If signal ‘b’ rose high, then in the past {x:y] cycles signal ‘a’ should be high”

To express the requirement:
Whenever signal ‘b’ rises (i.e., $rose(b)), signal ‘a’ should have been high at least once in the range of cycles from x to y cycles before the current cycle (exclusive of the current cycle).

Why $past Alone Is Not Enough

SystemVerilog’s $past(signal, N) only checks the value of signal exactly N cycles ago, not over a range of cycles. You cannot write $past(a, x:y); this is illegal syntax[2]. To check a range in the past, you need to either:

  • Use a sequence with delays and the .triggered method, or
  • Use support logic like a shift register to store the past values of a and check the range explicitly[2][5].

Solution 1: Using Support Logic (Shift Register)

Support logic approach:
Create a shift register to store the last y cycles of a. Then, when $rose(b), check that at least one of the bits corresponding to cycles x to y in the past is high.

Example for x=2, y=5

// Support logic: shift register for 'a'
logic [5:1] a_hist;
always_ff @(posedge clk) begin
    a_hist <= {a_hist[4:1], a};
end

// Assertion: On $rose(b), 'a' was high in any of cycles 2, 3, 4, or 5 ago
ap_b_a_past: assert property (
    @(posedge clk)
    $rose(b) |-> (|a_hist[5:2])
);
  • a_hist[2] is the value of a 2 cycles ago, a_hist[5] is 5 cycles ago.
  • (|a_hist[5:2]) checks that at least one of these bits is high[2].

Generalized for x and y (x < y):

logic [y:1] a_hist;
always_ff @(posedge clk) begin
    a_hist <= {a_hist[y-1:1], a};
end

ap_b_a_past: assert property (
    @(posedge clk)
    $rose(b) |-> (|a_hist[y:x])
);

Solution 2: Using SVA Sequences and .triggered

Alternatively, you can use a sequence to check if a was high at any time in the range [x:y] cycles ago, and then use .triggered in the property[2][5].

sequence a_in_past_range;
    ##[x:y] a;
endsequence

ap_b_a_past: assert property (
    @(posedge clk)
    $rose(b) |-> a_in_past_range.triggered
);
  • This sequence starts when $rose(b) occurs and looks for a being high in any cycle between x and y cycles ago[5].

Summary Table

Approach Code Example (for x=2, y=5) Notes
Shift Register See above Most flexible, works for any condition
SVA Sequence See above Concise, leverages .triggered

Key Points

  • $past(a, N) only checks a single cycle in the past, not a range[2].
  • To check a range, use a shift register or a sequence with .triggered[2][5].
  • Both methods avoid checking in the “reverse” direction (i.e., they only check when b rises, not when a is high).

This approach is widely used for such “window in the past” checks in SVA[2][5].

Citations:
[1] System Verilog Assertions Simplified - Design And Reuse System Verilog Assertions Simplified
[2] [PDF] 1 SUPPORT LOGIC AND THE ALWAYS PROPERTY - Ben Cohen https://systemverilog.us/vf/support_logic_always.pdf
[3] Way to write assertion to check an signal has been set from past time Way to write assertion to check an signal has been set from past time
[4] usage of $past macro in system verilog for a signal to high https://stackoverflow.com/questions/61971883/usage-of-past-macro-in-system-verilog-for-a-signal-to-high
[5] What is the best way to check an event occurred in the past in SVA? https://stackoverflow.com/questions/56978167/what-is-the-best-way-to-check-an-event-occurred-in-the-past-in-sva
[6] What is the best way to check an event occurred in the past in SVA? https://stackoverflow.com/questions/56978167/what-is-the-best-way-to-check-an-event-occurred-in-the-past-in-sva
[7] SystemVerilog assertion Sequence - Verification Guide SystemVerilog assertion Sequence - Verification Guide
[8] Assertion | EasyFormal Assertion | EasyFormal
[9] Using $past for range of cycles - SystemVerilog - Verification Academy Using $past for range of cycles
[10] Check is a signal is stable for the past ‘n’ clock cycles - SystemVerilog Check is a signal is stable for the past 'n' clock cycles
[11] Assertion to check variable distance of two signals - SystemVerilog Assertion to check variable distance of two signals
[12] SystemVerilog Assertions Basics SystemVerilog Assertions Basics - systemverilog.io
[13] Verifying time based signal assertions? : r/FPGA - Reddit https://www.reddit.com/r/FPGA/comments/o2tw0b/verifying_time_based_signal_assertions/
[14] System Verilog Assertion Constructs (1) - The Octet Institute System Verilog Assertion Constructs (1) | The Octet Institute
[15] How to verify the duration of any signal using SVA? - The Vtool How to verify the duration of any signal using SVA? - Career in ASIC Design/Verification, Embedded
[16] How to implement an 8bit Shift Register (left/right) using Verilog https://www.youtube.com/watch?v=nhrir0r8JcI
[17] Retrieving a particular previous value from a shift register. Retrieving a particular previous value from a shift register. - NI Community
[18] How can I use a shift register in this way? : r/FPGA - Reddit https://www.reddit.com/r/FPGA/comments/lcikvk/how_can_i_use_a_shift_register_in_this_way/
[19] SN54HC595: How to make a test for testing the shift register’s basic … SN54HC595: How to make a test for testing the shift register's basic functionality - Logic forum - Logic - TI E2E support forums
[20] Verilog Shift Register with Two Inputs - Electronics Stack Exchange https://electronics.stackexchange.com/questions/232870/verilog-shift-register-with-two-inputs
[21] GUBBALA GIRIDHAR VENKATESH’s Post - LinkedIn Exploring SIPO Shift Registers in Verilog | GUBBALA GIRIDHAR VENKATESH posted on the topic | LinkedIn
[22] [PDF] SVA Advanced Topics: SVAUnit and Assertions for Formal https://www.accellera.org/images/resources/videos/SystemVerilog_Assertions_Tutorial_2016.pdf
[23] Shift Register Implementation - SystemVerilog - Verification Academy Shift Register Implementation
[24] [SOLVED] - How to use shift in SystemVerilog - Forum for Electronics [SOLVED] - How to use shift in SystemVerilog ? | Forum for Electronics
[25] Assertion to check a signal asserting before or after few clock cycles Assertion to check a signal asserting before or after few clock cycles
[26] SystemVerilog Assertions Tutorial - Doulos SystemVerilog Assertions Tutorial
[27] [SVA] signal rise and stay stable → how to write an assertion? AMD Customer Community
[28] Need help with understanding SVA (systemverilog assertions) - Reddit https://www.reddit.com/r/FPGA/comments/ihhzsa/need_help_with_understanding_sva_systemverilog/
[29] Basic Assertions Examples Part-2 | The Art Of Verification https://theartofverification.com/assertions-examples-part-2/
[30] System Verilog Assertions Simplified - eInfochips https://www.einfochips.com/blog/system-verilog-assertions-simplified/
[31] [PDF] Overcoming SystemVerilog Assertions limitations through temporal … https://www.syosil.com/images/resources/DVConEU2022.pdf
[32] Shift Operator - Verilog Example - Nandland Shift Operator - Verilog Example
[33] Using Sequence Properties to Verify a Serial Port Transmitter Using Sequence Properties to Verify a Serial Port Transmitter

1 Like