350 rub
Journal Science Intensive Technologies №1 for 2017 г.
Article in number:
Approaches to formal verification of model of microprocessor commutation subsystem devices
Keywords: commutation subsystem formal verification model checking cone of influence reduction Kripke structure extended hierarchical automata
Authors:
I.A. Stotland - Ph. D. (Eng.), Associate Professor, Moscow State University of Information Technologies, Radio Engineering and Electronics (MIREA) E-mail: irastot@mail.ru N.A. Starikovskaya - Ph. D. (Eng.), Associate Professor, Moscow State University of Information Technologies, Radio Engineering and Electronics (MIREA) E-mail: starikovskaya@mirea.ru M.A. Kirichenko - Student, Moscow State University of Information Technologies, Radio Engineering and Electronics (MIREA) E-mail: kmar.kmar@mail.ru
Abstract:
The novel approaches to formal verification of commutation subsystem components of microprocessor is proposed in this paper. The approaches are based on formal verification of automata models using model checking. The detailed review of the existing methods of the functional verification is provided: simulation modeling and the formal verification. Methods of a reduction of number of states and its applicability in case of verification of commutation subsystem models are considered. Main requirements to microprocessor commutation subsystem functionality are selected, classified and formalized. The paper includes general description of the approaches, considers several particular cases, and outlines our experience.
Pages: 3-8
References

 

  1. Bergeron J. Writing testbenches: functional verification of HDL models. Kluwer Academic Publishers. 2003. 478 p.
  2. Stotland I.A., Lagutin A.A. Primenenie ehtalonnykh sobytijjnykh modelejj dlja avtonomnojj verifikacii modulejj mikroprocessorov // Voprosy radioehlektroniki. 2014. T. 4. № 3. S. 17−27.
  3. Bentley R.M. Validating the Pentium 4 Microprocessor // Proc. of the Int. Conference on Dependable Systems and Networks. 2001. P. 493−498.
  4. Clarke E., Grumberg O., Peled D. Model Checking. MIT Press. 1999. 314 p.
  5. Karpov JU.G. Model Checking. Verifikacija parallelnykh i raspredelennykh programmnykh sistem. SPb.: BKHV-Peterburg. 2010. 560 s.
  6. Clarke E., Grumberg O., Long O. Model checking and abstraction // ACM Transaction on Programming Languages and Systems. 1994. V. 16. № 5. P. 1512−1542.
  7. Drechsler R. Advanced formal verification. Kluwer Academic Publishers. 2014. 628 p.
  8. Petrochenkov M.V., Stotland I.A. Metodika avtonomnojj verifikacii ustrojjstv podsistemy pamjati mnogojadernykh mikroprocessorov // Voprosy radioehlektroniki. 2016. Ser. EHVT. № 3. S. 42−47.
  9. Kamkin A.C., CHupilko M.M. Mekhanizmy podderzhki funkcionalnogo testirovanija modelejj apparatury na raznykh urovnjakh abstrakcii // Trudy Instituta sistemnogo programmirovanija RAN. 2011. T. 20. S. 143−160.
  10. Stotland I.A. Metod dinamicheskojj verifikacii modulejj sistemnogo obmena mikroprocessornykh vychislitelnykh kompleksov // Nauchno-tekhnich. vestnik Povolzhja. 2012. № 4. S. 191−196.