Сингх Э., Девараржеговда К., Саймоно С., Шнайдер Р., Ганешан К., Фадиех М., Штоффель Д., Кунц В., Баррет К., Экер В., Митра С. Символьная QED-проверка ошибок для предкристаллической верификации автомобильных микроконтроллерных ядер: промышленное исследование. В статье представлено промышленное исследование, демонстрирующее практичность и эффективность метода символьной быстрой проверки ошибок (Symbolic QED) для обнаружения логических ошибок при предкристаллической верификации. Исследование сфокусировано на нескольких ядрах микроконтроллеров (около 1800 триггеров, 70 000 логических элементов), которые прошли тщательную верификацию с использованием промышленного процесса и применяются в различных автомобильных продуктах. Результаты исследования показывают, что: 1) Symbolic QED обнаружил все логические ошибки, которые были выявлены промышленным верификационным процессом (включающим симуляции и формальную верификацию); 2) Symbolic QED выявил дополнительные ошибки, не зарегистрированные в промышленном процессе; 3) Symbolic QED обеспечивает значительное повышение производительности проектирования: 8-кратное сокращение верификационных усилий для новой конструкции (8 человеко-недель против 17 человеко-месяцев), 60-кратное сокращение для последующих конструкций (2 человеко-дня против 4-7 человеко-месяцев), быстрое обнаружение ошибок (время работы не более 20 секунд) и короткие контрпримеры (10 или меньше инструкций) для быстрой отладки.

Ключевые слова: ограниченная проверка моделей, формальная верификация, предкристаллическая верификация, символьная быстрая проверка ошибок.

Abstract: Singh E., Devarajegowda K., Simon S., Schnieder R., Ganesan K., Fadiheh M., Stoffel D., Kunz W., Barrett C., Ecker W., Mitra S. Symbolic QED Pre-silicon Verification for Automotive Microcontroller Cores: Industrial Case Study. We present an industrial case study that demonstrates the practicality and effectiveness of Symbolic Quick Error Detection (Symbolic QED) in detecting logic design flaws during pre-silicon verification. Our study focuses on several microcontroller core designs (~1,800 flip-flops, ~70,000 logic gates) that have been extensively verified using an industrial verification flow and used for various commercial automotive products. The results of our study are as follows: 1. Symbolic QED detected all logic bugs in the designs that were detected by the industrial verification flow (which includes various flavors of simulation-based verification and formal verification). 2. Symbolic QED detected additional logic bugs that were not recorded as detected by the industrial verification flow. 3. Symbolic QED enables significant design productivity improvements: (a) 8X improved verification effort for a new design (8 person-weeks for Symbolic QED vs. 17 person-months using the industrial verification flow). (b) 60X improved verification effort for subsequent designs (2 person-days for Symbolic QED vs. 4-7 person-months using the industrial verification flow). (c) Quick bug detection (runtime of 20 seconds or less), together with short counterexamples (10 or fewer instructions) for quick debug, using Symbolic QED.

Keywords: Bounded Model Checking, Formal verification, Pre-silicon verification, Symbolic Quick Error Detection.

1. Цель промышленного исследования

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

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

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

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

Символьная быстрая проверка ошибок (Symbolic QED) — это новый подход к предкристаллической верификации со следующими характеристиками:

• применима к любой системе на кристалле (SoC), содержащей хотя бы одно программируемое процессорное ядро (что верно для большинства современных систем).
• Широко применима для обнаружения логических ошибок в ядрах процессоров и акселераторах.
• Хотя она основана на методе ограниченной проверки моделей (BMC), для её применения не требуется создавать специфические для проектирования свойства вручную.
• Несмотря на использование BMC, она обеспечивает высокую скорость выполнения и масштабируется для проектов с миллиардами транзисторов.
• Результаты, полученные на различных конструкциях (от ядер процессоров до многопроцессорных систем), демонстрируют эффективность Symbolic QED и её расширений.

Цель данного промышленного исследования — продемонстрировать практичность и эффективность метода Symbolic QED в реальных промышленных условиях. Особое внимание уделяется вопросам: какие логические ошибки обнаруживает Symbolic QED по сравнению с современными промышленными процессами верификации, сколько трудозатрат требуется для её внедрения, и сколько времени и вычислительных ресурсов необходимо для запуска.

2. Исследуемые конструкции

