 Donald Sebastian Leung
|
425bc49784
|
Parallelize all verification tasks for Minerva
|
2020-09-18 15:59:59 +08:00 |
|
Donald Sebastian Leung
|
b0a914b48e
|
Parallelize instruction verification tasks
|
2020-09-18 13:23:17 +08:00 |
|
Donald Sebastian Leung
|
c4cbc4bfea
|
Explicitly define reset value in cycle signal for uniqueness check
|
2020-09-17 13:25:52 +08:00 |
|
Donald Sebastian Leung
|
32388adce0
|
Make liveness checks pass
|
2020-09-17 13:22:52 +08:00 |
|
Donald Sebastian Leung
|
b38f19411a
|
Make uniqueness checks pass
|
2020-09-17 13:08:04 +08:00 |
|
Donald Sebastian Leung
|
ee19bc49e7
|
Add bounded fairness constraints for liveness check
|
2020-09-15 17:12:58 +08:00 |
|
Donald Sebastian Leung
|
0f4a2a76bd
|
Tweak parameters for Minerva verification tasks
|
2020-09-15 15:44:02 +08:00 |
|
Donald Sebastian Leung
|
a9f1431959
|
Record failing instructions in individual instruction checks
|
2020-09-07 15:43:39 +08:00 |
|
Donald Sebastian Leung
|
d84852e368
|
Replace unconditional pass and OOM issue with assertion failure
|
2020-09-07 12:32:14 +08:00 |
|
Donald Sebastian Leung
|
fe835e272d
|
Replace RV32I with RV32M for Minerva verification tasks
|
2020-08-27 10:48:35 +08:00 |
|
Donald Sebastian Leung
|
ca9e9c9ca6
|
Add prototype for instruction/data bus implementation
|
2020-08-25 12:41:30 +08:00 |
|
Donald Sebastian Leung
|
ac7991ae86
|
Merge instruction and data bus abstractions
|
2020-08-25 10:12:02 +08:00 |
|
Donald Sebastian Leung
|
ca135d024f
|
Wire instruction and data buses (WIP) to Minerva core
|
2020-08-24 14:46:52 +08:00 |
|
Donald Sebastian Leung
|
2a4f6dd07e
|
Wire interrupt signals to Minerva for verification
|
2020-08-24 13:28:33 +08:00 |
|
Donald Sebastian Leung
|
ee80bff3db
|
Merge riscv_formal_parameters.py into verify.py
|
2020-08-24 10:20:30 +08:00 |
|
Donald Sebastian Leung
|
dad6022572
|
Replace individual instruction checks with ISA check
|
2020-08-21 15:14:42 +08:00 |
|
Donald Sebastian Leung
|
908ecf9e7e
|
Add uniqueness check
|
2020-08-21 13:25:52 +08:00 |
|
Donald Sebastian Leung
|
a7b6b7a169
|
Add liveness check
|
2020-08-21 12:54:53 +08:00 |
|
Donald Sebastian Leung
|
d7d4f8b0ad
|
Reduce code duplication in Minerva verification script
|
2020-08-21 11:43:20 +08:00 |
|
Donald Sebastian Leung
|
1a38b37473
|
Remove copy of Minerva
|
2020-08-20 15:32:10 +08:00 |
|
Donald Sebastian Leung
|
a6b4891a38
|
Add causal checks
|
2020-08-20 12:00:31 +08:00 |
|
Donald Sebastian Leung
|
2a9ddf0868
|
Add register checks
|
2020-08-20 11:10:33 +08:00 |
|
Donald Sebastian Leung
|
2383706012
|
Add PC backward checks
|
2020-08-19 17:22:03 +08:00 |
|
Donald Sebastian Leung
|
2bfd909b49
|
Add PC forward checks
|
2020-08-19 17:00:11 +08:00 |
|
Donald Sebastian Leung
|
c073411bd2
|
Add tests for all RV32I instructions
|
2020-08-19 14:56:26 +08:00 |
|
Donald Sebastian Leung
|
0e0d4b6e42
|
Add (currently failing) test case for LUI instruction
|
2020-08-18 14:10:47 +08:00 |
|
Donald Sebastian Leung
|
3faa8ed1b8
|
Add build instructions for Minerva
|
2020-08-17 16:46:15 +08:00 |
|
Donald Sebastian Leung
|
73707afe78
|
Modularize codebase
|
2020-08-17 11:50:53 +08:00 |