Component library¶
Reusable building blocks, under intrepyd.lib. The package docstring states the
API convention (combinational blocks are functions, stateful blocks are
classes); eda holds hardware/EDA blocks and plc the IEC 61131-3 function
blocks.
lib ¶
A structured library of reusable intrepyd components.
Two submodules:
- :mod:
intrepyd.lib.eda: hardware/EDA blocks — a clock, a counter, latches, flip-flops, a shift register, a multiplexer. - :mod:
intrepyd.lib.plc: the standard function blocks of IEC 61131-3, as a PLC program uses them — edge detectors (R_TRIG, F_TRIG), bistables (SR, RS), counters (CTU, CTD, CTUD) and timers (TON, TOF, TP).
and :mod:intrepyd.lib.catalogue, which describes every block of both as data
(its parameters, pins, outputs and types) for tools.
API convention¶
- A combinational block is a function
mk_<name>(ctx, ...) -> netthat returns its output net directly (for example :func:~intrepyd.lib.eda.mk_mux). - A block that builds its own state and needs no feedback from the caller
is also a function; it creates its internal latches and returns the output
net(s) (for example :func:
~intrepyd.lib.eda.mk_clock, :func:~intrepyd.lib.eda.mk_counter, and every block in :mod:intrepyd.lib.plc). - A stateful block whose next value depends on signals the caller provides
after construction is a class: build it, then call
set_init_next(...)to close the loop (for example :class:~intrepyd.lib.eda.LatchD, :class:~intrepyd.lib.eda.Delay, the flip-flops, and :class:~intrepyd.lib.eda.ShiftRegister). This two-step shape is what lets a component feed back into itself.
EDA blocks¶
eda ¶
Implementation of EDA-specific components
LatchD ¶
LatchD (LD)
A latch with enable
Symbol: ____ | | D ---| LD |--- Q | | E ---| | |____|
Diagram: A latch wrapped around a mux
+--------------------+
| __ |
| | \ ____ |
+--| 0 | | | |
| |----| L |---+--- Q
D ---| 1 | | | |/ |__| | | E -----+
Args: ctx: the context to use name: the unique name t: the type of the data stored
set_init_next ¶
Sets the initial value of the latch
Args: init: the initial value D: the input signal E: the enable signal
Delay ¶
Delay (D)
Delays a signal by one full clock cycle
Symbol: ____ | | D ---| D |--- Q | | |> | |____|
Diagram: Two latches in series
____ ____
| | | |
| D --- | L | --- | L | --- Q |
|---|---|---|---|---|
| ____ | ____ |
Args: ctx: the context to use name: the unique name t: the type of the data stored
set_init_next ¶
Sets the initial value of the latch
Args: init: the "fill" value for the first cycle D: the input signal
FlipFlopD ¶
Flip Flop D (FFD)
Args: ctx: the context to use name: the unique name t: the type of the data stored C: the clock signal
Returns: Q: the value stored in the flip flop
Symbol: _____ | | D ---| FFD |--- Q | | C ---|> | |_____|
Diagram: It consists of a master DL and a slave LD. The diagram shows the raising-edge version (notice the negated clock in the master latchD)
+---------------------+
| ____ |
_____ | | | |
| | +--| L |---+ __ |
D ----| LD |---+ | | | | \ | | | | || +--| 0 | | C -+-o| | | | |--+-- Q | |_| +------------------| 1 | | |__/ | | +---------------------------------+
Args: ctx: the context to use name: the unique name t: the type of the data stored C: the clock signal
set_init_next ¶
Sets the initial and next value
Args: init: the initial value D: the flip flop input signal
FlipFlopDE ¶
Flip Flop D with Enable (FFDE)
Symbol: _____ | | D ---| FFD |--- Q E ---| | C ---|> | |_____|
Diagram:
It consists of a FFD wrapped by a mux
+--------------------+ | __ | | | \ _____ | +--| 0 | | | | | |---| FFD |---+--- Q D ---| 1 | | | |/ +-|> | | | |___| E -----+ | | C ---------+
Args: ctx: the context to use name: the unique name t: the type of the data stored C: the clock signal
set_init_next ¶
Sets the initial and next value
Args: init: the initial value D: the flip flop input signal E: the flip flop enable signal
ShiftRegister ¶
Shift register (SR)
A chain of length one-cycle registers: the output q is the input
d delayed by length cycles. stages[i] is the output of the
i-th register, so stages[0] is d delayed by one cycle and
stages[-1] is q.
Diagram::
____ ____ ____
| | | | | |
D ---| L0 |---| L1 |-- ... --|Ln-1|--- Q || || |____|
Args: ctx: the context to use name: the unique name t: the type of the data shifted length: the number of stages (must be >= 1)
set_init_next ¶
Closes the register chain.
Args: init: the value every stage holds for its first cycles d: the input signal shifted into the first stage
mk_counter ¶
Counts from init to limit by increment. Returns the value of the counter and whether the limit has been reached or not. An enable signal and a reset signal may also be specified.
Args: context: the context to use name: the unique name of this counter type: the type of the data stored in the counter limit: the limit after which the counter saturates init (=0): the initial value of the counter increment (=1): the increment value enable (=true): the counter is incremented only if enable is true reset (=false): resets the counter to the initial value
Returns: counter: the current value of the counter Q: true iff the counter has reached saturation
mk_mux ¶
A 2:1 multiplexer: returns in1 when sel is true, else in0.
Symbol::
__
| | 1 |--- Q Q = in1 if sel else in0
in1 --| | | 0 | in0 --|__/ | sel ----+
Args: ctx: the context to use sel: the boolean selector net in0: the net selected when sel is false in1: the net selected when sel is true name: an optional name for the output net
Returns: the output net
PLC blocks (IEC 61131-3)¶
plc ¶
The standard function blocks of IEC 61131-3, the PLC programming standard, as reusable intrepyd components.
Everything here is modelled on a synchronous cycle: one simulation step is one PLC scan cycle. The edge detectors are combinational in the current and the previous cycle (so a detected edge appears in the same cycle), while the bistables and the counter hold their output in a latch, so it updates on the next cycle — the usual way these blocks enter a cycle-based model checker.
mk_r_trig ¶
Rising-edge detector (R_TRIG). Q is true for the one cycle in which
clk goes from false to true. Following IEC 61131-3, the internal memory
starts false, so an initial clk already true counts as a rising edge.
Q := clk AND NOT M; M := clk; M(0) = false
Args:
ctx: the context to use
clk: the boolean signal to watch
name: the unique name (the output net is named name)
Returns:
the boolean edge net Q
mk_f_trig ¶
Falling-edge detector (F_TRIG). Q is true for the one cycle in which
clk goes from true to false. Following IEC 61131-3, the internal memory
starts true, so no edge is reported in the first cycle.
Q := NOT clk AND M; M := clk; M(0) = true
Args:
ctx: the context to use
clk: the boolean signal to watch
name: the unique name (the output net is named name)
Returns:
the boolean edge net Q
mk_sr ¶
Set-dominant bistable (SR). The output is held in a latch, starting false;
when both s and r are true, the set wins.
Q(0) = false; Q := s OR (Q AND NOT r)
Args:
ctx: the context to use
s: the set signal
r: the reset signal
name: the unique name (the output latch is named name)
Returns:
the boolean output net Q
mk_rs ¶
Reset-dominant bistable (RS). The output is held in a latch, starting
false; when both s and r are true, the reset wins.
Q(0) = false; Q := NOT r AND (s OR Q)
Args:
ctx: the context to use
s: the set signal
r: the reset signal
name: the unique name (the output latch is named name)
Returns:
the boolean output net Q
mk_ctu ¶
Up counter (CTU). On each rising edge of cu the count CV goes up by
one, saturating at the preset pv; reset forces CV back to zero.
Q is true while CV >= pv. CV starts at zero.
Args:
ctx: the context to use
name: the unique name (CV is named name, Q name.Q)
cu: the count-up signal (counted on its rising edge)
reset: resets the count to zero when true
pv: the preset value net (of type typ)
typ: the type of the count
Returns:
a pair (CV, Q): the current count net and the boolean CV >= pv
mk_ton ¶
On-delay timer (TON). Q becomes true once in_ has been true for
pt consecutive cycles, and stays true while in_ stays true;
in_ going false resets the elapsed time and Q.
Args:
ctx: the context to use
name: the unique name (ET is name, Q is name.Q)
in_: the boolean input
pt: the preset time, in cycles, as a net of type typ
typ: the type counting the elapsed time
Returns:
a pair (ET, Q): the elapsed-time net and the boolean output
mk_tof ¶
Off-delay timer (TOF). Q follows in_ up, and when in_ goes
false Q stays true for pt more cycles before dropping. Q starts
false.
Args:
ctx: the context to use
name: the unique name (ET is name, Q is name.Q)
in_: the boolean input
pt: the preset time, in cycles, as a net of type typ
typ: the type counting the elapsed time
Returns:
a pair (ET, Q): the elapsed-time net and the boolean output
mk_tp ¶
Pulse timer (TP). A rising edge of in_ makes Q true for exactly
pt cycles; the pulse is not retriggerable (edges during the pulse are
ignored).
Args:
ctx: the context to use
name: the unique name (ET is name, Q is name.Q)
in_: the boolean input
pt: the pulse width, in cycles, as a net of type typ
typ: the type counting the elapsed time
Returns:
a pair (ET, Q): the elapsed-time net and the boolean output
mk_ctd ¶
Down counter (CTD). load sets the count CV to the preset pv;
each rising edge of cd lowers CV by one, down to zero. Q is true
while CV <= 0. CV starts at zero (so Q starts true until loaded).
Args:
ctx: the context to use
name: the unique name (CV is name, Q is name.Q)
cd: the count-down signal (counted on its rising edge)
load: loads pv into CV when true
pv: the preset value net (of type typ)
typ: the type of the count
Returns:
a pair (CV, Q): the current count net and the boolean CV <= 0
mk_ctud ¶
Up-down counter (CTUD). A rising edge of cu raises the count CV, a
rising edge of cd lowers it (down to zero); reset forces it to zero
and load sets it to the preset pv, with priority reset > load > up >
down. QU is CV >= pv and QD is CV <= 0. CV starts at
zero.
Args:
ctx: the context to use
name: the unique name (CV is name, QU/QD are
name.QU/name.QD)
cu: the count-up signal (counted on its rising edge)
cd: the count-down signal (counted on its rising edge)
reset: forces CV to zero when true
load: loads pv into CV when true
pv: the preset value net (of type typ)
typ: the type of the count
Returns:
a triple (CV, QU, QD)
The catalogue¶
Every block above, described as data for tools (the circuit editor's palette,
intrepyd.diagram). python -m intrepyd.diagram catalogue prints it as JSON.
catalogue ¶
The catalogue of :mod:intrepyd.lib: every library block described as data —
what it is called, its parameters, its input pins and their types, its outputs
and their types, and how to call it. It is what a tool needs to offer the
blocks without reading their code: the intrepid-vscode circuit editor builds
its palette from it (python -m intrepyd.diagram catalogue prints it as
JSON), and :mod:intrepyd.diagram builds the blocks of a diagram with it.
A block (one entry of BLOCKS) has:
module("eda"or"plc"),symbol(the name in that module),form("func": a function returning its outputs;"class": built, then closed withset_init_next),category,labelanddescription;params: the scalar parameters, each{"key", "kind", "label", "default"}withkind"type"(a type name:bool,int8, ...) or"int"(an integer);inputs: the input pins in order, each{"port", "at", "type"}(anulltype takes any), whereatis"ctor"(needed to build the block) or"setnext"(given toset_init_next, so it may come from the block's own output), and an"optional": truepin may stay unwired (the block's default is used);outputs: the outputs in order, each{"name", "type"}, andprimary, the index of the output a wire carries when it does not say;ctorArgsandsetnextArgs: the arguments of the call, each one of{"kind": "ctx"},{"kind": "name"}(the instance name),{"kind": "input", "port"}(the net wired to that pin; with"keyword", passed by that keyword and only when wired),{"kind": "type", "key"}and{"kind": "int", "key"}(a parameter);nameAsKeywordpasses the name asname=...instead.
A type is {"kind": "bool"}, {"kind": "param", "key"} (the type a
parameter names) or {"kind": "like", "port"} (the type of another input).