silabs-robin

Idea: Before I forget, adding support for `tests/cfg/*.yaml` might be easy? The formal makefile already sources some `mk/*` file(s)(?), so whatever is in there should be visible from the formal...

> the problem was that the ISACOV doesn't support pseudo-code I'm not convinced there is any issue with that. (You can ask Mike if you'd like more details on the...

> > It seems ISACOV lacks support for whatever those instructions are. > > these are csrr xx mcause (it's a csr instruction) That csrr pseudo instr is ran as...

> I think the dasm-spike decode `csrr rd, csr` [...] Here is what I don't understand: "csrr rd, csr" is a string. But AFAIK the decoder takes a raw binary...

> I think we should remove [rs2_toggle](https://github.com/openhwgroup/core-v-verif/blob/8fb291707e97a82582435bf845d8c5f0dc7c3e17/lib/uvm_agents/uvma_isacov/cov/uvma_isacov_cov_model.sv#L1198) from cg_cl because c.lw does not have rs2 I agree. There is no `rs2` in `CL` at all. And I can only find...

> isn't we should create cover group for instr_prev.name instead of instr.name ?? like this That seems to be it, yeah :)

Nice. Looking forward to re-measuring our coverage with all of the improvements you have made. I will close this issue after a related PR gets merged.

> > I will close this issue after a related PR gets merged. > > @silabs-robin can you provide the actual PR number here? Thanks. There is no PR number...

Just a note here: In the 40s dir (and rvfi agent) we have a lot of "support logic" which we use in formal. Several of the assertion modules also do...

> the existing "support logic" would not be impacted. What I was thinking is that I would like if the decoder could be used similar to how the support logic...