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

[bugzilla-daemon at libre-riscv.org]

http://bugs.libre-riscv.org/show_bug.cgi?id=120

--- 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.

appreciated.

> > 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.