Автоматизация проектирования симуляторов микропроцессоров и микроконтроллеров тема диссертации и автореферата по ВАК РФ 05.13.12, кандидат технических наук Негода, Дмитрий Викторович

• Негода, Дмитрий Викторович
• кандидат технических наук
• 2005

Оглавление диссертации кандидат технических наук Негода, Дмитрий Викторович

Введение.

1. Анализ технологий проектирования симуляторов.

1.1. Модели микропроцессоров.

1.2. Классификация симуляторов.

1.3. Базовые технологии проектирования симуляторов.

1.4. Оптимизация симуляторов по быстродействию.

1.5. Выводы по первой главе.

2. Исследование методов оптимизации симуляторов по быстродействию

2.1. Методы анализа и трансформаций программ.

2.1.1. Алгебра языков программирования.

2.1.2. Синтаксис и семантика языка While++.

2.1.3. Реляционная хоаровская логика.

2.2. Таблично-алгоритмическая оптимизация.

2.2.1. Функциональная модель.

2.2.2. Эксперимент.

2.2.3.Решение в общем случае.

2.2.4. Частичная реализация ветвей симулятора.

2.2.5. Поразрядная двоичная арифметика.

2.2.6. Решение систем уравнений и неравенств в поразрядной двоичной арифметике.

2.2.7. Эквивалентность выражений.

2.2.8. Процедура таблично-алгоритмической оптимизации.

2.3. Отложенное вычисление флагов.

2.3.1. Функциональная модель.

2.3.2. Эксперимент.

2.3.3. Автоматизация оптимизирующего преобразования.

2.4. Выводы по второй главе.

3. Автоматизация тестирования симуляторов.

3.1. Автоматизация тестирования программ.

3.2. Существующие методы тестирования симуляторов.

3.3. Метод тестирования симуляторов на основе генерации тестов и использования прототипа.

3.4. Выводы по третьей главе.

4. Автоматизация проектирования симуляторов микроконтроллеров и интеграция моделей микропроцессорных устройств в систему.

4.1. Структура МПС.

4.2. Взаимодействие компонентов МПС.

4.3. Маршрутизатор сообщений.

4.4. Планирование и дельта-задержка.

4.5. Дизассемблер.

4.6. Визуальная среда симуляции МПС.

4.7. Симулятор микропроцессора 18086. Создание новых симуляторов и моделей.

4.8. Выводы по четвертой главе.

Введение диссертации (часть автореферата) на тему «Автоматизация проектирования симуляторов микропроцессоров и микроконтроллеров»

Актуальность проблемы. Качество оценочного моделирования микропроцессорных систем на ранних этапах их проектирования существенным образом зависит от быстродействия и адекватности применяемых симулято-ров микропроцессоров (МП) и микроконтроллеров (МК). В инженерной практике проектирования симуляторов используются два подхода к повышению их быстродействия. Первый подход базируется на максимально возможном использовании оптимизаторов применяемых систем программирования. Второй подход заключается в предметно-ориентированной оптимизации создаваемых программных моделей МП и МК. Именно этот подход позволяет достигать наибольший прирост производительности. Осуществление этого подхода в практике инженерного проектирования симуляторов связано с очень большими трудозатратами, которые можно избежать, применяя механизмы автоматической генерации программных моделей МП и МК из формальных спецификаций или менее быстродействующих моделей.

Адекватность симуляторов обеспечивается процессом тестирования исходной спецификации или исходного симулятора. По мнению В.В.Липаева процесс тестирования программ занимает до 30-40% суммарных трудозатрат на их разработку. В этой связи особо актуальной является автоматизация верификации спецификаций.

К сожалению, на рынке программного обеспечения отсутствуют средства предметно-ориентированной оптимизации симуляторов и автоматизации их тестирования. Более того, основы теории оптимизации и автоматизации тестирования симуляторов развиты очень слабо. В отношении задачи создания интегрированных средств, в центре которых находится симулятор-отладчик, дело обстоит несколько лучше. Здесь имеются достаточно развитые мультиплатформенные симуляторы, характеризующиеся достаточно высокой степенью повторности использования кода в части реализации функций интеграции. Однако, доступны только конечные реализации проектных решений таких сред, но не модели, на базе которых эти решения построены.

