Skip to content

Commit

Permalink
[test] Add Verilog test of inline emission, NFC (#4548)
Browse files Browse the repository at this point in the history
* [test] Add Verilog test of inline emission, NFC

Add an integration test of SystemVerilog generation for inline layers.
This relies on new support in firtool 1.97.0 which adds support for
compiling this feature.  Previous versions of firtool could parse inline
layers, but error when compiling them.

* [test] Update btor2 emission test

There was a change in the btor2 emission upstream.  Update the test to
match the new emission.

I did not validate the correctness of this change.

Signed-off-by: Schuyler Eldridge <[email protected]>
  • Loading branch information
seldridge authored and chiselbot committed Dec 8, 2024
1 parent 5871a65 commit defa010
Show file tree
Hide file tree
Showing 2 changed files with 68 additions and 32 deletions.
50 changes: 43 additions & 7 deletions src/test/scala/chiselTests/LayerSpec.scala
Original file line number Diff line number Diff line change
Expand Up @@ -5,6 +5,7 @@ package chiselTests
import chisel3._
import chisel3.experimental.hierarchy.core.{Definition, Instance}
import chisel3.experimental.hierarchy.instantiable
import chisel3.ltl.AssertProperty
import chisel3.probe.{define, Probe, ProbeValue}
import chiselTests.{ChiselFlatSpec, FileCheck, Utils}
import java.nio.file.{FileSystems, Paths}
Expand Down Expand Up @@ -380,25 +381,60 @@ class LayerSpec extends ChiselFlatSpec with Utils with FileCheck {
)
}

"Inline layers" should "generated expected FIRRTL" in {
object A extends layer.Layer(layer.LayerConfig.Inline) {
object B extends layer.Layer(layer.LayerConfig.Inline)
"Inline layers" should "generate expected FIRRTL and SystemVerilog" in {
object A extends layer.Layer(layer.LayerConfig.Extract()) {
object B extends layer.Layer(layer.LayerConfig.Inline) {
object C extends layer.Layer(layer.LayerConfig.Inline)
}
}

class Foo extends RawModule {
class Foo extends Module {
val a = IO(Input(UInt(2.W)))

layer.block(A) {
layer.block(A.B) {}
AssertProperty(a > 0.U, "foo")
layer.block(A.B) {
AssertProperty(a > 1.U, "bar")
layer.block(A.B.C) {
AssertProperty(a > 2.U, "baz")
}
}
}
}

info("FIRRTL okay")
generateFirrtlAndFileCheck(new Foo) {
"""|CHECK: layer A, inline :
"""|CHECK: layer A, bind
|CHECK-NEXT: layer B, inline :
|CHECK-NEXT: layer C, inline :
|""".stripMargin
}

info("SystemVerilog okay")
val verilog = ChiselStage.emitSystemVerilog(
new Foo,
firtoolOpts = Array(
"-disable-all-randomization",
"-enable-layers=Verification,Verification.Assert,Verification.Assume,Verification.Cover"
)
)
fileCheckString(verilog) {
"""|CHECK: module Foo(
|CHECK-NOT: assert property
|
|CHECK: module Foo_A(
|CHECK-NOT: `ifdef
|CHECK: foo: assert property
|CHECK: `ifdef A_B
|CHECK-NEXT: bar: assert property
|CHECK-NEXT: `ifdef A_B_C
|CHECK-NEXT: baz: assert property
|CHECK-NEXT: `endif
|CHECK-NEXT: `endif""".stripMargin
}
}

"Inline layers" should "be ignored when choosing default output directories" in {
they should "be ignored when choosing default output directories" in {
object LayerWithDefaultOutputDir extends layer.Layer(layer.LayerConfig.Extract()) {
object InlineSublayer extends layer.Layer(layer.LayerConfig.Inline) {
object SublayerWithDefaultOutputDir extends layer.Layer(layer.LayerConfig.Extract()) {}
Expand Down
50 changes: 25 additions & 25 deletions src/test/scala/circtTests/stage/ChiselStageSpec.scala
Original file line number Diff line number Diff line change
Expand Up @@ -1200,31 +1200,31 @@ class ChiselStageSpec extends AnyFunSpec with Matchers with chiselTests.Utils {
new Counter,
firtoolOpts = Array("-enable-layers=Verification,Verification.Assert,Verification.Assume,Verification.Cover")
)
btor2 should include("""1 sort bitvec 1
|2 input 1 reset
|3 sort bitvec 32
|4 state 3 count
|5 state 1 hbr
|6 constd 1 0
|7 init 1 5 6
|8 constd 3 43
|9 constd 3 1
|10 constd 3 42
|11 constd 3 0
|12 eq 1 4 10
|13 add 3 4 9
|14 ite 3 12 11 13
|15 ult 1 4 8
|16 constd 1 -1
|17 or 1 2 5
|18 xor 1 2 16
|19 and 1 5 18
|20 implies 1 19 15
|21 not 1 20
|22 bad 21
|23 ite 3 2 11 14
|24 next 3 4 23
|25 next 1 5 17""".stripMargin)
btor2 should include("""|1 sort bitvec 1
|2 input 1 reset
|3 sort bitvec 32
|4 state 3 count
|5 constd 1 0
|6 state 1 hbr
|7 init 1 6 5
|8 constd 3 43
|9 constd 3 1
|10 constd 3 42
|11 constd 3 0
|12 eq 1 4 10
|13 add 3 4 9
|14 ite 3 12 11 13
|15 ult 1 4 8
|16 constd 1 -1
|17 or 1 2 6
|18 xor 1 2 16
|19 and 1 6 18
|20 implies 1 19 15
|21 not 1 20
|22 bad 21
|23 ite 3 2 11 14
|24 next 3 4 23
|25 next 1 6 17""".stripMargin)
}

it("""should error if give a "--target-directory" option""") {
Expand Down

0 comments on commit defa010

Please sign in to comment.