Safety Property

Definition and role

In the cited formal-verification setting, a safety property is the class of property used to describe the intended behavior of a digital circuit and to formalize its specification. Interval property checking (IPC) verifies only safety properties; the cited source states that this restriction is not serious in practice for digital circuits because they have finite response time. The same source also states that safety properties are a natural way to describe intended design behavior and that the restriction leads to bounded properties that can be checked efficiently with a SAT solver.

Formal representation

The cited model treats a synchronous circuit as a finite-state machine M = (I, S, S0, Δ, Λ, O), with inputs, states, initial states, transition behavior, outputs, and an output function. Within this setting, a safety property is written as:

f = AG(φ)

The property can be translated into a Boolean function [[f]]t that checks the validity of the formula φ at time point t. The translation is chosen so that a satisfying assignment of [[f]]t corresponds to a counterexample of φ. The resulting Boolean function depends on inputs, outputs, and states within a bounded time interval [0, c].

Checking with IPC

IPC searches for counterexamples by solving a SAT instance that combines an unrolling of the transition relation over a bounded interval with the single instantiated property formula. In the cited notation, the transition relation is unrolled over the interval and connected to [[f]]t.

A key feature of IPC is that it uses an arbitrary starting state rather than the initial state used in bounded model checking. If a property holds from an arbitrary state, it also holds from any reachable state and is therefore exhaustively verified. However, this can produce false negatives: counterexamples may start in unreachable states. The cited source says these false negatives must be removed by adding invariants that restrict the starting state.

Expression in ITL

The cited properties are written in the ITL language, where temporal logic expressions describe synchronous sequential-system behavior and discrete time steps correspond to clock cycles. ITL properties usually have an implication structure: if expressions in the assume part evaluate to true, then expressions in the prove part must also hold. ITL also supports freeze variables fixed to a particular time point, standard HDL operators, and temporal operators such as next and prev, which shift an expression one cycle into the future or past.

Use in complete property suites

Safety properties can form part of a property suite. The cited source describes completeness analysis as determining whether every possible input scenario, corresponding to a transaction sequence of the design, can be covered by a chain of properties that predicts states and outputs at every point in time. It further states that any two designs fulfilling all properties of a complete property suite are formally equivalent.