dunkirk.sh
optimizing a gate level bcm to the end of the earth and back
Fix truth tables and add exact synthesis exports
- Fix segment c truth table (was wrong for digits 2, 3)
- Fix segment f truth table (was wrong for digit 7)
- Fix gate function encoding (bit ordering was inverted)
- Add Verilog, C, and DOT export functions for exact synthesis
- Update CLI to use appropriate export based on result type
- Add exported 12-gate circuit files (verified correct for 0-9)
The corrected truth tables require 12 gates minimum (24 inputs)
compared to 11 gates with the buggy tables.
Co-Authored-By: Claude Opus 4.5 <noreply@anthropic.com>
+32
bcd_7seg.c
+32
bcd_7seg.c
···
···
1
+
/*
2
+
* BCD to 7-segment decoder (exact synthesis)
3
+
* 12 gates, 24 total gate inputs
4
+
* Method: exact_12gates
5
+
*/
6
+
7
+
#include <stdint.h>
8
+
9
+
uint8_t bcd_to_7seg(uint8_t bcd) {
10
+
// Extract individual bits
11
+
uint8_t A = (bcd >> 3) & 1;
12
+
uint8_t B = (bcd >> 2) & 1;
13
+
uint8_t C = (bcd >> 1) & 1;
14
+
uint8_t D = bcd & 1;
15
+
16
+
// Gate outputs
17
+
uint8_t g0 = (A | !D);
18
+
uint8_t g1 = (B ^ C);
19
+
uint8_t g2 = (C | !g0);
20
+
uint8_t g3 = (g0 ^ g1);
21
+
uint8_t g4 = !(A | g1);
22
+
uint8_t g5 = !(B & g3);
23
+
uint8_t g6 = (C | g3);
24
+
uint8_t g7 = (!D & g6);
25
+
uint8_t g8 = !(g4 & g5);
26
+
uint8_t g9 = (g3 | g7);
27
+
uint8_t g10 = !(g2 & g5);
28
+
uint8_t g11 = (g3 | !g9);
29
+
30
+
// Pack segment outputs (bit 6 = a, bit 0 = g)
31
+
return (g6 << 6) | (g5 << 5) | (g11 << 4) | (g9 << 3) | (g7 << 2) | (g10 << 1) | (g8 << 0);
32
+
}
+88
bcd_7seg.dot
+88
bcd_7seg.dot
···
···
1
+
digraph BCD_7Seg {
2
+
label="BCD to 7-Segment Decoder\n12 gates, 24 gate inputs";
3
+
labelloc="t";
4
+
fontsize=16;
5
+
rankdir=LR;
6
+
splines=ortho;
7
+
nodesep=0.5;
8
+
ranksep=1.0;
9
+
10
+
// Inputs
11
+
subgraph cluster_inputs {
12
+
label="Inputs";
13
+
style=dashed;
14
+
color=gray;
15
+
A [shape=circle, style=filled, fillcolor=lightblue, label="A"];
16
+
B [shape=circle, style=filled, fillcolor=lightblue, label="B"];
17
+
C [shape=circle, style=filled, fillcolor=lightblue, label="C"];
18
+
D [shape=circle, style=filled, fillcolor=lightblue, label="D"];
19
+
}
20
+
21
+
// Gates
22
+
subgraph cluster_gates {
23
+
label="Logic Gates";
24
+
style=dashed;
25
+
color=gray;
26
+
g0 [shape=box, style=filled, fillcolor=lightgray, label="A+!B"];
27
+
g1 [shape=box, style=filled, fillcolor=lightyellow, label="XOR"];
28
+
g2 [shape=box, style=filled, fillcolor=lightgray, label="A+!B"];
29
+
g3 [shape=box, style=filled, fillcolor=lightyellow, label="XOR"];
30
+
g4 [shape=box, style=filled, fillcolor=peachpuff, label="NOR"];
31
+
g5 [shape=box, style=filled, fillcolor=palegreen, label="NAND"];
32
+
g6 [shape=box, style=filled, fillcolor=lightsalmon, label="OR"];
33
+
g7 [shape=box, style=filled, fillcolor=lightgray, label="B>A"];
34
+
g8 [shape=box, style=filled, fillcolor=palegreen, label="NAND"];
35
+
g9 [shape=box, style=filled, fillcolor=lightsalmon, label="OR"];
36
+
g10 [shape=box, style=filled, fillcolor=palegreen, label="NAND"];
37
+
g11 [shape=box, style=filled, fillcolor=lightgray, label="A+!B"];
38
+
}
39
+
40
+
// Gate input connections
41
+
A -> g0;
42
+
D -> g0;
43
+
B -> g1;
44
+
C -> g1;
45
+
C -> g2;
46
+
g0 -> g2;
47
+
g0 -> g3;
48
+
g1 -> g3;
49
+
A -> g4;
50
+
g1 -> g4;
51
+
B -> g5;
52
+
g3 -> g5;
53
+
C -> g6;
54
+
g3 -> g6;
55
+
D -> g7;
56
+
g6 -> g7;
57
+
g4 -> g8;
58
+
g5 -> g8;
59
+
g3 -> g9;
60
+
g7 -> g9;
61
+
g2 -> g10;
62
+
g5 -> g10;
63
+
g3 -> g11;
64
+
g9 -> g11;
65
+
66
+
// Outputs
67
+
subgraph cluster_outputs {
68
+
label="Segment Outputs";
69
+
style=dashed;
70
+
color=gray;
71
+
out_a [shape=doublecircle, style=filled, fillcolor=lightpink, label="a"];
72
+
out_b [shape=doublecircle, style=filled, fillcolor=lightpink, label="b"];
73
+
out_c [shape=doublecircle, style=filled, fillcolor=lightpink, label="c"];
74
+
out_d [shape=doublecircle, style=filled, fillcolor=lightpink, label="d"];
75
+
out_e [shape=doublecircle, style=filled, fillcolor=lightpink, label="e"];
76
+
out_f [shape=doublecircle, style=filled, fillcolor=lightpink, label="f"];
77
+
out_g [shape=doublecircle, style=filled, fillcolor=lightpink, label="g"];
78
+
}
79
+
80
+
// Output connections
81
+
g6 -> out_a;
82
+
g5 -> out_b;
83
+
g11 -> out_c;
84
+
g9 -> out_d;
85
+
g7 -> out_e;
86
+
g10 -> out_f;
87
+
g8 -> out_g;
88
+
}
bcd_7seg.png
bcd_7seg.png
This is a binary file and will not be displayed.
+39
bcd_7seg.v
+39
bcd_7seg.v
···
···
1
+
// BCD to 7-segment decoder (exact synthesis)
2
+
// 12 gates, 24 total gate inputs
3
+
// Method: exact_12gates
4
+
5
+
module bcd_to_7seg (
6
+
input wire [3:0] bcd, // BCD input (0-9 valid)
7
+
output wire [6:0] seg // 7-segment output (a=seg[6], g=seg[0])
8
+
);
9
+
10
+
// Input aliases
11
+
wire A = bcd[3];
12
+
wire B = bcd[2];
13
+
wire C = bcd[1];
14
+
wire D = bcd[0];
15
+
16
+
// Internal gate outputs
17
+
wire g0 = (A | ~D);
18
+
wire g1 = (B ^ C);
19
+
wire g2 = (C | ~g0);
20
+
wire g3 = (g0 ^ g1);
21
+
wire g4 = ~(A | g1);
22
+
wire g5 = ~(B & g3);
23
+
wire g6 = (C | g3);
24
+
wire g7 = (~D & g6);
25
+
wire g8 = ~(g4 & g5);
26
+
wire g9 = (g3 | g7);
27
+
wire g10 = ~(g2 & g5);
28
+
wire g11 = (g3 | ~g9);
29
+
30
+
// Segment output assignments
31
+
assign seg[6] = g6; // a
32
+
assign seg[5] = g5; // b
33
+
assign seg[4] = g11; // c
34
+
assign seg[3] = g9; // d
35
+
assign seg[2] = g7; // e
36
+
assign seg[1] = g10; // f
37
+
assign seg[0] = g8; // g
38
+
39
+
endmodule
+10
-5
bcd_optimization/cli.py
+10
-5
bcd_optimization/cli.py
···
5
6
from .solver import BCDTo7SegmentSolver
7
from .truth_tables import print_truth_table
8
-
from .export import to_verilog, to_c_code, to_equations, to_dot
9
10
11
def main():
···
81
if quiet:
82
sys.stdout = old_stdout
83
84
-
# Output in requested format
85
if args.format == "verilog":
86
-
print(to_verilog(result))
87
elif args.format == "c":
88
-
print(to_c_code(result))
89
elif args.format == "equations":
90
print(to_equations(result))
91
elif args.format == "dot":
92
-
print(to_dot(result))
93
else:
94
print()
95
solver.print_result(result)
···
5
6
from .solver import BCDTo7SegmentSolver
7
from .truth_tables import print_truth_table
8
+
from .export import (
9
+
to_verilog, to_c_code, to_equations, to_dot,
10
+
to_verilog_exact, to_c_exact, to_dot_exact,
11
+
)
12
13
14
def main():
···
84
if quiet:
85
sys.stdout = old_stdout
86
87
+
# Output in requested format (use exact synthesis exports if available)
88
+
is_exact = result.gates is not None and len(result.gates) > 0
89
+
90
if args.format == "verilog":
91
+
print(to_verilog_exact(result) if is_exact else to_verilog(result))
92
elif args.format == "c":
93
+
print(to_c_exact(result) if is_exact else to_c_code(result))
94
elif args.format == "equations":
95
print(to_equations(result))
96
elif args.format == "dot":
97
+
print(to_dot_exact(result) if is_exact else to_dot(result))
98
else:
99
print()
100
solver.print_result(result)
+261
bcd_optimization/export.py
+261
bcd_optimization/export.py
···
402
return "\n".join(lines)
403
404
405
+
def to_verilog_exact(result: SynthesisResult, module_name: str = "bcd_to_7seg") -> str:
406
+
"""
407
+
Export exact synthesis result to Verilog.
408
+
409
+
Args:
410
+
result: The synthesis result with gates list populated
411
+
module_name: Name for the Verilog module
412
+
413
+
Returns:
414
+
Verilog source code as string
415
+
"""
416
+
if not result.gates:
417
+
raise ValueError("No gates in result - use to_verilog for SOP results")
418
+
419
+
lines = []
420
+
lines.append(f"// BCD to 7-segment decoder (exact synthesis)")
421
+
lines.append(f"// {len(result.gates)} gates, {result.cost} total gate inputs")
422
+
lines.append(f"// Method: {result.method}")
423
+
lines.append("")
424
+
lines.append(f"module {module_name} (")
425
+
lines.append(" input wire [3:0] bcd, // BCD input (0-9 valid)")
426
+
lines.append(" output wire [6:0] seg // 7-segment output (a=seg[6], g=seg[0])")
427
+
lines.append(");")
428
+
lines.append("")
429
+
lines.append(" // Input aliases")
430
+
lines.append(" wire A = bcd[3];")
431
+
lines.append(" wire B = bcd[2];")
432
+
lines.append(" wire C = bcd[1];")
433
+
lines.append(" wire D = bcd[0];")
434
+
lines.append("")
435
+
436
+
n_inputs = 4
437
+
node_names = ['A', 'B', 'C', 'D']
438
+
439
+
# Generate gate wires
440
+
lines.append(" // Internal gate outputs")
441
+
for gate in result.gates:
442
+
node_names.append(f"g{gate.index}")
443
+
in1 = node_names[gate.input1]
444
+
in2 = node_names[gate.input2]
445
+
expr = _gate_to_verilog_expr(gate.func, in1, in2)
446
+
lines.append(f" wire g{gate.index} = {expr};")
447
+
448
+
lines.append("")
449
+
lines.append(" // Segment output assignments")
450
+
451
+
for i, segment in enumerate(SEGMENT_NAMES):
452
+
if segment in result.output_map:
453
+
node_idx = result.output_map[segment]
454
+
src = node_names[node_idx]
455
+
seg_idx = 6 - i # a=seg[6], b=seg[5], ..., g=seg[0]
456
+
lines.append(f" assign seg[{seg_idx}] = {src}; // {segment}")
457
+
458
+
lines.append("")
459
+
lines.append("endmodule")
460
+
461
+
return "\n".join(lines)
462
+
463
+
464
+
def _gate_to_verilog_expr(func: int, in1: str, in2: str) -> str:
465
+
"""Convert gate function code to Verilog expression."""
466
+
# func encodes 2-input truth table: bit i = f(p,q) where i = p*2 + q
467
+
# Bit 0: f(0,0), Bit 1: f(0,1), Bit 2: f(1,0), Bit 3: f(1,1)
468
+
expressions = {
469
+
0b0000: "1'b0", # constant 0
470
+
0b0001: f"~({in1} | {in2})", # NOR
471
+
0b0010: f"(~{in1} & {in2})", # B AND NOT A
472
+
0b0011: f"~{in1}", # NOT A
473
+
0b0100: f"({in1} & ~{in2})", # A AND NOT B
474
+
0b0101: f"~{in2}", # NOT B
475
+
0b0110: f"({in1} ^ {in2})", # XOR
476
+
0b0111: f"~({in1} & {in2})", # NAND
477
+
0b1000: f"({in1} & {in2})", # AND
478
+
0b1001: f"~({in1} ^ {in2})", # XNOR
479
+
0b1010: in2, # B (pass through)
480
+
0b1011: f"(~{in1} | {in2})", # NOT A OR B
481
+
0b1100: in1, # A (pass through)
482
+
0b1101: f"({in1} | ~{in2})", # A OR NOT B
483
+
0b1110: f"({in1} | {in2})", # OR
484
+
0b1111: "1'b1", # constant 1
485
+
}
486
+
return expressions.get(func, f"/* unknown func {func} */")
487
+
488
+
489
+
def to_dot_exact(result: SynthesisResult, title: str = "BCD to 7-Segment Decoder") -> str:
490
+
"""
491
+
Export exact synthesis result as Graphviz DOT format.
492
+
493
+
Args:
494
+
result: The synthesis result with gates list populated
495
+
title: Title for the diagram
496
+
497
+
Returns:
498
+
DOT source code as string
499
+
"""
500
+
if not result.gates:
501
+
raise ValueError("No gates in result - use to_dot for SOP results")
502
+
503
+
lines = []
504
+
lines.append("digraph BCD_7Seg {")
505
+
lines.append(f' label="{title}\\n{len(result.gates)} gates, {result.cost} gate inputs";')
506
+
lines.append(' labelloc="t";')
507
+
lines.append(' fontsize=16;')
508
+
lines.append(' rankdir=LR;')
509
+
lines.append(' splines=ortho;')
510
+
lines.append(' nodesep=0.5;')
511
+
lines.append(' ranksep=1.0;')
512
+
lines.append("")
513
+
514
+
n_inputs = 4
515
+
node_names = ['A', 'B', 'C', 'D']
516
+
517
+
# Input nodes
518
+
lines.append(' // Inputs')
519
+
lines.append(' subgraph cluster_inputs {')
520
+
lines.append(' label="Inputs";')
521
+
lines.append(' style=dashed;')
522
+
lines.append(' color=gray;')
523
+
for name in node_names:
524
+
lines.append(f' {name} [shape=circle, style=filled, fillcolor=lightblue, label="{name}"];')
525
+
lines.append(' }')
526
+
lines.append("")
527
+
528
+
# Gate nodes
529
+
lines.append(' // Gates')
530
+
lines.append(' subgraph cluster_gates {')
531
+
lines.append(' label="Logic Gates";')
532
+
lines.append(' style=dashed;')
533
+
lines.append(' color=gray;')
534
+
535
+
gate_colors = {
536
+
'AND': 'lightgreen',
537
+
'OR': 'lightsalmon',
538
+
'XOR': 'lightyellow',
539
+
'XNOR': 'lightyellow',
540
+
'NAND': 'palegreen',
541
+
'NOR': 'peachpuff',
542
+
}
543
+
544
+
for gate in result.gates:
545
+
node_names.append(f"g{gate.index}")
546
+
color = gate_colors.get(gate.func_name, 'lightgray')
547
+
lines.append(f' g{gate.index} [shape=box, style=filled, fillcolor={color}, label="{gate.func_name}"];')
548
+
lines.append(' }')
549
+
lines.append("")
550
+
551
+
# Gate connections
552
+
lines.append(' // Gate input connections')
553
+
node_names_lookup = ['A', 'B', 'C', 'D'] + [f"g{g.index}" for g in result.gates]
554
+
for gate in result.gates:
555
+
in1 = node_names_lookup[gate.input1]
556
+
in2 = node_names_lookup[gate.input2]
557
+
lines.append(f' {in1} -> g{gate.index};')
558
+
lines.append(f' {in2} -> g{gate.index};')
559
+
lines.append("")
560
+
561
+
# Output nodes
562
+
lines.append(' // Outputs')
563
+
lines.append(' subgraph cluster_outputs {')
564
+
lines.append(' label="Segment Outputs";')
565
+
lines.append(' style=dashed;')
566
+
lines.append(' color=gray;')
567
+
for segment in SEGMENT_NAMES:
568
+
lines.append(f' out_{segment} [shape=doublecircle, style=filled, fillcolor=lightpink, label="{segment}"];')
569
+
lines.append(' }')
570
+
lines.append("")
571
+
572
+
# Output connections
573
+
lines.append(' // Output connections')
574
+
for segment in SEGMENT_NAMES:
575
+
if segment in result.output_map:
576
+
node_idx = result.output_map[segment]
577
+
src = node_names_lookup[node_idx]
578
+
lines.append(f' {src} -> out_{segment};')
579
+
580
+
lines.append("}")
581
+
582
+
return "\n".join(lines)
583
+
584
+
585
+
def to_c_exact(result: SynthesisResult, func_name: str = "bcd_to_7seg") -> str:
586
+
"""
587
+
Export exact synthesis result as C code.
588
+
589
+
Args:
590
+
result: The synthesis result with gates list populated
591
+
func_name: Name for the C function
592
+
593
+
Returns:
594
+
C source code as string
595
+
"""
596
+
if not result.gates:
597
+
raise ValueError("No gates in result - use to_c_code for SOP results")
598
+
599
+
lines = []
600
+
lines.append("/*")
601
+
lines.append(" * BCD to 7-segment decoder (exact synthesis)")
602
+
lines.append(f" * {len(result.gates)} gates, {result.cost} total gate inputs")
603
+
lines.append(f" * Method: {result.method}")
604
+
lines.append(" */")
605
+
lines.append("")
606
+
lines.append("#include <stdint.h>")
607
+
lines.append("")
608
+
lines.append(f"uint8_t {func_name}(uint8_t bcd) {{")
609
+
lines.append(" // Extract individual bits")
610
+
lines.append(" uint8_t A = (bcd >> 3) & 1;")
611
+
lines.append(" uint8_t B = (bcd >> 2) & 1;")
612
+
lines.append(" uint8_t C = (bcd >> 1) & 1;")
613
+
lines.append(" uint8_t D = bcd & 1;")
614
+
lines.append("")
615
+
616
+
node_names = ['A', 'B', 'C', 'D']
617
+
618
+
lines.append(" // Gate outputs")
619
+
for gate in result.gates:
620
+
node_names.append(f"g{gate.index}")
621
+
in1 = node_names[gate.input1]
622
+
in2 = node_names[gate.input2]
623
+
expr = _gate_to_c_expr(gate.func, in1, in2)
624
+
lines.append(f" uint8_t g{gate.index} = {expr};")
625
+
626
+
lines.append("")
627
+
lines.append(" // Pack segment outputs (bit 6 = a, bit 0 = g)")
628
+
629
+
pack_parts = []
630
+
for i, segment in enumerate(SEGMENT_NAMES):
631
+
if segment in result.output_map:
632
+
node_idx = result.output_map[segment]
633
+
src = node_names[node_idx]
634
+
pack_parts.append(f"({src} << {6-i})")
635
+
636
+
lines.append(f" return {' | '.join(pack_parts)};")
637
+
lines.append("}")
638
+
639
+
return "\n".join(lines)
640
+
641
+
642
+
def _gate_to_c_expr(func: int, in1: str, in2: str) -> str:
643
+
"""Convert gate function code to C expression."""
644
+
# func encodes 2-input truth table: bit i = f(p,q) where i = p*2 + q
645
+
expressions = {
646
+
0b0000: "0", # constant 0
647
+
0b0001: f"!({in1} | {in2})", # NOR
648
+
0b0010: f"(!{in1} & {in2})", # B AND NOT A
649
+
0b0011: f"!{in1}", # NOT A
650
+
0b0100: f"({in1} & !{in2})", # A AND NOT B
651
+
0b0101: f"!{in2}", # NOT B
652
+
0b0110: f"({in1} ^ {in2})", # XOR
653
+
0b0111: f"!({in1} & {in2})", # NAND
654
+
0b1000: f"({in1} & {in2})", # AND
655
+
0b1001: f"!({in1} ^ {in2})", # XNOR
656
+
0b1010: in2, # B (pass through)
657
+
0b1011: f"(!{in1} | {in2})", # NOT A OR B
658
+
0b1100: in1, # A (pass through)
659
+
0b1101: f"({in1} | !{in2})", # A OR NOT B
660
+
0b1110: f"({in1} | {in2})", # OR
661
+
0b1111: "1", # constant 1
662
+
}
663
+
return expressions.get(func, f"/* unknown func {func} */")
664
+
665
+
666
if __name__ == "__main__":
667
from .solver import BCDTo7SegmentSolver
668
+56
-28
bcd_optimization/solver.py
+56
-28
bcd_optimization/solver.py
···
35
36
37
@dataclass
38
class SynthesisResult:
39
"""Result of logic synthesis optimization."""
40
···
44
method: str
45
expressions: dict[str, str] = field(default_factory=dict)
46
cost_breakdown: CostBreakdown = None
47
48
49
class BCDTo7SegmentSolver:
···
233
cost_breakdown=cost_breakdown,
234
)
235
236
-
def exact_synthesis(self, max_gates: int = 15) -> SynthesisResult:
237
"""
238
Phase 3: SAT-based exact synthesis for provably optimal circuits.
239
240
Encodes the circuit synthesis problem as SAT and iteratively searches
241
for the minimum number of gates.
242
"""
243
-
for num_gates in range(1, max_gates + 1):
244
-
print(f" Trying {num_gates} gates...")
245
result = self._try_exact_synthesis(num_gates)
246
if result is not None:
247
return result
···
364
return var in model
365
366
node_names = ['A', 'B', 'C', 'D'] + [f'g{i}' for i in range(num_gates)]
367
-
gate_exprs = {}
368
369
for i in range(n_inputs, n_nodes):
370
for j in range(i):
···
377
if is_true(f[i][p][q]):
378
func |= (1 << (p * 2 + q))
379
380
-
op = self._decode_gate_function(func)
381
-
gate_exprs[i] = f"({node_names[j]} {op} {node_names[k]})"
382
-
node_names[i] = gate_exprs[i]
383
break
384
385
expressions = {}
386
for h, segment in enumerate(SEGMENT_NAMES):
387
for i in range(n_nodes):
388
if is_true(g[h][i]):
389
expressions[segment] = node_names[i]
390
break
391
392
# For exact synthesis, all gates are 2-input gates
393
-
# This is a different circuit topology than SOP
394
cost_breakdown = CostBreakdown(
395
-
and_inputs=num_gates * 2, # All gates treated as "AND-like"
396
-
or_inputs=0, # No separate OR level in multi-level
397
num_and_gates=num_gates,
398
num_or_gates=0,
399
)
400
401
return SynthesisResult(
402
-
cost=num_gates * 2, # 2 inputs per 2-input gate
403
implicants_by_output={},
404
shared_implicants=[],
405
method=f"exact_{num_gates}gates",
406
expressions=expressions,
407
cost_breakdown=cost_breakdown,
408
)
409
410
def _decode_gate_function(self, func: int) -> str:
411
"""Decode 4-bit function to gate type name."""
412
-
# func[pq] gives output for inputs (p, q)
413
# Bit 0: f(0,0), Bit 1: f(0,1), Bit 2: f(1,0), Bit 3: f(1,1)
414
names = {
415
-
0b0000: "0",
416
-
0b0001: "AND",
417
-
0b0010: "A>B", # A AND NOT B
418
-
0b0011: "A",
419
-
0b0100: "B>A", # B AND NOT A
420
-
0b0101: "B",
421
-
0b0110: "XOR",
422
-
0b0111: "OR",
423
-
0b1000: "NOR",
424
-
0b1001: "XNOR",
425
-
0b1010: "!B",
426
-
0b1011: "A+!B", # A OR NOT B
427
-
0b1100: "!A",
428
-
0b1101: "!A+B", # NOT A OR B
429
-
0b1110: "NAND",
430
-
0b1111: "1",
431
}
432
return names.get(func, f"F{func:04b}")
433
···
35
36
37
@dataclass
38
+
class GateInfo:
39
+
"""Information about a gate in exact synthesis."""
40
+
index: int # Gate index (0-based, after inputs)
41
+
input1: int # First input node index
42
+
input2: int # Second input node index
43
+
func: int # 4-bit function code
44
+
func_name: str # Human-readable function name
45
+
46
+
47
+
@dataclass
48
class SynthesisResult:
49
"""Result of logic synthesis optimization."""
50
···
54
method: str
55
expressions: dict[str, str] = field(default_factory=dict)
56
cost_breakdown: CostBreakdown = None
57
+
# For exact synthesis: gate-level circuit description
58
+
gates: list[GateInfo] = None
59
+
output_map: dict[str, int] = None # segment -> node index
60
61
62
class BCDTo7SegmentSolver:
···
246
cost_breakdown=cost_breakdown,
247
)
248
249
+
def exact_synthesis(self, max_gates: int = 15, min_gates: int = 1) -> SynthesisResult:
250
"""
251
Phase 3: SAT-based exact synthesis for provably optimal circuits.
252
253
Encodes the circuit synthesis problem as SAT and iteratively searches
254
for the minimum number of gates.
255
"""
256
+
import sys
257
+
for num_gates in range(min_gates, max_gates + 1):
258
+
print(f" Trying {num_gates} gates...", flush=True)
259
+
sys.stdout.flush()
260
result = self._try_exact_synthesis(num_gates)
261
if result is not None:
262
return result
···
379
return var in model
380
381
node_names = ['A', 'B', 'C', 'D'] + [f'g{i}' for i in range(num_gates)]
382
+
gates = []
383
384
for i in range(n_inputs, n_nodes):
385
for j in range(i):
···
392
if is_true(f[i][p][q]):
393
func |= (1 << (p * 2 + q))
394
395
+
func_name = self._decode_gate_function(func)
396
+
gates.append(GateInfo(
397
+
index=i - n_inputs,
398
+
input1=j,
399
+
input2=k,
400
+
func=func,
401
+
func_name=func_name,
402
+
))
403
+
404
+
# Build expression string
405
+
expr = f"({node_names[j]} {func_name} {node_names[k]})"
406
+
node_names[i] = expr
407
break
408
409
+
# Map outputs to nodes
410
+
output_map = {}
411
expressions = {}
412
for h, segment in enumerate(SEGMENT_NAMES):
413
for i in range(n_nodes):
414
if is_true(g[h][i]):
415
+
output_map[segment] = i
416
expressions[segment] = node_names[i]
417
break
418
419
# For exact synthesis, all gates are 2-input gates
420
cost_breakdown = CostBreakdown(
421
+
and_inputs=num_gates * 2,
422
+
or_inputs=0,
423
num_and_gates=num_gates,
424
num_or_gates=0,
425
)
426
427
return SynthesisResult(
428
+
cost=num_gates * 2,
429
implicants_by_output={},
430
shared_implicants=[],
431
method=f"exact_{num_gates}gates",
432
expressions=expressions,
433
cost_breakdown=cost_breakdown,
434
+
gates=gates,
435
+
output_map=output_map,
436
)
437
438
def _decode_gate_function(self, func: int) -> str:
439
"""Decode 4-bit function to gate type name."""
440
+
# func encodes 2-input truth table: bit i = f(p,q) where i = p*2 + q
441
# Bit 0: f(0,0), Bit 1: f(0,1), Bit 2: f(1,0), Bit 3: f(1,1)
442
names = {
443
+
0b0000: "0", # constant 0
444
+
0b0001: "NOR", # 1 only when both inputs 0
445
+
0b0010: "B>A", # B AND NOT A (inhibit)
446
+
0b0011: "!A", # NOT first input
447
+
0b0100: "A>B", # A AND NOT B (inhibit)
448
+
0b0101: "!B", # NOT second input
449
+
0b0110: "XOR", # exclusive or
450
+
0b0111: "NAND", # NOT (A AND B)
451
+
0b1000: "AND", # A AND B
452
+
0b1001: "XNOR", # NOT (A XOR B)
453
+
0b1010: "B", # pass through second input
454
+
0b1011: "!A+B", # NOT A OR B (implication)
455
+
0b1100: "A", # pass through first input
456
+
0b1101: "A+!B", # A OR NOT B (implication)
457
+
0b1110: "OR", # A OR B
458
+
0b1111: "1", # constant 1
459
}
460
return names.get(func, f"F{func:04b}")
461
+4
-4
bcd_optimization/truth_tables.py
+4
-4
bcd_optimization/truth_tables.py
···
22
SEGMENT_TRUTH_TABLES = {
23
'a': "1011011111------", # ON for 0,2,3,5,6,7,8,9
24
'b': "1111100111------", # ON for 0,1,2,3,4,7,8,9
25
-
'c': "1110111111------", # ON for 0,1,2,4,5,6,7,8,9
26
'd': "1011011011------", # ON for 0,2,3,5,6,8,9
27
'e': "1010001010------", # ON for 0,2,6,8
28
-
'f': "1000111111------", # ON for 0,4,5,6,7,8,9
29
'g': "0011111011------", # ON for 2,3,4,5,6,8,9
30
}
31
···
35
SEGMENT_MINTERMS = {
36
'a': [0, 2, 3, 5, 6, 7, 8, 9],
37
'b': [0, 1, 2, 3, 4, 7, 8, 9],
38
-
'c': [0, 1, 2, 4, 5, 6, 7, 8, 9],
39
'd': [0, 2, 3, 5, 6, 8, 9],
40
'e': [0, 2, 6, 8],
41
-
'f': [0, 4, 5, 6, 7, 8, 9],
42
'g': [2, 3, 4, 5, 6, 8, 9],
43
}
44
···
22
SEGMENT_TRUTH_TABLES = {
23
'a': "1011011111------", # ON for 0,2,3,5,6,7,8,9
24
'b': "1111100111------", # ON for 0,1,2,3,4,7,8,9
25
+
'c': "1101111111------", # ON for 0,1,3,4,5,6,7,8,9
26
'd': "1011011011------", # ON for 0,2,3,5,6,8,9
27
'e': "1010001010------", # ON for 0,2,6,8
28
+
'f': "1000110111------", # ON for 0,4,5,6,8,9
29
'g': "0011111011------", # ON for 2,3,4,5,6,8,9
30
}
31
···
35
SEGMENT_MINTERMS = {
36
'a': [0, 2, 3, 5, 6, 7, 8, 9],
37
'b': [0, 1, 2, 3, 4, 7, 8, 9],
38
+
'c': [0, 1, 3, 4, 5, 6, 7, 8, 9],
39
'd': [0, 2, 3, 5, 6, 8, 9],
40
'e': [0, 2, 6, 8],
41
+
'f': [0, 4, 5, 6, 8, 9],
42
'g': [2, 3, 4, 5, 6, 8, 9],
43
}
44