1. 23
    1. 3

      The Sail project generated formal specifications of PowerPC by parsing the pseudocode in the PDF architecture references. I think that they found that the x86 docs at the time were too limited (inconsistent and incomplete) to do the same. I’m curious how well this project manages it. Arm eventually moved to auto-generating their pseudocode from their internal Architecture Specification Language (ASL) and there’s a tool that will transform ASL to Sail. The RISC-V official spec now uses Sail as well.

      1. 1

        Seems you are talking about this project, - https://github.com/rems-project/sail. Haven’t heard about it. I didn’t get - is possible to translate assembler instructions to SMT representation (smt-lib2) using Sail?

        1. 4

          Seems you are talking about this project, - https://github.com/rems-project/sail

          Yup.

          I didn’t get - is possible to translate assembler instructions to SMT representation (smt-lib2) using Sail?

          It can prove SMT properties inline and can export to a variety of theorem provers. We used this to prove monotonicity properties about CHERI capabilities, for example.

    2. 2

      Why doesn’t Intel just open source whatever model they use to do hardware verification? It’s absurd to me that we’re still building on top of such closed foundations.

      1. 1

        20 years ago they had to compete with PPC, ARM, SPARC, MIPS, et cetera. Nowadays it’s x86 or ARM. So what incentive do they have?