tree e83fc6e87e2b59e6beb8ccd1de72032e9de37626
parent 7ac20f12050f2a4fb169358c1956995e87325cce
author George Hilliard <thirtythreeforty@gmail.com> 1646197115 -0600
committer George Hilliard <thirtythreeforty@gmail.com> 1646197751 -0600

Emit error when encountering assert/assume properties

Yosys doesn't have good handling of properties yet (see
YosysHQ/yosys#3223).  In the meantime, SymbiYosys with the UHDM plugin
will happily prove this model "correct":

    module wrong(input clk);
        logic data;
        always_comb data <= 0;
        assert property( @(posedge clk) data );
    endmodule

The `assert property` is silently dropped from the UHDM parse tree when
it's converted to AST nodes, and the user's design has a bug but passes
formal.  (Changing it to a clocked immediate assertion allows the solver
to find a counterexample.)

At least, emit an error for this case.  Real support for SVA assertions
can be added.

Signed-off-by: George Hilliard <thirtythreeforty@gmail.com>