Comb_gates (hardcaml_verify.hardcaml_verify.kernel.Hardcaml_verify_kernel.Comb

include Hardcaml.Comb.S with type t = Basic_gates.t Base.list

type t = Basic_gates.t Base.list

val sexp_of_t : t -> Sexplib0.Sexp.t

include Base.Equal.S__local with type t := t

val equal : t Base.Equal.equal

val vdd : t

logic 1

val gnd : t

logic 0

val of_constant : Hardcaml.Constant.t -> t

create signal from a constant

val of_bit_string : string -> t

convert binary string to constant

val of_int_trunc : width:int -> int -> t

Convert integer to constant. Negative values are sign extended up to width. Input values which are larger or smaller than those representable in width bits are truncated.

val of_int32_trunc : width:int -> int32 -> t

val of_int64_trunc : width:int -> int64 -> t

val of_int : width:int -> int -> t

Same as of_int_trunc

deprecated [since 2024-11] use [of_int_trunc]

val of_int32 : width:int -> int32 -> t

deprecated [since 2024-11] use [of_int32_trunc]

val of_int64 : width:int -> int64 -> t

deprecated [since 2024-11] use [of_int64_trunc]

val of_unsigned_int : width:int -> int -> t

Convert non-negative values to constant. Input values which are not representable in width bits will raise.

val of_unsigned_int32 : width:int -> int32 -> t

val of_unsigned_int64 : width:int -> int64 -> t

val of_signed_int : width:int -> int -> t

Convert signed values to constant. Input values which are not representable in width bits will raise.

val of_signed_int32 : width:int -> int32 -> t

val of_signed_int64 : width:int -> int64 -> t

val of_hex : ?signedness:Hardcaml.Signedness.t -> width:int -> string -> t

convert hex string to a constant. If the target width is greater than the hex length and signedness is Signed then the result is sign extended. Otherwise the result is zero padded.

val of_octal : ?signedness:Hardcaml.Signedness.t -> width:int -> string -> t

convert octal string to a constant. If the target width is greater than the octal length and signedness is Signed then the result is sign extended. Otherwise the result is zero padded.

val of_bigint : width:int -> Bigint.t -> t

Convert an arbitrarily wide integer value to a constant.

val of_string : string -> t

convert verilog style or binary string to constant

val of_bit_list : int list -> t

convert IntbitsList to constant

val of_decimal_string : width:int -> string -> t

val of_char : char -> t

convert a char to an 8 bit constant

val of_bool : bool -> t

convert a bool to vdd or gnd

val of_ascii_string_lsb : string -> t

convert a string to a series of 8-bit characters and concatenate them into a signal, with the first character of the string being in the least-significant bits

val of_ascii_string_msb : string -> t

convert a string to a series of 8-bit characters and concatenate them into a signal, with the first character of the string being in the most-significant bits

val random : width:int -> t

create random constant vector of given width

val zero : int -> t

zero w makes a the zero valued constant of width w

val ones : int -> t

ones w makes a constant of all ones of width w

val one : int -> t

one w makes a one valued constant of width w

val empty : t

the empty signal

val is_empty : t -> bool

returns true if the signal is empty

val (--) : loc:lexing_position -> t -> string -> t

names a signal

let a = a -- "a" in ...

signals may have multiple names.

val width : t -> int

returns the width (number of bits) of a signal.

let w = width s in ...

val address_bits_for : int -> int

addess_bits_for num_elements returns the address width required to index num_elements.

It is the same as Int.ceil_log2, except it wll return a minimum value of 1 (since you cannot have 0 width vectors). Raises if num_elements is < 0.

val num_bits_to_represent : int -> int

num_bits_to_represent x returns the number of bits required to represent the number x, which should be >= 0.

val to_constant : t -> Hardcaml.Constant.t

convert the signal to a constant

val concat_msb : t list -> t

concat ts concatenates a list of signals - the msb of the head of the list will become the msb of the result.

let c = concat [ a; b; c ] in ...

concat raises if ts is empty or if any t in ts is empty.

val concat_lsb : t list -> t

Similar to concat_msb except the lsb of the head of the list will become the lsb of the result.

val (@:) : t -> t -> t

concatenate two signals.

let c = a @: b in ...

equivalent to concat [ a; b ]

val is_vdd : t -> bool

deprecated [since 2025-03] use [to_bool]

val is_gnd : t -> bool

deprecated [since 2025-03] use [not to_bool]

val select : t -> high:int -> low:int -> t

select t ~high ~low selects from t bits in the range high...low, inclusive. select raises unless high and low fall within 0 .. width t - 1 and high >= lo.

val bit : t -> pos:int -> t

select a single bit

val msb : t -> t

get most significant bit

val lsbs : t -> t

get least significant bits

val lsb : t -> t

get least significant bit

val msbs : t -> t

get most significant bits

val drop_bottom : t -> width:int -> t

drop_bottom s ~width drop bottom width bits of s

val drop_top : t -> width:int -> t

drop_top s ~width drop top width bits of s

val sel_bottom : t -> width:int -> t

sel_bottom s ~width select bottom width bits of s

val sel_top : t -> width:int -> t

sel_top s ~width select top width bits of s

val (.:[]) : t -> (int * int) -> t

x.:[hi, lo] == select x hi lo

val (.:+[]) : t -> (int * int option) -> t

x.:+[lo, width] == select x (lo + width - 1) lo. If width is None it selects all remaining msbs of the vector ie x.:+[lo,None] == drop_bottom x lo

val (.:-[]) : t -> (int option * int) -> t

x.:-[hi, width] == select x hi (hi - width + 1). If hi is None it defaults to the msb of the vector ie x.:-[None, width] == sel_top x width

val (.:()) : t -> int -> t

x.(i) == bit x i

val insert : into:t -> t -> at_offset:int -> t

insert ~into:t x ~at_offset insert x into t at given offet

val mux : t -> t list -> t

multiplexer.

let m = mux sel inputs in ...

Given l = List.length inputs and w = width sel the following conditions must hold:

l <= Int.pow 2 w, l >= 1

If l < Int.pow 2 w, the last input is repeated.

All inputs provided must have the same width, which will in turn be equal to the width of m.

val mux_strict : t -> t list -> t

Same as mux except requires:

l = Int.pow 2 w

val mux2 : t -> t -> t -> t

mux2 c t f 2 input multiplexer. Selects t if c is high otherwise f.

t and f must have same width and c must be 1 bit.

Equivalent to mux c [f; t]

val mux_init : t -> int -> f:(int -> t) -> t

val cases : default:t -> t -> (t * t) list -> t

cases ~default select [(match0, value0); (match0, value0)...] compares select with matchN and outputs valueN. If nothing matches default is output. This construct maps to a case statement.

The matchN values must be constants.

val (&:) : t -> t -> t

logical and

val (&:.) : t -> int -> t

val (&+.) : t -> int -> t

val (&&:) : t -> t -> t

a <>:. 0 &: b <>:. 0

val (|:) : t -> t -> t

logical or

val (|:.) : t -> int -> t

val (|+.) : t -> int -> t

val (||:) : t -> t -> t

 a <>:. 0 |: b <>:. 0

val (^:) : t -> t -> t

logic xor

val (^:.) : t -> int -> t

val (^+.) : t -> int -> t

val (~:) : t -> t

logical not

val (+:) : t -> t -> t

addition

val (+:.) : t -> int -> t

val (++.) : t -> int -> t

val (-:) : t -> t -> t

subtraction

val (-:.) : t -> int -> t

val (-+.) : t -> int -> t

val negate : t -> t

negation

val (*:) : t -> t -> t

unsigned multiplication

val (*+) : t -> t -> t

signed multiplication

val (==:) : t -> t -> t

equality

val (==:.) : t -> int -> t

val (==+.) : t -> int -> t

val (<>:) : t -> t -> t

inequality

val (<>:.) : t -> int -> t

val (<>+.) : t -> int -> t

val (<:) : t -> t -> t

less than

val (<:.) : t -> int -> t

val lt : t -> t -> t

val (>:) : t -> t -> t

greater than

val (>:.) : t -> int -> t

val (<=:) : t -> t -> t

less than or equal to

val (<=:.) : t -> int -> t

val (>=:) : t -> t -> t

greater than or equal to

val (>=:.) : t -> int -> t

val (<+) : t -> t -> t

signed less than

val (<+.) : t -> int -> t

val (>+) : t -> t -> t

signed greater than

val (>+.) : t -> int -> t

val (<=+) : t -> t -> t

signed less than or equal to

val (<=+.) : t -> int -> t

val (>=+) : t -> t -> t

signed greated than or equal to

val (>=+.) : t -> int -> t

val (-->:) : t -> t -> t

Propositional logic implication operator

val to_string : t -> string

create string from signal

val to_int_trunc : t -> int

to_int t treats t as unsigned and resizes it to fit exactly within an OCaml Int.t.

If width t > Int.num_bits then the upper bits are truncated.
If width t >= Int.num_bits and bit t (Int.num_bits-1) = vdd (i.e. the msb of the resulting Int.t is set), then the result is negative.
If t is Signal.t and not a constant value, an exception is raised.

val to_int32_trunc : t -> int32

val to_int64_trunc : t -> int64

val to_int : t -> int

Same as to_int_trunc.

deprecated [since 2024-11] use [to_int_trunc]

val to_int32 : t -> int32

deprecated [since 2024-11] use [to_int32_trunc]

val to_int64 : t -> int64

deprecated [since 2024-11] use [to_int64_trunc]

val to_signed_int : t -> int

to_signed_int t treats t as signed and resizes it to fit exactly within an OCaml Int.t.

An exception is raised if the value cannot fit in the resulting int.
If t is Signal.t and not a constant value, an exception is raised.

val to_signed_int32 : t -> int32

val to_signed_int64 : t -> int64

val to_unsigned_int : t -> int

to_unsigned_int t treats t as unsigned and resizes it to fit exactly within an OCaml Int.t.

An exception is raised if the value cannot fit in the resulting int.
The value int value must be unsigned (so the max width is Int.num_bits - 1).
If t is Signal.t and not a constant value, an exception is raised.

val to_unsigned_int32 : t -> int32

val to_unsigned_int64 : t -> int64

val to_bool : t -> bool

Convert signal to a bool. The signal must be 1 bit wide.

val to_char : t -> char

Convert signal to a char. The signal must be 8 bits wide.

val to_ascii_string_lsb : t -> string

Convert into a string, with the first character being from the least-significant bits of the signal. The signal width must be a multiple of 8 bits.

val to_ascii_string_msb : t -> string

Convert into a string, with the first character being from the most-significant bits of the signal. The signal width must be a multiple of 8 bits.

val to_bstr : t -> string

create binary string from signal

val to_bigint : t -> signedness:Hardcaml.Signedness.t -> Bigint.t

Convert bits to a Zarith.t

val bits_msb : t -> t list

convert signal to a list of bits with msb at head of list

val bits_lsb : t -> t list

convert signal to a list of bits with lsb at head of list

val to_array : t -> t array

to_array s convert signal s to array of bits with lsb at index 0

val of_array : t array -> t

of_array a convert array a of bits to signal with lsb at index 0

val repeat : t -> count:int -> t

repeat signal count times

val split_in_half_msb : ?msbs:int -> t -> t * t

Split signal in half. The most significant bits will be in the left half of the returned tuple.

If msbs is not provided, the signal will be split in half with the MSB part possibly containing one more bit.
If msbs is provided, msbs most significant bits will be split off.

val split_in_half_lsb : ?lsbs:int -> t -> t * t

Same as split_in_half_msb, but

If lsbs is not provided, the LSB part might have one more bit.
If lsbs is provided, lsbs least significant bits will be split off.

The most significant bits will still be in the left half of the tuple.

val split_lsb : ?exact:bool -> part_width:int -> t -> t list

Split signal into a list of signals with width equal to part_width. The least significant bits are at the head of the returned list. If exact is true the input signal width must be exactly divisable by part_width. When exact is false and the input signal width is not exactly divisible by part_width, the last element will contains residual bits.

eg:

  split_lsb ~part_width:4 16b0001_0010_0011_0100 =
    [ 4b0100; 4b0011; 4b0010; 4b0001 ]

  split_lsb ~exact:false ~part_width:4 17b11_0001_0010_0011_0100 =
    [ 4b0100; 4b0011; 4b0010; 4b0001; 2b11 ]

val split_msb : ?exact:bool -> part_width:int -> t -> t list

Like split_lsb except the most significant bits are at the head of the returned list. Residual bits when exact is false goes to the last element of the list, so in the general case split_lsb is not necessarily equivalent to split_msb |> List.rev.

val bswap : t -> t

val sll : t -> by:int -> t

shift left logical

val srl : t -> by:int -> t

shift right logical

val sra : t -> by:int -> t

shift right arithmetic

val rotl : t -> by:int -> t

rotate left

val rotr : t -> by:int -> t

rotate right

val log_shift : f:(t -> by:int -> t) -> t -> by:t -> t

shift by variable amount

val uresize : t -> width:int -> t

uresize t ~width:w returns the unsigned resize of t to width w. If w = width t, this is a no-op. If w < width t, this selects the w low bits of t. If w > width t, this extends t with zero (w - width t).

val sresize : t -> width:int -> t

sresize t ~width:w returns the signed resize of t to width w. If w = width t, this is a no-op. If w < width t, this selects the w low bits of t. If w > width t, this extends t with w - width t copies of msb t.

val uextend : t -> width:int -> t

uextend t ~width:w behaves similarly to uresize t ~width:w but asserts that w >= width to prevent inadvertently chopping the signal.

val sextend : t -> width:int -> t

sextend t ~width:w behaves similarly to sresize t ~width:w but asserts that w >= width to prevent inadvertently chopping the signal.

val ue : t -> t

unsigned resize by +1 bit

val se : t -> t

signed resize by +1 bit

val resize_list : resize:(t -> int -> t) -> t list -> t list

resize_list ~resize l finds the maximum width in l and applies resize el max to each element.

val resize_op2 : resize:(t -> int -> t) -> (t -> t -> t) -> t -> t -> t

resize_op2 ~resize f a b applies resize x w to a and b where w is the maximum of their widths. It then returns f a b

val reduce : f:('a -> 'a -> 'a) -> 'a list -> 'a

fold 'op' though list

val reverse : t -> t

reverse bits

val mod_counter : max:int -> t -> t

mod_counter max t is if t = max then 0 else (t + 1), and can be used to count from 0 to max then from zero again. If max == (1<<n - 1), then a comparator is not generated and overflow arithmetic is used instead.

val compute_arity : steps:int -> int -> int

compute_arity ~steps num_values computes the tree arity required to reduce num_values in steps. steps<=0 raises.

val compute_tree_branches : steps:int -> int -> int list

compute_tree_branches ~steps num_values returns a list of length steps of branching factors required to reduce num_values. This tends to produce a slightly more balanced sequence than just applying compute_arity at every step.

val tree : arity:int -> f:('a list -> 'a) -> 'a list -> 'a

tree ~arity ~f input creates a tree of operations. The arity of the operator is configurable. tree raises if input = [].

val priority_select : 
  ?branching_factor:int ->
  (t, t) Hardcaml__.Comb_intf.with_valid2 list ->
  (t, t) Hardcaml__.Comb_intf.with_valid2

priority_select cases returns the value associated with the first case whose valid signal is high. valid will be set low in the returned with_valid if no case is selected.

val priority_select_with_default : 
  ?branching_factor:int ->
  (t, t) Hardcaml__.Comb_intf.with_valid2 list ->
  default:t ->
  t

Same as priority_select except returns default if no case matches.

val onehot_select : 
  ?branching_factor:int ->
  (t, t) Hardcaml__.Comb_intf.with_valid2 list ->
  t

Select a case where one and only one valid signal is enabled. If more than one case is valid then the return value is undefined. If no cases are valid, 0 is returned by the current implementation, though this should not be relied upon.

val popcount : ?branching_factor:int -> t -> t

popcount t returns the number of bits set in t.

val is_pow2 : ?branching_factor:int -> t -> t

is_pow2 t returns a bit to indicate if t is a power of 2.

val leading_ones : ?branching_factor:int -> t -> t

leading_ones t returns the number of consecutive 1s from the most significant bit of t down.

val trailing_ones : ?branching_factor:int -> t -> t

trailing_ones t returns the number of consecutive 1s from the least significant bit of t up.

val leading_zeros : ?branching_factor:int -> t -> t

leading_zeros t returns the number of consecutive 0s from the most significant bit of t down.

val trailing_zeros : ?branching_factor:int -> t -> t

trailing_zeros t returns the number of consecutive 0s from the least significant bit of t up.

val floor_log2 : 
  ?branching_factor:int ->
  t ->
  (t, t) Hardcaml__.Comb_intf.with_valid2

floor_log2 x returns the floor of log-base-2 of x. x is treated as unsigned and an error is indicated by valid = gnd in the return value if x = 0.

val ceil_log2 : 
  ?branching_factor:int ->
  t ->
  (t, t) Hardcaml__.Comb_intf.with_valid2

ceil_log2 x returns the ceiling of log-base-2 of x. x is treated as unsigned and an error is indicated by valid = gnd in the return value if x = 0.

val binary_to_onehot : t -> t

convert binary to onehot

val onehot_to_binary : t -> t

convert onehot to binary

val binary_to_gray : t -> t

convert binary to gray code

val gray_to_binary : t -> t

convert gray code to binary

val gray_increment : t -> by:int -> t

Increment a gray code value. The implementation converts to binary, increments the binary value, then converts back to gray code.

val any_bit_set : t -> t

any_bit_set t returns vdd if at least one bit if set in t and gnd otherwise.

val all_bits_set : t -> t

all_bits_set t returns vdd if all bits in t are set and gnd otherwise.

val no_bits_set : t -> t

no_bits_set t returns vdd if no bits in t are set and gnd otherwise.

val incr : ?by:int -> t -> t

Increment (defaults to 1). Wrap on overflow.

val decr : ?by:int -> t -> t

Decrement (defaults to 1). Wrap on overflow.

module With_zero_width : sig ... end

Concatention, selection and resizing functions for signals encoded as an option where None means zero width.

module type Typed_math = sig ... end

module Unsigned : Typed_math

Unsigned vector operations (ie may operate on Bits.t or Signal.t directly).

module Signed : Typed_math

Signed vector operations (ie may operate on Bits.t or Signal.t directly).

val input : Base.string -> Base.int -> t

input "name" width creates an input with "name" and given width in bits.

val cofactor : var:t -> t -> f:t -> t

cofactor ~var p ~f computes the cofactor of each bit of f wrt to each bit of var. p must be a constant and represents the value of var which which to perform the cofactor.

val forall : t -> f:t -> t

universal quantification

val exists : t -> f:t -> t

existential quantification

val cnf : ?show_hidden:Base.bool -> t -> Cnf.t

Create CNF for each bit of the given vector. In the resulting CNF the bits are logically AND'd.