Problems generating Verilog with Chisel 5.0.0 and firtool 1.48.0

[Øyvind Harboe]

I'm having problems generating Verilog because there are some missing annotations for formal verification.

Is there a workaround for this? Can I tell firtool to ignore this and generate Verilog anyway?

// Verilog generation with firtool fails on 1.48.0

//

// when(past(!isActive && io.activate)) {

// assert(isActive)

// }

when(RegNext(!isActive && io.activate)) {

assert(isActive)

}

[error] <stdin>:2:1: error: Unhandled annotation: {anno = {target = {circuit = "FoobarUnit", component = [], module = "FoobarUnit", path = [], ref = "out"}}, class = "chiseltest.simulator.Firrtl2AnnotationWrapper"}

new circt.stage.ChiselStage()

.execute(

args,

Seq(

circt.stage.CIRCTTargetAnnotation(circt.stage.CIRCTTarget.Verilog),

ChiselGeneratorAnnotation(() => new FoobarUnit()),

circt.stage.FirtoolOption("--lowering-options=disallowPackedArrays,disallowLocalVariables"),

circt.stage.FirtoolOption("--split-verilog"),

circt.stage.FirtoolOption("--dedup"),

circt.stage.FirtoolOption("--strip-debug-info"),

circt.stage.FirtoolOption("--extract-test-code"),

circt.stage.FirtoolOption("-o=" + args(0))

)

)

[Øyvind Harboe]

Answering myself :-)

circt.stage.FirtoolOption("--disable-annotation-unknown"),

[Øyvind Harboe]

Next problem... This used to work in 1.37.0, but fails now...

[error]   val blah = WireInit(foo.bar(pointer))
[error]                      ^
[error] src/main/scala/ascenium/control/FooBar.scala:434:22: note: see current operation: %96 = "hw.array_create"(%75, %73, %71, %69) : (i64, i64, i64, i64) -> !hw.array<4xi64>

class Foo extends Bundle {

...

val bar = Vec(8, UInt(64.W))

...

}

val foo = Reg(new Foo)

val pointer = Wire(UInt(3.W))

val blah = WireInit(foo.bar(pointer))

[Schuyler Eldridge]

Re: ChiselTest annotations. Yep, you can tell `firtool` to ignore any
annotations it doesn't recognize with: `-disable-annotation-unknown`.
The motivation for this behavior is that if an annotation is truly
unprocessed, then it's safer to assume that this is going to result in
incorrect behavior than to assume everything is fine. If you know
certain annotations are safe to ignore, then go for it.

You may want to take a look at Fabian's new linear-temporal-logic
package for Chisel 6.0.0-M2+. This lets you directly encode and emit
SVA-style sequences. The above can be rewritten as something like:

```
//> using scala "2.13.10"
//> using lib "org.chipsalliance::chisel::6.0.0-M2"
//> using plugin "org.chipsalliance:::chisel-plugin::6.0.0-M2"
//> using options "-unchecked", "-deprecation",
"-language:reflectiveCalls", "-feature", "-Xcheckinit",
"-Ywarn-dead-code", "-Ywarn-unused", "-Ymacro-annotations"

import chisel3._
import chisel3.ltl.{AssertProperty, Delay, Sequence}
import chisel3.ltl.Sequence.BoolSequence
import circt.stage.ChiselStage

class Foo extends RawModule {
val a, b = IO(Input(Bool()))

AssertProperty(Sequence(Delay(), !a && b))
}

object Main extends App {
println(
ChiselStage.emitSystemVerilog(
new Foo,
firtoolOpts = Array("-strip-debug-info")
)
)
}
```

To produce:
```
module Foo(
input a,
b
);

assert property (##1 ~a & b);
endmodule
```

For the second error, do you have any more context for the error
message that you can provide? There should be an error message before
that is missing which may help figure out what's going on.

> --
> You received this message because you are subscribed to the Google Groups "chisel-users" group.
> To unsubscribe from this group and stop receiving emails from it, send an email to chisel-users...@googlegroups.com.
> To view this discussion on the web visit https://groups.google.com/d/msgid/chisel-users/52e5a3b0-caf2-4188-9d18-d2bdbf3a81b7n%40googlegroups.com.

[Øyvind Harboe]

Thanks!

For the second error, I think I'm running into some sort of edge condition...

Output, only slightly redacted:

[no errors or warnings up until this point]

[info] ======== Starting circt.stage.phases.CIRCT ========
[info] Running CIRCT: 'firtool -format=fir -warn-on-unprocessed-annotations -dedup -output-annotation-file circt.anno.json --lowering-options=disallowPackedArrays,disallowLocalVariables --split-verilog --dedup --strip-debug-info --extract-test-code -o=xxx -verbose-pass-executions -annotation-file xxx.anno.json < $input'
[error] Exception in thread "main" circt.stage.phases.Exceptions$FirtoolNonZeroExitCode: firtool returned a non-zero exit code. Note that this version of Chisel (5.0.0) was published against firtool version 1.40.0.

