SystemVerilog Assertions: Past, Present, and Future SVA Standardization Experience Doron Bustan, Dmitry Korchemny, Erik Seligman and Jin Yang Intel Corporation added means to specify coverage, testbench, and Editors’ notes: assertions. The part of SysThis paper provides insight into the development of System Verilog temVerilog for assertion Assertions standardization efforts. Specifically it covers the evolution from specification and modelAccellera 3.1a version to its current state of standardization (the upcoming ing is called SystemVerilog SVA2012 release). Insight into the new features, changes and the reasons for the same exposes users of SVA to the direction the standard is evolving. Assertions (SVA). VShishpal S. Rawat, Intel, and Sumit DasGupta Si2 Unlike many other assertion specification languages SVA is not written h DURING THE LAST decade assertion-based in the form of interpreted comments, but rather is a verification (ABV) proved itself to be an efficient native part of SystemVerilog. This native integration verification methodology based on instrumenting enables defining a clear and consistent semantics the design with assertions. These assertions are for both simulation and formal verification. The checked by methods including simulation, emula- standardization of SVA makes it possible to integrate tion, and formal verification. Assertions also docu- tools from different vendors or to replace one tool ment the design and play the role of executable with another to achieve a similar functionality. This comments. To address the needs of ABV, many standardization started in Accellera and then moved assertion specification languages were created: to the P1800 project of IEEE. The authors of this Sugar [1], ForSpec [2], CBV [3], etc. The kernel of paper have been deeply involved in the various most assertion languages is declarative, which makes stages of the SVA standardization process. In this paper, we describe different aspects of SVA them concise and raises their level of abstraction. Because of their different nature, early assertion standardization. Sections I and II briefly overview specification languages were separate from hard- the history of SVA standardization. Section III deware design languages (such as Verilog and VHDL). scribes the current standardization effort. Section IV This situation changed with the introduction of describes an important use caseVthe specification SystemVerilog [4], the extension of Verilog that of an internal Intel bus. Section V looks at the reciprocal influence of SVA standard development and academic research. Section VI discusses a numDigital Object Identifier 10.1109/MDT.2012.2183336 ber of major problems that have yet to be addressed Date of publication: 09 January 2012; date of current version by SVA standardization. 26 June 2012. March/April 2012 Copublished by the IEEE CEDA, IEEE CASS, and IEEE SSCS 0740-7475/12/$31.00 B 2012 IEEE 23 EDA Industry Standards The beginnings of SVA standardization From SVA2005 to SVA2009 SVA was first announced as part of the SystemVerilog 3.1a standard [4] by the Accellera EDA standards committee in 2003. It was announced together with PSL as a standard specification language, but in contrast to PSL, it was designed to be closely coupled with the SystemVerilog and had an emphasis on dynamic verification [5]. SVA3.1a has two kinds of assertions: concurrent and immediate. Immediate assertions are nontemporal and are evaluated similarly to design code. In particular, they are sensitive to the order of events inside a single time step. Concurrent assertions have linear semantics, and may specify expressions that span multiple time steps. In linear semantics time progress is considered to be a trace, rather than a tree as in branching semantics. Similarly to PSL, SVA has a layered structure: Booleans, regular expressions (sequences), properties, and statements. This layered structure, which includes: concatenation, union, Kleene closure, on the sequence layer and not, or, and implication operators on the property layer, gives SVA3.1a full !-regular expressibility [2].1 SVA3.1a ties its Boolean layer to the design code of SystemVerilog by sharing the same Boolean expressions and defines the time regions where these expressions are evaluated. SystemVerilog’s clocking is used in SVA3.1a to determine time progression. Beyond the language skeleton described above, there are many more operators that make the language more usable. Among other notable features are local variables for data sampling and manipulation, and recursive properties. These features increased the usability of SVA3.1a but made it hard to formalize. Indeed, SVA3.1a suffered from conflicts, gaps, and redundant restrictions. In 2005, SystemVerilog 2005 was announced as the IEEE 1800 standard. SVA2005 had a set of features similar to those of SVA3.1a, but many of the features, such as use of local variables in expressions, arguments passing, operator precedence, restrictions on recursive properties, etc., were better defined. Nevertheless, there were still weaknesses in the language definition, including gaps in its formal semantics, as described in the following section. The release of the SVA2005 standard was a major milestone for design verification. Industry development teams immediately wanted to begin taking advantage of the new language. However, parts of the language had usability problems, and as a result local dialects emerged at several companies. For example, Intel had a local dialect with improved semantics for immediate assertions. As teams gained experience with the language, they identified a number of flaws that limited the effectiveness of SVA in common design and validation scenarios. We worked with the IEEE P1800 committee to define solutions for these flaws for the next standard. The major improvements are described briefly below. For a more detailed description, refer to [6]. 1 Note that expressibility is proven over ForSpec, which has similar operators, with the syntactic difference that the implication operator is called triggers. 24 Deferred assertions SystemVerilog allows procedures to execute multiple times within a single time step, to allow relaxation of changing values. In such a multiplyexecuted procedure, immediate assertions may be checked during each execution, sometimes reporting failures on intermediate values. To solve this problem, a new kind of immediate assertion, called a deferred assertion, was introduced. When a deferred assertion fails, the report of its failure is put in a queue rather than being reported immediately. If the same procedure is executed again, current assertion reports are flushed, and only the new execution of the assertions will take effect. Improved procedural concurrent assertions It is often useful to include a concurrent assertion inside procedural code. In SVA2005, this was permitted in some types of procedures, but defined through a set of syntactical transformations: the assertion was effectively treated as if outside the procedure, but with any enclosing procedure controls or conditionals integrated into the logic of the assertion. For example, always @ðposedge clkÞ if (en) c: cover property (a); became c: cover property (@(posedge clk) en j
> a); IEEE Design & Test of Computers In general, this rewriting could cause unexpected behavior. Most importantly, it could cause incorrect partial execution of assertions in nonexecuted locations in a procedure. In the particular example above, while the original cover property in the code looks like it should not execute in cases where en == 0, the transformed property will start a cover attempt and report it (vacuously) successful, since the property is true. In the revised 2009 standard, concurrent assertions in procedures remain a part of their procedure, and are placed in an execution queue when visited during procedural execution. The assertion is removed from the queue and evaluated at a time that depends on its clocking event. This definition is much more consistent with simulation, provides a natural definition for concurrent assertions in procedural loops, and provides behavior that correctly prevents any attempts of an assertion when it is in a nonexecuted location in procedural code. Strong and weak properties When describing properties that span infinite time it is important to define their behavior in case their clock stops ticking. In particular, when an assertion is used in simulation, its clock will always stop ticking at the end of simulation. In SVA2005 this definition was unintuitive and inflexible. In SVA2009 it is possible to specify user intent explicitly, and the defaults are intuitive. For example, weak and strong qualifiers were introduced for sequential properties. Given a sequence s, a sequential property strong(s) is true iff there is a nonempty match of the sequence s. A sequential property weak(s) is true iff there is no finite prefix of any computation witnessing a mismatch of s. Look at this simple example: a1: assert property (@(posedge clk) req j
> ##5 ack); The assertion a1 requires that every req should be followed by an ack after exactly 5 clock ticks. Consider a computation where a request occurs at its last clock tick. Should the assertion pass or fail? There is no clear answer to that; some systems may allow turning off the clock in the middle of a transaction, others may not. Furthermore, whether or not a test may terminate in the middle of a transaction could be a matter of methodology. March/April 2012 On the other hand, in a syntactically similar example: a2: assert property (@(posedge clk) req j
> ##[1:$] ack); weak semantics makes the assertion a2 trivially true. SVA2005, does not provide a way of choosing between the semantics. On infinite traces both assertions fail when the clock stops; on finite traces, both are considered pending. In SVA2009 assertion, a2 will pass unless the strong operator is applied to the suffix. Linear Temporal Logic (LTL) and abort constructs Engineers involved in formal verification have experience specifying properties using LTL, a wellknown logical language [2], [7], [8] that provides a basic set of operators including always, eventually, nexttime, and until. Frequently, a property simple to write in LTL would require a very convoluted definition in SVA2005. For example, the simple LTL statement eventually always !rst would have to be written in SVA2005 as: not (##[1:$] !rst j
> ##[1:$] rst)) Starting with SVA2009, strong and weak versions (in their bounded and unbounded forms) of the always, eventually, nexttime, and until2 operators have become directly available in the language. SVA2009 also added flexible abort operators preempting a property attempt execution when some Boolean condition holds. Global clocking In many cases, such as checking the stability of a local clock, users want to be able to enforce a condition at every time step. This can be a challenge in SVA2005, since all assertion clocking must be derived from a local clock signal. Thus, if we are trying to check the stability of the clock signal itself, we have no time points to refer to other than its own edges. SVA2009 introduces the concept of a global clock. The global clock can be declared with a global clocking statement and is intended to represent the finest-grained clock in a design. Even if a unit 2 There is no bounded form for the until operator in SVA. 25 EDA Industry Standards does not have any local signal that corresponds to this global clock, it can use a set of system functions to measure time in reference to it. Let expressions SVA2005 provided the useful property construct to enable modular, reusable concurrent assertions. This enabled properties to reuse other properties in building complex assertions. However, there was no corresponding container for immediate assertions. It was possible to use macros, but because these are expanded during preprocessing and not displayed as real language objects by most debuggers, this method caused many difficulties for users. SVA2009 added the new concept of let expressions. While similar to a macro in that it allows the definition of some symbol to represent a more complex expression, a let expression is a scoped object whose expansion is not considered part of preprocessing. Thus let expressions can be used as building blocks for immediate assertions in the same way properties are used to build concurrent assertions. Let expressions (and checkers) also lead to cleaner RTL by enabling a clear distinction between design and instrumentation code, and eliminate the need for many ‘ifdef statements previously used for this purpose. Checker constructs Having generic, flexible verification librariesV centrally maintained sets of packaged assertions and modeling code representing common situations seen in designsVis critical for ABV, and SVA provides a good infrastructure for this [9]. However, SVA2005 had a number of limitations affecting verification libraries. Most notably, the existing SystemVerilog containers were not always satisfactory for packaging sets of assertions and modeling code: the limited nature of the property construct made it hard to describe a set of related assertions and associated behavioral modeling. Modules and interfaces can package several assertions and modeling code, but they have many limitations: they require all arguments to be typed; they cannot accept arguments of the type sequence, property, or event; they cannot be instantiated in procedural code; they cannot infer clocks and resets from their context; and they have no concept of free variable support. 26 SVA2009 has a new container, a checker, designed as a flexible library building block that can contain assertions, modeling code, and other useful constructs [6]. Some notable features of checkers are the ability to take simple signals, sequences, properties, or events as inputs, the ability to be instantiated at the top level of a module or in procedural code, system functions to infer the clock and reset from its instantiation context, and the ability to include both assertions and modeling code. They also supply additional functionality useful in formal modeling, such as free (nondeterministic) variable support. Because of these features checkers are suitable to be containers for Verification IP (VIP). The impact of checkers (and the other features described in this section) on library development is clearly visible when comparing the SVA Checker Library [10], recently donated by Intel to Accellera, to the standard Open Verification Library (OVL) [11], which is based on modules and other SVA2005 constructs. Table 1 illustrates the differences in the two approaches. From SVA2009 to SVA2012 Work on the emerging standard is focused on refining the major enhancements introduced in SVA2009 and on addressing usability problems. Also, initial steps have been undertaken to support Analog and Mixed Signal (AMS) assertions. The features described in this section are not guaranteed to become part of the emerging standard. Checker usability Checkers introduced in SVA 2009 were intended to be building blocks for VIP. However, the checker modeling capability was limited: let expressions, functions, and edge-sensitive always procedures with nonblocking assignments only. Though these capabilities are sufficient for building VIP, the available modeling style is very different from the style VIP developers are used to. This resulted in slow acceptance of checkers for large VIP blocks. It was therefore important to introduce familiar modeling constructs, such as continuous assignments, blocking assignments, different kinds of always procedures, and procedural conditional and looping statements. This task is far from being trivial, considering that the simulation semantics in checkers differs from that of the modules. It requires reconciling free variable support, expression sampling, IEEE Design & Test of Computers and deferred assertions in checkers. At the price of a number of restrictions, it became possible to elaborate a proposal that handles all these issues consistently. Another important problem was a lack of output ports in checkersVthe checkers were pure observers. This fact is a serious obstacle to modularity, and it prevents shaping large VIP blocks as checkers: modules cannot be instantiated in checkers, whereas checkers cannot return computation results to their caller. Therefore it was decided to allow output ports in checkers. This feature also allows using checkers as generators. Taking advantage of nondeterministic modeling based on free variables, checkers may act as stimuli generators for a device under test (DUT), thus providing an attractive alternative to programs, especially for formal verification environments. Checker output ports are also important for capturing the outcome of an assertion (success or failure) and feeding it to scan latches, thus opening the door to automatic assertion synthesis on the silicon. Assertion system functions Assertion system functions such as $onehot (checking 1-hot encoding of a bit vector) belong to the Boolean layer of SVA that was believed to be well-defined. However, massive SVA usage revealed two critical issues with these functions: their behavior is not always satisfactory when their argument contains undefined values X or Z, and it is not clearly defined whether their argument can be of an unpacked type. To address these problems the definition was clarified to allow unpacked data types, and the new function $countbits was introduced to flexibly count the occurrences of any known or unknown bit values. Deferred assertions Deferred assertions introduced in SVA2009 solved the problem of glitch sensitivity in all cases except when the same assertion contains a mix of signals from the DUTand the testbench. To cope with this issue a different flavor of deferred assertions was suggested, one that matures after all value changes in a time step, from both DUTs and testbenches, are complete. Both flavors of deferred assertions are required because the action blocks of the new assertions may only be used to issue messages, but not to modify design or testbench data. March/April 2012 Table 1 OVL versus SVA checker library Assertion controllability SVA has the ability to switch assertions on and off using several system tasks such as $asserton and $assertkill. These capabilities are not sufficient for assertion management in large systems with power control that requires switching groups of assertions. For example, if there is a need to switch off all the assertions in some module hierarchy except those that appear in specific submodules, killing all assertions in the entire hierarchy and then reenabling them in the specific submodules does not work properly because the active assertion attempts have been stopped. To cope with this problem and to allow more finely-grained assertion management, a new system task, $assertcontrol, has been introduced. Global clocking The global clocking construct added in SVA2009, providing a model reference clock, works well for formal verification, but can result in a significant performance penalty in simulation. In practice, for different clock domains it is possible to define different reference clocks which are much slower than the reference clock for the entire system. Therefore it was proposed to allow hierarchical specification of reference clocks. 27 EDA Industry Standards Towards AMS assertions Since analog and mixed signal (AMS) validation is becoming more and more important, it has become necessary to have assertions validating AMS system behavior. Defining and incorporating AMS assertions into SVA requires merging VerilogAMS with SystemVerilog as a prerequisite. One key obstacle to AMS functionality was the requirement in SVA2009 that no real number data values be used in assertion expressions. As a first step towards allowing AMS assertions, this requirement was loosened to allow subexpressions be of a real data type as long as top-level assertion expressions evaluate to a Boolean. Use case: Intel IOSF By seamlessly combining declarative assertions with the behavioral modeling of SystemVerilog, SVA provides a powerful language for building complex VIPs. Here we share our experience in developing an SVA-based VIP for IOSF, an Intel on-chip system fabric standard for connecting various internal and third-party IPs, analogous to the AMBA interconnection used in the ARM community. It is scalable, supports multicore operation, and maintains PCI order for software compatibility [12]. IOSF spans multiple layers, from signal level protocols all the way up to message and transaction level protocols. VIP development methodology Given the central role of IOSF in the reuse of modular IPs and fast system integration, it is critical to ensure that: 1) the IOSF standard is correct, complete and consistent, and 2) that IPs are compliant with the IOSF standard. To achieve this challenging goal, we developed a large-scale SVA-based VIP, CompMon, that implements all the compliance rules annotated in the IOSF standard [13]. We formally verified CompMon against a set of carefully chosen properties, also written in SVA, in order to achieve a high level of confidence that the set of compliant rules it implements and the specification itself are close to the ideal of being complete, correct, and consistent. The verified VIP then became a golden compliance standard that every IP must validate against. To maximize the reuse of the VIP in different validation flows such as simulation, formal verification, and emulation, we implemented CompMon using a synthesizable subset of SystemVerilog with assertions. We also chose to stay with SVA2005 at the 28 time of the development to ensure that the VIP can work with a wide range of vendor and in-house tools. This strategy allowed us to quickly deploy the VIP to all SOC projects in Intel. As more and more tools start to support SVA2009 features, we believe that it is worthwhile to gradually upgrade the VIP to take advantage of these features. In the other direction, the learning we gained in developing and deploying CompMon has helped us identify new language requirements which have influenced the standard. A good example is the SVA checker library mentioned earlier in the paper. Usage and results Using CompMon to check for interface compliance is as simple as instantiating a SystemVerilog module which monitors the interface wires between the IOSF fabric and a connected IP (shown in Figure 1). Since its creation, CompMon has been deployed in seven different Intel design projects, spanning both Soft IP providers and SOC CPU designs. Since then, 18 issues have been found in the validation collaterals and 15 late compliance violations have been discovered in IP designs. All implementations claiming compliance with our protocols are now required to include CompMon as part of their test environment and to document how they check for the few rules that require IP-specific information. A design is considered compliant if it passes IP-specific functional testing without violating any of the rules. While waivers might be granted, some of the assertions will require coverage to ensure interoperability. If an IP exits functional testing without exercising these assertions, a hole in functional testing is revealed that must be filled by additional testing. SVA standardization and academic research The use of logic to describe and verify systems has a long history in academic research, and is beyond the scope of this paper. For a broad review of the history of logic and verification see [14]. SVA and PSL have not only relied on academic research, but inspired more academic research as well. Coming up with an industrial standard requires a new way of thinking. The specification language was judged not only by traditional academic parameters such as expressibility, complexity of the IEEE Design & Test of Computers Figure 1. RTL compliance checking. decision problem, and modularity, but also by ease of use, ease of debug, similarity to design languages, and adaptability to dynamic verification. Publications such as [1], [2], [15] were part of defining what the industry needs: linear vs. branching semantics, clock and reset handling, filling the gap between LTL and full !-regular language. Being able to have properties with consistent semantics for both finite and infinite computations required special care [16], [17]. Once the standards were announced and used, more practical issues arose. The high complexity of model-checking SVA [18] gave rise to several publications on efficient model-checking of a useful fragment of SVA [19]–[22] that can be used for both model checking and dynamic verification. Other efforts aimed at debugging SVA [23] using hybrid approaches [24] that combine static and dynamic methods, and extracting coverage and vacuity conditions from SVA assertions [25]. there are still several problems that remain due to the limited bandwidth that is available for the standardization effort. Coverage One important problem relates to the area of coverage, which is split between SVA and SVTB (SystemVerilog Test Bench). The root of this problem is that these parts of coverage have been owned, since the beginning of SVA standardization, by two different subcommittees. The syntax and the simulation semantics have nothing in common, and a large amount of manual work is required to combine temporal information with combinational coverage constructs. It is therefore important to define a tighter integration between these two parts of SystemVerilog coverage and to create temporal covergroups that combine the concepts of SVTB covergroups and SVA sequences, thereby facilitating compact definition of complex coverage spaces. Open problems Although many important problems have been solved in the course of the history of SVA standardization, or are in the process of being solved now, March/April 2012 AMS assertions Another large and important problem is support of AMS assertions, which requires, as a necessary 29 EDA Industry Standards preliminary condition, integration of Verilog-AMS into SystemVerilog. The first step towards AMS assertions support, the enabling of real data types in SVA, is being taken as part of the current standardization effort. A more challenging task is to define temporal operators based on a continuous time model, as opposed to the discrete time model used in current SVA assertions. UVM integration UVM methodology [26] leverages many aspects of object-oriented programming. Currently, SVA is poorly integrated with the object-oriented portions of SV, with such major limitations as not allowing properties or checkers within classes. It would be preferable, for example, to have monitors implemented as checkers, since this would permit checker reuse at different levels of abstraction. This requires the ability to specify checkers as class members. In general we need extensions of SVA that will fully enable its use in classes and other object-oriented constructs. Transaction-level assertions Currently in SystemVerilog, assertions are well defined only for the RTL level. It is important to adapt SVA for handling transaction-level verification, as well [27]. specific order, it is necessary to specify a group of sequences as an argument to a checker. Because of this fixed-length argument list limitation, different checkers need to be created to handle different numbers of events. IN THIS PAPER we covered several aspects of SVA standardization: its contents, history, justification, practical needs, major applications, interaction with academic research, and organizational problems and challenges. Some of these aspects are common to many standardization processes; others, such as the highly reciprocal interaction with the academic research, are more specific to SVA. For standardization to succeed, an appropriate investment needs to be made: designing features, writing documentation, reviewing, and proofreading require a dedicated effort. SVA is an example of standardization success, characterized by close, effective cooperation between customers and suppliers, industry and academia, and different standardization subcommittees. The history and lessons of the SVA effort can serve as a good example for other standardization projects. h h References [1] I. Beer et al. ‘‘The temporal logic sugar,’’ in Proc. Comput. Aided Verific., 2001. Type system In checkers, properties, and sequences it is possible to declare arguments of type property, sequence, or event. However, there is no generic data type for scalar arguments: they must either be declared using a specific data type or as untyped. Both alternatives are undesirable: the former prevents generality, whereas the latter prevents the code from being self-documenting, and makes error messages more obscure. For examle, instead of an error message like ‘‘a is a sequence, but an integral value is expected’’ at the checker invocation point, the user will get an error message like ‘‘goto repetition cannot be applied to sequences’’ somewhere in the checker internals. [2] R. Armony et al. ‘‘The ForSpec temporal logic: A new temporal property-specification language,’’ Tools and Algorithms for Construct. Analy. Syst., 2002. [3] N. Fedida, J. Havlicek, N. Levi, and H. Miller, CBV Semantics, 2002. [Online]. Available: http://www.vhdl. org/vfv/hm/att-0672/01-cbv_semantics.pdf. [4] IEEE Standard for SystemVerilogVUnified Hardware Design, Specification, and Verification, IEEE Std. 1800-2009, 2009. [5] J. Havlicek and Y. Wolfsthal, ‘‘PSL and SVA: Two standard assertion languages addressing complementary engineering needs,’’ in Proc. DVCon, 2005. [6] E. Cerny, S. Dudani, D. Korchemny, and L. Piper, ‘‘Verification case studies: Evolution from SVA 2005 to SVA 2009,’’ in Proc. DVCon, 2009. Variable number of arguments One more useful enhancement relates to the ability to specify a variable number of arguments in checkers and similar constructs. For example, to state that several events (sequences) happen in a 30 [7] IEEE Standard for Property Specification Language (PSL), IEEE 1850-2005, 2005. [8] A. Pnueli, ‘‘The temporal logic of programs,’’ in Proc. 18th IEEE Symp. Found. Comput. Sci., 1977, pp. 46–57. IEEE Design & Test of Computers [9] E. Cerny, S. Dudani, and D. Korchemny, ‘‘IEEE [24] E. Cerny, A. Dsouza, K. Harer, P.-H. Ho, and 1800-2009 SystemVerilog: Assertion-based Checker T. M. Hi-Keung, ‘‘Supporting sequential assumptions Libraries,’’ in Proc. DVCon, 2010. in hybrid verification,’’ in Proc. ASP-DAC, 2005, [10] E. Cerny, S. Dudani, and D. Korchemny, SVA Checker Library, 2010. [Online]. Available: http://www.accellera. org/apps/org/workgroup/ovl/download.php/3512/ SVACheckerLibrary_101006dk.pptx. [11] Accellera Standard Open Verification Library (OVL) V2.5, Accellera, 2010. [12] P. Clarke, ‘‘Intel SOCs aided by interconnect, IP library,’’ EE TimesVEDN, Jul. 2011. [13] R. Adler, S. Krstic, E. Seligman, and J. Yang, pp. 1035–1038. [25] D. Bustan, A. Flaisher, O. Grumberg, O. Kupferman, and M. Y. Vardi, ‘‘Regular vacuity,’’ Proc. CHARME, pp. 191–206, 2005. [26] Universal Verification Methodology. [Online]. Available: http://uvmworld.org/. [27] W. Ecker, V. Esen, T. Steininger, and M. Velten, ‘‘Requirements and concepts for transaction level assertions,’’ in Proc. IESS, 2007. ‘‘CompMon: Ensuring rigorous protocol specification and IP compliance,’’ presented at the Des. Verification Conf. Exhibition, San Jose, CA, 2011. [14] M. Y. Vardi, ‘‘From philosophical to industrial logics,’’ Proc. ICLA, pp. 89–115, 2009. [15] M. Y. Vardi, ‘‘Branching vs. linear time: Final Doron Bustan is working as software engineer at Intel Corporation and interested in high level modeling, high level specification, and security. In 2002, Bustan received a PhD in computer science from the Technion, Haifa, Israel. showdown,’’ in Proc. 2001 Conf. Tools and Algorithms for the Construct. Anal. Syst., 2001. [16] R. Armoni, D. Bustan, O. Kupferman, and M. Y. Vardi, ‘‘Aborts vs resets in linear temporal logic,’’ Proc. TACAS, pp. 65–80, 2003. [17] C. Eisner, D. Fisman, and J. Havlicek, ‘‘A topological characterization of weakness,’’ in Proc. PODC 2005. [18] D. Bustan and J. Havlicek, ‘‘Some complexity results Dmitry Korchemny is a senior CAD technical staff engineer at Intel. His interests include pre- and post-Si validation and debug. He is actively involved into SystemVerilog Assertion standardization. Korchemny has an MSc in electrical engineering and computer science from Moscow Institute of Radio-engineering, Electronics and Automation. He is a member of IEEE. for SystemVerilog assertions,’’ in Proc. Comput. Aided Verific., 2006, pp. 205–218. [19] M. Boule and Z. Zilic, ‘‘Automata-based assertion-checker synthesis of PSL properties,’’ ACM Trans. Design Autom. Electron. Syst., vol. 13, 2008. [20] S. Takeuchi, K. Hamaguchi, and T. Kashiwabara, ‘‘Checker generation of assertions with local variables Erik Seligman has been with Intel since 1994, in a variety of positions including software development, design, validation, and formal verification. Currently he is a formal verification architect in the Formal Verification Center of Expertise. Seligman has a MS in computer science from Carnegie-Mellon University, Pittsburgh, PA. for model checking,’’ IPSJ Trans. Syst. LSI Design Methodol., 2009. [21] R. Wille et al. ‘‘Identifying a subset of System Verilog assertions for efficient bounded model checking,’’ Digit. Syst. Design, 2008. [22] R. Armoni, D. Korchemny, A. Tiemeyer, M. Y Vardi, and Y. Zbar, ‘‘Deterministic dynamic monitors for linear-time assertions,’’ Proc. FATES, pp. 163–177, Jin Yang is a principal engineer in Strategic CAD Labs, Design and Technology Solutions at Intel. His research interests include system level specification, design, and validation, applied formal methods, and postsilicon validation diagnosis. Yang has a PhD in computer science from the University of Texas at Austin. 2006. [23] M. Siegel, A. Maggiore, and C. Pichler, ‘‘Untwist your h Direct questions and comments about this article brainVEfficient debugging and diagnosis of complex to Dmitry Korchemny, Intel Corporation, Intel Israel (74) LTD. P.O. BOX 1659, Haifa 31015, Israel; dmitry. korchemny@intel.com. assertions,’’ in Proc. Design Autom. Conf. (DAC), 2009. March/April 2012 31