Getting Started with ForSyDe

Ingo Sander
Royal Institute of Technology
Stockholm, Sweden
ingo@kth.se

Introduction

ForSyDe (Formal System Design) has been developed as system design methodology for heterogeneous embedded systems. The initial idea of ForSyDe has been to start with an abstract and formal specification model, that is then refined using well-defined design transformations into a low-level implementation model, and finally mapped into an implementation in hardware or software . Initially ForSyDe only used the synchronous model of computation (MoC), but has later been extended to cover additional models of computation, which can be integrated into one executable heterogeneous model of computation. For the synchronous model of computation there exists a synthesis back-end, which translates an executable synchronous ForSyDe model into the corresponding VHDL-code that can then further be synthesized using a commercial logic synthesis tool.

The tutorial focuses mainly on the modeling concepts of ForSyDe. We will explain the concepts using the synchronous model of computation, but the main concepts apply to all other supported ForSyDe models of computation as well. The tutorial has been written in such a way that knowledge of the functional programming language Haskell should not be required. However, in order to design systems in ForSyDe good knowledge of the main Haskell concepts is needed. For more information on Haskell consult the  Haskell web page, where you find a lot of information and links to books and tutorials. For more information on ForSyDe consult the ForSyDe page.

Installing ForSyDe

In order to set up a working ForSyDe modeling environment, we will need to:

  1. install a Haskell compiler,
  2. install the minimum required libraries,
  3. install ForSyDe.

We use the  Glasgow Haskell Compiler (GHC) to compile ForSyDe models. Installing Haskell libraries (including ForSyDe) can be performed manually according to their dependency order, or simply using the automated tool  cabal-install. We will describe the second way in this tutorial. It is recommended to try ForSyDe in a Unix-based environment (Linux or Mac OS). However, it should be possible to install it using Cygwin in windows.

Installing GHC

Download the GHC package binaries for your platform from  http://www.haskell.org/ghc/. The installation process should be straightforward for Windows and Mac OS. On Linux, running the the following sequence of commands with proper privileges in the extracted package folder accomplishes the job:

myprompt> ./configure
...
myprompt> make install

If you have already installed an older version, be careful about conflicts in the path. Note that if you use the GHC binary packages provided by your Linux distributor, you should check if its version is compatible with ForSyDe. The current version of ForSyDe (3.1.1) is tested to work with GHC version 6.12.3, 7.0.4, but also version 7.2.2 should work. Newer versions of GHC (>= 7.4.1) will not work due to changes in Template Haskell. We recommend to use GHC 7.0.4, since it works fine with the newest versions of cabal-install.

The cabal-install Tool

Download cabal-install from  here and install it using the instructions on the web page. On windows system you just need to put the cabal.exe file somewhere in your path. On Unix-based systems, the bootstrap.sh automates the installation process.

Update the package database after installation by running the following command in your terminal (command prompt):

myprompt> cabal update

Installing the ForSyDe package

Use the installed Cabal-Install tool to install the ForSyDe package and all the required dependencies by issuing the following command in your terminal:

myprompt> cabal install ForSyDe

System Modeling in ForSyDe

In contrast to other approaches based on functional languages, like Lava [2], ForSyDe has been designed to be able to specify systems at a high level of abstraction. However, we start with simple examples of the hardware world in order to introduce the main ForSyDe concepts.

If you have installed ForSyDe, start the GHC interpreter ghci and add the module ForSyDe.Shallow:

myprompt> ghci GHCi, version 6.12.3: http://www.haskell.org/ghc/ :? for help
Loading package ghc-prim ... linking ... done.
Loading package integer-gmp ... linking ... done.
Loading package base ... linking ... done.
Loading package ffi-1.0 ... linking ... done.
Prelude> :m +ForSyDe.Shallow
Prelude ForSyDe.Shallow>

Signals

Systems are modeled in ForSyDe by concurrent processes that interact via signals. Signals are similar to lists and can be created using the function signal that converts a list to a signal.

Prelude ForSyDe.Shallow> let s1 = signal [1,2,3]
Prelude ForSyDe.Shallow> let s2 = signal [2,3,4]

Signals are represented with curly brackets.

Prelude ForSyDe.Shallow> s1 {1,2,3}
Prelude ForSyDe.Shallow> s2 {2,3,4}

