mirror of
https://github.com/YosysHQ/yosys
synced 2025-04-06 01:24:10 +00:00
331ac5285f
Right now neither `sat` nor `sim` have support for the `$check` cell. For formal verification it is a good idea to always run either async2sync or clk2fflogic which will (in a future commit) lower `$check` to `$assert`, etc. While `sim` should eventually support `$check` directly, using `async2sync` is ok for the current tests that use `sim`, so this commit also runs `async2sync` before running sim on designs containing assertions.
56 lines
1.3 KiB
Plaintext
56 lines
1.3 KiB
Plaintext
logger -nowarn "Yosys has only limited support for tri-state logic at the moment\. .*"
|
|
|
|
read_verilog <<EOT
|
|
module top(input [24:0] A, input [17:0] B, output [47:0] P);
|
|
DSP48E1 #(.PREG(0)) dsp(.A(A), .B(B), .P(P));
|
|
endmodule
|
|
EOT
|
|
techmap -autoproc -wb -map +/xilinx/cells_sim.v
|
|
opt
|
|
scc -expect 0
|
|
|
|
|
|
design -reset
|
|
read_verilog <<EOT
|
|
module top(input signed [24:0] A, input signed [17:0] B, output [47:0] P);
|
|
assign P = A * B;
|
|
endmodule
|
|
EOT
|
|
synth_xilinx -abc9
|
|
techmap -autoproc -wb -map +/xilinx/cells_sim.v
|
|
opt -full -fine
|
|
select -assert-count 1 t:$mul
|
|
select -assert-count 0 t:* t:$mul %D
|
|
|
|
|
|
design -reset
|
|
read_verilog -icells -formal <<EOT
|
|
module top(output [42:0] P);
|
|
\$__MUL25X18 mul (.A(42), .B(42), .Y(P));
|
|
assert property (P == 42*42);
|
|
endmodule
|
|
EOT
|
|
async2sync
|
|
techmap -map +/xilinx/xc7_dsp_map.v
|
|
verilog_defaults -add -D ALLOW_WHITEBOX_DSP48E1
|
|
synth_xilinx -abc9
|
|
techmap -autoproc -wb -map +/xilinx/cells_sim.v
|
|
opt -full -fine
|
|
select -assert-count 0 t:* t:$assert %d
|
|
sat -verify -prove-asserts
|
|
|
|
|
|
design -reset
|
|
read_verilog <<EOT
|
|
module top(input signed [29:0] A, input signed [17:0] B, output signed [47:0] P);
|
|
wire [47:0] casc;
|
|
DSP48E1 #(.AREG(1)) u1(.A(A), .B(B), .PCOUT(casc));
|
|
DSP48E1 #(.AREG(1)) u2(.A(A), .B(B), .PCIN(casc), .P(P));
|
|
endmodule
|
|
EOT
|
|
synth_xilinx -run :prepare
|
|
abc9
|
|
clean
|
|
check
|
|
logger -expect-no-warnings
|