Merge pull request #54 from SergeyDegtyar/master

Add new tests to backends,equiv,frontends,misc,simple.

backends/scripts/write_btor_shift.ys

+read_verilog -sv ../top.v
+proc
+pmux2shiftx
+hierarchy -top top
+flatten
+write_btor btor.btor
+write_verilog synth.v

backends/scripts/write_firrtl_fsm.ys

+read_verilog ../top.v
+proc
+pmux2shiftx
+clean
+write_firrtl firrtl.firrtl
+write_verilog synth.v

backends/scripts/write_smt2_anyseq.ys

+read_verilog ../top.v
+proc
+setundef -anyseq
+memory
+write_smt2 -mem smt2.smt2
+write_verilog synth.v

backends/scripts/write_smt2_init_assert.ys

 read_verilog -sv ../top.v
 proc
-write_smt2 smt2.smt2
+write_smt2 -stbv smt2.smt2
 synth -top top
-write_smt2 smt2.smt2
+write_smt2 -stbv smt2.smt2
 design -reset
 read_verilog  -sv ../top_clean.v
 synth -top top

backends/scripts/write_verilog_lut.ys

+read_verilog ../top.v
+proc
+synth
+abc -lut 5
+write_verilog synth.v

backends/scripts/write_verilog_shift.ys

+read_verilog ../top.v
+proc
+pmux2shiftx
+write_verilog synth.v

backends/scripts/write_verilog_slice.ys

+read_verilog ../top.v
+proc
+splice
+write_verilog synth.v

backends/scripts/write_xaiger.ys

+read_verilog -sv ../top.v
+aigmap
+write_xaiger xaiger.xaiger
+design -reset
+read_verilog -sv ../top_clean.v
+aigmap
+write_xaiger xaiger.xaiger
+synth -top top
+write_verilog synth.v

backends/scripts/write_xaiger_ascii.ys

+read_verilog -sv ../top.v
+aigmap
+write_xaiger -ascii xaiger.xaiger
+design -reset
+read_verilog -sv ../top_clean.v
+aigmap
+write_xaiger xaiger.xaiger
+synth -top top
+write_verilog synth.v

backends/scripts/write_xaiger_cant_find_top_module.ys

+read_verilog -sv ../top.v
+aigmap
+write_xaiger xaiger.xaiger
+design -reset
+read_verilog -sv ../top_clean.v
+aigmap
+write_xaiger xaiger.xaiger
+synth -top top
+write_verilog synth.v

backends/scripts/write_xaiger_cant_open_file.ys

+read_verilog -sv ../top2.v
+aigmap
+write_xaiger -map tt/tt.map xaiger.xaiger
+design -reset
+read_verilog -sv ../top_clean.v
+aigmap
+write_xaiger xaiger.xaiger
+synth -top top
+write_verilog synth.v

backends/scripts/write_xaiger_map.ys

+read_verilog -sv ../top.v
+proc
+aigmap
+write_xaiger -map a.map xaiger.xaiger
+design -reset
+read_verilog -sv ../top_clean.v
+synth
+aigmap
+write_xaiger xaiger.xaiger
+synth -top top
+write_verilog synth.v

backends/scripts/write_xaiger_vmap.ys

+read_verilog -sv ../top.v
+aigmap
+write_xaiger -vmap a.map xaiger.xaiger
+design -reset
+read_verilog -sv ../top_clean.v
+aigmap
+write_xaiger xaiger.xaiger
+synth -top top
+write_verilog synth.v

backends/write_btor_init_assert/testbench.v

+module testbench;
+    reg [2:0] in;
+
+	reg patt_out = 0;
+	reg patt_carry_out = 0;
+	wire out;
+    wire carryout;
+
+    initial begin
+        // $dumpfile("testbench.vcd");
+        // $dumpvars(0, testbench);
+
+        #5 in = 0;
+        repeat (10000) begin
+            #5 in = in + 1;
+        end
+
+        $display("OKAY");
+    end
+
+    top uut (
+	.x(in[0]),
+	.y(in[1]),
+	.cin(in[2]),
+	.A(out),
+	.cout(carryout)
+	);
+	
+	always @(posedge in[0]) 
+        patt_out <=  in[1] + in[2];
+    always @(negedge in[0])
+        patt_carry_out <=  in[1] + patt_out;
+
+	assert_comb out_test(.A(patt_out), .B(out));
+	assert_comb carry_test(.A(patt_carry_out), .B(carryout));
+
+endmodule

backends/write_btor_init_assert/top.v

+module top
+(
+ input x,
+ input y,
+ input cin,
+
+ output reg A,
+ output reg cout
+ );
+ 
+ reg ASSERT = 1;
+ (* anyconst *) reg foo;
+ (* anyseq *) reg too;
+ 
+
+ 
+ initial begin
+    begin
+        A = 0;
+        cout = 0;
+    end
+ end
+
+`ifndef BUG
+always @(posedge x) begin
+    if ($initstate) 
+        A <= 0;
+    A <=  y + cin + too;
+    assume(too);    
+    assume(s_eventually too);
+end
+always @(negedge x) begin
+    if ($initstate) 
+        cout <= 0;
+        cout <=  y + A + foo;
+    assert(ASSERT);
+    assert(s_eventually ASSERT);
+end
+`else
+assign {cout,A} =  cin - y * x;
+`endif
+
+endmodule

backends/write_btor_init_assert/top_clean.v

+module top
+(
+ input x,
+ input y,
+ input cin,
+
+ output reg A,
+ output reg cout
+ );
+ 
+ initial begin
+    A = 0;
+    cout = 0;
+ end
+
+`ifndef BUG
+always @(posedge x) begin
+    A <=  y + cin;
+end
+always @(negedge x) begin
+    cout <=  y + A;
+end
+`else
+assign {cout,A} =  cin - y * x;
+`endif
+
+endmodule

backends/write_btor_shift_shiftx/testbench.v

+module testbench;
+    reg clk;
+
+    initial begin
+        // $dumpfile("testbench.vcd");
+        // $dumpvars(0, testbench);
+
+        #5 clk = 0;
+        repeat (10000) begin
+            #5 clk = 1;
+            #5 clk = 0;
+        end
+
+        $display("OKAY");    
+    end
+   
+    function [31:0] xorshift32;
+        input [31:0] arg;
+        begin
+                xorshift32 = arg;
+                // Xorshift32 RNG, doi:10.18637/jss.v008.i14
+                xorshift32 = xorshift32 ^ (xorshift32 << 13);
+                xorshift32 = xorshift32 ^ (xorshift32 >> 17);
+                xorshift32 = xorshift32 ^ (xorshift32 <<  5);
+        end
+    endfunction
+
+    reg [31:0] rng = 123456789;
+    always @(posedge clk) rng <= xorshift32(rng);
+
+    wire a = xorshift32(rng * 5);
+    wire b = xorshift32(rng * 7);
+    reg rst;
+    wire g0;
+    wire g1;
+    
+    top uut (
+        .a (a),
+        .b (b),
+        .clk (clk),
+        .rst (rst),
+        .g0(g0),
+        .g1(g1)
+    );
+    
+    initial begin
+        rst <= 1;
+        #5
+        rst <= 0;
+    end
+	
+    assert_Z g0_test(.clk(clk), .A(g0));
+	assert_Z g1_test(.clk(clk), .A(g1));
+  
+endmodule

backends/write_btor_shift_shiftx/top.v

