vestifmИзвестия Национальной академии наук Беларуси. Серия физико-математических наукProceedings of the National Academy of Sciences of Belarus. Physics and Mathematics Series1561-24302524-2415The Republican Unitary Enterprise Publishing House "Belaruskaya Navuka"vestifm-128Research ArticleИНФОРМАТИКАINFORMATICSПОИСК КРАТЧАЙШЕЙ УСТАНОВОЧНОЙ ПОСЛЕДОВАТЕЛЬНОСТИ СХЕМЫ С ПАМЯТЬЮ НА D-ТРИГГЕРАХSHORTEST SYNCHRONIZING SEQUENCE SEARCH FOR A SEQUENTIAL NETWORK WITH MEMORY ON D FLIP-FLOPSЧеремисиноваЛ. Д.CheremisinovaL. D.cld@newman.bas-net.byОбъединенный институт проблем информатики Национальной академии наук Беларуси, МинскUnited Institute of Informatics Problems of the National Academy of Sciences of Belarus, Minsk20151905201603119128Copyright © Черемисинова Л.Д., 20162016Черемисинова Л.Д.Cheremisinova L.D.Данная работа распространяется под лицензией Creative Commons Attribution 4.0.This work is licensed under a Creative Commons Attribution 4.0 License.https://vestifm.belnauka.by/jour/article/view/128

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

The problem under consideration is to find a synchronizing sequence of a minimal size for a logical network having flipflop primitives of type D as memory elements. A novel method is proposed, which is based on the formulation of the task as the Boolean satisfiability problem solved with any standard SAT-solver. The method is based on forming the conventional conjunctive normal form representation for combinational block, implementing excitation functions of the flip-flops.

