CSU-CS-Melange / AlphaZ

MIT License
2 stars 1 forks source link

Verification codegen does not work with external functions #1

Closed lnarmour closed 1 year ago

lnarmour commented 1 year ago

It's possible to use external function definitions in alphabets files. The alphabets (.ab) file contains a declaration of the headers (needed by codegen). If the header (.h) file does not exist, codegen creates it. Then, the user is supposed to put in the function definitions.

right now, both of the main and verify makefile targets include the definitions when they shouldn't. We would need to make sure the external function definitions don’t get pulled in twice during the verification build. We can probably use a check like “#ifndef VERIFY” since that is what get passed during the verification build.