Improving Formal Verification for IR

### What's hard to do? (limit 100 words)

Making the generated Z3 code independent and provable standalone. There are three things I would like to address:

1. The assertion node is unhandled while converting an IR to Z3.
2. Function parameters also do not show up in the Z3 code while converting an IR to Z3
3. Can the "**#test**" part of the DSLX code be used to generate an equivalent testbench in System Verilog?


### Current best alternative workaround (limit 100 words)

The second point of adding the function parameters to the Z3 can be easy, as the function signature is already present in the Package class but is not public and cannot be accessible from the "smtlib_emitter_main". For point 1, we need to modify the parser to handle the assertion node and convert it to equivalent Z3 code. For each line of the IR, we have an equivalent Z3 code that needs to be addressed. However, I am still not sure how to address point 3.

### Your view of the "best case XLS enhancement" (limit 100 words)

We can independently verify the IR without performing logical equivalence checking with the above advancements. Secondly, if the "#test" block can be converted to System Verilog in the same manner, then we can quickly verify the generated Verilog code via simulating.

### See also

#1344
#1537