aboutsummaryrefslogtreecommitdiffstats
path: root/picorv32.v
diff options
context:
space:
mode:
Diffstat (limited to 'picorv32.v')
-rw-r--r--picorv32.v9
1 files changed, 9 insertions, 0 deletions
diff --git a/picorv32.v b/picorv32.v
index d95c74f..f2cdce0 100644
--- a/picorv32.v
+++ b/picorv32.v
@@ -460,8 +460,17 @@ module picorv32 #(
if (mem_do_prefetch || mem_do_rinst || mem_do_rdata)
`assert(!mem_do_wdata);
+ if (mem_do_prefetch || mem_do_rinst)
+ `assert(!mem_do_rdata);
+
+ if (mem_do_rdata)
+ `assert(!mem_do_prefetch && !mem_do_rinst);
+
if (mem_do_wdata)
`assert(!(mem_do_prefetch || mem_do_rinst || mem_do_rdata));
+
+ if (mem_state == 2 || mem_state == 3)
+ `assert(mem_valid || mem_do_prefetch);
end
end