Формальная верификация логических описаний с функциональной неопределённостью на основе логарифмического кодирования условий

Рассматривается задача проверки реализуемости описания с функциональной неопределённостью, представленного системой частично определенных булевых функций (ЧБФ), заданной комбинационной схемой. Проверка реализуемости основана на формальном подходе, предполагающем построение конъюнктивной нормальной формы (КНФ) на основе кодирования многовыходных интервалов из области задания этой системы. Предлагается метод построения КНФ, связанной с системой ЧБФ, который основан на логарифмическом кодировании многовыходных интервалов из области задания этой системы и позволяет сократить число переменных, дополнительно вводимых в формируемую КНФ.

Статья представлена к публикации членом редколлегии: П. П. Пархоменко