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

aarch64 design: make vcpuBits available through MachineTypes 

Signed-off-by: Rafal Kolanski <rafal.kolanski@proofcraft.systems>
This commit is contained in:
Rafal Kolanski 2022-03-17 00:12:39 +11:00 committed by Gerwin Klein
parent f86a3944ba
commit 15dc7d2959
2 changed files with 3 additions and 2 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

3
spec/design/m-skel/AARCH64/MachineTypes.thy
View File

@ -115,7 +115,8 @@ definition
#INCLUDE_HASKELL SEL4/Machine/Hardware/AARCH64.hs CONTEXT AARCH64 ONLY \
VMFaultType HypFaultType vmFaultTypeFSR VMPageSize pageBits ptTranslationBits \
pageBitsForSize \
hcrVCPU hcrNative vgicHCREN sctlrDefault sctlrEL1VM actlrDefault gicVCPUMaxNumLR
hcrVCPU hcrNative vgicHCREN sctlrDefault sctlrEL1VM actlrDefault gicVCPUMaxNumLR \
vcpuBits
end

2
spec/design/skel/AARCH64/Hardware_H.thy
View File

@ -37,7 +37,7 @@ context Arch begin global_naming AARCH64_H
enableFpuEL01 \
getFAR getDFSR getIFSR getHSR setHCR getESR getSCTLR setSCTLR \
addressTranslateS1 \
readVCPUHardwareReg writeVCPUHardwareReg
readVCPUHardwareReg writeVCPUHardwareReg vcpuBits
end