// If (asynchronous reset & write_en) are true on the same clock, and then reset is low on the next clock,
// then the asynchronous reset gets ignored and the write_en applied
Im guessing that reset_wsync is a synchronised version of the asynchronous reset (given its name - synchronised to the write clock). Im guessing that the comments refer to the behaviour of the inputs.
If the problem is shown in the timing diagram in post #1, the only explanation i see is that reset goes to '0' just before the positive clock edge. What clock was used to do the recording?
If it was a dynamic testbench, Id say you have a delta race. Ie. reset_wsync is dropping just before the clock edge, hence it thinks a write has occured (because reset_wsync has actually dropped already).
For formal, Im wondering why you have asynchronous reset asserted at all. Have you made assumes for it?
Is this wave a counter-example where your asserts fail?
In your new example, enable and reset have no connection to each other.
In your example, if reset is high on a clock edge OR the rising edge of a reset, Q is set to 0.
I also dont understand why you have enable as the inverse of the clock. Is this set up with an assume?
You also dont show the synchroniser code.
Looking at the code, it still implies a delta race. Reset drops before the clock, and enable drops just after the clock. Hence q gets set to d
// [url]https://github.com/jbush001/NyuziProcessor/blob/master/hardware/core/synchronizer.sv[/url]//// Copyright 2011-2015 Jeff Bush//// Licensed under the Apache License, Version 2.0 (the "License");// you may not use this file except in compliance with the License.// You may obtain a copy of the License at//// [url]https://www.apache.org/licenses/LICENSE-2.0[/url]//// Unless required by applicable law or agreed to in writing, software// distributed under the License is distributed on an "AS IS" BASIS,// WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.// See the License for the specific language governing permissions and// limitations under the License.////// Transfer a signal into a clock domain, avoiding metastability and// race conditions due to propagation delay.//module synchronizer
#(parameter WIDTH =1,parameter RESET_STATE =0)(input clk,input reset,outputlogic[WIDTH -1:0] data_o,input[WIDTH -1:0] data_i);logic[WIDTH -1:0] sync0;logic[WIDTH -1:0] sync1;always_ff@(posedge clk,posedge reset)beginif(reset)begin
sync0 <={WIDTH{RESET_STATE}};
sync1 <={WIDTH{RESET_STATE}};
data_o <={WIDTH{RESET_STATE}};endelsebegin
sync0 <= data_i;
sync1 <= sync0;
data_o <= sync1;endendendmodule