TY - GEN
T1 - Formal Design and Verification of Memory Management Unit Microprocessor
AU - Yang, Hongwei
AU - Ma, Dianfu
N1 - Publisher Copyright:
© 2019 IEEE.
PY - 2019/8
Y1 - 2019/8
N2 - CPU is the core of modern computer system and the foundation of operating system and upper software. Memory management unit (MMU) and cache (Cache) are widely used in modern microprocessor design. They have been improving CPU performance while increasing the difficulties of CPU design and verification. As the structure of today's CPU is more and more complex, conventional design and verification methods such as testing and simulating can't guarantee the correctness of CPU structure designs. In this paper, we present an axiomatic system which could be used to formally describe the CPU structure with MMU and Cache. And we propose a formal method to formally verify an instruction path with MMU and Cache based on this axiom system. Meanwhile we develop an automated verification tool and completed formal verification of 86 MIPS instructions efficiently with the tool.
AB - CPU is the core of modern computer system and the foundation of operating system and upper software. Memory management unit (MMU) and cache (Cache) are widely used in modern microprocessor design. They have been improving CPU performance while increasing the difficulties of CPU design and verification. As the structure of today's CPU is more and more complex, conventional design and verification methods such as testing and simulating can't guarantee the correctness of CPU structure designs. In this paper, we present an axiomatic system which could be used to formally describe the CPU structure with MMU and Cache. And we propose a formal method to formally verify an instruction path with MMU and Cache based on this axiom system. Meanwhile we develop an automated verification tool and completed formal verification of 86 MIPS instructions efficiently with the tool.
KW - CPU structure verification
KW - MMU and Cache verification
KW - automated verification
KW - theorem prooving
UR - https://www.scopus.com/pages/publications/85080023090
U2 - 10.1109/CCET48361.2019.8989215
DO - 10.1109/CCET48361.2019.8989215
M3 - 会议稿件
AN - SCOPUS:85080023090
T3 - 2019 IEEE 2nd International Conference on Computer and Communication Engineering Technology, CCET 2019
SP - 124
EP - 128
BT - 2019 IEEE 2nd International Conference on Computer and Communication Engineering Technology, CCET 2019
PB - Institute of Electrical and Electronics Engineers Inc.
T2 - 2nd IEEE International Conference on Computer and Communication Engineering Technology, CCET 2019
Y2 - 16 August 2019 through 18 August 2019
ER -