mirror of
https://github.com/YosysHQ/yosys
synced 2025-04-23 17:15:33 +00:00
Merge branch 'YosysHQ:main' into main
This commit is contained in:
Akash Levy
GitHub
commit
120f69eda7
61 changed files with 16563 additions and 220 deletions
2
tests/arch/nanoxplore/.gitignore
vendored
Normal file
2
tests/arch/nanoxplore/.gitignore
vendored
Normal file
|
|
@ -0,0 +1,2 @@
|
|||
*.log
|
||||
/run-test.mk
|
||||
71
tests/arch/nanoxplore/add_sub.ys
Normal file
71
tests/arch/nanoxplore/add_sub.ys
Normal file
|
|
@ -0,0 +1,71 @@
|
|||
read_verilog ../common/add_sub.v
|
||||
hierarchy -top top
|
||||
proc
|
||||
equiv_opt -run :prove -map +/nanoxplore/cells_sim.v -map +/nanoxplore/cells_sim_u.v synth_nanoxplore -noiopad
|
||||
opt -full
|
||||
|
||||
miter -equiv -flatten -make_assert -make_outputs gold gate miter
|
||||
sat -verify -prove-asserts -seq 3 -set-init-zero -show-inputs -show-outputs miter
|
||||
design -load postopt # load the post-opt design (otherwise equiv_opt loads the pre-opt design)
|
||||
cd top # Constrain all select calls below inside the top module
|
||||
select -assert-count 2 t:NX_CY
|
||||
select -assert-count 4 t:NX_LUT
|
||||
select -assert-none t:NX_CY t:NX_LUT %% t:* %D
|
||||
|
||||
design -reset
|
||||
read_verilog <<EOT
|
||||
module top
|
||||
(
|
||||
input [5:0] x,
|
||||
input [5:0] y,
|
||||
|
||||
output [5:0] A,
|
||||
input CI,
|
||||
output CO
|
||||
);
|
||||
|
||||
assign {CO, A} = x + y + CI;
|
||||
endmodule
|
||||
EOT
|
||||
|
||||
hierarchy -top top
|
||||
proc
|
||||
equiv_opt -run :prove -map +/nanoxplore/cells_sim.v -map +/nanoxplore/cells_sim_u.v synth_nanoxplore -noiopad
|
||||
opt -full
|
||||
|
||||
miter -equiv -flatten -make_assert -make_outputs gold gate miter
|
||||
sat -verify -prove-asserts -seq 3 -set-init-zero -show-inputs -show-outputs miter
|
||||
|
||||
design -load postopt
|
||||
cd top
|
||||
stat
|
||||
select -assert-count 2 t:NX_CY
|
||||
select -assert-none t:NX_CY %% t:* %D
|
||||
|
||||
design -reset
|
||||
read_verilog <<EOT
|
||||
module top
|
||||
(
|
||||
input [189:0] x,
|
||||
input [189:0] y,
|
||||
|
||||
output [189:0] A
|
||||
);
|
||||
|
||||
assign A = x + y;
|
||||
endmodule
|
||||
EOT
|
||||
|
||||
hierarchy -top top
|
||||
proc
|
||||
equiv_opt -run :prove -map +/nanoxplore/cells_sim.v -map +/nanoxplore/cells_sim_u.v synth_nanoxplore -noiopad
|
||||
opt -full
|
||||
|
||||
miter -equiv -flatten -make_assert -make_outputs gold gate miter
|
||||
sat -verify -prove-asserts -seq 3 -set-init-zero -show-inputs -show-outputs miter
|
||||
|
||||
design -load postopt
|
||||
cd top
|
||||
stat
|
||||
select -assert-count 48 t:NX_CY
|
||||
select -assert-none t:NX_CY %% t:* %D
|
||||
47
tests/arch/nanoxplore/adffs.ys
Normal file
47
tests/arch/nanoxplore/adffs.ys
Normal file
|
|
@ -0,0 +1,47 @@
|
|||
read_verilog ../common/adffs.v
|
||||
design -save read
|
||||
|
||||
hierarchy -top adff
|
||||
proc
|
||||
equiv_opt -async2sync -assert -map +/nanoxplore/cells_sim.v synth_nanoxplore -noiopad # equivalency check
|
||||
design -load postopt # load the post-opt design (otherwise equiv_opt loads the pre-opt design)
|
||||
cd adff # Constrain all select calls below inside the top module
|
||||
select -assert-count 1 t:NX_DFF
|
||||
|
||||
select -assert-none t:NX_DFF %% t:* %D
|
||||
|
||||
|
||||
design -load read
|
||||
hierarchy -top adffn
|
||||
proc
|
||||
equiv_opt -async2sync -assert -map +/nanoxplore/cells_sim.v synth_nanoxplore -noiopad # equivalency check
|
||||
design -load postopt # load the post-opt design (otherwise equiv_opt loads the pre-opt design)
|
||||
cd adffn # Constrain all select calls below inside the top module
|
||||
select -assert-count 1 t:NX_DFF
|
||||
select -assert-count 1 t:NX_LUT
|
||||
|
||||
select -assert-none t:NX_DFF t:NX_LUT %% t:* %D
|
||||
|
||||
|
||||
design -load read
|
||||
hierarchy -top dffs
|
||||
proc
|
||||
equiv_opt -async2sync -assert -map +/nanoxplore/cells_sim.v synth_nanoxplore -noiopad # equivalency check
|
||||
design -load postopt # load the post-opt design (otherwise equiv_opt loads the pre-opt design)
|
||||
cd dffs # Constrain all select calls below inside the top module
|
||||
select -assert-count 1 t:NX_DFF
|
||||
select -assert-count 1 t:NX_LUT
|
||||
|
||||
select -assert-none t:NX_DFF t:NX_LUT %% t:* %D
|
||||
|
||||
|
||||
design -load read
|
||||
hierarchy -top ndffnr
|
||||
proc
|
||||
equiv_opt -async2sync -assert -map +/nanoxplore/cells_sim.v synth_nanoxplore -noiopad # equivalency check
|
||||
design -load postopt # load the post-opt design (otherwise equiv_opt loads the pre-opt design)
|
||||
cd ndffnr # Constrain all select calls below inside the top module
|
||||
select -assert-count 1 t:NX_DFF
|
||||
select -assert-count 1 t:NX_LUT
|
||||
|
||||
select -assert-none t:NX_DFF t:NX_LUT %% t:* %D
|
||||
22
tests/arch/nanoxplore/dffs.ys
Normal file
22
tests/arch/nanoxplore/dffs.ys
Normal file
|
|
@ -0,0 +1,22 @@
|
|||
read_verilog ../common/dffs.v
|
||||
design -save read
|
||||
|
||||
hierarchy -top dff
|
||||
proc
|
||||
equiv_opt -assert -async2sync -map +/nanoxplore/cells_sim.v synth_nanoxplore -noiopad # equivalency check
|
||||
design -load postopt # load the post-opt design (otherwise equiv_opt loads the pre-opt design)
|
||||
cd dff # Constrain all select calls below inside the top module
|
||||
select -assert-count 1 t:NX_DFF
|
||||
|
||||
select -assert-none t:NX_DFF %% t:* %D
|
||||
|
||||
design -load read
|
||||
hierarchy -top dffe
|
||||
proc
|
||||
equiv_opt -assert -async2sync -map +/nanoxplore/cells_sim.v synth_nanoxplore -noiopad -min_ce_use 0 # equivalency check
|
||||
design -load postopt # load the post-opt design (otherwise equiv_opt loads the pre-opt design)
|
||||
cd dffe # Constrain all select calls below inside the top module
|
||||
stat
|
||||
select -assert-count 1 t:NX_DFF
|
||||
|
||||
select -assert-none t:NX_DFF %% t:* %D
|
||||
16
tests/arch/nanoxplore/fsm.ys
Normal file
16
tests/arch/nanoxplore/fsm.ys
Normal file
|
|
@ -0,0 +1,16 @@
|
|||
read_verilog ../common/fsm.v
|
||||
hierarchy -top fsm
|
||||
proc
|
||||
flatten
|
||||
|
||||
equiv_opt -run :prove -map +/nanoxplore/cells_sim.v synth_nanoxplore -noiopad
|
||||
async2sync
|
||||
miter -equiv -make_assert -flatten gold gate miter
|
||||
sat -verify -prove-asserts -show-public -set-at 1 in_reset 1 -seq 20 -prove-skip 1 miter
|
||||
|
||||
design -load postopt # load the post-opt design (otherwise equiv_opt loads the pre-opt design)
|
||||
cd fsm # Constrain all select calls below inside the top module
|
||||
|
||||
select -assert-count 6 t:NX_DFF
|
||||
select -assert-min 13 t:NX_LUT
|
||||
select -assert-none t:NX_DFF t:NX_LUT %% t:* %D
|
||||
33
tests/arch/nanoxplore/latches.ys
Normal file
33
tests/arch/nanoxplore/latches.ys
Normal file
|
|
@ -0,0 +1,33 @@
|
|||
read_verilog ../common/latches.v
|
||||
design -save read
|
||||
|
||||
hierarchy -top latchp
|
||||
proc
|
||||
# Can't run any sort of equivalence check because latches are blown to LUTs
|
||||
synth_nanoxplore -noiopad
|
||||
cd latchp # Constrain all select calls below inside the top module
|
||||
select -assert-count 1 t:NX_LUT
|
||||
|
||||
select -assert-none t:NX_LUT %% t:* %D
|
||||
|
||||
|
||||
design -load read
|
||||
hierarchy -top latchn
|
||||
proc
|
||||
# Can't run any sort of equivalence check because latches are blown to LUTs
|
||||
synth_nanoxplore -noiopad
|
||||
cd latchn # Constrain all select calls below inside the top module
|
||||
select -assert-count 1 t:NX_LUT
|
||||
|
||||
select -assert-none t:NX_LUT %% t:* %D
|
||||
|
||||
|
||||
design -load read
|
||||
hierarchy -top latchsr
|
||||
proc
|
||||
# Can't run any sort of equivalence check because latches are blown to LUTs
|
||||
synth_nanoxplore -noiopad
|
||||
cd latchsr # Constrain all select calls below inside the top module
|
||||
select -assert-count 2 t:NX_LUT
|
||||
|
||||
select -assert-none t:NX_LUT %% t:* %D
|
||||
9
tests/arch/nanoxplore/logic.ys
Normal file
9
tests/arch/nanoxplore/logic.ys
Normal file
|
|
@ -0,0 +1,9 @@
|
|||
read_verilog ../common/logic.v
|
||||
hierarchy -top top
|
||||
proc
|
||||
equiv_opt -assert -map +/nanoxplore/cells_sim.v synth_nanoxplore -noiopad # equivalency check
|
||||
design -load postopt # load the post-opt design (otherwise equiv_opt loads the pre-opt design)
|
||||
cd top # Constrain all select calls below inside the top module
|
||||
|
||||
select -assert-count 9 t:NX_LUT
|
||||
select -assert-none t:NX_LUT %% t:* %D
|
||||
145
tests/arch/nanoxplore/lutram.ys
Normal file
145
tests/arch/nanoxplore/lutram.ys
Normal file
|
|
@ -0,0 +1,145 @@
|
|||
# Dual-port RAMs.
|
||||
# NX_RFB_U in mode 0 (DPREG)
|
||||
|
||||
read_verilog <<EOT
|
||||
module lutram_dpreg
|
||||
#(parameter D_WIDTH=18, A_WIDTH=5)
|
||||
(
|
||||
input [D_WIDTH-1:0] data,
|
||||
input [A_WIDTH:1] addr_w, addr_r,
|
||||
input we, clk,
|
||||
output reg [D_WIDTH-1:0] q
|
||||
);
|
||||
// Declare the RAM variable
|
||||
reg [D_WIDTH-1:0] ram[(2**A_WIDTH)-1:0];
|
||||
|
||||
// Port A
|
||||
always @ (posedge clk)
|
||||
begin
|
||||
if (we)
|
||||
ram[addr_w] <= data;
|
||||
q <= ram[addr_r];
|
||||
end
|
||||
endmodule
|
||||
EOT
|
||||
|
||||
hierarchy -top lutram_dpreg
|
||||
proc
|
||||
memory -nomap
|
||||
equiv_opt -run :prove -map +/nanoxplore/cells_sim.v -map +/nanoxplore/cells_sim_u.v synth_nanoxplore -noiopad
|
||||
memory
|
||||
opt -full
|
||||
|
||||
miter -equiv -flatten -make_assert -make_outputs gold gate miter
|
||||
sat -verify -prove-asserts -seq 3 -set-init-zero -show-inputs -show-outputs miter
|
||||
|
||||
design -load postopt
|
||||
cd lutram_dpreg
|
||||
stat
|
||||
select -assert-count 1 t:NX_RFB_U r:mode=0 %i
|
||||
select -assert-count 18 t:NX_DFF
|
||||
select -assert-none t:NX_RFB_U t:NX_DFF %% t:* %D
|
||||
|
||||
# Single-port RAMs.
|
||||
# NX_RFB_U in mode 1 (SPREG)
|
||||
design -reset
|
||||
|
||||
read_verilog ../common/lutram.v
|
||||
hierarchy -top lutram_1w1r -chparam A_WIDTH 5 -chparam D_WIDTH 18
|
||||
proc
|
||||
memory -nomap
|
||||
equiv_opt -run :prove -map +/nanoxplore/cells_sim.v -map +/nanoxplore/cells_sim_u.v synth_nanoxplore -noiopad
|
||||
memory
|
||||
opt -full
|
||||
|
||||
miter -equiv -flatten -make_assert -make_outputs gold gate miter
|
||||
sat -verify -prove-asserts -seq 3 -set-init-zero -show-inputs -show-outputs miter
|
||||
|
||||
design -load postopt
|
||||
cd lutram_1w1r
|
||||
select -assert-count 1 t:NX_RFB_U r:mode=1 %i
|
||||
select -assert-count 18 t:NX_DFF
|
||||
select -assert-none t:NX_RFB_U t:NX_DFF %% t:* %D
|
||||
|
||||
# Dual-port RAMs.
|
||||
# NX_RFB_U in mode 2 (NX_XRFB_64x18)
|
||||
design -reset
|
||||
read_verilog ../common/lutram.v
|
||||
hierarchy -top lutram_1w1r -chparam A_WIDTH 6 -chparam D_WIDTH 18
|
||||
proc
|
||||
memory -nomap
|
||||
equiv_opt -run :prove -map +/nanoxplore/cells_sim.v -map +/nanoxplore/cells_sim_u.v synth_nanoxplore -noiopad
|
||||
memory
|
||||
opt -full
|
||||
|
||||
miter -equiv -flatten -make_assert -make_outputs gold gate miter
|
||||
sat -verify -prove-asserts -seq 3 -set-init-zero -show-inputs -show-outputs miter
|
||||
|
||||
design -load postopt
|
||||
cd lutram_1w1r
|
||||
select -assert-count 1 t:NX_RFB_U r:mode=2 %i
|
||||
select -assert-count 18 t:NX_DFF
|
||||
select -assert-none t:NX_RFB_U t:NX_DFF %% t:* %D
|
||||
|
||||
# Dual-port RAMs.
|
||||
# NX_RFB_U in mode 3 (NX_XRFB_32x36)
|
||||
design -reset
|
||||
read_verilog ../common/lutram.v
|
||||
hierarchy -top lutram_1w1r -chparam A_WIDTH 5 -chparam D_WIDTH 36
|
||||
proc
|
||||
memory -nomap
|
||||
equiv_opt -run :prove -map +/nanoxplore/cells_sim.v -map +/nanoxplore/cells_sim_u.v synth_nanoxplore -noiopad
|
||||
memory
|
||||
opt -full
|
||||
|
||||
miter -equiv -flatten -make_assert -make_outputs gold gate miter
|
||||
sat -verify -prove-asserts -seq 3 -set-init-zero -show-inputs -show-outputs miter
|
||||
|
||||
design -load postopt
|
||||
cd lutram_1w1r
|
||||
select -assert-count 1 t:NX_RFB_U r:mode=3 %i
|
||||
select -assert-count 36 t:NX_DFF
|
||||
select -assert-none t:NX_RFB_U t:NX_DFF %% t:* %D
|
||||
|
||||
# Single write dual read RAMs.
|
||||
# NX_RFB_U in mode 4 (NX_XRFB_2R_1W)
|
||||
design -reset
|
||||
|
||||
read_verilog <<EOT
|
||||
module lutram_1w2r
|
||||
#(parameter D_WIDTH=8, A_WIDTH=5)
|
||||
(
|
||||
input [D_WIDTH-1:0] data_a, data_b,
|
||||
input [A_WIDTH:1] addr_a, addr_b,
|
||||
input we_a, clk,
|
||||
output reg [D_WIDTH-1:0] q_a, q_b
|
||||
);
|
||||
// Declare the RAM variable
|
||||
reg [D_WIDTH-1:0] ram[(2**A_WIDTH)-1:0];
|
||||
|
||||
// Port A
|
||||
always @ (posedge clk)
|
||||
begin
|
||||
if (we_a)
|
||||
ram[addr_a] <= data_a;
|
||||
q_a <= ram[addr_a];
|
||||
q_b <= ram[addr_b];
|
||||
end
|
||||
endmodule
|
||||
EOT
|
||||
|
||||
hierarchy -top lutram_1w2r -chparam A_WIDTH 5 -chparam D_WIDTH 18
|
||||
proc
|
||||
memory -nomap
|
||||
equiv_opt -run :prove -map +/nanoxplore/cells_sim.v -map +/nanoxplore/cells_sim_u.v synth_nanoxplore -noiopad
|
||||
memory
|
||||
opt -full
|
||||
|
||||
miter -equiv -flatten -make_assert -make_outputs gold gate miter
|
||||
sat -verify -prove-asserts -seq 3 -set-init-zero -show-inputs -show-outputs miter
|
||||
|
||||
design -load postopt
|
||||
cd lutram_1w2r
|
||||
select -assert-count 1 t:NX_RFB_U r:mode=4 %i
|
||||
select -assert-count 36 t:NX_DFF
|
||||
select -assert-none t:NX_RFB_U t:NX_DFF %% t:* %D
|
||||
50
tests/arch/nanoxplore/meminit.v
Normal file
50
tests/arch/nanoxplore/meminit.v
Normal file
|
|
@ -0,0 +1,50 @@
|
|||
module top(clk);
|
||||
parameter DEPTH_LOG2 = 10;
|
||||
parameter WIDTH = 36;
|
||||
parameter PRIME = 237481091;
|
||||
localparam DEPTH = 2**DEPTH_LOG2;
|
||||
|
||||
input wire clk;
|
||||
|
||||
(* syn_ramstyle = "distributed" *)
|
||||
reg [WIDTH-1:0] mem [DEPTH-1:0];
|
||||
|
||||
integer i;
|
||||
initial begin
|
||||
for (i = 0; i < DEPTH; i = i + 1) begin
|
||||
// Make up data by multiplying a large prime with the address,
|
||||
// then cropping and retaining the lower bits
|
||||
mem[i] = PRIME * (i*2+1);
|
||||
end
|
||||
end
|
||||
|
||||
reg [DEPTH_LOG2-1:0] counter = 0;
|
||||
reg done = 1'b0;
|
||||
|
||||
reg did_read = 1'b0;
|
||||
reg [DEPTH_LOG2-1:0] read_addr;
|
||||
reg [WIDTH-1:0] read_val;
|
||||
|
||||
always @(posedge clk) begin
|
||||
if (!done) begin
|
||||
did_read <= 1'b1;
|
||||
read_addr <= counter;
|
||||
read_val <= mem[counter];
|
||||
end else begin
|
||||
did_read <= 1'b0;
|
||||
end
|
||||
|
||||
if (!done)
|
||||
counter = counter + 1;
|
||||
if (counter == 0)
|
||||
done = 1;
|
||||
end
|
||||
|
||||
wire [WIDTH-1:0] expect_val = PRIME * (read_addr*2+1);
|
||||
always @(posedge clk) begin
|
||||
if (did_read) begin
|
||||
$display("addr %x expected %x actual %x", read_addr, expect_val, read_val);
|
||||
assert(read_val == expect_val);
|
||||
end
|
||||
end
|
||||
endmodule
|
||||
44
tests/arch/nanoxplore/meminit.ys
Normal file
44
tests/arch/nanoxplore/meminit.ys
Normal file
|
|
@ -0,0 +1,44 @@
|
|||
read_verilog -sv meminit.v
|
||||
chparam -set DEPTH_LOG2 5 -set WIDTH 36
|
||||
prep
|
||||
opt_dff
|
||||
prep -rdff
|
||||
synth_nanoxplore
|
||||
clean_zerowidth
|
||||
select -assert-none t:$mem_v2 t:$mem
|
||||
read_verilog +/nanoxplore/cells_sim.v +/nanoxplore/cells_sim_u.v
|
||||
prep
|
||||
async2sync
|
||||
hierarchy -top top
|
||||
sim -assert -q -n 66 -clock clk
|
||||
|
||||
design -reset
|
||||
read_verilog -sv meminit.v
|
||||
chparam -set DEPTH_LOG2 6 -set WIDTH 18
|
||||
prep
|
||||
opt_dff
|
||||
prep -rdff
|
||||
synth_nanoxplore
|
||||
clean_zerowidth
|
||||
select -assert-none t:$mem_v2 t:$mem
|
||||
read_verilog +/nanoxplore/cells_sim.v +/nanoxplore/cells_sim_u.v
|
||||
prep
|
||||
async2sync
|
||||
hierarchy -top top
|
||||
sim -assert -q -n 34 -clock clk
|
||||
|
||||
|
||||
design -reset
|
||||
read_verilog -sv meminit.v
|
||||
chparam -set DEPTH_LOG2 8 -set WIDTH 18
|
||||
prep
|
||||
opt_dff
|
||||
prep -rdff
|
||||
synth_nanoxplore
|
||||
clean_zerowidth
|
||||
select -assert-none t:$mem_v2 t:$mem
|
||||
read_verilog +/nanoxplore/cells_sim.v +/nanoxplore/cells_sim_u.v
|
||||
prep
|
||||
async2sync
|
||||
hierarchy -top top
|
||||
sim -assert -q -n 258 -clock clk
|
||||
41
tests/arch/nanoxplore/mux.ys
Normal file
41
tests/arch/nanoxplore/mux.ys
Normal file
|
|
@ -0,0 +1,41 @@
|
|||
read_verilog ../common/mux.v
|
||||
design -save read
|
||||
|
||||
hierarchy -top mux2
|
||||
proc
|
||||
equiv_opt -assert -map +/nanoxplore/cells_sim.v synth_nanoxplore -noiopad # equivalency check
|
||||
design -load postopt # load the post-opt design (otherwise equiv_opt loads the pre-opt design)
|
||||
cd mux2 # Constrain all select calls below inside the top module
|
||||
select -assert-count 1 t:NX_LUT
|
||||
|
||||
select -assert-none t:NX_LUT %% t:* %D
|
||||
|
||||
design -load read
|
||||
hierarchy -top mux4
|
||||
proc
|
||||
equiv_opt -assert -map +/nanoxplore/cells_sim.v synth_nanoxplore -noiopad # equivalency check
|
||||
design -load postopt # load the post-opt design (otherwise equiv_opt loads the pre-opt design)
|
||||
cd mux4 # Constrain all select calls below inside the top module
|
||||
#select -assert-count 2 t:NX_LUT
|
||||
|
||||
select -assert-none t:NX_LUT %% t:* %D
|
||||
|
||||
design -load read
|
||||
hierarchy -top mux8
|
||||
proc
|
||||
equiv_opt -assert -map +/nanoxplore/cells_sim.v synth_nanoxplore -noiopad # equivalency check
|
||||
design -load postopt # load the post-opt design (otherwise equiv_opt loads the pre-opt design)
|
||||
cd mux8 # Constrain all select calls below inside the top module
|
||||
#select -assert-count 5 t:NX_LUT
|
||||
|
||||
select -assert-none t:NX_LUT %% t:* %D
|
||||
|
||||
design -load read
|
||||
hierarchy -top mux16
|
||||
proc
|
||||
equiv_opt -assert -map +/nanoxplore/cells_sim.v synth_nanoxplore -noiopad # equivalency check
|
||||
design -load postopt # load the post-opt design (otherwise equiv_opt loads the pre-opt design)
|
||||
cd mux16 # Constrain all select calls below inside the top module
|
||||
select -assert-max 13 t:NX_LUT
|
||||
|
||||
select -assert-none t:NX_LUT %% t:* %D
|
||||
4
tests/arch/nanoxplore/run-test.sh
Executable file
4
tests/arch/nanoxplore/run-test.sh
Executable file
|
|
@ -0,0 +1,4 @@
|
|||
#!/usr/bin/env bash
|
||||
set -eu
|
||||
source ../../gen-tests-makefile.sh
|
||||
run_tests --yosys-scripts --bash --yosys-args "-w 'Yosys has only limited support for tri-state logic at the moment.'"
|
||||
10
tests/arch/nanoxplore/shifter.ys
Normal file
10
tests/arch/nanoxplore/shifter.ys
Normal file
|
|
@ -0,0 +1,10 @@
|
|||
read_verilog ../common/shifter.v
|
||||
hierarchy -top top
|
||||
proc
|
||||
flatten
|
||||
equiv_opt -async2sync -assert -map +/nanoxplore/cells_sim.v synth_nanoxplore -noiopad # equivalency check
|
||||
design -load postopt # load the post-opt design (otherwise equiv_opt loads the pre-opt design)
|
||||
cd top # Constrain all select calls below inside the top module
|
||||
|
||||
select -assert-count 8 t:NX_DFF
|
||||
select -assert-none t:NX_DFF %% t:* %D
|
||||
13
tests/arch/nanoxplore/tribuf.ys
Normal file
13
tests/arch/nanoxplore/tribuf.ys
Normal file
|
|
@ -0,0 +1,13 @@
|
|||
read_verilog ../common/tribuf.v
|
||||
hierarchy -top tristate
|
||||
proc
|
||||
tribuf
|
||||
flatten
|
||||
synth
|
||||
equiv_opt -assert -map +/nanoxplore/cells_sim.v -map +/simcells.v synth_nanoxplore # equivalency check
|
||||
design -load postopt # load the post-opt design (otherwise equiv_opt loads the pre-opt design)
|
||||
cd tristate # Constrain all select calls below inside the top module
|
||||
#Internal cell type used. Need support it.
|
||||
select -assert-count 1 t:NX_IOB
|
||||
select -assert-count 2 t:NX_IOB_I
|
||||
select -assert-none t:NX_IOB t:NX_IOB_I %% t:* %D
|
||||
80
tests/proc/proc_dff.ys
Normal file
80
tests/proc/proc_dff.ys
Normal file
|
|
@ -0,0 +1,80 @@
|
|||
read_verilog -formal <<EOT
|
||||
// From https://github.com/YosysHQ/yosys/pull/4568#issuecomment-2313740948
|
||||
|
||||
module top(input clk, a, b, c, input [1:0] d, output reg [1:0] q);
|
||||
|
||||
always @(posedge clk, posedge a, posedge b, posedge c) begin
|
||||
if (a) q <= '0;
|
||||
else if (b) q <= 2'b10;
|
||||
else if (c) q <= '0;
|
||||
else q <= d;
|
||||
end
|
||||
|
||||
always @* begin
|
||||
if (a) assert(q == '0);
|
||||
else if (b) assert(q == 2'b10);
|
||||
else if (c) assert(q == '0);
|
||||
end
|
||||
|
||||
endmodule
|
||||
EOT
|
||||
|
||||
proc
|
||||
select -assert-count 1 t:$dffsr
|
||||
clk2fflogic
|
||||
select -assert-count 3 t:$assert
|
||||
sat -tempinduct -verify -prove-asserts
|
||||
|
||||
design -reset
|
||||
|
||||
read_verilog -formal <<EOT
|
||||
// Tests aload combined with reset. The aload gets refactored into the set/reset
|
||||
// logic
|
||||
module top(input clk, rst, aload_n, input [1:0] l, d, output reg [1:0] q);
|
||||
|
||||
always @(posedge clk, posedge rst, negedge aload_n) begin
|
||||
if (rst) q <= '0;
|
||||
else if (!aload_n) q <= l;
|
||||
else q <= d;
|
||||
end
|
||||
|
||||
always @* begin
|
||||
if (rst) assert(q == '0);
|
||||
else if (!aload_n) assert(q == l);
|
||||
end
|
||||
|
||||
endmodule
|
||||
EOT
|
||||
|
||||
proc
|
||||
select -assert-count 1 t:$dffsr
|
||||
clk2fflogic
|
||||
select -assert-count 2 t:$assert
|
||||
sat -tempinduct -verify -prove-asserts
|
||||
|
||||
design -reset
|
||||
|
||||
read_verilog -formal <<EOT
|
||||
// Tests combining of common reset signals
|
||||
module top(input clk, rst_a, rst_b, rst_c, input [1:0] d, output reg [1:0] q);
|
||||
|
||||
always @(posedge clk, posedge rst_a, posedge rst_b, negedge rst_c) begin
|
||||
if (rst_a) q <= '1;
|
||||
else if (rst_b) q <= '1;
|
||||
else if (!rst_c) q <= '1;
|
||||
else q <= d;
|
||||
end
|
||||
|
||||
always @* if (rst_a || rst_b || !rst_c) assert(q == '1);
|
||||
|
||||
endmodule
|
||||
|
||||
EOT
|
||||
|
||||
proc
|
||||
select -assert-count 1 t:$adff
|
||||
clk2fflogic
|
||||
select -assert-count 1 t:$assert
|
||||
sat -tempinduct -verify -prove-asserts
|
||||
|
||||
design -reset
|
||||
Loading…
Add table
Add a link
Reference in a new issue