Abdul-Rehman
Newbie
Hi,
I have a question about the Symbiyosys tool.
I am doing Formal Verification of UART on the Symbiyosys tool. There are 3 further modules in UART which are Baud Rate Generator, a Transmitter, and a Receiver. Let's say that UART is working on a clock named "PCLK" which is also given to the Baud Rate Generator. Baud Rate Generator generates ticks(i.e. tx_tick/rx_tick) on a specific number of clock counts depending upon the baud rate, which are given to Transmitter and Receiver as well. Transmitter and Receiver's FSM are working on tick(or changing their states on posedge of tick).
The problem with the Transmitter/Receiver's FSM is that instead of changing their states on ticks(i.e. tx_tick / rx_tick) it is changing their states on PCLK as shown in the attached waveform diagram.
Plus, We have verified UART with UVM too, it is working perfectly. It's working exactly the same as the spec says.
so, my question is how can we tell the tool that the ticks are not the same as PCLK?
I am stuck at this point. Kindly help me to get out of this problem.
Thanks.
I have a question about the Symbiyosys tool.
I am doing Formal Verification of UART on the Symbiyosys tool. There are 3 further modules in UART which are Baud Rate Generator, a Transmitter, and a Receiver. Let's say that UART is working on a clock named "PCLK" which is also given to the Baud Rate Generator. Baud Rate Generator generates ticks(i.e. tx_tick/rx_tick) on a specific number of clock counts depending upon the baud rate, which are given to Transmitter and Receiver as well. Transmitter and Receiver's FSM are working on tick(or changing their states on posedge of tick).
The problem with the Transmitter/Receiver's FSM is that instead of changing their states on ticks(i.e. tx_tick / rx_tick) it is changing their states on PCLK as shown in the attached waveform diagram.
Plus, We have verified UART with UVM too, it is working perfectly. It's working exactly the same as the spec says.
so, my question is how can we tell the tool that the ticks are not the same as PCLK?
I am stuck at this point. Kindly help me to get out of this problem.
Thanks.