You signed in with another tab or window. Reload to refresh your session.You signed out in another tab or window. Reload to refresh your session.You switched accounts on another tab or window. Reload to refresh your session.Dismiss alert
Sail is a language for describing the instruction-set architecture (ISA) semantics of processors. The formal specification of RISC-V ISA is defined exactly in sail.
We could leverage sail to compile x86 and RISC-V models both down to Coq definitions. From there we can formally prove that our x86 assembly implementation of each RISC-V instruction, fully confronts to the RISC-V official specification.
Later when an aarch64 implementation is introduced, we could leverage the same proving techniques here.
This solution has the issue that Rust based interpreter cannot be proved. But once we have a formally proved assembly based fast implementation, not so many will care about Rust based interpreter :P
The text was updated successfully, but these errors were encountered:
Sail is a language for describing the instruction-set architecture (ISA) semantics of processors. The formal specification of RISC-V ISA is defined exactly in sail.
We could leverage sail to compile x86 and RISC-V models both down to Coq definitions. From there we can formally prove that our x86 assembly implementation of each RISC-V instruction, fully confronts to the RISC-V official specification.
Later when an aarch64 implementation is introduced, we could leverage the same proving techniques here.
This solution has the issue that Rust based interpreter cannot be proved. But once we have a formally proved assembly based fast implementation, not so many will care about Rust based interpreter :P
The text was updated successfully, but these errors were encountered: