Обзор методов извлечения моделей из HDL-описаний

В статье дается обзор существующих методов извлечения моделей из описаний цифровой аппаратуры, разработанных на языках семейства HDL (Hardware Description Language). Методы извлечения моделей используются для решения многих задач, связанных с процессом проектирования и обеспечения качества программных и аппаратных систем. В данной работе затрагиваются методы решения следующих актуальных задач – оптимизация кода, оптимизация логического синтеза, абстракция, функциональная верификация. В статье рассматриваются методы извлечения таких семейств моделей, как графы потока и зависимостей, а также автоматные модели. Подробно рассматриваются методы построения программных срезов, конечных автоматов и расширенных конечных автоматов.

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

1. А.С. Камкин, А.М. Коцыняк, С.А. Смолов, А.А. Сортов, А.Д. Татарников, М.М. Чупилко. Средства функциональной верификации микропроцессоров. Труды ИСП РАН, т. 26, вып. 1, 2014 г., стр. 149-200. doi: 10.15514/ISPRAS-2014-26(1)-5

2. Statistical Analysis of Floating Point Flaw: Intel White Paper Section 3. http://www.intel.com/support/processors/pentium/sb/CS-013007.htm. Дата публикации: 08.07.2004.

3. Z. Navabi. Languages for Design and Implementation of Hardware. W.-K. Chen (Ed.). The VLSI Handbook. CRC Press, London, 2007, 2320 p.

4. IEEE Standard for Verilog Hardware Description Language, 1364-2005, IEEE, 2006, 560 p.

5. IEEE Standard VHDL Language Reference Manual, 1076-2008, IEEE, 2009, 626 p.

6. A.V. Aho, M.S. Lam, R. Sethi, J.D. Ullman. Compilers: Principles, Technologies, and Tools (2nd Edition). Addison Wesley, 2006. 1000 p.

