ВСТРОЕННЫЕ ИНФОРМАЦИОННО- УПРАВЛЯЮЩИЕ СИСТЕМЫ РЕАЛЬНОГО ВРЕМЕНИ Лекция 2: Архитектура процессоров для ВИУСРВ ВМиК МГУ им. М.В. Ломоносова, Кафедра АСВК, - презентация

1 ВСТРОЕННЫЕ ИНФОРМАЦИОННО- УПРАВЛЯЮЩИЕ СИСТЕМЫ РЕАЛЬНОГО ВРЕМЕНИ Лекция 2: Архитектура процессоров для ВИУСРВ ВМиК МГУ им. М.В. Ломоносова, Кафедра АСВК, Лаборатория Вычислительных Комплексов, Ассистент Волканов Д.Ю.

2 2 План Интегрированная модульная авионика Процессор ARM Процессор обработки сигналов (NM 6403) Задача WCET

3 3 ЦВМ 3 4-е поколение боевых комплексов Федеративная структура КБО БЦВМ Система индикации РЭК ЦВМ УЦВМУЦВМ Система навигации СУО УЦВМУЦВМ ОЭК ЦВМ МКИО, ARINC 429, Низкоскоростные каналы информационного обмена (МКИО, ARINC 429) Большое количество разнотипных специализированных вычислителей Невозможность комплексной обработки информации Применение однопроцессорных вычислительных систем Комплекс средств связи УЦВМУЦВМ ЦВМ ОДОД ОСОС УЦВМУЦВМ

4 4 4 5-е поколение боевых комплексов Интегрированная структура КБО МКИО, ARINC 429, Fibre Channel ИУС БЦВМ ИУП Коммутато р БЦВМ ЦВМ РЭК Система навигации СУО ОЭК ЦВМ Комплекс средств связи УЦВМУЦВМ ЦВМ ОДОД ОСОС УЦВМУЦВМ коммутатор Использование высокоскоростных каналов информационного обмена наряду с МКИО Сокращение количества отдельных вычислителей Комплексная обработка информации Перенос третичной и вторичной (частично) обработки информации в «ядро» Применение многопроцессорных вычислительных систем

5 поколение боевых комплексов Интегрированная модульная авионика боевых комплексов ИУС БЦВМ ИУП БЦВМ Вычисл.модули РЭК СН СУО ОЭК КСС Fibre Channel Использование высокоскоростных каналов информационного обмена в качестве базового инструмента межмодульной и межблочной связи. Использование однородной вычислительной среды и унифицированных модулей в различных системах КБО Комплексная обработка информации и гибкая реконфигурация при отказах Использование многоядерных процессоров Вычисл. модули Единый вычислительный кластер

6 6 Требования к процессорам во встроенных системах Предсказуемость Энергопотребление Тепловыделение Надёжность

7 7 ARM Powered Products

8 8 ARM Парадигма программирования Набор инструкций Архитектура системы

9 9 Размер типов данных и набор инструкций ARM имеет 32-битную архитектуру. Обычно в ARM используется следующие ключевые слова: –Byte - 8 bits –Halfword - 16 bits (два байта) –Word - 32 bits (четыре байта) Большинство ARM процессоров реализует два набора инструкций –32-bit ARM Instruction Set –16-bit Thumb Instruction Set

10 10 Режимы работы процессора Семь основных режимов функционирования ARM: –User : непривилегированный режим, под которым выполняется большинство задач –FIQ : включается, когда приходит high priority (fast) прерывание –IRQ : включается, когда приходит low priority (normal) прерывание –Supervisor : включается при перегрузке и когда выполняется Software Interrupt instruction –Abort : позволяется ловить нарушения режима доступа к памяти –Undef : позволяет ловить нераспознанные инструкции –System : привилегированный режим использующий те же регистры, что и User режим

