commit 5cae0cf1fac783e0d0df8c8597bf65322a696a56
author Rupert Swarbrick <rswarbrick@lowrisc.org> Mon Mar 16 12:23:36 2020 +0000
committer Rupert Swarbrick <rswarbrick@gmail.com> Wed Jul 01 09:39:56 2020 +0100
tree b1172e437274b31c2d709191087c877ff0bd427f
parent 51b7fc46b6f5998d7c1be366c4897d9bf188a597

Allow different assertion "backends" in prim_assert.sv

Different tools support different assertions. This splits out the
definitions of the base macros from prim_assert.sv into separate
headers (prim_assert_standard_macros.svh, prim_assert_dummy_macros.svh
and prim_assert_yosys_macros.svh).

The last of the three is new: it's used for Yosys when not
synthesizing (so used when Yosys is being run as a formal tool).

At the moment, Yosys's (System)Verilog frontend doesn't support
concurrent assertions. It does, however, support the immediate form,
so prim_assert_yosys_macros.svh expresses them as such.

For example, ASSERT_I is normally

   name: assert (expr) else stmt

but here it becomes:

   begin : name
     assert (expr);
   end

(The name isn't reported by the error reporting machinery in the Yosys
flow, but at least it makes code a bit easier to figure out if you've
preprocessed your source with sv2v and the line numbers are all
bogus).

Similarly, ASSERT is normally something like:

   name: assert property (@(posedge clk_i) disable iff rst_ni expr)

Here it becomes:

   always_ff @(posedge clk_i) begin : name
     if (rst_ni) name: assert (prop);
   end

These transformations should not change the truth of an assertion, at
least with the Yosys tool (which isn't event based and samples signals
for assertions after everything has settled).

Signed-off-by: Rupert Swarbrick <rswarbrick@lowrisc.org>