Commit 05c2477c by SergeyDegtyar

Review 'misc' test group (abc - eval)

parent c0b775eb
*/work_*/
/.stamp
/run-test.mk
PYTHON_EXECUTABLE := $(shell if python3 -c ""; then echo "python3"; else echo "python"; fi)
all::
run-test.mk: ../generate.py
@$(PYTHON_EXECUTABLE) ../generate.py > run-test.mk
include run-test.mk
.PHONY: all clean
read_verilog ../top.v
proc
dff2dffe
synth -top top
abc
select -assert-count 3 t:$_NAND_
select -assert-count 2 t:$_XOR_
select -assert-none t:$_NAND_ t:$_XOR_ %% t:* %D
read_verilog ../top.v
proc
dff2dffe
synth -top top
tee -o result.out abc -D 2
read_verilog ../top.v
synth -top top
tee -o result.log abc -S 2
ERROR: Can't open ABC output file
read_verilog ../top.v
synth -top top
tee -o result.out abc -liberty -constr
abc -liberty -constr
read_verilog ../top.v
synth -top top
tee -o result.out abc -dff -clk u
abc -dff -clk u
read_verilog ../top.v
synth -top top
tee -o result.out abc -liberty -constr top.lib
ERROR: Got -constr but no -liberty!
read_verilog ../top.v
synth -top top
tee -o result.out abc -constr -liberty
abc -constr -liberty
read_verilog ../top_dff.v
synth -top top
dff2dffe
tee -o result.log abc -dff
abc -dff
read_verilog ../top_dff.v
synth -top top
tee -o result.log abc -keepff
abc -dff
read_verilog ../top_div_mul.v
proc
dff2dffe
synth -top top
tee -o result.out abc
read_verilog ../top_dff.v
proc
dff2dffe
synth -top top
tee -o result.out abc
read_verilog ../top_dff.v
proc
dff2dffe
synth -top top
tee -o result.out abc -clk clk
read_verilog ../top_fsm.v
synth -top top
tee -o result.out abc
read_verilog ../top_fsm.v
synth -top top
tee -o result.out abc -g all
read_verilog ../top_fsm.v
synth -top top
tee -o result.out abc -g all
read_verilog ../top_fsm.v
synth -top top
abc -g cmos4
select -assert-count 6 t:$_AOI3_
select -assert-count 1 t:$_AOI4_
select -assert-count 2 t:$_OAI3_
read_verilog ../top_fsm.v
synth -top top
abc -g gates
read_verilog ../top.v
synth -top top
abc -g aig
select -assert-count 2 t:$_AND_
select -assert-count 3 t:$_NAND_
select -assert-count 2 t:$_OR_
read_verilog ../top.v
synth -top top
abc -g cmos
select -assert-count 1 t:$_NAND_
select -assert-count 1 t:$_NOT_
select -assert-count 1 t:$_OAI3_
select -assert-count 2 t:$_XNOR_
read_verilog ../top.v
synth -top top
abc -g cmos2
select -assert-count 4 t:$_NAND_
select -assert-count 5 t:$_NOR_
select -assert-count 3 t:$_NOT_
read_verilog ../top.v
proc
dff2dffe
synth -top top
abc -g simple
select -assert-count 2 t:$_AND_
select -assert-count 1 t:$_OR_
select -assert-count 2 t:$_NOT_
read_verilog ../top.v
synth -top top
tee -o result.log abc -I 4
abc -dff
read_verilog ../top.v
synth -top top
tee -o result.out abc -luts :
abc -liberty -luts :
read_verilog ../top_logic.v
proc
synth -top top
tee -o result.out abc
read_verilog ../top_logic_loop.v
proc
synth -top top
tee -o result.out abc
read_verilog ../top.v
synth -top top
tee -o result.log abc -lut 4
abc -lut 3
stat
ERROR: Got -lut and -liberty! This two options are exclusive.
read_verilog ../top.v
synth -top top
tee -o result.out abc -lut 2 -liberty top.lib
abc -lut 2 -liberty top.lib
read_verilog ../top.v
synth -top top
tee -o result.log abc -lut -4
abc -lut -3:1
read_verilog ../top.v
synth -top top
tee -o result.log abc -luts 3:4
read_verilog ../top_dff.v
proc
dff2dffe
synth -top top
tee -o result.out abc -markgroups
read_verilog ../top_mux.v
proc
synth -top top
abc
select -assert-count 139 t:$_MUX_
read_verilog ../top_mux.v
synth -top top
tee -o result.log abc -mux16
stat
read_verilog ../top_mux.v
synth -top top
abc -mux4
select -assert-count 75 t:$_MUX4_
read_verilog ../top_mux.v
synth -top top
tee -o result.log abc -mux8
stat
read_verilog ../top_mux.v
synth -top top
tee -o result.out abc -g cmos3
abc -g cmos3
select -assert-count 144 t:$_AOI3_
select -assert-count 169 t:$_OAI3_
read_verilog ../top_mux.v
synth -top top
tee -o result.out abc -g cmos4
abc -g cmos4
select -assert-count 111 t:$_AOI3_
select -assert-count 28 t:$_AOI4_
select -assert-count 111 t:$_AOI3_
select -assert-count 24 t:$_OAI4_
read_verilog ../top.v
tee -o result.out abc
read_verilog ../top.v
proc
tee -o result.out abc
read_verilog ../top.v
synth -top top
tee -o result.log abc -P 4
abc -dff
read_verilog ../top.v
synth -top top
tee -o result.out abc -g XOR
abc -g XOR
ERROR: Can't open ABC output file
read_verilog ../top.v
synth -top top
tee -o result.out abc -script o
abc -script o
ERROR: Can't open ABC output file
read_verilog ../top.v
synth -top top
tee -o result.out abc -script top.yss
abc -script top.yss
read_verilog ../top_dff.v
tee -o result.out abc
ERROR: Command syntax error: Unsupported gate type: XO
read_verilog ../top.v
synth -top top
tee -o result.out abc -g XO
abc -g XO
(* black_box *) module top
(
input x,
input y,
input cin,
output A,
output cout
);
assign {cout,A} = cin + y + x;
endmodule
module adff
( input d, clk, clr, output reg q );
initial begin
q = 0;
end
always @( posedge clk, posedge clr )
if ( clr )
q <= 1'b0;
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 )
q <= 1'b0;
else
q <= d;
endmodule
module dffe
( input d, clk, en, output reg q );
initial begin
q = 0;
end
always @( posedge clk )
if ( en )
q <= d;
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 )
q <= 1'b0;
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 )
q <= 1'b0;
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
module top
(
input x,
input y,
input cin,
output A,
output cout
);
assign cout = x / y * cin;
endmodule
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
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
always @(posedge x) begin
A1 <= ~y + &cin;
end
always @(posedge x) begin
cout1 <= cin ? |y : ^A;
end
always @(posedge x) begin
A <= A1|y~&cin~^A1;
end
always @(posedge x) begin
cout <= cout1&cin~|y;
end
always @(posedge x) begin
A2 <= ~(y | cin);
end
always @(posedge x) begin
cout2 <= cin ~|y;
end
endmodule
module top
(
input x,
input y,
input z,
output A,
output B
);
wire A1,B1,A2,B2;
assign A1 = x & A2;
assign A2 = A1 & y;
assign A = ~A2;
endmodule
module top (
input [7:0] S,
input [255:0] D,
output M256
);
assign M256 = D[S];
endmodule
read_verilog ../top.v
proc
dff2dffe
synth -top top
abc9 -D 2 -lut 2
read_verilog ../top.v
proc
dff2dffe
synth -top top
abc9 -W -lut 2
abc9 -box box.txt -lut 2
read_verilog ../top_dff.v
proc
dff2dffe
synth -top top
abc9 -lut 5
abc9 -lut 5
read_verilog ../top_dff.v
proc
dff2dffe
synth -top top
abc9 -lut 5 -nomfs
abc9 -lut 5
read_verilog ../top_dff.v
proc
dff2dffe
techmap
abc9 -lut 5
abc9 -lut 5
read_verilog ../top.v
proc
dff2dffe
synth -top top
abc9 -fast -lut 2
read_verilog ../top.v
abc9 -luts 2:2:2:/2
read_verilog ../top.v
proc
dff2dffe
synth -top top
abc9 -lut 2
read_verilog ../top.v
proc
dff2dffe
synth -top top
abc9 -luts 2,3,4
read_verilog ../top.v
proc
dff2dffe
synth -top top
abc9 -markgroups -lut 2
read_verilog ../top_mem.v
proc
dff2dffe
synth -top top
abc9 -D 2 -lut 2
read_verilog ../top_mux.v
proc
synth -top top
abc9 -lut 2
read_verilog ../top.v
proc
dff2dffe
synth -top top
abc9 -nocleanup -lut 2
abc9 -script box.txt -lut 2
read_verilog ../top.v
proc
dff2dffe
synth -top top
abc9 -showtmp -lut 2
read_verilog ../top_mux.v
proc
techmap
abc9 -lut 2
read_verilog ../top_dff.v
abc9 -lut 2
read_verilog ../top_mux.v
proc
abc9 -lut 2
(* black_box *) module top
(
input x,
input y,
input cin,
output A,
output cout
);
assign {cout,A} = cin + y + x;
endmodule
module adff
( input d, clk, clr, output reg q );
initial begin
q = 0;
end
always @( posedge clk, posedge clr )
if ( clr )
q <= 1'b0;
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 )
q <= 1'b0;
else
q <= d;
endmodule
module dffe
( input d, clk, en, output reg q );
initial begin
q = 0;
end
always @( posedge clk )
if ( en )
q <= d;
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 )
q <= 1'b0;
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 )
q <= 1'b0;
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
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
if (we_a)
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
if (we_b)
begin
ram[addr_b] <= data_b;
q_b <= data_b;
end
if (re_b)
begin
q_b <= ram[addr_b];
end
end
endmodule
module top (
input [7:0] S,
input [255:0] D,
output M256
);
parameter i = 3;
assign M256 = D[S];
endmodule
read_verilog ../top.v
add -wire w 0
tee -o result.out dump
ERROR: Found incompatible object with same name in module \\top2!
read_verilog ../top.v
add -input i 2
add -wire i 2
tee -o result.log dump
wire width 32000 input 6 \\gi
read_verilog ../top.v
add -global_input gi 32000
tee -o result.out dump
wire width 3 inout 6 \\34
read_verilog ../top.v
add -inout \34 3
tee -o result.out dump
wire width 2 input 6 \\i
read_verilog ../top.v
add -input i 2
add -input i 2
tee -o result.out dump
read_verilog ../top.v
add -mod top3 -wire w 0
tee -o result.out dump
wire width 3 output 6 \\o
read_verilog ../top.v
add -output o 3
tee -o result.out dump
read_verilog ../top.v
add -wire w 1
tee -o result.out dump
module top
(
input x,
input y,
input cin,
output A,
output cout
);
assign {cout,A} = cin + y + x;
endmodule
module top2
(
input x,
input y,
input cin,
output A,
output cout
);
assign {cout,A} = cin * y / x;
endmodule
read_verilog ../top.v
proc
assertpmux
tee -o result.log dump
read_verilog ../top.v
proc
assertpmux -always
tee -o result.log dump
read_verilog ../top_mux.v
proc
assertpmux
tee -o result.log dump
read_verilog ../top.v
proc
assertpmux -noinit
tee -o result.log dump
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
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];
default: Y = 1'bx;
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];
default: Y = 1'bx;
endcase
end
endmodule
module mux16 (D, S, Y);
input [15:0] D;
input [3:0] S;
output Y;
reg Y;
wire[3:0] S;
wire[15: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];
8 : Y = D[8];
9 : Y = D[9];
10 : Y = D[10];
11 : Y = D[11];
12 : Y = D[12];
13 : Y = D[13];
14 : Y = D[14];
15 : Y = D[15];
default: Y = 1'bx;
endcase
end
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
attribute \\blackbox 1
attribute \\cells_not_processed 1
attribute \\src "../top.v:1"
module \\bb
read_verilog ../top.v
blackbox bb
tee -o result.out dump
read_verilog ../top_mem.v
blackbox top
tee -o result.log dump
attribute \\blackbox 1
attribute \\cells_not_processed 1
attribute \\src "../top.v:15"
module \\top
read_verilog ../top.v
blackbox top
tee -o result.out dump
module bb
(
input x,
input y,
input cin,
output A,
output cout
);
assign {cout,A} = cin + y + x;
endmodule
module top
(
input x,
input y,
input cin,
output A,
output cout
);
bb u_bb (x,y,cin,A,cout);
endmodule
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
if (we_a)
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
if (we_b)
begin
ram[addr_b] <= data_b;
q_b <= data_b;
end
if (re_b)
begin
q_b <= ram[addr_b];
end
end
endmodule
read_verilog ../top.v
tee -o result.log bugpoint -script ../script.yss -cells
read_verilog ../top.v
tee -o result.log bugpoint -script ../script.yss -clean
read_verilog ../top.v
tee -o result.log bugpoint -script ../script.yss -connections
ERROR: The provided script file and Yosys binary do not crash on this design!
read_verilog ../top.v
tee -o result.log bugpoint -script ../script.yss -connections
read_verilog ../top.v
tee -o result.log bugpoint -script ../script.yss -fast
ERROR: This command only operates on fully selected designs!
read_verilog ../top.v
select bb
tee -o result.log bugpoint -script ../script.yss
read_verilog ../top.v
tee -o result.log bugpoint -script ../script.yss -grep "Simplifications exhausted"
read_verilog ../top.v
tee -o result.log bugpoint -script ../script.yss -grep "SSS"
read_verilog ../top.v
tee -o result.log bugpoint
read_verilog ../top.v
tee -o result.log bugpoint -script ../script.yss -modules
read_verilog ../top.v
tee -o result.log bugpoint -script ../script.yss -ports
read_verilog ../top.v
tee -o result.log bugpoint -script ../script.yss
read_verilog ../top.v
tee -o result.log bugpoint -script script.ys -yosys yosys.yss
read_verilog ../top2.v
abc -g cmos4
module bb
(
input x,
input y,
input cin,
output A,
output cout
);
`ifndef BUG
assign {cout,A} = cin + y + x;
`else
assign {cout,A} = cin - y * x;
`endif
endmodule
module top
(
input x,
input y,
input cin,
output A,
output cout
);
bb u_bb (x,y,cin,A,cout);
endmodule
module bb2
(
input x,
input y,
input cin,
output A,
output cout
);
`ifndef BUG
assign {cout,A} = cin + y + x;
`else
assign {cout,A} = cin - y * x;
`endif
endmodule
module top2
(
input x,
input y,
input cin,
output A,
output cout
);
bb2 u_bb2 (x,y,cin,A,cout);
endmodule
read_verilog -sv ../top.v
proc
tee -o result.out check
read_verilog -sv ../top.v
proc
tee -o result.out check -assert
ERROR: Found 1 problems in 'check -assert'.
read_verilog -sv ../top1.v
proc
check -assert
read_verilog -sv ../top1.v
proc
tee -o result.out check -initdrv
read_verilog -sv ../top_logic_loop.v
proc
tee -o result.out check
read_verilog -sv ../top1.v
proc
tee -o result.out check -noinit
module top
( input d, clk, output reg q );
wire u;
always @( posedge clk )
q <= d;
endmodule
module top
( input d, clk, output reg q );
wire u;
wire s;
assign u = s;
assign u = d;
assign u = clk;
always @( posedge clk )
q <= u;
endmodule
module top
(
input x,
input y,
input z,
output A,
output B
);
wire A1,B1,A2,B2;
assign A1 = x & A2;
assign A2 = A1 & y;
assign A = ~A2;
endmodule
read_verilog -sv ../top.v
chformal -remove
tee -o result.log dump
read_verilog -sv ../top.v
chformal -assert -remove
tee -o result.log dump
read_verilog -sv ../top.v
chformal -assert2assume
tee -o result.log dump
read_verilog -sv ../top.v
chformal -assume -remove
tee -o result.log dump
read_verilog -sv ../top.v
chformal -assume2assert
tee -o result.log dump
read_verilog -sv ../top.v
tee -o result.log chformal -cover -remove
read_verilog -sv ../top.v
tee -o result.log chformal -delay 2
read_verilog -sv ../top_dff.v
chformal -remove
tee -o result.log dump
read_verilog -sv ../top.v
tee -o result.log chformal -early
read_verilog -sv ../top.v
chformal
tee -o result.log dump
read_verilog -sv ../top.v
tee -o res dump
chformal -fair -remove
tee -o result.log dump
read_verilog -sv ../top.v
chformal -fair2live
tee -o result.log dump
read_verilog -sv ../top.v
chformal -fair2live -assert2assume
tee -o result.log dump
read_verilog -sv ../top.v
proc
clk2fflogic
chformal -early
tee -o result.log dump
read_verilog -sv ../top_lat.v
chformal -remove
tee -o result.log dump
read_verilog -sv ../top.v
chformal -live -remove
tee -o result.log dump
read_verilog -sv ../top.v
chformal -live2fair
tee -o result.log dump
read_verilog -sv ../top.v
proc
tee -o result.log chformal -early
read_verilog -sv ../top.v
tee -o result.log chformal -skip 2
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
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
endmodule
module top
( input d, clk, output reg q );
always @( posedge clk )
q <= d;
endmodule
module alat
( input d, en, clr, output reg q );
initial begin
q = 0;
end
always @(*)
if ( clr )
q <= 1'b0;
else if (en)
q <= d;
endmodule
module alatn
( input d, en, clr, output reg q );
initial begin
q = 0;
end
always @(*)
if ( !clr )
q <= 1'b0;
else if (!en)
q <= d;
endmodule
module latsr
( input d, en, pre, clr, output reg q );
initial begin
q = 0;
end
always @(*)
if ( clr )
q <= 1'b0;
else if ( pre )
q <= 1'b1;
else if ( en )
q <= d;
endmodule
module nlatsr
( input d, en, pre, clr, output reg q );
initial begin
q = 0;
end
always @(*)
if ( !clr )
q <= 1'b0;
else if ( !pre )
q <= 1'b1;
else if ( !en )
q <= d;
endmodule
module dlatchsr (EN, SET, CLR, D, Q);
input EN;
input SET, CLR, D;
output reg Q;
always @*
if (CLR)
Q = 0;
else if (SET)
Q = 1;
else if (EN)
Q = D;
endmodule
module top (
input en,
input clr,
input pre,
input a,
output b,b1,b2,b3
);
latsr u_latsr (
.en (en ),
.clr (clr),
.pre (pre),
.d (a ),
.q (b )
);
nlatsr u_nlatsr (
.en (en ),
.clr (clr),
.pre (pre),
.d (a ),
.q (b1 )
);
alat u_alat (
.en (en ),
.clr (clr),
.d (a ),
.q (b2 )
);
alatn u_alatn (
.en (en ),
.clr (clr),
.d (a ),
.q (b3 )
);
endmodule
read_verilog ../top.v
proc
tee -o result.log chparam
ERROR: The options -set and -list cannot be used together.
read_verilog ../top.v
proc
tee -o result.log chparam -set X 2 -list top
read_verilog ../top.v
proc
chparam -set X 2 top
tee -o result.out chparam -list
read_verilog ../top.v
proc
tee -o result.out chparam -set X 2 top
read_verilog ../top.v
proc
tee -o result.log chparam top
module top
(
input x,
input y,
input cin,
output reg A,
output cout
);
wire o;
parameter X = 1;
always @(posedge cin)
A <= o;
assign cout = cin? y : x;
middle u_mid (x,y,o);
endmodule
module middle
(
input x,
input y,
output o
);
assign o = x + y;
endmodule
read_verilog -sv ../top.v
proc
chtype
read_verilog -sv ../top.v
proc
chtype -map $dff $adff $2
read_verilog -sv ../top.v
proc
chtype $2
read_verilog -sv ../top.v
proc
tee -o result.log chtype -set $adff $2
module top
( input d, clk, output reg q );
always @( posedge clk )
q <= d;
endmodule
ERROR: Failed to parse set lhs expression `sdf'.
read_verilog -sv ../top.v
proc
tee -o result.log connect -set sdf sdf
ERROR: Failed to parse set rhs expression `sdf'.
read_verilog -sv ../top.v
proc
tee -o result.log connect -set d sdf
read_verilog -sv ../top.v
proc
connect -set d q
tee -o result.log connect -port $procddff$2 D d
ERROR: Failed to parse unset expression `sdf'.
read_verilog -sv ../top.v
proc
tee -o result.log connect -unset sdf
ERROR: Failed to parse port expression `dd'.
read_verilog -sv ../top.v
proc
connect -set d q
tee -o result.log connect -port $procdff$2 D dd
ERROR: Found processes in selected module.
read_verilog -sv ../top.v
tee -o result.log connect -unset d q
ERROR: Multiple modules selected: top2, top
read_verilog -sv ../top_2.v
proc
tee -o result.log connect -unset d q
tee -o result.log connect -unset d q
read_verilog -sv ../top.v
proc
connect -nomap -port $procdff$2 D d1
tee -o result.out dump
read_verilog -sv ../top.v
proc
connect -nomap -set d1 q
tee -o result.out dump
wire $auto$connect.cc:33:unset_drivers$3
read_verilog -sv ../top.v
proc
connect -nomap -unset d q
tee -o result.out dump
read_verilog -sv ../top.v
proc
connect -nounset -set d1 q
tee -o result.out dump
ERROR: Expected -set, -unset, or -port.
read_verilog -sv ../top.v
proc
connect -set d q
tee -o result.log connect
read_verilog -sv ../top.v
proc
connect -port $procdff$2 D d1
tee -o result.out dump
ERROR: Can't use -port together with -nounset.
read_verilog -sv ../top.v
proc
tee -o result.log connect -port $procdff$2 D d -nounset d
read_verilog -sv ../top.v
proc
connect -set d1 q
tee -o result.out dump
ERROR: Can't use -set together with -unset and/or -port.
read_verilog -sv ../top.v
proc
tee -o result.log connect -set d q -port $procdff$2 D d
ERROR: Can't use -set together with -unset and/or -port.
read_verilog -sv ../top.v
proc
tee -o result.log connect -set d q -unset d -port $procdff$2 D d
ERROR: Can't use -set together with -unset and/or -port.
read_verilog -sv ../top.v
proc
tee -o result.log connect -set d q -unset d
connect $auto$connect.cc:33:unset_drivers$4 \\q
read_verilog -sv ../top.v
proc
connect -set d1 q
connect -unset d1 q
tee -o result.out dump
ERROR: Can't use -unset together with -port and/or -nounset.
read_verilog -sv ../top.v
proc
connect -set d q
tee -o result.log connect -unset d -port $procdff$2 D d -nounset d
ERROR: Can't use -unset together with -port and/or -nounset.
read_verilog -sv ../top.v
proc
connect -set d q
tee -o result.log connect -unset d -nounset d
ERROR: Can't use -unset together with -port and/or -nounset.
read_verilog -sv ../top.v
proc
connect -set d q
tee -o result.log connect -unset d -port $procdff$2 D d
module top
( input d, d1, clk, output reg q );
always @( posedge clk )
q <= d;
endmodule
module top
( input d, clk, output reg q );
always @( posedge clk )
q <= d;
endmodule
module top2
( input d, clk, output reg q );
always @( posedge clk )
q <= d;
endmodule
read_verilog ../top.v
proc
connwrappers
read_verilog ../top.v
proc
connwrappers -port $dff d1 32000 1
read_verilog ../top.v
proc
connwrappers -signed $dff d 3
read_verilog ../top.v
proc
connwrappers -unsigned $dff d 0
module top
( input d, clk, output reg q );
always @( posedge clk )
q <= d;
endmodule
read_verilog ../top.v
tee -o result.log cover
read_verilog ../top.v
tee -o result.log cover -a out.txt
ERROR: Can't create file aa/out.txt.
read_verilog ../top.v
tee -o result.log cover -o aa/out.txt
read_verilog ../top.v
tee -o result.log cover -d ../test
ERROR: Can't create file in directory test.
read_verilog ../top.v
tee -o result.log cover -d test
read_verilog ../top.v
tee -o result.log cover -o out.txt
read_verilog ../top.v
tee -o result.log cover -q
module top
(
input x,
input y,
input cin,
output A,
output cout
);
assign {cout,A} = cin + y + x;
endmodule
read_verilog ../top.v
tee -o result.log cutpoint top/y top/x top/cout top/A top/cin
tee -o result.log cutpoint top
read_verilog -sv ../top_asserts.v
tee -o result.log cutpoint top/y top/x top/cout top/A top/cin
tee -o result.log cutpoint -undef top/cin
tee -o result.log cutpoint top/$auto$cutpoint.cc:70:execute$53
dump
read_verilog ../top.v
tee -o result.log cutpoint top/y top/x top/cout top/A
tee -o result.log cutpoint -undef top/cin
tee -o result.log cutpoint -undef top
module bb
(
input x,
input y,
input cin,
output A,
output cout
);
assign {cout,A} = cin + y + x;
endmodule
module top
(
input x,
input y,
input cin,
output A,
output cout
);
bb u_bb (x,y,cin,A,cout);
endmodule
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
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
endmodule
debug read_verilog ../top.v
debug proc
tee -o result.log debug synth -top top
module top
(
input x,
input y,
input cin,
output A,
output cout
);
assign {cout,A} = cin + y + x;
endmodule
read_verilog ../top.v
delete middle
tee -o result.log dump
read_verilog ../top.v
delete top/$2
tee -o result.log dump
read_verilog ../top.v
tee -o res.log dump
delete -input top/x
tee -o result.log dump
read_verilog ../top_mem.v
delete top/$memrd$\ram$../top.v:30$7
tee -o result.log dump
read_verilog ../top_mem.v
proc
memory
delete top/$memrd$\ram$../top.v:30$7
tee -o result.log dump
read_verilog ../top.v
delete -output middle/o
tee -o result.log dump
read_verilog ../top.v
delete -port top/A
tee -o result.log dump
read_verilog ../top.v
tee -o resul.log dump
delete top/$1
tee -o result.log dump
read_verilog ../top.v
tee -o resul.log dump
delete top/o
tee -o result.log dump
module top
(
input x,
input y,
input cin,
output reg A,
output cout
);
wire o;
`ifndef BUG
always @(posedge cin)
A <= o;
assign cout = cin? y : x;
middle u_mid (x,y,o);
`else
assign {cout,A} = cin - y * x;
`endif
endmodule
module middle
(
input ux,
input y,
output o
);
assign o = ux + y;
endmodule
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
if (we_a)
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
if (we_b)
begin
ram[addr_b] <= data_b;
q_b <= data_b;
end
if (re_b)
begin
q_b <= ram[addr_b];
end
end
endmodule
read_verilog -sv ../top.v
proc
design -save first
design -copy-from first -as top_2 top
design -copy-to first -as top_2 top
read_verilog -sv ../top.v
proc
design -save first
design -reset
design -copy-from first top
read_verilog -sv ../top.v
proc
design -save first
design -reset
design -copy-to first top
read_verilog -sv ../top.v
proc
design -save first
design -import first top
read_verilog -sv ../top.v
proc
design -pop
read_verilog -sv ../top.v
proc
design -copy-from first -as top_2 top
read_verilog -sv ../top.v
proc
design -import first top
read_verilog -sv ../top.v
proc
design -load first
ERROR: No top module found in source design.
read_verilog -sv ../top.v
design -save first
design -import first
module top
(
input x,
input y,
input cin,
output reg A,
output cout
);
parameter X = 1;
wire o;
always @(posedge cin)
A <= o;
middle u_mid (.x(x),.o(o));
u_rtl inst_u_rtl (.x(x),.o(o));
endmodule
module middle
(
input x,
input y,
output o
);
assign o = x + y;
endmodule
module u_rtl
(
input x,
input y,
output o
);
assign o = x + y;
endmodule
module top
(
input x,
input y,
input cin,
output reg A,
output cout
);
wire o;
`ifndef BUG
always @(posedge cin)
A <= o;
assign cout = cin? y : x;
middle u_mid (x,y,o);
`else
assign {cout,A} = cin - y * x;
`endif
endmodule
module middle
(
input x,
input y,
output o
);
assign o = x + y;
endmodule
$_DFF_P_.Q $_XOR_.A
$_XOR_.Y $_DFF_N_.D
$_XOR_.Y $_DFF_P_.D
read_verilog ../top.v
synth
tee -o result.out edgetypes
$_ANDNOT_.Y $_OR_.A
$_AND_.Y $_OR_.B
$_XNOR_.Y $_ANDNOT_.B
$_XNOR_.Y $_XNOR_.A
read_verilog ../top_fulladder.v
edgetypes
synth
tee -o result.out edgetypes
module top
(
input x,
input y,
input cin,
output reg A,
output reg cout
);
initial begin
begin
A = 0;
cout = 0;
end
end
always @(posedge x) begin
A <= y + cin;
end
always @(negedge x) begin
cout <= y + A;
end
endmodule
module top
(
input x,
input y,
input cin,
output A,
output cout
);
`ifndef BUG
assign {cout,A} = cin + y + x;
`else
assign {cout,A} = cin - y * x;
`endif
endmodule
read_verilog ../top.v
proc
tee -o result.log eval middle
read_verilog ../top.v
proc
tee -o result.log eval -brute_force_equiv_checker_x top top
ERROR: Can't find input s in module middle!
read_verilog ../top_err_1.v
tee -o result.log eval -vloghammer_report mid dle s 1
read_verilog ../top.v
proc
tee -o result.log eval -brute_force_equiv_checker u top
read_verilog ../top.v
proc
tee -o result.log eval -brute_force_equiv_checker top u
ERROR: Can't find module dle in current design!
read_verilog ../top.v
tee -o result.log eval -vloghammer_report middle dle x 1
ERROR: Set expression with different lhs and rhs sizes:
read_verilog ../top.v
proc
tee -o result.log eval -set x 1 -set y 2'b11 u_rtl
ERROR: Can't perform EVAL on an empty selection!
read_verilog ../top.v
proc
tee -o result.log eval u
ERROR: Failed to parse lhs set expression `u'.
read_verilog ../top.v
proc
tee -o result.log eval -set u 0 middle
read_verilog ../top.v
tee -o result.log eval -vloghammer_report mid dle x d
ERROR: Failed to parse rhs set expression `u'.
read_verilog ../top.v
proc
tee -o result.log eval -set x u middle
ERROR: Failed to parse show expression `u'.
read_verilog ../top.v
proc
tee -o result.log eval -show u middle
ERROR: Failed to parse table expression `u'.
read_verilog ../top.v
proc
tee -o result.log eval -table u middle
ERROR: Port \\cout in module 1 has no counterpart in module 2!
read_verilog ../top.v
proc
tee -o result.log eval -brute_force_equiv_checker top u_rtl
ERROR: Modules are not equivalent!
read_verilog ../top_err_1.v
proc
tee -o result.log eval -brute_force_equiv_checker middle u_rtl
ERROR: No output wire (y) found in module middle!
read_verilog ../top_err_1.v
tee -o result.log eval -vloghammer_report mid dle x 1
ERROR: Only one module must be selected for the EVAL pass! (selected: u_rtl and middle)
read_verilog ../top.v
proc
tee -o result.log eval
read_verilog ../top_err_2.v
tee -o result.log eval -vloghammer_report mid dle x 1'b1
ERROR: Port \\o in module 1 does not match its counterpart in module 2!
read_verilog ../top.v
proc
tee -o result.log eval -brute_force_equiv_checker u_rtl top
ERROR: Right-hand-side set expression `x' is not constant.
read_verilog ../top.v
proc
tee -o result.log eval -set x 1 -set y x u_rtl
read_verilog ../top.v
proc
tee -o result.log eval -set x 1 -set y 0 middle
read_verilog ../top.v
proc
tee -o result.log eval -set-undef middle
read_verilog ../top.v
proc
tee -o result.log eval -set x 1 -set y 0 -show o middle
read_verilog ../top.v
proc
tee -o result.log eval -show o middle
read_verilog ../top.v
proc
tee -o result.log eval -table o middle
read_verilog ../top.v
proc
tee -o result.log eval -set-undef -table o middle
ERROR: Found two distinct solutions to SAT problem.
read_verilog ../top_err_3.v
tee -o result.log eval -vloghammer_report u_ rtl x 1'b1
read_verilog ../top.v
proc
tee -o result.log eval -vloghammer_report mid dle x 1
read_verilog ../top.v
proc
tee -o result.log eval -vloghammer_report u_ rtl y 1
ERROR: Wire w in module middle is not an input!
read_verilog ../top.v
tee -o result.log eval -vloghammer_report mid dle w 1
module top
(
input x,
input y,
input cin,
output reg A,
output cout
);
parameter X = 1;
wire o;
`ifndef BUG
always @(posedge cin)
A <= o;
assign cout = cin? y : x;
middle u_mid (.x(x),.o(o),.y(1'b0));
u_rtl inst_u_rtl (.x(x),.o(o));
`else
assign {cout,A} = cin - y * x;
`endif
endmodule
module middle
(
input x,
input y,
output o
);
wire w;
assign o = x + y;
endmodule
module u_rtl
(
input x,
input y,
output o
);
assign o = x + y;
endmodule
module top
(
input x,
input y,
input cin,
output reg A,
output cout
);
parameter X = 1;
wire o;
wire w;
`ifndef BUG
always @(posedge cin)
A <= o;
assign cout = cin? y : x;
middle u_mid (.x(x),.o(o),.y(1'b0));
u_rtl inst_u_rtl (.x(x),.o(o));
`else
assign {cout,A} = cin - y * x;
`endif
endmodule
module middle
(
input x,
// input y,
output o
);
assign o = x;
endmodule
module u_rtl
(
input x,
input y,
output o
);
assign o = x + y;
endmodule
module top
(
input [7:0] x,
input[7:0] y,
input cin,
output reg [7:0] A,
output [7:0] cout
);
parameter X = 1;
wire o;
`ifndef BUG
always @(posedge cin)
A <= o;
assign cout = cin? y : x;
middle #(7) u_mid (.x(x),.o(o),.y(1'b0));
middle #(0) u_mid2 (.x(x),.o(o));
`else
assign {cout,A} = cin - y * x;
`endif
endmodule
module middle
(
x,
y,
o
);
parameter u = 7;
input [u:0] x;
input [u:0] y;
output [u:0] o;
assign o = x + y;
endmodule
module xiddle
(
input [1:0] x,
input y,
output [1:0] o
);
assign o = x + y;
endmodule
module top
(
input x,
input y,
input cin,
output reg A,
output cout
);
parameter X = 1;
wire o;
`ifndef BUG
always @(posedge cin)
A <= o;
assign cout = cin? y : x;
middle u_mid (.x(x),.o(o),.y(1'b0));
u_rtl inst_u_rtl (.x(x),.o(o));
`else
assign {cout,A} = cin - y * x;
`endif
endmodule
module middle
(
input x,
input y,
output o
);
wire w;
assign o = x + y;
endmodule
module u_rtl
(
input x,
input y,
output o
);
assign o = x + y;
endmodule
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment