Commit 2a7be41f by SergeyDegtyar

Review and update tests in 'equiv' test group.

parent c0b775eb
*/work_*/ */work_*/
/.stamp /.stamp
/run-test.mk
all: work PYTHON_EXECUTABLE := $(shell if python3 -c ""; then echo "python3"; else echo "python"; fi)
touch .stamp
clean:: all:: run-test.mk
rm -f .stamp @touch .stamp
@$(MAKE) -f run-test.mk
clean:: run-test.mk
@rm -f .stamp
@$(MAKE) -f run-test.mk clean
define template run-test.mk: ../generate.py
$(foreach design,$(1), @$(PYTHON_EXECUTABLE) ../generate.py > run-test.mk
$(foreach script,$(2),
work:: $(design)/work_$(script)/.stamp
$(design)/work_$(script)/.stamp:
bash run.sh $(design) $(script)
clean::
rm -rf $(design)/work_$(script)
))
endef
#equiv_make
$(eval $(call template,equiv_make,equiv_make equiv_make_inames equiv_make_blacklist equiv_make_encfile))
$(eval $(call template,equiv_make_fsm,equiv_make_encfile equiv_make_encfile_fsm))
$(eval $(call template,equiv_make_error,equiv_make_synth_error equiv_make_cant_open_encfile equiv_make_cant_open_blacklist equiv_make_cant_find_gate_mod equiv_make_cant_find_gold_mod equiv_make_invalid_num_of_args equiv_make_cant_match equiv_make_cant_match_gold_to_gate equiv_make_equiv_mod_already_exists equiv_make_gold_mod_contains_proc equiv_make_gate_mod_contains_proc))
$(eval $(call template,equiv_make_fsm_error,equiv_make_redefenition_of_signal))
#equiv_simple
$(eval $(call template,equiv_simple,equiv_simple equiv_simple_v equiv_simple_undef equiv_simple_short equiv_simple_seq equiv_simple_nogroup))
$(eval $(call template,equiv_simple_fsm,equiv_simple equiv_simple_v equiv_simple_undef equiv_simple_short equiv_simple_seq equiv_simple_nogroup))
#equiv_status
$(eval $(call template,equiv_status,equiv_status))
$(eval $(call template,equiv_status_error,equiv_status_assert))
#equiv_struct
$(eval $(call template,equiv_struct,equiv_struct equiv_struct_fwd equiv_struct_fwonly equiv_struct_icells equiv_struct_maxiter))
#equiv_remove
$(eval $(call template,equiv_remove,equiv_remove equiv_remove_gold equiv_remove_gate ))
$(eval $(call template,equiv_remove_error,equiv_remove_gold_gate ))
#equiv_purge
$(eval $(call template,equiv_purge,equiv_purge ))
#equiv_miter
#equiv_miter_invalid_num_of_args - no error
$(eval $(call template,equiv_miter,equiv_miter equiv_miter_trigger equiv_miter_cmp equiv_miter_assert equiv_miter_undef))
$(eval $(call template,equiv_miter_error,equiv_miter_miter_module_already_exists equiv_miter_one_module_must_be_selected))
#equiv_mark
$(eval $(call template,equiv_mark,equiv_mark ))
#equiv_induct
$(eval $(call template,equiv_induct,equiv_induct equiv_induct_undef equiv_induct_seq ))
#equiv_add
$(eval $(call template,equiv_add,equiv_add equiv_add_try ))
# ERROR: This command must be executed in module context!
#equiv_add_cant_find_gold_cell equiv_add_cant_find_gate_cell equiv_add_invalid_number_of_args
$(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 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 .PHONY: all clean
module assert_dff(input clk, input test, input pat);
always @(posedge clk)
begin
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
...@@ -13,6 +13,3 @@ equiv_make gold gate equiv ...@@ -13,6 +13,3 @@ equiv_make gold gate equiv
design -save something design -save something
design -push design -push
equiv_add gold gate equiv_add gold gate
design -reset
read_verilog ../top.v
write_verilog synth.v
ERROR: This command must be executed in module context!
...@@ -11,6 +11,3 @@ design -copy-from gold -as gold top ...@@ -11,6 +11,3 @@ design -copy-from gold -as gold top
design -copy-from gate -as gate top design -copy-from gate -as gate top
equiv_make gold gate equiv equiv_make gold gate equiv
equiv_add -try gold gate equiv_add -try gold gate
design -reset
read_verilog ../top.v
write_verilog synth.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 rst;
wire f;
top uut ( .clk(clk),
.rst(rst),
.count(f));
initial begin
rst <= 1;
#5
rst <= 0;
end
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
`timescale 1ns/10ps
`celldefine
module NOR2_X0X2 (A, B, Y);
input A ;
input B ;
output Y ;
wire I0_out;
or (I0_out, A, B);
not (Y, I0_out);
endmodule
`endcelldefine
`timescale 1ns/10ps
`celldefine
module DFFARAS_X2X2(Q,QN,D,CLK,SN,RN);
input D,CLK,SN,RN;
output Q,QN;
reg Q,QN;
always @ (posedge CLK or negedge RN or negedge SN)
begin
if (!RN) begin
Q<=1'b0;
QN<=1'b1;
end
else if (!SN) begin
Q<=1'b1;
QN<=1'b0;
end
else begin
Q<=D;
QN<=!D;
end
end
endmodule
`endcelldefine
`timescale 1ns/10ps
`celldefine
module TIEHL (tiehi, tielo);
output tiehi ;
output tielo ;
assign tiehi = 1'b1;
assign tielo = 1'b0;
endmodule
`endcelldefine
`timescale 1ns/10ps
`celldefine
module INV_X2X2 (A, Y);
input A ;
output Y ;
not (Y, A);
/*
specify
// delay parameters
specparam
tplhl$A$Y = 0.23:0.23:0.23,
tphlh$A$Y = 0.33:0.33:0.33;
// path delays
(A *> Y) = (tphlh$A$Y, tplhl$A$Y);
endspecify
*/
endmodule
`endcelldefine
/* Generated by Yosys 0.7 (git sha1 UNKNOWN, clang 3.4.2 -fPIC -Os) */
(* src = "top.v:1" *)
module top(clk, rst, count);
(* src = "top.v:3" *)
wire _0_;
wire _1_;
wire _2_;
(* src = "top.v:1" *)
input clk;
(* src = "top.v:1" *)
output count;
(* src = "top.v:1" *)
input rst;
INV_X2X2 _3_ (
.A(rst),
.Y(_1_)
);
TIEHL _4_ (
.tiehi(_2_)
);
DFFARAS_X2X2 _5_ (
.CLK(clk),
.D(_0_),
.Q(count),
.QN(_0_),
.RN(_1_),
.SN(_2_)
);
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 rst;
wire f;
top uut ( .clk(clk),
.rst(rst),
.count(f));
initial begin
rst <= 1;
#5
rst <= 0;
end
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
module top(input wire clk,rst,output reg count);
always @(posedge clk or posedge rst)begin
if(rst)
count <= 0;
else
count <= count + 1'b1;
end
endmodule
...@@ -11,6 +11,3 @@ design -copy-from gold -as gold top ...@@ -11,6 +11,3 @@ design -copy-from gold -as gold top
design -copy-from gate -as gate top design -copy-from gate -as gate top
equiv_make gold gate equiv equiv_make gold gate equiv
equiv_induct equiv_induct
design -reset
read_verilog ../top.v
write_verilog synth.v
...@@ -11,6 +11,3 @@ design -copy-from gold -as gold top ...@@ -11,6 +11,3 @@ design -copy-from gold -as gold top
design -copy-from gate -as gate top design -copy-from gate -as gate top
equiv_make gold gate equiv equiv_make gold gate equiv
equiv_induct -seq 3 equiv_induct -seq 3
design -reset
read_verilog ../top.v
write_verilog synth.v
...@@ -11,6 +11,3 @@ design -copy-from gold -as gold top ...@@ -11,6 +11,3 @@ design -copy-from gold -as gold top
design -copy-from gate -as gate top design -copy-from gate -as gate top
equiv_make gold gate equiv equiv_make gold gate equiv
equiv_induct -undef equiv_induct -undef
design -reset
read_verilog ../top.v
write_verilog synth.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 rst;
wire f;
top uut ( .clk(clk),
.rst(rst),
.count(f));
initial begin
rst <= 1;
#5
rst <= 0;
end
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
...@@ -10,6 +10,3 @@ design -stash gate ...@@ -10,6 +10,3 @@ design -stash gate
design -copy-from gold -as gold top design -copy-from gold -as gold top
design -copy-from gate -as gate top design -copy-from gate -as gate top
equiv_make gold gate equiv equiv_make gold gate equiv
design -reset
read_verilog ../top.v
write_verilog synth.v
...@@ -10,6 +10,3 @@ design -stash gate ...@@ -10,6 +10,3 @@ design -stash gate
design -copy-from gold -as gold top design -copy-from gold -as gold top
design -copy-from gate -as gate top design -copy-from gate -as gate top
equiv_make -blacklist ../blacklist.txt gold gate equiv equiv_make -blacklist ../blacklist.txt gold gate equiv
design -reset
read_verilog ../top.v
write_verilog synth.v
...@@ -11,7 +11,3 @@ design -stash gate ...@@ -11,7 +11,3 @@ design -stash gate
design -copy-from gold -as gold top design -copy-from gold -as gold top
design -copy-from gate -as gate top design -copy-from gate -as gate top
equiv_make gold gat equiv equiv_make gold gat equiv
design -reset
read_verilog ../top.v
proc
write_verilog synth.v
...@@ -11,7 +11,3 @@ design -stash gate ...@@ -11,7 +11,3 @@ design -stash gate
design -copy-from gold -as gold top design -copy-from gold -as gold top
design -copy-from gate -as gate top design -copy-from gate -as gate top
equiv_make gol gat equiv equiv_make gol gat equiv
design -reset
read_verilog ../top.v
proc
write_verilog synth.v
ERROR: Can't match gate port `rst_gate' to a gold port.
...@@ -10,7 +10,3 @@ design -stash gate ...@@ -10,7 +10,3 @@ design -stash gate
design -copy-from gold -as gold top design -copy-from gold -as gold top
design -copy-from gate -as gate top design -copy-from gate -as gate top
equiv_make gold gate equiv equiv_make gold gate equiv
design -reset
read_verilog ../top.v
proc
write_verilog synth.v
ERROR: Can't match gold port `set_gold' to a gate port.
...@@ -10,7 +10,3 @@ design -stash gate ...@@ -10,7 +10,3 @@ design -stash gate
design -copy-from gold -as gold top design -copy-from gold -as gold top
design -copy-from gate -as gate top design -copy-from gate -as gate top
equiv_make gold gate equiv equiv_make gold gate equiv
design -reset
read_verilog ../top.v
proc
write_verilog synth.v
ERROR: Can't open blacklist file '../black.txt'!
...@@ -10,6 +10,3 @@ design -stash gate ...@@ -10,6 +10,3 @@ design -stash gate
design -copy-from gold -as gold top design -copy-from gold -as gold top
design -copy-from gate -as gate top design -copy-from gate -as gate top
equiv_make -blacklist ../black.txt gold gate equiv equiv_make -blacklist ../black.txt gold gate equiv
design -reset
read_verilog ../top.v
write_verilog synth.v
ERROR: Can't open encfile 'encfile111.fsm'!
...@@ -11,7 +11,3 @@ design -stash gate ...@@ -11,7 +11,3 @@ design -stash gate
design -copy-from gold -as gold top design -copy-from gold -as gold top
design -copy-from gate -as gate top design -copy-from gate -as gate top
equiv_make -encfile encfile111.fsm gold gate equiv equiv_make -encfile encfile111.fsm gold gate equiv
design -reset
read_verilog ../top.v
proc
write_verilog synth.v
...@@ -11,7 +11,3 @@ design -stash gate ...@@ -11,7 +11,3 @@ design -stash gate
design -copy-from gold -as gold top design -copy-from gold -as gold top
design -copy-from gate -as gate top design -copy-from gate -as gate top
equiv_make -encfile encfile.fsm gold gate equiv equiv_make -encfile encfile.fsm gold gate equiv
design -reset
read_verilog ../top.v
proc
write_verilog synth.v
read_verilog ../top.v read_verilog ../top_fsm.v
proc proc
fsm_detect fsm_detect
fsm_extract fsm_extract
fsm_recode -encfile encfile.fsm fsm_recode -encfile encfile.fsm
design -stash gold design -stash gold
read_verilog ../synth_top.v read_verilog ../synth_top_fsm.v
read_verilog ../logic.v read_verilog ../logic_fsm.v
proc proc
design -stash gate design -stash gate
design -copy-from gold -as gold FSM design -copy-from gold -as gold FSM
design -copy-from gate -as gate FSM design -copy-from gate -as gate FSM
equiv_make -blacklist ../blacklist.txt -inames -encfile encfile.fsm gold gate equiv equiv_make -blacklist ../blacklist.txt -inames -encfile encfile.fsm gold gate equiv
design -reset
read_verilog ../top.v
proc
write_verilog synth.v
...@@ -11,7 +11,3 @@ design -copy-from gold -as gold top ...@@ -11,7 +11,3 @@ design -copy-from gold -as gold top
design -copy-from gate -as gate top design -copy-from gate -as gate top
equiv_make gold gate equiv equiv_make gold gate equiv
equiv_make gold gate equiv equiv_make gold gate equiv
design -reset
read_verilog ../top.v
proc
write_verilog synth.v
ERROR: Gate module contains memories or processes. Run 'memory' or 'proc' respectively.
...@@ -9,7 +9,3 @@ design -stash gold ...@@ -9,7 +9,3 @@ design -stash gold
design -copy-from gold -as gold top design -copy-from gold -as gold top
design -copy-from gate -as gate top design -copy-from gate -as gate top
equiv_make gold gate equiv equiv_make gold gate equiv
design -reset
read_verilog ../top.v
proc
write_verilog synth.v
ERROR: Gold module contains memories or processes. Run 'memory' or 'proc' respectively.
...@@ -9,7 +9,3 @@ design -stash gate ...@@ -9,7 +9,3 @@ design -stash gate
design -copy-from gold -as gold top design -copy-from gold -as gold top
design -copy-from gate -as gate top design -copy-from gate -as gate top
equiv_make gold gate equiv equiv_make gold gate equiv
design -reset
read_verilog ../top.v
proc
write_verilog synth.v
...@@ -10,6 +10,3 @@ design -stash gate ...@@ -10,6 +10,3 @@ design -stash gate
design -copy-from gold -as gold top design -copy-from gold -as gold top
design -copy-from gate -as gate top design -copy-from gate -as gate top
equiv_make -inames gold gate equiv equiv_make -inames gold gate equiv
design -reset
read_verilog ../top.v
write_verilog synth.v
...@@ -11,7 +11,3 @@ design -stash gate ...@@ -11,7 +11,3 @@ design -stash gate
design -copy-from gold -as gold top design -copy-from gold -as gold top
design -copy-from gate -as gate top design -copy-from gate -as gate top
equiv_make gold gate equiv_make gold gate
design -reset
read_verilog ../top.v
proc
write_verilog synth.v
ERROR: Re-definition of signal '\\st' in encfile '../encfile.fsm'!
read_verilog ../top.v read_verilog ../top_fsm.v
proc proc
fsm_detect fsm_detect
fsm_extract fsm_extract
fsm_recode -encfile encfile.fsm fsm_recode -encfile encfile.fsm
design -stash gold design -stash gold
read_verilog ../synth_top.v read_verilog ../synth_top_fsm.v
read_verilog ../logic.v read_verilog ../logic_fsm.v
proc proc
design -stash gate design -stash gate
design -copy-from gold -as gold top design -copy-from gold -as gold top
design -copy-from gate -as gate top design -copy-from gate -as gate top
equiv_make -encfile ../encfile_redef.fsm -encfile ../encfile.fsm gold gate equiv equiv_make -encfile ../encfile_redef.fsm -encfile ../encfile.fsm gold gate equiv
design -reset
read_verilog ../top.v
proc
write_verilog synth.v
ERROR: Syntax error in encfile '../encfile_synth_error.fsm'!
...@@ -11,7 +11,3 @@ design -stash gate ...@@ -11,7 +11,3 @@ design -stash gate
design -copy-from gold -as gold top design -copy-from gold -as gold top
design -copy-from gate -as gate top design -copy-from gate -as gate top
equiv_make -encfile ../encfile_synth_error.fsm gold gate equiv equiv_make -encfile ../encfile_synth_error.fsm gold gate equiv
design -reset
read_verilog ../top.v
proc
write_verilog synth.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 rst;
wire f;
top uut ( .clk(clk),
.rst(rst),
.count(f));
initial begin
rst <= 1;
#5
rst <= 0;
end
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
`timescale 1ns/10ps
`celldefine
module NOR2_X0X2 (A, B, Y);
input A ;
input B ;
output Y ;
wire I0_out;
or (I0_out, A, B);
not (Y, I0_out);
endmodule
`endcelldefine
`timescale 1ns/10ps
`celldefine
module DFFARAS_X2X2(Q,QN,D,CLK,SN,RN);
input D,CLK,SN,RN;
output Q,QN;
reg Q,QN;
always @ (posedge CLK or negedge RN or negedge SN)
begin
if (!RN) begin
Q<=1'b0;
QN<=1'b1;
end
else if (!SN) begin
Q<=1'b1;
QN<=1'b0;
end
else begin
Q<=D;
QN<=!D;
end
end
endmodule
`endcelldefine
`timescale 1ns/10ps
`celldefine
module TIEHL (tiehi, tielo);
output tiehi ;
output tielo ;
assign tiehi = 1'b1;
assign tielo = 1'b0;
endmodule
`endcelldefine
`timescale 1ns/10ps
`celldefine
module INV_X2X2 (A, Y);
input A ;
output Y ;
not (Y, A);
/*
specify
// delay parameters
specparam
tplhl$A$Y = 0.23:0.23:0.23,
tphlh$A$Y = 0.33:0.33:0.33;
// path delays
(A *> Y) = (tphlh$A$Y, tplhl$A$Y);
endspecify
*/
endmodule
`endcelldefine
/* Generated by Yosys 0.7 (git sha1 UNKNOWN, clang 3.4.2 -fPIC -Os) */
(* src = "top.v:1" *)
module top(clk, rst, count);
(* src = "top.v:3" *)
wire _0_;
wire _1_;
wire _2_;
(* src = "top.v:1" *)
input clk;
(* src = "top.v:1" *)
output count;
(* src = "top.v:1" *)
input rst;
INV_X2X2 _3_ (
.A(rst),
.Y(_1_)
);
TIEHL _4_ (
.tiehi(_2_)
);
DFFARAS_X2X2 _5_ (
.CLK(clk),
.D(_0_),
.Q(count),
.QN(_0_),
.RN(_1_),
.SN(_2_)
);
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 rst;
wire f;
top uut ( .clk(clk),
.rst(rst),
.count(f));
initial begin
rst <= 1;
#5
rst <= 0;
end
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
module top(input wire clk,rst,output reg count);
always @(posedge clk or posedge rst)begin
if(rst)
count <= 0;
else
count <= count + 1'b1;
end
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 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
.fsm FSM st
.map 0000 -------------1
.map 1000 ------------1-
.map 1010 ------------1-
.map 1010 -------------1
.map 0100 -----------1--
.map 1100 ----------1---
.map 0010 ---------1----
.map 1010 --------1-----
.map 0110 -------1------
.map 0001 ------1-------
.map 1001 -----1--------
.map 0101 ----1---------
.map 1101 ---1----------
.map 0011 --1-----------
.map 1011 -1------------
.map 0111 1-------------
.map 1000 1-----1-------
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
...@@ -11,6 +11,3 @@ design -copy-from gold -as gold top ...@@ -11,6 +11,3 @@ design -copy-from gold -as gold top
design -copy-from gate -as gate top design -copy-from gate -as gate top
equiv_make gold gate equiv equiv_make gold gate equiv
equiv_mark equiv_mark
design -reset
read_verilog ../top.v
write_verilog synth.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 rst;
wire f;
top uut ( .clk(clk),
.rst(rst),
.count(f));
initial begin
rst <= 1;
#5
rst <= 0;
end
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
ERROR: Exactly one module must be selected for 'equiv_miter'!
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 rst;
wire f;
top uut ( .clk(clk),
.rst(rst),
.count(f));
initial begin
rst <= 1;
#5
rst <= 0;
end
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
`timescale 1ns/10ps
`celldefine
module NOR2_X0X2 (A, B, Y);
input A ;
input B ;
output Y ;
wire I0_out;
or (I0_out, A, B);
not (Y, I0_out);
endmodule
`endcelldefine
`timescale 1ns/10ps
`celldefine
module DFFARAS_X2X2(Q,QN,D,CLK,SN,RN);
input D,CLK,SN,RN;
output Q,QN;
reg Q,QN;
always @ (posedge CLK or negedge RN or negedge SN)
begin
if (!RN) begin
Q<=1'b0;
QN<=1'b1;
end
else if (!SN) begin
Q<=1'b1;
QN<=1'b0;
end
else begin
Q<=D;
QN<=!D;
end
end
endmodule
`endcelldefine
`timescale 1ns/10ps
`celldefine
module TIEHL (tiehi, tielo);
output tiehi ;
output tielo ;
assign tiehi = 1'b1;
assign tielo = 1'b0;
endmodule
`endcelldefine
`timescale 1ns/10ps
`celldefine
module INV_X2X2 (A, Y);
input A ;
output Y ;
not (Y, A);
/*
specify
// delay parameters
specparam
tplhl$A$Y = 0.23:0.23:0.23,
tphlh$A$Y = 0.33:0.33:0.33;
// path delays
(A *> Y) = (tphlh$A$Y, tplhl$A$Y);
endspecify
*/
endmodule
`endcelldefine
/* Generated by Yosys 0.7 (git sha1 UNKNOWN, clang 3.4.2 -fPIC -Os) */
(* src = "top.v:1" *)
module top(clk, rst, count);
(* src = "top.v:3" *)
wire _0_;
wire _1_;
wire _2_;
(* src = "top.v:1" *)
input clk;
(* src = "top.v:1" *)
output count;
(* src = "top.v:1" *)
input rst;
INV_X2X2 _3_ (
.A(rst),
.Y(_1_)
);
TIEHL _4_ (
.tiehi(_2_)
);
DFFARAS_X2X2 _5_ (
.CLK(clk),
.D(_0_),
.Q(count),
.QN(_0_),
.RN(_1_),
.SN(_2_)
);
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 rst;
wire f;
top uut ( .clk(clk),
.rst(rst),
.count(f));
initial begin
rst <= 1;
#5
rst <= 0;
end
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
module top(input wire clk,rst,output reg count);
always @(posedge clk or posedge rst)begin
if(rst)
count <= 0;
else
count <= count + 1'b1;
end
endmodule
ERROR: This command only operates on fully selected designs!
ERROR: No optimization pass specified!
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