SymbiYosys doesn't handle latches properly

[ZipCPU]

Steps to reproduce the issue

Given the attached file, first change its name to latchchk.sby and then run sby -f latchchk.sby. It contains a series of 9 tests describing latch behavior, ranging from a basic latch and enable, to one with a set, reset, and enable. While the latch with enable passes, all of the more complex tests (tests 2-9) fail.

Expected behavior

I expect this design to pass a formal verification check.

Actual behavior

Tests 2-9 fail. Failures are marked within by the assertion failing. In general, the latch fails to take on the value of the input when enabled. In two cases, the test also fails on a negative set condition failing to set the latch.

This failure was seen when using the SymbioticEDA Suite, dated 20200803A.

Dan
latchchk.txt

[clairexen]

It passes with YOSYS_NOVERIFIC=1. So for some reason we get a different semantic when we import through Verific.