search

ymherklotz / vericert

A formally verified high-level synthesis tool based on CompCert and written in Coq.
https://vericert.ymhg.org
GNU General Public License v3.0
86 stars 5 forks source link

Optimise division implementation #10

Open ymherklotz opened 3 years ago

ymherklotz commented 3 years ago

Currently, the division algorithm heavily influences the frequency at which the design can run. Instead of using the division operator, it should therefore be possible to use a specialised division module, which should also be proven correct separately.

Instead, a division function in C can be used for now to go around that.