The Definition of a Temporal Clock Operator

Modern hardware designs are typically based on multiple clocks. While a singly-clocked hardware design is easily described in standard temporal logics, describing a multiply-clocked design is cumbersome. Thus it is desirable to have an easier way to formulate properties related to clocks in a temporal logic. We present a relatively simple solution built on top of the traditional LTL-based semantics, study the properties of the resulting logic, and compare it with previous solutions.

15^th ICALP