I’m trying to combine and simplify my burst assertions. Any suggestions?
HBURST4_VALID: assume property (@ (posedge HCLK) disable iff (!HRESETn) HTRANS == 2 && HREADY && HBURST[2:1] == 1 |=> ((HTRANS[0] throughout (HREADY && HTRANS[1])[->3]) |=> !HTRANS[0]) and ((HREADY && HTRANS == 3)[=0:2] intersect !HTRANS[0][->1] |-> HRESP && HREADY && !HTRANS)) else $display(“HBURST4 violation”);
HBURST8_VALID: assume property (@ (posedge HCLK) disable iff (!HRESETn) HTRANS == 2 && HREADY && HBURST[2:1] == 2 |=> ((HTRANS[0] throughout (HREADY && HTRANS[1])[->7]) |=> !HTRANS[0]) and ((HREADY && HTRANS == 3)[=0:6] intersect !HTRANS[0][->1] |-> HRESP && HREADY && !HTRANS)) else $display(“HBURST8 violation”);
HBURST16_VALID: assume property (@ (posedge HCLK) disable iff (!HRESETn) HTRANS == 2 && HREADY && HBURST[2:1] == 3 |=> ((HTRANS[0] throughout (HREADY && HTRANS[1])[->15]) |=> !HTRANS[0]) and ((HREADY && HTRANS == 3)[=0:14] intersect !HTRANS[0][->1] |-> HRESP && HREADY && !HTRANS)) else $display(“HBURST16 violation”);
I would like to improve performance, and I find it impossible to simplify what I’ve already done. Am I missing something?
Thanks,
Noah
In reply to nachumk:
Taking a very quick look at your code, I can say that you have way way too many implication operators. You need to break down the requirements, and use a single implication operator.
Use }->, or |-> ##1. Avoid altogether using
sequence |-> other_sequence |-> other2_sequence.
Thus, break your verification into smaller sections based on the requirements.
Your code
HBURST4_VALID: assume property (@ (posedge HCLK) disable iff (!HRESETn)
HTRANS == 2 && HREADY && HBURST[2:1] == 1 |=>
((HTRANS[0] throughout (HREADY && HTRANS[1])[->3]) |=>
!HTRANS[0]) and ((HREADY && HTRANS == 3)[=0:2] intersect !HTRANS[0][->1] |->
HRESP && HREADY && !HTRANS)) else $display("HBURST4 violation");
HBURST8_VALID: assume property (@ (posedge HCLK) disable iff (!HRESETn)
HTRANS == 2 && HREADY && HBURST[2:1] == 2 |=>
((HTRANS[0] throughout (HREADY && HTRANS[1])[->7]) |=>
!HTRANS[0]) and ((HREADY && HTRANS == 3)[=0:6] intersect !HTRANS[0][->1] |->
HRESP && HREADY && !HTRANS)) else $display("HBURST8 violation");
HBURST16_VALID: assume property (@ (posedge HCLK) disable iff (!HRESETn)
HTRANS == 2 && HREADY && HBURST[2:1] == 3 |=>
((HTRANS[0] throughout (HREADY && HTRANS[1])[->15]) |=>
!HTRANS[0]) and ((HREADY && HTRANS == 3)[=0:14] intersect !HTRANS[0][->1] |->
HRESP && HREADY && !HTRANS)) else $display("HBURST16 violation");
Ben Cohen
http://www.systemverilog.us/ ben@systemverilog.us
For training, consulting, services: contact http://cvcblr.com/home.html
** SVA Handbook 4th Edition, 2016 ISBN 978-1518681448
…
- SVA Package: Dynamic and range delays and repeats SVA: Package for dynamic and range delays and repeats | Verification Academy
- Free books: Component Design by Example FREE BOOK: Component Design by Example … A Step-by-Step Process Using VHDL with UART as Vehicle | Verification Academy
Real Chip Design and Verification Using Verilog and VHDL($3) Amazon.com
- Papers:
In reply to ben@SystemVerilog.us:
Hi Ben,
Can you give an example for one of these? I’ve been working to break them apart, but it’s not easy to get all cases covered. I’m thinking there’s some better way but I’ve yet to come up with it.
Thanks,
Noah
In reply to nachumk:
When I wrote my PSL book I addressed the assertions and verification.
This link is the content of that chapter. You can easily convert the PSL to SVA.
http://systemverilog.us/vf/PSL_AHB_Ch8.zip
In that zip file is jpslbk_08_ahb.pdf that represents the whole chapter.
Also, ahbCompliance.v includes some PSL assertions. Below are those assertions in PSL.
/**************************** PSL ASSERTIONS **************************/
/* define default clock that will be used to sample all subsequent asserts */
/* NOTE: it is important that data does not change on the same edge as clock
because, like HDL, assertions can be sensitive to races */
// sugar default clock = (posedge hclk);
/* Behavior: If reset is active then Transfer Type is IDLE and Resp is OKAY
(default clock) */
// sugar property IdleAndOkayDuringReset = always(
// {(hresetn == 0);(hresetn == 1)} |->
// {(htrans == IDLE) && (hresp == OKAY)});
/* Behavior: If the transfer type is NONSEQ and Burst Mode is SINGLE,
then on the next clock cycle, the transfer type is not SEQ and not BUSY
(default clock) */
// sugar property BusyAndSeqNeverFollowNonseqOnSingleTransfer = always (
// (htrans == NONSEQ) && (hburst == SINGLE ) ->
// next ((htrans != SEQ) && (htrans != BUSY)) );
/* Behavior: If the transfer type is BUSY and slave is ready,
then on the next clock cycle, the transfer type must not be IDLE and
must not be NONSEQ unless grant is 0 and ready is 1 (default clock) */
// sugar property NeverGoFromBusyToIdleOrNonseqUnlessNoGrant = always (
// ((htrans == BUSY) && (hready == 1)) ->
// next ((htrans != IDLE) && (htrans != NONSEQ))
// abort ((hready == 1)) || (hresetn == 0));
//// abort ((hgnt == 0) && (hready == 1)) || (hresetn == 0));
/* Behavior: if the transfer type is IDLE, then on the next clock
cycle, the transfer type must be either IDLE or NONSEQ (default clock)*/
// sugar property AlwaysGoToNonseqFromIdle = always (
// (htrans == IDLE) ->
// next ((htrans == IDLE) || (htrans == NONSEQ)) );
/* Behavior: if the transfer type is BUSY then on the corresponding
data transfer , the slave must provide a zero wait state OKAY response
(default clock) */
// sugar property ResponseToBusyMustBeZeroWaitOKAY = always (
// ((htrans == BUSY) && (hready == 1)) ->
// next ((hresp == OKAY) && (hready == 1)) );
/* Behavior: if the transfer type is IDLE then on the corresponding data
transfer, the slave must provide a zero wait state OKAY response
(default clock) */
// sugar property ResponseToIdleMustBeZeroWaitOKAY = always (
// ((htrans == IDLE) && (hready == 1)) ->
// next ((hresp == OKAY) && (hready == 1)) );
/* Behavior: if the previous response was OKAY, and the current response
is not OKAY, then Ready must be 0 during the second not OKAY response
(default clock) */
// sugar property ReadyMustBeZeroDuringFirstNotOkayResponse = always (
// {(hresp == OKAY);(hresp != OKAY)} |->
// {hready == 0}) ;
/* Behavior: if the response is SPLIT or RETRY, the master must drive IDLE
(default clock) */
// sugar property FirstNotOkayResponseCausesNextIdle = always (
// ((hresp == SPLIT) || (hresp == RETRY)) && (hready == 0) ->
// next (htrans == IDLE));
/* Behavior: if the transfer type is SEQ or BUSY, then the controls of the
corresponding data transfer must be the same as their previous control
(default clock) NOTE: the equivalence operator is used with hprot
because this is an optional signal and may be an "X" value if not
connected */
// sugar property ControlMustBeConstantDuringABurst = always (
// (htrans == SEQ) || (htrans == BUSY) ->
// ((hsize == prev_hsize) && (hprot === prev_hprot) &&
// (hwrite == prev_hwrite)) );
/* Behavior: if Ready is 0 and the response is OK or ERROR, the address
and control, and data from the master are held constant (default clock)
NOTE: the equivalence operator is used with hprot because this is an
optional signal and may be an "X" value if not connected */
// sugar property ControlMustBeConstantWhenSlaveNotReady = always (
// (hready == 0) && ((hresp == OKAY) || (hresp == ERROR)) -> next
// (htrans == prev_htrans) && (hsize == prev_hsize) &&
// (hprot === prev_hprot) && (hwrite == prev_hwrite) &&
// (haddr == prev_haddr) && (hburst == prev_hburst)
// abort (hresetn == 0));
/* Behavior: if ready is 0 and the previous transfer type was SEQ or NONSEQ,
then on the next cycle the write data is the same as the previous write data
(default clock) (This assertion is designed to fail!!!) */
// sugar property WriteDataMustBeConstantWhenSlaveNotReadyAndDataBeingTransferred = always (
// (hready == 0) && (hwrite == 1) &&
// ((prev_htrans == SEQ) || (prev_htrans == NONSEQ)) -> next
// (hwdata == prev_hwdata)
// abort (hresetn == 0));
/* Behavior: if transfer type is BUSY then address does not change
(default clock) */
// sugar property AddrHeldWhenMasterBusy = always (
// (htrans == BUSY) -> next (haddr == prev_haddr) );
/* Behavior: if transfer is in progress, then 1K boundary is not exceeded
(default clock) */
// sugar property PageAddressNeverExceeds1kBoundary = always (
// ((htrans == SEQ) || (htrans == BUSY)) ->
// (haddr[31:10] == prev_haddr[31:10]) );
/* Behavior: If the burst type is not INCR and the transfer type is not
IDLE , then the NumberBeats for the Burst Mode is not exceeded
(default clock) */
// sugar property BurstIsNotTooLong = always (
// (hburst != INCR) && (htrans != IDLE) ->
// ((hburst == SINGLE) && (NumberBeats <= 1)) ||
// ((hburst == WRAP4) && (NumberBeats <= 4)) ||
// ((hburst == WRAP8) && (NumberBeats <= 8)) ||
// ((hburst == WRAP16) && (NumberBeats <= 16)) ||
// ((hburst == INCR4) && (NumberBeats <= 4)) ||
// ((hburst == INCR8) && (NumberBeats <= 8)) ||
// ((hburst == INCR16) && (NumberBeats <= 16)) );
/* Behavior: For all but INCR Burst mode, if the end of the packet is being
transferred as indicated by a transition from SEQ to IDLE when Resp is ok
then the NumberBeats for the Burst Mode is the max number unless grant is 0
(default clock) */
// 7/16/03 Modified to correct error in number because of last increment
// sugar property BurstIsNotTooShort = always (
// {((hburst != INCR) && (hresp == OKAY) && (htrans == SEQ));
// (htrans == IDLE) } |->
// {((prev_hburst == SINGLE) && (NumberBeats == 1)) ||
// ((prev_hburst == WRAP4) && (NumberBeats == (4+1))) ||
// ((prev_hburst == WRAP8) && (NumberBeats == 8)) ||
// ((prev_hburst == WRAP16) && (NumberBeats == 16)) ||
// ((prev_hburst == INCR4) && (NumberBeats == 4)) ||
// ((prev_hburst == INCR8) && (NumberBeats == 8)) ||
// ((prev_hburst == INCR16) && (NumberBeats == 16))});
//// abort (hgnt == 0)) ;
/* Behavior: if the transfer type is IDLE , then on the next clock cycle,
the transfer type is not SEQ and the transfer type is not BUSY
(default clock) */
// sugar property NeverGoFromIdleToSeqOrBusy = always (
// (htrans == IDLE) ->
// next ((htrans != SEQ) && (htrans != BUSY)) );
/* Behavior: RETRY is always asserted for two cycles unless reset is asserted
(default clock)*/
// sugar property RetryResponseMustPersistTwoCycles = always (
// {(hresp != RETRY);(hresp == RETRY)} |=>
// {(hresp == RETRY)}
// abort (hresetn == 0));
/* Behavior: SPLIT is always asserted for two cycles unless reset is asserted
(default clock) */
// sugar property SplitResponseMustPersistTwoCycles = always (
// {(hresp != SPLIT);(hresp == SPLIT)} |=>
// {(hresp == SPLIT)}
// abort (hresetn == 0));
/* Behavior: ERROR is always asserted for two cycles unless reset is asserted
(default clock) */
// sugar property ErrorResponseMustPersistTwoCycles = always (
// {(hresp != ERROR);(hresp == ERROR)} |=>
// {(hresp == ERROR)}
// abort (hresetn == 0));
/******* incorrectAddressCalculation for 3 example WRAP modes: This calculates
whether the next address is correct for all wrap modes*******/
/* Behavior: if Burst mode is WRAP4 and Size is 8 bits, then if
transfer mode is SEQ or BUSY, then if previous transfer mode is not
busy and previous Ready is not zero, then check that the address is as predicted */
// sugar property CorrectAddressDuringPageSize4BurstWrap = always (
// ((hburst== WRAP4) && (hsize == bits8)) ->
// ((htrans == SEQ || htrans == BUSY)) ->
// ((prev_htrans != BUSY) && (prev_hready != 0)) ->
// ((haddr[31:2] == prev_haddr[31:2]) &&
// (haddr[1:0] == prev_haddrPlusSize[1:0])) );
//
// sugar property CorrectAddressDuringPageSize8BurstWrap = always (
// ((hburst== WRAP4) && (hsize == bits16)) ||
// ((hburst== WRAP8) && (hsize == bits8)) ->
// ((htrans == SEQ) || (htrans == BUSY)) ->
// ((prev_htrans != BUSY) && (prev_hready != 0)) ->
// ((haddr[31:3] == prev_haddr[31:3]) &&
// (haddr[2:0] == prev_haddrPlusSize[2:0])) );
//
// sugar property CorrectAddressDuringPageSize2048BurstWrap = always (
// ((hburst== WRAP16) && (hsize == bits1024)) ->
// ((htrans == SEQ) || (htrans == BUSY)) ->
// ((prev_htrans != BUSY) && (prev_hready != 0)) ->
// ((haddr[31:11] == prev_haddr[31:11]) &&
// (haddr[10:0] == prev_haddrPlusSize[10:0])) );
/* Behavior: the address must increment by size during all INCR beats */
// sugar property AddressIncBySizeDuringAllBurstIncrBeats = always (
// ((hburst == INCR16) || (hburst == INCR8) ||
// (hburst == INCR4)) ->
// ((htrans == SEQ) || (htrans == BUSY)) ->
// ((prev_htrans != BUSY) && (hready != 0)) ->
// (haddr == prev_haddrPlusSize) );
/* Behavior: always address must be aligned to the transfer size */
// sugar property AddressNotAlignedToTransferSize = always (
// ((hsize == bits8) ||
// ((hsize == bits16) && (haddr[0] == 1'b0)) ||
// ((hsize == bits32) && (haddr[1:0] == 2'b00)) ||
// ((hsize == bits64) && (haddr[2:0] == 3'b000)) ||
// ((hsize == bits128) && (haddr[3:0] == 4'b0000)) ||
// ((hsize == bits256) && (haddr[4:0] == 5'b00000)) ||
// ((hsize == bits512) && (haddr[5:0] == 6'b000000)) ||
// ((hsize == bits1024) && (haddr[6:0] == 7'b0000000)) ) );
/* Behavior: always the maximum number of wait states is 16 */
// sugar property NeverMoreThan16WaitStates = always (
// {(hready == 1);(hready == 0)} |=>
// {{(hready == 0)[*0..15]};{hready == 1}}
// abort (hresp != OKAY));
endmodule
It has been a long time since I looked at AHB, but I hope that this info would help in what you need. BTW, I do not recommend PSL as I prefer SVA. In fact, I took my PSL book off the market.
Ben Cohen
http://www.systemverilog.us/ ben@systemverilog.us
For training, consulting, services: contact http://cvcblr.com/home.html
** SVA Handbook 4th Edition, 2016 ISBN 978-1518681448
…
- SVA Package: Dynamic and range delays and repeats SVA: Package for dynamic and range delays and repeats | Verification Academy
- Free books: Component Design by Example FREE BOOK: Component Design by Example … A Step-by-Step Process Using VHDL with UART as Vehicle | Verification Academy
Real Chip Design and Verification Using Verilog and VHDL($3) Amazon.com
- Papers: