Merge pull request #147 from stffrdhrn/or1k-linux-failing

Revert "dcache: Allow writing during write_pending"

.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

.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: |

bench/formal/.gitignore

@@ -1 +1 @@
-mor1kx_*/
+mor1kx*/

bench/formal/Makefile

@@ -35,7 +35,7 @@ TESTS := mor1kx_cache_lru \
 
 all: $(TESTS)
 clean:
-	rm -rf $(TESTS)
+	rm -rf mor1kx*/
 
 .PHONY: all clean $(TESTS)
 

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

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

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

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