logicaffeine_compile/codegen_sva/protocols/
riscv.rs

1//! RISC-V ISA Formal Verification Templates
2//!
3//! Pre-verified instruction semantics as parameterizable SVA templates.
4//! Users describe their CPU configuration, templates generate SVA properties.
5
6use super::ProtocolProperty;
7use super::SvaAssertionKind;
8
9/// RISC-V extension identifiers.
10#[derive(Debug, Clone, PartialEq, Eq)]
11pub enum RiscvExtension {
12    I, // Base integer
13    M, // Multiply/Divide
14    A, // Atomic
15    F, // Single-precision float
16    D, // Double-precision float
17    C, // Compressed
18}
19
20/// RISC-V CPU configuration.
21#[derive(Debug, Clone)]
22pub struct RiscvConfig {
23    pub xlen: u32,
24    pub extensions: Vec<RiscvExtension>,
25    pub reg_prefix: String,
26    pub pc_name: String,
27    pub mem_name: String,
28}
29
30impl RiscvConfig {
31    pub fn rv32i() -> Self {
32        Self {
33            xlen: 32,
34            extensions: vec![RiscvExtension::I],
35            reg_prefix: "x".into(),
36            pc_name: "pc".into(),
37            mem_name: "mem".into(),
38        }
39    }
40
41    pub fn rv64i() -> Self {
42        Self {
43            xlen: 64,
44            extensions: vec![RiscvExtension::I],
45            reg_prefix: "x".into(),
46            pc_name: "pc".into(),
47            mem_name: "mem".into(),
48        }
49    }
50}
51
52/// Generate ALU instruction properties.
53pub fn riscv_alu_properties(config: &RiscvConfig) -> Vec<ProtocolProperty> {
54    let w = config.xlen;
55    let r = &config.reg_prefix;
56    let mut props = vec![
57        ProtocolProperty {
58            name: "RISCV_ADD".into(),
59            spec: format!("When opcode is R-type ADD, rd = rs1 + rs2 ({}bit).", w),
60            sva_body: format!(
61                "(opcode == 7'h33 && funct3 == 3'h0 && funct7 == 7'h00) |-> (rd == rs1 + rs2)"
62            ),
63            kind: SvaAssertionKind::Assert,
64        },
65        ProtocolProperty {
66            name: "RISCV_SUB".into(),
67            spec: format!("When opcode is R-type SUB, rd = rs1 - rs2 ({}bit).", w),
68            sva_body: format!(
69                "(opcode == 7'h33 && funct3 == 3'h0 && funct7 == 7'h20) |-> (rd == rs1 - rs2)"
70            ),
71            kind: SvaAssertionKind::Assert,
72        },
73        ProtocolProperty {
74            name: "RISCV_AND".into(),
75            spec: format!("When opcode is R-type AND, rd = rs1 & rs2 ({}bit).", w),
76            sva_body: "(opcode == 7'h33 && funct3 == 3'h7 && funct7 == 7'h00) |-> (rd == (rs1 & rs2))".into(),
77            kind: SvaAssertionKind::Assert,
78        },
79        ProtocolProperty {
80            name: "RISCV_OR".into(),
81            spec: format!("When opcode is R-type OR, rd = rs1 | rs2 ({}bit).", w),
82            sva_body: "(opcode == 7'h33 && funct3 == 3'h6 && funct7 == 7'h00) |-> (rd == (rs1 | rs2))".into(),
83            kind: SvaAssertionKind::Assert,
84        },
85        ProtocolProperty {
86            name: "RISCV_XOR".into(),
87            spec: format!("When opcode is R-type XOR, rd = rs1 ^ rs2 ({}bit).", w),
88            sva_body: "(opcode == 7'h33 && funct3 == 3'h4 && funct7 == 7'h00) |-> (rd == (rs1 ^ rs2))".into(),
89            kind: SvaAssertionKind::Assert,
90        },
91        ProtocolProperty {
92            name: "RISCV_SLT".into(),
93            spec: "When opcode is SLT, rd = (rs1 < rs2) signed.".into(),
94            sva_body: "(opcode == 7'h33 && funct3 == 3'h2 && funct7 == 7'h00) |-> (rd == ($signed(rs1) < $signed(rs2)))".into(),
95            kind: SvaAssertionKind::Assert,
96        },
97        ProtocolProperty {
98            name: "RISCV_SLTU".into(),
99            spec: "When opcode is SLTU, rd = (rs1 < rs2) unsigned.".into(),
100            sva_body: "(opcode == 7'h33 && funct3 == 3'h3 && funct7 == 7'h00) |-> (rd == (rs1 < rs2))".into(),
101            kind: SvaAssertionKind::Assert,
102        },
103    ];
104
105    // M extension: MUL, DIV
106    if config.extensions.contains(&RiscvExtension::M) {
107        props.push(ProtocolProperty {
108            name: "RISCV_MUL".into(),
109            spec: format!("When opcode is MUL, rd = (rs1 * rs2)[{}:0].", w - 1),
110            sva_body: "(opcode == 7'h33 && funct3 == 3'h0 && funct7 == 7'h01) |-> (rd == rs1 * rs2)".into(),
111            kind: SvaAssertionKind::Assert,
112        });
113        props.push(ProtocolProperty {
114            name: "RISCV_DIV".into(),
115            spec: "When opcode is DIV, rd = rs1 / rs2 (signed).".into(),
116            sva_body: "(opcode == 7'h33 && funct3 == 3'h4 && funct7 == 7'h01) |-> (rd == $signed(rs1) / $signed(rs2))".into(),
117            kind: SvaAssertionKind::Assert,
118        });
119    }
120
121    props
122}
123
124/// Generate decoder mutual exclusion properties.
125pub fn riscv_decoder_properties(config: &RiscvConfig) -> Vec<ProtocolProperty> {
126    vec![
127        ProtocolProperty {
128            name: "RISCV_Decoder_Mutual_Exclusion".into(),
129            spec: "At most one instruction type is active per cycle.".into(),
130            sva_body: "!(is_r_type && is_i_type) && !(is_r_type && is_s_type) && !(is_r_type && is_b_type) && !(is_i_type && is_s_type) && !(is_i_type && is_b_type) && !(is_s_type && is_b_type)".into(),
131            kind: SvaAssertionKind::Assert,
132        },
133    ]
134}
135
136/// Generate register file properties.
137pub fn riscv_register_properties(config: &RiscvConfig) -> Vec<ProtocolProperty> {
138    let r = &config.reg_prefix;
139    let w = config.xlen;
140    let mut props = vec![
141        ProtocolProperty {
142            name: "RISCV_X0_Always_Zero".into(),
143            spec: format!("Register {}0 always reads as zero.", r),
144            sva_body: format!("{}0 == {}'d0", r, w),
145            kind: SvaAssertionKind::Assert,
146        },
147        ProtocolProperty {
148            name: "RISCV_X0_Write_Ignored".into(),
149            spec: format!("Writing to {}0 has no effect; it remains zero.", r),
150            sva_body: format!("(rd_addr == 5'd0) |=> ({}0 == {}'d0)", r, w),
151            kind: SvaAssertionKind::Assert,
152        },
153    ];
154
155    // PC alignment
156    if config.extensions.contains(&RiscvExtension::C) {
157        props.push(ProtocolProperty {
158            name: "RISCV_PC_Alignment_C".into(),
159            spec: format!("PC is always 2-byte aligned (C extension present)."),
160            sva_body: format!("{}[0] == 1'b0", config.pc_name),
161            kind: SvaAssertionKind::Assert,
162        });
163    } else {
164        props.push(ProtocolProperty {
165            name: "RISCV_PC_Alignment".into(),
166            spec: format!("PC is always 4-byte aligned (no C extension)."),
167            sva_body: format!("{}[1:0] == 2'b00", config.pc_name),
168            kind: SvaAssertionKind::Assert,
169        });
170    }
171
172    props
173}
174
175/// Generate branch instruction properties.
176pub fn riscv_branch_properties(config: &RiscvConfig) -> Vec<ProtocolProperty> {
177    vec![
178        ProtocolProperty {
179            name: "RISCV_BEQ".into(),
180            spec: "When BEQ and rs1 == rs2, PC = PC + immediate.".into(),
181            sva_body: "(opcode == 7'h63 && funct3 == 3'h0 && rs1 == rs2) |-> (pc_next == pc + imm_b)".into(),
182            kind: SvaAssertionKind::Assert,
183        },
184    ]
185}
186
187/// Generate memory access properties.
188pub fn riscv_memory_properties(config: &RiscvConfig) -> Vec<ProtocolProperty> {
189    let w = config.xlen;
190    vec![
191        ProtocolProperty {
192            name: "RISCV_LW_SW_Roundtrip".into(),
193            spec: "Store word then load word at same address yields same value.".into(),
194            sva_body: format!(
195                "(sw_valid && sw_addr == addr) |=> (lw_valid && lw_addr == addr) |-> (lw_data == sw_data)"
196            ),
197            kind: SvaAssertionKind::Assert,
198        },
199        ProtocolProperty {
200            name: "RISCV_Memory_Alignment".into(),
201            spec: "LW address is 4-byte aligned.".into(),
202            sva_body: "(opcode == 7'h03 && funct3 == 3'h2) |-> (addr[1:0] == 2'b00)".into(),
203            kind: SvaAssertionKind::Assert,
204        },
205    ]
206}
logicaffeine_compile/codegen_sva/protocols/riscv.rs

logicaffeine_compile/codegen_sva/protocols/
riscv.rs
