diff --git a/Makefile b/Makefile
index 3e84e6891d42afdd1025cdaaa8ed40f77b0e528a..48269dde4fae4c4a58aafa552b66b647f038296b 100644
--- a/Makefile
+++ b/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))
diff --git a/include/riscv_pkg.sv b/include/riscv_pkg.sv
index 3799734e8e879a5c0b1659ce1123a02b9c19682e..db864f4a567baf8966dbf8711d23be6ee608a30b 100644
--- a/include/riscv_pkg.sv
+++ b/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;
// -----
diff --git a/src/pmp b/src/pmp
deleted file mode 120000
index 2ae9b9f6906d3cdf387a0364d9aaadcaacafada4..0000000000000000000000000000000000000000
--- a/src/pmp
+++ /dev/null
@@ -1 +0,0 @@
-/home/mo/Documents/mixedcriticality/code/iopmp
\ No newline at end of file
diff --git a/src/pmp/.gitignore b/src/pmp/.gitignore
new file mode 100644
index 0000000000000000000000000000000000000000..b255355662125d4c03559b37376f367c0a3d524e
--- /dev/null
+++ b/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
+
diff --git a/src/pmp/Bender.yml b/src/pmp/Bender.yml
new file mode 100644
index 0000000000000000000000000000000000000000..7fede43330d72ab876f47265112df6e329ec8e93
--- /dev/null
+++ b/src/pmp/Bender.yml
@@ -0,0 +1,24 @@
+package:
+ name: pmp
+ authors:
+ - "Moritz Schneider <moritz.schneider@inf.ethz.ch>"
+
+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
\ No newline at end of file
diff --git a/src/pmp/Makefile b/src/pmp/Makefile
new file mode 100644
index 0000000000000000000000000000000000000000..3e6d38f5639912e3293c97e7e96c16a413d048aa
--- /dev/null
+++ b/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
\ No newline at end of file
diff --git a/src/pmp/README.md b/src/pmp/README.md
new file mode 100644
index 0000000000000000000000000000000000000000..e48445b5c9c12f7527de8d390fe2f8705acf693e
--- /dev/null
+++ b/src/pmp/README.md
@@ -0,0 +1,3 @@
+# PMP
+
+This repository houses a purely combinatorial and parametrizable physical memory protection (PMP) unit.
\ No newline at end of file
diff --git a/src/pmp/formal.sby b/src/pmp/formal.sby
new file mode 100644
index 0000000000000000000000000000000000000000..28c822eb9a558a1d8b5b525994af94807c04930b
--- /dev/null
+++ b/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
diff --git a/src/pmp/scripts/dc_compile.tcl b/src/pmp/scripts/dc_compile.tcl
new file mode 100644
index 0000000000000000000000000000000000000000..6ac2d039a69b8b906d59f40f93f559ca401aca41
--- /dev/null
+++ b/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
\ No newline at end of file
diff --git a/src/pmp/src/napot_extract.sv b/src/pmp/src/napot_extract.sv
new file mode 100644
index 0000000000000000000000000000000000000000..ad175751330f3e21a572b32d870642b47b408169
--- /dev/null
+++ b/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
\ No newline at end of file
diff --git a/src/pmp/src/pmp.sv b/src/pmp/src/pmp.sv
new file mode 100644
index 0000000000000000000000000000000000000000..af2e550ce418840577f4955dd7306784cf1177f9
--- /dev/null
+++ b/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
diff --git a/src/pmp/src/pmp_entry.sv b/src/pmp/src/pmp_entry.sv
new file mode 100644
index 0000000000000000000000000000000000000000..6ab15e91dcba536d768c2c8c02d1e44ed89e6f94
--- /dev/null
+++ b/src/pmp/src/pmp_entry.sv
@@ -0,0 +1,80 @@
+// 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: single PMP entry
+
+module pmp_entry #(
+ parameter int unsigned XLEN = 64,
+ parameter int unsigned PMP_LEN = 54
+) (
+ // Input
+ input logic [XLEN-1:0] addr_i,
+
+ // Configuration
+ input logic [PMP_LEN-1:0] conf_addr_i,
+ input logic [PMP_LEN-1:0] conf_addr_prev_i,
+ input riscv::pmp_addr_mode_t conf_addr_mode_i,
+
+ // Output
+ output logic match_o
+);
+ logic [3:0] match;
+
+ pmp_tor_entry #(
+ .XLEN(XLEN),
+ .PMP_LEN(PMP_LEN)
+ ) i_pmp_tor_entry(
+ .addr_i,
+ .conf_addr_lo_i (conf_addr_prev_i),
+ .conf_addr_hi_i (conf_addr_i ),
+ .match_o (match[riscv::TOR])
+ );
+
+ pmp_na4_entry #(
+ .XLEN(XLEN),
+ .PMP_LEN(PMP_LEN)
+ ) i_pmp_na4_entry(
+ .addr_i,
+ .conf_addr_i,
+ .match_o (match[riscv::NA4])
+ );
+
+ pmp_napot_entry #(
+ .XLEN(XLEN),
+ .PMP_LEN(PMP_LEN)
+ ) i_pmp_napot_entry(
+ .addr_i,
+ .conf_addr_i,
+ .match_o (match[riscv::NAPOT])
+ );
+
+ assign match[riscv::OFF] = 0;
+
+ always_comb begin
+ unique case (conf_addr_mode_i)
+ riscv::TOR: match_o = match[riscv::TOR];
+ riscv::NA4: match_o = match[riscv::NA4];
+ riscv::NAPOT: match_o = match[riscv::NAPOT];
+ riscv::OFF: match_o = match[riscv::OFF];
+ default: match_o = 0;
+ endcase
+ end
+
+ `ifdef FORMAL
+ always @(*) begin
+ if(conf_addr_mode_i == riscv::OFF) begin
+ assert(match_o == '0);
+ end
+ end
+ `endif
+
+endmodule
\ No newline at end of file
diff --git a/src/pmp/src/pmp_na4_entry.sv b/src/pmp/src/pmp_na4_entry.sv
new file mode 100644
index 0000000000000000000000000000000000000000..d0fd3f58574d26db2cbf9fe63bfa98de62e025c9
--- /dev/null
+++ b/src/pmp/src/pmp_na4_entry.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: NA4 PMP entry
+
+module pmp_na4_entry #(
+ parameter int unsigned XLEN = 64,
+ parameter int unsigned PMP_LEN = 54
+) (
+ input logic [XLEN-1:0] addr_i,
+ input logic [PMP_LEN-1:0] conf_addr_i,
+
+ output logic match_o
+);
+ always_comb begin
+ logic [XLEN-1:0] base;
+ logic [XLEN-1:0] padded_addr;
+ logic [XLEN-1:0] mask;
+
+ mask = '1 << 2;
+ // pad the addr such that size_i lower bits are zero
+ padded_addr = addr_i & mask;
+
+ base = (conf_addr_i << 2) & mask;
+
+ if (padded_addr == base) begin
+ match_o = '1;
+ end else begin
+ match_o = '0;
+ end
+
+ `ifdef FORMAL
+ if (base + 2**2 > base) begin // check for overflow
+ if (match_o == 0) begin
+ assert(addr_i >= base + 2**2 || addr_i < base);
+ end else begin
+ assert(addr_i < base + 2**2 && addr_i >= base);
+ end
+ end else begin
+ if (match_o == 0) begin
+ assert(addr_i - 2**2 >= base || addr_i < base);
+ end else begin
+ assert(addr_i - 2**2 < base && addr_i >= base);
+ end
+ end
+ `endif
+ end
+endmodule
\ No newline at end of file
diff --git a/src/pmp/src/pmp_napot_entry.sv b/src/pmp/src/pmp_napot_entry.sv
new file mode 100644
index 0000000000000000000000000000000000000000..f8145fb3beb5888c2b90cf161469c276f044f117
--- /dev/null
+++ b/src/pmp/src/pmp_napot_entry.sv
@@ -0,0 +1,71 @@
+// 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 PMP entry
+
+module pmp_napot_entry #(
+ parameter int unsigned XLEN = 64,
+ parameter int unsigned PMP_LEN = 54
+) (
+ input logic [XLEN-1:0] addr_i,
+ input logic [PMP_LEN-1:0] conf_addr_i,
+
+ output logic match_o
+);
+ int unsigned size;
+
+ napot_extract #(.PMP_LEN(PMP_LEN)) i_napot_extract (
+ .conf_addr_i,
+ .size_o(size)
+ );
+
+ always_comb begin
+ logic [XLEN-1:0] padded_addr;
+ logic [XLEN-1:0] mask;
+ logic [XLEN-1:0] base;
+
+ mask = '1 << size;
+ // pad the addr such that size_i lower bits are zero
+ padded_addr = addr_i & mask;
+
+ base = (conf_addr_i << 2) & mask;
+
+ if (padded_addr == base) begin
+ match_o = '1;
+ end else begin
+ match_o = '0;
+ end
+
+ end
+
+ `ifdef FORMAL
+ always @(*) begin
+ logic[XLEN-1:0] base_lo;
+ logic[XLEN:0] base_hi;
+ base_lo = (conf_addr_i << 2) & ('1 << size);
+ base_hi = base_lo + 2**size;
+ if (base_hi < base_lo) begin
+ base_hi = '1;
+ end
+ if (size < XLEN) begin
+ if (match_o == 0) begin
+ assert(addr_i >= base_hi || addr_i < base_lo);
+ end else begin
+ assert(addr_i < base_hi && addr_i >= base_lo);
+ end
+ end else begin
+ assert(match_o == 1);
+ end
+ end
+ `endif
+
+endmodule
\ No newline at end of file
diff --git a/src/pmp/src/pmp_tor_entry.sv b/src/pmp/src/pmp_tor_entry.sv
new file mode 100644
index 0000000000000000000000000000000000000000..7e5b74499e04adf181a747fea7f0139a4573e34e
--- /dev/null
+++ b/src/pmp/src/pmp_tor_entry.sv
@@ -0,0 +1,45 @@
+// 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: TOR PMP entry
+
+module pmp_tor_entry #(
+ parameter int unsigned XLEN = 64,
+ parameter int unsigned PMP_LEN = 54
+) (
+ input logic [XLEN-1:0] addr_i,
+ input logic [PMP_LEN-1:0] conf_addr_lo_i,
+ input logic [PMP_LEN-1:0] conf_addr_hi_i,
+
+ output logic match_o
+);
+ logic [XLEN-1:0] addr_lo, addr_hi;
+ assign addr_lo = conf_addr_lo_i << 2;
+ assign addr_hi = conf_addr_hi_i << 2;
+ always_comb begin
+ if (addr_i >= addr_lo && addr_i < addr_hi ) begin
+ match_o = '1;
+ end else begin
+ match_o = '0;
+ end
+ end
+
+ `ifdef FORMAL
+ always @(*) begin
+ if (match_o == 0) begin
+ assert(addr_i >= addr_hi || addr_i < addr_lo);
+ end else begin
+ assert(addr_i < addr_hi || addr_i >= addr_lo);
+ end
+ end
+ `endif
+endmodule
\ No newline at end of file
diff --git a/src/pmp/tb/pmp_napot_entry_tb.sv b/src/pmp/tb/pmp_napot_entry_tb.sv
new file mode 100644
index 0000000000000000000000000000000000000000..c14f064e116f16cde08135fa1a51cb01eb6a98c7
--- /dev/null
+++ b/src/pmp/tb/pmp_napot_entry_tb.sv
@@ -0,0 +1,66 @@
+// 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:
+
+import tb_pkg::*;
+
+module pmp_napot_entry_tb;
+ timeunit 1ns;
+ timeprecision 1ps;
+
+ localparam int unsigned WIDTH = 16;
+ localparam int unsigned PMP_LEN = 13;
+
+ logic[WIDTH-1:0] addr;
+ logic[WIDTH-1:0] base;
+ int unsigned size;
+
+ logic[PMP_LEN-1:0] conf_addr;
+
+ logic out;
+
+ pmp_napot_entry #(.XLEN(WIDTH), .PMP_LEN(PMP_LEN))
+ i_iopmp(
+ .addr_i(addr),
+ .conf_addr_i(conf_addr),
+ .match_o(out)
+ );
+
+ initial begin
+ addr = 16'b00011001_10111010;
+ base = 16'b00011001_10110000;
+ size = 4;
+ conf_addr = P#(.WIDTH(WIDTH), .PMP_LEN(PMP_LEN))::base_to_conf(base, size);
+ assert(conf_addr == 16'b00000110_01101101);
+ #5ns;
+ assert(out == 1);
+ addr = 16'b00011001_10110000;
+ base = 16'b00011001_10100000;
+ size = 4;
+ conf_addr = P#(.WIDTH(WIDTH), .PMP_LEN(PMP_LEN))::base_to_conf(base, size);
+ #5ns;
+ assert(out == 0);
+ addr = 16'b00011001_10111000;
+ base = 16'b00011001_10100000;
+ size = 5;
+ conf_addr = P#(.WIDTH(WIDTH), .PMP_LEN(PMP_LEN))::base_to_conf(base, size);
+ #5ns;
+ assert(out == 1);
+ addr = 16'b00011001_10111000;
+ base = 16'b00011001_10100000;
+ size = 6;
+ conf_addr = P#(.WIDTH(WIDTH), .PMP_LEN(PMP_LEN))::base_to_conf(base, size);
+ #5ns;
+ assert(out == 1);
+ end
+endmodule
\ No newline at end of file
diff --git a/src/pmp/tb/pmp_tb.sv b/src/pmp/tb/pmp_tb.sv
new file mode 100644
index 0000000000000000000000000000000000000000..2d1e508d2e8b9fb0dd52fab0d2af78def04d3121
--- /dev/null
+++ b/src/pmp/tb/pmp_tb.sv
@@ -0,0 +1,99 @@
+// 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:
+
+import pmp_pkg::*;
+import tb_pkg::*;
+
+module pmp_tb;
+ timeunit 1ns;
+ timeprecision 1ps;
+
+ localparam int unsigned WIDTH = 16;
+ localparam int unsigned PMP_LEN = 13;
+ localparam int unsigned NR_ENTRIES = 4;
+
+ logic [WIDTH-1:0] addr;
+ access_t access_type;
+
+ // Configuration
+ logic [NR_ENTRIES-1:0][PMP_LEN-1:0] conf_addr;
+ pmp_conf_t [NR_ENTRIES-1:0] conf;
+
+ // Output
+ logic allow;
+
+ // helper signals
+ logic[WIDTH-1:0] base;
+ int unsigned size;
+
+ pmp #(
+ .XLEN(WIDTH),
+ .PMP_LEN(PMP_LEN),
+ .NR_ENTRIES(NR_ENTRIES)
+ ) i_pmp(
+ .addr_i ( addr ),
+ .access_type_i ( access_type ),
+ .conf_addr_i ( conf_addr ),
+ .conf_i ( conf ),
+ .allow_o ( allow )
+ );
+
+
+ initial begin
+ // set all pmps to disabled initially
+ for (int i = 0; i < NR_ENTRIES; i++) begin
+ conf[i].addr_mode = OFF;
+ end
+
+ // test napot 1
+ addr = 16'b00011001_10111010;
+ access_type = READ;
+
+ // pmp 0
+ base = 16'b00011001_00000000;
+ size = 8;
+ conf_addr[0] = P#(.WIDTH(WIDTH), .PMP_LEN(PMP_LEN))::base_to_conf(base, size);
+ conf[0].addr_mode = NAPOT;
+ conf[0].access_type = READ | WRITE | EXECUTE;
+
+ #5ns;
+ assert(allow == 1);
+
+ // add second PMP entry that disallows
+
+ // pmp 1
+ base = 16'b00011001_10110000;
+ size = 4;
+ conf_addr[1] = P#(.WIDTH(WIDTH), .PMP_LEN(PMP_LEN))::base_to_conf(base, size);
+ conf[1].addr_mode = NAPOT;
+ conf[1].access_type = '0;
+
+ #5ns;
+ assert(allow == 0);
+
+ // add third PMP entry that allows again
+ // should fail since pmp1 disallows
+
+ // pmp 2
+ base = 16'b00011001_10111000;
+ size = 3;
+ conf_addr[2] = P#(.WIDTH(WIDTH), .PMP_LEN(PMP_LEN))::base_to_conf(base, size);
+ conf[2].addr_mode = NAPOT;
+ conf[2].access_type = READ;
+
+ #5ns;
+ assert(allow == 0);
+
+ end
+endmodule
\ No newline at end of file
diff --git a/src/pmp/tb/pmp_tor_entry_tb.sv b/src/pmp/tb/pmp_tor_entry_tb.sv
new file mode 100644
index 0000000000000000000000000000000000000000..381cf864f8192cb0c19e92c7e4b74dfc686a0f54
--- /dev/null
+++ b/src/pmp/tb/pmp_tor_entry_tb.sv
@@ -0,0 +1,58 @@
+// 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:
+
+module pmp_tor_entry_tb;
+ timeunit 1ns;
+ timeprecision 1ps;
+
+ localparam int unsigned WIDTH = 16;
+ localparam int unsigned PMP_LEN = 13;
+
+ logic[WIDTH-1:0] addr;
+ logic[PMP_LEN-1:0] addr_lo;
+ logic[PMP_LEN-1:0] addr_hi;
+
+ logic out;
+
+ pmp_tor_entry #(.XLEN(WIDTH), .PMP_LEN(PMP_LEN))
+ i_iopmp(
+ .addr_i(addr),
+ .conf_addr_lo_i(addr_lo),
+ .conf_addr_hi_i(addr_hi),
+ .match_o(out)
+ );
+
+ initial begin
+ addr = 16'h1a54;
+ addr_lo = 16'h1a53 >> 2;
+ addr_hi = 16'h1a5F >> 2;
+ #5ns;
+ assert(out == 1);
+ addr = 16'h1a54;
+ addr_lo = 16'h1a54 >> 2;
+ addr_hi = 16'h1a5F >> 2;
+ #5ns;
+ assert(out == 1);
+ addr = 16'h1a54;
+ addr_lo = 16'h1a50 >> 2;
+ addr_hi = 16'h1a54 >> 2;
+ #5ns;
+ assert(out == 0);
+ addr = 16'h1a50;
+ addr_lo = 16'h1a54 >> 2;
+ addr_hi = 16'h1a5F >> 2;
+ #5ns;
+ assert(out == 0);
+ end
+endmodule
\ No newline at end of file
diff --git a/src/pmp/tb/tb_pkg.sv b/src/pmp/tb/tb_pkg.sv
new file mode 100644
index 0000000000000000000000000000000000000000..ffd39587a699e587f51c8b159fef4af5131e147b
--- /dev/null
+++ b/src/pmp/tb/tb_pkg.sv
@@ -0,0 +1,36 @@
+// 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:
+
+package tb_pkg;
+
+ class P #(parameter WIDTH=32, parameter PMP_LEN=32);
+ static function logic[PMP_LEN-1:0] base_to_conf(logic[WIDTH-1:0] base, int unsigned size_i);
+ logic[PMP_LEN-1:0] pmp_reg;
+
+ pmp_reg = '0;
+ for (int i = 0; i < WIDTH-2 && i < PMP_LEN; i++) begin
+ if (i+3 > size_i) begin
+ pmp_reg[i] = base[i+2];
+ end else if (i+3 == size_i) begin
+ pmp_reg[i] = 1'b0;
+ end else begin
+ pmp_reg[i] = 1'b1;
+ end
+ end
+
+ return pmp_reg;
+ endfunction
+ endclass
+
+endpackage
\ No newline at end of file