The five IEC 61131-3 languages¶

Ask how many languages IEC 61131-3 defines and you will be told five. That answer was right for twenty years and is now out of date, so it is worth getting the current shape of the standard straight before looking at the syntax.

Edition 4.0, published 2025-05-22, describes its suite as "the textual language structured text (ST), and the graphical languages, ladder diagram (LD) and function block diagram (FBD)". Sequential function chart sits outside that suite: "An additional set of graphical and equivalent textual elements named sequential function chart (SFC) is defined for structuring the internal organization of programs and function blocks". Instruction list was deprecated in edition 3.0 in 2013 and removed outright in edition 4.0.

Those edition facts come from the IEC catalogue entries for IEC 61131-3:2025, edition 4.0 of 2025-05-22, and IEC 61131-3:2013, edition 3.0 of 2013-02-20.

So the standard today names three languages plus a structuring notation. Five names still matter, because IL runs in installed plants that will outlive the standard that dropped it, and because every tool you will benchmark still parses it. All five are below.

language	form	in Ed 4.0 (2025)	what it is for
LD	graphical	yes	boolean interlocks, drawn as relay contacts and coils
FBD	graphical	yes	signal flow, reusable blocks, analog chains
ST	textual	yes	arithmetic, loops, anything with structure
SFC	graphical, with textual equivalents	yes, as structuring elements	sequences: steps and the transitions between them
IL	textual	removed; deprecated since 2013	legacy code you still have to read

One circuit, five ways¶

The four notations the standard still defines, plus the one it dropped, all say the same thing here:

Run := (Start OR Run) AND NOT Stop

Press Start and the motor runs. Release Start and it keeps running, because Run feeds itself. Press Stop and it drops out. That is a seal-in latch, and lesson 1.4 verifies exactly this circuit.

Every rendering below is a benchmark in the catalog, and every one is a file you can download and run.

file	what it is	size	sha256
`seal_in.ld`	ladder program, textual DSL	0.1 KB	`e7eae122c6ce`
`program.xml`	ladder program, PLCopen XML	2.1 KB	`ef99cd998a07`
`seal_in.st`	structured text	0.3 KB	`151889afdc34`
`fbd_seal_in_program.xml`	ladder program, PLCopen XML	5.1 KB	`4248a110cf10`
`seal_in.il`	instruction list	0.5 KB	`2d1ddbb717ae`

Ladder diagram, drawn¶

This is what an electrician sees. Power leaves the left rail, finds a path through Start or through the latched Run contact, is broken by the normally closed Stop, and energizes the coil. Nothing is written down; the meaning is in the drawing.

Ladder diagram, as text¶

benchmarks/motor_control/ld_seal_in/seal_in.ld

// seal_in: self-holding (seal-in) coil with stop
OTE(Run) := (XIC(Start) + XIC(Run)) * XIO(Stop) ;

The same rung in the K-LD textual notation. XIC is a normally open contact, examine if closed; XIO is normally closed; OTE is an output coil. Series becomes *, parallel becomes +. It reads like Boolean algebra because that is what a rung is.

Compact, diffable and reviewable, and also not what any vendor tool on the market actually exports, which is exactly why the suite carries both spellings as a syntax pair rather than picking one and calling the other a detail.

Ladder diagram, as PLCopen XML¶

benchmarks/motor_control/g_seal_in/program.xml (ladder program, PLCopen XML, 2.1 KB)

