Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

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

Closed
wants to merge 2 commits into from
Closed

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

Changes from all commits
Commits
Show all changes
2 commits
Select commit Hold shift + click to select a range
cd1ff81
SpinalFormalConfig use _hasAsync per default, as per default an ASYNC…
janschiefer Feb 20, 2024
04d37b5
SpinalFormalConfig: Set _hasAsync accodring to clock config; set incl…
janschiefer Feb 20, 2024
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
6 changes: 4 additions & 2 deletions core/src/main/scala/spinal/core/formal/FormalBootstraps.scala
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -25,6 +25,7 @@ import org.apache.commons.io.FileUtils
import spinal.core.internals.{PhaseContext, PhaseNetlist}
import spinal.core.sim.SimWorkspace
import spinal.core.{BlackBox, Component, GlobalData, SpinalConfig, SpinalReport}
import spinal.core.ASYNC
import spinal.sim._

import scala.collection.mutable
Expand Down Expand Up @@ -62,7 +63,7 @@ case class SpinalFormalConfig(
var _backend: SpinalFormalBackendSel = SpinalFormalBackendSel.SYMBIYOSYS,
var _keepDebugInfo: Boolean = false,
var _skipWireReduce: Boolean = false,
var _hasAsync: Boolean = false,
var _hasAsync: Boolean = (SpinalConfig().includeFormal.defaultConfigForClockDomains.resetKind == ASYNC),
var _timeout: Option[Int] = None,
var _engines: ArrayBuffer[FormalEngin] = ArrayBuffer()
) {
Expand Down Expand Up @@ -118,7 +119,8 @@ case class SpinalFormalConfig(
}

def withConfig(config: SpinalConfig): this.type = {
_spinalConfig = config
_spinalConfig = config.includeFormal
Copy link
Collaborator

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

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

Copy link
Collaborator

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

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

Copy link
Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

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

Copy link
Collaborator

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

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.

_hasAsync = (_spinalConfig.defaultConfigForClockDomains.resetKind == ASYNC)
this
}

Expand Down
Loading