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))
|- 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)
// 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
// 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
// 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
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!).