Definition
Architectural style properties are verification properties reformulated so that the processor architecture is described explicitly rather than only implicitly through per-operation properties. The cited work introduces this style because an instruction set simulator (ISS) needs an architecture description, mainly an architectural state and a next-state function describing the effects of instructions and interrupts on that state. Operation properties can resemble a high-level specification, but their architecture description is implicit, making generic automatic extraction difficult; architectural style makes ISS generation straightforward. [Architectural-style purpose]
Required structure
An architectural style verification is characterized by four explicit elements:
- modeling of the architectural state and the interfaces to memories or ports;
- definition of a
next_statemacro that captures the effects of instructions and interrupts on the architectural state; - definition of macros that capture the behavior of memory and port interfaces; and
- definition of the architectural reset state. [Architectural-style characteristics]
The architectural state is established using a user-defined VHDL record data type that combines the relevant architectural elements. Typical contents include a register file, status flags, and a program counter. New data types are also defined for interfaces to memories and ports. [Architectural-state representation]
Next-state semantics
The next_state macro is central to the style. In the cited ADD-instruction example, decoded instruction fields are held in an instruction_t record, and next_state returns the architectural state modified by executing the current instruction. The execution is modeled in a case block: when the opcode denotes ADD, the register file in the current architectural state is updated with the sum of the source operands. [Next-state macro role]
The formulation uses an update keyword to explicitly define write access to array or record data structures. In the example, a state record of type state_t holds the architectural state, and update writes the computed ADD result into the destination register. [Update keyword]
Relation to equivalence checking
Architectural style properties can be checked against RTL, and automatic gap detection is executed as well. The cited source states that discrepancies between architectural and operation properties are identified automatically, and that the reformulated property set remains equivalent to the design when checked in this process. [RTL checking and gap detection]
The equivalence proof uses an abstraction function, named vstate in the cited example, to map the CPU implementation state to the ISA state. The intended proof obligation is that applying the implementation transition relation and then mapping to the architectural state corresponds to mapping first and then applying next_state. The proof also has to show that interface signals behave as specified by interface macros and that the implementation reset state complies with the architectural reset state. [Equivalence proof structure]
Use in ISS generation
The outcome of reformulating in architectural style is a single property that captures all behavior of the verified design using next_state; the cited paper describes this as a formally checkable ISA description and uses it as the starting point for generating a C++ instruction set simulator. [ISA description outcome]
Full ISA/RTL equivalence proof is not required before generating the ISS, nor is it necessary to identify mapping functions between architectural and implementation state for early generation. The ISA can be developed in ITL early in the design process, used to generate an ISS, and regenerated only when the ISA changes; full confidence that the ISS complies with the design is obtained at the end of verification. [Early ISS generation]
When verification has been carried out in architectural style from the beginning, the ISS can be generated from the verification without manual steps in between. The source also notes that mapping functions for the architectural state, while difficult to find for verification, are not needed for automatic ISS generation. [No-manual-step generation]
Resulting simulator core
In the described generation flow, the generated C++ class forms the core functionality of the ISS: it contains instruction-execution code and holds the architectural state. A separate user-provided wrapper calls generated public functions to execute instructions and connects the simulation core to peripheral components such as external memories or buses; integration with commercial simulation and debugging tools is also described as possible. [Generated simulator core]
Significance
The paper concludes that a complete, gap-free property suite formulated in architectural style can be used to generate a C++ ISS. After successful formal verification, the property suite forms an architectural model of the verified design, making the generated ISS equivalent to the design by construction. The authors also report that optimizations during C++ generation make the resulting simulator performance comparable to state-of-the-art commercial tools. [Verified ISS significance]