Project

General

Profile

Installation Guide » History » Version 102

Alexander Kamkin, 01/10/2020 02:13 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
## @System and Security@;
34
## @System@;
35
## @Advanced system settings@.
36
# 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 98 Alexander Kamkin
To generate test data based on constraints, MicroTESK uses external SMT solvers. There are supported https://github.com/z3prover/[Z3] and https://github.com/CVC4/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 96 Alexander Kamkin
If solvers are already installed, MicroTESK can find them by using the @Z3_PATH@ and @CVC4_PATH@ environment variables.
74 13 Andrei Tatarnikov
75 96 Alexander Kamkin
*NOTE:* Each @_PATH@ variable specifies the path to the corresponding executable.
76 1 Andrei Tatarnikov
77 96 Alexander Kamkin
*Installing Z3*
78 1 Andrei Tatarnikov
79 96 Alexander Kamkin
* Build Z3 as it is described in https://github.com/Z3Prover/z3.
80
* Move the executable file to the following path (or create a symbolic link):
81
  - @<INSTALL_DIR>/tools/z3/windows/z3.exe@ (Windows);
82
  - @<INSTALL_DIR>/tools/z3/unix/z3@ (Linux);
83
  - @<INSTALL_DIR>/tools/z3/osx/z3@ (macOS).
84 1 Andrei Tatarnikov
85 96 Alexander Kamkin
*Installing CVC4*
86 1 Andrei Tatarnikov
87 96 Alexander Kamkin
* Build CVC4 as it is described in https://github.com/CVC4/CVC4/.
88
* Move the executable file to the following path (or create a symbolic link):
89
  - @<INSTALL_DIR>/tools/cvc4/windows/cvc4.exe@ (Windows);
90
  - @<INSTALL_DIR>/tools/cvc4/unix/cvc4@ (Linux);
91
  - @<INSTALL_DIR>/tools/cvc4/osx/cvc4@ (macOS).
92 1 Andrei Tatarnikov
93 96 Alexander Kamkin
h2. Usage
94 1 Andrei Tatarnikov
95 96 Alexander Kamkin
h3. Model Compilation
96
97
To compile a microprocessor model from its specification, run the following command:
98
99
* @sh compile.sh <SPECIFICATION>@ (Linux and macOS);
100
* @compile.bat <SPECIFICATION>@ (Windows).
101
102
For example, the actions below compile the model from the miniMIPS specification:
103
104 1 Andrei Tatarnikov
<pre>
105 96 Alexander Kamkin
$ cd $MICROTESK_HOME
106
$ sh bin/compile.sh arch/minimips/model/minimips.nml arch/minimips/model/mmu/minimips.mmu
107 1 Andrei Tatarnikov
</pre>
108
109 96 Alexander Kamkin
*NOTE:* Models for all demo specifications are included into the MicroTESK distribution package. There is no need to compile them.
110 1 Andrei Tatarnikov
111 96 Alexander Kamkin
h3. Test Program Generation
112 1 Andrei Tatarnikov
113 96 Alexander Kamkin
To generate a test program for a given architecture (model) and a given test template, run the following command:
114 1 Andrei Tatarnikov
115 96 Alexander Kamkin
* @sh generate.sh <ARCH> <TEMPLATE>@ (Linux and macOS);
116
* @generate.bat <ARCH> <TEMPLATE>@ (Windows).
117 1 Andrei Tatarnikov
118 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:
119
120 33 Alexander Kamkin
<pre>
121 96 Alexander Kamkin
$ cd $MICROTESK_HOME
122
$ sh bin/generate.sh minimips arch/minimips/templates/euclid.rb
123 43 Andrei Tatarnikov
</pre>
124
125 99 Alexander Kamkin
The output file name depends on the @--code-file-prefix@ and @--code-file-extension@ options (see [[Command-Line Options]]).
126 14 Andrei Tatarnikov
127 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):
128
129 89 Alexander Kamkin
<pre>
130 96 Alexander Kamkin
$ cd $MICROTESK_HOME
131
$ sh bin/generate.sh -s cvc4 minimips arch/minimips/templates/constraint.rb
132 95 Andrei Tatarnikov
</pre>
133 27 Andrei Tatarnikov
134 1 Andrei Tatarnikov
h2. Options
135 100 Alexander Kamkin
136
h3. Command-Line Options
137
138
See [[Command-Line Options]].
139 96 Alexander Kamkin
140
h3. Settings File
141
142
Default values of options are stored in the @<INSTALL_DIR>/etc/settings.xml@ configuration file:
143
144
<pre>
145
<?xml version="1.0" encoding="utf-8"?>
146
<settings>
147
  <setting name="random-seed" value="0"/>
148
  <setting name="branch-exec-limit" value="1000"/>
149
  <setting name="code-file-extension" value="asm"/>
150
  <setting name="code-file-prefix" value="test"/>
151
  <setting name="data-file-extension" value="dat"/>
152
  <setting name="data-file-prefix" value="test"/>
153
  <setting name="exception-file-prefix" value="test_except"/>
154
  <setting name="program-length-limit" value="1000"/>
155
  <setting name="trace-length-limit" value="1000"/>
156
  <setting name="comments-enabled" value=""/>
157
  <setting name="comments-debug" value=""/>
158
  <setting name="default-test-data" value=""/>
159
  <setting
160
    name="arch-dirs"
161
    value="cpu=arch/demo/cpu/settings.xml:minimips=arch/minimips/settings.xml"
162
  />
163
</settings>
164
</pre>