The mod operation is not supported when XLS_IR is converted to Z3. Is there a solution

[zhang0504]

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

UNIMPLEMENTED: Unhandled node for conversion from XLS IR to Z3:

Current best alternative workaround (limit 100 words)

I'll go crazy

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

I don't know.

[hzeller]

It is always good to include an example (e.g. DSLX code and the commands that you executed) to reproduce the issue.

[zhang0504]

It is always good to include an example (e.g. DSLX code and the commands that you executed) to reproduce the issue.

For example, there's an example： a % b //A modulates b

Then an error occurs during the conversion of xls_ir to Z3. This is the output after execution： UNIMPLEMENTED: Unhandled node for conversion from XLS IR to Z3

[ericastor]

The commands you were executing would be important, including a file that lets us reproduce the issue - as would the context.

Generally speaking, we expect users to run our optimizer before running certain tools. It would help us understand the issue if you can share more details as to what you're trying to do, how you're trying to do it, and if it's a nonstandard approach, the reason why you need to follow the approach you're taking!

[allight]

As far as we can tell our smtlib emitter fully supports umod and smod.

Manual tests indicate this all works:

allight@wenix ‹ main › : ~/xls
[0] % cat /tmp/mod.x
fn modtest(a: u64, b: u64, c: u64, d: s64, e: s64, f: s64) -> (u64, s64) {
  ((a + b) % c, (d * e) % f)
}

allight@wenix ‹ main › : ~/xls
[0] % bazel run //xls/dslx/ir_convert:ir_converter_main -- /tmp/mod.x --top=modtest > /tmp/mod.ir
Computing main repo mapping:
Loading:
Loading: 0 packages loaded
Analyzing: target //xls/dslx/ir_convert:ir_converter_main (0 packages loaded, 0 targets configured)
Analyzing: target //xls/dslx/ir_convert:ir_converter_main (0 packages loaded, 0 targets configured)
[0 / 1] [Prepa] BazelWorkspaceStatusAction stable-status.txt
INFO: Analyzed target //xls/dslx/ir_convert:ir_converter_main (0 packages loaded, 0 targets configured).
INFO: Found 1 target...
Target //xls/dslx/ir_convert:ir_converter_main up-to-date:
  bazel-bin/xls/dslx/ir_convert/ir_converter_main
INFO: Elapsed time: 0.271s, Critical Path: 0.00s
INFO: 1 process: 1 internal.
INFO: Build completed successfully, 1 total action
INFO: Running command line: bazel-bin/xls/dslx/ir_convert/ir_converter_main /tmp/mod.x '--top=modtest'

allight@wenix ‹ main › : ~/xls
[0] % cat /tmp/mod.ir
package mod

file_number 0 "/tmp/mod.x"

top fn __mod__modtest(a: bits[64] id=1, b: bits[64] id=2, c: bits[64] id=3, d: bits[64] id=4, e: bits[64] id=5, f: bits[64] id=6) -> (bits[64], bits[64]) {
  add.7: bits[64] = add(a, b, id=7, pos=[(0,1,6)])
  smul.9: bits[64] = smul(d, e, id=9, pos=[(0,1,19)])
  umod.8: bits[64] = umod(add.7, c, id=8, pos=[(0,1,11)])
  smod.10: bits[64] = smod(smul.9, f, id=10, pos=[(0,1,24)])
  ret tuple.11: (bits[64], bits[64]) = tuple(umod.8, smod.10, id=11, pos=[(0,1,2)])
}

allight@wenix ‹ main › : ~/xls
[1] % bazel run //xls/solvers:smtlib_emitter_main -- --ir_path=/tmp/mod.ir
INFO: Analyzed target //xls/solvers:smtlib_emitter_main (0 packages loaded, 0 targets configured).
INFO: Found 1 target...
Target //xls/solvers:smtlib_emitter_main up-to-date:
  bazel-bin/xls/solvers/smtlib_emitter_main
