Цена доставки диссертации от 500 рублей 
Поиск:

Каталог / ТЕХНИЧЕСКИЕ НАУКИ

Формальная верификация процессора с устройствами поддержки виртуальной памяти

Диссертация

Автор: Далингер, Яков

Заглавие: Формальная верификация процессора с устройствами поддержки виртуальной памяти

Справка об оригинале: Далингер, Яков. Формальная верификация процессора с устройствами поддержки виртуальной памяти : диссертация ... кандидата технических наук : 05.00.00 / Далингер Яков; [Место защиты: Ун-т Саарланда] - Саарбрюккен, 2006 - Количество страниц: 152 с. ил. Саарбрюккен, 2006 152 c. :

Физическое описание: 152 стр.

Выходные данные: Саарбрюккен, 2006




Стоимость Доставки
500 руб.


Содержание:

1 Введение
11 Используемые обозначения
12 Среда формальных доказательств PVS
13 Базовые логические элементы
14 Виртуальная память
15 Декомпозиция доказательства
151 Уровень интерфейса памяти
152 Уровень интерфейса процессора
2 Блок поддержки виртуальной памяти
21 Спецификация MMU
211 Допущение для MMU
212 Гарантии MMU
22 Дизайн MMU
23 Корректность MMU
3 VAMP с поддержкой виртуальной памяти
31 Спецификация VAMP процессора
32 Имплементация процессора VAMP
321 Алгоритм Томасуло
322 Дизайн процессора VAMP
323 Имплементация блока памяти процессора VAMP
33 Критерий корректности
331 Планировочные функции
332 Инвариант корректности
333 Обзор доказательства
34 Корректность между прерываниями
341 Корректность блока памяти при чтении / записи
342 Выборка инструкций
35 Корректность с прерываниями
351 Полная корректность

Введение:
На текущий момент, существует много приложений где процессора используются в устройствах, критичных для жизни человека, например атомные электрические станции, самолеты, поезда, автомобили или медицинские приборы. Разработчики процессоров используют различные тесты для того чтобы обнаружить ошибки в них. Так как не исчерпывающие тесты пе покрывают все возможные случаи поведения процессора, процессора выпускаемые индустрией могут содержать ошибки. Формальная верификация все больше и больше признается единственной альтернативой, так как актуальные результаты в формальной верификации эквивалентны симуляции всех возможных случаев поведения процессора. Более того, это даже лучше чем симуляция потому, что можно получить корректность нескольких модулей сразу.В данной работе доказывается только корректность работы аппаратного обеспечения используемого в академической системе проекта Verisoft. Следует отметить, что ошибки программного обеспечения также могут быть причиной неправильного поведения системы. Поэтому, как доказательство корректности работы апнаратного уровня, так и доказательство корректности программного обеспечения необходимы, а доказательство корректности работы аппаратного уровня это только первый шаг на пути получения корректности полной компьютерной системы.К р а т к о е с о д е р ж а н и е глав В главе 1 рассматривается основная нотация, используемая во всей работе. Так же будут рассмотрены: система формальных доказательств, виртуальная память и основной подход к декомпозиции доказательств в данной работе.В главе 2 рассматривается конструкция неоптимизированного блока поддержки виртуальной памяти (ММи), который является аппаратной частью поддержки виртуальной памяти. Здесь же будет доказана корректность работы данного блока при нетривиальных условиях: данные в ячейках памяти И используемые для транслирования адреса не должны быть перезаписаны в течении всего запроса к MMU.В последней главе 4 обобпдаются результаты, проводится дискуссия о достоинствах и недостатках разработанной системы, представляется информация о работах других ученый в данном направлении, а также обсуждаются возможности для дальнейшей работы.
Список литературы:

