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