Коректне проектування апаратно-програмних засобів обчислювальної техніки на основі логічних мов специфікацій і сучасних мов опису дискретних систем

Размещено на http://www.allbest.ru/

НАЦІОНАЛЬНА АКАДЕМІЯ НАУК УКРАЇНИ

ІНСТИТУТ КІБЕРНЕТИКИ ІМЕНІ В.М. ГЛУШКОВА

УДК 519.713.1

Автореферат

дисертації на здобуття наукового ступеня

кандидата технічних наук

КОРЕКТНЕ ПРОЕКТУВАННЯ АПАРАТНО-ПРОГРАМНИХ ЗАСОБІВ ОБЧИСЛЮВАЛЬНОЇ ТЕХНІКИ НА ОСНОВІ ЛОГІЧНИХ МОВ СПЕЦИФІКАЦІЙ І СУЧАСНИХ МОВ ОПИСУ ДИСКРЕТНИХ СИСТЕМ

05.13.13 - обчислювальні машини, системи та мережі

ЗАКУТАЙЛО ДЕНИС ОЛЕКСАНДРОВИЧ

Київ - 2006

Дисертацією є рукопис.

Робота виконана в Інституті кібернетики імені В.М. Глушкова НАН України.

Науковий керівник:

Коваль Валерій Миколайович, доктор технічних наук, професор, Інститут кібернетики ім. В.М. Глушкова НАН України.

Офіційні опоненти:

Кривий Сергій Лук'янович, доктор фізико-математичних наук, професор, Інститут кібернетики ім. В.М. Глушкова НАН України;

Марковський Олександр Петрович, кандидат технічних наук, доцент, Національний технічний університет України, "Київський політехнічний інститут".

Провідна організація: Інститут проблем математичних машин та систем, відділ "Інтегрованих автоматизованих систем спеціального призначення".

Захист відбудеться "10" січня 2007 р. о (об) 14 годині на засіданні спеціалізованої вченої ради Д 26.194.03 при Інституті кібернетики ім. В.М. Глушкова НАН України за адресою: 03680, МСП, Київ-187, проспект Академіка Глушкова, 40.

З дисертацією можна ознайомитись у науково-технічному архіві Інституту кібернетики ім. В.М. Глушкова НАН України.

Автореферат розісланий "4" грудня 2006 р.

Учений секретар спеціалізованої вченої ради Романов. В.О.

ЗАГАЛЬНА ХАРАКТЕРИСТИКА РОБОТИ

Актуальність теми дисертаційного дослідження. У зв'язку з бурхливим розвитком технічного прогресу в мікроелектроніці з'явилася можливість виготовлення цифрових систем, які містять мільйони логічних вентилів. При розробці таких складних пристроїв неминуче виникають помилки, як на стадії проектування, так і в процесі виробництва кінцевого продукту. Особливо зазнають помилок проектування системи реального часу, вимоги до функціонування яких містять суворі часові обмеження на виконання певних дій. Помилки у функціонуванні таких систем, як системи керування ядерними реакторами, хімічним виробництвом, засобами космічної техніки можуть призвести до катастрофічних наслідків, пов'язаних з великими матеріальними втратами й людськими жертвами. Тому до надійності й безпомилковості функціонування таких систем пред'являються надзвичайно суворі вимоги, для задоволення яких необхідні методи коректного проектування такого роду систем.

Одним з підходів до коректного проектування є тестування. Тестова послідовність задається за допомогою вказівки значень сигналів у певні моменти часу. У такий спосіб важко описати складні часові залежності для багатьох сигналів, крім того, верифікується тільки певне коло властивостей. Для послідовних пристроїв такий спосіб гарантує вірогідність отриманих результатів тільки на тих послідовностях станів, які брали участь у тестуванні. Про істинність або хибність властивостей на послідовностях станів, які не брали участь у тестуванні, нічого не можна стверджувати. Тому при проектуванні високо надійних систем важливого значення набуває використання формальних методів, що засновані на мовах, методах і інструментальних засобах для специфікації й верифікації таких систем.

Для застосування формальних методів верифікації апаратних і програмних систем необхідно одержати модель системи, що верифікується. Це завдання полягає в перетворенні опису пристрою у формалізм, що розуміється системою верифікації.

Багато розробників систем для верифікації часових властивостей використовували запропоновані ними мови для опису об'єкта, що верифікується. Сучасні розробники електронних систем на ПЛІС використовують мови VHDL і Verilog. Тому у якості мови для опису об'єкта, що верифікується, доцільно використовувати одну із цих мов. При цьому для розробника відпадає необхідність вивчати ще будь-яку мову опису електронних схем для проведення верифікації.

