RTL2GDS: Проверка логического эквивалента, LEC

Перед выпуском в производство RTL проходит множество инструментов EDA. Может ли этот процесс быть полностью свободным от ошибок? Что, если ошибка в инструменте добавила лишний инвертор?

Формальная верификация, а именно проверка логической эквивалентности (LEC), является важной методологией в современном процессе проектирования ASIC.

В отличие от симуляции, LEC не использует тестовые векторы. Вместо этого она представляет собой методологию, которая выполняет статический анализ, чтобы гарантировать, что два представления проекта демонстрируют идентичное поведение с математической и логической точки зрения во всех возможных случаях. Основная цель LEC — проверка целостности в процессе преобразования проекта. Она проверяет, что первоначальное намерение проектировщика (золотой дизайн) полностью сохраняется в модифицированном дизайне (пересмотренном дизайне), когда: - код RTL (Register Transfer Level) преобразуется в список цепей на уровне вентилей посредством логического синтеза; - инструменты P&R модифицируют логику для оптимизации временных характеристик; - или сканирующие цепочки вставляются в процессе DFT (Design for Testability).



Как видно на приведенном выше диаграмме, LEC выполняется итеративно на различных этапах: RTL по сравнению с синтезированным списком сетей, синтезированный список сетей по сравнению с DFT-списком сетей и окончательная проверка списка сетей макета.

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

Чтобы понять, что означает «математическое доказательство» для LEC, необходимо рассмотреть лежащие в его основе алгоритмические принципы. Инструменты LEC работают в основном на основе двух основных технологий: бинарных диаграмм решений (BDD) и булевой удовлетворимости (SAT).2.1 Конфигурация схемы Miter и верификация на основе опровержения

Основной принцип LEC заключается в сравнении двух схем (эталонной и тестовой) с целью выявления «хотя бы одного случая», когда их выходы различаются. Для этого инструмент создает виртуальную схему Miter. Структура схемы Miter соединяет идентичные входные порты двух схем и связывает соответствующие выходные порты через XOR-врата.

Логически, XOR-вход выдает «1» только в том случае, если его два входа различаются. Таким образом, цель инструментов LEC сводится к ответу на вопрос: «Существует ли комбинация входов, при которой вентиль XOR выдает «1»?».Если такая комбинация входов (контрпример) существует, две схемы неэквивалентны.Если выход XOR всегда равен «0» для всех возможных входов, две схемы эквивалентны.

Этот подход основан на контрфактуальном мышлении, согласно которому «поиск различий» может быть алгоритмически более эффективным, чем «доказательство эквивалентности».2.2 Бинарные диаграммы решений, BDD

BDD, которые легли в основу ранних инструментов LEC, представляют собой структуру данных, отображающую булевы выражения в виде направленного ациклического графа (DAG). Самая мощная особенность BDD — это их каноническая форма.

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

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

Однако BDD имеют серьезный недостаток: проблему взрыва памяти. Для определенных арифметических схем, таких как умножитель, или сложной логики с многочисленными входными переменными, количество узлов BDD увеличивается экспоненциально, превышая физические ограничения памяти. В результате верификация на основе BDD показала свои ограничения при обработке крупномасштабных проектов SoC.2.3 Решатель удовлетворимости (SAT)

Решатель SAT — это технология, внедренная для преодоления ограничений BDD. SAT — это алгоритм, который ищет присвоение переменной, которое делает заданное булево выражение (в основном CNF, конъюнктивная нормальная форма) истинным. В отличие от BDD, SAT не пытается хранить всю таблицу истинности в сжатом виде. Вместо этого он использует методы поиска в глубину (DFS), обратного прослеживания и обучения для нахождения решения.Преимущества: значительно меньшее использование памяти по сравнению с BDD и эффективная работа даже с крупномасштабными схемами. Особенно быстрый поиск контрпримеров.Недостатки: для некоторых задач пространство поиска может быть чрезмерно большим, что приводит к очень длительному времени решения (NP-полные задачи). В результате современные инструменты LEC используют гибридный подход, либо комбинируя BDD и SAT, либо автоматически выбирая подходящий движок на основе структуры схемы.2.4 Разбиение на логические конусы

