A Survey of Methods for Model Extraction from HDL Descriptions

In this paper a survey of existing methods of model extraction from hardware system descriptions written in Hardware Description Languages (like Verilog and VHDL) is presented. There are many tasks in hardware and software design where models are applied. The most actual tasks that are mentioned in this paper are: code optimization, logical synthesis optimization, model abstraction, and functional verification. The model categories that are mostly described here are flow or dependency graph models and automata models. As for flow graphs or dependency graphs, the methods of program slices extraction are described in details. Program slices can be characterized as suitable enough for directed test generation. Almost all the described automata models are finite state machine models and extended finite state machine models and so methods of such models extraction are the most popular for logical synthesis optimization and for functional test generation. The tests that can be generated from automata models shows high coverage of the target description. The key problems of existing model extraction methods are: the complexity of an application to industrial hardware descriptions (because of their complex structure), lack of automation (sometimes the hardware designer’s knowledge is needed), the absence of open-source implementations. Also it is an actual task to create extendible frameworks for integration of different model extraction and analysis methods. Such framework can help in development of effective hybrid methods for hardware synthesis and verification.

hardware description languages, model extraction, static analysis, code optimization, model abstraction, logical synthesis, functional verification, program slicing, flow graphs, dependency graphs, finite state machines, extended finite state machines

1. 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

2. A. Kamkin, A. Kotsynyak, S. Smolov, A. Sortov, A. Tatarnikov, M. Chupilko. Sredstva funktsionalnoy verifikatsii mikroprotsessorov [Tools for Functional Verification of Microprocessors]. Trudy ISP RAN [The Proceedings of ISP RAS], vol. 26, issue 1, 2014, pp. 149-200. doi: 10.15514/ISPRAS-2014-26(1)-5

3. 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

4. Statistical Analysis of Floating Point Flaw: Intel White Paper Section 3. http://www.intel.com/support/processors/pentium/sb/CS-013007.htm. Access date: 08.07.2004.

5. OSCI TLM-2.0. http://www.accellera.org/resources/videos/tlm20andsubset/. Access date: 22.02.2010.

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

7. HIFSuite. https://www.edalab.it/. Access date: 05.05.2015.

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

9. A. Kamkin, S. Smolov. The method of EFSM extraction from HDL: application to functional verification. Proceedings of the conference on Problems of Perspective Micro- and Nanoelectronic Systems Development, Part II, 2014, pp. 113-118.

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

11. 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.

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

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

14. 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.

15. 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

16. 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.

17. 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

18. 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.

19. 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

20. 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.

21. 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.

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

23. 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

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

25. 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.

26. Cadence SMV Symbolic Model Checker. http://www.kenmcmil.com/smv.html. Access date: 02.03.2015.

27. SCOOT A Tool for the Static Analysis of SystemC. http://www.cprover.org/scoot/. Access date: 04.03.2015.

28. 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

29. 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

30. STAR. http://users.crhc.illinois.edu/liu187/. Access date: 04.03.2015.

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

32. 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

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

34. GoldMine. http://goldmine.csl.illinois.edu/. Access date: 04.03.2015.

35. Cadence Incisive. http://www.cadence.com/products/fv/iv_kit/pages/default.aspx. Access date: 04.03.2015.

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

37. 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.

38. Codesurfer. http://www.grammatech.com/research/technologies/codesurfer. Access date: 02.03.2015

39. 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

40. 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

41. 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

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

43. 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.

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

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

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

47. 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.

48. A. Kamkin. Metod formalnoy spetsifikatsii apparaturyi s konveyernoy organizatsiey i ego prilozhenie k zadacham funktsionalnogo testirovaniya [A Method of Pipelined Hardware Specification and its Application to Functional Verification]. Trudy ISP RAN [The Proceedings of ISP RAS], vol. 16, 2009, pp. 107-128 (in Russian).

49. 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

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

51. 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.

52. 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.

53. 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.

54. 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

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

56. Asynchronous Verilog Synthesizer. http://wsong83.github.io/index.html. Access date: 05.03.2015.

57. 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

58. NuSMV. http://nusmv.fbk.eu/. Access date: 05.03.2015.

59. 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

60. 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.

61. 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

62. 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

63. 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

64. 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

65. OSCI TLM-2.0. http://www.accellera.org/resources/videos/tlm20andsubset/. Access date: 22.02.2010.

66. HIFSuite. https://www.edalab.it/. Access date: 05.05.2015.

67. A. Kamkin, S. Smolov. The method of EFSM extraction from HDL: application to functional verification. Proceedings of the conference on Problems of Perspective Micro- and Nanoelectronic Systems Development, Part II, 2014, pp. 113-118.

68. 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.

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

70. 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

71. 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

72. 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