Спец курс (Избранные главы VHDL)/Верификация описания - История изменений

Vidokq в 09:16, 2 декабря 2013

2013-12-02T09:16:32Z

Vidokq в 09:15, 2 декабря 2013

2013-12-02T09:15:47Z

Vidokq в 09:06, 2 декабря 2013

2013-12-02T09:06:31Z

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

2012-12-04T21:14:40Z

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

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

2012-11-21T13:00:47Z

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

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

2012-11-21T13:00:00Z

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

Vidokq: /* Слайд: Прототипирование */

2012-11-21T12:54:54Z

‎Слайд: Прототипирование

Vidokq: /* Слайд: Эмуляция */

2012-11-21T12:28:02Z

‎Слайд: Эмуляция

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

2012-11-21T12:09:47Z

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

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

2012-11-21T11:55:08Z

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

@@ Строка 4: / Строка 4: @@
 ;author: Зайцев В.С.
 </slideshow>
-</slideshow>
 {| align=center width=800px
 ![[Файл:Функциональная_верификация.mm]]

@@ Строка 4: / Строка 4: @@
 ;author: Зайцев В.С.
 </slideshow>
 ==Слайд:Методы верификации проекта==

← Предыдущая		Версия 09:06, 2 декабря 2013
Строка 1:		Строка 1:
		+	{{ИГСАПР_TOC}}
	<slideshow style="custis" headingmark="Слайд:" incmark=":step" scaled="true" >		<slideshow style="custis" headingmark="Слайд:" incmark=":step" scaled="true" >
	;title: '''Верификация описания.'''		;title: '''Верификация описания.'''

@@ Строка 163: / Строка 163: @@
   '''Simulate->Start Simulation''' на закладке other поставить птичку '''enable code coverage'''
-{{Сн|<big>'''Команда для компиляции'''</big>}}
+{{Сн|<big>'''Команда для запуска'''</big>}}
   '''vsim -coverage'''

@@ Строка 106: / Строка 106: @@
 <slides split="-----" width="600" >
+{{V|24px}} В '''ModelSim''' для учета метрик покрытия при компиляции проекта нужно задать в меню '''Compile->Compiler option''' опции покрытия
 [[Файл:Опции компиляции покрытия.jpg|center]]

@@ Строка 212: / Строка 212: @@
-==Слайд: Прототипирование ==
+==Слайд: Быстродействие и расход памяти ==
-<slides split="-----" width="400" >
+Кроме полноты тестирования, одной из важных характеристик тестирующей программы являются:
-</slides>
+* {{Зел|<big>'''Требуемая память'''</big>}}

← Предыдущая		Версия 12:09, 21 ноября 2012
Строка 196:		Строка 196:

	==Слайд: Запуск моделирования в ModelSim с верификацией на основе утверждений ==		==Слайд: Запуск моделирования в ModelSim с верификацией на основе утверждений ==
		+
		+	{{Сн\|'''Для компиляции проекта содержащего файл верификации утверждений выполняем команду:'''}}
		+
		+	'''vcom''' -93 DIGITAL_BLOCK.vhd '''-pslfile''' DIGITAL_PSL.psl
		+
		+	После параметра '''-pslfile'''e указываем имя или путь к файлу
		+
		+	{{Сн\|'''Для запуска моделирования проекта содержащего файл верификации утверждений выполняем команду:'''}}
		+
		+	'''vsim''' '''''имя_проекта'''''
		+
		+	Для отключения выполнения проверок используем параметр '''-nopsl'''
		+
		+	'''vsim''' '''''имя проекта''''' '''-nopsl'''
		+
		+
		+	==Слайд: Эмуляция ==
		+
		+	<slides split="-----" width="400" >
		+
		+	</slides>

← Предыдущая		Версия 11:55, 21 ноября 2012
Строка 170:		Строка 170:

	'''coverage save -onexit'''		'''coverage save -onexit'''
		+
		+	==Слайд: Верификация на основе утверждений ==
		+	<big>'''Позволяет контролировать'''</big>:
		+
		+	* {{Сн\|'''Булева логика'''}} (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) являются простейшей формой свойств/утверждений, представляющие последовательность событий/состояний.\
		+
		+	{{ЖЛампа\|24px}} 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 с верификацией на основе утверждений ==