Instructions to download and install GameTime.
The current version of GameTime is 1.5 (released July 2015, download size: 115 MB). The previous version is also available (version 1.0, released June 2014, download size: 115MB). Version 1.5 adds new feature called overcomplete basis described in Tutorial 4 on the tutorials page.
To install GameTime, download and follow the installation instructions.
GameTime is currently only available for Microsoft Windows. Efforts are currently underway to make it available for other operating systems. If you would like to contribute to GameTime as a developer, please contact us.
Version 1.0 (released June 2, 2014): Initial release of GameTime.
The list below details the code constructs that are not completely supported by the latest version of GameTime. Better support is planned and scheduled for future versions.
If you notice that GameTime is unable to deal with a code construct not listed above, please contact us with information about the code construct and, preferably, a sample.
If you run into any issues during installation, please contact us and we will respond as soon as possible.
Install the 32-bit version of Cygwin. During the Cygwin installation process, you will be asked to select packages to install. Select at least the following packages:
Install either Microsoft Visual Studio 2008 or
Microsoft Visual C++ Express 2008.
If you do not have a copy of either, but you are a student or a staff member at an academic institution, you may be able to use Microsoft DreamSpark, which allows the download of Microsoft Visual C++ Express 2008.
Install Microsoft Phoenix, the infrastructure for program analysis and transformation from Microsoft. We have provided a copy of the installer with the name Phoenix-SDK-June-2008-RC1.msi, located in the directory ext.
GameTime uses an SMT (satisfiability modulo theories) solver and an ILP (integer linear programming) solver as part of its workflow. It thus expects the paths to an SMT solver and to an ILP solver to be available in the PATH system variable. (To learn about how to add a path to the PATH system variable, refer to the appendix.)
At least one of these SMT solvers must be installed and available:
Boolector: Once configured and installed, add the path for the Boolector executable (boolector.exe) to the PATH system variable. Additionally, GameTime supports the use of Boolector with any of its recommended backend SAT solvers: Lingeling, MiniSat, or PicoSAT.
Z3: Add the path for the directory that contains the Z3 Python interface (z3.pyc) to the PATH system variable. This interface is usually located in the bin directory of the downloaded Z3 package.
In step 1, you installed the GNU Linear Programming Kit (glpk), which provides an ILP solver. However, using the pulp Python package, GameTime can also support the following ILP solvers (if installed): CBC mixed ILP solver, IBM ILOG CPLEX Optimizer, Gurobi Optimizer, and FICO Xpress Optimizer.
GameTime currently supports one simulator:
PTARM simulator: This is a simulator for a precision-timed ARM architecture, developed by a collaborative effort lead by Prof. Edward A. Lee at University of California, Berkeley and Prof. Stephen A. Edwards at Columbia University.
To install the PTARM simulator in Cygwin, follow the process described here, but with the following editions:
If you are unable to access the website where the binaries for the GNU-ARM toolchain are located (http://gnuarm.com/files.html), you may be able to access an archived version of the website, such as the one located here.
After the GNU-ARM toolchain has been installed as part of "Requirements", copy the DLL file cygwin1.dll from the root directory of Cygwin to the bin directory located within the root directory of the GNU-ARM toolchain.
After the GNU-ARM toolchain has been installed as part of "Requirements", add the path to the directory libexec/gcc/arm-elf/4.1.1 to the PATH system variable. (To learn how to do this, refer to the appendix.)
The simulator source code needs to be modified slightly. Before the step labeled "Compiling PTARM", navigate to the root directory of the simulator source code and run the following command in Cygwin to apply a patch to the source code:
where GAMETIME_DIR is the path for
the root directory of the GameTime source
patch -d src/cpu <
Once the simulator has been installed, add the path for the simulator executable (pret.exe) to the PATH system variable. (To learn how to do this, refer to the appendix.) The executable should be present in the bin directory located within the root directory of the simulator source code.
Add the path for the directory that contains the Python interpreter, installed in the previous step, to the PATH system variable. (To learn how to do this, refer to the appendix.)
Cygwin must be launched within the Microsoft Phoenix Command Prompt: right-click on Phoenix SDK Command Prompt - Debug - x86 under Microsoft Phoenix SDK June 2008 in the Start menu, and select Run as administrator.
To launch Cygwin, enter the following command at
where CYGWIN_DIR is the absolute path for
the root directory of Cygwin, usually located at
Navigate to the GameTime directory and run the following
command at the prompt:
./configure && make install
This command will configure different files within GameTime. It will then install the Python setuptools module, which will be used to install the following PyPI packages: networkx, numpy, ply, pulp, pyparsing, and pyside. Finally, GameTime itself will be installed as a Python module.
To test your installation, navigate to the GameTime directory
in the Phoenix window running Cygwin. From within the directory,
run the command:
This should conduct a GameTime analysis on exemplar code that performs modular exponentiation, available in the directory demo/modexp_unrolled. GameTime should run completely without producing errors.
The command assumes default values for the solvers that GameTime uses in its verification of the installation: The default SMT solver is Z3 and the default ILP solver is the solver that is included with the pulp Python package.
To specify a different ILP solver, use the
--ilp-solver) command-line switch,
followed by the name of the ILP solver. The names supported
are the same as those supported by the
<ilp-solver> tag in a project
configuration file, as enumerated
To specify a different SMT solver, use the
--smt-solver) command-line switch,
followed by the name of the SMT solver. The names supported
are the same as those supported by the
<smt-solver> tag in a project
configuration file, as enumerated
./verify-installation -i glpk -s boolector
If you have successfully installed GameTime, try out the tutorials.
To add a path to the PATH system variable, add this line to the end of the .bashrc file for Cygwin, usually located in the home subdirectory of the Cygwin directory:
where NEW_PATH is the Unix form of the absolute
path that needs to be added. So, for example, if the directory
of the Python interpreter is located at C:\Python27,
and this directory needs to be added to the PATH
system variable, NEW_PATH will be
/cygdrive/c/Python27. The command
cygpath -u can be used to determine