Formal languages are increasingly used to describe the functional requirements (specifications) of circuits. These requirements are used as a means to communicate design intent and as basis for verification. In both settings it is of utmost importance that the specifications are of high quality. However, formal requirements are seldom the object of validation, even though they can be hard to understand and interactions between them can be subtle. In this paper we present techniques and guidelines to explore and assure the quality of a formal specification. We define a technique to interactively explore the semantics of a specification by simulating its behavior for user-defined scenarios. Further-more, we define techniques to automatically check specifications against a set of user-provided assertions, which must be satisfied, and a set of possibilities, which must not be conradicted. The proposed techniques support the user in the iterative development and refinement of high-quality specifications.

The IEEE standard property specification language (PSL) allows to express all omega-regular properties mixing linear temporal logic (LTL) with sequential extended regular expressions (SEREs), and is increasingly used in many phases of the hardware design cycle, from specification to verification. Many verification engines are able to manipulate nondeterministic Buchi automata (NBA), that can represent omega-regular properties. Thus, the ability to convert PSL into NBA is an important enabling factor for the reuse of a large wealth of verification tools. Recent works propose a two-step conversion from PSL to NBA: first, the PSL property is encoded into an alternating Buchi automaton (ABA); then, the ABA is converted into an NBA with variants of Miyano-Hayashi's construction. These approaches are problematic in practice: in fact, they are often unable to carry out the conversion in acceptable time, even for PSL specifications of moderate size. In this paper, we propose a modular encoding of PSL into symbolically represented NBA. We convert a PSL property into a normal form that separates the LTL and the SERE components. Each of these components can be processed separately, so that the NBA corresponding to the original PSL property is presented in the form of an implicit product, delaying composition until search time. Our approach has two other advantages: first, we can leverage mature techniques for the LTL components; second, we leverage the particular form of the PSL components that appear in the normal form to improve over the general translation. The transformation is proved correct. A thorough experimental analysis over large sets of paradigmatic properties (from patterns of properties commonly used in practice) shows that our approach drastically reduces the construction time of the symbolic NBA, and positively affects the overall verification time