Merge branch 'sockeye' into master
authorDaniel Schwyn <schwyda@student.ethz.ch>
Tue, 26 Sep 2017 14:00:50 +0000 (16:00 +0200)
committerDaniel Schwyn <schwyda@student.ethz.ch>
Tue, 26 Sep 2017 14:01:10 +0000 (16:01 +0200)
Signed-off-by: Daniel Schwyn <schwyda@student.ethz.ch>

24 files changed:
doc/025-sockeye/Hakefile [new file with mode: 0644]
doc/025-sockeye/Sockeye.tex [new file with mode: 0644]
doc/025-sockeye/example.soc [new file with mode: 0644]
doc/style/barrelfish.bib
hake/RuleDefs.hs
socs/Hakefile [new file with mode: 0644]
socs/cortex/cortexA9.soc [new file with mode: 0644]
socs/omap44xx.soc [new file with mode: 0644]
socs/omap44xx/cortexA9-subsystem.soc [new file with mode: 0644]
tools/sockeye/Hakefile [new file with mode: 0644]
tools/sockeye/Main.hs [new file with mode: 0644]
tools/sockeye/SockeyeASTDecodingNet.hs [new file with mode: 0644]
tools/sockeye/SockeyeASTInstantiator.hs [new file with mode: 0644]
tools/sockeye/SockeyeASTParser.hs [new file with mode: 0644]
tools/sockeye/SockeyeASTTypeChecker.hs [new file with mode: 0644]
tools/sockeye/SockeyeBackendProlog.hs [new file with mode: 0644]
tools/sockeye/SockeyeChecks.hs [new file with mode: 0644]
tools/sockeye/SockeyeInstantiator.hs [new file with mode: 0644]
tools/sockeye/SockeyeNetBuilder.hs [new file with mode: 0644]
tools/sockeye/SockeyeParser.hs [new file with mode: 0644]
tools/sockeye/SockeyeTypeChecker.hs [new file with mode: 0644]
usr/skb/Hakefile
usr/skb/programs/decoding_net.pl [new file with mode: 0644]
usr/skb/programs/decoding_net_queries.pl [new file with mode: 0644]