Combinational Processes

Processes are functions that take input signals and produce output signals. An adder can be modeled as a process in ForSyDe using the following code.

Prelude ForSyDe.Shallow> let adder in1 in2 = zipWithSY (+) in1 in2

Here adder is a process that takes two input signals in1 and in2 and produces an output signal. We can simulate the adder by applying the signals in1 and in2 to the process adder.

Prelude ForSyDe.Shallow> adder s1 s2
{3,5,7}

If we look closer to the definition of the adder, the adder is constructed by a process constructor zipWithSY and a function (+). The concept of process constructor is central in ForSyDe. All processes in ForSyDe are created using process constructors.

The process constructor zipWithSY belongs to the synchronous model of computation as indicated by the suffix SY. It defines the model of computation and the interface of the process. Process constructors are functions that take functions as arguments and produce another function as output. Such functions are called higher-order-functions in the functional programming community. Here, the process constructor zipWithSY takes a function (+) as argument, and produces a process adder as output. The concept of process constructor separates communication, provided by the process constructor, from computation, provided by the function. The names of the process constructors in ForSyDe originate from Haskell and many other functional languages, where higher-order-functions like map and zipWith operate on lists.

The concept of process constructor is very general. We can use zipWithSY to create other synchronous combinational processes, which takes two input signals and one output signal. Here follows another example.

Prelude ForSyDe.Shallow> let and2 = zipWithSY (&&)

Please observe that we did not provide the input signals when we declare the process and2. In fact we could have declared the adder in the same way without providing the input signals.

Prelude ForSyDe.Shallow> let adder' = zipWithSY (+)

We can simulate the new process and2 with input signals of the required type.

Prelude ForSyDe.Shallow> let s3 = signal [True, False, True]
Prelude ForSyDe.Shallow> let s4 = signal [False, True, True]
Prelude ForSyDe.Shallow> and2 s3 s4 {False,False,True}

As you may have observed, the process adder operates on signals of numerical data types, while the process and2 operates on signals of Boolean. This could give the impression that Haskell has a weak or dynamic type system. However, this is not true. Haskell has a static and strong type system, which infers the type of the functions. We can ask for the type of a function using the :t command in ghci.

Prelude ForSyDe.Shallow> :t adder
adder :: (Num a) => Signal a -> Signal a -> Signal a
Prelude ForSyDe.Shallow> :t and2
and2 :: Signal Bool -> Signal Bool -> Signal Bool

We can read the information provided by ghci as follows. The process adder takes a signal of data type a as first argument, a signal of data type a as second argument, and produces a signal of data type a as result. A further requirement is that the data type a needs to belong to the class of numerical values Num. Thus the process adder can also be applied on signals of real numbers.

Prelude ForSyDe.Shallow> let s5 = signal [1.0, 2.0, 3.0]
Prelude ForSyDe.Shallow> let s6 = signal [2.0, 3.0, 4.0]
Prelude ForSyDe.Shallow> adder s5 s6
{3.0,5.0,7.0}

However, Haskell’s type system will complain, if adder is applied to one signal of integers and another signal of real numbers, since these are two different data types.

Prelude ForSyDe.Shallow> adder s1 s5
<interactive>:1:9:
    Couldn't match expected type `Integer'
              against inferred type `Double'
      Expected type: Signal Integer
      Inferred type: Signal Double
    In the second argument of `adder', namely `s7'
    In the expression: adder s1 s7

We can now take a look on the type declaration of zipWithSY.

Prelude ForSyDe.Shallow> :t zipWithSY
zipWithSY :: (a -> b -> c) -> Signal a -> Signal b -> Signal c

The process constructor zipWithSY takes a function as first argument. This function has two arguments, the first one of a data type a and the second one of a data type b. It produces a result of a data type c. The second argument of zipWithSY is a signal of data type a, and the third argument is a signal of data type b. zipWithSY produces as result a signal of data type c. Observe that the data types a, b, and c may be different, but do not have to be, as in the case of adder and and2.

Since process constructors can take any function that complies to the type declaration, there is no need for a large set of process constructors. For the synchronous model of computation, the following set of process constructors is defined.

