logicaffeine_compile/extraction/
verilog.rs

1//! Verilog Extraction: Kernel Term → SystemVerilog
2//!
3//! Converts kernel proof terms (which ARE circuits under Curry-Howard)
4//! into synthesizable SystemVerilog source code.
5//!
6//! # Extraction Rules
7//!
8//! | Kernel Term | SystemVerilog Output |
9//! |---|---|
10//! | `Global("bit_and")` applied to a, b | `a & b` |
11//! | `Global("bit_or")` applied to a, b | `a \| b` |
12//! | `Global("bit_not")` applied to a | `~a` |
13//! | `Global("bit_xor")` applied to a, b | `a ^ b` |
14//! | `Global("bit_mux")` applied to s, a, b | `s ? a : b` |
15//! | `Global("B0")` | `1'b0` |
16//! | `Global("B1")` | `1'b1` |
17//! | `Var(name)` | `name` |
18
19use logicaffeine_kernel::Term;
20
21/// Convert a kernel Term to a SystemVerilog expression string.
22///
23/// This handles the hardware-specific subset of kernel Terms:
24/// gate operations, constants, variables, and their compositions.
25pub fn term_to_verilog(term: &Term) -> String {
26    // Collect the application chain: flatten App(App(App(f, a), b), c) → (f, [a, b, c])
27    let (head, args) = collect_app_chain(term);
28
29    if let Term::Global(name) = &head {
30        match (name.as_str(), args.len()) {
31            // Constants
32            ("B0", 0) => return "1'b0".to_string(),
33            ("B1", 0) => return "1'b1".to_string(),
34            ("Tt", 0) => return "/* unit */".to_string(),
35
36            // Unary operations
37            ("bit_not", 1) => {
38                let a = term_to_verilog(&args[0]);
39                return format!("(~{})", a);
40            }
41
42            // Binary operations
43            ("bit_and", 2) => {
44                let a = term_to_verilog(&args[0]);
45                let b = term_to_verilog(&args[1]);
46                return format!("({} & {})", a, b);
47            }
48            ("bit_or", 2) => {
49                let a = term_to_verilog(&args[0]);
50                let b = term_to_verilog(&args[1]);
51                return format!("({} | {})", a, b);
52            }
53            ("bit_xor", 2) => {
54                let a = term_to_verilog(&args[0]);
55                let b = term_to_verilog(&args[1]);
56                return format!("({} ^ {})", a, b);
57            }
58
59            // Ternary: bit_mux sel then_v else_v → sel ? then_v : else_v
60            ("bit_mux", 3) => {
61                let sel = term_to_verilog(&args[0]);
62                let then_v = term_to_verilog(&args[1]);
63                let else_v = term_to_verilog(&args[2]);
64                return format!("({} ? {} : {})", sel, then_v, else_v);
65            }
66
67            // BVec operations
68            ("bv_and", 3) => {
69                // bv_and n v1 v2 — skip the Nat width argument
70                let a = term_to_verilog(&args[1]);
71                let b = term_to_verilog(&args[2]);
72                return format!("({} & {})", a, b);
73            }
74            ("bv_or", 3) => {
75                let a = term_to_verilog(&args[1]);
76                let b = term_to_verilog(&args[2]);
77                return format!("({} | {})", a, b);
78            }
79            ("bv_xor", 3) => {
80                let a = term_to_verilog(&args[1]);
81                let b = term_to_verilog(&args[2]);
82                return format!("({} ^ {})", a, b);
83            }
84            ("bv_not", 2) => {
85                let a = term_to_verilog(&args[1]);
86                return format!("(~{})", a);
87            }
88
89            // Partial application or unknown global — emit as function call
90            (fname, _) if !args.is_empty() => {
91                let arg_strs: Vec<String> = args.iter().map(|a| term_to_verilog(a)).collect();
92                return format!("{}({})", fname, arg_strs.join(", "));
93            }
94
95            // Bare global (no args) — emit as identifier
96            (gname, 0) => return gname.to_string(),
97
98            _ => {}
99        }
100    }
101
102    // Variable reference
103    if let Term::Var(name) = term {
104        return name.clone();
105    }
106
107    // Lambda — emit as comment (lambdas become module ports at higher level)
108    if let Term::Lambda { param, body, .. } = term {
109        let body_sv = term_to_verilog(body);
110        return format!("/* λ{} */ {}", param, body_sv);
111    }
112
113    // Match on Bit — ternary operator
114    if let Term::Match { discriminant, cases, .. } = term {
115        if cases.len() == 2 {
116            let disc = term_to_verilog(discriminant);
117            let case_b0 = term_to_verilog(&cases[0]);
118            let case_b1 = term_to_verilog(&cases[1]);
119            return format!("({} ? {} : {})", disc, case_b1, case_b0);
120        }
121    }
122
123    // Literal
124    if let Term::Lit(lit) = term {
125        return format!("{}", lit);
126    }
127
128    // Fallback
129    format!("/* unsupported: {} */", term)
130}
131
132/// Flatten a left-associative application chain.
133/// App(App(App(f, a), b), c) → (f, [a, b, c])
134fn collect_app_chain(term: &Term) -> (Term, Vec<Term>) {
135    let mut args = Vec::new();
136    let mut current = term.clone();
137
138    while let Term::App(func, arg) = current {
139        args.push(*arg);
140        current = *func;
141    }
142
143    args.reverse();
144    (current, args)
145}
logicaffeine_compile/extraction/verilog.rs

logicaffeine_compile/extraction/
verilog.rs
