[aes/dv] added idle assert check
Signed-off-by: Rasmus Madsen <rasmus.madsen@wdc.com>
diff --git a/hw/ip/aes/dv/sva/aes_bind.sv b/hw/ip/aes/dv/sva/aes_bind.sv
index fd4f1f7..4febb66 100644
--- a/hw/ip/aes/dv/sva/aes_bind.sv
+++ b/hw/ip/aes/dv/sva/aes_bind.sv
@@ -20,4 +20,12 @@
.d2h (tl_o)
);
+ bind aes aes_idle_check idle_check (
+ .clk_i (clk_i),
+ .rst_ni (rst_ni),
+ .reg2hw (reg2hw),
+ .idle_i (idle_o)
+ );
+
+
endmodule
diff --git a/hw/ip/aes/dv/sva/aes_idle_check.sv b/hw/ip/aes/dv/sva/aes_idle_check.sv
new file mode 100644
index 0000000..b810283
--- /dev/null
+++ b/hw/ip/aes/dv/sva/aes_idle_check.sv
@@ -0,0 +1,24 @@
+// Copyright lowRISC contributors.
+// Licensed under the Apache License, Version 2.0, see LICENSE for details.
+// SPDX-License-Identifier: Apache-2.0
+
+`include "prim_assert.sv"
+
+module aes_idle_check
+ import aes_reg_pkg::*;
+(
+ input logic clk_i,
+ input logic rst_ni,
+ input aes_reg2hw_t reg2hw,
+ input logic idle_i
+ );
+
+
+ logic is_running;
+ logic idle;
+
+ assign idle = (reg2hw.status.idle.q == 1'b1);
+
+ // make sure idle_i always matched the register idle state
+ `ASSERT(IdleNotIdle_A, idle == idle_i);
+endmodule
diff --git a/hw/ip/aes/dv/sva/aes_sva.core b/hw/ip/aes/dv/sva/aes_sva.core
index 9320f48..2db03f4 100644
--- a/hw/ip/aes/dv/sva/aes_sva.core
+++ b/hw/ip/aes/dv/sva/aes_sva.core
@@ -9,8 +9,10 @@
depend:
- lowrisc:tlul:headers
- lowrisc:fpv:csr_assert_gen
+ - lowrisc:ip:aes
files:
- aes_bind.sv
+ - aes_idle_check.sv
file_type: systemVerilogSource
files_formal:
