Тестирование софта - статьи


Модели аппаратного обеспечения и технология UniTesK - часть 2


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

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

Проиллюстрируем этот подход на примере. Рассмотрим модуль на языке Verilog HDL. module Module(x, y, z, r); input x, y, z; output r; reg r; always @(posedge(x), negedge(y)) begin: Process r = z; end endmodule

Интерфейс модуля состоит из трех входов: x, y, z и одного выхода r. Для процесса, определенного в модуле, входы x и y являются управляющими, а вход z - информационным. При возникновении фронта сигнала на входе x или среза сигнала на входе y процесс присваивает r значение сигнала на входе z. Для спецификации возможности наступления событий из списка чувствительности процесса, состояние спецификационной модели данных должно включать текущие значения сигналов на входах x и у. // спецификационная модель данных модуля typedef struct { // текущие значения сигналов на входах x и y bool x, y; } Module;

Спецификационная функция, описывающая поведение процесса, будет иметь в качестве параметров указатель на состояние спецификационной модели данных, индикаторы событий из списка чувствительности и значение информационного входа z. // спецификационная функция процесса specification bool Process(Module *module, bool posedge_x, bool negedge_y, bool z) // процесс читает какие события произошли, // а также значение информационного входа z reads posedge x, negedge _y, z // тестовое воздействие изменяет значения // сигналов на управляющих входах updates x = module->x, y = module->y { pre { // проверка возможности реализации событий return ((posedge x negedge _y) && (posedge х => !x) && (negedge у => y)); } post { // проверка реализации событий return ((posedge x => x) && (negedge у => !y)) && Process == z; } }

Заметим, что данный подход к выделению спецификационных функций является достаточно общим, а потому не всегда оптимальным.


Начало  Назад  Вперед