ISSN 0236-235X (P)
ISSN 2311-2735 (E)

Публикационная активность

(сведения по итогам 2017 г.)
2-летний импакт-фактор РИНЦ: 0,500
2-летний импакт-фактор РИНЦ без самоцитирования: 0,405
Двухлетний импакт-фактор РИНЦ с учетом цитирования из всех
источников: 0,817
5-летний импакт-фактор РИНЦ: 0,319
5-летний импакт-фактор РИНЦ без самоцитирования: 0,264
Суммарное число цитирований журнала в РИНЦ: 6012
Пятилетний индекс Херфиндаля по цитирующим журналам: 404
Индекс Херфиндаля по организациям авторов: 338
Десятилетний индекс Хирша: 17
Место в общем рейтинге SCIENCE INDEX за 2017 год: 527
Место в рейтинге SCIENCE INDEX за 2017 год по тематике "Автоматика. Вычислительная техника": 16

Больше данных по публикационной активности нашего журнале за 2008-2017 гг. на сайте РИНЦ

Вход


Забыли пароль? / Регистрация

Добавить в закладки

Следующий номер на сайте

4
Ожидается:
16 Декабря 2018

Формальные методы верификации RTL-моделей сверхбольших интегральных схем

Статья опубликована в выпуске журнала № 4 за 2008 год.[ 23.12.2008 ]
Аннотация:
Abstract:
Авторы: Новожилов Е.Е. () - , ,
Ключевые слова: программирование устройств, rtl-модель, микросхемы, устройства, сбис
Keywords: , RTL model, microchips, , vlsi
Количество просмотров: 11819
Версия для печати
Выпуск в формате PDF (8.40Мб)

Размер шрифта:       Шрифт:

Высокая конкуренция на рынке микроэлектронных устройств требует от разработчиков создания все более сложных и многофункциональных сверхбольших интегральных схем (СБИС) и сокращения сроков их проектирования. Эти противоречивые требования привели к появлению нового единого языка для описания и тестирования аппаратуры SystemVerilog (IEEE Std 1800™-2005), расширяющего возможности языка Verilog. Кроме того, появилась новая методология тестирования современных СБИС, предполагающая использование следующих возможностей языка SystemVerilog.

1.    Использование формальных утверждений (SystemVerilog Assertions (SVA)) о предполагаемом поведении устройства, проектируемого на языке Verilog. SVA предлагает 2 основных преимущества для разработчика.

·       SVA позволяет вставить требуемые утверждения о должном поведении блока устройства в HDL-описание устройства, чтобы при последующем моделировании или при использовании средств формальной верификации иметь возможность проверить соответствие созданной RTL-модели заданному набору утверждений. (Правильно ли это работает?) В небольших проектах для такой проверки будет достаточно средств формальной верификации. Для больших проектов с большим количеством состояний средства формальной верификации не смогут проверить все созданные утверждения, поэтому в данном случае описанные свойства устройства будут проверяться в течение всего времени моделирования, чтобы гарантировать выполнение утверждений хотя бы на заданном наборе тестов. При нарушении утверждения в последнем случае система моделирования выдаст предупреждение, укажет время нарушения и утверждение, которое не было выполнено.

·         Разработчик может описать на этом языке свойства и функции элементов своего устройства и возможные операции с ними, например, наличие определенного набора регистров и возможные операции с ними (чтение, запись). Эти элементы необходимы для анализа функционального покрытия устройства.

2.      Функциональное покрытие – это набор специальных конструкций и методов для работы со SVA и элементами устройства, чтобы в процессе тестирования устройства иметь информацию о том, какие операции с какими элементами устройства тестом выполнялись, а какие нет (например, можно увидеть, что запись в регистр производилась, а чтение нет, и т.д.). Иными словами, функциональное покрытие позволяет оценить качество проверки отдельных функций устройства. Эта информация может использоваться разработчиком теста для его дополнения таким образом, чтобы выполнялись все возможные операции со всеми элементами устройства.

