We formalise the semantics of V~-, a simple version of Verilog hardware description language using an extension of Duration Calculus. The language is simple enough for experimenting formalisation, but contains sufficient features for being practically relevant. V~- programs can exhibit a rich variety of computations, and it is therefore necessary to extend Duration Calculus with several features, including Weakly Monotonic Time, infinite intervals and fixed point operators. The semantics is compositional and can be used as the formal basis of a formal theory of Verilog.
展开▼
