Model Checking Formal Verification Methodology for Virtual Channel NoCs

2016 ◽  
Vol 850 ◽  
pp. 30-37
Author(s):  
Sherif Agamy ◽  
Ahmed Sayed ◽  
Rafik Guindi
Keyword(s):  
Model Checking ◽  
Formal Verification ◽  
Formal Methods ◽  
Virtual Channel ◽  
Time To Market ◽  
System On A Chip ◽  
Verification Methodology ◽  
Network On A Chip ◽  
Current Practices

The increasing complexity of System on a Chip (SOC) using Network on a Chip (NoC) results in significant increases in traditional verification times. Formal methods fully prove design properties, without deadline vs. coverage compromises, hence tremendously reducing time to market. In this work we use the CONNECT NOC to illustrate our new white box formal verification methodology. We develop constraints and assertions for properties verification. Our methodology is faster than the current methods; it also uncovered key gaps in current practices. In addition, our assertion checkers can be reused both in simulation and as monitors on silicon.

Formal Verification Methods

2015 ◽  
pp. 10-20
Keyword(s):  
Model Checking ◽  
Formal Verification ◽  
Formal Methods ◽  
Theorem Proving ◽  
Critical Systems ◽  
Verification Methods

This chapter provides a brief introduction to the domain of formal methods (Boca, Bowen, & Siddiqi, 2009) and the most commonly used verification methods (i.e., theorem proving [Harrison, 2009] and model checking [Baier & Katoen, 2008]). Due to their inherent precision, formal verification methods are increasingly being used in modeling and verifying safety and financial-critical systems these days.

The Role of Formal Methods in Software Development for Railway Applications

2014 ◽  
pp. 1103-1118
Author(s):  
Alessandro Fantechi
Keyword(s):  
Model Checking ◽  
Software Development ◽  
Formal Verification ◽  
Formal Methods ◽  
Industrial Application ◽  
Safety Certification ◽  
Software Designers ◽  
Recent Trends ◽  
Railway Domain

Formal methods for thirty years have promised to be the solution for the safety certification headaches of railway software designers. This chapter looks at the current industrial application of formal methods in the railway domain. After a recall of the dawning of formal methods in this domain, recent trends are presented that focus in particular on formal verification by means of model checking engines, with its potential and limitations. The paper ends with a perspective into the next future, in which formal methods will be expected to pervade in more respects the production of railway software and systems.

The Role of Formal Methods in Software Development for Railway Applications

2012 ◽  
pp. 282-297 ◽  
Author(s):  
Alessandro Fantechi
Keyword(s):  
Model Checking ◽  
Software Development ◽  
Formal Verification ◽  
Formal Methods ◽  
Industrial Application ◽  
Safety Certification ◽  
Software Designers ◽  
Recent Trends ◽  
Railway Domain

Formal methods for thirty years have promised to be the solution for the safety certification headaches of railway software designers. This chapter looks at the current industrial application of formal methods in the railway domain. After a recall of the dawning of formal methods in this domain, recent trends are presented that focus in particular on formal verification by means of model checking engines, with its potential and limitations. The paper ends with a perspective into the next future, in which formal methods will be expected to pervade in more respects the production of railway software and systems.

Formal verification of an industrial system-on-a-chip

2002 ◽  
Author(s):  
Hoon Choi ◽  
Myung-Kyoon Yim ◽  
Jae-Young Lee ◽  
Byeong-Whee Yun ◽  
Yun-Tae Lee
Keyword(s):  
Formal Verification ◽  
Industrial System ◽  
System On A Chip

scholarly journals A Unique Test Bench for Various System-on-a-Chip

2017 ◽  
Vol 7 (6) ◽  
pp. 3318 ◽  
Author(s):  
Sridevi Chitti ◽  
P. Chandrasekhar ◽  
M. Asharani
Keyword(s):  
Intellectual Property ◽  
Test Bench ◽  
General Purpose ◽  
Technology Tools ◽  
Automated Test ◽  
System On A Chip ◽  
Verification Process ◽  
Verification Methodology ◽  
Efficient Verification ◽  
State Of Art

