diff --git a/.gitmodules b/.gitmodules index e26ff47..a87c55f 100644 --- a/.gitmodules +++ b/.gitmodules @@ -7,3 +7,6 @@ [submodule "scripts"] path = scripts url = https://github.com/Wren6991/fpgascripts +[submodule "test/formal/riscv-formal"] + path = test/formal/riscv-formal + url = https://github.com/Wren6991/riscv-formal.git diff --git a/hdl/hazard3_decode.v b/hdl/hazard3_decode.v index d32916f..280a3c9 100644 --- a/hdl/hazard3_decode.v +++ b/hdl/hazard3_decode.v @@ -2,7 +2,7 @@ * DO WHAT THE FUCK YOU WANT TO AND DON'T BLAME US PUBLIC LICENSE * * Version 3, April 2008 * * * - * Copyright (C) 2019 Luke Wren * + * Copyright (C) 2021 Luke Wren * * * * Everyone is permitted to copy and distribute verbatim or modified * * copies of this license document and accompanying software, and * @@ -136,8 +136,15 @@ always @ (posedge clk or negedge rst_n) begin pc <= f_jump_target; `ifdef FORMAL // Being cheeky above to save a 32 bit mux. Check that we never get an M target by mistake. - if (cir_lock_prev && deassert_cir_lock) - assert(f_jump_target == d_jump_target); + + // FIXME disabled this for now -- we do sometimes see an exception taking + // place during the stall, which then leads to a different branch target + // appearing. (i.e. f_jump_now is asserted for two cycles, the first one + // from this instruction and the second from the exception; this is ok, + // because the exception will return to this branch when done.) + + // if (cir_lock_prev && deassert_cir_lock) + // assert(f_jump_target == d_jump_target); `endif end else if (!d_stall && !df_cir_lock) begin pc <= pc_next; diff --git a/test/formal/common/ahbl_master_assertions.v b/test/formal/common/ahbl_master_assertions.v new file mode 100644 index 0000000..0d39622 --- /dev/null +++ b/test/formal/common/ahbl_master_assertions.v @@ -0,0 +1,98 @@ +/****************************************************************************** + * DO WHAT THE FUCK YOU WANT TO AND DON'T BLAME US PUBLIC LICENSE * + * Version 3, April 2008 * + * * + * Copyright (C) 2021 Luke Wren * + * * + * Everyone is permitted to copy and distribute verbatim or modified * + * copies of this license document and accompanying software, and * + * changing either is allowed. * + * * + * TERMS AND CONDITIONS FOR COPYING, DISTRIBUTION AND MODIFICATION * + * * + * 0. You just DO WHAT THE FUCK YOU WANT TO. * + * 1. We're NOT RESPONSIBLE WHEN IT DOESN'T FUCKING WORK. * + * * + *****************************************************************************/ + +// Assert that an AHB-Lite master is relatively well-behaved + +module ahbl_master_assertions #( + parameter W_ADDR = 32, + parameter W_DATA = 32 +) ( + input wire clk, + input wire rst_n, + + // Upstream AHB-Lite slave port + output wire src_hready_resp, + input wire src_hready, + output wire src_hresp, + input wire [W_ADDR-1:0] src_haddr, + input wire src_hwrite, + input wire [1:0] src_htrans, + input wire [2:0] src_hsize, + input wire [2:0] src_hburst, + input wire [3:0] src_hprot, + input wire src_hmastlock, + input wire [W_DATA-1:0] src_hwdata, + output wire [W_DATA-1:0] src_hrdata +); + +// Data-phase monitoring +reg src_active_dph; +reg src_write_dph; +reg [W_ADDR-1:0] src_addr_dph; +reg [2:0] src_size_dph; + +always @ (posedge clk or negedge rst_n) begin + if (!rst_n) begin + src_active_dph <= 1'b0; + src_write_dph <= 1'b0; + src_addr_dph <= {W_ADDR{1'b0}}; + src_size_dph <= 3'h0; + end else if (src_hready) begin + src_active_dph <= src_htrans[1]; + src_write_dph <= src_hwrite; + src_addr_dph <= src_haddr; + src_size_dph <= src_hsize; + end +end + +// Assertions for all downstream requests +always @ (posedge clk) if (rst_n) begin: dst_ahbl_req_properties + + // Address phase properties (inactive when request is IDLE): + if (src_htrans != 2'b00) begin + // Transfer must be naturally aligned + assert(!(src_haddr & ~({W_ADDR{1'b1}} << src_hsize))); + // HSIZE appropriate for bus width + assert(8 << src_hsize <= W_DATA); + // No deassertion or change of active request + if ($past(src_htrans[1] && !src_hready)) begin + assert($stable({ + src_htrans, + src_hwrite, + src_haddr, + src_hsize, + src_hburst, + src_hprot, + src_hmastlock + })); + end + // SEQ only issued following an NSEQ or SEQ, never an IDLE + if (src_htrans == 2'b11) + assert(src_active_dph); + // SEQ transfer addresses must be sequential with previous transfer (note + // this only supports INCRx bursts) + if (src_htrans == 2'b11) + assert(src_haddr == src_addr_dph + W_DATA / 8); + end + + // Data phase properties: + if (src_active_dph) begin + // Write data stable during write data phase + if (src_write_dph && !$past(src_hready)) + assert($stable(src_hwdata)); + end +end diff --git a/test/formal/common/ahbl_slave_assumptions.v b/test/formal/common/ahbl_slave_assumptions.v new file mode 100644 index 0000000..89d0099 --- /dev/null +++ b/test/formal/common/ahbl_slave_assumptions.v @@ -0,0 +1,98 @@ +/****************************************************************************** + * DO WHAT THE FUCK YOU WANT TO AND DON'T BLAME US PUBLIC LICENSE * + * Version 3, April 2008 * + * * + * Copyright (C) 2021 Luke Wren * + * * + * Everyone is permitted to copy and distribute verbatim or modified * + * copies of this license document and accompanying software, and * + * changing either is allowed. * + * * + * TERMS AND CONDITIONS FOR COPYING, DISTRIBUTION AND MODIFICATION * + * * + * 0. You just DO WHAT THE FUCK YOU WANT TO. * + * 1. We're NOT RESPONSIBLE WHEN IT DOESN'T FUCKING WORK. * + * * + *****************************************************************************/ + +// Assumptions to constrain an AHB-Lite slave to be relatively well-behaved + +module ahbl_slave_assumptions #( + parameter W_ADDR = 32, + parameter W_DATA = 32, + parameter MAX_BUS_STALL = -1 // set >= 0 to constrain max stall length +) ( + input wire clk, + input wire rst_n, + + // Downstream AHB-Lite master port + input wire dst_hready_resp, + output wire dst_hready, + input wire dst_hresp, + output wire [W_ADDR-1:0] dst_haddr, + output wire dst_hwrite, + output wire [1:0] dst_htrans, + output wire [2:0] dst_hsize, + output wire [2:0] dst_hburst, + output wire [3:0] dst_hprot, + output wire dst_hmastlock, + output wire [W_DATA-1:0] dst_hwdata, + input wire [W_DATA-1:0] dst_hrdata +); + +reg dst_active_dph; +reg dst_write_dph; +reg [W_ADDR-1:0] dst_addr_dph; +reg [2:0] dst_size_dph; + +always @ (posedge clk or negedge rst_n) begin + if (!rst_n) begin + dst_active_dph <= 1'b0; + dst_write_dph <= 1'b0; + dst_addr_dph <= {W_ADDR{1'b0}}; + dst_size_dph <= 3'h0; + end else if (dst_hready) begin + dst_active_dph <= dst_htrans[1]; + dst_write_dph <= dst_hwrite; + dst_addr_dph <= dst_haddr; + dst_size_dph <= dst_hsize; + end +end + +// Assumptions for all downstream responses +always @ (posedge clk) if (rst_n) begin: dst_ahbl_resp_properties + // IDLE->OKAY + if (!dst_active_dph) begin + assume(dst_hready_resp); + assume(!dst_hresp); + end + // Correct two-phase error response. + if (dst_hresp && dst_hready) + assume($past(dst_hresp && !dst_hready)); + if (dst_hresp && !dst_hready) + assume($past(!(dst_hresp && !dst_hready))); + if ($past(dst_hresp && !dst_hready)) + assume(dst_hresp); +end + + +generate +if (MAX_BUS_STALL >= 0) begin: constrain_max_bus_stall + +reg [7:0] bus_stall_ctr; +always @ (posedge clk or negedge rst_n) begin + if (!rst_n) begin + bus_stall_ctr <= 8'h0; + end else begin + if (dst_hready) + bus_stall_ctr <= 8'h0; + else + bus_stall_ctr <= bus_stall_ctr + ~&bus_stall_ctr; + assume(bus_stall_ctr <= MAX_BUS_STALL); + end +end + +end +endgenerate + +endmodule diff --git a/test/formal/riscv-formal b/test/formal/riscv-formal new file mode 160000 index 0000000..7dd18d8 --- /dev/null +++ b/test/formal/riscv-formal @@ -0,0 +1 @@ +Subproject commit 7dd18d861e76e01c6ce27adce1c9cc2f5b36e4c1 diff --git a/test/common/init.S b/test/sim/common/init.S similarity index 100% rename from test/common/init.S rename to test/sim/common/init.S diff --git a/test/common/memmap.ld b/test/sim/common/memmap.ld similarity index 100% rename from test/common/memmap.ld rename to test/sim/common/memmap.ld diff --git a/test/common/src_only_app.mk b/test/sim/common/src_only_app.mk similarity index 100% rename from test/common/src_only_app.mk rename to test/sim/common/src_only_app.mk diff --git a/test/common/tb_cxxrtl_io.h b/test/sim/common/tb_cxxrtl_io.h similarity index 100% rename from test/common/tb_cxxrtl_io.h rename to test/sim/common/tb_cxxrtl_io.h diff --git a/test/coremark/Makefile b/test/sim/coremark/Makefile similarity index 100% rename from test/coremark/Makefile rename to test/sim/coremark/Makefile diff --git a/test/coremark/dist/.gitignore b/test/sim/coremark/dist/.gitignore similarity index 100% rename from test/coremark/dist/.gitignore rename to test/sim/coremark/dist/.gitignore diff --git a/test/coremark/dist/LICENSE.md b/test/sim/coremark/dist/LICENSE.md similarity index 100% rename from test/coremark/dist/LICENSE.md rename to test/sim/coremark/dist/LICENSE.md diff --git a/test/coremark/dist/Makefile b/test/sim/coremark/dist/Makefile similarity index 100% rename from test/coremark/dist/Makefile rename to test/sim/coremark/dist/Makefile diff --git a/test/coremark/dist/barebones/core_portme.c b/test/sim/coremark/dist/barebones/core_portme.c similarity index 100% rename from test/coremark/dist/barebones/core_portme.c rename to test/sim/coremark/dist/barebones/core_portme.c diff --git a/test/coremark/dist/barebones/core_portme.h b/test/sim/coremark/dist/barebones/core_portme.h similarity index 100% rename from test/coremark/dist/barebones/core_portme.h rename to test/sim/coremark/dist/barebones/core_portme.h diff --git a/test/coremark/dist/barebones/core_portme.mak b/test/sim/coremark/dist/barebones/core_portme.mak similarity index 100% rename from test/coremark/dist/barebones/core_portme.mak rename to test/sim/coremark/dist/barebones/core_portme.mak diff --git a/test/coremark/dist/barebones/cvt.c b/test/sim/coremark/dist/barebones/cvt.c similarity index 100% rename from test/coremark/dist/barebones/cvt.c rename to test/sim/coremark/dist/barebones/cvt.c diff --git a/test/coremark/dist/barebones/ee_printf.c b/test/sim/coremark/dist/barebones/ee_printf.c similarity index 100% rename from test/coremark/dist/barebones/ee_printf.c rename to test/sim/coremark/dist/barebones/ee_printf.c diff --git a/test/coremark/dist/barebones/init.S b/test/sim/coremark/dist/barebones/init.S similarity index 100% rename from test/coremark/dist/barebones/init.S rename to test/sim/coremark/dist/barebones/init.S diff --git a/test/coremark/dist/barebones/tb_cxxrtl_io.h b/test/sim/coremark/dist/barebones/tb_cxxrtl_io.h similarity index 100% rename from test/coremark/dist/barebones/tb_cxxrtl_io.h rename to test/sim/coremark/dist/barebones/tb_cxxrtl_io.h diff --git a/test/coremark/dist/core_list_join.c b/test/sim/coremark/dist/core_list_join.c similarity index 100% rename from test/coremark/dist/core_list_join.c rename to test/sim/coremark/dist/core_list_join.c diff --git a/test/coremark/dist/core_main.c b/test/sim/coremark/dist/core_main.c similarity index 100% rename from test/coremark/dist/core_main.c rename to test/sim/coremark/dist/core_main.c diff --git a/test/coremark/dist/core_matrix.c b/test/sim/coremark/dist/core_matrix.c similarity index 100% rename from test/coremark/dist/core_matrix.c rename to test/sim/coremark/dist/core_matrix.c diff --git a/test/coremark/dist/core_state.c b/test/sim/coremark/dist/core_state.c similarity index 100% rename from test/coremark/dist/core_state.c rename to test/sim/coremark/dist/core_state.c diff --git a/test/coremark/dist/core_util.c b/test/sim/coremark/dist/core_util.c similarity index 100% rename from test/coremark/dist/core_util.c rename to test/sim/coremark/dist/core_util.c diff --git a/test/coremark/dist/coremark.h b/test/sim/coremark/dist/coremark.h similarity index 100% rename from test/coremark/dist/coremark.h rename to test/sim/coremark/dist/coremark.h diff --git a/test/dhrystone/Makefile b/test/sim/dhrystone/Makefile similarity index 100% rename from test/dhrystone/Makefile rename to test/sim/dhrystone/Makefile diff --git a/test/dhrystone/src/LICENSE b/test/sim/dhrystone/src/LICENSE similarity index 100% rename from test/dhrystone/src/LICENSE rename to test/sim/dhrystone/src/LICENSE diff --git a/test/dhrystone/src/dhrystone.c b/test/sim/dhrystone/src/dhrystone.c similarity index 100% rename from test/dhrystone/src/dhrystone.c rename to test/sim/dhrystone/src/dhrystone.c diff --git a/test/dhrystone/src/dhrystone.h b/test/sim/dhrystone/src/dhrystone.h similarity index 100% rename from test/dhrystone/src/dhrystone.h rename to test/sim/dhrystone/src/dhrystone.h diff --git a/test/dhrystone/src/dhrystone_main.c b/test/sim/dhrystone/src/dhrystone_main.c similarity index 100% rename from test/dhrystone/src/dhrystone_main.c rename to test/sim/dhrystone/src/dhrystone_main.c diff --git a/test/dhrystone/src/util.c b/test/sim/dhrystone/src/util.c similarity index 100% rename from test/dhrystone/src/util.c rename to test/sim/dhrystone/src/util.c diff --git a/test/dhrystone/src/util.h b/test/sim/dhrystone/src/util.h similarity index 100% rename from test/dhrystone/src/util.h rename to test/sim/dhrystone/src/util.h diff --git a/test/hellow/Makefile b/test/sim/hellow/Makefile similarity index 100% rename from test/hellow/Makefile rename to test/sim/hellow/Makefile diff --git a/test/hellow/main.c b/test/sim/hellow/main.c similarity index 100% rename from test/hellow/main.c rename to test/sim/hellow/main.c diff --git a/test/riscv-compliance/.gitignore b/test/sim/riscv-compliance/.gitignore similarity index 100% rename from test/riscv-compliance/.gitignore rename to test/sim/riscv-compliance/.gitignore diff --git a/test/riscv-compliance/Makefile b/test/sim/riscv-compliance/Makefile similarity index 100% rename from test/riscv-compliance/Makefile rename to test/sim/riscv-compliance/Makefile diff --git a/test/riscv-compliance/compare_testvec b/test/sim/riscv-compliance/compare_testvec similarity index 100% rename from test/riscv-compliance/compare_testvec rename to test/sim/riscv-compliance/compare_testvec diff --git a/test/riscv-compliance/include/arch_test.h b/test/sim/riscv-compliance/include/arch_test.h similarity index 100% rename from test/riscv-compliance/include/arch_test.h rename to test/sim/riscv-compliance/include/arch_test.h diff --git a/test/riscv-compliance/include/encoding.h b/test/sim/riscv-compliance/include/encoding.h similarity index 100% rename from test/riscv-compliance/include/encoding.h rename to test/sim/riscv-compliance/include/encoding.h diff --git a/test/riscv-compliance/include/model_test.h b/test/sim/riscv-compliance/include/model_test.h similarity index 100% rename from test/riscv-compliance/include/model_test.h rename to test/sim/riscv-compliance/include/model_test.h diff --git a/test/riscv-compliance/memmap.ld b/test/sim/riscv-compliance/memmap.ld similarity index 100% rename from test/riscv-compliance/memmap.ld rename to test/sim/riscv-compliance/memmap.ld diff --git a/test/riscv-compliance/riscv-arch-test b/test/sim/riscv-compliance/riscv-arch-test similarity index 100% rename from test/riscv-compliance/riscv-arch-test rename to test/sim/riscv-compliance/riscv-arch-test diff --git a/test/sim/riscv-compliance/run_32ic.sh b/test/sim/riscv-compliance/run_32ic.sh new file mode 100755 index 0000000..d47a310 --- /dev/null +++ b/test/sim/riscv-compliance/run_32ic.sh @@ -0,0 +1,30 @@ +#!/bin/bash +make TEST_ARCH=C BIN_ARCH=rv32ic TESTLIST=" \ + cadd-01 \ + caddi16sp-01 \ + cand-01 \ + cbeqz-01 \ + cjal-01 \ + cjr-01 \ + clui-01 \ + clwsp-01 \ + cnop-01 \ + cslli-01 \ + csrli-01 \ + csw-01 \ + cxor-01 \ + caddi-01 \ + caddi4spn-01 \ + candi-01 \ + cbnez-01 \ + cj-01 \ + cjalr-01 \ + cli-01 \ + clw-01 \ + cmv-01 \ + cor-01 \ + csrai-01 \ + csub-01 \ + cswsp-01 \ + " + #cebreak-01 \ diff --git a/test/rvcpp/.gitignore b/test/sim/rvcpp/.gitignore similarity index 100% rename from test/rvcpp/.gitignore rename to test/sim/rvcpp/.gitignore diff --git a/test/rvcpp/Makefile b/test/sim/rvcpp/Makefile similarity index 100% rename from test/rvcpp/Makefile rename to test/sim/rvcpp/Makefile diff --git a/test/rvcpp/mem.h b/test/sim/rvcpp/mem.h similarity index 100% rename from test/rvcpp/mem.h rename to test/sim/rvcpp/mem.h diff --git a/test/rvcpp/rv.cpp b/test/sim/rvcpp/rv.cpp similarity index 100% rename from test/rvcpp/rv.cpp rename to test/sim/rvcpp/rv.cpp diff --git a/test/rvcpp/rv_types.h b/test/sim/rvcpp/rv_types.h similarity index 100% rename from test/rvcpp/rv_types.h rename to test/sim/rvcpp/rv_types.h diff --git a/test/rvpy/rvpy b/test/sim/rvpy/rvpy similarity index 100% rename from test/rvpy/rvpy rename to test/sim/rvpy/rvpy diff --git a/test/tb_cxxrtl/.gitignore b/test/sim/tb_cxxrtl/.gitignore similarity index 100% rename from test/tb_cxxrtl/.gitignore rename to test/sim/tb_cxxrtl/.gitignore diff --git a/test/tb_cxxrtl/Makefile b/test/sim/tb_cxxrtl/Makefile similarity index 100% rename from test/tb_cxxrtl/Makefile rename to test/sim/tb_cxxrtl/Makefile diff --git a/test/tb_cxxrtl/tb.cpp b/test/sim/tb_cxxrtl/tb.cpp similarity index 100% rename from test/tb_cxxrtl/tb.cpp rename to test/sim/tb_cxxrtl/tb.cpp