X86-64-semantics
Semantics of x86-64 in K (by kframework)
hs-arm
(Dis)assembler and analyzer generated from the machine-readable ARMv8.3-A specification (by nspin)
| X86-64-semantics | hs-arm | |
|---|---|---|
| 1 | 1 | |
| 130 | 25 | |
| 1.5% | - | |
| 10.0 | 10.0 | |
| about 4 years ago | over 6 years ago | |
| Assembly | Haskell | |
| GNU General Public License v3.0 or later | - |
The number of mentions indicates the total number of mentions that we've tracked plus the number of user suggested alternatives.
Stars - the number of stars that a project has on GitHub. Growth - month over month growth in stars.
Activity is a relative number indicating how actively a project is being developed. Recent commits have higher weight than older ones.
For example, an activity of 9.0 indicates that a project is amongst the top 10% of the most actively developed projects that we are tracking.
Stars - the number of stars that a project has on GitHub. Growth - month over month growth in stars.
Activity is a relative number indicating how actively a project is being developed. Recent commits have higher weight than older ones.
For example, an activity of 9.0 indicates that a project is amongst the top 10% of the most actively developed projects that we are tracking.
X86-64-semantics
Posts with mentions or reviews of X86-64-semantics.
We have used some of these posts to build our list of alternatives
and similar projects. The last one was on 2022-01-30.
-
Machine readable specifications at scale
I guess I already ran into this argument in practice, with ISAs. For x86 there is an external machine-readable specification (semantics) in the K framework, built by fuzzing and reading the documentation.
hs-arm
Posts with mentions or reviews of hs-arm.
We have used some of these posts to build our list of alternatives
and similar projects. The last one was on 2022-01-30.
-
Machine readable specifications at scale
If I want to use the ARM spec I have to deal with ASL, but because ASL is a simpler language there is already an independent parser/implementation, hs-arm. OTOH I won't get the nice K features like automatic verification. Apparently you wrote a tool for ISA-Formal to translate ASL to Verilog - this doesn't seem to be public though.
What are some alternatives?
When comparing X86-64-semantics and hs-arm you can also consider the following projects:
riscv-formal - RISC-V Formal Verification Framework