we need a formal proof of both MultiCompUnit and FunctionUnitBaseSingle.
a formal proof of the ALU that is used is *not* necessary, so a very
basic (stub) ALU can be created and used.
however, the proof needs to be written to test the following:
* 1 to 3 src input operands
* 1 to 2 dest operands
* with *and without* zero_a capabiltiy
* with *and without* immediate capability
so that's actually quite a lot of combinations: 3x2x2x2
the tricky bit: MultiCompUnit is time-dependent. that involves use
of "Past()". it is similar in some ways to the formal proof for
SyncFIFO because it is similar signalling rules on each of the
Does the module that this proof is for exist yet? I don't see it at the moment.
(In reply to Michael Nolan from comment #2)
> Does the module that this proof is for exist yet? I don't see it at the
although it's probably a good idea to start with MultiCompUnit instead
(and alu_hier.ALU or probably better alu_hier.DummyALU as a first experiment)
the actual ALU doesn't matter as much as the CompUnit.
michael am just going over the notes in proof_fu.py
# Assume no instruction is issued until rd_rel is
# released. Idk if this is valid
comb += Assume(issue == 0)
ok so yes, nothing happens at the ALU - nothing is sent to the ALU - until
all incoming operands are valid, and the condition for that is:
* busy_o is set HI
* all bits of rd_rel are LOW
note btw the industry-standard convention in circuits, a "N" at the end
of a name indicates that it is inverted from what you would normally think
its function should be. this means shadown is LOW if shadowing is requested,
and when shadown is HI, shadowing is *not* being enabled.
extra little funny things that can be thrown in:
* all of rd.go, rd.req, wr.go, wr.req, and issue: if done_o is LOW then
absolutely all of those should be LOW as well.
the reason for the existence of done_o over busy_o is because, sigh,
if you look closely, you can see that some of the latches are reset
synchronously (a 1 clock delay). this means that busy_o actually
drops immediately on completion, and done_o drops a cycle later.
* when the write phase has started, the rd phase is *definitely* over.
therefore, if wr.req is non-zero, rd.req and rd.go should *definitely*
another one, a part of the API: issue_i is only asserted for one cycle.
however as an external signal i have no idea how that woule be expressed. Assume?
with m.If(Past(wr_rel) & Past(go_wr)):
# the alu data is output
comb += Assert(dut.data_o == alu_temp)
# wr_rel is dropped
comb += Assert(wr_rel == 0)
# busy is dropped.
comb += Assert(busy == 0)
Shouldn't the module drop busy after go_die is asserted? If I delete the m.If(~Past(go_die)) the proof fails.
(In reply to Michael Nolan from comment #7)
> with m.If(Past(wr_rel) & Past(go_wr)):
> # the alu data is output
> comb += Assert(dut.data_o == alu_temp)
> # wr_rel is dropped
> comb += Assert(wr_rel == 0)
> # busy is dropped.
> with m.If(~Past(go_die)):
> comb += Assert(busy == 0)
> Shouldn't the module drop busy after go_die is asserted? If I delete the
> m.If(~Past(go_die)) the proof fails.
annoyingly, it's one cycle after, because of the syncs setting the latches.
fascinatingly, in practice, we get away with it. the code is complex enough
that i am not sure why.
cesar, would you like to have a go at this one?
FSM CompUnit proof, using a shifter unit as an ALU to be tested