What4.Protocol.VerilogWriter.AST

Documentation

type Identifier = String

data Binop (inTp :: BaseType) (outTp :: BaseType) where

A type for Verilog binary operators that enforces well-typedness, including bitvector size constraints.

Constructors

And :: Binop BaseBoolType BaseBoolType

Or :: Binop BaseBoolType BaseBoolType

Xor :: Binop BaseBoolType BaseBoolType

Eq :: Binop tp BaseBoolType

Ne :: Binop tp BaseBoolType

Lt :: Binop (BaseBVType w) BaseBoolType

Le :: Binop (BaseBVType w) BaseBoolType

BVAnd :: Binop (BaseBVType w) (BaseBVType w)

BVOr :: Binop (BaseBVType w) (BaseBVType w)

BVXor :: Binop (BaseBVType w) (BaseBVType w)

BVAdd :: Binop (BaseBVType w) (BaseBVType w)

BVSub :: Binop (BaseBVType w) (BaseBVType w)

BVMul :: Binop (BaseBVType w) (BaseBVType w)

BVDiv :: Binop (BaseBVType w) (BaseBVType w)

BVRem :: Binop (BaseBVType w) (BaseBVType w)

BVPow :: Binop (BaseBVType w) (BaseBVType w)

BVShiftL :: Binop (BaseBVType w) (BaseBVType w)

BVShiftR :: Binop (BaseBVType w) (BaseBVType w)

BVShiftRA :: Binop (BaseBVType w) (BaseBVType w)

binopType :: Binop inTp outTp -> BaseTypeRepr inTp -> BaseTypeRepr outTp

data Unop (tp :: BaseType) where

A type for Verilog unary operators that enforces well-typedness.

Constructors

Not :: Unop BaseBoolType

BVNot :: Unop (BaseBVType w)

data IExp (tp :: BaseType) where

A type for Verilog expression names that enforces well-typedness. This type exists essentially to pair a name and type to avoid needing to repeat them and ensure that all uses of the name are well-typed.

Constructors

Ident :: BaseTypeRepr tp -> Identifier -> IExp tp

iexpType :: IExp tp -> BaseTypeRepr tp

data LHS

Constructors

LHS Identifier

LHSBit Identifier Integer

data Exp (tp :: BaseType) where

A type for Verilog expressions that enforces well-typedness, including bitvector size constraints.

Constructors

IExp :: IExp tp -> Exp tp

Binop :: Binop inTp outTp -> IExp inTp -> IExp inTp -> Exp outTp

Unop :: Unop tp -> IExp tp -> Exp tp

BVRotateL :: NatRepr w -> IExp tp -> BV w -> Exp tp

BVRotateR :: NatRepr w -> IExp tp -> BV w -> Exp tp

Mux :: IExp BaseBoolType -> IExp tp -> IExp tp -> Exp tp

Bit :: IExp (BaseBVType w) -> Integer -> Exp BaseBoolType

BitSelect :: (1 <= len, (start + len) <= w) => IExp (BaseBVType w) -> NatRepr start -> NatRepr len -> Exp (BaseBVType len)

Concat :: 1 <= w => NatRepr w -> [Some IExp] -> Exp (BaseBVType w)

BVLit :: 1 <= w => NatRepr w -> BV w -> Exp (BaseBVType w)

BoolLit :: Bool -> Exp BaseBoolType

expType :: Exp tp -> BaseTypeRepr tp

mkLet :: Exp tp -> VerilogM sym n (IExp tp)

Create a let binding, associating a name with an expression. In Verilog, this is a new "wire".

signed :: IExp tp -> VerilogM sym n (IExp tp)

Indicate than an expression name is signed. This causes arithmetic operations involving this name to be interpreted as signed operations.

binop :: Binop inTp outTp -> IExp inTp -> IExp inTp -> VerilogM sym n (IExp outTp)

Apply a binary operation to two expressions and bind the result to a new, returned name.

