Module Hardcaml.Scope

Scopes control the process of hierarchical circuit generation.

They track a circuit database of instantiated modules, and a scheme for managing the naming of signals within the design.

module Path : sig ... end
module Naming_scheme : sig ... end

Control of name generation in a hierarchy of modules. The position of a module within a hierarchy is determined by a path which leads back to the (single) top most parent module. Signal names may be pre-pended with some representation of that path.

type t
val sexp_of_t : t -> Sexplib0.Sexp.t
val create : ?flatten_design:Base.bool -> ?auto_label_hierarchical_ports:Base.bool -> ?trace_properties:Base.bool -> ?naming_scheme:Naming_scheme.t -> ?name:Base.string -> Base.unit -> t

create ?flatten_design ?naming_scheme ?name () creates a new scope. If flatten_design is true, then all module instantions are inlined. Names for wires are determined by naming_scheme.

val sub_scope : t -> Base.string -> t

sub_scope t label returns a new scope with (mangled) label appended to its hierarchical path

val path : t -> Path.t

path t returns the Path.t associated with t. This will determine the prefix used when naming modules that are associated with this scope.

val circuit_database : t -> Circuit_database.t

circuit_database t returns the circuit database associated with t. Note that circuit databases are shared among sub_scopes.

val flatten_design : t -> Base.bool

flatten_design t returns true when HardCaml will inline all module instantiations.

val auto_label_hierarchical_ports : t -> Base.bool

auto_label_hierarical_ports t returns true when Hardcaml will add names to input and outputs ports of each hierarchical module.

This is useful with the interactive waveform viewer. The port names are prefixed with i$ and o$ and will be arranged in a tree view automactically.

val trace_properties : t -> Base.bool

trace_properties t returns true when tracing of ltl properties is enabled

val naming_scheme : t -> Naming_scheme.t

naming_scheme t returns the Naming.t that t was constructed with.

val name : ?sep:Base.string -> t -> Base.string -> Base.string

name ?sep t signal string creates a heirarchical name based on the path of t and string. sep, when provided, determines the separator for path components in the heirarchical name (default is $).

val instance : t -> Base.string Base.option

Return the current (mangled) instance name. The top level module has no instance name, so returns None.

val naming : ?sep:Base.string -> t -> Signal.t -> Base.string -> Signal.t

Creates a hierarchical name, built with name, and applies it to the signal.

This is typically used as a partial application to construct a new signal naming operator, .e.g:

let (--) = naming scope in
let named_signal = some_signal -- "data" in
val make_ltl_ap : t -> Base.string -> Signal.t -> Property.LTL.path

Creates an atomic proposition for use in an LTL formula, naming the AP with the scope's name and the provided string argument

val add_assertion : t -> Base.string -> Signal.t -> Base.unit
val add_ltl_property : t -> Base.string -> Property.LTL.path -> Base.unit
val assertion_manager : t -> Assertion_manager.t
val property_manager : t -> Property_manager.t
val assert_signal_in_always : t -> Base.string -> Signal.t -> Always.t

add an assertion to the scope's assertion manager