M-Labs/riscv-formal-nmigen
6
0
Fork 0
Code Issues Pull Requests Releases Wiki Activity

Add "Known Issues" section to README

Browse Source
This commit is contained in:
Donald Sebastian Leung 2020-08-21 16:58:33 +08:00
parent dad6022572
commit 607d82f27c
1 changed files with 4 additions and 0 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

4
README.md
View File

@ -33,6 +33,10 @@ This should run in the order of a few minutes.
Support for the RV32I base ISA and RV32M extension are planned and well underway. Support for other ISAs in the original riscv-formal such as RV32C and their 64-bit counterparts may also be added in the future as time permits.
## Known Issues
As of 21/08/2020, the verification passes unconditionally, even when obvious, deliberate bugs are introduced to the Minerva core and/or its components thereof (such as replacing subtraction with addition in the adder). This is caused by the Minerva core having its `rvfi.valid` signal de-asserted all of the time. The cause of this issue is very likely due to the absence of proper interrupt signals and instruction + data buses, which must be connected to the core for it to function properly. Perhaps the issue could be solved by constructing abstract instruction + data buses with suitable assumed properties and connecting those abstract interfaces to the Minerva core (but then, what would those properties be?).
## License
See [LICENSE](./LICENSE)