The Sail-to-SystemVerilog translator cannot handle `undefined`.

[yutakang]

Hi @Alasdair ,

I noticed the Sail-to-SystemVerilog translator encounters difficulties with certain elements. Specifically, it cannot translate undefined.

Below is a minimal Sail code example that reproduces this limitation:

$include <prelude.sail>
val execute: bits(1) -> unit
function execute arg = {
  hehe:bits(1) = undefined;
  ()
}

The translator showed messages such as "Cannot translate literal to SMT" and "Please report this as an issue on GitHub". I hope this message is helpful.

[Alasdair]

Yes, the systemverilog translation is currently a work in progress, and there a quite a few features it doesn't support yet. You might be able to use the --undefined-gen option to replace the undefined literals with function calls that can be implemented in systemverilog.

[yutakang]

Hi @Alasdair, thank you for the very quick response.

I managed to produce the relevant SystemVerilog code using the -undefined_gen option you referred to. I hope I can overcome this problem by implementing an appropriate sail_undefined_bitvector function.