Complete Property Suite

A complete property suite is a set of formal verification properties that is complete enough to cover every possible input scenario of a design, where an input scenario corresponds to a transaction sequence. Completeness analysis checks whether such scenarios can be covered by a chain of properties that predicts the values of states and outputs at every point in time. In this sense, any two designs satisfying all properties of a complete property suite are formally equivalent. [CompletenessDefinition]

Completeness analysis

The cited methodology characterizes completeness by checking the end state of each property. The analysis verifies that:

1. there is always a successor property with matching assumptions;
2. the successor property is uniquely determined; and
3. each property describes the outputs and states of the design under verification in a unique way. [CompletenessChecks]

This makes the property suite more than a collection of selected assertions: when the suite is complete and the verification succeeds, it describes the design behavior sufficiently to act as a model of the verified design. [VerifiedDesignModel]

Role in formal verification

The cited work uses Interval Property Checking (IPC), a SAT-based formal-verification method related to bounded model checking. IPC verifies safety properties from an arbitrary starting state rather than only from the initial state. A property that holds from an arbitrary state also holds from any reachable state, so the property is exhaustively verified. However, IPC can produce false negatives when counterexamples start from unreachable states; such cases are removed by adding invariants that restrict the starting state. [IPC]

The properties are written in ITL. In ITL, temporal-logic expressions describe synchronous sequential systems, and discrete time steps correspond to clock cycles. ITL properties typically have an implication structure: assumptions in an assume part imply obligations in a prove part. ITL also supports macro functions, HDL operators and data types, arrays, user-defined types, and nested VHDL record types. [ITL]

Operation-view properties

For processor verification, the property view of the design can be a high-level operation view. An operation naturally corresponds to the execution of a single instruction, so each operation property describes the change of internal state and the behavior of output signals when the processor executes an instruction. The design state is expressed as a high-level or architectural state corresponding to the programmer-visible registers, using mapping functions to connect the architectural view to the implementation. [OperationView]

The cited ADD-instruction example illustrates this style: under constraints for an ADD instruction, the property proves that one time step later the register file is updated with the correct value. Because of completeness requirements, the property also has to state that the remaining registers do not change and must specify the processor output behavior. [ADDCompleteness]

Architectural-style formulation

For instruction set simulator generation, the paper focuses on reformulating operation properties into architectural style properties. An architectural description for an ISS mainly consists of an architectural state and a next-state function describing the effects of instructions and interrupts on that state. The paper notes that automatic extraction from generic operation properties would be difficult, so architectural style is used to make ISS generation straightforward. [ArchitecturalStylePurpose]

Architectural-style verification is characterized by four explicit elements:

1. modeling of the architectural state and memory or port interfaces;
2. a next_state macro capturing the effects of instructions and interrupts on the architectural state;
3. macros capturing the behavior of interfaces to memories and ports; and
4. an architectural reset state. [ArchitecturalStyleElements]

If verification is carried out in architectural style from the beginning, the ISS can be generated from the verification without manual steps in between. The reformulation of operation properties is still checked against the RTL, and automatic gap-detection is executed, so discrepancies between architectural and operation properties can be identified automatically. [ArchitecturalStyleVerification]

Use for instruction set simulator generation

After reformulation in architectural style, the outcome is a single property that captures all behavior of the verified design using the next_state function. The paper describes this as a formally checkable ISA description and uses it as the starting point for automatic generation of a C++ instruction set simulator. [ISSGeneration]

The architectural state is represented using a user-defined VHDL record data type that combines the parts of the architectural state, typically including a register file, status flags, and a program counter. Additional data types describe memory and port interfaces. The ITL update keyword is used to explicitly define writes to arrays or record data structures, such as updating a destination register for an ADD operation in next_state. [ArchitecturalStateModeling]

Practical significance

The practical value of a complete property suite is that, once verification has succeeded, the same formal artifact can serve both as a verification specification and as a basis for a simulator model. In the cited processor flow, the suite supports a transition from checked properties to a formally checkable ISA description and then to a generated C++ ISS. [PracticalSignificance]