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

fYear

1998

fDate

6/20/1905 12:00:00 AM

Firstpage

107

Lastpage

110

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;

fLanguage

English

Publisher

ieee

Conference_Titel

Microelectronics, 1998. ICM '98. Proceedings of the Tenth International Conference on

Conference_Location

Monastir

Print_ISBN

0-7803-4969-5

Type

conf

DOI

10.1109/ICM.1998.825580

Filename

825580