Radiotekhnika
Publishing house Radiotekhnika

"Publishing house Radiotekhnika":
scientific and technical literature.
Books and journals of publishing houses: IPRZHR, RS-PRESS, SCIENCE-PRESS


Тел.: +7 (495) 625-9241

 

Approaches to formal verification of model of microprocessor commutation subsystem devices

Keywords:

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


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.
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.

 

© Издательство «РАДИОТЕХНИКА», 2004-2017            Тел.: (495) 625-9241                   Designed by [SWAP]Studio