Documentation

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

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

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.

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

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

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

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

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

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.

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

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

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

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

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

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.

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

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

Necessary monadic operations

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.

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

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

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

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

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.