Микроэлектроника, 2020, T. 49, № 1, стр. 66-80

ВВЕДЕНИЕ

Для описания поведения и схемной реализации цифровых систем на современной элементной базе заказных СБИС (сверхбольших интегральных схем) либо в базисе программируемых логических схем (ПЛИС) типа FPGA (FPGA – Field-Programmable Gate Array) разработан ряд языков, основными из которых являются Verilog и VHDL [1]. Практически все современные развитые САПР (системы автоматизированного проектирования) позволяют использовать исходные спецификации проектируемых цифровых устройств на одном из этих языков (либо на обоих вместе). Процесс синтеза в САПР СБИС автоматизирован, с увеличением сложности проектов актуальной проблемой является верификация исходных Verilog- и VHDL-описаний проектов. Последние стандарты языка VHDL [2] ориентированы на решение проблем верификации – добавлены конструкции, облегчающие написание тестирующих программ, генерацию управляемых тестов и сбор статистики. Аналогичные потребности привели к созданию языка SystemVerilog [3, 4], в котором можно применять объектно-ориентированный подход для выполнения моделирования и верификации исходных описаний.

Для проектов на Verilog и VHDL предложен язык PSL [5], позволяющий использовать аппарат ассертов – формальных утверждений о свойствах проектов. По существу, проблема верификации исходных спецификаций проектов [6], наряду с проблемой сокращения энергопотребления логических схем, реализующих исходные описания, являются основными проблемами, стоящими перед разработчиками САПР СБИС. Для повышения эффективности проектирования предпринимаются различные попытки использования языков и средств повышения уровня абстракции исходных описаний, а именно, использовать описания на языке С, графические описания в подсистеме State Flow системы MatLab и др. Например, в работе [7] показано, что описания, подготовленные в State Flow были конвертированы в VHDL-описания, которые затем были успешно реализованы на ПЛИС. САПР становятся “многоязыковыми”, например, система моделирования Questa Sim [8] поддерживает языки VHDL, Verilog, PSL, System Verilog, SystemC и C/C++.

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

Язык ПРАЛУ (Простых Алгоритмов Логического Управления) предназначен для описания параллельных алгоритмов логического управления. Его характерными особенностями являются логическая стройность, простота, компактность получаемых описаний, использование двоичных (булевых) переменных для входных и выходных переменных устройств управления, алгоритм функционирования которых задан на языке ПРАЛУ. Полное описание языка ПРАЛУ содержится в работе [9], где предложена модель параллельного автомата и преобразование ее в модель секвенциального автомата [10], являющейся промежуточной при схемной реализации параллельных автоматов, представленных на языке ПРАЛУ.

В данной работе описывается верификация исходных ПРАЛУ-описаний параллельных автоматов. Верификация может быть проведена на основе моделирования исходных описаний и на основе проверки семантических свойств автомата. Предлагаются средства перехода к эквивалентным по поведению VHDL-моделям параллельных автоматов и VHDL-моделям секвенциальных автоматов, получаемые алгоритмические VHDL-модели автоматов являются синтезируемыми, т.е. по ним возможно автоматическое построение логических схем в заданных технологических базисах. Отметим, что в работах [9, 10] предлагается схемная реализация секвенциальных (и тем самым и параллельных) автоматов в виде программируемой логической матрицы (ПЛМ) с памятью в виде регистра RS-триггеров. Получение VHDL-моделей секвенциальных автоматов позволяет получать логические схемы в произвольном функционально полном базисе логических элементов ASIC либо FPGA. Кроме того, использование VHDL-моделей позволяет также привлечь для верификации мощные средства промышленных систем моделирования VHDL-описаний цифровых систем, например средства системы Questa Sim (ф. Mentor Graphics). Таким образом, предлагаемый подход к верификации имеет комплексный характер – при верификации проверяются как семантические свойства, так и осуществляется функциональная верификация проекта, а получение VHDL-моделей позволяет проводить как быстрое моделирование для функциональной верификации, так и проводить синтез логических схем, в различных технологических базисах, для чего может быть использован синтезатор Leonardo Spectrum [11]. В отличие от формальной верификации, когда на эквивалентность поведения проверяются два VHDL-описания цифровой системы, в данной статье под верификацией далее будет пониматься проверка правильности исходного VHDL-описания, т.е. проверка соответствия составленного синтезируемого VHDL-описания проектируемой цифровой системы спецификациям на проектирование [6]. Так как параллельные автоматы могут входить в состав более сложных проектов цифровых систем, то предлагаются также средства построения компактных функциональных тестов для выполнения функциональной верификации параллельных автоматов.

1. ПРАЛУ-ОПИСАНИЯ ПАРАЛЛЕЛЬНЫХ АВТОМАТОВ

Модель параллельного автомата [9, 10] позволяет учитывать параллелизм логического управления и является функциональной моделью дискретного устройства управления. Данная модель состоит из множества X входных булевых переменных, множества Y выходных булевых переменных и множества цепочек (строк-переходов). Согласно [9] цепочки имеют вид

в которой операция $ - k_{i}^{1}$ или $ \to k_{i}^{2}$ (или обе вместе) может отсутствовать. В общем случае цепочка состоит из четырех частей:

μ_i – множество начальных частичных состояний i-ой цепочки;

$ - k_{i}^{1}$ – операция ожидания события $k_{i}^{1};$

$ \to k_{i}^{2}$ – операция действия;

ν_i – множество заключительных частичных состояний цепочки.

В формуле (1) двоеточие служит разделителем, а стрелка $ \Rightarrow $ перед ν_i играет роль операции внесения элементов в текущее множество запуска цепочек. Множества μ_i, ν_i – это подмножества из множества M частичных состояний, в работе [9] частичные состояния названы метками. Будем предполагать, что начальное частичное состояние всегда имеет номер 1, и что частичные состояния последовательно нумеруются (номера идут без пропусков). Сначала поясним, что представляют собой операции ожидания и действия, а затем – каким образом выполняется алгоритм в целом, т.е. как выполняются (срабатывают) цепочки, как они взаимодействуют друг с другом и какую роль играет множество запуска цепочек. Ниже представлен пример параллельного автомата Zak178 из книги [9, c. 178]

В данном примере X = {u, v, w} – множество входных булевых (двоичных) переменных, Y = {a, b, c, d} – множество выходных булевых переменных параллельного автомата. Множество M образуют частичные состояния с номерами от 1 до 13. В записи (1) $k_{i}^{1},$ $k_{i}^{2}$ представляют собой элементарные конъюнкции булевых переменных (с инверсиями либо без инверсий), штрихами помечены инверсии булевых переменных. Конъюнкции $k_{i}^{1}$ образуются из булевых переменных множества X, конъюнкции $k_{i}^{2}$ образуются из булевых переменных множества Y. Если переменные входят как во множество X, так и во множество Y, то такие переменные в ПРАЛУ-описаниях объявляются внутренними. В рассматриваемом примере (табл. 1) внутренних переменных нет – в разделе INTER нет переменных.

Если конъюнкция $k_{i}^{1}$ отсутствует в (1), то предполагается, что она тождественно равна 1. Операция $ - k_{i}^{1}$ представляет собой операцию ожидания события $k_{i}^{1}.$ Выполнение этой операции сводится к ожиданию события, когда переменные, входящие в конъюнкцию $k_{i}^{1},$ примут значения, обращающие $k_{i}^{1}$ в единицу. Операция действия →$k_{i}^{2}$ означает присвоение таких значений переменным конъюнкции $k_{i}^{2},$ при которых $k_{i}^{2}$ обращается в единицу. Если же $k_{i}^{2}$ отсутствует в (1), то предполагается, что никакие операции действия в данной цепочке не выполняются.

Предполагается синхронная модель параллельного автомата – в каждом такте любая из цепочек может сработать (либо не сработать). Управление цепочками осуществляется в дискретном (тактируемом) времени с помощью множества $N \subseteq M,$ называемого множеством запуска. Цепочка (1) срабатывает, если в текущем множестве запуска содержится множество μ_i и если выполнилась операция ожидания $ - k_{i}^{1}.$ В начале работы алгоритма в текущее множество запуска включается частичное состояние 1. Срабатывание цепочки в текущем такте предполагает удаление множества μ_i из текущего множества запуска, выполнение операции действия →$k_{i}^{2},$ и включении множества ν_i в текущее множество запуска. Алгоритм заканчивает работу, если множество запуска содержит заключительное частичное состояние, т.е. частичное состояние, которого нет в множествах μ_i начальных частичных состояний цепочек. В рассматриваемом примере заключительного частичного состояния нет – алгоритм “зациклен”.

Полное состояние (далее просто состояние) параллельного автомата в текущем такте образуют частичные состояния из множества N запуска цепочек.

В процессе работы алгоритма некоторые цепочки могут выполняться одновременно (параллельно), поэтому такой формализм позволяет описывать параллельные алгоритмы логического управления. При этом множество цепочек должно удовлетворять определенным требованиям, например, цепочки, имеющие одинаковые множества начальных частичных состояний, должны иметь ортогональные конъюнкции в операциях ожидания. Другие требования к корректности исходных ПРАЛУ-описаний изложены в [9, 10].

2. ВЕРИФИКАЦИЯ ПАРАЛЛЕЛЬНЫХ АВТОМАТОВ

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

Результаты моделирования параллельного автомата Zak178 на 33 псевдослучайных наборах заданы в табл. 2: во втором столбце – входные наборы (тест); в третьем столбце – значения выходных переменных (выходные реакции), в четвертом столбце – состояния (состояния параллельного автомата для следующего такта моделирования). По результатам моделирования может быть построен граф G (рис. 1) переходов, вершинами которого являются состояния параллельного автомата (см. строки из четвертого столбца табл. 1).

Рис. 1.

Граф G переходов параллельного автомата, построенный по результатам моделирования (табл. 1) на 33 входных наборах.

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

Для параллельных алгоритмов в работе [9] сформулированы пять семантических свойств: безызбыточность, восстанавливаемость, непротиворечивость, устойчивость, самосогласованность. Формальные методы проверки таких свойств для параллельных автоматов имеют отдельный интерес, они представлены в [10], и в данной работе не рассматриваются. Однако некоторые из таких свойств могут быть проверены на уровне VHDL-описаний параллельных автоматов.

3. СИНХРОННАЯ VHDL-МОДЕЛЬ ПАРАЛЛЕЛЬНОГО АВТОМАТА

Предлагается представлять VHDL-описание параллельного автомата в виде двух взаимодействующих процессов (оператор process). Для каждого текущего частичного состояния i вводится соответствующий сигнал текущего Li и сигнал n_Li следующего частичного состояния. В первом процессе (process p1) в текущем такте ${{t}_{i}}$ определяются элементарные цепочки, которые работают параллельно и следующие (для следующего такта ${{t}_{{i + 1}}}$ дискретного времени) значения переменных ${{y}_{j}}$ действия и значения сигналов частичных состояний. Подготавливаемые значения сигналов для переменных действия обозначаются через $n\_{{y}_{j}},$ а подготавливаемые значения переменных множества запуска – через n_Li. Во втором процессе (process p2) осуществляется смена состояния параллельного автомата по переднему фронту сигнала синхронизации clk. Для этого используется оператор if (clk = '1' and clk’event) then нахождения переднего фронта сигнала clk. Установка автомата в начальное состояние (переменные действия имеют значение 0, а в множество запуска включается только сигнал L1) осуществляется по единичному значению сигнала rst разрешения, который имеет более высокий приоритет по отношению к другим входным сигналам. На момент смены такта значения сигналов, соответствующих переменным ожидания из конъюнкций $k_{i}^{1},$ должны быть установившимися. Заметим, что в исходном описании параллельного автомата сигнал clk отсутствует. В Приложении 1 дана VHDL-модель Zak178_PA параллельного автомата Zak178, ПРАЛУ описание которого дано в табл. 1. Вектор state в VHDL-модели автомата отражает состояние параллельного автомата и нужен для тестирующей программы, которая выдает результаты VHDL-моделирования в таком же формате, что и программа QPralu моделирования исходного описания автомата. Формат входных тестов является одинаковым для обоих вариантов моделирования.

4. ВЕРИФИКАЦИЯ VHDL-ОПИСАНИЙ ПАРАЛЛЕЛЬНЫХ АВТОМАТОВ

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

Свойство безызбыточности: алгоритм безызбыточен, если в нем нет операций, которые никогда не выполняются, ни при каких условиях не могут быть выполнены [9, с. 61]. Очевидно, что удаление соответствующих фрагментов из алгоритма не скажется на его функциональных свойствах. На уровне VHDL-описаний проверка свойства осуществляется выполнением моделирования с покрытием VHDL-кода в системе Questa Sim. Покрытие VHDL-кода при моделировании подробно описано в [2]. Непокрытые конструкции (строки VHDL-кода) будут означать возможную избыточность описания, по которой можно легко (однозначно) установить избыточность в исходном описании параллельного автомата.

Свойство восстанавливаемости: алгоритм восстанавливаем, если из любого достижимого состояния он может вернуться в исходное. На уровне VHDL-описаний решение осуществляется построением и анализом графа переходов между состояниями ‑ из любой вершины графа должен быть путь в начальное состояние. В число функциональных тестов могут входить тесты, позволяющие приходить из начального состояния в заданное состояние (заданную вершину графа переходов) и выходить из заданного состояния в начальное состояние.

Свойство непротиворечивости: алгоритм непротиворечив, если при его выполнении не может возникнуть ситуация, в которой одновременно выполняются несовместимые между собой операции. Для языка ПРАЛУ такая противоречивая ситуация возникает при совместном выполнении двух операций действия с ортогональными конъюнкциями: в этом случае некоторой внутренней либо выходной переменной присваиваются два различных значения, что невозможно.

5. ПОСТРОЕНИЕ КОМПАКТНЫХ ФУНКЦИОНАЛЬНЫХ ТЕСТОВ ПО РЕЗУЛЬТАТАМ МОДЕЛИРОВАНИЯ

Основной подход к верификации VHDL-моделей схем управляющей логики реализуется на основе моделирования и комплексного тестирования, целью которых являются соответствующие проверки для подтверждения того, что функциональность VHDL-описания будет правильной [2, 6, 7]. Данный подход не ограничен стилями исходных описаний, основные проблемы заключаются в генерации направленных функциональных тестов и организации тестирования. В рамках данного подхода, являющегося наиболее распространенным подходом к верификации, предлагается решать поставленную задачу верификации VHDL-описаний параллельных автоматов. Обзор существующих моделей параллельно функционирующих распределенных систем, методов и инструментальных средств их верификации представлен в [11], где указывается, что одной из основных проблем, возникающих при верификации взаимодействующих цифровых систем, описываемых в терминах состояний, является комбинаторный взрыв числа возможных параллельных состояний всей системы в целом. Это касается как формальной верификации, так и верификации на основе моделирования.

В отличие от VHDL-модели конечного автомата, граф переходов которого извлекается в системе Questa Sim и может быть проанализирован [2], из VHDL-модели (см. Приложение 1) параллельного автомата система Questa Sim граф переходов не извлекает, так как модель параллельно автомата является более общей, чем модель конечного автомата. Поэтому для автоматизированного построения графа $G$ состояний параллельных автоматов и получения компактного функционального теста, обеспечивающего покрытие всех дуг данного графа, были разработаны и модифицированы соответствующие программы [12, 13] позволяющие обрабатывать результаты моделирования (см. табл. 1), содержащие тестовые последовательности с миллионами тестовых наборов. Входные тестовые наборы, соответствующие дугам, вошедшим в покрытие графа, образуют тест для функциональной верификации параллельного автомата. Ориентированный граф G переходов, построенный по результатам моделирования, должен удовлетворять следующему условию: из начального состояния в каждую вершину должен существовать путь и из каждой вершины в начальную вершину также должен быть путь. При выполнении данного условия может быть построен компактный тест (в виде циклов), покрывающий все дуги графа.

Покрытие дуг графа G осуществляется циклами (замкнутыми контурами) из начальной вершины 1. Например, граф переходов параллельного автомата, построенный по результатам моделирования на 20 000 входных наборов (см. табл. 2 и рис. 2) содержит 21 вершину. Имена вершин графа G даны в табл. 4. Граф G имеет 63 дуги и покрывается 18 циклами (табл. 5), которые содержат 181 дугу. Так как каждой дуге соответствует входной набор, то функциональный тест, обеспечивающий переходы по всем 63 дугам графа, содержит 181 входной набор. Результаты моделирования на 23 входных наборах компактного теста, соответствующих первому циклу, показаны в табл. 6.

Рис. 2.

Граф G переходов параллельного автомата, построенный по результатам моделирования на 20 000 входных наборах.

6. СХЕМНАЯ РЕАЛИЗАЦИЯ ПАРАЛЛЕЛЬНЫХ И СЕКВЕНЦИАЛЬНЫХ АВТОМАТОВ

Будем предполагать, что исходное ПРАЛУ-описание, по которому осуществляется схемная реализация, является корректным. Синтез логических схем, реализующих параллельные автоматы, может выполняться двумя способами.

