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.
Name Last modified Size Description
![[ ]](/icons/compressed.gif)
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