Currently, the methods based on a Boolean satisfiability (SAT) problem are one of the efficient approaches to solving the problem of Boolean matching and the equivalence checking of digital circuits. In combination with classic routing algorithms and optimization techniques, the SAT methods demonstrate the results exceeding the classic routing algorithms by the operation speed and the quality of obtained results. In the paper, the analysis of the modern practice of using the SAT methods in the CAD systems for VLSI has been performed. The examples of modern SAT approaches to the problems of the formal equivalence checking of digital circuits descriptions within the technological mapping framework and to the routing problem as a part of the FPGA design flow have been considered. The algorithm of the detailed routing of the FPGA switching blocks using the satisfiability problem has been developed and presented. The results of its work have been demonstrated on the example of the programmable logic block of the domestic made integrated circuit 5400TP094. The block has the island architecture, where the configurable logic blocks and switching blocks form a regularly repeated layout template. The properties of the chosen classic architecture permit to expand the region of presented algorithm to the entire class of island style FPGA. The algorithm has been tested on the project benchmarks ISCAS-85, ISCAS-89 and LGSynth-89. The comparison of the developed SAT-based algorithm with the well-known routing algorithm Pathfinder by criteria of the elapsed time and the achieved portion of routed nets in the switching blocks is presented. It has been determined that the considered Boolean satisfiability methods for the routing problem are capable to prove the circuit unroutability, unlike the algorithm Pathfinder which results can only implicitly indicate it. The paper demonstrates that the application of more efficient SAT solver significantly accelerates work of the suggested detailed routing algorithm.
Mariya A. Zapletina
Institute for Design Problems in Microelectronics of Russian Academy of Sciences, Moscow, Russia
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.