Unverified Commit 14623819 by Miodrag Milanović Committed by GitHub

Merge pull request #37 from SergeyDegtyar/master

Add tests for error messages in 'misc' test group.
parents 2934eb5b 971f4827
read_verilog ../top.v
synth_xilinx -nosrl
write_verilog synth.v
(* black_box *) 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 ../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
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 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 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 top
(
input x,
input y,
input cin,
output reg A,
output cout
);
wire o;
parameter X = 1;
`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
module top
( input d, 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
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
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));
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 + 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;
`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
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_mid1 (.x(x),.o(o),.y(1'b0));
middle u_mid2 (.x(x),.o(o),.y(1'b1));
middle u_mid3 (.x(x),.o(o),.y(1'bX));
middle u_mid4 (.x(x),.o(o),.y(1'bX));
`else
assign {cout,A} = cin - y * x;
`endif
endmodule
module middle
(
input x,
input y,
output o
);
urtl u_urtl (.x(x),.o(o),.y(y));
endmodule
module urtl
(
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;
parameter U = "string";
wire o;
`ifndef BUG
always @(posedge cin)
A <= o;
assign cout = cin? y : x;
middle u_mid1 (.x(x),.o(o),.y(1'b0));
middle u_mid2 (.x(x),.o(o),.y(1'b1));
middle u_mid3 (.x(x),.o(o),.y(1'bX));
middle u_mid4 (.x(x),.o(o),.y(1'bX));
urtl u_urtl (.x(x),.o(o),.y(y));
`else
assign {cout,A} = cin - y * x;
`endif
endmodule
module middle
(
input x,
input y,
output o
);
parameter u = 12;
urtl u_urtl (.x(x),.o(o),.y(y));
endmodule
module urtl
(
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;
`ifndef BUG
always @(posedge cin)
A <= o;
//assign cout = cin? y : x;
middle u_mid (.x(x),.o(o));
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 + 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;
`ifndef BUG
always @(posedge cin)
A <= o;
//assign cout = cin? y : x;
middle u_mid (.x(x),.o(o));
u_rtl inst_u_rtl (.x(o),.o(x));
`else
assign {cout,A} = cin - y * x;
`endif
endmodule
module middle
(
input x,
input y,
output o
);
wire ll;
assign ll = x & o;
assign o = y & ll;
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;
`ifndef BUG
always @(posedge cin)
A <= o;
//assign cout = cin? y : x;
middle u_mid (.x(x),.o(o));
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 + 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;
`ifndef BUG
always @(posedge cin)
A <= o;
//assign cout = cin? y : x;
middle u_mid (.x(x),.o(o));
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 + y;
endmodule
module u_rtl
(
input x,
// input y,
output o
);
assign o = x;
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
module top
( input d, clk, output reg q );
always @( posedge clk )
q <= d;
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
);
wire dd;
assign o = x + y;
endmodule
module low ();
endmodule
module top
(
input x,
input y,
input cin,
output reg A,
output cout
);
parameter X = 1;
wire o;
initial A = 0;
initial cout = 0;
`ifndef BUG
always @(posedge cin)
A <= o;
assign cout = cin? y : x;
middle u_mid (.x(x),.o(o));
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 + 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
read_verilog ../top.v
add -input i 2
add -wire i 2
tee -o result.log dump
read_verilog ../top.v
tee -o result.log bugpoint -script ../script.ys -connections
read_verilog ../top.v
select bb
tee -o result.log bugpoint -script ../script.ys
read_verilog ../top.v
tee -o result.log bugpoint -script ../script.ys -grep "SSS"
read_verilog ../top.v
tee -o result.log bugpoint
read_verilog -sv ../top.v
proc
tee -o result.log check -assert
read_verilog -sv ../top.v
read_verilog -sv ../top1.v
proc
tee -o result.log check -initdrv
read_verilog -sv ../top.v
read_verilog -sv ../top1.v
proc
tee -o result.log check -noinit
read_verilog -sv ../top.v
chformal
tee -o result.log dump
read_verilog ../top.v
proc
tee -o result.log chparam -set X 2 -list top
read_verilog -sv ../top.v
proc
tee -o result.log connect -set sdf 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
read_verilog -sv ../top.v
proc
tee -o result.log connect -unset sdf
read_verilog -sv ../top.v
proc
connect -set d q
tee -o result.log connect -port $procdff$2 D dd
read_verilog -sv ../top.v
tee -o result.log connect -unset d q
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 -set d q
tee -o result.log connect
read_verilog -sv ../top.v
proc
tee -o result.log connect -port $procdff$2 D d -nounset d
read_verilog -sv ../top.v
proc
tee -o result.log connect -set d q -port $procdff$2 D d
read_verilog -sv ../top.v
proc
tee -o result.log connect -set d q -unset d
read_verilog -sv ../top.v
proc
tee -o result.log connect -set d q -unset d -port $procdff$2 D d
read_verilog -sv ../top.v
proc
connect -set d q
tee -o result.log connect -unset d -nounset d
read_verilog -sv ../top.v
proc
connect -set d q
tee -o result.log connect -unset d -port $procdff$2 D d -nounset d
read_verilog -sv ../top.v
proc
connect -set d q
tee -o result.log connect -unset d -port $procdff$2 D d
read_verilog ../top.v
tee -o result.log cover -o aa/out.txt
read_verilog -sv ../top.v
proc
tee -o result.log design -pop
read_verilog -sv ../top.v
proc
tee -o result.log design -copy-from first -as top_2 top
read_verilog -sv ../top.v
proc
tee -o result.log design -import first top
read_verilog -sv ../top.v
proc
design -load first
read_verilog -sv ../top.v
design -save first
tee -o result.log design -import first
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
read_verilog ../top.v
tee -o result.log eval -vloghammer_report middle dle x 1
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 -set x 1 -set y 2'b11 u_rtl
read_verilog ../top.v
proc
tee -o result.log eval 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
read_verilog ../top.v
proc
tee -o result.log eval -set x u middle
read_verilog ../top.v
proc
tee -o result.log eval -show u middle
read_verilog ../top.v
proc
tee -o result.log eval -table u middle
read_verilog ../top.v
proc
tee -o result.log eval -brute_force_equiv_checker top u_rtl
read_verilog ../top_err_1.v
proc
tee -o result.log eval -brute_force_equiv_checker middle u_rtl
read_verilog ../top_err_1.v
tee -o result.log eval -vloghammer_report mid dle x 1
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
read_verilog ../top.v
proc
tee -o result.log eval -brute_force_equiv_checker u_rtl top
read_verilog ../top.v
proc
tee -o result.log eval -set x 1 -set y x u_rtl
read_verilog ../top_err_3.v
tee -o result.log eval -vloghammer_report u_ rtl x 1'b1
read_verilog ../top.v
tee -o result.log eval -vloghammer_report mid dle w 1
read_verilog ../top.v
proc
tee -o result.log fmcombine top u_mid1 u_mid8
read_verilog ../top.v
proc
tee -o result.log fmcombine top u_mid8 u_mid3
read_verilog ../top.v
proc
tee -o result.log fmcombine
read_verilog ../top.v
proc
tee -o result.log fmcombine topp u_mid1 u_mid3
read_verilog ../top.v
tee -o result.log fmcombine -nop -bwd top u_mid1 u_mid2
read_verilog ../top.v
tee -o result.log fmcombine -nop -fwd top u_mid1 u_mid2
read_verilog ../top.v
tee -o result.log fmcombine -nop -fwd -bwd top u_mid1 u_mid2
read_verilog ../top_err_1.v
proc
tee -o result.log fmcombine top u_mid1 u_urtl
read_verilog ../top_err_1.v
tee -o result.log freduce
proc
tee -o result.log freduce
synth
tee -o result.log freduce
read_verilog -sv ../top.v
proc
tee -o result.log miter -equiv top gate top
read_verilog -sv ../top.v
proc
tee -o result.log miter -equiv gold gate top
read_verilog -sv ../top.v
proc
tee -o result.log miter -assert t
read_verilog -sv ../top.v
proc
tee -o result.log miter
read_verilog -sv ../top_err_1.v
proc
tee -o result.log miter -equiv middle u_rtl top1
read_verilog -sv ../top_err_1.v
proc
tee -o result.log miter -equiv u_rtl middle top1
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