next up previous contents index
Next: Kiwic Internal Operation Up: Kiwi kiwic Compiler Users' Previous: Contents   Contents   Index

Subsections

Overview Summary

Figure 1: The main flow using the default recipe (kiwic00.rcp) in the Kiwic tool.
\begin{figure*}\centerline{\epsfbox{base00.eps}}\end{figure*}

Kiwic is a compiler for the Kiwi project. It aims to produce an RTL design out of a named sub-program of a C# program.

Kiwic does not currently invoke the C# compiler: instead it reads a CIL portable assembly language file (.exe or .dll) generated by a Microsoft or Mono C# compiler.

Figure 1 shows the main flow through the tool as set up with the provided recipe file (kiwic00.rcp). This is a six stage recipe and the obj folder created by running the tool contains the log files and intermediate forms for each stage. Other output flows and formats can be deployed by changing the recipe. The dotted line shows that using the simvnl command line option the internal simulator (Diosim) can be applied to the RTL after it has been round-tripped through Verilog. For debugging, Diosim can be applied to any HPR machine intermediate form, by varying the recipe. (There's also a shortcut `-conerefine disable -repack disable -verilogen disable' that will cause diosim to run the original VM generated by the Kiwic front end without conversion to hardware).

The .NET executable is read using the Mono.Cecil front end and combined with some canned system libraries as an abstract syntax tree.

The Kiwic front end (IL elaborate stage) converts the .net AST to the internal form used by the core library, the HPR VM2 machine, which contains imperative code sections and assertions. Code sections can be in series or parallel with each other, using Occam-like SER and PAR blocks.

The front end-stage subsumes a number of variable present in the input source code, including all fixed object pointers.

The VM code emitted by Kiwic front end is a set of parallel `dic' blocks. These are `directly indexed code' arrays of imperative commands and there is one for for each user thread. These are placed in parallel using the PAR construct. Each dic array is indexed by a program counter for that thread. There is no stack or dynamic storage allocation. The statements are: assign, conditional branch, exit and calls to certain built-in functions, including hpr_testandset, hpr_printf and hpr_barrier. The expressions occurring in branch conditions, rhs of assignment and function call arguments still use all of the arithmetic and logic operators found in the IL input form. In addition, limited string handling, including a string concat function are handled, so that console output from the IL input is preserved as console output in the generated forms (eg. $display in Verilog RTL).

The conversion to FSM is described in §3.5 and is common to the h2tool flow.. Actually, that is the old scheduler and a new one is now being used.

Its output is an HPR machine stylised in that there are no program counters and every statement operates in parallel.

The output forms available include Verilog RTL, which we have used for FPGA layout. The stylised output from the FSM generation stage is readily converted to a list of Verilog blocking assignments.

Background: HPR Library and Orangepath Tool

Orangepath is a refinement framework designed for synthesis of protocols and interfaces in hardware and software forms.

Orangepath H2 represents a system as an hierarchy of abstract machines. Each machine is a database of declarations, executable code and assertions/goals. The goals are assertions about the system behaviour, input directly, or generated from compilation of temporal logic and data conservation rules into automata. Executable code can pass through the system unchanged, but any undriven internal nodes are provided with driver code that ensures the system meets its goals.

As far as possible, all operations are `src-to-src' like operations on HPR virtual machines and the operations are stored in a standard opath command format to be executed by an orangepath recipe (program of commands

The library is structured as a number of components that operate on a VM to return another VM. The opath mini-language enables a `recipe' to be run that invokes a sequence of library operations in turn. An opath recipe is held in an XML file and the default file is kiwic00.rcp.

Loops in the recipe can be user to repeat a step until a property holds.

