Построение с использованием SAT-решателей схем, маскирующих логические неисправности и вредоносные подсхемы управляющих компонент сложных физических систем | Известия вузов. Физика. 2020. № 12. DOI: 10.17223/00213411/63/12/114

Построение с использованием SAT-решателей схем, маскирующих логические неисправности и вредоносные подсхемы управляющих компонент сложных физических систем

С целью повышения надежности управляющих компонент сложных физических систем рассматривается проблема маскирования неисправностей и вредоносных подсхем, обнаруживаемых на заключительных этапах создания этих компонент. Управляющие компоненты, как правило, являются логическими схемами, комбинационными или последовательностными. Комбинационная схема С (комбинационная часть последовательностной схемы) состоит из вентилей. В ней выделена подсхема с множеством V выходных полюсов и множеством U входных полюсов. Множество V состоит из выходных полюсов неисправных элементов схемы С и входных полюсов ее исправных элементов. Предлагается корректировать поведение схемы С , используя маскирующую схему, по возможности, более простую. Eе входы соединяются с полюсами из U , а выходы - либо с полюсами, питаемыми полюсами из V (выходными полюсами элементов схемы С ), либо непосредственно с полюсами из V (входными полюсами элементов схемы С ) в рамках Engineering Change Order (ECO) технологий. В отличие от известных подходов к построению маскирующей схемы, основанных на результатах моделирования корректируемой схемы С , обеспечивающих в результате маскирования корректное поведение схемы на множестве моделируемых наборов, предлагается использовать частичные функции полюсов множества V . Применение частичных функций при построении маскирующей схемы позволяет гарантировать корректное поведение схемы С на множестве всех ее входных наборов. Построение частичных функций выполняется с использованием SAT-решателей. По полученной системе частичных функций с помощью систем ESPRESSO и ABC строится маскирующая схема.

