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

Спец курс (Избранные главы VHDL)/Верификация описания — различия между версиями

Материал из Wiki
Перейти к: навигация, поиск
(→‎Слайд: Работа с переменными)
 
(не показана 31 промежуточная версия 5 участников)
Строка 1: Строка 1:
 +
{{ИГСАПР_TOC}}
 
<slideshow style="custis" headingmark="Слайд:" incmark=":step" scaled="true" >
 
<slideshow style="custis" headingmark="Слайд:" incmark=":step" scaled="true" >
 
;title: '''Верификация описания.'''
 
;title: '''Верификация описания.'''
Строка 4: Строка 5:
 
</slideshow>
 
</slideshow>
  
−
[[Файл:SystemC_From_the_ground_up.mm]]
+
{| align=center width=800px
 +
![[Файл:Функциональная_верификация.mm]]
 +
|}
 +
 
 +
 
 +
==Слайд:Методы верификации проекта==
 +
* {{Сн|'''<big>Имитационная верификация</big>'''}} - верификация с использованием моделирования
 +
* {{Сн|'''<big>Формальная верификация</big>'''}} -проверка модели с целью доказательства ее корректности и эквивалентности спецификации
 +
(Пример: пакет FormulPro ф. MentorGraphics, пакеты фирмы Verplex, www.verplex.com)
 +
 
  
 
==Слайд:Верификация описания==
 
==Слайд:Верификация описания==
Строка 10: Строка 20:
  
 
==Слайд:Верификация описания:step==
 
==Слайд:Верификация описания:step==
−
*{{Гол|''' <big>Среда моделирования</big>'''}}
+
* {{Гол|''' <big>Среда моделирования</big>'''}}
 
** Active-HDL™
 
** Active-HDL™
 
** Riviera-PRO™
 
** Riviera-PRO™
Строка 24: Строка 34:
 
** Отчеты и базы по результатам моделирования
 
** Отчеты и базы по результатам моделирования
  
−
==Слайд:Эталонная модель на языке ''{{Зел| <big>SystemC</big>}}''==
 
  
−
# Высокий уровень абстракции
+
== Слайд:Средства верификации ==
−
# Скорость моделирования
+
−
# Возможности языка C++
+
−
# Инструменты для автоматизации
+
−
# Совместное моделирование с другими HDL-языками
+
  
−
== Основы языка SystemC ==
+
* {{Сн|'''Прямые тесты'''}} (Directed tests)
 +
* {{Сн|'''Псевдослучайные тесты'''}} (Random tests)
 +
* {{Сн|'''Управляемые псевдослучайные тесты'''}} (Constrained Random tests)
 +
* {{Сн|'''Верификация управляемая покрытием'''}} (на основе покрытия) (Coverage driven verification)
 +
** {{Гол|'''''Покрытие кода'''''}} (Code coverage)
 +
** {{Гол|'''''Функциональное покрытие'''''}} (Functional coverage )
 +
* {{Сн|'''Верификация на основе утверждений'''}} (Assertion based verification)
 +
* {{Сн|'''Эмуляция'''}} (Emulation)
 +
* {{Сн|'''Формальная верификация'''}} (Formal verification)
  
−
===Слайд:Типы данных (Форматы и способ представления данных) ===
+
==Слайд: Типы тестов ФК==
−
[[Файл:Типы_данных.png]]
+
На что проверяем:
 +
* {{Гол|'''<big>Детерминистский</big>'''}} - Проверяет обычные режимы работы системы, а также функционирование в граничных условиях на основе фиксированного набора тестов
 +
* {{Гол|'''<big>Случайный</big>'''}} - Предполагает наличие генератора случайных входных воздействий
 +
* {{Гол|'''<big>Транзакционный</big>'''}} - Фиксирует внимание на проверке интерфейсов и прохождению пакетов данных через них
  
−
===Слайд:Типы данных (native)===
+
Способ проведения проверки:
−
<source lang="cpp">                // Пример типа данных C++
+
* {{Сн|'''<big>"Черный ящик"</big>'''}}   
−
int spark_offset;
+
* {{Сн|'''<big>"Серый ящик"</big>'''}}
−
unsigned repairs = 0 ;            // Count repair
+
* {{Сн|'''<big>"Прозрачный ящик"</big>'''}}
−
unsigned long mileage;            // Miles driven
+
−
short int speedometer;            // -20.. 0.. 100 MPH
+
−
float temperature;                // Engine temp in C
+
−
double time_of_last_request;      //Time of bus
+
−
std:: string license_plate;      // Text for license
+
−
const bool WARNING_LIGHT = true;  // Status
+
−
enum compass {SW,W,NW,N,NE,E, SE, S} ;
+
−
</source>
+
  
−
===Слайд:Типы данных (Arithmetic)===
+
== Слайд:Что такое покрытие (Coverage)? ==
−
<source lang="cpp">                // Пример целочисленных типов данных C++
+
−
sc_int<LENGTH> NAME...;
+
−
sc_uint<LENGTH> NAME...;
+
−
sc_bigint<BITWIDTH> NAME...;
+
−
sc_biguint<BITWIDTH> NAME...;
+
−
// SystemC integer data types
+
−
sc_int<5> seat_position=3; //5 bits: 4 plus sign
+
−
sc_uint<13> days_SLOC(4000); //13 bits: no sign
+
−
sc_biguint<80> revs_SLOC; // 80 bits: no sign
+
−
</source>
+
  
−
===Слайд:Типы данных (Boolean)===
+
* {{Зел|'''Покрытие'''}} является крайне {{Кр|'''неоднозначным термином'''}}, когда используется сам по себе.
−
<source lang="cpp">                // Пример типа данных SystemC
+
−
sc_bit NAME...;
+
−
sc_bv<BITWIDTH> NAME...;
+
−
</source>
+
  
−
* sc_bit и sc_bv могут принимать значения: '''SC_LOGIC_1''' и '''SC_LOGIC_0.'''  
+
{{Info |'''Покрытие  в электронике''' ('''''Coverage''''') является одной из разновидностей метрик проекта, которая сообщает, если определённые аспекты проекта были правильно выполнены во время процедуры тестирования.}}
−
* Для сокращения типов, можно использовать '''Log_1 и Log_0''' или '''‘1’ и ‘0’.'''
+
−
* Над этим типом данных возможно выполнение битовых операций '''and, or, xor (&,|, ^).'''
+
−
* Для обращения к отдельным битам и массивам '''[], range()'''.
+
  
−
<source lang="cpp">
+
* Обычно уточняют термин покрытия, говоря какой аспект был протестирован:
−
sc_bit flag(SC_LOGIC_1); // more efficient to use bool
+
** '''Тестирование качества кода''' — покрытие кода (code coverage)
−
sc_bv<5> positions = "01101";
+
** '''Проверка свойств/утверждений''' — покрытие свойств/утверждений (property coverage)
−
sc_bv<6> mask = "100111";
+
** '''Сбор значений переменных проекта''' — функциональное покрытие (functional coverage).
−
sc_bv<5> active = positions & mask;// 00101
+
−
sc_bv<1> all = active. and_reduce (); // SC_LOGIC_0
+
−
positions. range (3,2) = "00"; // 00001
+
−
positions [2] = active[0] ^ flag;
+
−
</source>
+
  
−
===Слайд:Типы данных ( многозначные (ZX10))===
+
== Слайд:Покрытие кода vs. функциональное покрытие==
−
<source lang="cpp">                // Пример типа данных SystemC
+
−
sc_logic NAME[,NAME]...;
+
−
sc_lv<BITNIDTH> NAME[,NAME ]...;
+
−
sc_logic buf(sc_dt::Log_Z);
+
−
sc_lv<8> data_drive ("zz01XZ1Z");
+
−
data_drive.range (5,4) = "ZZ";// ZZZZXZ1Z
+
−
buf = '1';
+
  
−
</source>
+
[[Файл:Code quality-vs-functionality.png|center|400px]]
  
