#
5529fcdf |
|
29-Jan-2016 |
Anthony Fox <anthony.fox@cl.cam.ac.uk> |
Update the RISC-V model and add decompilation support. The model itself supports multiple cores (with a shared memory) and the state assertions reflect this, e.g. riscv_c_gpr core reg value riscv_MEM8 address value However, for decompilation we fix on core 0, i.e. we use riscv_REG reg value . The model also supports virtual memory, but we assume that this is turned off when generating step and spec theorems.
|