Исследования должны охватывать достаточно представительный круг вопросов.

Во-первых, необходимо проанализировать существующую практику автоматической генерации симуляторов и соответствующие формальные модели.

Во-вторых, поскольку предметно-ориентированная оптимизация заключается в преобразовании исходных кодов симуляторов, то необходимо исследовать методы и средства такой трансформации программ симуляции, при которой достигается заметное повышение быстродействия.

В-третьих, включение программ автоматической генерации в систему автоматизации проектирования симуляторов переносит центр приложения основных усилий разработчика в сферу формирования входных спецификаций, что порождает задачу исследования методов и средств верификации этих спецификаций.

В-четвертых, инженерные САПР микропроцессорных систем обычно интегрируют симуляторы МП и МК с другими средствами автоматизации проектирования - кросс-компиляторами, трассировщиками, профилировщиками, моделями внешней среды и т.п. Необходимость создания средств интеграции программ различных производителей, порождает задачу исследования методов повышения повторности использования кода управляющих оболочек САПР МПС.

Область исследования - автоматизация проектирования микропроцессорных систем.

Объект исследования - симуляторы микропроцессоров и микроконтроллеров.

Предмет исследования диссертации — методы и средства автоматизации проектирования симуляторов микропроцессоров и микроконтроллеров.

Целью диссертационной работы является разработка методов и средств автоматизации проектирования. симуляторов, обладающих высоким быстродействием.

Задачи диссертационной работы. Для достижения этой цели необходимо решить следующие основные задачи:

1. Исследование формальных моделей МП и МК, методов и средств построения и тестирования их симуляторов, анализ технологий автоматической генерации.

2. Разработка и исследование методов оптимизирующих преобразований, нацеленных на повышение быстродействие симуляторов.

3. Разработка и исследование методов автоматической генерации тестов машинных команд.

4. Проведение объектно-ориентированного анализа задачи интеграции симуляторов МП и МК в САПР МПС, разработка архитектурного каркаса САПР МПС, центральным компонентами которого являются программные модели средств микропроцессорной техники.

Методы исследования. Для решения поставленных задач использовались формальные методы анализа и преобразования программ, основанных на алгоритмических алгебрах, анализе потоков данных, реляционной хоаров-ской логике, системах перезаписи термов.

Научная новизна проведенных исследований заключается в следующем:

1. Предложенные в работе расширения языка While позволяют моделировать свойства таких широко распространенных языков как Си и Java. Тем самым создается более конструктивная основа для осуществления оптимизирующих преобразований программных моделей МП и МК.

2. Разработанный метод преобразования программ на промежуточном языке While++, в отличие от известных в теории компиляции методов оптимизирующих преобразований программ, работающих над графами потоков управления, позволяет получать продукт оптимизации на исходном языке программирования. Расширена реляционная хоаровская логика на язык While++, что позволяет доказывать корректность преобразований.

3. Разработанные методы оптимизации отличаются от известных тем, что используют в качестве входных данных исходный текст симулятора. Это позволяет сократить затраты труда на создание быстродействующих симуляторов за счет использования доступных исходных кодов программных моделей и развитых инструментальных средств проектирования программ.

4. Разработанный метод таблично-алгоритмической оптимизации позволяет повышать производительность симулятора практически без затрат времени разработчика (на 40% в проведенных экспериментах).

5. Разработанный метод оптимизации «отложенное вычисление флагов» позволяет повышать производительность симулятора практически без затрат времени разработчика (на 4-18% в проведенных экспериментах).

6. Метод тестирования симуляторов, разработанный в диссертации, отличается от известных тем, что использует исходный код симулятора для генерации тестов машинных команд, которые затем выполняются на существующих интерпретаторах машинных команд - либо реальных микропроцессорах, либо заведомо правильных симуляторах. Благодаря этому трудозатраты на тестирование симуляторов сокращаются примерно в 3-4 раза.