Більшість формалізмів, які використовувались для опису моделі системи, що верифікується, ґрунтуються на дискретному поданні часу, при якому перехід між будь-якими двома станами моделі завжди триває однакову кількість часу. У цьому випадку верифікація тверджень, що вимагають явного кількісного завдання часу, приводить до значного росту числа станів моделі. Наприклад, якщо перехід між станами вихідної моделі дорівнює 1 нс, то при верифікації твердження, про те що, якщо подія X трапилася в цей момент часу, то в майбутньому обов'язково не пізніше ніж через 30 нс наступить подія Y, прийдеться ввести 29 нових станів. Таким чином, верифікація систем при наявності явних часових обмежень неефективна при використанні фіксованого інтервалу дискретного часу.

Після одержання моделі системи, що верифікується, необхідно специфікувати необхідні властивості роботи пристрою. Така специфікація звичайно описується за допомогою формул деякої логічної мови. Для запису властивостей з явними часовими обмеженнями необхідний відповідний формалізм. Так, Алуром і Хензингером було запропоновано часову логіку TCTL. Ця логіка інтерпретується на структурах з неперервним часом. При такій моделі часу складність перевірки на моделі є експонентною від розміру двійкового подання часових обмежень. Така експонентна залежність обмежує можливість верифікації систем промислового масштабу.

Із усього сказаного випливає, що розробка методів коректного проектування апаратно-програмних засобів обчислювальної техніки на основі логічних мов специфікацій, що допускають кількісний опис часових обмежень, і сучасних мов опису дискретних систем є актуальною задачею.

Зв'язок роботи з науковими програмами й темами. Дослідження по роботі проводилися у рамках наступних науково-дослідних робіт: "Розробити теоретичні основи та створити високопродуктивні мультипроцесорні інтелектуальні ЕОМ з кластерною організацією обробки інформації для вирішення обчислювальних задач та задач штучного інтелекту" номер державної реєстрації 0103U000709 (2003-2007), "Теоретичні аспекти розвитку високопродуктивних ЕОМ з високим рівнем машинного інтелекту" номер державної реєстрації 0101U000077 (2001-2005), "Розробка теоретичних та технологічних засад знання-орієнтованих комп'ютерних систем для широкого призначення" номер державної реєстрації 0102U003207 (2002-2006).

Метою дисертаційної роботи є розробка методів верифікації алгоритмів функціонування дискретних систем, що задовольняють заданим часовим обмеженням, на основі методу перевірки властивостей на моделі, що вимагає розробки відповідних часових логік для опису властивостей алгоритмів і методів побудови моделей систем, описаних у сучасних мовах проектування.

Основні задачі дисертаційної роботи, що визначені поставленою метою, полягають у наступному:

1) провести аналіз існуючих часових логік з погляду можливості й зручності їхнього використання для кількісного опису часових властивостей алгоритмів, що верифікуються;

2) розробити часові логіки, що дозволяють кількісно охарактеризувати часові властивості алгоритмів, що верифікуються;

3) розробити й реалізувати алгоритм трансляції VHDL описів, що містять явні часові затримки, у детерміновані кінцеві автомати;

4) розробити й реалізувати алгоритм перевірки еквівалентності пристроїв, заданих на VHDL;

5) здійснити модифікацію існуючих алгоритмів перевірки на моделі, пов'язану з використанням запропонованих логік;

6) провести оцінку часової складності запропонованих алгоритмів перевірки на моделі.

Об'єктом дослідження даної роботи є процес верифікації апаратно-програмних засобів на основі методу перевірки на моделі.

Предметом дослідження є методи перевірки властивостей, що характеризуються явними часовими обмеженнями, на моделі, побудованої по специфікації мовою VHDL.

Методи досліджень ґрунтуються на теорії автоматів, яку застосовано для розробки лексичного й синтаксичного аналізаторів системи верифікації; теорії графів, яку застосовано для розробки алгоритму перевірки на моделі формул запропонованої логіки LCTL, за допомогою обходу графа переходів пристрою, що верифікується; теорії складності, що дозволяє дати теоретичну оцінку складності розроблених алгоритмів; теорії часових логік, яку застосовано для опису властивостей системи, що верифікуються; теорії нерухомої точки, за допомогою якої описані всі оператори логіки LCTL.

Наукова новизна отриманих результатів полягає в наступному:

1) Одержала подальший розвиток теорія часових логік, а саме: розроблені часові логіки, що дозволяють кількісно характеризувати часові властивості алгоритмів, що верифікуються. Семантика цих часових логік, дозволяє використовувати моделі алгоритмів, що верифікуються, із числом станів меншим, ніж у відповідних моделях для існуючих часових логік і їх семантик;

