logicaffeine_compile/codegen_sva/
traffic_flow.rs

1//! Traffic FLOW / capacity analysis as model checking.
2//!
3//! An approach's queue is a bit-vector counter; "can it JAM (overflow capacity)?" is a
4//! **reachability** question — exactly what our BMC engine answers, no new mathematics. Each
5//! model is synthesizable Verilog, so it rides the existing RTL path
6//! (`parse_transition_system` → `bmc` / `prove_invariant`) and the queue level renders straight
7//! into the waveform.
8//!
9//! * An approach whose **service keeps up with demand** only ever drains → `prove_invariant`
10//!   certifies it never jams (for all time).
11//! * An approach that is **under-served** (green only part of the cycle while demand keeps
12//!   arriving) grows without bound until it jams → `bmc` finds the exact cycle (the jam trace).
13//!
14//! `capacity` here is the queue width's range; the `jam` threshold is the level we forbid.
15
16/// A queue served only every other cycle while one vehicle arrives each cycle: net inflow is
17/// positive, so the queue climbs to `jam`. BMC finds the cycle it overflows.
18pub fn congested_approach(width: u32, jam: u64) -> String {
19    let hi = width - 1;
20    format!(
21        "module flow(input clk);\n\
22         \u{20}\u{20}reg [{hi}:0] q;\n\
23         \u{20}\u{20}reg phase;\n\
24         \u{20}\u{20}initial begin q = {width}'d0; phase = 1'd0; end\n\
25         \u{20}\u{20}always @(posedge clk) begin\n\
26         \u{20}\u{20}\u{20}\u{20}phase <= ~phase;\n\
27         \u{20}\u{20}\u{20}\u{20}if (phase == 1'd1) q <= q + {width}'d1;\n\
28         \u{20}\u{20}end\n\
29         \u{20}\u{20}assert property (q < {width}'d{jam});\n\
30         endmodule\n"
31    )
32}
33
34/// A queue with a starting backlog and service that exceeds arrivals: it only ever drains, so it
35/// provably never reaches `jam` — for all reachable states (k-induction).
36pub fn balanced_approach(width: u32, jam: u64, backlog: u64) -> String {
37    let hi = width - 1;
38    format!(
39        "module flow(input clk);\n\
40         \u{20}\u{20}reg [{hi}:0] q;\n\
41         \u{20}\u{20}initial begin q = {width}'d{backlog}; end\n\
42         \u{20}\u{20}always @(posedge clk)\n\
43         \u{20}\u{20}\u{20}\u{20}if (q != {width}'d0) q <= q - {width}'d1;\n\
44         \u{20}\u{20}assert property (q < {width}'d{jam});\n\
45         endmodule\n"
46    )
47}
48
49#[cfg(test)]
50mod tests {
51    use super::*;
52    use crate::codegen_sva::rtl::parse_transition_system;
53    use logicaffeine_proof::bmc::{BmcOutcome, InductionOutcome};
54
55    #[test]
56    fn congested_approach_jams_and_bmc_finds_the_cycle() {
57        let ts = parse_transition_system(&congested_approach(3, 7))
58            .unwrap_or_else(|e| panic!("congested model did not parse: {}", e.message));
59        match ts.bmc(24) {
60            BmcOutcome::CounterexampleAt { .. } => {}
61            other => panic!("an under-served approach must jam, got {other:?}"),
62        }
63    }
64
65    #[test]
66    fn balanced_approach_provably_never_jams() {
67        let ts = parse_transition_system(&balanced_approach(3, 7, 5))
68            .unwrap_or_else(|e| panic!("balanced model did not parse: {}", e.message));
69        assert_eq!(
70            ts.prove_invariant(1),
71            InductionOutcome::Proven,
72            "a draining queue must be PROVEN jam-free"
73        );
74    }
75
76    #[test]
77    fn a_well_sized_queue_does_not_overflow_within_the_horizon() {
78        // The same congestion against a larger capacity survives longer before jamming — the
79        // sizing lever. Within a short horizon it stays clean.
80        let ts = parse_transition_system(&congested_approach(4, 15)).unwrap();
81        assert_eq!(
82            ts.bmc(8),
83            BmcOutcome::NoneWithin(8),
84            "a 4-bit queue should not jam within 8 cycles"
85        );
86    }
87
88    #[test]
89    fn jam_is_pushed_later_by_more_capacity() {
90        // Wider queue (bigger jam threshold) jams strictly later than a narrow one.
91        let narrow = parse_transition_system(&congested_approach(3, 7)).unwrap();
92        let wide = parse_transition_system(&congested_approach(4, 15)).unwrap();
93        let cycle = |o: BmcOutcome| match o {
94            BmcOutcome::CounterexampleAt { k, .. } => k,
95            _ => u32::MAX,
96        };
97        let narrow_k = cycle(narrow.bmc(40));
98        let wide_k = cycle(wide.bmc(40));
99        assert!(
100            narrow_k < wide_k,
101            "more capacity must delay the jam: narrow@{narrow_k} vs wide@{wide_k}"
102        );
103    }
104}
logicaffeine_compile/codegen_sva/traffic_flow.rs

logicaffeine_compile/codegen_sva/
traffic_flow.rs
