Skip to content

Commit

Permalink
change to stkz_stall logic and simpliied stkz design (no restart)
Browse files Browse the repository at this point in the history
  • Loading branch information
@kliuMsft
kliuMsft committed Sep 13, 2024
1 parent 70d1963 commit eedb0ac
Show file tree
Hide file tree
Showing 6 changed files with 187 additions and 155 deletions.
40 changes: 26 additions & 14 deletions dv/cheriot/fcov/core_ibex_fcov_if.sv
View file
Original file line number Diff line number Diff line change
Expand Up @@ -1113,18 +1113,19 @@ interface core_ibex_fcov_if import ibex_pkg::*; import cheri_pkg::*; import cher
// addr/perm violations. this may cause either tag clearing or exception
cp_cheri_vio: coverpoint {g_cheri_ex.u_cheri_ex.perm_vio_vec, g_cheri_ex.u_cheri_ex.addr_bound_vio} iff
(g_cheri_ex.u_cheri_ex.cheri_exec_id_i) {
wildcard bins bound = {10'b??_????_???1};
wildcard bins tag = {10'b??_????_??1?};
wildcard bins seal = {10'b??_????_?1??};
wildcard bins ex = {10'b??_????_1???};
wildcard bins ld = {10'b??_???1_????};
wildcard bins sd = {10'b??_??1?_????};
wildcard bins sc = {10'b??_?1??_????};
wildcard bins sr = {10'b??_1???_????};
wildcard bins align = {10'b?1_????_????};
wildcard bins slc = {10'b1?_????_????};
wildcard bins bound = {9'b?_????_???1};
wildcard bins tag = {9'b?_????_??1?};
wildcard bins seal = {9'b?_????_?1??};
wildcard bins ex = {9'b?_????_1???};
wildcard bins ld = {9'b?_???1_????};
wildcard bins sd = {9'b?_??1?_????};
wildcard bins sc = {9'b?_?1??_????};
wildcard bins sr = {9'b?_1???_????};
wildcard bins align = {9'b1_????_????};
}

cp_cheri_vio_slc: coverpoint {g_cheri_ex.u_cheri_ex.perm_vio_slc} iff (g_cheri_ex.u_cheri_ex.cheri_exec_id_i);

cp_tag_clear_cs1cd: coverpoint fcov_tag_clear_cs1cd iff
(g_cheri_ex.u_cheri_ex.cheri_exec_id_i);

Expand Down Expand Up @@ -1210,12 +1211,12 @@ interface core_ibex_fcov_if import ibex_pkg::*; import cheri_pkg::*; import cher

cp_mshwm_set: coverpoint g_cheri_ex.u_cheri_ex.csr_mshwm_set_o;

cp_stkz_stall1: coverpoint g_cheri_ex.u_cheri_ex.cpu_stkz_stall1 iff
cp_stkz_stall1: coverpoint g_cheri_ex.u_cheri_ex.cpu_grant_to_stkz_o iff
(g_cheri_ex.u_cheri_ex.cheri_ex_dv_ext_i.fcov_cpu_lsu_req);
cp_stkz_stall0: coverpoint g_cheri_ex.u_cheri_ex.cpu_stkz_stall0 iff
cp_stkz_stall0: coverpoint g_cheri_ex.u_cheri_ex.cpu_stall_by_stkz_o iff
(g_cheri_ex.u_cheri_ex.cheri_ex_dv_ext_i.fcov_cpu_lsu_req);

cp_sktz_err: coverpoint g_cheri_ex.u_cheri_ex.cpu_stkz_err; // abort error (exception)
// cp_sktz_err: coverpoint g_cheri_ex.u_cheri_ex.cpu_stkz_err; // abort error (exception)

cp_clsc_mem_err: coverpoint load_store_unit_i.lsu_dv_ext_i.fcov_clsc_mem_err {
illegal_bins illegal = {7}; // rsvd value
Expand Down Expand Up @@ -1423,6 +1424,11 @@ interface core_ibex_fcov_if import ibex_pkg::*; import cheri_pkg::*; import cher
wildcard ignore_bins igonroe1 = {5'b?11??};
}

cp_rs2_req_len: coverpoint g_cheri_ex.u_cheri_ex.rf_rdata_b {
bins little[] = {[0:8]};
bins other = {[9:$]};
}

cp_rs1_bitsize: coverpoint fcov_rs1_bitsize;

cp_mstatus_mie: coverpoint cs_registers_i.csr_mstatus_mie_o;
Expand Down Expand Up @@ -1864,7 +1870,8 @@ interface core_ibex_fcov_if import ibex_pkg::*; import cheri_pkg::*; import cher
bins bin1 = {1'b1};
}

cheriot_instr_clc_cross0: cross cp_cs1_tag, cp_cs1_sealed, cp_cs1_perms_load, cp_clc_mem_cap_perms, cp_instr_clc;
// QQQ - this is needs to be delayed/crossed with cp_clc_mem_cap*
cheriot_instr_clc_cross0: cross cp_cs1_tag, cp_cs1_sealed, cp_cs1_perms_load, cp_instr_clc;
cheriot_instr_clc_cross1: cross cp_cs1_tag, cp_clsc_bound_cases, cp_cheri_imm12, cp_clsc_addr_lsb, cp_instr_clc;

// CSC
Expand Down Expand Up @@ -1913,6 +1920,11 @@ interface core_ibex_fcov_if import ibex_pkg::*; import cheri_pkg::*; import cher
((!binsof(cp_cs1_exp) intersect {24}) && (binsof(cp_setbounds_cases) with (cp_setbounds_cases %2 == 1)));
}

cheriot_instr_csetbounds_cross1: cross cp_cs1_tag, cp_setbounds_cases, cp_rs2_req_len, cp_cs1_exp, cp_cd_tag, cp_instr_csetbounds {
ignore_bins ignore = (binsof(cp_cs1_tag) intersect {1'b0}) ||
((!binsof(cp_cs1_exp) intersect {24}) && (binsof(cp_setbounds_cases) with (cp_setbounds_cases %2 == 1)));
}

// CSetboundsexact
cp_instr_csetboundsexact: coverpoint cheri_ops[CSET_BOUNDS_EX] iff (g_cheri_ex.u_cheri_ex.cheri_exec_id_i) {
bins bin1 = {1'b1};
Expand Down
128 changes: 88 additions & 40 deletions dv/cheriot/fcov/module_dv_ext.sv
View file
Original file line number Diff line number Diff line change
Expand Up @@ -347,7 +347,7 @@ module ibex_lsu_dv_ext import ibex_pkg::*; import cheri_pkg::*; import cheriot_d
input logic pmp_err_q,
input logic data_pmp_err_i,
input logic cheri_err_q,
input logic resp_is_tbre_q,
input logic req_is_tbre_q,
input cap_rx_fsm_t cap_rx_fsm_q,
input logic data_we_q,
input logic cap_lsw_err_q,
Expand Down Expand Up @@ -462,10 +462,12 @@ module ibex_lsu_dv_ext import ibex_pkg::*; import cheri_pkg::*; import cheriot_d

`ASSERT(IbexLsuFsmIdle, (((ls_fsm_cs == IDLE) && lsu_req_i) |->
(cap_rx_fsm_q==CRX_IDLE) | (cap_rx_fsm_q==CRX_WAIT_RESP2)))

// `ASSERT(IbexLsuMisc1, (req_is_tbre_q == resp_is_tbre_q))
endmodule


////////////////////////////////////////////////////////////////
//////////////////////////////////////////////////////////////////
// cheri_ex
////////////////////////////////////////////////////////////////

Expand Down Expand Up @@ -875,7 +877,8 @@ module cheri_stkz_dv_ext import ibex_pkg::*; import cheri_pkg::*; (
input logic ztop_wr_i,
input logic [31:0] ztop_wdata_i,
input full_cap_t ztop_wfcap_i,
input logic cmd_new,
input logic cmd_new_null,
input logic cmd_new_cap,
input logic cmd_cap_good,
input logic lsu_stkz_req_done_i
);
Expand Down Expand Up @@ -971,20 +974,18 @@ module ibex_core_dv_ext import ibex_pkg::*; import cheri_pkg::*; (

logic outstanding_load_id;
logic outstanding_store_id;
logic cheri_intl_clbc;

assign outstanding_load_id = (id_stage_i.instr_executing & (id_stage_i.lsu_req_dec & ~id_stage_i.lsu_we)) |
(cheri_exec_id & cheri_operator[CLOAD_CAP]);
assign outstanding_store_id = (id_stage_i.instr_executing & id_stage_i.lsu_req_dec & id_stage_i.lsu_we) |
(cheri_exec_id & cheri_operator[CSTORE_CAP]);
assign cheri_intl_clbc = cheri_operator[CLOAD_CAP] & ~u_ibex_core.CheriPPLBC & cheri_tsafe_en_i;

if (u_ibex_core.WritebackStage) begin : gen_wb_stage
// When the writeback stage is present a load/store could be in ID or WB. A Load/store in ID can
// see a response before it moves to WB when it is unaligned otherwise we should only see
// a response when load/store is in WB.
assign outstanding_load_resp = outstanding_load_wb |
(outstanding_load_id & (load_store_unit_i.split_misaligned_access | cheri_intl_clbc));
(outstanding_load_id & load_store_unit_i.split_misaligned_access );

assign outstanding_store_resp = outstanding_store_wb |
(outstanding_store_id & load_store_unit_i.split_misaligned_access);
Expand Down Expand Up @@ -1091,10 +1092,21 @@ module ibex_core_dv_ext import ibex_pkg::*; import cheri_pkg::*; (
`ifdef FORMAL
// in simulation div and memory access takes too long - could lead in assertion failure
// note load/store could be delayed by TBRE arbitration & memory delay
`ASSERT(FvxIbexAlwaysTerminateID, (instr_valid_id |-> ##[0:15] instr_terminate_id))
`ifndef MODEL_STKZ_STALL_FORMAL
// -- use [0:15] if no STKZ stall
`ASSERT(FvxIbexAlwaysTerminateID, (instr_valid_id |-> ##[0:15] instr_terminate_id))
`ASSERT(FvxIbexInstrIdDone1, (id_stage_i.instr_executing |-> ##[0:15] instr_id_done))
`else
`ASSERT(FvxIbexAlwaysTerminateID, (instr_valid_id |-> ##[0:25] instr_terminate_id))
// worst case -> cpu cload stalled by stkz_active, then an tbre_req (which gets in since
// there is a 1 cycle gap betwen end of stkz stalling and cpu reclaiming memory interface
// (since cheri_ex is using stall_q to optimize memory address timing)
// use [0:15] if no STKZ
`ASSERT(FvxIbexInstrIdDone1, (id_stage_i.instr_executing |-> ##[0:20] instr_id_done))
`endif

`ASSERT(FvxIbexAlwaysClearID, (instr_terminate_id |-> ##[0:5] instr_valid_clear))
`ASSERT(FvxIbexInstrDone0, (instr_id_done |-> (ready_wb & id_stage_i.instr_executing)))
`ASSERT(FvxIbexInstrDone1, (id_stage_i.instr_executing |-> ##[0:15] instr_id_done))
`endif


Expand Down Expand Up @@ -1262,66 +1274,102 @@ module ibex_top_dv_ext import ibex_pkg::*; import cheri_pkg::*; (
// Assumptions defined for formal verification
//////////////////////////////////////////////////////////
`ifdef FORMAL
//
// Constant tie-offs
//
AssumeCfgCheriMode: assume property (cheri_pmode_i == 1'b1);
AssumeCfgTsafe: assume property (cheri_tsafe_en_i == 1'b1);
AssumeCfgNotTestMode: assume property (test_en_i == 1'b0);
AssumeCfgBootAddr: assume property (boot_addr_i == 32'h8000_0000);

AssumeFetchEnable: assume property (fetch_enable_i == 1'b1);

//
// NMI/debug I/O, etc.
//
// NMI causes WillFetch to fail since it keeps interrupting the fetch process
AssumeNoNMI: assume property (irq_nm_i == 1'b0);

// for controller assertion IbexSetExceptionPCOnSpecialReqIfExpected
// enter_debug_mode is not covered by assertion logic right now. QQQ
AssumeNoDebug: assume property (debug_req_i == 1'b0);

//
// Memory interface I/O assumptions
//
logic data_rvalid_exp, instr_rvalid_exp;

always @(posedge clk_i, negedge rst_ni) begin
if (~rst_ni) begin
data_rvalid_exp <= 1'b0;
instr_rvalid_exp <= 1'b0;
end else begin
data_rvalid_exp <= data_req_o & data_gnt_i;
instr_rvalid_exp <= instr_req_o & instr_gnt_i;
end
end

// model the data/instruction interface (gnt/rvalid always comes back after req)
`ifdef MEM_0DLY_FORMAL
AssumeDataIntfNoDly0: assume property (disable iff (~rst_ni) data_req_o |-> data_gnt_i);
AssumeDataIntfNoDly1: assume property (disable iff (~rst_ni) ~data_req_o |-> ~data_gnt_i);
AssumeDataIntfNoDly2: assume property (disable iff (~rst_ni) data_req_o |=> data_rvalid_i);
AssumeDataIntfNoDly3: assume property (disable iff (~rst_ni) ~data_req_o |=> ~data_rvalid_i);

AssumeInstrIntfNoDly0: assume property (disable iff (~rst_ni) instr_req_o |-> instr_gnt_i);
AssumeInstrIntfNoDly1: assume property (disable iff (~rst_ni) ~instr_req_o |-> ~instr_gnt_i);
AssumeInstrIntfNoDly2: assume property (disable iff (~rst_ni) instr_req_o |=> instr_rvalid_i);
AssumeInstrIntfNoDly3: assume property (disable iff (~rst_ni) ~instr_req_o |=> ~instr_rvalid_i);
AssumeDataGntNoDly0: assume property (data_req_o |-> data_gnt_i);
AssumeDataGntNoDly1: assume property (~data_req_o |-> ~data_gnt_i);
//AssumeDataValidNoDly0: assume property (data_req_o |=> data_rvalid_i);
//AssumeDataValidNoDly1: assume property (~data_req_o |=> ~data_rvalid_i);
AssumeDataValid: assume property (data_rvalid_i == data_rvalid_exp);

AssumeInstrGntNoDly0: assume property (instr_req_o |-> instr_gnt_i);
AssumeInstrGntNoDly1: assume property (~instr_req_o |-> ~instr_gnt_i);
// AssumeInstrValidNoDly0: assume property (instr_req_o |=> instr_rvalid_i);
// AssumeInstrValidNoDly1: assume property (~instr_req_o |=> ~instr_rvalid_i);
AssumeInstrValid: assume property (instr_rvalid_i == instr_rvalid_exp);
`else
// assume data_gnt can happen any time, don't constrain it.
// also note, ##2 also proves but run time is longer
AssumeDataIntf0: assume property (data_req_o |-> ##[0:3] data_gnt_i);
AssumeDataIntf1: assume property (data_req_o & data_gnt_i |-> ##1 data_rvalid_i);
AssumeDataIntf2: assume property (~(data_req_o & data_gnt_i) |-> ##1 ~data_rvalid_i);
AssumeDataGnt0: assume property (data_req_o |-> ##[0:2] data_gnt_i);
AssumeDataGnt1: assume property ((~rst_ni|~data_req_o) |-> ~data_gnt_i);
AssumeDataValid: assume property (data_rvalid_i == data_rvalid_exp);
//AssumeDataIntf3: assume property (##1 data_rvalid_i == ~rst_ni & $past (data_req_o & data_gnt_i));
//AssumeDataIntf4: assume property (~rst_ni |-> ~data_rvalid_i);

//`ASSERT(x1, (data_rvalid_i == data_rvalid_exp))

AssumeInstrIntf0: assume property (instr_req_o |-> ##[0:3] instr_gnt_i);
AssumeInstrIntf1: assume property (instr_req_o & instr_gnt_i |=> instr_rvalid_i);
AssumeInstrIntf2: assume property (~(instr_req_o & instr_gnt_i) |=> ~instr_rvalid_i);
AssumeInstrGnt0: assume property (instr_req_o |-> ##[0:3] instr_gnt_i);
AssumeInstrGnt1: assume property ((~rst_ni | ~instr_req_o) |-> ~instr_gnt_i);
AssumeInstrValid: assume property (instr_rvalid_i == instr_rvalid_exp);
//AssumeInstrValid0: assume property ((instr_req_o & instr_gnt_i) |=> instr_rvalid_i);
//AssumeInstrValid1: assume property (~(instr_req_o & instr_gnt_i) |=> ~instr_rvalid_i);
`endif

// for FvxIbexWbWrRegs (tell JPG that resp_valid can only happen if valid instruction in wb_stage)
AssumeWbValid: assume property (disable iff (~rst_ni) u_ibex_core.wb_stage_i.lsu_resp_valid_i |-> u_ibex_core.wb_stage_i.g_writeback_stage.wb_valid_q);

// for controller assertion IbexSetExceptionPCOnSpecialReqIfExpected
// enter_debug_mode is not covered by assertion logic right now. QQQ
// AssumeNoDebug: assume property (u_ibex_core.id_stage_i.controller_i.enter_debug_mode == 1'b0);
AssumeNoDebug: assume property (debug_req_i == 1'b0);

// stkz_stall is not fully understood by FV tool - need better constrains. QQQ
AssumeStkzStall0: assume property (u_ibex_core.g_cheri_ex.u_cheri_ex.cpu_stkz_stall0 == 1'b0);
AssumeStkzStall1: assume property (u_ibex_core.g_cheri_ex.u_cheri_ex.cpu_stkz_stall1 == 1'b0);

// model tbre mmreg interface
`ifdef FETCH_CORRECT_FORMAL
AssumeFetchedInstr: assume property (instr_rdata_i == u_ibex_core.ibex_core_dv_ext_i.instr_data_assumed);
`endif

//
// Model tbre mmreg i/o interface
//
AssumeMMreg0: assume property ($stable(u_ibex_core.cheri_tbre_wrapper_i.g_tbre.cheri_tbre_i.tbre_ctrl.start_addr));
AssumeMmreg1: assume property ($stable(u_ibex_core.cheri_tbre_wrapper_i.g_tbre.cheri_tbre_i.tbre_ctrl.end_addr));
AssumeMmreg2: assume property ($stable(u_ibex_core.cheri_tbre_wrapper_i.g_tbre.cheri_tbre_i.tbre_ctrl.add1wait));

//
// Internal signal assumptions
//

`ifndef MODEL_STKZ_STALL_FORMAL
AssumeStkzStall0: assume property (u_ibex_core.g_cheri_ex.u_cheri_ex.cpu_stall_by_stkz_o == 1'b0);
AssumeStkzStall1: assume property (u_ibex_core.g_cheri_ex.u_cheri_ex.cpu_grant_to_stkz_o == 1'b0);
`else
`ifdef FAST_STKZ_FORMAL
AssumeStkzFast0: assume property (u_ibex_core.cheri_tbre_wrapper_i.g_stkz.cheri_stkz_i.ztop_wdata_i <= u_ibex_core.cheri_tbre_wrapper_i.g_stkz.cheri_stkz_i.ztop_wfcap_i.base32 + 4);
AssumeStkzData1: assume property (u_ibex_core.cheri_tbre_wrapper_i.g_stkz.cheri_stkz_i.ztop_wfcap_i.base32 < 32'hfff_fffc);
`endif
`endif

// div instruction takes too long for the tool to converge
// jasperGold complains about precondition unreachable for this, however without this assumption IbexInstrAlwaysRetireID won't prove
AssumeFastDiv: assume property (disable iff (~rst_ni) u_ibex_core.ex_block_i.gen_multdiv_fast.multdiv_i.div_en_i |-> u_ibex_core.ex_block_i.gen_multdiv_fast.multdiv_i.valid_o);


`ifdef FETCH_CORRECT_FORMAL
AssumeFetchedInstr: assume property (instr_rdata_i == u_ibex_core.ibex_core_dv_ext_i.instr_data_assumed);
`endif

`endif

endmodule
39 changes: 13 additions & 26 deletions rtl/cheri_ex.sv
View file
Original file line number Diff line number Diff line change
Expand Up @@ -84,6 +84,8 @@ module cheri_ex import cheri_pkg::*; #(
output logic [32:0] lsu_wdata_o,
output reg_cap_t lsu_wcap_o,
output logic lsu_sign_ext_o,
output logic cpu_stall_by_stkz_o,
output logic cpu_grant_to_stkz_o,

input logic addr_incr_req_i,
input logic [31:0] addr_last_i,
Expand Down Expand Up @@ -1029,20 +1031,11 @@ module cheri_ex import cheri_pkg::*; #(
//
// muxing in cheri LSU signals with the rv32 signals
//
logic cpu_stkz_stall0, cpu_stkz_stall1;
logic cpu_stkz_err;
assign lsu_req_o = (instr_is_cheri_i ? cheri_lsu_req : rv32_lsu_req_i);
assign cpu_lsu_dec_o = ((instr_is_cheri_i && is_cap) | instr_is_rv32lsu_i);

if (CheriStkZ) begin
// load/store takes 1 cycle when stkz_active
assign lsu_req_o = ~cpu_stkz_stall0 & (instr_is_cheri_i ? cheri_lsu_req : rv32_lsu_req_i);
assign cpu_lsu_dec_o = ~cpu_stkz_stall1 & ((instr_is_cheri_i && is_cap) | instr_is_rv32lsu_i);
end else begin
assign lsu_req_o = (instr_is_cheri_i ? cheri_lsu_req : rv32_lsu_req_i);
assign cpu_lsu_dec_o = ((instr_is_cheri_i && is_cap) | instr_is_rv32lsu_i);

end

assign cpu_lsu_cheri_err = cpu_stkz_err | (instr_is_cheri_i ? cheri_lsu_err : rv32_lsu_err);
assign cpu_lsu_cheri_err = instr_is_cheri_i ? cheri_lsu_err : rv32_lsu_err;
assign cpu_lsu_addr = instr_is_cheri_i ? cheri_lsu_addr : rv32_lsu_addr_i;
assign cpu_lsu_we = instr_is_cheri_i ? cheri_lsu_we : rv32_lsu_we_i;
assign cpu_lsu_wdata = instr_is_cheri_i ? cheri_lsu_wdata : {1'b0, rv32_lsu_wdata_i};
Expand Down Expand Up @@ -1098,10 +1091,10 @@ module cheri_ex import cheri_pkg::*; #(
//

if (CheriStkZ) begin
logic lsu_addr_in_range, stkz_stall_q;
logic lsu_addr_in_stkz_range, stkz_stall_q;

assign lsu_addr_in_range = (cpu_lsu_addr[31:4] >= stkz_base_i[31:4]) &&
(cpu_lsu_addr[31:2] < stkz_ptr_i[31:2]);
assign lsu_addr_in_stkz_range = cpu_lsu_dec_o && (cpu_lsu_addr[31:4] >= stkz_base_i[31:4]) &&
(cpu_lsu_addr[31:2] < stkz_ptr_i[31:2]);

// cpu_lsu_dec_o is meant to be an early hint to help LSU to generate mux selects for
// address/ctrl/wdata (eventually to help timing on those output ports)
Expand All @@ -1117,26 +1110,20 @@ module cheri_ex import cheri_pkg::*; #(
// -- Also, since the cpu_lsu_addr only increments (clc/csc/unaligned) and stkz address
// only decrements, if lsu_addr_in_range = 0 for the 1st word, it will stay 0 for 2nd
// -- Need to ensure stkz design meet those requirements
assign cpu_stkz_stall0 = (instr_first_cycle_i & stkz_active_i & lsu_addr_in_range) | stkz_stall_q;
assign cpu_stkz_stall1 = ~instr_first_cycle_i & stkz_stall_q;
assign cpu_stall_by_stkz_o = stkz_active_i & lsu_addr_in_stkz_range;
assign cpu_grant_to_stkz_o = ~instr_first_cycle_i & stkz_stall_q;

always_ff @(posedge clk_i or negedge rst_ni) begin
if (!rst_ni) begin
stkz_stall_q <= 1'b0;
cpu_stkz_err <= 1'b0;
end else begin
stkz_stall_q <= stkz_active_i & lsu_addr_in_range;
if (lsu_req_done_i)
cpu_stkz_err <= 1'b0;
else if (stkz_abort_i & lsu_addr_in_range & (cheri_lsu_req | rv32_lsu_req_i))
cpu_stkz_err <= 1'b1;
stkz_stall_q <= stkz_active_i & lsu_addr_in_stkz_range;
end
end

end else begin
assign cpu_stkz_stall0 = 1'b0;
assign cpu_stkz_stall1 = 1'b0;
assign cpu_stkz_err = 1'b0;
assign cpu_stall_by_stkz_o = 1'b0;
assign cpu_grant_to_stkz_o = 1'b0;
end

//
Expand Down
Loading

0 comments on commit eedb0ac

Please sign in to comment.