11 11 r0 r1 r2 r3 r4 r5 r6 r7 r8 r9 r10 r11 r12 r13 (sp) r14 (lr) r15 (pc) cpsr r13 (sp) r14 (lr) spsr r13 (sp) r14 (lr) spsr r13 (sp) r14 (lr) spsr r13 (sp) r14 (lr) spsr r8 r9 r10 r11 r12 r13 (sp) r14 (lr) spsr FIQIRQSVCUndefAbort User Mode r0 r1 r2 r3 r4 r5 r6 r7 r8 r9 r10 r11 r12 r13 (sp) r14 (lr) r15 (pc) cpsr r13 (sp) r14 (lr) spsr r13 (sp) r14 (lr) spsr r13 (sp) r14 (lr) spsr r13 (sp) r14 (lr) spsr r8 r9 r10 r11 r12 r13 (sp) r14 (lr) spsr Current Visible Registers Banked out Registers FIQIRQSVCUndefAbort r0 r1 r2 r3 r4 r5 r6 r7 r15 (pc) cpsr r13 (sp) r14 (lr) spsr r13 (sp) r14 (lr) spsr r13 (sp) r14 (lr) spsr r13 (sp) r14 (lr) spsr r8 r9 r10 r11 r12 r13 (sp) r14 (lr) spsr Current Visible Registers Banked out Registers UserIRQSVCUndefAbort r8 r9 r10 r11 r12 r13 (sp) r14 (lr) FIQ ModeIRQ Mode r0 r1 r2 r3 r4 r5 r6 r7 r8 r9 r10 r11 r12 r15 (pc) cpsr r13 (sp) r14 (lr) spsr r13 (sp) r14 (lr) spsr r13 (sp) r14 (lr) spsr r13 (sp) r14 (lr) spsr r8 r9 r10 r11 r12 r13 (sp) r14 (lr) spsr Current Visible Registers Banked out Registers UserFIQSVCUndefAbort r13 (sp) r14 (lr) Undef Mode r0 r1 r2 r3 r4 r5 r6 r7 r8 r9 r10 r11 r12 r15 (pc) cpsr r13 (sp) r14 (lr) spsr r13 (sp) r14 (lr) spsr r13 (sp) r14 (lr) spsr r13 (sp) r14 (lr) spsr r8 r9 r10 r11 r12 r13 (sp) r14 (lr) spsr Current Visible Registers Banked out Registers UserFIQIRQSVCAbort r13 (sp) r14 (lr) SVC Mode r0 r1 r2 r3 r4 r5 r6 r7 r8 r9 r10 r11 r12 r15 (pc) cpsr r13 (sp) r14 (lr) spsr r13 (sp) r14 (lr) spsr r13 (sp) r14 (lr) spsr r13 (sp) r14 (lr) spsr r8 r9 r10 r11 r12 r13 (sp) r14 (lr) spsr Current Visible Registers Banked out Registers UserFIQIRQUndefAbort r13 (sp) r14 (lr) Abort Mode r0 r1 r2 r3 r4 r5 r6 r7 r8 r9 r10 r11 r12 r15 (pc) cpsr r13 (sp) r14 (lr) spsr r13 (sp) r14 (lr) spsr r13 (sp) r14 (lr) spsr r13 (sp) r14 (lr) spsr r8 r9 r10 r11 r12 r13 (sp) r14 (lr) spsr Current Visible Registers Banked out Registers UserFIQIRQSVCUndef r13 (sp) r14 (lr) Набор регистров в ARM

12 12 Организация регистров User mode r0-r7, r15, and cpsr r8 r9 r10 r11 r12 r13 (sp) r14 (lr) spsr FIQ r8 r9 r10 r11 r12 r13 (sp) r14 (lr) r15 (pc) cpsr r0 r1 r2 r3 r4 r5 r6 r7 User r13 (sp) r14 (lr) spsr IRQ User mode r0-r12, r15, and cpsr r13 (sp) r14 (lr) spsr Undef User mode r0-r12, r15, and cpsr r13 (sp) r14 (lr) spsr SVC User mode r0-r12, r15, and cpsr r13 (sp) r14 (lr) spsr Abort User mode r0-r12, r15, and cpsr Thumb состояние Low registers Thumb состояние High registers Note: System mode использует те же регистры, что и User mode

