ВЕРИФИКАЦИЯ ФУНКЦИОНАЛЬНЫХ ОПИСАНИЙ С НЕОПРЕДЕЛЕННОСТЬЮ НА ОСНОВЕ ПАРАФАЗНОГО ПРЕДСТАВЛЕНИЯ БУЛЕВЫХ ФУНКЦИЙ
Abstract
Исследуется задача проверки реализуемости системы частично определенных булевых функций многоблочной структурой, каждый блок которой также задается системой частично определенных булевых функций. Предлагается метод сведения задачи к проверке выполнимости конъюнктивной нормальной формы (КНФ), которая является объединением КНФ разрешения многоблочной структуры и КНФ запрета исходной системы функций. В основе построения КНФ разрешения лежит парафазное представление функций, реализуемых структурой.
About the Authors
Д. Новиков
Объединенный институт проблем информатики НАН Беларуси
Belarus
Belarus
Л. Черемисинова
Объединенный институт проблем информатики НАН Беларуси
Belarus
Belarus
References
1. Advanced Formal Verification / R. Drechsler [et al.]. – Kluwer Academic Publishers, 2005. –
2. p.
3. Kunz, W. SAT and ATPG: Algorithms for Boolean Decision Problems. – Logic synthesis and
4. Verification / W. Kunz ; ed. S. Hassoun, T. Sasao and R.K. Brayton. – Kluwer Academic Publishers,
5. – P. 309–341.
6. Goldberg, E. BerkMin: A fast and robust SAT-Solver / E. Goldberg , Y. Novikov // Proceedings
7. of the conference on Design, automation and test in Europe. – France, Paris, 2002. – P. 142–149.
8. Cheremisinova, L. Simulation-based approach to verification of logical descriptions with
9. functional indeterminacy / L. Cheremisinova, D. Novikov // Information Theories & Applications
10. (IJ ITA). – 2008. – Vol. 15, № 3. – P. 218–224.
11. Cheremisinova, L. SAT-Based Approach to Verification of Logical Descriptions with Functional
12. Indeterminacy / L. Cheremisinova, D. Novikov // Proc. 8th International Workshop on Boolean
13. Problems. – Germany, Freiberg, 2008. – P. 59–66.
14. 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.
15. Cheremisinova, L.D. Verification of multi-block structures with functional indeterminacy /
16. L. Cheremisinova, D. Novikov // Материалы VI Междунар. конф. «Автоматизация проектирования дискретных устройств» (CAD DD’07). – Минск : ОИПИ НАН Беларуси, 2007. – С. 103–108.
Review
For citations:
, . Informatics. 2010;(3(27)):54-62. (In Russ.)
Views: 508
Email this article 