−
===Слайд:Операторы SystemC ===
+
==Слайд: Полнота покрытия ==
−
[[Файл:Операции.png]]
+
  
−
===Слайд:Главный модуль MAIN===
+
* {{X|24px}}В реальных условия обычно полный перебор {{Кр|'''<big>невозможен</big>'''}}
−
{{Гол|'''<big>Описание на языке C++</big>'''}}
+
* {{V|24px}}Поэтому поступают следующим образом. Например для сумматора:
−
<source lang="cpp">
+
# Тестируют как {{Фио|'''"Серый ящик"'''}} и проверяют простейшие случаи 0+0, 0+1, FFFF+FFFF, 0+FFFF
−
int main(int argc, char* argv[]) {
+
# Затем целенаправленно проверяют граничные условия - переполнение, перенос
−
BODY_OF_PROGRAM
+
# Затем тестирую как {{Фио|'''"Черный ящик"'''}} на случайном наборе тестов
−
return EXIT_CODE; //
+
# Оценивают полноту проверки модели
−
}
+
−
</source>
+
  
−
{{Гол|'''<big>Описание на языке SystemC</big>'''}}
+
==Слайд: Метрики оценки полноты тестов==
−
<source lang="cpp">
+
{{ЖЛампа|24px}}'''Необходимое условие''' : Управляемость (выполняется строка или переход)
−
int sc_main(int argc, char* argv[]) {
+
−
//ELABORATION
+
−
sc_start(); // <-- Simulation begins & ends
+
−
            // in this function!
+
−
//[POST-PROCESSING]
+
−
return EXIT_CODE; //
+
−
}
+
−
</source>
+
  
−
===Слайд: Модуль ===
+
{{ЖЛампа|24px}}'''Достаточное условие''' : Наблюдаемость (результат исполнения влияет на выход сравниваемый с эталоном)
−
<source lang="cpp">
+
−
#include <systemc.h>
+
−
SC_MODULE(module_name) {
+
−
MODULE_BODY
+
−
};</source>
+
−
Содержит:
+
−
* '''{{Фио|<big>Порты</big>}}'''
+
−
* '''{{Фио|<big>Каналы связи</big>}}'''
+
−
* '''{{Фио|<big>Объявления переменных для хранения данных</big>}}'''
+
−
* '''{{Фио|<big>Другие модули с большей вложенностью</big>}}'''
+
−
* '''{{Фио|<big>Конструктор</big>}}'''
+
−
* '''{{Фио|<big>Деструктор</big>}}'''
+
−
* '''{{Фио|<big>Функции -процессы</big>}}'''
+
−
* '''{{Фио|<big>Вспомогательные функции</big>}}'''
+
  
−
===Слайд: Конструктор (SC_CTOR)===
+
* {{Сн|'''<big>Эвристические метрики </big>'''}} - основанные на статистике появления ошибок
−
<source lang="cpp">SC_CTOR(module_name)
+
* {{Сн|'''<big>Программные метрики </big>'''}}
−
: Initialization // OPTIONAL
+
* {{Сн|'''<big>Автоматно-метрический подход </big>'''}}(лучший вариант использовать формальную верификацию для автоматов)
−
{
+
* {{Сн|'''<big>Моделирование неисправностей </big>'''}}(в модель вносится неисправность)
−
Subdesign_Allocation
+
* {{Сн|'''<big>Мониторинг событий</big>'''}}
−
Subdesign_Connectivity
+
−
Process_Registration
+
−
Miscellaneous_Setup
+
−
}</source>
+
  
