From afb195f62335654b2fa6d99719695c9087c111ed Mon Sep 17 00:00:00 2001
From: Alban Gruin <alban.gruin@irit.fr>
Date: Tue, 23 Mar 2021 10:27:05 +0100
Subject: [PATCH] verifier: add assert to check for concurrent bus accesses
Signed-off-by: Alban Gruin <alban.gruin@irit.fr>
---
src/verifier.sv | 4 ++++
1 file changed, 4 insertions(+)
diff --git a/src/verifier.sv b/src/verifier.sv
index 80d20591..3d5346bb 100644
--- a/src/verifier.sv
+++ b/src/verifier.sv
@@ -78,6 +78,10 @@ module verifier #(
@(posedge clk_i) disable iff (!rst_ni) commit_ack_i[i] |-> commit_correct[i])
else $warning (1,"Invalid commit");
end
+
+ assert property (
+ @(posedge clk_i) disable iff (!rst_ni) ~should_lock_icache_o)
+ else $warning (1,"Concurrent access on the bus");
`endif
//pragma translate on
--
GitLab