Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

VexRiscv imem/dmem checks #5

Merged
merged 5 commits into from Nov 26, 2017
Merged
Changes from 1 commit
Commits
File filter...
Filter file types
Jump to…
Jump to file
Failed to load files.

Always

Just for now

Add dmemcheck

  • Loading branch information
Dolu1990 committed Nov 26, 2017
commit 1be1a23cd5c2941872f0017cfbcf31fb0e2620e3
@@ -3,7 +3,7 @@ riscv-formal proofs for VexRiscv
================================

### Current state:
Test a simple VexRiscv configuration (https://github.com/SpinalHDL/VexRiscv/blob/formal/src/main/scala/vexriscv/demo/FormalSimple.scala)
Test a simple VexRiscv configuration (https://github.com/SpinalHDL/VexRiscv/blob/master/src/main/scala/vexriscv/demo/FormalSimple.scala)

All standards checks are passing
- Instruction Checks
@@ -14,6 +14,7 @@ All standards checks are passing

Other tests passing :
- Instruction Memory check
- Data Memory check

### Quickstart guide:

@@ -38,15 +39,15 @@ export test=insn_beq_ch0; rm -r checks/$test; make -C checks -j$(nproc) $test/PA
```


Running the instruction memory check :
Running the memory checks :

```
sby -f imemcheck.sby
sby -f dmemcheck.sby
```

### Todo:
- Integrate others VexRiscv configurations into the framework
- Add Data Memcheck check
- Add Checking for equivalence of core with and without RVFI check
- Add Complete check
- Add Cover check
ProTip! Use n and p to navigate between commits in a pull request.