Проверка функциональной эквивалентности на этапах проектирования электронных схем

Введение

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

Проверка эквивалентности и уровни абстрагирования

В целом, существует широкий спектр возможных определений функциональной эквивалентности, охватывающих сравнения между различными уровнями абстракции и различной детализацией временных характеристик. Наиболее распространенным подходом является рассмотрение задачи эквивалентности машин, которая определяет две синхронные конструкторские спецификации функционально эквивалентными, если, такт за тактом, они генерируют абсолютно идентичную последовательность выходных сигналов для любой допустимой последовательности входных сигналов. Разработчики микропроцессоров используют проверку эквивалентности для сравнения функций, определенных для архитектуры набора команд (ISA), с реализацией на уровне передачи регистров (RTL), обеспечивая, чтобы любая программа, выполняемая на обеих моделях, вызывала идентичное обновление содержимого основной памяти. Это более общая задача. Процесс проектирования системы требует сравнения модели уровня транзакций (TLM), например, написанной на SystemC, с соответствующей спецификацией RTL. Такая проверка приобретает все большую актуальность в среде разработки систем на кристалле (SoC).

Эквивалентность синхронных машин

Поведение на уровне передачи регистров (RTL) цифровой микросхемы обычно описывается с помощью языка описания аппаратуры, такого как Verilog или VHDL. Это описание является золотой эталонной моделью, которая детально описывает, какие операции будут выполнены в течение какого тактового цикла и какими аппаратными блоками. После того, как разработчики логики, посредством моделирования и других методов верификации, подтвердили описание передачи регистров, схема обычно преобразуется в сетевой список (netlist) с помощью инструмента логического синтеза. Эквивалентность не следует путать с функциональной корректностью, которая должна быть установлена посредством функциональной верификации. Исходный сетевой список обычно подвергается ряду преобразований, таких как оптимизация, добавление структур для обеспечения тестируемости (DFT) и т.д., прежде чем он будет использован в качестве основы для размещения логических элементов в физической компоновке. Современное программное обеспечение для физического проектирования иногда также вносит существенные изменения (например, заменяет логические элементы эквивалентными, но с другой мощностью драйвера и/или площадью) в сетевой список. На каждом этапе очень сложной многоступенчатой процедуры исходная функциональность и поведение, описанное исходным кодом, должны быть сохранены. К моменту изготовления окончательной фотошаблона цифровой микросхемы, множество различных EDA-программ и, возможно, ручные правки изменяют сетевой список. В теории, инструмент логического синтеза гарантирует, что первый сетевой список логически эквивалентен исходному коду RTL. Все программы, которые впоследствии в процессе вносят изменения в сетевой список, также, в теории, обеспечивают, чтобы эти изменения были логически эквивалентны предыдущей версии. На практике программы содержат ошибки, и было бы серьезным риском предполагать, что все этапы от RTL до окончательного сетевого списка фотошаблона выполнены без ошибок. Кроме того, в реальной жизни дизайнеры часто вносят ручные изменения в сетевой список, обычно известные как Engineering Change Orders (ECO), тем самым внося дополнительный фактор ошибок. Поэтому, вместо того чтобы слепо полагаться на отсутствие ошибок, необходим этап верификации для проверки логической эквивалентности окончательной версии сетевого списка исходному описанию схемы (золотой эталонной модели). Исторически одним из способов проверки эквивалентности было повторное моделирование, с использованием окончательного сетевого списка, тестовых случаев, разработанных для верификации корректности RTL. Этот процесс называется логическим моделированием на уровне элементов (gate-level logic simulation). Однако проблема в том, что качество проверки не выше качества тестовых случаев. Кроме того, моделирование на уровне элементов печально известно своей низкой скоростью выполнения, что является серьезной проблемой, поскольку размер цифровых схем продолжает экспоненциально расти. Альтернативным решением является формальное доказательство того, что код RTL и синтезированный из него сетевой список имеют абсолютно одинаковое поведение во всех (релевантных) случаях. Этот процесс называется формальной проверкой эквивалентности и является задачей, изучаемой в более широкой области формальной верификации. Формальная проверка эквивалентности может быть выполнена между любыми двумя представлениями схемы: RTL ↔ netlist, netlist ↔ netlist или RTL ↔ RTL, хотя последний случай встречается редко по сравнению с первыми двумя. Как правило, инструмент формальной проверки эквивалентности также с высокой точностью указывает, в какой точке существует различие между двумя представлениями.

