Project

General

Profile

Installation Guide » History » Version 106

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