MicroTESK » MicroTESK for ARM Demo

ISA¶

The Instruction Set Architecture of MicroTESK for ARM Demo version.

Installation Steps¶

1. Download and unpack a distribution package (the latest .tar.gz file).
   The destination directory will be further referred to as <INSTALL_DIR>.
2. Set the MICROTESK_HOME environment variable to the <INSTALL_DIR> path (see Setting Environment Variables).
3. Add the <INSTALL_DIR>/bin path to the PATH environment variable.
4. If required, install SMT solver(s) to the <INSTALL_DIR>/tools directory (see Installing SMT Solvers).

You can learn more about Installation Directory Structure by following the link.

Next we will use the following directories:

• arch - contains microprocessor specifications and test templates.
• bin - contains scripts for model compilation and test generation

Test Program Generation¶

To generate the test program for the ARM architecture (model) and the bubble_sort template, run the following command:

$ cd $MICROTESK_HOME
$ sh bin/generate.sh armv8 arch/armv8/templates/bubble_sort.rb -dgp memory

The output file name depends on the --code-file-prefix and --code-file-extension options (see Command-Line Options).

Self-Check Test Program Generation¶

To generate the self-check test program for the the bubble_sort template, run the following command:

$ sh bin/generate.sh armv8 arch/armv8/templates/bubble_sort.rb -dgp memory -sc

Templates¶

The entire list of demo templates can be found in the directory: <INSTALL_DIR>/arch/armv8/templates.

$ cd $MICROTESK_HOME/arch/armv8/templates

You can use the run.sh script from this directory to generate the test program:

./run.sh branch_generation

The generated test program will be in this directory: $MICROTESK_HOME/output_test/branch_generation

cd $MICROTESK_HOME/output_test/branch_generation

Also you can use the run-sc.sh script from this directory to generate the self-check test program:

./run.sh branch_generation

The generated test program will be in this directory: $MICROTESK_HOME/output_test_sc/branch_generation

Test trace¶

The option --tracer-log enables generation of tracer logs for simulation. (In scripts run.sh, run-sc.sh it is enabled.)
The trace format is described here: https://forge.ispras.ru/projects/qemu4v/wiki/QEMU4V_Trace_Format
The test trace you can compare with the program execution trace on simulator. You can use the Trace Matcher tool.
To simulate ARMv8 assembler programs you can use QEMU4V tool.

Or you can use the approach shown in the picture below: