Regarding assertion implementation

SystemVerilog
1

I wanted to write an assertion that data_input which is one bit should match rx_data[0]th bit at posedge and rx_data[1]th at negedge , but when the rx_data changes the assertion fails ? I am not getting why it is checking the previous data and getting failed , at the rising edge or failing edge of rx_data as the data is correctly received?
Can you please let me know


sequence posedge_di;
@(posedge clk) ##0 (di == rx_data[0]);
endsequence
sequence negedge_di;
@(negedge clk) ##0 (di_a == rx_data[1]);
endsequence
property input;
@(posedge clk) disable_iff (!rst)
(data_valid) |=> negedge_di ##0 posedge_di ;
endproperty 
INPUT_CHECK : assert property (input)
2

In reply to bijal:
Your assertion expresses the following:

 
property input;
  @(posedge clk) disable_iff (!rst)
  (data_valid) |=> @(negedge clk) ##0 (di_a == rx_data[1])
                   ##0 @(posedge clk) ##0 (di == rx_data[0]) ;
endproperty
  1. @(posedge clk) if the the sampled(data_valid) then
    at the next (negedge clk) (the sampled(di_a) == the sampled(rx_data[1])
    // sampling is at eh negedge clk
    Then at the next (posedge clk) ##0 (the sampled(di) == the sampled(rx_data[0]))
  2. The issue you have is that you have a posedge clocking event
    followed by |=> @(negedge clk). This behaves in the same manner as
    @(posedge clk) (data_valid) |-> @(negedge clk) ##0 (di_a == rx_data[1])
    // In this case, because you have clocking eventat different times,
    // the |-> behaves the same as |=>
  3. The |=> or the |-> operators synchronize the last expression of the antecedent clocked with the antecedent clock and the first elements of the consequent property being evaluated clocked with the consequent clock. The synchronization is the same as the one used with ##1 (for the |=>) and ##0 (for the |->) operators.
  4. Multiclocked sequences are built by concatenating singly clocked subsequences using the single delay concatenation operator ##1 or the zero-delay concatenation operator ##0. The single delay indicated by ##1 is understood to be from the end point of the first sequence, which occurs at a tick of the first clock, to the nearest strictly subsequent tick of the second clock, where the second sequence begins. The zero delay indicated by ##0 is understood to be from the end point of the first sequence, which occurs at a tick of the first clock, to the nearest possibly overlapping tick of the second clock, where the second sequence b.

You want one of those two


property input_next_cycle;
  @(posedge clk) disable_iff (!rst)
  (data_valid) |=> (di == rx_data[0]) ##0 // @ posedge cycle after data_valid
                   @(negedge clk) (di_a == rx_data[1]); // 1/2 cycle later   
endproperty 

property input_same_cycle;
  @(posedge clk) disable_iff (!rst)
  (data_valid) |->  (di == rx_data[0]) ##0 // @ same posedge cycle as data_valid 
                    @(negedge clk) ##0 (di_a == rx_data[1]); // 1/2 cycle later 
endproperty

Ben Cohen
http://www.systemverilog.us/ ben@systemverilog.us
For training, consulting, services: contact http://cvcblr.com/home.html
** SVA Handbook 4th Edition, 2016 ISBN 978-1518681448
…

  1. SVA Package: Dynamic and range delays and repeats SVA: Package for dynamic and range delays and repeats - SystemVerilog - Verification Academy
  2. Free books: Component Design by Example https://rb.gy/9tcbhl
    Real Chip Design and Verification Using Verilog and VHDL($3) Amazon.com
  3. Papers:

Ben Cohen
http://www.systemverilog.us/ ben@systemverilog.us
For training, consulting, services: contact http://cvcblr.com/home.html
** SVA Handbook 4th Edition, 2016 ISBN 978-1518681448
…

  1. SVA Package: Dynamic and range delays and repeats SVA: Package for dynamic and range delays and repeats - SystemVerilog - Verification Academy
  2. Free books: Component Design by Example https://rb.gy/9tcbhl
    Real Chip Design and Verification Using Verilog and VHDL($3) Amazon.com
  3. Papers:
3

In reply to ben@SystemVerilog.us:
Consider this multiclocking assertion assertion
http://systemverilog.us/vf/mclk2.sv


module mclk2; 
    import uvm_pkg::*; `include "uvm_macros.svh"
	bit clk1=1, a=1, b=1; 
	initial forever #5 clk1=!clk1; 
	always @(posedge clk1)  
		#2 if (!randomize(a, b))  `uvm_error("MYERR", "This is a randomize error");  
		
	ap0: assert property(@(posedge clk1) $rose(a) |-> @(negedge clk1)  b);
	ap1: assert property(@(posedge clk1) $rose(a) |=> @(negedge clk1)  b);  
endmodule

959×919 118 KB

Ben Cohen
http://www.systemverilog.us/ ben@systemverilog.us
For training, consulting, services: contact http://cvcblr.com/home.html
** SVA Handbook 4th Edition, 2016 ISBN 978-1518681448
…

  1. SVA Package: Dynamic and range delays and repeats SVA: Package for dynamic and range delays and repeats - SystemVerilog - Verification Academy
  2. Free books: Component Design by Example https://rb.gy/9tcbhl
    Real Chip Design and Verification Using Verilog and VHDL($3) https://rb.gy/cwy7nb
  3. Papers: