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

trivial: restyle `spec/machine/ARM*/Platform.thy` 

Signed-off-by: Matthew Brecknell <Matthew.Brecknell@data61.csiro.au>
This commit is contained in:
Matthew Brecknell 2021-06-24 18:23:18 +10:00 committed by Matthew Brecknell
parent 8dd93a52a0
commit 2aadbf9589
2 changed files with 26 additions and 48 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

30
spec/machine/ARM/Platform.thy
View File

@ -29,45 +29,35 @@ type_synonym paddr = word32
abbreviation (input) "toPAddr \<equiv> id"
abbreviation (input) "fromPAddr \<equiv> id"
definition
pageColourBits :: nat where
definition pageColourBits :: nat where
"pageColourBits \<equiv> 2"
definition
cacheLineBits :: nat where
definition cacheLineBits :: nat where
"cacheLineBits = 5"
definition
cacheLine :: nat where
definition cacheLine :: nat where
"cacheLine = 2^cacheLineBits"
(* Arch specific kernel base address used for haskell spec *)
definition
pptrBase :: word32 where
definition pptrBase :: word32 where
"pptrBase \<equiv> 0xe0000000"
definition
physBase :: word32 where
definition physBase :: word32 where
"physBase \<equiv> 0x10000000"
definition
pptrBaseOffset :: word32 where
definition pptrBaseOffset :: word32 where
"pptrBaseOffset \<equiv> pptrBase - physBase"
definition
ptrFromPAddr :: "paddr \<Rightarrow> word32" where
definition ptrFromPAddr :: "paddr \<Rightarrow> word32" where
"ptrFromPAddr paddr \<equiv> paddr + pptrBaseOffset"
definition
addrFromPPtr :: "word32 \<Rightarrow> paddr" where
definition addrFromPPtr :: "word32 \<Rightarrow> paddr" where
"addrFromPPtr pptr \<equiv> pptr - pptrBaseOffset"
definition
minIRQ :: "irq" where
definition minIRQ :: "irq" where
"minIRQ \<equiv> 0"
definition
maxIRQ :: "irq" where
definition maxIRQ :: "irq" where
"maxIRQ \<equiv> 0x9F"
end

44
spec/machine/ARM_HYP/Platform.thy
View File

@ -29,62 +29,50 @@ type_synonym paddr = word32
abbreviation (input) "toPAddr \<equiv> id"
abbreviation (input) "fromPAddr \<equiv> id"
definition
pageColourBits :: nat where
definition pageColourBits :: nat where
"pageColourBits \<equiv> 2"
definition
cacheLineBits :: nat where
definition cacheLineBits :: nat where
"cacheLineBits = 6"
definition
cacheLine :: nat where
definition cacheLine :: nat where
"cacheLine = 2^cacheLineBits"
(* Arch specific kernel base address used for haskell spec *)
definition
pptrBase :: word32 where
definition pptrBase :: word32 where
"pptrBase \<equiv> 0xe0000000"
definition
physBase :: word32 where
definition physBase :: word32 where
"physBase \<equiv> 0x80000000"
abbreviation (input) "paddrBase \<equiv> physBase"
definition
pptrTop :: "32 word" where
definition pptrTop :: "32 word" where
"pptrTop \<equiv> 0xfff00000"
definition
paddrTop :: "32 word" where
definition paddrTop :: "32 word" where
"paddrTop \<equiv> pptrTop - (pptrBase - physBase)"
definition
pptrBaseOffset :: word32 where
definition pptrBaseOffset :: word32 where
"pptrBaseOffset \<equiv> pptrBase - physBase"
definition
ptrFromPAddr :: "paddr \<Rightarrow> word32" where
definition ptrFromPAddr :: "paddr \<Rightarrow> word32" where
"ptrFromPAddr paddr \<equiv> paddr + pptrBaseOffset"
definition
addrFromPPtr :: "word32 \<Rightarrow> paddr" where
definition addrFromPPtr :: "word32 \<Rightarrow> paddr" where
"addrFromPPtr pptr \<equiv> pptr - pptrBaseOffset"
definition
minIRQ :: "irq" where
definition minIRQ :: "irq" where
"minIRQ \<equiv> 0"
definition
maxIRQ :: "irq" where
definition maxIRQ :: "irq" where
"maxIRQ \<equiv> 191"
definition irqVGICMaintenance :: "irq"
where "irqVGICMaintenance \<equiv> 25"
definition irqVGICMaintenance :: "irq" where
"irqVGICMaintenance \<equiv> 25"
definition irqVTimerEvent :: "irq"
where "irqVTimerEvent \<equiv> 27"
definition irqVTimerEvent :: "irq" where
"irqVTimerEvent \<equiv> 27"
end