RISC-V CPU formal specification F# edition

• riscv-fs

  2 276 4.1 F#

  F# RISC-V Instruction Set formal specification

• rtasm

  2 13 2.6 C++

  Runtime Assembler for C++

I created this for x86 many years ago: https://github.com/kristiandupont/rtasm

It's not an emulator, it allows you to assemble code in C++ at runtime. It breaks down the architecture (as it looked at the time) quite detailed, if you are interested :-)

• InfluxDB

  www.influxdata.com featured

  Power Real-Time Data Analytics at Scale. Get real-time insights from all types of time series data with InfluxDB. Ingest, query, and analyze billions of data points in real-time with unbounded cardinality.

  

• riscv-coq

  1 99 5.8 Coq

  RISC-V Specification in Coq

  

>it allows to formally verify the correctness of a particular ISA

That must be hypothetical. Functionalness of the language doesn't make anything that is written in it automatically subject to formal verification. (mechanized or pen and paper). What kind of correctness properties does it actually allow to formally verify? I understand if it was the F* language, which is a full blown dependently typed proof checker, but with F#, which is defined by the implementation and 300 page English spec, I don't think you can verify anything interesting. As far as I know F# itself doesn't have mechanized formal semantics and its type system could be unsound.

https://github.com/mit-plv/riscv-coq and https://github.com/riscv/sail-riscv (don't know how complete they are) approaches actually allow to formally (mechanically) verify riscv properties.

• sail-riscv

  9 390 8.2 Coq

  Sail RISC-V model

  

>it allows to formally verify the correctness of a particular ISA

That must be hypothetical. Functionalness of the language doesn't make anything that is written in it automatically subject to formal verification. (mechanized or pen and paper). What kind of correctness properties does it actually allow to formally verify? I understand if it was the F* language, which is a full blown dependently typed proof checker, but with F#, which is defined by the implementation and 300 page English spec, I don't think you can verify anything interesting. As far as I know F# itself doesn't have mechanized formal semantics and its type system could be unsound.

https://github.com/mit-plv/riscv-coq and https://github.com/riscv/sail-riscv (don't know how complete they are) approaches actually allow to formally (mechanically) verify riscv properties.

• Forvis_RISCV-ISA-Spec

  1 96 10.0 Haskell

  Formal specification of RISC-V Instruction Set

I completely agree. And I specifically draw your attention to the fact that this is not a formal verification, which it would be reasonable to do: Coq, Isabellll, Agda, F* etc. However, Formal Specification. Those. representation of the specification in a formalized form. Haskell example: https://github.com/rsnikhil/Forvis_RISCV-ISA-Spec.

In this case, the term "formal" refers to the formalization of the representation of the specification. And it seems to be already established.

• SaaSHub

  www.saashub.com featured

  SaaSHub - Software Alternatives and Reviews. SaaSHub helps you find the best software and product alternatives

  

Suggest a related project