ВЕРИФИКАЦИЯ ФУНКЦИОНАЛЬНЫХ ОПИСАНИЙ С НЕОПРЕДЕЛЕННОСТЬЮ НА ОСНОВЕ ПАРАФАЗНОГО ПРЕДСТАВЛЕНИЯ БУЛЕВЫХ ФУНКЦИЙ
Аннотация
Исследуется задача проверки реализуемости системы частично определенных булевых функций многоблочной структурой, каждый блок которой также задается системой частично определенных булевых функций. Предлагается метод сведения задачи к проверке выполнимости конъюнктивной нормальной формы (КНФ), которая является объединением КНФ разрешения многоблочной структуры и КНФ запрета исходной системы функций. В основе построения КНФ разрешения лежит парафазное представление функций, реализуемых структурой.
Об авторах
Д. Я. Новиков
Объединенный институт проблем информатики НАН Беларуси
Беларусь
Беларусь
Л. Д. Черемисинова
Объединенный институт проблем информатики НАН Беларуси
Беларусь
Беларусь
Список литературы
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.
Рецензия
Для цитирования:
Новиков Д.Я., Черемисинова Л.Д. ВЕРИФИКАЦИЯ ФУНКЦИОНАЛЬНЫХ ОПИСАНИЙ С НЕОПРЕДЕЛЕННОСТЬЮ НА ОСНОВЕ ПАРАФАЗНОГО ПРЕДСТАВЛЕНИЯ БУЛЕВЫХ ФУНКЦИЙ. Информатика. 2010;(3(27)):54-62.
Просмотров: 533
Послать статью по эл. почте 