ИСТИНА

Цель НИР состоит в проведении исследований и получении решения серии актуальных задач, связанных с синтезом, анализом и тестированием дискретных управляющих систем, с передачей информации о дискретных функциях, а также с эквивалентностью, оптимизацией и верификацией автоматных вычислительных моделей.

Discrete control systems are traditionallly studied in discrete mathematics and mathematical cybernetics. Either new trends (obtaining of high-precise asymptotical bounds) or classical branches (the development of methods and algorithms of analysis, testing, and optimization of some control system models like VLSI models) are very perspective. The theotetical results in this field are applicable to some practic problems like nano-level VLSI design, design of distributed informational systems. All these facts permit to conclude the usefullness of theoretical investigations and applications of obtained results in the fields of VLSI design in the frames of the suggested theme.

1. Получение асимптотических оценок, имеющих, как правило, высокую степень точности, для сложности "типичных" или "самых сложных" функций в некоторых классах схем. На базе различных вариантов предложенного С. А. Ложкиным метода асимптотических оценок высокой степени точности (АОВСТ) будет продолжено создание оригинальных эффективных методов реализации "типичных" и самых "сложных" функций в ряде моделей дискретных управляющих систем, обладающих определенными специальными метрическими, структурными или функциональными свойствами. С помощью этих методов для сложности данных функций в рассматриваемых классах схем будут получены асимптотические оценки, имеющие, как правило, высокую степень точности. Так, будет продолжено исследование на уровне АОВСТ сложности реализации указанных функций в ряде классов схем проводящего и предикатного типов, классов формул и схем из функциональных элементов (СФЭ) с некоторыми структурными ограничениями, а также исследование возможности их реализации схемами, оптимальными по нескольким критериям сложности. 2. Разработка методов синтеза схем в некоторых моделях, связанных с логическим проектированием дискретных устройств преобразования информации и, в частности, СБИС. На основе метода АОВСТ и других методов будет продолжено исследование модели задержки СФЭ, в которой задержка переключения выхода элемента зависит от ряда факторов, связанных как с самим элементом, так и с примыкающими к нему элементами. В рамках данной модели будет установлено асимптотическое поведение функции Шеннона для задержки СФЭ в различных базисах, а также получены близкие к АОВСТ оценки этой функции. Будет продолжена разработка методов синтеза схем, оптимальных по так называемой статической или динамической активности, которые являются моделями энергопотребления СБИС. Будут разработаны методы синтеза, позволяющие получать асимптотически оптимальные по сложности схемы, динамическая активность которых оптимальна по порядку, а также методы исследования «индивидуальной» активности. 3. Разработка методов "вложения" ("геометрической" реализации) схем в некоторые регулярные структуры, связанные, в частности, с топологическим синтезом СБИС. Будут развиты и исследованы модели "вложения" схем в плоские прямоугольные решетки – т. н. "клеточные" схемы, единичные кубы и другие структуры. При этом будут рассмотрены различные модификации клеточных схем, моделирующие те или иные особенности структуры СБИС наноуровня. Будут созданы новые эффективные методы построения оптимальных вложений указанного вида как для "типичных" или "самых сложных" функций, так и для функций, встречающихся в приложениях. 4. Исследование индивидуальной сложности и структуры оптимальных схем для ряда "специальных" функций. Будут развиты методы синтеза и исследована структура оптимальных схем для некоторых функций, связанных с выполнением арифметических и логических операций (симметрические функции, счетчики четности, дешифраторы, мультиплексоры и др.). При этом будет продолжено исследование глубины и сложности некоторых из указанных функций на уровне АОВСТ. Будет продолжено изучение влияния ряда структурных ограничений, а также степени самокоррекции на сложность реализации некоторых специальных функций. 5. Построение и анализ тестов для различных задач контроля в некоторых классах схем. Будет продолжено изучение близких к оптимальным тестов в ряде задач контроля для схем из функциональных элементов и контактных схем, а также при неисправностях различных типов на входах схем; будет установлено или уточнено поведение соответствующих функций Шеннона длины теста. 6. Получение простых представлений, оценок на минимальный размер области определения и сложность получения универсальных функций. Универсальная функция возникает естественным образом как порождающая частью своих значений любую соответствующую априорной ложной информации функцию. Будет решена задача представимости универсальных функций для класса линейных функций полиномами, в том числе над полями Галуа. Будут найдены быстрые алгоритмы для построения универсальных функций с малой областью определения. Будут установлены общие свойства задачи нахождения универсальных функций как тестовой задачи, представленной в матричном виде. 7. Исследование ряда фундаментальных проблем программирования, таких как проблемы эквивалентности, оптимизации и верификации автоматных вычислительных моделей. Будет продолжена разработка эффективных алгоритмов проверки эквивалентности программ в автоматных моделях, семантика которых основана на полугруппах, порождающихся операторами программ. Предполагаются улучшение существующих алгоритмов проверки эквивалентности для моделей линейных и металинейных унарных рекурсивных программ и разработка эффективных алгоритмов проверки эквивалентности для металинейных унарных рекурсивных программ в семантиках, порождающихся операторами программ, а также исследование смежных проблем.

