Blocks

The blocks of the palette, by its sections. Each has its input pins on the left, in the order below, and its outputs on the right.

Sources & sinks

Block	Inputs	Output	What it is
In		its value	An input of the circuit: its value is free at each step, given by the stimuli, chosen by Verify. Its type is in its properties. Inside a subsystem, a pin of the subsystem.
Out	in		An output of the circuit. Inside a subsystem, a pin of the subsystem.
Constant		its value	A number, of the type in its properties (int8 by default).
true, false			The boolean constants.

Logic

The gates take booleans and give a boolean. AND, OR and XOR take 2 to 8 inputs (inputs in their properties).

Block	Inputs	Output
AND	a, b (or in0 … in7)	true when all are true
OR	a, b (or in0 … in7)	true when one is true
NOT	in	the negation
XOR	a, b (or in0 … in7)	exclusive or
XNOR	a, b	equivalence: true when both are equal
IMPLIES	a, b	a ⇒ b: false only when a is true and b false

Compare

=, ≠, <, ≤, >, ≥: two inputs a and b of one type, a boolean output (a < b, …).

Math

Block	Inputs	Output
+	a, b (or in0 … in7)	the sum
−	a, b	the difference a − b
×	a, b (or in0 … in7)	the product
÷	a, b	the quotient a ÷ b
mod	a, b	the remainder
−x	in	the negation

The operands are of one type, the result of that type. Machine integers wrap around on overflow.

Routing

Switch: inputs if (a boolean), then, else (of one type); its output is then when if holds, else otherwise.

State

Unit delay (1/z): inputs init and next, of its type. Its output is init at the first step, then at each step the value next had at the step before. Every loop of wires goes through one.

Verification

Block	Input	What it is
Assertion	in, a boolean	must hold at every step: Verify proves it, or finds the steps that break it
Target	in, a boolean	a condition to reach: Verify finds the steps that reach it, or proves it unreachable
Assume	in, a boolean	a condition the inputs keep to at every step: Verify and the MC/DC tests consider only the runs where it holds

See Properties and verdicts.

Hierarchy

Subsystem: a part of the circuit as one block; its In and Out blocks are its pins. Double-click to open it. See Circuits.

EDA

The blocks of intrepyd's library for hardware designs. type is a parameter in their properties.

Block	Inputs	Outputs	What it is
MUX 2:1	sel, in0, in1	out	in1 if sel, else in0
Clock		clk, in	a clock signal, and the free input that drives its first cycle
Counter	limit, init?, increment?, enable?, reset?	counter, Q	counts from init by increment while enable holds, up to limit; reset brings it back to init; Q: it reached the limit. type (int8)
Latch D (LD)	init, d, e	q	a data latch with enable: q holds d when e is true
Delay	init, d	q	d delayed by one full clock cycle
Flip-flop D (FFD)	c, init, d	q	a D flip-flop clocked by c
Flip-flop D+E (FFDE)	c, init, d, e	q	a D flip-flop with enable, clocked by c
Shift register	init, d	q	d delayed by length cycles (3)

The pins marked ? are optional: they may stay unwired.

PLC

The function blocks of IEC 61131-3, from intrepyd's library. Times are in steps (cycles).

Block	Inputs	Outputs	What it is
R_TRIG	clk	Q	rising-edge detector
F_TRIG	clk	Q	falling-edge detector
SR bistable	s, r	Q	set-dominant bistable: Q := s or (Q and not r)
RS bistable	s, r	Q	reset-dominant bistable: Q := not r and (s or Q)
CTU	cu, reset, pv	CV, Q	counts up on cu's rising edge, saturates at the preset pv
CTD	cd, load, pv	CV, Q	counts down on cd's rising edge from the preset
CTUD	cu, cd, reset, load, pv	CV, QU, QD	up and down counter
TON	in, pt	ET, Q	on-delay timer, preset pt
TOF	in, pt	ET, Q	off-delay timer, preset pt
TP	in, pt	ET, Q	pulse timer, preset pt

The bistables keep their output in a latch, starting false: Q at a step is what s and r set at the steps before. The counters and timers have a type (int8).

A block with several outputs is wired from the one you pick: drag from that output's pin. The palette shows the library blocks of the intrepyd you use, so a newer intrepyd's blocks show up without a new editor.