3.                Случайное тестирование с наложением внешних ограничений – набор методов для формирования случайных тестовых воздействий на устройство, ограниченных внешними параметрами. Появление данного инструмента было вызвано возрастающей сложностью создаваемых устройств и невозможностью за разумное время вручную протестировать все функции этих устройств. Так как тестирование при использовании данного метода происходит случайным образом, единственная адекватная шкала для оценки качества тестирования – это опять же функциональное покрытие. Таким образом, 100 %-е функциональное покрытие блока означает, что случайный тест покрыл все возможные воздействия на СБИС, которые разработчик предусмотрел, при этом случайное тестирование покрывает и множество комбинаций, которые разработчик не предвидел.

4.                Объектно-ориентированное программирование (ООП) для создания высокоуровневых моделей и тестов. Максимальное заимствование кода благодаря механизмам наследования, упрощенная интеграция с поведенческими моделями на языке C благодаря механизму DPI (Direct Programming Interface), поддержке моделирования на уровне транзакций TLM (Transaction-level modeling) и т.д.

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

Эволюция методологии тестирования RTL-модели СБИС

До 2004 года, когда начал получать распространение язык PSL (Property Specification Language), положенный в основу SVA, методология тестирования RTL-модели устройства предполагала разделение команды разработчиков на 2 группы:

-     первая группа формировала RTL-описание устройства (в дальнейшем членов этой группы будем называть RTL-разработчиками),

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

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

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

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

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

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

а) общее описание архитектуры блока;

б) общее описание выполняемых блоком функций (так называемый «один день из жизни блока»);

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

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

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

Указанная методика позволяет повысить качество тестирования устройства, используя шкалы функционального покрытия в качестве новой методики оценки полноты тестов. Более того, с использованием данного подхода у разработчиков появляется возможность анализировать тестовое покрытие не по блокам, а по функциям, оставляя тестирование менее приоритетных функций на конец цикла тестирования. Кроме того, использование шкалы функционального покрытия – это единственный адекватный способ оценки тщательности тестирования устройства при использовании случайно формируемых наборов тестовых воздействий. Хотя использование SVA и приводит к увеличению трудозатрат разработчиков на начальном этапе, такой подход позволяет сократить трудозатраты по отладке схемы на последующих этапах и работу по написанию тестов в дальнейшем, избегая ситуации, когда новые тесты более чем на 90 % повторяют старые.

Тестирование RTL-модели СБИС при использовании генератора готовых утверждений

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

·     открытые, например OVL (Open Verification Library);

·     закрытые, пополняемые компанией-производителем сопутствующего программного обеспе- чения, например IAL (Incisive Assertion Library), пополняемая фирмой Cadence Design Systems Inc.

Эти библиотеки содержат ограниченный набор функций, реализующих сложные утверждения, наиболее часто используемые разработчиками. Например, проверку на четность результирующего операнда (assert_odd), проверку инкремента (assert_ increment) и т.д.

Предлагается расширить современный подход и сформировать обязательный набор правил, используемый при формировании утверждений для типовых элементов, встречающихся в большинстве цифровых СБИС (регистры, блоки памяти, счетчики, автоматы, конвейеры, АЛУ, FIFO и т.д).

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

Единый набор правил позволит создать программу по формированию готовых утверждений на языке SVA на основе исходных шаблонов для конкретного компонента. Наличие программы, формирующей готовые блоки утверждений, позволит сократить усилия разработчиков по добавлению кода утверждений в RTL-модель СБИС и понизит вероятность ошибки разработчика при добавлении кода утверждения. Таким образом, цикл создания устройства еще более сократится, а качество его проверки возрастет благодаря наличию общепринятого стандарта, доказавшего свою эффективность на различных проектах.

Можно было бы вместо такой программы создать еще одну высокоуровневую поведенческую библиотеку, но ввиду сложности описываемого элемента такая библиотека содержала бы слишком большое количество либо функций (под каждый возможный вариант реализации элемента), либо параметров. И тот, и другой варианты усложняют процесс формирования поведенческих описаний для внутренних элементов СБИС, снижают читаемость кода и усложняют процесс проектирования. Кроме этого, готовый блок утверждений на языке SVA обладает следующими преимуществами:

·     гибкость – при желании разработчик может модифицировать набор утверждений, чтобы они соответствовали специфическим требованиям, накладываемым на конкретный элемент;

·     расширяемость – возможность дополнения готового блока новыми функциями;

