sail
riscv-profiles
sail | riscv-profiles | |
---|---|---|
2 | 21 | |
546 | 87 | |
6.0% | - | |
9.5 | 8.0 | |
4 days ago | about 1 month ago | |
Isabelle | Makefile | |
GNU General Public License v3.0 or later | Creative Commons Attribution 4.0 |
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.
sail
-
How to improve the RISC-V specification
Sail is pretty similar to ASL (both current ASL and ASL 1.0) except that (1) it has a more expressive type system, so that bitvector lengths can all be statically checked, (2) it has proper tagged unions and pattern matching, and (3) there's a wide range of open-source tooling available, for execution, specification coverage, generating emulators, integrating with relaxed concurrency models, generating theorem-prover definitions, etc. We've recently updated the Sail README, which spells some of this out: https://github.com/rems-project/sail .
As Alastair Reid says, one of the main things missing in the current RISC-V specification documents is simply that the associated Sail definitions are not yet interspersed with the prose instruction descriptions. The infrastructure to do that has been available for some time, in the Sail AsciiDoc support by Alasdair Armstrong (https://github.com/Alasdair/asciidoctor-sail/blob/master/doc...) and older LaTeX versions by Prashanth Mundkur and Alasdair (https://github.com/rems-project/riscv-isa-manual/blob/sail/r...).
-
Candy – a minimalistic functional programming language
That's completely feasible and there are languages that do this. It doesn't really eliminate the need to run your program unless the inputs to your program are also completely restricted types like One, Two, Three. In which case yeah, you don't need to run it and the type system can just tell you the answer.
I believe you can do that sort of thing in loads of type systems, e.g. Typescript, but there are languages that intentionally support it. I use a niche DSL that has fancy types like this called Sail. https://github.com/rems-project/sail
In my experience the downsides of these fancy "first class type systems" are
1. More incomprehensible error messages.
2. The type checker moves from a deterministic process that either succeeds or fails in an understandable way, to SMT solvers which can just say "yep it's ok" or "nope, couldn't prove it", semi-randomly, and there's little you can do about it.
Still my experience of Sail is that it's very comfortable to go a little bit further into SMT land, and my experience of Dafny is that it's very unpleasant to go full formal-verification at the moment.
I've done a fair bit of hardware formal verification too and that's a different story - very easy and very powerful. I'm hoping one day that software formal verification is like that.
riscv-profiles
-
How to improve the RISC-V specification
Ssstrict is supposed to address the undefined behaviour problem, or at least it'll make undefined instructions actually trap.
https://github.com/riscv/riscv-profiles/blob/main/rva23-prof...
-
Raspberry Pi receives strategic investment from Arm
>there are a lot of incompatible ISA implementations of RISC-V
This is common FUD.
In reality, most chips in the market, including all known application processors, follow the RVA profile[0] spec.
So do Linux distributions.
0. https://github.com/riscv/riscv-profiles/releases
-
You Won’t Believe This One Weird CPU Instruction (2019)
The bit manipulation [0] extension has been ratified for a while now and is part of the RVA22 application extension profile [1].
You can already buy SOCs that support it, e.g. vision five 2 and star64.
Interestingly the risc-v vector has it's own popcount instructions for vector registers/register masks. This is needed, because the scalable architecture doesn't guarantee that a vector mask can fit into a 64 bit register, so vector masks are stored in a single LMUL=1 register. This works really well, because with LMUL=8 and SEW=8 you get 100% utilization of the single LMUL=1 vector register.
Another interesting thing is that the vector crypto extension will likely introduce a element wise popcount instruction.
[0] https://github.com/riscv/riscv-bitmanip/releases/download/1....
[1] https://github.com/riscv/riscv-profiles/blob/main/profiles.a...
-
The legend of "x86 CPUs decode instructions into RISC form internally"
That's why we have RISC-V profiles.
-
Why is std::hardware_destructive_interference_size a compile-time constant instead of a run-time value?
Yeah more or less. They now have RISC-V Application Profiles which are basically minimum requirements for "application processors" - essentially devices like phones where you might want to distribute binary apps.
-
RISC-V Profiles: Defining sets of extensions for coherent ecosystems
The Profiles spec which includes RVA22 was finally ratified[0] last week.
0. https://github.com/riscv/riscv-profiles/releases/tag/v1.0
-
RISC-V Profiles
Context: RISC-V profiles spec got ratified last week.
- Questions about standard extensions
-
RISC-V Business: Testing StarFive's VisionFive 2 SBC
Yeah unfortunately there isn't really a great place that lists all the extensions with links and ratification status.
But anyway there is a sort of standard set of extensions that "application processors" (I guess CPUs that want to run precompiled code) should support:
https://github.com/riscv/riscv-profiles/blob/main/profiles.a...
The 22 indicates the year.
-
TinyEMU – x86 and RISC-V emulator, small and simple while being complete
Ah, you're right: https://github.com/riscv/riscv-profiles/blob/main/profiles.a...
That's good to see. (Boy, it's really hard to find info about RISC-V profiles on Google. It just seems to ignore all the letters and numbers.)
What are some alternatives?
riscv-platform-specs - RISC-V Profiles and Platform Specification
xuantie-yocto - Yocto project for Xuantie RISC-V CPU
openc906 - OpenXuantie - OpenC906 Core
riscv-v-spec - Working draft of the proposed RISC-V V vector extension
volk - The Vector Optimized Library of Kernels
riscv-bitmanip - Working draft of the proposed RISC-V Bitmanipulation extension
linux-on-litex-vexriscv - Linux on LiteX-VexRiscv
riscv-code-size-reduction
VisionFive2
openc910 - OpenXuantie - OpenC910 Core
herdtools7 - The Herd toolsuite to deal with .cat memory models (version 7.xx)
PSn00bSDK - The most powerful open source SDK for the PS1 (as far as open source PS1 SDKs go). Not recommended for beginner use.