mirror of
https://github.com/YosysHQ/yosys
synced 2025-06-29 01:18:46 +00:00
Start adding RFB simulation models
This commit is contained in:
parent
8eb099c1f4
commit
f4d8ea4c40
5 changed files with 240 additions and 114 deletions
|
@ -12,5 +12,5 @@ design -load postopt # load the post-opt design (otherwise equiv_opt loads the p
|
|||
cd fsm # Constrain all select calls below inside the top module
|
||||
|
||||
select -assert-count 6 t:NX_DFF
|
||||
select -assert-count 14 t:NX_LUT
|
||||
select -assert-min 13 t:NX_LUT
|
||||
select -assert-none t:NX_DFF t:NX_LUT %% t:* %D
|
||||
|
|
|
@ -1,8 +1,61 @@
|
|||
# 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
|
||||
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
|
||||
synth_nanoxplore
|
||||
proc
|
||||
memory -nomap
|
||||
equiv_opt -run :prove -map +/nanoxplore/cells_sim.v -map +/nanoxplore/cells_sim_u.v synth_nanoxplore
|
||||
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
|
||||
|
@ -13,9 +66,17 @@ select -assert-none t:NX_RFB_U t:NX_DFF %% t:* %D
|
|||
design -reset
|
||||
read_verilog ../common/lutram.v
|
||||
hierarchy -top lutram_1w1r -chparam A_WIDTH 6 -chparam D_WIDTH 18
|
||||
synth_nanoxplore
|
||||
proc
|
||||
memory -nomap
|
||||
equiv_opt -run :prove -map +/nanoxplore/cells_sim.v -map +/nanoxplore/cells_sim_u.v synth_nanoxplore
|
||||
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
|
||||
stat
|
||||
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
|
||||
|
@ -25,7 +86,16 @@ select -assert-none t:NX_RFB_U t:NX_DFF %% t:* %D
|
|||
design -reset
|
||||
read_verilog ../common/lutram.v
|
||||
hierarchy -top lutram_1w1r -chparam A_WIDTH 5 -chparam D_WIDTH 36
|
||||
synth_nanoxplore
|
||||
proc
|
||||
memory -nomap
|
||||
equiv_opt -run :prove -map +/nanoxplore/cells_sim.v -map +/nanoxplore/cells_sim_u.v synth_nanoxplore
|
||||
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
|
||||
|
@ -39,8 +109,8 @@ read_verilog <<EOT
|
|||
module lutram_1w2r
|
||||
#(parameter D_WIDTH=8, A_WIDTH=5)
|
||||
(
|
||||
input [D_WIDTH-1:0] data_a, data_b, data_c,
|
||||
input [A_WIDTH:1] addr_a, addr_b, addr_c,
|
||||
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
|
||||
);
|
||||
|
@ -59,7 +129,16 @@ endmodule
|
|||
EOT
|
||||
|
||||
hierarchy -top lutram_1w2r -chparam A_WIDTH 5 -chparam D_WIDTH 18
|
||||
synth_nanoxplore
|
||||
proc
|
||||
memory -nomap
|
||||
equiv_opt -run :prove -map +/nanoxplore/cells_sim.v -map +/nanoxplore/cells_sim_u.v synth_nanoxplore
|
||||
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
|
||||
|
|
Loading…
Add table
Add a link
Reference in a new issue