Improving Formal Verification for IR

[dassbrothers]

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

[proppy]

@dassbrothers was asking for a few pointers:

how to get the Function params name:

• https://github.com/google/xls/blob/aa165490129cdb522c13d2369f9b8aabb32e2cbe/xls/ir/function_base.h#L84
• https://github.com/google/xls/blob/aa165490129cdb522c13d2369f9b8aabb32e2cbe/xls/ir/nodes.h#L724

how params are translated to z3

• https://github.com/google/xls/blob/aa165490129cdb522c13d2369f9b8aabb32e2cbe/xls/solvers/z3_ir_translator.cc#L644-L669

assert IR semantic

• https://google.github.io/xls/ir_semantics/#assert
• https://github.com/google/xls/blob/aa165490129cdb522c13d2369f9b8aabb32e2cbe/xls/ir/nodes.h#L172

[allight]

So it seems like it would be somewhat helpful to get some more details about what exactly you think a good result would be.

Reading this and your other bugs I assume you'd like a few different things

Z3 Improvements - input declarations

Currently if you have some function like

fn muladd(a: u8, b: u8, c: u8) -> u8 { (a * b) + c }

you'll get a z3 program like

(bvadd ((_ extract 7 0) (bvmul ((_ zero_extend 1) a) ((_ zero_extend 1) b))) c)

It sounds like for (2) you would want instead it to print something like

(declare-const a (_ BitVec 8))
(declare-const b (_ BitVec 8))
(declare-const c (_ BitVec 8))
(bvadd ((_ extract 7 0) (bvmul ((_ zero_extend 1) a) ((_ zero_extend 1) b))) c)

This seems easy enough to do but seems like it would cause problems with anything that wants to read in the emitter output directly.

z3 improvement - assert node

The (1) would make this problem even worse since presumably you want any assert! (and #[test]?) turned into smtlib asserts to check satisfiability.

So if you have a function like

fn muladd(a: u8, b: u8, c: u8) -> u8 { 
  assert!(a != u8:42, "lucky number")
  (a * b) + c 
}

#[test]
fn muladd_test() {
  assert_eq!(muladd(u8:1, u8:1, u8: 1), u8:2);
}

It would generate a z3 like

(declare-const a (_ BitVec 8))
(declare-const b (_ BitVec 8))
(declare-const c (_ BitVec 8))
(declare-const RESULT (_ BitVec 8))

; muladd definition
(assert (not (= a #x2a)))
(assert (= RESULT (bvadd ((_ extract 7 0) (bvmul ((_ zero_extend 1) a) ((_ zero_extend 1) b))) c)))

; muladd_test
(assert (implies (and (= a #x01) (= b #x 01) (= c #x01)) 
                 (= RESULT #x02))

Is this basically correct?

[dassbrothers]

Yes, @allight, you are correct. If we alter the current Z3 output, we cannot directly read the output. Ideally, in hardware verification, if we have some modules (assuming them as functions in DSLX), we would like to validate them against a set of properties specified in the design spec. Instead of performing a logical equivalence check, I would like to do that formally, guaranteeing that the module is expected to work correctly in all conditions, irrespective of the inputs. The assets within the functions should be treated as constraints or assumed, and the assets within the #[test] part must be validated.

Now, there may be some gaps or corner cases of writing properties from design specs, and some properties may be covered. So all this comes under coverage management, indicating which properties failed and which passed. So, I am trying to build a framework that could formally verify the IR generated from the DLSX code and hence, the final verilog output as well.