[libre-riscv-dev] [Bug 342] New: formal proof of soc.fu.compunits.FunctionUnitBaseSingle needed

[libre-riscv-dev] [Bug 342] New: formal proof of soc.fu.compunits.FunctionUnitBaseSingle needed

[bugzilla-daemon]

https://bugs.libre-soc.org/show_bug.cgi?id=342

            Bug ID: 342
           Summary: formal proof of
                    soc.fu.compunits.FunctionUnitBaseSingle needed
           Product: Libre-SOC's first SoC
           Version: unspecified
          Hardware: PC
                OS: Linux
            Status: CONFIRMED
          Severity: enhancement
          Priority: ---
         Component: Source Code
          Assignee: lkcl@lkcl.net
          Reporter: lkcl@lkcl.net
                CC: libre-riscv-dev@lists.libre-riscv.org
   NLnet milestone: ---

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

-- 
You are receiving this mail because:
You are on the CC list for the bug.
_______________________________________________
libre-riscv-dev mailing list
libre-riscv-dev@lists.libre-riscv.org
http://lists.libre-riscv.org/mailman/listinfo/libre-riscv-dev

[libre-riscv-dev] [Bug 342] formal proof of soc.fu.compunits.FunctionUnitBaseSingle needed

[bugzilla-daemon]

https://bugs.libre-soc.org/show_bug.cgi?id=342

Luke Kenneth Casson Leighton <lkcl@lkcl.net> changed:

           What    |Removed                     |Added
----------------------------------------------------------------------------
          Component|Source Code                 |Formal Verification
    NLnet milestone|---                         |NLNet.2019.10.Formal

-- 
You are receiving this mail because:
You are on the CC list for the bug.
_______________________________________________
libre-riscv-dev mailing list
libre-riscv-dev@lists.libre-riscv.org
http://lists.libre-riscv.org/mailman/listinfo/libre-riscv-dev

[libre-riscv-dev] [Bug 342] formal proof of soc.fu.compunits.FunctionUnitBaseSingle needed

[bugzilla-daemon]

https://bugs.libre-soc.org/show_bug.cgi?id=342

Luke Kenneth Casson Leighton <lkcl@lkcl.net> changed:

           What    |Removed                     |Added
----------------------------------------------------------------------------
           See Also|                            |https://bugs.libre-soc.org/
                   |                            |show_bug.cgi?id=341

-- 
You are receiving this mail because:
You are on the CC list for the bug.
_______________________________________________
libre-riscv-dev mailing list
libre-riscv-dev@lists.libre-riscv.org
http://lists.libre-riscv.org/mailman/listinfo/libre-riscv-dev

[libre-riscv-dev] [Bug 342] formal proof of soc.fu.compunits.FunctionUnitBaseSingle needed

[bugzilla-daemon]

https://bugs.libre-soc.org/show_bug.cgi?id=342

--- Comment #1 from Luke Kenneth Casson Leighton <lkcl@lkcl.net> ---
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.

-- 
You are receiving this mail because:
You are on the CC list for the bug.
_______________________________________________
libre-riscv-dev mailing list
libre-riscv-dev@lists.libre-riscv.org
http://lists.libre-riscv.org/mailman/listinfo/libre-riscv-dev

[libre-riscv-dev] [Bug 342] formal proof of soc.fu.compunits.FunctionUnitBaseSingle needed

[bugzilla-daemon]

https://bugs.libre-soc.org/show_bug.cgi?id=342

Michael Nolan <mtnolan2640@gmail.com> changed:

           What    |Removed                     |Added
----------------------------------------------------------------------------
                 CC|                            |mtnolan2640@gmail.com
           Assignee|lkcl@lkcl.net               |mtnolan2640@gmail.com

-- 
You are receiving this mail because:
You are on the CC list for the bug.
_______________________________________________
libre-riscv-dev mailing list
libre-riscv-dev@lists.libre-riscv.org
http://lists.libre-riscv.org/mailman/listinfo/libre-riscv-dev

[libre-riscv-dev] [Bug 342] formal proof of soc.fu.compunits.FunctionUnitBaseSingle needed

[bugzilla-daemon]

https://bugs.libre-soc.org/show_bug.cgi?id=342

Luke Kenneth Casson Leighton <lkcl@lkcl.net> changed:

           What    |Removed                     |Added
----------------------------------------------------------------------------
 total budget (EUR)|0                           |750
  for completion of|                            |
       task and all|                            |
           subtasks|                            |
    parent task for|                            |197
  budget allocation|                            |

-- 
You are receiving this mail because:
You are on the CC list for the bug.
_______________________________________________
libre-riscv-dev mailing list
libre-riscv-dev@lists.libre-riscv.org
http://lists.libre-riscv.org/mailman/listinfo/libre-riscv-dev

[libre-riscv-dev] [Bug 342] formal proof of soc.fu.compunits.FunctionUnitBaseSingle needed

[bugzilla-daemon]

https://bugs.libre-soc.org/show_bug.cgi?id=342

--- Comment #2 from Michael Nolan <mtnolan2640@gmail.com> ---
Does the module that this proof is for exist yet? I don't see it at the moment.

-- 
You are receiving this mail because:
You are on the CC list for the bug.
_______________________________________________
libre-riscv-dev mailing list
libre-riscv-dev@lists.libre-riscv.org
http://lists.libre-riscv.org/mailman/listinfo/libre-riscv-dev

[libre-riscv-dev] [Bug 342] formal proof of soc.fu.compunits.FunctionUnitBaseSingle needed

[bugzilla-daemon]

https://bugs.libre-soc.org/show_bug.cgi?id=342

--- Comment #3 from Luke Kenneth Casson Leighton <lkcl@lkcl.net> ---
(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.

-- 
You are receiving this mail because:
You are on the CC list for the bug.
_______________________________________________
libre-riscv-dev mailing list
libre-riscv-dev@lists.libre-riscv.org
http://lists.libre-riscv.org/mailman/listinfo/libre-riscv-dev

[libre-riscv-dev] [Bug 342] formal proof of soc.fu.compunits.FunctionUnitBaseSingle needed

[bugzilla-daemon]

https://bugs.libre-soc.org/show_bug.cgi?id=342

--- Comment #4 from Luke Kenneth Casson Leighton <lkcl@lkcl.net> ---
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.

-- 
You are receiving this mail because:
You are on the CC list for the bug.
_______________________________________________
libre-riscv-dev mailing list
libre-riscv-dev@lists.libre-riscv.org
http://lists.libre-riscv.org/mailman/listinfo/libre-riscv-dev

[libre-riscv-dev] [Bug 342] formal proof of soc.fu.compunits.FunctionUnitBaseSingle needed

[bugzilla-daemon]

https://bugs.libre-soc.org/show_bug.cgi?id=342

--- Comment #5 from Luke Kenneth Casson Leighton <lkcl@lkcl.net> ---
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.

-- 
You are receiving this mail because:
You are on the CC list for the bug.
_______________________________________________
libre-riscv-dev mailing list
libre-riscv-dev@lists.libre-riscv.org
http://lists.libre-riscv.org/mailman/listinfo/libre-riscv-dev

[libre-riscv-dev] [Bug 342] formal proof of soc.fu.compunits.FunctionUnitBaseSingle needed

[bugzilla-daemon]

https://bugs.libre-soc.org/show_bug.cgi?id=342

--- Comment #6 from Luke Kenneth Casson Leighton <lkcl@lkcl.net> ---
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?

-- 
You are receiving this mail because:
You are on the CC list for the bug.
_______________________________________________
libre-riscv-dev mailing list
libre-riscv-dev@lists.libre-riscv.org
http://lists.libre-riscv.org/mailman/listinfo/libre-riscv-dev

[libre-riscv-dev] [Bug 342] formal proof of soc.fu.compunits.FunctionUnitBaseSingle needed

[bugzilla-daemon]

https://bugs.libre-soc.org/show_bug.cgi?id=342

--- Comment #7 from Michael Nolan <mtnolan2640@gmail.com> ---
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.

-- 
You are receiving this mail because:
You are on the CC list for the bug.
_______________________________________________
libre-riscv-dev mailing list
libre-riscv-dev@lists.libre-riscv.org
http://lists.libre-riscv.org/mailman/listinfo/libre-riscv-dev

[libre-riscv-dev] [Bug 342] formal proof of soc.fu.compunits.FunctionUnitBaseSingle needed

[bugzilla-daemon]

https://bugs.libre-soc.org/show_bug.cgi?id=342

--- Comment #8 from Luke Kenneth Casson Leighton <lkcl@lkcl.net> ---
(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.

-- 
You are receiving this mail because:
You are on the CC list for the bug.
_______________________________________________
libre-riscv-dev mailing list
libre-riscv-dev@lists.libre-riscv.org
http://lists.libre-riscv.org/mailman/listinfo/libre-riscv-dev