Chisel3.4.0のリリースノートを確認した（4） - verificationオブジェクト

Chisel3.4.0の変更点確認の4回目。今回は#1499で追加されたverificationオブジェクトについて。

(#1499) Basic model checking API

PR #1499でexperimental扱いではあるが、verificationというパッケージ・オブジェクトが追加されており、次のメソッドが使用できるようになったとのこと。

• assert()
• assume()
• cover()

名前だけみると、System Verilogのassertionを想像するのだが、試してみたいと思う。

サンプルからRTLを生成する（Verilog HDL）

ということで、まずは適当にサンプルを準備してModule内で使ってみる。

import chisel3._
import chisel3.util._
import chisel3.experimental.verification

class TryVerification extends Module {
  val io = IO(new Bundle {
    val in = Input(Bool())
    val out = Output(Bool())
  })

  io.out := io.in

  verification.assert(io.out === io.in)
  // とりあえずassertと同じものを与えてみる
  verification.assume(io.out === io.in)
  verification.cover(io.out === io.in)
}

object ElaborateTryVerification extends App {
  println((new chisel3.stage.ChiselStage).Verilog(new TryVerification))
}

これをエラボレートしてみると、とりあえずエラーにならずにエラボレートが完了する。 ということで、まあ想像はしていたけどModuleの内部では普通にverificationオブジェクトのメソッドを呼び出すことが出来た。

ただ、上記のコードをそのままエラボレートすると次のようなログが出力される。

------------------------------------------------------------------------------
Warning: 2 verification statements (assert, assume or cover) were
removed when compiling to Verilog because the basic Verilog standard
does not support them. If this was not intended, compile to System
Verilog instead using the `-X sverilog` compiler flag.
------------------------------------------------------------------------------

この状態で生成されたRTLを確認すると、次のようになっていた。

module TryVerification(
  input   clock,
  input   reset,
  input   io_in,
  output  io_out
);
  assign io_out = io_in; // @[TryVerification.scala 12:10]
  always @(posedge clock) begin
    `ifndef SYNTHESIS
    `ifdef STOP_COND
      if (`STOP_COND) begin
    `endif
        if (~(io_out == io_in)) begin
          $fatal; // @[TryVerification.scala 14:22]
        end
    `ifdef STOP_COND
      end
    `endif
    `endif // SYNTHESIS
  end
endmodule

Verilog HDLにはassert/asusme/coverに相当するものがないので、assertの処理のみが$fatalを使って実装される結果となった。

サンプルからRTLを生成する（System Verilog）

これだけだと片手落ちなのでSystem Verilogを生成してみる。
System Verilogで生成する場合は、firrtlのオプションに-X sverilogを与えればいいのだが、 Chisel 3.3からはこのオプションが自動で付与されるemitSystemVerilogメソッドが追加されている。 そのため、サンプルのコードでエラボレートに使用していたemitVerilogを置き換えるだけで良い。

  println((new chisel3.stage.ChiselStage).emitSystemVerilog(new TryVerification))

この状態でエラボレートして、生成されたRTLは次のようにSystem Verilogの各アサーション構文が使用される結果となった。 （何気に自分的には、これが初めてのChisel→System Verilogの変換だったということに気づいた。）

module TryVerification(
  input   clock,
  input   reset,
  input   io_in,
  output  io_out
);
  wire  _T = io_out == io_in; // @[TryVerification.scala 14:30]
  assign io_out = io_in; // @[TryVerification.scala 12:10]
  always @(posedge clock) begin
    //
    if (1'h1) begin
      assert(io_out == io_in); // @[TryVerification.scala 14:22]
    end
    //
    if (1'h1) begin
      assume(_T); // @[TryVerification.scala 15:22]
    end
    //
    if (1'h1) begin
      cover(_T); // @[TryVerification.scala 16:21]
    end
  end
endmodule

ちなみに、Chisel3.assertというものが元々実装されており、そちらを使うと次のようなRTLが生成される。

  always @(posedge clock) begin
    `ifndef SYNTHESIS
    `ifdef PRINTF_COND
      if (`PRINTF_COND) begin
    `endif
        if (~(_T | reset)) begin
          $fwrite(32'h80000002,"Assertion failed\n    at TryVerification.scala:17 assert(io.out === io.in)\n"); // @[TryVerification.scala 17:9]
        end
    `ifdef PRINTF_COND
      end
    `endif
    `endif // SYNTHESIS
    `ifndef SYNTHESIS
    `ifdef STOP_COND
      if (`STOP_COND) begin
    `endif
        if (~(_T | reset)) begin
          $fatal; // @[TryVerification.scala 17:9]
        end
    `ifdef STOP_COND
      end
    `endif
    `endif // SYNTHESIS
  end

まあSystem Veirlogの方は言語仕様としてサポートされているassertに直接マッピングされるので、検証でSystem Verilogの環境を使用するなら、こちらの方がスマートになるな、という印象。商用のシミュレータ使うなら、色々そっち方面の機能はたくさんあるし。

今後どうなるかは不明だが、今の所、各サイクル毎の即時アサーションのみのサポートなので、複数サイクルにまたがったようなアサーションは書くことが出来ない。 PRには今後はSystem Verilogの$pastとかもサポートしたい、と書いてあるので、拡充されることを期待。 とはいえ、きちんとしたアサーションはモジュールの外側からbindとかでやるのが良さそうな感じである。（信号名変わったりは普通に起こるから、色々対策しとかないとではあるけど。。）

あと、System Verilogの構文のサポートも始まったっぽいので、ぜひVecとかBundleの変換も頑張って欲しいと思った。