The register-transfer-level design case study examines defining requirements and an architecture for a simple alarm clock controller. This is an appropriate case study because it uses common abstractions from electronic systems design and extends those abstractions to include elements of system-level design. The first model is exclusively behavioral and uses a single behavioral specification to define systems requirements. The second model uses a collection of behavioral specifications to define an architecture for the controller. Finally, some correctness conditions are defined using Rosetta’s special-purpose component constructs.
Figure 17.1 graphically defines both the system-level view and the architecture to be defined. Defined in terms of signals from Figure 17.1, the requirements for the clock controller are:
When the setTime
bit is set, (timeInHr
*60 + timeInMin)
is stored as the clockTime
while timeInHr
and timeInMin
are output to the time display.
When the setAlarm
bit is set, (timeInHr60 + timeInMin)
is stored as the new value of alarmTime
while timeInHr
and timeInMin
are output to the time display.
When the alarmToggle
bit is set, the alarmOn
bit is toggled.
When clockTime
and alarmTime
are equivalent and alarmOn
is asserted, the alarm should be sounded. Otherwise it should not.
When setTime
is clear and setAlarm
is clear, clockTime
is output as the display time.
The clock increments its time value when clk
is asserted.
The models defining this case study are organized into three collections. The timeTypes
package defines basic types and functions used throughout both the behavioral and structural models. The alarmClockBehav
model defines functional requirements for the clock system. Each of the previous requirements maps into one or more requirements in the alarmClockBehav
model. Several RT level specifications define the components of the implementation architecture defined by alarmClockStruct
. These include a data store, multiplexer, comparator, and counter defined as individual models. Finally, alarmClock
defines relationships between the behavioral and structural alarm clock models that define correctness of the architecture.
Each model in this case study prototypical of models useful when designing using RTL components. The requirements model provides a behavioral description of the entire system of interest. The component models provide excellent examples of RTL specifications in Rosetta, while the structural model exemplifies structural assembly. Finally, the requirements model shows how correctness conditions can be expressed as a part of the system model.
Two specifications define the requirements-level models for the alarm clock controller. The first is a package of types and functions used across all models. The timeTypes
package represents common definitions that are shared or appear in the interfaces of specifications. The second is a model defining the system-level requirements. The alarmClockBehav
model translates the English description from the introduction into a formal Rosetta specification.
Figure 17.2 shows the timeTypes
package specification. The only element of this package is a function for incrementing time values that is used frequently throughout the case study. Frequently, a package like this will contain definitions of types as well as functions. This is particularly useful for shared types used in interfaces that cannot be defined within facets. Because interface types are standard Rosetta base types, this is not necessary here.
Example 17.2. Time types shared among specifications.
package timeTypes::static is increment_time ( minutes :: integer ) :: integer is if minutes < 12 * 60 then minutes + 1 else 0 end if; end package timeTypes;
Figures 17.3 and 17.4 show the basic requirements specification, similar to what would be called a behavioral specification in VHDL or Verilog. This specification is separated into interface and body to simplify the presentation. The interface specification defines the signals that appear at the system interface described in Figure 17.1. The association between model parameters and signals from the figure is readily visible.
Example 17.3. The interface of the system-level requirements model.
use timeTypes; facet interface alarmClockBehav ( timeInHr, timeInMin :: input integer; setAlarm, setTime, alarmToggle, clk :: input bit; displayTimeHr, displayTimeMin :: output integer; alarm :: output bit ) :: state_based is end facet interface alarmClockBehav;
Example 17.4. System requirements specification.
use timeTypes; facet body alarmClockBehav is alarmTime, clockTime :: integer alarmOn :: bit; begin setClock_label: if %setTime then(clockTime' = timeInHr * 60 + timeInMin) and(displayTimeHr' = timeInHr) and(displayTimeMin' = timeInMin) elseif event(clk) and clk=1 then clockTime' = increment_time(clockTime) else clockTime' = clockTime end if; setAlarm_label: if %setAlarm then(alarmTime' = timeInHr * 60 + timeInMin) and(displayTimeHr' = timeInHr) and(displayTimeMin' = timeInMin) else alarmTime' = alarmTime end if; displayClock_label: ((setTime = 0 )and(setAlarm = 0)) => (displayTimeHr' = clockTime div 60) and(displayTimeMin' = clockTime mod;60); armAlarm_label: if event(alarmToggle) and alarmToggle = 1 then (alarmOn' = not alarmOn) else (alarmOn' = alarmOn) end if; sound_label: alarm' == if (alarmOn = 1)and(alarmTime = clockTime) then 1; else 0 end if; end facet Body alarmClockBehav;
The specification body takes the requirements specified in the introduction and formalizes them as specification terms. Each term label describes the action specified by that label. In each case, if
expressions or implications define the relationship between inputs and current state, and the values to be stored or output in the next state. Remember that terms are simultaneously true and their order within the model is immaterial.
A deeper explanation of several terms will help to understand the specification and its style. setClock_label
is the name of the term specifying how and when the clock time gets set. There are three possible cases defined in this term. When setTime
is asserted, the internal clock time is set to the time inputs and the input time is displayed. This corresponds to behavior when setting a digital clock. If the clock is not being set and there is a rising edge on clk
, then the internal state is updated by incrementing the current state. Finally, if nothing has happened, then the internal clock state does not change. The setAlarmLabel_term
is similar, without the need to update the internal clock.
The clock’s display is managed by the displayClock_label
term. If the clock is not being set and the alarm is not being set, this term specifies that the clock display should be the current time. Note that this term is not dependent on the clock and does not reference any variables in the next state. Thus, the term must always hold for the clock to function properly. If nothing is being set, the clock must always display the current time.
The armAlarm_label
and sound_label
manage the arming and sounding of an alarm. armAlarm_label
states that the alarm state is toggled when a rising edge occurs on the alarmToggle
signal. Note that this is an asynchronous signal, as the term does not reference the clock. sound_label
indicates that the alarm is sounded whenever the stored alarm time is equal to the stored clock time. Like the display requirement, this requirement does not depend on the clock or reference variables in the next state. Thus, the term is invariant across all states.
As usual, symbols decorated with ticks represent values in the next state. In most cases, the use of ticked symbols is limited to the left side of equalities. This is in no way required by Rosetta. However, it reflects a common HDL style, where the next value to be assigned to a signal is calculated and a signal assignment operator used to schedule an update. Specifications written in this form are easier to synthesize and simulate. However, when writing specifications of incomplete systems, this style may not be appropriate or even feasible.
The basic component set defines a collection of custom RTL components that will be used to define a structural architecture for the controller. One facet is defined to implement each of the basic functional blocks from Figure 17.1. These facets will be assembled later to define the complete architecture.
The mux
component in Figure 17.5 is a specialized multiplexer that selects from three different times to display. Two control signals, setAlarm
and setTime
, are used to choose whether to display the new alarm time or clock time being entered, or the time maintained by the clock. Where as the store
component will use these signals to control when data is replaced in the internal clock store, the mux
component uses them to determine what value should be displayed.
Example 17.5. The clock multiplexer component.
use timeTypes; component mux ( timeInHr, timeInMin ::input integer; clockTime ::input integer; setAlarm, setTime ::input bit; displayTimeHr, displayTimeMin ::output integer ) :: state_based is begin assumptions ambiguous_select:not(%setTime and %setAlarm) end assumptions; definitions 11: %setAlarm or %setTime => (displayTimeHr' = timeInHr)and(displayTimeMin' = timeInMin); 13: not (%setTime or %setAlarm) => (displayTimeHr' = clockTime div 60) and (displayTimeMin' = clockTime mod 60); end definitions; implications end implications; end component mux;
A component is used for this model, rather than a facet, because of the desire to specify a usage condition. The ambiguous_select
term in the assumptions
section asserts that this component requires that these two inputs must not be simultaneously asserted. If so, the function of the device cannot be uniquely determined. Using the assumption in this way simplifies the component specification by eliminating the need to specify behavior for this case. It is simply deemed a bad input state that cannot be managed.
The store
component in Figure 17.6 defines a simple register specialized for storing time values used in this system. The device is rising-edge triggered on any one of three signals. The state_based
predicate event
checks to see if a value has changed during the state change. When conjuncted with a check to see if the new value is 1, the result is a rising-edge check. In effect, store
behaves like three registers packaged in the same component.
Example 17.6. The alarm clock store component.
use timeTypes; facet store ( timeInHr, timeInMin, nextClockTime ::input integer; setAlarm, setTime, alarmToggle ::input bit; clockTime, alarmTime ::output integer; alarmOn ::output bit ) :: state_based is begin 11: if event(setAlarm)and %setAlarm then alarmTime' = timeInHr * 60 + timeInMin else alarmTime' = alarmTime end if; l2: if event(setTime)and%setTime then clockTime' = timeInHr * 60 + timeInMin else clockTime' = clocktime end if; 13: if event(alarmToggle)and %alarmToggle then alarmOn' = not alarmOn else alarmOn'= alarmOn end if; end facet store;
Possibly the most interesting thing about store
is that it uses no internal variables to store values. Because each value is associated with its own update signal and the stored value is the same as the output value, the output parameter is effectively the store. The model could have as easily represented the internal store explicitly.
A facet model is used for the store
component because there are no correctness conditions or usage assumptions associated with the device. A component could easily be used, but the assumptions and implications blocks would be empty. The only reason to use a component would be in anticipation of additional information or back annotation during analysis.
The counter
specification (Figure 17.7) is somewhat misnamed, as it defines the next state function for the internal timer, but does not store it. Instead, the value is output to the store
component, where it is saved. In effect, the counter outputs a new value each time the clk
signal rises and outputs the current input otherwise.
Example 17.7. Alarm clock counter component.
use timeTypes; facet counter ( clockTime ::input integer; clk ::input bit; nextClockTime ::output integer ) :: state_based is begin l4: nextClockTime'=if event(clk)and %clk then increment_time(clockTime) else clockTime end if; end facet counter;
The comparator
specification (Figure 17.8) implements an equality comparison on time values and outputs the result if the clock’s alarm is engaged. In effect, it is a comparator whose output is conjuncted with the setAlarm
input.
The clock
facet in Figure 17.9 defines a signal that simply changes state. The clock is defined in the state_based
domain, implying that nothing can be said about its period. It is modeled simply as a component that inverts its output in each state change. Note that in this case the model is a facet rather than a component, due to the simplicity of the device. There is no need to understand usage assumptions or specify correctness conditions for the clock.
With the component models defined, the structural design merely provides interconnections between components. Like the behavioral specification, the structural specification is split into interface and body. The interface, shown in Figure 17.10, is uninteresting, with the exception of being identical to the behavioral interface (excluding the name of the model). Rosetta does not currently support multiple implementations for the same interface, thus the structural and behavioral interfaces must both exist.
Example 17.10. Alarm clock structural implementation interface.
use TimeTypes; facet interface alarmClockStruct ( timeInHr, timeInMin :: input integer; setAlarm, setTime, alarmToggle, clk :: input bit; displayTimeHr, displayTimeMin :: output integer; alarm :: output bit ) :: state_based is end facet interface alarmClockStruct;
The specification body, shown in Figure 17.11, provides interconnection details. Each internal component has a unique design and is thus instantiated only once within the structural design. A local declaration defines internal signals using the same naming conventions used in Figure 17.1.
Example 17.11. Alarm clock structural implementation body.
facet body alarmClockStruct is clockTime, nextClockTime, alarmTime :: integer; alarmOn :: bit; begin store_1 : store ( timeInHr, timeInMin, nextClockTime, setAlarm, setTime, alarmToggle, clockTime, alarmTime, alarmOn ); counter_1 : counter ( clockTime, clk, nextClockTime ); comparator_1 : comparator ( setAlarm, alarmTime, clockTime, alarm ); mux_1 : mux ( timeInHr, timeInMin, clockTime, setAlarm, setTime, displayTimeHr, displayTimeMin); end facet alarmClockStruct;
At this point in the alarm clock design, requirements exist in the form of a behavioral specification, and architectural requirements exist in the form of a structural specification. However, there is no correctness condition explicitly stating the relationship that should exist for them. An implied correctness condition can be read into the system description. However, this is not sufficient for achieving true system-level design.
The component alarmClock
shown in Figure 17.12 defines correctness between the structural and behavioral models in a component that can be used in other models. The alarmClock
component instantiates a single copy of alarmClockBehav
in its definitions
section. By instantiating the behavioral specification with parameters from the component interface, the component now has the behavior specified by the behavioral specification.
Example 17.12. Specification of design requirements and correctness conditions.
correctness: alarmClockStruct(timeInHr,timeInMin,setAlarm,setTime, alarmToggle,displayTimeHr,displayTimeMin, alarm) => alarmClockBehav(timeInHr,timeInMin,setAlarm,setTime, alarmToggle,displayTimeHr,displayTimeMin, alarm); component alarmClock ( timeInHr, timeInMin ::input integer; setAlarm, setTime, alarmToggle, clk ::input bit; displayTimeHr, displayTimeMin ::output integer; alarm ::output bit ) :: state_based is begin Assumptions end Assumptions definitions def: alarmClockBehav(timeInHr,timeInMin,setAlarm,setTime, alarmToggle,clk,displayTimeHr, displayTimeMin,alarm); end definitions; implications correctness: alarmClockStruct(timeInHr,timeInMin,setAlarm,setTime, alarmToggle,clk,displayTimeHr, displayTimeMin,alarm) => alarmClockBehav(timeInHr,timeInMin,setAlarm,setTime, alarmToggle,clk,displayTimeHr, displayTimeMin,alarm); end implications; end component alarmClock;
The component’s correctness condition is expressed in the implications
section using the term:
The =>
operation on facets and components is defined as homomorphism. Thus, the correctness condition asserts that all properties of the alarmClockStruct
component must be derivable from the alarmClockBehav
component. This is the same instantiation of the component specified in the definitions
block.
The correctness condition accomplishes two important things. First, it explicitly states that all behaviors of the behavioral specification must be exhibited by the structural specification. This is a rather strong correctness condition, but for such a small component this is quite manageable. The second, and less obvious, result is that the behavioral specification is tied to the structural specification. If the structural specification is altered in a way that causes it to not satisfy the behavioral specification, the correctness condition is violated and one of the specifications must be modified. Thus, the behavioral specification tracks the structural specification with the component defining correctness wherever it is used.
An alternate definition of correctness is shown in Figure 17.13 as a component defining testing conditions. The alarmClockTest
component instantiates one copy of the behavioral and structural specifications. It then drives inputs of each internal component with external signals from the interface.
Example 17.13. Specification of correctness conditions in a testing component.
component alarmClockTest ( timeInHr, timeInMin :: input integer; setAlarm, setTime, alarmToggle, clk :: input bit; ) :: state_based is displayTimeHrS, displayTimeMinS :: integer; displayTimeHrB, displayTimeMinB :: integer; alarmS :: output bit alarmB :: output bit begin Assumptions end Assumptions definitions beh: alarmClockBehav(timeInHr,timeInMin,setAlarm,setTime, alarmToggle,clk,displayTimeHrB, displayTimeMinB,alarmB); struct: alarmClockStruct(timeInHr,timeInMin,setAlarm,setTime, alarmToggle,clk,displayTimeHrS, displayTimeMinS,alarmS); end definitions; implications c1: displayTimeHrS == displayTimeHrB; c2: displayTimeMinS == displayTimeMinB;; c3: alarmS == alarmB; end implications; end component alarmClockTest;
Each component’s outputs are gathered by a collection of internal variables. Instead of generating outputs, the alarmClockTest
component compares like outputs from the behavioral and structural models using these variables. These assertions are made in the implications
section and are invariant over state change. This is a weaker correctness condition than that defined earlier because it specifies only three properties that must be maintained. The name alarmClockTest
is chosen because the component defines a testing architecture in addition to correctness conditions.
The alarm clock controller is included as an example of how Rosetta extends classical RTL design. At the functional design level, Rosetta adds little over VHDL or Verilog. Components are defined using a largely operational subset of the expression language, similar in nature to behavioral VHDL or Verilog specification. Components are then integrated using structural constructs, again similar to structural VHDL or Verilog.
Where Rosetta introduces new capabilities is in the inclusion of usage assumptions and correctness conditions. In the components alarmClock
and alarmClockTest
, the implications
and definitions
sections are used to define usage assumptions and correctness conditions. Thus, design intent is memorialized as a part of the system specification in an interpretable fashion.
Recording usage assumptions formally as requirements and implications has two advantages. First, design intent is not lost and moves through design stages with component requirements. Design intent becomes a part of the living specification. Second, design intent is usable by tools in the design flow. Representing intent formally in Rosetta enables input and analysis using tools in the design flow. For example, both requirements and implications can frequently be used as assertions in simulators and model checkers. The designer is thus rewarded for maintaining this information as part of the specification.