Практическая ценность. Практическую ценность представляют следующие результаты осуществления разрабатываемых и развиваемых в диссертации методов и средств: а) симулятор микропроцессора 18086, б) архитектурный каркас САПР МПС, в) экспериментальная программа выполнения оптимизирующих преобразований г) программа анализа потока данных в программе.

Достоверность и эффективность. Достоверность полученных в диссертации результатов подтверждается теоретическими доказательствами, вычислительными экспериментами и результатами экспериментальных разработок.

Внедрение результатов. Результаты внедрены в учебный процесс Ул-ГТУ и в ООО «Креативная разработка».

Основные положения, выносимые на защиту:

1. Абстрактный язык программирования While++, включающий операции общеизвестного языка While, операции с побочным эффектом (такие как ++, += и т.п.), вызовы функций и процедур, неструктурные операторы (return и многоуровневый break), адресную арифметику и массивы; формальная спецификация синтаксиса и денотационной семантики этого языка. Предложенный язык обладает достаточной строгостью для того, чтобы использоваться в формальных методах анализа и преобразования программ, с одной стороны, и достаточной полнотой для моделирования реальных языков программирования, с другой.

2. Расширение реляционной хоаровской логики, используемой для спецификации и доказательства корректности анализа и преобразований императивных программ, на случай языка While++.

3. Поразрядная двоичная арифметика, позволяющая анализировать поток данных в логике принятия решений в разборе машинных инструкций и получать оценки вида х and a = b, где and - поразрядное И, а и b -константы. Логика позволяет получать: а) оценки результата выполнения операций из оценок операндов (прямой DFA); б) уточненные оценки операндов на основе исходных оценок операндов и оценки результата операции (обратный DFA). Правила этой логики позволяют получать локальные решения систем уравнений и неравенств, используемых при анализе алгоритмов декодирования машинной инструкции.

4. Процедура таблично-алгоритмического оптимизирующего преобразования, основанная на перезаписи термов, упрощениях целочисленных арифметических формул и поразрядной двоичной арифметике. Корректность преобразований доказывается с позиций реляционной хоаровской логики.

5. Оптимизирующее преобразование, основанное на отложенном вычислении флагов целевой архитектуры.

6. Метод тестирования симуляторов, который заключается в: а) автоматической генерации самотестирующейся программы из исходного кода разрабатываемого симулятора согласно некоторой метрике покрытия, б) прогоне самотестирующихся программ на реальном физическом микропроцессоре или на заведомо корректном симуляторе и . анализе не прошедших тестовых проверок.

Структура диссертационной работы.

Работа содержит введение, четыре главы, заключение, перечень сокращений, список опубликованных по теме диссертации работ, библиографический список и приложение.

Заключение диссертации по теме «Системы автоматизации проектирования (по отраслям)», Негода, Дмитрий Викторович

4.8. Выводы по четвертой главе

1. Модель МПС в контексте задачи создания средств интеграции симуляторов в САПР МПС и построения архитектурного каркаса целесообразно рассматривать в аспектах конструирования, симуляции и визуализации.

2. С точки зрения конструирования модель должна содержать универсальные средства связывания компонентов и соответствующие абстракции времени проектирования, такие как компонент, параметризация, совместимость интерфейсов, постоянное хранение (persistance).

3. С точки зрения симуляции интерес, представляют такие абстракции времени выполнения, как сообщения, их классификация и параметризация, план и стратегия симуляции.

4. С точки зрения визуализации модель МПС является моделью данных для соответствующих визуальных компонентов, что обеспечивает возможность комбинировать модели и представления (например, один и тот же отладчик можно использовать для моделей различных МП).

5. Оценка степени повторности использования кода архитектурного каркаса в экспериментальной разработке САПР МПС на базе i8086 показывает, что примерно 25% кода САПР составляет код архитектурного каркаса.

Заключение

В ходе исследований по теме диссертации получены следующие основные результаты:

