ВЕРИФИКАЦИЯ ЛОГИЧЕСКИХ СХЕМ, РЕАЛИЗУЮЩИХ СИСТЕМЫ ЧАСТИЧНЫХ БУЛЕВЫХ ФУНКЦИЙ
Abstract
Рассматривается задача верификации логических схем, реализующих системы частично определенных булевых функций. Описываются VHDL-модели различных форм задания таких систем. Предлагается программа для решения рассматриваемой задачи на основе совместного использования троичного параллельного моделирования и сведения к задаче проверки выполнимости конъюнктивной нормальной формы. Приводятся результаты экспериментов по верификации, показывающие высокую эффективность разработанной программы по сравнению с VHDL-моделированием, которое позволяет проводить система ModelSim.
About the Authors
П. Бибило
Объединенный институт проблем информатики НАН Беларуси
Belarus
Belarus
Д. Новиков
Объединенный институт проблем информатики НАН Беларуси
Belarus
Belarus
References
1. Закревский, А.Д. Логические основы проектирования дискретных устройств /
2. А.Д. Закревский, Ю.В. Поттосин, Л.Д. Черемисинова. – М. : Физматлит, 2007. – 589 c.
3. Бибило, П.Н. Cистемы проектирования интегральных схем на основе языка VHDL.
4. StateCAD, ModelSim, LeonardoSpectrum / П.Н. Бибило. – М. : СОЛОН-Пресс, 2005. – 384 с.
5. Черемисинова, Л.Д. Верификация многоблочных структур с функциональной неопределенностью / Л.Д. Черемисинова, Д.Я. Новиков // Известия Нац. акад. наук Беларуси. Сер. физ-техн. наук. – 2009. – № 2. – С. 98–105.
6. Черемисинова, Л.Д. Проверка схемной реализации частичных булевых функций /
7. Л.Д. Черемисинова, Д.Я. Новиков // Вестник Томского государственного университета.
8. Сер. Управление, вычислительная техника и информатика. – 2008. – № 4. – С. 102–111.
9. Novikov, Ya. Foundations of Hierarchical SAT-Solving / Ya. Novikov, R. Brinkmann //
10. th International Workshop on Boolean Problems : Proc. of the Workshop, Freiberg, 23–24 September 2004 / University of Mining and Technology. – Freiberg, 2004. – P. 103–142.
11. Tsetin, G.S. On the Complexity of Derivation in Propositional Calculus / G.S. Tsetin // Studies in Constructive Mathematics and Mathematical Logic / ed. by A.O. Slisenko ; Steklov Mathematical Institute. – Leningrad, 1968. – Part 2. – P. 115–125.
12. Een, N. An Extensible SAT-solver / N. Een, N. Sorensson // Theory and Applications of Satisfiability Testing (SAT 2003) : Proc. of the Intern. Conf., Santa Margherita Ligure, Italy, May 5–8, 2003 / Microsoft Research. – Santa Margherita Ligure, 2003. – P. 502–518.
13. Sorensson, N. MiniSat v1.13 – A SAT Solver with Conflict-Clause Minimization /
14. 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/results/descriptions/solvers/minisat_static.pdf. – Date of access : 16.07.2010.
15. Kuehlmann, A. Combinational and Sequential Equivalence Checking / A. Kuehlmann,
16. A.J. Cornelis van Eijk // Logic synthesis and Verification. – Norwell : Kluwer Academic Publishers, 2002. – P. 343–372.
17. Бибило, П.Н. Совместное использование синтезаторов Leonardo и XST при проекти-
18. ровании цифровых схем на FPGA / П.Н. Бибило // Информационные технологии. – 2008. – № 3. – С. 7–12.
19. Espresso examples / University of California Berkeley [Electronic resource]. – 2006. –
20. Mode of access : http://www1.cs.columbia.edu/~cs4861/sis/espresso-examples/ex. – Date of access : 06.01.2010.
Review
For citations:
, . Informatics. 2011;(3(31)):68-76. (In Russ.)
Views: 584
Email this article 