Bug #6159
Updated by Alexander Kamkin almost 9 years ago
Executions: # @LOAD, LOAD, BYTE, isMapped=1, DTLB.Event=MISS, JTLB.Event=HIT, VA[12]=0, G=1, V=1, D=1, isHiMem=0, C[0:1]=2, STOP,@ STOP, # @LOAD, LOAD, BYTE, isMapped=1, DTLB.Event=MISS, JTLB.Event=HIT, VA[12]=0, G=1, V=1, D=1, isHiMem=0, C[0:1]=2, STOP,@ STOP, Dependencies: # @VAAddrNotEqualPAAddrNotEqualDTLBTagReplaced@ VAAddrNotEqualPAAddrNotEqualDTLBTagReplaced Result: # @UNSAT@ UNSAT Constraint: # @[isMapped$0$[0, [isMapped$0$[0, 0] = 1],@ == 1], # @[VA$0$[12, [VA$0$[12, 12] = 0],@ == 0], # @[D$0$[0, [D$0$[0, 0] = == D0$0$[0, 0]],@ 0]], # @[V$0$[0, [V$0$[0, 0] = == V0$0$[0, 0]],@ 0]], # @[PFN$0$[0, [PFN$0$[0, 23] = == PFN0$0$[0, 23]],@ 23]], # @[C$0$[0, [C$0$[0, 1] = == C0$0$[0, 1]],@ 1]], # @[C$0$[2, [C$0$[2, 2] = == C0$0$[2, 2]],@ 2]], # @[G$0$[0, [G$0$[0, 0] = 1],@ == 1], # @[V$0$[0, [V$0$[0, 0] = 1],@ == 1], # @[D$0$[0, [D$0$[0, 0] = 1],@ == 1], # @[isHiMem$0$[0, [isHiMem$0$[0, 0] = 0],@ == 0], # @[PA$0$[0, [PA$0$[0, 11] = == VA$0$[0, 11]],@ 11]], # @[PA$0$[12, [PA$0$[12, 35] = == PFN$0$[0, 23]],@ 23]], # @[C$0$[0, [C$0$[0, 1] = 2],@ == 2], # @[isMapped$1$[0, [isMapped$1$[0, 0] = 1],@ == 1], # @[VA$1$[12, [VA$1$[12, 12] = 0],@ == 0], # @[D$1$[0, [D$1$[0, 0] = == D0$1$[0, 0]],@ 0]], # @[V$1$[0, [V$1$[0, 0] = == V0$1$[0, 0]],@ 0]], # @[PFN$1$[0, [PFN$1$[0, 23] = == PFN0$1$[0, 23]],@ 23]], # @[C$1$[0, [C$1$[0, 1] = == C0$1$[0, 1]],@ 1]], # @[C$1$[2, [C$1$[2, 2] = == C0$1$[2, 2]],@ 2]], # @[G$1$[0, [G$1$[0, 0] = 1],@ == 1], # @[V$1$[0, [V$1$[0, 0] = 1],@ == 1], # @[D$1$[0, [D$1$[0, 0] = 1],@ == 1], # @[isHiMem$1$[0, [isHiMem$1$[0, 0] = 0],@ == 0], # @[PA$1$[0, [PA$1$[0, 11] = == VA$1$[0, 11]],@ 11]], # @[PA$1$[12, [PA$1$[12, 35] = == PFN$1$[0, 23]],@ 23]], # @[C$1$[0, [C$1$[0, 1] = 2],@ == 2], # @[VA$0$[0, [VA$0$[0, 11] = == VA$1$[0, 11]],@ 11]], # @[VA$0$[12, [VA$0$[12, 12] = == VA$1$[12, 12]],@ 12]], # @[VA$0$[40, [VA$0$[40, 63] = == VA$1$[40, 63]],@ 63]], # @[PA$0$[0, [PA$0$[0, 11] = == PA$1$[0, 11]],@ 11]], # @[PA$0$[12, [PA$0$[12, 35] = == PA$1$[12, 35]],@ 35]], # @[VA$0$[13, [VA$0$[13, 39] = == VA$1$[13, 39]],@ 39]], ## *UNSAT* # @[VA$0$[13, [VA$0$[13, 39] != VA$1$[13, 39]]@ 39]] ## @UNSAT@ *UNSAT*