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.

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

Verify component without withAsync option with synchronous reset as default. #1435

Merged
merged 18 commits into from
Jun 6, 2024

Conversation

Readon
Copy link
Collaborator

@Readon Readon commented Jun 3, 2024

Closes #1430

Context, Motivation & Description

Impact on code generation

Checklist

  • Unit tests were added
  • API changes are or will be documented:

@Readon Readon marked this pull request as draft June 3, 2024 07:16
@Readon
Copy link
Collaborator Author

Readon commented Jun 3, 2024

This might lead to a very slow formal verification in the lib itself.

@Readon
Copy link
Collaborator Author

Readon commented Jun 3, 2024

The checker fails because of "multiclock on" statement would lead to an erron initial value while prove.
In theory, the initial value in prove should follow the assert and assume condition. However, when multiclock on the prove tools would not follow the initial condition.
This is tested on existing implementation and current version of yosys.

@Readon
Copy link
Collaborator Author

Readon commented Jun 3, 2024

@Dolu1990 How can I change the default clockDomain's reset kind in Component?
Never mind, I have found the config way to achieve this.

We might need to change the default clockDomain's resetKind to SYNC for formal verification only.

@Readon Readon marked this pull request as ready for review June 3, 2024 14:11
@Readon
Copy link
Collaborator Author

Readon commented Jun 3, 2024

Now the existing verification are mostly in synchronous mode, which is faster.
I would test if it works in latest yosys.

@Readon Readon marked this pull request as draft June 3, 2024 14:32
@Readon
Copy link
Collaborator Author

Readon commented Jun 3, 2024

As tested in yosys 0.41 here, the synchronous design have been passed.
However, it failed on FifoCC tester, which turned multiclock on in a strange mode.
The waveform shows that it fails during the second reset time, the assertion does not follow the reset check priority.
It's not a proper time to upgrade to the latest version, IMO.

@Readon Readon changed the title fix #1430. Verify component without withAsync option with synchronous reset as default. Jun 4, 2024
@Readon Readon marked this pull request as ready for review June 4, 2024 01:18
@Readon
Copy link
Collaborator Author

Readon commented Jun 4, 2024

I have also moved the ModuleAnalyzer and DataAnalyzer from lib to core directory, because there might be some analysis could be easily done by those tools, also in core.

@Readon
Copy link
Collaborator Author

Readon commented Jun 6, 2024

OK, all the verification testers have been run through under the Yosys 0.41.

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
None yet
Projects
None yet
Development

Successfully merging this pull request may close these issues.

Formal proofs started to fail with newer versions of sby
1 participant