The horizontal line shown in a timeline to
represent the zero point of a waveform.
The section of a signal type to the left of the turnstile, consisting of a list of
key types. Each array dimension of a variable has a corresponding key type in the variable’s
block prefix. In definitions, block prefixes contain block prefix variables represented by
the letter Γ (gamma). See the article on blocks and arrays for
An operation that loops over an array dimension and accumulates the entries along that dimension to produce an
array with one fewer dimension. A varargs primitive can be made to perform a fold operation by setting it
to block mode. For example, an AND gate set to block level 1, given as input a 1-dimensional array, will output
a single Boolean value that is True if and only if all of the values in the input array are True.
Custom fold operations can be written using the One Index Delay and Fold End primitives. See the article on
blocks and arrays for more information.
Value Y is instantaneously dependent upon value X if X must be
computed before Y can be computed within a single frame.
CertSAFE only evaluates this statically; so, for example, the output
of a Boolean switch is instantaneously dependent on all three of its inputs
even though only two of the input values are used on any frame.
A table whose inputs and outputs are
continuous, with the output values determined by interpolating
between known data points. Interpolation tables are commonly used for
approximating complex functions.
A grid location where three or more wire ends come
together. Represented as a thick black dot in CertSAFE. Contrast with
The type used to index an array dimension. Each dimension of an array has a corresponding key type, listed in the
block prefix of the variable. For example, a variable with type “UInt8 ⊢ Float32” is a
single-dimensional array of 256 floating point values. The key type of the single array dimension is UInt8, and
the scalar type is Float32.
A primitive that simply outputs a constant value,
like True or 3.14. Numeric literals are polymorphic in
A collection of components organized for fast access
during diagram creation. There is a default palette that every
project gets on creation, and it is also possible to create
user-defined palettes. Palettes can be displayed in the Palette
Used in reference to components that operate on each element of an array individually and independently of every
other element. When applied to multiple arrays, a pointwise operation is applied to elements at corresponding
locations in the input arrays.
A unit is polymorphic if it can be used with
various different data types for some of its I/Os. For
example, the switch primitive is polymorphic because the type of
data being switched upon can be different for different switch units.
A polymorphic unit has type variables in its type signature.
The display and user interaction aspects of a
component, including how the component is drawn, where its
pins are positioned, etc.
A component that is built into CertSAFE rather
than being user-defined. Boolean logic gates, arithmetic operations,
and one-frame delays are examples of some of the types of primitives
A constraint that restricts a type variable to be
instantiated only with data types that support certain
operations. A type class is not itself a data type, but rather a
restriction on which data types can be used in the presence of
polymorphism. For example, the Ordered type class imposes a
requirement that a type variable be substituted with a type that
supports “less than” / “greater than” comparisons.
A description of how a unit interacts with
CertSAFE’s type inference
system. The type signature of a unit can be viewed in CertSAFE by
mousing over the unit.
A placeholder where an actual data type will
be substituted in the type signature of a unit that is
polymorphic. Type variables are represented by Greek letters in
the CertSAFE user interface to distinguish them from ordinary data
types. Contrast with type constant.
A class of unit. Multiple individual units can
have the same unit type. “Switch” is an example of a unit type, since
a CertSAFE project can contain many individual switch units.
Similarly, each diagram, stitch, and table in a project
is a unit type that can be specified as the implementation for a
A pluggable chunk of logic with inputs and outputs
(I/Os). The main elements making up a CertSAFE model. The
implementation of a component is a unit.
A primitive component that has a variable number of inputs, controlled by a numeric property. Examples of
varargs primitives include the Boolean AND/OR/XOR components and the Min/Max Selector components. Varargs
primitives can be set to block mode to perform a fold over an input array.
A line that can connect pins and other wire
segments together to form a wire network. Each wire segment has
two wire ends. Together with components,
wire segments are one of the two types of objects that can be placed in a