Sciweavers

Share
SCP
2016

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

4 years 3 months ago
Randomised testing of a microprocessor model using SMT-solver state generation
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.
Brian Campbell, Ian Stark
Added 09 Apr 2016
Updated 09 Apr 2016
Type Journal
Year 2016
Where SCP
Authors Brian Campbell, Ian Stark
Comments (0)
books