In reply to ben@SystemVerilog.us:
I checked, Yes, multiclocking should be supported in general.
Ben
Hi Ben,
Thanks for your reply!
I have to add a -lca option to the elaborate command for this syntax to work but in the attached waveform, the signal is still toggling at the negative edge (as seen in marker intervals).
I have a bit as a primary input to the DUT.
The only specification for this signal is that the value cannot change at the negative edge of the clock.
Sorry, you should have used the assume instead of the assert.
I still don’t understand why the signal toggles in mid-bit.
Do you have things toggling at both edges of the clock?
Why do you have this need to make this assumption?
Yes I did modify your snippet to be an assume property.
The signal in question, though being a primary input to the DUT, is actually flopped outside of the DUT – hence constraining that it should only be toggling / changing values at the posedge.
As far as I know, the DUT and the submodules within are operating on the posedge of the clock.
The behavior of the signal toggling at the negedge is most likely a result of the formal tool (VC-Formal to be exact)
In reply to erictaur:
Does it really matter if sig** is toggling at the negedge as long as setup time is abided by? Besides, Formal verification does not handle setup and hold as this is done by a static timing analyzer tool. Thus, going back to the original question: Why the need for this assumption of the sig not toggling at the midway point?
Perhaps your intend if for the signal to be stable for 2 consecutive cycles, something like:
The reason for constraining this signal is because it is messing with my helper FSMs. The next_state (being driven by combinational logic) would jump all over the place if this signal is not stable at the negedge.
For now indeed I am forcing the signal (with the following) to be high for 2 or more cycles but that snips out a portion of the valid state space.
ASSUME_FullCycle: assume property (@(posedge CCLK)
sig
|->
sig[*2:$]
);
The reason for constraining this signal is because it is messing with my helper FSMs. The next_state (being driven by combinational logic) would jump all over the place if this signal is not stable at the negedge.
I must be missing something here because support-logic driven with proper SV guidelines and synchronous to the DUT should not be dependent on setup times. Are you using nonblocking assignments? Are you using the edge of the clock in your logic?
I may be wrong, but it seems to me that something is wrong with the way you are using SystemVerilog. Typical good SystemVerilog Example:
Again, I fail to understand your need for the assume.
If I were a reviewer of your code then you better give me a good explanation.
module top;
bit clk, a, b, c, e, f;
typedef enum {A,B} AB_t;
AB_t fsm;
initial forever #10 clk = !clk;
always @(posedge clk) begin
if(a) fsm <= A;
else fsm <= B;
end
always_comb begin
if(fsm==A) c=e && f;
else c=0;
end
...
endmodule