mirror of https://github.com/YosysHQ/yosys.git
dlatchlibmap: modified copies of dfflibmap* test files for dlatchlibmap tests
This commit is contained in:
Iztok Jeras
parent
69df81756c
commit
0df2169f81
|
|
@ -1,30 +1,18 @@
|
|||
module dffn(input CLK, D, output reg Q, output QN);
|
||||
module dlatchn(input ENA, D, output reg Q, output QN);
|
||||
|
||||
always @(negedge CLK)
|
||||
Q <= D;
|
||||
always @*
|
||||
if (~ENA) Q <= D;
|
||||
|
||||
assign QN = ~Q;
|
||||
|
||||
endmodule
|
||||
|
||||
module dffsr(input CLK, D, CLEAR, PRESET, output reg Q, output QN);
|
||||
module dlatchsr(input ENA, D, CLEAR, PRESET, output reg Q, output QN);
|
||||
|
||||
always @(posedge CLK, posedge CLEAR, posedge PRESET)
|
||||
if (CLEAR)
|
||||
Q <= 0;
|
||||
else if (PRESET)
|
||||
Q <= 1;
|
||||
else
|
||||
Q <= D;
|
||||
|
||||
assign QN = ~Q;
|
||||
|
||||
endmodule
|
||||
|
||||
module dffe(input CLK, EN, D, output reg Q, output QN);
|
||||
|
||||
always @(negedge CLK)
|
||||
if (EN) Q <= D;
|
||||
always @*
|
||||
if (CLEAR) Q <= 1'b0;
|
||||
else if (PRESET) Q <= 1'b1;
|
||||
else if (ENA) Q <= D;
|
||||
|
||||
assign QN = ~Q;
|
||||
|
||||
|
|
|
|||
|
|
@ -1,16 +1,17 @@
|
|||
library(test) {
|
||||
/* D-type flip-flop with asynchronous reset and preset */
|
||||
cell (dffn) {
|
||||
/* D-type latch with reset and preset */
|
||||
cell (dlatchn) {
|
||||
area : 6;
|
||||
ff("IQ", "IQN") {
|
||||
next_state : "D";
|
||||
clocked_on : "!CLK";
|
||||
latch("IQ", "IQN") {
|
||||
data_in : "D";
|
||||
enable : "!ENA";
|
||||
}
|
||||
pin(D) {
|
||||
direction : input;
|
||||
}
|
||||
pin(CLK) {
|
||||
pin(ENA) {
|
||||
direction : input;
|
||||
clock : true;
|
||||
}
|
||||
pin(Q) {
|
||||
direction: output;
|
||||
|
|
@ -21,21 +22,22 @@ library(test) {
|
|||
function : "IQN";
|
||||
}
|
||||
}
|
||||
cell (dffsr) {
|
||||
cell (dlatchsr) {
|
||||
area : 6;
|
||||
ff("IQ", "IQN") {
|
||||
next_state : "D";
|
||||
clocked_on : "CLK";
|
||||
clear : "CLEAR";
|
||||
preset : "PRESET";
|
||||
latch("IQ", "IQN") {
|
||||
data_in : "D";
|
||||
enable : "ENA";
|
||||
clear : "CLEAR";
|
||||
preset : "PRESET";
|
||||
clear_preset_var1 : L;
|
||||
clear_preset_var2 : L;
|
||||
}
|
||||
pin(D) {
|
||||
direction : input;
|
||||
}
|
||||
pin(CLK) {
|
||||
pin(ENA) {
|
||||
direction : input;
|
||||
clock : true;
|
||||
}
|
||||
pin(CLEAR) {
|
||||
direction : input;
|
||||
|
|
@ -52,28 +54,4 @@ library(test) {
|
|||
function : "IQN";
|
||||
}
|
||||
}
|
||||
cell (dffe) {
|
||||
area : 6;
|
||||
ff("IQ", "IQN") {
|
||||
next_state : "(D EN) | (IQ !EN)";
|
||||
clocked_on : "!CLK";
|
||||
}
|
||||
pin(D) {
|
||||
direction : input;
|
||||
}
|
||||
pin(EN) {
|
||||
direction : input;
|
||||
}
|
||||
pin(CLK) {
|
||||
direction : input;
|
||||
}
|
||||
pin(Q) {
|
||||
direction: output;
|
||||
function : "IQ";
|
||||
}
|
||||
pin(QN) {
|
||||
direction: output;
|
||||
function : "IQN";
|
||||
}
|
||||
}
|
||||
}
|
||||
|
|
|
|||
|
|
@ -1,15 +1,14 @@
|
|||
read_verilog -icells <<EOT
|
||||
|
||||
module top(input C, D, E, S, R, output [11:0] Q);
|
||||
module top(input E, D, S, R, output [9:0] Q);
|
||||
|
||||
$_DFF_P_ ff0 (.C(C), .D(D), .Q(Q[0]));
|
||||
$_DFF_PP0_ ff1 (.C(C), .D(D), .R(R), .Q(Q[1]));
|
||||
$_DFF_PP1_ ff2 (.C(C), .D(D), .R(R), .Q(Q[2]));
|
||||
$_DFFSR_PPP_ ff3 (.C(C), .D(D), .R(R), .S(S), .Q(Q[3]));
|
||||
$_DFFSR_NNN_ ff4 (.C(C), .D(D), .R(R), .S(S), .Q(Q[4]));
|
||||
$_DFFE_PP_ ff5 (.C(C), .D(D), .E(E), .Q(Q[5]));
|
||||
$_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]));
|
||||
$_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[11:6] = ~Q[5:0];
|
||||
assign Q[9:5] = ~Q[4:0];
|
||||
|
||||
endmodule
|
||||
|
||||
|
|
@ -18,82 +17,76 @@ EOT
|
|||
simplemap
|
||||
|
||||
design -save orig
|
||||
read_liberty -lib dfflibmap.lib
|
||||
read_liberty -lib dlatchlibmap.lib
|
||||
|
||||
equiv_opt -map dfflibmap-sim.v -assert -multiclock dfflibmap -liberty dfflibmap.lib
|
||||
equiv_opt -map dfflibmap-sim.v -assert -multiclock dfflibmap -prepare -liberty dfflibmap.lib
|
||||
equiv_opt -map dlatchlibmap-sim.v -assert -multiclock dfflibmap -liberty dlatchlibmap.lib
|
||||
equiv_opt -map dlatchlibmap-sim.v -assert -multiclock dfflibmap -prepare -liberty dlatchlibmap.lib
|
||||
|
||||
dfflibmap -prepare -liberty dfflibmap.lib
|
||||
equiv_opt -map dfflibmap-sim.v -assert -multiclock dfflibmap -map-only -liberty dfflibmap.lib
|
||||
dfflibmap -prepare -liberty dlatchlibmap.lib
|
||||
equiv_opt -map dlatchlibmap-sim.v -assert -multiclock dfflibmap -map-only -liberty dlatchlibmap.lib
|
||||
|
||||
design -load orig
|
||||
dfflibmap -liberty dfflibmap.lib
|
||||
dfflibmap -liberty dlatchlibmap.lib
|
||||
clean
|
||||
|
||||
select -assert-count 5 t:$_NOT_
|
||||
select -assert-count 1 t:dffn
|
||||
select -assert-count 4 t:dffsr
|
||||
select -assert-count 1 t:dffe
|
||||
select -assert-none t:dffn t:dffsr t:dffe t:$_NOT_ %% %n t:* %i
|
||||
select -assert-count 1 t:dlatchn
|
||||
select -assert-count 4 t:dlatchsr
|
||||
select -assert-none t:dlatchn t:dlatchsr t:$_NOT_ %% %n t:* %i
|
||||
|
||||
design -load orig
|
||||
dfflibmap -prepare -liberty dfflibmap.lib
|
||||
dfflibmap -prepare -liberty dlatchlibmap.lib
|
||||
|
||||
select -assert-count 11 t:$_NOT_
|
||||
select -assert-count 1 t:$_DFF_N_
|
||||
select -assert-count 4 t:$_DFFSR_PPP_
|
||||
select -assert-count 1 t:$_DFFE_NP_
|
||||
select -assert-none t:$_DFF_N_ t:$_DFFSR_PPP_ t:$_DFFE_NP_ t:$_NOT_ %% %n t:* %i
|
||||
select -assert-count 1 t:$_DLATCH_N_
|
||||
select -assert-count 4 t:$_DLATCHSR_PPP_
|
||||
select -assert-none t:$_DLATCH_N_ t:$_DLATCHSR_PPP_ t:$_NOT_ %% %n t:* %i
|
||||
|
||||
design -load orig
|
||||
dfflibmap -map-only -liberty dfflibmap.lib
|
||||
dfflibmap -map-only -liberty dlatchlibmap.lib
|
||||
|
||||
select -assert-count 6 t:$_NOT_
|
||||
select -assert-count 0 t:dffn
|
||||
select -assert-count 1 t:dffsr
|
||||
select -assert-count 0 t:dlatchn
|
||||
select -assert-count 1 t:dlatchsr
|
||||
|
||||
design -load orig
|
||||
dfflibmap -prepare -liberty dfflibmap.lib
|
||||
dfflibmap -map-only -liberty dfflibmap.lib
|
||||
dfflibmap -prepare -liberty dlatchlibmap.lib
|
||||
dfflibmap -map-only -liberty dlatchlibmap.lib
|
||||
clean
|
||||
|
||||
select -assert-count 5 t:$_NOT_
|
||||
select -assert-count 1 t:dffn
|
||||
select -assert-count 4 t:dffsr
|
||||
select -assert-count 1 t:dffe
|
||||
select -assert-none t:dffn t:dffsr t:dffe t:$_NOT_ %% %n t:* %i
|
||||
select -assert-count 1 t:dlatchn
|
||||
select -assert-count 4 t:dlatchsr
|
||||
select -assert-none t:dlatchn t:dlatchsr t:$_NOT_ %% %n t:* %i
|
||||
|
||||
design -load orig
|
||||
dfflibmap -prepare -liberty dfflibmap_dffn_dffe.lib -liberty dfflibmap_dffsr_r.lib
|
||||
dfflibmap -map-only -liberty dfflibmap_dffn_dffe.lib -liberty dfflibmap_dffsr_r.lib
|
||||
dfflibmap -prepare -liberty dlatchlibmap_dlatchn.lib -liberty dlatchlibmap_dlatchsr_r.lib
|
||||
dfflibmap -map-only -liberty dlatchlibmap_dlatchn.lib -liberty dlatchlibmap_dlatchsr_r.lib
|
||||
clean
|
||||
|
||||
select -assert-count 5 t:$_NOT_
|
||||
select -assert-count 1 t:dffn
|
||||
select -assert-count 1 t:dffe
|
||||
select -assert-count 4 t:dffsr
|
||||
select -assert-none t:dffn t:dffsr t:dffe t:$_NOT_ %% %n t:* %i
|
||||
select -assert-count 1 t:dlatchn
|
||||
select -assert-count 4 t:dlatchsr
|
||||
select -assert-none t:dlatchn t:dlatchsr t:$_NOT_ %% %n t:* %i
|
||||
|
||||
design -load orig
|
||||
dfflibmap -liberty dfflibmap.lib -dont_use *ffn
|
||||
dfflibmap -liberty dlatchlibmap.lib -dont_use *latchn
|
||||
clean
|
||||
|
||||
select -assert-count 0 t:dffn
|
||||
select -assert-count 5 t:dffsr
|
||||
select -assert-count 1 t:dffe
|
||||
select -assert-count 0 t:dlatchn
|
||||
select -assert-count 5 t:dlatchsr
|
||||
|
||||
design -load orig
|
||||
dfflibmap -liberty dfflibmap.lib -liberty dfflibmap_dffsr_mixedpol.lib -dont_use dffsr
|
||||
dfflibmap -liberty dlatchlibmap.lib -liberty dlatchlibmap_dlatchsr_mixedpol.lib -dont_use dlatchsr
|
||||
clean
|
||||
# We have one more _NOT_ than with the regular dffsr
|
||||
# We have one more _NOT_ than with the regular dlatchsr
|
||||
select -assert-count 6 t:$_NOT_
|
||||
select -assert-count 1 t:dffn
|
||||
select -assert-count 4 t:dffsr_mixedpol
|
||||
select -assert-count 1 t:dffe
|
||||
# The additional NOT is on ff2.
|
||||
# Originally, ff2.R is an active high "set".
|
||||
# dffsr_mixedpol has functionally swapped labels due to the next_state inversion,
|
||||
select -assert-count 1 t:dlatchn
|
||||
select -assert-count 4 t:dlatchsr_mixedpol
|
||||
# The additional NOT is on latch2.
|
||||
# Originally, latch2.R is an active high "set".
|
||||
# dlatchsr_mixedpol has functionally swapped labels due to the next_state inversion,
|
||||
# so we use its CLEAR port for the "set",
|
||||
# but we have to invert it because the CLEAR pin is active low.
|
||||
# ff2.CLEAR = !R
|
||||
select -assert-count 1 c:ff2 %x:+[CLEAR] %ci t:$_NOT_ %i
|
||||
# latch2.CLEAR = !R
|
||||
select -assert-count 1 c:latch2 %x:+[CLEAR] %ci t:$_NOT_ %i
|
||||
|
|
|
|||
|
|
@ -1,11 +1,11 @@
|
|||
library (test_not_next) {
|
||||
cell (dff_not_next) {
|
||||
library (test_not_data) {
|
||||
cell (dff_not_data) {
|
||||
area: 1.0;
|
||||
pin (QN) {
|
||||
direction : output;
|
||||
function : "STATE";
|
||||
}
|
||||
pin (CLK) {
|
||||
pin (ENA) {
|
||||
direction : input;
|
||||
clock : true;
|
||||
}
|
||||
|
|
@ -15,9 +15,9 @@ library (test_not_next) {
|
|||
pin (RN) {
|
||||
direction : input;
|
||||
}
|
||||
ff (STATE, STATEN) {
|
||||
clocked_on: "CLK";
|
||||
next_state: "!D";
|
||||
latch (STATE, STATEN) {
|
||||
enable: "ENA";
|
||||
data_in: "!D";
|
||||
preset : "!RN";
|
||||
}
|
||||
}
|
||||
|
|
|
|||
|
|
@ -1,15 +1,16 @@
|
|||
library(test) {
|
||||
cell (dffn) {
|
||||
cell (dlatchn) {
|
||||
area : 6;
|
||||
ff("IQ", "IQN") {
|
||||
next_state : "D";
|
||||
clocked_on : "!CLK";
|
||||
latch("IQ", "IQN") {
|
||||
data_in : "D";
|
||||
enable : "!ENA";
|
||||
}
|
||||
pin(D) {
|
||||
direction : input;
|
||||
}
|
||||
pin(CLK) {
|
||||
pin(ENA) {
|
||||
direction : input;
|
||||
clock : true;
|
||||
}
|
||||
pin(Q) {
|
||||
direction: output;
|
||||
|
|
@ -20,28 +21,4 @@ library(test) {
|
|||
function : "IQN";
|
||||
}
|
||||
}
|
||||
cell (dffe) {
|
||||
area : 6;
|
||||
ff("IQ", "IQN") {
|
||||
next_state : "(D&EN) | (IQ&!EN)";
|
||||
clocked_on : "!CLK";
|
||||
}
|
||||
pin(D) {
|
||||
direction : input;
|
||||
}
|
||||
pin(EN) {
|
||||
direction : input;
|
||||
}
|
||||
pin(CLK) {
|
||||
direction : input;
|
||||
}
|
||||
pin(Q) {
|
||||
direction: output;
|
||||
function : "IQ";
|
||||
}
|
||||
pin(QN) {
|
||||
direction: output;
|
||||
function : "IQN";
|
||||
}
|
||||
}
|
||||
}
|
||||
|
|
|
|||
|
|
@ -1,21 +1,20 @@
|
|||
library(test) {
|
||||
cell (dffsr_mixedpol) {
|
||||
cell (dlatchsr_mixedpol) {
|
||||
area : 6;
|
||||
ff("IQ", "IQN") {
|
||||
// look here
|
||||
next_state : "!D";
|
||||
clocked_on : "CLK";
|
||||
// look here
|
||||
clear : "!CLEAR";
|
||||
preset : "PRESET";
|
||||
latch("IQ", "IQN") {
|
||||
data_in : "!D";
|
||||
enable : "ENA";
|
||||
clear : "!CLEAR";
|
||||
preset : "PRESET";
|
||||
clear_preset_var1 : L;
|
||||
clear_preset_var2 : L;
|
||||
}
|
||||
pin(D) {
|
||||
direction : input;
|
||||
}
|
||||
pin(CLK) {
|
||||
pin(ENA) {
|
||||
direction : input;
|
||||
clock : true;
|
||||
}
|
||||
pin(CLEAR) {
|
||||
direction : input;
|
||||
|
|
|
|||
|
|
@ -1,11 +1,11 @@
|
|||
library (test_not_next) {
|
||||
cell (dffsr_not_next) {
|
||||
library (test_not_data) {
|
||||
cell (dlatchsr_not_data) {
|
||||
area : 1.0;
|
||||
pin (Q) {
|
||||
direction : output;
|
||||
function : "STATE";
|
||||
}
|
||||
pin (CLK) {
|
||||
pin (ENA) {
|
||||
clock : true;
|
||||
direction : input;
|
||||
}
|
||||
|
|
@ -18,10 +18,10 @@ library (test_not_next) {
|
|||
pin (SN) {
|
||||
direction : input;
|
||||
}
|
||||
ff (STATE,STATEN) {
|
||||
latch (STATE,STATEN) {
|
||||
clear : "!SN";
|
||||
clocked_on : "CLK";
|
||||
next_state : "!D";
|
||||
enable : "ENA";
|
||||
data_in : "!D";
|
||||
preset : "!RN";
|
||||
}
|
||||
}
|
||||
|
|
|
|||
|
|
@ -1,19 +1,20 @@
|
|||
library(test) {
|
||||
cell (dffr_not_next) {
|
||||
cell (dlatchr_not_data) {
|
||||
area : 6;
|
||||
ff("IQ", "IQN") {
|
||||
next_state : "!D";
|
||||
clocked_on : "CLK";
|
||||
clear : "CLEAR";
|
||||
preset : "PRESET";
|
||||
latch("IQ", "IQN") {
|
||||
data_in : "!D";
|
||||
enable : "ENA";
|
||||
clear : "CLEAR";
|
||||
preset : "PRESET";
|
||||
clear_preset_var1 : L;
|
||||
clear_preset_var2 : L;
|
||||
}
|
||||
pin(D) {
|
||||
direction : input;
|
||||
}
|
||||
pin(CLK) {
|
||||
pin(ENA) {
|
||||
direction : input;
|
||||
clock : true;
|
||||
}
|
||||
pin(CLEAR) {
|
||||
direction : input;
|
||||
|
|
|
|||
|
|
@ -1,19 +1,20 @@
|
|||
library(test) {
|
||||
cell (dffsr) {
|
||||
cell (dlatchsr) {
|
||||
area : 6;
|
||||
ff("IQ", "IQN") {
|
||||
next_state : "D";
|
||||
clocked_on : "CLK";
|
||||
clear : "CLEAR";
|
||||
preset : "PRESET";
|
||||
latch("IQ", "IQN") {
|
||||
data_in : "D";
|
||||
enable : "ENA";
|
||||
clear : "CLEAR";
|
||||
preset : "PRESET";
|
||||
clear_preset_var1 : L;
|
||||
clear_preset_var2 : H;
|
||||
}
|
||||
pin(D) {
|
||||
direction : input;
|
||||
}
|
||||
pin(CLK) {
|
||||
pin(ENA) {
|
||||
direction : input;
|
||||
clock : true;
|
||||
}
|
||||
pin(CLEAR) {
|
||||
direction : input;
|
||||
|
|
|
|||
|
|
@ -1,19 +1,20 @@
|
|||
library(test) {
|
||||
cell (dffsr) {
|
||||
cell (dlatchsr) {
|
||||
area : 6;
|
||||
ff("IQ", "IQN") {
|
||||
next_state : "D";
|
||||
clocked_on : "CLK";
|
||||
clear : "CLEAR";
|
||||
preset : "PRESET";
|
||||
latch("IQ", "IQN") {
|
||||
data_in : "D";
|
||||
enable : "ENA";
|
||||
clear : "CLEAR";
|
||||
preset : "PRESET";
|
||||
clear_preset_var1 : H;
|
||||
clear_preset_var2 : L;
|
||||
}
|
||||
pin(D) {
|
||||
direction : input;
|
||||
}
|
||||
pin(CLK) {
|
||||
pin(ENA) {
|
||||
direction : input;
|
||||
clock : true;
|
||||
}
|
||||
pin(CLEAR) {
|
||||
direction : input;
|
||||
|
|
|
|||
|
|
@ -1,19 +1,20 @@
|
|||
library(test) {
|
||||
cell (dffsr) {
|
||||
cell (dlatchsr) {
|
||||
area : 6;
|
||||
ff("IQ", "IQN") {
|
||||
next_state : "D";
|
||||
clocked_on : "CLK";
|
||||
clear : "CLEAR";
|
||||
preset : "PRESET";
|
||||
latch("IQ", "IQN") {
|
||||
data_in : "D";
|
||||
enable : "ENA";
|
||||
clear : "CLEAR";
|
||||
preset : "PRESET";
|
||||
clear_preset_var1 : X;
|
||||
clear_preset_var2 : X;
|
||||
}
|
||||
pin(D) {
|
||||
direction : input;
|
||||
}
|
||||
pin(CLK) {
|
||||
pin(ENA) {
|
||||
direction : input;
|
||||
clock : true;
|
||||
}
|
||||
pin(CLEAR) {
|
||||
direction : input;
|
||||
|
|
|
|||
|
|
@ -2,19 +2,17 @@
|
|||
|
||||
read_verilog -sv -icells <<EOT
|
||||
|
||||
module top(input C, D, E, S, R, output [11:0] Q);
|
||||
module top(input E, D, S, R, output [9:0] Q);
|
||||
|
||||
$_DFF_P_ ff0 (.C(C), .D(D), .Q(Q[0]));
|
||||
$_DFF_PP0_ ff1 (.C(C), .D(D), .R(R), .Q(Q[1]));
|
||||
$_DFF_PP1_ ff2 (.C(C), .D(D), .R(R), .Q(Q[2]));
|
||||
$_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);
|
||||
$_DFFSR_PPP_ ff3 (.C(C), .D(D), .R(R), .S(S), .Q(Q[3]));
|
||||
$_DFFSR_NNN_ ff4 (.C(C), .D(D), .R(~R), .S(~S), .Q(Q[4]));
|
||||
$_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]));
|
||||
|
||||
$_DFFE_PP_ ff5 (.C(C), .D(D), .E(E), .Q(Q[5]));
|
||||
|
||||
assign Q[11:6] = ~Q[5:0];
|
||||
assign Q[9:5] = ~Q[4:0];
|
||||
|
||||
endmodule
|
||||
|
||||
|
|
@ -22,10 +20,10 @@ EOT
|
|||
|
||||
proc
|
||||
opt
|
||||
read_liberty dfflibmap_dffsr_s.lib
|
||||
read_liberty dlatchlibmap_dlatchsr_s.lib
|
||||
|
||||
copy top top_unmapped
|
||||
dfflibmap -liberty dfflibmap_dffsr_s.lib top
|
||||
dfflibmap -liberty dlatchlibmap_dlatchsr_s.lib top
|
||||
|
||||
clk2fflogic
|
||||
flatten
|
||||
|
|
@ -42,19 +40,17 @@ sat -falsify -prove-asserts -enable_undef -set-init-undef -seq 3 miter
|
|||
design -reset
|
||||
read_verilog -sv -icells <<EOT
|
||||
|
||||
module top(input C, D, E, S, R, output [11:0] Q);
|
||||
module top(input E, D, S, R, output [9:0] Q);
|
||||
|
||||
$_DFF_P_ ff0 (.C(C), .D(D), .Q(Q[0]));
|
||||
$_DFF_PP0_ ff1 (.C(C), .D(D), .R(R), .Q(Q[1]));
|
||||
$_DFF_PP1_ ff2 (.C(C), .D(D), .R(R), .Q(Q[2]));
|
||||
$_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);
|
||||
$_DFFSR_PPP_ ff3 (.C(C), .D(D), .R(R), .S(S), .Q(Q[3]));
|
||||
$_DFFSR_NNN_ ff4 (.C(C), .D(D), .R(~R), .S(~S), .Q(Q[4]));
|
||||
$_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]));
|
||||
|
||||
$_DFFE_PP_ ff5 (.C(C), .D(D), .E(E), .Q(Q[5]));
|
||||
|
||||
assign Q[11:6] = ~Q[5:0];
|
||||
assign Q[9:5] = ~Q[4:0];
|
||||
|
||||
endmodule
|
||||
|
||||
|
|
@ -62,10 +58,10 @@ EOT
|
|||
|
||||
proc
|
||||
opt
|
||||
read_liberty dfflibmap_dffsr_r.lib
|
||||
read_liberty dlatchlibmap_dlatchsr_r.lib
|
||||
|
||||
copy top top_unmapped
|
||||
dfflibmap -liberty dfflibmap_dffsr_r.lib top
|
||||
dfflibmap -liberty dlatchlibmap_dlatchsr_r.lib top
|
||||
|
||||
clk2fflogic
|
||||
flatten
|
||||
|
|
@ -82,19 +78,17 @@ sat -falsify -prove-asserts -enable_undef -set-init-undef -seq 3 miter
|
|||
design -reset
|
||||
read_verilog -sv -icells <<EOT
|
||||
|
||||
module top(input C, D, E, S, R, output [11:0] Q);
|
||||
module top(input E, D, S, R, output [9:0] Q);
|
||||
|
||||
$_DFF_P_ ff0 (.C(C), .D(D), .Q(Q[0]));
|
||||
$_DFF_PP0_ ff1 (.C(C), .D(D), .R(R), .Q(Q[1]));
|
||||
$_DFF_PP1_ ff2 (.C(C), .D(D), .R(R), .Q(Q[2]));
|
||||
$_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
|
||||
$_DFFSR_PPP_ ff3 (.C(C), .D(D), .R(R), .S(S), .Q(Q[3]));
|
||||
$_DFFSR_NNN_ ff4 (.C(C), .D(D), .R(~R), .S(~S), .Q(Q[4]));
|
||||
$_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]));
|
||||
|
||||
$_DFFE_PP_ ff5 (.C(C), .D(D), .E(E), .Q(Q[5]));
|
||||
|
||||
assign Q[11:6] = ~Q[5:0];
|
||||
assign Q[9:5] = ~Q[4:0];
|
||||
|
||||
endmodule
|
||||
|
||||
|
|
@ -102,11 +96,11 @@ EOT
|
|||
|
||||
proc
|
||||
opt
|
||||
read_liberty dfflibmap_dffsr_x.lib
|
||||
read_liberty dlatchlibmap_dlatchsr_x.lib
|
||||
opt
|
||||
|
||||
copy top top_unmapped
|
||||
dfflibmap -liberty dfflibmap_dffsr_x.lib top
|
||||
dfflibmap -liberty dlatchlibmap_dlatchsr_x.lib top
|
||||
|
||||
clk2fflogic
|
||||
flatten
|
||||
|
|
@ -122,22 +116,21 @@ sat -verify -prove-asserts -set-init-undef -show-public -seq 3 miter
|
|||
design -reset
|
||||
read_verilog -sv -icells <<EOT
|
||||
|
||||
module top(input C, D, E, S, R, output [11:0] Q);
|
||||
module top(input E, D, S, R, output [9:0] Q);
|
||||
|
||||
$_DFF_P_ ff0 (.C(C), .D(D), .Q(Q[0]));
|
||||
$_DFF_PP0_ ff1 (.C(C), .D(D), .R(R), .Q(Q[1]));
|
||||
$_DFF_PP1_ ff2 (.C(C), .D(D), .R(R), .Q(Q[2]));
|
||||
$_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]));
|
||||
|
||||
// Formal checking of directly instantiated DFFSR doesn't work at the moment
|
||||
// TODO: this comment is just a copy from 'dfflibmap_formal.ys'
|
||||
// Formal checking of directly instantiated DLATCHSR doesn't work at the moment
|
||||
// likely due to an equiv_induct -set-assumes assume bug #5196
|
||||
|
||||
// no assume when mapping to unset clear_preset_var
|
||||
$_DFFSR_PPP_ ff3 (.C(C), .D(D), .R(R), .S(S), .Q(Q[3]));
|
||||
$_DFFSR_NNN_ ff4 (.C(C), .D(D), .R(~R), .S(~S), .Q(Q[4]));
|
||||
$_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]));
|
||||
|
||||
$_DFFE_PP_ ff5 (.C(C), .D(D), .E(E), .Q(Q[5]));
|
||||
|
||||
assign Q[11:6] = ~Q[5:0];
|
||||
assign Q[9:5] = ~Q[4:0];
|
||||
|
||||
endmodule
|
||||
|
||||
|
|
@ -145,11 +138,11 @@ EOT
|
|||
|
||||
proc
|
||||
opt
|
||||
read_liberty dfflibmap_dffn_dffe.lib
|
||||
read_liberty dfflibmap_dffsr_not_next.lib
|
||||
read_liberty dlatchlibmap_dlatchn.lib
|
||||
read_liberty dlatchlibmap_dlatchsr_not_data.lib
|
||||
|
||||
copy top top_unmapped
|
||||
dfflibmap -liberty dfflibmap_dffn_dffe.lib -liberty dfflibmap_dffsr_not_next.lib top
|
||||
dfflibmap -liberty dlatchlibmap_dlatchn.lib -liberty dlatchlibmap_dlatchsr_not_data.lib top
|
||||
|
||||
clk2fflogic
|
||||
flatten
|
||||
|
|
@ -165,19 +158,17 @@ sat -verify -prove-asserts -set-init-undef -show-public -seq 3 miter
|
|||
design -reset
|
||||
read_verilog -sv -icells <<EOT
|
||||
|
||||
module top(input C, D, E, S, R, output [11:0] Q);
|
||||
module top(input E, D, S, R, output [9:0] Q);
|
||||
|
||||
$_DFF_P_ ff0 (.C(C), .D(D), .Q(Q[0]));
|
||||
$_DFF_PP0_ ff1 (.C(C), .D(D), .R(R), .Q(Q[1]));
|
||||
$_DFF_PP1_ ff2 (.C(C), .D(D), .R(R), .Q(Q[2]));
|
||||
$_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);
|
||||
$_DFFSR_PPP_ ff3 (.C(C), .D(D), .R(R), .S(S), .Q(Q[3]));
|
||||
$_DFFSR_NNN_ ff4 (.C(C), .D(D), .R(~R), .S(~S), .Q(Q[4]));
|
||||
$_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]));
|
||||
|
||||
$_DFFE_PP_ ff5 (.C(C), .D(D), .E(E), .Q(Q[5]));
|
||||
|
||||
assign Q[11:6] = ~Q[5:0];
|
||||
assign Q[9:5] = ~Q[4:0];
|
||||
|
||||
endmodule
|
||||
|
||||
|
|
@ -185,10 +176,10 @@ EOT
|
|||
|
||||
proc
|
||||
opt
|
||||
read_liberty dfflibmap_dffsr_not_next_l.lib
|
||||
read_liberty dlatchlibmap_dlatchsr_not_data_l.lib
|
||||
|
||||
copy top top_unmapped
|
||||
dfflibmap -liberty dfflibmap_dffsr_not_next_l.lib top
|
||||
dfflibmap -liberty dlatchlibmap_dlatchsr_not_data_l.lib top
|
||||
|
||||
clk2fflogic
|
||||
flatten
|
||||
|
|
@ -206,28 +197,24 @@ sat -falsify -prove-asserts -enable_undef -set-init-undef -seq 3 miter
|
|||
design -reset
|
||||
read_verilog <<EOT
|
||||
|
||||
module top(input C, D, E, S, R, output Q);
|
||||
// DFFSR with priority R over S
|
||||
always @(posedge C, posedge R, posedge S)
|
||||
if (R == 1)
|
||||
Q <= 0;
|
||||
else if (S == 1)
|
||||
Q <= 1;
|
||||
else
|
||||
Q <= D;
|
||||
|
||||
module top(input E, D, S, R, output Q);
|
||||
// DLATCHSR with priority R over S
|
||||
always_latch
|
||||
if (R) Q <= 1'b0;
|
||||
else if (S) Q <= 1'b1;
|
||||
else if (E) Q <= D;
|
||||
endmodule
|
||||
|
||||
EOT
|
||||
|
||||
proc
|
||||
opt
|
||||
read_liberty dfflibmap_dffn_dffe.lib
|
||||
read_liberty dfflibmap_dffsr_not_next.lib
|
||||
read_liberty dlatchlibmap_dlatchn.lib
|
||||
read_liberty dlatchlibmap_dlatchsr_not_data.lib
|
||||
|
||||
copy top top_unmapped
|
||||
simplemap top
|
||||
dfflibmap -liberty dfflibmap_dffn_dffe.lib -liberty dfflibmap_dffsr_not_next.lib top
|
||||
dfflibmap -liberty dlatchlibmap_dlatchn.lib -liberty dlatchlibmap_dlatchsr_not_data.lib top
|
||||
|
||||
clk2fflogic
|
||||
flatten
|
||||
|
|
@ -241,28 +228,27 @@ equiv_status -assert equiv
|
|||
design -reset
|
||||
read_verilog <<EOT
|
||||
|
||||
module top(input C, D, R, output Q);
|
||||
// DFF with preset
|
||||
always @(posedge C or negedge R) begin
|
||||
if (!R) Q <= 1'b1;
|
||||
else Q <= D;
|
||||
end
|
||||
module top(input E, D, R, output Q);
|
||||
// DLATCH with preset
|
||||
always_latch
|
||||
if (~R) Q <= 1'b1;
|
||||
else if (E) Q <= D;
|
||||
endmodule
|
||||
|
||||
EOT
|
||||
|
||||
proc
|
||||
opt
|
||||
read_liberty dfflibmap_dffn_dffe.lib
|
||||
read_liberty dfflibmap_dff_not_next.lib
|
||||
read_liberty dlatchlibmap_dlatchn.lib
|
||||
read_liberty dlatchlibmap_dlatch_not_data.lib
|
||||
|
||||
copy top top_unmapped
|
||||
simplemap top
|
||||
dfflibmap -liberty dfflibmap_dffn_dffe.lib -liberty dfflibmap_dff_not_next.lib 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
|
||||
equiv_status -assert equiv
|
||||
|
|
|
|||
|
|
@ -2,41 +2,19 @@
|
|||
|
||||
read_verilog -sv -icells <<EOT
|
||||
|
||||
module top(input C, D, E, S, R, output [7:0] Q);
|
||||
module top(input E, D, S, R, output [3:0] Q);
|
||||
|
||||
always @( posedge C, posedge S, posedge R)
|
||||
if (R)
|
||||
Q[0] <= 0;
|
||||
else if (S)
|
||||
Q[0] <= 1;
|
||||
else
|
||||
Q[0] <= D;
|
||||
always_latch
|
||||
if (R) Q[0] <= 1'b0;
|
||||
else if (S) Q[0] <= 1'b1;
|
||||
else if (E) Q[0] <= D;
|
||||
|
||||
always @( posedge C, posedge S, posedge R)
|
||||
if (S)
|
||||
Q[1] <= 1;
|
||||
else if (R)
|
||||
Q[1] <= 0;
|
||||
else
|
||||
Q[1] <= D;
|
||||
always_latch
|
||||
if (S) Q[1] <= 1'b1;
|
||||
else if (R) Q[1] <= 1'b0;
|
||||
else if (E) Q[1] <= D;
|
||||
|
||||
always @( posedge C, posedge S, posedge R)
|
||||
if (R)
|
||||
Q[2] <= 0;
|
||||
else if (S)
|
||||
Q[2] <= 1;
|
||||
else if (E)
|
||||
Q[2] <= D;
|
||||
|
||||
always @( posedge C, posedge S, posedge R)
|
||||
if (S)
|
||||
Q[3] <= 1;
|
||||
else if (R)
|
||||
Q[3] <= 0;
|
||||
else if (E)
|
||||
Q[3] <= D;
|
||||
|
||||
assign Q[7:4] = ~Q[3:0];
|
||||
assign Q[3:2] = ~Q[1:0];
|
||||
|
||||
endmodule
|
||||
|
||||
|
|
@ -44,10 +22,10 @@ EOT
|
|||
|
||||
proc
|
||||
opt
|
||||
read_liberty dfflibmap_dffsr_s.lib
|
||||
read_liberty dlatchlibmap_dlatchsr_s.lib
|
||||
|
||||
copy top top_unmapped
|
||||
dfflibmap -liberty dfflibmap_dffsr_s.lib top
|
||||
dfflibmap -liberty dlatchlibmap_dlatchsr_s.lib top
|
||||
|
||||
clk2fflogic
|
||||
flatten
|
||||
|
|
@ -62,7 +40,7 @@ sat -verify -prove-asserts -set-init-undef -show-public -seq 3 miter
|
|||
delete top miter
|
||||
|
||||
copy top_unmapped top
|
||||
dfflibmap -liberty dfflibmap_dffsr_r.lib top
|
||||
dfflibmap -liberty dlatchlibmap_dlatchsr_r.lib top
|
||||
|
||||
clk2fflogic
|
||||
flatten
|
||||
|
|
@ -76,7 +54,7 @@ sat -verify -prove-asserts -set-init-undef -show-public -seq 3 miter
|
|||
delete top miter
|
||||
|
||||
copy top_unmapped top
|
||||
dfflibmap -liberty dfflibmap_dffsr_mixedpol.lib top
|
||||
dfflibmap -liberty dlatchlibmap_dlatchsr_mixedpol.lib top
|
||||
|
||||
clk2fflogic
|
||||
flatten
|
||||
|
|
@ -90,7 +68,7 @@ sat -verify -prove-asserts -set-init-undef -show-public -seq 3 miter
|
|||
delete top miter
|
||||
|
||||
copy top_unmapped top
|
||||
dfflibmap -liberty dfflibmap_dffsr_not_next.lib top
|
||||
dfflibmap -liberty dlatchlibmap_dlatchsr_not_data.lib top
|
||||
|
||||
clk2fflogic
|
||||
flatten
|
||||
|
|
|
|||
Loading…
Reference in New Issue