<?xml version="1.0" encoding="utf-8"?>
<project xmlns="http://www.plcopen.org/xml/tc6_0200">
  <fileHeader companyName="Anonymous" productName="Benchmark Suite" productVersion="1.0" creationDateTime="2026-07-09T00:00:00" />
  <contentHeader name="g_seal_in"><coordinateInfo><fbd><scaling x="1" y="1" /></fbd><ld><scaling x="1" y="1" /></ld><sfc><scaling x="1" y="1" /></sfc></coordinateInfo></contentHeader>
  <types><dataTypes /><pous><pou name="g_seal_in" pouType="program">
    <interface><inputVars><variable name="Start"><type><BOOL /></type></variable><variable name="Stop"><type><BOOL /></type></variable></inputVars><outputVars><variable name="Run"><type><BOOL /></type></variable></outputVars></interface>
    <body><LD>
      <leftPowerRail localId="0"><position x="0" y="0" /><connectionPointOut formalParameter="none" /></leftPowerRail>
      <contact localId="3" negated="false" storage="none" edge="none"><position x="20" y="10" /><connectionPointIn><connection refLocalId="0" /></connectionPointIn><connectionPointOut /><variable>Start</variable></contact><contact localId="4" negated="false" storage="none" edge="none"><position x="20" y="20" /><connectionPointIn><connection refLocalId="0" /></connectionPointIn><connectionPointOut /><variable>Run</variable></contact><contact localId="5" negated="true" storage="none" edge="none"><position x="80" y="10" /><connectionPointIn><connection refLocalId="3" /><connection refLocalId="4" /></connectionPointIn><connectionPointOut /><variable>Stop</variable></contact><coil localId="6" negated="false" storage="none"><position x="100" y="10" /><connectionPointIn><connection refLocalId="5" /></connectionPointIn><connectionPointOut /><variable>Run</variable></coil>
      <rightPowerRail localId="2147483646"><position x="400" y="0" /><connectionPointIn /></rightPowerRail>
    </LD></body>
  </pou></pous></types>
  <instances><configurations><configuration name="Config0"><resource name="Res0"><task name="tcyclic" interval="T#10ms" priority="0"><pouInstance name="inst0" typeName="g_seal_in" /></task></resource></configuration></configurations></instances>
</project>

The same rung again, and now it is a graph. Every element carries a localId, and every element names the elements it draws power from:

<coil localId="6" negated="false" storage="none">
  <connectionPointIn>
    <connection refLocalId="4" />
    <connection refLocalId="5" />
  </connectionPointIn>
  <variable>Run</variable>
</coil>

Two connections into one input is the parallel junction. There is no element for it and no line in the file that says "OR". A tool has to work that out, which is the whole subject of lesson 1.2.

Structured text¶

benchmarks/motor_control/st_seal_in/seal_in.st

(* seal_in: self-holding (seal-in) coil with stop.
   Structured Text rendering of ld_seal_in / g_seal_in.
   Run := (Start OR Run) AND NOT Stop *)
PROGRAM drive
  VAR_INPUT
    Start : BOOL;
    Stop  : BOOL;
  END_VAR
  VAR_OUTPUT
    Run : BOOL;
  END_VAR

  Run := (Start OR Run) AND NOT Stop;
END_PROGRAM

The shortest of the five, and the only one where the latch is visible as a latch, since Run appears on both sides of the assignment and anyone who has written code in any language reads that correctly on first sight. That matters when the reviewer is not a control engineer.

Function block diagram¶

benchmarks/motor_control/fbd_seal_in/program.xml (ladder program, PLCopen XML, 5.1 KB)

<?xml version="1.0" encoding="utf-8"?>
<!-- seal_in: self-holding (seal-in) coil with stop.
     Function Block Diagram rendering of ld_seal_in / g_seal_in.
     Run := (Start OR Run) AND NOT Stop -->
