Preview

Информатика

Расширенный поиск

ВЕРИФИКАЦИЯ ФУНКЦИОНАЛЬНЫХ ОПИСАНИЙ С НЕОПРЕДЕЛЕННОСТЬЮ НА ОСНОВЕ ПАРАФАЗНОГО ПРЕДСТАВЛЕНИЯ БУЛЕВЫХ ФУНКЦИЙ

Аннотация

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

Об авторах

Д. Я. Новиков
Объединенный институт проблем информатики НАН Беларуси
Беларусь


Л. Д. Черемисинова
Объединенный институт проблем информатики НАН Беларуси
Беларусь


Список литературы

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.

Просмотров: 478


Creative Commons License
Контент доступен под лицензией Creative Commons Attribution 4.0 License.


ISSN 1816-0301 (Print)
ISSN 2617-6963 (Online)