English
Hierarchical Assertion-Based Verification
by NGUYEN Huy Nam
Bull S.A. – METASymbiose S.A.S.
Abstract
Assertion-based verification has become more popular with the use of standardized assertion languages to provide the much-needed visibility into the inner workings of a design during verification. Meanwhile, Model Checking has become a widely accepted method to verify main features and key micro-architectural functionality of a design. The combination of both techniques provides the ability to verify design properties early in the design cycle without the need to create test benches and test. This requires a well-elaborated method to cope with the combinatorial explosion issue still faced by Model Checking.
This paper describes a hierarchical approach to assertion-based formal verification and illustrates this purpose with results obtained from application to industrial designs.
Introduction
Functional verification has become a bottleneck in the design process due to the increasing complexity and size of today’s ASICs and SoCs. Simulation still plays the major role in checking design correctness and has been recently enhanced with assertion-based methods to provide a much-needed increase in observable behavior during testing [2]. Assertion-Based Verification (ABV) favors obviously the verification of IP-based design and the standardization of assertion languages (eg. Sugar/PSL[1]) contributes to its growing popularity.
Meanwhile, thanks to perseverance, Model Checking [4] is gaining in efficiency and becomes more and more an accepted method to verify exhaustively functional features. ABV provides the links between static and dynamic verification and therefore permits cooperation between both techniques, verification re-use and subsequently promotes Model Checking.
However, Model Checking still suffers from size and complexity limitations, thus requiring an application methodology to overcome those issues and to provide the ability to demonstrate complex properties/assertions on useful large parts of the design.
This paper proposes a hierarchical approach to ABV which main purpose is the development of assertions to support effectively and in a cooperative manner static and dynamic verification.
This work is partly supported by the European Medea+/A502-MESA project.
A hierarchical approach to ABV
Design verification ensures that a RTL model of the design (implementation) behaves according to a set of requirements (specification) which consist of a set of specific behaviors (or assertions/properties). Large RTL models are defined hierarchically, therefore it is rather natural to consider the partitioning of large verification problems into a set of properties associated locally to each node of the model hierarchy.
Besides the “classical” classifications (eg. safety vs liveness properties or assumption vs assertion), from the design point of view, we consider two types of assertions : computation and communication assertions.
Figure 1 illustrates the hierarchical ABV methodology.
Figure 1. Hierarchical ABV
Static and dynamic verification
In order to support the hierarchical static ABV, the model checker Logan [4] developed by METASymbiose has been adapted to provide the ability to reason either on design logic or (exclusive) on temporal logic expressed by a set of assertions. Obviously, reasoning on temporal logic (ie. demonstration of a property from a set of properties) is still restricted to some types of properties (eg. invariants, time bounded properties, …) which are fortunately useful enough. The current version of Logan supports both LTL and CTL, a (restricted) hierarchical demonstration of assertions and adopts the Sugar/PSL standard (together with the proprietary TPL language).
The dynamic verification of assertions is supported by Kraml [5] another tool developed by METASymbiose and which main functionality is to synthesize RTL models from a set of Sugar/PSL properties. Obviously, only LTL properties are supported and the approach adopted by Kraml is tailored towards on-the-fly checking in hardware emulation / acceleration (connection of error detection to the triggering mechanism) (Cf. Figure 2).
Figure 2. Static and Dynamic Checking
Assertion Specification
The development of assertions represents the main part of efforts in ABV. As assertions vary according to the type and logic of the design, our purpose in this paragraph is to present some types of properties to illustrate the granularity of assertion specification we target in ABV.
a/ Computation assertions include :
Example of ECC checking property :
assert always (change[31:0==change_pattern) ->
s_err&~ d_err & (d_out[25:0]==d_in[25:0]) &
(e_out[4:0]==e_int[4:0]) & ~(par_out.0 ^ par_int.0) ;
Figure 3. ECC implementation checking
b/ Communication assertions
Communication assertions are mainly used to check for the correctness of data transfer between blocks. In our type of design, they are mainly dedicated to express the specific features of communication protocols at various protocol layers (eg. physical/ link/ network … or flit/ logic/ transaction …).
Figure 4 illustrates a classical scheme of flow control between blocks suitable for a hierarchical checking of its consistency using assertions on the arbiter of the emitting block and assertions on the fifo of the receiving block..
Figure 4. Flow control Checking
Results
The hierarchical ABV method described in this paper has been used at Bull on many industrial projects. The following results obtained from a partial application of such method to the verification of the FSS switch designed to connect processors in the NovaScale open server family demonstrate the efficiency of the approach:
This paper presents an application methodology for ABV with as special objective to promote the usage of Model Checking to support static verification. Results obtained on real-life projects demonstrate the efficiency of the method. Present and future works on the model checker include improvements of debugging functions and enhancement in hierarchical checking by handling a larger subset of temporal logic and allowing the demonstration of assertion on mixed design logic and temporal logic.
References
[1] Accellera : “Property Specification Language PSL” http://www.eda.org/vfv/docs/psl_lrm-1.0.pdf
[2] Y.Abarbanel, I.Beer et als., “FoCs : Automatic Generation of Simulation Checkers from Formal Specifications”, Proc. Of CAV, pp. 538-542, 2000
[3] H.D. Foster et als., “Assertion-Based Design”, Klwer Academic Publishers, 2003
[4] METASymbiose “Logan – User Manual”
[5] METASymbiose “Kraml – User Manual”
[6] H.N. Nguyen et als., “Verification of a DSP IP Core by Model Checking”, Proc. Of the HLDVT’02, 2002
Bull S.A. – METASymbiose S.A.S.
Abstract
Assertion-based verification has become more popular with the use of standardized assertion languages to provide the much-needed visibility into the inner workings of a design during verification. Meanwhile, Model Checking has become a widely accepted method to verify main features and key micro-architectural functionality of a design. The combination of both techniques provides the ability to verify design properties early in the design cycle without the need to create test benches and test. This requires a well-elaborated method to cope with the combinatorial explosion issue still faced by Model Checking.
This paper describes a hierarchical approach to assertion-based formal verification and illustrates this purpose with results obtained from application to industrial designs.
Introduction
Functional verification has become a bottleneck in the design process due to the increasing complexity and size of today’s ASICs and SoCs. Simulation still plays the major role in checking design correctness and has been recently enhanced with assertion-based methods to provide a much-needed increase in observable behavior during testing [2]. Assertion-Based Verification (ABV) favors obviously the verification of IP-based design and the standardization of assertion languages (eg. Sugar/PSL[1]) contributes to its growing popularity.
Meanwhile, thanks to perseverance, Model Checking [4] is gaining in efficiency and becomes more and more an accepted method to verify exhaustively functional features. ABV provides the links between static and dynamic verification and therefore permits cooperation between both techniques, verification re-use and subsequently promotes Model Checking.
However, Model Checking still suffers from size and complexity limitations, thus requiring an application methodology to overcome those issues and to provide the ability to demonstrate complex properties/assertions on useful large parts of the design.
This paper proposes a hierarchical approach to ABV which main purpose is the development of assertions to support effectively and in a cooperative manner static and dynamic verification.
This work is partly supported by the European Medea+/A502-MESA project.
A hierarchical approach to ABV
Design verification ensures that a RTL model of the design (implementation) behaves according to a set of requirements (specification) which consist of a set of specific behaviors (or assertions/properties). Large RTL models are defined hierarchically, therefore it is rather natural to consider the partitioning of large verification problems into a set of properties associated locally to each node of the model hierarchy.
Besides the “classical” classifications (eg. safety vs liveness properties or assumption vs assertion), from the design point of view, we consider two types of assertions : computation and communication assertions.
- Computation assertions associated to a node of a model hierarchy, express how this node should operate by itself locally (eg. algorithmic features, computation features,…),
- Communication assertions related to the transfer of data and are mainly located to the interface of blocks (eg. buffering, communication protocol, …etc.)
- Decomposition of complex properties into a set of simpler assertions suitable to be proved locally at block level,
- Support hierarchically model checking, that is the demonstration of assertions at a node of the hierarchy using available assertions at lower levels of the hierarchy.
Figure 1 illustrates the hierarchical ABV methodology.
Figure 1. Hierarchical ABV
Static and dynamic verification
In order to support the hierarchical static ABV, the model checker Logan [4] developed by METASymbiose has been adapted to provide the ability to reason either on design logic or (exclusive) on temporal logic expressed by a set of assertions. Obviously, reasoning on temporal logic (ie. demonstration of a property from a set of properties) is still restricted to some types of properties (eg. invariants, time bounded properties, …) which are fortunately useful enough. The current version of Logan supports both LTL and CTL, a (restricted) hierarchical demonstration of assertions and adopts the Sugar/PSL standard (together with the proprietary TPL language).
The dynamic verification of assertions is supported by Kraml [5] another tool developed by METASymbiose and which main functionality is to synthesize RTL models from a set of Sugar/PSL properties. Obviously, only LTL properties are supported and the approach adopted by Kraml is tailored towards on-the-fly checking in hardware emulation / acceleration (connection of error detection to the triggering mechanism) (Cf. Figure 2).
Figure 2. Static and Dynamic Checking
Assertion Specification
The development of assertions represents the main part of efforts in ABV. As assertions vary according to the type and logic of the design, our purpose in this paragraph is to present some types of properties to illustrate the granularity of assertion specification we target in ABV.
a/ Computation assertions include :
- Algorithm features to be checked against its implementation (eg. arithmetic operators). Figure 3 illustrates the verification of an error correction code (ECC) which requires the development of an extra model to separate the generation and checking parts of this algorithm.
- “Generic” properties related to common class of objects (eg. fifo, arbiter, …).
Example : Generic properties of an arbiter
property ack_on_val =always(AG(~elway[i] | valway[i]));
property ack_if_val=always(AG(AF(elway[i]| ~valway[i])));
… etc.
property ack_on_val =always(AG(~elway[i] | valway[i]));
property ack_if_val=always(AG(AF(elway[i]| ~valway[i])));
… etc.
- Specific computing behaviors
Example of ECC checking property :
assert always (change[31:0==change_pattern) ->
s_err&~ d_err & (d_out[25:0]==d_in[25:0]) &
(e_out[4:0]==e_int[4:0]) & ~(par_out.0 ^ par_int.0) ;
Figure 3. ECC implementation checking
b/ Communication assertions
Communication assertions are mainly used to check for the correctness of data transfer between blocks. In our type of design, they are mainly dedicated to express the specific features of communication protocols at various protocol layers (eg. physical/ link/ network … or flit/ logic/ transaction …).
Figure 4 illustrates a classical scheme of flow control between blocks suitable for a hierarchical checking of its consistency using assertions on the arbiter of the emitting block and assertions on the fifo of the receiving block..
Figure 4. Flow control Checking
Results
The hierarchical ABV method described in this paper has been used at Bull on many industrial projects. The following results obtained from a partial application of such method to the verification of the FSS switch designed to connect processors in the NovaScale open server family demonstrate the efficiency of the approach:
- Design : FSS directory-based switch snoop filtering (~60M transistors, 0.18µ Cu process)
- Over 1000 assertions developed for 2 computing units and distributed functions (eg. debug bus, performance monitoring, …)
- Number of design errors detected : 62
This paper presents an application methodology for ABV with as special objective to promote the usage of Model Checking to support static verification. Results obtained on real-life projects demonstrate the efficiency of the method. Present and future works on the model checker include improvements of debugging functions and enhancement in hierarchical checking by handling a larger subset of temporal logic and allowing the demonstration of assertion on mixed design logic and temporal logic.
References
[1] Accellera : “Property Specification Language PSL” http://www.eda.org/vfv/docs/psl_lrm-1.0.pdf
[2] Y.Abarbanel, I.Beer et als., “FoCs : Automatic Generation of Simulation Checkers from Formal Specifications”, Proc. Of CAV, pp. 538-542, 2000
[3] H.D. Foster et als., “Assertion-Based Design”, Klwer Academic Publishers, 2003
[4] METASymbiose “Logan – User Manual”
[5] METASymbiose “Kraml – User Manual”
[6] H.N. Nguyen et als., “Verification of a DSP IP Core by Model Checking”, Proc. Of the HLDVT’02, 2002