Для анализа эффективности Symbolic QED были выбраны промышленные конструкции со следующими характеристиками:

1. Промышленные ядра микроконтроллеров, которые прошли тщательную верификацию (более 5 лет) с использованием промышленных методов верификации, особенно потому, что они ориентированы на автомобильные применения.
2. Наличие нескольких конструкций, основанных на одной и той же архитектуре набора инструкций (ISA), для оценки усилий, необходимых для применения Symbolic QED к новой конструкции и к последующим конструкциям с той же ISA.
3. Наличие одной или нескольких версий каждой конструкции (с обновлениями RTL для исправления ошибок и добавления функций) для анализа эффективности Symbolic QED на различных этапах зрелости проектирования.

Три ядра микроконтроллеров, выбранные для этого исследования, использовались в различных автомобильных продуктах. Все три конструкции были получены из Конструкции 1 и включают различные функции, нацеленные на конкретные коммерческие продукты. Для исследования доступны несколько последних версий каждой конструкции (всего 16 версий).

Каждая конструкция содержит примерно 1800 триггеров и 70 000 логических элементов и реализует пользовательскую ISA с более чем 50 инструкциями. Конструкции также реализуют встроенные механизмы безопасности и классифицируются как ASIL-рейтинговые (Automotive Safety Integrity Level) согласно стандарту ISO 26262.

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

3. Реализация промышленного верификационного процесса

Для каждой версии конструкции промышленный верификационный процесс использовал три метода верификации:

1. Направленные симуляционные тесты (DST). На этапе проектирования разработчики вручную создают тестбенчи для симуляции конкретных тестовых сценариев. Основная цель этих тестов — верифицировать конкретные функции или возможности. Типичные проверки включают: переходы между различными состояниями (сброс, встроенный самотест, остановка, перезапуск, выборка, выполнение); различные «классы» инструкций (одно- и двухкодовые инструкции). Направленные тесты не предназначены для комплексной верификации RTL, поэтому логические ошибки могут оставаться незамеченными. Ошибки, обнаруженные с помощью DST, немедленно исправлялись разработчиками и не регистрировались.

2. Формальная верификация (OCS-FV). Команда верификации применяла формальную верификацию с использованием свойств, генерируемых внутренним автоматизированным инструментом. Для каждой инструкции создается отдельное свойство, которое затем проверяется для микроконтроллерного ядра. Например, для инструкции «ADD» проверяется, что после декодирования инструкции состояние ядра переходит в состояние выполнения, результат вычисления корректен, и значение сохраняется в файле регистров. Свойства OCS-FV отличаются от так называемых Single-Instruction свойств, которые будут рассмотрены позже в контексте Symbolic QED. Значительная сложность при использовании OCS-FV заключается в избежании ложных сбоев из-за взаимодействия с множеством инструкций. Это требует добавления ручных ограничений, что может привести к избыточным ограничениям конструкции и упущенным ошибкам.

3. Ограниченная случайная симуляция (CRS). Этот метод верификации использует тестбенчи, созданные в соответствии с универсальной методологией верификации (UVM). Разработчики, архитекторы и инженеры по верификации сначала создают план верификации, включающий различные аспекты: конкретные тесты и методы, инструменты, критерии завершения, ресурсы (персонал, оборудование, программное обеспечение), функции для верификации, непроверенные функции и т.д. Затем инженеры по верификации создают тестовые сценарии на основе этого плана. Тщательность таких тестовых сценариев зависит от качества плана верификации. Критерии завершения часто определяются метриками покрытия кода и функционального покрытия. Основная сложность — обеспечить тщательность плана верификации и соответствующих тестовых сценариев.

4. Трудозатраты на настройку и запуск верификационных методов в промышленном процессе

Настройка DST: для Конструкции 1 (всех версий) DST потребовал общих усилий в 10 человеко-месяцев. Для каждой последующей конструкции (A-C) DST потребовал 1-3 человеко-месяца для всех версий. Отметим, что трудно отделить усилия DST от общих усилий проектирования, поскольку DST применяется самими разработчиками.

Время выполнения DST: коммерческий симулятор на процессоре Intel Xeon E5-2690 v3 @ 2.6 ГГц с 32 ГБ ОЗУ потребовал примерно 1 час для симуляции всех направленных тестовых сценариев (для каждой версии конструкции).

