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

Dev/mac op #15

Closed dwRchyngqxs closed 1 year ago

dwRchyngqxs commented 2 years ago

Merging (a = mul y z; b = add x a) into (b = MAC x y z) on GiblePar basic blocs (after scheduling) whenever (a) is not read elsewhere in the basic bloc.

dwRchyngqxs commented 1 year ago

This branch / pull request is orphaned. I won't work on it anymore.

ymherklotz commented 1 year ago

Thanks, will merge it anyways to develop further later on.