Open vaishnavi08 opened 3 years ago
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!
Hi, I'm new to coq and I am facing a few issues with understanding the code
MultiplierCorrectness.v
. I could understand till the lemmamul_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 lemmasenq_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 akoika
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 :)