IEEE CEDA / Taiwan MOE, ICCAD 2016 Contest

I. Introduction

    Boolean Matching [1,2] is one of the most widely-used engines in industrial applications and most widely-studied engines in academic research. Basic Boolean matching is for NPNP-equivalence, which negates (N) and permutes (P) circuit inputs and outputs to achieve circuit equivalences. In this contest, we extend the problem more closely to recent industrial challenges from two directions, Non-exact and Projective. The goal of non-exact is to achieve the largest number of output equivalences; projective extends the matching that allows grouping to match another design. Therefore, Non-exact Projective NPNP (NP3) Boolean matching is a problem to find input-groups of two designs for achieving maximum equivalent output-groups as shown in Figure 1. Beyond the basic NPNP Boolean matching, it could be used for achieving better quality and applied to related applications, such as library binding [3], synthesis [4,5], engineering change order [6,7], logic verification [8], and hardware Trojan detection [9]. In our application, the main issue is to find appropriate input-groups, so the number of circuit outputs in a circuit will be limited to 1~16 in this contest.

Fig.1 NP3 Boolean matching

    In recent academic research, the methods of basic Boolean matching are developed in several approaches including structure-based, simulation-based, and formal methods [2-16]. Each approach has its own advantages and limitations. In our topic, NP3 Boolean matching is an extension of the basic one and can bring more significant values for research in next generation.

II. Contest Objectives

    The objective of the contest is to develop a more flexible and powerful Boolean matching engine that can be widely utilized in industry tools. We will provide industrial benchmarks which can represent our challenging problems in diverse applications. We look forward to milestone ideas to achieve optimal matching and bring about new topics in this research area.

III. FORMAL PROBLEM DEFINITION AND INPUT/OUTPUT FORMAT

    Given two combinational circuits, contestants need to find the matching groups of their inputs and outputs that will achieve the largest number of equivalent output groups. A matching group consists of corresponding merged inputs along with their phase, or the inputs which should be set to constants. For example, given two circuits in Figure 2, the first circuit has output functions $ \{ f_1=(a \land c),f_2=(a \lor (b \land c)) \}$, and the second circuit has output functions $ \{ h_1=(x \lor (-y \land z)),h2=(x \land u) \}$. In order to achieve the most equivalent output-groups, the matching groups could be $(a,x), (b,-y), (c,u,z), (f_1,h_2), (f_2,h_1)$ thereby achieving two equivalences$(f_1 == h_2)$and$(f_2 == h_1)$. However, if the matching groups are $(a,-y), (b,u), (c,z), (x=0), (f_1,h_1), (f_2,h_2)$, only one equivalence$(f_1==h_1)$is achieved.

Fig.2

In addition, there are some limitations for grouping:

1. Every matching group can have only one input or output of the first circuit.
2. Contestants cannot bind the inputs of the first circuit to constants.
3. One circuit input/output can exist in at most one group.

Program Requirements

    The requested program should run in a Linux system with a single thread (multiple threads or processes are not allowed). The time limit of running each test case is 1800 seconds in CPU time. The executable file should be named “bmatch” and accepts three arguments:

./bmatch <cir1.v> <cir2.v> <match.out>

<cir1.v> <cir2.v> are input files which describe a Verilog circuit individually. <match.out> is an output file where contestants answer the matching groups.

Input Format

<cir1.v> <cir2.v> is gate-level circuit which has only one module with primitive gates in Verilog. Notice that there may be same name token between <cir1.v> and <cir2.v>.

modeule <cir_name> ( <name0>, <name1>, … );
input <name0>, <name1>, …;
output <name0>, <name1>,…;
wire <name0>, <name1> , …;
<primitive gate type> ( <name0>, <name1>, … );
<primitive gate type> ( <name0>, <name1>, … );
…
endmodule

Output Format

<match.out> includes three kinds of matching groups: INGROUP, OUTGROUP, and CONST0GROUP.

1. An INGROUP is the matching group of circuit inputs in both circuits. Its format is:

   INGROUP 1 + <name0>
   2 + <name1>
   2 - <name2>
   2 + <name3>
   …
   END

   The first character of each line is “1” or “2” which means the circuit input is from <cir1.v> or <cir2.v>. The second character is “+” or “-“ which means positive or negative phase. The last string <name0> is the name of a circuit input. Here are some limitation rules for grouping.

   1. A group must include exactly one name of circuit input in . For example, it cannot be:

      One INGROUP
      1 + name0
      1 + name1
      2 + name2
      END

   2. One circuit input’s name can exist in at most one group. For example, it cannot be:

      INGROUP
      1 + name0
      2 + name1
      END
      INGROUP
      1 + name2
      2 + name1
      END
      