7. A. Balboni, M. Mastretti, M. Stefanoni. Static Analysis for VHDL Model Evaluation. Proceedings of the European Design Automation Conference (EURO-DAC '94), IEEE Computer Society Press, Los Alamitos, 1994, pp. 586-591.

8. L. Baresi, C. Bolchini, D. Sciuto. Software Methodologies for VHDL Code Static Analysis based on Flow Graphs. Proceedings of the European Design Automation Conference (EURO-DAC '94), IEEE Computer Society Press, Los Alamitos, 1994, pp. 406-411.

9. D.-C. Peixoto, D. Silva Jr., J.-M. Mata, C.-N. Coelho Jr., A.-O. Fernandes. Translation of hardware description languages to structured representation: a tool for digital system analysis. Proceedings of 13th Symposium on Computer Architecture and High Performance Computing (SBAC - PAD), 2001, Pirenуpolis.

10. VAUL. A VHDL Analyzer and Utility Library. http://www-dt.e-technick.uin-dortmund.de/~mvo/vaul/ University of Dortmund, Department of Electrical Engineering, AG SIV, 1994.

11. M. Zaki, Y. Mokhtari, S. Tahar. A Path Dependency Graph for Verilog Program Analysis. Proceedings of the IEEE Northeast Workshop on Circuits and Systems (NEWCAS'03), Montreal, 2003, pp. 109-112.

12. R. Floyd. Assigning meanings to programs. Proceedings of Symposia in Applied Mathematics, vol. 19, 1967, pp. 19-32.

13. N. Blanc, D. Kroening. Race Analysis for SystemC using Model Checking. ACM Transactions on Design Automation of Electronic Systems (TODAES), vol. 15 issue 3, 2010, pp. 356 – 363. doi: 10.1109/ICCAD.2008.4681598

14. IEEE Standard SystemC Language Reference Manual, 1666-2005, IEEE, 2003, 428 p.

15. E. Clarke, O. Grumberg, S. Jha, Y. Lu, H. Veith. Counterexample-Guided Abstraction Refinement. Computer Aided Verification, Lecture Notes in Computer Science vol. 1855, 2000, pp. 154-169.

16. Cadence SMV Symbolic Model Checker. http://www.kenmcmil.com/smv.html. Дата обращения: 02.03.2015.

17. SCOOT A Tool for the Static Analysis of SystemC. http://www.cprover.org/scoot/. Дата обращения: 04.03.2015.

18. L. Liu, S. Vasudevan. Scaling Input Stimulus Generation through Hybrid Static and Dynamic Analysis of RTL. ACM Transactions on Design Automation of Electronic Systems (TODAES), vol. 20 issue 1, 2014. doi:10.1145/2676549

19. P. Godefroid. Compositional dynamic test generation. Proceedings of the 34th Annual ACM Symposium on Principles of Programming Languages (SIGPLAN-SIGACT), 2007, pp. 47-54. doi: 10.1145/1190216.1190226

20. STAR. http://users.crhc.illinois.edu/liu187/. Дата обращения: 04.03.2015.

21. S. Hertz, D. Sheridan, S. Vasudevan. Mining Hardware Assertions With Guidance From

22. Static Analysis. Computer-Aided Design of Integrated Circuits and Systems, Transactions on IEEE, vol. 32, issue 6, 2013, pp. 952-965. doi: 10.1109/TCAD.2013.2241176

23. E. Clarke, O. Grumberg, D. Peled. Model checking. The MIT Press, 1999, 314 p.

24. GoldMine. http://goldmine.csl.illinois.edu/. Дата обращения: 04.03.2015.

25. Cadence Incisive. http://www.cadence.com/products/fv/iv_kit/pages/default.aspx. Дата обращения: 04.03.2015.

26. M. Weiser. Program slicing. IEEE Transactions on Software Engineering, vol. 10, issue 4, 1984, pp. 352–357.

27. E.M. Clarke, M. Fujita, S.P Rajan, T. Reps, S. Shankar. Program Slicing of Hardware Description Languages. Proceedings of the 10th IFIP WG 10.5 Advanced Research Working Conference on Correct Hardware Design and Verification Methods, pp. 298-302.

28. Codesurfer. http://www.grammatech.com/research/technologies/codesurfer. Дата обращения: 02.03.2015

29. T. Li, Y. Guo, S.-K. Li. Automatic Circuit Extractor for HDL Description Using Program Slicing. Journal of Computer Science and Technology vol. 19, issue 5, pp. 718-728. doi: 10.1007/BF02945599

30. C. Dawson, S.K. Pattanam, D. Roberts. The Verilog Procedural Interface for the Verilog Hardware Description Language. Proceedings of Verilog HDL Conference, 1996, pp. 17-23. doi: 10.1109/IVC.1996.496013

31. S. Vasudevan, E. A. Emerson, J. A. Abraham. Efficient Model Checking of Hardware Using Conditioned Slicing. Proceedings of the Fouth International Workshop on Automated Verification of Critical Systems (AVoCS), Vo1. 28, issue 6, 2005, pp. 279–294. doi: 10.1016/j.entcs.2005.04.017

32. M. Huth, M. Ryan. Logic in Computer Science: Modelling and Reasoning about Systems. Cambridge University Press, New York, 2004, 440 p.

33. A. Tepurov, V. Tihhomirov, M. Jenihhin, J. Raik, G. Bartsch, J.H. Meza Escobar, H. Wuttke. Localization of Bugs in Processor Designs Using ZamiaCAD Framework. Proceedings of 13th International Workshop on Microprocessor Test and Verification (MTV), 2012, pp. 41-47.

34. ZamiaCAD. http://zamiacad.sourceforge.net/web/. Дата обращения: 06.03.2015.

35. J. Hopcroft, R. Motwani, J. Ullman. Introduction to Automata Theory: Languages, and Computation. Pearson/Addison Wesley, 2007, 535 p.

36. M. Yuang. Survey of protocol verification techniques based on finite state machine models. Proceedings of the Computer Networking Symposium, 1988, pp. 164-172.

37. R. Obermaisser, C. El-Salloum, B. Huber, H. Kopetz. Modeling and Verification of Distributed Real-Time Systems using Periodic Finite State Machines. Journal of Computer Systems Science & Engineering, vol. 22, No. 6, 2007.

38. А.С. Камкин. Метод формальной спецификации аппаратуры с конвейерной организацией и его приложение к задачам функционального тестирования. Труды ИСП РАН, Вып. 16, 2009 г., стр. 107-128.

39. T.-H. Wang, T. Edsall. Practical FSM Analysis for Verilog. Proceedings of Verilog HDL Conference and VHDL International Users Forum, 1998, pp. 52-58. doi:10.1109/IVC.1998.660680

40. A. Gill. Introduction to the Theory of Finite-state Machines. McGraw-Hill, 1962, 207 p.

41. J.-C. Giomi. Method of Extracting Implicit Sequential Behavior from Hardware Description Languages. 5.774.370, USA, 531.996, 18.09.1995, 30.06.1998, pp. 1-44.

42. C.-N. Liu, J.-Y. Jou. A FSM Extractor for HDL Description at RTL Level. Proceedings of the 2nd International Symposium on Quality Electronic Design, 2001, p. 372.

43. M. E. J. Gilford, G. N. Walker, J. L. Tredinnick, M. W. P. Dane, M. J. Reynolds. Recognition of a State Machine in High-Level Integrated Circuit Description Language Code. 7.152.214 B2, USA, 10/736.967, 15.12.2003, 19.12.2006, pp. 1-32.

44. W. Song, J. Garside. Automatic Controller Detection for Large Scale RTL Designs. Euromicro Conference on Digital System Design (DSD), Los Alamitos, CA. 2013, pp. 844-851. doi: 10.1109/DSD.2013.94

45. G. D. Micheli. Synthesis and Optimization of Digital Circuits. McGraw-Hill Science/Engineering/Math, 1994, 576 p.

46. Asynchronous Verilog Synthesizer. http://wsong83.github.io/index.html. Дата обращения: 05.03.2015.

47. A. Höller, C. Preschern, C. Steger, C. Kreiner, A. Krieg, H. Bock, J. Haid. Automatized High-Level Evaluation of Security Properties for RTL Hardware Designs. Proceedings of the Workshop on Embedded Systems Security, No. 6, 2013, pp. 1-8. Doi:10.1145/2527317.2527323

48. NuSMV. http://nusmv.fbk.eu/. Дата обращения: 05.03.2015.

49. K.-T. Cheng, A.S. Krishnakumar. Automatic Generation of Functional Vectors Using the Extended Finite State Machine Model. ACM Transactions on Design Automation of Electronic Systems (TODAES), vol. 1 issue 1, 1996, pp. 57-79. doi: 10.1145/225871.225880

50. J-Y. Jou, S. Rothweiler, R. Ernst, S. Sutarwala, A. Prabhu. BESTMAP: Behavioral Synthesis from C. In International Workshop on Logic Synthesis (Research Triangle Park, NC, May), 1998.

51. G. D. Guglielmo, L. D. Guglielmo, F. Fummi, G. Pravadelli. Efficient Generation of Stimuli for Functional Verification by Backjumping Across Extended FSMs. Journal of Electronic Testing, vol. 27, issue 2, 2011, pp. 137-162. Doi: 10.1007/s10836-011-5209-8

52. G. Di Guglielmo, F. Fummi, G. Pravadelli, S. Soffia, M. Roveri. Semi-formal functional verification by EFSM traversing via NuSMV. IEEE International High Level Design Validation and Test Workshop (HLDVT), 2010, pp. 58-65. doi: 10.1109/HLDVT.2010.5496660

53. D. Kim, M. Ciesielski, K. Shim, S. Yang. Temporal Parallel Simulation: A Fast Gate-level HDL Simulation Using Higher Level Models. Proceedings of the Conference on Design, Automation and Test in Europe (DATE), 2011. doi: 10.1109/DATE.2011.5763251

54. N. Bombieri, F. Fummi, G. Pravadelli. Automatic Abstraction of RTL IPs into Equivalent TLM Descriptions. IEEE Transactions on Computers, vol. 60, issue 12, 2011, pp. 1730-1743. doi: 10.1109/TC.2010.187

55. OSCI TLM-2.0. http://www.accellera.org/resources/videos/tlm20andsubset/. Дата создания: 22.02.2010.

56. HIFSuite. https://www.edalab.it/. Дата обращения: 05.05.2015.

57. А.С. Камкин, С.А. Смолов. Метод извлечения EFSM-моделей из HDL-описаний:

58. применение к функциональной верификации. Сборник трудов конференции «Проблемы разработки перспективных микро- и наноэлектронных систем» под общ. ред. академика РАН А.Л. Стемпковского, часть 2, 2014, стр. 113-118.

59. Brandt J., Gemünde M., Schneider K., Shukla S., Talpin J.-P. Integrating System Descriptions by Clocked Guarded Actions. Forum on Design Languages, 2011, pp. 1-8.

60. Retrascope. http://forge.ispras.ru/projects/retrascope/. Дата обращения: 05.03.2015.

61. D. Moundanos, J.A. Abraham, Y.V. Hoskote. Abstraction Techniques for Validation Coverage Analysis and Test Generation. IEEE Transactions on Computers, IEEE, 1998, vol. 47, issue 1, pp. 2-14. doi:10.1109/12.656068

62. T.M. Niermann, J.H. Patel. HITEC: A Test Generation Package for Sequential Circuits. Proceedings of International European Design Automation Conference (EDAC), 1996, pp. 875-884. doi:10.1109/EDAC.1991.206393

63. C.-N. Jimmy Liu, J.-Y. Jou. An Efficient Functional Coverage Test for HDL Descriptions at RTL. Proceedings of International Conference on Computer Design (ICCD), Austin, TX, 1999, pp. 325-327. doi:10.1109/ICCD.1999.808561