Настройка OCS-FV: для Конструкции 1.v1 OCS-FV потребовал 4 человеко-месяца усилий. Для последующих конструкций (A.v1, B.v1 и C.v1) потребовалось 1 человеко-месяц для обновления существующих свойств. Между версиями конструкций (например, A.v[2] – A.v[f]) свойства не требовали значительных обновлений — обычно менее 1 человеко-часа.

Время выполнения OCS-FV: Onespin 360 DV Verify (версия 2016.12) на процессоре Intel Xeon E5-2690 v3 @ 2.6 ГГц с 32 ГБ ОЗУ потребовал примерно 3 часа для запуска полного набора свойств (для каждой версии конструкции).

Настройка CRS: CRS впервые был применен к Конструкции 1.v[m]. Общий процесс от Конструкции 1.v[m] до Конструкции 1.v[f] потребовал 12 человеко-месяцев. Для последующих конструкций (A-C) тестбенчи в основном переиспользовались (с соответствующими модификациями). Для каждой последующей конструкции потребовалось 3-6 человеко-месяцев для обновления тестбенчей во всех версиях.

Время выполнения CRS: коммерческий симулятор на процессоре Intel Xeon E5-2690 v3 @ 2.6 ГГц с 32 ГБ ОЗУ потребовал примерно 24 часа (для каждой версии конструкции).

5. Реализация Symbolic QED для данного исследования

Symbolic QED требует начального состояния, согласованного с QED, чтобы избежать ложных сбоев. Было использовано начальное состояние с ядром в рабочем режиме, пустым конвейером и всеми регистрами и ячейками памяти, равными нулю. Для наших конструкций эти условия гарантируют, что (при отсутствии ошибки) последовательности QED будут выполняться корректно.

Для данного исследования был использован модуль QED, который является улучшенной версией предыдущих разработок. Кроме того, EDDI-V (Error Detection using Duplicated Instructions for Validation) был дополнительно улучшен.

Улучшенный EDDI-V: ошибки управления потоком. EDDI-V был расширен для обнаружения ошибок, вызывающих ошибки в управлении потоком выполнения. В рамках расширенного подхода EDDI-V для обнаружения ошибок потока управления используется модуль QED-Control Flow (QED-CF), который размещается между модулем QED и стадией выборки инструкций ядра. Модуль QED-CF захватывает целевые адреса каждой инструкции управления потоком (ветвления или перехода) и сравнивает цели оригинальной инструкции управления потоком с соответствующей дублированной инструкцией. При несовпадении инструмент BMC может ввести любую инструкцию, чтобы представить некорректное управление потоком — эта введенная инструкция затем вызывает сбой проверки QED.

Улучшенный EDDI-V: дублирование с использованием памяти. В отличие от базового подхода EDDI-V, мы можем выбрать вариант, при котором регистровое пространство не делится на две половины. Вместо этого (оригинальные и) дублированные значения могут временно храниться в памяти по различным причинам: определенные инструкции могут использовать только конкретные регистры (например, загрузка-непосредственно может загружать только в R0), или ошибка может быть вызвана только при использовании определенных регистров.

Свойства для отдельных инструкций (Single-I). Для каждой инструкции в ISA специфицируем (с использованием SystemVerilog) ожидаемое поведение этой инструкции. Любые значения операндов инструкции определяются символически, позволяя инструменту BMC оценивать свойства для всех возможных значений операндов. Каждое такое свойство проверяется независимо (т.е. когда конвейер не содержит других инструкций). Следовательно, это отличается от OCS-FV (которому требуется обширная ручная работа для избежания ложных сбоев, как упоминалось ранее).

6. Время настройки и запуска Symbolic QED

Настройка для Конструкции A. Настройка Symbolic QED (с использованием EDDI-V и модуля QED) заняла 4 человеко-недели. Основная задача заключалась в создании модуля QED (что требовало понимания конструкции и ISA, включая кодирование инструкций и отображение регистров).

Улучшенная версия EDDI-V для ошибок потока управления и дублирования с использованием памяти потребовала еще по 1 человеко-неделе каждая. Это включает создание модели памяти, которая предотвращает резкое увеличение пространства состояний во время BMC.

Свойства Single-I для Конструкции A заняли 2 человеко-недели.

Настройка для последующих конструкций B и C.

