Через {0, 1}, N, обозначается множество всех двоичных слов дли­ ны. Также рассматривается множество всевозможных двоичных слов произвольной конечной длины:

Далее под дискретными функциями понимаются любые функции вида : {0, 1}* {0, 1}*. Дискретные функции вида : {0, 1} {0, 1}*, N, называются дискретными функциями от переменных. Функции вида : {0, 1} {0, 1} называются булевыми.

Область определения и область значения дискретной функции будем обозначать соответственно через и.

Дискретные функции : {0, 1}* {0, 1}* и : {0, 1} {0, 1}*, N, называются всюду определенными (тотальными), если = {0, 1}*, Пусть = {1,..., } — множество булевых переменных и пусть (1,..., ) — произвольная формула исчисления высказываний [27]. Дан­ ная формула естественным образом задает тотальную булеву функцию от булевых переменных 1,...,. Тот факт, что при подстановке (1,..., ) принимает значение {0, 1} обозначаем через |(1,..., ) = левыми уравнениями (в некоторых источниках, например в [34], использу­ ется термин «логические уравнения»). Набор (1,..., ), {0, 1}, {1,..., }, такой, что (1,..., )|(1,..., ) =, {0, 1}, называется ре­ шением уравнения (1,..., ) =. Если такого набора не существует, то говорят, что данное уравнение не имеет решений.

Произвольный конечный набор булевых уравнений называется систе­ мой булевых уравнений (СБУ). Произвольный набор значений истинности булевых переменных, входящих в систему, являющийся решением всех ее уравнений, называется решением данной системы. Если такого набора не существует, то СБУ называется несовместной.

Далее в качестве базовой формальной вычислительной модели рас­ сматривается детерминированная машина Тьюринга (ДМТ) с входным ал­ фавитом = {0, 1} (см. [29]).

Произвольная ДМТ-программа, останавливающаяся на произволь­ ном входном слове из {0, 1}*, естественным образом задает тотальную дис­ кретную функцию : {0, 1}* {0, 1}*.

Очевидно, что данная функция может рассматриваться как счетное семейство дискретных функций вида : {0, 1} {0, 1}*, N. Стан­ дартным образом (см. [29]) можно определить временную сложность про­ граммы, вычисляющей функции данного семейства, как функцию от длины входа. Если сложность программы ограничена полиномом от, то функция называется полиномиально вычислимой.

Поведение дискретных систем из широкого класса может быть описа­ но полиномиально вычислимыми функциями. В качестве примеров можно привести различные управляющие/управляемые системы, в том числе на основе СБИС, протоколы обмена информацией в системах связи, шифрую­ щие преобразования и др. Криптографические функции в данном контек­ сте особенно важны как источники аргументированно сложных в вычисли­ тельном отношении тестов.

В последние годы в связи с интенсивным развитием таких областей как Hardware/Software model checking [35–38], комбинаторная оптимизация [39– 41], криптография/криптоанализ возрастает актуальность проблем разра­ ботки как методов решения булевых уравнений, так и методов преобразо­ вания комбинаторных задач в булевы уравнения.

1.2. Пропозициональное кодирование программ для формальных вычислительных моделей Базовые положения рассматриваемой далее техники пропозициональ­ ного кодирования программ для формальных вычислительных моделей впервые были предложены С. А. Куком в работе [42]. Следует отметить, что изначально теорема Кука воспринималась как результат «деструктивного»

характера, поскольку для определяемого с ее помощью класса задач скорее всего не существует полиномиальных алгоритмов. Однако наблюдающийся рост мощности вычислительной техники позволяет не воспринимать подоб­ ную аргументацию трудности задачи как непреодолимое препятствие. Дей­ ствительно, во многих практически важных частных случаях даже точные решения NP-трудных задач могут быть найдены за приемлемое время при помощи эвристик, базирующихся на «разумных аргументах». Сказанное означает актуальность проблем разработки как эффективных на практике вычислительных алгоритмов решения систем булевых уравнений большой размерности, так и процедур сведения различных комбинаторных задач к булевым уравнениям.

