Verilog Hardware Description Language

The material here consists of relics from an ancient EPSRC project by David Greaves and Mike Gordon entitled Checking Equivalence Between Synthesised Logic and Non-Synthesisable Behavioural Prototypes.

Revised version of a paper entitled The Semantic Challenge of Verilog HDL that accompanied an invited talk given at the Tenth Annual IEEE Symposium on Logic in Computer Science (LICS'95), June 26-29, 1995, San Diego, California.
Relating event and trace semantics of Hardware Description Languages, The Computer Journal, vol. 45, No. 1, 2002.
An expository talk on the Verilog semantics entitled Event, Trace and Cycle Semantics of Hardware Description Languages.
Another talk is entitled Unified View of Hardware and Software for Systems-On-a-Chip. A version of this with a different emphasis is Program Verification and Hardware Synthesis.
The paper Language Independent RTL Semantics, jointly authored with Abhijit Ghosh of Synopsys, was originally written as an invited contribution to the 1998 IEEE CS Annual Workshop on VLSI: System Level Design in Orlando Florida. However, due to flights being completely full during "spring break", I failed to get a ticket and so, alas, was not able to present it!
The representation of state machines in higher order logic is discussed in a short tutorial note and the Prosper deliverable D2.1c.
Miscellaneous fragments and drafts: Banff99Paper.ps, HDLpaper.ps, SV0.ps, SV1.ps, GhoshGordon.ps, SV.ps.gz