[Libre-soc-bugs] [Bug 419] MUL pipeline formal proof needed

[bugzilla-daemon at libre-soc.org]

https://bugs.libre-soc.org/show_bug.cgi?id=419

--- Comment #7 from Luke Kenneth Casson Leighton <lkcl at lkcl.net> ---
commit 2e117c06cb6b147e59e80fcba6d060695c62766e (HEAD -> master, origin/master)
Author: Luke Kenneth Casson Leighton <lkcl at lkcl.net>
Date:   Wed Aug 19 07:24:58 2020 +0100

    bit of a reorg of mul proof, tracking down missing
    Assume op.is_32bit == 0 for OP_MUL_H32

ok now we've worked out that OP_MUL_H32 is only suited to 32-bit,
the next step is to do the signed multiply.  this is the implementation
from decode/helpers.py of a python-based signed multiply:

# signed version of MUL
def MULS(a, b):
    a_s = a.value & (1 << (a.bits-1)) != 0
    b_s = b.value & (1 << (b.bits-1)) != 0
    result = abs(a) * abs(b)
    print("MULS", result, a_s, b_s)
    if a_s == b_s:
        return result
    return -result 

because - again - OP_MUL_H32 *only* works on 32-bit numbers, we can
do:

   a_s = a[31]
   b_s = b[31]

rather than mungy-mess above (which copes with variable-size numbers)

-- 
You are receiving this mail because:
You are on the CC list for the bug.