1. Построенный в работе язык While++ позволяет моделировать свойства таких широко распространенных языков как Си и Java. В отличие от базового языка While, расширенный язык становится средством практического осуществления оптимизирующих преобразований программных моделей МП и МК, созданных на указанных языках программирования.

2. Разработан метод преобразования программ на промежуточном языке While++. В отличие от известных в теории компиляции методов оптимизирующих преобразований программ, работающих над графами потоков управления, предлагаемый метод позволяет получать продукт оптимизации на исходном языке программирования. Расширена реляционная хоа-ровская логика на язык While++, что позволяет доказывать корректность преобразований.

3. Разработан метод таблично-алгоритмической оптимизации симулятора по быстродействию, который позволяет повышать производительность симулятора на 43% практически без затрат времени разработчика.

4. Разработан метод оптимизации на основе отложенного вычисления флагов позволяет повышать производительность симулятора на 4-18%.

5. Разработан метод тестирования симуляторов, отличающийся от известных тем, что использует исходный код симулятора для генерации тестов машинных команд, которые затем выполняются на существующих интерпретаторах машинных команд - либо реальных микропроцессорах, либо заведомо правильных симуляторах. Благодаря этому трудозатраты на тестирование симуляторов сокращаются примерно в 3-4 раза.

6. Разработан объектно-ориентированный архитектурный каркас симуляции МПС, включающий базовую реализацию функций симулятора и интерфейсы для его настройки на конкретную систему команд МП и архитектуру МПС.

Полученные результаты могут явиться хорошей основой для широкого спектра дальнейших исследований, связанных с построением САПР МПС. К основным из направлений таких исследований следует отнести:

1. Исследование методов автоматизации проектирования симуляторов, базирующихся на полном спектре средств технологии объектно-ориентированного программирования.

2. Исследование возможностей распространения предложенных в диссертации методов на создание средств автоматизации проектирования программных моделей интерфейсных и прочих БИС окружения микропроцессора.

3. Исследование возможностей использования предложенных методов автоматизации проектирования симуляторов в симуляторах с динамической компиляцией.

Список используемых сокращений

ББ - базовый блок, максимальная последовательная цепочка операторов (или инструкций) без операций перехода. Иногда накладывается еще одно требование: в программе не должно быть переходов внутрь ББ, а только на его начало.

СК - система команд (instruction set).

СТП - самотестирующаяся программа (self-testing program)

МП - микропроцессор.

МПС - микропроцессорная система, включающая МП, память, порты ввода/вывода, контроллеры шины, периферийные устройства и пр.

МК - микроконтроллер, частный случай МПС.

ПДА - поразрядная двоичная арифметика.

ТАО - таблично-алгоритмическая оптимизация, при которой получается таблица частичных процедур.

ASM - Abstract State Machine. Абстрактная машина состояний (автомат).

CFG - Control Flow Graph, граф потока управления.

CFA - Control Flow Analysis, анализ потока управления.

DFA - Data Flow Analysis, анализ потока данных.

RHL - Relation Hoare Logic, расширение классической Хоаровской логики для анализа преобразований программ.

RTL - 1) Register Transfer Level, уровень межрегистровых передач, 2) Register Transfers List, внутренняя структура в виде трехадресного кода, используемая для внутреннего представления программ в компиляторах.

SoC - System on Chip, система на кристалле - (полу)заказная МПС, технологически выполненная на одном кристалле.

Публикации по теме диссертации

1. Negoda D. Fully Automated Test Generation for a Processor Simulator. Ulyanovsk State Technical University, Interactive Systems: The Problems of Human-Computer Interaction. - Collection of scientific papers, 2005.

2. Негода Д.В. Таблично-алгоритмическая оптимизация симулятора микропроцессора // Труды Белорусской Инженерной Академии, 2004.

3. Негода Д.В. Реинжениринг программной модели микропроцессора с целью повышения быстродействия. // Труды международной научно-технической конференции «Современные информационные технологии». Пенза. Пенз. технологич. ин-т., 2004.

4. Негода Д.В. Использование подстановки термов в оптимизации эмуляторов микропроцессоров // Пятая Международная научно-практическая конференция «Компьютерные технологии в науке, производстве, социальных и экономических процессах», Новочеркасск, 2004

