Міністерство освіти і науки України НУ „Львівська політехніка” ІКТА Кафедра ЕОМ Лабораторна робота №4 з курсу „Проектуванння периферійних комп’ютерних мікросистем” на тему: „Верифікація” Львів-2004 Мета роботи: Наскрізне тестування результатів попередніх етапів. Етап верифікації є не менш важливим за інші. Тому пакет Alliance передбачає набір потужних засобів перевірки. 1). Утиліта DRUC перевіряє готову топологію кристалу на відповідність правилам проектування (Design Rule Checker). Перевірка базується на швидких алгоритмах. 2). Утиліта LVX перевіряє відповідність двох структурних VHDL-описів одного і того ж пристрою.У пропонованій схемі проектування перший структурний опис отримується на етапі розробки на структурному рівні, а другий - генерується утилітою LYNX з відтрасованого шару елементів на підкладинці кристалу. Структурний опис, отриманий утилітою LYNX, має транзисторний рівень. Отже, необхідно перевірити на відповідність два структурних описи на рівні бібліотечних елементів кристалу та на рівні транзисторів. 3). Утиліта DESB є функціональним абстрактором, що створює функціональний VHDL-опис із структурного опису на транзисторному рівні. При такій трансляції відбувається перевірка ряду умов, а результуючий функціональний опис використовується при подальших перевірках утилітами ASIMUT та PROOF. При виявленні помилок на етапі верифікації відбувається повернення на попередні рівні проектування. 4) Завершальне тестування на цьому етапі проводить утиліта PROOF. Вона порівнює вхідний функціональний VHDL-опис кристалу з отриманим із структурного транзисторного рівня утилітою DESB. Якщо помилок не виявлено і повернення на попередні етапи проектування не потрібне, то можна перейти до завершення проектування. Виконання Верифікації 8-розрядного перемножувача На цьому етапі проводиться перевірка отриманого кристалу. Перевірка має три незалежних гілки. При виявленні помилки відбувається повернення на попередні рівні проектування. 1. Використовую пару утиліт 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 показано відповідно на рис.1 і рис.2. @@@@@@ @@ @@ @@ @@@@@ @@@ @@@ @@@ @@@@ @@@ @@ @@ @ @@@ @ @@ @ @@ @@ @ @@ @@ @@ @ @@ @@ @ @@ @@ @@@ @@ @@ @ @@ @@ @@@ @@ @ @@@ @@ @@ @ @@ @@ @ @@ @@ @@ @ @@ @@@@@@@@@@ @@ @ @@@@ @@@@ @@@ @@@@ @@ @ @@@ Netlist extractor Alliance CAD System 3.2b, lynx 1.16 Copyright (c) 1997-2002, ASIM/LIP6/UPMC E-mail support: alliance-support@asim.lip6.fr ---> Extracts symbolic figure core ---> Translate Mbk -> Rds ---> Build windows <--- 114 ---> Rectangles : 1001 ---> Figure size : ( -50, -100 ) ( 58850, 17100 ) ---> Cut transistors <--- 0 ---> Build equis <--- 37 ---> Delete windows ---> Build signals <--- 37 ---> Build instances <--- 41 ---> Build transistors <--- 0 ---> Save netlist <--- done ! Рис. 1. Повідомлення системи при виконанні програми LYNX Проводжу перевірку (LYNX + LVX) для готової топології кристалу (multiplier.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 multiplier multiplier [9] multiplier.ap --> multiplier.al # ###---------------------------------------------------------------### # compare extracted net-list and structural description # # to check that the ring router performed correctly # # ###---------------------------------------------------------------### lvx vst al multiplier [10] multiplier.vst ?? multiplier.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 multiplier multiplier extracted [11] вихідний файл з результатами тестування multiplier.pat multiplier.al @@@@@@ @@@@ @@@ @@@@ @@@@ @@ @@ @ @@ @ @@ @@ @ @@ @ @@ @@ @ @@ @ @@ @@ @ @@ @@ @@ @ @@ @@ @@ @ @@@ @@ @@@ @ @@ @@ @ @@@ @ @@ @@ @ @ @ @@ @@@@@@@@@@ @ @@@ @@@@ Gate Netlist Comparator Alliance CAD System 3.2b, lvx 2.23 Copyright (c) 1992-2002, ASIM/LIP6/UPMC E-mail support: alliance-support@asim.lip6.fr ***** Loading and flattening core (vst)... ***** Loading and flattening core (al)... ***** Compare Terminals .............. ***** O.K. (0 sec) ***** Compare Instances .......... ***** O.K. (0 sec) ***** Compare Connections ............ ***** O.K. (0 sec) ===== Terminals .......... 16 ===== Instances .......... 25 ===== Connectors ......... 150 ***** Netlists are Identical. ***** (0 sec) Рис.2. Повідомлення системи при виконанні програми LVX 2. Тут за допомогою утиліти 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 multiplier [12] multiplier.ap Повідомлення системи при виконанні програми DRUC показано на рис.3. @@@@@@@ @@@@@@@ @@@@ @ @@ @@ @@ @@ @@ @@ @@ @@ @@ @@ @@ @ @@ @@ @@ @@ @@@ @@@@ @@ @ @@ @@ @@ @@ @@ @@ @@ @@ @@ @@@@@ @@ @@ @@ @@ @@ @@ @@ @@ @@ @@ @@ @@ @@ @@ @@ @@ @@ @@ @@ @@ @@ @@ @@ @@ @ @@ @@ @@ @@ @@ @@@ @@ @@ @@@@@@@ @@@@@ @@@ @@@@ @@ @@@@ Design Rule Checker Alliance CAD System 3.2b, druc 3.00 Copyright (c) 1993-2002, ASIM/LIP6/UPMC E-mail support: alliance-support@asim.lip6.fr Flatten DRC on: addaccu Delete MBK figure : addaccu Load Flatten Rules : /usr/alliance/etc/cmos_7.rds Unify : addaccu Create Ring : addaccu_rng Merge Errorfiles: Merge Error Instances: instructionCourante : 50 End DRC on: addaccu Saving the Error file figure Done 0 File: addaccu.drc is empty: no errors detected. Рис. 3. Повідомлення системи при виконанні програми DRUC 3. Метою третьої гілки перевірки є відпрацювання утиліти PROOF, яка порівнює два функціональних VHDL-описи: вихідний та отриманий шляхом дизасемблювання утилітою DESB Отже, спочатку за допомогою LYNX отримуємо структурний опис транзисторного рівня з готової топології кристалу (multiplier.ap --> multiplier.al). Далі дизасемблюємо його утилітою DESB (YAGLE) до функціонального рівня (multiplier.al --> multiplier.vbe). Тестуємо отриманий функціональний опис утилітою ASIMUT, а далі порівнюємо вихідний та отриманий функціональні описи на логічну ідентичність утилітою PROOF (multiplier.vbe ?? multiplier.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 multiplier multiplier ;\ [13] desb multiplier -i -v multiplier.ap --> multiplier.al використовується файл multiplier.inf multiplier.al --> multiplier.vbe Файл multiplier.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 multiplier multiplier multiplier [14] вихідний файл з результатами тестування multiplier.ap multiplier.vbe симуляція на функціональному рівні (Behavioral) Сценарій моделювання має такий вигляд: delete_signals set_mode functional restart watch CLK CL DATA Y PREV SEL vector X X[7:0] vector AS_OUT AS_OUT[7:0] vector SH_IN SH_IN[7:0] vector RES RES[7:0] step 10ns clock CLK 0 1 ASSIGN Y 0 assign CL 1 AFTER 20ns DO ( assign X 00000101\b;ASSIGN Y 0) after 40 ns do (assign CL 0) after 60 ns do (assign CL 1) after 80 ns do (assign CL 0) after 100 ns do (assign CL 1) after 120 ns do (assign CL 0;assign Y 1) after 140 ns do (assign CL 1) after 160 ns do (assign CL 0;assign Y 0) after 180 ns do (assign CL 1) after 200 ns do (assign CL 0) after 220 ns do (assign CL 1) after 240 ns do (assign CL 0) after 260 ns do (assign CL 1) after 280 ns do (assign CL 0) sim 300 ns Результат верифікації згідно сценарію симуляції:
Порівняння двох функціональних VHDL-описів: # ###---------------------------------------------------------### # check the correctness of the extracted data_flow # # description running the formal proover # # ###---------------------------------------------------------### proof -d multiplier multiplier [15] multiplier.vbe multiplier.vbe Показувати логічні функції в порядку їх обробки. Повідомлення системи при виконанні програми PROOF показано на рис.4 . @@@@@@@ @@@ @@ @@ @ @@ @@ @@ @@ @@ @@ @@ @@@ @@@ @@@ @@@ @@ @@ @@ @@@ @@ @@ @@ @@ @@ @@@@@@@@ @@@@@ @@ @@ @@ @@ @@ @@ @@ @@ @@ @@ @@ @@ @@ @@ @@ @@ @@ @@ @@ @@ @@ @@ @@ @@ @@ @@ @@ @@ @@ @@ @@ @@ @@ @@ @@ @@@@@@ @@@@ @@@ @@@ @@@@@@ Formal Proof Alliance CAD System 3.2b, proof 4.20 [1997/10/09] Copyright (c) 1990-2002, ASIM/LIP6/UPMC E-mail support: alliance-support@asim.lip6.fr ================================ Environment ================================ MBK_WORK_LIB = . MBK_CATA_LIB = . ======================= Files, Options and Parameters ======================= First VHDL file = addaccue.vbe Second VHDL file = addaccu.vbe The auxiliary signals are erased Errors are displayed =============================================================================== Compiling 'addaccue' ... Compiling 'addaccu' ... Running abl ordonnancer on `addaccue` ........ Running Abl2Bdd on `addaccue` ---> final number of nodes = 663(404) Running Abl2Bdd on `addaccu` ------------------------------------------------------------------------------- Formal proof with Ordered Binary Decision Diagrams between './addaccue' and './addaccu' ------------------------------------------------------------------------------- ============================== PRIMARY OUTPUT =============================== ============================= AUXILIARY SIGNAL ============================== ============================== REGISTER SIGNAL ============================== =============================== EXTERNAL BUS ================================= ================================ INTERNAL BUS ================================= Formal Proof : OK Ppppppppppppppppppprrrrrrrrrrrrooooooooooooooooooooooooooooooooofffffffffffffff ------------------------------------------------------------------------------- Рис. 4 Повідомлення системи при виконанні програми PROOF Висновок.