13 13 Типы регистров В ARM есть 37 регистров размером 32-bits. –1 специальный регистр: program counter –1 специальный регистр: current program status –5 специальных регистров для хранения program status –30 регистров общего назначения В любом режиме работы процессора имеется доступ к следующим регистрам: –r0-r12 РОН –r13 (the stack pointer, sp) иr14 (the link register, lr) –program counter, r15 (pc) –current program status register, cpsr Привилегированный (except System) режим может обращаться к spsr (saved program status register)

14 14 Регистры состояния программы Флаги условных переходов –N = Negative вычисляется АЛУ –Z = Zero вычисляется АЛУ –C = АЛУ операция Carried out –V = АЛУ операция oVerflowed Sticky Overflow флаг - Q flag –Только для 5TE/J архитектур –Определяет насыщение J bit –Только для 5TEJ архитектур –J = 1: процессор в состоянии Jazelle Биты отключения прерываний. –I = 1: отключает IRQ. –F = 1: отключает FIQ. T Bit –Только для xT аржитетур –T = 0: процессор в состоянии ARM –T = 1: процессор в состоянии Thumb Mode bits –Указывают режим работы процессора 2731 N Z C V Q 2867 I F T mode fsxc U n d e f i n e dJ

15 15 Если процессор находится в режиме ARM: –Все инструкции размером 32 бита –Все инструкции должны быть выровнены по слову (word aligned) Если процессор находится в режиме Thumb: –Все инструкции размером 16 бит –Все инструкции должны быть выровнены по полуслову (halfword aligned) Если процессор находится в режиме Jazelle: –Все инструкции размером 8 бит –Процессор позволяется читать по 4 инструкции сразу Program Counter (r15)

16 16 Vector Table Обработка исключений Алгоритм обработки исключений: –Копируется CPSR в SPSR_ –Заполняются CPSR биты Состояние изменяется на ARM Включается exception mode Игнорируются прерывания (if appropriate) –Stores the return address in LR_ –Sets PC to vector address Для возврата к нормальной работе: –Восстанавливается CPSR из SPSR_ –Восстанавливается PC из LR_ Все это может проделываться только в состоянии ARM. Vector table может находится по адресу 0xFFFF0000 на ARM720T и ARM9/10 семействе устройств FIQ IRQ (Reserved) Data Abort Prefetch Abort Software Interrupt Undefined Instruction Reset 0x1C 0x18 0x14 0x10 0x0C 0x08 0x04 0x00

17 17 Разработка ARM архитектуры SA-110 ARM7TDMI 4T 1 Поддержка Halfword иsigned halfword / байтов System mode Thumb instruction set 2 4 ARM9TDMI SA-1110 ARM720TARM940T Improved ARM/Thumb Interworking CLZ 5TE Saturated maths DSP multiply- accumulate instructions XScale ARM1020E ARM9E-S ARM966E-S 3 Ранние ARM архитектуры ARM9EJ-S 5TEJ ARM7EJ-S ARM926EJ-S Jazelle выполнение Java bytecode 6 ARM1136EJ-S ARM1026EJ-S SIMD Instructions Multi-processing V6 Memory architecture (VMSA) Unaligned data support

18 18 Процессор ARM Парадигма программирования Набор инструкций Архитектура системы

19 19 ARM инструкции могут выполнятся условно путем проставления постфикса с кодом условия. –CMP r3,#0 CMP r3,#0 BEQ skip ADDNE r0,r1,r2 ADD r0,r1,r2 skip По умолчанию, инструкции обработки данных не влияют на условные флаги, но данные флаги могут быть опционально установлены используя S. CMP не нуждается вS. loop … SUBS r1,r1,#1 BNE loop если Z флаг нулевой, то осуществляем переход декрементируем r1 и устанавливаем флаги Условные переходы и флаги