Решение всего чипа как одного огромного булева уравнения невозможно. В результате инструменты LEC разбивают проект на более мелкие единицы, называемые логическими конусами, для верификации.p>Сравнительные точки (ключевые точки): Это элементы, которые служат ориентиром для проверки. В первую очередь к ним относятся первичный выход, входы триггера (D-контакт) и контакты входа черного ящика.Формирование логического конуса: Каждая точка сравнения обозначается как вершина. Определяется область комбинационной логики, причем все первичные входы, выходы триггера (Q-pin) и выходы черного ящика, влияющие на эту точку, служат в качестве основания.

LEC отображает дизайны Golden и Revised в соотношении 1:1 с использованием этих единиц логического конуса, а затем независимо проверяет, что каждая пара эквивалентна. Это решает общую сложность задачи с помощью подхода «разделяй и властвуй».3. Подробные этапы процесса верификации LEC

При использовании таких инструментов, как Synopsys Formality или Cadence Conformal LEC, в реальных промышленных условиях процесс верификации обычно состоит из четырех этапов: Настройка, Сопоставление, Сравнение и отладки. Каждый этап включает в себя важные подробные задачи, обеспечивающие надежность верификации.3.1 Шаг 1: Моделирование дизайна, настройка - Создание среды верификации

Этап настройки включает в себя загрузку двух сравниваемых проектов (эталонного/золотого и реализованного/переработанного) в инструмент и настройку правильной среды верификации. Незначительные ошибки на этом этапе могут привести к значительным затратам на отладку в дальнейшем, поэтому требуется максимальная тщательность.Загрузка библиотеки: загрузите библиотеку стандартных ячеек, библиотеку I/O-контактов и модели «черного ящика», такие как память или аналоговый IP.Synopsys Formality в основном использует формат .db (Synopsys Liberty Binary).Cadence Conformal поддерживает как .lib (Liberty), так и модели Verilog для симуляции (.v). Важно, что оба проекта должны ссылаться на библиотеки с идентичными функциональными определениями.Читаемый проект:Золотой проект: проект, служащий в качестве эталона для верификации. В основном состоит из кода RTL (Verilog, VHDL, SystemVerilog). При чтении RTL процесс elaborate финализирует параметры и генерирует иерархию.Пересмотренный проект: Это проект, который сравнивается. Это список сетей, сгенерированный после синтеза, или список сетей после P&R.Настройка ограничений: Это рекомендации, помогающие инструменту LEC правильно интерпретировать проект.Установить константу: Список цепей содержит логику сканирующей цепи для тестирования, что делает его структурно отличным от RTL. Поэтому сигнал Scan Enable должен быть зафиксирован на 0 (или его неактивном значении), чтобы заставить инструмент проверять только функциональный путь, а не путь сканирования.Обработка неактивированных сигналов: Определите, должны ли плавающие входы (порты без подключенных входов) интерпретироваться как «0», «1», «Z» (High-Z) или «X» (Don't Care). Неправильная конфигурация может привести к ненужным расхождениям.3.2 Шаг 2: Сопоставление проектов — связывание сравнений-Design">3.2 Шаг 2: Сопоставление конструкций — связывание целей сравнения

Сопоставление — это процесс установления соответствия 1:1 между ключевыми точками сравнения «золотой» конструкции и точками сравнения переработанной конструкции. Для инструментальной цепочки Synopsys этот процесс упрощает файл SVF.Сопоставление по имени: используется, когда имена регистров или портов идентичны или следуют регулярному шаблону. Инструмент в первую очередь пытается сопоставить имена.Сопоставление на основе функций: даже если имена изменились (например, когда инструменты синтеза произвольно переименовывают компоненты во время оптимизации или когда триггер шины данных подвергается банковской операции или дебанковской операции, чтобы стать многоразрядным триггером), сопоставление осуществляется путем анализа схожести логической функции (логического конуса), управляющей портом. Это требует больших вычислительных затрат, но необходимо для проверки списков сетей, в которых нарушены правила именования. Например, если RTL reg изменяется на reg_0_ в списке соединений, инструменту можно дать указание выполнить сопоставление, заменив `` на _.Анализ несопоставленных точек: Несопоставленные точки исключаются из сравнения. Крайне важно проверить, является ли это намеренным (например, удаление неиспользуемой логики) или ошибкой (например, пропуск правила переименования).Именно здесь возникают списки несоответствий. Не только LEC Fails, но и списки несоответствий требуют анализа со стороны верификатора.3.3 Шаг 3: Сравнение проектов

Сопоставленные точки проходят проверку LEC. Инструмент использует многоэтапную стратегию для максимальной эффективности.Симмуляция случайных паттернов: сначала вводятся тысячи случайных входных паттернов для быстрого сравнения выходных значений. Если на этом этапе происходит несоответствие, оно немедленно оценивается как неэквивалентное, что позволяет сэкономить дорогостоящие ресурсы решателя.Структурный анализ и формальная верификация: для точек, прошедших тест случайных шаблонов, активируется SAT или BDD Solver для попытки формального доказательства.

Результаты классифицируются по следующим четырем типам:Эквивалентность: вывод одинаков для всех комбинаций входных данных (верификация успешна).Неэквивалентность: вывод отличается для конкретного входа (проблема настройки или функциональная ошибка).Инвертированный эквивалент: Выходные данные являются точными противоположностями (например, отображение Q и Qbar). Это может быть функционально эквивалентно (если разрешена инверсия фазы), но требует тщательной проверки.Прерывание / Неокончательный результат: Инструмент не может завершить проверку в заданные сроки или в пределах ограничений памяти. Это в основном происходит в схемах с большими умножителями или другими арифметическими логическими элементами, а также в схемах с очень большой глубиной логики.3.4 Шаг 4: Отладка — анализ первопричин и устранение неполадок

Если результат сравнения является неэквивалентным или происходит прерывание, процесс переходит в стадию отладки. Это стадия, на которой наиболее востребованы навыки инженера LEC. Короче говоря, если LEC не работает, отладка становится действительно сложной задачей.Диагностика: сгенерируйте контрпример, вызывающий несоответствие, и обратный трассировку, чтобы определить, какой вход в логическом конусе является потенциальной ошибкой.Анализ шаблонов: Визуально проанализируйте распространение сигнала до точки несоответствия с помощью просмотрщика сигналов или просмотрщика схем инструмента. Пользователи сравнивают исходный код RTL и схему сетевого списка для выявления логических несоответствий.strong> и выявить несоответствия.4. Оптимизация синтеза и структурные преобразования

Самая большая проблема при верификации LEC заключается в том, что RTL и netlist имеют очень разную структуру. Инструменты логического синтеза (такие как Design Compiler и Genus) значительно преобразуют логическую структуру RTL для оптимизации площади, мощности и синхронизации. Если инструмент LEC не понимает эти структурные преобразования, он может неправильно оценить проект как несоответствующий (ложное отрицание), несмотря на идентичную функциональность.4.1 Оптимизация комбинационной логики (Оптимизация комбинационной логики)

Наиболее фундаментальной оптимизацией является упрощение логики с использованием законов булевой алгебры.Распространение констант: если определенный вход фиксируется как константа, связанная с ним логика удаляется или упрощается. Инструменты LEC также могут распознать это как ошибку, если они не знают об идентичном ограничении константы.Репликация и слияние логики: вентили с большим разветвлением реплицируются для решения проблем синхронизации или, наоборот, идентичная логика сливаются для уменьшения площади. Инструменты LEC должны обрабатывать эти сопоставления «многие к одному» (N:1) или «один ко многим» (1:N).4.-%EB%85%BC%EB%A6%AC-%EC%B5%9C%EC%A0%81%ED%99%94-sequential-logic-optimization">4.2 Последовательная оптимизация логики

Оптимизация, которая изменяет не только комбинационную логику, но и сами регистры (триггеры), затрудняет верификацию.Пересинхронизация: Пересинхронизация — это техника, при которой регистры физически перемещаются на противоположную сторону комбинационной логики, чтобы уменьшить время задержки на критическом пути. В этом случае расположение регистров в RTL отличается от расположения в списке сетей.(критический путь) путем физического перемещения регистров по комбинационной логике. Это приводит к тому, что положения регистров в RTL отличаются от положений в списке сетей, что делает невозможным отображение 1:1.Решение: Файл проверки настройки (SVF) или файл-руководство, сгенерированный инструментом синтеза, имеет важное значение. Этот файл содержит информацию, описывающую, что «регистр RTL A переместился в регистр netlist B», что позволяет инструменту LEC ссылаться на это и сбрасывать точки сравнения.Более подробную информацию можно найти в руководстве по автоматическому файлу настройки (SVF) Formality®.Однако SVF часто содержат ошибки. Следовательно, использование SVF может привести к сбою, а его отсутствие — к успеху.Оптимизация регистров конвейераПерекодирование FSM4.3 Изменения иерархии

Иерархия проектирования также подлежит оптимизации. Инструменты синтеза часто разрушают границы подмодулей (разгруппировка) и объединяют их с родительскими модулями, чтобы уплостить иерархию, повышая эффективность оптимизации.Проблема: Когда границы модулей исчезают, иерархические сравнения становятся невозможными. Для сравнения необходимо уплостить весь проект, что приводит к резкому увеличению времени верификации. Кроме того, изменения имен, такие как submodule/reg на submodule_reg, приводят к сбоям в сопоставлении.Решение: Использовать функцию автоматического сопоставления имен или для критически важных модулей применять атрибут set_ungroup false во время синтеза, чтобы сохранить иерархическую структуру.

Оптимизация границ: эта техника включает перемещение логики через границы модулей (например, вынесение инвертора за пределы модуля) или распространение констант из входных портов внутри модуля. Это также приводит к несоответствиям на граничных контактах во время иерархического сравнения, поэтому в настройках LEC должны быть включены такие опции, как set flatten model -boundary_optimisation.LEC с UPF для проектирования с низким энергопотреблениемПрименение технологий низкого энергопотребления имеет важное значение в современном проектировании мобильных устройств и чипов для Интернета вещей. Внедрение технологий Multi-Voltage Domain и Power Gating добавляет новую сложность к верификации LEC.

5.1 UPF/CPF и Power Intent

Сам код RTL не содержит информации о сети питания. Такие детали, как домены питания, изоляция и сдвигатели уровня, определяются в отдельных файлах: UPF (Unified Power Format) или CPF (Common Power Format).Во время верификации LEC эти файлы UPF/CPF должны быть загружены вместе с RTL. Инструмент использует эту информацию для вставки виртуальной логики питания в модель RTL, создавая список сетей, сопоставимый с тем, который содержит реальные устройства питания.

6. ECO (заказ на инженерные изменения) и LEC

На поздних этапах проектирования микросхем, особенно когда ошибки обнаруживаются непосредственно перед P&R или изготовлением маски, выполняется FECO (Functional Engineering Change Order, функциональное изменение проекта). Это предполагает изменение только минимального количества вентилей, а не повторное выполнение всего синтеза. Инструменты LEC также играют важную роль в процессе ECO.

• Функциональный ECO: этот процесс включает в себя модификацию RTL, а затем применение минимальных патчей к существующему списку сетей, чтобы сделать его идентичным модифицированному RTL. Такие инструменты, как Conformal ECO, сравнивают измененный RTL с существующим списком сетей и автоматически генерируют необходимую логику исправления для устранения различий.
• Использование запасных ячеек ECO: Если выпуск уже завершен и процесс FEOL закончен, ошибка должна быть исправлена с помощью запасных вентилей(Spare Cells), предварительно распределенные внутри чипа, и модифицируют металлический слой BEOL для исправления ошибки. Инструменты LEC могут сгенерировать оптимальный патч-нетлист, используя их, путем ввода списка доступных запасных ячеек.-%EB%AC%B4%EA%B2%B0%EC%A0%90-%EC%84%A4%EA%B3%84%EB%A5%BC-%EC%9C%84%ED%95%9C-%EC%B5%9C%ED%9B%84%EC%9D%98-Заключение: последний бастион безупречного проектированияLEC выходит за рамки простого выполнения инструмента; это строгая инженерная процедура, которая математически гарантирует целостность проекта. На протяжении длительного процесса проектирования от RTL до ворот и, в конечном итоге, до окончательной компоновки, происходит множество оптимизаций и структурных преобразований. Тем не менее, LEC остается последним бастионом в его основе, гарантируя, что функциональная сущность остается неизменной. Для успешной работы LEC необходимо понимание формальных теорий верификации, таких как BDD/SAT, глубокое знание процессов синтеза и преобразования DFT, Необходимы также систематическая методология отладки. По мере увеличения размеров проектирования и усложнения вычислительной логики, как это видно на примере полупроводников для искусственного интеллекта, важность таких передовых технологий, как иерархическая верификация, проверка эквивалентности последовательной логики (SLEC) и параллельная верификация на основе облачных технологий, будет только расти. Для инженеров по верификации LEC больше не является опцией, а является необходимым навыком для выживания.