Glynn Winskel
A grouping.
Glynn Winskel, at the Cambridge Computer Laboratory. Three records, all from 1986-88, all on the same problem, and all held in full because he keeps them openly on his own page -- which is why the corpus can show this line at all when the Kluwer and Springer volumes carrying it are closed.
Read them in this order.
The Marktoberdorf lectures (1987) are the motivation and the survey, and the most readable statement in the corpus of why any of this matters: "verification of any device can only be done in terms of a model for its behaviour. However it is very easy to forget that verification depends crucially on the accuracy of the model." Their diagnosis is specific -- designers reason neither in volts nor in booleans but in crude discrete notions of strength and of information flow, and no formal model supported that.
"A compositional model of MOS circuits" (1988) is the model itself. Its objection to Bryant is not inaccuracy but structure: Bryant's model is the most accurate anyone had and is "not compositional", so a circuit's behaviour cannot be determined from its parts' -- fine for a simulator, fatal for a structured proof.
"Relating two models of hardware" (1987) then takes that model and Gordon's two-valued relational one and, by an adjunction between the associated partial-order categories, derives conditions under which assertions proved in the simpler model hold in the more accurate one. The machinery is borrowed from abstract interpretation. Its closing worry is that those conditions "are generally expressed in terms of the more complicated model", so the licence to reason cheaply must be earned expensively -- which is the problem melham1990formalizing answers a year later by discharging it once per circuit design style.
What ties the three together, and what makes Winskel the corpus's most useful single author on this subject, is that he is the only one who treats the choice of model as itself a formal object. Everyone else in the-switch-or-the-curve picks a level and argues for it. He relates levels and asks what the relation guarantees.
All three restrict attention to static behaviour -- steady states, ignoring oscillation and changing inputs -- and say so plainly. That boundary is where fugger2016unfaithful, marino1981general and yan2012oscillator take over.