A Specification Is a Testable State Machine

This checkpoint connects the ideas already established about SLEIGH constructors, p-code semantics, and GenSYS’s symbolic traversal. The subject is still the processor specification, but the focus now is the boundary between reaching a represented decode path and validating the behavior that path claims to describe. The practical judgment is simple to state and easy to lose: a generated instruction is valuable evidence, but only if its scope is made explicit.

A SLEIGH specification is a state machine in two related senses. Its constructors move a decoder through choices based on instruction bits and context. Its selected semantic sections then move an architectural state through p-code operations. InSPECtor can explore the first machine systematically and prepare cases for the second. Trust grows only when those two forms of state are connected without treating either one as a substitute for the other.

A generated instruction is a chain of obligations

Start with a single instruction form rather than with a whole architecture. The specification receives instruction bits and an initial decoder context. A root constructor constrains part of the encoding and may select a subtable. That subtable resolves an operand, an immediate, a prefix phase, or another part of the instruction. Each choice adds conditions to the path. Some conditions fix bits immediately; others remain relationships to be solved later. Decode actions can alter context so that the next choice is evaluated under a state produced by the path itself.

GenSYS follows that chain. If a field must equal a constant, it can record the corresponding bit values and reject an immediate contradiction. If two fields must be equal, or if a later condition depends on an expression derived from earlier bits, it preserves the relationship instead of choosing prematurely. When all required constructor choices have been considered, the solver searches for a concrete instruction encoding satisfying the combined conditions, including the exclusions implied by overlapping constructors and invalid values ruled out by attachments.

The output is therefore more informative than a byte string. It is a byte string associated with a particular constructor path, a decoder-context history, and a set of constraints that explain why the specification should decode it in that way. If the path includes a subtable that returns a memory reference, the resulting semantic section can use that reference for a load or store. If a prefix changes the decoding phase, the encoding includes the bytes and context transition needed to reach the later interpretation. The case is a concrete witness for the specification’s structural claim.

The next transformation is semantic. The selected constructors produce p-code, and the p-code sequence names the reads, writes, branches, and intermediate values that the model attributes to the instruction. An addition may have separate operations for its result and flags. A memory instruction may read through a decoded address. A width-specific operation may write only part of a register representation. The generated encoding and its p-code path belong together: testing one without understanding the other would leave a gap between what the decoder selected and what the model says that selection does.

flowchart LR A[Instruction bits and initial context] --> B[Constructor path] B --> C[Fixed constraints] B --> D[Deferred relationships] C --> E[Decode actions and subtables] D --> E E --> F[Overlap and attachment exclusions] F --> G[SMT-satisfied encoding] G --> H[Selected p-code semantics] H --> I[Structural test case with a semantic path]