mirror of
https://github.com/YosysHQ/yosys
synced 2026-03-04 12:40:25 +00:00
dfflibmap: fix formal $dffsr tests with sat, prove "no s&r" assumption only needed when appropriate
This commit is contained in:
parent
b2bf69be80
commit
95978b68be
4 changed files with 121 additions and 38 deletions
|
|
@ -1,33 +0,0 @@
|
|||
library(test) {
|
||||
cell (dffr_not_next) {
|
||||
area : 6;
|
||||
ff("IQ", "IQN") {
|
||||
next_state : "!D";
|
||||
clocked_on : "CLK";
|
||||
clear : "CLEAR";
|
||||
preset : "PRESET";
|
||||
clear_preset_var1 : L;
|
||||
clear_preset_var2 : L;
|
||||
}
|
||||
pin(D) {
|
||||
direction : input;
|
||||
}
|
||||
pin(CLK) {
|
||||
direction : input;
|
||||
}
|
||||
pin(CLEAR) {
|
||||
direction : input;
|
||||
}
|
||||
pin(PRESET) {
|
||||
direction : input;
|
||||
}
|
||||
pin(Q) {
|
||||
direction: output;
|
||||
function : "IQ";
|
||||
}
|
||||
pin(QN) {
|
||||
direction: output;
|
||||
function : "IQN";
|
||||
}
|
||||
}
|
||||
}
|
||||
Loading…
Add table
Add a link
Reference in a new issue