diff options
Diffstat (limited to 'tests/arch/xilinx')
| -rw-r--r-- | tests/arch/xilinx/lutram.ys | 40 |
1 files changed, 40 insertions, 0 deletions
diff --git a/tests/arch/xilinx/lutram.ys b/tests/arch/xilinx/lutram.ys index 9b2c30ba1..36367eff1 100644 --- a/tests/arch/xilinx/lutram.ys +++ b/tests/arch/xilinx/lutram.ys @@ -97,3 +97,43 @@ select -assert-count 1 t:BUFG select -assert-count 24 t:FDRE select -assert-count 8 t:RAM64M select -assert-none t:BUFG t:FDRE t:RAM64M %% t:* %D + + +design -reset +read_verilog ../common/lutram.v +hierarchy -top lutram_1w1r -chparam A_WIDTH 5 -chparam D_WIDTH 6 +proc +memory -nomap +equiv_opt -run :prove -map +/xilinx/cells_sim.v synth_xilinx +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:BUFG +select -assert-count 6 t:FDRE +select -assert-count 1 t:RAM32M +select -assert-none t:BUFG t:FDRE t:RAM32M %% t:* %D + + +design -reset +read_verilog ../common/lutram.v +hierarchy -top lutram_1w1r -chparam A_WIDTH 6 -chparam D_WIDTH 6 +proc +memory -nomap +equiv_opt -run :prove -map +/xilinx/cells_sim.v synth_xilinx +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:BUFG +select -assert-count 6 t:FDRE +select -assert-count 2 t:RAM64M +select -assert-none t:BUFG t:FDRE t:RAM64M %% t:* %D |