[libre-riscv-dev] [Bug 61] Formal Mathematical Proofs needed

[Luke Kenneth Casson Leighton]

hendrik: does the demo at the end (bounded proof) mean *anything* to you?
https://symbiyosys.readthedocs.io/en/latest/quickstart.html

what about this?
https://github.com/m-labs/nmigen/blob/master/nmigen/test/test_lib_fifo.py

ngggggh!

On Wed, May 1, 2019 at 8:54 PM <bugzilla-daemon at libre-riscv.org> wrote:
>
> http://bugs.libre-riscv.org/show_bug.cgi?id=61
>
> --- Comment #6 from Luke Kenneth Casson Leighton <lkcl at lkcl.net> ---
> https://github.com/m-labs/nmigen/blob/master/nmigen/test/test_lib_fifo.py
>
> tracking through from there is something called FHDLTestCase.assertFormal
> which calls the prerequisite sby proof, creating the sby config file
> in the process.
>
> --
> You are receiving this mail because:
> You are on the CC list for the bug.
> _______________________________________________
> libre-riscv-dev mailing list
> libre-riscv-dev at lists.libre-riscv.org
> http://lists.libre-riscv.org/mailman/listinfo/libre-riscv-dev