H1 is designed to be the interworking language between the SML parent and the solvers. It includes all of the algorithms with exponential cost.
Variables may be
An input variable has its value provided at the current timestep in the final design. Its future values must be universally quantified (although other restricting declarations can be imported).
A state variable is universally quantified at the current time step. A next state function is specified and future time expressions are generated by recursive application of the next state function.
\A s0; X(s0) = exp;
An intermediate variable defines a macro expansion.
mystate = a & b;
Regular expressions operate (by default) on the time axis.
We convert them to declarations at the moment. Keeping them more behavioural may be an optimisation.
Alternation is simply disjunction.
a | b --> a \/ b;
Time Concatenation becomes conjunction
a . b --> a /\ X(b);
Prescribed repetition by a constant becomes macro expansion
a ** n --> a /\ X(a) .... X(a, n-1);
Arbitrary repetition is lifted from the usual circuit
Currently only Boolean fully implemented but integers are in there.
Abstract datatypes next.
Home. SRG Talk. 12 March 2003. DJ Greaves. www.cl.cam.ac.uk.