Адаптация настройки EDDI-V (включая улучшения EDDI-V) от Конструкции A к Конструкциям B и C потребовала по одному человеко-дню каждая. Между Конструкцией A и Конструкциями B и C были два значительных изменения конструкции: одинарный интерфейс ROM в B и C (в отличие от двойного интерфейса ROM в A) и одна дополнительная инструкция в B и C (в отличие от A).

Адаптация свойств Single-I (вручную) от Конструкции A к Конструкциям B и C заняла по 1 человеко-дню каждая.

Между версиями конструкций адаптация Symbolic QED потребовала практически нулевых усилий (1 человеко-час или меньше).

Таблица 1: Трудозатраты на настройку: промышленный верификационный процесс против Symbolic QED

Метод	Общие трудозатраты: начальная конструкция	Общие трудозатраты: последующие конструкции
OCS-FV	5 человеко-месяцев	1 человеко-месяц
CRS	12 человеко-месяцев	3-6 человеко-месяцев
Общий промышленный верификационный процесс (OCS-FV, CRS)	17 человеко-месяцев	4-7 человеко-месяцев
Symbolic QED	8 человеко-недель	2 человеко-дня

Время выполнения: Symbolic QED с улучшенным EDDI-V потребовал от 6 до 12 секунд для генерации контрпримеров. Свойства Single-I были еще быстрее, находя контрпримеры за 6-8 секунд.

7. Какие ошибки обнаружил Symbolic QED?

Symbolic QED обнаружил все логические ошибки, выявленные промышленным верификационным процессом для всех 16 конструкций. Эти ошибки были связаны как с RTL-проектированием, так и со спецификацией проектирования.

Инструмент BMC генерировал контрпримеры Symbolic QED, начиная с состояния, когда ядро находится в нормальном режиме выполнения, конвейер пуст, а все регистры и ячейки памяти установлены в 0 (согласованное с QED архитектурное состояние).

Дополнительные 7%, обнаруженные исключительно Symbolic QED, связаны со спецификацией для Конструкции A.v[f]. После обсуждения с разработчиками мы предполагаем, что эти 7% были, возможно, также обнаружены с использованием промышленного верификационного процесса (но не были зарегистрированы, и документ спецификации также не был обновлен).

Все эти ошибки были обнаружены только CRS в промышленном верификационном процессе; они оставались незамеченными как в DST, так и в OCS-FV.

8. Какие ошибки обнаружили различные функции Symbolic QED?

Symbolic QED с использованием EDDI-V обнаружил 35.7% ошибок. Улучшенный EDDI-V уникально обнаружил еще 35.7% ошибок: 28.6% этих ошибок вызывали ошибки потока управления с неправильными направлениями ветвления (обнаруженные улучшенным EDDI-V с использованием модуля QED-CF), а оставшиеся 7.1% использовали инструкции с определенным регистром назначения (обнаруженные улучшенным EDDI-V с использованием памяти для дублирования).

Оставшиеся 28.6% ошибок были обнаружены с помощью Single-I. Можно было бы ожидать, что ошибки, обнаруженные с помощью Single-I, также должны быть обнаружены OCS-FV. Однако из-за человеческой ошибки (вызванной способами справиться с ложными сбоями, как объяснялось ранее), свойства OCS-FV пропустили определенные детали. В результате ошибки Single-I не были обнаружены OCS-FV (до тех пор, пока ошибки не были обнаружены с помощью CRS и свойства не были вручную обновлены на основе обнаруженных ошибок).

9. Сколько времени потребовалось на отладку с использованием Symbolic QED?

Контрпримеры, генерируемые Symbolic QED, были очень короткими. В результате время отладки было сопоставимо со временем в промышленном верификационном процессе (менее одного дня для анализа и исправления каждой ошибки).

Таблица 2: Длина контрпримеров для Symbolic QED

Метод	Длина контрпримера (циклы) [мин., средн., макс.]	Длина контрпримера (инструкции) [мин., средн., макс.]
Symbolic QED с обоими улучшениями EDDI-V	[5, 7.4, 11]	[4, 6.2, 10]
Single Instruction	[2, 2, 2]	[1, 1, 1]

10. Каковы перспективные направления развития Symbolic QED?

