Hardware description in Functional Languages and Introduction to Lava

Hardware Description and Verification

Thomas Hallgren

2009-04-27

Where are we?

• Take a look at the schedule
• First half of the course: Industry standard languages and tools
  • VHDL
  • PSL
  • Jasper Gold

Where are we?

Second half of the course: a peek at what comes next...

• Hardware designs are becoming more and more complex
• There is a need to control low-level details even at high levels of design
• Better languages are needed
• Transfer progress in programming languages to Hardware Description Languages

Guests Lectures

• Monday, May 4
  • Wolfgang Kunz (TU Kaiserslautern): SoC verification
• Tuesday, May 12
  • Satnam Singh (Microsoft): current trends, FPGAs in Bluespec
• Thursday, May 14
  • Emil Axelsson, Joel Svensson (Chalmers)

Hardware Description in Functional Language

• Advantages of Functional Languages:
  • Provide a concise notation
  • Powerful abstraction mechanisms to deal with complexity
  • Good support for generic hardware descriptions
  • Equational style supports reasoning and rewrites
• What are people doing?
  • See the HFL workshop

Hardware Description in Functional Languages

• Examples
  • Lava (Chalmers)
  • Lava (Xilinx)
  • Hawk
  • Bluespec
• In this course
  • Lava (Chalmers)

What is Lava?

Lava is a hardware description language embedded in Haskell

• Haskell is a purely functional programming language.
• Like VHDL, Haskell is a strongly typed language.
• A compiler (GHC) and two interactive systems (Hugs, ghci) are available.
• Everything about Haskell: www.haskell.org.

What is Lava?

Lava is essentially a Haskell library from which you can import types and functions for

• describing circuits,
• simulating circuits,
• feeding circuits to other tools, e.g. for formal verification
  • We will use SMV

Lava Documentation

• The Lava Tutorial introduces Lava without requiring previous knowledge of Haskell.
• There is also the guide How to Use the Lava System.
• Instructions for accessing the tools have recently been updated.

A First Example: a Half Adder

Half Adder implementation

Half Adder in VHDL

• entity halfAdder is
    port (a,b  : in  bit;
          sum,carry : out bit);
  end halfAdder;
   
  architecture ha_beh of halfAdder is
  begin 
    sum <= a xor b;
    c_out <= a and b;
  end ha_beh;
  

• Just to have something to compare to

Half Adder in Lava

• halfAdder (a, b) = (sum, carry)
    where
      sum   = xor2 (a, b)
      carry = and2 (a, b)
  

• Note: it's a direct transcription of the circuit diagram!

  

Half Adder Interface

• halfAdder :: (Signal Bool,Signal Bool) -> (Signal Bool,Signal Bool)
  halfAdder (a,b) = (sum,carry)
    where
      ...
  

• The first line is the type signature for halfAdder.
• A circuit is represented as a function from input to output
  • A->B: a function with input of type A and output of type B
  • (A1,A2): a pair. Pairing allows several signals to be grouped together and treated as one signal.
  • Signal A: signals carrying values of type A
  • Bool: boolean values, False or True

Half Adder Interface

• Introducing a shorter name for the type of boolean signals

  • type Bit = Signal Bool
    
    low, high :: Bit

• We can now write

  • halfAdder :: (Bit,Bit) -> (Bit,Bit)
    halfAdder (a,b) = (sum,carry)
      where
        ...
    

Simulating Lava circuits

• Simulating a single cycle
  • simulate circuit input
• Example:
  • simulate halfAdder (low,high)
(high,low)
  • simulate halfAdder (high,high)
(low,high)
• More later

Logical Gates in the Lava library

• From Appendix A (Quick Reference) in the Lava Tutorial:

• id, inv :: Bit -> Bit
   
  and2, nand2, or2, nor2, xor2, equiv, impl :: (Bit,Bit) -> Bit
  <&>,         <|>,       <#>,  <=>,   ==>  :: (Bit,Bit) -> Bit

• a <&> b is the same as and2 (a,b), etc.

Half Adder in Lava, alternate versions

• halfAdder (a, b) = (sum, carry)
    where
      sum   = xor2 (a, b)
      carry = and2 (a, b)
  

• In functional languages, you can substitute equals for equals:

• halfAdder (a, b) = (xor2 (a,b),and2(a,b))
  

• Using the alternative infix operators:

