Transitional assertion

SystemVerilog
1 
sequence sequ_A;
( (i_mtx_byte == 8'hab),$display ("i_mtx_byte is %0h \n",i_mtx_byte,$time)) ##1 ( (i_mtx_byte == 8'h0b),$display ("i_mtx_byte is %0h \n",i_mtx_byte,$time)) ;

endsequence 

property command_sequence_check ;
   @(posedge command)  disable iff(!rstn ) 
   sequ_A[*1:6] ##1  (i_mtx_byte == 8'hb9) ;

endproperty
k1_qspi_comand_sequence_check_p     :assert property (command_sequence_check) else $warning ("ASSERT", "Command sequence ab->0b->b9 not followed");

The command sequence should follow the sequence ab → ob → b9 , the command sequence is exactly comming but assertion is failling ,THe sequence ab → 0b can happen minimum 1 and maximum 5 times .
I have used no clock

2

In reply to bijal thakkar:

The way you wrote the property, your clocking event is @(posedge command).
Thus, when you say I have used no clock, you are incorrect, you are defining that clock to be the posedge command.
Assuming that your sequence is clocked with a clk, you most likely mean


property command_sequence_check ;
@(posedge clk) disable iff(!rstn )
$rose(command) |-> sequ_A[*1:6] ##1 (i_mtx_byte == 8'hb9) ;

I strongly suggest that you read my recent paper SVA Alternative for Complex Assertions
Verification Horizons - March 2018 Issue | Verification Academy
Ben Cohen
http://www.systemverilog.us/ ben@systemverilog.us
For training, consulting, services: contact Home - My cvcblr

** 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 | Verification Academy
  2. Free books: Component Design by Example FREE BOOK: Component Design by Example … A Step-by-Step Process Using VHDL with UART as Vehicle | Verification Academy
    Real Chip Design and Verification Using Verilog and VHDL($3) Amazon.com
  3. Papers:
3

Thanks Ben,
But still the sampling is not happening and assertion is failing still .
property command_sequence_check ;
@(posedge clk) disable iff(!rstn )
$rose(command) |-> sequ_A[*1:6] ##1 (i_mtx_byte == 8’hb9) ;

4

In reply to bijal thakkar:

A few comments:

  1. When you need to display the content of a sampled variable you need to use the $sampled(the-var)

sequence sequ_A;
( (i_mtx_byte == 8'hab),$display ("i_mtx_byte is %0h \n",$sampled(i_mtx_byte),$time))
##1 ( (i_mtx_byte == 8'h0b),$display ("i_mtx_byte is %0h \n",$sampled(i_mtx_byte),$time)) ;
endsequence
  1. If your design and testbench follow the proper design rules and your requirements are met by this assertion and your directed tests are correct then you should not have an assertion error. My guess as to why you experiencing an assertion failure is because you either have not followed the proper rules or your test pattern is incorrect.
  2. The rules I am talking about:
  • 4. for the clock, use something like initial forever #10 clk=!clk;
    5. for the design and testbench, use nonblocking assignments when updating variables

    verilog always @(posedge clk) begin var <= a && b; end

    6. consider using randomized variables after your directed tests. Something like:

    verilog initial begin repeat(200) begin @(posedge clk); if (!randomize(a, b) with { a dist {1'b1:=1, 1'b0:=1}; b dist {1'b1:=1, 1'b0:=2}; }) `uvm_error("MYERR", "This is a randomize error"); end $finish; end

    7. See my post on the various SV evaluation regions.
    Sampling point of Assertions | Verification Academy


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

** 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 | Verification Academy
  2. Free books: Component Design by Example FREE BOOK: Component Design by Example … A Step-by-Step Process Using VHDL with UART as Vehicle | Verification Academy
    Real Chip Design and Verification Using Verilog and VHDL($3) Amazon.com
  3. Papers:
5

Thanks Ben
It was helpful

6

In reply to bijal thakkar:
A correction to a statement I made:

  • A $display of a variable used in the sequence_match_item uses the sampled variable and thus does not need the $sampled of that variable.
    For example (a, $display(“a=%b”, a) ##1 b |-> c)
  • A $display of a variable used in the action block needs to be address with the $sampled because the action block occurs in the Reactive Region
    Sampling point of Assertions - SystemVerilog - Verification Academy

module m; 
  bit clk;
  initial forever #10 clk=!clk;  
  ap: assert property(
    @(posedge clk) (1, $display("in prop clk=%b, sample_clk=%b", clk, $sampled(clk))))
    $display("in action_block clk=%b, AB_sample_clk=%b", clk, $sampled(clk)); 
                    
   initial  
     repeat(10) begin 
             @(posedge clk);    
     end
 endmodule 
// simulation 
# in prop clk=0, sample_clk=0
# in action_block clk=1, AB_sample_clk=0

Ben SystemVerilog.us