Randomised testing of a microprocessor model using SMT-solver state generation

Research output: Contribution to journalArticlepeer-review


We validate a HOL4 model of the ARM Cortex-M0 microcontroller core by testing the model's behaviour on randomly chosen instructions against real chips from several manufacturers. 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. We also use additional constraints to test our hypotheses about the timing anomalies encountered.
Original languageEnglish
Pages (from-to)60-76
Number of pages17
JournalScience of Computer Programming
Early online date31 Oct 2015
Publication statusPublished - 1 Mar 2016


  • SMT


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