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

bugzilla-daemon at libre-soc.org bugzilla-daemon at libre-soc.org
Mon May 25 20:00:32 BST 2020


--- 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.

More information about the libre-riscv-dev mailing list