scalMult :: 1 <= w => NatRepr w -> Binop (BaseBVType w) (BaseBVType w) -> BV w -> IExp (BaseBVType w) -> VerilogM sym n (IExp (BaseBVType w))

A special binary operation for scalar multiplication. This avoids the need to call litBV at every call site.

data BVConst

A wrapper around the BV type allowing it to be put into a map or set. We use this to make sure we generate only one instance of each distinct constant.

Constructors

BVConst (Pair NatRepr BV)

Instances

Eq BVConst

Defined in What4.Protocol.VerilogWriter.AST

Methods

(==) :: BVConst -> BVConst -> Bool

(/=) :: BVConst -> BVConst -> Bool

Ord BVConst

Defined in What4.Protocol.VerilogWriter.AST

Methods

compare :: BVConst -> BVConst -> Ordering

(<) :: BVConst -> BVConst -> Bool

(<=) :: BVConst -> BVConst -> Bool

(>) :: BVConst -> BVConst -> Bool

(>=) :: BVConst -> BVConst -> Bool

max :: BVConst -> BVConst -> BVConst

min :: BVConst -> BVConst -> BVConst

litBV :: 1 <= w => NatRepr w -> BV w -> VerilogM sym n (IExp (BaseBVType w))

Return the (possibly-cached) name for a literal bitvector value.

litBool :: Bool -> VerilogM sym n (IExp BaseBoolType)

Return the (possibly-cached) name for a literal Boolean value.

unop :: Unop tp -> IExp tp -> VerilogM sym n (IExp tp)

Apply a unary operation to an expression and bind the result to a new, returned name.

mux :: IExp BaseBoolType -> IExp tp -> IExp tp -> VerilogM sym n (IExp tp)

Create a conditional, with the given condition, true, and false branches, and bind the result to a new, returned name.

bit :: IExp (BaseBVType w) -> Integer -> VerilogM sym n (IExp BaseBoolType)

Extract a single bit from a bit vector and bind the result to a new, returned name.

bitSelect :: (1 <= len, (idx + len) <= w) => IExp (BaseBVType w) -> NatRepr idx -> NatRepr len -> VerilogM sym n (IExp (BaseBVType len))

Extract a range of bits from a bit vector and bind the result to a new, returned name. The two NatRepr values are the starting index and the number of bits to extract, respectively.

concat2 :: (w ~ (w1 + w2), 1 <= w) => NatRepr w -> IExp (BaseBVType w1) -> IExp (BaseBVType w2) -> VerilogM sym n (IExp (BaseBVType w))

Concatenate two bit vectors and bind the result to a new, returned name.

data Item where

A data type for items that may show up in a Verilog module.

Constructors

Input :: BaseTypeRepr tp -> Identifier -> Item

Output :: BaseTypeRepr tp -> Identifier -> Item

Wire :: BaseTypeRepr tp -> Identifier -> Item

Assign :: LHS -> Exp tp -> Item

data ModuleState sym n

Necessary monadic operations

Constructors

ModuleState

Fields

• vsInputs :: [(Some BaseTypeRepr, Identifier)]

  All module inputs, in reverse order.

• vsOutputs :: [(Some BaseTypeRepr, Bool, Identifier, Some Exp)]

  All module outputs, in reverse order. Includes the type, signedness, name, and initializer of each.

• vsWires :: [(Some BaseTypeRepr, Bool, Identifier, Some Exp)]

  All internal wires, in reverse order. Includes the type, signedness, name, and initializer of each.

• vsFreshIdent :: Int

  A counter for generating fresh names.

• vsExpCache :: IdxCache n IExp

  An expression cache to preserve sharing present in the What4 representation.

• vsBVCache :: Map BVConst Identifier

  A cache of bit vector constants, to avoid duplicating constant declarations.

• vsBoolCache :: Map Bool Identifier

  A cache of Boolean constants, to avoid duplicating constant declarations.

• vsSym :: sym

  The What4 symbolic backend to use with vsBVCache.

Instances

MonadState (ModuleState sym n) (VerilogM sym n)

