MultIter (m,n,acc) = if m = 0 then (0,n,acc) else MultIter (m-1,n,n+acc)
|- 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
// 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
// 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
// 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
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.