[error] ExitCode:

[error] 1
[error] STDOUT:
[error] STDERR:
[error] [firtool] Running fir parser
[error] [firtool] -- Done in 0.958 sec
[error] [firtool] Running "firrtl.circuit(firrtl-lower-open-aggs,firrtl-lower-annotations{disable-annotation-classless=false disable-annotation-unknown=true no-ref-type-ports=false},firrtl-lower-intrinsics,firrtl-inject-dut-hier,firrtl.module(firrtl-drop-names{preserve-values=named},cse,firrtl-lower-chirrtl,firrtl-lower-matches),firrtl-infer-widths,firrtl-mem-to-reg-of-vec{ignore-read-enable-mem=false repl-seq-mem=false},firrtl-infer-resets,any(firrtl-drop-const),firrtl-dedup,firrtl-dft,firrtl.module(firrtl-flatten-memory),firrtl-lower-types{flatten-mem=false preserve-aggregate=1d-vec preserve-memories=1d-vec},firrtl.module(firrtl-expand-whens,firrtl-sfc-compat),firrtl-inliner,firrtl.module(firrtl-randomize-register-init),firrtl-check-comb-loops,firrtl.module(canonicalize{  max-iterations=10 max-num-rewrites=-1 region-simplify=false test-convergence=false top-down=true},firrtl-infer-rw),firrtl-prefix-modules,firrtl-imconstprop,firrtl-add-seqmem-ports)"
[error] [firtool]   Running "firrtl-lower-open-aggs"
[error] [firtool]   -- Done in 0.260 sec
[error] [firtool]   Running "firrtl-lower-annotations{disable-annotation-classless=false disable-annotation-unknown=true no-ref-type-ports=false}"
[error] [firtool]   -- Done in 0.289 sec
[error] [firtool]   Running "firrtl-lower-intrinsics"
[error] [firtool]   -- Done in 0.016 sec
[error] [firtool]   Running "firrtl-inject-dut-hier"
[error] [firtool]   -- Done in 0.000 sec
[error] [firtool]   Running "firrtl.module(firrtl-drop-names{preserve-values=named},cse,firrtl-lower-chirrtl,firrtl-lower-matches)"
[error] [firtool]   -- Done in 0.690 sec
[error] [firtool]   Running "firrtl-infer-widths"
[error] [firtool]   -- Done in 0.489 sec
[error] [firtool]   Running "firrtl-mem-to-reg-of-vec{ignore-read-enable-mem=false repl-seq-mem=false}"
[error] [firtool]   -- Done in 0.231 sec
[error] [firtool]   Running "firrtl-infer-resets"
[error] [firtool]   -- Done in 0.455 sec
[error] [firtool]   Running "any(firrtl-drop-const)"
[error] [firtool]   -- Done in 0.253 sec
[error] [firtool]   Running "firrtl-dedup"
[error] [firtool]   -- Done in 0.761 sec
[error] [firtool]   Running "firrtl-dft"
[error] [firtool]   -- Done in 0.031 sec
[error] [firtool]   Running "firrtl.module(firrtl-flatten-memory)"
[error] [firtool]   -- Done in 0.130 sec
[error] [firtool]   Running "firrtl-lower-types{flatten-mem=false preserve-aggregate=1d-vec preserve-memories=1d-vec}"
[error] [firtool]   -- Done in 0.247 sec
[error] [firtool]   Running "firrtl.module(firrtl-expand-whens,firrtl-sfc-compat)"
[error] [firtool]   -- Done in 0.161 sec
[error] [firtool]   Running "firrtl-inliner"
[error] [firtool]   -- Done in 0.155 sec
[error] [firtool]   Running "firrtl.module(firrtl-randomize-register-init)"
[error] [firtool]   -- Done in 0.094 sec
[error] [firtool]   Running "firrtl-check-comb-loops"
[error] [firtool]   -- Done in 7.754 sec
[error] [firtool]   Running "firrtl.module(canonicalize{  max-iterations=10 max-num-rewrites=-1 region-simplify=false test-convergence=false top-down=true},firrtl-infer-rw)"
[error] [firtool]   -- Done in 0.253 sec
[error] [firtool]   Running "firrtl-prefix-modules"
[error] [firtool]   -- Done in 0.052 sec
[error] [firtool]   Running "firrtl-imconstprop"
[error] [firtool]   -- Done in 0.431 sec
[error] [firtool]   Running "firrtl-add-seqmem-ports"
[error] [firtool]   -- Done in 0.006 sec
[error] [firtool] -- Done in 12.758 sec
[error] [firtool] Running "firrtl-emit-metadata{repl-seq-mem=false repl-seq-mem-file=}"
[error] [firtool] -- Done in 0.075 sec
[error] [firtool] Running "firrtl.circuit(firrtl-extract-instances,firrtl-grand-central{instantiate-companion-only=false},firrtl-blackbox-reader{input-prefix=},symbol-dce)"
[error] [firtool]   Running "firrtl-extract-instances"
[error] [firtool]   -- Done in 0.021 sec
[error] [firtool]   Running "firrtl-grand-central{instantiate-companion-only=false}"
[error] [firtool]   -- Done in 0.000 sec
[error] [firtool]   Running "firrtl-blackbox-reader{input-prefix=}"
[error] [firtool]   -- Done in 0.075 sec
[error] [firtool]   Running "symbol-dce"
[error] [firtool]   -- Done in 0.177 sec
[error] [firtool] -- Done in 0.273 sec
[error] [firtool] Running "firrtl-inner-symbol-dce"
[error] [firtool] -- Done in 0.145 sec
[error] [firtool] Running "firrtl.circuit(firrtl.module(canonicalize{  max-iterations=10 max-num-rewrites=-1 region-simplify=false test-convergence=false top-down=true},firrtl-register-optimizer))"
[error] [firtool]   Running "firrtl.module(canonicalize{  max-iterations=10 max-num-rewrites=-1 region-simplify=false test-convergence=false top-down=true},firrtl-register-optimizer)"
[error] [firtool]   -- Done in 0.121 sec
[error] [firtool] -- Done in 0.121 sec
[error] [firtool] Running "firrtl-imdeadcodeelim"
[error] [firtool] -- Done in 0.378 sec
[error] [firtool] Running "firrtl.circuit(firrtl-emit-omir{file=},firrtl.module(merge-connections{aggressive-merging=true},vectorization),firrtl-resolve-traces{file=circt.anno.json},firrtl-lower-xmr)"
[error] [firtool]   Running "firrtl-emit-omir{file=}"
[error] [firtool]   -- Done in 0.000 sec
[error] [firtool]   Running "firrtl.module(merge-connections{aggressive-merging=true},vectorization)"
[error] [firtool]   -- Done in 0.089 sec
[error] [firtool]   Running "firrtl-resolve-traces{file=circt.anno.json}"
[error] [firtool]   -- Done in 0.017 sec
[error] [firtool]   Running "firrtl-lower-xmr"
[error] [firtool]   -- Done in 0.076 sec
[error] [firtool] -- Done in 0.183 sec
[error] [firtool] Running "lower-firrtl-to-hw{disable-mem-randomization=false disable-reg-randomization=false emit-chisel-asserts-as-sva=false warn-on-unprocessed-annotations=true}"
[error] [firtool] -- Done in 0.128 sec
[error] [firtool] Running "hw.module(cse,canonicalize{  max-iterations=10 max-num-rewrites=-1 region-simplify=false test-convergence=false top-down=true})"
[error] [firtool] -- Done in 0.092 sec
[error] [firtool] Running "sv-extract-test-code{disable-instance-extraction=false disable-module-inlining=false disable-register-extraction=false}"
[error] [firtool] -- Done in 0.068 sec
[error] [firtool] Running "externalize-clock-gate{enable=en input=in instance-name=ckg name=EICG_wrapper output=out test-enable=test_en}"
[error] [firtool] -- Done in 0.002 sec
[error] [firtool] Running "hw.module(lower-seq-firrtl-to-sv{disable-reg-randomization=false emit-separate-always-blocks=false})"
[error] [firtool] -- Done in 0.014 sec
[error] [firtool] Running "lower-seq-firmem"
[error] [firtool] -- Done in 0.014 sec
[error] [firtool] Running "hw-memory-sim{add-mux-pragmas=false add-vivado-ram-address-conflict-synthesis-bug-workaround=false disable-mem-randomization=false disable-reg-randomization=false ignore-read-enable=false repl-seq-mem=false}"
[error] [firtool] -- Done in 0.011 sec
[error] [firtool] Running "hw.module(cse,canonicalize{  max-iterations=10 max-num-rewrites=-1 region-simplify=false test-convergence=false top-down=true},cse,hw-cleanup{merge-always-blocks=true})"
[error] [firtool] -- Done in 0.034 sec
[error] [firtool] Running "hw.module(hw-legalize-modules,prettify-verilog)"

[error] val blah = WireInit(foo.bar(pointer))

[error] ^
[error] FooBar.scala:434:22: note: see current operation: %96 = "hw.array_create"(%75, %73, %71, %69) : (i64, i64, i64, i64) -> !hw.array<4xi64>

[Schuyler Eldridge]

(After some offline debugging and help from others on the CIRCT team:)
The issue here is that the `-lowering-options=disallowPackedArrays`
can cause the `hw-legalize-modules` pass to fail after some
canonicalizers were added that create array concatenation and slicing
operations. The pass doesn't handle these in `disallowPackedArrays`
mode. This has been observed on some open-source designs from
Chipyard.

A tracking issue is here: https://github.com/llvm/circt/issues/5355

> To view this discussion on the web visit https://groups.google.com/d/msgid/chisel-users/e6a0987f-ca1a-429f-9805-40bd40cfc6f5n%40googlegroups.com.