Multiple clocks in an assertion

SystemVerilog
,
4

In reply to rrkk66418:

sequence_expr |=> property_expr // is equivalent to:
sequence_expr ##1 `true |-> property_expr
// Thus
ap1: assert property(@(posedge clk1) $rose(a) |=> @(posedge clk2) b); // equivalent to 
ap1: assert property(@(posedge clk1) $rose(a) ##1 1'b1 |-> @(posedge clk2) b);  // same as 
ap1: assert property(@(posedge clk1) $rose(a) ##1 @(posedge clk1) 1'b1 // clock flow through 
  |-> @(posedge clk2) b);
/* 1800'2017 Differently clocked or multiclocked sequence operands cannot be combined with any sequence operators other than ##1 and ##0. For example, if clk1 and clk2 are not identical, then the following are illegal: */
@(posedge clk1) s1 ##2 @(posedge clk2) s2
@(posedge clk1) s1 intersect @(posedge clk2) s2
//[Ben] The following should be legal though 
@(posedge clk1) s1 ##1 '1b1 ##1 @(posedge clk2) s2
// equivalent to 
sequence s1b; 
  @(posedge clk1) s1 ##1 1'b1; 
endsequence 
@(posedge clk1) s1b  ##1 @(posedge clk2) s2

As to why? Amybe to keep it simple as there are other ways to clearly express the intent.

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: