Есть ли «стандартный» способ проверки HDL конечного автомата?

Конечные автоматы — это шаблон, который очень часто используется при написании синхронных проектов. Они служат контроллерами в конструкции. Итак, есть ли стандартный способ проверить их, если они написаны с использованием VHDL или Verilog/SystemVerilog? Или лучше использовать некоторый графический интерфейс для их рисования, а затем вместо этого генерировать код из графического интерфейса?

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

Дело в том, что конечные автоматы могут быть довольно большими, и придется писать код для проверки каждой ветки в конечном автомате, что приводит к большому количеству кода в тестовом стенде.

Редактировать: я занимаюсь только самостоятельной проверкой самого fsm, чтобы убедиться, что он соответствует диаграмме состояний fsm и не существует ошибок в кодировании rtl.

Мне любопытно посмотреть, что другие говорят об этом. Я написал много автоматов состояний, но нет, у меня нет стандартного процесса проверки. Для меня написание HDL для реализации данного проекта конечного автомата на самом деле не является сложной частью — трудная часть заключается в том, чтобы убедиться, что дизайн самого конечного автомата имеет поведение , требуемое приложением, при всех возможных входных комбинациях.
Я подумал, что если для этого существует специальный инструмент с графическим интерфейсом и мы его используем, мы можем считать само собой разумеющимся, что код правильный, пока верна диаграмма конечного автомата. Как вы указали, написание всего этого кода тестового стенда для проверки всех возможных маршрутов, которые должен пройти конечный автомат, раздражает даже для простых конечных автоматов. Основная проблема, если я понимаю, что конечный автомат нужно изменить, а затем код должен быть переписан или изменен. Это утомительно.
По сути, некоторое время назад я прошел курс комплексного VHDL от Doulos в Великобритании. Это был фантастический курс. В нем также учили, как писать конечный автомат на VHDL, идея заключалась в том, чтобы отделить синхронные процессы, которые присваивают следующее состояние текущему состоянию, от асинхронного (не тактового) процесса, который генерирует значение для следующего состояния из текущего состояния и текущих входных данных. . Это было очень интересно, так как избавляло от многих ловушек в конструкции конечного автомата. Однако, хотя они касались исключительно проектирования конечного автомата, это не относится к проверке конечного автомата.
Stateflow от MathWorks — это инструмент с графическим интерфейсом для кодирования конечных автоматов.
@quantum231 Модель ModelSim от Mentor Graphics также определяет покрытие конечного автомата, которое используется для покрытия состояний и переходов состояний. Смотрите мой ответ для более подробной информации.
Да, единый подход к проверке FSM можно найти по этой ссылке: verificationacademy.com/verification-horizons/…
Лучший способ - сделать формальную проверку! Я обновил свой ответ после того, как попробовал сам. Больше не нужно беспокоиться об этом угловом случае!
Хорошо, Шашанк бхай. Я попытался прочитать о том, как на самом деле сделать формальную проверку. Я столкнулся с концепцией использования свойства и утверждения (SVA или PSL). Я нашел упоминание о проверке логической эквивалентности. Я также нашел упоминание о проверке модели. Я наткнулся на название программы под названием Jasper. Однако во всем этом я не смог найти ничего, что говорило бы мне о том, как я сам могу провести формальную проверку моего проекта. Я бы хотел, чтобы формальный преподавался и на университетском уровне.

Ответы (2)

Проверка — огромная часть процесса проектирования; в сложном проекте не было бы ничего необычного в том, чтобы потратить на проверку столько же или даже больше времени, сколько вы тратите на сам проект. В таком случае вопрос, который, по сути, сводится к тому, «как вы проверяете сложные проекты», довольно широк.

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

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

Существует ряд методологий, которые пытаются помочь управлять процессом создания стимула и записи результатов. Я использую OSVVM , о которой узнал из курса пару лет назад. Мне это нравится, потому что он использует тот же язык VHDL, к которому я привык, вместе с небольшим количеством сценариев TCL и не требует никаких «дополнительных услуг» для работы с моим симулятором. Есть много альтернатив, которые я не буду здесь перечислять, но быстрый поиск в Google по запросу «проверка fpga» выдает много ресурсов.

Я имел в виду только тестирование конечного автомата самостоятельно, чтобы его поведение соответствовало диаграмме состояний fsm
Лучший способ проверить это как часть системы, которую он контролирует. Если вы тестируете его изолированно, вы рискуете не дать ему того же стимула, который он получает в реальной системе. В любом случае вам нужно создать тестовый стенд для системы в целом , так что вы можете сделать один тестовый стенд, который сделает все это.

Я рекомендую использовать формальные методы проверки.

Напишите 2 набора утверждений:

  1. Утверждения для проверки того, что каждый переход состояния происходит при правильном условии.
  2. Утверждения для проверки каждого выходного перехода только в предполагаемом состоянии.

Иногда вы можете написать одно утверждение для проверки всей функциональности FSM, как я сделал здесь: https://electronics.stackexchange.com/a/505842/238188 .

Для небольших FSM нарисуйте их в графическом интерфейсе и сгенерируйте HDL-код или сгенерируйте диаграмму перехода состояний из HDL-кода и проверьте диаграмму.

Я знаю 2 решения для этих 2 случаев:

  1. StateFlow от MathWorks может генерировать HDL-код из диаграммы конечного автомата.
  2. ModelSim от Mentor Graphics имеет встроенную программу просмотра FSM для просмотра конечного автомата, сгенерированного из HDL.