Translating HOL functions to hardware: factorial example


  Start with recursion equations in higher order logic

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

FACT n = if n=0 then 1 else Mult(n, FACT(n-1))

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 v58 v59 v60 v61 v62 v63 v64 v65 v66
           v67 v68 v69 v70 v71 v72 v73 v74 v75 v76 v77 v78 v79 v80 v81 v82
           v83 v84 v85 v86 v87 v88 v89 v90 v91 v92 v93 v94 v95 v96 v97 v98
           v99 v100 v101 v102 v103 v104 v105 v106 v107 v108 v109 v110 v111
           v112 v113 v114 v115 v116 v117 v118 v119 v120 v121 v122 v123 v124
           v125 v126 v127 v128.
          CONSTANT 1 v0 /\ DtypeT (clk,load,v20) /\ NOT (v20,v19) /\
          AND (v19,load,v18) /\ Dtype (clk,done,v17) /\ AND (v18,v17,v16) /\
          OR (v16,v15,v11) /\ DtypeT (clk,v14,v22) /\ NOT (v22,v21) /\
          AND (v21,v14,v15) /\ MUX (v15,v13,inp,v4) /\
          MUX (v15,v12,v0,v3) /\ DtypeT (clk,v11,v25) /\ NOT (v25,v24) /\
          AND (v24,v11,v23) /\ MUX (v23,v4,v26,v10) /\
          Dtype (clk,v10,v26) /\ DtypeT (clk,v11,v29) /\ NOT (v29,v28) /\
          AND (v28,v11,v27) /\ MUX (v27,v3,v30,v9) /\ Dtype (clk,v9,v30) /\
          DtypeT (clk,v11,v34) /\ NOT (v34,v33) /\ AND (v33,v11,v32) /\
          NOT (v32,v8) /\ CONSTANT 0 v35 /\ EQ (v4,v35,v31) /\
          Dtype (clk,v31,v7) /\ DtypeT (clk,v8,v39) /\ NOT (v39,v38) /\
          AND (v38,v8,v37) /\ AND (v37,v7,v6) /\ NOT (v7,v36) /\
          AND (v36,v37,v5) /\ DtypeT (clk,v6,v42) /\ NOT (v42,v41) /\
          AND (v41,v6,v40) /\ NOT (v40,v2) /\ Dtype (clk,v10,v1) /\
          Dtype (clk,v9,out) /\ DtypeT (clk,v5,v51) /\ NOT (v51,v50) /\
          AND (v50,v5,v49) /\ Dtype (clk,v14,v48) /\ AND (v49,v48,v47) /\
          DtypeT (clk,v47,v55) /\ NOT (v55,v54) /\ AND (v54,v47,v53) /\
          NOT (v53,v46) /\ CONSTANT 1 v56 /\ SUB (v10,v56,v52) /\
          Dtype (clk,v52,v44) /\ CONSTANT 0 v57 /\ DtypeT (clk,v47,v81) /\
          NOT (v81,v80) /\ AND (v80,v47,v79) /\ Dtype (clk,v45,v78) /\
          AND (v79,v78,v77) /\ OR (v77,v76,v71) /\ DtypeT (clk,v75,v83) /\
          NOT (v83,v82) /\ AND (v82,v75,v76) /\ MUX (v76,v74,v10,v63) /\
          MUX (v76,v73,v9,v62) /\ MUX (v76,v72,v57,v61) /\
          DtypeT (clk,v71,v86) /\ NOT (v86,v85) /\ AND (v85,v71,v84) /\
          MUX (v84,v63,v87,v70) /\ Dtype (clk,v70,v87) /\
          DtypeT (clk,v71,v90) /\ NOT (v90,v89) /\ AND (v89,v71,v88) /\
          MUX (v88,v62,v91,v69) /\ Dtype (clk,v69,v91) /\
          DtypeT (clk,v71,v94) /\ NOT (v94,v93) /\ AND (v93,v71,v92) /\
          MUX (v92,v61,v95,v68) /\ Dtype (clk,v68,v95) /\
          DtypeT (clk,v71,v99) /\ NOT (v99,v98) /\ AND (v98,v71,v97) /\
          NOT (v97,v67) /\ CONSTANT 0 v100 /\ EQ (v63,v100,v96) /\
          Dtype (clk,v96,v66) /\ DtypeT (clk,v67,v104) /\ NOT (v104,v103) /\
          AND (v103,v67,v102) /\ AND (v102,v66,v65) /\ NOT (v66,v101) /\
          AND (v101,v102,v64) /\ DtypeT (clk,v65,v108) /\ NOT (v108,v107) /\
          AND (v107,v65,v106) /\ NOT (v106,v60) /\ CONSTANT 0 v105 /\
          Dtype (clk,v105,v58) /\ Dtype (clk,v69,v59) /\
          Dtype (clk,v68,v43) /\ DtypeT (clk,v64,v113) /\ NOT (v113,v112) /\
          AND (v112,v64,v111) /\ NOT (v111,v75) /\ CONSTANT 1 v114 /\
          SUB (v70,v114,v110) /\ ADD (v69,v68,v109) /\
          Dtype (clk,v110,v74) /\ Dtype (clk,v69,v73) /\
          Dtype (clk,v109,v72) /\ Dtype (clk,v75,v116) /\
          AND (v75,v116,v115) /\ AND (v60,v67,v117) /\
          AND (v117,v115,v45) /\ DtypeT (clk,v46,v120) /\ NOT (v120,v119) /\
          AND (v119,v46,v118) /\ MUX (v118,v44,v121,v13) /\
          Dtype (clk,v13,v121) /\ DtypeT (clk,v45,v124) /\
          NOT (v124,v123) /\ AND (v123,v45,v122) /\
          MUX (v122,v43,v125,v12) /\ Dtype (clk,v12,v125) /\
          AND (v46,v45,v14) /\ Dtype (clk,v14,v127) /\
          AND (v14,v127,v126) /\ AND (v2,v8,v128) /\
          AND (v128,v126,done)) ==>
       DEV FACT (load at clk,inp at clk,done at clk,out at clk)

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 FACT [Created: Sun Apr 24 20:59:13 2005]