<project xmlns="http://www.plcopen.org/xml/tc6_0200">
  <fileHeader companyName="Anonymous" productName="Benchmark Suite" productVersion="1.0" creationDateTime="2026-08-26T00:00:00" />
  <contentHeader name="fbd_seal_in">
    <coordinateInfo><fbd><scaling x="1" y="1" /></fbd><ld><scaling x="1" y="1" /></ld><sfc><scaling x="1" y="1" /></sfc></coordinateInfo>
  </contentHeader>
  <types>
    <dataTypes />
    <pous>
      <pou name="drive" pouType="program">
        <interface>
          <inputVars>
            <variable name="Start"><type><BOOL /></type></variable>
            <variable name="Stop"><type><BOOL /></type></variable>
          </inputVars>
          <outputVars>
            <variable name="Run"><type><BOOL /></type></variable>
          </outputVars>
        </interface>
        <body>
          <FBD>
            <inVariable localId="1" height="20" width="80">
              <position x="20" y="20" />
              <connectionPointOut><relPosition x="80" y="10" /></connectionPointOut>
              <expression>Start</expression>
            </inVariable>
            <inVariable localId="2" height="20" width="80">
              <position x="20" y="60" />
              <connectionPointOut><relPosition x="80" y="10" /></connectionPointOut>
              <expression>Run</expression>
            </inVariable>
            <inVariable localId="3" height="20" width="80">
              <position x="20" y="140" />
              <connectionPointOut><relPosition x="80" y="10" /></connectionPointOut>
              <expression>Stop</expression>
            </inVariable>
            <block localId="4" width="60" height="60" typeName="OR">
              <position x="160" y="20" />
              <inputVariables>
                <variable formalParameter="IN1">
                  <connectionPointIn><relPosition x="0" y="20" /><connection refLocalId="1" ><position x="0" y="0" /><position x="0" y="0" /></connection></connectionPointIn>
                </variable>
                <variable formalParameter="IN2">
                  <connectionPointIn><relPosition x="0" y="40" /><connection refLocalId="2" ><position x="0" y="0" /><position x="0" y="0" /></connection></connectionPointIn>
                </variable>
              </inputVariables>
              <inOutVariables />
              <outputVariables>
                <variable formalParameter="OUT">
                  <connectionPointOut><relPosition x="60" y="20" /></connectionPointOut>
                </variable>
              </outputVariables>
            </block>
            <block localId="5" width="60" height="40" typeName="NOT">
              <position x="160" y="130" />
              <inputVariables>
                <variable formalParameter="IN">
                  <connectionPointIn><relPosition x="0" y="20" /><connection refLocalId="3" ><position x="0" y="0" /><position x="0" y="0" /></connection></connectionPointIn>
                </variable>
              </inputVariables>
              <inOutVariables />
              <outputVariables>
                <variable formalParameter="OUT">
                  <connectionPointOut><relPosition x="60" y="20" /></connectionPointOut>
                </variable>
              </outputVariables>
            </block>
            <block localId="6" width="60" height="60" typeName="AND">
              <position x="300" y="60" />
              <inputVariables>
                <variable formalParameter="IN1">
                  <connectionPointIn><relPosition x="0" y="20" /><connection refLocalId="4" formalParameter="OUT" ><position x="0" y="0" /><position x="0" y="0" /></connection></connectionPointIn>
                </variable>
                <variable formalParameter="IN2">
                  <connectionPointIn><relPosition x="0" y="40" /><connection refLocalId="5" formalParameter="OUT" ><position x="0" y="0" /><position x="0" y="0" /></connection></connectionPointIn>
                </variable>
              </inputVariables>
              <inOutVariables />
              <outputVariables>
                <variable formalParameter="OUT">
                  <connectionPointOut><relPosition x="60" y="20" /></connectionPointOut>
                </variable>
              </outputVariables>
            </block>
            <outVariable localId="7" height="20" width="80">
              <position x="440" y="80" />
              <connectionPointIn><relPosition x="0" y="10" /><connection refLocalId="6" formalParameter="OUT" ><position x="0" y="0" /><position x="0" y="0" /></connection></connectionPointIn>
              <expression>Run</expression>
            </outVariable>
          </FBD>
        </body>
      </pou>
    </pous>
  </types>
  <instances>
    <configurations>
      <configuration name="Config0">
        <resource name="Res0">
          <task name="tcyclic" interval="T#10ms" priority="0">
            <pouInstance name="inst0" typeName="drive" />
          </task>
        </resource>
      </configuration>
    </configurations>
  </instances>
