From 17a96c9516323be9022b28070c6a62d16b60f03d Mon Sep 17 00:00:00 2001 From: mike Date: Wed, 3 Jan 2024 14:48:09 -0500 Subject: [PATCH] Flag duplicate properties for future FIXME --- .../tb/uvmt/uvmt_cv32e40p_debug_assert.sv | 19 +++++++++++++++++-- 1 file changed, 17 insertions(+), 2 deletions(-) diff --git a/cv32e40p/tb/uvmt/uvmt_cv32e40p_debug_assert.sv b/cv32e40p/tb/uvmt/uvmt_cv32e40p_debug_assert.sv index 3ffab6661a..a959338c4a 100644 --- a/cv32e40p/tb/uvmt/uvmt_cv32e40p_debug_assert.sv +++ b/cv32e40p/tb/uvmt/uvmt_cv32e40p_debug_assert.sv @@ -116,6 +116,18 @@ module uvmt_cv32e40p_debug_assert else `uvm_error(info_tag,$sformatf("Debug mode with wrong cause after ebreak, case = %d",cov_assert_if.dcsr_q[8:6])); + //////////////////////////////////////////////////////////////////////////// + // FIXME: start + // It appears that the properties "p_cebreak_exception" and + // "p_ebreak_exception" are identical in all but name. However, at + // the time of this writting (2024-01-03) it has been deemed too + // risky to clean this up as the CV32E40P v2.0.0 is driving toward + // closing coverage. + // + // Before conducting any future maintenance of this code, refactor with . + // See GitHub issue #1084. + + // c.ebreak without dcsr.ebreakm results in exception at mtvec // Exclude single stepping as the sequence gets very complicated property p_cebreak_exception; @@ -126,7 +138,7 @@ module uvmt_cv32e40p_debug_assert && (cov_assert_if.mepc_q == pc_at_ebreak) && (cov_assert_if.id_stage_pc == cov_assert_if.mtvec); endproperty - + a_cebreak_exception: assert property(p_cebreak_exception) else `uvm_error(info_tag,$sformatf("Exception not entered correctly after c.ebreak with dcsr.ebreak=0")); @@ -141,13 +153,16 @@ module uvmt_cv32e40p_debug_assert && (cov_assert_if.mepc_q == pc_at_ebreak) && (cov_assert_if.id_stage_pc == cov_assert_if.mtvec); endproperty - + // TODO: Fails formal as above a_ebreak_exception: assert property(p_ebreak_exception) else `uvm_error(info_tag,$sformatf("Exception not entered correctly after ebreak with dcsr.ebreak=0")); // c.ebreak during debug mode results in relaunch of debug mode + // FIXME: end + //////////////////////////////////////////////////////////////////////////// + property p_cebreak_during_debug_mode; $rose(cov_assert_if.is_cebreak) ##0 cov_assert_if.debug_mode_q |-> decode_valid [->2] ##0 cov_assert_if.debug_mode_q && (cov_assert_if.id_stage_pc == halt_addr_at_entry); // TODO should check no change in dpc and dcsr