Automated Generation of Synchronous Formal Models from SystemC Descriptions

2019 ◽  
Vol 28 (04) ◽  
pp. 1950061 ◽  
Author(s):  
Hamoudi Kalla ◽  
David Berner ◽  
Jean-Pierre Talpin
Keyword(s):  
Formal Verification ◽  
Structural Information ◽  
Electronic System ◽  
Design Flow ◽  
Theorem Prover ◽  
System Level ◽  
Original Structure ◽  
Automated Generation ◽  
Synchronous Language ◽  
Verification Techniques

SystemC is one of the most popular electronic system-level design language and it is embraced by a growing community that seeks to move to a higher level of abstraction. It lacks however a standard way of integrating formal methods and formal verification techniques into a SystemC design flow. In this paper, we show how SystemC descriptions are automatically transformed into the formal synchronous language Signal, while conserving the original structure and enabling the application of formal verification techniques. Signal provides a simple semantics of concurrency and time, and allows verification with an existing theorem prover and model checker. The approach that we propose consists of two steps: the extraction of the structure and the transformation of the behavior. In the first step, SystemC model is analyzed and the structural information is extracted. In the second step, for each SystemC module, the corresponding Signal behavior is generated and filled into the already prepared Signal structure.

scholarly journals Task-Level Data Model for Hardware Synthesis Based on Concurrent Collections

2012 ◽  
Vol 2012 ◽  
pp. 1-24
Author(s):  
Jason Cong ◽  
Karthik Gururaj ◽  
Peng Zhang ◽  
Yi Zou
Keyword(s):  
Data Model ◽  
Electronic System ◽  
Design Flow ◽  
System Level ◽  
Hardware Synthesis ◽  
Synthesis Design ◽  
Electronic System Level ◽  
Level Data ◽  
Modeling Task ◽  
Task Level

The ever-increasing design complexity of modern digital systems makes it necessary to develop electronic system-level (ESL) methodologies with automation and optimization in the higher abstraction level. How the concurrency is modeled in the application specification plays a significant role in ESL design frameworks. The state-of-art concurrent specification models are not suitable for modeling task-level concurrent behavior for the hardware synthesis design flow. Based on the concurrent collection (CnC) model, which provides the maximum freedom of task rescheduling, we propose task-level data model (TLDM), targeted at the task-level optimization in hardware synthesis for data processing applications. Polyhedral models are embedded in TLDM for concise expression of task instances, array accesses, and dependencies. Examples are shown to illustrate the advantages of our TLDM specification compared to other widely used concurrency specifications.

Formal Verification of Control System Software

2019 ◽  
Author(s):  
Pierre-Loïc Garoche
Keyword(s):  
Control System ◽  
Formal Verification ◽  
Formal Analysis ◽  
Critical Systems ◽  
System Software ◽  
Unified Approach ◽  
Verification Methods ◽  
Autonomous Cars ◽  
Computer Scientists ◽  
Verification Techniques

The verification of control system software is critical to a host of technologies and industries, from aeronautics and medical technology to the cars we drive. The failure of controller software can cost people their lives. This book provides control engineers and computer scientists with an introduction to the formal techniques for analyzing and verifying this important class of software. Too often, control engineers are unaware of the issues surrounding the verification of software, while computer scientists tend to be unfamiliar with the specificities of controller software. The book provides a unified approach that is geared to graduate students in both fields, covering formal verification methods as well as the design and verification of controllers. It presents a wealth of new verification techniques for performing exhaustive analysis of controller software. These include new means to compute nonlinear invariants, the use of convex optimization tools, and methods for dealing with numerical imprecisions such as floating point computations occurring in the analyzed software. As the autonomy of critical systems continues to increase—as evidenced by autonomous cars, drones, and satellites and landers—the numerical functions in these systems are growing ever more advanced. The techniques presented here are essential to support the formal analysis of the controller software being used in these new and emerging technologies.

scholarly journals Fast equivalence -- checking for quantum circuits

2010 ◽  
Vol 10 (9&10) ◽  
pp. 721-734
Author(s):  
Shigeru Yamashita ◽  
Igor L. Markov
Keyword(s):  
Formal Verification ◽  
Quantum Algorithms ◽  
Quantum Circuits ◽  
Equivalence Checking ◽  
Sat Solvers ◽  
Reversible Circuits ◽  
Verification Tools ◽  
Verification Methodology ◽  
Verification Techniques ◽  
Factoring Algorithm

We perform formal verification of quantum circuits by integrating several techniques specialized to particular classes of circuits. Our verification methodology is based on the new notion of a reversible miter that allows one to leverage existing techniques for simplification of quantum circuits. For reversible circuits which arise as runtime bottlenecks of key quantum algorithms, we develop several verification techniques and empirically compare them. We also combine existing quantum verification tools with the use of SAT-solvers. Experiments with circuits for Shor's number-factoring algorithm, containing thousands of gates, show improvements in efficiency by four orders of magnitude.

PSK Transciever designing using SystemVue

2019 ◽  
Vol 3 (1) ◽  
Author(s):  
Deepali Chaurasia
Keyword(s):  
Signal Processing ◽  
System Integration ◽  
Communication Systems ◽  
Energy Savings ◽  
Electronic Devices ◽  
Physical Space ◽  
Electronic System ◽  
System Level ◽  
Complex Nature ◽  
Wide Range

Since, the industrial electronics is trending towards more compact components and system integration, innovative products offering greater flexibility, quality, safety, reliability, energy savings, wide range of connectivity with long operating lifetime. Now, Electronics is widely used in information processing, telecommunication and signal processing. Due to the complex nature of electronics theory, laboratory experimentation is an important part of development of electronic devices. These experiments are used to test or verify the proposed design and detect errors. Historically, electronics labs have consisted of electronic devices and equipment located in the physical space. Although in more recent years, the trend has been towards electronics lab simulation softwares and SystemVue is also one of them. SystemVue is a focussed electronic design automation (EDA) environment for electronic system-level (ESL) design. It enables system architects and algorithm developers to innovate the physical layer (PHY) of wireless and aerospace/defence communication systems and provide unique value to RF, DSP and FPGA/ASIC implementers. As a dedicated platform for ESL design and signal processing realization, SystemVue replaces general-purpose digital, analog and math environments. SystemVue “speaks RF”, cuts PHY development and verification time in half and connects to your mainstream EDA flow.

Sign in / Sign up

Export Citation Format

Share Document