mapSY :: (a -> b) -> Signal a -> Signal b
zipWithSY :: (a -> b -> c) -> Signal a -> Signal b -> Signal c
zipWith3SY :: (a -> b -> c -> d) -> Signal a -> Signal b -> Signal c -> Signal d
zipWith4SY :: (a -> b -> c -> d -> e) -> Signal a -> Signal b -> Signal c -> Signal d -> Signal e

So far we have in an interactive way provided the input for ghci, but the natural way is to specify the models using files. The file GettingStarted.hs provides the code for the adder and some input signals. Observe that you

  • should have a module name that is identical to the file name
  • need to import the module ForSyDe.Shallow
  • shall not have the let statement before function and signal declaration.
module GettingStarted where

import ForSyDe.Shallow

adder in1 in2 = zipWithSY (+) in1 in2

s1 = signal [1,2,3]
s2 = signal [2,3,4]

You can now load the file into ghci using the command ’:l’.

Prelude ForSyDe.Shallow> :l GettingStarted
[1 of 1] Compiling
GettingStarted ( GettingStarted.hs, interpreted )
Ok, modules loaded:
GettingStarted.
*GettingStarted ForSyDe.Shallow> adder s1 s2
{3,5,7}

You can reload your program with the command ’:r’. For other commands use ’:h’, which displays the help menu.

Sequential Processes

ForSyDe also provides process constructors for sequential processes. The basic process constructor is delaySY, which delays an input signal one event cycle.

*GettingStarted ForSyDe.Shallow> s1
{1,2,3}
*GettingStarted ForSyDe.Shallow> delaySY 0 s1
{0,1,2,3}

In the current implementation of ForSyDe we have chosen that delaySY outputs one more event than the corresponding input signal, although this could be regarded as non-causal (more output events are produced than input events are consumed). However, the additional output event can be predicted, and gives also a clear advantage when dealing with feedback loops, since no extra delay needs to be inserted.

There exists a number of process constructors for finite state machines. scanldSY models a finite state machine without output decoder. It takes a function to calculate the next state as first argument, a value for the initial state as second argument, and creates a process with one input and one output signal.

The following program implements a counter that counts in both directions between 0 and 4.

data Direction = UP
               | HOLD 
               | DOWN deriving (Show)

counter dir = scanldSY count 0 dir

count state HOLD = state
count 4     UP   = 0
count state UP   = state + 1
count 0     DOWN = 4
count state DOWN = state - 1

Direction is an enumerated data type with the values UP and DOWN. The process counter is modeled with the process constructor scanldSY. It takes a function count and an initial state value 0 as arguments. The function count uses pattern matching. The first row of count reads as follows. If the direction has the value HOLD, the state will not change. The second row matches, if the state is 4 and the direction is UP. In this case the next state will be 0. The third row matches all other patterns for state, if the direction is UP. In this case, the state is incremented by one. The fourth and fifth row give the corresponding functionality for the direction DOWN.

*GettingStarted> counter (signal [UP,UP,UP,HOLD,UP,UP,DOWN,DOWN])
{0,1,2,3,3,4,0,4,3}

More complex finite state machines can be designed using the process constructors mooreSY and mealySY for finite state machines with an output decoder. In a Moore FSM, the output signal only depends on the state, while in a Mealy FSM, the state also depends on the current input.

In the following the types of the main sequential process constructors for one and two input values are given.

delaySY :: a -> Signal a -> Signal a
scanldSY :: (a -> b -> a) -> a -> Signal b -> Signal a
mooreSY :: (a -> b -> a) -> (a -> c) -> a -> Signal b -> Signal c
mealySY :: (a -> b -> a) -> (a -> b -> c) -> a -> Signal b -> Signal c
scanld2SY :: (a -> b -> c -> a) -> a -> Signal b -> Signal c -> Signal a
moore2SY :: (a -> b -> c -> a) -> (a -> d) -> a -> Signal b -> Signal c -> Signal d
mealy2SY :: (a -> b -> c -> a) -> (a -> b -> c -> d) -> a -> Signal b -> Signal c -> Signal d

Process Networks

In the following we model a binary counter as a Mealy FSM and use it to connect several binary counters to an n-bit-counter that counts in both directions from 0 to 2n.

