Міністерство освіти і науки України Національний університет „Львівська політехніка” Кафедра ЕОМ Звіт з лабораторної роботи №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 Показувати логічні функції в порядку їх обробки. Висновок: на даній лабораторній роботі я робив наскрізне тестування результатів попередніх етапів.