diff --git a/.github/workflows/main.yml b/.github/workflows/main.yml index 134810b..1b31e22 100644 --- a/.github/workflows/main.yml +++ b/.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.jg-fpv' --impure diff --git a/readme.md b/readme.md index c1654ce..af62ab8 100644 --- a/readme.md +++ b/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 +* jg-fpv: Formal Property 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 property verification. Then you can run: + +```bash +nix build '.#gcd.jg-fpv' --impure +``` + +and the 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 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/GCD.scala b/templates/chisel/gcd/src/GCD.scala index b11c5e8..d35991d 100644 --- a/templates/chisel/gcd/src/GCD.scala +++ b/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 - ) -} diff --git a/templates/chisel/gcd/src/GCDFormal.scala b/templates/chisel/gcd/src/GCDFormal.scala new file mode 100644 index 0000000..df3dcc8 --- /dev/null +++ b/templates/chisel/gcd/src/GCDFormal.scala @@ -0,0 +1,99 @@ +// 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 + + AssumeProperty( + inputNotValid |=> not(inputFire), + label = Some("GCD_ASSUMPTION_INPUT_NOT_VALID") + ) + AssumeProperty( + dut.io.input.bits.x === 4.U && dut.io.input.bits.y === 6.U, + label = Some("GCD_ASSUMPTION_INPUT_4_6") + ) + + 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 |-> dut.io.output.bits === 2.U, + label = Some("GCD_RESULT_IS_CORRECT") + ) + + CoverProperty( + inputNotValid, + label = Some("GCD_COVER_BACK_PRESSURE") + ) +} diff --git a/templates/chisel/gcd/src/GCDTestBench.scala b/templates/chisel/gcd/src/GCDTestBench.scala new file mode 100644 index 0000000..ce5191a --- /dev/null +++ b/templates/chisel/gcd/src/GCDTestBench.scala @@ -0,0 +1,198 @@ +// 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} + +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 + ) +} diff --git a/templates/chisel/nix/gcd/default.nix b/templates/chisel/nix/gcd/default.nix index c4bc76f..2c53907 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,20 @@ 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; + }; + jg-fpv = scope.callPackage ./jg-fpv.nix { + rtl = scope.formal-rtl; + }; + # TODO: designConfig should be read from OM tbConfig = with builtins; fromJSON (readFile ./../../configs/${tbTarget}Main.json); diff --git a/templates/chisel/nix/gcd/jg-fpv.nix b/templates/chisel/nix/gcd/jg-fpv.nix new file mode 100644 index 0000000..b137a1e --- /dev/null +++ b/templates/chisel/nix/gcd/jg-fpv.nix @@ -0,0 +1,51 @@ +# SPDX-License-Identifier: Apache-2.0 +# SPDX-FileCopyrightText: 2024 Jiuyang Liu + +{ stdenvNoCC +, rtl +, cds-fhs-env +}: + +stdenvNoCC.mkDerivation { + name = "jg-fpv"; + + # Add "sandbox = relaxed" into /etc/nix/nix.conf, and run `systemctl restart nix-daemon` + # + # run nix build with "--impure" flag to build this package without chroot + # require license + __noChroot = true; + dontPatchELF = true; + + src = rtl; + + passthru = { + inherit rtl; + }; + + shellHook = '' + echo "[nix] entering fhs env" + ${cds-fhs-env}/bin/cds-fhs-env + ''; + + buildPhase = '' + runHook preBuild + + echo "[nix] running Jasper" + fhsBash=${cds-fhs-env}/bin/cds-fhs-env + "$fhsBash" -c "jg -batch ${./scripts/FPV.tcl}" + + runHook postBuild + ''; + + installPhase = '' + runHook preInstall + + mkdir -p $out + + cp report.txt $out + cp -r jgproject $out + + runHook postInstall + ''; + +} diff --git a/templates/chisel/nix/gcd/scripts/FPV.tcl b/templates/chisel/nix/gcd/scripts/FPV.tcl new file mode 100644 index 0000000..b167b91 --- /dev/null +++ b/templates/chisel/nix/gcd/scripts/FPV.tcl @@ -0,0 +1,39 @@ +# 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 . + +# 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 -file report.txt + +set failed_properties [get_property_list -include {status {cex unreachable}}] +set length [llength $failed_properties] +if { $length > 0 } { + puts "There are $length failed properties!" + exit 1 +} else { + puts "All properties passed!" + exit 0 +} diff --git a/templates/chisel/nix/gcd/vcs-wrapper.sh b/templates/chisel/nix/gcd/scripts/vcs-wrapper.sh similarity index 100% rename from templates/chisel/nix/gcd/vcs-wrapper.sh rename to templates/chisel/nix/gcd/scripts/vcs-wrapper.sh diff --git a/templates/chisel/nix/gcd/vcs.nix b/templates/chisel/nix/gcd/vcs.nix index 40bb5c2..f951da4 100644 --- a/templates/chisel/nix/gcd/vcs.nix +++ b/templates/chisel/nix/gcd/vcs.nix @@ -79,7 +79,7 @@ stdenv.mkDerivation (finalAttr: { cp ${binName} $out/lib cp -r ${binName}.daidir $out/lib - substitute ${./vcs-wrapper.sh} $out/bin/${binName} \ + substitute ${./scripts/vcs-wrapper.sh} $out/bin/${binName} \ --subst-var-by shell "${bash}/bin/bash" \ --subst-var-by dateBin "$(command -v date)" \ --subst-var-by vcsSimBin "$out/lib/${binName}" \ diff --git a/templates/chisel/nix/overlay.nix b/templates/chisel/nix/overlay.nix index 55a1ee4..c5f2512 100644 --- a/templates/chisel/nix/overlay.nix +++ b/templates/chisel/nix/overlay.nix @@ -21,6 +21,14 @@ final: prev: { assert final.lib.assertMsg (final.snpslmdLicenseFile != "") "You forget to set SNPSLMD_LICENSE_FILE or the '--impure' flag"; final.callPackage ./pkgs/vcs-fhs-env.nix { }; + jasperHome = builtins.getEnv "JASPER_HOME"; + cdsLicenseFile = builtins.getEnv "CDS_LIC_FILE"; + cds-fhs-env = assert final.lib.assertMsg (final.jasperHome != "") + "You forget to set JASPER_HOME or the '--impure' flag"; + assert final.lib.assertMsg (final.cdsLicenseFile != "") + "You forget to set CDS_LIC_FILE or the '--impure' flag"; + final.callPackage ./pkgs/cds-fhs-env.nix { }; + projectDependencies = final.callPackage ./pkgs/project-dependencies.nix { }; diff --git a/templates/chisel/nix/pkgs/cds-fhs-env.nix b/templates/chisel/nix/pkgs/cds-fhs-env.nix new file mode 100644 index 0000000..af95332 --- /dev/null +++ b/templates/chisel/nix/pkgs/cds-fhs-env.nix @@ -0,0 +1,90 @@ +# SPDX-License-Identifier: Apache-2.0 +# SPDX-FileCopyrightText: 2024 Jiuyang Liu +{ jasperHome +, cdsLicenseFile +, fetchFromGitHub +}: +let + nixpkgsSrcs = fetchFromGitHub { + owner = "NixOS"; + repo = "nixpkgs"; + "rev" = "c374d94f1536013ca8e92341b540eba4c22f9c62"; + "hash" = "sha256-Z/ELQhrSd7bMzTO8r7NZgi9g5emh+aRKoCdaAv5fiO0="; + }; + + # The cds we have only support x86-64_linux + lockedPkgs = import nixpkgsSrcs { system = "x86_64-linux"; }; +in +lockedPkgs.buildFHSEnv { + name = "cds-fhs-env"; + + profile = '' + [ ! -e "${jasperHome}" ] && echo "env JASPER_HOME not set" && exit 1 + [ ! -d "${jasperHome}" ] && echo "JASPER_HOME not accessible" && exit 1 + [ -z "${cdsLicenseFile}" ] && echo "env CDS_LIC_FILE not set" && exit 1 + export JASPER_HOME=${jasperHome} + export CDS_LIC_FILE=${cdsLicenseFile} + export PATH=$JASPER_HOME/bin:$PATH + export _oldCdsEnvPath="$PATH" + preHook() { + PATH="$PATH:$_oldCdsEnvPath" + } + export -f preHook + ''; + targetPkgs = (ps: with ps; [ + dejavu_fonts + libGL + util-linux + libxcrypt-legacy + coreutils-full + ncurses5 + gmp5 + bzip2 + glib + bc + time + elfutils + ncurses5 + e2fsprogs + cyrus_sasl + expat + sqlite + nssmdns + (libkrb5.overrideAttrs rec { + version = "1.18.2"; + src = fetchurl { + url = "https://kerberos.org/dist/krb5/${lib.versions.majorMinor version}/krb5-${version}.tar.gz"; + hash = "sha256-xuTJ7BqYFBw/XWbd8aE1VJBQyfq06aRiDumyIIWHOuA="; + }; + sourceRoot = "krb5-${version}/src"; + }) + (gnugrep.overrideAttrs rec { + version = "3.1"; + doCheck = false; + src = fetchurl { + url = "mirror://gnu/grep/grep-${version}.tar.xz"; + hash = "sha256-22JcerO7PudXs5JqXPqNnhw5ka0kcHqD3eil7yv3oH4="; + }; + }) + keyutils + graphite2 + libpulseaudio + libxml2 + gcc + gnumake + xorg.libX11 + xorg.libXft + xorg.libXScrnSaver + xorg.libXext + xorg.libxcb + xorg.libXau + xorg.libXrender + xorg.libXcomposite + xorg.libXi + xorg.libSM + xorg.libICE + fontconfig + freetype + zlib + ]); +}