how to "Formally" verify arithmetic blocks such as 16 bit+ adders and multipliers

[kaaliakahn]

I am looking for latest formal methods of verifying arithmetic blocks such as large 16 bits or more multipliers, adders and other arithmetic blocks.

Secondly, how to do formal verification of a synthesized gate-level netlist say of a 16 bit or 32 bit multiplier.

Any insight, examples, methodology or white papers shall be highly appreciated.

Thanks and Kind Regards,

[kaaliakahn]

No one? Really !!!

[daniel_payne]

A quick Google search produces thousands of results: https://www.google.com/search?ix=tea...ion+multiplier

[kaaliakahn]

Daneil

I know this area a bit. All the solutions that i have seen suffer from scalability issues as formal techniques can not deal with large state space.

[lingcore]

Daneil

I know this area a bit. All the solutions that i have seen suffer from scalability issues as formal techniques can not deal with large state space.

Here is an introduction paper on theorem-prover based formal method:

G. Chen and F. Liu, Proofs of correctness and properties of integer adder circuits,
in IEEE Transactions on Computers, Vol. 59, No. 1, Jan., 2010.

[kaaliakahn]

Thanks lingcore. I have seen this paper before.

If you know any papers on formally verifying multipliers, please let me know.

THanks

Kind Regards,

[lingcore]

Thanks lingcore. I have seen this paper before.

If you know any papers on formally verifying multipliers, please let me know.

THanks

Kind Regards,

There are plenty of them. An earlier paper is:
Circuits as streams in Coq: Verification of a sequential multiplier
by Christine Paulin-Mohring

[kaaliakahn]

Thanks lingcore encore (which means again)

Could you list an easier paper which goes beyond theorem proving.

[UlricWihey]

I have seen suffer can not deal with large state space.



Good to the last second--DVD sales online.

[larditi]

Automatic (i.e. non theorem-proving based) techniques can verify adders, comparators, etc. even if they are huge. Most commercial and free tools do that.
Multipliers and dividers are more tricky. Some techniques such as using *BMDs (Binary Moment Diagrams) have been popular some 15 years ago for that.