logicaffeine_compile/codegen_sva/protocols/
mod.rs

1//! Pre-Verified Protocol Templates
2//!
3//! Parameterizable SVA properties for standard hardware protocols.
4//! Each template produces SvaProperty + English spec string.
5
6pub mod riscv;
7
8use super::sva_model::SvaExpr;
9use super::SvaAssertionKind;
10
11/// A protocol template — produces parameterized SVA properties.
12#[derive(Debug, Clone)]
13pub struct ProtocolProperty {
14    pub name: String,
15    pub spec: String,
16    pub sva_body: String,
17    pub kind: SvaAssertionKind,
18}
19
20/// AXI4 write channel handshake properties.
21pub fn axi4_write_handshake(clock: &str) -> Vec<ProtocolProperty> {
22    vec![
23        ProtocolProperty {
24            name: "AXI_AW_Handshake".into(),
25            spec: "Always, if AWVALID is asserted, then eventually AWREADY responds.".into(),
26            sva_body: "AWVALID |-> s_eventually(AWREADY)".into(),
27            kind: SvaAssertionKind::Assert,
28        },
29        ProtocolProperty {
30            name: "AXI_W_Follows_AW".into(),
31            spec: "Always, if the address handshake completes, then eventually WVALID is asserted.".into(),
32            sva_body: "(AWVALID && AWREADY) |-> s_eventually(WVALID)".into(),
33            kind: SvaAssertionKind::Assert,
34        },
35        ProtocolProperty {
36            name: "AXI_B_Follows_W".into(),
37            spec: "Always, if the write data handshake completes, then eventually BVALID is asserted.".into(),
38            sva_body: "(WVALID && WREADY) |-> s_eventually(BVALID)".into(),
39            kind: SvaAssertionKind::Assert,
40        },
41    ]
42}
43
44/// APB setup/access phase properties.
45pub fn apb_protocol(clock: &str) -> Vec<ProtocolProperty> {
46    vec![
47        ProtocolProperty {
48            name: "APB_Setup_Phase".into(),
49            spec: "Always, if PSEL is asserted without PENABLE, then PENABLE follows next cycle.".into(),
50            sva_body: "(PSEL && !PENABLE) |=> PENABLE".into(),
51            kind: SvaAssertionKind::Assert,
52        },
53        ProtocolProperty {
54            name: "APB_Ready_In_Access".into(),
55            spec: "Always, if PSEL and PENABLE are both asserted, eventually PREADY responds.".into(),
56            sva_body: "(PSEL && PENABLE) |-> s_eventually(PREADY)".into(),
57            kind: SvaAssertionKind::Assert,
58        },
59    ]
60}
61
62/// UART transmit properties.
63pub fn uart_tx(clock: &str) -> Vec<ProtocolProperty> {
64    vec![
65        ProtocolProperty {
66            name: "UART_TX_Busy".into(),
67            spec: "Always, if tx_start is asserted, then tx_busy holds until transmission completes.".into(),
68            sva_body: "tx_start |-> s_eventually(tx_busy)".into(),
69            kind: SvaAssertionKind::Assert,
70        },
71    ]
72}
73
74/// SPI properties.
75pub fn spi_protocol(clock: &str) -> Vec<ProtocolProperty> {
76    vec![
77        ProtocolProperty {
78            name: "SPI_MOSI_Stable".into(),
79            spec: "Always, when chip select is active, MOSI is stable on the clock edge.".into(),
80            sva_body: "!ss |-> $stable(mosi)".into(),
81            kind: SvaAssertionKind::Assert,
82        },
83    ]
84}
85
86/// I2C properties.
87pub fn i2c_protocol(clock: &str) -> Vec<ProtocolProperty> {
88    vec![
89        ProtocolProperty {
90            name: "I2C_Start_Condition".into(),
91            spec: "A start condition is SDA falling while SCL is high.".into(),
92            sva_body: "$fell(sda) && scl".into(),
93            kind: SvaAssertionKind::Cover,
94        },
95        ProtocolProperty {
96            name: "I2C_Stop_Condition".into(),
97            spec: "A stop condition is SDA rising while SCL is high.".into(),
98            sva_body: "$rose(sda) && scl".into(),
99            kind: SvaAssertionKind::Cover,
100        },
101    ]
102}
logicaffeine_compile/codegen_sva/protocols/mod.rs

logicaffeine_compile/codegen_sva/protocols/
mod.rs
