Ideas and Proof of Concept » History » Revision 5
Revision 4 (Alexander Kamkin, 07/21/2013 08:12 AM) → Revision 5/9 (Alexander Kamkin, 07/23/2013 07:07 AM)
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. Задачи (обсуждение темы диссертации Сергея Смолова)
# Парсер для языка Verilog и представление абстрактного синтаксиса.
# Внутреннее представление для анализа и преобразований Verilog-кода.
# Анализ потоков управления и данных на основе внутреннего представления.
# NEW: Выявление неявных переменных состояния (инструкций ожидание) и их замена явными переменными.
# NEW: Построение системы GAs по внутреннему представлению кода.
# Символическое выполнения для внутреннего представления.
# Извлечение EFSM-моделей из Verilog-кода (системы GAs).
# Анализ причинно-следственных связей (влияния входов на выходы).
# Выявление ограничений на входы по охранным предикатам переходов EFSM-моделей.
# Динамическая/статическая генерация тестов по EFSM-моделям.
# Генерация safety-правил для пар EFSM-моделей (нарушение целостности потока данных).
# Анализ возможности тупиков для сети взаимодействующих EFSM-моделей.
# Трансляция Verilog-кода (EFSM-моделей) в язык одного из инструментов проверки моделей.
# Предикатная абстракция Verilog-кода (EFSM-моделей).
# Группировка сигналов в сообщения на основе анализа их использования в Verilog-коде.
# Выявление многотактных транзакций с устройством.
# Формат для описания транзакторов (мэппинга сообщений на сигналы).
# Средства прототипирования тестовых систем (ручного описания транзакторов).
# Формат для описания ограничений на сообщения (тестовых ситуаций).
# Генерация шаблона тестовой системы по описанию транзакторов.
# Генерация тестового сценария по EFSM-моделям и описанию ограничений.
# Локализация ошибок в коде по ошибочным реакциям.
# NEW: Абстракция на уровне GAs (удаление избыточной синхронизации и управляющей логики, увеличение параллелизма)
# Трансформация RTL-модели в синхронно-эквивалентную TLM-модель.
# Трансформация синхронной TLM-модели в событийно-эквивалентную TLM-модель.
# Трансляция событийной TLM-модели в язык одного из инструментов проверки моделей.
# Формальный анализ свойств событийной TLM-модели (гонки и конфликты).
# Абстракция операций по структуре комбинационных схем и использованию результатов.
# Генерация кода для событийной TLM-модели на С++ и SystemC (TLM 2.0).
h2. Implementation Ideas
h2. Related Work
The paper [FAST12] presents a FAST framework that accelerates fault simulation (mutation testing) through automatic abstraction of HDL descriptions (code with injected faults) into event-equivalent transaction-level models (TLMs). Fault injection/simulation techniques have been widely investigated in the past decades. The most interesting part of the work is related to RTL-to-TLM abstraction (see also [17]), which, in turn, is based on EFSM extraction. Given an EFSM model, the tool is able to recognize computational phases (paths that must be traversed to (1) get the input data, (2) elaborate them, and (3) produce the output result). Abstraction is carried out by collapsing computational subphases according to a set of state-merging rules.
Some papers address the problem of EFSM-based test generation [EFSM11,11-13]. If EFSMs are derived from HDL descriptions, such tests are able to achieve high level of code coverage and, as opposed to [7], to cope with state dependencies. The dominant approach used in the area (as well as in model checking) is state graph traversal. Comparing with the FSM-targeted methods, there is an issue related to transition guards. When guards depend on registers (not only on inputs), it is hard to determine whether a path is feasible or not. There are techniques for EFSM transformation that eliminate dependencies [11-13], but they may lead to state explosion. An alternative is to use backtracking (and backjumping) to search for reachable states [EFSM11].
In [EFSM11], generation of “easy-to-traverse” EFSMs from HDL code is described. The process consists of the four steps: (1) an initial EFSM (REFSM, reference EFSM) is extracted from code by using standard procedures [18]; (2) new states are added to the REFSM to split transitions into “smaller” ones, with no conditional statements in actions (LEFSM, largest EFSM); (3) the LEFSM is transformed by grouping compatible transitions to be time-equivalent to the REFSM (SEFSM, smallest EFSM); (4) the SEFSM is stabilized [13] on the register encoding the design state (S ^2^ EFSM, semi-stabilized EFSM). The method is rather powerful, but, we believe, it could be improved if it took notice of the state register(s) from the beginning.
h2. References
| [FAST12] | N. Bombieri, F. Fummi and V. Guarnieri, “FAST: An RTL Fault Simulation Framework based on RTL-to-TLM Abstraction”, Journal of Electronic Functional testing, Springer, 2012. |
| [EFSM11] | G. Guglielmo, L. Guglielmo, F. Fummi and G. Pravadelli, “Efficient Generation of Stimuli for Functional Verification by Backjumping Across Extended FSMs”, Journal of Electronic Functional testing: Theory and Application, Volume 27, Issue 2, 2011, pp. 137-162. |
| [EFSM] | http://www.google.com/patents/US5774370 |