Using SAT-solvers for deriving patch circuits that mask nodes faults and trojan circuits injections.pdf Введение Работоспособность сложных физических систем зависит от надежности составляющих их компонент, в частности, от надежности управляющих компонент, которые, как правило, являются логическими схемами высокой производительности. Высокая производительность - это высокая скорость выполнения операций и высокий уровень интеграции. Последний фактор приводит к большой сложности логических схем в условиях относительно малого числа полюсов, на которых можно наблюдать поведение схемы. В связи с этим в логических схемах возможно обнаружение неисправностей на поздних стадиях производства. В таких случаях приходится либо возвращать схемы на более ранние стадии, либо выбрасывать их как непригодные к использованию. Подобные ситуации снижают выход годных схем, что весьма нежелательно. Кроме того, в схемы, изготовленные сторонними фирмами, могут быть внедрены вредоносные подсхемы (Trojan Circuits (TCs)) с целью разрушения системы или извлечения конфиденциальной информации. Срабатывание вредоносной подсхемы (TC) также может рассматриваться как проявление логической неисправности на полюсе, являющемся выходом линии связи, к которой присоединен выход (payload) вредоносной подсхемы. Речь идет о широком классе вредоносных подсхем, у которых выход активирующего блока включается в линию логической схемы. (Структура TC и способ подключения ее входов в схему C значения не имеют.) В связи со сказанным, в дальнейшем будем говорить только о коррекции неисправных полюсов. Для коррекции схем в случае обнаружения неисправностей применяются ECO (Engineering Change Order)-технологии [1-3]. В рамках этих технологий неисправности в изготавливаемой схеме можно, в частности, маскировать с помощью корректирующей (маскирующей) схемы, подключаемой к внутренним полюсам корректируемой схемы. Часть из этих внутренних полюсов подключается к выходам маскирующей схемы, остальные - к входным полюсам маскирующей схемы. Для маскирующей схемы на кристалле отводится дополнительная площадь. Маскирующая схема, по возможности, минимизируется с целью сокращения используемой дополнительной площади. Существующие подходы к маскированию основаны на использовании входных наборов корректируемой схемы, на которых в результате моделирования на некоторых полюсах обнаружено несовпадение результатов моделирования с ожидаемыми корректными значениями. Такая информация для сложных логических схем с несколькими десятками входов, как правило, оказывается неполной, а корректное поведение схемы гарантируется только на моделируемом множестве входных наборов. В предлагаемом нами подходе коррекция гарантирована на всем множестве входных наборов корректируемой схемы, причем достаточно обнаружить искажение поведения полюса хотя бы на одном входном наборе корректируемой схемы. Будем иметь в виду, что каждому внутреннему полюсу комбинационной схемы С соответствует частично определенная булева функция [4], зависящая от входных переменных этой схемы. При проявлении неисправности, а также при активации вредоносной подсхемы происходит искажение этой функции. В работе [5] корректное функционирование корректируемой схемы С в условиях доступности множеств V, U ее внутренних полюсов достигается отображением 225166028812516633601 частичных функций полюсов из V от входных переменных схемы С на множество U полюсов с последующей реализацией полученного отображения в виде логической схемы. Такая коррекция была нами разработана в условиях применения операций над ROBDD-графами [5]. Однако ROBDD-графы могут быть построены не для всяких корректируемых логических схем. Дело в том, что для некоторых схем количество внутренних вершин ROBDD-графа растет экспоненциально по отношению к числу переменных графа (числу входов корректируемой схемы) независимо от выбора порядка разложения по переменным, что исключает возможность использования ROBDD-графов, если число входов таких схем достигает нескольких десятков. В данной работе предлагается альтернативный подход, основанный на определении выполнимости соответствующих схемам булевых формул, записанных в конъюнктивной нормальной форме (КНФ). Для каждого из неисправных полюсов строятся две логические схемы, представляющие множества единичных и нулевых наборов соответствующей ему частичной функции от входных переменных схемы. Затем для получения КНФ к этим схемам применяется преобразование Цейтина [6]. Построенные КНФ, будем называть их в дальнейшем КНФ Цейтина, содержат входные и внутренние переменные, сопоставляемые элементам схемы С, а их длина линейно зависит от числа элементов схем, порождающих эти КНФ. С помощью SAT-решателя из КНФ Цейтина извлекаются множества единичных и нулевых наборов частичной функции полюса. Множества представляются в виде дизъюнктивных нормальных форм (ДНФ) в пространстве входных переменных схемы. Для них находится отображение на множество U внутренних переменных схемы также с использованием SAT-решателя. Затем по полученному отображению строится маскирующая схема. Заметим, что SAT-решатели становятся все более эффективными. Их использование позволяет продвигаться в область маскирования неисправностей все более сложных логических схем. Цель работы - обеспечение надежности функционирования логических управляющих устройств на всем множестве их входных наборов за счет использования маскирующей схемы, требующей меньшей, чем при дублировании, площади кристалла. Рассматриваются устройства, поведение которых не может быть представлено ROBDD-графами из-за гигантских размеров последних. 1. Постановка задачи Задана комбинационная логическая схема С (комбинационный эквивалент схемы с памятью), построенная из вентилей AND, OR, NAND, NOR, NOT, XOR, в которой выделена подсхема с множеством V выходных полюсов и множеством U входных полюсов. Множество V состоит из выходных полюсов неисправных элементов схемы С (рассматриваются логические неисправности) и входных полюсов ее исправных элементов, таких, что полюс является выходом линии, в которую включена вредоносная подсхема. Конкретный выбор множества U зависит от технической реализации схемы C на кристалле и здесь не обсуждается [3]. Необходимо корректировать поведение схемы С, используя маскирующую схему, желательно более простую, чем заданная подсхема, используя SAT-решатели. В работе [5] показано, что получение более простых маскирующих схем, основанное на применении операций над ROBDD-графами, возможно, в частности, когда неисправные полюсы удалены как от входов, так и от выходов корректируемой схемы. Именно в таких полюсах соответствующие частичные функции оказываются, как правило, слабо определенными, а неисправности, сопоставляемые этим полюсам, - трудно обнаружимыми. Такие неисправности зачастую удается локализовать лишь на последних этапах создания схемы. Заметим также, что вредоносные подсхемы (TCs) обычно включаются в линии, константные неисправности которых трудно обнаружить. 2. Необходимые понятия и общий подход к решению задачи Обозначим через fv частичную функцию, сопоставляемую полюсу v схемы C, зависящую от входных переменных схемы. Пусть M1(fv) - множество единичных наборов этой функции, а M0(fv) - множество ее нулевых наборов. Рассмотрим частичную булеву функцию f1 и полностью определенную булеву функцию f2, зависящие от одного и того же множества переменных и заданные множествами их единичных и нулевых наборов: M1(f1), M0(f1); M1(f2), M0(f2). Определение. Полностью определенная функция f2 является реализацией частичной функции f1, если и . Это значит, что и . В работе [5] предложен алгоритм нахождения множеств единичных и нулевых наборов частичной функции полюса v от входных переменных схемы С на основе построения функции наблюдаемости этого полюса с применением операций над ROBDD-графами, извлекаемыми из комбинационной схемы С. Как уже отмечалось выше, не для всех схем и их фрагментов можно построить ROBDD-графы. В этой ситуации в данной работе предлагается находить представление множества единичных и нулевых наборов частичной функции в виде двух ортогональных ДНФ, используя SAT-решатели, а если необходимо, то дополнительно и операции над ROBDD-графами. Частичная функция полюса затем отображается на множество U внутренних полюсов схемы С также с использованием SAT-решателей, по полученным множествам в пространстве U переменных строится соответствующая маскирующая схема, являющаяся реализацией частичной функции, представленной этими множествами. Рассмотрим функцию , реализуемую на i-м выходе схемы С, в предположении, что переменная v является входной наряду с переменными . Эта функция представляется подсхемой схемы C, получаемой при движении от i-го выхода к входам схемы С и подстановке функций от входных переменных соответствующих вентилей вместо внутренних переменных (кроме переменной v) схемы С пока это возможно. Выход полученной подсхемы есть i-й выход схемы C, а полюс v является ее входом наряду с входами схемы С. Представим булеву разность Dv fi функции fi по переменной v: . (1) Здесь , . Заметим, что булева разность Dv fi задает также функцию наблюдаемости полюса v на i-м выходе схемы C. Действительно, функция Dv fi принимает единичное значение на всяком наборе значений переменных , при подстановке которого в схему C изменение значения перемен¬ной v приводит к изменению значения i-го выхода схемы C. Функция наблюдаемости полюса v для схемы C в целом представляется выражением , (2) где mv - число выходов схемы C, связанных с полюсом v. Для полюса v схемы C рассмотрим функцию , представляемую подсхемой Cv схемы C. Выходом подсхемы Cv является полюс v, а ее входами - входы схемы C. Представим множество M1(fv) единичных наборов частичной функции fv, которое в то же время является множеством всех тестовых наборов для константной неисправности 0 на полюсе v, выражением , (3) а множество M0(fv) нулевых наборов частичной функции fv, которое, в свою очередь, является множеством всех тестовых наборов для константной неисправности 1 на полюсе v, выражением . (4) Напомним, что конъюнкции ортогональны, если они содержат взаимно инверсные литеры. Под литерой здесь и далее будем понимать переменную вместе с ее знаком инверсии. ДНФ ортогональна, если ее конъюнкции попарно ортогональны. Опишем более детально общий подход к решению поставленной выше задачи. 1. Представляем формулы (3), (4) двумя логическими схемами. 2. Упрощаем эти схемы с тем, чтобы сократить число внутренних переменных в соответствующих схемам КНФ Цейтина. 3. Строим КНФ для упрощенных схем методом Цейтина. Эти КНФ представляют множества единичных и нулевых наборов частичной функции fv полюса v. 4. Используя SAT-решатель из имеющихся КНФ Цейтина, получаем представление множеств единичных и нулевых наборов частичной функции fv в виде двух ортогональных ДНФ на множестве входных переменных схемы С. 5. Находим отображение частичной функции fv на множество U внутренних переменных схемы С, представляя отображение также в виде двух ДНФ. Внутренние переменные в то же время являются внутренними переменными подсхемы Cv. Множество переменных выбирается из различных соображений, учитывающих техническую реализацию схемы С [3]. При этом подсхема с выходным полюсом v и входами вместе с подсхемами, имеющими в качестве выходов полюсы и входы , образуют подсхему Cv. Обозначим символом частичную функцию полюса v в пространстве переменных . Заметим, что подсхема с выходом v и входами является реализацией частичной функции . Наша цель - найти, по возможности, более простую реализацию и затем использовать ее в качестве маскирующей схемы. В работе [5] показано, что маскирующая схема может быть в несколько раз проще, чем упомянутая выше реализация. Будем иметь в виду, что множество , как правило, невелико, и его мощность достигает одного-двух десятков, в то время как число входных переменных схемы С может достигать многих десятков. 6. С помощью системы ESPRESSO [7] из полученной частичной функции извлекаем безызбыточную ДНФ, ее реализующую. 7. С помощью системы АВС [8] по безызбыточной ДНФ в пространстве переменных получаем маскирующую схему. Будем иметь в виду, что при построении по схеме КНФ методом Цейтина следует использовать различные внутренние переменные для различных подсхем схемы С, даже если подсхемы реализуют взаимно инверсные функции. При неисправности множества V полюсов, , необходимо получить безызбыточную систему ДНФ для полюсов множества V в пространстве переменных . Остановимся на детальном описании некоторых из перечисленных шагов. 3. Упрощение схемы, представляющей булеву разность Dv fi Выполним упрощение схемы, представляющей булеву разность , отыскивая в ней одинаковые подсхемы, с целью упрощения соответствующей схеме КНФ. Рис. 1. Схема, реализующая булеву разность Dv fi Булева разность Dv fi может быть представлена схемой рис. 1. Здесь схема реализует функцию , а схема реализует функцию . В этих схемах могут найтись одинаковые подсхемы, которые не зависят от переменной v. Это значит, что в схеме можно оставлять одну из одинаковых подсхем такого типа. Алгоритм упрощения схемы, представляющей булеву разность Dvfi Извлекаем подсхему из схемы C. 1. Включаем в подсхему все вентили между полюсом v и i-м выходом схемы C вместе с линиями, их соединяющими. В полученной подсхеме имеется один выход, совпадающий с i-м выходом схемы C, а ее входами являются свободные входы вентилей, вошедших в подсхему, и полюс v. 2. Разделим входы схемы на s подмножеств. Каждый вход j-го подмножества связан с одним и тем же внутренним полюсом wj схемы C. 3. Формируем множество таких полюсов. Они питают вентили, имеющие входы, связанные с полюсом v. Будем рассматривать полюсы в качестве входов подсхемы Cv (out). 4. Подсхема порождает две подсхемы: и при фиксировании полюса v константами 1, 0 соответственно. Рис. 2. Упрощенная схема, представляющая булеву разность Dvfi Рис. 3. Схема C Далее формируем подсхему схемы из схемы C с выходами , включая полюс v, если это необходимо, и входами . Формируем упрощенный фрагмент схемы рис. 1 (рис. 2). Проиллюстрируем алгоритм упрощения булевой разности на примере. Рис. 3 представляет схему C, ее выделенный полюс обозначен символом v. Схемы и две схемы , представлены на рис. 4, a, б и в соответственно. Схема Cv(in) показана на рис. 5. Схема, реализующая булеву разность Dv fi (без упрощения) представлена на рис. 6. Рис. 4. Схемы: a - ; б - ; в - Рис. 5. Схема Cv(in) Рис. 6. Схема, реализующая булеву разность Dv fi без упрощения с дополнительным выходом v Упрощенная схема, представляющая булеву разность Dv fi, показана на рис. 7. Рис. 7. Упрощенная схема, представляющая булеву разность Dv fi c дополнительным выходом v Формула (5) представляет КНФ для булевой разности без упрощения, а формула (6) - с упрощением. Формулы получены методом Цейтина. С этой целью для каждого вентиля схем (рис. 5 и 6) предварительно построены следующие КНФ: (5) (6) Рис. 8. Представление функции наблюдаемости для многовыходной схемы C В результате упрощения удалось сократить КНФ на 36 символов, т.е. почти в 2 раза, а число внутренних переменных - на 3. Проведенные нами эксперименты на контрольных примерах из базы ISCAS показали, что, как правило, число внутренних переменных удается сократить на 30 % и более. Напомним, что булева разность Dv fi для одного выхода схемы C есть функция наблюдаемости полюса v на этом выходе. Для схемы в целом функция наблюдаемости представляется схемой на рис. 8. 4. Представление частичной функции внутреннего полюса в виде двух схем и извлечение из них ортогональных ДНФ Представив в виде схемы функцию наблюдаемости для многовыходной схемы C, мы можем получить схемы, задающие множества единичных и нулевых наборов частичной функции полюса v, показанные на рис. 9, а и б соответственно. Полюс v используется как дополнительный выход. Рис. 9. Схемы, представляющие множество: единичных наборов частичной функции полюса v (a) и нулевых наборов частичной функции полюса v (б) По схемам, представляющим множества единичных и нулевых наборов частичной функции, формируются КНФ Цейтина: КНФ1 и КНФ0. Далее с помощью SAT-решателей получаем из этих КНФ ортогональные ДНФ. Извлечение ОДНФ из КНФ Цейтина 1. Для КНФ1 (КНФ0) находим набор, обращающий эту КНФ в единицу, используя SAT-решатель. Если такого набора не существует, переходим к п. 4 алгоритма. В найденном наборе выделяем его часть, представленную входными переменными схемы С. 2. Расширяем этот набор, последовательно удаляя входные переменные, насколько это возможно, получая в результате конъюнкцию от входных переменных. При удалении каждой переменной обращаемся к SAT-решателю с целью проверки, является ли соответствующая конъюнкция импликантой функции, представленной рассматриваемой КНФ. (Алгоритм проверки будет описан далее.) Если это первый из найденных наборов, то расширение происходит в области единичных значений исходной КНФ. Иначе расширяем этот набор в оставшейся от исходной КНФ области единичных значений, полученной исключением из исходной области уже найденных конъюнкций. Конъюнкция исключается путем добавления ее инверсии (клаузы) к имеющейся КНФ. 3. Очередная полученная конъюнкция включается в формируемую ортогональную ДНФ (ОДНФ). Переходим к п. 1 алгоритма, рассматривая оставшуюся КНФ. 4. Работа алгоритма закончена. Применив предложенный алгоритм к КНФ1 и КНФ0, получим представление частичной функции fv в виде двух ОДНФ на множестве входных переменных схемы С: , соответственно. Предварительные эксперименты показали, что извлечение ОДНФ с помощью SAT-решателя происходит для некоторых схем существенно дольше, чем извлечение безызбыточной ДНФ методом, предложенным в [9]. В этом случае можно сначала получить безызбыточную ДНФ, потом на ее основе построить ROBDD-граф и уже из этого графа извлекать ОДНФ. Поскольку рассматриваются неисправные полюсы, характеризующиеся, как правило, слабо определенными частичными функциями, то безызбыточные ДНФ, их представляющие, могут быть заданы ROBDD-гра¬фами. Иными словами, в этих ситуациях могут быть совместно применены ROBDD и SAT-техно¬логии. Необходимо далее найти отображение множеств единичных и нулевых наборов частичной функции, представленных двумя ОДНФ, на внутренние переменные множества U, т.е. найти множества единичных и нулевых наборов частичной функции полюса v схемы С на заданном подмножестве внутренних переменных этой схемы. Для корректируемых схем большого (возможно, многих десятков) числа входных переменных нельзя воспользоваться двоичным моделированием с целью получения такого отображения. Поэтому предлагается специальная процедура, основанная на использовании сочетания троичного моделирования с двоичным моделированием и применении SAT-решателя. 5. Отображение частичной функции от входных переменных схемы С на множество ее внутренних переменных Сначала к троичным векторам, представляющим конъюнкции ДНФ , , применяется точное троичное моделирование [10], позволяющее получить области, содержащие единичные и нулевые наборы частичной функции . Эта функция, как правило, зависит от небольшого числа переменных (в пределах одного-двух десятков). Затем используется двоичное моделирование на подсхеме с целью выделения двоичных векторов, относящихся к области единичных и нулевых наборов этой подсхемы. Далее с помощью SAT-решателя выполняется проверка каждого выделенного набора на его достижимость в процессе функционирования схемы С. Достижимые наборы (булевы векторы) включаются в соответствующие им области единичных (нулевых) наборов частичной функции . Под точным троичным моделированием [10] одновыходной логической схемы будем понимать моделирование, приводящее к следующим результатам. Результатом точного троичного моделирования некоторой схемы, обозначим ее , является значение 1 (0), если на всех булевых векторах, представляемых троичным вектором, результатом двоичного моделирования этой схемы является значение 1 (0). Это значит, что интервал, сопоставляемый троичному вектору, целиком содержится в области единичных (нулевых) наборов значений функции, представляемой схемой . Иначе, результатом троичного моделирования этой схемы является неопределенное значение «-». Известно, что непосредственная подстановка троичного вектора в логическую схему (традиционное троичное моделирование) может давать значение «-» в ситуации, когда соответствующий вектору интервал содержится в области единичных (нулевых) наборов значений переменных функции, представляемой схемой, что нежелательно. В работе [10] было предложено выполнять точное троичное моделирование с использованием операций над ROBDD-графами. Рис. 10. Схемы: a - ; б - В данной работе предлагается использовать для этой цели SAT-решатель с целью расширения класса схем, для которых маскирование оказывается возможным. Пусть Kα - конъюнкция, сопоставляемая троичному вектору α. Строим две схемы для получения по ним КНФ Цейтина. Схема рис. 10, a используется для проверки поглощаемости конъюнкции Kα областью единичных наборов значений входных переменных схемы , схема рис. 10, б - областью нулевых наборов значений переменных этой схемы. Обозначим полученные схемы , соответственно. Строим для них КНФ Цейтина: и . Здесь f - функция, реализуемая схемой на выходе ui. Алгоритм точного троичного моделирования по КНФ Цейтина 1. Находим выполняющий набор для . Если его не существует, то результатом троичного моделирования является значение 1. Иначе переходим к следующему пункту алгоритма. 2. Находим выполняющий набор для . Если его не существует, то результатом троичного моделирования является значение 0. Иначе результатом троичного моделирования является значение «-». Выполнив точное троичное моделирование для каждой из подсхем схемы с выходами и входами , получим троичный вектор β. Вектор β является результатом точного троичного моделирования вектора α для множества полюсов схемы С. Зная результаты точного троичного моделирования для конъюнкций (троичных векторов) ДНФ , , получим множества троичных векторов , , которые содержат булевы векторы, множества единичных и нулевых наборов искомой частичной функции . Получая значение «-» на троичном векторе β из множеств , , мы не знаем, на каких именно порождаемых им булевых векторах достигается значение 1, а на каких значение 0 и какие из порождаемых векторов достижимы на полюсах схемы С. Поэтому далее предлагается выполнить следующие процедуры. Воспользуемся двоичным моделированием, а именно для каждого троичного вектора из , ( ) формируем множество булевых векторов в пространстве переменных. Подставляем булев вектор γ в подсхему . Если подсхема обращается в 1 (0), формируем для вектора γ схему Cγ. Схема Cγ представляет перемножение функций одновыходных подсхем схемы С, соответствующих компонентам вектора γ и зависящих от входных переменных схемы С. Если компонента вектора γ принимает значение 0, выходной элемент подсхемы заменяется инверсным элементом. Входные переменные заменены константами из троичного вектора α, порождающего вектор β, а затем вектор γ. В случае выполнимости КНФ сопоставляемой схеме Cγ, вносим булев вектор γ в множество единичных наборов значений переменных частичной функции . Для множества неисправных полюсов получаем множества , для частичных функций каждого полюса vj из V. 6. Получение маскирующей схемы Получив множества , для частичных функций каждого полюса vj из V, применяем систему ESPRESSO [7] с целью представления реализации частичных функций в виде системы ДНФ, а затем используем эту систему ДНФ в ABC [8] комплексе для создания маскирующей схемы Cp. Полученная маскирующая схема своими входами связана с внутренними полюсами схемы C, а каждый ее выход соединяется с полюсами, питаемыми соответствующим неисправным полюсом схемы C (рис. 11). При маскировании вредоносной подсхемы, выход которой подключен к некоторой линии l схемы С, выход маскирующей схемы Cp соединяется с входом вентиля (одного), питаемого этой линией (рис. 12). Рис. 11. Подключение одновыходной маскирующей схемы для неисправного полюса v Рис. 12. Подключение одновыходной маскирующей схемы для маскирования TC Заключение С целью повышения надежности управляющих компонент сложных физических систем разработаны методы маскирования неисправностей полюсов компонент, вызванные как дефектами в процессе производства, так и возможными введениями в линии управляющего устройства вредоносных подсхем (Trojan Circuits). Проведенные предварительные эксперименты показали целесообразность применения изложенного подхода для получения, по возможности, более простых маскирующих схем к корректируемым схемам, для которых ROBDD-графы построить не удается. Поскольку SAT-технологии непрерывно и быстро совершенствуются, использование SAT-решателей, когда применение ROBDD-графов для коррекции логических схем невозможно, позволит продвинуться в применении предлагаемого подхода к более сложным схемам.

