Dedicated retire channels in dual issue

[coderkalyan]

Hi,

I am using riscv-formal to verify a dual issue in order core I'm working on (I've successfully verified single issue cores in the past, thank you for such a great project!). However, my core is not capable of dual issuing all combinations of instructions - for example, there is only one arithmetic and one logical functional unit. Dual issue only occurs when one arithmetic and one logical (i.e. addi and xori) are fetched in the same cycle.

I wired up my RVFI ports with NRET=2 such that the arithmetic unit will always retire to the first channel if possible, and the the logic unit will retire to either channel 1 or 2 based on usage. However, I'm getting a PREUNSAT error when verifying that I realized is happening because the formal interface assumes it can always retire an add instruction on either channel 1 or 2, which is not possible in my design (since only one add can retire per cycle, and it chooses channel 1 if at all possible with priority).

Am I configuring or or wiring up the formal interface incorrectly? I can disable checking certain instructions for channel 1 by manually specifying the checks to run but this seems tedious and error prone. I can also adapt my interface to randomly shuffle instructions between retiring on channels 1 and 2 but this also doesn't seem like the right way. What is the recommended way to address this?

[KrystalDelusion]

I think the intended way to handle this is by specifying the instruction checks in your .cfg file. Like mentioned in https://yosyshq.readthedocs.io/projects/riscv-formal/en/latest/procedure.html#filter-checks

Something like

[filter-checks]
- insn_addi_ch2

or

[filter-checks]
+ insn_xori_ch2
- insn_*_ch2

Depending on whether its easier to specify all disabled or all enabled. Also it's matching regex, so you can do things like - insn_(add|sub)[i]_ch2.