Semiwiki on LinkedIn Semiwiki on Facebook Semiwiki on Twitter Register / Log in 
Array
(
    [content] => 
    [params] => Array
        (
            [0] => /forum/threads/how-to-formally-verify-arithmetic-blocks-such-as-16-bit-adders-and-multipliers.1433/
        )

    [addOns] => Array
        (
            [DL6/MLTP] => 13
            [Hampel/TimeZoneDebug] => 1000070
            [SV/ChangePostDate] => 2010200
            [SemiWiki/Newsletter] => 1000010
            [SemiWiki/WPMenu] => 1000010
            [SemiWiki/XPressExtend] => 1000010
            [ThemeHouse/XLink] => 1000970
            [ThemeHouse/XPress] => 1010570
            [XF] => 2021770
            [XFI] => 1050270
        )

    [wordpress] => /var/www/html
)

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

K

kaaliakahn

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

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,
 
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.
 
kaaliakahn said:
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.
Click to expand...

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

G. Chen</SPAN> and F. Liu, </SPAN>Proofs of correctness and properties of integer adder circuits, </SPAN> </SPAN>
in IEEE Transactions on Computers, Vol. 59, No. 1, Jan., 2010.</SPAN></SPAN>
 
Thanks lingcore. I have seen this paper before.

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

THanks

Kind Regards,
 
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.
 
larditi

could you name the commercial and free tools for adders and comparators that you are talking about.

THanks

Kind Regards,
tariq
 
I prefer not to name tools on this forum. But Google for hardware formal verification, model checking, property checking, etc.
 
You must log in or register to reply here.
Back
Top