diff --git a/.github/workflows/Dockerfile b/.github/workflows/Dockerfile index a72fffa1..bda25f85 100644 --- a/.github/workflows/Dockerfile +++ b/.github/workflows/Dockerfile @@ -14,15 +14,13 @@ # FROM ubuntu:18.04 RUN apt-get update && apt-get -y install \ - build-essential \ - python3 python3-pip -RUN apt-get -y install git + build-essential python3 python3-pip xz-utils git iverilog \ + flex libelf-dev RUN pip3 install setuptools wheel RUN pip3 install fusesoc RUN apt-get -y install curl -RUN apt-get -y install iverilog libelf-dev RUN groupadd -g 999 runner && \ useradd -m -r -u 999 -g runner runner diff --git a/.github/workflows/ci.yml b/.github/workflows/ci.yml index 15cb03b2..9e657909 100644 --- a/.github/workflows/ci.yml +++ b/.github/workflows/ci.yml @@ -34,7 +34,8 @@ jobs: # Install OS and Python Tools - name: Install Tools run: | - sudo apt-get install build-essential python3 xz-utils git iverilog libelf-dev + sudo apt-get install build-essential python3 xz-utils git iverilog \ + libfl2 libelf-dev pip3 install setuptools wheel pip3 install fusesoc export PATH=$PATH:$HOME/.local/bin @@ -47,9 +48,8 @@ jobs: mkdir -p /tmp/tools/lib cd /tmp/tools curl --remote-name --location \ - https://github.com/stffrdhrn/gcc/releases/download/or1k-10.0.0-20190723/or1k-elf-10.0.0-20190723.tar.xz - tar xC /tmp/tools -f or1k-elf-10.0.0-20190723.tar.xz - ln -s /usr/lib/x86_64-linux-gnu/libmpfr.so.6 /tmp/tools/lib/libmpfr.so.4 + https://github.com/openrisc/or1k-gcc/releases/download/or1k-12.0.1-20220210-20220304/or1k-elf-12.0.1-20220210-20220304.tar.xz + tar xC /tmp/tools -f or1k-elf-12.0.1-20220210-20220304.tar.xz export PATH=$PATH:/tmp/tools/or1k-elf/bin/ or1k-elf-gcc --version @@ -59,7 +59,7 @@ jobs: export PATH=$PATH:/tmp/tools/or1k-elf/bin:$HOME/.local/bin mkdir -p /tmp/tools cd /tmp/tools - git clone --depth 1 https://github.com/openrisc/or1k-tests.git -b v1.0.4 + git clone --depth 1 https://github.com/openrisc/or1k-tests.git -b v1.0.5 cd or1k-tests/native make -j8 fusesoc library add mor1kx-generic https://github.com/openrisc/mor1kx-generic.git @@ -77,7 +77,8 @@ jobs: export PIPELINE=CAPPUCCINO export TARGET=mor1kx_tb export TARGET_ARGS="--tool=icarus" - export CORE_ARGS="--pipeline=$PIPELINE $EXTRA_CORE_ARGS" + export CORE_ARGS="--pipeline=$PIPELINE --vcd --trace_enable $EXTRA_CORE_ARGS" + export ARTIFACT_PATH="build/mor1kx-generic_*/mor1kx_tb-icarus" cd /tmp/tools/or1k-tests/native ./runtests.sh result=$? @@ -86,6 +87,13 @@ jobs: fi exit $result + # Upload test results + - uses: actions/upload-artifact@v2 + if: failure() + with: + name: runtest-results + path: /tmp/tools/or1k-tests/native/artifacts/**/* + strategy: matrix: env: @@ -113,6 +121,7 @@ jobs: libreadline-dev gawk tcl-dev libffi-dev git graphviz xdot \ pkg-config python python3 libboost-system-dev \ libboost-python-dev libboost-filesystem-dev zlib1g-dev + pip3 install dataclasses - name: Install clang run: | diff --git a/bench/formal/.gitignore b/bench/formal/.gitignore index 20dd2dc4..33ab0df4 100644 --- a/bench/formal/.gitignore +++ b/bench/formal/.gitignore @@ -1 +1 @@ -mor1kx_*/ +mor1kx*/ diff --git a/bench/formal/Makefile b/bench/formal/Makefile index 26f912c1..692b1f3c 100644 --- a/bench/formal/Makefile +++ b/bench/formal/Makefile @@ -35,7 +35,7 @@ TESTS := mor1kx_cache_lru \ all: $(TESTS) clean: - rm -rf $(TESTS) + rm -rf mor1kx*/ .PHONY: all clean $(TESTS) diff --git a/bench/formal/mor1kx.gtkw b/bench/formal/mor1kx.gtkw new file mode 100644 index 00000000..d8d2deed --- /dev/null +++ b/bench/formal/mor1kx.gtkw @@ -0,0 +1,51 @@ +[*] +[*] GTKWave Analyzer v3.3.108 (w)1999-2020 BSI +[*] Sat Apr 16 09:30:26 2022 +[*] +[dumpfile] "/home/shorne/work/openrisc/local-cores/mor1kx/bench/formal/mor1kx/engine_0/trace_induct.vcd" +[dumpfile_mtime] "Sat Apr 16 09:19:48 2022" +[dumpfile_size] 313480 +[savefile] "/home/shorne/work/openrisc/local-cores/mor1kx/bench/formal/mor1kx.gtkw" +[timestart] 0 +[size] 1000 600 +[pos] -1 -1 +*-4.914850 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 +[treeopen] mor1kx. +[treeopen] mor1kx.mor1kx_cpu. +[treeopen] mor1kx.mor1kx_cpu.cappuccino. +[treeopen] mor1kx.mor1kx_cpu.cappuccino.mor1kx_cpu. +[treeopen] mor1kx.mor1kx_cpu.cappuccino.mor1kx_cpu.mor1kx_lsu_cappuccino. +[treeopen] mor1kx.mor1kx_cpu.cappuccino.mor1kx_cpu.mor1kx_lsu_cappuccino.dcache_gen. +[sst_width] 281 +[signals_width] 142 +[sst_expanded] 1 +[sst_vpaned_height] 295 +@28 +smt_clock +@420 +smt_step +@200 +-LSU +@28 +mor1kx.mor1kx_cpu.cappuccino.mor1kx_cpu.mor1kx_lsu_cappuccino.dc_enable_i +@29 +mor1kx.mor1kx_cpu.cappuccino.mor1kx_cpu.mor1kx_lsu_cappuccino.dmmu_enable_i +@28 +mor1kx.mor1kx_cpu.cappuccino.mor1kx_cpu.mor1kx_lsu_cappuccino.dbus_err_i +mor1kx.mor1kx_cpu.cappuccino.mor1kx_cpu.mor1kx_lsu_cappuccino.dc_enabled +mor1kx.mor1kx_cpu.cappuccino.mor1kx_cpu.mor1kx_lsu_cappuccino.dc_err +@2024 +[color] 3 +^2 /home/shorne/work/openrisc/local-cores/mor1kx/bench/formal/states-lsu.txt +mor1kx.mor1kx_cpu.cappuccino.mor1kx_cpu.mor1kx_lsu_cappuccino.state[2:0] +@28 +mor1kx.mor1kx_cpu.cappuccino.mor1kx_cpu.mor1kx_lsu_cappuccino.dc_refill_req +mor1kx.mor1kx_cpu.cappuccino.mor1kx_cpu.mor1kx_lsu_cappuccino.dc_refill_done +@200 +-LSU.dcache +@2024 +[color] 3 +^1 /home/shorne/work/openrisc/local-cores/mor1kx/bench/formal/states-dcache.txt +mor1kx.mor1kx_cpu.cappuccino.mor1kx_cpu.mor1kx_lsu_cappuccino.dcache_gen.mor1kx_dcache.state[4:0] +[pattern_trace] 1 +[pattern_trace] 0 diff --git a/bench/formal/mor1kx.sby b/bench/formal/mor1kx.sby index f731c672..c0cd630f 100644 --- a/bench/formal/mor1kx.sby +++ b/bench/formal/mor1kx.sby @@ -1,7 +1,7 @@ # We only check the first few cycles since we just confirm reset conditions [options] -mode prove -depth 5 +mode bmc +depth 10 [engines] smtbmc yices diff --git a/bench/formal/mor1kx_cpu_cappuccino.gtkw b/bench/formal/mor1kx_cpu_cappuccino.gtkw new file mode 100644 index 00000000..a4bd55a4 --- /dev/null +++ b/bench/formal/mor1kx_cpu_cappuccino.gtkw @@ -0,0 +1,158 @@ +[*] +[*] GTKWave Analyzer v3.3.108 (w)1999-2020 BSI +[*] Mon May 2 02:35:06 2022 +[*] +[dumpfile] "/home/shorne/work/openrisc/local-cores/mor1kx/bench/formal/mor1kx_cpu_cappuccino/engine_0/trace_induct.vcd" +[dumpfile_mtime] "Sun May 1 08:39:41 2022" +[dumpfile_size] 776476 +[savefile] "/home/shorne/work/openrisc/local-cores/mor1kx/bench/formal/mor1kx_cpu_cappuccino.gtkw" +[timestart] 28 +[size] 1360 872 +[pos] -1 -1 +*-5.214850 146 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 +[treeopen] mor1kx_cpu_cappuccino. +[treeopen] mor1kx_cpu_cappuccino.mor1kx_lsu_cappuccino.dcache_gen. +[treeopen] mor1kx_cpu_cappuccino.mor1kx_lsu_cappuccino.dcache_gen.mor1kx_dcache. +[sst_width] 281 +[signals_width] 278 +[sst_expanded] 1 +[sst_vpaned_height] 251 +@28 +smt_clock +@420 +smt_step +@200 +-exceptions +@28 +mor1kx_cpu_cappuccino.decode_except_ibus_err_o +mor1kx_cpu_cappuccino.execute_except_ibus_err_o +mor1kx_cpu_cappuccino.msync_stall_o +mor1kx_cpu_cappuccino.pipeline_flush_o +mor1kx_cpu_cappuccino.snoop_en_i +@200 +-ibus +@28 +mor1kx_cpu_cappuccino.ibus_req_o +mor1kx_cpu_cappuccino.ibus_ack_i +[color] 1 +mor1kx_cpu_cappuccino.ibus_err_i +@200 +-dbus +@28 +mor1kx_cpu_cappuccino.dbus_req_o +mor1kx_cpu_cappuccino.dbus_we_o +mor1kx_cpu_cappuccino.dbus_ack_i +[color] 1 +mor1kx_cpu_cappuccino.dbus_err_i +@200 +- +-FETCH +@22 +mor1kx_cpu_cappuccino.mor1kx_fetch_cappuccino.pc_addr[31:0] +mor1kx_cpu_cappuccino.mor1kx_fetch_cappuccino.pc_decode_o[31:0] +mor1kx_cpu_cappuccino.mor1kx_fetch_cappuccino.decode_insn_o[31:0] +@24 +[color] 2 +mor1kx_cpu_cappuccino.mor1kx_fetch_cappuccino.fetch_rfa_adr_o[4:0] +[color] 3 +mor1kx_cpu_cappuccino.mor1kx_fetch_cappuccino.fetch_rfb_adr_o[4:0] +@28 +[color] 3 +mor1kx_cpu_cappuccino.mor1kx_fetch_cappuccino.fetch_valid_o +@200 +-DECODE +@22 +[color] 1 +mor1kx_cpu_cappuccino.mor1kx_decode.decode_imm16_o[15:0] +@24 +[color] 2 +mor1kx_cpu_cappuccino.mor1kx_decode.decode_rfa_adr_o[4:0] +[color] 3 +mor1kx_cpu_cappuccino.mor1kx_decode.decode_rfb_adr_o[4:0] +@28 +mor1kx_cpu_cappuccino.mor1kx_decode.decode_op_mfspr_o +mor1kx_cpu_cappuccino.mor1kx_decode.decode_op_mtspr_o +mor1kx_cpu_cappuccino.mor1kx_decode.decode_op_lsu_load_o +mor1kx_cpu_cappuccino.mor1kx_decode.decode_op_lsu_store_o +mor1kx_cpu_cappuccino.mor1kx_decode.decode_op_lsu_atomic_o +mor1kx_cpu_cappuccino.mor1kx_decode.decode_op_msync_o +@200 +-DECODE EXEC +@28 +[color] 7 +mor1kx_cpu_cappuccino.mor1kx_decode_execute_cappuccino.padv_i +mor1kx_cpu_cappuccino.mor1kx_decode_execute_cappuccino.execute_op_lsu_load_o +mor1kx_cpu_cappuccino.mor1kx_decode_execute_cappuccino.execute_op_lsu_store_o +mor1kx_cpu_cappuccino.mor1kx_decode_execute_cappuccino.execute_op_lsu_atomic_o +mor1kx_cpu_cappuccino.mor1kx_decode_execute_cappuccino.execute_op_msync_o +@200 +-EXEC_CTRL +@28 +[color] 7 +mor1kx_cpu_cappuccino.mor1kx_execute_ctrl_cappuccino.padv_i +mor1kx_cpu_cappuccino.mor1kx_execute_ctrl_cappuccino.ctrl_op_mfspr_o +mor1kx_cpu_cappuccino.mor1kx_execute_ctrl_cappuccino.ctrl_op_mtspr_o +mor1kx_cpu_cappuccino.mor1kx_execute_ctrl_cappuccino.ctrl_op_lsu_load_o +mor1kx_cpu_cappuccino.mor1kx_execute_ctrl_cappuccino.ctrl_op_lsu_store_o +mor1kx_cpu_cappuccino.mor1kx_execute_ctrl_cappuccino.ctrl_op_lsu_atomic_o +mor1kx_cpu_cappuccino.mor1kx_execute_ctrl_cappuccino.ctrl_op_msync_o +@200 +- +-LSU +@28 +mor1kx_cpu_cappuccino.mor1kx_lsu_cappuccino.dmmu_enable_i +mor1kx_cpu_cappuccino.mor1kx_lsu_cappuccino.dc_enable_i +[color] 3 +mor1kx_cpu_cappuccino.mor1kx_lsu_cappuccino.lsu_valid_o +@200 +-LSU.s1 +@28 +[color] 7 +mor1kx_cpu_cappuccino.mor1kx_lsu_cappuccino.padv_execute_i +mor1kx_cpu_cappuccino.mor1kx_lsu_cappuccino.exec_op_lsu_load_i +mor1kx_cpu_cappuccino.mor1kx_lsu_cappuccino.exec_op_lsu_store_i +mor1kx_cpu_cappuccino.mor1kx_lsu_cappuccino.exec_op_lsu_atomic_i +@200 +-LSU.s2 +@28 +[color] 7 +mor1kx_cpu_cappuccino.mor1kx_lsu_cappuccino.padv_ctrl_i +mor1kx_cpu_cappuccino.mor1kx_lsu_cappuccino.ctrl_op_lsu_load_i +mor1kx_cpu_cappuccino.mor1kx_lsu_cappuccino.ctrl_op_lsu_store_i +mor1kx_cpu_cappuccino.mor1kx_lsu_cappuccino.ctrl_op_lsu_atomic_i +mor1kx_cpu_cappuccino.mor1kx_lsu_cappuccino.ctrl_op_msync_i +mor1kx_cpu_cappuccino.mor1kx_lsu_cappuccino.spr_bus_stb_i +@200 +- +@2024 +[color] 3 +^1 /home/shorne/work/openrisc/local-cores/mor1kx/bench/formal/states-lsu.txt +mor1kx_cpu_cappuccino.mor1kx_lsu_cappuccino.state[2:0] +@28 +mor1kx_cpu_cappuccino.mor1kx_lsu_cappuccino.tlb_reload_done +mor1kx_cpu_cappuccino.mor1kx_lsu_cappuccino.store_buffer_write_pending +mor1kx_cpu_cappuccino.mor1kx_lsu_cappuccino.store_buffer_full +mor1kx_cpu_cappuccino.mor1kx_lsu_cappuccino.dbus_stall +mor1kx_cpu_cappuccino.mor1kx_lsu_cappuccino.dcache_gen.dc_req +mor1kx_cpu_cappuccino.mor1kx_lsu_cappuccino.dc_ack +mor1kx_cpu_cappuccino.mor1kx_lsu_cappuccino.dc_refill +mor1kx_cpu_cappuccino.mor1kx_lsu_cappuccino.dc_refill_r +mor1kx_cpu_cappuccino.mor1kx_lsu_cappuccino.dc_refill_req +mor1kx_cpu_cappuccino.mor1kx_lsu_cappuccino.dc_refill_done +@200 +-LSU[dcache] +@2024 +[color] 3 +^2 /home/shorne/work/openrisc/local-cores/mor1kx/bench/formal/states-dcache.txt +mor1kx_cpu_cappuccino.mor1kx_lsu_cappuccino.dcache_gen.mor1kx_dcache.state[4:0] +@200 +-CTRL +@28 +mor1kx_cpu_cappuccino.mor1kx_ctrl_cappuccino.spr_we +@22 +mor1kx_cpu_cappuccino.mor1kx_ctrl_cappuccino.spr_sr[15:0] +mor1kx_cpu_cappuccino.mor1kx_ctrl_cappuccino.spr_dmmucfgr[31:0] +mor1kx_cpu_cappuccino.mor1kx_ctrl_cappuccino.spr_dccfgr[31:0] +mor1kx_cpu_cappuccino.mor1kx_ctrl_cappuccino.spr_dcfgr[31:0] +[pattern_trace] 1 +[pattern_trace] 0 diff --git a/bench/formal/mor1kx_cpu_cappuccino.sby b/bench/formal/mor1kx_cpu_cappuccino.sby index 70d19be8..20ada002 100644 --- a/bench/formal/mor1kx_cpu_cappuccino.sby +++ b/bench/formal/mor1kx_cpu_cappuccino.sby @@ -1,7 +1,7 @@ # We only check the first few cycles since we just confirm reset conditions [options] -mode prove -depth 5 +mode bmc +depth 16 [engines] smtbmc yices @@ -14,7 +14,7 @@ read -formal mor1kx_fetch_cappuccino.v read -formal mor1kx_icache.v read -formal mor1kx_cache_lru.v read_verilog mor1kx_branch_prediction.v -read -formal mor1kx_cpu_cappuccino.v +read -formal -D CPU_CAPPUCCINO mor1kx_cpu_cappuccino.v read -formal mor1kx_ctrl_cappuccino.v read -formal mor1kx_execute_ctrl_cappuccino.v read -formal mor1kx_rf_cappuccino.v diff --git a/bench/formal/mor1kx_dcache.gtkw b/bench/formal/mor1kx_dcache.gtkw new file mode 100644 index 00000000..4e961fcd --- /dev/null +++ b/bench/formal/mor1kx_dcache.gtkw @@ -0,0 +1,88 @@ +[*] +[*] GTKWave Analyzer v3.3.108 (w)1999-2020 BSI +[*] Sun Apr 17 21:04:51 2022 +[*] +[dumpfile] "/home/shorne/work/openrisc/local-cores/mor1kx/bench/formal/mor1kx_dcache_prv/engine_0/trace_induct.vcd" +[dumpfile_mtime] "Sun Apr 17 11:12:31 2022" +[dumpfile_size] 119689 +[savefile] "/home/shorne/work/openrisc/local-cores/mor1kx/bench/formal/mor1kx_dcache.gtkw" +[timestart] 111 +[size] 1162 721 +[pos] -1 -1 +*-5.096636 117 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 +[treeopen] mor1kx_dcache. +[sst_width] 281 +[signals_width] 198 +[sst_expanded] 1 +[sst_vpaned_height] 152 +@420 +smt_step +@28 +mor1kx_dcache.clk +mor1kx_dcache.rst +[color] 1 +mor1kx_dcache.dc_dbus_err_i +[color] 1 +mor1kx_dcache.snoop_valid_i +@200 +-FSM +@28 +mor1kx_dcache.invalidate +mor1kx_dcache.write_pending +@2024 +[color] 3 +^1 /home/shorne/work/openrisc/local-cores/mor1kx/bench/formal/states-dcache.txt +mor1kx_dcache.state[4:0] +@200 +-CPU +@28 +mor1kx_dcache.cpu_we_i +mor1kx_dcache.cpu_req_i +@22 +mor1kx_dcache.cpu_adr_i[31:0] +mor1kx_dcache.cpu_adr_match_i[31:0] +mor1kx_dcache.cpu_dat_i[31:0] +mor1kx_dcache.cpu_dat_o[31:0] +@28 +mor1kx_dcache.cpu_ack_o +@200 +-SPR +@28 +[color] 2 +mor1kx_dcache.spr_bus_stb_i +[color] 2 +mor1kx_dcache.spr_bus_we_i +[color] 2 +mor1kx_dcache.spr_bus_ack_o +@22 +[color] 2 +mor1kx_dcache.spr_bus_addr_i[15:0] +[color] 2 +mor1kx_dcache.spr_bus_dat_i[31:0] +@200 +-REFILL +@28 +mor1kx_dcache.refill_allowed_i +mor1kx_dcache.refill_req_o +mor1kx_dcache.refill_we_i +mor1kx_dcache.refill_done_o +mor1kx_dcache.refill_hit +mor1kx_dcache.refill_o +@22 +mor1kx_dcache.refill_adr_i[31:0] +mor1kx_dcache.refill_dat_i[31:0] +mor1kx_dcache.way_wr_dat[31:0] +@200 +-formal +@22 +[color] 5 +mor1kx_dcache.f_op_count[4:0] +@28 +[color] 5 +mor1kx_dcache.f_read_pending +[color] 5 +mor1kx_dcache.f_write_pending +[color] 5 +mor1kx_dcache.f_flush_pending +[pattern_trace] 1 +[pattern_trace] 0 diff --git a/bench/formal/mor1kx_dcache.sby b/bench/formal/mor1kx_dcache.sby index 79234d66..82323007 100644 --- a/bench/formal/mor1kx_dcache.sby +++ b/bench/formal/mor1kx_dcache.sby @@ -1,21 +1,21 @@ [tasks] -prv cvr +prv [options] -prv: mode prove cvr: mode cover -depth 25 +prv: mode prove +depth 24 [engines] smtbmc [script] - read -formal -D DCACHE mor1kx_dcache.v read -formal mor1kx_cache_lru.v read -formal mor1kx_simple_dpram_sclk.v read -formal fspr_slave.v +chparam -set OPTION_DCACHE_BLOCK_WIDTH 4 mor1kx_dcache prep -top mor1kx_dcache [files] diff --git a/bench/formal/mor1kx_decode_execute_cappuccino.sby b/bench/formal/mor1kx_decode_execute_cappuccino.sby index e21023c3..ea15afe4 100644 --- a/bench/formal/mor1kx_decode_execute_cappuccino.sby +++ b/bench/formal/mor1kx_decode_execute_cappuccino.sby @@ -1,12 +1,12 @@ [options] mode prove -depth 20 +depth 8 [engines] smtbmc yices [script] -read -formal mor1kx_decode_execute_cappuccino.v +read -formal -D DECODE_EXECUTE mor1kx_decode_execute_cappuccino.v chparam -set FEATURE_SYSCALL "ENABLED" mor1kx_decode_execute_cappuccino chparam -set FEATURE_TRAP "ENABLED" mor1kx_decode_execute_cappuccino diff --git a/bench/formal/mor1kx_dmmu.gtkw b/bench/formal/mor1kx_dmmu.gtkw new file mode 100644 index 00000000..e0b3169e --- /dev/null +++ b/bench/formal/mor1kx_dmmu.gtkw @@ -0,0 +1,77 @@ +[*] +[*] GTKWave Analyzer v3.3.108 (w)1999-2020 BSI +[*] Fri Mar 11 13:23:11 2022 +[*] +[dumpfile] "(null)" +[savefile] "/home/shorne/work/openrisc/local-cores/mor1kx/bench/formal/mor1kx_dmmu.gtkw" +[timestart] 0 +[size] 1336 1014 +[pos] -1 -1 +*-4.640134 59 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 +[treeopen] mor1kx_dmmu. +[sst_width] 281 +[signals_width] 310 +[sst_expanded] 1 +[sst_vpaned_height] 286 +@28 +mor1kx_dmmu.u_f_dmmu_slave.clk +mor1kx_dmmu.rst +mor1kx_dmmu.enable_i +@22 +mor1kx_dmmu.virt_addr_i[31:0] +mor1kx_dmmu.virt_addr_match_i[31:0] +mor1kx_dmmu.phys_addr_o[31:0] +@28 +mor1kx_dmmu.cache_inhibit_o +mor1kx_dmmu.pagefault_o +mor1kx_dmmu.tlb_miss_o +mor1kx_dmmu.way_hit +@200 +-TLB +@28 +mor1kx_dmmu.spr_way_idx +mor1kx_dmmu.dtlb_match_spr_cs +mor1kx_dmmu.dtlb_match_we +@22 +mor1kx_dmmu.dtlb_match_addr[5:0] +mor1kx_dmmu.dtlb_match_din[31:0] +mor1kx_dmmu.dtlb_match_dout<0>[31:0] +@28 +mor1kx_dmmu.dtlb_trans_spr_cs +mor1kx_dmmu.dtlb_trans_we +@22 +mor1kx_dmmu.dtlb_trans_addr[5:0] +mor1kx_dmmu.dtlb_trans_din[31:0] +mor1kx_dmmu.dtlb_trans_dout<0>[31:0] +@200 +-SPR +@28 +mor1kx_dmmu.spr_bus_we_i +mor1kx_dmmu.spr_bus_stb_i +@22 +mor1kx_dmmu.spr_bus_addr_i[15:0] +mor1kx_dmmu.spr_bus_dat_i[31:0] +@28 +[color] 5 +mor1kx_dmmu.f_past_valid +[color] 5 +mor1kx_dmmu.f_match_set +[color] 5 +mor1kx_dmmu.f_trans_set +[color] 5 +mor1kx_dmmu.f_tlb_setup +[color] 5 +mor1kx_dmmu.f_way[1:0] +@22 +[color] 5 +mor1kx_dmmu.f_set[5:0] +@23 +[color] 5 +mor1kx_dmmu.f_vaddr[31:0] +@22 +mor1kx_dmmu.f_spr_match_addr[10:0] +mor1kx_dmmu.f_spr_match_data[31:0] +mor1kx_dmmu.f_spr_trans_addr[10:0] +mor1kx_dmmu.f_spr_trans_data[31:0] +[pattern_trace] 1 +[pattern_trace] 0 diff --git a/bench/formal/mor1kx_dmmu.sby b/bench/formal/mor1kx_dmmu.sby index d28dfb70..cc8265a8 100644 --- a/bench/formal/mor1kx_dmmu.sby +++ b/bench/formal/mor1kx_dmmu.sby @@ -3,12 +3,12 @@ prv cvr [options] -prv: mode prove +prv: mode bmc cvr: mode cover -depth 20 +depth 8 [engines] -smtbmc yices +smtbmc [script] diff --git a/bench/formal/mor1kx_execute_ctrl_cappuccino.sby b/bench/formal/mor1kx_execute_ctrl_cappuccino.sby index dbc3966c..d185746e 100644 --- a/bench/formal/mor1kx_execute_ctrl_cappuccino.sby +++ b/bench/formal/mor1kx_execute_ctrl_cappuccino.sby @@ -1,12 +1,12 @@ [options] mode prove -depth 20 +depth 8 [engines] smtbmc yices [script] -read -formal mor1kx_execute_ctrl_cappuccino.v +read -formal -D EXECUTE_CTRL mor1kx_execute_ctrl_cappuccino.v chparam -set FEATURE_FPU "ENABLED" mor1kx_execute_ctrl_cappuccino prep -top mor1kx_execute_ctrl_cappuccino diff --git a/bench/formal/mor1kx_lsu_cappuccino.gtkw b/bench/formal/mor1kx_lsu_cappuccino.gtkw new file mode 100644 index 00000000..fe5c2c9a --- /dev/null +++ b/bench/formal/mor1kx_lsu_cappuccino.gtkw @@ -0,0 +1,197 @@ +[*] +[*] GTKWave Analyzer v3.3.108 (w)1999-2020 BSI +[*] Sat Apr 16 22:27:21 2022 +[*] +[dumpfile] "/home/shorne/work/openrisc/local-cores/mor1kx/bench/formal/mor1kx_lsu_cappuccino_prv/engine_0/trace.vcd" +[dumpfile_mtime] "Sat Apr 16 22:20:31 2022" +[dumpfile_size] 80309 +[savefile] "/home/shorne/work/openrisc/local-cores/mor1kx/bench/formal/mor1kx_lsu_cappuccino.gtkw" +[timestart] 0 +[size] 1577 928 +[pos] -1 -1 +*-5.176430 47 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 +[treeopen] mor1kx_lsu_cappuccino. +[treeopen] mor1kx_lsu_cappuccino.dcache_gen. +[treeopen] mor1kx_lsu_cappuccino.dmmu_gen. +[treeopen] mor1kx_lsu_cappuccino.store_buffer_gen. +[treeopen] mor1kx_lsu_cappuccino.store_buffer_gen.mor1kx_store_buffer. +[sst_width] 281 +[signals_width] 238 +[sst_expanded] 1 +[sst_vpaned_height] 277 +@28 +smt_clock +@420 +smt_step +@28 +mor1kx_lsu_cappuccino.rst +@200 +-err +@28 +[color] 1 +mor1kx_lsu_cappuccino.pipeline_flush_i +[color] 1 +mor1kx_lsu_cappuccino.snoop_en_i +[color] 1 +mor1kx_lsu_cappuccino.except_align +[color] 1 +mor1kx_lsu_cappuccino.except_dbus +[color] 1 +mor1kx_lsu_cappuccino.except_dpagefault +[color] 1 +mor1kx_lsu_cappuccino.except_dtlb_miss +@200 +-DBUS +@28 +mor1kx_lsu_cappuccino.dbus_req_o +mor1kx_lsu_cappuccino.dbus_we_o +mor1kx_lsu_cappuccino.dbus_ack_i +[color] 1 +mor1kx_lsu_cappuccino.dbus_err_i +@22 +[color] 6 +mor1kx_lsu_cappuccino.dbus_adr_o[31:0] +@23 +[color] 6 +mor1kx_lsu_cappuccino.dbus_dat_i[31:0] +@200 +- +-LSU +@28 +mor1kx_lsu_cappuccino.padv_execute_i +mor1kx_lsu_cappuccino.padv_ctrl_i +@2024 +[color] 3 +^1 /home/shorne/work/openrisc/local-cores/mor1kx/bench/formal/states-lsu.txt +mor1kx_lsu_cappuccino.state[2:0] +@28 +[color] 3 +mor1kx_lsu_cappuccino.lsu_valid_o +mor1kx_lsu_cappuccino.msync_stall_o +@200 +- +@28 +[color] 7 +mor1kx_lsu_cappuccino.exec_op_lsu_load_i +[color] 7 +mor1kx_lsu_cappuccino.exec_op_lsu_store_i +[color] 7 +mor1kx_lsu_cappuccino.exec_op_lsu_atomic_i +@22 +[color] 7 +mor1kx_lsu_cappuccino.exec_lsu_adr_i[31:0] +@200 +- +@28 +[color] 6 +mor1kx_lsu_cappuccino.ctrl_op_lsu_load_i +[color] 6 +mor1kx_lsu_cappuccino.ctrl_op_lsu_store_i +[color] 6 +mor1kx_lsu_cappuccino.ctrl_op_lsu_atomic_i +[color] 6 +mor1kx_lsu_cappuccino.ctrl_op_msync_i +@22 +[color] 6 +mor1kx_lsu_cappuccino.ctrl_lsu_adr_i[31:0] +@200 +- +@22 +mor1kx_lsu_cappuccino.ctrl_rfb_i[31:0] +@28 +mor1kx_lsu_cappuccino.ctrl_lsu_length_i[1:0] +@200 +- +-STORE BUFFER +@22 +[color] 3 +mor1kx_lsu_cappuccino.store_buffer_wadr[31:0] +@28 +[color] 3 +mor1kx_lsu_cappuccino.store_buffer_write +[color] 3 +mor1kx_lsu_cappuccino.store_buffer_write_pending +[color] 2 +mor1kx_lsu_cappuccino.store_buffer_read +[color] 2 +mor1kx_lsu_cappuccino.store_buffer_atomic +[color] 2 +mor1kx_lsu_cappuccino.store_buffer_ack +[color] 2 +mor1kx_lsu_cappuccino.store_buffer_empty +[color] 2 +mor1kx_lsu_cappuccino.store_buffer_full +@22 +[color] 2 +mor1kx_lsu_cappuccino.store_buffer_radr[31:0] +@200 +-SPR +@28 +mor1kx_lsu_cappuccino.spr_bus_stb_i +mor1kx_lsu_cappuccino.spr_bus_we_i +@22 +mor1kx_lsu_cappuccino.spr_bus_addr_i[15:0] +@28 +mor1kx_lsu_cappuccino.spr_bus_ack_dc_o +mor1kx_lsu_cappuccino.spr_bus_ack_dmmu_o +@200 +-DMMU +@28 +mor1kx_lsu_cappuccino.dmmu_gen.mor1kx_dmmu.op_load_i +mor1kx_lsu_cappuccino.dmmu_gen.mor1kx_dmmu.op_store_i +@22 +mor1kx_lsu_cappuccino.dmmu_gen.mor1kx_dmmu.virt_addr_i[31:0] +mor1kx_lsu_cappuccino.dmmu_gen.mor1kx_dmmu.virt_addr_match_i[31:0] +mor1kx_lsu_cappuccino.dmmu_gen.mor1kx_dmmu.phys_addr_o[31:0] +@28 +mor1kx_lsu_cappuccino.dmmu_gen.mor1kx_dmmu.pagefault_o +mor1kx_lsu_cappuccino.dmmu_gen.mor1kx_dmmu.tlb_miss_o +@200 +-DCACHE +@28 +mor1kx_lsu_cappuccino.dc_enable_i +[color] 1 +mor1kx_lsu_cappuccino.dcache_gen.mor1kx_dcache.dc_dbus_err_i +@2024 +[color] 3 +^2 /home/shorne/work/openrisc/local-cores/mor1kx/bench/formal/states-dcache.txt +mor1kx_lsu_cappuccino.dcache_gen.mor1kx_dcache.state[4:0] +@28 +[color] 2 +mor1kx_lsu_cappuccino.dcache_gen.mor1kx_dcache.cpu_we_i +[color] 2 +mor1kx_lsu_cappuccino.dcache_gen.mor1kx_dcache.cpu_req_i +[color] 2 +mor1kx_lsu_cappuccino.dcache_gen.mor1kx_dcache.cpu_ack_o +mor1kx_lsu_cappuccino.dc_hit_o +@22 +[color] 2 +mor1kx_lsu_cappuccino.dcache_gen.mor1kx_dcache.cpu_adr_i[31:0] +[color] 2 +mor1kx_lsu_cappuccino.dcache_gen.mor1kx_dcache.cpu_bsel_i[3:0] +[color] 2 +mor1kx_lsu_cappuccino.dcache_gen.mor1kx_dcache.cpu_dat_i[31:0] +[color] 2 +mor1kx_lsu_cappuccino.dcache_gen.mor1kx_dcache.cpu_dat_o[31:0] +@28 +[color] 6 +mor1kx_lsu_cappuccino.dcache_gen.mor1kx_dcache.refill_req_o +[color] 6 +mor1kx_lsu_cappuccino.dcache_gen.mor1kx_dcache.refill_we_i +[color] 6 +mor1kx_lsu_cappuccino.dcache_gen.mor1kx_dcache.refill_done_o +@22 +[color] 6 +mor1kx_lsu_cappuccino.dcache_gen.mor1kx_dcache.refill_adr_i[31:0] +@200 +-FORMAL +@28 +mor1kx_lsu_cappuccino.dcache_gen.mor1kx_dcache.f_past_valid +@22 +mor1kx_lsu_cappuccino.f_op_count[4:0] +@28 +mor1kx_lsu_cappuccino.f_spr_pending +mor1kx_lsu_cappuccino.f_lsu_pending +mor1kx_lsu_cappuccino.f_msync_pending +[pattern_trace] 1 +[pattern_trace] 0 diff --git a/bench/formal/mor1kx_lsu_cappuccino.sby b/bench/formal/mor1kx_lsu_cappuccino.sby index 146d312e..28a423b8 100644 --- a/bench/formal/mor1kx_lsu_cappuccino.sby +++ b/bench/formal/mor1kx_lsu_cappuccino.sby @@ -1,5 +1,10 @@ +[tasks] +cvr +prv + [options] -mode prove +cvr: mode cover +prv: mode bmc depth 20 [engines] @@ -17,7 +22,10 @@ read -formal mor1kx_cache_lru.v read -formal fspr_slave.v chparam -set FEATURE_DATACACHE "ENABLED" mor1kx_lsu_cappuccino +chparam -set OPTION_DCACHE_BLOCK_WIDTH 4 mor1kx_lsu_cappuccino chparam -set FEATURE_DMMU "ENABLED" mor1kx_lsu_cappuccino +chparam -set FEATURE_STORE_BUFFER "ENABLED" mor1kx_lsu_cappuccino +chparam -set OPTION_STORE_BUFFER_DEPTH_WIDTH 2 mor1kx_lsu_cappuccino chparam -set FEATURE_ATOMIC "ENABLED" mor1kx_lsu_cappuccino prep -top mor1kx_lsu_cappuccino diff --git a/bench/formal/mor1kx_simple_dpram_sclk.gtkw b/bench/formal/mor1kx_simple_dpram_sclk.gtkw new file mode 100644 index 00000000..62658988 --- /dev/null +++ b/bench/formal/mor1kx_simple_dpram_sclk.gtkw @@ -0,0 +1,40 @@ +[*] +[*] GTKWave Analyzer v3.3.108 (w)1999-2020 BSI +[*] Sat Mar 12 08:16:57 2022 +[*] +[dumpfile] "/home/shorne/work/openrisc/local-cores/mor1kx/bench/formal/mor1kx_simple_dpram_sclk_bypass_cvr/engine_0/trace0.vcd" +[dumpfile_mtime] "Sat Mar 12 08:14:13 2022" +[dumpfile_size] 1561 +[savefile] "/home/shorne/work/openrisc/local-cores/mor1kx/bench/formal/mor1kx_simple_dpram_sclk.gtkw" +[timestart] 0 +[size] 1262 600 +[pos] -1 -1 +*-3.576178 78 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 +[sst_width] 281 +[signals_width] 134 +[sst_expanded] 1 +[sst_vpaned_height] 155 +@28 +smt_clock +@420 +smt_step +@28 +mor1kx_simple_dpram_sclk.clk +mor1kx_simple_dpram_sclk.f_past_valid +mor1kx_simple_dpram_sclk.we +@22 +mor1kx_simple_dpram_sclk.waddr[7:0] +@23 +mor1kx_simple_dpram_sclk.din[31:0] +@22 +mor1kx_simple_dpram_sclk.f_addr[7:0] +[color] 3 +mor1kx_simple_dpram_sclk.f_data[31:0] +@28 +[color] 5 +mor1kx_simple_dpram_sclk.re +@22 +mor1kx_simple_dpram_sclk.raddr[7:0] +mor1kx_simple_dpram_sclk.dout[31:0] +[pattern_trace] 1 +[pattern_trace] 0 diff --git a/bench/formal/mor1kx_simple_dpram_sclk.sby b/bench/formal/mor1kx_simple_dpram_sclk.sby index ee8ed943..1ce63976 100644 --- a/bench/formal/mor1kx_simple_dpram_sclk.sby +++ b/bench/formal/mor1kx_simple_dpram_sclk.sby @@ -1,10 +1,14 @@ [tasks] -BYPASS bypass -NO_BYPASS no_bypass +bypass_prv bypass prove +nopypass_prv prove +bypass_cvr bypass cover +nopypass_cvr cover + [options] -mode prove -depth 20 +prove: mode prove +cover: mode cover +depth 10 wait on [engines] @@ -16,6 +20,7 @@ read -formal -D SDPRAM mor1kx_simple_dpram_sclk.v --pycode-begin-- cmd = "hierarchy -top mor1kx_simple_dpram_sclk" cmd+= " -chparam ENABLE_BYPASS %d" % (1 if "bypass" in tags else 0) +cmd+= " -chparam ADDR_WIDTH 8" output(cmd) --pycode-end-- diff --git a/bench/formal/mor1kx_store_buffer.gtkw b/bench/formal/mor1kx_store_buffer.gtkw new file mode 100644 index 00000000..0ea60640 --- /dev/null +++ b/bench/formal/mor1kx_store_buffer.gtkw @@ -0,0 +1,40 @@ +[*] +[*] GTKWave Analyzer v3.3.108 (w)1999-2020 BSI +[*] Thu Apr 14 21:03:02 2022 +[*] +[dumpfile] "/home/shorne/work/openrisc/local-cores/mor1kx/bench/formal/mor1kx_store_buffer_cvr/engine_0/trace0.vcd" +[dumpfile_mtime] "Thu Apr 14 21:02:09 2022" +[dumpfile_size] 23380 +[savefile] "/home/shorne/work/openrisc/local-cores/mor1kx/bench/formal/mor1kx_store_buffer.gtkw" +[timestart] 0 +[size] 1467 600 +[pos] -1 -1 +*-4.576430 23 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 +[treeopen] mor1kx_store_buffer. +[treeopen] mor1kx_store_buffer.fifo_ram. +[sst_width] 281 +[signals_width] 222 +[sst_expanded] 1 +[sst_vpaned_height] 152 +@28 +mor1kx_store_buffer.clk +mor1kx_store_buffer.rst +mor1kx_store_buffer.read_i +mor1kx_store_buffer.write_i +[color] 3 +mor1kx_store_buffer.read_pointer[3:0] +[color] 3 +mor1kx_store_buffer.write_pointer[3:0] +mor1kx_store_buffer.empty_o +mor1kx_store_buffer.full_o +@24 +[color] 6 +mor1kx_store_buffer.f_curr_fifo_entries[4:0] +@28 +[color] 6 +mor1kx_store_buffer.f_write_idx[4:0] +@29 +[color] 6 +mor1kx_store_buffer.f_seen_full +[pattern_trace] 1 +[pattern_trace] 0 diff --git a/bench/formal/mor1kx_store_buffer.sby b/bench/formal/mor1kx_store_buffer.sby index 5c5cc943..3964752e 100644 --- a/bench/formal/mor1kx_store_buffer.sby +++ b/bench/formal/mor1kx_store_buffer.sby @@ -1,14 +1,20 @@ +[tasks] +cvr +prv + [options] -mode prove +cvr: mode cover +prv: mode prove depth 30 [engines] smtbmc yices [script] - read -formal mor1kx_simple_dpram_sclk.v read -formal -DBUFFER mor1kx_store_buffer.v + +chparam -set DEPTH_WIDTH 3 mor1kx_store_buffer prep -top mor1kx_store_buffer [files] diff --git a/bench/formal/mor1kx_true_dpram_sclk.gtkw b/bench/formal/mor1kx_true_dpram_sclk.gtkw new file mode 100644 index 00000000..0b84eb30 --- /dev/null +++ b/bench/formal/mor1kx_true_dpram_sclk.gtkw @@ -0,0 +1,67 @@ +[*] +[*] GTKWave Analyzer v3.3.108 (w)1999-2020 BSI +[*] Sat Mar 12 06:30:56 2022 +[*] +[dumpfile] "/home/shorne/work/openrisc/local-cores/mor1kx/bench/formal/mor1kx_true_dpram_sclk_prv/engine_0/trace.vcd" +[dumpfile_mtime] "Sat Mar 12 06:27:12 2022" +[dumpfile_size] 2738 +[savefile] "/home/shorne/work/openrisc/local-cores/mor1kx/bench/formal/mor1kx_true_dpram_sclk.gtkw" +[timestart] 0 +[size] 1479 600 +[pos] -1 -1 +*-3.976430 24 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 +[sst_width] 281 +[signals_width] 142 +[sst_expanded] 1 +[sst_vpaned_height] 273 +@28 +smt_clock +@420 +smt_step +@22 +mor1kx_true_dpram_sclk.mem<9e>[31:0] +mor1kx_true_dpram_sclk.mem<8e>[31:0] +@200 +-PORT-A +@28 +[color] 2 +mor1kx_true_dpram_sclk.clk_a +[color] 2 +mor1kx_true_dpram_sclk.we_a +@22 +[color] 2 +mor1kx_true_dpram_sclk.addr_a[7:0] +[color] 2 +mor1kx_true_dpram_sclk.din_a[31:0] +[color] 2 +mor1kx_true_dpram_sclk.dout_a[31:0] +@200 +-PORT-B +@28 +[color] 7 +mor1kx_true_dpram_sclk.clk_b +[color] 7 +mor1kx_true_dpram_sclk.we_b +@22 +[color] 7 +mor1kx_true_dpram_sclk.addr_b[7:0] +[color] 7 +mor1kx_true_dpram_sclk.din_b[31:0] +[color] 7 +mor1kx_true_dpram_sclk.dout_b[31:0] +@200 +-FORMAL +@28 +[color] 5 +mor1kx_true_dpram_sclk.f_past_valid +@22 +[color] 5 +mor1kx_true_dpram_sclk.f_addr_a[7:0] +[color] 5 +mor1kx_true_dpram_sclk.f_data_a[31:0] +[color] 5 +mor1kx_true_dpram_sclk.f_addr_b[7:0] +[color] 5 +mor1kx_true_dpram_sclk.f_data_b[31:0] +[pattern_trace] 1 +[pattern_trace] 0 diff --git a/bench/formal/mor1kx_true_dpram_sclk.sby b/bench/formal/mor1kx_true_dpram_sclk.sby index cda781b8..3c0e866c 100644 --- a/bench/formal/mor1kx_true_dpram_sclk.sby +++ b/bench/formal/mor1kx_true_dpram_sclk.sby @@ -1,8 +1,13 @@ +[tasks] +prv +cvr + [options] -mode prove -#True DPRAM uses two clocks, so turning on multiclock option +prv: mode prove +cvr: mode cover +#True DPRAM uses two clocks, so turning on multiclock option multiclock on -depth 30 +depth 10 wait on [engines] @@ -11,6 +16,7 @@ smtbmc yices [script] read -formal -D TDPRAM mor1kx_true_dpram_sclk.v +hierarchy -top mor1kx_true_dpram_sclk -chparam ADDR_WIDTH 8 prep -top mor1kx_true_dpram_sclk [files] diff --git a/bench/formal/states-dcache.txt b/bench/formal/states-dcache.txt new file mode 100644 index 00000000..ca5984d2 --- /dev/null +++ b/bench/formal/states-dcache.txt @@ -0,0 +1,5 @@ +1 IDLE +2 READ +4 WRITE +8 REFILL +16 INVALIDATE diff --git a/bench/formal/states-lsu.txt b/bench/formal/states-lsu.txt new file mode 100644 index 00000000..12ff5d12 --- /dev/null +++ b/bench/formal/states-lsu.txt @@ -0,0 +1,5 @@ +0 IDLE +1 READ +2 WRITE +3 TLB_RELOAD +4 DC_REFILL diff --git a/rtl/verilog/mor1kx_cpu_cappuccino.v b/rtl/verilog/mor1kx_cpu_cappuccino.v index 9db05715..9811cbae 100644 --- a/rtl/verilog/mor1kx_cpu_cappuccino.v +++ b/rtl/verilog/mor1kx_cpu_cappuccino.v @@ -1567,6 +1567,10 @@ module mor1kx_cpu_cappuccino traceport_exec_insn_o <= {`OR1K_INSN_WIDTH{1'b0}}; traceport_exec_pc_o <= 32'h0; traceport_exec_valid_o <= 1'b0; + traceport_exec_jbtarget_o <= 32'h0; + traceport_exec_jal_o <= 1'b0; + traceport_exec_jr_o <= 1'b0; + traceport_exec_jb_o <= 1'b0; end end @@ -1633,6 +1637,28 @@ module mor1kx_cpu_cappuccino $rose(spr_bus_ack_dc_i) || $rose(spr_bus_ack_ic_i))) assert (spr_bus_stb_o || $past(spr_bus_stb_o)); +// Simple interface assumptions when testing cpu_cappuccino alone +`ifdef CPU_CAPPUCCINO + // DBUS/IBUS inputs + always @(posedge clk) begin + // When we send a request we either get back an ack or an error + if ($past(ibus_req_o) & ibus_req_o) + assume ($onehot({ibus_ack_i,ibus_err_i})); + if ($past(dbus_req_o) & dbus_req_o) + assume ($onehot({dbus_ack_i,dbus_err_i})); + + // Don't allow spurious errors and acks when no requests + if (!dbus_req_o) begin + assume (!dbus_ack_i); + assume (!dbus_err_i); + end + if (!ibus_req_o) begin + assume (!ibus_ack_i); + assume (!ibus_err_i); + end + end +`endif // CPU_CAPPUCCINO + always @(*) case (ibus_dat_i[`OR1K_ALU_OPC_SELECT]) `OR1K_ALU_OPC_ADDC, @@ -1666,5 +1692,5 @@ module mor1kx_cpu_cappuccino .spr_bus_ack_immu_i(spr_bus_ack_immu_i), .f_past_valid(f_past_valid) ); -`endif +`endif // FORMAL endmodule // mor1kx_cpu_cappuccino diff --git a/rtl/verilog/mor1kx_ctrl_cappuccino.v b/rtl/verilog/mor1kx_ctrl_cappuccino.v index 40d11cfd..8a562025 100644 --- a/rtl/verilog/mor1kx_ctrl_cappuccino.v +++ b/rtl/verilog/mor1kx_ctrl_cappuccino.v @@ -1491,6 +1491,9 @@ module mor1kx_ctrl_cappuccino spr_drr <= 0; du_npc_written <= 0; cpu_stall <= 0; + + stepped_into_rfe <= 0; + stepped_into_exception <= 0; end end endgenerate @@ -1621,14 +1624,11 @@ endgenerate if (f_past_valid && !$past(rst) && $rose(ctrl_bubble_o)) assert ($past(execute_bubble_i)); +`ifndef CTRL //SPR shouldn't give more than one acknowledgement always @* assert ($onehot0(spr_access_ack)); - - //SPR acknowledgement makes spr access valid - always @* - if ($onehot(spr_access_ack)) - assert (spr_access_valid); +`endif //Insn mfspr should always read from spr and //insn mtspr should always write to spr. diff --git a/rtl/verilog/mor1kx_dcache.v b/rtl/verilog/mor1kx_dcache.v index d4609028..692d2236 100644 --- a/rtl/verilog/mor1kx_dcache.v +++ b/rtl/verilog/mor1kx_dcache.v @@ -9,6 +9,72 @@ ******************************************************************************/ +// The mor1kx dcache is implemented as a write around cache with an +// optimization to populate cache line (write though) entries if a there is +// a valid entry in the dcache. + +// Cases: + +// 1. Write to cached memory entry +// A data cache write operation will update cached way data if there is +// a valid cache-line entry. A write request must be guaranteed to finish in +// 2 clock cycles. First clock cycle request, second clock cycle write. The +// LSU does not expect a response and will only present the write request to +// the data cache for 2 clock cycles. This will be extended only if there is +// a snoop hit or in refill state. +// +// A write starts by transitioning the data cache FSM into WRITE state. +// While in the WRITE state the tag memory and way memory will be written to. +// +// If already in WRITE state a write option can complete in one cycle. +// +// 2. Write to non-cached memory entry +// A data cache write to a non-cached entry is similar to a cached write +// however tag and way memory will not be updated. The FSM will sill need to +// transition to the WRITE state in order to check the cache-line. +// +// 3. Read from cached memory entry +// A data cache read will first transition the data cache FSM to the READ +// state. When in the read state a valid entry in the way memory will be +// represented as a hit. +// +// The cache-line data be provided back to the LSU. This is done by +// asserting the cpu ack line. +// +// If the data cache is already in the READ state valid read requests will +// complete in 1 clock cycle. +// +// 4. Read from non-cached memory entry +// A data cache read for a non-cached memory entry will first transition the +// FSM to the READ state to check the cache-line. If the cache-line does not +// have a valid entry (miss) the data cache will transition to the REFILL +// state. During REFILL the data cache requests the LSU to operate the data +// bus and provide cache REFILL data. When a cache-line if filled the data +// cache requests the LSU to stop. +// +// During refill when the request cache-line entry is being filled it will be +// provided back to the LSU. This provides better performance as the pending +// read does not need to wait for the refill to complete. This is done by +// asserting the cpu ack line. +// +// 5. SPR request to invalidate or flush entries +// A data cache SPR request will first transition the FSM into the +// INVALIDATE state. Once in the invalidate state the requested cache-line +// entries will be invalidated. The completion of this operation is +// represented as an SPR ack. +// +// 6. Snoop Operation +// Snoop is a signal that comes when there has been a CPU external memory +// write on bus. The data cache must invalidate valid entries in tag +// memory when this occurs. +// +// Snoop operations are highest priority and like other operations take +// a maximum of 2 clock cycles. One cycle to register the request and one +// cycle to perform the invalidation. +// +// When there is a snoop hit the data cache indicates this to the LSU to +// delay any pending writes. + `include "mor1kx-defines.v" module mor1kx_dcache @@ -25,11 +91,24 @@ module mor1kx_dcache input rst, input dc_dbus_err_i, + // Indicates if data cache is enabled on the CPU input dc_enable_i, + // Indicates the data cache is being accessed for a read or write input dc_access_i, + + // Refill Interface + // Indicate to LSU that refill is in progress output refill_o, + // Request to the LSU to start and complete a refill transaction + // at the current read address. output refill_req_o, output refill_done_o, + // Refill inputs from the LSU + input refill_allowed_i, + input [OPTION_OPERAND_WIDTH-1:0] refill_adr_i, + input [OPTION_OPERAND_WIDTH-1:0] refill_dat_i, + input refill_we_i, + output cache_hit_o, // CPU Interface @@ -43,12 +122,6 @@ module mor1kx_dcache input cpu_we_i, input [3:0] cpu_bsel_i, - input refill_allowed, - - input [OPTION_OPERAND_WIDTH-1:0] wradr_i, - input [OPTION_OPERAND_WIDTH-1:0] wrdat_i, - input we_i, - // Snoop address input [31:0] snoop_adr_i, // Snoop event in this cycle @@ -57,13 +130,11 @@ module mor1kx_dcache // this cycle. The LSU may need to stall the pipeline. output snoop_hit_o, - // SPR interface input [15:0] spr_bus_addr_i, input spr_bus_we_i, input spr_bus_stb_i, input [OPTION_OPERAND_WIDTH-1:0] spr_bus_dat_i, - output [OPTION_OPERAND_WIDTH-1:0] spr_bus_dat_o, output spr_bus_ack_o ); @@ -161,8 +232,10 @@ module mor1kx_dcache wire [OPTION_DCACHE_WAYS-1:0] way_hit; // This is the least recently used value before access the memory. - // Those are one hot encoded. - wire [OPTION_DCACHE_WAYS-1:0] lru; + // It is the value of current_lru_history that is combinationally + // one hot encoded. + // Used to select which way to replace during refill. + wire [OPTION_DCACHE_WAYS-1:0] current_lru; // Register that stores the LRU value from lru reg [OPTION_DCACHE_WAYS-1:0] tag_save_lru; @@ -171,9 +244,12 @@ module mor1kx_dcache // a hit or is refilled. It is also one-hot encoded. reg [OPTION_DCACHE_WAYS-1:0] access; - // The current LRU history as read from tag memory and the update - // value after we accessed it to write back to tag memory. + // The current encoded LRU history as read from tag memory. wire [TAG_LRU_WIDTH_BITS-1:0] current_lru_history; + // This is the encoded value of current LRU history after being combined + // with the access vector. + // This value is written back to tag memory if there is a hit or + // refill. wire [TAG_LRU_WIDTH_BITS-1:0] next_lru_history; // Intermediate signals to ease debugging @@ -215,13 +291,17 @@ module mor1kx_dcache genvar i; + // Ack the to LSU to indicate a Data Cache read is ready assign cpu_ack_o = ((read | refill) & hit & !write_pending | refill_hit) & cpu_req_i & !snoop_hit; assign tag_rindex = cpu_adr_i[WAY_WIDTH-1:OPTION_DCACHE_BLOCK_WIDTH]; assign tag_tag = cpu_adr_match_i[OPTION_DCACHE_LIMIT_WIDTH-1:WAY_WIDTH]; - assign tag_wtag = wradr_i[OPTION_DCACHE_LIMIT_WIDTH-1:WAY_WIDTH]; + assign tag_wtag = refill_adr_i[OPTION_DCACHE_LIMIT_WIDTH-1:WAY_WIDTH]; + + assign cpu_err_o = 0; + assign spr_bus_dat_o = 0; generate if (OPTION_DCACHE_WAYS >= 2) begin @@ -234,7 +314,7 @@ module mor1kx_dcache for (i = 0; i < OPTION_DCACHE_WAYS; i=i+1) begin : ways assign way_raddr[i] = cpu_adr_i[WAY_WIDTH-1:2]; assign way_waddr[i] = write ? cpu_adr_match_i[WAY_WIDTH-1:2] : - wradr_i[WAY_WIDTH-1:2]; + refill_adr_i[WAY_WIDTH-1:2]; assign way_din[i] = way_wr_dat; // compare stored tag with incoming tag and check valid bit @@ -280,16 +360,16 @@ module mor1kx_dcache end assign next_refill_adr = (OPTION_DCACHE_BLOCK_WIDTH == 5) ? - {wradr_i[31:5], wradr_i[4:0] + 5'd4} : // 32 byte - {wradr_i[31:4], wradr_i[3:0] + 4'd4}; // 16 byte + {refill_adr_i[31:5], refill_adr_i[4:0] + 5'd4} : // 32 byte + {refill_adr_i[31:4], refill_adr_i[3:0] + 4'd4}; // 16 byte assign refill_done_o = refill_done; assign refill_done = refill_valid[next_refill_adr[OPTION_DCACHE_BLOCK_WIDTH-1:2]]; assign refill_hit = refill_valid_r[cpu_adr_match_i[OPTION_DCACHE_BLOCK_WIDTH-1:2]] & cpu_adr_match_i[OPTION_DCACHE_LIMIT_WIDTH-1: OPTION_DCACHE_BLOCK_WIDTH] == - wradr_i[OPTION_DCACHE_LIMIT_WIDTH-1: - OPTION_DCACHE_BLOCK_WIDTH] & + refill_adr_i[OPTION_DCACHE_LIMIT_WIDTH-1: + OPTION_DCACHE_BLOCK_WIDTH] & refill & !write_pending; assign refill = (state == REFILL); @@ -298,7 +378,7 @@ module mor1kx_dcache assign refill_o = refill; - assign refill_req_o = read & cpu_req_i & !hit & !write_pending & refill_allowed | refill; + assign refill_req_o = read & cpu_req_i & !hit & !write_pending & refill_allowed_i | refill; /* * SPR bus interface @@ -339,9 +419,6 @@ module mor1kx_dcache */ integer w1; always @(posedge clk `OR_ASYNC_RST) begin - // The default is (of course) not to acknowledge the invalidate - invalidate_ack <= 1'b0; - if (rst) begin state <= IDLE; write_pending <= 0; @@ -377,7 +454,7 @@ module mor1kx_dcache // Store address in invalidate_adr that is muxed to the tag // memory write address invalidate_adr <= spr_bus_dat_i[WAY_WIDTH-1:OPTION_DCACHE_BLOCK_WIDTH]; - invalidate_ack <= 1'b1; + // Change to invalidate state that actually accesses // the tag memory state <= INVALIDATE; @@ -389,21 +466,21 @@ module mor1kx_dcache READ: begin if (dc_access_i | cpu_we_i & dc_enable_i) begin - if (!hit & cpu_req_i & !write_pending & refill_allowed) begin + if (cpu_we_i | write_pending) begin + state <= WRITE; + end else if (!hit & cpu_req_i & refill_allowed_i) begin refill_valid <= 0; refill_valid_r <= 0; // Store the LRU information for correct replacement // on refill. Always one when only one way. - tag_save_lru <= (OPTION_DCACHE_WAYS==1) | lru; + tag_save_lru <= (OPTION_DCACHE_WAYS==1) | current_lru; for (w1 = 0; w1 < OPTION_DCACHE_WAYS; w1 = w1 + 1) begin tag_way_save[w1] <= tag_way_out[w1]; end state <= REFILL; - end else if (cpu_we_i | write_pending) begin - state <= WRITE; end else if (invalidate) begin state <= IDLE; end @@ -413,8 +490,8 @@ module mor1kx_dcache end REFILL: begin - if (we_i) begin - refill_valid[wradr_i[OPTION_DCACHE_BLOCK_WIDTH-1:2]] <= 1; + if (refill_we_i) begin + refill_valid[refill_adr_i[OPTION_DCACHE_BLOCK_WIDTH-1:2]] <= 1; if (refill_done) state <= IDLE; @@ -431,19 +508,23 @@ module mor1kx_dcache WRITE: begin if ((!dc_access_i | !cpu_req_i | !cpu_we_i) & !snoop_hit) begin write_pending <= 0; - state <= READ; + state <= IDLE; end end INVALIDATE: begin - if (invalidate) begin + if (cpu_we_i) begin + // If we get a write while we are in invalidate its because + // We have already acked the invalidate and the control unit + // has moved on. So start the write as if we were in READ + // or idle. + state <= WRITE; + end else if (invalidate) begin // Store address in invalidate_adr that is muxed to the tag // memory write address invalidate_adr <= spr_bus_dat_i[WAY_WIDTH-1:OPTION_DCACHE_BLOCK_WIDTH]; - invalidate_ack <= 1'b1; + state <= INVALIDATE; - end else if (cpu_we_i | write_pending) begin - state <= WRITE; end else begin state <= IDLE; end @@ -472,7 +553,10 @@ module mor1kx_dcache access = {(OPTION_DCACHE_WAYS){1'b0}}; - way_wr_dat = wrdat_i; + way_wr_dat = refill_dat_i; + + // The default is (of course) not to acknowledge the invalidate + invalidate_ack = 1'b0; if (snoop_hit) begin // This is the write access @@ -488,16 +572,16 @@ module mor1kx_dcache end else begin // // The tag mem is written during reads and writes to write - // the lru info and during refill and invalidate. + // the lru info and during refill and invalidate. // tag_windex = read | write ? cpu_adr_match_i[WAY_WIDTH-1:OPTION_DCACHE_BLOCK_WIDTH] : (state == INVALIDATE) ? invalidate_adr : - wradr_i[WAY_WIDTH-1:OPTION_DCACHE_BLOCK_WIDTH]; + refill_adr_i[WAY_WIDTH-1:OPTION_DCACHE_BLOCK_WIDTH]; case (state) READ: begin - if (hit) begin + if (hit & cpu_req_i) begin // // We got a hit. The LRU module gets the access // information. Depending on this we update the LRU @@ -514,7 +598,7 @@ module mor1kx_dcache WRITE: begin way_wr_dat = cpu_dat_i; - if (hit & (cpu_req_i | write_pending)) begin + if (hit & cpu_req_i) begin /* Mux cache output with write data */ if (!cpu_bsel_i[3]) way_wr_dat[31:24] = cpu_dat_o[31:24]; @@ -525,6 +609,7 @@ module mor1kx_dcache if (!cpu_bsel_i[0]) way_wr_dat[7:0] = cpu_dat_o[7:0]; + // Only write data to way ram if we have a valid cacheline way_we = way_hit; tag_lru_in = next_lru_history; @@ -534,7 +619,7 @@ module mor1kx_dcache end REFILL: begin - if (we_i) begin + if (refill_we_i) begin // // Write the data to the way that is replaced (which is // the LRU) @@ -575,6 +660,8 @@ module mor1kx_dcache end INVALIDATE: begin + invalidate_ack = 1'b1; + // Lazy invalidation, invalidate everything that matches tag address tag_lru_in = 0; for (w2 = 0; w2 < OPTION_DCACHE_WAYS; w2 = w2 + 1) begin @@ -613,20 +700,12 @@ module mor1kx_dcache end if (OPTION_DCACHE_WAYS >= 2) begin : gen_u_lru - /* mor1kx_cache_lru AUTO_TEMPLATE( - .current (current_lru_history), - .update (next_lru_history), - .lru_pre (lru), - .lru_post (), - .access (access), - ); */ - mor1kx_cache_lru #(.NUMWAYS(OPTION_DCACHE_WAYS)) - u_lru(/*AUTOINST*/ + u_lru( // Outputs .update (next_lru_history), // Templated - .lru_pre (lru), // Templated + .lru_pre (current_lru), // Templated .lru_post (), // Templated // Inputs .current (current_lru_history), // Templated @@ -685,301 +764,240 @@ endgenerate `define ASSUME assert `endif + wire [WAY_WIDTH-OPTION_DCACHE_BLOCK_WIDTH-1:0] f_cpu_adr; reg f_past_valid; initial f_past_valid = 1'b0; initial assume (rst); + assign f_cpu_adr = cpu_adr_i[WAY_WIDTH-1:OPTION_DCACHE_BLOCK_WIDTH]; + always @(posedge clk) f_past_valid <= 1'b1; always @(*) if (!f_past_valid) - assume (rst); + assume (rst); //-----------Assumptions on Inputs----------- always @(posedge clk) begin if (cpu_req_i) - `ASSUME (dc_access_i); + `ASSUME (dc_access_i); + + if (spr_bus_we_i) + `ASSUME (spr_bus_stb_i); + + // We cannot overlap read/write with flushes + `ASSUME ($onehot0({cpu_req_i, spr_bus_stb_i})); + + // Assert to ensure induction doesn't enter a state where + // dout and memory register feedback loop doesn't start out + // of sync. This is kind of a bug, but dcache should only + // be used if properly initialized by flushing all dcache entries + // which will avoid this case. + if (f_past_valid && + state == READ && $stable(state) && + $past(f_cpu_adr) == $past(f_cpu_adr,2)) + a1_no_register_feedback: assert ($stable(tag_dout[TAG_LRU_LSB-1:0])); end -//-------------Assertions-------------------- +//---------Tests are only valid after setup `ifdef DCACHE + localparam F_COUNT_WIDTH = 5; + localparam F_COUNT_MSB = F_COUNT_WIDTH-1; + localparam F_COUNT_START = {1'b0,{(F_COUNT_WIDTH-1){1'b1}}}; + localparam F_COUNT_RESET = {F_COUNT_WIDTH{1'b1}}; + + (* anyconst *) wire [OPTION_OPERAND_WIDTH-1:0] f_addr; + wire [OPTION_DCACHE_BLOCK_WIDTH-3:0] f_cacheline_idx; + wire f_cpu_addr_here; + wire f_spr_addr_here; + + reg [F_COUNT_WIDTH-1:0] f_op_count; + reg f_write_pending; + reg f_read_pending; + reg f_flush_pending; + reg f_write_complete; + reg f_read_complete; + reg f_flush_complete; + wire [2:0] f_pending; + + assign f_cacheline_idx = f_addr[OPTION_DCACHE_BLOCK_WIDTH-1:2]; + assign f_cpu_addr_here = f_addr[OPTION_OPERAND_WIDTH-1:OPTION_DCACHE_BLOCK_WIDTH] == + cpu_adr_i[OPTION_OPERAND_WIDTH-1:OPTION_DCACHE_BLOCK_WIDTH]; + assign f_spr_addr_here = f_addr[OPTION_OPERAND_WIDTH-1:OPTION_DCACHE_BLOCK_WIDTH] == + spr_bus_dat_i[OPTION_OPERAND_WIDTH-1:OPTION_DCACHE_BLOCK_WIDTH]; + + assign f_pending = {f_write_pending, f_read_pending, f_flush_pending}; + + // Basic cases we need to help simulate + // 1. Cache invalidate + // 2. Read + // 3. Write + // + // 1, 2 and 3 cannot happen at the same time. + // Read and Write are only possible after invalidation. + // Read may trigger a refill. -//----------Verifying functionality--------- - -//Case 1: Refill followed by read + // Used to confirm invalidation/read/write complete + initial f_op_count = {F_COUNT_WIDTH{1'b1}}; - (* anyconst *) wire [OPTION_OPERAND_WIDTH-1:0] f_refill_addr; - (* anyconst *) reg [OPTION_OPERAND_WIDTH-1:0] f_refill_data; - wire f_this_refill; - reg f_refilled; - initial f_refilled = 1'b0; - assign f_this_refill = (wradr_i == f_refill_addr) && refill_o; + initial f_flush_pending = 0; + initial f_write_pending = 0; + initial f_read_pending = 0; + initial f_flush_complete = 0; + initial f_write_complete = 0; + initial f_read_complete = 0; - //Refilling always @(posedge clk) begin - if ($past(f_this_refill) && (f_refill_data == wrdat_i) - && !$past(write_pending) && $past(refill_allowed) - && !$past(cache_hit_o)&& $past(cpu_req_i) - && f_past_valid && !$past(rst) && - $past(state) == READ) begin - assert (refill); - f_refilled <= 1'b1; - assert ($onehot(way_we)); + // Don't block out refill when testing DCACHE + assume (refill_allowed_i); + + assume ($past(cpu_adr_i) == cpu_adr_match_i); + + // Request lags write by 1 clock cycle, not always true + // might be more, but helps with testing DCACHE + if ($past(cpu_we_i)) + assume (cpu_req_i); + + if (|f_pending) + assume (!cpu_we_i); + + if (f_flush_pending) begin + assume ($stable(spr_bus_addr_i)); + assume ($stable(spr_bus_we_i)); + assume ($stable(spr_bus_stb_i)); + assume ($stable(spr_bus_dat_i)); + end else if (f_read_pending) begin + assume ($stable(cpu_req_i)); + assume ($stable(cpu_adr_match_i)); + assume ($stable(cpu_bsel_i)); + end else if (f_write_pending) begin + assume ($stable(cpu_adr_i)); + assume ($stable(cpu_bsel_i)); end - end - //Read: Asserting if f_refill_data is returned if the - // cpu requests for same address f_refill_addr. - always @(posedge clk) begin - if ($rose(f_refilled) && (cpu_adr_match_i == f_refill_addr) - && cache_hit_o && f_past_valid && !$past(rst)) begin - assert (cpu_dat_o == f_refill_data); - assert (read); - assert (cpu_ack_o); - end - end + a0_one_op_pending: assert ($onehot0(f_pending)); - reg f_after_invalidate; - initial f_after_invalidate = 1'b0; + // If f_op_count has MSB set all bits are set in reset state + if (f_op_count[F_COUNT_MSB]) + assert (&f_op_count); - //Invalidation : Checking if ways of set have invalid tag bit - // on set invalidation. - always @(posedge clk) begin - if ($past(invalidate) && !$past(refill) && f_past_valid && - $past(spr_bus_dat_i) == f_refill_addr[WAY_WIDTH-1:OPTION_DCACHE_BLOCK_WIDTH] - && $past(f_refilled) && !$past(f_refilled,2)) begin - assert (spr_bus_ack_o); - assert (invalidate); - assert (!cpu_ack_o); - assert (tag_we); - assert (!tag_din[TAGMEM_WAY_VALID]); - f_after_invalidate <= 1; - end - end + // Induction helpers - //There shouldn't be any cache hit for f_refill_addr after invalidation. - always @(posedge clk) - if (cpu_adr_match_i == f_refill_addr && $rose(f_after_invalidate) - && f_past_valid) - assert (!cache_hit_o); - -//Case 2: Write followed by read - - (* anyconst *) wire [OPTION_OPERAND_WIDTH-1:0] f_write_addr; - (* anyconst *) reg [OPTION_OPERAND_WIDTH-1:0] f_write_data; - wire f_this_write; - reg f_written; - initial f_written = 1'b0; - assign f_this_write = (cpu_adr_match_i == f_write_addr); + // If we have anything pending we must be counting + if (|f_pending) + a1_count_if_pending: assert (f_op_count[F_COUNT_MSB] == 0); + // And vice versa, if we are counting something should be pending + if (f_op_count[F_COUNT_MSB] == 0) + a2_pending_if_counting: assert (|f_pending); + end - //Write - always @(posedge clk) - if (f_this_write && (f_write_data == cpu_dat_i) - && $past(cpu_we_i) && f_past_valid && !$past(rst) - && !$past(invalidate) && cpu_bsel_i == 4'hf - && !$past(write_pending) && !$past(dc_dbus_err_i) - && !invalidate && !dc_dbus_err_i && $past(state) == IDLE - && $onehot(way_hit) && cpu_req_i) begin - assert (write); - assert ($onehot(way_we)); - f_written <= 1; - end - - //Read - always @(posedge clk) - if (f_past_valid && $past(f_written) && !$past(f_written,2) - && $past(cpu_adr_i) == f_write_addr && (cpu_adr_match_i == f_write_addr) - && !write_pending && cpu_req_i && !$past(rst) - && cache_hit_o && !$past(way_we)) begin - assert (cpu_dat_o == f_write_data); - end + // Track pending operations + always @(posedge clk) begin + if (rst | dc_dbus_err_i) begin + f_write_pending <= 0; + f_flush_pending <= 0; + f_read_pending <= 0; + f_op_count <= F_COUNT_RESET; + end else if (f_past_valid & f_op_count[F_COUNT_MSB]) begin + // If idle check if we can start a transaction + if (invalidate & !spr_bus_ack_o) begin + f_flush_pending <= 1; + f_op_count <= F_COUNT_START; + end else if (cpu_we_i | (write_pending & cpu_req_i)) begin + f_write_pending <= 1; + f_op_count <= F_COUNT_START; + end else if (cpu_req_i & !cpu_ack_o) begin + f_read_pending <= 1; + f_op_count <= F_COUNT_START; + end + end else if (f_op_count == {F_COUNT_WIDTH{1'b0}}) begin + // If the counter expires check if we have anything pending + a1_flush_complete: assert (!f_flush_pending); + a2_write_complete: assert (!f_write_pending); + a3_read_complete: assert (!f_read_pending); + + f_op_count <= F_COUNT_RESET; + end else if (f_op_count <= F_COUNT_START) + // If we are in counding mode count + f_op_count <= f_op_count - 1; + + // Track completes + if (f_past_valid & !f_op_count[F_COUNT_MSB] & f_op_count > 0) begin + // If we just get into write state assume complete + if (write) begin + f_write_pending <= 0; + f_op_count <= F_COUNT_RESET; + if (tag_we & f_cpu_addr_here) + f_write_complete <= 1; + end - reg f_invalid; - initial f_invalid = 1'b0; + if (f_flush_pending & spr_bus_ack_o) begin + f_flush_pending <= 0; + f_op_count <= F_COUNT_RESET; + if (f_spr_addr_here) + f_flush_complete <= 1; + end - //Invalidate f_write_addr - always @(posedge clk) - if (!$past(invalidate,2) && $past(invalidate) && f_past_valid && - $past(spr_bus_dat_i) == f_write_addr[WAY_WIDTH-1:OPTION_DCACHE_BLOCK_WIDTH] - && $rose(f_written) && !$past(dc_dbus_err_i) && !$past(cpu_we_i)) begin - assert (spr_bus_ack_o); - assert (!cpu_ack_o); - assert (tag_we); - assert (!tag_din[TAGMEM_WAY_VALID]); - f_invalid <= 1'b1; + if (cpu_ack_o) begin + f_read_pending <= 0; + f_op_count <= F_COUNT_RESET; + if (f_cpu_addr_here) + f_read_complete <= 1; + end end - - //No cache hit for invalidated address - always @(posedge clk) - if (f_past_valid && cpu_adr_match_i == f_write_addr - && $rose(f_invalid) && f_past_valid) - assert (!cache_hit_o); - -`endif - -//-------------DCACHE PROPERTIES------------------- - - //Cache hit in read state updates lru access variable - always @(posedge clk) begin - if (f_past_valid && !$past(rst) && way_hit[0] - && $onehot(way_hit) && read) - assert (access == way_hit[0]); end - //Way ram writes only on cpu write request or refill request. - always @(posedge clk) - if (way_we == way_hit && $onehot(way_hit) && - f_past_valid && !$past(rst) && !dc_dbus_err_i) - assert (cpu_we_i || write_pending || we_i || - $past(write_pending)); - - //CPU acknowledgement is given only if cache fulfills cpu's request. - always @(posedge clk) - if (cpu_ack_o) - assert (cpu_req_i); - - //CPU receives acknowledgement only on cache hits or refill hits. - always @(posedge clk) - if (cpu_ack_o && f_past_valid && !$past(rst)) - assert (cache_hit_o || refill_hit); - - //Back to back writes should keep write pending high - always @(posedge clk) - if (f_past_valid && !$past(rst) && $past(cpu_we_i) && cpu_we_i - && !$past(dc_dbus_err_i) && cache_hit_o && - !$past(cpu_we_i,2) && $past(rst,2)) - assert (write_pending); - always @(posedge clk) - if (write_pending && f_past_valid && !$past(rst)) - assert ($past(cpu_we_i) || $past(write_pending)); - - //Write is successful only if there is cache hit - always @(*) - if ($onehot(way_we) && write) - assert (cache_hit_o); - - //Cache writes should update both way and tag memories - always @(posedge clk) - if (write && cpu_req_i && cache_hit_o && $onehot(way_hit) && f_past_valid) - assert (tag_we && $onehot(way_we)); - - //Refill data 'wrdat_i' shouldn't be written while doing write operation - always @(posedge clk) - if (write && f_past_valid && cpu_dat_i != wrdat_i && - !$past(rst) && cpu_bsel_i == 4'hf) - assert (way_wr_dat != wrdat_i); - - //Dcache triggers to refill state only if there is cache miss - always @(posedge clk) - if ($rose(refill_o) && f_past_valid && !$past(rst)) - assert (!$past(cache_hit_o)); + // Simulate refill transactions when requested + reg [OPTION_OPERAND_WIDTH-1:0] f_refill_addr; + reg f_refill_we; - //Refill hit shouldn't happen in any state other than refill - always @(posedge clk) - if (refill_hit && f_past_valid && !$past(rst)) - assert (state != READ && state != WRITE && state != INVALIDATE && state != IDLE); - - //Refilling should always update way ram - always @(*) - if (refill_o && we_i && $onehot(tag_save_lru)) - assert ($onehot(way_we)); + initial f_refill_addr = 0; + initial f_refill_we = 0; - //Before refilling tag should be invalidated - always @(*) - if (refill_o && !refill_valid && we_i) - assert (tag_we); - -//---------INVALIDATION AND SPR BUS ---------- - - //Dcache invalidation is initiated only if the spr request - // is for block flush or block invalidate - always @(posedge clk) - if (invalidate) - assert (spr_bus_addr_i == `OR1K_SPR_DCBFR_ADDR | - spr_bus_addr_i == `OR1K_SPR_DCBIR_ADDR); - - //Invalidate should acknowledge only if spr has some invalidate request - //or if cache remains in either idle or invalidate state. - always @(posedge clk) - if ($rose(invalidate_ack) && f_past_valid && !$past(rst)) - assert (state == INVALIDATE || state == IDLE || $past(invalidate)); - - reg f_1st_inv; - initial f_1st_inv = 1'b0; - - //Checking back to back invalidation writes - always @(posedge clk) - if ($past(invalidate) && invalidate && f_past_valid && !$past(rst) - && $past(rst,2) && !$past(dc_dbus_err_i) && !$past(cpu_we_i,2) - && !dc_dbus_err_i && !rst) begin - assert (tag_we); - f_1st_inv <= 1'b1; - end - always @(posedge clk) - if ($rose(f_1st_inv) && f_past_valid) begin - assert (tag_we); - assert (invalidate_ack); + always @(posedge clk) begin + assume (refill_we_i == f_refill_we); + assume (refill_adr_i == f_refill_addr); + + if (f_refill_we & refill_req_o) begin + if (refill_done_o) + f_refill_we <= 0; + else + f_refill_addr <= f_refill_addr + 4; + end else if (f_past_valid & refill_req_o) begin + f_refill_we <= 1; + f_refill_addr <= { cpu_adr_i[31:OPTION_DCACHE_BLOCK_WIDTH], {OPTION_DCACHE_BLOCK_WIDTH{1'b0}} }; + end else begin + f_refill_we <= 0; + f_refill_addr <= 0; end + end - //SPR acknowledgement is valid only if there is invalidate acknowledgement. - always @(posedge clk) - if (spr_bus_ack_o) - assert (invalidate_ack); - - //If invalidation and write arrives at same the clock invalidation wins over writing - //Case 1: Just after reset - always @(posedge clk) - if ($past(invalidate) && f_past_valid && !$past(rst) - && $past(cpu_we_i) && !$past(dc_dbus_err_i) - && !$past(cpu_we_i,2) && $past(rst,2)) begin - assert (write_pending); - assert (invalidate_ack); - end + always @(posedge clk) begin + c0_cache_invalidate: cover(f_past_valid & f_flush_complete); + c1_cache_read: cover(f_past_valid & f_read_complete); + c2_cache_write: cover(f_past_valid & f_write_complete); + end - //Case 2:Invalidate and write signal arriving at same clock, not right after reset. - //If cache is in read state and these signals arrive then write wins over invalidation. - always @(posedge clk) - if ($past(invalidate) && f_past_valid && !$past(rst) - && $past(cpu_we_i) && !$past(dc_dbus_err_i) && !$past(cpu_we_i,2) - && !$past(rst,2) && !$past(write_pending,2) && !$past(write_pending)) - assert (write_pending); +`endif fspr_slave #( .OPTION_OPERAND_WIDTH(OPTION_OPERAND_WIDTH), .SLAVE("DCACHE") ) - u_f_icache_slave ( - .clk(clk), - .rst(rst), - // SPR interface - .spr_bus_addr_i(spr_bus_addr_i), - .spr_bus_we_i(spr_bus_we_i), - .spr_bus_stb_i(spr_bus_stb_i), - .spr_bus_dat_i(spr_bus_dat_i), - .spr_bus_dat_o(spr_bus_dat_o), - .spr_bus_ack_o(spr_bus_ack_o), - .f_past_valid(f_past_valid) + u_f_dcache_slave ( + .clk(clk), + .rst(rst), + // SPR interface + .spr_bus_addr_i(spr_bus_addr_i), + .spr_bus_we_i(spr_bus_we_i), + .spr_bus_stb_i(spr_bus_stb_i), + .spr_bus_dat_i(spr_bus_dat_i), + .spr_bus_dat_o(spr_bus_dat_o), + .spr_bus_ack_o(spr_bus_ack_o), + .f_past_valid(f_past_valid) ); -//----------------Cover----------------- - - //Cache Write-----------Trace 0 - always @(posedge clk) - cover (state == WRITE && tag_we && $onehot(way_we) && f_past_valid && !$past(rst)); - - //Invalidation----------Trace 1 - always @(posedge clk) - cover (tag_we && state == INVALIDATE && !$past(rst) && f_past_valid); - - //Cache Read------------Trace 2 - always @(posedge clk) - cover (state == READ && tag_we && cache_hit_o && cpu_ack_o && !$past(rst) && f_past_valid); - - //Refilling-------------Trace 3 - always @(posedge clk) - cover (refill_o && $onehot(way_we) && refill_done && tag_we && !$past(rst) && f_past_valid); - `endif endmodule diff --git a/rtl/verilog/mor1kx_decode_execute_cappuccino.v b/rtl/verilog/mor1kx_decode_execute_cappuccino.v index 1b63e007..b88c2f17 100644 --- a/rtl/verilog/mor1kx_decode_execute_cappuccino.v +++ b/rtl/verilog/mor1kx_decode_execute_cappuccino.v @@ -594,6 +594,12 @@ module mor1kx_decode_execute_cappuccino `ifdef FORMAL +`ifdef DECODE_EXECUTE +`define ASSUME assume +`else +`define ASSUME assert +`endif + reg f_past_valid; initial f_past_valid = 1'b0; initial assume (rst); @@ -758,6 +764,37 @@ module mor1kx_decode_execute_cappuccino end end + //one instruction => one opcode + wire [30:0] f_input_opcodes; + wire [30:0] f_output_opcodes; + assign f_input_opcodes = {decode_op_lsu_load_i, decode_op_lsu_store_i, + decode_op_mfspr_i, decode_op_mtspr_i, + decode_op_rfe_i, decode_op_setflag_i, + decode_op_add_i, decode_op_mul_signed_i, + decode_op_mul_unsigned_i, + decode_op_div_signed_i, + decode_op_ext_i, decode_op_div_unsigned_i, + decode_op_shift_i, decode_op_ffl1_i, + decode_op_movhi_i, decode_op_msync_i, + decode_op_branch_i}; + + assign f_output_opcodes = {execute_op_lsu_load_o, execute_op_lsu_store_o, + execute_op_mfspr_o, execute_op_mtspr_o, + execute_op_rfe_o, execute_op_setflag_o, + execute_op_add_o, execute_op_mul_signed_o, + execute_op_mul_unsigned_o, + execute_op_div_signed_o, execute_op_ext_o, + execute_op_div_unsigned_o, execute_op_shift_o, + execute_op_ffl1_o,execute_op_movhi_o, + execute_op_msync_o,execute_op_branch_o}; + + //one instruction => one opcode + always @(*) begin + `ASSUME ($onehot0(f_input_opcodes)); + if (f_past_valid) + assert ($onehot0(f_output_opcodes)); + end + //Fetch related any exceptions should be observed in decode stage always @(posedge clk) begin if (f_past_valid && $rose(execute_except_illegal_o) diff --git a/rtl/verilog/mor1kx_dmmu.v b/rtl/verilog/mor1kx_dmmu.v index a6325ecb..ec68cbbd 100644 --- a/rtl/verilog/mor1kx_dmmu.v +++ b/rtl/verilog/mor1kx_dmmu.v @@ -7,6 +7,80 @@ ******************************************************************************/ +// The mor1k data memory management unit (MMU) provides an multi way +// configurable MMU with optional support for harward TLB reloading. + +// Cases: + +// 1. TLB Matching +// When the MMU is enabled and a valid entry exists in the TLB memory +// the virtual address to physical address translation takes one clock +// cycle. +// +// In the case that a valid TLB entry does not exist the TLB MISS output +// will be raised. +// +// In the case that a valid TLB entry exists but request does not have +// permission to proceed the PAGE FAULT output will be raised. +// +// 2. TLB SPR Write/Read +// Writing and Reading to the TLB Match and Translate registers conforms +// to the SPR databus standard protocol. +// +// 3. Hardware TLB Reload and Huge Pages +// Hardware TLB reloading is supported by using the base pointer from +// the DMMUCR SPR. TLB reloading also supports loading huge pages which +// provide 16MB (24-bit) pages. +// +// This is documented below, but not in a lot of detail as this feature +// is not actively used. +// +// When a TLB miss happens the hardware reloading enabled the MMU will +// request to the LSU to control the data bus to perform the TLB. This +// takes multiple cycles. + +// virt_addr_match ---------------+ +// | +// virt_addr ( == )-+->o--> tlb_miss +// | | | +// +---+-----> [ Match TLB ] ---+ | +// | ^ 0--[ 0 ] +// +-----> [ Trans TLB ] -------[ 1 ]--> phys_addr +// ^ +// clk---------------+ + +// SPR Addresses +// +// +-----------+-------+---+-------+---------+ +// | 15 11 | 10 8 | 7 | 6 4 | 3 0 | +// +-----------+-------+---+-------+---------+ +// | group | way | MT| set | +// +-----------+-------+---+-------+---------+ +// | 0 0 0 0 1 | 0 1 0 | 0 | x x x | x x x x | +// | 0 0 0 0 1 | 0 1 0 | 1 | x x x | x x x x | +// | 0 0 0 0 1 | 0 1 1 | 0 | x x x | x x x x | +// | 0 0 0 0 1 | 0 1 1 | 1 | x x x | x x x x | +// | 0 0 0 0 1 | 1 0 0 | 0 | x x x | x x x x | +// | 0 0 0 0 1 | 1 0 0 | 1 | x x x | x x x x | +// | 0 0 0 0 1 | 1 0 1 | 0 | x x x | x x x x | +// | 0 0 0 0 1 | 1 0 1 | 1 | x x x | x x x x | +// +-----------+-------+---+-------+---------+ + +// 8K pages (13-bits) +// +// / TLB Match Addr \ +// +------------+--------------------+---------+ +// | 31 .. | 13+SET_WIDTH .. 13 | 12 .. 0 | +// +------------+--------------------+---------+ +// +// Huge 16MB Page (24-bits), only available with TLB reload +// +// / TLB Match Addr \ +// +------------+--------------------+---------+ +// | 31 .. | 24+SET_WIDTH .. 24 | 23 .. 0 | +// +------------+--------------------+---------+ + + `include "mor1kx-defines.v" module mor1kx_dmmu @@ -124,14 +198,22 @@ module mor1kx_dmmu generate for (i = 0; i < OPTION_DMMU_WAYS; i=i+1) begin : ways - assign way_huge[i] = &dtlb_match_huge_dout[i][1:0]; // huge & valid - assign way_hit[i] = (dtlb_match_dout[i][31:13] == virt_addr_match_i[31:13]) & dtlb_match_dout[i][0]; // valid bit - assign way_huge_hit[i] = (dtlb_match_huge_dout[i][31:24] == - virt_addr_match_i[31:24]) & - dtlb_match_huge_dout[i][0]; + // Huge pages are only supported with TLB RELOAD, if we don't + // block this off way_huge may be asserted randomly after + // reset based on the contents of TLB ram which are not + // cleared. + if (FEATURE_DMMU_HW_TLB_RELOAD == "ENABLED") begin + assign way_huge[i] = &dtlb_match_huge_dout[i][1:0]; // huge & valid + assign way_huge_hit[i] = (dtlb_match_huge_dout[i][31:24] == + virt_addr_match_i[31:24]) & + dtlb_match_huge_dout[i][0]; + end else begin + assign way_huge[i] = 0; + assign way_huge_hit[i] = 0; + end end endgenerate @@ -394,6 +476,7 @@ end else begin // if (FEATURE_DMMU_HW_TLB_RELOAD == "ENABLED") tlb_reload_req_o <= 0; tlb_reload_addr_o <= 0; tlb_reload_pagefault <= 0; + tlb_reload_huge <= 0; dtlb_trans_reload_we <= 0; dtlb_trans_reload_din <= 0; dtlb_match_reload_we <= 0; @@ -461,73 +544,111 @@ endgenerate `define ASSUME assert `endif - reg f_past_valid; - (* anyconst *) wire [OPTION_OPERAND_WIDTH-1:0] f_vaddr; + reg f_past_valid; + initial f_past_valid = 1'b0; - initial assume (rst); always @(posedge clk) f_past_valid <= 1'b1; + always @(*) if (!f_past_valid) - assume (rst); + assume (rst); else - assume (!rst); + assume (!rst); - always @(posedge clk) begin - if (f_past_valid && !$past(rst)) - `ASSUME ($onehot0({op_load_i, op_store_i})); - end + always @(*) + if (f_past_valid) + a0_load_or_store: `ASSUME ($onehot0({op_load_i, op_store_i})); -//------------------DMMU PROPERTIES------------------- +`ifdef DMMU + + reg f_match_set; + reg f_trans_set; + wire f_tlb_setup; + wire f_spr_addr_is_tlb; + reg [OPTION_OPERAND_WIDTH-1:0] f_spr_match_data; + reg [OPTION_OPERAND_WIDTH-1:0] f_spr_trans_data; + wire [OPTION_DMMU_SET_WIDTH-1:0] f_set; + + (* anyconst *) wire [OPTION_OPERAND_WIDTH-1:0] f_vaddr; + (* anyconst *) wire [WAYS_WIDTH-1:0] f_way; + + initial f_match_set = 0; + initial f_trans_set = 0; + initial f_spr_match_data = 0; + initial f_spr_trans_data = 0; + + assign f_tlb_setup = f_match_set & f_trans_set & f_spr_match_data[0]; + + assign f_set = f_vaddr[13+(OPTION_DMMU_SET_WIDTH-1):13]; + + assign f_spr_addr_is_tlb = spr_way_idx == f_way && // match way + (spr_bus_addr_i[OPTION_DMMU_SET_WIDTH-1:0] == + f_set); // match set + + always @(*) begin + assume (spr_way_idx < OPTION_DMMU_WAYS); + end - //Physical Address of f_vaddr virtual address is asserted to verify expected PPN. - //Case 1: Page bits = 13 bits always @(posedge clk) begin - if ((virt_addr_match_i == f_vaddr) && way_hit[0] - && !way_huge[0] && !pagefault_o && f_past_valid) - assert ((phys_addr_o[12:0] == f_vaddr[12:0]) && - phys_addr_o[31:13] == dtlb_trans_dout[0][31:13]); + a1_virt_addr_progress: `ASSUME ($past(virt_addr_i) == virt_addr_match_i); end - //Case 2: Page bits = 24 bits (huge) always @(posedge clk) begin - if ((virt_addr_match_i == f_vaddr) && way_huge_hit[0] - && way_huge[0] && !pagefault_o && f_past_valid) - assert ((phys_addr_o[23:0] == f_vaddr[23:0]) && - phys_addr_o[31:24] == dtlb_trans_huge_dout[0][31:24]); + if (f_past_valid) begin + if (f_spr_addr_is_tlb && spr_bus_we_i) begin + + if (spr_bus_dat_i[31:13] == f_vaddr[31:13]) begin + // Capture match address or translate address + if (dtlb_match_spr_cs) begin + f_match_set <= 1; + f_spr_match_data <= spr_bus_dat_i; + end else if (dtlb_trans_spr_cs) begin + f_trans_set <= 1; + f_spr_trans_data <= spr_bus_dat_i; + end + end else begin + // If we change the match address, de-assert setup + if (dtlb_match_spr_cs) begin + f_match_set <= 0; + end + end + end + + // If we are setup assert translates will be valid + if (virt_addr_match_i[31:13] == f_vaddr[31:13]) begin + if ($past(f_tlb_setup) & !$past(spr_bus_stb_i)) begin + a2_tlb_hit: assert (!tlb_miss_o); + end + end + end end - //On TLB miss, mmu should not inhibit cache. - always @(*) - if (tlb_miss_o) - assert (!cache_inhibit_o); +//----------------Cover------------------ + always @(*) begin - assert ($onehot0(way_hit)); - assert ($onehot0(way_huge_hit)); + c0_spr_match_write: cover (f_past_valid & f_match_set); + c1_spr_trans_write: cover (f_past_valid & f_trans_set); + c2_spr_tlb_setup: cover (f_past_valid & f_tlb_setup); + c3_spr_tlb_hit: cover (f_past_valid & f_tlb_setup && !tlb_miss_o); + c4_spr_pagefault: cover (f_past_valid & f_tlb_setup && pagefault_o); end +`endif - //On TLB hit, tlb_miss_o should be 0. - always @(*) - if (way_huge[0] & way_huge_hit[0] || !way_huge[0] & way_hit[0]) - assert (!tlb_miss_o); +//------------------DMMU PROPERTIES------------------- - //DMMU SPR registers are accessible only if the last 5 bits - // of spr_bus_addr_i corresponds to group 1. - always @(*) - if ($onehot(dtlb_match_we) || $onehot(dtlb_trans_we)) - assert (spr_bus_addr_i[15:11] == 5'd1); + //We can't have cache_inhibit when we have a tlb miss + always @(*) begin + if (f_past_valid) begin + assert ($onehot0({tlb_miss_o, cache_inhibit_o})); + end + end //Spr can't access both Match TLB and Translation TLB at the same time. - always @(posedge clk) - if (dtlb_match_spr_cs) - assert (!dtlb_trans_spr_cs); - - //Disabling Hardware TLB loads dtlb_match_din and dtlb_trans_din - // with spr_bus_dat_i, so its neccessary to check both match and - // translate TLBs don't write TLB with same data. - always @(*) - if ($onehot(dtlb_match_we)) - assert (!$onehot(dtlb_trans_we)); + always @(posedge clk) begin + assert ($onehot0({dtlb_match_spr_cs, dtlb_trans_spr_cs})); + assert ($onehot0({dtlb_match_we, dtlb_trans_we})); + end //If spr ack is received, assert stb always @(posedge clk) @@ -556,24 +677,5 @@ endgenerate .f_past_valid(f_past_valid) ); -//----------------Cover------------------ - -`ifdef DMMU - - always @(posedge clk) begin - if (f_past_valid && !$past(rst)) begin - //TLB HIT-------------Trace 0 - cover (!tlb_miss_o && phys_addr_o != 0); - //Trans write---------Trace 1 - cover (dtlb_trans_spr_cs && $past(dtlb_trans_we) - && $rose(spr_bus_ack_o)); - //Match write---------Trace 2 - cover (dtlb_match_spr_cs && $past(dtlb_match_we) - && $rose(spr_bus_ack_o)); - end - end - -`endif - `endif endmodule // mor1kx_dmmu diff --git a/rtl/verilog/mor1kx_execute_alu.v b/rtl/verilog/mor1kx_execute_alu.v index e31b5010..998516ee 100644 --- a/rtl/verilog/mor1kx_execute_alu.v +++ b/rtl/verilog/mor1kx_execute_alu.v @@ -702,6 +702,8 @@ endgenerate /* verilator lint_on WIDTH */ assign cmov_result = flag_i ? a : b; end + else + assign cmov_result = 32'b0; endgenerate // Sign Extension @@ -733,6 +735,9 @@ endgenerate ext_result = a; endcase // case(opc_alu_i) end + else + always @* + ext_result = 32'b0; endgenerate // Comparison logic diff --git a/rtl/verilog/mor1kx_execute_ctrl_cappuccino.v b/rtl/verilog/mor1kx_execute_ctrl_cappuccino.v index 8f88c3bb..ffe78f69 100644 --- a/rtl/verilog/mor1kx_execute_ctrl_cappuccino.v +++ b/rtl/verilog/mor1kx_execute_ctrl_cappuccino.v @@ -386,6 +386,12 @@ endgenerate `ifdef FORMAL +`ifdef EXECUTE_CTRL +`define ASSUME assume +`else +`define ASSUME assert +`endif + reg f_past_valid; initial f_past_valid = 1'b0; initial assume (rst); @@ -438,6 +444,24 @@ endgenerate end end + wire [7:0] f_input_opcodes; + wire [7:0] f_output_opcodes; + assign f_input_opcodes = {op_lsu_load_i, op_lsu_store_i, + op_mfspr_i, op_mtspr_i, + op_rfe_i, op_mul_i, op_msync_i}; + assign f_output_opcodes = {ctrl_op_lsu_load_o, ctrl_op_lsu_store_o, + ctrl_op_mfspr_o, ctrl_op_mtspr_o, + ctrl_op_rfe_o, ctrl_op_mul_o, + ctrl_op_msync_o}; + + //one instruction => one opcode + always @(*) begin + if (f_past_valid) begin + `ASSUME ($onehot0(f_input_opcodes)); + assert ($onehot0(f_output_opcodes)); + end + end + //If bubble is inserted in the pipeline //then the pc ctrl shouldn't advance to the next execution pc. always @(posedge clk) diff --git a/rtl/verilog/mor1kx_icache.v b/rtl/verilog/mor1kx_icache.v index f5161fd1..1ac12e0b 100644 --- a/rtl/verilog/mor1kx_icache.v +++ b/rtl/verilog/mor1kx_icache.v @@ -250,6 +250,7 @@ module mor1kx_icache */ assign invalidate_o = spr_bus_stb_i & spr_bus_we_i & (spr_bus_addr_i == `OR1K_SPR_ICBIR_ADDR); + assign spr_bus_dat_o = 32'b0; /* * Cache FSM diff --git a/rtl/verilog/mor1kx_lsu_cappuccino.v b/rtl/verilog/mor1kx_lsu_cappuccino.v index 544a8d7b..aa9f0fe7 100644 --- a/rtl/verilog/mor1kx_lsu_cappuccino.v +++ b/rtl/verilog/mor1kx_lsu_cappuccino.v @@ -15,6 +15,11 @@ `include "mor1kx-defines.v" +// The mor1kx load store unit (LSU) module controls access to the CPU data bus +// to provide memory load and store operations. The LSU provides configurable +// data cache, memmory management unit (MMU), store buffer and atomic +// operations. + module mor1kx_lsu_cappuccino #( parameter FEATURE_DATACACHE = "NONE", @@ -138,6 +143,8 @@ module mor1kx_lsu_cappuccino wire [OPTION_OPERAND_WIDTH-1:0] lsu_sdat; wire lsu_ack; + // Data Cache + // From Data Cache to LSU to indicate load request is ready wire dc_ack; wire dc_err; wire [31:0] dc_ldat; @@ -220,8 +227,11 @@ module mor1kx_lsu_cappuccino assign align_err_word = |ctrl_lsu_adr_i[1:0]; assign align_err_short = ctrl_lsu_adr_i[0]; - - assign lsu_valid_o = (lsu_ack | access_done) & !tlb_reload_busy & !dc_snoop_hit; + // Assert lsu_valid_o to progress pipeline past LSU operation if the LSU + // operation is done and we are not waiting on tlb reloads or data cache + // invalidations. + assign lsu_valid_o = (lsu_ack | access_done) & + !tlb_reload_busy & !dc_snoop_hit; assign lsu_except_dbus_o = except_dbus | store_buffer_err_o; @@ -242,6 +252,7 @@ module mor1kx_lsu_cappuccino assign lsu_except_dpagefault_o = except_dpagefault & !pipeline_flush_i; + // Assert access_done one cycle after lsu_ack, clear on padv_execute_i always @(posedge clk `OR_ASYNC_RST) if (rst) access_done <= 0; @@ -253,10 +264,10 @@ module mor1kx_lsu_cappuccino always @(posedge clk `OR_ASYNC_RST) if (rst) except_dbus <= 0; - else if (padv_execute_i | pipeline_flush_i) - except_dbus <= 0; else if (dbus_err_i) except_dbus <= 1; + else if (padv_execute_i | pipeline_flush_i) + except_dbus <= 0; always @(posedge clk `OR_ASYNC_RST) if (rst) @@ -350,6 +361,7 @@ module mor1kx_lsu_cappuccino reg [2:0] state; + // Indicates if reads come from the data bus or data cache assign dbus_access = (!dc_access | tlb_reload_busy | ctrl_op_lsu_store_i) & (state != DC_REFILL) | (state == WRITE); reg dc_refill_r; @@ -358,21 +370,23 @@ module mor1kx_lsu_cappuccino dc_refill_r <= dc_refill; wire store_buffer_ack; + // The store buffer ack is used to ack incoming write requests assign store_buffer_ack = (FEATURE_STORE_BUFFER!="NONE") ? store_buffer_write : write_done; - - // If we are writing we wait for the store buffer ack and - // in case of dcache being busy we wait for data cache ack too + + // If we are writing we wait for the store buffer ack + // If we are reading we wait for the dbus ack or in case of the + // dcache being busy wait for data cache ack assign lsu_ack = (ctrl_op_lsu_store_i | state == WRITE) ? (ctrl_op_lsu_atomic_i ? write_done : store_buffer_ack) : (dbus_access ? dbus_ack : dc_ack); + // Load data to be sent to lsu_result_o assign lsu_ldat = dbus_access ? dbus_dat : dc_ldat; - assign dbus_adr_o = dbus_adr; + assign dbus_adr_o = dbus_adr; assign dbus_dat_o = dbus_dat; - assign dbus_burst_o = (state == DC_REFILL) & !dc_refill_done; // @@ -405,10 +419,17 @@ module mor1kx_lsu_cappuccino dbus_bsel_o <= 4'hf; dbus_atomic <= 0; last_write <= 0; - if (store_buffer_write | !store_buffer_empty) begin + if (dbus_err_i | dbus_err) begin + state <= IDLE; + end else if (store_buffer_write | !store_buffer_empty) begin + // Write must be higher priority for store order state <= WRITE; + end else if (dc_refill_req) begin + dbus_req_o <= 1; + dbus_adr <= dc_adr_match; + state <= DC_REFILL; end else if (ctrl_op_lsu & dbus_access & !dc_refill & !dbus_ack & - !dbus_err & !except_dbus & !access_done & + !except_dbus & !access_done & !pipeline_flush_i) begin if (tlb_reload_req) begin dbus_adr <= tlb_reload_addr; @@ -431,10 +452,6 @@ module mor1kx_lsu_cappuccino state <= READ; end end - end else if (dc_refill_req) begin - dbus_req_o <= 1; - dbus_adr <= dc_adr_match; - state <= DC_REFILL; end end @@ -582,6 +599,9 @@ endgenerate (store_buffer_full | dc_refill | dc_refill_r | dc_snoop_hit)) store_buffer_write_pending <= 1; + // Indicates a request to write an entry to the store buffer + // this is also used to indicate the store buffer ack to + // which feeds back to the pipeline control to advance the pipeline. assign store_buffer_write = (ctrl_op_lsu_store_i & (padv_ctrl_i | tlb_reload_done) | store_buffer_write_pending) & @@ -631,6 +651,7 @@ end else begin assign store_buffer_dat = lsu_sdat; assign store_buffer_bsel = dbus_bsel; assign store_buffer_empty = 1'b1; + assign store_buffer_atomic = 1'b0; reg store_buffer_full_r; always @(posedge clk `OR_ASYNC_RST) @@ -646,6 +667,12 @@ end endgenerate assign store_buffer_wadr = dc_adr_match; + // Data Cache Logic + // Dcache Enable + // - Disabled on reset + // - When enabling the dcache wait for bus requests to finish + // - When disabling the dcache wait for dcache to lsu refill requests + // to finish always @(posedge clk `OR_ASYNC_RST) if (rst) dc_enable_r <= 0; @@ -654,10 +681,20 @@ endgenerate else if (!dc_enable_i & !dc_refill) dc_enable_r <= 0; - assign dc_enabled = dc_enable_i & dc_enable_r; + assign dc_enabled = dc_enable_r; + + // Dcache Address + // - If the *execute* stage has an upcoming LSU operation present that + // address to the dcache. + // - Otherwise present the *control* stage address. assign dc_adr = padv_execute_i & (exec_op_lsu_load_i | exec_op_lsu_store_i) ? exec_lsu_adr_i : ctrl_lsu_adr_i; + // Datacache Match Address (Pyhsical Address) + // The match address is used by the dcache on the second clock cycle + // of the lookup. + // - If the MMU is enabled present the dmmu physical address output. + // - Otherwise present the *control* stage address. assign dc_adr_match = dmmu_enable_i ? {dmmu_phys_addr[OPTION_OPERAND_WIDTH-1:2],2'b0} : {ctrl_lsu_adr_i[OPTION_OPERAND_WIDTH-1:2],2'b0}; @@ -689,76 +726,51 @@ if (FEATURE_DATACACHE!="NONE") begin : dcache_gen dbus_atomic & dbus_we_o & !write_done | ctrl_op_lsu_store_i & tlb_reload_busy & !tlb_reload_req; - /* mor1kx_dcache AUTO_TEMPLATE ( + mor1kx_dcache + #( + .OPTION_OPERAND_WIDTH(OPTION_OPERAND_WIDTH), + .OPTION_DCACHE_BLOCK_WIDTH(OPTION_DCACHE_BLOCK_WIDTH), + .OPTION_DCACHE_SET_WIDTH(OPTION_DCACHE_SET_WIDTH), + .OPTION_DCACHE_WAYS(OPTION_DCACHE_WAYS), + .OPTION_DCACHE_LIMIT_WIDTH(OPTION_DCACHE_LIMIT_WIDTH), + .OPTION_DCACHE_SNOOP(OPTION_DCACHE_SNOOP) + ) + mor1kx_dcache + ( + .clk (clk), + .rst (rst), + // Datacache high level control signals + .dc_dbus_err_i (dbus_err), + .dc_enable_i (dc_enabled), + .dc_access_i (dc_access), + // Datacache to LSU refill signals .refill_o (dc_refill), .refill_req_o (dc_refill_req), .refill_done_o (dc_refill_done), - .cache_hit_o (dc_hit), + .refill_allowed_i (dc_refill_allowed), + .refill_adr_i (dbus_adr), + .refill_dat_i (dbus_dat_i), + .refill_we_i (dbus_ack_i), + + .cache_hit_o (dc_hit_o), + + // LSU to Datacache load store interface .cpu_err_o (dc_err), .cpu_ack_o (dc_ack), .cpu_dat_o (dc_ldat), - .spr_bus_dat_o (spr_bus_dat_dc_o), - .spr_bus_ack_o (spr_bus_ack_dc_o), - .snoop_hit_o (dc_snoop_hit), - // Inputs - .clk (clk), - .rst (rst), - .dc_dbus_err_i (dbus_err), - .dc_enable_i (dc_enabled), - .dc_access_i (dc_access), .cpu_dat_i (lsu_sdat), - .cpu_adr_i (dc_adr), - .cpu_adr_match_i (dc_adr_match), + .cpu_adr_i (dc_adr), // index addr - exec stage vaddr + .cpu_adr_match_i (dc_adr_match), // tag addr - ctrl stage paddr .cpu_req_i (dc_req), .cpu_we_i (dc_we), .cpu_bsel_i (dc_bsel), - .refill_allowed (dc_refill_allowed), - .wradr_i (dbus_adr), - .wrdat_i (dbus_dat_i), - .we_i (dbus_ack_i), - .snoop_valid_i (snoop_valid), - );*/ - mor1kx_dcache - #( - .OPTION_OPERAND_WIDTH(OPTION_OPERAND_WIDTH), - .OPTION_DCACHE_BLOCK_WIDTH(OPTION_DCACHE_BLOCK_WIDTH), - .OPTION_DCACHE_SET_WIDTH(OPTION_DCACHE_SET_WIDTH), - .OPTION_DCACHE_WAYS(OPTION_DCACHE_WAYS), - .OPTION_DCACHE_LIMIT_WIDTH(OPTION_DCACHE_LIMIT_WIDTH), - .OPTION_DCACHE_SNOOP(OPTION_DCACHE_SNOOP) - ) - mor1kx_dcache - (/*AUTOINST*/ - // Outputs - .refill_o (dc_refill), // Templated - .refill_req_o (dc_refill_req), // Templated - .refill_done_o (dc_refill_done), // Templated - .cache_hit_o (dc_hit_o), // Templated - .cpu_err_o (dc_err), // Templated - .cpu_ack_o (dc_ack), // Templated - .cpu_dat_o (dc_ldat), // Templated - .snoop_hit_o (dc_snoop_hit), // Templated - .spr_bus_dat_o (spr_bus_dat_dc_o), // Templated - .spr_bus_ack_o (spr_bus_ack_dc_o), // Templated - // Inputs - .clk (clk), // Templated - .rst (rst), // Templated - .dc_dbus_err_i (dbus_err), // Templated - .dc_enable_i (dc_enabled), // Templated - .dc_access_i (dc_access), // Templated - .cpu_dat_i (lsu_sdat), // Templated - .cpu_adr_i (dc_adr), // Templated - .cpu_adr_match_i (dc_adr_match), // Templated - .cpu_req_i (dc_req), // Templated - .cpu_we_i (dc_we), // Templated - .cpu_bsel_i (dc_bsel), // Templated - .refill_allowed (dc_refill_allowed), // Templated - .wradr_i (dbus_adr), // Templated - .wrdat_i (dbus_dat_i), // Templated - .we_i (dbus_ack_i), // Templated .snoop_adr_i (snoop_adr_i[31:0]), - .snoop_valid_i (snoop_valid), // Templated + .snoop_valid_i (snoop_valid), + .snoop_hit_o (dc_snoop_hit), + + .spr_bus_dat_o (spr_bus_dat_dc_o), + .spr_bus_ack_o (spr_bus_ack_dc_o), .spr_bus_addr_i (spr_bus_addr_i[15:0]), .spr_bus_we_i (spr_bus_we_i), .spr_bus_stb_i (spr_bus_stb_i), @@ -775,6 +787,8 @@ end else begin assign dc_snoop_hit = 0; assign dc_hit_o = 0; assign dc_ldat = 0; + assign spr_bus_dat_dc_o = 0; + assign spr_bus_ack_dc_o = 0; end endgenerate @@ -797,27 +811,6 @@ if (FEATURE_DMMU!="NONE") begin : dmmu_gen assign dmmu_enable = dmmu_enable_i & !pipeline_flush_i; - /* mor1kx_dmmu AUTO_TEMPLATE ( - .enable_i (dmmu_enable), - .phys_addr_o (dmmu_phys_addr), - .cache_inhibit_o (dmmu_cache_inhibit), - .op_store_i (ctrl_op_lsu_store_i), - .op_load_i (ctrl_op_lsu_load_i), - .tlb_miss_o (tlb_miss), - .pagefault_o (pagefault), - .tlb_reload_req_o (tlb_reload_req), - .tlb_reload_busy_o (tlb_reload_busy), - .tlb_reload_addr_o (tlb_reload_addr), - .tlb_reload_pagefault_o (tlb_reload_pagefault), - .tlb_reload_ack_i (tlb_reload_ack), - .tlb_reload_data_i (tlb_reload_data), - .tlb_reload_pagefault_clear_i (tlb_reload_pagefault_clear), - .spr_bus_dat_o (spr_bus_dat_dmmu_o), - .spr_bus_ack_o (spr_bus_ack_dmmu_o), - .spr_bus_stb_i (dmmu_spr_bus_stb), - .virt_addr_i (virt_addr), - .virt_addr_match_i (ctrl_lsu_adr_i), - ); */ mor1kx_dmmu #( .FEATURE_DMMU_HW_TLB_RELOAD(FEATURE_DMMU_HW_TLB_RELOAD), @@ -826,7 +819,7 @@ if (FEATURE_DMMU!="NONE") begin : dmmu_gen .OPTION_DMMU_WAYS(OPTION_DMMU_WAYS) ) mor1kx_dmmu - (/*AUTOINST*/ + ( // Outputs .phys_addr_o (dmmu_phys_addr), // Templated .cache_inhibit_o (dmmu_cache_inhibit), // Templated @@ -841,26 +834,30 @@ if (FEATURE_DMMU!="NONE") begin : dmmu_gen // Inputs .clk (clk), .rst (rst), - .enable_i (dmmu_enable), // Templated - .virt_addr_i (virt_addr), // Templated - .virt_addr_match_i (ctrl_lsu_adr_i), // Templated - .op_store_i (ctrl_op_lsu_store_i), // Templated - .op_load_i (ctrl_op_lsu_load_i), // Templated + .enable_i (dmmu_enable), + .virt_addr_i (virt_addr), + .virt_addr_match_i (ctrl_lsu_adr_i), + .op_store_i (ctrl_op_lsu_store_i), + .op_load_i (ctrl_op_lsu_load_i), .supervisor_mode_i (supervisor_mode_i), - .tlb_reload_ack_i (tlb_reload_ack), // Templated - .tlb_reload_data_i (tlb_reload_data), // Templated - .tlb_reload_pagefault_clear_i (tlb_reload_pagefault_clear), // Templated + .tlb_reload_ack_i (tlb_reload_ack), + .tlb_reload_data_i (tlb_reload_data), + .tlb_reload_pagefault_clear_i (tlb_reload_pagefault_clear), .spr_bus_addr_i (spr_bus_addr_i[15:0]), .spr_bus_we_i (spr_bus_we_i), - .spr_bus_stb_i (dmmu_spr_bus_stb), // Templated + .spr_bus_stb_i (dmmu_spr_bus_stb), .spr_bus_dat_i (spr_bus_dat_i[OPTION_OPERAND_WIDTH-1:0])); end else begin assign dmmu_cache_inhibit = 0; + assign dmmu_phys_addr = 0; assign tlb_miss = 0; + assign tlb_reload_addr = 0; assign pagefault = 0; assign tlb_reload_busy = 0; assign tlb_reload_req = 0; assign tlb_reload_pagefault = 0; + assign spr_bus_dat_dmmu_o = 0; + assign spr_bus_ack_dmmu_o = 0; end endgenerate @@ -875,7 +872,8 @@ endgenerate `define ASSUME assert `endif - reg f_past_valid; + reg f_past_valid; + initial f_past_valid = 1'b0; initial assume (rst); @@ -883,295 +881,325 @@ endgenerate f_past_valid <= 1'b1; always @(*) if (!f_past_valid) - assume (rst); + assume (rst); //------------Assumptions on Inputs------------- -`ifdef LSU - always @(posedge clk) begin - if (f_past_valid && $past(exec_op_lsu_load_i) && !$past(rst) - && $past(padv_ctrl_i) && !$past(pipeline_flush_i) && !rst) - assume (ctrl_op_lsu_load_i); - if (f_past_valid && $past(exec_op_lsu_store_i) && !$past(rst) - && $past(padv_ctrl_i) && !$past(pipeline_flush_i) && !rst) - assume (ctrl_op_lsu_store_i); - if (f_past_valid && $past(exec_op_lsu_atomic_i) && !$past(rst) - && $past(padv_ctrl_i) && !$past(pipeline_flush_i) && !rst) - assume (ctrl_op_lsu_atomic_i); - end -`endif - always @(posedge clk) begin - if (f_past_valid && !$past(rst)) begin - `ASSUME ($onehot0({exec_op_lsu_load_i, exec_op_lsu_store_i})); - `ASSUME ($onehot0({ctrl_op_lsu_store_i, ctrl_op_lsu_load_i})); + if (f_past_valid) begin + `ASSUME ($onehot0({exec_op_lsu_load_i, + exec_op_lsu_store_i})); + `ASSUME ($onehot0({ctrl_op_lsu_load_i, + ctrl_op_lsu_store_i, + ctrl_op_msync_i, + spr_bus_stb_i})); + + // For induction: Exceptions will clear the control + // signals after 2 clock cycles. 1 To register in + // execute stage 1 to register in control stage. + if ($past(pipeline_flush_i) | $past(except_dbus, 2)) begin + assert (!ctrl_op_lsu_load_i); + assert (!ctrl_op_lsu_store_i); + assert (!ctrl_op_lsu_atomic_i); + + `ASSUME (!ctrl_op_lsu_load_i); + `ASSUME (!ctrl_op_lsu_store_i); + `ASSUME (!ctrl_op_lsu_atomic_i); + end end end //-------------------Assertions----------------- -//------------------LSU Properties-------------- - - //Based on ctrl_lsu_adr_i, requested data is put on output port of LSU - always @(*) - casex ({ctrl_lsu_zext_i, ctrl_lsu_length_i, ctrl_lsu_adr_i[1:0]}) - 5'b11x00: assert (lsu_result_o == lsu_ldat); - 5'b10011: assert (lsu_result_o == {24'd0, lsu_ldat[7:0]}); - 5'b10110: assert (lsu_result_o == {16'd0, lsu_ldat[15:0]}); - 5'b00011: assert (lsu_result_o == {{24{lsu_ldat[7]}}, lsu_ldat[7:0]}); - 5'b00110: assert (lsu_result_o == {{16{lsu_ldat[15]}}, lsu_ldat[15:0]}); - endcase + always @(*) begin + if (f_past_valid) begin + assert ($onehot0({ctrl_op_lsu_load_i, + ctrl_op_lsu_store_i, + ctrl_op_msync_i, + spr_bus_stb_i})); + + // For induction: If we are in refill state + // dcache should be requesting refill + if (state == DC_REFILL) + a3_req_when_refill: assert (dc_refill_req); + + // The dcache should not request refills while + // disabled. + if (!dc_enabled) + a5_norefill_when_disabled: assert (!dc_refill_req); + + // Similarly if we are in READ or DC_REFILL state we must + // have dbus_req_o asserted. + if (state == READ | state == DC_REFILL) + assert (dbus_req_o); + + assert (state == IDLE | + state == READ | + state == WRITE | + state == DC_REFILL | + state == TLB_RELOAD); + end - always @(*) - if (pipeline_flush_i) - assert (!lsu_except_dpagefault_o && - !lsu_except_dtlb_miss_o && !lsu_except_align_o); + // When we have spr bus write enabled we should also have strobe + // TODO maybe this should be in spr slave. + if (spr_bus_we_i) + `ASSUME (spr_bus_stb_i); - //For exceptions related to dmmu, dmmu should be enabled - always @(*) - if (lsu_except_dtlb_miss_o | lsu_except_dpagefault_o) - assert (dmmu_enable_i); + end - always @(posedge clk) - if (f_past_valid && !$past(rst) && !$past(pipeline_flush_i) - && !$past(padv_execute_i) && $past(dbus_err_i)) - assert (lsu_except_dbus_o); -//---------------LSU SPR Properties----------------------- +//------------------LSU Properties-------------- - always @(posedge clk) - if (spr_bus_ack_dc_o && f_past_valid && !$past(rst) && - FEATURE_DMMU != "NONE" && FEATURE_DATACACHE != "NONE") - assert (!spr_bus_ack_dmmu_o); - //For spr read, dcache shouldn't acknowledge as dcache - // won't support any read requests - always @(posedge clk) - if (dc_access && spr_bus_stb_i && !spr_bus_we_i && - !$past(spr_bus_we_i) && f_past_valid && !$past(rst)) - assert (!spr_bus_ack_dc_o); +`ifdef LSU - always @(posedge clk) - if (f_past_valid && spr_bus_ack_dmmu_o) - assert (spr_bus_we_i | !spr_bus_we_i); + wire f_lsu_stall; + wire [3:0] f_lsu_except; -//---------------DCACHE----------------- + // Similate pipeline stall controlled by LSU same + // as generated by execute_ctrl + assign f_lsu_stall = (|{ctrl_op_lsu_store_i,ctrl_op_lsu_load_i} & !lsu_valid_o) | + ctrl_op_msync_i & msync_stall_o | + spr_bus_stb_i & ~|{spr_bus_ack_dmmu_o,spr_bus_ack_dc_o}; - //Load - //Case 1: If address is found in cache then cache hit is seen immediately - // and data will be muxed to lsudat immediately if dbus_access is low. - (* anyconst *) wire [OPTION_OPERAND_WIDTH-1:0] f_loaded_data; + assign f_lsu_except = {lsu_except_align_o, + lsu_except_dbus_o, + lsu_except_dpagefault_o, + lsu_except_dtlb_miss_o}; - always @(posedge clk) - if (f_past_valid && !$past(rst) && dc_ack && !dc_refill - && dc_enabled && dc_access && ctrl_op_lsu_load_i && - !dbus_access && (dc_ldat == f_loaded_data) - && ctrl_lsu_adr_i[1:0] == 2'd0 && ctrl_lsu_length_i == 2'd3) begin - assert (dc_hit_o); - assert (lsu_ack); - assert (lsu_valid_o); - assert (lsu_ldat == f_loaded_data); - assert (lsu_result_o == f_loaded_data); - end + // Drive inputs as per how the CPU control unit would drive + // the inputs. + always @(posedge clk) begin - //Case 2: If address is found in cache then cache hit is seen immediately and - // if dbus_access is high, then data is put on output port as soon as dbus_access goes low. + // Assume dmmu is disabled if your address is not setup + assume (dmmu_enable_i == 0); + // This causes dcache to complain keep on for now + assume (dc_enable_i); - always @(posedge clk) - if (f_past_valid && !$past(rst) && $past(dc_ack) && !$past(dc_refill) - && $past(dc_enabled) && $past(dc_access) && $past(ctrl_op_lsu_load_i) - && ctrl_op_lsu_load_i && $past(dbus_access) && !$past(rst,2) && $past(state != WRITE) && - $past(dc_ldat) == f_loaded_data && !$past(dbus_ack) && (dc_ldat == f_loaded_data) - && !dbus_access) begin - assert($past(dc_hit_o)); - assert(!$past(lsu_ack)); - assert(lsu_ack); - assert ($stable(lsu_ldat)); - assert(lsu_ldat == f_loaded_data); + if (!dbus_req_o) begin + assume (!dbus_ack_i); + assume (!dbus_err_i); end - //access_done will be high only if lsu_ack is high in previous clock - always @(posedge clk) - if (f_past_valid && !$past(rst) && $past(lsu_ack) && !$past(padv_execute_i)) begin - assert (access_done); - assert (lsu_valid_o); + // Each dbus requests is followed by an ack or error + if ($past(dbus_req_o) & dbus_req_o) + assume ($onehot({dbus_ack_i,dbus_err_i})); + + // Control pipeline as per control cappuccino + if (rst) begin + assume (!padv_execute_i); + assume (!padv_ctrl_i); + assume (!exec_op_lsu_load_i); + assume (!exec_op_lsu_store_i); + assume (!ctrl_op_lsu_store_i); + assume (!ctrl_op_lsu_load_i); + assume (!ctrl_op_msync_i); + assume (!spr_bus_stb_i); + end else begin + // Pipeline advance from execute is high whenever a new operation starts + // or the current operation completes, otherwise it can change freely + if (f_lsu_stall) + assume (!padv_execute_i); + else if ($rose(|{exec_op_lsu_load_i,exec_op_lsu_store_i})) + assume ($rose(padv_execute_i)); + else if (|{ctrl_op_lsu_store_i,ctrl_op_lsu_load_i,ctrl_op_msync_i,spr_bus_stb_i}) + assume (padv_execute_i); + + // Pipeline advance control lags pipeline advance execute + // by one clock cycle + assume (padv_ctrl_i == $past(padv_execute_i)); + + // Restrict to the typical case where execute flows to control + if ($past(padv_execute_i)) begin + assume ($past(exec_lsu_adr_i) == ctrl_lsu_adr_i); + assume ($past(exec_op_lsu_store_i) == ctrl_op_lsu_store_i); + assume ($past(exec_op_lsu_load_i) == ctrl_op_lsu_load_i); + assume ($past(exec_op_lsu_atomic_i) == ctrl_op_lsu_atomic_i); + end + + // If execute stage is not advacing signals are stable + if (padv_execute_i == 0) begin + assume ($stable({exec_op_lsu_load_i, + exec_op_lsu_store_i, + exec_op_lsu_atomic_i, + exec_lsu_adr_i})); + end + + // If control stage is not advacing singals are stable + if (padv_ctrl_i == 0) begin + assume ($stable({ctrl_op_lsu_load_i, + ctrl_op_lsu_store_i, + ctrl_op_msync_i, + ctrl_lsu_zext_i, + ctrl_lsu_length_i, + ctrl_op_lsu_atomic_i, + ctrl_lsu_adr_i, + ctrl_rfb_i, + ctrl_epcr_i})); + end end - - /*/Fail: dmmu_cache_inhibit fails to inhibit dcache - always @(posedge clk) - if (dmmu_cache_inhibit && f_past_valid && !$past(rst) && !ctrl_op_lsu_store_i) - assert (!dc_access);*/ - - always @(*) begin - if (dbus_burst_o) - assert (state == DC_REFILL); - if (dbus_access) - assert (state != DC_REFILL); - end - -//----------------------DATA BUS----------------------------- -//Walk through memory load access - - (* anyconst *) wire [OPTION_OPERAND_WIDTH-1:0] f_adr; - reg f_track_state = 0; - initial f_track_state = 0; - always @(posedge clk) begin - - if ($past(ctrl_op_lsu_load_i) - && $past(store_buffer_empty) && !$past(dc_refill) && !$past(dbus_ack) - && !$past(dbus_err) && !$past(except_dbus) && !$past(access_done) && $past(dbus_access) - && !$past(pipeline_flush_i) && !$past(tlb_reload_req) && !$past(dmmu_enable_i) - && !$past(except_align) && $past(ctrl_lsu_adr_i) == f_adr && f_past_valid && state == IDLE - && !$past(rst) && $past(rst,2)) begin - assert (dbus_req_o); - assert (state == READ); - assert (dbus_adr == f_adr); - f_track_state <= 1; - end - - if ($rose(f_track_state) && f_past_valid && $past(dbus_dat_i) == f_loaded_data - && $past(dbus_ack_i) && !$past(rst)) begin - assert (dbus_dat_o == f_loaded_data); - assert (dbus_ack); - assert (lsu_ack); - assert (lsu_valid_o); - assert (!dbus_burst_o); - end end - always @(posedge clk) - if (f_past_valid && dbus_req_o && !$past(rst)) - assert (state != IDLE); - -//----------------------LSU ACKS------------------------ -//This code snippet checks if all store and load requests -//are acknowledged by lsu unit.Some load requests could be -//fulfilled immediately and some requests leads to refilling -//which might take maximum of 8 clock cycles to acknowledge. - - //Counts load requests - reg [5:0]f_ld_reqs; - initial f_ld_reqs = 0; - //Counts store_requests - reg [5:0]f_st_reqs; - initial f_st_reqs = 0; - - always @(posedge clk) - if (rst || pipeline_flush_i) begin - f_ld_reqs <=0; - f_st_reqs <=0; - end - else if (ctrl_op_lsu_load_i) - f_ld_reqs <=f_ld_reqs+1; - else if (ctrl_op_lsu_store_i) - f_st_reqs <=f_st_reqs +1; - - //Counts acknowledgements - reg [5:0]f_lsu_acks; - initial f_lsu_acks = 0; - - always @(posedge clk) begin - if (rst || pipeline_flush_i) - f_lsu_acks <=0; - else if (lsu_valid_o && lsu_ack) - f_lsu_acks<= f_lsu_acks +1; - end + // Track pending operations + localparam F_COUNT_WIDTH = 5; + localparam F_COUNT_START = 5'd16; + localparam F_COUNT_RESET = {F_COUNT_WIDTH{1'b1}}; + + wire f_spr_here; + wire f_spr_dmmu; + wire f_spr_dcache; + + reg [F_COUNT_WIDTH-1:0] f_op_count; + reg f_msync_pending; + reg f_lsu_pending; + reg f_spr_pending; + reg f_msync_complete; + reg f_lsu_complete; + reg f_spr_complete; + wire [2:0] f_pending; + wire f_count_reset; + wire f_counting; + +// Generate the SPR signals only if we have enabled the +// modules. +generate + if (FEATURE_DMMU!="NONE") + assign f_spr_dmmu = (spr_bus_addr_i[15:11] == 5'd1 & + |spr_bus_addr_i[10:9]); + else + assign f_spr_dmmu = 0; +endgenerate - //Critical path taken by lsu_ack while refilling is 8 clk cycles. - //To assert completed requests f_no_ips is used to make sure no - // new requests arise during refilling. - reg [5:0] f_no_ips; - initial f_no_ips = 0; +generate + if (FEATURE_DATACACHE!="NONE") + assign f_spr_dcache = spr_bus_we_i & + (spr_bus_addr_i == `OR1K_SPR_DCBFR_ADDR | + spr_bus_addr_i == `OR1K_SPR_DCBIR_ADDR); + else + assign f_spr_dcache = 0; +endgenerate - always @(posedge clk) - if (rst || pipeline_flush_i) - f_no_ips <=0; - else if (f_past_valid && !ctrl_op_lsu && !$past(ctrl_op_lsu) - && !$past(rst) && !$past(pipeline_flush_i) && !pipeline_flush_i) - f_no_ips <= f_no_ips + 1; + assign f_spr_here = f_spr_dmmu | f_spr_dcache; - //Assert acks are sum of load and store requests - always @(posedge clk) - if (f_past_valid && !$past(rst) && $rose(f_no_ips) == 8) - assert (f_lsu_acks == f_ld_reqs + f_st_reqs); + assign f_pending = {f_lsu_pending, f_spr_pending, f_msync_pending}; -//----------------Store buffer Properties--------------------- + assign f_count_reset = &f_op_count; + assign f_counting = !f_count_reset; - //Don't read from store buffer if store buffer is empty - always @(posedge clk) - if (store_buffer_empty && !store_buffer_write - && f_past_valid && !$past(rst)) - assert (!store_buffer_read); + // Basic cases we need to help simulate + // 1. SPR ops, DCACHE/MMU + // 2. LSU Read/Write + // + // 1, 2 and 3 cannot happen at the same time. + // Read and Write are only possible after invalidation. + // Read may trigger a refill. - //Assert store buffer can't be empty and full at the same time - always @(*) - if (store_buffer_full) - assert (!store_buffer_empty); + // Used to confirm invalidation/read/write complete + initial f_op_count = F_COUNT_RESET; - //No write when store buffer is full - always @(*) - if (store_buffer_full) - assert (!store_buffer_write); + initial f_msync_pending = 0; + initial f_lsu_pending = 0; + initial f_spr_pending = 0; + initial f_msync_complete = 0; + initial f_lsu_complete = 0; + initial f_spr_complete = 0; - //Store buffer ack implies buffer write was successful - always @(*) - if (store_buffer_ack) - assert (store_buffer_write); + // Lock out invalid inputs + always @(posedge clk) begin + if (|f_pending) begin + assume ($stable({spr_bus_stb_i, + spr_bus_we_i, + spr_bus_addr_i, + spr_bus_dat_i})); + end - always @(posedge clk) - if (f_past_valid && !$past(rst) && !$past(pipeline_flush_i) - && $past(dbus_err_i) && $past(dbus_we_o)) - assert (store_buffer_err_o); - - //Walk through store buffer - (* anyconst *) wire [OPTION_OPERAND_WIDTH-1:0] f_pc; - (* anyconst *) wire [OPTION_OPERAND_WIDTH-1:0] f_wadr; - (* anyconst *) reg [OPTION_OPERAND_WIDTH-1:0] f_dat_i; - (* anyconst *) wire [3:0] f_bsel; - reg f_stored; - initial f_stored = 0; - - //Queing incoming store info in buffer. - always @(posedge clk) - if (f_past_valid && !$past(rst) && (ctrl_epcr_i == f_pc) - && store_buffer_wadr == f_wadr && f_dat_i == lsu_sdat - && dbus_bsel == f_bsel && !ctrl_op_lsu_atomic_i && - store_buffer_write && store_buffer_empty) - //Buffer has one entry - f_stored <= 1; + if (f_lsu_pending) begin + assert (!spr_bus_stb_i); + assert ($onehot({ctrl_op_lsu_load_i,ctrl_op_lsu_store_i})); + end + if (f_msync_pending) begin + assert (!ctrl_op_lsu_load_i); + assert (!ctrl_op_lsu_store_i); + end - always @(posedge clk) - if (f_past_valid && store_buffer_radr == f_wadr && !$past(rst) - && $rose(f_stored) && $past(store_buffer_read) && !rst) begin - assert (store_buffer_dat == f_dat_i); - assert (store_buffer_epcr_o == f_pc); - assert (store_buffer_bsel == f_bsel); - assert (!store_buffer_atomic); - //Poping this entry, makes buffer empty - assert (store_buffer_empty); + a0_one_op_pending: assert ($onehot0(f_pending)); + + // Induction helpers + + // If we are working we should be doing something + if (f_lsu_pending & + $past(f_lsu_pending) & + $past(f_lsu_pending,2) & + $past(f_lsu_pending,3) & + $past(f_lsu_pending,4)) begin + a3_work_while_pending: assert (!(state == IDLE && + ($past(state) == IDLE) && + ($past(state,2) == IDLE) && + ($past(state,3) == IDLE) && + ($past(state,4) == IDLE))); end - //Writing all queued stores is completed if last buffer data is written - always @(posedge clk) - if (f_past_valid && !$past(rst) && write_done && !$past(dbus_err_i)) - assert ($past(last_write)); + // If spr is pending a request should be in progress + if (f_spr_pending) + assert (spr_bus_stb_i & f_spr_here); - //If there are any exceptions then store buffer shouldn't store anything. - always @(*) - if (except_align | except_dbus | except_dtlb_miss | except_dpagefault) begin - assert (!store_buffer_write); - assert (dbus_stall); + // If we have anything pending we must be counting + if (|f_pending) + assert (f_counting); + // And vice versa, if we are counting something should be pending + if (f_counting) + assert (|f_pending); + end + + // Track pending operations + always @(posedge clk) begin + if (f_past_valid & f_count_reset) begin + // If idle check if we can start a transaction + if (spr_bus_stb_i && f_spr_here) begin + f_spr_pending <= 1; + f_op_count <= F_COUNT_START; + end else if (padv_execute_i & + |{exec_op_lsu_store_i,exec_op_lsu_load_i}) begin + f_lsu_pending <= 1; + f_op_count <= F_COUNT_START; + end else if (ctrl_op_msync_i) begin + f_msync_pending <= 1; + f_op_count <= F_COUNT_START; + end + end else if (f_op_count == {F_COUNT_WIDTH{1'b0}}) begin + // If the counter expires check if we have anything pending + a1_lsu_complete: assert (!f_lsu_pending); + a2_spr_complete: assert (!f_spr_pending); + a3_msync_complete: assert (!f_msync_pending); + + f_op_count <= F_COUNT_RESET; + end else if (f_op_count <= F_COUNT_START) + // If we are in counding mode count + f_op_count <= f_op_count - 1; + + // Track completes + if (f_past_valid & f_counting) begin + if ((|f_lsu_except) | + (f_lsu_pending & lsu_valid_o) | + (f_msync_pending & !msync_stall_o) | + (f_spr_pending & |{spr_bus_ack_dmmu_o,spr_bus_ack_dc_o})) begin + f_spr_pending <= 0; + f_lsu_pending <= 0; + f_msync_pending <= 0; + f_op_count <= F_COUNT_RESET; + end end + end - //While refilling don't write store buffer - always @(*) - if (dc_refill) - assert (!store_buffer_write); + // Cover + always @(posedge clk) begin + c0_lsu_load: cover(f_past_valid & f_lsu_pending & + ctrl_op_lsu_load_i & lsu_valid_o); + c1_lsu_store: cover(f_past_valid & f_lsu_pending & + ctrl_op_lsu_store_i & lsu_valid_o); + end - //Don't allow refilling while doing store operation - always @(*) - if (ctrl_op_lsu_store_i || state == WRITE) - assert (!dc_refill_allowed); +`endif // LSU -`endif +`endif // FORMAL endmodule // mor1kx_lsu_cappuccino diff --git a/rtl/verilog/mor1kx_simple_dpram_sclk.v b/rtl/verilog/mor1kx_simple_dpram_sclk.v index ace12355..8fa4ab6c 100644 --- a/rtl/verilog/mor1kx_simple_dpram_sclk.v +++ b/rtl/verilog/mor1kx_simple_dpram_sclk.v @@ -71,34 +71,46 @@ endgenerate `ifdef FORMAL reg f_past_valid; - (* anyconst *) wire [ADDR_WIDTH-1:0] f_addr; - (* anyconst *) reg [DATA_WIDTH-1:0] f_data; + wire f_bypass; initial f_past_valid = 1'b0; always @(posedge clk) f_past_valid <= 1'b1; + assign f_bypass = waddr == raddr && we && re && ENABLE_BYPASS; + `ifdef SDPRAM - reg f_written = 0; - initial f_written = 0; + (* anyconst *) wire [ADDR_WIDTH-1:0] f_addr; + reg [DATA_WIDTH-1:0] f_data; + + initial assume (f_data == mem[f_addr]); + always @(*) + assert(mem[f_addr] == f_data); //Writing f_data at address f_addr always @(posedge clk) - if (f_past_valid && $past(we) && $past(waddr) == f_addr && !ENABLE_BYPASS && $past(din) == f_data) - f_written <= 1; + if (we && waddr == f_addr) + f_data <= din; - //Read access for address f_addr should return f_data + //Read access for the non bypass case always @(posedge clk) - if (f_past_valid && $past(re) && $past(raddr) == f_addr && !ENABLE_BYPASS && $rose(f_written)) - assert (dout == f_data); + if (f_past_valid && $past(re) && $past(raddr == f_addr) + && $past(!f_bypass)) + assert (dout == $past(f_data)); + + always @(posedge clk) begin + c0_write: cover (f_past_valid && we); + c1_read: cover (f_past_valid && re); + c2_bypass: cover (f_past_valid && waddr == raddr && we && re); + end `endif - //Verifying Bypass logic of SDPRAM + //Read access for the bypass case always @(posedge clk) - if (f_past_valid && $past(we) && $past(re) && $past(waddr) == f_addr && $past(raddr) == f_addr && ENABLE_BYPASS) - assert (dout == $past(din)); + if (f_past_valid && $past(f_bypass)) + assert (dout == $past(din)); //Output data should remain unchanged if there is no read enable always @(posedge clk) diff --git a/rtl/verilog/mor1kx_store_buffer.v b/rtl/verilog/mor1kx_store_buffer.v index a80220bf..5c81747d 100644 --- a/rtl/verilog/mor1kx_store_buffer.v +++ b/rtl/verilog/mor1kx_store_buffer.v @@ -102,9 +102,19 @@ module mor1kx_store_buffer assume (rst); localparam f_total_fifo_entries = 2 ** DEPTH_WIDTH; - wire [DEPTH_WIDTH:0]f_curr_fifo_entries; + wire [DEPTH_WIDTH+1:0] f_curr_fifo_entries; + wire [DEPTH_WIDTH+1:0] f_write_idx; + wire f_ptr_cross; + reg f_seen_full; - assign f_curr_fifo_entries = write_pointer - read_pointer; + initial f_seen_full = 0; + + // Writes are always ahead of reads, so to calculate the + // fifo size we need to simulate that. + assign f_ptr_cross = read_pointer > write_pointer; + assign f_write_idx = {f_ptr_cross, write_pointer}; + + assign f_curr_fifo_entries = f_write_idx - read_pointer; //Reset Assertions----------------> always @(posedge clk) @@ -113,62 +123,50 @@ module mor1kx_store_buffer && empty_o && !full_o && (f_curr_fifo_entries == 0)); - //Full FIFO Assertions------------> - //1. When FIFO is full, full flag should be set. - always @(posedge clk `OR_ASYNC_RST) - if (f_past_valid && f_curr_fifo_entries == f_total_fifo_entries) - assert (full_o); + // Input assumptions -------------- + always @(posedge clk `OR_ASYNC_RST) begin + if (f_past_valid) begin + if (full_o && !read_i) + `ASSUME (!write_i); - //2. When fifo has f_total_fifo_entries-1 entries, and - // write_i occurs, then full_o has to be set. - always @(posedge clk) - if (f_past_valid && ($past(f_curr_fifo_entries) == - f_total_fifo_entries - 1) && $past(write_i) && - !$past(read_i) && !$past(rst)) - assert (full_o); - - //2. When FIFO is full, no write_i. - always @(posedge clk) begin - if (f_past_valid && full_o) - `ASSUME (!write_i); + if (empty_o && !write_i) + `ASSUME (!read_i); + end end - //Empty FIFO Assertions----------> - //1. When FIFO has no entries, empty flag has to be set. - always @(posedge clk) - if (f_curr_fifo_entries == 0 && f_past_valid) - assert (empty_o); - - //2. When FIFO has one entry, and read occurs, then empty flag should be set. - always @(posedge clk) - if ($past(f_curr_fifo_entries == 1) && f_past_valid - && $past(read_i) && !$past(write_i)) - assert (empty_o); + // FIFO Assertions ------------ - //3. When FIFO is empty, no read_i. - always @(posedge clk) - if (empty_o && f_past_valid && !write_i) - `ASSUME (!read_i); - - //Empty flag and Full flag can't be 1 at the same time. + // Empty flag and Full flag can't be 1 at the same time. always @(*) - assert ($onehot0({empty_o, full_o})); - - //When FIFO is neither full nor empty, both full and empty flags should be 0. - always @(posedge clk) - if (f_curr_fifo_entries && (f_curr_fifo_entries - < f_total_fifo_entries) && f_past_valid && !$past(rst)) - assert (!full_o && !empty_o); - - //Write pointer should not change when write_i is 0. - always @(posedge clk) - if (f_past_valid && !$past(write_i) && !$past(rst)) - assert ($stable(write_pointer)); - - //Read pointer should not change when read_i is 0. - always @(posedge clk) - if (f_past_valid && !$past(read_i) && !$past(rst)) - assert ($stable(read_pointer)); + a0_full_or_empty: assert ($onehot0({empty_o, full_o})); + + always @(posedge clk `OR_ASYNC_RST) begin + if (rst) + f_seen_full <= 0; + else if (f_past_valid) begin + // When FIFO is full, full flag should be set. + if (f_curr_fifo_entries == f_total_fifo_entries) begin + f_seen_full <= 1; + a1_full: assert (full_o); + end + + // When FIFO has no entries, empty flag has to be set. + if (f_curr_fifo_entries == 0) + a2_empty: assert (empty_o); + + a3_max_depth: assert (f_curr_fifo_entries <= f_total_fifo_entries); + end + end -`endif +`ifdef BUFFER + // FIFO Cover ------------ + always @(posedge clk `OR_ASYNC_RST) begin + if (f_past_valid) begin + cover ($past(write_i) && full_o); + cover (f_seen_full && empty_o); + cover ($past(read_i) && f_ptr_cross); + end + end +`endif // BUFFER +`endif // FORMAL endmodule diff --git a/rtl/verilog/mor1kx_true_dpram_sclk.v b/rtl/verilog/mor1kx_true_dpram_sclk.v index f6992a3e..b1855adc 100644 --- a/rtl/verilog/mor1kx_true_dpram_sclk.v +++ b/rtl/verilog/mor1kx_true_dpram_sclk.v @@ -71,66 +71,77 @@ module mor1kx_true_dpram_sclk `define ASSUME assert `endif -`ifdef TDPRAM - + // Don't allow write to the same address from both ports always @(*) - `ASSUME (addr_a != addr_b); - - (* anyconst *) wire [ADDR_WIDTH-1:0] f_addr; - (* anyconst *) reg [DATA_WIDTH-1:0] f_data_a; - (* anyconst *) reg [DATA_WIDTH-1:0] f_data_b; + if (we_a & we_b) + `ASSUME (addr_a != addr_b); - reg f_write_a = 0; - initial f_write_a = 0; - reg f_write_b = 0; - initial f_write_b = 0; +`ifdef TDPRAM - always @(posedge global_clock) begin + (* anyconst *) wire [ADDR_WIDTH-1:0] f_addr_a; + (* anyconst *) wire [ADDR_WIDTH-1:0] f_addr_b; + + reg [DATA_WIDTH-1:0] f_data_a; + reg [DATA_WIDTH-1:0] f_data_ab; // a port writes to b address + reg [DATA_WIDTH-1:0] f_data_b; + reg [DATA_WIDTH-1:0] f_data_ba; // b port writes to a address + + // Setup properties for confirming memory + initial f_data_ab = 0; + initial f_data_ba = 0; + initial assume (f_data_a == mem[f_addr_a]); + initial assume (f_data_b == mem[f_addr_b]); + always @(*) begin + assert (f_data_a == mem[f_addr_a] | f_data_ba == mem[f_addr_a]); + assert (f_data_b == mem[f_addr_b] | f_data_ab == mem[f_addr_b]); + end - if ($rose(clk_a)) begin - //Port A: Writing f_data_a at address f_addr - if ($past(we_a) && $past(addr_a) == f_addr && $past(din_a) == f_data_a && f_past_valid) begin - assert (dout_a == f_data_a); - f_write_a <= 1; - end - //Port A: Reading data from address f_addr - if (!$past(we_a) && $past(addr_a) == f_addr && f_past_valid && $rose(f_write_a)) - assert (dout_a == f_data_a); - end + // Track writes and reads to port A + always @(posedge clk_a) begin + // Port A: Capture writing any data to address f_addr_a + if (we_a && addr_a == f_addr_a) + f_data_a <= din_a; + + // Port A: Capture writing any data to address f_addr_b + // this may show up on port B + if (we_a && addr_a == f_addr_b) + f_data_ab <= din_a; + + //Port A: When reading or writing we always get our data on dout + // the data may be written from port A or port B + if ($rose(clk_a) && $past(addr_a) == f_addr_a) + assert (dout_a == f_data_a | dout_a == f_data_ba); + end - if ($rose(clk_b)) begin - //Port B: Writing f_data_b at address f_addr - if ($past(we_b) && $past(addr_b) == f_addr && $past(din_b) == f_data_b && f_past_valid) begin - assert (dout_b == f_data_b); - f_write_b <= 1; - end - //Port B: Writing f_data_b at address f_addr - if (!$past(we_b) && $past(addr_b) == f_addr && f_past_valid && $rose(f_write_b)) - assert (dout_b == f_data_b); - end + // Track writes and reads to port B + always @(posedge clk_b) begin + // Port B: Capture writing any data to address f_addr_b + if (we_b && addr_b == f_addr_b) + f_data_b <= din_b; + + // Port B: Capture writing any data to address f_addr_a + // this may show up on port A + if (we_b && addr_b == f_addr_a) + f_data_ba <= din_b; + + // Port B: When reading or writing we always get our data on dout + // the data may be written from port A or port B + if ($rose(clk_b) && $past(addr_b) == f_addr_b) + assert (dout_b == f_data_b | dout_b == f_data_ab); end + always @(posedge global_clock) begin + c0_write_a: cover property (f_past_valid && $rose(clk_a) && + $past(we_a) && $past(addr_a) == f_addr_a); + c1_read_a: cover property (f_past_valid && $rose(clk_a) && + !$past(we_a) && $past(addr_a) == f_addr_a); + + c2_write_b: cover property (f_past_valid && $rose(clk_b) && + $past(we_b) && $past(addr_b) == f_addr_b); + c3_read_b: cover property (f_past_valid && $rose(clk_b) && + !$past(we_b) && $past(addr_b) == f_addr_b); + end `endif - //Port A output data changes only if there is read or write access at port A - always @(posedge clk_a) - if (f_past_valid && $changed(dout_a)) - assert ($past(we_a) | !$past(we_a)); - - //Port B output data changes only if there is read or write access at port B - always @(posedge clk_b) - if (f_past_valid && $changed(dout_b)) - assert ($past(we_b) | !$past(we_b)); - - //Port B shouldn't be affected by write signals of port A - always @(posedge global_clock) - if (f_past_valid && $rose(clk_a) && $fell(clk_b) && $past(we_a)) - assert ($stable(dout_b)); - - //Port A shouldn't be affected by write signals of port B - always @(posedge global_clock) - if (f_past_valid && $rose(clk_b) && $fell(clk_a) && $past(we_b)) - assert ($stable(dout_a)); - `endif endmodule