SpinalFormalConfig: Set _hasAsync accodring to clock config; set includeFormal as default in SpinalFormalConfig

[janschiefer]

Closes #

SpinalHDL/SpinalTemplateSbt#39
#1314

Context, Motivation & Description

• SymbiYosys multiclock mode has to be used when using ResetKind == ASYNC, so enable multiclock mode when using this reset mode in the default clock domain
• always use ".includeFormal" in FormalConfig, to generate the "right" kind of "assert" depending on mode ( simulation vs. verification )

Impact on code generation

RTL:

• use .includeFormal as default and therefore do not generate "assert(...) else ... begin" blocks in formal verification mode

SymbiYosis configuration file:

• use "multiclock on" when an using an ASYNC reset in the default clock domain

Checklist

• API changes are or will be documented: No changes on outward facing API

[Readon]

How about only keep this line to help user easily work around the config problem?

[Readon]

Multiclock features of formal tools only good for the design which is really have several clocks. It might work slower.

[janschiefer]

You have a actually working alternative with ASYNC reset without multiclock?

[Readon]

You have a actually working alternative with ASYNC reset without multiclock?

The tester in located in tester/ subproject are all use ASYNC reset as default. The SYNC reset has not been tested.
However, although the design itself use ASYNC reset, the verification actually run is still in SYNC manner.
So I think it doesn't matter.

[Readon]

according to #1435 this can be closed.