7.5 Using Sandbox as a Method of Protection …
699
Developers of security systems for modern SoC need to study these materials with
great attention.
Development of the corresponding verification tools. Generation of the above
rules and the tools for verification of time and quality of execution can be fully
automated if the developer has relevant means to determine desired and undesired
behavior of the selected IP components. However, since we deal with hardware IPs
and standards COTSs and have no information about their internal operation, we
only need to determine their desirable limit characteristics. Of course, this usually
raises a question: which language would best describe and implement this task?
Fortunately, the today’s community of specialists dealing with insidious verification
problems, work very actively in this direction, creating various languages and means
of identification of IP properties on the interface; however, all this is usually done to
verify a developed SoC. The authors of [90] suggest using this property specification
language (PSL), which is very common among specialists, as a reference point to
create (describe) the process of designing a safe SoC (Fig. 9.33).
Property specification. Here we should single out the PSL language, a verification
language based on assertions, which historically evolved from IBM’s Sugar language
that was previously widely used to test similar models, and ultimately developed into
the IEEE standard (1850–2005) [90]. Of course, this PSL standard can be used to
identify separate timing properties of the designed SoC systems, i.e., the properties
that describe behavior of the system during a specified period of time through the
combination of ratios between linear time logic (LTL) formulas [108] and known
regular expressions. As a rule, this PSL function consists of four layers: Boolean layer,
normal temporary layer, temporary check layer, and temporary modeling layer. Basic
relationship between all observed interface signals and all variable conditions here
are usually determined as a boolean layer. Logic expressions on this level are always
regular Boolean expressions of the VHDL (not reset and rd_en) or Verilog flavor
(reset && rd_en) type. Each one of such temporary layers is used to describe behavior
of signals in a finite or infinite sequence of states. Each one of such sequences is
usually based on basic Boolean operators integrated with sequential operators united
with sequential operators. As a result, this PSL supports the so-called sequential
extended regular expression (SERE), which makes it possible to assess all the final
information based on the multitude of clock cycles. After that, all these properties
are built over other standard sequences and can contain both Boolean expressions
and other dependent properties, e.g., describe a system with req, ack, start, busy, and
done signals, each of which is true only at a certain point in time [109]. It is necessary
to note that always start ˆ next busy expression known to specialists, which states
that every time the start operation is checked at each particular moment in time, the
busy operation will be correct at the next point in time.
Other expressions such as {[*]; req; ack}] | = > {start; busy [*]; done} state
that in each case of req immediately followed by ack, handling of a verified request
also starts at each following point in time after emergence of ack. Expressions of
the {start; busy; done} type are also an example of a sequential presentation of the
phase of subsequent events. It is only a handling sequence starting with the start
command, followed by the busy command over certain predefined N of time points
699
Developers of security systems for modern SoC need to study these materials with
great attention.
Development of the corresponding verification tools. Generation of the above
rules and the tools for verification of time and quality of execution can be fully
automated if the developer has relevant means to determine desired and undesired
behavior of the selected IP components. However, since we deal with hardware IPs
and standards COTSs and have no information about their internal operation, we
only need to determine their desirable limit characteristics. Of course, this usually
raises a question: which language would best describe and implement this task?
Fortunately, the today’s community of specialists dealing with insidious verification
problems, work very actively in this direction, creating various languages and means
of identification of IP properties on the interface; however, all this is usually done to
verify a developed SoC. The authors of [90] suggest using this property specification
language (PSL), which is very common among specialists, as a reference point to
create (describe) the process of designing a safe SoC (Fig. 9.33).
Property specification. Here we should single out the PSL language, a verification
language based on assertions, which historically evolved from IBM’s Sugar language
that was previously widely used to test similar models, and ultimately developed into
the IEEE standard (1850–2005) [90]. Of course, this PSL standard can be used to
identify separate timing properties of the designed SoC systems, i.e., the properties
that describe behavior of the system during a specified period of time through the
combination of ratios between linear time logic (LTL) formulas [108] and known
regular expressions. As a rule, this PSL function consists of four layers: Boolean layer,
normal temporary layer, temporary check layer, and temporary modeling layer. Basic
relationship between all observed interface signals and all variable conditions here
are usually determined as a boolean layer. Logic expressions on this level are always
regular Boolean expressions of the VHDL (not reset and rd_en) or Verilog flavor
(reset && rd_en) type. Each one of such temporary layers is used to describe behavior
of signals in a finite or infinite sequence of states. Each one of such sequences is
usually based on basic Boolean operators integrated with sequential operators united
with sequential operators. As a result, this PSL supports the so-called sequential
extended regular expression (SERE), which makes it possible to assess all the final
information based on the multitude of clock cycles. After that, all these properties
are built over other standard sequences and can contain both Boolean expressions
and other dependent properties, e.g., describe a system with req, ack, start, busy, and
done signals, each of which is true only at a certain point in time [109]. It is necessary
to note that always start ˆ next busy expression known to specialists, which states
that every time the start operation is checked at each particular moment in time, the
busy operation will be correct at the next point in time.
Other expressions such as {[*]; req; ack}] | = > {start; busy [*]; done} state
that in each case of req immediately followed by ack, handling of a verified request
also starts at each following point in time after emergence of ack. Expressions of
the {start; busy; done} type are also an example of a sequential presentation of the
phase of subsequent events. It is only a handling sequence starting with the start
command, followed by the busy command over certain predefined N of time points