Проверки согласованности памяти при RTL. Инновации в проверке

Многоядерные системы, работающие с общей памятью, должны поддерживать четко определенную модель согласованности доступа потоков к этой памяти. Существует несколько возможных моделей согласованности. Может ли группа разработчиков выполнять проверки согласованности памяти в RTL? Пол Каннингем (GM, Verification at Cadence), Рауль Кампосано (Silicon Catalyst, предприниматель, бывший технический директор Synopsys) и я продолжаем нашу серию статей об исследовательских идеях. Как всегда, отзывы приветствуются.

Инновация

Выбор в этом месяце RTLCheck: проверка согласованности памяти проектов RTL. Статья была опубликована в журнале IEEE/ACM MICRO за 2017 год. Авторы из Принстона и NVIDIA.

Согласованность памяти — это соглашение между разработчиками аппаратного и программного обеспечения об упорядочении операций чтения и записи в многоядерной системе. Если два или более потока могут загружаться из логической области памяти или сохраняться в ней, при отсутствии необходимой синхронизации между ядрами и оптимизаций, таких как выполнение не по порядку, некоторые заказы могут быть разрешены, а некоторые — нет. Существует несколько возможных способов определения таких правил. Согласованный набор правил, ограничивающих это поведение, определяет модель согласованности памяти (MCM). RTLCheck — это вклад авторов в автоматическую проверку того, что дизайн RTL соответствует набору (модифицированных) определяемых пользователем аксиом, кодирующих MCM.

Метод обнаруживает нарушения аксиомы как циклы в графах «происходит до» (hb) тестовых случаев, разработанных как операции выборки-декодирования/выполнения-обратной записи между ядрами. Одна из таких лакмусовых бумажек проверяет передачу сообщений между ядрами. Поскольку дуги в hb-графе обозначают разрешенный порядок операций, цикл в hb-графе подразумевает последовательность операций, которые должны завершиться до их начала, что невозможно. Аксиомы, используемые для доказательства работы MCM с абстрактными архитектурными спецификациями. Механизмы временных доказательств, используемые в формальных методах для RTL, не обладают такой гибкостью (согласно авторам), поэтому аксиомы «синтезируются» в соответствии с отраслевыми стандартами System Verilog Assertions (SVA) и ограничениями с некоторыми ограничениями на то, что может быть отображено.

Взгляд Павла

Проверка согласованности памяти в многопроцессорных (MP) системах сложна, и я всегда сторонник повышения уровня абстракции как важного способа решения сложных проблем проверки. Основная предпосылка статьи — скомпилировать аксиомы MCM высокого уровня микроархитектуры в SVA — отличная идея, а графы «происходит до», используемые в этих аксиомах, — элегантный и интуитивно понятный способ выразить намерения MCM.

Документ тщательный, и всегда приятно видеть совместные исследования между академическими кругами и промышленностью. Авторы четко описывают свой подход и предоставляют полностью проработанный пример ядра RISC-V с открытым исходным кодом, в котором они нашли реальную ошибку, используя свои методы. Хотя, как указывают авторы, баг есть баг даже для единичного экземпляра ядра RISC-V. Сигнал «готовности» памяти был случайно привязан к высокому уровню, поэтому память всегда готова принять новое значение.

Я действительно задаюсь вопросом, насколько проще авторские аксиоматические спецификации в формате инструмента «Проверка», чем их синтезированные стандартные эквиваленты SVA. Отображение 1-1, просто более подробное в формате SVA. Например, одно ключевое наблюдение в статье состоит в том, что SVA для «A подразумевает, что B происходит позже» (A |-> ##[1:$] B) может соответствовать случаю, когда A происходит несколько раз до B, где hb- аксиоматического эквивалента графа не было бы — представьте, что A — это «хранимое значение x», а B — «загружаемое значение x». Промежуточное «сохранение значения y», очевидно, сделало бы аксиому недействительной. Синтез дополнительного синтаксиса SVA для предотвращения нескольких A перед B является одним из вкладов в статью (A |-> ##[0:$]!A ##1 B), но этот вклад больше похож на синтаксическое подслащивание, чем на фундаментальное поднятие уровень абстракции.

В целом, плотная статья, хорошо написанная и на важную тему. Кроме того, приятно видеть, что автор использует формальный инструмент Cadence Jasper для проверки своих синтезированных SVA. И найдите этот баг RISC-V 😃

Взгляд Рауля

Для заинтересованного читателя статья объясняет аксиоматические микроархитектурные модели в 𝜇spec (логика первого порядка). Вместе с соответствующими графами 𝜇hb (происходит до) и темпоральными утверждениями. Они проходят небольшой мотивирующий пример с двумя ядрами. Каждый запускает небольшую общую лакмусовую бумажку «передачи сообщений» из 2 инструкций в каждом ядре, которой легко следовать. Фактическая генерация временных утверждений довольно сложна и включает в себя дополнительные неавтоматические действия пользователя:

• сопоставление инструкций и значений программы лакмусовой бумажки с выражениями RTL
• сопоставление узлов графа 𝜇hb с выражениями Verilog

Для этого требуется «пользователь» с глубокими знаниями в данной области, т. е. аксиоматические спецификации, 𝜇spec, SVA, RTL и т. д. Разработчики параллельных архитектур, работающие с экспертами по верификации и имеющие доступ к JasperGold и набору проверок [33], потенциально могут извлечь выгоду из использования RTLCheck. .

Результаты хорошие: для 4-ядерного RISC-V 89% сгенерированных утверждений для 56 лакмусовых тестов полностью подтверждены. Остальные 11% завершены с ограниченными доказательствами. К ним относятся обнаружение реальной ошибки в процессоре Multi-V и ее исправление.

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

Мой взгляд

Я надеялся, что это будет аккуратный боковой способ проверки когерентности. Но Пол и Рауль отговорили меня от этого. Опыт и усилия, необходимые для установки аксиом и ограничений для управления формальным анализом на современной SoC, кажутся обескураживающими. Я надеюсь, что основная концепция все еще может иметь ценность. Возможно, при применении (каким-то образом) в приложении для моделирования.

Поделитесь этим постом через: Источник: https://semiwiki.com/eda/304308-memory-consistency-checks-at-rtl-innovation-in-verification/