pmp: Add pmps and riscv definitions

Flatten PMP repo. Move definitions to `riscv_pkg.sv`.

Makefile

@@ -81,7 +81,6 @@ ariane_pkg := include/riscv_pkg.sv                          \
               include/axi_intf.sv                           \
               tb/ariane_soc_pkg.sv                          \
               include/ariane_axi_pkg.sv                     \
-              src/pmp/include/pmp_pkg.sv                    \
               src/fpu/src/fpnew_pkg.sv                      \
               src/fpu/src/fpu_div_sqrt_mvp/hdl/defs_div_sqrt_mvp.sv
 ariane_pkg := $(addprefix $(root-dir), $(ariane_pkg))

include/riscv_pkg.sv

@@ -528,20 +528,33 @@ package riscv;
     } fcsr_t;
 
     // PMP
-    typedef enum logic [1:0] { 
-        OFF   = 2'b00, 
-        TOR   = 2'b01, 
-        NA4   = 2'b10, 
-        NAPOT = 2'b11 
+    typedef enum logic [1:0] {
+        OFF   = 2'b00,
+        TOR   = 2'b01,
+        NA4   = 2'b10,
+        NAPOT = 2'b11
     } pmp_addr_mode_t;
+
+    // PMP Access Type
+    typedef enum logic [2:0] {
+        ACCESS_NONE  = 3'b000,
+        ACCESS_READ  = 3'b001,
+        ACCESS_WRITE = 3'b010,
+        ACCESS_EXEC  = 3'b100
+    } pmp_access_t;
+
+    typedef struct packed {
+        logic           x;
+        logic           w;
+        logic           r;
+    } pmpcfg_access_t;
+
     // packed struct of a PMP configuration register (8bit)
     typedef struct packed {
         bit             locked;     // lock this configuration
         logic [1:0]     reserved;
         pmp_addr_mode_t addr_mode;  // Off, TOR, NA4, NAPOT
-        logic           x;          // execute
-        logic           w;          // write
-        logic           r;          // read
+        pmpcfg_access_t access_type;
     } pmpcfg_t;
 
     // -----

src/pmp/.gitignore

@@ -0,0 +1,85 @@
+cockpit
+
+# Created by https://www.gitignore.io/api/modelsim,visualstudiocode
+# Edit at https://www.gitignore.io/?templates=modelsim,visualstudiocode
+
+### ModelSim ###
+# ignore ModelSim generated files and directories (temp files and so on)
+[_@]*
+
+# ignore compilation output of ModelSim
+*.mti
+*.dat
+*.dbs
+*.psm
+*.bak
+*.cmp
+*.jpg
+*.html
+*.bsf
+
+# ignore simulation output of ModelSim
+wlf*
+*.wlf
+*.vstf
+*.ucdb
+cov*/
+transcript*
+sc_dpiheader.h
+vsim.dbg
+modelsim.ini
+
+### VisualStudioCode ###
+.vscode/*
+!.vscode/settings.json
+!.vscode/tasks.json
+!.vscode/launch.json
+!.vscode/extensions.json
+
+### VisualStudioCode Patch ###
+# Ignore all local history of files
+.history
+
+# Created by https://www.gitignore.io/api/synopsysvcs
+# Edit at https://www.gitignore.io/?templates=synopsysvcs
+
+### SynopsysVCS ###
+# Waveform formats
+*.vcd
+*.vpd
+*.evcd
+*.fsdb
+
+# Default name of the simulation executable.  A different name can be
+# specified with this switch (the associated daidir database name is
+# also taken from here):  -o <path>/<filename>
+simv
+
+# Generated for Verilog and VHDL top configs
+simv.daidir/
+simv.db.dir/
+
+# Infrastructure necessary to co-simulate SystemC models with
+# Verilog/VHDL models.  An alternate directory may be specified with this
+# switch:  -Mdir=<directory_path>
+csrc/
+
+# Log file - the following switch allows to specify the file that will be
+# used to write all messages from simulation:  -l <filename>
+*.log
+
+# Coverage results (generated with urg) and database location.  The
+# following switch can also be used:  urg -dir <coverage_directory>.vdb
+simv.vdb/
+urgReport/
+
+# DVE and UCLI related files.
+DVEfiles/
+ucli.key
+
+# When the design is elaborated for DirectC, the following file is created
+# with declarations for C/C++ functions.
+vc_hdrs.h
+
+# End of https://www.gitignore.io/api/modelsim,visualstudiocode
+

src/pmp/Bender.yml

@@ -0,0 +1,24 @@
+package:
+  name: pmp
+  authors:
+    - "Moritz Schneider <[email protected]>"
+
+export_include_dirs:
+  - include
+
+sources:
+  # packages
+  - include/pmp_pkg.sv
+  # sources
+  - src/napot_extract.sv
+  - src/pmp_napot_entry.sv
+  - src/pmp_tor_entry.sv
+  - src/pmp_na4_entry.sv
+  - src/pmp_entry.sv
+  - src/pmp.sv
+
+  - target: simulation
+    files:
+      - tb/pmp_napot_entry_tb.sv
+      - tb/pmp_tor_entry_tb.sv
+      - tb/pmp_tb.sv

src/pmp/Makefile

@@ -0,0 +1,31 @@
+# questa library
+library        ?= work
+# Top level module to compile
+top_level      ?= pmp_tb
+# QuestaSim Version
+questa_version ?= 10.7b
+
+compile_flags = +cover -incr -64 -permissive
+sim_flags = -t 1ps -debugdb -voptargs="+acc" -do "run -all; quit" 
+
+src = $(wildcard src/*.sv)
+inc = $(wildcard include/*.sv)
+tb = $(wildcard tb/*.sv)
+
+compile-sim:
+	rm -rf ${library}
+	vlog-${questa_version} -work ${library} ${compile_flags} ${inc}
+	vlog-${questa_version} -work ${library} ${compile_flags} ${src}
+	vlog-${questa_version} -work ${library} ${compile_flags} ${tb}
+
+sim: compile-sim
+	vsim-${questa_version} -c -work ${library} ${sim_flags} ${top_level}
+
+sim-gui:
+	rm -rf ${library}
+	vlog-${questa_version} -work ${library} ${compile_flags} ${src}
+	vlog-${questa_version} -work ${library} ${compile_flags} ${tb}
+	vsim-${questa_version} -work ${library} ${sim_flags} ${top_level}
+
+clean:
+	@rm -rf ${library} transcript vsim.dbg vsim.wlf

src/pmp/README.md

@@ -0,0 +1,3 @@
+# PMP
+
+This repository houses a purely combinatorial and parametrizable physical memory protection (PMP) unit.

src/pmp/formal.sby

@@ -0,0 +1,31 @@
+[options]
+mode prove
+depth 20
+
+[engines]
+smtbmc boolector
+smtbmc z3
+smtbmc yices
+
+[script]
+verific -vlog-incdir ./include
+verific -sv -DFORMAL \
+    pmp_pkg.sv \
+    napot_extract.sv \
+    pmp_napot_entry.sv \
+    pmp_tor_entry.sv \
+    pmp_na4_entry.sv \
+    pmp_entry.sv \
+    pmp.sv
+
+verific -import -all pmp
+prep -flatten -nordff -top pmp
+
+[files]
+include/pmp_pkg.sv
+src/napot_extract.sv
+src/pmp_napot_entry.sv
+src/pmp_tor_entry.sv
+src/pmp_na4_entry.sv
+src/pmp_entry.sv
+src/pmp.sv

src/pmp/scripts/dc_compile.tcl

@@ -0,0 +1,41 @@
+# remove previous library
+sh rm -rf WORK/*
+remove_design -design
+
+# set multithreading
+set disable_multicore_resource_checks true
+set NumberThreads [exec cat /proc/cpuinfo | grep -c processor]
+set_host_options -max_cores $NumberThreads
+
+# This script was generated automatically by bender.
+set search_path_initial $search_path
+set ROOT "/home/scmoritz/Documents/platformsec/iopmp"
+
+set search_path $search_path_initial
+lappend search_path "$ROOT/include"
+
+analyze -format sv \
+    [list \
+        "$ROOT/include/pmp_pkg.sv" \
+        "$ROOT/src/napot_extract.sv" \
+        "$ROOT/src/pmp_napot_entry.sv" \
+        "$ROOT/src/pmp_tor_entry.sv" \
+        "$ROOT/src/pmp_na4_entry.sv" \
+        "$ROOT/src/pmp_entry.sv" \
+        "$ROOT/src/pmp.sv" \
+    ]
+
+set search_path $search_path_initial
+
+elaborate pmp
+
+# Constraints
+set_max_delay -to [all_outputs] 200
+set_max_area 0
+set_load 0.1 [all_outputs]
+set_max_fanout 1 [all_inputs]
+set_fanout_load 8 [all_outputs]
+
+compile_ultra
+
+report_timing

src/pmp/src/napot_extract.sv

@@ -0,0 +1,43 @@
+// Copyright 2019 ETH Zurich and University of Bologna.
+// Copyright and related rights are licensed under the Solderpad Hardware
+// License, Version 0.51 (the "License"); you may not use this file except in
+// compliance with the License.  You may obtain a copy of the License at
+// http://solderpad.org/licenses/SHL-0.51. Unless required by applicable law
+// or agreed to in writing, software, hardware and materials distributed under
+// this License is distributed on an "AS IS" BASIS, WITHOUT WARRANTIES OR
+// CONDITIONS OF ANY KIND, either express or implied. See the License for the
+// specific language governing permissions and limitations under the License.
+//
+// Author: Moritz Schneider, ETH Zurich
+// Date: 2.10.2019
+// Description: NAPOT extract
+
+module napot_extract #(
+    parameter int unsigned PMP_LEN = 54
+) (
+    input logic [PMP_LEN-1:0] conf_addr_i,
+    output int unsigned size_o
+);
+    always_comb begin
+        int unsigned i;
+        for (i = 0; i < PMP_LEN; i++) begin
+            if (conf_addr_i[i] != 1'b1) begin
+                break;
+            end
+        end
+        size_o = i+3;
+
+        `ifdef FORMAL
+        assert(size_o > 2);
+        if (size_o < PMP_LEN) begin
+            assert(conf_addr_i[size_o - 3] == 0);  // check 0 bit that seperates the ones in the end
+        end
+
+        for (i = 0; i < PMP_LEN; i++) begin
+            if (size_o > 3 && i <= size_o - 4) begin
+                assert(conf_addr_i[i] == 1); // check that all the rest are ones
+            end
+        end
+        `endif
+    end
+endmodule

src/pmp/src/pmp.sv

@@ -0,0 +1,57 @@
+// Copyright 2019 ETH Zurich and University of Bologna.
+// Copyright and related rights are licensed under the Solderpad Hardware
+// License, Version 0.51 (the "License"); you may not use this file except in
+// compliance with the License.  You may obtain a copy of the License at
+// http://solderpad.org/licenses/SHL-0.51. Unless required by applicable law
+// or agreed to in writing, software, hardware and materials distributed under
+// this License is distributed on an "AS IS" BASIS, WITHOUT WARRANTIES OR
+// CONDITIONS OF ANY KIND, either express or implied. See the License for the
+// specific language governing permissions and limitations under the License.
+//
+// Author: Moritz Schneider, ETH Zurich
+// Date: 2.10.2019
+// Description: purely combinatorial PMP unit (with extraction for more complex configs such as NAPOT)
+
+module pmp #(
+    parameter int unsigned XLEN = 32,       // rv64: 64
+    parameter int unsigned PMP_LEN = 32,    // rv64: 54
+    parameter int unsigned NR_ENTRIES = 4
+) (
+    // Input
+    input logic [XLEN-1:0] addr_i,
+    input riscv::pmp_access_t access_type_i,
+    // Configuration
+    input logic [NR_ENTRIES-1:0][PMP_LEN-1:0] conf_addr_i,
+    input riscv::pmpcfg_t [NR_ENTRIES-1:0] conf_i,
+    // Output
+    output logic allow_o
+);
+    logic [NR_ENTRIES-1:0] match;
+
+    for (genvar i = 0; i < NR_ENTRIES; i++) begin
+        pmp_entry #(
+            .XLEN(XLEN),
+            .PMP_LEN(PMP_LEN)
+        ) i_pmp_entry(
+            .addr_i           ( addr_i                         ),
+            .conf_addr_i      ( conf_addr_i[i]                 ),
+            .conf_addr_prev_i ( i == 0 ? '0 : conf_addr_i[i-1] ),
+            .conf_addr_mode_i ( conf_i[i].addr_mode            ),
+            .match_o          ( match[i]                       )
+        );
+    end
+
+    always_comb begin
+        allow_o = 1'b1;
+        if (access_type_i == 3'b000) begin
+            allow_o = 1'b0;
+        end else begin
+            for (int j = 0; j < NR_ENTRIES; j++) begin
+                if (match[j]) begin
+                    if ((access_type_i & conf_i[j].access_type) != access_type_i) allow_o &= 1'b0;
+                    else allow_o &= 1'b1;
+                end
+            end
+        end
+    end
+endmodule