search

tuura / plato

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

Add support for 'may-fire' semantics #86

Open snowleopard opened 7 years ago

snowleopard commented 7 years ago

As discussed in #83:

I attached the most permissive state graph for srHalfLatch. Here pink arcs have the 'may-fire' semantics for outputs, while the usual black ones correspond to usual 'must-fire' semantics.

The idea is that in states 100 and 011 the circuit must eventually do q+ and q- transitions, respectively. On the other hand, in states 110 and 111 the circuit may switch q but doesn't necessarily have to. If we remove the pink arcs, then we get @jrbeaumont's spec for srHalfLatch. If we forbid states 110 and 111 by restricting the environment we get my spec.

Unfortunately, without pink/may arcs we cannot have a fully permissive specification.

srhalflatch

Can we add support for may-fire semantics to Plato?

snowleopard commented 7 years ago

Note that there is a simple monoid on 'no/may/must` arcs:

data Dependency = No | May | Must deriving (Eq, Ord)

instance Monoid Dependency where
    mempty  = No
    mappend = max

That is, May combined with Must gives us Must, and No is the identity.

This means that one can start with a very permissive concept specification and later add a few Must dependencies in the environment that fully resolve the ambiguity leading to purely Must-ful specifications.

snowleopard commented 7 years ago

For another example of a circuit with 'may' dependencies is the WAIT element, see Figure 4 here:

http://homepages.cs.ncl.ac.uk/victor.khomenko/papers/waitx.pdf

Note that it is called 'optional' in the paper. Maybe this is a better term.