Adding Formal Verification for IR

[dassbrothers]

The Google XLS document says designs are converted from DSLX --> IR --> Optimized IR --> Codegen --> Verilog. Moreover, to verify an IR, it is converted to Z3, another equivalent Z3 implementation is done, and the outputs are checked for equivalence. This is provided in the link: https://google.github.io/xls/solvers/. However, to convert an IR to Z3, the tool makes use of the smtlib_emitter_main (as provided in https://google.github.io/xls/solvers/), which again outputs the key functionality of the function that it covers.

Since Z3 is a powerful engine for problem-solving, we can use Z3 standalone to verify the design. As provided in smtlib_emitter_main the command
bazel run -c opt //xls/tools:smtlib_emitter_main -- --ir_path $PWD/bazel-bin/xls/examples/tiny_adder.opt.ir
is used to convert an IR function to Z3. However, the output only captures the functionality (bvadd (concat #b0 x) (concat #b0 y)).

I feel three enhancements can be made. The following are listed below:

1. The assertions in the DSLX get converted into IR, but it throws an error when I convert the IR into the Z3 equivalent. For example, if I convert the example given in xls/examples/assertions/assertions.x, it gets converted into IR and Optimized IR, but I cannot generate its equivalent Z3. This is because the assertion node is unhandled. The screenshot for the same is given below:

2. Moreover, considering the output of the "smtlib_emitter_main," it also does not consider the function parameters. We can add the function parameters as they are already available in the Package class, where functions output function parameters and function bodies, but they are not public. [(ParseFunctionSignature, ParseBody, … ) present inside xls/ir/ir_parser.h]

3. The DSLX code comes with a code block where there is #[test] that serves the purpose of checking the functionality of the DSLX code. Can the #[test] part be converted to a testbench?

@proppy : Can you please check this once? This is what we have discussed in our monthly meetings.

[proppy]

@dassbrothers that sounds fine, would you mind filing an enhancement proposal for those solver improvement using this template ?

Note: part of that discussion was also captured in #1344.

[dassbrothers]

@proppy I have added the above discussion as an enhancement proposal. Issue id : #1549