1. BCBZ02. S. Berezin, E. Clarke, A. Biere, and Y. Zhu. Verification of out-of-order processor designs using model checking and a lightweight completion function. In Formal Methods in System Design, volume 20, 2002.
2. BD94. J. R. Burch and D. L. Dill. Automatic verification of pipelined microprocessors control. In CAV 94, volume 818, pages 68-80. Springer-Verlag, 1994.
3. BerOl. Christoph Berg. Formal verification of an IEEE floating point adder.
4. Master's thesis, Saarland University, Saarbr?cken, Germany, May 2001.
5. Bey05. Sven Beyer. Putting it all together—Formal Verification of the VAMP. PhD thesis, Saarland University, Saarbr?cken, Germany, 2005.
6. BHK94. B. Brock, W. A. Hunt, and M. Kaufmann. The FM9001 microprocessor proof. Technical Report 86, Computational Logic Inc., 1994.
7. BJ01. Christoph Berg and Christian Jacobi. Formal verification of the VAMP floating point unit. In CHARME 2001, volume 2144 of LNCS, pages 325-339. Springer, 2001.
8. BJK01. Christoph Berg, Christian Jacobi, and Daniel Kr?ning. Formal verification of a basic circuits library. In Proc. 19th IASTED International Conference on Applied Informatics, Innsbruck (AF2001), pages 252-255. ACTA Press, 2001.
9. Bog05. Sebastian Bogan. Formal Verification of a Simple Operating System (Draft). PhD thesis, Saarland University, Saarbr?cken, Germany, 2005.
10. DHP05. I. Dalinger, M. Hillebrand, and W. Paul. On the verification of memory management mechanisms. In D. Borrione and W. Paul, editors, CHARME 2005, LNCS. Springer, 2005.
11. GHLP05. M. Gargano, M. Hillebrand, D. Leinenbach, and W. Paul. On the correctness of operating system kernels. In J. Hurd and T. Melham, editors, TPHOLs 2005 (to appear), LNCS. Springer, 2005.
12. Hil05. Mark Hillebrand. Address Spaces and Virtual Memory: Specification, Implementation, and Correctnesss. PhD thesis, Saarland University, Saarbr?cken, Germany, 2005.
13. HIP05. Mark Hillebrand, Thomas In der Rieden, and Wolfgang Paul.
14. Dealing with I/O devices in the context of pervasive system verification. In I CCD '05. IEEE Computer Society, 2005. To appear.
15. HP96a. J. L. Hennessy and D. A. Patterson. Computer Architecture: A Quantitative Approach. Morgan Kaufmann, San Mateo, CA, second edition, 1996.
16. HP96b. John L. Hennessy and David A. Patterson. Computer Architecture: A Quantitative Approach. Morgan Kaufmann Publishers, INC., San Mateo, CA, 2nd edition, 1996.
17. HS99. W. A. Hunt and J. Sawada,. Verifying the FM9801 microarchitecture. In IEEE Micro, pages 47-55, 1999.
18. HSG99. Ravi Hosabettu, Mandayam Srivas, and Ganesh Gopalakrishnan.
19. Proof of correctness of a processor with reorder buffer using the completion functions approach. In Computer-Aided Verification, CAV '99, volume 1633, pages 47-59. Springer-Verlag, 1999.
20. E85. Institute of Electrical and Electronics Engineers. ANSI/IEEE standard 75^-1985, IEEE Standard for Binary Floating-Point Arithmetic, 1985.
21. Jac02a. Christian Jacobi. Formal Verification of a fully IEEE-compliant Floating-Point Unit. PhD thesis, Saarland University, Saarbr?cken, Germany, 2002.
22. JK00. Christian Jacobi and Daniel Kr?ning. Proving the correctness of a complete microprocessor. In Proc. of the 30. Jahrestagung der Gesellschaft four Informatik. Springer, 2000.
23. JM98. Bruce Jacob and Trevor Mudge. Virtual memory in contemporary microprocessors. IEEE Micro, 18(4):60—75, 1998.
24. JWPB05. C. Jacobi, K. Weber, V. Paruthi, and J. Baumgartner. Automatic Formal Verification of Fused-Multiply-Add FPUs. In DATE, pages 1298-1303, 2005.
25. McM98. K. McMillan. Verification of an implementation of Tomasulo's algorithm by compositional model checking. In CA V 98, volume 1427. Springer, June 1998.
26. MP00. Silvia M. M?ller and Wolfgang J. Paul. Computer Architecture: Complexity and Correctness. Springer, 2000.
27. MS05. Panagiotis Manolios and Sudarshan K. Srinivasan. A parameterized benchmark suite of hard pipelined-machine-verification problems. In CHARME 2005, volume 3725 of LNCS, pages 363-366. Springer, 2005.
28. OSR92. S. Owre, N. Shankar, and J. M. Rushby. PVS: A prototype verification system. In CADE 11, volume 607 of LNAI, pages 748752. Springer, 1992.
29. Pet04. Elena Petrova. Formal Verification of Compilers on the Source Code Level (Draft). PhD thesis, Saarland University, Saarbr?cken, Germany, 2004.
30. SH98. J. Sawada and W. A. Hunt. Processor verification with precise exceptions and speculative execution. In CAV 98, volume 1427 of LNCS. Springer, 1998.
31. SP88. James E. Smith and Andrew R. Pleszkun. Implementing precise interrupts in pipelined processors. In IEEE Transactions on Computers, volume C-37, pages 562-573. 1988.
32. Tom67. R. M. Tomasulo. An efficient algorithm for exploiting multiple arithmetic units. In IBM Journal of Research & Development, volume 11 (1), pages 25-33. IBM, 1967.
33. Tve05a. Sergey Tverdyshev. Combination of Isabelle/HOL with automatic tools. In 5th International Workshop on Frontiers of Combining Systems (FroCoS)(to appear), Lecture Notes in Artificial Intelligence. Springer, 2005.
34. Tve05b. Sergey Tverdyshev. Formal Verification of the VAMP processor by using automated methods (Draft). PhD thesis, Saarland University, Saarbr?cken, Germany, 2005.
35. VB99. M. Velev and R. Bryant. Superscalar processor verification using efficient reductions of the logic of equality with uninterpreted functions to propositional logic. In L. Pierre and T. Kropf, editors, CHARME 1999, LNCS. Springer, 1999.
36. VB00. Miroslav N. Velev and Randal E. Bryant. Formal verification of superscale microprocessors with multicycle functional units, exception, and branch prediction. In DAC. ACM, 2000.
37. Ver03. The Verisoft Project, http://www.verisoft.de/, 2003.