[libre-riscv-dev] [Bug 336] ALU CompUnit needs to recognise that RA (src1) can be zero

[bugzilla-daemon@libre-soc.org]

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

--- Comment #39 from Luke Kenneth Casson Leighton <lkcl@lkcl.net> ---
(In reply to Cesar Strauss from comment #38)

> > in particular the ALU may *not* necessarily be ready to proceed at the time
> > operands are available.
> 
> Feel free to put this on my queue, if you wish (formal proof of the
> CompUnit-ALU interface).

sure, go for it.

> While I have no practical experience on formal proofs, I've been reading
> about it for some time, with the goal of applying it to my own designs. I
> like to think I've reached a good understanding.

good place to learn.

i would suggest simply adding them to proof_fu.py - focus on ready_(i/o),
valid_(i/o) - these are accessible signals.

if you assume that the DummyALU takes exactly one cycle between data_i and
data_o, this may make life easier.  the sequence will go:

* p.valid_i is set HI by CU
* p.ready_o is asserted HI by ALU in response (takes 1 cycle and asserts for
  ONLY one cycle)
* n.valid_o is asserted HI by ALU
* n.ready_i is set HI by CU
* n.valid_o is asserted LO by ALU in response (takes 1 cycle)

regarding data:

* data input should be placed by CU on the input at the same time as it
  raises p.valid_i.  it should REMAIN valid until p.ready_o is seen asserted.

* data output should be ready and valid when n_ready_i is HI.
all other times, it *may* still be left on the bus, but should *NOT* be
taken to be valid.

this is basically a standard ready/valid signalling system used by wishbone,
AXI4, etc. etc. etc. etc.

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