−
* '''{{Фио|<big>Объявление под модулей</big>}}'''
+
==Слайд: Эвристические метрики ==
−
* '''{{Фио|<big>Подключение и соединение с подмодулями</big>}}'''
+
−
* '''{{Фио|<big>Регистрация процессов на SystemC</big>}}'''
+
−
* '''{{Фио|<big>Обеспечение постоянной чувствительности</big>}}'''
+
−
* '''{{Фио|<big>Разнообразные пользовательские объявления</big>}}''
+
  
−
===Слайд: Конструктор (SC_HAS_PROCESS)===
+
* Календарное время между моментами обнаружения ошибок проекта (к концу процесса верификации оно увеличивается);
−
<source lang="cpp">
+
* Общее количество промоделированных тактов работы проектируемого устройства;
−
//FILE: module_name.h
+
* Общее число обнаруженных ошибок в проекте и т.д.
−
SC_MODULE(module_name) {
+
* Число обнаруженных ошибок в день, неделю, месяц
−
SC_HAS_PROCESS(module_name);
+
−
module_name(sc_module_name instname[, other_args…])
+
−
: sc_module(instname)
+
−
[, other_initializers]
+
−
{
+
−
CONSTRUCTOR_BODY
+
−
}
+
−
};</source>
+
  
−
* '''{{Фио|<big>Все возможности конструктора SC_CTOR</big>}}'''
+
==Слайд: Программные метрики ==
−
* '''{{Фио|<big>Альтернативный метод создания модуля</big>}}'''
+
* '''Полнота покрытия тестом строк кода модели'''
−
* '''{{Фио|<big>Позволяет создавать конструктор с аргументами(+ к имени модуля)</big>}}'''
+
* '''Полнота покрытия переходов''' (число пополнений ветвей оператора if и case )
−
* '''{{Фио|<big>Используется, если желаете расположить конструктор в файле описания .cpp (не в файле .h)</big>}}'''
+
* '''Полнота покрытия путей ''(Branch coverage)''''' (все пути в графе программы)
 +
* '''Полнота покрытия выражений ''(Expression coverage)''''' (оценка числа вычислений выражения по различных наборах)
 +
* '''Полнота переключений из 0 в 1 и из 1 в 0 каждого бита ''(Toggle coverage)'''''
  
−
===Слайд: Процесс SC_THREAD ===
+
== Слайд: Метрики в ModelSim ==
  
−
<source lang="cpp">
+
<slides split="-----" width="600" >
−
SC_MODULE(simple_process_ex) {
+
{{V|24px}} В '''ModelSim''' для учета метрик покрытия при компиляции проекта нужно задать в меню '''Compile->Compiler option''' опции покрытия
−
  SC_CTOR(simple_process_ex) {
+
[[Файл:Опции компиляции покрытия.jpg|center]]
−
      SC_THREAD(my_thread_process);
+
−
  }
+
−
  void my_thread_process(void);
+
−
};</source>
+
  
−
{{Зел|'''SC_THREAD'''}} в '''SystemC''':
+
</slides>
−
# аналог {{Зел|'''initial block'''}} в '''Verilog'''
+
−
# {{Зел|'''process'''}} без списка чувствительности с оператором '''wait()''' в '''VHDL'''.
+
  
−
===Слайд:Введение времени===
+
== Слайд: Виды покрытия кода в ModelSim ==
  
−
{{Ор|<big>'''Единицы измерения времени'''</big>}}
+
* {{Сн|'''Statement coverage'''}} — покрытие состояний
  
−
<source lang="cpp">
+
* {{Сн|'''Branch coverage'''}} — покрытие ветвлений
−
SC_SEC // seconds
+
−
SC_MS  // milliseconds
+
−
SC_US  // microseconds
+
−
SC_NS  // nanoseconds
+
−
SC_PS  // picoseconds
+
−
SC_FS  // femtoseconds
+
−
</source>
+
−
{{Ор|<big>'''Объявление переменной типа '''</big>}}{{Зел|<big>'''sc_time'''</big>}}
+
−
<source lang="cpp">
+
−
sc_time t_PERIOD(5, SC_NS) ;
+
−
sc_time t_TIMEOUT (100, SC_MS) ;
+
−
sc_time t_MEASURE, t_CURRENT, t_LAST_CLOCK;
+
−
t_MEASURE = (t_CURRENT-t_LAST_CLOCK) ;
+
−
if (t_MEASURE > t_HOLD) { error ("Setup violated") }
+
−
</source>
+
  
 +
* {{Сн|'''Condition coverage'''}} — покрытие условий
  
−
===Слайд:Запуск выполнения '''sc_start()'''===
+
* {{Сн|'''Expression coverage'''}} — покрытие выражений
  
−
{{Ор|<big>'''Функция запускающая выполнения главного процесса '''</big>}}
+
* {{Сн|'''Toggle coverage'''}} — покрытие принимаемых значений
  
−
{{Сн|'''Пример запуска моделирования на 60 секунд модельного времени'''}}
+
* {{Сн|'''FSM coverage'''}} — покрытие состояний автомата
  
−
<source lang="cpp">
+
== Слайд: Мониторинг покрытия кода в ModelSim ==
−
int sc_main(int argc, char* argv[]) { // args unused
+
−
simple_process_ex my_instance ("my_instance");
+
−
sc_start(60.0,SC_SEC); // Limit sim to one minute
+
−
return 0 ;
+
−
}</source>
+
  
−
===Слайд:Контроль текущего времени моделирования '''sc_time_stamp ()'''===
 
−
 
−
<source lang="cpp">
 
−
std::cout << " The time is now "
 
−
<< sc_time_stamp()
 
−
<< "!" << std::endl;</source>
 
−
 
−
После запуска моделирования в консоли получим
 
−
The time is now 0 ns! 
 
−
 
−
 
−
===Слайд: Остановка выполнения моделирования wait(sc_time)===
 
−
 
−
 
−
{{Ор|<big>'''Функция останавливающая выполнение процесса до заданного времени или до прихода события'''</big>}}
 
−
 
−
<source lang="cpp">
 
−
void simple_process_ex::my_thread_process (void) {
 
−
wait (10,SC_NS);
 
−
std::cout<< "Now at "<< sc_time_stamp() << std::endl;
 
−
sc_time t_DELAY(2,SC_MS); // keyboard debounce time
 
−
t_DELAY *= 2;
 
−
std::cout<< "Delaying "<< t_DELAY<< std::endl;
 
−
wait(t_DELAY);
 
−
std::cout << "Now at " << sc_time_stamp()
 
−
<< std::endl;
 
−
}</source>
 
−
 
−
% . /run_example
 
−
Now at 10 ns
 
−
Delaying 4 ms
 
−
Now at 4000010 ns
 
−
 
−
===Слайд:События '''sc_event'''===
 
 
<slides split="-----" width="400" >
 
<slides split="-----" width="400" >
−
[[Файл:Процес_моделирования_по_событиям.png]]
+
[[Файл:Отметки_о_покрытие_строк_кода.jpg]]
 +
-----
 +
[[Файл:Отчет_по_покрытию.jpg]]
 +
-----
 +
[[Файл:Отчет_по_покрытию_2.jpg]]
 +
-----
 +
[[Файл:Детали_по_оттчеты_по_покрытию_кода.jpg]]
 
</slides>
 
</slides>
  
−
===Слайд:События '''SC_THREAD::wait()'''===
+
==Слайд: Команды ModelSim для работы с покрытием ==
−
Процесс '''SC_THREAD''' процес выполняющийся {{Кр|'''<big>один раз!!</big>'''}}, для управления работой такого процесса используют функцию задержки выполнения wait
+
  
−
<source lang="cpp">wait(time);
+
{{Сн|<big>'''Команда для компиляции'''</big>}}
−
wait(event);
+
−
wait(event1 | event2) // до прихода любого из событий
+
−
wait(event1 & event2) // до прихода всех событий вместе
+
−
wait(timeout, event); // до прихода события ожидает в течении времени
+
−
wait ( timeout, event1 | event2 )
+
−
wait ( timeout, event1 & event2 )
+
−
wait(); // ожидание дельта цикла выполнения, статическая задержка
+
−
</source>
+
−
===Слайд:Запуск события (установка,назначение)===
+
  
−
Для запуска события используется атрибут {{Зел|<big>'''.notify()'''</big>}}
+
vcom +{{Зел|'''cover'''}}={{Гол|'''bcsxf'''}} -work $wlibname $name
  
−
Он выполняет запуск событий,  отсчет времени идет от запуска моделирования. Для сброса точки отсчета используют {{Зел|<big>'''.cancel()'''</big>}}
+
Ключевое слово {{Зел|'''+cover'''}} и после него строка из букв каждая из которых значит следующее:
  
−
<source lang="cpp">sc_event action;
+
# '''b''' - покрытие ветвлений
−
sc_time now(sc_time_stamp()); //вытягиваем текущее время моделирования
+
# '''c''' - покрытие условий
−
//стартуем событие немедленно
+
# '''s''' - покрытие состояний
−
action.notify();
+
# '''x''' - покрытие принимаемых битами значений ( 0\1\Z )
−
//следующее событие через 20 ms от текущего момента
+
# '''t''' - покрытие принимаемых битами значений ( 0\1 )
−
action.notify(20, SC_MS);
+
# '''f''' - покрытие состояний конечного автомата
−
//переопределим событие на время 1.5 ns от текущего момента
+
−
action.notify(1.5,SC_NS);
+
−
//продублируем событие (не имеет эффекта)
+
−
action.notify(1.5, SC_NS);
+
−
//зададим событие от предыдущего на 1.5 ns
+
−
action.notify(3.0,SC_NS);
+
−
//запустим дельта цикл (не имеет эффекта)
+
−
action.notify(SC_ZERO_TIME);
+
−
//сбросим время задания события
+
−
action.cancel();
+
−
//зададим событие на 20 fs после сброса
+
−
action.notify(20,SC_FS);</source>
+
  
−
===Слайд:Процесс со списком чувствительности SC_METHOD ===
+
==Слайд: Команды ModelSim для работы с покрытием ==
−
{{ЖЛампа|24px}}Аналог '''process''' в '''VHDL'''
+
<slides split="-----" width="600" >
 +
[[Файл:Запуск_моделирования.jpg]]
 +
</slides>
  
−
<source lang="cpp">SC_METHOD(process_name);</source>
+
==Слайд: Команды ModelSim для работы с покрытием ==
  
−
{{ЖЛампа|24px}}Список чуствительности задаеться после ключевого слова {{Зел|'''sensitive'''}}
+
{{ЖЛампа|24px}}{{Сн|<big>'''Для запуска моделирования с покрытием нужно включить следующие опции:'''</big>}}  
  
−
<source lang="cpp"> sensitive << event [<< event] ;// поточный стил
+
  '''Simulate->Start Simulation''' на закладке other поставить птичку '''enable code coverage'''
−
  sensitive (event [, event] ); // стиль с использованием функции</source>
+
  
 +
{{Сн|<big>'''Команда для запуска'''</big>}}
  
−
===Слайд:dont_initialize() ===
+
'''vsim -coverage'''
−
{{ЖЛампа|24px}} Отменяет начальную установку значений
+
−
* После запуска моделирования конструктор создает модуль и инициализирует все процессы и переменные.
+
  
−
* Это заставляет выполниться всем методам работающим по событию по одному разу во время запуска если событие устанавливалось в значение.
+
{{ЖЛампа|24px}}{{Сн|<big>'''Для того чтобы база данных с информацие по покрытию сохранялась в файл после завершения моделирования, нужно выполнить след команду:'''</big>}}
  
−
* Для исключения начального выполнения используется функция '''dont_initialize()'''
+
'''coverage save -onexit'''
  
−
===Слайд: Стек событий '''sc_event_queue'''===
+
==Слайд: Верификация на основе утверждений ==
 +
<big>'''Позволяет контролировать'''</big>:
  
−
{{ЖЛампа|24px}}  Событие можно задать не только от начального момента времени, а и от текущего.
+
* {{Сн|'''Булева логика'''}} (Boolean logic) - тестирует основные утверждения (statements) о проекте.
 +
* {{Сн|'''Временная логика'''}} (Temporal logic) - добавляет временное измерение (dimension) в булеву логику (Boolean logic) и тестирует отсутствие (absence), наличие (presence), неизменность/повторяемость (persistence), последовательность (sequence), и прочее определённых событий.
 +
* {{Сн|'''Свойства/утверждения'''}} (Property) - это формальное описание поведения проекта, взятое из спецификации проекта и выраженное в терминах временной логики (temporal logic).
 +
Могут быть выражены с помощью PSL (Property Specification Language – теперь включен в VHDL) или с помощью SVA (подмножество SystemVerilog Assertions – работает с VHDL через модули проверок (checker modules)).
 +
* {{Сн|'''Последовательности'''}} (Sequences) являются простейшей формой свойств/утверждений, представляющие последовательность событий/состояний.\
  
−
Для этого используется функция '''sc_event_queue()'''
+
{{ЖЛампа|24px}} Assertions – работает с VHDL через модули проверок (checker modules)).
  
−
<source lang="cpp">
+
==Слайд:  Пример верификации на основе утверждений ==
−
sc_event_queue action;
+
* Можно вставлять PSL код в '''специальные комментарии''' в VHDL; таким образом, этот код не будет оказывать влияния на синтез и похожие программы.  
−
sc_time now(sc_time_stamp());
+
* Можно задать  '''последовательности (sequences)''' для представления разных фаз задаваемого свойства.  
−
action.notify(20, SC_MS);
+
* Конечное описания '''свойства (property)''' объединяет эти последовательности.  
−
action.notify(1.5,SC_NS);
+
* Помеченная меткой '''директива cover''' показывает симулятору, как проверять это свойство.  
−
action.notify(1.5,SC_NS);
+
−
action.notify(3.0,SC_NS);
+
−
action.notify(SC_ZERO_TIME);
+
−
action.notify(1,SC_SEC);
+
−
action.cancel_all();
+
−
</source>
+
  
−
===Слайд:Совместное использование ресурсов===
+
--@clk  rising_edge(CLK);
 +
--@psl  sequence ack35_s is { rose(ACK) : (ACK='1')[*3 to 5] } ;
 +
--@psl  sequence dvalid24_s is { rose(DVALID) : (DVALID='1')[*2 to 4] } ;
 +
--@psl  sequence dvalid2inf_s is { fell(ACK) : (DVALID='1')[*2 to inf] } ;
 +
--@psl  property ackdvalid_p is { ack35_s ; dvalid24_s ; dvalid2inf_s } ;
 +
--@psl  ackdvalid_c: cover(ackdvalid_p) report "Sequence ACK/DVALID covered!";
  
−
* При совместном использовании ресурсов, шин, памяти нужно разграничить область полномочий каждого процесса.
+
==Слайд: Запуск моделирования в ModelSim с верификацией на основе утверждений ==
−
* Иначе при одновременной, к примеру записи будет происходить сбой или некорректная запись.
+
−
Если управлением доступом к одному ресурсу
+
−
<source lang="cpp">sc_mutex NAME;
+
−
// блокируем mutex NAME (ждем пока разблокируется)
+
−
NAME.lock();
+
−
// Возвращает статус состояния блокировки
+
−
NAME.try lock()
+
−
// Снимает блокировку
+
−
NAME.unlock();</source>
+
  
−
Если управлением доступом к нескольким ресурсам
+
{{Сн|'''Для компиляции проекта содержащего файл верификации утверждений выполняем команду:'''}}
  
−
<source lang="cpp">sc_semaphore NAME(COUNT);
+
'''vcom''' -93 DIGITAL_BLOCK.vhd '''-pslfile''' DIGITAL_PSL.psl
−
// блокируем mutex NAME (ждем пока разблокируеться)
+
−
NAME.wait();
+
−
// Возвращает статус состояния блокировки
+
−
NAME.trywait()
+
−
//Возвращает число свободных ресурсов
+
−
NAME.get_value()
+
−
// Снимает блокировку
+
−
NAME.post();</source>
+
  
 +
После параметра '''-pslfile'''e указываем имя или путь к файлу
  
−
===Слайд:Иерархия и структура проекта===
+
{{Сн|'''Для запуска моделирования проекта содержащего файл верификации утверждений выполняем команду:'''}}
−
[[Файл:Иерархия.png]]
+
−
 
+
−
===Слайд:Иерархия и структура проекта (sc_main)===
+
−
 
+
−
{{ЖЛампа|24px}}Подключение и создание {{Зел|<big>'''модуля'''</big>}} внутри '''главного''' модуля аналогично созданию {{Зел|<big>'''объекта'''</big>}} заданного{{Зел| <big>'''класса'''</big>}}
+
−
{{Фио|<big>'''Стандартная конструкция блока хранения информации для RFID'''</big>}}
+
−
{| cellspacing="0" cellpadding="0" border="1"
+
−
|
+
−
* {{Гол|'''Статический метод'''}}
+
−
<source lang="cpp">//FILE: main.cpp
+
−
#include "Wheel.h"
+
−
int sc_main(int argc, char* argv[]) {
+
−
Wheel wheel_FL("wheel_FL");
+
−
Wheel wheel_FR("wheel_FR");
+
−
sc_start();
+
−
}</source>
+
−
|
+
−
* {{Гол|'''Динамический метод'''}}
+
−
<source lang="cpp">//FILE: main.cpp
+
−
#include "Wheel.h"
+
−
int sc_main(int argc, char* argv[]) {
+
−
Wheel* wheel_FL; // pointer to FL wheel
+
−
Wheel* wheel_FR; // pointer to FR wheel
+
−
wheel_FL = new Wheel ("wheel_FL"); // create FL
+
−
wheel_FR = new Wheel ("wheel_FR"); // create FR
+
−
sc_start();
+
−
delete wheel_FL;
+
−
delete wheel_FR;
+
−
}</source>
+
−
|}
+
−
 
+
−
===Слайд:Иерархия и структура проекта (SC_MODULE)===
+
−
 
+
−
{{ЖЛампа|24px}}Подключение и создание {{Зел|<big>'''модуля'''</big>}} внутри другого модуля аналогично созданию {{Зел|<big>'''объекта'''</big>}} заданного{{Зел| <big>'''класса'''</big>}}, внутри другого класса. Поэтому объявления производиться в конструкторе верхнего модуля
+
−
{| cellspacing="0" cellpadding="0" border="1"
+
−
|
+
−
 
+
−
* {{Гол|'''Статический метод'''}}
+
−
<source lang="cpp">//FILE:Body.h
+
−
#include "Wheel.h"
+
−
SC_MODULE(Body) {
+
−
Wheel wheel_FL;
+
−
Wheel wheel_FR;
+
−
SC_CTOR(Body)
+
−
: wheel_FL("wheel_FL"), //initialization
+
−
wheel_FR("wheel_FR") //initialization
+
−
{
+
−
// other initialization
+
−
}
+
−
};
+
−
}</source>
+
−
|
+
−
* {{Гол|'''Динамический метод'''}}
+
−
<source lang="cpp">//FILE:Body.h
+
−
#include "Wheel.h"
+
−
SC_MODULE(Body) {
+
−
Wheel* wheel_FL;
+
−
Wheel* wheel_FR;
+
−
SC_CTOR(Body) {
+
−
wheel_FL = new Wheel("wheel_FL");
+
−
wheel_FR = new Wheel("wheel_FR");
+
−
// other initialization
+
−
}
+
−
};
+
−
}</source>
+
−
|}
+
−
 
+
−
===Слайд:Порты - точки подачи и снятия внешних воздействий===
+
−
[[Файл:Порты_соединение_модулей.png]]
+
−
 
+
−
===Слайд:Типы портов ===
+
−
 
+
−
* {{Сн|'''sc_port'''}}  - аналог inout порта в языке VHDL
+
−
* {{Сн|'''sc_in'''}}    - аналог in порта в языке VHDL
+
−
* {{Сн|'''sc_out'''}}    - аналог out порта в языке VHDL
+
−
* {{Сн|'''sc_export'''}} - внешний порт, порт который позволяет получить доступ к private данным модуля, но иерархически модулю не принадлежит.
+
−
{{ЖЛампа|24px}} Механизм использования '''sc_export''' порта напоминает '''доступ к сигналам по иерархии''', как в '''VHDL-2008'''.
+
−
 
+
−
===Слайд:Порты - точки подачи и снятия внешних воздействий===
+
−
[[Файл:Порты_соединение_модулей_экспорт.png]]
+
−
[[Файл:Порты_соединение_модулей_экспорт2.png]]
+
−
 
+
−
===Слайд:Управление процессом и контроль статуса моделирования===
+
−
 
+
−
== Слайд: VHDL и SystemC конструкции ==
+
−
===Слайд: Entity ===
+
−
 
+
−
<slides split="-----" width="700" >
+
−
{| cellspacing="0" cellpadding="0" border="1"
+
−
|
+
−
{{Фио|'''<big></big>Пример поведенческой модели накопителя (VHDL)'''}}
+
−
<source lang="vhdl">
+
−
entity soft is
+
−
  generic (UART_Speed : integer := 115200;  -- UART Speed
+
−
          System_CLK : integer := 50000000;  -- System CLK in Hz
+
−
          comand_file : string :="/home/Vidokq/djin18reader/vhd/D18/comfile.txt"
+
−
          );
+
−
  port (
+
−
    CLK      : out  std_logic;                    -- system clk
+
−
    RST_N    : out  std_logic;                    -- system reset#   
+
−
    DATA_IN  : out  std_logic_vector(7 downto 0);  -- Transmit data
+
−
    DATA_OUT : in  std_logic_vector(7 downto 0);  -- Recieved data
+
−
    RX_VALID : in  std_logic;                    -- RX buffer data ready
+
−
    TX_VALID : out  std_logic;                    -- Data for TX avaible
+
−
    TX_BUSY  : in  std_logic;                    --
+
−
    RX_BUSY  : in  std_logic);
+
 
   
 
   
−
end soft;
+
'''vsim''' '''''имя_проекта'''''
−
</source>
+
  
−
|
+
Для отключения выполнения проверок используем параметр '''-nopsl'''
−
{{Фио|'''<big></big>Пример поведенческой модели накопителя (Verilog)'''}}
+
  
−
<source lang="cpp">
+
'''vsim''' '''''имя проекта''''' '''-nopsl'''
  
−
SC_MODULE (soft_sc_module)
 
−
{
 
−
  public :
 
−
    sc_in  < sc_logic >  tx_busy;
 
−
    sc_in  < sc_logic >  rx_busy;
 
−
    sc_in  < sc_lv < 8 > > data_out;
 
−
    sc_in  < sc_logic >  rx_valid;
 
−
    sc_out < sc_logic >  tx_valid;
 
−
    sc_out < bool >  clk;
 
−
    sc_out < sc_logic >  rst_n;
 
−
    sc_out < sc_lv < 8 > > data_in;
 
  
 +
==Слайд: Быстродействие и расход памяти ==
  
−
  public:
+
Кроме полноты тестирования, одной из важных характеристик тестирующей программы являются:
  
−
    ifstream fin;
+
* {{Зел|<big>'''Требуемая память'''</big>}}
 +
* {{Зел|<big>'''Расход машинного времени'''</big>}}
  
−
    SC_CTOR(soft_sc_module)
+
==Слайд: Требуемая память==
−
      : rst_n("rst_n"),
+
−
      data_in("data_in"),
+
−
      data_out ("data_out"),
+
−
      rx_valid("rx_valid"),
+
−
      tx_valid("tx_valid"),
+
−
      tx_busy("tx_busy"),
+
−
      rx_busy("rx_busy"),
+
−
      rst_n_i("rst_n_i"),
+
−
      clk_i("clk_i"),
+
−
      clk("clk")
+
−
      {
+
−
      }
+
−
    ~soft_sc_module()
+
−
      {
+
−
delete [] str_b;
+
−
      }
+
−
};
+
  
−
#endif
+
* Зависит от числа данных в программе
−
</source>
+
* Их размера (размерности)
−
|}
+
* От количества и сложности операторов
−
</slides>
+
  
−
===Слайд: Architecture ===
+
Пример:  
  
−
<slides split="-----" width="700" >
+
{{ЖЛампа|24px}}Данные типа {{Кр|'''signal'''}} в VHDL занимают {{Кр|'''на порядок!! больше'''}} места, чем {{Зел|'''variable'''}}, поэтому массивы данных большого объема в тестирующих модулях лучше объявлять с использованием '''variable'''.
−
{| cellspacing="0" cellpadding="0" border="1"
+
−
|
+
−
{{Фио|'''<big></big>Пример Архитектуры на VHDL'''}}
+
−
<source lang="vhdl">
+
  
−
architecture beh of soft is
+
{{ЖЛампа|24px}}Verilog расходует {{Кр|'''обычно'''}} в 4 раза меньше памяти на хранение одного бита данных, чем VHDL.
−
  file comfile : text open read_mode is comand_file;
+
−
 
+
−
begin  -- beh
+
−
-- тело архитектуры
+
−
  signal str        : string(1 to 1000) := (others => ' ');
+
−
  signal RST_N_i    : std_logic;
+
−
  signal DATA_IN_i  : std_logic_vector(7 downto 0);
+
−
  signal f_get_answer      : boolean := false;
+
−
  signal tmd : time := 0 ms;
+
  
−
end beh;
+
==Слайд: Сокращение расхода машинного времени==
−
</source>
+
  
−
|
+
# '''Профилирование''' - эффективня организация тестирующей программы
−
{{Фио|'''<big></big>Пример аналогичной конструкции на SystemC'''}}
+
# Использование '''систем и языков''' предназначенных для '''верификации'''
 +
# Выбор более быстрой системы моделирования (вместо интерпретатора '''компилятор''')
 +
# Использование более '''мощной ЭВМ'''
 +
# '''Ограничение''' множества '''входных''' наборов '''тестов''' ({{Зел|'''''нет ничего мощнее здравого смысла'''''}})
 +
# Использование '''аппаратных ускорителей''' моделирования (10-100раз)
 +
# Использование '''прототипов''' схем '''для прогонов тестов''' (на этапе отладки тестов)
  
−
<source lang="cpp">
+
{{ЖЛампа|24px}}{{Зел|'''<big>Пример:  </big>'''}}
−
SC_MODULE (soft_sc_module)
+
−
{
+
−
  public :
+
−
    std::string comand_file;
+
−
  public :
+
−
    sc_signal< sc_logic >    rst_n_i;
+
−
    sc_signal< sc_lv < 8 > > data_in_i;
+
−
    sc_signal < bool > f_get_answer;
+
−
    sc_signal < sc_time > tmd;
+
−
    sc_time btmd (0, SC_MS);
+
−
  SC_CTOR(soft_sc_module)
+
−
      :
+
−
      rst_n_i("rst_n_i"),
+
−
      data_in_i("data_in_i"),
+
−
      f_get_answer("f_get_answer"),
+
−
      tmd("tmd")
+
−
      {  
+
−
      str = new char [1000];
+
−
//объявление функций
+
−
//выбор списка чувствительности
+
−
//установка значений по умолчанию
+
−
      tmd.write(btmd);
+
−
      // tmd = btmd;
+
−
//оператор присваивания перегружен и выолнит вызов функции write
+
−
      }
+
−
    ~soft_sc_module()
+
−
      {
+
−
delete [] str;
+
−
      }
+
−
</source>
+
−
|}
+
−
</slides>
+
  
−
===Слайд: Generic ===
+
{{Зел|'''<big>1. Три отдельных процесса требуют больше времени, чем те же операции объединенные в один процесс.</big>'''}}
−
 
+
−
<slides split="-----" width="700" >
+
−
{| cellspacing="0" cellpadding="0" border="1"
+
−
|
+
−
{{Фио|'''<big></big>Пример на VHDL'''}}
+
−
<source lang="vhdl">
+
−
entity soft is
+
−
  generic (UART_Speed : integer := 115200; 
+
−
          System_CLK : integer := 50000000
+
−
          );
+
−
--
+
−
--
+
−
--
+
−
architecture beh of soft is
+
−
CLK_i <= not CLK_i after 1 ns * (1000000000 / System_CLK );
+
−
end beh;
+
−
</source>
+
−
 
+
−
|
+
−
{{Фио|'''<big></big>Пример на SystemC (sc_get_param)'''}}
+
−
 
+
−
<source lang="cpp">
+
−
SC_MODULE (soft_sc_module)
+
−
{
+
−
public:
+
−
    SC_CTOR(soft_sc_module)
+
−
      : rst_n("rst_n"),
+
−
      tmd("tmd")
+
−
      {
+
−
if (!sc_get_param("System_CLK",System_CLK)) cout << "error get generic";
+
−
if (!sc_get_param("UART_Speed",UART_Speed)) cout << "error get generic";
+
−
period_ns=(1000000000)/System_CLK;
+
−
str = new char [1000];
+
−
    }
+
−
    ~soft_sc_module()
+
−
      {
+
−
delete [] str_b;
+
−
      }
+
−
};
+
−
</source>
+
−
|}
+
−
</slides>
+
−
 
+
−
===Слайд: Process без списка чувствительности ===
+
−
 
+
−
<slides split="-----" width="700" >
+
−
{| cellspacing="0" cellpadding="0" border="1"
+
−
|
+
−
{{Фио|'''<big></big>Пример на VHDL'''}}
+
−
<source lang="vhdl">
+
−
wait_byte_timer: process
+
−
begin  -- process wiat_timer
+
−
  wait for 0.5 ms;
+
−
  if (NOW - tmd) > 1 ms then
+
−
    if f_start_get_answer then
+
−
      f_byte_timer <= true;
+
−
      wait for 0.1 ms;
+
−
      f_byte_timer <= false;   
+
−
    end if;
+
−
  end if;
+
−
end process wait_byte_timer;
+
−
</source>
+
−
 
+
−
|
+
−
{{Фио|'''<big></big>Пример на SystemC'''}}
+
−
 
+
−
<source lang="cpp">
+
−
SC_MODULE (soft_sc_module)
+
−
{
+
−
public:
+
−
    SC_CTOR(soft_sc_module):
+
−
      { SC_METHOD (wait_byte_timer); }
+
−
    ~soft_sc_module()
+
−
      {      }
+
−
};
+
−
void soft_sc_module :: wait_byte_timer ()
+
−
{
+
−
  next_trigger (0.5,SC_MS);
+
−
  if ((sc_time_stamp()-tmd) > sc_time(1, SC_MS) )
+
−
    if (f_start_get_answer)
+
−
      {f_byte_timer=true;
+
−
      next_trigger (0.1,SC_MS);
+
−
      f_byte_timer=false;
+
−
      }
+
−
  cout<< "wait_byte_timer work\n";
+
−
}
+
−
</source>
+
−
|}
+
−
</slides>
+
−
 
+
−
===Слайд: Process со списком чувствительности (пример 1)===
+
−
 
+
−
<slides split="-----" width="700" >
+
−
{| cellspacing="0" cellpadding="0" border="1"
+
−
|
+
−
{{Фио|'''<big></big>Пример на VHDL'''}}
+
−
<source lang="vhdl">
+
−
CLK_i <= not CLK_i after 1 ns * (1000000000 / System_CLK );
+
−
--или
+
−
process (clk)
+
−
begin
+
−
if clk'event then
+
−
clk_i <= not clk_i after 1 ns * (1000000000 / System_CLK );
+
−
end if;
+
−
end process;
+
−
</source>
+
−
|
+
−
{{Фио|'''<big></big>Пример на SystemC'''}}
+
−
 
+
−
<source lang="cpp">
+
−
SC_MODULE (soft_sc_module)
+
−
{
+
−
public:
+
−
    SC_CTOR(soft_sc_module):
+
−
      { clk_i=true;
+
−
        period_ns=(1000000000)/System_CLK;
+
−
        SC_METHOD (clk_gen);
+
−
      }
+
−
    ~soft_sc_module()
+
−
      {      }
+
−
};
+
−
 
+
−
void soft_sc_module :: clk_gen ()
+
−
{
+
−
  clk_i.write(!clk_i.read());
+
−
  next_trigger (period_ns, SC_NS);
+
−
 
+
−
}
+
−
</source>
+
−
|}
+
−
</slides>
+
−
 
+
−
===Слайд: Process со списком чувствительности (пример 2) ===
+
−
 
+
−
<slides split="-----" width="700" >
+
−
{| cellspacing="0" cellpadding="0" border="1"
+
−
|
+
−
{{Фио|'''<big></big>Пример на VHDL'''}}
+
−
<source lang="vhdl">
+
−
  RST_N <= RST_N_i;
+
−
--или
+
−
process (RST_N_i)
+
−
begin
+
−
if RST_N_i'event then
+
−
  RST_N <= RST_N_i;
+
−
end if;
+
−
end process;
+
−
</source>
+
−
|
+
−
{{Фио|'''<big></big>Пример на SystemC'''}}
+
−
 
+
−
<source lang="cpp">
+
−
SC_MODULE (soft_sc_module)
+
−
{
+
−
public:
+
−
    SC_CTOR(soft_sc_module):
+
−
      { clk_i=true;
+
−
SC_METHOD (rst_n_i2rst_n);
+
−
sensitive << rst_n_i;
+
−
dont_initialize();
+
−
      }
+
−
    ~soft_sc_module()
+
−
      {      }
+
−
};
+
−
 
+
−
void soft_sc_module :: reset_gen ()
+
−
{
+
−
  rst_n_i.write( SC_LOGIC_0 );
+
−
  wait (100, SC_NS);
+
−
  cout << "run reset";
+
−
  rst_n_i.write( SC_LOGIC_1 );
+
−
}
+
−
</source>
+
−
|}
+
−
</slides>
+
−
 
+
−
===Слайд: Работа с файлами ===
+
−
<slides split="-----" width="700" >
+
−
{| cellspacing="0" cellpadding="0" border="1"
+
−
|
+
−
{{Фио|'''<big></big>Пример на VHDL'''}}
+
−
<source lang="vhdl">
+
−
  p_send      : process
+
−
  variable l : line;
+
−
  variable byte_r : std_logic_vector(0 to 7);
+
−
  variable good : boolean;
+
−
  variable f_first_byte : boolean:=false;   
+
−
  begin  -- process p1
+
−
 
+
−
    loop1: while not endfile(comfile) loop
+
−
 
+
−
      readline (comfile,l);
+
−
      skip_space (l);                 
+
−
      next loop1 when l'length = 0;   
+
−
   
+
−
      for i in 1 to l'length loop
+
−
        str(i) <= l(i);
+
−
      end loop;  -- i
+
−
      str((l'length)+1 to 1000) <= (others => ' ');
+
−
      str_l <= l'length;
+
−
</source>
+
−
| 
+
−
<source lang="vhdl"> 
+
−
      if l(1) = '#' then               
+
−
        assert false report "коментарий:"&str(1 to str_l) severity NOTE;
+
−
      else                             
+
−
        assert false report "коментарий"&str(1 to str_l) severity NOTE;
+
−
        f_first_byte := true;
+
−
        while l'length /= 0 loop
+
−
          hread (l,byte_r,good);
+
−
          assert good report "ошибка" severity FAILURE;
+
−
          if f_first_byte then
+
−
            f_first_byte := false;     
+
−
            comand <= byte_r;
+
−
          end if;
+
−
          TX_VALID_i <= '1';
+
−
          DATA_IN_i <= byte_r;
+
−
          skip_space (l);     
+
−
          wait until TX_BUSY = '1';
+
−
        end loop;
+
−
        f_start_timer <= true;
+
−
        TX_VALID_i <= '0';           
+
−
        wait until f_get_answer or f_timer;     
+
−
        assert not f_timer report "1мкс" severity FAILURE;
+
−
        f_start_timer <= false;
+
−
      end if;     
+
−
    end loop;
+
−
  assert false report "======" severity failure;
+
−
  end process p_send;
+
−
</source>
+
−
|}
+
−
</slides>
+
−
 
+
−
===Слайд: Работа с файлами ===
+
−
<slides split="-----" width="700" >
+
−
{| cellspacing="0" cellpadding="0" border="1"
+
−
|
+
−
{{Фио|'''<big></big>Пример на SystemC'''}}
+
−
<source lang="cpp">
+
−
void soft_sc_module :: p_send ()
+
−
{
+
−
  fin.open(comand_file.c_str(),ios::out);
+
−
  cout << "work4\n";
+
−
  bool f_first_byte=false;
+
−
  if (!fin){
+
−
    std::cout << "File invalide open";
+
−
    exit (0);
+
−
  }
+
−
  while (!fin.eof()){
+
−
    fin.getline (str,1000);
+
−
    skip_space (&(str));     
+
−
    if (strlen(str)){       
+
−
      if (str[0] == '#')
+
−
cout << "koment: "<< str <<endl;
+
−
      else {
+
−
cout << "data: "<< str <<endl;
+
−
f_first_byte=true;
+
−
//while ( str[0] != '\0' ){
+
−
while ( strlen(str) ){
+
−
  if ( str[0] == ' ' )
+
−
    skip_space(&(str));
+
−
  else {
+
−
    //cout << "1/2\n";
+
−
    byte_b.range(7,4)=str[0];
+
−
    str++;
+
−
    skip_space(&(str));
+
−
    if (!strlen(str)){
+
−
      cout<<endl<<"error";
+
−
      sc_stop();
+
−
    }
+
−
    else {
+
−
      //cout << "2/2\n";
+
−
      byte_b.range(3,0)=str[0];
+
−
      str++;
+
−
              }
+
−
</source>
+
−
|
+
−
<source lang="cpp">
+
−
   
+
−
    if (f_first_byte){
+
−
      f_first_byte=false;
+
−
      comand=byte_b;
+
−
    }
+
−
    //cout << byte_b << endl;
+
−
    tx_valid_i.write(SC_LOGIC_1);
+
−
    data_in.write(byte_b);
+
−
    wait (tx_busy.posedge_event());
+
−
  }
+
−
}
+
−
f_start_timer = true;
+
−
tx_valid_i.write(SC_LOGIC_0);
+
−
wait ( f_get_answer.posedge_event() | f_timer.posedge_event() );
+
−
if ( f_timer ) {cout << "error";sc_stop();}
+
−
f_start_timer = false;
+
−
      }
+
−
      }
+
−
    str=str_b;
+
−
  }
+
−
  cout << "error";
+
−
  fin.close();
+
−
  sc_stop();
+
−
}
+
−
</source>
+
−
|}
+
−
</slides>
+
−
 
+
−
===Слайд: Работа с функциями ===
+
−
<slides split="-----" width="600" >
+
−
{| cellspacing="0" cellpadding="0" border="1"
+
−
|
+
−
{{Фио|'''<big></big>Пример на VHDL'''}}
+
−
<source lang="vhdl">
+
−
entity soft is
+
−
end soft;
+
−
 
+
−
architecture beh of soft is
+
−
 
+
−
  procedure skip_space (variable l : inout line) is
+
−
    variable char : character;
+
−
    variable flag : boolean:=true;
+
−
  begin  -- skip_space
+
−
    while flag loop
+
−
      if l'length = 0 then
+
−
        flag := false;
+
−
      elsif l(1) = ' ' then
+
−
        read(l, char);
+
−
      else
+
−
        flag := false;
+
−
      end if;
+
−
    end loop;
+
−
  end skip_space;
+
−
end beh;
+
−
</source>
+
−
|
+
−
{{Фио|'''<big></big>Пример на SystemC'''}}
+
−
<source lang="cpp">
+
−
SC_MODULE (soft_sc_module)
+
−
{
+
−
public:
+
−
    SC_CTOR(soft_sc_module):
+
−
      { SC_METHOD (wait_byte_timer); }
+
−
 
+
−
    void skip_space (char ** str);
+
−
    ~soft_sc_module()
+
−
      {      }
+
−
};
+
−
void soft_sc_module :: skip_space (char ** str)
+
−
{
+
−
  bool flag = true;
+
−
 
+
−
  while ( flag ) {              //
+
−
    if ( !strlen((*str)) )
+
−
      flag = false;
+
−
    else
+
−
      if ((*str)[0]==' ')
+
−
(*str) += 1;
+
−
      else
+
−
flag = false;
+
−
    }   
+
−
}
+
−
 
+
−
</source>
+
−
|}
+
−
</slides>
+
  
−
===Слайд: Работа с сигналами ===
+
{{Зел|'''<big>2. Использование языков C,C++,SystemC позволяет не несколько раз снизить расход памяти</big>'''}}
−
===Слайд: Арифметические, логические, операции присваивания ===
+
−
===Слайд: Конструкции С++ ===
+
−
===Слайд: Создание модуля ===
+
−
===Слайд: Коммуникации между модулями ===
+
−
===Слайд: Управление процессом моделирования (сообщения, запуск останов моделирования)===
+
−
== Слайд: Компиляция описания ==
+
−
== Слайд: Запуск моделирования только SystemC описания ==
+
−
== Слайд: Запуск моделирования SystemC описания и VHDL ==
+

Текущая версия на 13:16, 2 декабря 2013

Лекции ИГСАПР
Лекции
Практические
Тесты
Лабораторные
Табель
Доп. материалы
Slide Show
Slide Show
Заголовок
Верификация описания.
Автор
Зайцев В.С.
Нижний колонтитул
Спец курс (Избранные главы VHDL)/Верификация описания
Дополнительный нижний колонтитул
Зайцев В.С., 13:16, 2 декабря 2013



Содержание

Слайд:Методы верификации проекта

  • Имитационная верификация - верификация с использованием моделирования
  • Формальная верификация -проверка модели с целью доказательства ее корректности и эквивалентности спецификации 
(Пример: пакет FormulPro ф. MentorGraphics, пакеты фирмы Verplex, www.verplex.com)


Слайд:Верификация описания

Процевв верификации.png

Слайд:Верификация описания:step

  • Среда моделирования
    • Active-HDL™
    • Riviera-PRO™
    • NC-Sim®
    • ModelSim®
    • QuestaSim®
    • VCS-MX®
  • Структура проекта
    • Тестовое окружение
    • RTL-модель (Verilog,VHDL)
    • Эталонная модель (SystemC)
    • Assert'ы (psl, OVVM, UVM)
    • Отчеты и базы по результатам моделирования


Слайд:Средства верификации

  • Прямые тесты (Directed tests)
  • Псевдослучайные тесты (Random tests)
  • Управляемые псевдослучайные тесты (Constrained Random tests)
  • Верификация управляемая покрытием (на основе покрытия) (Coverage driven verification)
    • Покрытие кода (Code coverage)
    • Функциональное покрытие (Functional coverage )
  • Верификация на основе утверждений (Assertion based verification)
  • Эмуляция (Emulation)
  • Формальная верификация (Formal verification)

Слайд: Типы тестов ФК

На что проверяем:
  • Детерминистский - Проверяет обычные режимы работы системы, а также функционирование в граничных условиях на основе фиксированного набора тестов
  • Случайный - Предполагает наличие генератора случайных входных воздействий
  • Транзакционный - Фиксирует внимание на проверке интерфейсов и прохождению пакетов данных через них 
Способ проведения проверки:
  • "Черный ящик"
  • "Серый ящик"
  • "Прозрачный ящик"

Слайд:Что такое покрытие (Coverage)?

  • Покрытие является крайне неоднозначным термином, когда используется сам по себе.
Информация

Покрытие в электронике (Coverage) является одной из разновидностей метрик проекта, которая сообщает, если определённые аспекты проекта были правильно выполнены во время процедуры тестирования.

  • Обычно уточняют термин покрытия, говоря какой аспект был протестирован:
    • Тестирование качества кода — покрытие кода (code coverage)
    • Проверка свойств/утверждений — покрытие свойств/утверждений (property coverage)
    • Сбор значений переменных проекта — функциональное покрытие (functional coverage).

Слайд:Покрытие кода vs. функциональное покрытие

Code quality-vs-functionality.png

Слайд: Полнота покрытия

  • Nuvola apps error.pngВ реальных условия обычно полный перебор невозможен
  • 200px-Yes check.pngПоэтому поступают следующим образом. Например для сумматора:
  1. Тестируют как "Серый ящик" и проверяют простейшие случаи 0+0, 0+1, FFFF+FFFF, 0+FFFF
  2. Затем целенаправленно проверяют граничные условия - переполнение, перенос
  3. Затем тестирую как "Черный ящик" на случайном наборе тестов
  4. Оценивают полноту проверки модели

Слайд: Метрики оценки полноты тестов

Bombilla amarilla - yellow Edison lamp.pngНеобходимое условие : Управляемость (выполняется строка или переход)

Bombilla amarilla - yellow Edison lamp.pngДостаточное условие : Наблюдаемость (результат исполнения влияет на выход сравниваемый с эталоном)

  • Эвристические метрики - основанные на статистике появления ошибок
  • Программные метрики
  • Автоматно-метрический подход (лучший вариант использовать формальную верификацию для автоматов)
  • Моделирование неисправностей (в модель вносится неисправность)
  • Мониторинг событий

Слайд: Эвристические метрики

  • Календарное время между моментами обнаружения ошибок проекта (к концу процесса верификации оно увеличивается);
  • Общее количество промоделированных тактов работы проектируемого устройства;
  • Общее число обнаруженных ошибок в проекте и т.д.
  • Число обнаруженных ошибок в день, неделю, месяц

Слайд: Программные метрики

  • Полнота покрытия тестом строк кода модели
  • Полнота покрытия переходов (число пополнений ветвей оператора if и case )
  • Полнота покрытия путей (Branch coverage) (все пути в графе программы)
  • Полнота покрытия выражений (Expression coverage) (оценка числа вычислений выражения по различных наборах)
  • Полнота переключений из 0 в 1 и из 1 в 0 каждого бита (Toggle coverage)

Слайд: Метрики в ModelSim

200px-Yes check.png В ModelSim для учета метрик покрытия при компиляции проекта нужно задать в меню Compile->Compiler option опции покрытия
Опции компиляции покрытия.jpg

Слайд: Виды покрытия кода в ModelSim

  • Statement coverage — покрытие состояний
  • Branch coverage — покрытие ветвлений
  • Condition coverage — покрытие условий
  • Expression coverage — покрытие выражений
  • Toggle coverage — покрытие принимаемых значений
  • FSM coverage — покрытие состояний автомата

Слайд: Мониторинг покрытия кода в ModelSim

Отметки о покрытие строк кода.jpg

Отчет по покрытию.jpg

Отчет по покрытию 2.jpg

Детали по оттчеты по покрытию кода.jpg

Слайд: Команды ModelSim для работы с покрытием

Команда для компиляции 

vcom +cover=bcsxf -work $wlibname $name

Ключевое слово +cover и после него строка из букв каждая из которых значит следующее:

  1. b - покрытие ветвлений
  2. c - покрытие условий
  3. s - покрытие состояний
  4. x - покрытие принимаемых битами значений ( 0\1\Z )
  5. t - покрытие принимаемых битами значений ( 0\1 )
  6. f - покрытие состояний конечного автомата

Слайд: Команды ModelSim для работы с покрытием

Запуск моделирования.jpg

Слайд: Команды ModelSim для работы с покрытием

Bombilla amarilla - yellow Edison lamp.pngДля запуска моделирования с покрытием нужно включить следующие опции: 

Simulate->Start Simulation на закладке other поставить птичку enable code coverage

Команда для запуска 

vsim -coverage

Bombilla amarilla - yellow Edison lamp.pngДля того чтобы база данных с информацие по покрытию сохранялась в файл после завершения моделирования, нужно выполнить след команду: 

coverage save -onexit

Слайд: Верификация на основе утверждений

Позволяет контролировать:

  • Булева логика (Boolean logic) - тестирует основные утверждения (statements) о проекте.
  • Временная логика (Temporal logic) - добавляет временное измерение (dimension) в булеву логику (Boolean logic) и тестирует отсутствие (absence), наличие (presence), неизменность/повторяемость (persistence), последовательность (sequence), и прочее определённых событий.
  • Свойства/утверждения (Property) - это формальное описание поведения проекта, взятое из спецификации проекта и выраженное в терминах временной логики (temporal logic).

Могут быть выражены с помощью PSL (Property Specification Language – теперь включен в VHDL) или с помощью SVA (подмножество SystemVerilog Assertions – работает с VHDL через модули проверок (checker modules)).

  • Последовательности (Sequences) являются простейшей формой свойств/утверждений, представляющие последовательность событий/состояний.\

Bombilla amarilla - yellow Edison lamp.png Assertions – работает с VHDL через модули проверок (checker modules)).

Слайд: Пример верификации на основе утверждений

  • Можно вставлять PSL код в специальные комментарии в VHDL; таким образом, этот код не будет оказывать влияния на синтез и похожие программы.
  • Можно задать последовательности (sequences) для представления разных фаз задаваемого свойства.
  • Конечное описания свойства (property) объединяет эти последовательности.
  • Помеченная меткой директива cover показывает симулятору, как проверять это свойство. 
--@clk  rising_edge(CLK);
--@psl  sequence ack35_s is { rose(ACK) : (ACK='1')[*3 to 5] } ;
--@psl  sequence dvalid24_s is { rose(DVALID) : (DVALID='1')[*2 to 4] } ;
--@psl  sequence dvalid2inf_s is { fell(ACK) : (DVALID='1')[*2 to inf] } ;
--@psl  property ackdvalid_p is { ack35_s ; dvalid24_s ; dvalid2inf_s } ;
--@psl  ackdvalid_c: cover(ackdvalid_p) report "Sequence ACK/DVALID covered!";

Слайд: Запуск моделирования в ModelSim с верификацией на основе утверждений

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

vcom -93 DIGITAL_BLOCK.vhd -pslfile DIGITAL_PSL.psl

После параметра -pslfilee указываем имя или путь к файлу

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

vsim имя_проекта

Для отключения выполнения проверок используем параметр -nopsl 

vsim имя проекта -nopsl


Слайд: Быстродействие и расход памяти

Кроме полноты тестирования, одной из важных характеристик тестирующей программы являются:

  • Требуемая память
  • Расход машинного времени

Слайд: Требуемая память

  • Зависит от числа данных в программе
  • Их размера (размерности)
  • От количества и сложности операторов

Пример:

Bombilla amarilla - yellow Edison lamp.pngДанные типа signal в VHDL занимают на порядок!! больше места, чем variable, поэтому массивы данных большого объема в тестирующих модулях лучше объявлять с использованием variable.

Bombilla amarilla - yellow Edison lamp.pngVerilog расходует обычно в 4 раза меньше памяти на хранение одного бита данных, чем VHDL.

Слайд: Сокращение расхода машинного времени

  1. Профилирование - эффективня организация тестирующей программы
  2. Использование систем и языков предназначенных для верификации
  3. Выбор более быстрой системы моделирования (вместо интерпретатора компилятор)
  4. Использование более мощной ЭВМ
  5. Ограничение множества входных наборов тестов (нет ничего мощнее здравого смысла)
  6. Использование аппаратных ускорителей моделирования (10-100раз)
  7. Использование прототипов схем для прогонов тестов (на этапе отладки тестов)

Bombilla amarilla - yellow Edison lamp.pngПример:

1. Три отдельных процесса требуют больше времени, чем те же операции объединенные в один процесс.

2. Использование языков C,C++,SystemC позволяет не несколько раз снизить расход памяти

Источник — «http://www.simhard.com/wiki/index.php?title=Спец_курс_(Избранные_главы_VHDL)/Верификация_описания&oldid=3558»