Skip to content

Commit

Permalink
Fix syntax error by applying .triggered for VALID_JAL
Browse files Browse the repository at this point in the history
When performing logical operation on sequence, we must use `.triggered`
to avoid syntax errors.
  • Loading branch information
fennecJ committed Oct 27, 2024
1 parent 63e8edc commit a452c6e
Showing 1 changed file with 7 additions and 7 deletions.
14 changes: 7 additions & 7 deletions property/isa.sv
Original file line number Diff line number Diff line change
Expand Up @@ -9,7 +9,7 @@ typedef enum logic [6:0] {
OPC_JAL = 7'b1101111,
OPC_LUI = 7'b0110111,
OPC_AUIPC = 7'b0010111,
OPC_FENCE = 7'b0001111, // FENCE, FENCE.TSO, PAUSE
OPC_FENCE = 7'b0001111, // FENCE, FENCE.I
OPC_E = 7'b1110011 // ECALL, EBREAK
} opcode_t;

Expand Down Expand Up @@ -222,17 +222,16 @@ module isa (
if (rst) ex_bubble_misc <= 1'b1;
else if (!core_ex_stall) ex_bubble_misc <= id_pipeline_info.bubble;
// 0 means valid here (no bubble)
// only when (there is no bubble from id) and (inst from id is valid) then we can set to valid (0)
// However, we have assumed that all inst should be validInst, thus there is no need for checking
// if inst valid. Original logic is
// only when (there is no bubble from id) and (inst from id is valid RV32I inst) then we
// can set to valid (0) However, we have assumed that all inst should be validInst, thus
// there is no need for checking if inst valid. Original logic is
// ex_bubble_misc <= (!id_pipeline_info.bubble && is_validInst(id_pipeline_info.inst_pc.inst)) ? 1'b0 : 1'b1;
// Which can be simply to ex_bubble_misc <= id_pipeline_info.bubble; when is_validInst is always hold.
// Which can be simplify to ex_bubble_misc <= id_pipeline_info.bubble; when is_validInst is always hold.
end

assign if_inst = core.if_unit.rv_instr; //! use imem_parcel_i instead?

// Directly follow the logic in core.if_unit

always_comb begin
if (rst) if_pc = PC_INIT;
// if_pc will never be du_dato_i (with assume no_dbg_change_pc)
Expand Down Expand Up @@ -665,7 +664,8 @@ module isa (
endproperty : E2E_JAL_RD

property E2E_JAL_WE1; // rd != 0 -> must enable write;
@(posedge clk) disable iff (rst) VALID_JAL && (|wb_inst_dc.rd) |-> (core.wb_we == 1);
@(posedge clk) disable iff (rst) VALID_JAL.triggered && (|wb_inst_dc.rd) |->
(core.wb_we == 1);
endproperty : E2E_JAL_WE1

// [->x] goto : means that goto the x-th time the sequence is pulled up.
Expand Down

0 comments on commit a452c6e

Please sign in to comment.