The opath core provides command line handling so that parameters from the receipe and the command line are fed to the components. The opath core also processes a few `early args' that must be at the start of the command line. These enable the recipe file to be specified and the logging level to be set.

The Orangepath library has a number of supported input and output formats.

In this manual, we concentrate almost entirely on the .NET CIL input format and the Verilog RTL output format.

Get Started (Fsharp/Dotnet)

Kiwic is supplied as a zip file that contains folders called lib, bin, doc and so on.

Requirements: Kiwic/HPR is now implemented in Fsharp. You need a working dotnet environment (mono or windows) on your machine and if Fsharp is not locally installed you will need to add at least the FSharpCore.dll added to the kiwic/lib folder.

Kiwic uses the Mono.Cecil front end and hence the Mono.Cecil.dll is required, either installed on the machine or copied to the kiwic/lib folder.

Place the kiwic distribution somewhere on your filesystem. Let us call that place PREFIX. To run kiwic on linux you must execute the kiwic shell script

  $ $(PREFIX)/bin/kiwic ... args ...
The shellscript just contains mono $(PREFIX)/lib/kiwic.exe

Windows users can invoke the kiwic.exe executable directly.

The arguments to kiwic should either be portable assembly files (suffix .dll or .exe) or option flags prefixed with a minus sign. Generally you will supply the current design and also the kiwi.dll library as arguments.

Two common flags, always needed in the past, were -root and -vnl. But now the latter is supplied in the default recipe and instead of using the -root command line flag, the Kiwi.Hardware attribute can be put on a classes in the input program. Both methds can be used at once: all marked classes are converted to hardware, however specified.

To obtain Verilog RTL output, Kiwic used to require a source file name, a root point, saying what to compile from the source file and an output verilog netlist file name. So the most basic command line is something like

  $ $(PREFIX)/bin/kiwic tiny.exe  -root "tiny;tiny.Main" -vnl tiny.v

Given that you have a file called tiny.exe to hand, this should result in a file called tiny.v in your current directory.

To generate tiny.exe one can do the following:

$ cat > tiny.cs
using System;
class tiny
{
  public static int Main (string []argv)
  {
    Console.WriteLine("Hello World");
    return 1;
  }
}
$ gmcs tiny.cs

NB: Kiwic will write a dissasembly of the pe file to obj/ast.cil in the current folder.

Old Get Started (MOSCOW ML)

HPR was implemented in moscow ML but you should now be using the dotnet (fsharp) version. Please now ignore this section.

These instructions apply to running on koo, but should be understandable enough for self-port to other machines.

The h2tool requires the toolmisc, and h2tool directories from the usr/groups/han CVS hprls tree. Examples and documentation are in the examples and doc directories.

The kiwic tool also requires the mono directory.

Both the h2tool and the kiwic tool have separate front-end parser binaries. These must be compiled using the command make in the relevant subdirectory: h2fe or cilfe.

Before use, please set the MOSML and HPRLS shell variables

At the computer lab use:

  export MOSML=/usr/groups/theory/mosml2.01

HPRLS should be set to your copy of the H2 tool. DJG uses:

  export HPRLS=$HOME/d320/hprls

ESPRESSO should point to the unix espresso binary or be set to NULL. Espresso is not currently needed for Fsharp implementaion of HPR.

If you get this error:

  Uncaught exception:
  Fail: libmunix.so: cannot open shared object file: No such file or directory while loading C library libmunix.so

then the setting of LD_LIBRARY_PATH is not working.

The following env vars should be sufficient for the kiwic command to be run in any directory:

export HPRLS=/usr/local/hprls/hprls for current 'stable' release
or
export HPRLS=/home/djg11/d320/hprls for djg latest live version

also

export MOSML=/usr/local/mosml2.01

Basic invocation, in any directory where the source .il file resides

   $(HPRLS)/mono/kiwic TimesTable.il -root `TimesTable;TimesTable.Main' -vnl TimesTable.v
See also $HPRLS/mono/README

To compile a .il file from C# using the Kiwi attribute library, the following sequence of commands can be used:

   KLIB=$(PREFIX)/support/attribute_definitions.dll
   KIWIC=$(PREFIX)/bin/kiwic  $(KLIB)
   ROOT=-root 'DVI4.DVI_Ports;DVI4.Generator.Generate_Synch_Only'
   
   framestore.exe:framestore.cs
           gmcs framestore.cs -r:$(KLIB)
   
   framestore:framestore.exe
           $(KIWIC) framestore.exe $(ROOT) -vnl verilogoutput.v


next up previous contents index
Next: Kiwic Internal Operation Up: Kiwi kiwic Compiler Users' Previous: Contents   Contents   Index
David Greaves 2011-03-31