Учитывая, что автоматная модель программного продукта представлена взаимодействием операционного и управляющего автомат, рис. 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.

c0: coverpoint xin

{

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});