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 that you have read and understand our privacy policy and code of conduct.

Browse other questions tagged or ask your own question.