Для разработки практически применимой технологии преобразования алгоритмов, вычисляющих дискретные функции, в булевы уравнения необ­ ходимо построение прототипа данной технологии на уровне формальной вычислительной модели. Выбираемая при этом формальная модель долж­ на обеспечивать относительно простой переход от разработанного прототи­ па к процедурам преобразования в булевы уравнения алгоритмов, записан­ ных на процедурных языках программирования. Кроме этого, архитекту­ ра такой модели должна быть максимально близка к архитектурам совре­ менных ЭВМ. Всем перечисленным требованиям удовлетворяет машина с произвольным доступом (RAM) (см. [43]). Далее используется вариант RAM, синтаксис программ которой фактически совпадает с синтаксисом программ для машины с неограниченными регистрами (МНР) в форма­ лизме Н. Катленда [28]. Он близок к синтаксису современных ассемблер­ ных языков, что делает данный вариант RAM перспективной основой для разработки теоретической базы технологии преобразования алгоритмов вы­ числения дискретных функций в булевы уравнения.

Итак, далее рассматривается двоичная (бинарная) RAM в формализ­ ме Н. Катленда. Ее рабочая область состоит из бесконечной вправо ленты, разделенной на ячейки, которые пронумерованы натуральными числами. В каждой ячейке может быть записан только один бит. Произвольная RAM­ программа — это нумерованный список команд, каждая из которых может быть командой одного из следующих двух типов:

1. команды записи в ячейку с номером бита «0» или бита «1» — соот­ ветственно 0 () и 1 ();

2. команды условного перехода (,, ) — сравнить содержимое ячеек с номерами и, в случае совпадения перейти к команде с номером в списке, в противном случае перейти к команде, которая следует в списке за командой (,, ).

Вычисление останавливается либо после выполнения последней коман­ ды в программе (если данная команда не является командой условного перехода), либо если происходит ссылка на несуществующую команду.

Пример 1.1 (см. [29]) Программа проверки делимости на 4 произвольно­ го натурального числа, двоичное представление которого имеет длину, может быть записана в виде:

2. (1, 1, 100) 3. (1,, 5) 4. (1, 1, 100) В первой ячейке записывается бит ответа: «0» означает, что число не делится на 4, «1» — число делится на 4. В начальной конфигурации RAM в первой ячейке записан «0», а в следующих ячейках записывается двоич­ ное представление натурального числа. Программа проверяет два младших бита числа на равенство нулю, если это выполняется, то в первую ячейку записывается «1».

1.2.1. Механизмы преобразования в булевы уравнения RAM-программ, вычисляющих дискретные функции Итак, далее рассматривается тотальная функция вычислимая программой для машины Тьюринга с входным алфавитом = {0, 1} за полиномиальное время. Как отмечалось выше, программа задает счетное семейство дискретных функций Проблемой обращения произвольной функции из данного семейства в точке называется следующая задача: зная, число и Пропозициональный подход к данной задаче основан на следующем факте: процесс работы программы на произвольном входе можно эф­ фективно (в общем случае за полиномиальное от время) представить в виде формулы исчисления высказываний. Истинность данной формулы при некоторых дополнительных условиях, характеризующих конкретный выход, означает существование такого входа {0, 1}, ре­ зультатом трансформации которого посредством программы является. Фактически в этом состоит теорема Кука [42].

Мы приводим два утверждения из работы [44], являющиеся теорети­ ческой базой описываемых далее процедур преобразования алгоритмов.

Лемма 1.1 (о моделировании) Пусть — ДМТ-программа, вычисляющая тотальную дискретную функцию : {0, 1}* {0, 1}*, и функция сложности программы ограничена некоторым полиномом от. Суще­ ствует тотальная алгоритмически вычислимая функция, которая за по­ линомиальное от время по тексту программы и числу выдает текст программы, вычисляющей функцию. Функция сложности (), со­ поставляемая получаемому семейству RAM-программ, ограничена сверху полиномом от.

Данный факт означает наличие эффективной процедуры перехода от ДМТ-программы, вычисляющей, к семейству RAM-программ, каждая из которых вычисляет функцию, N. Как уже отмечалось, синтаксис RAM-программ близок к ассемблерным программам, что крайне важно при построении практичных процедур пропозиционального кодирования алгоритмов. В техническом плане доказательство леммы 1.1 стандартно — работа ДМТ с входным алфавитом {0, 1} на всевозможных входах длины моделируется на описанной выше RAM. Данная лемма используется при доказательстве следующей теоремы.

Теорема 1.1. Пусть = { }N — семейство алгоритмически вычисли­ мых за полиномиальное время дискретных функций и пусть { }N — семейство RAM-программ, сопоставляемое в соответствии с леммой о моделировании. Существует алгоритмически вычислимая тотальная функ­ ция, которая, получая на входе текст программы, за полиномиальное в общем случае от время строит такую систему булевых уравнений ( ), что:

1. для произвольного система ( ) | совместна;

2. если — решение системы ( ) |, то за линейное от |^| время воз­ Доказательство. Полное доказательство данного факта приведено в [44]. Здесь мы приводим несколько иное доказательство, дающее основу для последующего построения программного комплекса, осуществляющего преобразования процедурных описаний алгоритмов вычисления дискрет­ ных функций в булевы уравнения.

Базовая идея пропозиционального кодирования алгоритмов состоит в построении символьного описания всех возможных эволюций соответству­ ющего вычисления на произвольных входах. В нашем случае требуется описать поведение RAM-вычисления на всевозможных входных двоичных словах длины. Это можно сделать, если описывать каждую последую­ щую конфигурацию набором функций от предыдущей конфигурации. Если к некоторой конфигурации применяется оператор условного перехода, то, вообще говоря, возможен переход как в +, так и в, однако можно рассмотреть «абстрактную» конфигурацию +1, ячейкам которой сопоставлены булевы переменные, принимающие (в зависимости от соот­ ветствующего условия) либо значения, которые формируют конфигурацию +, либо значения, которые формируют конфигурацию. Тем самым, биты в ячейках памяти RAM в конфигурации +1 можно считать значени­ ями булевых функций от содержимого памяти RAM в конфигурации.

Данные функции можно записать в явном виде, используя только текст программы. Очень важно то, что при этом мы точно знаем, сколько потребуется булевых переменных, кодирующих содержимое памяти RAM в конфигурации +1. Это число заведомо не больше максимального номера ячейки, к которой обращается программа в процессе вычисления.

Рис. 1.2. Условный переход в RAM-программе.

Итак, процесс пропозиционального кодирования программы состо­ ит в следующем. Предполагается, что получает на вход произвольный двоичный вектор, кодируемый булевыми переменными 1,..., (старто­ вая конфигурация 0 ). Предположим, что первой командой в является команда условного перехода (,, ). Символически переход из 0 в + или в представлен на рисунке 1.2.

Для описания конфигурации 1 вводятся переменные 1,..., 1, где () — максимальное натуральное число, фигурирующее в тексте програм­ мы (рост функции () ограничен некоторым полиномом от ). Каж­ дой переменной 1, {1,..., ()}, ставим в соответствие формулу где (1,..., ) — формула исчисления высказывания, задающая некото­ рую булеву функцию от переменных 1,...,. Далее действуем по ана­ логии: содержимое конфигурации 2 кодируется булевыми переменными 2, {1,..., ()}, связанными с формулами И так далее. Пусть — множества переменных, соответствующие в указанном смысле конфигу­ рациям 0, 1,..., ( — заключительная конфигурация). Описанный процесс изображен на рисунке 1.3.

Данному процессу сопоставляется следующая система булевых урав­ нений, обозначаемая через ( ):

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

В [44] показано, что система (1.1) обладает следующими свойствами:

1. размерность системы ( ) ограничена полиномом от ;

2. подстановка в ( ) произвольного вектора {0, 1}* дает несов­ лучаем систему ( ) | относительно переменных из 0..., имеющую решения;

3. пусть — некоторое решение системы ( ) |, тогда из построения данной системы следует, что вектор длины, образованный компо­ нентами в, которые соответствуют переменным из множества 0, дает прообраз в {0, 1} при отображении.

Все сказанное означает справедливость теоремы 1.1.

Следующие примеры иллюстрируют основные принципы пропозицио­ нального кодирования алгоритмов, описанные в доказательстве теоремы 1.1.

Пример 1.2. Рассматривается регистр сдвига с линейной обратной свя­ зью (далее РСЛОС) (см. [45], [46], [47]). РСЛОС длины, задаваемый по­ линомом обратной связи () = + 1 1 +... + 1 1 + 0 над по­ лем GF(2), обозначается через, () ( — формальная переменная).

Выходная последовательность длины данного генератора — это после­ довательность битов, являющаяся результатом первых тактов работы РСЛОС. Сами по себе РСЛОС не являются криптографически стойкими, однако они используются в качестве примитивов в более сложных шиф­ рах. Далее предполагается, что выходом регистра сдвига на каждом такте является крайний правый бит регистра.

Рис. 1.4. Схема n-битного РСЛОС с функцией обратной связи.

Рассмотрим -битный РСЛОС как фрагмент памяти RAM. Полагаем, что множество булевых переменных 0 = {0,..., 0 } кодирует началь­ ное заполнение регистра, которое соответствует начальной конфигурации RAM-машины. Множества булевых переменных 1,...,, кодирующие соответствующие конфигурации RAM, строятся по формулам где (·) — функция обратной связи (см. [45]). Множество булевых перемен­ ных {,..., } кодирует выходную последовательность реги­ стра сдвига. Пусть биты выходной последовательности известны, тогда, подставив их в систему булевых уравнений, получим совместную систему. Из решения данной системы определяем на­ чальное заполнение 0 = 0,..., 0 регистра сдвига.

Пример 1.3. В этом примере строится система булевых уравнений, опи­ сывающая процесс порождения ключевого потока в известном генераторе поточного шифрования A5/1. Общая схема работы данного генератора вы­ глядит следующим образом (см. [46, 48]).

Рис. 1.5. Схема генератора ключевого потока А5/1.

В генераторе A5/1 используются три регистра с линейной обратной связью, задаваемые следующими полиномами обратной связи над GF(2):

19 + 18 + 17 + 14 + 1 (длина регистра 19 бит); 22 + 21 + 1 (длина регистра 22 бита); 23 + 22 + 21 + 8 + 1 (длина регистра 23 бита).

Ячейки регистров нумеруются с нуля и справа налево.

Особенностью данного генератора является то, что на каждом так­ те могут сдвигаться не все регистры. Сдвиг регистра с номером, {1, 2, 3}, происходит, если значение функции 1, 2, 3 равно 1, и не происходит, если значение данной функции равно 0. Функция (·) опре­ деляется следующим образом:

где majority (,, ) = · · · (функция большинства), 1, 2, 3 — так называемые серединные биты, то есть биты, находящиеся в девятой ячейке первого РСЛОС, и в ячейках с номером 11 во втором и третьем РСЛОС (на рисунке данные ячейки закрашены в темно-серый цвет).

В каждом такте с регистров снимаются старшие биты, складываются по mod 2, результирующий бит является битом ключевого потока данного такта. Задача криптоанализа состоит в нахождении начальных заполнений регистров по некоторой известной последовательности битов ключевого по­ тока и по известному алгоритму их порождения. Сведем данную задачу к задаче поиска решений системы булевых уравнений. Начальное заполнение регистров кодируем множеством булевых переменных 0 = 0,..., 0.

Далее приведена система булевых уравнений, описывающая шагов работы первого регистра в A5/1. Сдвиг регистра выполняется в зависимо­ сти от текущего значения битов 1, 2 и 3, и определяется булевой функ­ цией 1 *, *, *. Система (1.2) принимает вид:

{1,..., }. Аналогичным образом определяются системы, описываю­ щие работу второго и третьего РСЛОС в каждый такт с номером {1, 2,..., }. Остается добавить уравнения, описывающие формирование битов ключевого потока:

Объединив все перечисленные уравнения, получим систему булевых урав­ нений, описывающую шагов работы генератора А5/1. Таким образом, решение задачи криптоанализа генератора A5/1 по известным битам клю­ чевого потока сводится к решению полученной системы с подставленными в нее значениями переменных 1, 2,...,.

