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

Brian Campbell,Ian Stark

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

2014

Brian Campbell
Ian Stark

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.

Keywords:

Real-time computing
Microcontroller
Computer architecture
Satisfiability modulo theories
Chip
Computer science
Microprocessor
Computer hardware

Correction
Source
Cite
Save
Machine Reading By IdeaReader

References

Citations