Merge pull request #3305 from jix/sva_value_change_logic

verific: Improve logic generated for SVA value change expressions

diff --git a/CHANGELOG b/CHANGELOG
index a27adc5bff0333995c6e6da133c9f27d2bbc40e0..4004c534b8e1e75e330f17ee3d87f704a5fab854 100644 (file)
--- a/CHANGELOG
+++ b/CHANGELOG
@@ -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

diff --git a/Makefile b/Makefile
index 2df16ba589f681672d1d28a4be86579d5854e6f5..5a69278808b2ce11e495bc3050abeef5eef6f4bc 100644 (file)
--- a/Makefile
+++ b/Makefile
@@ -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 145a5acf2dd0c66fd50bc87137d454e5b18bc3d3..fd8bbc3f12bfa30638a9ac632378cb65b1e8e65a 100644 (file)
--- 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 416b26396c84952ec0f8f7ec382bb409c609d121..695c04f3bcba3ae5451008ef8d7c196f91ff73fe 100644 (file)
--- 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 1bbdcf0167f061005b674b02735e0886e8064c92..12bac2a3d058b7b586b25fe7577842051a98a09a 100644 (file)
--- 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 e68da3318f542742bdf3db49c2f61000021286dd..bafce6de6fe87f0400e88ad6d0a30d807d7b852c 100644 (file)
--- 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 (file)
index 0000000..4421cb3
--- /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