search

YosysHQ / sby

SymbiYosys (sby) -- Front-end for Yosys-based formal verification flows
Other
379 stars 74 forks source link

sby_design: Also track fairness assumptions #260

Closed jix closed 5 months ago

jix commented 5 months ago

If we track $assume we should also track $fair and certainly need to support $check cells where the flavor is fair.

nakengelhardt commented 5 months ago

Fairness properties aren't supported at all yet in sby, are they?

jix commented 5 months ago

$fair is roughly to $live as $assume is to $assert so $fair would be used for for liveness properties and in fact the one liveness example included in SBY does have a $fair cell which sby_design so far ignored. With a $check cell it wouldn't ignore it but instead error out making the test for that example fail.