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?



Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge you have read our privacy policy.

Browse other questions tagged or ask your own question.