Skip to content

Commit

Permalink
Merge pull request #9 from fennecJ/revert-8-jhsy1209021/jal_properties
Browse files Browse the repository at this point in the history
Revert "Complete JAL ISA formal properties"
  • Loading branch information
fennecJ authored Oct 23, 2024
2 parents b0eec37 + 6157d1b commit bc6ea86
Showing 1 changed file with 2 additions and 43 deletions.
45 changes: 2 additions & 43 deletions property/isa.sv
Original file line number Diff line number Diff line change
Expand Up @@ -311,23 +311,6 @@ module isa (
end

// JAL
logic [31:0] previous_jal_pc;
logic [20:0] previous_jal_imm;
logic [31:0] previous_jal_imm_signed_exted;

always_ff @(posedge clk) begin
if (rst) begin
previous_jal_pc <= 32'd0;
previous_jal_imm <= 21'd0;
end else begin
if ((wb_inst_dc.opcode == OPC_JAL) && (!core_wb_stall) &&
(wb_pipeline_info.bubble == 1'b0)) begin
previous_jal_pc <= wb_pipeline_info.inst_pc.pc;
previous_jal_imm <= wb_inst_dc.imm21_j;
end
end
end
assign previous_jal_imm_signed_exted = {{11{previous_jal_imm[20]}}, previous_jal_imm};

// AUIPC
logic auipc_trigger;
Expand Down Expand Up @@ -609,31 +592,14 @@ module isa (
blt_followed_by_valid_inst_immediately |-> core.wb_pc == blt_gold_addr;
endproperty : E2E_BLT

// FIXME:
// For JAL
// Add extra assume to ensure branch target is aligned to 4 (assume inst[8] = 0)
// When the instruction in the WB staged is JAL,
// Let taken_pc = WB's pc + (simm20 << 1)
// |-> ##[1: $] inst's pc == taken_pc
// result to be write back should be WB's pc + 4
// |-> ##[1: $] reg[rd] should be same as result
// verilog_format: off
property E2E_JAL_RD_IS_PC_PLUS_4;
@(posedge clk) disable iff (rst) (wb_inst_dc.opcode == OPC_JAL) && (!core_wb_stall) &&
(wb_pipeline_info.bubble == 1'b0) && (core.wb_we)
|-> (core.wb_r == wb_pipeline_info.inst_pc.pc + 4);
endproperty

sequence FIRST_VALID_INST_AFTER_JAL_CAPTURED;
(wb_inst_dc.opcode == OPC_JAL) && (!core_wb_stall) && (wb_pipeline_info.bubble == 1'b0) ##1
(wb_pipeline_info.bubble == 1'b0);
endsequence

property E2E_JAL_NEXT_VALID_INST_IS_CORRECT;
@(posedge clk) disable iff (rst)
FIRST_VALID_INST_AFTER_JAL_CAPTURED
|->(wb_pipeline_info.inst_pc.pc == previous_jal_pc + previous_jal_imm_signed_exted);
endproperty
// verilog_format: on

// For AUIPC
// When the instruction in the WB staged is AUIPC
Expand Down Expand Up @@ -729,6 +695,7 @@ module isa (
`endif // PipeFollower



`ifdef ISA_GROUP_A
/* FIXME: add other isa for group A [XORI, BLT, JAL, LB, AUIPC] */
invalid_no_wen :
Expand Down Expand Up @@ -758,14 +725,6 @@ module isa (
assert property (E2E_BLT);
`endif // blt

`ifdef jal
e2e_jal_rd_correct :
assert property (E2E_JAL_RD_IS_PC_PLUS_4);

e2e_jal_pc_jump_correct :
assert property (E2E_JAL_NEXT_VALID_INST_IS_CORRECT);
`endif // jal

`ifdef auipc
e2e_auipc_pre_wb :
assert property (E2E_AUIPC_PRE_WB);
Expand Down

0 comments on commit bc6ea86

Please sign in to comment.