VexRiscv imem/dmem checks

cores/VexRiscv/README.md

@@ -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
@@ -12,12 +12,16 @@ All standards checks are passing
 - Causality
 - Liveness
 
+Others tests passing :
+- Instruction Memory check
+- Data Memory check
+
 ### Quickstart guide:
 
 First install Yosys, SymbiYosys, and the solvers. See [here](http://symbiyosys.readthedocs.io/en/latest/quickstart.html#installing)
 for instructions.
 
-To run all checks:
+To run all standards checks:
 
 ```
 python3 ../../checks/genchecks.py
@@ -34,10 +38,16 @@ python3 ../../checks/genchecks.py
 export test=insn_beq_ch0; rm -r checks/$test; make -C checks -j$(nproc) $test/PASS; python3 disasm.py checks/$test/engine_0/trace.vcd
 ```
 
+
+To run imem/dmem checks checks : 
+
+```
+sby -f imemcheck.sby
+sby -f dmemcheck.sby
+```
+
 ### Todo:
 - Integrate others VexRiscv configurations into the framework
-- Add Instruction Memcheck check
-- Add Data Memcheck check
 - Add Checking for equivalence of core with and without RVFI check
 - Add Complete check
 - Add Cover check