Formally Verifying the MUL and DIV Instructions of the Ibex RISC-V CPU Using Aristotle

It takes one sentence to formally verify that all the multiplication and division instructions of the Ibex RISC-V CPU compute the right result. With Aristotle connected to your coding agent over MCP, this is the whole prompt:

Use Aristotle to formally verify the multiplication and division instructions for the Ibex RISC-V core configured with a single-cycle multiplier by comparing the RTL implementation against the SAIL RISC-V SVA formal specification.

Your agent sets up a check of each instruction against the formal specification of the RISC-V ISA written in Sail, and Aristotle reports whether it proved each property.

Run it yourself

Install Aristotle and register its MCP server with your agent, such as Claude Code or Codex. You can sign up at aristotle.harmonic.fun. Then clone the Ibex core from lowRISC, open your agent in the ibex directory, and give it the prompt.

The agent downloads what else it needs, such as the Sail RISC-V model, and writes a harness for the proof. The Sail model is the formal model of the RISC-V ISA from RISC-V International, built with the Sail tools from the Universities of Cambridge and Edinburgh.

Once the setup is ready, the agent submits it to Aristotle. The project then shows in your history at aristotle.harmonic.fun, where you can follow the run.

Aristotle compiles the source SystemVerilog code and any SystemVerilog Assertions into Lean 4 code against a carefully handcrafted formal model of digital circuits. Our approach does not rely on a non-deterministic and unsound transliteration of SystemVerilog into Lean with an LLM.

What Aristotle proved

Aristotle proved 9 properties about MUL, MULH, MULHSU, MULHU, DIV, DIVU, REM and REMU. When the run finishes, the project page shows the result of each property, along with Aristotle's summary of what it checked. You can see the full verification report in Aristotle (you'll need to sign in first).

Eight of the properties are assertions, from assert_mul to assert_remu. Each one says that whenever Ibex's ibex_multdiv_fast module, configured with RV32M = RV32MSingleCycle, reports a valid result for its instruction, the result equals what the Sail model writes to rd for the same operands. The prompt asked Aristotle to cover division by zero, signed overflow (0x80000000 / -1) and both values of data_ind_timing. The ninth property says that every instruction completes, so the eight assertions can't pass vacuously. There are no environment assumptions.

This is the SVA assertion for MUL, which connects the RTL result to the result of the Sail model:

always_comb begin
  assert_mul: assert
    (!(reset_seen_q && rst_ni && valid) ||
      (multdiv_result == spec_result));
end

The Lean definition at the top of this post is the Lean representation of this assertion.

Beyond the existing Ibex proof

In the Ibex repo there are formal verification scripts for formally verifying many Sail ISA properties but the formal check for the functional correctness of the MUL instruction is omitted because that can't be done with model checking based tools. However, as you see, Aristotle has no problems proving correct the MUL and related instructions.

We also ran the check on the fast multi-cycle multiplier, RV32MFast, and Aristotle proved MUL there too.

Try it on your own design

Try this verification yourself, or run Aristotle on your own SystemVerilog. You can give it SVA properties, describe the properties you want in English and have Aristotle formalize them, or ask Aristotle to come up with the relevant properties and prove them. Get started at aristotle.harmonic.fun.