MicroTESK 2.3 Alpha Released
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.