Ключевые слова

комбинационные схемы, частичные функции, функции наблюдаемости внутренних полюсов, конъюнктивная нормальная форма Цейтина, дизъюнктивные нормальные формы, ортогональные дизъюнктивные нормальные формы, SAT-решатели

Авторы

ФИООрганизацияДополнительноE-mail
Матросова Анжела ЮрьевнаНациональный исследовательский Томский государственный университетд.т.н., профессор, профессор каф. компьютерной безопасности ИПМКН НИ ТГУmau11@yandex.ru
Провкин Виктор АлексеевичНациональный исследовательский Томский государственный университетаспирант ИПМКН НИ ТГУprowkan@mail.ru
Тычинский Вячеслав ЗиновьевичНациональный исследовательский Томский государственный университетмагистр ИПМКН НИ ТГУtvz.041@gmail.com
Николаева Екатерина АлександровнаНациональный исследовательский Томский государственный университетк.т.н., доцент каф. компьютерной безопасности ИПМКН НИ ТГУnikolaeve-ea@yandex.ru
Гошин Геннадий ГеоргиевичТомский государственный университет систем управления и радиоэлектроникид.ф-м.н., профессор, профессор каф. сверхвысокочастотной и квантовой радиотехники ТУСУРаgoshingg@svch.tusur.ru
Всего: 5

