sail-riscv

Sail RISC-V model (by riscv)
Review Suggest topics
Source Code
lists.riscv.org
sail-riscv Reviews
Suggest alternative
Edit details
SaaSHub - Software Alternatives and Reviews
SaaSHub helps you find the best software and product alternatives
www.saashub.com
featured

Sail-riscv Alternatives

Similar projects and alternatives to sail-riscv

riscv
sail-riscv

  1. riscv-isa-manual

    45 sail-riscv VS riscv-isa-manual

    RISC-V Instruction Set Manual

  2. SaaSHub

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

    SaaSHub logo

  3. riscv-profiles

    23 sail-riscv VS riscv-profiles

    RISC-V Architecture Profiles

  4. libriscv

    17 sail-riscv VS libriscv

    The fastest RISC-V sandbox

  5. riscv-isa-sim

    15 sail-riscv VS riscv-isa-sim

    Spike, a RISC-V ISA Simulator

  6. sandsifter

    17 sail-riscv VS sandsifter

    The x86 processor fuzzer

  7. riscv-boom

    12 sail-riscv VS riscv-boom

    SonicBOOM: The Berkeley Out-of-Order Machine

  8. riscv-fs

    2 sail-riscv VS riscv-fs

    F# RISC-V Instruction Set formal specification

  9. riscv-gnu-toolchain

    11 sail-riscv VS riscv-gnu-toolchain

    GNU toolchain for RISC-V, including GCC (by brucehoult)

  10. litmus-tests-riscv

    2 sail-riscv VS litmus-tests-riscv

    RISC-V architecture concurrency model litmus tests

  11. riscv-dv

    6 sail-riscv VS riscv-dv

    Random instruction generator for RISC-V processor verification

  12. riscv-coq

    1 sail-riscv VS riscv-coq

    RISC-V Specification in Coq

  13. riscv-opcodes

    5 sail-riscv VS riscv-opcodes

    RISC-V Opcodes

  14. riscv-config

    1 sail-riscv VS riscv-config

    RISC-V Configuration Validator

  15. force-riscv

    1 sail-riscv VS force-riscv

    Instruction Set Generator initially contributed by Futurewei

  16. Forvis_RISCV-ISA-Spec

    1 sail-riscv VS Forvis_RISCV-ISA-Spec

    Formal specification of RISC-V Instruction Set

  17. sail

    2 sail-riscv VS sail

    Sail architecture definition language (by rems-project)

  18. rtasm

    2 sail-riscv VS rtasm

    Runtime Assembler for C++

  19. herdtools7

    1 sail-riscv VS herdtools7

    The Herd toolsuite to deal with .cat memory models (version 7.xx)

  20. tinyrv

    1 sail-riscv VS tinyrv

    A tiny RISC-V instruction decoder and instruction set simulator

  21. asciidoctor-sail

    1 sail-riscv VS asciidoctor-sail

    Sail Asciidoctor plugin

NOTE: The number of mentions on this list indicates mentions on common posts plus user suggested alternatives. Hence, a higher number means a better sail-riscv alternative or higher similarity.
Suggest an alternative to sail-riscv

sail-riscv discussion

Log in or Post with

sail-riscv reviews and mentions

