MicroTESK

Executions:

1. 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,
2. 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,

Dependencies:

1. VAAddrNotEqualPAAddrNotEqualDTLBTagReplaced

Result:

1. UNSAT

Constraint:

1. [isMapped$0$[0, 0] = 1],
2. [VA$0$[12, 12] = 0],
3. [D$0$[0, 0] = D0$0$[0, 0]],
4. [V$0$[0, 0] = V0$0$[0, 0]],
5. [PFN$0$[0, 23] = PFN0$0$[0, 23]],
6. [C$0$[0, 1] = C0$0$[0, 1]],
7. [C$0$[2, 2] = C0$0$[2, 2]],
8. [G$0$[0, 0] = 1],
9. [V$0$[0, 0] = 1],
10. [D$0$[0, 0] = 1],
11. [isHiMem$0$[0, 0] = 0],
12. [PA$0$[0, 11] = VA$0$[0, 11]],
13. [PA$0$[12, 35] = PFN$0$[0, 23]],
14. [C$0$[0, 1] = 2],
15. [isMapped$1$[0, 0] = 1],
16. [VA$1$[12, 12] = 0],
17. [D$1$[0, 0] = D0$1$[0, 0]],
18. [V$1$[0, 0] = V0$1$[0, 0]],
19. [PFN$1$[0, 23] = PFN0$1$[0, 23]],
20. [C$1$[0, 1] = C0$1$[0, 1]],
21. [C$1$[2, 2] = C0$1$[2, 2]],
22. [G$1$[0, 0] = 1],
23. [V$1$[0, 0] = 1],
24. [D$1$[0, 0] = 1],
25. [isHiMem$1$[0, 0] = 0],
26. [PA$1$[0, 11] = VA$1$[0, 11]],
27. [PA$1$[12, 35] = PFN$1$[0, 23]],
28. [C$1$[0, 1] = 2],
29. [VA$0$[0, 11] = VA$1$[0, 11]],
30. [VA$0$[12, 12] = VA$1$[12, 12]],
31. [VA$0$[40, 63] = VA$1$[40, 63]],
32. [PA$0$[0, 11] = PA$1$[0, 11]],
33. [PA$0$[12, 35] = PA$1$[12, 35]],
34. [VA$0$[13, 39] = VA$1$[13, 39]],
35. [VA$0$[13, 39] != VA$1$[13, 39]]
    1. UNSAT