Hi ,
Since throughout operator doesn’t allow LHS as temporal , I was trying the following using ‘intersect’ :

// ip_clk is much higher frequency than global_clk
property inter_sect ;
not( @( ip_clk ) 1 ) intersect @(posedge global_clk) ( $fell( en ) [->1] ); // <- Need help here . 'en' is sampled on global_clk
endproperty
property No_Toggle ;
@(posedge global_clk) en |=> inter_sect ;
endproperty

Currently I observe Compilation Error :
Error-[SVA-CMISO] Clocks mismatch in sequence operator . Clocks mismatch in ‘intersect’ sequence operator.

Requirement is that that when ‘en’ is high , ‘ip_clk’ shouldn’t toggle till ‘en’ is de-asserted .

In reply to MICRO_91:
**Requirement is that that when ‘en’ is high , ‘ip_clk’ shouldn’t toggle till ‘en’ is de-asserted .**y
Whenever I encounter a tricky requirement, particularly when clocks are involved, I start with a task model and then see if can convert it to an SVA assertion.

task automatic t();
// bit ip_clk_toggle; // Initial thoughts
// but that is not panning to anything useful
// fork
// @(negedge en) // ip_clk can toggle
// join_any
fork
@(ip_clk) // If ip_clk is toggling, then en must be==0
#1; // The #1 is needed if en changes in the NBA region of ip_clk
am_ip_clk: assert final (en==0);
join
endtask
always @(posedge global_clk) begin // ip_clk is much higher frequency than global_clk
fork t(); join_none
end

You can tune this model as needed.
I do not see an easy path to model these requirements into straight SVA.
The task model is structured around my paper Understanding the SVA Engine Using the Fork-Join Model

Using a model, the paper addresses important concepts about attempts and threads. Emphasizes the total independence of attempts.
Ben Cohen Ben@systemverilog.us
Link to the list of papers and books that I wrote, many are now donated.

In reply to ben@SystemVerilog.us:
After some thoughts, you can convert the task approach to SVA.

// Best Option: if en then no toggling
ap_ipclk_en1: assert property(
@(posedge global_clk) (en) |=> // clock switch
@(ip_clk) 1[*N] en==0); // If ip_clk is toggling, then en must be==0
// Another option
// when 'en' is high , 'ip_clk' shouldn't toggle till 'en' is de-asserted .
let N=2; // to allow for a few ip_clk edges to occur before checking for the en
ap_ipclk_en0: assert property(
@(posedge global_clk) 1 ##1 // clock switch
@(ip_clk) 1[*N] en==0); // If ip_clk is toggling, then en must be==0
// more simply
always(@(ip_clk) assert(en==0);
//

Whenever I encounter a tricky requirement, particularly when clocks are involved, I start with a task model and then see if can convert it to an SVA assertion.

I agree , having referred to your response , I have a task based solution ( using immediate assertion ) which uses SV constructs.

I was wondering if I could achieve the same using concurrent assertion.

Since I was trying a few codes , I have a question related to intersect operator : Can the RHS N LHS of intersect operator have different clocks ? i.e can we have a multi-clocked intersect operator ?

I am aware that multi-clocked or/and operator are legal ( assuming there is a single leading clock )

I made an update in my previous response (see above) .
On not( @( ip_clk ) 1 ) intersect …
Illegal since the not is property operator.
On RHS N LHS of intersect operator have different clocks, I don’t believe so.
Sometimes, the best way to get such answers is to try it out; in general, and hopefully,
the vendors know 1800 better than any of us.
:)
Ben

Sometimes, the best way to get such answers is to try it out; in general, and hopefully, the vendors know 1800 better than any of us.

I did try it out , I run into a compilation error : edalink

I was going through LRM Section 16.9.6 and 16.13.2 but I don’t see multi-clocked intersect operator as illegal . Since multi-clocked and/or operator are legal within a property , why isn’t multi-clocked intersect operator legal ?

