diff --git a/isa.tcl b/isa.tcl index d7468b3..74ec161 100644 --- a/isa.tcl +++ b/isa.tcl @@ -36,16 +36,16 @@ proc setCheckFlag {flagName flagValue} { } # set check flag -setCheckFlag "CheckInstValidAssume" 0 -setCheckFlag "RegFileStable" 0 -setCheckFlag "PipeFollower" 0 +setCheckFlag "CheckInstValidAssume" 1 +setCheckFlag "RegFileStable" 1 +setCheckFlag "PipeFollower" 1 setCheckFlag "ISA_GROUP_A" 1 # Following Flag works only when "ISA_GROUP_A" set to 1 - setCheckFlag "xori" 0 - setCheckFlag "lb" 0 + setCheckFlag "xori" 1 + setCheckFlag "lb" 1 setCheckFlag "blt" 1 - setCheckFlag "jal" 0 - setCheckFlag "auipc" 0 + setCheckFlag "jal" 1 + setCheckFlag "auipc" 1 eval $ANALYZE_COMMAND diff --git a/property/isa.sv b/property/isa.sv index b97ae9d..0ce4b1b 100644 --- a/property/isa.sv +++ b/property/isa.sv @@ -789,17 +789,17 @@ module isa ( `endif // blt `ifdef jal - // e2e_jal_rd_correct : - // assert property (E2E_JAL_RD_IS_PC_PLUS_4); + 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); + e2e_jal_pc_jump_correct : + assert property (E2E_JAL_NEXT_VALID_INST_IS_CORRECT); - // e2e_jal_rd : - // assert property (E2E_JAL_RD); + e2e_jal_rd : + assert property (E2E_JAL_RD); - // e2e_jal_we1 : - // assert property (E2E_JAL_WE1); + e2e_jal_we1 : + assert property (E2E_JAL_WE1); check_goto_meaning : assert property (@(posedge clk) disable iff (rst) (VALID_JAL) |->