·     простота кода – разработчику достаточно знать синтаксис SVA, чтобы понять, что именно проверяет блок, и нет необходимости помнить несколько сотен стандартных функций и очередность передаваемых им параметров.

Рассмотрим возможный вариант реализации базового набора правил для типового элемента устройства – регистра управления/состояния.

Предлагается следующий набор правил.

1.   По сигналу сброс или установка все разряды регистра, за исключением разрядов статуса, должны устанавливаться в состояние логического 0 или 1 соответственно.

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

3.   Все разряды, кроме разрядов статуса, не должны меняться до поступления сигнала записи, сброса или установки.

4.   Разряды статуса должны повторять состояние внешних сигналов статуса с задержкой не более чем на 1 такт.

5.   Зарезервированные разряды вне зависимости от внешних воздействий при чтении должны возвращать указанное постоянное значение.

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

7.   При формировании сигнала записи в момент активного сигнала установки данные в регистре, за исключением разрядов статуса, должны устанавливаться в состояние логической 1.

8.    В момент фронта синхросигнала ни один разряд регистра не должен находиться в состоянии X или Z.

9.    В момент фронта синхросигнала ни один из управляющих сигналов регистра не должен находиться в состоянии X или Z.

Для оценки теста, использующего данный регистр, можно сформировать набор контрольных точек, позволяющий выяснить, сколько раз производились запись 0 и 1 в каждый используемый разряд регистра, сброс/установка для данного регистра, чтение из регистра.

Дополнительные контрольные точки для регистра управления/состояния: количество сочетаний двух произвольных используемых разрядов регистра; количество сочетаний трех произвольных используемых разрядов регистра.

RTL-модель регистра управления/состояния с синхронным сбросом и резервными разрядами, установленными в 0:

//CSR: Control-Status register addr:0xad

//15 14 13 12 11 10 09 08 07 06 05 04 03 02 01 00 : BIT NUM

//RS RS RS RS RW RW RW RW RW RW RW RW RD RD RD RD : ACESS TYPE

//----- RTL code: ------------------------------------------

reg [15:0] csr;

wire [3:0] status;

wire [3:0] reserved;

wire [15:0] data_in;

assign reserved=4’h0;

 always @(posedge clk)

    if (!reset_n) csr<={reserved[3:0],8’h00,status[3:0]};

     else if (write) csr <={reserved[3:0],data_in[11:4], status[3:0]};

     else csr <={csr[15:4],status[3:0]};

На языке SystemVerilog набор утверждений и контрольных точек для данного регистра при использовании упомянутых правил будет выглядеть так:

//---- Assertions based on standard rules ------------------

//1. Reset check

assert property (@(posedge clk) !reset_n |Þ csr[15:4] == 12’b000000000000;)

 else $error(“Category: Registers, Base rule No: 1, csr register wasn’t reset correctly!”);

//2.Check write complete

reg [15:0] v_2;

assert property (@(posedge clk) disable iff (!reset)(write,v_2=data_in[15:0]) |Þ (csr =={reserved[3:0],v_2[11:4],status[3:0]});)

 else $error(“Category: Registers, Base rule No: 2, csr register write wasn’t succesfull!”);

//3 e.t.c.

Для компактности изложения реализация остальных правил не иллюстрируется.

Таким образом, можно видеть, что работа по созданию утверждений для небольшого стандартного элемента СБИС, коим является регистр управления/состояния, превышает работу по описанию этого элемента на языке Verilog приблизительно в 9 раз (если сравнивать объем требуемого кода). Следовательно, необходимо максимально сократить эту работу, например, используя генератор готовых утверждений на основе шаблонов и данных из спецификации. Создание такого генератора станет возможным после формирования стандартного набора правил для основных типовых элементов СБИС.

Данный подход наряду с применением других средств, предлагаемых языком SystemVerilog, позволит значительно сократить время тестирования RTL-модели устройства и повысить качество ее тестирования.

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


Постоянный адрес статьи:
http://swsys.ru/index.php?page=article&id=1606
Версия для печати
Выпуск в формате PDF (8.40Мб)
Статья опубликована в выпуске журнала № 4 за 2008 год.

Возможно, Вас заинтересуют следующие статьи схожих тематик: