STU-FEI
At present, in designing digital devices, particularly in the functional and timing specification development phases, description languages (HDL) such as VHDL are commonly used. At the specification development level mentioned above, it is sometimes more convenient to use some formal specification means that lies above the specifications described by some HDL and which can be automatically translated to such a language.
One of the reasons may rest in the better specification capture capability that allows to express the designer's view in the easiest way. Good examples of such an approach are various graphically oriented specification means like Statemate and SpecCharts. Another reason, motivated mainly by demand of formal verification of systems implementations against their source specifications, may rest in the necessity to reach for logic or algebraic specification representations that are formally (exactly) semantically defined.
This paper deals with a special specification model. It is based on agents (here nontrivial actions that specify partial behaviors of the system over the defined discrete time structure in frame of a finite length interval of real numbers) and of processes that contain agents as their atoms.
An agent is able to specify a part of the system input-output communication with its environment, and the system final state at the end of the time interval. The i/o communication represented by a (possibly infinite) set of combined input/output words (i/o words) is described here by special regular expressions, dealing with symbolic variable values. The individual discrete time-points over which the input and output variable values are indicated, are specified by special events (changes of variable values) called timing events. The discrete time-points are defined as occurence times of the timing events. Then the i/o words we represent as sequences of triplets:
The agents may contain a set of timing rules that specify the timing discipline which must hold in the continuous time interval in order to obtain the correct behavior specified over the defined discrete time structure.
In this paper the agents are assumed to specify a deterministic behavior, although including concurrency in the agent conception is envisioned. The parallelism can be specified in our model by means of parallel processes or by external starting mechanism for agents and processes. The external starting mechanism allows to set agents and processes to be executed from the system environment. The first discrete time-points of the i/o words of a started agent (or of the first agent of a started process), are defined by the starting mechanism in dependence on input events and system (also state) variables. The starting mechanism can be used to efficiently specify exeptions (like resets and interrupts).
The motivation for the introduction of such a new specification model has arisen from the reasons mentioned above.
To experiment with the specification model, a language called HSL, has been introduced. The syntactic constructions of this language are similar to those of the language C. We omit the detailed description of the language; we merely demonstrate it by means of an example. This language is also used as input language in the developed functional simulator, called animator.
Animation is understood here as a functional simulation of the digital system specified by an HSL specification. By the animation program it is possible to validate the function, specified by the designer, i.e., it is possible to validate the execution of agents and processes that follows after starting their execution by proper events with the allowed input sequences contained in the presented i/o communications.
The full paper contains an example, which introduces the conception and illustrates the notions of our specification model.