1.2.2. Преобразования Цейтина От произвольной системы ( ) | возможен эффективный (в общем случае за полиномиальное от время) переход к одному уравнению вида КНФ=1. Этот переход осуществляется при помощи преобразований Цей­ тина. При этом множество переменных разрастается (не более чем поли­ номиально), однако между множеством решений ( ) | и множеством решений получаемого уравнения вида КНФ=1 существует биекция [49].

Преобразования Цейтина были предложены Г. С. Цейтиным в 1968 го­ ду в работе [50] (перепечатана на английском языке в [51]). Данные преоб­ разования в последние годы активно используются в задачах верификации схем из функциональных элементов (см. [52–57]). Далее приведено описа­ ние преобразований Цейтина в контексте проблемы приведения систем бу­ левых уравнений к нормальным формам.

Дано булево уравнение Формулы,..., задают некоторые (в общем случае сложные) бу­ левы функции. Положим Введем булеву функцию 1 1,..., 11, 1, 1 : {0, 1}1 +1 {0, 1}, зна­ чение которой на произвольном векторе 1,..., 1, 1 {0, 1}1 +1 опре­ делим следующим образом:

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

Рассмотрим булево уравнение Здесь через 1 1,..., 11, 1 обозначено представление функции над 1,..., 11, 1 произвольной булевой формулой (как правило, для представления 1 используется некоторая нормальна форма — ДНФ, КНФ или АНФ). Через 1(1,...,1 )1 (1,...,, 1 ) обозначена булева формула, полученная заменой вхождений одной или нескольких (быть может, всех) формул 1 1,..., 11 в левой части (1.4) на вхождения литерала 1. Пе­ реход от уравнения (1.4) к уравнению (1.5) — это одна итерация преобразо­ ваний Цейтина в применении к булевым уравнениям.

Теорема 1.2 (см. [49]) Множество решений уравнения (1.4) пусто тогда и только тогда, когда пусто множество решений уравнения (1.5). Если эти множества не пусты, то существует взаимно однозначное соответствие меж­ ду ними. Переход от произвольного решения уравнения (1.5) к соответству­ ющему решению уравнения (1.4) осуществляется за линейное время.

Пример 1.4. В примере 1.3 было показано, что задача логического крип­ тоанализа генератора поточного шифрования А5/1 сводится к решению системы булевых уравнений вида (1.3). Тем не менее, вопрос о способе решения данной системы остается открытым. Например, для использо­ вания SAT-решателя требуется преобразовать систему к уравнению вида КНФ=1. Покажем, как это можно сделать при помощи преобразований Цейтина на примере одного уравнения из (1.3).

Рассмотрим уравнение Учтем, что Введем дополнительные булевы переменные 1, 2 и рассмотрим формулы Рассмотрим уравнение В соответствии со сказанным выше между множествами решений уравне­ ний (1.6) и (1.7) существует биекция. Формулы в скобках в левой части (1.7) можно представить в виде КНФ, используя таблицы истинности.

Поступим аналогичным образом со всеми уравнениями системы (1.3).

Все полученные КНФ объединим конъюнкцией. В результате имеем урав­ нение вида КНФ=1, между множеством решений которого и множеством решений системы (1.3) существует биекция.

1.3. Основные алгоритмы решения систем булевых Для решения систем булевых уравнений можно использовать целый ряд методов. Одним из первых булевы уравнения начал решать осново­ положник булевой алгебры Дж. Буль [58]. Используемый им подход осно­ вывался на процедурах «переразрешения» уравнения или системы посред­ ством выражения одних переменных через другие. Эти идеи развивались более 100 лет, и долгое время соответствующие методы (методы «булевой унификации») были доминирующими ([59–63]).

На сегодняшний день можно сделать вывод, что идеи булевой унифи­ кации малопригодны для решения уравнений, кодирующих аргументиро­ ванно трудные задачи обращения дискретных функций. Это связано, как правило, с существенным разрастанием формул при попытках явного вы­ ражения одних переменных (скажем, переменных входа рассматриваемой функции) через другие. Данный эффект хорошо заметен при переразреше­ нии систем, кодирующих криптографические алгоритмы (например, DES [64]).

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