20 20 Возможные условные коды приведены ниже: Условные коды Not equal Unsigned higher or same Unsigned lower Minus Equal Overflow No overflow Unsigned higher Unsigned lower or same Positive or Zero Less than Greater than Less than or equal Always Greater or equal EQ NE CS/HS CC/LO PL VS HI LS GE LT GT LE AL MI VC Суффикс Описание Z=0 C=1 C=0 Z=1 Флаг N=1 N=0 V=1 V=0 C=1 & Z=0 C=0 or Z=1 N=V N!=V Z=0 & N=V Z=1 or N=!V

21 21 Примеры условного выполнения Использование последовательности условных инструкций if (a==0) func(1); CMP r0,#0 MOVEQ r0,#1 BLEQ func Установка флагов, после использование различных условных кодов if (a==0) x=0; if (a>0) x=1; CMP r0,#0 MOVEQ r1,#0 MOVGT r1,#1 Использование условных инструкций сравнения if (a==4 || a==10) x=0; CMP r0,#4 CMPNE r0,#10 MOVEQ r1,#0

22 22 Branch : B{ } label Branch со связью: BL{ } subroutine_label Cond L Offset Condition field Link bit 0 = Branch 1 = Branch with link Инструкции ветвления

23 23 Инструкции обработки данных Состоят из: –Арифметических: ADDADCSUBSBCRSBRSC –Логических: ANDORREORBIC –Сравнений: CMPCMNTSTTEQ –Перемещения данных: MOVMVN Данные инструкции работают только с регистрами, НЕ с памятью. Синтаксис: { }{S} Rd, Rn, Operand2 Сравнения только устанавливают флаги Перемещение данных не специфицирует Rn Второй операнд отправляется на АЛУ через barrel shifter.

24 24 Barrel Shifter Destination CF 0 Destination CF LSL : Logical Left Shift ASR: Arithmetic Right Shift Умножение на 2Деление на 2, сохраняя бит флага Destination CF...0 Destination CF LSR : Logical Shift RightROR: Rotate Right Деление на 2Циклическое смещение бита от LSB к MSB Destination RRX: Rotate Right Extended Циклическое смещение через CF к MSB CF

25 25 Результат Операнд 1 Barrel Shifter Операнд 2 АЛУ Использование Barrel Shifter: Второй операнд

26 26 Умножение Синтаксис: –MUL{ }{S} Rd, Rm, RsRd = Rm * Rs –MLA{ }{S} Rd,Rm,Rs,RnRd = (Rm * Rs) + Rn –[U|S]MULL{ }{S} RdLo, RdHi, Rm, RsRdHi,RdLo := Rm*Rs –[U|S]MLAL{ }{S} RdLo, RdHi, Rm, Rs RdHi,RdLo := (Rm*Rs)+RdHi,RdLo Время в циклах –Основная MUL инструкция 2-5 циклов на ARM7TDMI 1-3 циклов на StrongARM/XScale 2 цикла на ARM9E/ARM102xE –+1 цикл для ARM9TDMI (over ARM7TDMI) –+1 цикл для long

27 27 Помещение данных в регистр LDRSTR Word LDRBSTRB Byte LDRHSTRH Halfword LDRSB Signed byte load LDRSH Signed halfword load Память должна поддерживать все допустимые размеры Синтаксис: – LDR { }{ } Rd, –STR { }{ } Rd, e.g. LDREQB

28 28 Доступ по адресу Адрес доступные по LDR/STR определяется как значение регистра плюс смещение Для слова и беззнакового байта доступа, смещение может быть – bytes LDR r0,[r1,#8] Для полуслова и знакового полуслова, смещение может быть : –0-255 bytes. –регистр

29 29 0x5 r1 0x200 Base Register 0x20 0 r0 0x5 Source Register for STR Offset 12 0x20 c r1 0x200 Original Base Register 0x20 0 r0 0x5 Source Register for STR Offset 12 0x20 c r1 0x20c Updated Base Register Автообновление из: STR r0,[r1,#12]! Префиксный или постфиксный адрес? Префиксный: STR r0,[r1,#12] Постфискный: STR r0,[r1],#12

30 30 LDM / STM Синтаксис: { } Rb{!}, 4 режима адресования: LDMIA / STMIA инкрементить после LDMIB / STMIB инкрементить до LDMDA / STMDA декриментить после LDMDB / STMDB декриментить до IA r1 Увеличение адресов r4 r0 r1 r4 r0 r1 r4 r0r1 r4 r0 r10 IBDADB LDMxx r10, {r0,r1,r4} STMxx r10, {r0,r1,r4} Base Register (Rb)

31 31 Программное прерывание (SWI) Возбуждает обработчик прерываний в соответствии с SWI hardware vector SWI handler может определить SWI number чтобы решить какую операцию надо выполнить Используя SWI механизм, ОС может реализовать набор привилегированных операций Синтаксис: – SWI{ } Cond SWI number (ignored by processor) 23 Условное поле

32 32 PSR инструкции MRS и MSR позволяет переместить содержимое CPSR / SPSR в или из регистра общего назначения Синтаксис: – MRS{ } Rd, ; Rd = – MSR{ },Rm ; = Rm где – = CPSR or SPSR –[_fields] = any combination of fsxc Так же возможно – MSR{ },#Immediate 2731 N Z C V Q 2867 I F T mode fsxc U n d e f i n e dJ

33 33 ARM ветви B –PC relative. ±32 Mbyte range. BL –Хранит и возвращает адрес в LR STMFD sp!,{regs,lr} : BL func2 : LDMFD sp!,{regs,pc } func1func2 : BL func1 : MOV pc, lr

34 34 Пример While (i!=j) (i > j) ? i-=j : j-=i; loop CMP Ri, Rj; SUBGT Ri, Ri, Rj ; i = i - j SUBLT Rj, Rj, Ri ; j = j – I BNE loop ; if NE (not equal),then loop

35 35 Процессор ARM Парадигма программирования Набор инструкций Архитектура системы

36 36 Пример ARM-based системы 16 bit RAM 8 bit ROM 32 bit RAM ARM Core I/O Peripherals Interrupt Controller nFIQnIRQ

37 37 AMBA Bridge Timer On-chip RAM ARM Interrupt Controller Remap/ Pause TIC Arbiter Bus Interface External ROM External RAM Reset System BusPeripheral Bus AMBA –Advanced Microcontroller Bus Architecture ADK –Complete AMBA Design Kit ACT –AMBA Compliance Testbench PrimeCell –ARMs AMBA compliant peripherals AHB or ASBAPB External Bus Interface Decoder

38 38 Процессоры DSP Особенности DSP процессоров Процессор NM6403

39 39 Особенности DSP процессоров Аппаратная поддержка программных циклов, кольцевых буферов Один или несколько операндов извлекаются из памяти в цикле исполнения команды Нет команд R,R->R Реализация однотактного умножения и команд, использующих в качестве операндов содержимое ячеек памяти

40 40 Особенности DSP процессоров (2) Сложение и умножение требуют: –произвести выборку двух операндов –выполнить сложение или умножение (обычно и то и другое) –сохранить результат или удерживать его до повторения Множественный доступ к памяти за один и тот же командный цикл.

41 Антоненко В.А. Волканов Д.Ю Процессор NM Mhz RISC ядро 32-битные данные 32-битные операции регистров Векторное устройство Переменная разрядность До 2048 параллельных умноженей

42 42 RISC-ядро 5-ти ступенчатый 32-разрядный конвейер; 32- и 64-разрядные команды (обычно выполняется две операции в одной команде); Два адресных генератора, адресное пространство - 16 GB; Два 64-разрядных программируемых интерфейса с SRAM/DRAM-разделяемой памятью; Формат данных - 32-разрядные целые; Регистры: 8 32-разрядных регистров общего назначения; 8 32-разрядных адресных регистров; Специальные регистры управления и состояния; Два высокоскоростных коммуникационных порта ввода/вывода, Аппаратно совместимых с портами TMS320C4x.

43 43 VECTOR-сопроцессор Переменная 1-64-разрядная длина векторных операндов и результатов; Формат данных - целые числа, упакованные в 64-разрядные блоки, в форме слов переменной длины от 1 до 64 разрядов каждое; Поддержка векторно-матричных и матрично-матричных операций; Два типа функций насыщения на кристалле; Три внутренних 32x64-разрядных RAM- блока

44 44 Производительность Скалярные операции: –50 MIPS; –200 MOPS для 32-разрядных данных; Векторные операции: –от 50 до MMAC (миллионов умножений с накоплением в секунду); I/O и интерфейсы с памятью: –пропускная способность двух 64-разрядных интерфейсов с памятью - до 800 Мбайт/сек; I/O коммуникационные порты - до 20 Мбайт/сек кажд

45 45 Особенности NM64003 (1) Возможность работы с входными сигналами (синапсами) и весами переменной разрядности (от 1 до 64 бит), задаваемой программно, что обеспечивает уникальную способность нейропроцессора увеличивать производительность с уменьшением разрядности операндов; Быстрая подкачка новых весов на фоне вычислений; (24 операции умножения с накоплением за один такт при длине операндов 8 бит); V аппаратная поддержка эмуляции нейросетей большой размерности; Реализация функции активации в виде пороговой функции или функции ограничения;

46 46 Особенности NM64003 (2) Наличие двух широких шин (по 64 разряда) для работы с внешней памятью любого типа: до 4Мб SRAM и до 16 Гб DRAM; Наличие двух байтовых коммуникационных портов ввода/вывода, аппаратно совместимых с коммуникационными портами TMS320C4x для реализации параллельных распределенных вычислительных систем большой производительности. Возможность работать с данными переменной разрядности по различным алгоритмам, реализуемым с помощью хранящихся во внешнем ОЗУ программ

47 Антоненко В.А. Волканов Д.Ю Системы на NM 6403 MC431 – однопроцессорная плата NM4 – четырехпроцессорная плата 6MCBO – 4 платы по 6 процессоров и платы для обработки входных сигналов

48 48 Схема нейровычислителя

49 49 WCET Постановка задачи Статический метод Измерительный метод Гибридный метод Метод Bound Checking

50 50 WCET – задача оценки наихудшего времени выполнения программ Актуальна при проектировании и анализе программ для РВ систем В РВ системах должно быть гарантировано время реакции системы на внешние события Введение

51 51 WCET

52 52 Анализ программы без выполнения на реальном оборудовании Общая схема: –Построение CFG –Анализ линейных участков –Вычисление оценки WCET по CFG Статический метод

53 53 Пример организации: Статический метод

54 54 CFG – граф: – вершины - линейные участки программы – ребра – возможные переходы CFG

55 55 …// 1 if (a>5) { sleep(5);// 2 if (a>7) { sleep(7);// 3 } else { sleep(7);// 4 } sleep(5);// 5 CFG

56 56 Цель: –Вычисление количества итераций циклов –Выявление границ рекурсий –Определение недостижимых блоков Анализ потоков управления

57 57 if (a>10) { if (a

58 58 Вычисление времени выполнения линейных участков При этом учитывается влияние архитектурных компонент: –Кэши –Конвееры –Предсказатель переходов Анализ поведения процессора

59 59 for ( i=0 ; i

60 60 Производится проход по графу и вычисление оценки WCET Существует три подхода к вычислению оценки: –structure-based –path-based –implicit path enumeration techniques (IPET) Вычисление оценки WCET

61 61 Перебираются листья синтаксического дерева Выделяются группы листьев и объединяются по определенным правилам После полного прохода получается одна вершина WCET = время выполнения этой вершины Structure-based

62 62 Structure-based

63 63 Перебираются все возможные пути программы Для каждого пути вычисляется время выполнения Выбирается путь с максимальным временем выполнения WCET = время этого пути Path-based

64 64 Path-based

65 65 Всем ребрам и вершинам сопоставляется коэффициент - число проходов по ребру или вершине Cоставляется система уравнений следующего вида: –Коэффициент вершины = сумма коэффициентов входящих ребер –Коэффициент вершины = сумма коэффициентов исходящих ребер Составляется функция, равная сумме произведений коэффициентов на время выполнения каждого линейного участка WCET – максимальное значение этой функции IPET

66 66 IPET

67 67 Программа выполняется на реальном оборудовании Производится серия запусков программы на различных наборах подготовленных входных данных Определяется оценка наихудшего времени выполнения Измерительный метод

68 68 Преимущества: –Не требуется описание модели вычислителя Недостатки: –Необходимость запуска программы на целевом оборудовании –Подготовка входных данных, покрывающих все возможные пути выполнения –Оценка WCET не точна Измерительный метод

69 69 Соединяет в себе измерительный и статический методы Общая схема анализа: –Построение CFG –Вычисление времени выполнения каждого линейного участка измерительным методом –Вычисление оценки wcet по графу статическим методом Гибридный метод

70 70 Преимущества: –Сокращается количество выполнений на реальном оборудовании –Не требуется подготовка входных данных Недостатки: –Необходимость запуска на целевом вычислителе –Оценка WCET завышена Гибридный метод

71 71 Bounded model checking Технология верификации программ на модели с ограничением на длину вычислений Основана на представлении программ в виде КНФ Проверка свойств производится путем проверки выполнимости построенной КНФ

72 72 Bounded model checking Типичная схема анализа: Программа Преобразователь КНФ Решатель Результат

73 73 Bounded model checking Построение КНФ: … if ( a < 5 ) a = b + 1; else a = 5; return a; КНФ: (a_1 = b_0 + 1) && (a_2 = 5) && [ (a_0 < 5 && a_3 = a_1) || (a_0 >= 5 && a_3=a_2)] && (out = a_3)

74 74 Bounded model checking Циклы: Ограничение количества итераций мажорантой Разворачивание циклов

75 75 Bounded model checking for ( int i = 0; i < 3; ++ i ) { if ( a < 5 ) a += i; } i = 0; if ( i < 3 ) { if ( a < 5 ) a += i; ++i; if ( i < 3 ) { if ( a < 5 ) a += i; ++i; …

76 76 Bounded model checking Проверка свойств: void f(int a, int b) { if ( a < 5 ) a = b + 1; else a = 5; assert( a

77 77 Bounded model checking Проверка выполнимости КНФ – решение задачи ВЫП Решатели: Z3 (Microsoft) Yices (SRI) Boolector

78 78 Bounded model checking Ограничение на длину вычислений: Построение КНФ длины не более k Проверка свойств полученной КНФ Если свойство выполняется, то увеличение k Позволяет быстро проверять свойства!

79 79 Использование BMC для оценки WCET Известно время выполнения каждого линейного участка Добавление вычисления времени выполнения в КНФ assert (time

80 80 Использование BMC для оценки WCET Исходная программа void f(int a) { a = a + 5; // time = [1, 2] if (a < 0) { /* path1 */ // time = [10, 15] } /* path2 */ // time = [5, 16] } при a принадлежащем [-4; 0]

81 81 Использование BMC для оценки WCET void f(int a) { a = a + 5; // time = [1, 2] if (a < 0) { /* path1 */ // time = [10, 15] } /* path2 */ // time = [5, 16] assert(time

82 82 Использование BMC для оценки WCET Система выполнима Строим модель, time_3 = 16 wcet = 16 Строим КНФ заново: Исходная КНФ && !(time_3

83 83 Использование BMC для оценки WCET После нескольких итераций получаем wcet = 33 КНФ && !(time_3

84 84 Литература Материалы сайта 32-разрядные высокопроизводительные RISС-процессоры семейства ARM ( Нейропроцессор NM6403. Материалы компании ЗАО НТЦ «Модуль». Адрес в Интернет: Черников В. М., Виксне П. Е., Фомин Д. В., Шевченко П. А. "Архитектурные особенности нейропроцессора NM6403". Всероссийская научно-техническая конференция "Нейроинформатика-99". Сборник научных трудов. Часть 2, Москва, 1999, С ( sessions/1999/Neuro_2/093.pdf) Wilhelm R. et al. The worst-case execution-time problemoverview of methods and survey of tools //ACM Transactions on Embedded Computing Systems (TECS). – – Т. 7. –. 3. – С. 36. (

85 85 Спасибо за внимание!