Skip to content
STIMSMITH

Architectural Properties

Concept WIKI v1 · 7/10/2026

Architectural properties are a class of formal-verification assertions used to characterize the correct architectural behavior of a RISC-V core (such as the Ibex Core) when executing RV32IMC instructions. Unlike strobe properties, they do not require duplicating the design and are reused to explore silent data corruptions (SDCs), crashes, and hangs caused by single event upsets (SEUs).

Architectural Properties

Definition and Scope

In the context of formal verification of processor cores, architectural properties are assertions that specify the correct architectural behavior of a RISC-V core when executing an RV32IMC instruction. They are developed with reference to the RISC-V Instruction Set Manual and encode the expected semantics of individual instructions in formal-property form [chunk 9878e45e-8ce3-4830-9f35-5ba6ab2eeaa7].

Relationship to Strobe Properties

Architectural properties are contrasted with strobe properties, which duplicate the design (one golden core plus one faulty core with injected arbitrary SEUs) and compare important signals such as the retired instructions and program counters between the two instances [chunk 9878e45e-8ce3-4830-9f35-5ba6ab2eeaa7].

Key distinctions:

  • No design duplication: Architectural properties do not require duplicating the Ibex Core, avoiding the increased design and verification complexity introduced by strobe-based duplication [chunk 9878e45e-8ce3-4830-9f35-5ba6ab2eeaa7].
  • Higher initial effort, but reusable: Architectural properties are more difficult to develop than strobe properties, but they are a one-time cost because the same architectural properties can be reused for other RISC-V designs [chunk 9878e45e-8ce3-4830-9f35-5ba6ab2eeaa7].
  • Equivalent fault coverage: Both property groups produce the same results—identifying the same bits vulnerable to SEUs [chunk 9878e45e-8ce3-4830-9f35-5ba6ab2eeaa7].

Example: BGE Instruction Property

A representative architectural property specifies the correct behavior of the RGE-class BGE (Branch if Greater Than or Equal) instruction [chunk 9878e45e-8ce3-4830-9f35-5ba6ab2eeaa7]. The antecedent RV32I_BGE is true when the executed instruction in the Ibex Core is a valid 32-bit BGE instruction (opcode 7'b1100011, funct3 3'b101). The consequent compares pc_wdata (the next program counter extracted from the core) against the expected value next_pc_bge, which is computed by selecting between pc_rdata + imm_b_type and pc_rdata + 4 based on a signed comparison of rs1_rdata and rs2_rdata.

Use Cases

Architectural properties are used to explore three classes of fault-induced behavior:

  1. Silent Data Corruption (SDC) – properties that specify correct per-instruction behavior. Proving these took about 13 days of compute time [chunk ede74f7b-1054-4e1e-a123-09b0126b0203].
  2. Crash – architectural properties describing instruction access faults, illegal instructions, ECall, breakpoints, and load/store access faults. Both crash and hang properties are architectural [chunk 9878e45e-8ce3-4830-9f35-5ba6ab2eeaa7]. Proving crash properties took about 5 days [chunk 2482ce8f-998a-418c-b553-0bfafc73c168].
  3. Hang – properties characterizing situations (e.g., WFI) in which the core fails to make forward progress. Proving hang properties took about one day [chunk 2482ce8f-998a-418c-b553-0bfafc73c168].

Results on the Ibex Core

When applied to the Ibex Core (which contains 2008 bits in total), architectural properties identify, for each monitored instruction, the number of bits whose SEU-induced faults may corrupt the function and execution of that instruction [chunk ede74f7b-1054-4e1e-a123-09b0126b0203]. For example, SEUs at 91 bits lead to malfunctioning of the RV32I_LUI instruction (e.g., a wrong read value) and hence cause an SDC [chunk ede74f7b-1054-4e1e-a123-09b0126b0203].

The architectural-property analysis agrees with strobe-property analysis on which bits are vulnerable. For instance, both property sets identify two SDC-vulnerable bits in the ibex_prefetch_buffer module, forming the 2-bit register rdata_pmp_err_q (the PMP error signal, normally zero) [chunk 2482ce8f-998a-418c-b553-0bfafc73c168].

See Also

  • Using Formal Verification to Evaluate Single Event Upsets in a RISC-V Core – the paper that introduces and applies architectural properties to the Ibex Core.

LINKED ENTITIES

1 links
Using Formal Verification to Evaluate Single Event Upsets in a RISC-V Core USES

CITATIONS

8 sources
8 citations
[1] Architectural properties specify the correct architectural behavior of a RISC-V core when executing an RV32IMC instruction and are developed using the RISC-V Instruction Set Manual. Using Formal Verification to Evaluate Single Event Upsets in a RISC-V Core
[2] Architectural properties do not require duplicating the Ibex Core, in contrast to strobe properties which compare a golden and faulty core instance. Using Formal Verification to Evaluate Single Event Upsets in a RISC-V Core
[3] Architectural properties are more difficult to develop than strobe properties but are reusable across RISC-V designs, while both property groups identify the same bits as vulnerable to SEUs. Using Formal Verification to Evaluate Single Event Upsets in a RISC-V Core
[4] The architectural property for the BGE instruction uses the antecedent RV32I_BGE (valid 32-bit BGE with opcode 7'b1100011 and funct3 3'b101) and the consequent comparing pc_wdata to a next-pc value selected by a signed comparison of rs1_rdata and rs2_rdata. Using Formal Verification to Evaluate Single Event Upsets in a RISC-V Core
[5] Proving architectural SDC properties took about 13 days of compute time, while strobe SDC properties took about 11 days. Using Formal Verification to Evaluate Single Event Upsets in a RISC-V Core
[6] Proving crash properties took about 5 days and proving hang properties took about one day; both crash and hang properties are architectural. Using Formal Verification to Evaluate Single Event Upsets in a RISC-V Core
[7] Architectural properties report, per monitored instruction, the number of bits whose SEUs may corrupt that instruction's function and execution; e.g., SEUs at 91 bits cause malfunctioning of RV32I_LUI. Using Formal Verification to Evaluate Single Event Upsets in a RISC-V Core
[8] Both strobe and architectural properties agree on the same vulnerable bits, including the two SDC-vulnerable bits forming the rdata_pmp_err_q register in the ibex_prefetch_buffer module. Using Formal Verification to Evaluate Single Event Upsets in a RISC-V Core