bitloom_sim/
ip_dual.rs

1//! FR103 — first-class IP dual-model matrix (NFR14 FIFO/UART/SPI/I2C/AXI).
2//!
3//! Cycle path = FrozenHir [`crate::Sim::tick`]. Functional path =
4//! [`crate::GeneratedFunctional`] (generation path) **or** handwritten
5//! [`SyncFifoFunctional`] when FR103 nails architectural FL for Mem-based FIFO.
6//! **FR126** adds handwritten [`GpioFunctional`]; **FR135** adds handwritten
7//! [`UartTxFunctional`]; **FR163** adds handwritten [`UartRxFunctional`] beyond
8//! UartTx / Gpio / GeneratedFunctional alone; **FR168** adds handwritten
9//! [`SpiMasterFunctional`] / [`I2cMasterFunctional`] / [`Axi4LiteSlaveFunctional`]
10//! (all three; ≠ FR163 alone; ≠ GeneratedFunctional alone).
11//!
12//! Design crates stay on `bitloom-prelude`; this module lives in the toolchain.
13
14use bitloom_hir::{FrozenHir, PortValues};
15
16use crate::{
17    AbstractionView, EquivStatus, FormalEquivProduct, PortMismatch, Sim, check_functional_equiv,
18    compare_port_values,
19};
20
21/// Depth-4 SyncFifo functional model (architectural PortValues).
22///
23/// FR103 completion face for FIFO. **FR112** separately deepens
24/// `GeneratedFunctional` MemRead≡tick; that path does not replace this
25/// handwritten SyncFifo FL (see `docs/fr103-ip-dual-model.md`).
26#[derive(Debug, Clone, Default)]
27pub struct SyncFifoFunctional {
28    ram: [u64; 4],
29    wr_ptr: u8,
30    rd_ptr: u8,
31    count: u8,
32    dout: u64,
33}
34
35impl SyncFifoFunctional {
36    pub fn new() -> Self {
37        Self::default()
38    }
39}
40
41impl AbstractionView for SyncFifoFunctional {
42    fn cycle(&mut self, inputs: &PortValues) -> PortValues {
43        let rst = inputs.get("rst").unwrap_or(0) != 0;
44        let wr_en = inputs.get("wr_en").unwrap_or(0) != 0;
45        let rd_en = inputs.get("rd_en").unwrap_or(0) != 0;
46        let data_in = inputs.get("data_in").unwrap_or(0);
47
48        if rst {
49            self.ram = [0; 4];
50            self.wr_ptr = 0;
51            self.rd_ptr = 0;
52            self.count = 0;
53            self.dout = 0;
54        } else {
55            // Match SyncFifo HIR order: mem write (if can_wr), then async
56            // dout := ram[rd_ptr], then advance pointers/count.
57            let full = self.count >= 4;
58            let empty = self.count == 0;
59            let can_wr = wr_en && !full;
60            let can_rd = rd_en && !empty;
61
62            if can_wr {
63                self.ram[self.wr_ptr as usize % 4] = data_in & 0xff;
64            }
65            // Unconditional async-style head peek (assign_reg_d_mem_read on declare_mem).
66            self.dout = self.ram[self.rd_ptr as usize % 4];
67
68            if can_wr {
69                self.wr_ptr = self.wr_ptr.wrapping_add(1) & 0b11;
70            }
71            if can_rd {
72                self.rd_ptr = self.rd_ptr.wrapping_add(1) & 0b11;
73            }
74            match (can_wr, can_rd) {
75                (true, true) => {}
76                (true, false) => self.count = self.count.saturating_add(1).min(4),
77                (false, true) => self.count = self.count.saturating_sub(1),
78                (false, false) => {}
79            }
80        }
81
82        let mut out = inputs.clone();
83        out.set("full", u64::from(self.count >= 4));
84        out.set("empty", u64::from(self.count == 0));
85        out.set("data_out", self.dout);
86        out
87    }
88}
89
90/// Documented SyncFifo dual-model stimulus (reset, push, pop) — FR103 fixture.
91pub fn sync_fifo_dual_stimulus() -> Vec<PortValues> {
92    let mut out = Vec::new();
93    let mut frame = |rst: u64, wr_en: u64, rd_en: u64, data_in: u64| {
94        let mut pv = PortValues::default();
95        pv.set("rst", rst);
96        pv.set("wr_en", wr_en);
97        pv.set("rd_en", rd_en);
98        pv.set("data_in", data_in);
99        out.push(pv);
100    };
101    frame(1, 0, 0, 0);
102    frame(0, 1, 0, 0x11);
103    frame(0, 1, 0, 0x22);
104    frame(0, 0, 1, 0);
105    frame(0, 0, 1, 0);
106    frame(0, 0, 0, 0);
107    out
108}
109
110/// Handwritten `Gpio` FL (FR126) — beyond FR103 SyncFifo / GeneratedFunctional UART–AXI.
111///
112/// Models architectural ports `pad_out` / `rd_data` ≡ `Sim::tick` on
113/// [`gpio_dual_stimulus`]. Not GeneratedFunctional; not FR112 MemRead≡tick;
114/// not FR119 sby alone.
115#[derive(Debug, Clone, Default)]
116pub struct GpioFunctional {
117    out_r: u64,
118}
119
120impl GpioFunctional {
121    pub fn new() -> Self {
122        Self::default()
123    }
124}
125
126impl AbstractionView for GpioFunctional {
127    fn cycle(&mut self, inputs: &PortValues) -> PortValues {
128        let rst = inputs.get("rst").unwrap_or(0) != 0;
129        let dir = inputs.get("dir").unwrap_or(0) & 0xff;
130        let wr_en = inputs.get("wr_en").unwrap_or(0) != 0;
131        let wr_data = inputs.get("wr_data").unwrap_or(0) & 0xff;
132        let wr_mask = inputs.get("wr_mask").unwrap_or(0) & 0xff;
133        let pad_in = inputs.get("pad_in").unwrap_or(0) & 0xff;
134
135        if rst {
136            self.out_r = 0;
137        } else if wr_en {
138            let kept = self.out_r & (!wr_mask & 0xff);
139            let newt = wr_data & wr_mask;
140            self.out_r = (kept | newt) & 0xff;
141        }
142
143        let pad_out = self.out_r & dir;
144        let rd_data = (self.out_r & dir) | (pad_in & (!dir & 0xff));
145
146        let mut out = inputs.clone();
147        out.set("pad_out", pad_out);
148        out.set("rd_data", rd_data);
149        out
150    }
151}
152
153/// Documented Gpio dual-model stimulus (reset, masked write, pad read) — FR126.
154pub fn gpio_dual_stimulus() -> Vec<PortValues> {
155    let mut out = Vec::new();
156    let mut frame = |rst: u64, dir: u64, wr_en: u64, wr_data: u64, wr_mask: u64, pad_in: u64| {
157        let mut pv = PortValues::default();
158        pv.set("rst", rst);
159        pv.set("dir", dir);
160        pv.set("wr_en", wr_en);
161        pv.set("wr_data", wr_data);
162        pv.set("wr_mask", wr_mask);
163        pv.set("pad_in", pad_in);
164        out.push(pv);
165    };
166    frame(1, 0xff, 0, 0, 0, 0);
167    frame(0, 0xff, 1, 0xa5, 0xff, 0);
168    frame(0, 0xff, 0, 0, 0, 0);
169    frame(0, 0x0f, 0, 0, 0, 0xf0); // lower nybble out, upper from pad
170    frame(0, 0x0f, 1, 0x03, 0x0f, 0xf0);
171    frame(0, 0x0f, 0, 0, 0, 0xaa);
172    out
173}
174
175/// Handwritten `UartTx` FL (FR135) — beyond FR126 Gpio / FR103 SyncFifo / GeneratedFunctional.
176///
177/// Models architectural ports `tx` / `tx_byte` / `tx_busy` ≡ `Sim::settle`+`tick` on
178/// [`uart_tx_dual_stimulus`]. Not GeneratedFunctional; not Gpio alone; not SyncFifo alone.
179#[derive(Debug, Clone, Default)]
180pub struct UartTxFunctional {
181    hold: u64,
182    shift_reg: u64,
183    busy: u64,
184    bit_idx: u64,
185    baud_cnt: u64,
186}
187
188impl UartTxFunctional {
189    pub fn new() -> Self {
190        Self::default()
191    }
192}
193
194impl AbstractionView for UartTxFunctional {
195    fn cycle(&mut self, inputs: &PortValues) -> PortValues {
196        let rst = inputs.get("rst").unwrap_or(0) != 0;
197        let wr_en = inputs.get("wr_en").unwrap_or(0) != 0;
198        let wr_data = inputs.get("wr_data").unwrap_or(0) & 0xff;
199        let baud_div = inputs.get("baud_div").unwrap_or(0) & 0xff;
200
201        if rst {
202            self.hold = 0;
203            self.shift_reg = 0;
204            self.busy = 0;
205            self.bit_idx = 0;
206            self.baud_cnt = 0;
207        } else {
208            let busy = self.busy != 0;
209            let accept = wr_en && !busy;
210            let is_start = self.bit_idx == 0;
211            let is_stop = self.bit_idx == 9;
212            let baud_eq = self.baud_cnt == baud_div;
213            let baud_tick = busy && baud_eq;
214
215            let baud_cnt_busy = if baud_eq {
216                0
217            } else {
218                self.baud_cnt.wrapping_add(1) & 0xff
219            };
220            let baud_cnt_busy_or_idle = if busy { baud_cnt_busy } else { 0 };
221            let next_baud_cnt = if accept { 0 } else { baud_cnt_busy_or_idle };
222
223            let busy_after_tick = if is_stop { 0 } else { 1 };
224            let busy_when_busy = if baud_tick { busy_after_tick } else { 1 };
225            let busy_when_busy_or_idle = if busy { busy_when_busy } else { 0 };
226            let next_busy = if accept { 1 } else { busy_when_busy_or_idle };
227
228            let bit_idx_p1 = (self.bit_idx.wrapping_add(1)) & 0xf;
229            let bit_after_tick = if is_stop { 0 } else { bit_idx_p1 };
230            let bit_when_busy = if baud_tick {
231                bit_after_tick
232            } else {
233                self.bit_idx
234            };
235            let bit_when_busy_or_idle = if busy { bit_when_busy } else { 0 };
236            let next_bit_idx = if accept { 0 } else { bit_when_busy_or_idle };
237
238            let do_shift = busy && !is_start && !is_stop;
239            let do_shift_tick = do_shift && baud_eq;
240            let shift_shr = (self.shift_reg >> 1) & 0xff;
241            let shift_after_tick = if do_shift_tick {
242                shift_shr
243            } else {
244                self.shift_reg
245            };
246            let next_shift_busy = if busy {
247                shift_after_tick
248            } else {
249                self.shift_reg
250            };
251            let next_shift_final = if accept { wr_data } else { next_shift_busy };
252            let next_hold = if accept { wr_data } else { self.hold };
253
254            self.busy = next_busy;
255            self.bit_idx = next_bit_idx;
256            self.shift_reg = next_shift_final;
257            self.hold = next_hold;
258            self.baud_cnt = next_baud_cnt;
259        }
260
261        let busy = self.busy != 0;
262        let is_start = self.bit_idx == 0;
263        let is_stop = self.bit_idx == 9;
264        let data_bit = (self.shift_reg & 1) != 0;
265        let tx_data_or_stop = if is_stop { 1 } else { u64::from(data_bit) };
266        let tx_active = if is_start { 0 } else { tx_data_or_stop };
267        let tx = if busy { tx_active } else { 1 };
268
269        let mut out = inputs.clone();
270        out.set("tx", tx);
271        out.set("tx_byte", self.hold & 0xff);
272        out.set("tx_busy", self.busy & 1);
273        out
274    }
275}
276
277/// Documented UartTx dual-model stimulus (reset, 8N1 frame, baud_div hold) — FR135.
278pub fn uart_tx_dual_stimulus() -> Vec<PortValues> {
279    let mut out = Vec::new();
280    let mut frame = |rst: u64, wr_en: u64, wr_data: u64, baud_div: u64| {
281        let mut pv = PortValues::default();
282        pv.set("rst", rst);
283        pv.set("wr_en", wr_en);
284        pv.set("wr_data", wr_data);
285        pv.set("baud_div", baud_div);
286        out.push(pv);
287    };
288    // baud_div=0: 1 clk/bit — full 0xA5 frame + idle clear
289    frame(1, 0, 0, 0);
290    frame(0, 0, 0, 0);
291    frame(0, 1, 0xa5, 0); // accept → start
292    for _ in 0..9 {
293        frame(0, 0, 0, 0); // data…stop
294    }
295    frame(0, 0, 0, 0); // clear busy
296    // baud_div=1: 2 clk/bit — start held then LSB
297    frame(1, 0, 0, 1);
298    frame(0, 1, 0x01, 1);
299    frame(0, 0, 0, 1); // start held
300    frame(0, 0, 0, 1); // LSB
301    // busy ignore: latch 0x3C, wr_en with 0xFF must not replace
302    frame(1, 0, 0, 0);
303    frame(0, 1, 0x3c, 0);
304    frame(0, 1, 0xff, 0);
305    frame(0, 0, 0, 0);
306    out
307}
308
309/// Handwritten `UartRx` FL (FR163) — beyond FR135 `UartTx` / FR126 Gpio / GeneratedFunctional.
310///
311/// Models architectural ports `rd_data` / `rd_valid` / `rx_busy` ≡ `Sim::settle`+`tick` on
312/// [`uart_rx_dual_stimulus`]. Not GeneratedFunctional; not UartTx alone; not Gpio alone.
313#[derive(Debug, Clone, Default)]
314pub struct UartRxFunctional {
315    rx_prev: u64,
316    busy: u64,
317    bit_idx: u64,
318    baud_cnt: u64,
319    shift_reg: u64,
320    hold: u64,
321    valid: u64,
322}
323
324impl UartRxFunctional {
325    pub fn new() -> Self {
326        Self::default()
327    }
328}
329
330impl AbstractionView for UartRxFunctional {
331    fn cycle(&mut self, inputs: &PortValues) -> PortValues {
332        let rst = inputs.get("rst").unwrap_or(0) != 0;
333        let rx = inputs.get("rx").unwrap_or(1) & 1;
334        let baud_div = inputs.get("baud_div").unwrap_or(0) & 0xff;
335
336        if rst {
337            self.rx_prev = 0;
338            self.busy = 0;
339            self.bit_idx = 0;
340            self.baud_cnt = 0;
341            self.shift_reg = 0;
342            self.hold = 0;
343            self.valid = 0;
344        } else {
345            let busy = self.busy != 0;
346            let fall = self.rx_prev == 1 && rx == 0;
347            let start = !busy && fall;
348            let is_stop = self.bit_idx == 9;
349            let baud_eq = self.baud_cnt == baud_div;
350            let baud_tick = busy && baud_eq;
351
352            let baud_cnt_busy = if baud_eq {
353                0
354            } else {
355                self.baud_cnt.wrapping_add(1) & 0xff
356            };
357            let baud_cnt_busy_or_idle = if busy { baud_cnt_busy } else { 0 };
358            let next_baud_cnt = if start { 0 } else { baud_cnt_busy_or_idle };
359
360            let do_sample = baud_tick && !is_stop;
361            let do_finish = baud_tick && is_stop;
362
363            let shift_shr = (self.shift_reg >> 1) & 0xff;
364            let rx8 = if rx != 0 { 0x80 } else { 0 };
365            let shift_in = shift_shr | rx8;
366
367            let busy_after_tick = if is_stop { 0 } else { 1 };
368            let busy_when_busy = if baud_tick { busy_after_tick } else { 1 };
369            let busy_when_busy_or_idle = if busy { busy_when_busy } else { 0 };
370            let next_busy = if start { 1 } else { busy_when_busy_or_idle };
371
372            let bit_idx_p1 = (self.bit_idx.wrapping_add(1)) & 0xf;
373            let bit_after_tick = if is_stop { 0 } else { bit_idx_p1 };
374            let bit_when_busy = if baud_tick {
375                bit_after_tick
376            } else {
377                self.bit_idx
378            };
379            let bit_when_busy_or_idle = if busy { bit_when_busy } else { 0 };
380            let next_bit_idx = if start { 1 } else { bit_when_busy_or_idle };
381
382            let shift_after_sample = if do_sample { shift_in } else { self.shift_reg };
383            let next_shift_busy = if busy {
384                shift_after_sample
385            } else {
386                self.shift_reg
387            };
388            let next_shift = if start { 0 } else { next_shift_busy };
389
390            let next_hold = if do_finish { self.shift_reg } else { self.hold };
391            let next_valid = if do_finish { 1 } else { 0 };
392
393            self.rx_prev = rx;
394            self.busy = next_busy;
395            self.bit_idx = next_bit_idx;
396            self.baud_cnt = next_baud_cnt;
397            self.shift_reg = next_shift;
398            self.hold = next_hold;
399            self.valid = next_valid;
400        }
401
402        let mut out = inputs.clone();
403        out.set("rd_data", self.hold & 0xff);
404        out.set("rd_valid", self.valid & 1);
405        out.set("rx_busy", self.busy & 1);
406        out
407    }
408}
409
410/// Documented UartRx dual-model stimulus (reset, 8N1 RX frame, baud_div hold) — FR163.
411pub fn uart_rx_dual_stimulus() -> Vec<PortValues> {
412    let mut out = Vec::new();
413    let mut frame = |rst: u64, rx: u64, baud_div: u64| {
414        let mut pv = PortValues::default();
415        pv.set("rst", rst);
416        pv.set("rx", rx);
417        pv.set("baud_div", baud_div);
418        out.push(pv);
419    };
420    // baud_div=0: 1 clk/bit — 0xA5 LSB-first (matches prelude uart_rx smoke)
421    frame(1, 1, 0);
422    frame(0, 1, 0);
423    // start + data 0b1010_0101 LSB-first + stop
424    for &b in &[0u64, 1, 0, 1, 0, 0, 1, 0, 1, 1] {
425        frame(0, b, 0);
426    }
427    frame(0, 1, 0); // idle after valid
428    // baud_div=1: 2 clk/bit — start held then sample 0x01 (LSB=1)
429    frame(1, 1, 1);
430    frame(0, 1, 1);
431    frame(0, 0, 1); // fall → start
432    frame(0, 0, 1); // start held (baud_cnt 0→1)
433    frame(0, 1, 1); // sample bit0=1 @ baud_tick; bit_idx 1→2
434    frame(0, 1, 1); // hold
435    for _ in 0..7 {
436        // remaining data 0 + stop, 2 clk each
437        frame(0, 0, 1);
438        frame(0, 0, 1);
439    }
440    frame(0, 1, 1); // stop held
441    frame(0, 1, 1); // finish
442    out
443}
444
445/// Architectural ports compared for SyncFifo dual-model (avoid internal wires).
446const SYNC_FIFO_ARCH_PORTS: &[&str] = &["full", "empty", "data_out"];
447
448/// Architectural ports for Gpio handwritten FL (FR126).
449const GPIO_ARCH_PORTS: &[&str] = &["pad_out", "rd_data"];
450
451/// Architectural ports for UartTx handwritten FL (FR135).
452const UART_TX_ARCH_PORTS: &[&str] = &["tx", "tx_byte", "tx_busy"];
453
454/// Architectural ports for UartRx handwritten FL (FR163).
455const UART_RX_ARCH_PORTS: &[&str] = &["rd_data", "rd_valid", "rx_busy"];
456
457/// Architectural ports for SpiMaster handwritten FL (FR168).
458const SPI_MASTER_ARCH_PORTS: &[&str] = &[
459    "mosi_byte",
460    "rx_data",
461    "rx_valid",
462    "busy",
463    "cs_n",
464    "sclk",
465    "mosi",
466];
467
468/// Architectural ports for I2cMaster handwritten FL (FR168).
469const I2C_MASTER_ARCH_PORTS: &[&str] = &[
470    "tx_byte",
471    "busy",
472    "scl",
473    "sda_out",
474    "rx_data",
475    "rx_valid",
476    "ack_error",
477];
478
479/// Architectural ports for Axi4LiteSlave handwritten FL (FR168).
480const AXI4_LITE_SLAVE_ARCH_PORTS: &[&str] = &[
481    "s_axi_awready",
482    "s_axi_wready",
483    "s_axi_bresp",
484    "s_axi_bvalid",
485    "s_axi_arready",
486    "s_axi_rdata",
487    "s_axi_rresp",
488    "s_axi_rvalid",
489];
490
491/// Handwritten `SpiMaster` FL (FR168) — Mode-0 single-byte path ≡ tick on
492/// [`spi_master_dual_stimulus`]. Not GeneratedFunctional; not FR163 UartRx alone.
493#[derive(Debug, Clone, Default)]
494pub struct SpiMasterFunctional {
495    hold: u64,
496    shift: u64,
497    rx_shift: u64,
498    rx_hold: u64,
499    busy_r: u64,
500    bit_idx: u64,
501    half: u64,
502    bytes_left: u64,
503    valid_r: u64,
504    mosi_r: u64,
505}
506
507impl SpiMasterFunctional {
508    pub fn new() -> Self {
509        Self::default()
510    }
511}
512
513impl AbstractionView for SpiMasterFunctional {
514    fn cycle(&mut self, inputs: &PortValues) -> PortValues {
515        let rst = inputs.get("rst").unwrap_or(0) != 0;
516        let start = inputs.get("start").unwrap_or(0) != 0;
517        let tx_data = inputs.get("tx_data").unwrap_or(0) & 0xff;
518        let miso = inputs.get("miso").unwrap_or(0) & 1;
519        let cpol = inputs.get("cpol").unwrap_or(0) & 1;
520        let cpha = inputs.get("cpha").unwrap_or(0) & 1;
521        let byte_count = inputs.get("byte_count").unwrap_or(0) & 0x7;
522
523        if rst {
524            *self = Self::default();
525        } else {
526            let busy = self.busy_r != 0;
527            let accept = start && !busy;
528            let eff_count = if byte_count == 0 { 1 } else { byte_count };
529            let cpha0 = cpha == 0;
530            let half0 = self.half == 0;
531            let is_last_bit = self.bit_idx == 7;
532            let is_last_byte = self.bytes_left == 1;
533            let tx_msb = u64::from((tx_data & 0x80) != 0);
534            let accept_mosi = if cpha0 { tx_msb } else { 0 };
535            let shift_shl8 = (self.shift << 1) & 0xff;
536            let sh8_msb = u64::from((shift_shl8 & 0x80) != 0);
537            let sh_msb = u64::from((self.shift & 0x80) != 0);
538            let rx_sampled = ((self.rx_shift << 1) & 0xff) | miso;
539            let bit_p1 = (self.bit_idx.wrapping_add(1)) & 0xf;
540            let bytes_m1 = (self.bytes_left.wrapping_sub(1)) & 0x7;
541
542            let do_lead = busy && half0;
543            let do_trail = busy && !half0;
544            let sample_lead = do_lead && cpha0;
545            let launch_lead = do_lead && !cpha0;
546            let shift_trail = do_trail && cpha0;
547            let sample_trail = do_trail && !cpha0;
548            let finish_byte = do_trail && is_last_bit;
549            let cont_frame = finish_byte && !is_last_byte;
550            let end_frame = finish_byte && is_last_byte;
551
552            let lead_shift = if launch_lead { shift_shl8 } else { self.shift };
553            let lead_mosi = if launch_lead { sh_msb } else { self.mosi_r };
554            let lead_rxsh = if sample_lead {
555                rx_sampled
556            } else {
557                self.rx_shift
558            };
559
560            let tr_shift0 = if shift_trail { shift_shl8 } else { self.shift };
561            let tr_mosi0 = if shift_trail { sh8_msb } else { self.mosi_r };
562            let tr_rxsh0 = if sample_trail {
563                rx_sampled
564            } else {
565                self.rx_shift
566            };
567            let tr_valid = u64::from(finish_byte);
568            let tr_busy = if end_frame { 0 } else { 1 };
569            let tr_bit = if finish_byte { 0 } else { bit_p1 };
570            let tr_bytes = if cont_frame {
571                bytes_m1
572            } else {
573                self.bytes_left
574            };
575            let tr_hold = if cont_frame { tx_data } else { self.hold };
576            let tr_shift = if cont_frame { tx_data } else { tr_shift0 };
577            let tr_mosi = if cont_frame { accept_mosi } else { tr_mosi0 };
578            let tr_rxh = if finish_byte { tr_rxsh0 } else { self.rx_hold };
579            let tr_rxsh = if finish_byte { 0 } else { tr_rxsh0 };
580
581            let b_half = if do_lead { 1 } else { 0 };
582            let b_bit = if do_trail { tr_bit } else { self.bit_idx };
583            let b_bytes = if do_trail { tr_bytes } else { self.bytes_left };
584            let b_hold = if do_trail { tr_hold } else { self.hold };
585            let b_shift = if do_trail { tr_shift } else { lead_shift };
586            let b_rxsh = if do_trail { tr_rxsh } else { lead_rxsh };
587            let b_rxh = if do_trail { tr_rxh } else { self.rx_hold };
588            let b_valid = if do_trail { tr_valid } else { 0 };
589            let b_mosi = if do_trail { tr_mosi } else { lead_mosi };
590            let b_busy = if do_trail { tr_busy } else { 1 };
591
592            let nb_busy = if busy { b_busy } else { 0 };
593            let nb_half = if busy { b_half } else { 0 };
594            let nb_bit = if busy { b_bit } else { 0 };
595            let nb_bytes = if busy { b_bytes } else { 0 };
596            let nb_shift = if busy { b_shift } else { self.shift };
597            let nb_rxsh = if busy { b_rxsh } else { self.rx_shift };
598            let nb_hold = if busy { b_hold } else { self.hold };
599            let nb_rxh = if busy { b_rxh } else { self.rx_hold };
600            let nb_valid = if busy { b_valid } else { 0 };
601            let nb_mosi = if busy { b_mosi } else { 0 };
602
603            self.busy_r = if accept { 1 } else { nb_busy };
604            self.half = if accept { 0 } else { nb_half };
605            self.bit_idx = if accept { 0 } else { nb_bit };
606            self.bytes_left = if accept { eff_count } else { nb_bytes };
607            self.shift = if accept { tx_data } else { nb_shift };
608            self.rx_shift = if accept { 0 } else { nb_rxsh };
609            self.hold = if accept { tx_data } else { nb_hold };
610            self.rx_hold = if accept { self.rx_hold } else { nb_rxh };
611            self.valid_r = if accept { 0 } else { nb_valid };
612            self.mosi_r = if accept { accept_mosi } else { nb_mosi };
613        }
614
615        let busy = self.busy_r != 0;
616        let sclk = if busy { cpol ^ (self.half & 1) } else { cpol };
617        let mut out = inputs.clone();
618        out.set("mosi_byte", self.hold & 0xff);
619        out.set("rx_data", self.rx_hold & 0xff);
620        out.set("rx_valid", self.valid_r & 1);
621        out.set("busy", self.busy_r & 1);
622        out.set("cs_n", u64::from(!busy));
623        out.set("sclk", sclk & 1);
624        out.set("mosi", if busy { self.mosi_r & 1 } else { 0 });
625        out
626    }
627}
628
629/// Documented SpiMaster dual-model stimulus (reset + Mode-0 single-byte RX) — FR168.
630pub fn spi_master_dual_stimulus() -> Vec<PortValues> {
631    let mut out = Vec::new();
632    let mut frame =
633        |rst: u64, start: u64, tx_data: u64, miso: u64, cpol: u64, cpha: u64, bc: u64| {
634            let mut pv = PortValues::default();
635            pv.set("rst", rst);
636            pv.set("start", start);
637            pv.set("tx_data", tx_data);
638            pv.set("miso", miso);
639            pv.set("cpol", cpol);
640            pv.set("cpha", cpha);
641            pv.set("byte_count", bc);
642            out.push(pv);
643        };
644    let tx = 0xa5u64;
645    // MISO MSB-first → 0x3C (matches fr98_spi_mode0_byte_transfer_rx)
646    let rx_bits = [0u64, 0, 1, 1, 1, 1, 0, 0];
647    frame(1, 0, 0, 0, 0, 0, 1);
648    frame(0, 0, 0, 0, 0, 0, 1);
649    frame(0, 1, tx, rx_bits[0], 0, 0, 1);
650    for &bit in &rx_bits {
651        frame(0, 0, 0, bit, 0, 0, 1); // lead sample
652        frame(0, 0, 0, bit, 0, 0, 1); // trail shift / finish
653    }
654    frame(0, 0, 0, 0, 0, 0, 1); // clear rx_valid
655    out
656}
657
658/// Handwritten `I2cMaster` FL (FR168) — write+ACK path ≡ tick on
659/// [`i2c_master_dual_stimulus`]. Not GeneratedFunctional; not FR163 alone.
660#[derive(Debug, Clone, Default)]
661pub struct I2cMasterFunctional {
662    hold: u64,
663    shift: u64,
664    rx_shift: u64,
665    rx_hold: u64,
666    busy_r: u64,
667    half: u64,
668    bit_idx: u64,
669    stage: u64,
670    rw_r: u64,
671    valid_r: u64,
672    ack_err_r: u64,
673}
674
675impl I2cMasterFunctional {
676    pub fn new() -> Self {
677        Self::default()
678    }
679}
680
681impl AbstractionView for I2cMasterFunctional {
682    fn cycle(&mut self, inputs: &PortValues) -> PortValues {
683        let rst = inputs.get("rst").unwrap_or(0) != 0;
684        let start = inputs.get("start").unwrap_or(0) != 0;
685        let addr = inputs.get("addr").unwrap_or(0) & 0xff;
686        let rw = inputs.get("rw").unwrap_or(0) & 1;
687        let tx_data = inputs.get("tx_data").unwrap_or(0) & 0xff;
688        let sda_in = inputs.get("sda_in").unwrap_or(1) & 1;
689
690        if rst {
691            *self = Self::default();
692        } else {
693            let busy = self.busy_r != 0;
694            let accept = start && !busy;
695            let addr_byte = ((addr << 1) & 0xfe) | rw;
696            let nack = sda_in != 0;
697            let rw_read = self.rw_r != 0;
698            let half0 = self.half == 0;
699            let is_last_bit = self.bit_idx == 7;
700            let shift_shl8 = (self.shift << 1) & 0xff;
701            let rx_sampled = ((self.rx_shift << 1) & 0xff) | sda_in;
702            let bit_p1 = (self.bit_idx.wrapping_add(1)) & 0xf;
703
704            let mut n_busy = 0u64;
705            let mut n_half = 0u64;
706            let mut n_bit = 0u64;
707            let mut n_stage = 0u64;
708            let mut n_shift = self.shift;
709            let mut n_hold = self.hold;
710            let mut n_rxsh = self.rx_shift;
711            let mut n_rxh = self.rx_hold;
712            let mut n_valid = 0u64;
713            let mut n_ackerr = self.ack_err_r;
714            let mut n_rw = self.rw_r;
715
716            if accept {
717                n_busy = 1;
718                n_half = 0;
719                n_bit = 0;
720                n_stage = 0;
721                n_shift = addr_byte;
722                n_hold = addr_byte;
723                n_rxsh = 0;
724                n_valid = 0;
725                n_ackerr = 0;
726                n_rw = rw;
727            } else if busy {
728                match self.stage {
729                    0 => {
730                        // START → ADDR
731                        n_busy = 1;
732                        n_half = 0;
733                        n_bit = 0;
734                        n_stage = 1;
735                    }
736                    1 => {
737                        // ADDR
738                        n_busy = 1;
739                        if half0 {
740                            n_half = 1;
741                            n_bit = self.bit_idx;
742                            n_stage = 1;
743                        } else {
744                            n_half = 0;
745                            n_shift = shift_shl8;
746                            if is_last_bit {
747                                n_bit = 0;
748                                n_stage = 2;
749                            } else {
750                                n_bit = bit_p1;
751                                n_stage = 1;
752                            }
753                        }
754                    }
755                    2 => {
756                        // AACK
757                        n_busy = 1;
758                        if half0 {
759                            n_half = 1;
760                            n_bit = self.bit_idx;
761                            n_stage = 2;
762                        } else {
763                            n_half = 0;
764                            n_bit = 0;
765                            if nack {
766                                n_stage = 5;
767                                n_ackerr = 1;
768                            } else {
769                                n_stage = 3;
770                                if rw_read {
771                                    n_rxsh = 0;
772                                } else {
773                                    n_shift = tx_data;
774                                    n_hold = tx_data;
775                                }
776                            }
777                        }
778                    }
779                    3 => {
780                        // DATA
781                        n_busy = 1;
782                        if half0 {
783                            n_half = 1;
784                            n_bit = self.bit_idx;
785                            n_stage = 3;
786                        } else {
787                            n_half = 0;
788                            n_shift = shift_shl8;
789                            if rw_read {
790                                n_rxsh = rx_sampled;
791                            }
792                            if is_last_bit {
793                                n_bit = 0;
794                                n_stage = 4;
795                            } else {
796                                n_bit = bit_p1;
797                                n_stage = 3;
798                            }
799                        }
800                    }
801                    4 => {
802                        // DACK
803                        n_busy = 1;
804                        if half0 {
805                            n_half = 1;
806                            n_bit = self.bit_idx;
807                            n_stage = 4;
808                        } else {
809                            n_half = 0;
810                            n_bit = self.bit_idx;
811                            n_stage = 5;
812                            if rw_read {
813                                n_valid = 1;
814                                n_rxh = self.rx_shift;
815                            } else if nack {
816                                n_ackerr = 1;
817                            }
818                        }
819                    }
820                    _ => {
821                        // STOP (5+)
822                        if half0 {
823                            n_busy = 1;
824                            n_half = 1;
825                            n_bit = self.bit_idx;
826                            n_stage = 5;
827                        } else {
828                            n_busy = 0;
829                            n_half = 0;
830                            n_bit = 0;
831                            n_stage = 0;
832                        }
833                    }
834                }
835            }
836
837            self.busy_r = n_busy;
838            self.half = n_half;
839            self.bit_idx = n_bit;
840            self.stage = n_stage;
841            self.shift = n_shift;
842            self.hold = n_hold;
843            self.rx_shift = n_rxsh;
844            self.rx_hold = n_rxh;
845            self.valid_r = n_valid;
846            self.ack_err_r = n_ackerr;
847            self.rw_r = n_rw;
848        }
849
850        let busy = self.busy_r != 0;
851        let msb = u64::from((self.shift & 0x80) != 0);
852        let sda_data = if self.rw_r != 0 { 1 } else { msb };
853        let sda_mid = if self.stage == 1 { msb } else { sda_data };
854        let is_ackph = self.stage == 2 || self.stage == 4;
855        let sda_or_ack = if is_ackph { 1 } else { sda_mid };
856        let is_lowdrv = self.stage == 0 || self.stage == 5;
857        let sda_active = if is_lowdrv { 0 } else { sda_or_ack };
858        let sda_out = if busy { sda_active } else { 1 };
859        let scl_busy = if self.stage == 0 { 1 } else { self.half & 1 };
860        let scl = if busy { scl_busy } else { 1 };
861
862        let mut out = inputs.clone();
863        out.set("tx_byte", self.hold & 0xff);
864        out.set("busy", self.busy_r & 1);
865        out.set("scl", scl & 1);
866        out.set("sda_out", sda_out & 1);
867        out.set("rx_data", self.rx_hold & 0xff);
868        out.set("rx_valid", self.valid_r & 1);
869        out.set("ack_error", self.ack_err_r & 1);
870        out
871    }
872}
873
874/// Documented I2cMaster dual-model stimulus (reset + write with ACK) — FR168.
875pub fn i2c_master_dual_stimulus() -> Vec<PortValues> {
876    let mut out = Vec::new();
877    let mut frame = |rst: u64, start: u64, addr: u64, rw: u64, tx_data: u64, sda_in: u64| {
878        let mut pv = PortValues::default();
879        pv.set("rst", rst);
880        pv.set("start", start);
881        pv.set("addr", addr);
882        pv.set("rw", rw);
883        pv.set("tx_data", tx_data);
884        pv.set("sda_in", sda_in);
885        out.push(pv);
886    };
887    let addr = 0x50u64;
888    let data = 0xa5u64;
889    frame(1, 0, 0, 0, 0, 1);
890    frame(0, 0, 0, 0, 0, 1);
891    frame(0, 1, addr, 0, data, 0);
892    // START→ADDR×16→AACK×2→DATA×16→DACK×2→STOP×2 = 39 post-start halves
893    for _ in 0..39 {
894        frame(0, 0, addr, 0, data, 0);
895    }
896    out
897}
898
899/// Handwritten `Axi4LiteSlave` FL (FR168) — write+read handshake ≡ tick on
900/// [`axi4_lite_slave_dual_stimulus`]. Not GeneratedFunctional; not FR163 alone.
901#[derive(Debug, Clone, Default)]
902pub struct Axi4LiteSlaveFunctional {
903    data0_r: u64,
904    data1_r: u64,
905    data2_r: u64,
906    data3_r: u64,
907    rdata_r: u64,
908    bvalid_r: u64,
909    rvalid_r: u64,
910}
911
912impl Axi4LiteSlaveFunctional {
913    pub fn new() -> Self {
914        Self::default()
915    }
916}
917
918impl AbstractionView for Axi4LiteSlaveFunctional {
919    fn cycle(&mut self, inputs: &PortValues) -> PortValues {
920        let rst = inputs.get("rst").unwrap_or(0) != 0;
921        let awaddr = inputs.get("s_axi_awaddr").unwrap_or(0) & 0xff;
922        let awvalid = inputs.get("s_axi_awvalid").unwrap_or(0) != 0;
923        let wdata = inputs.get("s_axi_wdata").unwrap_or(0) & 0xffff_ffff;
924        let wstrb = inputs.get("s_axi_wstrb").unwrap_or(0) & 0xf;
925        let wvalid = inputs.get("s_axi_wvalid").unwrap_or(0) != 0;
926        let bready = inputs.get("s_axi_bready").unwrap_or(0) != 0;
927        let araddr = inputs.get("s_axi_araddr").unwrap_or(0) & 0xff;
928        let arvalid = inputs.get("s_axi_arvalid").unwrap_or(0) != 0;
929        let rready = inputs.get("s_axi_rready").unwrap_or(0) != 0;
930
931        if rst {
932            *self = Self::default();
933        } else {
934            let aw_ready = self.bvalid_r == 0;
935            let ar_ready = self.rvalid_r == 0 && self.bvalid_r == 0;
936            let do_write = awvalid && aw_ready && wvalid;
937            let do_read = !do_write && arvalid && ar_ready;
938            let b_fire = self.bvalid_r != 0 && bready;
939            let r_fire = self.rvalid_r != 0 && rready;
940
941            let mut byte_mask = 0u64;
942            if wstrb & 1 != 0 {
943                byte_mask |= 0x0000_00ff;
944            }
945            if wstrb & 2 != 0 {
946                byte_mask |= 0x0000_ff00;
947            }
948            if wstrb & 4 != 0 {
949                byte_mask |= 0x00ff_0000;
950            }
951            if wstrb & 8 != 0 {
952                byte_mask |= 0xff00_0000;
953            }
954            let byte_mask_n = (!byte_mask) & 0xffff_ffff;
955            let wdata_m = wdata & byte_mask;
956
957            let merge = |old: u64| (wdata_m) | (old & byte_mask_n);
958            if do_write {
959                match awaddr {
960                    0x00 => self.data0_r = merge(self.data0_r),
961                    0x04 => self.data1_r = merge(self.data1_r),
962                    0x08 => self.data2_r = merge(self.data2_r),
963                    0x0c => self.data3_r = merge(self.data3_r),
964                    _ => {}
965                }
966            }
967
968            let rdata_mux = match araddr {
969                0x00 => self.data0_r,
970                0x04 => self.data1_r,
971                0x08 => self.data2_r,
972                0x0c => self.data3_r,
973                _ => 0,
974            };
975            if do_read {
976                self.rdata_r = rdata_mux;
977            }
978
979            self.bvalid_r = if do_write {
980                1
981            } else if b_fire {
982                0
983            } else {
984                self.bvalid_r
985            };
986            self.rvalid_r = if do_read {
987                1
988            } else if r_fire {
989                0
990            } else {
991                self.rvalid_r
992            };
993        }
994
995        let aw_ready = self.bvalid_r == 0;
996        let ar_ready = self.rvalid_r == 0 && self.bvalid_r == 0;
997        let mut out = inputs.clone();
998        out.set("s_axi_awready", u64::from(aw_ready));
999        out.set("s_axi_wready", u64::from(aw_ready));
1000        out.set("s_axi_bresp", 0);
1001        out.set("s_axi_bvalid", self.bvalid_r & 1);
1002        out.set("s_axi_arready", u64::from(ar_ready));
1003        out.set("s_axi_rdata", self.rdata_r & 0xffff_ffff);
1004        out.set("s_axi_rresp", 0);
1005        out.set("s_axi_rvalid", self.rvalid_r & 1);
1006        out
1007    }
1008}
1009
1010/// Documented Axi4LiteSlave dual-model stimulus (reset + write + read) — FR168.
1011pub fn axi4_lite_slave_dual_stimulus() -> Vec<PortValues> {
1012    let mut out = Vec::new();
1013    let mut frame = |rst: u64,
1014                     awaddr: u64,
1015                     awvalid: u64,
1016                     wdata: u64,
1017                     wstrb: u64,
1018                     wvalid: u64,
1019                     bready: u64,
1020                     araddr: u64,
1021                     arvalid: u64,
1022                     rready: u64| {
1023        let mut pv = PortValues::default();
1024        pv.set("rst", rst);
1025        pv.set("s_axi_awaddr", awaddr);
1026        pv.set("s_axi_awvalid", awvalid);
1027        pv.set("s_axi_wdata", wdata);
1028        pv.set("s_axi_wstrb", wstrb);
1029        pv.set("s_axi_wvalid", wvalid);
1030        pv.set("s_axi_bready", bready);
1031        pv.set("s_axi_araddr", araddr);
1032        pv.set("s_axi_arvalid", arvalid);
1033        pv.set("s_axi_rready", rready);
1034        out.push(pv);
1035    };
1036    frame(1, 0, 0, 0, 0, 0, 0, 0, 0, 0);
1037    frame(0, 0, 0, 0, 0, 0, 0, 0, 0, 0);
1038    frame(0, 0x00, 1, 0xdead_beef, 0xf, 1, 0, 0, 0, 0);
1039    frame(0, 0, 0, 0, 0, 0, 1, 0, 0, 0);
1040    frame(0, 0, 0, 0, 0, 0, 0, 0x00, 1, 0);
1041    frame(0, 0, 0, 0, 0, 0, 0, 0, 0, 1);
1042    out
1043}
1044
1045/// FR103 product entry: co-verify functional + cycle models for the NFR14 IP set.
1046#[derive(Debug, Clone, Default)]
1047pub struct IpDualModelMatrix;
1048
1049impl IpDualModelMatrix {
1050    pub fn new() -> Self {
1051        Self
1052    }
1053
1054    /// SyncFifo: handwritten FL vs `settle`+`tick` on pinned stimulus.
1055    pub fn verify_sync_fifo(&self, hir: FrozenHir) -> EquivStatus {
1056        let mut sim = Sim::new(hir);
1057        let mut fl = SyncFifoFunctional::new();
1058        let mut cycles = 0usize;
1059        for inputs in sync_fifo_dual_stimulus() {
1060            sim.set_inputs(inputs.clone());
1061            sim.settle();
1062            sim.tick();
1063            let abs_out = fl.cycle(&inputs);
1064            if let Err(mismatches) =
1065                compare_named_ports(sim.ports(), &abs_out, SYNC_FIFO_ARCH_PORTS)
1066            {
1067                return EquivStatus::Fail {
1068                    cycle: cycles,
1069                    mismatches,
1070                };
1071            }
1072            cycles += 1;
1073        }
1074        EquivStatus::Pass { cycles }
1075    }
1076
1077    /// Deliberate mismatch ATDD for SyncFifo.
1078    pub fn verify_sync_fifo_with<A: AbstractionView>(
1079        &self,
1080        hir: FrozenHir,
1081        abs: &mut A,
1082    ) -> EquivStatus {
1083        let mut sim = Sim::new(hir);
1084        let mut cycles = 0usize;
1085        for inputs in sync_fifo_dual_stimulus() {
1086            sim.set_inputs(inputs.clone());
1087            sim.settle();
1088            sim.tick();
1089            let abs_out = abs.cycle(&inputs);
1090            if let Err(mismatches) =
1091                compare_named_ports(sim.ports(), &abs_out, SYNC_FIFO_ARCH_PORTS)
1092            {
1093                return EquivStatus::Fail {
1094                    cycle: cycles,
1095                    mismatches,
1096                };
1097            }
1098            cycles += 1;
1099        }
1100        EquivStatus::Pass { cycles }
1101    }
1102
1103    /// FR126: handwritten `Gpio` FL ≡ tick on [`gpio_dual_stimulus`].
1104    pub fn verify_gpio_handwritten(&self, hir: FrozenHir) -> EquivStatus {
1105        let mut sim = Sim::new(hir);
1106        let mut fl = GpioFunctional::new();
1107        let mut cycles = 0usize;
1108        for inputs in gpio_dual_stimulus() {
1109            sim.set_inputs(inputs.clone());
1110            sim.settle();
1111            sim.tick();
1112            let abs_out = fl.cycle(&inputs);
1113            if let Err(mismatches) = compare_named_ports(sim.ports(), &abs_out, GPIO_ARCH_PORTS) {
1114                return EquivStatus::Fail {
1115                    cycle: cycles,
1116                    mismatches,
1117                };
1118            }
1119            cycles += 1;
1120        }
1121        EquivStatus::Pass { cycles }
1122    }
1123
1124    /// FR135: handwritten `UartTx` FL ≡ tick on [`uart_tx_dual_stimulus`].
1125    pub fn verify_uart_tx_handwritten(&self, hir: FrozenHir) -> EquivStatus {
1126        let mut sim = Sim::new(hir);
1127        let mut fl = UartTxFunctional::new();
1128        let mut cycles = 0usize;
1129        for inputs in uart_tx_dual_stimulus() {
1130            sim.set_inputs(inputs.clone());
1131            sim.settle();
1132            sim.tick();
1133            let abs_out = fl.cycle(&inputs);
1134            if let Err(mismatches) = compare_named_ports(sim.ports(), &abs_out, UART_TX_ARCH_PORTS)
1135            {
1136                return EquivStatus::Fail {
1137                    cycle: cycles,
1138                    mismatches,
1139                };
1140            }
1141            cycles += 1;
1142        }
1143        EquivStatus::Pass { cycles }
1144    }
1145
1146    /// Deliberate mismatch / alternate FL ATDD for UartTx (FR135).
1147    pub fn verify_uart_tx_handwritten_with<A: AbstractionView>(
1148        &self,
1149        hir: FrozenHir,
1150        abs: &mut A,
1151    ) -> EquivStatus {
1152        let mut sim = Sim::new(hir);
1153        let mut cycles = 0usize;
1154        for inputs in uart_tx_dual_stimulus() {
1155            sim.set_inputs(inputs.clone());
1156            sim.settle();
1157            sim.tick();
1158            let abs_out = abs.cycle(&inputs);
1159            if let Err(mismatches) = compare_named_ports(sim.ports(), &abs_out, UART_TX_ARCH_PORTS)
1160            {
1161                return EquivStatus::Fail {
1162                    cycle: cycles,
1163                    mismatches,
1164                };
1165            }
1166            cycles += 1;
1167        }
1168        EquivStatus::Pass { cycles }
1169    }
1170
1171    /// FR163: handwritten `UartRx` FL ≡ tick on [`uart_rx_dual_stimulus`].
1172    pub fn verify_uart_rx_handwritten(&self, hir: FrozenHir) -> EquivStatus {
1173        let mut sim = Sim::new(hir);
1174        let mut fl = UartRxFunctional::new();
1175        let mut cycles = 0usize;
1176        for inputs in uart_rx_dual_stimulus() {
1177            sim.set_inputs(inputs.clone());
1178            sim.settle();
1179            sim.tick();
1180            let abs_out = fl.cycle(&inputs);
1181            if let Err(mismatches) = compare_named_ports(sim.ports(), &abs_out, UART_RX_ARCH_PORTS)
1182            {
1183                return EquivStatus::Fail {
1184                    cycle: cycles,
1185                    mismatches,
1186                };
1187            }
1188            cycles += 1;
1189        }
1190        EquivStatus::Pass { cycles }
1191    }
1192
1193    /// Deliberate mismatch / alternate FL ATDD for UartRx (FR163).
1194    pub fn verify_uart_rx_handwritten_with<A: AbstractionView>(
1195        &self,
1196        hir: FrozenHir,
1197        abs: &mut A,
1198    ) -> EquivStatus {
1199        let mut sim = Sim::new(hir);
1200        let mut cycles = 0usize;
1201        for inputs in uart_rx_dual_stimulus() {
1202            sim.set_inputs(inputs.clone());
1203            sim.settle();
1204            sim.tick();
1205            let abs_out = abs.cycle(&inputs);
1206            if let Err(mismatches) = compare_named_ports(sim.ports(), &abs_out, UART_RX_ARCH_PORTS)
1207            {
1208                return EquivStatus::Fail {
1209                    cycle: cycles,
1210                    mismatches,
1211                };
1212            }
1213            cycles += 1;
1214        }
1215        EquivStatus::Pass { cycles }
1216    }
1217
1218    /// FR168: handwritten `SpiMaster` FL ≡ tick on [`spi_master_dual_stimulus`].
1219    pub fn verify_spi_master_handwritten(&self, hir: FrozenHir) -> EquivStatus {
1220        let mut sim = Sim::new(hir);
1221        let mut fl = SpiMasterFunctional::new();
1222        let mut cycles = 0usize;
1223        for inputs in spi_master_dual_stimulus() {
1224            sim.set_inputs(inputs.clone());
1225            sim.settle();
1226            sim.tick();
1227            let abs_out = fl.cycle(&inputs);
1228            if let Err(mismatches) =
1229                compare_named_ports(sim.ports(), &abs_out, SPI_MASTER_ARCH_PORTS)
1230            {
1231                return EquivStatus::Fail {
1232                    cycle: cycles,
1233                    mismatches,
1234                };
1235            }
1236            cycles += 1;
1237        }
1238        EquivStatus::Pass { cycles }
1239    }
1240
1241    /// Deliberate mismatch / alternate FL ATDD for SpiMaster (FR168).
1242    pub fn verify_spi_master_handwritten_with<A: AbstractionView>(
1243        &self,
1244        hir: FrozenHir,
1245        abs: &mut A,
1246    ) -> EquivStatus {
1247        let mut sim = Sim::new(hir);
1248        let mut cycles = 0usize;
1249        for inputs in spi_master_dual_stimulus() {
1250            sim.set_inputs(inputs.clone());
1251            sim.settle();
1252            sim.tick();
1253            let abs_out = abs.cycle(&inputs);
1254            if let Err(mismatches) =
1255                compare_named_ports(sim.ports(), &abs_out, SPI_MASTER_ARCH_PORTS)
1256            {
1257                return EquivStatus::Fail {
1258                    cycle: cycles,
1259                    mismatches,
1260                };
1261            }
1262            cycles += 1;
1263        }
1264        EquivStatus::Pass { cycles }
1265    }
1266
1267    /// FR168: handwritten `I2cMaster` FL ≡ tick on [`i2c_master_dual_stimulus`].
1268    pub fn verify_i2c_master_handwritten(&self, hir: FrozenHir) -> EquivStatus {
1269        let mut sim = Sim::new(hir);
1270        let mut fl = I2cMasterFunctional::new();
1271        let mut cycles = 0usize;
1272        for inputs in i2c_master_dual_stimulus() {
1273            sim.set_inputs(inputs.clone());
1274            sim.settle();
1275            sim.tick();
1276            let abs_out = fl.cycle(&inputs);
1277            if let Err(mismatches) =
1278                compare_named_ports(sim.ports(), &abs_out, I2C_MASTER_ARCH_PORTS)
1279            {
1280                return EquivStatus::Fail {
1281                    cycle: cycles,
1282                    mismatches,
1283                };
1284            }
1285            cycles += 1;
1286        }
1287        EquivStatus::Pass { cycles }
1288    }
1289
1290    /// Deliberate mismatch / alternate FL ATDD for I2cMaster (FR168).
1291    pub fn verify_i2c_master_handwritten_with<A: AbstractionView>(
1292        &self,
1293        hir: FrozenHir,
1294        abs: &mut A,
1295    ) -> EquivStatus {
1296        let mut sim = Sim::new(hir);
1297        let mut cycles = 0usize;
1298        for inputs in i2c_master_dual_stimulus() {
1299            sim.set_inputs(inputs.clone());
1300            sim.settle();
1301            sim.tick();
1302            let abs_out = abs.cycle(&inputs);
1303            if let Err(mismatches) =
1304                compare_named_ports(sim.ports(), &abs_out, I2C_MASTER_ARCH_PORTS)
1305            {
1306                return EquivStatus::Fail {
1307                    cycle: cycles,
1308                    mismatches,
1309                };
1310            }
1311            cycles += 1;
1312        }
1313        EquivStatus::Pass { cycles }
1314    }
1315
1316    /// FR168: handwritten `Axi4LiteSlave` FL ≡ tick on [`axi4_lite_slave_dual_stimulus`].
1317    pub fn verify_axi4_lite_slave_handwritten(&self, hir: FrozenHir) -> EquivStatus {
1318        let mut sim = Sim::new(hir);
1319        let mut fl = Axi4LiteSlaveFunctional::new();
1320        let mut cycles = 0usize;
1321        for inputs in axi4_lite_slave_dual_stimulus() {
1322            sim.set_inputs(inputs.clone());
1323            sim.settle();
1324            sim.tick();
1325            let abs_out = fl.cycle(&inputs);
1326            if let Err(mismatches) =
1327                compare_named_ports(sim.ports(), &abs_out, AXI4_LITE_SLAVE_ARCH_PORTS)
1328            {
1329                return EquivStatus::Fail {
1330                    cycle: cycles,
1331                    mismatches,
1332                };
1333            }
1334            cycles += 1;
1335        }
1336        EquivStatus::Pass { cycles }
1337    }
1338
1339    /// Deliberate mismatch / alternate FL ATDD for Axi4LiteSlave (FR168).
1340    pub fn verify_axi4_lite_slave_handwritten_with<A: AbstractionView>(
1341        &self,
1342        hir: FrozenHir,
1343        abs: &mut A,
1344    ) -> EquivStatus {
1345        let mut sim = Sim::new(hir);
1346        let mut cycles = 0usize;
1347        for inputs in axi4_lite_slave_dual_stimulus() {
1348            sim.set_inputs(inputs.clone());
1349            sim.settle();
1350            sim.tick();
1351            let abs_out = abs.cycle(&inputs);
1352            if let Err(mismatches) =
1353                compare_named_ports(sim.ports(), &abs_out, AXI4_LITE_SLAVE_ARCH_PORTS)
1354            {
1355                return EquivStatus::Fail {
1356                    cycle: cycles,
1357                    mismatches,
1358                };
1359            }
1360            cycles += 1;
1361        }
1362        EquivStatus::Pass { cycles }
1363    }
1364
1365    /// UART/SPI/I2C/AXI: generated FL ≡ tick via FormalEquivProduct (rst alphabet).
1366    pub fn verify_generated_rst_compare(&self, hir: FrozenHir) -> EquivStatus {
1367        FormalEquivProduct::new(0xC0FFEE, 8)
1368            .with_boolean_ports(&["rst"])
1369            .check_random_compare(hir)
1370    }
1371
1372    /// Convenience: handwritten equiv path (for fixtures that supply their own FL).
1373    pub fn verify_handwritten<A: AbstractionView>(
1374        &self,
1375        hir: FrozenHir,
1376        abs: &mut A,
1377        stimuli: impl IntoIterator<Item = PortValues>,
1378    ) -> EquivStatus {
1379        check_functional_equiv(hir, abs, stimuli)
1380    }
1381}
1382
1383fn compare_named_ports(
1384    left: &PortValues,
1385    right: &PortValues,
1386    names: &[&str],
1387) -> Result<(), Vec<PortMismatch>> {
1388    let mut l = PortValues::default();
1389    let mut r = PortValues::default();
1390    for name in names {
1391        if let Some(v) = left.get(name) {
1392            l.set(*name, v);
1393        }
1394        if let Some(v) = right.get(name) {
1395            r.set(*name, v);
1396        }
1397    }
1398    compare_port_values(&l, &r)
1399}
bitloom_sim/ip_dual.rs

bitloom_sim/
ip_dual.rs
