Abstract
This chapter continues discussion about sequences started in Chap. 6, and covers all remaining SVA sequence operators. The new sequence operators described in this chapter do not add more expressive power to the language, but they make the specifications more elegant and concise. Some of these sequence operators, such as goto- and nonconsecutive repetition, are pure syntactic sugaring on top of the basic ones, others, like first_match and intersect, do not admit direct rewriting, though in each specific case it is possible to rewrite the sequence using basic operators only. We also describe of sequence methods triggered and matched that generalize the sampled value function $past for Boolean values. We conclude this chapter by a discussion about usong sequences as events.
Poe’s saying that a long poem is a sequence of short ones is perfectly just.
— John Drinkwater
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.
It can be proven formally [23].
- 2.
In PSL [6] , there is a property operator called next_event with a similar behavior.
- 3.
See Sect. 6.4.1 for a discussion about nested implications.
- 4.
Except when a or b has a match item, see Chap. 16.
- 5.
- 6.
For some tools, it may be more efficient to implement seq_not_first using modeling code to set a flag after clock tick 0.
References
IEEE Std. 1800–2005, IEEE Standard for SystemVerilog—Unified Hardware Design, Specification, and Verification Language (2005)
IEEE Std. 1800–2009, IEEE Standard for SystemVerilog—Unified Hardware Design, Specification, and Verification Language (2009)
IEEE Std. 1850–2010, IEEE Standard for Property Specification Language (PSL) (2010)
D. Bustan, J. Havlicek, Some complexity results for SystemVerilog assertions, in Proceedings of Computer Aided Verification, Lecture Notes in Computer Science. ISBN 3-540-37406-X, pp. 205–218 (Springer, 2006)
E.A. Emerson, Temporal and modal logic, in Handbook of Theoretical Computer Science, ed. by J. van Leeuwen (Elsevier Sience Publishers B.V., Amsterdam, 1990), pp. 996–1072
Author information
Authors and Affiliations
Rights and permissions
Copyright information
© 2015 Springer International Publishing Switzerland
About this chapter
Cite this chapter
Cerny, E., Dudani, S., Havlicek, J., Korchemny, D. (2015). Advanced Sequences. In: SVA: The Power of Assertions in SystemVerilog. Springer, Cham. https://doi.org/10.1007/978-3-319-07139-8_11
Download citation
DOI: https://doi.org/10.1007/978-3-319-07139-8_11
Published:
Publisher Name: Springer, Cham
Print ISBN: 978-3-319-07138-1
Online ISBN: 978-3-319-07139-8
eBook Packages: EngineeringEngineering (R0)