Unverified Commit 87b97ca9 by Miodrag Milanović Committed by GitHub

Merge pull request #17 from SergeyDegtyar/master

 Add new tests to 'simple' and 'misc' groups
parents 7d40fce4 76f18bfc
...@@ -138,7 +138,9 @@ $(eval $(call template,miter_assert, miter_assert miter_assert_flatten )) ...@@ -138,7 +138,9 @@ $(eval $(call template,miter_assert, miter_assert miter_assert_flatten ))
$(eval $(call template,miter_assert_assume, miter_assert miter_assert_flatten )) $(eval $(call template,miter_assert_assume, miter_assert miter_assert_flatten ))
#sat #sat
$(eval $(call template,sat, sat_dump_cnf sat_dump_json sat_dump_vcd sat_initsteps sat_maxsteps sat_max sat_prove_x sat_set_all_undef_at sat_set_all_undef sat_set_any_undef_at sat_set_any_undef sat_set_def_at sat_set_def sat_set_init sat_set sat_show sat_stepsize sat_tempinduct_skip sat_unset_at )) #sat_tempinduct_def sat_tempinduct_tempinduct_def
#ERROR: Assert `!undef_mode || model_undef' failed in ./kernel/satgen.h:90.
$(eval $(call template,sat, sat_dump_cnf sat_dump_json sat_dump_vcd sat_initsteps sat_maxsteps sat_max sat_prove_x sat_set_all_undef_at sat_set_all_undef sat_set_any_undef_at sat_set_any_undef sat_set_def_at sat_set_def sat_set_init sat_set sat_show sat_stepsize sat_tempinduct_skip sat_unset_at sat_set_at sat_seq sat_prove_skip sat_timeout sat_prove sat_tempinduct sat sat_all sat_ignore_unknown_cells sat_enable_undef sat_max_undef sat_show_inputs sat_show_outputs sat_show_ports sat_show_regs sat_show_public sat_show_all sat_set_assumes sat_set_init_undef sat_set_init_def sat_set_init_zero sat_tempinduct_baseonly sat_tempinduct_inductonly sat_verify sat_verify_no_timeout sat_falsify sat_falsify_no_timeout sat_prove_asserts sat_tempinduct_tempinduct_baseonly sat_set_def_inputs sat_tempinduct_baseonly_maxsteps ))
#sim #sim
$(eval $(call template,sim,sim sim_a sim_clock sim_d sim_n sim_rstlen sim_vcd sim_w sim_zinit )) $(eval $(call template,sim,sim sim_a sim_clock sim_d sim_n sim_rstlen sim_vcd sim_w sim_zinit ))
...@@ -151,4 +153,23 @@ $(eval $(call template,splitnets_logic, splitnets splitnets_format splitnets_por ...@@ -151,4 +153,23 @@ $(eval $(call template,splitnets_logic, splitnets splitnets_format splitnets_por
#splice #splice
$(eval $(call template,splice, splice splice_sel_by_cell splice_sel_by_wire splice_sel_any_bit splice_wires splice_no_outputs splice_port splice_no_port )) $(eval $(call template,splice, splice splice_sel_by_cell splice_sel_by_wire splice_sel_any_bit splice_wires splice_no_outputs splice_port splice_no_port ))
#supercover
$(eval $(call template,supercover, supercover))
#rmports
$(eval $(call template,rmports, rmports))
#check
$(eval $(call template,check, check check_noinit check_initdrv check_assert))
#design
$(eval $(call template,design, design_import design_copy_from design_copy_to design_as))
#log
$(eval $(call template,log, log log_stdout log_stderr log_nolog log_n))
#tee
$(eval $(call template,tee, tee))
.PHONY: all clean .PHONY: all clean
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
);
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));
`else
assign {cout,A} = cin - y * x;
`endif
endmodule
module middle
(
input x,
input y,
output o
);
assign o = x + y;
endmodule
...@@ -10,11 +10,16 @@ module top ...@@ -10,11 +10,16 @@ module top
parameter X = 1; parameter X = 1;
wire o; wire o;
initial A = 0;
initial cout = 0;
`ifndef BUG `ifndef BUG
always @(posedge cin) always @(posedge cin)
A <= o; A <= o;
//assign cout = cin? y : x; assign cout = cin? y : x;
middle u_mid (.x(x),.o(o)); middle u_mid (.x(x),.o(o));
u_rtl inst_u_rtl (.x(x),.o(o)); u_rtl inst_u_rtl (.x(x),.o(o));
......
read_verilog -sv ../top.v
proc
tee -o result.log check
read_verilog -sv ../top.v
proc
tee -o result.log check -assert
read_verilog -sv ../top.v
proc
tee -o result.log check -initdrv
read_verilog -sv ../top.v
proc
tee -o result.log check -noinit
read_verilog -sv ../top.v
proc
design -save first
tee -o result.log design -copy-from first -as top_2 top
tee -o result.log design -copy-to first -as top_2 top
read_verilog -sv ../top.v
proc
design -save first
tee -o result.log design -copy-from first top
read_verilog -sv ../top.v
proc
design -save first
tee -o result.log design -copy-to first top
read_verilog -sv ../top.v
proc
design -save first
tee -o result.log design -import first top
tee -o result.log log "OK"
tee -o result.log log -n "OK"
tee -o result.log log -nolog "OK"
tee -o result.log log -stderr "OK"
tee -o result.log log -stdout "OK"
read_verilog ../top.v
proc
tee -o result.log rmports
read_verilog ../top.v
proc
tee -o result.log sat middle
read_verilog ../top.v
proc
tee -o result.log sat -ignore_unknown_cells -all top
read_verilog ../top.v
proc
tee -o result.log sat -enable_undef middle
read_verilog ../top.v
proc
tee -o result.log sat -prove x 1 -falsify middle
read_verilog ../top.v
proc
tee -o result.log sat -prove x 1 -falsify-no-timeout middle
read_verilog ../top.v
proc
tee -o result.log sat -ignore-div-by-zero middle
read_verilog ../top.v
proc
tee -o result.log sat -ignore_unknown_cells top
read_verilog ../top.v
proc
tee -o result.log sat -max_undef middle
read_verilog ../top.v
proc
tee -o result.log sat -ignore_unknown_cells -prove x 1 top
read_verilog ../top.v
proc
tee -o result.log sat -prove-asserts middle
read_verilog ../top.v
proc
tee -o result.log sat -prove-skip 1 -seq 2 middle
read_verilog ../top.v
proc
tee -o result.log sat -seq 1 middle
read_verilog ../top.v
proc
tee -o result.log sat -set-assumes middle
read_verilog ../top.v
proc
tee -o result.log sat -set-at 1 x 3 middle
read_verilog ../top.v
proc
tee -o result.log sat -set-def-inputs middle
read_verilog ../top.v
proc
tee -o result.log sat -set-init-def middle
read_verilog ../top.v
proc
tee -o result.log sat -set-init-undef middle
read_verilog ../top.v
proc
tee -o result.log sat -set-init-zero middle
read_verilog ../top.v
proc
tee -o result.log sat -show-all middle
read_verilog ../top.v
proc
tee -o result.log sat -show-inputs middle
read_verilog ../top.v
proc
tee -o result.log sat -show-outputs middle
read_verilog ../top.v
proc
tee -o result.log sat -show-ports middle
read_verilog ../top.v
proc
tee -o result.log sat -show-public middle
read_verilog ../top.v
proc
tee -o result.log sat -ignore_unknown_cells -show-regs top
read_verilog ../top.v
proc
tee -o result.log sat -prove x 1 -tempinduct middle
read_verilog ../top.v
proc
tee -o result.log sat -prove x 1 -tempinduct-baseonly middle
read_verilog ../top.v
proc
tee -o result.log sat -prove x 1 -tempinduct-baseonly -maxsteps 1 middle
read_verilog ../top.v
proc
tee -o result.log sat -prove x 1 -tempinduct-def middle
read_verilog ../top.v
proc
tee -o result.log sat -prove x 1 -tempinduct-inductonly middle
read_verilog ../top.v
proc
tee -o result.log sat -prove x 1 -tempinduct -tempinduct-baseonly middle
read_verilog ../top.v
proc
tee -o result.log sat -prove x 1 -tempinduct -tempinduct-def middle
read_verilog ../top.v
proc
tee -o result.log sat -timeout 0 -ignore_unknown_cells top
read_verilog ../top.v
proc
tee -o result.log sat -verify -ignore_unknown_cells -show x,y -set x y -set x 1 top
read_verilog ../top.v
proc
tee -o result.log sat -verify-no-timeout -ignore_unknown_cells -show x,y -set x y -set x 1 top
read_verilog ../top.v
proc
tee -o result.log supercover
read_verilog ../top.v
proc
tee -q -o result.log -a result2.log ls
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
...@@ -8,7 +8,7 @@ opt_clean ...@@ -8,7 +8,7 @@ opt_clean
opt opt
wreduce wreduce
alumacc alumacc
share share -aggressive -force
opt opt
fsm fsm
opt -fast opt -fast
......
...@@ -124,5 +124,37 @@ $(eval $(call template,flowmap_mem,flowmap flowmap_cells flowmap_debug_relax flo ...@@ -124,5 +124,37 @@ $(eval $(call template,flowmap_mem,flowmap flowmap_cells flowmap_debug_relax flo
#iopadmap #iopadmap
$(eval $(call template,iopadmap,iopadmap)) $(eval $(call template,iopadmap,iopadmap))
#tribuf
$(eval $(call template,tribuf,tribuf tribuf_top tribuf_merge_top tribuf_logic_top tribuf_merge_logic_top))
#expose
$(eval $(call template,expose,expose_cut expose_input expose_evert expose_sep expose_shared expose_dff expose_evert_dff expose_evert_shared expose_evert_dff_shared))
$(eval $(call template,expose_dff,expose_cut expose_input expose_evert expose_sep expose_shared expose_dff expose_evert_dff expose_evert_shared expose_evert_dff_shared))
#opt_demorgan
$(eval $(call template,opt_demorgan,opt_demorgan))
$(eval $(call template,opt_demorgan_reduce,opt_demorgan))
#fsm_expand
$(eval $(call template,fsm_expand, fsm_expand fsm_expand_full))
#fsm_export
$(eval $(call template,fsm_export, fsm_export fsm_export_noauto fsm_export_o fsm_export_origenc))
#fsm_recode
$(eval $(call template,fsm_recode, fsm_recode fsm_recode_encoding_binary fsm_recode_encoding_binary_twice fsm_recode_encoding_one_hot fsm_recode_fm_set_fsm_file fsm_recode_all_opt))
#fsm command
$(eval $(call template,fsm_command, fsm_command fsm_fm_set_fsm_file fsm_encfile fsm_encoding_binary fsm_encoding_one-hot fsm_encoding_auto fsm_encoding_none fsm_encoding_user fsm_encoding_unknown fsm_nodetect fsm_norecode fsm_nomap fsm_command_expand fsm_fullexpand fsm_command_export ))
#share
$(eval $(call template,share, share share_force share_aggressive share_fast share_limit))
$(eval $(call template,share_shr, share share_force share_aggressive share_fast share_limit))
$(eval $(call template,share_macc, share_force_macc share_aggressive_macc share_fast_macc share_limit_macc share_macc))
#+ yosys -ql yosys.log ../../scripts/share_force.ys
#ERROR: Abort in passes/opt/share.cc:724.
#make: *** [Makefile:152: share_fsm/work_share_force/.stamp] Error 1
#$(eval $(call template,share_fsm, share share_force share_aggressive share_fast share_limit))
.PHONY: all clean .PHONY: all clean
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 dinA = 0;
wire doutB;
top uut (
.clk (clk ),
.a (dinA ),
.b (doutB )
);
always @(posedge clk) begin
#3;
dinA <= !dinA;
end
assert_dff ff_test(.clk(clk), .test(doutB), .pat(1'b0));
endmodule
module dffr
( input d, clk, rst, output reg q );
always @( posedge clk )
if ( rst )
q <= 1'b0;
else
q <= d;
endmodule
module top (
input clk,
input a,
output b
);
dffr u_dffr (
.clk (clk),
`ifndef BUG
.rst (1'b1),
`else
.rst (1'b0),
`endif
.d (a ),
.q (b )
);
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 dinA = 0;
wire doutB;
top uut (
.clk (clk ),
.a (dinA ),
.b (doutB )
);
always @(posedge clk) begin
//#3;
dinA <= !dinA;
end
assert_dff ff_test(.clk(clk), .test(doutB), .pat(!dinA));
endmodule
module dffr
( input d, clk, output reg q );
always @( posedge clk )
q <= d;
endmodule
module top (
input clk,
input a,
output b
);
dffr u_dffr (
.clk (clk),
`ifndef BUG
.d (a ),
`else
.d (1'b1 ),
`endif
.q (b )
);
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
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
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
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
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
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
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
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
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
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 dinA = 0;
wire doutB;
top uut (
.clk (clk ),
.a (dinA ),
.b (doutB )
);
always @(posedge clk) begin
#3;
dinA <= !dinA;
end
assert_dff ff_test(.clk(clk), .test(doutB), .pat(1'b0));
endmodule
module dffr
( input d, clk, rst, output reg q );
always @( posedge clk )
if ( rst )
q <= 1'b0;
else
q <= d;
endmodule
module top (
input clk,
input a,
output b
);
dffr u_dffr (
.clk (clk),
`ifndef BUG
.rst (1'b1),
`else
.rst (1'b0),
`endif
.d (a ),
.q (b )
);
endmodule
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 = 0;
wire carryout = 0;
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
module top
(
input x,
input [2:0] y,
input [2:0] cin,
output A,
output cout
);
wire A1,cout1;
wire [2:0] n_y;
wire [2:0] n_cin;
// initial begin
// A = 0;
// cout = 0;
// end
assign n_y[0] = ~y[0];
assign n_y[1] = y[1];
assign n_y[2] = ~y[2];
assign n_cin[0] = ~cin[0];
assign n_cin[1] = cin[1];
assign n_cin[2] = ~cin[2];
`ifndef BUG
assign A1 = n_y + &(~cin);
assign cout1 = cin ? |n_y : ^A;
assign A = A1|y~&(~cin)~^A1;
assign cout = cout1&cin~|(~y);
`else
assign {cout,A} = 1'bZ;
`endif
endmodule
read_verilog ../top.v
synth -top top
proc
flatten
opt
opt_rmdff
expose -cut
write_verilog synth.v
read_verilog ../top.v
synth -top top
proc
flatten
opt
opt_rmdff
expose -dff
write_verilog synth.v
read_verilog ../top.v
expose -evert
synth -top top
expose -evert
proc
expose -evert
flatten
opt
opt_rmdff
expose -evert
write_verilog synth.v
read_verilog ../top.v
proc
expose -evert-dff
synth -top top
expose -evert-dff
proc
flatten
opt
opt_rmdff
expose -evert-dff
write_verilog synth.v
read_verilog ../top.v
proc
expose -evert-dff -shared
synth -top top
proc
flatten
opt
opt_rmdff
expose -evert-dff
design -reset
read_verilog ../top.v
proc
write_verilog synth.v
read_verilog ../top.v
synth -top top
proc
flatten
opt
opt_rmdff
expose -evert -shared
write_verilog synth.v
read_verilog ../top.v
synth -top top
expose -input
proc
flatten
opt
opt_rmdff
expose -input
design -reset
read_verilog ../top.v
synth -top top
write_verilog synth.v
read_verilog ../top.v
synth -top top
proc
flatten
opt
opt_rmdff
expose -sep |
write_verilog synth.v
read_verilog ../top.v
synth -top top
proc
flatten
opt
opt_rmdff
expose -shared
write_verilog synth.v
read_verilog ../top.v
proc
fsm
synth -top top
write_verilog synth.v
read_verilog ../top.v
proc
fsm -expand
synth -top top
write_verilog synth.v
read_verilog ../top.v
proc
fsm -export
synth -top top
write_verilog synth.v
read_verilog ../top.v
proc
fsm -encfile fsm.fsm
synth -top top
write_verilog synth.v
read_verilog ../top.v
proc
fsm_detect
fsm_extract
fsm_recode -encoding binary
fsm_map
fsm
fsm -encoding binary
fsm -encoding auto
synth -top top
write_verilog synth.v
read_verilog ../top.v
proc
fsm -encoding binary
synth -top top
write_verilog synth.v
read_verilog ../top.v
proc
fsm_detect
fsm_extract
fsm_recode -encoding binary
fsm_map
fsm
fsm -encoding binary
fsm -encoding none
synth -top top
write_verilog synth.v
read_verilog ../top.v
proc
fsm -encoding one-hot
synth -top top
write_verilog synth.v
read_verilog ../top.v
proc
fsm_detect
fsm_extract
fsm_recode -encoding binary
fsm_map
fsm
fsm -encoding binary
fsm -encoding unknown
synth -top top
write_verilog synth.v
read_verilog ../top.v
proc
fsm_detect
fsm_extract
fsm_recode -encoding binary
fsm_map
fsm
fsm -encoding binary
fsm -encoding user
synth -top top
write_verilog synth.v
read_verilog ../top.v
proc
fsm_detect
fsm_extract
fsm_expand
opt
fsm_opt
synth -top top
write_verilog synth.v
read_verilog ../top.v
proc
fsm_detect
fsm_extract
fsm_expand -full
opt
fsm_opt
synth -top top
write_verilog synth.v
read_verilog ../top.v
proc
fsm_detect
fsm_extract
fsm_expand -full
opt
fsm_opt
synth -top top
write_verilog synth.v
read_verilog ../top.v
proc
fsm_detect
fsm_extract
fsm_export
opt
fsm_opt
synth -top top
write_verilog synth.v
read_verilog ../top.v
proc
fsm_detect
fsm_extract
fsm_export -noauto
opt
fsm_opt
synth -top top
write_verilog synth.v
read_verilog ../top.v
proc
fsm_detect
fsm_extract
fsm_export -o fsm.kiss2
opt
fsm_opt
synth -top top
write_verilog synth.v
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