Cover the scenario

SystemVerilog
1

Hi All,
I have signal a,b,c. After a fell to zero, b &c will be true for two times at some cycles.
here is cover property ,

cover ($fell(a)[->1] ##1 (b&c)[->2])

is it correct?
thank you

2 
cover property (@(posedge clk) $fell(a)##1 (b&&c)[->2]); // updated
// you need the cover property  because it is concurrent. 
// Use the logical && Operator instead of the bitwise & Operator 
//  It is best practice because it is more readable
3

Hi Ben,
Thanks for reply. How to detect if b&&c happen over two times, and report fail?
Thanks

4
  1. I am updating my previous reply to
cover property ($fell(a) ##1 (b&&c)[->2]);
// you don't need that first goto, my error.
// 2) if you want to fire the cover once
initial cover property ($fell(a)[->1] ##1 (b&&c)[->2]) ;
// 3) on detecting no 3rd b&c
initial assert property ($fell(a)[->1] ##1 (b&&c)[->2] |-> always(not (b&&c)) );
5

Thanks for reply. I am sorry that I miss some information
signal A is a level signal and it will fell for few times, and b&&c can not happen over 2 times before next $rose(a). Also, b&c can not assert if no $fell(a) happen before.

 assert property ($fell(a)[->1] ##1 (b&&c)[->2] |-> not ( (b&&c) throughout $rose(A) ) );
 assert property (b&&c |-> $past($fell(a)...... // not know how to detect b&c can not assert if no $fell(a) happen before

For b&&c can not happen over 2 times before next $rose(a), the property is correct?
I do not know how to detect b&c can not assert if $fell(a) never happen before
Thank you

6 
/* signal A is a level signal and it will fell for few times, and b&&c can not happen
 over 2 times before next $rise(a). Also, b&c can not assert if no $fell(a) happen before.

 assert property ($fell(a)[->1] ##1 (b&&c)[->2] |-> not ( (b&&c) throughout $rise(A) ) );
 assert property (b&&c |-> $past($fell(a)...... // not know how to detect b&c can not assert if no $fell(a) happen before
For b&&c can not happen over 2 times before next $rise(a), the property is correct?
I do not know how to detect b&c can not assert if $fell(a) never happen before */
module m;
bit clk, a, b, c;
// b&c can not assert if ! $fell(a) 
bit a_fell=0;
always_ff @(posedge clk) begin 
 if($fell(a)) a_fell <=1;
// Note, depending upon your requitrements, you can asjest this support variable 
 if($rose(a)) a_fell <=0; // Check if this is what is needed 
end 
assert property(@(posedge clk)  b&&c |-> !a_fell);


// signal A is a level signal and it will fell for few times, and b&&c can not happen
//   over 2 times before next $rise(a)
assert property (@(posedge clk) $fell(a)[->1] ##1 (b&&c)[->2] |->
     ($rose(a)) or ##1  ( !(b&&c) throughout $rose(a)[->1] ) );
// 1) The "not" is a property operator; it cannot be combined with a sequential "throughout operator"
// You cannot use the |-> with an immediate test of !(b&&c).
// To solve this, I delayed the throughout by 1 cycle, and in the immedate cycle 
// tested for a rose(a) 

// Instead of throughout you can use its expanded version 
     assert property (@(posedge clk) $fell(a)[->1] ##1 (b&&c)[->2] |->
      ($rose(a)) or ##1  ( !(b&&c)[*1:$] intersect $rose(a)[->1] ) );

endmodule
7

thanks for reply
As for using throughout and intersect, which one is better practice?

8

Q: As for using throughout and intersect, which one is better practice?
A: First the syntax and its meaning per 1800

expression_or_dist throughout sequence_expr
The construct exp throughout seq is an abbreviation for the following:
(exp) [*0:$] intersect seq
[Ben] The intersect is only an abbreviation, in processing (simulation or FV) it is actually expanded to the intersect version; thus, there is no performance impact. 
I prefer the use of the intersect insead of its abbreviation because: 
1) If I use the throughout, I then have to go thru a mental jiggle to reconstruct its meaning.  In fact, you made that very point in your coding of:
     (b&&c) throughout $rose(A) ) )  
where you missunderstood its definition and missed the definition of the sequence $rose(A)[->1]. 
2) I come from a hardware design background and for me, the intersect is more visual. 
Here I see a possible set of threads (the exp[*0:$]) instersecting (or crossing) a fixed sequence (the $rose(A)[->1]).

One more comment: In your initital posting you missed to specify many requirements.
An advice: I strongly believe in the use of AI, like perplexity, to check and expressing requirements, creating SV/SVA RTL and TB code. Yes, AI is not quite there yet, but the structures and information it brings help better express what is needed in the design and verification.
I used perplexity in writing my paper (link below) to address the requirements and even fixing my English composition.
The Traditional Req/Ack Handshake, It’s More Complicated Than You Think!