Проверка эквивалентности частично построенных комбинационных схем | Вестник Томского государственного университета. Управление, вычислительная техника и информатика. 2025. № 71. DOI: 10.17223/19988605/71/13

ГлавнаяАрхивПроверка эквивалентности частично построенных комбинационных схем | Вестник Томского государственного университета. Управление, вычислительная техника и информатика. 2025. № 71. DOI: 10.17223/19988605/71/13

Проверка эквивалентности частично построенных комбинационных схем

Предложен алгоритм проверки эквивалентности частично построенной схемы и ее спецификации. Алгоритм основан на использовании операций пересечения однокоренных ROBDD-графов многовыходных подсхем частично построенной схемы, зависящих как от входных и выходных переменных подсхем, так и только от их выходных переменных. Для обнаружения неисправности подсхемы разработан алгоритм поиска тестовых наборов от входных переменных схемы, содержащей подсхему. Рассматриваемый в данной работе подход позволяет отказаться от использования Quantified Boolean Function (QBF) решателей или их модификаций, требующих, как правило, более сложных вычислений, чем операции над ROBDD-графами. Вклад авторов: все авторы сделали эквивалентный вклад в подготовку публикации. Авторы заявляют об отсутствии конфликта интересов.

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

программное обеспечение, компьютерная томография, промышленная дефектоскопия, эвристический алгоритм, эталонный образец, многопоточная обработка

Авторы

ФИООрганизацияДополнительноE-mail
Матросова Анжела ЮрьевнаНациональный исследовательский Томский государственный университетпрофессор, доктор технических наук, профессор кафедры компьютерной безопасности Института прикладной математики и компьютерных наукmau11@yandex.ru
Савенкова Марина МаксимовнаНациональный исследовательский Томский государственный университетмагистрант кафедры компьютерной безопасности Института прикладной математики и компьютерных наукmarina1412_11@mail.ru
Всего: 2

Ссылки

Матросова А.Ю., Савенкова М.М., Провкин В.А., Сухорученко К.А. Тестирование многовыходных схем // Вестник Том ского государственного университета. Управление, вычислительная техника и информатика. 2024. № 69. С. 134-143. doi: 10.17223/19988605/69/14.
Провкин В.А., Матросова А.Ю. Графовые представления множеств всех достижимых реакций комбинационной схемы // Вестник Томского государственного университета. Управление, вычислительная техника и информатика. 2022. № 61. С. 128-138. doi: 10.17223/19988605/61/13.
Scholl C., Becker B. Checking equivalence for circuits containing incompletely specified boxes // Int’l Conf. on Computer Design (ICCD). IEEE, 2002. P. 56-63.
Herbstritt M., Becker B., Scholl C. Advanced SAT-techniques for bounded model checking of blackbox designs // Int’l Workshop on Microprocessor Test and Verification (MTV). IEEE, 2006. P. 37-44.
Bryant R.E. Graph-Based Algorithms for Boolean Function Manipulation // IEEE Transactions on Computers. 1986. V. C-35, is. 8. P. 677-691.
dd package // Github.com. URL: https://github.com/tulip-control/dd (accessed: 25.04.2025).
The CUDD package, BDD, ADD Tutorial and examples // David Kebo Houngninou. URL: https://www.davidkebo.com/cudd#cudd1 (accessed: 25.04.2025).
Проверка эквивалентности частично построенных комбинационных схем | Вестник Томского государственного университета. Управление, вычислительная техника и информатика. 2025. № 71. DOI: 10.17223/19988605/71/13

Проверка эквивалентности частично построенных комбинационных схем | Вестник Томского государственного университета. Управление, вычислительная техника и информатика. 2025. № 71. DOI: 10.17223/19988605/71/13