Free Online Productivity Tools
i2Speak
i2Symbol
i2OCR
iTex2Img
iWeb2Print
iWeb2Shot
i2Type
iPdf2Split
iPdf2Merge
i2Bopomofo
i2Arabic
i2Style
i2Image
i2PDF
iLatex2Rtf
Sci2ools

VLSID

2002

IEEE

2002

IEEE

Satisfiability of complex word-level formulas often arises as a problem in formal verification of hardware designs described at the register transfer level (RTL). Even though most designs are described in a hardware description language (HDL), like Verilog or VHDL, usually this problem is solved in the Boolean domain, using Boolean solvers. These engines often show a poor performance for data path verification. Instead of solving the problem at the bit-level, a method is proposed to transform conjunctions of bitvector equalities and inequalities into sets of integer linear arithmetic constraints. It is shown that it is possible to correctly model the modulo semantics of HDL operators as linear constraints. Integer linear constraint solvers are used as a decision procedure for bitvector arithmetic. In the implementation we focus on verification of arithmetic properties of Verilog-HDL designs. Experimental results show considerable performance advantages over high-end Boolean SAT solver...

Related Content

Added |
01 Dec 2009 |

Updated |
01 Dec 2009 |

Type |
Conference |

Year |
2002 |

Where |
VLSID |

Authors |
Raik Brinkmann, Rolf Drechsler |

Comments (0)