Derived, not checked

A subject the papers are about. The loosest grouping, and the one to reach for last.

Verification asks whether a circuit that exists is correct. This set collects the works that refuse the question and build the circuit out of the proof instead, so that correctness is a property of how it was made rather than something established afterwards. Membership requires the derivation to be the contribution -- a paper that verifies a synthesised design belongs elsewhere.

**The date keeps moving earlier, and that is the first thing this set records.** The corpus spent months treating 1991 as the moment the idea was named, on the strength of basin1991formally and fourman1991formal, which appeared in the same year. Both are later than everything else here.

1983 gordon1983proving a hard-wired controller derived from a microprogram by machine-checked inference, in Appendix 2 1983 snepscheut1983trace a method of deriving semiconductor chips from programs, as the closing chapter of a thesis 1985 martin1985delayinsensitive a fair arbiter described as a communicating process and compiled into a circuit 1986 martin1986compiling the method stated in general: semantics-preserving transformation from CSP-like programs 1989 ebergen1989translating syntax-directed translation, element count proportional to program length 1991 basin1991formally, fourman1991formal 1993 martin1993tomorrows the method applied to the first asynchronous microprocessor, functional on first silicon

**What the members share.** The verification burden is moved onto a program, where it is cheap, and the transformation is required to preserve semantics so that whatever was proved of the program holds of the circuit. martin1986compiling states it most directly: "the circuit obtained is correct by construction: all semantic properties that can be proved of the program hold for the circuit as well". Nothing is checked of the circuit afterwards, because on this account nothing needs to be.

**Two things worth noticing that no single member says.**

First, **the strongest demonstration in the set is of a liveness property, not a functional one.** martin1985delayinsensitive carries *fairness* across the transformations -- a pending request is granted after finitely many others -- and uses that to settle an open question that had been conjectured the other way. Deriving functional correctness is the usual claim; deriving fairness is harder and is the better advertisement.

Second, **the two traditions here were in contact, and the corpus can show it.** ebergen1989translating names Martin's technique in its introduction and says the two exhibit a similarity; its preface records that Rem sent Ebergen to Caltech in early 1982 for Chuck Seitz's course. So Eindhoven and Pasadena are one conversation. What differs is the vehicle: Martin compiles CSP-like programs by transformation, Ebergen translates a program syntax into a fixed set of basic elements, and snepscheut1983trace supplies the trace-structure formalism both rest on.

**The honest limit, stated by a member.** martin1986compiling says of its own central word: "At the moment, the term compiling means a systematic, semantics-preserving transformation. The ultimate goal of the transformation being carried out automatically has not yet been achieved." In 1985 this was a discipline performed by hand. martin1993tomorrows reports five people working part-time for under five months to derive a 20,000-transistor processor that worked on first silicon -- which is the strongest evidence in the set that the discipline scaled, and also a measure of what it cost.

**One member does both, and it is the newest.** alsayeg2010synthese synthesises QDI sequential controllers by direct mapping -- construction, as every other member here -- and then formally verifies the result in PSL with the RAT tool and proves it functionally correct. That is the school declining to rely on its own derivation, in a property language borrowed from the synchronous assertion-based world. It is the one place in this set where the argument above is not accepted by a practitioner of it.

**The clearest statement of why this set exists comes from a TIMA thesis acquired on 2026-09-17, and it is an argument from intractability rather than from elegance.** bregier2007synthese observes that quasi delay insensitivity is "une propriete complexe, qu'il est tres difficile de verifier: determiner si un circuit est quasi insensible aux delais ou non est un probleme a part entiere, qu'on ne sait generalement pas resoudre simplement". Deciding the property of a finished circuit is an open problem; so he proves instead that the synthesis flow necessarily produces QDI circuits under stated conditions on the model. **Derivation is chosen here not because checking is wasteful but because checking is not available.** That is a stronger warrant than this set usually gets, and it sits pointedly next to alsayeg2010synthese, three years later and from the same laboratory, which synthesises by construction and then checks anyway.

It also supplies the set's sharpest limitation, stated by the author about his own method. "Les possibles transformations du circuit apres la synthese peuvent compromettre la quasi insensibilite aux delais du circuit." **A correctness-by-construction guarantee ends where the construction ends**, and every downstream tool is a place to lose it -- the failure this corpus watches in bozga2002verification, bouesse2005dpa and sarma2024maskedhls. His answer is the honest and expensive one: forbid the transformations, permitting only gate fusion, and move optimisation upstream of synthesis onto a decision-graph model whose optimised form is still a member of the same class, so the proof still applies. A set about building circuits out of proofs should record that the price of the method is paid in what you may afterwards do to the circuit.

**Its companion one level up, added 2026-09-18.** cheng2023seer puts the HLS *source* program in an e-graph and orchestrates MLIR software passes together with ROVER's datapath rewriting inside it, so no ordering of transformations has to be committed to -- their name for the difficulty, **the phase-ordering problem**, is worth adopting: transformations interact, and for hardware a chosen order fixes timing and area at once. Correctness is again a chain of single-rewrite equivalence checks, generated through egg proof production as SystemC and discharged by a commercial checker. **So this set now holds the same derive-and-certify pattern at two levels of one toolchain**, with reported results up to 38x performance within 1.4x area, average 2.9x, and an Intel case study said to outperform hand-optimised designs.

**And a member from inside Intel, where the certificate is the product.** coward2024rover rewrites datapath RTL over an e-graph using rules "inspired by designers at Intel", then ships the optimised RTL **together with a re-runnable proof certificate**: because a commercial equivalence checker sometimes "returns an inconclusive result" on the whole transformation, ROVER extracts a chain of intermediate designs "differing by a single local rewrite at each step" -- "hundreds of intermediate steps" -- and has the checker prove each adjacent pair. **The engine is a product nobody can modify, so the input was changed instead**, which is this corpus's recurring finding in its purest form. Its premise is an admission worth quoting: "commercial logic and high-level synthesis tools are unable to match human designs", which is why manual RTL optimisation persists. **One caveat belongs on the set's own terms:** the rewrite *applications* are certified pair by pair, but the rewrite *conditions* "rel[y] upon an unproven extrapolation assumption", which the authors hope to discharge with ACL2. **Certified transformations are not certified transformation rules.**

**A 2026 member where the object without a specification is the tool, not the circuit.** tanaka2026relational derives the optimised form of a high-level-synthesis program from the naive one by a relational Hoare logic judgement, with a theorem that source and target simulate each other -- correctness as a property of the derivation, which is this set's rule exactly. Its motivating fact belongs in the corpus generally: two C programs computing the same thing, one indexing upward and one downward, synthesise to hardware differing **more than fivefold in speed**, because the commercial tool recognises the burst-transfer pattern in one and not the other. The authors' complaint is that such tools' "optimization strategies lack transparency" and have no "formal specification of the underlying program transformations". **So the derivation here is built to persuade an unspecified compiler to do its job** -- and the proof covers the transformation, not the synthesis step that follows it. They also state, to their credit, that the implementation restricts index patterns in ways the formalisation does not, so the theorem is more general than the tool.

Overlaps proved-here-used-there, which asks whether a claim travels between two descriptions; here the claim does not have to travel, because there is only ever one description being transformed.