过分伤痛Abstract. We have developed the first hardware and software (intellectual property) metering scheme that enables reliable low overhead proofs for the number of manufactured parts and copied programs. The key idea is to make each design slightly different d
4.if (F’ is satisfiable)
F = F’ and goto step 1.
5.else
mark v and goto step 2.
We select variable v greedily in step 2 and modify the formula in step 3. We use SAT solver to solve the new SAT formula (the one without variable v), if we fail to find a truth assignment, we put v back and select the variable that has the second smallest c(v). If the new formula is still satisfiable, then we recalculate c(v) for the remainder variables in the modified formula F’ and select the next one. We continue this process until we find enough “don’t-cares” to create the desired number of different solutions.
7 Experimental Results
In this section we analyze the ability of the proposed metering scheme to generate a large pool of designs with unique ID. We first show our results for hardware metering. The last part of this section illustrates the analysis for the software metering approach.
Table 2 shows the results of the application of the scheme on generating numerous graph coloring (register assignment). The first column indicates the name of design from the Hyper benchmark suite [33]. The second and third column indicate the number of vari-ables and registers in the designs. Two final columns indicate the number of the unique solutions which can be obtained using the following two methods. The first one (column 4) is the assignment of exactly the same subset of variables to different registers in their physical instances. The last column indicates the number of different solutions produced using the technique presented in Section 5. In both cases, even for the smallest design, the number of solutions is very high. The key reason for this situation is that it is well known that the interval graphs for all known designs are very sparse and it is very easy to color them in many different ways using the minimal number of colors.
In order to test the technique in a much more demanding scenario, we applied the hardware metering scheme on the SAT problem. The experimental results are shown in Table 3. The first column indicates the name of DIMACS benchmark [12] and the middle column indicates the number of used variables. The last column indicates the number of solutions that were generated using the technique presented in Section 4. Although, the number of the generated solutions is smaller than in the case of graph coloring, it is still very large and much higher than required in any of today’s designs.
