tuura / plato

A DSL for asynchronous circuits specification
Other
11 stars 2 forks source link

Implement verification for incorrect causalities. #62

Open jrbeaumont opened 7 years ago

jrbeaumont commented 7 years ago

For example, if an internal transition causes an input transition, this is erroneous.

Are there further checks of this style?

snowleopard commented 7 years ago

There may also be a report on timing assumptions and concurrency reductions that have been detected in the specification: an input causing another input is usually a timing assumption, and an output causing another output is called a concurrency reduction.