Translating HOL functions to hardware: multiplier example


  Start with a recursion equation in higher order logic

MultIter (m,n,acc) = if m = 0 then (0,n,acc) else MultIter (m-1,n,n+acc)

Automatically compile to an implementation represented in logic (here's how).

    |- InfRise clk ==>
       (?v0 v1 v2 v3 v4 v5 v6 v7 v8 v9 v10 v11 v12 v13 v14 v15 v16 v17 v18
           v19 v20 v21 v22 v23 v24 v25 v26 v27 v28 v29 v30 v31 v32 v33 v34
           v35 v36 v37 v38 v39 v40 v41 v42 v43 v44 v45 v46 v47 v48 v49 v50
           v51 v52 v53 v54 v55 v56 v57.
          DtypeT (clk,load,v21) /\ NOT (v21,v20) /\ AND (v20,load,v19) /\
          Dtype (clk,done,v18) /\ AND (v19,v18,v17) /\ OR (v17,v16,v11) /\
          DtypeT (clk,v15,v23) /\ NOT (v23,v22) /\ AND (v22,v15,v16) /\
          MUX (v16,v14,inp1,v3) /\ MUX (v16,v13,inp2,v2) /\
          MUX (v16,v12,inp3,v1) /\ DtypeT (clk,v11,v26) /\ NOT (v26,v25) /\
          AND (v25,v11,v24) /\ MUX (v24,v3,v27,v10) /\
          Dtype (clk,v10,v27) /\ DtypeT (clk,v11,v30) /\ NOT (v30,v29) /\
          AND (v29,v11,v28) /\ MUX (v28,v2,v31,v9) /\ Dtype (clk,v9,v31) /\
          DtypeT (clk,v11,v34) /\ NOT (v34,v33) /\ AND (v33,v11,v32) /\
          MUX (v32,v1,v35,v8) /\ Dtype (clk,v8,v35) /\
          DtypeT (clk,v11,v39) /\ NOT (v39,v38) /\ AND (v38,v11,v37) /\
          NOT (v37,v7) /\ CONSTANT 0 v40 /\ EQ (v3,v40,v36) /\
          Dtype (clk,v36,v6) /\ DtypeT (clk,v7,v44) /\ NOT (v44,v43) /\
          AND (v43,v7,v42) /\ AND (v42,v6,v5) /\ NOT (v6,v41) /\
          AND (v41,v42,v4) /\ DtypeT (clk,v5,v48) /\ NOT (v48,v47) /\
          AND (v47,v5,v46) /\ NOT (v46,v0) /\ CONSTANT 0 v45 /\
          Dtype (clk,v45,out1) /\ Dtype (clk,v9,out2) /\
          Dtype (clk,v8,out3) /\ DtypeT (clk,v4,v53) /\ NOT (v53,v52) /\
          AND (v52,v4,v51) /\ NOT (v51,v15) /\ CONSTANT 1 v54 /\
          SUB (v10,v54,v50) /\ ADD (v9,v8,v49) /\ Dtype (clk,v50,v14) /\
          Dtype (clk,v9,v13) /\ Dtype (clk,v49,v12) /\
          Dtype (clk,v15,v56) /\ AND (v15,v56,v55) /\ AND (v0,v7,v57) /\
          AND (v57,v55,done)) ==>
       DEV MultIter
         (load at clk,(inp1 <> inp2 <> inp3) at clk,done at clk,
          (out1 <> out2 <> out3) at clk) : thm

This is converted to Verilog. The modules needed are shown below. Those that are automatically generated during compilation have the HOL they implement printed in comments for easy visual comparison.

// Definition of module MultIter [Created: Mon Apr 25 09:37:28 2005]

// Definitions of components used in MultIter

// Read only register
module CONSTANT (out);
 parameter size  = 31;
 parameter value = 0;
 output [size:0] out;

 assign out = value;

endmodule

// Verilog module implementing HOL unary operator
// $~ :bool -> bool
//
// Automatically generated definition of NOT
module NOT (inp,out);
 parameter inpsize = 0;
 parameter outsize = 0;
 input   [inpsize:0] inp;
 output  [outsize:0] out;

 assign out = ! inp;

endmodule

// Combinational multiplexer
module MUX (sw,in1,in2,out);
 parameter size = 31;
 input sw;
 input  [size:0] in1,in2;
 output [size:0] out;

 assign out = sw?in1:in2;

endmodule

// Verilog module implementing HOL binary operator
// UNCURRY $/\ :bool # bool -> bool
//
// Automatically generated definition of AND
module AND (in1,in2,out);
 parameter in1size = 0;
 parameter in2size = 0;
 parameter outsize = 0;
 input   [in1size:0] in1;
 input   [in2size:0] in2;
 output  [outsize:0] out;

 assign out = in1 && in2;

endmodule

// Verilog module implementing HOL binary operator
// UNCURRY $\/ :bool # bool -> bool
//
// Automatically generated definition of OR
module OR (in1,in2,out);
 parameter in1size = 0;
 parameter in2size = 0;
 parameter outsize = 0;
 input   [in1size:0] in1;
 input   [in2size:0] in2;
 output  [outsize:0] out;

 assign out = in1 || in2;

endmodule

// Positive edge triggered Dtype register
module Dtype (clk,d,q);
 parameter size = 31;
 input clk;
 input  [size:0] d;
 output [size:0] q;
 reg    [size:0] q;

 initial q = 0;

 always @(posedge clk) q <= d;

endmodule

// Boolean positive edge triggered flip-flop starting in state 1
module DtypeT (clk,d,q);
 input clk,d;
 output q;
 reg q;

 initial q = 1;

 always @(posedge clk) q <= d;

endmodule

// Verilog module implementing HOL binary operator
// UNCURRY $+ :num # num -> num
//
// Automatically generated definition of ADD
module ADD (in1,in2,out);
 parameter in1size = 31;
 parameter in2size = 31;
 parameter outsize = 31;
 input   [in1size:0] in1;
 input   [in2size:0] in2;
 output  [outsize:0] out;

 assign out = in1 + in2;

endmodule

// Verilog module implementing HOL binary operator
// UNCURRY $- :num # num -> num
//
// Automatically generated definition of SUB
module SUB (in1,in2,out);
 parameter in1size = 31;
 parameter in2size = 31;
 parameter outsize = 31;
 input   [in1size:0] in1;
 input   [in2size:0] in2;
 output  [outsize:0] out;

 assign out = in1 - in2;

endmodule

// Verilog module implementing HOL binary operator
// UNCURRY $= :num # num -> bool
//
// Automatically generated definition of EQ
module EQ (in1,in2,out);
 parameter in1size = 31;
 parameter in2size = 31;
 parameter outsize = 0;
 input   [in1size:0] in1;
 input   [in2size:0] in2;
 output  [outsize:0] out;

 assign out = in1 == in2;

endmodule

Using these modules, the multiplier is then generated from the compiled HOL. The HOL terms used to generate the module instances are shown in comments.

// Definition of module MultIter
module MultIter (clk,load,inp1,inp2,inp3,done,out1,out2,out3);
 input clk,load;
 input [31:0] inp1;
 input [31:0] inp2;
 input [31:0] inp3;
 output done;
 output [31:0] out1;
 output [31:0] out2;
 output [31:0] out3;
 wire clk,done;

 wire [0:0] v0;
 wire [31:0] v1;
 wire [31:0] v2;
 wire [31:0] v3;
 wire [0:0] v4;
 wire [0:0] v5;
 wire [0:0] v6;
 wire [0:0] v7;
 wire [31:0] v8;
 wire [31:0] v9;
 wire [31:0] v10;
 wire [0:0] v11;
 wire [31:0] v12;
 wire [31:0] v13;
 wire [31:0] v14;
 wire [0:0] v15;
 wire [0:0] v16;
 wire [0:0] v17;
 wire [0:0] v18;
 wire [0:0] v19;
 wire [0:0] v20;
 wire [0:0] v21;
 wire [0:0] v22;
 wire [0:0] v23;
 wire [0:0] v24;
 wire [0:0] v25;
 wire [0:0] v26;
 wire [31:0] v27;
 wire [0:0] v28;
 wire [0:0] v29;
 wire [0:0] v30;
 wire [31:0] v31;
 wire [0:0] v32;
 wire [0:0] v33;
 wire [0:0] v34;
 wire [31:0] v35;
 wire [0:0] v36;
 wire [0:0] v37;
 wire [0:0] v38;
 wire [0:0] v39;
 wire [31:0] v40;
 wire [0:0] v41;
 wire [0:0] v42;
 wire [0:0] v43;
 wire [0:0] v44;
 wire [31:0] v45;
 wire [0:0] v46;
 wire [0:0] v47;
 wire [0:0] v48;
 wire [31:0] v49;
 wire [31:0] v50;
 wire [0:0] v51;
 wire [0:0] v52;
 wire [0:0] v53;
 wire [31:0] v54;
 wire [0:0] v55;
 wire [0:0] v56;
 wire [0:0] v57;

 /* DtypeT ((clk :num -> bool),(load :num -> bool),(v21 :num -> bool)) */
 DtypeT        DtypeT_0 (clk,load,v21);

 /* NOT ((v21 :num -> bool),(v20 :num -> bool)) */
 NOT        NOT_0 (v21,v20);
   defparam NOT_0.inpsize = 0;
   defparam NOT_0.outsize = 0;

 /* AND ((v20 :num -> bool),(load :num -> bool),(v19 :num -> bool)) */
 AND        AND_0 (v20,load,v19);
   defparam AND_0.in1size = 0;
   defparam AND_0.in2size = 0;
   defparam AND_0.outsize = 0;

 /* Dtype ((clk :num -> bool),(done :num -> bool),(v18 :num -> bool)) */
 Dtype      Dtype_0 (clk,done,v18);
   defparam Dtype_0.size = 0;

 /* AND ((v19 :num -> bool),(v18 :num -> bool),(v17 :num -> bool)) */
 AND        AND_1 (v19,v18,v17);
   defparam AND_1.in1size = 0;
   defparam AND_1.in2size = 0;
   defparam AND_1.outsize = 0;

 /* OR ((v17 :num -> bool),(v16 :num -> bool),(v11 :num -> bool)) */
 OR        OR_0 (v17,v16,v11);
   defparam OR_0.in1size = 0;
   defparam OR_0.in2size = 0;
   defparam OR_0.outsize = 0;

 /* DtypeT ((clk :num -> bool),(v15 :num -> bool),(v23 :num -> bool)) */
 DtypeT        DtypeT_1 (clk,v15,v23);

 /* NOT ((v23 :num -> bool),(v22 :num -> bool)) */
 NOT        NOT_1 (v23,v22);
   defparam NOT_1.inpsize = 0;
   defparam NOT_1.outsize = 0;

 /* AND ((v22 :num -> bool),(v15 :num -> bool),(v16 :num -> bool)) */
 AND        AND_2 (v22,v15,v16);
   defparam AND_2.in1size = 0;
   defparam AND_2.in2size = 0;
   defparam AND_2.outsize = 0;

 /*
 MUX
  ((v16 :num -> bool),(v14 :num -> num),(inp1 :num -> num),
   (v3 :num -> num))
 */
 MUX        MUX_0 (v16,v14,inp1,v3);
   defparam MUX_0.size = 31;

 /*
 MUX
  ((v16 :num -> bool),(v13 :num -> num),(inp2 :num -> num),
   (v2 :num -> num))
 */
 MUX        MUX_1 (v16,v13,inp2,v2);
   defparam MUX_1.size = 31;

 /*
 MUX
  ((v16 :num -> bool),(v12 :num -> num),(inp3 :num -> num),
   (v1 :num -> num))
 */
 MUX        MUX_2 (v16,v12,inp3,v1);
   defparam MUX_2.size = 31;

 /* DtypeT ((clk :num -> bool),(v11 :num -> bool),(v26 :num -> bool)) */
 DtypeT        DtypeT_2 (clk,v11,v26);

 /* NOT ((v26 :num -> bool),(v25 :num -> bool)) */
 NOT        NOT_2 (v26,v25);
   defparam NOT_2.inpsize = 0;
   defparam NOT_2.outsize = 0;

 /* AND ((v25 :num -> bool),(v11 :num -> bool),(v24 :num -> bool)) */
 AND        AND_3 (v25,v11,v24);
   defparam AND_3.in1size = 0;
   defparam AND_3.in2size = 0;
   defparam AND_3.outsize = 0;

 /*
 MUX
  ((v24 :num -> bool),(v3 :num -> num),(v27 :num -> num),
   (v10 :num -> num))
 */
 MUX        MUX_3 (v24,v3,v27,v10);
   defparam MUX_3.size = 31;

 /* Dtype ((clk :num -> bool),(v10 :num -> num),(v27 :num -> num)) */
 Dtype      Dtype_1 (clk,v10,v27);
   defparam Dtype_1.size = 31;

 /* DtypeT ((clk :num -> bool),(v11 :num -> bool),(v30 :num -> bool)) */
 DtypeT        DtypeT_3 (clk,v11,v30);

 /* NOT ((v30 :num -> bool),(v29 :num -> bool)) */
 NOT        NOT_3 (v30,v29);
   defparam NOT_3.inpsize = 0;
   defparam NOT_3.outsize = 0;

 /* AND ((v29 :num -> bool),(v11 :num -> bool),(v28 :num -> bool)) */
 AND        AND_4 (v29,v11,v28);
   defparam AND_4.in1size = 0;
   defparam AND_4.in2size = 0;
   defparam AND_4.outsize = 0;

 /*
 MUX
  ((v28 :num -> bool),(v2 :num -> num),(v31 :num -> num),
   (v9 :num -> num))
 */
 MUX        MUX_4 (v28,v2,v31,v9);
   defparam MUX_4.size = 31;

 /* Dtype ((clk :num -> bool),(v9 :num -> num),(v31 :num -> num)) */
 Dtype      Dtype_2 (clk,v9,v31);
   defparam Dtype_2.size = 31;

 /* DtypeT ((clk :num -> bool),(v11 :num -> bool),(v34 :num -> bool)) */
 DtypeT        DtypeT_4 (clk,v11,v34);

 /* NOT ((v34 :num -> bool),(v33 :num -> bool)) */
 NOT        NOT_4 (v34,v33);
   defparam NOT_4.inpsize = 0;
   defparam NOT_4.outsize = 0;

 /* AND ((v33 :num -> bool),(v11 :num -> bool),(v32 :num -> bool)) */
 AND        AND_5 (v33,v11,v32);
   defparam AND_5.in1size = 0;
   defparam AND_5.in2size = 0;
   defparam AND_5.outsize = 0;

 /*
 MUX
  ((v32 :num -> bool),(v1 :num -> num),(v35 :num -> num),
   (v8 :num -> num))
 */
 MUX        MUX_5 (v32,v1,v35,v8);
   defparam MUX_5.size = 31;

 /* Dtype ((clk :num -> bool),(v8 :num -> num),(v35 :num -> num)) */
 Dtype      Dtype_3 (clk,v8,v35);
   defparam Dtype_3.size = 31;

 /* DtypeT ((clk :num -> bool),(v11 :num -> bool),(v39 :num -> bool)) */
 DtypeT        DtypeT_5 (clk,v11,v39);

 /* NOT ((v39 :num -> bool),(v38 :num -> bool)) */
 NOT        NOT_5 (v39,v38);
   defparam NOT_5.inpsize = 0;
   defparam NOT_5.outsize = 0;

 /* AND ((v38 :num -> bool),(v11 :num -> bool),(v37 :num -> bool)) */
 AND        AND_6 (v38,v11,v37);
   defparam AND_6.in1size = 0;
   defparam AND_6.in2size = 0;
   defparam AND_6.outsize = 0;

 /* NOT ((v37 :num -> bool),(v7 :num -> bool)) */
 NOT        NOT_6 (v37,v7);
   defparam NOT_6.inpsize = 0;
   defparam NOT_6.outsize = 0;

 /* CONSTANT (0 :num) (v40 :num -> num) */
 CONSTANT   CONSTANT_0 (v40);
   defparam CONSTANT_0.size  = 31;
   defparam CONSTANT_0.value = 0;

 /* EQ ((v3 :num -> num),(v40 :num -> num),(v36 :num -> bool)) */
 EQ        EQ_0 (v3,v40,v36);
   defparam EQ_0.in1size = 31;
   defparam EQ_0.in2size = 31;
   defparam EQ_0.outsize = 0;

 /* Dtype ((clk :num -> bool),(v36 :num -> bool),(v6 :num -> bool)) */
 Dtype      Dtype_4 (clk,v36,v6);
   defparam Dtype_4.size = 0;

 /* DtypeT ((clk :num -> bool),(v7 :num -> bool),(v44 :num -> bool)) */
 DtypeT        DtypeT_6 (clk,v7,v44);

 /* NOT ((v44 :num -> bool),(v43 :num -> bool)) */
 NOT        NOT_7 (v44,v43);
   defparam NOT_7.inpsize = 0;
   defparam NOT_7.outsize = 0;

 /* AND ((v43 :num -> bool),(v7 :num -> bool),(v42 :num -> bool)) */
 AND        AND_7 (v43,v7,v42);
   defparam AND_7.in1size = 0;
   defparam AND_7.in2size = 0;
   defparam AND_7.outsize = 0;

 /* AND ((v42 :num -> bool),(v6 :num -> bool),(v5 :num -> bool)) */
 AND        AND_8 (v42,v6,v5);
   defparam AND_8.in1size = 0;
   defparam AND_8.in2size = 0;
   defparam AND_8.outsize = 0;

 /* NOT ((v6 :num -> bool),(v41 :num -> bool)) */
 NOT        NOT_8 (v6,v41);
   defparam NOT_8.inpsize = 0;
   defparam NOT_8.outsize = 0;

 /* AND ((v41 :num -> bool),(v42 :num -> bool),(v4 :num -> bool)) */
 AND        AND_9 (v41,v42,v4);
   defparam AND_9.in1size = 0;
   defparam AND_9.in2size = 0;
   defparam AND_9.outsize = 0;

 /* DtypeT ((clk :num -> bool),(v5 :num -> bool),(v48 :num -> bool)) */
 DtypeT        DtypeT_7 (clk,v5,v48);

 /* NOT ((v48 :num -> bool),(v47 :num -> bool)) */
 NOT        NOT_9 (v48,v47);
   defparam NOT_9.inpsize = 0;
   defparam NOT_9.outsize = 0;

 /* AND ((v47 :num -> bool),(v5 :num -> bool),(v46 :num -> bool)) */
 AND        AND_10 (v47,v5,v46);
   defparam AND_10.in1size = 0;
   defparam AND_10.in2size = 0;
   defparam AND_10.outsize = 0;

 /* NOT ((v46 :num -> bool),(v0 :num -> bool)) */
 NOT        NOT_10 (v46,v0);
   defparam NOT_10.inpsize = 0;
   defparam NOT_10.outsize = 0;

 /* CONSTANT (0 :num) (v45 :num -> num) */
 CONSTANT   CONSTANT_1 (v45);
   defparam CONSTANT_1.size  = 31;
   defparam CONSTANT_1.value = 0;

 /* Dtype ((clk :num -> bool),(v45 :num -> num),(out1 :num -> num)) */
 Dtype      Dtype_5 (clk,v45,out1);
   defparam Dtype_5.size = 31;

 /* Dtype ((clk :num -> bool),(v9 :num -> num),(out2 :num -> num)) */
 Dtype      Dtype_6 (clk,v9,out2);
   defparam Dtype_6.size = 31;

 /* Dtype ((clk :num -> bool),(v8 :num -> num),(out3 :num -> num)) */
 Dtype      Dtype_7 (clk,v8,out3);
   defparam Dtype_7.size = 31;

 /* DtypeT ((clk :num -> bool),(v4 :num -> bool),(v53 :num -> bool)) */
 DtypeT        DtypeT_8 (clk,v4,v53);

 /* NOT ((v53 :num -> bool),(v52 :num -> bool)) */
 NOT        NOT_11 (v53,v52);
   defparam NOT_11.inpsize = 0;
   defparam NOT_11.outsize = 0;

 /* AND ((v52 :num -> bool),(v4 :num -> bool),(v51 :num -> bool)) */
 AND        AND_11 (v52,v4,v51);
   defparam AND_11.in1size = 0;
   defparam AND_11.in2size = 0;
   defparam AND_11.outsize = 0;

 /* NOT ((v51 :num -> bool),(v15 :num -> bool)) */
 NOT        NOT_12 (v51,v15);
   defparam NOT_12.inpsize = 0;
   defparam NOT_12.outsize = 0;

 /* CONSTANT (1 :num) (v54 :num -> num) */
 CONSTANT   CONSTANT_2 (v54);
   defparam CONSTANT_2.size  = 31;
   defparam CONSTANT_2.value = 1;

 /* SUB ((v10 :num -> num),(v54 :num -> num),(v50 :num -> num)) */
 SUB        SUB_0 (v10,v54,v50);
   defparam SUB_0.in1size = 31;
   defparam SUB_0.in2size = 31;
   defparam SUB_0.outsize = 31;

 /* ADD ((v9 :num -> num),(v8 :num -> num),(v49 :num -> num)) */
 ADD        ADD_0 (v9,v8,v49);
   defparam ADD_0.in1size = 31;
   defparam ADD_0.in2size = 31;
   defparam ADD_0.outsize = 31;

 /* Dtype ((clk :num -> bool),(v50 :num -> num),(v14 :num -> num)) */
 Dtype      Dtype_8 (clk,v50,v14);
   defparam Dtype_8.size = 31;

 /* Dtype ((clk :num -> bool),(v9 :num -> num),(v13 :num -> num)) */
 Dtype      Dtype_9 (clk,v9,v13);
   defparam Dtype_9.size = 31;

 /* Dtype ((clk :num -> bool),(v49 :num -> num),(v12 :num -> num)) */
 Dtype      Dtype_10 (clk,v49,v12);
   defparam Dtype_10.size = 31;

 /* Dtype ((clk :num -> bool),(v15 :num -> bool),(v56 :num -> bool)) */
 Dtype      Dtype_11 (clk,v15,v56);
   defparam Dtype_11.size = 0;

 /* AND ((v15 :num -> bool),(v56 :num -> bool),(v55 :num -> bool)) */
 AND        AND_12 (v15,v56,v55);
   defparam AND_12.in1size = 0;
   defparam AND_12.in2size = 0;
   defparam AND_12.outsize = 0;

 /* AND ((v0 :num -> bool),(v7 :num -> bool),(v57 :num -> bool)) */
 AND        AND_13 (v0,v7,v57);
   defparam AND_13.in1size = 0;
   defparam AND_13.in2size = 0;
   defparam AND_13.outsize = 0;

 /* AND ((v57 :num -> bool),(v55 :num -> bool),(done :num -> bool)) */
 AND        AND_14 (v57,v55,done);
   defparam AND_14.in1size = 0;
   defparam AND_14.in2size = 0;
   defparam AND_14.outsize = 0;

endmodule

Add a testbench to evaluate MultIter (5,7,0).

// Clock
module Clock (clk);
 parameter period = 10; // time between clock edges
 output clk;
 reg clk;

 initial begin clk = 0; forever #period clk <= !clk; end

endmodule

module Main ();
 wire clk;
 reg  load;
 reg  [31:0] inp1;
 reg  [31:0] inp2;
 reg  [31:0] inp3;
 wire done;
 wire [31:0] out1;
 wire [31:0] out2;
 wire [31:0] out3;

 initial
  begin
   $dumpfile("MultIter.vcd");
   $dumpvars(1,clk,load,inp1,inp2,inp3,done,out1,out2,out3);
  end

 initial load = 0;

 always @(posedge clk) if (done)
                        begin
                         #1 load = 1;
                         #1 inp1 = 5; inp2 = 7; inp3 = 0; 
                         forever @(posedge clk) if (done) $finish;
                        end

 Clock      Clock_0 (clk);
   defparam Clock_0.period = 5;

 MultIter    MultIter (clk,load,inp1,inp2,inp3,done,out1,out2,out3);

endmodule

Simulate and view waveform:

If the values on Main.inp1, Main.inp2 and Main.inp3 are 5, 7 and 0, respectively when Main.load is asserted, then when Main.done is subsequently high, the values on Main.out1, Main.out2 and Main.out3 are 0, 7 and 35 ( i.e. 5x7), respectively.

 


Page maintained by Mike Gordon
Sun Apr 24 2005