-
Notifications
You must be signed in to change notification settings - Fork 58
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
I apparently don't know how to define a ClockDomain #273
Comments
Aha. What you're hitting there is that So writing this:
is equivalent to writing this:
(It works the same regardless of the domain name until you get to |
Ah, so the absence of |
Indeed! Right now the SymbiYosys flow is not very ergonomic unfortunately. I'll make sure to improve this but this is more of a medium-term plan. |
Here's a file that should fail formal verification:
And hey, BMC passes! But it shouldn't because there's a bad assertion in there that should fail every single time.
If I delete my
ClockDomain
and just replacem.d.ph1
withm.d.sync
, BMC properly fails. So how do I define aClockDomain
correctly?The text was updated successfully, but these errors were encountered: