Symbolic Validator

The first of Neo's interpreters is a symbolic execution engine powered by Z3. It executes over each module and type declaration, performing various correctness checks. Should these checks pass, it is guaranteed that any instantiation of the module or type will be successful (if that's not the case, report a bug!). All checks report helpful errors and include the line that caused the error. They can also be displayed in-editor as you type.

At a high level, the process is quite simple. Any parameters are instantiated with symbolic values in Z3, and then the body of the module or type is executed. Any operations that could be invalid are checked either statically or symbolically through Z3 to ensure there is no possible combination of input parameters that would cause generated hardware to be invalid. Each module and type is validated independently and only depends on the signature of other modules/types, ensuring the solver's performance scales linearly with the codebase.

Supported checks

Type Matching

All operators, function calls, and assignments are strictly type-checked. This includes ensuring that instances of parameterized types have the same type parameters.

Timing Matching

TODO

Single Assignment

Neo ensures that each logic value is only assigned once in your design, including preventing assignments to constant or constructed values. This includes checking for unnasigned wires and conditionals that don't have the same set of assignments in each branch. These checks ensure you'll never have to debug zs or xs in your design.

Array Bounds

All array indexes are ensured to be within bounds. This also applies to arrays that have a parameterized length and/or parameterized indexing.

Bit Select Bounds

Any bit selections are ensured to be within the bounds of the base value.

Minor Checks

Simple things such as syntax errors, duplicate names, invalid fields, etc... are also checked to mitigate simple mistakes.