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

bugzilla-daemon at libre-soc.org bugzilla-daemon at libre-soc.org
Tue Sep 22 13:09:34 BST 2020


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


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

More information about the libre-soc-bugs mailing list