The register transfer level (RTL) behavior of a digital chip is usually described with a hardware description language, such as Verilog or VHDL. This description is the golden reference model that describes in detail which operations will be executed during which clock cycle and by which pieces of hardware. Once the logic designers, by simulations and other verification methods, have verified register transfer description, the design is usually converted into a netlist by a logic synthesis tool. Equivalence is not to be confused with functional correctness, which must be determined by functional verification. The initial netlist will usually undergo a number of transformations such as optimization, addition of Design For Test (DFT) structures, etc., before it is used as the basis for the placement of the logic elements into a physical layout. Contemporary physical design software will occasionally also make significant modifications (such as replacing logic elements with equivalent similar elements that have a higher or lower drive strength and/or area) to the netlist. Throughout every step of a very complex, multi step procedure, the original functionality and the behavior described by the original code must be maintained. When the final tape out is made of a digital chip, many different EDA programs and possibly some manual edits will have altered the netlist. In theory, a logic synthesis tool guarantees that the first netlist is logically equivalent to the RTL source code. All the programs later in the process that make changes to the netlist also, in theory, ensure that these changes are logically equivalent to a previous version. In practice, programs have bugs and it would be a major risk to assume that all steps from RTL through the final tape out netlist have been performed without error. Also, in real life, it is common for designers to make manual changes to a netlist, commonly known as Engineering Change Orders, or ECOs, thereby introducing a major additional error factor. Therefore, instead of blindly assuming that no mistakes were made, a verification step is needed to check the logical equivalence of the final version of the netlist to the original description of the design (golden reference model). Historically, one way to check the equivalence was to re simulate, using the final netlist, the test cases that were developed for verifying the correctness of the RTL. This process is called gate level logic simulation. However, the problem with this is that the quality of the check is only as good as the quality of the test cases. Also, gate level simulations are notoriously slow to execute, which is a major problem as the size of digital designs continues to grow exponentially. An alternative way to solve this is to formally prove that the RTL code and the netlist synthesized from it have exactly the same behavior in all (relevant) cases. This process is called formal equivalence checking and is a problem that is studied under the broader area of formal verification. A formal equivalence check can be performed between any two representations of a design: RTL <> netlist, netlist <> netlist or RTL <> RTL, though the latter is rare compared to the first two. Typically, a formal equivalence checking tool will also indicate with great precision at which point there exists a difference between two representations.

Обобщения

Проверка эквивалентности ретаймированных схем: Иногда полезно перемещать логику с одной стороны регистра на другую, что усложняет задачу проверки. Проверка последовательной эквивалентности: Иногда две машины совершенно различны на комбинационном уровне, но должны выдавать одинаковые выходные сигналы при одинаковых входных сигналах. Классическим примером являются две идентичные машины состояний с разными кодировками состояний. Поскольку эту задачу нельзя свести к комбинационной, требуются более общие методы. Эквивалентность программ, то есть проверка того, эквивалентны ли две чётко определённые программы, принимающие N входов и выдающие M выходов: концептуально, программное обеспечение можно представить в виде машины состояний (именно это делает комбинация компилятора, поскольку компьютер вместе с его памятью образуют очень большую машину состояний). Тогда, теоретически, различные методы проверки свойств могут гарантировать, что они выдают одинаковые результаты. Эта задача ещё сложнее, чем проверка последовательной эквивалентности, поскольку выходные данные двух программ могут появляться в разное время, но она решаема, и исследователи над ней работают.