Types¶

Literal types¶

Boolean literal: <bool_literal> ::= true | false
Non-negative integer: <int> ::= n with $n \in \mathbb N_{0}$
Bounded range: <bounded_range> ::= (bounded-range m n) with $m,n \in \mathbb N_{0}$ and $m \leq n$
Constant range: <range> ::= (range m n) | (range m $) with $m,n \in \mathbb N_{0}$ and $m \leq n$

Literal types are used as parameters for primitives.

Boolean literals true and false are used to define constant signals (constant true) and (constant false), which correspond to 1'b1 and 1'b0.

There are two variants of ranges. A bounded range has an upper bound and a lower bound, which are both non-negative integers, with the upper bound being equal to or higher than the lower bound. The constant range can have the upper bound $, indicating that it is unbounded. It is important to use the correct range type expected by a primitive. For example, delay accepts unbounded ranges, so it requires the range keyword even if the provided range is bounded, whereas weak eventually accepts only bounded ranges and therefore requires the bounded-range keyword.

(clk-seq-delay (range 2 4) (clk-seq-bool b)) ; ##[2:4] b

(clk-seq-delay (range 2 $) (clk-seq-bool b)) ; ##[2:$] b

(clk-prop-eventually (bounded-range 3 5) (clk-prop-bool b)) ; eventually [3:5] b

For most SVA operations with integer parameters, the corresponding Property IR primitive expects a range argument where the lower and upper bound have the same value.

(clk-seq-delay (range 2 2) (clk-seq-bool b)) ; ##2 b

The primitives corresponding to nexttime, having only an integer parameter, are exempt from this rule.

(clk-prop-nexttime 2 (clk-prop-bool b)) ; nexttime[2] b

Expression types¶

Boolean Expression bool
Clocked Sequence clk-seq
Clocked Property clk-prop

There exist additional internal types to represent automata states and circuits. They are used internally during the verification flow and are not part of the public interface. There exist additional types to represent simple sequences and simple properties. Although they are used internally, they are included here because it is possible to use them in assertions by applying the clk-prop-prop or clk-seq-seq primitives to them. However, if you want to translate a SystemVerilog property into a Property IR expression, you want to use the clocked versions of properties and sequences.

Boolean Expressions¶

Boolean expressions correspond to signals, either directly through the declaration of and external signal, as Boolean constants, or as a Boolean function using a basic set of logical operators. They can only take the values true or false.

(declare-input a)
(declare-input b)
(declare c (and (or a b) (not b) (constant true)))

Clocked Sequences¶

Sequences model the progression of Boolean expression values over time, with one value sampled at each clock tick. Clocked sequences use a clock that may be different from the global clock. The basic building blocks of sequences are sequences of length 1, consisting of one value of a Boolean expression. They can be combined via concatenation, repetition, and more complex operations.

(declare-input a)
(declare-input b)
(declare-input c)
(declare seq_1 (clk-seq-and
   (clk-seq-concat
      (clk-seq-delay (range 0 3) (clk-seq-bool (not a)))
      (clk-seq-bool (or a b)))
   (clk-seq-repeat (range 3 $) (clk-seq-bool c))))

All clock controls are of type bool and expected to be level-sensitive (or rather a time-discrete global-clock sampled clock control), i.e., they are high in the global clock tick immediately before they have their rising (resp. falling) edge and low else. It is possible to convert an edge-sensitive clock to a level-sensitive clock inside Property IR using the global clocking future sampled value functions. For example, the clock control of the sequence seq_1 can be set to @(posedge clk) as follows, where, roughly speaking, clk is the edge-sensitive clock, and clk_def states whether clk has a defined value.

(declare-input clk)
(declare-input clk_def)
(declare seq_1_clk (clk-seq-clocked (rising-gclk clk clk_def) seq_1))

Note

Primitives corresponding to future sampled value functions, like rising-gclk, are based on future-gclk and are not synthesizable. However, it is possible to remove future-gclk from the checker circuit by delaying the rest of the circuit by one global time step in order to obtain a synthesizable circuit again.

Clocked Properties¶

Properties model the behavior of a design and are built on the basis of sequences, whose presence can be checked and tied to various conditions. Like clocked sequences, clocked properties use a clock that may be different from the global clock.

