Skip to content

Y
yosys-tests
Unverified Commit 7d7c08ec by Miodrag Milanović Committed by GitHub
Options

Merge pull request #8 from SergeyDegtyar/master 

Add new tests to 'simple' and 'misc' groups;  Add test group for equiv_* commands.
parents 151e9a30 5b39f7c6
Showing with 3495 additions and 1 deletions
Makefile
SUBDIRS := architecture backends bigsim frontends misc regression simple
SUBDIRS := architecture backends bigsim equiv frontends misc regression simple
ifeq ($(VERIFIC),1)
export VERIFIC=1
......
equiv/.gitignore 0 → 100644
*/work_*/
/.stamp
equiv/Makefile 0 → 100644
all: work
touch .stamp
clean::
rm -f .stamp
define template
$(foreach design,$(1),
$(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))
#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))
#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 ))
#equiv_purge
$(eval $(call template,equiv_purge,equiv_purge ))
#equiv_miter
$(eval $(call template,equiv_miter,equiv_miter equiv_miter_trigger equiv_miter_cmp equiv_miter_assert equiv_miter_undef))
#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 ))
#equiv_opt
$(eval $(call template,equiv_opt,equiv_opt equiv_opt_run equiv_opt_map))
.PHONY: all clean
equiv/common.v 0 → 100644
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
equiv/equiv_add/logic.v 0 → 100644
`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
equiv/equiv_add/synth_top.v 0 → 100644
/* 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
equiv/equiv_add/testbench.v 0 → 100644
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
equiv/equiv_add/top.v 0 → 100644
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
equiv/equiv_induct/logic.v 0 → 100644
`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
equiv/equiv_induct/synth_top.v 0 → 100644
/* 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
equiv/equiv_induct/testbench.v 0 → 100644
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
equiv/equiv_induct/top.v 0 → 100644
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
equiv/equiv_make/logic.v 0 → 100644
`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
equiv/equiv_make/synth_top.v 0 → 100644
/* 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
equiv/equiv_make/testbench.v 0 → 100644
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
equiv/equiv_make/top.v 0 → 100644
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
equiv/equiv_make_fsm/logic.v 0 → 100644
module \$fsm (CLK, ARST, CTRL_IN, CTRL_OUT);
parameter NAME = "";
parameter CLK_POLARITY = 1'b1;
parameter ARST_POLARITY = 1'b1;
parameter CTRL_IN_WIDTH = 1;
parameter CTRL_OUT_WIDTH = 1;
parameter STATE_BITS = 1;
parameter STATE_NUM = 1;
parameter STATE_NUM_LOG2 = 1;
parameter STATE_RST = 0;
parameter STATE_TABLE = 1'b0;
parameter TRANS_NUM = 1;
parameter TRANS_TABLE = 4'b0x0x;
input CLK, ARST;
input [CTRL_IN_WIDTH-1:0] CTRL_IN;
output reg [CTRL_OUT_WIDTH-1:0] CTRL_OUT;
wire pos_clk = CLK == CLK_POLARITY;
wire pos_arst = ARST == ARST_POLARITY;
reg [STATE_BITS-1:0] state;
reg [STATE_BITS-1:0] state_tmp;
reg [STATE_BITS-1:0] next_state;
reg [STATE_BITS-1:0] tr_state_in;
reg [STATE_BITS-1:0] tr_state_out;
reg [CTRL_IN_WIDTH-1:0] tr_ctrl_in;
reg [CTRL_OUT_WIDTH-1:0] tr_ctrl_out;
integer i;
task tr_fetch;
input [31:0] tr_num;
reg [31:0] tr_pos;
reg [STATE_NUM_LOG2-1:0] state_num;
begin
tr_pos = (2*STATE_NUM_LOG2+CTRL_IN_WIDTH+CTRL_OUT_WIDTH)*tr_num;
tr_ctrl_out = TRANS_TABLE >> tr_pos;
tr_pos = tr_pos + CTRL_OUT_WIDTH;
state_num = TRANS_TABLE >> tr_pos;
tr_state_out = STATE_TABLE >> (STATE_BITS*state_num);
tr_pos = tr_pos + STATE_NUM_LOG2;
tr_ctrl_in = TRANS_TABLE >> tr_pos;
tr_pos = tr_pos + CTRL_IN_WIDTH;
state_num = TRANS_TABLE >> tr_pos;
tr_state_in = STATE_TABLE >> (STATE_BITS*state_num);
tr_pos = tr_pos + STATE_NUM_LOG2;
end
endtask
/*
always @(posedge pos_clk, posedge pos_arst) begin
if (pos_arst) begin
state_tmp = STATE_TABLE[STATE_BITS*(STATE_RST+1)-1:STATE_BITS*STATE_RST];
for (i = 0; i < STATE_BITS; i = i+1)
if (state_tmp[i] === 1'bz)
state_tmp[i] = 0;
state <= state_tmp;
end else begin
state_tmp = next_state;
for (i = 0; i < STATE_BITS; i = i+1)
if (state_tmp[i] === 1'bz)
state_tmp[i] = 0;
state <= state_tmp;
end
end
always @(state, CTRL_IN) begin
next_state <= STATE_TABLE[STATE_BITS*(STATE_RST+1)-1:STATE_BITS*STATE_RST];
CTRL_OUT <= 'bx;
// $display("---");
// $display("Q: %b %b", state, CTRL_IN);
for (i = 0; i < TRANS_NUM; i = i+1) begin
tr_fetch(i);
// $display("T: %b %b -> %b %b [%d]", tr_state_in, tr_ctrl_in, tr_state_out, tr_ctrl_out, i);
casez ({state, CTRL_IN})
{tr_state_in, tr_ctrl_in}: begin
// $display("-> %b %b <- MATCH", state, CTRL_IN);
{next_state, CTRL_OUT} <= {tr_state_out, tr_ctrl_out};
end
endcase
end
end
*/
endmodule
equiv/equiv_make_fsm/synth_top.v 0 → 100644
/* Generated by Yosys 0.8+96 (git sha1 2d73e1b6, gcc 8.2.0-7ubuntu1 -Og -fPIC) */
(* cells_not_processed = 1 *)
(* src = "top.v:1" *)
module FSM(clk, rst, en, ls, rs, stop, busy, finish);
(* src = "top.v:71" *)
wire [2:0] _00_;
(* src = "top.v:19" *)
(* unused_bits = "0 1 2 3" *)
wire [3:0] _01_;
(* src = "top.v:80" *)
wire [31:0] _02_;
(* src = "top.v:43" *)
wire _03_;
(* src = "top.v:76" *)
wire _04_;
(* src = "top.v:85" *)
wire _05_;
(* src = "top.v:85" *)
wire _06_;
(* src = "top.v:87" *)
wire _07_;
(* src = "top.v:89" *)
wire _08_;
(* src = "top.v:89" *)
wire _09_;
(* src = "top.v:39" *)
wire _10_;
(* src = "top.v:53" *)
wire _11_;
(* src = "top.v:60" *)
wire _12_;
(* src = "top.v:85" *)
wire _13_;
(* src = "top.v:89" *)
wire _14_;
wire [2:0] _15_;
wire [2:0] _16_;
(* unused_bits = "0" *)
wire _17_;
(* unused_bits = "0" *)
wire _18_;
(* unused_bits = "0" *)
wire _19_;
(* unused_bits = "0" *)
wire _20_;
(* unused_bits = "0" *)
wire _21_;
(* unused_bits = "0" *)
wire _22_;
(* unused_bits = "0" *)
wire _23_;
(* unused_bits = "0" *)
wire _24_;
(* unused_bits = "0" *)
wire _25_;
(* unused_bits = "0" *)
wire _26_;
(* unused_bits = "0" *)
wire _27_;
(* unused_bits = "0" *)
wire _28_;
(* unused_bits = "0" *)
wire _29_;
(* unused_bits = "0" *)
wire _30_;
(* unused_bits = "0" *)
wire _31_;
(* unused_bits = "0" *)
wire _32_;
(* unused_bits = "0" *)
wire _33_;
(* unused_bits = "0" *)
wire _34_;
(* unused_bits = "0" *)
wire _35_;
(* unused_bits = "0" *)
wire _36_;
(* src = "top.v:9" *)
output busy;
(* src = "top.v:2" *)
input clk;
(* src = "top.v:16" *)
reg [2:0] count;
(* src = "top.v:4" *)
input en;
(* src = "top.v:10" *)
output finish;
(* src = "top.v:5" *)
input ls;
(* src = "top.v:6" *)
input rs;
(* src = "top.v:3" *)
input rst;
(* src = "top.v:8" *)
output stop;
assign _02_ = count + (* src = "top.v:80" *) 32'd1;
assign _03_ = ~ (* src = "top.v:43" *) ls;
(* fsm_encoding = "auto" *)
(* src = "top.v:14" *)
\$fsm #(
.ARST_POLARITY(1'h1),
.CLK_POLARITY(1'h1),
.CTRL_IN_WIDTH(32'd7),
.CTRL_OUT_WIDTH(32'd6),
.NAME("\\st"),
.STATE_BITS(32'd14),
.STATE_NUM(32'd14),
.STATE_NUM_LOG2(32'd4),
.STATE_RST(32'd0),
.STATE_TABLE(196'b1zzzzzzzzzzzzzz1zzzzzzzzzzzzzz1zzzzzzzzzzzzzz1zzzzzzzzzzzzzz1zzzzzzzzzzzzzz1zzzzzzzzzzzzzz1zzzzzzzzzzzzzz1zzzzzzzzzzzzzz1zzzzzzzzzzzzzz1zzzzzzzzzzzzzz1zzzzzzzzzzzzzz1zzzzzzzzzzzzzz1zzzzzzzzzzzzzz1),
.TRANS_NUM(32'd34),
.TRANS_TABLE(714'b1101zzz0z0z10100000001101zzz1z0z10010000001101zzzzz1z00000000001100zzzzz0z00110000001100zzzzz1z00000000001011zzzzz0z01110000011011zzzzz1z00000000011010zzzzz0z10101000001010zzzzz1z000010000010010zzzz0z101100000010011zzzz0z01100000001001zzzzz1z00000000001000zzzzz0z00010010001000zzzzz1z00000010000111zzzzz0z01000000000111zzzzz1z00000000000110zzzz10z11010000000110zzzz00z00010000000110zzzzz1z00000000000101zzzzz0111000000000101zzzzz0000100000000101zzzzz1z00000000000100zz1zz0z10110000000100zz0zz0z00100000000100zzzzz1z00000000000011zzzzz0z01010000100011zzzzz1z00000000100010z0zzz0z10010100000010z1zzz0z01010100000010zzzzz1z00000100000001zzzzz0z10000001000001zzzzz1z00000001000000zzzzz0z01110000000000zzzzz1z0000000000)
) _39_ (
.ARST(1'h0),
.CLK(clk),
.CTRL_IN({ _03_, _10_, rs, _11_, ls, rst, _12_ }),
.CTRL_OUT({ _07_, _04_, _09_, _08_, _06_, _05_ })
);
assign _10_ = count > (* src = "top.v:39" *) 32'd7;
assign _11_ = ls && (* src = "top.v:53" *) rs;
assign _12_ = ls || (* src = "top.v:60" *) rs;
assign _13_ = _05_ || (* src = "top.v:85" *) _06_;
assign _14_ = _08_ || (* src = "top.v:89" *) _09_;
always @(posedge clk)
count <= _00_;
assign _15_ = _10_ ? (* src = "top.v:77" *) 3'h0 : _02_[2:0];
assign _16_ = _04_ ? (* src = "top.v:76" *) _15_ : count;
assign _00_ = rst ? (* src = "top.v:72" *) _16_ : 3'h0;
assign stop = _13_ ? (* src = "top.v:85" *) 1'h1 : 1'h0;
assign finish = _07_ ? (* src = "top.v:87" *) 1'h1 : 1'h0;
assign busy = _14_ ? (* src = "top.v:89" *) 1'h1 : 1'h0;
endmodule
(* cells_not_processed = 1 *)
(* src = "top.v:94" *)
module top(clk, rst, en, a, b, s, bs, f);
(* src = "top.v:98" *)
input a;
(* src = "top.v:99" *)
input b;
(* src = "top.v:101" *)
output bs;
(* src = "top.v:95" *)
input clk;
(* src = "top.v:97" *)
input en;
(* src = "top.v:102" *)
output f;
(* src = "top.v:96" *)
input rst;
(* src = "top.v:100" *)
output s;
(* module_not_derived = 32'd1 *)
(* src = "top.v:105" *)
FSM u_FSM (
.busy(bs),
.clk(clk),
.en(en),
.finish(f),
.ls(a),
.rs(b),
.rst(rst),
.stop(s)
);
endmodule
equiv/equiv_make_fsm/testbench.v 0 → 100644
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
equiv/equiv_make_fsm/top.v 0 → 100644
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
equiv/equiv_mark/logic.v 0 → 100644
`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
equiv/equiv_mark/synth_top.v 0 → 100644
/* 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
equiv/equiv_mark/testbench.v 0 → 100644
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
equiv/equiv_mark/top.v 0 → 100644
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
equiv/equiv_miter/logic.v 0 → 100644
`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
equiv/equiv_miter/synth_top.v 0 → 100644
/* 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
equiv/equiv_miter/testbench.v 0 → 100644
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
equiv/equiv_miter/top.v 0 → 100644
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
equiv/equiv_opt/logic.v 0 → 100644
`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
equiv/equiv_opt/map.map 0 → 100644
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
equiv/equiv_opt/synth_top.v 0 → 100644
/* 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
equiv/equiv_opt/testbench.v 0 → 100644
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
equiv/equiv_opt/top.v 0 → 100644
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
equiv/equiv_purge/logic.v 0 → 100644
`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
equiv/equiv_purge/synth_top.v 0 → 100644
/* 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
equiv/equiv_purge/testbench.v 0 → 100644
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
equiv/equiv_purge/top.v 0 → 100644
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
equiv/equiv_remove/logic.v 0 → 100644
`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
equiv/equiv_remove/synth_top.v 0 → 100644
/* 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
equiv/equiv_remove/testbench.v 0 → 100644
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
equiv/equiv_remove/top.v 0 → 100644
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
equiv/equiv_simple/logic.v 0 → 100644
`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
equiv/equiv_simple/synth_top.v 0 → 100644
/* 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
equiv/equiv_simple/testbench.v 0 → 100644
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
equiv/equiv_simple/top.v 0 → 100644
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
equiv/equiv_simple_fsm/logic.v 0 → 100644
module \$fsm (CLK, ARST, CTRL_IN, CTRL_OUT);
parameter NAME = "";
parameter CLK_POLARITY = 1'b1;
parameter ARST_POLARITY = 1'b1;
parameter CTRL_IN_WIDTH = 1;
parameter CTRL_OUT_WIDTH = 1;
parameter STATE_BITS = 1;
parameter STATE_NUM = 1;
parameter STATE_NUM_LOG2 = 1;
parameter STATE_RST = 0;
parameter STATE_TABLE = 1'b0;
parameter TRANS_NUM = 1;
parameter TRANS_TABLE = 4'b0x0x;
input CLK, ARST;
input [CTRL_IN_WIDTH-1:0] CTRL_IN;
output reg [CTRL_OUT_WIDTH-1:0] CTRL_OUT;
wire pos_clk = CLK == CLK_POLARITY;
wire pos_arst = ARST == ARST_POLARITY;
reg [STATE_BITS-1:0] state;
reg [STATE_BITS-1:0] state_tmp;
reg [STATE_BITS-1:0] next_state;
reg [STATE_BITS-1:0] tr_state_in;
reg [STATE_BITS-1:0] tr_state_out;
reg [CTRL_IN_WIDTH-1:0] tr_ctrl_in;
reg [CTRL_OUT_WIDTH-1:0] tr_ctrl_out;
integer i;
task tr_fetch;
input [31:0] tr_num;
reg [31:0] tr_pos;
reg [STATE_NUM_LOG2-1:0] state_num;
begin
tr_pos = (2*STATE_NUM_LOG2+CTRL_IN_WIDTH+CTRL_OUT_WIDTH)*tr_num;
tr_ctrl_out = TRANS_TABLE >> tr_pos;
tr_pos = tr_pos + CTRL_OUT_WIDTH;
state_num = TRANS_TABLE >> tr_pos;
tr_state_out = STATE_TABLE >> (STATE_BITS*state_num);
tr_pos = tr_pos + STATE_NUM_LOG2;
tr_ctrl_in = TRANS_TABLE >> tr_pos;
tr_pos = tr_pos + CTRL_IN_WIDTH;
state_num = TRANS_TABLE >> tr_pos;
tr_state_in = STATE_TABLE >> (STATE_BITS*state_num);
tr_pos = tr_pos + STATE_NUM_LOG2;
end
endtask
/*
always @(posedge pos_clk, posedge pos_arst) begin
if (pos_arst) begin
state_tmp = STATE_TABLE[STATE_BITS*(STATE_RST+1)-1:STATE_BITS*STATE_RST];
for (i = 0; i < STATE_BITS; i = i+1)
if (state_tmp[i] === 1'bz)
state_tmp[i] = 0;
state <= state_tmp;
end else begin
state_tmp = next_state;
for (i = 0; i < STATE_BITS; i = i+1)
if (state_tmp[i] === 1'bz)
state_tmp[i] = 0;
state <= state_tmp;
end
end
always @(state, CTRL_IN) begin
next_state <= STATE_TABLE[STATE_BITS*(STATE_RST+1)-1:STATE_BITS*STATE_RST];
CTRL_OUT <= 'bx;
// $display("---");
// $display("Q: %b %b", state, CTRL_IN);
for (i = 0; i < TRANS_NUM; i = i+1) begin
tr_fetch(i);
// $display("T: %b %b -> %b %b [%d]", tr_state_in, tr_ctrl_in, tr_state_out, tr_ctrl_out, i);
casez ({state, CTRL_IN})
{tr_state_in, tr_ctrl_in}: begin
// $display("-> %b %b <- MATCH", state, CTRL_IN);
{next_state, CTRL_OUT} <= {tr_state_out, tr_ctrl_out};
end
endcase
end
end
*/
endmodule
equiv/equiv_simple_fsm/synth_top.v 0 → 100644
/* Generated by Yosys 0.8+96 (git sha1 2d73e1b6, gcc 8.2.0-7ubuntu1 -Og -fPIC) */
(* cells_not_processed = 1 *)
(* src = "top.v:1" *)
module FSM(clk, rst, en, ls, rs, stop, busy, finish);
(* src = "top.v:71" *)
wire [2:0] _00_;
(* src = "top.v:19" *)
(* unused_bits = "0 1 2 3" *)
wire [3:0] _01_;
(* src = "top.v:80" *)
wire [31:0] _02_;
(* src = "top.v:43" *)
wire _03_;
(* src = "top.v:76" *)
wire _04_;
(* src = "top.v:85" *)
wire _05_;
(* src = "top.v:85" *)
wire _06_;
(* src = "top.v:87" *)
wire _07_;
(* src = "top.v:89" *)
wire _08_;
(* src = "top.v:89" *)
wire _09_;
(* src = "top.v:39" *)
wire _10_;
(* src = "top.v:53" *)
wire _11_;
(* src = "top.v:60" *)
wire _12_;
(* src = "top.v:85" *)
wire _13_;
(* src = "top.v:89" *)
wire _14_;
wire [2:0] _15_;
wire [2:0] _16_;
(* unused_bits = "0" *)
wire _17_;
(* unused_bits = "0" *)
wire _18_;
(* unused_bits = "0" *)
wire _19_;
(* unused_bits = "0" *)
wire _20_;
(* unused_bits = "0" *)
wire _21_;
(* unused_bits = "0" *)
wire _22_;
(* unused_bits = "0" *)
wire _23_;
(* unused_bits = "0" *)
wire _24_;
(* unused_bits = "0" *)
wire _25_;
(* unused_bits = "0" *)
wire _26_;
(* unused_bits = "0" *)
wire _27_;
(* unused_bits = "0" *)
wire _28_;
(* unused_bits = "0" *)
wire _29_;
(* unused_bits = "0" *)
wire _30_;
(* unused_bits = "0" *)
wire _31_;
(* unused_bits = "0" *)
wire _32_;
(* unused_bits = "0" *)
wire _33_;
(* unused_bits = "0" *)
wire _34_;
(* unused_bits = "0" *)
wire _35_;
(* unused_bits = "0" *)
wire _36_;
(* src = "top.v:9" *)
output busy;
(* src = "top.v:2" *)
input clk;
(* src = "top.v:16" *)
reg [2:0] count;
(* src = "top.v:4" *)
input en;
(* src = "top.v:10" *)
output finish;
(* src = "top.v:5" *)
input ls;
(* src = "top.v:6" *)
input rs;
(* src = "top.v:3" *)
input rst;
(* src = "top.v:8" *)
output stop;
assign _02_ = count + (* src = "top.v:80" *) 32'd1;
assign _03_ = ~ (* src = "top.v:43" *) ls;
(* fsm_encoding = "auto" *)
(* src = "top.v:14" *)
\$fsm #(
.ARST_POLARITY(1'h1),
.CLK_POLARITY(1'h1),
.CTRL_IN_WIDTH(32'd7),
.CTRL_OUT_WIDTH(32'd6),
.NAME("\\st"),
.STATE_BITS(32'd14),
.STATE_NUM(32'd14),
.STATE_NUM_LOG2(32'd4),
.STATE_RST(32'd0),
.STATE_TABLE(196'b1zzzzzzzzzzzzzz1zzzzzzzzzzzzzz1zzzzzzzzzzzzzz1zzzzzzzzzzzzzz1zzzzzzzzzzzzzz1zzzzzzzzzzzzzz1zzzzzzzzzzzzzz1zzzzzzzzzzzzzz1zzzzzzzzzzzzzz1zzzzzzzzzzzzzz1zzzzzzzzzzzzzz1zzzzzzzzzzzzzz1zzzzzzzzzzzzzz1),
.TRANS_NUM(32'd34),
.TRANS_TABLE(714'b1101zzz0z0z10100000001101zzz1z0z10010000001101zzzzz1z00000000001100zzzzz0z00110000001100zzzzz1z00000000001011zzzzz0z01110000011011zzzzz1z00000000011010zzzzz0z10101000001010zzzzz1z000010000010010zzzz0z101100000010011zzzz0z01100000001001zzzzz1z00000000001000zzzzz0z00010010001000zzzzz1z00000010000111zzzzz0z01000000000111zzzzz1z00000000000110zzzz10z11010000000110zzzz00z00010000000110zzzzz1z00000000000101zzzzz0111000000000101zzzzz0000100000000101zzzzz1z00000000000100zz1zz0z10110000000100zz0zz0z00100000000100zzzzz1z00000000000011zzzzz0z01010000100011zzzzz1z00000000100010z0zzz0z10010100000010z1zzz0z01010100000010zzzzz1z00000100000001zzzzz0z10000001000001zzzzz1z00000001000000zzzzz0z01110000000000zzzzz1z0000000000)
) _39_ (
.ARST(1'h0),
.CLK(clk),
.CTRL_IN({ _03_, _10_, rs, _11_, ls, rst, _12_ }),
.CTRL_OUT({ _07_, _04_, _09_, _08_, _06_, _05_ })
);
assign _10_ = count > (* src = "top.v:39" *) 32'd7;
assign _11_ = ls && (* src = "top.v:53" *) rs;
assign _12_ = ls || (* src = "top.v:60" *) rs;
assign _13_ = _05_ || (* src = "top.v:85" *) _06_;
assign _14_ = _08_ || (* src = "top.v:89" *) _09_;
always @(posedge clk)
count <= _00_;
assign _15_ = _10_ ? (* src = "top.v:77" *) 3'h0 : _02_[2:0];
assign _16_ = _04_ ? (* src = "top.v:76" *) _15_ : count;
assign _00_ = rst ? (* src = "top.v:72" *) _16_ : 3'h0;
assign stop = _13_ ? (* src = "top.v:85" *) 1'h1 : 1'h0;
assign finish = _07_ ? (* src = "top.v:87" *) 1'h1 : 1'h0;
assign busy = _14_ ? (* src = "top.v:89" *) 1'h1 : 1'h0;
endmodule
(* cells_not_processed = 1 *)
(* src = "top.v:94" *)
module top(clk, rst, en, a, b, s, bs, f);
(* src = "top.v:98" *)
input a;
(* src = "top.v:99" *)
input b;
(* src = "top.v:101" *)
output bs;
(* src = "top.v:95" *)
input clk;
(* src = "top.v:97" *)
input en;
(* src = "top.v:102" *)
output f;
(* src = "top.v:96" *)
input rst;
(* src = "top.v:100" *)
output s;
(* module_not_derived = 32'd1 *)
(* src = "top.v:105" *)
FSM u_FSM (
.busy(bs),
.clk(clk),
.en(en),
.finish(f),
.ls(a),
.rs(b),
.rst(rst),
.stop(s)
);
endmodule
equiv/equiv_simple_fsm/testbench.v 0 → 100644
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
equiv/equiv_simple_fsm/top.v 0 → 100644
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
equiv/equiv_status/logic.v 0 → 100644
`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
equiv/equiv_status/synth_top.v 0 → 100644
/* 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
equiv/equiv_status/testbench.v 0 → 100644
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
equiv/equiv_status/top.v 0 → 100644
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
equiv/equiv_struct/logic.v 0 → 100644
`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
equiv/equiv_struct/synth_top.v 0 → 100644
/* 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
equiv/equiv_struct/testbench.v 0 → 100644
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
equiv/equiv_struct/top.v 0 → 100644
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
equiv/run.sh 0 → 100644
#!/bin/bash
set -ex
test -d $1
test -f scripts/$2.ys
rm -rf $1/work_$2
mkdir $1/work_$2
cd $1/work_$2
yosys -ql yosys.log ../../scripts/$2.ys
sed -i 's/reg =/dummy =/' ./synth.v
iverilog -o testbench ../testbench.v synth.v ../../common.v ../../../../../techlibs/common/simcells.v ../../../../../techlibs/common/simlib.v
if ! vvp -N testbench > testbench.log 2>&1; then
grep 'ERROR' testbench.log
echo fail > ${1}_${2}.status
elif grep 'ERROR' testbench.log || ! grep 'OKAY' testbench.log; then
echo fail > ${1}_${2}.status
else
echo pass > ${1}_${2}.status
fi
touch .stamp
equiv/scripts/equiv_add.ys 0 → 100644
read_verilog ../top.v
prep -flatten -top top
splitnets -ports;;
design -stash gold
read_verilog ../synth_top.v
read_verilog ../logic.v
prep -flatten -top top
splitnets -ports;;
design -stash gate
design -copy-from gold -as gold top
design -copy-from gate -as gate top
equiv_make gold gate equiv
equiv_add gold gate
design -reset
read_verilog ../top.v
write_verilog synth.v
equiv/scripts/equiv_add_try.ys 0 → 100644
read_verilog ../top.v
prep -flatten -top top
splitnets -ports;;
design -stash gold
read_verilog ../synth_top.v
read_verilog ../logic.v
prep -flatten -top top
splitnets -ports;;
design -stash gate
design -copy-from gold -as gold top
design -copy-from gate -as gate top
equiv_make gold gate equiv
equiv_add -try gold gate
design -reset
read_verilog ../top.v
write_verilog synth.v
equiv/scripts/equiv_induct.ys 0 → 100644
read_verilog ../top.v
prep -flatten -top top
splitnets -ports;;
design -stash gold
read_verilog ../synth_top.v
read_verilog ../logic.v
prep -flatten -top top
splitnets -ports;;
design -stash gate
design -copy-from gold -as gold top
design -copy-from gate -as gate top
equiv_make gold gate equiv
equiv_induct
design -reset
read_verilog ../top.v
write_verilog synth.v
equiv/scripts/equiv_induct_seq.ys 0 → 100644
read_verilog ../top.v
prep -flatten -top top
splitnets -ports;;
design -stash gold
read_verilog ../synth_top.v
read_verilog ../logic.v
prep -flatten -top top
splitnets -ports;;
design -stash gate
design -copy-from gold -as gold top
design -copy-from gate -as gate top
equiv_make gold gate equiv
equiv_induct -seq 3
design -reset
read_verilog ../top.v
write_verilog synth.v
equiv/scripts/equiv_induct_undef.ys 0 → 100644
read_verilog ../top.v
prep -flatten -top top
splitnets -ports;;
design -stash gold
read_verilog ../synth_top.v
read_verilog ../logic.v
prep -flatten -top top
splitnets -ports;;
design -stash gate
design -copy-from gold -as gold top
design -copy-from gate -as gate top
equiv_make gold gate equiv
equiv_induct -undef
design -reset
read_verilog ../top.v
write_verilog synth.v
equiv/scripts/equiv_make.ys 0 → 100644
read_verilog ../top.v
prep -flatten -top top
splitnets -ports;;
design -stash gold
read_verilog ../synth_top.v
read_verilog ../logic.v
prep -flatten -top top
splitnets -ports;;
design -stash gate
design -copy-from gold -as gold top
design -copy-from gate -as gate top
equiv_make gold gate equiv
design -reset
read_verilog ../top.v
write_verilog synth.v
equiv/scripts/equiv_make_blacklist.ys 0 → 100644
read_verilog ../top.v
prep -flatten -top top
splitnets -ports;;
design -stash gold
read_verilog ../synth_top.v
read_verilog ../logic.v
prep -flatten -top top
splitnets -ports;;
design -stash gate
design -copy-from gold -as gold top
design -copy-from gate -as gate top
equiv_make -blacklist ../blacklist.txt gold gate equiv
design -reset
read_verilog ../top.v
write_verilog synth.v
equiv/scripts/equiv_make_encfile.ys 0 → 100644
read_verilog ../top.v
proc
fsm_detect
fsm_extract
fsm_recode -encfile encfile.fsm
design -stash gold
read_verilog ../synth_top.v
read_verilog ../logic.v
proc
design -stash gate
design -copy-from gold -as gold top
design -copy-from gate -as gate top
equiv_make -encfile encfile.fsm gold gate equiv
design -reset
read_verilog ../top.v
proc
write_verilog synth.v
equiv/scripts/equiv_make_encfile_fsm.ys 0 → 100644
read_verilog ../top.v
proc
fsm_detect
fsm_extract
fsm_recode -encfile encfile.fsm
design -stash gold
read_verilog ../synth_top.v
read_verilog ../logic.v
proc
design -stash gate
design -copy-from gold -as gold FSM
design -copy-from gate -as gate FSM
equiv_make -blacklist ../blacklist.txt -inames -encfile encfile.fsm gold gate equiv
design -reset
read_verilog ../top.v
proc
write_verilog synth.v
equiv/scripts/equiv_make_inames.ys 0 → 100644
read_verilog ../top.v
prep -flatten -top top
splitnets -ports;;
design -stash gold
read_verilog ../synth_top.v
read_verilog ../logic.v
prep -flatten -top top
splitnets -ports;;
design -stash gate
design -copy-from gold -as gold top
design -copy-from gate -as gate top
equiv_make -inames gold gate equiv
design -reset
read_verilog ../top.v
write_verilog synth.v
equiv/scripts/equiv_mark.ys 0 → 100644
read_verilog ../top.v
prep -flatten -top top
splitnets -ports;;
design -stash gold
read_verilog ../synth_top.v
read_verilog ../logic.v
prep -flatten -top top
splitnets -ports;;
design -stash gate
design -copy-from gold -as gold top
design -copy-from gate -as gate top
equiv_make gold gate equiv
equiv_mark
design -reset
read_verilog ../top.v
write_verilog synth.v
equiv/scripts/equiv_miter.ys 0 → 100644
read_verilog ../top.v
prep -flatten -top top
splitnets -ports;;
design -stash gold
read_verilog ../synth_top.v
read_verilog ../logic.v
prep -flatten -top top
splitnets -ports;;
design -stash gate
design -copy-from gold -as gold top
design -copy-from gate -as gate top
equiv_make gold gate equiv
equiv_miter miter_module equiv
design -reset
read_verilog ../top.v
write_verilog synth.v
equiv/scripts/equiv_miter_assert.ys 0 → 100644
read_verilog ../top.v
prep -flatten -top top
splitnets -ports;;
design -stash gold
read_verilog ../synth_top.v
read_verilog ../logic.v
prep -flatten -top top
splitnets -ports;;
design -stash gate
design -copy-from gold -as gold top
design -copy-from gate -as gate top
equiv_make gold gate equiv
equiv_miter -assert miter_module equiv
design -reset
read_verilog ../top.v
write_verilog synth.v
equiv/scripts/equiv_miter_cmp.ys 0 → 100644
read_verilog ../top.v
prep -flatten -top top
splitnets -ports;;
design -stash gold
read_verilog ../synth_top.v
read_verilog ../logic.v
prep -flatten -top top
splitnets -ports;;
design -stash gate
design -copy-from gold -as gold top
design -copy-from gate -as gate top
equiv_make gold gate equiv
equiv_miter -cmp miter_module equiv
design -reset
read_verilog ../top.v
write_verilog synth.v
equiv/scripts/equiv_miter_trigger.ys 0 → 100644
read_verilog ../top.v
prep -flatten -top top
splitnets -ports;;
design -stash gold
read_verilog ../synth_top.v
read_verilog ../logic.v
prep -flatten -top top
splitnets -ports;;
design -stash gate
design -copy-from gold -as gold top
design -copy-from gate -as gate top
equiv_make gold gate equiv
equiv_miter -trigger miter_module equiv
design -reset
read_verilog ../top.v
write_verilog synth.v
equiv/scripts/equiv_miter_undef.ys 0 → 100644
read_verilog ../top.v
prep -flatten -top top
splitnets -ports;;
design -stash gold
read_verilog ../synth_top.v
read_verilog ../logic.v
prep -flatten -top top
splitnets -ports;;
design -stash gate
design -copy-from gold -as gold top
design -copy-from gate -as gate top
equiv_make gold gate equiv
equiv_miter -undef miter_module equiv
design -reset
read_verilog ../top.v
write_verilog synth.v
equiv/scripts/equiv_opt.ys 0 → 100644
read_verilog ../top.v
prep -flatten -top top
splitnets -ports;;
design -stash gold
read_verilog ../synth_top.v
read_verilog ../logic.v
prep -flatten -top top
splitnets -ports;;
design -stash gate
design -copy-from gold -as gold top
design -copy-from gate -as gate top
equiv_make gold gate equiv
equiv_opt equiv_purge
design -reset
read_verilog ../top.v
write_verilog synth.v
equiv/scripts/equiv_opt_assert.ys 0 → 100644
read_verilog ../top.v
proc
equiv_opt -assert equiv_purge
prep -flatten -top top
splitnets -ports;;
design -stash gold
read_verilog ../synth_top.v
read_verilog ../logic.v
prep -flatten -top top
splitnets -ports;;
design -stash gate
design -copy-from gold -as gold top
design -copy-from gate -as gate top
equiv_make gold gate equiv
equiv_opt equiv_purge
design -reset
read_verilog ../top.v
write_verilog synth.v
equiv/scripts/equiv_opt_map.ys 0 → 100644
read_verilog ../top.v
prep -flatten -top top
splitnets -ports;;
design -stash gold
read_verilog ../synth_top.v
read_verilog ../logic.v
prep -flatten -top top
splitnets -ports;;
design -stash gate
design -copy-from gold -as gold top
design -copy-from gate -as gate top
equiv_make gold gate equiv
equiv_opt -map ../map.map equiv_purge
design -reset
read_verilog ../top.v
write_verilog synth.v
equiv/scripts/equiv_opt_run.ys 0 → 100644
read_verilog ../top.v
prep -flatten -top top
splitnets -ports;;
design -stash gold
read_verilog ../synth_top.v
read_verilog ../logic.v
prep -flatten -top top
splitnets -ports;;
design -stash gate
design -copy-from gold -as gold top
design -copy-from gate -as gate top
equiv_make gold gate equiv
equiv_opt -run a:b equiv_purge
design -reset
read_verilog ../top.v
write_verilog synth.v
equiv/scripts/equiv_purge.ys 0 → 100644
read_verilog ../top.v
prep -flatten -top top
splitnets -ports;;
design -stash gold
read_verilog ../synth_top.v
read_verilog ../logic.v
prep -flatten -top top
splitnets -ports;;
design -stash gate
design -copy-from gold -as gold top
design -copy-from gate -as gate top
equiv_make gold gate equiv
equiv_purge
design -reset
read_verilog ../top.v
write_verilog synth.v
equiv/scripts/equiv_remove.ys 0 → 100644
read_verilog ../top.v
prep -flatten -top top
splitnets -ports;;
design -stash gold
read_verilog ../synth_top.v
read_verilog ../logic.v
prep -flatten -top top
splitnets -ports;;
design -stash gate
design -copy-from gold -as gold top
design -copy-from gate -as gate top
equiv_make gold gate equiv
equiv_remove equiv
design -reset
read_verilog ../top.v
write_verilog synth.v
equiv/scripts/equiv_remove_gate.ys 0 → 100644
read_verilog ../top.v
prep -flatten -top top
splitnets -ports;;
design -stash gold
read_verilog ../synth_top.v
read_verilog ../logic.v
prep -flatten -top top
splitnets -ports;;
design -stash gate
design -copy-from gold -as gold top
design -copy-from gate -as gate top
equiv_make gold gate equiv
equiv_remove -gate equiv
design -reset
read_verilog ../top.v
write_verilog synth.v
equiv/scripts/equiv_remove_gold.ys 0 → 100644
read_verilog ../top.v
prep -flatten -top top
splitnets -ports;;
design -stash gold
read_verilog ../synth_top.v
read_verilog ../logic.v
prep -flatten -top top
splitnets -ports;;
design -stash gate
design -copy-from gold -as gold top
design -copy-from gate -as gate top
equiv_make gold gate equiv
equiv_remove -gold equiv
design -reset
read_verilog ../top.v
write_verilog synth.v
equiv/scripts/equiv_simple.ys 0 → 100644
read_verilog ../top.v
prep -flatten -top top
splitnets -ports;;
design -stash gold
read_verilog ../synth_top.v
read_verilog ../logic.v
prep -flatten -top top
splitnets -ports;;
design -stash gate
design -copy-from gold -as gold top
design -copy-from gate -as gate top
equiv_make gold gate equiv
equiv_simple
design -reset
read_verilog ../top.v
write_verilog synth.v
equiv/scripts/equiv_simple_nogroup.ys 0 → 100644
read_verilog ../top.v
prep -flatten -top top
splitnets -ports;;
design -stash gold
read_verilog ../synth_top.v
read_verilog ../logic.v
prep -flatten -top top
splitnets -ports;;
design -stash gate
design -copy-from gold -as gold top
design -copy-from gate -as gate top
equiv_make gold gate equiv
equiv_simple -nogroup
design -reset
read_verilog ../top.v
write_verilog synth.v
equiv/scripts/equiv_simple_seq.ys 0 → 100644
read_verilog ../top.v
prep -flatten -top top
splitnets -ports;;
design -stash gold
read_verilog ../synth_top.v
read_verilog ../logic.v
prep -flatten -top top
splitnets -ports;;
design -stash gate
design -copy-from gold -as gold top
design -copy-from gate -as gate top
equiv_make gold gate equiv
equiv_simple -seq 2
design -reset
read_verilog ../top.v
write_verilog synth.v
equiv/scripts/equiv_simple_short.ys 0 → 100644
read_verilog ../top.v
prep -flatten -top top
splitnets -ports;;
design -stash gold
read_verilog ../synth_top.v
read_verilog ../logic.v
prep -flatten -top top
splitnets -ports;;
design -stash gate
design -copy-from gold -as gold top
design -copy-from gate -as gate top
equiv_make gold gate equiv
equiv_simple -short
design -reset
read_verilog ../top.v
write_verilog synth.v
equiv/scripts/equiv_simple_undef.ys 0 → 100644
read_verilog ../top.v
prep -flatten -top top
splitnets -ports;;
design -stash gold
read_verilog ../synth_top.v
read_verilog ../logic.v
prep -flatten -top top
splitnets -ports;;
design -stash gate
design -copy-from gold -as gold top
design -copy-from gate -as gate top
equiv_make gold gate equiv
equiv_simple -undef
design -reset
read_verilog ../top.v
write_verilog synth.v
equiv/scripts/equiv_simple_v.ys 0 → 100644
read_verilog ../top.v
prep -flatten -top top
splitnets -ports;;
design -stash gold
read_verilog ../synth_top.v
read_verilog ../logic.v
prep -flatten -top top
splitnets -ports;;
design -stash gate
design -copy-from gold -as gold top
design -copy-from gate -as gate top
equiv_make gold gate equiv
equiv_simple -v
design -reset
read_verilog ../top.v
write_verilog synth.v
equiv/scripts/equiv_status.ys 0 → 100644
read_verilog ../top.v
prep -flatten -top top
splitnets -ports;;
design -stash gold
read_verilog ../synth_top.v
read_verilog ../logic.v
prep -flatten -top top
splitnets -ports;;
design -stash gate
design -copy-from gold -as gold top
design -copy-from gate -as gate top
equiv_status -assert
equiv_make gold gate equiv
equiv_status
design -reset
read_verilog ../top.v
write_verilog synth.v
equiv/scripts/equiv_struct.ys 0 → 100644
read_verilog ../top.v
prep -flatten -top top
splitnets -ports;;
design -stash gold
read_verilog ../synth_top.v
read_verilog ../logic.v
prep -flatten -top top
splitnets -ports;;
design -stash gate
design -copy-from gold -as gold top
design -copy-from gate -as gate top
equiv_struct
equiv_make gold gate equiv
equiv_struct
design -reset
read_verilog ../top.v
write_verilog synth.v
equiv/scripts/equiv_struct_fwd.ys 0 → 100644
read_verilog ../top.v
prep -flatten -top top
splitnets -ports;;
design -stash gold
read_verilog ../synth_top.v
read_verilog ../logic.v
prep -flatten -top top
splitnets -ports;;
design -stash gate
design -copy-from gold -as gold top
design -copy-from gate -as gate top
equiv_make gold gate equiv
equiv_struct -fwd
design -reset
read_verilog ../top.v
write_verilog synth.v
equiv/scripts/equiv_struct_fwonly.ys 0 → 100644
read_verilog ../top.v
prep -flatten -top top
splitnets -ports;;
design -stash gold
read_verilog ../synth_top.v
read_verilog ../logic.v
prep -flatten -top top
splitnets -ports;;
design -stash gate
design -copy-from gold -as gold top
design -copy-from gate -as gate top
equiv_make gold gate equiv
equiv_struct -fwonly $equiv
design -reset
read_verilog ../top.v
write_verilog synth.v
equiv/scripts/equiv_struct_icells.ys 0 → 100644
read_verilog ../top.v
prep -flatten -top top
splitnets -ports;;
design -stash gold
read_verilog ../synth_top.v
read_verilog ../logic.v
prep -flatten -top top
splitnets -ports;;
design -stash gate
design -copy-from gold -as gold top
design -copy-from gate -as gate top
equiv_make gold gate equiv
equiv_struct -icells
design -reset
read_verilog ../top.v
write_verilog synth.v
equiv/scripts/equiv_struct_maxiter.ys 0 → 100644
read_verilog ../top.v
prep -flatten -top top
splitnets -ports;;
design -stash gold
read_verilog ../synth_top.v
read_verilog ../logic.v
prep -flatten -top top
splitnets -ports;;
design -stash gate
design -copy-from gold -as gold top
design -copy-from gate -as gate top
equiv_make gold gate equiv
equiv_struct -maxiter 3
design -reset
read_verilog ../top.v
write_verilog synth.v
misc/Makefile
......@@ -69,4 +69,7 @@ $(eval $(call template,delete_mem, delete_mem ))
#cover
$(eval $(call template,cover, cover cover_q cover_o cover_dir cover_a ))
#insbuf ERROR: Found error in internal cell
#$(eval $(call template,insbuf,insbuf insbuf_cell))
.PHONY: all clean
misc/insbuf/testbench.v 0 → 100644
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 in;
wire [7:0] f;
top uut ( .clk(clk),
.in(in),
.out(f));
always @(posedge clk) begin
#3
in <= ~in;
end
assert_expr f_test(.clk(clk), .A(f[0]));
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
misc/insbuf/top.v 0 → 100644
module top (
out,
i,
clk,
o,
in
);
output [7:0] out;
input clk, in;
reg [7:0] out;
input i;
output o;
always @(posedge clk)
begin
out <= out << 1;
out[0] <= in;
end
endmodule
misc/scripts/insbuf.ys 0 → 100644
read_verilog ../top.v
synth
insbuf
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