• halfAddder (a,b) = (a <#> b, a <&> b)
  

A Second Example: a Full Adder

Full Adder implementation

Full Adder in VHDL

• entity fullAdder is
    port (a,b,carryIn  : in  bit;
          sum,carryOut : out bit);
  end fullAdder;
   
  architecture fa_beh of fullAdder is
    signal s1,c1,c2 : bit;
  begin  -- fa_beh
    ha1: entity work.halfAdder
      port map (a, b, s1, c1);
    
    ha2: entity work.halfAdder
      port map (carryIn, s1, sum, c2);
    
    xor1: carryOut <= c1 xor c2;
    
  end fa_beh;

• A structural description that refers to the previously defined entity halfAdder.

Full adder in Lava

• fullAdder (carryIn, (a,b)) = (sum, carryOut)
    where
      (s1,  c1) = halfAdder (a, b)
      (sum, c2) = halfAdder (carryIn,s1)
      carryOut  = xor2 (c2, c1)
  

• Again, it should be a direct transcription of the circuit diagram.
• Using previously defined components is just as easy as using basic gates.

  

Full Adder Interface

• fullAdder :: (Bit,(Bit,Bit)) -> (Bit,Bit)
  fullAdder (carryIn, (a,b)) = (sum, carryOut)
    where
      ...
  

• The first line is the type signature of function fullAdder.
• It is inferred automatically if you leave it out.

A third example: a Ripple Carry Adder

• A row of full adders form a ripple carry adder

  

• We will write a generic implemention

Ripple Carry Adder in VHDL

• entity rippleCarryAdder is
    generic (n : natural);
    port (
      carryIn       : in bit;
      a, b          : in bit_vector(n-1 downto 0);
      sum           : out bit_vector(n-1 downto 0);
      carryOut      : out bit);
  
  end rippleCarryAdder;
  
  architecture rca_beh of rippleCarryAdder is
    signal c : bit_vector(0 to n);
  begin
    c(0) <= carryIn;
    
    adders: for i in 0 to n-1 generate
    begin
      bit : entity work.fullAdder
            port map (c(i),a(i),b(i),sum(i),c(i+1));
    end generate;
    
    carryOut <= c(n);
   
  end rca_beh;
  

• A structural description that refers to the previously defined entity fullAdder.

Ripple Carry Adder in Lava

• rippleCarryAdder (carryIn, (as,bs)) = (sum,carryOut)
    where
      (sum,carryOut) = row fullAdder (carryIn,zipp (as,bs))
  

• row is a connection pattern that does exactly what we need here.

  

• zipp takes care of pairing up the bits at corresponding positions in the two input bit vectors as and bs.

Ripple Carry Adder Interface

• rippleCarryAdder :: (Bit,([Bit],[Bit])) -> ([Bit],Bit)
  rippleCarryAdder (carryIn, (as,bs)) = (sum,carryOut)
    where
      (sum,carryOut) = row fullAdder (carryIn,zipp (as,bs))
  

• [A]: lists of values of type A. Examples of lists:
  • [] (empty list)
  • [low,high,low,low] :: [Bit]
  • [(low,high),(low,low)] :: [(Bit,Bit)]
  • domain enumerates all values of a finite type
• List are used both for sequences in time and for parallel signals (busses).
• Length can be arbitrary and is not indicated in the type.

Lists and Connection patterns

• Rearranging input:
  • zipp :: ([a],[b]) -> [(a,b)], where a and b are arbitrary types
  • unzipp :: [(a,b)] -> ([a],[b])
• Replicating circuits:
  • map :: (a->b) -> ([a] -> [b])
  • row :: ((c, a) -> (b, c)) -> (c, [a]) -> ([b], c)

    

• It's easy to define new connection patterns in Lava

Simulating Lava circuits

• Single cycle
  • simulate circuit input
• Simulating a sequence
  • simulateSeq circuit list_of_inputs
• Examples:
  • simulate fullAdder (high,(low,high))
(low,high)
  • simulate rippleCarryAdder (low,([low,high],[high,high]))
([high,low],high)
  • simulateSeq fullAdder domain
[(low,low),(high,low),(high,low),(low,high),(high,low),(low,high),(low,high),(high,high)]

Generating VHDL from Lava circuits

• In the simplest case

  • writeVhdl "fullAdder" fullAdder
    

• Assigning names to the inputs

  • writeVhdlInput "fullAdder" fullAdder (var "carryIn",(var "a",var "b"))
    

• Assigning names also to the outputs

  • writeVhdlInputOutput "fullAdder" fullAdder
                         (var "carryIn",(var "a",var "b"))
                         (var "sum",var "carryOut")
    

• Generic circuits are not supported, so you need to pick a size

  • writeVhdlInputOutput "rippleCarryAdder" rippleCarryAdder
                         (var "carryIn",(varList 8 "a",varList 8 "b"))
                         (varList 8 "sum",var "carryOut")
    

VHDL for combinational circuits

• The VHDL translator assumes all components need a clock signal. There is a newer version of the translator that allows you to omit the clock.
• Put import VhdlNew08 in your source file.
• Add NoClk to the end of the function name
• Example

  • writeVhdlNoClk "fullAdder" fullAdder
    

Formal Verification of Lava circuits

• smv property
• For verifying safety properties, the property can a circuit with
  • a number of inputs of fixed size
  • a single boolean output
• For verifying generic circuits, a size has to be chosen...

FV example

• Our own implementation of exclusive or:

  • xor (a,b) = (a <|> b) <&> inv (a <&> b)
    

• Specifying correctness:

  • prop_xor = prop_Equivalent xor xor2
    

• Exhaustive testing

  • test_xor = simulateSeq prop_xor domain
    

• Formal verification using SMV

  • vrfy_xor = smv prop_xor
    

Equivalence Checking

What does prop_Equivalent do?

Creates a bigger circuit

• includes the two circuits to be checked for equivalence
• feeds the same input to both circuits
• compares the output

Equivalence checking

• Checking a specific circuit:

  • prop_xor (a,b) = ok
     where
       out1 = xor (a,b)
       out2 = xor2 (a,b)
       ok = out1 <==> out2
    

• We can capture this pattern in a more general function:

  • prop_Equivalent circ1 circ2 inp = ok
      where
        out1 = circ1 inp
        out2 = circ2 inp
        ok = out1 <==> out2
    

  • prop_xor = prop_Equivalent xor xor2
    

Conclusion

• The examples from this lecture:
  • LavaIntro.hs
• Next
  • Sequential circuits
  • Connection patterns
  • Multipliers
  • Parallel prefix
  • Wired and Obsidian