ALU Chip Verification Instances

These instances are IP models of property checking problems on a very simple arithmetic logical unit (ALU). The name of each model denotes the number of bits of each input register, and the number of the property.

The property checking problem is to prove that a given property of the chip design holds, or to generate a counter-example. The IP model is infeasible, iff the property holds. Each feasible solution in the IP model represents a counter-example of the property.

The properties 1 to 8 are valid, meaning that instances alu*_1.mps to alu*_8.mps are infeasible. Property 9 is invalid, and instances alu*_9.mps are feasible.

In the file alumodel.tgz, we provide the original chip design implemented in the hardware programming language SMV. There is also a C implementation of a SMV -> IP converter together with script files for compiling and running the code.

Note that the ALU design includes signed and unsigned multiplication of the two input registers. Therefore, intermediate calculations are performed on integer variables with upper bound in the range of 2^(2n). Some of the coefficients in the constraint matrix are in the same range. Thus, the instances tend to produce major numerical difficulties. With feasibility tolerances set to 10^(-9), the 10-bit instances should be solveable.

Icon  Name                    Last modified      Size  Description
[   ] aluinstances.tgz 23-May-2005 10:32 1.3M [   ] alumodel.tgz 23-May-2005 10:20 217K [   ] alu18_8.mps.gz 23-May-2005 10:18 15K MPS format instance [   ] alu18_9.mps.gz 23-May-2005 10:18 15K MPS format instance [   ] alu16_8.mps.gz 23-May-2005 10:18 14K MPS format instance [   ] alu18_7.mps.gz 23-May-2005 10:18 14K MPS format instance [   ] alu16_9.mps.gz 23-May-2005 10:18 14K MPS format instance [   ] alu14_8.mps.gz 23-May-2005 10:18 14K MPS format instance [   ] alu14_9.mps.gz 23-May-2005 10:18 13K MPS format instance [   ] alu16_7.mps.gz 23-May-2005 10:18 13K MPS format instance [   ] alu18_5.mps.gz 23-May-2005 10:18 13K MPS format instance [   ] alu18_6.mps.gz 23-May-2005 10:18 13K MPS format instance [   ] alu18_2.mps.gz 23-May-2005 10:18 13K MPS format instance [   ] alu12_8.mps.gz 23-May-2005 10:18 13K MPS format instance [   ] alu18_4.mps.gz 23-May-2005 10:18 13K MPS format instance [   ] alu18_1.mps.gz 23-May-2005 10:18 13K MPS format instance [   ] alu18_3.mps.gz 23-May-2005 10:18 13K MPS format instance [   ] alu14_7.mps.gz 23-May-2005 10:18 13K MPS format instance [   ] alu12_9.mps.gz 23-May-2005 10:18 13K MPS format instance [   ] alu16_5.mps.gz 23-May-2005 10:18 13K MPS format instance [   ] alu16_6.mps.gz 23-May-2005 10:18 13K MPS format instance [   ] alu10_8.mps.gz 23-May-2005 10:18 13K MPS format instance [   ] alu16_4.mps.gz 23-May-2005 10:18 13K MPS format instance [   ] alu16_2.mps.gz 23-May-2005 10:18 12K MPS format instance [   ] alu16_1.mps.gz 23-May-2005 10:18 12K MPS format instance [   ] alu9_8.mps.gz 23-May-2005 10:18 12K MPS format instance [   ] alu10_9.mps.gz 23-May-2005 10:18 12K MPS format instance [   ] alu16_3.mps.gz 23-May-2005 10:18 12K MPS format instance [   ] alu12_7.mps.gz 23-May-2005 10:18 12K MPS format instance [   ] alu14_5.mps.gz 23-May-2005 10:18 12K MPS format instance [   ] alu14_6.mps.gz 23-May-2005 10:18 12K MPS format instance [   ] alu9_9.mps.gz 23-May-2005 10:18 12K MPS format instance [   ] alu14_4.mps.gz 23-May-2005 10:18 12K MPS format instance [   ] alu14_2.mps.gz 23-May-2005 10:18 12K MPS format instance [   ] alu14_1.mps.gz 23-May-2005 10:18 12K MPS format instance [   ] alu14_3.mps.gz 23-May-2005 10:18 12K MPS format instance [   ] alu10_7.mps.gz 23-May-2005 10:18 12K MPS format instance [   ] alu12_6.mps.gz 23-May-2005 10:18 12K MPS format instance [   ] alu12_5.mps.gz 23-May-2005 10:18 12K MPS format instance [   ] alu8_8.mps.gz 23-May-2005 10:18 12K MPS format instance [   ] alu12_4.mps.gz 23-May-2005 10:18 12K MPS format instance [   ] alu9_7.mps.gz 23-May-2005 10:18 12K MPS format instance [   ] alu12_2.mps.gz 23-May-2005 10:18 12K MPS format instance [   ] alu10_5.mps.gz 23-May-2005 10:18 12K MPS format instance [   ] alu8_9.mps.gz 23-May-2005 10:18 12K MPS format instance [   ] alu7_8.mps.gz 23-May-2005 10:18 12K MPS format instance [   ] alu10_6.mps.gz 23-May-2005 10:18 12K MPS format instance [   ] alu12_1.mps.gz 23-May-2005 10:18 12K MPS format instance [   ] alu12_3.mps.gz 23-May-2005 10:18 12K MPS format instance [   ] alu9_5.mps.gz 23-May-2005 10:18 11K MPS format instance [   ] alu9_6.mps.gz 23-May-2005 10:18 11K MPS format instance [   ] alu10_4.mps.gz 23-May-2005 10:18 11K MPS format instance [   ] alu7_9.mps.gz 23-May-2005 10:18 11K MPS format instance [   ] alu10_2.mps.gz 23-May-2005 10:18 11K MPS format instance [   ] alu10_1.mps.gz 23-May-2005 10:18 11K MPS format instance [   ] alu10_3.mps.gz 23-May-2005 10:18 11K MPS format instance [   ] alu8_7.mps.gz 23-May-2005 10:18 11K MPS format instance [   ] alu6_8.mps.gz 23-May-2005 10:18 11K MPS format instance [   ] alu9_4.mps.gz 23-May-2005 10:18 11K MPS format instance [   ] alu9_2.mps.gz 23-May-2005 10:18 11K MPS format instance [   ] alu5_8.mps.gz 23-May-2005 10:18 11K MPS format instance [   ] alu9_1.mps.gz 23-May-2005 10:18 11K MPS format instance [   ] alu8_5.mps.gz 23-May-2005 10:18 11K MPS format instance [   ] alu9_3.mps.gz 23-May-2005 10:18 11K MPS format instance [   ] alu6_9.mps.gz 23-May-2005 10:18 11K MPS format instance [   ] alu8_6.mps.gz 23-May-2005 10:18 11K MPS format instance [   ] alu7_7.mps.gz 23-May-2005 10:18 11K MPS format instance [   ] alu5_9.mps.gz 23-May-2005 10:18 11K MPS format instance [   ] alu7_5.mps.gz 23-May-2005 10:18 11K MPS format instance [   ] alu7_6.mps.gz 23-May-2005 10:18 11K MPS format instance [   ] alu8_4.mps.gz 23-May-2005 10:18 11K MPS format instance [   ] alu8_2.mps.gz 23-May-2005 10:18 11K MPS format instance [   ] alu8_1.mps.gz 23-May-2005 10:18 11K MPS format instance [   ] alu8_3.mps.gz 23-May-2005 10:18 11K MPS format instance [   ] alu6_7.mps.gz 23-May-2005 10:18 11K MPS format instance [   ] alu7_4.mps.gz 23-May-2005 10:18 11K MPS format instance [   ] alu4_8.mps.gz 23-May-2005 10:18 11K MPS format instance [   ] alu6_6.mps.gz 23-May-2005 10:18 11K MPS format instance [   ] alu6_5.mps.gz 23-May-2005 10:18 11K MPS format instance [   ] alu7_2.mps.gz 23-May-2005 10:18 11K MPS format instance [   ] alu5_5.mps.gz 23-May-2005 10:18 11K MPS format instance [   ] alu7_1.mps.gz 23-May-2005 10:18 11K MPS format instance [   ] alu5_7.mps.gz 23-May-2005 10:18 11K MPS format instance [   ] alu7_3.mps.gz 23-May-2005 10:18 11K MPS format instance [   ] alu5_6.mps.gz 23-May-2005 10:18 11K MPS format instance [   ] alu4_9.mps.gz 23-May-2005 10:18 11K MPS format instance [   ] alu6_4.mps.gz 23-May-2005 10:18 11K MPS format instance [   ] alu6_2.mps.gz 23-May-2005 10:18 10K MPS format instance [   ] alu6_1.mps.gz 23-May-2005 10:18 10K MPS format instance [   ] alu5_4.mps.gz 23-May-2005 10:18 10K MPS format instance [   ] alu6_3.mps.gz 23-May-2005 10:18 10K MPS format instance [   ] alu5_2.mps.gz 23-May-2005 10:18 10K MPS format instance [   ] alu5_1.mps.gz 23-May-2005 10:18 10K MPS format instance [   ] alu4_5.mps.gz 23-May-2005 10:18 10K MPS format instance [   ] alu5_3.mps.gz 23-May-2005 10:18 10K MPS format instance [   ] alu4_6.mps.gz 23-May-2005 10:18 10K MPS format instance [   ] alu4_7.mps.gz 23-May-2005 10:18 10K MPS format instance [   ] alu4_4.mps.gz 23-May-2005 10:18 10K MPS format instance [   ] alu4_2.mps.gz 23-May-2005 10:18 10K MPS format instance [   ] alu4_1.mps.gz 23-May-2005 10:18 10K MPS format instance [   ] alu4_3.mps.gz 23-May-2005 10:18 10K MPS format instance