The Infona portal uses cookies, i.e. strings of text saved by a browser on the user's device. The portal can access those files and use them to remember the user's data, such as their chosen settings (screen view, interface language, etc.), or their login data. By using the Infona portal the user accepts automatic saving and using this information for portal operation purposes. More information on the subject can be found in the Privacy Policy and Terms of Service. By closing this window the user confirms that they have read the information on cookie usage, and they accept the privacy policy and the way cookies are used by the portal. You can change the cookie settings in your browser.
In the context of industrial size circuits, the interconnection of many blocks from many sources lead to globally asynchronous locally synchronous designs. The transmission of information between clock domains requires complex synchronizers, the correctness of which must be thoroughly verified. Current EDA tools are able to recognize predefined synchronizing modules, but fail to identify custom synchronizers...
It is well known that the correct behavior of asynchronous circuits is not guaranteed when the inputs switch too slowly. The erroneous behavior is generally difficult to be spotted by simulation based methods. We applied formal methods to study the analog switching behavior of a full-buffer circuit composed of C-elements. We used our reach ability analysis tool COHO to compute all reachable states...
This paper describes VSYML, a symbolic simulator that extracts formal models from VHDL descriptions. The generated models are adequate to formal reasoning in various frameworks. VSYML is a reimplementation of its ancestor Theosim; it brings various improvements e.g., with regard to arrays and other complex data types.
This paper presents a new method for formally verifying asynchronous circuits with a symbolic model checking tool called RAT. The main idea is to use a PSL description which models the circuit and gate behaviors. For each circuit, the behavior correctness is formally checked with RAT. The gates are abstracted by their PSL properties. As the gates are assembled together to build a larger circuit, the...
Horus is a prototype environment for the support of assertion-based design. Formal properties, written in a standard (PSL or SVA) language, are automatically translated into synthesizable IP's, using a modular, efficient and proven correct method. The resulting monitors (for observing asserted properties) and generators (for generating constrained test vectors) are connected to the design under test,...
Modern assertion languages, such as PSL and SVA, include many constructs that are best handled by rewriting to a small set of base cases. Since previous rewrite attempts have shown that the rules could be quite involved, sometimes counterintuitive, and that they can make a significant difference in the complexity of interpreting assertions, workable procedures for proving the correctness of these...
The Horus tool, based on formally proven correct methods, provides a unified support to assertion-based design, between the specification and the test phases. Given a set of logical and temporal properties written in PSL, Horus automatically constructs a test environment for the design. This construction is fast, correct, and produces efficient monitors and generators. The size of the instrumented...
From an assumed property, which constrains the inputs of a design under test, we produce a RTL synthesizable design that generates compliant sequences of values for all the signals named in the property. Such generator can be connected to the design under test for verification by simulation or emulation. Experiments on our prototype tool show that the technique is efficient, and allows to test the...
We propose an efficient solution to automatically generate test vectors that satisfy an assumed property written in PSL. From a "foundation language" formula, we build a synthesizable generator that produces random temporal test vectors compliant with the formula. Generators are space and speed efficient when synthesized on FPGA, and their connection to the device under test is a portable...
We developed an original method to synthesize monitors from declarative specifications written in the PSL standard. Monitors observe sequences of values on their input signals, and check their conformance to a specified temporal expression. Our method implements both the weak and strong versions of PSL FL operators, and has been proven correct using the PVS theorem proven This paper discusses the...
PSL is a standard formal language to specify logic and temporal properties in a declarative style, under the form of assertions. We defined a library of components, and an interconnection method to automatically synthesize hardware monitors that can be linked to a prototype of the design under verification, thus providing an efficient debugging platform. The existing tool produces on-line checkers...
In the context of embedded systems design, the authors developed an original method for generating hardware that monitors signals whose behavior is specified by logical and temporal properties written in PSL. The method is based on a library of primitive digital components, and a technique to interconnect them, both formally proven correct with respect to the mathematical semantics of PSL. The resulting...
Set the date range to filter the displayed results. You can set a starting date, ending date or both. You can enter the dates manually or choose them from the calendar.