// Definitions of components used in FACT

// 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, a module to compute the factirial function is then generated from the compiled HOL. The HOL terms used to generate the module instances are shown in comments.

// Definition of module FACT
module FACT (clk,load,inp,done,out);
 input clk,load;
 input [31:0] inp;
 output done;
 output [31:0] out;
 wire clk,done;

 wire [31:0] v0;
 wire [31:0] v1;
 wire [0:0] v2;
 wire [31:0] v3;
 wire [31:0] v4;
 wire [0:0] v5;
 wire [0:0] v6;
 wire [0:0] v7;
 wire [0:0] v8;
 wire [31:0] v9;
 wire [31:0] v10;
 wire [0:0] v11;
 wire [31:0] v12;
 wire [31:0] v13;
 wire [0: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 [31:0] v26;
 wire [0:0] v27;
 wire [0:0] v28;
 wire [0:0] v29;
 wire [31:0] v30;
 wire [0: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 [0:0] v40;
 wire [0:0] v41;
 wire [0:0] v42;
 wire [31:0] v43;
 wire [31:0] v44;
 wire [0:0] v45;
 wire [0:0] v46;
 wire [0:0] v47;
 wire [0:0] v48;
 wire [0:0] v49;
 wire [0:0] v50;
 wire [0:0] v51;
 wire [31:0] v52;
 wire [0:0] v53;
 wire [0:0] v54;
 wire [0:0] v55;
 wire [31:0] v56;
 wire [31:0] v57;
 wire [31:0] v58;
 wire [31:0] v59;
 wire [0:0] v60;
 wire [31:0] v61;
 wire [31:0] v62;
 wire [31:0] v63;
 wire [0:0] v64;
 wire [0:0] v65;
 wire [0:0] v66;
 wire [0:0] v67;
 wire [31:0] v68;
 wire [31:0] v69;
 wire [31:0] v70;
 wire [0:0] v71;
 wire [31:0] v72;
 wire [31:0] v73;
 wire [31:0] v74;
 wire [0:0] v75;
 wire [0:0] v76;
 wire [0:0] v77;
 wire [0:0] v78;
 wire [0:0] v79;
 wire [0:0] v80;
 wire [0:0] v81;
 wire [0:0] v82;
 wire [0:0] v83;
 wire [0:0] v84;
 wire [0:0] v85;
 wire [0:0] v86;
 wire [31:0] v87;
 wire [0:0] v88;
 wire [0:0] v89;
 wire [0:0] v90;
 wire [31:0] v91;
 wire [0:0] v92;
 wire [0:0] v93;
 wire [0:0] v94;
 wire [31:0] v95;
 wire [0:0] v96;
 wire [0:0] v97;
 wire [0:0] v98;
 wire [0:0] v99;
 wire [31:0] v100;
 wire [0:0] v101;
 wire [0:0] v102;
 wire [0:0] v103;
 wire [0:0] v104;
 wire [31:0] v105;
 wire [0:0] v106;
 wire [0:0] v107;
 wire [0:0] v108;
 wire [31:0] v109;
 wire [31:0] v110;
 wire [0:0] v111;
 wire [0:0] v112;
 wire [0:0] v113;
 wire [31:0] v114;
 wire [0:0] v115;
 wire [0:0] v116;
 wire [0:0] v117;
 wire [0:0] v118;
 wire [0:0] v119;
 wire [0:0] v120;
 wire [31:0] v121;
 wire [0:0] v122;
 wire [0:0] v123;
 wire [0:0] v124;
 wire [31:0] v125;
 wire [0:0] v126;
 wire [0:0] v127;
 wire [0:0] v128;

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

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

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

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

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

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

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

 /* DtypeT ((clk :num -> bool),(v14 :num -> bool),(v22 :num -> bool)) */
 DtypeT        DtypeT_1 (clk,v14,v22);

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

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

 /*
 MUX
  ((v15 :num -> bool),(v13 :num -> num),(inp :num -> num),
   (v4 :num -> num))
 */
 MUX        MUX_0 (v15,v13,inp,v4);
   defparam MUX_0.size = 31;

 /*
 MUX
  ((v15 :num -> bool),(v12 :num -> num),(v0 :num -> num),
   (v3 :num -> num))
 */
 MUX        MUX_1 (v15,v12,v0,v3);
   defparam MUX_1.size = 31;

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

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

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

 /*
 MUX
  ((v23 :num -> bool),(v4 :num -> num),(v26 :num -> num),
   (v10 :num -> num))
 */
 MUX        MUX_2 (v23,v4,v26,v10);
   defparam MUX_2.size = 31;

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

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

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

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

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

 /* Dtype ((clk :num -> bool),(v9 :num -> num),(v30 :num -> num)) */
 Dtype      Dtype_2 (clk,v9,v30);
   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;

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

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

 /* EQ ((v4 :num -> num),(v35 :num -> num),(v31 :num -> bool)) */
 EQ        EQ_0 (v4,v35,v31);
   defparam EQ_0.in1size = 31;
   defparam EQ_0.in2size = 31;
   defparam EQ_0.outsize = 0;

 /* Dtype ((clk :num -> bool),(v31 :num -> bool),(v7 :num -> bool)) */
 Dtype      Dtype_3 (clk,v31,v7);
   defparam Dtype_3.size = 0;

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

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

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

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

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

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

 /* DtypeT ((clk :num -> bool),(v6 :num -> bool),(v42 :num -> bool)) */
 DtypeT        DtypeT_6 (clk,v6,v42);

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

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

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

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

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

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

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

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

 /* Dtype ((clk :num -> bool),(v14 :num -> bool),(v48 :num -> bool)) */
 Dtype      Dtype_6 (clk,v14,v48);
   defparam Dtype_6.size = 0;

 /* AND ((v49 :num -> bool),(v48 :num -> bool),(v47 :num -> bool)) */
 AND        AND_11 (v49,v48,v47);
   defparam AND_11.in1size = 0;
   defparam AND_11.in2size = 0;
   defparam AND_11.outsize = 0;

 /* DtypeT ((clk :num -> bool),(v47 :num -> bool),(v55 :num -> bool)) */
 DtypeT        DtypeT_8 (clk,v47,v55);

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

 /* AND ((v54 :num -> bool),(v47 :num -> bool),(v53 :num -> bool)) */
 AND        AND_12 (v54,v47,v53);
   defparam AND_12.in1size = 0;
   defparam AND_12.in2size = 0;
   defparam AND_12.outsize = 0;

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

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

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

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

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

 /* DtypeT ((clk :num -> bool),(v47 :num -> bool),(v81 :num -> bool)) */
 DtypeT        DtypeT_9 (clk,v47,v81);

 /* NOT ((v81 :num -> bool),(v80 :num -> bool)) */
 NOT        NOT_13 (v81,v80);
   defparam NOT_13.inpsize = 0;
   defparam NOT_13.outsize = 0;

 /* AND ((v80 :num -> bool),(v47 :num -> bool),(v79 :num -> bool)) */
 AND        AND_13 (v80,v47,v79);
   defparam AND_13.in1size = 0;
   defparam AND_13.in2size = 0;
   defparam AND_13.outsize = 0;

 /* Dtype ((clk :num -> bool),(v45 :num -> bool),(v78 :num -> bool)) */
 Dtype      Dtype_8 (clk,v45,v78);
   defparam Dtype_8.size = 0;

 /* AND ((v79 :num -> bool),(v78 :num -> bool),(v77 :num -> bool)) */
 AND        AND_14 (v79,v78,v77);
   defparam AND_14.in1size = 0;
   defparam AND_14.in2size = 0;
   defparam AND_14.outsize = 0;

 /* OR ((v77 :num -> bool),(v76 :num -> bool),(v71 :num -> bool)) */
 OR        OR_1 (v77,v76,v71);
   defparam OR_1.in1size = 0;
   defparam OR_1.in2size = 0;
   defparam OR_1.outsize = 0;

 /* DtypeT ((clk :num -> bool),(v75 :num -> bool),(v83 :num -> bool)) */
 DtypeT        DtypeT_10 (clk,v75,v83);

 /* NOT ((v83 :num -> bool),(v82 :num -> bool)) */
 NOT        NOT_14 (v83,v82);
   defparam NOT_14.inpsize = 0;
   defparam NOT_14.outsize = 0;

 /* AND ((v82 :num -> bool),(v75 :num -> bool),(v76 :num -> bool)) */
 AND        AND_15 (v82,v75,v76);
   defparam AND_15.in1size = 0;
   defparam AND_15.in2size = 0;
   defparam AND_15.outsize = 0;

 /*
 MUX
  ((v76 :num -> bool),(v74 :num -> num),(v10 :num -> num),
   (v63 :num -> num))
 */
 MUX        MUX_4 (v76,v74,v10,v63);
   defparam MUX_4.size = 31;

 /*
 MUX
  ((v76 :num -> bool),(v73 :num -> num),(v9 :num -> num),
   (v62 :num -> num))
 */
 MUX        MUX_5 (v76,v73,v9,v62);
   defparam MUX_5.size = 31;

 /*
 MUX
  ((v76 :num -> bool),(v72 :num -> num),(v57 :num -> num),
   (v61 :num -> num))
 */
 MUX        MUX_6 (v76,v72,v57,v61);
   defparam MUX_6.size = 31;

 /* DtypeT ((clk :num -> bool),(v71 :num -> bool),(v86 :num -> bool)) */
 DtypeT        DtypeT_11 (clk,v71,v86);

 /* NOT ((v86 :num -> bool),(v85 :num -> bool)) */
 NOT        NOT_15 (v86,v85);
   defparam NOT_15.inpsize = 0;
   defparam NOT_15.outsize = 0;

 /* AND ((v85 :num -> bool),(v71 :num -> bool),(v84 :num -> bool)) */
 AND        AND_16 (v85,v71,v84);
   defparam AND_16.in1size = 0;
   defparam AND_16.in2size = 0;
   defparam AND_16.outsize = 0;

 /*
 MUX
  ((v84 :num -> bool),(v63 :num -> num),(v87 :num -> num),
   (v70 :num -> num))
 */
 MUX        MUX_7 (v84,v63,v87,v70);
   defparam MUX_7.size = 31;

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

 /* DtypeT ((clk :num -> bool),(v71 :num -> bool),(v90 :num -> bool)) */
 DtypeT        DtypeT_12 (clk,v71,v90);

 /* NOT ((v90 :num -> bool),(v89 :num -> bool)) */
 NOT        NOT_16 (v90,v89);
   defparam NOT_16.inpsize = 0;
   defparam NOT_16.outsize = 0;

 /* AND ((v89 :num -> bool),(v71 :num -> bool),(v88 :num -> bool)) */
 AND        AND_17 (v89,v71,v88);
   defparam AND_17.in1size = 0;
   defparam AND_17.in2size = 0;
   defparam AND_17.outsize = 0;

 /*
 MUX
  ((v88 :num -> bool),(v62 :num -> num),(v91 :num -> num),
   (v69 :num -> num))
 */
 MUX        MUX_8 (v88,v62,v91,v69);
   defparam MUX_8.size = 31;

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

 /* DtypeT ((clk :num -> bool),(v71 :num -> bool),(v94 :num -> bool)) */
 DtypeT        DtypeT_13 (clk,v71,v94);

 /* NOT ((v94 :num -> bool),(v93 :num -> bool)) */
 NOT        NOT_17 (v94,v93);
   defparam NOT_17.inpsize = 0;
   defparam NOT_17.outsize = 0;

 /* AND ((v93 :num -> bool),(v71 :num -> bool),(v92 :num -> bool)) */
 AND        AND_18 (v93,v71,v92);
   defparam AND_18.in1size = 0;
   defparam AND_18.in2size = 0;
   defparam AND_18.outsize = 0;

 /*
 MUX
  ((v92 :num -> bool),(v61 :num -> num),(v95 :num -> num),
   (v68 :num -> num))
 */
 MUX        MUX_9 (v92,v61,v95,v68);
   defparam MUX_9.size = 31;

 /* Dtype ((clk :num -> bool),(v68 :num -> num),(v95 :num -> num)) */
 Dtype      Dtype_11 (clk,v68,v95);
   defparam Dtype_11.size = 31;

 /* DtypeT ((clk :num -> bool),(v71 :num -> bool),(v99 :num -> bool)) */
 DtypeT        DtypeT_14 (clk,v71,v99);

 /* NOT ((v99 :num -> bool),(v98 :num -> bool)) */
 NOT        NOT_18 (v99,v98);
   defparam NOT_18.inpsize = 0;
   defparam NOT_18.outsize = 0;

 /* AND ((v98 :num -> bool),(v71 :num -> bool),(v97 :num -> bool)) */
 AND        AND_19 (v98,v71,v97);
   defparam AND_19.in1size = 0;
   defparam AND_19.in2size = 0;
   defparam AND_19.outsize = 0;

 /* NOT ((v97 :num -> bool),(v67 :num -> bool)) */
 NOT        NOT_19 (v97,v67);
   defparam NOT_19.inpsize = 0;
   defparam NOT_19.outsize = 0;

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

 /* EQ ((v63 :num -> num),(v100 :num -> num),(v96 :num -> bool)) */
 EQ        EQ_1 (v63,v100,v96);
   defparam EQ_1.in1size = 31;
   defparam EQ_1.in2size = 31;
   defparam EQ_1.outsize = 0;

 /* Dtype ((clk :num -> bool),(v96 :num -> bool),(v66 :num -> bool)) */
 Dtype      Dtype_12 (clk,v96,v66);
   defparam Dtype_12.size = 0;

 /* DtypeT ((clk :num -> bool),(v67 :num -> bool),(v104 :num -> bool)) */
 DtypeT        DtypeT_15 (clk,v67,v104);

 /* NOT ((v104 :num -> bool),(v103 :num -> bool)) */
 NOT        NOT_20 (v104,v103);
   defparam NOT_20.inpsize = 0;
   defparam NOT_20.outsize = 0;

 /* AND ((v103 :num -> bool),(v67 :num -> bool),(v102 :num -> bool)) */
 AND        AND_20 (v103,v67,v102);
   defparam AND_20.in1size = 0;
   defparam AND_20.in2size = 0;
   defparam AND_20.outsize = 0;

 /* AND ((v102 :num -> bool),(v66 :num -> bool),(v65 :num -> bool)) */
 AND        AND_21 (v102,v66,v65);
   defparam AND_21.in1size = 0;
   defparam AND_21.in2size = 0;
   defparam AND_21.outsize = 0;

 /* NOT ((v66 :num -> bool),(v101 :num -> bool)) */
 NOT        NOT_21 (v66,v101);
   defparam NOT_21.inpsize = 0;
   defparam NOT_21.outsize = 0;

 /* AND ((v101 :num -> bool),(v102 :num -> bool),(v64 :num -> bool)) */
 AND        AND_22 (v101,v102,v64);
   defparam AND_22.in1size = 0;
   defparam AND_22.in2size = 0;
   defparam AND_22.outsize = 0;

 /* DtypeT ((clk :num -> bool),(v65 :num -> bool),(v108 :num -> bool)) */
 DtypeT        DtypeT_16 (clk,v65,v108);

 /* NOT ((v108 :num -> bool),(v107 :num -> bool)) */
 NOT        NOT_22 (v108,v107);
   defparam NOT_22.inpsize = 0;
   defparam NOT_22.outsize = 0;

 /* AND ((v107 :num -> bool),(v65 :num -> bool),(v106 :num -> bool)) */
 AND        AND_23 (v107,v65,v106);
   defparam AND_23.in1size = 0;
   defparam AND_23.in2size = 0;
   defparam AND_23.outsize = 0;

 /* NOT ((v106 :num -> bool),(v60 :num -> bool)) */
 NOT        NOT_23 (v106,v60);
   defparam NOT_23.inpsize = 0;
   defparam NOT_23.outsize = 0;

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

 /* Dtype ((clk :num -> bool),(v105 :num -> num),(v58 :num -> num)) */
 Dtype      Dtype_13 (clk,v105,v58);
   defparam Dtype_13.size = 31;

 /* Dtype ((clk :num -> bool),(v69 :num -> num),(v59 :num -> num)) */
 Dtype      Dtype_14 (clk,v69,v59);
   defparam Dtype_14.size = 31;

 /* Dtype ((clk :num -> bool),(v68 :num -> num),(v43 :num -> num)) */
 Dtype      Dtype_15 (clk,v68,v43);
   defparam Dtype_15.size = 31;

 /* DtypeT ((clk :num -> bool),(v64 :num -> bool),(v113 :num -> bool)) */
 DtypeT        DtypeT_17 (clk,v64,v113);

 /* NOT ((v113 :num -> bool),(v112 :num -> bool)) */
 NOT        NOT_24 (v113,v112);
   defparam NOT_24.inpsize = 0;
   defparam NOT_24.outsize = 0;

 /* AND ((v112 :num -> bool),(v64 :num -> bool),(v111 :num -> bool)) */
 AND        AND_24 (v112,v64,v111);
   defparam AND_24.in1size = 0;
   defparam AND_24.in2size = 0;
   defparam AND_24.outsize = 0;

 /* NOT ((v111 :num -> bool),(v75 :num -> bool)) */
 NOT        NOT_25 (v111,v75);
   defparam NOT_25.inpsize = 0;
   defparam NOT_25.outsize = 0;

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

 /* SUB ((v70 :num -> num),(v114 :num -> num),(v110 :num -> num)) */
 SUB        SUB_1 (v70,v114,v110);
   defparam SUB_1.in1size = 31;
   defparam SUB_1.in2size = 31;
   defparam SUB_1.outsize = 31;

 /* ADD ((v69 :num -> num),(v68 :num -> num),(v109 :num -> num)) */
 ADD        ADD_0 (v69,v68,v109);
   defparam ADD_0.in1size = 31;
   defparam ADD_0.in2size = 31;
   defparam ADD_0.outsize = 31;

 /* Dtype ((clk :num -> bool),(v110 :num -> num),(v74 :num -> num)) */
 Dtype      Dtype_16 (clk,v110,v74);
   defparam Dtype_16.size = 31;

 /* Dtype ((clk :num -> bool),(v69 :num -> num),(v73 :num -> num)) */
 Dtype      Dtype_17 (clk,v69,v73);
   defparam Dtype_17.size = 31;

 /* Dtype ((clk :num -> bool),(v109 :num -> num),(v72 :num -> num)) */
 Dtype      Dtype_18 (clk,v109,v72);
   defparam Dtype_18.size = 31;

 /* Dtype ((clk :num -> bool),(v75 :num -> bool),(v116 :num -> bool)) */
 Dtype      Dtype_19 (clk,v75,v116);
   defparam Dtype_19.size = 0;

 /* AND ((v75 :num -> bool),(v116 :num -> bool),(v115 :num -> bool)) */
 AND        AND_25 (v75,v116,v115);
   defparam AND_25.in1size = 0;
   defparam AND_25.in2size = 0;
   defparam AND_25.outsize = 0;

 /* AND ((v60 :num -> bool),(v67 :num -> bool),(v117 :num -> bool)) */
 AND        AND_26 (v60,v67,v117);
   defparam AND_26.in1size = 0;
   defparam AND_26.in2size = 0;
   defparam AND_26.outsize = 0;

 /* AND ((v117 :num -> bool),(v115 :num -> bool),(v45 :num -> bool)) */
 AND        AND_27 (v117,v115,v45);
   defparam AND_27.in1size = 0;
   defparam AND_27.in2size = 0;
   defparam AND_27.outsize = 0;

 /* DtypeT ((clk :num -> bool),(v46 :num -> bool),(v120 :num -> bool)) */
 DtypeT        DtypeT_18 (clk,v46,v120);

 /* NOT ((v120 :num -> bool),(v119 :num -> bool)) */
 NOT        NOT_26 (v120,v119);
   defparam NOT_26.inpsize = 0;
   defparam NOT_26.outsize = 0;

 /* AND ((v119 :num -> bool),(v46 :num -> bool),(v118 :num -> bool)) */
 AND        AND_28 (v119,v46,v118);
   defparam AND_28.in1size = 0;
   defparam AND_28.in2size = 0;
   defparam AND_28.outsize = 0;

 /*
 MUX
  ((v118 :num -> bool),(v44 :num -> num),(v121 :num -> num),
   (v13 :num -> num))
 */
 MUX        MUX_10 (v118,v44,v121,v13);
   defparam MUX_10.size = 31;

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

 /* DtypeT ((clk :num -> bool),(v45 :num -> bool),(v124 :num -> bool)) */
 DtypeT        DtypeT_19 (clk,v45,v124);

 /* NOT ((v124 :num -> bool),(v123 :num -> bool)) */
 NOT        NOT_27 (v124,v123);
   defparam NOT_27.inpsize = 0;
   defparam NOT_27.outsize = 0;

 /* AND ((v123 :num -> bool),(v45 :num -> bool),(v122 :num -> bool)) */
 AND        AND_29 (v123,v45,v122);
   defparam AND_29.in1size = 0;
   defparam AND_29.in2size = 0;
   defparam AND_29.outsize = 0;

 /*
 MUX
  ((v122 :num -> bool),(v43 :num -> num),(v125 :num -> num),
   (v12 :num -> num))
 */
 MUX        MUX_11 (v122,v43,v125,v12);
   defparam MUX_11.size = 31;

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

 /* AND ((v46 :num -> bool),(v45 :num -> bool),(v14 :num -> bool)) */
 AND        AND_30 (v46,v45,v14);
   defparam AND_30.in1size = 0;
   defparam AND_30.in2size = 0;
   defparam AND_30.outsize = 0;

 /* Dtype ((clk :num -> bool),(v14 :num -> bool),(v127 :num -> bool)) */
 Dtype      Dtype_22 (clk,v14,v127);
   defparam Dtype_22.size = 0;

 /* AND ((v14 :num -> bool),(v127 :num -> bool),(v126 :num -> bool)) */
 AND        AND_31 (v14,v127,v126);
   defparam AND_31.in1size = 0;
   defparam AND_31.in2size = 0;
   defparam AND_31.outsize = 0;

 /* AND ((v2 :num -> bool),(v8 :num -> bool),(v128 :num -> bool)) */
 AND        AND_32 (v2,v8,v128);
   defparam AND_32.in1size = 0;
   defparam AND_32.in2size = 0;
   defparam AND_32.outsize = 0;

 /* AND ((v128 :num -> bool),(v126 :num -> bool),(done :num -> bool)) */
 AND        AND_33 (v128,v126,done);
   defparam AND_33.in1size = 0;
   defparam AND_33.in2size = 0;
   defparam AND_33.outsize = 0;

endmodule

Add a testbench to evaluate FACT 4.

// Clock
module Clock (clk);
 parameter period = 10; // default 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] inp;
 wire done;
 wire [31:0] out;

 initial
  begin
   $dumpfile("FACT.vcd");
   $dumpvars(1,clk,load,inp,done,out);
  end

 initial load = 0;

 always @(posedge clk) if (done)
                        begin
                         #1 load = 1;
                         #1 inp = 4;
                         forever @(posedge clk) if (done) $finish;
                        end

 /* Change time between edges */
 Clock      Clock_0 (clk);
   defparam Clock_0.period = 5;

 FACT    FACT (clk,load,inp,done,out);

endmodule

Simulate and view waveform:

If the value 4 is input on Main.inp when Main.load is asserted, then when Main.done is subsequently high, the value on Main.out is 24 (i.e. 4!).

 


Page maintained by Mike Gordon
Sun Apr 24 2005