Randomised Testing of a Microprocessor Model Using SMT-Solver State Generation

Research output: Chapter in Book/Report/Conference proceedingConference contribution

Abstract

We validate a HOL4 model of the ARM Cortex-M0 microcontroller core by testing the model’s behaviour on randomly chosen instructions against a real chip.

The model and our intended application involve precise timing information about instruction execution, but the implementations are pipelined, so checking the behaviour of single instructions would not give us sufficient confidence in the model. Thus we test the model using sequences of randomly chosen instructions.

The main challenge is to meet the constraints on the initial and intermediate execution states: we must ensure that memory accesses are in range and that we respect restrictions on the instructions. By careful transformation of these constraints an off-the-shelf SMT solver can be used to find suitable states for executing test sequences.
Original languageEnglish
Title of host publicationFormal Methods for Industrial Critical Systems
Subtitle of host publication19th International Conference, FMICS 2014, Florence, Italy, September 11-12, 2014. Proceedings
EditorsFrédéric Lang, Francesco Flammini
PublisherSpringer International Publishing
Pages185-199
Number of pages15
ISBN (Electronic)978-3-319-10702-8
ISBN (Print)978-3-319-10701-1
DOIs
Publication statusPublished - 2014

Publication series

NameLecture Notes in Computer Science
PublisherSpringer
Volume8718
ISSN (Print)0302-9743
ISSN (Electronic)1611-3349

Fingerprint Dive into the research topics of 'Randomised Testing of a Microprocessor Model Using SMT-Solver State Generation'. Together they form a unique fingerprint.

Cite this