kansas-lava- Kansas Lava is a hardware simulator and VHDL generator.

Safe HaskellNone



KansasLava is designed for generating hardware circuits. This module provides a Rep class that allows us to model, in the shallow embedding of KL, two important features of hardware signals. First, all signals must have some static width, as they will be synthsized to a collection of hardware wires. Second, a value represented by a signal may be unknown, in part or in whole.



allOkayRep :: Size w => Matrix w (X Bool) -> Maybe (Matrix w Bool) Source

Check to see if all bits in a bitvector (represented as a Matrix) are valid. Returns Nothing if any of the bits are unknown.

data IntegerWidth Source

Integers are unbounded in size. We use the type IntegerWidth as the associated type representing this size in the instance of Rep for Integers.



log2 :: Integral a => a -> a Source

Calculate the base-2 logrithim of a integral value.

sizedFromRepToIntegral :: forall w. (Rep w, Integral w, Size w) => RepValue -> X w Source

This is a version of fromRepToIntegral that check to see if the result is inside the size bounds.

class Rep w where Source

A 'Rep a' is an a value that we Represent, aka we can push it over a wire. The general idea is that instances of Rep should have a width (for the corresponding bitvector representation) and that Rep instances should be able to represent the "unknown" -- X -- value. For example, Bools can be represented with one bit, and the inclusion of the unknown X value corresponds to three-valued logic.

Minimal complete definition

unX, optX, toRep, fromRep, repType

Associated Types

type W w Source

the width of the represented value, as a type-level number.

data X w Source

X are lifted inputs to this wire.


unX :: X w -> Maybe w Source

check for bad things.

optX :: Maybe w -> X w Source

and, put the good or bad things back.

toRep :: X w -> RepValue Source

convert to binary (rep) format

fromRep :: RepValue -> X w Source

convert from binary (rep) format

repType :: Witness w -> Type Source

Each wire has a known type.

showRep :: X w -> String Source


Rep Bool 
Rep Int 
Rep Integer 
Rep Word8 
Rep Word32 
Rep () 
Rep X0 
Rep Ready 
Rep Ack 
Rep a => Rep (Maybe a) 
Size ix => Rep (Unsigned ix) 
Size ix => Rep (Signed ix) 
(Integral x, Size x) => Rep (X0_ x) 
(Integral x, Size x) => Rep (X1_ x) 
(Size ix, Rep a, Rep ix) => Rep (ix -> a) 
(Rep a, Rep b) => Rep (a, b) 
(Enum ix, Size m, Size ix) => Rep (Sampled m ix) 
(Size ix, Rep a) => Rep (Matrix ix a) 
(Rep a, Rep b) => Rep ((:>) a b) 
(Rep a, Rep b, Rep c) => Rep (a, b, c) 

class (Size (W a), Eq a, Rep a) => BitRep a where Source

Bitrep is list of values, and their bitwise representation. It is used to derive (via Template Haskell) the Rep for user Haskell datatypes.


bitRep :: [(a, BitPat (W a))] Source

allReps :: Rep w => Witness w -> [RepValue] Source

Given a witness of a representable type, generate all (2^n) possible values of that type.

repWidth :: Rep w => Witness w -> Int Source

Figure out the width in bits of a type.

unknownRepValue :: Rep w => Witness w -> RepValue Source

unknownRepValue returns a RepValue that is completely filled with X.

pureX :: Rep w => w -> X w Source

pureX lifts a value to a (known) representable value.

unknownX :: forall w. Rep w => X w Source

unknownX is an unknown value of every representable type.

liftX :: (Rep a, Rep b) => (a -> b) -> X a -> X b Source

liftX converts a function over values to a function over possibly unknown values.

showRepDefault :: forall w. (Show w, Rep w) => X w -> String Source

showRepDefault will print a Representable value, with "?" for unknown. This is not wired into the class because of the extra Show requirement.

toRepFromIntegral :: forall v. (Rep v, Integral v) => X v -> RepValue Source

Convert an integral value to a RepValue -- its bitvector representation.

fromRepToIntegral :: forall v. (Rep v, Integral v) => RepValue -> X v Source

Convert a RepValue representing an integral value to a representable value of that integral type.

fromRepToInteger :: RepValue -> Integer Source

fromRepToInteger always a positve number, unknowns defin

cmpRep :: Rep a => X a -> X a -> Bool Source

Compare a golden value with a generated value.

bitRepEnum :: (Rep a, Enum a, Bounded a, Size (W a)) => [(a, BitPat (W a))] Source

Helper for generating the bit pattern mappings.

bitRepToRep :: forall w. (BitRep w, Ord w) => X w -> RepValue Source

bitRepToRep' :: forall w. (BitRep w, Ord w) => Map w RepValue -> X w -> RepValue Source

bitRepFromRep :: forall w. (Ord w, BitRep w) => RepValue -> X w Source

bitRepFromRep' :: forall w. (Ord w, BitRep w) => Map RepValue w -> RepValue -> X w Source

bitRepMap :: forall w. (BitRep w, Ord w) => Map RepValue w Source