</project>

Three blocks and four wires: Start and Run into an OR, Stop through a NOT, both into an AND, the result back to Run. FBD makes the data flow explicit where ladder makes the current path explicit. On a Boolean latch the two say the same thing; on an analog chain with filters and a PID, FBD is the readable one and ladder is not.

Instruction list¶

benchmarks/motor_control/il_seal_in/seal_in.il

(* seal_in: self-holding (seal-in) coil with stop.
   Instruction List rendering of ld_seal_in / g_seal_in.
   Deprecated in IEC 61131-3 edition 3.0 (2013) and removed in
   edition 4.0 (2025); kept here because deployed plants still run it.
   Run := (Start OR Run) AND NOT Stop *)
PROGRAM drive
  VAR_INPUT
    Start : BOOL;
    Stop  : BOOL;
  END_VAR
  VAR_OUTPUT
    Run : BOOL;
  END_VAR

      LD    Start
      OR    Run
      ANDN  Stop
      ST    Run
END_PROGRAM

An accumulator machine. Load Start, OR in Run, AND with the negation of Stop, store the result. Four instructions, each acting on one implicit register, in the order they are written.

Do not write new IL. Edition 4.0 removed it, and the committee's stated reason was that an assembler-like language is not up to date in a modern development environment. Read it, because plants commissioned in 1998 are still running it.

Sequential function chart, and why it is not here¶

SFC is the odd one, and the standard treats it that way: it structures a program rather than replacing the language inside it. You draw steps, the transitions between them, and the condition that fires each transition. The actions inside a step are written in one of the other languages.

A latch is the wrong example for SFC, because a latch is not a sequence. It is one Boolean relation that holds every scan. Writing it as a two-step chart would be a translation exercise rather than a design.

A tank cycle is the right one:

The double border on Idle marks the initial step. Each short horizontal bar is a transition, and the text beside it is the condition that has to hold for the chart to move on. Control leaves Draining and returns to Idle, which is the cycle. That program is in the catalog as sfc_batch_fill_drain. Use the notation the process has, not the one a suite wants to tick off.

The interchange format¶

Vendor project files are proprietary and mutually unreadable, which is why PLCopen TC6 defined an XML interchange format. A program becomes a <pou> holding an <interface> that declares the variables and a <body> holding exactly one language element: <LD>, <FBD>, <ST>, <SFC>, or <IL>.

For a graphical body that means every element carries an identity and its wiring:

<contact localId="10" negated="false" storage="none" edge="none">
  <position x="20" y="10"/>
  <connectionPointIn><connection refLocalId="0"/></connectionPointIn>
  <variable>Start</variable>
</contact>

Two <connection> elements inside one <connectionPointIn> is how a wired OR is written, and that is the seal-in junction drawn above.

Textual bodies are simpler: the source sits inside the element as text.

Every graphical program in this suite is PLCopen XML. The files carry a .ld extension while their content is XML, because the verifier keys its front end off the extension. Lesson 1 has the full file to read.

Which of these can ESBMC read?¶

One, directly.

Recorded 2026-08-28T18:37:09Z. Every build ran the same command.

cp benchmarks/motor_control/g_seal_in/program.xml benchmarks/motor_control/g_seal_in/program.ld
esbmc benchmarks/motor_control/g_seal_in/program.ld --ld-props benchmarks/motor_control/g_seal_in/props.yaml --k-induction --ld-scan-watchdog --ld-scan-budget 8 --timeout 30s

Recorded 2026-08-28T18:37:09Z.

master

cp benchmarks/motor_control/g_seal_in/program.xml benchmarks/motor_control/g_seal_in/program.ld
esbmc benchmarks/motor_control/g_seal_in/program.ld --ld-props benchmarks/motor_control/g_seal_in/props.yaml --k-induction --ld-scan-watchdog --ld-scan-budget 8 --timeout 30s

