| //------------------------------------------- |
| // FPGA Synthesizable Verilog Netlist |
| // Description: FPGA Verilog Testbench for Formal Top-level netlist of Design: top |
| // Author: Xifan TANG |
| // Organization: University of Utah |
| // Date: Tue Nov 24 18:04:19 2020 |
| //------------------------------------------- |
| //----- Time scale ----- |
| `timescale 1ns / 1ps |
| |
| module top_top_formal_verification_random_tb; |
| // ----- Default clock port is added here since benchmark does not contain one ------- |
| reg [0:0] clk; |
| |
| // ----- Shared inputs ------- |
| reg [0:0] a; |
| reg [0:0] b; |
| |
| // ----- FPGA fabric outputs ------- |
| wire [0:0] out:c_gfpga; |
| |
| `ifdef AUTOCHECKED_SIMULATION |
| |
| // ----- Benchmark outputs ------- |
| wire [0:0] out:c_bench; |
| |
| // ----- Output vectors checking flags ------- |
| reg [0:0] out:c_flag; |
| |
| `endif |
| |
| // ----- Error counter ------- |
| integer nb_error= 0; |
| |
| // ----- FPGA fabric instanciation ------- |
| top_top_formal_verification FPGA_DUT( |
| .a_fm(a), |
| .b_fm(b), |
| .out:c_fm(out:c_gfpga) ); |
| // ----- End FPGA Fabric Instanication ------- |
| |
| `ifdef AUTOCHECKED_SIMULATION |
| // ----- Reference Benchmark Instanication ------- |
| top REF_DUT( |
| .a(a), |
| .b(b), |
| .c(out:c_bench) ); |
| // ----- End reference Benchmark Instanication ------- |
| |
| `endif |
| |
| // ----- Clock Initialization ------- |
| initial begin |
| clk[0] <= 1'b0; |
| while(1) begin |
| #0.4159859701 |
| clk[0] <= !clk[0]; |
| end |
| end |
| |
| // ----- Input Initialization ------- |
| initial begin |
| a <= 1'b0; |
| b <= 1'b0; |
| |
| out:c_flag[0] <= 1'b0; |
| end |
| |
| // ----- Input Stimulus ------- |
| always@(negedge clk[0]) begin |
| a <= $random; |
| b <= $random; |
| end |
| |
| `ifdef AUTOCHECKED_SIMULATION |
| // ----- Begin checking output vectors ------- |
| // ----- Skip the first falling edge of clock, it is for initialization ------- |
| reg [0:0] sim_start; |
| |
| always@(negedge clk[0]) begin |
| if (1'b1 == sim_start[0]) begin |
| sim_start[0] <= ~sim_start[0]; |
| end else begin |
| if(!(out:c_gfpga === out:c_bench) && !(out:c_bench === 1'bx)) begin |
| out:c_flag <= 1'b1; |
| end else begin |
| out:c_flag<= 1'b0; |
| end |
| end |
| end |
| |
| always@(posedge out:c_flag) begin |
| if(out:c_flag) begin |
| nb_error = nb_error + 1; |
| $display("Mismatch on out:c_gfpga at time = %t", $realtime); |
| end |
| end |
| |
| `endif |
| |
| `ifdef ICARUS_SIMULATOR |
| // ----- Begin Icarus requirement ------- |
| initial begin |
| $dumpfile("top_formal.vcd"); |
| $dumpvars(1, top_top_formal_verification_random_tb); |
| end |
| `endif |
| // ----- END Icarus requirement ------- |
| |
| initial begin |
| sim_start[0] <= 1'b1; |
| $timeformat(-9, 2, "ns", 20); |
| $display("Simulation start"); |
| // ----- Can be changed by the user for his/her need ------- |
| #332 |
| if(nb_error == 0) begin |
| $display("Simulation Succeed"); |
| end else begin |
| $display("Simulation Failed with %d error(s)", nb_error); |
| end |
| $finish; |
| end |
| |
| endmodule |
| // ----- END Verilog module for top_top_formal_verification_random_tb ----- |
| |