کد مقاله کد نشریه سال انتشار مقاله انگلیسی نسخه تمام متن
434884 1441631 2016 17 صفحه PDF دانلود رایگان
عنوان انگلیسی مقاله ISI
Randomised testing of a microprocessor model using SMT-solver state generation
کلمات کلیدی
موضوعات مرتبط
مهندسی و علوم پایه مهندسی کامپیوتر نظریه محاسباتی و ریاضیات
پیش نمایش صفحه اول مقاله
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.

ناشر
Database: Elsevier - ScienceDirect (ساینس دایرکت)
Journal: Science of Computer Programming - Volume 118, 1 March 2016, Pages 60–76
نویسندگان
, ,