[Libre-soc-dev] daily kan-ban update 14nov2020

[Cesar Strauss]

Last week
==========

* Helped Cole and Luke with a I-cache unit test issue.

* Joined a discussion in nMigen about multi-clock formal verification.

It had to do with "Past(signal)", which should represent the state of
the signal on the previous clock. But, in which clock domain? And what
if the signal is asynchronous?

The current model is to take the domain from the context, but (as I
pointed out) you don't always have a context. A lively discussion ensued.

Some think you can use the clock in which the signal is updated, but
nMigen does not store this information. Others think you must always
write "Past(signal, domain=<domain>)" for non-default clock domains.

Also, "comb" would be a special "clock domain", for asynchronous signals.

In the process, I learned a bit about the subject. When you have only
one clock, it becomes the "formal time step". It's like event-driven
simulation, you don't really see the clock rising and falling. Also, the
clock is fair: as long as the verification progresses, the clock will tick.

In multi-clock, clocks become explicit. Flip-flops in the design are
automatically expanded to circuits that monitor, at each formal
time-step, if their clock rose, and only then store their inputs.

Formal verification no longer require input clocks to be fair. It can
generate a counter-example in which some clock never ticks enough, or at
all!

* Investigated liveness formal verification

So, I found a flaw in my formal verification of FSMs. For instance:

    with m.If(done):
        m.d.comb += Assert(result == expected)

In other words, whenever the FSM is done, check whether the result is as
expected. However, what if, for some input, the FSM becomes stuck, and
never produces any result at all? Since "done" never becomes active, the
assertion is never reached, and formal verification silently passes!

A (simple, dumb, effective) solution is to do bounded liveness checking,
which is to add a timeout counter to requests, and assert it never expires.

Another (better, elegant) solution is to do formal liveness checking,
which is supported by yosys, but not by nMigen as yet. In SystemVerilog,
it would be:

    always @(posedge clk)
        if (request)
            assert(s_eventually(done))

In other words, for each request, there will inevitably be a response in
some finite time. A counter-example is to find a request, followed by a
looped sequence of states in which "done" happens to be inactive all the
time. By repeating this loop indefinitely, you have your (infinite)
counter-example.

Interestingly, you can find such loops with a normal bounded model
checker, by a clever addition to the model. It saves a visited state, at
random, and asserts "I was already here, and that signal did not become
active, not once". See:
http://fmv.jku.at/papers/BiereArthoSchuppan-FMICS02.pdf.

Next week
=========

* Resume work on the CompUnit unit tests and formal verification.

Future work
===========

* Help Luke and Cole with the I-cache unit test. This involves studying
how it is really supposed to work, since the unit test from Microwatt is
of no help.

* Maybe, join the ongoing discussion on performance modeling of
parametrized multi-issue out-of-order execution architectures in face of
register dependency hazards and data-bus bottlenecks.

Regards,

Cesar