SVA to check if the signal changes on the clock edge

SystemVerilog
1

Hi

I am looking for a system verilog assertion to check if the signal changes on the posedge of clock (rising edge of clock and signal are aligned). I tried below assertions but did not seem to work.

assert property (@(posedge clock) (clock & en) |-> $rose(sig_a) )

assert property (@(posedge gsync) (en) |-> sig_a )

but both did not work. Can you please help.

2

In reply to Sudarshan:

I am looking for a system verilog assertion to check if the signal changes on the posedge of clock (rising edge of clock and signal are aligned). I tried below assertions but did not seem to work.
assert property (@(posedge clock) (clock & en) |-> $rose(sig_a) )
assert property (@(posedge gsync) (en) |-> sig_a )
but both did not work. Can you please help.

See discussion at https://verificationacademy.com/forums/systemverilog/sv-assertion/checker-stable-input-posedge-clock.
assertions uses events for the checks, and if in1 changes sometime before the @(posedge clk) the assertion will succeed, instead of failing. Actually, assertions are not intended for timing checks. In the audio field, undersampling is called “aliasing” Aliasing - Wikipedia
The best solution is to use the SystemVerilog timing checks that are defined in the language.

1800:31.3 Timing checks using a stability window wrote:

The following timing checks are discussed in this subclause:
$setup $hold $setuphold
$recovery $removal $recrem
These checks accept two signals, the reference event and the data event, and define a time window with
respect to one signal while checking the time of transition of the other signal with respect to the window. In general, they all perform the following steps:
a) Define a time window with respect to the reference signal using the specified limit or limits.
b) Check the time of transition of the data signal with respect to the time window.
c) Report a timing violation if the data signal transitions within the time window.
Ben Cohen
http://www.systemverilog.us/ ben@systemverilog.us
For training, consulting, services: contact Home - My cvcblr

3

In reply to Sudarshan:

Just make the assertion trigger on every change of the given signal. Do not make the assertion to be synchronous with clock. Here is a similar forum question. Following is the sample code to detect that the signal a is toggling at posedge of clock only.

Basically the assertion checks that whenever a toggles, at that time, a clock event must be triggered.

module top();
  parameter period = 5;
  parameter tgl = 3;
  bit a, clk;
  always #(period) clk = ~clk;
  always #(tgl) a = ~a;
 
  property detect_glitch;
    time leading;                  // declare the last edge occurence variable
    @(a)                      // At every change of glitch signal
    (my_func());
endproperty : detect_glitch
  event ev;
  always @( posedge clk) ->ev;
 
  function bit my_func();
    if (ev.triggered) return 1;
    else return 0;
  endfunction
 
DETECT_GLITCH : assert property (detect_glitch)
else
    $display ("ERROR"); 
 
  initial #100 $finish;
 
endmodule

The code is from a similar question from here.

4

Thank you Ben and Sharvil for the solutions.

5

In reply to ben@SystemVerilog.us:

Thanks Ben for the explanation. Just in case if we ignore delays can this be a possible solution?


``` verilog
 
input sig1;
input clk;

wire clk_d;  // delayed version of clk
assign clk_d = #0.1 clk;  // we can delay this signal by the smallest possible value

property align_clk_sig1_pos_chk ();
  @(posedege clk) (sig_1 === 0) ##1 (sig_1 === 1) |-> $past(sig_1==1,1,1,@(posedge clk_d));
endproperty 

assert property (align_clk_sig1_pos_chk)
  else $error(“signal didn’t rose @posedge of clk”);




Regards,
Aditya
6

In reply to gulkotwar.aditya:
Sorry, but the above assertion makes no sense, with or without the delayed clock.
Comments:

  1. @(posedege clk) (sig_1 === 0) ##1 (sig_1 === 1) is same as
    @(posedege clk) $rose(sig_1)
  2. Your assertion fails with the same clock throughout. All this assertion is stating is that when sig_1 rises (becomes 1), it was 1 in the previous cycle(without the clk_d); obviously, it can’t be 1 the previous cycle.
  3. With the dealy it may be a 1 in the previous cycle.
  4. Use timing checks if that is your concern
  5. Assertions are written in the style where
    antecedent |-> current_and_or_future_expectations.
    AVOID the following style:
    antecedent |-> past_occurences // POOR STYLE

Ben Cohen
http://www.systemverilog.us/ ben@systemverilog.us
For training, consulting, services: contact Home - My cvcblr

7

In reply to ben@SystemVerilog.us:

Thanks Ben for your feedback.

8 

`define PWR_ASSERT(input_pwr_domain,output_pwr_domain,str) \
   assign creat_event =input_pwr_domain;\
    pos_pwr_ctrl_assert_``str : assert property (@(posedge simlation_clk or input_pwr_domain) disable iff (!resetn) ((input_pwr_domain) |->  @pwr_event_p ((output_pwr_domain))))\
                      else\
                      begin\
                      $error("Assertion Failed at ``str Power UP Domain Control");\
                      $finish;\
                      end \

I am using this define for so many instances with different arguments.so the assertion is created for every str. This causes a warning of [SVA-OPTCOV-LMFA] Large memory footprint assertion. with this I am unable to open -vpd it taking too much of time. How can I get out of this.