Title :
Modeling and formal verification of a commercial microcontroller for embedded system applications
Author :
Balakrishnan, S. ; Tahar, Sofihe
Author_Institution :
Dept. of Electr. & Comput. Eng., Concordia Univ., Montreal, Que., Canada
fDate :
6/20/1905 12:00:00 AM
Abstract :
Embedded systems are finding widespread application. A formal model for the underlying hardware (RT level) of the microcontroller (PIC 16C71) in commercial use, along with its Instruction Set Architecture (ISA) using Multiway Decision Graphs (MDG) is proposed. Using the MDG verification tools, we verified if the instructions in the instruction set are implemented correctly in the microcontroller hardware. Models for the flowchart specification and the assembly language implementation of an embedded software, used in a mouse controller application are portrayed. Applying the platform of the ISA verification, the correctness of the embedded software has been verified at a higher level of abstraction. Inconsistencies in the assembly code with respect to the specification, as published in the application notes of the manufacturer, were uncovered through our experiments
Keywords :
directed graphs; embedded systems; flowcharting; formal verification; instruction sets; microcontrollers; PIC 16C71; RTL model; assembly language; embedded system; flowchart; formal verification; instruction set architecture; microcontroller; mouse controller; multiway decision graph; Application software; Assembly; Computer architecture; Embedded software; Embedded system; Flowcharts; Formal verification; Hardware; Instruction sets; Microcontrollers;
Conference_Titel :
Microelectronics, 1998. ICM '98. Proceedings of the Tenth International Conference on
Conference_Location :
Monastir
Print_ISBN :
0-7803-4969-5
DOI :
10.1109/ICM.1998.825580
