Частина тексту файла (без зображень, графіків і формул):
Міністерство освіти і науки України
Національний університет „Львівська політехніка”
Кафедра ЕОМ
Звіт
з лабораторної роботи №5
на тему:
„Верифікація”
Підготував: ст. гр. СКС-5
Львів 2006
Тема: Верифікація.
Мета: Наскрізне тестування результатів попередніх етапів.
Хід роботи:
ПЕРША ГІЛКА ПЕРЕВІРКИ:
Використовуємо пару утиліт LYNX та LVX. LYNX отримує структурний опис з топології кристалу на транзисторному рівні, використовуючи технологічний файл (.ap --> .al). LVX порівнює отриманий структурний опис транзисторного рівня з початковим структурним описом (.al ?? .vst).
Проводимо перевірку (LYNX + LVX) для відтрасованого шару елементів на підкладинці кристалу (core.ap):
# ###---------------------------------------------------------###
# extract net-list from symbolic layout for the core #
# ###---------------------------------------------------------###
MBK_IN_PH=ap ;\
MBK_OUT_LO=al ;\
RDS_TECHNO_NAME=$TOP/etc/cmos_5.rds ;\
MBK_CATA_LIB=$TOP/cells/scr:$TOP/cells/ring ;\
export MBK_IN_PH MBK_OUT_LO RDS_TECHNO_NAME MBK_CATA_LIB ;\
lynx -v core core [7]
core.ap --> core.al
# ###-----------------------------------------------------------------------###
# compare extracted net-list and structural description #
# to check that the standard cell router performed correctly #
# ###-----------------------------------------------------------------------###
MBK_CATA_LIB=$TOP/cells/scr:$TOP/cells/ring ;\
export MBK_CATA_LIB ;\
lvx vst al core core -f [8]
робити порівняння у термах
core.vst ?? core.al
Проводимо перевірку (LYNX + LVX) для готової топології кристалу (addaccu.ap).
# ###------------------------------------------------------------###
# extract net-list from symbolic layout for the circuit #
# ###------------------------------------------------------------###
MBK_IN_PH=ap ;\
MBK_OUT_LO=al ;\
RDS_TECHNO_NAME=$TOP/etc/cmos_5.rds ;\
MBK_CATA_LIB=$TOP/cells/scr:$TOP/cells/ring ;\
export MBK_IN_PH MBK_OUT_LO RDS_TECHNO_NAME MBK_CATA_LIB ;\
lynx -v addaccu addaccu [9]
addaccu.ap --> addaccu.al
# ###---------------------------------------------------------------###
# compare extracted net-list and structural description #
# to check that the ring router performed correctly #
# ###---------------------------------------------------------------###
lvx vst al addaccu [10]
addaccu.vst ?? addaccu.al
Проводимо симуляцію на структурному транзисторному рівні з використанням тестових наборів:
# ###---------------------------------------------------------###
# simulate the extracted net-list #
# ###---------------------------------------------------------###
MBK_IN_LO=al ;\
MBK_CATA_LIB=$TOP/cells/scr:$TOP/cells/ring ;\
export MBK_IN_LO MBK_CATA_LIB ;\
asimut addaccu addaccu extracted [11]
вихідний файл з результатами тестування
addaccu.pat
addaccu.al
ДРУГА ГІЛКА ПЕРЕВІРКИ:
Тут за допомогою утиліти DRUC перевіряється топологія кристалу на рівні транзисторів у відповідності технологічних правил проектування. Враховуються також паразитні ємності. Така перевірка може вимагати багато машинного часу:
# ###---------------------------------------------------------###
# check design rules #
# ###---------------------------------------------------------###
MBK_IN_PH=ap ;\
RDS_OUT=cif ;\
RDS_TECHNO_NAME=$TOP/etc/cmos_5.rds ;\
MBK_CATA_LIB=$TOP/cells/scr:$TOP/cells/ring ;\
export MBK_IN_PH RDS_OUT RDS_TECHNO_NAME MBK_CATA_LIB ;\
druc addaccu [12]
addaccu.ap
ТРЕТЯ ГІЛКА ПЕРЕВІРКИ:
Метою третьої гілки перевірки є відпрацювання утиліти PROOF, яка порівнює два функціональних VHDL-описи: вихідний та отриманий шляхом дизасемблювання утилітою DESB.
Отже, спочатку за допомогою LYNX отримуємо структурний опис транзисторного рівня з готової топології кристалу (addaccu.ap --> addaccue.al). Далі дизасемблюємо його утилітою DESB (YAGLE) до функціонального рівня (addaccue.al --> addaccue.vbe). Тестуємо отриманий функціональний опис утилітою ASIMUT, а далі порівнюємо вихідний та отриманий функціональні описи на логічну ідентичність утилітою PROOF (addaccu.vbe ?? addaccue.vbe):
# ###------------------------------------------------------------------------###
# generate a Data-Flow description from the transistor level #
# extracted net-list #
# ###-----------------------------------------------------------------------###
MBK_IN_PH=ap ;\
MBK_IN_LO=al ;\
MBK_OUT_LO=al ;\
RDS_TECHNO_NAME=$TOP/etc/cmos_5.rds ;\
MBK_CATA_LIB=$TOP/cells/scr:$TOP/cells/ring ;\
export MBK_IN_PH MBK_IN_LO MBK_OUT_LO RDS_TECHNO_NAME MBK_CATA_LIB ;\
lynx -v -t addaccu addaccue ;\ [13]
desb addaccue -i -v
addaccu.ap --> addaccue.al
використовується файл addaccue.inf
addaccue.al --> addaccue.vbe
Файл addaccue.inf може використовуватись для переіменовування термів, щоби забезпечити строгу відповідність між початковим функціональним VHDL-описом та отриманим утилітою DESB (YAGLE).
rename
core.l0.dff_s : reg(0) ;
core.l1.dff_s : reg(1) ;
core.l2.dff_s : reg(2) ;
core.l3.dff_s : reg(3) ;
end
DESB (YAGLE) переіменовує терми core.l* в структурному VHDL-описі транзисторного рівня в терми reg(*) - як вони описані у початковому функціональному VHDL-описі.
Проводимо симуляцію отриманого функціонального VHDL-описа. Використовуємо тестові набори, на яких перевіряємо роботу схеми:
# ###---------------------------------------------------------###
# simulate the extracted data_flow description #
# ###---------------------------------------------------------###
asimut -b addaccue addaccu abstracted [14]
вихідний файл з результатами тестування
addaccu.ap
addaccue.vbe
симуляція на функціональному рівні (Behavioral)
Порівняння двох функціональних VHDL-описів:
# ###---------------------------------------------------------###
# check the correctness of the extracted data_flow #
# description running the formal proover #
# ###---------------------------------------------------------###
proof -d addaccue addaccu [15]
addaccu.vbe
addaccue.vbe
Показувати логічні функції в порядку їх обробки.
Висновок: на даній лабораторній роботі я робив наскрізне тестування результатів попередніх етапів.