2) Уперше запропоновані методи трансляції програм з мови VHDL, яка застосовує конструкції з часовими затримками, у транзиційні системи. Роботи інших дослідників у цій області стосувалися мови VHDL без часових затримок. Використання конструкцій мови VHDL з часовими затримками дозволяє істотно скоротити строки розробки дискретних систем;

3) Одержав подальший розвиток метод перевірки на моделі, а саме: для запропонованих логік розроблені методи перевірки властивостей з явними часовими обмеженнями, отримано оцінку часової складності запропонованого методу перевірки на моделі для логіки LCTL.

Практичне значення отриманих результатів. Практичне значення розробленої системи для верифікації цифрових пристроїв, описаних мовою VHDL, полягає в тісній інтеграції із САПР фірми Xilinx, обліку явних часових затримок. Запропоновані алгоритми дозволили верифікувати транзиційні системи практичного рівня складності з часовими обмеженнями на переходи.

Запропоновані методи, алгоритми й засоби проектування використалися в ряді розробок, у тому числі:

1) автоматичного метеорологічного аеродромного комплексу АМАС "Авіа-1" разом з підприємством "Инкомтех",

2) мобільного метеорологічного комплексу разом з підприємством "Инкомтех".

Теоретичні й прикладні результати досліджень передбачається використовувати в ряді навчальних курсів по відповідним спеціальностям у Національному авіаційному університеті, м. Київ.

Особистий внесок здобувача. Всі наукові й практичні результати, наведені в дисертації, отримані особисто здобувачем.

Апробація результатів дисертації. Результати дослідження неодноразово обговорювалися на семінарах Наукової ради НАН України з проблеми "Кібернетика": "Питання теорії проектування ЕОМ і інтелектуальних вирішальних систем", "Теорія автоматів і її застосування", на міжнародних науково-технічних конференціях "Штучний інтелект", що проходили в сел. Кацивелі, Україна, з 16-20 вересня 2002 р. і в сел. Дивноморськ, Росія, 22-27 вересня 2003.

Публікації. За темою дисертації опубліковано 6 наукових праць, причому 4 із них - статті у фахових виданнях наукових праць, 2 - публікації в матеріалах науково-практичних конференцій.

Структура й об'єм роботи. Дисертація складається із вступу, п'яти розділів, висновків, списку літератури з 83 найменувань. Загальний обсяг дисертації - 154 сторінок, обсяг основного тексту дисертації - 136 сторінок.

ОСНОВНИЙ ЗМІСТ ДОСЛІДЖЕННЯ

У вступі обґрунтовано актуальність теми дисертації, сформульовано мету й задачі роботи, наведено загальну характеристику роботи й одержані в ній наукові й практичні результати.

У першому розділі наведено опис математичних методів, часових логік, структур даних, застосовуваних для верифікації. Структури даних типу BDD використовуються в розробленій системі верифікації для компактного подання відношень на скінченних множинах. Наведено основну інформацію про ці структури. У цьому розділі також приводиться опис часових логік CTL, LTL. Часова логіка CTL лягла в основу пропонованих часових логік LCTL, GCTL. Викладено сучасні методи верифікації: дедукція, перевірка на моделі. Наведено приклади використання обох методів.

У другому розділі описано пропоновані часові логіки LCTL, GCTL, що дозволяють специфікувати кількісні часові властивості.

Часова логіка LCTL є розвитком логіки CTL і містить як всі оператори логіки CTL, так і ряд нових операторів, що враховують зміну часової структури, на якій інтерпретується логіка. Семантика LCTL визначається за допомогою структури , що є модифікованою структурою Крипке, де - множина станів модифікованої структури Крипке; - тотальне відношення переходів, (тобто); - множина атомарних висловлень; - функція, що ставить у відповідність кожному стану множину атомарних висловлень, істинних у цьому стані.

Далі характеристична функція відношення має те ж саме ім'я.

Шляхом у М називається така нескінченна послідовність, що. Запис, використовується для позначення шляху, що починається в стані .

Синтаксис мови LCTL збігається із синтаксисом мови CTL з додаванням операторів. дискретна алгоритм часове логіка

Нижче використані наступні позначення: - атомарне висловлення;, - формули LCTL. Семантика операторів логіки LCTL збігається із семантикою однойменних операторів логіки CTL, для інших операторів логіки LCTL відношення виконуваності формули в стані структури визначається в такий спосіб:

1) коли в кожному шляху, що починається в, у стані цього шляху істинна формула, і час, за який з досягне, задовольняє умові;

2) коли існує такий шлях, що починається в, у стані якого істинна формула, і час, за який з досягне, задовольняє умові;

3) коли в кожному шляху, що починається в, існує такий стан, що формула істинна в ньому, і у всіх станах цього шляху, де істинні формула й помилкова формула, і сумарний час, за який з досягне, задовольняє умові;

4) коли існує шлях, що починається в, у стані якого істинна формула, і у всіх станах цього шляху, де істинні формула й помилкова формула, і сумарний час, за який з досягне, задовольняє умові;

5) коли в кожному шляху, що починається в, у всіх станах, де істинна формула, і час, за який з досягне, де задовольняє умові;

6) коли існує такий шлях, що починається в, у якому у всіх станах, де істинна формула, і час, за який з досягне, де задовольняє умові.

Для зручності користування запропонованою логікою вводиться ряд додаткових операторів.

Для логіки LCTL наведено алгоритм перевірки на моделі за допомогою явного обходу графа переходів пристрою, що верифікується. Наведено приклади запису властивостей, що верифікуються, у цих логіках, оцінки істинності цих властивостей на моделях транзиційних систем.

Доведено оцінку часової складності алгоритму перевірки на моделі для логіки LCTL. А саме, часова складність алгоритму CheckLCTL дорівнює O(|f|*(|S|+r*|R|)).

Часова логіка GCTL є розвитком логіки CTL і містить як всі оператори логіки CTL, так і ряд нових операторів, що враховують властивості структури, на якій інтерпретується логіка.

Для інтерпретації формул GCTL необхідна транзиційна система з нескінченним числом станів, де структура визначена вище. Тут - множина станів системи; - множина початкових станів; відношення визначається в такий спосіб: тоді й тільки тоді, коли.

Переходом у транзиційної системі називається така трійка, що. Трійку будемо також записувати як. Нескінченним шляхом, що починається в стані, транзиційної системи називається нескінченна послідовність переходів, тобто для кожного трійка.

Синтаксис мови GCTL збігається із синтаксисом мови LCTL.

Нижче використані наступні позначення: - атомарне висловлення;, - формули GCTL. Семантика операторів логіки GCTL збігається із семантикою однойменних операторів логіки CTL, для інших операторів логіки GCTL відношення виконуваності формули в стані структури визначається в такий спосіб:

1) коли для кожного шляху, що починається в, у стані цього шляху істинна формула, і час, що дорівнює плюс час переходу з у, задовольняє умові;

2) коли існує такий шлях, що починається в, і в стані якого істинна формула, і час, який дорівнює плюс час переходу з у, задовольняє умові;

3) коли в кожному шляху, що починається в, існує такий стан, в якому істинна формула й у всіх станах цього шляху, де істинні формула й заперечення формули, і час, що дорівнює плюс час, за який з досягається, задовольняє умові;

4) коли існує такий шлях, що починається в, і в стані якого істинна формула, і у всіх станах цього шляху, де істинні формула й заперечення формули, і час, що дорівнює плюс час, за який з досягається, задовольняє умові;

5) коли в кожному шляху, що починається в, у всіх станах, де, істинна формула, і час переходу з у, де задовольняє умові;

6) коли існує такий шлях, що починається в, у якому у всіх станах, де, істинна формула, і час переходу з у, де, задовольняє умові.

Для зручності використання запропонованої логіки вводиться додаткові оператори, що виражаються через оператори, що наведено вище:

Приклад. Оцінимо виконуваність формули мови GCTL на структурі M, представленої на мал. 1. Ця формула істинна в стані тоді й тільки тоді, коли в кожному шляху, що починається в, існує такий стан, що формула істинна в ньому й у всіх станах цього шляху, де істинна формула й хибна формула , час , рівний .

У стані формула хибна, тому що в стані хибні формула й формула. У стані, де формула істинна. У стані, де формула істинна. У стані, де формула істинна. У стані формула хибна, тому що в стані хибні формула й формула . У стані, де формула істинна.

У третьому розділі розглядається розроблена програмна система для дослідження запропонованих часових логік LCTL і GCTL. Основною проблемою при цьому є обчислення множини станів розглянутої модифікованої структури Крипке, на яких істинна задана формула. Для запису властивості, що верифікується, необхідно ввести список атомарних висловлень. Після цього користувач може візуально створити модифіковану структуру Крипке для системи, що верифікується. Для подання в системі відношення переходів необхідно здійснити кодування станів, що належать першій і третій проекціям цього відношення, а також часів переходів значеннями уведених для цього змінних. Так, для приклада на рис. 2 стани, що належать першій і третій проекціям R кодуються відповідно змінними, а значення часів переходів - змінними. Відповідні коди станів показані на рис. 2.