5. НЕГОДА Д.В. Анализ потока данных в объектной надстройке над РСУБД // КЛИН, УлГТУ, 2005.

6. НЕГОДА Д.В. Отложенное вычисление флагов в симуляторах микропроцессоров // КЛИН, УлГТУ, 2005.

7. Negoda D. Ontology Representation Languages. Ulyanovsk State Technical University, Interactive Systems: The Problems of Human-Computer Interaction. - Collection of scientific papers, 2003, pp. 174-177

8. Negoda V.N., Negoda D.V. Foundation of Model Interaction in Microprocessor System Simulation System. Ulyanovsk State Technical University, Interactive Systems: The Problems of Human-Computer Interaction, 2001, pp. 70-72.

9. Negoda D. Interactive Telecommunication Simulator of i8086 Microprocessor. Ulyanovsk State Technical University, Interactive Systems: The Problems of Human-Computer Interaction, 1999, pp. 160.

Ю.Соснин П.И., Негода Д.В. Автоматическая классификация в базах данных опыта. // Информационные технологии в учебном процессе кафедр физики и математики (ИТФМ-2002): Труды VI международного совещания-семинара (24-26 сентября 2002 г.), под ред. Климовского А.Б. -Ульяновск: УлГТУ, 2002. - с. 104-106.

11.Негода В.Н., Негода Д.В. Репозитарий программно-информационных ресурсов учебной системы моделирования. // Информационные технологии, системы и приборы: Сборник научных трудов/УлГТУ. - Ульяновск, 2000. - с. 51-56.

12.Него да В.Н., Негода Д.В. Программа подготовки описаний информационных ресурсов. // Материалы выставки 2-й международной научно-технической конференции "Интерактивные системы проблемы челове-ко-компьютерного взаимодействия", - Ульяновск, 1997, с. 18-19.

Список литературы диссертационного исследования кандидат технических наук Негода, Дмитрий Викторович, 2005 год

1. Ахо, А, В., Сети, Р., Ульман, Дж., Компиляторы: принципы, технологии и инструменты.: Пер. с англ. - М.: Издательский дом «Вильяме», 2001. - 768 с.

2. Бердж В. Методы рекурсивного программирования/Пер. с англ. С.П. Забродина и др.; Под ред. Н.И. Иващенко. М.: Машиностроение, 1983.

3. Гамма Э., Хелм Р., Джонсон Р., Влиссидес Дж. Приемы объектно-ориентированного проектирования. Паттерны проектирования. -СПб.: Питер, 2001. 368 е.: ил.

4. Ицысков В. М. Исследование и проектирование моделей программных средств эмуляции вычислительных систем: Дис. канд. техн. наук: 05.13.13.-СПб, 1999.-249 е.: ил.

5. Негода В.Н. Средства автоматизации структурно-функционального проектирования микропроцессорных систем. Дисс. на соиск. уч. Степени д.т.н., Ульяновск: УлГТУ, 2001. - 156~с.

6. Негода Д.В. Таблично-алгоритмическая оптимизация симулятора микропроцессора микропроцессора // Труды Белорусской Инженерной Академии, 2004.

7. Капитонова Ю.В., Летичевский А.А. Математическая теория проектирования вычислительных систем. М.: Наука. Гл. ред. физ.-мат. лит., 1988.-296 с.

8. Липаев В. В. Тестирование программ. ■— М.: Радио и связь, 1986. — 296 с.

9. Соммервилл И. Инженерия программного обеспечения, 6-е издание.: Пер. с англ. — М.: Издательский дом «Вильяме», 2002. — 624

10. Ю.Суворова Е. А., Шейнин Ю. Е. Проектирование цифровых систем на VHDL. СПб.: БХВ-Петербург, 2003. - 576 е.: ил.

11. AVR® Instruction Set. Atmel Inc. http://www.atmel.com/dyn/resources/proddocuments/DOC0856.PDF

