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-sc.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.
To simulate ARMv8 assembler programs you can use QEMU4V tool. (See: Toolchain)

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