[libre-riscv-dev] [Bug 120] implement RISC-V FSGNJ instruction

bugzilla-daemon at libre-riscv.org bugzilla-daemon at libre-riscv.org
Mon Jan 27 00:09:38 GMT 2020


--- Comment #10 from Luke Kenneth Casson Leighton <lkcl at lkcl.net> ---
(In reply to Michael Nolan from comment #9)
> > i need your agreement (on-list) to the charter, first.
> I (just now) replied to the HDL Workflow thread with my agreement.


> > that's a little trickier as it's outside of everyone currently in the teams' experience.
> I should probably have mentioned this in my intro post, but I have some
> experience with formal verification (the yosys flavor anyway). Provided the
> pipeline control signals don't screw things up too much, it should be pretty
> straightforward.

niiice. that'll come in real handy.

you'll be interested to know that one of the pipelines uses nmigen FIFO, and
that that does actually have a formal proof in nmigen as a unit test.  it's
worth taking a look at.

there is a lot to do here which is why formal proofs has its own entire budget.

let's keep this particular bugreport on topic though.

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

More information about the libre-riscv-dev mailing list