Retrascope

h1. Reverse Engineering of HDL Descriptions Based on Static Code Analysis

h2. Abstract

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

В проектировании бывают и обратные процессы (reverse engineering) – когда по результатам анализа моделей низкого уровня, создаются или меняются модели более высоких уровней. Например, ошибка, обнаруженная в реализации системы, может привести к пересмотру концепции всей системы. В общем случае задача формулируется так – по имеющейся модели уровня I (реализации, низкоуровнему описанию) построить модель (или часть модели) более высокого уровня S (спецификацию, концептуальное описание). Вероятно, потребность в обратной инженерии возникает из-за недостатков в организации процесса разработки, однако реальность такова, что такие задачи возникают достаточно часто. Примеры задач и наша мотивация в исследованиях по этой тематике подробно рассмотрены в соответствующем разделе.

В контексте проектирования цифровой аппаратуры (digital hardware) задача обратной инженерии может быть поставлена следующим образом. Имеется описание устройства на уровне RTL (Register Transfer Level), требуется построить более абстрактное описание на архитектурном уровне (уровне TLM – Transaction Modeling Language). Возможна и другая постановка задачи – по описанию схемы устройства уровня логических вентилей (gate-level netlist) построить его описание на уровне RTL (или на более абстрактном уровне). Следует отметить, что, несмотря на то, что вторая постановка задачи (судя по беглому анализу работ) распространена шире, нас, в первую очередь, будет интересовать первый вариант задачи. Суть проблемы состоит в преобразовании описания устройства с уровня преобразования логических сигналов (возможно объединенных в битовые векторы) на уровень обработки сообщений (структурированных данных, обрабатываемых как единое целое).

h2. Problem Statement

В своей работе мы рассматриваем следующую постановку задачи. Имеется HDL-описание цифрового устройства на уровне RTL (Verilog или VHDL). Требуется построить описание устройства (модель) на уровне TLM (C++, SystemC или ином языке). Предполагается, что устройство является синхронным (управляется одним тактовым импульсом). (В дальнейшем это ограничение может быть снято.) Кроме того, HDL-описание является синтезируемым (такие конструкции, как вызовы внешних функций, игнорируются, поскольку их семантика неясна).

Чтобы уточнить постановку задачи, рассмотрим, что понимается под уровнями RTL и TLM.

На наш взгляд, наиболее адекватное определение уровня RTL можно дать, используя формализм действий с условиями (guarded actions), определенных над двоичными векторами. Если рассматривать только синхронные устройства, условия проверяются параллельно на каждом такте (с учетом зависимостей по данным); для выполненных условий, запускаются соответствующие действия. Именно такого рода системы определяются на HDL-языках.

Основные элементы метамодели TLM описаны ниже.

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

# Интерфейс (interface) — «точка», связывающая модель устройства с его окружением: через интерфейс происходит подача сообщений на модель устройства или выдача сообщений наружу. Интерфейсы подразделяются на входные интерфейсы (входы) и выходные интерфейсы (выходы).

# Блок (block) — часть модели устройства, которая, в свою очередь, является моделью (имеет входные и выходные интерфейсы, вложенные блоки и т.п.).

# Примитив (primitive) — элементарный блок (блок, который не раскладывается на другие блоки). Примерами примитивов являются функция, очередь и другие.

# Канал (channel) — средство передачи сообщений с выхода одного блока модули устройства на вход другого блока. Каналы различаются временем передачи сообщений и возможностью параллельной передачи нескольких сообщений. Простейшим типом канала является пересылка данных с одних регистров на другие. Более сложный пример – синхронный канал – канал, осуществляющий передачу сообщений в случае готовности передатчика и приемника.

# Функция (function) — примитив, осуществляющий преобразование сообщений. Функция имеет один вход и один выход. В общем случае, тип выходного сообщения отличается от типа входного сообщения. Преобразование сообщения осуществляется мгновенно (аналогично комбинационной логике в RTL-описании).

# Очередь (queue) — примитив, осуществляющий хранение сообщений в памяти и выбор сообщений из хранилища в соответствии с некоторой стратегией. Простейшим типом очереди является очередь FIFO ограниченного размера.

Другими примитивами являются маршрутизатор (switch), арбитр (merge), ветвление (fork) и соединение (join). Они используются для управления потоком сообщений в модели.

h2. Research Motivation

Мотивация наших исследований основана на актуальности следующих задач (порядок перечисления задач никак не отражает их важности).

# Поддержка унаследованного (legacy) кода – есть унаследованный код (без подробной документации), который необходимо поддерживать (оптимизировать / исправлять ошибки, не нарушая функциональность) – чтобы это делать, необходимо понять его концептуальную организацию и ограничения, при которых код работает.

# Верификация модульного уровня – есть модуль (компонент) системы, который требуется тщательно проверифицировать (поскольку есть подозрение, что в модуле есть ошибки), но для которого нет документации (при этом документация на систему в целом может и быть). В условиях неполной документации анализ функций модуля в той или иной степени базируется на реконструкции концептуальной модели устройства. Далее проверяется эта модель (инспекция, формальная верификация) и соответствие ей реализации (динамическая верификация, проверка эквивалентности).

# Формальная проверка соответствия (equivalence checking) – важная подзадача верификации, которую можно рассмотреть отдельно – имеются две модели, RTL-модель и TLM-модель, необходимо формально проверить их эквивалентность в смысле некоторого отношения эквивалентности (синхронная эквивалентность, событийная эквивалентность).

# Анализ высокоуровневых свойств – есть описание свойств системы, выполненное на более высоком уровне по сравнению с реализацией системы. Например, свойства могут формулироваться в терминах сообщений (TLM), а реализация быть описанной в терминах логических сигналов (RTL, netlist). В таких случаях нужно преобразование уровня абстракции. Для динамического анализа свойств вокруг реализации делается обертка (адаптеры, транзакторы), осуществляющая преобразование интерфейсов. Для статического анализа удобнее построить абстрактную модель и провести анализ свойств на ней.

