Add Verilib folder

[Kukovec]

• Source code modifications highlighted and justified
• Proof cheats (assume(false), sorry, etc.) highlighted and justified

closes #741

[sergiubur]

When we make change to code, how will change in code-line be caught up ? Does it need to ?

[Kukovec]

When we make change to code, how will change in code-line be caught up ? Does it need to ?

The validation status only references the function name. On remote, the code gets re-atomized, which updates the line numbers. The next step is to add automatic verilib-cli reclone to the CI (I've already added VERRILIB_CLI_AUTH_KEY as an org-level secret for this), but the CLI is still one or two steps away from being ready for this.

[astefano]

i was also thinking that if we don't want to use verilib-cli, we should be able to use github artifacts instead of committing .verilib. And if we're fine with validating all specs, we don't need to do anything locally so we don't need to commit .verilib.
An example of a workflow is https://github.com/Beneficial-AI-Foundation/dalek-lite/pull/665/changes. It reuses Beneficial-AI-Foundation/verilib-cli#5.

[sergiubur]

or, CLI can be transparent. problem is that new line numbers will need to be pushed after atomization to git, and I dont see from what account that would come. so, maybe deploy action would be easier, since its maybe more permissive (?)

[astefano]

or, CLI can be transparent. problem is that new line numbers will need to be pushed after atomization to git, and I dont see from what account that would come. so, maybe deploy action would be easier, since its maybe more permissive (?)

we'll look into it. when we have a better solution, we can just as well rm .verilib from git.

[sergiubur]

actually, verilib does not need to push us line numbers. it could simply store on their server

[Kukovec]

Yeah, we can remove all of this later, I just need it for now so I can set up the persistent Verilib image for tomorrow.