| 1.обратно | Statistical Analysis of Floating Point Flaw in the Pentium Processor. Intel Corporation, November 1994. |
| 2.обратно | B. Beizer. The Pentium Bug - An Industry Watershed. Testing Techniques Newsletter (TTN), TTN Online Edition, September 1995. |
| 3.обратно | А. Wolfe. For Intel, It's a Case of FPU All Over Again. EE Times, May 1997. |
| 4.обратно | B. Meyer. Design by Contract. Technical Report TR-EI-12/CO, Interactive Software Engineering Inc., 1986. |
| 5.обратно | B. Meyer. Applying `Design by Contract'. IEEE Computer, vol. 25, No. 10, October 1992. |
| 6.обратно | |
| 7.обратно | IEEE Standard VHDL Language Reference Manual. IEEE Std 1076-1987. |
| 8.обратно | IEEE Standard Hardware Description Language Based on the Verilog Hardware Description Language. IEEE Std 1364-1995. |
| 9.обратно | |
| 10.обратно | |
| 11.обратно | |
| 12.обратно | |
| 13.обратно | I. Bourdonov, A. Kossatchev, V. Kuliamin, and A. Petrenko. UniTesK Test Suite Architecture. FME'2002. LNCS 2391, Springer-Verlag, 2002. |
| 14.обратно | |
| 15.обратно | A. Kamkin. The UniTESK Approach to Specification-Based Validation of Hardware Designs. IEEE-ISoLA'2006: The 2nd International Symposium on Leveraging Applications of Formal Methods, Verification and Validation, November 2006. |
| 16.обратно | |
| 17.обратно | S.A. Edwards. Design and Verification Languages. Technical Report, Columbia University, New York, USA, November 2004. |
| 18.обратно | R. Armoni, L. Fix, A. Flaisher, R. Gerth, B. Ginsburg, T. Kanza, A. Landver, S. Mador-Haim, E. Singerman, A. Tiemeyer, M. Vardi, and Y. Zbar. The ForSpec Temporal Logic: A New Temporal Property-Specification Language. Tools and Algorithms for Construction and Analysis of Systems, 2002. |
| 19.обратно | I. Beer, S. Ben-David, C. Eisner, D. Fisman, A. Gringauze, and Y. Rodeh. The Temporal Logic Sugar. Lecture Notes in Computer Science, 2001. |
| 20.обратно | |
| 21.обратно | OpenVera® Language Reference Manual: Assertions. Version 1.4.1, November 2004. |
| 22.обратно | |
| 23.обратно | |
| 24.обратно | MIPS64™ Architecture For Programmers. Revision 2.0. MIPS Tecnologies Inc., June 9, 2003. |
| 1(к тексту) | Pentium - торговая марка нескольких поколений микропроцессоров семейства x86, выпускаемых компанией Intel с 22 марта 1993 года. |
| 2(к тексту) | Именно такие модели являются предметом исследования настоящей работы. |
| 3(к тексту) | Число транзисторов в современных микросхемах достигает сотней миллионов. Согласно закону Мура (Moore) это число возрастает примерно вдвое через каждые 18-24 месяцев. |
| 4(к тексту) | Мы не рассматриваем здесь разного рода неопределенные значения, часто используемые в моделировании аппаратного обеспечения. |
| 5(к тексту) | В дальнейшем будем называть такие процессы модельными процессами, чтобы отличать их от процессов операционной системы. |
| 6(к тексту) | В начале симуляции активными являются процессы, осуществляющие инициализацию. |
| 7(к тексту) | Для наглядности мы не вводим модель данных и не уточняем сигнатуры пред- и постусловий. |
| 8(к тексту) | Исключение составляет обходчик ndfsm [], позволяющий обходить графы состояний для некоторого класса недетерминированных конечных автоматов. |
| 9(к тексту) | Вариант логики LTL, используемой в ForSpec, называется FTL (ForSpec temporal logic) []. |
| 10(к тексту) | При подсчете числа входов и выходов не учитывался интерфейс JTAG (joint test action group) - стандартный интерфейс, используемый для тестирования аппаратуры с помощью метода граничного сканирования. |