# Быстрая симуляция аппаратуры – есть описание системы на низком уровне (RTL, netlist), для которого нужно в динамике проверять некоторые высокоуровневые свойства. Можно использовать транзакторы (см. предыдущий пункт), но в этом случае симуляция осуществляется медленно. Альтернативой является трансляция низкоуровневых описаний системы в более абстрактные (и, возможно, оптимизированные) описания на языках программирования.

# Важным частным случаем этой задачи является оптимизация симуляции больших TLM-моделей с включенными в их состав RTL-компонентами (IP cores). Как уже отмечалось ранее (см. пункт 1), многие компоненты современных аппаратных систем являются унаследованными (legacy), и для них нет разработанных моделей уровня TLM. Такие компоненты существенно замедляют симуляцию и анализ результирующей TLM-модели, сводя на нет преимущества TLM. Создание TLM моделей для существующих (и, как правило, плохо специфицированных) RTL-моделей является трудоемкой задачей, которую желательно автоматизировать.

h2. Possible Results (Methods/Tools)

Результатами работы (помимо общей методологии анализа и обратной инженерии HDL-описаний) могут быть следующие методы/инструменты.

# Метамодель (система связанных формализмов), предназначенная для описания цифровой аппаратуры на разных уровнях абстракции (RTL и разные разновидности TLM: системы действий с условиями (guarded actions) (чистый RTL), расширенные конечные автоматы (EFSM, ASM) (разделение управляющей логики и функций преобразования данных), микроархитектурые сети (xMAS) (выявление типовых компонентов и каналов связи) и т.д.). Библиотека классов, предназначенная для моделирования цифровой аппаратуры (внутреннее представление).

# Методы анализа моделей цифровой аппаратуры, позволяющие выявлять или проверять некоторые свойства аппаратуры (наличие «мертвого кода», зависаний, конфликтов и т.п.). Инструменты анализа моделей цифровой аппаратуры.

# Методы (вертикальной) трансформации моделей цифровой аппаратуры, позволяющие по низкоуровневым описаниям строить более высокоуровневые модели (функционально эквивалентные (в смысле синхронной эквивалентности) или с более общей моделью поведения). Инструменты трансформации моделей цифровой аппаратуры.

# Методы проверки соответствия (синхронной эквивалентности, событийной эквивалентности) между моделями цифровой аппаратуры разного уровня абстракции. Методы генерации тестов для моделей цифровой аппаратуры. Инструменты проверки соответствия между моделями цифровой аппаратуры. Инструменты генерации тестов для моделей цифровой аппаратуры.

# Методы трансляции моделей цифровой аппаратуры на языки программирования высокого уровня для целей симуляции и динамического анализа этих моделей (приведение моделей к стандартизованному виду, прежде всего, к формату SystemC TLM). Инструменты трансляции и симуляции моделей цифровой аппаратуры.

Некоторые конкретные примеры методов/инструментов:

TODO:

h2. Method Concept

Основные концепции метода:

# Абстракция интерфейса (выделение сообщений и каналов)

# Абстракция управляющей логики (выделение арбитров и маршрутизаторов)

# Абстракция функций преобразования данных (абстракция преобразователей)

h2. Research Plan

Ниже представлен ориентировочный план исследований.

# Выделение сообщений:

a.	группировка сигналов — анализ совместного использования сигналов (если несколько сигналов всегда (или очень часто) используются совместно, они могут быть объединены в сообщение);

b.	выделение многотактных транзакций — анализ формирования внутренних сообщений по входным сигналам и анализ формирования выходных сигналов по внутренним сообщениям.

# Выделение функций обработки сообщений:

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

b.	Абстракция функциональных преобразований (абстракция комбинационной логики) — реконструкция функций по комбинационным схемам (например, выделение сложения и других типовых функций по паттернам, анализ способов использования результатов схем и т.д.).

# Выделение каналов передачи сообщений:

a.	Выделение каналов между вложенными модулями — анализ передачи сообщений во вложенные модули (если есть вложенный модуль, соединенный с исходным модулем или другим вложенным модулем сигналами, соответствующими сообщению, в модели создается простейший канал между ними).

b.	Выделение каналов внутри исходного модуля — выделение точек хранения сообщений (данных, соответствующих сообщениям) и пересылок сообщений из одной точки в другую.

# Выделение примитивов, управляющих передачей сообщений (абстракция управляющей логики):

a.	Выделение примитивов, управляющих передачей сообщений (арбитров (мультиплексоров), маршрутизаторов (демультиплексоров) и др.).

# Выделение блоков, описываемых автоматными моделями (FSM, EFSM):

a.	Выделение переменных, кодирующих состояния (выявление циклов обратной связи потоках данных элементарных действий).

b.	Выделение пространства состояний (состояние – конкретное значение переменных состояний или класс значение (ограничение на значения)).

c.	Построения отношения переходов (переход – охраняемое действие)

# Генерация функциональных тестов по построенной модели:

a.	Создание адекватных метрик тестового покрытия на основе моделей.

b.	Создание методов генерации тестов на основе предложенных метрик.

# Формальный анализ и оптимизация построенной модели:

a.	Анализ наличия недостижимого кода (dead code), тупиков/зависаний (deadlocks), переполнения очередей и т.п.

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

c.	Оптимизация автоматных моделей (минимизация числа состояний и т.п.).

d.	Оптимизация коммуникационной сети.

h2. Implementation Ideas

h2. Related Work

h2. References

h3. EFSM Extraction

# http://www.google.com/patents/US5774370