SpinalTemplateSbt icon indicating copy to clipboard operation
SpinalTemplateSbt copied to clipboard

Use multiclock mode in formal verification

Open janschiefer opened this issue 1 year ago • 1 comments

Specify we have async signals / resets in the formal verification configuration with SpinalFormalConfig( _hasAsync = true ) . This works for SpinalHDL 1.10.1.

With the newer SpinalHDL versions ( dev-branch ) we could use FormalConfig.withAsync() .

janschiefer avatar Feb 19 '24 00:02 janschiefer

Hi the withAsync function has been added two years ago. I suppose it could be used after v1.7.0. :) In addition, the cross-clocking feature is not used as a default setting because it is much more complex than the synchronized clocking feature, as it involves the concept of global clocking.

Readon avatar Feb 19 '24 01:02 Readon