Cindy Eisner (IBM Haifa Research Laboratory)
Modern hardware designs are typically based on multiple clocks. While a singly-clocked design is easily described in standard temporal logics, describing a multiply-clocked design is cumbersome. In recent years there have been a number of attempts to define a temporal clock operator. Each of these attempts suffers at least one important weakness, and none gives a satisfactory solution in the case that the clocks are not well-behaved. This talk presents the problem of describing multiply-clocked hardware designs using temporal logic, and the simple problem (but alas, no solution) of describing cascaded flip-flops when the clocks are not well-behaved.