тестированиеверификациялогический синтезавтоматизация проектированияtestingverificationlogic synthesisdesign automationReferencesStrunz, B. Design for Testability in Digital Integrated circuits [Electronic resourсe] / B. Strunz , C. Flanagan , T. Hall ; University of Limerick, Ireland. – Mode of access: http://www.cs.colostate.edu/~cs530/digital_testing.pdf. – Date of access: 01.07.2015.Strunz, B. Design for Testability in Digital Integrated circuits [Electronic resourсe] / B. Strunz , C. Flanagan , T. Hall ; University of Limerick, Ireland. – Mode of access: http://www.cs.colostate.edu/~cs530/digital_testing.pdf. – Date of access: 01.07.2015.Logic BIST: State-of-the-Art and Open Problems [Electronic resourсe] / N. Li [et al.]. – Mode of access: http://arxiv.org/ pdf/1503.04628.pdf. – Date of access: 01.07.2015.Logic BIST: State-of-the-Art and Open Problems [Electronic resourсe] / N. Li [et al.]. – Mode of access: http://arxiv.org/ pdf/1503.04628.pdf. – Date of access: 01.07.2015.Chakrabarty, K. DFBT: A Design-for-Testability Method Based on Balance Testing [Electronic resourсe] / K. Chakrabarty, P. Hayes; Department of Electrical Engineering and Computer Science University of Michigan. – Mode of access: http://citeseerx. ist.psu.edu/viewdoc/download?doi=10.1.1.380.9873&rep=rep1&type=pdf. – Date of access: 01.07.2015.Chakrabarty, K. DFBT: A Design-for-Testability Method Based on Balance Testing [Electronic resourсe] / K. Chakrabarty, P. Hayes; Department of Electrical Engineering and Computer Science University of Michigan. – Mode of access: http://citeseerx. ist.psu.edu/viewdoc/download?doi=10.1.1.380.9873&rep=rep1&type=pdf. – Date of access: 01.07.2015.Rene, D. Random testing of digital circuits. Theory and application / D. Rene. – [S. l.]: Marcel Dekker, Inc. 1998.Rene, D. Random testing of digital circuits. Theory and application / D. Rene. – [S. l.]: Marcel Dekker, Inc. 1998.Crouch, A. Design-for-Test for Digital IC’s and Embedded Core Systems / A. Crouch. – [S. l.]: Prentice Hall, 1999.Crouch, A. Design-for-Test for Digital IC’s and Embedded Core Systems / A. Crouch. – [S. l.]: Prentice Hall, 1999.Bushnell, M. L. Essentials of electronic testing for digital, memory and mixed-signal VLSI circuits / M. L. Bushnell, V. D. Agrawal. – [S. l.]: Kluwer Academic Publishers, 2002.Bushnell, M. L. Essentials of electronic testing for digital, memory and mixed-signal VLSI circuits / M. L. Bushnell, V. D. Agrawal. – [S. l.]: Kluwer Academic Publishers, 2002.Kohavi, Z. Switching and Finite Automata Theory / Z. Kohavi. – 2nd ed. – Cambridge [et al.]: Cambridge Univ. Press, 1978.Kohavi, Z. Switching and Finite Automata Theory / Z. Kohavi. – 2nd ed. – Cambridge [et al.]: Cambridge Univ. Press, 1978.Gill, A. Introduction to the Theory of Finite-state Machines / A. Gill. – [S. l.]: McGraw-Hill, 1962.Gill, A. Introduction to the Theory of Finite-state Machines / A. Gill. – [S. l.]: McGraw-Hill, 1962.Lee, D. Principles and methods of testing finite state machine – a survey / D. Lee, M. Yannakakis // Proc. of the IEEE. – 1996. – Vol. 84 (8). – P. 1090–1123.Lee, D. Principles and methods of testing finite state machine – a survey / D. Lee, M. Yannakakis // Proc. of the IEEE. – 1996. – Vol. 84 (8). – P. 1090–1123.Eppstein, D. Reset sequences for monotonic automata / D. Eppstein // SIAM J. on Computing. – 1990. – Vol. 19, no. 3. – P. 500–510.Eppstein, D. Reset sequences for monotonic automata / D. Eppstein // SIAM J. on Computing. – 1990. – Vol. 19, no. 3. – P. 500–510.Biere, A. PicoSAT essentials / A. Biere // J. on Satisfiability. Boolean Modeling and Computation. – 2008. – Vol. 4. – P. 75–97.Biere, A. PicoSAT essentials / A. Biere // J. on Satisfiability. Boolean Modeling and Computation. – 2008. – Vol. 4. – P. 75–97.Mahajan, Y. Zchaff 2004: an efficient SAT solver / Y. Mahajan, Z. Fu, S. Malik // Theory and Applications of Satisfiability Testing (2004 SAT Solver Competition and QBF Solver Evaluation (Invited Papers)). – Berlin; Heidelberg: Springer, 2005. – P. 360–375.Mahajan, Y. Zchaff 2004: an efficient SAT solver / Y. Mahajan, Z. Fu, S. Malik // Theory and Applications of Satisfiability Testing (2004 SAT Solver Competition and QBF Solver Evaluation (Invited Papers)). – Berlin; Heidelberg: Springer, 2005. – P. 360–375.Goldberg, E. BerkMin: afast and robust SAT-solver / E. Goldberg, Y. Novikov // 2002 Design, Automation and Test in Europe Conference and Exposition (DATE 2002), 4–8 March 2002, Paris, France. – [S. l.]: IEEE Computer Society, 2002. – P. 142–149.Goldberg, E. BerkMin: afast and robust SAT-solver / E. Goldberg, Y. Novikov // 2002 Design, Automation and Test in Europe Conference and Exposition (DATE 2002), 4–8 March 2002, Paris, France. – [S. l.]: IEEE Computer Society, 2002. – P. 142–149.Kuehlmann, A. Combinational and Sequential Equivalence Checking / A. Kuehlmann A., C. A. J. van Eijk. // Logic synthesis and Verification / eds S. Hassoun, T. Sasao, R. K. Brayton. – [S. l.]: Kluwer Academic Publishers, 2002. – P. 343–372.Kuehlmann, A. Combinational and Sequential Equivalence Checking / A. Kuehlmann A., C. A. J. van Eijk. // Logic synthesis and Verification / eds S. Hassoun, T. Sasao, R. K. Brayton. – [S. l.]: Kluwer Academic Publishers, 2002. – P. 343–372.

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