diff --git a/doc/025-sockeye/Hakefile b/doc/025-sockeye/Hakefile
new file mode 100644 (file)
index 0000000..4790050
--- /dev/null
@@ -0,0 +1,26 @@
+----------------------------------------------------------------------
+-- Copyright (c) 2017, ETH Zurich.
+-- All rights reserved.
+--
+-- This file is distributed under the terms in the attached LICENSE file.
+-- If you do not find this file, copies can be found by writing to:
+-- ETH Zurich D-INFK, Universitaetstr. 6, CH-8092 Zurich. Attn: Systems Group.
+--
+-- Hakefile for /doc/TN-025-Sockeye.pdf
+--
+----------------------------------------------------------------------
+
+let
+    sockeyeToProlog = [ "example" ]
+    sockeyeRule f = Rule [ sockeyeProgLoc,
+                           In SrcTree "src" (f ++ ".soc"),
+                           Str "-o",
+                           Out "docs" (f ++ ".pl")
+                         ]
+    prologFromSockeye = [ Dep BuildTree "docs" (f ++ ".pl") | f <- sockeyeToProlog]
+in
+[ buildTechNoteWithDeps "Sockeye.tex" "TN-025-Sockeye.pdf" True False [] 
+    prologFromSockeye
+]
+++
+[sockeyeRule f | f <- sockeyeToProlog]
diff --git a/doc/025-sockeye/Sockeye.tex b/doc/025-sockeye/Sockeye.tex
new file mode 100644 (file)
index 0000000..ddbf57e
--- /dev/null
@@ -0,0 +1,716 @@
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+% Copyright (c) 2017, ETH Zurich.
+% All rights reserved.
+%
+% This file is distributed under the terms in the attached LICENSE file.
+% If you do not find this file, copies can be found by writing to:
+% ETH Zurich D-INFK, Universitaetstr 6, CH-8092 Zurich. Attn: Systems Group.
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+
+\providecommand{\pgfsyspdfmark}[3]{}
+
+\documentclass[a4paper,11pt,twoside]{report}
+\usepackage[T1]{fontenc}
+\usepackage{amsmath}
+\usepackage{bftn}
+\usepackage{calc}
+\usepackage{verbatim}
+\usepackage{xspace}
+\usepackage{pifont}
+\usepackage{pxfonts}
+\usepackage{textcomp}
+
+\usepackage{multirow}
+\usepackage{listings}
+\usepackage{todonotes}
+\usepackage{hyperref}
+
+\title{Sockeye in Barrelfish}
+\author{Barrelfish project}
+% \date{\today}   % Uncomment (if needed) - date is automatic
+\tnnumber{025}
+\tnkey{Sockeye}
+
+
+\lstdefinelanguage{Sockeye}{
+    morekeywords={accept, are, as, at, import, in, input, is, map, module, output, over, reserved, to, with},
+    sensitive=true,
+    morecomment=[l]{//},
+    morecomment=[s]{/*}{*/},
+    morestring=[b]",
+}
+
+\presetkeys{todonotes}{inline}{}
+
+\begin{document}
+\maketitle      % Uncomment for final draft
+
+\begin{versionhistory}
+\vhEntry{0.1}{15.06.2017}{DS}{Initial Version}
+\vhEntry{0.2}{03.08.2017}{DS}{Describe Modularity Features}
+\end{versionhistory}
+
+% \intro{Abstract}    % Insert abstract here
+% \intro{Acknowledgements}  % Uncomment (if needed) for acknowledgements
+\tableofcontents    % Uncomment (if needed) for final draft
+% \listoffigures    % Uncomment (if needed) for final draft
+% \listoftables     % Uncomment (if needed) for final draft
+\cleardoublepage
+\setcounter{secnumdepth}{2}
+
+\newcommand{\fnname}[1]{\textit{\texttt{#1}}}%
+\newcommand{\datatype}[1]{\textit{\texttt{#1}}}%
+\newcommand{\varname}[1]{\texttt{#1}}%
+\newcommand{\keywname}[1]{\textbf{\texttt{#1}}}%
+\newcommand{\pathname}[1]{\texttt{#1}}%
+\newcommand{\tabindent}{\hspace*{3ex}}%
+\newcommand{\Sockeye}{\lstinline[language=Sockeye]}
+\newcommand{\Prolog}{\lstinline[language=Prolog]}
+\newcommand{\ccode}{\lstinline[language=C]}
+
+\lstset{
+  basicstyle=\ttfamily \small,
+  keywordstyle=\bfseries,
+  flexiblecolumns=false,
+  basewidth={0.5em,0.45em},
+  boxpos=t,
+  captionpos=b,
+  frame=single,
+  breaklines=true,
+  postbreak=\mbox{\textcolor{red}{$\hookrightarrow$}\space}
+}
+
+
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+\chapter{Introduction and Usage}
+\label{chap:introduction}
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+
+\emph{Sockeye}\footnote{Sockeye salmon (Oncorhynchus nerka), also called red salmon, kokanee salmon, or blueback salmon, is an anadromous species of salmon found in the Northern Pacific Ocean and rivers discharging into it. This species is a Pacific salmon that is primarily red in hue during spawning. They can grow up to 84 cm in length and weigh 2.3 to 7 kg. 
+Source: \href{https://en.wikipedia.org/wiki/Sockeye_salmon}{Wikipedia}}
+is a domain specific language to describe SoCs (Systems on a Chip).
+
+Achermann~et~al.~\cite{achermann:mars17} propose a formal model to describe address spaces and interrupt routes in a system as a directed graph.
+They call such a graph a ``decoding net''.
+Each node in the graph can accept a set of addresses and translate another (not necessarily disjunct) set of addresses (when describing interrupt routes they accept or translate interrupt vectors).
+Starting at a specific node, addresses can be resolved by following the appropriate edges in the decoding net.
+When a node translates an address, resolution is continued at the referenced node.
+When a node accepts an address, resolution terminates
+
+Achermann~et~al.~\cite{achermann:mars17} also propose a concrete syntax for specifying decoding nets.
+Sockeye is an implementation of the proposed language but adds some features to address issues encountered in practice.
+
+The Sockeye compiler is written in Haskell using the Parsec parsing library. It
+generates Prolog files from the Sockeye files. These Prolog files contain facts that represent a decoding net (see Chapter~\ref{chap:prolog}).
+The Prolog files can then be loaded into Barrelfish's System Knowledgebase (SKB).
+
+In the future the compiler should also be able to generate Isabelle code from Sockeye specifications to be able to verify hardware designs.
+
+The source code for Sockeye can be found in \pathname{SOURCE/tools/sockeye}.
+
+\clearpage
+\section{Command Line Options}
+
+\begin{verbatim}
+$ sockeye [options] file
+\end{verbatim}
+
+
+The available options are:
+\begin{description}
+\item[-P] Generate a Prolog file that can be loaded into the SKB (default).
+\item[-i] Add a directory to the search path where Sockeye looks for imports.
+\item[-o] \varname{filename} The path to the output file (required)
+\item[-d] \varname{filename} The path to the dependency output file (optional)
+\item[-h] show usage information
+\end{description}
+
+The backend (capital letter options) specified last takes precedence.
+At the moment there is only a backend for generating Prolog for use in Barrelfish's SKB.
+
+Multiple directories can be added by giving the \texttt{-i} options multiple times.
+Sockeye will first look for files in the current directory and then check the given directories in the order they were given.
+
+When invoked with the \texttt{-d} option, the compiler will generate a dependency file for GNU make to be able to track changes in imported files.
+
+The Sockeye file to compile is given via the \texttt{file} parameter.
+
+
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+\chapter{Lexical Conventions}
+\label{chap:lexer}
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+
+The Sockeye parser follows a similar convention as opted by modern day 
+programming languages like C and Java. Hence, Sockeye uses a Java-style-like
+parser based on the Haskell Parsec Library. The following conventions are used:
+
+\begin{description}
+\item[Encoding] The file should be encoded using plain text.
+\item[Whitespace:]  As in C and Java, Sockeye considers sequences of
+  space, newline, tab, and carriage return characters to be
+  whitespace.  Whitespace is generally not significant. 
+
+\item[Comments:] Sockeye supports C-style comments.  Single line comments
+  start with \texttt{//} and continue until the end of the line.
+  Multiline comments are enclosed between \texttt{/*} and \texttt{*/};
+  anything in between is ignored and treated as white space.
+  Nested comments are not supported.
+
+\item[Identifiers:] Valid Sockeye identifiers are sequences of numbers
+  (0-9), letters (a-z, A-Z), the underscore character ``\texttt{\_}'' and the dash character ``\textendash''. They
+  must start with a letter.
+  \begin{align*}
+  identifier & \rightarrow letter (letter \mid digit \mid \text{\_} \mid \text{\textendash})^{\textrm{*}} \\
+  letter & \rightarrow (\textsf{A \ldots Z} \mid  \textsf{a \ldots z})\\
+  digit & \rightarrow (\textsf{0 \ldots 9})
+    \end{align*}
+
+\item[Case sensitivity:] Sockeye is case sensitive hence identifiers \Sockeye{node1} and \Sockeye{Node2} are not the same.
+  
+\item[Integer Literals:] A Sockeye integer literal is a sequence of
+  digits, optionally preceded by a radix specifier.  As in C, decimal (base 10)
+  literals have no specifier and hexadecimal literals start with
+  \texttt{0x}.
+
+\begin{align*}
+decimal & \rightarrow (\textsf{0 \ldots 9})^{\textrm{1}}\\
+hexadecimal & \rightarrow (\textsf{0x})(\textsf{0 \ldots 9} \mid \textsf{A \ldots F} \mid \textsf{a \ldots f})^{\textrm{1}}\\
+\end{align*}
+
+\item[Reserved words:] The following are reserved words in Sockeye:
+\begin{verbatim}
+accept, are, as, at, import, in, input, is, map,
+module, output, over, reserved, to, with
+\end{verbatim}
+
+\end{description}
+
+
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+\chapter{Syntax}
+\label{chap:declaration}
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+
+In this chapter we define the layout of a Sockeye file.
+The node declarations in a Sockeye file describe a single decoding net.
+Parts of a decoding net can be packaged into reusable modules (see Section~\ref{sec:modules}).
+With imports (see Section~\ref{sec:imports}) modules can also be put into separate files.
+
+In the following sections we use EBNF to describe the Sockeye syntax. Terminals are \textbf{bold} while non-terminals are \textit{italic}.
+The non-terminals \textit{iden}, \textit{letter}, \textit{decimal} and \textit{hexadecimal} correspond to the ones defined in Chapter~\ref{chap:lexer}.
+
+The examples are all taken from the Texas Instruments OMAP4460 SoC used on the PandaboardES\footnote{The technical reference manual can be found \href{http://www.
+ti.com/lit/ug/swpu235ab/swpu235ab.pdf}{here}.}.
+A more complete specification of the SoC is located in \pathname{SOURCE/socs/omap44xx.soc}.
+
+\section{Basic Syntax}
+This section describes the basic syntax for Sockeye.
+It closely corresponds to the concrete syntax described in \cite{achermann:mars17}.
+If there are important syntactic or semantic differences it is stated explicitly in the description of the respective syntactical construct.
+
+\subsection{Node Declarations}
+A node declaration contains one or more identifiers and the node specification.
+The order in which the nodes are declared does not matter.
+
+\paragraph{Syntax}
+\begin{align*}
+\textit{net}_s & \mathop{=}
+    \Big\{
+        \textit{iden}\ \textbf{is}\ \textit{node}_s\
+    \Big|\
+        \textit{iden}\bigl\{\textbf{,}\ \textit{iden}\bigr\}\ \textbf{are}\ \textit{node}_s
+    \Big\} \\
+\end{align*}
+
+\clearpage
+\paragraph{Example}
+\begin{example}
+    SDRAM \textbf{is} \ldots
+
+    UART1,
+    UART2 \textbf{are} \ldots
+\end{example}
+
+\subsection{Node Specifications}
+A node specification consists of a type, a set of accepted address blocks, a set of address mappings to other nodes, a set of reserved address blocks and an overlay.
+All of these are optional.
+The reserved address blocks are only relevant in conjunction with overlays and are used to exclude some addresses from the overlay.
+The overlay is specified as a node identifier and a number of address bits.
+The overlay will span addresses from \texttt{0x0} to \(\texttt{0x2}^\texttt{bits} - \texttt{1}\).
+
+\paragraph{Syntax}
+\begin{align*}
+\textit{node}_s & \mathop{=}
+    \Big[\ 
+       \textit{type}\ 
+    \Big]\  
+    \Big[
+       \textit{accept}\ 
+    \Big]\ 
+    \Big[\ 
+       \textit{map}\ 
+    \Big]\ 
+    \Big[\ 
+        \textit{reserved}\ 
+    \Big]\ 
+    \Big[\ 
+        \textit{overlay}\ 
+    \Big]\\
+\textit{accept} & \mathop{=}
+    \textbf{accept [}\ \big\{\ \textit{block}_s\ \big\}\ \textbf{]}\\
+\textit{map} & \mathop{=}
+    \textbf{map [}\ \big\{\ \textit{map}_s\ \big\}\ \textbf{]}\\
+\textit{reserved} & \mathop{=}
+    \textbf{reserved [}\ \big\{\ \textit{block}_s\ \big\}\ \textbf{]}\\
+\textit{overlay} & \mathop{=}
+    \textbf{over}\ \textit{iden}\textbf{/}\textit{decimal}\\
+\end{align*}
+
+\paragraph{Example}
+\begin{example}
+    SDRAM \textbf{is} \textbf{accept} [\ldots]
+    L3 \textbf{is} \textbf{map} [\ldots]
+    CORETEXA9_SS_Interconnect \textbf{is} \textbf{reserved} [\ldots] \textbf{over} L3/32
+\end{example}
+
+\subsection{Node Type}
+Currently there are three types: \Sockeye{core}, \Sockeye{device} and \Sockeye{memory}. A fourth internal type \Sockeye{other} is given to nodes for which no type is specified.
+The \Sockeye{core} type designates the node as a CPU core. The \Sockeye{device} type specifies that the accepted addresses are device registers while the \Sockeye{memory} type is for memory nodes like RAM or ROM.
+
+\paragraph{Syntax}
+\begin{align*}
+\textit{type} & \mathop{=}
+    \textbf{core}\
+    |\
+    \textbf{device}\
+    |\
+    \textbf{memory} \\
+\end{align*}
+
+\paragraph{Example}
+\begin{example}
+    CORETEXA9_1 \textbf{is} core \textbf{map} [\ldots]
+    UART3 \textbf{is} device \textbf{accept} [\ldots]
+    SDRAM \textbf{is} memory \textbf{accept} [\ldots]
+\end{example}
+
+\subsection{Addresses}
+Addresses are specified as hexadecimal literals.
+
+\paragraph{Syntax}
+\begin{align*}
+\textit{addr} & \mathop{=} \textit{hexadecimal} \\
+\end{align*}
+
+\subsection{Block Specifications}
+A block is specified by its start and end address.
+If the start and end address are the same, the end address can be omitted.
+Sockeye also supports specifying a block as its base address and the number of address bits the block spans:
+A block from \Sockeye{0x0} to \Sockeye{0xFFF} with a size of 4kB can be specified as \Sockeye{0x0/12}.
+
+\paragraph{Syntax}
+\begin{align*}
+\textit{block}_s & \mathop{=} \textit{addr}\
+    \Big[
+        \textbf{-}\ \textit{addr}\ 
+    \Big|\
+        \textbf{/}\textit{decimal}
+    \Big] \\
+\end{align*}
+
+\paragraph{Example}
+\begin{example}
+    UART1 is \textbf{accept} [0x0-0xFFF]
+    UART3 is \textbf{accept} [0x0/12]    // \textit{same as \textup{0x0-0xFFF}}
+    IF_A9_0 is \textbf{accept} [0x44]      // \textit{same as \textup{0x44-0x44}}
+\end{example}
+
+\subsection{Map Specification}
+A map specification is a source address block, a target node identifier and optionally a target base address to which the source block is translated within the target node.
+If no target base address is given, the block is translated to the target node starting at \Sockeye{0x0}.
+Note that this is different from the concrete syntax described in \cite{achermann:mars17} where in this case the base address of the source block is used.
+This was changed due to the mapping to \Sockeye{0x0} being used more often in practice.
+Multiple translation targets can be specified by giving a comma-separated list of targets.
+
+\paragraph{Syntax}
+\begin{align*}
+\textit{map}_s & \mathop{=}
+\textit{block}_s\ \textbf{to}\ \textit{iden}\ 
+    \Big[
+        \textbf{at}\ \textit{addr}
+    \Big]\
+    \Big\{
+        \textbf{,}\ \textit{iden}\ 
+        \Big[
+            \textbf{at}\ \textit{addr}
+        \Big]
+    \Big\}\\
+\end{align*}
+
+\paragraph{Example}
+\begin{example}
+    /* \textit{Translate \textup{0x54000000-0x0x54FFFFFF}
+     * to \textup{L3_EMU} at \textup{0x54000000-0x0x54FFFFFF}:}
+     */
+    L3 is \textbf{map} [0x54000000/24 \textbf{to} L3_EMU \textbf{at} 0x54000000] 
+
+    /* \textit{This is the same as \textup{0x80000000/30 \textbf{to} SDRAM \textbf{at} 0x0}:} */
+    L3 is \textbf{map} [0x80000000/30 \textbf{to} SDRAM]
+
+    /* \textit{Multiple translation targets, interrupt vector \textup{0x2} is translated to
+     * - \textup{SPIMap} at \textup{0xC}
+     * - \textup{NVIC} at \textup{0x12}:}
+     * /
+    SDMA is \textbf{map} [0x2 \textbf{to} SPIMap \textbf{at} 0xC, NVIC \textbf{at} 0x12]
+\end{example}
+
+\section{Modules}
+\label{sec:modules}
+A module encapsulates a decoding net which can be integrated into a larger decoding net.
+A module instantiation always creates a namespace inside the current one.
+Normally nodes can only be referenced by nodes in the same namespace.
+To properly integrate a module into a larger decoding net we need a mechanism to connect the module to the enclosing decoding net.
+This is done via ports.
+There are input ports, which create a connection into the module and output ports which create connections from the module to outside nodes.
+A port has always a width, specified as the number of address bits the port spans.
+All declared input ports must have a corresponding node declaration in the module body.
+
+When a module is instantiated a list of port mappings can be specified.
+An input port mapping creates a node outside the module that overlays the node inside the module.
+An output port mapping creates a node inside the module that overlays the node outside the module.
+Not all ports a module declares have to be mapped.
+Not mapping an input port simply means there is no connection to the corresponding node inside the module.
+For unmapped output ports an empty node inside the module will be generated, acting as a dead end for address resolution.
+
+Additionally a module can be parametrized.
+It will then be a module template that only becomes a fully defined module when instantiated with concrete arguments.
+Module parameters are typed and the Sockeye compiler checks that they are used in a type safe way.
+There are two types of parameters: address parameters and natural parameters.
+Address parameters allow to parametrize addresses in node specifications.
+Natural parameters are used in combination with interval template identifiers (see Section~\ref{sec:template_idens}).
+Parameters can also be passed as arguments to module template instantiations in the module body.
+
+\subsection{Module Declarations}
+A module declaration starts with the keyword \Sockeye{module} and a unique module name.
+If the module is a template, a list of typed parameters can be specified.
+The module body is enclosed in curly braces and starts with the port definitions.
+The rest of the body are node declarations and module instantiations.
+If the module has address parameters the name of the parameter can be used wherever in the body an address is expected.
+
+\paragraph{Syntax}
+\begin{align*}
+    \textit{param\_type} & \mathop{=}
+        \textbf{addr}\ |\ \textbf{nat}\\
+    \textit{parameter} & \mathop{=}
+        \textit{param\_type}\ \textit{iden}\\
+    \textit{param\_list} & \mathop{=}
+        \textbf{(}\big[\ 
+            \textit{parameter}\big\{\textbf{,}\ \textit{parameter}\big\}\ 
+        \big] \textbf{)}\\
+    \textit{input\_port} & \mathop{=}
+        \textbf{input}\ \textit{iden}\textbf{/}\textit{decimal}
+        \big\{
+            \textbf{,}\ \textit{iden}\textbf{/}\textit{decimal}
+        \big\}\\
+    \textit{output\_port} & \mathop{=}
+        \textbf{output}\ \textit{iden}\textbf{/}\textit{decimal}
+        \big\{
+            \textbf{,}\ \textit{iden}\textbf{/}\textit{decimal}
+        \big\}\\
+    \textit{body}_s & \mathop{=}
+        \big\{\ 
+            \textit{net}_s\ |\ \textit{mod\_inst}_s\ 
+        \big\}\\
+    \textit{mod\_decl}_s & \mathop{=}
+        \textbf{module}\ \textit{iden} \big[\textit{param\_list}\big]\ 
+        \textbf{\{}\ 
+            \big\{\textit{input\_port}\ |\ \textit{output\_port}\big\}\ 
+            \textit{body}_s\ 
+        \textbf{\}}\\
+\end{align*}
+
+\paragraph{Example}
+For some examples of module declarations see Listing~\ref{lst:sockeye_example}.
+
+\subsection{Module Instantiations}
+Module instantiations start with the module name and in the case of a module template with the list of arguments.
+After that the identifier of the namespace in which to instantiate the module has to be given followed by an optional list of port mappings.
+
+\paragraph{Syntax}
+\begin{align*}
+    \textit{argument} & \mathop{=}
+        \textit{decimal}\ |\ \textit{hexadecimal}\ |\ \textit{iden}\\
+    \textit{arg\_list} & \mathop{=}
+        \textbf{(}\big[\ 
+            \textit{argument}\big\{\textbf{,}\ \textit{argument}\big\}\ 
+        \big] \textbf{)}\\
+    \textit{mod\_inst}_s & \mathop{=}
+        \textit{iden} \big[\textit{arg\_list}\big]\ \textbf{as}\ \textit{iden}\ \big[\ 
+            \textbf{with}\ \big\{\textit{input\_map}\ |\ \textit{output\_map}\big\}\ 
+        \big]\\
+    \textit{input\_map} & \mathop{=}
+        \textit{iden}\ \textbf{>}\ \textit{iden}\\
+    \textit{output\_map} & \mathop{=}
+        \textit{iden}\ \textbf{<}\ \textit{iden}\\
+\end{align*}
+
+\clearpage
+\paragraph{Example}
+\begin{example}
+    /* Instantiate module 'CortexA9-Subsystem' in namespace 'CortexA9_SS' */
+    CortexA9-Subsystem as CortexA9_SS
+
+    /* Pass arguments to module template e.g. to instantiate a
+     * CortexA9 MPCore module with
+     * - 2 cores
+     * - 0x48240000 as the base of the private memory region
+     */
+    CortexA9-MPCore(2, 0x48240000) \textbf{as} MPU
+
+    /* Declare port mappings:
+     * - map 'CORTEXA9_1' to input port 'CPU_1'
+     * - map output port 'Interconnect' to 'L3'
+     */
+    CortexA9-Subsystem as CortexA9_SS \textbf{with}
+        CORTEXA9_1 > CPU_1
+        L3 < Interconnect
+\end{example}
+
+\section{Templated Identifiers}
+\label{sec:template_idens}
+Templated identifiers allow to declare multiple nodes and ports at once and instantiate a module multiple times at once.
+There are two forms of templated identifiers:
+\begin{description}
+    \item[Interval template]
+        The template contains one or several intervals.
+        The identifier will be instantiated for all possible combinations of values in the intervals.
+        Index variables can optionally be named so they can be referenced later.
+    \item[Simple template]
+        Simple templates work very similar to interval templates.
+        The only difference is, that a simple template can only reference index variables declared in the same context.
+        It can not contain intervals to declare new index variables.
+\end{description}
+
+Interval templates can be used in identifiers of node declarations (to declare multiple nodes), port declarations (to declare multiple ports) and namespace identifiers of module instantiations (to instantiate a module multiple times).
+The scope of index variables is the corresponding syntactic construct the interval template was used in.
+Simple templates can be used in any place a node identifier is expected.
+This includes the places where interval templates can be used, identifiers of translation destination nodes and overlays but not module parameter or index variable names.
+
+An important thing to note is that the limits of an interval can reference module parameters of type \Sockeye{nat}.
+This allows module parameters to control how many ports or nodes are instantiated from a certain interval template.
+
+\paragraph{Syntax}
+\begin{align*}
+    \textit{var} & \mathop{=}
+        \textit{iden}\\
+    \textit{limit} & \mathop{=}
+        \textit{decimal}\ |\ \textit{iden} \\
+    \textit{interval} & \mathop{=}
+        \textbf{[}\textit{limit}\textbf{..}\textit{limit}\textbf{]}\\
+    \textit{interval\_templ}_s & \mathop{=}
+        \textit{iden}\textbf{\{}\textit{var}\ \textbf{in}\ \textit{interval}\textbf{\}}
+        \Big[
+            \textit{iden}\ |\ \textit{templ\_iden}_s\ |\ \textit{for\_iden}_s
+        \Big]\\
+    \textit{simple\_templ}_s & \mathop{=}
+        \textit{iden}\textbf{\{}\textit{var}\textbf{\}}\Big[\textit{iden}\ |\ \textit{templ\_iden}_s\Big]\\
+\end{align*}
+
+\paragraph{Example}
+\begin{example}
+    /* Declare similar nodes
+     * Note that interval templates in node declarations
+     * always require the usage of '\textbf{are}'
+     */
+    GPTIMER_\verb+{+[1..5]\verb+}+ \textbf{are} device \textbf{accept} [0x0/12]
+
+    /* Use the index in the node definition */
+    GPTIMER_ALIAS_\verb+{+i in [1..5]\verb+}+ \textbf{is} \textbf{map} [0x100/12 to GPTIMER_\verb+{+i\verb+}+]
+
+    /* Declare similar module ports
+     * (possibly depending on module parameters)
+     */
+    \textbf{module} module CortexA9-MPCore(nat cores, addr periphbase) \verb+{+
+        input CPU_\verb+{+[1..cores]\verb+}+
+        \ldots
+    \verb+}+
+
+    /* Instantiate module multiple times
+     * and use index variable in port mappings
+     */
+    CortexA9-Core \textbf{as} Core_\verb+{+c in [1..2]\verb+}+ \textbf{with}
+        CPU_\verb+{+c\verb+}+ > CPU
+\end{example}
+
+\section{Imports}
+\label{sec:imports}
+Imports allow a specification to be split across several files.
+They also allow the reuse of modules.
+Imports have to be specified at the very top of a Sockeye file.
+An import will cause the compiler to load all modules from \pathname{<import\_path>.soc}
+Nodes declared outside of modules will not be loaded.
+The compiler will first look for files in the current directory and then check the directories passed with the \texttt{-i} option in the order they were given.
+
+\paragraph{Syntax}
+\begin{align*}
+\textit{import}_s & \mathop{=}
+    \textbf{import}\ \big\{\ \textit{letter}\ |\ \textbf{/}\ \big\}
+\end{align*}
+
+\paragraph{Example}
+\begin{example}
+    /* Invoked with 'sockeye -i imports -i modules' the following
+     * will cause the compiler to look for the files
+     * 1. ./cortex/cortexA9.soc
+     * 2. imports/cortex/cortexA9.soc
+     * 3. modules/cortex/cortexA9.soc
+     * and import all modules from the first one that exists.
+     */
+    \textbf{import} cortex/cortexA9
+\end{example}
+
+\section{Sockeye Files}
+A sockeye file consists of imports, module declarations and the specification body (node declarations and module instantiations).
+
+\paragraph{Syntax}
+\begin{align*}
+    \textit{sockeye}_s & \mathop{=}
+        \big\{\ 
+            \textit{import}_s\ 
+        \big\}\ 
+        \big\{\ 
+            \textit{mod\_decl}_s\ 
+        \big\}\ 
+        \big\{\ 
+            \textit{net}_s\ |\ \textit{mod\_inst}_s\ 
+        \big\}
+\end{align*}
+
+\paragraph{Example}
+Listing~\ref{lst:sockeye_example} shows an example Sockeye specification.
+
+\clearpage
+\lstinputlisting[caption={Example Sockeye specification}, label={lst:sockeye_example}, language=Sockeye]{example.soc}
+
+
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+\chapter{Checks on the AST}
+\label{chap:checks}
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+The compiler performs the transformation from parsed Sockeye to decoding nets in three steps:
+\begin{enumerate}
+    \item Type checker
+    \item Instantiator
+    \item Net builder
+\end{enumerate}
+In each of the steps some checks are performed.
+The type checker checks that all referenced symbols (modules, parameters and index variables) are defined and ensures module template parameter type safety.
+The instantiator instantiates module and identifier templates and ensures that each identifier is declared only once.
+The net builder instantiates the modules and ensures referential integrity in the generated decoding net. It also transforms overlays to translation sets.
+The checks are detailed in the following sections.
+
+\section{Type Checker}
+\subsection{Duplicate Modules}
+This check makes sure that all module names in any of the imported files are unique.
+
+\subsection{Duplicate Parameters}
+This check makes sure that no module has two parameters with the same name.
+
+\subsection{Duplicate Index Variables}
+This check makes sure that no two index variables in the same scope have the same name.
+
+\subsection{Undefined Modules}
+This check makes sure that all modules being instantiated actually exist.
+
+\subsection{Undefined Parameters}
+This check makes sure that all referenced parameters are in scope.
+
+\subsection{Undefined Index Variables}
+This check makes sure that all index variables referenced in templated identifiers are in scope. 
+
+\subsection{Parameter Type Mismatch}
+This check makes sure that parameters are used in a type safe way.
+
+\subsection{Argument Count Mismatch}
+This check makes sure that module instantiations give the correct number of arguments to the module template being instantiated.
+
+\subsection{Argument Type Mismatch}
+This check makes sure that the arguments passed to module templates have the correct type.
+
+\section{Instantiator}
+\subsection{Module Instantiation Loops}
+This check makes sure that there are no loops in module instantiations which would result in an infinite nesting of decoding subnets.
+
+\subsection{Duplicate Namespaces}
+This check makes sure that all module instantiations in a module have a unique namespace.
+
+\subsection{Duplicate Identifiers}
+This check makes sure that all node identifiers are unique.
+This includes output ports, declared nodes and nodes mapped to input ports of instantiated modules.
+
+\subsection{Duplicate Ports}
+This check makes sure, that there are no duplicate input or output ports.
+Note that declaring an output port with the same identifier as an input port is allowed and results in all address resolutions going through the input port being passed through the module to the output port.
+
+\subsection{Duplicate Port Mapping}
+This check makes sure that no port is mapped twice in the same module instantiation.
+
+\section{Net Builder}
+
+\subsection{Mapping to Undefined Port}
+This check makes sure that there are no port mappings to ports not declared by the instantiated module.
+
+\subsection{References to Undefined Nodes}
+This check makes sure that all nodes referenced in translation sets, overlays and port mappings exist.
+It also checks that every input port has a corresponding node declaration.
+
+
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+\chapter{Prolog Mapping for Sockeye}
+\label{chap:prolog}
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+The Sockeye compiler generates \(\text{ECL}^i\text{PS}^e\)-Prolog\footnote{\href{http://eclipseclp.org/}{http://eclipseclp.org/}} to be used within the SKB.
+A decoding net is expressed by the predicate \Prolog{node/2}.
+The first argument to the predicate is the node identifier and the second one the node specification.
+
+Node identifiers are represented as a functor \Prolog{node_id/2}.
+The first argument is the node's name, represented as an atom, and the second one is the (possibly nested) namespace it is in.
+The namespace is represented as a list of atoms where the head is the innermost namespace component.
+
+Node specifications are represented by a Prolog functor \Prolog{node_spec/3}.
+The arguments to the functor are the node type, the list of accepted addresses and the list of translated addresses.
+The overlay is translated to address mappings and added to the list of translated addresses during compilation.
+
+The node type is one of four atoms: \Prolog{core}, \Prolog{device}, \Prolog{memory} or \Prolog{other}.
+The accepted addresses are a list of address blocks where each block is represented through the functor \Prolog{block/2} with the start and end addresses as arguments.
+The translated addresses are a list of mappings to other nodes, represented by the functor \Prolog{map/3} where the first argument is the translated address block, the second one is the target node's identifier and the third one is the base address for the mapping in the target node.
+
+There is a predicate clause for \Prolog{node/2} for every node specified.
+
+The code is generated using \(\text{ECL}^i\text{PS}^e\)'s structure notation.
+This enables more readable and concise notation when accessing specific arguments of the functors.
+
+Listing~\ref{lst:prolog_example} shows the generated Prolog code for the Sockeye example in Listing~\ref{lst:sockeye_example}.
+
+\clearpage
+\lstinputlisting[caption={Generated Prolog code},label={lst:prolog_example},language=Prolog]{example.pl}
+
+
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+\chapter{Compiling Sockeye Files with Hake}
+\label{chap:hake}
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+SoC descriptions are placed in the directory \pathname{SOURCE/socs} with the file extension \pathname{soc}.
+Each top-level Sockeye file has to be added to the list of SoCs in the Hakefile in the same directory.
+When passed a filename (without extension), the function \verb|sockeye :: String -> HRule| creates a rule to compile the file \pathname{SOURCE/socs/<filename>.soc} to \pathname{BUILD/sockeyefacts/<filename>.pl}.
+The rule will also generate \pathname{BUILD/sockeyefacts/<filename>.pl.depend} (with the \texttt{-d} option of the Sockeye compiler) and include it in the Makefile.
+This causes \texttt{make} to rebuild the file also when imported files are changed.
+To add a compiled Sockeye specification to the SKB RAM disk, the filename can be added to the \varname{sockeyeFiles} list in the SKBs Hakefile.
+
+
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+\bibliographystyle{abbrv}
+\bibliography{defs,barrelfish}
+
+\end{document}
\ No newline at end of file
diff --git a/doc/025-sockeye/example.soc b/doc/025-sockeye/example.soc
new file mode 100644 (file)
index 0000000..c28298e
--- /dev/null
@@ -0,0 +1,43 @@
+module CortexA9-Core(addr periphbase) {
+    input CPU/32
+    output SCU/8
+    output L2/32
+
+    PERIPHBASE is map [
+            0x0000-0x00FC to SCU
+            0x0600/8 to Private_Timers
+        ]
+
+    CPU is map [
+            periphbase/13 to PERIPHBASE
+        ]
+        over L2/32
+
+    Private_Timers is device accept [0x0/8]
+}
+
+module CortexA9-MPCore(nat cores, addr periphbase) {
+    input CPU_{[1..cores]}/32
+    output L2/32
+
+    SCU is device accept [0x0-0xFC]
+
+    CortexA9-Core(periphbase) as Core_{c in [1..cores]} with
+        CPU_{c} > CPU
+        SCU < SCU
+        L2 < L2
+}
+
+UART{[1..3]} are device accept [0x0/12]
+SDRAM is memory accept [0x0/30]
+
+L3 is map [
+    0x48020000/12 to UART3
+    0x4806A000/12 to UART1
+    0x4806C000/12 to UART2
+    0x80000000/30 to SDRAM
+]
+
+CortexA9-MPCore(2, 0x48240000) as CORTEXA9_SS with
+    CORTEXA9_{c in [1..2]} > CPU_{c}
+    L3 < L2
\ No newline at end of file
index 24dade9..157f765 100644 (file)
@@ -131,6 +131,15 @@ Note that this file will not compile without defs.bib; ie. you need to do:
   number =      {Revision 0.21},
   month =       {October}}
 
+@inproceedings{achermann:mars17,
+  title = {Formalizing Memory Accesses and Interrupts},
+  author = {Reto Achermann and Lukas Humbel and David Cock and Timothy Roscoe},
+  booktitle = proc # {2nd Workshop on Models for Formal Analysis of Real Systems},
+  year = 2017,
+  location = {Upsala, Sweden},
+  pages = {66--116}
+} 
+
 @inproceedings{adya:stackripping:usenix02,
   author = {Atul Adya and John Howell and Marvin Theimer and William J. Bolosky
             and John R. Douceur},
index 444562f..48f3bfe 100644 (file)
@@ -778,6 +778,30 @@ skateGenSchemas opts schema =
       ]]
 
 
+--
+-- Build SKB facts from Sockeye file
+--
+sockeyeProgLoc = In InstallTree "tools" "/bin/sockeye"
+sockeyeSocDir = In SrcTree "src" "/socs"
+sockeyeSocFileLoc d = In SrcTree "src" ("/socs" </> d <.> "soc")
+sockeyeFactFilePath d = "/sockeyefacts" </> d <.> "pl"
+sockeyeFactFileLoc d = In BuildTree "" $ sockeyeFactFilePath d
+
+sockeye :: String -> HRule
+sockeye net = 
+    let
+        factFile = sockeyeFactFilePath net
+        depFile = dependFilePath factFile
+    in Rules
+        [ Rule
+            [ sockeyeProgLoc
+            , Str "-i", sockeyeSocDir
+            , Str "-o", Out "" factFile
+            , Str "-d", Out "" depFile
+            , sockeyeSocFileLoc net
+            ]
+        , Include (Out "" depFile)
+        ]
 
 --
 -- Build a Fugu library
diff --git a/socs/Hakefile b/socs/Hakefile
new file mode 100644 (file)
index 0000000..ac5d30e
--- /dev/null
@@ -0,0 +1,15 @@
+--------------------------------------------------------------------------
+-- Copyright (c) 2017, ETH Zurich.
+-- All rights reserved.
+--
+-- This file is distributed under the terms in the attached LICENSE file.
+-- If you do not find this file, copies can be found by writing to:
+-- ETH Zurich D-INFK, Haldeneggsteig 4, CH-8092 Zurich. Attn: Systems Group.
+--
+-- Hakefile for devices/
+--
+--------------------------------------------------------------------------
+
+[ sockeye f
+  | f <- [ "omap44xx" ]
+]
diff --git a/socs/cortex/cortexA9.soc b/socs/cortex/cortexA9.soc
new file mode 100644 (file)
index 0000000..d5cc89d
--- /dev/null
@@ -0,0 +1,49 @@
+/*
+ * Copyright (c) 2017, ETH Zurich. All rights reserved.
+ *
+ * This file is distributed under the terms in the attached LICENSE file.
+ * If you do not find this file, copies can be found by writing to:
+ * ETH Zurich D-INFK, Universitaetsstrasse 6, CH-8092 Zurich.
+ * Attn: Systems Group.
+ */
+
+module CortexA9-Core(addr periphbase) {
+    input CPU/32
+    output SCU/8, Global_Timer/8
+    output GIC_PROC/8, GIC_DISTR/12
+    output L2/32
+
+    PERIPHBASE is map [
+            0x0000-0x00FC to SCU
+            0x0100/8 to GIC_PROC
+            0x0200/8 to Global_Timer
+            0x0600/8 to Private_Timers
+            0x1000/12 to GIC_DISTR
+        ]
+
+    CPU is map [
+            periphbase/13 to PERIPHBASE
+        ]
+        over L2/32
+
+    Private_Timers is device accept [0x0/8]
+}
+
+module CortexA9-MPCore(nat cores, addr periphbase) {
+    input CPU_{[1..cores]}/32
+    output L2/32
+
+    SCU is device accept [0x0-0xFC]
+    Global_Timer is device accept [0x0/8]
+
+    GIC_PROC is device accept [0x0/8]
+    GIC_DISTR is device accept [0x0/12]
+
+    CortexA9-Core(periphbase) as Core_{c in [1..cores]} with
+        CPU_{c} > CPU
+        SCU < SCU
+        Global_Timer < Global_Timer
+        GIC_PROC < GIC_PROC
+        GIC_DISTR < GIC_DISTR
+        L2 < L2
+}
\ No newline at end of file
diff --git a/socs/omap44xx.soc b/socs/omap44xx.soc
new file mode 100644 (file)
index 0000000..d9dc289
--- /dev/null
@@ -0,0 +1,778 @@
+/*
+ * Copyright (c) 2017, ETH Zurich. All rights reserved.
+ *
+ * This file is distributed under the terms in the attached LICENSE file.
+ * If you do not find this file, copies can be found by writing to:
+ * ETH Zurich D-INFK, Universitaetsstrasse 6, CH-8092 Zurich.
+ * Attn: Systems Group.
+ */
+
+/**
+ * Physical memory map for TI OMAP4460 SoC
+ *
+ * This is derived from:
+ * OMAP4460 Multimedia Device Silicon Revision 1.x Technical Reference
+ * Manual Version Q
+ *
+ */
+
+import omap44xx/cortexA9-subsystem
+
+/*
+ * 2.2 L3 Memory space mapping
+ */
+/* Q0 */
+SRAM is memory accept [0x0/30]
+
+/* Q1 */
+L3_OCM_RAM is memory accept [0x0-0xDFFF]
+
+/* Q2 */
+SDRAM is memory accept [0x0/30]
+
+/* TODO: Tiler view */
+
+L3 is map [
+        0x00000000/30 to SRAM
+        /* 0x40000000-0x4002FFFF reserved */
+        /* 0x40030000-0x4003BFFF Cortex-A9 ROM */
+        /* 0x4003C000-0x400FFFFF reserved */ //TRM: 0x40034000-0x400FFFFF?
+        /* 0x40100000/20 L4_ABE private access for Cortex A9
+        /* 0x40200000/20 reserved */
+        0x40300000-0x4030DFFF to L3_OCM_RAM
+        /* 0x4030E000-0x43FFFFFF reserved */
+        0x44000000/26 to L3_config
+        0x48000000/24 to L4_PER at 0x48000000
+        0x49000000/24 to L4_ABE
+        0x4A000000/24 to L4_CFG at 0x4A000000
+        /* 0x4B000000/24 reserved */
+        0x4C000000/24 to EMIF1
+        0x4D000000/24 to EMIF2
+        0x4E000000/25 to DMM
+        0x50000000/25 to GPMC
+        0x52000000/25 to ISS
+        0x54000000/24 to L3_EMU at 0x54000000
+        0x55000000/24 to CORTEXM3
+        0x56000000/25 to SGX
+        0x58000000/24 to Display
+        /* 0x59000000/24 reserved */
+        // 0x5A000000/24 IVA-HD configuration
+        // 0x5B000000/24 IVA-HD SL2
+        /* 0x5C000000/26 reserved */
+        // 0x60000000/28 Tiler address mapping
+        0x80000000/30 to SDRAM
+      ]
+
+/*
+ * 2.2.1 L3_EMU Memory Space Mapping
+ */
+L3_EMU is map [
+            0x54000000/20 to MIPI_STM_0
+            0x54100000/18 to MIPI_STM_1
+            0x54140000/13 to A9_CPU0_debug_PMU
+            0x54142000/13 to A9_CPU1_debug_PMU
+            /* 0x54144000/14 reserved */
+            0x54148000/12 to CTI0
+            0x54149000/12 to CTI1
+            /* 0x5414A000/13 reserved */
+            0x5414C000/12 to PTM0
+            0x5414D000/12 to PTM1
+            /* 0x5414E000/13 reserved */
+            0x54158000/12 to A9_CS-TF
+            0x54159000/12 to DAP_PC
+            /* 0x5415A000-0x5415EFFF reserved */
+            0x5416F000/12 to APB
+            0x54160000/12 to DRM
+            0x54161000/12 to MIPI_STM
+            0x54162000/12 to CS-ETB
+            0x54163000/12 to CS-TPIU
+            0x54164000/12 to CS-TF
+            /* 0x54165000/13 reserved */
+            // 0x54167000/12 Technology specific registers
+            /* 0x54168000-0x5417FFFF reserved */
+            // 0x54180000/12 Technology specific registers
+            /* 0x54181000-0x541FFFFF reserved */
+            // XXX: What about 0x54200000-0x54FFFFFF?
+          ]
+
+/*
+ * 2.3.1 L4_CFG Memory Space Mapping
+ */
+SAR_ROM is device accept [0x0/13]
+
+L4_CFG is map [
+            0x4A000000/11 to CFG_AP
+            0x4A000800/11 to CFG_LA
+            0x4A001000/12 to CFG_IP0
+            0x4A002000/12 to SYSCTRL_GENERAL_CORE
+            // 0x4A003000/12 L4 interconnect
+            0x4A004000/12 to CM1
+            // 0x4A005000/12 L4 interconnect
+            /* 0x4A006000/13 reserved
+            0x4A008000/13 to CM2
+            // 0x4A00A000/12 L4 interconnect
+            /* 0x4A00B000-0x4A055FFF reserved */
+            0x4A056000/12 to SDMA
+            // 0x4A057000/12 L4 interconnect
+            0x4A058000/12 to HSI
+            // 0x4A05C000/12 L4 interconnect
+            /* 0x4A05D000/12 reserved */
+            0x4A05E000/13 to SAR_ROM
+            // 0x4A060000/12 L4 interconnect
+            /* 0x4A061000/12 reserved */
+            0x4A062000/12 to HSUSBTLL
+            // 0x4A063000/12 L4 interconnect
+            0x4A064000/12 to HSUSBHOST
+            // 0x4A065000/12 L4 interconnect
+            0x4A066000/12 to DSP at 0x01C20000
+            // 0x4A067000/12 L4 interconnect
+            /* 0x4A068000-0x4A0A8FFF reserved */
+            0x4A0A9000/12 to FSUSBHOST
+            // 0x4A0AA000/12 L4 interconnect
+            0x4A0AB000/12 to HSUSBOTG
+            // 0x4A0AC000/12 L4 interconnect
+            0x4A0AD000/12 to USBPHY
+            // 0x4A0AE000/12 L4 interconnect
+            /* 0x4A0AF000-0x4A0D8FFF reserved */
+            0x4A0D9000/12 to SR_MPU
+            // 0x4A0DA000/12 L4 interconnect
+            0x4A0DB000/12 to SR_IVA
+            // 0x4A0DC000/12 L4 interconnect
+            0x4A0DD000/12 to SR_CORE
+            // 0x4A0DE000/12 L4 interconnect
+            /* 0x4A0DF000-0x4A0F3FFF reserved */
+            0x4A0F4000/12 to System_Mailbox
+            // 0x4A0F5000/12 L4 interconnect
+            0x4A0F6000/12 to Spinlock
+            // 0x4A0F7000/12 L4 interconnect
+            /* 0x4A0F8000/15 reserved */
+            0x4A100000/12 to SYSCTRL_PADCONF_CORE
+            // 0x4A101000/12 L4 interconnect
+            0x4A102000/12 to OCP-WP
+            // 0x4A103000/12 L4 interconnect
+            /* 0x4A104000-0x4A109FFF reserved */
+            0x4A10A000/12 to FDIF
+            // 0x4A10B000/12 L4 interconnect
+            /* 0x4A10C000-0x4A203FFF reserved */
+            0x4A204000/12 to C2C_INIT_firewall
+            // 0x4A205000/12 L4 interconnect
+            0x4A206000/12 to C2C_TARGET_firewall
+            // 0x4A207000/12 L4 interconnect
+            /* 0x4A208000/13 reserved */
+            0x4A20A000/12 to MA_firewall
+            // 0x4A20B000/12 L4 interconnect
+            0x4A20C000/12 to EMIF_firewall
+            // 0x4A20D000/12 L4 interconnect
+            /* 0x4A20E000/13 reserved */
+            0x4A210000/12 to GPMC_firewall
+            // 0x4A211000/12 L4 interconnect
+            0x4A212000/12 to L3_OCMC_RAM_firewall
+            // 0x4A213000/12 L4 interconnect
+            0x4A214000/12 to SGX_firewall
+            // 0x4A215000/12 L4 interconnect
+            0x4A216000/12 to ISS_firewall
+            // 0x4A217000/12 L4 interconnect
+            0x4A218000/12 to M3_firewall
+            // 0x4A219000/12 L4 interconnect
+            /* 0x4A21A000/13 reserved */
+            0x4A21C000/12 to DSS_firewall
+            // 0x4A21D000/12 L4 interconnect
+            0x4A21E000/12 to SL2_firewall
+            // 0x4A21F000/12 L4 interconnect
+            0x4A220000/12 to IVA-HD_firewall
+            // 0x4A221000/12 L4 interconnect
+            /* 0x4A222000/14 reserved */
+            0x4A226000/12 to L4-EMU_firewall
+            // 0x4A227000/12 L4 interconnect
+            0x4A228000/12 to L4-ABE_firewall
+            // 0x4A229000/12 L4 interconnect
+            /* 0x4A22A000-0x4A2FFFFF reserved */
+            0x4A300000/18 to L4_WKUP at 0x4A300000
+            // 0x4A340000/12 L4 interconnect
+            /* 0x4A341000-0x4AFFFFFF reserved */
+          ]
+
+
+/*
+ * 2.3.2 L4_WKUP Memory Space Mapping
+ */
+SAR_RAM1 is memory accept [0x0/12]
+SAR_RAM2 is memory accept [0x0/10]
+SAR_RAM3 is memory accept [0x0/11]
+SAR_RAM4 is memory accept [0x0/10]
+
+L4_WKUP is map [
+                0x4A300000/11 to WKUP_AP
+                0x4A300800/11 to WKUP_LA
+                0x4A301000/12 to WKUP_IP0
+                /* 0x4A302000/13 reserved */
+                0x4A304000/12 to S32KTIMER
+                // 0x4A305000/12 L4 interconnect
+                0x4A306000/13 to PRM
+                // 0x4A308000/12 L4 interconnect
+                /* 0x4A309000/12 reserved */
+                0x4A30A000/12 to SCRM
+                // 0x4A30B000/12 L4 interconnect
+                0x4A30C000/12 to SYSCTRL_GENERAL_WKUP
+                // 0x4A30D000/12 L4 interconnect
+                /* 0x4A30E000/13 reserved */
+                0x4A310000/12 to GPIO1
+                // 0x4A311000/12 L4 interconnect
+                /* 0x4A312000/13 reserved */
+                0x4A314000/12 to WDTIMER2
+                // 0x4A315000/12 L4 interconnect
+                /* 0x4A316000/13 reserved */
+                0x4A318000/12 to GPTIMER1
+                // 0x4A319000/12 L4 interconnect
+                /* 0x4A31A000/13 reserved (XXX: 'Module - Address space 0'?) */
+                0x4A31C000/12 to Keyboard
+                // 0x4A31D000/12 L4 interconnect
+                0x4A31E000/12 to SYSCTRL_PADCONF_WKUP
+                // 0x4A31F000/12 L4 interconnect
+                /* 0x4A320000-0x4A325FFF reserved */
+                0x4A326000/12 to SAR_RAM1
+                0x4A327000/10 to SAR_RAM2
+                /* 0x4A327400-0x4A327FFF reserved */
+                0x4A328000/11 to SAR_RAM3
+                /* 0x4A328800-0x4A328FFF reserved */
+                0x4A329000/10 to SAR_RAM4
+                /* 0x4A329400-0x4A329FFF reserved */
+                // 0x4A32A000/12 L4 interconnect
+                /* 0x4A32B000-0x4A33FFFF reserved */
+           ]
+
+/*
+ * 2.3.3 L4_PER Memory Space Mapping
+ */
+L4_PER is map [
+            0x48000000/11 to PER_AP
+            0x48000800/11 to PER_LA
+            0x48001000/10 to PER_IP0
+            0x48001400/10 to PER_IP1
+            0x48001800/10 to PER_IP2
+            0x48001C00/10 to PER_IP3
+            /* 0x48002000-0x4801FFFF reserved */
+            0x48020000/12 to UART3
+            // 0x48021000/12 L4 interconnect
+            /* 0x48022000/16 reserved */
+            0x48032000/12 to GPTIMER2
+            // 0x48033000/12 L4 interconnect
+            0x48034000/12 to GPTIMER3
+            // 0x48035000/12 L4 interconnect
+            0x48036000/12 to GPTIMER4
+            // 0x48037000/12 L4 interconnect
+            /* 0x48038000-0x4803DFFF reserved */
+            0x4803E000/12 to GPTIMER9
+            // 0x4803F000/12 L4 interconnect
+            0x48040000/16 to Display
+            // 0x48050000/12 L4 interconnect
+            /* 0x48051000/14 reserved */
+            0x48055000/12 to GPIO2
+            // 0x48056000/12 L4 interconnect
+            0x48057000/12 to GPIO3
+            // 0x48058000/12 L4 interconnect
+            0x48059000/12 to GPIO4
+            // 0x4805A000/12 L4 interconnect
+            0x4805B000/12 to GPIO5
+            // 0x4805C000/12 L4 interconnect
+            0x4805D000/12 to GPIO6
+            // 0x4805E000/12 L4 interconnect
+            /* 0x4805F000/12 reserved */
+            0x48060000/12 to I2C3
+            // 0x48061000/12 L4 interconnect
+            /* 0x48062000/15 reserved */
+            0x4806A000/12 to UART1
+            // 0x4806B000/12 L4 interconnect
+            0x4806C000/12 to UART2
+            // 0x4806D000/12 L4 interconnect
+            0x4806E000/12 to UART4
+            // 0x4806F000/12 L4 interconnect
+            0x48070000/12 to I2C1
+            // 0x48071000/12 L4 interconnect
+            0x48072000/12 to I2C2
+            // 0x48073000/12 L4 interconnect
+            /* 0x48074000/13 reserved */
+            0x48076000/12 to SLIMBUS2
+            // 0x48077000/12 L4 interconnect
+            0x48078000/12 to ELM
+            // 0x48079000/12 L4 interconnect
+            /* 0x4807A000-0x48085FFF reserved */
+            0x48086000/12 to GPTIMER10
+            // 0x48087000/12 L4 interconnect
+            0x48088000/12 to GPTIMER11
+            // 0x48089000/12 L4 interconnect
+            /* 0x4808A000-0x48095FFF reserved */
+            0x48096000/12 to McBSP4
+            // 0x48097000/12 L4 interconnect
+            0x48098000/12 to McSPI1
+            // 0x48099000/12 L4 interconnect
+            0x4809A000/12 to McSPI2
+            // 0x4809B000/12 L4 interconnect
+            0x4809C000/12 to HSMMC1
+            // 0x4809D000/12 L4 interconnect
+            /* 0x4809E000-0x480ACFFF reserved */
+            0x480AD000/12 to MMC_SD3
+            // 0x480AE000/12 L4 interconnect
+            /* 0x480AF000-0x480B1FFF reserved */
+            0x480B2000/12 to HDQ
+            // 0x480B3000/12 L4 interconnect
+            0x480B4000/12 to HSMMC2
+            // 0x480B5000/12 L4 interconnect
+            /* 0x480B6000/13 reserved */
+            0x480B8000/12 to McSPI3
+            // 0x480B9000/12 L4 interconnect
+            0x480BA000/12 to McSPI4
+            // 0x480BB000/12 L4 interconnect
+            /* 0x480BC000-0x480D0FFF reserved */
+            0x480D1000/12 to MMC_SD4
+            // 0x480D2000/12 L4 interconnect
+            /* 0x480D3000/13 reserved */
+            0x480D5000/12 to MMC_SD5
+            // 0x480D6000/12 L4 interconnect
+            /* 0x480D7000-0x4834FFFF reserved */
+            0x48350000/12 to I2C4
+            // 0x48351000/12 L4 interconnect
+            /* 0x48352000-0x48FFFFFF reserved */
+          ]
+
+/*
+ * 2.3.4 L4_ABE Memory Space Mapping
+ */
+DMEM,
+CMEM,
+SMEM are memory accept [0x0/16]
+
+L4_ABE is accept [0x00000/14] // XXX: First 16KB do what?
+          map [
+            /* 0x04000-0x021FFF reserved */
+            0x22000/12 to McBSP1
+            // 0x23000/12 L4 interconnect
+            0x24000/12 to McBSP2
+            // 0x25000/12 L4 interconnect
+            0x26000/12 to McBSP3
+            // 0x27000/12 L4 interconnect
+            0x28000/12 to McASP
+            // 0x29000/12 L4 interconnect
+            0x2A000/12 to McASP_DATA
+            // 0x2B000/12 L4 interconnect
+            0x2C000/12 to SLIMBUS1
+            // 0x2D000/12 L4 interconnect
+            0x2E000/12 to DMIC
+            // 0x2F000/12 L4 interconnect
+            0x30000/12 to WDTIMER3
+            // 0x31000/12 L4 interconnect
+            0x32000/12 to McPDM
+            // 0x33000/12 L4 interconnect
+            /* 0x34000/14 reserved */
+            0x38000/12 to GPTIMER5
+            // 0x39000/12 L4 interconnect
+            0x3A000/12 to GPTIMER6
+            // 0x3B000/12 L4 interconnect
+            0x3C000/12 to GPTIMER7
+            // 0x3D000/12 L4 interconnect
+            0x3E000/12 to GPTIMER8
+            // 0x3F000/12 L4 interconnect
+            /* 0x40000/18 reserved */
+            0x80000/16 to DMEM
+            // 0x90000/12 L4 interconnect
+            /* 0x91000-0x9FFFF reserved */
+            0xA0000/16 to CMEM
+            // 0xB0000/12 L4 interconnect
+            /* 0xB1000-0xBFFFF reserved */
+            0xC0000/16 to SMEM
+            // 0xD0000/12 L4 interconnect
+            /* 0xD1000/17 reserved */
+            0xF1000/12 to AESS
+            // 0xF2000/12 L4 interconnect
+            /* 0xF3000-0xFFFFF reserved */
+          ]
+
+/*
+ * Cortex A9 Memory Space Mapping
+ */
+CortexA9-Subsystem as CortexA9_SS with
+    CORTEXA9_{c in [1..2]} > CPU_{c}
+    L3 < L3
+    L4_ABE < L4_ABE
+
+/*
+ * 2.4 Dual Cortex-M3 Subsystem Memory Space Mapping
+ */
+CORTEXM3_ROM is memory accept [0x0/14]
+CORTEXM3_RAM is memory accept [0x0/16]
+
+// TODO: address space not accessible from L3
+CORTEXM3 is map [
+                    0x00000000-0x54FFFFFF to L3
+                    0x55000000/14 to CORTEXM3_ROM
+                    0x55020000/16 to CORTEXM3_RAM
+                    /* 0x55030000/16 reserved */
+                    0x55040000/18 to ISS at 0x10000 // XXX: Not accessible from L3?
+                    0x55080000/12 to M3_MMU
+                    0x55081000/12 to M3_WUGEN
+                    /* 0x55082000-0x55FFFFFF reserved */
+                    0x56000000/25 to L3
+                ]
+
+/*
+ * 2.5 DSP Subsystem Memory Space Mapping
+ */
+ // TODO: address space not accessible from L4_CFG
+ DSP is map [
+            0x01C20000/12 to SYSC
+        ]
+
+/*
+ * 2.6 Display Subsystem Memory Space Mapping
+ */
+Display is map [
+                // 0x0000/12 Display subsystem registers
+                0x1000/12 to DISPC
+                0x2000/12 to RFBI
+                0x3000/12 to VENC
+                0x4000/12 to DSI1
+                0x5000/12 to DSI2
+                0x6000/12 to HDMI
+                0x7000/12 to HDCP
+           ]
+
+/*
+ * 3 Power, Reset and Clock Management
+ */
+/*
+/* 3.11.1 PRM Instance Summary */
+INTRCONN_SOCKET_PRM is device accept [0x0/8]
+CKGEN_PRM is device accept [0x0/8]
+MPU_PRM is device accept [0x0/8]
+DSP_PRM is device accept [0x0/8]
+ABE_PRM is device accept [0x0/8]
+ALWAYS_ON_PRM is device accept [0x0/8]
+CORE_PRM is device accept [0x0/11]
+IVAHD_PRM is device accept [0x0/8]
+CAM_PRM is device accept [0x0/8]
+DSS_PRM is device accept [0x0/8]
+SGX_PRM is device accept [0x0/8]
+L3INIT_PRM is device accept [0x0/8]
+L4PER_PRM is device accept [0x0/9]
+WKUP_PRM is device accept [0x0/8]
+WKUP_CM is device accept [0x0/8]
+EMU_PRM is device accept [0x0/8]
+EMU_CM is device accept [0x0/8]
+DEVICE_PRM is device accept [0x0/8]
+INSTR_PRM is device accept [0x0/8]
+PRM is map [
+            0x0000/8 to INTRCONN_SOCKET_PRM
+            0x0100/8 to CKGEN_PRM
+            0x0300/8 to MPU_PRM
+            0x0400/8 to DSP_PRM
+            0x0500/8 to ABE_PRM
+            0x0600/8 to ALWAYS_ON_PRM
+            0x0700/11 to CORE_PRM
+            0x0F00/8 to IVAHD_PRM
+            0x1000/8 to CAM_PRM
+            0x1100/8 to DSS_PRM
+            0x1200/8 to SGX_PRM
+            0x1300/8 to L3INIT_PRM
+            0x1400/9 to L4PER_PRM
+            0x1700/8 to WKUP_PRM
+            0x1800/8 to WKUP_CM
+            0x1900/8 to EMU_PRM
+            0x1A00/8 to EMU_CM
+            0x1B00/8 to DEVICE_PRM
+            0x1F00/8 to INSTR_PRM
+       ]
+
+/* 3.11.21 CM1 Instance Summary */
+INTERCONN_SOCKET_CM1 is device accept [0x0/8]
+CKGEN_CM1 is device accept [0x0/9]
+CM1 is map [
+        0x000/8 to INTERCONN_SOCKET_CM1
+        0x100/9 to CKGEN_CM1
+       ]
+
+/* 3.11.29 CM2 Instance Summary */
+INTRCONN_SOCKET_CM2 is device accept [0x0/8]
+CKGEN_CM2 is device accept [0x0/8]
+ALWAYS_ON_CM2 is device accept [0x0/8]
+CORE_CM2 is device accept [0x0/11]
+IVAHD_CM2 is device accept [0x0/8]
+CAM_CM2 is device accept [0x0/8]
+DSS_CM2 is device accept [0x0/8]
+SGX_CM2 is device accept [0x0/8]
+L3INIT_CM2 is device accept [0x0/8]
+L4PER_CM2 is device accept [0x0/9]
+RESTORE_CM2 is device accept [0x0/8]
+INSTR_CM2 is device accept [0x0/8]
+CM2 is map [
+        0x0000/8 to INTRCONN_SOCKET_CM2
+        0x0100/8 to CKGEN_CM2
+        0x0600/8 to ALWAYS_ON_CM2
+        0x0700/11 to CORE_CM2
+        0x0F00/8 to IVAHD_CM2
+        0x1000/8 to CAM_CM2
+        0x1200/8 to SGX_CM2
+        0x1300/8 to L3INIT_CM2
+        0x1400/9 to L4PER_CM2
+        0x1E00/8 to RESTORE_CM2
+        0x1F00/8 to INSTR_CM2
+       ]
+
+/* 3.12 SCRM Register Manual */
+SCRM is device accept [0x0/12]
+
+/* 3.13 SR Register Manual */
+SR_MPU is device accept [0x0/8]
+SR_IVA is device accept [0x0/8]
+SR_CORE is device accept [0x0/8]
+
+/*
+ * 5 DSP Subsystem
+ */
+SYS_INTC is device accept [0x0/16]
+SYS_PD is device accept [0x0/16]
+EDM is device accept [0x0/12]
+TPCC is device accept [0x0/16]
+TPTC0,
+TPTC1 are device accept [0x0/10]
+SYSC is device accept [0x0/12]
+WUGEN is device accept [0x0/12]
+L1_SCACHE,
+L2_SCACHE are device accept [0x0/8]
+SCACHE_SCTM is device accept [0x0/9]
+SCACHE_MMU is device accept [0x0/11]
+
+/*
+ * 6 IVA-HD Subsystem
+ */
+SYSCTRL is device accept [0x0/10]
+
+/*
+ * 7 Dual Cortex-M3 MPU Subsystem
+ */
+M3_WUGEN is device accept [0x0/12]
+
+/*
+ * 8 Imaging Subsystem
+ */
+ISS_TOP is device accept [0x0/8]
+ISP5 is device accept [0x0/16]
+SIMCOP is device accept [0x0/17]
+ISS is map [
+            0x00000/8 to ISS_TOP
+            // TODO: Interfaces
+            0x10000/17 to ISP5
+            0x20000/17 to SIMCOP
+          ]
+
+/*
+ * 9 Face Detect
+ */
+FDIF is device accept [0x0/12]
+
+/*
+ * 10 Display Subsystem
+ */
+DISPC,
+RFBI,
+VENC,
+DSI1,
+DSI2,
+HDMI,
+HDCP are device accept [0x0/12]
+
+/*
+ * 11 2D/3D Graphics Accelerator
+ */
+SGX is device accept [0x0/25]
+
+/*
+ * 12 Audio Backend
+ */
+AESS is device accept [0x0/12]
+
+/*
+ * 13 Interconnect
+ */
+/* 13.2 L3 Interconnect */
+L3_config is device accept [0x0/26]
+C2C_INIT_firewall is device accept [0x0/12] // not in TRM, from omap44xx_map.h
+C2C_TARGET_firewall is device accept [0x0/12] // not in TRM, from omap44xx_map.h
+MA_firewall is device accept[0x0/12]
+EMIF_firewall is device accept [0x0/12]
+GPMC_firewall is device accept [0x0/12]
+L3_OCMC_RAM_firewall is device accept [0x0/12]
+SGX_firewall is device accept [0x0/12]
+ISS_firewall is device accept [0x0/12]
+M3_firewall is device accept [0x0/12]
+DSS_firewall is device accept [0x0/12]
+SL2_firewall is device accept [0x0/12]
+IVA-HD_firewall is device accept [0x0/12]
+L4-EMU_firewall is device accept [0x0/12]
+L4-ABE_firewall is device accept [0x0/12]
+
+/* 13.3 L4 Interconnects */
+PER_AP is device accept [0x0/11]
+PER_LA is device accept [0x0/11]
+PER_IP0 is device accept [0x0/10]
+PER_IP1 is device accept [0x0/10]
+PER_IP2 is device accept [0x0/10]
+PER_IP3 is device accept [0x0/10]
+
+CFG_AP is device accept [0x0/11]
+CFG_LA is device accept [0x0/11]
+CFG_IP0 is device accept [0x0/12]
+
+WKUP_AP is device accept [0x0/11]
+WKUP_LA is device accept [0x0/11]
+WKUP_IP0 is device accept [0x0/12]
+
+/*
+ * 15 Memory Subsystem
+ */
+DMM is device accept [0x0/25]
+EMIF1,
+EMIF2 are device accept [0x4D000000/24]
+GPMC is device accept [0x0/25]
+ELM is device accept [0x48078000/12]
+
+/*
+ * 16 SDMA
+ */
+SDMA is device accept [0x0/12]
+
+/*
+ * 17 Interrupt Controllers
+ */
+// TODO
+
+/*
+ * 18 Control Module
+ */
+SYSCTRL_GENERAL_CORE,
+SYSCTRL_GENERAL_WKUP,
+SYSCTRL_PADCONF_CORE,
+SYSCTRL_PADCONF_WKUP are device accept [0x0/12]
+
+
+/*
+ * 19 Mailbox
+ */
+System_Mailbox,
+IVAHD_Mailbox are device accept[0x0/12]
+
+/*
+ * 20 Memory Management Units
+ */
+M3_MMU,
+DSP_MMU are device accept [0x0/12]
+
+/*
+ * 21 Spinlock
+ */
+Spinlock is device accept [0x0/12]
+
+/*
+ * 22 Timers
+ */
+/* 22.2 General Purpose Timers */
+GPTIMER{[1..11]} are device accept [0x0/12]
+
+/* 22.3 Watchdog Timers */
+WDTIMER{[2..3]} are device accept [0x0/12]
+
+/* 22.4 32-KHz Synchronized Timer */
+S32KTIMER is device accept [0x0/12]
+
+/*
+ * 23 Serial Communication Interface
+ */
+
+/* 23.1 Multimaster High-Speed I2C Controller */
+I2C{[1..4]} are device accept [0x0/8]
+
+/* 23.2 HDQ/1-Wire */
+HDQ is device accept [0x0/12]
+
+/* 23.3.1 UART/IrDA/CIR */
+UART{[1..4]} are device accept [0x0/10]
+
+/* 23.4 Mulitchannel Serial Port Interface */
+McSPI{[1..4]} are device accept [0x0/12]
+
+/* 23.5 Multichannel Buffered Serial Port */
+McBSP{[1..4]} are device accept [0x0/12]
+
+/* 23.6 Multichannel PDM Controller */
+McPDM is device accept [0x0/12]
+
+/* 23.7 Digital Microphone Module */
+DMIC is device accept [0x0/12]
+
+/* 23.8 Multichannel Audio Serial Port */
+McASP is device accept [0x0/12]
+McASP_DATA is device accept [0x0/12]
+
+/* 23.9 Serial Low-Power Inter-Chip Media Bus Controller */
+SLIMBUS{[1..2]} are device accept [0x0/12]
+
+/* 23.10 MIPI-HSI */
+HSI_TOP is device accept [0x0-0x1400]
+HSI_DMA_CHANNELS is device accept [0x0/10]
+HSI_PORTS is device accept [0x0/13]
+
+HSI is map [
+        0x0000-0x1400 to HSI_TOP
+        0x1800/10 to HSI_DMA_CHANNELS
+        0x000/13 to HSI_PORTS
+       ]
+
+/* 23.11 High-Speed Multiport USB Host Subsystem */
+HSUSBTLL is device accept [0x0/12]
+HSUSBHOST is device accept [0x0/12]
+
+/* 23.12 High-Speed USB OTG Controller */
+HSUSBOTG is device accept [0x0/12]
+USBPHY is device accept [0x0/12]
+
+/* 23.13 Full-speed USB Host Controller */
+FSUSBHOST is device accept[0x0/12]
+
+/*
+ * 24 MMC/SD/SDIO
+ */
+HSMMC{[1..2]},
+MMC_SD{[3..5]} are device accept [0x0/12]
+
+/*
+ * 25 General Purpose Interface
+ */
+GPIO{[1..6]} are device accept [0x0/12]
+
+/*
+ * 26 Keyboard Controller
+ */
+Keyboard is device accept [0x0/12]
+
+/*
+ * 28.10 On-Chip Debug Support Memory Mapping
+ */
+MIPI_STM_0 is device accept [0x0/20]
+MIPI_STM_1 is device accept [0x0/18]
+A9_CPU0_debug_PMU is device accept [0x0/13]
+A9_CPU1_debug_PMU is device accept [0x0/13]
+CTI0 is device accept [0x0/12]
+CTI1 is device accept [0x0/12]
+PTM0 is device accept [0x0/12]
+PTM1 is device accept [0x0/12]
+A9_CS-TF is device accept [0x0/12]
+DAP_PC is device accept [0x0/12]
+APB is device accept [0x0/12]
+DRM is device accept [0x0/12]
+MIPI_STM is device accept [0x0/12]
+CS-ETB is device accept [0x0/12]
+CS-TPIU is device accept [0x0/12]
+CS-TF is device accept [0x0/12]
+
+OCP-WP is device accept [0x0/12]
+
+PMI is device accept [0x0/8]
\ No newline at end of file
diff --git a/socs/omap44xx/cortexA9-subsystem.soc b/socs/omap44xx/cortexA9-subsystem.soc
new file mode 100644 (file)
index 0000000..703aaf3
--- /dev/null
@@ -0,0 +1,56 @@
+/*
+ * Copyright (c) 2017, ETH Zurich. All rights reserved.
+ *
+ * This file is distributed under the terms in the attached LICENSE file.
+ * If you do not find this file, copies can be found by writing to:
+ * ETH Zurich D-INFK, Universitaetsstrasse 6, CH-8092 Zurich.
+ * Attn: Systems Group.
+ */
+
+/**
+ * CortexA9 subsystem of TI OMAP4460 SoC
+ *
+ * This is derived from:
+ * OMAP4460 Multimedia Device Silicon Revision 1.x Technical Reference
+ * Manual Version Q
+ *
+ * Section 4
+ *
+ */
+
+import cortex/cortexA9
+
+module CortexA9-Subsystem {
+    input CPU_{[1..2]}/32
+    output L3/32, L4_ABE/20
+
+    ROM is memory accept [0x0-0xBFFF]
+
+    PL310 is device accept [0x0/12]
+    CORTEXA9_SOCKET_PRCM is device accept [0x0/9]
+    CORTEXA9_PRM is device accept [0x0/9]
+    CORTEXA9_CPU{[0..1]} are device accept [0x0/10]
+    CORTEXA9_WUGEN is device accept [0x0/12]
+    CMU is device accept [0x0/16]
+    Interconnect_config is device accept [0x0/12]
+    MA is device accept [0x0/12]
+
+    Interconnect is map [
+        0x40030000-0x4003BFFF to ROM
+        0x40100000/20 to L4_ABE
+        0x48242000/12 to PL310
+        0x48243000/9 to CORTEXA9_SOCKET_PRCM
+        0x48243200/9 to CORTEXA9_PRM
+        0x48243400/10 to CORTEXA9_CPU0
+        0x48243800/10 to CORTEXA9_CPU1
+        0x48281000/12 to CORTEXA9_WUGEN
+        0x48290000/16 to CMU
+        0x482A0000/12 to Interconnect_config
+        0x482AF000/12 to MA
+    ] over L3/32
+    
+
+    CortexA9-MPCore(2, 0x48240000) as MPU with
+        CPU_{c in [1..2]} > CPU_{c}
+        Interconnect < L2
+}
diff --git a/tools/sockeye/Hakefile b/tools/sockeye/Hakefile
new file mode 100644 (file)
index 0000000..7a4ada4
--- /dev/null
@@ -0,0 +1,14 @@
+----------------------------------------------------------------------
+-- Copyright (c) 2017, ETH Zurich.
+-- All rights reserved.
+--
+-- This file is distributed under the terms in the attached LICENSE file.
+-- If you do not find this file, copies can be found by writing to:
+-- ETH Zurich D-INFK, Universitaetsstrasse 6, CH-8092 Zurich. 
+-- Attn: Systems Group.
+--
+-- Hakefile for /tools/sockeye
+--
+----------------------------------------------------------------------
+
+[ compileHaskell "sockeye" "Main.hs" (find withSuffices [ ".hs" ]) ]
\ No newline at end of file
diff --git a/tools/sockeye/Main.hs b/tools/sockeye/Main.hs
new file mode 100644 (file)
index 0000000..d96c7ed
--- /dev/null
@@ -0,0 +1,268 @@
+{-
+  SockeyeMain.hs: Sockeye
+
+  Copyright (c) 2017, ETH Zurich.
+
+  All rights reserved.
+
+  This file is distributed under the terms in the attached LICENSE file.
+  If you do not find this file, copies can be found by writing to:
+  ETH Zurich D-INFK, CAB F.78, Universitaetstr. 6, CH-8092 Zurich,
+  Attn: Systems Group.
+-}
+
+module Main where
+
+import Control.Monad
+
+import Data.List (intercalate)
+import qualified Data.Map as Map
+
+import System.Console.GetOpt
+import System.Directory
+import System.Exit
+import System.Environment
+import System.FilePath
+import System.IO
+
+import qualified SockeyeASTParser as ParseAST
+import qualified SockeyeASTTypeChecker as CheckAST
+import qualified SockeyeASTInstantiator as InstAST
+import qualified SockeyeASTDecodingNet as NetAST
+
+import SockeyeParser
+import SockeyeTypeChecker
+import SockeyeInstantiator
+import SockeyeNetBuilder
+
+import qualified SockeyeBackendProlog as Prolog
+
+{- Exit codes -}
+usageError :: ExitCode
+usageError = ExitFailure 1
+
+fileError :: ExitCode
+fileError = ExitFailure 2
+
+parseError :: ExitCode
+parseError = ExitFailure 3
+
+checkError :: ExitCode
+checkError = ExitFailure 4
+
+buildError :: ExitCode
+buildError = ExitFailure 5
+
+{- Compilation targets -}
+data Target = Prolog
+
+{- Possible options for the Sockeye Compiler -}
+data Options = Options
+    { optInputFile  :: FilePath
+    , optInclDirs   :: [FilePath]
+    , optTarget     :: Target
+    , optOutputFile :: FilePath
+    , optDepFile    :: Maybe FilePath
+    }
+
+{- Default options -}
+defaultOptions :: Options
+defaultOptions = Options
+    { optInputFile  = ""
+    , optInclDirs   = [""]
+    , optTarget     = Prolog
+    , optOutputFile = ""
+    , optDepFile    = Nothing
+    }
+
+{- Set the input file name -}
+optSetInputFileName :: FilePath -> Options -> Options
+optSetInputFileName f o = o { optInputFile = f }
+
+optAddInclDir :: FilePath -> Options -> Options
+optAddInclDir f o = o { optInclDirs = optInclDirs o ++ [f] }
+
+{- Set the target -}
+optSetTarget :: Target -> Options -> Options
+optSetTarget t o = o { optTarget = t }
+
+{- Set the output file name -}
+optSetOutputFile :: FilePath -> Options -> Options
+optSetOutputFile f o = o { optOutputFile = f }
+
+{- Set the dependency file name -}
+optSetDepFile :: FilePath -> Options -> Options
+optSetDepFile f o = o { optDepFile = Just f }
+
+{- Prints usage information possibly with usage errors -}
+usage :: [String] -> IO ()
+usage errors = do
+    prg <- getProgName
+    let usageString = "Usage: " ++ prg ++ " [options] file\nOptions:"
+    case errors of
+        [] -> return ()
+        _  -> hPutStrLn stderr $ concat errors
+    hPutStrLn stderr $ usageInfo usageString options
+    hPutStrLn stderr "The backend (capital letter options) specified last takes precedence."
+
+
+{- Setup option parser -}
+options :: [OptDescr (Options -> IO Options)]
+options = 
+    [ Option "P" ["Prolog"]
+        (NoArg (\opts -> return $ optSetTarget Prolog opts))
+        "Generate a prolog file that can be loaded into the SKB (default)."
+    , Option "i" ["include"]
+        (ReqArg (\f opts -> return $ optAddInclDir f opts) "DIR")
+        "Add a directory to the search path where Sockeye looks for imports."
+    , Option "o" ["output-file"]
+        (ReqArg (\f opts -> return $ optSetOutputFile f opts) "FILE")
+        "Output file in which to store the compilation result (required)."
+    , Option "d" ["dep-file"]
+        (ReqArg (\f opts -> return $ optSetDepFile f opts) "FILE")
+        "Generate a dependency file for GNU make"
+    , Option "h" ["help"]
+        (NoArg (\_ -> do
+                    usage []
+                    exitWith ExitSuccess))
+        "Show help."
+    ]
+
+{- evaluates the compiler options -}
+compilerOpts :: [String] -> IO (Options)
+compilerOpts argv = do
+    opts <- case getOpt Permute options argv of
+        (actions, fs, []) -> do
+            opts <- foldl (>>=) (return defaultOptions) actions
+            case fs of
+                []  -> do
+                    usage ["No input file\n"]
+                    exitWith usageError
+                [f] -> return $ optSetInputFileName f opts
+                _   -> do
+                    usage ["Multiple input files not supported\n"]
+                    exitWith usageError
+
+        (_, _, errors) -> do
+            usage errors
+            exitWith $ usageError
+    case optOutputFile opts of
+        "" -> do
+            usage ["No output file\n"]
+            exitWith $ usageError
+        _  -> return opts
+
+{- Parse Sockeye and resolve imports -}
+parseSpec :: [FilePath] -> FilePath -> IO (ParseAST.SockeyeSpec, [FilePath])
+parseSpec inclDirs fileName = do
+    file <- resolveFile fileName
+    specMap <- parseWithImports Map.empty file
+    let
+        specs = Map.elems specMap
+        deps = Map.keys specMap
+        topLevelSpec = specMap Map.! file
+        modules = concat $ map ParseAST.modules specs
+        spec = topLevelSpec
+            { ParseAST.imports = []
+            , ParseAST.modules = modules
+            }
+    return (spec, deps)
+    where
+        parseWithImports importMap importPath = do
+            file <- resolveFile importPath
+            if file `Map.member` importMap
+                then return importMap
+                else do
+                    ast <- parseFile file
+                    let
+                        specMap = Map.insert file ast importMap
+                        imports = ParseAST.imports ast
+                        importFiles = map ParseAST.filePath imports
+                    foldM parseWithImports specMap importFiles
+        resolveFile path = do
+            let
+                subDir = takeDirectory path
+                name = takeFileName path
+                dirs = map (</> subDir) inclDirs
+            file <- findFile dirs name
+            extFile <- findFile dirs (name <.> "soc")
+            case (file, extFile) of
+                (Just f, _) -> return f
+                (_, Just f) -> return f
+                _ -> do
+                    hPutStrLn stderr $ "'" ++ path ++ "' not on import path"
+                    exitWith fileError
+
+
+{- Runs the parser on a single file -}
+parseFile :: FilePath -> IO (ParseAST.SockeyeSpec)
+parseFile file = do
+    src <- readFile file
+    case parseSockeye file src of
+        Left err -> do
+            hPutStrLn stderr $ "Parse error at " ++ show err
+            exitWith parseError
+        Right ast -> return ast
+
+{- Runs the checker -}
+typeCheck :: ParseAST.SockeyeSpec -> IO CheckAST.SockeyeSpec
+typeCheck parsedAst = do
+    case typeCheckSockeye parsedAst of 
+        Left fail -> do
+            hPutStr stderr $ show fail
+            exitWith checkError
+        Right intermAst -> return intermAst
+
+instanitateModules :: CheckAST.SockeyeSpec -> IO InstAST.SockeyeSpec
+instanitateModules ast = do
+    case instantiateSockeye ast of 
+        Left fail -> do
+            hPutStr stderr $ show fail
+            exitWith buildError
+        Right simpleAST -> return simpleAST
+
+{- Builds the decoding net from the Sockeye AST -}
+buildNet :: InstAST.SockeyeSpec -> IO NetAST.NetSpec
+buildNet ast = do
+    case buildSockeyeNet ast of 
+        Left fail -> do
+            hPutStr stderr $ show fail
+            exitWith buildError
+        Right netAst -> return netAst
+
+{- Compiles the AST with the appropriate backend -}
+compile :: Target -> NetAST.NetSpec -> IO String
+compile Prolog ast = return $ Prolog.compile ast
+
+{- Generates a dependency file for GNU make -}
+dependencyFile :: FilePath -> FilePath -> [FilePath] -> IO String
+dependencyFile outFile depFile deps = do
+    let
+        targets = outFile ++ " " ++ depFile ++ ":"
+        lines = targets:deps
+    return $ intercalate " \\\n " lines
+
+{- Outputs the compilation result -}
+output :: FilePath -> String -> IO ()
+output outFile out = writeFile outFile out
+
+main = do
+    args <- getArgs
+    opts <- compilerOpts args
+    let
+        inFile = optInputFile opts
+        inclDirs = optInclDirs opts
+        outFile = optOutputFile opts
+        depFile = optDepFile opts
+    (parsedAst, deps) <- parseSpec inclDirs inFile
+    ast <- typeCheck parsedAst
+    instAst <- instanitateModules ast
+    netAst <- buildNet instAst
+    out <- compile (optTarget opts) netAst
+    output outFile out
+    case depFile of
+        Nothing -> return ()
+        Just f  -> do
+            out <- dependencyFile outFile f deps
+            output f out
+    
\ No newline at end of file
diff --git a/tools/sockeye/SockeyeASTDecodingNet.hs b/tools/sockeye/SockeyeASTDecodingNet.hs
new file mode 100644 (file)
index 0000000..7974fd5
--- /dev/null
@@ -0,0 +1,57 @@
+{-
+  SockeyeASTDecodingNet.hs: Decoding net AST for Sockeye
+
+  Part of Sockeye
+
+  Copyright (c) 2017, ETH Zurich.
+
+  All rights reserved.
+
+  This file is distributed under the terms in the attached LICENSE file.
+  If you do not find this file, copies can be found by writing to:
+  ETH Zurich D-INFK, CAB F.78, Universitaetstr. 6, CH-8092 Zurich,
+  Attn: Systems Group.
+-}
+
+module SockeyeASTDecodingNet where
+
+import Data.List (intercalate)
+import Data.Map (Map)
+
+type NetSpec = Map NodeId NodeSpec
+
+data NodeId = NodeId
+    { name      :: !String
+    , namespace :: [String]
+    } deriving (Eq, Ord)
+
+instance Show NodeId where
+    show (NodeId n ns) =
+        let noEmpty = filter ((> 0) . length) ns
+        in intercalate "." $ reverse (n:noEmpty)
+
+data NodeSpec = NodeSpec
+    { nodeType  :: NodeType
+    , accept    :: [BlockSpec]
+    , translate :: [MapSpec]
+    } deriving (Show)
+
+data NodeType
+    = Core
+    | Device
+    | Memory
+    | Other
+    deriving (Show)
+
+data BlockSpec = BlockSpec
+    { base  :: Address
+    , limit :: Address
+    } deriving (Show)
+
+data MapSpec = MapSpec
+    { srcBlock :: BlockSpec
+    , destNode :: NodeId
+    , destBase :: Address
+    } deriving (Show)
+
+type Address = Integer
diff --git a/tools/sockeye/SockeyeASTInstantiator.hs b/tools/sockeye/SockeyeASTInstantiator.hs
new file mode 100644 (file)
index 0000000..d6f9240
--- /dev/null
@@ -0,0 +1,90 @@
+{-
+  SockeyeASTInstantiator.hs: AST with instantiated modules for Sockeye
+
+  Part of Sockeye
+
+  Copyright (c) 2017, ETH Zurich.
+
+  All rights reserved.
+
+  This file is distributed under the terms in the attached LICENSE file.
+  If you do not find this file, copies can be found by writing to:
+  ETH Zurich D-INFK, CAB F.78, Universitaetstr. 6, CH-8092 Zurich,
+  Attn: Systems Group.
+-}
+
+module SockeyeASTInstantiator
+    ( module SockeyeASTInstantiator
+    , module SockeyeASTDecodingNet
+    ) where
+
+import Data.Map (Map)
+
+import SockeyeASTDecodingNet
+    ( NodeType(Core, Device, Memory, Other)
+    , BlockSpec(BlockSpec)
+    , base, limit
+    , Address
+    )
+
+data SockeyeSpec = SockeyeSpec
+    { root :: ModuleInst
+    , modules :: Map Identifier Module
+    } deriving (Show)
+
+data Module = Module
+    { inputPorts   :: [Port]
+    , outputPorts  :: [Port]
+    , moduleInsts  :: [ModuleInst]
+    , nodeDecls    :: [NodeDecl]
+    } deriving (Show)
+
+data Port
+    = InputPort 
+        { portId    :: Identifier
+        , portWidth :: !Integer
+        }
+    | OutputPort
+        { portId    :: Identifier
+        , portWidth :: !Integer
+        }
+    deriving (Show)
+
+data ModuleInst
+    = ModuleInst
+        { namespace  :: Maybe Identifier
+        , moduleName :: Identifier
+        , inPortMap  :: PortMap
+        , outPortMap :: PortMap
+        } deriving (Show)
+
+type PortMap = Map Identifier Identifier
+
+data NodeDecl
+    = NodeDecl
+        { nodeId   :: Identifier
+        , nodeSpec :: NodeSpec
+        } deriving (Show)
+
+type Identifier = String
+
+data NodeSpec = NodeSpec
+    { nodeType  :: NodeType
+    , accept    :: [BlockSpec]
+    , translate :: [MapSpec]
+    , reserved  :: [BlockSpec]
+    , overlay   :: Maybe OverlaySpec
+    } deriving (Show)
+
+data MapSpec 
+    = MapSpec
+        { srcBlock :: BlockSpec
+        , destNode :: !Identifier
+        , destBase :: !Address
+        } deriving (Show)
+
+data OverlaySpec
+    = OverlaySpec
+        { over  :: !Identifier
+        , width :: !Integer
+        } deriving (Show)
diff --git a/tools/sockeye/SockeyeASTParser.hs b/tools/sockeye/SockeyeASTParser.hs
new file mode 100644 (file)
index 0000000..cb182bc
--- /dev/null
@@ -0,0 +1,123 @@
+{-
+    SockeyeASTParser.hs: AST for the Sockeye parser
+
+    Part of Sockeye
+
+    Copyright (c) 2017, ETH Zurich.
+
+    All rights reserved.
+
+    This file is distributed under the terms in the attached LICENSE file.
+    If you do not find this file, copies can be found by writing to:
+    ETH Zurich D-INFK, CAB F.78, Universitaetstr. 6, CH-8092 Zurich,
+    Attn: Systems Group.
+-}
+
+module SockeyeASTParser 
+( module SockeyeASTParser
+, module SockeyeASTTypeChecker
+) where
+
+import SockeyeASTTypeChecker
+    ( Identifier(SimpleIdent, TemplateIdent)
+    , prefix, varName, suffix
+    , ModuleParamType(NaturalParam, AddressParam)
+    , ModuleArg(AddressArg, NaturalArg, ParamArg)
+    , NodeSpec(NodeSpec)
+    , nodeType, accept, translate, reserved, overlay
+    , NodeType(Core, Device, Memory, Other)
+    , BlockSpec(SingletonBlock, RangeBlock, LengthBlock)
+    , base, limit, bits
+    , MapSpec(MapSpec)
+    , OverlaySpec(OverlaySpec)
+    , over, width
+    , block, destNode, destBase
+    , Address(LiteralAddress, ParamAddress)
+    , ForLimit(LiteralLimit, ParamLimit)
+    )
+
+data SockeyeSpec = SockeyeSpec
+    { imports :: [Import]
+    , modules :: [Module]
+    , net     :: [NetSpec]
+    } deriving (Show)
+
+data Import = Import 
+    { filePath :: !FilePath }
+    deriving (Show)
+
+data Module = Module
+    { name       :: String
+    , parameters :: [ModuleParam]
+    , moduleBody :: ModuleBody
+    } deriving (Show)
+
+data ModuleParam = ModuleParam
+    { paramName :: !String
+    , paramType :: ModuleParamType
+    } deriving (Show)
+
+data ModuleBody = ModuleBody
+    { ports     :: [Port]
+    , moduleNet :: [NetSpec]
+    } deriving (Show)
+
+data NetSpec
+    = ModuleInstSpec ModuleInst
+    | NodeDeclSpec NodeDecl
+    deriving (Show)
+
+data Port
+    = InputPort 
+        { portId    :: Identifier
+        , portWidth :: !Integer
+        }
+    | OutputPort
+        { portId    :: Identifier
+        , portWidth :: !Integer
+        }
+    | MultiPort (For Port)
+    deriving (Show)
+
+data ModuleInst
+    = ModuleInst
+        { moduleName   :: String
+        , namespace    :: Identifier
+        , arguments    :: [ModuleArg]
+        , portMappings :: [PortMap]
+        }
+    | MultiModuleInst (For ModuleInst)
+    deriving (Show)
+
+data PortMap
+    = InputPortMap
+        { mappedId   :: Identifier
+        , mappedPort :: Identifier
+        }
+    | OutputPortMap
+        { mappedId   :: Identifier
+        , mappedPort :: Identifier
+        }
+    | MultiPortMap (For PortMap)
+    deriving (Show)
+
+data NodeDecl
+    = NodeDecl
+        { nodeId   :: Identifier
+        , nodeSpec :: NodeSpec
+        }
+    | MultiNodeDecl (For NodeDecl)
+    deriving (Show)
+
+data For a 
+    = For
+        { varRanges :: [ForVarRange]
+        , body      :: a
+        } deriving (Show)
+
+data ForVarRange
+    = ForVarRange
+    { var   :: !String
+    , start :: ForLimit
+    , end   :: ForLimit
+    } deriving (Show)
diff --git a/tools/sockeye/SockeyeASTTypeChecker.hs b/tools/sockeye/SockeyeASTTypeChecker.hs
new file mode 100644 (file)
index 0000000..7c45a4b
--- /dev/null
@@ -0,0 +1,157 @@
+{-
+  SockeyeASTTypeChecker.hs: Type checked AST for Sockeye
+
+  Part of Sockeye
+
+  Copyright (c) 2017, ETH Zurich.
+
+  All rights reserved.
+
+  This file is distributed under the terms in the attached LICENSE file.
+  If you do not find this file, copies can be found by writing to:
+  ETH Zurich D-INFK, CAB F.78, Universitaetstr. 6, CH-8092 Zurich,
+  Attn: Systems Group.
+-}
+
+module SockeyeASTTypeChecker
+ ( module SockeyeASTTypeChecker
+ , module SockeyeASTInstantiator
+ ) where
+
+import Data.Map (Map)
+
+import SockeyeASTInstantiator
+    ( NodeType(Core, Device, Memory, Other) )
+
+data SockeyeSpec = SockeyeSpec
+    { root    :: ModuleInst
+    , modules :: Map String Module }
+    deriving (Show)
+
+data Module = Module
+    { paramNames   :: [String]
+    , paramTypeMap :: Map String ModuleParamType
+    , ports        :: [Port]
+    , moduleInsts  :: [ModuleInst]
+    , nodeDecls    :: [NodeDecl]
+    } deriving (Show)
+
+data ModuleParamType 
+    = NaturalParam
+    | AddressParam
+    deriving (Eq)
+
+instance Show ModuleParamType where
+    show NaturalParam = "nat"
+    show AddressParam = "addr"
+
+data Port
+    = InputPort 
+        { portId    :: Identifier
+        , portWidth :: !Integer
+        }
+    | OutputPort
+        { portId    :: Identifier
+        , portWidth :: !Integer
+        }
+    | MultiPort (For Port)
+    deriving (Show)
+
+data ModuleInst
+    = ModuleInst
+        { namespace  :: Maybe Identifier
+        , moduleName :: String
+        , arguments  :: Map String ModuleArg
+        , inPortMap  :: [PortMap]
+        , outPortMap :: [PortMap]
+        }
+    | MultiModuleInst (For ModuleInst)
+    deriving (Show)
+
+data ModuleArg
+    = AddressArg !Integer
+    | NaturalArg !Integer
+    | ParamArg !String
+    deriving (Show)
+
+data PortMap
+    = PortMap
+        { mappedId   :: Identifier
+        , mappedPort :: Identifier
+        }
+    | MultiPortMap (For PortMap)
+    deriving (Show)
+
+data NodeDecl
+    = NodeDecl
+        { nodeId   :: Identifier
+        , nodeSpec :: NodeSpec
+        }
+    | MultiNodeDecl (For NodeDecl)
+    deriving (Show)
+
+data Identifier
+    = SimpleIdent 
+        { prefix  :: !String }
+    | TemplateIdent
+        { prefix  :: !String
+        , varName :: !String
+        , suffix  :: Maybe Identifier
+        }
+    deriving (Show)
+
+data NodeSpec = NodeSpec
+    { nodeType  :: NodeType
+    , accept    :: [BlockSpec]
+    , translate :: [MapSpec]
+    , reserved  :: [BlockSpec]
+    , overlay   :: Maybe OverlaySpec
+    } deriving (Show)
+
+data BlockSpec 
+    = SingletonBlock
+        { base :: Address }
+    | RangeBlock
+        { base  :: Address
+        , limit :: Address
+        }
+    | LengthBlock
+        { base :: Address
+        , bits :: !Integer
+        }
+    deriving (Show)
+
+data MapSpec 
+    = MapSpec
+        { block    :: BlockSpec
+        , destNode :: Identifier
+        , destBase :: Maybe Address
+        } deriving (Show)
+
+data OverlaySpec
+    = OverlaySpec
+        { over  :: Identifier
+        , width :: !Integer
+        } deriving (Show)
+
+data Address
+    = LiteralAddress !Integer
+    | ParamAddress !String
+    deriving (Show)
+
+data For a 
+    = For
+        { varRanges :: Map String ForRange
+        , body      :: a
+        } deriving (Show)
+
+data ForRange
+    = ForRange
+    { start :: ForLimit
+    , end   :: ForLimit
+    } deriving (Show)
+
+data ForLimit 
+    = LiteralLimit !Integer
+    | ParamLimit !String
+    deriving (Show)
diff --git a/tools/sockeye/SockeyeBackendProlog.hs b/tools/sockeye/SockeyeBackendProlog.hs
new file mode 100644 (file)
index 0000000..929ffb9
--- /dev/null
@@ -0,0 +1,120 @@
+{-
+  SockeyeBackendProlog.hs: Backend for generating ECLiPSe-Prolog facts for Sockeye
+
+  Part of Sockeye
+
+  Copyright (c) 2017, ETH Zurich.
+
+  All rights reserved.
+
+  This file is distributed under the terms in the attached LICENSE file.
+  If you do not find this file, copies can be found by writing to:
+  ETH Zurich D-INFK, CAB F.78, Universitaetstr. 6, CH-8092 Zurich,
+  Attn: Systems Group.
+-}
+
+{-# LANGUAGE TypeSynonymInstances #-}
+{-# LANGUAGE FlexibleInstances #-}
+
+module SockeyeBackendProlog
+( compile ) where
+
+import Data.Char
+import Data.List
+import qualified Data.Map as Map
+import Numeric (showHex)
+
+import qualified SockeyeASTDecodingNet as AST
+
+compile :: AST.NetSpec -> String
+compile = generate
+
+{- Code Generator -}
+class PrologGenerator a where
+    generate :: a -> String
+
+instance PrologGenerator AST.NetSpec where
+    generate net = let
+        mapped = Map.mapWithKey toFact net
+        facts = Map.elems mapped
+        in unlines facts
+        where
+            toFact nodeId nodeSpec = let
+                idString = generate nodeId
+                specString = generate nodeSpec
+                in struct "node" [("id", idString), ("spec", specString)] ++ "."
+
+instance PrologGenerator AST.NodeId where
+    generate ast = let
+        name = AST.name ast
+        namespace = AST.namespace ast
+        in struct "node_id" [("name", atom name), ("namespace", list $ map atom namespace)]
+
+instance PrologGenerator AST.NodeSpec where
+    generate ast = let
+        nodeType = generate $ AST.nodeType ast
+        accept = generate $ AST.accept ast
+        translate = generate $ AST.translate ast
+        in struct "node_spec" [("type", nodeType), ("accept", accept), ("translate", translate)]
+
+instance PrologGenerator AST.BlockSpec where
+    generate blockSpec = let
+        base = generate $ AST.base blockSpec
+        limit = generate $ AST.limit blockSpec
+        in struct "block" [("base", base), ("limit", limit)]
+
+instance PrologGenerator AST.MapSpec where
+    generate mapSpec = let
+        src  = generate $ AST.srcBlock mapSpec
+        dest = generate $ AST.destNode mapSpec
+        base = generate $ AST.destBase mapSpec
+        in struct "map" [("src_block", src), ("dest_node", dest), ("dest_base", base)]
+
+instance PrologGenerator AST.NodeType where
+    generate AST.Core   = atom "core"
+    generate AST.Device = atom "device"
+    generate AST.Memory = atom "memory"
+    generate AST.Other  = atom "other"
+
+instance PrologGenerator AST.Address where
+    generate addr = "0x" ++ showHex addr ""
+
+instance PrologGenerator a => PrologGenerator [a] where
+    generate ast = let
+        mapped = map generate ast
+        in list mapped
+
+{- Helper functions -}
+atom :: String -> String
+atom "" = ""
+atom name@(c:cs)
+    | isLower c && allAlphaNum cs = name
+    | otherwise = quotes name
+    where
+        allAlphaNum cs = foldl (\acc c -> isAlphaNum c && acc) True cs
+
+predicate :: String -> [String] -> String
+predicate name args = name ++ (parens $ intercalate "," args)
+
+struct :: String -> [(String, String)] -> String
+struct name fields = name ++ (braces $ intercalate "," (map toFieldString fields))
+    where
+        toFieldString (key, value) = key ++ ":" ++ value
+
+list :: [String] -> String
+list elems = brackets $ intercalate "," elems
+
+enclose :: String -> String -> String -> String
+enclose start end string = start ++ string ++ end
+
+parens :: String -> String
+parens = enclose "(" ")"
+
+brackets :: String -> String
+brackets = enclose "[" "]"
+
+braces :: String -> String
+braces = enclose "{" "}"
+
+quotes :: String -> String
+quotes = enclose "'" "'"
\ No newline at end of file
diff --git a/tools/sockeye/SockeyeChecks.hs b/tools/sockeye/SockeyeChecks.hs
new file mode 100644 (file)
index 0000000..da32f27
--- /dev/null
@@ -0,0 +1,72 @@
+{-
+    SockeyeChecks.hs: Helpers to run checks for Sockeye
+
+    Part of Sockeye
+
+    Copyright (c) 2017, ETH Zurich.
+
+    All rights reserved.
+
+    This file is distributed under the terms in the attached LICENSE file.
+    If you do not find this file, copies can be found by writing to:
+    ETH Zurich D-INFK, CAB F.78, Universitaetstr. 6, CH-8092 Zurich,
+    Attn: Systems Group.
+-}
+
+module SockeyeChecks where
+
+import Control.Monad.Writer
+
+import Data.List (nub, sort)
+
+data FailedCheck t = FailedCheck
+    { inModule :: !String
+    , failed   :: t
+    }
+
+newtype FailedChecks t = FailedChecks [FailedCheck t]
+
+instance (Show t) => Show (FailedChecks t) where
+    show (FailedChecks fs) = 
+        let modules = sort  (nub $  map inModule fs)
+        in unlines $ concat (map showFailsForModule modules)
+        where
+            showFailsForModule name =
+                let
+                    title = "\nIn module '" ++ name ++ "':"
+                    fails = filter (\f -> name == inModule f) fs
+                in case name of
+                    ('@':_) -> "":showFails 0 fails
+                    _       -> title:showFails 1 fails
+            showFails indentLevel fs =
+                let
+                    indent = replicate (indentLevel * 4) ' '
+                    failStrings = nub $ map showFail fs
+                in map (indent ++) failStrings
+            showFail f = (show $ failed f)
+
+type Checks f = Writer [FailedCheck f]
+
+failCheck :: String -> t -> Checks t ()
+failCheck context f = tell [FailedCheck context f]
+
+runChecks :: Checks f a -> Either (FailedChecks f) a
+runChecks checks = do
+    let
+        (a, fs) = runWriter checks
+    case fs of
+        [] -> return a
+        _  -> Left $ FailedChecks fs
+
+checkDuplicates :: (Eq a) => String  -> (a -> t) -> [a] -> (Checks t) ()
+checkDuplicates context fail xs = do
+    let
+        ds = duplicates xs
+    case ds of
+        [] -> return ()
+        _  -> mapM_ (failCheck context . fail) ds
+    where
+        duplicates [] = []
+        duplicates (x:xs)
+            | x `elem` xs = nub $ [x] ++ duplicates xs
+            | otherwise = duplicates xs
diff --git a/tools/sockeye/SockeyeInstantiator.hs b/tools/sockeye/SockeyeInstantiator.hs
new file mode 100644 (file)
index 0000000..3d6be8d
--- /dev/null
@@ -0,0 +1,387 @@
+{-
+    SockeyeInstantiator.hs: Module instantiator for Sockeye
+
+    Part of Sockeye
+
+    Copyright (c) 2017, ETH Zurich.
+
+    All rights reserved.
+
+    This file is distributed under the terms in the attached LICENSE file.
+    If you do not find this file, copies can be found by writing to:
+    ETH Zurich D-INFK, CAB F.78, Universitaetstr. 6, CH-8092 Zurich,
+    Attn: Systems Group.
+-}
+
+{-# LANGUAGE MultiParamTypeClasses #-}
+{-# LANGUAGE FlexibleInstances #-}
+{-# LANGUAGE FlexibleContexts #-}
+
+module SockeyeInstantiator
+( instantiateSockeye ) where
+
+import Control.Monad.State
+
+import Data.List (intercalate)
+import Data.Map (Map)
+import qualified Data.Map as Map
+import Data.Maybe (catMaybes, fromMaybe)
+
+import Numeric (showHex)
+
+import SockeyeChecks
+
+import qualified SockeyeASTTypeChecker as CheckAST
+import qualified SockeyeASTInstantiator as InstAST
+
+data InstFail
+    = ModuleInstLoop     [String]
+    | DuplicateNamespace !String
+    | DuplicateIdentifer !String
+    | DuplicateInPort    !String
+    | DuplicateOutPort   !String
+    | DuplicateInMap     !String !String
+    | DuplicateOutMap    !String !String
+
+instance Show InstFail where
+    show (ModuleInstLoop     loop)    = concat ["Module instantiation loop: '", intercalate "' -> '" loop, "'"]
+    show (DuplicateInPort    port)    = concat ["Multiple declarations of input port '", port, "'"]
+    show (DuplicateOutPort   port)    = concat ["Multiple declarations of output port '", port, "'"]
+    show (DuplicateNamespace ident)   = concat ["Multiple usage of namespace '", ident, "'"]
+    show (DuplicateIdentifer ident)   = concat ["Multiple declarations of node '", ident, "'"]
+    show (DuplicateInMap   inst port) = concat ["Multiple mappings for input port '",  port, "' in module instantiation '", inst, "'"]
+    show (DuplicateOutMap  inst port) = concat ["Multiple mappings for output port '", port, "' in module instantiation '", inst, "'"]
+
+type PortMapping = (InstAST.Identifier, InstAST.Identifier)
+
+data Context = Context
+    { modules     :: Map String CheckAST.Module
+    , modulePath  :: [String]
+    , paramValues :: Map String Integer
+    , varValues   :: Map String Integer
+    }
+
+instantiateSockeye :: CheckAST.SockeyeSpec -> Either (FailedChecks InstFail) InstAST.SockeyeSpec
+instantiateSockeye ast = do
+    let context = Context
+            { modules     = Map.empty
+            , modulePath  = []
+            , paramValues = Map.empty
+            , varValues   = Map.empty
+            }
+    runChecks $ evalStateT (instantiate context ast) Map.empty
+
+--
+-- Instantiate Module Templates
+--
+class Instantiatable a b where
+    instantiate :: Context -> a -> StateT (Map String InstAST.Module) (Checks InstFail) b
+
+instance Instantiatable CheckAST.SockeyeSpec InstAST.SockeyeSpec where
+    instantiate context ast = do
+        let root = CheckAST.root ast
+            mods  = CheckAST.modules ast
+            specContext = context
+                { modules = mods }
+        [instRoot] <- instantiate specContext root
+        modules <- get
+        return InstAST.SockeyeSpec
+            { InstAST.root = instRoot
+            , InstAST.modules = modules
+            }
+
+instance Instantiatable CheckAST.Module InstAST.Module where
+    instantiate context ast = do
+        let ports = CheckAST.ports ast
+            moduleInsts = CheckAST.moduleInsts ast
+            nodeDecls = CheckAST.nodeDecls ast
+            modName = head $ modulePath context
+        modules <- get
+        if modName `Map.member` modules
+            then do
+                return $ modules Map.! modName
+            else do
+                let sentinel = InstAST.Module
+                        { InstAST.inputPorts  = []
+                        , InstAST.outputPorts = []
+                        , InstAST.nodeDecls   = []
+                        , InstAST.moduleInsts = []
+                        }
+                modify $ Map.insert modName sentinel
+                (instInPorts, instOutPorts) <- do
+                    instPorts <- instantiate context ports
+                    let allPorts = concat (instPorts :: [[InstAST.Port]])
+                        inPorts = filter isInPort allPorts
+                        outPorts = filter isOutPort allPorts
+                    return (inPorts, outPorts)
+                instInsts <- do
+                    insts <- instantiate context moduleInsts
+                    return $ concat (insts :: [[InstAST.ModuleInst]])
+                instDecls <- do
+                    decls <- instantiate context nodeDecls
+                    return $ concat (decls :: [[InstAST.NodeDecl]])
+                let
+                    inPortIds = map InstAST.portId instInPorts
+                    outPortIds = map InstAST.portId instOutPorts
+                    inMapNodeIds = concat $ map (Map.elems . InstAST.inPortMap) instInsts
+                    declNodeIds = map InstAST.nodeId instDecls
+                lift $ checkDuplicates modName DuplicateInPort  inPortIds
+                lift $ checkDuplicates modName DuplicateOutPort outPortIds
+                lift $ checkDuplicates modName DuplicateNamespace (catMaybes $ map InstAST.namespace instInsts)
+                lift $ checkDuplicates modName DuplicateIdentifer $ outPortIds ++ inMapNodeIds ++ declNodeIds
+                return InstAST.Module
+                    { InstAST.inputPorts  = instInPorts
+                    , InstAST.outputPorts = instOutPorts
+                    , InstAST.nodeDecls   = instDecls
+                    , InstAST.moduleInsts = instInsts
+                    }
+        where
+            isInPort  (InstAST.InputPort  {}) = True
+            isInPort  (InstAST.OutputPort {}) = False
+            isOutPort (InstAST.InputPort  {}) = False
+            isOutPort (InstAST.OutputPort {}) = True
+
+instance Instantiatable CheckAST.Port [InstAST.Port] where
+    instantiate context (CheckAST.MultiPort for) = do
+        instFor <- instantiate context for
+        return $ concat (instFor :: [[InstAST.Port]])
+    instantiate context ast@(CheckAST.InputPort {}) = do
+        let ident = CheckAST.portId ast
+            width = CheckAST.portWidth ast
+        instIdent <- instantiate context ident
+        let instPort = InstAST.InputPort
+                { InstAST.portId    = instIdent
+                , InstAST.portWidth = width
+                }
+        return [instPort]
+    instantiate context ast@(CheckAST.OutputPort {}) = do
+        let ident = CheckAST.portId ast
+            width = CheckAST.portWidth ast
+        instIdent <- instantiate context ident
+        let instPort = InstAST.OutputPort
+                { InstAST.portId    = instIdent
+                , InstAST.portWidth = width
+                }
+        return [instPort]
+
+instance Instantiatable CheckAST.ModuleInst [InstAST.ModuleInst] where
+    instantiate context (CheckAST.MultiModuleInst for) = do 
+        simpleFor <- instantiate context for
+        return $ concat (simpleFor :: [[InstAST.ModuleInst]])
+    instantiate context ast = do
+        let namespace = CheckAST.namespace ast
+            name = CheckAST.moduleName ast
+            args = CheckAST.arguments ast
+            inPortMap = CheckAST.inPortMap ast
+            outPortMap = CheckAST.outPortMap ast
+            modPath = modulePath context
+            mod = getModule context name
+        instNs <- maybe (return Nothing) (\ns -> instantiate context ns >>= return . Just) namespace
+        instInMap <- do
+            inMaps <- instantiate context inPortMap
+            return $ concat (inMaps :: [[PortMapping]])
+        instOutMap <- do
+            outMaps <- instantiate context outPortMap
+            return $ concat (outMaps :: [[PortMapping]])
+        instArgs <- instantiate context args
+        let instName = concat [name, "(", intercalate ", " $ argStrings instArgs mod, ")"]
+            moduleContext = context
+                    { modulePath  = instName:modPath
+                    , paramValues = instArgs
+                    , varValues   = Map.empty
+                    }
+        lift $ checkSelfInst modPath instName
+        lift $ checkDuplicates (head modPath) (DuplicateInMap  instName) $ map fst instInMap
+        lift $ checkDuplicates (head modPath) (DuplicateOutMap instName) $ map fst instOutMap
+        let instantiated = InstAST.ModuleInst
+                { InstAST.moduleName = instName
+                , InstAST.namespace  = instNs
+                , InstAST.inPortMap  = Map.fromList instInMap
+                , InstAST.outPortMap = Map.fromList instOutMap
+                }
+        instModule <- instantiate moduleContext mod
+        modify $ Map.insert instName instModule
+        return [instantiated]
+        where
+            argStrings args mod =
+                let paramNames = CheckAST.paramNames mod
+                    paramTypes = CheckAST.paramTypeMap mod
+                    params = map (\p -> (p, paramTypes Map.! p)) paramNames
+                in map showValue params
+                    where
+                        showValue (name, CheckAST.AddressParam)  = "0x" ++ showHex (args Map.! name) ""
+                        showValue (name, CheckAST.NaturalParam) = show (args Map.! name)
+            checkSelfInst path name = do
+                case loop path of
+                    [] -> return ()
+                    l  -> failCheck "@all" $ ModuleInstLoop (reverse $ name:l)
+                    where
+                        loop [] = []
+                        loop path@(p:ps)
+                            | name `elem` path = p:(loop ps)
+                            | otherwise = []
+
+instance Instantiatable CheckAST.ModuleArg Integer where
+    instantiate _ (CheckAST.AddressArg value) = return value
+    instantiate _ (CheckAST.NaturalArg value) = return value
+    instantiate context (CheckAST.ParamArg name) = return $ getParamValue context name
+
+instance Instantiatable CheckAST.PortMap [PortMapping] where
+    instantiate context (CheckAST.MultiPortMap for) = do
+        instFor <- instantiate context for
+        return $ concat (instFor :: [[PortMapping]])
+    instantiate context ast = do
+        let mappedId = CheckAST.mappedId ast
+            mappedPort = CheckAST.mappedPort ast
+        instId <- instantiate context mappedId
+        instPort <- instantiate context mappedPort
+        return [(instPort, instId)]
+
+instance Instantiatable CheckAST.NodeDecl [InstAST.NodeDecl] where
+    instantiate context (CheckAST.MultiNodeDecl for) = do
+        instFor <- instantiate context for
+        return $ concat (instFor :: [[InstAST.NodeDecl]])
+    instantiate context ast = do
+        let nodeId = CheckAST.nodeId ast
+            nodeSpec = CheckAST.nodeSpec ast
+        instNodeId <- instantiate context nodeId
+        instNodeSpec <- instantiate context nodeSpec
+        let instDecl = InstAST.NodeDecl
+                { InstAST.nodeId   = instNodeId
+                , InstAST.nodeSpec = instNodeSpec
+                }
+        return $ [instDecl]
+
+instance Instantiatable CheckAST.Identifier InstAST.Identifier where
+    instantiate _ (CheckAST.SimpleIdent name) = do
+        return name
+    instantiate context ast = do
+        let prefix = CheckAST.prefix ast
+            varName = CheckAST.varName ast
+            suffix = CheckAST.suffix ast
+            varValue = show $ getVarValue context varName
+        suffixName <- case suffix of
+            Nothing -> return ""
+            Just s  -> instantiate context s
+        return $ prefix ++ varValue ++ suffixName
+
+instance Instantiatable CheckAST.NodeSpec InstAST.NodeSpec where
+    instantiate context ast = do
+        let nodeType = CheckAST.nodeType ast
+            accept = CheckAST.accept ast
+            translate = CheckAST.translate ast
+            reserved = CheckAST.reserved ast
+            overlay = CheckAST.overlay ast
+        instAccept <- instantiate context accept
+        instTranslate <- instantiate context translate
+        instReserved <- instantiate context reserved
+        instOverlay <- maybe (return Nothing) (\o -> instantiate context o >>= return . Just) overlay
+        return InstAST.NodeSpec
+            { InstAST.nodeType  = nodeType
+            , InstAST.accept    = instAccept
+            , InstAST.translate = instTranslate
+            , InstAST.reserved  = instReserved
+            , InstAST.overlay   = instOverlay
+            }
+
+instance Instantiatable CheckAST.BlockSpec InstAST.BlockSpec where
+    instantiate context (CheckAST.SingletonBlock base) = do
+        instBase <- instantiate context base
+        return InstAST.BlockSpec
+            { InstAST.base  = instBase
+            , InstAST.limit = instBase
+            }
+    instantiate context (CheckAST.RangeBlock base limit) = do
+        instBase <- instantiate context base
+        instLimit <- instantiate context limit
+        return InstAST.BlockSpec
+            { InstAST.base  = instBase
+            , InstAST.limit = instLimit
+            }
+    instantiate context (CheckAST.LengthBlock base bits) = do
+        instBase <- instantiate context base
+        let instLimit = instBase + 2^bits - 1
+        return InstAST.BlockSpec
+            { InstAST.base  = instBase
+            , InstAST.limit = instLimit
+            }
+
+instance Instantiatable CheckAST.MapSpec InstAST.MapSpec where
+    instantiate context ast = do
+        let block = CheckAST.block ast
+            destNode = CheckAST.destNode ast
+            destBase = fromMaybe (CheckAST.LiteralAddress 0) (CheckAST.destBase ast)
+        instBlock <- instantiate context block
+        instDestNode <- instantiate context destNode
+        instDestBase <- instantiate context destBase
+        return InstAST.MapSpec
+            { InstAST.srcBlock    = instBlock
+            , InstAST.destNode = instDestNode
+            , InstAST.destBase = instDestBase
+            }
+
+instance Instantiatable CheckAST.OverlaySpec InstAST.OverlaySpec where
+    instantiate context ast = do
+        let over = CheckAST.over ast
+            width = CheckAST.width ast
+        instOver <- instantiate context over
+        return InstAST.OverlaySpec
+            { InstAST.over  = instOver
+            , InstAST.width = width
+            }
+
+instance Instantiatable CheckAST.Address InstAST.Address where
+    instantiate context (CheckAST.ParamAddress name) = do
+        let value = getParamValue context name
+        return value
+    instantiate _ (CheckAST.LiteralAddress value) = return value
+
+instance Instantiatable a b => Instantiatable (CheckAST.For a) [b] where
+    instantiate context ast = do
+        let body = CheckAST.body ast
+            varRanges = CheckAST.varRanges ast
+        concreteRanges <- instantiate context varRanges
+        let valueList = Map.foldWithKey iterations [] concreteRanges
+            iterContexts = map iterationContext valueList
+        mapM (\c -> instantiate c body) iterContexts
+        where
+            iterations k vs [] = [Map.fromList [(k,v)] | v <- vs]
+            iterations k vs ms = concat $ map (f ms k) vs
+                where
+                    f ms k v = map (Map.insert k v) ms
+            iterationContext varMap =
+                let
+                    values = varValues context
+                in context
+                    { varValues = values `Map.union` varMap }
+
+instance Instantiatable CheckAST.ForRange [Integer] where
+    instantiate context ast = do
+        let start = CheckAST.start ast
+            end = CheckAST.end ast
+        simpleStart <- instantiate context start
+        simpleEnd <- instantiate context end
+        return [simpleStart..simpleEnd]
+
+instance Instantiatable CheckAST.ForLimit Integer where
+    instantiate _ (CheckAST.LiteralLimit value) = return value
+    instantiate context (CheckAST.ParamLimit name) = return $ getParamValue context name
+
+instance (Traversable t, Instantiatable a b) => Instantiatable (t a) (t b) where
+    instantiate context ast = mapM (instantiate context) ast
+
+---
+--- Helpers
+---
+getModule :: Context -> String -> CheckAST.Module
+getModule context name = (modules context) Map.! name
+
+getParamValue :: Context -> String -> Integer
+getParamValue context name =
+    let params = paramValues context
+    in params Map.! name
+
+getVarValue :: Context -> String -> Integer
+getVarValue context name =
+    let vars = varValues context
+    in vars Map.! name
diff --git a/tools/sockeye/SockeyeNetBuilder.hs b/tools/sockeye/SockeyeNetBuilder.hs
new file mode 100644 (file)
index 0000000..4bd5481
--- /dev/null
@@ -0,0 +1,329 @@
+{-
+    SockeyeNetBuilder.hs: Decoding net builder for Sockeye
+
+    Part of Sockeye
+
+    Copyright (c) 2017, ETH Zurich.
+
+    All rights reserved.
+
+    This file is distributed under the terms in the attached LICENSE file.
+    If you do not find this file, copies can be found by writing to:
+    ETH Zurich D-INFK, CAB F.78, Universitaetstr. 6, CH-8092 Zurich,
+    Attn: Systems Group.
+-}
+
+{-# LANGUAGE MultiParamTypeClasses #-}
+{-# LANGUAGE FlexibleInstances #-}
+{-# LANGUAGE FlexibleContexts #-}
+
+module SockeyeNetBuilder
+( buildSockeyeNet ) where
+
+import Control.Monad.State
+
+import Data.List (sort)
+import Data.Map (Map)
+import qualified Data.Map as Map
+import Data.Set (Set)
+import qualified Data.Set as Set
+
+import SockeyeChecks
+
+import qualified SockeyeASTInstantiator as InstAST
+import qualified SockeyeASTDecodingNet as NetAST
+
+data NetBuildFail
+    = UndefinedOutPort   !String !String
+    | UndefinedInPort    !String !String
+    | UndefinedReference !String !String
+
+instance Show NetBuildFail where
+    show (UndefinedInPort  inst port)  = concat ["Undefined input port '",   port, "' in module instantiation '", inst, "'"]
+    show (UndefinedOutPort inst port)  = concat ["Undefined output port '",  port, "' in module instantiation '", inst, "'"]
+    show (UndefinedReference context ident) = concat ["Reference to undefined node '", ident, "' in ", context]
+
+type PortMap = Map InstAST.Identifier NetAST.NodeId
+
+data Context = Context
+    { modules      :: Map InstAST.Identifier InstAST.Module
+    , curModule    :: !String
+    , curNamespace :: [String]
+    , curNode      :: !String
+    , inPortMap    :: PortMap
+    , outPortMap   :: PortMap
+    , nodes        :: Set String
+    , mappedBlocks :: [InstAST.BlockSpec]
+    }
+
+buildSockeyeNet :: InstAST.SockeyeSpec -> Either (FailedChecks NetBuildFail) NetAST.NetSpec
+buildSockeyeNet ast = do
+    let
+        context = Context
+            { modules      = Map.empty
+            , curModule    = ""
+            , curNamespace = []
+            , curNode      = ""
+            , inPortMap    = Map.empty
+            , outPortMap   = Map.empty
+            , nodes        = Set.empty
+            , mappedBlocks = []
+            }        
+    net <- runChecks $ transform context ast
+    return net
+
+--            
+-- Build net
+--
+class NetTransformable a b where
+    transform :: Context -> a -> Checks NetBuildFail b
+
+instance NetTransformable InstAST.SockeyeSpec NetAST.NetSpec where
+    transform context ast = do
+        let
+            rootInst = InstAST.root ast
+            mods = InstAST.modules ast
+            specContext = context
+                { modules = mods }
+        transform specContext rootInst
+
+instance NetTransformable InstAST.Module NetAST.NetSpec where
+    transform context ast = do
+        let inPorts = InstAST.inputPorts ast
+            outPorts = InstAST.outputPorts ast
+            moduleInsts = InstAST.moduleInsts ast
+            nodeDecls = InstAST.nodeDecls ast
+            outPortIds = map InstAST.portId outPorts
+            inMapIds = concatMap Map.elems $ map InstAST.inPortMap moduleInsts
+            declIds = map InstAST.nodeId nodeDecls
+            modContext = context
+                { nodes = Set.fromList $ outPortIds ++ inMapIds ++ declIds }
+        inPortDecls <- transform modContext inPorts
+        outPortDecls <- transform modContext outPorts
+        netDecls <- transform modContext nodeDecls
+        netInsts <- transform modContext moduleInsts     
+        return $ Map.unions (inPortDecls ++ outPortDecls ++ netDecls ++ netInsts)
+
+instance NetTransformable InstAST.Port NetAST.NetSpec where
+    transform context ast@(InstAST.InputPort {}) = do
+        let portId = InstAST.portId ast
+            portWidth = InstAST.portWidth ast
+            portMap = inPortMap context
+            mappedId = Map.lookup portId portMap
+            errorContext = "input port declaration"
+        checkReference context (UndefinedReference errorContext) portId
+        netPortId <- transform context portId
+        case mappedId of
+            Nothing    -> return Map.empty
+            Just ident -> do
+                let node = portNode netPortId portWidth
+                return $ Map.fromList [(ident, node)]
+    transform context ast@(InstAST.OutputPort {}) = do
+        let portId = InstAST.portId ast
+            portWidth = InstAST.portWidth ast
+            portMap = outPortMap context
+            mappedId = Map.lookup portId portMap
+        netPortId <- transform context portId
+        case mappedId of
+            Nothing    -> return $ Map.fromList [(netPortId, portNodeTemplate)]
+            Just ident -> do
+                let node = portNode ident portWidth
+                return $ Map.fromList $ [(netPortId, node)]
+
+portNode :: NetAST.NodeId -> Integer -> NetAST.NodeSpec
+portNode destNode width =
+    let base = 0
+        limit = 2^width - 1
+        srcBlock = NetAST.BlockSpec
+            { NetAST.base  = base
+            , NetAST.limit = limit
+            }
+        map = NetAST.MapSpec
+                { NetAST.srcBlock = srcBlock
+                , NetAST.destNode = destNode
+                , NetAST.destBase = base
+                }
+    in portNodeTemplate { NetAST.translate = [map] }
+
+portNodeTemplate :: NetAST.NodeSpec
+portNodeTemplate = NetAST.NodeSpec
+    { NetAST.nodeType  = NetAST.Other
+    , NetAST.accept    = []
+    , NetAST.translate = []
+    }
+
+instance NetTransformable InstAST.ModuleInst NetAST.NetSpec where
+    transform context ast = do
+        let name = InstAST.moduleName ast
+            namespace = InstAST.namespace ast
+            inPortMap = InstAST.inPortMap ast
+            outPortMap = InstAST.outPortMap ast
+            mod = (modules context) Map.! name
+            inPortIds = Set.fromList $ map InstAST.portId (InstAST.inputPorts mod)
+            outPortIds = Set.fromList $ map InstAST.portId (InstAST.outputPorts mod)
+            instString = concat [name, maybe  "" (" as " ++ ) namespace]
+            errorContext = concat ["port mapping for '", instString, "'"]
+        mapM_ (checkReference context $ UndefinedReference errorContext) $ (Map.elems inPortMap) ++ (Map.elems outPortMap)
+        checkAllExist (UndefinedInPort instString) inPortIds $ Map.keysSet inPortMap
+        checkAllExist (UndefinedOutPort instString) outPortIds $ Map.keysSet outPortMap
+        netInMap <- transform context inPortMap
+        netOutMap <- transform context outPortMap
+        let curNs = curNamespace context
+            instContext = context
+                { curModule    = name
+                , curNamespace = maybe curNs (:curNs) namespace
+                , inPortMap    = netInMap
+                , outPortMap   = netOutMap
+                }
+        transform instContext mod
+        where
+            checkAllExist fail existing xs = do
+                let undef = xs Set.\\ existing
+                if Set.null undef
+                    then return ()
+                    else mapM_ (failCheck (curModule context) . fail) undef
+
+instance NetTransformable InstAST.NodeDecl NetAST.NetSpec where
+    transform context ast = do
+        let nodeId = InstAST.nodeId ast
+            nodeSpec = InstAST.nodeSpec ast
+            nodeContext = context
+                { curNode = nodeId }
+        netNodeId <- transform context nodeId
+        netNodeSpec <- transform nodeContext nodeSpec
+        return $ Map.fromList [(netNodeId, netNodeSpec)]
+
+instance NetTransformable InstAST.Identifier NetAST.NodeId where
+    transform context ast = do
+        let namespace = curNamespace context
+        return NetAST.NodeId
+            { NetAST.namespace = namespace
+            , NetAST.name      = ast
+            }
+
+instance NetTransformable InstAST.NodeSpec NetAST.NodeSpec where
+    transform context ast = do
+        let
+            nodeType = InstAST.nodeType ast
+            accept = InstAST.accept ast
+            translate = InstAST.translate ast
+            reserved = InstAST.reserved ast
+            overlay = InstAST.overlay ast
+        netTranslate <- transform context translate
+        let
+            mapBlocks = map NetAST.srcBlock netTranslate
+            nodeContext = context
+                { mappedBlocks = accept ++ mapBlocks ++ reserved }
+        netOverlay <- case overlay of
+                Nothing -> return []
+                Just o  -> transform nodeContext o
+        return NetAST.NodeSpec
+            { NetAST.nodeType  = nodeType
+            , NetAST.accept    = accept
+            , NetAST.translate = netTranslate ++ netOverlay
+            }
+
+instance NetTransformable InstAST.MapSpec NetAST.MapSpec where
+    transform context ast = do
+        let
+            srcBlock = InstAST.srcBlock ast
+            destNode = InstAST.destNode ast
+            destBase = InstAST.destBase ast
+            errorContext = "tranlate set of node '" ++ curNode context ++ "'"
+        checkReference context (UndefinedReference errorContext) destNode
+        netDestNode <- transform context destNode
+        return NetAST.MapSpec
+            { NetAST.srcBlock = srcBlock
+            , NetAST.destNode = netDestNode
+            , NetAST.destBase = destBase
+            }
+
+instance NetTransformable InstAST.OverlaySpec [NetAST.MapSpec] where
+    transform context ast = do
+        let
+            over = InstAST.over ast
+            width = InstAST.width ast
+            blocks = mappedBlocks context
+            errorContext = "overlay of node '" ++ curNode context ++ "'"
+        checkReference context (UndefinedReference errorContext) over
+        netOver <- transform context over
+        let maps = overlayMaps netOver width blocks
+        return maps
+
+overlayMaps :: NetAST.NodeId -> Integer -> [NetAST.BlockSpec] -> [NetAST.MapSpec]
+overlayMaps destId width blocks =
+    let
+        blockPoints = concat $ map toScanPoints blocks
+        maxAddress = 2^width
+        overStop  = BlockStart $ maxAddress
+        scanPoints = filter ((maxAddress >=) . address) $ sort (overStop:blockPoints)
+        startState = ScanLineState
+            { insideBlocks    = 0
+            , startAddress    = 0
+            }
+    in evalState (scanLine scanPoints []) startState
+    where
+        toScanPoints (NetAST.BlockSpec base limit) =
+                [ BlockStart base
+                , BlockEnd   limit
+                ]
+        scanLine [] ms = return ms
+        scanLine (p:ps) ms = do
+            maps <- pointAction p ms
+            scanLine ps maps
+        pointAction (BlockStart a) ms = do
+            s <- get       
+            let
+                i = insideBlocks s
+                base = startAddress s
+                limit = a - 1
+            maps <- if (i == 0) && (base <= limit)
+                then
+                    let
+                        baseAddress = startAddress s
+                        limitAddress = a - 1
+                        srcBlock = NetAST.BlockSpec baseAddress limitAddress
+                        m = NetAST.MapSpec srcBlock destId baseAddress
+                    in return $ m:ms
+                else return ms
+            modify (\s -> s { insideBlocks = i + 1})
+            return maps
+        pointAction (BlockEnd a) ms = do
+            s <- get
+            let
+                i = insideBlocks s
+            put $ ScanLineState (i - 1) (a + 1)
+            return ms
+
+data StoppingPoint
+    = BlockStart { address :: !NetAST.Address }
+    | BlockEnd   { address :: !NetAST.Address }
+    deriving (Eq, Show)
+
+instance Ord StoppingPoint where
+    (<=) (BlockStart a1) (BlockEnd   a2)
+        | a1 == a2 = True
+        | otherwise = a1 <= a2
+    (<=) (BlockEnd   a1) (BlockStart a2)
+        | a1 == a2 = False
+        | otherwise = a1 <= a2
+    (<=) sp1 sp2 = (address sp1) <= (address sp2)
+
+data ScanLineState
+    = ScanLineState
+        { insideBlocks :: !Integer
+        , startAddress :: !NetAST.Address
+        } deriving (Show)
+
+instance (Traversable t, NetTransformable a b) => NetTransformable (t a)  (t b) where
+    transform context as = mapM (transform context) as
+
+
+---
+--- Helpers
+---
+checkReference :: Context -> (String -> NetBuildFail) -> String -> (Checks NetBuildFail) ()
+checkReference context fail name =
+    if name `Set.member` (nodes context)
+        then return ()
+        else failCheck (curModule context) (fail name)
diff --git a/tools/sockeye/SockeyeParser.hs b/tools/sockeye/SockeyeParser.hs
new file mode 100644 (file)
index 0000000..6797bd9
--- /dev/null
@@ -0,0 +1,423 @@
+{-
+  SockeyeParser.hs: Parser for Sockeye
+
+  Part of Sockeye
+
+  Copyright (c) 2017, ETH Zurich.
+
+  All rights reserved.
+
+  This file is distributed under the terms in the attached LICENSE file.
+  If you do not find this file, copies can be found by writing to:
+  ETH Zurich D-INFK, CAB F.78, Universitaetstr. 6, CH-8092 Zurich,
+  Attn: Systems Group.
+-}
+
+module SockeyeParser
+( parseSockeye ) where
+
+import Text.Parsec
+import qualified Text.Parsec.Token as P
+import Text.Parsec.Language (javaStyle)
+
+import qualified SockeyeASTParser as AST
+
+{- Parser main function -}
+parseSockeye :: String -> String -> Either ParseError AST.SockeyeSpec
+parseSockeye = parse sockeyeFile
+
+{- Sockeye parsing -}
+sockeyeFile = do
+    whiteSpace
+    spec <- sockeyeSpec
+    eof
+    return spec
+
+sockeyeSpec = do
+    imports <- many imports
+    modules <- many sockeyeModule
+    net <- many netSpecs
+    return AST.SockeyeSpec
+        { AST.imports = imports
+        , AST.modules = modules
+        , AST.net     = concat net
+        }
+
+imports = do
+    reserved "import"
+    path <- try importPath <?> "import path"
+    return $ AST.Import path
+
+
+sockeyeModule = do
+    reserved "module"
+    name <- moduleName
+    params <- option [] $ parens (commaSep moduleParam)
+    body <- braces moduleBody
+    return AST.Module
+        { AST.name       = name
+        , AST.parameters = params
+        , AST.moduleBody = body
+        }
+
+moduleParam = do
+    paramType <- choice [intType, addrType] <?> "parameter type"
+    paramName <- parameterName
+    return AST.ModuleParam
+        { AST.paramName = paramName
+        , AST.paramType = paramType 
+        }
+    where
+        intType = do
+            symbol "nat"
+            return AST.NaturalParam
+        addrType = do
+            symbol "addr" 
+            return AST.AddressParam
+
+moduleBody = do
+    ports <- many ports
+    net <- many netSpecs
+    return AST.ModuleBody
+        { AST.ports     = concat ports
+        , AST.moduleNet = concat net
+        }
+
+ports = choice [inputPorts, outputPorts]
+    where
+        inputPorts = do
+            reserved "input"
+            commaSep1 inDef
+        inDef = do
+            (forFn, portId) <- identifierFor
+            symbol "/"
+            portWidth <- decimal <?> "number of bits"
+            let port = AST.InputPort portId portWidth
+            case forFn of
+                Nothing -> return port
+                Just f  -> return $ AST.MultiPort (f port)
+        outputPorts = do
+            reserved "output"
+            commaSep1 outDef
+        outDef = do
+            (forFn, portId) <- identifierFor
+            symbol "/"
+            portWidth <- decimal <?> "number of bits"
+            let port = AST.OutputPort portId portWidth
+            case forFn of
+                Nothing -> return port
+                Just f  -> return $ AST.MultiPort (f port)
+
+netSpecs = choice [ inst <?> "module instantiation"
+                 , decl <?> "node declaration"
+                 ]
+    where
+        inst = do
+            moduleInst <- moduleInst
+            return $ [AST.ModuleInstSpec moduleInst]
+        decl = do
+            nodeDecls <- nodeDecls
+            return $ [AST.NodeDeclSpec decl | decl <- nodeDecls]
+
+moduleInst = do
+    (name, args) <- try $ do
+        name <- moduleName
+        args <- option [] $ parens (commaSep moduleArg)
+        symbol "as"
+        return (name, args)
+    (forFn, namespace) <- identifierFor
+    portMappings <- option [] $ symbol "with" *> many1 portMapping
+    return $ let
+        moduleInst = AST.ModuleInst
+            { AST.moduleName = name
+            , AST.namespace  = namespace
+            , AST.arguments  = args 
+            , AST.portMappings = portMappings
+            }
+        in case forFn of
+            Nothing -> moduleInst
+            Just f  -> AST.MultiModuleInst $ f moduleInst
+
+moduleArg = choice [addressArg, numberArg, paramArg]
+    where
+        addressArg = do
+            addr <- addressLiteral
+            return $ AST.AddressArg addr
+        numberArg = do
+            num <- numberLiteral
+            return $ AST.NaturalArg num
+        paramArg = do
+            name <- parameterName
+            return $ AST.ParamArg name
+
+portMapping = choice [inputMapping, outputMapping]
+    where
+        inputMapping = do
+            (forFn, mappedId) <- try $ identifierFor <* symbol ">"
+            portId <- identifier
+            return $ let
+                portMap = AST.InputPortMap
+                    { AST.mappedId   = mappedId
+                    , AST.mappedPort = portId
+                    }
+                in case forFn of
+                    Nothing -> portMap
+                    Just f  -> AST.MultiPortMap $ f portMap
+        outputMapping = do
+            (forFn, mappedId) <- try $ identifierFor <* symbol "<"
+            portId <- identifier
+            return $ let
+                portMap = AST.OutputPortMap
+                    { AST.mappedId   = mappedId
+                    , AST.mappedPort = portId
+                    }
+                in case forFn of
+                    Nothing -> portMap
+                    Just f  -> AST.MultiPortMap $ f portMap
+
+nodeDecls = do
+    nodeIds <- choice [try single, try multiple]
+    nodeSpec <- nodeSpec
+    return $ map (toNodeDecl nodeSpec) nodeIds
+    where
+        single = do
+            nodeId <- identifier
+            reserved "is"
+            return [(Nothing, nodeId)]
+        multiple = do
+            nodeIds <- commaSep1 identifierFor
+            reserved "are"
+            return nodeIds
+        toNodeDecl nodeSpec (forFn, ident) = let
+            nodeDecl = AST.NodeDecl
+                { AST.nodeId = ident
+                , AST.nodeSpec = nodeSpec
+                }
+            in case forFn of
+                Nothing -> nodeDecl
+                Just f  -> AST.MultiNodeDecl $ f nodeDecl
+
+identifier = do
+    (_, ident) <- identifierHelper False
+    return ident
+
+nodeSpec = do
+    nodeType <- option AST.Other $ try nodeType
+    accept <- option [] accept 
+    translate <- option [] tranlsate
+    reserve <- option [] reserve
+    overlay <- optionMaybe overlay
+    return AST.NodeSpec 
+        { AST.nodeType  = nodeType
+        , AST.accept    = accept
+        , AST.translate = translate
+        , AST.reserved  = reserve
+        , AST.overlay   = overlay
+        }
+    where
+        accept = do
+            try $ reserved "accept"
+            brackets $ many blockSpec
+        tranlsate = do
+            try $ reserved "map"
+            specs <- brackets $ many mapSpecs
+            return $ concat specs
+        reserve = do
+            try $ reserved "reserved"
+            brackets $ many blockSpec
+
+nodeType = choice [core, device, memory]
+    where
+        core = do
+            symbol "core"
+            return AST.Core
+        device = do
+            symbol "device"
+            return AST.Device
+        memory = do
+            symbol "memory"
+            return AST.Memory
+
+blockSpec = choice [range, length, singleton]
+    where
+        singleton = do
+            address <- address
+            return $ AST.SingletonBlock address
+        range = do
+            base <- try $ address <* symbol "-"
+            limit <- address
+            return $ AST.RangeBlock base limit
+        length = do
+            base <- try $ address <* symbol "/"
+            bits <- decimal <?> "number of bits"
+            return $ AST.LengthBlock base bits
+
+address = choice [address, param]
+    where
+        address = do
+            addr <- addressLiteral
+            return $ AST.LiteralAddress addr
+        param = do
+            name <- parameterName
+            return $ AST.ParamAddress name
+
+mapSpecs = do
+    block <- blockSpec
+    reserved "to"
+    dests <- commaSep1 $ mapDest
+    return $ map (toMapSpec block) dests
+    where
+        mapDest = do
+            destNode <- identifier
+            destBase <- optionMaybe $ reserved "at" *> address
+            return (destNode, destBase)
+        toMapSpec block (destNode, destBase) = AST.MapSpec
+            { AST.block    = block
+            , AST.destNode = destNode
+            , AST.destBase = destBase
+            }
+
+overlay = do
+    reserved "over"
+    over <- identifier
+    symbol "/"
+    width <- decimal <?> "number of bits"
+    return AST.OverlaySpec
+        { AST.over  = over
+        , AST.width = width
+        }
+
+identifierFor = identifierHelper True
+
+forVarRange optVarName
+    | optVarName = do 
+        var <- option "#" (try $ variableName <* reserved "in")
+        range var
+    | otherwise = do
+        var <- variableName
+        reserved "in"
+        range var
+    where
+        range var = brackets (do
+            start <- index
+            symbol ".."
+            end <- index
+            return AST.ForVarRange
+                { AST.var   = var
+                , AST.start = start
+                , AST.end   = end
+                }
+            )
+            <?> "range ([a..b])"
+        index = choice [numberIndex, paramIndex]
+        numberIndex = do
+            num <- numberLiteral
+            return $ AST.LiteralLimit num
+        paramIndex = do
+            name <- parameterName
+            return $ AST.ParamLimit name
+
+{- Helper functions -}
+lexer = P.makeTokenParser (
+    javaStyle  {
+        {- list of reserved Names -}
+        P.reservedNames = keywords,
+
+        {- valid identifiers -}
+        P.identStart = letter,
+        P.identLetter = identLetter,
+
+        {- comment start and end -}
+        P.commentStart = "/*",
+        P.commentEnd = "*/",
+        P.commentLine = "//",
+        P.nestedComments = False
+    })
+
+whiteSpace    = P.whiteSpace lexer
+reserved      = P.reserved lexer
+parens        = P.parens lexer
+brackets      = P.brackets lexer
+braces        = P.braces lexer
+symbol        = P.symbol lexer
+commaSep      = P.commaSep lexer
+commaSep1     = P.commaSep1 lexer
+identString   = P.identifier lexer
+hexadecimal   = symbol "0" *> P.hexadecimal lexer <* whiteSpace
+decimal       = P.decimal lexer <* whiteSpace
+
+keywords = ["import", "module",
+            "input", "output",
+            "in",
+            "as", "with",
+            "is", "are",
+            "accept", "map",
+            "reserved", "over",
+            "to", "at"]   
+
+identStart     = letter
+identLetter    = alphaNum <|> char '_' <|> char '-'
+
+importPath     = many (identLetter <|> char '/') <* whiteSpace
+moduleName     = identString <?> "module name"
+parameterName  = identString <?> "parameter name"
+variableName   = identString <?> "variable name"
+identifierName = try ident <?> "identifier"
+    where
+        ident = do
+            start <- identStart
+            rest <- many identLetter
+            let ident = start:rest
+            if ident `elem` keywords
+                then unexpected $ "reserved word \"" ++ ident ++ "\""
+                else return ident
+
+numberLiteral  = try decimal <?> "number literal"
+addressLiteral = try hexadecimal <?> "address literal (hex)"
+
+identifierHelper inlineFor = do
+    (varRanges, Just ident) <- choice [template identifierName, simple identifierName] <* whiteSpace
+    let
+        forFn = case varRanges of
+         [] -> Nothing
+         _  -> Just $ \body -> AST.For
+                { AST.varRanges = varRanges
+                , AST.body      = body
+                }
+    return (forFn, ident)
+    where
+        simple ident = do
+            name <- ident
+            return $ ([], Just $ AST.SimpleIdent name)
+        template ident = do
+            prefix <- try $ ident <* symbol "{"
+            (ranges, varName, suffix) <- if inlineFor 
+                then choice [forTemplate, varTemplate]
+                else varTemplate
+            let
+                ident = Just AST.TemplateIdent
+                    { AST.prefix = prefix
+                    , AST.varName = varName
+                    , AST.suffix = suffix
+                    }
+            return (ranges, ident)
+        varTemplate = do
+            varName <- variableName
+            char '}'
+            (ranges, suffix) <- templateSuffix
+            return (ranges, varName, suffix)
+        forTemplate = do
+            optVarRange <- forVarRange True
+            char '}'
+            (subRanges, suffix) <- templateSuffix
+            return $ let
+                varName = mapOptVarName subRanges (AST.var optVarRange)
+                varRange = optVarRange { AST.var = varName }
+                ranges = varRange:subRanges
+                in (ranges, varName, suffix)
+        templateSuffix = option ([], Nothing) $ choice
+            [ template $ many identLetter
+            , simple $ many1 identLetter
+            ]
+        mapOptVarName prev "#" = "#" ++ (show $ (length prev) + 1)
+        mapOptVarName _ name = name
diff --git a/tools/sockeye/SockeyeTypeChecker.hs b/tools/sockeye/SockeyeTypeChecker.hs
new file mode 100644 (file)
index 0000000..e04dc29
--- /dev/null
@@ -0,0 +1,451 @@
+{-
+    SockeyeChecker.hs: AST checker for Sockeye
+
+    Part of Sockeye
+
+    Copyright (c) 2017, ETH Zurich.
+
+    All rights reserved.
+
+    This file is distributed under the terms in the attached LICENSE file.
+    If you do not find this file, copies can be found by writing to:
+    ETH Zurich D-INFK, CAB F.78, Universitaetstr. 6, CH-8092 Zurich,
+    Attn: Systems Group.
+-}
+
+{-# LANGUAGE MultiParamTypeClasses #-}
+{-# LANGUAGE FlexibleInstances #-}
+{-# LANGUAGE FlexibleContexts #-}
+
+module SockeyeTypeChecker
+( typeCheckSockeye ) where
+
+import Control.Monad
+
+import Data.Map(Map)
+import qualified Data.Map as Map
+import Data.Set (Set)
+import qualified Data.Set as Set
+import Data.Either
+
+import SockeyeChecks
+
+import qualified SockeyeASTParser as ParseAST
+import qualified SockeyeASTTypeChecker as CheckAST
+
+data TypeCheckFail
+    = DuplicateModule String
+    | DuplicateParameter String
+    | DuplicateVariable String
+    | NoSuchModule String
+    | NoSuchParameter String
+    | NoSuchVariable String
+    | ParamTypeMismatch String CheckAST.ModuleParamType CheckAST.ModuleParamType
+    | WrongNumberOfArgs String Int Int
+    | ArgTypeMismatch String String CheckAST.ModuleParamType CheckAST.ModuleParamType
+
+instance Show TypeCheckFail where
+    show (DuplicateModule name)    = concat ["Multiple definitions for module '", name, "'"]
+    show (DuplicateParameter name) = concat ["Multiple parameters named '", name, "'"]
+    show (DuplicateVariable name)  = concat ["Multiple definitions for variable '", name, "'"]
+    show (NoSuchModule name)       = concat ["No definition for module '", name, "'"]
+    show (NoSuchParameter name)    = concat ["Parameter '", name, "' not in scope"]
+    show (NoSuchVariable name)     = concat ["Variable '", name, "' not in scope"]
+    show (WrongNumberOfArgs name takes given) = concat ["Module '", name, "' takes ", show takes, " argument(s), given ", show given]
+    show (ParamTypeMismatch name expected actual) =
+        concat ["Expected type '", show expected, "' but '", name, "' has type '", show actual, "'"]
+    show (ArgTypeMismatch modName name expected actual) =
+        concat ["Type mismatch for argument '", name, "' for module '", modName, "': Expected '", show expected, "', given '", show actual, "'"]
+
+data ModuleSymbol = ModuleSymbol
+    { paramNames :: [String]
+    , paramTypes :: Map String CheckAST.ModuleParamType
+    }
+type SymbolTable = Map String ModuleSymbol
+
+data Context = Context
+    { symTable   :: SymbolTable
+    , curModule  :: !String
+    , instModule :: !String
+    , vars       :: Set String
+    }
+
+typeCheckSockeye :: ParseAST.SockeyeSpec -> Either (FailedChecks TypeCheckFail) CheckAST.SockeyeSpec
+typeCheckSockeye ast = do
+    symbolTable <- runChecks $ buildSymbolTable ast
+    let context = Context
+            { symTable   = symbolTable
+            , curModule  = ""
+            , instModule = ""
+            , vars       = Set.empty
+            }
+    runChecks $ check context ast
+
+--
+-- Build Symbol table
+--
+class SymbolSource a where
+    buildSymbolTable :: a -> Checks TypeCheckFail SymbolTable
+
+instance SymbolSource ParseAST.SockeyeSpec where
+    buildSymbolTable ast = do
+        let mods = ParseAST.modules ast
+        symbolTables <- mapM buildSymbolTable mods
+        let names = concat $ map Map.keys symbolTables
+        checkDuplicates "@all" DuplicateModule names
+        return $ Map.unions symbolTables
+        
+instance SymbolSource ParseAST.Module where
+    buildSymbolTable ast = do
+        let modName = ParseAST.name ast
+            params = ParseAST.parameters ast
+            names = map ParseAST.paramName params
+            types = map ParseAST.paramType params
+        checkDuplicates modName DuplicateParameter names
+        let typeMap = Map.fromList $ zip names types
+            modSymbol = ModuleSymbol
+                { paramNames = names
+                , paramTypes = typeMap
+                }
+        return $ Map.singleton modName modSymbol
+
+--
+-- Check module bodies
+--
+class Checkable a b where
+    check :: Context -> a -> Checks TypeCheckFail b
+
+instance Checkable ParseAST.SockeyeSpec CheckAST.SockeyeSpec where
+    check context ast = do
+        let mods = ParseAST.modules ast
+            rootNetSpecs = ParseAST.net ast
+            names = map ParseAST.name mods
+            rootName = "@root"
+            rootSymbol = ModuleSymbol
+                { paramNames = []
+                , paramTypes = Map.empty
+                }
+            rootModContext = context
+                { symTable = Map.insert rootName rootSymbol $ symTable context
+                , curModule = rootName
+                }
+        checkedRootNetSpecs <- check rootModContext rootNetSpecs
+        checkedModules <- check context mods
+        let root = CheckAST.ModuleInst
+                { CheckAST.namespace  = Nothing
+                , CheckAST.moduleName = rootName
+                , CheckAST.arguments  = Map.empty
+                , CheckAST.inPortMap  = []
+                , CheckAST.outPortMap = []
+                }
+            rootModule = CheckAST.Module
+                { CheckAST.paramNames   = []
+                , CheckAST.paramTypeMap = Map.empty
+                , CheckAST.ports        = []
+                , CheckAST.nodeDecls    = lefts  checkedRootNetSpecs
+                , CheckAST.moduleInsts  = rights checkedRootNetSpecs
+                }
+            moduleMap = Map.fromList $ zip (rootName:names) (rootModule:checkedModules)
+        return CheckAST.SockeyeSpec
+            { CheckAST.root    = root
+            , CheckAST.modules = moduleMap
+            }
+
+instance Checkable ParseAST.Module CheckAST.Module where
+    check context ast = do
+        let
+            name = ParseAST.name ast
+            body = ParseAST.moduleBody ast
+            ports = ParseAST.ports body
+            netSpecs = ParseAST.moduleNet body
+            symbol = (symTable context) Map.! name
+        let bodyContext = context
+                { curModule = name }
+        checkedPorts <- check bodyContext ports
+        checkedNetSpecs <- check bodyContext netSpecs
+        let
+            checkedNodeDecls = lefts checkedNetSpecs
+            checkedModuleInsts = rights checkedNetSpecs
+        return CheckAST.Module
+            { CheckAST.paramNames   = paramNames symbol
+            , CheckAST.paramTypeMap = paramTypes symbol
+            , CheckAST.ports        = checkedPorts
+            , CheckAST.nodeDecls    = checkedNodeDecls
+            , CheckAST.moduleInsts  = checkedModuleInsts
+            }
+
+instance Checkable ParseAST.Port CheckAST.Port where
+    check context (ParseAST.InputPort portId portWidth) = do
+        checkedId <- check context portId
+        return $ CheckAST.InputPort checkedId portWidth
+    check context (ParseAST.OutputPort portId portWidth) = do
+        checkedId <- check context portId
+        return $ CheckAST.OutputPort checkedId portWidth
+    check context (ParseAST.MultiPort for) = do
+        checkedFor <- check context for
+        return $ CheckAST.MultiPort checkedFor
+
+instance Checkable ParseAST.NetSpec (Either CheckAST.NodeDecl CheckAST.ModuleInst) where
+    check context (ParseAST.NodeDeclSpec decl) = do
+        checkedDecl <- check context decl
+        return $ Left checkedDecl
+    check context (ParseAST.ModuleInstSpec inst) = do
+        checkedInst <- check context inst
+        return $ Right checkedInst
+
+instance Checkable ParseAST.ModuleInst CheckAST.ModuleInst where
+    check context (ParseAST.MultiModuleInst for) = do
+        checkedFor <- check context for
+        return $ CheckAST.MultiModuleInst checkedFor
+    check context ast = do
+        let
+            namespace = ParseAST.namespace ast
+            name = ParseAST.moduleName ast
+            arguments = ParseAST.arguments ast
+            portMaps = ParseAST.portMappings ast
+        checkedArgs <- if Map.member name (symTable context)
+            then check (context { instModule = name }) arguments
+            else do
+                failCheck (curModule context) $ NoSuchModule name
+                return Map.empty
+        checkedNamespace <- check context namespace
+        inPortMap  <- check context $ filter isInMap  portMaps
+        outPortMap <- check context $ filter isOutMap portMaps
+        return CheckAST.ModuleInst
+            { CheckAST.namespace  = Just checkedNamespace
+            , CheckAST.moduleName = name
+            , CheckAST.arguments  = checkedArgs
+            , CheckAST.inPortMap  = inPortMap
+            , CheckAST.outPortMap = outPortMap
+            }
+        where
+            isInMap  (ParseAST.InputPortMap  {}) = True
+            isInMap  (ParseAST.OutputPortMap {}) = False
+            isInMap  (ParseAST.MultiPortMap for) = isInMap $ ParseAST.body for
+            isOutMap (ParseAST.InputPortMap  {}) = False
+            isOutMap (ParseAST.OutputPortMap {}) = True
+            isOutMap (ParseAST.MultiPortMap for) = isOutMap $ ParseAST.body for
+
+instance Checkable [ParseAST.ModuleArg] (Map String CheckAST.ModuleArg) where
+    check context ast = do
+        let symbol = (symTable context) Map.! instName
+            names = paramNames symbol
+            expTypes = map (paramTypes symbol Map.!) names
+        checkArgCount names ast
+        checkedArgs <- zipWithM checkArgType (zip names expTypes) ast
+        return $ Map.fromList $ zip names checkedArgs
+        where
+            checkArgCount params args = do
+                let
+                    paramc = length params
+                    argc = length args
+                if argc == paramc
+                    then return ()
+                    else failCheck curName $ WrongNumberOfArgs instName paramc argc
+            checkArgType (name, expType) arg = do
+                case arg of
+                    ParseAST.AddressArg value -> do
+                        if expType == CheckAST.AddressParam
+                            then return $ CheckAST.AddressArg value
+                            else do
+                                mismatch CheckAST.AddressParam
+                                return $ CheckAST.AddressArg value
+                    ParseAST.NaturalArg value -> do
+                        if expType == CheckAST.NaturalParam
+                            then return $ CheckAST.NaturalArg value
+                            else do
+                                mismatch CheckAST.NaturalParam
+                                return $ CheckAST.AddressArg value
+                    ParseAST.ParamArg paramName -> do
+                        checkParamType context paramName expType
+                        return $ CheckAST.ParamArg paramName
+                where
+                    mismatch = failCheck curName . ArgTypeMismatch instName name expType
+            curName = curModule context
+            instName = instModule context
+
+instance Checkable ParseAST.PortMap CheckAST.PortMap where
+    check context (ParseAST.MultiPortMap for) = do
+        checkedFor <- check context for
+        return $ CheckAST.MultiPortMap checkedFor
+    check context portMap = do
+        let
+            mappedId = ParseAST.mappedId portMap
+            mappedPort = ParseAST.mappedPort portMap
+        checkedId <- check context mappedId
+        checkedPort <- check context mappedPort
+        return $ CheckAST.PortMap
+            { CheckAST.mappedId   = checkedId
+            , CheckAST.mappedPort = checkedPort
+            }
+
+instance Checkable ParseAST.NodeDecl CheckAST.NodeDecl where
+    check context (ParseAST.MultiNodeDecl for) = do
+        checkedFor <- check context for
+        return $ CheckAST.MultiNodeDecl checkedFor
+    check context ast = do
+        let
+            nodeId = ParseAST.nodeId ast
+            nodeSpec = ParseAST.nodeSpec ast
+        checkedId <- check context nodeId
+        checkedSpec <- check context nodeSpec
+        return CheckAST.NodeDecl
+            { CheckAST.nodeId   = checkedId
+            , CheckAST.nodeSpec = checkedSpec
+            }
+
+instance Checkable ParseAST.Identifier CheckAST.Identifier where
+    check _ (ParseAST.SimpleIdent name) = return $ CheckAST.SimpleIdent name
+    check context ast = do
+        let
+            prefix = ParseAST.prefix ast
+            varName = ParseAST.varName ast
+            suffix = ParseAST.suffix ast
+        checkVarInScope context varName
+        checkedSuffix <- case suffix of
+            Nothing    -> return Nothing
+            Just ident -> do
+                checkedIdent <- check context ident
+                return $ Just checkedIdent
+        return CheckAST.TemplateIdent
+            { CheckAST.prefix  = prefix
+            , CheckAST.varName = varName
+            , CheckAST.suffix  = checkedSuffix
+            }
+
+instance Checkable ParseAST.NodeSpec CheckAST.NodeSpec where
+    check context ast = do
+        let 
+            nodeType = ParseAST.nodeType ast
+            accept = ParseAST.accept ast
+            translate = ParseAST.translate ast
+            overlay = ParseAST.overlay ast
+            reserved = ParseAST.reserved ast
+        checkedAccept <- check context accept
+        checkedTranslate <- check context translate
+        checkedReserved <- check context reserved
+        checkedOverlay <- case overlay of
+            Nothing    -> return Nothing
+            Just ident -> do
+                checkedIdent <- check context ident
+                return $ Just checkedIdent
+        return CheckAST.NodeSpec
+            { CheckAST.nodeType  = nodeType
+            , CheckAST.accept    = checkedAccept
+            , CheckAST.translate = checkedTranslate
+            , CheckAST.reserved  = checkedReserved
+            , CheckAST.overlay   = checkedOverlay
+            }
+
+instance Checkable ParseAST.BlockSpec CheckAST.BlockSpec where
+    check context (ParseAST.SingletonBlock address) = do
+        checkedAddress <- check context address
+        return CheckAST.SingletonBlock
+            { CheckAST.base = checkedAddress }
+    check context (ParseAST.RangeBlock base limit) = do
+        checkedBase <- check context base
+        checkedLimit <- check context limit
+        return CheckAST.RangeBlock
+            { CheckAST.base  = checkedBase
+            , CheckAST.limit = checkedLimit
+            }
+    check context (ParseAST.LengthBlock base bits) = do
+        checkedBase <- check context base
+        return CheckAST.LengthBlock
+            { CheckAST.base = checkedBase
+            , CheckAST.bits = bits
+            }
+
+instance Checkable ParseAST.MapSpec CheckAST.MapSpec where
+    check context ast = do
+        let
+            block = ParseAST.block ast
+            destNode = ParseAST.destNode ast
+            destBase = ParseAST.destBase ast
+        checkedBlock <- check context block
+        checkedDestNode <- check context destNode
+        checkedDestBase <- case destBase of
+            Nothing      -> return Nothing
+            Just address -> do
+                checkedAddress <- check context address
+                return $ Just checkedAddress
+        return CheckAST.MapSpec
+            { CheckAST.block    = checkedBlock
+            , CheckAST.destNode = checkedDestNode
+            , CheckAST.destBase = checkedDestBase
+            }
+
+instance Checkable ParseAST.OverlaySpec CheckAST.OverlaySpec where
+    check context (ParseAST.OverlaySpec over width) = do
+        checkedOver <- check context over
+        return $ CheckAST.OverlaySpec checkedOver width
+
+instance Checkable ParseAST.Address CheckAST.Address where
+    check _ (ParseAST.LiteralAddress value) = do
+        return $ CheckAST.LiteralAddress value
+    check context (ParseAST.ParamAddress name) = do
+        checkParamType context name CheckAST.AddressParam
+        return $ CheckAST.ParamAddress name
+
+instance Checkable a b => Checkable (ParseAST.For a) (CheckAST.For b) where
+    check context ast = do
+        let
+            varRanges = ParseAST.varRanges ast
+            varNames = map ParseAST.var varRanges
+            body = ParseAST.body ast
+            currentVars = vars context
+        checkDuplicates (curModule context) DuplicateVariable (varNames ++ Set.elems currentVars)
+        ranges <- check context varRanges
+        let
+            bodyVars = currentVars `Set.union` (Set.fromList varNames)
+            bodyContext = context
+                { vars = bodyVars }
+        checkedBody <- check bodyContext body
+        let
+            checkedVarRanges = Map.fromList $ zip varNames ranges
+        return CheckAST.For
+                { CheckAST.varRanges = checkedVarRanges
+                , CheckAST.body      = checkedBody
+                }
+
+instance Checkable ParseAST.ForVarRange CheckAST.ForRange where
+    check context ast = do
+        let 
+            start = ParseAST.start ast
+            end = ParseAST.end ast
+        checkedStart <- check context start
+        checkedEnd<- check context end
+        return CheckAST.ForRange
+            { CheckAST.start = checkedStart
+            , CheckAST.end   = checkedEnd
+            }
+
+instance Checkable ParseAST.ForLimit CheckAST.ForLimit where
+    check _ (ParseAST.LiteralLimit value) = do
+        return $ CheckAST.LiteralLimit value
+    check context (ParseAST.ParamLimit name) = do
+        checkParamType context name CheckAST.NaturalParam
+        return $ CheckAST.ParamLimit name
+
+instance (Traversable t, Checkable a b) => Checkable (t a) (t b) where
+    check context as = mapM (check context) as
+
+--
+-- Helpers
+--    
+checkVarInScope :: Context -> String -> Checks TypeCheckFail ()
+checkVarInScope context name = do
+    if name `Set.member` (vars context)
+        then return ()
+        else failCheck (curModule context) $ NoSuchVariable name
+
+
+checkParamType :: Context -> String -> CheckAST.ModuleParamType -> Checks TypeCheckFail ()
+checkParamType context name expected = do
+    let symbol = (symTable context) Map.! (curModule context)
+    case Map.lookup name $ paramTypes symbol of
+        Nothing -> failCheck (curModule context) $ NoSuchParameter name
+        Just actual -> do
+            if actual == expected
+                then return ()
+                else failCheck (curModule context) $ ParamTypeMismatch name expected actual
index 3a768ac..c188504 100644 (file)
@@ -12,6 +12,7 @@
 
 let ramfs_files = find inDir "programs" ".pl" ++
                   find inDir ("programs" </> "platforms") ".pl"
+    sockeyeFiles = [ "omap44xx" ]
     ramdisk = "/skb_ramfs.cpio.gz"
     args arch = application {
                         target = "skb",
@@ -37,5 +38,6 @@ in
     Rule ( [ Str "bash",
              In SrcTree "src" "skripts/mkcpio",
              NoDep SrcTree "src" "", Out "root" ramdisk]
-             ++ [ In SrcTree "src" f | f <- ramfs_files ] )
+             ++ [ In SrcTree "src" f | f <- ramfs_files ]
+             ++ [ In BuildTree "" (sockeyeFactFilePath f) | f <- sockeyeFiles ] )
   ]
diff --git a/usr/skb/programs/decoding_net.pl b/usr/skb/programs/decoding_net.pl
new file mode 100644 (file)
index 0000000..b4b5fd5
--- /dev/null
@@ -0,0 +1,153 @@
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+% Copyright (c) 2017, ETH Zurich.
+% All rights reserved.
+%
+% This file is distributed under the terms in the attached LICENSE file.
+% If you do not find this file, copies can be found by writing to:
+% ETH Zurich D-INFK, Universitaetsstrasse 6, CH-8092 Zurich.
+% Attn: Systems Group.
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+
+:- module(decoding_net).
+:- export load_net/1.
+:- export decodes_to/2.
+:- export resolve/2.
+:- export node/2.
+
+:- dynamic node/2.
+
+:- export struct(node(id:node_id,spec:node_spec)).
+:- export struct(node_id(name,namespace)).
+:- export struct(node_spec(type,accept,translate)).
+:- local struct(map(src_block,dest_node,dest_base)).
+:- local struct(block(base,limit)).
+
+:- export struct(name(node_id:node_id,address)).
+:- export struct(region(node_id:node_id,base,size)).
+
+:- lib(ic).
+
+:- set_flag(syntax_option,based_bignums).
+:- set_flag(syntax_option,iso_base_prefix).
+
+%% Load a precompiled decoding net
+load_net(File) :-
+    ensure_loaded(File).
+
+%% Convert from regions to names
+to_name(Region,Name) :-
+    region{
+        node_id:Id,
+        base:Base,
+        size:Size
+    } = Region,
+    Addr #>= Base,
+    Addr #< Base + Size,
+    Name = name{
+        node_id:Id,
+        address:Addr
+    }.
+
+%% Convert from names to regions
+to_region(Name,Region) :-
+    name{
+        node_id:Id,
+        address:Addr
+    } = Name,
+    get_bounds(Addr,Min,Max),
+    Size is Max - Min + 1,
+    ( get_domain_size(Addr,Size) ->
+            Region = region{
+            node_id:Id,
+            base:Min,
+            size:Size
+        }
+    ;
+        writeln(stderr,"Name conversion to region failed: Non continuous domain for address"),
+        fail
+    ).
+
+%% Address range in block
+block_range(Block,Range) :-
+    block{
+        base:Base,
+        limit:Limit
+    } = Block,
+    Range = Base..Limit.
+
+maps_to_name([Map|_],Addr,Name) :-
+        map{
+        src_block:SrcBlock,
+        dest_node:Dest,
+        dest_base:DestBase
+    } = Map,
+    name{
+        node_id:Dest,
+        address:DestAddr
+    } = Name,
+    block_range(SrcBlock,Range),
+    Addr :: Range,
+    block{base:SrcBase} = SrcBlock,
+    DestAddr #= Addr - SrcBase + DestBase.
+
+maps_to_name([_|Maps],Addr,Name) :-
+    maps_to_name(Maps,Addr,Name).    
+
+translate(NodeSpec,Addr,Name) :-
+    node_spec{translate:Translate} = NodeSpec,
+    maps_to_name(Translate,Addr,Name).
+
+accept(NodeSpec,Addr) :-
+    node_spec{accept:Accept} = NodeSpec,
+    (
+        foreach(Block,Accept),
+        fromto([],Prev,Next,Ranges)
+    do
+        block_range(Block,Range),
+        Next = [Range|Prev]
+    ),
+    Addr :: Ranges.
+
+accepted_name(Name) :-
+    name{
+        node_id:NodeId,
+        address:Addr
+    } = Name,
+    node{
+        id:NodeId,
+        spec:NodeSpec
+    },
+    accept(NodeSpec,Addr).
+
+decode_step(SrcName,DestName) :-
+    name{
+        node_id:NodeId,
+        address:Addr
+    } = SrcName,
+    node{
+        id:NodeId,
+        spec:NodeSpec
+    },
+    translate(NodeSpec,Addr,DestName).
+
+% Reflexive, transitive closure of decode_step
+decodes_to(SrcName,DestName) :-
+    SrcName = DestName.
+
+decodes_to(SrcName,DestName) :-
+    decode_step(SrcName,Name),
+    decodes_to(Name,DestName).
+
+resolve(SrcName,DestName) :-
+    name{} = SrcName,
+    name{} = DestName,
+    decodes_to(SrcName,DestName),
+    accepted_name(DestName).
+
+resolve(SrcRegion,DestRegion) :-
+    to_name(SrcRegion,SrcName),
+    to_name(DestRegion,DestName),
+    resolve(SrcName,DestName),
+    to_region(SrcName,SrcRegion),
+    to_region(DestName,DestRegion).
+  
\ No newline at end of file
diff --git a/usr/skb/programs/decoding_net_queries.pl b/usr/skb/programs/decoding_net_queries.pl
new file mode 100644 (file)
index 0000000..114c66e
--- /dev/null
@@ -0,0 +1,46 @@
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+% Copyright (c) 2017, ETH Zurich.
+% All rights reserved.
+%
+% This file is distributed under the terms in the attached LICENSE file.
+% If you do not find this file, copies can be found by writing to:
+% ETH Zurich D-INFK, Universitaetsstrasse 6, CH-8092 Zurich.
+% Attn: Systems Group.
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+
+:- module(decoding_net_queries).
+:- export find_device_region/2.
+:- export find_memory_region/2.
+:- export find_shared_memory_region/3.
+
+:- use_module(decoding_net).
+
+
+%%%%%%%%%%%%%
+%% Queries %%
+%%%%%%%%%%%%%
+%% Address space queries
+find_device_region(SrcRegion,DestRegion) :-
+    region{node_id:DeviceId} = DestRegion,
+    node{
+        id:DeviceId,
+        type:device
+    },
+    resolve(SrcRegion,DestRegion).
+
+find_memory_region(SrcRegion,DestRegion) :-
+    region{node_id:MemoryId} = DestRegion,
+    node{
+        id:MemoryId,
+        type:memory
+    },
+    resolve(SrcRegion,DestRegion).
+
+find_shared_memory_region(SrcRegion,DestRegion,SharedRegion) :-
+    region{node_id:SharedId} = SharedRegion,
+    node{
+        id:SharedId,
+        type:memory
+    },
+    resolve(SrcRegion,SharedRegion),
+    resolve(DestRegion,SharedRegion).