Formal verification: Verilog generated when using synchronous resets is not understood by SymbiYosys about spinalhdl HOT 10 OPEN

The problem of your code is

.withConfig( Config.spinal )

This line use Spinal's elaboration config which is not compatible with the formal config one, delete it would work.

from spinalhdl.

The line is necessary to get a purely synchronous reset in this context.

Without this line, the following code is generated:

(...)
  always @(posedge clk or posedge reset) begin
(...)

Maybe I'm wrong, but that seems like an async reset to me.

This async reset actually triggers another bug, but within SpinalTemplateSbt: SpinalHDL/SpinalTemplateSbt#39

Proposed fix / hack / bypass (?): #1315

from spinalhdl.

This might be a solution.

.withConfig( Config.spinal.includeFormal )

from spinalhdl.

Yes this actually works in SYNC reset mode.

In ASYNC reset mode we actually need to set the SymbiYosys multiclock mode.

Here my attempt to fix both issues: #1320
--> use .includeFormal as default in FormalConfig and therefore do not generate "assert(...) else ... begin" blocks in formal verification mode
--> use "multiclock on" when an using an ASYNC reset in the default clock domain

from spinalhdl.

Yes this actually works in SYNC reset mode.

In ASYNC reset mode we actually need to set the SymbiYosys multiclock mode.

Here my attempt to fix both issues: #1320 --> use .includeFormal as default in FormalConfig and therefore do not generate "assert(...) else ... begin" blocks in formal verification mode --> use "multiclock on" when an using an ASYNC reset in the default clock domain

I think use "multiclock on" for a synchronized design with only ASYNC reset is a little bit redundant. It might be slower.
If you are using asynchronous clocks, then multiclock on might be a good choice. Have you looked at the FormalFifoCCTester example in the lib?

from spinalhdl.

Not yet...ok.
Well, the assumeResetReleaseSync / assumeIOSync2Clock in this complex example make sense...

--> I need to implement this in the SpinalHDL Template, so the template formal workflow works again by default.

Actually the real issue here seens the complete lack of documentation for all of SpinalHDL awesome and kick-ass "hidden" features.

from spinalhdl.

Can you help me getting the Spinal basic template to run with assumeResetReleaseSync, and GlobalClock without multiclock mode?

I'm kinda lost here...

from spinalhdl.

Can you help me getting the Spinal basic template to run with assumeResetReleaseSync, and GlobalClock without multiclock mode?

I'm kinda lost here...

Those assumeResetReleaseSync and GlobalClock are initially designed for clock crossing design, if you just want to verify a design with different reset, I think they are not necessary.

So if what you want is to verify your design which have cross clock manner, I can give you some hits.
In formal verification of yosys, the asynchronous verification is driven by a hidden clock, so called GlobalClock.
All clocks for the design is generated from that.

The relationship between each clock and reset or io signals should be explicit declared.
This make things complex, so some functions have been wrapped for that.

//assume the pushClock's period while verification.
gclk.assumeClockTiming(pushClock, pushPeriod)
//this keep the reset signal synchronize with it's corresponding clock. here pushClock domain's reset is synchronized with it's clock.
gclk.assumeResetReleaseSync(pushClock)
//this function make sure push.valid signal is a signal synchronized with the pushClock domain's clock.
gclk.assumeIOSync2Clock(pushClock, dut.io.push.valid)

Also, some utilities is design for timing.

//this keep the reset last for popPeriod.
gclk.keepBoolLeastCycles(reset, popPeriod)
//this make sure pushClock domain's reset and popClock domain's reset active at the same time.
gclk.alignAsyncResetStart(pushClock, popClock)

from spinalhdl.

you can use them by calling withAsync method of FormalConfig.

from spinalhdl.

About the documentation, the formal verification currently is still not widely used, especially the Cross Clocking one. So I want to wait more test before we documented the usage.
Because if it is documented, the backward compatibility would be the most important thing we should take consider in.

from spinalhdl.