Unverified Commit 64ab84a7 by Miodrag Milanović Committed by GitHub

Merge pull request #81 from SergeyDegtyar/review_frontends_group

Review frontends group
parents cfd1c5c9 45df44f0
*/work_*/
/.stamp
/run-test.mk
module assert_dff(input clk, input test, input pat);
always @(posedge clk)
begin
#1;
if (test != pat)
begin
$display("ERROR: ASSERTION FAILED in %m:",$time);
$stop;
end
end
endmodule
module assert_tri(input en, input A, input B);
always @(posedge en)
begin
#1;
if (A !== B)
begin
$display("ERROR: ASSERTION FAILED in %m:",$time," ",A," ",B);
$stop;
end
end
endmodule
module assert_Z(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
module assert_comb(input A, input B);
always @(*)
begin
#1;
if (A !== B)
begin
$display("ERROR: ASSERTION FAILED in %m:",$time," ",A," ",B);
$stop;
end
end
endmodule
read -formal ../top.v
read -define MACRO
read -formal ../top.v
read -define MACRO=1
read -formal ../top.v
read -formal ../top.v
read -incdir ../include_dir
read -sv2005 ../top.v
read -sv2009 ../top.v
read -sv2012 ../top.v
read -formal ../top.v
read -define MACRO
read -undef MACRO
read -formal ../top.v
read -vhdl ../top.vhd
design -reset
read_verilog ../top.v
synth -top top
......
read -vhdl ../top.vhd
read -formal ../top.v
read -define MACRO
read -vhdl2k ../top.vhd
design -reset
read_verilog ../top.v
synth -top top
......
read -vhdl2k ../top.vhd
read -formal ../top.v
read -define MACRO=1
read -vhdl87 ../top.vhd
design -reset
read_verilog ../top.v
synth -top top
......
read -vhdl87 ../top.vhd
read -formal ../top.v
read -incdir ../include_dir
read -vhdl93 ../top.vhd
design -reset
read_verilog ../top.v
synth -top top
......
read -vhdl93 ../top.vhd
read -vlog2k ../top.v
read -vlog95 ../top.v
module testbench;
reg [2:0] in;
wire patt_out;
wire patt_carry_out;
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)
);
assign patt_out = in[1] + in[2];
assign patt_carry_out = in[0] + patt_out;
assert_comb out_test(.A(patt_out), .B(out));
assert_comb carry_test(.A(patt_carry_out), .B(carryout));
endmodule
......@@ -9,12 +9,7 @@ module top
output cout
);
`ifndef BUG
assign A = y + cin;
assign cout = x + A;
`else
assign {cout,A} = cin - y * x;
`endif
endmodule
......@@ -3,7 +3,8 @@ aigmap
write_aiger aiger.aiger
design -reset
read_aiger aiger.aiger
design -reset
read_verilog -sv ../top.v
synth -top top
write_verilog synth.v
select -assert-count 6 t:$_AND_
select -assert-count 7 t:$_NOT_
select -assert-none t:$_AND_ t:$_NOT_ %% t:* %D
read_aiger -clk_name clk -module_name top ../aiger_ff.aig
select -assert-count 4 t:$_AND_
select -assert-count 1 t:$_DFF_P_
select -assert-count 4 t:$_NOT_
select -assert-none t:$_AND_ t:$_DFF_P_ t:$_NOT_ %% t:* %D
......@@ -3,7 +3,8 @@ aigmap
write_aiger -ascii aiger.aiger
design -reset
read_aiger aiger.aiger
design -reset
read_verilog -sv ../top.v
synth -top top
write_verilog synth.v
select -assert-count 6 t:$_AND_
select -assert-count 7 t:$_NOT_
select -assert-none t:$_AND_ t:$_NOT_ %% t:* %D
ERROR: Line 4 cannot be interpreted as a bad state property!
ERROR: Line 6 cannot be interpreted as an AND!
ERROR: Line 2 cannot be interpreted as an input!
read_aiger -clk_name clk ../aiger_ff.aig
select -assert-count 4 t:$_AND_
select -assert-count 1 t:$_DFF_P_
select -assert-count 4 t:$_NOT_
select -assert-none t:$_AND_ t:$_DFF_P_ t:$_NOT_ %% t:* %D
......@@ -3,7 +3,8 @@ aigmap
write_aiger aiger.aiger
design -reset
read_aiger -clk_name clk -module_name top aiger.aiger
design -reset
read_verilog -sv ../top.v
synth -top top
write_verilog synth.v
select -assert-count 6 t:$_AND_
select -assert-count 7 t:$_NOT_
select -assert-none t:$_AND_ t:$_NOT_ %% t:* %D
ERROR: Duplicate definition of module top!
ERROR: Line 1 has invalid reset literal for latch!
read_aiger -clk_name clk -module_name top ../aiger_latch.aig
stat
select -assert-count 1 t:$_DFF_P_
select -assert-count 1 t:$_NOT_
select -assert-none t:$_DFF_P_ t:$_NOT_ %% t:* %D
read_aiger -clk_name clk -module_name top ../aiger_logic.aig
select -assert-count 3 t:$_AND_
select -assert-count 4 t:$_NOT_
select -assert-none t:$_AND_ t:$_NOT_ %% t:* %D
......@@ -3,7 +3,8 @@ aigmap
write_aiger aiger.aiger
design -reset
read_aiger -map aig.map aiger.aiger
design -reset
read_verilog -sv ../top.v
synth -top top
write_verilog synth.v
select -assert-count 6 t:$_AND_
select -assert-count 7 t:$_NOT_
select -assert-none t:$_AND_ t:$_NOT_ %% t:* %D
......@@ -3,7 +3,8 @@ aigmap
write_aiger aiger.aiger
design -reset
read_aiger -module_name top aiger.aiger
design -reset
read_verilog -sv ../top.v
synth -top top
write_verilog synth.v
select -assert-count 6 t:$_AND_
select -assert-count 7 t:$_NOT_
select -assert-none t:$_AND_ t:$_NOT_ %% t:* %D
read_aiger -clk_name clk -module_name top ../aiger_mult.aig
stat
select -assert-count 8 t:$_AND_
select -assert-count 2 t:$dff
select -assert-count 9 t:$_NOT_
select -assert-none t:$_AND_ t:$dff t:$_NOT_ %% t:* %D
......@@ -4,7 +4,8 @@ aigmap
write_aiger aiger.aiger
design -reset
read_aiger aiger.aiger
design -reset
read_verilog -sv ../top.v
synth -top top
write_verilog synth.v
select -assert-count 6 t:$_AND_
select -assert-count 7 t:$_NOT_
select -assert-none t:$_AND_ t:$_NOT_ %% t:* %D
module testbench;
reg [2:0] in;
wire patt_out;
wire patt_carry_out;
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)
);
assign patt_out = in[1] + in[2];
assign 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
......@@ -9,12 +9,7 @@ module top
output cout
);
`ifndef BUG
assign A = y + cin;
assign cout = y + A;
`else
assign {cout,A} = cin - y * x;
`endif
endmodule
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 n1,n2 = 0;
wire n3,n3_inv;
reg n3p;
wire n3ip;
top uut (
.clk (clk ),
.__1__ (n1 ),
.__2__ (n2 ),
.__3__ (n3 ),
.__3b__ (n3_inv )
);
always @(posedge clk) begin
#3;
n1 <= n1 + 1;
#1;
n2 <= n2 + 1;
end
wire _0_;
wire n4p;
assign _0_ = ~(n3p ^ n1);
assign n4p = n2 & ~(_0_);
assign n3ip = ~n3p;
always @(posedge clk)
n3p <= n4p;
assert_dff dff_test(.clk(clk), .test(n3), .pat(n3p));
endmodule
module testbench;
reg en;
initial begin
// $dumpfile("testbench.vcd");
// $dumpvars(0, testbench);
#5 en = 0;
repeat (10000) begin
#5 en = 1;
#5 en = 0;
end
$display("OKAY");
end
reg dinA = 0;
wire doutB;
reg lat = 0;
top uut (
.clk (en ),
//.__1__ (dinA ),
.__1b__ (doutB )
);
always @(posedge en) begin
#3;
dinA <= dinA + 1;
end
always @(* )
if ( en )
lat <= dinA;
assert_dff lat_test(.clk(en), .test(doutB), .pat(lat));
endmodule
module testbench;
reg [0:1] in;
wire pat,pat1;
wire c,s;
initial begin
// $dumpfile("testbench.vcd");
// $dumpvars(0, testbench);
#5 in = 0;
repeat (10000) begin
#5 in = in + 1;
end
$display("OKAY");
end
top uut (
.c(c),
.s(s),
.x(in[0]),
.y(in[1])
);
assign pat = in[1] ^ in[0];
assign pat1 = in[1] & in[0];
assert_comb out_test(.A(pat), .B(s));
assert_comb out1_test(.A(pat1), .B(c));
endmodule
module testbench;
reg [0:1] in;
wire pat,pat1;
wire c,s;
initial begin
// $dumpfile("testbench.vcd");
// $dumpvars(0, testbench);
#5 in = 0;
repeat (10000) begin
#5 in = in + 1;
end
$display("OKAY");
end
endmodule
module testbench;
reg [0:1] in;
wire pat,pat1;
wire c,s;
initial begin
// $dumpfile("testbench.vcd");
// $dumpvars(0, testbench);
#5 in = 0;
repeat (10000) begin
#5 in = in + 1;
end
$display("OKAY");
end
endmodule
......@@ -3,8 +3,8 @@ synth -top top
write_blif blif1.blif
design -reset
read_blif blif1.blif
design -reset
read_verilog -sv ../top.v
synth -top top
write_blif blif5.blif
write_verilog synth.v
select -assert-count 2 t:$dff
select -assert-count 2 t:$lut
select -assert-none t:$dff t:$lut %% t:* %D
read_verilog ../top_and_or.v
synth -top top
write_blif blif1.blif
design -reset
read_blif blif1.blif
stat
select -assert-count 1 t:$dff
select -assert-count 11 t:$lut
select -assert-none t:$dff t:$lut %% t:* %D
......@@ -3,8 +3,8 @@ synth -top top
write_blif -attr blif1.blif
design -reset
read_blif blif1.blif
design -reset
read_verilog -sv ../top.v
synth -top top
write_blif blif5.blif
write_verilog synth.v
select -assert-count 2 t:$dff
select -assert-count 2 t:$lut
select -assert-none t:$dff t:$lut %% t:* %D
read_verilog ../top_mem.v
synth -top top
write_blif -attr blif1.blif
design -reset
read_blif blif1.blif
stat
select -assert-count 528 t:$dff
select -assert-count 2372 t:$lut
select -assert-none t:$dff t:$lut %% t:* %D
read_verilog ../top_mux.v
synth -top top
write_blif -attr blif1.blif
design -reset
read_blif blif1.blif
stat
select -assert-count 58 t:$lut
select -assert-count 1 t:$paramod\mux4\dw?4
#select -assert-none t:$lut t:$paramod\mux4\dw?4 %% t:* %D
......@@ -3,8 +3,8 @@ synth -top top
write_blif -buf a a a blif1.blif
design -reset
read_blif blif1.blif
design -reset
read_verilog -sv ../top.v
synth -top top
write_blif blif5.blif
write_verilog synth.v
stat
select -assert-count 2 t:$dff
select -assert-count 2 t:$lut
select -assert-none t:$dff t:$lut %% t:* %D
read_verilog ../top_mem.v
synth -top top
write_blif -buf a a a blif1.blif
design -reset
read_blif blif1.blif
stat
select -assert-count 528 t:$dff
select -assert-count 2372 t:$lut
select -assert-none t:$dff t:$lut %% t:* %D
read_verilog ../top_mux.v
synth -top top
write_blif -buf a a a blif1.blif
design -reset
read_blif blif1.blif
stat
select -assert-count 58 t:$lut
select -assert-count 1 t:$paramod\mux4\dw?4
#select -assert-none t:$lut t:$paramod\mux4\dw?4 %% t:* %D
......@@ -3,8 +3,8 @@ synth -top top
write_blif -cname blif1.blif
design -reset
read_blif blif1.blif
design -reset
read_verilog -sv ../top.v
synth -top top
write_blif blif5.blif
write_verilog synth.v
select -assert-count 2 t:$dff
select -assert-count 2 t:$lut
select -assert-none t:$dff t:$lut %% t:* %D
read_verilog ../top_mem.v
synth -top top
write_blif -cname blif1.blif
design -reset
read_blif blif1.blif
stat
select -assert-count 528 t:$dff
select -assert-count 2372 t:$lut
select -assert-none t:$dff t:$lut %% t:* %D
read_verilog ../top_mux.v
synth -top top
write_blif -cname blif1.blif
design -reset
read_blif blif1.blif
stat
select -assert-count 58 t:$lut
select -assert-count 1 t:$paramod\mux4\dw?4
#select -assert-none t:$lut t:$paramod\mux4\dw?4 %% t:* %D
......@@ -3,8 +3,8 @@ synth -top top
write_blif -conn blif1.blif
design -reset
read_blif blif1.blif
design -reset
read_verilog -sv ../top.v
synth -top top
write_blif blif5.blif
write_verilog synth.v
select -assert-count 2 t:$dff
select -assert-count 2 t:$lut
select -assert-none t:$dff t:$lut %% t:* %D
read_verilog ../top_mem.v
synth -top top
write_blif -conn blif1.blif
design -reset
read_blif blif1.blif
stat
select -assert-count 528 t:$dff
select -assert-count 2372 t:$lut
select -assert-none t:$dff t:$lut %% t:* %D
read_verilog ../top_mux.v
synth -top top
write_blif -conn blif1.blif
design -reset
read_blif blif1.blif
stat
select -assert-count 58 t:$lut
select -assert-count 1 t:$paramod\mux4\dw?4
#select -assert-none t:$lut t:$paramod\mux4\dw?4 %% t:* %D
ERROR: Duplicate definition of module top in line 3!
......@@ -2,8 +2,3 @@ read_verilog ../top.v
synth -top top
write_blif blif1.blif
read_blif blif1.blif
design -reset
read_verilog -sv ../top.v
synth -top top
write_blif blif5.blif
write_verilog synth.v
read_blif -wideports ../eblif.eblif
stat
select -assert-count 1 t:$dff
select -assert-count 2 t:$lut
select -assert-none t:$dff t:$lut %% t:* %D
read_verilog ../top_fsm.v
synth -top top
write_blif blif1.blif
design -reset
read_blif blif1.blif
stat
select -assert-count 17 t:$dff
select -assert-count 58 t:$lut
#select -assert-none t:$dff t:$lut %% t:* %D
read_verilog ../top_logic.v
synth -top top
write_blif blif1.blif
design -reset
read_blif blif1.blif
stat
select -assert-count 4 t:$dff
select -assert-count 6 t:$lut
select -assert-none t:$dff t:$lut %% t:* %D
read_verilog ../top_mem.v
synth -top top
write_blif blif1.blif
design -reset
read_blif blif1.blif
stat
select -assert-count 528 t:$dff
select -assert-count 2372 t:$lut
select -assert-none t:$dff t:$lut %% t:* %D
read_verilog ../top_mux.v
synth -top top
write_blif blif1.blif
design -reset
read_blif blif1.blif
stat
select -assert-count 58 t:$lut
select -assert-count 1 t:$paramod\mux4\dw?4
#select -assert-none t:$lut t:$paramod\mux4\dw?4 %% t:* %D
......@@ -3,8 +3,8 @@ synth -top top
write_blif -param blif1.blif
design -reset
read_blif blif1.blif
design -reset
read_verilog -sv ../top.v
synth -top top
write_blif blif5.blif
write_verilog synth.v
select -assert-count 2 t:$dff
select -assert-count 2 t:$lut
select -assert-none t:$dff t:$lut %% t:* %D
read_verilog ../top_mem.v
synth -top top
write_blif -param blif1.blif
design -reset
read_blif blif1.blif
stat
select -assert-count 528 t:$dff
select -assert-count 2372 t:$lut
select -assert-none t:$dff t:$lut %% t:* %D
read_verilog ../top_mux.v
synth -top top
write_blif -param blif1.blif
design -reset
read_blif blif1.blif
stat
select -assert-count 58 t:$lut
select -assert-count 1 t:$paramod\mux4\dw?4
#select -assert-none t:$lut t:$paramod\mux4\dw?4 %% t:* %D
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