diff options
| -rw-r--r-- | CHANGELOG | 8 | ||||
| -rw-r--r-- | Makefile | 4 | ||||
| -rw-r--r-- | frontends/verific/verific.cc | 8 | ||||
| -rw-r--r-- | frontends/verific/verific.h | 1 | ||||
| -rw-r--r-- | frontends/verific/verificsva.cc | 12 | ||||
| -rw-r--r-- | manual/command-reference-manual.tex | 44 | ||||
| -rw-r--r-- | tests/sva/nested_clk_else.sv | 11 |
7 files changed, 80 insertions, 8 deletions
@@ -2,9 +2,15 @@ List of major changes and improvements between releases ======================================================= -Yosys 0.16 .. Yosys 0.16-dev +Yosys 0.17 .. Yosys 0.17-dev -------------------------- +Yosys 0.16 .. Yosys 0.17 +-------------------------- + * New commands and options + - Added "write_jny" ( JSON netlist metadata format ) + - Added "tribuf -formal" + * SystemVerilog - Fixed automatic `nosync` inference for local variables in `always_comb` procedures not applying to nested blocks and blocks in functions @@ -129,12 +129,12 @@ LDFLAGS += -rdynamic LDLIBS += -lrt endif -YOSYS_VER := 0.16+73 +YOSYS_VER := 0.17+0 GIT_REV := $(shell git -C $(YOSYS_SRC) rev-parse --short HEAD 2> /dev/null || echo UNKNOWN) OBJS = kernel/version_$(GIT_REV).o bumpversion: - sed -i "/^YOSYS_VER := / s/+[0-9][0-9]*$$/+`git log --oneline b63e0a0.. | wc -l`/;" Makefile + sed -i "/^YOSYS_VER := / s/+[0-9][0-9]*$$/+`git log --oneline 6f9602b.. | wc -l`/;" Makefile # set 'ABCREV = default' to use abc/ as it is # diff --git a/frontends/verific/verific.cc b/frontends/verific/verific.cc index 145a5acf2..fd8bbc3f1 100644 --- a/frontends/verific/verific.cc +++ b/frontends/verific/verific.cc @@ -1888,15 +1888,19 @@ VerificClocking::VerificClocking(VerificImporter *importer, Net *net, bool sva_a if (inst_mux == nullptr || inst_mux->Type() != PRIM_MUX) break; - if (!inst_mux->GetInput1()->IsPwr()) + bool pwr1 = inst_mux->GetInput1()->IsPwr(); + bool pwr2 = inst_mux->GetInput2()->IsPwr(); + + if (!pwr1 && !pwr2) break; - Net *sva_net = inst_mux->GetInput2(); + Net *sva_net = pwr1 ? inst_mux->GetInput2() : inst_mux->GetInput1(); if (!verific_is_sva_net(importer, sva_net)) break; body_net = sva_net; cond_net = inst_mux->GetControl(); + cond_pol = pwr1; } while (0); clock_net = net; diff --git a/frontends/verific/verific.h b/frontends/verific/verific.h index 416b26396..695c04f3b 100644 --- a/frontends/verific/verific.h +++ b/frontends/verific/verific.h @@ -44,6 +44,7 @@ struct VerificClocking { SigBit disable_sig = State::S0; bool posedge = true; bool gclk = false; + bool cond_pol = true; VerificClocking() { } VerificClocking(VerificImporter *importer, Verific::Net *net, bool sva_at_only = false); diff --git a/frontends/verific/verificsva.cc b/frontends/verific/verificsva.cc index 1bbdcf016..12bac2a3d 100644 --- a/frontends/verific/verificsva.cc +++ b/frontends/verific/verificsva.cc @@ -1522,10 +1522,13 @@ struct VerificSvaImporter if (inst == nullptr) return false; - if (clocking.cond_net != nullptr) + if (clocking.cond_net != nullptr) { trig = importer->net_map_at(clocking.cond_net); - else + if (!clocking.cond_pol) + trig = module->Not(NEW_ID, trig); + } else { trig = State::S1; + } if (inst->Type() == PRIM_SVA_S_EVENTUALLY || inst->Type() == PRIM_SVA_EVENTUALLY) { @@ -1587,8 +1590,11 @@ struct VerificSvaImporter SigBit trig = State::S1; - if (clocking.cond_net != nullptr) + if (clocking.cond_net != nullptr) { trig = importer->net_map_at(clocking.cond_net); + if (!clocking.cond_pol) + trig = module->Not(NEW_ID, trig); + } if (inst == nullptr) { diff --git a/manual/command-reference-manual.tex b/manual/command-reference-manual.tex index e68da3318..bafce6de6 100644 --- a/manual/command-reference-manual.tex +++ b/manual/command-reference-manual.tex @@ -2592,6 +2592,28 @@ the resulting cells to more sophisticated PAD cells. Tristate PADS (-toutpad, -tinoutpad) always operate in -bits mode. \end{lstlisting} +\section{jny -- write design and metadata} +\label{cmd:jny} +\begin{lstlisting}[numbers=left,frame=single] + jny [options] [selection] + +Write a JSON netlist metadata for the current design + + -o <filename> + write to the specified file. + + -no-connections + Don't include connection information in the netlist output. + + -no-attributes + Don't include attributed information in the netlist output. + + -no-properties + Don't include property information in the netlist output. + +See 'help write_jny' for a description of the JSON format used. +\end{lstlisting} + \section{json -- write design in JSON format} \label{cmd:json} \begin{lstlisting}[numbers=left,frame=single] @@ -7647,6 +7669,11 @@ This pass transforms $mux cells with 'z' inputs to tristate buffers. -logic convert tri-state buffers that do not drive output ports to non-tristate logic. this option implies -merge. + + -formal + convert all tri-state buffers to non-tristate logic and + add a formal assertion that no two buffers are driving the + same net simultaneously. this option implies -merge. \end{lstlisting} \section{uniquify -- create unique copies of modules} @@ -8428,6 +8455,23 @@ a tool for Coarse-Grain Example-Driven Interconnect Synthesis. http://bygone.clairexen.net/intersynth/ \end{lstlisting} +\section{write\_jny -- generate design metadata} +\label{cmd:write_jny} +\begin{lstlisting}[numbers=left,frame=single] + jny [options] [selection] + + -no-connections + Don't include connection information in the netlist output. + + -no-attributes + Don't include attributed information in the netlist output. + + -no-properties + Don't include property information in the netlist output. + +Write a JSON metadata for the current design +\end{lstlisting} + \section{write\_json -- write design to a JSON file} \label{cmd:write_json} \begin{lstlisting}[numbers=left,frame=single] diff --git a/tests/sva/nested_clk_else.sv b/tests/sva/nested_clk_else.sv new file mode 100644 index 000000000..4421cb36a --- /dev/null +++ b/tests/sva/nested_clk_else.sv @@ -0,0 +1,11 @@ +module top (input clk, a, b); + always @(posedge clk) begin + if (a); + else assume property (@(posedge clk) b); + end + +`ifndef FAIL + assume property (@(posedge clk) !a); +`endif + assert property (@(posedge clk) b); +endmodule |