1800: The two operands of intersect are sequences. The requirements for match of the intersect operation are as follows: — Both the operands shall match. — The lengths of the two matches of the operand sequences shall be the same.
[Ben] Because the lengths of the two matches of the operand sequences cannot be guaranteed to be the same.
Also, your example not( @( ip_clk ) 1 ) intersect @(posedge global_clk) ( $fell( en ) [->1] ); has a property_expr intersect sequence_expr, which is illegal.
Ben

Because the lengths of the two matches of the operand sequences cannot be guaranteed to be the same.

I see your point .
and / or operator do not have the requirement that the lengths of the LHS and RHS be the same , hence and / or operator can have non-identical clocks in LHS and RHS.

I tried using throughout operator :

property inter_sect ;
not( @( ip_clk ) 1 ) throughout @(posedge global_clk) ( $fell( en ) [->1] );
endproperty

As the LHS of throughout operator can’t be temporal , I observe compilation error

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

Have another question :

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 ?

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,
...

Would like to add a point related to throughout operator being illegal as a multi-clocked property.

Syntax for throughout operator as per Syntax 16-11 :

expression_or_dist throughout sequence_expr

i.e LHS of throughout operator can’t be a sequence or sub-sequence . Only a signal or expression is valid as LHS.

As a result ‘throughout’ operator as a multi-clocked property is illegal.

To summarize multi-clocked properties :

1) Using and/or operator is Legal :

property mclocks_and_or ;
@(posedge clk1) B and @(posedge clk2) C ; // Could be "or" operator as well
endproperty
ap0:assert property ( @(posedge clk0) A |=> mclocks_and_or ); // Leading edge present

2) Using intersect operator is Illegal as the requirement for intersect operator is that the length of the sequences must match
( which can’t be guaranteed due to non-identical clocks ):

property mclocks_intersect ;
@(posedge clk1) B intersect @(posedge clk2) C ; // Illegal due to unequal length
endproperty
ap0:assert property ( @(posedge clk0) A |=> mclocks_intersect );

3) Using throughout operator is Illegal as the LHS of throughout operator can’t be a sequence :

property mclocks_throughout ;
@(posedge clk1) B throughout @(posedge clk2) C ; // Illegal as LHS is sequence
endproperty
ap0:assert property ( @(posedge clk0) A |=> mclocks_throughout );

Thus only and/or/not operators are valid within a multi-clocked property.

EDIT : As Ben pointed implies operator is valid as well

In reply to MICRO_91:
The toughout operator specifies that a signal (expression) must hold throughout a sequence. *( b throughout R ) is equivalent to ( b [0:$] intersect R )
Multiclocking is illegal for your reason 2

Add the implies

assert property(@(posedge clk1) 1 |-> @(posedge clk1) a implies @(posedge clk2) b);
// assert property(@(posedge clk1) a implies @(posedge clk2) b); // illegal, No LCE
// LCE Leading Clocking Event

Hi Ben ,
I tried multi-clocked property for ‘within’ operator ( both LHS and RHS of ‘within’ can be a sequence expression ) :

property mclocks_within ;
@(posedge clk1) ( B ##1 C ) within @(posedge clk2) ( D ##1 E[->1] );
endproperty
assert property ( @(posedge clk0) A |=> mclocks_within ); // Leading clock ' clk0 '

I observe a compilation error with above code.

Please correct me if following reasoning is wrong :

Generally for : seq1 within seq2

Starting point of seq1 must be no earlier than starting point of seq2 , so with non-identical clocks since there is no guarantee that this occurs .
Hence ‘within’ operator is illegal for a multi-clocked property

In reply to MICRO_91:
COrrect
(seq1 within seq2) is equivalent to:
*((1[0:] ##1 seq1 ##1 1[*0:]) intersect seq2 )
start time must be the same. You Cannot guarantee that with multiclockings, therefore
multiclicking with the within is illegal;.
BEn