The binary counter is modeled using the process constructor mealySY, a function for the next state decoder binCount, another function for the output decoder carry, and an initial state value 0. The last row in the carry function uses ’_’, which expresses a don’t-care pattern.

binCounter = mealySY binCount carry 0

binCount state HOLD = state
binCount 0     UP   = 1
binCount 1     UP   = 0
binCount 0     DOWN = 1
binCount 1     DOWN = 0

carry 1 UP   = UP
carry 0 DOWN = DOWN
carry _ _    = HOLD

There are many ways to create a process network of several processes. The most general is to construct a process network as a net-list, where the net-list is specified as a set of equations using a where-clause. So a three-bit counter can be modeled as follows, where s1 and s2 are internal signals.

counter3Bit dir = out
   where out = binCounter s2
         s2  = binCounter s1
         s1  = binCounter dir

For simulation it is often useful to define signals of infinite length. Since Haskell is a language that uses lazy evaluation, an infinite signal can be defined recursively. The signal ups is an infinite signal, where all events have the value UP.

ups = UP :- ups

Since Haskell is a lazy language, only the part of the signal that is needed will be executed. The ForSyDe function takeS will return the first n values of the signal. So, we can for instance execute the 3-bit counter for 10 cycles.

*GettingStarted> takeS 10 (counter3Bit ups)
{HOLD,HOLD,HOLD,HOLD,HOLD,HOLD,HOLD,UP,HOLD,HOLD}

However, ForSyDe offers also function composition, which is a basic operation in Haskell to create a new function be connecting two functions. The function composition operator ∘ is written in Haskell as a dot ’.’. It is defined as follows.

(.) :: (b -> c) -> (a -> b) -> a -> c
(f . g) x = f(g (x))

Using this operator we can create a two-bit counter by composition of two binary counters.

counter2Bit = binCounter . binCounter

Another very useful operator is the function application operator ’$’. It is defined as

f $ x = f x

At first sight, it looks pretty useless. However, it makes the program more readable, since usual function application is left-associative, while function application with ’$’ is right-associative.

The following two process networks network1 and network2 are equivalent:

network1 in1 in2 = mapSY even (zipWithSY (+) in1 in2)
network2 in1 in2 = mapSY even $ zipWithSY (+) in1 in2

Using more advanced features of Haskell, we can now express a general n-bit counter.

counterNBit n = foldl (.) id $ replicate n binCounter

The function replicate creates a list of n binCounter processes. Remember that functions - a ForSyDe process is a function - are first-class data types in Haskell and thus they can be part of a list. Then the higher-order-function foldl composes our n binary counters together with an identity function id into an n-bit counter.

*GettingStarted> counterNBit 2 $ takeS 12 ups
{HOLD,HOLD,HOLD,UP,HOLD,HOLD,HOLD,UP,HOLD,HOLD,HOLD,UP}
*GettingStarted> counterNBit 3 $ takeS 12 ups
{HOLD,HOLD,HOLD,HOLD,HOLD,HOLD,HOLD,UP,HOLD,HOLD,HOLD,HOLD}

Finally, since Haskell allows partial function application, we can create fixed-size counters using the generic n-bit counters.

counter1Bit' = counterNBit 1
counter2Bit' = counterNBit 2
counter3Bit' = counterNBit 3

The counters execute as expected.

*GettingStarted> counter1Bit' $ takeS 12 ups
{HOLD,UP,HOLD,UP,HOLD,UP,HOLD,UP,HOLD,UP,HOLD,UP}
*GettingStarted> counter2Bit' $ takeS 12 ups
{HOLD,HOLD,HOLD,UP,HOLD,HOLD,HOLD,UP,HOLD,HOLD,HOLD,UP}
*GettingStarted> counter3Bit' $ takeS 12 ups
{HOLD,HOLD,HOLD,HOLD,HOLD,HOLD,HOLD,UP,HOLD,HOLD,HOLD,HOLD}

Hardware Design in ForSyDe

The previous section illustrated how to model systems in ForSyDe. Naturally, we would like to generate hardware or software from these models, but the so called shallow-embedded implementation of ForSyDe discussed in the previous section does not give access to the internal structure of the ForSyDe model. Thus the only way to develop a synthesis tool would be to write a traditional compiler, which requires an enormous engineering effort.