2. An OUTGROUP is the matching group of circuit outputs in both circuits. Its format is:

   OUTGROUP
   1 + <name0>
   2 + <name1>
   2 - <name2>
   2 + <name3>
   …
   END
   

   The first character of each line is “1” or “2” which means the circuit output is from <cir1.v> or <cir2.v>. The second character is “+” or “-“ which means positive or negative phase. The last string is the name of a circuit output. Here are some limitation rules for grouping:

   1. A group must include exactly one name of circuit output in <cir1.v>
   2. One circuit output’s name can exist in at most one group.


3. CONST0GROUP is a group of binding <cir2.v> circuit inputs to constants. There can be at most one CONST0GROUP in <match.out>. Its format is;

   CONST0GROUP
   2 + <name0>
   2 - <name1>
   2 + <name2>
   …
   END
   

   The first character is “2” which means it is in <cir2.v>. The second character is “+” or “-“ which means positive or negative phase to bind the constant. “2 + <name0>” is to bind to constant 0.”2 - <name1>” is to bind <name1> to constant 1. Here are some limitation rules for grouping:

   1. Only circuit inputs in <cir2.v> are allowed to be in this group. There cannot be any circuit input of <cir1.v> or any circuit output of <cir1.v> and <cir2.v> in this group. For example, it cannot be:

      CONST0GROUP
      1 + name0
      END
      

   2. If one name exists in this group, it cannot exist in other groups (including an INGROUP and an OUTGROUP). For example, it cannot be:

      CONST0GROUP
      2 + name0
      END
      INGROUP
      1 + name1
      2 + name0
      END
      

IV. Evaluation Methodology

    In this problem, matching pairs between two designs are most important. Merging outputs and efficiency are the secondary considerations. Hence, we design an evaluation methodology as follows.

    The score of each case is calculated based on the scores of OUTGROUPs. If an OUTGROUP has any non-equivalence, there is no score for this group. If circuit outputs in OUTGROUP are all pair-wise equivalent, the score is 10 + N where N is the number of circuit outputs. The summation of the scores of output groups is the score of this case. The summation of the scores of all cases is the score of your result. The team with the highest score wins the contest.

    For example, given a in <cir1.v> and x, y in <cir2.v>, $a == x == y$. The matching group $(a,x)$ can get a score 10 + 2 = 12. The matching group $(a,x,y)$ can get a score 10 + 3 = 13. However, if $a \neq y$, the matching group $(a,x,y)$ will get a score 0, but the matching group $(a,x)$ still get a score 12.

    If two teams have the same score, the rank will be decided by the total runtime of all cases. If a case runs longer than the time limit of 1800 seconds and there is no , this case will get a score 0 and have a runtime of 1800 seconds. Also, a crash case is evaluated to have a runtime of 1800 seconds.

V. Example

    Given a case with two designs:

cir1.v	cir2.v
module top( a, b, c, g, f, h ); input a, b, c;, output g, f, h; and ( f, a, b ); or ( h, a, c ); xor ( g, f, h ); endmodule	module top( s, t, u, v, w, x, y, z ); input s, t, u, v, w; output x, y, z; wire tn; not ( tn, t ); and ( x, w, v, tn ); or ( y, w, u, tn ); xor ( z, y, s ); endmodule

    Team A:

$t$ is negatively grouped with w, and s is bind to constant 1, so$f==x$and$h==y==-z$.
The score is (10+2) + (10+3) = 25, where(10+2) is from $f==x$ and (10+3) is from $h==y==-z$.

    Team B:

$f==x$ and $h==y$ are correct.Hence, Team B gets the score (10+2) + (10+2) = 24.

    Team C:

$f==x$ and $h==y$ are correct, but $f==z$ is incorrect.Hence, Team C only get score 12 from $h==y$.

Team Ranking:1. Team A ( score 25 ) 2. Team B ( score 24 ) 3. Team C ( score 12 )

VI. Problem Guidance

    At the start, we suggest contestants write a simple Verilog gate-level parser to put designs into proper circuit structures so that a Boolean matching engine can be developed based on such circuit structures and output <match.out>. Contestants are encouraged to brainstorm for new ideas. For a tutorial and an overview of current algorithms, contestants are advised to survey the course slides [1], the book chapter [2] and the papers related to [16].

    For old basic Boolean matching, there are some academic papers developed in various aspects: Spectral [3], Signature [2,10,11], Canonical-form [12,13], BDD [3,8,14], and SAT [2,11,15,16]. Notice that they are just for reference and cannot be directly applied to this new topic. Besides, some circuit cases may be too large to be directly represented by BDDs. We encourage contestants to try some new ideas. Your program should generate as possible before a time out of 1800 seconds.

    Finally, have fun and welcome to submit questions.

VII. Reference