[Libre-soc-bugs] [Bug 417] FSM-based ALU example needed (compliant with ALU CompUnit)

[bugzilla-daemon at libre-soc.org]

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

--- Comment #27 from Cesar Strauss <cestrauss at gmail.com> ---
Some updates:

1) The design now works under both pysim and cxxsim.

2) To gain experience, ended-up writing a formal proof for it, with coverage,
bounded model check, and induction:

src/soc/experiment/formal/proof_alu_fsm.py

https://git.libre-soc.org/?p=soc.git;a=blob;f=src/soc/experiment/formal/proof_alu_fsm.py;h=bb83c9187d69c73a624079e605b42c40f16b7fb4;hb=70cee4d6e7d454c5378b455dd8a2779dbd82adcd

Note that this proof relies on the FSM nature of the Shifter (at most one
operation in flight), and will likely not work on a pipelined design.

Next steps:

1) I think the FSM can have a shortcut from DONE directly to SHIFT (bypassing
IDLE) when the output data is accepted, and there is already an input waiting.
It should avoid wasting one clock period, improving throughput.

2) Maybe, add a logarithmic pipelined shifter, for comparison.

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