`$stable` assumption is violated

[albydnc]

Hello,

I'm trying to verify a multiclock design. I took example from the @ZipCPU async FIFO to setup the signals. here is the part of the formal definition that is not working as expected:

  always @($global_clock)
    if (f_past_valid_gbl) begin
      assume (test_rose_signal == $rose(TELL40_output_clock));
      if (!$rose(DP_clock)) begin
        //data
        assume ($stable(valid_ST_sink_data_processing));
        assume ($stable(data_ST_sink_data_processing));
        assume ($stable(FTYPE_ST_sink_data_processing));
        assume ($stable(FTYPE_bxiderrorinfo_ST_source_data_processing));
        assert ($stable(ready_ST_source_data_processing));
        //tfc
        assume ($stable(valid_ST_sink_tfc_processing));
        assume ($stable(data_ST_sink_tfc_processing));
        assert ($stable(ready_ST_source_tfc_processing));
      end

      if (!$rose(TELL40_output_clock)) begin
        //data
        assume ($stable(ready_ST_sink_data_processing_out)); // THIS ASSUMPTION IS VIOLATED!!!
        assert ($stable(valid_ST_source_data_processing_out));
        assert ($stable(data_ST_source_data_processing_out));
        assert ($stable(SOF_ST_source_data_processing_out));
        assert ($stable(EOF_ST_source_data_processing_out));
        assert ($stable(BXID_ST_source_data_processing_out));
        assert ($stable(FTYPE_ST_source_data_processing_out));
        assert ($stable(FSIZE_ST_source_data_processing_out));
        //tfc
        assert ($stable(tfc_data_ST_source_data_processing_o

        assert ($stable(tfc_valid_ST_source_data_processing_out));

      end
    end

since ready_ST_sink_data_processing_out is not kept stable, assertions $stable on ready_ST_source_tfc_processing and ready_ST_source_data_processing are failing.

I added the VCD and the waveform issue as jpg.

ut));

vcd_out.zip

[ZipCPU]

Reviewing your image alone, this looks like the correct tool behavior. The issue associated with a toggle on the last step, when the clock doesn't rise, is the correct behavior: since the clock hasn't risen (yet), or more specifically since the global clock hasn't risen yet, there's no ability to evaluate $rose. You have to wait one more time step.

Find me on IRC if you want to chat more.

Dan