Bug 342 - formal proof of soc.fu.compunits.FunctionUnitBaseSingle needed
Summary: formal proof of soc.fu.compunits.FunctionUnitBaseSingle needed
Status: RESOLVED FIXED
Alias: None
Product: Libre-SOC's first SoC
Classification: Unclassified
Component: Formal Verification (show other bugs)
Version: unspecified
Hardware: PC Linux
: --- enhancement
Assignee: Cesar Strauss
URL:
Depends on:
Blocks:
 
Reported: 2020-05-23 23:57 BST by Luke Kenneth Casson Leighton
Modified: 2022-09-25 19:28 BST (History)
1 user (show)

See Also:
NLnet milestone: NLNet.2019.10.032.Formal
total budget (EUR) for completion of task and all subtasks: 2500
budget (EUR) for this task, excluding subtasks' budget: 2500
parent task for budget allocation: 197
child tasks for budget allocation:
The table of payments (in EUR) for this task; TOML format:
"cesar"={amount=2500,submitted=2022-07-04,paid=2022-07-21}

Attachments
Add an attachment (proposed patch, testcase, etc.)

Note You need to log in before you can comment on or make changes to this bug.
Description Luke Kenneth Casson Leighton 2020-05-23 23:57:30 BST 
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
Comment 1 Luke Kenneth Casson Leighton 2020-05-24 00:17:09 BST 
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
REQ/GO signals.
Comment 2 Michael Nolan 2020-05-24 21:29:06 BST 
Does the module that this proof is for exist yet? I don't see it at the moment.
Comment 3 Luke Kenneth Casson Leighton 2020-05-24 21:40:42 BST 
(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
> moment.

soc.fu.compunits.FunctionUnitBaseSingle.

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.
Comment 4 Luke Kenneth Casson Leighton 2020-05-25 20:00:32 BST 
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

            with m.If(busy):
                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.
Comment 5 Luke Kenneth Casson Leighton 2020-05-25 20:09:44 BST 
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*
  be non-zero.
Comment 6 Luke Kenneth Casson Leighton 2020-05-25 21:56:03 BST 
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?
Comment 7 Michael Nolan 2020-05-26 18:35:49 BST 
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.
Comment 8 Luke Kenneth Casson Leighton 2020-05-26 18:52:49 BST 
(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.
Comment 9 Luke Kenneth Casson Leighton 2020-12-02 14:55:36 GMT 
cesar, would you like to have a go at this one?