+ module fsm (
+ clock,
+ reset,
+ req_0,
+ req_1,
+ gnt_0,
+ gnt_1      
+ );
+ input   clock,reset,req_0,req_1;
+ output  gnt_0,gnt_1;
+ wire    clock,reset,req_0,req_1;
+ reg     gnt_0,gnt_1;
+ 
+ parameter SIZE = 3           ;
+ parameter IDLE  = 3'b001,GNT0 = 3'b010,GNT1 = 3'b100,GNT2 = 3'b101 ;
+ 
+ reg [SIZE-1:0] state;
+ reg [SIZE-1:0] next_state;
+ 
+ always @ (posedge clock)
+ begin : FSM
+ if (reset == 1'b1) begin
+   state <=  #1  IDLE;
+   gnt_0 <= 0;
+   gnt_1 <= 0;
+ end else
+  case(state)
+    IDLE : if (req_0 == 1'b1) begin
+                 state <=  #1  GNT0;
+`ifndef BUG        
+                 gnt_0 <= 1;
+`else
+                 gnt_0 <= 1'bZ;
+`endif
+               end else if (req_1 == 1'b1) begin
+                 gnt_1 <= 1;
+                 state <=  #1  GNT0;
+               end else begin
+                 state <=  #1  IDLE;
+               end
+    GNT0 : if (req_0 == 1'b1) begin
+                 state <=  #1  GNT0;
+               end else begin
+                 gnt_0 <= 0;
+                 state <=  #1  IDLE;
+               end
+    GNT1 : if (req_1 == 1'b1) begin
+                 state <=  #1  GNT2;
+				 gnt_1 <= req_0;
+               end
+    GNT2 : if (req_0 == 1'b1) begin
+                 state <=  #1  GNT1;
+				 gnt_1 <= req_1;
+               end 
+    default : state <=  #1  IDLE;
+ endcase
+ end
+ 
+ endmodule
+ 
+ module top (
+input clk,
+input rst,
+input a,
+input b,
+output g0,
+output g1
+);
+
+fsm u_fsm ( .clock(clk),
+            .reset(rst), 
+            .req_0(a), 
+            .req_1(b), 
+            .gnt_0(g0), 
+            .gnt_1(g1));
+
+endmodule

backends/write_firrtl_fsm/testbench.v

+module testbench;
+    reg clk;
+
+    initial begin
+        // $dumpfile("testbench.vcd");
+        // $dumpvars(0, testbench);
+
+        #5 clk = 0;
+        repeat (10000) begin
+            #5 clk = 1;
+            #5 clk = 0;
+        end
+
+        $display("OKAY");    
+    end
+   
+    function [31:0] xorshift32;
+        input [31:0] arg;
+        begin
+                xorshift32 = arg;
+                // Xorshift32 RNG, doi:10.18637/jss.v008.i14
+                xorshift32 = xorshift32 ^ (xorshift32 << 13);
+                xorshift32 = xorshift32 ^ (xorshift32 >> 17);
+                xorshift32 = xorshift32 ^ (xorshift32 <<  5);
+        end
+    endfunction
+
+    reg [31:0] rng = 123456789;
+    always @(posedge clk) rng <= xorshift32(rng);
+
+    wire a = xorshift32(rng * 5);
+    wire b = xorshift32(rng * 7);
+    reg rst;
+    wire g0;
+    wire g1;
+    
+    top uut (
+        .a (a),
+        .b (b),
+        .clk (clk),
+        .rst (rst),
+        .g0(g0),
+        .g1(g1)
+    );
+    
+    initial begin
+        rst <= 1;
+        #5
+        rst <= 0;
+    end
+	
+    assert_Z g0_test(.clk(clk), .A(g0));
+	assert_Z g1_test(.clk(clk), .A(g1));
+  
+endmodule

backends/write_firrtl_fsm/top.v

+ module fsm (
+ clock,
+ reset,
+ req_0,
+ req_1,
+ gnt_0,
+ gnt_1      
+ );
+ input   clock,reset,req_0,req_1;
+ output  gnt_0,gnt_1;
+ wire    clock,reset,req_0,req_1;
+ reg     gnt_0,gnt_1;
+ 
+ parameter SIZE = 3           ;
+ parameter IDLE  = 3'b001,GNT0 = 3'b010,GNT1 = 3'b100,GNT2 = 3'b101 ;
+ 
+ reg [SIZE-1:0] state;
+ reg [SIZE-1:0] next_state;
+ 
+ always @ (posedge clock)
+ begin : FSM
+ if (reset == 1'b1) begin
+   state <=  #1  IDLE;
+   gnt_0 <= 0;
+   gnt_1 <= 0;
+ end else
+  case(state)
+    IDLE : if (req_0 == 1'b1) begin
+                 state <=  #1  GNT0;
+`ifndef BUG        
+                 gnt_0 <= 1;
+`else
+                 gnt_0 <= 1'bZ;
+`endif
+               end else if (req_1 == 1'b1) begin
+                 gnt_1 <= 1;
+                 state <=  #1  GNT0;
+               end else begin
+                 state <=  #1  IDLE;
+               end
+    GNT0 : if (req_0 == 1'b1) begin
+                 state <=  #1  GNT0;
+               end else begin
+                 gnt_0 <= 0;
+                 state <=  #1  IDLE;
+               end
+    GNT1 : if (req_1 == 1'b1) begin
+                 state <=  #1  GNT2;
+				 gnt_1 <= req_0;
+               end
+    GNT2 : if (req_0 == 1'b1) begin
+                 state <=  #1  GNT1;
+				 gnt_1 <= req_1;
+               end 
+    default : state <=  #1  IDLE;
+ endcase
+ end
+ 
+ endmodule
+ 
+ module top (
+input clk,
+input rst,
+input a,
+input b,
+output g0,
+output g1
+);
+
+fsm u_fsm ( .clock(clk),
+            .reset(rst), 
+            .req_0(a), 
+            .req_1(b), 
+            .gnt_0(g0), 
+            .gnt_1(g1));
+
+endmodule

backends/write_smt2_init_assert/top.v

@@ -10,8 +10,8 @@ module top
  );
 
  reg ASSERT = 1;
- (* anyconst *) reg foo;
- (* anyseq *) reg too;
+ (* allconst *) reg foo;
+ (* allseq *) reg too;
 
 
 

backends/write_verilog_shift_shiftx/testbench.v

+module testbench;
+    reg clk;
+
+    initial begin
+        // $dumpfile("testbench.vcd");
+        // $dumpvars(0, testbench);
+
+        #5 clk = 0;
+        repeat (10000) begin
+            #5 clk = 1;
+            #5 clk = 0;
+        end
+
+        $display("OKAY");    
+    end
+   
+    function [31:0] xorshift32;
+        input [31:0] arg;
+        begin
+                xorshift32 = arg;
+                // Xorshift32 RNG, doi:10.18637/jss.v008.i14
+                xorshift32 = xorshift32 ^ (xorshift32 << 13);
+                xorshift32 = xorshift32 ^ (xorshift32 >> 17);
+                xorshift32 = xorshift32 ^ (xorshift32 <<  5);
+        end
+    endfunction
+
+    reg [31:0] rng = 123456789;
+    always @(posedge clk) rng <= xorshift32(rng);
+
+    wire a = xorshift32(rng * 5);
+    wire b = xorshift32(rng * 7);
+    reg rst;
+    wire g0;
+    wire g1;
+    
+    top uut (
+        .a (a),
+        .b (b),
+        .clk (clk),
+        .rst (rst),
+        .g0(g0),
+        .g1(g1)
+    );
+    
+    initial begin
+        rst <= 1;
+        #5
+        rst <= 0;
+    end
+	
+    assert_Z g0_test(.clk(clk), .A(g0));
+	assert_Z g1_test(.clk(clk), .A(g1));
+  
+endmodule

backends/write_verilog_shift_shiftx/top.v

+ module fsm (
+ clock,
+ reset,
+ req_0,
+ req_1,
+ gnt_0,
+ gnt_1
+ );
+ input   clock,reset,req_0,req_1;
+ output signed   gnt_0,gnt_1;
+ wire    clock,reset,req_0,req_1;
+ reg     gnt_0,gnt_1;
+
+ parameter SIZE = 3           ;
+ parameter IDLE  = 3'b001,GNT0 = 3'b010,GNT1 = 3'b100,GNT2 = 3'b101 ;
+
+ reg signed [SIZE-1:0] state;
+ reg signed [SIZE-1:0] next_state;
+
+ always @ (posedge clock)
+ begin : FSM
+ if (reset == 1'b1) begin
+   state <=  #1  IDLE;
+   gnt_0 <= 0;
+   gnt_1 <= 0;
+ end else
+  case(state)
+    IDLE : if (req_0 == 1'b1) begin
+                 state <=  #1  GNT0;
+`ifndef BUG
+                 gnt_0 <= 1;
+`else
+                 gnt_0 <= 1'bZ;
+`endif
+               end else if (req_1 == 1'b1) begin
+                 gnt_1 <= 1;
+                 state <=  #1  GNT0;
+               end else begin
+                 state <=  #1  IDLE;
+               end
+    GNT0 : if (req_0 == 1'b1) begin
+                 state <=  #1  GNT0;
+               end else begin
+                 gnt_0 <= 0;
+                 state <=  #1  IDLE;
+               end
+    GNT1 : if (req_1 == 1'b1) begin
+                 state <=  #1  GNT2;
+				 gnt_1 <= req_0;
+               end
+    GNT2 : if (req_0 == 1'b1) begin
+                 state <=  #1  GNT1;
+				 gnt_1 <= req_1;
+               end
+    default : state <=  #1  IDLE;
+ endcase
+ end
+
+ endmodule
+
+ module top (
+input clk,
+input rst,
+input a,
+input b,
+output g0,
+output g1
+);
+
+fsm u_fsm ( .clock(clk),
+            .reset(rst),
+            .req_0(a),
+            .req_1(b),
+            .gnt_0(g0),
+            .gnt_1(g1));
+
+endmodule

backends/write_xaiger/testbench.v

+module testbench;
+    reg [2:0] in;
+
+	reg patt_out = 0;
+	reg patt_carry_out = 0;
+	wire out;
+    wire carryout;
+
+    initial begin
+        // $dumpfile("testbench.vcd");
+        // $dumpvars(0, testbench);
+
+        #5 in = 0;
+        repeat (10000) begin
+            #5 in = in + 1;
+        end
+
+        $display("OKAY");
+    end
+
+    top uut (
+	.x(in[0]),
+	.y(in[1]),
+	.cin(in[2]),
+	.A(out),
+	.cout(carryout)
+	);
+	
+	always @(posedge in[0]) 
+        patt_out <=  in[1] + in[2];
+    always @(negedge in[0])
+        patt_carry_out <=  in[1] + patt_out;
+
+	assert_comb out_test(.A(patt_out), .B(out));
+	assert_comb carry_test(.A(patt_carry_out), .B(carryout));
+
+endmodule

backends/write_xaiger/top.v

+module top
+(
+ input x,
+ input y,
+ input cin,
+
+ output reg A,
+ output reg cout
+ );
+ 
+ reg ASSERT = 1;
+ (* anyconst *) reg foo;
+ (* anyseq *) reg too;
+ 
+
+ 
+ initial begin
+    begin
+        A = 0;
+        cout = 0;
+    end
+ end
+
+`ifndef BUG
+always @(posedge x) begin
+    if ($initstate) 
+        A <= 0;
+    A <=  y + cin + too;
+    assume(too);    
+    assume(s_eventually too);
+end
+always @(negedge x) begin
+    if ($initstate) 
+        cout <= 0;
+        cout <=  y + A + foo;
+    assert(ASSERT);
+    assert(s_eventually ASSERT);
+end
+`else
+assign {cout,A} =  cin - y * x;
+`endif
+
+endmodule

backends/write_xaiger/top_clean.v

+module top
+(
+ input x,
+ input y,
+ input cin,
+
+ output reg A,
+ output reg cout
+ );
+ 
+ initial begin
+    A = 0;
+    cout = 0;
+ end
+
+`ifndef BUG
+always @(posedge x) begin
+    A <=  y + cin;
+end
+always @(negedge x) begin
+    cout <=  y + A;
+end
+`else
+assign {cout,A} =  cin - y * x;
+`endif
+
+endmodule

backends/write_xaiger_error/testbench.v

+module testbench;
+    reg [2:0] in;
+
+	reg patt_out = 0;
+	reg patt_carry_out = 0;
+	wire out;
+    wire carryout;
+
+    initial begin
+        // $dumpfile("testbench.vcd");
+        // $dumpvars(0, testbench);
+
+        #5 in = 0;
+        repeat (10000) begin
+            #5 in = in + 1;
+        end
+
+        $display("OKAY");
+    end
+
+    top uut (
+	.x(in[0]),
+	.y(in[1]),
+	.cin(in[2]),
+	.A(out),
+	.cout(carryout)
+	);
+	
+	always @(posedge in[0]) 
+        patt_out <=  in[1] + in[2];
+    always @(negedge in[0])
+        patt_carry_out <=  in[1] + patt_out;
+
+	assert_comb out_test(.A(patt_out), .B(out));
+	assert_comb carry_test(.A(patt_carry_out), .B(carryout));
+
+endmodule

backends/write_xaiger_error/top.v

+module top
+(
+ input x,
+ input y,
+ input cin,
+
+ output reg A,
+ output reg cout
+ );
+
+ reg ASSERT = 1;
+ (* anyconst *) reg foo;
+ (* anyseq *) reg too;
+
+
+
+ initial begin
+    begin
+        A = 0;
+        cout = 0;
+    end
+ end
+
+`ifndef BUG
+always @(posedge x) begin
+    if ($initstate)
+        A <= 0;
+    A <=  y + cin + too;
+    assume(too);
+    assume(s_eventually too);
+end
+always @(negedge x) begin
+    if ($initstate)
+        cout <= 0;
+        cout <=  y + A + foo;
+    assert(ASSERT);
+    assert(s_eventually ASSERT);
+end
+`else
+assign {cout,A} =  cin - y * x;
+`endif
+
+endmodule
+
+module top2
+(
+ input x,
+ input y,
+ input cin,
+
+ output reg A,
+ output reg cout
+ );
+
+ reg ASSERT = 1;
+ (* anyconst *) reg foo;
+ (* anyseq *) reg too;
+
+
+
+ initial begin
+    begin
+        A = 0;
+        cout = 0;
+    end
+ end
+
+`ifndef BUG
+always @(posedge x) begin
+    if ($initstate)
+        A <= 0;
+    A <=  y + cin + too;
+    assume(too);
+    assume(s_eventually too);
+end
+always @(negedge x) begin
+    if ($initstate)
+        cout <= 0;
+        cout <=  y + A + foo;
+    assert(ASSERT);
+    assert(s_eventually ASSERT);
+end
+`else
+assign {cout,A} =  cin - y * x;
+`endif
+
+endmodule

backends/write_xaiger_error/top2.v

+module top
+(
+ input x,
+ input y,
+ input cin,
+
+ output reg A,
+ output reg cout,
+ output X
+ );
+
+ reg ASSERT = 1'bX;
+ (* anyconst *) reg foo;
+ (* anyseq *) reg too;
+
+
+
+ initial begin
+    begin
+        A = 1'bX;
+        cout = 1'bZ;
+    end
+ end
+
+`ifndef BUG
+always @(posedge x) begin
+    if ($initstate)
+        A <= 1'bX;
+    A <=  y + cin + too;
+    assume(too);
+    assume(s_eventually too);
+end
+always @(negedge x) begin
+    if ($initstate)
+        cout <= 1'bZ;
+        cout <=  y + A + foo;
+    assert(ASSERT);
+    assert(s_eventually ASSERT);
+end
+
+assign X = 1'bX;
+`else
+assign {cout,A} =  cin - y * x;
+`endif
+
+endmodule
+

backends/write_xaiger_error/top_clean.v

+module top
+(
+ input x,
+ input y,
+ input cin,
+
+ output reg A,
+ output reg cout
+ );
+ 
+ initial begin
+    A = 0;
+    cout = 0;
+ end
+
+`ifndef BUG
+always @(posedge x) begin
+    A <=  y + cin;
+end
+always @(negedge x) begin
+    cout <=  y + A;
+end
+`else
+assign {cout,A} =  cin - y * x;
+`endif
+
+endmodule

backends/write_xaiger_fsm/testbench.v

+module testbench;
+    reg clk;
+
+    initial begin
+        // $dumpfile("testbench.vcd");
+        // $dumpvars(0, testbench);
+
+        #5 clk = 0;
+        repeat (10000) begin
+            #5 clk = 1;
+            #5 clk = 0;
+        end
+
+        $display("OKAY");    
+    end
+   
+    
+    reg a = 0;
+    reg b = 0;
+    reg rst;    
+    reg en;
+    wire s;
+    wire bs;
+    wire f;
+    
+    top uut ( .clk(clk),
+              .rst(rst), 
+              .en(en), 
+              .a(a), 
+              .b(b), 
+              .s(s), 
+              .bs(bs), 
+              .f(f));
+              
+    always @(posedge clk)
+    begin
+        #2
+        a <= ~a;
+    end
+    
+    always @(posedge clk)
+    begin
+        #4
+        b <= ~b;
+    end
+    
+    initial begin
+        en <= 1;
+        rst <= 1;
+        #5
+        rst <= 0;
+    end
+    
+    
+    assert_expr s_test(.clk(clk), .A(s));
+	assert_expr bs_test(.clk(clk), .A(bs));
+	assert_expr f_test(.clk(clk), .A(f));
+  
+endmodule
+
+
+module assert_expr(input clk, input A);
+    always @(posedge clk)
+    begin
+        //#1;
+        if (A == 1'bZ)
+        begin
+            $display("ERROR: ASSERTION FAILED in %m:",$time," ",A);
+            $stop;
+        end
+    end
+endmodule

backends/write_xaiger_fsm/top.v

+module top (
+input clk,
+input rst,
+input en,
+input a,
+input b,
+output s,
+output bs,
+output f
+);
+
+
+    parameter S0 = 4'b0000, S1 = 4'b0001, S2 = 4'b0010, S3 = 4'b0011, S4 = 4'b0100, S5 = 4'b0101, S6 = 4'b0110, S7 = 4'b0111, S8 = 4'b1000, S9 = 4'b1001, S10 = 4'b1010, S11 = 4'b1011, S12 = 4'b1100, S13 = 4'b1101, S14 = 4'b1110;
+
+	reg [3:0] ns, st;
+
+	reg [2:0] count;
+
+
+	always @(posedge clk)
+	begin : CurrstProc
+		if (rst)
+			st <= S0;
+		else
+			st <= ns;
+	end
+
+	always @*
+	begin : NextstProc
+		ns = st;
+		case (st)
+			S0: ns = S1;
+			S1: ns = S2;
+			S2:
+				if (b == 1'b1)
+					ns = S3;
+				else
+					ns = S4;
+			S3: ns = S1;
+			S4: if (count > 7)
+					ns = S10;
+				else
+					ns = S5;
+			S5: if (a == 1'b0)
+					ns = S6;
+				else
+					ns = S3;
+			S6:
+				if (a == 1'b1)
+					ns = S7;
+				else
+					ns = S8;
+			S7:
+				if (a == 1'b1 && b == 1'b1)
+					ns = S5;
+				else
+					ns = S13;
+			S8: ns = S9;
+			S9: ns = S8;
+			S10:
+				if (a == 1'b1 || b == 1'b1)
+					ns = S11;
+				else
+					ns = S4;
+			S11: ns = S12;
+			S12: ns = S10;
+			S13: ;
+			default: ns = S0;
+		endcase;
+	end
+
+	always @(posedge clk)
+		if(~rst)
+			count <= 0;
+		else
+		begin
+			if(st == S4)
+				if (count > 7)
+					count <= 0;
+				else
+					count <= count + 1;
+		end
+
+	//FSM outputs (combinatorial)
+
+	assign s   = (st == S3 || st == S12) ? 1'b1 : 1'b0;
+
+	assign f = (st == S13) ? 1'b1 : 1'b0;
+
+	assign bs   = (st == S8 || st == S9) ? 1'b1 : 1'b0;
+
+endmodule

backends/write_xaiger_fsm/top_clean.v

+module top (
+input clk,
+input rst,
+input en,
+input a,
+input b,
+output s,
+output bs,
+output f
+);
+
+
+    parameter S0 = 4'b0000, S1 = 4'b0001, S2 = 4'b0010, S3 = 4'b0011, S4 = 4'b0100, S5 = 4'b0101, S6 = 4'b0110, S7 = 4'b0111, S8 = 4'b1000, S9 = 4'b1001, S10 = 4'b1010, S11 = 4'b1011, S12 = 4'b1100, S13 = 4'b1101, S14 = 4'b1110;
+
+	reg [3:0] ns, st;
+
+	reg [2:0] count;
+
+
+	always @(posedge clk)
+	begin : CurrstProc
+		if (rst)
+			st <= S0;
+		else
+			st <= ns;
+	end
+
+	always @*
+	begin : NextstProc
+		ns = st;
+		case (st)
+			S0: ns = S1;
+			S1: ns = S2;
+			S2:
+				if (b == 1'b1)
+					ns = S3;
+				else
+					ns = S4;
+			S3: ns = S1;
+			S4: if (count > 7)
+					ns = S10;
+				else
+					ns = S5;
+			S5: if (a == 1'b0)
+					ns = S6;
+				else
+					ns = S3;
+			S6:
+				if (a == 1'b1)
+					ns = S7;
+				else
+					ns = S8;
+			S7:
+				if (a == 1'b1 && b == 1'b1)
+					ns = S5;
+				else
+					ns = S13;
+			S8: ns = S9;
+			S9: ns = S8;
+			S10:
+				if (a == 1'b1 || b == 1'b1)
+					ns = S11;
+				else
+					ns = S4;
+			S11: ns = S12;
+			S12: ns = S10;
+			S13: ;
+			default: ns = S0;
+		endcase;
+	end
+
+	always @(posedge clk)
+		if(~rst)
+			count <= 0;
+		else
+		begin
+			if(st == S4)
+				if (count > 7)
+					count <= 0;
+				else
+					count <= count + 1;
+		end
+
+	//FSM outputs (combinatorial)
+
+	assign s   = (st == S3 || st == S12) ? 1'b1 : 1'b0;
+
+	assign f = (st == S13) ? 1'b1 : 1'b0;
+
+	assign bs   = (st == S8 || st == S9) ? 1'b1 : 1'b0;
+
+endmodule

backends/write_xaiger_mem/testbench.v

+module testbench;
+    reg clk;
+
+    initial begin
+        // $dumpfile("testbench.vcd");
+        // $dumpvars(0, testbench);
+
+        #5 clk = 0;
+        repeat (10000) begin
+            #5 clk = 1;
+            #5 clk = 0;
+        end
+
+        $display("OKAY");    
+    end
+   
+    
+    reg [7:0] data_a = 0;
+	reg [7:0] data_b = 0;
+	reg [5:0] addr_a = 0;	
+	reg [5:0] addr_b = 0;
+    reg we_a = 0;
+	reg we_b = 1;	
+    reg re_a = 1;
+	reg re_b = 1;
+	wire [7:0] q_a,q_b;
+	reg mem_init = 0;
+
+    top uut (
+    .data_a(data_a),
+	.data_b(data_b),
+	.addr_a(addr_a),
+	.addr_b(addr_b),
+	.we_a(we_a), 
+	.we_b(we_b), 	
+	.re_a(re_a), 
+	.re_b(re_b), 
+	.clka(clk),
+	.clkb(clk),
+	.q_a(q_a), 
+	.q_b(q_b)
+    );
+    
+    always @(posedge clk) begin
+    #3;
+    data_a <= data_a + 17;	
+    data_b <= data_b + 5;
+	
+    addr_a <= addr_a + 1;	
+    addr_b <= addr_b + 1;
+    end
+    
+    always @(posedge addr_a) begin
+    #10;
+        if(addr_a > 6'h3E)
+            mem_init <= 1;
+    end
+	
+	always @(posedge clk) begin
+    //#3;
+    we_a <= !we_a; 
+    we_b <= !we_b; 
+    end
+	
+	uut_mem_checker port_a_test(.clk(clk), .init(mem_init), .en(!we_a), .A(q_a));
+    uut_mem_checker port_b_test(.clk(clk), .init(mem_init), .en(!we_b), .A(q_b));
+    
+endmodule
+
+module uut_mem_checker(input clk, input init, input en, input [7:0] A);
+    always @(posedge clk)
+    begin
+        #1;
+        if (en == 1 & init == 1 & A === 8'bXXXXXXXX)
+        begin
+            $display("ERROR: ASSERTION FAILED in %m:",$time," ",A);
+            $stop;
+        end
+    end
+endmodule

backends/write_xaiger_mem/top.v

+module top
+(
+	input [7:0] data_a, data_b,
+	input [6:1] addr_a, addr_b,
+	input we_a, we_b, re_a, re_b, clka, clkb,
+	output reg [7:0] q_a, q_b
+);
+	// Declare the RAM variable
+	reg [7:0] ram[63:0];
+	
+	initial begin
+        q_a <= 8'h00;        
+        q_b <= 8'd0;
+	end
+	
+	// Port A
+	always @ (posedge clka)
+	begin
+`ifndef BUG        
+		if (we_a) 
+`else        
+		if (we_b) 
+`endif
+		begin
+			ram[addr_a] <= data_a;
+			q_a <= data_a;
+		end
+		if (re_b) 
+		begin
+			q_a <= ram[addr_a];
+		end
+	end
+	
+	// Port B
+	always @ (posedge clkb)
+	begin
+`ifndef BUG        
+		if (we_b) 
+`else        
+		if (we_a) 
+`endif
+		begin
+			ram[addr_b] <= data_b;
+			q_b <= data_b;
+		end
+		if (re_b)
+		begin
+			q_b <= ram[addr_b];
+		end
+	end
+	
+endmodule								 

backends/write_xaiger_mem/top_clean.v

+module top
+(
+	input [7:0] data_a, data_b,
+	input [6:1] addr_a, addr_b,
+	input we_a, we_b, re_a, re_b, clka, clkb,
+	output reg [7:0] q_a, q_b
+);
+	// Declare the RAM variable
+	reg [7:0] ram[63:0];
+	
+	initial begin
+        q_a <= 8'h00;        
+        q_b <= 8'd0;
+	end
+	
+	// Port A
+	always @ (posedge clka)
+	begin
+`ifndef BUG        
+		if (we_a) 
+`else        
+		if (we_b) 
+`endif
+		begin
+			ram[addr_a] <= data_a;
+			q_a <= data_a;
+		end
+		if (re_b) 
+		begin
+			q_a <= ram[addr_a];
+		end
+	end
+	
+	// Port B
+	always @ (posedge clkb)
+	begin
+`ifndef BUG        
+		if (we_b) 
+`else        
+		if (we_a) 
+`endif
+		begin
+			ram[addr_b] <= data_b;
+			q_b <= data_b;
+		end
+		if (re_b)
+		begin
+			q_b <= ram[addr_b];
+		end
+	end
+	
+endmodule								 

equiv/Makefile

@@ -59,7 +59,7 @@ $(eval $(call template,equiv_add,equiv_add equiv_add_try ))
 $(eval $(call template,equiv_add_error,equiv_add_module_context ))
 
 #equiv_opt
-$(eval $(call template,equiv_opt,equiv_opt equiv_opt_run equiv_opt_map))
+$(eval $(call template,equiv_opt,equiv_opt equiv_opt_run equiv_opt_map equiv_opt_undef))
 $(eval $(call template,equiv_opt_error,equiv_opt_unknown_option equiv_opt_no_opt equiv_opt_fully_selected_des))
 
 .PHONY: all clean

equiv/scripts/equiv_opt_undef.ys

+read_verilog ../top.v
+prep -flatten -top top
+splitnets -ports;;
+design -stash gold
+read_verilog ../synth_top.v
+read_verilog ../logic.v
+prep -flatten -top top
+splitnets -ports;;
+design -stash gate
+design -copy-from gold -as gold top
+design -copy-from gate -as gate top
+equiv_make gold gate equiv
+equiv_opt -undef equiv_purge
+design -reset
+read_verilog ../top.v
+write_verilog synth.v

frontends/read_liberty_tech/testbench.v

+module testbench;
+    reg a;
+
+	wire b;
+
+    initial begin
+        // $dumpfile("testbench.vcd");
+        // $dumpvars(0, testbench);
+
+        #5 a = 0;
+        repeat (10000) begin
+            #5 a = ~a;
+        end
+
+        $display("OKAY");
+    end
+
+    top uut (
+	.A(a),
+	.Y(b)
+	);
+
+	assert_comb b_test(.A(~a),.B(b));
+
+endmodule

frontends/read_verilog_assert/testbench.v

+module testbench;
+    reg [2:0] in;
+
+	reg patt_out = 0;
+	reg patt_carry_out = 0;
+	wire out;
+    wire carryout;
+
+    initial begin
+        // $dumpfile("testbench.vcd");
+        // $dumpvars(0, testbench);
+
+        #5 in = 0;
+        repeat (10000) begin
+            #5 in = in + 1;
+        end
+
+        $display("OKAY");
+    end
+
+    top uut (
+	.x(in[0]),
+	.y(in[1]),
+	.cin(in[2]),
+	.A(out),
+	.cout(carryout)
+	);
+	
+	always @(posedge in[0]) 
+        patt_out <=  in[1] + in[2];
+    always @(negedge in[0])
+        patt_carry_out <=  in[1] + patt_out;
+
+	assert_comb out_test(.A(patt_out), .B(out));
+	assert_comb carry_test(.A(patt_carry_out), .B(carryout));
+
+endmodule

frontends/read_verilog_assert/top.v

+module top
+(
+ input x,
+ input y,
+ input cin,
+
+ output reg A,
+ output reg cout
+ );
+
+ reg ASSERT = 1;
+ (* allconst *) reg foo;
+ (* allseq *) reg too;
+
+
+
+ initial begin
+    begin
+        A = 0;
+        cout = 0;
+    end
+ end
+
+`ifndef BUG
+always @(posedge x) begin
+    if ($initstate)
+        A <= 0;
+    A <=  y + cin + too;
+    assume(too);
+    assume(s_eventually too);
+end
+always @(negedge x) begin
+    if ($initstate)
+        cout <= 0;
+        cout <=  y + A + foo;
+    assert(ASSERT);
+    assert(s_eventually ASSERT);
+end
+`else
+assign {cout,A} =  cin - y * x;
+`endif
+
+endmodule

frontends/read_verilog_assert/top_clean.v

+module top
+(
+ input x,
+ input y,
+ input cin,
+
+ output reg A,
+ output reg cout
+ );
+ 
+ initial begin
+    A = 0;
+    cout = 0;
+ end
+
+`ifndef BUG
+always @(posedge x) begin
+    A <=  y + cin;
+end
+always @(negedge x) begin
+    cout <=  y + A;
+end
+`else
+assign {cout,A} =  cin - y * x;
+`endif
+
+endmodule

frontends/read_verilog_attributes/testbench.v

+module testbench;
+    reg clk;
+
+    initial begin
+        // $dumpfile("testbench.vcd");
+        // $dumpvars(0, testbench);
+
+        #5 clk = 0;
+        repeat (10000) begin
+            #5 clk = 1;
+            #5 clk = 0;
+        end
+
+        $display("OKAY");    
+    end
+   
+    
+    reg [15:0] D = 1;
+    reg [3:0] S = 0;
+    wire M2,M4,M8,M16;
+
+    top uut (
+        .S (S ),
+        .D (D ),
+        .M2 (M2 ),
+        .M4 (M4 ),
+        .M8 (M8 ),
+        .M16 (M16 )
+    );
+    
+    always @(posedge clk) begin
+    //#3;
+	D <= {D[14:0],D[15]};
+    //D <= D <<< 1;
+    S <= S + 1;
+    end
+	
+	assert_tri m2_test(.en(clk), .A(D[0]|D[1]), .B(M2));
+	assert_tri m4_test(.en(clk), .A(D[0]|D[1]|D[2]|D[3]), .B(M4));
+	assert_tri m8_test(.en(clk), .A(!S[3]), .B(M8));
+	assert_tri m16_test(.en(clk), .A(1'b1), .B(M16));
+  
+endmodule

frontends/read_verilog_attributes/top.v

+(* black_box *) module mux2 (S,A,B,Y);
+    input S;
+    input A,B;
+    output reg Y;
+`ifndef BUG
+
+    always @(*)
+		Y = (S)? B : A;
+`else
+
+    always @(*)
+		Y = (~S)? B : A;
+`endif
+endmodule
+
+(* white_box *)module mux4 ( S, D, Y );
+
+input[1:0] S;
+input[3:0] D;
+output Y;
+
+reg Y;
+wire[1:0] S;
+wire[3:0] D;
+
+always @*
+begin
+    case( S )
+       0 : Y = D[0];
+       1 : Y = D[1];
+`ifndef BUG
+       2 : Y = D[2];
+`else
+       2 : Y = D[3];
+`endif
+       3 : Y = D[3];
+   endcase
+end
+
+endmodule
+
+module mux8 ( S, D, Y );
+
+input[2:0] S;
+input[7:0] D;
+output Y;
+
+reg Y;
+wire[2:0] S;
+wire[7:0] D;
+
+always @*
+begin
+   case( S )
+       0 : Y = D[0];
+       1 : Y = D[1];
+       2 : Y = D[2];
+       3 : Y = D[3];
+`ifndef BUG
+       4 : Y = D[4];
+`else
+       4 : Y = D[7];
+`endif
+       5 : Y = D[5];
+       6 : Y = D[6];
+       7 : Y = D[7];
+   endcase
+end
+
+endmodule
+
+module mux16 (D, S, Y);
+ 	input  [15:0] D;
+ 	input  [3:0] S;
+ 	output Y;
+
+assign Y = D[S];
+
+endmodule
+
+
+module top (
+input [3:0] S,
+input [15:0] D,
+output M2,M4,M8,M16
+);
+
+mux2 u_mux2 (
+        .S (S[0]),
+        .A (D[0]),
+        .B (D[1]),
+        .Y (M2)
+    );
+
+
+mux4 u_mux4 (
+        .S (S[1:0]),
+        .D (D[3:0]),
+        .Y (M4)
+    );
+
+mux8 u_mux8 (
+        .S (S[2:0]),
+        .D (D[7:0]),
+        .Y (M8)
+    );
+
+mux16 u_mux16 (
+        .S (S[3:0]),
+        .D (D[15:0]),
+        .Y (M16)
+    );
+
+endmodule

frontends/read_verilog_comparison/testbench.v

+module testbench;
+    reg clk;
+
+    initial begin
+        // $dumpfile("testbench.vcd");
+        // $dumpvars(0, testbench);
+
+        #5 clk = 0;
+        repeat (10000) begin
+            #5 clk = 1;
+            #5 clk = 0;
+        end
+
+        $display("OKAY");
+    end
+
+
+    reg [15:0] I0 = 1;
+    reg [15:0] I1 = 0;
+    wire A,B,C,D,E,F;
+    reg Ap,Bp,Cp,Dp,Ep,Fp;
+
+    top uut (
+		.clk (clk),
+        .I0 (I0 ),
+        .I1 (I1 ),
+        .A (A ),
+        .B (B ),
+        .C (C ),
+        .D (D ),
+        .E (E ),
+        .F (F )
+    );
+
+    always @(posedge clk)
+	begin
+		if (I0 < I1)
+			Ap <= 1'b1;
+		else
+			Ap <= 1'b0;
+
+		if (I0 <= I1)
+			Bp <= 1'b1;
+		else
+			Bp <= 1'b0;
+
+		if (I0 != I1)
+			Cp <= 1'b1;
+		else
+			Cp <= 1'b0;
+
+		if (I0 === I1)
+			Dp <= 1'b1;
+		else
+			Dp <= 1'b0;
+
+		if (I0 !== I1)
+			Ep <= 1'b1;
+		else
+			Ep <= 1'b0;
+
+		if (I0 >= I1)
+			Fp <= 1'b1;
+		else
+			Fp <= 1'b0;
+	end
+
+    always @(posedge clk) begin
+    //#3;
+	I0 <= {I0[14:0],I0[15]};
+    //D <= D <<< 1;
+    I1 <= I1 + 1;
+    end
+
+	assert_tri A_test(.en(clk), .A(A), .B(Ap));
+	assert_tri B_test(.en(clk), .A(B), .B(Bp));
+	assert_tri C_test(.en(clk), .A(C), .B(Cp));
+	//assert_tri D_test(.en(clk), .A(D), .B(Dp));
+	assert_tri E_test(.en(clk), .A(E), .B(Ep));
+	assert_tri F_test(.en(clk), .A(F), .B(Fp));
+
+endmodule

frontends/read_verilog_comparison/top.v

+module top (
+input clk,
+input [15:0] I0,
+input [15:0] I1,
+output reg A,B,C,D,E,F
+);
+
+always @(posedge clk)
+begin
+    if (I0 < I1)
+		A <= 1'b1;
+	else
+		A <= 1'b0;
+
+	if (I0 <= I1)
+		B <= 1'b1;
+	else
+		B <= 1'b0;
+
+	if (I0 != I1)
+		C <= 1'b1;
+	else
+		C <= 1'b0;
+
+	if (I0 === I1)
+		D <= 1'b1;
+	else
+		D <= 1'b0;
+
+	if (I0 !== I1)
+		E <= 1'b1;
+	else
+		E <= 1'b0;
+
+	if (I0 >= I1)
+		F <= 1'b1;
+	else
+		F <= 1'b0;
+
+end
+
+
+endmodule

frontends/read_verilog_div_mod/testbench.v

+module testbench;
+    reg [2:0] in;
+
+	wire patt_out,out;
+	wire patt_carry_out,carryout;
+
+    initial begin
+         $dumpfile("testbench.vcd");
+         $dumpvars(0, testbench);
+
+        #5 in = 0;
+        repeat (10000) begin
+            #5 in = in + 1;
+        end
+
+        $display("OKAY");
+    end
+
+    top uut (
+	.x(in[0]),
+	.y(in[1]),
+	.cin(in[2]),
+	.A(out),
+	.cout(carryout)
+	);
+
+	assign {patt_carry_out,patt_out} =  in[2] % in[1] / in[0];
+
+	assert_Z out_test(in[0], out);
+	assert_Z carry_test(in[0], carryout);
+
+endmodule
+

frontends/read_verilog_div_mod/top.v

+module top
+(
+ input x,
+ input y,
+ input cin,
+
+ output A,
+ output cout
+ );
+
+ wire pow,p,n;
+
+`ifndef BUG
+assign {cout,A} =  cin % y / x;
+
+assign pow =  y ** x;
+
+assign p =  +x;
+assign n =  -x;
+`else
+assign {cout,A} =  2'bZZ;
+`endif
+
+endmodule

frontends/read_verilog_dpi/testbench.v

+module testbench;
+    reg clk;
+
+    initial begin
+        // $dumpfile("testbench.vcd");
+        // $dumpvars(0, testbench);
+
+        #5 clk = 0;
+        repeat (10000) begin
+            #5 clk = 1;
+            #5 clk = 0;
+        end
+
+        $display("OKAY");    
+    end
+   
+    
+    reg [15:0] D = 1;
+    reg [3:0] S = 0;
+    wire M2,M4,M8,M16;
+
+    top uut (
+        .S (S ),
+        .D (D ),
+        .M2 (M2 ),
+        .M4 (M4 ),
+        .M8 (M8 ),
+        .M16 (M16 )
+    );
+    
+    always @(posedge clk) begin
+    //#3;
+	D <= {D[14:0],D[15]};
+    //D <= D <<< 1;
+    S <= S + 1;
+    end
+	
+	assert_tri m2_test(.en(clk), .A(D[0]|D[1]), .B(M2));
+	assert_tri m4_test(.en(clk), .A(D[0]|D[1]|D[2]|D[3]), .B(M4));
+	assert_tri m8_test(.en(clk), .A(!S[3]), .B(M8));
+	assert_tri m16_test(.en(clk), .A(1'b1), .B(M16));
+  
+endmodule

frontends/read_verilog_dpi/top.v

+module mux2 (S,A,B,Y);
+    input S;
+    input A,B;
+    output reg Y;
+`ifndef BUG
+
+    always @(*)
+		Y = (S)? B : A;
+`else
+
+    always @(*)
+		Y = (~S)? B : A;
+`endif
+endmodule
+
+module mux4 ( S, D, Y );
+
+input[1:0] S;
+input[3:0] D;
+output Y;
+
+reg Y;
+wire[1:0] S;
+wire[3:0] D;
+
+always @*
+begin
+    case( S )
+       0 : Y = D[0];
+       1 : Y = D[1];
+`ifndef BUG
+       2 : Y = D[2];
+`else
+       2 : Y = D[3];
+`endif
+       3 : Y = D[3];
+   endcase
+end
+
+endmodule
+
+module mux8 ( S, D, Y );
+
+input[2:0] S;
+input[7:0] D;
+output Y;
+
+reg Y;
+wire[2:0] S;
+wire[7:0] D;
+
+always @*
+begin
+   case( S )
+       0 : Y = D[0];
+       1 : Y = D[1];
+       2 : Y = D[2];
+       3 : Y = D[3];
+`ifndef BUG
+       4 : Y = D[4];
+`else
+       4 : Y = D[7];
+`endif
+       5 : Y = D[5];
+       6 : Y = D[6];
+       7 : Y = D[7];
+   endcase
+end
+
+endmodule
+
+module mux16 (D, S, Y);
+ 	input  [15:0] D;
+ 	input  [3:0] S;
+ 	output Y;
+
+assign Y = D[S];
+
+endmodule
+
+
+module top (
+input [3:0] S,
+input [15:0] D,
+output M2,M4,M8,M16
+);
+
+mux2 u_mux2 (
+        .S (S[0]),
+        .A (D[0]),
+        .B (D[1]),
+        .Y (M2)
+    );
+
+
+mux4 u_mux4 (
+        .S (S[1:0]),
+        .D (D[3:0]),
+        .Y (M4)
+    );
+
+mux8 u_mux8 (
+        .S (S[2:0]),
+        .D (D[7:0]),
+        .Y (M8)
+    );
+
+mux16 u_mux16 (
+        .S (S[3:0]),
+        .D (D[15:0]),
+        .Y (M16)
+    );
+
+endmodule
+
+
+
+package my_pkg;
+	localparam u = 0;
+endpackage
+
+
+module tb_dpi;
+
+  import "DPI-C" function int add();
+	wire logic w;
+
+endmodule
+
+module hello();
+    import "DPI-C" function void print_hello();
+endmodule

frontends/read_verilog_ff_edge/testbench.v

+module testbench;
+    reg clk;
+
+    initial begin
+        // $dumpfile("testbench.vcd");
+        // $dumpvars(0, testbench);
+
+        #5 clk = 0;
+        repeat (10000) begin
+            #5 clk = 1;
+            #5 clk = 0;
+        end
+
+        $display("OKAY");    
+    end
+   
+    
+    reg [2:0] dinA = 0;
+    wire doutB,doutB1,doutB2,doutB3,doutB4;
+	reg dff,ndff,adff,adffn,dffe = 0;
+
+    top uut (
+        .clk (clk ),
+        .a (dinA[0] ),
+        .pre (dinA[1] ),
+        .clr (dinA[2] ),
+        .b (doutB ),
+        .b1 (doutB1 ),
+        .b2 (doutB2 ),
+        .b3 (doutB3 ),
+        .b4 (doutB4 )
+    );
+    
+    always @(posedge clk) begin
+    #3;
+    dinA <= dinA + 1;
+    end
+	
+	always @( posedge clk, posedge dinA[1], posedge dinA[2] )
+		if ( dinA[2] )
+			dff <= 1'b0;
+		else if ( dinA[1] )
+			dff <= 1'b1;
+		else
+            dff <= dinA[0];
+    
+    always @( negedge clk, negedge dinA[1], negedge dinA[2] )
+		if ( !dinA[2] )
+			ndff <= 1'b0;
+		else if ( !dinA[1] )
+			ndff <= 1'b1;
+		else
+            ndff <= dinA[0];
+            
+    always @( posedge clk, posedge dinA[2] )
+		if ( dinA[2] )
+			adff <= 1'b0;
+		else
+            adff <= dinA[0];
+            
+    always @( posedge clk, negedge dinA[2] )
+		if ( !dinA[2] )
+			adffn <= 1'b0;
+		else
+            adffn <= dinA[0];
+
+    always @( posedge clk )
+		if ( dinA[2] )
+            dffe <= dinA[0];
+            
+	assert_dff dff_test(.clk(clk), .test(doutB), .pat(dff));
+    assert_dff ndff_test(.clk(clk), .test(doutB1), .pat(ndff));
+    assert_dff adff_test(.clk(clk), .test(doutB2), .pat(adff));    
+    assert_dff adffn_test(.clk(clk), .test(doutB3), .pat(adffn));
+    assert_dff dffe_test(.clk(clk), .test(doutB4), .pat(dffe));
+    
+endmodule

frontends/read_verilog_ff_edge/top.v

+module adff
+    ( input d, clk, clr, output reg q );
+    initial begin
+      q = 0;
+    end
+	always @( posedge clk, posedge clr )
+		if ( clr )
+`ifndef BUG        
+			q <= 1'b0;
+`else        
+			q <= d;
+`endif
+		else
+            q <= d;
+endmodule
+
+module adffn
+    ( input d, clk, clr, output reg q );
+    initial begin
+      q = 0;
+    end
+	always @( posedge clk, negedge clr )
+		if ( !clr )
+`ifndef BUG        
+			q <= 1'b0;
+`else        
+			q <= d;
+`endif
+		else
+            q <= d;
+endmodule
+
+module dffe
+    ( input d, clk, en, output reg q );
+    initial begin
+      q = 0;
+    end
+	always @( posedge clk )
+		if ( en )
+`ifndef BUG        
+			q <= d;
+`else        
+			q <= 1'b0;
+`endif
+endmodule
+
+module dffsr
+    ( input d, clk, pre, clr, output reg q );
+    initial begin
+      q = 0;
+    end
+	always @( posedge clk, posedge pre, posedge clr )
+		if ( clr )
+`ifndef BUG        
+			q <= 1'b0;
+`else        
+			q <= d;
+`endif
+		else if ( pre )
+			q <= 1'b1;
+		else
+            q <= d;
+endmodule
+
+module ndffnsnr
+    ( input d, clk, pre, clr, output reg q );
+    initial begin
+      q = 0;
+    end
+	always @( negedge clk, negedge pre, negedge clr )
+		if ( !clr )
+`ifndef BUG        
+			q <= 1'b0;
+`else        
+			q <= d;
+`endif
+		else if ( !pre )
+			q <= 1'b1;
+		else
+            q <= d;
+endmodule
+
+module top (
+input clk,
+input clr,
+input pre,
+input a,
+output b,b1,b2,b3,b4
+);
+
+dffsr u_dffsr (
+        .clk (clk ),
+        .clr (clr),
+        .pre (pre),
+        .d (a ),
+        .q (b )
+    );
+    
+ndffnsnr u_ndffnsnr (
+        .clk (clk ),
+        .clr (clr),
+        .pre (pre),
+        .d (a ),
+        .q (b1 )
+    );
+    
+adff u_adff (
+        .clk (clk ),
+        .clr (clr),
+        .d (a ),
+        .q (b2 )
+    );
+    
+adffn u_adffn (
+        .clk (clk ),
+        .clr (clr),
+        .d (a ),
+        .q (b3 )
+    );
+    
+dffe u_dffe (
+        .clk (clk ),
+        .en (clr),
+        .d (a ),
+        .q (b4 )
+    );
+
+endmodule

frontends/read_verilog_for_while/testbench.v

+module testbench;
+    reg clk;
+
+    initial begin
+        // $dumpfile("testbench.vcd");
+        // $dumpvars(0, testbench);
+
+        #5 clk = 0;
+        repeat (10000) begin
+            #5 clk = 1;
+            #5 clk = 0;
+        end
+
+        $display("OKAY");    
+    end
+   
+    
+    reg [15:0] D = 1;
+    reg [3:0] S = 0;
+    wire M2,M4,M8,M16;
+
+    top uut (
+        .S (S ),
+        .D (D ),
+        .M2 (M2 ),
+        .M4 (M4 ),
+        .M8 (M8 ),
+        .M16 (M16 )
+    );
+    
+    always @(posedge clk) begin
+    //#3;
+	D <= {D[14:0],D[15]};
+    //D <= D <<< 1;
+    S <= S + 1;
+    end
+	
+	assert_tri m2_test(.en(clk), .A(D[0]|D[1]), .B(M2));
+	assert_tri m4_test(.en(clk), .A(D[0]|D[1]|D[2]|D[3]), .B(M4));
+	assert_tri m8_test(.en(clk), .A(!S[3]), .B(M8));
+	assert_tri m16_test(.en(clk), .A(1'b1), .B(M16));
+  
+endmodule

frontends/read_verilog_for_while/top.v

+module mux2 (S,A,B,Y);
+    input S;
+    input A,B;
+    output reg Y;
+`ifndef BUG
+
+    always @(*)
+		Y = (S)? B : A;
+`else
+
+    always @(*)
+		Y = (~S)? B : A;
+`endif
+endmodule
+
+module mux4 ( S, D, Y );
+
+input[1:0] S;
+input[3:0] D;
+output Y;
+
+reg Y;
+wire[1:0] S;
+wire[3:0] D;
+
+reg i;
+
+function integer log2;
+  input integer value;
+  begin
+    value = value-1;
+    for (log2=0; value>0; log2=log2+1)
+		while (1)
+      value = value>>1;
+
+      repeat(10)
+      begin
+      end
+  end
+endfunction
+
+always @*
+begin
+    case( S )
+       0 : Y = D[0];
+       1 : Y = D[1];
+`ifndef BUG
+       2 : Y = D[2];
+`else
+       2 : Y = D[3];
+`endif
+       3 : Y = D[3];
+   endcase
+end
+
+endmodule
+
+module mux8 ( S, D, Y );
+
+input[2:0] S;
+input[7:0] D;
+output Y;
+
+reg Y;
+wire[2:0] S;
+wire[7:0] D;
+
+always @*
+begin
+
+   case( S )
+       0 : Y = D[0];
+       1 : Y = D[1];
+       2 : Y = D[2];
+       3 : Y = D[3];
+`ifndef BUG
+       4 : Y = D[4];
+`else
+       4 : Y = D[7];
+`endif
+       5 : Y = D[5];
+       6 : Y = D[6];
+       7 : Y = D[7];
+   endcase
+end
+
+endmodule
+
+module mux16 (D, S, Y);
+ 	input  [15:0] D;
+ 	input  [3:0] S;
+ 	output Y;
+
+assign Y = D[S];
+
+endmodule
+
+
+module top (
+input [3:0] S,
+input [15:0] D,
+output M2,M4,M8,M16
+);
+
+mux2 u_mux2 (
+        .S (S[0]),
+        .A (D[0]),
+        .B (D[1]),
+        .Y (M2)
+    );
+
+
+mux4 u_mux4 (
+        .S (S[1:0]),
+        .D (D[3:0]),
+        .Y (M4)
+    );
+
+mux8 u_mux8 (
+        .S (S[2:0]),
+        .D (D[7:0]),
+        .Y (M8)
+    );
+
+mux16 u_mux16 (
+        .S (S[3:0]),
+        .D (D[15:0]),
+        .Y (M16)
+    );
+
+
+endmodule

frontends/read_verilog_fsm/testbench.v

+module testbench;
+    reg clk;
+
+    initial begin
+        // $dumpfile("testbench.vcd");
+        // $dumpvars(0, testbench);
+
+        #5 clk = 0;
+        repeat (10000) begin
+            #5 clk = 1;
+            #5 clk = 0;
+        end
+
+        $display("OKAY");    
+    end
+   
+    
+    reg a = 0;
+    reg b = 0;
+    reg rst;    
+    reg en;
+    wire s;
+    wire bs;
+    wire f;
+    
+    top uut ( .clk(clk),
+              .rst(rst), 
+              .en(en), 
+              .a(a), 
+              .b(b), 
+              .s(s), 
+              .bs(bs), 
+              .f(f));
+              
+    always @(posedge clk)
+    begin
+        #2
+        a <= ~a;
+    end
+    
+    always @(posedge clk)
+    begin
+        #4
+        b <= ~b;
+    end
+    
+    initial begin
+        en <= 1;
+        rst <= 1;
+        #5
+        rst <= 0;
+    end
+    
+    
+    assert_expr s_test(.clk(clk), .A(s));
+	assert_expr bs_test(.clk(clk), .A(bs));
+	assert_expr f_test(.clk(clk), .A(f));
+  
+endmodule
+
+
+module assert_expr(input clk, input A);
+    always @(posedge clk)
+    begin
+        //#1;
+        if (A == 1'bZ)
+        begin
+            $display("ERROR: ASSERTION FAILED in %m:",$time," ",A);
+            $stop;
+        end
+    end
+endmodule

frontends/read_verilog_fsm/top.v

+module FSM ( clk,rst, en, ls, rs, stop, busy, finish);
+	input wire clk;
+	input wire rst;
+	input wire en;
+	input wire ls;
+	input wire rs;
+
+	output wire stop;
+	output wire busy;
+	output wire finish;
+	
+    parameter S0 = 4'b0000, S1 = 4'b0001, S2 = 4'b0010, S3 = 4'b0011, S4 = 4'b0100, S5 = 4'b0101, S6 = 4'b0110, S7 = 4'b0111, S8 = 4'b1000, S9 = 4'b1001, S10 = 4'b1010, S11 = 4'b1011, S12 = 4'b1100, S13 = 4'b1101, S14 = 4'b1110;
+	
+	reg [3:0] ns, st;
+
+	reg [2:0] count;
+
+
+	always @(posedge clk)
+	begin : CurrstProc
+		if (rst)
+			st <= S0;
+		else
+			st <= ns;
+	end
+
+	always @*
+	begin : NextstProc
+		ns = st;
+		case (st)
+			S0: ns = S1;
+			S1: ns = S2;
+			S2:
+				if (rs == 1'b1)
+					ns = S3;
+				else
+					ns = S4;
+			S3: ns = S1;
+			S4: if (count > 7)
+					ns = S10;
+				else
+					ns = S5;
+			S5: if (ls == 1'b0)
+					ns = S6;
+				else
+					ns = S3;
+			S6:
+				if (ls == 1'b1)
+					ns = S7;
+				else
+					ns = S8;
+			S7:
+				if (ls == 1'b1 && rs == 1'b1)
+					ns = S5;
+				else
+					ns = S13;
+			S8: ns = S9;
+			S9: ns = S8;
+			S10:
+				if (ls == 1'b1 || rs == 1'b1)
+					ns = S11;
+				else
+					ns = S4;
+			S11: ns = S12;
+			S12: ns = S10;
+			S13: ;
+			default: ns = S0;
+		endcase;
+	end
+	
+	always @(posedge clk)
+		if(~rst)
+			count <= 0;
+		else
+		begin
+			if(st == S4)
+				if (count > 7)
+					count <= 0;
+				else
+					count <= count + 1;
+		end
+
+	//FSM outputs (combinatorial)
+
+	assign stop   = (st == S3 || st == S12) ? 1'b1 : 1'b0;
+
+	assign finish = (st == S13) ? 1'b1 : 1'b0;
+
+	assign busy   = (st == S8 || st == S9) ? 1'b1 : 1'b0;
+
+endmodule
+
+
+module top (
+input clk,
+input rst,
+input en,
+input a,
+input b,
+output s,
+output bs,
+output f
+);
+
+FSM u_FSM ( .clk(clk),
+            .rst(rst), 
+            .en(en), 
+            .ls(a), 
+            .rs(b), 
+            .stop(s), 
+            .busy(bs), 
+            .finish(f));
+
+endmodule

frontends/read_verilog_generate/testbench.v

+module testbench;
+    reg clk;
+
+    initial begin
+        // $dumpfile("testbench.vcd");
+        // $dumpvars(0, testbench);
+
+        #5 clk = 0;
+        repeat (10000) begin
+            #5 clk = 1;
+            #5 clk = 0;
+        end
+
+        $display("OKAY");    
+    end
+   
+    
+    reg [15:0] D = 1;
+    reg [3:0] S = 0;
+    wire M2,M4,M8,M16;
+
+    top uut (
+        .S (S ),
+        .D (D ),
+        .M2 (M2 ),
+        .M4 (M4 ),
+        .M8 (M8 ),
+        .M16 (M16 )
+    );
+    
+    always @(posedge clk) begin
+    //#3;
+	D <= {D[14:0],D[15]};
+    //D <= D <<< 1;
+    S <= S + 1;
+    end
+	
+	assert_tri m2_test(.en(clk), .A(D[0]|D[1]), .B(M2));
+	assert_tri m4_test(.en(clk), .A(D[0]|D[1]|D[2]|D[3]), .B(M4));
+	assert_tri m8_test(.en(clk), .A(!S[3]), .B(M8));
+	assert_tri m16_test(.en(clk), .A(1'b1), .B(M16));
+  
+endmodule

frontends/read_verilog_generate/top.v

+module mux2 (S,A,B,Y);
+    input S;
+    input A,B;
+    output reg Y;
+`ifndef BUG
+
+    always @(*)
+		Y = (S)? B : A;
+`else
+
+    always @(*)
+		Y = (~S)? B : A;
+`endif
+endmodule
+
+module mux4 ( S, D, Y );
+
+input[1:0] S;
+input[3:0] D;
+output Y;
+
+reg Y;
+wire[1:0] S;
+wire[3:0] D;
+
+always @*
+begin
+    casez( S )
+       0 : Y = D[0];
+       1 : Y = D[1];
+`ifndef BUG
+       2 : Y = D[2];
+`else
+       2 : Y = D[3];
+`endif
+       3 : Y = D[3];
+   endcase
+end
+
+endmodule
+
+module mux8 ( S, D, Y );
+
+input[2:0] S;
+inout[7:0] D;
+output Y;
+
+reg Y;
+wire[2:0] S;
+wire[7:0] D;
+
+always @*
+begin
+   casex( S )
+       0 : Y = D[0];
+       1 : Y = D[1];
+       2 : Y = D[2];
+       3 : Y = D[3];
+`ifndef BUG
+       4 : Y = D[4];
+`else
+       4 : Y = D[7];
+`endif
+       5 : Y = D[5];
+       6 : Y = D[6];
+       7 : Y = D[7];
+   endcase
+end
+
+endmodule
+
+module mux16 (D, S, Y);
+ 	input  [15:0] D;
+ 	input  [3:0] S;
+ 	output Y;
+
+assign Y = D[S];
+
+endmodule
+
+
+module top (
+input [3:0] S,
+input [15:0] D,
+output M2,M4,M8,M16
+);
+parameter u = 0;
+
+mux2 u_mux2 (
+        .S (S[0]),
+        .A (D[0]),
+        .B (D[1]),
+        .Y (M2)
+    );
+
+
+mux4 u_mux4 (
+        .S (S[1:0]),
+        .D (D[3:0]),
+        .Y (M4)
+    );
+
+mux8 u_mux8 (
+        .S (S[2:0]),
+        .D (D[7:0]),
+        .Y (M8)
+    );
+
+mux16 u_mux16 (
+        .S (S[3:0]),
+        .D (D[15:0]),
+        .Y (M16)
+    );
+
+genvar index;
+generate
+for (index=0; index < 8; index=index+1)
+  begin: gen_code_label
+  end
+endgenerate
+
+genvar index;
+generate
+case( u )
+       0 : begin end
+       1 : begin end
+       2 : begin end
+       3 : begin end
+   endcase
+endgenerate
+
+// reg angle;
+// case (index)
+// //Create the case statement
+// 	1 :
+// 	begin
+//     generate
+//     genvar caseIndex;
+//         for (caseIndex = 0; caseIndex < 1024; caseIndex=caseIndex+1)
+//             begin
+//                 caseIndex: angle = 2*pi*caseIndex/1024;
+//             end
+//     endgenerate
+//     end
+// endcase
+
+endmodule

frontends/read_verilog_logic/testbench.v

+module testbench;
+    reg [2:0] in;
+
+	reg patt_out = 0;
+	reg patt_carry_out = 0;
+	reg patt_out1 = 0;
+	reg patt_carry_out1 = 0;
+	wire out;
+    wire carryout;
+
+    initial begin
+        // $dumpfile("testbench.vcd");
+        // $dumpvars(0, testbench);
+
+        #5 in = 0;
+        repeat (10000) begin
+            #5 in = in + 1;
+        end
+
+        $display("OKAY");
+    end
+
+    top uut (
+	.x(in[0]),
+	.y(in[1]),
+	.cin(in[2]),
+	.A(out),
+	.cout(carryout)
+	);
+
+    always @(posedge in[0]) begin
+    patt_out1 <=  ~in[1] + &in[2];
+    end
+    always @(negedge in[0]) begin
+        patt_carry_out1 <= in[2] ? |in[1] : patt_out;
+    end
+
+    always @(*) begin
+        if (in[0])
+            patt_out <=  patt_out|in[1]~&in[2];
+    end
+    always @(*) begin
+        if (~in[0])
+            patt_carry_out <=  patt_carry_out1&in[2]~|in[1];
+    end
+	assert_Z out_test(.A(out));
+
+endmodule

frontends/read_verilog_logic/top.v

+module top
+(
+ input x,
+ input y,
+ input cin,
+
+ output reg A,
+ output reg cout
+ );
+
+ reg A1,cout1,A2,cout2;
+
+ initial begin
+    A = 0;
+    cout = 0;
+ end
+
+`ifndef BUG
+always @(posedge x) begin
+    A1 <=  ~y + &cin;
+end
+always @(posedge x) begin
+    cout1 <= cin ? |y : ^A;
+end
+
+always @(posedge x) begin
+    A2 <=  ~y ^ cin;
+end
+always @(posedge x) begin
+    cout2 <= cin ? |y : ~^A;
+end
+
+always @(posedge x) begin
+        A <=  A1|y~&cin~^A1;
+end
+always @(posedge x) begin
+        cout <=  cout1&cin~|y;
+end
+`else
+assign {cout,A} =  1'bZ;
+`endif
+
+endmodule

frontends/read_verilog_logic/top_clean.v

+module top
+(
+ input x,
+ input y,
+ input cin,
+
+ output reg A,
+ output reg cout
+ );
+ 
+ initial begin
+    A = 0;
+    cout = 0;
+ end
+
+`ifndef BUG
+always @(posedge x) begin
+    A <=  y + cin;
+end
+always @(negedge x) begin
+    cout <=  y + A;
+end
+`else
+assign {cout,A} =  cin - y * x;
+`endif
+
+endmodule

frontends/read_verilog_mem/testbench.v

+module testbench;
+    reg clk;
+
+    initial begin
+        // $dumpfile("testbench.vcd");
+        // $dumpvars(0, testbench);
+
+        #5 clk = 0;
+        repeat (10000) begin
+            #5 clk = 1;
+            #5 clk = 0;
+        end
+
+        $display("OKAY");    
+    end
+   
+    
+    reg [7:0] data_a = 0;
+	reg [7:0] data_b = 0;
+	reg [5:0] addr_a = 0;	
+	reg [5:0] addr_b = 0;
+    reg we_a = 0;
+	reg we_b = 1;	
+    reg re_a = 1;
+	reg re_b = 1;
+	wire [7:0] q_a,q_b;
+	reg mem_init = 0;
+
+    top uut (
+    .data_a(data_a),
+	.data_b(data_b),
+	.addr_a(addr_a),
+	.addr_b(addr_b),
+	.we_a(we_a), 
+	.we_b(we_b), 	
+	.re_a(re_a), 
+	.re_b(re_b), 
+	.clk(clk),
+	.q_a(q_a), 
+	.q_b(q_b)
+    );
+    
+    always @(posedge clk) begin
+    #3;
+    data_a <= data_a + 17;	
+    data_b <= data_b + 5;
+	
+    addr_a <= addr_a + 1;	
+    addr_b <= addr_b + 1;
+    end
+    
+    always @(posedge addr_a) begin
+    #10;
+        if(addr_a > 6'h3E)
+            mem_init <= 1;
+    end
+	
+	always @(posedge clk) begin
+    //#3;
+    we_a <= !we_a; 
+    we_b <= !we_b; 
+    end
+	
+	uut_mem_checker port_a_test(.clk(clk), .init(mem_init), .en(!we_a), .A(q_a));
+    uut_mem_checker port_b_test(.clk(clk), .init(mem_init), .en(!we_b), .A(q_b));
+    
+endmodule
+
+module uut_mem_checker(input clk, input init, input en, input [7:0] A);
+    always @(posedge clk)
+    begin
+        #1;
+        if (en == 1 & init == 1 & A === 8'bXXXXXXXX)
+        begin
+            $display("ERROR: ASSERTION FAILED in %m:",$time," ",A);
+            $stop;
+        end
+    end
+endmodule

frontends/read_verilog_mem/top.v

+module top
+(
+	input [7:0] data_a, data_b,
+	input [6:1] addr_a, addr_b,
+	input we_a, we_b, re_a, re_b, clk,
+	output reg [7:0] q_a, q_b
+);
+	parameter WIDTH=8;
+	// Declare the RAM variable
+	reg [WIDTH-1:0] ram[63:0];
+
+	initial begin
+        q_a <= 8'h00;
+        q_b <= 8'd0;
+	end
+
+	// Port A
+	always @ (posedge clk)
+	begin
+`ifndef BUG
+		if (we_a)
+`else
+		if (we_b)
+`endif
+		begin
+			ram[addr_a] <= data_a;
+			q_a <= data_a;
+		end
+		if (re_b)
+		begin
+			q_a <= ram[addr_a];
+		end
+	end
+
+	// Port B
+	always @ (posedge clk)
+	begin
+`ifndef BUG
+		if (we_b)
+`else
+		if (we_a)
+`endif
+		begin
+			ram[addr_b] <= data_b;
+			q_b <= data_b;
+		end
+		if (re_b)
+		begin
+			q_b <= ram[addr_b];
+		end
+	end
+
+endmodule

frontends/read_verilog_param_defparam/testbench.v

+module testbench;
+    reg clk;
+
+    initial begin
+        // $dumpfile("testbench.vcd");
+        // $dumpvars(0, testbench);
+
+        #5 clk = 0;
+        repeat (10000) begin
+            #5 clk = 1;
+            #5 clk = 0;
+        end
+
+        $display("OKAY");    
+    end
+   
+    
+    reg [15:0] D = 1;
+    reg [3:0] S = 0;
+    wire M2,M4,M8,M16;
+
+    top uut (
+        .S (S ),
+        .D (D ),
+        .M2 (M2 ),
+        .M4 (M4 ),
+        .M8 (M8 ),
+        .M16 (M16 )
+    );
+    
+    always @(posedge clk) begin
+    //#3;
+	D <= {D[14:0],D[15]};
+    //D <= D <<< 1;
+    S <= S + 1;
+    end
+	
+	assert_tri m2_test(.en(clk), .A(D[0]|D[1]), .B(M2));
+	assert_tri m4_test(.en(clk), .A(D[0]|D[1]|D[2]|D[3]), .B(M4));
+	assert_tri m8_test(.en(clk), .A(!S[3]), .B(M8));
+	assert_tri m16_test(.en(clk), .A(1'b1), .B(M16));
+  
+endmodule

frontends/read_verilog_param_defparam/top.v

+module mux2 (S,A,B,Y);
+    input S;
+    input A,B;
+    output reg Y;
+`ifndef BUG
+
+    always @(*)
+		Y = (S)? B : A;
+`else
+
+    always @(*)
+		Y = (~S)? B : A;
+`endif
+endmodule
+
+module mux4 ( S, D, Y );
+
+input[1:0] S;
+input[3:0] D;
+output Y;
+
+reg Y;
+wire[1:0] S;
+wire[3:0] D;
+
+always @*
+begin
+    case( S )
+       0 : Y = D[0];
+       1 : Y = D[1];
+`ifndef BUG
+       2 : Y = D[2];
+`else
+       2 : Y = D[3];
+`endif
+       3 : Y = D[3];
+   endcase
+end
+
+endmodule
+
+module mux8 ( S, D, Y );
+
+input[2:0] S;
+input[7:0] D;
+output Y;
+
+reg Y;
+wire[2:0] S;
+wire[7:0] D;
+
+always @*
+begin
+   case( S )
+       0 : Y = D[0];
+       1 : Y = D[1];
+       2 : Y = D[2];
+       3 : Y = D[3];
+`ifndef BUG
+       4 : Y = D[4];
+`else
+       4 : Y = D[7];
+`endif
+       5 : Y = D[5];
+       6 : Y = D[6];
+       7 : Y = D[7];
+   endcase
+end
+
+endmodule
+
+module mux16 (D, S, Y);
+ 	input  [15:0] D;
+ 	input  [3:0] S;
+ 	output Y;
+
+parameter WIDTH = 8;
+parameter DEPTH = 64;
+parameter LOG2DEPTH = 6;
+
+localparam L = 6;
+
+assign Y = D[S];
+
+endmodule
+
+
+
+
+module top (
+input [3:0] S,
+input [15:0] D,
+output M2,M4,M8,M16
+);
+
+
+
+mux2 u_mux2 (
+        .S (S[0]),
+        .A (D[0]),
+        .B (D[1]),
+        .Y (M2)
+    );
+
+
+mux4 u_mux4 (
+        .S (S[1:0]),
+        .D (D[3:0]),
+        .Y (M4)
+    );
+
+mux8 u_mux8 (
+        .S (S[2:0]),
+        .D (D[7:0]),
+        .Y (M8)
+    );
+
+mux16 u_mux16 (
+        .S (S[3:0]),
+        .D (D[15:0]),
+        .Y (M16)
+    );
+
+defparam u_mux16.WIDTH = 32;
+defparam u_mux16.DEPTH = 64;
+defparam u_mux16.LOG2DEPTH = 2;
+
+endmodule

frontends/read_verilog_real_value_shift_concat/testbench.v

+module testbench;
+    reg clk;
+
+    initial begin
+        // $dumpfile("testbench.vcd");
+        // $dumpvars(0, testbench);
+
+        #5 clk = 0;
+        repeat (10000) begin
+            #5 clk = 1;
+            #5 clk = 0;
+        end
+
+        $display("OKAY");    
+    end
+   
+    
+    reg [15:0] D = 1;
+    reg [3:0] S = 0;
+    wire M2,M4,M8,M16;
+
+    top uut (
+        .S (S ),
+        .D (D ),
+        .M2 (M2 ),
+        .M4 (M4 ),
+        .M8 (M8 ),
+        .M16 (M16 )
+    );
+    
+    always @(posedge clk) begin
+    //#3;
+	D <= {D[14:0],D[15]};
+    //D <= D <<< 1;
+    S <= S + 1;
+    end
+	
+	assert_tri m2_test(.en(clk), .A(D[0]|D[1]), .B(M2));
+	assert_tri m4_test(.en(clk), .A(D[0]|D[1]|D[2]|D[3]), .B(M4));
+	assert_tri m8_test(.en(clk), .A(!S[3]), .B(M8));
+	assert_tri m16_test(.en(clk), .A(1'b1), .B(M16));
+  
+endmodule

frontends/read_verilog_real_value_shift_concat/top.v

+module mux2 (S,A,B,Y);
+    input S;
+    input A,B;
+    output reg Y;
+`ifndef BUG
+
+    always @(*)
+		Y = (S)? B : A;
+`else
+
+    always @(*)
+		Y = (~S)? B : A;
+`endif
+endmodule
+
+module mux4 ( S, D, Y );
+
+input[1:0] S;
+input[3:0] D;
+output Y;
+
+reg Y;
+wire[1:0] S;
+wire[3:0] D;
+
+always @*
+begin
+    case( S )
+       0 : Y = D[0];
+       1 : Y = D[1];
+`ifndef BUG
+       2 : Y = D[2];
+`else
+       2 : Y = D[3];
+`endif
+       3 : Y = D[3];
+   endcase
+end
+
+endmodule
+
+module mux8 ( S, D, Y );
+
+input[2:0] S;
+input[7:0] D;
+output Y;
+
+reg Y;
+wire[2:0] S;
+wire[7:0] D;
+
+always @*
+begin
+   case( S )
+       0 : Y = D[0];
+       1 : Y = D[1];
+       2 : Y = D[2];
+       3 : Y = D[3];
+`ifndef BUG
+       4 : Y = D[4];
+`else
+       4 : Y = D[7];
+`endif
+       5 : Y = D[5];
+       6 : Y = D[6];
+       7 : Y = D[7];
+   endcase
+end
+
+endmodule
+
+module mux16 (D, S, Y);
+ 	input  [15:0] D;
+ 	input  [3:0] S;
+ 	output Y;
+
+assign Y = D[S];
+
+endmodule
+
+
+module top (
+input [3:0] S,
+input [15:0] D,
+output M2,M4,M8,M16
+);
+
+mux2 u_mux2 (
+        .S (S[0]),
+        .A (D[0]),
+        .B (D[1]),
+        .Y (M2)
+    );
+
+
+mux4 u_mux4 (
+        .S (S[1:0]),
+        .D (D[3:0]),
+        .Y (M4)
+    );
+
+mux8 u_mux8 (
+        .S (S[2:0]),
+        .D (D[7:0]),
+        .Y (M8)
+    );
+
+mux16 u_mux16 (
+        .S (S[3:0]),
+        .D (D[15:0]),
+        .Y (M16)
+    );
+
+reg b,c = 1.01;
+wire a;
+
+
+endmodule
+
+module concatenation_operator();
+  reg [3:0]  r_VAL_1 = 4'b0111;
+  reg [3:0]  r_VAL_2 = 4'b1100;
+  wire [7:0] w_CAT;
+
+  reg  [3:0]       r_UNSIGNED = 4'b0010;
+  reg signed [3:0] r_SIGNED   = 4'b1110;
+  wire [7:0]       w_CAT_2;
+  wire [15:0]      w_CAT_3;
+
+  reg              r_CLOCK = 1'b0;
+  reg [7:0]        r_SHIFT_REG = 8'h01;
+
+  // Demonstrates a common concatenation.
+  assign w_CAT = {r_VAL_1, r_VAL_2};
+
+  // Demonstrates concatenation of different types
+  assign w_CAT_2 = {r_SIGNED, r_UNSIGNED};
+
+  // Demonstrates Verilog padding upper bits with 0.
+  assign w_CAT_3 = {r_VAL_1, r_VAL_2};
+
+  // Generate a clock to drive shift register below
+  always #1 r_CLOCK = !r_CLOCK;
+
+  // Demonstrate Shifting of a 1 through an 8 bit register.
+  always @(posedge r_CLOCK)
+    begin
+      r_SHIFT_REG[7:0] <= {r_SHIFT_REG[6:0], r_SHIFT_REG[7]};
+    end
+
+endmodule // concatenation_operator
+
+module replication_operator();
+  reg [3:0]  r_VAL_1 = 4'b0111;
+
+  parameter c_MULTIPLIER = 4'b0010;
+
+  parameter WIDTH = 1;
+wire [WIDTH-1:0] connection;
+
+generate
+  if (WIDTH > 1) begin
+    assign connection = { {WIDTH-1{1'b0}}, 1'b1 };
+  end
+  else begin
+    assign connection = 1'b1 ;
+  end
+endgenerate
+
+
+endmodule // replication_operator
+
+module Shift (A, Y1, Y2);
+
+
+
+                 input [7:0] A;
+
+                 output [7:0] Y1, Y2;
+
+                 parameter B=3; reg [7:0] Y1, Y2;
+
+
+
+                 always @(A)
+
+                 begin
+
+                                  Y1=A<<B; //logical shift left
+
+                                  Y2=A>>B; //logical shift right
+
+                 end
+
+endmodule
+
+module SShift (A, Y1, Y2);
+
+
+
+                 input [7:0] A;
+
+                 output [7:0] Y1, Y2;
+
+                 parameter B=3; reg [7:0] Y1, Y2;
+
+
+
+                 always @(A)
+
+                 begin
+
+                                  Y1=A<<<B; //logical shift left
+
+                                  Y2=A>>>B; //logical shift right
+
+                 end
+
+endmodule

frontends/read_verilog_real_value_shift_concat/top1.v

+module mux2 (S,A,B,Y);
+    input S;
+    input A,B;
+    output reg Y;
+    always @(*)
+		Y = (S)? B : A;
+endmodule
+
+module mux4 ( S, D, Y );
+
+input[1:0] S;
+input[3:0] D;
+output Y;
+
+reg Y;
+wire[1:0] S;
+wire[3:0] D;
+
+always @*
+begin
+    case( S )
+       0 : Y = D[0];
+       1 : Y = D[1];
+       2 : Y = D[2];
+       3 : Y = D[3];
+   endcase
+end
+
+endmodule
+
+module mux8 ( S, D, Y );
+
+input[2:0] S;
+input[7:0] D;
+output Y;
+
+reg Y;
+wire[2:0] S;
+wire[7:0] D;
+
+always @*
+begin
+   case( S )
+       0 : Y = D[0];
+       1 : Y = D[1];
+       2 : Y = D[2];
+       3 : Y = D[3];
+       4 : Y = D[4];
+       5 : Y = D[5];
+       6 : Y = D[6];
+       7 : Y = D[7];
+   endcase
+end
+
+endmodule
+
+module mux16 (D, S, Y);
+ 	input  [15:0] D;
+ 	input  [3:0] S;
+ 	output Y;
+
+assign Y = D[S];
+
+endmodule
+
+
+module top (
+input [3:0] S,
+input [15:0] D,
+output M2,M4,M8,M16
+);
+
+mux2 u_mux2 (
+        .S (S[0]),
+        .A (D[0]),
+        .B (D[1]),
+        .Y (M2)
+    );
+
+
+mux4 u_mux4 (
+        .S (S[1:0]),
+        .D (D[3:0]),
+        .Y (M4)
+    );
+
+mux8 u_mux8 (
+        .S (S[2:0]),
+        .D (D[7:0]),
+        .Y (M8)
+    );
+
+mux16 u_mux16 (
+        .S (S[3:0]),
+        .D (D[15:0]),
+        .Y (M16)
+    );
+
+endmodule

frontends/read_verilog_string/testbench.v

+module testbench;
+    reg clk;
+
+    initial begin
+        // $dumpfile("testbench.vcd");
+        // $dumpvars(0, testbench);
+
+        #5 clk = 0;
+        repeat (10000) begin
+            #5 clk = 1;
+            #5 clk = 0;
+        end
+
+        $display("OKAY");    
+    end
+   
+    
+    reg [15:0] D = 1;
+    reg [3:0] S = 0;
+    wire M2,M4,M8,M16;
+
+    top uut (
+        .S (S ),
+        .D (D ),
+        .M2 (M2 ),
+        .M4 (M4 ),
+        .M8 (M8 ),
+        .M16 (M16 )
+    );
+    
+    always @(posedge clk) begin
+    //#3;
+	D <= {D[14:0],D[15]};
+    //D <= D <<< 1;
+    S <= S + 1;
+    end
+	
+	assert_tri m2_test(.en(clk), .A(D[0]|D[1]), .B(M2));
+	assert_tri m4_test(.en(clk), .A(D[0]|D[1]|D[2]|D[3]), .B(M4));
+	assert_tri m8_test(.en(clk), .A(!S[3]), .B(M8));
+	assert_tri m16_test(.en(clk), .A(1'b1), .B(M16));
+  
+endmodule

frontends/read_verilog_string/top.v

+module mux2 (S,A,B,Y);
+    input S;
+    input A,B;
+    output reg Y;
+`ifndef BUG
+
+    always @(*)
+		Y = (S)? B : A;
+`else
+
+    always @(*)
+		Y = (~S)? B : A;
+`endif
+endmodule
+
+module mux4 ( S, D, Y );
+
+input[1:0] S;
+input[3:0] D;
+output Y;
+
+reg Y;
+wire[1:0] S;
+wire[3:0] D;
+
+always @*
+begin
+    case( S )
+       0 : Y = D[0];
+       1 : Y = D[1];
+`ifndef BUG
+       2 : Y = D[2];
+`else
+       2 : Y = D[3];
+`endif
+       3 : Y = D[3];
+   endcase
+end
+
+endmodule
+
+module mux8 ( S, D, Y );
+
+input[2:0] S;
+input[7:0] D;
+output Y;
+
+reg Y;
+wire[2:0] S;
+wire[7:0] D;
+
+always @*
+begin
+   case( S )
+       0 : Y = D[0];
+       1 : Y = D[1];
+       2 : Y = D[2];
+       3 : Y = D[3];
+`ifndef BUG
+       4 : Y = D[4];
+`else
+       4 : Y = D[7];
+`endif
+       5 : Y = D[5];
+       6 : Y = D[6];
+       7 : Y = D[7];
+   endcase
+end
+
+endmodule
+
+module mux16 (D, S, Y);
+ 	input  [15:0] D;
+ 	input  [3:0] S;
+ 	output Y;
+
+assign Y = D[S];
+
+endmodule
+
+
+module top (
+input [3:0] S,
+input [15:0] D,
+output M2,M4,M8,M16
+);
+
+parameter FILE_OUT= "\"file1.txt\"";
+reg [8*10:1]        stringvar;
+reg [7:0] q;
+
+initial begin
+stringvar="Starting";
+q <= '1;
+end
+
+mux2 u_mux2 (
+        .S (S[0]),
+        .A (D[0]),
+        .B (D[1]),
+        .Y (M2)
+    );
+
+
+mux4 u_mux4 (
+        .S (S[1:0]),
+        .D (D[3:0]),
+        .Y (M4)
+    );
+
+mux8 u_mux8 (
+        .S (S[2:0]),
+        .D (D[7:0]),
+        .Y (M8)
+    );
+
+mux16 u_mux16 (
+        .S (S[3:0]),
+        .D (D[15:0]),
+        .Y (M16)
+    );
+
+endmodule

frontends/read_verilog_string/top1.v

+module mux2 (S,A,B,Y);
+    input S;
+    input A,B;
+    output reg Y;
+    always @(*)
+		Y = (S)? B : A;
+endmodule
+
+module mux4 ( S, D, Y );
+
+input[1:0] S;
+input[3:0] D;
+output Y;
+
+reg Y;
+wire[1:0] S;
+wire[3:0] D;
+
+always @*
+begin
+    case( S )
+       0 : Y = D[0];
+       1 : Y = D[1];
+       2 : Y = D[2];
+       3 : Y = D[3];
+   endcase
+end
+
+endmodule
+
+module mux8 ( S, D, Y );
+
+input[2:0] S;
+input[7:0] D;
+output Y;
+
+reg Y;
+wire[2:0] S;
+wire[7:0] D;
+
+always @*
+begin
+   case( S )
+       0 : Y = D[0];
+       1 : Y = D[1];
+       2 : Y = D[2];
+       3 : Y = D[3];
+       4 : Y = D[4];
+       5 : Y = D[5];
+       6 : Y = D[6];
+       7 : Y = D[7];
+   endcase
+end
+
+endmodule
+
+module mux16 (D, S, Y);
+ 	input  [15:0] D;
+ 	input  [3:0] S;
+ 	output Y;
+
+assign Y = D[S];
+
+endmodule
+
+
+module top (
+input [3:0] S,
+input [15:0] D,
+output M2,M4,M8,M16
+);
+
+mux2 u_mux2 (
+        .S (S[0]),
+        .A (D[0]),
+        .B (D[1]),
+        .Y (M2)
+    );
+
+
+mux4 u_mux4 (
+        .S (S[1:0]),
+        .D (D[3:0]),
+        .Y (M4)
+    );
+
+mux8 u_mux8 (
+        .S (S[2:0]),
+        .D (D[7:0]),
+        .Y (M8)
+    );
+
+mux16 u_mux16 (
+        .S (S[3:0]),
+        .D (D[15:0]),
+        .Y (M16)
+    );
+
+endmodule

frontends/read_verilog_task_func/testbench.v

+module testbench;
+    reg clk;
+
+    initial begin
+        // $dumpfile("testbench.vcd");
+        // $dumpvars(0, testbench);
+
+        #5 clk = 0;
+        repeat (10000) begin
+            #5 clk = 1;
+            #5 clk = 0;
+        end
+
+        $display("OKAY");    
+    end
+   
+    
+    reg [15:0] D = 1;
+    reg [3:0] S = 0;
+    wire M2,M4,M8,M16;
+
+    top uut (
+        .S (S ),
+        .D (D ),
+        .M2 (M2 ),
+        .M4 (M4 ),
+        .M8 (M8 ),
+        .M16 (M16 )
+    );
+    
+    always @(posedge clk) begin
+    //#3;
+	D <= {D[14:0],D[15]};
+    //D <= D <<< 1;
+    S <= S + 1;
+    end
+	
+	assert_tri m2_test(.en(clk), .A(D[0]|D[1]), .B(M2));
+	assert_tri m4_test(.en(clk), .A(D[0]|D[1]|D[2]|D[3]), .B(M4));
+	assert_tri m8_test(.en(clk), .A(!S[3]), .B(M8));
+	assert_tri m16_test(.en(clk), .A(1'b1), .B(M16));
+  
+endmodule

frontends/read_verilog_task_func/top.v

+module mux2 (S,A,B,Y);
+    input S;
+    input A,B;
+    output reg Y;
+`ifndef BUG
+
+    always @(*)
+		Y = (S)? B : A;
+`else
+
+    always @(*)
+		Y = (~S)? B : A;
+`endif
+endmodule
+
+module mux4 ( S, D, Y );
+
+input[1:0] S;
+input[3:0] D;
+output Y;
+
+reg Y;
+wire[1:0] S;
+wire[3:0] D;
+
+always @*
+begin
+    case( S )
+       0 : Y = D[0];
+       1 : Y = D[1];
+`ifndef BUG
+       2 : Y = D[2];
+`else
+       2 : Y = D[3];
+`endif
+       3 : Y = D[3];
+   endcase
+end
+
+endmodule
+
+module mux8 ( S, D, Y );
+
+input[2:0] S;
+input[7:0] D;
+output Y;
+
+reg Y;
+wire[2:0] S;
+wire[7:0] D;
+
+always @*
+begin
+   case( S )
+       0 : Y = D[0];
+       1 : Y = D[1];
+       2 : Y = D[2];
+       3 : Y = D[3];
+`ifndef BUG
+       4 : Y = D[4];
+`else
+       4 : Y = D[7];
+`endif
+       5 : Y = D[5];
+       6 : Y = D[6];
+       7 : Y = D[7];
+   endcase
+end
+
+endmodule
+
+module mux16 (D, S, Y);
+ 	input  [15:0] D;
+ 	input  [3:0] S;
+ 	output Y;
+
+assign Y = D[S];
+
+endmodule
+
+
+module top (
+input [3:0] S,
+input [15:0] D,
+output M2,M4,M8,M16
+);
+
+wire [7:0] temp_a,temp_b;
+wire e;
+
+task convert;
+input [7:0] temp_in;
+output [7:0] temp_out;
+begin
+   temp_out = (9/5) *( temp_in + 32);
+ end
+endtask
+
+function  myfunction;
+input a, b, c, d;
+ begin
+   myfunction = ((a+b) + (c-d));
+ end
+endfunction
+
+always @ (temp_a)
+begin
+   convert (temp_a, temp_b);
+end
+assign e = myfunction (a,b,c,d);
+
+mux2 u_mux2 (
+        .S (S[0]),
+        .A (D[0]),
+        .B (D[1]),
+        .Y (M2)
+    );
+
+
+mux4 u_mux4 (
+        .S (S[1:0]),
+        .D (D[3:0]),
+        .Y (M4)
+    );
+
+mux8 u_mux8 (
+        .S (S[2:0]),
+        .D (D[7:0]),
+        .Y (M8)
+    );
+
+mux16 u_mux16 (
+        .S (S[3:0]),
+        .D (D[15:0]),
+        .Y (M16)
+    );
+
+endmodule

frontends/scripts/read_ilang_lib.ys

+read_verilog ../top.v
+proc
+memory
+dump -o file.il
+write_ilang ilang.ilang
+design -reset
+read_ilang -lib ilang.ilang
+read_ilang ilang.ilang
+dump -n -o file1.il
+write_verilog synth.v

frontends/scripts/read_ilang_nooverwrite.ys

+read_verilog ../top.v
+proc
+memory
+dump -o file.il
+write_ilang ilang.ilang
+design -reset
+read_ilang -nooverwrite ilang.ilang
+dump -n -o file1.il
+write_verilog synth.v

frontends/scripts/read_ilang_overwrite.ys

+read_verilog ../top.v
+proc
+memory
+dump -o file.il
+write_ilang ilang.ilang
+design -reset
+read_ilang -overwrite ilang.ilang
+dump -n -o file1.il
+write_verilog synth.v

frontends/scripts/read_verilog_assert.ys

+read_verilog -sv ../top.v
+synth -top top
+write_verilog synth.v
+design -reset
+read_verilog -sv ../top_clean.v
+synth -top top
+write_verilog synth.v

frontends/scripts/read_verilog_assert_ast1.ys

+read_verilog -sv -dump_ast1 ../top.v
+synth -top top
+write_verilog synth.v
+design -reset
+read_verilog -sv ../top_clean.v
+synth -top top
+write_verilog synth.v

frontends/scripts/read_verilog_assert_ast2.ys

+read_verilog -sv -dump_ast2 ../top.v
+synth -top top
+write_verilog synth.v
+design -reset
+read_verilog -sv ../top_clean.v
+synth -top top
+write_verilog synth.v

frontends/scripts/read_verilog_specify.ys

+read_verilog -specify ../top.v
+synth -top top
+write_verilog synth.v

frontends/scripts/read_verilog_sv_ast1.ys

+read_verilog -sv  -dump_ast1 ../top.v
+synth -top top
+write_verilog synth.v

frontends/scripts/read_verilog_sv_ast2.ys

+read_verilog -sv  -dump_ast2 ../top.v
+synth -top top
+write_verilog synth.v

misc/Makefile

@@ -231,4 +231,16 @@ $(eval $(call template,pmuxtree, pmuxtree))
 #opt_rmdff_sat
 $(eval $(call template,opt_rmdff_sat, opt_rmdff_sat))
 
+#wbflip
+$(eval $(call template,wbflip, wbflip wbflip_top))
+
+#pmux2shiftx
+$(eval $(call template,pmux2shiftx, pmux2shiftx_norange pmux2shiftx_onehot_shiftx pmux2shiftx_onehot_pmux pmux2shiftx_onehot_ignore pmux2shiftx_min_choices_0 pmux2shiftx_min_choices_3000 pmux2shiftx_min_dens_3000 pmux2shiftx_min_dens_0 pmux2shiftx_vv pmux2shiftx_v pmux2shiftx_top pmux2shiftx ))
+$(eval $(call template,pmux2shiftx_2, pmux2shiftx_norange pmux2shiftx_onehot_shiftx pmux2shiftx_onehot_pmux pmux2shiftx_onehot_ignore pmux2shiftx_min_choices_0 pmux2shiftx_min_choices_3000 pmux2shiftx_min_dens_3000 pmux2shiftx_min_dens_0 pmux2shiftx_vv pmux2shiftx_v pmux2shiftx_top pmux2shiftx ))
+$(eval $(call template,pmux2shiftx_fsm, pmux2shiftx_norange pmux2shiftx_onehot_shiftx pmux2shiftx_onehot_pmux pmux2shiftx_onehot_ignore pmux2shiftx_min_choices_0 pmux2shiftx_min_choices_3000 pmux2shiftx_min_dens_3000 pmux2shiftx_min_dens_0 pmux2shiftx_vv pmux2shiftx_v pmux2shiftx_top pmux2shiftx ))
+
+#onehot
+$(eval $(call template,onehot, onehot onehot_v onehot_vv ))
+
+
 .PHONY: all clean

misc/onehot/top.v

+module top(C, S, Y);
+input C;
+input [1:0] S;
+output reg [3:0] Y;
+
+initial Y = 0;
+
+always @(posedge C) begin
+        case (S)
+                2'b00: Y <= 4'b0001;
+                2'b01: Y <= 4'b0010;
+                2'b10: Y <= 4'b0100;
+                2'b11: Y <= 4'b1000;
+        endcase
+end
+
+endmodule

misc/pmux2shiftx/top.v

+module top(C, S, Y);
+input C;
+input [1:0] S;
+output reg [3:0] Y;
+
+initial Y = 0;
+
+always @(posedge C) begin
+        case (S)
+                2'b00: Y <= 4'b0001;
+                2'b01: Y <= 4'b0010;
+                2'b10: Y <= 4'b0100;
+                2'b11: Y <= 4'b1000;
+        endcase
+end
+
+endmodule

misc/pmux2shiftx_2/top.v

+module top(input [7:0] i, output o);
+always @*
+case (i[6:3])
+    4: o <= i[0];
+    3: o <= i[2];
+    7: o <= i[3];
+    default: o <= 1'b0;
+endcase
+endmodule

misc/pmux2shiftx_fsm/top.v

+ module fsm (
+ clock,
+ reset,
+ req_0,
+ req_1,
+ gnt_0,
+ gnt_1      
+ );
+ input   clock,reset,req_0,req_1;
+ output  gnt_0,gnt_1;
+ wire    clock,reset,req_0,req_1;
+ reg     gnt_0,gnt_1;
+ 
+ parameter SIZE = 3           ;
+ parameter IDLE  = 3'b001,GNT0 = 3'b010,GNT1 = 3'b100,GNT2 = 3'b101 ;
+ 
+ reg [SIZE-1:0] state;
+ reg [SIZE-1:0] next_state;
+ 
+ always @ (posedge clock)
+ begin : FSM
+ if (reset == 1'b1) begin
+   state <=  #1  IDLE;
+   gnt_0 <= 0;
+   gnt_1 <= 0;
+ end else
+  case(state)
+    IDLE : if (req_0 == 1'b1) begin
+                 state <=  #1  GNT0;
+`ifndef BUG        
+                 gnt_0 <= 1;
+`else
+                 gnt_0 <= 1'bZ;
+`endif
+               end else if (req_1 == 1'b1) begin
+                 gnt_1 <= 1;
+                 state <=  #1  GNT0;
+               end else begin
+                 state <=  #1  IDLE;
+               end
+    GNT0 : if (req_0 == 1'b1) begin
+                 state <=  #1  GNT0;
+               end else begin
+                 gnt_0 <= 0;
+                 state <=  #1  IDLE;
+               end
+    GNT1 : if (req_1 == 1'b1) begin
+                 state <=  #1  GNT2;
+				 gnt_1 <= req_0;
+               end
+    GNT2 : if (req_0 == 1'b1) begin
+                 state <=  #1  GNT1;
+				 gnt_1 <= req_1;
+               end 
+    default : state <=  #1  IDLE;
+ endcase
+ end
+ 
+ endmodule
+ 
+ module top (
+input clk,
+input rst,
+input a,
+input b,
+output g0,
+output g1
+);
+
+fsm u_fsm ( .clock(clk),
+            .reset(rst), 
+            .req_0(a), 
+            .req_1(b), 
+            .gnt_0(g0), 
+            .gnt_1(g1));
+
+endmodule

misc/run.sh

@@ -514,6 +514,12 @@ else
 	elif [ "$2" = "pmuxtree" ]; then
 		expected_string="cell \$pmux"
 		expected="0"
+	elif [ "$1" = "pmux2shiftx" ]; then
+		if [ "$2" = "pmux2shiftx_min_choices_3000" ] || \
+		   [ "$2" = "pmux2shiftx_min_dens_3000" ]; then
+		   expected="0"
+		fi
+		expected_string="cell \$shiftx"
 	elif [ "$1" = "qwp" ]; then
 		expected_string="attribute \\\qwp_position"
 	elif [ "$2" = "rename" ]; then

misc/scripts/onehot.ys

+read_verilog ../top.v
+proc
+pmux2shiftx
+onehot
+tee -o result.log dump

misc/scripts/onehot_v.ys

+read_verilog ../top.v
+proc
+pmux2shiftx
+onehot -v
+tee -o result.log dump

misc/scripts/onehot_vv.ys

+read_verilog ../top.v
+proc
+pmux2shiftx
+onehot -vv
+tee -o result.log dump

misc/scripts/pmux2shiftx.ys

+read_verilog ../top.v
+proc
+pmux2shiftx
+tee -o result.log dump

misc/scripts/pmux2shiftx_min_choices_0.ys

+read_verilog ../top.v
+proc
+pmux2shiftx -min_choices 0
+onehot
+tee -o result.log dump

misc/scripts/pmux2shiftx_min_choices_3000.ys

+read_verilog ../top.v
+proc
+pmux2shiftx -min_choices 3000
+tee -o result.log dump

misc/scripts/pmux2shiftx_min_dens_0.ys

+read_verilog ../top.v
+proc
+pmux2shiftx -min_density 0
+onehot
+tee -o result.log dump

misc/scripts/pmux2shiftx_min_dens_3000.ys

+read_verilog ../top.v
+proc
+pmux2shiftx -min_density 3000
+tee -o result.log dump

misc/scripts/pmux2shiftx_norange.ys

+read_verilog ../top.v
+proc
+pmux2shiftx -norange
+onehot
+tee -o result.log dump

misc/scripts/pmux2shiftx_onehot_ignore.ys

+read_verilog ../top.v
+proc
+pmux2shiftx -onehot ignore
+onehot
+tee -o result.log dump