aboutsummaryrefslogtreecommitdiffstats
diff options
context:
space:
mode:
Diffstat
-rw-r--r--frontends/verific/verific.cc35
-rw-r--r--tests/sva/.gitignore1
-rw-r--r--tests/sva/Makefile1
-rw-r--r--tests/sva/runtest.sh4
-rw-r--r--tests/sva/sva_value_change_changed.sv17
-rw-r--r--tests/sva/sva_value_change_rose.sv20
-rw-r--r--tests/sva/sva_value_change_sim.sv51
-rw-r--r--tests/sva/sva_value_change_sim.ys3
8 files changed, 121 insertions, 11 deletions
diff --git a/frontends/verific/verific.cc b/frontends/verific/verific.cc
index d19d837ff..145a5acf2 100644
--- a/frontends/verific/verific.cc
+++ b/frontends/verific/verific.cc
@@ -1557,17 +1557,25 @@ void VerificImporter::import_netlist(RTLIL::Design *design, Netlist *nl, std::ma
SigSpec sig_d = net_map_at(inst->GetInput1());
SigSpec sig_o = net_map_at(inst->GetOutput());
- SigSpec sig_q = module->addWire(new_verific_id(inst));
+ SigSpec sig_dx = module->addWire(new_verific_id(inst), 2);
+ SigSpec sig_qx = module->addWire(new_verific_id(inst), 2);
if (verific_verbose) {
+ log(" NEX with A=%s, B=0, Y=%s.\n",
+ log_signal(sig_d), log_signal(sig_dx[0]));
+ log(" EQX with A=%s, B=1, Y=%s.\n",
+ log_signal(sig_d), log_signal(sig_dx[1]));
log(" %sedge FF with D=%s, Q=%s, C=%s.\n", clocking.posedge ? "pos" : "neg",
- log_signal(sig_d), log_signal(sig_q), log_signal(clocking.clock_sig));
- log(" XNOR with A=%s, B=%s, Y=%s.\n",
- log_signal(sig_d), log_signal(sig_q), log_signal(sig_o));
+ log_signal(sig_dx), log_signal(sig_qx), log_signal(clocking.clock_sig));
+ log(" EQ with A=%s, B=%s, Y=%s.\n",
+ log_signal(sig_dx), log_signal(sig_qx), log_signal(sig_o));
}
- clocking.addDff(new_verific_id(inst), sig_d, sig_q);
- module->addXnor(new_verific_id(inst), sig_d, sig_q, sig_o);
+ module->addNex(new_verific_id(inst), sig_d, State::S0, sig_dx[0]);
+ module->addEqx(new_verific_id(inst), sig_d, State::S1, sig_dx[1]);
+
+ clocking.addDff(new_verific_id(inst), sig_dx, sig_qx, Const(1, 2));
+ module->addEq(new_verific_id(inst), sig_dx, sig_qx, sig_o);
if (!mode_keep)
continue;
@@ -1601,13 +1609,20 @@ void VerificImporter::import_netlist(RTLIL::Design *design, Netlist *nl, std::ma
SigBit sig_d = net_map_at(inst->GetInput1());
SigBit sig_o = net_map_at(inst->GetOutput());
SigBit sig_q = module->addWire(new_verific_id(inst));
+ SigBit sig_d_no_x = module->addWire(new_verific_id(inst));
- if (verific_verbose)
+ if (verific_verbose) {
+ log(" EQX with A=%s, B=%d, Y=%s.\n",
+ log_signal(sig_d), inst->Type() == PRIM_SVA_ROSE, log_signal(sig_d_no_x));
log(" %sedge FF with D=%s, Q=%s, C=%s.\n", clocking.posedge ? "pos" : "neg",
- log_signal(sig_d), log_signal(sig_q), log_signal(clocking.clock_sig));
+ log_signal(sig_d_no_x), log_signal(sig_q), log_signal(clocking.clock_sig));
+ log(" EQ with A={%s, %s}, B={0, 1}, Y=%s.\n",
+ log_signal(sig_q), log_signal(sig_d_no_x), log_signal(sig_o));
+ }
- clocking.addDff(new_verific_id(inst), sig_d, sig_q);
- module->addEq(new_verific_id(inst), {sig_q, sig_d}, Const(inst->Type() == PRIM_SVA_ROSE ? 1 : 2, 2), sig_o);
+ module->addEqx(new_verific_id(inst), sig_d, inst->Type() == PRIM_SVA_ROSE ? State::S1 : State::S0, sig_d_no_x);
+ clocking.addDff(new_verific_id(inst), sig_d_no_x, sig_q, State::S0);
+ module->addEq(new_verific_id(inst), {sig_q, sig_d_no_x}, Const(1, 2), sig_o);
if (!mode_keep)
continue;
diff --git a/tests/sva/.gitignore b/tests/sva/.gitignore
index cc254049a..b1965c97d 100644
--- a/tests/sva/.gitignore
+++ b/tests/sva/.gitignore
@@ -3,5 +3,6 @@
/*_pass
/*_fail
/*.ok
+/*.fst
/vhdlpsl[0-9][0-9]
/vhdlpsl[0-9][0-9].sby
diff --git a/tests/sva/Makefile b/tests/sva/Makefile
index 1b217f746..dcabcf42b 100644
--- a/tests/sva/Makefile
+++ b/tests/sva/Makefile
@@ -10,4 +10,5 @@ clean:
rm -rf $(addsuffix .ok,$(TESTS)) $(addsuffix .sby,$(TESTS)) $(TESTS)
rm -rf $(addsuffix _pass.sby,$(TESTS)) $(addsuffix _pass,$(TESTS))
rm -rf $(addsuffix _fail.sby,$(TESTS)) $(addsuffix _fail,$(TESTS))
+ rm -rf $(addsuffix .fst,$(TESTS))
diff --git a/tests/sva/runtest.sh b/tests/sva/runtest.sh
index 8ed7f8cbc..2ecc9780c 100644
--- a/tests/sva/runtest.sh
+++ b/tests/sva/runtest.sh
@@ -57,7 +57,9 @@ generate_sby() {
fi
}
-if [ -f $prefix.sv ]; then
+if [ -f $prefix.ys ]; then
+ $PWD/../../yosys -q -e "Assert .* failed." -s $prefix.ys
+elif [ -f $prefix.sv ]; then
generate_sby pass > ${prefix}_pass.sby
generate_sby fail > ${prefix}_fail.sby
sby --yosys $PWD/../../yosys -f ${prefix}_pass.sby
diff --git a/tests/sva/sva_value_change_changed.sv b/tests/sva/sva_value_change_changed.sv
new file mode 100644
index 000000000..8f3a05a2f
--- /dev/null
+++ b/tests/sva/sva_value_change_changed.sv
@@ -0,0 +1,17 @@
+module top (
+ input clk,
+ input a, b
+);
+ default clocking @(posedge clk); endclocking
+
+ assert property (
+ $changed(b)
+ );
+
+`ifndef FAIL
+ assume property (
+ b !== 'x ##1 $changed(b)
+ );
+`endif
+
+endmodule
diff --git a/tests/sva/sva_value_change_rose.sv b/tests/sva/sva_value_change_rose.sv
new file mode 100644
index 000000000..d1c5290f1
--- /dev/null
+++ b/tests/sva/sva_value_change_rose.sv
@@ -0,0 +1,20 @@
+module top (
+ input clk,
+ input a, b
+);
+ default clocking @(posedge clk); endclocking
+
+ wire a_copy;
+ assign a_copy = a;
+
+ assert property (
+ $rose(a) |-> b
+ );
+
+`ifndef FAIL
+ assume property (
+ $rose(a_copy) |-> b
+ );
+`endif
+
+endmodule
diff --git a/tests/sva/sva_value_change_sim.sv b/tests/sva/sva_value_change_sim.sv
new file mode 100644
index 000000000..80ff309cd
--- /dev/null
+++ b/tests/sva/sva_value_change_sim.sv
@@ -0,0 +1,51 @@
+module top (
+ input clk
+);
+
+reg [7:0] counter = 0;
+
+reg a = 0;
+reg b = 1;
+reg c;
+
+wire a_fell; assign a_fell = $fell(a, @(posedge clk));
+wire a_rose; assign a_rose = $rose(a, @(posedge clk));
+wire a_stable; assign a_stable = $stable(a, @(posedge clk));
+
+wire b_fell; assign b_fell = $fell(b, @(posedge clk));
+wire b_rose; assign b_rose = $rose(b, @(posedge clk));
+wire b_stable; assign b_stable = $stable(b, @(posedge clk));
+
+wire c_fell; assign c_fell = $fell(c, @(posedge clk));
+wire c_rose; assign c_rose = $rose(c, @(posedge clk));
+wire c_stable; assign c_stable = $stable(c, @(posedge clk));
+
+always @(posedge clk) begin
+ counter <= counter + 1;
+
+ case (counter)
+ 0: begin
+ assert property ( $fell(a) && !$rose(a) && !$stable(a));
+ assert property (!$fell(b) && $rose(b) && !$stable(b));
+ assert property (!$fell(c) && !$rose(c) && $stable(c));
+ a <= 1; b <= 1; c <= 1;
+ end
+ 1: begin a <= 0; b <= 1; c <= 'x; end
+ 2: begin
+ assert property ( $fell(a) && !$rose(a) && !$stable(a));
+ assert property (!$fell(b) && !$rose(b) && $stable(b));
+ assert property (!$fell(c) && !$rose(c) && !$stable(c));
+ a <= 0; b <= 0; c <= 0;
+ end
+ 3: begin a <= 0; b <= 1; c <= 'x; end
+ 4: begin
+ assert property (!$fell(a) && !$rose(a) && $stable(a));
+ assert property (!$fell(b) && $rose(b) && !$stable(b));
+ assert property (!$fell(c) && !$rose(c) && !$stable(c));
+ a <= 'x; b <= 'x; c <= 'x;
+ end
+ 5: begin a <= 0; b <= 1; c <= 'x; counter <= 0; end
+ endcase;
+end
+
+endmodule
diff --git a/tests/sva/sva_value_change_sim.ys b/tests/sva/sva_value_change_sim.ys
new file mode 100644
index 000000000..e004520ce
--- /dev/null
+++ b/tests/sva/sva_value_change_sim.ys
@@ -0,0 +1,3 @@
+read -sv sva_value_change_sim.sv
+hierarchy -top top
+sim -clock clk -fst sva_value_change_sim.fst
generated by cgit v1.2.3 (git 2.25.1) at 2024-09-12 18:55:27 +0000