Instead we have chosen to develop a second implementation, called deep-embedded ForSyDe [], which gives access to the internal structure of the ForSyDe model. Based on this structural information ForSyDe’s embedded compiler can perform different analysis and transformations, like the simulation of the system model or the synthesis of the model to a target language like VHDL.

In order to have access to the internal data structure, the designer has to write the code in a slightly different way, which requires more effort. However, the deep-embedded implementation follows strictly the ideas of ForSyDe as presented in the previous section. Also deep-embedded synthesizable models can be co-simulated with shallow-embedded models.

Seven Segment Decoder

In order to introduce the deep-embedded version of ForSyDe we start with the design of a seven segment decoder. To see the difference between the shallow-embedded and the deep-embedded version of ForSyDe, we will first present the shallow-embedded version of the seven segment decoder in the following listing:

module SevenSegmentDecoder (sevenSegDec) where
import ForSyDe.Shallow
import ForSyDe.Bit
import Data.Param.FSVec
import Data.Int
import Data.TypeLevel.Num.Reps
import Data.TypeLevel.Num.Aliases

-- L turns LED on
decode :: Int8 -> FSVec D7 Bit
decode 0 = H +> L +> L +> L +> L +> L +> L +> empty
decode 1 = H +> H +> H +> H +> L +> L +> H +> empty
decode 2 = L +> H +> L +> L +> H +> L +> L +> empty
decode 3 = L +> H +> H +> L +> L +> L +> L +> empty
decode 4 = L +> L +> H +> H +> L +> L +> H +> empty
decode 5 = L +> L +> H +> L +> L +> H +> L +> empty
decode 6 = L +> L +> L +> L +> L +> H +> L +> empty
decode 7 = H +> H +> H +> H +> L +> L +> L +> empty
decode 8 = L +> L +> L +> L +> L +> L +> L +> empty
decode 9 = L +> L +> H +> L +> L +> L +> L +> empty
decode _ = H +> H +> H +> H +> H +> H +> H +> empty

sevenSegDec :: Signal Int8 -> Signal (FSVec D7 Bit)
sevenSegDec = mapSY decode

We want to point out that this shallow-embedded model is already prepared for hardware synthesis. It uses a data type Bit with the values L and H, which can be synthesized in the deep-embedded version of ForSyDe. Even more important is the use of the fixed-sized vector data type FSVec instead of a list or vector data type. For hardware synthesis it is of essential importance to give the exact size of a vector, which is possible with FSVec. Here D7 gives the size of the fixed-sized vector, which in this case is a vector of seven bits.

The deep-embedded ForSyDe implementation uses  Template Haskell, which allows to access the internal structure of the model. In order to enable the Template Haskell extension, we prepend the following pragma to our model.