Сведение произвольных систем булевых уравнений к системам поли­ номиальных уравнений над полем GF(2) с последующим их решени­ ем при помощи разнообразных модификаций алгоритма Бухбергера Методы, использующие идеи линеаризации (к последним относится, например, метод линеаризационного множества, предложенный и раз­ витый в работах [67–69]);

SAT-подход, в основе которого лежит техника перехода от произволь­ ной системы булевых уравнений к одному уравнению вида КНФ=1 с сохранениям ряда свойств (преобразования Цейтина) [1, 44, 70, 71];

Подход, использующий в своей основе двоичные диаграммы решений (Binary Decision Diagrams, BDD, ROBDD), [72–74].

Наилучшие результаты при решении булевых уравнений, кодирующих аргументированно трудные задачи обращения дискретных функций, на данный демонстрирует SAT-подход, использующий решатели, базирующи­ еся на алгоритме DPLL ([16, 75–78]).

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

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

Как известно, многие NP-трудные задачи возникли из совершенно кон­ кретных практических постановок. В ряде направлений без умения решать данные задачи невозможно обойтись. Речь идет о проблемах синтеза и вери­ фикации дискретных управляющих/управляемых систем, проблемах эко­ номики, производственного планирования, логистики и многих других. В этих областях вопросы построения практически эффективных алгоритмов решения соответствующих комбинаторных задач чрезвычайно актуальны.

Большое число исследований посвящено построению приближенных алго­ ритмов решения NP-трудных проблем. Однако в некоторых приложениях, например, в задачах верификации микросхем приближенные алгоритмы (даже обладающие малой погрешностью) совершенно бесполезны, а необ­ ходимость поиска точных решений существенно сужает класс методов — методы непрерывной математики, генетические алгоритмы, разнообразные «эволюционные эвристики» в общем случае не дают точных решений.

С другой стороны, проблематика решения булевых уравнений (особен­ но в форме SAT-задач) демонстрирует в последние годы впечатляющий алгоритмический прогресс. Современные алгоритмы решения SAT-задач можно воспринимать как эффективные вычислительные методы, приме­ нимые к решению задач из различных областей кибернетики. Сказанное означает, что автоматизированная система, позволяющая сводить к буле­ вым уравнениям проблемы исследования различных дискретных систем, является практически востребованной.

Как уже отмечалось, в противовес потоку статей по алгоритмам поис­ ка решений булевых уравнений, работ, посвященных методам сведения к булевым уравнениям комбинаторных проблем, относительно немного. Хо­ рошим введением в эту проблематику является обзор [1]. В [11], [79], [5] и некоторых других работах рассматривались процедуры построения КНФ, кодирующих различные комбинаторные «игровые» задачи (задача о фер­ зях, задача о Ханойской башне и др.). Механизмы преобразования в булевы уравнений задач планирования и составления расписаний были описаны в статьях [80–82]. Ряд работ посвящен использованию «SAT-технологий» в общей задаче удовлетворения ограничений (CSP) [83–87]. В статьях [8–10] аппарат булевых уравнений применяется к планированию вычислений в распределенных средах.

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

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

Решить проблему преобразования в булевы уравнения алгоритмиче­ ских описаний дискретных функций в принципе возможно при помощи современных систем описания аппаратуры [88, 89]. Однако эти системы ориентированы на задачи проектирования аппаратных реализаций алго­ ритмов. Поэтому при программировании на данных языках приходится учитывать многочисленные нюансы, обусловленные особенностями реали­ зации рассматриваемого алгоритма в аппаратной архитектуре. Так, язык VHDL основан на параллельной многопроцессорной модели. Нижний уро­ вень модели образует архитектура виртуального процессорного элемента (ВПЭ), а верхний уровень — множество ВПЭ, объединенных некоторой си­ стемой межпроцессорных связей.

Структура ВПЭ состоит из АЛУ (арифметико-логическое устройство), ОЗУ (оперативное запоминающее устройство) данных, ОЗУ программы, источников сигналов (входы) и приемников сигналов (выходы). АЛУ вы­ полняет элементарные операции над данными (дискретные преобразова­ ния). В ОЗУ программ хранится программа в виде последовательности операторов. Операторы, включая условные операторы, выполняются по­ следовательно друг за другом, как в обычных языках программирования.

