informИнформатикаInformatics1816-03012617-6963UIIP NASBinform-354Research ArticleЛОГИЧЕСКОЕ ПРОЕКТИРОВАНИЕLOGICAL DESIGNВЕРИФИКАЦИЯ ЛОГИЧЕСКИХ СХЕМ, РЕАЛИЗУЮЩИХ СИСТЕМЫ ЧАСТИЧНЫХ БУЛЕВЫХ ФУНКЦИЙБибилоП. Н.НовиковД. Я.Объединенный институт проблем информатики НАН БеларусиBelarus20111904201803(31)6876Copyright © Бибило П.Н., Новиков Д.Я., 20182018Бибило П.Н., Новиков Д.Я.Бибило П.Н., Новиков Д.Я.Данная работа распространяется под лицензией Creative Commons Attribution 4.0.This work is licensed under a Creative Commons Attribution 4.0 License.https://inf.grid.by/jour/article/view/354

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

ReferencesЗакревский, А.Д. Логические основы проектирования дискретных устройств /Закревский, А.Д. Логические основы проектирования дискретных устройств /А.Д. Закревский, Ю.В. Поттосин, Л.Д. Черемисинова. – М. : Физматлит, 2007. – 589 c.А.Д. Закревский, Ю.В. Поттосин, Л.Д. Черемисинова. – М. : Физматлит, 2007. – 589 c.Бибило, П.Н. Cистемы проектирования интегральных схем на основе языка VHDL.Бибило, П.Н. Cистемы проектирования интегральных схем на основе языка VHDL.StateCAD, ModelSim, LeonardoSpectrum / П.Н. Бибило. – М. : СОЛОН-Пресс, 2005. – 384 с.StateCAD, ModelSim, LeonardoSpectrum / П.Н. Бибило. – М. : СОЛОН-Пресс, 2005. – 384 с.Черемисинова, Л.Д. Верификация многоблочных структур с функциональной неопределенностью / Л.Д. Черемисинова, Д.Я. Новиков // Известия Нац. акад. наук Беларуси. Сер. физ-техн. наук. – 2009. – № 2. – С. 98–105.Черемисинова, Л.Д. Верификация многоблочных структур с функциональной неопределенностью / Л.Д. Черемисинова, Д.Я. Новиков // Известия Нац. акад. наук Беларуси. Сер. физ-техн. наук. – 2009. – № 2. – С. 98–105.Черемисинова, Л.Д. Проверка схемной реализации частичных булевых функций /Черемисинова, Л.Д. Проверка схемной реализации частичных булевых функций /Л.Д. Черемисинова, Д.Я. Новиков // Вестник Томского государственного университета.Л.Д. Черемисинова, Д.Я. Новиков // Вестник Томского государственного университета.Сер. Управление, вычислительная техника и информатика. – 2008. – № 4. – С. 102–111.Сер. Управление, вычислительная техника и информатика. – 2008. – № 4. – С. 102–111.Novikov, Ya. Foundations of Hierarchical SAT-Solving / Ya. Novikov, R. Brinkmann //Novikov, Ya. Foundations of Hierarchical SAT-Solving / Ya. Novikov, R. Brinkmann //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.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.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.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.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.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.Sorensson, N. MiniSat v1.13 – A SAT Solver with Conflict-Clause Minimization /Sorensson, N. MiniSat v1.13 – A SAT Solver with Conflict-Clause Minimization /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.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.Kuehlmann, A. Combinational and Sequential Equivalence Checking / A. Kuehlmann,Kuehlmann, A. Combinational and Sequential Equivalence Checking / A. Kuehlmann,A.J. Cornelis van Eijk // Logic synthesis and Verification. – Norwell : Kluwer Academic Publishers, 2002. – P. 343–372.A.J. Cornelis van Eijk // Logic synthesis and Verification. – Norwell : Kluwer Academic Publishers, 2002. – P. 343–372.Бибило, П.Н. Совместное использование синтезаторов Leonardo и XST при проекти-Бибило, П.Н. Совместное использование синтезаторов Leonardo и XST при проекти-ровании цифровых схем на FPGA / П.Н. Бибило // Информационные технологии. – 2008. – № 3. – С. 7–12.ровании цифровых схем на FPGA / П.Н. Бибило // Информационные технологии. – 2008. – № 3. – С. 7–12.Espresso examples / University of California Berkeley [Electronic resource]. – 2006. –Espresso examples / University of California Berkeley [Electronic resource]. – 2006. –Mode of access : http://www1.cs.columbia.edu/~cs4861/sis/espresso-examples/ex. – Date of access : 06.01.2010.Mode of access : http://www1.cs.columbia.edu/~cs4861/sis/espresso-examples/ex. – Date of access : 06.01.2010.

The authors declare that there are no conflicts of interest present.