Verification of behavioral descriptions by combining symbolic simulation and automatic reasoning
Ghiath Al Sammane, D. Borrione, Remy Chevallier · 2005
We present a property verification method for behavioral descriptions with TheoSim, a tool that combines symbolic simulation and automatic reasoning. The effectiveness of the method is illustrated on the verification of SPSMALL, a memory designed by STMicroelectronics. The proof of correctness was established independently of the memory size.