verific: Fix conditions of SVAs with explicit clocks within procedures
authorJannis Harder <me@jix.one>
Tue, 3 May 2022 11:22:18 +0000 (13:22 +0200)
committerJannis Harder <me@jix.one>
Tue, 3 May 2022 12:13:08 +0000 (14:13 +0200)
commit96f64f4788ca64adde55421a6abadefd182d9a1a
treeb3c7faecdbcf26b4b7357024994719f3c06869e9
parent11e75bc27ceacb909c31fc201110f78ee995f979
verific: Fix conditions of SVAs with explicit clocks within procedures

For SVAs that have an explicit clock and are contained in a procedure
which conditionally executes the assertion, verific expresses this using
a mux with one input connected to constant 1 and the other output
connected to an SVA_AT. The existing code only handled the case where
the first input is connected to 1. This patch also handles the other
case.
frontends/verific/verific.cc
frontends/verific/verific.h
frontends/verific/verificsva.cc
tests/sva/nested_clk_else.sv [new file with mode: 0644]