Property index 0 is greater than the number of properties in file (.btor2) #2248
Comments
|
Anything about the Formal subset of SV is not currently supported in Synlig. If you can sponsor such development we can find resources to work on it and expedite it, else it's probably years away. An other alternative is you find resources to work on it and we can guide them (for free) on how to add the support. |
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
When I refactored the property：
always @(posedge clk) begin
if (qed_ready) begin
sqed: assert ((mem1 == mem17) && (mem2 == mem18) &&
(mem3 == mem19) && (mem4 == mem20) &&
(mem5 == mem21) && (mem6 == mem22) &&
(mem7 == mem23) && (mem8 == mem24) &&
(mem9 == mem25) && (mem10 == mem26) &&
(mem11 == mem27) && (mem12 == mem28) &&
(mem13 == mem29) && (mem14 == mem30) &&
(mem15 == mem31)
);
end
end
into the following form:
property self_consistency;
@(posedge clk) qed_ready |-> ((mem1 == mem17) && (mem2 == mem18) &&
(mem3 == mem19) && (mem4 == mem20) &&
(mem5 == mem21) && (mem6 == mem22) &&
(mem7 == mem23) && (mem8 == mem24) &&
(mem9 == mem25) && (mem10 == mem26) &&
(mem11 == mem27) && (mem12 == mem28) &&
(mem13 == mem29) && (mem14 == mem30) &&
(mem15 == mem31)
);
endproperty
sqed: assert property (self_consistency);
and attempted to generate a btor2 file, an error occurred during the solving process using Pono.
The text was updated successfully, but these errors were encountered: