The released version of MicroTESK (v2.3) supports test program generation for MMU. The approach is based on formal specifications of memory access instructions (loads and stores) and buffers (TLB, L1/L2, etc.). Test programs are generated by enumerating all feasible situations (instruction execution paths) and dependencies (sets of inter-instruction conflicts) for a given memory access template. It is important that situations and dependencies are automatically extracted from specifications.
New version can be downloaded from the page http://forge.ispras.ru/projects/microtesk/files.