Portal de Periódicos da CAPES

Some Complexity Results for SystemVerilog Assertions

2006; Springer Science+Business Media; Linguagem: Inglês

10.1007/11817963_21

1611-3349

Doron Bustan, John Havlicek,

Model-Driven Software Engineering Techniques

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.