Preview

Информатика

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

ИМПЛИКАТИВНЫЙ МЕТОД АНАЛИЗА ЧАСТИЧНЫХ БУЛЕВЫХ ФУНКЦИЙ

Аннотация

Рассматривается задача определения, находятся ли системы частичных булевых функций в
отношении эквивалентности или реализации. Предлагается метод решения задачи путем сведения ее к проверке выполнимости конъюнктивной нормальной формы, в основе формирования которой лежит использование отношения импликации.

Об авторах

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


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


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

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.


Рецензия

Для цитирования:


Новиков Д.Я., Черемисинова Л.Д. ИМПЛИКАТИВНЫЙ МЕТОД АНАЛИЗА ЧАСТИЧНЫХ БУЛЕВЫХ ФУНКЦИЙ. Информатика. 2012;(2(34)):79-86.

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


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


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