# Verilog Simulation Optimization via Instruction Reduction
## Content
[ToC]
## Intrduction
Hardware description language such as Verilog is used to design a hardware. The design nowaday is growing exponentially to satisfy various applications. Also, we now that the complexity of the circuit is related to the number of the instructions and assignments of the verilog HDL. Therefore, we hope to design a tool to minimize the number of instructions and assignments of the verilog file.
This topic aims at facilitating Verilog simulation while keeping the correct outcome. The simulation efficiency is fundamentally equivalent to how much CPU time is spent on instruction execution. For simplicity, we only focus on the CPU instruction counts, which can be further interpreted as how many and what kinds of Verilog constructs are generated.
In this contest, contestants need to convert a given Verilog design into an optimized Verilog design (so called source-to-source transformation. With a firm principle of simulation correctness, the optimized design is expected to have better simulation performance than the original one. Furthermore, only continuous assignments, wire type signals, bit operations, and bit/part-selects of vectors are considered in the given Verilog design for optimization.The objective is to minimize the total number of continuous assignments and vector bit/part-selects in the Verilog design. We look forward to any innovative optimization strategies suitable for Verilog simulation.
## Problem Statement
The input of the logic synthesis tool will be a verilog file, and we will need to output an optimized verilog file whose functionality will remain unchanged.
### Input
The original design, in the Verilog file named original.v, contains only 2 modules: dut and tb. The module dut is the main module to be optimized and the module tb is merely an auxiliary module for checking the simulation correctness. Thus, contestants should put all their efforts on the module dut. There are only 2 ports, out and in, declared for module dut as follows:
```
module dut (out, in);
output[SIZEOUT:0] out;
input[SIZEIN:0] in;
```
Both of them are packed vector ports, where SIZEOUT and SIZEIN are positive integer constants. Please note that Verilog ports are by default 4-state wires, where a value can be 0, 1, x, or z.
In addition to the ports, there are also a bunch of 1-bit wire signals declared locally in the module dut. These local wires serve as temporary variables, which are common in real designs, as follows:
```
wire origtmp1;
wire origtmp2;
...
wire origtmpN;
```
In the combination circuit of the verilog file, we will have the assignment to assign the functionality of the circuit. In the input file, we will only allow certain forms for the assignment. The following expression of the ports and local wires are all continuous assignments.
```
assign <LHS> = <RHS>;
```
Here are the rules about LHS and RHS. To avoid confusion, Backus-Naur Form (BNF) is adopted here.
```
<LHS> ::=
out[#]
| origtmp#
<RHS> ::=
<ITEM>
| <UNARY_OP> <ITEM>
| <ITEM> <BINARY_OP> <ITEM>
<ITEM> ::=
<1-bit 4-state constant>
| out[#]
| in[#]
| origtmp#
<UNARY_OP> ::=
~ (bit negation)
<BINARY_OP> ::=
& (bit and)
| | (bit or)
| ^ (bit or)
```
### Example
```verilog =
module dut (out, in);
output[3:0] out;
input[15:0] in;
wire origtmp1;
assign origtmp1 = 1'b0;
assign out[2] = in[0] | origtmp1;
assign out[3] = origtmp1 | 1'b0;
endmodule
```
### Output
The information (such as the input length, output length, and the declaration of the wire) of the output function need to be the same as that of the input function.
In output file, LHS allows 2 more types: xformtmp# and out[MSB:LSB]. In Verilog syntax, out[MSB:LSB] denotes part select, which means consecutive bits of port out from index MSB to index LSB (width equals to MSB-LSB+1). Both MSB and LSB are non-negative integers and MSB is greater than LSB.
```
<LHS> ::=
out[#]
| origtmp#
| xformtmp#
| out[MSB:LSB]
<ITEM> ::= <1 or N-bit 4-state constant>
| out[#]
| in[#]
| origtmp#
| out[MSB:LSB]
| in[MSB:LSB]
| xformtmp#
| xformtmp#[MSB:LSB]
<RHS>, <UNARY_OP>, and <BINARY_OP> is the same as the input verilog file.
```
### Example
#### Version 1
```verilog
module dut (out, in);
output[3:0] out;
input[15:0] in;
assign out[2] = in[0] | 1'b0;
assign out[3] = in[1] | 1'b0;
endmodule
```
#### Version 2
```verilog
module dut (out, in);
output[3:0] out;
input[15:0] in;
wire[1:0] xformtmp1;
assign xformtmp1 = 2'b0;
assign out[3:2] = in[1:0] | xformtmp1;
endmodule
```
#### Version 3
```verilog
module dut (out, in);
output[3:0] out;
input[15:0] in;
assign out[3:2] = in[1:0];
endmodule
```
### Evaluation
Simulation of original.v and optimized.v will be conducted by the industrial Verilog simulator Synopsys VCS. The result is PASS if no text diff is observed; otherwise, it is FAIL.
```
RSCORE = 1 (if all regulations followed)
RSCORE = 0 (if any regulation violated)
TSCORE = 1 (if execution time executes 600sec or less)
TSCORE = 0 (if execution time executes longer than 600sec)
ESCORE =
(<OUT_PORT_WIDTH> + <IN_PORT_WIDTH>) / (<COUNT_ASGN> + <COUNT_SELS>)
```
### Example
#### Version 1
``` verilog
assign out[2] = in[0] | 1'b0;
assign out[3] = in[1] | 1'b0;
COUNT_ASGN = 2 (Two assign in the code)
COUNT_SELS = 4 (4 bit/part selects: out[2], in[0], out[3], in[1])
```
#### Version 2
``` verilog
assign xformtmp1 = 2'b0;
assign out[3:2] = in[1:0] | xformtmp1;
COUNT_ASGN = 2 (Two assign in the code)
COUNT_SELS = 2 (2 bit/part selects: out[3:2], in[1:0])
```
#### Version 3
``` verilog
assign out[3:2] = in[1:0];
COUNT_ASGN = 1 (Two assign in the code)
COUNT_SELS = 2 (2 bit/part selects: out[3:2], in[1:0])
```
Here is the summary of the 3 versions and respective FSCORE achieved. Basically, the sum of port widths is identical for all 3 optimization results:
<OUT_PORT_WIDTH> + <IN_PORT_WIDTH> = 4 + 16 = 20.
Version 3 of optimized.v leads to the smallest (<COUNT_ASGN> + <COUNT_SELS>) and highest FSCORE (6.67), which implies the best performance for demanding the least CPU instructions on simulating assignments and selects.
```
Version 1: 20/6 = 3.33
Version 2: 20/4 = 5
Version 3: 20/3 = 6.67
```
## Verilog Parser
We define a node with the following information: operation, left type, left value, right type, right value, and flag. A node is used to record one assignment of the input verilog file. Before using the parser to extract the information, we will read the information of the input file such as the input and output size, and the number of the origtmp size. After we have read the input information, we will construct two arrays output array and origtmp array. The data structure of a cell of the array will be the node we have constructed previously.
```cpp
typedef struct node{
char operation;
string left_type;
string right_type;
int left_value;
int right_value;
}node;
```
We will use the istringstream in c++ to read the file. As the code below:
```cpp
string line;
if(myfile.is_open()){
while(getline(myfile, line)){
istringstream is(line);
string s;
while(is >> s){
if(s.substr(0,6) == "assign"){
//read the current type of the assignment
//store the left and right information to the arrays
//First see the type of the current node(out or origtmp)
//Then read the following information such as
//out[0] = in[0] | in[1];
//store the correct information to the array structure
//omission
}
}
}
}
```
The right_type and left_type of the node structure will be three conditions (origtmp, in, constant). The right_value and left_value will denote the index if the type is origtmp or in; those will be the constant value (1'b1, 1'b0, 1'bz, 1'bx) if the type is const(constant).
### Further Discussion on Parser
## Data Structure
Once we finish the parser of the input file and get all information of the input assignments, we will now consider constructing the type of data structure. Since we will have the perfect structure that will only contain two inputs in one assignment. Therefore, for each output node (out[#]), we can view it as the root of the binary tree.
Before we construct the binary tree, we have to define the tree node of the binary tree. The node structure can be defined as followed:
```cpp
typedef struct Treenode{
char operation;
string left_type;
string right_type;
int left_value;
int right_value;
int printed; //used for printing file
string name; //record the name of the node e.g out[0]
Treenode* left;
Treenode* right;
}Treenode;
```
Therefore, we will construct a binary for each output node with the help of the previous constructed arrays (output and origtmp). We will now introduce the function called "factoringTree" as the **partial** **code** below:
```cpp
void factorTree(Treenode &first, Treenode* dout, Treenode* dorigtmp){
if(first.left_type == "" && first.right_type != ""){
if(first.right_type == "out"){
first.right = &dout[first.right_value];
factorTree(dout[first.right_value], dout, dorigtmp);
}
else if(first.right_type == "origtmp"){
first.right = &dorigtmp[first.right_value];
factorTree(dorigtmp[first.right_value], dout, dorigtmp);
}
}
else if(first.left_type != "" && first.right_type == ""){
if(first.left_type == "out"){
first.left = &dout[first.left_value];
factorTree(dout[first.left_value], dout, dorigtmp);
}
else if(first.left_type == "origtmp"){
first.left = &dorigtmp[first.left_value];
factorTree(dorigtmp[first.left_value], dout, dorigtmp);
}
}
else if(first.left_type != "" && first.right_type != ""){
//Find other possible combination and follow the previous
//solution to factorize the tree.
//omission
}
}
```
In this partial code, we will be based on the left type/value and right type/value to point the current node's pointer to the right array cell. Therefore, we will get the final binary tree.
For checking the functionality of the circuit, we can use the tree preorder traversal to see the final factor form. The final factor form will help us to see whether the parser is correct or not. As the partial code below:
```cpp
void Traversal(Treenode &first, Treenode* doutput, Treenode* dorigtmp){
if(first.left == NULL && first.right == NULL){
//print the information of the node
//omission
}
else if(first.left != NULL && first.right == NULL){
//Since the right pointer is NULL
//We can first traverse the left subtree.
//omission
}
else if(first.left == NULL && first.right != NULL){
//Similar to the previous condition
//omission
}
else if(first.left != NULL && first.right != NULL){
cout << "(";
Traversal(*first.left, doutput, dorigtmp);
cout << first.operation;
Traversal(*first.right, doutput, dorigtmp);
cout << ")";
}
}
```
If the size of output is M and the size of origtmp is N, the complexity of factoring tree will be O(M+N) due to the fact that we will read the arrays to factor the tree. Also, since we will go through the entire tree to traverse the node, the complexity of traversal will also be O(M+N).
## Minimization
### First Step Minimization
In boolean algebra, we all know there are several boolean identities that are used to minimize the boolean function. First of all, we will list some common constant operations of the boolean function as the following table.
Therefore, we will go through all the cells of the array to see whether there is possible bits operation in the first step minimization. Also, note that high z signals and don't care signals will have the same behavior in the table. Therefore, we will view those two signals in the same variable (constant 2).
When a cell of the array consist a constant and a variable, the boolean identities also tell us that we can use those identities to minimize the function as follow:
```
1. A|0 = A
2. A|1 = 1
3. A|2 = either 1 or 2 ( = 1 when A is 1). Therefore, for simplicity, A|2 = 1
4. A&0 = 0
5. A&1 = A
6. A&2 = 0 ( same reason as 3.)
7. A^0 = A
8. A^1 = ~A
9. A^2 = 2 ( by previous chart )
```
As the following partial code:
```cpp
void seeConstant(Treenode& first){
if(first.left_type == "const" && first.right_type == "const"){
if(first.operation == '|'){
//omission
//list all possible combination of two constants operation
}
else if(first.operation == '&'){
//list all possible combination of two constants operation
//omission
}
else if(first.operation == '^'){
//list all possible combination of two constants operation
//omission
}
}
else if(first.left_type != "const" && first.right_type == "const"){
//implement all minimization equation that previous mentioned
//omission
}
else if(first.left_type == "const" && first.right_type != "const"){
//implement all minimization equation that previous mentioned
//omission
}
}
```
Therefore, we will go through each cell of the arrays to check if those cells are conformed to the conditions mentioned above. If the size of the output array is M and the size of the origtmp array is N, the overall complexity will be O(M+N).
### Second Step Minimization
After minimizing the inner data structure, we hope to combine or substitute some variables with the corresponding equations. For example, if we have two equations:
```
1. out[0] = origtmp1;
origtmp1 = in[0] & in[1];
2. out[0] = origtmp1 | origtmp2;
origtmp1 = in[0];
origtmp2 = in[2];
```
It is obviously that we can substitute origtmp1 with in[0] | in[1] into out[1] for the first case. When we represent the equations as our data structure, we can see the relationship between two equations. Also, we will hope that we will start our minimization from the leaves; hence, we will first use the postorder traversal to start the minimization from roots. As the partial code below:
```cpp
void secondMinimization(Treenode &first, Treenode* doutput, Treenode* dorigtmp){
if(first.left == NULL && first.right == NULL)
return;
else if(first.left != NULL && first.right == NULL && first.left_type != "" && first.right_type == ""){
secondMinimization(*first.left, doutput, dorigtmp);
if(first.operation == '~' ){
if(first.left -> right_type == "" ){
if(first.left -> operation != '~'){
first.left_type = first.left -> left_type;
first.left_value = first.left->left_value;
first.left = first.left -> left;
}
else if(first.left -> operation == '~'){
first.operation = ' ';
first.left_type = first.left -> left_type;
first.left_value = first.left->left_value;
first.left = first.left -> left;
}
}
}
else if(first.operation != '~'){
if(first.left -> right_type == "" ){
if(first.left -> operation != '~'){
first.left_type = first.left -> left_type;
first.left_value = first.left->left_value;
first.left = first.left -> left;
}
else if(first.left -> operation == '~'){
first.operation = first.left -> operation;
first.left_type = first.left -> left_type;
first.left_value = first.left->left_value;
first.left = first.left -> left;
}
}
else if(first.left -> right_type != ""){
first.left_type = first.left -> left_type;
first.left_value = first.left -> left_value;
first.right_type = first.left -> right_type;
first.right_value = first.left -> right_value;
first.operation = first.left -> operation;
first.right = first.left -> right;
first.left = first.left -> left;
}
}
seeConstant(first);
}
//Find all possible pattern of the second step minimization
//omission
}
```
In second step minimization, the worst case will be going through all nodes of the binary tree. Therefore, if the size of output is M and the size of origtmp is N, then the overall complexity of second step minimization will be O(M+N).
### Third Step Minimization (Pattern Comparison)
In third step minimization, we offer several boolean equations that can be minimized as the equations below. If we use tree traversal to find the subtree patterns of the equations, then we can rewrite the structure of the subtree to optimize the circuit.
```
1. a|(ab) = a
2. a&(a|b) = a
3. a|(~a&b) = a|b
4. a&(~a|b) = a&b
5. ~a&b | a&~b = a^b
```
For example, the previous equations will have the structure as the following graph:
```verilog
Before Minimization:
assign out[1] = origtmp2 | origtmp1;
assign origtmp1 = origtmp2 & origtmp3;
After Minimization:
assign origtmp1 = origtmp2;
```
```verilog
Before Minimization:
assign out[1] = origtmp4 | origtmp1;
assign origtmp1 = origtmp2 & origtmp3;
assign origtmp2 = ~origtmp4;
After Minimization:
assign out[1] = origtmp4 | origtmp3;
```
```verilog
Before Minimization:
assign out[1] = origtmp1 | origtmp2;
assign origtmp1= origtmp3 & in[2];
assign origtmp2 =in[1] & origtmp4;
assign origtmp3 = ~in[1];
assign origtmp4 = ~in[2];
After Minimization:
assign out[1] = in[1] ^ in[2];
```
Also, we will hope that we will start our minimization from the leaves; hence, we will first use the postorder traversal to start the minimization from roots. By the previous mentioned conditions, we can write the partial code as follow:
```cpp
void thirdMinimization(Treenode &first, Treenode* doutput, Treenode* dorigtmp){
if(first.left == NULL && first.right == NULL)
return;
else if(first.left != NULL && first.right != NULL){
thirdMinimization(*first.left, doutput, dorigtmp);
thirdMinimization(*first.right, doutput, dorigtmp);
if(first.left == first.right -> left && ((first.operation == '|'&& first.right->operation == '&') || (first.operation == '&'&& first.right->operation == '|'))){
first.right_type = "";
first.right_value = 0;
first.operation = ' ';
first.right = NULL;
}
else if(first.left == first.right -> right && ((first.operation == '|'&& first.right->operation == '&') || (first.operation == '&'&& first.right->operation == '|'))){
first.right_type = "";
first.right_value = 0;
first.operation = ' ';
first.right = NULL;
}
else if(first.right == first.left -> left && ((first.operation == '|'&& first.left->operation == '&') || (first.operation == '&'&& first.left->operation == '|'))){
first.left_type = "";
first.left_value = 0;
first.operation = ' ';
first.left = NULL;
}
else if(first.right == first.left -> right && ((first.operation == '|'&& first.left->operation == '&') || (first.operation == '&'&& first.left->operation == '|'))){
first.left_type = "";
first.left_value = 0;
first.operation = ' ';
first.left = NULL;
}
}
//other patterns are omitted.
}
```
In third step minimization, the worst case will be going through the all nodes of the binary tree. Therefore, if the size of output is M and the size of origtmp is N, then the overall complexity of second step minimization will be O(M+N).
## Further Pattern Comparison
### Communative Law
In the boolean equation, several gates have the commutative identity. Therefore, it is likely to get an optimized function with the help of commutative law. For example,
```verilog
Before Commutative Law:
assign out[0] = origtmp1 & origtmp2;
assign origmtp1 = in[0] & in[2];
assign origtmp2 = in[1] & in[2];
After Commutative Law:
assign out[0] = origtmp1 & origtmp2;
assign origmtp1 = in[0] & in[1];
assign origtmp2 = in[2] & in[2];
Applying the previous second step minimization:
assign out[0] = origtmp1 & in[2];
assign origtmp1 = in[0] & in[1]
```
With the help of pattern comparison, we can get the optimized circuit in the simple tree traversal. However, if we use the method to revise the circuit, we will change the functionality of the circuit (We have changed the functionality of origtmp1 and origtmp2). Therefore, we will need to construct an additional wire to help us implement the commutative law. The equation should be revised as:
```verilog
Before Commutative Law:
assign out[0] = origtmp1 & origtmp2;
assign origmtp1 = in[0] & in[2];
assign origtmp2 = in[1] & in[2];
After Commutative Law:
assign out[0] = xformtmp1 & xformtmp2;
assign xformtmp1 = in[0] & in[1];
assign xformtmp2 = in[2] & in[2];
Applying the previous second step minimization:
assign out[0] = xformtmp1 & in[2];
assign xformtmp1 = in[0] & in[1]
```
Also, we will hope that we will start our minimization from the leaves; hence, we will first use the postorder traversal to start the minimization from roots.
Note that we can only use origtmp, xformtmp wire in the output file. Therefore, the additional wires should only be named as xformtmp. The dynamic method to allocate the xformtmp can be referred to the following graph and code:
```cpp
void commutative(Treenode &first, Treenode *doutput, Treenode *dorigtmp){
if(first.left == NULL && first.right == NULL) return;
else if(first.left != NULL && first.right != NULL){
commutative(*first.left, doutput, dorigtmp);
commutative(*first.right, doutput, dorigtmp);
if(first.operation == first.left -> operation && first.operation == first.right -> operation && first.operation != '~'){
if(first.left -> left_type == first.right -> left_type && first.left -> left_value == first.right -> left_value){
stringstream ss;
ss << xformtmp_cnt;
Treenode tmp_l, tmp_r;
tmp_l.operation = first.left -> operation;
tmp_l.left_type = first.left -> left_type;
tmp_l.left_value = first.left -> left_value;
tmp_l.left = first.left -> left;
tmp_l.right_type = first.right -> left_type;
tmp_l.right_value = first.right -> left_value;
tmp_l.right = first.right -> left;
tmp_l.name = "xformtmp" + ss.str();
ss.str("");
first.left_type = "xformtmp";
first.left_value = xformtmp_cnt;
xformtmp[xformtmp_cnt] = tmp_l;
//xformtmp.push_back(tmp_l);
xformtmp_cnt++;
ss << xformtmp_cnt;
tmp_r.operation = first.right->operation;
tmp_r.left_type = first.left -> right_type;
tmp_r.left_value = first.left -> right_value;
tmp_r.left = first.left -> right;
tmp_r.right_type = first.right -> right_type;
tmp_r.right_value = first.right -> right_value;
tmp_r.right = first.right -> right;
tmp_r.name = "xformtmp" + ss.str();
ss.str("");
first.right_type = "xformtmp";
first.right_value = xformtmp_cnt;
xformtmp[xformtmp_cnt] = tmp_r;
first.left = &xformtmp[xformtmp_cnt-1];
first.right = &xformtmp[xformtmp_cnt];
//xformtmp.push_back(tmp_r);
xformtmp_cnt++;
seeConstant(*first.left);
seeConstant(*first.right);
secondMinimization(first, doutput, dorigtmp);
seeConstant(first);
}
//other conditions are omitted
}
}
}
```
In commutative law, the worst case will be going through all nodes of the binary tree. Therefore, if the size of output is M and the size of origtmp is N, then the overall complexity of second step minimization will be O(M+N).
### Final Minimization
In final minimization, we offer several boolean equations that can be minimized as the equations below. If we use tree traversal to find the subtree patterns of the equations, then we can rewrite the structure of the subtree to optimize the circuit.
```
1. a^(a&b) = a&~b;
2. a^(a|b) = ~a&b;
3. a&(a^b) = a&~b;
4. a|(a^b) = a|b;
5. a^~(a&b) = ~a|b;
6. a^~(a|b) = a|~b;
7. a&(a^b) = ~a&b;
8. a|(a^b) = ~a|~b;
```
We will use pattern comparison the same as the third step minimization, and we will use the xformtmp to avoid the revision of the functionality. We will hope that we will start our minimization from the leaves; hence, we will first use the postorder traversal to start the minimization from roots. The code is as follow:
```cpp
void finalMinimization(Treenode &first, Treenode* doutput, Treenode* dorigtmp){
if(first.left == NULL && first.right == NULL) return;
else if(first.left == NULL && first.right != NULL){
finalMinimization(*first.right, doutput, dorigtmp);//a^(a&b)
if(first.left_type == first.right -> left_type && first.left_value == first.right -> left_value && first.operation == '^' && first.right -> operation == '&'){
Treenode tmp;
tmp.operation = '~';
tmp.left_type = first.right -> right_type;
tmp.left_value = first.right -> right_value;
tmp.left = first.right -> right;
tmp.right_type = "";
tmp.right_value = 0;
tmp.right = NULL;
stringstream ss;
ss << xformtmp_cnt;
tmp.name = "xformtmp" + ss.str(); //+ to_string(xformtmp_cnt);
first.right_type = "xformtmp";
first.right_value = xformtmp_cnt;
first.operation = '&';
xformtmp[xformtmp_cnt] = tmp;
first.right = &xformtmp[xformtmp_cnt];
ss.str("");
ss.clear();
xformtmp_cnt++;
}
//other patterns are omitted.
}
else if(first.left != NULL && first.right == NULL){
finalMinimization(*first.left, doutput, dorigtmp);
}
else{
finalMinimization(*first.left, doutput, dorigtmp);
finalMinimization(*first.right, doutput, dorigtmp);
}
}
```
### Other Pattern
In other pattern comparison, we offer several boolean equations that can be minimized as the equations below. If we use tree traversal to find the subtree patterns of the equations, then we can rewrite the structure of the subtree to optimize the circuit.
```verilog
Before Minimization:
assign origtmp1 = origtmp2 | origtmp3;
assign origtmp2 = ~xformtmp1;
assign origtmp3 = ~xformtmp1;
After Minimization:
assign origtmp1 = ~xformtmp1;
Before Minimization:
assign out[1] = origtmp1 ^ in[1];
assign origtmp1 = ~in[1];
After Minimization:
assign out[1] = 1'b0;
```
The code is omitted due to the similarity to the previous type of pattern comparison.
## Further Optimization
Nowaday, we have various logic minimization algorithms such as Quine-McCluskey, ESSPRESSO, AIG, etc. However, those algorithms are not a polynomial problem. Although the pattern comparison will be much more efficient, pattern comparison is less general than the algorithm previously mentioned.
We will now move to implement two general algorithms which are Quine-McCluskey and SAT-based redundant wire checking. Before we move onto the algorithm, notice that we will need the SOP (Sum of Product) form to implement the Quine-McCluskey algorithm.
In order to get the SOP form, we will need to assign all possible combinations of the inputs to the circuit to get the result.
### Generating Truth Table
First, we will need to design the input value into the circuit. Go through the array of output and origtmp, and we can discover the array cells whose left or right type are input as the code below:
```cpp
for(int i = 0 ; i <= num_out; i++){
if(toutput[i].left_type == "in"){
toutput[i].left_type = "const";
toutput[i].left_value = infor[toutput[i].left_value]-'0';
}
if(toutput[i].right_type == "in"){
toutput[i].right_type = "const";
toutput[i].right_value = infor[toutput[i].right_value]-'0';
}
}
```
The infor array stores the value that we assign to the input. After assigning the constant value to input, we will use the previous technique (First and second minimization) to minimize the circuit. With the help of first and second minimization, we will get the output with a constant bit. With the help of the output result, we can use those as the input into the Quine-McCluskey algorithm.
### Verifying Circuit
Generating truth table can also help us to verify the circuit. Our goal is to compare the results of the original verilog file and optimized verilog file. Therefore, we will assign two identical input patterns into the original and optimized verilog file, respectively. Finally, we will get two output sequences, and we can next compare the output sequences of two verilog files.
Although this method cannot guarantee the original and optimized verilog files are exactly the same if we only offer the limited input sequences, the verification is still possible to discover the wrong functionality of the output. The equivalence checking will be thorough only if we use the SAT solver which we will discuss in the next session.
### SAT-Based Redundant Wire Checking
In EDA, we will use testing (stuck-at-fault) to check the possible faults in the chips. However, stuck-at-fault can also help us to find out the redundant wire of the circuit. For a combination circuit, an undetectable fault is corresponding to a redundant wire. Undetectable faults do not change the functionality of the circuit. The reason can be referred to here.
The previous graph shows when the s-a-1 fault is assigned to an AND gate. No matter which value m and n is, wirel can always be viewed as the redundant wire. On the other hand, we will get three redundant wires when wire l is assigned to constant 0.
How can we say the wire is redundant? As previously mentioned, we will get the same functionality of the original circuit and the stuck-at-fault circuit. Therefore, we will need to generate the whole possible inputs in order to compare the functionality of the original circuit and the stuck-at-fault circuit.
Note that we will use XOR gate to check two circuits to check whether the circuits are equivalent or not as the following equations.
In the final equation of the example, we tend to find the possible combination of a, b and c for equation abc' = 1. Note that this is a SAT problem; therefore, we will use an SAT solver to check the circuit. We can find lots of open source modern SAT solvers. With the help of modern SAT solvers, we can efficiently check if the wire is redundant or not. In this project, we will use [Glucose SAT](https://www.labri.fr/perso/lsimon/glucose/).
In order to implement the SAT-based redundant wire checking, we will need to first duplicate the original circuit for the purpose of a stuck-at-fault circuit.
```cpp
Treenode duplicateTree(Treenode &root, Treenode* doutput, Treenode * dorigtmp, int a, int b){
Treenode result;
result.right = NULL;
result.left = NULL;
Treenode loutput[a+10];//duplicate tree for original circuit
Treenode lorigtmp[b+10];
Treenode routput[a+10];//duplicate tree for stuck-at-fault circuit
Treenode rorigtmp[b+10];
Treenode* ltmp = NULL;
Treenode* rtmp = NULL;
}
```
After we duplicate the tree, we will need an additional XOR gate to connect two circuits into a miter circuit. Then , we can next assign either s-a-1 or s-a-0 fault into an assigned wire. When finishing assigning the wire, we will use tseitin transformation to transform the miter circuit into a form that can be used by SAT solver.
[Tseitin transformation](https://en.wikipedia.org/wiki/Tseytin_transformation) takes as input an arbitrary combinational logic circuit and produces a boolean formula in conjunctive normal form (CNF), which can be solved by a CNF-SAT solver. The length of the formula is linear in the size of the circuit. Input vectors that make the circuit output "true" are in 1-to-1 correspondence with assignments that satisfy the formula. This reduces the problem of circuit satisfiability on any circuit (including any formula) to the satisfiability problem on 3-CNF formulas.
The one-to-one relation of logic gate and tseitin transformation is shown in the following graph.
Before we construct the tseitin form of the miter circuit, we will need to assign an id to each input and wire. In the following partial, we will first use tree traversal to see which inputs or wires are used in the circuit.
```cpp
void buildgate(Treenode &first, int count, map<string, int>& nameid, vector<gate> Gate){
if(first.left == NULL && first.right == NULL){
//go through left and right type value
nameid.insert(pair<string, int>(first.name, count));
if(nameid.find(first.left_type + to_string(first.left_value)) == nameid.end() && first.left_type != ""){
nameid.insert(pair<string, int>(first.left_type + to_string(first.left_value), count));
}
if(nameid.find(first.right_type + to_string(first.right_value)) == nameid.end() && first.right_type != ""){
nameid.insert(pair<string, int>(first.right_type + to_string(first.right_value), count));
}
return;
}
else if(first.left != NULL && first.right == NULL){
buildgate(*first.left, count, nameid, Gate);
//omission
}
else if(first.left == NULL && first.right != NULL){
buildgate(*first.right, count, nameid, Gate);
//omission
}
else{
buildgate(*first.left, count, nameid, Gate);
buildgate(*first.right, count, nameid, Gate);
nameid.insert(pair<string, int>(first.name, count));
}
}
```
After we store the emerging inputs and wire them into a map structure (nameid), we can now assign the id into those names stored in the "nameid".
```cpp
for(it = nameid.begin(); it != nameid.end(); it++){
it -> second += map_cnt;
map_cnt++;
}
```
With the help of tree traversal, we construct the c struct that stores the information of the gate (type of gate and the id of inputs and output) as the code below.
```cpp
void buildGate(Treenode* first, map<string, int> nameid, vector<gate>& Gate){
if(first == NULL) return;
else{
gate p;
p.type = first -> operation;
p.output = nameid[first->name];
if(first->left == NULL && first->left_type != "")
p.input.push_back(nameid[first->left_type+to_string(first->left_value)]);
else if(first->left_type != "")
p.input.push_back(nameid[first->left->name]);
if(first->right == NULL && first ->right_type != "")
p.input.push_back(nameid[first->right_type+to_string(first->right_value)]);
else if(first->right_type != "")
p.input.push_back(nameid[first->right->name]);
Gate.push_back(p);
buildGate(first->left, nameid, Gate);
buildGate(first->right, nameid, Gate);
}
}
```
We now can use the tseitin transformation to build the clause for the input of the SAT solver. We have mentioned the one-to-one relation between original gates and the tseitin form. Therefore, we can apply the Glucose SAT solver as follows. (addClause(), mkLit() are the functions of SAT solver)
```cpp
Solver so;
for( int i=1 ; i<=nameid.size() ; i++ )
auto var = so.newVar();
int cnt_c = 0;
for(int i = 0; i < Gate.size(); i++)
{
gate cur = Gate[i];
if(cur.type == '&'){
so.addClause(~mkLit(cur.input[0]), ~mkLit(cur.input[1]), mkLit(cur.output));
so.addClause(mkLit(cur.input[0]), ~mkLit(cur.output));
so.addClause(mkLit(cur.input[1]), ~mkLit(cur.output));
cnt_c+=3;
}
else if(cur.type == '|'){
so.addClause(mkLit(cur.input[0]), mkLit(cur.input[1]), ~mkLit(cur.output));
so.addClause(~mkLit(cur.input[0]), mkLit(cur.output));
so.addClause(~mkLit(cur.input[1]), mkLit(cur.output));
cnt_c+=3;
}
else if(cur.type == '~'){
so.addClause(~mkLit(cur.input[0]), ~mkLit(cur.output));
so.addClause(mkLit(cur.input[0]), mkLit(cur.output));
cnt_c+=2;
}
else if(cur.type == '^'){
so.addClause(~mkLit(cur.input[0]), ~mkLit(cur.input[1]), ~mkLit(cur.output));
so.addClause(mkLit(cur.input[0]), mkLit(cur.input[1]), ~mkLit(cur.output));
so.addClause(mkLit(cur.input[0]), ~mkLit(cur.input[1]), mkLit(cur.output));
so.addClause(~mkLit(cur.input[0]), mkLit(cur.input[1]), mkLit(cur.output));
cnt_c+=4;
}
else if(cur.type == ' '){
so.addClause(~mkLit(cur.input[0]), mkLit(cur.output));
so.addClause(mkLit(cur.input[0]), ~mkLit(cur.output));
cnt_c+=2;
}
}
so.addClause(mkLit(nameid[result.name]));
bool ans = so.solve();
//cout << ans << endl;
if(ans == 1){
//not a redundant wire
}else{
//a redundant wire
}
```
Sign in with Wallet
Connect another wallet