Most papers that I have seen on proving digital logic focus only on the combinational circuits (ie using boolean logic). But real life circuits also have flip-flops, ie a time element an a clock. How to model such time and clocks in theorem provers, eg in hol or coq?
(as a very simple example) how do I model a modulo-10 counter and prove that value=11 will never be reached?
Can you please point me to some such papers, and possibly with code that I can run?
