mirror of
https://github.com/YosysHQ/yosys
synced 2026-07-15 11:45:41 +00:00
250 lines
6.1 KiB
Text
250 lines
6.1 KiB
Text
##################################################################
|
|
|
|
read_verilog -sv -icells <<EOT
|
|
|
|
module top(input E, D, S, R, output [9:0] Q);
|
|
|
|
$_DLATCH_P_ latch0 (.E(E), .D(D), .Q(Q[0]));
|
|
$_DLATCH_PP0_ latch1 (.E(E), .D(D), .R(R), .Q(Q[1]));
|
|
$_DLATCH_PP1_ latch2 (.E(E), .D(D), .R(R), .Q(Q[2]));
|
|
|
|
assume property (~R || ~S);
|
|
$_DLATCHSR_PPP_ latch3 (.E(E), .D(D), .R( R), .S( S), .Q(Q[3]));
|
|
$_DLATCHSR_NNN_ latch4 (.E(E), .D(D), .R(~R), .S(~S), .Q(Q[4]));
|
|
|
|
assign Q[9:5] = ~Q[4:0];
|
|
|
|
endmodule
|
|
|
|
EOT
|
|
|
|
proc
|
|
opt
|
|
read_liberty dlatchlibmap_dlatchsr_s.lib
|
|
|
|
copy top top_unmapped
|
|
dfflibmap -liberty dlatchlibmap_dlatchsr_s.lib top
|
|
|
|
clk2fflogic
|
|
flatten
|
|
opt_clean -purge
|
|
miter -equiv -make_assert -flatten top_unmapped top miter
|
|
hierarchy -top miter
|
|
# Prove that this is equivalent with the assumption
|
|
sat -verify -prove-asserts -set-assumes -enable_undef -set-init-undef -show-public -seq 3 miter
|
|
# Prove that this is NOT equivalent WITHOUT the assumption
|
|
sat -falsify -prove-asserts -enable_undef -set-init-undef -seq 3 miter
|
|
|
|
##################################################################
|
|
|
|
design -reset
|
|
read_verilog -sv -icells <<EOT
|
|
|
|
module top(input E, D, S, R, output [9:0] Q);
|
|
|
|
$_DLATCH_P_ latch0 (.E(E), .D(D), .Q(Q[0]));
|
|
$_DLATCH_PP0_ latch1 (.E(E), .D(D), .R(R), .Q(Q[1]));
|
|
$_DLATCH_PP1_ latch2 (.E(E), .D(D), .R(R), .Q(Q[2]));
|
|
|
|
assume property (~R || ~S);
|
|
$_DLATCHSR_PPP_ latch3 (.E(E), .D(D), .R( R), .S( S), .Q(Q[3]));
|
|
$_DLATCHSR_NNN_ latch4 (.E(E), .D(D), .R(~R), .S(~S), .Q(Q[4]));
|
|
|
|
assign Q[9:5] = ~Q[4:0];
|
|
|
|
endmodule
|
|
|
|
EOT
|
|
|
|
proc
|
|
opt
|
|
read_liberty dlatchlibmap_dlatchsr_r.lib
|
|
|
|
copy top top_unmapped
|
|
dfflibmap -liberty dlatchlibmap_dlatchsr_r.lib top
|
|
|
|
clk2fflogic
|
|
flatten
|
|
opt_clean -purge
|
|
miter -equiv -make_assert -flatten top_unmapped top miter
|
|
hierarchy -top miter
|
|
# Prove that this is equivalent with the assumption
|
|
sat -verify -prove-asserts -set-assumes -enable_undef -set-init-undef -show-public -seq 3 miter
|
|
# Prove that this is NOT equivalent WITHOUT the assumption
|
|
sat -falsify -prove-asserts -enable_undef -set-init-undef -seq 3 miter
|
|
|
|
##################################################################
|
|
|
|
design -reset
|
|
read_verilog -sv -icells <<EOT
|
|
|
|
module top(input E, D, S, R, output [9:0] Q);
|
|
|
|
$_DLATCH_P_ latch0 (.E(E), .D(D), .Q(Q[0]));
|
|
$_DLATCH_PP0_ latch1 (.E(E), .D(D), .R(R), .Q(Q[1]));
|
|
$_DLATCH_PP1_ latch2 (.E(E), .D(D), .R(R), .Q(Q[2]));
|
|
|
|
// no assume when mapping to X
|
|
$_DLATCHSR_PPP_ latch3 (.E(E), .D(D), .R( R), .S( S), .Q(Q[3]));
|
|
$_DLATCHSR_NNN_ latch4 (.E(E), .D(D), .R(~R), .S(~S), .Q(Q[4]));
|
|
|
|
assign Q[9:5] = ~Q[4:0];
|
|
|
|
endmodule
|
|
|
|
EOT
|
|
|
|
proc
|
|
opt
|
|
read_liberty dlatchlibmap_dlatchsr_x.lib
|
|
opt
|
|
|
|
copy top top_unmapped
|
|
dfflibmap -liberty dlatchlibmap_dlatchsr_x.lib top
|
|
|
|
clk2fflogic
|
|
flatten
|
|
opt_clean -purge
|
|
miter -equiv -make_assert -flatten top_unmapped top miter
|
|
hierarchy -top miter
|
|
|
|
# Prove that this is equivalent
|
|
sat -verify -prove-asserts -set-init-undef -show-public -seq 3 miter
|
|
|
|
##################################################################
|
|
|
|
design -reset
|
|
read_verilog -sv -icells <<EOT
|
|
|
|
module top(input E, D, S, R, output [9:0] Q);
|
|
|
|
$_DLATCH_P_ latch0 (.E(E), .D(D), .Q(Q[0]));
|
|
$_DLATCH_PP0_ latch1 (.E(E), .D(D), .R(R), .Q(Q[1]));
|
|
$_DLATCH_PP1_ latch2 (.E(E), .D(D), .R(R), .Q(Q[2]));
|
|
|
|
// no assume when mapping to unset clear_preset_var
|
|
$_DLATCHSR_PPP_ latch3 (.E(E), .D(D), .R( R), .S( S), .Q(Q[3]));
|
|
$_DLATCHSR_NNN_ latch4 (.E(E), .D(D), .R(~R), .S(~S), .Q(Q[4]));
|
|
|
|
assign Q[9:5] = ~Q[4:0];
|
|
|
|
endmodule
|
|
|
|
EOT
|
|
|
|
proc
|
|
opt
|
|
read_liberty dlatchlibmap_dlatchn.lib
|
|
read_liberty dlatchlibmap_dlatchsr_not_data.lib
|
|
|
|
copy top top_unmapped
|
|
dfflibmap -liberty dlatchlibmap_dlatchn.lib -liberty dlatchlibmap_dlatchsr_not_data.lib top
|
|
|
|
clk2fflogic
|
|
flatten
|
|
opt_clean -purge
|
|
miter -equiv -make_assert -flatten top_unmapped top miter
|
|
hierarchy -top miter
|
|
|
|
# Prove that this is equivalent
|
|
sat -verify -prove-asserts -set-init-undef -show-public -seq 3 miter
|
|
|
|
##################################################################
|
|
|
|
design -reset
|
|
read_verilog -sv -icells <<EOT
|
|
|
|
module top(input E, D, S, R, output [9:0] Q);
|
|
|
|
$_DLATCH_P_ latch0 (.E(E), .D(D), .Q(Q[0]));
|
|
$_DLATCH_PP0_ latch1 (.E(E), .D(D), .R(R), .Q(Q[1]));
|
|
$_DLATCH_PP1_ latch2 (.E(E), .D(D), .R(R), .Q(Q[2]));
|
|
|
|
assume property (~R || ~S);
|
|
$_DLATCHSR_PPP_ latch3 (.E(E), .D(D), .R( R), .S( S), .Q(Q[3]));
|
|
$_DLATCHSR_NNN_ latch4 (.E(E), .D(D), .R(~R), .S(~S), .Q(Q[4]));
|
|
|
|
assign Q[9:5] = ~Q[4:0];
|
|
|
|
endmodule
|
|
|
|
EOT
|
|
|
|
proc
|
|
opt
|
|
read_liberty dlatchlibmap_dlatchsr_not_data_l.lib
|
|
|
|
copy top top_unmapped
|
|
dfflibmap -liberty dlatchlibmap_dlatchsr_not_data_l.lib top
|
|
|
|
clk2fflogic
|
|
flatten
|
|
opt_clean -purge
|
|
miter -equiv -make_assert -flatten top_unmapped top miter
|
|
hierarchy -top miter
|
|
|
|
# Prove that this is equivalent with the assumption
|
|
sat -verify -prove-asserts -set-assumes -enable_undef -set-init-undef -show-public -seq 3 miter
|
|
# Prove that this is NOT equivalent WITHOUT the assumption
|
|
sat -falsify -prove-asserts -enable_undef -set-init-undef -seq 3 miter
|
|
|
|
##################################################################
|
|
|
|
design -reset
|
|
read_verilog <<EOT
|
|
|
|
module top(input E, D, S, R, output Q);
|
|
// DLATCHSR with priority R over S
|
|
always @*
|
|
if (R) Q <= 1'b0;
|
|
else if (S) Q <= 1'b1;
|
|
else if (E) Q <= D;
|
|
endmodule
|
|
|
|
EOT
|
|
|
|
proc
|
|
opt
|
|
read_liberty dlatchlibmap_dlatchn.lib
|
|
read_liberty dlatchlibmap_dlatchsr_not_data.lib
|
|
|
|
copy top top_unmapped
|
|
simplemap top
|
|
dfflibmap -liberty dlatchlibmap_dlatchn.lib -liberty dlatchlibmap_dlatchsr_not_data.lib top
|
|
|
|
clk2fflogic
|
|
flatten
|
|
opt_clean -purge
|
|
equiv_make top top_unmapped equiv
|
|
equiv_induct -set-assumes equiv
|
|
equiv_status -assert equiv
|
|
|
|
##################################################################
|
|
|
|
design -reset
|
|
read_verilog <<EOT
|
|
|
|
module top(input E, D, R, output Q);
|
|
// DLATCH with preset
|
|
always @*
|
|
if (~R) Q <= 1'b1;
|
|
else if (E) Q <= D;
|
|
endmodule
|
|
|
|
EOT
|
|
|
|
proc
|
|
opt
|
|
read_liberty dlatchlibmap_dlatchn.lib
|
|
read_liberty dlatchlibmap_dlatch_not_data.lib
|
|
|
|
copy top top_unmapped
|
|
simplemap top
|
|
dfflibmap -liberty dlatchlibmap_dlatchn.lib -liberty dlatchlibmap_dlatch_not_data.lib top
|
|
|
|
clk2fflogic
|
|
flatten
|
|
opt_clean -purge
|
|
equiv_make top top_unmapped equiv
|
|
equiv_induct -set-assumes equiv
|
|
equiv_status -assert equiv
|