Extracting assertions for conflicts in HDL descriptions

При проектировании модулей цифровой аппаратуры могут возникать конфликты доступа к данным. Одним из способов их выявления на ранних стадиях проектирования является статический анализ описаний цифровой аппаратуры (или HDL-описаний). В данной статье описывается метод поиска конфликтов доступа к данным в HDL-описаниях. Метод реализован в инструменте Retrascope и ориентирован на конфликты следующих типов: одновременные чтение и запись; одновременная запись; обращение к неинициализированным данным; отсутствие чтения между двумя актами записи. Конфликты задаются в виде условий (assertion) на внутренние переменные. Входное HDL-описание автоматически транслируется в формальную модель на языке, являющемся входным для инструмента проверки моделей nuXmv. Трансляция включает следующие этапы: 1) предварительная обработка; 2) построение графа потока управления; 3) трансформация графа потока управления в решающую диаграмму охраняемых действий (GADD-модель); 4) трансляция GADD-модели в формат инструмента nuXmv. Условия возникновения конфликтов строятся автоматически на основе статического анализа GADD-модели и передаются инструменту проверки моделей nuXmv. Найденные контрпримеры (последовательности значений входных сигналов, приводящие к достижению конфликта) автоматически транслируются инструментом Retrascope в тесты, которые могут быть исполнены на симуляторе. Предложенный метод поиска конфликтов был применен к ряду открытых тестовых наборов и модулей — Texas-97, Verilog2SMV, VCEGAR, mips16. Были выявлены потенциальные конфликты для всех указанных категорий. В качестве направлений дальнейших исследований рассматриваются вынос условий конфликтов на уровень входных сигналов (и получение, таким образом, сведений о протоколах взаимодействия между модулями), а также генерация встроенных проверок в коде HDL-описаний.