Add Formal

.github/workflows/main.yml

@@ -73,3 +73,19 @@ jobs:
       - name: "Run verilator"
         run: |
           nix run '.#gcd.verilated'
+
+  run-formal-verification:
+    name: "Run Formal Verification"
+    strategy:
+      fail-fast: false
+    runs-on: [self-hosted, linux, nixos]
+    defaults:
+      run:
+        working-directory: ./templates/chisel
+    steps:
+      - uses: actions/checkout@v4
+        with:
+          ref: ${{ github.event.pull_request.head.sha }}
+      - name: "Run Formal Verification"
+        run: |
+          nix build '.#gcd.formal' --impure

readme.md

@@ -30,14 +30,15 @@ Every thing that developers want to add or modify should go into the `overlay.ni
 This skeleton provides a simple [GCD](https://en.wikipedia.org/wiki/Greatest_common_divisor) example.
 It's build script is in `nix/gcd` folder, providing the below attributes:
 
-* {gcd,tb}-compiled: JVM bytecode for the GCD/GCDTestbench and elaborator
-* {gcd,tb}-compiled.elaborator: A bash wrapper for running the elaborator with JDK
-* [tb-]elaborate: Unlowered MLIR bytecode output from firrtl elaborated by elaborator
-* [tb-]mlirbc: MLIR bytecode lowered by circt framework
-* [tb-]rtl: SystemVerilog generated from the lowered MLIR bytecode
+* {gcd,tb,formal}-compiled: JVM bytecode for the GCD/GCDTestbench and elaborator
+* {gcd,tb,formal}-compiled.elaborator: A bash wrapper for running the elaborator with JDK
+* [{tb,formal}-]elaborate: Unlowered MLIR bytecode output from firrtl elaborated by elaborator
+* [{tb,formal}-]mlirbc: MLIR bytecode lowered by circt framework
+* [{tb,formal}-]rtl: SystemVerilog generated from the lowered MLIR bytecode
 * tb-dpi-lib: DPI library written in Rust for both Verilator and VCS
 * verilated[-trace]: C++ simulation executable and libaray generated by Verilator with/without `fst` waveform trace
 * vcs[-trace]: C simulation executable compiled by VCS with/without `fsdb` waveform trace
+* formal: Formal verification report generated by JasperGold
 
 To get the corresponding output, developers can use:
 
@@ -89,7 +90,17 @@ nix run '.#gcd.vcs-trace' --impure -- +dump-start=0 +dump-end=10000 +wave-path=t
 
 The DPI lib can automatically match the arguments and does not interact with VCS. In this case, the first three parameters will be passed to the DPI lib to control waveform generation, and the last parameter will be passed to the VCS to dump the results of all sva statements.
 
-Note that in order to use VCS for simulation, you need to set the environment variables `VC_STATIC_HOME` and `SNPSLMD_LICENSE_FILE` and add the`--impure` flag.
+* Note that in order to use VCS for simulation, you need to set the environment variables `VC_STATIC_HOME` and `SNPSLMD_LICENSE_FILE` and add the`--impure` flag.
+
+To run the formal verification. Then you can run:
+
+```bash
+nix run '.#gcd.formal' --impure
+```
+
+and the formal verification report will be generated in the result/
+
+* Note that in order to use jasper gold for formal verification, you need to set the environment variables `JASPER_HOME` and `CDS_LIC_FILE` and add the`--impure` flag.
 
 ## References
 

templates/chisel/configs/GCDFormalMain.json

@@ -0,0 +1,6 @@
+{
+    "gcdParameter": {
+        "width": 16,
+        "useAsyncReset": false
+    }
+}

templates/chisel/elaborator/src/GCDFormal.scala

@@ -0,0 +1,36 @@
+// SPDX-License-Identifier: Unlicense
+// SPDX-FileCopyrightText: 2024 Jiuyang Liu <[email protected]>
+package org.chipsalliance.gcd.elaborator
+
+import mainargs._
+import org.chipsalliance.gcd.{GCDFormal, GCDFormalParameter}
+import org.chipsalliance.gcd.elaborator.Elaborator
+import org.chipsalliance.gcd.elaborator.GCDMain.GCDParameterMain
+
+object GCDFormalMain extends Elaborator {
+  @main
+  case class GCDFormalParameterMain(
+    @arg(name = "gcdParameter") gcdParameter: GCDParameterMain) {
+    def convert: GCDFormalParameter = GCDFormalParameter(gcdParameter.convert)
+  }
+
+  implicit def GCDParameterMainParser: ParserForClass[GCDParameterMain] =
+    ParserForClass[GCDParameterMain]
+
+  implicit def GCDFormalParameterMainParser: ParserForClass[GCDFormalParameterMain] =
+    ParserForClass[GCDFormalParameterMain]
+
+  @main
+  def config(@arg(name = "parameter") parameter: GCDFormalParameterMain) =
+    configImpl(parameter.convert)
+
+  @main
+  def design(
+    @arg(name = "parameter") parameter:    os.Path,
+    @arg(name = "run-firtool") runFirtool: mainargs.Flag,
+    @arg(name = "target-dir") targetDir:   os.Path
+  ) =
+    designImpl[GCDFormal, GCDFormalParameter](parameter, runFirtool.value, targetDir)
+
+  def main(args: Array[String]): Unit = ParserForMethods(this).runOrExit(args)
+}

templates/chisel/gcd/src/GCD.scala

@@ -6,12 +6,9 @@ package org.chipsalliance.gcd
 import chisel3._
 import chisel3.experimental.hierarchy.{instantiable, public, Instance, Instantiate}
 import chisel3.experimental.{SerializableModule, SerializableModuleParameter}
-import chisel3.ltl.Property.{eventually, not}
-import chisel3.ltl.{AssertProperty, CoverProperty, Delay, Sequence}
 import chisel3.probe.{define, Probe, ProbeValue}
 import chisel3.properties.{AnyClassType, Class, Property}
-import chisel3.util.circt.dpi.{RawClockedNonVoidFunctionCall, RawUnclockedNonVoidFunctionCall}
-import chisel3.util.{Counter, DecoupledIO, HasExtModuleInline, RegEnable, Valid}
+import chisel3.util.{DecoupledIO, Valid}
 
 object GCDParameter {
   implicit def rwP: upickle.default.ReadWriter[GCDParameter] =
@@ -85,188 +82,3 @@ class GCD(val parameter: GCDParameter)
   val omInstance: Instance[GCDOM] = Instantiate(new GCDOM(parameter))
   io.om := omInstance.getPropertyReference.asAnyClassType
 }
-
-object GCDTestBenchParameter {
-  implicit def rwP: upickle.default.ReadWriter[GCDTestBenchParameter] =
-    upickle.default.macroRW
-}
-
-/** Parameter of [[GCD]]. */
-case class GCDTestBenchParameter(
-  testVerbatimParameter: TestVerbatimParameter,
-  gcdParameter:          GCDParameter,
-  timeout:               Int,
-  testSize:              Int)
-    extends SerializableModuleParameter {
-  require(
-    (testVerbatimParameter.useAsyncReset && gcdParameter.useAsyncReset) ||
-      (!testVerbatimParameter.useAsyncReset && !gcdParameter.useAsyncReset),
-    "Reset Type check failed."
-  )
-}
-
-@instantiable
-class GCDTestBenchOM(parameter: GCDTestBenchParameter) extends Class {
-  val gcd = IO(Output(Property[AnyClassType]()))
-  @public
-  val gcdIn = IO(Input(Property[AnyClassType]()))
-  gcd := gcdIn
-}
-
-class GCDTestBenchInterface(parameter: GCDTestBenchParameter) extends Bundle {
-  val om = Output(Property[AnyClassType]())
-}
-
-@instantiable
-class GCDTestBench(val parameter: GCDTestBenchParameter)
-    extends FixedIORawModule(new GCDTestBenchInterface(parameter))
-    with SerializableModule[GCDTestBenchParameter]
-    with ImplicitClock
-    with ImplicitReset {
-  override protected def implicitClock: Clock = verbatim.io.clock
-  override protected def implicitReset: Reset = verbatim.io.reset
-  // Instantiate Drivers
-  val verbatim: Instance[TestVerbatim] = Instantiate(
-    new TestVerbatim(parameter.testVerbatimParameter)
-  )
-  // Instantiate DUT.
-  val dut: Instance[GCD] = Instantiate(new GCD(parameter.gcdParameter))
-  // Instantiate OM
-  val omInstance = Instantiate(new GCDTestBenchOM(parameter))
-  io.om := omInstance.getPropertyReference.asAnyClassType
-  omInstance.gcdIn := dut.io.om
-
-  dut.io.clock := implicitClock
-  dut.io.reset := implicitReset
-
-  // Simulation Logic
-  val simulationTime: UInt = RegInit(0.U(64.W))
-  simulationTime := simulationTime + 1.U
-  // For each timeout ticks, check it
-  val (_, callWatchdog) = Counter(true.B, parameter.timeout / 2)
-  val watchdogCode = RawUnclockedNonVoidFunctionCall("gcd_watchdog", UInt(8.W))(callWatchdog)
-  when(watchdogCode =/= 0.U) {
-    stop(cf"""{"event":"SimulationStop","reason": ${watchdogCode},"cycle":${simulationTime}}\n""")
-  }
-  class TestPayload extends Bundle {
-    val x = UInt(parameter.gcdParameter.width.W)
-    val y = UInt(parameter.gcdParameter.width.W)
-    val result = UInt(parameter.gcdParameter.width.W)
-  }
-  val request =
-    RawClockedNonVoidFunctionCall("gcd_input", Valid(new TestPayload))(
-      dut.io.clock,
-      !dut.io.reset.asBool && dut.io.input.ready
-    )
-  when(dut.io.input.ready) {
-    dut.io.input.valid := request.valid
-    dut.io.input.bits := request.bits
-  }.otherwise {
-    dut.io.input.valid := false.B;
-    dut.io.input.bits := DontCare;
-  }
-
-  // LTL Checker
-  import Sequence._
-  val inputFire:         Sequence = dut.io.input.fire
-  val inputNotFire:      Sequence = !dut.io.input.fire
-  val outputFire:        Sequence = dut.io.output.valid
-  val outputNotFire:     Sequence = !dut.io.output.valid
-  val lastRequestResult: UInt = RegEnable(request.bits.result, dut.io.input.fire)
-  val checkRight:        Sequence = lastRequestResult === dut.io.output.bits
-  val inputNotValid:     Sequence = dut.io.input.ready && !dut.io.input.valid
-
-  AssertProperty(
-    inputFire |=> inputNotFire.repeatAtLeast(1) ### outputFire,
-    label = Some("GCD_ALWAYS_RESPONSE")
-  )
-  AssertProperty(
-    inputFire |=> not(inputNotFire.repeatAtLeast(1) ### (outputNotFire.and(inputFire))),
-    label = Some("GCD_NO_DOUBLE_FIRE")
-  )
-  AssertProperty(
-    outputFire |-> checkRight,
-    label = Some("GCD_ASSERT_RESULT_CHECK")
-  )
-  // TODO: need generate $rose function in SVA
-  // CoverProperty(
-  //   rose(outputFire).nonConsecutiveRepeat(parameter.testSize - 1),
-  //   label = Some("GCD_COVER_FIRE")
-  // )
-  CoverProperty(
-    inputNotValid,
-    label = Some("GCD_COVER_BACK_PRESSURE")
-  )
-}
-object TestVerbatimParameter {
-  implicit def rwP: upickle.default.ReadWriter[TestVerbatimParameter] =
-    upickle.default.macroRW
-}
-
-case class TestVerbatimParameter(
-  useAsyncReset:    Boolean,
-  initFunctionName: String,
-  dumpFunctionName: String,
-  clockFlipTick:    Int,
-  resetFlipTick:    Int)
-    extends SerializableModuleParameter
-
-@instantiable
-class TestVerbatimOM(parameter: TestVerbatimParameter) extends Class {
-  val useAsyncReset:    Property[Boolean] = IO(Output(Property[Boolean]()))
-  val initFunctionName: Property[String] = IO(Output(Property[String]()))
-  val dumpFunctionName: Property[String] = IO(Output(Property[String]()))
-  val clockFlipTick:    Property[Int] = IO(Output(Property[Int]()))
-  val resetFlipTick:    Property[Int] = IO(Output(Property[Int]()))
-  val gcd = IO(Output(Property[AnyClassType]()))
-  @public
-  val gcdIn = IO(Input(Property[AnyClassType]()))
-  gcd := gcdIn
-  useAsyncReset := Property(parameter.useAsyncReset)
-  initFunctionName := Property(parameter.initFunctionName)
-  dumpFunctionName := Property(parameter.dumpFunctionName)
-  clockFlipTick := Property(parameter.clockFlipTick)
-  resetFlipTick := Property(parameter.resetFlipTick)
-}
-
-/** Test blackbox for clockgen, wave dump and extra testbench-only codes. */
-class TestVerbatimInterface(parameter: TestVerbatimParameter) extends Bundle {
-  val clock: Clock = Output(Clock())
-  val reset: Reset = Output(
-    if (parameter.useAsyncReset) AsyncReset() else Bool()
-  )
-}
-
-@instantiable
-class TestVerbatim(parameter: TestVerbatimParameter)
-    extends FixedIOExtModule(new TestVerbatimInterface(parameter))
-    with HasExtModuleInline {
-  setInline(
-    s"$desiredName.sv",
-    s"""module $desiredName(output reg clock, output reg reset);
-       |  export "DPI-C" function ${parameter.dumpFunctionName};
-       |  function ${parameter.dumpFunctionName}(input string file);
-       |`ifdef VCS
-       |    $$fsdbDumpfile(file);
-       |    $$fsdbDumpvars("+all");
-       |    $$fsdbDumpSVA;
-       |    $$fsdbDumpon;
-       |`endif
-       |`ifdef VERILATOR
-       |    $$dumpfile(file);
-       |    $$dumpvars(0);
-       |`endif
-       |  endfunction;
-       |
-       |  import "DPI-C" context function void ${parameter.initFunctionName}();
-       |  initial begin
-       |    ${parameter.initFunctionName}();
-       |    clock = 1'b0;
-       |    reset = 1'b1;
-       |  end
-       |  initial #(${parameter.resetFlipTick}) reset = 1'b0;
-       |  always #${parameter.clockFlipTick} clock = ~clock;
-       |endmodule
-       |""".stripMargin
-  )
-}