[libre-riscv-dev] [Bug 342] formal proof of soc.fu.compunits.FunctionUnitBaseSingle needed

[bugzilla-daemon at libre-soc.org]

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

--- Comment #4 from Luke Kenneth Casson Leighton <lkcl at lkcl.net> ---
michael am just going over the notes in proof_fu.py

            # Assume no instruction is issued until rd_rel is
            # released. Idk if this is valid

            with m.If(busy):
                comb += Assume(issue == 0)

ok so yes, nothing happens at the ALU - nothing is sent to the ALU - until
all incoming operands are valid, and the condition for that is:

* busy_o is set HI
* all bits of rd_rel are LOW


note btw the industry-standard convention in circuits, a "N" at the end
of a name indicates that it is inverted from what you would normally think
its function should be.  this means shadown is LOW if shadowing is requested,
and when shadown is HI, shadowing is *not* being enabled.

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