[formal] add Formal TestBench

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 <liu@jiuyang.me>
+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/GCDFormal.scala

@@ -0,0 +1,103 @@
+// SPDX-License-Identifier: Unlicense
+// SPDX-FileCopyrightText: 2024 Jiuyang Liu <liu@jiuyang.me>
+
+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.properties.{AnyClassType, Class, Property}
+import chisel3.util.circt.dpi.{RawClockedNonVoidFunctionCall, RawUnclockedNonVoidFunctionCall}
+import chisel3.util.{Counter, HasExtModuleInline, RegEnable, Valid}
+import chisel3.layers.Verification.Assume
+import chisel3.ltl.AssumeProperty
+
+object GCDFormalParameter {
+  implicit def rwP: upickle.default.ReadWriter[GCDFormalParameter] =
+    upickle.default.macroRW
+}
+
+/** Parameter of [[GCD]]. */
+case class GCDFormalParameter(gcdParameter: GCDParameter) extends SerializableModuleParameter {}
+
+@instantiable
+class GCDFormalOM(parameter: GCDFormalParameter) extends Class {
+  val gcd = IO(Output(Property[AnyClassType]()))
+  @public
+  val gcdIn = IO(Input(Property[AnyClassType]()))
+  gcd := gcdIn
+}
+
+class GCDFormalInterface(parameter: GCDFormalParameter) extends Bundle {
+  val clock = Input(Clock())
+  val reset = Input(if (parameter.gcdParameter.useAsyncReset) AsyncReset() else Bool())
+  val input = Flipped(Valid(new Bundle {
+    val x = UInt(parameter.gcdParameter.width.W)
+    val y = UInt(parameter.gcdParameter.width.W)
+  }))
+  val om = Output(Property[AnyClassType]())
+}
+
+@instantiable
+class GCDFormal(val parameter: GCDFormalParameter)
+    extends FixedIORawModule(new GCDFormalInterface(parameter))
+    with SerializableModule[GCDFormalParameter]
+    with ImplicitClock
+    with ImplicitReset {
+  layer.enable(layers.Verification)
+  override protected def implicitClock: Clock = io.clock
+  override protected def implicitReset: Reset = io.reset
+  // Instantiate DUT.
+  val dut: Instance[GCD] = Instantiate(new GCD(parameter.gcdParameter))
+  // Instantiate OM
+  val omInstance = Instantiate(new GCDFormalOM(parameter))
+  io.om := omInstance.getPropertyReference.asAnyClassType
+  omInstance.gcdIn := dut.io.om
+
+  dut.io.clock := implicitClock
+  dut.io.reset := implicitReset
+
+  // 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 inputNotValid: Sequence = dut.io.input.ready && !dut.io.input.valid
+
+  dut.io.input.bits := io.input.bits
+  dut.io.input.valid := io.input.valid
+
+  val x = RegEnable(dut.io.input.bits.x, dut.io.input.fire)
+  val y = RegEnable(dut.io.input.bits.y, dut.io.input.fire)
+  val result = dut.io.output.bits
+
+  AssumeProperty(
+    inputNotValid |=> not(inputFire),
+    label = Some("GCD_ASSUMPTION_INPUT_NOT_VALID")
+  )
+  AssumeProperty(
+    dut.io.input.bits.x > 0.U && dut.io.input.bits.y > 0.U,
+    label = Some("GCD_ASSUMPTION_INPUT_POSITIVE")
+  )
+
+  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 |-> x % result === 0.U && y % result === 0.U,
+    label = Some("GCD_RESULT_IS_CORRECT")
+  )
+
+  CoverProperty(
+    inputNotValid,
+    label = Some("GCD_COVER_BACK_PRESSURE")
+  )
+}

templates/chisel/nix/gcd/default.nix

@@ -6,6 +6,7 @@ lib.makeScope newScope (scope:
 let
   designTarget = "GCD";
   tbTarget = "GCDTestBench";
+  formalTarget = "GCDFormal";
   dpiLibName = "gcdemu";
 in
 {
@@ -49,6 +50,15 @@ in
     dpi-lib = scope.vcs.dpi-lib.override { enable-trace = true; };
   };
 
+  # Formal
+  formal-compiled = scope.callPackage ./gcd.nix { target = formalTarget; };
+  formal-elaborate = scope.callPackage ./elaborate.nix {
+    elaborator = scope.formal-compiled.elaborator;
+  };
+  formal-mlirbc =
+    scope.callPackage ./mlirbc.nix { elaborate = scope.formal-elaborate; };
+  formal-rtl = scope.callPackage ./rtl.nix { mlirbc = scope.formal-mlirbc; };
+
   # TODO: designConfig should be read from OM
   tbConfig = with builtins;
     fromJSON (readFile ./../../configs/${tbTarget}Main.json);

templates/chisel/scripts/formal/FPV.tcl

@@ -0,0 +1,31 @@
+# Make sure you have run the nix build command to build the formal results
+# Now the result/ directory should contain the GCD.sv and GCDFormal.sv
+
+clear -all
+
+# Analyze design under verification files
+set RESULT_PATH ./result
+
+# Analyze source files and property files
+analyze -sv12 \
+  ${RESULT_PATH}/GCD.sv \
+  ${RESULT_PATH}/GCDFormal.sv
+
+# Elaborate design and properties
+elaborate -top GCDFormal
+
+# Set up Clocks and Resets
+clock clock
+reset reset
+
+# Get design information to check general complexity
+get_design_info
+
+# Prove properties
+# 1st pass: Quick validation of properties with default engines
+set_max_trace_length 100
+prove -all
+
+# Report proof results
+report
+