12. Bartak, R. Constraint Programming: In Pursuit of the Holy Grail, in: Proceedings of WDS99 (invited lecture), Charles University, Prague, June 1999.

13. Batcher K. et al. Instruction Randomization Self Test for Processor Cores, VTS, 1999.

14. BelIard, F., QEMU, a Fast and Portable Dynamic Translator, Proceedings of USENIX 2005 Annual Technical Conference, FREENIX Track, Anaheim, Canada, 2005, Pp. 41-46.

15. Benton, N. Semantics of Program Analyses and.Transformations. Lecture notes for the PAT Summer School. June 2005.

16. Benton, N. Simple Relational Correctness Proofs for Static Analyses and Program Transformations. Proceedings of the 31st ACM Symposium on Principles of Programming Languages (POPL). January 2004.

17. Borger E. and Stark R., Abstract State Machines: A Method for High-Level System Design and Analysis. Springer-Verlag, 2003.

18. Chandra, S. Retargetable Functional Simultor. A Master Thesis, Department of Computer Science & Engineering, Indian Institute of Technology, Kanpur, 1999.

19. Chen L. et al. DEFUSE: A Deterministic Functional Self-Test Methodology for Processors, VTS, 2000.

20. Chernoff A., Hookway R., DIGITAL FX!32 Running 32-Bit x86 Applications on Alpha NT, in Proceedings of the USENIX Windows NT Workshop, USENIX Association, Berkeley CA, August 1997.

21. Cifuentes C, Lewis B.T, Ung D., "Walkabout-A Retargetable Dynamic Binary Translation Framework", Sun Labs Tech Report TR-2002-106, January 2002.

22. Cifuentes, C. and Sendall, S. Specifying the Semantics of Machine Instructions. In Proceedings of the 6th international Workshop on Program Comprehension (June 24 26, 1998). IWPC. IEEE Computer Society, Washington, 1998.

23. Cirstea, H. and Kirchner, C. An introduction to the rewriting calculus. Research Report RR-3818, INRIA, December 1999.

24. Corno F. et al. On the Test of Microprocessor IP Cores, DATE, 2001.

25. Das, M., Lerner, S., Seigle, M., ESP: Path-Sensitive Program Verification in Polynomial Time. In Proceedings of the 2002 ACM SIGPLAN Conference on Programming Language Design and Implementation, 2002. pp. 57-68.

26. Dershowitz N., Jouannaud J.P. Rewrite Systems. Chapter 6 of Handbook of Theoretical Computer Science. Volume B: Formal Methods and Semantics, J. van Leeuwen ed. pp. 243-320, North Holland, Amsterdam, 1990.

27. Farfeleder S., Krall A., Horspool N. Ultra Fast Cycle-Accurate Compiled Emulation of Inorder Pipelined Architectures, To appear in Proceedings of SAMOS V: Embedded Computer Systems: Architectures, Modeling, and Simulation, 2005.

28. Fernandez, M. F., Ramsey, N., The New Jersey machine-code toolkit, Proceedings of the 1995 USENIX Technical Conference, 1995, pp. 289302.

29. Fox A.C.J., Harman N.A. Algebraic models of correctness for microprocessors. Technical Report CSR 8-98 (accepted for Formal Aspects of Computer Science). University of Wales Swansea, 1998. - 22 p.

30. Fox A.C.J., Harman N. A. Algebraic Models of Temporal Abstraction for Initialised Iterated State Systems: An Abstract Pipelined Case Study.Technical Report CSR 21-98 (submitted to Acta Informatica) -University of Wales Swansea, 1998. 32 p.

31. Fred kin E. Trie Memory. Communication of the ACM, 3: 490-500, 1960.

32. GENERATOR home page, http://www.squish.net/generator/

33. Gurevich Yu., Evolving Algebras 1993: Lipari Guide, Specification and Validation Methods, ed. E. Borger, Oxford University Press, 1995, 9—36.

34. Gurevich Yu., Huggins J. The Semantics of С Programming Language. Computer Science Logic, LNCS, vol. 702, 1993, pp. 274-309.

35. Hadjiyiannis, G., Hanono, S., Devadas, S., ISDL: An Instruction Set Description Language for Retargetability. DAC: Software Synthesis for Embedded Systems Anaheim, California, USA, 1997, pp. 299-302.

36. HaIambi, A., Grun, P., et al., EXPRESSION: A language for architecture exploration through compiler/simulator retargetability, in: Proceedings of the European Conference on Design, Automation and Test (DATE), Mar. 1999.

37. Harman N. A., Tucker J.V. Algebraic Models of Microprocessors: Architecture and Organisation. / Acta Informatica 33, 1996, pp. 421-456.

38. HedIey D. Final Year Project. An IBM PC Emulator For.Unix and Windows, 1994.

39. Hennessy J., Patterson D. Computer Organization and Design: The Hardware-Software Interface (Appendix A, by James R. Larus), Morgan Kaufman, 1993.

40. Herold, A., Siekmann, J., Unification in Abelian semigroups, J. of Automated reasoning 3 (3), 1987, pp. 215-221.

41. Hoare C.A.R. An axiomatic basis for computer programming. Communications of the ACM, 12(10):576-585, October 1969.

42. Hoffmann A., et al., A novel methodology for the design of application-specific instruction-set processors using a machine description language, IEEE Trans, on CAD of Integrated Circuits and Systems, vol. 20, pp 13381354, Nov. 2001.

43. Huang C., Cheng K., Assertion checking by combined word-level ATPG and modular arithmetic constraint-solving techniques. In Proceedings of the 37th Conference on Design Automation. Los Angeles, California, June 05 -09, 2000, pp. 118-123.

44. Huggins J. K. and Wallace C, An Abstract State Machine Primer, Technical Report CS-TR-02-04, Computer Science Department, Michigan Technological University, 4 December 2002.

45. Jones, N.D., Gomard, C.K., Sestoft, P. Partial Evaluation and Automatic program generation, Prentice Hall International, 1993. http://www.dina.kvl.dk/~sestoft/pebook/pebook.html.

46. Khare, A., et al., V-SAT: A visual specification and analysis tool for system-on-chip exploration, in: Journal of Systems Architecture 47, 2001, pp. 263-275.

