 |
|
|
|
|
|
|
|
|
|
|
|
|
 SVUG Community Forum
|
|
| Author |
Messages |
|
Takaaki
Posts:5
 |
| 05/27/2009 11:07 PM |
|
| I am in trouble how to write cover property using "within".
Bus protocol is as follows. Two cases can be observed:
HCLK | | | | | | | |
HREADY |~~~|\__|___|___|___|___|/~~|
HRESP |___|___|___|___|___|/~~|~~~|
HCLK | | | | | | | |
HREADY |~~~|\__|___|___|___|___|/~~|
HRESP |___|___|___|___|___|___|___|
# Actually, above this is AHB Slave.
I want to detect and I do not want to detect .
The way I think is, checker begins at $fell(HREADY) and check ends at $rose(HREADY).
I tired following SVA but it does not find the case when "within..." is added to.
I would like to be adviced how following should be corrected.
-----------------------
property AhbSlaveError;
@(posedge HCLK) disable iff(! HRESETn)
($fell(HREADY)) |=>
(HREADY==1'b0 && HRESP==1'b1)[->1] ##1
(HREADY==1'b1 && HRESP==1'b1)
within (HREADY==1'b1 );
endproperty
-----------------------
My expectation is When appears, it matches, and when is observed, checker ends without success.
HCLK | | | | | | | |
HREADY |~~~|\__|___|___|___|___|/~~|
HRESP |___|___|___|___|___|/~~|~~~|
* <-- $fell(HREADY)
$rose(HREADY)--> *
Thank you |
|
|
|
|
Takaaki
Posts:5
|
| 05/27/2009 11:19 PM |
|
** Previous message does not contain white space and return code, somehow.
I am resending the same message. ***
I am in trouble how to write cover property using "within".
Bus protocol is as follows. Two cases can be observed:
HCLK | | | | | | | |
HREADY |~~~|\__|___|___|___|___|/~~|
HRESP |___|___|___|___|___|/~~|~~~|
HCLK | | | | | | | |
HREADY |~~~|\__|___|___|___|___|/~~|
HRESP |___|___|___|___|___|___|___|
# Actually, above this is AHB Slave.
I want to detect and I do not want to detect .
The way I think is, checker begins at $fell(HREADY) and check ends at $rose(HREADY).
I tired following SVA but it does not find the case when "within..." is added to.
I would like to be adviced how following should be corrected.
-----------------------
property AhbSlaveError;
@(posedge HCLK) disable iff(! HRESETn)
($fell(HREADY)) |=>
(HREADY==1'b0 && HRESP==1'b1)[->1] ##1
(HREADY==1'b1 && HRESP==1'b1)
within (HREADY==1'b1 );
endproperty
-----------------------
My expectation is When appears, it matches, and when is observed,
checker ends without success.
HCLK | | | | | | | |
HREADY |~~~|\__|___|___|___|____|/~~|
HRESP |____|___|___|___|___|/~~|~~~|
* <-- $fell(HREADY)
$rose(HREADY) --> *
Thank you |
|
|
|
|
Takaaki
Posts:5
|
| 05/27/2009 11:32 PM |
|
** Previous two messages do not contain white space and return code, somehow.
I am re-resending the same message. I am sorry to bother you ***
I am in trouble how to write cover property using "within".
Bus protocol is as follows. Two cases can be observed:
Case: ErrorResp
HCLK | | | | | | | |
HREADY |~~~|\__|___|___|___|___|/~~|
HRESP |___|___|___|___|___|/~~|~~~|
Case: NormalResp
HCLK | | | | | | | |
HREADY |~~~|\__|___|___|___|___|/~~|
HRESP |___|___|___|___|___|___|___|
# Actually, above this is AHB Slave protocol.
I want to detect ErrorResp and I do not want to detect NormalResp .
The way I think is, checker begins at $fell(HREADY) and check ends at $rose(HREADY).
I tired following SVA but it does not find the case when "within..." is added to.
I would like to be adviced how following should be corrected.
-----------------------
property AhbSlaveError;
@(posedge HCLK) disable iff(! HRESETn)
($fell(HREADY)) |=>
(HREADY==1'b0 && HRESP==1'b1)[->1] ##1
(HREADY==1'b1 && HRESP==1'b1)
within ($rose(HREADY));
endproperty
-----------------------
My expectation is When ErrorResp appears, it matches, and when NormalResp is observed,
checker ends without success.
HCLK | | | | | | | |
HREADY |~~~|\__|___|___|___|___|/~~|
HRESP |___|___|___|___|___|___|___|
* <-- $fell(HREADY)
$rose(HREADY) -----------------> *
Thank you |
|
|
|
|
|
| You are not authorized to post a reply. |
|
|
|
ActiveForums 3.7
|
|
|
|
|
|
|
|
|
|
|
|
|
 |
|