[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:12:30 BST 2020
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.
More information about the libre-soc-bugs
mailing list