Formal verification: Verilog generated when using synchronous resets is not understood by SymbiYosys

[janschiefer]

SpinalHDL: 1.10.1
Scala version: 2.12.18
sbt version: 1.9.8
SymbiYosys version: Git 19.02.204

Problem:

• SymbiYosys chokes on "assert(xxx) else begin end"- statements ( maybe not supported? )
• also, a ";" is missing after the assert-statement

Fix:

• remove generation of this block... at least for now:

else begin
        $fatal(""); // MyTopLevelFormal.scala:L23
        $finish;
      end

• generate ";" behind assert

Full demonstration: https://github.com/janschiefer/SpinalTemplateSbt/tree/code-generation-sync-reset

Let's try to verify code, that geneate a sychronous reset:

Config.scala:

package projectname

import spinal.core._
import spinal.core.sim._

object Config {
  def spinal = SpinalConfig(
    targetDirectory = "hw/gen",
    defaultConfigForClockDomains = ClockDomainConfig(
      resetActiveLevel = HIGH,
      resetKind = SYNC
    ),
    onlyStdLogicVectorAtTopLevelIo = true
  )

  def sim = SimConfig.withConfig(spinal).withFstWave
}

MyTopLevelFormal.scala:

package projectname

import spinal.core._
import spinal.core.formal._

// You need SymbiYosys to be installed.
// See https://spinalhdl.github.io/SpinalDoc-RTD/master/SpinalHDL/Formal%20verification/index.html#installing-requirements
object MyTopLevelFormal extends App {
  FormalConfig
    .withConfig( Config.spinal )
    .withBMC(10)
    .doVerify(new Component {
      val dut = FormalDut(MyTopLevel())

      // Ensure the formal test start with a reset
      assumeInitial(clockDomain.isResetActive)

      // Provide some stimulus
      anyseq(dut.io.cond0)
      anyseq(dut.io.cond1)

      // Check the state initial value and increment
      assert(dut.io.state === past(dut.io.state + U(dut.io.cond0)).init(0))
    })
}

SymbiYosys logfile:

SBY  2:03:42 [/home/jschiefer/Code/SpinalTemplateSbt/./simWorkspace/unamed/unamed_bmc] Removing directory '/home/jschiefer/Code/SpinalTemplateSbt/simWorkspace/unamed/unamed_bmc'.
SBY  2:03:42 [/home/jschiefer/Code/SpinalTemplateSbt/./simWorkspace/unamed/unamed_bmc] Copy '/home/jschiefer/Code/SpinalTemplateSbt/simWorkspace/unamed/rtl/unamed.sv' to '/home/jschiefer/Code/SpinalTemplateSbt/simWorkspace/unamed/unamed_bmc/src/unamed.sv'.
SBY  2:03:42 [/home/jschiefer/Code/SpinalTemplateSbt/./simWorkspace/unamed/unamed_bmc] engine_0: smtbmc --progress yices
SBY  2:03:42 [/home/jschiefer/Code/SpinalTemplateSbt/./simWorkspace/unamed/unamed_bmc] base: starting process "cd /home/jschiefer/Code/SpinalTemplateSbt/./simWorkspace/unamed/unamed_bmc/src; yosys -ql ../model/design.log ../model/design.ys"
SBY  2:03:42 [/home/jschiefer/Code/SpinalTemplateSbt/./simWorkspace/unamed/unamed_bmc] base: unamed.sv:41: ERROR: syntax error, unexpected TOK_ELSE, expecting ';'
SBY  2:03:42 [/home/jschiefer/Code/SpinalTemplateSbt/./simWorkspace/unamed/unamed_bmc] base: finished (returncode=1)
SBY  2:03:42 [/home/jschiefer/Code/SpinalTemplateSbt/./simWorkspace/unamed/unamed_bmc] base: task failed. ERROR.
SBY  2:03:42 [/home/jschiefer/Code/SpinalTemplateSbt/./simWorkspace/unamed/unamed_bmc] summary: Elapsed clock time [H:MM:SS (secs)]: 0:00:00 (0)
SBY  2:03:42 [/home/jschiefer/Code/SpinalTemplateSbt/./simWorkspace/unamed/unamed_bmc] summary: Elapsed process time [H:MM:SS (secs)]: 0:00:00 (0)
SBY  2:03:42 [/home/jschiefer/Code/SpinalTemplateSbt/./simWorkspace/unamed/unamed_bmc] summary: engine_0 (smtbmc --progress yices) did not return a status
SBY  2:03:42 [/home/jschiefer/Code/SpinalTemplateSbt/./simWorkspace/unamed/unamed_bmc] summary: engine_0 did not produce any traces
SBY  2:03:42 [/home/jschiefer/Code/SpinalTemplateSbt/./simWorkspace/unamed/unamed_bmc] DONE (ERROR, rc=16)

unnamed.sv:

// Generator : SpinalHDL v1.10.1    git head : 2527c7c6b0fb0f95e5e1a5722a0be732b364ce43
// Component : unamed
// Git hash  : 3b8455515888705f2bee9f6a3c42b0e43cb49558

