<script type="text/javascript">
<!--
document.write('<div id="oa_widget"></div>');
document.write('<script type="text/javascript" src="https://www.openaire.eu/index.php?option=com_openaire&view=widget&format=raw&projectId=undefined&type=result"></script>');
-->
</script>

COPY SCRIPT

For further information contact us at helpdesk@openaire.eu

Checkers in Formal Verification

Name: Checkers in Formal Verification
Keywords: 2. Zero hunger, 16. Peace & justice

descriptionPublicationkeyboard_double_arrow_right Part of book or chapter of book , Other literature type 01 Jan 2010 English Publisher:Springer US

Authors: Eduard Cerny; Dmitry Korchemny; Surrendra Dudani; John Havlicek;

doi: 10.1007/978-1-4419-6600-1_22 , 10.1007/978-3-319-07139-8_23

Checkers in Formal Verification

- Summary
- Metrics

Abstract

This chapter continues the description of checkers started in Chap 9. It focuses on the application of checkers to formal verification—composing non-deterministic abstract models. The main feature in checkers supporting non-determinism are free variables, which are introduced in this chapter. We also introduce a special case of free variables: constant free variables, also called rigid variables. We show how free and rigid variables can be used as an alternative to local variables, and discuss advantages and drawbacks of each approach. Another topic addressed in this chapter is the use of checkers as a synthesizable testbench—a DUT environment model supported both in simulation and in formal verification.

Related Organizations

Cadence Design Systems (United States)
United States
Intel (United States)
United States
Synopsys (Switzerland)
Switzerland

Impact byBIP!

	citations This is an alternative to the "Influence" indicator, which also reflects the overall/total impact of an article in the research community at large, based on the underlying citation network (diachronically).	0
	popularity This indicator reflects the "current" impact/attention (the "hype") of an article in the research community at large, based on the underlying citation network.	Average
	influence This indicator reflects the overall/total impact of an article in the research community at large, based on the underlying citation network (diachronically).	Average
	impulse This indicator reflects the initial momentum of an article directly after its publication, based on the underlying citation network.	Average