Training Ladder Logic & IEC 61131-3 Programming Ladder Logic — Boolean Algebra, Karnaugh Maps & Formal Verification
1 / 2

Ladder Logic — Boolean Algebra, Karnaugh Maps & Formal Verification

60 min Ladder Logic & IEC 61131-3 Programming

Ladder Logic — Boolean Algebra, Karnaugh Maps & Formal Verification

Ladder Diagram (LD) is the most widely used IEC 61131-3 language because its relay-schematic metaphor is accessible to electricians and engineers alike. However, industrial programs often grow to thousands of rungs with redundant or contradictory logic. PhD-level mastery requires reducing Boolean expressions, verifying correctness, and understanding the formal underpinnings of the language.

1. Contact & Coil Semantics

Each rung computes a Boolean function of input contacts (XIC = normally-open, XIO = normally-closed) and drives one or more output coils (OTE = non-retentive, OTL/OTU = latch/unlatch). A rung evaluates to TRUE when there is a continuous path of TRUE contacts from left power rail to output coil. The PLC evaluates all rungs sequentially each scan — this is fundamentally a Boolean function evaluation engine.

2. Boolean Minimisation with Karnaugh Maps

The Karnaugh map (K-map) is a graphical method for minimising a Boolean SOP (Sum-of-Products) expression. For a 4-variable function $F(A,B,C,D)$, the 16-cell K-map groups 1-cells into power-of-2 rectangles, each rectangle yielding one product term. The minimal SOP has the fewest literals and gates, reducing rung count and execution time.

Example: given a 4-variable function with minterms $\{0,2,5,7,8,10,13,15\}$, the K-map reveals:

$$F = \overline{B}\,\overline{D} + BD = \overline{B \oplus D}$$

The XOR implementation uses one fewer gate than the SOP form — a non-trivial saving in a hot-standby safety loop where every contact represents a physical relay with finite MTBF.

3. De Morgan and Rung Conversion

De Morgan's theorems are essential for converting AND-of-NORs into OR-of-NANDs (changing XIC contacts to XIO and vice versa):

$$\overline{A+B} = \overline{A}\cdot\overline{B} \qquad \overline{A\cdot B} = \overline{A}+\overline{B}$$

In ladder form, a rung implementing $Y = \overline{A+B}$ (NOR) is physically impossible with a single power rail — De Morgan converts it to $Y = \overline{A} \cdot \overline{B}$, implemented as two series XIO contacts.

4. Formal Verification Concepts

Safety-critical applications (SIL-2/SIL-3) require formal verification beyond testing. The two main approaches are:

  • Truth-table exhaustion — for $n \leq 20$ inputs, enumerate all $2^n$ combinations and check outputs against specifications. Feasible for individual function blocks.
  • SAT solving — model-check the combined safety function. Modern SAT solvers (Z3, MiniSat) can handle hundreds of Boolean variables and verify temporal properties (e.g., "the emergency stop coil is energised within 10 ms of input de-energisation").
Worked Example — 3-Rung Interlock Verification

Given: $Y_1 = A \cdot B$, $Y_2 = (A+C)\cdot\overline{D}$, $Y_3 = Y_1 + (B \cdot D)$. Verify that it is impossible for $Y_2$ and $Y_3$ to both be TRUE simultaneously when $D=1$.

When $D=1$: $Y_2 = (A+C)\cdot 0 = 0$. So $Y_2 = 0$ whenever $D=1$, regardless of $Y_3$. The interlock is valid. ✓

Now verify $Y_1=1 \Rightarrow Y_2=0$ when $D=1$: trivially true from above. ✓

Ladder Logic Simulator — Boolean Verification
Y1 = A·B0
Y2 = (A+C)·/D1
Y3 = Y1+(B·D)0

Practice Problems

1. Use a 3-variable K-map to minimise $F = \sum(0,1,4,5,6,7)$. Write the minimal SOP and implement it as a ladder rung.
2. Apply De Morgan to convert $Y = \overline{(A\cdot B + C)}$ into a form implementable with XIC and XIO contacts only.
3. A safety interlock requires $Y_{EStop} = 1$ if ANY of three E-stop buttons are pressed OR if the door guard is open. Write the ladder rung and verify by truth table (16 combinations).
IEC 61131-3 Timers, Counters & Structured Text