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

riscv machine: add remaining machine interface 

These are unused in RISCV64 at the moment, but referred to
in generic code, and will likely need to be filled in for
real hardware later.
This commit is contained in:
Gerwin Klein 2018-06-19 14:17:32 +02:00
parent 52486ccd79
commit aa510dbb93
1 changed files with 13 additions and 13 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

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

@ -81,27 +81,19 @@ where
gets configureTimer_val
od"
consts' (* XXX: replaces configureTimer in new boot code
TODO: remove configureTimer when haskell updated *)
consts'
initTimer_impl :: "unit machine_rest_monad"
definition
initTimer :: "unit machine_monad"
where "initTimer \<equiv> machine_op_lift initTimer_impl"
where
"initTimer \<equiv> machine_op_lift initTimer_impl"
consts'
resetTimer_impl :: "unit machine_rest_monad"
definition
resetTimer :: "unit machine_monad"
where "resetTimer \<equiv> machine_op_lift resetTimer_impl"
consts'
invalidateTLB_impl :: "unit machine_rest_monad"
definition
invalidateTLB :: "unit machine_monad"
where "invalidateTLB \<equiv> machine_op_lift invalidateTLB_impl"
lemmas cache_machine_op_defs = invalidateTLB_def
where
"resetTimer \<equiv> machine_op_lift resetTimer_impl"
definition
debugPrint :: "unit list \<Rightarrow> unit machine_monad"
@ -216,6 +208,12 @@ definition
definition
"setNextPC \<equiv> setRegister NEXTPC"
consts'
initL2Cache_impl :: "unit machine_rest_monad"
definition
initL2Cache :: "unit machine_monad"
where
"initL2Cache \<equiv> machine_op_lift initL2Cache_impl"
consts'
hwASIDFlush_impl :: "machine_word \<Rightarrow> unit machine_rest_monad"
@ -231,6 +229,8 @@ definition
where
"sfence \<equiv> machine_op_lift sfence_impl"
lemmas cache_machine_op_defs = sfence_def hwASIDFlush_def
consts'
sbadaddr_val :: "machine_state \<Rightarrow> machine_word"
definition