Первый способ – переход к синтезируемой VHDL-модели параллельного автомата и выполнение синтеза в одном из промышленных синтезаторов схем ASIC либо ПЛИС типа FPGA. Далее в качестве такого синтезатора будет использоваться синтезатор LeonatdoSpectrum [14].

Второй способ – получение матричного описания секвенциального автомата, поведение которого совпадает с поведением параллельного автомата, и переход к синтезируемой VHDL-модели секвенциального автомата [10].

Секвенциальный автомат является моделью цифровой системы, функционирующей в дискретном времени, и состоит из множества S секвенций s_i. Каждая секвенция s_i имеет форму ${{f}_{i}}$ ├ ${{k}_{i}},$ где ${{f}_{i}}$ – булева функция входных и внутренних переменных, ${{k}_{i}}$ – элементарная конъюнкция внутренних и выходных переменных. Каждая секвенция ${{f}_{i}}$ ├ ${{k}_{i}}$ описывает определенное требование к поведению цифровой системы: если в некоторый момент времени ${{f}_{i}}$ принимает значение 1, то непосредственно вслед за этим (в следующем такте дискретного времени) ${{k}_{i}}$ также принимает значение 1. Будем интерпретировать данную систему секвенций как инерционный секвенциальный автомат. В инерционном секвенциальном автомате предполагается следующее [10]: если во всех элементарных конъюнкциях ${{k}_{i}},$ соответствующих функциям ${{f}_{i}},$ принимающим в текущий момент времени значение 1, отсутствует символ некоторой переменной, то считается, что эта переменная сохраняет свое значение. В табл. 7 дано матричное описание секвенциального автомата Zak178 в формате программы QPralu. Переход от модели параллельного автомата к эквивалентной по поведению синхронной модели секвенциального автомата основывается на сложных методах кодирования состояний параллельного автомата с нахождением параллельных состояний. Такие методы подробно описаны в [9, 10], три из таких методов программно реализованы в QPralu, основное их различие – длина получаемого кода состояний автомата. В примере (табл. 7) для кодирования тринадцати частичных состояний потребовалось шесть кодирующих переменных Z0,…, Z5. В аналитической форме секвенциальный автомат (табл. 7) задается формулами

VHDL-модель секвенциального автомата в целом аналогична VHDL-модели параллельного автомата, например, первая секвенция $u{{z}_{0}}{{z}_{1}}{{z}_{2}}$ ├ ${{\bar {z}}_{0}}ab,$ описывается следующим фрагментом VHDL-кода:

Результаты схемной реализации VHDL-моделей параллельных и секвенциальных автоматов в библиотеке проектирования заказных КМОП СБИС, выполненные в синтезаторе LeonardoSpectrum даны в табл. 8.

Первые три примера Zak178, Zak135, Pott1, Wagon взяты из [9, 10], Kamkin_2 – пример параллельной сети из двух узлов (конечных автоматов), рассматриваемый в [16]. Параметры схемной реализации VHDL-моделей: S – площадь в условных единицах; L – общее число элементов (комбинационных и элементов памяти – триггеров); Tr – число триггеров; $\tau $ – задержка (нс).

Результаты схемной реализации, приведенные в табл. 8, показывают, что реализация VHDL-моделей секвенциальных автоматов чаще дает схемы меньшей сложности, однако схемные реализации VHDL-моделей параллельных автоматов являются более быстродействующими, все зависит от вида автомата – числа входов, выходов, цепочек и распределения подмножеств меток по цепочкам.

Программный инструментарий для моделирования ПРАЛУ-описаний параллельных автоматов разработан на языке программирования C++ в среде QT [15]. Разработанная программа QPralu позволяет провести моделирование параллельных автоматов, выполнить проверку их семантических свойств, получить секвенциальные автоматы и синтезируемые VHDL-модели автоматов.

ЗАКЛЮЧЕНИЕ

Более половины времени и других ресурсов при разработке проектов цифровых систем расходуется на верификацию, поэтому использование компактных, ясных ПРАЛУ-описаний алгоритмов логического управления позволяет более эффективно провести их запись и последующую верификацию. Преобразование модели параллельного автомата в модель секвенциального автомата позволяет уменьшать сложность логических схем при схемной реализации VHDL-моделей автоматов. Предложенный в данной статье подход в целом повышает эффективность проектирования и может сократить сроки разработки проектов цифровых систем, реализующих параллельные алгоритмы логического управления, характеризуемые большим числом состояний и управляющих сигналов.