ISA¶
The Instruction Set Architecture of MicroTESK for ARM Demo version.
Installation Steps¶
- Download and unpack a distribution package (the latest
.tar.gz
file).
The destination directory will be further referred to as<INSTALL_DIR>
. - Set the
MICROTESK_HOME
environment variable to the<INSTALL_DIR>
path (see Setting Environment Variables). - Add the
<INSTALL_DIR>/bin
path to thePATH
environment variable. - 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:
Updated by Alexander Protsenko almost 2 years ago ยท 10 revisions