soc.fu.mul.formal package¶
Submodules¶
soc.fu.mul.formal.proof_main_stage module¶
Formal Correctness Proof for POWER9 multiplier
notes for ov/32. similar logic applies for 64-bit quantities (m63)
m31 = exp_prod[31:64] comb += expected_ov.eq(m31.bool() & ~m31.all())
If the instruction enables the OV and OV32 flags to be set, then we must set them both to 1 if and only if the resulting product cannot be contained within a 32-bit quantity.
This is detected by checking to see if the resulting upper bits are either all 1s or all 0s. If even one bit in this set differs from its peers, then we know the signed value cannot be contained in the destination’s field width.
m31.bool() is true if any high bit is set. m31.all() is true if all high bits are set.
- m31.bool() m31.all() Meaning
- 0 x All upper bits are 0, so product
- is positive. Thus, it fits.
- 1 0 At least one high bit is clear.
- Implying, not all high bits are clones of the output sign bit. Thus, product extends beyond destination register size.
- 1 1 All high bits are set and they
- match the sign bit. The number is properly negative, and fits in the destination register width.
Note that OV/OV32 are set to the inverse of m31.all(), hence the expression m31.bool() & ~m31.all().