mirror of
https://github.com/YosysHQ/yosys
synced 2025-10-31 03:32:29 +00:00
Merge pull request #3305 from jix/sva_value_change_logic
verific: Improve logic generated for SVA value change expressions
This commit is contained in:
Jannis Harder
GitHub
commit
587e09d551
8 changed files with 121 additions and 11 deletions
|
|
@ -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;
|
||||
|
|
|
|||
1
tests/sva/.gitignore
vendored
1
tests/sva/.gitignore
vendored
|
|
@ -3,5 +3,6 @@
|
|||
/*_pass
|
||||
/*_fail
|
||||
/*.ok
|
||||
/*.fst
|
||||
/vhdlpsl[0-9][0-9]
|
||||
/vhdlpsl[0-9][0-9].sby
|
||||
|
|
|
|||
|
|
@ -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))
|
||||
|
||||
|
|
|
|||
|
|
@ -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
|
||||
|
|
|
|||
17
tests/sva/sva_value_change_changed.sv
Normal file
17
tests/sva/sva_value_change_changed.sv
Normal file
|
|
@ -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
|
||||
20
tests/sva/sva_value_change_rose.sv
Normal file
20
tests/sva/sva_value_change_rose.sv
Normal file
|
|
@ -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
|
||||
51
tests/sva/sva_value_change_sim.sv
Normal file
51
tests/sva/sva_value_change_sim.sv
Normal file
|
|
@ -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
|
||||
3
tests/sva/sva_value_change_sim.ys
Normal file
3
tests/sva/sva_value_change_sim.ys
Normal file
|
|
@ -0,0 +1,3 @@
|
|||
read -sv sva_value_change_sim.sv
|
||||
hierarchy -top top
|
||||
sim -clock clk -fst sva_value_change_sim.fst
|
||||
Loading…
Add table
Add a link
Reference in a new issue