This paper discusses a standard flow on how an automated test bench environment which is randomized with constraints can verify a SOC efficiently for its functionality and coverage. Today, in the time of multimillion gate ASICs, reusable intellectual property (IP), and system-on-a-chip (SoC) designs, verification consumes about 70 % of the design effort. Automation means a machine completes a task autonomously, quicker and with predictable results. Automation requires standard processes with well-defined inputs and outputs. By using this efficient methodology it is possible to provide a general purpose automation solution for verification, given today’s technology. Tools automating various portions of the verification process are being introduced. Here, we have Communication based SOC The content of the paper discusses about the methodology used to verify such a SOC-based environment. Cadence Efficient Verification Methodology libraries are explored for the solution of this problem. We can take this as a state of art approach in verifying SOC environments. The goal of this paper is to emphasize the unique testbench for different SOC using Efficient Verification Constructs implemented in system verilog for SOC verification.

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.

A Methodology for Automatic Formal Verification of Enterprise Architecture

2019 ◽  
Vol 10 (1) ◽  
pp. 1-19
Author(s):  
Eduard Babkin ◽  
Pavel Malyzhenkov ◽  
Marina Ivanova ◽  
Nikita Ponomarev
Keyword(s):  
Model Checking ◽  
Formal Verification ◽  
Iterative Process ◽  
Enterprise Architecture ◽  
Description Language ◽  
Architecture Description Language ◽  
Business Modeling ◽  
Business Alignment ◽  
Architecture Description ◽  
Software Prototype

For over a decade, IT-business alignment has been ranked as a top-priority management concern, but there is little research on practical ways to achieve the alignment. EA development is a continuous iterative process, which implicitly ensures the achievement of a specific IT-business alignment level. Therefore, it is necessary to formalize the requirements for architecture and be able to automatically verify them. The authors propose a new methodology for detecting logical contradictions in enterprise architecture models based on a model checking approach adopted in the context of business modeling. In such a methodology, they use ArchiMate standard for a conceptual enterprise architecture description language which is fully aligned with TOGAF. The authors also offer several important verification queries and demonstrate practical applicability of their approach using a software prototype of the modeling tool which exploits MIT Alloy Analyzer model checking framework integrated with AchiMate Archi workbench.

scholarly journals A Network Adaptive Fault-Tolerant Routing Algorithm for Demanding Latency and Throughput Applications of Network-on-a-Chip Designs

Electronics ◽  
2020 ◽  
Vol 9 (7) ◽  
pp. 1076 ◽  
Author(s):  
Zulqar Nain ◽  
Rashid Ali ◽  
Sheraz Anjum ◽  
Muhammad Khalil Afzal ◽  
Sung Won Kim
Keyword(s):  
Fault Tolerant ◽  
Current System ◽  
Routing Algorithm ◽  
Adaptive Routing ◽  
Traffic Load ◽  
Delivery Ratio ◽  
Processing Elements ◽  
System On A Chip ◽  
On Chip ◽  
Network On A Chip

Scalability is a significant issue in system-on-a-chip architectures because of the rapid increase in numerous on-chip resources. Moreover, hybrid processing elements demand diverse communication requirements, which system-on-a-chip architectures are unable to handle gracefully. Network-on-a-chip architectures have been proposed to address the scalability, contention, reusability, and congestion-related problems of current system-on-a-chip architectures. The reliability appears to be a challenging aspect of network-on-a-chip architectures because of the physical faults introduced in post-manufacturing processes. Therefore, to overcome such failures in network-on-a-chip architectures, fault-tolerant routing is critical. In this article, a network adaptive fault-tolerant routing algorithm is proposed, where the proposed algorithm enhances an efficient dynamic and adaptive routing algorithm. The proposed algorithm avoids livelocks because of its ability to select an alternate outport. It also manages to bypass congested regions of the network and balances the traffic load between outports that have an equal number of hop counts to its destination. Simulation results verified that in a fault-free scenario, the proposed solution outperformed a fault-tolerant XY by achieving a lower latency. At the same time, it attained a higher flit delivery ratio compared to the efficient dynamic and adaptive routing algorithm. Meanwhile, in the situation of a faulty network, the proposed algorithm could reach a higher flit delivery ratio of up to 18% while still consuming less power compared to the efficient dynamic and adaptive routing algorithm.

Sign in / Sign up

Export Citation Format

Share Document