informИнформатикаInformatics1816-03012617-6963UIIP NASBinform-298Research ArticleЛОГИЧЕСКОЕ ПРОЕКТИРОВАНИЕLOGICAL DESIGNИМПЛИКАТИВНЫЙ МЕТОД АНАЛИЗА ЧАСТИЧНЫХ БУЛЕВЫХ ФУНКЦИЙНовиковД. Я.ЧеремисиноваЛ. Д.Объединенный институт проблем информатики НАН БеларусиBelarus20121903201802(34)7986Copyright © Новиков Д.Я., Черемисинова Л.Д., 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/298

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

ReferencesKuehlmann, 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 ; ed. S. Hassoun, T. Sasao, R.K. Brayton. – Kluwer Academic Publishers, 2002. – P. 343–372.A.J. Cornelis van Eijk // Logic synthesis and Verification ; ed. S. Hassoun, T. Sasao, R.K. Brayton. – Kluwer Academic Publishers, 2002. – P. 343–372.Advanced Formal Verification / R. Drechsler [et al.]. – Boston, Dordrecht, London : KluwerAdvanced Formal Verification / R. Drechsler [et al.]. – Boston, Dordrecht, London : KluwerAcademic Publishers, 2005. – 249 p.Academic Publishers, 2005. – 249 p.Новиков, Д.Я. Программный комплекс для верификации комбинационных устройств в процессе логического проектирования / Д.Я. Новиков, Л.Д. Черемисинова // Четвертый Белорусский космический конгресс : Материалы конгресса, Минск, 25–27 октября 2011 г. : в 2 т. / ОИПИ НАН Беларуси ; редкол.: А.В. Тузиков [и др.]. – Минск, 2011. – Т. 2. – С. 289–293.Новиков, Д.Я. Программный комплекс для верификации комбинационных устройств в процессе логического проектирования / Д.Я. Новиков, Л.Д. Черемисинова // Четвертый Белорусский космический конгресс : Материалы конгресса, Минск, 25–27 октября 2011 г. : в 2 т. / ОИПИ НАН Беларуси ; редкол.: А.В. Тузиков [и др.]. – Минск, 2011. – Т. 2. – С. 289–293.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/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.02.2009.results/descriptions/solvers/minisat_static.pdf. – Date of access : 16.02.2009.Kunz, W. SAT and ATPG: Algorithms for Boolean Decision Problems / W. Kunz,Kunz, W. SAT and ATPG: Algorithms for Boolean Decision Problems / W. Kunz,J. Marques-Silva, S. Malik // Logic synthesis and Verification ; еd. S. Hassoun, T. Sasao andJ. Marques-Silva, S. Malik // Logic synthesis and Verification ; еd. S. Hassoun, T. Sasao andR.K. Brayton. – Kluwer Academic Publishers, 2002. – P. 309–341.R.K. Brayton. – Kluwer Academic Publishers, 2002. – P. 309–341.Goldberg, E. BerkMin: A fast and robust SAT-Solver / E. Goldberg, Y. Novikov // EuropeanGoldberg, E. BerkMin: A fast and robust SAT-Solver / E. Goldberg, Y. Novikov // EuropeanDesign and Test Conference (DATE’02) : Proc. of the conf., Paris, 4–8 March 2002 / Le Palais des Congres. – Paris, 2002. – P. 142–149.Design and Test Conference (DATE’02) : Proc. of the conf., Paris, 4–8 March 2002 / Le Palais des Congres. – Paris, 2002. – P. 142–149.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. byCheremisinova, 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. byB. Steinbach. – Freiberg, 2008. – P. 59–66.B. Steinbach. – Freiberg, 2008. – P. 59–66.Черемисинова, Л.Д. Формальная верификация описаний с функциональной неопределенностью на основе проверки выполнимости конъюнктивной нормальной формы / Л.Д. Черемисинова, Д.Я. Новиков // Автоматика и вычислительная техника. – 2010. – № 1. – C. 5–16.Черемисинова, Л.Д. Формальная верификация описаний с функциональной неопределенностью на основе проверки выполнимости конъюнктивной нормальной формы / Л.Д. Черемисинова, Д.Я. Новиков // Автоматика и вычислительная техника. – 2010. – № 1. – C. 5–16.Закревский, А.Д. Генераторы псевдослучайных логико-комбинаторных объектов вЗакревский, А.Д. Генераторы псевдослучайных логико-комбинаторных объектов вС++ / А.Д. Закревский, Н.Р. Торопов // Логическое проектирование. – Минск : Ин-т техн. кибернетики НАН Беларуси, 1999. – Вып. 4. – С. 49–63.С++ / А.Д. Закревский, Н.Р. Торопов // Логическое проектирование. – Минск : Ин-т техн. кибернетики НАН Беларуси, 1999. – Вып. 4. – С. 49–63.

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