Тестирование и верификация HDL-моделей компонентов SOC
ТЕСТИРОВАНИЕ И
ВЕРИФИКАЦИЯ HDL-МОДЕЛЕЙ КОМПОНЕНТОВ SOC
1. Анализ тестопригодности графа управления
Учитывая, что автоматная модель программного продукта
представлена взаимодействием операционного и управляющего автомат, рис. 1, то
наряду с моделированием транзакционного графа, необходимо иметь возможность
анализировать тестопригодность граф-схемы алгоритма управления (ГСА).
Рис. 1. Автоматная модель HDL-программы
Предлагается ГСА представить в виде содержательного графа
управления (СГУ), который является подобным транзакционному графу. Здесь
вершины есть операции программного кода, а дуги представляют условия перехода
из одной вершины в другую для выполнения команды, обозначенной вершиной-стоком.
Следовательно, для СГУ можно использовать процедуры,
ранее разработанные для подсчета критериев тестопригодности транзакционного
графа в части управляемости и наблюдаемости. Примером содержательного графа
может служить рис. 2, имеющий 6 вершин и 9 дуг.
Рис. 2. Содержательный граф HDL-программы
Подсчет управляемостей графа, представленного на рис. 2,
имеет следующий вид:
Подсчет наблюдаемостей графа, представленного на рис. 2,
содержит следующие выражения:
Рис. 3. Графики тестопригодности для графа управления
Для использования тестопригодности выполняется построение
управляемости и наблюдаемости всех компонентов HDL-модели (рис. 3). Затем
вычисляется обобщенная характеристика – тестопригодность каждого компонента как
произведение управляемости и наблюдаемости:
. (1)
Далее интерес представляет создание таблицы
тестопригодности, управляемости и наблюдаемости, а также соответствующий им
график для визуального контроля «плохих» компонентов. Фиксация определенной
планки тестопригодности, ниже которой значения будут считаться неприемлемыми,
позволит разработчику создавать ассерции и другие дополнительные средства
повышения тестопригодности для проблемных функциональных блоков. Кроме того,
средства повышения тестопригодности должны обеспечивать глубину
диагностирования до функционального компонента и привязанных к нему операций в
целях быстрого восстановления работоспособности программной HDL-модели. В целях
построения алгоритмов поиска ошибок в программном коде можно использовать
таблицу неисправностей, по аналогии с технологией тестирования hardware.
Любопытное решение в процессе проверки функциональных блоков связано с
сигнатурным анализом, где обобщенная сигнатура отождествляется с исправным
поведением всего кода, а также с каждым компонентом. Любое несовпадение
эталонной сигнатуры с фактической приводит к выполнению процедуры
диагностирования и восстановления работоспособности HDL-модели путем
исправления семантики кода.
Предложенная модель верификации HDL-проекта использует
testbench, функциональное покрытие, механизм ассерций, описанную выше метрику
оценки тестопригодности, таблицу неисправностей и вектор экспериментальной
проверки (ВЭП), формируемый по заданным контрольным точкам путем сравнения
сигнатур. Функциональное ограничение testbench связано с неразличимостью
компонентов программного кода, в которых могут быть ошибки. Его основное
назначение – проверка исправности HDL-модели. Поэтому в качестве дополнения к
процедуре проверки придается механизм ассерций, основная цель которого с
заданной глубиной – до программного компонента – определить место и вид ошибки
на стадии выполнения диагностирования, после того, как testbench зафиксировал
неправильное функционирование программного проекта. Две стадии верификации:
тестирование и диагностирование – представлены ниже в виде следующих двух
векторно-матричных операций:
Для первой стадии используется двоичный вектор
экспериментальной проверки ,
формируемый на основе процедуры тестирования. На второй стадии используется уже
матрица экспериментальной
проверки, которая с наперед заданной глубиной определяет диагноз проекта на
основе сравнения технических состояний HDL-модели и механизма ассерций:
В процессе выполнения процедуры верификации выполняется
сравнение фактического и эталонного (специфицированного) технического состояния
компонента путем применения операции Xor:
Практически, если выполнены условия тестопригодности и
правильно расставлены ассерции в критических точках программного кода для
диагностирования всех компонентов, то ВЭП может однозначно идентифицировать
адрес (место) и тип ошибки на основе построенной ранее таблицы неисправностей –
механизма ассерций.
2. Верификация DCT IP-core, Xilinx
Представленные модели верификации программного HDL-кода
проверены на реальном проекте Xilinx IP-core в целях определения наличия в нем
ошибок. При этом удалось получить положительный результат относительно неверной
семантики работы программы для последующего исправления кода. Фрагмент модуля
дискретного косинусного преобразования представлен листингом 1 [Xilinx.com].
Вся HDL-модель насчитывает 900 строк кода System Verilog.
Листинг. 1.
module Xilinx
`timescale 1ns/10ps
module dct ( CLK, RST,
xin,dct_2d,rdy_out);
output [11:0] dct_2d;
input CLK, RST;
input[7:0] xin; /* input */
output rdy_out;
wire[11:0] dct_2d;
………………….
/* The first 1D-DCT output becomes valid
after 14 +64 clk cycles. For the first 2D-DCT output to be valid it takes 78 +
1clk to write into the ram + 1clk to write out of the ram + 8 clks to shift in
the 1D-DCT values + 1clk to register the 1D-DCT values + 1clk to add/sub + 1clk
to take compliment + 1 clk for multiplying + 2clks to add product. So the 2D-DCT
output will be valid at the 94th clk. rdy_out goes high at 93rd clk so that the
first data is valid for the next block*/
Endmodule
В соответствии с правилами тестопригодного анализа,
приведенными выше, спроектирован транзакционный граф как развитие графа
регистровых передач, представленный на рис. 4, который для module Xilinx имеет
28 вершин-компонентов (входная и выходная шины, логические и регистровые
переменные, векторы и память).
Рис. 4. Транзакционный граф Xilinx модели
Идентификатор дуги имеет верхний индекс, обозначающий
число транзакций в программе между исходящей и входящей вершинами. Для каждой
вершины строятся логические функции управляемости и наблюдаемости. Пример
логической функции управляемости для вершины имеет следующий вид:
Для остальных вершин аналогично выполняется вычисление
ДНФ функций управляемостей.
Примеры вычисления функций наблюдаемостей для отдельных
вершин имеют следующий вид:
Синтезированные логические функции задают все возможные
пути управления, как во времени, так и в пространстве, что можно считать новой
аналитической формой описания тестопригодности проекта. По ДНФ, следуя
выражениям для подсчета тестопригодности, можно определить критерии
управляемости (наблюдаемости) для всех компонентов HDL-модели. Здесь следует
рассмотреть для варианта (сценария) обсчета программной модели. 1) Учитывается
только графовая структура, где вес каждой дуги равен 1, независимо от числа
транзакций в программном коде. 2). Все дуги графа отмечаются реальным
количеством транзакций, имеющих место быть между двумя рассматриваемыми
вершинами-компонентами транзакционного графа. Оценки тестопригодности описанных
процедур могут существенно различаться друг от друга. Пользователь должен
определиться, что важнее только структура программного кода – применить первый
сценарий, или иметь более сложную и точную модель транзакций, распределенных во
времени, на множестве графовых компонентов. В качестве примера ниже приводится
процедура вычисления управляемости для вершины :
.
Применение аналогичных вычислений управляемостей
(наблюдаемостей) для других вершин графа дает результат в виде графика,
представленного на рис. 5, которые позволяют определить критические точки для
установки необходимых ассерций.
Такой вершиной может быть компонент , если транзакционный граф представлен
одиночными дугами. Для случая, когда дуги отмечены реальным количеством
транзакций, критические вершины принадлежат компонентам, находящихся ближе к
выходной шине . Здесь
существенным представляется не структура графа, а вес дуги входящей, который в
большей степени оказывает негативное влияние, если структурная глубина
рассматриваемого компонента достаточно высока. Используется формула (1)
вычисления тестопригодности с мультипликативными членами , что дает оценку ниже, чем любой из
сомножителей (управляемость, наблюдаемость).
Если модифицировать формулу (1) исчисления
тестопригодности для компонентов к следующему виду:
,
то кривая тестопригодности существенно поднимется вверх
по оси ординат, чем обеспечивается меньший разброс параметров для каждой
вершины. Данное обстоятельство фиксирует несколько отличные таблицы и графики,
представленные ниже (рис.6).
Рис. 5. Графики М-тестопригодности Xilinx модели
Рис. 6. Графики A-тестопригодности Xilinx модели
Интересным представляется поведение отдельных вершин.
Например, управляемость вершины в мультипликативном транзакционном графе HDL-кода
неожиданно «упала» вниз по сравнению с графом единичных дуг. Это связано с
высоким весом транзакций, поступающих на рассматриваемую вершину со стороны
входных компонентов ,
которые практически превращают в ноль значимость единичных транзакций от вершин
.
После определения управляемостей и наблюдаемостей вершин
транзакционного графа выполняется подсчет обобщенного критерия
тестопригодностей каждого компонента программного кода в соответствии с
выражением (5). Затем определяется интегральная оценка тестопригодности проекта
по формуле:
,
которая определяет качество проектного варианта, что
представляется весьма существенным при сравнении нескольких альтернативных
решений. В качестве примера позитивного использования разработанных моделей и
методов предлагается анализ тестопригодности программного кода дискретного
косинусного преобразования из Xilinx библиотеки. Было выполнено построение
транзакционной модели, подсчет характеристик тестопригодности (), определение критических точек. Затем в
соответствии с числом и типами компонентов было разработано функциональное
покрытие, фрагмент которого представлен листингом 2.
Листинг 2.
{
bins minus_big={[128:235]};
bins minus_sm={[236:255]};
bins plus_big={[21:127]};
bins plus_sm={[1:20]};
bins zero={0};
}
c1: coverpoint dct_2d
{
bins minus_big={[128:235]};
bins minus_sm={[236:255]};
bins plus_big={[21:127]};
bins plus_sm={[1:20]};
bins zero={0};
bins zero2=(0=>0);
}
endgroup
Для критических точек, определенных в результате анализа
тестопригодности транзакционного графа разработана ассерционная модель проверки
основных характеристик дискретного косинусного преобразования. Существенный
фрагмент кода механизма ассерций представлен листингом 3.
Листинг 3.
sequence first( reg[7:0] a, reg[7:0]b);
reg[7:0] d;
(!RST,d=a)
##7 (b==d);
endsequence
property f(a,b);
@(posedge CLK)
// disable iff(RST||$isunknown(a))
first(a,b);
!RST |=> first(a,b);
endproperty
odin:assert property (f(xin,xa7_in))
// $display("Very good");
else $error("The end, xin
=%b,xa7_in=%b", $past(xin, 7),xa7_in);
В результате проведенной верификации дискретного
косинусного преобразования в среде Questa, Mentor Graphics были найдены
неточности в восьми строках исходного кода HDL-модели:
// add_sub1a <= xa7_reg + xa0_reg;//
Последующее исправление ошибок привело к появлению
исправленного фрагмента кода, который показан в листинге 4.
Листинг 4.
add_sub1a <= ({xa7_reg[8],xa7_reg} +
{xa0_reg[8],xa0_reg});
add_sub2a <= ({xa6_reg[8],xa6_reg}
+{xa1_reg[8],xa1_reg});
add_sub3a <= ({xa5_reg[8],xa5_reg}
+{xa2_reg[8],xa2_reg});
add_sub4a <= ({xa4_reg[8],xa4_reg} +
{xa3_reg[8],xa3_reg});
end
else if (toggleA == 1'b0)
begin
add_sub1a <= ({xa7_reg[8],xa7_reg} -
{xa0_reg[8],xa0_reg});
add_sub2a <= ({xa6_reg[8],xa6_reg} -
{xa1_reg[8],xa1_reg});
add_sub3a <= ({xa5_reg[8],xa5_reg} -
{xa2_reg[8],xa2_reg});
add_sub4a <= ({xa4_reg[8],xa4_reg} -
{xa3_reg[8],xa3_reg});