Project

General

Profile

Installation Guide » History » Version 109

Sergey Smolov, 02/17/2021 03:57 PM

1 1 Andrei Tatarnikov
h1. Installation Guide
2
3 36 Alexander Kamkin
{{toc}}
4
5 96 Alexander Kamkin
h2. System Requirements
6 1 Andrei Tatarnikov
7 96 Alexander Kamkin
Being developed in Java, MicroTESK can be used on Windows, Linux, macOS, and other platforms with the following software installed:
8 1 Andrei Tatarnikov
9 109 Sergey Smolov
* JDK 11+ (https://openjdk.java.net)
10 108 Alexander Protsenko
* Apache Ant 1.8+ (https://ant.apache.org)
11 96 Alexander Kamkin
12 98 Alexander Kamkin
To generate test data based on constraints (if required), MicroTESK needs an SMT solver such as Z3 or CVC4 (see [[Installation Guide#Installing-SMT-Solvers|Installing SMT Solvers]]).
13 96 Alexander Kamkin
14
h2. Installation
15
16 1 Andrei Tatarnikov
h3. Installation Steps
17
18 109 Sergey Smolov
# "Download":http://forge.ispras.ru/projects/microtesk/files and unpack a distribution package (the latest @.tar.gz@ file).
19 98 Alexander Kamkin
  The destination directory will be further referred to as @<INSTALL_DIR>@.
20 96 Alexander Kamkin
# Set the @MICROTESK_HOME@ environment variable to the @<INSTALL_DIR>@ path (see [[Installation Guide#Setting-Environment-Variables|Setting Environment Variables]]).
21 1 Andrei Tatarnikov
# Add the @<INSTALL_DIR>/bin@ path to the @PATH@ environment variable.
22 98 Alexander Kamkin
# If required, install SMT solver(s) to the @<INSTALL_DIR>/tools@ directory (see [[Installation Guide#Installing-SMT-Solvers|Installing SMT Solvers]]).
23 96 Alexander Kamkin
24 101 Alexander Kamkin
h3. Setting Environment Variables
25 96 Alexander Kamkin
26
*Windows*
27
28
# Start the @Control Panel@ dialog.
29
# Click on the following items:
30 105 Alexander Kamkin
  - @System and Security@;
31
  - @System@;
32
  - @Advanced system settings@.
33 96 Alexander Kamkin
# Click on @Environment Variables@.
34
# Click on @New...@ under @System Variables@.
35
# Specify @Variable name@ as @MICROTESK_HOME@ and @Variable value@ as @<INSTALL_DIR>@.
36
# Click @OK@ in all open windows.
37 1 Andrei Tatarnikov
# Reopen the command prompt window.
38
39 96 Alexander Kamkin
*Linux and macOS*
40 1 Andrei Tatarnikov
41 96 Alexander Kamkin
Add the command below to @~/.bash_profile@ (Linux) or @~/.profile@ (macOS):
42 1 Andrei Tatarnikov
43 96 Alexander Kamkin
<pre>
44
export MICROTESK_HOME=<INSTALL_DIR>
45
</pre>
46 1 Andrei Tatarnikov
47 96 Alexander Kamkin
Changes will be applied after restarting the terminal.
48 1 Andrei Tatarnikov
49 96 Alexander Kamkin
h3. Installation Directory Structure
50 1 Andrei Tatarnikov
51 96 Alexander Kamkin
@<INSTALL_DIR>@ contains the following subdirectories:
52 1 Andrei Tatarnikov
53 96 Alexander Kamkin
table=.
54
{font-style:italic; font-weight:bold; background:#ddd}. |<. Directory |<. Description |
55 102 Alexander Kamkin
                      |<. @arch@    |<. Microprocessor specifications and test templates |
56
{background:#f6fcff}. |<. @bin@     |<. Scripts for model compilation and test generation |
57
                      |<. @doc@     |<. Documentation |
58
{background:#f6fcff}. |<. @etc@     |<. Configuration files |
59
                      |<. @gen@     |<. Generated code of microprocessor models |
60
{background:#f6fcff}. |<. @lib@     |<. JAR files and Ruby scripts |
61
                      |<. @src@     |<. Source code |
62
{background:#f6fcff}. |<. @tools@   |<. SMT solvers |
63 1 Andrei Tatarnikov
64 101 Alexander Kamkin
h3. Installing SMT Solvers
65 96 Alexander Kamkin
66 104 Alexander Kamkin
To generate test data based on constraints, MicroTESK uses external SMT solvers. There are supported "Z3":https://github.com/z3prover/ and "CVC4":https://github.com/CVC4/CVC4/. Solver executables should be placed to @<INSTALL_DIR>/tools@.
67 1 Andrei Tatarnikov
68 96 Alexander Kamkin
*Specifying paths*
69 40 Alexander Kamkin
70 106 Alexander Kamkin
If solvers are already installed, MicroTESK can find them by using the @Z3_PATH@ and @CVC4_PATH@ environment variables. Each @_PATH@ variable specifies the path to the corresponding executable.
71 1 Andrei Tatarnikov
72 96 Alexander Kamkin
*Installing Z3*
73 1 Andrei Tatarnikov
74 109 Sergey Smolov
# Build Z3 as it is described in https://github.com/Z3Prover/z3.
75
# Move the executable file to the following path (or create a symbolic link):
76 96 Alexander Kamkin
  - @<INSTALL_DIR>/tools/z3/windows/z3.exe@ (Windows);
77
  - @<INSTALL_DIR>/tools/z3/unix/z3@ (Linux);
78
  - @<INSTALL_DIR>/tools/z3/osx/z3@ (macOS).
79 1 Andrei Tatarnikov
80 96 Alexander Kamkin
*Installing CVC4*
81 1 Andrei Tatarnikov
82 109 Sergey Smolov
# Build CVC4 as it is described in https://github.com/CVC4/CVC4/.
83
# Move the executable file to the following path (or create a symbolic link):
84 96 Alexander Kamkin
  - @<INSTALL_DIR>/tools/cvc4/windows/cvc4.exe@ (Windows);
85
  - @<INSTALL_DIR>/tools/cvc4/unix/cvc4@ (Linux);
86
  - @<INSTALL_DIR>/tools/cvc4/osx/cvc4@ (macOS).
87 1 Andrei Tatarnikov
88 96 Alexander Kamkin
h2. Usage
89 1 Andrei Tatarnikov
90 96 Alexander Kamkin
h3. Model Compilation
91
92
To compile a microprocessor model from its specification, run the following command:
93
94
* @sh compile.sh <SPECIFICATION>@ (Linux and macOS);
95
* @compile.bat <SPECIFICATION>@ (Windows).
96
97
For example, the actions below compile the model from the miniMIPS specification:
98
99 1 Andrei Tatarnikov
<pre>
100 96 Alexander Kamkin
$ cd $MICROTESK_HOME
101
$ sh bin/compile.sh arch/minimips/model/minimips.nml arch/minimips/model/mmu/minimips.mmu
102 1 Andrei Tatarnikov
</pre>
103
104 96 Alexander Kamkin
*NOTE:* Models for all demo specifications are included into the MicroTESK distribution package. There is no need to compile them.
105 1 Andrei Tatarnikov
106 96 Alexander Kamkin
h3. Test Program Generation
107 1 Andrei Tatarnikov
108 96 Alexander Kamkin
To generate a test program for a given architecture (model) and a given test template, run the following command:
109 1 Andrei Tatarnikov
110 96 Alexander Kamkin
* @sh generate.sh <ARCH> <TEMPLATE>@ (Linux and macOS);
111
* @generate.bat <ARCH> <TEMPLATE>@ (Windows).
112 1 Andrei Tatarnikov
113 96 Alexander Kamkin
For example, the actions below generate a test program for the miniMIPS model compiled in the previous example and the @euclid.rb@ test template:
114
115 33 Alexander Kamkin
<pre>
116 96 Alexander Kamkin
$ cd $MICROTESK_HOME
117
$ sh bin/generate.sh minimips arch/minimips/templates/euclid.rb
118 43 Andrei Tatarnikov
</pre>
119
120 99 Alexander Kamkin
The output file name depends on the @--code-file-prefix@ and @--code-file-extension@ options (see [[Command-Line Options]]).
121 14 Andrei Tatarnikov
122 96 Alexander Kamkin
To specify which SMT solver should be used to solve constraints (if required), specify the @--solver <SOLVER>@ (or @-s <SOLVER>@) option, where @<SOLVER>@ is @z3@ or @cvc4@ (by default, Z3 is used):
123
124 89 Alexander Kamkin
<pre>
125 96 Alexander Kamkin
$ cd $MICROTESK_HOME
126
$ sh bin/generate.sh -s cvc4 minimips arch/minimips/templates/constraint.rb
127 95 Andrei Tatarnikov
</pre>
128 27 Andrei Tatarnikov
129 1 Andrei Tatarnikov
h2. Options
130 100 Alexander Kamkin
131
h3. Command-Line Options
132
133
See [[Command-Line Options]].
134 96 Alexander Kamkin
135
h3. Settings File
136
137
Default values of options are stored in the @<INSTALL_DIR>/etc/settings.xml@ configuration file:
138
139
<pre>
140
<?xml version="1.0" encoding="utf-8"?>
141
<settings>
142
  <setting name="random-seed" value="0"/>
143
  <setting name="branch-exec-limit" value="1000"/>
144
  <setting name="code-file-extension" value="asm"/>
145
  <setting name="code-file-prefix" value="test"/>
146
  <setting name="data-file-extension" value="dat"/>
147
  <setting name="data-file-prefix" value="test"/>
148
  <setting name="exception-file-prefix" value="test_except"/>
149
  <setting name="program-length-limit" value="1000"/>
150
  <setting name="trace-length-limit" value="1000"/>
151
  <setting name="comments-enabled" value=""/>
152
  <setting name="comments-debug" value=""/>
153
  <setting name="default-test-data" value=""/>
154
  <setting
155
    name="arch-dirs"
156
    value="cpu=arch/demo/cpu/settings.xml:minimips=arch/minimips/settings.xml"
157
  />
158
</settings>
159
</pre>