From fc84bcd80fb19295aee9e4073438773f8621ca2d Mon Sep 17 00:00:00 2001 From: Clo91eaf Date: Sat, 14 Sep 2024 23:28:58 +0800 Subject: [PATCH] [formal] add Formal TestBench --- templates/chisel/configs/GCDFormalMain.json | 6 + .../chisel/elaborator/src/GCDFormal.scala | 36 ++++++ templates/chisel/gcd/src/GCDFormal.scala | 103 ++++++++++++++++++ templates/chisel/nix/gcd/default.nix | 10 ++ templates/chisel/scripts/formal/FPV.tcl | 31 ++++++ 5 files changed, 186 insertions(+) create mode 100644 templates/chisel/configs/GCDFormalMain.json create mode 100644 templates/chisel/elaborator/src/GCDFormal.scala create mode 100644 templates/chisel/gcd/src/GCDFormal.scala create mode 100644 templates/chisel/scripts/formal/FPV.tcl diff --git a/templates/chisel/configs/GCDFormalMain.json b/templates/chisel/configs/GCDFormalMain.json new file mode 100644 index 0000000..832f92b --- /dev/null +++ b/templates/chisel/configs/GCDFormalMain.json @@ -0,0 +1,6 @@ +{ + "gcdParameter": { + "width": 16, + "useAsyncReset": false + } +} diff --git a/templates/chisel/elaborator/src/GCDFormal.scala b/templates/chisel/elaborator/src/GCDFormal.scala new file mode 100644 index 0000000..0488160 --- /dev/null +++ b/templates/chisel/elaborator/src/GCDFormal.scala @@ -0,0 +1,36 @@ +// SPDX-License-Identifier: Unlicense +// SPDX-FileCopyrightText: 2024 Jiuyang Liu +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) +} diff --git a/templates/chisel/gcd/src/GCDFormal.scala b/templates/chisel/gcd/src/GCDFormal.scala new file mode 100644 index 0000000..cff2cd2 --- /dev/null +++ b/templates/chisel/gcd/src/GCDFormal.scala @@ -0,0 +1,103 @@ +// SPDX-License-Identifier: Unlicense +// SPDX-FileCopyrightText: 2024 Jiuyang Liu + +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") + ) +} diff --git a/templates/chisel/nix/gcd/default.nix b/templates/chisel/nix/gcd/default.nix index c4bc76f..dfb1c79 100644 --- a/templates/chisel/nix/gcd/default.nix +++ b/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); diff --git a/templates/chisel/scripts/formal/FPV.tcl b/templates/chisel/scripts/formal/FPV.tcl new file mode 100644 index 0000000..e146927 --- /dev/null +++ b/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 +