`timescale 1ns/1ps

module unamed (
  input  wire          reset,
  input  wire          clk
);

  wire                dut_io_cond0;
  wire                dut_io_cond1;
  wire                dut_io_flag;
  wire       [7:0]    dut_io_state;
  wire       [7:0]    _zz__zz_1;
  wire       [0:0]    _zz__zz_1_1;
  reg        [7:0]    _zz_1;

  assign _zz__zz_1_1 = dut_io_cond0;
  assign _zz__zz_1 = {7'd0, _zz__zz_1_1};
  MyTopLevel dut (
    .io_cond0 (dut_io_cond0     ), //i
    .io_cond1 (dut_io_cond1     ), //i
    .io_flag  (dut_io_flag      ), //o
    .io_state (dut_io_state[7:0]), //o
    .clk      (clk              ), //i
    .reset    (reset            )  //i
  );
  initial begin
    assume(reset); // MyTopLevelFormal.scala:L16
  end

  assign dut_io_cond0 = $anyseq(1);
  assign dut_io_cond1 = $anyseq(1);
  always @(posedge clk) begin
    if(reset) begin
      _zz_1 <= 8'h00;
    end else begin
      _zz_1 <= (dut_io_state + _zz__zz_1);
      assert((dut_io_state == _zz_1)) else begin
        $fatal(""); // MyTopLevelFormal.scala:L23
        $finish;
      end
    end
  end


endmodule

module MyTopLevel (
  input  wire          io_cond0,
  input  wire          io_cond1,
  output wire          io_flag,
  output wire [7:0]    io_state,
  input  wire          clk,
  input  wire          reset
);

  reg        [7:0]    counter;

  assign io_state = counter;
  assign io_flag = ((counter == 8'h00) || io_cond1);
  always @(posedge clk) begin
    if(reset) begin
      counter <= 8'h00;
    end else begin
      if(io_cond0) begin
        counter <= (counter + 8'h01);
      end
    end
  end


endmodule

When I manually edit the generated file and change line 41 to "assert((dut_io_state != _zz_1));" and remove the "else begin (...) end"-block sby works like a charm.

[Readon]

The problem of your code is

.withConfig( Config.spinal )

This line use Spinal's elaboration config which is not compatible with the formal config one, delete it would work.

[janschiefer]

The line is necessary to get a purely synchronous reset in this context.

Without this line, the following code is generated:

(...)
  always @(posedge clk or posedge reset) begin
(...)

Maybe I'm wrong, but that seems like an async reset to me.

This async reset actually triggers another bug, but within SpinalTemplateSbt: SpinalHDL/SpinalTemplateSbt#39

Proposed fix / hack / bypass (?): #1315

[Readon]

This might be a solution.

.withConfig( Config.spinal.includeFormal )

[janschiefer]

Yes this actually works in SYNC reset mode.

In ASYNC reset mode we actually need to set the SymbiYosys multiclock mode.

Here my attempt to fix both issues: #1320
--> use .includeFormal as default in FormalConfig and therefore do not generate "assert(...) else ... begin" blocks in formal verification mode
--> use "multiclock on" when an using an ASYNC reset in the default clock domain

[Readon]

Yes this actually works in SYNC reset mode.

In ASYNC reset mode we actually need to set the SymbiYosys multiclock mode.

Here my attempt to fix both issues: #1320 --> use .includeFormal as default in FormalConfig and therefore do not generate "assert(...) else ... begin" blocks in formal verification mode --> use "multiclock on" when an using an ASYNC reset in the default clock domain

I think use "multiclock on" for a synchronized design with only ASYNC reset is a little bit redundant. It might be slower.
If you are using asynchronous clocks, then multiclock on might be a good choice. Have you looked at the FormalFifoCCTester example in the lib?

[janschiefer]

Not yet...ok.
Well, the assumeResetReleaseSync / assumeIOSync2Clock in this complex example make sense...

--> I need to implement this in the SpinalHDL Template, so the template formal workflow works again by default.

Actually the real issue here seens the complete lack of documentation for all of SpinalHDL awesome and kick-ass "hidden" features.

[janschiefer]

Can you help me getting the Spinal basic template to run with assumeResetReleaseSync, and GlobalClock without multiclock mode?

I'm kinda lost here...

[Readon]

Can you help me getting the Spinal basic template to run with assumeResetReleaseSync, and GlobalClock without multiclock mode?

I'm kinda lost here...

Those assumeResetReleaseSync and GlobalClock are initially designed for clock crossing design, if you just want to verify a design with different reset, I think they are not necessary.

So if what you want is to verify your design which have cross clock manner, I can give you some hits.
In formal verification of yosys, the asynchronous verification is driven by a hidden clock, so called GlobalClock.
All clocks for the design is generated from that.

The relationship between each clock and reset or io signals should be explicit declared.
This make things complex, so some functions have been wrapped for that.

//assume the pushClock's period while verification.
gclk.assumeClockTiming(pushClock, pushPeriod)
//this keep the reset signal synchronize with it's corresponding clock. here pushClock domain's reset is synchronized with it's clock.
gclk.assumeResetReleaseSync(pushClock)
//this function make sure push.valid signal is a signal synchronized with the pushClock domain's clock.
gclk.assumeIOSync2Clock(pushClock, dut.io.push.valid)

Also, some utilities is design for timing.

//this keep the reset last for popPeriod.
gclk.keepBoolLeastCycles(reset, popPeriod)
//this make sure pushClock domain's reset and popClock domain's reset active at the same time.
gclk.alignAsyncResetStart(pushClock, popClock)

[Readon]

you can use them by calling withAsync method of FormalConfig.

[Readon]

About the documentation, the formal verification currently is still not widely used, especially the Cross Clocking one. So I want to wait more test before we documented the usage.
Because if it is documented, the backward compatibility would be the most important thing we should take consider in.