lion
riscv-formal
Our great sponsors
lion | riscv-formal | |
---|---|---|
10 | 10 | |
242 | 550 | |
0.8% | 3.6% | |
4.3 | 0.0 | |
about 2 months ago | about 2 years ago | |
Haskell | Verilog | |
BSD 3-clause "New" or "Revised" License | ISC License |
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.
lion
-
A year of RISC-V adventures: embracing chaos in your software journey [video]
I've been starting to dabble with digital logic design via Clash (https://clash-lang.org/), and there is a very cool-looking RISC-V SoC project done in that tool that looks fairly serious: https://github.com/standardsemiconductor/lion.
-
C++ Concurrency Model on x86 for Dummies
That’s fascinating about the M1. In retrospect it seems like kind of a no-brainer but I doubt I would have thought of it.
SPARC had different memory models at different ISA revs IIRC: it’s been like 20 years since I was dealing with SPARC so I might be misremembering the details. Alpha would have been a better example.
RISC-V is really interesting. I’ve been slowly working through this: https://github.com/standardsemiconductor/lion, highly recommend!
-
Why More Networks Should Imitate Cardano When It Comes To Writing And Shipping Code | Bitcoinist.com
Interesting. Actually, you may be just the person to answer my question: Is it possible/plausible to run a Cardano node on Lion OS on a RISC-V machine? IMO, it would be great for the community if we could run all Cardano stake pools on end to end formally verified machines using open source core and hardware.
- Lion is a formally verified, 5-stage pipeline RISC-V core
- Lion: A formally verified, 5-stage pipeline RISC-V core
-
Hacker News top posts: Mar 4, 2021
Lion: A formally verified, 5-stage pipeline RISC-V core\ (30 comments)
-
Where Lions Roam: RISC-V on the VELDT
In addition, you can actually set the riscv-formal suite to verify correctness by k-induction: https://github.com/SymbioticEDA/riscv-formal/pull/28 https://symbiyosys.readthedocs.io/en/latest/quickstart.html#beyond-bounded-model-checks although I concur that by looking at https://github.com/standardsemiconductor/lion/blob/main/lion-formal/app/Main.hs the lion core is only verified with BMC.
riscv-formal
-
RISC-V simulator
You might be able to hook up your simulator to risc v-formal https://github.com/SymbioticEDA/riscv-formal
- how is to use symbiflow in my fpga projects.
-
Machine readable specifications at scale
Then we have RISC, which wrote their own formal verification toolchain here. They just generate Verilog with a Python script. AFAICT this would be really hard to adapt to an assembler. Fortunately the ISA is simple to implement.
- Looking for an rv32i asm program that covers all possible scenarios of all instructions for testing
- Is a single cycle CPU of any use besides learning?
- When to use Formal Verification vs Simulation?
-
Where Lions Roam: RISC-V on the VELDT
Your question is certainly not dumb; on the contrary, it is very important! I suppose the developers are responsible for verifying the formal verifier and ensuring it covers the spec. Maybe there is a way to formally verify the formal verifier? Either way, I must give a shout out to the riscv-formal project and its contributors; the project was instrumental to the development of Lion.
Not trying to put words in your mouth, but I do want to clarify something for this audience: the bound in the BMC done by the riscv-formal suite is on the number of cycles, not on the number of bits. Case in point, when you try to BMC the (M)ultiply extensions with the riscv-formal suite, you're actually not allowed to use multiplication because the state space blows up: https://github.com/SymbioticEDA/riscv-formal/blob/master/docs/rvfi.md#alternative-arithmetic-operations
-
Any advices for my first RISC-V Core in Verilog ?
Use riscv-formal. It will save a ton of headaches trying to track down a bad instruction. It can generate a module that does checks on the fly during normal sims.
-
FPGA and Simulation tools for Risc-V design
I recommend SymbiYosys for formally testing your CPU before ever placing it into a simulation. You can use the riscv-formal property set to get you started, but I'd personally go for an inductive proof of some type and the riscv-formal property set may not get you that far.
What are some alternatives?
prometheus-cpp - Prometheus Client Library for Modern C++
riscv-arch-test
cocotb - cocotb, a coroutine based cosimulation library for writing VHDL and Verilog testbenches in Python
rp32 - RISC-V processor with CPI=1 (every single instruction executed in a single clock cycle).
atomic-story - Understanding how atomics and memory ordering work
riscv-tests
VexRiscv - A FPGA friendly 32 bit RISC-V CPU implementation
autofpga - A utility for Composing FPGA designs from Peripherals
libcxx - Project moved to: https://github.com/llvm/llvm-project
Cores-VeeR-EH1 - VeeR EH1 core
wit - WIT (Wikipedia-based Image Text) Dataset is a large multimodal multilingual dataset comprising 37M+ image-text sets with 11M+ unique images across 100+ languages.
hs-arm - (Dis)assembler and analyzer generated from the machine-readable ARMv8.3-A specification