package hardcaml

  1. Overview
  2. Docs
package hardcaml
Legend:
Library
Module
Module type
Parameter
Class
Class type

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

OCaml

Innovation. Community. Security.

GitHub Discord Twitter Peertube RSS
About
Changelog Releases Industrial Users Academic Users Why OCaml
Ecosystem
Packages Community Events OCaml Planet Jobs
Resources
Install OCaml Get Started Platform Tools Language Manual Standard Library API Books Exercises Papers OCaml Playground Logo
Policies
Carbon Footprint Governance Privacy Code of Conduct