Project

General

Profile

Installation Guide » History » Version 100

Alexander Kamkin, 01/10/2020 02:09 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 98 Alexander Kamkin
h4. *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
|<. @arch@    |<. Microprocessor specifications and test templates |
59
|<. @bin@     |<. Scripts for model compilation and test generation |
60
|<. @doc@     |<. Documentation |
61
|<. @etc@     |<. Configuration files |
62
|<. @gen@     |<. Generated code of microprocessor models |
63
|<. @lib@     |<. JAR files and Ruby scripts |
64 1 Andrei Tatarnikov
|<. @src@     |<. Source code |
65 96 Alexander Kamkin
|<. @tools@   |<. SMT solvers |
66 1 Andrei Tatarnikov
67 98 Alexander Kamkin
h4. *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>