• Дополнительные кейс-статьи: хотя в этом исследовании использовались ядра микроконтроллеров, кейс-статьи по более сложным SoC могут продемонстрировать дальнейшие преимущества Symbolic QED.
• Symbolic QED с символьным начальным состоянием: Symbolic QED, использованный в этом исследовании, использует фиксированное начальное состояние. Для ошибок с очень длинными последовательностями активации инструмент BMC может испытывать трудности с развертыванием конструкции на достаточную глубину. Symbolic QED с символьными начальными состояниями может преодолеть эту проблему.
• Безопасность аппаратного обеспечения: методы, основанные на Symbolic QED, могут быть высокоэффективными в обнаружении уязвимостей безопасности в цифровых системах. Примеры включают: (a) уникальную проверку выполнения программ (UPEC) для обнаружения уязвимостей безопасности, основанных на временных каналах, в процессорах; (b) обнаружение аппаратных троянов во время доизготовительной верификации с использованием Symbolic QED с символьными начальными состояниями.
• Методы Symbolic QED могут быть расширены для включения аналогово-цифровых блоков проектирования.
• Локализация ошибок во время постпроизводственной валидации и эксплуатации системы: Symbolic QED и методы E-QED показывают многообещающие результаты в локализации логических и электрических ошибок во время постпроизводственной валидации и эксплуатации системы.

Список источников

1. Clarke, E., A. Biere, R. Raimi, Y. Zhu, "Bounded Model Checking Using Satisfiability Solving," Formal Methods in System Design, Vol. 19, No. 1, pp. 7-34, 2001.
2. Ecker, W., et al. "Memory models for the formal verification of assembler code using bounded model checking," Proc. Seventh IEEE International Symposium on Object-Oriented Real-Time Distributed Computing, pp. 129-135, 2004.
3. Ecker, W., et al. "The metamodeling approach to system level synthesis," Proc. Design Automation and Test in Europe, p. 311, 2014.
4. Fadiheh, M. R., et al. "Symbolic quick error detection using symbolic initial state for pre-silicon verification," Proc. Design Automation and Test in Europe, pp. 55-60, 2018.
5. Fadiheh, M. R., et al. "Processor Hardware Security Vulnerabilities and their Detection by Unique Program Execution Checking," Proc. Design Automation and Test in Europe, 2019.
6. Foster, H. D., "Trends in Functional Verification: A 2014 Industry Study," Proc. IEEE/ACM Design Automation Conf., pp. 48-52, 2015.
7. Ganesan, K., et al. "Effective Pre-Silicon Verification of Processor Cores by Breaking the Bounds of Symbolic Quick Error Detection," available at https://tinyurl.com/y9s9k7lt, 2018.
8. Gielen, G., et al. "Review of Methodologies for Pre- and Post-Silicon Analog Verification in Mixed-Signal SOCs," Proc. Design Automation and Test in Europe, 2019.
9. ISO, ISO. "26262–1: 2011 road vehicles functional safety. ISO." International Organization for Standardization, Geneva, Switzerland (2011).
10. Kocher, P., et al. "Spectre attacks: Exploiting speculative execution," arXiv:1801.01203[cs.CR], 2018.
11. Lin, D., et al., "Effective Post-Silicon Validation of System-on-Chips Using Quick Error Detection," IEEE Trans. Computer Aided Design of Integrated Circuits Systems, Vol. 33, No. 10, pp. 1573-1590, 2014.
12. Lin, D., et al. "A Structured Approach to Post-Silicon Validation and Debug Using Symbolic Quick Error Detection," Proc. IEEE Intl. Test Conf., 6-8 Oct. 2015, pp.1-10.
13. Lipp, M., et al. "Meltdown: Reading kernel memory from user space," 27th USENIX Security Symposium, pp. 973-990, 2018.
14. Reid, A., et al. "End-to-end verification of processors with ISA-Formal," Proc. Intl. Conf. on Computer Aided Verification, pp. 42-58, 2016.
15. Singh, E., C. Barrett, S. Mitra. "E-QED: Electrical Bug Localization during Post-silicon Validation Enabled by Quick Error Detection and Formal Methods," Proc. Intl. Conf. on Computer Aided Verification, pp. 104-125, 2017.
16. Singh E., et al. "Logic Bug Detection and Localization Using Symbolic Quick Error Detection," IEEE Trans. Computer Aided Design of Integrated Circuits Systems, 2018.
17. "IEEE Standard for Universal Verification Methodology Language Reference Manual," in IEEE Std 1800.2-2017, pp.1-472, 2017.
18. Wile B., J. Gross C., Roesner W., "Comprehensive Functional Verification," 1st Edition, MK Publishers, 2005.