Formally Verified Isolation of DMA
Published in Formal Methods in Computer-Aided Design, 2022
This paper describes a generic formal model in HOL of the common characteristics of DMA controllers. This generic model can be instantiated to describe the operational behavior of a specific DMA controller. It is formally verified under which conditions such DMA controllers are isolated.