Groups | Search | Server Info | Keyboard shortcuts | Login | Register [http] [https] [nntp] [nntps]

Groups > comp.lang.forth > #135677

Re: First result in riscv optimiser

Show all headers | View raw

Kragen Javier Sitaker <kragen@canonical.org> writes:
>> I have 106 peephole patterns, some quite complicated.
> How confident are you that all 106 are correct?

It's sometimes possible to use SAT solvers to prove that two code
sequences are equivalent, without much human input.  There are also
formal models of RISC-V that you can put into a proof assistant.  Or
these days maybe you can throw the whole set into an LLM and ask for
formal proofs.

Back to comp.lang.forth | Previous | Next — Previous in thread | Next in thread | Find similar | Unroll thread

Thread

First result in riscv optimiser albert@spenarnc.xs4all.nl - 2026-09-01 10:49 +0200
  Re: First result in riscv optimiser anton@mips.complang.tuwien.ac.at (Anton Ertl) - 2026-09-01 15:33 +0000
    Re: First result in riscv optimiser albert@spenarnc.xs4all.nl - 2026-09-01 18:54 +0200
    Re: First result in riscv optimiser albert@spenarnc.xs4all.nl - 2026-09-02 11:18 +0200
    Re: First result in riscv optimiser Kragen Javier Sitaker <kragen@canonical.org> - 2026-09-04 13:14 -0300
      Re: First result in riscv optimiser albert@spenarnc.xs4all.nl - 2026-09-05 13:06 +0200
        Re: First result in riscv optimiser Kragen Javier Sitaker <kragen@canonical.org> - 2026-09-08 02:21 -0300
          Re: First result in riscv optimiser albert@spenarnc.xs4all.nl - 2026-09-08 12:38 +0200
            Re: First result in riscv optimiser Kragen Javier Sitaker <kragen@canonical.org> - 2026-09-11 07:50 -0300
              Re: First result in riscv optimiser Paul Rubin <no.email@nospam.invalid> - 2026-09-11 17:09 -0700
              Re: First result in riscv optimiser albert@spenarnc.xs4all.nl - 2026-09-13 14:03 +0200
            Re: First result in riscv optimiser antispam@fricas.org (Waldek Hebisch) - 2026-09-13 02:53 +0000

csiph-web