Multiplier correctness example

[vaishnavi08]

Hi, I'm new to coq and I am facing a few issues with understanding the code MultiplierCorrectness.v. I could understand till the lemma mul_to_partial_mul. I don't understand what the rest of the code does. @math-fehr It would be really helpful if I could get what are we trying to prove in lemmas enq_preserves_invariant, deq_preserves_invariant, step_preserves_result_invariant, step_preserves_result_finished_invariant. It would be really helpful for beginners like me if a few comments could be added giving the description of the lemma.

I am currently working on proving correctness of different modules of a processor based on riscv architecture. I would also like to start a discussion (if interested) as to how can we prove the functionality and timing correctness of different modules. For instance, I currently wrote a koika code for alu module of the processor. I was thinking how could the functionality correctness of this module could be proved with the help of coq (ie, what lemmas would be good to prove since its not a mathematical problem).

Any sort of idea or suggestion would be really helpful. Thank you :)

[math-fehr]

Hi! Sorry for the delay. I'm currently a bit busy, so here is the main idea.

We want to show that our multiplier state satisfy some invariants at each cycle:

• step_invariant asserts that the n_step variable is always less than the number of cycles required for the multiplication.
• finished_invariants asserts that the finished bit (which is 1 once the multiplication is done) cannot be set if valid (which is 1 when the multiplication is being computed) is not set.
• result_invariants asserts that if the multiplication is being computed, and that it is not finished, then the result bits contain the partial multiplication of our two operands.
• result_finished_invariants asserts that if the multiplication is finished, then the result bits contain the multiplication of the two operands.

Then, the lemmas you mentionned are used to prove that the invariants will hold for each cycle. For example, enq_preserves_invariant proves that after a enq rule, if the invariants held, then the invariants will still hold.
However, we need to be careful and make sure that the variables used inside the multiplier module were not previously written, otherwise the rule would not trigger.

For proving functional and timing correctness of modules, maybe @cpitclaudel or @threonorm would have some ideas. I haven't worked with koika for the last year, so I don't know what kind of progress has been made!