Modify assertions in l15 adapter.

This commit is contained in:
Michael Schaffner 2018-11-22 21:28:03 +01:00
parent 2f38fcb853
commit 6b99b47270
No known key found for this signature in database
GPG key ID: 7AA09AE049819C2C

View file

@ -378,12 +378,12 @@ fifo_v2 #(
else $fatal(1,"[l15_adapter] got invalidation package with zero invalidation flags");
blockstore_o: assert property (
@(posedge clk_i) disable iff (~rst_ni) l15_req_o.l15_val|-> !l15_req_o.l15_blockstore)
else $fatal(1,"[l15_adapter] blockstores are not supported");
@(posedge clk_i) disable iff (~rst_ni) l15_req_o.l15_val |-> l15_req_o.l15_rqtype == L15_STORE_RQ |-> !(l15_req_o.l15_blockstore || l15_req_o.l15_blockinitstore))
else $fatal(1,"[l15_adapter] blockstores are not supported (out)");
blockstore_i: assert property (
@(posedge clk_i) disable iff (~rst_ni) l15_rtrn_i.l15_val|-> !l15_rtrn_i.l15_blockinitstore)
else $fatal(1,"[l15_adapter] blockstores are not supported");
@(posedge clk_i) disable iff (~rst_ni) l15_rtrn_i.l15_val |-> l15_rtrn_i.l15_returntype inside {L15_ST_ACK, L15_ST_ACK} |-> !l15_rtrn_i.l15_blockinitstore)
else $fatal(1,"[l15_adapter] blockstores are not supported (in)");
unsuported_rtrn_types: assert property (
@(posedge clk_i) disable iff (~rst_ni) (l15_rtrn_i.l15_val |-> l15_rtrn_i.l15_returntype inside {L15_LOAD_RET, L15_ST_ACK, L15_IFILL_RET, L15_EVICT_REQ, L15_CPX_RESTYPE_ATOMIC_RES}))