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