Такая программа в VHDL-программе называется процессом — ВПЭ выпол­ няет его как отдельный вычислительный процесс.

Таким образом, задача описания алгоритма вычисления дискретной функции на языке VHDL превращается в задачу описания взаимодействий между перечисленными выше элементами многопроцессорной модели с пе­ речисленными ниже особенностями:

1. все процессы исполняются параллельно;

2. необходимо учитывать временные задержки в распространении сиг­ налов между ВПЭ;

3. работа процессов должна быть синхронизирована.

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

Основные выводы по первой главе. В данной главе обоснована ак­ туальность проблемы преобразования процедурных описаний дискретных функций в булевы уравнения. На основе формальных вычислительных мо­ делей (RAM) сформулированы базовые принципы методологии пропозици­ онального кодирования алгоритмов. Все эти принципы допускают перенос на современные вычислительные архитектуры и современные средства про­ граммирования.

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

Преобразование процедурных описаний дискретных функций в булевы уравнения Далее мы развиваем общую технику преобразования в булевы уравне­ ния программ вычисления дискретных функций, написанных на специаль­ ном высокоуровневом языке. Получаемая система булевых уравнений яв­ ляется результатом применения к рассматриваемой программе пошаговой интерпретации специального вида. Фактически речь идет о символьном ис­ полнении программы (symbolic execution, [90–93]) — технике, используемой в статическом анализе программ [94, 95]. Мы позволим себе привести цита­ ту из статьи [90], которая является одной из первых работ по символьному исполнению программ.

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

При символьном исполнении семантика основных операторов языка рас­ ширена таким образом, чтобы принимать на входе символы и выдавать на выходе формулы.

Особо отметим, что процесс пропозиционального кодирования алго­ ритмов в том смысле, как он описан в первой главе, представляет собой специальный случай символьного исполнения программ. Действительно, при пропозициональном кодировании результатом интерпретации каждой инструкции программы является формула исчисления высказываний и бу­ лево уравнение вполне конкретного вида. Особенность пропозиционально­ го кодирования заключается в том, что обе ветви произвольного оператора условного перехода могут быть эффективно преобразованы в одну форму­ лу. В этом основное отличие от ранних работ по символьному исполнению программ (см. [90]), в которых каждая ветвь условного оператора интер­ претируется отдельной формулой.

Далее представлен проблемно-ориентированный процедурный язык (язык ТА) (см. [96]), обладающий операционной семантикой (см. [13]). Про­ граммы на данном языке (ТА-программы) представляют собой алгоритми­ ческие описания дискретных функций. При интерпретации произвольной ТА-программы происходит ее символьное исполнение, результатом которо­ го является система булевых уравнений ( ). Подстановка в ( ) некото­ рого дает систему ( ), из произвольного решения которой можно эффективно выделить такое слово {0, 1}, что () =. Для поиска решений систем вида ( ) можно использовать современные бу­ левы решатели.

2.1. Описание проблемно-ориентированного языка ТА Язык ТА представляет собой процедурный язык описания алгорит­ мов с блочной структурой и С-подобным синтаксисом (стандарт ISO/IEC 9899:1999). Вся терминология, применяемая далее при описании языка TA, является стандартной и может быть найдена в любом из общедоступных источников по теории программирования и компиляции (например, см.

[97–99]). Особо отметим, что некоторые конструкции языка ТА совпада­ ют с их прототипами в языке С [100]. Далее приводится описание всех основных конструкций языка ТА с использованием нотации Бэкуса-Наура (БНФ).

В таблице 2.1 приведены лексемы (терминальные символы граммати­ ки) языка программирования ТА. Терминальные символы могут разделять­ ся произвольным количеством «пустых» символов. К пустым символам от­ носятся пробелы, переносы строк, табуляция.

Ключевые слова _in, _out, _mem, define, void, int, bool, bit, if, else, Идентификаторы Целочисленные константы Разделители