Після завдання формули, що описує властивість, що верифікується, мовою LCTL або GCTL програмна система здійснює перевірку виконуваності цієї формули на моделі системи.

Наведено синтаксис мови специфікації часових властивостей, використовуваної в системі, що однаковий для логік LCTL і GCTL. Для кожного оператора мови LCTL визначене монотонне перетворення множини станів модифікованої структури Крипке. Обчислення множини станів структури Крипке, на яких істинна задана формула логіки LCTL, здійснюється шляхом обчислення найменшої (найбільшої) нерухомої точки перетворення, що відповідає головному операторові цієї формули.

Четвертий розділ присвячений опису й обґрунтуванню методів трансляції VHDL програми у функцію переходів автомата, що подається за допомогою BDD структури. Для одержання функції переходів із програми на VHDL необхідно перетворити вихідний опис в абстрактне синтаксичне дерево.

Конструкції VHDL можуть виконуватися послідовно або паралельно. Паралельно виконуються процеси; присвоєння значень сигналам, якщо останні перебувають поза процесом. Послідовно виконуються оператори, що перебувають у тілі процесу. Хоча можливо паралельне присвоєння значень сигналам, що не належать яким-небудь процесам, однак такі присвоєння завжди можна перетворити в присвоєння усередині спеціально створених процесів. При цьому необхідно останнім виразом процесу зробити конструкцію, де x права частина присвоювання, - множина сигналів, які входять у вираз x. Таким чином, задачу перетворення VHDL тексту в автомат можна звести до задачі перетворення відповідних процесів.

Для кожного виразу wait необхідно обчислити умову, за якою відбувається поновлення відповідного процесу по формулі, де - масив, що містить умови поновлення; i - номер wait виразу, нумерація починається з 1.

Тому що виконання VHDL процесу припиняється в wait виразах х, то такі вирази можна розглядати, як стани деякого автомата, що описує вихідну програму. Для подання цих станів уводиться змінна state. Значення цієї змінної дорівнює номеру останнього виконаного виразу wait, що спричинив припинення навколишнього процесу. Для обробки wait виразів виконуються наступні кроки:

1) пронумерувати wait вирази,

2) вставити вираз state=i, де i номер wait вираза

3) сформувати масив Resump, що містить умови поновлень роботи процесів

4) сформувати список останніх станів процесів.

Нумерація wait виразів необхідна для встановлення відповідності між wait конструкцією й станом автомата, що описує вихідну програму. Другий крок необхідний для одержання функцій переходу між станами автомата. Після виконання третього кроку вирази wait стають більше непотрібними й тому знищуються й замість них вставляються конструкції виду state=i. Такі вставки необхідні для подальшої деталізації функцій переходу. Нумерація wait виразів починається з 1. Для коректної побудови автомата по VHDL програмі необхідно, крім станів відповідних wait виразам увести початковий стан. Саме тому індекс 0 зарезервований для позначення початкового стану.

Формування списку останніх станів процесів необхідно для коректного формування функції переходу автомата VHDL програми. При обчисленні функції переходу необхідно знати попередній стан описуваної програми. При послідовному виконанні процесу зверху донизу заздалегідь невідомо, який стан процесу буде останнім. Для того щоб знати заздалегідь, які стани процесів є останніми, уводиться список останніх станів процесів.

Семантика присвоєння значення сигналам відрізняється від присвоєння значення змінної відповідно до стандарту VHDL. Присвоєння змінної виконується негайно. Якщо змінна, якій привласнене нове значення, зустрічається далі при виконанні процесу, то розглядається вже нове значення цієї змінної. При присвоєнні значення сигналу, значення сигналу не змінюється, змінюється лише ефективне значення сигналу. Якщо деякому сигналу усередині процесу привласнені значення й цей сигнал зустрівся усередині процесу знову, то значення сигналу залишається попереднім. Сигнал одержить нове значення тільки після того, як всі процеси призупиняться, до цього моменту часу значення сигналу не змінюється. Таким чином, необхідно знати умову, при якому всі процеси призупиняться. Таку умову можна виразити формулою.

Для одержання функцій переходів для сигналів і змінних необхідно обійти все дерево VHDL програми й пройти по всіх його гілках. При цьому якщо зустрінеться присвоєння змінної, то обчислити нове значення змінної, з огляду на всі умови, які зустрінуться у відповідних гілках умовних операторів по формулі:

NewVal [Variable]= CurCond LastState Value (CurCond LastState) OldValue,

де CurCond - вирази утворені гілками умовних операторів; LastState - останній стан процесу; Value - значення, що привласнюється; OldValue - поточне значення змінної; NewVal [Variable]- функція, що представляє нове значення змінної.

