[Libre-soc-bugs] [Bug 590] Formally verify experiments/icache.py

bugzilla-daemon at libre-soc.org bugzilla-daemon at libre-soc.org
Mon Feb 8 23:01:21 GMT 2021


--- Comment #2 from Cesar Strauss <cestrauss at gmail.com> ---
(In reply to Cole Poirier from comment #0)
> Presently, I'm taking inspiration from Cesar's excellent
> fu/compunits/formal/proof_fu.py, with detailed comments for each of the N
> properties that must hold for the formal verification to pass.

Thanks, but that's not my work. Here are some of mine:

A FSM Shifter with valid/ready handshake:


The main thing here is counting input and output transfers, and asserting that
they are equal. Unless the unit is busy, then they differ by one.

Partitioned Signals:


This one seems pretty complex, but it really is all about implementing the
strategy defined in the first paragraph.

Anyway, for the ICache I would recommend first to understand what it is
supposed to do. Maybe, capture a VCD trace from a Microwatt simulation, and
read the code while following the traces.

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

More information about the libre-soc-bugs mailing list