Skip to content

Y
yosys-tests
Commit 78573f91 by SergeyDegtyar
Options

Update backends group. 

- write_intersynth;
- write_json;
- write_simplec;
- write_smt2;
- write_smv;
- write_spice;
- write_table;
- write_verilog;
- write_xaiger.
parent 16b8fe3f
Showing with 1287 additions and 0 deletions
backends_reviewed/write_intersynth/top.v 0 → 100644
module top
(
input x,
input y,
input cin,
output reg A,
output reg cout,
output c
);
initial begin
A = 0;
cout = 0;
end
assign c = 1'b0;
always @(posedge x) begin
A <= y + cin;
end
always @(negedge x) begin
cout <= y + A;
end
endmodule
backends_reviewed/write_intersynth/write_intersynth.pat 0 → 100644
node $procdff$7 $dff CLK x Q A D $add$../top.v:20$2_Y CLK_POLARITY '1 WIDTH 0x1
node $procdff$6 $dff CLK x Q cout D $add$../top.v:23$4_Y CLK_POLARITY '0 WIDTH 0x1
node $add$../top.v:23$4 $add Y $add$../top.v:23$4_Y B A A y Y_WIDTH 0x1 B_WIDTH 0x1 A_WIDTH 0x1 B_SIGNED 0x0 A_SIGNED 0x0
node $add$../top.v:20$2 $add Y $add$../top.v:20$2_Y B cin A y Y_WIDTH 0x1 B_WIDTH 0x1 A_WIDTH 0x1 B_SIGNED 0x0 A_SIGNED 0x0
# constant cells
node CONST_1_0x0 CONST_1 CONST CONST_1_0x0 VALUE 0x0
backends_reviewed/write_intersynth/write_intersynth.ys 0 → 100644
read_verilog ../top.v
proc
write_intersynth result.out
backends_reviewed/write_intersynth/write_intersynth_cant_export_fail.pat 0 → 100644
ERROR: Can't export composite or non-word-wide signal { \\y \\A }.
backends_reviewed/write_intersynth/write_intersynth_cant_export_fail.ys 0 → 100644
read_verilog ../top.v
proc
synth
abc -lut 4
write_intersynth intersynth.intersynth
backends_reviewed/write_intersynth/write_intersynth_cant_open_lib_file_fail.ys 0 → 100644
read_verilog ../top.v
proc
write_intersynth -lib u intersynth.intersynth
backends_reviewed/write_intersynth/write_intersynth_lib.ys 0 → 100644
read_verilog ../top.v
proc
write_intersynth -lib ../top.v result.out
backends_reviewed/write_intersynth/write_intersynth_notypes.ys 0 → 100644
read_verilog ../top.v
proc
write_intersynth -notypes result.out
backends_reviewed/write_intersynth/write_intersynth_selected.ys 0 → 100644
read_verilog ../top.v
proc
write_intersynth -selected result.out
backends_reviewed/write_intersynth/write_intersynth_unprocessed_proc_fail.pat 0 → 100644
ERROR: Can't generate a netlist for a module with unprocessed memories or processes!
backends_reviewed/write_intersynth/write_intersynth_unprocessed_proc_fail.ys 0 → 100644
read_verilog ../top.v
write_intersynth intersynth.intersynth
backends_reviewed/write_json/json.ys 0 → 100644
read_verilog ../top.v
proc
json
backends_reviewed/write_json/json_aig.ys 0 → 100644
read_verilog ../top.v
proc
json -aig
backends_reviewed/write_json/json_o.pat 0 → 100644
"cells": {
"$add$../top.v:17$2": {
"hide_name": 1,
"type": "$add",
"parameters": {
"A_SIGNED": 0,
"A_WIDTH": 1,
"B_SIGNED": 0,
"B_WIDTH": 1,
"Y_WIDTH": 1
},
"attributes": {
"src": "../top.v:17"
},
"port_directions": {
"A": "input",
"B": "input",
"Y": "output"
},
"connections": {
"A": [ 3 ],
"B": [ 4 ],
"Y": [ 7 ]
}
},
"$add$../top.v:20$4": {
"hide_name": 1,
"type": "$add",
"parameters": {
"A_SIGNED": 0,
"A_WIDTH": 1,
"B_SIGNED": 0,
"B_WIDTH": 1,
"Y_WIDTH": 1
},
"attributes": {
"src": "../top.v:20"
},
"port_directions": {
"A": "input",
"B": "input",
"Y": "output"
},
"connections": {
"A": [ 3 ],
"B": [ 5 ],
"Y": [ 8 ]
}
},
"$procdff$6": {
"hide_name": 1,
"type": "$dff",
"parameters": {
"CLK_POLARITY": "0",
"WIDTH": 1
},
"attributes": {
"src": "../top.v:19"
},
"port_directions": {
"CLK": "input",
"D": "input",
"Q": "output"
},
"connections": {
"CLK": [ 2 ],
"D": [ 8 ],
"Q": [ 6 ]
}
},
"$procdff$7": {
"hide_name": 1,
"type": "$dff",
"parameters": {
"CLK_POLARITY": "1",
"WIDTH": 1
},
"attributes": {
"src": "../top.v:16"
},
"port_directions": {
"CLK": "input",
"D": "input",
"Q": "output"
},
"connections": {
"CLK": [ 2 ],
"D": [ 7 ],
"Q": [ 5 ]
}
}
},
backends_reviewed/write_json/json_o.ys 0 → 100644
read_verilog ../top.v
proc
json -o result.out
design -reset
read_json result.out
backends_reviewed/write_json/json_o_aig.ys 0 → 100644
read_verilog ../top.v
proc
json -aig -o result.out
backends_reviewed/write_json/top.v 0 → 100644
module top
(
input x,
input y,
input cin,
output reg A,
output reg cout
);
initial begin
A = 0;
cout = 0;
end
always @(posedge x) begin
A <= y + cin;
end
always @(negedge x) begin
cout <= y + A;
end
endmodule
backends_reviewed/write_json/write_json.pat 0 → 100644
"cells": {
"$add$../top.v:17$2": {
"hide_name": 1,
"type": "$add",
"parameters": {
"A_SIGNED": 0,
"A_WIDTH": 1,
"B_SIGNED": 0,
"B_WIDTH": 1,
"Y_WIDTH": 1
},
"attributes": {
"src": "../top.v:17"
},
"port_directions": {
"A": "input",
"B": "input",
"Y": "output"
},
"connections": {
"A": [ 3 ],
"B": [ 4 ],
"Y": [ 7 ]
}
},
"$add$../top.v:20$4": {
"hide_name": 1,
"type": "$add",
"parameters": {
"A_SIGNED": 0,
"A_WIDTH": 1,
"B_SIGNED": 0,
"B_WIDTH": 1,
"Y_WIDTH": 1
},
"attributes": {
"src": "../top.v:20"
},
"port_directions": {
"A": "input",
"B": "input",
"Y": "output"
},
"connections": {
"A": [ 3 ],
"B": [ 5 ],
"Y": [ 8 ]
}
},
"$procdff$6": {
"hide_name": 1,
"type": "$dff",
"parameters": {
"CLK_POLARITY": "0",
"WIDTH": 1
},
"attributes": {
"src": "../top.v:19"
},
"port_directions": {
"CLK": "input",
"D": "input",
"Q": "output"
},
"connections": {
"CLK": [ 2 ],
"D": [ 8 ],
"Q": [ 6 ]
}
},
"$procdff$7": {
"hide_name": 1,
"type": "$dff",
"parameters": {
"CLK_POLARITY": "1",
"WIDTH": 1
},
"attributes": {
"src": "../top.v:16"
},
"port_directions": {
"CLK": "input",
"D": "input",
"Q": "output"
},
"connections": {
"CLK": [ 2 ],
"D": [ 7 ],
"Q": [ 5 ]
}
}
},
backends_reviewed/write_json/write_json.ys 0 → 100644
read_verilog ../top.v
proc
write_json result.out
design -reset
read_json result.out
backends_reviewed/write_json/write_json_aig.ys 0 → 100644
read_verilog ../top.v
proc
write_json -aig result.out
backends_reviewed/write_json/write_json_error_fail.pat 0 → 100644
ERROR: Can't open file `tt/json.json' for writing: No such file or directory
backends_reviewed/write_json/write_json_error_fail.ys 0 → 100644
read_verilog ../top.v
proc
json -o tt/json.json
backends_reviewed/write_simplec/top.v 0 → 100644
module mux16 (D, S, Y);
input [15:0] D;
input [3:0] S;
output Y;
assign Y = D[S];
endmodule
module top (
input [3:0] S,
input [15:0] D,
output M16
);
reg A;
initial begin
A = 0;
end
mux16 u_mux16 (
.S (S[3:0]),
.D (D[15:0]),
.Y (M16)
);
endmodule
backends_reviewed/write_simplec/write_simplec.ys 0 → 100644
read_verilog ../top.v
synth -top top
write_simplec result.out
backends_reviewed/write_simplec/write_simplec_cmos3.ys 0 → 100644
read_verilog ../top.v
synth -top top
abc -g cmos3
write_simplec result.out
backends_reviewed/write_simplec/write_simplec_cmos4.ys 0 → 100644
read_verilog ../top.v
synth -top top
abc -g cmos4
write_simplec result.out
backends_reviewed/write_simplec/write_simplec_i16.ys 0 → 100644
read_verilog ../top.v
synth -top top
write_simplec -i16 result.out
backends_reviewed/write_simplec/write_simplec_i32.ys 0 → 100644
read_verilog ../top.v
synth -top top
write_simplec -i32 result.out
backends_reviewed/write_simplec/write_simplec_i64.ys 0 → 100644
read_verilog ../top.v
synth -top top
write_simplec -i64 result.out
backends_reviewed/write_simplec/write_simplec_i8.ys 0 → 100644
read_verilog ../top.v
synth -top top
write_simplec -i8 result.out
backends_reviewed/write_simplec/write_simplec_no_c_model_fail.pat 0 → 100644
ERROR: No C model for $lut available at the moment (FIXME).
backends_reviewed/write_simplec/write_simplec_no_c_model_fail.ys 0 → 100644
read_verilog ../top.v
synth -top top
abc -lut 4
write_simplec c.c
write_verilog synth.v
backends_reviewed/write_simplec/write_simplec_verbose.ys 0 → 100644
read_verilog ../top.v
synth -top top
write_simplec -verbose result.out
backends_reviewed/write_smt2/top.tpl 0 → 100644
; we need QF_UFBV for this poof
(set-logic QF_UFBV)
; insert the auto-generated code here
%%
; declare two state variables s1 and s2
(declare-fun s1 () test_s)
(declare-fun s2 () test_s)
; state s2 is the successor of state s1
(assert (test_t s1 s2))
; we are looking for a model with y non-zero in s1
(assert (distinct (|test_n y| s1) #b0000))
; we are looking for a model with y zero in s2
(assert (= (|test_n y| s2) #b0000))
; is there such a model?
(check-sat)
backends_reviewed/write_smt2/top.v 0 → 100644
module tristate (en, i, o);
input en;
input i;
output [1:0] o;
wire [1:0] io;
assign io[0] = (en)? i : 1'bZ;
assign io[1] = (i)? en : 1'bZ;
assign o = io;
endmodule
module top (
input en,
input a,
inout [1:0] b,
output [1:0] c
);
tristate u_tri (
.en (en ),
.i (a ),
.o (c )
);
endmodule
backends_reviewed/write_smt2/top_cyclic_dep.v 0 → 100644
module tristate (en, i, o);
input en;
input i;
output [1:0] o;
wire [1:0] io;
assign io[0] = (en)? i : 1'bZ;
assign io[1] = (i)? en : 1'bZ;
assign o = io;
top utop (en,i,o,io);
endmodule
module top (
input en,
input a,
inout [1:0] b,
output [1:0] c
);
tristate u_tri (
.en (en ),
.i (a ),
.o (c )
);
endmodule
backends_reviewed/write_smt2/top_fsm.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;
//typedef enum logic [3:0] {S0, S1, S2, S3, S4, S5, S6, S7, S8, S9, S10, S11, S12, S13, S14} sts;
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
backends_reviewed/write_smt2/top_init_assert.v 0 → 100644
module top
(
input x,
input y,
input cin,
output reg A,
output reg cout,
output reg B,C
);
reg ASSERT = 1;
(* allconst *) reg foo;
(* allseq *) reg too;
initial begin
begin
A = 0;
cout = 0;
end
end
always @(posedge x) begin
if ($initstate)
A <= 0;
A <= y + cin + too;
assume(too);
assume(s_eventually too);
end
always @(posedge x) begin
if ($initstate)
cout <= 0;
cout <= y + A + foo;
assert(ASSERT);
assert(s_eventually ASSERT);
end
assign {B,C} = {cout,A} << 1;
endmodule
backends_reviewed/write_smt2/top_logic.v 0 → 100644
module top
(
input x,
input y,
input z,
input clk,
input A,
output B
);
assign B = (x || y || !z)? (A & z) : ~x;
endmodule
backends_reviewed/write_smt2/top_logic_loop.v 0 → 100644
module tristate (en, i, o);
input en;
input i;
output [1:0] o;
wire [1:0] io;
assign io[0] = (en)? i : 1'bZ;
assign io[1] = (i)? o[1] : 1'bZ;
assign o = io;
endmodule
module top (
input en,
input a,
inout [1:0] b,
output [1:0] c
);
tristate u_tri (
.en (en ),
.i (a ),
.o (c )
);
endmodule
backends_reviewed/write_smt2/top_mem.v 0 → 100644
module top
(
input [7:0] data_a, data_b,
input [6:1] addr_a, addr_b,
input we_a, we_b, re_a, re_b, clka, clkb,
output reg [7:0] q_a, q_b
);
// Declare the RAM variable
reg [7:0] ram[63:0];
initial begin
q_a <= 8'h00;
q_b <= 8'd0;
end
// Port A
always @ (posedge clka)
begin
if (we_a)
begin
ram[addr_a] <= data_a;
q_a <= data_a;
end
if (re_b)
begin
q_a <= ram[addr_a];
end
end
// Port B
always @ (posedge clkb)
begin
if (we_b)
begin
ram[addr_b] <= data_b;
q_b <= data_b;
end
if (re_b)
begin
q_b <= ram[addr_b];
end
end
endmodule
backends_reviewed/write_smt2/top_multiple_drivers.v 0 → 100644
module tristate (en, i, o);
input en;
input i;
output [1:0] o;
wire [1:0] io;
assign io[0] = (en)? i : 1'bZ;
assign io[1] = (i)? en : 1'bZ;
assign io[0] = (~en)? ~i : 1'bZ;
assign o = io;
endmodule
module top (
input en,
input a,
inout [1:0] b,
output [1:0] c
);
tristate u_tri (
.en (en ),
.i (a ),
.o (c )
);
endmodule
backends_reviewed/write_smt2/top_reduce.v 0 → 100644
module top
(
input x,
input y,
input cin,
output reg A,
output reg cout
);
reg A1,cout1;
initial begin
A = 0;
cout = 0;
end
always @(posedge x) begin
A1 <= ~y + &cin;
end
always @(posedge x) begin
cout1 <= cin ? |y : ^A;
end
always @(posedge x) begin
A <= A1|y~&cin~^A1;
end
always @(posedge x) begin
cout <= cout1&cin~|y;
end
endmodule
backends_reviewed/write_smt2/top_shiftx.v 0 → 100644
// VERIFIC-SKIP
module top(a, y);
input signed [4:0] a;
output signed y;
integer signed i = 0, j = 0;
reg signed [31:0] lut;
initial begin
for (i = 0; i < 32; i = i+1) begin
lut[i] = i > 1;
for (j = 2; j*j <= i; j = j+1)
if (i % j == 0)
lut[i] = 0;
end
end
assign y = lut[a];
endmodule
backends_reviewed/write_smt2/write_smt2.ys 0 → 100644
read_verilog ../top.v
proc
write_smt2 result.out
backends_reviewed/write_smt2/write_smt2_anyseq.ys 0 → 100644
read_verilog ../top_mem.v
proc
setundef -anyseq
memory
write_smt2 -mem result.out
backends_reviewed/write_smt2/write_smt2_bv.ys 0 → 100644
read_verilog ../top_mem.v
proc
memory
write_smt2 -bv result.out
backends_reviewed/write_smt2/write_smt2_cant_open_tpl_fail.ys 0 → 100644
read_verilog ../top.v
proc
memory
write_smt2 -tpl u smt2.smt2
backends_reviewed/write_smt2/write_smt2_cyclic_dependency_fail.pat 0 → 100644
ERROR: Cyclic dependency between modules found! Cycle includes module tristate.
backends_reviewed/write_smt2/write_smt2_cyclic_dependency_fail.ys 0 → 100644
read_verilog ../top_cyclic_dep.v
proc
memory
write_smt2 smt2.smt2
backends_reviewed/write_smt2/write_smt2_init_assert.ys 0 → 100644
read_verilog -sv ../top_init_assert.v
proc
write_smt2 -stbv smt2.smt2
synth -top top
write_smt2 -stbv smt2.smt2
backends_reviewed/write_smt2/write_smt2_logic.ys 0 → 100644
read_verilog ../top_logic.v
proc
write_smt2 result.out
backends_reviewed/write_smt2/write_smt2_logic_loop_fail.ys 0 → 100644
read_verilog ../top_logic_loop.v
proc
memory
write_smt2 smt2.smt2
backends_reviewed/write_smt2/write_smt2_mem.ys 0 → 100644
read_verilog ../top.v
proc
memory
write_smt2 -mem result.out
backends_reviewed/write_smt2/write_smt2_mem_fsm.ys 0 → 100644
read_verilog ../top_fsm.v
proc
memory
write_smt2 -mem result.out
backends_reviewed/write_smt2/write_smt2_mem_memtest.ys 0 → 100644
read_verilog ../top_mem.v
proc
memory
write_smt2 -mem result.out
backends_reviewed/write_smt2/write_smt2_memtest.ys 0 → 100644
read_verilog ../top_mem.v
proc
memory
write_smt2 result.out
backends_reviewed/write_smt2/write_smt2_multiple_drivers_fail.ys 0 → 100644
read_verilog ../top_multiple_drivers.v
proc
memory
write_smt2 smt2.smt2
backends_reviewed/write_smt2/write_smt2_nobv.ys 0 → 100644
read_verilog ../top.v
synth
write_smt2 -nobv result.out
backends_reviewed/write_smt2/write_smt2_nobv_fsm.ys 0 → 100644
read_verilog ../top_fsm.v
synth
write_smt2 -nobv result.out
backends_reviewed/write_smt2/write_smt2_nomem.ys 0 → 100644
read_verilog ../top.v
proc
write_smt2 -nomem result.out
backends_reviewed/write_smt2/write_smt2_reduce.ys 0 → 100644
read_verilog ../top_reduce.v
proc
write_smt2 result.out
backends_reviewed/write_smt2/write_smt2_shiftx.ys 0 → 100644
read_verilog ../top_shiftx.v
proc
write_smt2 result.out
backends_reviewed/write_smt2/write_smt2_stbv.ys 0 → 100644
read_verilog ../top.v
proc
write_smt2 -stbv result.out
backends_reviewed/write_smt2/write_smt2_stbv_memtest.ys 0 → 100644
read_verilog ../top_mem.v
proc
memory
write_smt2 -stbv result.out
backends_reviewed/write_smt2/write_smt2_stdt.ys 0 → 100644
read_verilog ../top.v
proc
write_smt2 -stdt result.out
backends_reviewed/write_smt2/write_smt2_synth.ys 0 → 100644
read_verilog ../top.v
synth -top top
write_smt2 result.out
backends_reviewed/write_smt2/write_smt2_tpl.ys 0 → 100644
read_verilog ../top.v
proc
write_smt2 -tpl ../top.tpl result.out
backends_reviewed/write_smt2/write_smt2_verbose.ys 0 → 100644
read_verilog ../top.v
proc
memory
write_smt2 -verbose result.out
backends_reviewed/write_smt2/write_smt2_verbose_fsm.ys 0 → 100644
read_verilog ../top_fsm.v
proc
memory
write_smt2 -verbose result.out
backends_reviewed/write_smt2/write_smt2_wires.ys 0 → 100644
read_verilog ../top.v
proc
write_smt2 -wires result.out
backends_reviewed/write_smv/top.tpl 0 → 100644
; we need QF_UFBV for this poof
(set-logic QF_UFBV)
; insert the auto-generated code here
%%
; declare two state variables s1 and s2
(declare-fun s1 () test_s)
(declare-fun s2 () test_s)
; state s2 is the successor of state s1
(assert (test_t s1 s2))
; we are looking for a model with y non-zero in s1
(assert (distinct (|test_n y| s1) #b0000))
; we are looking for a model with y zero in s2
(assert (= (|test_n y| s2) #b0000))
; is there such a model?
(check-sat)
backends_reviewed/write_smv/top.v 0 → 100644
module tristate (en, i, io, o);
input en;
input i;
inout [1:0] io;
output [1:0] o;
wire [1:0] io;
assign io[0] = (en)? i : 1'bZ;
assign io[1] = (i)? en : 1'bZ;
assign o = io;
endmodule
module top (
input en,
input a,
inout [1:0] b,
output [1:0] c
);
tristate u_tri (
.en (en ),
.i (a ),
.io (b ),
.o (c )
);
endmodule
backends_reviewed/write_smv/top_cmos4_mux.v 0 → 100644
module mux16 (D, S, Y);
input [15:0] D;
input [3:0] S;
output Y;
assign Y = D[S];
endmodule
module top (
input [3:0] S,
input [15:0] D,
output M16
);
mux16 u_mux16 (
.S (S[3:0]),
.D (D[15:0]),
.Y (M16)
);
endmodule
backends_reviewed/write_smv/top_fsm.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;
//typedef enum logic [3:0] {S0, S1, S2, S3, S4, S5, S6, S7, S8, S9, S10, S11, S12, S13, S14} sts;
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
backends_reviewed/write_smv/top_fulladder.v 0 → 100644
module top
(
input x,
input y,
input cin,
output reg A,
output reg cout
);
initial begin
A = 0;
cout = 0;
end
`ifndef BUG
always @(posedge x) begin
A <= y + cin;
end
always @(negedge x) begin
cout <= y + A;
end
`else
assign {cout,A} = cin - y * x;
`endif
endmodule
backends_reviewed/write_smv/top_init_assert.v 0 → 100644
module top
(
input x,
input y,
input cin,
output reg A,
output reg cout,
output reg B,C
);
reg ASSERT = 1;
initial begin
begin
A = 0;
cout = 0;
end
end
assign A = y + cin;
assign cout = y + A;
always @*
assert(ASSERT);
assign {B,C} = {cout,A} <<< 1;
endmodule
backends_reviewed/write_smv/top_logic.v 0 → 100644
module top
(
input x,
input y,
input z,
input clk,
input A,
output signed B,
output signed C,D,E
);
assign B = (x || y || !z)? (A & z) : ~x;
assign {D,C} = {y,z} >>> 1;
assign E = {x,y,z} / 3;
endmodule
backends_reviewed/write_smv/top_mem.v 0 → 100644
module top
(
input [7:0] data_a, data_b,
input [6:1] addr_a, addr_b,
input we_a, we_b, re_a, re_b, clka, clkb,
output reg [7:0] q_a, q_b
);
// Declare the RAM variable
reg [7:0] ram[63:0];
initial begin
q_a <= 8'h00;
q_b <= 8'd0;
end
// Port A
always @ (posedge clka)
begin
if (we_a)
begin
ram[addr_a] <= data_a;
q_a <= data_a;
end
if (re_b)
begin
q_a <= ram[addr_a];
end
end
// Port B
always @ (posedge clkb)
begin
if (we_b)
begin
ram[addr_b] <= data_b;
q_b <= data_b;
end
if (re_b)
begin
q_b <= ram[addr_b];
end
end
endmodule
backends_reviewed/write_smv/top_noproc_reduce.v 0 → 100644
module top
(
input x,
input y,
input cin,
output A,
output cout
);
wire A1,cout1;
assign A1 = ~y + &cin;
assign cout1 = cin ? |y : ^A;
assign A = A1|y~&cin~^A1;
assign cout = cout1&cin~|y;
endmodule
backends_reviewed/write_smv/top_shift.v 0 → 100644
module top
(
input signed x,
input signed y,
input signed cin,
output signed A,
output signed cout,
output signed B,C
);
assign A = y >> x;
assign cout = y + A >>> y;
assign {B,C} = {cout,A} << 1;
endmodule
backends_reviewed/write_smv/top_shiftx.v 0 → 100644
// VERIFIC-SKIP
module top(a, y);
input signed [4:0] a;
output signed y;
integer signed i = 0, j = 0;
reg signed [31:0] lut;
initial begin
for (i = 0; i < 32; i = i+1) begin
lut[i] = i > 1;
for (j = 2; j*j <= i; j = j+1)
if (i % j == 0)
lut[i] = 0;
end
end
assign y = lut[a];
endmodule
backends_reviewed/write_smv/top_wide_tri.v 0 → 100644
module tristate (en, i, io, o);
input en;
input [3:0] i;
inout [3:0] io;
output [1:0] o;
wire [3:0] io;
assign io[1:0] = (en)? i[1:0] : 1'bZ;
assign io[3:2] = (i[1:0])? en : 1'bZ;
assign o = io[2:1];
endmodule
module top (
input en,
input [3:0] a,
inout [3:0] b,
output [1:0] c
);
tristate u_tri (
.en (en ),
.i (a ),
.io (b ),
.o (c )
);
endmodule
backends_reviewed/write_smv/write_smv.pat 0 → 100644
_$ternary$###top#v#11$2_Y := bool(_i) ? _en : 0ub1_0;
_$ternary$###top#v#9$1_Y := bool(_en) ? _i : 0ub1_0;
_io := (_$ternary$###top#v#11$2_Y :: _$ternary$###top#v#9$1_Y);
_o := (_$ternary$###top#v#11$2_Y :: _$ternary$###top#v#9$1_Y);
backends_reviewed/write_smv/write_smv.ys 0 → 100644
read_verilog ../top.v
proc
write_smv result.out
backends_reviewed/write_smv/write_smv_cant_open_template_fail.ys 0 → 100644
read_verilog ../top.v
proc
memory
write_smv -tpl t smv.smv
write_verilog synth.v
backends_reviewed/write_smv/write_smv_cmos4.ys 0 → 100644
read_verilog ../top_cmos4_mux.v
synth -top top
abc -g cmos4
write_smv result.out
backends_reviewed/write_smv/write_smv_fsm.ys 0 → 100644
read_verilog ../top_fsm.v
proc
write_smv result.out
backends_reviewed/write_smv/write_smv_fulladder.pat 0 → 100644
_$add$###top_fulladder#v#21$4_Y := resize(_y, 1) + resize(_A, 1);
_$add$###top_fulladder#v#18$2_Y := resize(_y, 1) + resize(_cin, 1);
_$0#A#0#0# := _$add$###top_fulladder#v#18$2_Y;
_$0#cout#0#0# := _$add$###top_fulladder#v#21$4_Y;
backends_reviewed/write_smv/write_smv_fulladder.ys 0 → 100644
read_verilog ../top_fulladder.v
proc
write_smv result.out
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