Open arithmic-ASHISH opened 1 month ago
For this constraint:
(LB_flag + LBU_flag + SB_flag) [remainder*(remainder -1)*(remainder -2)*(remainder-3)] + (LH_flag + LHU_flag + SH_flag) [remainder*(remainder -2)] + (LW_flag + SW_flag)*remainder = 0
Isn't the first term guaranteed to be zero?
[remainder*(remainder -1)*(remainder -2)*(remainder-3)] == 0
remainder \in {0,1,2,3}
If the goal is just to check that remainder is in fact {0,1,2,3} then we can get rid of the flat term out front.
Not sure how we can remove it. The first term ensures that the remainder is in {0,1,2,3} when the instruction is LB, LBU, or SB. For example if the instruction is LB and remainder is 5 then constraint is non-zero, and hence an invalid execution. This cannot be captured if we remove this term.
For this constraint:
(LB_flag + LBU_flag + SB_flag) [remainder*(remainder -1)*(remainder -2)*(remainder-3)] + (LH_flag + LHU_flag + SH_flag) [remainder*(remainder -2)] + (LW_flag + SW_flag)*remainder = 0
Isn't the first term guaranteed to be zero?
[remainder*(remainder -1)*(remainder -2)*(remainder-3)] == 0
remainder \in {0,1,2,3}
If the goal is just to check that remainder is in fact {0,1,2,3} then we can get rid of the flat term out front.For
(LH_flag + LHU_flag + SH_flag) [remainder*(remainder -2)]
I believe it would be clearer to structure it as: