From 694eea1f13c0c03a12eca3c341432951ffc3f778 Mon Sep 17 00:00:00 2001 From: Henrik Fegran Date: Fri, 18 Aug 2023 14:16:02 +0200 Subject: [PATCH 1/4] Added covers for nmi in debug followed by single stepping with stepie = 0/1 Signed-off-by: Henrik Fegran --- .../tb/uvmt/uvmt_cv32e40s_debug_assert.sv | 37 +++++++++++++++++++ 1 file changed, 37 insertions(+) diff --git a/cv32e40s/tb/uvmt/uvmt_cv32e40s_debug_assert.sv b/cv32e40s/tb/uvmt/uvmt_cv32e40s_debug_assert.sv index 399caa7e5d..ae3c51e114 100644 --- a/cv32e40s/tb/uvmt/uvmt_cv32e40s_debug_assert.sv +++ b/cv32e40s/tb/uvmt/uvmt_cv32e40s_debug_assert.sv @@ -1070,4 +1070,41 @@ module uvmt_cv32e40s_debug_assert end end + sequence dbg_with_nmi_dret_stepie; + rvfi.rvfi_dbg_mode + ##1 + rvfi.is_dret + && rvfi.rvfi_nmip + && csr_dcsr.rvfi_csr_rdata[DCSR_STEPIE_POS] + && csr_dcsr.rvfi_csr_rdata[DCSR_STEP_POS] + && rvfi.rvfi_valid + ##1 + csr_mtvec.rvfi_csr_rdata > 3 // ignore lower bits + && csr_dpc.rvfi_csr_rdata != 0 + && csr_mtvec.rvfi_csr_rdata != csr_dpc.rvfi_csr_rdata + && !rvfi.rvfi_trap.exception + && rvfi.rvfi_valid[->1] + ; + endsequence : dbg_with_nmi_dret_stepie + + sequence dbg_with_nmi_dret_stepie_n; + rvfi.rvfi_dbg_mode + ##1 + rvfi.is_dret + && rvfi.rvfi_nmip + && !csr_dcsr.rvfi_csr_rdata[DCSR_STEPIE_POS] + && csr_dcsr.rvfi_csr_rdata[DCSR_STEP_POS] + && rvfi.rvfi_valid + ##1 + csr_mtvec.rvfi_csr_rdata > 3 // ignore lower bits + && csr_dpc.rvfi_csr_rdata != 0 + && csr_mtvec.rvfi_csr_rdata != csr_dpc.rvfi_csr_rdata + && !rvfi.rvfi_trap.exception + && rvfi.rvfi_valid[->1] + ; + endsequence : dbg_with_nmi_dret_stepie_n + + cov_dbg_with_nmi_dret_stepie: cover property (dbg_with_nmi_dret_stepie); + cov_dbg_with_nmi_dret_stepie_n: cover property (dbg_with_nmi_dret_stepie_n); + endmodule : uvmt_cv32e40s_debug_assert From 961c7cb40d0925b554f170382215226717179b4a Mon Sep 17 00:00:00 2001 From: Henrik Fegran Date: Fri, 18 Aug 2023 14:27:34 +0200 Subject: [PATCH 2/4] Simplified sequences Signed-off-by: Henrik Fegran --- .../tb/uvmt/uvmt_cv32e40s_debug_assert.sv | 25 +++---------------- 1 file changed, 4 insertions(+), 21 deletions(-) diff --git a/cv32e40s/tb/uvmt/uvmt_cv32e40s_debug_assert.sv b/cv32e40s/tb/uvmt/uvmt_cv32e40s_debug_assert.sv index ae3c51e114..8b6b33f6ad 100644 --- a/cv32e40s/tb/uvmt/uvmt_cv32e40s_debug_assert.sv +++ b/cv32e40s/tb/uvmt/uvmt_cv32e40s_debug_assert.sv @@ -1070,13 +1070,13 @@ module uvmt_cv32e40s_debug_assert end end - sequence dbg_with_nmi_dret_stepie; + sequence dbg_with_nmi_dret_stepie(bit stepie_value); rvfi.rvfi_dbg_mode ##1 rvfi.is_dret && rvfi.rvfi_nmip && csr_dcsr.rvfi_csr_rdata[DCSR_STEPIE_POS] - && csr_dcsr.rvfi_csr_rdata[DCSR_STEP_POS] + && csr_dcsr.rvfi_csr_rdata[DCSR_STEP_POS] == stepie_value && rvfi.rvfi_valid ##1 csr_mtvec.rvfi_csr_rdata > 3 // ignore lower bits @@ -1087,24 +1087,7 @@ module uvmt_cv32e40s_debug_assert ; endsequence : dbg_with_nmi_dret_stepie - sequence dbg_with_nmi_dret_stepie_n; - rvfi.rvfi_dbg_mode - ##1 - rvfi.is_dret - && rvfi.rvfi_nmip - && !csr_dcsr.rvfi_csr_rdata[DCSR_STEPIE_POS] - && csr_dcsr.rvfi_csr_rdata[DCSR_STEP_POS] - && rvfi.rvfi_valid - ##1 - csr_mtvec.rvfi_csr_rdata > 3 // ignore lower bits - && csr_dpc.rvfi_csr_rdata != 0 - && csr_mtvec.rvfi_csr_rdata != csr_dpc.rvfi_csr_rdata - && !rvfi.rvfi_trap.exception - && rvfi.rvfi_valid[->1] - ; - endsequence : dbg_with_nmi_dret_stepie_n - - cov_dbg_with_nmi_dret_stepie: cover property (dbg_with_nmi_dret_stepie); - cov_dbg_with_nmi_dret_stepie_n: cover property (dbg_with_nmi_dret_stepie_n); + cov_dbg_with_nmi_dret_stepie: cover property (dbg_with_nmi_dret_stepie(1)); + cov_dbg_with_nmi_dret_stepie_n: cover property (dbg_with_nmi_dret_stepie(0)); endmodule : uvmt_cv32e40s_debug_assert From 66c25d398270b0e67b5981d3a4ba8ed6e44f8f5e Mon Sep 17 00:00:00 2001 From: Henrik Fegran Date: Fri, 18 Aug 2023 14:50:55 +0200 Subject: [PATCH 3/4] Fixed typo Signed-off-by: Henrik Fegran --- cv32e40s/tb/uvmt/uvmt_cv32e40s_debug_assert.sv | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/cv32e40s/tb/uvmt/uvmt_cv32e40s_debug_assert.sv b/cv32e40s/tb/uvmt/uvmt_cv32e40s_debug_assert.sv index 8b6b33f6ad..a0886958a4 100644 --- a/cv32e40s/tb/uvmt/uvmt_cv32e40s_debug_assert.sv +++ b/cv32e40s/tb/uvmt/uvmt_cv32e40s_debug_assert.sv @@ -1075,8 +1075,8 @@ module uvmt_cv32e40s_debug_assert ##1 rvfi.is_dret && rvfi.rvfi_nmip - && csr_dcsr.rvfi_csr_rdata[DCSR_STEPIE_POS] - && csr_dcsr.rvfi_csr_rdata[DCSR_STEP_POS] == stepie_value + && csr_dcsr.rvfi_csr_rdata[DCSR_STEPIE_POS] == stepie_value + && csr_dcsr.rvfi_csr_rdata[DCSR_STEP_POS] && rvfi.rvfi_valid ##1 csr_mtvec.rvfi_csr_rdata > 3 // ignore lower bits From 2ea8901b2f225286d6dc287f37964fb54be6e48c Mon Sep 17 00:00:00 2001 From: Henrik Fegran Date: Mon, 21 Aug 2023 09:36:34 +0200 Subject: [PATCH 4/4] Adressed review feedback Signed-off-by: Henrik Fegran --- .../tb/uvmt/uvmt_cv32e40s_debug_assert.sv | 30 +++++++++++-------- 1 file changed, 18 insertions(+), 12 deletions(-) diff --git a/cv32e40s/tb/uvmt/uvmt_cv32e40s_debug_assert.sv b/cv32e40s/tb/uvmt/uvmt_cv32e40s_debug_assert.sv index a0886958a4..19564ee771 100644 --- a/cv32e40s/tb/uvmt/uvmt_cv32e40s_debug_assert.sv +++ b/cv32e40s/tb/uvmt/uvmt_cv32e40s_debug_assert.sv @@ -1070,24 +1070,30 @@ module uvmt_cv32e40s_debug_assert end end - sequence dbg_with_nmi_dret_stepie(bit stepie_value); + sequence s_dbg_with_nmi_dret_stepie(bit stepie_value); rvfi.rvfi_dbg_mode - ##1 - rvfi.is_dret - && rvfi.rvfi_nmip + && rvfi.is_dret + && rvfi.rvfi_nmip[0] && csr_dcsr.rvfi_csr_rdata[DCSR_STEPIE_POS] == stepie_value && csr_dcsr.rvfi_csr_rdata[DCSR_STEP_POS] && rvfi.rvfi_valid ##1 - csr_mtvec.rvfi_csr_rdata > 3 // ignore lower bits - && csr_dpc.rvfi_csr_rdata != 0 - && csr_mtvec.rvfi_csr_rdata != csr_dpc.rvfi_csr_rdata - && !rvfi.rvfi_trap.exception - && rvfi.rvfi_valid[->1] + rvfi.rvfi_valid[->1] + ; + endsequence : s_dbg_with_nmi_dret_stepie + + property p_dbg_with_nmi_dret_stepie(bit stepie_value); + reject_on( + csr_mtvec.rvfi_csr_rdata[31:2] == 0 // ignore lower bits + || csr_dpc.rvfi_csr_rdata == 0 + || csr_mtvec.rvfi_csr_rdata == csr_dpc.rvfi_csr_rdata + || rvfi.rvfi_trap.exception) + s_dbg_with_nmi_dret_stepie(stepie_value) ; - endsequence : dbg_with_nmi_dret_stepie + endproperty : p_dbg_with_nmi_dret_stepie + - cov_dbg_with_nmi_dret_stepie: cover property (dbg_with_nmi_dret_stepie(1)); - cov_dbg_with_nmi_dret_stepie_n: cover property (dbg_with_nmi_dret_stepie(0)); + cov_dbg_with_nmi_dret_stepie: cover property (p_dbg_with_nmi_dret_stepie(1)); + cov_dbg_with_nmi_dret_stepie_n: cover property (p_dbg_with_nmi_dret_stepie(0)); endmodule : uvmt_cv32e40s_debug_assert