Anzeige
Erschienen in:
2006 | OriginalPaper | Buchkapitel
Some Complexity Results for SystemVerilog Assertions
verfasst von : Doron Bustan, John Havlicek
Erschienen in: Computer Aided Verification
Verlag: Springer Berlin Heidelberg
Aktivieren Sie unsere intelligente Suche, um passende Fachinhalte oder Patente zu finden.
Wählen Sie Textabschnitte aus um mit Künstlicher Intelligenz passenden Patente zu finden. powered by
Markieren Sie Textabschnitte, um KI-gestützt weitere passende Inhalte zu finden. powered by
SystemVerilog Assertions (
SVA)
is a linear temporal logic within the recently approved IEEE 1800 SystemVerilog standard. The complexities of the satisfiability and model-checking problems are studied for a basic subset of (
SVA)
and for extensions of the basic subset obtained by adding each of the following features: local variables, regular expression intersection, quantified variables, and property declarations with arguments. It is shown that the complexities for the basic subset are PSPACE-complete, while the complexities increase to EXPSPACE-complete in each of the extensions. Alternating Büchi automata constructions provide the upper bounds, while reductions from PSPACE and EXPSPACE tiling problems provide the lower bounds.