(declare-input a)
(declare-input b)
(declare prop_1 (clk-prop-non-overlapped-implication
   (clk-seq-bool a)
   (clk-prop-until (clk-prop-bool b) (clk-prop-always a))))

Simple Sequences and Simple Properties¶

Simple Sequence seq
Simple Property prop

Simple properties and simple sequences are used internally in a preparation step for the verification flow, where clocked properties and clocked sequences are first rewritten to their respective simple versions by applying several rewriting passes. They are simple in the following sense:

They have a smaller set of primitives.
They use the global clock, which is why there is no need to explicitly specify a clock.
They do not contain any subsequences that admit empty matches.

Establishing these restrictions will facilitate the subsequent automata constructions. These separate types were introduced to avoid inconsistencies that would result from clock rewriting.

The following explanations can be skipped, but might be interesting as a background.

Smaller primitive set¶

The reduced set of primitives was chosen in such a way that at least

nonderived primitives are included, and
dual operations are included.

Additional primitives may be added if they turn out benefical for automata constructions or subsequent optimizations.

Including dual operations is necessary in order to establish the negation normal form, which is done before the transformation into automata. For example, (prop-overlapped-followed-by <seq> <prop>) is equivalent to (prop-not (prop-overlapped-implication <seq> (prop-not <prop>))) and is therefore the dual of the nonderived primitive prop-overlapped-implication.

On the other hand, an example for a derived primitive that can be removed is (seq-goto-repeat <range> <bool>), because it can be rewritten in the following way.

(seq-repeat <range> (seq-concat
   (seq-repeat (range 0 $) (seq-bool (not <bool>)))
   (seq-bool <bool>)))

Global clock¶

Clocked properties, that can have one or multiple clocks, are rewritten in such a way that they use the global clock. Roughly speaking, this is achieved by recursively rewriting property expressions such that sequences of length 1 are replaced by a sequence waiting for the clock event to happen (and additional rewriting rules for handling operations like nexttime and until).

Let b be a signal, and c the level-sensitive clock signal. Then (clk-seq-clocked c (clk-seq-bool b)) becomes the following expression.

(seq-concat (seq-repeat (range 0 $) (not c)) (and c b))

Empty matches¶

In the process of translating a clocked property into a simple property, the empty part of sequences is removed in order to exclude special cases. This is possible because on the level of properties, empty matches only play a role insofar that they have an influence on non-empty sequences via concatenation. In an overlapped implication, an empty match of the antecedent sequence does not cause it to trigger. According to the SystemVerilog standard, the sequence expression of a sequential property shall not admit an empty match. To exclude sequences with empty matches, empty repeat (seq-repeat (range 0 0) <seq>) (and more generally, repeat with lower bound 0) must not be applied to simple sequences.

Consider the following example showing equivalent expressions, where the first expression is split into a disjunction of the empty and the nonempty part.

(clk-seq-concat
   (clk-seq-bool a)
   (clk-seq-repeat (range 0 1) (clk-seq-bool b))
   (clk-seq-bool c))

(clk-seq-or
   (clk-seq-concat (clk-seq-bool a) (clk-seq-bool c))
   (clk-seq-concat (clk-seq-bool a) (clk-seq-bool b) (clk-seq-bool c)))

Transformation steps¶

Translating a clocked property to a simple property is performed in several steps in the same order as these points are discussed above:

rewrite primitives to use smaller subset
rewrite to global clock
remove empty part

Note that all these steps operate on clocked properties. In particular, during the clock rewriting pass, the level-sensitive clock of (clk-seq-clocked <bool> <clk_seq>) becomes the constant (true). Only after removing the empty part, the clock specification is removed and all primitives are replaced by their simple counterparts.

(clk-prop-clocked <bool> <clk_prop>)    ; clocked

|   reduce primitives
V

(clk-prop-clocked <bool> <clk_prop2>)   ; fewer primitives

|   apply clock
V

(clk-prop-clocked (true) <clk_prop3>)   ; global-clocked

|  nonempty part
V

(clk-prop-clocked (true) <clk_prop4>)   ; global-clocked and non-empty-matching

|  remove clock
V

<prop>                                  ; simple/unclocked