build	ESBMC	verdict	expected	outcome	ingestion gate	cpu
master	8.4.0 `0064c4ac`	`SAFE`	`SAFE`	correct	pass	0.016 s

master found its solution by the inductive step (k = 2).

What the front end encoded. The scan body as the solver receives it, branch guards kept. An assignment-only view hides the guards and makes a guarded accumulator read as a constant.

master

     1: IF !1 THEN GOTO 9
        ASSIGN Start=NONDET(_Bool);
        ASSIGN Stop=NONDET(_Bool);
        ASSIGN Run__prev=1 && Run;
        IF !1 THEN GOTO 2
        ASSIGN pf4=0;
     2: IF !(1 && Run__prev) THEN GOTO 3
        ASSIGN pf4=1;
     3: IF !1 THEN GOTO 4
        ASSIGN pf3=0;
     4: IF !(1 && Start) THEN GOTO 5
        ASSIGN pf3=1;
     5: IF !1 THEN GOTO 6
        ASSIGN pf5=0;
     6: IF !(1 && pf4 && !Stop) THEN GOTO 7
        ASSIGN pf5=1;
     7: IF !(1 && pf3 && !Stop) THEN GOTO 8
        ASSIGN pf5=1;
     8: ASSIGN Run=1 && pf5;
        GOTO 1
     9:

Recorded 2026-08-28T18:37:09Z. Every build ran the same command.

cp benchmarks/motor_control/fbd_seal_in/program.xml benchmarks/motor_control/fbd_seal_in/program.ld
esbmc benchmarks/motor_control/fbd_seal_in/program.ld --ld-props benchmarks/motor_control/fbd_seal_in/props.yaml --k-induction --ld-scan-watchdog --ld-scan-budget 8 --timeout 30s

Recorded 2026-08-28T18:37:09Z.

master

cp benchmarks/motor_control/fbd_seal_in/program.xml benchmarks/motor_control/fbd_seal_in/program.ld
esbmc benchmarks/motor_control/fbd_seal_in/program.ld --ld-props benchmarks/motor_control/fbd_seal_in/props.yaml --k-induction --ld-scan-watchdog --ld-scan-budget 8 --timeout 30s

build	ESBMC	verdict	expected	outcome	ingestion gate	cpu
master	8.4.0 `0064c4ac`	`error`	`SAFE`	error	fail	0.008 s

What the front end encoded. The scan body as the solver receives it, branch guards kept. An assignment-only view hides the guards and makes a guarded accumulator read as a constant.

master

Target: 64-bit little-endian aarch64-unknown-macos with esbmclibc
Parsing /Users/user/Claude/Overleaf Projects (2 items)/ESBMC-Benchmark-Suite (P6)/benchmarks/motor_control/fbd_seal_in/program.ld
ERROR: UnsupportedConstruct(FBD body of POU 'drive', tier=2)
ERROR: PARSING ERROR

Both report SUCCESSFUL. Only the first verified a seal-in: watch the ingestion gate on the second, which fails because ESBMC discards an <FBD> body without saying so. The textual ladder, the structured text and the instruction list are not shown with verdicts at all, because the front end XML-parses whatever file it is handed and none of those three is XML.

That is the direct route. A second route reaches every notation by translating through Structured Text and C, and it is described with its evidence and its costs on How ESBMC-PLC works. Twenty tasks in the catalog now carry a verdict from both.

What this suite covers today¶

language	tasks	variants
FBD	5	7
IL	3	3
LD-graphical	53	88
LD-textual	20	25
SFC	3	5
ST	33	58
total	117	186

Those counts are generated from the catalog when the site builds, so they cannot drift from it. FBD, SFC and IL entered the suite for language coverage, with expected verdicts established by construction rather than by a tool run, which is why they carry validation_status: candidate. The benchmarks catalog lists every task.