{-# LANGUAGE TemplateHaskell #-}
module SevenSegmentDecoderHW (sevenSegDecSys) where

import ForSyDe
import ForSyDe.Bit
import Data.Param.FSVec
import Data.Int
import Data.TypeLevel.Num.Reps
import Data.TypeLevel.Num.Aliases

Observe that the deep-embedded implementation of ForSyDe is imported using the command import ForSyDe, while the shallow-embedded implementation is imported using `import ForSyDe.Shallow`. The other import commands are used to import the data types Bit, Int8, and the fixed-sized vector data type.

Also in deep-embedded ForSyDe processes are created by means of process constructors taking functions and variables as arguments. However, we define an additional level, which is called system definition and creates a reusable synthesizable component.

In the deep-embedded world the functions that are arguments of the process constructor are called process functions and have a different data type ProcFun. Since we need access to the internal representation of the function Template Haskell is used for the definition of the function.

decodeFun :: ProcFun (Int8 -> FSVec D7 Bit)
decodeFun
   = $(newProcFun
         [d|decode :: Int8 -> FSVec D7 Bit
            decode x
              = case x of
                  0 -> H +> L +> L +> L +> L +> L +> L +> empty
                  1 -> H +> H +> H +> H +> L +> L +> H +> empty
                  2 -> L +> H +> L +> L +> H +> L +> L +> empty
                  3 -> L +> H +> H +> L +> L +> L +> L +> empty
                  4 -> L +> L +> H +> H +> L +> L +> H +> empty
                  5 -> L +> L +> H +> L +> L +> H +> L +> empty
                  6 -> L +> L +> L +> L +> L +> H +> L +> empty
                  7 -> H +> H +> H +> H +> L +> L +> L +> empty
                  8 -> L +> L +> L +> L +> L +> L +> L +> empty
                  9 -> L +> L +> H +> L +> L +> L +> L +> empty
                  _ -> H +> H +> H +> H +> H +> H +> H +> empty
                    |])

The main difference to the shallow-embedded version is the special syntax. First the function has the data type `ProcFun (Int8 -> FSVec D7 Bit) instead of Int8 -> FSVec D7 Bit`. Then we declare the computation function inside a code pattern that allows to have access to the internal structure of the model, the abstract syntax tree (AST). The code pattern is $(newProcFun [d| ... |]) Inside this pattern the function is declared in the same way as before. In contrast to the shallow-embedded version, the type for the function, here decode :: Int8 -> FSVec D7 Bit, needs to be provided.

The next level declares the process using process constructor and process function. In contrast to the shallow-embedded version an additional label needs to be provided to distuinguish different processes.

sevenSegDecProc :: Signal Int8 -> Signal (FSVec D7 Bit)
sevenSegDecProc = mapSY "decode" decodeFun

Finally the system definition is created. The system is defined providing the process, a label, a list of input port names, and a list of output port names.

sevenSegDecSys :: SysDef (Signal Int8 -> Signal (FSVec D7 Bit))
sevenSegDecSys = newSysDef sevenSegDecProc "sevenSegDec" ["in"] ["out"]

The deep-embedded ForSyDe compiler makes use of the knowledge of the internal structure of a system by providing different backends that operate on the internal structure of the system. The first backend is the simulation backend. The seven segment decoder can be simulated using the following command:

*SevenSegmentDecoderHW> simulate sevenSegDecSys [4,0,2]
[<L,L,H,H,L,L,H>,<H,L,L,L,L,L,L>,<L,H,L,L,H,L,L>]

Observe that the deep-embedded compiler uses plain Haskell lists for signals.

More interesting is the second backend that generates VHDL-code for a system.

*SevenSegmentDecoderHW> writeVHDL sevenSegDecSys

This generates the VHDL-code for the seven segment decoder. The VHDL-code is located in the directorysevenSegDec/vhdl. Further we can invoke the Altera Quartus tool with design options using the following command:

compileQuartus_sevenSegDecSys :: IO ()
compileQuartus_sevenSegDecSys = writeVHDLOps vhdlOps sevenSegDecSys
 where vhdlOps = defaultVHDLOps{execQuartus=Just quartusOps}
       quartusOps
          = QuartusOps{action=FullCompilation,
                       -- fMax is not needed for combinational circuits
                       fMax=Just 50, -- in MHz
                       fpgaFamiliyDevice=Just ("CycloneII",
                                                Just "EP2C35F672C6"),
                       -- Possibility for Pin Assignments
                       pinAssigs=[("in[0]", "PIN_N25"), -- SW0
                                  ("in[1]", "PIN_N26"), -- SW1
                                  ("in[2]", "PIN_P25"), -- SW2
                                  ("in[3]", "PIN_AE14"), -- SW3
                                  ("in[4]", "PIN_AF14"), -- SW4
                                  ("in[5]", "PIN_AD13"), -- SW5
                                  ("in[6]", "PIN_AC13"), -- SW6
                                  ("in[7]", "PIN_C13"), -- SW7
                                  ("out[6]","PIN_AF10"), -- HEX0[0]
                                  ("out[5]","PIN_AB12"), -- HEX0[1]
                                  ("out[4]","PIN_AC12"), -- HEX0[2]
                                  ("out[3]","PIN_AD11"), -- HEX0[3]
                                  ("out[2]","PIN_AE11"), -- HEX0[4]
                                  ("out[1]","PIN_V14"), -- HEX0[5]
                                  ("out[0]","PIN_V13") -- HEX0[6]
                                 ]
                              }

In case Quartus is installed an implementation of the seven segment decoder sevenSegDec.sof is generated, which is located in the directorysevenSegDec/vhdl. The pin assignments are compatible with Altera’s DE2 board.

Counter

As an example for a sequential circuit we will implement a simple counter, which counts up- or downwards between 0 and 9.

{-# LANGUAGE TemplateHaskell #-}
module CounterHW (Direction, counterSys) where

import ForSyDe
import Data.Int

type Direction = Bit

nextStateFun :: ProcFun (Int8 -> Direction -> Int8)
nextStateFun = $(newProcFun
   [d| nextState state dir = if dir == H then
                                 if state < 9 then
                                    state + 1
                                 else
                                    0
                              else
                                 if state == 0 then
                                    9
                                 else
                                    state - 1
     |])

counterProc :: Signal Direction -> Signal Int8
counterProc = scanldSY "counterProc" nextStateFun 0

counterSys :: SysDef (Signal Direction -> Signal Int8)
counterSys = newSysDef counterProc "Counter" ["direction"] ["number"]

Structured Hardware Design

Finally we will develop use instances of the seven segment decoder and the counter to create a new synthesizable design that counts up- and downwards and shows the actual state on the seven-segment display.

systemProc :: Signal Direction -> Signal (FSVec D7 Bit)
systemProc dir = sevenSeg
   where
      sevenSeg
         = (instantiate "sevenSegDec" sevenSegDecSys) counterOut
      counterOut = (instantiate "counter" counterSys) dir

system :: SysDef (Signal Direction -> Signal (FSVec D7 Bit))
system = newSysDef systemProc "system" ["in"] ["out"]

Here we see that a composite process systemProc is created by describing a ’netlist’ as a set of equations. In this set of equations the systems sevenSegDecSys and counterSys are instantiated. Finally the new system system is created by a system definition using the process systemProc.

The full synthesizable code for the system is given below including parameters for the Quartus tool targeting the DE2 board.

{-# LANGUAGE TemplateHaskell #-}

module CounterSystemHW where

import ForSyDe
import CounterHW
import SevenSegmentDecoderHW
import ForSyDe.Bit
import Data.Param.FSVec
import Data.Int
import Data.TypeLevel.Num.Reps
import Data.TypeLevel.Num.Aliases

systemProc :: Signal Direction -> Signal (FSVec D7 Bit)
systemProc dir = sevenSeg
   where
      sevenSeg
         = (instantiate "sevenSegDec" sevenSegDecSys)
      counterOut counterOut = (instantiate "counter" counterSys) dir

system :: SysDef (Signal Direction -> Signal (FSVec D7 Bit))
system = newSysDef systemProc "system" ["in"] ["out"]

-- Hardware Generation
compileQuartus_CounterSystem :: IO ()
compileQuartus_CounterSystem = writeVHDLOps vhdlOps system
   where
      vhdlOps = defaultVHDLOps{execQuartus=Just quartusOps}
      quartusOps
        = QuartusOps{action=FullCompilation,
                     fMax=Just 50, -- in MHz 
                     fpgaFamiliyDevice=Just ("CycloneII",
                                             Just "EP2C35F672C6"),
                     -- Possibility for Pin Assignments
                     pinAssigs=[("in", "PIN_N25"), -- SW0
                                ("resetn", "PIN_N26"), -- SW1
                                ("clock","PIN_G26"), -- KEY[0]
                                ("out[6]","PIN_AF10"), -- HEX0[0]
                                ("out[5]","PIN_AB12"), -- HEX0[1]
                                ("out[4]","PIN_AC12"), -- HEX0[2]
                                ("out[3]","PIN_AD11"), -- HEX0[3]
                                ("out[2]","PIN_AE11"), -- HEX0[4]
                                ("out[1]","PIN_V14"), -- HEX0[5]
                                ("out[0]","PIN_V13") -- HEX0[6]
                               ]
                     }

References

  1. ^Ingo Sander and Axel Jantsch, System Modeling and Transformational Design Refinement in {ForSyDe}, {IEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems}, 23, 1, January, 2004, 23, article, 17--32,
  2. ^Bjesse, Per and Claessen, Koen and Sheeran, Mary and Singh, Satnam, Lava: hardware design in Haskell, Proceedings of the third ACM SIGPLAN international conference on Functional programming, http://doi.acm.org/10.1145/289423.289440, ICFP '98, ACM, 1998, inproceedings, 1-58113-024-4, 174--184,
    http://doi.acm.org/10.1145/289423.289440

Attachments