[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 #5 from Luke Kenneth Casson Leighton <lkcl at lkcl.net> ---
extra little funny things that can be thrown in:

* all of rd.go, rd.req, wr.go, wr.req, and issue: if done_o is LOW then
  absolutely all of those should be LOW as well.

  the reason for the existence of done_o over busy_o is because, sigh,
  if you look closely, you can see that some of the latches are reset
  synchronously (a 1 clock delay).  this means that busy_o actually
  drops immediately on completion, and done_o drops a cycle later.

* when the write phase has started, the rd phase is *definitely* over.
  therefore, if wr.req is non-zero, rd.req and rd.go should *definitely*
  be non-zero.

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