Accellera FV Committee. Sugar for examples 1-18 from the property list. Note: There is usually more than one way to express a property in Sugar. Which way is used is a matter of personal taste. In order to provide a better feel for the language, some of the examples below have been expressed in two or more Sugar "styles". 1. If a snoop hits a modified line in the l1 cache, then the next transaction must be a snoop writeback. (design 1) a. AG ((snoop & hitm) -> AX next_event(trans_start)(writeback)) b. AG {snoop & hitm} |=> {!trans_start[*],trans_start & writeback} c. {[*],snoop & hitm} |=> {!trans_start[*],trans_start & writeback} 2. If signal "enable" rises, then a clock after the fourth transfer signal "pending" must rise. (design 1) a. AG (rose(enable) -> AX next_event(transfer)[4](AX rose(pending))) b. AG {!enable,enable,{!transfer[*],transfer}[4]} |-> {!pending,pending} c. {[*],rose(enable),{!transfer[*],transfer}[4]} |=> {rose(pending)} 3. If signal "boff" is asserted, then if the first request which is accepted after the assertion of "boff" is not a snoop request, then it is a write request. (design 1) a. AG (boff -> AX next_event(accepted)(!snoop_req -> write_req)) b. AG {boff,!accepted[*],accepted} |-> {!snoop_req -> write_req} 4. If signal "hit" is active and signal "pending" is not, then next time signal "pending" is active, signal "sel5" is active. (design 1) a. AG ((hit & !pending) -> next_event(pending)(sel5)) b. AG {hit & !pending, !pending[*], pending} |-> {sel5} 5. An urgent request should be the next handled. (design 2) (If an urgent request is issued, then it should be the next handled, regardless of whether there are older requests pending.) a. AG (urgent_req -> AX next_event(grant)(urgent_answered)) b. {[*], urgent_req, !grant[*], grant} |-> {urgent_answered} 6. Between a request and its acknowledge the busy signal must remain asserted. (design 2) a. AG (req -> (busy until ack)) b. {[*], req} |-> {busy[*], ack} 7. If a data packet of any size starts and eventually gets a LAST bit, then next data packet must have the FIRST bit asserted. (design 3) a. AG {dp_start, !LAST[*], LAST}(next_event(dp_start)(FIRST)) b. {[*], dp_start, !LAST[*], LAST ~ {!dp_start[*], dp_start}} |-> {FIRST} 8. If a write command starts and size=N (N=1 through 8), then N assertions of signal "gx_start" should occur before the LAST bit goes active. (design 3) forall N: 1..8: AG within(write_command_start & size=N,LAST){gx_start[=N]} 9. The address queue ptr increment consecutively (cyclic). In other words, every time that an address is entered into the queue with queue ptr = N, the next time that an address is entered into the queue, the address will be N+1 (cyclically). (design 4) forall x(3..0): boolean: AG ((addr_queue_ptr_p_q(3..0)=x(3..0)) -> next_event((addr_queue_ptr_p_q(3..0)!=x(3..0))) ((addr_queue_ptr_p_q(3..0)=(x(3..0) + 1)))) 10. If data grant received then as soon as dbusy is high for two clocks, take the data bus. (design 5) a. AG (data_grant -> next_event(dbusy & prev(dbusy))(dvalid)) b. AG {data_grant, !dbusy[*], dbusy[2]} |-> {dvalid} 11. The data that returns for read is the last data that was written to the register before the read was issued. (design 5) forall dbits(0..7): boolean: forall addr(3..6): boolean: AG( {write_valid & reg_addr(11..14)=addr(3..6) & data_bus(0..7)=dbits(0..7), !(write_valid & reg_addr(11..14)=addr(3..6))[*], read_valid & reg_addr(11..14)=addr(3..6)} |-> {data_bus(0..7) = dbits(0..7)} ) 12. Every buffer will be read before it is overwritten. (design 6) forall addrbits(0..1): boolean: AG ((write_enable & write_address(0..1)=addrbits(0..1)) -> AX ((read_enable & read_address(0..1) =addrbits(0..1)) before (write_enable & write_address(0..1)=addrbits(0..1)))) 13. A write request of a certain transfer size will result in an equivalent number of data transfers. (design 6) forall N: 1..16: AG {write_request & size=N} |-> {data_en[=N] && done[=0], done} 14. For every write, data transfers must alternate between odd and even entries. In other words, if there is a write, then as long as we are transferring data belonging to this write, consecutive data transfers must alternate between even and odd addresses. (design 6) AG within(write_start, write_end) {{!write_en[*], write_en & !addr(0), !write_en[*], write_en & addr(0)}[*]} 15. Two consecutive writes cannot be to the same address. (design 6) a. forall addr(0..7): boolean: AG (write_valid -> AX ((addr_bus(0..7)=addr(0..7)) -> AX next_event(write_valid)(AX (addr_bus(0..7)!=addr(0..7))))) b. forall addr(0..7): boolean: {[*],write_valid,addr_bus(0..7)=addr(0..7),!write_valid[*],write_valid} |=> {addr_bus(0..7) != addr(0..7)} 16. If an address was set valid then the next time the "retire" signal is asserted for this address, the address will be invalidated 3-8 clocks later. (design 6) a. forall addr(0..4): boolean: AG ((write_en & data_valid & write_address(0..4)=addr(0..4)) -> next_event (retire & retire_address(0..4)=addr(0..4)) (ABF[3..8] (write_en & !data_valid & write_address(0..4)=addr(0..4)))) b. forall addr(0..4): boolean: AG {write_en & data_valid & write_address(0..4)=addr(0..4), !(retire & retire_address(0..4)=addr(0..4))[*], (retire & retire_address(0..4)=addr(0..4))} |-> {[3..8], write_en & !data_valid & write_address(0..4)=addr(0..4)} 17. If read req is received, then either the next output req to PLB is read, or the one after that. (design 7) a. AG (rose(read_req) -> next_event_f(rose(out_en))[1..2](output_read)) b. AG {!read_req, read_req} |-> {{!out_en[+], out_en}[1..2] ~ output_read} 18. If read req is received and then write req is received before read req is output, then read req will be output before write req is output. (design 7) (Assumption: reqs stay asserted until output.) AG {{rose(read_req),[*],rose(write_req)} && !(out_en & output_read)[*]} ((out_en & output_read) before (out_en & output_write))