Якщо зустрінеться присвоєння сигналу, то нове значення сигналу обчислюється за формулою:

NewVal [Signal]= stop_cond CurCond LastState Value (stop_cond CurCond LastState) OldValue,

де stop_cond умова припинення процесів; CurCond - вираз, утворений гілками умовних операторів; LastState - останній стан процесу; Value - значення, що привласнюється; OldValue -поточне значення сигналу; NewVal [Variable]- функція, що представляє нове значення сигналу.

У п'ятому розділі розглянута розроблена система для верифікації часових властивостей з явними часовими обмеженнями, що використовує як модель дискретної системи опис пристрою мовою VHDL. Особливості системи полягають у наступному:

1) розроблювальна система верифікації орієнтована на взаємодії з існуючими САПР для проектування цифрових систем на ПЛІС;

2) у системі реалізований транслятор з деякої підмножини VHDL0 конструкцій мови VHDL у функції переходів;

3) для опису часових властивостей використовуються запропоновані часові логіки, що дозволяють кількісно характеризувати часові властивості систем, що верифікуються;

4) у системі реалізований метод перевірок на моделі для запропонованих логік;

5) можлива генерація тестових послідовностей, що задовольняють користувальницьким критеріям;

6) за бажанням користувача здійснюється перевірки досяжності станів у системі;

7) система дозволяє встановлювати еквівалентність двох описів пристроїв на VHDL0.

Для опису цифрових систем у САПР широко використовується мова VHDL. Вибір підмножини VHDL0 був продиктований використовуваною підмножиною мови VHDL у САПР фірми Xilinx. Приводяться приклади використання конструкцій мови VHDL0.

Система, одержавши вхідні дані, перевіряє істинність або хибність сформульованих тверджень на всіх досяжних станах цифрової системи, описаної на VHDL. При невиконанні необхідної властивості генерується контрприклад. У випадку виконання властивості система (за бажанням користувача) генерує приклад, що підтверджує істинність властивості. Спрощений алгоритм роботи системи зображений на рис. 3.

Можливість встановлення еквівалентності двох описів пристроїв на VHDL може бути корисна в наступних випадках:

1) Дано два описи на VHDL, потрібно встановити їхню семантичну ідентичність.

2) За допомогою САПР отримано структурний опис пристрою на VHDL, користувач вносить зміни й необхідно довідатися, чи не вплинуть вони на функціонування схеми.

3) Поведінковий опис на VHDL перетворюється в структурний опис за допомогою синтезатора САПР. У цьому процесі дуже важливо гарантувати еквівалентність двох описів. Якщо виявляється невідповідність, то це свідчить про серйозні помилки в роботі синтезатора САПР. Таким чином, можна провести верифікацію синтезатора САПР.

Шостий розділ містить висновки даної роботи.

Далі представлений список літератури і додаток, який містить акті про впровадження результатів дисертаційної роботи.

ВИСНОВКИ

Сукупність отриманих у дисертації результатів пов'язана з розробкою підходу до верифікації алгоритмів функціонування дискретних систем, що задовольняють заданим часовим обмеженням, на основі методу перевірки властивостей на моделі, що обумовило розробки відповідних часових логік для опису властивостей алгоритмів і методів побудови моделей алгоритмів, описаних у сучасних мовах проектування.

При цьому були отримані наступні основні результати:

1) Одержала подальший розвиток теорія часових логік, а саме: розроблено часові логіки, що дозволяють кількісно характеризувати часові властивості алгоритмів, що верифікуються. Семантика цих часових логік, дозволяє використовувати моделі алгоритмів із числом станів меншим, ніж у відповідних моделях для існуючих часових логік і їх семантик;

2) Уперше запропоновано методи трансляції програм з мови VHDL, що застосовує конструкції з часовими затримками, у транзиційні системи. Використання конструкцій мови VHDL з часовими затримками дозволяє істотно скоротити строки розробки дискретних систем;

3) Реалізовано транслятор з мови VHDL у функції переходів транзиційної системи;

4) Одержав подальший розвиток метод перевірки на моделі, а саме: для запропонованих логік розроблені методи перевірки властивостей з явними часовими обмеженнями, отримано поліноміальну оцінку часової складності запропонованого методу перевірки на моделі для логіки LCTL;

5) Для дослідження властивостей одної із запропонованих часових логік (LCTL) реалізована система для перевірки виконуваності формул цієї логіки;

6) Розроблено автоматизовану систему верифікації цифрових систем, описаних мовою VHDL, що використовує запропоновані часові логіки.