Ссылки

Krishnavami S., Ren H., Modi N., and Puri R. // Proc. Asia and South Pacific Design Automation Conference. - 2009. - P. 789-796.
Cheng A.-C., Jiang H.-R. and Jou J.-Y. // Proc. DATE. - 2016.
Dao A.Q., Lee N.-Z., Chen L.-C., et al. // Proc. DAC. - 2018.
Матросова А.Ю., Останин С.А., Кириенко И.Е. // Изв. вузов. Физика. - 2014. - Т. 57. - № 6. С. 127-132.
Matrosova A., Provkin V., and Nikolaeva E. // Proc. IEEE East-West Design & Test Symposium (EWDTS), 13-16 September 2019. - Batumi: IEEE, 2019. - P. 416-419.
Цейтин Г.С. // Записки научных семинаров ЛОМИ АН СССР. - 1968. - Т. 8. - С. 234-259.
Logic Minimization Software (http://ramos.elo.utfsm.cl/~lsb/elo211/aplicaciones/aplicaciones/espresso/ESPRESSO Logic Minimization Software.htm).
ABC: A System for Sequential Synthesis and Verification (https://people.eecs.berkeley.edu/~alanmi/abc/).
Petkovska А., Mishchtnko A., Novo D., et al. // Advanced Logic Synthesis. - Springer, 2008. -P. 169-188.
Matrosova A., Goloubeva O., and Tsurikov S. // Proc. 6-th Biennal Conf. on Electronics and Microsystems Technology. - Tallinn, 1998. - P. 183-186.
 Построение с использованием SAT-решателей схем, маскирующих логические неисправности и вредоносные подсхемы управляющих компонент сложных физических систем | Известия вузов. Физика. 2020. № 12. DOI: 10.17223/00213411/63/12/114

Построение с использованием SAT-решателей схем, маскирующих логические неисправности и вредоносные подсхемы управляющих компонент сложных физических систем | Известия вузов. Физика. 2020. № 12. DOI: 10.17223/00213411/63/12/114