A Semantics for Verilog using Duration Calculus

摘要

This paper presents a denotational semantics for the hard-ware description language Verilog using Duration Calculus. The language contains interesting features such as event-driven process, shared-variable concurrency and simulator-based description. We examine algebraic properties of Verilog, which can be used in support of program simplification and optimisation. To covert programs to normal form, we enrich the language with guarded choice and composite guard.