XIF Invalid Compressed Instrs - Assert Slightly Wrong

[silabs-robin]

Regarding this property: https://github.com/openhwgroup/core-v-verif/blob/master/lib/uvm_agents/uvma_cvxif/src/uvma_cvxif_assert.sv#L30
cvxif_assert.compressed_valid |-> cvxif_assert.compressed_req.instr[1:0] != 2'b11;

The assert seems to be based on an ambiguous part of the spec, and chosing the meaning not intended by spec.
See openhwgroup/core-v-xif#231

[silabs-robin]

@ZElkacimi @AyoubJalali

[silabs-robin]

It seems you have asserts for both interpretations of the spec item.

(cvxif_assert.compressed_valid && cvxif_assert.compressed_ready && cvxif_assert.compressed_req.instr[1:0] == 2'b11) |-> !cvxif_assert.compressed_resp.accept;

This is (apparently) how that spec item was intended.

Also... Wouldn't that assert just be vacuous then?
The antecedent could never get a match if the previous assert is true.

[silabs-robin]

(CVXIF_UNCOMPRESSED_RESP is also not based on spec, afaict. The spec even explicitly says "All opcodes which are not used (i.e. considered to be invalid) by the CPU can be used for extensions.".)

[silabs-robin]

(The covers of these properties are also, strictly speaking, not doing anything, under "default" SV behavior, afaik.)
(There are multiple other issues too.)