Unexpected behaviour with asynchronous reset

[mpardalos]

I am attempting to verify a module with an asynchronous reset, and sby is giving me a counterexample trace that does not seem to match with what I get when simulating with icarus verilog.

counter.sv

module counter(input clk, input rst, output reg [7:0] count);
   always @(posedge clk or posedge rst) begin
      if (rst)
        count <= 0;
      else
        count <= count + 1;
   end

   assert property (@(posedge rst) count == 0);
endmodule // counter

counter.sby

[options]
mode prove

[engines]
smtbmc

[script]
read -formal counter.sv
prep -top counter

[files]
counter.sv

The symbiyosys trace: trace.vcd.gz

I would expect the rst signal to always reset the counter, but the trace from sby shows it having no effect when an rst and clk edge arrive at the same time. Attempting to replicate this in simulation (using icarus verilog) shows rst behaving as expected (resetting the counter) rather that what sby shows.

[cmichon]

I'm facing similar issue with version 0.38 on similar code

I had to change your verilog to get it to compile with sby

module counter(input clk, input rst, output reg [7:0] count);
   always @(posedge clk or posedge rst) begin
      if (rst)
        count <= 0;
      else
        count <= count + 1;
   end

   always @(posedge rst)
       assert property ( count == 0);

endmodule // counter

[aiju]

Since your design uses asynchronous logic in the form of async reset, you need to set "multiclock on" in your [options] block. Without multiclock you cannot have different edge-sensitive triggers, i.e. "@(posedge clk)" and "@(posedge rst)". All edge-sensitive triggers must be synchronous to the edge of a single clock (which is the implied global clock). After enabling multiclock, the traces now correctly show the counter being reset to 0.

Your assertion still fails, but I think that's because the assertion is allowed to run before the first always block and you maybe want something like assert property(@(posedge rst) rst |-> count == 0).

[whitequark]

By the way, why does multiclock off even exist? It seems like it's causing an entire class of bugs to be silently introduced.

[jix]

@whitequark multiclock on often has significantly worse performance and can break k-induction (meaning that for some engines you will not be able to successfully perform unbounded checks that otherwise would pass).

[whitequark]

@jix I see. Can a check be added so that multiclock off only accepts single-clock (actually single-async-signal) designs? This seems like a really common footgun; we hit it in Amaranth some time ago too, IIRC.

[aiju]

So the only thing that multiclock off does is add a async2sync pass to yosys (instead of clk2fflogic). This pass replaces every appearance of asynchronous logic with synchronous logic that assumes all signals are synchronised the clock edges. Maybe the pass could issue a warning if it modifies the design? The ff.has_gclk check looks promising to me but I could be way off base there.

That said, as an aside, after having a look at this code I'm a little confused why the original code produces incorrect traces. Surely if yosys basically replaces posedge clk or posedge rst with posedge clk then there should never be a trace where it just fails to reset. I'll do some more poking.

[jix]

@whitequark One issue is that using multiclock off for a design that has a single clock but async resets is supported, but treats the async resets as sync resets (as @aiju just mentioned, multiclock off runs the async2sync pass). This does allow for efficient verification of the synchronous part of the design even in the presence of an async reset (with some mild implicit assumptions on how async resets are sequenced wrt each other and the clock), which is what you usually want to do in practice. The problem is that there is no simple way to tell how the async resets are actually used or rather whether the implicit assumptions that come with using async2sync are valid for a specific verification use case.

I'm not opposed to adding more checks that catch some of the obviously broken cases, e.g. I added one rather limited specific check a while ago (having a posedge and negedge of the same signal in the same module), but I'm sure there is more that can be safely rejected the way things currently work, even if that would still come short of exactly characterizing the supported use cases.

Overall, I'm also not at all happy with how multiclock currently works. What I'd really want is to unconditionally have the multiclock on behavior. To get that working without getting the performance/completeness issues of the current implementation and to avoid making the FV flow unmaintainable I would make significant changes to several parts of the flow. The same changes would also benefit or even be required for a lot of other improvements, so I hope this is something I get to start working on sooner than later.

[jix]

After discussing this with @aiju and having a closer look at the input design and resulting trace I think there's a check that we can add to async2sync to prevent this specific failure mode, making this less of a footgun.

When the same signal is simultaneously used as a) a clock input of one FF and b) an async reset input of a different FF, the transformation done by async2sync is invalid (unless the signal never actually toggles), so it should reject such inputs. It may be possible to extend the check to also cover combinationally related signals instead of just the same signal, but for that we might have to be more careful about false-positives.