News

MicroTESK (Microprocessor TEsting and Specification Kit) version 2.3 has been released

MicroTESK (Microprocessor TEsting and Specification Kit) version 2.3 has been released. The new version supports generating test programs for functional verification of memory management units of microprocessors. The approach being used is based on formal specifications of memory access instructions, namely load and store instructions, and memory devices such as cache units and address translation buffers. The use of formal specifications helps automate development of test program generators and makes verification systematic due to clear definition of testing goals. The test generator constructs test programs by using combinatorial techniques, which means that stimuli – sequences of loads and stores – are created by enumerating all feasible combinations of instructions, situations (instruction execution paths) and dependencies (sets of conflicts between instructions). It is important that test situations and dependencies are automatically extracted from specifications. The approach is scalable to industrial projects and allows discovering critical bugs in memory management mechanisms.

More information is available here.