From aa510dbb933119bc2e54102eac0d4029813694e0 Mon Sep 17 00:00:00 2001 From: Gerwin Klein Date: Tue, 19 Jun 2018 14:17:32 +0200 Subject: [PATCH] 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. --- spec/machine/RISCV64/MachineOps.thy | 26 +++++++++++++------------- 1 file changed, 13 insertions(+), 13 deletions(-) diff --git a/spec/machine/RISCV64/MachineOps.thy b/spec/machine/RISCV64/MachineOps.thy index 0ec51f9d5..7474e8fe8 100644 --- a/spec/machine/RISCV64/MachineOps.thy +++ b/spec/machine/RISCV64/MachineOps.thy @@ -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 \ machine_op_lift initTimer_impl" +where + "initTimer \ machine_op_lift initTimer_impl" consts' resetTimer_impl :: "unit machine_rest_monad" - definition resetTimer :: "unit machine_monad" -where "resetTimer \ machine_op_lift resetTimer_impl" - -consts' - invalidateTLB_impl :: "unit machine_rest_monad" -definition - invalidateTLB :: "unit machine_monad" -where "invalidateTLB \ machine_op_lift invalidateTLB_impl" - -lemmas cache_machine_op_defs = invalidateTLB_def +where + "resetTimer \ machine_op_lift resetTimer_impl" definition debugPrint :: "unit list \ unit machine_monad" @@ -216,6 +208,12 @@ definition definition "setNextPC \ setRegister NEXTPC" +consts' + initL2Cache_impl :: "unit machine_rest_monad" +definition + initL2Cache :: "unit machine_monad" +where + "initL2Cache \ machine_op_lift initL2Cache_impl" consts' hwASIDFlush_impl :: "machine_word \ unit machine_rest_monad" @@ -231,6 +229,8 @@ definition where "sfence \ machine_op_lift sfence_impl" +lemmas cache_machine_op_defs = sfence_def hwASIDFlush_def + consts' sbadaddr_val :: "machine_state \ machine_word" definition