Clarification needed for verification of MUL/DIV

[JobNoorman]

The documentation mentions that

Some arithmetic operations (such as multiplication and division) are beyond to practical capabilities of even modern hardware model checkers.

However, there are checks implemented for the MUL/DIV family of instruction (e.g., insn_mul.v), and their implementations seem sensible.

So I was wondering what "beyond the practical capabilities" exactly means. Do we just need to be more patient with the model checker (and maybe increase the depth for insn checks) or is it really useless?

[cliffordwolf]

Read the entire paragraph:

Some arithmetic operations (such as multiplication and division) are beyond to practical capabilities of even modern hardware model checkers. In order to still be able to verify things like bypassing for the arithmetic units performing those operations we define a set of alternative arithmetic operations. When the define RISCV_FORMAL_ALTOPS is set riscv-formal will expect the processor under test to implement those alternative operations instead.

The implication is that when RISCV_FORMAL_ALTOPS is not set, the model will implement the original (non-altops) behavior. This can be useful for example in simulation-based testing against the same spec. And that is exactly what you can find for example in insn_mul.v.

So I was wondering what "beyond the practical capabilities" exactly means.

There have been recent improvements in SAT-based model checking of multipliers, but unless you use an experimental model checking flow that can make use of those improvements, we are talking about at least decades of compute time for solving non-trivial circuit problems involving 64-bit multipliers. For the really interesting stuff the time until the heat-death of the universe may still be a more reasonable reference point than years or decades.

But even if you were using a solver with those improvements you'd still want to do system verification with ALTOPS. Because for the system-level bugs the exact operation doesn't matter and ALTOPS will always be faster. But you may want to use multiplier-based models for a separate unit-based verification of just the multiplier IP.

[JobNoorman]

Thanks for the clarification.

The reason I asked was because I was getting counterexample traces from the tool but didn't expect this (since I thought it would take too long). Now that the obvious bugs seem to be fixed, the tool indeed seems to run much longer (and I guess I shouldn't wait for it to finish).

[cliffordwolf]

Now that the obvious bugs seem to be fixed, the tool indeed seems to run much longer (and I guess I shouldn't wait for it to finish).

Yes. In the case were there is a bug the solver might still find a counter example quickly. But it would be very unsafe to assume that when the solver takes a long time, it means the only thing not left checked is the multiply itself.