47. Lacey D., De Moor O. Imperative program transformation by rewriting. In Compiler Construction (CC'01), Lecture Notes in Computer Science. SpringerVerlag, April 2001.

48. Larsson F. Generating Efficient Simulators from Specification Language. SICS Technical Report T97:01, 1997. 25 p.

49. Larsson F., Magnusson P, Werner B. SimGen: Development of Efficient Instruction Set Simulators. SICS Technical Report T97:03, 1997. 17 p.

50. Leupers R., Elste J., Landwehr B. Generation of Interpretive and Compiled Instruction Set Simulators. ASP-DAC 1999, pp. 339-342.

51. Nakada Т., Nakashima H. Design and Implementation of a High Speed Microprocessor Simulator BurstScalar. MASCOTS 2004: 364-372.

52. Nanda A.K., Hu Y., Ohara M., Giampapa M., Benveniste C., Michael

53. M., The Design of COMPASS : An Execution Driven Simulator for Commercial 152 Applications Running on Shared Memory Multiprocessors. Proceedings of International Parallel Processing Symposium, Apr. 1998.

54. Negoda D. Interactive Telecommunication Simulator of i8086 Microprocessor. Ulyanovsk State Technical University, Interactive Systems: The Problems of Human-Computer Interaction, 1999, pp. 160.

55. Nilsson, N.J. Principles of Artificial Intelligence, Tioga, Palo Alto, 1980.

56. Nilsson S. Radix sorting & searching. PhD thesis, Department of Computer Science, Lund University, Lund, Sweden, 1996.

57. PearPC PowerPC Architecture Emulator, http://pearpc.sourceforge.net/

58. QEMU Internals, http://fabrice.bellard.free.fr/qemu/qemu-tech.html

59. Rajesh V., A Generic Approach to Performance Modeling and Its Application to Simulator Generator, available at http://www.cse.iitk.ac.in/research/mtechl996/9611123.html

60. Rapps S., Weyuker E.J. Data Flow Analysis Techniques for Test Data Selection, IEEE proc. of ICSE-6, 1982, pp.272—278.

61. Reshadi, M. Dutt, N. Reducing compilation time overhead in compiled simulators, In Computer Design, 2003. Proceedings., 2003, pp. 151 -153.

62. Sakharov A. Specialization of Imperative Programs Through Analysis of Relational Expressions. Dagstuhl Seminar on Partial Evaluation 1996: 430-445.

63. Sakharov, A. Propagation of constants and assertions. SIGPLAN Not. 29, 5, 1994, pp. 3-6.

64. Shaffer J. H. A Performance Evaluation of Operating System Emulators. Bachelor Thesis, Department of Computer Science of Bucknell University 2004.

65. Shen J. and Abraham J.A., Native Mode Functional Test Generation for Processors with Applications to Self Test and Design Validation, International Test Conference, 1998, pp. 990-999.

66. Skrien, D. CPU Sim 3.1: A tool for simulating computer architectures for computer organization classes. ACM Journal of Educational Resources in Computing (JERIC) 1 (4), 2001, pp. 46-59.

67. Stickel, M. E., A unification algorithm for associative-commutative functions, J. of the Association for Computing Machinery 28 (3), 1981, pp. 423-434.

68. The vmips Project Home Page, http://vmips.sourceforge.net/

69. Tijms A. Binary translation: Classification of emulators. Leiden Institute for Advanced Computer Science, [e-mail]. http ://www.liacs.nl/~atij ms/bintrans .pdf.

70. Tip F. A Survey of Program Slicing Techniques. Journal of Programming Languages, 1995, vol. 3, no. 3, pp. 121-189.

71. Titzer B. L., Lee D. K., Palsberg J. Avrora: Scalable sensor network simulation with precise timing. In Proceedings of IPSN'05, International Conference on Information Processing in Sensor Networks, 2005.

72. Troger J. Specification-driven Dynamic Binary Translation. PhD Thesis, Faculty of Information technology, Queensland University of Technology, Brisbane, Australia, 2004.

73. Tsang, E. Foundations of Constraint Satisfaction, Academic Press, London, 1995.

74. Turing A. On Computable Numbers, with an Application to the Ent-sheidungsproblem. Proceedings of the London Mathematical Society, Series 2, Vol. 42:230-265, 1936.

75. Tupuri R. and Abraham J. A., A novel functional test generation method for processors using commercial ATPG, Proceedings of the International Test Conference 1997, Washington DC, Nov. 1997, pp. 743 752.

76. Ung, D. and Cifuentes, C. Machine-adaptable dynamic binary translation. In Proceedings of the ACM SIGPLAN Workshop on Dynamic and Adaptive Compilation and Optimization DYNAMO '00. ACM Press, New York, 2000. pp. 41-51.

77. Wallace C. The Semantics of the Java Programming Language: Preliminary Version. University, of Michigan EECS Department Technical Report CSE-TR-355-97.

78. Warren A. Hunt Jr. Microprocessor Design Verification. Journal of Automated Reasoning, Volume 5, Number 4, December 1989, pp. 429460.

79. Windley Ph.J. A Theory of Generic Interpreters. /In L.Pierre, G.Milne, editor, Correct Hardware Design and Verification Methods, p. 122—134. Lecture Notes in Computer Science 683, Springer-Verlag, 1993.

80. Zamulin A. V. A State-Based Semantics of a Pascal-Like Language. Siberian Devision of the Russian Academy of Sciences. A.P. Ershov Institute of Informatics Systems. Novosibirsk, 2003.

81. Zhang, Y. and Xu, B. A survey of semantic description frameworks for programming languages. SIGPLANNot. 39, 3, Mar. 2004, pp. 14-30.

82. Zhu, J., Gajski, D. D. A retargetable, ultra-fast instruction set simulator. In Proceedings of the Conference on Design, Automation and Test in Europe (Munich, Germany). ACM Press, New York, 1999.