|
Direct Synthesis of Logic Using a SAT Solver
Almost Trivial, divide by 3 example.
In this example, we allow the SAT solver to make the state assignment
for a divide by 3 circuit. We give it 3 flip-flops, so one-hot coding
is one solution it might choose.
The flip-flops are s1 to s3. The next-state function is selected
by the SAT solver by filling in values for xa and xb variables.
The SAT solver also generates logic to implement the counter by
giving values to the xxx variables.
The H1 source code for this example is as follows. All variables
whose names start with `x' will be allocated constant values by the
SAT solver.
// Almost trivial, divide by 3 example.
\A s1, s2, s3;
a = xa1 & s1 | xa2 & ~s1 | xa3 & s2 | xa4 & ~s2 | xa5 & s3 | xa6 & ~s3;
na = xa1 & vs1 | xa2 & ~vs1 | xa3 & vs2 | xa4 & ~vs2 | xa5 & vs3 | xa6 & ~vs3;
b = xb1 & s1 | xb2 & ~s1 | xb3 & s2 | xb4 & ~s2 | xb5 & s3 | xb6 & ~s3;
nb = xb1 & vs1 | xb2 & ~vs1 | xb3 & vs2 | xb4 & ~vs2 | xb5 & vs3 | xb6 & ~vs3;
state1 = a & b; state2 = a & ~b; state3 = ~a & ~b;
nstate1 = na & nb; nstate2 = na & ~nb; nstate3 = ~na & ~nb;
// assert that one state or another is always active.
always state1 | state2 | state3;
//
always state1 => nstate2; always state2 => nstate3; always state3 => nstate1;
vs1 = xxxa1 & s1 | xxxa2 & ~s1 | xxxa3 & s2 | xxxa4 & ~s2 | xxxa5 & s3 | xxxa6 & ~s3;
vs2 = xxxb1 & s1 | xxxb2 & ~s1 | xxxb3 & s2 | xxxb4 & ~s2 | xxxb5 & s3 | xxxb6 & ~s3;
vs3 = xxxc1 & s1 | xxxc2 & ~s1 | xxxc3 & s2 | xxxc4 & ~s2 | xxxc5 & s3 | xxxc6 & ~s3;
X(s1) = vs1;
X(s2) = vs2;
X(s3) = vs3;
// eof
A shortcoming of this simple source file is that it forces all 8 settings
of the state variables to be part of the main count sequence, whereas
normal hardware design requires that the circuit is self-starting, in
that any setting of the state variables will cause it to eventually enter into
the desired sequence.
Expanded H1 code
Here is the expanded SML representation of the input file.
(* prob_pins.sml *)
open hprls_hdr;
val pindump = [
("xb6", 1) ,
("xb5", 2) ,
("xb4", 3) ,
("xb3", 4) ,
("xb2", 5) ,
("xb1", 6) ,
("xa6", 7) ,
("xa5", 8) ,
("xa4", 9) ,
("xa3", 10) ,
("xa2", 11) ,
("xa1", 12) ,
("xxxc6", 13) ,
("xxxc5", 14) ,
("xxxc4", 15) ,
("xxxc3", 16) ,
("xxxc2", 17) ,
("xxxc1", 18) ,
("xxxb6", 19) ,
("xxxb5", 20) ,
("xxxb4", 21) ,
("xxxb3", 22) ,
("xxxb2", 23) ,
("xxxb1", 24) ,
("xxxa6", 25) ,
("xxxa5", 26) ,
("xxxa4", 27) ,
("xxxa3", 28) ,
("xxxa2", 29) ,
("xxxa1", 30) ];
val hprls_equations = [
x_diadic(v_interm, x_net("vs3"),x_diadic(v_bitor, x_diadic(v_bitand,
x_not(x_net("s3")),x_net("xxxc6")),x_diadic(v_bitor,
x_diadic(v_bitand, x_net("s3"),x_net("xxxc5")),x_diadic(v_bitor,
x_diadic(v_bitand,
x_not(x_net("s2")),x_net("xxxc4")),x_diadic(v_bitor,
x_diadic(v_bitand, x_net("s2"),x_net("xxxc3")),x_diadic(v_bitor,
x_diadic(v_bitand,
x_not(x_net("s1")),x_net("xxxc2")),x_diadic(v_bitand,
x_net("s1"),x_net("xxxc1"))))))))
, x_diadic(v_interm, x_net("vs2"),x_diadic(v_bitor, x_diadic(v_bitand,
x_not(x_net("s3")),x_net("xxxb6")),x_diadic(v_bitor,
x_diadic(v_bitand, x_net("s3"),x_net("xxxb5")),x_diadic(v_bitor,
x_diadic(v_bitand,
x_not(x_net("s2")),x_net("xxxb4")),x_diadic(v_bitor,
x_diadic(v_bitand, x_net("s2"),x_net("xxxb3")),x_diadic(v_bitor,
x_diadic(v_bitand,
x_not(x_net("s1")),x_net("xxxb2")),x_diadic(v_bitand,
x_net("s1"),x_net("xxxb1"))))))))
, x_diadic(v_interm, x_net("vs1"),x_diadic(v_bitor, x_diadic(v_bitand,
x_not(x_net("s3")),x_net("xxxa6")),x_diadic(v_bitor,
x_diadic(v_bitand, x_net("s3"),x_net("xxxa5")),x_diadic(v_bitor,
x_diadic(v_bitand,
x_not(x_net("s2")),x_net("xxxa4")),x_diadic(v_bitor,
x_diadic(v_bitand, x_net("s2"),x_net("xxxa3")),x_diadic(v_bitor,
x_diadic(v_bitand,
x_not(x_net("s1")),x_net("xxxa2")),x_diadic(v_bitand,
x_net("s1"),x_net("xxxa1"))))))))
, x_diadic(v_interm, x_net("nstate3"),x_diadic(v_bitand,
x_not(x_net("nb")),x_not(x_net("na"))))
, x_diadic(v_interm, x_net("nstate2"),x_diadic(v_bitand,
x_not(x_net("nb")),x_net("na")))
, x_diadic(v_interm, x_net("nstate1"),x_diadic(v_bitand,
x_net("nb"),x_net("na")))
, x_diadic(v_interm, x_net("state3"),x_diadic(v_bitand,
x_not(x_net("b")),x_not(x_net("a"))))
, x_diadic(v_interm, x_net("state2"),x_diadic(v_bitand,
x_not(x_net("b")),x_net("a")))
, x_diadic(v_interm, x_net("state1"),x_diadic(v_bitand,
x_net("b"),x_net("a")))
, x_diadic(v_interm, x_net("nb"),x_diadic(v_bitor, x_diadic(v_bitand,
x_not(x_net("vs3")),x_net("xb6")),x_diadic(v_bitor, x_diadic(v_bitand,
x_net("vs3"),x_net("xb5")),x_diadic(v_bitor, x_diadic(v_bitand,
x_not(x_net("vs2")),x_net("xb4")),x_diadic(v_bitor, x_diadic(v_bitand,
x_net("vs2"),x_net("xb3")),x_diadic(v_bitor, x_diadic(v_bitand,
x_not(x_net("vs1")),x_net("xb2")),x_diadic(v_bitand,
x_net("vs1"),x_net("xb1"))))))))
, x_diadic(v_interm, x_net("b"),x_diadic(v_bitor, x_diadic(v_bitand,
x_not(x_net("s3")),x_net("xb6")),x_diadic(v_bitor, x_diadic(v_bitand,
x_net("s3"),x_net("xb5")),x_diadic(v_bitor, x_diadic(v_bitand,
x_not(x_net("s2")),x_net("xb4")),x_diadic(v_bitor, x_diadic(v_bitand,
x_net("s2"),x_net("xb3")),x_diadic(v_bitor, x_diadic(v_bitand,
x_not(x_net("s1")),x_net("xb2")),x_diadic(v_bitand,
x_net("s1"),x_net("xb1"))))))))
, x_diadic(v_interm, x_net("na"),x_diadic(v_bitor, x_diadic(v_bitand,
x_not(x_net("vs3")),x_net("xa6")),x_diadic(v_bitor, x_diadic(v_bitand,
x_net("vs3"),x_net("xa5")),x_diadic(v_bitor, x_diadic(v_bitand,
x_not(x_net("vs2")),x_net("xa4")),x_diadic(v_bitor, x_diadic(v_bitand,
x_net("vs2"),x_net("xa3")),x_diadic(v_bitor, x_diadic(v_bitand,
x_not(x_net("vs1")),x_net("xa2")),x_diadic(v_bitand,
x_net("vs1"),x_net("xa1"))))))))
, x_diadic(v_interm, x_net("a"),x_diadic(v_bitor, x_diadic(v_bitand,
x_not(x_net("s3")),x_net("xa6")),x_diadic(v_bitor, x_diadic(v_bitand,
x_net("s3"),x_net("xa5")),x_diadic(v_bitor, x_diadic(v_bitand,
x_not(x_net("s2")),x_net("xa4")),x_diadic(v_bitor, x_diadic(v_bitand,
x_net("s2"),x_net("xa3")),x_diadic(v_bitor, x_diadic(v_bitand,
x_not(x_net("s1")),x_net("xa2")),x_diadic(v_bitand,
x_net("s1"),x_net("xa1"))))))))
,
x_diadic(v_interm, x_x(x_net("s1"), 1),x_net("vs1"))
,
x_diadic(v_interm, x_x(x_net("s2"), 1),x_net("vs2"))
,
x_diadic(v_interm, x_x(x_net("s3"), 1),x_net("vs3"))
];
(* eof *)
And here is the sat output:
-1 -2 3 -4 -5 -6 7 -8 9 -10
-11 -12 -13 -14 -15 16 -17 -18 19 -20
21 -22 -23 -24 -25 -26 -27 -28 29 -30
Gate-level output.
After re-hydrating the logic equations using the constant
values supplied by the first solution from the SAT solver, and trimming
gates using normal identities, we obtain
the following logic circuit:
module circuit(clk, rst);
input clk;
input rst;
wire b137;
wire g136;
wire g135;
wire g134;
wire b133;
wire g132;
wire g131;
wire g130;
wire b129;
wire g128;
wire b127;
wire g126;
wire b125;
wire g124;
wire b123;
wire g122;
wire g121;
wire b120;
wire g119;
wire g118;
wire g117;
wire b116;
wire g115;
wire b114;
wire g113;
wire g112;
wire b111;
wire g110;
wire g109;
wire g108;
wire b107;
wire g106;
wire b105;
wire g104;
wire g103;
wire g102;
wire b101;
DFF it140(s3, vs3, clk, 1, rst, 0);
DFF it139(s2, vs2, clk, 1, rst, 0);
DFF it138(s1, vs1, clk, 1, rst, 0);
BUF ib137(a, g136);
OR2 ig136(g136, g134, g135);
INV ig135(g135, s2);
INV ig134(g134, s3);
BUF ib133(na, g132);
OR2 ig132(g132, g130, g131);
INV ig131(g131, vs2);
INV ig130(g130, vs3);
BUF ib129(b, g128);
INV ig128(g128, s2);
BUF ib127(nb, g126);
INV ig126(g126, vs2);
BUF ib125(state1, g124);
AND2 ig124(g124, b, a);
BUF ib123(state2, g122);
AND2 ig122(g122, g121, a);
INV ig121(g121, b);
BUF ib120(state3, g119);
AND2 ig119(g119, g117, g118);
INV ig118(g118, a);
INV ig117(g117, b);
BUF ib116(nstate1, g115);
AND2 ig115(g115, nb, na);
BUF ib114(nstate2, g113);
AND2 ig113(g113, g112, na);
INV ig112(g112, nb);
BUF ib111(nstate3, g110);
AND2 ig110(g110, g108, g109);
INV ig109(g109, na);
INV ig108(g108, nb);
BUF ib107(vs1, g106);
INV ig106(g106, s1);
BUF ib105(vs2, g104);
OR2 ig104(g104, g102, g103);
INV ig103(g103, s2);
INV ig102(g102, s3);
BUF ib101(vs3, s2);
endmodule
Here is the simulation trace for this circuit: postscript file.
|