adbrucker
/
lh-l4v
1
0
Fork 0
Code Issues Pull Requests Packages Projects Releases Wiki Activity

riscv design: sFence and readSBADAddr -> sfence and read_sbadaddr

This commit is contained in:
Rafal Kolanski 2018-06-19 12:23:06 +10:00 committed by Gerwin Klein
parent 53774a7a47
commit 39b8b1cb28
1 changed files with 6 additions and 6 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

12
spec/machine/RISCV64/MachineOps.thy
View File

@ -225,18 +225,18 @@ where
"hwASIDFlush asid \<equiv> machine_op_lift (hwASIDFlush_impl asid)"
consts'
sFence_impl :: "unit machine_rest_monad"
sfence_impl :: "unit machine_rest_monad"
definition
sFence :: "unit machine_monad"
sfence :: "unit machine_monad"
where
"sFence \<equiv> machine_op_lift sFence_impl"
"sfence \<equiv> machine_op_lift sfence_impl"
consts'
sBadAddr_val :: "machine_state \<Rightarrow> machine_word"
sbadaddr_val :: "machine_state \<Rightarrow> machine_word"
definition
readSBADAddr :: "machine_word machine_monad"
readsbadaddr :: "machine_word machine_monad"
where
"readSBADAddr = gets sBadAddr_val"
"readsbadaddr = gets sbadaddr_val"
end