In reply to MICRO_91:
So to summarize multi-clocked properties are only valid for and/or/not operators,
i.e the LHS and RHS can have non-identical clocks
and/or/not/implies, for sequential multiclocking the ##0, ##1
Note that there must be a single leading clocking event! THus
module m;
bit clk1, clk2, a, b;
assert property(@(posedge clk1) 1 |-> @(posedge clk1) a and @(posedge clk2) b);
assert property(@(posedge clk1) a and @(posedge clk2) b); // line 4
// Error: testbench.sv(4): (vlog-2048) Directive ‘assert__1’ has multiple leading clocks for its maximal property.
Also, your example not( @( ip_clk ) 1 ) intersect @(posedge global_clk) ( $fell( en ) [->1] ); has a property_expr intersect sequence_expr, which is illegal.
Why is $fell( en )[->1] considered a sequence_expression ?
As the intersect operator is written within a property , won’t it consider RHS as property automatically ?
the goto is defined as a sequence. a[->1] is equivalent to !a[*0:$] ##1 a
A property has many definitions, see the syntax.
sequence_expr |-> property_expr // a property definition
sequence_epr // another property definition,
...
Ben