search

jeras / rp32

RISC-V processor with CPI=1 (every single instruction executed in a single clock cycle).
Apache License 2.0
12 stars 3 forks source link

Have you tried applying riscv-formal to your processor? #3

Closed mithro closed 2 years ago

mithro commented 2 years ago

https://github.com/SymbioticEDA/riscv-formal is a framework for formal verification of RISC-V processors which uses fully open source tooling.

mithro commented 2 years ago

BTW -- Quite a few people have been successful applying riscv-format to their cores including https://github.com/olofk/serv and https://github.com/SpinalHDL/VexRiscv

jeras commented 2 years ago

The last time I checked, it seemed like a lot of work for a hobby project. I will look into it again when my CPU will be good enough to attract some users.

For now my main concern is whether the SystemVerilog instruction decoder really does what I wrote it for, without some unexpected overhead. And if it is versatile enough to be reusable. I was rather sure abut it till I compared logic resource consumption with other short pipeline RV32I implementations (reported on doc pages for VexRisc and NEORV32). From there I can write various pipeline configurations, that are not just a curiosity (the current IPC=1 pipeline).

I wanted to run VexRiscv synthesis myself, but I got afraid of polluting my Ubuntu with all the dependencies. SERV on the other hand is serial and is not great for logic utilization comparison.

mithro commented 2 years ago

No pressure! I know lots of people have had fun with it, so thought I would share.