Posts with mentions or reviews of sail-riscv. We have used some of these posts to build our list of alternatives and similar projects. The last one was on 2024-04-28.
  • How to improve the RISC-V specification
    9 projects | news.ycombinator.com | 28 Apr 2024
    I've been doing a lot of work with Sail (not SAIL btw) and I'm not sure I agree with the points about it.

    There's already a way to extract functions into asciidoc as the author noted. I've used it. It works well.

    The liquid types do take some getting used to but they aren't actually used in most of the code; mostly for utility function definitions like `zero_extend`. If you look at the definition for simple instructions they can be very readable and practically pseudocode:

    https://github.com/riscv/sail-riscv/blob/0aae5bc7f57df4ebedd...

    A lot of instructions are more complex or course but that's what you get if you want to precisely define them.

    Overall Sail is a really fantastic language and the liquid types really help avoid bugs.

    The biggest actual problems are:

    1. The RISC-V spec is chock full of undefined / implementation defined behaviour. How do you capture that in code, where basically everything is defined. The biggest example is probably WARL fields which can do basically anything. Another example is decomposing misaligned accesses. You can decompose them into any number of atomic memory operations and do them in any order. E.g. Spike decomposes them into single byte accesses. (This problem isn't really unique to Sail tbf).

    2. The RISC-V Sail model doesn't do a good job of letting you configure it currently. E.g. you can't even set the spec version at the moment. This is just an engineering problem though. We're hoping to fix it one day using riscv-config which is a YAML file that's supposed to specify all the configurable behaviour about a RISC-V chip.

    I definitely agree about the often wooly language in the spec though. It doesn't even use RFC-style MUST/SHOULD/MAY terms.

  • RISC-V Vector benchmark results
    4 projects | news.ycombinator.com | 11 Nov 2023
    The official formal specification of the Vector Extension has just been merged into the Golden RISC-V model:

    https://github.com/riscv/sail-riscv/commit/c90cf2e6eff5fa4ef...

  • Cascade: CPU Fuzzing via Intricate Program Generation
    3 projects | news.ycombinator.com | 23 Oct 2023
    the retired instruction counters when written by software.

    Funnily enough the Sail model had this bug too! https://github.com/riscv/sail-riscv/issues/256

  • Arm’s Cortex A510: Two Kids in a Trench Coat
    1 project | news.ycombinator.com | 2 Oct 2023
    > loose specification of the RISC-V ISA.

    This is being worked on with the Sail model [1]. In order for a RISC-V extension to be ratified it ought to be implemented in Sail. The understanding is also that the RISC-V ISA manual should be built with code snippets from the Sail model (similar to how the Arm Arm is build from ASL definition). The main issue is a lack of people willing and able to write Sail for RISC-V. But that is beginning to change, since RISC-V member companies are increasingly use Sail. As an example, the RISC-V exception type is defined in [2]. Is that precise enough for you?

    [1] https://github.com/riscv/sail-riscv

    [2] https://github.com/riscv/sail-riscv/blob/master/model/riscv_...

  • RISC-V CPU formal specification F# edition
    6 projects | news.ycombinator.com | 28 Jul 2023
    >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.

  • 64-bit Arm ∩ 64-bit RISC V
    2 projects | /r/asm | 7 Jun 2023
  • C++17 RISC-V RV32/64/128 userspace emulator library
    5 projects | news.ycombinator.com | 18 Nov 2022
  • Starting up with RISC-V
    3 projects | /r/RISCV | 4 Feb 2022
    I guess you will also use Spike and the Sail model for RISC-V.
  • Areas to contribute in RISC-V RTL verification
    5 projects | /r/RISCV | 6 Mar 2021
    Doing something leveraging the SAIL model would be valuable, as that's the official formal model: https://github.com/rems-project/sail-riscv
  • A note from our sponsor - SaaSHub
    www.saashub.com | 24 Jan 2025
    SaaSHub helps you find the best software and product alternatives Learn more →

Stats

Basic sail-riscv repo stats
9
491
9.2
9 days ago

riscv/sail-riscv is an open source project licensed under GNU General Public License v3.0 or later which is an OSI approved license.

The primary programming language of sail-riscv is Coq.

Popular Comparisons

  1. sail-riscv VS riscv-fs
  2. sail-riscv VS riscv-dv
  3. sail-riscv VS litmus-tests-riscv
  4. sail-riscv VS riscv-isa-sim
  5. sail-riscv VS libriscv
  6. sail-riscv VS riscv-coq
  7. sail-riscv VS riscv-config
  8. sail-riscv VS force-riscv
  9. sail-riscv VS Forvis_RISCV-ISA-Spec
  10. sail-riscv VS sandsifter

Sponsored
SaaSHub - Software Alternatives and Reviews
SaaSHub helps you find the best software and product alternatives
www.saashub.com
Loading...