KNOWNBUG test for nonblocking followed by blocking assignment

[kroening]

Summary

Adds a KNOWNBUG regression test for a pre-existing soundness bug that is present in both the legacy synthesis flow and the new RTL construction (#2119).

A nonblocking assignment schedules the update in the NBA region, which follows the active region in which the blocking assignments of the same time step execute (1800-2017 4.9.3). A blocking assignment to the same variable later in the same block is therefore overridden by the earlier nonblocking one. Both flows instead let the last assignment in program order win.

always @(posedge clk) begin
  x <= 1;
  x = 2;
end
p0: assert property (@(posedge clk) ##1 x == 1);  // REFUTED: x == 2

Also covers y <= y + 10; y++;. Expected values cross-checked with Icarus Verilog.

Testing

• regression/verilog/assignments/nonblocking-then-blocking1.desc is reported as SKIPPED by test.pl.
• Run as CORE, the test fails with both the legacy and the RTL flow at e224197c.

Root cause

record_assignment in src/verilog/verilog_rtl.cpp writes blocking and nonblocking values into the same state.values map, so program order decides. Nonblocking values need to take precedence over blocking ones in the committed next-state value (while blocking values are still what subsequent reads in the block see).