informИнформатикаInformatics1816-03012617-6963UIIP NASBinform-408Research ArticleМАТЕМАТИЧЕСКОЕ МОДЕЛИРОВАНИЕMATHEMATICAL MODELINGВЕРИФИКАЦИЯ ФУНКЦИОНАЛЬНЫХ ОПИСАНИЙ С НЕОПРЕДЕЛЕННОСТЬЮ НА ОСНОВЕ ПАРАФАЗНОГО ПРЕДСТАВЛЕНИЯ БУЛЕВЫХ ФУНКЦИЙНовиковД. Я.ЧеремисиноваЛ. Д.Объединенный институт проблем информатики НАН БеларусиBelarus20100205201803(27)5462Copyright © Новиков Д.Я., Черемисинова Л.Д., 20182018Новиков Д.Я., Черемисинова Л.Д.Новиков Д.Я., Черемисинова Л.Д.Данная работа распространяется под лицензией Creative Commons Attribution 4.0.This work is licensed under a Creative Commons Attribution 4.0 License.https://inf.grid.by/jour/article/view/408

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

ReferencesAdvanced Formal Verification / R. Drechsler [et al.]. – Kluwer Academic Publishers, 2005. –Advanced Formal Verification / R. Drechsler [et al.]. – Kluwer Academic Publishers, 2005. –p.p.Kunz, W. SAT and ATPG: Algorithms for Boolean Decision Problems. – Logic synthesis andKunz, W. SAT and ATPG: Algorithms for Boolean Decision Problems. – Logic synthesis andVerification / W. Kunz ; ed. S. Hassoun, T. Sasao and R.K. Brayton. – Kluwer Academic Publishers,Verification / W. Kunz ; ed. S. Hassoun, T. Sasao and R.K. Brayton. – Kluwer Academic Publishers,– P. 309–341.– P. 309–341.Goldberg, E. BerkMin: A fast and robust SAT-Solver / E. Goldberg , Y. Novikov // ProceedingsGoldberg, E. BerkMin: A fast and robust SAT-Solver / E. Goldberg , Y. Novikov // Proceedingsof the conference on Design, automation and test in Europe. – France, Paris, 2002. – P. 142–149.of the conference on Design, automation and test in Europe. – France, Paris, 2002. – P. 142–149.Cheremisinova, L. Simulation-based approach to verification of logical descriptions withCheremisinova, L. Simulation-based approach to verification of logical descriptions withfunctional indeterminacy / L. Cheremisinova, D. Novikov // Information Theories & Applicationsfunctional indeterminacy / L. Cheremisinova, D. Novikov // Information Theories & Applications(IJ ITA). – 2008. – Vol. 15, № 3. – P. 218–224.(IJ ITA). – 2008. – Vol. 15, № 3. – P. 218–224.Cheremisinova, L. SAT-Based Approach to Verification of Logical Descriptions with FunctionalCheremisinova, L. SAT-Based Approach to Verification of Logical Descriptions with FunctionalIndeterminacy / L. Cheremisinova, D. Novikov // Proc. 8th International Workshop on BooleanIndeterminacy / L. Cheremisinova, D. Novikov // Proc. 8th International Workshop on BooleanProblems. – Germany, Freiberg, 2008. – P. 59–66.Problems. – Germany, Freiberg, 2008. – P. 59–66.Tseitin, G.C. On the Complexity of Derivation in Propositional Calculus / G.C. Tseitin // Studies in Constructive Mathematics and Mathematical Logic. – New York, London, 1968. – Part 2. – P. 115–125.Tseitin, G.C. On the Complexity of Derivation in Propositional Calculus / G.C. Tseitin // Studies in Constructive Mathematics and Mathematical Logic. – New York, London, 1968. – Part 2. – P. 115–125.Cheremisinova, L.D. Verification of multi-block structures with functional indeterminacy /Cheremisinova, L.D. Verification of multi-block structures with functional indeterminacy /L. Cheremisinova, D. Novikov // Материалы VI Междунар. конф. «Автоматизация проектирования дискретных устройств» (CAD DD’07). – Минск : ОИПИ НАН Беларуси, 2007. – С. 103–108.L. Cheremisinova, D. Novikov // Материалы VI Междунар. конф. «Автоматизация проектирования дискретных устройств» (CAD DD’07). – Минск : ОИПИ НАН Беларуси, 2007. – С. 103–108.

The authors declare that there are no conflicts of interest present.