Defined in What4.Protocol.VerilogWriter.AST

Methods

get :: VerilogM sym n (ModuleState sym n)

put :: ModuleState sym n -> VerilogM sym n ()

state :: (ModuleState sym n -> (a, ModuleState sym n)) -> VerilogM sym n a

newtype VerilogM sym n a

Constructors

VerilogM (StateT (ModuleState sym n) (ExceptT String IO) a)

Instances

MonadError String (VerilogM sym n)

Defined in What4.Protocol.VerilogWriter.AST

Methods

throwError :: String -> VerilogM sym n a

catchError :: VerilogM sym n a -> (String -> VerilogM sym n a) -> VerilogM sym n a

Monad (VerilogM sym n)

Defined in What4.Protocol.VerilogWriter.AST

Methods

(>>=) :: VerilogM sym n a -> (a -> VerilogM sym n b) -> VerilogM sym n b

(>>) :: VerilogM sym n a -> VerilogM sym n b -> VerilogM sym n b

return :: a -> VerilogM sym n a

Functor (VerilogM sym n)

Defined in What4.Protocol.VerilogWriter.AST

Methods

fmap :: (a -> b) -> VerilogM sym n a -> VerilogM sym n b

(<$) :: a -> VerilogM sym n b -> VerilogM sym n a

Applicative (VerilogM sym n)

Defined in What4.Protocol.VerilogWriter.AST

Methods

pure :: a -> VerilogM sym n a

(<*>) :: VerilogM sym n (a -> b) -> VerilogM sym n a -> VerilogM sym n b

liftA2 :: (a -> b -> c) -> VerilogM sym n a -> VerilogM sym n b -> VerilogM sym n c

(*>) :: VerilogM sym n a -> VerilogM sym n b -> VerilogM sym n b

(<*) :: VerilogM sym n a -> VerilogM sym n b -> VerilogM sym n a

MonadIO (VerilogM sym n)

Defined in What4.Protocol.VerilogWriter.AST

Methods

liftIO :: IO a -> VerilogM sym n a

MonadState (ModuleState sym n) (VerilogM sym n)

Defined in What4.Protocol.VerilogWriter.AST

Methods

get :: VerilogM sym n (ModuleState sym n)

put :: ModuleState sym n -> VerilogM sym n ()

state :: (ModuleState sym n -> (a, ModuleState sym n)) -> VerilogM sym n a

newtype Module sym n

Constructors

Module (ModuleState sym n)

mkModule :: sym -> VerilogM sym n (IExp tp) -> ExceptT String IO (Module sym n)

Create a Verilog module in the context of a given What4 symbolic backend and a monadic computation that returns an expression name that corresponds to the module's output.

initModuleState :: sym -> IO (ModuleState sym n)

runVerilogM :: VerilogM sym n a -> ModuleState sym n -> ExceptT String IO (a, ModuleState sym n)

execVerilogM :: sym -> VerilogM sym n a -> ExceptT String IO (ModuleState sym n)

addFreshInput :: BaseTypeRepr tp -> Identifier -> VerilogM sym n Identifier

Returns and records a fresh input with the given type and with a name constructed from the given base.

addOutput :: BaseTypeRepr tp -> Identifier -> Exp tp -> VerilogM sym n ()

Add an output to the current Verilog module state, given a type, a name, and an initializer expression.

addWire :: BaseTypeRepr tp -> Bool -> Identifier -> Exp tp -> VerilogM sym n ()

Add a new wire to the current Verilog module state, given a type, a signedness flag, a name, and an initializer expression.

freshIdentifier :: String -> VerilogM sym n Identifier

Create a fresh identifier by concatenating the given base with the current fresh identifier counter.

addFreshWire :: BaseTypeRepr tp -> Bool -> String -> Exp tp -> VerilogM sym n Identifier

Add a new wire to the current Verilog module state, given a type, a signedness flag, the prefix of a name, and an initializer expression. The name prefix will be freshened by appending current value of the fresh variable counter.