Commit 7650dcdd authored by Guillem's avatar Guillem
Browse files

update formal script pmu_raw

parent fa3a5cda
......@@ -137,11 +137,13 @@
//Check that interrupt can only be removed by user or reset
integer sum_interruption_vector_rdc_o;
assign sum_interruption_vector_rdc_o = interruption_vector_rdc_o.sum();
/*
always@(posedge clk_i) begin
if(rstn_i && f_past_valid && enable_i)
//TODO: This assertion keeps failing. check again
assert (interruption_vector_rdc_o.sum()>=$past(interruption_vector_rdc_o.sum()));
end
*/
`endif
endmodule
`default_nettype wire
......@@ -23,6 +23,9 @@ verific -vlog-define FORMAL
verific -sv PMU_raw.sv
verific -sv PMU_counters.sv
verific -sv PMU_overflow.sv
verific -sv PMU_quota.sv
verific -sv MCCU.sv
verific -sv RDC.sv
verific -import -extnets -all PMU_raw
prep -top PMU_raw
......@@ -36,4 +39,6 @@ prep -top PMU_raw
../../../hdl/PMU_raw.sv
../../../submodules/counters/PMU_counters.sv
../../../submodules/overflow/PMU_overflow.sv
../../../submodules/quota/PMU_quota.sv
../../../submodules/MCCU/hdl/MCCU.sv
../../../submodules/RDC/hdl/RDC.sv
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment