ИМПЛИКАТИВНЫЙ МЕТОД АНАЛИЗА ЧАСТИЧНЫХ БУЛЕВЫХ ФУНКЦИЙ
Abstract
Рассматривается задача определения, находятся ли системы частичных булевых функций в
отношении эквивалентности или реализации. Предлагается метод решения задачи путем сведения ее к проверке выполнимости конъюнктивной нормальной формы, в основе формирования которой лежит использование отношения импликации.
About the Authors
Д. Новиков
Объединенный институт проблем информатики НАН Беларуси
Belarus
Belarus
Л. Черемисинова
Объединенный институт проблем информатики НАН Беларуси
Belarus
Belarus
References
1. Kuehlmann, A. Combinational and Sequential Equivalence Checking / A. Kuehlmann,
2. A.J. Cornelis van Eijk // Logic synthesis and Verification ; ed. S. Hassoun, T. Sasao, R.K. Brayton. – Kluwer Academic Publishers, 2002. – P. 343–372.
3. Advanced Formal Verification / R. Drechsler [et al.]. – Boston, Dordrecht, London : Kluwer
4. Academic Publishers, 2005. – 249 p.
5. Новиков, Д.Я. Программный комплекс для верификации комбинационных устройств в процессе логического проектирования / Д.Я. Новиков, Л.Д. Черемисинова // Четвертый Белорусский космический конгресс : Материалы конгресса, Минск, 25–27 октября 2011 г. : в 2 т. / ОИПИ НАН Беларуси ; редкол.: А.В. Тузиков [и др.]. – Минск, 2011. – Т. 2. – С. 289–293.
6. Sorensson, N. MiniSat v1.13 A SAT Solver with Conflict-Clause Minimization /
7. N. Sorensson, N. Een // The International Conference on Theory and Applications of Satisfiability Testing (SAT 2005) [Electronic resource]. – 2005. – Mode of access : http://www.lri.fr/~simon/contest/
8. results/descriptions/solvers/minisat_static.pdf. – Date of access : 16.02.2009.
9. Kunz, W. SAT and ATPG: Algorithms for Boolean Decision Problems / W. Kunz,
10. J. Marques-Silva, S. Malik // Logic synthesis and Verification ; еd. S. Hassoun, T. Sasao and
11. R.K. Brayton. – Kluwer Academic Publishers, 2002. – P. 309–341.
12. Goldberg, E. BerkMin: A fast and robust SAT-Solver / E. Goldberg, Y. Novikov // European
13. Design and Test Conference (DATE’02) : Proc. of the conf., Paris, 4–8 March 2002 / Le Palais des Congres. – Paris, 2002. – P. 142–149.
14. Cheremisinova, L. SAT-Based Approach to Verification of Logical Descriptions with Functional Indeterminacy / L. Cheremisinova, D. Novikov // 8th Intern. Workshop on Boolean Problems : Proc. of the Workshop, Freiberg, 18–19 September 2008 / Techn. univ. Bergakademie ; ed. by
15. B. Steinbach. – Freiberg, 2008. – P. 59–66.
16. Черемисинова, Л.Д. Формальная верификация описаний с функциональной неопределенностью на основе проверки выполнимости конъюнктивной нормальной формы / Л.Д. Черемисинова, Д.Я. Новиков // Автоматика и вычислительная техника. – 2010. – № 1. – C. 5–16.
17. Закревский, А.Д. Генераторы псевдослучайных логико-комбинаторных объектов в
18. С++ / А.Д. Закревский, Н.Р. Торопов // Логическое проектирование. – Минск : Ин-т техн. кибернетики НАН Беларуси, 1999. – Вып. 4. – С. 49–63.
Review
For citations:
, . Informatics. 2012;(2(34)):79-86. (In Russ.)
Views: 543
Email this article 