Generate verilog formal code only in systemVerilog output

[Martoni]

As comment say :

------------------------------------------------------------------------------
Warning: 5 verification statements (assert, assume or cover) were removed when compiling to Verilog because the basic Verilog standard does not support them. If this was not intended, compile to System Verilog instead using the `-X sverilog` compiler flag.
------------------------------------------------------------------------------

It's impossible to generate verifications statement in standard verilog file *.v. So, is it possible to generate formal specific code only for System Verilog generated code *.sv ?

Because code added by Formal module generate some verilator compilation error in my simulation, then I have to comment the trait (// with Formal { ) each time I want to launch simulation.

> generate systemVerilog for formal
[info] [0.000] Elaborating design...
[info] [0.025] Done elaborating.
Use of CompilerAnnotation is deprecated. Ignoring CompilerAnnotation(firrtl.SystemVerilogCompiler@24c37598)
[success] Total time: 13 s, completed Oct 28, 2020, 7:00:14 AM
echo "\`timescale "1ns"/"1ns"" > /media/stockage/projets/GbVga/cocotb/test_gbwrite/GbWrite_withtp.v
echo "" >> /media/stockage/projets/GbVga/cocotb/test_gbwrite/GbWrite_withtp.v
cat /media/stockage/projets/GbVga/cocotb/test_gbwrite/../../chisel/GbWrite.v >> /media/stockage/projets/GbVga/cocotb/test_gbwrite/GbWrite_withtp.v
verilator -cc --exe -Mdir sim_build -DCOCOTB_SIM=1 --top-module GbWrite -DCOCOTB_VERILATOR --vpi --public-flat-rw --prefix Vtop -o GbWrite -LDFLAGS "-Wl,-rpath,/home/fabien/pyenv/pyenv37/lib/python3.7/site-packages/cocotb/libs -L/home/fabien/pyenv/pyenv37/lib/python3.7/site-packages/cocotb/libs -lcocotbvpi_verilator -lgpi -lcocotb -lgpilog -lcocotbutils" --trace --trace-structs /media/stockage/projets/GbVga/cocotb/test_gbwrite/GbWrite_withtp.v /home/fabien/pyenv/pyenv37/lib/python3.7/site-packages/cocotb/share/lib/verilator/verilator.cpp
%Error-TIMESCALEMOD: /media/stockage/projets/GbVga/cocotb/test_gbwrite/GbWrite_withtp.v:47:16: Timescale missing on this module as other modules have it (IEEE 1800-2017 3.14.2.2)
                     /media/stockage/projets/GbVga/cocotb/test_gbwrite/GbWrite_withtp.v:3:8: ... Location of module with timescale
    3 | module GbWrite(
      |        ^~~~~~~
%Error-TIMESCALEMOD: /media/stockage/projets/GbVga/cocotb/test_gbwrite/GbWrite_withtp.v:53:12: Timescale missing on this module as other modules have it (IEEE 1800-2017 3.14.2.2)
                     /media/stockage/projets/GbVga/cocotb/test_gbwrite/GbWrite_withtp.v:3:8: ... Location of module with timescale
    3 | module GbWrite(
      |        ^~~~~~~
%Error: Exiting due to 2 error(s)
        ... See the manual and https://verilator.org for more assistance.

If I comment the trait, it's ok.

[ekiwi]

Hi @Martoni, could you please also file an issue in the firrtl repository? This bug seems to be mostly related to functionality provided by the firrtl compiler: https://github.com/freechipsproject/firrtl

[ekiwi]

After some discussion on the firrtl bug tracker it turns out that @Martoni needs a way to not emit the ResetCounter and TestCase modules. This feature would need to be added in chisel-formal since that's where these modules come from.

[Martoni]

I' wondering if it's possible to add this option in src/main/scala/chisel3/formal/formal/Driver.scala or if it should be put somewhere else ?

[tdb-alcorn]

Sorry for the slow follow-up from me.

@Martoni is it the case that if these two modules had a Verilog timescale set then that would fix the issue for you? If so that's probably the easiest fix, I can add that relatively quickly.

[Martoni]

@Martoni is it the case that if these two modules had a Verilog timescale set then that would fix the issue for you? If so that's probably the easiest fix, I can add that relatively quickly.

If it's the easiest way I can test it yes. But I don't know if it's the solution.

[tdb-alcorn]

Sorry that it's taken me so very long to follow up on this. I just added timescale to those two modules in 1add8e6d5b233d37ce1ee54df148eb4d1ff64046. Does that fix your use case?

[Martoni]

Does that fix your use case?

I will try it.

[Martoni]

It's work with verilator. But it would really be better if ResetCounter and TestCase are not generated. But it's work as it.

[Martoni]

This lines should be removed from pure verilog sources I think :

  wire  ResetCounter_clock; // @[Formal.scala 14:36]
  wire  ResetCounter_reset; // @[Formal.scala 14:36]
  wire [31:0] ResetCounter_numResets; // @[Formal.scala 14:36]
  wire [31:0] ResetCounter_timeSinceReset; // @[Formal.scala 14:36]
  wire [31:0] TestCase_testCase; // @[Formal.scala 20:32]
  ResetCounter ResetCounter ( // @[Formal.scala 14:36]
    .clock(ResetCounter_clock),
    .reset(ResetCounter_reset),
    .numResets(ResetCounter_numResets),
    .timeSinceReset(ResetCounter_timeSinceReset)
  );
  TestCase TestCase ( // @[Formal.scala 20:32]
    .testCase(TestCase_testCase)
  );

[Martoni]

I made a quick&dirty script to suppress it.

[Martoni]

Maybe the code to modify is in FIRRTL package here. But I'm not good enough in Scala to do it.

[ekiwi]

It might also help to write these modules in Chisel instead of Verilog. Looking at this implementation might help: https://github.com/ekiwi/kiwi-formal/blob/d9be8efab5e8b7c7f04410ca943299b441bf1dad/src/kiwi/formal/VerificationAspect.scala#L20