[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 #28 from Luke Kenneth Casson Leighton <lkcl at lkcl.net> ---
(In reply to Cesar Strauss from comment #27)
> Some updates:
> 
> 1) The design now works under both pysim and cxxsim.

fantastic.  there is reasonable demonstration now that if there
are issues with cxxsim it's probably not in the CompUnits.

> 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

nice!

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

yes it is quite common for proofs to be very closely tied to the
implementation details.

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

you can create classes (Formal Correctness Proofs are modules after all)
and you _should_ be able to create a FSM Formal Proof base class then
over-ride the shifter and sub-class (child module) the shifter proof.

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