+81

bcd_22input.dot

reviewed

··· 1 1 + digraph BCD_7Seg { 2 2 + label="BCD to 7-Segment Decoder\n22 gate inputs (8x2-input + 2x3-input)"; 3 3 + labelloc="t"; 4 4 + fontsize=16; 5 5 + rankdir=LR; 6 6 + splines=ortho; 7 7 + nodesep=0.5; 8 8 + ranksep=1.0; 9 9 + 10 10 + subgraph cluster_inputs { 11 11 + label="Inputs"; 12 12 + style=dashed; 13 13 + A [shape=circle, style=filled, fillcolor=lightblue, label="A"]; 14 14 + B [shape=circle, style=filled, fillcolor=lightblue, label="B"]; 15 15 + C [shape=circle, style=filled, fillcolor=lightblue, label="C"]; 16 16 + D [shape=circle, style=filled, fillcolor=lightblue, label="D"]; 17 17 + nA [shape=circle, style=filled, fillcolor=lightcyan, label="A'"]; 18 18 + nB [shape=circle, style=filled, fillcolor=lightcyan, label="B'"]; 19 19 + nC [shape=circle, style=filled, fillcolor=lightcyan, label="C'"]; 20 20 + nD [shape=circle, style=filled, fillcolor=lightcyan, label="D'"]; 21 21 + } 22 22 + 23 23 + subgraph cluster_gates { 24 24 + label="Logic Gates"; 25 25 + style=dashed; 26 26 + g0 [shape=box, style=filled, fillcolor=peachpuff, label="NOR"]; 27 27 + g1 [shape=box, style=filled, fillcolor=lightyellow, label="XOR"]; 28 28 + g2 [shape=box, style=filled, fillcolor=lightyellow, label="XOR"]; 29 29 + g3 [shape=box, style=filled, fillcolor=palegreen, label="NAND"]; 30 30 + g4 [shape=box, style=filled, fillcolor=palegreen, label="NAND"]; 31 31 + g5 [shape=box, style=filled, fillcolor=lightsalmon, label="OR"]; 32 32 + g6 [shape=box, style=filled, fillcolor=lightgreen, label="AND"]; 33 33 + g7 [shape=box, style=filled, fillcolor=lightsalmon, label="OR"]; 34 34 + g8 [shape=box, style=filled, fillcolor=coral, label="OR3"]; 35 35 + g9 [shape=box, style=filled, fillcolor=plum, label="SPECIAL"]; 36 36 + } 37 37 + 38 38 + // Connections 39 39 + A -> g0; 40 40 + C -> g0; 41 41 + B -> g1; 42 42 + g0 -> g1; 43 43 + D -> g2; 44 44 + g1 -> g2; 45 45 + B -> g3; 46 46 + g2 -> g3; 47 47 + g1 -> g4; 48 48 + g3 -> g4; 49 49 + g0 -> g5 [taillabel="'"]; 50 50 + g2 -> g5; 51 51 + nD -> g6; 52 52 + g5 -> g6; 53 53 + g2 -> g7; 54 54 + g6 -> g7; 55 55 + nA -> g8 [taillabel="'"]; 56 56 + g2 -> g8; 57 57 + g6 -> g8; 58 58 + D -> g9; 59 59 + nC -> g9; 60 60 + g2 -> g9; 61 61 + 62 62 + subgraph cluster_outputs { 63 63 + label="Outputs"; 64 64 + style=dashed; 65 65 + out_a [shape=doublecircle, style=filled, fillcolor=lightpink, label="a"]; 66 66 + out_b [shape=doublecircle, style=filled, fillcolor=lightpink, label="b"]; 67 67 + out_c [shape=doublecircle, style=filled, fillcolor=lightpink, label="c"]; 68 68 + out_d [shape=doublecircle, style=filled, fillcolor=lightpink, label="d"]; 69 69 + out_e [shape=doublecircle, style=filled, fillcolor=lightpink, label="e"]; 70 70 + out_f [shape=doublecircle, style=filled, fillcolor=lightpink, label="f"]; 71 71 + out_g [shape=doublecircle, style=filled, fillcolor=lightpink, label="g"]; 72 72 + } 73 73 + 74 74 + g5 -> out_a; 75 75 + g3 -> out_b; 76 76 + g8 -> out_c; 77 77 + g7 -> out_d; 78 78 + g6 -> out_e; 79 79 + g9 -> out_f; 80 80 + g4 -> out_g; 81 81 + }

bcd_22input.png

reviewed

This is a binary file and will not be displayed.

+344 -3

bcd_optimization/solver.py

reviewed

··· 410 410 411 411 # Constraint 3b: Restrict to standard gate functions 412 412 if restrict_functions: 413 413 - # 2-input: AND, OR, XOR, NAND, NOR (no XNOR - use XOR+INV if needed) 414 414 - allowed_2input = [0b1000, 0b1110, 0b0110, 0b0111, 0b0001] 413 413 + # 2-input: AND, OR, XOR, XNOR, NAND, NOR 414 414 + allowed_2input = [0b1000, 0b1110, 0b0110, 0b1001, 0b0111, 0b0001] 415 415 for gate_idx in range(num_2input): 416 416 i = n_inputs + gate_idx 417 417 or_clause = [] ··· 428 428 cnf.append([-match_var, -f2[i][p][q]]) 429 429 cnf.append(or_clause) 430 430 431 431 - # 3-input: AND3, OR3, XOR3, NAND3, NOR3 (user's available gates) 431 431 + # 3-input: AND3, OR3, XOR3, XNOR3, NAND3, NOR3 432 432 allowed_3input = [ 433 433 0b10000000, # AND3 434 434 0b11111110, # OR3 435 435 0b01111111, # NAND3 436 436 0b00000001, # NOR3 437 437 0b10010110, # XOR3 (odd parity) 438 438 + 0b01101001, # XNOR3 (even parity) 438 439 ] 439 440 for gate_idx in range(num_2input, num_2input + num_3input): 440 441 i = n_inputs + gate_idx ··· 585 586 0b00010111: "MIN", # Minority 586 587 } 587 588 return known.get(func, f"F3_{func:08b}") 589 589 + 590 590 + def _decode_4input_function(self, func: int) -> str: 591 591 + """Decode 16-bit function for 4-input gate.""" 592 592 + known = { 593 593 + 0x0001: "NOR4", 594 594 + 0x7FFF: "NAND4", 595 595 + 0x8000: "AND4", 596 596 + 0xFFFE: "OR4", 597 597 + 0x6996: "XOR4", # Odd parity 598 598 + 0x9669: "XNOR4", # Even parity 599 599 + } 600 600 + return known.get(func, f"F4_{func:016b}") 601 601 + 602 602 + def _try_general_synthesis(self, num_2input: int, num_3input: int, num_4input: int, 603 603 + use_complements: bool = True, restrict_functions: bool = True) -> Optional[SynthesisResult]: 604 604 + """Try synthesis with a mix of 2, 3, and 4-input gates.""" 605 605 + n_primary = 4 606 606 + n_inputs = 8 if use_complements else 4 607 607 + n_outputs = 7 608 608 + n_gates = num_2input + num_3input + num_4input 609 609 + n_nodes = n_inputs + n_gates 610 610 + 611 611 + truth_rows = list(range(10)) 612 612 + n_rows = len(truth_rows) 613 613 + 614 614 + cnf = CNF() 615 615 + var_counter = [1] 616 616 + 617 617 + def new_var(): 618 618 + v = var_counter[0] 619 619 + var_counter[0] += 1 620 620 + return v 621 621 + 622 622 + # x[i][t] = output of node i on row t 623 623 + x = {i: {t: new_var() for t in range(n_rows)} for i in range(n_nodes)} 624 624 + 625 625 + # Selection and function variables for each gate size 626 626 + s2, s3, s4 = {}, {}, {} 627 627 + f2, f3, f4 = {}, {}, {} 628 628 + 629 629 + # Assign gate types: first num_2input are 2-input, then num_3input are 3-input, rest are 4-input 630 630 + gate_sizes = [2] * num_2input + [3] * num_3input + [4] * num_4input 631 631 + 632 632 + for gate_idx in range(n_gates): 633 633 + i = n_inputs + gate_idx 634 634 + size = gate_sizes[gate_idx] 635 635 + 636 636 + if size == 2: 637 637 + s2[i] = {} 638 638 + for j in range(i): 639 639 + s2[i][j] = {k: new_var() for k in range(j + 1, i)} 640 640 + f2[i] = {p: {q: new_var() for q in range(2)} for p in range(2)} 641 641 + elif size == 3: 642 642 + s3[i] = {} 643 643 + for j in range(i): 644 644 + s3[i][j] = {} 645 645 + for k in range(j + 1, i): 646 646 + s3[i][j][k] = {l: new_var() for l in range(k + 1, i)} 647 647 + f3[i] = {p: {q: {r: new_var() for r in range(2)} for q in range(2)} for p in range(2)} 648 648 + else: # size == 4 649 649 + s4[i] = {} 650 650 + for j in range(i): 651 651 + s4[i][j] = {} 652 652 + for k in range(j + 1, i): 653 653 + s4[i][j][k] = {} 654 654 + for l in range(k + 1, i): 655 655 + s4[i][j][k][l] = {m: new_var() for m in range(l + 1, i)} 656 656 + f4[i] = {p: {q: {r: {s: new_var() for s in range(2)} for r in range(2)} for q in range(2)} for p in range(2)} 657 657 + 658 658 + # g[h][i] = output h comes from node i 659 659 + g = {h: {i: new_var() for i in range(n_nodes)} for h in range(n_outputs)} 660 660 + 661 661 + # Constraint 1: Primary inputs fixed by truth table 662 662 + for t_idx, t in enumerate(truth_rows): 663 663 + for i in range(n_primary): 664 664 + bit = (t >> (n_primary - 1 - i)) & 1 665 665 + cnf.append([x[i][t_idx] if bit else -x[i][t_idx]]) 666 666 + if use_complements: 667 667 + for i in range(n_primary): 668 668 + bit = (t >> (n_primary - 1 - i)) & 1 669 669 + cnf.append([x[n_primary + i][t_idx] if not bit else -x[n_primary + i][t_idx]]) 670 670 + 671 671 + # Constraint 2: Each gate has exactly one input selection 672 672 + for gate_idx in range(n_gates): 673 673 + i = n_inputs + gate_idx 674 674 + size = gate_sizes[gate_idx] 675 675 + 676 676 + if size == 2: 677 677 + all_sels = [s2[i][j][k] for j in range(i) for k in range(j + 1, i)] 678 678 + elif size == 3: 679 679 + all_sels = [s3[i][j][k][l] for j in range(i) for k in range(j + 1, i) for l in range(k + 1, i)] 680 680 + else: 681 681 + all_sels = [s4[i][j][k][l][m] for j in range(i) for k in range(j + 1, i) for l in range(k + 1, i) for m in range(l + 1, i)] 682 682 + 683 683 + if not all_sels: 684 684 + return None # Not enough nodes for this gate size 685 685 + 686 686 + cnf.append(all_sels) # At least one 687 687 + for idx1, sel1 in enumerate(all_sels): 688 688 + for sel2 in all_sels[idx1 + 1:]: 689 689 + cnf.append([-sel1, -sel2]) # At most one 690 690 + 691 691 + # Constraint 3: Gate function consistency 692 692 + for gate_idx in range(n_gates): 693 693 + i = n_inputs + gate_idx 694 694 + size = gate_sizes[gate_idx] 695 695 + 696 696 + if size == 2: 697 697 + for j in range(i): 698 698 + for k in range(j + 1, i): 699 699 + for t_idx in range(n_rows): 700 700 + for pv in range(2): 701 701 + for qv in range(2): 702 702 + for outv in range(2): 703 703 + clause = [-s2[i][j][k]] 704 704 + clause.append(-x[j][t_idx] if pv else x[j][t_idx]) 705 705 + clause.append(-x[k][t_idx] if qv else x[k][t_idx]) 706 706 + clause.append(-f2[i][pv][qv] if outv else f2[i][pv][qv]) 707 707 + clause.append(x[i][t_idx] if outv else -x[i][t_idx]) 708 708 + cnf.append(clause) 709 709 + elif size == 3: 710 710 + for j in range(i): 711 711 + for k in range(j + 1, i): 712 712 + for l in range(k + 1, i): 713 713 + for t_idx in range(n_rows): 714 714 + for pv in range(2): 715 715 + for qv in range(2): 716 716 + for rv in range(2): 717 717 + for outv in range(2): 718 718 + clause = [-s3[i][j][k][l]] 719 719 + clause.append(-x[j][t_idx] if pv else x[j][t_idx]) 720 720 + clause.append(-x[k][t_idx] if qv else x[k][t_idx]) 721 721 + clause.append(-x[l][t_idx] if rv else x[l][t_idx]) 722 722 + clause.append(-f3[i][pv][qv][rv] if outv else f3[i][pv][qv][rv]) 723 723 + clause.append(x[i][t_idx] if outv else -x[i][t_idx]) 724 724 + cnf.append(clause) 725 725 + else: # size == 4 726 726 + for j in range(i): 727 727 + for k in range(j + 1, i): 728 728 + for l in range(k + 1, i): 729 729 + for m in range(l + 1, i): 730 730 + for t_idx in range(n_rows): 731 731 + for pv in range(2): 732 732 + for qv in range(2): 733 733 + for rv in range(2): 734 734 + for sv in range(2): 735 735 + for outv in range(2): 736 736 + clause = [-s4[i][j][k][l][m]] 737 737 + clause.append(-x[j][t_idx] if pv else x[j][t_idx]) 738 738 + clause.append(-x[k][t_idx] if qv else x[k][t_idx]) 739 739 + clause.append(-x[l][t_idx] if rv else x[l][t_idx]) 740 740 + clause.append(-x[m][t_idx] if sv else x[m][t_idx]) 741 741 + clause.append(-f4[i][pv][qv][rv][sv] if outv else f4[i][pv][qv][rv][sv]) 742 742 + clause.append(x[i][t_idx] if outv else -x[i][t_idx]) 743 743 + cnf.append(clause) 744 744 + 745 745 + # Constraint 3b: Restrict to standard gate functions 746 746 + if restrict_functions: 747 747 + # 2-input: AND, OR, XOR, XNOR, NAND, NOR 748 748 + allowed_2input = [0b1000, 0b1110, 0b0110, 0b1001, 0b0111, 0b0001] 749 749 + 750 750 + # 3-input: AND3, OR3, XOR3, XNOR3, NAND3, NOR3 751 751 + allowed_3input = [0b10000000, 0b11111110, 0b01111111, 0b00000001, 0b10010110, 0b01101001] 752 752 + 753 753 + # 4-input: AND4, OR4, XOR4, XNOR4, NAND4, NOR4 754 754 + allowed_4input = [0x8000, 0xFFFE, 0x7FFF, 0x0001, 0x6996, 0x9669] 755 755 + 756 756 + for gate_idx in range(n_gates): 757 757 + i = n_inputs + gate_idx 758 758 + size = gate_sizes[gate_idx] 759 759 + 760 760 + if size == 2: 761 761 + or_clause = [] 762 762 + for func in allowed_2input: 763 763 + match_var = new_var() 764 764 + or_clause.append(match_var) 765 765 + for p in range(2): 766 766 + for q in range(2): 767 767 + bit_idx = p * 2 + q 768 768 + expected = (func >> bit_idx) & 1 769 769 + if expected: 770 770 + cnf.append([-match_var, f2[i][p][q]]) 771 771 + else: 772 772 + cnf.append([-match_var, -f2[i][p][q]]) 773 773 + cnf.append(or_clause) 774 774 + elif size == 3: 775 775 + or_clause = [] 776 776 + for func in allowed_3input: 777 777 + match_var = new_var() 778 778 + or_clause.append(match_var) 779 779 + for p in range(2): 780 780 + for q in range(2): 781 781 + for r in range(2): 782 782 + bit_idx = p * 4 + q * 2 + r 783 783 + expected = (func >> bit_idx) & 1 784 784 + if expected: 785 785 + cnf.append([-match_var, f3[i][p][q][r]]) 786 786 + else: 787 787 + cnf.append([-match_var, -f3[i][p][q][r]]) 788 788 + cnf.append(or_clause) 789 789 + else: # size == 4 790 790 + or_clause = [] 791 791 + for func in allowed_4input: 792 792 + match_var = new_var() 793 793 + or_clause.append(match_var) 794 794 + for p in range(2): 795 795 + for q in range(2): 796 796 + for r in range(2): 797 797 + for s in range(2): 798 798 + bit_idx = p * 8 + q * 4 + r * 2 + s 799 799 + expected = (func >> bit_idx) & 1 800 800 + if expected: 801 801 + cnf.append([-match_var, f4[i][p][q][r][s]]) 802 802 + else: 803 803 + cnf.append([-match_var, -f4[i][p][q][r][s]]) 804 804 + cnf.append(or_clause) 805 805 + 806 806 + # Constraint 4: Each output assigned to exactly one node 807 807 + for h in range(n_outputs): 808 808 + cnf.append([g[h][i] for i in range(n_nodes)]) 809 809 + for i in range(n_nodes): 810 810 + for j in range(i + 1, n_nodes): 811 811 + cnf.append([-g[h][i], -g[h][j]]) 812 812 + 813 813 + # Constraint 5: Output correctness 814 814 + for h, segment in enumerate(SEGMENT_NAMES): 815 815 + for t_idx, t in enumerate(truth_rows): 816 816 + expected = 1 if t in SEGMENT_MINTERMS[segment] else 0 817 817 + for i in range(n_nodes): 818 818 + if expected: 819 819 + cnf.append([-g[h][i], x[i][t_idx]]) 820 820 + else: 821 821 + cnf.append([-g[h][i], -x[i][t_idx]]) 822 822 + 823 823 + # Solve 824 824 + with Solver(bootstrap_with=cnf) as solver: 825 825 + if solver.solve(): 826 826 + model = set(solver.get_model()) 827 827 + return self._decode_general_solution( 828 828 + model, gate_sizes, n_inputs, n_nodes, 829 829 + x, s2, s3, s4, f2, f3, f4, g, use_complements 830 830 + ) 831 831 + return None 832 832 + 833 833 + def _decode_general_solution(self, model, gate_sizes, n_inputs, n_nodes, 834 834 + x, s2, s3, s4, f2, f3, f4, g, use_complements) -> SynthesisResult: 835 835 + """Decode SAT solution for general mixed gate sizes.""" 836 836 + def is_true(var): 837 837 + return var in model 838 838 + 839 839 + n_gates = len(gate_sizes) 840 840 + if use_complements: 841 841 + node_names = ['A', 'B', 'C', 'D', "A'", "B'", "C'", "D'"] + [f'g{i}' for i in range(n_gates)] 842 842 + else: 843 843 + node_names = ['A', 'B', 'C', 'D'] + [f'g{i}' for i in range(n_gates)] 844 844 + 845 845 + gates = [] 846 846 + total_cost = 0 847 847 + 848 848 + for gate_idx in range(n_gates): 849 849 + i = n_inputs + gate_idx 850 850 + size = gate_sizes[gate_idx] 851 851 + total_cost += size 852 852 + 853 853 + if size == 2: 854 854 + for j in range(i): 855 855 + for k in range(j + 1, i): 856 856 + if is_true(s2[i][j][k]): 857 857 + func = 0 858 858 + for p in range(2): 859 859 + for q in range(2): 860 860 + if is_true(f2[i][p][q]): 861 861 + func |= (1 << (p * 2 + q)) 862 862 + func_name = self._decode_gate_function(func) 863 863 + gates.append(GateInfo(index=gate_idx, input1=j, input2=k, func=func, func_name=func_name)) 864 864 + node_names[i] = f"({node_names[j]} {func_name} {node_names[k]})" 865 865 + break 866 866 + elif size == 3: 867 867 + for j in range(i): 868 868 + for k in range(j + 1, i): 869 869 + for l in range(k + 1, i): 870 870 + if is_true(s3[i][j][k][l]): 871 871 + func = 0 872 872 + for p in range(2): 873 873 + for q in range(2): 874 874 + for r in range(2): 875 875 + if is_true(f3[i][p][q][r]): 876 876 + func |= (1 << (p * 4 + q * 2 + r)) 877 877 + func_name = self._decode_3input_function(func) 878 878 + gates.append(GateInfo(index=gate_idx, input1=j, input2=(k, l), func=func, func_name=func_name)) 879 879 + node_names[i] = f"({node_names[j]} {func_name} {node_names[k]} {node_names[l]})" 880 880 + break 881 881 + else: # size == 4 882 882 + for j in range(i): 883 883 + for k in range(j + 1, i): 884 884 + for l in range(k + 1, i): 885 885 + for m in range(l + 1, i): 886 886 + if is_true(s4[i][j][k][l][m]): 887 887 + func = 0 888 888 + for p in range(2): 889 889 + for q in range(2): 890 890 + for r in range(2): 891 891 + for s in range(2): 892 892 + if is_true(f4[i][p][q][r][s]): 893 893 + func |= (1 << (p * 8 + q * 4 + r * 2 + s)) 894 894 + func_name = self._decode_4input_function(func) 895 895 + gates.append(GateInfo(index=gate_idx, input1=j, input2=(k, l, m), func=func, func_name=func_name)) 896 896 + node_names[i] = f"({node_names[j]} {func_name} {node_names[k]} {node_names[l]} {node_names[m]})" 897 897 + break 898 898 + 899 899 + # Map outputs 900 900 + output_map = {} 901 901 + expressions = {} 902 902 + for h, segment in enumerate(SEGMENT_NAMES): 903 903 + for i in range(n_nodes): 904 904 + if is_true(g[h][i]): 905 905 + output_map[segment] = i 906 906 + expressions[segment] = node_names[i] 907 907 + break 908 908 + 909 909 + num_2 = gate_sizes.count(2) 910 910 + num_3 = gate_sizes.count(3) 911 911 + num_4 = gate_sizes.count(4) 912 912 + cost_breakdown = CostBreakdown( 913 913 + and_inputs=total_cost, 914 914 + or_inputs=0, 915 915 + num_and_gates=n_gates, 916 916 + num_or_gates=0, 917 917 + ) 918 918 + 919 919 + return SynthesisResult( 920 920 + cost=total_cost, 921 921 + implicants_by_output={}, 922 922 + shared_implicants=[], 923 923 + method=f"exact_general_{num_2}x2_{num_3}x3_{num_4}x4", 924 924 + expressions=expressions, 925 925 + cost_breakdown=cost_breakdown, 926 926 + gates=gates, 927 927 + output_map=output_map, 928 928 + ) 588 929 589 930 def _try_exact_synthesis(self, num_gates: int, use_complements: bool = False, restrict_functions: bool = False) -> Optional[SynthesisResult]: 590 931 """

+183

search_optimal.py

reviewed

··· 1 1 + #!/usr/bin/env python3 2 2 + """ 3 3 + Search for optimal BCD to 7-segment decoder circuit. 4 4 + Uses parallel SAT solving to search multiple configurations simultaneously. 5 5 + """ 6 6 + 7 7 + import multiprocessing as mp 8 8 + from concurrent.futures import ProcessPoolExecutor, as_completed 9 9 + import sys 10 10 + import time 11 11 + 12 12 + from bcd_optimization.solver import BCDTo7SegmentSolver 13 13 + from bcd_optimization.truth_tables import SEGMENT_MINTERMS, SEGMENT_NAMES 14 14 + 15 15 + 16 16 + def try_config(args): 17 17 + """Try a single (n2, n3) configuration. Run in separate process.""" 18 18 + n2, n3, use_complements, restrict_functions = args 19 19 + cost = n2 * 2 + n3 * 3 20 20 + n_gates = n2 + n3 21 21 + 22 22 + if n_gates < 7: 23 23 + return None, cost, f"Skipped (only {n_gates} gates)" 24 24 + 25 25 + solver = BCDTo7SegmentSolver() 26 26 + solver.generate_prime_implicants() 27 27 + 28 28 + try: 29 29 + result = solver._try_mixed_synthesis(n2, n3, use_complements, restrict_functions) 30 30 + if result: 31 31 + return result, cost, "SUCCESS" 32 32 + else: 33 33 + return None, cost, "UNSAT" 34 34 + except Exception as e: 35 35 + return None, cost, f"Error: {e}" 36 36 + 37 37 + 38 38 + def verify_result(result): 39 39 + """Verify a synthesis result is correct.""" 40 40 + def eval_func2(func, a, b): 41 41 + return (func >> (a * 2 + b)) & 1 42 42 + 43 43 + def eval_func3(func, a, b, c): 44 44 + return (func >> (a * 4 + b * 2 + c)) & 1 45 45 + 46 46 + for digit in range(10): 47 47 + A = (digit >> 3) & 1 48 48 + B = (digit >> 2) & 1 49 49 + C = (digit >> 1) & 1 50 50 + D = digit & 1 51 51 + 52 52 + nodes = [A, B, C, D, 1-A, 1-B, 1-C, 1-D] 53 53 + 54 54 + for g in result.gates: 55 55 + if isinstance(g.input2, tuple): 56 56 + k, l = g.input2 57 57 + val = eval_func3(g.func, nodes[g.input1], nodes[k], nodes[l]) 58 58 + else: 59 59 + val = eval_func2(g.func, nodes[g.input1], nodes[g.input2]) 60 60 + nodes.append(val) 61 61 + 62 62 + for seg in SEGMENT_NAMES: 63 63 + expected = 1 if digit in SEGMENT_MINTERMS[seg] else 0 64 64 + actual = nodes[result.output_map[seg]] 65 65 + if actual != expected: 66 66 + return False, f"Digit {digit}, {seg}: expected {expected}, got {actual}" 67 67 + 68 68 + return True, "All correct" 69 69 + 70 70 + 71 71 + def main(): 72 72 + print("=" * 60) 73 73 + print("BCD to 7-Segment Optimal Circuit Search") 74 74 + print("=" * 60) 75 75 + print() 76 76 + print("Gates: AND, OR, XOR, NAND, NOR (2 and 3 input variants)") 77 77 + print("Primary input complements (A', B', C', D') are free") 78 78 + print() 79 79 + 80 80 + # Configurations to try, sorted by cost 81 81 + configs = [] 82 82 + for n2 in range(0, 15): 83 83 + for n3 in range(0, 8): 84 84 + cost = n2 * 2 + n3 * 3 85 85 + n_gates = n2 + n3 86 86 + if 7 <= n_gates <= 12 and 18 <= cost <= 22: 87 87 + configs.append((n2, n3, True, True)) 88 88 + 89 89 + # Sort by cost, then by number of gates 90 90 + configs.sort(key=lambda x: (x[0]*2 + x[1]*3, x[0]+x[1])) 91 91 + 92 92 + print(f"Searching {len(configs)} configurations from {min(c[0]*2+c[1]*3 for c in configs)} to {max(c[0]*2+c[1]*3 for c in configs)} inputs") 93 93 + print(f"Using {mp.cpu_count()} CPU cores") 94 94 + print() 95 95 + 96 96 + best_result = None 97 97 + best_cost = float('inf') 98 98 + 99 99 + start_time = time.time() 100 100 + 101 101 + # Group configs by cost for better progress reporting 102 102 + cost_groups = {} 103 103 + for cfg in configs: 104 104 + cost = cfg[0] * 2 + cfg[1] * 3 105 105 + if cost not in cost_groups: 106 106 + cost_groups[cost] = [] 107 107 + cost_groups[cost].append(cfg) 108 108 + 109 109 + with ProcessPoolExecutor(max_workers=mp.cpu_count()) as executor: 110 110 + for cost in sorted(cost_groups.keys()): 111 111 + if cost >= best_cost: 112 112 + continue 113 113 + 114 114 + group = cost_groups[cost] 115 115 + print(f"Trying {cost} inputs ({len(group)} configurations)...", flush=True) 116 116 + 117 117 + futures = {executor.submit(try_config, cfg): cfg for cfg in group} 118 118 + 119 119 + for future in as_completed(futures): 120 120 + cfg = futures[future] 121 121 + n2, n3 = cfg[0], cfg[1] 122 122 + 123 123 + try: 124 124 + result, result_cost, status = future.result(timeout=300) 125 125 + 126 126 + if result is not None: 127 127 + valid, msg = verify_result(result) 128 128 + if valid: 129 129 + print(f" {n2}x2 + {n3}x3 = {result_cost}: {status} (verified)") 130 130 + if result_cost < best_cost: 131 131 + best_result = result 132 132 + best_cost = result_cost 133 133 + # Cancel remaining futures at this cost level 134 134 + for f in futures: 135 135 + f.cancel() 136 136 + break 137 137 + else: 138 138 + print(f" {n2}x2 + {n3}x3 = {result_cost}: INVALID - {msg}") 139 139 + else: 140 140 + print(f" {n2}x2 + {n3}x3 = {result_cost}: {status}") 141 141 + 142 142 + except Exception as e: 143 143 + print(f" {n2}x2 + {n3}x3: Error - {e}") 144 144 + 145 145 + if best_result is not None and best_cost <= cost: 146 146 + print(f"\nFound solution at {best_cost} inputs, stopping search.") 147 147 + break 148 148 + 149 149 + elapsed = time.time() - start_time 150 150 + 151 151 + print() 152 152 + print("=" * 60) 153 153 + print("RESULTS") 154 154 + print("=" * 60) 155 155 + print(f"Search time: {elapsed:.1f} seconds") 156 156 + 157 157 + if best_result: 158 158 + print(f"Best solution: {best_cost} gate inputs") 159 159 + print() 160 160 + print("Gates:") 161 161 + 162 162 + node_names = ['A', 'B', 'C', 'D', "A'", "B'", "C'", "D'"] 163 163 + for g in best_result.gates: 164 164 + i1 = node_names[g.input1] 165 165 + if isinstance(g.input2, tuple): 166 166 + k, l = g.input2 167 167 + i2, i3 = node_names[k], node_names[l] 168 168 + print(f" g{g.index}: {g.func_name}({i1}, {i2}, {i3})") 169 169 + else: 170 170 + i2 = node_names[g.input2] 171 171 + print(f" g{g.index}: {g.func_name}({i1}, {i2})") 172 172 + node_names.append(f"g{g.index}") 173 173 + 174 174 + print() 175 175 + print("Outputs:") 176 176 + for seg in SEGMENT_NAMES: 177 177 + print(f" {seg} = {node_names[best_result.output_map[seg]]}") 178 178 + else: 179 179 + print("No solution found in the search range.") 180 180 + 181 181 + 182 182 + if __name__ == "__main__": 183 183 + main()

+196

search_with_4input.py

reviewed

··· 1 1 + #!/usr/bin/env python3 2 2 + """ 3 3 + Search for optimal BCD to 7-segment decoder circuit with 2, 3, and 4-input gates. 4 4 + """ 5 5 + 6 6 + import multiprocessing as mp 7 7 + from concurrent.futures import ProcessPoolExecutor, as_completed 8 8 + import sys 9 9 + import time 10 10 + 11 11 + from bcd_optimization.solver import BCDTo7SegmentSolver 12 12 + from bcd_optimization.truth_tables import SEGMENT_MINTERMS, SEGMENT_NAMES 13 13 + 14 14 + 15 15 + def try_config(args): 16 16 + """Try a single (n2, n3, n4) configuration. Run in separate process.""" 17 17 + n2, n3, n4, use_complements, restrict_functions = args 18 18 + cost = n2 * 2 + n3 * 3 + n4 * 4 19 19 + n_gates = n2 + n3 + n4 20 20 + 21 21 + if n_gates < 7: 22 22 + return None, cost, f"Skipped (only {n_gates} gates)" 23 23 + 24 24 + solver = BCDTo7SegmentSolver() 25 25 + solver.generate_prime_implicants() 26 26 + 27 27 + try: 28 28 + result = solver._try_general_synthesis(n2, n3, n4, use_complements, restrict_functions) 29 29 + if result: 30 30 + return result, cost, "SUCCESS" 31 31 + else: 32 32 + return None, cost, "UNSAT" 33 33 + except Exception as e: 34 34 + return None, cost, f"Error: {e}" 35 35 + 36 36 + 37 37 + def verify_result(result): 38 38 + """Verify a synthesis result is correct.""" 39 39 + def eval_func2(func, a, b): 40 40 + return (func >> (a * 2 + b)) & 1 41 41 + 42 42 + def eval_func3(func, a, b, c): 43 43 + return (func >> (a * 4 + b * 2 + c)) & 1 44 44 + 45 45 + def eval_func4(func, a, b, c, d): 46 46 + return (func >> (a * 8 + b * 4 + c * 2 + d)) & 1 47 47 + 48 48 + for digit in range(10): 49 49 + A = (digit >> 3) & 1 50 50 + B = (digit >> 2) & 1 51 51 + C = (digit >> 1) & 1 52 52 + D = digit & 1 53 53 + 54 54 + nodes = [A, B, C, D, 1-A, 1-B, 1-C, 1-D] 55 55 + 56 56 + for g in result.gates: 57 57 + if isinstance(g.input2, tuple): 58 58 + if len(g.input2) == 2: 59 59 + k, l = g.input2 60 60 + val = eval_func3(g.func, nodes[g.input1], nodes[k], nodes[l]) 61 61 + else: 62 62 + k, l, m = g.input2 63 63 + val = eval_func4(g.func, nodes[g.input1], nodes[k], nodes[l], nodes[m]) 64 64 + else: 65 65 + val = eval_func2(g.func, nodes[g.input1], nodes[g.input2]) 66 66 + nodes.append(val) 67 67 + 68 68 + for seg in SEGMENT_NAMES: 69 69 + expected = 1 if digit in SEGMENT_MINTERMS[seg] else 0 70 70 + actual = nodes[result.output_map[seg]] 71 71 + if actual != expected: 72 72 + return False, f"Digit {digit}, {seg}: expected {expected}, got {actual}" 73 73 + 74 74 + return True, "All correct" 75 75 + 76 76 + 77 77 + def main(): 78 78 + print("=" * 60) 79 79 + print("BCD to 7-Segment Optimal Circuit Search (with 4-input gates)") 80 80 + print("=" * 60) 81 81 + print() 82 82 + print("Gates: AND, OR, XOR, XNOR, NAND, NOR (2, 3, and 4 input variants)") 83 83 + print("Primary input complements (A', B', C', D') are free") 84 84 + print() 85 85 + 86 86 + # Generate configurations sorted by cost 87 87 + configs = [] 88 88 + for n2 in range(0, 12): 89 89 + for n3 in range(0, 8): 90 90 + for n4 in range(0, 6): 91 91 + cost = n2 * 2 + n3 * 3 + n4 * 4 92 92 + n_gates = n2 + n3 + n4 93 93 + # Need at least 7 gates for 7 outputs 94 94 + # Limit to reasonable ranges 95 95 + if 7 <= n_gates <= 11 and 14 <= cost <= 22: 96 96 + configs.append((n2, n3, n4, True, True)) 97 97 + 98 98 + # Sort by cost, then by number of gates 99 99 + configs.sort(key=lambda x: (x[0]*2 + x[1]*3 + x[2]*4, x[0]+x[1]+x[2])) 100 100 + 101 101 + print(f"Searching {len(configs)} configurations from {min(c[0]*2+c[1]*3+c[2]*4 for c in configs)} to {max(c[0]*2+c[1]*3+c[2]*4 for c in configs)} inputs") 102 102 + print(f"Using {mp.cpu_count()} CPU cores") 103 103 + print() 104 104 + 105 105 + best_result = None 106 106 + best_cost = float('inf') 107 107 + 108 108 + start_time = time.time() 109 109 + 110 110 + # Group configs by cost 111 111 + cost_groups = {} 112 112 + for cfg in configs: 113 113 + cost = cfg[0] * 2 + cfg[1] * 3 + cfg[2] * 4 114 114 + if cost not in cost_groups: 115 115 + cost_groups[cost] = [] 116 116 + cost_groups[cost].append(cfg) 117 117 + 118 118 + with ProcessPoolExecutor(max_workers=mp.cpu_count()) as executor: 119 119 + for cost in sorted(cost_groups.keys()): 120 120 + if cost >= best_cost: 121 121 + continue 122 122 + 123 123 + group = cost_groups[cost] 124 124 + print(f"Trying {cost} inputs ({len(group)} configurations)...", flush=True) 125 125 + 126 126 + futures = {executor.submit(try_config, cfg): cfg for cfg in group} 127 127 + 128 128 + for future in as_completed(futures): 129 129 + cfg = futures[future] 130 130 + n2, n3, n4 = cfg[0], cfg[1], cfg[2] 131 131 + 132 132 + try: 133 133 + result, result_cost, status = future.result(timeout=300) 134 134 + 135 135 + if result is not None: 136 136 + valid, msg = verify_result(result) 137 137 + if valid: 138 138 + print(f" {n2}x2 + {n3}x3 + {n4}x4 = {result_cost}: {status} (verified)") 139 139 + if result_cost < best_cost: 140 140 + best_result = result 141 141 + best_cost = result_cost 142 142 + for f in futures: 143 143 + f.cancel() 144 144 + break 145 145 + else: 146 146 + print(f" {n2}x2 + {n3}x3 + {n4}x4 = {result_cost}: INVALID - {msg}") 147 147 + else: 148 148 + print(f" {n2}x2 + {n3}x3 + {n4}x4 = {result_cost}: {status}") 149 149 + 150 150 + except Exception as e: 151 151 + print(f" {n2}x2 + {n3}x3 + {n4}x4: Error - {e}") 152 152 + 153 153 + if best_result is not None and best_cost <= cost: 154 154 + print(f"\nFound solution at {best_cost} inputs, stopping search.") 155 155 + break 156 156 + 157 157 + elapsed = time.time() - start_time 158 158 + 159 159 + print() 160 160 + print("=" * 60) 161 161 + print("RESULTS") 162 162 + print("=" * 60) 163 163 + print(f"Search time: {elapsed:.1f} seconds") 164 164 + 165 165 + if best_result: 166 166 + print(f"Best solution: {best_cost} gate inputs") 167 167 + print() 168 168 + print("Gates:") 169 169 + 170 170 + node_names = ['A', 'B', 'C', 'D', "A'", "B'", "C'", "D'"] 171 171 + for g in best_result.gates: 172 172 + i1 = node_names[g.input1] 173 173 + if isinstance(g.input2, tuple): 174 174 + if len(g.input2) == 2: 175 175 + k, l = g.input2 176 176 + i2, i3 = node_names[k], node_names[l] 177 177 + print(f" g{g.index}: {g.func_name}({i1}, {i2}, {i3})") 178 178 + else: 179 179 + k, l, m = g.input2 180 180 + i2, i3, i4 = node_names[k], node_names[l], node_names[m] 181 181 + print(f" g{g.index}: {g.func_name}({i1}, {i2}, {i3}, {i4})") 182 182 + else: 183 183 + i2 = node_names[g.input2] 184 184 + print(f" g{g.index}: {g.func_name}({i1}, {i2})") 185 185 + node_names.append(f"g{g.index}") 186 186 + 187 187 + print() 188 188 + print("Outputs:") 189 189 + for seg in SEGMENT_NAMES: 190 190 + print(f" {seg} = {node_names[best_result.output_map[seg]]}") 191 191 + else: 192 192 + print("No solution found in the search range.") 193 193 + 194 194 + 195 195 + if __name__ == "__main__": 196 196 + main()