Beta Release

This release updates the SecVerilog codebase to reflect the type system as described in this paper: https://ieeexplore.ieee.org/abstract/document/8060290

There are a few additional features, as well as a few missing components of the typechecker, which are documented below:

• Wellformedness of labels. SecVerilog requires that all of the labels of dependent variables in a label must flow to that label (see https://dl.acm.org/doi/abs/10.1145/2775054.2694372). This is not checked at the moment but could easily be inferred by JOIN-ing the labels of all dependent variables with the top level label written by the user.
• Definite Assignment. If a registered (seq) value has a dependent label, then we must assign to it on all possible execution paths, to check that, on any path, its new label is not lower than its old label (even when keeping the value the same). This is not enforced by the compiler right now.
• Seq vs. Comb identification - The seq and com tags are used to tell secverilog whether or not the value is a simple wire or a registered value that gets updated on a clock edge. These tags are not checked for their accuracy (i.e., whether or not something tagged as seq is only updated with non-blocking assignment in clocked events, and whether or not com registers are only updated with non-blocking assignments).
• We also support quantified labels which can be used to label different elements of arrays based on their index; currently we only infer information about indices when those indices are realized as constants or variables (so array accesses with complex expressions will throw an error if they use this quantified type). Furthermore, for any index variables, we will infer fairly precise values for them (for typechecking purposes) as long as they are wires or they are used in other dependent label expressions.