Expand description
Verilog Extraction: Kernel Term → SystemVerilog
Converts kernel proof terms (which ARE circuits under Curry-Howard) into synthesizable SystemVerilog source code.
§Extraction Rules
| Kernel Term | SystemVerilog Output |
|---|---|
Global("bit_and") applied to a, b | a & b |
Global("bit_or") applied to a, b | a | b |
Global("bit_not") applied to a | ~a |
Global("bit_xor") applied to a, b | a ^ b |
Global("bit_mux") applied to s, a, b | s ? a : b |
Global("B0") | 1'b0 |
Global("B1") | 1'b1 |
Var(name) | name |
Functions§
- term_
to_ verilog - Convert a kernel Term to a SystemVerilog expression string.