Реалізація на практиці перерахованих вище результатів дозволяє значно скоротити строки розробок, істотно зменшивши обсяг робіт, пов'язаних із забезпеченням коректності функціонування апаратно-програмних систем.

Можливі напрямки розвитку даної роботи. Необхідно верифікувати значно більше описів електронних пристроїв на VHDL за допомогою розробленої системи верифікації. Аналіз прикладів верифікації конкретних пристроїв дозволить увести ряд необхідних операторів, що спрощують специфікацію властивостей, що верифікуються.

У даній роботі запропоновані методи перетворення найбільш уживаних конструкцій мови VHDL у функції переходів. Бажано розширити кількість перетворюваних конструкцій до повного стандарту мови. Це дозволило б розглядати кінцеву програму як комерційний продукт, а не як дослідницьку роботу.

СПИСОК ОПУБЛІКОВАНИХ РОБІТ З ТЕМ ДИСЕРТАЦІЇ

1. Закутайло Д.А. Использование структур данных типа BDD для формальной верификации аппаратуры // Нові комп`ютерні засоби, обчислювальні машини та мережі. - Киев: Институт кибернетики имени В.М. Глушкова, 2001. - Т.1. - С. 140-152.

2. Закутайло Д.А. Современные автоматизированные системы для формальной верификации аппаратуры (обзор) // Засоби комп`ютерної техніки з віртуальними функціями і нові інформаційні технології. - Киев: Институт кибернетики имени В.М. Глушкова, 2002. - С. 99-104.

3. Закутайло Д.А. Автоматизированная система верификации цифровых систем // Искусственный интеллект. - Донецк: Институт проблем искусственного интеллекта, 2003. - №3. - С. 95-101.

4. Закутайло Д.А. Трансляция VHDL программы в BDD структуры // Комп`ютерні засоби, мережі та системи. - Киев: Институт кибернетики имени В.М. Глушкова, 2003. - №2. - С. 144-150.

5. Закутайло Д.А. Язык спецификации временных свойств дискретных систем // Международная научно-техническая конференция "Искусственный интеллект". - Таганрог, Изд-во ТРТУ: 2002. - Т.1. - С. 236-237.

6. Закутайло Д.А. Автоматизированная система верификации цифровых систем // Международная научно-техническая конференция "Интеллектуальные и многопроцессорные системы-2003". - Таганрог, Изд-во ТРТУ: 2003. - Том 2. - С. 113-116.

АНОТАЦІЯ

Закутайло Д.О. Коректне проектування апаратно-програмних засобів обчислювальної техніки на основі логічних мов специфікацій і сучасних мов опису дискретних систем. - Рукопис.

Дисертація на здобуття наукового ступеня кандидата технічних наук за фахом 05.13.13 - обчислювальні машини, системи й мережі. - Інститут кібернетики ім. В.М. Глушкова НАН України, Київ, 2006.

Наукова новизна отриманих результатів полягає в наступному: розроблені часові логіки LCTL і GCTL, що дозволяють кількісно характеризувати часові властивості алгоритмів, що верифікуються. Семантика цих часових логік, дозволяє використовувати моделі алгоритмів, що верифікуються, із числом станів меншим, чим у відповідних моделей для існуючих раніше часових логік і їх семантик; уперше запропоновані методи трансляції програм з мови VHDL, що застосовувають конструкції з часовими затримками, у транзиційні системи; для запропонованих логік розроблені методи перевірки властивостей з явними часовими обмеженнями, отримана оцінка часової складності запропонованого методу перевірки на моделі для логіки LCTL.

Практичне значення розробленої системи для верифікації цифрових пристроїв, описаних мовою VHDL, полягає в тісній інтеграції із САПР фірми Xilinx, обліку явних часових затримок. Запропоновані алгоритми дозволили верифікувати транзиційні системи практичного рівня складності з часовими обмеженнями на переходи.

Реалізація на практиці отриманих результатів дозволяє значно скоротити строки розробок, істотно зменшивши обсяг робіт, пов'язаних із забезпеченням коректності функціонування апаратно-програмних систем.

Ключові слова: верифікація, реактивні системи, VHDL, часові логіки, метод перевірки на моделі.

АННОТАЦИЯ

Закутайло Д.А. Корректное проектирование аппаратно-программных средств вычислительной техники на основе логических языков спецификаций и современных языков описания дискретных систем. - Рукопись.

Диссертация на соискание ученой степени кандидата технических наук по специальности 05.13.13 - вычислительные машины, системы и сети. - Институт кибернетики им. В.М. Глушкова НАН Украины, Киев, 2006.

