Checking the equivalence of a system-level model against an RTL design is a major challenge. The reason is that usually the system-level model is written by a system architect, whereas the RTL implementation is created by a hardware designer. This approach leads to two models that are significantly different. Checking the equivalence of real-life designs requires strong solver technology. The challenges can only be overcome with a combination of bit-level and word-level reasoning techniques, combined with the right orchestration. In this paper, we discuss solver technology that has shown to be effective on many real-life equivalence checking problems.

When designers create RTL models from a system-level specification, arrays in the system-level model are often implemented as memories in the RTL. Knowing the correspondence between ESL arrays and RTL memories can significantly reduce the complexity of a formal equivalence check between the ESL model and the RTL. In practice, however, handling memory mappings in ESL-RTL equivalence checking is non-trivial for the following reasons: First, because of a lack of bit-accurate data-types in the systemlevel language, the information stored in an array location may be stored in a compressed form in the RTL. Second, a single array in the ESL model may be implemented by multiple memories in the RTL and/or corresponding data items may be stored in different locations. And last but not least, due to timing differences between the ESL model and the RTL, the correspondence between arrays and memories may not hold in every clock cycle. In this paper, we propose an approach to ESL-RTL equivalence checking which can deal with all of these difficulties.

A rigorous system-level model (SLM) for a hardware design project is extremely important, often critical. Such a functional model not only defines the architect's ideas but also builds a precise foundation for both hardware designers and verification engineers. The key uses of SLMs are: architecture validation; performance modeling and architectural trade-off; platforms for software development and verification; and functional reference model. In this tutorial, we discuss how to formally verify sequential equivalence between SLMs and RTL, for both timed and untimed models. First, we provide a formal definition of the sequential equivalence. Then we discuss various formal verification technology that enables such practice in real designs.

Symbolic simulation is a formal verification technique which combines the flexibility of conventional simulation with powerful symbolic methods. Some constructs, however, which are easy to handle in conventional simulation need special consideration in symbolic simulation. This paper discusses some special constructs that require unique treatment in symbolic simulation such as the symbolic representation of arrays, an efficient This paper discusses some special constructs that are unique to symbolic simulation such as the symbolic representation of arrays, an efficient symbolic method for storing arrayed instances and the handling of symbolic data-dependent delays. We present results which demonstrate the effectiveness of our symbolic array model in the simulation of highly regular structures like FPGAs, memories or cellular automata.

Symbolic simulation is a promising formal verification technique combining the flexibility of conventional simulation with powerful symbolic methods. Unfortunately, existing symbolic simulators are restricted to gate level simulation or handle just a synthesizable subset of an HDL. Simulation of systems composed of design, testbench and correctness checkers, however, requires the complete set of HDL constructs. We present an approach that enables symbolic simulation of the complete set of RT-level Verilog constructs with full delay support. Additionally, we propose a flexible scheme for introducing symbolic variables and demonstrate how error traces can be simulated with this new scheme. Finally, we present some experimental results on an 8051 micro-controller design which prove the effectiveness of our approach.

Article Free Access Share on Reducing power dissipation after technology mapping by structural transformations Authors: Bernhard Rohfleisch Institute of Electronic Design Automation, Technical University of Munich, 80290 Munich, Germany Institute of Electronic Design Automation, Technical University of Munich, 80290 Munich, GermanyView Profile , Alfred Kölbl Institute of Electronic Design Automation, Technical University of Munich, 80290 Munich, Germany Institute of Electronic Design Automation, Technical University of Munich, 80290 Munich, GermanyView Profile , Bernd Wurth Synopsys, Inc., 700 E. Middlefield Rd., Mountain View, CA Synopsys, Inc., 700 E. Middlefield Rd., Mountain View, CAView Profile Authors Info & Claims DAC '96: Proceedings of the 33rd annual Design Automation ConferenceJune 1996 Pages 789–794https://doi.org/10.1145/240518.240667Published:01 June 1996Publication History 25citation233DownloadsMetricsTotal Citations25Total Downloads233Last 12 Months19Last 6 weeks5 Get Citation AlertsNew Citation Alert added!This alert has been successfully added and will be sent to:You will be notified whenever a record that you have chosen has been cited.To manage your alert preferences, click on the button below.Manage my AlertsNew Citation Alert!Please log in to your account Save to BinderSave to BinderCreate a New BinderNameCancelCreateExport CitationPublisher SiteeReaderPDF