Architectural Properties

Concept

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).

First seen 7/10/2026

Last seen 7/10/2026

Evidence 3 chunks

Wiki v1

WIKI

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].

READ FULL ARTICLE →

NEIGHBORHOOD

No graph connections found for this entity yet. It may appear in future ingestion runs.

explore full graph →

RELATIONSHIPS

1 connections

Using Formal Verification to Evaluate Single Event Upsets in a RISC-V Core ← uses 95% 2e

Architectural properties specify RISC-V core behavior to identify SEUs.

LINKED ENTITIES

1 links

Using Formal Verification to Evaluate Single Event Upsets in a RISC-V Core USES Extracted graph relationship

CITATIONS

8 sources

8 citations — click to expand

[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