В связи с бурным развитием технического прогресса в микроэлектронике появилась возможность изготовления цифровых систем, которые содержат миллионы логических вентилей. При разработке таких сложных устройств неизбежно возникают ошибки, как на стадии проектирования, так и в процессе производства конечного изделия. Особенно подвержены ошибкам проектирования системы реального времени, требования к функционированию которых содержат жесткие временные ограничения на выполнение некоторых действий. Ошибки в функционировании таких систем, как системы управления ядерными реакторами, химическим производством, средствами космической техники могут привести к катастрофическим последствиям, связанным с большими материальными потерями и человеческими жертвами. Поэтому к надежности и безошибочности функционирования таких систем предъявляются чрезвычайно жесткие требования, для удовлетворения которых необходимы методы корректного проектирования такого рода систем.

Научная новизна полученных результатов состоит в следующем: разработаны временные логики LCTL и GCTL, позволяющие количественно характеризовать временные свойства верифицируемых алгоритмов. Семантика этих временных логик, позволяет использовать модели верифицируемых алгоритмов с числом состояний меньшим, чем у соответствующих моделей для существовавших ранее временных логик и их семантик; впервые предложены методы трансляции программ с языка VHDL, использующего конструкции с временными задержками, в транзиционные системы; для предложенных логик разработаны методы проверки свойств с явными временными ограничениями, получена оценка временной сложности предложенного метода проверки на модели для логики LCTL.

Практическое значение разработанной системы для верификации цифровых устройств, описанных на языке VHDL, заключается в тесной интеграции с САПР фирмы Xilinx, учете явных временных задержек. Предложенные алгоритмы позволили верифицировать транзиционные системы практического уровня сложности с временными ограничениями на переходы.

Теоретические и прикладные результаты исследований предполагается использовать в ряде учебных курсов по соответствующим специальностям в Национальном авиационном университете, г. Киев.

Совокупность полученных в диссертации результатов связана с разработкой подхода к верификации алгоритмов функционирования дискретных систем, удовлетворяющих заданным временным ограничениям, на основе метода проверки свойств на модели, что потребовало разработки соответствующих временных логик для описания свойств алгоритмов и методов построения моделей алгоритмов, описанных в современных языках проектирования.

При этом были получены следующие основные результаты: разработаны временные логики, позволяющие количественно характеризовать временные свойства верифицируемых алгоритмов; впервые предложены методы трансляции программ с языка VHDL, использующего конструкции с временными задержками, в транзиционные системы; реализован транслятор с языка VHDL в функции переходов транзиционной системы; для предложенных логик разработаны методы проверки свойств с явными временными ограничениями; получена оценка временной сложности предложенного метода проверки на модели для логики LCTL; для исследования предложенных временных логик реализована система для проверки выполнимости временной формулы, описанной в одной из предложенных временных логик; разработана автоматизированная система верификации цифровых систем, описанных на языке VHDL, использующая предложенные временные логики.

Реализация на практике перечисленных выше результатов позволяет значительно сократить сроки разработок, существенно уменьшив объем работ, связанных с обеспечением корректности функционирования аппартно-программных систем.

Ключевые слова: верификация, реактивные системы, VHDL, временные логики, метод проверки на модели.

ABSTRACT

Zacoutailo D.A. The corrective design of the hardware and software package of computer systems on the basis of logical languages of specifications and modern languages of description of discrete systems. - Manuscript.

The thesis for the degree of Candidate of Technical Science in specialty No.05.13.13 - Computers, systems and networks. - Glushkov Institute of Cybernetics of the National Academy of Sciences of Ukraine. - Kyiv, 2006.

The scientific novelty of the obtained results consists in the following: there were developed temporal logics LCTL and GCTL that allow to describe in quantitative way the temporal properties of the verifying algorithms. Semantics of these temporal logics allow to use the model of the verifying algorithms with number of states which are less than that for the corresponding models for the existing temporal logics and their semantics; for the first time there were developed the new methods of the program translation from the VHDL language, which uses the constructs with temporal delays into transition system; the new methods are devised for proposed logics which will enable to verify properties with explicit real-time constraints, the new evaluation was obtained of the temporal complexity of the proposed method for the model-checking problem for LCTL logic.

The practical significance of the devised system for digital circuits verification which are described in VHDL language consist in close integration with Xilinx's CAD, and taking into account the explicit temporal delays. The proposed algorithms allow for verifying transition system of the practical level of complexity with temporal constraints for the transitions.

The practical realization of the above results allows substantially shortening the development time by significantly reducing the volume of work to ensure correctness of the hardware/software systems functioning.

Keywords: verifications, reactive systems, VHDL, temporal logics, model checking.

Размещено на Allbest.ru

...