Abstract
Increasing complexity of both hardware and software in System-on-Chip (SoC) designs coupled with time-to-market pressure create a critical need to develop efficient functional validation techniques. To achieve the required functional coverage goal, billions of random or constrained-random tests are used during simulation of today’s SoC designs. Various studies suggest that functional validation is a major bottleneck in SoC design—up to 70 % of design development efforts are spent during validation. To reduce the overall validation effort, this book focuses on system-level validation using efficient directed tests. This chapter first highlights the increasing design and validation complexity of SoC designs. Next, it studies the existing validation techniques. Then, we discuss the challenges as well as opportunities associated with system-level validation. Finally, we present a high-level validation framework that can drastically reduce the overall validation effort.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Notes
- 1.
The Pentium FDIV bug was the most infamous one of the Intel microprocessor bugs. Due to an error in a lookup table, certain floating point division operations would produce incorrect results.
- 2.
On June 4, 1996 an unmanned Ariane 5 rocket launched by the European Space Agency exploded a few seconds after its liftoff.
- 3.
“Validation” is performed at different abstraction levels to uncover two types of faults: specification flaws and implementation bugs. Formal verification refers to the use of formal methods to ensure that the implementation satisfies the specification. In this book, the term “verification” refers to the use of both simulation-based validation and formal methods to detect implementation bugs (errors). Please note that the terms “validation” and “verification” have different usage and interpretation in different domains.
- 4.
In the ESL Design and Verification book [2], the term ESL is defined as: “the utilization of appropriate abstractions in order to increase comprehension about a system, and to enhance the probability of a successful implementation of functionality in a cost-effective manner.”.
- 5.
Depending on application domains and abstraction levels, different types of specification languages may be applicable. For example, architecture description languages (ADL) [9] are very popular in early exploration and validation of processor-based SoCs.
- 6.
The size of the state space grows exponentially with the number of state variables of the system.
- 7.
The input space (all possible input sequences) can be prohibitively large for complex designs with large number of inputs.
References
Wolf W, Jerraya A, Martin G (2008) Multiprocessor system-on-chip (MPSoC) technology. IEEE Trans Comput Aided Des Integr Circuits Syst (TCAD) 27(10):1701–1713
Bailey B, Martin G, Piziali A (2007) ESL design and verification: a prescription for electronic system level methodology. Morgan Kaufmann/Elsevier, Burlington
Open SystemC Initiative (OSCI) (2006) SystemC. http://www.systemc.org
Berry G, Gonthier G (1992) The esterel synchronous programming language: design, semantics, implementation. Sci Comput Program 19(2):87–152
SysML. http://www.sysml.org/
Peterson J (1981) Petri nets theory and the modeling of systems. Prentice-Hall, Englewood Cliffs
Mishra P, Dutt N (2008) Processor description languages: applications and methodlogies. Morgan Kaufmann, San Fransisco
Cai L, Gajski D (2003) Transaction level modeling: an overview. In: Proceedings of international conference on hardware/software codesign and system, synthesis (CODES\(+\)ISSS), pp 19–24
Rose A, Swan S, Pierce J, Fernandez J (2005) Transaction level modeling in systemC. http://www.systemc.org
Object Management Group (2007) UML superstructure V2.1.2. http://www.omg.org/docs/formal/07-11-02.pdf. Accessed Nov 2007
Schutten R, Fitzpatrick T (2003) Design for verification methodology allows silicon success. EETIMES, Number: 16500856
Bentley B (2002) High level validation of next generation microprocessors. In: Proceedings of high level design validation and test (HLDVT), pp 31–35
Schubert T (2003) High level formal verification of next generation microprocessors. In: Proceedings of design automation conference (DAC), pp 1–6
Fine S, Ziv A (2003) Coverage directed test generation for functional verification using Bayesian networks. In: Proceedings of design automation conference (DAC), pp 286–291
Bryant R (1991) A methodology for hardware verification based on logic simulation. J ACM 38(2):299–328
Adir A, Asaf S, Fournier L, Jaeger I, Peled O (2007) A framework for the validation of processor architecture compliance. In: Proceedings of design automation conference (DAC), pp 902–905
Ezer S, Johnson S (2005) Smart diagnostics for configurable processor verification. In: Proceedings of design automation conference (DAC), pp 789–794
Puig-Medina M, Ezer G, Konas P (2000) Verification of configurable processor cores. In: Proceedings of design automation conference (DAC), pp 426–431
Roy A, Panda S, Kumar R, Chakrabarti P (2005) A framework for systematic validation and debugging of pipeline simulators. ACM Trans Des Autom Electron Syst (TODAES) 10(3):462–491
Adir A, Almog E, Fournier L, Marcus E, Rimon M, Vinov M, Ziv A (2004) Genesys-Pro: innovations in test program generation for functional processor verification. IEEE Des Test Comput 21(2):84–93
Shimizu K, Gupta S, Koyama T, Omizo T, Abdulhafiz J, McConville L, Swanson T (2006) Verification of the cell broadband engine processor. In: Proceedings of design automation conference (DAC), pp 338–343
Koo H, Mishra P (2006) Functional coverage-driven test generation for microprocessor verification. In: Proceedings of US-Korea conference (UKC), pp 19–24
Mishra P, Dutt N (2005) Functional verification of programmable embedded architectures: a top-down approach. Springer, Berlin
Camurati P, Prinetto P (1988) Formal verification of hardware correctness: introduction and survey of current research. IEEE Comput 21(7):8–19
Kern C, Greenstreet M (1999) Formal verification in hardware design: a survey. ACM Trans Des Autom Electron Syst (TODAES) 4(2):123–193
McMillan K (1993) Symbolic model checking: an approach to the state explosion problem. Kluwer Academic Publishers, Boston
Clarke E, Grumberg O, Peled D (2000) Model checking. The MIT press, Cambridge
Srivas M, Bickford M (1990) Formal verification of a pipelined microprocessor. IEEE Softw 7(5):52–64
Wilding M, Greve D, Hardin D (2001) Efficient simulation of formal processor models. Formal Methods Syst Des 18(3):233–248
Kuehlmann A, Eijk C (2001) Combinational and sequential equivalence checking. In: Logic synthesis and verification, Kluwer Academic Publishers, Norwell
Clarke E, Biere A, Ramimi R, Zhu Y (2001) Bounded model checking using satisfiability solving. Formal Methods Syst Des 19(1):7–34
Prasad M, Biere A, Gupta A (2005) A survey of recent advances in SAT-based formal verification. Int J Softw Tools Technol Transfer (STTT) 7(2):156–173
Ammann P, Black P, Majurski W (1998) Using model checking to generate tests from specifications. In: Proceedings of international conference on formal engineering methods (ICFEM), pp 46–54
Foster H, Krolnik A, Lacey D (2004) Assertion-based design, 2nd edn. Kluwer Academic Publishers, Boston
PSL working group (2005) Property Specification Language. http://www.eda.org/ieee-1850/
SVA committee (2004) SystemVerilog Assertion. http://www.eda.org/sv-ac/
Author information
Authors and Affiliations
Corresponding author
Rights and permissions
Copyright information
© 2013 Springer Science+Business Media New York
About this chapter
Cite this chapter
Chen, M., Qin, X., Koo, HM., Mishra, P. (2013). Introduction. In: System-Level Validation. Springer, New York, NY. https://doi.org/10.1007/978-1-4614-1359-2_1
Download citation
DOI: https://doi.org/10.1007/978-1-4614-1359-2_1
Published:
Publisher Name: Springer, New York, NY
Print ISBN: 978-1-4614-1358-5
Online ISBN: 978-1-4614-1359-2
eBook Packages: EngineeringEngineering (R0)