cover fails in output port

[Topi-ab]

Description
The same cover between signal and port behave differently. Test file with out port "a" and signal "b". Both have identical cover.

Using image: hdlc/formal:all

SBY 13:37:55 [test_cover] summary: engine_0 (smtbmc) returned pass
SBY 13:37:55 [test_cover] summary: cover trace: test_cover/engine_0/trace0.vcd
SBY 13:37:55 [test_cover] summary: reached cover statement test.cover_a at in step 0
SBY 13:37:55 [test_cover] summary: cover trace: test_cover/engine_0/trace1.vcd
SBY 13:37:55 [test_cover] summary: reached cover statement test.cover_b at in step 12

Expected behaviour
cover_a and cover_b results should be identical.

How to reproduce?

library ieee;
use ieee.std_logic_1164.all;
use ieee.numeric_std.all;

entity test is
	port(
		clk_in: in std_logic;
		a: out std_logic
	);
end;

architecture formal of test is
	signal b: std_logic;
begin
	default clock is rising_edge(clk_in);
	
	cover_a: cover {a[*13]};
	cover_b: cover {b[*13]};
end;

[tasks]
bmc
cover

[options]
bmc: mode bmc
bmc: depth 50
cover: mode cover
cover: depth 50

[engines]
bmc: smtbmc
cover: smtbmc

[script]
ghdl --std=08 test.vhdl -e test
prep -top test

[files]
test.vhdl

sby --yosys "yosys -m ghdl" -f test.sby cover

NOTE: :file: and :image: identifiers are specific to issue-runner. We suggest to use these, since it allows continuous integration workflows to automatically test the MWE. Using ghdl/ghdl:* docker images to run the MWEs ensures that the latest available GHDL is used.

NOTE: Large files can be uploaded one-by-one or in a tarball/zipfile.

Context
Please, provide the following information:

• OS:
• Origin:
  • Package manager: version
  • Released binaries: tarball_url
  • Built from sources: commit SHA

If a GHDL Bug occurred block is shown in the log, please paste it here:

******************** GHDL Bug occurred ***************************
Please report this bug on https://github.com/ghdl/ghdl/issues
...
******************************************************************

Additional context
Add any other context about the problem here. If applicable, add screenshots to help explain your problem.

[tgingold]

I am not sure what is expected here. The signals are not assigned.

[Topi-ab]

My colleagues don't like my habit of always finding corner cases ;)

I would expect them to behave identically. And both should keep waiting for cover until cycle 12.

There is also something weird going on:

If I add attribute keep to b

	attribute keep: boolean;
	attribute keep of b: signal is true;

And look the cover_b waveform generated by symbiyosys, b is always '0', even when cover requests it to be high.

If I add an assume that b is always '1', the generated cover waveform shows b as '0'.

GHDL seems to be synthesizing $cover which is met on arbitrary case.

[Topi-ab]

Valid use case:

A cover to check that the output port can transition. This would be to find forgotten assignments.

[tgingold]

Covering an output is OK, but I am not sure what covering an undefined signal means.

[Topi-ab]

I understand.

Do you agree that both a and b should give the same cover result?

[Topi-ab]

I passed test.vhdl through yosys:

yosys -m ghdl
ghdl --std=08 test.vhdl -e test
opt
write_verilog test.vo

For me it looks like the first cover is trying to cover a hallucinated wire?

And neither of the covers have anything left of 13 cycles. I probably mis-used yosys.
What is correct way to simplify ghdl output to human readable form, including proper PSL translation?

/* Generated by Yosys 0.36+8 (git sha1 e6021b2b4, clang 11.0.1-2 -fPIC -Os) */

module test(clk_in, a);
  wire _0_;
  output a;
  wire a;
  wire b;
  input clk_in;
  wire clk_in;
  always @* if (1'h1) cover(_0_);
  always @* if (1'h1) cover(1'h0);
  assign a = 1'hz;
  assign b = 1'hx;
endmodule

[tgingold]

You can see the non-optimized, original netlist by using (as a command, not within yosys):

ghdl synth --formal --std=08 test.vhdl -e

But as both a and b are not driven, a lot of optimization can happen and some of them can be random (eg: a or 'Z' can be optimized as '1' or as a).

Note that a and b are not the same: the default value of b is 'U' which is synthesized as 'X', while the default value of a is 'Z'.