[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 #29 from Cesar Strauss <cestrauss at gmail.com> ---
(In reply to Cesar Strauss from comment #27)
> 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

It also generates three GTKW documents, using the new write_gtkw API:

1) Coverage (similar to a test case):
$ gtkwave test_formal_cover_alu_fsm.gtkw

2) Bounded model check
$ gtkwave test_formal_bmc_alu_fsm.gtkw

3) Induction
$ gtkwave test_formal_induct_alu_fsm.gtkw

Note that traces for 2 and 3 are only actually generated if the corresponding
proof fails. They are empty now, but were useful during development, when they
did fail.

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