INFO: Elapsed time: 0.265s, Critical Path: 0.00s
INFO: 1 process: 1 internal.
INFO: Build completed successfully, 1 total action
INFO: Running command line: bazel-bin/xls/solvers/smtlib_emitter_main '--ir_path=/tmp/mod.ir'
(|(bits[64], bits[64])|
  (ite (= c #x0000000000000000) c (bvurem (bvadd a b) c))
  (ite (= f #x0000000000000000) f (bvsrem (bvmul d e) f)))

At a best guess I'd say you probably are trying to convert an IR with 'invoke' nodes present.

If this is the case then run them through //xls/tools:opt_main before the z3 conversion to inline everything.

If having our optimization pipeline go at them is undesired for some reason you can pass the flag --passes='pre-inlining inlining' --opt_level=0 like so:

allight@wenix ‹ main › : ~/xls
[0] % cat /tmp/mod.x
fn umod(a: u64, b: u64, c: u64) -> u64 {
  (a + b) % c
}
fn smod(d: s64, e: s64, f: s64) -> s64 {
  (d * e) % f
}
fn modtest(a: u64, b: u64, c: u64, d: s64, e: s64, f: s64) -> (u64, s64) {
  (umod(a, b, c), smod(d, e, f))
}

allight@wenix ‹ main › : ~/xls
[0] % bazel run //xls/dslx/ir_convert:ir_converter_main -- /tmp/mod.x --top=modtest > /tmp/mod.ir
Computing main repo mapping:
Loading:
Loading: 0 packages loaded
Analyzing: target //xls/dslx/ir_convert:ir_converter_main (0 packages loaded, 0 targets configured)
Analyzing: target //xls/dslx/ir_convert:ir_converter_main (0 packages loaded, 0 targets configured)
[0 / 1] [Prepa] BazelWorkspaceStatusAction stable-status.txt
INFO: Analyzed target //xls/dslx/ir_convert:ir_converter_main (0 packages loaded, 0 targets configured).
INFO: Found 1 target...
Target //xls/dslx/ir_convert:ir_converter_main up-to-date:
  bazel-bin/xls/dslx/ir_convert/ir_converter_main
INFO: Elapsed time: 0.263s, Critical Path: 0.00s
INFO: 1 process: 1 internal.
INFO: Build completed successfully, 1 total action
INFO: Running command line: bazel-bin/xls/dslx/ir_convert/ir_converter_main /tmp/mod.x '--top=modtest'

allight@wenix ‹ main › : ~/xls
[0] % cat /tmp/mod.ir
package mod

file_number 0 "/tmp/mod.x"

fn __mod__umod(a: bits[64] id=1, b: bits[64] id=2, c: bits[64] id=3) -> bits[64] {
  add.4: bits[64] = add(a, b, id=4, pos=[(0,1,5)])
  ret umod.5: bits[64] = umod(add.4, c, id=5, pos=[(0,1,10)])
}

fn __mod__smod(d: bits[64] id=6, e: bits[64] id=7, f: bits[64] id=8) -> bits[64] {
  smul.9: bits[64] = smul(d, e, id=9, pos=[(0,4,5)])
  ret smod.10: bits[64] = smod(smul.9, f, id=10, pos=[(0,4,10)])
}

top fn __mod__modtest(a: bits[64] id=11, b: bits[64] id=12, c: bits[64] id=13, d: bits[64] id=14, e: bits[64] id=15, f: bits[64] id=16) -> (bits[64], bits[64]) {
  invoke.17: bits[64] = invoke(a, b, c, to_apply=__mod__umod, id=17, pos=[(0,7,7)])
  invoke.18: bits[64] = invoke(d, e, f, to_apply=__mod__smod, id=18, pos=[(0,7,22)])
  ret tuple.19: (bits[64], bits[64]) = tuple(invoke.17, invoke.18, id=19, pos=[(0,7,2)])
}

allight@wenix ‹ main › : ~/xls
[0] % bazel run //xls/tools:opt_main -- --passes='pre-inlining inlining' --opt_level=0 /tmp/mod.ir > /tmp/mod.opt.ir
Computing main repo mapping:
Loading:
Loading: 0 packages loaded
Analyzing: target //xls/tools:opt_main (0 packages loaded, 0 targets configured)
Analyzing: target //xls/tools:opt_main (0 packages loaded, 0 targets configured)
[0 / 1] [Prepa] BazelWorkspaceStatusAction stable-status.txt
INFO: Analyzed target //xls/tools:opt_main (0 packages loaded, 0 targets configured).
INFO: Found 1 target...
Target //xls/tools:opt_main up-to-date:
  bazel-bin/xls/tools/opt_main
INFO: Elapsed time: 0.476s, Critical Path: 0.00s
INFO: 1 process: 1 internal.
INFO: Build completed successfully, 1 total action
INFO: Running command line: bazel-bin/xls/tools/opt_main '--passes=pre-inlining inlining' '--opt_level=0' /tmp/mod.ir

allight@wenix ‹ main › : ~/xls
[0] % cat /tmp/mod.opt.ir
package mod

file_number 0 "/tmp/mod.x"

fn __mod__umod(a: bits[64] id=1, b: bits[64] id=2, c: bits[64] id=3) -> bits[64] {
  add.4: bits[64] = add(a, b, id=4, pos=[(0,1,5)])
  ret umod.5: bits[64] = umod(add.4, c, id=5, pos=[(0,1,10)])
}

fn __mod__smod(d: bits[64] id=6, e: bits[64] id=7, f: bits[64] id=8) -> bits[64] {
  smul.9: bits[64] = smul(d, e, id=9, pos=[(0,4,5)])
  ret smod.10: bits[64] = smod(smul.9, f, id=10, pos=[(0,4,10)])
}

top fn __mod__modtest(a: bits[64] id=11, b: bits[64] id=12, c: bits[64] id=13, d: bits[64] id=14, e: bits[64] id=15, f: bits[64] id=16) -> (bits[64], bits[64]) {
  add.20: bits[64] = add(a, b, id=20, pos=[(0,1,5)])
  smul.22: bits[64] = smul(d, e, id=22, pos=[(0,4,5)])
  umod.21: bits[64] = umod(add.20, c, id=21, pos=[(0,1,10)])
  smod.23: bits[64] = smod(smul.22, f, id=23, pos=[(0,4,10)])
  ret tuple.19: (bits[64], bits[64]) = tuple(umod.21, smod.23, id=19, pos=[(0,7,2)])
}

allight@wenix ‹ main › : ~/xls
[0] % bazel run //xls/solvers:smtlib_emitter_main -- --ir_path=/tmp/mod.opt.ir
INFO: Analyzed target //xls/solvers:smtlib_emitter_main (0 packages loaded, 86 targets configured).
INFO: Found 1 target...
Target //xls/solvers:smtlib_emitter_main up-to-date:
  bazel-bin/xls/solvers/smtlib_emitter_main
INFO: Elapsed time: 0.576s, Critical Path: 0.03s
INFO: 1 process: 1 internal.
INFO: Build completed successfully, 1 total action
INFO: Running command line: bazel-bin/xls/solvers/smtlib_emitter_main '--ir_path=/tmp/mod.opt.ir'
(|(bits[64], bits[64])|
  (ite (= c #x0000000000000000) c (bvurem (bvadd a b) c))
  (ite (= f #x0000000000000000) f (bvsrem (bvmul d e) f)))

[zhang0504]

I have two questions: First of all, my commit is: 7198c00cf0dc9a55b79d9f3034a362b0b3741ba9. Is umod supported by later versions?

Second, does lec_main support umod?

[ericastor]

If that's the commit you're using, you're very nearly two years of frequent commits out of date - I'm not particularly inclined to go hunting to figure out whether umod was supported by our Z3 translator at that point, but it should be today, as @allight demonstrated above. And if I'm not mistaken, everything supported by the Z3 translator should be compatible with lec_main.

Also, it really would help if you'd share reproducible instructions for your troubles! If we can see what's going wrong (not just a statement that it isn't working), we might be able to help more precisely!

[zhang0504]

My purpose is to verify the consistency

The aa folder contains the following files:

aa.sh aa_ma_action.ir aa_ma_action_opt.ir aa_ma_action.netlist.v aa_ma_action.xml

The code in aa.sh is： ./bazel-bin/xls/tools/opt_main aa_ma_action.ir > aa_ma_action_opt.ir

cd ../xls ./bazel-bin/xls/tools/lec_main --ir_path=xls/aa_test/aa/aa_action_opt.ir --netlist_path=xls/aa_test/aa/aa_action.netlist.v --cell_lib_path=xls/shift_op_test/cmos_cells.lib --netlist_module_name=aa_ma_action --ports_mapping_file=xls/aa_test/aa/aa_action.xml

Open the terminal in the aa folder and run the following command: sh aa.sh And then it's an error：UNIMPLEMENTED: Unhandled node for conversion from XLS IR to Z3:

[ericastor]

Can you share the next line of the error? It might help if we knew which node was unhandled for conversion, since our local tests seem to confirm that umod is supported, at least at the current tip of tree for XLS.

Beyond that, we really can't do much more without a set of IR files that replicate the error you're experiencing. If you can please share either the files you're using, or a reduced reproduction that avoids anything you're trying to keep private, we can do more. Otherwise, there's no real way to see the error you're getting or test potential fixes.

[zhang0504]

The aa_ma_action.ir file contains the following code: fn _ZN7xxx_res14__xxx_mod_valueIN6xxx_dt17xxx_uint_internalILi4EEENS2_ILi6EEEEEjTT0(value: bits[4], members: bits[6]) -> bits[32] { literal.1561: bits[1] = literal(value=1, id=1561, pos=[(0,267,5)]) zero_ext.1558: bits[32] = zero_ext(value, new_bit_count=32, id=1558, pos=[(0,267,5)]) zero_ext.1557: bits[32] = zero_ext(members, new_bit_count=32, id=1557, pos=[(0,267,5)]) literal.1560: bits[1] = literal(value=1, id=1560) not.1562: bits[1] = not(literal.1561, id=1562, pos=[(0,267,5)]) not.1563: bits[1] = not(literal.1561, id=1563, pos=[(0,264,1)]) ret umod.1559: bits[32] = umod(zero_ext.1558, zero_ext.1557, id=1559, pos=[(0,267,5)]) }

The aa_ma_action_opt_ir file contains the following information: umod.5880: bits[32] = umod(concat.5878, concat.5879, id=5880, pos=[(0,267,5)]) bit_slice.1568: bits[4] = bit_slice(umod.5880, start=0, width=4, id=1568, pos=[(0,110,5)])

The output error of the command is as follows: UNIMPLEMENTED: Unhandled node for conversion from XLS IR to Z3: umod.5880: bits[32] = umod(concat.5878, concat.5879, id=5880, pos=[(0,267,5)])

[allight]

You need to update your xls build to a more recent one.

That error message is from the z3_ir_translator.cc and at some point between that 2 year old commit and now the mod operations were added to that file. Looking at blame it seems the operation was added about 16 months ago when the mod is was added to dslx (in commit https://github.com/google/xls/commit/e2a9129febabdf64360cc0d2a1abcd51edb230eb).

[zhang0504]

Okay, thank you guys,

I'll use the latest code to verify

[zhang0504]

During the compilation process, I encountered a new issue: due to the lack of support for accessing dl.google.com So fetch https://dl.google.com/go/go1.20.linux-amd64.tar.gz Failed This process may take several hours So, what methods do I have to change it to local or other ways