Участники проекта имеют большой набор методов и результатов, связанных с разработкой методов синтеза и получением асимптотических оценок высокой и близкой к ней степени точности как для различных функций Шеннона, так и для некоторых специальных ФАЛ. Основным методом, с помощью которого планируется получать новые результаты, является метод асимптотических оценок высокой степени точности (АОВСТ) и его модификации. В недавних работах были получены следующие результаты. Поведение функции Шеннона на уровне АОВСТ установлено для сложности BDD, где «вес» «слившихся» вершин больше, чем «вес» остальных, и для сложности формул стандартного базиса с ограниченной глубиной альтернирования, соответственно. Поведение функции Шеннона для задержки СФЭ в некоторых содержательных моделях установлено на уровне АОВСТ и на уровне близких к ним оценок. В направлении, связанном с тестированием схем, участники проекта имеют опыт в получении рекордных оценок функций Шеннона длин тестов при неисправностях элементов в схемах и при неисправностях на входах схем. В направлении, связанном с теоретическим программированием, участниками темы разработаны общие методы построения эффективных алгоритмов распознавания эквивалентности программ, теория аппроксимации отношения эквивалентности для моделей программ, методы верификации моделей распределённых программ и формул темпоральных логик, методы маскировки программ.

Разработан метод синтеза, с помощью которого получены асимптотически точные оценки функции Шеннона для площади клеточных схем ограниченной высоты с кратными входами из функциональных и коммутационных элементов, расположенными на горизонтальном разрезе схемы. Получены новые более точные оценки для сложности мультиплексорной функции в классе схем из функциональных элементов в стандартном базисе. Установлено точное значение $n+2$ глубины в стандартном базисе мультиплексорной функции с $n$, $n\ge 2$, адресными переменными при всех значениях $n$, отличных от 8 и 9. Построена контактная схема, реализующая мультиплексорную функцию, асимптотически оптимальная по сложности и сохраняющая порядок роста статической и динамической активности. Построена контактная схема, реализующая дешифратор, асимптотически оптимальная по сложности и сохраняющая порядок роста статической и динамической активности. Получено точное значение функции Шеннона длины диагностического теста относительно прибавления по модулю 2 одной переменной к остальным переменным, а также установлена линейность по числу переменных порядка роста функции Шеннона длины проверяющего теста относительно прибавления по модулю 2 одной переменной к остальным переменным. Установлены точные значения функции Шеннона длины единичного проверяющего теста относительно произвольных константных неисправностей на выходах элементов в формулах над одним базисом жегалкинского типа. Получены новые верхние оценки функций Шеннона длин единичных тестов относительно отождествлений входов функциональных элементов в СФЭ над некоторыми базисами. Обоснован критерий существования универсальных полиномов для классов линейных функций в зависимости от значности и количества переменных. Доказана универсальность произведения для классов линейных функций над полем Галуа. Результаты, полученные в прошлом году и касающиеся проверки эквивалентности линейных унарных рекурсивных программ, опубликованы в сборнике трудов конференции. Разработаны эффективные алгоритмы проверки эквивалентности для модели программ, совмещающей синтаксис дискретных преобразователей Глушкова–Летичевского и семантику пропозициональных программ Захарова, для некоторых полугрупп, задающих семантику программ. Разработаны основные принципы построения архитектуры программной системы автоматизации рассуждения, основанной на предложенном Н.П. Брусенцовым алгебраического методе анализа логических взаимосвязей, выработаны критерии ее эффективности. Произведена подготовка к программной реализации системы. Исследованы некоторые особенности симметричных систем остаточных классов.