Definition

The Chain Constraint is a formal guidance constraint used by EPEX when generating multi-instruction equivalent program sequences ( \hat{P}_i^j ). It is formalized in the EPEX paper as:

Definition 2 (Chain Constraint).

$$has_result(current_instr_p) \rightarrow (rs1_{p+1} = rd_p \vee rs2_{p+1} = rd_p)$$

Purpose

When EPEX's formal search generates an instruction sequence rather than a single instruction, the chain constraint guides the search to produce sequences whose instructions build on each other's results. Without such guidance, a naive search over instruction sequences would still admit large numbers of "uninteresting" variants (such as de-facto NOPs) that the Effect Constraint alone is insufficient to suppress.

Mechanism

The constraint is indexed by the instruction position ( p ) within the generated sequence ( P_i^j ). It states that:

• If the current instruction at position ( p ) produces a result (i.e., has_result(current_instr_p) holds — relevant for instructions like ALU operations but excluding branches, which have no destination register),
• Then the next instruction at position ( p+1 ) must use that result: at least one of its source operands (rs1_{p+1} or rs2_{p+1}) must equal the destination register rd_p of the preceding instruction.

This effectively chains the instructions together by relating the register variables across the sequence, ensuring data-flow continuity.

Role within EPEX

The chain constraint is one of two essential constraints used to guide EPEX's formal search toward interesting programs, alongside the Effect Constraint. Together, these constraints are applied when generating multi-instruction equivalent programs that are pushed into the instruction queues feeding the two processor instances ( I_1 ) and ( I_2 ), enabling later architectural-state comparison against the reference ISS.

Formal Context

The constraint is expressed within the formal ISA model developed for EPEX and is applied by the EPEX library as part of the generation step for ( \hat{P}_i^j ) — the sequence equivalent to the original instruction ( P_i ) that activates different control and/or data paths of the processor under test.