Документ взят из кэша поисковой машины. Адрес оригинального документа : http://oit.cmc.msu.ru/lectures/klim-sem.htm
Дата изменения: Wed Oct 22 11:04:58 2003
Дата индексирования: Mon Oct 1 20:35:14 2012
Кодировка: Windows-1251
Аннотация

Аннотация:
Основы моделирования и формальной верификации схем из
функциональных элементов.
1. Методы задания СФЭ
 1) Уровни детализации и их соответствие этапам разработки
 2) Специальные языки
 - Verilog
 2. Моделирование СФЭ
1) Моделирование СФЭ, заданных на специальных языках
- Потактовое моделирование
- Событийное моделирование2) Программное моделирование, уровни детализации
 - Моделирование системы команд
 - Потактовое моделирование
- Моделирование машины
 3. Формальная верификация СФЭ
 1) Математический аппарат, лежащий в основе ФВ
 - Натуральный вывод
 - Темпоральные логики
2) "Машинное" доказательство теорем
3) Символьное моделирование
4) Оценка траекторий символов

 Рекомендуемая литература:
 1. С. В. Яблонский. Введение в дискретную математику.
2. Formal Verification Surveys.
 http://www.cerc.utexas.edu/~jay/fv_surveys/
 3. R. Drechsler and B. Becker. Overview of decision diagrams. In IEE Procs. on Computers and Digital Techniques, volume 144, pages 187-193, May  1997.
4. Daniel C Hyde. Handbook on Verilog HDL. Computer Science Department,
 Bucknell University, Lewisburg, PA 17837, 1997.
5. Bob Bentley and Rand Gray. Validating the Intel Pentium 4 processor.