Методы анализа выполнимости булевых формул являются одним из эффективных подходов к решению задачи булевого сопоставления и проверки эквивалентности цифровых схем. В комбинации с классическими трассировочными алгоритмами и оптимизационными техниками данные методы показывают результаты, превосходящие классические алгоритмы трассировки по скорости работы и качеству получаемого результата. В работе выполнен анализ современной практики применения методов на основе задачи выполнимости булевых формул в системах автоматизации проектирования сверхбольших интегральных схем. Рассмотрены примеры подходов на основе задачи выполнимости булевых формул к задачам трассировки и формальной проверки эквивалентности описаний цифровых схем в рамках технологического отображения в составе маршрута проектирования ПЛИС. Разработан и представлен алгоритм детальной трассировки блоков коммутации ПЛИС с применением задачи выполнимости. Результаты его работы продемонстрированы на примере программируемого логического блока интегральной микросхемы российского производства 5400ТР094. Блок имеет островную архитектуру, т.е. малые программируемые логические блоки и блоки коммутации образуют регулярно повторяющуюся схемотехническую структуру. Свойства выбранной классической архитектуры позволяют расширить область применения предложенного алгоритма на весь класс ПЛИС островного типа. Тестирование алгоритма проведено на наборах проектных схем ISCAS-85, ISCAS-89 и LGSynth-89. Выполнено сравнение разработанного алгоритма на основе методов анализа выполнимости булевых формул с известным алгоритмом трассировки Pathfinder по критериям затраченного времени и достигнутой степени разводимости блоков коммутации. Установлено, что методы анализа выполнимости булевых формул для задачи трассировки способны к доказательству неразводимости рассматриваемой трассировочной задачи в отличие от алгоритма Pathfinder, результаты работы которого могут лишь косвенно свидетельствовать об этом. Показано, что применение более производительного решателя для задачи выполнимости существенно ускоряет работу предложенного алгоритма детальной трассировки.
1. Гаврилов С.В., Глебов А.Л., Стемпковский А.Л. Методы логического и логико-временного ана-лиза цифровых КМОП СБИС. M.: Наука, 2007. 223 c.
2. Cook S. The complexity of theorem proving procedures // Proc. of the Third Annual ACM Symposium on Theory of Computing. 1971. P. 151–158.
3. Левин Л.А. Универсальные задачи перебора // Проблемы передачи информации. 1973. Т. 9. № 3. С. 115–116.
4. SAT-solving in practice, with a tutorial example from supervisory control / C. Koen, N. Eén, M. Sheeran et al. // Discrete Event Dynamic Systems. 2009. Vol.19 (4). P. 495–524.
5. Ohrimenko O., Stuckey P.J., Codish M. Propagation = Lazy clause generation // Principles and Practice of Constraint Programming – CP 2007 Lecture Notes in Computer Science / Ed. by C. Bessière. Berlin, Heidel-berg: Springer, 2007. P. 544–558.
6. Järvisalo M., Le Berre D., Roussel O., Simon L. The international sat solver competitions // AI Mag. 2012. Vol. 33 (1). P. 89–92.
7. Marques-Silva J. Practical applications of Boolean satisfiability // Proc. of the 9th International Work-shop on Discrete Event Systems (Goteborg, Sweden, May 2008). 2008. P. 74–80.
8. The International SAT Competition Web Page. URL: http://www.satcompetition.org/ (дата обращения: 29.04.2020).
9. Katebi H., Markov I.L. Large-scale Boolean matching // 2010 Design, Automation & Test in Europe Conference & Exhibition (DATE 2010). Dresden, 2010. P. 771–776.
10. A two-step search engine for large scale boolean matching under NP3 equivalence / C. Pui, P. Tu,
H. Li et al. // 2018 23rd Asia and South Pacific Design Automation Conference (ASP-DAC). Jeju, 2018.
P. 592–598.
11. Dehbashi M., Fey G. Debug automation for synchronization bugs at RTL // 27th Intern. Conf. on VLSI Design and 2014 13th International Conference on Embedded Systems. 2014. P. 44–49.
12. Гаврилов С.В. Методы анализа логических корреляций для САПР цифровых КМОП СБИС.
М.: Техносфера, 2011. 136 c.
13. ABC: A system for sequential synthesis and verification. URL: https://people.eecs.berkeley.edu/~alanmi/abc/ (дата обращения: 31.05.2020).
14. Mishchenko A., Brayton R., Jiang J.-H. R., Jang S. SAT-based logic optimization and resynthesis // Proc. IWLS. 2007. P. 358–364.
15. Een N., Sörensson N. An extensible SAT-solver // SAT’03. URL: http://www.cs.chalmers.se/Cs/Research/FormalMethods/MiniSat (дата обращения: 31.05.2020).
16. Wood R.G., Rutenbar R.A. FPGA routing and routability estimation via boolean satisfiability // IEEE Transactions on Very Large Scale Integration (VLSI) Systems. 1998. Vol. 6. No. 2. P. 222–231.
17. Nam G.-J., Sakaliah K.A., Rutenbar R.A. Satisfiability-based layout revisited: detailed routing of complex FPGAs via search-based boolean SAT // Proc. of the 1999 ACM/SIGDA Seventh International Sympo-sium on Field Programmable Gate Arrays (Feb. 1999). 1999. P. 167–175.
18. Nam G.-J., Aloul F., Sakallah K.A., Rutenbar R.A. A comparative study of two Boolean formulations of FPGA detailed routing constraints // IEEE Transactions on Computers. 2001. Vol. 53. No. 6. P. 688–696.
19. Nam G.-J., Sakallah K.A., Rutenbar R.A. A new FPGA detailed routing approach via search-based Boolean satisfiability // IEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems. 2002. Vol. 21. No. 6. P. 674–684.
20. Nam G.-J., Sakallah K., Rutenbar R.A. Hybrid routing for FPGAs by integrating boolean satisfiability with geometric search // Field-Programmable Logic and Applications: Reconfigurable Computing Is Going Mainstream Lecture Notes in Computer Science / Ed. by M. Glesner, P. Zipf, M. Renovell. Berlin, Heidelberg: Springer Berlin Heidelberg, 2002. P. 360–369.
21. Железников Д.А., Заплетина М.А., Хватов В.М. Исследование механизма разрыва и перетрас-сировки на этапе топологического синтеза в базисе реконфигурируемых систем на кристалле // Пробле-мы разработки перспективных микро- и наноэлектронных систем МЭС. 2018. С. 188–192.
22. Marques Silva J.P., Sakallah K. GRASP – a new search algorithm for satisfiability // Proc. of the 1996 IEEE/ACM International Conference on Computer-Aided Design (ICCAD ’96). IEEE Computer Society, USA, 1997. P. 220–227.
23. McMurchie L.E., Ebeling C. PathFinder: a negotiation-based path-driven router for FPGAs // Proc. ACM/IEEE Int. Symposium on Field Programmable Gate Arrays (Feb. 1995). 1995. P. 111–117.
24. Liu Z., Yu Z., Gu X. A new and efficient algorithm for FPGA routing // 2007 2nd IEEE Conference on Industrial Electronics and Applications. Harbin, 2007. P. 1431–1436.
25. Fraisse H., Joshi A., Gaitonde D., Kaviani A. Boolean satisfiability-based routing and its application to xilinx ultrascale clock network // Proc. of the 2016 ACM/SIGDA Intern. Symposium on Field-Programmable Gate Arrays (FPGA ’16). 2016. P. 74–79.
26. Board-level multiterminal net assignment for the partial cross-bar architecture / X. Song,
W.N.N. Hung, A. Mishchenko et al. // IEEE Transactions on Very Large Scale Integration (VLSI) Systems. 2003. Vol. 11. No. 3. P. 511–514.
27. Velev M.N., Gao P. Comparison of boolean satisfiability encodings on FPGA detailed routing
problems // 2008 Design, Automation and Test in Europe. Munich, 2008. P. 1268–1273.
28. Fraisse H. Incremental routing for circuit designs using a SAT router // Pat. 10445456 USA. 2019.
29. Xilinx Vivado Design Suite. URL: https://www.xilinx.com/products/design-tools/vivado.html (дата обращения: 31.05.2020).
30. ДЦ «Союз»: 5400ТР094 ПАЦИС. URL: https://dcsoyuz.ru/products/pais/art/1605 (дата обращения: 09.07.2020).
31. Zhukov D.V., Zheleznikov D.A., Zapletina M.A. The iterative SAT based approach to detailed routing for reconfigurable system-on-a-chip // 2020 IEEE Conf. of Russian Young Researchers in Electrical and Elec-tronic Engineering (EIConRus). 2020. P. 1905–1910.
32. Наборы тестовых схем ISCAS’89 и LGSynth’89. URL: https://ddd.fit.cvut.cz/prj/Benchmarks/ (дата обращения: 09.07.2020).
33. Davis M., Logemann G., Loveland D. A machine program for theorem-proving // Commun. ACM. 1962. Vol.5. No. 7. P. 394–397.