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

From: bugzilla-daemon@libre-soc.org
To: libre-riscv-dev@lists.libre-riscv.org
Subject: [libre-riscv-dev] [Bug 342] formal proof of soc.fu.compunits.FunctionUnitBaseSingle needed
Date: Mon, 25 May 2020 19:09:44 +0000
Message-ID: <bug-342-13-lIIMEAoTTY@https.bugs.libre-soc.org/> (raw)
In-Reply-To: <bug-342-13@https.bugs.libre-soc.org/>

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

--- Comment #5 from Luke Kenneth Casson Leighton <lkcl@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.
_______________________________________________
libre-riscv-dev mailing list
libre-riscv-dev@lists.libre-riscv.org
http://lists.libre-riscv.org/mailman/listinfo/libre-riscv-dev