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

• We test a formal microprocessor model using randomly chosen instruction sequences.
• SMT constraint solving provides processor and memory states for fault-free execution.
• Successfully tested against several chips and identified minor timing anomalies.
• Checked hypotheses for timing anomalies by supplying additional constraints.

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.