[Libre-soc-bugs] [Bug 879] New: Formal proof of soc.experiment.compalu_multi.MultiCompUnit needed

[bugzilla-daemon at libre-soc.org]

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

            Bug ID: 879
           Summary: Formal proof of
                    soc.experiment.compalu_multi.MultiCompUnit needed
           Product: Libre-SOC's first SoC
           Version: unspecified
          Hardware: PC
                OS: Linux
            Status: CONFIRMED
          Severity: enhancement
          Priority: ---
         Component: Formal Verification
          Assignee: cestrauss at gmail.com
          Reporter: cestrauss at gmail.com
                CC: libre-soc-bugs at lists.libre-soc.org
   NLnet milestone: NLNet.2019.10.032.Formal
    parent task for 197
 budget allocation:

In short, MultiCompUnit:

1) stores an opcode from Issue, when not "busy", and "issue" is pulsed
2) signals "busy" high
3) fetches its operand(s), if any (which are not masked or zero) from the
Scoreboard (REQ/REL protocol)
4) starts the ALU (ready/valid protocol), as soon as all inputs are available
5) captures result from ALU (again ready/valid)
5) sends the result(s) back to the Scoreboard (again REQ/REL)
6) pulses "done", and drops "busy"

Note that, if the conditions are right, many of the above can occur together,
on a single cycle.

The formal proof involves ensuring that:
1) the ALU gets the right opcode from Issue
2) the ALU gets the right operands from the Scoreboard
3) the Scoreboard receives the right result from the ALU
4) no transactions are dropped or repeated

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