systemverilog assertion for a 3x3 unsigned gate-level multiplier

[kaaliakahn]

[h=2][/h]

Hi
I am wondering if the following assertion completely describes the behavior of a 3x3 unsigned gate-level multiplier at the bit level.

The idea is the following. A 3x3 unsigned multiplier with 3 bit inputs "a" and "b" and 6 bit output "out" can be thought of as an adder that can add "
a" 0 to 7 times OR an adder that can add "b" 0 to 7 times. With this in mind, can i NOT write a systemverilog assertion like the following??

mult_propc: assert property (
@ (posedge clk)
disable iff(~rst_n)
out == 0 ||
1*(a[0] + 2*a[1] + 4*a[2]) &&
2*(a[0] + 2*a[1] + 4*a[2]) &&
3*(a[0] + 2*a[1] + 4*a[2]) &&
4*(a[0] + 2*a[1] + 4*a[2]) &&
5*(a[0] + 2*a[1] + 4*a[2]) &&
6*(a[0] + 2*a[1] + 4*a[2]) &&
7*(a[0] + 2*a[1] + 4*a[2]) &&
1*(b[0] + 2*b[1] + 4*b[2]) &&
2*(b[0] + 2*b[1] + 4*b[2]) &&
3*(b[0] + 2*b[1] + 4*b[2]) &&
4*(b[0] + 2*b[1] + 4*b[2]) &&
5*(b[0] + 2*b[1] + 4*b[2]) &&
6*(b[0] + 2*b[1] + 4*b[2]) &&
7*(b[0] + 2*b[1] + 4*b[2])

);


I coded the property this way and tried it on 3x3 unsigned multiplier using Cadence Incisive formal verifier and it PASSED.

If you feel there is a discrepancy, please educate me or where do you think this assertion might fail?

Thanks a lot​

 

[Daniel Payne]

I think that you are looking at this assertion from too low of a level. Look at the snippet in this book for writing assertions on a multiplier.

 

[kaaliakahn]

Daniel, thanks for your comment

My previous approach is wrong and confusing.

Here is an approach that works till 8x8 multipliers. For 16x16, formal tools give up because of the scalability issues


mult_propc: assert property ( //coded for unsigned 3x3 multiplier
@ (posedge clk)
disable iff(~rst_n)
cout == (~b[2]& ~b[1]& ~b[0])*0*(a[0] + 2*a[1] + 4*a[2]) |
(~b[2]& ~b[1]& b[0])*1*(a[0] + 2*a[1] + 4*a[2]) |
(~b[2]& b[1]& ~b[0])*2*(a[0] + 2*a[1] + 4*a[2]) |
(~b[2]& b[1]& b[0])*3*(a[0] + 2*a[1] + 4*a[2]) |
(b[2]& ~b[1]& ~b[0])*4*(a[0] + 2*a[1] + 4*a[2]) |
(b[2]& ~b[1]& b[0])*5*(a[0] + 2*a[1] + 4*a[2]) |
(b[2]& b[1]& ~b[0])*6*(a[0] + 2*a[1] + 4*a[2]) |
(b[2]& b[1]& b[0])* 7 * (a[0] + 2*a[1] + 4*a[2]);