156 lines
4.6 KiB
Coq
156 lines
4.6 KiB
Coq
|
/////////////////////////////////////
|
||
|
// //
|
||
|
// ERI summit demo-benchmark //
|
||
|
// pipelined_32b_adder_tb //
|
||
|
// by Aurelien //
|
||
|
// //
|
||
|
/////////////////////////////////////
|
||
|
|
||
|
`timescale 1 ns/ 1 ps
|
||
|
|
||
|
module pipelined_32b_adder_ERI_demo_tb();
|
||
|
reg clk;
|
||
|
reg[10:0] raddr;
|
||
|
reg[10:0] waddr;
|
||
|
reg ren;
|
||
|
reg wen;
|
||
|
reg[30:0] a;
|
||
|
reg[30:0] b;
|
||
|
wire[31:0] q_gfpga;
|
||
|
wire[31:0] q_bench;
|
||
|
reg[31:0] q_flag;
|
||
|
|
||
|
pipelined_32b_adder_top_formal_verification DUT(
|
||
|
.clk_fm (clk),
|
||
|
.raddr_0_fm (raddr[0]),
|
||
|
.raddr_1_fm (raddr[1]),
|
||
|
.raddr_2_fm (raddr[2]),
|
||
|
.raddr_3_fm (raddr[3]),
|
||
|
.raddr_4_fm (raddr[4]),
|
||
|
.raddr_5_fm (raddr[5]),
|
||
|
.raddr_6_fm (raddr[6]),
|
||
|
.raddr_7_fm (raddr[7]),
|
||
|
.raddr_8_fm (raddr[8]),
|
||
|
.raddr_9_fm (raddr[9]),
|
||
|
.raddr_10_fm (raddr[10]),
|
||
|
.waddr_0_fm (waddr[0]),
|
||
|
.waddr_1_fm (waddr[1]),
|
||
|
.waddr_2_fm (waddr[2]),
|
||
|
.waddr_3_fm (waddr[3]),
|
||
|
.waddr_4_fm (waddr[4]),
|
||
|
.waddr_5_fm (waddr[5]),
|
||
|
.waddr_6_fm (waddr[6]),
|
||
|
.waddr_7_fm (waddr[7]),
|
||
|
.waddr_8_fm (waddr[8]),
|
||
|
.waddr_9_fm (waddr[9]),
|
||
|
.waddr_10_fm (waddr[10]),
|
||
|
.ren_fm (ren),
|
||
|
.wen_fm (wen),
|
||
|
.a_0_fm (a[0]),
|
||
|
.a_1_fm (a[1]),
|
||
|
.a_2_fm (a[2]),
|
||
|
.a_3_fm (a[3]),
|
||
|
.a_4_fm (a[4]),
|
||
|
.a_5_fm (a[5]),
|
||
|
.a_6_fm (a[6]),
|
||
|
.a_7_fm (a[7]),
|
||
|
.a_8_fm (a[8]),
|
||
|
.a_9_fm (a[9]),
|
||
|
.a_10_fm (a[10]),
|
||
|
.a_11_fm (a[11]),
|
||
|
.a_12_fm (a[12]),
|
||
|
.a_13_fm (a[13]),
|
||
|
.a_14_fm (a[14]),
|
||
|
.a_15_fm (a[15]),
|
||
|
.a_16_fm (a[16]),
|
||
|
.a_17_fm (a[17]),
|
||
|
.a_18_fm (a[18]),
|
||
|
.a_19_fm (a[19]),
|
||
|
.a_20_fm (a[20]),
|
||
|
.a_21_fm (a[21]),
|
||
|
.a_22_fm (a[22]),
|
||
|
.a_23_fm (a[23]),
|
||
|
.a_24_fm (a[24]),
|
||
|
.a_25_fm (a[25]),
|
||
|
.a_26_fm (a[26]),
|
||
|
.a_27_fm (a[27]),
|
||
|
.a_28_fm (a[28]),
|
||
|
.a_29_fm (a[29]),
|
||
|
.a_30_fm (a[30]),
|
||
|
.b_0_fm (b[0]),
|
||
|
.b_1_fm (b[1]),
|
||
|
.b_2_fm (b[2]),
|
||
|
.b_3_fm (b[3]),
|
||
|
.b_4_fm (b[4]),
|
||
|
.b_5_fm (b[5]),
|
||
|
.b_6_fm (b[6]),
|
||
|
.b_7_fm (b[7]),
|
||
|
.b_8_fm (b[8]),
|
||
|
.b_9_fm (b[9]),
|
||
|
.b_10_fm (b[10]),
|
||
|
.b_11_fm (b[11]),
|
||
|
.b_12_fm (b[12]),
|
||
|
.b_13_fm (b[13]),
|
||
|
.b_14_fm (b[14]),
|
||
|
.b_15_fm (b[15]),
|
||
|
.b_16_fm (b[16]),
|
||
|
.b_17_fm (b[17]),
|
||
|
.b_18_fm (b[18]),
|
||
|
.b_19_fm (b[19]),
|
||
|
.b_20_fm (b[20]),
|
||
|
.b_21_fm (b[21]),
|
||
|
.b_22_fm (b[22]),
|
||
|
.b_23_fm (b[23]),
|
||
|
.b_24_fm (b[24]),
|
||
|
.b_25_fm (b[25]),
|
||
|
.b_26_fm (b[26]),
|
||
|
.b_27_fm (b[27]),
|
||
|
.b_28_fm (b[28]),
|
||
|
.b_29_fm (b[29]),
|
||
|
.b_30_fm (b[30]),
|
||
|
.out_q_0_fm (q_gfpga[0]),
|
||
|
.out_q_1_fm (q_gfpga[1]),
|
||
|
.out_q_2_fm (q_gfpga[2]),
|
||
|
.out_q_3_fm (q_gfpga[3]),
|
||
|
.out_q_4_fm (q_gfpga[4]),
|
||
|
.out_q_5_fm (q_gfpga[5]),
|
||
|
.out_q_6_fm (q_gfpga[6]),
|
||
|
.out_q_7_fm (q_gfpga[7]),
|
||
|
.out_q_8_fm (q_gfpga[8]),
|
||
|
.out_q_9_fm (q_gfpga[9]),
|
||
|
.out_q_10_fm (q_gfpga[10]),
|
||
|
.out_q_11_fm (q_gfpga[11]),
|
||
|
.out_q_12_fm (q_gfpga[12]),
|
||
|
.out_q_13_fm (q_gfpga[13]),
|
||
|
.out_q_14_fm (q_gfpga[14]),
|
||
|
.out_q_15_fm (q_gfpga[15]),
|
||
|
.out_q_16_fm (q_gfpga[16]),
|
||
|
.out_q_17_fm (q_gfpga[17]),
|
||
|
.out_q_18_fm (q_gfpga[18]),
|
||
|
.out_q_19_fm (q_gfpga[19]),
|
||
|
.out_q_20_fm (q_gfpga[20]),
|
||
|
.out_q_21_fm (q_gfpga[21]),
|
||
|
.out_q_22_fm (q_gfpga[22]),
|
||
|
.out_q_23_fm (q_gfpga[23]),
|
||
|
.out_q_24_fm (q_gfpga[24]),
|
||
|
.out_q_25_fm (q_gfpga[25]),
|
||
|
.out_q_26_fm (q_gfpga[26]),
|
||
|
.out_q_27_fm (q_gfpga[27]),
|
||
|
.out_q_28_fm (q_gfpga[28]),
|
||
|
.out_q_29_fm (q_gfpga[29]),
|
||
|
.out_q_30_fm (q_gfpga[30]),
|
||
|
.out_q_31_fm (q_gfpga[31])
|
||
|
);
|
||
|
|
||
|
pipelined_32b_adder ref0(
|
||
|
.clk (clk),
|
||
|
.raddr (raddr),
|
||
|
.waddr (waddr),
|
||
|
.ren (ren),
|
||
|
.wen (wen),
|
||
|
.a (a),
|
||
|
.b (b),
|
||
|
.q (q_bench)
|
||
|
);
|
||
|
|
||
|
endmodule : pipelined_32b_adder_ERI_demo_tb
|